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

@@ -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

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'

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