Pi-Squared-Inc · traiansf · Dec 16, 2024 · Dec 16, 2024 · Dec 16, 2024 · Dec 16, 2024
diff --git a/Makefile b/Makefile
@@ -20,10 +20,19 @@ endif
 pykwasm:
 	$(POETRY) install
 
-.PHONY: build
+.PHONY: build build-simple build-prove build-wrc20
 build: pykwasm
 	$(KDIST) -v build -j3
 
+build-simple: pykwasm
+	$(KDIST) -v build wasm-semantics.llvm -j3
+
+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
@@ -229,27 +238,27 @@ 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
 
-tests/%.run-term: tests/%
+tests/%.run-term: tests/% build-simple
 	$(TEST) run $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out
 	grep --after-context=2 "<instrs>" tests/$*.$(TEST_CONCRETE_BACKEND)-out > tests/$*.$(TEST_CONCRETE_BACKEND)-out-term
 	$(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out-term tests/success-k.out
 	rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
 	rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out-term
 
-tests/%.parse: tests/%
+tests/%.parse: tests/% build-simple
 	K_OPTS='-Xmx16G -Xss512m' $(TEST) kast --output kore $< > $@-out
 	rm -rf $@-out
 
-tests/%.prove: tests/%
+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"
 

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md
@@ -267,13 +267,66 @@ 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 (L1:List ListItem(X:KItem))[size(L1)] => X
+      [simplification]
+
+    rule (L1:List ListItem(_:KItem))[size(L1) <- V] =>
+      L1:List ListItem(V)
+      [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]
+```
+
+ListInt Operations
+------------------
+
+```k
+    rule size(L1:ListInt L2:ListInt) =>
+      size(L1) +Int size(L2)
+      [simplification]
+
+    rule size(_:ListInt) >=Int 0 => true [simplification, smt-lemma]
+
+```
+
 Memory
 ------
 

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/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 ])  // requires needed to make rule valid
 
     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

diff --git a/tests/proofs/locals-spec.k b/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
diff --git a/tests/proofs/loops-spec.k b/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

diff --git a/tests/proofs/memory-spec.k b/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
diff --git a/tests/proofs/wrc20-spec.k b/tests/proofs/wrc20-spec.k
@@ -1,5 +1,3 @@
-requires "wrc20.md"
-
 // This is the "fast transfer" version of the WRC20 spec by pauld.
 
 module WRC20-SPEC
@@ -14,28 +12,30 @@ 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')) </mems>
+          // TODO: Ideally, there should also be a list variable at the end of the <mems> cell
+          //  however, list unification does not seem to work that well in the Haskell Backend at the moment
+          // hence we end in the memory location being affected, for the time being.
+          //
           // 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)