Skip to content

Commit

Permalink
Helper changes for symbolic testing (#769)
Browse files Browse the repository at this point in the history 
* specs/lemmas.k: extracted some lemmas common to Java and Haskell to common module. Required for symbolic testing.

* evm-types: #lookup: marking [functional]. Sound change.

* lemmas: extra lemma for byte array simplification (+1 squashed commits)

Squashed commits:

[ca5056a] lemmas.k: extra for kore and symb-testing.

* symb-test: evm-types: Yi changes

* edsl,evm-types,serialization: extensions for symb-test

* edsl: small refactoring for symb-test

* formatting fixes

* Revert "symb-test: evm-types: Yi changes"

This reverts commit 8682019.

* evm-types, edsl: replacing some [functional] with #Ceil rules

* formatting fixes

* evm-types: One more #Ceil rule

* evm-types: #Ceil rule correction

* evm-types: replaced [functional] with #Ceil for #lookup

* lemmas: PR comments addressed

* evm-types: moved all #Ceil rules in one place, to be compatible with all backends.

* PR fixes

* PR fix - #Ceil(#buf) rule generates condition for SIZE and DATA

* symb-test: #Ceil rules for #padToWidth, #patRightToWidth corrected.

* symb-test: reverting rule #Ceil(#buf(SIZE, DATA)) to simplified form for performance reasons.

* evm-types, Makefile: tangle filter for #Ceil(padToWidth) & related rules.

* lemmas.k: [..] rule simplified

* lemmas.k: #sizeWordStack rule side conditions

* erc20/abstract-semantics-segmented-gas.k: dependency removed

* fix for previous

* evm-types: removed #Ceil rules for padLeftBytes, padRightBytes. Moved to k/domains.k

* edsl: Full #Ceil rule for #buf, but slow for erc20-verifier.

* evm-types: replaced 3 `#Ceil` rules with complete definition and [functional]

* Reverse commit "evm-types, Makefile: tangle filter for #Ceil(padToWidth) & related rules"

* formatting

* evm: performance enhancement driven by profiling ERC20 specs.

* Makefile: added tangle mode `symbolic-bytes` just for Haskell backend.

* evm-types: fixes

* evm-types: make #padToWidth and #padRightToWidth total

* evm-types: leave wordstack alone if negative update is provided

* evm: formatting

* Reverse commit "Makefile: added tangle mode `symbolic-bytes` just for Haskell backend."

Co-authored-by: Everett Hildenbrandt <[email protected]>
  • Loading branch information
@denis-bogdanas @ehildenb
denis-bogdanas and ehildenb authored May 12, 2020
1 parent 5b4d864 commit 309d449
Show file tree
Hide file tree
Showing 7 changed files with 64 additions and 48 deletions.
10 changes: 7 additions & 3 deletions edsl.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,9 +54,11 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
syntax ByteArray ::= #abiCallData ( String , TypedArgs ) [function]
// -------------------------------------------------------------------
rule #abiCallData( FNAME , ARGS )
=> #parseByteStack(substrString(Keccak256(#generateSignature(FNAME, ARGS)), 0, 8))
++ #encodeArgs(ARGS)
rule #abiCallData( FNAME , ARGS ) => #signatureCallData(FNAME, ARGS) ++ #encodeArgs(ARGS)
syntax ByteArray ::= #signatureCallData ( String, TypedArgs ) [function]
// ------------------------------------------------------------------------
rule #signatureCallData( FNAME , ARGS ) => #parseByteStack(substrString(Keccak256(#generateSignature(FNAME, ARGS)), 0, 8))
syntax String ::= #generateSignature ( String, TypedArgs ) [function]
| #generateSignatureArgs ( TypedArgs ) [function]
Expand Down Expand Up @@ -183,6 +185,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8)))
[concrete]
rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) andBool #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) #Equals true} [anywhere]
syntax Int ::= #getValue ( TypedArg ) [function]
// ------------------------------------------------
rule #getValue(#uint160( DATA )) => DATA
Expand Down
40 changes: 23 additions & 17 deletions evm-types.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -412,22 +412,25 @@ A cons-list is used for the EVM wordstack.
- `WS [ N := W ]` sets element $N$ of $WS$ to $W$ (padding with zeros as needed).

