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

Module instructions.
  Module host_env.
    (*
    pub fn chainid<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        check!(interpreter, ISTANBUL);
        gas!(interpreter, gas::BASE);
        push!(interpreter, U256::from(host.env().cfg.chain_id));
    }
    *)
    Definition chainid (ε : 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::BASE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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.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 "u64" ]
                            |),
                            [
                              M.read (|
                                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",
                                    "cfg"
                                  |),
                                  "revm_primitives::env::CfgEnv",
                                  "chain_id"
                                |)
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_chainid :
      M.IsFunction "revm_interpreter::instructions::host_env::chainid" chainid.
    
    (*
    pub fn coinbase<H: Host + ?Sized>(interpreter: &mut Interpreter, host: &mut H) {
        gas!(interpreter, gas::BASE);
        push_b256!(interpreter, host.env().block.coinbase.into_word());
    }
    *)
    Definition coinbase (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ 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.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::BASE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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_b256",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| interpreter |),
                            "revm_interpreter::interpreter::Interpreter",
                            "stack"
                          |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "alloy_primitives::bits::address::Address",
                              "into_word",
                              []
                            |),
                            [
                              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",
                                "coinbase"
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_coinbase :
      M.IsFunction "revm_interpreter::instructions::host_env::coinbase" coinbase.
    
    (*
    pub fn timestamp<H: Host + ?Sized>(interpreter: &mut Interpreter, host: &mut H) {
        gas!(interpreter, gas::BASE);
        push!(interpreter, host.env().block.timestamp);
    }
    *)
    Definition timestamp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ 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.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::BASE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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 (|
                            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",
                              "timestamp"
                            |)
                          |)
                        ]
                      |)
                    |),
                    [
                      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_timestamp :
      M.IsFunction "revm_interpreter::instructions::host_env::timestamp" timestamp.
    
    (*
    pub fn block_number<H: Host + ?Sized>(interpreter: &mut Interpreter, host: &mut H) {
        gas!(interpreter, gas::BASE);
        push!(interpreter, host.env().block.number);
    }
    *)
    Definition block_number (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ 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.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::BASE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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 (|
                            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"
                            |)
                          |)
                        ]
                      |)
                    |),
                    [
                      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_block_number :
      M.IsFunction "revm_interpreter::instructions::host_env::block_number" block_number.
    
    (*
    pub fn difficulty<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        gas!(interpreter, gas::BASE);
        if SPEC::enabled(MERGE) {
            push_b256!(interpreter, host.env().block.prevrandao.unwrap());
        } else {
            push!(interpreter, host.env().block.difficulty);
        }
    }
    *)
    Definition difficulty (ε : 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::BASE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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 (| 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::MERGE"
                                    []
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) 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.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                            [ Value.Integer IntegerKind.Usize 32 ]
                                            []
                                        ],
                                      "unwrap",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        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",
                                          "prevrandao"
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              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 [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (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 (|
                                    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",
                                      "difficulty"
                                    |)
                                  |)
                                ]
                              |)
                            |),
                            [
                              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_difficulty :
      M.IsFunction "revm_interpreter::instructions::host_env::difficulty" difficulty.
    
    (*
    pub fn gaslimit<H: Host + ?Sized>(interpreter: &mut Interpreter, host: &mut H) {
        gas!(interpreter, gas::BASE);
        push!(interpreter, host.env().block.gas_limit);
    }
    *)
    Definition gaslimit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ 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.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::BASE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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 (|
                            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",
                              "gas_limit"
                            |)
                          |)
                        ]
                      |)
                    |),
                    [
                      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_gaslimit :
      M.IsFunction "revm_interpreter::instructions::host_env::gaslimit" gaslimit.
    
    (*
    pub fn gasprice<H: Host + ?Sized>(interpreter: &mut Interpreter, host: &mut H) {
        gas!(interpreter, gas::BASE);
        push!(interpreter, host.env().effective_gas_price());
    }
    *)
    Definition gasprice (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ 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.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::BASE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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.call_closure (|
                            M.get_associated_function (|
                              Ty.path "revm_primitives::env::Env",
                              "effective_gas_price",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "revm_interpreter::host::Host",
                                  H,
                                  [],
                                  "env",
                                  []
                                |),
                                [ M.read (| host |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_gasprice :
      M.IsFunction "revm_interpreter::instructions::host_env::gasprice" gasprice.
    
    (*
    pub fn basefee<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        check!(interpreter, LONDON);
        gas!(interpreter, gas::BASE);
        push!(interpreter, host.env().block.basefee);
    }
    *)
    Definition basefee (ε : 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::LONDON"
                                        []
                                    ]
                                  |)
                                |)
                              |)) 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::BASE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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 (|
                            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",
                              "basefee"
                            |)
                          |)
                        ]
                      |)
                    |),
                    [
                      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_basefee :
      M.IsFunction "revm_interpreter::instructions::host_env::basefee" basefee.
    
    (*
    pub fn origin<H: Host + ?Sized>(interpreter: &mut Interpreter, host: &mut H) {
        gas!(interpreter, gas::BASE);
        push_b256!(interpreter, host.env().tx.caller.into_word());
    }
    *)
    Definition origin (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ 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.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::BASE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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_b256",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| interpreter |),
                            "revm_interpreter::interpreter::Interpreter",
                            "stack"
                          |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "alloy_primitives::bits::address::Address",
                              "into_word",
                              []
                            |),
                            [
                              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",
                                  "tx"
                                |),
                                "revm_primitives::env::TxEnv",
                                "caller"
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_origin : M.IsFunction "revm_interpreter::instructions::host_env::origin" origin.
    
    (*
    pub fn blob_hash<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        check!(interpreter, CANCUN);
        gas!(interpreter, gas::VERYLOW);
        pop_top!(interpreter, index);
        let i = as_usize_saturated!(index);
        *index = match host.env().tx.blob_hashes.get(i) {
            Some(hash) => U256::from_be_bytes(hash.0),
            None => U256::ZERO,
        };
    }
    *)
    Definition blob_hash (ε : 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::VERYLOW"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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~ i :=
                  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",
                                      []
                                    |),
                                    [ M.read (| index |) ]
                                  |)
                                |) 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
                let~ _ :=
                  M.write (|
                    M.read (| index |),
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                    [ Value.Integer IntegerKind.Usize 32 ]
                                    []
                                ],
                              "get",
                              [ Ty.path "usize" ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  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"
                                    ],
                                  [],
                                  "deref",
                                  []
                                |),
                                [
                                  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",
                                      "tx"
                                    |),
                                    "revm_primitives::env::TxEnv",
                                    "blob_hashes"
                                  |)
                                ]
                              |);
                              M.read (| i |)
                            ]
                          |)
                        |),
                        [
                          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
                              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
                                      ]
                                      [],
                                    "from_be_bytes",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_struct_tuple_field (|
                                        M.read (| hash |),
                                        "alloy_primitives::bits::fixed::FixedBytes",
                                        0
                                      |)
                                    |)
                                  ]
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                              M.get_constant (| "ruint::ZERO" |)))
                        ]
                      |)
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_blob_hash :
      M.IsFunction "revm_interpreter::instructions::host_env::blob_hash" blob_hash.
    
    (*
    pub fn blob_basefee<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, host: &mut H) {
        check!(interpreter, CANCUN);
        gas!(interpreter, gas::BASE);
        push!(
            interpreter,
            U256::from(host.env().block.get_blob_gasprice().unwrap_or_default())
        );
    }
    *)
    Definition blob_basefee (ε : 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::BASE"
                                        |)
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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.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 "u128" ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u128" ],
                                  "unwrap_or_default",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_primitives::env::BlockEnv",
                                      "get_blob_gasprice",
                                      []
                                    |),
                                    [
                                      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"
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_blob_basefee :
      M.IsFunction "revm_interpreter::instructions::host_env::blob_basefee" blob_basefee.
  End host_env.
End instructions.
