Improvements for the multisig-full contract

.gitignore

@@ -5,6 +5,10 @@
 
 .build
 .kprove-*
+.kore-repl-history
+.sessionCommands
+kore-*.tar.gz
+tmp
 
 # User-specific files
 *.rsuser

kmxwasm/k-src/ceils.k

@@ -0,0 +1,152 @@
+module CEILS
+    imports BOOL
+    imports BYTES
+    imports INT
+
+    syntax Bool ::= definedSubstrBytes(Bytes, startIndex: Int, endIndex: Int)  [function, total]
+    rule definedSubstrBytes(B:Bytes, StartIndex:Int, EndIndex:Int)
+        => (0 <=Int StartIndex) andBool (0 <=Int EndIndex)
+            andBool (StartIndex <Int lengthBytes(B))
+            andBool (EndIndex <=Int lengthBytes(B))
+            andBool (StartIndex <=Int EndIndex)
+
+
+    syntax Bool ::= definedReplaceAtBytes(dest: Bytes, index: Int, src: Bytes)  [function, total]
+    rule definedReplaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes)
+        =>  (0 <=Int Index)
+            andBool (Index +Int lengthBytes(Src) <=Int lengthBytes(Dest))
+
+
+    syntax Bool ::= definedPadRightBytes(Bytes, length: Int, value: Int)  [function, total]
+    rule definedPadRightBytes(_B:Bytes, Length:Int, Value:Int)
+        =>  (0 <=Int Length)
+            andBool (0 <=Int Value)
+            andBool (Value <=Int 255)
+
+
+    syntax Bool ::= definedModInt(Int, Int)  [function, total]
+    rule definedModInt (_:Int, X:Int) => X =/=Int 0
+
+
+    // ---------------------------------------
+
+
+    rule #Ceil(substrBytes(@Arg0:Bytes, @StartIndex:Int, @EndIndex:Int))
+        =>  ((({ definedSubstrBytes(@Arg0, @StartIndex, @EndIndex)  #Equals true }
+          #And #Ceil(@Arg0))
+          #And #Ceil(@StartIndex))
+          #And #Ceil(@EndIndex))
+        [simplification]
+
+
+    syntax Bytes ::= substrBytesTotal(Bytes, startIndex: Int, endIndex: Int)
+        [function, total, klabel(substrBytesTotal), symbol, no-evaluators]
+
+    rule substrBytesTotal(Arg0:Bytes, StartIndex:Int, EndIndex:Int)
+        => substrBytes(Arg0, StartIndex, EndIndex)
+        requires definedSubstrBytes(Arg0, StartIndex, EndIndex)
+        [concrete, simplification]
+
+    rule substrBytes(Arg0:Bytes, StartIndex:Int, EndIndex:Int)
+        => substrBytesTotal(Arg0, StartIndex, EndIndex)
+        requires definedSubstrBytes(Arg0, StartIndex, EndIndex)
+        [symbolic(Arg0), simplification]
+
+    rule substrBytes(Arg0:Bytes, StartIndex:Int, EndIndex:Int)
+        => substrBytesTotal(Arg0, StartIndex, EndIndex)
+        requires definedSubstrBytes(Arg0, StartIndex, EndIndex)
+        [symbolic(StartIndex), simplification]
+
+    rule substrBytes(Arg0:Bytes, StartIndex:Int, EndIndex:Int)
+        => substrBytesTotal(Arg0, StartIndex, EndIndex)
+        requires definedSubstrBytes(Arg0, StartIndex, EndIndex)
+        [symbolic(EndIndex), simplification]
+
+    rule #Ceil(replaceAtBytes(@Dest:Bytes, @Index:Int, @Src:Bytes))
+        =>  ((({ definedReplaceAtBytes(@Dest, @Index, @Src)  #Equals true }
+          #And #Ceil(@Dest))
+          #And #Ceil(@Index))
+          #And #Ceil(@Src))
+        [simplification]
+
+
+    syntax Bytes ::= replaceAtBytesTotal(dest: Bytes, index: Int, src: Bytes)
+        [function, total, klabel(replaceAtBytesTotal), symbol, no-evaluators]
+
+    rule replaceAtBytesTotal(Dest:Bytes, Index:Int, Src:Bytes)
+        => replaceAtBytes(Dest, Index, Src)
+        requires definedReplaceAtBytes(Dest, Index, Src)
+        [concrete, simplification]
+
+    rule replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes)
+        => replaceAtBytesTotal(Dest, Index, Src)
+        requires definedReplaceAtBytes(Dest, Index, Src)
+        [symbolic(Dest), simplification]
+
+    rule replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes)
+        => replaceAtBytesTotal(Dest, Index, Src)
+        requires definedReplaceAtBytes(Dest, Index, Src)
+        [symbolic(Index), simplification]
+
+    rule replaceAtBytes(Dest:Bytes, Index:Int, Src:Bytes)
+        => replaceAtBytesTotal(Dest, Index, Src)
+        requires definedReplaceAtBytes(Dest, Index, Src)
+        [symbolic(Src), simplification]
+
+    rule #Ceil(padRightBytes(@Arg0:Bytes, @Length:Int, @Value:Int))
+        =>  ((({ definedPadRightBytes(@Arg0, @Length, @Value)  #Equals true }
+          #And #Ceil(@Arg0))
+          #And #Ceil(@Length))
+          #And #Ceil(@Value))
+        [simplification]
+
+
+    syntax Bytes ::= padRightBytesTotal(Bytes, length: Int, value: Int)
+        [function, total, klabel(padRightBytesTotal), symbol, no-evaluators]
+
+    rule padRightBytesTotal(Arg0:Bytes, Length:Int, Value:Int)
+        => padRightBytes(Arg0, Length, Value)
+        requires definedPadRightBytes(Arg0, Length, Value)
+        [concrete, simplification]
+
+    rule padRightBytes(Arg0:Bytes, Length:Int, Value:Int)
+        => padRightBytesTotal(Arg0, Length, Value)
+        requires definedPadRightBytes(Arg0, Length, Value)
+        [symbolic(Arg0), simplification]
+
+    rule padRightBytes(Arg0:Bytes, Length:Int, Value:Int)
+        => padRightBytesTotal(Arg0, Length, Value)
+        requires definedPadRightBytes(Arg0, Length, Value)
+        [symbolic(Length), simplification]
+
+    rule padRightBytes(Arg0:Bytes, Length:Int, Value:Int)
+        => padRightBytesTotal(Arg0, Length, Value)
+        requires definedPadRightBytes(Arg0, Length, Value)
+        [symbolic(Value), simplification]
+
+    rule #Ceil(@Arg0:Int modInt @Arg1:Int)
+        =>  (({ definedModInt(@Arg0, @Arg1)  #Equals true }
+          #And #Ceil(@Arg0))
+          #And #Ceil(@Arg1))
+        [simplification]
+
+
+    syntax Int ::= Int "modIntTotal" Int
+        [function, total, klabel(modIntTotal), symbol, no-evaluators, smtlib(modIntTotal)]
+
+    rule Arg0:Int modIntTotal Arg1:Int
+        => Arg0 modInt Arg1
+        requires definedModInt(Arg0, Arg1)
+        [concrete, simplification]
+
+    rule Arg0:Int modInt Arg1:Int
+        => Arg0 modIntTotal Arg1
+        requires definedModInt(Arg0, Arg1)
+        [symbolic(Arg0), simplification]
+
+    rule Arg0:Int modInt Arg1:Int
+        => Arg0 modIntTotal Arg1
+        requires definedModInt(Arg0, Arg1)
+        [symbolic(Arg1), simplification]
+
+endmodule

kmxwasm/k-src/elrond-impl.md

@@ -1,8 +1,10 @@
 ```k
+require "ceils.k"
 require "elrond-configuration.md"
 require "wasm-text.md"
 
 module ELROND-IMPL
+  imports CEILS
   imports ELROND-CONFIGURATION
   imports WASM-TEXT
   imports LIST-BYTESW-EXTENSIONS
@@ -236,6 +238,20 @@ module ELROND-IMPL
                       )
                     ]
               )
+  rule  <wasm>
+            <instrs>
+              elrond_trap("\"mBufferCopyByteSlice\"") => i32.const 1
+              ...
+            </instrs>
+            <locals>
+                (0 |-> <i32> _SourceHandle:Int)
+                (1 |-> <i32> _StartingPosition:Int)
+                (2 |-> <i32> _SliceLength:Int)
+                (3 |-> <i32> _DestinationHandle:Int)
+            </locals>
+            ...
+        </wasm>
+      [owise]
 
   rule  <wasm>
             <instrs>
@@ -449,7 +465,10 @@ module ELROND-IMPL
             </buffers>
             ...
         </elrond>
-      ensures notBool wrap(?NewHandle) in_keys(M) andBool ?NewHandle >Int 0
+      ensures true
+          andBool notBool wrap(?NewHandle) in_keys(M)
+          andBool 0 <Int ?NewHandle
+          andBool ?NewHandle <Int #pow(i32)
 
   rule  <wasm>
             <instrs>
@@ -472,7 +491,10 @@ module ELROND-IMPL
         </elrond>
     requires true
         #And #Ceil(substrBytes(Mem, Ptr, Ptr +Int Len))
-    ensures notBool wrap(?NewHandle) in_keys(M) andBool ?NewHandle >Int 0
+    ensures true
+        andBool notBool wrap(?NewHandle) in_keys(M)
+        andBool ?NewHandle >Int 0
+        andBool ?NewHandle <Int #pow(i32)
 
   rule  <wasm>
             <instrs>
@@ -571,14 +593,17 @@ module ELROND-IMPL
   rule  <wasm>
             <instrs>
               // TODO: Should append to the returned result, or something like that.
-              elrond_trap("\"mBufferFinish\"") => i32.const ?_MBufferFinishResult:Int
+              elrond_trap("\"mBufferFinish\"") => i32.const ?MBufferFinishResult:Int
               ...
             </instrs>
             <locals>
                 (0 |-> <i32> _Handle:Int)
             </locals>
             ...
         </wasm>
+      ensures true
+          andBool 0 <Int ?MBufferFinishResult
+          andBool ?MBufferFinishResult <Int #pow(i32)
 
   rule  <wasm>
             <instrs>
@@ -902,11 +927,13 @@ module ELROND-IMPL
         </wasm>
         <elrond>
             <gas>
-                PreviousGasLeft:Int
+                PreviousGasLeft:Int => ?NewGasLeft
             </gas>
             ...
         </elrond>
-      ensures ?NewGasLeft <Int PreviousGasLeft andBool 0 <=Int ?NewGasLeft
+      ensures true
+          andBool ?NewGasLeft <Int PreviousGasLeft
+          andBool 0 <=Int ?NewGasLeft
 
   rule <instrs>
           #import(MOD, Name, #funcDesc(... id: OID, type: TIDX))