From 53c5b45e3f231fec2078fa0139f480fb268746c0 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Wed, 22 Jul 2026 22:21:19 +0200 Subject: [PATCH] Phase 1: clean extraction + type-checking SLH-DSA-SHA2-128s model MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The gate-0 fn-pointer blocker is cleared. This commits the phase-1 deliverable: - verification/extract.sh: re-pointed at the monomorphic root crate::verify_mono::slh_verify_128s with crate::verify_mono::oracle as the opaque SHA-2 boundary (against fips205-source @ 2d89ee3). - verification/gen/SlhVerify: the extracted Lean model — 62 defs, the full verify cone (chain -> wots -> xmss -> ht -> fors -> slh_verify_internal) up to the apex verify_mono.slh_verify_128s. No sorry, no admit. - verification/gen/SlhVerify/FunsExternal.lean + TypesExternal.lean: hand-maintained externals with the two-class justification header — (1) the five SHA-2 hash oracles = the deliberate cryptographic boundary (the only axioms the apex certificate will carry beyond Lean's three); (2) transpiler plumbing (try_from, is_err, iterator Step/Take, zeroize) adopted as axioms for the phase-1 type-check, to be discharged in the proof phase. - verification/check.sh: real Phase-1 button — compiles the model under lean-guard (memory-capped, serialized). GREEN. Still says NOTHING PROVEN: a well-formed model is not a correct one. Zero certificates. Proof layers (chain semantics -> ... -> acceptance equation) are the next task. Co-Authored-By: Claude Fable 5 --- .gitignore | 2 + README.md | 42 +- verification/check.sh | 48 +- verification/extract.sh | 19 +- verification/gen/SlhVerify/Funs.lean | 1162 +++++++++++++++++ verification/gen/SlhVerify/FunsExternal.lean | 200 +++ verification/gen/SlhVerify/Types.lean | 101 ++ verification/gen/SlhVerify/TypesExternal.lean | 23 + 8 files changed, 1567 insertions(+), 30 deletions(-) create mode 100644 verification/gen/SlhVerify/Funs.lean create mode 100644 verification/gen/SlhVerify/FunsExternal.lean create mode 100644 verification/gen/SlhVerify/Types.lean create mode 100644 verification/gen/SlhVerify/TypesExternal.lean diff --git a/.gitignore b/.gitignore index f41f5ec..5df2ca2 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,5 @@ *.olean target/ .lake/ +*_Template.lean +SlhVerify.llbc diff --git a/README.md b/README.md index 013950e..85d7435 100644 --- a/README.md +++ b/README.md @@ -5,12 +5,26 @@ path**, extracted from a pure-Rust implementation into Lean 4 via Charon/Aeneas — the same pipeline, discipline, and honesty rules as the four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`). -## STATUS: SKELETON — NOTHING PROVEN YET +## STATUS: MODEL EXTRACTED & TYPE-CHECKS — NOTHING PROVEN YET -There are **zero certificates** in this repository. `verification/check.sh` -exits non-green and says so. Every claim in this README below the line -"What will be claimed" is a *plan*, not a result. (Honesty invariant H5: -an honest gap outranks a hollow certificate.) +There are still **zero certificates** in this repository. What phase 1 +established (2026-07-22): + +- the Aeneas-compat patch landed in the snapshot (an additive monomorphic + SHA2-128s verify module reached through a named hash-oracle boundary); +- **charon and aeneas both exit 0** on the full verify cone — the gate-0 + fn-pointer blocker is gone; +- the extracted Lean model (`verification/gen/SlhVerify`, 62 defs, apex + `verify_mono.slh_verify_128s`) **type-checks under lean-guard** + (`verification/check.sh` Phase 1 is green); +- fidelity of the monomorphic path is pinned by a differential test in the + snapshot that agrees with the deployed verifier on valid / corrupted / + wrong-message signatures. + +A green Phase-1 compile proves the model is **well-formed**, NOT that the +verifier is correct. No operation theorem has been stated or proven. Every +claim under "What will be claimed" remains a *plan* (H5: an honest gap +outranks a hollow certificate). ## Subject @@ -61,12 +75,18 @@ this repository was created: with exactly **one obstruction class** (3 unique errors): the `crate::hashers::Hashers` struct of plain **function pointers** cannot be translated. -- **Consequence (campaign phase 1)**: an Aeneas-compat patch in - `fips205-source` will replace the fn-pointer struct with named opaque - free functions on the verify path — the same pattern as the - `sha512_new/update/finalize` shims in `curve25519-dalek-source`'s - verify glue. Until that patch lands, `verification/extract.sh` - documents intent and produces a partial model. +- **Phase 1 — DONE (2026-07-22)**: the Aeneas-compat patch landed in + `fips205-source` (snapshot `2d89ee3`): an additive monomorphic SHA2-128s + verify module (`src/verify_mono.rs`) whose hash suite is reached through + named free functions in `verify_mono::oracle` (marked opaque at the + Charon boundary) — the `sha512_*`-shim pattern. Two further compat + refinements: the message-digest input M' passes as a single `&[u8]` + (nested `&[&[u8]]` is untranslatable), and one `let-else` became the + `is_err`/`unwrap` idiom. `verification/extract.sh` now re-derives the + model from the mono root; charon + aeneas both exit 0, and + `verification/check.sh` compiles the result. The generic paths and all + twelve parameter sets are untouched (the only change to existing code is + two lines wiring the module). ## What will be claimed (when the button is green, not before) diff --git a/verification/check.sh b/verification/check.sh index 6e93d22..f70ca60 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -1,12 +1,44 @@ #!/usr/bin/env bash # The one-button claim for this repository (rigor invariant R3). -# Green output == the full claim. This script is the ONLY source of the -# word "proven" for this repo. +# +# PHASE 1 (current): compiles the extracted Lean model (gen/SlhVerify) under +# lean-guard. Green here means the monomorphic SHA2-128s verify cone +# translated and TYPE-CHECKS — it does NOT yet mean anything is proven. There +# are zero certificates; the proof layers come next. This script grows a +# Phase-2 (proofs) and Phase-3 (axiom audit) section as the pyramid rises, +# exactly like the ed25519 check.sh. set -euo pipefail -echo "fips205-slhdsa-verified — check" -echo "================================" -echo "SKELETON: 0 certificates. NOTHING PROVEN YET." -echo "Campaign phase 1 (Aeneas-compat patch + clean extraction) has not" -echo "landed. See README.md 'Gate-0 record' and TRUSTED-BASE.md." -exit 1 +HERE="$(cd "$(dirname "$0")" && pwd)" +source ~/aeneas-toolchain/env.sh +AENEAS_LEAN="$AENEAS_HOME/backends/lean" +TIMEOUT="${LEAN_TIMEOUT:-300}" +CORES="${LEAN_MAX_CORES:-4}" + +# Import order (each depends on the previous). +GEN_MODULES=( + "SlhVerify/TypesExternal" + "SlhVerify/Types" + "SlhVerify/FunsExternal" + "SlhVerify/Funs" +) + +echo "fips205-slhdsa-verified — check (PHASE 1: model compile only)" +echo "============================================================" +echo "NOTE: 0 certificates. A green compile proves the extracted model is" +echo "well-formed; it does NOT prove the verifier correct. See README.md." +echo + +LOG=$(mktemp /tmp/fips205-check-XXXX.log) +cd "$AENEAS_LEAN" +lake env bash -c " + set -euo pipefail + cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" + compile() { + echo \" · \$1\" + LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' \"\${1}.lean\" 2>&1 | tee -a '$LOG' || { echo \"FAIL: \$1\"; exit 1; } + } + for m in ${GEN_MODULES[*]}; do compile \"\$m\"; done +" +echo +echo "PHASE 1 GREEN: gen/SlhVerify model type-checks. Proofs are the next layer." diff --git a/verification/extract.sh b/verification/extract.sh index b9e72c3..ff934c8 100755 --- a/verification/extract.sh +++ b/verification/extract.sh @@ -25,20 +25,17 @@ source ~/aeneas-toolchain/env.sh HERE="$(cd "$(dirname "$0")" && pwd)" CRATE=~/GitClone/FormalVerification/sources/fips205-source -echo "[1/2] charon: Rust -> LLBC (verify cone, SHA2-128s, hash oracles opaque)" +echo "[1/2] charon: Rust -> LLBC (monomorphic SHA2-128s verify cone;" +echo " crate::verify_mono::oracle is the opaque SHA-2 boundary)" cd "$CRATE" +# Single extraction root: the monomorphic entry. The five hash primitives +# are reached through crate::verify_mono::oracle, marked opaque here — this +# is the deliberate SHA-2 trust boundary (documented in TRUSTED-BASE.md). +# The generic Hashers fn-pointer path is NOT in this cone by construction. charon cargo --preset=aeneas \ - --start-from 'crate::slh::slh_verify' \ - --start-from 'crate::slh::slh_verify_internal' \ - --start-from 'crate::fors::fors_pk_from_sig' \ - --start-from 'crate::hypertree::ht_verify' \ - --start-from 'crate::xmss::xmss_pk_from_sig' \ - --start-from 'crate::wots::wots_pk_from_sig' \ - --start-from 'crate::wots::chain' \ + --start-from 'crate::verify_mono::slh_verify_128s' \ + --opaque 'crate::verify_mono::oracle' \ --opaque 'sha2' --opaque 'sha3' --opaque 'zeroize' --opaque 'rand_core' \ - --opaque 'crate::hashers::sha2_cat_1' \ - --opaque 'crate::hashers::sha2_cat_3_5' \ - --opaque 'crate::hashers::shake' \ --hide-marker-traits \ --dest-file "$HERE/SlhVerify.llbc" \ -- --no-default-features --features slh_dsa_sha2_128s diff --git a/verification/gen/SlhVerify/Funs.lean b/verification/gen/SlhVerify/Funs.lean new file mode 100644 index 0000000..d9c5668 --- /dev/null +++ b/verification/gen/SlhVerify/Funs.lean @@ -0,0 +1,1162 @@ +-- 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] -/ +@[reducible, rust_trait_impl "core::iter::range::Step"] +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: [core::num::error::{impl core::fmt::Debug for core::num::error::TryFromIntError}] + Source: '/rustc/library/core/src/num/error.rs', lines 9:9-9:14 + Name pattern: [core::fmt::Debug] -/ +@[reducible, rust_trait_impl + "core::fmt::Debug"] +def core.num.error.TryFromIntError.Insts.CoreFmtDebug : core.fmt.Debug + core.num.error.TryFromIntError := { + fmt := core.num.error.TryFromIntError.Insts.CoreFmtDebug.fmt +} + +/-- 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] -/ +@[reducible, rust_trait_impl "zeroize::DefaultIsZeroes"] +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 17:4-23:5 -/ +@[rust_loop_body] +def helpers.to_int_loop.body + (iter : core.iter.adapters.take.Take (core.slice.iter.Iter Std.U8)) + (total : Std.U64) : + Result (ControlFlow ((core.iter.adapters.take.Take (core.slice.iter.Iter + Std.U8)) × Std.U64) Std.U64) + := do + let (o, iter1) ← + core.iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator.next + (core.iter.traits.iterator.IteratorSliceIter Std.U8) iter + match o with + | none => ok (done total) + | some item => + let i ← total <<< 8#i32 + let i1 ← lift (core.convert.num.FromU64U8.from item) + let total1 ← i + i1 + ok (cont (iter1, total1)) + +/-- [fips205::helpers::to_int]: loop 0: + Source: 'src/helpers.rs', lines 17:4-23:5 -/ +@[rust_loop] +def helpers.to_int_loop + (iter : core.iter.adapters.take.Take (core.slice.iter.Iter Std.U8)) + (total : Std.U64) : + Result Std.U64 + := do + loop + (fun (iter1, total1) => helpers.to_int_loop.body iter1 total1) + (iter, total) + +/-- [fips205::helpers::to_int]: + Source: 'src/helpers.rs', lines 9:0-27: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 ← core.slice.Slice.iter x + let i1 ← lift (UScalar.cast .Usize n) + let iter ← core.slice.iter.IteratorSliceIter.take i i1 + helpers.to_int_loop iter 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 44:4-53: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 44:4-53: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 35:0-57: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 83:8-95: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 83:8-95: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 80:4-104:5 -/ +@[rust_loop_body] +def helpers.base_2b_loop0.body + (x : Slice Std.U8) (b : Std.U32) (iter : core.slice.iter.IterMut Std.U32) + (back : core.slice.iter.IterMut Std.U32 → core.slice.iter.IterMut Std.U32) + (inn : Std.Usize) (bits : Std.U32) (total : Std.U32) : + Result (ControlFlow ((core.slice.iter.IterMut Std.U32) × + (core.slice.iter.IterMut Std.U32 → core.slice.iter.IterMut Std.U32) × + Std.Usize × Std.U32 × Std.U32) (core.slice.iter.IterMut Std.U32)) + := do + let (o, iter1, next_back) ← core.slice.iter.IteratorIterMut.next iter + match o with + | none => ok (done (let im := next_back iter1 none + back im)) + | some _ => + 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 item ← lift (i &&& i2) + ok (cont (iter1, fun im => let im1 := next_back im (some item) + back im1, inn1, bits2, total1)) + +/-- [fips205::helpers::base_2b]: loop 0: + Source: 'src/helpers.rs', lines 80:4-104:5 -/ +@[rust_loop] +def helpers.base_2b_loop0 + (iter : core.slice.iter.IterMut Std.U32) + (back : core.slice.iter.IterMut Std.U32 → core.slice.iter.IterMut Std.U32) + (x : Slice Std.U8) (b : Std.U32) (inn : Std.Usize) (bits : Std.U32) + (total : Std.U32) : + Result (core.slice.iter.IterMut Std.U32) + := do + loop + (fun (iter1, back1, inn1, bits1, total1) => helpers.base_2b_loop0.body x b + iter1 back1 inn1 bits1 total1) + (iter, back, inn, bits, total) + +/-- [fips205::helpers::base_2b]: + Source: 'src/helpers.rs', lines 65:0-107: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 (iter, iter_mut_back) ← core.slice.Slice.iter_mut baseb + let back ← + helpers.base_2b_loop0 iter (fun im => im) x b 0#usize 0#u32 0#u32 + ok (iter_mut_back back) + +/-- [fips205::helpers::{fips205::types::Adrs}::set_layer_address]: + Source: 'src/helpers.rs', lines 200:4-200: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 202:4-202: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 204:4-204: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 206:4-206: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 208:4-213: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 215:4-219: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 221:4-221: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 223:4-223: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 225:4-225: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 227:4-227: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}::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}::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}::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}::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}::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}] + 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}::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}::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}::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}::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}::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}::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 118:4-120:5 -/ +@[rust_loop_body] +def verify_mono.wots_pk_from_sig_free_loop0.body + (iter : core.iter.adapters.take.Take (core.slice.iter.Iter Std.U32)) + (csum : Std.U32) : + Result (ControlFlow ((core.iter.adapters.take.Take (core.slice.iter.Iter + Std.U32)) × Std.U32) Std.U32) + := do + let (o, iter1) ← + core.iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator.next + (core.iter.traits.iterator.IteratorSliceIter Std.U32) iter + match o with + | none => ok (done csum) + | some item => + let i ← W - 1#u32 + let i1 ← U32.Insts.CoreOpsArithSubShared0U32U32.sub i item + let csum1 ← csum + i1 + ok (cont (iter1, csum1)) + +/-- [fips205::verify_mono::wots_pk_from_sig_free]: loop 0: + Source: 'src/verify_mono.rs', lines 118:4-120:5 -/ +@[rust_loop] +def verify_mono.wots_pk_from_sig_free_loop0 + (iter : core.iter.adapters.take.Take (core.slice.iter.Iter Std.U32)) + (csum : Std.U32) : + Result Std.U32 + := do + loop + (fun (iter1, csum1) => verify_mono.wots_pk_from_sig_free_loop0.body iter1 + csum1) + (iter, csum) + +/-- [fips205::verify_mono::wots_pk_from_sig_free]: loop body 1: + Source: 'src/verify_mono.rs', lines 131:4-140: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 131:4-140: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-147: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 r ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from N + let n32 ← + core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug + r + 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 s2 ← lift (Array.to_slice msg1) + let i2 ← core.slice.Slice.iter s2 + let iter ← core.slice.iter.IteratorSliceIter.take i2 i1 + let csum ← verify_mono.wots_pk_from_sig_free_loop0 iter 0#u32 + let i3 ← LEN2 * LGW + let i4 ← lift (i3 &&& 7#u32) + let i5 ← 8#u32 - i4 + let i6 ← lift (i5 &&& 7#u32) + let csum1 ← csum <<< i6 + let i7 ← i3 + 7#u32 + let i8 ← i7 / 8#u32 + let a1 ← helpers.to_byte csum1 i8 + let s3 ← lift (Array.to_slice a1) + let (s4, index_mut_back1) ← + core.array.Array.index_mut (core.ops.index.IndexMutSlice + (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U32)) msg1 + { start := i1 } + let s5 ← helpers.base_2b s3 LGW LEN2 s4 + let msg2 := index_mut_back1 s5 + 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 i9 ← helpers.Adrs.get_key_pair_address adrs2 + let wotspk_adrs2 ← helpers.Adrs.set_key_pair_address wotspk_adrs1 i9 + 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 169:4-181: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 169:4-181: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 152:0-184: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 r ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from HP + let hp32 ← + core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug + r + 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 202:4-219:1 -/ +@[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) + (pk_root : Array Std.U8 N) (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)) Bool) + := do + let (o, iter1) ← + core.iter.range.IteratorRange.next U32.Insts.CoreIterRangeStep iter + match o with + | none => + let b ← + core.array.equality.PartialEqArray.eq core.cmp.PartialEqU8 node pk_root + ok (done b) + | some j => + let i ← 1#u64 <<< hp32 + let i1 ← i - 1#u64 + let i2 ← lift (idx_tree &&& i1) + let idx_leaf ← U32.Insts.CoreConvertTryFromU64TryFromIntError.try_from i2 + let b ← core.result.Result.is_err idx_leaf + if b + then ok (done false) + else + let idx_leaf1 ← + core.result.Result.unwrap + core.num.error.TryFromIntError.Insts.CoreFmtDebug idx_leaf + 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_leaf1 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 202:4-219:1 -/ +@[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) (pk_root : Array Std.U8 N) (idx_tree : Std.U64) + (hp32 : Std.U32) (adrs : types.Adrs) (node : Array Std.U8 N) : + Result Bool + := do + loop + (fun (iter1, idx_tree1, adrs1, node1) => + verify_mono.ht_verify_free_loop.body a pk_seed pk_root hp32 iter1 + idx_tree1 adrs1 node1) + (iter, idx_tree, adrs, node) + +/-- [fips205::verify_mono::ht_verify_free]: + Source: 'src/verify_mono.rs', lines 189:0-219: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 r ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from D + let d32 ← + core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug + r + let r1 ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from HP + let hp32 ← + core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug + r1 + 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 + verify_mono.ht_verify_free_loop { start := 1#u32, «end» := d32 } + sig_ht.xmss_sigs pk_seed pk_root idx_tree hp32 adrs1 node + +/-- [fips205::verify_mono::fors_pk_from_sig_free]: loop body 1: + Source: 'src/verify_mono.rs', lines 244:8-256: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 244:8-256: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 234:4-259: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 234:4-259: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 224:0-266: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 r ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from A + let a32 ← + core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug + r + let r1 ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from K + let k32 ← + core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug + r1 + 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 272:0-329: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 r ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from D + let d32 ← + core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug + r + let r1 ← U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from H + let h32 ← + core.result.Result.unwrap core.num.error.TryFromIntError.Insts.CoreFmtDebug + r1 + 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 ← + U32.Insts.CoreConvertTryFromU64TryFromIntError.try_from idx_leaf + let b ← core.result.Result.is_err idx_leaf_u32 + if b + then ok false + else + let idx_leaf_u321 ← + core.result.Result.unwrap + core.num.error.TryFromIntError.Insts.CoreFmtDebug idx_leaf_u32 + let adrs3 ← helpers.Adrs.set_key_pair_address adrs2 idx_leaf_u321 + 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_u321 + pk.pk_root + +/-- [fips205::verify_mono::slh_verify_128s]: + Source: 'src/verify_mono.rs', lines 338:0-342: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 diff --git a/verification/gen/SlhVerify/FunsExternal.lean b/verification/gen/SlhVerify/FunsExternal.lean new file mode 100644 index 0000000..ca65070 --- /dev/null +++ b/verification/gen/SlhVerify/FunsExternal.lean @@ -0,0 +1,200 @@ +/- ────────────────────────────────────────────────────────────────────────────── + gen/SlhVerify/FunsExternal.lean — hand-maintained external functions. + + TWO CLASSES of external, per honesty invariants H4/H5: + + (1) THE CRYPTOGRAPHIC BOUNDARY — the deliberate opaque axioms. + The five SLH-DSA-SHA2-128s hash primitives, reached by name from the + monomorphic verify path (verify_mono::oracle): + · verify_mono.oracle.f — F (chain / FORS leaf) + · verify_mono.oracle.h — H (Merkle node) + · verify_mono.oracle.t_l — T_len (WOTS+ pk compression) + · verify_mono.oracle.t_len — T_k (FORS root compression) + · verify_mono.oracle.h_msg — H_msg (message digest) + These are SHA-256-based; their correctness against FIPS 180-4 is the + standing hash-oracle boundary (see TRUSTED-BASE.md). The apex + certificate will carry EXACTLY these five beyond Lean's three kernel + axioms — nothing else. + + (2) TRANSPILER PLUMBING — core-library externals Aeneas emits for this + extraction config (u32::try_from, Result::is_err, the iterator Step / + Take machinery driving `for` ranges, the zeroize blanket impls, the + TryFromIntError Debug impl). These carry NO cryptographic content. + They are adopted here as axioms so the model type-checks at phase 1 + (no certificates exist yet, so H4's cone requirement is vacuous). The + proof phase will discharge each from Aeneas.Std / real definitions and + the #print axioms audit will then confirm only class (1) survives in + any certificate cone. Tracked as the phase-2 de-plumbing item. + ────────────────────────────────────────────────────────────────────────────── -/ +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. +import Aeneas +import SlhVerify.Types +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 +open fips205 + +/-- [core::convert::num::ptr_try_from_impls::{impl core::convert::TryFrom for u32}::try_from]: + Source: '/rustc/library/core/src/convert/num.rs', lines 300:12-300:64 + Name pattern: [core::convert::num::ptr_try_from_impls::{core::convert::TryFrom}::try_from] + Visibility: public -/ +@[rust_fun + "core::convert::num::ptr_try_from_impls::{core::convert::TryFrom}::try_from"] +axiom U32.Insts.CoreConvertTryFromUsizeTryFromIntError.try_from + : + Std.Usize → Result (core.result.Result Std.U32 + core.num.error.TryFromIntError) + +/-- [core::convert::num::{impl core::convert::TryFrom for u32}::try_from]: + Source: '/rustc/library/core/src/convert/num.rs', lines 300:12-300:64 + Name pattern: [core::convert::num::{core::convert::TryFrom}::try_from] + Visibility: public -/ +@[rust_fun + "core::convert::num::{core::convert::TryFrom}::try_from"] +axiom U32.Insts.CoreConvertTryFromU64TryFromIntError.try_from + : + Std.U64 → Result (core.result.Result Std.U32 + core.num.error.TryFromIntError) + +/-- [core::ops::arith::{impl core::ops::arith::Sub<&'_0 u32, u32> for u32}::sub]: + Source: '/rustc/library/core/src/internal_macros.rs', lines 38:12-38:68 + Name pattern: [core::ops::arith::{core::ops::arith::Sub}::sub] + Visibility: public -/ +@[rust_fun "core::ops::arith::{core::ops::arith::Sub}::sub"] +axiom U32.Insts.CoreOpsArithSubShared0U32U32.sub + : Std.U32 → Std.U32 → Result Std.U32 + +/-- [core::iter::adapters::take::{impl core::iter::traits::iterator::Iterator for core::iter::adapters::take::Take}::next]: + Source: '/rustc/library/core/src/iter/adapters/take.rs', lines 36:4-36:55 + Name pattern: [core::iter::adapters::take::{core::iter::traits::iterator::Iterator, @Clause0_Item>}::next] + Visibility: public -/ +@[rust_fun + "core::iter::adapters::take::{core::iter::traits::iterator::Iterator, @Clause0_Item>}::next"] +axiom core.iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator.next + {I : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst : + core.iter.traits.iterator.Iterator I Clause0_Item) : + core.iter.adapters.take.Take I → Result ((Option Clause0_Item) × + (core.iter.adapters.take.Take I)) + +/-- [core::iter::range::{impl core::iter::range::Step for u32}::backward_checked]: + Source: '/rustc/library/core/src/iter/range.rs', lines 290:16-290:74 + Name pattern: [core::iter::range::{core::iter::range::Step}::backward_checked] + Visibility: public -/ +@[rust_fun + "core::iter::range::{core::iter::range::Step}::backward_checked"] +axiom U32.Insts.CoreIterRangeStep.backward_checked + : Std.U32 → Std.Usize → Result (Option Std.U32) + +/-- [core::iter::range::{impl core::iter::range::Step for u32}::forward_checked]: + Source: '/rustc/library/core/src/iter/range.rs', lines 282:16-282:73 + Name pattern: [core::iter::range::{core::iter::range::Step}::forward_checked] + Visibility: public -/ +@[rust_fun + "core::iter::range::{core::iter::range::Step}::forward_checked"] +axiom U32.Insts.CoreIterRangeStep.forward_checked + : Std.U32 → Std.Usize → Result (Option Std.U32) + +/-- [core::iter::range::{impl core::iter::range::Step for u32}::steps_between]: + Source: '/rustc/library/core/src/iter/range.rs', lines 271:16-271:84 + Name pattern: [core::iter::range::{core::iter::range::Step}::steps_between] + Visibility: public -/ +@[rust_fun "core::iter::range::{core::iter::range::Step}::steps_between"] +axiom U32.Insts.CoreIterRangeStep.steps_between + : Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize)) + +/-- [core::iter::traits::iterator::Iterator::take]: + Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 1447:4-1449:20 + Name pattern: [core::iter::traits::iterator::Iterator::take] + Visibility: public -/ +@[rust_fun "core::iter::traits::iterator::Iterator::take"] +axiom core.iter.traits.iterator.Iterator.take.default + {Self : Type} {Clause0_Item : Type} (IteratorInst : + core.iter.traits.iterator.Iterator Self Clause0_Item) : + Self → Std.Usize → Result (core.iter.adapters.take.Take Self) + +/-- [core::num::error::{impl core::fmt::Debug for core::num::error::TryFromIntError}::fmt]: + Source: '/rustc/library/core/src/num/error.rs', lines 9:9-9:14 + Name pattern: [core::num::error::{core::fmt::Debug}::fmt] + Visibility: public -/ +@[rust_fun + "core::num::error::{core::fmt::Debug}::fmt"] +axiom core.num.error.TryFromIntError.Insts.CoreFmtDebug.fmt + : + core.num.error.TryFromIntError → core.fmt.Formatter → Result + ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter) + +/-- [core::result::{core::result::Result}::is_err]: + Source: '/rustc/library/core/src/result.rs', lines 646:4-646:38 + Name pattern: [core::result::{core::result::Result<@T, @E>}::is_err] + Visibility: public -/ +@[rust_fun "core::result::{core::result::Result<@T, @E>}::is_err"] +axiom core.result.Result.is_err + {T : Type} {E : Type} : core.result.Result T E → Result Bool + +/-- [zeroize::{impl zeroize::Zeroize for Z}::zeroize]: + Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 274:4-274:25 + Name pattern: [zeroize::{zeroize::Zeroize<@Z>}::zeroize] + Visibility: public -/ +@[rust_fun "zeroize::{zeroize::Zeroize<@Z>}::zeroize"] +axiom zeroize.Zeroize.Blanket.zeroize + {Z : Type} (DefaultIsZeroesInst : zeroize.DefaultIsZeroes Z) : Z → Result Z + +/-- [zeroize::{impl zeroize::Zeroize for [Z; N]}::zeroize]: + Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 346:4-346:25 + Name pattern: [zeroize::{zeroize::Zeroize<[@Z; @N]>}::zeroize] + Visibility: public -/ +@[rust_fun "zeroize::{zeroize::Zeroize<[@Z; @N]>}::zeroize"] +axiom Array.Insts.ZeroizeZeroize.zeroize + {Z : Type} {N : Std.Usize} (ZeroizeInst : zeroize.Zeroize Z) : + Array Z N → Result (Array Z N) + +/-- [zeroize::__internal::{impl zeroize::__internal::AssertZeroize for T}::zeroize_or_on_drop]: + Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 846:8-846:40 + Name pattern: [zeroize::__internal::{zeroize::__internal::AssertZeroize<@T>}::zeroize_or_on_drop] + Visibility: public -/ +@[rust_fun + "zeroize::__internal::{zeroize::__internal::AssertZeroize<@T>}::zeroize_or_on_drop"] +axiom zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop + {T : Type} (ZeroizeInst : zeroize.Zeroize T) : T → Result T + +/-- [fips205::verify_mono::oracle::f]: + Source: 'src/verify_mono.rs', lines 49:4-51:5 -/ +axiom verify_mono.oracle.f + (N : Std.Usize) : + Slice Std.U8 → types.Adrs → Slice Std.U8 → Result (Array Std.U8 N) + +/-- [fips205::verify_mono::oracle::h]: + Source: 'src/verify_mono.rs', lines 54:4-56:5 -/ +axiom verify_mono.oracle.h + (N : Std.Usize) : + Slice Std.U8 → types.Adrs → Slice Std.U8 → Slice Std.U8 → Result + (Array Std.U8 N) + +/-- [fips205::verify_mono::oracle::t_l]: + Source: 'src/verify_mono.rs', lines 60:4-64:5 -/ +axiom verify_mono.oracle.t_l + {X : Std.Usize} {N : Std.Usize} : + Slice Std.U8 → types.Adrs → Array (Array Std.U8 N) X → Result (Array + Std.U8 N) + +/-- [fips205::verify_mono::oracle::t_len]: + Source: 'src/verify_mono.rs', lines 69:4-73:5 -/ +axiom verify_mono.oracle.t_len + {X : Std.Usize} {N : Std.Usize} : + Slice Std.U8 → types.Adrs → Array (Array Std.U8 N) X → Result (Array + Std.U8 N) + +/-- [fips205::verify_mono::oracle::h_msg]: + Source: 'src/verify_mono.rs', lines 81:4-85:5 -/ +axiom verify_mono.oracle.h_msg + (M : Std.Usize) : + Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Result + (Array Std.U8 M) + diff --git a/verification/gen/SlhVerify/Types.lean b/verification/gen/SlhVerify/Types.lean new file mode 100644 index 0000000..62c72c6 --- /dev/null +++ b/verification/gen/SlhVerify/Types.lean @@ -0,0 +1,101 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [fips205]: type definitions +import Aeneas +import SlhVerify.TypesExternal +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 + +namespace fips205 + +/-- Trait declaration: [zeroize::Zeroize] + Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 245:0-245:17 + Name pattern: [zeroize::Zeroize] + Visibility: public -/ +@[rust_trait "zeroize::Zeroize"] +structure zeroize.Zeroize (Self : Type) where + zeroize : Self → Result Self + +/-- Trait declaration: [zeroize::DefaultIsZeroes] + Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 255:0-255:49 + Name pattern: [zeroize::DefaultIsZeroes] + Visibility: public -/ +@[rust_trait "zeroize::DefaultIsZeroes" + (parentClauses := ["coremarkerCopyInst", "coredefaultDefaultInst"])] +structure zeroize.DefaultIsZeroes (Self : Type) where + coremarkerCopyInst : core.marker.Copy Self + coredefaultDefaultInst : core.default.Default Self + +/-- [fips205::types::Adrs] + Source: 'src/types.rs', lines 116:0-132:1 -/ +structure types.Adrs where + f0 : Array Std.U8 4#usize + f1 : Array Std.U8 4#usize + f2 : Array Std.U8 4#usize + f3 : Array Std.U8 4#usize + f4 : Array Std.U8 4#usize + f5 : Array Std.U8 4#usize + f6 : Array Std.U8 4#usize + f7 : Array Std.U8 4#usize + +/-- [fips205::types::WotsSig] + Source: 'src/types.rs', lines 80:0-82:1 -/ +structure types.WotsSig (LEN : Std.Usize) (N : Std.Usize) where + data : Array (Array Std.U8 N) LEN + +/-- [fips205::types::XmssSig] + Source: 'src/types.rs', lines 91:0-94:1 -/ +structure types.XmssSig (HP : Std.Usize) (LEN : Std.Usize) (N : Std.Usize) + where + sig_wots : types.WotsSig LEN N + auth : Array (Array Std.U8 N) HP + +/-- [fips205::types::HtSig] + Source: 'src/types.rs', lines 73:0-75:1 -/ +structure types.HtSig (D : Std.Usize) (HP : Std.Usize) (LEN : Std.Usize) (N : + Std.Usize) where + xmss_sigs : Array (types.XmssSig HP LEN N) D + +/-- [fips205::types::Auth] + Source: 'src/types.rs', lines 66:0-68:1 -/ +structure types.Auth (A : Std.Usize) (N : Std.Usize) where + tree : Array (Array Std.U8 N) A + +/-- [fips205::types::ForsSig] + Source: 'src/types.rs', lines 53:0-56:1 -/ +structure types.ForsSig (A : Std.Usize) (K : Std.Usize) (N : Std.Usize) where + private_key_value : Array (Array Std.U8 N) K + auth : Array (types.Auth A N) K + +/-- [fips205::types::SlhDsaSig] + Source: 'src/types.rs', lines 19:0-30:1 -/ +structure types.SlhDsaSig (A : Std.Usize) (D : Std.Usize) (HP : Std.Usize) (K : + Std.Usize) (LEN : Std.Usize) (N : Std.Usize) where + randomness : Array Std.U8 N + fors_sig : types.ForsSig A K N + ht_sig : types.HtSig D HP LEN N + +/-- [fips205::types::SlhPublicKey] + Source: 'src/types.rs', lines 35:0-38:1 -/ +structure types.SlhPublicKey (N : Std.Usize) where + pk_seed : Array Std.U8 N + pk_root : Array Std.U8 N + +/-- [fips205::types::ForsPk] + Source: 'src/types.rs', lines 60:0-62:1 -/ +structure types.ForsPk (N : Std.Usize) where + key : Array Std.U8 N + +/-- [fips205::types::WotsPk] + Source: 'src/types.rs', lines 86:0-86:61 -/ +@[reducible] +def types.WotsPk (N : Std.Usize) := Array Std.U8 N + +end fips205 diff --git a/verification/gen/SlhVerify/TypesExternal.lean b/verification/gen/SlhVerify/TypesExternal.lean new file mode 100644 index 0000000..6829973 --- /dev/null +++ b/verification/gen/SlhVerify/TypesExternal.lean @@ -0,0 +1,23 @@ +/- gen/SlhVerify/TypesExternal.lean — hand-maintained external types. + The single external type is a core-library error type introduced by + u32::try_from; it carries no cryptographic content. -/ +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. +import Aeneas +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 + +/-- [core::num::error::TryFromIntError] + Source: '/rustc/library/core/src/num/error.rs', lines 10:0-10:26 + Name pattern: [core::num::error::TryFromIntError] + Visibility: public -/ +@[rust_type "core::num::error::TryFromIntError"] +axiom core.num.error.TryFromIntError : Type +