Skip to content
Permalink
Browse files

Full migration to kevm-imap. Projects using old map model now depend …

…on an extra module: evm-semantics-map-concrete.k, which contains copies of rules from kevm, but without [concrete].
  • Loading branch information...
denis-bogdanas committed Apr 14, 2019
1 parent c33e46e commit 86bf8aa87757486f2077e4cc3a49f299e78586b1
@@ -1,9 +1,11 @@
requires "evm-symbolic.k"
requires "evm-data-map-concrete.k"
requires "edsl.k"
requires "../lemmas.k"

module VERIFICATION
imports EVM-SYMBOLIC
imports EVM-DATA-MAP-CONCRETE
imports EDSL
imports LEMMAS

@@ -1,9 +1,11 @@
requires "evm-symbolic.k"
requires "evm-data-map-concrete.k"
requires "edsl.k"
requires "../lemmas.k"

module VERIFICATION
imports EVM-SYMBOLIC
imports EVM-DATA-MAP-CONCRETE
imports EDSL
imports LEMMAS

@@ -1,7 +1,8 @@
BUILD_DIR:=../.build

LOCAL_LEMMAS:=verification.k \
../../resources/evm-symbolic.k ../../resources/abstract-semantics-common.k
../../resources/evm-symbolic.k ../../resources/evm-data-map-concrete.k \
../../resources/abstract-semantics-common.k
TMPLS:=../module-tmpl.k ../spec-tmpl.k

SPEC_GROUP:=ds-token-erc20
@@ -1,9 +1,11 @@
requires "evm-symbolic.k"
requires "evm-data-map-concrete.k"
requires "edsl.k"
requires "../lemmas.k"

module VERIFICATION
imports EVM-SYMBOLIC
imports EVM-DATA-MAP-CONCRETE
imports EDSL
imports LEMMAS

@@ -1,7 +1,8 @@
BUILD_DIR:=../.build

LOCAL_LEMMAS:=verification.k \
../../resources/evm-symbolic.k ../../resources/abstract-semantics-common.k
../../resources/evm-symbolic.k ../../resources/evm-data-map-concrete.k \
../../resources/abstract-semantics-common.k
TMPLS:=../module-tmpl.k spec-tmpl.k

SPEC_GROUP:=gno-erc20
@@ -1,9 +1,11 @@
requires "evm-symbolic.k"
requires "evm-data-map-concrete.k"
requires "edsl.k"
requires "../lemmas.k"

module VERIFICATION
imports EVM-SYMBOLIC
imports EVM-DATA-MAP-CONCRETE
imports EDSL
imports LEMMAS

@@ -1,7 +1,8 @@
BUILD_DIR:=../.build

LOCAL_LEMMAS:=verification.k \
../../resources/evm-symbolic.k ../../resources/abstract-semantics-common.k
../../resources/evm-symbolic.k ../../resources/evm-data-map-concrete.k \
../../resources/abstract-semantics-common.k
TMPLS:=../module-tmpl.k ../spec-tmpl.k

SPEC_GROUP:=hkg-erc20
@@ -1,9 +1,11 @@
requires "evm-symbolic.k"
requires "evm-data-map-concrete.k"
requires "edsl.k"
requires "../lemmas.k"

module VERIFICATION
imports EVM-SYMBOLIC
imports EVM-DATA-MAP-CONCRETE
imports EDSL
imports LEMMAS

@@ -1,7 +1,8 @@
BUILD_DIR:=../.build

LOCAL_LEMMAS:=verification.k \
../../resources/evm-symbolic.k ../../resources/abstract-semantics-common.k
../../resources/evm-symbolic.k ../../resources/evm-data-map-concrete.k \
../../resources/abstract-semantics-common.k
TMPLS:=../module-tmpl.k ../spec-tmpl.k

SPEC_GROUP:=hobby-erc20
@@ -1,9 +1,11 @@
requires "evm-symbolic.k"
requires "evm-data-map-concrete.k"
requires "edsl.k"
requires "../lemmas.k"

module VERIFICATION
imports EVM-SYMBOLIC
imports EVM-DATA-MAP-CONCRETE
imports EDSL
imports LEMMAS

@@ -1,10 +1,10 @@
requires "evm-symbolic.k"
requires "evm-data-symbolic.k"
requires "evm-data-map-symbolic.k"
requires "../lemmas.k"

module VERIFICATION
imports EVM-SYMBOLIC
imports EVM-DATA-SYMBOLIC
imports EVM-DATA-MAP-SYMBOLIC
imports EDSL
imports LEMMAS

@@ -1,7 +1,7 @@
BUILD_DIR:=../../.build

LOCAL_LEMMAS:=../verification.k \
../../resources/evm-symbolic.k ../../resources/evm-data-symbolic.k \
../../resources/evm-symbolic.k ../../resources/evm-data-map-symbolic.k \
../../resources/abstract-semantics-common.k
TMPLS:=../module-tmpl.k ../spec-tmpl.k

