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

Module gas.
  (* StructRecord
    {
      name := "Gas";
      const_params := [];
      ty_params := [];
      fields :=
        [ ("limit", Ty.path "u64"); ("remaining", Ty.path "u64"); ("refunded", Ty.path "i64") ];
    } *)
  
  Module Impl_core_clone_Clone_for_revm_interpreter_gas_Gas.
    Definition Self : Ty.t := Ty.path "revm_interpreter::gas::Gas".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      Value.DeclaredButUndefined,
                      [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_revm_interpreter_gas_Gas.
  
  Module Impl_core_marker_Copy_for_revm_interpreter_gas_Gas.
    Definition Self : Ty.t := Ty.path "revm_interpreter::gas::Gas".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_revm_interpreter_gas_Gas.
  
  Module Impl_core_fmt_Debug_for_revm_interpreter_gas_Gas.
    Definition Self : Ty.t := Ty.path "revm_interpreter::gas::Gas".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field3_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "Gas" |);
              M.read (| Value.String "limit" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_interpreter::gas::Gas",
                "limit"
              |);
              M.read (| Value.String "remaining" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_interpreter::gas::Gas",
                "remaining"
              |);
              M.read (| Value.String "refunded" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::gas::Gas",
                  "refunded"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_revm_interpreter_gas_Gas.
  
  Module Impl_core_default_Default_for_revm_interpreter_gas_Gas.
    Definition Self : Ty.t := Ty.path "revm_interpreter::gas::Gas".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_interpreter::gas::Gas"
            [
              ("limit",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "u64",
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("remaining",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "u64",
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("refunded",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "i64",
                    [],
                    "default",
                    []
                  |),
                  []
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::default::Default"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method default) ].
  End Impl_core_default_Default_for_revm_interpreter_gas_Gas.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_interpreter_gas_Gas.
    Definition Self : Ty.t := Ty.path "revm_interpreter::gas::Gas".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_interpreter_gas_Gas.
  
  Module Impl_core_cmp_PartialEq_for_revm_interpreter_gas_Gas.
    Definition Self : Ty.t := Ty.path "revm_interpreter::gas::Gas".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          LogicalOp.and (|
            LogicalOp.and (|
              BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_interpreter::gas::Gas",
                    "limit"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_interpreter::gas::Gas",
                    "limit"
                  |)
                |)
              |),
              ltac:(M.monadic
                (BinOp.eq (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_interpreter::gas::Gas",
                      "remaining"
                    |)
                  |),
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_interpreter::gas::Gas",
                      "remaining"
                    |)
                  |)
                |)))
            |),
            ltac:(M.monadic
              (BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_interpreter::gas::Gas",
                    "refunded"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_interpreter::gas::Gas",
                    "refunded"
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_revm_interpreter_gas_Gas.
  
  Module Impl_core_cmp_Eq_for_revm_interpreter_gas_Gas.
    Definition Self : Ty.t := Ty.path "revm_interpreter::gas::Gas".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      Value.DeclaredButUndefined,
                      [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_revm_interpreter_gas_Gas.
  
  Module Impl_core_hash_Hash_for_revm_interpreter_gas_Gas.
    Definition Self : Ty.t := Ty.path "revm_interpreter::gas::Gas".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "u64", [], "hash", [ __H ] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_interpreter::gas::Gas",
                      "limit"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "u64", [], "hash", [ __H ] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_interpreter::gas::Gas",
                      "remaining"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Ty.path "i64", [], "hash", [ __H ] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_interpreter::gas::Gas",
                    "refunded"
                  |);
                  M.read (| state |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_revm_interpreter_gas_Gas.
  
  Module Impl_revm_interpreter_gas_Gas.
    Definition Self : Ty.t := Ty.path "revm_interpreter::gas::Gas".
    
    (*
        pub const fn new(limit: u64) -> Self {
            Self {
                limit,
                remaining: limit,
                refunded: 0,
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ limit ] =>
        ltac:(M.monadic
          (let limit := M.alloc (| limit |) in
          Value.StructRecord
            "revm_interpreter::gas::Gas"
            [
              ("limit", M.read (| limit |));
              ("remaining", M.read (| limit |));
              ("refunded", Value.Integer IntegerKind.I64 0)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub const fn new_spent(limit: u64) -> Self {
            Self {
                limit,
                remaining: 0,
                refunded: 0,
            }
        }
    *)
    Definition new_spent (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ limit ] =>
        ltac:(M.monadic
          (let limit := M.alloc (| limit |) in
          Value.StructRecord
            "revm_interpreter::gas::Gas"
            [
              ("limit", M.read (| limit |));
              ("remaining", Value.Integer IntegerKind.U64 0);
              ("refunded", Value.Integer IntegerKind.I64 0)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new_spent : M.IsAssociatedFunction Self "new_spent" new_spent.
    
    (*
        pub const fn limit(&self) -> u64 {
            self.limit
        }
    *)
    Definition limit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_interpreter::gas::Gas",
              "limit"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_limit : M.IsAssociatedFunction Self "limit" limit.
    
    (*
        pub const fn memory(&self) -> u64 {
            0
        }
    *)
    Definition memory (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.Integer IntegerKind.U64 0))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_memory : M.IsAssociatedFunction Self "memory" memory.
    
    (*
        pub const fn refunded(&self) -> i64 {
            self.refunded
        }
    *)
    Definition refunded (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_interpreter::gas::Gas",
              "refunded"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_refunded : M.IsAssociatedFunction Self "refunded" refunded.
    
    (*
        pub const fn spent(&self) -> u64 {
            self.limit - self.remaining
        }
    *)
    Definition spent (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.sub (|
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_interpreter::gas::Gas",
                "limit"
              |)
            |),
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_interpreter::gas::Gas",
                "remaining"
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_spent : M.IsAssociatedFunction Self "spent" spent.
    
    (*
        pub const fn spend(&self) -> u64 {
            self.spent()
        }
    *)
    Definition spend (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "revm_interpreter::gas::Gas", "spent", [] |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_spend : M.IsAssociatedFunction Self "spend" spend.
    
    (*
        pub const fn remaining(&self) -> u64 {
            self.remaining
        }
    *)
    Definition remaining (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_interpreter::gas::Gas",
              "remaining"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_remaining : M.IsAssociatedFunction Self "remaining" remaining.
    
    (*
        pub fn erase_cost(&mut self, returned: u64) {
            self.remaining += returned;
        }
    *)
    Definition erase_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; returned ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let returned := M.alloc (| returned |) in
          M.read (|
            let~ _ :=
              let β :=
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::gas::Gas",
                  "remaining"
                |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| returned |) |) |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_erase_cost : M.IsAssociatedFunction Self "erase_cost" erase_cost.
    
    (*
        pub fn spend_all(&mut self) {
            self.remaining = 0;
        }
    *)
    Definition spend_all (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::gas::Gas",
                  "remaining"
                |),
                Value.Integer IntegerKind.U64 0
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_spend_all : M.IsAssociatedFunction Self "spend_all" spend_all.
    
    (*
        pub fn record_refund(&mut self, refund: i64) {
            self.refunded += refund;
        }
    *)
    Definition record_refund (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; refund ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let refund := M.alloc (| refund |) in
          M.read (|
            let~ _ :=
              let β :=
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::gas::Gas",
                  "refunded"
                |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| refund |) |) |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_record_refund :
      M.IsAssociatedFunction Self "record_refund" record_refund.
    
    (*
        pub fn set_final_refund(&mut self, is_london: bool) {
            let max_refund_quotient = if is_london { 5 } else { 2 };
            self.refunded = (self.refunded() as u64).min(self.spent() / max_refund_quotient) as i64;
        }
    *)
    Definition set_final_refund (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; is_london ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let is_london := M.alloc (| is_london |) in
          M.read (|
            let~ max_refund_quotient :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.use is_london in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.Integer IntegerKind.U64 5 |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 2 |)))
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::gas::Gas",
                  "refunded"
                |),
                M.rust_cast
                  (M.call_closure (|
                    M.get_trait_method (| "core::cmp::Ord", Ty.path "u64", [], "min", [] |),
                    [
                      M.rust_cast
                        (M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "revm_interpreter::gas::Gas",
                            "refunded",
                            []
                          |),
                          [ M.read (| self |) ]
                        |));
                      BinOp.Wrap.div (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "revm_interpreter::gas::Gas",
                            "spent",
                            []
                          |),
                          [ M.read (| self |) ]
                        |),
                        M.read (| max_refund_quotient |)
                      |)
                    ]
                  |))
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_set_final_refund :
      M.IsAssociatedFunction Self "set_final_refund" set_final_refund.
    
    (*
        pub fn set_refund(&mut self, refund: i64) {
            self.refunded = refund;
        }
    *)
    Definition set_refund (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; refund ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let refund := M.alloc (| refund |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::gas::Gas",
                  "refunded"
                |),
                M.read (| refund |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_set_refund : M.IsAssociatedFunction Self "set_refund" set_refund.
    
    (*
        pub fn record_cost(&mut self, cost: u64) -> bool {
            let (remaining, overflow) = self.remaining.overflowing_sub(cost);
            let success = !overflow;
            if success {
                self.remaining = remaining;
            }
            success
        }
    *)
    Definition record_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; cost ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let cost := M.alloc (| cost |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "overflowing_sub", [] |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::gas::Gas",
                        "remaining"
                      |)
                    |);
                    M.read (| cost |)
                  ]
                |)
              |),
              [
                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 remaining := M.copy (| γ0_0 |) in
                    let overflow := M.copy (| γ0_1 |) in
                    let~ success := M.alloc (| UnOp.not (| M.read (| overflow |) |) |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.use success in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ _ :=
                                M.write (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm_interpreter::gas::Gas",
                                    "remaining"
                                  |),
                                  M.read (| remaining |)
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    success))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_record_cost : M.IsAssociatedFunction Self "record_cost" record_cost.
  End Impl_revm_interpreter_gas_Gas.
End gas.
