Lemmas on Boolean reasoning, set reasoning, map lookup (#2037)

* lemmas on Boolean reasoning, set reasoning, map lookup, and keccak * Set Version: 1.0.277 * removing keccak lemmas that should not be upstreamed * addressing comments * Set Version: 1.0.278 * Set Version: 1.0.278 * corrections * removing ==Bool from expected files * Set Version: 1.0.279 * Set Version: 1.0.279 * Set Version: 1.0.309 * Set Version: 1.0.311 * updating expected outputs * Set Version: 1.0.312 * Set Version: 1.0.330 * Set Version: 1.0.334 * revisiting set simplifications * --amend * --amend * --amend * streamlining lookup simplifications * streamlining set simplifications * removing set reasoning entirely * Set Version: 1.0.336 * concretising set simplifications: * streamlining set simplifications * Set Version: 1.0.337 * even more concrete set simplifications * bringing old simplifications back * Set Version: 1.0.340 * resolving parsing ambiguities * --amend * --amend * Set Version: 1.0.341 * Set Version: 1.0.342 * Set Version: 1.0.343 * correction * syntax * --amend * Set Version: 1.0.349 * Set Version: 1.0.355 * Set Version: 1.0.356 * Set Version: 1.0.357 * Correctly ordered arguments in `typed_args` (#2174) * Correctly ordered arguments in `typed_args` * Set Version: 1.0.357 --------- Co-authored-by: devops <devops@runtimeverification.com> * Inject `ccopts` directly into `kevm_kompile` and fix some tests (#2164) * Makefile: make sure evm-optimizations-spec is rebuilt on changes to optimizations.md * kproj/optimizations: remove symbolic attribute on evm-optimizations-lemmas * tests/specs/examples/sum-to-n-foundry-spec: correct imports for LLVM backend * tests/specs/functional/infinite-gas-spec.k: allow import of main module in symbolic module for LLVM * kevm-pyk/__main__, Makefile, VERIFICATION: rename kevm {kompile => kompile-spec} for more accurate usage * README: update documentation * kevm-pyk/: all builds require plugin_dir, compute it directly * kevm-pyk/: move calculation of plugin_dir out of run_kompile, pass in ccopts directly * kevm-pyk/__main__: adjust acceptable values for kevm kompile-spec * VERIFICATION: update documentation * Makefile: bring back --target argument * Set Version: 1.0.343 * test_prove: only add ccopts if were using the booster * Set Version: 1.0.355 * package/test-package: add previously failing test of using booster due to plugin_dir being missing * kevm-pyk/__main__: use correct target for kompile-spec * Set Version: 1.0.356 * Set Version: 1.0.356 * kevm-pyk/plugin: correction from code review * kevm-pyk/kdist/plugin: hardcode plugin as dependency for other targets * kevm-pyk/: factor out generic run_kompile from kevm_kompile * kevm_pyk/kompile: rename lib_ccopts => _lib_ccopts * Set Version: 1.0.357 * kevm-pyk/kdist/plugin: make sure all KEVMTarget have plugin as depenndency * Set Version: 1.0.357 * kdist/plugin: drop self._deps * Set Version: 1.0.358 * Set Version: 1.0.358 --------- Co-authored-by: devops <devops@runtimeverification.com> * Fix circular import (#2179) * Fix circular import * Set Version: 1.0.359 --------- Co-authored-by: devops <devops@runtimeverification.com> * Move `--port` arguments to `rpc_args` (#2178) * Move `--port` arguments to `rpc_args` * Set Version: 1.0.359 * Set Version: 1.0.360 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * Update dependency: deps/pyk_release (#2175) * deps/pyk_release: Set Version v0.1.501 * Set Version: 1.0.357 * kevm-pyk/: sync poetry files pyk version v0.1.501 * deps/k_release: sync release file version 6.1.14 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.359 * kevm-pyk/: sync poetry files pyk version v0.1.501 * Set Version: 1.0.361 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * Update dependency: deps/pyk_release (#2181) * deps/pyk_release: Set Version v0.1.505 * kevm-pyk/: sync poetry files pyk version v0.1.505 * deps/k_release: sync release file version 6.1.20 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.362 --------- Co-authored-by: devops <devops@runtimeverification.com> * Set Version: 1.0.364 * Set Version: 1.0.364 * Set Version: 1.0.365 * Set Version: 1.0.372 * Set Version: 1.0.379 * adding tests * Set Version: 1.0.381 * normalising comparisons, adding keccak * reverting normalisation * removing equality simplification * Set Version: 1.0.382 * Set Version: 1.0.382 * bringing back comparison (but not equality) normalisation * bringing back equality normalisation * Set Version: 1.0.394 * Set Version: 1.0.396 * Set Version: 1.0.398 * removing unsound keccak simplifying assumptions * Set Version: 1.0.399 * Set Version: 1.0.400 * Set Version: 1.0.406 * Set Version: 1.0.407 * adding tests for comparison normalisation, removing keccak * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * ----- alignment * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>
runtimeverification · Dec 27, 2023 · 7e4409f · 7e4409f
1 parent 43a18d0
commit 7e4409f
Show file tree

Hide file tree

Showing 5 changed files with 152 additions and 38 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
@@ -54,6 +54,11 @@ module BYTES-SIMPLIFICATION [symbolic]
       requires lengthBytes(B) <=Int 32
        andBool #rangeUInt(256, X) [simplification, concrete(B), comm]
 
+    rule [buf-as-int-ml]:
+      { B:Bytes #Equals #buf(32, X:Int) } => { X #Equals #asInteger(B) }
+      requires lengthBytes(B) <=Int 32
+       andBool #rangeUInt(256, X) [simplification, concrete(B), comm]
+
     rule [buf-asWord-invert]:
       #buf (W:Int , #asWord(B:Bytes)) => #buf(W -Int lengthBytes(B), 0) +Bytes B
       requires lengthBytes(B) <=Int W andBool W <=Int 32

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k
@@ -13,35 +13,77 @@ module INT-SIMPLIFICATION-HASKELL [symbolic, kore]
 
     // associativity normalization
 
-    rule A +Int B => B +Int A [concrete(A), symbolic(B), simplification(40)]
-
-    rule A +Int (B +Int C) => (A +Int B) +Int C [symbolic(A, B), simplification(40)]
-    rule A +Int (B -Int C) => (A +Int B) -Int C [symbolic(A, B), simplification(40)]
-    rule A -Int (B +Int C) => (A -Int B) -Int C [symbolic(A, B), simplification(40)]
-    rule A -Int (B -Int C) => (A -Int B) +Int C [symbolic(A, B), simplification(40)]
+    rule A +Int (B +Int C) => (A +Int B) +Int C [symbolic(A, B), concrete(C), simplification(40)]
+    rule A +Int (B -Int C) => (A +Int B) -Int C [symbolic(A, B), concrete(C), simplification(40)]
+    rule A -Int (B +Int C) => (A -Int B) -Int C [symbolic(A, B), concrete(C), simplification(40)]
+    rule A -Int (B -Int C) => (A -Int B) +Int C [symbolic(A, B), concrete(C), simplification(40)]
 
     rule A +Int (B -Int C) => (A -Int C) +Int B [symbolic(A, C), concrete(B), simplification(40)]
     rule A -Int (B -Int C) => (A +Int C) -Int B [symbolic(A, C), concrete(B), simplification(40)]
 
-    rule (A +Int B) +Int C => (A +Int C) +Int B [concrete(B), symbolic(C), simplification(40)]
-    rule (A +Int B) -Int C => (A -Int C) +Int B [concrete(B), symbolic(C), simplification(40)]
-    rule (A -Int B) +Int C => (A +Int C) -Int B [concrete(B), symbolic(C), simplification(40)]
-    rule (A -Int B) -Int C => (A -Int C) -Int B [concrete(B), symbolic(C), simplification(40)]
+    rule (A +Int B) +Int C => (A +Int C) +Int B [concrete(B), symbolic(A, C), simplification(40)]
+    rule (A +Int B) -Int C => (A -Int C) +Int B [concrete(B), symbolic(A, C), simplification(40)]
+    rule (A -Int B) +Int C => (A +Int C) -Int B [concrete(B), symbolic(A, C), simplification(40)]
+    rule (A -Int B) -Int C => (A -Int C) -Int B [concrete(B), symbolic(A, C), simplification(40)]
 
     rule (A +Int B) +Int C => A +Int (B +Int C) [concrete(B, C), symbolic(A), simplification(40)]
     rule (A +Int B) -Int C => A +Int (B -Int C) [concrete(B, C), symbolic(A), simplification(40)]
     rule (A -Int B) +Int C => A +Int (C -Int B) [concrete(B, C), symbolic(A), simplification(40)]
     rule (A -Int B) -Int C => A -Int (B +Int C) [concrete(B, C), symbolic(A), simplification(40)]
 
   // ###########################################################################
-  // inequality
+  // comparison normalization
   // ###########################################################################
 
-    rule A +Int B  <Int C        => A         <Int C -Int B [concrete(B), simplification(40)]
-    rule A         <Int B +Int C => A -Int C  <Int B        [concrete(A, C), simplification(40)]
-    rule A        <=Int B +Int C => A -Int C <=Int B        [concrete(A, C), simplification(40)]
-    rule A -Int B  <Int C        => A -Int C  <Int B        [concrete(A, C), simplification(40)]
-    rule A        <=Int B -Int C => C        <=Int B -Int A [concrete(A, B), simplification(40)]
+    rule A +Int B   <Int C => A  <Int C -Int B [concrete(B, C), symbolic(A), simplification(45)]
+    rule A +Int B  <=Int C => A <=Int C -Int B [concrete(B, C), symbolic(A), simplification(45)]
+    rule A +Int B   >Int C => A  >Int C -Int B [concrete(B, C), symbolic(A), simplification(45)]
+    rule A +Int B  >=Int C => A >=Int C -Int B [concrete(B, C), symbolic(A), simplification(45)]
+
+    rule A +Int B   <Int C => B  <Int C -Int A [concrete(A, C), symbolic(B), simplification(45)]
+    rule A +Int B  <=Int C => B <=Int C -Int A [concrete(A, C), symbolic(B), simplification(45)]
+    rule A +Int B   >Int C => B  >Int C -Int A [concrete(A, C), symbolic(B), simplification(45)]
+    rule A +Int B  >=Int C => B >=Int C -Int A [concrete(A, C), symbolic(B), simplification(45)]
+
+    rule A -Int B   <Int C => A  <Int C +Int B [concrete(B, C), symbolic(A), simplification(45)]
+    rule A -Int B  <=Int C => A <=Int C +Int B [concrete(B, C), symbolic(A), simplification(45)]
+    rule A -Int B   >Int C => A  >Int C +Int B [concrete(B, C), symbolic(A), simplification(45)]
+    rule A -Int B  >=Int C => A >=Int C +Int B [concrete(B, C), symbolic(A), simplification(45)]
+
+    rule A -Int B   <Int C => A -Int C  <Int B [concrete(A, C), symbolic(B), simplification(45)]
+    rule A -Int B  <=Int C => A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)]
+    rule A -Int B   >Int C => A -Int C  >Int B [concrete(A, C), symbolic(B), simplification(45)]
+    rule A -Int B  >=Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)]
+
+    rule A   <Int B +Int C => A -Int B  <Int C [concrete(A, B), symbolic(C), simplification(45)]
+    rule A  <=Int B +Int C => A -Int B <=Int C [concrete(A, B), symbolic(C), simplification(45)]
+    rule A   >Int B +Int C => A -Int B  >Int C [concrete(A, B), symbolic(C), simplification(45)]
+    rule A  >=Int B +Int C => A -Int B >=Int C [concrete(A, B), symbolic(C), simplification(45)]
+
+    rule A   <Int B +Int C => A -Int C  <Int B [concrete(A, C), symbolic(B), simplification(45)]
+    rule A  <=Int B +Int C => A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)]
+    rule A   >Int B +Int C => A -Int C  >Int B [concrete(A, C), symbolic(B), simplification(45)]
+    rule A  >=Int B +Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)]
+
+    rule A   <Int B -Int C => C  <Int B -Int A [concrete(A, B), symbolic(C), simplification(45)]
+    rule A  <=Int B -Int C => C <=Int B -Int A [concrete(A, B), symbolic(C), simplification(45)]
+    rule A   >Int B -Int C => C  >Int B -Int A [concrete(A, B), symbolic(C), simplification(45)]
+    rule A  >=Int B -Int C => C >=Int B -Int A [concrete(A, B), symbolic(C), simplification(45)]
+
+    rule A   <Int B -Int C => A +Int C  <Int B [concrete(A, C), symbolic(B), simplification(45)]
+    rule A  <=Int B -Int C => A +Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)]
+    rule A   >Int B -Int C => A +Int C  >Int B [concrete(A, C), symbolic(B), simplification(45)]
+    rule A  >=Int B -Int C => A +Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)]
+
+    rule A +Int B  ==Int C => A ==Int C -Int B [concrete(B, C), symbolic(A), simplification(45), comm]
+    rule A +Int B  ==Int C => B ==Int C -Int A [concrete(A, C), symbolic(B), simplification(45), comm]
+    rule A -Int B  ==Int C => A ==Int C +Int B [concrete(B, C), symbolic(A), simplification(45), comm]
+    rule A -Int B  ==Int C => A -Int C ==Int B [concrete(A, C), symbolic(B), simplification(45), comm]
+
+    rule { A +Int B #Equals C } => { A #Equals C -Int B } [concrete(B, C), symbolic(A), simplification(45), comm]
+    rule { A +Int B #Equals C } => { B #Equals C -Int A } [concrete(A, C), symbolic(B), simplification(45), comm]
+    rule { A -Int B #Equals C } => { A #Equals C +Int B } [concrete(B, C), symbolic(A), simplification(45), comm]
+    rule { A -Int B #Equals C } => { A -Int C #Equals B } [concrete(A, C), symbolic(B), simplification(45), comm]
 
 endmodule
 

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
@@ -28,7 +28,7 @@ module LEMMAS [symbolic]
     rule         chop(_V) <Int pow256 => true        [simplification]
 
     rule X *Int Y <Int pow256 => true requires Y <=Int maxUInt256 /Int X [simplification]
-    rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification] 
+    rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification]
 
   // ########################
   // Set Reasoning
@@ -37,6 +37,9 @@ module LEMMAS [symbolic]
     rule X in (SetItem(Y) _   ) => true      requires X  ==Int Y [simplification]
     rule X in (SetItem(Y) REST) => X in REST requires X =/=Int Y [simplification]
 
+    rule   ( S:Set |Set SetItem ( X )                      ) |Set SetItem( X ) =>   ( S:Set |Set SetItem ( X )                      ) [simplification]
+    rule ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) |Set SetItem( X ) => ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) [simplification]
+
   // ########################
   // Word Reasoning
   // ########################
