#[local] Open Scope lens_scope.

Notation u256t := (Tnamed (Ninst (Nscoped (Nglobal (Nid "intx")) (Nid "uint")) [Avalue (Eint 256 "unsigned int")])).

Notation resultn ty :=
                  (Ninst (Nscoped (Nscoped (Nglobal (Nid "boost")) (Nid "outcome_v2")) (Nid "basic_result"))
                   [Atype ty;
                    Atype
                      (Tnamed
                         (Ninst (Nscoped (Nglobal (Nid "system_error2")) (Nid "errored_status_code")) [Atype (Tnamed (Ninst (Nscoped (Nscoped (Nglobal (Nid "system_error2")) (Nid "detail")) (Nid "erased")) [Atype "long"]))]));
                    Atype
                      (Tnamed
                         (Ninst (Nscoped (Nscoped (Nscoped (Nscoped (Nglobal (Nid "boost")) (Nid "outcome_v2")) (Nid "experimental")) (Nid "policy")) (Nid "status_code_throw"))
                            [Atype ty;
                             Atype
                               (Tnamed
                                  (Ninst (Nscoped (Nglobal (Nid "system_error2")) (Nid "errored_status_code"))
                                     [Atype (Tnamed (Ninst (Nscoped (Nscoped (Nglobal (Nid "system_error2")) (Nid "detail")) (Nid "erased")) [Atype "long"]))]));
                             Atype "void"]))]).

  Record AccountSubstateModel : Type := {
    asm_destructed : bool;
    asm_touched : bool;
    asm_accessed : bool;
    asm_accessed_keys : list Corelib.Numbers.BinNums.N
  }.

#[local] Open Scope Z_scope.

Record AssumptionExactness :=
  {
    min_balance: option N;
    nonce_exact: bool;
  }.

Record AssumedPreTxAccountState :=
  {
    preTxState : option AccountM;
    preTxStorage : list (N × N);
    assumExactness: AssumptionExactness;
  }.

Record UpdatedAccountState :=
  {
    postTxState: option AccountM;
    substateModel : AccountSubstateModel;
  }.

Record TxAssumptionsAndUpdates :=
  {
    preAssumption: AssumedPreTxAccountState;
    originalLoc: ptr;
    txUpdates : option (ptr*(ptr ×UpdatedAccountState));
  }.

Definition check_min_balance_ok (cur debit: N) : bool :=
  bool_decide (debit ≤ cur)%N.

Definition min_balance_update
           (old: AssumptionExactness)
           (orig cur debit: N) : AssumptionExactness :=
  if check_min_balance_ok cur debit then
    match min_balance old with
    | None ⇒ old
    | Some old_min ⇒
        
        let diff := N.sub cur debit in
        let new_min :=
          if N.ltb diff orig
          then N.max old_min (N.sub orig diff)
          else old_min in
        {| min_balance := Some new_min;
           nonce_exact := nonce_exact old |}
    end
  else
    
    {| min_balance := None;
       nonce_exact := nonce_exact old |}.

Definition update_assum_exactness_at
           (addr: evm.address)
           (f: AssumptionExactness → AssumptionExactness)
           (m: MapModel evm.address AssumedPreTxAccountState)
  : MapModel evm.address AssumedPreTxAccountState :=
  map (fun p ⇒
         let '(addr', (loc, aps)) := p in
         if bool_decide (addr' = addr) then
           (addr', (loc,
                    {| preTxState := preTxState aps;
                       preTxStorage := preTxStorage aps;
                       assumExactness := f (assumExactness aps) |}))
         else p) m.

Definition exact_balance_update
           (old: AssumptionExactness) : AssumptionExactness :=
  {| min_balance := None;
     nonce_exact := nonce_exact old |}.

Module OneTbbMap. Section with_Sigma.
  Context `{Sigma:cpp_logic} {CU: genv} {hh: HasOwn mpredI fracR}.
  Definition Rauth {K V:Type} (tykey tyval: type) (khash: K → N) {eqd: EqDecision K}
           (krep : Qp → K → Rep)
           (vrep : Qp → V → Rep)
           
           (q: stdpp.numbers.Qp)
           (m: list (K×V))
    : Rep.

  Definition Rfrag {K V:Type} (tykey tyval: type) (khash: K → N) `{EqDecidable K}
           (krep : K → Rep)
           (vrep : V → Rep)
           (q: stdpp.numbers.Qp): Rep.

End with_Sigma. End OneTbbMap.

Section with_Sigma.
  Context `{Sigma:cpp_logic} {CU: genv} {hh: HasOwn mpredI fracR}.
  Definition u256R (q:Qp) (n:N) : Rep.

  Fixpoint bytes32_be_values_from (len : nat) (z : N) : list val :=
    match len with
    | O ⇒ []
    | S len' ⇒
        Vint (Z.of_N (N.land (N.shiftr z (8 × N.of_nat len')) 255))
        :: bytes32_be_values_from len' z
    end.

  Definition bytes32_be_values (z : N) : list val :=
    bytes32_be_values_from 32 z.

  Definition evmc_bytes32_wordR (q : Qp) (z : N) : Rep :=
    _field "evmc_bytes32::bytes"
      |-> (type_ptrR (Tarray Tuchar 32)
          ** arrayR Tuchar (primR Tuchar (cQp.mut q))
               (bytes32_be_values z))
    ** structR "evmc_bytes32"%cpp_name (cQp.mut q).

  Definition bytes32R (q : Qp) (z : N) : Rep :=
    structR "evmc::bytes32"%cpp_name (cQp.mut q)
    ** _base "evmc::bytes32"%cpp_name "evmc_bytes32"%cpp_name
       |-> evmc_bytes32_wordR q z
    ** pureR [| (z < 2 ^ 256)%N |].

  Definition evmc_bytes32R (q : Qp) : Rep :=
    evmc_bytes32_wordR q 0.

  Lemma evmc_bytes32R_zero_fold
      `{MODd : state_cpp.module ⊧ CU} (p : ptr) :
    p ,, o_field CU "evmc_bytes32::bytes"
      |-> arrayR Tuchar (primR Tuchar 1$m) (replicateN 32 (Vint 0))
    ** p |-> structR "evmc_bytes32"%cpp_name 1$m
    |-- p |-> evmc_bytes32R 1.

  Definition evmc_bytes32R_zero_fold_B
      `{MODd : state_cpp.module ⊧ CU} p :=
    [BWD] (evmc_bytes32R_zero_fold p).

  Lemma evmc_bytes32R_zero_unfold
      `{MODd : state_cpp.module ⊧ CU} (p : ptr) :
    p |-> evmc_bytes32R 1
    |--
    p ,, o_field CU "evmc_bytes32::bytes"
      |-> arrayR Tuchar (primR Tuchar 1$m) (replicateN 32 (Vint 0))
    ** p |-> structR "evmc_bytes32"%cpp_name 1$m.

  Definition evmc_bytes32R_zero_unfold_F
      `{MODd : state_cpp.module ⊧ CU} p :=
    [FWD] (evmc_bytes32R_zero_unfold p).

  Definition DeltaR {T:Type} (ty: type) (Trep : Qp→ T → Rep) (q:Qp) (beforeafter: T × T) : Rep.

  Definition AccessedKeysR (q: stdpp.numbers.Qp)
           (keys: list Corelib.Numbers.BinNums.N)
    : skylabs.lang.cpp.logic.rep_defs.Rep :=
    anyR
      "ankerl::unordered_dense::v4_1_0::detail::table<evmc::bytes32, void, ankerl::unordered_dense::v4_1_0::hash<evmc::bytes32, void>, std::equal_to<evmc::bytes32>, std::allocator<evmc::bytes32>, ankerl::unordered_dense::v4_1_0::bucket_type::standard, 0b>"%cpp_type
      (cQp.mut q).

  Definition StorageMapKeyTy : type :=
    Tnamed (Nscoped (Nglobal (Nid "evmc")) (Nid "bytes32")).

  Definition StorageMapHashName : name :=
    Ninst
      (Nscoped
        (Nscoped
          (Nscoped (Nglobal (Nid "ankerl")) (Nid "unordered_dense"))
          (Nid "v4_1_0"))
        (Nid "hash"))
      [Atype StorageMapKeyTy; Atype Tvoid].

  Definition StorageMapEqName : name :=
    Ninst (Nscoped (Nglobal (Nid "std")) (Nid "equal_to"))
      [Atype StorageMapKeyTy].

  Definition StorageMapHeapPolicyName : name :=
    Ninst (Nscoped (Nglobal (Nid "immer")) (Nid "free_list_heap_policy"))
      [Atype (Tnamed (Nscoped (Nglobal (Nid "immer")) (Nid "cpp_heap")));
       Avalue (Eint 1024 Tulong)].

  Definition StorageMapMemoryPolicyName : name :=
    Ninst (Nscoped (Nglobal (Nid "immer")) (Nid "memory_policy"))
      [Atype (Tnamed StorageMapHeapPolicyName);
       Atype (Tnamed (Nscoped (Nglobal (Nid "immer")) (Nid "refcount_policy")));
       Atype (Tnamed (Nscoped (Nglobal (Nid "immer")) (Nid "spinlock_policy")));
       Atype (Tnamed (Nscoped (Nglobal (Nid "immer")) (Nid "no_transience_policy")));
       Avalue (Eint 0 Tbool);
       Avalue (Eint 1 Tbool)].

  Definition StorageMapName : name :=
    Ninst (Nscoped (Nglobal (Nid "immer")) (Nid "map"))
      [Atype StorageMapKeyTy;
       Atype StorageMapKeyTy;
       Atype (Tnamed StorageMapHashName);
       Atype (Tnamed StorageMapEqName);
       Atype (Tnamed StorageMapMemoryPolicyName);
       Avalue (Eint 5 Tuint)].

  Definition StorageMapTy : type := Tnamed StorageMapName.

  Definition StorageMapR (q: Qp)
             (m: list (N×N)) : Rep :=
    immer_specs.ImmerMapR StorageMapTy bytes32R bytes32R q m.

  Definition account_code (am: AccountM) : evm.program :=
    block.block_account_code (coreAc am).

  Definition code_entry_of_updates
      (updates: list (ptr × UpdatedAccountState))
    : option (N × evm.program) :=
    match updates with
    | (_, up) :: _ ⇒
        match postTxState up with
        | Some am ⇒
            let code := account_code am in
            Some (code_hash_of_program code, code)
        | None ⇒ None
        end
    | [] ⇒ None
    end.

Definition code_entries_of_state
      (m: MapModel evm.address (list (ptr × UpdatedAccountState)))
    : list (N × evm.program) :=
    fold_right (fun kv acc ⇒
      let '(_, (_, updates)) := kv in
      match code_entry_of_updates updates with
      | Some kv' ⇒ kv' :: acc
      | None ⇒ acc
      end) [] m.

  Definition code_entry_of_assumed
      (aps: AssumedPreTxAccountState) : option (N × evm.program) :=
    match preTxState aps with
    | Some am ⇒
        let code := account_code am in
        Some (code_hash_of_program code, code)
    | None ⇒ None
    end.

  Definition code_entries_of_preTxAssumed
      (m: MapModel evm.address AssumedPreTxAccountState)
    : list (N × evm.program) :=
    fold_right (fun kv acc ⇒
      let '(_, (_, aps)) := kv in
      match code_entry_of_assumed aps with
      | Some kv' ⇒ kv' :: acc
      | None ⇒ acc
      end) [] m.

  Definition IncarnationR (q:Qp) (i: Indices): Rep.

  #[global] Instance observe_IncarnationR_type_ptr q idx :
    Observe (type_ptrR (Tnamed "monad::Incarnation"%cpp_name))
      (IncarnationR q idx).

  Definition observe_IncarnationR_type_ptr_F :=
    ltac:(mk_at_obs_fwd observe_IncarnationR_type_ptr).

  Definition AccountSubstateR
             (q: stdpp.numbers.Qp)
             (m: AccountSubstateModel)
    : skylabs.lang.cpp.logic.rep_defs.Rep :=
    _field "AccountSubstate::destructed_" |-> boolR (cQp.mut q) m.(asm_destructed)
    ** _field "AccountSubstate::touched_" |-> boolR (cQp.mut q) m.(asm_touched)
    ** _field "AccountSubstate::accessed_" |-> boolR (cQp.mut q) m.(asm_accessed)
    ** _field "AccountSubstate::accessed_storage_" |-> AccessedKeysR q m.(asm_accessed_keys)
    ** structR "monad::AccountSubstate"%cpp_name (cQp.mut q).

  Definition AccountR
             (q: stdpp.numbers.Qp)
             (ac: AccountM) : Rep :=
    let ba := coreAc ac in
    [| ac.(balance) = w256_to_N ba.(monad.EVMOpSem.block.block_account_balance) |]
    ** _field "monad::Account::balance" |-> u256R q (w256_to_N ba.(monad.EVMOpSem.block.block_account_balance))
    ** _field "monad::Account::code_hash" |-> bytes32R q (code_hash_of_program ba.(monad.EVMOpSem.block.block_account_code))
    ** _field "monad::Account::nonce" |-> primR "unsigned long" (cQp.mut q) (w256_to_Z ba.(monad.EVMOpSem.block.block_account_nonce))
    ** _field "monad::Account::incarnation"|-> IncarnationR q (incarnation ac)
    ** structR "monad::Account"%cpp_name (cQp.mut q).

  Definition addressR (q: Qp) (a: evm.address): Rep.
  Definition optionAddressR (q:Qp) (oaddr: option evm.address): Rep :=
    optional_specs.optionR "evmc::address" (fun a ⇒ addressR q a) q oaddr.

  Definition bytes32_to_w256 (n : N) : keccak.w256 :=
    Z_to_w256 (Z.of_N n).

  Definition account_storage_value (ac : AccountM) (key : N) : N :=
    w256_to_N
      (block.block_account_storage (coreAc ac) (bytes32_to_w256 key)).

  Definition storageMapOf (p : option AccountM) : list (N × N) :=
    match p with
    | Some ac ⇒ map (fun key ⇒ (key, account_storage_value ac key))
                   (relevantKeys ac)
    | None ⇒ []
    end.

  Definition AccountStateRcore (q: Qp) (origp: option AccountM) : Rep :=
    (_field "monad::AccountState::account_"
         |-> optional_specs.optionR
              "monad::Account"%cpp_type
              (fun ba ⇒ AccountR q ba)
              q
              origp
    ** _field "monad::AccountState::storage_"
              |-> StorageMapR q (storageMapOf origp)
   ** (Exists transient_map, _field "monad::AccountState::transient_storage_"
                                          |-> StorageMapR q transient_map)
    ** structR "monad::AccountState"%cpp_name (cQp.mut q)).

  Definition unusedAccountSubstate : AccountSubstateModel :=
    {| asm_destructed := false; asm_touched := false; asm_accessed := false; asm_accessed_keys := [] |}.

  Definition OriginalAccountStateR
    (q: Qp)
    (os: AssumedPreTxAccountState) : Rep :=
    let asm := assumExactness os in
    structR "monad::OriginalAccountState"%cpp_name (cQp.mut q)
    ** (o_base CU "monad::OriginalAccountState" "monad::AccountState" |->
          (_field "monad::AccountState::account_"
             |-> optional_specs.optionR
                  "monad::Account"%cpp_type
                  (fun ba ⇒ AccountR q ba)
                  q
                  (preTxState os)
           ** _field "monad::AccountState::storage_"
             |-> StorageMapR q (preTxStorage os)
           ** (Exists transient_map,
                _field "monad::AccountState::transient_storage_"
                  |-> StorageMapR q transient_map)
           ** structR "monad::AccountState"%cpp_name (cQp.mut q)))

    
    ** _field "monad::OriginalAccountState::validate_exact_balance_" |-> boolR (cQp.mut q)
                                                                    (~~
                                                                       (bool_decide (is_Some (min_balance asm))))
    
    ** _field "monad::OriginalAccountState::min_balance_" |->
        match min_balance asm with
        | Some n ⇒ u256R q n
        | None ⇒
           Exists (nb: N), u256R q nb
        end
        ** (o_base CU "monad::OriginalAccountState" "monad::AccountState" |->
              _base "monad::AccountState"%cpp_name "monad::AccountSubstate"%cpp_name
                           |-> AccountSubstateR q unusedAccountSubstate)
    .

  Definition UpdatedAccountStateR
    (q: Qp)
    (os: UpdatedAccountState) : Rep :=
    AccountStateRcore q (postTxState os) **
      _base "monad::AccountState"%cpp_name "monad::AccountSubstate"%cpp_name
      |-> AccountSubstateR q (substateModel os).

  Definition accountStorageDelta (beforeafter: evm.storage × evm.storage) : list (N × (N × N)).

  Definition pairMap {A B:Type} (f: A → B) (p : A×A) : B×B := (f (fst p), f (snd p)).


  Definition StateDeltaR (q:Qp) (beforeaft: AccountM × AccountM) : Rep :=
    _field "monad::StateDelta::account" |-> DeltaR "monad::Account" AccountR q beforeaft
    ** _field "monad::StateDelta::storage"
      |-> OneTbbMap.Rauth
           "::evmc::bytes32"
           (Tnamed (Ninst "monad::Delta" [Atype "::evmc::bytes32"]))
           (fun x:N ⇒ x)
           bytes32R
           (DeltaR "::evmc::bytes32" bytes32R)
           q
           (accountStorageDelta
              (pairMap (fun x ⇒ (block.block_account_storage (coreAc x))) beforeaft))
    ** structR "monad::StateDelta" q.


  Definition globalDelta (beforeAfter: evm.GlobalState × evm.GlobalState) : list (evm.address × (AccountM × AccountM)).

  Definition StateDeltasR (q:Qp) (beforeAfter: evm.GlobalState × evm.GlobalState) : Rep :=
    OneTbbMap.Rauth
      "evmc::address"
      "monad::StateDelta"
      (fun a ⇒ a)
      addressR
      StateDeltaR
      q
      (globalDelta beforeAfter).

  Definition CodeDeltaR (q:Qp) (beforeAfter: evm.GlobalState × evm.GlobalState) : Rep.
End with_Sigma.
#[global] Hint Resolve
  observe_IncarnationR_type_ptr_F : sl_opacity.
 Definition CodeHash := N.
 Module BlockState. Section with_Sigma.
  Context `{Sigma:cpp_logic} {CU: genv} {hh: HasOwn mpredI fracR}.
  Context (blockPreState: AugmentedState).

  Record glocs :=
    {
      cmap: gname;
    }.

  Notation Code := evm.program.

  Definition fullCodeMap (newState: AugmentedState): gmap CodeHash Code.

  Definition Rauth (g: glocs) (newState: AugmentedState): Rep.

  Definition Rfrag (q:Qp) (g: glocs): Rep.

  Definition CodeMapContainsEntries (g: glocs) (entries: gmap CodeHash Code) : Rep.

  Definition CodeMapContainsKeys (g: glocs) (keys: list CodeHash) : Rep.

  Lemma split_frag {T} q g (l : list T):
    Rfrag q g -|- Rfrag (q/(N_to_Qp (1+ lengthN l))) g **
    ([∗ list] _ ∈ l, (Rfrag (q×/(N_to_Qp (1+ lengthN l))) g)).

  Lemma split_frag_loopinv {T} q g (l : list T) (i:nat) (prf: i=0):
    Rfrag q g -|- Rfrag (q/(N_to_Qp (1+ lengthN l))) g**
    ([∗ list] _ ∈ (drop i l), (Rfrag (q×/(N_to_Qp (1+ lengthN l))) g)).

  Lemma code_map_lb (q:Qp) (g: glocs) (codeMapLb: gmap CodeHash Code) currentState:
    Observe [| codeMapLb ⊆ fullCodeMap currentState |]
      (CodeMapContainsEntries g codeMapLb ** Rauth g currentState).

  Lemma code_map_lb2 (q:Qp) (g: glocs) (keys: list CodeHash) currentState:
    Observe [| keys ⊆ map fst (map_to_list (fullCodeMap currentState)) |]
      (CodeMapContainsKeys g keys ** Rauth g currentState).

  Lemma duplicableCodeMapEntries (q:Qp) (g: glocs) (codeMapLb: gmap CodeHash Code):
    CodeMapContainsEntries g codeMapLb |-- CodeMapContainsEntries g codeMapLb ** CodeMapContainsEntries g codeMapLb.

  Lemma codeMapWeaken (q:Qp) (g: glocs) (codeMapLb1 codeMapLb2: gmap CodeHash Code):
    codeMapLb2 ⊆ codeMapLb1
    → CodeMapContainsEntries g codeMapLb1 |-- CodeMapContainsEntries g codeMapLb2.


