(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module instructions.
  Module host.
    (*
    pub fn balance<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        pop_address!(interpreter, address);
        let Some((balance, is_cold)) = host.balance(address) else {
            interpreter.instruction_result = InstructionResult::FatalExternalError;
            return;
        };
        gas!(
            interpreter,
            if SPEC::enabled(BERLIN) {
                warm_cold_cost(is_cold)
            } else if SPEC::enabled(ISTANBUL) {
                // EIP-1884: Repricing for trie-size-dependent opcodes
                700
            } else if SPEC::enabled(TANGERINE) {
                400
            } else {
                20
            }
        );
        push!(interpreter, balance);
    }
    *)
    Definition balance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ address :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "alloy_primitives::bits::address::Address",
                        "from_word",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::From",
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [],
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                []
                            ],
                            "from",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm_interpreter::interpreter::stack::Stack",
                                "pop_unsafe",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| interpreter |),
                                  "revm_interpreter::interpreter::Interpreter",
                                  "stack"
                                |)
                              ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (| "revm_interpreter::host::Host", H, [], "balance", [] |),
                      [ M.read (| host |); M.read (| address |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                        let balance := M.copy (| γ1_0 |) in
                        let is_cold := M.copy (| γ1_1 |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "revm_interpreter::gas::Gas",
                                              "record_cost",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| interpreter |),
                                                "revm_interpreter::interpreter::Interpreter",
                                                "gas"
                                              |);
                                              M.read (|
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.use
                                                            (M.alloc (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "revm_primitives::specification::Spec",
                                                                  SPEC,
                                                                  [],
                                                                  "enabled",
                                                                  []
                                                                |),
                                                                [
                                                                  Value.StructTuple
                                                                    "revm_primitives::specification::SpecId::BERLIN"
                                                                    []
                                                                ]
                                                              |)
                                                            |)) in
                                                        let _ :=
                                                          M.is_constant_or_break_match (|
                                                            M.read (| γ |),
                                                            Value.Bool true
                                                          |) in
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "revm_interpreter::gas::calc::warm_cold_cost",
                                                              []
                                                            |),
                                                            [ M.read (| is_cold |) ]
                                                          |)
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.match_operator (|
                                                          M.alloc (| Value.Tuple [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "revm_primitives::specification::Spec",
                                                                          SPEC,
                                                                          [],
                                                                          "enabled",
                                                                          []
                                                                        |),
                                                                        [
                                                                          Value.StructTuple
                                                                            "revm_primitives::specification::SpecId::ISTANBUL"
                                                                            []
                                                                        ]
                                                                      |)
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                M.alloc (|
                                                                  Value.Integer IntegerKind.U64 700
                                                                |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.match_operator (|
                                                                  M.alloc (| Value.Tuple [] |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let γ :=
                                                                          M.use
                                                                            (M.alloc (|
                                                                              M.call_closure (|
                                                                                M.get_trait_method (|
                                                                                  "revm_primitives::specification::Spec",
                                                                                  SPEC,
                                                                                  [],
                                                                                  "enabled",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  Value.StructTuple
                                                                                    "revm_primitives::specification::SpecId::TANGERINE"
                                                                                    []
                                                                                ]
                                                                              |)
                                                                            |)) in
                                                                        let _ :=
                                                                          M.is_constant_or_break_match (|
                                                                            M.read (| γ |),
                                                                            Value.Bool true
                                                                          |) in
                                                                        M.alloc (|
                                                                          Value.Integer
                                                                            IntegerKind.U64
                                                                            400
                                                                        |)));
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (M.alloc (|
                                                                          Value.Integer
                                                                            IntegerKind.U64
                                                                            20
                                                                        |)))
                                                                  ]
                                                                |)))
                                                          ]
                                                        |)))
                                                  ]
                                                |)
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                              []
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_interpreter::interpreter::stack::Stack",
                                  "push",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| interpreter |),
                                    "revm_interpreter::interpreter::Interpreter",
                                    "stack"
                                  |);
                                  M.read (| balance |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Ok",
                                      0
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Err",
                                      0
                                    |) in
                                  let e := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            M.read (| e |)
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_balance : M.IsFunction "revm_interpreter::instructions::host::balance" balance.
    
    (*
    pub fn selfbalance<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        check!(interpreter, ISTANBUL);
        gas!(interpreter, gas::LOW);
        let Some((balance, _)) = host.balance(interpreter.contract.target_address) else {
            interpreter.instruction_result = InstructionResult::FatalExternalError;
            return;
        };
        push!(interpreter, balance);
    }
    *)
    Definition selfbalance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "revm_primitives::specification::Spec",
                                      SPEC,
                                      [],
                                      "enabled",
                                      []
                                    |),
                                    [
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::ISTANBUL"
                                        []
                                    ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::NotActivated"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::gas::Gas",
                                      "record_cost",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "gas"
                                      |);
                                      M.read (|
                                        M.get_constant (| "revm_interpreter::gas::constants::LOW" |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (| "revm_interpreter::host::Host", H, [], "balance", [] |),
                      [
                        M.read (| host |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| interpreter |),
                              "revm_interpreter::interpreter::Interpreter",
                              "contract"
                            |),
                            "revm_interpreter::interpreter::contract::Contract",
                            "target_address"
                          |)
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                        let balance := M.copy (| γ1_0 |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_interpreter::interpreter::stack::Stack",
                                  "push",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| interpreter |),
                                    "revm_interpreter::interpreter::Interpreter",
                                    "stack"
                                  |);
                                  M.read (| balance |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Ok",
                                      0
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Err",
                                      0
                                    |) in
                                  let e := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            M.read (| e |)
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_selfbalance :
      M.IsFunction "revm_interpreter::instructions::host::selfbalance" selfbalance.
    
    (*
    pub fn extcodesize<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        pop_address!(interpreter, address);
        let Some((code, is_cold)) = host.code(address) else {
            interpreter.instruction_result = InstructionResult::FatalExternalError;
            return;
        };
        if SPEC::enabled(BERLIN) {
            gas!(interpreter, warm_cold_cost(is_cold));
        } else if SPEC::enabled(TANGERINE) {
            gas!(interpreter, 700);
        } else {
            gas!(interpreter, 20);
        }
    
        push!(interpreter, U256::from(code.len()));
    }
    *)
    Definition extcodesize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ address :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "alloy_primitives::bits::address::Address",
                        "from_word",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::From",
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [],
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                []
                            ],
                            "from",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm_interpreter::interpreter::stack::Stack",
                                "pop_unsafe",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| interpreter |),
                                  "revm_interpreter::interpreter::Interpreter",
                                  "stack"
                                |)
                              ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (| "revm_interpreter::host::Host", H, [], "code", [] |),
                      [ M.read (| host |); M.read (| address |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                        let code := M.copy (| γ1_0 |) in
                        let is_cold := M.copy (| γ1_1 |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "revm_primitives::specification::Spec",
                                            SPEC,
                                            [],
                                            "enabled",
                                            []
                                          |),
                                          [
                                            Value.StructTuple
                                              "revm_primitives::specification::SpecId::BERLIN"
                                              []
                                          ]
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  UnOp.not (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "revm_interpreter::gas::Gas",
                                                        "record_cost",
                                                        []
                                                      |),
                                                      [
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| interpreter |),
                                                          "revm_interpreter::interpreter::Interpreter",
                                                          "gas"
                                                        |);
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "revm_interpreter::gas::calc::warm_cold_cost",
                                                            []
                                                          |),
                                                          [ M.read (| is_cold |) ]
                                                        |)
                                                      ]
                                                    |)
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  let~ _ :=
                                                    M.write (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "instruction_result"
                                                      |),
                                                      Value.StructTuple
                                                        "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                        []
                                                    |) in
                                                  M.return_ (| Value.Tuple [] |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "revm_primitives::specification::Spec",
                                                    SPEC,
                                                    [],
                                                    "enabled",
                                                    []
                                                  |),
                                                  [
                                                    Value.StructTuple
                                                      "revm_primitives::specification::SpecId::TANGERINE"
                                                      []
                                                  ]
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          UnOp.not (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "revm_interpreter::gas::Gas",
                                                                "record_cost",
                                                                []
                                                              |),
                                                              [
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| interpreter |),
                                                                  "revm_interpreter::interpreter::Interpreter",
                                                                  "gas"
                                                                |);
                                                                Value.Integer IntegerKind.U64 700
                                                              ]
                                                            |)
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          let~ _ :=
                                                            M.write (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| interpreter |),
                                                                "revm_interpreter::interpreter::Interpreter",
                                                                "instruction_result"
                                                              |),
                                                              Value.StructTuple
                                                                "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                                []
                                                            |) in
                                                          M.return_ (| Value.Tuple [] |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          UnOp.not (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "revm_interpreter::gas::Gas",
                                                                "record_cost",
                                                                []
                                                              |),
                                                              [
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| interpreter |),
                                                                  "revm_interpreter::interpreter::Interpreter",
                                                                  "gas"
                                                                |);
                                                                Value.Integer IntegerKind.U64 20
                                                              ]
                                                            |)
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          let~ _ :=
                                                            M.write (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| interpreter |),
                                                                "revm_interpreter::interpreter::Interpreter",
                                                                "instruction_result"
                                                              |),
                                                              Value.StructTuple
                                                                "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                                []
                                                            |) in
                                                          M.return_ (| Value.Tuple [] |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)))
                            ]
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_interpreter::interpreter::stack::Stack",
                                  "push",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| interpreter |),
                                    "revm_interpreter::interpreter::Interpreter",
                                    "stack"
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [],
                                      "from",
                                      [ Ty.path "usize" ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm_primitives::bytecode::Bytecode",
                                          "len",
                                          []
                                        |),
                                        [ code ]
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Ok",
                                      0
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Err",
                                      0
                                    |) in
                                  let e := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            M.read (| e |)
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_extcodesize :
      M.IsFunction "revm_interpreter::instructions::host::extcodesize" extcodesize.
    
    (*
    pub fn extcodehash<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        check!(interpreter, CONSTANTINOPLE);
        pop_address!(interpreter, address);
        let Some((code_hash, is_cold)) = host.code_hash(address) else {
            interpreter.instruction_result = InstructionResult::FatalExternalError;
            return;
        };
        if SPEC::enabled(BERLIN) {
            gas!(interpreter, warm_cold_cost(is_cold));
        } else if SPEC::enabled(ISTANBUL) {
            gas!(interpreter, 700);
        } else {
            gas!(interpreter, 400);
        }
        push_b256!(interpreter, code_hash);
    }
    *)
    Definition extcodehash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "revm_primitives::specification::Spec",
                                      SPEC,
                                      [],
                                      "enabled",
                                      []
                                    |),
                                    [
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::CONSTANTINOPLE"
                                        []
                                    ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::NotActivated"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ address :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "alloy_primitives::bits::address::Address",
                        "from_word",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::From",
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [],
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                []
                            ],
                            "from",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm_interpreter::interpreter::stack::Stack",
                                "pop_unsafe",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| interpreter |),
                                  "revm_interpreter::interpreter::Interpreter",
                                  "stack"
                                |)
                              ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "revm_interpreter::host::Host",
                        H,
                        [],
                        "code_hash",
                        []
                      |),
                      [ M.read (| host |); M.read (| address |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                        let code_hash := M.copy (| γ1_0 |) in
                        let is_cold := M.copy (| γ1_1 |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "revm_primitives::specification::Spec",
                                            SPEC,
                                            [],
                                            "enabled",
                                            []
                                          |),
                                          [
                                            Value.StructTuple
                                              "revm_primitives::specification::SpecId::BERLIN"
                                              []
                                          ]
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  UnOp.not (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "revm_interpreter::gas::Gas",
                                                        "record_cost",
                                                        []
                                                      |),
                                                      [
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| interpreter |),
                                                          "revm_interpreter::interpreter::Interpreter",
                                                          "gas"
                                                        |);
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "revm_interpreter::gas::calc::warm_cold_cost",
                                                            []
                                                          |),
                                                          [ M.read (| is_cold |) ]
                                                        |)
                                                      ]
                                                    |)
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  let~ _ :=
                                                    M.write (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "instruction_result"
                                                      |),
                                                      Value.StructTuple
                                                        "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                        []
                                                    |) in
                                                  M.return_ (| Value.Tuple [] |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "revm_primitives::specification::Spec",
                                                    SPEC,
                                                    [],
                                                    "enabled",
                                                    []
                                                  |),
                                                  [
                                                    Value.StructTuple
                                                      "revm_primitives::specification::SpecId::ISTANBUL"
                                                      []
                                                  ]
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          UnOp.not (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "revm_interpreter::gas::Gas",
                                                                "record_cost",
                                                                []
                                                              |),
                                                              [
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| interpreter |),
                                                                  "revm_interpreter::interpreter::Interpreter",
                                                                  "gas"
                                                                |);
                                                                Value.Integer IntegerKind.U64 700
                                                              ]
                                                            |)
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          let~ _ :=
                                                            M.write (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| interpreter |),
                                                                "revm_interpreter::interpreter::Interpreter",
                                                                "instruction_result"
                                                              |),
                                                              Value.StructTuple
                                                                "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                                []
                                                            |) in
                                                          M.return_ (| Value.Tuple [] |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let~ _ :=
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          UnOp.not (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "revm_interpreter::gas::Gas",
                                                                "record_cost",
                                                                []
                                                              |),
                                                              [
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| interpreter |),
                                                                  "revm_interpreter::interpreter::Interpreter",
                                                                  "gas"
                                                                |);
                                                                Value.Integer IntegerKind.U64 400
                                                              ]
                                                            |)
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          let~ _ :=
                                                            M.write (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| interpreter |),
                                                                "revm_interpreter::interpreter::Interpreter",
                                                                "instruction_result"
                                                              |),
                                                              Value.StructTuple
                                                                "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                                []
                                                            |) in
                                                          M.return_ (| Value.Tuple [] |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)))
                            ]
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_interpreter::interpreter::stack::Stack",
                                  "push_b256",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| interpreter |),
                                    "revm_interpreter::interpreter::Interpreter",
                                    "stack"
                                  |);
                                  M.read (| code_hash |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Ok",
                                      0
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::result::Result::Err",
                                      0
                                    |) in
                                  let e := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            M.read (| e |)
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_extcodehash :
      M.IsFunction "revm_interpreter::instructions::host::extcodehash" extcodehash.
    
    (*
    pub fn extcodecopy<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        pop_address!(interpreter, address);
        pop!(interpreter, memory_offset, code_offset, len_u256);
    
        let Some((code, is_cold)) = host.code(address) else {
            interpreter.instruction_result = InstructionResult::FatalExternalError;
            return;
        };
    
        let len = as_usize_or_fail!(interpreter, len_u256);
        gas_or_fail!(
            interpreter,
            gas::extcodecopy_cost(SPEC::SPEC_ID, len as u64, is_cold)
        );
        if len == 0 {
            return;
        }
        let memory_offset = as_usize_or_fail!(interpreter, memory_offset);
        let code_offset = min(as_usize_saturated!(code_offset), code.len());
        resize_memory!(interpreter, memory_offset, len);
    
        // Note: this can't panic because we resized memory to fit.
        interpreter
            .shared_memory
            .set_data(memory_offset, code_offset, len, &code.original_bytes());
    }
    *)
    Definition extcodecopy (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ address :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "alloy_primitives::bits::address::Address",
                        "from_word",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::From",
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [],
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                []
                            ],
                            "from",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm_interpreter::interpreter::stack::Stack",
                                "pop_unsafe",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| interpreter |),
                                  "revm_interpreter::interpreter::Interpreter",
                                  "stack"
                                |)
                              ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 3
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "pop3_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let γ0_2 := M.SubPointer.get_tuple_field (| γ, 2 |) in
                        let memory_offset := M.copy (| γ0_0 |) in
                        let code_offset := M.copy (| γ0_1 |) in
                        let len_u256 := M.copy (| γ0_2 |) in
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "revm_interpreter::host::Host",
                                H,
                                [],
                                "code",
                                []
                              |),
                              [ M.read (| host |); M.read (| address |) ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                let code := M.copy (| γ1_0 |) in
                                let is_cold := M.copy (| γ1_1 |) in
                                let~ len :=
                                  M.copy (|
                                    let~ x :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [],
                                            "as_limbs",
                                            []
                                          |),
                                          [ len_u256 ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    LogicalOp.or (|
                                                      LogicalOp.or (|
                                                        BinOp.ne (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 1
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |),
                                                        ltac:(M.monadic
                                                          (BinOp.ne (|
                                                            M.read (|
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| x |),
                                                                M.alloc (|
                                                                  Value.Integer IntegerKind.Usize 2
                                                                |)
                                                              |)
                                                            |),
                                                            Value.Integer IntegerKind.U64 0
                                                          |)))
                                                      |),
                                                      ltac:(M.monadic
                                                        (BinOp.ne (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 3
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |)))
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    let~ _ :=
                                                      M.write (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| interpreter |),
                                                          "revm_interpreter::interpreter::Interpreter",
                                                          "instruction_result"
                                                        |),
                                                        Value.StructTuple
                                                          "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                          []
                                                      |) in
                                                    M.return_ (| Value.Tuple [] |)
                                                  |)
                                                |)
                                              |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::TryFrom",
                                            Ty.path "usize",
                                            [ Ty.path "u64" ],
                                            "try_from",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_array_field (|
                                                M.read (| x |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                              |)
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::result::Result::Ok",
                                                0
                                              |) in
                                            let val := M.copy (| γ0_0 |) in
                                            val))
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "revm_interpreter::gas::calc::extcodecopy_cost",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.get_constant (|
                                              "revm_primitives::specification::Spec::SPEC_ID"
                                            |)
                                          |);
                                          M.rust_cast (M.read (| len |));
                                          M.read (| is_cold |)
                                        ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let gas_used := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "revm_interpreter::gas::Gas",
                                                              "record_cost",
                                                              []
                                                            |),
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| interpreter |),
                                                                "revm_interpreter::interpreter::Interpreter",
                                                                "gas"
                                                              |);
                                                              M.read (| gas_used |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        let~ _ :=
                                                          M.write (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| interpreter |),
                                                              "revm_interpreter::interpreter::Interpreter",
                                                              "instruction_result"
                                                            |),
                                                            Value.StructTuple
                                                              "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                              []
                                                          |) in
                                                        M.return_ (| Value.Tuple [] |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "instruction_result"
                                                    |),
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                      []
                                                  |) in
                                                M.return_ (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.eq (|
                                                  M.read (| len |),
                                                  Value.Integer IntegerKind.Usize 0
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (| M.return_ (| Value.Tuple [] |) |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let~ memory_offset :=
                                  M.copy (|
                                    let~ x :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [],
                                            "as_limbs",
                                            []
                                          |),
                                          [ memory_offset ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    LogicalOp.or (|
                                                      LogicalOp.or (|
                                                        BinOp.ne (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 1
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |),
                                                        ltac:(M.monadic
                                                          (BinOp.ne (|
                                                            M.read (|
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| x |),
                                                                M.alloc (|
                                                                  Value.Integer IntegerKind.Usize 2
                                                                |)
                                                              |)
                                                            |),
                                                            Value.Integer IntegerKind.U64 0
                                                          |)))
                                                      |),
                                                      ltac:(M.monadic
                                                        (BinOp.ne (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 3
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |)))
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    let~ _ :=
                                                      M.write (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| interpreter |),
                                                          "revm_interpreter::interpreter::Interpreter",
                                                          "instruction_result"
                                                        |),
                                                        Value.StructTuple
                                                          "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                          []
                                                      |) in
                                                    M.return_ (| Value.Tuple [] |)
                                                  |)
                                                |)
                                              |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::TryFrom",
                                            Ty.path "usize",
                                            [ Ty.path "u64" ],
                                            "try_from",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_array_field (|
                                                M.read (| x |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                              |)
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::result::Result::Ok",
                                                0
                                              |) in
                                            let val := M.copy (| γ0_0 |) in
                                            val))
                                      ]
                                    |)
                                  |) in
                                let~ code_offset :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (| "core::cmp::min", [ Ty.path "usize" ] |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              []
                                              [
                                                Ty.path "usize";
                                                Ty.path "core::num::error::TryFromIntError"
                                              ],
                                            "unwrap_or",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::convert::TryFrom",
                                                Ty.path "usize",
                                                [ Ty.path "u64" ],
                                                "try_from",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  let~ x :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "ruint::Uint")
                                                            [
                                                              Value.Integer IntegerKind.Usize 256;
                                                              Value.Integer IntegerKind.Usize 4
                                                            ]
                                                            [],
                                                          "as_limbs",
                                                          []
                                                        |),
                                                        [ code_offset ]
                                                      |)
                                                    |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                LogicalOp.and (|
                                                                  LogicalOp.and (|
                                                                    BinOp.eq (|
                                                                      M.read (|
                                                                        M.SubPointer.get_array_field (|
                                                                          M.read (| x |),
                                                                          M.alloc (|
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              1
                                                                          |)
                                                                        |)
                                                                      |),
                                                                      Value.Integer
                                                                        IntegerKind.U64
                                                                        0
                                                                    |),
                                                                    ltac:(M.monadic
                                                                      (BinOp.eq (|
                                                                        M.read (|
                                                                          M.SubPointer.get_array_field (|
                                                                            M.read (| x |),
                                                                            M.alloc (|
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                2
                                                                            |)
                                                                          |)
                                                                        |),
                                                                        Value.Integer
                                                                          IntegerKind.U64
                                                                          0
                                                                      |)))
                                                                  |),
                                                                  ltac:(M.monadic
                                                                    (BinOp.eq (|
                                                                      M.read (|
                                                                        M.SubPointer.get_array_field (|
                                                                          M.read (| x |),
                                                                          M.alloc (|
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              3
                                                                          |)
                                                                        |)
                                                                      |),
                                                                      Value.Integer
                                                                        IntegerKind.U64
                                                                        0
                                                                    |)))
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          M.SubPointer.get_array_field (|
                                                            M.read (| x |),
                                                            M.alloc (|
                                                              Value.Integer IntegerKind.Usize 0
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.get_constant (| "core::num::MAX" |)))
                                                    ]
                                                  |)
                                                |)
                                              ]
                                            |);
                                            M.read (| M.get_constant (| "core::num::MAX" |) |)
                                          ]
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_primitives::bytecode::Bytecode",
                                            "len",
                                            []
                                          |),
                                          [ code ]
                                        |)
                                      ]
                                    |)
                                  |) in
                                let~ new_size :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "usize",
                                        "saturating_add",
                                        []
                                      |),
                                      [ M.read (| memory_offset |); M.read (| len |) ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.gt (|
                                                  M.read (| new_size |),
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                                      "len",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "shared_memory"
                                                      |)
                                                    ]
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "revm_interpreter::interpreter::resize_memory",
                                                              []
                                                            |),
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| interpreter |),
                                                                "revm_interpreter::interpreter::Interpreter",
                                                                "shared_memory"
                                                              |);
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| interpreter |),
                                                                "revm_interpreter::interpreter::Interpreter",
                                                                "gas"
                                                              |);
                                                              M.read (| new_size |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        let~ _ :=
                                                          M.write (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| interpreter |),
                                                              "revm_interpreter::interpreter::Interpreter",
                                                              "instruction_result"
                                                            |),
                                                            Value.StructTuple
                                                              "revm_interpreter::instruction_result::InstructionResult::MemoryOOG"
                                                              []
                                                          |) in
                                                        M.return_ (| Value.Tuple [] |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path
                                          "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                        "set_data",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| interpreter |),
                                          "revm_interpreter::interpreter::Interpreter",
                                          "shared_memory"
                                        |);
                                        M.read (| memory_offset |);
                                        M.read (| code_offset |);
                                        M.read (| len |);
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::deref::Deref",
                                            Ty.path "bytes::bytes::Bytes",
                                            [],
                                            "deref",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::deref::Deref",
                                                Ty.path "alloy_primitives::bytes_::Bytes",
                                                [],
                                                "deref",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "revm_primitives::bytecode::Bytecode",
                                                      "original_bytes",
                                                      []
                                                    |),
                                                    [ code ]
                                                  |)
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_extcodecopy :
      M.IsFunction "revm_interpreter::instructions::host::extcodecopy" extcodecopy.
    
    (*
    pub fn blockhash<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        gas!(interpreter, gas::BLOCKHASH);
        pop_top!(interpreter, number);
    
        let block_number = host.env().block.number;
    
        match block_number.checked_sub( *number) {
            Some(diff) if !diff.is_zero() => {
                let diff = as_usize_saturated!(diff);
    
                // blockhash should push zero if number is same as current block number.
                if SPEC::enabled(PRAGUE) && diff <= BLOCKHASH_SERVE_WINDOW {
                    let value = sload!(
                        interpreter,
                        host,
                        BLOCKHASH_STORAGE_ADDRESS,
                        number.wrapping_rem(U256::from(BLOCKHASH_SERVE_WINDOW))
                    );
                    *number = value;
                    return;
                } else if diff <= BLOCK_HASH_HISTORY {
                    let Some(hash) = host.block_hash( *number) else {
                        interpreter.instruction_result = InstructionResult::FatalExternalError;
                        return;
                    };
                    *number = U256::from_be_bytes(hash.0);
                    return;
                }
            }
            _ => {
                // If blockhash is requested for the current block, the hash should be 0, so we fall
                // through.
            }
        }
    
        *number = U256::ZERO;
    }
    *)
    Definition blockhash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::gas::Gas",
                                      "record_cost",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "gas"
                                      |);
                                      M.read (|
                                        M.get_constant (|
                                          "revm_interpreter::gas::constants::BLOCKHASH"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ number :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "top_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |) in
                let~ block_number :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        M.call_closure (|
                          M.get_trait_method (| "revm_interpreter::host::Host", H, [], "env", [] |),
                          [ M.read (| host |) ]
                        |),
                        "revm_primitives::env::Env",
                        "block"
                      |),
                      "revm_primitives::env::BlockEnv",
                      "number"
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [],
                          "checked_sub",
                          []
                        |),
                        [ M.read (| block_number |); M.read (| M.read (| number |) |) ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let diff := M.copy (| γ0_0 |) in
                          let γ :=
                            M.alloc (|
                              UnOp.not (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "is_zero",
                                    []
                                  |),
                                  [ diff ]
                                |)
                              |)
                            |) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ diff :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::result::Result")
                                    []
                                    [ Ty.path "usize"; Ty.path "core::num::error::TryFromIntError"
                                    ],
                                  "unwrap_or",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::convert::TryFrom",
                                      Ty.path "usize",
                                      [ Ty.path "u64" ],
                                      "try_from",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        let~ x :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [],
                                                "as_limbs",
                                                []
                                              |),
                                              [ diff ]
                                            |)
                                          |) in
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      LogicalOp.and (|
                                                        LogicalOp.and (|
                                                          BinOp.eq (|
                                                            M.read (|
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| x |),
                                                                M.alloc (|
                                                                  Value.Integer IntegerKind.Usize 1
                                                                |)
                                                              |)
                                                            |),
                                                            Value.Integer IntegerKind.U64 0
                                                          |),
                                                          ltac:(M.monadic
                                                            (BinOp.eq (|
                                                              M.read (|
                                                                M.SubPointer.get_array_field (|
                                                                  M.read (| x |),
                                                                  M.alloc (|
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      2
                                                                  |)
                                                                |)
                                                              |),
                                                              Value.Integer IntegerKind.U64 0
                                                            |)))
                                                        |),
                                                        ltac:(M.monadic
                                                          (BinOp.eq (|
                                                            M.read (|
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| x |),
                                                                M.alloc (|
                                                                  Value.Integer IntegerKind.Usize 3
                                                                |)
                                                              |)
                                                            |),
                                                            Value.Integer IntegerKind.U64 0
                                                          |)))
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.SubPointer.get_array_field (|
                                                  M.read (| x |),
                                                  M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.get_constant (| "core::num::MAX" |)))
                                          ]
                                        |)
                                      |)
                                    ]
                                  |);
                                  M.read (| M.get_constant (| "core::num::MAX" |) |)
                                ]
                              |)
                            |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        LogicalOp.and (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "revm_primitives::specification::Spec",
                                              SPEC,
                                              [],
                                              "enabled",
                                              []
                                            |),
                                            [
                                              Value.StructTuple
                                                "revm_primitives::specification::SpecId::PRAGUE"
                                                []
                                            ]
                                          |),
                                          ltac:(M.monadic
                                            (BinOp.le (|
                                              M.read (| diff |),
                                              M.read (|
                                                M.get_constant (|
                                                  "revm_primitives::constants::BLOCKHASH_SERVE_WINDOW"
                                                |)
                                              |)
                                            |)))
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ value :=
                                          M.copy (|
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "revm_interpreter::host::Host",
                                                    H,
                                                    [],
                                                    "sload",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| host |);
                                                    M.read (|
                                                      M.get_constant (|
                                                        "revm_primitives::constants::BLOCKHASH_STORAGE_ADDRESS"
                                                      |)
                                                    |);
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "ruint::Uint")
                                                          [
                                                            Value.Integer IntegerKind.Usize 256;
                                                            Value.Integer IntegerKind.Usize 4
                                                          ]
                                                          [],
                                                        "wrapping_rem",
                                                        []
                                                      |),
                                                      [
                                                        M.read (| M.read (| number |) |);
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "ruint::Uint")
                                                              [
                                                                Value.Integer IntegerKind.Usize 256;
                                                                Value.Integer IntegerKind.Usize 4
                                                              ]
                                                              [],
                                                            "from",
                                                            [ Ty.path "usize" ]
                                                          |),
                                                          [
                                                            M.read (|
                                                              M.get_constant (|
                                                                "revm_primitives::constants::BLOCKHASH_SERVE_WINDOW"
                                                              |)
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::option::Option::Some",
                                                        0
                                                      |) in
                                                    let γ1_0 :=
                                                      M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                                    let γ1_1 :=
                                                      M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                                    let value := M.copy (| γ1_0 |) in
                                                    let is_cold := M.copy (| γ1_1 |) in
                                                    let~ _ :=
                                                      M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (|
                                                                    UnOp.not (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.path
                                                                            "revm_interpreter::gas::Gas",
                                                                          "record_cost",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.SubPointer.get_struct_record_field (|
                                                                            M.read (|
                                                                              interpreter
                                                                            |),
                                                                            "revm_interpreter::interpreter::Interpreter",
                                                                            "gas"
                                                                          |);
                                                                          M.call_closure (|
                                                                            M.get_function (|
                                                                              "revm_interpreter::gas::calc::sload_cost",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.read (|
                                                                                M.get_constant (|
                                                                                  "revm_primitives::specification::Spec::SPEC_ID"
                                                                                |)
                                                                              |);
                                                                              M.read (| is_cold |)
                                                                            ]
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |)
                                                                  |)) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              M.alloc (|
                                                                M.never_to_any (|
                                                                  M.read (|
                                                                    let~ _ :=
                                                                      M.write (|
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          M.read (| interpreter |),
                                                                          "revm_interpreter::interpreter::Interpreter",
                                                                          "instruction_result"
                                                                        |),
                                                                        Value.StructTuple
                                                                          "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                                          []
                                                                      |) in
                                                                    M.return_ (| Value.Tuple [] |)
                                                                  |)
                                                                |)
                                                              |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |) in
                                                    value))
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.write (| M.read (| number |), M.read (| value |) |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.le (|
                                                  M.read (| diff |),
                                                  M.read (|
                                                    M.get_constant (|
                                                      "revm_primitives::constants::BLOCK_HASH_HISTORY"
                                                    |)
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "revm_interpreter::host::Host",
                                                        H,
                                                        [],
                                                        "block_hash",
                                                        []
                                                      |),
                                                      [
                                                        M.read (| host |);
                                                        M.read (| M.read (| number |) |)
                                                      ]
                                                    |)
                                                  |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "core::option::Option::Some",
                                                            0
                                                          |) in
                                                        let hash := M.copy (| γ0_0 |) in
                                                        let~ _ :=
                                                          M.write (|
                                                            M.read (| number |),
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "ruint::Uint")
                                                                  [
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      256;
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      4
                                                                  ]
                                                                  [],
                                                                "from_be_bytes",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  M.SubPointer.get_struct_tuple_field (|
                                                                    hash,
                                                                    "alloy_primitives::bits::fixed::FixedBytes",
                                                                    0
                                                                  |)
                                                                |)
                                                              ]
                                                            |)
                                                          |) in
                                                        M.return_ (| Value.Tuple [] |)))
                                                  ]
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.write (|
                    M.read (| number |),
                    M.read (| M.get_constant (| "ruint::ZERO" |) |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_blockhash :
      M.IsFunction "revm_interpreter::instructions::host::blockhash" blockhash.
    
    (*
    pub fn sload<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        pop_top!(interpreter, index);
        let value = sload!(
            interpreter,
            host,
            interpreter.contract.target_address,
            *index
        );
        *index = value;
    }
    *)
    Definition sload (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ index :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "top_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |) in
                let~ value :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "revm_interpreter::host::Host",
                            H,
                            [],
                            "sload",
                            []
                          |),
                          [
                            M.read (| host |);
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| interpreter |),
                                  "revm_interpreter::interpreter::Interpreter",
                                  "contract"
                                |),
                                "revm_interpreter::interpreter::contract::Contract",
                                "target_address"
                              |)
                            |);
                            M.read (| M.read (| index |) |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                            let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                            let value := M.copy (| γ1_0 |) in
                            let is_cold := M.copy (| γ1_1 |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            UnOp.not (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "revm_interpreter::gas::Gas",
                                                  "record_cost",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| interpreter |),
                                                    "revm_interpreter::interpreter::Interpreter",
                                                    "gas"
                                                  |);
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "revm_interpreter::gas::calc::sload_cost",
                                                      []
                                                    |),
                                                    [
                                                      M.read (|
                                                        M.get_constant (|
                                                          "revm_primitives::specification::Spec::SPEC_ID"
                                                        |)
                                                      |);
                                                      M.read (| is_cold |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| interpreter |),
                                                  "revm_interpreter::interpreter::Interpreter",
                                                  "instruction_result"
                                                |),
                                                Value.StructTuple
                                                  "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                  []
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            value))
                      ]
                    |)
                  |) in
                let~ _ := M.write (| M.read (| index |), M.read (| value |) |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_sload : M.IsFunction "revm_interpreter::instructions::host::sload" sload.
    
    (*
    pub fn sstore<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        require_non_staticcall!(interpreter);
    
        pop!(interpreter, index, value);
        let Some(SStoreResult {
            original_value: original,
            present_value: old,
            new_value: new,
            is_cold,
        }) = host.sstore(interpreter.contract.target_address, index, value)
        else {
            interpreter.instruction_result = InstructionResult::FatalExternalError;
            return;
        };
        gas_or_fail!(interpreter, {
            let remaining_gas = interpreter.gas.remaining();
            gas::sstore_cost(SPEC::SPEC_ID, original, old, new, remaining_gas, is_cold)
        });
        refund!(
            interpreter,
            gas::sstore_refund(SPEC::SPEC_ID, original, old, new)
        );
    }
    *)
    Definition sstore (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.SubPointer.get_struct_record_field (|
                                M.read (| interpreter |),
                                "revm_interpreter::interpreter::Interpreter",
                                "is_static"
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 2
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "pop2_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let index := M.copy (| γ0_0 |) in
                        let value := M.copy (| γ0_1 |) in
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "revm_interpreter::host::Host",
                                H,
                                [],
                                "sstore",
                                []
                              |),
                              [
                                M.read (| host |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "contract"
                                    |),
                                    "revm_interpreter::interpreter::contract::Contract",
                                    "target_address"
                                  |)
                                |);
                                M.read (| index |);
                                M.read (| value |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let γ1_0 :=
                                  M.SubPointer.get_struct_record_field (|
                                    γ0_0,
                                    "revm_interpreter::host::SStoreResult",
                                    "original_value"
                                  |) in
                                let γ1_1 :=
                                  M.SubPointer.get_struct_record_field (|
                                    γ0_0,
                                    "revm_interpreter::host::SStoreResult",
                                    "present_value"
                                  |) in
                                let γ1_2 :=
                                  M.SubPointer.get_struct_record_field (|
                                    γ0_0,
                                    "revm_interpreter::host::SStoreResult",
                                    "new_value"
                                  |) in
                                let γ1_3 :=
                                  M.SubPointer.get_struct_record_field (|
                                    γ0_0,
                                    "revm_interpreter::host::SStoreResult",
                                    "is_cold"
                                  |) in
                                let original := M.copy (| γ1_0 |) in
                                let old := M.copy (| γ1_1 |) in
                                let new := M.copy (| γ1_2 |) in
                                let is_cold := M.copy (| γ1_3 |) in
                                let~ _ :=
                                  M.match_operator (|
                                    let~ remaining_gas :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_interpreter::gas::Gas",
                                            "remaining",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "gas"
                                            |)
                                          ]
                                        |)
                                      |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "revm_interpreter::gas::calc::sstore_cost",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.get_constant (|
                                              "revm_primitives::specification::Spec::SPEC_ID"
                                            |)
                                          |);
                                          M.read (| original |);
                                          M.read (| old |);
                                          M.read (| new |);
                                          M.read (| remaining_gas |);
                                          M.read (| is_cold |)
                                        ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let gas_used := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "revm_interpreter::gas::Gas",
                                                              "record_cost",
                                                              []
                                                            |),
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| interpreter |),
                                                                "revm_interpreter::interpreter::Interpreter",
                                                                "gas"
                                                              |);
                                                              M.read (| gas_used |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        let~ _ :=
                                                          M.write (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| interpreter |),
                                                              "revm_interpreter::interpreter::Interpreter",
                                                              "instruction_result"
                                                            |),
                                                            Value.StructTuple
                                                              "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                              []
                                                          |) in
                                                        M.return_ (| Value.Tuple [] |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "instruction_result"
                                                    |),
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                      []
                                                  |) in
                                                M.return_ (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_interpreter::gas::Gas",
                                        "record_refund",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| interpreter |),
                                          "revm_interpreter::interpreter::Interpreter",
                                          "gas"
                                        |);
                                        M.call_closure (|
                                          M.get_function (|
                                            "revm_interpreter::gas::calc::sstore_refund",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.get_constant (|
                                                "revm_primitives::specification::Spec::SPEC_ID"
                                              |)
                                            |);
                                            M.read (| original |);
                                            M.read (| old |);
                                            M.read (| new |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_sstore : M.IsFunction "revm_interpreter::instructions::host::sstore" sstore.
    
    (*
    pub fn tstore<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        check!(interpreter, CANCUN);
        require_non_staticcall!(interpreter);
        gas!(interpreter, gas::WARM_STORAGE_READ_COST);
    
        pop!(interpreter, index, value);
    
        host.tstore(interpreter.contract.target_address, index, value);
    }
    *)
    Definition tstore (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "revm_primitives::specification::Spec",
                                      SPEC,
                                      [],
                                      "enabled",
                                      []
                                    |),
                                    [
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::CANCUN"
                                        []
                                    ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::NotActivated"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.SubPointer.get_struct_record_field (|
                                M.read (| interpreter |),
                                "revm_interpreter::interpreter::Interpreter",
                                "is_static"
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::gas::Gas",
                                      "record_cost",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "gas"
                                      |);
                                      M.read (|
                                        M.get_constant (|
                                          "revm_interpreter::gas::constants::WARM_STORAGE_READ_COST"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 2
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "pop2_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let index := M.copy (| γ0_0 |) in
                        let value := M.copy (| γ0_1 |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "revm_interpreter::host::Host",
                                H,
                                [],
                                "tstore",
                                []
                              |),
                              [
                                M.read (| host |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "contract"
                                    |),
                                    "revm_interpreter::interpreter::contract::Contract",
                                    "target_address"
                                  |)
                                |);
                                M.read (| index |);
                                M.read (| value |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_tstore : M.IsFunction "revm_interpreter::instructions::host::tstore" tstore.
    
    (*
    pub fn tload<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        check!(interpreter, CANCUN);
        gas!(interpreter, gas::WARM_STORAGE_READ_COST);
    
        pop_top!(interpreter, index);
    
        *index = host.tload(interpreter.contract.target_address, *index);
    }
    *)
    Definition tload (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "revm_primitives::specification::Spec",
                                      SPEC,
                                      [],
                                      "enabled",
                                      []
                                    |),
                                    [
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::CANCUN"
                                        []
                                    ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::NotActivated"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::gas::Gas",
                                      "record_cost",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "gas"
                                      |);
                                      M.read (|
                                        M.get_constant (|
                                          "revm_interpreter::gas::constants::WARM_STORAGE_READ_COST"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ index :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "top_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.read (| index |),
                    M.call_closure (|
                      M.get_trait_method (| "revm_interpreter::host::Host", H, [], "tload", [] |),
                      [
                        M.read (| host |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| interpreter |),
                              "revm_interpreter::interpreter::Interpreter",
                              "contract"
                            |),
                            "revm_interpreter::interpreter::contract::Contract",
                            "target_address"
                          |)
                        |);
                        M.read (| M.read (| index |) |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_tload : M.IsFunction "revm_interpreter::instructions::host::tload" tload.
    
    (*
    pub fn log<const N: usize, H: Host + ?Sized>(interpreter: &mut Interpreter, host: &mut H) {
        require_non_staticcall!(interpreter);
    
        pop!(interpreter, offset, len);
        let len = as_usize_or_fail!(interpreter, len);
        gas_or_fail!(interpreter, gas::log_cost(N as u8, len as u64));
        let data = if len == 0 {
            Bytes::new()
        } else {
            let offset = as_usize_or_fail!(interpreter, offset);
            resize_memory!(interpreter, offset, len);
            Bytes::copy_from_slice(interpreter.shared_memory.slice(offset, len))
        };
    
        if interpreter.stack.len() < N {
            interpreter.instruction_result = InstructionResult::StackUnderflow;
            return;
        }
    
        let mut topics = Vec::with_capacity(N);
        for _ in 0..N {
            // SAFETY: stack bounds already checked few lines above
            topics.push(B256::from(unsafe { interpreter.stack.pop_unsafe() }));
        }
    
        let log = Log {
            address: interpreter.contract.target_address,
            data: LogData::new(topics, data).expect("LogData should have <=4 topics"),
        };
    
        host.log(log);
    }
    *)
    Definition log (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [ N ], [ H ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.SubPointer.get_struct_record_field (|
                                M.read (| interpreter |),
                                "revm_interpreter::interpreter::Interpreter",
                                "is_static"
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 2
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "pop2_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let offset := M.copy (| γ0_0 |) in
                        let len := M.copy (| γ0_1 |) in
                        let~ len :=
                          M.copy (|
                            let~ x :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "as_limbs",
                                    []
                                  |),
                                  [ len ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            LogicalOp.or (|
                                              LogicalOp.or (|
                                                BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.ne (|
                                                    M.read (|
                                                      M.SubPointer.get_array_field (|
                                                        M.read (| x |),
                                                        M.alloc (|
                                                          Value.Integer IntegerKind.Usize 2
                                                        |)
                                                      |)
                                                    |),
                                                    Value.Integer IntegerKind.U64 0
                                                  |)))
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 3
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |)))
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| interpreter |),
                                                  "revm_interpreter::interpreter::Interpreter",
                                                  "instruction_result"
                                                |),
                                                Value.StructTuple
                                                  "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                  []
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::TryFrom",
                                    Ty.path "usize",
                                    [ Ty.path "u64" ],
                                    "try_from",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_array_field (|
                                        M.read (| x |),
                                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                      |)
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::result::Result::Ok",
                                        0
                                      |) in
                                    let val := M.copy (| γ0_0 |) in
                                    val))
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (| "revm_interpreter::gas::calc::log_cost", [] |),
                                [
                                  M.rust_cast
                                    (M.read (|
                                      M.get_constant (|
                                        "revm_interpreter::instructions::host::log::N"
                                      |)
                                    |));
                                  M.rust_cast (M.read (| len |))
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let gas_used := M.copy (| γ0_0 |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "revm_interpreter::gas::Gas",
                                                      "record_cost",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "gas"
                                                      |);
                                                      M.read (| gas_used |)
                                                    ]
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "instruction_result"
                                                    |),
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                      []
                                                  |) in
                                                M.return_ (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                              []
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |) in
                        let~ data :=
                          M.copy (|
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.eq (|
                                            M.read (| len |),
                                            Value.Integer IntegerKind.Usize 0
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "alloy_primitives::bytes_::Bytes",
                                          "new",
                                          []
                                        |),
                                        []
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let~ offset :=
                                      M.copy (|
                                        let~ x :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [],
                                                "as_limbs",
                                                []
                                              |),
                                              [ offset ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        LogicalOp.or (|
                                                          LogicalOp.or (|
                                                            BinOp.ne (|
                                                              M.read (|
                                                                M.SubPointer.get_array_field (|
                                                                  M.read (| x |),
                                                                  M.alloc (|
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      1
                                                                  |)
                                                                |)
                                                              |),
                                                              Value.Integer IntegerKind.U64 0
                                                            |),
                                                            ltac:(M.monadic
                                                              (BinOp.ne (|
                                                                M.read (|
                                                                  M.SubPointer.get_array_field (|
                                                                    M.read (| x |),
                                                                    M.alloc (|
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        2
                                                                    |)
                                                                  |)
                                                                |),
                                                                Value.Integer IntegerKind.U64 0
                                                              |)))
                                                          |),
                                                          ltac:(M.monadic
                                                            (BinOp.ne (|
                                                              M.read (|
                                                                M.SubPointer.get_array_field (|
                                                                  M.read (| x |),
                                                                  M.alloc (|
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      3
                                                                  |)
                                                                |)
                                                              |),
                                                              Value.Integer IntegerKind.U64 0
                                                            |)))
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        let~ _ :=
                                                          M.write (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| interpreter |),
                                                              "revm_interpreter::interpreter::Interpreter",
                                                              "instruction_result"
                                                            |),
                                                            Value.StructTuple
                                                              "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                              []
                                                          |) in
                                                        M.return_ (| Value.Tuple [] |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::convert::TryFrom",
                                                Ty.path "usize",
                                                [ Ty.path "u64" ],
                                                "try_from",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| x |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ0_0 :=
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    γ,
                                                    "core::result::Result::Ok",
                                                    0
                                                  |) in
                                                let val := M.copy (| γ0_0 |) in
                                                val))
                                          ]
                                        |)
                                      |) in
                                    let~ new_size :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "usize",
                                            "saturating_add",
                                            []
                                          |),
                                          [ M.read (| offset |); M.read (| len |) ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    BinOp.gt (|
                                                      M.read (| new_size |),
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                                          "len",
                                                          []
                                                        |),
                                                        [
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| interpreter |),
                                                            "revm_interpreter::interpreter::Interpreter",
                                                            "shared_memory"
                                                          |)
                                                        ]
                                                      |)
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            UnOp.not (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "revm_interpreter::interpreter::resize_memory",
                                                                  []
                                                                |),
                                                                [
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| interpreter |),
                                                                    "revm_interpreter::interpreter::Interpreter",
                                                                    "shared_memory"
                                                                  |);
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| interpreter |),
                                                                    "revm_interpreter::interpreter::Interpreter",
                                                                    "gas"
                                                                  |);
                                                                  M.read (| new_size |)
                                                                ]
                                                              |)
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            let~ _ :=
                                                              M.write (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| interpreter |),
                                                                  "revm_interpreter::interpreter::Interpreter",
                                                                  "instruction_result"
                                                                |),
                                                                Value.StructTuple
                                                                  "revm_interpreter::instruction_result::InstructionResult::MemoryOOG"
                                                                  []
                                                              |) in
                                                            M.return_ (| Value.Tuple [] |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "alloy_primitives::bytes_::Bytes",
                                          "copy_from_slice",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                              "slice",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| interpreter |),
                                                "revm_interpreter::interpreter::Interpreter",
                                                "shared_memory"
                                              |);
                                              M.read (| offset |);
                                              M.read (| len |)
                                            ]
                                          |)
                                        ]
                                      |)
                                    |)))
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.lt (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "revm_interpreter::interpreter::stack::Stack",
                                              "len",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| interpreter |),
                                                "revm_interpreter::interpreter::Interpreter",
                                                "stack"
                                              |)
                                            ]
                                          |),
                                          M.read (|
                                            M.get_constant (|
                                              "revm_interpreter::instructions::host::log::N"
                                            |)
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                              []
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ topics :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                      [ Value.Integer IntegerKind.Usize 32 ]
                                      [];
                                    Ty.path "alloc::alloc::Global"
                                  ],
                                "with_capacity",
                                []
                              |),
                              [
                                M.read (|
                                  M.get_constant (|
                                    "revm_interpreter::instructions::host::log::N"
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.use
                            (M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::collect::IntoIterator",
                                    Ty.apply
                                      (Ty.path "core::ops::range::Range")
                                      []
                                      [ Ty.path "usize" ],
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [
                                    Value.StructRecord
                                      "core::ops::range::Range"
                                      [
                                        ("start", Value.Integer IntegerKind.Usize 0);
                                        ("end_",
                                          M.read (|
                                            M.get_constant (|
                                              "revm_interpreter::instructions::host::log::N"
                                            |)
                                          |))
                                      ]
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.loop (|
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::iter::traits::iterator::Iterator",
                                                  Ty.apply
                                                    (Ty.path "core::ops::range::Range")
                                                    []
                                                    [ Ty.path "usize" ],
                                                  [],
                                                  "next",
                                                  []
                                                |),
                                                [ iter ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_struct_tuple (|
                                                      γ,
                                                      "core::option::Option::None"
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (| M.read (| M.break (||) |) |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let~ _ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "alloc::vec::Vec")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "alloy_primitives::bits::fixed::FixedBytes")
                                                                [ Value.Integer IntegerKind.Usize 32
                                                                ]
                                                                [];
                                                              Ty.path "alloc::alloc::Global"
                                                            ],
                                                          "push",
                                                          []
                                                        |),
                                                        [
                                                          topics;
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::convert::From",
                                                              Ty.apply
                                                                (Ty.path
                                                                  "alloy_primitives::bits::fixed::FixedBytes")
                                                                [ Value.Integer IntegerKind.Usize 32
                                                                ]
                                                                [],
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "ruint::Uint")
                                                                  [
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      256;
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      4
                                                                  ]
                                                                  []
                                                              ],
                                                              "from",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path
                                                                    "revm_interpreter::interpreter::stack::Stack",
                                                                  "pop_unsafe",
                                                                  []
                                                                |),
                                                                [
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| interpreter |),
                                                                    "revm_interpreter::interpreter::Interpreter",
                                                                    "stack"
                                                                  |)
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                    |)))
                              ]
                            |)) in
                        let~ log :=
                          M.alloc (|
                            Value.StructRecord
                              "alloy_primitives::log::Log"
                              [
                                ("address",
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "contract"
                                      |),
                                      "revm_interpreter::interpreter::contract::Contract",
                                      "target_address"
                                    |)
                                  |));
                                ("data",
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "alloy_primitives::log::LogData" ],
                                      "expect",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "alloy_primitives::log::LogData",
                                          "new",
                                          []
                                        |),
                                        [ M.read (| topics |); M.read (| data |) ]
                                      |);
                                      M.read (| Value.String "LogData should have <=4 topics" |)
                                    ]
                                  |))
                              ]
                          |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "revm_interpreter::host::Host",
                                H,
                                [],
                                "log",
                                []
                              |),
                              [ M.read (| host |); M.read (| log |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_log : M.IsFunction "revm_interpreter::instructions::host::log" log.
    
    (*
    pub fn selfdestruct<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        require_non_staticcall!(interpreter);
        pop_address!(interpreter, target);
    
        let Some(res) = host.selfdestruct(interpreter.contract.target_address, target) else {
            interpreter.instruction_result = InstructionResult::FatalExternalError;
            return;
        };
    
        // EIP-3529: Reduction in refunds
        if !SPEC::enabled(LONDON) && !res.previously_destroyed {
            refund!(interpreter, gas::SELFDESTRUCT)
        }
        gas!(interpreter, gas::selfdestruct_cost(SPEC::SPEC_ID, res));
    
        interpreter.instruction_result = InstructionResult::SelfDestruct;
    }
    *)
    Definition selfdestruct (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H; SPEC ], [ interpreter; host ] =>
        ltac:(M.monadic
          (let interpreter := M.alloc (| interpreter |) in
          let host := M.alloc (| host |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.SubPointer.get_struct_record_field (|
                                M.read (| interpreter |),
                                "revm_interpreter::interpreter::Interpreter",
                                "is_static"
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StateChangeDuringStaticCall"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ target :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "alloy_primitives::bits::address::Address",
                        "from_word",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::From",
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [],
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                []
                            ],
                            "from",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm_interpreter::interpreter::stack::Stack",
                                "pop_unsafe",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| interpreter |),
                                  "revm_interpreter::interpreter::Interpreter",
                                  "stack"
                                |)
                              ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "revm_interpreter::host::Host",
                        H,
                        [],
                        "selfdestruct",
                        []
                      |),
                      [
                        M.read (| host |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| interpreter |),
                              "revm_interpreter::interpreter::Interpreter",
                              "contract"
                            |),
                            "revm_interpreter::interpreter::contract::Contract",
                            "target_address"
                          |)
                        |);
                        M.read (| target |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let res := M.copy (| γ0_0 |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        LogicalOp.and (|
                                          UnOp.not (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "revm_primitives::specification::Spec",
                                                SPEC,
                                                [],
                                                "enabled",
                                                []
                                              |),
                                              [
                                                Value.StructTuple
                                                  "revm_primitives::specification::SpecId::LONDON"
                                                  []
                                              ]
                                            |)
                                          |),
                                          ltac:(M.monadic
                                            (UnOp.not (|
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  res,
                                                  "revm_interpreter::host::SelfDestructResult",
                                                  "previously_destroyed"
                                                |)
                                              |)
                                            |)))
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_interpreter::gas::Gas",
                                        "record_refund",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| interpreter |),
                                          "revm_interpreter::interpreter::Interpreter",
                                          "gas"
                                        |);
                                        M.read (|
                                          M.get_constant (|
                                            "revm_interpreter::gas::constants::SELFDESTRUCT"
                                          |)
                                        |)
                                      ]
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "revm_interpreter::gas::Gas",
                                              "record_cost",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| interpreter |),
                                                "revm_interpreter::interpreter::Interpreter",
                                                "gas"
                                              |);
                                              M.call_closure (|
                                                M.get_function (|
                                                  "revm_interpreter::gas::calc::selfdestruct_cost",
                                                  []
                                                |),
                                                [
                                                  M.read (|
                                                    M.get_constant (|
                                                      "revm_primitives::specification::Spec::SPEC_ID"
                                                    |)
                                                  |);
                                                  M.read (| res |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                              []
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| interpreter |),
                              "revm_interpreter::interpreter::Interpreter",
                              "instruction_result"
                            |),
                            Value.StructTuple
                              "revm_interpreter::instruction_result::InstructionResult::SelfDestruct"
                              []
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_selfdestruct :
      M.IsFunction "revm_interpreter::instructions::host::selfdestruct" selfdestruct.
  End host.
End instructions.
