fips205-slhdsa-verified/verification/gen/SlhVerify/Funs.lean

-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [fips205]: function definitions
import Aeneas
import SlhVerify.Types
import SlhVerify.FunsExternal
open Aeneas Aeneas.Std Result ControlFlow Error
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false

/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
set_option maxHeartbeats 1000000

/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
set_option maxRecDepth 2048

/- You can remove the following line by using the CLI option `-all-computable`: -/
noncomputable section

namespace fips205

/-- Trait implementation: [core::iter::range::{impl core::iter::range::Step for u32}]
    Source: '/rustc/library/core/src/iter/range.rs', lines 266:12-266:43
    Name pattern: [core::iter::range::Step<u32>] -/
@[reducible, rust_trait_impl "core::iter::range::Step<u32>"]
def U32.Insts.CoreIterRangeStep : core.iter.range.Step Std.U32 := {
  cloneInst := core.clone.CloneU32
  partialOrdInst := core.cmp.PartialOrdU32
  steps_between := U32.Insts.CoreIterRangeStep.steps_between
  forward_checked := U32.Insts.CoreIterRangeStep.forward_checked
  backward_checked := U32.Insts.CoreIterRangeStep.backward_checked
}

/-- Trait implementation: [zeroize::{impl zeroize::Zeroize for Z}]
    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 270:0-272:23
    Name pattern: [zeroize::Zeroize<@Z>] -/
@[reducible, rust_trait_impl "zeroize::Zeroize<@Z>"]
def zeroize.Zeroize.Blanket {Z : Type} (DefaultIsZeroesInst :
  zeroize.DefaultIsZeroes Z) : zeroize.Zeroize Z := {
  zeroize := zeroize.Zeroize.Blanket.zeroize DefaultIsZeroesInst
}

/-- Trait implementation: [zeroize::{impl zeroize::DefaultIsZeroes for u8}]
    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 282:10-282:40
    Name pattern: [zeroize::DefaultIsZeroes<u8>] -/
@[reducible, rust_trait_impl "zeroize::DefaultIsZeroes<u8>"]
def U8.Insts.ZeroizeDefaultIsZeroes : zeroize.DefaultIsZeroes Std.U8 := {
  coremarkerCopyInst := core.marker.CopyU8
  coredefaultDefaultInst := core.default.DefaultU8
}

/-- Trait implementation: [zeroize::{impl zeroize::Zeroize for [Z; N]}]
    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 342:0-344:15
    Name pattern: [zeroize::Zeroize<[@Z; @N]>] -/
@[reducible, rust_trait_impl "zeroize::Zeroize<[@Z; @N]>"]
def Array.Insts.ZeroizeZeroize {Z : Type} (N : Std.Usize) (ZeroizeInst :
  zeroize.Zeroize Z) : zeroize.Zeroize (Array Z N) := {
  zeroize := Array.Insts.ZeroizeZeroize.zeroize ZeroizeInst
}

/-- [fips205::helpers::to_int]: loop body 0:
    Source: 'src/helpers.rs', lines 20:4-26:5 -/
@[rust_loop_body]
def helpers.to_int_loop.body
  (x : Slice Std.U8) (iter : core.ops.range.Range Std.Usize) (total : Std.U64)
  :
  Result (ControlFlow ((core.ops.range.Range Std.Usize) × Std.U64) Std.U64)
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
  match o with
  | none => ok (done total)
  | some i =>
    let i1 ← total <<< 8#i32
    let i2 ← Slice.index_usize x i
    let i3 ← lift (core.convert.num.FromU64U8.from i2)
    let total1 ← i1 + i3
    ok (cont (iter1, total1))

/-- [fips205::helpers::to_int]: loop 0:
    Source: 'src/helpers.rs', lines 20:4-26:5 -/
@[rust_loop]
def helpers.to_int_loop
  (iter : core.ops.range.Range Std.Usize) (x : Slice Std.U8) (total : Std.U64)
  :
  Result Std.U64
  := do
  loop
    (fun (iter1, total1) => helpers.to_int_loop.body x iter1 total1)
    (iter, total)

/-- [fips205::helpers::to_int]:
    Source: 'src/helpers.rs', lines 9:0-30:1 -/