@@ -1,7 +1,7 @@
BUILD_DIR:=../../.build

LOCAL_LEMMAS:=../verification.k \
../../resources/evm-symbolic.k ../../resources/evm-data-symbolic.k \
../../resources/evm-symbolic.k ../../resources/evm-data-map-symbolic.k \
../../resources/abstract-semantics-common.k
TMPLS:=../module-tmpl.k ../spec-tmpl.k

@@ -1,7 +1,7 @@
BUILD_DIR:=../.build

LOCAL_LEMMAS:=abstract-semantics.k verification.k \
../resources/evm-symbolic.k ../resources/evm-data-symbolic.k ../resources/ecrec-symbolic.k \
../resources/evm-symbolic.k ../resources/evm-data-map-symbolic.k ../resources/ecrec-symbolic.k \
../resources/abstract-semantics-common.k
TMPLS:=module-tmpl.k spec-tmpl.k

@@ -1,7 +1,7 @@
BUILD_DIR:=../../.build

LOCAL_LEMMAS:=../abstract-semantics.k ../verification.k ../../resources/evm-symbolic.k \
../../resources/evm-data-symbolic.k ../../resources/ecrec-symbolic.k \
../../resources/evm-data-map-symbolic.k ../../resources/ecrec-symbolic.k \
../../resources/abstract-semantics-common.k
TMPLS:=../module-tmpl.k ../spec-tmpl.k

@@ -1,10 +1,10 @@
requires "evm-symbolic.k"
requires "evm-data-symbolic.k"
requires "evm-data-map-symbolic.k"
requires "../lemmas.k"

module VERIFICATION
imports EVM-SYMBOLIC
imports EVM-DATA-SYMBOLIC
imports EVM-DATA-MAP-SYMBOLIC
imports EDSL
imports LEMMAS

@@ -2,8 +2,9 @@ BUILD_DIR:=../erc20/.build

# verification.k is required to import evm-symbolic.k
LOCAL_LEMMAS:=abstract-semantics.k verification.k \
../resources/evm-symbolic.k ../resources/ecrec-symbolic.k \
../resources/abstract-semantics-common.k
../resources/evm-symbolic.k ../resources/evm-data-map-concrete.k \
../resources/abstract-semantics-common.k \
../resources/ecrec-symbolic.k

# Just to have the simplest initial config
TMPLS:=../gnosis/module-tmpl.k spec-tmpl.k
@@ -1,8 +1,10 @@
requires "evm-symbolic.k"
requires "evm-data-map-concrete.k"
requires "../lemmas.k"

module VERIFICATION
imports EVM-SYMBOLIC
imports EVM-DATA-MAP-CONCRETE
imports EDSL
imports LEMMAS

@@ -1,11 +1,13 @@
requires "evm-symbolic.k"
requires "evm-data-map-concrete.k"
requires "edsl.k"
requires "../lemmas.k"

module VERIFICATION
imports EDSL
imports LEMMAS
imports EVM-SYMBOLIC
imports EVM-DATA-MAP-CONCRETE

rule #sizeWordStack(WS, N) <Int SIZE => #sizeWordStack(WS, 0) +Int N <Int SIZE requires N =/=Int 0
rule SIZELIMIT <Int #sizeWordStack(WS, N) +Int DELTA => SIZELIMIT <Int (#sizeWordStack(WS, 0) +Int N) +Int DELTA requires N =/=Int 0
@@ -0,0 +1,20 @@
requires "edsl.k"

module EVM-DATA-MAP-CONCRETE [symbolic]
imports K-REFLECTION
imports EVM-DATA
imports EDSL

// Same rules exist in KEVM, but are marked [concrete]. Allowing them for symbolic arguments here.

rule #lookup( (KEY |-> VAL) M, KEY ) => VAL
rule #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M)

rule #range(WM, START, WIDTH) => #range(WM, START +Int WIDTH -Int 1, WIDTH, .WordStack)

rule WM[ N := W : WS ] => (WM[N <- W])[N +Int 1 := WS]

//semantics of #buf
rule #buf(LEN, BYTES) => #padToWidth(LEN, #asByteStack( BYTES ))

endmodule
@@ -1,6 +1,6 @@
requires "edsl.k"

module EVM-DATA-SYMBOLIC [symbolic]
module EVM-DATA-MAP-SYMBOLIC [symbolic]
imports K-REFLECTION
imports EVM-DATA
imports EDSL
@@ -22,7 +22,7 @@ $(error SPEC_NAMES is not set)
endif

SPEC_INI?=spec.ini
LOCAL_LEMMAS?=../resources/abstract-semantics-common.k verification.k
LOCAL_LEMMAS?=../resources/abstract-semantics-common.k ../resources/evm-data-map-concrete.k verification.k
TMPLS?=module-tmpl.k spec-tmpl.k

# additional options to kprove command

0 comments on commit 86bf8aa

Please sign in to comment.
You can’t perform that action at this time.