Progress on fixing tests

Author: traiansf

Makefile

@@ -30,6 +30,9 @@ build-simple: pykwasm
 build-prove: pykwasm
 	$(KDIST) -v build wasm-semantics.kwasm-lemmas -j3
 
+build-wrc20: pykwasm
+	$(KDIST) -v build wasm-semantics.wrc20 -j3
+
 .PHONY: clean
 clean: pykwasm
 	$(KDIST) clean
@@ -235,7 +238,7 @@ test: test-execution test-prove
 
 # Generic Test Harnesses
 
-tests/%.run: tests/%
+tests/%.run: tests/% build-simple
 	$(TEST) run $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out
 	$(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/success-$(TEST_CONCRETE_BACKEND).out
 	rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
@@ -255,7 +258,7 @@ tests/%.prove: tests/% build-prove
 	$(eval SOURCE_DIR := $(shell $(KDIST) which wasm-semantics.source))
 	$(TEST) prove $< kwasm-lemmas -I $(SOURCE_DIR)/wasm-semantics -w2e
 
-tests/proofs/wrc20-spec.k.prove: tests/proofs/wrc20-spec.k
+tests/proofs/wrc20-spec.k.prove: tests/proofs/wrc20-spec.k build-wrc20
 	$(eval SOURCE_DIR := $(shell $(KDIST) which wasm-semantics.source))
 	$(TEST) prove $< wrc20 -I $(SOURCE_DIR)/wasm-semantics -w2e --haskell-backend-command "kore-exec --smt-timeout 500"
 

pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md

@@ -267,13 +267,47 @@ In this case, it's simpler (and safe) to simply discard the `#chop`, instead of
     rule #minSigned(ITYPE) => 0 -Int #pow1(ITYPE)
 ```
 
-Lookups
--------
+Map Lookups
+-----------
 
 ```k
     rule (_MAP:Map [KEY <- VAL])[KEY] => VAL [simplification]
 ```
 
+List Operations
+---------------
+
+These should probably be integrated into `domains.md`
+
+```k
+    rule (L1:List ListItem(X:KItem) _:List)[size(L1)] => X
+      [simplification]
+
+    rule (L1:List ListItem(_:KItem) L2:List)[size(L1) <- V] =>
+      L1:List ListItem(V) L2:List
+      [simplification]
+
+    rule (ListItem(X:KItem) _:List)[0] => X
+      [simplification]
+
+    rule (ListItem(_) L:List)[N:Int] => L[ N -Int 1]
+      requires N >Int 0
+      [simplification]
+
+    rule (ListItem(_) L:List)[0 <- X:KItem] => ListItem(X) L
+      [simplification]
+
+    rule (ListItem(A) L:List)[N:Int <- X:KItem] => ListItem(A) (L[ N -Int 1 <- X])
+      requires N >Int 0
+      [simplification]
+
+    rule size(L1:List L2:List) =>
+      size(L1) +Int size(L2)
+      [simplification]
+
+    rule size(_:List) >=Int 0 => true [simplification, smt-lemma]
+```
+
 Memory
 ------
 

pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md

@@ -572,6 +572,7 @@ The `*_local` instructions are defined here.
     rule <instrs> #local.get(I) => .K ... </instrs>
          <valstack> VALSTACK => {LOCALS [ I ]}:>Val : VALSTACK </valstack>
          <locals> LOCALS </locals>
+         requires isVal(LOCALS [ I ])
 
     rule <instrs> #local.set(I) => .K ... </instrs>
          <valstack> VALUE : VALSTACK => VALSTACK </valstack>
@@ -623,7 +624,7 @@ The importing and exporting parts of specifications are dealt with in the respec
            ...
          </globals>
       requires #typeMatches(TYP, VAL)
-    
+
 ```
 
 The `get` and `set` instructions read and write globals.
@@ -704,7 +705,7 @@ The `get` and `set` instructions read and write globals.
         </tabInst>
       requires 0 <=Int I
        andBool I <Int size(TDATA)
-        
+
     rule [tableGet-trap]:
         <instrs> #tableGet( TADDR, I) => trap ... </instrs>
         <tabInst>
@@ -732,7 +733,7 @@ The `get` and `set` instructions read and write globals.
           <tabAddrs> ... TID |-> TADDR ... </tabAddrs>
           ...
         </moduleInst>
-    
+
     rule [tableSet-oob]:
         <instrs> #tableSet(TADDR, _VAL, I) => trap ... </instrs>
         <tabInst>
@@ -840,7 +841,7 @@ The `get` and `set` instructions read and write globals.
  // ------------------------------------------------------
     rule [tableFill-zero]:
         <instrs> #tableFill(_, 0, _, _) => .K ... </instrs>
-    
+
     rule [tableFill-loop]:
         <instrs> #tableFill(TID, N, RVAL, I)
               => <i32> I
@@ -1617,7 +1618,7 @@ Element Segments
     syntax Alloc ::= allocelem(RefValType, ListRef, OptionalId)
  // -----------------------------------------------------
     rule [elem-active]:
-        <instrs> #elem(TYPE:RefValType, INIT:ListRef, MODE:ElemMode, OID:OptionalId) 
+        <instrs> #elem(TYPE:RefValType, INIT:ListRef, MODE:ElemMode, OID:OptionalId)
               => allocelem(TYPE, INIT, OID)
               ~> #elemAux(size(INIT), MODE)
                  ...
@@ -1668,11 +1669,11 @@ Element Segments
     syntax ListRef ::= resolveAddrs(ListInt, ListRef)  [function]
  // -----------------------------------------------------------
     rule resolveAddrs(_, .ListRef) => .ListRef
-    rule resolveAddrs(FADDRS, ListItem(<TYP> I) IS) 
-      => ListItem(<TYP> FADDRS {{ I }} orDefault -1) resolveAddrs(FADDRS, IS) 
-    rule resolveAddrs(FADDRS, ListItem(<TYP> null) IS) 
-      => ListItem(<TYP> null)                        resolveAddrs(FADDRS, IS) 
-    
+    rule resolveAddrs(FADDRS, ListItem(<TYP> I) IS)
+      => ListItem(<TYP> FADDRS {{ I }} orDefault -1) resolveAddrs(FADDRS, IS)
+    rule resolveAddrs(FADDRS, ListItem(<TYP> null) IS)
+      => ListItem(<TYP> null)                        resolveAddrs(FADDRS, IS)
+
 ```
 
 Data Segments

tests/proofs/locals-spec.k

@@ -1,21 +1,30 @@
 requires "kwasm-lemmas.md"
 
 module LOCALS-SPEC
-    imports KWASM-LEMMAS
+    imports WASM
 
     claim <instrs> #local.get(X) ~> #local.set(X) => .K ... </instrs>
           <locals>
-            X |-> _:IVal
+            Locals:List
+            ListItem(_:IVal)
+            _:List
           </locals>
+          requires size(Locals) ==Int X
 
     claim <instrs> #local.get(X) ~> #local.set(X) => .K ... </instrs>
           <locals>
-            X |-> _:FVal
+            Locals:List
+            ListItem(_:FVal)
+            _:List
           </locals>
+          requires size(Locals) ==Int X
 
     claim <instrs> #local.get(X) ~> #local.set(X) => .K ... </instrs>
           <locals>
-            X |-> _:RefVal
+            Locals:List
+            ListItem(_:RefVal)
+            _:List
           </locals>
+          requires size(Locals) ==Int X
 
 endmodule

tests/proofs/loops-spec.k

@@ -29,8 +29,8 @@ module LOOPS-SPEC
           </instrs>
           <valstack> _ => STACK </valstack>
           <locals>
-            0 |-> < ITYPE > (I => 0)
-            1 |-> < ITYPE > (X => X +Int ((I *Int (I +Int 1)) /Int 2))
+            ListItem(< ITYPE > (I => 0))
+            ListItem(< ITYPE > (X => X +Int ((I *Int (I +Int 1)) /Int 2)))
           </locals>
        requires #inUnsignedRange(ITYPE, I)
         andBool I >Int 0
@@ -60,8 +60,8 @@ module LOOPS-SPEC
            ...
           </instrs>
           <locals>
-            0 |-> < ITYPE > (N => 0)
-            1 |-> < ITYPE > (0 => (N *Int (N +Int 1)) /Int 2)
+            ListItem(< ITYPE > (N => 0))
+            ListItem(< ITYPE > (0 => (N *Int (N +Int 1)) /Int 2))
           </locals>
        requires #inUnsignedRange(ITYPE, N)
         andBool N >Int 0

tests/proofs/memory-spec.k

@@ -7,32 +7,24 @@ module MEMORY-SPEC
           <curModIdx> CUR </curModIdx>
           <moduleInst>
             <modIdx> CUR </modIdx>
-            <memAddrs> 0 |-> MEMADDR </memAddrs>
+           <memAddrs> ListItem(MEMADDR) </memAddrs>
             ...
           </moduleInst>
-          <memInst>
-            <mAddr> MEMADDR </mAddr>
-            <msize> SIZE    </msize>
-            <mdata> _BM      </mdata>
-            ...
-          </memInst>
+          <mems> MEMS1:List ListItem(memInst(_, SIZE, _)) _:List </mems>
         requires
-         ADDR +Int #numBytes(i64) <=Int SIZE *Int #pageSize()
-         andBool #inUnsignedRange(i32, ADDR)
+         #inUnsignedRange(i32, ADDR)
+         andBool size(MEMS1) ==Int MEMADDR
+         andBool ADDR +Int #numBytes(i64) <=Int SIZE *Int #pageSize()
 
     claim <instrs>  i32.const ADDR ~> i32.const ADDR ~> #load(ITYPE:IValType, load, 0) ~> #store(ITYPE, store, 0) => .K ... </instrs>
           <curModIdx> CUR </curModIdx>
           <moduleInst>
             <modIdx> CUR </modIdx>
-            <memAddrs> 0 |-> MEMADDR </memAddrs>
+            <memAddrs> ListItem(MEMADDR) </memAddrs>
             ...
           </moduleInst>
-          <memInst>
-            <mAddr> MEMADDR </mAddr>
-            <msize> SIZE    </msize>
-            <mdata> _BM      </mdata>
-            ...
-          </memInst>
+          <mems> MEMS1:List ListItem(memInst(_, SIZE, _)) _:List </mems>
         requires
-         #get(#chop(<i32> ADDR)) +Int #numBytes(ITYPE) <=Int SIZE *Int #pageSize()
+         size(MEMS1) ==Int MEMADDR
+         andBool #get(#chop(<i32> ADDR)) +Int #numBytes(ITYPE) <=Int SIZE *Int #pageSize()
 endmodule

tests/proofs/wrc20-spec.k

@@ -14,28 +14,26 @@ module WRC20-SPEC
                 ~> (invoke NEXTADDR) // TODO: Use `call`.
                 ~> #store(i64, store, 0)
                 => .K
-                   ...
+//                   ...
           </instrs>
           <curModIdx> CUR </curModIdx>
           <moduleInst>
             <modIdx> CUR </modIdx>
             <types> #wrc20ReverseBytesTypeIdx |-> #wrc20ReverseBytesType </types>
-            <memAddrs> 0 |-> MEMADDR </memAddrs>
-            <funcAddrs> _ => ?_ </funcAddrs>
+            <memAddrs> ListItem(MEMADDR) </memAddrs>
+            <funcAddrs> FUNCADDRS => ?_ </funcAddrs>
             <nextFuncIdx> NEXTFUNCIDX => NEXTFUNCIDX +Int 1 </nextFuncIdx>
             ...
           </moduleInst>
           <funcs> .Bag => ?_ </funcs>
           <nextFuncAddr> NEXTADDR => NEXTADDR +Int 1 </nextFuncAddr>
-          <memInst>
-            <mAddr> MEMADDR  </mAddr>
-            <msize> SIZE     </msize>
-            <mdata> BM => ?BM' </mdata>
-            ...
-          </memInst>
+          <mems> MEMS1:List ListItem(memInst(_, SIZE, BM => ?BM')) _:List </mems>
           // TODO: Make function out of this tricky side condition.
        requires ADDR +Int #numBytes(i64) <=Int SIZE *Int #pageSize()
+        andBool NEXTFUNCIDX >=Int 0
+        andBool NEXTFUNCIDX ==Int size(FUNCADDRS)
         andBool #inUnsignedRange(i32, ADDR)
+        andBool size(MEMS1) ==Int MEMADDR
        ensures  #getRange(BM, ADDR +Int 0, 1) ==Int #getRange(?BM', ADDR +Int 7, 1)
         andBool #getRange(BM, ADDR +Int 1, 1) ==Int #getRange(?BM', ADDR +Int 6, 1)
         andBool #getRange(BM, ADDR +Int 2, 1) ==Int #getRange(?BM', ADDR +Int 5, 1)