Include keccak & aux lemmas conditionally

src/kontrol/cli.py

@@ -343,6 +343,20 @@ def parse(s: str) -> list[T]:
         action='store_true',
         help='Do not append cbor or bytecode_hash metadata to bytecode.',
     )
+    build.add_argument(
+        '--no-keccak-lemmas',
+        dest='keccak_lemmas',
+        default=None,
+        action='store_false',
+        help='Do not include assumptions on keccak properties.',
+    )
+    build.add_argument(
+        '--no-auxiliary-lemmas',
+        dest='auxiliary_lemmas',
+        default=None,
+        action='store_false',
+        help='Do not include auxiliary Kontrol lemmas.',
+    )
 
     state_diff_args = command_parser.add_parser(
         'load-state',

src/kontrol/kdist/keccak.md

@@ -0,0 +1,62 @@
+Keccak Assumptions
+==============
+
+The provided K Lemmas define assumptions and properties related to the keccak hash function used in the verification of smart contracts within the symbolic execution context.
+
+```k
+module KECCAK-LEMMAS
+    imports FOUNDRY
+    imports INT-SYMBOLIC
+```
+
+1. The result of the `keccak` function is always a non-negative integer, and it is always less than 2^256.
+
+```k
+    rule 0 <=Int keccak( _ )             => true [simplification, smt-lemma]
+    rule         keccak( _ ) <Int pow256 => true [simplification, smt-lemma]
+```
+
+2. The result of the `keccak` function applied on a symbolic input does not equal any concrete value.
+
+```k
+    // keccak does not equal a concrete value
+    rule [keccak-eq-conc-false]: keccak(_A)  ==Int _B => false [symbolic(_A), concrete(_B), simplification(30), comm]
+    rule [keccak-neq-conc-true]: keccak(_A) =/=Int _B => true  [symbolic(_A), concrete(_B), simplification(30), comm]
+```
+
+In addition, equality involving keccak of a symbolic variable is reduced to a comparison that always results in `false` for concrete values.
+
+```k
+    rule [keccak-eq-conc-false-ml-lr]: { keccak(A) #Equals B } => { true #Equals keccak(A) ==Int B } [symbolic(A), concrete(B), simplification]
+    rule [keccak-eq-conc-false-ml-rl]: { B #Equals keccak(A) } => { true #Equals keccak(A) ==Int B } [symbolic(A), concrete(B), simplification]
+```
+
+3. Injectivity of Keccak. If `keccak(A)` equals `keccak(B)`, then `A` must equal `B`.
+
+In reality, cryptographic hash functions like `keccak` are not injective. They are designed to be collision-resistant, meaning it is computationally infeasible to find two different inputs that produce the same hash output, but not impossible.
+The assumption of injectivity simplifies reasoning about the keccak function in formal verification, but it is not fundamentally true. It is used to aid in the verification process.
+
+```k
+    // keccak is injective
+    rule [keccak-inj]: keccak(A) ==Int keccak(B) => A ==K B [simplification]
+    rule [keccak-inj-ml]: { keccak(A) #Equals keccak(B) } => { true #Equals A ==K B } [simplification]
+```
+
+4. Negating keccak. Instead of allowing a negative value, the rule adjusts it within the valid range, ensuring the value remains non-negative.
+
+```k
+    // chop of negative keccak
+    rule chop (0 -Int keccak(BA)) => pow256 -Int keccak(BA)
+       [simplification]
+```
+
+5. Ensure that any value resulting from a `keccak` is within the valid range of 0 and 2^256 - 1.
+
+```k
+    // keccak cannot equal a number outside of its range
+    rule { X #Equals keccak (_) } => #Bottom
+      requires X <Int 0 orBool X >=Int pow256
+      [concrete(X), simplification]
+
+endmodule
+```

src/kontrol/kompile.py

@@ -57,15 +57,20 @@ def foundry_kompile(
         regen = True
         foundry_up_to_date = False
 
-    for r in options.requires:
+    requires = (
+        options.requires
+        + ([KSRC_DIR / 'keccak.md'] if options.keccak_lemmas else [])
+        + ([KSRC_DIR / 'kontrol_lemmas.md'] if options.auxiliary_lemmas else [])
+    )
+    for r in tuple(requires):
         req = Path(r)
         if not req.exists():
             raise ValueError(f'No such file: {req}')
         if req.name in requires_paths.keys():
             raise ValueError(
                 f'Required K files have conflicting names: {r} and {requires_paths[req.name]}. Consider changing the name of one of these files.'
             )
-        requires_paths[req.name] = r  # noqa: B909
+        requires_paths[req.name] = str(r)
         req_path = foundry_requires_dir / req.name
         if regen or not req_path.exists():
             _LOGGER.info(f'Copying requires path: {req} -> {req_path}')
@@ -86,7 +91,7 @@ def foundry_kompile(
     if regen or not foundry_contracts_file.exists() or not foundry.main_file.exists():
         if regen and foundry_up_to_date:
             console.print(
-                f'[{_rv_blue()}][bold]--regen[/bold] option provied. Rebuilding Kontrol Project.[/{_rv_blue()}]'
+                f'[{_rv_blue()}][bold]--regen[/bold] option provided. Rebuilding Kontrol Project.[/{_rv_blue()}]'
             )
 
         copied_requires = []
@@ -106,6 +111,8 @@ def foundry_kompile(
             contracts=foundry.contracts.values(),
             requires=(['contracts.k'] + copied_requires),
             imports=_imports,
+            keccak_lemmas=options.keccak_lemmas,
+            auxiliary_lemmas=options.auxiliary_lemmas,
         )
 
         kevm = KEVM(
@@ -189,14 +196,20 @@ def _foundry_to_main_def(
     empty_config: KInner,
     requires: Iterable[str],
     imports: dict[str, list[str]],
+    keccak_lemmas: bool,
+    auxiliary_lemmas: bool,
 ) -> KDefinition:
     modules = [
         contract_to_verification_module(contract, empty_config, imports=imports[contract.name_with_path])
         for contract in contracts
     ]
     _main_module = KFlatModule(
         main_module,
-        imports=(KImport(mname) for mname in [_m.name for _m in modules]),
+        imports=tuple(
+            [KImport(mname) for mname in (_m.name for _m in modules)]
+            + ([KImport('KECCAK-LEMMAS')] if keccak_lemmas else [])
+            + ([KImport('KONTROL-AUX-LEMMAS')] if auxiliary_lemmas else [])
+        ),
     )
 
     return KDefinition(

src/kontrol/options.py

@@ -821,6 +821,8 @@ class BuildOptions(LoggingOptions, KOptions, KGenOptions, KompileOptions, Foundr
     no_forge_build: bool
     no_silence_warnings: bool
     no_metadata: bool
+    keccak_lemmas: bool
+    auxiliary_lemmas: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -830,6 +832,8 @@ def default() -> dict[str, Any]:
             'no_forge_build': False,
             'no_silence_warnings': False,
             'no_metadata': False,
+            'keccak_lemmas': True,
+            'auxiliary_lemmas': True,
         }
 
     @staticmethod