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

Module blake2.
  Definition value_F_ROUND : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 1 |))).
  
  Definition value_INPUT_LENGTH : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 213 |))).
  
  Definition value_FUN : Value.t :=
    M.run
      ltac:(M.monadic
        (M.alloc (|
          Value.StructTuple
            "revm_precompile::PrecompileWithAddress"
            [
              M.call_closure (|
                M.get_function (| "revm_precompile::u64_to_address", [] |),
                [ Value.Integer IntegerKind.U64 9 ]
              |);
              Value.StructTuple
                "revm_primitives::precompile::Precompile::Standard"
                [
                  (* ReifyFnPointer *)
                  M.pointer_coercion (M.get_function (| "revm_precompile::blake2::run", [] |))
                ]
            ]
        |))).
  
  (*
  pub fn run(input: &Bytes, gas_limit: u64) -> PrecompileResult {
      let input = &input[..];
  
      if input.len() != INPUT_LENGTH {
          return Err(Error::Blake2WrongLength);
      }
  
      let f = match input[212] {
          1 => true,
          0 => false,
          _ => return Err(Error::Blake2WrongFinalIndicatorFlag),
      };
  
      // rounds 4 bytes
      let rounds = u32::from_be_bytes(input[..4].try_into().unwrap()) as usize;
      let gas_used = rounds as u64 * F_ROUND;
      if gas_used > gas_limit {
          return Err(Error::OutOfGas);
      }
  
      let mut h = [0u64; 8];
      let mut m = [0u64; 16];
  
      for (i, pos) in (4..68).step_by(8).enumerate() {
          h[i] = u64::from_le_bytes(input[pos..pos + 8].try_into().unwrap());
      }
      for (i, pos) in (68..196).step_by(8).enumerate() {
          m[i] = u64::from_le_bytes(input[pos..pos + 8].try_into().unwrap());
      }
      let t = [
          u64::from_le_bytes(input[196..196 + 8].try_into().unwrap()),
          u64::from_le_bytes(input[204..204 + 8].try_into().unwrap()),
      ];
  
      algo::compress(rounds, &mut h, m, t, f);
  
      let mut out = [0u8; 64];
      for (i, h) in (0..64).step_by(8).zip(h.iter()) {
          out[i..i + 8].copy_from_slice(&h.to_le_bytes());
      }
  
      Ok((gas_used, out.into()))
  }
  *)
  Definition run (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ input; gas_limit ] =>
      ltac:(M.monadic
        (let input := M.alloc (| input |) in
        let gas_limit := M.alloc (| gas_limit |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ input :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::Index",
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      [ Ty.path "core::ops::range::RangeFull" ],
                      "index",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::deref::Deref",
                          Ty.path "bytes::bytes::Bytes",
                          [],
                          "deref",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.path "alloy_primitives::bytes_::Bytes",
                              [],
                              "deref",
                              []
                            |),
                            [ M.read (| input |) ]
                          |)
                        ]
                      |);
                      Value.StructTuple "core::ops::range::RangeFull" []
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.ne (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| input |) ]
                                |),
                                M.read (|
                                  M.get_constant (| "revm_precompile::blake2::INPUT_LENGTH" |)
                                |)
                              |)
                            |)) 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::precompile::PrecompileError::Blake2WrongLength"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ f :=
                M.copy (|
                  M.match_operator (|
                    M.SubPointer.get_array_field (|
                      M.read (| input |),
                      M.alloc (| Value.Integer IntegerKind.Usize 212 |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_constant_or_break_match (|
                              M.read (| γ |),
                              Value.Integer IntegerKind.U8 1
                            |) in
                          M.alloc (| Value.Bool true |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_constant_or_break_match (|
                              M.read (| γ |),
                              Value.Integer IntegerKind.U8 0
                            |) in
                          M.alloc (| Value.Bool false |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::precompile::PrecompileError::Blake2WrongFinalIndicatorFlag"
                                        []
                                    ]
                                |)
                              |)
                            |)
                          |)))
                    ]
                  |)
                |) in
              let~ rounds :=
                M.alloc (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (| Ty.path "u32", "from_be_bytes", [] |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.apply
                                  (Ty.path "array")
                                  [ Value.Integer IntegerKind.Usize 4 ]
                                  [ Ty.path "u8" ];
                                Ty.path "core::array::TryFromSliceError"
                              ],
                            "unwrap",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::convert::TryInto",
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                [
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 4 ]
                                    [ Ty.path "u8" ]
                                ],
                                "try_into",
                                []
                              |),
                              [
                                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::RangeTo")
                                        []
                                        [ Ty.path "usize" ]
                                    ],
                                    "index",
                                    []
                                  |),
                                  [
                                    M.read (| input |);
                                    Value.StructRecord
                                      "core::ops::range::RangeTo"
                                      [ ("end_", Value.Integer IntegerKind.Usize 4) ]
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      ]
                    |))
                |) in
              let~ gas_used :=
                M.alloc (|
                  BinOp.Wrap.mul (|
                    M.rust_cast (M.read (| rounds |)),
                    M.read (| M.get_constant (| "revm_precompile::blake2::F_ROUND" |) |)
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.gt (| M.read (| gas_used |), M.read (| 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"
                                  [
                                    Value.StructTuple
                                      "revm_primitives::precompile::PrecompileError::OutOfGas"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ h :=
                M.alloc (|
                  repeat (| Value.Integer IntegerKind.U64 0, Value.Integer IntegerKind.Usize 8 |)
                |) in
              let~ m :=
                M.alloc (|
                  repeat (| Value.Integer IntegerKind.U64 0, Value.Integer IntegerKind.Usize 16 |)
                |) 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 "core::iter::adapters::enumerate::Enumerate")
                            []
                            [
                              Ty.apply
                                (Ty.path "core::iter::adapters::step_by::StepBy")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ]
                            ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply
                                (Ty.path "core::iter::adapters::step_by::StepBy")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ],
                              [],
                              "enumerate",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ],
                                  [],
                                  "step_by",
                                  []
                                |),
                                [
                                  Value.StructRecord
                                    "core::ops::range::Range"
                                    [
                                      ("start", Value.Integer IntegerKind.Usize 4);
                                      ("end_", Value.Integer IntegerKind.Usize 68)
                                    ];
                                  Value.Integer IntegerKind.Usize 8
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::iter::adapters::enumerate::Enumerate")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::iter::adapters::step_by::StepBy")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "core::ops::range::Range")
                                                  []
                                                  [ Ty.path "usize" ]
                                              ]
                                          ],
                                        [],
                                        "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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                        let i := M.copy (| γ1_0 |) in
                                        let pos := M.copy (| γ1_1 |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_array_field (| h, i |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "u64",
                                                "from_le_bytes",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "array")
                                                          [ Value.Integer IntegerKind.Usize 8 ]
                                                          [ Ty.path "u8" ];
                                                        Ty.path "core::array::TryFromSliceError"
                                                      ],
                                                    "unwrap",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::convert::TryInto",
                                                        Ty.apply
                                                          (Ty.path "&")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "slice")
                                                              []
                                                              [ Ty.path "u8" ]
                                                          ],
                                                        [
                                                          Ty.apply
                                                            (Ty.path "array")
                                                            [ Value.Integer IntegerKind.Usize 8 ]
                                                            [ Ty.path "u8" ]
                                                        ],
                                                        "try_into",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::index::Index",
                                                            Ty.apply
                                                              (Ty.path "slice")
                                                              []
                                                              [ Ty.path "u8" ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path "core::ops::range::Range")
                                                                []
                                                                [ Ty.path "usize" ]
                                                            ],
                                                            "index",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| input |);
                                                            Value.StructRecord
                                                              "core::ops::range::Range"
                                                              [
                                                                ("start", M.read (| pos |));
                                                                ("end_",
                                                                  BinOp.Wrap.add (|
                                                                    M.read (| pos |),
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      8
                                                                  |))
                                                              ]
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) 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 "core::iter::adapters::enumerate::Enumerate")
                            []
                            [
                              Ty.apply
                                (Ty.path "core::iter::adapters::step_by::StepBy")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ]
                            ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply
                                (Ty.path "core::iter::adapters::step_by::StepBy")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ],
                              [],
                              "enumerate",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ],
                                  [],
                                  "step_by",
                                  []
                                |),
                                [
                                  Value.StructRecord
                                    "core::ops::range::Range"
                                    [
                                      ("start", Value.Integer IntegerKind.Usize 68);
                                      ("end_", Value.Integer IntegerKind.Usize 196)
                                    ];
                                  Value.Integer IntegerKind.Usize 8
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::iter::adapters::enumerate::Enumerate")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::iter::adapters::step_by::StepBy")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "core::ops::range::Range")
                                                  []
                                                  [ Ty.path "usize" ]
                                              ]
                                          ],
                                        [],
                                        "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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                        let i := M.copy (| γ1_0 |) in
                                        let pos := M.copy (| γ1_1 |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_array_field (| m, i |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "u64",
                                                "from_le_bytes",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "array")
                                                          [ Value.Integer IntegerKind.Usize 8 ]
                                                          [ Ty.path "u8" ];
                                                        Ty.path "core::array::TryFromSliceError"
                                                      ],
                                                    "unwrap",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::convert::TryInto",
                                                        Ty.apply
                                                          (Ty.path "&")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "slice")
                                                              []
                                                              [ Ty.path "u8" ]
                                                          ],
                                                        [
                                                          Ty.apply
                                                            (Ty.path "array")
                                                            [ Value.Integer IntegerKind.Usize 8 ]
                                                            [ Ty.path "u8" ]
                                                        ],
                                                        "try_into",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::index::Index",
                                                            Ty.apply
                                                              (Ty.path "slice")
                                                              []
                                                              [ Ty.path "u8" ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path "core::ops::range::Range")
                                                                []
                                                                [ Ty.path "usize" ]
                                                            ],
                                                            "index",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| input |);
                                                            Value.StructRecord
                                                              "core::ops::range::Range"
                                                              [
                                                                ("start", M.read (| pos |));
                                                                ("end_",
                                                                  BinOp.Wrap.add (|
                                                                    M.read (| pos |),
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      8
                                                                  |))
                                                              ]
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              let~ t :=
                M.alloc (|
                  Value.Array
                    [
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "u64", "from_le_bytes", [] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 8 ]
                                    [ Ty.path "u8" ];
                                  Ty.path "core::array::TryFromSliceError"
                                ],
                              "unwrap",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::convert::TryInto",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                  [
                                    Ty.apply
                                      (Ty.path "array")
                                      [ Value.Integer IntegerKind.Usize 8 ]
                                      [ Ty.path "u8" ]
                                  ],
                                  "try_into",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::index::Index",
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::ops::range::Range")
                                          []
                                          [ Ty.path "usize" ]
                                      ],
                                      "index",
                                      []
                                    |),
                                    [
                                      M.read (| input |);
                                      Value.StructRecord
                                        "core::ops::range::Range"
                                        [
                                          ("start", Value.Integer IntegerKind.Usize 196);
                                          ("end_",
                                            BinOp.Wrap.add (|
                                              Value.Integer IntegerKind.Usize 196,
                                              Value.Integer IntegerKind.Usize 8
                                            |))
                                        ]
                                    ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "u64", "from_le_bytes", [] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 8 ]
                                    [ Ty.path "u8" ];
                                  Ty.path "core::array::TryFromSliceError"
                                ],
                              "unwrap",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::convert::TryInto",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                  [
                                    Ty.apply
                                      (Ty.path "array")
                                      [ Value.Integer IntegerKind.Usize 8 ]
                                      [ Ty.path "u8" ]
                                  ],
                                  "try_into",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::index::Index",
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::ops::range::Range")
                                          []
                                          [ Ty.path "usize" ]
                                      ],
                                      "index",
                                      []
                                    |),
                                    [
                                      M.read (| input |);
                                      Value.StructRecord
                                        "core::ops::range::Range"
                                        [
                                          ("start", Value.Integer IntegerKind.Usize 204);
                                          ("end_",
                                            BinOp.Wrap.add (|
                                              Value.Integer IntegerKind.Usize 204,
                                              Value.Integer IntegerKind.Usize 8
                                            |))
                                        ]
                                    ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "revm_precompile::blake2::algo::compress", [] |),
                    [ M.read (| rounds |); h; M.read (| m |); M.read (| t |); M.read (| f |) ]
                  |)
                |) in
              let~ out :=
                M.alloc (|
                  repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 64 |)
                |) 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 "core::iter::adapters::zip::Zip")
                            []
                            [
                              Ty.apply
                                (Ty.path "core::iter::adapters::step_by::StepBy")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ];
                              Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u64" ]
                            ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply
                                (Ty.path "core::iter::adapters::step_by::StepBy")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ],
                              [],
                              "zip",
                              [ Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u64" ] ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ],
                                  [],
                                  "step_by",
                                  []
                                |),
                                [
                                  Value.StructRecord
                                    "core::ops::range::Range"
                                    [
                                      ("start", Value.Integer IntegerKind.Usize 0);
                                      ("end_", Value.Integer IntegerKind.Usize 64)
                                    ];
                                  Value.Integer IntegerKind.Usize 8
                                ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u64" ],
                                  "iter",
                                  []
                                |),
                                [ h ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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::iter::adapters::zip::Zip")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::iter::adapters::step_by::StepBy")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "core::ops::range::Range")
                                                  []
                                                  [ Ty.path "usize" ]
                                              ];
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              []
                                              [ Ty.path "u64" ]
                                          ],
                                        [],
                                        "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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                        let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                        let i := M.copy (| γ1_0 |) in
                                        let h := M.copy (| γ1_1 |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                                "copy_from_slice",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::index::IndexMut",
                                                    Ty.apply
                                                      (Ty.path "array")
                                                      [ Value.Integer IntegerKind.Usize 64 ]
                                                      [ Ty.path "u8" ],
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::ops::range::Range")
                                                        []
                                                        [ Ty.path "usize" ]
                                                    ],
                                                    "index_mut",
                                                    []
                                                  |),
                                                  [
                                                    out;
                                                    Value.StructRecord
                                                      "core::ops::range::Range"
                                                      [
                                                        ("start", M.read (| i |));
                                                        ("end_",
                                                          BinOp.Wrap.add (|
                                                            M.read (| i |),
                                                            Value.Integer IntegerKind.Usize 8
                                                          |))
                                                      ]
                                                  ]
                                                |);
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "u64",
                                                      "to_le_bytes",
                                                      []
                                                    |),
                                                    [ M.read (| M.read (| h |) |) ]
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |)) in
              M.alloc (|
                Value.StructTuple
                  "core::result::Result::Ok"
                  [
                    Value.Tuple
                      [
                        M.read (| gas_used |);
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::Into",
                            Ty.apply
                              (Ty.path "array")
                              [ Value.Integer IntegerKind.Usize 64 ]
                              [ Ty.path "u8" ],
                            [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                            "into",
                            []
                          |),
                          [ M.read (| out |) ]
                        |)
                      ]
                  ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_run : M.IsFunction "revm_precompile::blake2::run" run.
  
  Module algo.
    Definition value_SIGMA : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            Value.Array
              [
                Value.Array
                  [
                    Value.Integer IntegerKind.Usize 0;
                    Value.Integer IntegerKind.Usize 1;
                    Value.Integer IntegerKind.Usize 2;
                    Value.Integer IntegerKind.Usize 3;
                    Value.Integer IntegerKind.Usize 4;
                    Value.Integer IntegerKind.Usize 5;
                    Value.Integer IntegerKind.Usize 6;
                    Value.Integer IntegerKind.Usize 7;
                    Value.Integer IntegerKind.Usize 8;
                    Value.Integer IntegerKind.Usize 9;
                    Value.Integer IntegerKind.Usize 10;
                    Value.Integer IntegerKind.Usize 11;
                    Value.Integer IntegerKind.Usize 12;
                    Value.Integer IntegerKind.Usize 13;
                    Value.Integer IntegerKind.Usize 14;
                    Value.Integer IntegerKind.Usize 15
                  ];
                Value.Array
                  [
                    Value.Integer IntegerKind.Usize 14;
                    Value.Integer IntegerKind.Usize 10;
                    Value.Integer IntegerKind.Usize 4;
                    Value.Integer IntegerKind.Usize 8;
                    Value.Integer IntegerKind.Usize 9;
                    Value.Integer IntegerKind.Usize 15;
                    Value.Integer IntegerKind.Usize 13;
                    Value.Integer IntegerKind.Usize 6;
                    Value.Integer IntegerKind.Usize 1;
                    Value.Integer IntegerKind.Usize 12;
                    Value.Integer IntegerKind.Usize 0;
                    Value.Integer IntegerKind.Usize 2;
                    Value.Integer IntegerKind.Usize 11;
                    Value.Integer IntegerKind.Usize 7;
                    Value.Integer IntegerKind.Usize 5;
                    Value.Integer IntegerKind.Usize 3
                  ];
                Value.Array
                  [
                    Value.Integer IntegerKind.Usize 11;
                    Value.Integer IntegerKind.Usize 8;
                    Value.Integer IntegerKind.Usize 12;
                    Value.Integer IntegerKind.Usize 0;
                    Value.Integer IntegerKind.Usize 5;
                    Value.Integer IntegerKind.Usize 2;
                    Value.Integer IntegerKind.Usize 15;
                    Value.Integer IntegerKind.Usize 13;
                    Value.Integer IntegerKind.Usize 10;
                    Value.Integer IntegerKind.Usize 14;
                    Value.Integer IntegerKind.Usize 3;
                    Value.Integer IntegerKind.Usize 6;
                    Value.Integer IntegerKind.Usize 7;
                    Value.Integer IntegerKind.Usize 1;
                    Value.Integer IntegerKind.Usize 9;
                    Value.Integer IntegerKind.Usize 4
                  ];
                Value.Array
                  [
                    Value.Integer IntegerKind.Usize 7;
                    Value.Integer IntegerKind.Usize 9;
                    Value.Integer IntegerKind.Usize 3;
                    Value.Integer IntegerKind.Usize 1;
                    Value.Integer IntegerKind.Usize 13;
                    Value.Integer IntegerKind.Usize 12;
                    Value.Integer IntegerKind.Usize 11;
                    Value.Integer IntegerKind.Usize 14;
                    Value.Integer IntegerKind.Usize 2;
                    Value.Integer IntegerKind.Usize 6;
                    Value.Integer IntegerKind.Usize 5;
                    Value.Integer IntegerKind.Usize 10;
                    Value.Integer IntegerKind.Usize 4;
                    Value.Integer IntegerKind.Usize 0;
                    Value.Integer IntegerKind.Usize 15;
                    Value.Integer IntegerKind.Usize 8
                  ];
                Value.Array
                  [
                    Value.Integer IntegerKind.Usize 9;
                    Value.Integer IntegerKind.Usize 0;
                    Value.Integer IntegerKind.Usize 5;
                    Value.Integer IntegerKind.Usize 7;
                    Value.Integer IntegerKind.Usize 2;
                    Value.Integer IntegerKind.Usize 4;
                    Value.Integer IntegerKind.Usize 10;
                    Value.Integer IntegerKind.Usize 15;
                    Value.Integer IntegerKind.Usize 14;
                    Value.Integer IntegerKind.Usize 1;
                    Value.Integer IntegerKind.Usize 11;
                    Value.Integer IntegerKind.Usize 12;
                    Value.Integer IntegerKind.Usize 6;
                    Value.Integer IntegerKind.Usize 8;
                    Value.Integer IntegerKind.Usize 3;
                    Value.Integer IntegerKind.Usize 13
                  ];
                Value.Array
                  [
                    Value.Integer IntegerKind.Usize 2;
                    Value.Integer IntegerKind.Usize 12;
                    Value.Integer IntegerKind.Usize 6;
                    Value.Integer IntegerKind.Usize 10;
                    Value.Integer IntegerKind.Usize 0;
                    Value.Integer IntegerKind.Usize 11;
                    Value.Integer IntegerKind.Usize 8;
                    Value.Integer IntegerKind.Usize 3;
                    Value.Integer IntegerKind.Usize 4;
                    Value.Integer IntegerKind.Usize 13;
                    Value.Integer IntegerKind.Usize 7;
                    Value.Integer IntegerKind.Usize 5;
                    Value.Integer IntegerKind.Usize 15;
                    Value.Integer IntegerKind.Usize 14;
                    Value.Integer IntegerKind.Usize 1;
                    Value.Integer IntegerKind.Usize 9
                  ];
                Value.Array
                  [
                    Value.Integer IntegerKind.Usize 12;
                    Value.Integer IntegerKind.Usize 5;
                    Value.Integer IntegerKind.Usize 1;
                    Value.Integer IntegerKind.Usize 15;
                    Value.Integer IntegerKind.Usize 14;
                    Value.Integer IntegerKind.Usize 13;
                    Value.Integer IntegerKind.Usize 4;
                    Value.Integer IntegerKind.Usize 10;
                    Value.Integer IntegerKind.Usize 0;
                    Value.Integer IntegerKind.Usize 7;
                    Value.Integer IntegerKind.Usize 6;
                    Value.Integer IntegerKind.Usize 3;
                    Value.Integer IntegerKind.Usize 9;
                    Value.Integer IntegerKind.Usize 2;
                    Value.Integer IntegerKind.Usize 8;
                    Value.Integer IntegerKind.Usize 11
                  ];
                Value.Array
                  [
                    Value.Integer IntegerKind.Usize 13;
                    Value.Integer IntegerKind.Usize 11;
                    Value.Integer IntegerKind.Usize 7;
                    Value.Integer IntegerKind.Usize 14;
                    Value.Integer IntegerKind.Usize 12;
                    Value.Integer IntegerKind.Usize 1;
                    Value.Integer IntegerKind.Usize 3;
                    Value.Integer IntegerKind.Usize 9;
                    Value.Integer IntegerKind.Usize 5;
                    Value.Integer IntegerKind.Usize 0;
                    Value.Integer IntegerKind.Usize 15;
                    Value.Integer IntegerKind.Usize 4;
                    Value.Integer IntegerKind.Usize 8;
                    Value.Integer IntegerKind.Usize 6;
                    Value.Integer IntegerKind.Usize 2;
                    Value.Integer IntegerKind.Usize 10
                  ];
                Value.Array
                  [
                    Value.Integer IntegerKind.Usize 6;
                    Value.Integer IntegerKind.Usize 15;
                    Value.Integer IntegerKind.Usize 14;
                    Value.Integer IntegerKind.Usize 9;
                    Value.Integer IntegerKind.Usize 11;
                    Value.Integer IntegerKind.Usize 3;
                    Value.Integer IntegerKind.Usize 0;
                    Value.Integer IntegerKind.Usize 8;
                    Value.Integer IntegerKind.Usize 12;
                    Value.Integer IntegerKind.Usize 2;
                    Value.Integer IntegerKind.Usize 13;
                    Value.Integer IntegerKind.Usize 7;
                    Value.Integer IntegerKind.Usize 1;
                    Value.Integer IntegerKind.Usize 4;
                    Value.Integer IntegerKind.Usize 10;
                    Value.Integer IntegerKind.Usize 5
                  ];
                Value.Array
                  [
                    Value.Integer IntegerKind.Usize 10;
                    Value.Integer IntegerKind.Usize 2;
                    Value.Integer IntegerKind.Usize 8;
                    Value.Integer IntegerKind.Usize 4;
                    Value.Integer IntegerKind.Usize 7;
                    Value.Integer IntegerKind.Usize 6;
                    Value.Integer IntegerKind.Usize 1;
                    Value.Integer IntegerKind.Usize 5;
                    Value.Integer IntegerKind.Usize 15;
                    Value.Integer IntegerKind.Usize 11;
                    Value.Integer IntegerKind.Usize 9;
                    Value.Integer IntegerKind.Usize 14;
                    Value.Integer IntegerKind.Usize 3;
                    Value.Integer IntegerKind.Usize 12;
                    Value.Integer IntegerKind.Usize 13;
                    Value.Integer IntegerKind.Usize 0
                  ]
              ]
          |))).
    
    Definition value_IV : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            Value.Array
              [
                Value.Integer IntegerKind.U64 7640891576956012808;
                Value.Integer IntegerKind.U64 13503953896175478587;
                Value.Integer IntegerKind.U64 4354685564936845355;
                Value.Integer IntegerKind.U64 11912009170470909681;
                Value.Integer IntegerKind.U64 5840696475078001361;
                Value.Integer IntegerKind.U64 11170449401992604703;
                Value.Integer IntegerKind.U64 2270897969802886507;
                Value.Integer IntegerKind.U64 6620516959819538809
              ]
          |))).
    
    (*
        pub fn g(v: &mut [u64], a: usize, b: usize, c: usize, d: usize, x: u64, y: u64) {
            v[a] = v[a].wrapping_add(v[b]).wrapping_add(x);
            v[d] = (v[d] ^ v[a]).rotate_right(32);
            v[c] = v[c].wrapping_add(v[d]);
            v[b] = (v[b] ^ v[c]).rotate_right(24);
            v[a] = v[a].wrapping_add(v[b]).wrapping_add(y);
            v[d] = (v[d] ^ v[a]).rotate_right(16);
            v[c] = v[c].wrapping_add(v[d]);
            v[b] = (v[b] ^ v[c]).rotate_right(63);
        }
    *)
    Definition g (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ v; a; b; c; d; x; y ] =>
        ltac:(M.monadic
          (let v := M.alloc (| v |) in
          let a := M.alloc (| a |) in
          let b := M.alloc (| b |) in
          let c := M.alloc (| c |) in
          let d := M.alloc (| d |) in
          let x := M.alloc (| x |) in
          let y := M.alloc (| y |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.SubPointer.get_array_field (| M.read (| v |), a |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "wrapping_add", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "u64", "wrapping_add", [] |),
                      [
                        M.read (| M.SubPointer.get_array_field (| M.read (| v |), a |) |);
                        M.read (| M.SubPointer.get_array_field (| M.read (| v |), b |) |)
                      ]
                    |);
                    M.read (| x |)
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_array_field (| M.read (| v |), d |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "rotate_right", [] |),
                  [
                    BinOp.bit_xor
                      (M.read (| M.SubPointer.get_array_field (| M.read (| v |), d |) |))
                      (M.read (| M.SubPointer.get_array_field (| M.read (| v |), a |) |));
                    Value.Integer IntegerKind.U32 32
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_array_field (| M.read (| v |), c |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "wrapping_add", [] |),
                  [
                    M.read (| M.SubPointer.get_array_field (| M.read (| v |), c |) |);
                    M.read (| M.SubPointer.get_array_field (| M.read (| v |), d |) |)
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_array_field (| M.read (| v |), b |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "rotate_right", [] |),
                  [
                    BinOp.bit_xor
                      (M.read (| M.SubPointer.get_array_field (| M.read (| v |), b |) |))
                      (M.read (| M.SubPointer.get_array_field (| M.read (| v |), c |) |));
                    Value.Integer IntegerKind.U32 24
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_array_field (| M.read (| v |), a |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "wrapping_add", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "u64", "wrapping_add", [] |),
                      [
                        M.read (| M.SubPointer.get_array_field (| M.read (| v |), a |) |);
                        M.read (| M.SubPointer.get_array_field (| M.read (| v |), b |) |)
                      ]
                    |);
                    M.read (| y |)
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_array_field (| M.read (| v |), d |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "rotate_right", [] |),
                  [
                    BinOp.bit_xor
                      (M.read (| M.SubPointer.get_array_field (| M.read (| v |), d |) |))
                      (M.read (| M.SubPointer.get_array_field (| M.read (| v |), a |) |));
                    Value.Integer IntegerKind.U32 16
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_array_field (| M.read (| v |), c |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "wrapping_add", [] |),
                  [
                    M.read (| M.SubPointer.get_array_field (| M.read (| v |), c |) |);
                    M.read (| M.SubPointer.get_array_field (| M.read (| v |), d |) |)
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_array_field (| M.read (| v |), b |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "u64", "rotate_right", [] |),
                  [
                    BinOp.bit_xor
                      (M.read (| M.SubPointer.get_array_field (| M.read (| v |), b |) |))
                      (M.read (| M.SubPointer.get_array_field (| M.read (| v |), c |) |));
                    Value.Integer IntegerKind.U32 63
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_g : M.IsFunction "revm_precompile::blake2::algo::g" g.
    
    (*
        pub fn compress(rounds: usize, h: &mut [u64; 8], m: [u64; 16], t: [u64; 2], f: bool) {
            let mut v = [0u64; 16];
            v[..h.len()].copy_from_slice(h); // First half from state.
            v[h.len()..].copy_from_slice(&IV); // Second half from IV.
    
            v[12] ^= t[0];
            v[13] ^= t[1];
    
            if f {
                v[14] = !v[14] // Invert all bits if the last-block-flag is set.
            }
            for i in 0..rounds {
                // Message word selection permutation for this round.
                let s = &SIGMA[i % 10];
                g(&mut v, 0, 4, 8, 12, m[s[0]], m[s[1]]);
                g(&mut v, 1, 5, 9, 13, m[s[2]], m[s[3]]);
                g(&mut v, 2, 6, 10, 14, m[s[4]], m[s[5]]);
                g(&mut v, 3, 7, 11, 15, m[s[6]], m[s[7]]);
    
                g(&mut v, 0, 5, 10, 15, m[s[8]], m[s[9]]);
                g(&mut v, 1, 6, 11, 12, m[s[10]], m[s[11]]);
                g(&mut v, 2, 7, 8, 13, m[s[12]], m[s[13]]);
                g(&mut v, 3, 4, 9, 14, m[s[14]], m[s[15]]);
            }
    
            for i in 0..8 {
                h[i] ^= v[i] ^ v[i + 8];
            }
        }
    *)
    Definition compress (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ rounds; h; m; t; f ] =>
        ltac:(M.monadic
          (let rounds := M.alloc (| rounds |) in
          let h := M.alloc (| h |) in
          let m := M.alloc (| m |) in
          let t := M.alloc (| t |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ v :=
              M.alloc (|
                repeat (| Value.Integer IntegerKind.U64 0, Value.Integer IntegerKind.Usize 16 |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u64" ],
                    "copy_from_slice",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::index::IndexMut",
                        Ty.apply
                          (Ty.path "array")
                          [ Value.Integer IntegerKind.Usize 16 ]
                          [ Ty.path "u64" ],
                        [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                        "index_mut",
                        []
                      |),
                      [
                        v;
                        Value.StructRecord
                          "core::ops::range::RangeTo"
                          [
                            ("end_",
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u64" ],
                                  "len",
                                  []
                                |),
                                [ M.read (| h |) ]
                              |))
                          ]
                      ]
                    |);
                    M.read (| h |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u64" ],
                    "copy_from_slice",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::index::IndexMut",
                        Ty.apply
                          (Ty.path "array")
                          [ Value.Integer IntegerKind.Usize 16 ]
                          [ Ty.path "u64" ],
                        [ Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ] ],
                        "index_mut",
                        []
                      |),
                      [
                        v;
                        Value.StructRecord
                          "core::ops::range::RangeFrom"
                          [
                            ("start",
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u64" ],
                                  "len",
                                  []
                                |),
                                [ M.read (| h |) ]
                              |))
                          ]
                      ]
                    |);
                    M.get_constant (| "revm_precompile::blake2::algo::IV" |)
                  ]
                |)
              |) in
            let~ _ :=
              let β :=
                M.SubPointer.get_array_field (|
                  v,
                  M.alloc (| Value.Integer IntegerKind.Usize 12 |)
                |) in
              M.write (|
                β,
                BinOp.bit_xor
                  (M.read (| β |))
                  (M.read (|
                    M.SubPointer.get_array_field (|
                      t,
                      M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                    |)
                  |))
              |) in
            let~ _ :=
              let β :=
                M.SubPointer.get_array_field (|
                  v,
                  M.alloc (| Value.Integer IntegerKind.Usize 13 |)
                |) in
              M.write (|
                β,
                BinOp.bit_xor
                  (M.read (| β |))
                  (M.read (|
                    M.SubPointer.get_array_field (|
                      t,
                      M.alloc (| Value.Integer IntegerKind.Usize 1 |)
                    |)
                  |))
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use f in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.write (|
                        M.SubPointer.get_array_field (|
                          v,
                          M.alloc (| Value.Integer IntegerKind.Usize 14 |)
                        |),
                        UnOp.not (|
                          M.read (|
                            M.SubPointer.get_array_field (|
                              v,
                              M.alloc (| Value.Integer IntegerKind.Usize 14 |)
                            |)
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) 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 "core::ops::range::Range") [] [ Ty.path "usize" ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        Value.StructRecord
                          "core::ops::range::Range"
                          [
                            ("start", Value.Integer IntegerKind.Usize 0);
                            ("end_", M.read (| rounds |))
                          ]
                      ]
                    |)
                  |),
                  [
                    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::ops::range::Range")
                                        []
                                        [ Ty.path "usize" ],
                                      [],
                                      "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 i := M.copy (| γ0_0 |) in
                                      let~ s :=
                                        M.alloc (|
                                          M.SubPointer.get_array_field (|
                                            M.get_constant (|
                                              "revm_precompile::blake2::algo::SIGMA"
                                            |),
                                            M.alloc (|
                                              BinOp.Wrap.rem (|
                                                M.read (| i |),
                                                Value.Integer IntegerKind.Usize 10
                                              |)
                                            |)
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "revm_precompile::blake2::algo::g",
                                              []
                                            |),
                                            [
                                              v;
                                              Value.Integer IntegerKind.Usize 0;
                                              Value.Integer IntegerKind.Usize 4;
                                              Value.Integer IntegerKind.Usize 8;
                                              Value.Integer IntegerKind.Usize 12;
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                                                  |)
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 1 |)
                                                  |)
                                                |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "revm_precompile::blake2::algo::g",
                                              []
                                            |),
                                            [
                                              v;
                                              Value.Integer IntegerKind.Usize 1;
                                              Value.Integer IntegerKind.Usize 5;
                                              Value.Integer IntegerKind.Usize 9;
                                              Value.Integer IntegerKind.Usize 13;
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 2 |)
                                                  |)
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 3 |)
                                                  |)
                                                |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "revm_precompile::blake2::algo::g",
                                              []
                                            |),
                                            [
                                              v;
                                              Value.Integer IntegerKind.Usize 2;
                                              Value.Integer IntegerKind.Usize 6;
                                              Value.Integer IntegerKind.Usize 10;
                                              Value.Integer IntegerKind.Usize 14;
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 4 |)
                                                  |)
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 5 |)
                                                  |)
                                                |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "revm_precompile::blake2::algo::g",
                                              []
                                            |),
                                            [
                                              v;
                                              Value.Integer IntegerKind.Usize 3;
                                              Value.Integer IntegerKind.Usize 7;
                                              Value.Integer IntegerKind.Usize 11;
                                              Value.Integer IntegerKind.Usize 15;
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 6 |)
                                                  |)
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 7 |)
                                                  |)
                                                |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "revm_precompile::blake2::algo::g",
                                              []
                                            |),
                                            [
                                              v;
                                              Value.Integer IntegerKind.Usize 0;
                                              Value.Integer IntegerKind.Usize 5;
                                              Value.Integer IntegerKind.Usize 10;
                                              Value.Integer IntegerKind.Usize 15;
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 8 |)
                                                  |)
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 9 |)
                                                  |)
                                                |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "revm_precompile::blake2::algo::g",
                                              []
                                            |),
                                            [
                                              v;
                                              Value.Integer IntegerKind.Usize 1;
                                              Value.Integer IntegerKind.Usize 6;
                                              Value.Integer IntegerKind.Usize 11;
                                              Value.Integer IntegerKind.Usize 12;
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 10 |)
                                                  |)
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 11 |)
                                                  |)
                                                |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "revm_precompile::blake2::algo::g",
                                              []
                                            |),
                                            [
                                              v;
                                              Value.Integer IntegerKind.Usize 2;
                                              Value.Integer IntegerKind.Usize 7;
                                              Value.Integer IntegerKind.Usize 8;
                                              Value.Integer IntegerKind.Usize 13;
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 12 |)
                                                  |)
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 13 |)
                                                  |)
                                                |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "revm_precompile::blake2::algo::g",
                                              []
                                            |),
                                            [
                                              v;
                                              Value.Integer IntegerKind.Usize 3;
                                              Value.Integer IntegerKind.Usize 4;
                                              Value.Integer IntegerKind.Usize 9;
                                              Value.Integer IntegerKind.Usize 14;
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 14 |)
                                                  |)
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_array_field (|
                                                  m,
                                                  M.SubPointer.get_array_field (|
                                                    M.read (| s |),
                                                    M.alloc (| Value.Integer IntegerKind.Usize 15 |)
                                                  |)
                                                |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            M.use
              (M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::IntoIterator",
                      Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                      [],
                      "into_iter",
                      []
                    |),
                    [
                      Value.StructRecord
                        "core::ops::range::Range"
                        [
                          ("start", Value.Integer IntegerKind.Usize 0);
                          ("end_", Value.Integer IntegerKind.Usize 8)
                        ]
                    ]
                  |)
                |),
                [
                  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::ops::range::Range")
                                      []
                                      [ Ty.path "usize" ],
                                    [],
                                    "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 i := M.copy (| γ0_0 |) in
                                    let~ _ :=
                                      let β :=
                                        M.SubPointer.get_array_field (| M.read (| h |), i |) in
                                      M.write (|
                                        β,
                                        BinOp.bit_xor
                                          (M.read (| β |))
                                          (BinOp.bit_xor
                                            (M.read (| M.SubPointer.get_array_field (| v, i |) |))
                                            (M.read (|
                                              M.SubPointer.get_array_field (|
                                                v,
                                                M.alloc (|
                                                  BinOp.Wrap.add (|
                                                    M.read (| i |),
                                                    Value.Integer IntegerKind.Usize 8
                                                  |)
                                                |)
                                              |)
                                            |)))
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                      |)))
                ]
              |))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_compress : M.IsFunction "revm_precompile::blake2::algo::compress" compress.
  End algo.
End blake2.
