Update Dafny / Java code for Dafny 4.2.0

This makes a small number of adjustments to the Dafny code (e.g.
removing unnecessary semi-colons) and the Java code (e.g. Dafny naming
has changed from `EvmState_Compile` to just `EvmState`).  This adds the
DafnyRuntime as a Maven dependency, since it is now available.

Various updates were required to the `build.gradle` file related to
ordering of command-line arguments, etc.  Obviously the CLI is getting a
bit stricter.

.github/workflows/build.yml

@@ -16,7 +16,7 @@ jobs:
       - name: Install Dafny
         uses: dafny-lang/[email protected]
         with:
-          dafny-version: "3.13.0"
+          dafny-version: "4.2.0"
 
       - name: Setup Gradle
         uses: gradle/[email protected]

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")

src/dafny/core/stack.dfy

@@ -24,7 +24,7 @@ module Stack {
     type ValidStackContent = xs: seq<u256> | |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<u256>): Stack
+    function Make(xs: seq<u256>): EvmStack
         requires |xs| <= CAPACITY {
             Stack(contents := xs)
     }
 
-    /** Create an empty stack. */
-    function Create(): Stack { Stack(contents := [])}
-
+    // An empty evm stack
+    const EmptyEvmStack : EvmStack := Stack([])
 }

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.

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.

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

src/main/java/dafnyevm/DafnyEvm.java

@@ -408,7 +408,7 @@ private static byte[] concat(byte[]... arrays) {
 	/**
 	 * <p>
 	 * Represents the various possible states of the Dafny EVM. In effect, it is a
-	 * wrapper for the Dafny data type <code>EvmState.State</code>. A key objective
+	 * wrapper for the Dafny data type <code>EvmState_Compile.State</code>. 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: <code>Ok</code> (EVM running as
 	 * normal); <code>CallContinue</code> (EVM executing a <code>CALL</code>