```k
syntax Int ::= WordStack "[" Int "]" [function]
// -----------------------------------------------
syntax Int ::= WordStack "[" Int "]" [function, functional]
// -----------------------------------------------------------
rule (W : _):WordStack [ N ] => W requires N ==Int 0
rule WS:WordStack [ N ] => #drop(N, WS) [ 0 ] requires N >Int 0
rule WS:WordStack [ N ] => 0 requires N <Int 0
syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function]
// --------------------------------------------------------------
syntax WordStack ::= WordStack "[" Int ":=" Int "]" [function, functional]
// --------------------------------------------------------------------------
rule (W0 : WS):WordStack [ N := W ] => W : WS requires N ==Int 0
rule (W0 : WS):WordStack [ N := W ] => W0 : (WS [ N -Int 1 := W ]) requires N >Int 0
rule WS:WordStack [ N := W ] => WS requires N <Int 0
rule .WordStack [ N := W ] => (0 : .WordStack) [ N := W ]
```

- Definedness conditions for `WS [ N ]` and `WS [ N := W ]`
- Definedness conditions for `WS [ N ]`:

```{.k .symbolic}
rule #Ceil(WS[N]) => {((0 <=Int N) andBool (N <Int #sizeWordStack(WS))) #Equals true} [anywhere]
rule #Ceil(WS[ N := W ]) => {((0 <=Int N) andBool (N <Int #sizeWordStack(WS))) #Equals true} [anywhere]
rule #Ceil(#lookup( _ |-> VAL M, KEY )) => {(#Ceil(#lookup( M, KEY )) andBool isInt(VAL)) #Equals true} [anywhere]
rule #Ceil(#lookup( .Map, _ )) => true [anywhere]
```

- `#sizeWordStack` calculates the size of a `WordStack`.
Expand Down Expand Up @@ -478,9 +481,10 @@ Most of EVM data is held in local memory.

```{.k .membytes}
syntax Memory = Bytes
syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, klabel(mapWriteBytes)]
// -------------------------------------------------------------------------------------
rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') [concrete]
syntax Memory ::= Memory "[" Int ":=" ByteArray "]" [function, functional, klabel(mapWriteBytes)]
// -------------------------------------------------------------------------------------------------
rule WS [ START := WS' ] => replaceAtBytes(padRightBytes(WS, START +Int #sizeByteArray(WS'), 0), START, WS') requires START >=Int 0 [concrete]
rule WS [ START := WS':ByteArray ] => .Memory requires START <Int 0 [concrete]
syntax ByteArray ::= #range ( Memory , Int , Int ) [function, functional]
// -------------------------------------------------------------------------
Expand Down Expand Up @@ -599,11 +603,13 @@ The local memory of execution is a byte-array (instead of a word-array).
// ----------------------------------------------------------------------------------------------------------------
rule #sizeByteArray ( WS ) => lengthBytes(WS) [concrete]
syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function]
| #padRightToWidth ( Int , ByteArray ) [function]
// --------------------------------------------------------------------
rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) [concrete]
rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) [concrete]
syntax ByteArray ::= #padToWidth ( Int , ByteArray ) [function, functional]
| #padRightToWidth ( Int , ByteArray ) [function, functional]
// --------------------------------------------------------------------------------
rule #padToWidth(N, BS) => BS requires notBool (N >=Int 0)
rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) requires N >=Int 0 [concrete]
rule #padRightToWidth(N, BS) => BS requires notBool (N >=Int 0)
rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) requires N >=Int 0 [concrete]
```

