Include keccak & aux lemmas conditionally (#779)

* Add `--no-keccak-lemmas` option for conditional exclusion of keccak assumptions

* Use `KSRC_DIR` to access `keccak.md`

* Code quality adjustment

* Add aux Kontrol lemmas, update output

* `/Int` lemmas fix

* Update CSE output

* Move `keccak` lemma

* Turn off aux lemmas by default

* keccak lemmas

* two more lemmas

* correction

* expected output update

* Another output update

* Update `TGovernance` output

---------

Co-authored-by: Petar Maksimovic <petar.maksimovic@runtimeverification.com>

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(
+        '--auxiliary-lemmas',
+        dest='auxiliary_lemmas',
+        default=None,
+        action='store_true',
+        help='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. `keccak` always returns an integer in the range `[0, 2 ^ 256)`.
+
+```k
+    rule 0 <=Int keccak( _ )             => true [simplification, smt-lemma]
+    rule         keccak( _ ) <Int pow256 => true [simplification, smt-lemma]
+```
+
+2. No value outside of the `[0, 2 ^ 256)` range can be the result of a `keccak`.
+
+```k
+    rule [keccak-out-of-range]:      X  ==Int  keccak (_)   => false   requires X <Int 0 orBool X >=Int pow256 [concrete(X), simplification]
+    rule [keccak-out-of-range-ml]: { X #Equals keccak (_) } => #Bottom requires X <Int 0 orBool X >=Int pow256 [concrete(X), simplification]
+```
+
+3. This lemma directly simplifies an expression that involves a `keccak` and is often introduced by the Solidity compiler.
+
+```k
+    rule chop (0 -Int keccak(BA)) => pow256 -Int keccak(BA)
+       [simplification]
+```
+
+4. The result of a `keccak` is assumed not to fall too close to the edges of its official range. This accounts for the shifts added to the result of a `keccak` when accessing storage slots, and is a hypothesis made by the ecosystem.
+
+```k
+    rule BOUND:Int <Int keccak(B:Bytes) => true requires BOUND <=Int 32             [simplification, concrete(BOUND)]
+    rule keccak(B:Bytes) <Int BOUND:Int => true requires BOUND >=Int pow256 -Int 32 [simplification, concrete(BOUND)]
+```
+
+5. `keccak` is injective: that is, if `keccak(A)` equals `keccak(B)`, then `A` equals `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.
+This assumption reflects that hypothesis in the context of formal verification, making it more tractable.
+
+```k
+    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]
+```
+
+6. `keccak` of a symbolic parameter does not equal a concrete value. This lemma is based on our experience in Foundry-supported testing and is specific to how `keccak` functions are used in practical symbolic execution. The underlying hypothesis that justifies it is that the storage slots of a given mapping are presumed to be disjoint from slots of other mappings and also the non-mapping slots of a contract.
+
+```k
+    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]
+
+    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]
+```
+
+```k
+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': False,
         }
 
     @staticmethod