runtimeverification · virgil-serbanuta · Dec 13, 2019 · Dec 13, 2019
diff --git a/.build/.k.rev b/.build/.k.rev
@@ -1 +1 @@
-b0b7ee6c94c4efd8fbcbb17b7a068db6af184684
+8def058cc3aab804e5a6ef111c6a889aaefb4495
diff --git a/resources/Makefile b/resources/Makefile
@@ -12,5 +12,14 @@ TMPLS:=
 include kprove.mak
 
 # non-standard spec generation
-$(SPECS_DIR)/$(SPEC_GROUP)/sum-to-n-spec.k: $(RESOURCES)/sum-to-n.md $(TANGLER) $(LEMMAS)
+$(SPECS_DIR)/$(SPEC_GROUP)/sum-to-n-common.k: \
+		$(RESOURCES)/sum-to-n-common.md $(TANGLER) \
+		$(LEMMAS)
+	pandoc --from markdown --to "$(TANGLER)" --metadata="code:.sum-to-n" $< > $@
+
+$(SPECS_DIR)/$(SPEC_GROUP)/sum-to-n-$(K_BACKEND)-spec.k: \
+		$(RESOURCES)/sum-to-n-$(K_BACKEND).md \
+		$(TANGLER) \
+		$(LEMMAS) \
+		$(SPECS_DIR)/$(SPEC_GROUP)/sum-to-n-common.k
 	pandoc --from markdown --to "$(TANGLER)" --metadata="code:.sum-to-n" $< > $@
diff --git a/resources/kprove.mak b/resources/kprove.mak
@@ -108,8 +108,11 @@ KSERVER_LOG_FILE:=$(SPECS_DIR)/$(SPEC_GROUP)/kserver.log
 SPAWN_KSERVER:=$(K_BIN)/kserver >> "$(KSERVER_LOG_FILE)" 2>&1 &
 STOP_KSERVER:=$(K_BIN)/stop-kserver || true
 
-SPEC_FILES:=$(patsubst %,$(SPECS_DIR)/$(SPEC_GROUP)/%-spec.k,$(SPEC_NAMES))
-LEMMAS:=$(SPECS_DIR)/$(SPEC_GROUP)/lemmas.timestamp $(dir $(SPECS_DIR)/$(SPEC_GROUP))/lemmas.k
+SPEC_FILES:=$(patsubst %,$(SPECS_DIR)/$(SPEC_GROUP)/%-$(K_BACKEND)-spec.k,$(SPEC_NAMES))
+LEMMAS:= \
+	$(SPECS_DIR)/$(SPEC_GROUP)/lemmas.timestamp $(dir $(SPECS_DIR)/$(SPEC_GROUP))/lemmas.k \
+	$(dir $(SPECS_DIR)/$(SPEC_GROUP))/lemmas-common.k \
+	$(dir $(SPECS_DIR)/$(SPEC_GROUP))/lemmas-$(K_BACKEND).k
 
 PANDOC_TANGLE_SUBMODULE:=$(ROOT)/.build/pandoc-tangle
 TANGLER:=$(PANDOC_TANGLE_SUBMODULE)/tangle.lua
@@ -188,11 +191,17 @@ $(SPEC_INI): $(SPEC_INI:.ini=.md) $(PANDOC_TANGLE_SUBMODULE)/submodule.timestamp
 	pandoc --from markdown --to "$(TANGLER)" --metadata=code:".ini" $< > $@
 endif
 
-%/lemmas.k: $(RESOURCES)/lemmas.md $(PANDOC_TANGLE_SUBMODULE)/submodule.timestamp
+%/lemmas-common.k: $(RESOURCES)/lemmas-common.md $(PANDOC_TANGLE_SUBMODULE)/submodule.timestamp
+	pandoc --from markdown --to "$(TANGLER)" --metadata=code:".k" $< > $@
+
+%/lemmas.k: $(RESOURCES)/lemmas-java.md $(PANDOC_TANGLE_SUBMODULE)/submodule.timestamp %/lemmas-common.k
+	pandoc --from markdown --to "$(TANGLER)" --metadata=code:".k" $< > $@
+
+%/lemmas-$(K_BACKEND).k: $(RESOURCES)/lemmas-$(K_BACKEND).md $(PANDOC_TANGLE_SUBMODULE)/submodule.timestamp %/lemmas-common.k
 	pandoc --from markdown --to "$(TANGLER)" --metadata=code:".k" $< > $@
 
 # When building a -spec.k file, build all run dependencies.