```{.k .nobytes}
Expand Down Expand Up @@ -686,8 +692,8 @@ Addresses
```k
syntax Int ::= #lookup ( Map , Int ) [function]
// -----------------------------------------------
rule [#lookup.some]: #lookup( (KEY |-> VAL) M, KEY ) => VAL
rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M)
rule [#lookup.some]: #lookup( (KEY |-> VAL:Int) M, KEY ) => VAL
rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M)
```

### Substate Log
Expand Down
4 changes: 2 additions & 2 deletions evm.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2496,8 +2496,8 @@ After interpreting the strings representing programs as a `WordStack`, it should
- `#dasmOpCode` interperets a `Int` as an `OpCode`.

```k
syntax OpCode ::= #dasmOpCode ( Int , Schedule ) [function]
// -----------------------------------------------------------
syntax OpCode ::= #dasmOpCode ( Int , Schedule ) [function, memo]
// -----------------------------------------------------------------
rule #dasmOpCode( 0, _ ) => STOP
rule #dasmOpCode( 1, _ ) => ADD
rule #dasmOpCode( 2, _ ) => MUL
Expand Down
4 changes: 2 additions & 2 deletions serialization.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ Address/Hash Helpers
- `keccak` serves as a wrapper around the `Keccak256` in `KRYPTO`.

```k
syntax Int ::= keccak ( ByteArray ) [function, smtlib(smt_keccak)]
// ------------------------------------------------------------------
syntax Int ::= keccak ( ByteArray ) [function, functional, smtlib(smt_keccak)]
// ------------------------------------------------------------------------------
rule [keccak]: keccak(WS) => #parseHexWord(Keccak256(#unparseByteStack(WS)))
```

Expand Down
3 changes: 1 addition & 2 deletions tests/specs/erc20/abstract-semantics-segmented-gas.k
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,8 @@
requires "evm-symbolic.k"
requires "../lemmas.k"

module ABSTRACT-SEMANTICS-SEGMENTED-GAS
imports EVM
imports EVM-SYMBOLIC
imports LEMMAS

// to avoid unnecessary case analyses
rule <k> LT W0 W1 => bool2Word(W0 <Int W1) ~> #push ... </k> [trusted]
Expand All @@ -27,4 +25,5 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
<gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
<callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
[trusted, matching(#gas)]

endmodule
2 changes: 2 additions & 0 deletions tests/specs/imp-specs/verification.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,14 @@ requires "../erc20/abstract-semantics-segmented-gas.k"
requires "edsl.k"
requires "../erc20/evm-symbolic.k"
requires "evm-imp-specs.k"
requires "../lemmas.k"

module VERIFICATION
imports ABSTRACT-SEMANTICS-SEGMENTED-GAS
imports EDSL
imports EVM-SYMBOLIC
imports EVM-IMP-SPECS
imports LEMMAS

//semantics of #buf
rule #buf(LEN, BYTES) => #padToWidth(LEN, #asByteStack( BYTES )) [concrete]
Expand Down
49 changes: 27 additions & 22 deletions tests/specs/lemmas.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,20 +5,43 @@ module LEMMAS
imports LEMMAS-JAVA
imports LEMMAS-HASKELL

rule WS ++ .ByteArray => WS [simplification]
rule .ByteArray ++ WS => WS [simplification]

//Byte array store operations sorting. Slices with lower index first. Helps applying rule below.
rule MEM [ N := BUF:ByteArray ] [ M := BUF' ] => MEM [ M := BUF' ] [ N := BUF ]
requires N >Int M andBool N -Int M >=Int #sizeByteArray(BUF') [simplification]

rule M [ N := BUF ] [ N := BUF' ] => M [ N := BUF' ] requires #sizeByteArray(BUF) ==Int #sizeByteArray(BUF') [simplification]

rule BUF [ L .. W ] => .ByteArray requires W ==Int 0 [simplification]
rule BUF [ 0 .. W ] => BUF requires W ==Int #sizeByteArray(BUF) [simplification]

rule #sizeByteArray(BUF1 ++ BUF2) => #sizeByteArray(BUF1) +Int #sizeByteArray(BUF2) [simplification]
rule #sizeByteArray(#buf(SIZE, _)) => SIZE [simplification]
rule #sizeByteArray(#buf(SIZE, _)[START .. WIDTH]) => WIDTH
requires #range(0 <= START < SIZE)
andBool #range(0 < WIDTH <= SIZE -Int START) [simplification]

rule #sizeByteArray(#range(_, START, WIDTH)) => WIDTH
requires WIDTH >=Int 0 andBool START >=Int 0 [simplification]

//Todo custom ==K unification doesn't work in Haskell yet
//++ unification
rule #buf(N, A) ++ BUF1 ==K #buf(N, B) ++ BUF2 => #buf(N, A) ==K #buf(N, B) andBool BUF1 ==K BUF2 [simplification]

endmodule

module LEMMAS-JAVA [symbolic, kast]
imports EVM
imports EDSL
imports K-REFLECTION

rule #asWord( BUF => #drop(1, BUF) ) requires BUF [ 0 ] ==Int 0 [simplification]
rule BUF [ L .. W ] => .ByteArray requires L >=Int #sizeByteArray(BUF) [simplification]

rule WS ++ .ByteArray => WS [simplification]
rule #asWord( BUF => #drop(1, BUF) ) requires BUF [ 0 ] ==Int 0 [simplification]

rule #sizeByteArray(W : WS) => 1 +Int #sizeByteArray(WS) [simplification]
rule #sizeByteArray(#buf(N, _) ) => N [simplification]
rule #sizeByteArray(BUF1 ++ BUF2) => #sizeByteArray(BUF1) +Int #sizeByteArray(BUF2) [simplification]
rule #sizeByteArray(#drop(N, BUF)) => maxInt(#sizeByteArray(BUF) -Int N, 0) [simplification]

rule #take(N, BUF) => BUF requires N ==Int #sizeByteArray(BUF) [simplification]
Expand All @@ -33,12 +56,6 @@ module LEMMAS-JAVA [symbolic, kast]

rule #asWord(BUF) /Int 26959946667150639794667015087019630673637144422540572481103610249216 => #asWord(#take(4, BUF)) [simplification]

rule M [ N := BUF ] [ N := BUF' ] => M [ N := BUF' ] requires #sizeByteArray(BUF) ==Int #sizeByteArray(BUF') [simplification]

rule BUF [ L .. W ] => .ByteArray requires W <=Int 0 [simplification]
rule BUF [ 0 .. W ] => BUF requires W ==Int #sizeByteArray(BUF) [simplification]
rule BUF [ L .. W ] => .ByteArray requires L >Int #sizeByteArray(BUF) [simplification]

rule #range(M, N, K) => .ByteArray requires notBool K >Int 0 [simplification]

rule #range(M [ N := BUF:ByteArray ], L, K) => #range(M, L, minInt(K, N -Int L)) ++ #range(M [ N := BUF ], N, K -Int minInt(K, N -Int L))
Expand Down Expand Up @@ -213,18 +230,6 @@ module LEMMAS-HASKELL [symbolic, kore]
imports EVM
imports EDSL

rule WS ++ .ByteArray => WS [simplification]
rule .ByteArray ++ WS => WS [simplification]

rule #sizeByteArray(BUF1 ++ BUF2) => #sizeByteArray(BUF1) +Int #sizeByteArray(BUF2) [simplification]
rule #sizeByteArray(#buf(SIZE, _)) => SIZE [simplification]
rule #sizeByteArray(#buf(SIZE, _)[START .. WIDTH]) => WIDTH
requires #range(0 <= START < SIZE)
andBool #range(0 < WIDTH <= SIZE -Int START) [simplification]

rule BUF [ L .. W ] => .ByteArray requires W <=Int 0 [simplification]
rule BUF [ 0 .. W ] => BUF requires W ==Int #sizeByteArray(BUF) [simplification]

rule (BUF1 ++ BUF2)[START .. WIDTH] => (BUF1[START .. #sizeByteArray(BUF1) -Int START]) ++ (BUF2[0 .. START +Int WIDTH -Int #sizeByteArray(BUF1)])
requires #range(0 <= START < #sizeByteArray(BUF1))
andBool #sizeByteArray(BUF1) <Int START +Int WIDTH [simplification]
Expand Down

0 comments on commit 309d449

Please sign in to comment.