def helpers.to_int (x : Slice Std.U8) (n : Std.U32) : Result Std.U64 := do
  let left_val := Slice.len x
  let right_val ← lift (UScalar.cast .Usize n)
  massert (left_val = right_val)
  massert (n <= 8#u32)
  let i ← lift (UScalar.cast .Usize n)
  helpers.to_int_loop { start := 0#usize, «end» := i } x 0#u64

/-- [fips205::LEN2]
    Source: 'src/lib.rs', lines 74:0-74:20 -/
@[global_simps, irreducible] def LEN2 : Std.U32 := 3#u32

/-- [fips205::LGW]
    Source: 'src/lib.rs', lines 72:0-72:19 -/
@[global_simps, irreducible] def LGW : Std.U32 := 4#u32

/-- [fips205::helpers::to_byte]: loop body 0:
    Source: 'src/helpers.rs', lines 47:4-56:5 -/
@[rust_loop_body]
def helpers.to_byte_loop.body
  (n : Std.U32) (iter : core.ops.range.Range Std.U32)
  (s : Array Std.U8 2#usize) (total : Std.U32) :
  Result (ControlFlow ((core.ops.range.Range Std.U32) × (Array Std.U8 2#usize)
    × Std.U32) (Array Std.U8 2#usize))
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next U32.Insts.CoreIterRangeStep iter
  match o with
  | none => ok (done s)
  | some i =>
    let a ← lift (core.num.U32.to_le_bytes total)
    let i1 ← Array.index_usize a 0#usize
    let i2 ← n - 1#u32
    let i3 ← i2 - i
    let i4 ← lift (UScalar.cast .Usize i3)
    let a1 ← Array.update s i4 i1
    let total1 ← total >>> 8#i32
    ok (cont (iter1, a1, total1))

/-- [fips205::helpers::to_byte]: loop 0:
    Source: 'src/helpers.rs', lines 47:4-56:5 -/
@[rust_loop]
def helpers.to_byte_loop
  (iter : core.ops.range.Range Std.U32) (n : Std.U32)
  (s : Array Std.U8 2#usize) (total : Std.U32) :
  Result (Array Std.U8 2#usize)
  := do
  loop
    (fun (iter1, s1, total1) => helpers.to_byte_loop.body n iter1 s1 total1)
    (iter, s, total)

/-- [fips205::helpers::to_byte]:
    Source: 'src/helpers.rs', lines 38:0-60:1 -/
def helpers.to_byte
  (x : Std.U32) (n : Std.U32) : Result (Array Std.U8 2#usize) := do
  let s := Array.repeat 2#usize 0#u8
  let i ← LEN2 * LGW
  let _ ← i + 7#u32
  let i1 ← lift (Std.U32.wrapping_mul LEN2 LGW)
  let i2 ← lift (Std.U32.wrapping_add i1 7#u32)
  let right_val ← i2 / 8#u32
  massert (n = right_val)
  massert (n = 2#u32)
  helpers.to_byte_loop { start := 0#u32, «end» := n } n s x

/-- [fips205::helpers::base_2b]: loop body 1:
    Source: 'src/helpers.rs', lines 90:8-102:9 -/
@[rust_loop_body]
def helpers.base_2b_loop0_loop0.body
  (x : Slice Std.U8) (b : Std.U32) (inn : Std.Usize) (bits : Std.U32)
  (total : Std.U32) :
  Result (ControlFlow (Std.Usize × Std.U32 × Std.U32) (Std.Usize × Std.U32
    × Std.U32))
  := do
  if bits < b
  then
    let i ← total <<< 8#i32
    let i1 ← Slice.index_usize x inn
    let i2 ← lift (core.convert.num.FromU32U8.from i1)
    let total1 ← i + i2
    let inn1 ← inn + 1#usize
    let bits1 ← bits + 8#u32
    ok (cont (inn1, bits1, total1))
  else ok (done (inn, bits, total))

/-- [fips205::helpers::base_2b]: loop 1:
    Source: 'src/helpers.rs', lines 90:8-102:9 -/
@[rust_loop]
def helpers.base_2b_loop0_loop0
  (x : Slice Std.U8) (b : Std.U32) (inn : Std.Usize) (bits : Std.U32)
  (total : Std.U32) :
  Result (Std.Usize × Std.U32 × Std.U32)
  := do
  loop
    (fun (inn1, bits1, total1) => helpers.base_2b_loop0_loop0.body x b inn1
      bits1 total1)
    (inn, bits, total)

/-- [fips205::helpers::base_2b]: loop body 0:
    Source: 'src/helpers.rs', lines 87:4-111:5 -/
@[rust_loop_body]
def helpers.base_2b_loop0.body
  (x : Slice Std.U8) (b : Std.U32) (iter : core.ops.range.Range Std.Usize)
  (baseb : Slice Std.U32) (inn : Std.Usize) (bits : Std.U32) (total : Std.U32)
  :
  Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Slice Std.U32) ×
    Std.Usize × Std.U32 × Std.U32) (Slice Std.U32))
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
  match o with
  | none => ok (done baseb)
  | some out =>
    let (inn1, bits1, total1) ←
      helpers.base_2b_loop0_loop0 x b inn bits total
    let bits2 ← bits1 - b
    let i ← total1 >>> bits2
    let i1 ← 32#u32 - b
    let i2 ← core.num.U32.MAX >>> i1
    let i3 ← lift (i &&& i2)
    let s ← Slice.update baseb out i3
    ok (cont (iter1, s, inn1, bits2, total1))

/-- [fips205::helpers::base_2b]: loop 0:
    Source: 'src/helpers.rs', lines 87:4-111:5 -/
@[rust_loop]
def helpers.base_2b_loop0
  (iter : core.ops.range.Range Std.Usize) (x : Slice Std.U8) (b : Std.U32)
  (baseb : Slice Std.U32) (inn : Std.Usize) (bits : Std.U32) (total : Std.U32)
  :
  Result (Slice Std.U32)
  := do
  loop
    (fun (iter1, baseb1, inn1, bits1, total1) => helpers.base_2b_loop0.body x b
      iter1 baseb1 inn1 bits1 total1)
    (iter, baseb, inn, bits, total)

/-- [fips205::helpers::base_2b]:
    Source: 'src/helpers.rs', lines 68:0-114:1 -/
def helpers.base_2b
  (x : Slice Std.U8) (b : Std.U32) (out_len : Std.U32) (baseb : Slice Std.U32)
  :
  Result (Slice Std.U32)
  := do
  let i := Slice.len x
  let i1 ← out_len * b
  let i2 ← i1 + 7#u32
  let i3 ← i2 / 8#u32
  let i4 ← lift (UScalar.cast .Usize i3)
  massert (i >= i4)
  massert (b < 16#u32)
  let left_val ← lift (UScalar.cast .Usize out_len)
  let right_val := Slice.len baseb
  massert (left_val = right_val)
  let i5 ← lift (UScalar.cast .Usize out_len)
  helpers.base_2b_loop0 { start := 0#usize, «end» := i5 } x b baseb 0#usize
    0#u32 0#u32

/-- [fips205::helpers::{fips205::types::Adrs}::set_layer_address]:
    Source: 'src/helpers.rs', lines 207:4-207:86 -/
def helpers.Adrs.set_layer_address
  (self : types.Adrs) (la : Std.U32) : Result types.Adrs := do
  let a ← lift (core.num.U32.to_be_bytes la)
  ok { self with f0 := a }

/-- [fips205::helpers::{fips205::types::Adrs}::get_key_pair_address]:
    Source: 'src/helpers.rs', lines 209:4-209:84 -/
def helpers.Adrs.get_key_pair_address
  (self : types.Adrs) : Result Std.U32 := do
  ok (core.num.U32.from_be_bytes self.f5)

/-- [fips205::helpers::{fips205::types::Adrs}::set_key_pair_address]:
    Source: 'src/helpers.rs', lines 211:4-211:100 -/
def helpers.Adrs.set_key_pair_address
  (self : types.Adrs) (kp_addr : Std.U32) : Result types.Adrs := do
  let a ← lift (core.num.U32.to_be_bytes kp_addr)
  ok { self with f5 := a }

/-- [fips205::helpers::{fips205::types::Adrs}::set_chain_address]:
    Source: 'src/helpers.rs', lines 213:4-213:85 -/
def helpers.Adrs.set_chain_address
  (self : types.Adrs) (i : Std.U32) : Result types.Adrs := do
  let a ← lift (core.num.U32.to_be_bytes i)
  ok { self with f6 := a }

/-- [fips205::helpers::{fips205::types::Adrs}::set_type_and_clear]:
    Source: 'src/helpers.rs', lines 215:4-220:5 -/
def helpers.Adrs.set_type_and_clear
  (self : types.Adrs) (type_t : Std.U32) : Result types.Adrs := do
  let a ← lift (core.num.U32.to_be_bytes type_t)
  let a1 ← lift (core.num.U32.to_be_bytes 0#u32)
  let a2 ← lift (core.num.U32.to_be_bytes 0#u32)
  let a3 ← lift (core.num.U32.to_be_bytes 0#u32)
  ok { self with f4 := a, f5 := a1, f6 := a2, f7 := a3 }

/-- [fips205::helpers::{fips205::types::Adrs}::set_tree_address]:
    Source: 'src/helpers.rs', lines 222:4-226:5 -/
def helpers.Adrs.set_tree_address
  (self : types.Adrs) (t : Std.U64) : Result types.Adrs := do
  let bytes ← lift (core.num.U64.to_be_bytes t)
  let (s, to_slice_mut_back) ← lift (Array.to_slice_mut self.f2)
  let s1 ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.slice.index.SliceIndexRangeToUsizeSlice Std.U8)) bytes
      { «end» := 4#usize }
  let s2 ← core.slice.Slice.copy_from_slice core.marker.CopyU8 s s1
  let (s3, to_slice_mut_back1) ← lift (Array.to_slice_mut self.f3)
  let s4 ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U8)) bytes
      { start := 4#usize }
  let s5 ← core.slice.Slice.copy_from_slice core.marker.CopyU8 s3 s4
  let a := to_slice_mut_back s2
  let a1 := to_slice_mut_back1 s5
  ok { self with f2 := a, f3 := a1 }

/-- [fips205::helpers::{fips205::types::Adrs}::set_hash_address]:
    Source: 'src/helpers.rs', lines 228:4-228:89 -/
def helpers.Adrs.set_hash_address
  (self : types.Adrs) (addr : Std.U32) : Result types.Adrs := do
  let a ← lift (core.num.U32.to_be_bytes addr)
  ok { self with f7 := a }

/-- [fips205::helpers::{fips205::types::Adrs}::set_tree_height]:
    Source: 'src/helpers.rs', lines 230:4-230:82 -/
def helpers.Adrs.set_tree_height
  (self : types.Adrs) (z : Std.U32) : Result types.Adrs := do
  let a ← lift (core.num.U32.to_be_bytes z)
  ok { self with f6 := a }

/-- [fips205::helpers::{fips205::types::Adrs}::get_tree_index]:
    Source: 'src/helpers.rs', lines 232:4-232:82 -/
def helpers.Adrs.get_tree_index
  (self : types.Adrs) : Result (Std.U32 × types.Adrs) := do
  let i ← lift (core.num.U32.from_be_bytes self.f7)
  ok (i, self)

/-- [fips205::helpers::{fips205::types::Adrs}::set_tree_index]:
    Source: 'src/helpers.rs', lines 234:4-234:81 -/
def helpers.Adrs.set_tree_index
  (self : types.Adrs) (i : Std.U32) : Result types.Adrs := do
  let a ← lift (core.num.U32.to_be_bytes i)
  ok { self with f7 := a }

/-- [fips205::W]
    Source: 'src/lib.rs', lines 73:0-73:18 -/
@[global_simps, irreducible] def W : Std.U32 := 16#u32

/-- [fips205::types::{impl core::ops::drop::Drop for fips205::types::ForsPk<N>}::drop]:
    Source: 'src/types.rs', lines 59:25-59:38
    Visibility: public -/
def types.ForsPk.Insts.CoreOpsDropDrop.drop
  {N : Std.Usize} (self : types.ForsPk N) : Result (types.ForsPk N) := do
  let key ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize N (zeroize.Zeroize.Blanket
      U8.Insts.ZeroizeDefaultIsZeroes)) self.key
  ok { key }

/-- [fips205::types::{impl core::clone::Clone for fips205::types::Auth<A, N>}::clone]:
    Source: 'src/types.rs', lines 65:9-65:14
    Visibility: public -/
def types.Auth.Insts.CoreCloneClone.clone
  {A : Std.Usize} {N : Std.Usize} (self : types.Auth A N) :
  Result (types.Auth A N)
  := do
  let a ←
    core.array.CloneArray.clone (core.clone.CloneArray N core.clone.CloneU8)
      self.tree
  ok { tree := a }

/-- [fips205::types::{impl core::ops::drop::Drop for fips205::types::Auth<A, N>}::drop]:
    Source: 'src/types.rs', lines 65:32-65:45
    Visibility: public -/
def types.Auth.Insts.CoreOpsDropDrop.drop
  {A : Std.Usize} {N : Std.Usize} (self : types.Auth A N) :
  Result (types.Auth A N)
  := do
  let tree ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize A (Array.Insts.ZeroizeZeroize N
      (zeroize.Zeroize.Blanket U8.Insts.ZeroizeDefaultIsZeroes))) self.tree
  ok { tree }

/-- [fips205::types::{impl core::clone::Clone for fips205::types::WotsSig<LEN, N>}::clone]:
    Source: 'src/types.rs', lines 79:9-79:14
    Visibility: public -/
def types.WotsSig.Insts.CoreCloneClone.clone
  {LEN : Std.Usize} {N : Std.Usize} (self : types.WotsSig LEN N) :
  Result (types.WotsSig LEN N)
  := do
  let a ←
    core.array.CloneArray.clone (core.clone.CloneArray N core.clone.CloneU8)
      self.data
  ok { data := a }

/-- [fips205::types::{impl zeroize::Zeroize for fips205::types::WotsSig<LEN, N>}::zeroize]:
    Source: 'src/types.rs', lines 79:23-79:30
    Visibility: public -/
def types.WotsSig.Insts.ZeroizeZeroize.zeroize
  {LEN : Std.Usize} {N : Std.Usize} (self : types.WotsSig LEN N) :
  Result (types.WotsSig LEN N)
  := do
  let data ←
    Array.Insts.ZeroizeZeroize.zeroize (Array.Insts.ZeroizeZeroize N
      (zeroize.Zeroize.Blanket U8.Insts.ZeroizeDefaultIsZeroes)) self.data
  ok { data }

/-- Trait implementation: [fips205::types::{impl zeroize::Zeroize for fips205::types::WotsSig<LEN, N>}]
    Source: 'src/types.rs', lines 79:23-79:30 -/
@[reducible]
def types.WotsSig.Insts.ZeroizeZeroize (LEN : Std.Usize) (N : Std.Usize) :
  zeroize.Zeroize (types.WotsSig LEN N) := {
  zeroize := types.WotsSig.Insts.ZeroizeZeroize.zeroize
}

/-- [fips205::types::{impl core::ops::drop::Drop for fips205::types::WotsSig<LEN, N>}::drop]:
    Source: 'src/types.rs', lines 79:32-79:45
    Visibility: public -/
def types.WotsSig.Insts.CoreOpsDropDrop.drop
  {LEN : Std.Usize} {N : Std.Usize} (self : types.WotsSig LEN N) :
  Result (types.WotsSig LEN N)
  := do
  let data ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize LEN (Array.Insts.ZeroizeZeroize N
      (zeroize.Zeroize.Blanket U8.Insts.ZeroizeDefaultIsZeroes))) self.data
  ok { data }

/-- [fips205::types::{impl core::ops::drop::Drop for fips205::types::WotsPk<N>}::drop]:
    Source: 'src/types.rs', lines 85:25-85:38
    Visibility: public -/
def types.WotsPk.Insts.CoreOpsDropDrop.drop
  {N : Std.Usize} (self : types.WotsPk N) : Result (types.WotsPk N) := do
  let __zeroize_field_0 ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize N (zeroize.Zeroize.Blanket
      U8.Insts.ZeroizeDefaultIsZeroes)) self
  ok __zeroize_field_0

/-- [fips205::types::{impl core::clone::Clone for fips205::types::XmssSig<HP, LEN, N>}::clone]:
    Source: 'src/types.rs', lines 90:9-90:14
    Visibility: public -/
def types.XmssSig.Insts.CoreCloneClone.clone
  {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize}
  (self : types.XmssSig HP LEN N) :
  Result (types.XmssSig HP LEN N)
  := do
  let ws ← types.WotsSig.Insts.CoreCloneClone.clone self.sig_wots
  let a ←
    core.array.CloneArray.clone (core.clone.CloneArray N core.clone.CloneU8)
      self.auth
  ok { sig_wots := ws, auth := a }

/-- [fips205::types::{impl core::ops::drop::Drop for fips205::types::XmssSig<HP, LEN, N>}::drop]:
    Source: 'src/types.rs', lines 90:32-90:45
    Visibility: public -/
def types.XmssSig.Insts.CoreOpsDropDrop.drop
  {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize}
  (self : types.XmssSig HP LEN N) :
  Result (types.XmssSig HP LEN N)
  := do
  let sig_wots ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (types.WotsSig.Insts.ZeroizeZeroize LEN N) self.sig_wots
  let auth ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize HP (Array.Insts.ZeroizeZeroize N
      (zeroize.Zeroize.Blanket U8.Insts.ZeroizeDefaultIsZeroes))) self.auth
  ok { sig_wots, auth }

/-- [fips205::types::{fips205::types::XmssSig<HP, LEN, N>}::get_wots_sig]:
    Source: 'src/types.rs', lines 98:4-98:76 -/
def types.XmssSig.get_wots_sig
  {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize}
  (self : types.XmssSig HP LEN N) :
  Result (types.WotsSig LEN N)
  := do
  ok self.sig_wots

/-- [fips205::types::{fips205::types::XmssSig<HP, LEN, N>}::get_xmss_auth]:
    Source: 'src/types.rs', lines 100:4-100:71 -/
def types.XmssSig.get_xmss_auth
  {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize}
  (self : types.XmssSig HP LEN N) :
  Result (Array (Array Std.U8 N) HP)
  := do
  ok self.auth

/-- [fips205::types::WOTS_HASH]
    Source: 'src/types.rs', lines 104:0-104:36 -/
@[global_simps, irreducible] def types.WOTS_HASH : Std.U32 := 0#u32

/-- [fips205::types::WOTS_PK]
    Source: 'src/types.rs', lines 105:0-105:34 -/
@[global_simps, irreducible] def types.WOTS_PK : Std.U32 := 1#u32

/-- [fips205::types::TREE]
    Source: 'src/types.rs', lines 106:0-106:31 -/
@[global_simps, irreducible] def types.TREE : Std.U32 := 2#u32

/-- [fips205::types::FORS_TREE]
    Source: 'src/types.rs', lines 107:0-107:36 -/
@[global_simps, irreducible] def types.FORS_TREE : Std.U32 := 3#u32

/-- [fips205::types::FORS_ROOTS]
    Source: 'src/types.rs', lines 108:0-108:37 -/
@[global_simps, irreducible] def types.FORS_ROOTS : Std.U32 := 4#u32

/-- [fips205::types::{impl core::clone::Clone for fips205::types::Adrs}::clone]:
    Source: 'src/types.rs', lines 114:9-114:14
    Visibility: public -/
def types.Adrs.Insts.CoreCloneClone.clone
  (self : types.Adrs) : Result types.Adrs := do
  let a ← core.array.CloneArray.clone core.clone.CloneU8 self.f0
  let a1 ← core.array.CloneArray.clone core.clone.CloneU8 self.f1
  let a2 ← core.array.CloneArray.clone core.clone.CloneU8 self.f2
  let a3 ← core.array.CloneArray.clone core.clone.CloneU8 self.f3
  let a4 ← core.array.CloneArray.clone core.clone.CloneU8 self.f4
  let a5 ← core.array.CloneArray.clone core.clone.CloneU8 self.f5
  let a6 ← core.array.CloneArray.clone core.clone.CloneU8 self.f6
  let a7 ← core.array.CloneArray.clone core.clone.CloneU8 self.f7
  ok
    {
      f0 := a,
      f1 := a1,
      f2 := a2,
      f3 := a3,
      f4 := a4,
      f5 := a5,
      f6 := a6,
      f7 := a7
    }

/-- [fips205::types::{impl core::default::Default for fips205::types::Adrs}::default]:
    Source: 'src/types.rs', lines 114:16-114:23
    Visibility: public -/
def types.Adrs.Insts.CoreDefaultDefault.default : Result types.Adrs := do
  let a ← core.default.DefaultArray.default 4#usize core.default.DefaultU8
  ok { f0 := a, f1 := a, f2 := a, f3 := a, f4 := a, f5 := a, f6 := a, f7 := a }

/-- [fips205::types::{impl core::ops::drop::Drop for fips205::types::Adrs}::drop]:
    Source: 'src/types.rs', lines 114:34-114:47
    Visibility: public -/
def types.Adrs.Insts.CoreOpsDropDrop.drop
  (self : types.Adrs) : Result types.Adrs := do
  let f0 ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize 4#usize (zeroize.Zeroize.Blanket
      U8.Insts.ZeroizeDefaultIsZeroes)) self.f0
  let f1 ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize 4#usize (zeroize.Zeroize.Blanket
      U8.Insts.ZeroizeDefaultIsZeroes)) self.f1
  let f2 ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize 4#usize (zeroize.Zeroize.Blanket
      U8.Insts.ZeroizeDefaultIsZeroes)) self.f2
  let f3 ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize 4#usize (zeroize.Zeroize.Blanket
      U8.Insts.ZeroizeDefaultIsZeroes)) self.f3
  let f4 ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize 4#usize (zeroize.Zeroize.Blanket
      U8.Insts.ZeroizeDefaultIsZeroes)) self.f4
  let f5 ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize 4#usize (zeroize.Zeroize.Blanket
      U8.Insts.ZeroizeDefaultIsZeroes)) self.f5
  let f6 ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize 4#usize (zeroize.Zeroize.Blanket
      U8.Insts.ZeroizeDefaultIsZeroes)) self.f6
  let f7 ←
    zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
      (Array.Insts.ZeroizeZeroize 4#usize (zeroize.Zeroize.Blanket
      U8.Insts.ZeroizeDefaultIsZeroes)) self.f7
  ok { f0, f1, f2, f3, f4, f5, f6, f7 }

