From bc8ea7857099ca48a8b72f9b81ace0d1571134c0 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Wed, 22 Jul 2026 23:03:33 +0200 Subject: [PATCH] audit catch 3: state the per-layer allowed axiom set precisely MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 'What will be claimed' promised cones of exactly the three kernel axioms — right for ed25519 field/scalar layers, wrong here: the hash oracles permeate every SLH-DSA layer (chain already calls F). The honest contract, now stated: each certificate cone = the three kernel axioms + at most the five named oracles, nothing else; plumbing axioms must be discharged before any certificate ships, audit-enforced. Co-Authored-By: Claude Fable 5 --- README.md | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index aa80f4f..b503411 100644 --- a/README.md +++ b/README.md @@ -92,12 +92,21 @@ this repository was created: ## What will be claimed (when the button is green, not before) One theorem per layer, each a statement about the **extracted** functions -(H3), compiled by `verification/check.sh` with `#print axioms` reporting -exactly `[propext, Classical.choice, Quot.sound]` (H1): chain semantics, -WOTS+ pk recomputation, XMSS path recomputation, hypertree acceptance, -FORS pk recomputation, and the apex — `slh_verify_internal` accepts iff -the recomputed hypertree root equals the pinned public-key root, under -the stated oracle boundary. +(H3), compiled by `verification/check.sh` with a per-certificate +`#print axioms` audit (H1): chain semantics, WOTS+ pk recomputation, +XMSS path recomputation, hypertree acceptance, FORS pk recomputation, +and the apex — `slh_verify_internal` accepts iff the recomputed +hypertree root equals the pinned public-key root. + +**The allowed axiom set, stated precisely:** unlike the ed25519 field and +scalar layers (whose cones are exactly `[propext, Classical.choice, +Quot.sound]`), the hash oracles permeate *every* SLH-DSA layer — `chain` +already calls `F`. So each certificate's cone may contain the three +kernel axioms **plus at most the five named oracles** +(`verify_mono.oracle.{h_msg, f, h, t_l, t_len}`) — and nothing else: the +transpiler-plumbing axioms currently in `FunsExternal.lean` must be +discharged before any certificate ships, and the audit fails the button +if any of them (or anything unlisted) appears in a cone. ## Discipline