@@ -56,8 +59,6 @@ module LEMMAS [symbolic]
     rule bool2Word(_B) |Int 1 => 1            [simplification]
     rule bool2Word( B) &Int 1 => bool2Word(B) [simplification]
 
-    rule notBool notBool B => B [simplification]
-
     // #newAddr range
     rule 0 <=Int #newAddr(_,_)             => true   [simplification]
     rule         #newAddr(_,_) <Int pow160 => true   [simplification]
@@ -72,20 +73,21 @@ module LEMMAS [symbolic]
   // Keccak
   // ########################
 
-    //Required for #Ceil(#buf)
+    // Required for #Ceil(#buf)
     rule 0 <=Int keccak( _ )             => true [simplification]
     rule         keccak( _ ) <Int pow256 => true [simplification]
 
   // ########################
   // Map Reasoning
   // ########################
 
-    rule #lookup ( _M:Map [ K1 <- V1 ] , K2 ) => #lookup ( K1 |-> V1 , K1 )  requires K1 ==Int  K2 [simplification]
-    rule #lookup (  M:Map [ K1 <- _  ] , K2 ) => #lookup ( M         , K2 )  requires K1 =/=Int K2 [simplification]
-
     rule 0 <=Int #lookup( _M:Map , _ )             => true [simplification, smt-lemma]
     rule         #lookup( _M:Map , _ ) <Int pow256 => true [simplification, smt-lemma]
 