End with_Sigma. End BlockState.

Record StateM :=
  {
    relaxedValidation: bool;
    preTxAssumedState: MapModel evm.address AssumedPreTxAccountState;
    newStates: MapModel evm.address (list (ptr×UpdatedAccountState));
    blockStatePtr: ptr;
    indices: Indices;
    blockStateGloc: BlockState.glocs;
    dbBlockStateCodeMapLb : gmap CodeHash evm.program;
    codeMap : gmap CodeHash evm.program;
  }.

Definition update_assum_exactness_state_at
           (st: StateM)
           (addr: evm.address)
           (f: AssumptionExactness → AssumptionExactness) : StateM :=
  {| relaxedValidation := relaxedValidation st;
     preTxAssumedState := update_assum_exactness_at addr f (preTxAssumedState st);
     newStates := newStates st;
     blockStatePtr := blockStatePtr st;
    indices := indices st;
    blockStateGloc := blockStateGloc st;
    dbBlockStateCodeMapLb := dbBlockStateCodeMapLb st;
    codeMap := codeMap st;
  |}.


Section with_Sigma.
  Context `{Sigma:cpp_logic} {CU: genv} {hh: HasOwn mpredI fracR}.

  Definition ChainR (q: Qp) (c: Chain): Rep.

  Lemma ChainR_split_loopinv {T} q (b: Chain) (l : list T) (i:nat) (p:i=0):
    ChainR q b -|- ChainR (q/(N_to_Qp (1+ lengthN l))) b **
    ([∗ list] _ ∈ (drop i l), (ChainR (q×/(N_to_Qp (1+ lengthN l))) b)).

  Definition tx_nonce tx :=
    (w256_to_N (block.tr_nonce tx)).
  Definition tx_gas_limit tx :=
    (w256_to_N (block.tr_gas_limit tx)).
  Definition TransactionR (q:Qp) (tx: Transaction) : Rep :=
    structR "monad::Transaction" q **
      _field "monad::Transaction::nonce" |-> ulongR q (tx_nonce tx.1) **
      o_field CU "monad::Transaction::gas_limit" |-> ulongR q (tx_gas_limit tx.1).

  #[global] Instance learnTrRbase: LearnEq2 TransactionR:= ltac:(solve_learnable).

  Definition BheaderR (q:Qp) (hdr: BlockHeader) : Rep :=
    structR "monad::BlockHeader" q
    ** _field "monad::BlockHeader::base_fee_per_gas" |-> optional_specs.optionR u256t (u256R q) q (base_fee_per_gas hdr)
    ** _field "monad::BlockHeader::number" |-> ulongR q (number hdr)
    ** _field "monad::BlockHeader::beneficiary"
         |-> addressR 1 (beneficiary hdr)
    ** _field "monad::BlockHeader::timestamp" |-> primR "unsigned long" q (timestamp hdr).

  Definition BlockR (q: Qp) (c: Block): Rep :=
    _field "::monad::Block::transactions" |-> VectorR (Tnamed "::monad::Transaction") (fun t ⇒ TransactionR q t) q (transactions c)
    ** _field "::monad::Block::header" |-> BheaderR q (header c)
      ** structR "::monad::Block" q.

  Record History {T:Type} : Type :=
    { currentBlock: T;
      parentBlock: option T;
      grandParentBlock: option T }.

  Record MonadChainContext : Type :=
    { senders_and_authoritiesp: History ptr;
      blocks: History Block;
      sendersp: ptr;
      authsp: ptr }.

  Definition sendersAndAuthorities (b: Block): list EvmAddr :=
    map sender (txsWithHdr b) ++
    flat_map
      (fun tx ⇒
         flat_map
           (fun oa ⇒
              match oa with
              | Some addr ⇒ [addr]
              | None ⇒ []
              end)
           (map del_from (authorities (tx.2))))
      (transactions b).
  Definition addressToN (a: evm.address) : N.
  Definition address_set_table_ty : type :=
    ankerl_specs.anker_set_table_ty "evmc::address".

  #[global] Instance evmaddr : concepts.BundledRep "evmc::address" EvmAddr.

  #[global] Instance optionalrep (bty: type) (bT: Type)
    {cb: concepts.BundledRep bty bT} :
    concepts.BundledRep (Tnamed ("std::optional".<<Atype bty>>)) (option bT).

  Notation stdvector ty := (std.vector.T ty (std.allocator.T ty)).

  #[global] Instance vectorrep (bty: type) (bT: Type)
    {cb: concepts.BundledRep bty bT} :
    concepts.BundledRep (stdvector bty) (list bT).

  Definition txAuthoritiesDelFrom (t: Transaction) : list (option EvmAddr) :=
    map del_from (authorities (t.2)).

  Definition SenderAuthoritiesSetR (q: Qp) (addrs: list EvmAddr) : Rep :=
    ankerl_specs.AnkerSetR "evmc::address" addressToN addressR q addrs.

  Definition ptr_of_option (op : option ptr) : ptr :=
    match op with
    | Some p ⇒ p
    | None ⇒ nullptr
    end.

  Definition MonadChainContextR (q: Qp) (m: MonadChainContext) : Rep :=
    let curblock := currentBlock (blocks m) in
    let cursetp := currentBlock (senders_and_authoritiesp m) in
    let parentsetpo := parentBlock (senders_and_authoritiesp m) in
    let grandparentsetpo := grandParentBlock (senders_and_authoritiesp m) in
    structR "monad::MonadChainContext" (cQp.mut q)
      ** _field "monad::MonadChainContext::grandparent_senders_and_authorities" |->
           primR
             (Tptr address_set_table_ty)
             (cQp.m q) (Vptr (ptr_of_option grandparentsetpo))
      ** (match grandparentsetpo, grandParentBlock (blocks m) with
          | None, None ⇒ [| (number (header curblock) ≤ 2)%N |]
          | Some grandparentsetp, Some grandparentblock ⇒
              ([| (2 < number (header curblock))%N |]
               ** [| grandparentsetp ≠ nullptr |]
               ** pureR (grandparentsetp |-> SenderAuthoritiesSetR (cQp.m q)
                                (sendersAndAuthorities grandparentblock)))
          | _, _ ⇒ pureR False
          end)
      ** _field "monad::MonadChainContext::parent_senders_and_authorities" |->
           primR
             (Tptr address_set_table_ty)
             (cQp.m q) (Vptr (ptr_of_option parentsetpo))
      ** (match parentsetpo, parentBlock (blocks m) with
          | None, None ⇒ [| (number (header curblock) ≤ 1)%N |]
          | Some parentsetp, Some parentblock ⇒
              ([| (1 < number (header curblock))%N |]
               ** [| parentsetp ≠ nullptr |]
               ** pureR (parentsetp |-> SenderAuthoritiesSetR (cQp.m q)
                                (sendersAndAuthorities parentblock)))
          | _, _ ⇒ pureR False
          end)
      ** _field "monad::MonadChainContext::senders_and_authorities" |->
           primR
             (Tref address_set_table_ty)
             (cQp.m q) (Vptr cursetp)
      ** pureR (cursetp |-> SenderAuthoritiesSetR (cQp.m q)
                    (sendersAndAuthorities curblock))
      ** _field "monad::MonadChainContext::senders" |->
          primR (Tref (stdvector "evmc::address")) (cQp.m q) (Vptr (sendersp m))
      ** pureR ((sendersp m) |-> std.vector.R "evmc::address" (cQp.m q) (map sender (txsWithHdr curblock)))
      ** _field "monad::MonadChainContext::authorities" |->
          primR (Tref (stdvector (stdvector "std::optional<evmc::address>"))) (cQp.m q) (Vptr (authsp m))
      ** pureR ((authsp m) |-> std.vector.R (stdvector "std::optional<evmc::address>") (cQp.m q)
                 (map txAuthoritiesDelFrom (transactions curblock))).

  Definition wei_per_mon : N := 1000000000000000000%N.
  Definition DefReserve : N := (10 × wei_per_mon)%N.

  Definition sender_in_block (b: Block) (addr : EvmAddr) : Prop :=
    addr ∈ map sender (txsWithHdr b).

  Definition authority_in_block (b: Block) (addr : EvmAddr) : Prop :=
    Some addr ∈ flat_map txAuthoritiesDelFrom (transactions b).

  Definition sender_in_recent_history
      (ctx : MonadChainContext) (tx : TxWithHdr) : Prop :=
    (match parentBlock (blocks ctx) with
     | Some parent ⇒ sender_in_block parent (sender tx)
     | None ⇒ False
     end) ∨
    (match grandParentBlock (blocks ctx) with
     | Some grandparent ⇒ sender_in_block grandparent (sender tx)
     | None ⇒ False
     end).

  Definition delundel_in_recent_history
      (ctx : MonadChainContext) (tx : TxWithHdr) : Prop :=
    (match parentBlock (blocks ctx) with
     | Some parent ⇒ authority_in_block parent (sender tx)
     | None ⇒ False
     end) ∨
    (match grandParentBlock (blocks ctx) with
     | Some grandparent ⇒ authority_in_block grandparent (sender tx)
     | None ⇒ False
     end).

  Definition sender_in_recent_historyb
      (ctx : MonadChainContext) (tx : TxWithHdr) : bool :=
    match parentBlock (blocks ctx), grandParentBlock (blocks ctx) with
    | Some parent, Some grandparent ⇒
        asbool (sender tx ∈ map sender (txsWithHdr parent)) ||
        asbool (sender tx ∈ map sender (txsWithHdr grandparent))
    | Some parent, None ⇒
        asbool (sender tx ∈ map sender (txsWithHdr parent))
    | None, Some grandparent ⇒
        asbool (sender tx ∈ map sender (txsWithHdr grandparent))
    | None, None ⇒ false
    end.

  Definition delundel_in_recent_historyb
      (ctx : MonadChainContext) (tx : TxWithHdr) : bool :=
    match parentBlock (blocks ctx), grandParentBlock (blocks ctx) with
    | Some parent, Some grandparent ⇒
        asbool (Some (sender tx) ∈ flat_map txAuthoritiesDelFrom (transactions parent)) ||
        asbool (Some (sender tx) ∈ flat_map txAuthoritiesDelFrom (transactions grandparent))
    | Some parent, None ⇒
        asbool (Some (sender tx) ∈ flat_map txAuthoritiesDelFrom (transactions parent))
    | None, Some grandparent ⇒
        asbool (Some (sender tx) ∈ flat_map txAuthoritiesDelFrom (transactions grandparent))
    | None, None ⇒ false
    end.

  Definition sender_in_current_prefixb
      (ctx : MonadChainContext) (i : nat) (tx : TxWithHdr) : bool :=
    existsb
      (fun j ⇒
         bool_decide
           (nth_error (map sender (txsWithHdr (currentBlock (blocks ctx)))) j =
            Some (sender tx)))
      (seq 0 i).

  Definition delundel_in_current_prefixb
      (ctx : MonadChainContext) (i : nat) (tx : TxWithHdr) : bool :=
    existsb
      (fun j ⇒
         match nth_error
                 (map txAuthoritiesDelFrom (transactions (currentBlock (blocks ctx)))) j
         with
         | Some auths ⇒ bool_decide (Some (sender tx) ∈ auths)
         | None ⇒ false
         end)
      (seq 0 i).

  Definition tx_seen_within_k (e : ExtraAcStates) (tx : TxWithHdr) : bool :=
    let startIndex := (txBlockNum tx - 2)%N in
    match lastTxInBlockIndex (e (sender tx)) with
    | Some index ⇒ asbool ((startIndex ≤ index)%N ∧ (index ≤ txBlockNum tx)%N)
    | None ⇒ false
    end.

  Definition delundel_seen_within_k (e : ExtraAcStates) (tx : TxWithHdr) : bool :=
    let startIndex := (txBlockNum tx - 2)%N in
    match lastDelUndelInBlockIndex (e (sender tx)) with
    | Some index ⇒ asbool ((startIndex ≤ index)%N ∧ (index ≤ txBlockNum tx)%N)
    | None ⇒ false
    end.

  Definition historyConsistent (c: MonadChainContext) (e: ExtraAcStates) : Prop :=
    ∀ i tx,
      nth_error (txsWithHdr (currentBlock (blocks c))) i = Some tx →
      tx_seen_within_k e tx =
        (sender_in_recent_historyb c tx || sender_in_current_prefixb c i tx)
      ∧
      delundel_seen_within_k e tx =
        (delundel_in_recent_historyb c tx || delundel_in_current_prefixb c i tx).
  #[global] Opaque sender_in_block authority_in_block.
  #[global] Opaque sender_in_recent_history delundel_in_recent_history.
  #[global] Opaque sender_in_recent_historyb delundel_in_recent_historyb.
  #[global] Opaque sender_in_current_prefixb delundel_in_current_prefixb.
  #[global] Opaque tx_seen_within_k delundel_seen_within_k.
  #[global] Opaque historyConsistent.

  Definition cblock (b: MonadChainContext) : Block := currentBlock (blocks b).

  Definition ResultSuccessR {T} (trep: T → Rep) (t:T): Rep.
  Definition ReceiptR (t: TxResult): Rep.
  Definition EvmcResultR (t: TxResult): Rep.
  Definition ResultFailureR: Rep.

  Definition valOfRev (r : Revision) : val := Vint 0.   Definition gas_price_model (rev: Z) (tx: Transaction) (base_fee_per_gas: N) : N :=
    gas_price_cpp_model tx base_fee_per_gas.

  Definition validTx (tx: TxWithHdr) : Prop :=
    (tx_nonce tx.1.1 < 2 ^ 64 - 1)%N ∧
    (tx_gas_limit tx.1.1 < 2 ^ 64)%N ∧
    (gas_price_cpp_model tx.1 (tx_base_fee_per_gas tx) < 2 ^ 128)%N ∧
    maxTxFee tx =
      (tx_gas_limit tx.1.1 × gas_price_cpp_model tx.1 (tx_base_fee_per_gas tx))%N.

  Record BlockHashBuffer :=
    { fullHistory: list N;
      startIndex: N}.

  Definition lastIndex (b: BlockHashBuffer) : N := startIndex b + lengthN (fullHistory b).

  Definition BlockHashBufferR (q:Qp) (m: BlockHashBuffer) : Rep :=
    _field "monad::n_" |-> u64R q (lastIndex m).
  Lemma bhb_split_sn {T} q (b: BlockHashBuffer) (l : list T):
    BlockHashBufferR q b -|- BlockHashBufferR (q/(N_to_Qp (1+ lengthN l))) b **
    ([∗ list] _ ∈ l, (BlockHashBufferR (q×/(N_to_Qp (1+ lengthN l))) b)).

  Lemma bhb_splitl_loopinv {T} q (b: BlockHashBuffer) (l : list T) (i:nat) (p:i=0):
    BlockHashBufferR q b -|- BlockHashBufferR (q/(N_to_Qp (1+ lengthN l))) b **
    ([∗ list] _ ∈ (drop i l), (BlockHashBufferR (q×/(N_to_Qp (1+ lengthN l))) b)).

  Lemma header_split_loopinv {T} q (b: BlockHeader) (l : list T) (i:nat) (p:i=0):
    BheaderR q b -|- BheaderR (q/(N_to_Qp (1+ lengthN l))) b **
    ([∗ list] _ ∈ (drop i l), (BheaderR (q×/(N_to_Qp (1+ lengthN l))) b)).



Context {MODd : exb.module ⊧ CU}.

  Definition txAuthoritires (t: Transaction) : list EIP7702Authority := authorities (t.2).

  Definition AuthoritiesR q (auths: list EIP7702Authority) : Rep :=
    VectorR "std::optional<evmc::address>" (fun oa ⇒ optional_specs.optionR "evmc::address" (addressR q) q oa) q (map del_from auths).

  Definition BlockMetricsR : Rep.

  Definition dummyCallTracerR (t: Transaction) : Rep.
  Definition dummyStateTracerR (t: Transaction) : Rep.






Definition resultT := Tnamed (resultn "monad::ExecutionResult").
Definition ExecutionResultR (tr: TxResult): Rep.

Definition oResultT := (Tnamed (Ninst "std::optional" [Atype resultT])).








Definition txIndex (t: TxWithHdr) : N := indexInBlock t.1.2.

  Definition execute_transaction_spec : WpSpec mpredI val val :=
    \arg{chainp :ptr} "chain" (Vref chainp)
    \prepost{(qchain:Qp) (chain: Chain)} chainp |-> ChainR qchain chain
    \arg{(tx:TxWithHdr)} "i" (Vn (txIndex tx))
    \pre [| (txIndex tx) < 2^64 - 1 |]%N
    \arg{txp} "tx" (Vref txp)
    \prepost{qtx t} txp |-> TransactionR qtx t.1
    \arg{senderp} "sender" (Vref senderp)
    \prepost{qs} senderp |-> addressR qs (sender t)
    \arg{hdrp: ptr} "hdr" (Vref hdrp)
    \prepost{qh} hdrp |-> BheaderR qh t.2
    \arg{block_hash_bufferp: ptr} "block_hash_buffer" (Vref block_hash_bufferp)
    \arg{block_statep: ptr} "block_state" (Vref block_statep)
    \prepost{g qf preBlockState} block_statep |-> BlockState.Rfrag preBlockState qf g
    \arg{prevp: ptr} "prev" (Vref prevp)
    \pre{(prg: gname) (prevTxGlobalState: AugmentedState) (OtherPromisedResources:mpred)}
        prevp |-> PromiseConsumerR prg (OtherPromisedResources ** block_statep |-> BlockState.Rauth preBlockState g prevTxGlobalState)
    \post{retp}[Vptr retp] OtherPromisedResources ** prevp |-> PromiseUnusableR **
    match execTx prevTxGlobalState t with
    | Some (finalState, result)
      ⇒
        retp |-> ResultSuccessR ExecutionResultR result
          ** block_statep |-> BlockState.Rauth preBlockState g finalState
    | None ⇒ retp |-> ResultFailureR
               ** Exists garbage, block_statep |-> BlockState.Rauth preBlockState g garbage

    end.


Definition destr_res {T} ty (tyR: T→ Rep):=
λ {thread_info : biIndex} {_Σ : gFunctors} {Sigma : cpp_logic thread_info _Σ} {CU : genv},
  specify
    {|
      info_name :=
        Nscoped
          (resultn ty)
          (Ndtor);
      info_type :=
        tDtor
          (resultn ty)
    |} (λ this : ptr, \pre{res} this |-> ResultSuccessR tyR res
                        \post emp).
#[global] Instance : LearnEq2 ChainR:= ltac:(solve_learnable).
#[global] Instance : LearnEq4 BlockState.Rfrag := ltac:(solve_learnable).
#[global] Instance : LearnEq2 BheaderR := ltac:(solve_learnable).
#[global] Instance rrr {T}: LearnEq2 (@ResultSuccessR T) := ltac:(solve_learnable).

End with_Sigma.

#[global] Hint Unfold MonadChainContextR : unfold.

Section with_Sigma.
  Context `{Sigma:cpp_logic} {CU: genv} {hh: HasOwn mpredI fracR}.
  Context {hf: fracG () _Σ}.
  Context {MODd : ext.module ⊧ CU}.