/-- [fips205::verify_mono::chain_free]: loop body 0:
    Source: 'src/verify_mono.rs', lines 97:4-100:5 -/
@[rust_loop_body]
def verify_mono.chain_free_loop.body
  {N : Std.Usize} (pk_seed : Slice Std.U8)
  (iter : core.ops.range.Range Std.U32) (adrs : types.Adrs)
  (tmp : Array Std.U8 N) :
  Result (ControlFlow ((core.ops.range.Range Std.U32) × types.Adrs × (Array
    Std.U8 N)) (Array Std.U8 N))
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next U32.Insts.CoreIterRangeStep iter
  match o with
  | none => ok (done tmp)
  | some j =>
    let adrs1 ← helpers.Adrs.set_hash_address adrs j
    let s ← lift (Array.to_slice tmp)
    let tmp1 ← verify_mono.oracle.f N pk_seed adrs1 s
    ok (cont (iter1, adrs1, tmp1))

/-- [fips205::verify_mono::chain_free]: loop 0:
    Source: 'src/verify_mono.rs', lines 97:4-100:5 -/
@[rust_loop]
def verify_mono.chain_free_loop
  {N : Std.Usize} (iter : core.ops.range.Range Std.U32)
  (pk_seed : Slice Std.U8) (adrs : types.Adrs) (tmp : Array Std.U8 N) :
  Result (Array Std.U8 N)
  := do
  loop
    (fun (iter1, adrs1, tmp1) => verify_mono.chain_free_loop.body pk_seed iter1
      adrs1 tmp1)
    (iter, adrs, tmp)