-$(SPECS_DIR)/$(SPEC_GROUP)/%-spec.k: $(TMPLS) $(SPEC_INI) $(LEMMAS)
+$(SPECS_DIR)/$(SPEC_GROUP)/%-$(K_BACKEND)-spec.k: $(TMPLS) $(SPEC_INI) $(LEMMAS)
 	python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) $* $* > $@
 
 #
@@ -201,7 +210,7 @@ $(SPECS_DIR)/$(SPEC_GROUP)/%-spec.k: $(TMPLS) $(SPEC_INI) $(LEMMAS)
 
 test: $(addsuffix .test,$(SPEC_FILES))
 
-$(SPECS_DIR)/$(SPEC_GROUP)/%-spec.k.test: $(SPECS_DIR)/$(SPEC_GROUP)/%-spec.k
+$(SPECS_DIR)/$(SPEC_GROUP)/%-spec.k.test: $(SPECS_DIR)/$(SPEC_GROUP)/%-$(K_BACKEND)-spec.k
 	$(KPROVE) $<
 
 spawn-kserver:

diff --git a/resources/lemmas.md → resources/lemmas-common.md b/resources/lemmas.md → resources/lemmas-common.md
@@ -5,7 +5,7 @@ Verification Lemmas
 requires "evm.k"
 requires "edsl.k"
 
-module LEMMAS
+module LEMMAS-COMMON
     imports EVM
     imports EDSL
     imports K-REFLECTION
@@ -143,11 +143,6 @@ It reduces the reasoning efforts of the underlying theorem prover, factoring out
 
     rule keccakIntList(V:Int .IntList) => hash1(V)
     rule keccakIntList(V1:Int V2:Int .IntList) => hash2(V1, V2)
