Use the booster backend and small improvements. (#12)

* Prove lemmas * Run json claims * Make json claims work * Small fixes * Multisig improvements * Refactoring property testing * Add missing lemmas * Use the booster backend * Fixes * Tests * Testing * Update the Elrond semantics * Fix lint warnings * Fix .ProofOperationList name * Remove unused variable
runtimeverification · Oct 7, 2023 · c749f3e · c749f3e
1 parent 0f7830f
commit c749f3e
Show file tree

Hide file tree

Showing 35 changed files with 2,337 additions and 163 deletions.
diff --git a/kmxwasm/k-src/elrond-lemmas.md b/kmxwasm/k-src/elrond-lemmas.md
@@ -1,16 +1,13 @@
 ```k
 require "ceils.k"
 
-module ELROND-LEMMAS
+module ELROND-LEMMAS  [symbolic]
   imports private CEILS
   imports private ELROND
   imports private INT-KORE
   imports private SET
   imports private WASM-TEXT
 
-  rule  ( size ( _L:List ) >=Int 0 => true )
-    [simplification(), smt-lemma()]
-
   rule Bytes2Int(#getBytesRange(_:Bytes, _:Int, N:Int), _:Endianness, _:Signedness) <Int M:Int
         => true
       requires 2 ^Int (8 *Int N) <=Int M
@@ -32,9 +29,12 @@ module ELROND-LEMMAS
       requires 0 <=Int Value
       [simplification]
 
-  rule { b"" #Equals Int2Bytes(Len:Int, _Value:Int, _E:Endianness)}:Bool
+  rule { b"" #Equals Int2Bytes(Len:Int, _Value:Int, _E:Endianness) }:Bool
       => {0 #Equals Len}
       [simplification]
+  rule { b"" #Equals Int2Bytes(Value:Int, _E:Endianness, _S:Signedness) }:Bool
+      => {0 #Equals Value}
+      [simplification]
 
   rule 0 <=Int A +Int B => true
       requires 0 <=Int A andBool 0 <=Int B
@@ -85,6 +85,54 @@ module ELROND-LEMMAS
           andBool (PadLen <Int Start orBool Start +Int GetLen <Int lengthBytes(B))
       [simplification]
 
+  rule #setRange(
+          #setRange(M:Bytes, Addr1:Int, Val1:Int, Width1:Int),
+          Addr2:Int, Val2:Int, Width2:Int
+      )
+      => #setRange(
+          #setRange(M:Bytes, Addr2:Int, Val2:Int, Width2:Int),
+          Addr1:Int, Val1:Int, Width1:Int
+      )
+      requires disjontRanges(Addr1, Val1, Addr2, Val2)
+      [simplification, concrete(Addr1,Val1,Width1), symbolic(Val2)]
+      // TODO: Consider adding rules for when Addr1 or Width1 are symbolic
+  rule #getBytesRange(
+          #setRange(M:Bytes, SetAddr:Int, _SetVal:Int, SetWidth:Int),
+          GetAddr:Int, GetWidth:Int
+      )
+      => #getBytesRange(M, GetAddr:Int, GetWidth:Int)
+      requires disjontRanges(SetAddr, SetWidth, GetAddr, GetWidth)
+      [simplification]
+  rule #getBytesRange(
+          #setRange(_M:Bytes, Addr:Int, Val:Int, Width:Int),
+          Addr:Int, Width:Int
+      )
+      => Int2Bytes(Width, Val, LE)
+      requires 0 <Int Width andBool 0 <=Int Val andBool 0 <=Int Addr
+      [simplification]
+
+  rule replaceAtBytesTotal
+      ( #setRange(M:Bytes, Addr1:Int, Val1:Int, Width1:Int)
+      , Addr2
+      , Src:Bytes
+      )
+    => #setRange
+      ( replaceAtBytesTotal(M, Addr2, Src)
+      , Addr1:Int, Val1:Int, Width1:Int
+      )
+      requires disjontRanges(Addr1, Width1, Addr2, lengthBytes(Src))
+    [simplification, concrete(Addr2, Src), symbolic(Val1)]
+
+  rule padRightBytesTotal
+      ( #setRange(M:Bytes, Addr1:Int, Val1:Int, Width1:Int)
+      , Len, 0
+      )
+    => #setRange
+      ( padRightBytesTotal(M:Bytes, Len, 0)
+      , Addr1:Int, Val1:Int, Width1:Int
+      )
+      [simplification]
+
   syntax Bool ::= disjontRangesSimple(start1:Int, len1:Int, start2:Int, len2:Int)  [function, total]
   rule disjontRangesSimple(Start1:Int, Len1:Int, Start2:Int, Len2:Int)
       => (Start1 +Int Len1 <=Int Start2)
@@ -328,62 +376,10 @@ module ELROND-LEMMAS
       requires 0 <Int A
       [simplification]
 
-  rule  0 <=Int #bool ( _B ) => true
-    [simplification(), smt-lemma()]
-
-  rule  #bool ( _B ) <=Int 1 => true
-    [simplification(), smt-lemma()]
-
-  rule  #bool ( B:Bool ) <Int 1 => notBool (B:Bool)
-    [simplification()]
-
-  rule  { 0 #Equals #bool ( B:Bool ) } => { false #Equals B:Bool }
-    [simplification]
-
-  rule  { 1 #Equals #bool ( B:Bool ) } => { true #Equals B:Bool }
-    [simplification()]
-
-  rule  X:Int <Int maxInt ( Y:Int , Z:Int ) => true
-    requires ( X:Int <Int Y:Int
-      orBool ( X:Int <Int Z:Int
-              ))
-    [simplification()]
-
-  rule  X:Int >=Int maxInt ( Y:Int , Z:Int ) => true
-    requires ( X:Int >=Int Y:Int
-      andBool ( X:Int >=Int Z:Int
-              ))
-    [simplification()]
-
-  rule  X:Int >Int maxInt ( Y:Int , Z:Int ) => true
-    requires ( X:Int >Int Y:Int
-      andBool ( X:Int >Int Z:Int
-              ))
-    [simplification()]
-
-  rule  maxInt ( Y:Int , Z:Int ) >=Int X:Int => true
-    requires ( X:Int <=Int Y:Int
-      orBool ( X:Int <=Int Z:Int
-              ))
-    [simplification()]
-
-  rule  maxInt ( Y:Int , Z:Int ) >Int X:Int => true
-    requires ( X:Int <Int Y:Int
-      orBool ( X:Int <Int Z:Int
-              ))
-    [simplification()]
-
-  rule  maxInt ( Y:Int , Z:Int ) <=Int X:Int => true
-    requires ( X:Int >=Int Y:Int
-      andBool ( X:Int >=Int Z:Int
-              ))
-    [simplification()]
-
-  rule  maxInt ( Y:Int , Z:Int ) <Int X:Int => true
-    requires ( X:Int >Int Y:Int
-      andBool ( X:Int >Int Z:Int
-              ))
-    [simplification()]
+  rule 0 |Int I:Int => I
+      [simplification]
+  rule I:Int |Int 0 => I
+      [simplification]
 
 endmodule
 

diff --git a/kmxwasm/k-src/elrond-semantics b/kmxwasm/k-src/elrond-semantics
diff --git a/kmxwasm/k-src/elrond-wasm.md b/kmxwasm/k-src/elrond-wasm.md
@@ -1,6 +1,7 @@
 ```k
 require "elrond-lemmas.md"
 require "elrond-semantics/foundry.md"
+require "lemmas/proven-elrond-lemmas.md"
 require "proof-extensions.md"
 require "specification-lemmas.md"
 require "wasm-semantics/kwasm-lemmas.md"
@@ -13,6 +14,7 @@ endmodule
 module ELROND-WASM
   imports ELROND-LEMMAS
   imports ELROND-WASM-NO-LOCAL-LEMMAS
+  imports PROVEN-ELROND-LEMMAS
 endmodule
 
 module ELROND-WASM-NO-LOCAL-LEMMAS

diff --git a/kmxwasm/k-src/kbuild.toml b/kmxwasm/k-src/kbuild.toml
@@ -13,3 +13,12 @@ backend='llvm'
 [targets.haskell]
 main-file = 'elrond-wasm.md'
 backend='haskell'
+
+[targets.lemma-proofs]
+main-file = 'lemmas/semantics/elrond-wasm-lemma-proofs.md'
+backend='haskell'
+
+[targets.llvm-library]
+llvm-kompile-type='c'
+main-file = 'elrond-wasm.md'
+backend='llvm'