Let MapOriginalR
           (q: stdpp.numbers.Qp)
           (m: MapModel
                  evm.address
                  AssumedPreTxAccountState)
  : Rep :=
  AnkerMapR "evmc::address" "monad::OriginalAccountState"
           addressToN
           addressR
           OriginalAccountStateR
           q
           m.

Definition VersionStack_ty (cppType : type) : type :=
  Tnamed ("monad::VersionStack".<< Atype cppType >>)%cpp_name.

Definition VersionStackSpineR (cppType: type) (q:Qp) (lt:list ptr): Rep.

Definition VersionStackR {ElemType} (cppType: type) (elemRep: Qp → ElemType → Rep) (q:Qp) (lt:list (ptr×ElemType)): Rep :=
  VersionStackSpineR cppType q (map fst lt) ** pureR ([∗ list] p ∈ lt, let '(loc, val) := p in (loc:ptr) |-> elemRep q val).

Let MapCurrentR
           (q: stdpp.numbers.Qp)
           (m: MapModel address (list (ptr× UpdatedAccountState)))
  : Rep :=
  AnkerMapR "evmc::address" "monad::VersionStack<monad::AccountState>"
           addressToN
           addressR
           (VersionStackR "monad::AccountState" UpdatedAccountStateR)
           q
           m.

Definition StateDirtyStackR (q : Qp) (dirty : list (list evm.address)) : Rep :=
  Exists elts : list (ptr × list evm.address),
    [| map snd elts = dirty |]
    ** deque_specs.DequeR address_set_table_ty (std.allocator.T address_set_table_ty)
         SenderAuthoritiesSetR q elts.


Definition AnkerMapSliceR {K V:Type} `{EqDecision K} (tykey tyval: type) (khash: K → N)
           (krep : Qp → K → Rep)
           (vrep : Qp → V → Rep)
           
           (qspine: Qp)
           (key: K)
           (val:V)
           map
           
  : Rep := AnkerMapSpineR tykey tyval khash krep qspine map
             ** Exists (i:N),
    match nth_error map (N.to_nat i) with
    | Some (k, loc) ⇒ [| k= key |]
                            ** pureR (loc ,, pairSndOffset tykey tyval |-> vrep 1%Qp val)
    | None ⇒ False
    end.

Definition LogsR (q: stdpp.numbers.Qp) : Rep :=
  structR
    "monad::VersionStack<std::vector<monad::Receipt::Log, std::allocator<monad::Receipt::Log>>>"
    (cQp.mut q).

Definition CodeMapR
           (q: stdpp.numbers.Qp)
           (cm: stdpp.gmap.gmap Corelib.Numbers.BinNums.N
                             evm.program)
  : Rep.

Definition isNone {T} (a: option T) := negb (isSome a).

Definition min_balanceN (a: AssumptionExactness) : N :=
  match min_balance a with
  | Some f ⇒ f
  | None ⇒ 0
  end.

Global Instance lkk {K V} `{Countable K} :
  Lookup K (ModelWithPtr V) (MapModel K V) :=
  fun k m ⇒ ((list_to_map m : gmap K (ModelWithPtr V)) !! k).

Definition mapModelLookup {K V} `{Countable K} (m: MapModel K V) (k: K)
  : option (ModelWithPtr V) :=
  ((list_to_map m : gmap K (ModelWithPtr V)) !! k).

Definition initial_assumption_exactness : AssumptionExactness :=
  {| min_balance := Some 0%N; nonce_exact := false |}.

Definition initial_original_account_state
    (acct: option AccountM) : AssumedPreTxAccountState :=
  {| preTxState := acct;
     preTxStorage := storageMapOf acct;
     assumExactness := initial_assumption_exactness |}.

Definition initial_updated_account_state
    (orig: AssumedPreTxAccountState) : UpdatedAccountState :=
  {| postTxState := preTxState orig;
     substateModel := unusedAccountSubstate |}.

Definition state_original_account_state_post
    (orig: MapModel evm.address AssumedPreTxAccountState)
    (addr: evm.address)
    (orig_final: MapModel evm.address AssumedPreTxAccountState)
    (loc: ptr)
    (orig_state: AssumedPreTxAccountState) : Prop :=
  match mapModelLookup orig addr with
  | Some (old_loc, old_state) ⇒
      orig_final = orig ∧ loc = old_loc ∧ orig_state = old_state
  | None ⇒
      ∃ acct : option AccountM,
        orig_state = initial_original_account_state acct
        ∧ orig_final = (addr, (loc, orig_state)) :: orig
  end.

Definition assumptionOfAddr (s: MapModel evm.address AssumedPreTxAccountState) (a: evm.address)
  : option AssumedPreTxAccountState :=
  match s !! a with
  | None ⇒ None
  | Some p ⇒
          Some (snd p)
  end.

Definition assumptionAndUpdateOfAddr (s: StateM) (a: evm.address)
  : option TxAssumptionsAndUpdates :=
  match preTxAssumedState s !! a with
  | None ⇒ None
  | Some p ⇒
      Some
        {|
          preAssumption := snd p;
          originalLoc := fst p;
          txUpdates :=
            ((newStates s) !! a) ≫=
              (fun a ⇒
                 match head (snd a) with
                 | None ⇒ None
                 | Some (loc, upd) ⇒ Some (fst a, (loc, upd))
                 end)
        |}
  end.

Definition validAU (relaxedValidation: bool) (a: option TxAssumptionsAndUpdates)
  : Prop :=
  match option_map preAssumption a with
  | None ⇒ True
  | Some assumedPreState ⇒
      let assumEx := assumExactness assumedPreState in
      match preTxState assumedPreState with
      | None ⇒ True
      | Some cs ⇒
          if isSome (min_balance assumEx)
          then (min_balanceN assumEx ≤ cs .^ _balance)%N
          else True
      end
  end.

Definition validStateM (a: StateM) : Prop :=
  ∀ addr,
    validAU (relaxedValidation a) (assumptionAndUpdateOfAddr a addr).

Definition nonEmptyPostStackAndPostNoneImpliesAssumedPreNone (s: StateM) : Prop :=
  ∀ addr loc tl loc0 aps,
    mapModelLookup (newStates s) addr = Some (loc, tl) →
    mapModelLookup (preTxAssumedState s) addr = Some (loc0, aps) →
    match tl with
    | [] ⇒ False
    | (_, upd) :: _ ⇒ postTxState upd = None → preTxState aps = None
    end.

Definition validPostNone (s: StateM) : Prop :=
  nonEmptyPostStackAndPostNoneImpliesAssumedPreNone s.

Definition validModel s : Prop :=
  map fst (newStates s) ⊆ map fst (preTxAssumedState s)
  ∧ validStateM s
  ∧ validPostNone s.

Definition ldom {K V} {eqd: EqDecision K} {c: Countable K} (g: gmap K V) := map fst (map_to_list g).

Definition codeMapOfNewStates
  (s : StateM)
  : gmap N evm.program :=
  list_to_map (code_entries_of_state (newStates s)).

Definition codeMapOfPreTxAssumedAccounts
  (s : StateM)
  : gmap N evm.program :=
  list_to_map (code_entries_of_preTxAssumed (preTxAssumedState s)).

Definition consistentMaps (maps: list (gmap N evm.program)) : Prop.

Definition code_entries_functional (l: list (N × evm.program)) : Prop :=
  ∀ (h: N) (c1 c2: evm.program),
    (h, c1) ∈ l → (h, c2) ∈ l → c1 = c2.

Definition code_entries_nonzero (l: list (N × evm.program)) : Prop :=
  ∀ (h: N) (c: evm.program),
    (h, c) ∈ l → h = 0%N → monad.EVMOpSem.evm.program_length c = 0%Z.

Definition all_code_entries (s : StateM) : list (N × evm.program) :=
  code_entries_of_state (newStates s)
  ++ map_to_list (codeMap s)
  ++ map_to_list (dbBlockStateCodeMapLb s)
  ++ map_to_list (codeMapOfPreTxAssumedAccounts s).

Definition stateCodeMapInvariants s :=
  ldom (codeMapOfNewStates s) ⊆ ldom (dbBlockStateCodeMapLb s) ++ ldom (codeMap s)
  ∧ (consistentMaps [codeMap s; (dbBlockStateCodeMapLb s); codeMapOfNewStates s; codeMapOfPreTxAssumedAccounts s])
  ∧ (codeMapOfPreTxAssumedAccounts s ⊆ (dbBlockStateCodeMapLb s))
  ∧ code_entries_functional (all_code_entries s)
  ∧ code_entries_nonzero (all_code_entries s).

Definition StateCodeMapR (s: StateM) : Rep :=
    _field "monad::State::code_" |-> CodeMapR 1$m%cQp (codeMap s)
    ** BlockState.CodeMapContainsEntries (blockStateGloc s) (dbBlockStateCodeMapLb s)
    ** [| stateCodeMapInvariants s |].

Definition StateOriginalR
    (orig: MapModel evm.address AssumedPreTxAccountState) : Rep :=
  _field "monad::State::original_" |-> MapOriginalR 1$m%cQp orig.

  Definition StateR (s: StateM) : Rep := Eval unfold MapOriginalR, MapCurrentR in (
   _field "monad::State::block_state_" |-> refR<"monad::BlockState"> 1$m (blockStatePtr s) ∗
   _field "monad::State::incarnation_" |-> IncarnationR 1$m%cQp (indices s) ∗
   _field "monad::State::original_" |-> MapOriginalR 1$m%cQp (preTxAssumedState s) ∗
   _field "monad::State::current_" |-> MapCurrentR 1$m%cQp (newStates s) ∗
   _field "monad::State::logs_" |-> LogsR 1$m%cQp ∗
   _field "monad::State::version_" |-> uintR 1$m 0 ∗
   _field "monad::State::dirty_" |-> StateDirtyStackR 1$m%cQp [] ∗
   _field "monad::State::relaxed_validation_" |-> boolR 1$m (relaxedValidation s) ∗
   StateCodeMapR s **
   [| validModel s|] **
   structR "monad::State" 1$m).



  Definition preTxAccountOf (st: StateM) (addr: evm.address) : option AccountM :=
    mapModelLookup (preTxAssumedState st) addr ≫= (fun p ⇒ preTxState (snd p)).

  Definition preTxAccountOf_map
      (orig: MapModel evm.address AssumedPreTxAccountState)
      (addr: evm.address) : option AccountM :=
    mapModelLookup orig addr ≫= (fun p ⇒ preTxState (snd p)).

  Definition recentAccountOf (st: StateM) (addr: evm.address) : option AccountM :=
    match mapModelLookup (newStates st) addr with
    | Some (_, updates) ⇒
        match head updates with
        | Some (_, upd) ⇒ postTxState upd
        | None ⇒ None
        end
    | None ⇒ preTxAccountOf st addr
    end.

  Definition state_with_preTxAssumedState
      (st : StateM)
      (orig : MapModel evm.address AssumedPreTxAccountState) : StateM :=
    {| relaxedValidation := relaxedValidation st;
       preTxAssumedState := orig;
       newStates := newStates st;
       blockStatePtr := blockStatePtr st;
       indices := indices st;
       blockStateGloc := blockStateGloc st;
       dbBlockStateCodeMapLb := dbBlockStateCodeMapLb st;
       codeMap := codeMap st |}.

  Definition state_with_preTxAssumedState_and_newStates
      (st : StateM)
      (orig : MapModel evm.address AssumedPreTxAccountState)
      (cur : MapModel evm.address (list (ptr × UpdatedAccountState))) : StateM :=
    {| relaxedValidation := relaxedValidation st;
       preTxAssumedState := orig;
       newStates := cur;
       blockStatePtr := blockStatePtr st;
       indices := indices st;
       blockStateGloc := blockStateGloc st;
       dbBlockStateCodeMapLb := dbBlockStateCodeMapLb st;
       codeMap := codeMap st |}.

  Definition state_original_account_state_block_stateR
      (this : ptr)
      (orig : MapModel evm.address AssumedPreTxAccountState)
      (addr : evm.address) : mpred :=
    match mapModelLookup orig addr with
    | Some _ ⇒ emp
    | None ⇒
        Exists (block_statep : ptr),
        Exists (preBlockState : AugmentedState),
        Exists (g : BlockState.glocs),
          Exists (qblock : Qp),
            this ,, o_field CU "monad::State::block_state_"
              |-> refR<"monad::BlockState"> 1$m block_statep
            ** block_statep |-> BlockState.Rfrag preBlockState qblock g
    end.

  Definition state_recent_account_state_post
      (st : StateM) (addr : evm.address)
      (st_final : StateM) (retp : ptr) (acct : option AccountM) : Prop :=
    match mapModelLookup (newStates st) addr with
    | Some (_, updates) ⇒
        ∃ upd_loc upd tl,
          updates = (upd_loc, upd) :: tl
          ∧ st_final = st
          ∧ retp = upd_loc
          ∧ acct = postTxState upd
    | None ⇒
        ∃ loc orig_final orig_state,
          state_original_account_state_post
            (preTxAssumedState st) addr orig_final loc orig_state
          ∧ st_final = state_with_preTxAssumedState st orig_final
          ∧ retp =
               loc ,, pairSndOffset "evmc::address" "monad::OriginalAccountState"
                   ,, o_base CU "monad::OriginalAccountState" "monad::AccountState"
          ∧ acct = preTxState orig_state
    end.


  Definition replace_current_head_update
      (upd : UpdatedAccountState)
      (updates : list (ptr × UpdatedAccountState))
      : list (ptr × UpdatedAccountState) :=
    match updates with
    | [] ⇒ []
    | (upd_loc, _) :: tl ⇒ (upd_loc, upd) :: tl
    end.

  Definition replace_current_account_update
      (addr : evm.address)
      (upd : UpdatedAccountState)
      (cur : MapModel evm.address (list (ptr × UpdatedAccountState)))
      : MapModel evm.address (list (ptr × UpdatedAccountState)) :=
    map (fun '(a, (loc, updates)) ⇒
           if bool_decide (a = addr)
           then (a, (loc, replace_current_head_update upd updates))
           else (a, (loc, updates))) cur.

  Definition state_update_current_account
      (st : StateM) (addr : evm.address) (upd : UpdatedAccountState)
      : StateM :=
    state_with_preTxAssumedState_and_newStates st (preTxAssumedState st)
      (replace_current_account_update addr upd (newStates st)).

  Definition state_current_account_state_post
      (st : StateM) (addr : evm.address)
      (st_final : StateM) (retp : ptr) (upd : UpdatedAccountState) : Prop :=
    match mapModelLookup (newStates st) addr with
    | Some (_, updates) ⇒
        match updates with
        | (upd_loc, upd0) :: _ ⇒
            st_final = st
            ∧ retp = upd_loc
            ∧ upd = upd0
        | [] ⇒ False
        end
    | None ⇒
        ∃ orig_loc orig_final orig_state cur_loc,
          state_original_account_state_post
            (preTxAssumedState st) addr orig_final orig_loc orig_state
          ∧ upd = initial_updated_account_state orig_state
          ∧ st_final =
               state_with_preTxAssumedState_and_newStates st orig_final
                 ((addr, (cur_loc, [(retp, upd)])) :: newStates st)
    end.


  Definition balanceOfAccount (oa: option AccountM) : N :=
    match oa with
    | Some ac ⇒ ac .^ _balance
    | None ⇒ 0%N
    end.

  Definition account_set_balance (ac : AccountM) (bal : N) : AccountM :=
    (ac &: _coreAc .@ _block_account_balance .= Z_to_w256 (Z.of_N bal))
       &: _balance .= bal.

  Lemma storageMapOf_account_set_balance (ac : AccountM) (bal : N) :
    storageMapOf (Some (account_set_balance ac bal)) =
    storageMapOf (Some ac).

  Definition account_substate_touch_model
      (m : AccountSubstateModel) : AccountSubstateModel :=
    {| asm_destructed := asm_destructed m;
       asm_touched := true;
       asm_accessed := asm_accessed m;
       asm_accessed_keys := asm_accessed_keys m |}.




  Definition optional_account_has_value_spec : mpred :=
    specify.template.method
      ("std::optional".<<Atype "monad::Account"%cpp_type>>)%cpp_name
      "has_value" function_qualifiers.Nc "bool" [] $
      \this this
      \prepost{acct : option AccountM}
        this |-> optional_specs.optionR
          "monad::Account"%cpp_type (fun ba ⇒ AccountR 1 ba) 1 acct
      \post[Vbool (bool_decide (is_Some acct))] emp.

  Definition SpecFor_optional_account_has_value :=
    RegisterSpec optional_account_has_value_spec.
  #[global] Existing Instance SpecFor_optional_account_has_value.

  Definition optional_account_value_spec : mpred :=
    specify.template.method
      ("std::optional".<<Atype "monad::Account"%cpp_type>>)%cpp_name
      "value" function_qualifiers.Nl (Tref "monad::Account"%cpp_type) [] $
      \this this
      \prepost{acct : AccountM}
        this |-> optional_specs.optionR
          "monad::Account"%cpp_type (fun ba ⇒ AccountR 1 ba) 1 (Some acct)
      \post[Vptr (this ,, optional_specs.opt_somety_offset
                     "monad::Account"%cpp_type)] emp.

  Definition SpecFor_optional_account_value :=
    RegisterSpec optional_account_value_spec.
  #[global] Existing Instance SpecFor_optional_account_value.

  Definition SpecFor_optional_account_reconstruct :=
    RegisterSpec
      (optional_specs.opt_reconstr AccountM "monad::Account"%cpp_type).
  #[global] Existing Instance SpecFor_optional_account_reconstruct.

  Definition optional_account_arrow_spec : mpred :=
    specify.template.op
      ("std::optional".<<Atype "monad::Account"%cpp_type>>)%cpp_name
      OOArrow function_qualifiers.N (Tptr "monad::Account"%cpp_type) [] $
      \this this
      \prepost{acct : AccountM}
        this |-> optional_specs.optionR
          "monad::Account"%cpp_type (fun ba ⇒ AccountR 1 ba) 1
          (Some acct)
      \post[Vptr (this ,, optional_specs.opt_somety_offset
                    "monad::Account"%cpp_type)]
        reference_to "monad::Account"
          (this ,, optional_specs.opt_somety_offset "monad::Account"%cpp_type)
        ** reference_to "intx::uint<256u>"
             (this ,, optional_specs.opt_somety_offset "monad::Account"%cpp_type
                  ,, o_field CU "monad::Account::balance")
        ** emp.

  Definition SpecFor_optional_account_arrow :=
    RegisterSpec optional_account_arrow_spec.
  #[global] Existing Instance SpecFor_optional_account_arrow.



  Definition account_add_to_balance_model
      (ac : AccountM) (delta : N) : AccountM :=
    account_set_balance ac (balance ac + delta).

  Definition account_subtract_from_balance_model
      (ac : AccountM) (delta : N) : AccountM :=
    account_set_balance ac (balance ac - delta).

  Definition account_set_nonce_model
      (ac : AccountM) (nonce : Z) : AccountM :=
    ac &: _coreAc .@ _block_account_nonce .= Z_to_w256 nonce.

  Definition updated_account_add_to_balance_model
      (upd : UpdatedAccountState) (ac : AccountM) (delta : N)
      : UpdatedAccountState :=
    {| postTxState := Some (account_add_to_balance_model ac delta);
       substateModel := account_substate_touch_model (substateModel upd) |}.

  Definition updated_account_subtract_from_balance_model
      (upd : UpdatedAccountState) (ac : AccountM) (delta : N)
      : UpdatedAccountState :=
    {| postTxState := Some (account_subtract_from_balance_model ac delta);
       substateModel := account_substate_touch_model (substateModel upd) |}.

  Definition account_storage_write
      (storage : evm.storage) (key value : N) : evm.storage :=
    fun k ⇒
      if bool_decide (k = bytes32_to_w256 key)
      then bytes32_to_w256 value
      else storage k.

  Definition account_set_storage_model
      (ac : AccountM) (key value : N) : AccountM :=
    {| coreAc :=
         {| block.block_account_address :=
              block.block_account_address (coreAc ac);
            block.block_account_storage :=
              account_storage_write
                (block.block_account_storage (coreAc ac)) key value;
            block.block_account_code :=
              block.block_account_code (coreAc ac);
            block.block_account_balance :=
              block.block_account_balance (coreAc ac);
            block.block_account_nonce :=
              block.block_account_nonce (coreAc ac);
            block.block_account_exists :=
              block.block_account_exists (coreAc ac);
            block.block_account_hascode :=
              block.block_account_hascode (coreAc ac) |};
       incarnation := incarnation ac;
       relevantKeys :=
         key :: filter (fun k ⇒ negb (bool_decide (k = key)))
                  (relevantKeys ac);
       balance := balance ac |}.

  Definition updated_account_set_nonce_model
      (upd : UpdatedAccountState) (ac : AccountM) (nonce : Z)
      : UpdatedAccountState :=
    {| postTxState := Some (account_set_nonce_model ac nonce);
       substateModel := substateModel upd |}.

  Definition updated_account_set_storage_model
      (upd : UpdatedAccountState) (ac : AccountM) (key value : N)
      : UpdatedAccountState :=
    {| postTxState := Some (account_set_storage_model ac key value);
       substateModel := substateModel upd |}.

  Definition evmc_storage_assigned : Z := 0.
  Definition evmc_storage_added : Z := 1.
  Definition evmc_storage_deleted : Z := 2.
  Definition evmc_storage_modified : Z := 3.
  Definition evmc_storage_deleted_added : Z := 4.
  Definition evmc_storage_modified_deleted : Z := 5.
  Definition evmc_storage_deleted_restored : Z := 6.
  Definition evmc_storage_added_deleted : Z := 7.
  Definition evmc_storage_modified_restored : Z := 8.

  Definition account_state_set_storage_status
      (_ac : AccountM) (_key value original current : N) : Z :=
    if bool_decide (value = 0%N) then
      if bool_decide (current = 0%N) then
        evmc_storage_assigned
      else if bool_decide (original = current) then
        evmc_storage_deleted
      else if bool_decide (original = 0%N) then
        evmc_storage_added_deleted
      else
        evmc_storage_modified_deleted
    else if bool_decide (current = 0%N) then
      if bool_decide (original = 0%N) then
        evmc_storage_added
      else if bool_decide (value = original) then
        evmc_storage_deleted_restored
      else
        evmc_storage_deleted_added
    else if bool_decide (original = current) then
      if bool_decide (original = value) then
        evmc_storage_assigned
      else
        evmc_storage_modified
    else if bool_decide (original = value) then
      evmc_storage_modified_restored
    else
      evmc_storage_assigned.

  Definition account_state_set_storage_post
      (upd : UpdatedAccountState) (ac : AccountM)
      (key value original : N) (status : Z)
      (upd_final : UpdatedAccountState) : Prop :=
    ∃ current,
      status =
        account_state_set_storage_status ac key value original current ∧
      upd_final = updated_account_set_storage_model upd ac key value.

  Definition record_original_storage_read_assumed
      (aps : AssumedPreTxAccountState) (key value : N)
      : AssumedPreTxAccountState :=
    {| preTxState := preTxState aps;
       preTxStorage := immer_map_insert key value (preTxStorage aps);
       assumExactness := assumExactness aps |}.

  Definition record_original_storage_read_map
      (addr : evm.address) (key value : N)
      (orig : MapModel evm.address AssumedPreTxAccountState)
      : MapModel evm.address AssumedPreTxAccountState :=
    map (fun '(addr', (loc, aps)) ⇒
           if bool_decide (addr' = addr)
           then (addr',
                 (loc, record_original_storage_read_assumed aps key value))
           else (addr', (loc, aps))) orig.

  Definition state_record_original_storage_read
      (st : StateM) (addr : evm.address) (key value : N)
      : StateM :=
    state_with_preTxAssumedState_and_newStates st
      (record_original_storage_read_map addr key value
         (preTxAssumedState st))
      (newStates st).

  Definition current_balance_pessimistic_model (st: StateM) (addr: evm.address) : N :=
    balanceOfAccount (recentAccountOf st addr).

  Definition original_balance_pessimistic_model (st: StateM) (addr: evm.address) : N :=
    balanceOfAccount (preTxAccountOf st addr).

  Definition original_balance_pessimistic_model_map
      (orig: MapModel evm.address AssumedPreTxAccountState)
      (addr: evm.address) : N :=
    balanceOfAccount (preTxAccountOf_map orig addr).

  Definition state_add_to_balance_post
      (st : StateM) (addr : evm.address) (delta : N)
      (st_final : StateM) : Prop :=
    ∃ st_current retp upd ac,
      state_current_account_state_post st addr st_current retp upd ∧
      postTxState upd = Some ac ∧
      st_final =
        state_update_current_account st_current addr
          (updated_account_add_to_balance_model upd ac delta).

  Definition state_subtract_from_balance_post
      (st : StateM) (addr : evm.address) (delta : N)
      (st_final : StateM) : Prop :=
    ∃ st_current retp upd ac,
      state_current_account_state_post st addr st_current retp upd ∧
      postTxState upd = Some ac ∧
      st_final =
        state_update_current_account
          (update_assum_exactness_state_at st_current addr
             (fun ex ⇒
                min_balance_update ex
                  (original_balance_pessimistic_model st_current addr)
                  (current_balance_pessimistic_model st_current addr)
                  delta))
         addr
         (updated_account_subtract_from_balance_model upd ac delta).

  Definition state_set_storage_post
      (st : StateM) (addr : evm.address) (key value : N) (status : Z)
      (st_final : StateM) : Prop :=
    ∃ st_current retp upd ac original upd_final,
      state_current_account_state_post st addr st_current retp upd ∧
      postTxState upd = Some ac ∧
      account_state_set_storage_post
        upd ac key value original status upd_final ∧
      let st_updated := state_update_current_account st_current addr upd_final in
      st_final = st_updated ∨
      st_final = state_record_original_storage_read st_updated addr key original.

  Definition state_set_nonce_post
      (st : StateM) (addr : evm.address) (nonce : Z)
      (st_final : StateM) : Prop :=
    ∃ st_current retp upd ac,
      state_current_account_state_post st addr st_current retp upd ∧
      postTxState upd = Some ac ∧
      st_final =
        state_update_current_account st_current addr
          (updated_account_set_nonce_model upd ac nonce).

  Definition recentAccountOf_stack (updates: list (ptr × UpdatedAccountState)) : option AccountM :=
    match updates with
    | [] ⇒ None
    | (_, upd) :: _ ⇒ postTxState upd
    end.

  Definition current_balance_pessimistic_model_stack
      (updates: list (ptr × UpdatedAccountState)) : N :=
    balanceOfAccount (recentAccountOf_stack updates).

  Definition StateCurrentLookupR
      (this: ptr)
      (qcur: Qp)
      (addr: evm.address)
      (cur: MapModel evm.address (list (ptr × UpdatedAccountState))) : mpred :=
    match mapModelLookup cur addr with
    | Some (_, cur_stack) ⇒
        this ,, o_field CU "monad::State::current_"
          |-> AnkerMapSliceR "evmc::address" "monad::VersionStack<monad::AccountState>"
                addressToN addressR (VersionStackR "monad::AccountState" UpdatedAccountStateR)
                qcur addr cur_stack
                (map (fun '(a1, (b0, _)) ⇒ (a1, b0)) cur)
    | None ⇒
        this ,, o_field CU "monad::State::current_"
          |-> AnkerMapSpineR "evmc::address" "monad::VersionStack<monad::AccountState>"
                addressToN addressR qcur
                (map (fun '(a1, (b0, _)) ⇒ (a1, b0)) cur)
    end.

  Definition check_min_balance_recent_account_model
      (cur: MapModel evm.address (list (ptr × UpdatedAccountState)))
      (addr: evm.address)
      (orig_state: AssumedPreTxAccountState) : option AccountM :=
    match mapModelLookup cur addr with
    | Some (_, updates) ⇒ recentAccountOf_stack updates
    | None ⇒ preTxState orig_state
    end.

  Definition check_min_balance_update_model
      (orig: MapModel evm.address AssumedPreTxAccountState)
      (addr: evm.address)
      (acct: option AccountM)
      (value: N) : MapModel evm.address AssumedPreTxAccountState :=
    update_assum_exactness_at addr
      (fun ex ⇒
         min_balance_update ex
           (original_balance_pessimistic_model_map orig addr)
           (balanceOfAccount acct)
           value)
      orig.

  Definition original_balance_pessimistic_model_assumed
      (orig_state: AssumedPreTxAccountState) : N :=
    balanceOfAccount (preTxState orig_state).

  Definition update_assum_exactness_assumed
      (f: AssumptionExactness → AssumptionExactness)
      (aps: AssumedPreTxAccountState) : AssumedPreTxAccountState :=
    {| preTxState := preTxState aps;
       preTxStorage := preTxStorage aps;
       assumExactness := f (assumExactness aps) |}.

  Definition set_min_balance_update_assumed
      (orig_state : AssumedPreTxAccountState)
      (value : N) : AssumedPreTxAccountState :=
    update_assum_exactness_assumed
      (fun ex ⇒
         match min_balance ex with
         | Some old ⇒
             {| min_balance := Some (N.max old value);
                nonce_exact := nonce_exact ex |}
         | None ⇒ ex
         end) orig_state.










  Definition code_piece_qp : Qp := (1 / N_to_Qp (2 ^ 32)%N)%Qp.
  Definition VarCodeR (q: Qp) (code: evm.program ) : Rep.
  Definition intercode_piece_qp : Qp := (1 / N_to_Qp (2 ^ 32)%N)%Qp.
  Definition IntercodeR (q: Qp) (code: evm.program) : Rep.

  Definition read_code_program
      (st: StateM) (hash: N) : option evm.program :=
    match codeMapOfNewStates st !! hash with
    | Some code ⇒ Some code
    | None ⇒
        match codeMapOfPreTxAssumedAccounts st !! hash with
        | Some code ⇒ Some code
        | None ⇒ dbBlockStateCodeMapLb st !! hash
        end
    end.



  #[global] Instance evmc_revision_type_compat :
    TypeCompat "enum evmc_revision" Vint := {}.

  #[global] Instance monad_revision_type_compat :
    TypeCompat "enum monad_revision" Vint := {}.

  Section monad_traits_specs.
    Context (rev: Z).

    Definition monad_traits_monad_rev_spec :=
      specify
        {|
          info_name :=
            (("monad::MonadTraits" .<< Avalue (Eint rev "enum monad_revision") >>)%cpp_name
               .:: Nfunction function_qualifiers.N "monad_rev" []);
          info_type := tFunction "enum monad_revision"%cpp_type []
        |} (
        \post[Vint rev] emp
        ).

    Definition SpecFor_monad_traits_monad_rev :=
      RegisterSpec monad_traits_monad_rev_spec.
    #[global] Existing Instance SpecFor_monad_traits_monad_rev.

    Definition gas_price_traits_spec :=
      specify
        {|
          info_name :=
            ("monad::gas_price(const monad::Transaction&, const intx::uint<256u>&)"
               .<< Atype
                     (Tnamed
                        ("monad::MonadTraits" .<< Avalue (Eint rev "enum monad_revision") >>))
               >>);
          info_type :=
            tFunction u256t
              [Tref (Tconst (Tnamed "monad::Transaction"));
               Tref (Tconst u256t)]
        |} (
        \arg{txp: ptr} "tx" (Vref txp)
        \prepost{qtx tx} txp |-> TransactionR qtx tx
        \arg{basefeep: ptr} "base_fee_per_gas" (Vref basefeep)
        \prepost{qfee base_fee} basefeep |-> u256R qfee base_fee
        \post{retp: ptr} [Vptr retp]
          retp |-> u256R 1 (gas_price_model rev tx base_fee)
        ).

    Definition SpecFor_gas_price_traits := RegisterSpec gas_price_traits_spec.
    #[global] Existing Instance SpecFor_gas_price_traits.
  End monad_traits_specs.


  Definition nullifyBalNonceStorage (e: AccountM) : AccountM.



  Definition zbvfun (fz: Z → Z) (w: keccak.w256): keccak.w256:=
    let wnz := fz (w256_to_Z w) in
    Z_to_w256 wnz.


  Definition zbvlens {A:Type} (l: Lens A A keccak.w256 keccak.w256): Lens A A Z Z :=
    {| view := λ a : A, w256_to_Z (a .^ l);
      over := λ (fz : Z → Z) (a : A), (l %= zbvfun fz) a |}.
  Locate _balance.
  Definition _nonce : Lens AccountM evm.account_state Z Z:=
    zbvlens (_coreAc .@ _block_account_nonce).

  Definition _storage (key: Z): Lens AccountM evm.account_state Z Z:=
    zbvlens (_coreAc .@ _block_account_storage .@ (ix (Z_to_w256 key))).

  Definition satAccountNonStorageAssumptions (relaxedValidation: bool) (a: option AssumedPreTxAccountState) (actualPreTxAcState: option AccountM) : Prop :=
      match a with
      | Some assumedPre ⇒
          let assumEx := assumExactness assumedPre in
          match preTxState assumedPre, actualPreTxAcState with
          | Some cs, Some csActual ⇒
             (let bal_exact := cs .^ _balance = csActual .^ _balance in
              let bal_min_ok :=
                if isSome (min_balance assumEx)
                then (min_balanceN assumEx ≤ csActual .^ _balance)%N
                else True in
              if negb relaxedValidation
              then bal_exact ∧ bal_min_ok
              else if isNone (min_balance assumEx)
                   then bal_exact
                   else bal_min_ok)
             ∧ (if (negb relaxedValidation || nonce_exact assumEx)
                 then cs .^ _nonce = (csActual).^ _nonce
                 else True)
          | None, None ⇒ True
          | _, _ ⇒ False
          end
      | None ⇒ True
      end.

  Definition satAccountStrageAssumptions (relaxedValidation: bool) (a: option AssumedPreTxAccountState) (actualPreTxAcState: option AccountM) : Prop :=
      match a with
      | Some assumedPreState ⇒
          let assumEx := assumExactness assumedPreState in
          match preTxState assumedPreState, actualPreTxAcState with
          | Some cs, Some csActual ⇒
             account_code csActual = account_code cs
             ∧ (∀ storageKey: N, storageKey ∈ relevantKeys cs
                                       → csActual .^ _storage storageKey = cs .^ _storage storageKey)
          | None, None ⇒ True
          | _, _ ⇒ False
          end
      | None ⇒ True
      end.


  Definition satAccountAssumptions (relaxedValidation: bool) (a: option AssumedPreTxAccountState) (actualPreTxAcState: option AccountM) : Prop :=
    satAccountNonStorageAssumptions relaxedValidation a actualPreTxAcState ∧ satAccountStrageAssumptions relaxedValidation a actualPreTxAcState.

  Definition satisfiesAssumptions' (relaxed : bool) (a: MapModel evm.address AssumedPreTxAccountState) (preTxState: StateOfAccounts) : Prop :=
    ∀ acAddr: address,
      satAccountAssumptions relaxed (assumptionOfAddr a acAddr) (Some (preTxState acAddr)).

  Definition satisfiesAssumptions (a: StateM) (preTxState: StateOfAccounts) : Prop :=
    satisfiesAssumptions' (relaxedValidation a) (preTxAssumedState a) preTxState.


  Definition dummyEx : AssumptionExactness := {| min_balance := None; nonce_exact := true |}.

  Definition postTxActualBalNonce (assumedPreTxState : account_state) (assumEx: AssumptionExactness) (speculativePostTxState: account_state) (actualPreTxState: account_state) : (Z×Z) :=
        (actualPreTxState .^ _balance + (speculativePostTxState .^ _balance - assumedPreTxState .^ _balance),
         actualPreTxState .^ _nonce + (speculativePostTxState .^ _nonce - assumedPreTxState .^ _nonce)).

  Definition dummyInc: Indices := {| block_index :=0; tx_index :=0 |}.


  Definition updateStorage (pre: option evm.storage) (updates: option AccountM) : evm.storage.
  Definition accountFinalVal (relaxedValidation: bool) (au : TxAssumptionsAndUpdates) (actualPreTxState: option AccountM) : option AccountM :=
    let assumEx := assumExactness (preAssumption au) in
    match txUpdates au with
    | None ⇒ actualPreTxState
    | Some (_, (_,txUpds)) ⇒
        match postTxState txUpds with
        | None ⇒ None
        | Some csUpdated ⇒
            let base := csUpdated &: _coreAc .@ _block_account_storage .= updateStorage (option_map (block.block_account_storage ∘ coreAc) actualPreTxState) (Some csUpdated) in
            if relaxedValidation then
              match preTxState (preAssumption au), actualPreTxState with
              | Some csAssumed, Some csActual ⇒
                let assumEx := assumExactness (preAssumption au) in
                  Some(
                  let '(postTxBal, postTxNonce) := postTxActualBalNonce csAssumed assumEx csUpdated csActual in
                  let postAcState := if (isNone (min_balance assumEx)) then base else base &: _balance .= Z.to_N postTxBal in
                  if (nonce_exact assumEx) then postAcState else (postAcState &: _nonce .= postTxNonce))
              | _ , _ ⇒ Some base
              end
            else Some base
        end
    end.

  Definition gmapMap {K V} `{Countable K} (f: K → V → option V) (g: gmap K V) : gmap K V.

  Definition applyUpdates (m: StateM) (preTxState: StateOfAccounts) :StateOfAccounts :=
    fun addr ⇒
      match assumptionAndUpdateOfAddr m addr with
      | None ⇒ preTxState addr
      | Some au ⇒
          match accountFinalVal (relaxedValidation m) au (Some (preTxState addr)) with
          | None ⇒ dummyAc
          | Some fv ⇒ fv
          end
      end.


  Definition execute_impl2_specg : WpSpec mpredI val val :=
    \with (speculative: bool)
     \arg{ctracerp} "" (Vref ctracerp)
    \arg{chainp :ptr} "chain" (Vref chainp)
    \prepost{(qchain:Qp) (chain: Chain)} chainp |-> ChainR qchain chain
    \arg{txp} "tx" (Vref txp)
    \prepost{qtx (t: TxWithHdr)} txp |-> TransactionR qtx t.1
    \arg{senderp} "sender" (Vref senderp)
    \prepost{qs} senderp |-> addressR qs (sender t)
    \arg{hdrp: ptr} "hdr" (Vref hdrp)
    \prepost{qh} hdrp |-> BheaderR qh t.2
    \arg{block_hash_bufferp: ptr} "block_hash_buffer" (Vref block_hash_bufferp)
    \arg{statep: ptr} "state" (Vref statep)
    \pre{au: StateM} statep |-> StateR au
    \pre [| newStates au = []|]
    \pre [| indices au = Build_Indices (txBlockNum t) (txIndex t) |]
    \prepost{(preBlockState: AugmentedState) (gl: BlockState.glocs) qb}
    (blockStatePtr au) |-> BlockState.Rfrag preBlockState qb gl
    \prepost{preTxState} (if speculative then emp else blockStatePtr au |-> BlockState.Rauth preBlockState gl preTxState)
    \post{retp}[Vptr retp] Exists assumptionsAndUpdates result,
      statep |-> StateR assumptionsAndUpdates
      ** retp |-> ResultSuccessR EvmcResultR result
      ** [| blockStatePtr assumptionsAndUpdates = blockStatePtr au |]
      ** [| validStateM assumptionsAndUpdates |]
       ** [| indices assumptionsAndUpdates = indices au |]
       ** [| let postCond (preTxState : StateOfAccounts) :=
               let 'Build_EvmExecResult postTxState actualResult changed execAccounts := execTxCore' preTxState t in
               postTxState = applyUpdates assumptionsAndUpdates preTxState ∧ result = actualResult in
             if speculative then
               ∀ preTxState, satisfiesAssumptions assumptionsAndUpdates preTxState → postCond preTxState
             else satisfiesAssumptions assumptionsAndUpdates preTxState.1 ∧ postCond preTxState.1
          |].





  Definition lookupStorage (s: StateOfAccounts) (addr: address) (key: N) (blockTxInd: Indices) : N.



  Definition WithdrawalR (q: cQp.t) (w: Withdrawal) : Rep.
  Definition ConsensusBlockHeaderR (q: cQp.t) (w: ConsensusBlockHeader) : Rep.
  Definition EmptyCallFramesR (q: cQp.t) : Rep.

  Definition recent_spec_core : ptr → WpSpec mpredI val val := (fun (this: ptr) ⇒
                \prepost{q h tl} this |-> VersionStackSpineR
                  "monad::AccountState"
                     (cQp.mut q)
                     (h::tl)
                     \post [Vptr h] emp).


  Definition sliceInvariants (au: TxAssumptionsAndUpdates) : Prop :=
    let assumEx := assumExactness (preAssumption au) in
    let assumedPreTxState := preTxState (preAssumption au) in
    match min_balance assumEx, txUpdates au with
    | _, None ⇒ True
    | None , _ ⇒ True
    | Some minbal, Some (_, (_,txUpds)) ⇒
        match (postTxState txUpds), assumedPreTxState with
        | None, _ ⇒ True
        | _, None ⇒ True
        | Some csUpdated, Some assumedPre ⇒
            incarnation csUpdated = incarnation assumedPre
            → (assumedPre .^ _balance - csUpdated .^ _balance ≤ minbal)
        end
    end.

  #[global] Instance llll: LearnEq2 MapCurrentR := ltac:(solve_learnable).
Definition is_empty_model (oas: option AccountM) : bool :=
  match oas with
  | None ⇒ true
  | Some am ⇒ let ba := coreAc am in
      let ch := code_hash_of_program
                  (monad.EVMOpSem.block.block_account_code ba) in
      let zn := w256_to_Z
                  (monad.EVMOpSem.block.block_account_nonce ba) in
      let bn := w256_to_N
                  (monad.EVMOpSem.block.block_account_balance ba) in
      (N.eqb ch 0%N)
      && (Z.eqb zn 0)
      && (N.eqb bn 0%N)
  end.

Definition is_dead_model (oas: option AccountM) : bool :=
  negb (bool_decide (option.is_Some oas)) || is_empty_model oas.















  #[global] Instance dec (i1 i2: Indices): Decision (i1=i2) := ltac:(solve_decision).



  Definition sender_seen_in_current_prefix
      (ctx : MonadChainContext) (i : nat) (tx : TxWithHdr) : Prop :=
    ∃ j : nat,
      j ≤ i ∧
      ((j < i ∧
        nth_error (map sender (txsWithHdr (cblock ctx))) j = Some (sender tx)) ∨
       ∃ auths,
         nth_error (map txAuthoritiesDelFrom (transactions (cblock ctx))) j = Some auths ∧
         Some (sender tx) ∈ auths).


  Definition reserve_violation_threshold_model
      (orig: MapModel evm.address AssumedPreTxAccountState)
      
      (addr sender: evm.address) (gas_fees: N) : option N :=
    let orig_bal := original_balance_pessimistic_model_map orig addr in
    let reserve := N.min DefReserve orig_bal in
    if asbool (addr = sender)
    then if N.ltb reserve gas_fees then None else Some (N.sub reserve gas_fees)
    else Some reserve.

  Definition check_min_original_balance_update
      (orig: MapModel evm.address AssumedPreTxAccountState)
      (addr: evm.address) (max_reserve: N)
      : MapModel evm.address AssumedPreTxAccountState :=
    let orig_bal := original_balance_pessimistic_model_map orig addr in
    update_assum_exactness_at addr
      (fun ex ⇒ min_balance_update ex orig_bal orig_bal max_reserve) orig.

  Definition dipped_into_reserve_name : name :=
    Ninst
      (Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
         (Nfunction function_qualifiers.N "dipped_into_reserve"
           [Tref (Qconst (Tnamed "evmc::address"));
            Tref (Qconst (Tnamed "monad::Transaction"));
            Tref (Qconst u256t);
            Tulong;
            Tref (Qconst (Tnamed "monad::MonadChainContext"));
            Tref (Tnamed "monad::State")]))
      [Atype (Tnamed ("monad::MonadTraits" .<< Avalue (Eint 9 "enum monad_revision") >>))].

  Definition dipped_into_reserve_lam : name :=
    Nscoped dipped_into_reserve_name (Nanon 1).

  Definition dipped_into_reserve_capture_field (nm: ident) : field :=
    Nscoped dipped_into_reserve_lam (field_name.CaptureVar nm).

  Definition DippedIntoReserveLambdaR
      (addrp statep senderp gas_feesp: ptr) : Rep :=
    
    (((o_field CU (dipped_into_reserve_capture_field "addr")
          |-> refR<"evmc::address"> 1$m addrp)
        ** o_field CU (dipped_into_reserve_capture_field "state")
          |-> refR<"monad::State"> 1$m statep)
      ** o_field CU (dipped_into_reserve_capture_field "sender")
        |-> refR<"evmc::address"> 1$m senderp)
    ** o_field CU (dipped_into_reserve_capture_field "gas_fees")
      |-> refR<"intx::uint<256u>"> 1$m gas_feesp
    ** structR dipped_into_reserve_lam 1$m.

  Definition dipped_into_reserve_lam_ctor_spec :=
    specify
      {| info_name := dipped_into_reserve_lam;
         info_type :=
           tFunction (Tnamed dipped_into_reserve_lam)
             [Tref (Qconst (Tnamed "evmc::address"));
              Tref (Tnamed "monad::State");
              Tref (Qconst (Tnamed "evmc::address"));
              Tref (Qconst u256t)] |} $
      \arg{addrp: ptr} "addr" (Vref addrp)
      \arg{statep: ptr} "state" (Vref statep)
      \arg{senderp: ptr} "sender" (Vref senderp)
      \arg{gas_feesp: ptr} "gas_fees" (Vref gas_feesp)
      \prepost{qaddr addr} addrp |-> addressR qaddr addr
      \prepost{qsender sender} senderp |-> addressR qsender sender
      \prepost{qfee gas_fees} gas_feesp |-> u256R qfee gas_fees
      \prepost{st} statep |-> StateR st
      \post{retp: ptr} [Vptr retp]
        retp |-> DippedIntoReserveLambdaR addrp statep senderp gas_feesp.

  Definition SpecFor_dipped_into_reserve_lam_ctor :=
    RegisterSpec dipped_into_reserve_lam_ctor_spec.
  #[global] Existing Instance SpecFor_dipped_into_reserve_lam_ctor.






#[global] Instance : LearnEq2 u256R := ltac:(solve_learnable).

  Lemma observeOrigState (state_addr:ptr) q t:
    Observe (type_ptr "monad::OriginalAccountState" state_addr)
            (state_addr |-> OriginalAccountStateR q t).

  Lemma observeState (state_addr:ptr) q t:
    Observe (type_ptr "monad::AccountState" state_addr)
            (state_addr |-> UpdatedAccountStateR q t).

  Lemma observeBytes32 (bp:ptr) q v:
    Observe (type_ptr "evmc::bytes32" bp)
            (bp |-> bytes32R q v).

  Definition observeStateF r q t:= @observe_fwd _ _ _ (observeState r q t).
  Definition observeOrigStateF r q t:= @observe_fwd _ _ _ (observeOrigState r q t).
  Definition observeBytes32F r q v := @observe_fwd _ _ _ (observeBytes32 r q v).

  Lemma observeBytes32Range (q : Qp) (v : N) :
    Observe (pureR [| (v < 2 ^ 256)%N |]) (bytes32R q v).

  Definition observeBytes32RangeF (q : Qp) (v : N) :=
    ltac:(mk_at_obs_fwd (observeBytes32Range q v)).

  Lemma observeU256 (bp:ptr) q v:
    Observe (type_ptr u256t bp)
            (bp |-> u256R q v).

  Definition observeU256F r q v := @observe_fwd _ _ _ (observeU256 r q v).

  Lemma observeU256Range (q : Qp) (v : N) :
    Observe (pureR [| (v < 2 ^ 256)%N |]) (u256R q v).

  Definition observeU256RangeF (q : Qp) (v : N) :=
    ltac:(mk_at_obs_fwd (observeU256Range q v)).

  Lemma observeBlockStateRfragTypePtr
      (bp : ptr) preBlockState q g :
    Observe (type_ptr "monad::BlockState" bp)
            (bp |-> BlockState.Rfrag preBlockState q g).

  Definition observeBlockStateRfragTypePtrF bp preBlockState q g :=
    @observe_fwd _ _ _ (observeBlockStateRfragTypePtr bp preBlockState q g).

  Lemma observeVersionStackSpineTypePtr
      (cppType : type) (q : Qp) (lt : list ptr) :
    Observe (type_ptrR (VersionStack_ty cppType))
            (VersionStackSpineR cppType q lt).

  Definition observeVersionStackSpineTypePtrF
      (cppType : type) (q : Qp) (lt : list ptr) :=
    ltac:(mk_at_obs_fwd
      (observeVersionStackSpineTypePtr cppType q lt)).

  Lemma version_stack_spine_keep_type_ptr
      (p : ptr) (cppType : type) (q : Qp) (lt : list ptr) :
    p |-> VersionStackSpineR cppType q lt
    |--
    p |-> VersionStackSpineR cppType q lt
    ** type_ptr (VersionStack_ty cppType) p.

  Definition version_stack_spine_keep_type_ptr_C
      (p : ptr) (cppType : type) (q : Qp) (lt : list ptr) :=
    [CANCEL] (version_stack_spine_keep_type_ptr p cppType q lt).

  #[global] Instance optionR_type_ptr_observe
      {T} (somety: type) (R: T → Rep) (q: Qp) (o: option T) (p: ptr)
    : Observe (type_ptr (Tnamed ("std::optional".<<Atype somety>>)) p)
        (p |-> optional_specs.optionR somety R q o).

  Definition observeOptionF {T} (somety: type) (R: T → Rep) (p: ptr) (q: Qp) (o: option T) :=
    @observe_fwd _ _ _ (@optionR_type_ptr_observe T somety R q o p).


  Lemma observeState2 (state_addr:ptr) t:
    Observe (type_ptr (Tnamed "monad::State") state_addr)
            (state_addr |-> StateR t).
  Definition observeStateF2 r t := @observe_fwd _ _ _ (observeState2 r t).

#[global] Instance : LearnEq2 (addressR) := ltac:(solve_learnable).
#[global] Instance : LearnEq2 optionAddressR := ltac:(solve_learnable).
#[global] Instance : LearnEq1 (StateR) := ltac:(solve_learnable).
#[global] Instance : LearnEq2 bytes32R := ltac:(solve_learnable).

Definition update_assum_exactness_map
           (m: MapModel evm.address AssumedPreTxAccountState)
           (updates: gmap evm.address AssumptionExactness)
  : MapModel evm.address AssumedPreTxAccountState :=
  map (fun p ⇒
         let '(addr, (loc, aps)) := p in
         match updates !! addr with
         | Some ex ⇒
             (addr, (loc, {| preTxState := preTxState aps;
                             preTxStorage := preTxStorage aps;
                             assumExactness := ex |}))
         | None ⇒ p
         end) m.

Definition update_assum_exactness_state
           (st: StateM)
           (updates: gmap evm.address AssumptionExactness) : StateM :=
  {| relaxedValidation := relaxedValidation st;
     preTxAssumedState := update_assum_exactness_map (preTxAssumedState st) updates;
     newStates := newStates st;
     blockStatePtr := blockStatePtr st;
     indices := indices st;
     blockStateGloc := blockStateGloc st;
     dbBlockStateCodeMapLb := dbBlockStateCodeMapLb st;
     codeMap := codeMap st;
  |}.

Definition min_balance_stricter (old new: option N) : Prop :=
  match old, new with
  | None, None ⇒ True
  | None, Some _ ⇒ False
  | Some _, None ⇒ True
  | Some m, Some m' ⇒ (m ≤ m')%N
  end.

