From 1e50295619d6198f16f87ced48cbeaee2f5179c3 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 28 Jul 2026 10:16:57 +0200 Subject: [PATCH] TypesExternal: correct a header that described a type the file no longer contains MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- verification/PROVENANCE.json | 2 +- verification/gen/SlhVerify/TypesExternal.lean | 15 ++++++++++++--- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/verification/PROVENANCE.json b/verification/PROVENANCE.json index 12ed48d..dfde3ea 100644 --- a/verification/PROVENANCE.json +++ b/verification/PROVENANCE.json @@ -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" diff --git a/verification/gen/SlhVerify/TypesExternal.lean b/verification/gen/SlhVerify/TypesExternal.lean index 585cab4..5c25dbd 100644 --- a/verification/gen/SlhVerify/TypesExternal.lean +++ b/verification/gen/SlhVerify/TypesExternal.lean @@ -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