mirror of
https://github.com/saymrwulf/fips205-slhdsa-verified.git
synced 2026-09-03 19:53:49 +00:00
mrwulf
7ebf9495d3
Round-8 estate review (GPT-5.6): this repository shipped a
FunsExternal_Template.lean / FunsExternal.lean pair and NO correspondence
check at all. This commit explains why, and fixes the cause rather than
bolting a check onto a missing input.
THE TEMPLATE WAS BEING DELETED. check.sh removed `*_Template.lean` on every
run and .gitignore excluded it. The stated reason was sound — "the verdict must
depend on COMMITTED BYTES, never on untracked build state", and an untracked
file on LEAN_PATH is exactly that problem. But it is the weaker of the two
available remedies. The ed25519 forks face the identical choice and COMMIT AND
PIN their templates, which removes the untracked state just as completely and
keeps the evidence.
The evidence is the point. The template is Aeneas's own statement of what the
extracted Rust needs from outside, and it is the ONLY artifact against which
"does the hand-written model ANSWER the extraction?" can be asked. Deleting it
made that question unaskable here — which is precisely why no check existed.
· template committed and pinned in model_integrity_sha256
· .gitignore no longer excludes it
· check.sh no longer deletes it, and says why at length
· Phase 0d runs model-correspondence.py — the forks' scanner, including both
round-8 corrections: a named Lean `section` does not qualify declaration
names, and an EXTRA AXIOM in the model (an assumption no template asks for)
fails rather than passing as a silent row
· MODEL-CORRESPONDENCE.txt committed, pinned, and compared byte-for-byte
Result: 11 externals, every one answered by the pinned model, no UNRESOLVED and
no EXTRA-AXIOM. Negative-tested — deleting one `axiom` from the model yields
`verify_mono.oracle.h_msg|UNRESOLVED` and a non-zero exit; restoring it returns
to green.
AND A REPRODUCIBILITY RESULT, obtained while recovering the deleted template.
charon is not available on this machine (the same wall the reviewer hit), but
SlhVerify.llbc IS committed and Aeneas is installed, so extraction step [2/2]
was re-run alone from the committed LLBC:
Types.lean: IDENTICAL Funs.lean: IDENTICAL
The LLBC -> Lean half of the extraction reproduces byte-for-byte from committed
inputs, on demand, by anyone with Aeneas and this repository. This does NOT
close `slh-extraction-unreproduced`: the Rust -> LLBC half still requires
charon, and this was still run by the author. Half the chain, verifiable today.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
103 lines
4.5 KiB
Text
103 lines
4.5 KiB
Text
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
|
||
-- [fips205]: external functions.
|
||
-- 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::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<u32>}::backward_checked]
|
||
Visibility: public -/
|
||
@[rust_fun
|
||
"core::iter::range::{core::iter::range::Step<u32>}::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<u32>}::forward_checked]
|
||
Visibility: public -/
|
||
@[rust_fun
|
||
"core::iter::range::{core::iter::range::Step<u32>}::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<u32>}::steps_between]
|
||
Visibility: public -/
|
||
@[rust_fun "core::iter::range::{core::iter::range::Step<u32>}::steps_between"]
|
||
axiom U32.Insts.CoreIterRangeStep.steps_between
|
||
: Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize))
|
||
|
||
/-- [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)
|
||
|