From 18bc41ef1b16b6a840f815ab2161508124c2fe74 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Fri, 13 Dec 2019 17:57:39 +0200 Subject: [PATCH 1/2] Roll me back --- .build/.k.rev | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.build/.k.rev b/.build/.k.rev index 9c3af0e5e..34f281dff 100644 --- a/.build/.k.rev +++ b/.build/.k.rev @@ -1 +1 @@ -b0b7ee6c94c4efd8fbcbb17b7a068db6af184684 +8def058cc3aab804e5a6ef111c6a889aaefb4495 \ No newline at end of file From cfe57c607d912a8b4e42ae8ee7b91715ac963532 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Fri, 13 Dec 2019 20:42:07 +0200 Subject: [PATCH 2/2] Refactor lemmas so that they work with the Haskell backend. --- resources/Makefile | 11 ++- resources/kprove.mak | 19 ++++-- resources/{lemmas.md => lemmas-common.md} | 35 +--------- resources/lemmas-haskell.md | 11 +++ resources/lemmas-java.md | 68 +++++++++++++++++++ resources/{sum-to-n.md => sum-to-n-common.md} | 6 +- resources/sum-to-n-haskell.md | 20 ++++++ resources/sum-to-n-java.md | 20 ++++++ 8 files changed, 146 insertions(+), 44 deletions(-) rename resources/{lemmas.md => lemmas-common.md} (86%) create mode 100644 resources/lemmas-haskell.md create mode 100644 resources/lemmas-java.md rename resources/{sum-to-n.md => sum-to-n-common.md} (98%) create mode 100644 resources/sum-to-n-haskell.md create mode 100644 resources/sum-to-n-java.md diff --git a/resources/Makefile b/resources/Makefile index 83329336e..09297cd9a 100644 --- 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 index bae82f313..82c6b0dc8 100644 --- 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 b/resources/lemmas-common.md similarity index 86% rename from resources/lemmas.md rename to resources/lemmas-common.md index 41375240a..8747584f8 100644 --- a/resources/lemmas.md +++ b/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 #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 new file mode 100644 index 000000000..fa91c83aa --- /dev/null +++ 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 new file mode 100644 index 000000000..041f95578 --- /dev/null +++ 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 b/resources/sum-to-n-common.md similarity index 98% rename from resources/sum-to-n.md rename to resources/sum-to-n-common.md index 98b567a12..6057e87c3 100644 --- a/resources/sum-to-n.md +++ b/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 new file mode 100644 index 000000000..8a9775a87 --- /dev/null +++ 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 new file mode 100644 index 000000000..373dd07bf --- /dev/null +++ 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 +```