Definition assumption_exactness_stricter
           (old new: AssumptionExactness) : Prop :=
  min_balance_stricter (min_balance old) (min_balance new)
  ∧ (nonce_exact old = true → nonce_exact new = true).

Definition updates_stricter
           (st: StateM)
           (updates: gmap evm.address AssumptionExactness) : Prop :=
  ∀ addr ex,
    updates !! addr = Some ex →
    ∃ loc aps,
      preTxAssumedState st !! addr = Some (loc, aps)
      ∧ assumption_exactness_stricter (assumExactness aps) ex.

Definition gdom {K V} `{Countable K} (g: gmap K V) : list K :=
  map fst (map_to_list g).

Lemma gdomemp {K V} `{Countable K} : @gdom K V _ _ ∅ = [].

Lemma updates_stricter_emp stm : updates_stricter stm ∅.

End with_Sigma.

Section reserve_balance_helpers.
  Context `{Sigma : cpp_logic} {CU : genv} {hh : HasOwn mpredI fracR}.

  Lemma empupd (m : MapModel evm.address AssumedPreTxAccountState) :
    update_assum_exactness_map m ∅ = m.

  Lemma mpmp {K V} (foo : MapModel K V) :
    map (fun x ⇒ (let '(a, (b, _)) := x in (a, b)).2) foo = map (fun x ⇒ x.2.1) foo.

  Lemma mpmp1 {K V} (foo : MapModel K V) :
    map (fun x ⇒ (let '(a, (b, _)) := x in (a, b)).1) foo = map fst foo.

  Lemma updsame (stm : StateM) (t : gmap evm.address AssumptionExactness) :
    map fst (update_assum_exactness_map (preTxAssumedState stm) t) = map fst (preTxAssumedState stm).
End reserve_balance_helpers.

Definition isAccountDelegated (o : option AccountM) : bool :=
  match o with
  | Some am ⇒ isDelegationMarker (block.block_account_code (coreAc am))
  | None ⇒ false
  end.

#[global] Hint Resolve observeStateF2 : sl_opacity.
#[global] Hint Resolve updates_stricter_emp : pure.
#[global] Hint Rewrite @lookup_empty @map_id : syntactic.
#[global] Hint Rewrite @gdomemp empupd : syntactic.
#[global] Hint Rewrite @map_map @mpmp @nth_error_map : syntactic.

#[global] Opaque
  bytes32_be_values_from
  bytes32_be_values
  evmc_bytes32_wordR
  bytes32R
  evmc_bytes32R.
#[global] Hint Opaque
  bytes32_be_values_from
  bytes32_be_values
  evmc_bytes32_wordR
  bytes32R
  evmc_bytes32R : sl_opacity.
#[global] Opaque BlockHashBufferR.
#[global] Hint Opaque BlockHashBufferR: sl_opacity.
#[global] Opaque BheaderR.
#[global] Hint Opaque BheaderR : sl_opacity.
#[global] Opaque TransactionR.
#[global] Hint Opaque TransactionR : sl_opacity.
#[global] Opaque StateR.
#[global] Hint Opaque StateR : sl_opacity.
#[only(lens)] derive StateM.
#[global] Hint Resolve observeStateF observeOrigStateF observeBytes32F
  observeBytes32RangeF observeU256F observeU256RangeF
  observeBlockStateRfragTypePtrF observeVersionStackSpineTypePtrF
  version_stack_spine_keep_type_ptr_C observeOptionF: sl_opacity.

Definition dummyTx : TxWithHdr.

Definition base_fee_per_gas (b: Block) : w256 :=
  match (base_fee_per_gas (header b)) with
  | Some s ⇒ s
  | None ⇒ 0%N
  end.

Lemma lengthZ_txsWithHdr (b : Block) :
  lengthZ (txsWithHdr b) = lengthZ (transactions b).
#[global] Hint Rewrite lengthZ_txsWithHdr : syntactic.

#[only(lazy_unfold)] derive TransactionR.
#[only(lazy_unfold)] derive AccountR.
#[only(lazy_unfold)] derive StateR.
#[only(eager_unfold)] derive DippedIntoReserveLambdaR.
#[only(eager_unfold)] derive UpdatedAccountStateR.
#[only(eager_unfold)] derive pairR.
#[only(eager_unfold)] derive VersionStackR.
#[only(eager_unfold)] derive StateOriginalR.
#[only(eager_unfold)] derive AnkerMapSliceR.
#[only(eager_unfold)] derive MonadChainContextR.

Section reserve_balance_proof_env.
  Context `{Sigma : cpp_logic} {CU : genv} {hh : HasOwn mpredI fracR}.