/-- [fips205::verify_mono::chain_free]:
    Source: 'src/verify_mono.rs', lines 91:0-102:1 -/
def verify_mono.chain_free
  {N : Std.Usize} (cap_x : Array Std.U8 N) (i : Std.U32) (s : Std.U32)
  (pk_seed : Slice Std.U8) (adrs : types.Adrs) :
  Result (Array Std.U8 N)
  := do
  let i1 ← i + s
  massert (i1 < core.num.U32.MAX)
  let adrs1 ← types.Adrs.Insts.CoreCloneClone.clone adrs
  verify_mono.chain_free_loop { start := i, «end» := i1 } pk_seed adrs1 cap_x

/-- [fips205::verify_mono::wots_pk_from_sig_free]: loop body 0:
    Source: 'src/verify_mono.rs', lines 122:4-124:5 -/
@[rust_loop_body]
def verify_mono.wots_pk_from_sig_free_loop0.body
  {LEN : Std.Usize} (msg : Array Std.U32 LEN)
  (iter : core.ops.range.Range Std.Usize) (csum : Std.U32) :
  Result (ControlFlow ((core.ops.range.Range Std.Usize) × Std.U32) Std.U32)
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
  match o with
  | none => ok (done csum)
  | some i =>
    let i1 ← W - 1#u32
    let i2 ← Array.index_usize msg i
    let i3 ← i1 - i2
    let csum1 ← csum + i3
    ok (cont (iter1, csum1))