+    rule #lookup ( _M:Map [ K1 <- V1 ] , K2 )    => #lookup ( K1 |-> V1 , K1 ) requires K1 ==Int  K2 [simplification]
+    rule #lookup (  M:Map [ K1 <- _  ] , K2 )    => #lookup ( M         , K2 ) requires K1 =/=Int K2 [simplification]
+    rule #lookup ( (K1:Int |-> _) M:Map, K2:Int) => #lookup ( M         , K2 ) requires K1 =/=Int K2 [simplification]
+
     rule M:Map [ I1:Int <- V1:Int ] [ I2:Int <- V2:Int ] ==K M:Map [ I2 <- V2 ] [ I1 <- V1 ] => true
       requires I1 =/=Int I2
       [simplification]
@@ -217,6 +219,11 @@ module LEMMAS-HASKELL [symbolic, kore]
   // Boolean Logic
   // ########################
 
-    rule B ==Bool false => notBool B [simplification]
+    rule B ==Bool true  => B         [simplification, comm]
+    rule B ==Bool false => notBool B [simplification, comm]
+
+    rule notBool notBool B => B [simplification]
+
     rule (notBool (A andBool B)) andBool A => (notBool B) andBool A [simplification]
+
 endmodule
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
@@ -22,7 +22,7 @@ Address/Hash Helpers
 
 ```k
     syntax Int ::= keccak ( Bytes ) [function, total, smtlib(smt_keccak)]
- // -------------------------------------------------------------------------
+ // ---------------------------------------------------------------------
     rule [keccak]: keccak(WS) => #parseHexWord(Keccak256bytes(WS)) [concrete]
 ```
 