-
-    // for terms came from bytecode not via #hashedLocation
-    rule keccak(WS) => keccakIntList(byteStack2IntList(WS))
-      requires ( notBool #isConcrete(WS) )
-       andBool ( #sizeWordStack(WS) ==Int 32 orBool #sizeWordStack(WS) ==Int 64 )
 ```
 
 ### Integer Expression Simplification Rules
@@ -183,23 +178,6 @@ The rules are applied only when the side-conditions are met.
 These rules are specific to reasoning about EVM programs.
 
 ```k
-    //orienting symbolic term to be first, converting -Int to +Int for concrete values.
-    rule I +Int B => B          +Int I when #isConcrete(I) andBool notBool #isConcrete(B)
-    rule A -Int I => A +Int (0 -Int I) when notBool #isConcrete(A) andBool #isConcrete(I)
-
-    rule (A +Int I2) +Int I3 => A +Int (I2 +Int I3) when notBool #isConcrete(A) andBool #isConcrete(I2) andBool #isConcrete(I3)
-
-    rule I1 +Int (B +Int I3) => B +Int (I1 +Int I3) when #isConcrete(I1) andBool notBool #isConcrete(B) andBool #isConcrete(I3)
-    rule I1 -Int (B +Int I3) => (I1 -Int I3) -Int B when #isConcrete(I1) andBool notBool #isConcrete(B) andBool #isConcrete(I3)
-    rule (I1 -Int B) +Int I3 => (I1 +Int I3) -Int B when #isConcrete(I1) andBool notBool #isConcrete(B) andBool #isConcrete(I3)
-
-    rule I1 +Int (I2 +Int C) => (I1 +Int I2) +Int C when #isConcrete(I1) andBool #isConcrete(I2) andBool notBool #isConcrete(C)
-    rule I1 +Int (I2 -Int C) => (I1 +Int I2) -Int C when #isConcrete(I1) andBool #isConcrete(I2) andBool notBool #isConcrete(C)
-    rule I1 -Int (I2 +Int C) => (I1 -Int I2) -Int C when #isConcrete(I1) andBool #isConcrete(I2) andBool notBool #isConcrete(C)
-    rule I1 -Int (I2 -Int C) => (I1 -Int I2) +Int C when #isConcrete(I1) andBool #isConcrete(I2) andBool notBool #isConcrete(C)
-
-    rule I1 &Int (I2 &Int C) => (I1 &Int I2) &Int C when #isConcrete(I1) andBool #isConcrete(I2) andBool notBool #isConcrete(C)
-
     // 0xffff...f &Int N = N
     rule MASK &Int N => N  requires MASK ==Int (2 ^Int (log2Int(MASK) +Int 1)) -Int 1 // MASK = 0xffff...f
                             andBool 0 <=Int N andBool N <=Int MASK
@@ -213,9 +191,6 @@ These rules are specific to reasoning about EVM programs.
     // for gas calculation
     rule A -Int (#if C #then B1 #else B2 #fi) => #if C #then (A -Int B1) #else (A -Int B2) #fi
 
-    rule (#if C #then B1 #else B2 #fi) -Int A => #if C #then (B1 -Int A) #else (B2 -Int A) #fi 
-        when notBool #isConcrete(A) andBool #notKLabel(A, "#if_#then_#else_#fi_K-EQUAL")
-
     rule (#if C #then B1 #else B2 #fi) +Int A => #if C #then (B1 +Int A) #else (B2 +Int A) #fi
 ```
 
@@ -346,14 +321,6 @@ They cause a major increase in the number of Z3 queries and slowdown.
     rule chop(I) => I requires 0 <=Int I andBool I <Int pow256
 ```
 
-### #getKLabelString helpers
-
-Function below returns true if the KLabel of `T` is not `L`, or if `T` is a variable.
-```k
-    syntax Bool ::= #notKLabel ( K , String ) [function]
-    rule #notKLabel(T, L) => #getKLabelString(T) =/=String L orBool #isVariable(T)
-```
-
 ### Wordstack
 
 These lemmas abstract some properties about `#sizeWordStack`:

diff --git a/resources/lemmas-haskell.md b/resources/lemmas-haskell.md
@@ -0,0 +1,11 @@
+Verification Lemmas for the Haskell backend
+===========================================
+
+```k
+requires "lemmas-common.k"
+
+module LEMMAS-HASKELL
+    imports LEMMAS-COMMON
+
+endmodule
+```
diff --git a/resources/lemmas-java.md b/resources/lemmas-java.md
@@ -0,0 +1,68 @@
+Verification Lemmas for the Java backend
+========================================
+
+```k
+requires "evm.k"
+requires "edsl.k"
+requires "lemmas-common.k"
+
+module LEMMAS-JAVA
+    imports EVM
+    imports EDSL
+    imports K-REFLECTION
+    imports LEMMAS-COMMON
+```
+
+### Hashed Location
+
+```k
+    // TODO: drop keccakIntList once new vyper hashed location scheme is captured in edsl.md
+
+    // for terms coming from bytecode not via #hashedLocation
+    rule keccak(WS) => keccakIntList(byteStack2IntList(WS))
+      requires ( notBool #isConcrete(WS) )
+       andBool ( #sizeWordStack(WS) ==Int 32 orBool #sizeWordStack(WS) ==Int 64 )
+```
+
+### Integer Expression Simplification Rules
+
+The following simplification rules are local, meant to be used in specific contexts.
+The rules are applied only when the side-conditions are met.
+These rules are specific to reasoning about EVM programs.
+
+```k
+    //orienting symbolic term to be first, converting -Int to +Int for concrete values.
+    rule I +Int B => B          +Int I when #isConcrete(I) andBool notBool #isConcrete(B)
+    rule A -Int I => A +Int (0 -Int I) when notBool #isConcrete(A) andBool #isConcrete(I)
+
+    rule (A +Int I2) +Int I3 => A +Int (I2 +Int I3) when notBool #isConcrete(A) andBool #isConcrete(I2) andBool #isConcrete(I3)
+
+    rule I1 +Int (B +Int I3) => B +Int (I1 +Int I3) when #isConcrete(I1) andBool notBool #isConcrete(B) andBool #isConcrete(I3)
+    rule I1 -Int (B +Int I3) => (I1 -Int I3) -Int B when #isConcrete(I1) andBool notBool #isConcrete(B) andBool #isConcrete(I3)
+    rule (I1 -Int B) +Int I3 => (I1 +Int I3) -Int B when #isConcrete(I1) andBool notBool #isConcrete(B) andBool #isConcrete(I3)
+
+    rule I1 +Int (I2 +Int C) => (I1 +Int I2) +Int C when #isConcrete(I1) andBool #isConcrete(I2) andBool notBool #isConcrete(C)
+    rule I1 +Int (I2 -Int C) => (I1 +Int I2) -Int C when #isConcrete(I1) andBool #isConcrete(I2) andBool notBool #isConcrete(C)
+    rule I1 -Int (I2 +Int C) => (I1 -Int I2) -Int C when #isConcrete(I1) andBool #isConcrete(I2) andBool notBool #isConcrete(C)
+    rule I1 -Int (I2 -Int C) => (I1 -Int I2) +Int C when #isConcrete(I1) andBool #isConcrete(I2) andBool notBool #isConcrete(C)
+
+    rule I1 &Int (I2 &Int C) => (I1 &Int I2) &Int C when #isConcrete(I1) andBool #isConcrete(I2) andBool notBool #isConcrete(C)
+
+    // for gas calculation
+    rule (#if C #then B1 #else B2 #fi) -Int A => #if C #then (B1 -Int A) #else (B2 -Int A) #fi
+        when notBool #isConcrete(A) andBool #notKLabel(A, "#if_#then_#else_#fi_K-EQUAL")
+```
+
+### #getKLabelString helpers
+
+Function below returns true if the KLabel of `T` is not `L`, or if `T` is a variable.
+```k
+    syntax Bool ::= #notKLabel ( K , String ) [function]
+    rule #notKLabel(T, L) => #getKLabelString(T) =/=String L orBool #isVariable(T)
+```
+
+
+```k
+
+endmodule
+```
diff --git a/resources/sum-to-n.md → resources/sum-to-n-common.md b/resources/sum-to-n.md → resources/sum-to-n-common.md
@@ -8,11 +8,9 @@ This program sums the numbers from 1 to N (for sufficiently small N), including
 
 ```{.k .sum-to-n}
 requires "edsl.k"
-requires "../lemmas.k"
 
-module VERIFICATION
+module VERIFICATION-COMMON
     imports EDSL
-    imports LEMMAS
     imports EVM-ASSEMBLY
 
     rule #sizeWordStack ( WS , N:Int )
@@ -44,7 +42,7 @@ Note that the program behaves incorrectly/unexpectedly if arithmetic overflow oc
 One challenge in verifying this program is to identify the conditions under which overflow does not occur.
 
 ```{.k .sum-to-n}
-module SUM-TO-N-SPEC
+module SUM-TO-N-COMMON
     imports VERIFICATION
 ```
 

diff --git a/resources/sum-to-n-haskell.md b/resources/sum-to-n-haskell.md
@@ -0,0 +1,20 @@
+The Sum To N Specification for the Haskell backend
+==================================================
+
+Uses the right imports for adapting the sum-to-n-common proof for the Haskell
+backend.
+
+```{.k .sum-to-n}
+requires "sum-to-n-common.k"
+requires "../lemmas-haskell.k"
+
+module VERIFICATION
+    imports VERIFICATION-COMMON
+    imports LEMMAS-HASKELL
+endmodule
+
+module SUM-TO-N-HASKELL-SPEC
+    imports VERIFICATION
+    imports SUM-TO-N-COMMON
+endmodule
+```
diff --git a/resources/sum-to-n-java.md b/resources/sum-to-n-java.md
@@ -0,0 +1,20 @@
+The Sum To N Specification for the Java backend
+==================================================
+
+Uses the right imports for adapting the sum-to-n-common proof for the Java
+backend.
+
+```{.k .sum-to-n}
+requires "sum-to-n-common.k"
+requires "../lemmas-java.k"
+
+module VERIFICATION
+    imports VERIFICATION-COMMON
+    imports LEMMAS-JAVA
+endmodule
+
+module SUM-TO-N-JAVA-SPEC
+    imports VERIFICATION
+    imports SUM-TO-N-COMMON
+endmodule
+```
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		b0b7ee6c94c4efd8fbcbb17b7a068db6af184684
		8def058cc3aab804e5a6ef111c6a889aaefb4495