From 41b5e7f4f48a7f40fa9b43c419b55cf7ea8599c0 Mon Sep 17 00:00:00 2001
From: DavePearce <dave01001110@gmail.com>
Date: Wed, 9 Oct 2024 11:10:10 +0100
Subject: [PATCH] Updating to Dafny `4.8.1`

This makes some changes which allow the DafnyEVM to compile and verify
under Dafny 4.8.1.
---
 .github/workflows/build.yml    | 4 ++--
 build.gradle                   | 3 +++
 src/dafny/core/precompiled.dfy | 2 +-
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 9b063d89..53dab90f 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -22,7 +22,7 @@ jobs:
           cache: 'gradle'        
       - uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
-          dafny-version: "4.4.0"
+          dafny-version: "4.8.1"
       - name: Set DAFNY_HOME
         run: echo "DAFNY_HOME=$(dirname $(which dafny))" >> $GITHUB_ENV
         # Build
@@ -50,7 +50,7 @@ jobs:
           cache: 'gradle'    
       - uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
-          dafny-version: "4.4.0"
+          dafny-version: "4.8.1"
       - name: Set DAFNY_HOME
         run: echo "DAFNY_HOME=$(dirname $(which dafny))" >> $GITHUB_ENV
         # Build
diff --git a/build.gradle b/build.gradle
index b77f7de2..fce7944a 100644
--- a/build.gradle
+++ b/build.gradle
@@ -64,6 +64,7 @@ final BOOGIE_FLAGS = RANDOMIZE_FLAG
 final DAFNY4_BUILD_FLAGS = [
     'build',
     '--no-verify',
+    '--allow-warnings',
     '--target','java',
     '--output','build/libs/evm',
     '--function-syntax','4',
@@ -72,6 +73,7 @@ final DAFNY4_BUILD_FLAGS = [
 
 final DAFNY4_VERIFY_FLAGS = [
     'verify',
+    '--allow-warnings',    
     '--resource-limit','1000000',
     '--verify-included-files',
     '--log-format','csv;LogFileName=build/logs/verify.csv',
@@ -81,6 +83,7 @@ final DAFNY4_VERIFY_FLAGS = [
 
 final DAFNY4_TEST_FLAGS = [
     'test',
+    '--allow-warnings',    
     '--target','java',
     '--function-syntax','4',
     '--quantifier-syntax','4'
diff --git a/src/dafny/core/precompiled.dfy b/src/dafny/core/precompiled.dfy
index fff4642f..c7b5c53e 100644
--- a/src/dafny/core/precompiled.dfy
+++ b/src/dafny/core/precompiled.dfy
@@ -183,7 +183,7 @@ module Precompiled {
      * See also EIP-2565.  Observe that efforts are made to avoid unnecessary
      * calculations where possible.
      */
-    function CallModExp(data: Array<u8>) : Option<(Array<u8>,nat)> {
+    function {:verify false} CallModExp(data: Array<u8>) : Option<(Array<u8>,nat)> {
         // Length of B
         var lB := ByteUtils.ReadUint256(data,0) as nat;
         // Length of E