@@ -37,7 +37,7 @@ Address/Hash Helpers
    syntax Bytes  ::= ECDSARecoverbytes ( Bytes , Int , Bytes , Bytes ) [function, total]
    syntax String ::= ECDSASignbytes ( Bytes, Bytes )                   [function, total]
                    | ECDSAPubKeybytes ( Bytes )                        [function, total]
- // -------------------------------------------------------------------------
+ // ------------------------------------------------------------------------------------
     rule Keccak256bytes(BS)      => Keccak256(Bytes2String(BS))      [concrete]
     rule Sha256bytes(BS)         => Sha256(Bytes2String(BS))         [concrete]
     rule RipEmd160bytes(BS)      => RipEmd160(Bytes2String(BS))      [concrete]

diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
@@ -73,6 +73,64 @@ module LEMMAS-SPEC
                                   => doneLemma(368263281805664599098893944405654396525700029268) ... </k>
                                requires #lookup(ACCT_STORAGE, 8) <Int pow160
 
+ // Comparisons
+ // -----------
+
+    claim [comp-norm-01]:
+      <k> runLemma (
+            ( ( 20 -Int ( 10 +Int X:Int ) ) -Int 5 ) +Int 3 <=Int 7
+          ) =>
+          doneLemma (
+            1 <=Int X
+          ) ...
+      </k>
+
+    claim [comp-norm-02]:
+      <k> runLemma (
+            ( ( 20 -Int ( 10 +Int X:Int ) ) -Int 5 ) +Int 3 <Int 7
+          ) =>
+          doneLemma (
+            1 <Int X
+          ) ...
+      </k>
+
+    claim [comp-norm-03]:
+      <k> runLemma (
+            ( ( 20 -Int ( 10 +Int X:Int ) ) -Int 5 ) +Int 3 >Int 7
+          ) =>
+          doneLemma (
+            1 >Int X
+          ) ...
+      </k>
+
+    claim [comp-norm-04]:
+      <k> runLemma (
+            ( ( 20 -Int ( 10 +Int X:Int ) ) -Int 5 ) +Int 3 >=Int 7
+          ) =>
+          doneLemma (
+            1 >=Int X
+          ) ...
+      </k>
+
+
+ // Sets
+ // ----
+
+    claim [set-union-01]:
+      <k> runLemma (
+            notBool ( ( ((((S:Set |Set SetItem(X)) |Set SetItem (X)) |Set SetItem(Y)) |Set SetItem(X))
+                          ==K
+                          ((S:Set |Set SetItem(X)) |Set SetItem (Y))
+                      ) ==Bool false
+                    ) ==Bool true
+          ) =>
+          doneLemma (
+            true
+          ) ...
+      </k>
+      requires X =/=K Y
+
+
  // Buffer write simplifications
  // ----------------------------
 
