moving lookup SMT lemmas to mcd

runtimeverification · Dec 26, 2024 · dd10d98 · dd10d98
1 parent 8513c80
commit dd10d98
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 10 deletions.
diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
@@ -34,12 +34,6 @@ module LEMMAS-SPEC
  // Arithmetic
  // ----------
 
-    claim <k> runLemma(#rangeUInt(256, #lookup(M, KX) -Int #lookup(M, KY))) => doneLemma(true) ... </k>
-      requires #rangeUInt(256, X) andBool X ==Int #lookup(M,  KX)
-       andBool #rangeUInt(256, Y) andBool Y ==Int #lookup(M,  KY)
-       andBool #rangeUInt(256, Z) andBool Z ==Int #lookup(M, _KZ)
-       andBool #rangeUInt(256, (X -Int Y) -Int Z)
-
     claim [address-reprojection]: <k> runLemma(((maxUInt160 &Int ((368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)) modInt pow256)) modInt pow160))
                                    => doneLemma(368263281805664599098893944405654396525700029268) ... </k>
                                 requires #rangeUInt(256, X)

diff --git a/tests/specs/mcd/verification.k b/tests/specs/mcd/verification.k
@@ -264,14 +264,12 @@ module LEMMAS-MCD [symbolic]
     rule #WordPackAddrUInt48UInt48(ADDR, maxUInt48 &Int (ADDR_UINT48_UINT48 /Int pow160), UINT48_2) => #WordPackAddrUInt48UInt48(ADDR, 0, UINT48_2) requires maxUInt48 &Int (ADDR_UINT48_UINT48 /Int pow160) ==Int 0 [simplification]
 
   // ########################
-   // Map
-   // ########################
+  // Map and #lookup
+  // ########################
 
     rule M:Bytes [ K <- V ]            [ K' <- V' ] => M [ K' <- V' ] [ K <- V ]             requires K' <Int K                        [simplification]
     rule M [ K := BUF:Bytes ] [ K' <- V' ] => M [ K' <- V' ] [ K := BUF ]  requires K' <Int K
                                                                                                orBool K +Int lengthBytes(BUF) <=Int K' [simplification]
-    rule M [ K <- V ] => M requires #lookup(M, K) ==Int V [simplification]
-
     rule M [ K := BUF:Bytes ] [ K' := BUF':Bytes ] => M [ K := (#range(BUF , 0 , K' -Int K )) ] [ K' := BUF' ]
        requires K <Int K'
         andBool K' <Int K +Int lengthBytes(BUF)
@@ -285,6 +283,11 @@ module LEMMAS-MCD [symbolic]
         andBool K1 +Int lengthBytes(BUF11) <=Int K2 +Int lengthBytes(BUF2)
        [simplification]
 
+    rule 0 <=Int #lookup( _M:Map , _ )             => true [simplification, smt-lemma]
+    rule         #lookup( _M:Map , _ ) <Int pow256 => true [simplification, smt-lemma]
+
+    rule M [ K <- V ] => M requires #lookup(M, K) ==Int V [simplification]
+
   // ########################
   // Arithmetic
   // ########################