diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py
index 69d3b88bb..d2c5612d7 100644
--- a/src/kontrol/cli.py
+++ b/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',
diff --git a/src/kontrol/kdist/keccak.md b/src/kontrol/kdist/keccak.md
new file mode 100644
index 000000000..993b30f85
--- /dev/null
+++ b/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
+```
\ No newline at end of file
diff --git a/src/kontrol/kdist/kontrol_lemmas.md b/src/kontrol/kdist/kontrol_lemmas.md
new file mode 100644
index 000000000..92c89251b
--- /dev/null
+++ b/src/kontrol/kdist/kontrol_lemmas.md
@@ -0,0 +1,467 @@
+Kontrol Auxiliary Lemmas
+==============
+
+The provided K Lemmas define auxiliary lemmas that facilitate reasoning in Kontrol.
+These lemmas are to be upstreamed to KEVM and removed from Kontrol once they are no longer needed.
+
+```k
+requires "foundry.md"
+
+module KONTROL-AUX-LEMMAS
+    imports EVM
+    imports FOUNDRY
+    imports INT-SYMBOLIC
+    imports MAP-SYMBOLIC
+    imports SET-SYMBOLIC
+
+    syntax StepSort ::= Int
+                      | Bool
+                      | Bytes
+                      | Map
+                      | Set
+ // -------------------------
+
+    syntax KItem ::= runLemma ( StepSort )
+                   | doneLemma( StepSort )
+ // --------------------------------------
+    rule <k> runLemma(T) => doneLemma(T) ... </k>
+
+    syntax Int ::= "ethMaxWidth" [macro]
+    syntax Int ::= "ethUpperBound" [macro]
+ // --------------------------------------
+    rule ethMaxWidth => 96
+    rule ethUpperBound => 2 ^Int ethMaxWidth
+ // ----------------------------------------
+
+    // chop and +Int
+    rule [chop-plus]: chop (A +Int B) ==Int 0 => A ==Int (-1) *Int B
+      requires #rangeUInt(256, A) andBool #rangeUInt(256, (-1) *Int B)
+      [concrete(B), simplification, comm]
+
+    // chop and -Int
+    rule [chop-zero-minus]: chop (0 -Int A) ==Int B => A ==Int (pow256 -Int B) modInt pow256
+      requires #rangeUInt(256, A) andBool #rangeUInt(256, B)
+      [concrete(B), simplification, comm, preserves-definedness]
+
+    // ==Int
+    rule [int-eq-refl]: X ==Int X => true [simplification]
+
+    // *Int
+    rule A *Int B ==Int 0 => A ==Int 0 orBool B ==Int 0 [simplification]
+
+    rule A *Int B => B *Int A [simplification(30), symbolic(A), concrete(B)]
+
+    // /Int
+    rule 0 /Int B         => 0        requires B =/=Int 0                 [simplification, preserves-definedness]
+    rule A /Int B ==Int 0 => A <Int B requires 0 <=Int A andBool 0 <Int B [simplification, preserves-definedness]
+
+    rule ( A *Int B ) /Int C => ( A /Int C ) *Int B requires A modInt C ==Int 0 [simplification, concrete(A, C), preserves-definedness]
+
+    // /Word
+    rule  _ /Word W1 => 0          requires W1  ==Int 0 [simplification]
+    rule W0 /Word W1 => W0 /Int W1 requires W1 =/=Int 0 [simplification, preserves-definedness]
+
+    // Further /Int and /Word arithmetic
+    rule ( X *Int Y ) /Int Y => X requires Y =/=Int 0              [simplification, preserves-definedness]
+    rule ( X *Int Y ) /Int X => Y requires X =/=Int 0              [simplification, preserves-definedness]
+    rule ( X ==Int ( X *Int Y ) /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness]
+    rule ( X ==Int ( Y *Int X ) /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness]
+    rule ( 0 ==Int          0   /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness]
+
+    rule A <=Int B /Int C =>         A  *Int C <=Int B requires 0 <Int C [simplification, preserves-definedness]
+    rule A  <Int B /Int C => (A +Int 1) *Int C <=Int B requires 0 <Int C [simplification, preserves-definedness]
+    rule A  >Int B /Int C =>         A  *Int C  >Int B requires 0 <Int C [simplification, preserves-definedness]
+    rule A >=Int B /Int C => (A +Int 1) *Int C  >Int B requires 0 <Int C [simplification, preserves-definedness]
+
+    rule B /Int C >=Int A =>         A  *Int C <=Int B requires 0 <Int C [simplification, preserves-definedness]
+    rule B /Int C  >Int A => (A +Int 1) *Int C <=Int B requires 0 <Int C [simplification, preserves-definedness]
+    rule B /Int C  <Int A =>         A  *Int C  >Int B requires 0 <Int C [simplification, preserves-definedness]
+    rule B /Int C <=Int A => (A +Int 1) *Int C  >Int B requires 0 <Int C [simplification, preserves-definedness]
+
+    // More specialised /Int and /Word arithmetic
+    rule ( X ==Int ( X *Int ( Y +Int C ) ) /Word ( Y +Int C ) ) orBool Y ==Int D => true
+      requires C +Int D ==Int 0 [simplification, preserves-definedness]
+
+    // modInt
+    rule (X *Int Y) modInt Z => 0 requires X modInt Z ==Int 0 [simplification, concrete(X, Z), preserves-definedness]
+
+    // Further generalization of: maxUIntXXX &Int #asWord ( BA )
+    rule X &Int #asWord ( BA ) => #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) )
+    requires #rangeUInt(256, X)
+     andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+     andBool log2Int (X +Int 1) modInt 8 ==Int 0
+     andBool (log2Int (X +Int 1)) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32
+     [simplification, concrete(X), preserves-definedness]
+
+    // #asWord
+    rule #asWord ( B1 +Bytes B2 ) => #asWord ( B2 )
+        requires #asWord ( B1 ) ==Int 0
+        [simplification, concrete(B1)]
+
+    rule #asWord( BA ) >>Int N => #asWord( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) )
+    requires 0 <=Int N andBool N modInt 8 ==Int 0
+    [simplification, concrete(N), preserves-definedness]
+
+    // >>Int
+    rule [shift-to-div]: X >>Int N => X /Int (2 ^Int N) [simplification(60), concrete(N)]
+
+    // Boolean equality
+    rule B ==K false => notBool B [simplification(30), comm]
+    rule B ==K true  =>         B [simplification(30), comm]
+
+    // bool2Word
+    rule bool2Word(X)  ==Int 0 => notBool X [simplification(30), comm]
+    rule bool2Word(X) =/=Int 0 => X         [simplification(30), comm]
+    rule bool2Word(X)  ==Int 1 => X         [simplification(30), comm]
+    rule bool2Word(X) =/=Int 1 => notBool X [simplification(30), comm]
+
+    rule [bool2Word-lt-true]:  bool2Word(_:Bool) <Int X:Int => true      requires 1 <Int X [simplification(30), concrete(X)]
+    rule [bool2Word-lt-one]:   bool2Word(B:Bool) <Int 1     => notBool B                   [simplification(30)]
+    rule [bool2Word-gt-zero]:  0 <Int bool2Word(B:Bool)     => B                           [simplification(30)]
+    rule [bool2Word-gt-false]: X:Int <Int bool2Word(_:Bool) => false     requires 1 <Int X [simplification(30), concrete(X)]
+
+    rule 0 <=Int bool2Word(X) => true [simplification, smt-lemma]
+    rule bool2Word(X) <=Int 1 => true [simplification, smt-lemma]
+
+    rule bool2Word ( X ) xorInt bool2Word ( Y ) => bool2Word ( (X andBool notBool Y) orBool (notBool X andBool Y) ) [simplification]
+    rule 1 xorInt bool2Word ( X ) => 1 -Int bool2Word ( X ) [simplification, comm]
+    rule 0 xorInt bool2Word ( X ) => bool2Word ( X ) [simplification, comm]
+
+    //
+    // .Bytes
+    //
+    rule .Bytes ==K b"" => true [simplification, comm]
+
+    rule    b"" ==K #buf(X, _) +Bytes _ => false requires 0 <Int X [simplification, concrete(X), comm]
+    rule    b"" ==K _ +Bytes #buf(X, _) => false requires 0 <Int X [simplification, concrete(X), comm]
+    rule .Bytes ==K #buf(X, _) +Bytes _ => false requires 0 <Int X [simplification, concrete(X), comm]
+    rule .Bytes ==K _ +Bytes #buf(X, _) => false requires 0 <Int X [simplification, concrete(X), comm]
+
+    rule [concat-neutral-left]:  b"" +Bytes B:Bytes => B:Bytes [simplification]
+    rule [concat-neutral-right]: B:Bytes +Bytes b"" => B:Bytes [simplification]
+
+    //
+    // Alternative memory update
+    //
+    rule [memUpdate-concat-in-right]: (B1 +Bytes B2) [ S := B ] => B1 +Bytes (B2 [ S -Int lengthBytes(B1) := B ])
+      requires lengthBytes(B1) <=Int S
+      [simplification(40)]
+
+    rule [memUpdate-concat-in-left]: (B1 +Bytes B2) [ S := B ] => (B1 [S := B]) +Bytes B2
+      requires 0 <=Int S andBool S +Int lengthBytes(B) <=Int lengthBytes(B1)
+      [simplification(45)]
+
+    //
+    // Equality of +Bytes
+    //
+    rule { B:Bytes #Equals B1:Bytes +Bytes B2:Bytes } =>
+           { #range ( B, 0, lengthBytes(B1) ) #Equals B1 } #And
+           { #range ( B, lengthBytes(B1), lengthBytes(B) -Int lengthBytes(B1) ) #Equals B2 }
+      requires lengthBytes(B1) <=Int lengthBytes(B)
+      [simplification(60), concrete(B, B1)]
+
+    rule { B1:Bytes +Bytes B2:Bytes #Equals B } =>
+           { #range ( B, 0, lengthBytes(B1) ) #Equals B1 } #And
+           { #range ( B, lengthBytes(B1), lengthBytes(B) -Int lengthBytes(B1) ) #Equals B2 }
+      requires lengthBytes(B1) <=Int lengthBytes(B)
+      [simplification(60), concrete(B, B1)]
+
+    rule { B:Bytes #Equals #buf( N, X:Int ) +Bytes B2:Bytes } =>
+           { X #Equals #asWord ( #range ( B, 0, N ) ) } #And
+           { #range ( B, N, lengthBytes(B) -Int N ) #Equals B2 }
+      requires N <=Int lengthBytes(B)
+      [simplification(60), concrete(B, N)]
+
+    rule { #buf( N, X:Int ) +Bytes B2:Bytes #Equals B } =>
+           { X #Equals #asWord ( #range ( B, 0, N ) ) } #And
+           { #range ( B, N, lengthBytes(B) -Int N ) #Equals B2 }
+      requires N <=Int lengthBytes(B)
+      [simplification(60), concrete(B, N)]
+
+    //
+    // Specific simplifications
+    //
+    rule X &Int #asWord ( BA ) ==Int Y:Int => true
+    requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+     andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+     andBool log2Int (X +Int 1) modInt 8 ==Int 0
+     andBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) ==Int Y:Int
+     [simplification, concrete(X), comm, preserves-definedness]
+
+    rule X &Int #asWord ( BA ) ==Int Y:Int => false
+    requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+     andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+     andBool log2Int (X +Int 1) modInt 8 ==Int 0
+     andBool notBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) ==Int Y:Int
+     [simplification, concrete(X), comm, preserves-definedness]
+
+    rule X &Int #asWord ( BA ) <Int Y:Int => true
+    requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+     andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+     andBool log2Int (X +Int 1) modInt 8 ==Int 0
+     andBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) <Int Y:Int
+     [simplification, concrete(X), preserves-definedness]
+
+    rule X &Int #asWord ( BA ) <Int Y:Int => false
+    requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+     andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+     andBool log2Int (X +Int 1) modInt 8 ==Int 0
+     andBool notBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) <Int Y:Int
+     [simplification, concrete(X), preserves-definedness]
+
+    rule X &Int #asWord ( BA ) <=Int Y:Int => true
+    requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+     andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+     andBool log2Int (X +Int 1) modInt 8 ==Int 0
+     andBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) <=Int Y:Int
+     [simplification, concrete(X), preserves-definedness]
+
+    rule X &Int #asWord ( BA ) <=Int Y:Int => false
+    requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+     andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+     andBool log2Int (X +Int 1) modInt 8 ==Int 0
+     andBool notBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) <=Int Y:Int
+     [simplification, concrete(X), preserves-definedness]
+
+    rule X &Int ( Y *Int Z ) => 0
+    requires 0 <=Int X andBool 0 <=Int Y andBool 0 <=Int Z
+     andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+     andBool Y ==Int 2 ^Int log2Int(Y)
+     andBool log2Int(X +Int 1) <=Int log2Int(Y)
+     [simplification, concrete(X, Y), preserves-definedness]
+
+    rule chop ( X *Int Y ) => X *Int Y
+      requires 0 <=Int X andBool X <Int ethUpperBound
+       andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 256 -Int ethMaxWidth )
+       [simplification]
+
+    rule [mul-overflow-check]:
+      X ==Int chop ( X *Int Y ) /Int Y => X *Int Y <Int pow256
+      requires #rangeUInt(256, X) andBool 0 <Int Y
+      [simplification, comm, preserves-definedness]
+
+    rule [mul-overflow-check-ML]:
+      { X #Equals chop ( X *Int Y ) /Int Y } => { true #Equals X *Int Y <Int pow256 }
+      requires #rangeUInt(256, X) andBool 0 <Int Y
+      [simplification, preserves-definedness]
+
+    rule [mul-cancel-10-le]:
+      A *Int B <=Int C *Int D => (A /Int 10) *Int B <=Int (C /Int 10) *Int D
+      requires 0 <=Int A andBool 0 <=Int C andBool A modInt 10 ==Int 0 andBool C modInt 10 ==Int 0
+      [simplification, concrete(A, C), preserves-definedness]
+
+    rule [mul-cancel-10-lt]:
+      A *Int B <Int C *Int D => (A /Int 10) *Int B <Int (C /Int 10) *Int D
+      requires 0 <=Int A andBool 0 <=Int C andBool A modInt 10 ==Int 0 andBool C modInt 10 ==Int 0
+      [simplification, concrete(A, C), preserves-definedness]
+
+    //
+    //  Overflows and ranges
+    //
+    rule X <=Int A +Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification, preserves-definedness]
+    rule X <=Int A *Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0 <=Int B [concrete(X), simplification, preserves-definedness]
+    rule X <=Int A /Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0  <Int B [concrete(X), simplification, preserves-definedness]
+
+    rule X <Int A +Int B => true requires X <=Int 0 andBool 0  <Int A andBool 0 <=Int B [concrete(X), simplification]
+    rule X <Int A +Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0  <Int B [concrete(X), simplification]
+    rule X <Int A *Int B => true requires X <=Int 0 andBool 0  <Int A andBool 0  <Int B [concrete(X), simplification]
+
+    rule [chop-no-overflow-add-l]: X:Int <=Int chop ( X +Int Y:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)             [simplification]
+    rule [chop-no-overflow-add-r]: X:Int <=Int chop ( Y +Int X:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)             [simplification]
+    rule [chop-no-overflow-mul-l]: X:Int <=Int chop ( X *Int Y:Int ) => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)             [simplification]
+    rule [chop-no-overflow-mul-r]: X:Int <=Int chop ( Y *Int X:Int ) => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)             [simplification]
+    rule [chop-no-overflow-div]:   X:Int <=Int chop ( X /Int Y:Int ) => X /Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0 <Int Y andBool Y <Int pow256 [simplification]
+
+    // Index of first bit that equals one
+    syntax Int ::=  #getFirstOneBit(Int) [function, total]
+
+    rule [gfo-succ]: #getFirstOneBit(X:Int) => log2Int ( X &Int ( ( maxUInt256 xorInt X ) +Int 1 ) ) requires          #rangeUInt(256, X) andBool X =/=Int 0
+    rule [gfo-fail]: #getFirstOneBit(X:Int) => -1                                                    requires notBool (#rangeUInt(256, X) andBool X =/=Int 0)
+
+    // Index of first bit that equals zero
+    syntax Int ::= #getFirstZeroBit(Int) [function, total]
+
+    rule [gfz-succ]: #getFirstZeroBit(X:Int) => #getFirstOneBit ( maxUInt256 xorInt X ) requires         #rangeUInt(256, X)
+    rule [gfz-fail]: #getFirstZeroBit(X:Int) => -1                                      requires notBool #rangeUInt(256, X)
+
+    // Slot updates are performed by the compiler with the help of masks,
+    // which are 256-bit integers of the form 11111111100000000000111111111111111
+    //                                                 |- WIDTH -||-   SHIFT   -|
+
+    // Shift of a mask, in bits and in bytes
+    syntax Int ::= #getMaskShiftBits(Int)  [function, total]
+    syntax Int ::= #getMaskShiftBytes(Int) [function, total]
+
+    rule [gms-bits]: #getMaskShiftBits(X:Int)  => #getFirstZeroBit(X) [concrete(X), simplification]
+
+    rule [gms-bits-succ]: #getMaskShiftBytes(X:Int) => #getFirstZeroBit(X) /Int 8 requires           #getMaskShiftBits(X) modInt 8 ==Int 0   [concrete(X), simplification, preserves-definedness]
+    rule [gms-bits-fail]: #getMaskShiftBytes(X:Int) => -1                         requires notBool ( #getMaskShiftBits(X) modInt 8 ==Int 0 ) [concrete(X), simplification, preserves-definedness]
+
+    // Width of a mask, in bits and in bytes
+    syntax Int ::= #getMaskWidthBits(Int)  [function, total]
+    syntax Int ::= #getMaskWidthBytes(Int) [function, total]
+
+    rule [gmw-bits-succ-1]: #getMaskWidthBits(X:Int) => 256 -Int #getMaskShiftBits(X:Int)             requires  0 <=Int #getMaskShiftBits(X) andBool 0 ==Int X >>Int #getMaskShiftBits(X) [concrete(X), simplification]
+    rule [gmw-bits-succ-2]: #getMaskWidthBits(X:Int) => #getFirstOneBit(X >>Int #getMaskShiftBits(X)) requires  0 <=Int #getMaskShiftBits(X) andBool 0  <Int X >>Int #getMaskShiftBits(X) [concrete(X), simplification]
+    rule [gmw-bits-fail]:   #getMaskWidthBits(X:Int) => -1                                            requires -1 ==Int #getMaskShiftBits(X) [concrete(X), simplification]
+
+    rule [gmw-bytes-succ]: #getMaskWidthBytes(X:Int) => #getMaskWidthBits(X) /Int 8 requires           #getMaskWidthBits(X) modInt 8 ==Int 0   [concrete(X), simplification, preserves-definedness]
+    rule [gmw-bytes-fail]: #getMaskWidthBytes(X:Int) => -1                          requires notBool ( #getMaskWidthBits(X) modInt 8 ==Int 0 ) [concrete(X), simplification, preserves-definedness]
+
+    // Mask recogniser
+    syntax Bool ::= #isMask(Int) [function, total]
+
+    // A number is a mask if it has a valid shift, and a valid width, and all remaining bits set to one
+    rule [is-mask-true]:
+      #isMask(X:Int) => maxUInt256 ==Int X |Int ( 2 ^Int ( #getMaskShiftBits(X) +Int #getMaskWidthBits(X) ) -Int 1 )
+        requires 0 <=Int #getMaskShiftBytes(X) andBool 0 <=Int #getMaskWidthBytes(X)
+        [concrete(X), simplification, preserves-definedness]
+
+    // and is not a mask otherwise
+    rule [is-mask-false]:
+      #isMask(X:Int) => false
+        requires notBool ( 0 <=Int #getMaskShiftBytes(X) andBool 0 <=Int #getMaskWidthBytes(X) )
+        [concrete(X), simplification, preserves-definedness]
+
+    // ###########################################################################
+    // Masking lemmas
+    // ###########################################################################
+
+    // Slot updates are of the general form (SHIFT *Int VALUE) |Int (MASK &Int #asWord( SLOT:Bytes )),
+    // andthe masking clears the part of the slot into which VALUE will be stored,
+    // and for VALUE to be stored correctly it first has to be shifted appropriately.
+    // Note that SHIFT and MASK are always concrete.
+    //
+    // We perform this update in several stages:
+    // 1. First, we simplify MASK &Int #asWord( SLOT ), which results in
+    //    ( VALUE *Int SHIFT ) |Int #asWord ( B1 +Bytes ... +Bytes BN ).
+    // 2. Then, we isolate the +Bytes-junct(s) that will be overwritten.
+    // 3. Then, we write the VALUE, possibly splitting the identified +Bytes-junct(s).
+    //
+    // Note that we require additional simplifications to account for the fact that
+    // VALUE and SLOT can also be concrete. In the former case, we need to extract the
+    // SHIFT appropriate, and in the latter case, the slot will appear on the LHS of the |Int.
+
+    // 1. Slot masking using &Int
+    rule [mask-b-and]:
+      MASK:Int &Int SLOT:Int =>
+        #asWord ( #buf ( 32, SLOT ) [ 32 -Int ( #getMaskShiftBytes(MASK) +Int #getMaskWidthBytes(MASK) ) := #buf ( #getMaskWidthBytes(MASK), 0 ) ] )
+        requires #rangeUInt(256, MASK) andBool #rangeUInt(256, SLOT)
+        andBool #isMask(MASK)
+        [simplification, concrete(MASK), preserves-definedness]
+
+    // 2a. |Int and +Bytes, update to be done in left
+    rule [bor-update-to-left]:
+      A |Int #asWord ( B1 +Bytes B2 ) =>
+        #asWord ( #buf ( 32 -Int lengthBytes(B2), (A /Int (2 ^Int (8 *Int lengthBytes(B2)))) |Int #asWord ( #buf (32 -Int (lengthBytes(B1) +Int lengthBytes(B2)), 0) +Bytes B1 ) ) +Bytes B2 )
+        requires #rangeUInt(256, A) andBool A modInt (2 ^Int (8 *Int lengthBytes(B2))) ==Int 0 andBool lengthBytes(B1 +Bytes B2) <=Int 32
+        [simplification, preserves-definedness]
+
+    // 2b. |Int of +Bytes, update to be done in right
+    rule [bor-update-to-right]:
+      A |Int #asWord ( B1 +Bytes B2 ) =>
+        #asWord ( B1 +Bytes #buf ( lengthBytes(B2), A |Int #asWord ( B2 ) ) )
+        requires 0 <=Int A andBool A <Int 2 ^Int (8 *Int lengthBytes(B2))
+        [simplification, preserves-definedness]
+
+    // 3a. Update with explicit shift and symbolic slot
+    rule [bor-update-with-shift]:
+      ( SHIFT *Int X ) |Int Y => #asWord ( #buf( 32 -Int ( log2Int(SHIFT) /Int 8 ), X ) +Bytes #buf( log2Int(SHIFT) /Int 8, Y ) )
+      requires rangeUInt(256, SHIFT) andBool SHIFT ==Int 2 ^Int log2Int(SHIFT) andBool log2Int(SHIFT) modInt 8 ==Int 0
+       andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int (32 -Int ( log2Int(SHIFT) /Int 8 )))
+       andBool 0 <=Int Y andBool Y <Int SHIFT
+       [simplification, concrete(SHIFT), comm, preserves-definedness]
+
+    // 3b. Buffer cropping
+    rule [buf-asWord-crop]:
+      #buf (W1:Int, #asWord(#buf(W2, X:Int) +Bytes B)) => #buf(W1 -Int lengthBytes(B), X) +Bytes B
+      requires 0 <=Int W1 andBool 0 <=Int W2 andBool lengthBytes(B) <=Int W1 andBool W1 <=Int W2 +Int lengthBytes(B)
+       andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int (W1 -Int lengthBytes(B)))
+      [simplification]
+
+    // 3c. Splitting the updated buffer into the updated value and the trailing zeros, explicit shift
+    rule [buf-split-l]:
+      #buf ( W, SHIFT *Int X ) => #buf( W -Int ( log2Int(SHIFT) /Int 8 ), X ) +Bytes #buf( log2Int(SHIFT) /Int 8, 0)
+      requires 0 <=Int W andBool W <=Int 32 andBool rangeUInt(256, SHIFT)
+       andBool SHIFT ==Int 2 ^Int log2Int(SHIFT)
+       andBool log2Int(SHIFT) modInt 8 ==Int 0
+       andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int (W -Int ( log2Int(SHIFT) /Int 8)))
+       [simplification, concrete(W, SHIFT), preserves-definedness]
+
+    // 3d. Splitting the updated buffer into the updated value and the trailing zeros, implicit shift
+    rule [bor-split]:
+      X |Int Y => #asWord ( #buf ( 32 -Int #getFirstOneBit(X) /Int 8, X /Int ( 2 ^Int ( 8 *Int ( #getFirstOneBit(X) /Int 8 ) ) ) ) +Bytes
+                            #buf ( #getFirstOneBit(X) /Int 8, Y ) )
+      requires #rangeUInt(256, X) andBool 0 <=Int #getFirstOneBit(X)
+       andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 8 *Int ( #getFirstOneBit(X) /Int 8 ) )
+       [simplification, concrete(X), preserves-definedness]
+
+    // 3e. Clearing update leftovers that only have bits higher than the buffer accepts
+    rule [buf-bor-subsume]:
+      #buf ( N, X |Int Y ) => #buf ( N, X )
+      requires 0 <=Int N andBool N <=Int 32
+       andBool 0 <=Int X andBool X <Int 2 ^Int ( 8 *Int N )
+       andBool Y modInt 2 ^Int ( 8 *Int N ) ==Int 0
+       [simplification, concrete(X), preserves-definedness]
+
+    //
+    // #lookup
+    //
+    rule M:Map [ K1 <- _ ] [ K1 <- V2 ]                                                                               => M:Map [ K1 <- V2 ] [simplification]
+    rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K1 <- V3 ]                                                                  => M:Map [ K2 <- V2 ] [ K1 <- V3 ] [simplification]
+    rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K3 <- V3 ] [ K1 <- V4 ]                                                     => M:Map [ K2 <- V2 ] [ K3 <- V3 ] [ K1 <- V4 ] [simplification]
+    rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K1 <- V5 ]                                        => M:Map [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K1 <- V5 ] [simplification]
+    rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K1 <- V6 ]                           => M:Map [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K1 <- V6 ] [simplification]
+    rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K6 <- V6 ] [ K1 <- V7 ]              => M:Map [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K6 <- V6 ] [ K1 <- V7 ] [simplification]
+    rule M:Map [ K1 <- _ ] [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K6 <- V6 ] [ K7 <- V7 ] [ K1 <- V8 ] => M:Map [ K2 <- V2 ] [ K3 <- V3 ] [ K4 <- V4 ] [ K5 <- V5 ] [ K6 <- V6 ] [ K7 <- V7 ] [ K1 <- V8 ] [simplification]
+
+    rule lengthBytes ( #padToWidth ( 32 , #asByteStack ( VALUE ) ) ) => 32
+        requires #rangeUInt(256, VALUE)
+        [simplification]
+
+    rule chop ( X -Int Y ) => X -Int Y
+        requires #rangeUInt(256, X)
+         andBool #rangeUInt(256, Y)
+         andBool Y <=Int X
+        [simplification]
+
+    rule X -Int Y <=Int Z => true
+        requires X <=Int Z
+         andBool 0 <=Int Y
+        [simplification, smt-lemma]
+
+    rule X modInt pow256 => X
+        requires 0 <=Int X
+         andBool X <=Int maxUInt128
+        [simplification]
+
+    rule X *Int Y <Int Z => true
+        requires #rangeUInt(256, X)
+         andBool #rangeUInt(256, Y)
+         andBool #rangeUInt(256, Z)
+         andBool X <Int 2 ^Int ( log2Int(Z) /Int 2 )
+         andBool Y <Int 2 ^Int ( log2Int(Z) /Int 2 )
+        [simplification, concrete(Z)]
+
+    //
+    // NEW LEMMAS
+    //
+
+    rule [symb-program-index]:
+      M:Bytes [ N:Int ] => #asWord ( #range(M, N, 1) )
+      requires 0 <=Int N andBool N <Int lengthBytes(M)
+      [simplification(60), symbolic(M), concrete(N), preserves-definedness]
+
+    rule bool2Word(B) *Int C <=Int A => notBool B orBool (B andBool C <=Int A)
+      requires 0 <=Int A
+      [simplification]
+
+    rule bool2Word(X) *Int Y ==Int Z => (X andBool (Y ==Int Z)) orBool ((notBool X) andBool Z ==Int 0)
+      [simplification]
+
+    rule X *Int Y <=Int Z => Y <Int ( Z +Int 1 ) /Int X
+      requires 0 <Int X andBool 0 <=Int Z andBool ( Z +Int 1) modInt X ==Int 0
+      [simplification, concrete(X, Z), preserves-definedness]
+
+endmodule
+```
\ No newline at end of file
diff --git a/src/kontrol/kompile.py b/src/kontrol/kompile.py
index eb2a1927b..de55075f6 100644
--- a/src/kontrol/kompile.py
+++ b/src/kontrol/kompile.py
@@ -57,7 +57,12 @@ 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}')
@@ -65,7 +70,7 @@ def foundry_kompile(
             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,6 +196,8 @@ 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])
@@ -196,7 +205,11 @@ def _foundry_to_main_def(
     ]
     _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(
diff --git a/src/kontrol/options.py b/src/kontrol/options.py
index ba7bd9677..c0641971f 100644
--- a/src/kontrol/options.py
+++ b/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
diff --git a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected
index ae2cb559e..4a2e880e6 100644
--- a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected
@@ -24,13 +24,13 @@
 ┃  │   statusCode: STATUSCODE:StatusCode
 ┃  │   method: test%CSETest.test_add_const(uint256,uint256)
 ┃  │
-┃  │  (464 steps)
+┃  │  (193 steps)
 ┃  └─ 12 (vacuous, leaf)
-┃      k: #execute ~> #return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K
-┃      pc: 0
-┃      callDepth: 1
+┃      k: #assume ( VV0_x_114b9705:Int <Int pow64 ) ~> #cheatcode_return 128 0 ~> #pc [ ST ...
+┃      pc: 737
+┃      callDepth: 0
 ┃      statusCode: STATUSCODE:StatusCode
-┃      method: src%cse%AddConst.setConst(uint256)
+┃      method: test%CSETest.test_add_const(uint256,uint256)
 ┃
 ┗━━┓ constraint: VV0_x_114b9705:Int <Int pow64
    │
@@ -67,9 +67,9 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0
            <kevm>
              <k>
                ( JUMPI 678 bool2Word ( pow64 <=Int VV0_x_114b9705:Int )
-               ~> #pc [ JUMPI ] => #execute
-               ~> #return 128 0
-               ~> #pc [ CALL ] )
+               ~> #pc [ JUMPI ] => #assume ( VV0_x_114b9705:Int <Int pow64 )
+               ~> #cheatcode_return 128 0
+               ~> #pc [ STATICCALL ] )
                ~> #execute
                ~> _CONTINUATION
              </k>
@@ -88,190 +88,32 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0
                    b""
                  </output>
                  <callStack>
-                   ( .List => ListItem ( <callState>
-                     <id>
-                       728815563385977040452943777879061427756277306518
-                     </id>
-                     <caller>
-                       CALLER_ID:Int
-                     </caller>
-                     <callData>
-                       b"\x0f\xee)\xd1" +Bytes #buf ( 32 , VV0_x_114b9705:Int ) +Bytes #buf ( 32 , VV1_y_114b9705:Int )
-                     </callData>
-                     <callValue>
-                       0
-                     </callValue>
-                     <wordStack>
-                       ( 164 : ( selector ( "setConst(uint256)" ) : ( 263400868551549723330807389252719309078400616203 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 220 : ( selector ( "test_add_const(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) )
-                     </wordStack>
-                     <localMem>
-                       b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe9\x19\xcf\x83" +Bytes #buf ( 32 , VV0_x_114b9705:Int )
-                     </localMem>
-                     <memoryUsed>
-                       0
-                     </memoryUsed>
-                     <callGas>
-                       0
-                     </callGas>
-                     <static>
-                       false
-                     </static>
-                     <callDepth>
-                       0
-                     </callDepth>
-                     ...
-                   </callState> ) )
+                   .List
                  </callStack>
                  <interimStates>
-                   ( .List => ListItem ( { <accounts>
-                     ( <account>
-                       <acctID>
-                         1405310203571408291950365054053061012934685786634
-                       </acctID>
-                       <balance>
-                         0
-                       </balance>
-                       <storage>
-                         .Map
-                       </storage>
-                       <origStorage>
-                         .Map
-                       </origStorage>
-                       <transientStorage>
-                         .Map
-                       </transientStorage>
-                       <nonce>
-                         1
-                       </nonce>
-                       ...
-                     </account>
-                     ( <account>
-                       <acctID>
-                         263400868551549723330807389252719309078400616203
-                       </acctID>
-                       <balance>
-                         0
-                       </balance>
-                       <storage>
-                         .Map
-                       </storage>
-                       <origStorage>
-                         .Map
-                       </origStorage>
-                       <transientStorage>
-                         .Map
-                       </transientStorage>
-                       <nonce>
-                         1
-                       </nonce>
-                       ...
-                     </account>
-                     ( <account>
-                       <acctID>
-                         491460923342184218035706888008750043977755113263
-                       </acctID>
-                       <balance>
-                         0
-                       </balance>
-                       <storage>
-                         .Map
-                       </storage>
-                       <origStorage>
-                         .Map
-                       </origStorage>
-                       <transientStorage>
-                         .Map
-                       </transientStorage>
-                       <nonce>
-                         1
-                       </nonce>
-                       ...
-                     </account>
-                     ( <account>
-                       <acctID>
-                         645326474426547203313410069153905908525362434349
-                       </acctID>
-                       <balance>
-                         0
-                       </balance>
-                       <storage>
-                         .Map
-                       </storage>
-                       <origStorage>
-                         .Map
-                       </origStorage>
-                       <transientStorage>
-                         .Map
-                       </transientStorage>
-                       <nonce>
-                         0
-                       </nonce>
-                       ...
-                     </account>
-                     <account>
-                       <acctID>
-                         728815563385977040452943777879061427756277306518
-                       </acctID>
-                       <balance>
-                         0
-                       </balance>
-                       <storage>
-                         ( ( 11 |-> 1 )
-                         ( ( 27 |-> 491460923342184218035706888008750043977755113263 )
-                         ( ( 28 |-> 263400868551549723330807389252719309078400616203 )
-                         ( ( 29 |-> 1405310203571408291950365054053061012934685786634 )
-                         ( 7 |-> 1 ) ) ) ) )
-                       </storage>
-                       <origStorage>
-                         .Map
-                       </origStorage>
-                       <transientStorage>
-                         .Map
-                       </transientStorage>
-                       <nonce>
-                         4
-                       </nonce>
-                       ...
-                     </account> ) ) ) )
-                   </accounts> | <substate>
-                     <selfDestruct>
-                       SELFDESTRUCT_CELL:Set
-                     </selfDestruct>
-                     <log>
-                       .List
-                     </log>
-                     <refund>
-                       0
-                     </refund>
-                     <accessedAccounts>
-                       ( SetItem ( 263400868551549723330807389252719309078400616203 ) SetItem ( 645326474426547203313410069153905908525362434349 ) )
-                     </accessedAccounts>
-                     <accessedStorage>
-                       .Map
-                     </accessedStorage>
-                   </substate> } ) )
+                   .List
                  </interimStates>
                  <touchedAccounts>
-                   ( .Set => ( SetItem ( 263400868551549723330807389252719309078400616203 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) )
+                   .Set
                  </touchedAccounts>
                  <callState>
                    <id>
-                     ( 728815563385977040452943777879061427756277306518 => 263400868551549723330807389252719309078400616203 )
+                     728815563385977040452943777879061427756277306518
                    </id>
                    <caller>
-                     ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 )
+                     CALLER_ID:Int
                    </caller>
                    <callData>
-                     ( b"\x0f\xee)\xd1" => b"\xe9\x19\xcf\x83" ) +Bytes #buf ( 32 , VV0_x_114b9705:Int ) +Bytes ( #buf ( 32 , VV1_y_114b9705:Int ) => b"" )
+                     b"\x0f\xee)\xd1" +Bytes #buf ( 32 , VV0_x_114b9705:Int ) +Bytes #buf ( 32 , VV1_y_114b9705:Int )
                    </callData>
                    <callValue>
                      0
                    </callValue>
                    <wordStack>
-                     ( ( bool2Word ( VV0_x_114b9705:Int <Int pow64 ) : ( selector ( "assume(bool)" ) : ( 645326474426547203313410069153905908525362434349 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 220 : ( selector ( "test_add_const(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) => .WordStack )
+                     ( ( bool2Word ( VV0_x_114b9705:Int <Int pow64 ) => 164 ) : ( selector ( "assume(bool)" ) : ( 645326474426547203313410069153905908525362434349 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 220 : ( selector ( "test_add_const(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" => b"" )
+                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_x_114b9705:Int <Int pow64 ) ) )
                    </localMem>
                    <memoryUsed>
                      0
@@ -283,14 +125,11 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0
                      false
                    </static>
                    <callDepth>
-                     ( 0 => 1 )
+                     0
                    </callDepth>
                    ...
                  </callState>
                  <substate>
-                   <selfDestruct>
-                     SELFDESTRUCT_CELL:Set
-                   </selfDestruct>
                    <log>
                      .List
                    </log>
@@ -298,11 +137,12 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0
                      0
                    </refund>
                    <accessedAccounts>
-                     ( .Set => ( SetItem ( 263400868551549723330807389252719309078400616203 ) ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) )
+                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   ...
                  </substate>
                  <origin>
                    ORIGIN_ID:Int
@@ -526,7 +366,6 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
                )))))))))))))))))
-       ensures #buf ( 32 , bool2Word ( VV0_x_114b9705:Int <Int pow64 ) ) +Bytes b"" ~> .K ==K b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ~> .K
       [priority(20), label(BASIC-BLOCK-10-TO-12)]
     
     rule [BASIC-BLOCK-11-TO-13]: <foundry>
diff --git a/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected
index 45bd58f8b..b7fe53771 100644
--- a/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected
@@ -24,13 +24,13 @@
 ┃  │   statusCode: STATUSCODE:StatusCode
 ┃  │   method: test%CSETest.test_identity(uint256,uint256)
 ┃  │
-┃  │  (412 steps)
+┃  │  (193 steps)
 ┃  └─ 12 (vacuous, leaf)
-┃      k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
-┃      pc: 0
-┃      callDepth: 1
+┃      k: #assume ( VV0_x_114b9705:Int <Int pow64 ) ~> #cheatcode_return 128 0 ~> #pc [ ST ...
+┃      pc: 2578
+┃      callDepth: 0
 ┃      statusCode: STATUSCODE:StatusCode
-┃      method: src%cse%Identity.applyOp(uint256)
+┃      method: test%CSETest.test_identity(uint256,uint256)
 ┃
 ┗━━┓ constraint: VV0_x_114b9705:Int <Int pow64
    │
@@ -67,8 +67,8 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0
            <kevm>
              <k>
                ( JUMPI 2519 bool2Word ( pow64 <=Int VV0_x_114b9705:Int )
-               ~> #pc [ JUMPI ] => #execute
-               ~> #return 128 32
+               ~> #pc [ JUMPI ] => #assume ( VV0_x_114b9705:Int <Int pow64 )
+               ~> #cheatcode_return 128 0
                ~> #pc [ STATICCALL ] )
                ~> #execute
                ~> _CONTINUATION
@@ -88,190 +88,32 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0
                    b""
                  </output>
                  <callStack>
-                   ( .List => ListItem ( <callState>
-                     <id>
-                       728815563385977040452943777879061427756277306518
-                     </id>
-                     <caller>
-                       CALLER_ID:Int
-                     </caller>
-                     <callData>
-                       b"\xc0\xbd\x83$" +Bytes #buf ( 32 , VV0_x_114b9705:Int ) +Bytes #buf ( 32 , VV1_y_114b9705:Int )
-                     </callData>
-                     <callValue>
-                       0
-                     </callValue>
-                     <wordStack>
-                       ( 164 : ( selector ( "applyOp(uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 220 : ( selector ( "test_identity(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) )
-                     </wordStack>
-                     <localMem>
-                       b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00i\xab\xff\xa1" +Bytes #buf ( 32 , VV1_y_114b9705:Int )
-                     </localMem>
-                     <memoryUsed>
-                       0
-                     </memoryUsed>
-                     <callGas>
-                       0
-                     </callGas>
-                     <static>
-                       false
-                     </static>
-                     <callDepth>
-                       0
-                     </callDepth>
-                     ...
-                   </callState> ) )
+                   .List
                  </callStack>
                  <interimStates>
-                   ( .List => ListItem ( { <accounts>
-                     ( <account>
-                       <acctID>
-                         1405310203571408291950365054053061012934685786634
-                       </acctID>
-                       <balance>
-                         0
-                       </balance>
-                       <storage>
-                         .Map
-                       </storage>
-                       <origStorage>
-                         .Map
-                       </origStorage>
-                       <transientStorage>
-                         .Map
-                       </transientStorage>
-                       <nonce>
-                         1
-                       </nonce>
-                       ...
-                     </account>
-                     ( <account>
-                       <acctID>
-                         263400868551549723330807389252719309078400616203
-                       </acctID>
-                       <balance>
-                         0
-                       </balance>
-                       <storage>
-                         .Map
-                       </storage>
-                       <origStorage>
-                         .Map
-                       </origStorage>
-                       <transientStorage>
-                         .Map
-                       </transientStorage>
-                       <nonce>
-                         1
-                       </nonce>
-                       ...
-                     </account>
-                     ( <account>
-                       <acctID>
-                         491460923342184218035706888008750043977755113263
-                       </acctID>
-                       <balance>
-                         0
-                       </balance>
-                       <storage>
-                         .Map
-                       </storage>
-                       <origStorage>
-                         .Map
-                       </origStorage>
-                       <transientStorage>
-                         .Map
-                       </transientStorage>
-                       <nonce>
-                         1
-                       </nonce>
-                       ...
-                     </account>
-                     ( <account>
-                       <acctID>
-                         645326474426547203313410069153905908525362434349
-                       </acctID>
-                       <balance>
-                         0
-                       </balance>
-                       <storage>
-                         .Map
-                       </storage>
-                       <origStorage>
-                         .Map
-                       </origStorage>
-                       <transientStorage>
-                         .Map
-                       </transientStorage>
-                       <nonce>
-                         0
-                       </nonce>
-                       ...
-                     </account>
-                     <account>
-                       <acctID>
-                         728815563385977040452943777879061427756277306518
-                       </acctID>
-                       <balance>
-                         0
-                       </balance>
-                       <storage>
-                         ( ( 11 |-> 1 )
-                         ( ( 27 |-> 491460923342184218035706888008750043977755113263 )
-                         ( ( 28 |-> 263400868551549723330807389252719309078400616203 )
-                         ( ( 29 |-> 1405310203571408291950365054053061012934685786634 )
-                         ( 7 |-> 1 ) ) ) ) )
-                       </storage>
-                       <origStorage>
-                         .Map
-                       </origStorage>
-                       <transientStorage>
-                         .Map
-                       </transientStorage>
-                       <nonce>
-                         4
-                       </nonce>
-                       ...
-                     </account> ) ) ) )
-                   </accounts> | <substate>
-                     <selfDestruct>
-                       SELFDESTRUCT_CELL:Set
-                     </selfDestruct>
-                     <log>
-                       .List
-                     </log>
-                     <refund>
-                       0
-                     </refund>
-                     <accessedAccounts>
-                       ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 645326474426547203313410069153905908525362434349 ) )
-                     </accessedAccounts>
-                     <accessedStorage>
-                       .Map
-                     </accessedStorage>
-                   </substate> } ) )
+                   .List
                  </interimStates>
                  <touchedAccounts>
-                   ( .Set => ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) )
+                   .Set
                  </touchedAccounts>
                  <callState>
                    <id>
-                     ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
+                     728815563385977040452943777879061427756277306518
                    </id>
                    <caller>
-                     ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 )
+                     CALLER_ID:Int
                    </caller>
                    <callData>
-                     ( b"\xc0\xbd\x83$" => b"i\xab\xff\xa1" ) +Bytes #buf ( 32 , ( VV0_x_114b9705:Int => VV1_y_114b9705:Int ) ) +Bytes ( #buf ( 32 , VV1_y_114b9705:Int ) => b"" )
+                     b"\xc0\xbd\x83$" +Bytes #buf ( 32 , VV0_x_114b9705:Int ) +Bytes #buf ( 32 , VV1_y_114b9705:Int )
                    </callData>
                    <callValue>
                      0
                    </callValue>
                    <wordStack>
-                     ( ( bool2Word ( VV0_x_114b9705:Int <Int pow64 ) : ( selector ( "assume(bool)" ) : ( 645326474426547203313410069153905908525362434349 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 220 : ( selector ( "test_identity(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) => .WordStack )
+                     ( ( bool2Word ( VV0_x_114b9705:Int <Int pow64 ) => 164 ) : ( selector ( "assume(bool)" ) : ( 645326474426547203313410069153905908525362434349 : ( VV1_y_114b9705:Int : ( VV0_x_114b9705:Int : ( 220 : ( selector ( "test_identity(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" => b"" )
+                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_x_114b9705:Int <Int pow64 ) ) )
                    </localMem>
                    <memoryUsed>
                      0
@@ -280,17 +122,14 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0
                      0
                    </callGas>
                    <static>
-                     ( false => true )
+                     false
                    </static>
                    <callDepth>
-                     ( 0 => 1 )
+                     0
                    </callDepth>
                    ...
                  </callState>
                  <substate>
-                   <selfDestruct>
-                     SELFDESTRUCT_CELL:Set
-                   </selfDestruct>
                    <log>
                      .List
                    </log>
@@ -298,11 +137,12 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0
                      0
                    </refund>
                    <accessedAccounts>
-                     ( .Set => ( SetItem ( 491460923342184218035706888008750043977755113263 ) ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) )
+                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
                    </accessedStorage>
+                   ...
                  </substate>
                  <origin>
                    ORIGIN_ID:Int
@@ -526,7 +366,6 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
                )))))))))))))))))
-       ensures #buf ( 32 , bool2Word ( VV0_x_114b9705:Int <Int pow64 ) ) +Bytes b"" ~> .K ==K b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ~> .K
       [priority(20), label(BASIC-BLOCK-10-TO-12)]
     
     rule [BASIC-BLOCK-11-TO-13]: <foundry>
diff --git a/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected b/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected
index bbd723d4a..812708b8e 100644
--- a/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected
+++ b/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected
@@ -271,7 +271,6 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < C_ENUM_MEMBER_CONTRACT_ID:Int <= 9 ) )
                ))))))))))))))))))))))))))))))))))
-       ensures #lookup ( C_ENUM_MEMBER_CONTRACT_STORAGE:Map , 1 ) <=Int 5
       [priority(20), label(BASIC-BLOCK-8-TO-6)]
     
     rule [BASIC-BLOCK-9-TO-7]: <foundry>
diff --git a/src/tests/integration/test-data/show/Enum.init.cse.expected b/src/tests/integration/test-data/show/Enum.init.cse.expected
index 82c446478..8615c5600 100644
--- a/src/tests/integration/test-data/show/Enum.init.cse.expected
+++ b/src/tests/integration/test-data/show/Enum.init.cse.expected
@@ -198,7 +198,6 @@ module SUMMARY-TEST%ENUM.INIT:0
        andBool ( ( notBool #range ( 0 < C_ENUM_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
                )))))))))))))))))))))))))
-       ensures V0_letter:Int <=Int 5
       [priority(20), label(BASIC-BLOCK-1-TO-3)]
 
 endmodule
\ No newline at end of file
diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
index 2e72b0bb3..dd1c6d260 100644
--- a/src/tests/integration/test-data/show/foundry.k.expected
+++ b/src/tests/integration/test-data/show/foundry.k.expected
@@ -3,6 +3,7 @@ requires "requires/lemmas.k"
 requires "requires/cse-lemmas.k"
 requires "requires/pausability-lemmas.k"
 requires "requires/symbolic-bytes-lemmas.k"
+requires "requires/keccak.md"
 
 module FOUNDRY-MAIN
     imports public S2KsrcZModduplicatesZMod2ZModDuplicateName-VERIFICATION
@@ -160,6 +161,7 @@ module FOUNDRY-MAIN
     imports public S2KlibZModforgeZSubstdZModsrcZModconsole2-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModsrcZModsafeconsole-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION
+    imports public KECCAK-LEMMAS
     
     
 
diff --git a/src/tests/integration/test-data/symbolic-bytes-lemmas.k b/src/tests/integration/test-data/symbolic-bytes-lemmas.k
index 4e0857d1a..abc913dfa 100644
--- a/src/tests/integration/test-data/symbolic-bytes-lemmas.k
+++ b/src/tests/integration/test-data/symbolic-bytes-lemmas.k
@@ -7,6 +7,12 @@ module SYMBOLIC-BYTES-LEMMAS
     imports INFINITE-GAS
     imports INT-SYMBOLIC
 
+    //
+    // Neutrality of b""
+    //
+    rule B   +Bytes b"" => B [simplification]
+    rule b"" +Bytes B   => B [simplification]
+
     //
     // Byte indexing in terms of #asWord
     //