/-- [fips205::verify_mono::wots_pk_from_sig_free]: loop 0:
    Source: 'src/verify_mono.rs', lines 122:4-124:5 -/
@[rust_loop]
def verify_mono.wots_pk_from_sig_free_loop0
  {LEN : Std.Usize} (iter : core.ops.range.Range Std.Usize) (csum : Std.U32)
  (msg : Array Std.U32 LEN) :
  Result Std.U32
  := do
  loop
    (fun (iter1, csum1) => verify_mono.wots_pk_from_sig_free_loop0.body msg
      iter1 csum1)
    (iter, csum)

/-- [fips205::verify_mono::wots_pk_from_sig_free]: loop body 1:
    Source: 'src/verify_mono.rs', lines 135:4-144:5 -/
@[rust_loop_body]
def verify_mono.wots_pk_from_sig_free_loop1.body
  {LEN : Std.Usize} {N : Std.Usize} (sig : types.WotsSig LEN N)
  (pk_seed : Slice Std.U8) (msg : Array Std.U32 LEN)
  (iter : core.ops.range.Range Std.Usize) (adrs : types.Adrs)
  (tmp : Array (Array Std.U8 N) LEN) :
  Result (ControlFlow ((core.ops.range.Range Std.Usize) × types.Adrs × (Array
    (Array Std.U8 N) LEN)) (types.Adrs × (Array (Array Std.U8 N) LEN)))
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
  match o with
  | none => ok (done (adrs, tmp))
  | some i =>
    let i1 ← lift (UScalar.cast .U32 i)
    let adrs1 ← helpers.Adrs.set_chain_address adrs i1
    let a ← Array.index_usize sig.data i
    let i2 ← Array.index_usize msg i
    let i3 ← W - 1#u32
    let i4 ← i3 - i2
    let a1 ← verify_mono.chain_free a i2 i4 pk_seed adrs1
    let a2 ← Array.update tmp i a1
    ok (cont (iter1, adrs1, a2))

/-- [fips205::verify_mono::wots_pk_from_sig_free]: loop 1:
    Source: 'src/verify_mono.rs', lines 135:4-144:5 -/
@[rust_loop]
def verify_mono.wots_pk_from_sig_free_loop1
  {LEN : Std.Usize} {N : Std.Usize} (iter : core.ops.range.Range Std.Usize)
  (sig : types.WotsSig LEN N) (pk_seed : Slice Std.U8) (adrs : types.Adrs)
  (tmp : Array (Array Std.U8 N) LEN) (msg : Array Std.U32 LEN) :
  Result (types.Adrs × (Array (Array Std.U8 N) LEN))
  := do
  loop
    (fun (iter1, adrs1, tmp1) => verify_mono.wots_pk_from_sig_free_loop1.body
      sig pk_seed msg iter1 adrs1 tmp1)
    (iter, adrs, tmp)

/-- [fips205::verify_mono::wots_pk_from_sig_free]:
    Source: 'src/verify_mono.rs', lines 107:0-151:1 -/
