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

Module gas.
  Module calc.
    (*
    pub fn sstore_refund(spec_id: SpecId, original: U256, current: U256, new: U256) -> i64 {
        if spec_id.is_enabled_in(SpecId::ISTANBUL) {
            // EIP-3529: Reduction in refunds
            let sstore_clears_schedule = if spec_id.is_enabled_in(SpecId::LONDON) {
                (SSTORE_RESET - COLD_SLOAD_COST + ACCESS_LIST_STORAGE_KEY) as i64
            } else {
                REFUND_SSTORE_CLEARS
            };
            if current == new {
                0
            } else {
                if original == current && new == U256::ZERO {
                    sstore_clears_schedule
                } else {
                    let mut refund = 0;
    
                    if original != U256::ZERO {
                        if current == U256::ZERO {
                            refund -= sstore_clears_schedule;
                        } else if new == U256::ZERO {
                            refund += sstore_clears_schedule;
                        }
                    }
    
                    if original == new {
                        let (gas_sstore_reset, gas_sload) = if spec_id.is_enabled_in(SpecId::BERLIN) {
                            (SSTORE_RESET - COLD_SLOAD_COST, WARM_STORAGE_READ_COST)
                        } else {
                            (SSTORE_RESET, sload_cost(spec_id, false))
                        };
                        if original == U256::ZERO {
                            refund += (SSTORE_SET - gas_sload) as i64;
                        } else {
                            refund += (gas_sstore_reset - gas_sload) as i64;
                        }
                    }
    
                    refund
                }
            }
        } else {
            if current != U256::ZERO && new == U256::ZERO {
                REFUND_SSTORE_CLEARS
            } else {
                0
            }
        }
    }
    *)
    Definition sstore_refund (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ spec_id; original; current; new ] =>
        ltac:(M.monadic
          (let spec_id := M.alloc (| spec_id |) in
          let original := M.alloc (| original |) in
          let current := M.alloc (| current |) in
          let new := M.alloc (| new |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "revm_primitives::specification::SpecId",
                              "is_enabled_in",
                              []
                            |),
                            [
                              M.read (| spec_id |);
                              Value.StructTuple
                                "revm_primitives::specification::SpecId::ISTANBUL"
                                []
                            ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ sstore_clears_schedule :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm_primitives::specification::SpecId",
                                          "is_enabled_in",
                                          []
                                        |),
                                        [
                                          M.read (| spec_id |);
                                          Value.StructTuple
                                            "revm_primitives::specification::SpecId::LONDON"
                                            []
                                        ]
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.rust_cast
                                    (BinOp.Wrap.add (|
                                      BinOp.Wrap.sub (|
                                        M.read (|
                                          M.get_constant (|
                                            "revm_interpreter::gas::constants::SSTORE_RESET"
                                          |)
                                        |),
                                        M.read (|
                                          M.get_constant (|
                                            "revm_interpreter::gas::constants::COLD_SLOAD_COST"
                                          |)
                                        |)
                                      |),
                                      M.read (|
                                        M.get_constant (|
                                          "revm_interpreter::gas::constants::ACCESS_LIST_STORAGE_KEY"
                                        |)
                                      |)
                                    |))
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.get_constant (|
                                  "revm_interpreter::gas::constants::REFUND_SSTORE_CLEARS"
                                |)))
                          ]
                        |)
                      |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [],
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          []
                                      ],
                                      "eq",
                                      []
                                    |),
                                    [ current; new ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (| Value.Integer IntegerKind.I64 0 |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          LogicalOp.and (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::cmp::PartialEq",
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [],
                                                [
                                                  Ty.apply
                                                    (Ty.path "ruint::Uint")
                                                    [
                                                      Value.Integer IntegerKind.Usize 256;
                                                      Value.Integer IntegerKind.Usize 4
                                                    ]
                                                    []
                                                ],
                                                "eq",
                                                []
                                              |),
                                              [ original; current ]
                                            |),
                                            ltac:(M.monadic
                                              (M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::cmp::PartialEq",
                                                  Ty.apply
                                                    (Ty.path "ruint::Uint")
                                                    [
                                                      Value.Integer IntegerKind.Usize 256;
                                                      Value.Integer IntegerKind.Usize 4
                                                    ]
                                                    [],
                                                  [
                                                    Ty.apply
                                                      (Ty.path "ruint::Uint")
                                                      [
                                                        Value.Integer IntegerKind.Usize 256;
                                                        Value.Integer IntegerKind.Usize 4
                                                      ]
                                                      []
                                                  ],
                                                  "eq",
                                                  []
                                                |),
                                                [ new; M.get_constant (| "ruint::ZERO" |) ]
                                              |)))
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    sstore_clears_schedule));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let~ refund := M.alloc (| Value.Integer IntegerKind.I64 0 |) in
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::cmp::PartialEq",
                                                        Ty.apply
                                                          (Ty.path "ruint::Uint")
                                                          [
                                                            Value.Integer IntegerKind.Usize 256;
                                                            Value.Integer IntegerKind.Usize 4
                                                          ]
                                                          [],
                                                        [
                                                          Ty.apply
                                                            (Ty.path "ruint::Uint")
                                                            [
                                                              Value.Integer IntegerKind.Usize 256;
                                                              Value.Integer IntegerKind.Usize 4
                                                            ]
                                                            []
                                                        ],
                                                        "ne",
                                                        []
                                                      |),
                                                      [ original; M.get_constant (| "ruint::ZERO" |)
                                                      ]
                                                    |)
                                                  |)) 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 (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::cmp::PartialEq",
                                                                Ty.apply
                                                                  (Ty.path "ruint::Uint")
                                                                  [
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      256;
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      4
                                                                  ]
                                                                  [],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "ruint::Uint")
                                                                    [
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        256;
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        4
                                                                    ]
                                                                    []
                                                                ],
                                                                "eq",
                                                                []
                                                              |),
                                                              [
                                                                current;
                                                                M.get_constant (| "ruint::ZERO" |)
                                                              ]
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      let~ _ :=
                                                        let β := refund in
                                                        M.write (|
                                                          β,
                                                          BinOp.Wrap.sub (|
                                                            M.read (| β |),
                                                            M.read (| sstore_clears_schedule |)
                                                          |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::cmp::PartialEq",
                                                                        Ty.apply
                                                                          (Ty.path "ruint::Uint")
                                                                          [
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              256;
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              4
                                                                          ]
                                                                          [],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "ruint::Uint")
                                                                            [
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                256;
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                4
                                                                            ]
                                                                            []
                                                                        ],
                                                                        "eq",
                                                                        []
                                                                      |),
                                                                      [
                                                                        new;
                                                                        M.get_constant (|
                                                                          "ruint::ZERO"
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |)) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              let~ _ :=
                                                                let β := refund in
                                                                M.write (|
                                                                  β,
                                                                  BinOp.Wrap.add (|
                                                                    M.read (| β |),
                                                                    M.read (|
                                                                      sstore_clears_schedule
                                                                    |)
                                                                  |)
                                                                |) in
                                                              M.alloc (| 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 (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::cmp::PartialEq",
                                                        Ty.apply
                                                          (Ty.path "ruint::Uint")
                                                          [
                                                            Value.Integer IntegerKind.Usize 256;
                                                            Value.Integer IntegerKind.Usize 4
                                                          ]
                                                          [],
                                                        [
                                                          Ty.apply
                                                            (Ty.path "ruint::Uint")
                                                            [
                                                              Value.Integer IntegerKind.Usize 256;
                                                              Value.Integer IntegerKind.Usize 4
                                                            ]
                                                            []
                                                        ],
                                                        "eq",
                                                        []
                                                      |),
                                                      [ original; new ]
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.match_operator (|
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.use
                                                            (M.alloc (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path
                                                                    "revm_primitives::specification::SpecId",
                                                                  "is_enabled_in",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (| spec_id |);
                                                                  Value.StructTuple
                                                                    "revm_primitives::specification::SpecId::BERLIN"
                                                                    []
                                                                ]
                                                              |)
                                                            |)) in
                                                        let _ :=
                                                          M.is_constant_or_break_match (|
                                                            M.read (| γ |),
                                                            Value.Bool true
                                                          |) in
                                                        M.alloc (|
                                                          Value.Tuple
                                                            [
                                                              BinOp.Wrap.sub (|
                                                                M.read (|
                                                                  M.get_constant (|
                                                                    "revm_interpreter::gas::constants::SSTORE_RESET"
                                                                  |)
                                                                |),
                                                                M.read (|
                                                                  M.get_constant (|
                                                                    "revm_interpreter::gas::constants::COLD_SLOAD_COST"
                                                                  |)
                                                                |)
                                                              |);
                                                              M.read (|
                                                                M.get_constant (|
                                                                  "revm_interpreter::gas::constants::WARM_STORAGE_READ_COST"
                                                                |)
                                                              |)
                                                            ]
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.alloc (|
                                                          Value.Tuple
                                                            [
                                                              M.read (|
                                                                M.get_constant (|
                                                                  "revm_interpreter::gas::constants::SSTORE_RESET"
                                                                |)
                                                              |);
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "revm_interpreter::gas::calc::sload_cost",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (| spec_id |);
                                                                  Value.Bool false
                                                                ]
                                                              |)
                                                            ]
                                                        |)))
                                                  ]
                                                |),
                                                [
                                                  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 gas_sstore_reset := M.copy (| γ0_0 |) in
                                                      let gas_sload := M.copy (| γ0_1 |) in
                                                      M.match_operator (|
                                                        M.alloc (| Value.Tuple [] |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ :=
                                                                M.use
                                                                  (M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::cmp::PartialEq",
                                                                        Ty.apply
                                                                          (Ty.path "ruint::Uint")
                                                                          [
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              256;
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              4
                                                                          ]
                                                                          [],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "ruint::Uint")
                                                                            [
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                256;
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                4
                                                                            ]
                                                                            []
                                                                        ],
                                                                        "eq",
                                                                        []
                                                                      |),
                                                                      [
                                                                        original;
                                                                        M.get_constant (|
                                                                          "ruint::ZERO"
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |)) in
                                                              let _ :=
                                                                M.is_constant_or_break_match (|
                                                                  M.read (| γ |),
                                                                  Value.Bool true
                                                                |) in
                                                              let~ _ :=
                                                                let β := refund in
                                                                M.write (|
                                                                  β,
                                                                  BinOp.Wrap.add (|
                                                                    M.read (| β |),
                                                                    M.rust_cast
                                                                      (BinOp.Wrap.sub (|
                                                                        M.read (|
                                                                          M.get_constant (|
                                                                            "revm_interpreter::gas::constants::SSTORE_SET"
                                                                          |)
                                                                        |),
                                                                        M.read (| gas_sload |)
                                                                      |))
                                                                  |)
                                                                |) in
                                                              M.alloc (| Value.Tuple [] |)));
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let~ _ :=
                                                                let β := refund in
                                                                M.write (|
                                                                  β,
                                                                  BinOp.Wrap.add (|
                                                                    M.read (| β |),
                                                                    M.rust_cast
                                                                      (BinOp.Wrap.sub (|
                                                                        M.read (|
                                                                          gas_sstore_reset
                                                                        |),
                                                                        M.read (| gas_sload |)
                                                                      |))
                                                                  |)
                                                                |) in
                                                              M.alloc (| Value.Tuple [] |)))
                                                        ]
                                                      |)))
                                                ]
                                              |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    refund))
                              ]
                            |)))
                      ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  LogicalOp.and (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            []
                                        ],
                                        "ne",
                                        []
                                      |),
                                      [ current; M.get_constant (| "ruint::ZERO" |) ]
                                    |),
                                    ltac:(M.monadic
                                      (M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [],
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              []
                                          ],
                                          "eq",
                                          []
                                        |),
                                        [ new; M.get_constant (| "ruint::ZERO" |) ]
                                      |)))
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.get_constant (|
                              "revm_interpreter::gas::constants::REFUND_SSTORE_CLEARS"
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.I64 0 |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_sstore_refund :
      M.IsFunction "revm_interpreter::gas::calc::sstore_refund" sstore_refund.
    
    (*
    pub const fn create2_cost(len: u64) -> Option<u64> {
        CREATE.checked_add(tri!(cost_per_word(len, KECCAK256WORD)))
    }
    *)
    Definition create2_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ len ] =>
        ltac:(M.monadic
          (let len := M.alloc (| len |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.call_closure (|
                M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                [
                  M.read (| M.get_constant (| "revm_interpreter::gas::constants::CREATE" |) |);
                  M.read (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "revm_interpreter::gas::calc::cost_per_word", [] |),
                          [
                            M.read (| len |);
                            M.read (|
                              M.get_constant (| "revm_interpreter::gas::constants::KECCAK256WORD" |)
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let v := M.copy (| γ0_0 |) in
                            v));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |)
                ]
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_create2_cost :
      M.IsFunction "revm_interpreter::gas::calc::create2_cost" create2_cost.
    
    (*
    const fn log2floor(value: U256) -> u64 {
        let mut l: u64 = 256;
        let mut i = 3;
        loop {
            if value.as_limbs()[i] == 0u64 {
                l -= 64;
            } else {
                l -= value.as_limbs()[i].leading_zeros() as u64;
                if l == 0 {
                    return l;
                } else {
                    return l - 1;
                }
            }
            if i == 0 {
                break;
            }
            i -= 1;
        }
        l
    }
    *)
    Definition log2floor (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ l := M.alloc (| Value.Integer IntegerKind.U64 256 |) in
                let~ i := M.alloc (| Value.Integer IntegerKind.Usize 3 |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.eq (|
                                        M.read (|
                                          M.SubPointer.get_array_field (|
                                            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",
                                                []
                                              |),
                                              [ value ]
                                            |),
                                            i
                                          |)
                                        |),
                                        Value.Integer IntegerKind.U64 0
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ _ :=
                                  let β := l in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.sub (|
                                      M.read (| β |),
                                      Value.Integer IntegerKind.U64 64
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let~ _ :=
                                  let β := l in
                                  M.write (|
                                    β,
                                    BinOp.Wrap.sub (|
                                      M.read (| β |),
                                      M.rust_cast
                                        (M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "u64",
                                            "leading_zeros",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_array_field (|
                                                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",
                                                    []
                                                  |),
                                                  [ value ]
                                                |),
                                                i
                                              |)
                                            |)
                                          ]
                                        |))
                                    |)
                                  |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.eq (|
                                                M.read (| l |),
                                                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 (| M.return_ (| M.read (| l |) |) |)
                                          |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                BinOp.Wrap.sub (|
                                                  M.read (| l |),
                                                  Value.Integer IntegerKind.U64 1
                                                |)
                                              |)
                                            |)
                                          |)
                                        |)))
                                  ]
                                |)))
                          ]
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.eq (|
                                        M.read (| i |),
                                        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.break (||) |) |) |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        let β := i in
                        M.write (|
                          β,
                          BinOp.Wrap.sub (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                        |) in
                      M.alloc (| Value.Tuple [] |)))
                  |) in
                l
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_log2floor : M.IsFunction "revm_interpreter::gas::calc::log2floor" log2floor.
    
    (*
    pub fn exp_cost(spec_id: SpecId, power: U256) -> Option<u64> {
        if power == U256::ZERO {
            Some(EXP)
        } else {
            // EIP-160: EXP cost increase
            let gas_byte = U256::from(if spec_id.is_enabled_in(SpecId::SPURIOUS_DRAGON) {
                50
            } else {
                10
            });
            let gas = U256::from(EXP)
                .checked_add(gas_byte.checked_mul(U256::from(log2floor(power) / 8 + 1))?)?;
    
            u64::try_from(gas).ok()
        }
    }
    *)
    Definition exp_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ spec_id; power ] =>
        ltac:(M.monadic
          (let spec_id := M.alloc (| spec_id |) in
          let power := M.alloc (| power |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [],
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                  "eq",
                                  []
                                |),
                                [ power; M.get_constant (| "ruint::ZERO" |) ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.read (|
                                M.get_constant (| "revm_interpreter::gas::constants::EXP" |)
                              |)
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ gas_byte :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [],
                                "from",
                                [ Ty.path "i32" ]
                              |),
                              [
                                M.read (|
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path
                                                      "revm_primitives::specification::SpecId",
                                                    "is_enabled_in",
                                                    []
                                                  |),
                                                  [
                                                    M.read (| spec_id |);
                                                    Value.StructTuple
                                                      "revm_primitives::specification::SpecId::SPURIOUS_DRAGON"
                                                      []
                                                  ]
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (| Value.Integer IntegerKind.I32 50 |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (M.alloc (| Value.Integer IntegerKind.I32 10 |)))
                                    ]
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let~ gas :=
                          M.copy (|
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::Try",
                                    Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          []
                                      ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        "checked_add",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [],
                                            "from",
                                            [ Ty.path "u64" ]
                                          |),
                                          [
                                            M.read (|
                                              M.get_constant (|
                                                "revm_interpreter::gas::constants::EXP"
                                              |)
                                            |)
                                          ]
                                        |);
                                        M.read (|
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::Try",
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "ruint::Uint")
                                                        [
                                                          Value.Integer IntegerKind.Usize 256;
                                                          Value.Integer IntegerKind.Usize 4
                                                        ]
                                                        []
                                                    ],
                                                  [],
                                                  "branch",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "ruint::Uint")
                                                        [
                                                          Value.Integer IntegerKind.Usize 256;
                                                          Value.Integer IntegerKind.Usize 4
                                                        ]
                                                        [],
                                                      "checked_mul",
                                                      []
                                                    |),
                                                    [
                                                      M.read (| gas_byte |);
                                                      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" ]
                                                        |),
                                                        [
                                                          BinOp.Wrap.add (|
                                                            BinOp.Wrap.div (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "revm_interpreter::gas::calc::log2floor",
                                                                  []
                                                                |),
                                                                [ M.read (| power |) ]
                                                              |),
                                                              Value.Integer IntegerKind.U64 8
                                                            |),
                                                            Value.Integer IntegerKind.U64 1
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Break",
                                                      0
                                                    |) in
                                                  let residual := M.copy (| γ0_0 |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::try_trait::FromResidual",
                                                              Ty.apply
                                                                (Ty.path "core::option::Option")
                                                                []
                                                                [ Ty.path "u64" ],
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "core::option::Option")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "core::convert::Infallible"
                                                                  ]
                                                              ],
                                                              "from_residual",
                                                              []
                                                            |),
                                                            [ M.read (| residual |) ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::ops::control_flow::ControlFlow::Continue",
                                                      0
                                                    |) in
                                                  let val := M.copy (| γ0_0 |) in
                                                  val))
                                            ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::ops::control_flow::ControlFlow::Break",
                                        0
                                      |) in
                                    let residual := M.copy (| γ0_0 |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          M.return_ (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::try_trait::FromResidual",
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [ Ty.path "u64" ],
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [ Ty.path "core::convert::Infallible" ]
                                                ],
                                                "from_residual",
                                                []
                                              |),
                                              [ M.read (| residual |) ]
                                            |)
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::ops::control_flow::ControlFlow::Continue",
                                        0
                                      |) in
                                    let val := M.copy (| γ0_0 |) in
                                    val))
                              ]
                            |)
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.path "u64";
                                  Ty.apply
                                    (Ty.path "ruint::from::FromUintError")
                                    []
                                    [ Ty.path "u64" ]
                                ],
                              "ok",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::convert::TryFrom",
                                  Ty.path "u64",
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                  "try_from",
                                  []
                                |),
                                [ M.read (| gas |) ]
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_exp_cost : M.IsFunction "revm_interpreter::gas::calc::exp_cost" exp_cost.
    
    (*
    pub const fn verylowcopy_cost(len: u64) -> Option<u64> {
        VERYLOW.checked_add(tri!(cost_per_word(len, COPY)))
    }
    *)
    Definition verylowcopy_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ len ] =>
        ltac:(M.monadic
          (let len := M.alloc (| len |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.call_closure (|
                M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                [
                  M.read (| M.get_constant (| "revm_interpreter::gas::constants::VERYLOW" |) |);
                  M.read (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "revm_interpreter::gas::calc::cost_per_word", [] |),
                          [
                            M.read (| len |);
                            M.read (|
                              M.get_constant (| "revm_interpreter::gas::constants::COPY" |)
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let v := M.copy (| γ0_0 |) in
                            v));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |)
                ]
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_verylowcopy_cost :
      M.IsFunction "revm_interpreter::gas::calc::verylowcopy_cost" verylowcopy_cost.
    
    (*
    pub const fn extcodecopy_cost(spec_id: SpecId, len: u64, is_cold: bool) -> Option<u64> {
        let base_gas = if spec_id.is_enabled_in(SpecId::BERLIN) {
            warm_cold_cost(is_cold)
        } else if spec_id.is_enabled_in(SpecId::TANGERINE) {
            700
        } else {
            20
        };
        base_gas.checked_add(tri!(cost_per_word(len, COPY)))
    }
    *)
    Definition extcodecopy_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ spec_id; len; is_cold ] =>
        ltac:(M.monadic
          (let spec_id := M.alloc (| spec_id |) in
          let len := M.alloc (| len |) in
          let is_cold := M.alloc (| is_cold |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ base_gas :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_primitives::specification::SpecId",
                                      "is_enabled_in",
                                      []
                                    |),
                                    [
                                      M.read (| spec_id |);
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::BERLIN"
                                        []
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "revm_interpreter::gas::calc::warm_cold_cost",
                                  []
                                |),
                                [ M.read (| is_cold |) ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "revm_primitives::specification::SpecId",
                                              "is_enabled_in",
                                              []
                                            |),
                                            [
                                              M.read (| spec_id |);
                                              Value.StructTuple
                                                "revm_primitives::specification::SpecId::TANGERINE"
                                                []
                                            ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (| Value.Integer IntegerKind.U64 700 |)));
                                fun γ =>
                                  ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 20 |)))
                              ]
                            |)))
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                    [
                      M.read (| base_gas |);
                      M.read (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (| "revm_interpreter::gas::calc::cost_per_word", [] |),
                              [
                                M.read (| len |);
                                M.read (|
                                  M.get_constant (| "revm_interpreter::gas::constants::COPY" |)
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let v := M.copy (| γ0_0 |) in
                                v));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        Value.StructTuple "core::option::Option::None" []
                                      |)
                                    |)
                                  |)
                                |)))
                          ]
                        |)
                      |)
                    ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_extcodecopy_cost :
      M.IsFunction "revm_interpreter::gas::calc::extcodecopy_cost" extcodecopy_cost.
    
    (*
    pub const fn log_cost(n: u8, len: u64) -> Option<u64> {
        tri!(LOG.checked_add(tri!(LOGDATA.checked_mul(len)))).checked_add(LOGTOPIC * n as u64)
    }
    *)
    Definition log_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n; len ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          let len := M.alloc (| len |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.call_closure (|
                M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                [
                  M.read (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                          [
                            M.read (|
                              M.get_constant (| "revm_interpreter::gas::constants::LOG" |)
                            |);
                            M.read (|
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "u64",
                                      "checked_mul",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.get_constant (|
                                          "revm_interpreter::gas::constants::LOGDATA"
                                        |)
                                      |);
                                      M.read (| len |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let v := M.copy (| γ0_0 |) in
                                      v));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              Value.StructTuple "core::option::Option::None" []
                                            |)
                                          |)
                                        |)
                                      |)))
                                ]
                              |)
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let v := M.copy (| γ0_0 |) in
                            v));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |);
                  BinOp.Wrap.mul (|
                    M.read (| M.get_constant (| "revm_interpreter::gas::constants::LOGTOPIC" |) |),
                    M.rust_cast (M.read (| n |))
                  |)
                ]
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_log_cost : M.IsFunction "revm_interpreter::gas::calc::log_cost" log_cost.
    
    (*
    pub const fn keccak256_cost(len: u64) -> Option<u64> {
        KECCAK256.checked_add(tri!(cost_per_word(len, KECCAK256WORD)))
    }
    *)
    Definition keccak256_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ len ] =>
        ltac:(M.monadic
          (let len := M.alloc (| len |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.call_closure (|
                M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                [
                  M.read (| M.get_constant (| "revm_interpreter::gas::constants::KECCAK256" |) |);
                  M.read (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "revm_interpreter::gas::calc::cost_per_word", [] |),
                          [
                            M.read (| len |);
                            M.read (|
                              M.get_constant (| "revm_interpreter::gas::constants::KECCAK256WORD" |)
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::option::Option::Some",
                                0
                              |) in
                            let v := M.copy (| γ0_0 |) in
                            v));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |)
                ]
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_keccak256_cost :
      M.IsFunction "revm_interpreter::gas::calc::keccak256_cost" keccak256_cost.
    
    (*
    pub const fn cost_per_word(len: u64, multiple: u64) -> Option<u64> {
        multiple.checked_mul(num_words(len))
    }
    *)
    Definition cost_per_word (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ len; multiple ] =>
        ltac:(M.monadic
          (let len := M.alloc (| len |) in
          let multiple := M.alloc (| multiple |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "u64", "checked_mul", [] |),
            [
              M.read (| multiple |);
              M.call_closure (|
                M.get_function (| "revm_interpreter::interpreter::shared_memory::num_words", [] |),
                [ M.read (| len |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_cost_per_word :
      M.IsFunction "revm_interpreter::gas::calc::cost_per_word" cost_per_word.
    
    (*
    pub const fn initcode_cost(len: u64) -> u64 {
        let Some(cost) = cost_per_word(len, INITCODE_WORD_COST) else {
            panic!("initcode cost overflow")
        };
        cost
    }
    *)
    Definition initcode_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ len ] =>
        ltac:(M.monadic
          (let len := M.alloc (| len |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "revm_interpreter::gas::calc::cost_per_word", [] |),
                  [
                    M.read (| len |);
                    M.read (|
                      M.get_constant (| "revm_interpreter::gas::constants::INITCODE_WORD_COST" |)
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let cost := M.copy (| γ0_0 |) in
                    cost))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_initcode_cost :
      M.IsFunction "revm_interpreter::gas::calc::initcode_cost" initcode_cost.
    
    (*
    pub const fn sload_cost(spec_id: SpecId, is_cold: bool) -> u64 {
        if spec_id.is_enabled_in(SpecId::BERLIN) {
            if is_cold {
                COLD_SLOAD_COST
            } else {
                WARM_STORAGE_READ_COST
            }
        } else if spec_id.is_enabled_in(SpecId::ISTANBUL) {
            // EIP-1884: Repricing for trie-size-dependent opcodes
            INSTANBUL_SLOAD_GAS
        } else if spec_id.is_enabled_in(SpecId::TANGERINE) {
            // EIP-150: Gas cost changes for IO-heavy operations
            200
        } else {
            50
        }
    }
    *)
    Definition sload_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ spec_id; is_cold ] =>
        ltac:(M.monadic
          (let spec_id := M.alloc (| spec_id |) in
          let is_cold := M.alloc (| is_cold |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "revm_primitives::specification::SpecId",
                              "is_enabled_in",
                              []
                            |),
                            [
                              M.read (| spec_id |);
                              Value.StructTuple "revm_primitives::specification::SpecId::BERLIN" []
                            ]
                          |)
                        |)) 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 is_cold in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.get_constant (|
                              "revm_interpreter::gas::constants::COLD_SLOAD_COST"
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.get_constant (|
                              "revm_interpreter::gas::constants::WARM_STORAGE_READ_COST"
                            |)))
                      ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_primitives::specification::SpecId",
                                      "is_enabled_in",
                                      []
                                    |),
                                    [
                                      M.read (| spec_id |);
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::ISTANBUL"
                                        []
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.get_constant (|
                              "revm_interpreter::gas::constants::INSTANBUL_SLOAD_GAS"
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "revm_primitives::specification::SpecId",
                                              "is_enabled_in",
                                              []
                                            |),
                                            [
                                              M.read (| spec_id |);
                                              Value.StructTuple
                                                "revm_primitives::specification::SpecId::TANGERINE"
                                                []
                                            ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (| Value.Integer IntegerKind.U64 200 |)));
                                fun γ =>
                                  ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 50 |)))
                              ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_sload_cost : M.IsFunction "revm_interpreter::gas::calc::sload_cost" sload_cost.
    
    (*
    pub fn sstore_cost(
        spec_id: SpecId,
        original: U256,
        current: U256,
        new: U256,
        gas: u64,
        is_cold: bool,
    ) -> Option<u64> {
        // EIP-1706 Disable SSTORE with gasleft lower than call stipend
        if spec_id.is_enabled_in(SpecId::ISTANBUL) && gas <= CALL_STIPEND {
            return None;
        }
    
        if spec_id.is_enabled_in(SpecId::BERLIN) {
            // Berlin specification logic
            let mut gas_cost = istanbul_sstore_cost::<WARM_STORAGE_READ_COST, WARM_SSTORE_RESET>(
                original, current, new,
            );
    
            if is_cold {
                gas_cost += COLD_SLOAD_COST;
            }
            Some(gas_cost)
        } else if spec_id.is_enabled_in(SpecId::ISTANBUL) {
            // Istanbul logic
            Some(istanbul_sstore_cost::<INSTANBUL_SLOAD_GAS, SSTORE_RESET>(
                original, current, new,
            ))
        } else {
            // Frontier logic
            Some(frontier_sstore_cost(current, new))
        }
    }
    *)
    Definition sstore_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ spec_id; original; current; new; gas; is_cold ] =>
        ltac:(M.monadic
          (let spec_id := M.alloc (| spec_id |) in
          let original := M.alloc (| original |) in
          let current := M.alloc (| current |) in
          let new := M.alloc (| new |) in
          let gas := M.alloc (| gas |) in
          let is_cold := M.alloc (| is_cold |) 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 (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_primitives::specification::SpecId",
                                      "is_enabled_in",
                                      []
                                    |),
                                    [
                                      M.read (| spec_id |);
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::ISTANBUL"
                                        []
                                    ]
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.le (|
                                      M.read (| gas |),
                                      M.read (|
                                        M.get_constant (|
                                          "revm_interpreter::gas::constants::CALL_STIPEND"
                                        |)
                                      |)
                                    |)))
                                |)
                              |)) 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.StructTuple "core::option::Option::None" [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::specification::SpecId",
                                  "is_enabled_in",
                                  []
                                |),
                                [
                                  M.read (| spec_id |);
                                  Value.StructTuple
                                    "revm_primitives::specification::SpecId::BERLIN"
                                    []
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ gas_cost :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_function (|
                                "revm_interpreter::gas::calc::istanbul_sstore_cost",
                                []
                              |),
                              [ M.read (| original |); M.read (| current |); M.read (| new |) ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ := M.use is_cold in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    let β := gas_cost in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.add (|
                                        M.read (| β |),
                                        M.read (|
                                          M.get_constant (|
                                            "revm_interpreter::gas::constants::COLD_SLOAD_COST"
                                          |)
                                        |)
                                      |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (|
                          Value.StructTuple "core::option::Option::Some" [ M.read (| gas_cost |) ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm_primitives::specification::SpecId",
                                          "is_enabled_in",
                                          []
                                        |),
                                        [
                                          M.read (| spec_id |);
                                          Value.StructTuple
                                            "revm_primitives::specification::SpecId::ISTANBUL"
                                            []
                                        ]
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  Value.StructTuple
                                    "core::option::Option::Some"
                                    [
                                      M.call_closure (|
                                        M.get_function (|
                                          "revm_interpreter::gas::calc::istanbul_sstore_cost",
                                          []
                                        |),
                                        [
                                          M.read (| original |);
                                          M.read (| current |);
                                          M.read (| new |)
                                        ]
                                      |)
                                    ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  Value.StructTuple
                                    "core::option::Option::Some"
                                    [
                                      M.call_closure (|
                                        M.get_function (|
                                          "revm_interpreter::gas::calc::frontier_sstore_cost",
                                          []
                                        |),
                                        [ M.read (| current |); M.read (| new |) ]
                                      |)
                                    ]
                                |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_sstore_cost :
      M.IsFunction "revm_interpreter::gas::calc::sstore_cost" sstore_cost.
    
    (*
    fn istanbul_sstore_cost<const SLOAD_GAS: u64, const SSTORE_RESET_GAS: u64>(
        original: U256,
        current: U256,
        new: U256,
    ) -> u64 {
        if new == current {
            SLOAD_GAS
        } else if original == current && original == U256::ZERO {
            SSTORE_SET
        } else if original == current {
            SSTORE_RESET_GAS
        } else {
            SLOAD_GAS
        }
    }
    *)
    Definition istanbul_sstore_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [ SLOAD_GAS; SSTORE_RESET_GAS ], [], [ original; current; new ] =>
        ltac:(M.monadic
          (let original := M.alloc (| original |) in
          let current := M.alloc (| current |) in
          let new := M.alloc (| new |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::cmp::PartialEq",
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [],
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  []
                              ],
                              "eq",
                              []
                            |),
                            [ new; current ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.get_constant (|
                      "revm_interpreter::gas::calc::istanbul_sstore_cost::SLOAD_GAS"
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  LogicalOp.and (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            []
                                        ],
                                        "eq",
                                        []
                                      |),
                                      [ original; current ]
                                    |),
                                    ltac:(M.monadic
                                      (M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [],
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              []
                                          ],
                                          "eq",
                                          []
                                        |),
                                        [ original; M.get_constant (| "ruint::ZERO" |) ]
                                      |)))
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.get_constant (| "revm_interpreter::gas::constants::SSTORE_SET" |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::cmp::PartialEq",
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [],
                                              [
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  []
                                              ],
                                              "eq",
                                              []
                                            |),
                                            [ original; current ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.get_constant (|
                                      "revm_interpreter::gas::calc::istanbul_sstore_cost::SSTORE_RESET_GAS"
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.get_constant (|
                                      "revm_interpreter::gas::calc::istanbul_sstore_cost::SLOAD_GAS"
                                    |)))
                              ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_istanbul_sstore_cost :
      M.IsFunction "revm_interpreter::gas::calc::istanbul_sstore_cost" istanbul_sstore_cost.
    
    (*
    fn frontier_sstore_cost(current: U256, new: U256) -> u64 {
        if current == U256::ZERO && new != U256::ZERO {
            SSTORE_SET
        } else {
            SSTORE_RESET
        }
    }
    *)
    Definition frontier_sstore_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ current; new ] =>
        ltac:(M.monadic
          (let current := M.alloc (| current |) in
          let new := M.alloc (| new |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          LogicalOp.and (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::cmp::PartialEq",
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [],
                                [
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    []
                                ],
                                "eq",
                                []
                              |),
                              [ current; M.get_constant (| "ruint::ZERO" |) ]
                            |),
                            ltac:(M.monadic
                              (M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [],
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                  "ne",
                                  []
                                |),
                                [ new; M.get_constant (| "ruint::ZERO" |) ]
                              |)))
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.get_constant (| "revm_interpreter::gas::constants::SSTORE_SET" |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.get_constant (| "revm_interpreter::gas::constants::SSTORE_RESET" |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_frontier_sstore_cost :
      M.IsFunction "revm_interpreter::gas::calc::frontier_sstore_cost" frontier_sstore_cost.
    
    (*
    pub const fn selfdestruct_cost(spec_id: SpecId, res: SelfDestructResult) -> u64 {
        // EIP-161: State trie clearing (invariant-preserving alternative)
        let should_charge_topup = if spec_id.is_enabled_in(SpecId::SPURIOUS_DRAGON) {
            res.had_value && !res.target_exists
        } else {
            !res.target_exists
        };
    
        // EIP-150: Gas cost changes for IO-heavy operations
        let selfdestruct_gas_topup = if spec_id.is_enabled_in(SpecId::TANGERINE) && should_charge_topup
        {
            25000
        } else {
            0
        };
    
        // EIP-150: Gas cost changes for IO-heavy operations
        let selfdestruct_gas = if spec_id.is_enabled_in(SpecId::TANGERINE) {
            5000
        } else {
            0
        };
    
        let mut gas = selfdestruct_gas + selfdestruct_gas_topup;
        if spec_id.is_enabled_in(SpecId::BERLIN) && res.is_cold {
            gas += COLD_ACCOUNT_ACCESS_COST
        }
        gas
    }
    *)
    Definition selfdestruct_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ spec_id; res ] =>
        ltac:(M.monadic
          (let spec_id := M.alloc (| spec_id |) in
          let res := M.alloc (| res |) in
          M.read (|
            let~ should_charge_topup :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::specification::SpecId",
                                  "is_enabled_in",
                                  []
                                |),
                                [
                                  M.read (| spec_id |);
                                  Value.StructTuple
                                    "revm_primitives::specification::SpecId::SPURIOUS_DRAGON"
                                    []
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          LogicalOp.and (|
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                res,
                                "revm_interpreter::host::SelfDestructResult",
                                "had_value"
                              |)
                            |),
                            ltac:(M.monadic
                              (UnOp.not (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    res,
                                    "revm_interpreter::host::SelfDestructResult",
                                    "target_exists"
                                  |)
                                |)
                              |)))
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          UnOp.not (|
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                res,
                                "revm_interpreter::host::SelfDestructResult",
                                "target_exists"
                              |)
                            |)
                          |)
                        |)))
                  ]
                |)
              |) in
            let~ selfdestruct_gas_topup :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              LogicalOp.and (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "revm_primitives::specification::SpecId",
                                    "is_enabled_in",
                                    []
                                  |),
                                  [
                                    M.read (| spec_id |);
                                    Value.StructTuple
                                      "revm_primitives::specification::SpecId::TANGERINE"
                                      []
                                  ]
                                |),
                                ltac:(M.monadic (M.read (| should_charge_topup |)))
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.Integer IntegerKind.U64 25000 |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 0 |)))
                  ]
                |)
              |) in
            let~ selfdestruct_gas :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::specification::SpecId",
                                  "is_enabled_in",
                                  []
                                |),
                                [
                                  M.read (| spec_id |);
                                  Value.StructTuple
                                    "revm_primitives::specification::SpecId::TANGERINE"
                                    []
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.Integer IntegerKind.U64 5000 |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 0 |)))
                  ]
                |)
              |) in
            let~ gas :=
              M.alloc (|
                BinOp.Wrap.add (|
                  M.read (| selfdestruct_gas |),
                  M.read (| selfdestruct_gas_topup |)
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            LogicalOp.and (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::specification::SpecId",
                                  "is_enabled_in",
                                  []
                                |),
                                [
                                  M.read (| spec_id |);
                                  Value.StructTuple
                                    "revm_primitives::specification::SpecId::BERLIN"
                                    []
                                ]
                              |),
                              ltac:(M.monadic
                                (M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    res,
                                    "revm_interpreter::host::SelfDestructResult",
                                    "is_cold"
                                  |)
                                |)))
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let β := gas in
                      M.write (|
                        β,
                        BinOp.Wrap.add (|
                          M.read (| β |),
                          M.read (|
                            M.get_constant (|
                              "revm_interpreter::gas::constants::COLD_ACCOUNT_ACCESS_COST"
                            |)
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            gas
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_selfdestruct_cost :
      M.IsFunction "revm_interpreter::gas::calc::selfdestruct_cost" selfdestruct_cost.
    
    (*
    pub const fn call_cost(
        spec_id: SpecId,
        transfers_value: bool,
        is_cold: bool,
        new_account_accounting: bool,
    ) -> u64 {
        // Account access.
        let mut gas = if spec_id.is_enabled_in(SpecId::BERLIN) {
            warm_cold_cost(is_cold)
        } else if spec_id.is_enabled_in(SpecId::TANGERINE) {
            // EIP-150: Gas cost changes for IO-heavy operations
            700
        } else {
            40
        };
    
        // transfer value cost
        if transfers_value {
            gas += CALLVALUE;
        }
    
        // new account cost
        if new_account_accounting {
            // EIP-161: State trie clearing (invariant-preserving alternative)
            if spec_id.is_enabled_in(SpecId::SPURIOUS_DRAGON) {
                // account only if there is value transferred.
                if transfers_value {
                    gas += NEWACCOUNT;
                }
            } else {
                gas += NEWACCOUNT;
            }
        }
    
        gas
    }
    *)
    Definition call_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ spec_id; transfers_value; is_cold; new_account_accounting ] =>
        ltac:(M.monadic
          (let spec_id := M.alloc (| spec_id |) in
          let transfers_value := M.alloc (| transfers_value |) in
          let is_cold := M.alloc (| is_cold |) in
          let new_account_accounting := M.alloc (| new_account_accounting |) in
          M.read (|
            let~ gas :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::specification::SpecId",
                                  "is_enabled_in",
                                  []
                                |),
                                [
                                  M.read (| spec_id |);
                                  Value.StructTuple
                                    "revm_primitives::specification::SpecId::BERLIN"
                                    []
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (| "revm_interpreter::gas::calc::warm_cold_cost", [] |),
                            [ M.read (| is_cold |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm_primitives::specification::SpecId",
                                          "is_enabled_in",
                                          []
                                        |),
                                        [
                                          M.read (| spec_id |);
                                          Value.StructTuple
                                            "revm_primitives::specification::SpecId::TANGERINE"
                                            []
                                        ]
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (| Value.Integer IntegerKind.U64 700 |)));
                            fun γ =>
                              ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 40 |)))
                          ]
                        |)))
                  ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use transfers_value in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        let β := gas in
                        M.write (|
                          β,
                          BinOp.Wrap.add (|
                            M.read (| β |),
                            M.read (|
                              M.get_constant (| "revm_interpreter::gas::constants::CALLVALUE" |)
                            |)
                          |)
                        |) in
                      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 new_account_accounting 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 (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::specification::SpecId",
                                        "is_enabled_in",
                                        []
                                      |),
                                      [
                                        M.read (| spec_id |);
                                        Value.StructTuple
                                          "revm_primitives::specification::SpecId::SPURIOUS_DRAGON"
                                          []
                                      ]
                                    |)
                                  |)) 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 transfers_value in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ _ :=
                                        let β := gas in
                                        M.write (|
                                          β,
                                          BinOp.Wrap.add (|
                                            M.read (| β |),
                                            M.read (|
                                              M.get_constant (|
                                                "revm_interpreter::gas::constants::NEWACCOUNT"
                                              |)
                                            |)
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ _ :=
                                let β := gas in
                                M.write (|
                                  β,
                                  BinOp.Wrap.add (|
                                    M.read (| β |),
                                    M.read (|
                                      M.get_constant (|
                                        "revm_interpreter::gas::constants::NEWACCOUNT"
                                      |)
                                    |)
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                        ]
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            gas
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_call_cost : M.IsFunction "revm_interpreter::gas::calc::call_cost" call_cost.
    
    (*
    pub const fn warm_cold_cost(is_cold: bool) -> u64 {
        if is_cold {
            COLD_ACCOUNT_ACCESS_COST
        } else {
            WARM_STORAGE_READ_COST
        }
    }
    *)
    Definition warm_cold_cost (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ is_cold ] =>
        ltac:(M.monadic
          (let is_cold := M.alloc (| is_cold |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use is_cold in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.get_constant (|
                      "revm_interpreter::gas::constants::COLD_ACCOUNT_ACCESS_COST"
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.get_constant (|
                      "revm_interpreter::gas::constants::WARM_STORAGE_READ_COST"
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_warm_cold_cost :
      M.IsFunction "revm_interpreter::gas::calc::warm_cold_cost" warm_cold_cost.
    
    (*
    pub const fn memory_gas_for_len(len: usize) -> u64 {
        memory_gas(crate::interpreter::num_words(len as u64))
    }
    *)
    Definition memory_gas_for_len (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ len ] =>
        ltac:(M.monadic
          (let len := M.alloc (| len |) in
          M.call_closure (|
            M.get_function (| "revm_interpreter::gas::calc::memory_gas", [] |),
            [
              M.call_closure (|
                M.get_function (| "revm_interpreter::interpreter::shared_memory::num_words", [] |),
                [ M.rust_cast (M.read (| len |)) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_memory_gas_for_len :
      M.IsFunction "revm_interpreter::gas::calc::memory_gas_for_len" memory_gas_for_len.
    
    (*
    pub const fn memory_gas(num_words: u64) -> u64 {
        MEMORY
            .saturating_mul(num_words)
            .saturating_add(num_words.saturating_mul(num_words) / 512)
    }
    *)
    Definition memory_gas (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ num_words ] =>
        ltac:(M.monadic
          (let num_words := M.alloc (| num_words |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "u64", "saturating_add", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "u64", "saturating_mul", [] |),
                [
                  M.read (| M.get_constant (| "revm_interpreter::gas::constants::MEMORY" |) |);
                  M.read (| num_words |)
                ]
              |);
              BinOp.Wrap.div (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "saturating_mul", [] |),
                  [ M.read (| num_words |); M.read (| num_words |) ]
                |),
                Value.Integer IntegerKind.U64 512
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_memory_gas : M.IsFunction "revm_interpreter::gas::calc::memory_gas" memory_gas.
    
    (*
    pub fn validate_initial_tx_gas(
        spec_id: SpecId,
        input: &[u8],
        is_create: bool,
        access_list: &[(Address, Vec<U256>)],
        initcodes: &[Bytes],
    ) -> u64 {
        let mut initial_gas = 0;
        let mut zero_data_len = input.iter().filter(|v| **v == 0).count() as u64;
        let mut non_zero_data_len = input.len() as u64 - zero_data_len;
    
        // Enabling of initcode is checked in `validate_env` handler.
        for initcode in initcodes {
            let zeros = initcode.iter().filter(|v| **v == 0).count() as u64;
            zero_data_len += zeros;
            non_zero_data_len += initcode.len() as u64 - zeros;
        }
    
        // initdate stipend
        initial_gas += zero_data_len * TRANSACTION_ZERO_DATA;
        // EIP-2028: Transaction data gas cost reduction
        initial_gas += non_zero_data_len
            * if spec_id.is_enabled_in(SpecId::ISTANBUL) {
                16
            } else {
                68
            };
    
        // get number of access list account and storages.
        if spec_id.is_enabled_in(SpecId::BERLIN) {
            let accessed_slots = access_list
                .iter()
                .fold(0, |slot_count, (_, slots)| slot_count + slots.len() as u64);
            initial_gas += access_list.len() as u64 * ACCESS_LIST_ADDRESS;
            initial_gas += accessed_slots * ACCESS_LIST_STORAGE_KEY;
        }
    
        // base stipend
        initial_gas += if is_create {
            if spec_id.is_enabled_in(SpecId::HOMESTEAD) {
                // EIP-2: Homestead Hard-fork Changes
                53000
            } else {
                21000
            }
        } else {
            21000
        };
    
        // EIP-3860: Limit and meter initcode
        // Initcode stipend for bytecode analysis
        if spec_id.is_enabled_in(SpecId::SHANGHAI) && is_create {
            initial_gas += initcode_cost(input.len() as u64)
        }
    
        initial_gas
    }
    *)
    Definition validate_initial_tx_gas (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ spec_id; input; is_create; access_list; initcodes ] =>
        ltac:(M.monadic
          (let spec_id := M.alloc (| spec_id |) in
          let input := M.alloc (| input |) in
          let is_create := M.alloc (| is_create |) in
          let access_list := M.alloc (| access_list |) in
          let initcodes := M.alloc (| initcodes |) in
          M.read (|
            let~ initial_gas := M.alloc (| Value.Integer IntegerKind.U64 0 |) in
            let~ zero_data_len :=
              M.alloc (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Ty.apply
                        (Ty.path "core::iter::adapters::filter::Filter")
                        []
                        [
                          Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ]
                                ]
                            ]
                            (Ty.path "bool")
                        ],
                      [],
                      "count",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u8" ],
                          [],
                          "filter",
                          [
                            Ty.function
                              [
                                Ty.tuple
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ]
                                  ]
                              ]
                              (Ty.path "bool")
                          ]
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                              "iter",
                              []
                            |),
                            [ M.read (| input |) ]
                          |);
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [ α0 ] =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      M.alloc (| α0 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let v := M.copy (| γ |) in
                                            BinOp.eq (|
                                              M.read (| M.read (| M.read (| v |) |) |),
                                              Value.Integer IntegerKind.U8 0
                                            |)))
                                      ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        ]
                      |)
                    ]
                  |))
              |) in
            let~ non_zero_data_len :=
              M.alloc (|
                BinOp.Wrap.sub (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                        "len",
                        []
                      |),
                      [ M.read (| input |) ]
                    |)),
                  M.read (| zero_data_len |)
                |)
              |) in
            let~ _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [ Ty.path "alloy_primitives::bytes_::Bytes" ]
                          ],
                        [],
                        "into_iter",
                        []
                      |),
                      [ M.read (| initcodes |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::slice::iter::Iter")
                                        []
                                        [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ iter ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let initcode := M.copy (| γ0_0 |) in
                                      let~ zeros :=
                                        M.alloc (|
                                          M.rust_cast
                                            (M.call_closure (|
                                              M.get_trait_method (|
                                                "core::iter::traits::iterator::Iterator",
                                                Ty.apply
                                                  (Ty.path "core::iter::adapters::filter::Filter")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::slice::iter::Iter")
                                                      []
                                                      [ Ty.path "u8" ];
                                                    Ty.function
                                                      [
                                                        Ty.tuple
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "&")
                                                                  []
                                                                  [ Ty.path "u8" ]
                                                              ]
                                                          ]
                                                      ]
                                                      (Ty.path "bool")
                                                  ],
                                                [],
                                                "count",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::iterator::Iterator",
                                                    Ty.apply
                                                      (Ty.path "core::slice::iter::Iter")
                                                      []
                                                      [ Ty.path "u8" ],
                                                    [],
                                                    "filter",
                                                    [
                                                      Ty.function
                                                        [
                                                          Ty.tuple
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "&")
                                                                    []
                                                                    [ Ty.path "u8" ]
                                                                ]
                                                            ]
                                                        ]
                                                        (Ty.path "bool")
                                                    ]
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "slice")
                                                          []
                                                          [ Ty.path "u8" ],
                                                        "iter",
                                                        []
                                                      |),
                                                      [
                                                        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.read (| initcode |) ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |);
                                                    M.closure
                                                      (fun γ =>
                                                        ltac:(M.monadic
                                                          match γ with
                                                          | [ α0 ] =>
                                                            ltac:(M.monadic
                                                              (M.match_operator (|
                                                                M.alloc (| α0 |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let v := M.copy (| γ |) in
                                                                      BinOp.eq (|
                                                                        M.read (|
                                                                          M.read (|
                                                                            M.read (| v |)
                                                                          |)
                                                                        |),
                                                                        Value.Integer
                                                                          IntegerKind.U8
                                                                          0
                                                                      |)))
                                                                ]
                                                              |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  ]
                                                |)
                                              ]
                                            |))
                                        |) in
                                      let~ _ :=
                                        let β := zero_data_len in
                                        M.write (|
                                          β,
                                          BinOp.Wrap.add (| M.read (| β |), M.read (| zeros |) |)
                                        |) in
                                      let~ _ :=
                                        let β := non_zero_data_len in
                                        M.write (|
                                          β,
                                          BinOp.Wrap.add (|
                                            M.read (| β |),
                                            BinOp.Wrap.sub (|
                                              M.rust_cast
                                                (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.read (| initcode |) ]
                                                    |)
                                                  ]
                                                |)),
                                              M.read (| zeros |)
                                            |)
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ _ :=
              let β := initial_gas in
              M.write (|
                β,
                BinOp.Wrap.add (|
                  M.read (| β |),
                  BinOp.Wrap.mul (|
                    M.read (| zero_data_len |),
                    M.read (|
                      M.get_constant (| "revm_interpreter::gas::constants::TRANSACTION_ZERO_DATA" |)
                    |)
                  |)
                |)
              |) in
            let~ _ :=
              let β := initial_gas in
              M.write (|
                β,
                BinOp.Wrap.add (|
                  M.read (| β |),
                  BinOp.Wrap.mul (|
                    M.read (| non_zero_data_len |),
                    M.read (|
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::specification::SpecId",
                                        "is_enabled_in",
                                        []
                                      |),
                                      [
                                        M.read (| spec_id |);
                                        Value.StructTuple
                                          "revm_primitives::specification::SpecId::ISTANBUL"
                                          []
                                      ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (| Value.Integer IntegerKind.U64 16 |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 68 |)))
                        ]
                      |)
                    |)
                  |)
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm_primitives::specification::SpecId",
                                "is_enabled_in",
                                []
                              |),
                              [
                                M.read (| spec_id |);
                                Value.StructTuple
                                  "revm_primitives::specification::SpecId::BERLIN"
                                  []
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ accessed_slots :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply
                                (Ty.path "core::slice::iter::Iter")
                                []
                                [
                                  Ty.tuple
                                    [
                                      Ty.path "alloy_primitives::bits::address::Address";
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [];
                                          Ty.path "alloc::alloc::Global"
                                        ]
                                    ]
                                ],
                              [],
                              "fold",
                              [
                                Ty.path "u64";
                                Ty.function
                                  [
                                    Ty.tuple
                                      [
                                        Ty.path "u64";
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.tuple
                                              [
                                                Ty.path "alloy_primitives::bits::address::Address";
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "ruint::Uint")
                                                      [
                                                        Value.Integer IntegerKind.Usize 256;
                                                        Value.Integer IntegerKind.Usize 4
                                                      ]
                                                      [];
                                                    Ty.path "alloc::alloc::Global"
                                                  ]
                                              ]
                                          ]
                                      ]
                                  ]
                                  (Ty.path "u64")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    []
                                    [
                                      Ty.tuple
                                        [
                                          Ty.path "alloy_primitives::bits::address::Address";
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [];
                                              Ty.path "alloc::alloc::Global"
                                            ]
                                        ]
                                    ],
                                  "iter",
                                  []
                                |),
                                [ M.read (| access_list |) ]
                              |);
                              Value.Integer IntegerKind.U64 0;
                              M.closure
                                (fun γ =>
                                  ltac:(M.monadic
                                    match γ with
                                    | [ α0; α1 ] =>
                                      ltac:(M.monadic
                                        (M.match_operator (|
                                          M.alloc (| α0 |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let slot_count := M.copy (| γ |) in
                                                M.match_operator (|
                                                  M.alloc (| α1 |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ := M.read (| γ |) in
                                                        let γ1_0 :=
                                                          M.SubPointer.get_tuple_field (| γ, 0 |) in
                                                        let γ1_1 :=
                                                          M.SubPointer.get_tuple_field (| γ, 1 |) in
                                                        let slots := M.alloc (| γ1_1 |) in
                                                        BinOp.Wrap.add (|
                                                          M.read (| slot_count |),
                                                          M.rust_cast
                                                            (M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "alloc::vec::Vec")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path "ruint::Uint")
                                                                      [
                                                                        Value.Integer
                                                                          IntegerKind.Usize
                                                                          256;
                                                                        Value.Integer
                                                                          IntegerKind.Usize
                                                                          4
                                                                      ]
                                                                      [];
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ],
                                                                "len",
                                                                []
                                                              |),
                                                              [ M.read (| slots |) ]
                                                            |))
                                                        |)))
                                                  ]
                                                |)))
                                          ]
                                        |)))
                                    | _ => M.impossible "wrong number of arguments"
                                    end))
                            ]
                          |)
                        |) in
                      let~ _ :=
                        let β := initial_gas in
                        M.write (|
                          β,
                          BinOp.Wrap.add (|
                            M.read (| β |),
                            BinOp.Wrap.mul (|
                              M.rust_cast
                                (M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [
                                        Ty.tuple
                                          [
                                            Ty.path "alloy_primitives::bits::address::Address";
                                            Ty.apply
                                              (Ty.path "alloc::vec::Vec")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [];
                                                Ty.path "alloc::alloc::Global"
                                              ]
                                          ]
                                      ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| access_list |) ]
                                |)),
                              M.read (|
                                M.get_constant (|
                                  "revm_interpreter::gas::constants::ACCESS_LIST_ADDRESS"
                                |)
                              |)
                            |)
                          |)
                        |) in
                      let~ _ :=
                        let β := initial_gas in
                        M.write (|
                          β,
                          BinOp.Wrap.add (|
                            M.read (| β |),
                            BinOp.Wrap.mul (|
                              M.read (| accessed_slots |),
                              M.read (|
                                M.get_constant (|
                                  "revm_interpreter::gas::constants::ACCESS_LIST_STORAGE_KEY"
                                |)
                              |)
                            |)
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              let β := initial_gas in
              M.write (|
                β,
                BinOp.Wrap.add (|
                  M.read (| β |),
                  M.read (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.use is_create 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 (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "revm_primitives::specification::SpecId",
                                              "is_enabled_in",
                                              []
                                            |),
                                            [
                                              M.read (| spec_id |);
                                              Value.StructTuple
                                                "revm_primitives::specification::SpecId::HOMESTEAD"
                                                []
                                            ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (| Value.Integer IntegerKind.U64 53000 |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (| Value.Integer IntegerKind.U64 21000 |)))
                              ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 21000 |)))
                      ]
                    |)
                  |)
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            LogicalOp.and (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm_primitives::specification::SpecId",
                                  "is_enabled_in",
                                  []
                                |),
                                [
                                  M.read (| spec_id |);
                                  Value.StructTuple
                                    "revm_primitives::specification::SpecId::SHANGHAI"
                                    []
                                ]
                              |),
                              ltac:(M.monadic (M.read (| is_create |)))
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let β := initial_gas in
                      M.write (|
                        β,
                        BinOp.Wrap.add (|
                          M.read (| β |),
                          M.call_closure (|
                            M.get_function (| "revm_interpreter::gas::calc::initcode_cost", [] |),
                            [
                              M.rust_cast
                                (M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| input |) ]
                                |))
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            initial_gas
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_validate_initial_tx_gas :
      M.IsFunction "revm_interpreter::gas::calc::validate_initial_tx_gas" validate_initial_tx_gas.
  End calc.
End gas.