#[global] Instance kjsfdjs {T} a : LearnEq3 (@VersionStackR _ _ _ T a) := ltac:(solve_learnable).
#[global] Instance kjfslksfdjs a : LearnEq2 (@VersionStackSpineR _ _ _ a) := ltac:(solve_learnable).
#[global] Instance learnStateDirtyStackR : LearnEq2 StateDirtyStackR := ltac:(solve_learnable).

#[global] Instance ll : LearnEq2 AccountStateRcore := ltac:(solve_learnable).
#[global] Instance lll : LearnEq2 MonadChainContextR := ltac:(solve_learnable).

End reserve_balance_proof_env.

#[global] Hint Unfold ModelWithPtr : unfold.

#[global] Hint Opaque OriginalAccountStateR : sl_opacity.
#[global] Hint Opaque SharedPtrR : sl_opacity.
#[global] Hint Opaque AccountStateRcore : sl_opacity.
#[global] Hint Opaque StorageMapR : sl_opacity.
#[global] Hint Opaque VersionStackR : sl_opacity.
#[global] Hint Opaque StateDirtyStackR : sl_opacity.
#[global] Hint Opaque optionAddressR : sl_opacity.
#[global] Hint Opaque VectorR : sl_opacity.
#[global] Hint Opaque atomicR : sl_opacity.
#[global] Hint Opaque MonadChainContextR : sl_opacity.
#[global] Hint Opaque blockStatePtr : sl_opacity.
#[global] Hint Opaque specify.exact.method : sl_opacity.
#[global] Hint Opaque gas_price_traits_spec : sl_opacity.
#[global] Hint Opaque authsp : sl_opacity.
#[global] Hint Opaque sendersp : sl_opacity.
#[global] Hint Opaque std.vector.base_pointer : sl_opacity.
#[global] Hint Opaque LogsR : sl_opacity.
#[global] Hint Opaque DippedIntoReserveLambdaR StateOriginalR : sl_opacity.
#[global] Hint Opaque dipped_into_reserve_lam_ctor_spec pairR : sl_opacity.
#[global] Hint Opaque AnkerMapSliceR : sl_opacity.
#[global] Hint Opaque incarnation_copy_spec : sl_opacity.
#[global] Hint Opaque incarnation_dtor_spec : sl_opacity.
#[global] Hint Opaque account_state_set_storage_spec : sl_opacity.
#[global] Hint Opaque state_set_storage_spec : sl_opacity.
#[global] Hint Opaque account_dtor_spec : sl_opacity.
#[global] Hint Opaque account_substate_touch_spec : sl_opacity.
#[global] Hint Opaque uint256_max_spec : sl_opacity.
#[global] Hint Opaque state_current_account_state_update_spec : sl_opacity.
#[global] Hint Opaque optional_account_has_value_spec : sl_opacity.
#[global] Hint Opaque optional_account_value_spec : sl_opacity.
#[global] Hint Opaque optional_account_bool_spec : sl_opacity.
#[global] Hint Opaque optional_account_arrow_spec : sl_opacity.
#[global] Hint Opaque optional_account_arrow_const_spec : sl_opacity.
#[global] Hint Opaque monad_assertion_failed_spec : sl_opacity.
#[global] Hint Opaque bytes32_evmc_bytes32_ctor_spec : sl_opacity.
#[global] Hint Opaque evmc_bytes32_dtor_spec : sl_opacity.
#[global] Hint Opaque bytes32_assign_spec : sl_opacity.
#[global] Hint Opaque StateCodeMapR : sl_opacity.

