saymrwulf/fips205-slhdsa-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/fips205-slhdsa-verified.git synced 2026-09-04 20:03:44 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

TypesExternal: correct a header that described a type the file no longer contains

Browse source 
Round-6 NEW-12: the header claimed 'the single external type is a core-library
error type introduced by u32::try_from', but de-plumbing deleted that
declaration and the file defines nothing at all; the Aeneas 'rename this
template and fill the holes' boilerplate had also never been removed. Both
corrected. Comment-only, so the audit digest is unchanged (d83e297a…); the
Phase-0 model pin rotates 37958beb -> 2988c04c.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-28 10:16:57 +02:00
parent 476f669f5c
commit 1e50295619
2 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
verification/PROVENANCE.json
View file

@ -39,7 +39,7 @@
"byte_identical_regeneration_verified": "2026-07-28 (re-verified after the test/vector commit: all four pinned model files unchanged)",
"model_integrity_sha256": {
"_comment": "All four Lean model files check.sh Phase 0 pins before compiling anything \u2014 the two aeneas-generated files AND the two hand-maintained *External files (which carry the five oracle axioms and the Step defs). A hand-edit of the model fails the build here (round-4 reviewer F3).",
"gen/SlhVerify/TypesExternal.lean": "37958beb7c90b649497a20b0802f98f0fb2d975c245eca956d7396af74d7759f",
"gen/SlhVerify/TypesExternal.lean": "2988c04c5fc8c634aff4d9bd13604b8a47e677daa1f45e8f4f321368606cdd0a",
"gen/SlhVerify/FunsExternal.lean": "5efe551c35969c9da28b2f3eaed4a6a67c410c62a1926aab390e3abf010390f8",
"gen/SlhVerify/Types.lean": "db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384",
"gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f"

15
verification/gen/SlhVerify/TypesExternal.lean
View file

@ -1,7 +1,16 @@
/- 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.
THIS FILE DECLARES NO TYPES, deliberately. It once carried a core-library
error type introduced by `u32::try_from`; the de-plumbing patches removed
that idiom from the verify path at source level, so the declaration was
deleted under the dead-stub rule and only the module shell remains (Aeneas's
split-file layout still expects the module to exist).
An earlier header claimed the error type was still here, and the Aeneas
"rename this template and fill the holes" boilerplate had never been removed;
external review (round-6 NEW-12) flagged both. Corrected 2026-07-28. The file
is hand-maintained (Aeneas does not regenerate it) and its bytes are
sha256-pinned by check.sh Phase 0. -/
import Aeneas
open Aeneas Aeneas.Std Result ControlFlow Error
set_option linter.dupNamespace false