diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index cf27f99a..8591228b 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -16,7 +16,7 @@ jobs: - name: Install Dafny uses: dafny-lang/setup-dafny-action@v1.6.1 with: - dafny-version: "3.13.0" + dafny-version: "4.2.0" - name: Setup Gradle uses: gradle/gradle-build-action@v2.4.2 diff --git a/build.gradle b/build.gradle index d6bf48f2..46a4cf10 100644 --- a/build.gradle +++ b/build.gradle @@ -38,27 +38,29 @@ if(project.hasProperty("randomize")) { // Configure boogie-specific flags. final BOOGIE_FLAGS = RANDOMIZE_FLAG -final DAFNY4_BASE_FLAGS = [ - '--resource-limit','1000000', - '--function-syntax','4', - '--quantifier-syntax','4'] - final DAFNY4_BUILD_FLAGS = [ 'build', '--no-verify', '--target','java', - '--output','build/libs/evm' -] + DAFNY4_BASE_FLAGS + '--output','build/libs/evm', + '--function-syntax','4', + '--quantifier-syntax','4', +] final DAFNY4_VERIFY_FLAGS = [ 'verify', + '--resource-limit','1000000', '--verify-included-files', '--log-format','csv;LogFileName=build/logs/verify.csv', - '--boogie'] + BOOGIE_FLAGS + DAFNY4_BASE_FLAGS + '--function-syntax','4', + '--quantifier-syntax','4', + '--boogie'] + BOOGIE_FLAGS final DAFNY4_TEST_FLAGS = [ - 'test' -] + DAFNY4_BASE_FLAGS + 'test', + '--function-syntax','4', + '--quantifier-syntax','4' +] // ====================================================================== // Dafny Build @@ -178,6 +180,7 @@ dependencies { implementation("org.web3j:rlp:5.0.0") implementation("org.web3j:crypto:5.0.0") implementation("org.whiley:evmtools:0.3.26") + implementation("org.dafny:DafnyRuntime:4.2.0") implementation files('build/libs/evm.jar') // testImplementation("org.junit.jupiter:junit-jupiter-api:5.7.0") diff --git a/src/dafny/core/stack.dfy b/src/dafny/core/stack.dfy index 958a339c..4924a0f3 100644 --- a/src/dafny/core/stack.dfy +++ b/src/dafny/core/stack.dfy @@ -24,7 +24,7 @@ module Stack { type ValidStackContent = xs: seq | |xs| <= CAPACITY /** The Stack type. */ - datatype Stack = Stack(contents: ValidStackContent) + datatype EvmStack = Stack(contents: ValidStackContent) { // Get number of items currently on this Stack. function Size(): nat { |contents| } @@ -37,7 +37,7 @@ module Stack { // Push word onto Stack. This requires that there is sufficient space for // that item. - function Push(val: u256): Stack + function Push(val: u256): EvmStack // Sanity check enough space. requires this.Size() < CAPACITY { Stack(contents:=([val] + contents)) @@ -60,21 +60,21 @@ module Stack { } // Pop word off of this Stack. This requires something to pop! - function Pop(): Stack + function Pop(): EvmStack // Sanity check something to pop. requires this.Size() > 0 { Stack(contents:= contents[1..]) } // Pop N words off of this Stack. This requires something to pop! - function PopN(n: nat): Stack + function PopN(n: nat): EvmStack // Sanity check something to pop. requires this.Size() >= n { Stack(contents:= contents[n..]) } /** Swap top item at index 0 and the k+1-th item at index k. */ - function Swap(k: nat) : Stack + function Swap(k: nat) : EvmStack requires this.Size() > k > 0 { var top := contents[0]; @@ -88,7 +88,7 @@ module Stack { * @param u An index. * @returns The stack made of the first u elements minus the first l. */ - function Slice(l: nat, u: nat): (r: Stack) + function Slice(l: nat, u: nat): (r: EvmStack) requires l <= u <= this.Size() { Stack(contents[l..u]) @@ -99,12 +99,11 @@ module Stack { const Empty := Stack(contents := []) /** Build a stack with some content. */ - function Make(xs: seq): Stack + function Make(xs: seq): EvmStack requires |xs| <= CAPACITY { Stack(contents := xs) } - /** Create an empty stack. */ - function Create(): Stack { Stack(contents := [])} - + // An empty evm stack + const EmptyEvmStack : EvmStack := Stack([]) } diff --git a/src/dafny/core/worldstate.dfy b/src/dafny/core/worldstate.dfy index ea7f0623..72792af2 100644 --- a/src/dafny/core/worldstate.dfy +++ b/src/dafny/core/worldstate.dfy @@ -29,7 +29,7 @@ module WorldState { import External // Sha3 hash of the empty sequence. - const HASH_EMPTYCODE : u256 := 0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470; + const HASH_EMPTYCODE : u256 := 0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470 /** * Account state associated with a given contract address. diff --git a/src/dafny/crypto/alt_bn128.dfy b/src/dafny/crypto/alt_bn128.dfy index cd937f54..42b042b1 100644 --- a/src/dafny/crypto/alt_bn128.dfy +++ b/src/dafny/crypto/alt_bn128.dfy @@ -20,7 +20,7 @@ module FiniteField { type pos = n:nat | n > 0 witness 1 // The number of elements in the given field. - const N : pos; + const N : pos // Define the raw set of field elements. type Field = n:nat | n < N @@ -63,9 +63,9 @@ module EllipticCurve refines FiniteField { // Define the so-called "point at infinity" const INFINITY : (nat,nat) := (0,0) // Parameter defining the curve - const A : Field; + const A : Field // Paramter defining the curve - const B : Field; + const B : Field /// Equation defining this particular elliptic curve. function Curve(x:Field,y:Field) : bool { // NOTE: should be field operations? @@ -140,12 +140,12 @@ module EllipticCurve refines FiniteField { // The ellptic curve given by y^2 == x^3 + 3. module AltBn128 refines EllipticCurve { // Specify the number of elements in the finite field - const N := ALT_BN128_PRIME; + const N := ALT_BN128_PRIME // As per EIP196 const ALT_BN128_PRIME := 21888242871839275222246405745257275088696311157297823662689037894645226208583 // Parameters for the curve - const A := 0; - const B := 3; + const A := 0 + const B := 3 // Axiom to establish that this is really a prime field. This is needed // because Dafny cannot possible determine that ALT_BN128_PRIME is a prime. diff --git a/src/dafny/evmstate.dfy b/src/dafny/evmstate.dfy index bd2927bc..bf9d8844 100644 --- a/src/dafny/evmstate.dfy +++ b/src/dafny/evmstate.dfy @@ -31,7 +31,7 @@ include "opcodes.dfy" module EvmState { import opened Int import opened Arrays - import Stack + import opened Stack import Memory import Storage import WorldState @@ -68,7 +68,7 @@ module EvmState { context: Context.T, precompiled: Precompiled.T, world : WorldState.T, - stack : Stack.Stack, + stack : EvmStack, memory : Memory.T, code: Code.T, substate: SubState.T, @@ -82,7 +82,7 @@ module EvmState { const EVM_WITNESS : Raw := EVM(Context.DEFAULT, Precompiled.DEFAULT, WorldState.Create(map[0:=WorldState.DefaultAccount()]), - Stack.Create(), + EmptyEvmStack, Memory.Create(), Code.Create([]), SubState.Create(), @@ -493,7 +493,7 @@ module EvmState { /** * Get the state of the internal stack. */ - function GetStack(): Stack.Stack + function GetStack(): EvmStack requires this.EXECUTING? { this.evm.stack } @@ -544,7 +544,7 @@ module EvmState { * @param u An index. * @returns A stack made of the first u elements of `st` minus the first `l`. */ - function SlicePeek(l: nat, u: nat): (r: Stack.Stack) + function SlicePeek(l: nat, u: nat): (r: EvmStack) requires this.EXECUTING? requires l <= u <= Operands() ensures r.Size() == u - l @@ -686,7 +686,7 @@ module EvmState { if |cod.contents| == 0 then RETURNS(gas, [], nw, substate) else // Construct fresh EVM - var stack := Stack.Create(); + var stack := EmptyEvmStack; var mem := Memory.Create(); var evm := EVM(ctx,precompiled,nw,stack,mem,cod,substate,gas,0); // Off we go! @@ -722,7 +722,7 @@ module EvmState { if |initcode| == 0 then RETURNS(gas, [], nw, substate) else // Construct fresh EVM - var stack := Stack.Create(); + var stack := EmptyEvmStack; var mem := Memory.Create(); var cod := Code.Create(initcode); // Mark new account as having been accessed diff --git a/src/main/java/dafnyevm/DafnyEvm.java b/src/main/java/dafnyevm/DafnyEvm.java index e4d8c532..1ca8ca5a 100644 --- a/src/main/java/dafnyevm/DafnyEvm.java +++ b/src/main/java/dafnyevm/DafnyEvm.java @@ -408,7 +408,7 @@ private static byte[] concat(byte[]... arrays) { /** *

* Represents the various possible states of the Dafny EVM. In effect, it is a - * wrapper for the Dafny data type EvmState.State. A key objective + * wrapper for the Dafny data type EvmState_Compile.State. A key objective * of this class is to isolate all of the Dafny specific data types from the * rest of the codebase. The states are: Ok (EVM running as * normal); CallContinue (EVM executing a CALL