#[global] Opaque AccountStateRcore.
#[global] Opaque AccountSubstateR.
#[global] Opaque StateDirtyStackR.

Section reserve_balance_proof_env2.
  Context `{Sigma : cpp_logic} {CU : genv} {hh : HasOwn mpredI fracR}.

#[global] Instance optionRSome {SomeTyModel : Type}
  (somety somety2 : skylabs.lang.cpp.syntax.core.type)
  (someTyRep someTyRep2 : SomeTyModel → Rep) (q : Qp)
  (s : SomeTyModel) (oa : option SomeTyModel) (b : ptr) :
  learn_exist_interface.Learnable
    (b ,, opt_somety_offset somety |-> someTyRep s)
    (b |-> optional_specs.optionR somety2 someTyRep2 q oa)
    [oa = Some s; someTyRep = someTyRep2] := ltac:(solve_learnable).

#[global] Instance optionRSomeT {SomeTyModel1 SomeTyModel2 : Type}
  (somety somety2 : skylabs.lang.cpp.syntax.core.type)
  (someTyRep : SomeTyModel1 → Rep) (someTyRep2 : SomeTyModel2 → Rep)
  (q : Qp) s1 (oa : option SomeTyModel2) (b : ptr) :
  learn_exist_interface.Learnable
    (b ,, opt_somety_offset somety |-> someTyRep s1)
    (b |-> optional_specs.optionR somety2 someTyRep2 q oa)
    [SomeTyModel1 = SomeTyModel2] := ltac:(solve_learnable).

#[global] Instance optionRSomeT2 {SomeTyModel1 SomeTyModel2 : Type}
  (somety somety2 : skylabs.lang.cpp.syntax.core.type)
  (someTyRep : SomeTyModel1 → Rep) (someTyRep2 : SomeTyModel2 → Rep)
  (q1 q2 : Qp) s1 (oa : option SomeTyModel2) (b : ptr) :
  learn_exist_interface.Learnable
    (b |-> optional_specs.optionR somety someTyRep q1 s1)
    (b |-> optional_specs.optionR somety2 someTyRep2 q2 oa)
    [SomeTyModel1 = SomeTyModel2] := ltac:(solve_learnable).

#[global] Instance optionRSomeq {SomeTyModel : Type} (somety : type)
  (someTyRep someTyRep2 : SomeTyModel → Rep) (q1 : Qp) (s : SomeTyModel)
  (a a2 : SomeTyModel) (b : ptr) :
  learn_exist_interface.Learnable
    (b |-> optional_specs.optionR somety someTyRep q1 (Some a))
    (b ,, opt_somety_offset somety |-> someTyRep2 a2)
    [a = a2; someTyRep = someTyRep2] := ltac:(solve_learnable).

Lemma optionRSomeqUnfold {SomeTyModel : Type} (somety : type)
  (someTyRep : SomeTyModel → Rep) (q1 : Qp) (s : SomeTyModel)
  (a : SomeTyModel) (b : ptr) :
  (b |-> optional_specs.optionR somety someTyRep q1 (Some a))
    -|-
  (b |-> structR ("std::optional" .<< Atype somety >>) q1$m **
   b ,, opt_engaged_offset somety |-> boolR q1$m true)
    ** (b ,, opt_somety_offset somety |-> someTyRep a).

Definition optionRSomeUnfoldF := [FWD->] @optionRSomeqUnfold.
Definition optionRSomeUnfoldB := [BWD->] @optionRSomeqUnfold.

#[global] Instance fsksdjfk q1 q2 :
  Refine1 false false (u256R q1 = u256R q2) [q1 = q2] :=
  ltac:(constructor; auto).

#[global] Instance codeMapInv (p : ptr) st :
  Observe [| stateCodeMapInvariants st |] (p |-> StateCodeMapR st) := _.
Definition observeCodeInv r t := @observe_fwd _ _ _ (codeMapInv r t).
#[global] Instance LearnEq1_StateCodeMapR : LearnEq1 StateCodeMapR :=
  ltac:(solve_learnable).

Lemma borrowIndex_at (q : Qp) {K V : Type} {eqd : EqDecision K}
  (tykey tyval : type) (krep : Qp → K → Rep) (vrep : Qp → V → Rep)
  (m : MapModel K V) (borrowIndex : N) bt btk (p : ptr) :
  nth_error m (N.to_nat borrowIndex) = Some bt →
  btk = bt.1 →
  p |-> AnkerMapPayloadsR tykey tyval krep vrep q m -|-
    ((bt.2.1 |-> pairR tykey tyval krep vrep (q / 2) q (bt.1, bt.2.2)))
      ** p |-> AnkerMapPayloadsR tykey tyval krep vrep q (removeKey m btk).

End reserve_balance_proof_env2.





#[global] Hint Resolve optionRSomeUnfoldF optionRSomeUnfoldB : sl_opacity.
#[global] Hint Resolve observeCodeInv : sl_opacity.

Section reserve_balance_specs.
  Context `{Sigma : cpp_logic} {CU : genv} {hh : HasOwn mpredI fracR}.
  Context {MODd : reserve_balance_cpp.module ⊧ CU}.

  Definition SpecFor_address_set_contains :=
    ankerl_specs.SpecFor_anker_set_contains.
  #[global] Existing Instance SpecFor_address_set_contains.

  Definition SpecFor_ranges_contains_optional_address :=
    RegisterSpec
      (ranges_specs.ranges_contains_optional_address_spec
         (fun q xs ⇒ std.vector.R "std::optional<evmc::address>" q xs)
         addressR).
  #[global] Existing Instance SpecFor_ranges_contains_optional_address.








  cpp.spec (functionNamed reserve_balance_cpp.module "dipped_into_reserve") as dipped_into_reserve_spec with (
  \arg{senderp: ptr} "sender" (Vref senderp)
  \let{(ctx: MonadChainContext) (i: nat)} tx := nth i (txsWithHdr (cblock ctx)) dummyTx
  \pre [| (Z.of_nat i < lengthZ (transactions (currentBlock (blocks ctx))))%Z |]
  \pre [| validTx tx |]
  \prepost{qsender } senderp |-> addressR qsender (sender tx)
  \arg{txp: ptr} "tx" (Vref txp)
  \prepost{qtx } txp |-> TransactionR qtx tx.1
  \arg{basefeep: ptr} "base_fee_per_gas" (Vref basefeep)
  \prepost{qfee} basefeep |-> u256R qfee (base_fee_per_gas (cblock ctx))
  \arg "i" (Vint i)
  \arg{ctxp: ptr} "ctx" (Vref ctxp)
  \prepost{qctx} ctxp |-> MonadChainContextR qctx ctx
  \pre{hist: ExtraAcStates} [| historyConsistent ctx hist ∧ ∀ addr, configuredReserveBal (hist addr) = DefReserve |]%N
  \arg{statep: ptr} "state" (Vref statep)
  \pre{(qstate:Qp) (st: StateM)} statep |-> StateR st
  \pre [| ∀ (i0 : N)
                 (nthElemPtr0 nthElemVstackTopPtr0 : ptr)
                 (nthElemVstackTop0 : UpdatedAccountState)
                 (nthElemVstackTl0 : list (ptr × UpdatedAccountState)),
            nth_error (newStates st) (N.to_nat i0) =
              Some (sender tx, (nthElemPtr0, (nthElemVstackTopPtr0, nthElemVstackTop0) :: nthElemVstackTl0)) →
            match
              mapModelLookup
                (check_min_original_balance_update
                   (preTxAssumedState st) (sender tx) DefReserve)
                (sender tx)
            with
            | Some (_, aps) ⇒
                match postTxState nthElemVstackTop0 with
                | Some am ⇒ isDelegationMarker (block.block_account_code (coreAc am))
                | None ⇒ false
                end =
                match preTxState aps with
                | Some am ⇒ isDelegationMarker (block.block_account_code (coreAc am))
                | None ⇒ false
                end && asbool (sender tx ∉ undels tx.1.2) || asbool (sender tx ∈ dels tx.1.2)
            | None ⇒ False
            end |]
  \prepost{preBlockState bs qb} blockStatePtr st |-> BlockState.Rfrag preBlockState qb bs
  \prepost{qnull} _global "monad::NULL_HASH" |-> bytes32R qnull 0
  \post{retb:bool} [Vbool retb]
    Exists (updates: gmap evm.address AssumptionExactness),
      let stf := update_assum_exactness_state st updates in
      statep |-> StateR stf **
      [| updates_stricter st updates |] **
      [| ∀ (preTxState: StateOfAccounts),
          satisfiesAssumptions stf preTxState →
          let postTxState := (applyUpdates stf preTxState) in
          let changedAcs := (map fst (newStates st)) in
          retb = negb (allFinalBalSufficient 3 (preTxState, hist) postTxState changedAcs tx)
      |]).

End reserve_balance_specs.