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

Module instructions.
  Module system.
    (*
    pub fn keccak256<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        pop_top!(interpreter, offset, len_ptr);
        let len = as_usize_or_fail!(interpreter, len_ptr);
        gas_or_fail!(interpreter, gas::keccak256_cost(len as u64));
        let hash = if len == 0 {
            KECCAK_EMPTY
        } else {
            let from = as_usize_or_fail!(interpreter, offset);
            resize_memory!(interpreter, from, len);
            crate::primitives::keccak256(interpreter.shared_memory.slice(from, len))
        };
        *len_ptr = hash.into();
    }
    *)
    Definition keccak256 (ε : 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 (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 2
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "pop_top_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let offset := M.copy (| γ0_0 |) in
                        let len_ptr := M.copy (| γ0_1 |) in
                        let~ len :=
                          M.copy (|
                            let~ x :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "as_limbs",
                                    []
                                  |),
                                  [ M.read (| len_ptr |) ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            LogicalOp.or (|
                                              LogicalOp.or (|
                                                BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.ne (|
                                                    M.read (|
                                                      M.SubPointer.get_array_field (|
                                                        M.read (| x |),
                                                        M.alloc (|
                                                          Value.Integer IntegerKind.Usize 2
                                                        |)
                                                      |)
                                                    |),
                                                    Value.Integer IntegerKind.U64 0
                                                  |)))
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 3
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |)))
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| interpreter |),
                                                  "revm_interpreter::interpreter::Interpreter",
                                                  "instruction_result"
                                                |),
                                                Value.StructTuple
                                                  "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                  []
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::TryFrom",
                                    Ty.path "usize",
                                    [ Ty.path "u64" ],
                                    "try_from",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_array_field (|
                                        M.read (| x |),
                                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                      |)
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::result::Result::Ok",
                                        0
                                      |) in
                                    let val := M.copy (| γ0_0 |) in
                                    val))
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "revm_interpreter::gas::calc::keccak256_cost",
                                  []
                                |),
                                [ M.rust_cast (M.read (| len |)) ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let gas_used := M.copy (| γ0_0 |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "revm_interpreter::gas::Gas",
                                                      "record_cost",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "gas"
                                                      |);
                                                      M.read (| gas_used |)
                                                    ]
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "instruction_result"
                                                    |),
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                      []
                                                  |) in
                                                M.return_ (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                              []
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |) in
                        let~ hash :=
                          M.copy (|
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.eq (|
                                            M.read (| len |),
                                            Value.Integer IntegerKind.Usize 0
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.get_constant (|
                                      "revm_primitives::utilities::KECCAK_EMPTY"
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let~ from :=
                                      M.copy (|
                                        let~ x :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [],
                                                "as_limbs",
                                                []
                                              |),
                                              [ offset ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        LogicalOp.or (|
                                                          LogicalOp.or (|
                                                            BinOp.ne (|
                                                              M.read (|
                                                                M.SubPointer.get_array_field (|
                                                                  M.read (| x |),
                                                                  M.alloc (|
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      1
                                                                  |)
                                                                |)
                                                              |),
                                                              Value.Integer IntegerKind.U64 0
                                                            |),
                                                            ltac:(M.monadic
                                                              (BinOp.ne (|
                                                                M.read (|
                                                                  M.SubPointer.get_array_field (|
                                                                    M.read (| x |),
                                                                    M.alloc (|
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        2
                                                                    |)
                                                                  |)
                                                                |),
                                                                Value.Integer IntegerKind.U64 0
                                                              |)))
                                                          |),
                                                          ltac:(M.monadic
                                                            (BinOp.ne (|
                                                              M.read (|
                                                                M.SubPointer.get_array_field (|
                                                                  M.read (| x |),
                                                                  M.alloc (|
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      3
                                                                  |)
                                                                |)
                                                              |),
                                                              Value.Integer IntegerKind.U64 0
                                                            |)))
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        let~ _ :=
                                                          M.write (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| interpreter |),
                                                              "revm_interpreter::interpreter::Interpreter",
                                                              "instruction_result"
                                                            |),
                                                            Value.StructTuple
                                                              "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                              []
                                                          |) in
                                                        M.return_ (| Value.Tuple [] |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.match_operator (|
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::convert::TryFrom",
                                                Ty.path "usize",
                                                [ Ty.path "u64" ],
                                                "try_from",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| x |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ0_0 :=
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    γ,
                                                    "core::result::Result::Ok",
                                                    0
                                                  |) in
                                                let val := M.copy (| γ0_0 |) in
                                                val))
                                          ]
                                        |)
                                      |) in
                                    let~ new_size :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "usize",
                                            "saturating_add",
                                            []
                                          |),
                                          [ M.read (| from |); M.read (| len |) ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    BinOp.gt (|
                                                      M.read (| new_size |),
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                                          "len",
                                                          []
                                                        |),
                                                        [
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| interpreter |),
                                                            "revm_interpreter::interpreter::Interpreter",
                                                            "shared_memory"
                                                          |)
                                                        ]
                                                      |)
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            UnOp.not (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "revm_interpreter::interpreter::resize_memory",
                                                                  []
                                                                |),
                                                                [
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| interpreter |),
                                                                    "revm_interpreter::interpreter::Interpreter",
                                                                    "shared_memory"
                                                                  |);
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| interpreter |),
                                                                    "revm_interpreter::interpreter::Interpreter",
                                                                    "gas"
                                                                  |);
                                                                  M.read (| new_size |)
                                                                ]
                                                              |)
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            let~ _ :=
                                                              M.write (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| interpreter |),
                                                                  "revm_interpreter::interpreter::Interpreter",
                                                                  "instruction_result"
                                                                |),
                                                                Value.StructTuple
                                                                  "revm_interpreter::instruction_result::InstructionResult::MemoryOOG"
                                                                  []
                                                              |) in
                                                            M.return_ (| Value.Tuple [] |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "alloy_primitives::utils::keccak256",
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                                          ]
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                              "slice",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| interpreter |),
                                                "revm_interpreter::interpreter::Interpreter",
                                                "shared_memory"
                                              |);
                                              M.read (| from |);
                                              M.read (| len |)
                                            ]
                                          |)
                                        ]
                                      |)
                                    |)))
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.write (|
                            M.read (| len_ptr |),
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::convert::Into",
                                Ty.apply
                                  (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                  [ Value.Integer IntegerKind.Usize 32 ]
                                  [],
                                [
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    []
                                ],
                                "into",
                                []
                              |),
                              [ M.read (| hash |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_keccak256 :
      M.IsFunction "revm_interpreter::instructions::system::keccak256" keccak256.
    
    (*
    pub fn address<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        gas!(interpreter, gas::BASE);
        push_b256!(interpreter, interpreter.contract.target_address.into_word());
    }
    *)
    Definition address (ε : 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.read (| interpreter |),
                                  "revm_interpreter::interpreter::Interpreter",
                                  "contract"
                                |),
                                "revm_interpreter::interpreter::contract::Contract",
                                "target_address"
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::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_address : M.IsFunction "revm_interpreter::instructions::system::address" address.
    
    (*
    pub fn caller<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        gas!(interpreter, gas::BASE);
        push_b256!(interpreter, interpreter.contract.caller.into_word());
    }
    *)
    Definition caller (ε : 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.read (| interpreter |),
                                  "revm_interpreter::interpreter::Interpreter",
                                  "contract"
                                |),
                                "revm_interpreter::interpreter::contract::Contract",
                                "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_caller : M.IsFunction "revm_interpreter::instructions::system::caller" caller.
    
    (*
    pub fn codesize<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        gas!(interpreter, gas::BASE);
        // Inform the optimizer that the bytecode cannot be EOF to remove a bounds check.
        assume!(!interpreter.contract.bytecode.is_eof());
        push!(interpreter, U256::from(interpreter.contract.bytecode.len()));
    }
    *)
    Definition codesize (ε : 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 (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  UnOp.not (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::bytecode::Bytecode",
                                        "is_eof",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| interpreter |),
                                            "revm_interpreter::interpreter::Interpreter",
                                            "contract"
                                          |),
                                          "revm_interpreter::interpreter::contract::Contract",
                                          "bytecode"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.call_closure (|
                                                M.get_function (|
                                                  "core::panicking::panic_fmt",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "core::fmt::Arguments",
                                                      "new_v1",
                                                      []
                                                    |),
                                                    [
                                                      M.alloc (|
                                                        Value.Array
                                                          [
                                                            M.read (|
                                                              Value.String
                                                                "internal error: entered unreachable code: !interpreter.contract.bytecode.is_eof()"
                                                            |)
                                                          ]
                                                      |);
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::rt::Argument",
                                                            "none",
                                                            []
                                                          |),
                                                          []
                                                        |)
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::hint::unreachable_unchecked",
                                                          []
                                                        |),
                                                        []
                                                      |)
                                                    |)
                                                  |) in
                                                M.alloc (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| 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 "usize" ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::bytecode::Bytecode",
                                  "len",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "contract"
                                    |),
                                    "revm_interpreter::interpreter::contract::Contract",
                                    "bytecode"
                                  |)
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_codesize :
      M.IsFunction "revm_interpreter::instructions::system::codesize" codesize.
    
    (*
    pub fn codecopy<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        pop!(interpreter, memory_offset, code_offset, len);
        let len = as_usize_or_fail!(interpreter, len);
        gas_or_fail!(interpreter, gas::verylowcopy_cost(len as u64));
        if len == 0 {
            return;
        }
        let memory_offset = as_usize_or_fail!(interpreter, memory_offset);
        let code_offset = as_usize_saturated!(code_offset);
        resize_memory!(interpreter, memory_offset, len);
    
        // Inform the optimizer that the bytecode cannot be EOF to remove a bounds check.
        assume!(!interpreter.contract.bytecode.is_eof());
        // Note: this can't panic because we resized memory to fit.
        interpreter.shared_memory.set_data(
            memory_offset,
            code_offset,
            len,
            &interpreter.contract.bytecode.original_bytes(),
        );
    }
    *)
    Definition codecopy (ε : 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 (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 3
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "pop3_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let γ0_2 := M.SubPointer.get_tuple_field (| γ, 2 |) in
                        let memory_offset := M.copy (| γ0_0 |) in
                        let code_offset := M.copy (| γ0_1 |) in
                        let len := M.copy (| γ0_2 |) in
                        let~ len :=
                          M.copy (|
                            let~ x :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "as_limbs",
                                    []
                                  |),
                                  [ len ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            LogicalOp.or (|
                                              LogicalOp.or (|
                                                BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.ne (|
                                                    M.read (|
                                                      M.SubPointer.get_array_field (|
                                                        M.read (| x |),
                                                        M.alloc (|
                                                          Value.Integer IntegerKind.Usize 2
                                                        |)
                                                      |)
                                                    |),
                                                    Value.Integer IntegerKind.U64 0
                                                  |)))
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 3
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |)))
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| interpreter |),
                                                  "revm_interpreter::interpreter::Interpreter",
                                                  "instruction_result"
                                                |),
                                                Value.StructTuple
                                                  "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                  []
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::TryFrom",
                                    Ty.path "usize",
                                    [ Ty.path "u64" ],
                                    "try_from",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_array_field (|
                                        M.read (| x |),
                                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                      |)
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::result::Result::Ok",
                                        0
                                      |) in
                                    let val := M.copy (| γ0_0 |) in
                                    val))
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "revm_interpreter::gas::calc::verylowcopy_cost",
                                  []
                                |),
                                [ M.rust_cast (M.read (| len |)) ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let gas_used := M.copy (| γ0_0 |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "revm_interpreter::gas::Gas",
                                                      "record_cost",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "gas"
                                                      |);
                                                      M.read (| gas_used |)
                                                    ]
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "instruction_result"
                                                    |),
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                      []
                                                  |) in
                                                M.return_ (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                              []
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.eq (|
                                          M.read (| len |),
                                          Value.Integer IntegerKind.Usize 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (| M.read (| M.return_ (| Value.Tuple [] |) |) |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ memory_offset :=
                          M.copy (|
                            let~ x :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "as_limbs",
                                    []
                                  |),
                                  [ memory_offset ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            LogicalOp.or (|
                                              LogicalOp.or (|
                                                BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.ne (|
                                                    M.read (|
                                                      M.SubPointer.get_array_field (|
                                                        M.read (| x |),
                                                        M.alloc (|
                                                          Value.Integer IntegerKind.Usize 2
                                                        |)
                                                      |)
                                                    |),
                                                    Value.Integer IntegerKind.U64 0
                                                  |)))
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 3
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |)))
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| interpreter |),
                                                  "revm_interpreter::interpreter::Interpreter",
                                                  "instruction_result"
                                                |),
                                                Value.StructTuple
                                                  "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                  []
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::TryFrom",
                                    Ty.path "usize",
                                    [ Ty.path "u64" ],
                                    "try_from",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_array_field (|
                                        M.read (| x |),
                                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                      |)
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::result::Result::Ok",
                                        0
                                      |) in
                                    let val := M.copy (| γ0_0 |) in
                                    val))
                              ]
                            |)
                          |) in
                        let~ code_offset :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  []
                                  [ Ty.path "usize"; Ty.path "core::num::error::TryFromIntError" ],
                                "unwrap_or",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::TryFrom",
                                    Ty.path "usize",
                                    [ Ty.path "u64" ],
                                    "try_from",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      let~ x :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [],
                                              "as_limbs",
                                              []
                                            |),
                                            [ code_offset ]
                                          |)
                                        |) in
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    LogicalOp.and (|
                                                      LogicalOp.and (|
                                                        BinOp.eq (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 1
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |),
                                                        ltac:(M.monadic
                                                          (BinOp.eq (|
                                                            M.read (|
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| x |),
                                                                M.alloc (|
                                                                  Value.Integer IntegerKind.Usize 2
                                                                |)
                                                              |)
                                                            |),
                                                            Value.Integer IntegerKind.U64 0
                                                          |)))
                                                      |),
                                                      ltac:(M.monadic
                                                        (BinOp.eq (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 3
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |)))
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.SubPointer.get_array_field (|
                                                M.read (| x |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic (M.get_constant (| "core::num::MAX" |)))
                                        ]
                                      |)
                                    |)
                                  ]
                                |);
                                M.read (| M.get_constant (| "core::num::MAX" |) |)
                              ]
                            |)
                          |) in
                        let~ new_size :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "saturating_add", [] |),
                              [ M.read (| memory_offset |); M.read (| len |) ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| new_size |),
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                              "len",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| interpreter |),
                                                "revm_interpreter::interpreter::Interpreter",
                                                "shared_memory"
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "revm_interpreter::interpreter::resize_memory",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "shared_memory"
                                                      |);
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "gas"
                                                      |);
                                                      M.read (| new_size |)
                                                    ]
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "instruction_result"
                                                    |),
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::MemoryOOG"
                                                      []
                                                  |) in
                                                M.return_ (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          UnOp.not (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "revm_primitives::bytecode::Bytecode",
                                                "is_eof",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| interpreter |),
                                                    "revm_interpreter::interpreter::Interpreter",
                                                    "contract"
                                                  |),
                                                  "revm_interpreter::interpreter::contract::Contract",
                                                  "bytecode"
                                                |)
                                              ]
                                            |)
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "core::panicking::panic_fmt",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::Arguments",
                                                              "new_v1",
                                                              []
                                                            |),
                                                            [
                                                              M.alloc (|
                                                                Value.Array
                                                                  [
                                                                    M.read (|
                                                                      Value.String
                                                                        "internal error: entered unreachable code: !interpreter.contract.bytecode.is_eof()"
                                                                    |)
                                                                  ]
                                                              |);
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path
                                                                      "core::fmt::rt::Argument",
                                                                    "none",
                                                                    []
                                                                  |),
                                                                  []
                                                                |)
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        let~ _ :=
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "core::hint::unreachable_unchecked",
                                                                  []
                                                                |),
                                                                []
                                                              |)
                                                            |)
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)
                                                      |)
                                                    |)
                                                  |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path
                                  "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                "set_data",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| interpreter |),
                                  "revm_interpreter::interpreter::Interpreter",
                                  "shared_memory"
                                |);
                                M.read (| memory_offset |);
                                M.read (| code_offset |);
                                M.read (| len |);
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::Deref",
                                    Ty.path "bytes::bytes::Bytes",
                                    [],
                                    "deref",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.path "alloy_primitives::bytes_::Bytes",
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "revm_primitives::bytecode::Bytecode",
                                              "original_bytes",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| interpreter |),
                                                  "revm_interpreter::interpreter::Interpreter",
                                                  "contract"
                                                |),
                                                "revm_interpreter::interpreter::contract::Contract",
                                                "bytecode"
                                              |)
                                            ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_codecopy :
      M.IsFunction "revm_interpreter::instructions::system::codecopy" codecopy.
    
    (*
    pub fn calldataload<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        gas!(interpreter, gas::VERYLOW);
        pop_top!(interpreter, offset_ptr);
        let mut word = B256::ZERO;
        let offset = as_usize_saturated!(offset_ptr);
        if offset < interpreter.contract.input.len() {
            let count = 32.min(interpreter.contract.input.len() - offset);
            // SAFETY: count is bounded by the calldata length.
            // This is `word[..count].copy_from_slice(input[offset..offset + count])`, written using
            // raw pointers as apparently the compiler cannot optimize the slice version, and using
            // `get_unchecked` twice is uglier.
            debug_assert!(count <= 32 && offset + count <= interpreter.contract.input.len());
            unsafe {
                ptr::copy_nonoverlapping(
                    interpreter.contract.input.as_ptr().add(offset),
                    word.as_mut_ptr(),
                    count,
                )
            };
        }
        *offset_ptr = word.into();
    }
    *)
    Definition calldataload (ε : 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::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~ offset_ptr :=
                  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~ word :=
                  M.copy (| M.get_constant (| "alloy_primitives::bits::fixed::ZERO" |) |) in
                let~ offset :=
                  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 (| offset_ptr |) ]
                                  |)
                                |) 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.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.read (| offset |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "bytes::bytes::Bytes",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::deref::Deref",
                                          Ty.path "alloy_primitives::bytes_::Bytes",
                                          [],
                                          "deref",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "contract"
                                            |),
                                            "revm_interpreter::interpreter::contract::Contract",
                                            "input"
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ count :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::Ord",
                                  Ty.path "usize",
                                  [],
                                  "min",
                                  []
                                |),
                                [
                                  Value.Integer IntegerKind.Usize 32;
                                  BinOp.Wrap.sub (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "bytes::bytes::Bytes",
                                        "len",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::deref::Deref",
                                            Ty.path "alloy_primitives::bytes_::Bytes",
                                            [],
                                            "deref",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| interpreter |),
                                                "revm_interpreter::interpreter::Interpreter",
                                                "contract"
                                              |),
                                              "revm_interpreter::interpreter::contract::Contract",
                                              "input"
                                            |)
                                          ]
                                        |)
                                      ]
                                    |),
                                    M.read (| offset |)
                                  |)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    UnOp.not (|
                                                      LogicalOp.and (|
                                                        BinOp.le (|
                                                          M.read (| count |),
                                                          Value.Integer IntegerKind.Usize 32
                                                        |),
                                                        ltac:(M.monadic
                                                          (BinOp.le (|
                                                            BinOp.Wrap.add (|
                                                              M.read (| offset |),
                                                              M.read (| count |)
                                                            |),
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path "bytes::bytes::Bytes",
                                                                "len",
                                                                []
                                                              |),
                                                              [
                                                                M.call_closure (|
                                                                  M.get_trait_method (|
                                                                    "core::ops::deref::Deref",
                                                                    Ty.path
                                                                      "alloy_primitives::bytes_::Bytes",
                                                                    [],
                                                                    "deref",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        M.read (| interpreter |),
                                                                        "revm_interpreter::interpreter::Interpreter",
                                                                        "contract"
                                                                      |),
                                                                      "revm_interpreter::interpreter::contract::Contract",
                                                                      "input"
                                                                    |)
                                                                  ]
                                                                |)
                                                              ]
                                                            |)
                                                          |)))
                                                      |)
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "core::panicking::panic",
                                                      []
                                                    |),
                                                    [
                                                      M.read (|
                                                        Value.String
                                                          "assertion failed: count <= 32 && offset + count <= interpreter.contract.input.len()"
                                                      |)
                                                    ]
                                                  |)
                                                |)
                                              |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::intrinsics::copy_nonoverlapping",
                                  [ Ty.path "u8" ]
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                          "as_ptr",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::deref::Deref",
                                              Ty.path "bytes::bytes::Bytes",
                                              [],
                                              "deref",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::deref::Deref",
                                                  Ty.path "alloy_primitives::bytes_::Bytes",
                                                  [],
                                                  "deref",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "contract"
                                                    |),
                                                    "revm_interpreter::interpreter::contract::Contract",
                                                    "input"
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        ]
                                      |);
                                      M.read (| offset |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                      "as_mut_ptr",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::deref::DerefMut",
                                          Ty.apply
                                            (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                            [ Value.Integer IntegerKind.Usize 32 ]
                                            [],
                                          [],
                                          "deref_mut",
                                          []
                                        |),
                                        [ word ]
                                      |)
                                    ]
                                  |);
                                  M.read (| count |)
                                ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.write (|
                    M.read (| offset_ptr |),
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::convert::Into",
                        Ty.apply
                          (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                          [ Value.Integer IntegerKind.Usize 32 ]
                          [],
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            []
                        ],
                        "into",
                        []
                      |),
                      [ M.read (| word |) ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_calldataload :
      M.IsFunction "revm_interpreter::instructions::system::calldataload" calldataload.
    
    (*
    pub fn calldatasize<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        gas!(interpreter, gas::BASE);
        push!(interpreter, U256::from(interpreter.contract.input.len()));
    }
    *)
    Definition calldatasize (ε : 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.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [],
                              "from",
                              [ Ty.path "usize" ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "bytes::bytes::Bytes",
                                  "len",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::deref::Deref",
                                      Ty.path "alloy_primitives::bytes_::Bytes",
                                      [],
                                      "deref",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| interpreter |),
                                          "revm_interpreter::interpreter::Interpreter",
                                          "contract"
                                        |),
                                        "revm_interpreter::interpreter::contract::Contract",
                                        "input"
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_calldatasize :
      M.IsFunction "revm_interpreter::instructions::system::calldatasize" calldatasize.
    
    (*
    pub fn callvalue<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        gas!(interpreter, gas::BASE);
        push!(interpreter, interpreter.contract.call_value);
    }
    *)
    Definition callvalue (ε : 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.read (| interpreter |),
                                "revm_interpreter::interpreter::Interpreter",
                                "contract"
                              |),
                              "revm_interpreter::interpreter::contract::Contract",
                              "call_value"
                            |)
                          |)
                        ]
                      |)
                    |),
                    [
                      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_callvalue :
      M.IsFunction "revm_interpreter::instructions::system::callvalue" callvalue.
    
    (*
    pub fn calldatacopy<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        pop!(interpreter, memory_offset, data_offset, len);
        let len = as_usize_or_fail!(interpreter, len);
        gas_or_fail!(interpreter, gas::verylowcopy_cost(len as u64));
        if len == 0 {
            return;
        }
        let memory_offset = as_usize_or_fail!(interpreter, memory_offset);
        let data_offset = as_usize_saturated!(data_offset);
        resize_memory!(interpreter, memory_offset, len);
    
        // Note: this can't panic because we resized memory to fit.
        interpreter.shared_memory.set_data(
            memory_offset,
            data_offset,
            len,
            &interpreter.contract.input,
        );
    }
    *)
    Definition calldatacopy (ε : 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 (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 3
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "pop3_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let γ0_2 := M.SubPointer.get_tuple_field (| γ, 2 |) in
                        let memory_offset := M.copy (| γ0_0 |) in
                        let data_offset := M.copy (| γ0_1 |) in
                        let len := M.copy (| γ0_2 |) in
                        let~ len :=
                          M.copy (|
                            let~ x :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "as_limbs",
                                    []
                                  |),
                                  [ len ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            LogicalOp.or (|
                                              LogicalOp.or (|
                                                BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.ne (|
                                                    M.read (|
                                                      M.SubPointer.get_array_field (|
                                                        M.read (| x |),
                                                        M.alloc (|
                                                          Value.Integer IntegerKind.Usize 2
                                                        |)
                                                      |)
                                                    |),
                                                    Value.Integer IntegerKind.U64 0
                                                  |)))
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 3
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |)))
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| interpreter |),
                                                  "revm_interpreter::interpreter::Interpreter",
                                                  "instruction_result"
                                                |),
                                                Value.StructTuple
                                                  "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                  []
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::TryFrom",
                                    Ty.path "usize",
                                    [ Ty.path "u64" ],
                                    "try_from",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_array_field (|
                                        M.read (| x |),
                                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                      |)
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::result::Result::Ok",
                                        0
                                      |) in
                                    let val := M.copy (| γ0_0 |) in
                                    val))
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "revm_interpreter::gas::calc::verylowcopy_cost",
                                  []
                                |),
                                [ M.rust_cast (M.read (| len |)) ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let gas_used := M.copy (| γ0_0 |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "revm_interpreter::gas::Gas",
                                                      "record_cost",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "gas"
                                                      |);
                                                      M.read (| gas_used |)
                                                    ]
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "instruction_result"
                                                    |),
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                      []
                                                  |) in
                                                M.return_ (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                              []
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.eq (|
                                          M.read (| len |),
                                          Value.Integer IntegerKind.Usize 0
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (| M.read (| M.return_ (| Value.Tuple [] |) |) |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ memory_offset :=
                          M.copy (|
                            let~ x :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "as_limbs",
                                    []
                                  |),
                                  [ memory_offset ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            LogicalOp.or (|
                                              LogicalOp.or (|
                                                BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.ne (|
                                                    M.read (|
                                                      M.SubPointer.get_array_field (|
                                                        M.read (| x |),
                                                        M.alloc (|
                                                          Value.Integer IntegerKind.Usize 2
                                                        |)
                                                      |)
                                                    |),
                                                    Value.Integer IntegerKind.U64 0
                                                  |)))
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 3
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |)))
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| interpreter |),
                                                  "revm_interpreter::interpreter::Interpreter",
                                                  "instruction_result"
                                                |),
                                                Value.StructTuple
                                                  "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                  []
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::TryFrom",
                                    Ty.path "usize",
                                    [ Ty.path "u64" ],
                                    "try_from",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_array_field (|
                                        M.read (| x |),
                                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                      |)
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::result::Result::Ok",
                                        0
                                      |) in
                                    let val := M.copy (| γ0_0 |) in
                                    val))
                              ]
                            |)
                          |) in
                        let~ data_offset :=
                          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",
                                              []
                                            |),
                                            [ data_offset ]
                                          |)
                                        |) in
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    LogicalOp.and (|
                                                      LogicalOp.and (|
                                                        BinOp.eq (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 1
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |),
                                                        ltac:(M.monadic
                                                          (BinOp.eq (|
                                                            M.read (|
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| x |),
                                                                M.alloc (|
                                                                  Value.Integer IntegerKind.Usize 2
                                                                |)
                                                              |)
                                                            |),
                                                            Value.Integer IntegerKind.U64 0
                                                          |)))
                                                      |),
                                                      ltac:(M.monadic
                                                        (BinOp.eq (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 3
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |)))
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.SubPointer.get_array_field (|
                                                M.read (| x |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic (M.get_constant (| "core::num::MAX" |)))
                                        ]
                                      |)
                                    |)
                                  ]
                                |);
                                M.read (| M.get_constant (| "core::num::MAX" |) |)
                              ]
                            |)
                          |) in
                        let~ new_size :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "saturating_add", [] |),
                              [ M.read (| memory_offset |); M.read (| len |) ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| new_size |),
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                              "len",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| interpreter |),
                                                "revm_interpreter::interpreter::Interpreter",
                                                "shared_memory"
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  M.call_closure (|
                                                    M.get_function (|
                                                      "revm_interpreter::interpreter::resize_memory",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "shared_memory"
                                                      |);
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "gas"
                                                      |);
                                                      M.read (| new_size |)
                                                    ]
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "instruction_result"
                                                    |),
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::MemoryOOG"
                                                      []
                                                  |) in
                                                M.return_ (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path
                                  "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                "set_data",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| interpreter |),
                                  "revm_interpreter::interpreter::Interpreter",
                                  "shared_memory"
                                |);
                                M.read (| memory_offset |);
                                M.read (| data_offset |);
                                M.read (| len |);
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::Deref",
                                    Ty.path "bytes::bytes::Bytes",
                                    [],
                                    "deref",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.path "alloy_primitives::bytes_::Bytes",
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| interpreter |),
                                            "revm_interpreter::interpreter::Interpreter",
                                            "contract"
                                          |),
                                          "revm_interpreter::interpreter::contract::Contract",
                                          "input"
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_calldatacopy :
      M.IsFunction "revm_interpreter::instructions::system::calldatacopy" calldatacopy.
    
    (*
    pub fn returndatasize<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, _host: &mut H) {
        check!(interpreter, BYZANTIUM);
        gas!(interpreter, gas::BASE);
        push!(
            interpreter,
            U256::from(interpreter.return_data_buffer.len())
        );
    }
    *)
    Definition returndatasize (ε : 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::BYZANTIUM"
                                        []
                                    ]
                                  |)
                                |)
                              |)) 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 "usize" ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "bytes::bytes::Bytes",
                                  "len",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::deref::Deref",
                                      Ty.path "alloy_primitives::bytes_::Bytes",
                                      [],
                                      "deref",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "return_data_buffer"
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_returndatasize :
      M.IsFunction "revm_interpreter::instructions::system::returndatasize" returndatasize.
    
    (*
    pub fn returndatacopy<H: Host + ?Sized, SPEC: Spec>(interpreter: &mut Interpreter, _host: &mut H) {
        check!(interpreter, BYZANTIUM);
        pop!(interpreter, memory_offset, offset, len);
        let len = as_usize_or_fail!(interpreter, len);
        gas_or_fail!(interpreter, gas::verylowcopy_cost(len as u64));
        let data_offset = as_usize_saturated!(offset);
        let data_end = data_offset.saturating_add(len);
        if data_end > interpreter.return_data_buffer.len() {
            interpreter.instruction_result = InstructionResult::OutOfOffset;
            return;
        }
        if len != 0 {
            let memory_offset = as_usize_or_fail!(interpreter, memory_offset);
            resize_memory!(interpreter, memory_offset, len);
            interpreter.shared_memory.set(
                memory_offset,
                &interpreter.return_data_buffer[data_offset..data_end],
            );
        }
    }
    *)
    Definition returndatacopy (ε : 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::BYZANTIUM"
                                        []
                                    ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::NotActivated"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| interpreter |),
                                        "revm_interpreter::interpreter::Interpreter",
                                        "stack"
                                      |)
                                    ]
                                  |),
                                  Value.Integer IntegerKind.Usize 3
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.write (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "instruction_result"
                                    |),
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_interpreter::interpreter::stack::Stack",
                        "pop3_unsafe",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| interpreter |),
                          "revm_interpreter::interpreter::Interpreter",
                          "stack"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                        let γ0_2 := M.SubPointer.get_tuple_field (| γ, 2 |) in
                        let memory_offset := M.copy (| γ0_0 |) in
                        let offset := M.copy (| γ0_1 |) in
                        let len := M.copy (| γ0_2 |) in
                        let~ len :=
                          M.copy (|
                            let~ x :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "as_limbs",
                                    []
                                  |),
                                  [ len ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            LogicalOp.or (|
                                              LogicalOp.or (|
                                                BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.ne (|
                                                    M.read (|
                                                      M.SubPointer.get_array_field (|
                                                        M.read (| x |),
                                                        M.alloc (|
                                                          Value.Integer IntegerKind.Usize 2
                                                        |)
                                                      |)
                                                    |),
                                                    Value.Integer IntegerKind.U64 0
                                                  |)))
                                              |),
                                              ltac:(M.monadic
                                                (BinOp.ne (|
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| x |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 3
                                                      |)
                                                    |)
                                                  |),
                                                  Value.Integer IntegerKind.U64 0
                                                |)))
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| interpreter |),
                                                  "revm_interpreter::interpreter::Interpreter",
                                                  "instruction_result"
                                                |),
                                                Value.StructTuple
                                                  "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                  []
                                              |) in
                                            M.return_ (| Value.Tuple [] |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::TryFrom",
                                    Ty.path "usize",
                                    [ Ty.path "u64" ],
                                    "try_from",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_array_field (|
                                        M.read (| x |),
                                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                      |)
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::result::Result::Ok",
                                        0
                                      |) in
                                    let val := M.copy (| γ0_0 |) in
                                    val))
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "revm_interpreter::gas::calc::verylowcopy_cost",
                                  []
                                |),
                                [ M.rust_cast (M.read (| len |)) ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let gas_used := M.copy (| γ0_0 |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "revm_interpreter::gas::Gas",
                                                      "record_cost",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "gas"
                                                      |);
                                                      M.read (| gas_used |)
                                                    ]
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "instruction_result"
                                                    |),
                                                    Value.StructTuple
                                                      "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                                      []
                                                  |) in
                                                M.return_ (| Value.Tuple [] |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interpreter |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "instruction_result"
                                            |),
                                            Value.StructTuple
                                              "revm_interpreter::instruction_result::InstructionResult::OutOfGas"
                                              []
                                          |) in
                                        M.return_ (| Value.Tuple [] |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |) in
                        let~ data_offset :=
                          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",
                                              []
                                            |),
                                            [ offset ]
                                          |)
                                        |) in
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    LogicalOp.and (|
                                                      LogicalOp.and (|
                                                        BinOp.eq (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 1
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |),
                                                        ltac:(M.monadic
                                                          (BinOp.eq (|
                                                            M.read (|
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| x |),
                                                                M.alloc (|
                                                                  Value.Integer IntegerKind.Usize 2
                                                                |)
                                                              |)
                                                            |),
                                                            Value.Integer IntegerKind.U64 0
                                                          |)))
                                                      |),
                                                      ltac:(M.monadic
                                                        (BinOp.eq (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 3
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |)))
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.SubPointer.get_array_field (|
                                                M.read (| x |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic (M.get_constant (| "core::num::MAX" |)))
                                        ]
                                      |)
                                    |)
                                  ]
                                |);
                                M.read (| M.get_constant (| "core::num::MAX" |) |)
                              ]
                            |)
                          |) in
                        let~ data_end :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "saturating_add", [] |),
                              [ M.read (| data_offset |); M.read (| len |) ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.read (| data_end |),
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "bytes::bytes::Bytes",
                                              "len",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::deref::Deref",
                                                  Ty.path "alloy_primitives::bytes_::Bytes",
                                                  [],
                                                  "deref",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| interpreter |),
                                                    "revm_interpreter::interpreter::Interpreter",
                                                    "return_data_buffer"
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)) 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::OutOfOffset"
                                              []
                                          |) 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 (|
                                      BinOp.ne (|
                                        M.read (| len |),
                                        Value.Integer IntegerKind.Usize 0
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ memory_offset :=
                                  M.copy (|
                                    let~ x :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [],
                                            "as_limbs",
                                            []
                                          |),
                                          [ memory_offset ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    LogicalOp.or (|
                                                      LogicalOp.or (|
                                                        BinOp.ne (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 1
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |),
                                                        ltac:(M.monadic
                                                          (BinOp.ne (|
                                                            M.read (|
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| x |),
                                                                M.alloc (|
                                                                  Value.Integer IntegerKind.Usize 2
                                                                |)
                                                              |)
                                                            |),
                                                            Value.Integer IntegerKind.U64 0
                                                          |)))
                                                      |),
                                                      ltac:(M.monadic
                                                        (BinOp.ne (|
                                                          M.read (|
                                                            M.SubPointer.get_array_field (|
                                                              M.read (| x |),
                                                              M.alloc (|
                                                                Value.Integer IntegerKind.Usize 3
                                                              |)
                                                            |)
                                                          |),
                                                          Value.Integer IntegerKind.U64 0
                                                        |)))
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    let~ _ :=
                                                      M.write (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| interpreter |),
                                                          "revm_interpreter::interpreter::Interpreter",
                                                          "instruction_result"
                                                        |),
                                                        Value.StructTuple
                                                          "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                                          []
                                                      |) in
                                                    M.return_ (| Value.Tuple [] |)
                                                  |)
                                                |)
                                              |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::TryFrom",
                                            Ty.path "usize",
                                            [ Ty.path "u64" ],
                                            "try_from",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_array_field (|
                                                M.read (| x |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                              |)
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::result::Result::Ok",
                                                0
                                              |) in
                                            let val := M.copy (| γ0_0 |) in
                                            val))
                                      ]
                                    |)
                                  |) in
                                let~ new_size :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "usize",
                                        "saturating_add",
                                        []
                                      |),
                                      [ M.read (| memory_offset |); M.read (| len |) ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.gt (|
                                                  M.read (| new_size |),
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                                      "len",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| interpreter |),
                                                        "revm_interpreter::interpreter::Interpreter",
                                                        "shared_memory"
                                                      |)
                                                    ]
                                                  |)
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "revm_interpreter::interpreter::resize_memory",
                                                              []
                                                            |),
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| interpreter |),
                                                                "revm_interpreter::interpreter::Interpreter",
                                                                "shared_memory"
                                                              |);
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| interpreter |),
                                                                "revm_interpreter::interpreter::Interpreter",
                                                                "gas"
                                                              |);
                                                              M.read (| new_size |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        let~ _ :=
                                                          M.write (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| interpreter |),
                                                              "revm_interpreter::interpreter::Interpreter",
                                                              "instruction_result"
                                                            |),
                                                            Value.StructTuple
                                                              "revm_interpreter::instruction_result::InstructionResult::MemoryOOG"
                                                              []
                                                          |) in
                                                        M.return_ (| Value.Tuple [] |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path
                                          "revm_interpreter::interpreter::shared_memory::SharedMemory",
                                        "set",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| interpreter |),
                                          "revm_interpreter::interpreter::Interpreter",
                                          "shared_memory"
                                        |);
                                        M.read (| memory_offset |);
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::index::Index",
                                            Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::ops::range::Range")
                                                []
                                                [ Ty.path "usize" ]
                                            ],
                                            "index",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::deref::Deref",
                                                Ty.path "bytes::bytes::Bytes",
                                                [],
                                                "deref",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::deref::Deref",
                                                    Ty.path "alloy_primitives::bytes_::Bytes",
                                                    [],
                                                    "deref",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| interpreter |),
                                                      "revm_interpreter::interpreter::Interpreter",
                                                      "return_data_buffer"
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |);
                                            Value.StructRecord
                                              "core::ops::range::Range"
                                              [
                                                ("start", M.read (| data_offset |));
                                                ("end_", M.read (| data_end |))
                                              ]
                                          ]
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_returndatacopy :
      M.IsFunction "revm_interpreter::instructions::system::returndatacopy" returndatacopy.
    
    (*
    pub fn returndataload<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        require_eof!(interpreter);
        gas!(interpreter, gas::VERYLOW);
        pop_top!(interpreter, offset);
        let offset_usize = as_usize_or_fail!(interpreter, offset);
        if offset_usize.saturating_add(32) > interpreter.return_data_buffer.len() {
            // TODO(EOF) proper error.
            interpreter.instruction_result = InstructionResult::OutOfOffset;
            return;
        }
        *offset =
            B256::from_slice(&interpreter.return_data_buffer[offset_usize..offset_usize + 32]).into();
    }
    *)
    Definition returndataload (ε : 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.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| interpreter |),
                                      "revm_interpreter::interpreter::Interpreter",
                                      "is_eof"
                                    |)
                                  |)
                                |)
                              |)) 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::EOFOpcodeDisabledInLegacy"
                                      []
                                  |) 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~ offset :=
                  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~ offset_usize :=
                  M.copy (|
                    let~ x :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [],
                            "as_limbs",
                            []
                          |),
                          [ M.read (| offset |) ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    LogicalOp.or (|
                                      LogicalOp.or (|
                                        BinOp.ne (|
                                          M.read (|
                                            M.SubPointer.get_array_field (|
                                              M.read (| x |),
                                              M.alloc (| Value.Integer IntegerKind.Usize 1 |)
                                            |)
                                          |),
                                          Value.Integer IntegerKind.U64 0
                                        |),
                                        ltac:(M.monadic
                                          (BinOp.ne (|
                                            M.read (|
                                              M.SubPointer.get_array_field (|
                                                M.read (| x |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 2 |)
                                              |)
                                            |),
                                            Value.Integer IntegerKind.U64 0
                                          |)))
                                      |),
                                      ltac:(M.monadic
                                        (BinOp.ne (|
                                          M.read (|
                                            M.SubPointer.get_array_field (|
                                              M.read (| x |),
                                              M.alloc (| Value.Integer IntegerKind.Usize 3 |)
                                            |)
                                          |),
                                          Value.Integer IntegerKind.U64 0
                                        |)))
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| interpreter |),
                                          "revm_interpreter::interpreter::Interpreter",
                                          "instruction_result"
                                        |),
                                        Value.StructTuple
                                          "revm_interpreter::instruction_result::InstructionResult::InvalidOperandOOG"
                                          []
                                      |) in
                                    M.return_ (| Value.Tuple [] |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::TryFrom",
                            Ty.path "usize",
                            [ Ty.path "u64" ],
                            "try_from",
                            []
                          |),
                          [
                            M.read (|
                              M.SubPointer.get_array_field (|
                                M.read (| x |),
                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                              |)
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Ok",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.gt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "usize",
                                      "saturating_add",
                                      []
                                    |),
                                    [ M.read (| offset_usize |); Value.Integer IntegerKind.Usize 32
                                    ]
                                  |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "bytes::bytes::Bytes",
                                      "len",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::deref::Deref",
                                          Ty.path "alloy_primitives::bytes_::Bytes",
                                          [],
                                          "deref",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| interpreter |),
                                            "revm_interpreter::interpreter::Interpreter",
                                            "return_data_buffer"
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |)
                              |)) 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::OutOfOffset"
                                      []
                                  |) in
                                M.return_ (| Value.Tuple [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.write (|
                    M.read (| offset |),
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::convert::Into",
                        Ty.apply
                          (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                          [ Value.Integer IntegerKind.Usize 32 ]
                          [],
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            []
                        ],
                        "into",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [],
                            "from_slice",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::index::Index",
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ],
                                "index",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::Deref",
                                    Ty.path "bytes::bytes::Bytes",
                                    [],
                                    "deref",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.path "alloy_primitives::bytes_::Bytes",
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| interpreter |),
                                          "revm_interpreter::interpreter::Interpreter",
                                          "return_data_buffer"
                                        |)
                                      ]
                                    |)
                                  ]
                                |);
                                Value.StructRecord
                                  "core::ops::range::Range"
                                  [
                                    ("start", M.read (| offset_usize |));
                                    ("end_",
                                      BinOp.Wrap.add (|
                                        M.read (| offset_usize |),
                                        Value.Integer IntegerKind.Usize 32
                                      |))
                                  ]
                              ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_returndataload :
      M.IsFunction "revm_interpreter::instructions::system::returndataload" returndataload.
    
    (*
    pub fn gas<H: Host + ?Sized>(interpreter: &mut Interpreter, _host: &mut H) {
        gas!(interpreter, gas::BASE);
        push!(interpreter, U256::from(interpreter.gas.remaining()));
    }
    *)
    Definition gas (ε : 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.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [],
                              "from",
                              [ Ty.path "u64" ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_interpreter::gas::Gas",
                                  "remaining",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| interpreter |),
                                    "revm_interpreter::interpreter::Interpreter",
                                    "gas"
                                  |)
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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_gas : M.IsFunction "revm_interpreter::instructions::system::gas" gas.
  End system.
End instructions.
