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

Module handler.
  Module mainnet.
    Module validation.
      (*
      pub fn validate_env<SPEC: Spec, DB: Database>(env: &Env) -> Result<(), EVMError<DB::Error>> {
          // Important: validate block before tx.
          env.validate_block_env::<SPEC>()?;
          env.validate_tx::<SPEC>()?;
          Ok(())
      }
      *)
      Definition validate_env (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ SPEC; DB ], [ env ] =>
          ltac:(M.monadic
            (let env := M.alloc (| env |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [ Ty.tuple []; Ty.path "revm_primitives::result::InvalidHeader" ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm_primitives::env::Env",
                                "validate_block_env",
                                [ SPEC ]
                              |),
                              [ M.read (| env |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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::result::Result")
                                          []
                                          [
                                            Ty.tuple [];
                                            Ty.apply
                                              (Ty.path "revm_primitives::result::EVMError")
                                              []
                                              [ Ty.associated ]
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "revm_primitives::result::InvalidHeader"
                                            ]
                                        ],
                                        "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
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [ Ty.tuple []; Ty.path "revm_primitives::result::InvalidTransaction"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm_primitives::env::Env",
                                "validate_tx",
                                [ SPEC ]
                              |),
                              [ M.read (| env |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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::result::Result")
                                          []
                                          [
                                            Ty.tuple [];
                                            Ty.apply
                                              (Ty.path "revm_primitives::result::EVMError")
                                              []
                                              [ Ty.associated ]
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "revm_primitives::result::InvalidTransaction"
                                            ]
                                        ],
                                        "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 (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_validate_env :
        M.IsFunction "revm::handler::mainnet::validation::validate_env" validate_env.
      
      (*
      pub fn validate_tx_against_state<SPEC: Spec, EXT, DB: Database>(
          context: &mut Context<EXT, DB>,
      ) -> Result<(), EVMError<DB::Error>> {
          // load acc
          let tx_caller = context.evm.env.tx.caller;
          let (caller_account, _) = context
              .evm
              .inner
              .journaled_state
              .load_account(tx_caller, &mut context.evm.inner.db)?;
      
          context
              .evm
              .inner
              .env
              .validate_tx_against_state::<SPEC>(caller_account)
              .map_err(EVMError::Transaction)?;
      
          Ok(())
      }
      *)
      Definition validate_tx_against_state
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [ SPEC; EXT; DB ], [ context ] =>
          ltac:(M.monadic
            (let context := M.alloc (| context |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ tx_caller :=
                    M.copy (|
                      M.SubPointer.get_struct_record_field (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.apply
                                    (Ty.path "revm::context::evm_context::EvmContext")
                                    []
                                    [ DB ],
                                  [],
                                  "deref",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| context |),
                                    "revm::context::Context",
                                    "evm"
                                  |)
                                ]
                              |),
                              "revm::context::inner_evm_context::InnerEvmContext",
                              "env"
                            |)
                          |),
                          "revm_primitives::env::Env",
                          "tx"
                        |),
                        "revm_primitives::env::TxEnv",
                        "caller"
                      |)
                    |) in
                  M.match_operator (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.tuple
                                  [
                                    Ty.apply
                                      (Ty.path "&mut")
                                      []
                                      [ Ty.path "revm_primitives::state::Account" ];
                                    Ty.path "bool"
                                  ];
                                Ty.apply
                                  (Ty.path "revm_primitives::result::EVMError")
                                  []
                                  [ Ty.associated ]
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm::journaled_state::JournaledState",
                                "load_account",
                                [ DB ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| context |),
                                      "revm::context::Context",
                                      "evm"
                                    |),
                                    "revm::context::evm_context::EvmContext",
                                    "inner"
                                  |),
                                  "revm::context::inner_evm_context::InnerEvmContext",
                                  "journaled_state"
                                |);
                                M.read (| tx_caller |);
                                M.SubPointer.get_struct_record_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| context |),
                                      "revm::context::Context",
                                      "evm"
                                    |),
                                    "revm::context::evm_context::EvmContext",
                                    "inner"
                                  |),
                                  "revm::context::inner_evm_context::InnerEvmContext",
                                  "db"
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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::result::Result")
                                          []
                                          [
                                            Ty.tuple [];
                                            Ty.apply
                                              (Ty.path "revm_primitives::result::EVMError")
                                              []
                                              [ Ty.associated ]
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.apply
                                                (Ty.path "revm_primitives::result::EVMError")
                                                []
                                                [ Ty.associated ]
                                            ]
                                        ],
                                        "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_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let caller_account := M.copy (| γ0_0 |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::Try",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [
                                        Ty.tuple [];
                                        Ty.apply
                                          (Ty.path "revm_primitives::result::EVMError")
                                          []
                                          [ Ty.associated ]
                                      ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.tuple [];
                                            Ty.path "revm_primitives::result::InvalidTransaction"
                                          ],
                                        "map_err",
                                        [
                                          Ty.apply
                                            (Ty.path "revm_primitives::result::EVMError")
                                            []
                                            [ Ty.associated ];
                                          Ty.function
                                            [ Ty.path "revm_primitives::result::InvalidTransaction"
                                            ]
                                            (Ty.apply
                                              (Ty.path "revm_primitives::result::EVMError")
                                              []
                                              [ Ty.associated ])
                                        ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_primitives::env::Env",
                                            "validate_tx_against_state",
                                            [ SPEC ]
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| context |),
                                                    "revm::context::Context",
                                                    "evm"
                                                  |),
                                                  "revm::context::evm_context::EvmContext",
                                                  "inner"
                                                |),
                                                "revm::context::inner_evm_context::InnerEvmContext",
                                                "env"
                                              |)
                                            |);
                                            M.read (| caller_account |)
                                          ]
                                        |);
                                        M.constructor_as_closure
                                          "revm_primitives::result::EVMError::Transaction"
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                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::result::Result")
                                                  []
                                                  [
                                                    Ty.tuple [];
                                                    Ty.apply
                                                      (Ty.path "revm_primitives::result::EVMError")
                                                      []
                                                      [ Ty.associated ]
                                                  ],
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.path "core::convert::Infallible";
                                                      Ty.apply
                                                        (Ty.path
                                                          "revm_primitives::result::EVMError")
                                                        []
                                                        [ Ty.associated ]
                                                    ]
                                                ],
                                                "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 (|
                            Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_validate_tx_against_state :
        M.IsFunction
          "revm::handler::mainnet::validation::validate_tx_against_state"
          validate_tx_against_state.
      
      (*
      pub fn validate_initial_tx_gas<SPEC: Spec, DB: Database>(
          env: &Env,
      ) -> Result<u64, EVMError<DB::Error>> {
          let input = &env.tx.data;
          let is_create = env.tx.transact_to.is_create();
          let access_list = &env.tx.access_list;
          let initcodes = &env.tx.eof_initcodes;
      
          let initial_gas_spend =
              gas::validate_initial_tx_gas(SPEC::SPEC_ID, input, is_create, access_list, initcodes);
      
          // Additional check to see if limit is big enough to cover initial gas.
          if initial_gas_spend > env.tx.gas_limit {
              return Err(InvalidTransaction::CallGasCostMoreThanGasLimit.into());
          }
          Ok(initial_gas_spend)
      }
      *)
      Definition validate_initial_tx_gas
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [ SPEC; DB ], [ env ] =>
          ltac:(M.monadic
            (let env := M.alloc (| env |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ input :=
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| env |),
                          "revm_primitives::env::Env",
                          "tx"
                        |),
                        "revm_primitives::env::TxEnv",
                        "data"
                      |)
                    |) in
                  let~ is_create :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "revm_primitives::env::TransactTo",
                          "is_create",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| env |),
                              "revm_primitives::env::Env",
                              "tx"
                            |),
                            "revm_primitives::env::TxEnv",
                            "transact_to"
                          |)
                        ]
                      |)
                    |) in
                  let~ access_list :=
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| env |),
                          "revm_primitives::env::Env",
                          "tx"
                        |),
                        "revm_primitives::env::TxEnv",
                        "access_list"
                      |)
                    |) in
                  let~ initcodes :=
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| env |),
                          "revm_primitives::env::Env",
                          "tx"
                        |),
                        "revm_primitives::env::TxEnv",
                        "eof_initcodes"
                      |)
                    |) in
                  let~ initial_gas_spend :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "revm_interpreter::gas::calc::validate_initial_tx_gas",
                          []
                        |),
                        [
                          M.read (|
                            M.get_constant (| "revm_primitives::specification::Spec::SPEC_ID" |)
                          |);
                          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 (| input |) ]
                              |)
                            ]
                          |);
                          M.read (| is_create |);
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  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 "alloc::alloc::Global"
                                ],
                              [],
                              "deref",
                              []
                            |),
                            [ M.read (| access_list |) ]
                          |);
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.path "alloy_primitives::bytes_::Bytes";
                                  Ty.path "alloc::alloc::Global"
                                ],
                              [],
                              "deref",
                              []
                            |),
                            [ M.read (| initcodes |) ]
                          |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.gt (|
                                    M.read (| initial_gas_spend |),
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| env |),
                                          "revm_primitives::env::Env",
                                          "tx"
                                        |),
                                        "revm_primitives::env::TxEnv",
                                        "gas_limit"
                                      |)
                                    |)
                                  |)
                                |)) 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::result::Result::Err"
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::convert::Into",
                                            Ty.path "revm_primitives::result::InvalidTransaction",
                                            [
                                              Ty.apply
                                                (Ty.path "revm_primitives::result::EVMError")
                                                []
                                                [ Ty.associated ]
                                            ],
                                            "into",
                                            []
                                          |),
                                          [
                                            Value.StructTuple
                                              "revm_primitives::result::InvalidTransaction::CallGasCostMoreThanGasLimit"
                                              []
                                          ]
                                        |)
                                      ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (|
                    Value.StructTuple "core::result::Result::Ok" [ M.read (| initial_gas_spend |) ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_validate_initial_tx_gas :
        M.IsFunction
          "revm::handler::mainnet::validation::validate_initial_tx_gas"
          validate_initial_tx_gas.
    End validation.
  End mainnet.
End handler.