@@ -113,6 +171,8 @@ module LEMMAS-SPEC
     claim <k> runLemma ( #lookup( _M:Map [ KEY <- 33 ] [ KEY' <- 728 ] [ KEY'' <- (pow256 +Int 5) ] [ KEY''' <- "hello" ] , KEY''  ) ) => doneLemma ( 5   ) ... </k> requires KEY =/=Int KEY' andBool KEY =/=Int KEY'' andBool KEY =/=Int KEY''' andBool KEY' =/=Int KEY'' andBool KEY' =/=Int KEY''' andBool KEY'' =/=Int KEY'''
     claim <k> runLemma ( #lookup( _M:Map [ KEY <- 33 ] [ KEY' <- 728 ] [ KEY'' <- (pow256 +Int 5) ] [ KEY''' <- "hello" ] , KEY''' ) ) => doneLemma ( 0   ) ... </k> requires KEY =/=Int KEY' andBool KEY =/=Int KEY'' andBool KEY =/=Int KEY''' andBool KEY' =/=Int KEY'' andBool KEY' =/=Int KEY''' andBool KEY'' =/=Int KEY'''
 
+    claim [lookup-key-neq]: <k> runLemma ( #lookup( ( (3 |-> 3) (5 |-> 5) (7 |-> 7) M:Map ) [ 9 <- 9 ] [ 11 <- 11 ] [ 13 <- 13 ], KEY ) ) => doneLemma ( #lookup (M, KEY) ) ... </k> requires 15 <=Int KEY
+
  // #range selection operation
  // --------------------------
 
@@ -422,18 +482,18 @@ module LEMMAS-SPEC
     claim <k> runLemma ( notMaxUInt240 &Int ( X <<Int 240 ) ) => doneLemma( X <<Int 240 ) ... </k> requires #rangeUInt ( 16 , X )
     claim <k> runLemma ( notMaxUInt248 &Int ( X <<Int 248 ) ) => doneLemma( X <<Int 248 ) ... </k> requires #rangeUInt (  8 , X )
 
-    claim <k> runLemma ( maxUInt8   &Int ( X |Int ( notMaxUInt8   &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (   8 , X )
-    claim <k> runLemma ( maxUInt16  &Int ( X |Int ( notMaxUInt16  &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  16 , X )
-    claim <k> runLemma ( maxUInt32  &Int ( X |Int ( notMaxUInt32  &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  32 , X )
-    claim <k> runLemma ( maxUInt64  &Int ( X |Int ( notMaxUInt64  &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  64 , X )
-    claim <k> runLemma ( maxUInt96  &Int ( X |Int ( notMaxUInt96  &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  96 , X )
-    claim <k> runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 128 , X )
-    claim <k> runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 160 , X )
-    claim <k> runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 192 , X )
-    claim <k> runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 208 , X )
-    claim <k> runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 224 , X )
-    claim <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X )
-    claim <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X )
+    claim <k> runLemma ( maxUInt8   &Int ( X |Int ( notMaxUInt8   &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (   8 , X )
+    claim <k> runLemma ( maxUInt16  &Int ( X |Int ( notMaxUInt16  &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  16 , X )
+    claim <k> runLemma ( maxUInt32  &Int ( X |Int ( notMaxUInt32  &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  32 , X )
+    claim <k> runLemma ( maxUInt64  &Int ( X |Int ( notMaxUInt64  &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  64 , X )
+    claim <k> runLemma ( maxUInt96  &Int ( X |Int ( notMaxUInt96  &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  96 , X )
+    claim <k> runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 128 , X )
+    claim <k> runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 160 , X )
+    claim <k> runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 192 , X )
+    claim <k> runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 208 , X )
+    claim <k> runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 224 , X )
+    claim <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X )
+    claim <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X )
 
     claim <k> runLemma ( #buf ( 32 , #asWord ( X ) ) ) => doneLemma( X ) </k> requires lengthBytes(X) ==Int 32
     claim <k> runLemma ( #buf ( 32 , X <<Int 248 ) ) => doneLemma( #buf ( 1 , X ) +Bytes #buf ( 31 , 0 ) ) ... </k> requires #rangeUInt (  8 , X )