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

Module bytecode.
  Module eof.
    Module decode_helpers.
      (*
      pub(crate) fn consume_u8(input: &[u8]) -> Result<(&[u8], u8), EofDecodeError> {
          if input.is_empty() {
              return Err(EofDecodeError::MissingInput);
          }
          Ok((&input[1..], input[0]))
      }
      *)
      Definition consume_u8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ input ] =>
          ltac:(M.monadic
            (let input := M.alloc (| input |) 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 (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                      "is_empty",
                                      []
                                    |),
                                    [ M.read (| input |) ]
                                  |)
                                |)) 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"
                                      [
                                        Value.StructTuple
                                          "revm_primitives::bytecode::eof::EofDecodeError::MissingInput"
                                          []
                                      ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        Value.Tuple
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::index::Index",
                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::RangeFrom")
                                    []
                                    [ Ty.path "usize" ]
                                ],
                                "index",
                                []
                              |),
                              [
                                M.read (| input |);
                                Value.StructRecord
                                  "core::ops::range::RangeFrom"
                                  [ ("start", Value.Integer IntegerKind.Usize 1) ]
                              ]
                            |);
                            M.read (|
                              M.SubPointer.get_array_field (|
                                M.read (| input |),
                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                              |)
                            |)
                          ]
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_consume_u8 :
        M.IsFunction "revm_primitives::bytecode::eof::decode_helpers::consume_u8" consume_u8.
      
      (*
      pub(crate) fn consume_u16(input: &[u8]) -> Result<(&[u8], u16), EofDecodeError> {
          if input.len() < 2 {
              return Err(EofDecodeError::MissingInput);
          }
          let (int_bytes, rest) = input.split_at(2);
          Ok((rest, u16::from_be_bytes([int_bytes[0], int_bytes[1]])))
      }
      *)
      Definition consume_u16 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ input ] =>
          ltac:(M.monadic
            (let input := M.alloc (| input |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.lt (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| input |) ]
                                    |),
                                    Value.Integer IntegerKind.Usize 2
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [
                                        Value.StructTuple
                                          "revm_primitives::bytecode::eof::EofDecodeError::MissingInput"
                                          []
                                      ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "split_at",
                          []
                        |),
                        [ M.read (| input |); Value.Integer IntegerKind.Usize 2 ]
                      |)
                    |),
                    [
                      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 int_bytes := M.copy (| γ0_0 |) in
                          let rest := M.copy (| γ0_1 |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::result::Result::Ok"
                              [
                                Value.Tuple
                                  [
                                    M.read (| rest |);
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "u16",
                                        "from_be_bytes",
                                        []
                                      |),
                                      [
                                        Value.Array
                                          [
                                            M.read (|
                                              M.SubPointer.get_array_field (|
                                                M.read (| int_bytes |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                              |)
                                            |);
                                            M.read (|
                                              M.SubPointer.get_array_field (|
                                                M.read (| int_bytes |),
                                                M.alloc (| Value.Integer IntegerKind.Usize 1 |)
                                              |)
                                            |)
                                          ]
                                      ]
                                    |)
                                  ]
                              ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_consume_u16 :
        M.IsFunction "revm_primitives::bytecode::eof::decode_helpers::consume_u16" consume_u16.
    End decode_helpers.
  End eof.
End bytecode.