def verify_mono.wots_pk_from_sig_free
  {LEN : Std.Usize} {N : Std.Usize} (sig : types.WotsSig LEN N)
  (m : Slice Std.U8) (pk_seed : Slice Std.U8) (adrs : types.Adrs) :
  Result (types.WotsPk N)
  := do
  let n32 ← lift (UScalar.cast .U32 N)
  let adrs1 ← types.Adrs.Insts.CoreCloneClone.clone adrs
  let a := Array.repeat N 0#u8
  let tmp := Array.repeat LEN a
  let msg := Array.repeat LEN 0#u32
  let i ← 2#u32 * n32
  let i1 ← 2#usize * N
  let (s, index_mut_back) ←
    core.array.Array.index_mut (core.ops.index.IndexMutSlice
      (core.slice.index.SliceIndexRangeUsizeSlice Std.U32)) msg
      { start := 0#usize, «end» := i1 }
  let s1 ← helpers.base_2b m LGW i s
  let msg1 := index_mut_back s1
  let csum ←
    verify_mono.wots_pk_from_sig_free_loop0 { start := 0#usize, «end» := i1 }
      0#u32 msg1
  let i2 ← LEN2 * LGW
  let i3 ← lift (i2 &&& 7#u32)
  let i4 ← 8#u32 - i3
  let i5 ← lift (i4 &&& 7#u32)
  let csum1 ← csum <<< i5
  let i6 ← i2 + 7#u32
  let i7 ← i6 / 8#u32
  let a1 ← helpers.to_byte csum1 i7
  let s2 ← lift (Array.to_slice a1)
  let (s3, index_mut_back1) ←
    core.array.Array.index_mut (core.ops.index.IndexMutSlice
      (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U32)) msg1
      { start := i1 }
  let s4 ← helpers.base_2b s2 LGW LEN2 s3
  let msg2 := index_mut_back1 s4
  let (adrs2, tmp1) ←
    verify_mono.wots_pk_from_sig_free_loop1
      { start := 0#usize, «end» := LEN } sig pk_seed adrs1 tmp msg2
  let wotspk_adrs ← types.Adrs.Insts.CoreCloneClone.clone adrs2
  let wotspk_adrs1 ←
    helpers.Adrs.set_type_and_clear wotspk_adrs types.WOTS_PK
  let i8 ← helpers.Adrs.get_key_pair_address adrs2
  let wotspk_adrs2 ← helpers.Adrs.set_key_pair_address wotspk_adrs1 i8
  let pk ← verify_mono.oracle.t_l pk_seed wotspk_adrs2 tmp1
  ok pk

/-- [fips205::verify_mono::xmss_pk_from_sig_free]: loop body 0:
    Source: 'src/verify_mono.rs', lines 173:4-185:5 -/
@[rust_loop_body]
def verify_mono.xmss_pk_from_sig_free_loop.body
  {HP : Std.Usize} {N : Std.Usize} (idx : Std.U32) (pk_seed : Slice Std.U8)
  (auth : Array (Array Std.U8 N) HP) (iter : core.ops.range.Range Std.U32)
  (adrs : types.Adrs) (node_0 : Array Std.U8 N) :
  Result (ControlFlow ((core.ops.range.Range Std.U32) × types.Adrs × (Array
    Std.U8 N)) (Array Std.U8 N))
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next U32.Insts.CoreIterRangeStep iter
  match o with
  | none => ok (done node_0)
  | some k =>
    let i ← k + 1#u32
    let adrs1 ← helpers.Adrs.set_tree_height adrs i
    let i1 ← idx >>> k
    let i2 ← lift (i1 &&& 1#u32)
    if i2 = 0#u32
    then
      let (i3, adrs2) ← helpers.Adrs.get_tree_index adrs1
      let tmp ← i3 / 2#u32
      let adrs3 ← helpers.Adrs.set_tree_index adrs2 tmp
      let s ← lift (Array.to_slice node_0)
      let i4 ← lift (UScalar.cast .Usize k)
      let a ← Array.index_usize auth i4
      let s1 ← lift (Array.to_slice a)
      let node_1 ← verify_mono.oracle.h N pk_seed adrs3 s s1
      ok (cont (iter1, adrs3, node_1))
    else
      let (i3, adrs2) ← helpers.Adrs.get_tree_index adrs1
      let i4 ← i3 - 1#u32
      let tmp ← i4 / 2#u32
      let adrs3 ← helpers.Adrs.set_tree_index adrs2 tmp
      let i5 ← lift (UScalar.cast .Usize k)
      let a ← Array.index_usize auth i5
      let s ← lift (Array.to_slice a)
      let s1 ← lift (Array.to_slice node_0)
      let node_1 ← verify_mono.oracle.h N pk_seed adrs3 s s1
      ok (cont (iter1, adrs3, node_1))

/-- [fips205::verify_mono::xmss_pk_from_sig_free]: loop 0:
    Source: 'src/verify_mono.rs', lines 173:4-185:5 -/
@[rust_loop]
def verify_mono.xmss_pk_from_sig_free_loop
  {HP : Std.Usize} {N : Std.Usize} (iter : core.ops.range.Range Std.U32)
  (idx : Std.U32) (pk_seed : Slice Std.U8) (adrs : types.Adrs)
  (auth : Array (Array Std.U8 N) HP) (node_0 : Array Std.U8 N) :
  Result (Array Std.U8 N)
  := do
  loop
    (fun (iter1, adrs1, node_01) => verify_mono.xmss_pk_from_sig_free_loop.body
      idx pk_seed auth iter1 adrs1 node_01)
    (iter, adrs, node_0)

/-- [fips205::verify_mono::xmss_pk_from_sig_free]:
    Source: 'src/verify_mono.rs', lines 156:0-188:1 -/
def verify_mono.xmss_pk_from_sig_free
  {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize} (idx : Std.U32)
  (sig_xmss : types.XmssSig HP LEN N) (m : Slice Std.U8)
  (pk_seed : Slice Std.U8) (adrs : types.Adrs) :
  Result (Array Std.U8 N)
  := do
  let hp32 ← lift (UScalar.cast .U32 HP)
  let adrs1 ← types.Adrs.Insts.CoreCloneClone.clone adrs
  let adrs2 ← helpers.Adrs.set_type_and_clear adrs1 types.WOTS_HASH
  let adrs3 ← helpers.Adrs.set_key_pair_address adrs2 idx
  let sig ← types.XmssSig.get_wots_sig sig_xmss
  let auth ← types.XmssSig.get_xmss_auth sig_xmss
  let wp ← verify_mono.wots_pk_from_sig_free sig m pk_seed adrs3
  let adrs4 ← helpers.Adrs.set_type_and_clear adrs3 types.TREE
  let adrs5 ← helpers.Adrs.set_tree_index adrs4 idx
  verify_mono.xmss_pk_from_sig_free_loop { start := 0#u32, «end» := hp32 }
    idx pk_seed adrs5 auth wp

/-- [fips205::verify_mono::ht_verify_free]: loop body 0:
    Source: 'src/verify_mono.rs', lines 206:4-220:5 -/
@[rust_loop_body]
def verify_mono.ht_verify_free_loop.body
  {D : Std.Usize} {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize}
  (a : Array (types.XmssSig HP LEN N) D) (pk_seed : Slice Std.U8)
  (hp32 : Std.U32) (iter : core.ops.range.Range Std.U32) (idx_tree : Std.U64)
  (adrs : types.Adrs) (node : Array Std.U8 N) :
  Result (ControlFlow ((core.ops.range.Range Std.U32) × Std.U64 × types.Adrs
    × (Array Std.U8 N)) (Array Std.U8 N))
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next U32.Insts.CoreIterRangeStep iter
  match o with
  | none => ok (done node)
  | some j =>
    let i ← 1#u64 <<< hp32
    let i1 ← i - 1#u64
    let i2 ← lift (idx_tree &&& i1)
    let idx_leaf ← lift (UScalar.cast .U32 i2)
    let idx_tree1 ← idx_tree >>> hp32
    let adrs1 ← helpers.Adrs.set_layer_address adrs j
    let adrs2 ← helpers.Adrs.set_tree_address adrs1 idx_tree1
    let i3 ← lift (UScalar.cast .Usize j)
    let xs ← Array.index_usize a i3
    let sig_tmp ← types.XmssSig.Insts.CoreCloneClone.clone xs
    let s ← lift (Array.to_slice node)
    let node1 ←
      verify_mono.xmss_pk_from_sig_free idx_leaf sig_tmp s pk_seed adrs2
    ok (cont (iter1, idx_tree1, adrs2, node1))

/-- [fips205::verify_mono::ht_verify_free]: loop 0:
    Source: 'src/verify_mono.rs', lines 206:4-220:5 -/
@[rust_loop]
def verify_mono.ht_verify_free_loop
  {D : Std.Usize} {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize}
  (iter : core.ops.range.Range Std.U32) (a : Array (types.XmssSig HP LEN N) D)
  (pk_seed : Slice Std.U8) (idx_tree : Std.U64) (hp32 : Std.U32)
  (adrs : types.Adrs) (node : Array Std.U8 N) :
  Result (Array Std.U8 N)
  := do
  loop
    (fun (iter1, idx_tree1, adrs1, node1) =>
      verify_mono.ht_verify_free_loop.body a pk_seed hp32 iter1 idx_tree1 adrs1
      node1)
    (iter, idx_tree, adrs, node)

/-- [fips205::verify_mono::ht_verify_free]:
    Source: 'src/verify_mono.rs', lines 193:0-223:1 -/
def verify_mono.ht_verify_free
  {D : Std.Usize} {HP : Std.Usize} {LEN : Std.Usize} {N : Std.Usize}
  (m : Slice Std.U8) (sig_ht : types.HtSig D HP LEN N) (pk_seed : Slice Std.U8)
  (idx_tree : Std.U64) (idx_leaf : Std.U32) (pk_root : Array Std.U8 N) :
  Result Bool
  := do
  let d32 ← lift (UScalar.cast .U32 D)
  let hp32 ← lift (UScalar.cast .U32 HP)
  let adrs ← types.Adrs.Insts.CoreDefaultDefault.default
  let adrs1 ← helpers.Adrs.set_tree_address adrs idx_tree
  let xs ← Array.index_usize sig_ht.xmss_sigs 0#usize
  let sig_tmp ← types.XmssSig.Insts.CoreCloneClone.clone xs
  let node ←
    verify_mono.xmss_pk_from_sig_free idx_leaf sig_tmp m pk_seed adrs1
  let node1 ←
    verify_mono.ht_verify_free_loop { start := 1#u32, «end» := d32 }
      sig_ht.xmss_sigs pk_seed idx_tree hp32 adrs1 node
  core.array.equality.PartialEqArray.eq core.cmp.PartialEqU8 node1 pk_root

/-- [fips205::verify_mono::fors_pk_from_sig_free]: loop body 1:
    Source: 'src/verify_mono.rs', lines 248:8-260:9 -/
@[rust_loop_body]
def verify_mono.fors_pk_from_sig_free_loop0_loop0.body
  {A : Std.Usize} {K : Std.Usize} {N : Std.Usize} (pk_seed : Slice Std.U8)
  (indices : Array Std.U32 K) (i : Std.U32) (auth : types.Auth A N)
  (iter : core.ops.range.Range Std.U32) (adrs : types.Adrs)
  (node_0 : Array Std.U8 N) :
  Result (ControlFlow ((core.ops.range.Range Std.U32) × types.Adrs × (Array
    Std.U8 N)) (types.Adrs × (Array Std.U8 N)))
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next U32.Insts.CoreIterRangeStep iter
  match o with
  | none => ok (done (adrs, node_0))
  | some j =>
    let i1 ← j + 1#u32
    let adrs1 ← helpers.Adrs.set_tree_height adrs i1
    let i2 ← lift (UScalar.cast .Usize i)
    let i3 ← Array.index_usize indices i2
    let i4 ← i3 >>> j
    let i5 ← lift (i4 &&& 1#u32)
    if i5 = 0#u32
    then
      let (i6, adrs2) ← helpers.Adrs.get_tree_index adrs1
      let tmp ← i6 / 2#u32
      let adrs3 ← helpers.Adrs.set_tree_index adrs2 tmp
      let s ← lift (Array.to_slice node_0)
      let i7 ← lift (UScalar.cast .Usize j)
      let a ← Array.index_usize auth.tree i7
      let s1 ← lift (Array.to_slice a)
      let node_1 ← verify_mono.oracle.h N pk_seed adrs3 s s1
      ok (cont (iter1, adrs3, node_1))
    else
      let (i6, adrs2) ← helpers.Adrs.get_tree_index adrs1
      let i7 ← i6 - 1#u32
      let tmp ← i7 / 2#u32
      let adrs3 ← helpers.Adrs.set_tree_index adrs2 tmp
      let i8 ← lift (UScalar.cast .Usize j)
      let a ← Array.index_usize auth.tree i8
      let s ← lift (Array.to_slice a)
      let s1 ← lift (Array.to_slice node_0)
      let node_1 ← verify_mono.oracle.h N pk_seed adrs3 s s1
      ok (cont (iter1, adrs3, node_1))

/-- [fips205::verify_mono::fors_pk_from_sig_free]: loop 1:
    Source: 'src/verify_mono.rs', lines 248:8-260:9 -/
@[rust_loop]
def verify_mono.fors_pk_from_sig_free_loop0_loop0
  {A : Std.Usize} {K : Std.Usize} {N : Std.Usize}
  (iter : core.ops.range.Range Std.U32) (pk_seed : Slice Std.U8)
  (adrs : types.Adrs) (indices : Array Std.U32 K) (i : Std.U32)
  (node_0 : Array Std.U8 N) (auth : types.Auth A N) :
  Result (types.Adrs × (Array Std.U8 N))
  := do
  loop
    (fun (iter1, adrs1, node_01) =>
      verify_mono.fors_pk_from_sig_free_loop0_loop0.body pk_seed indices i auth
      iter1 adrs1 node_01)
    (iter, adrs, node_0)

/-- [fips205::verify_mono::fors_pk_from_sig_free]: loop body 0:
    Source: 'src/verify_mono.rs', lines 238:4-263:5 -/
@[rust_loop_body]
def verify_mono.fors_pk_from_sig_free_loop0.body
  {A : Std.Usize} {K : Std.Usize} {N : Std.Usize}
  (sig_fors : types.ForsSig A K N) (pk_seed : Slice Std.U8) (a32 : Std.U32)
  (indices : Array Std.U32 K) (iter : core.ops.range.Range Std.U32)
  (adrs : types.Adrs) (root : Array (Array Std.U8 N) K) :
  Result (ControlFlow ((core.ops.range.Range Std.U32) × types.Adrs × (Array
    (Array Std.U8 N) K)) (types.Adrs × (Array (Array Std.U8 N) K)))
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next U32.Insts.CoreIterRangeStep iter
  match o with
  | none => ok (done (adrs, root))
  | some i =>
    let i1 ← lift (UScalar.cast .Usize i)
    let sk ← Array.index_usize sig_fors.private_key_value i1
    let adrs1 ← helpers.Adrs.set_tree_height adrs 0#u32
    let i2 ← i <<< a32
    let i3 ← lift (UScalar.cast .Usize i)
    let i4 ← Array.index_usize indices i3
    let i5 ← i2 + i4
    let adrs2 ← helpers.Adrs.set_tree_index adrs1 i5
    let s ← lift (Array.to_slice sk)
    let node_0 ← verify_mono.oracle.f N pk_seed adrs2 s
    let i6 ← lift (UScalar.cast .Usize i)
    let a ← Array.index_usize sig_fors.auth i6
    let auth ← types.Auth.Insts.CoreCloneClone.clone a
    let (adrs3, node_01) ←
      verify_mono.fors_pk_from_sig_free_loop0_loop0
        { start := 0#u32, «end» := a32 } pk_seed adrs2 indices i node_0 auth
    let i7 ← lift (UScalar.cast .Usize i)
    let a1 ← Array.update root i7 node_01
    ok (cont (iter1, adrs3, a1))

/-- [fips205::verify_mono::fors_pk_from_sig_free]: loop 0:
    Source: 'src/verify_mono.rs', lines 238:4-263:5 -/
@[rust_loop]
def verify_mono.fors_pk_from_sig_free_loop0
  {A : Std.Usize} {K : Std.Usize} {N : Std.Usize}
  (iter : core.ops.range.Range Std.U32) (sig_fors : types.ForsSig A K N)
  (pk_seed : Slice Std.U8) (a32 : Std.U32) (adrs : types.Adrs)
  (indices : Array Std.U32 K) (root : Array (Array Std.U8 N) K) :
  Result (types.Adrs × (Array (Array Std.U8 N) K))
  := do
  loop
    (fun (iter1, adrs1, root1) => verify_mono.fors_pk_from_sig_free_loop0.body
      sig_fors pk_seed a32 indices iter1 adrs1 root1)
    (iter, adrs, root)

/-- [fips205::verify_mono::fors_pk_from_sig_free]:
    Source: 'src/verify_mono.rs', lines 228:0-270:1 -/
def verify_mono.fors_pk_from_sig_free
  {A : Std.Usize} {K : Std.Usize} {N : Std.Usize}
  (sig_fors : types.ForsSig A K N) (md : Slice Std.U8) (pk_seed : Slice Std.U8)
  (adrs : types.Adrs) :
  Result (types.ForsPk N)
  := do
  let a32 ← lift (UScalar.cast .U32 A)
  let k32 ← lift (UScalar.cast .U32 K)
  let adrs1 ← types.Adrs.Insts.CoreCloneClone.clone adrs
  let indices := Array.repeat K 0#u32
  let (s, to_slice_mut_back) ← lift (Array.to_slice_mut indices)
  let s1 ← helpers.base_2b md a32 k32 s
  let a := Array.repeat N 0#u8
  let root := Array.repeat K a
  let indices1 := to_slice_mut_back s1
  let (adrs2, root1) ←
    verify_mono.fors_pk_from_sig_free_loop0 { start := 0#u32, «end» := k32 }
      sig_fors pk_seed a32 adrs1 indices1 root
  let fors_pk_adrs ← types.Adrs.Insts.CoreCloneClone.clone adrs2
  let fors_pk_adrs1 ←
    helpers.Adrs.set_type_and_clear fors_pk_adrs types.FORS_ROOTS
  let i ← helpers.Adrs.get_key_pair_address adrs2
  let fors_pk_adrs2 ← helpers.Adrs.set_key_pair_address fors_pk_adrs1 i
  let pk ← verify_mono.oracle.t_len pk_seed fors_pk_adrs2 root1
  ok { key := pk }

/-- [fips205::verify_mono::slh_verify_internal_free]:
    Source: 'src/verify_mono.rs', lines 276:0-332:1 -/
def verify_mono.slh_verify_internal_free
  {A : Std.Usize} {D : Std.Usize} (H : Std.Usize) {HP : Std.Usize} {K :
  Std.Usize} {LEN : Std.Usize} (M : Std.Usize) {N : Std.Usize}
  (mprime : Slice Std.U8) (sig : types.SlhDsaSig A D HP K LEN N)
  (pk : types.SlhPublicKey N) :
  Result Bool
  := do
  let d32 ← lift (UScalar.cast .U32 D)
  let h32 ← lift (UScalar.cast .U32 H)
  let adrs ← types.Adrs.Insts.CoreDefaultDefault.default
  let s ← lift (Array.to_slice sig.randomness)
  let s1 ← lift (Array.to_slice pk.pk_seed)
  let s2 ← lift (Array.to_slice pk.pk_root)
  let digest ← verify_mono.oracle.h_msg M s s1 s2 mprime
  let i ← K * A
  let i1 ← i + 7#usize
  let index1 ← i1 / 8#usize
  let md ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.slice.index.SliceIndexRangeUsizeSlice Std.U8)) digest
      { start := 0#usize, «end» := index1 }
  let i2 ← H / D
  let i3 ← H - i2
  let i4 ← i3 + 7#usize
  let i5 ← i4 / 8#usize
  let index2 ← index1 + i5
  let tmp_idx_tree ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.slice.index.SliceIndexRangeUsizeSlice Std.U8)) digest
      { start := index1, «end» := index2 }
  let i6 ← 8#usize * D
  let i7 ← H + i6
  let i8 ← i7 - 1#usize
  let i9 ← i8 / i6
  let index3 ← index2 + i9
  let tmp_idx_leaf ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.slice.index.SliceIndexRangeUsizeSlice Std.U8)) digest
      { start := index2, «end» := index3 }
  let i10 ← h32 / d32
  let i11 ← h32 - i10
  let i12 ← i11 + 7#u32
  let i13 ← i12 / 8#u32
  let i14 ← helpers.to_int tmp_idx_tree i13
  let i15 ← h32 - i10
  let i16 ← 64#u32 - i15
  let i17 ← core.num.U64.MAX >>> i16
  let idx_tree ← lift (i14 &&& i17)
  let i18 ← 8#u32 * d32
  let i19 ← h32 + i18
  let i20 ← i19 - 1#u32
  let i21 ← i20 / i18
  let i22 ← helpers.to_int tmp_idx_leaf i21
  let i23 ← 64#u32 - i10
  let i24 ← core.num.U64.MAX >>> i23
  let idx_leaf ← lift (i22 &&& i24)
  let adrs1 ← helpers.Adrs.set_tree_address adrs idx_tree
  let adrs2 ← helpers.Adrs.set_type_and_clear adrs1 types.FORS_TREE
  let idx_leaf_u32 ← lift (UScalar.cast .U32 idx_leaf)
  let adrs3 ← helpers.Adrs.set_key_pair_address adrs2 idx_leaf_u32
  let s3 ← lift (Array.to_slice pk.pk_seed)
  let pk_fors ← verify_mono.fors_pk_from_sig_free sig.fors_sig md s3 adrs3
  let s4 ← lift (Array.to_slice pk_fors.key)
  let s5 ← lift (Array.to_slice pk.pk_seed)
  verify_mono.ht_verify_free s4 sig.ht_sig s5 idx_tree idx_leaf_u32 pk.pk_root

/-- [fips205::verify_mono::slh_verify_128s]:
    Source: 'src/verify_mono.rs', lines 341:0-345:1 -/
def verify_mono.slh_verify_128s
  (mprime : Slice Std.U8)
  (sig : types.SlhDsaSig 12#usize 7#usize 9#usize 14#usize 35#usize 16#usize)
  (pk : types.SlhPublicKey 16#usize) :
  Result Bool
  := do
  verify_mono.slh_verify_internal_free 63#usize 30#usize mprime sig pk

end fips205