Fixes for PR

Some minor fixes which were causing the PR to fail.  Specifically, `t8n`
interface was not passing in a `basefee` parameter, and one verification
test was failing.

Author: DavePearce

src/dafny/t8n.dfy

@@ -70,7 +70,7 @@ include "core/precompiled.dfy"
         var callData : seq<u8> := [12];
         var writePermission := true;
         var gasPrice := 12;
-        var blockInfo := Context.Info(1,2,3,4,5,6);
+        var blockInfo := Context.Info(1,2,3,4,5,6,7);
         var context := Context.Create(sender, origin, recipient, callValue, callData, writePermission, gasPrice, blockInfo);
 
         var senderAccount := WorldState.Account(1,2,Storage.Create(map[]),emptyCode, 0);

src/test/dafny/proofs/FM-paper.dfy

@@ -58,17 +58,16 @@ module Kontract1 {
         /** The contract never runs out of gas. */
         ensures (st'.ERROR? && st'.error == REVERTS) || st'.RETURNS?
         /** It terminates normally iff storage at loc 0 is < MAX_U256. */
-        ensures st'.RETURNS? <==> (st.Load(0) as nat) < MAX_U256
+        ensures st'.RETURNS? ==> (st.Load(0) as nat) < MAX_U256
         /** The world state's accounts do not change. */
         ensures st'.RETURNS? ==> st'.world.accounts.Keys == st.evm.world.accounts.Keys
         /** Normal termination implies storage at Loc 0 has been incremented by 1. */
         ensures st'.RETURNS? ==> st'.world.Read(st.evm.context.address,0) as nat == st.Load(0) as nat + 1
     {
         // Assumption required because Z3 cannot figure this out!
         assume {:axiom} {PUSH1,SLOAD,ADD,DUP1,JUMPI,REVERT,JUMPDEST,SSTORE,STOP} <= EvmFork.BERLIN_BYTECODES;
-        //
         //  Execute 7 steps (PUSH1, 0x00, SLOAD, PUSH1, 0x01, ADD, DUP1, PUSH1, 0xf, JUMPI)
-        st' := ExecuteN(st,7);
+        st' := ExecuteN(st,7);        
         assert (st'.PC() == 0xa || st'.PC() == 0xf);
         // Peek(0) == 0 iff an overflow occurred in the increment.
         if st'.Peek(0) == 0 {