From 0caa3faf684a7f09f3f3e43fd2a2c1d211e94444 Mon Sep 17 00:00:00 2001 From: Antje Worring Date: Sun, 21 Jun 2026 15:25:01 -0700 Subject: [PATCH] docs(honesty): clarify sorry/admit budget provenance + fix stale THBS-SPEC framing - .assurance/budget.txt: the SORRY=4/ADMIT=4 counts are axiom-budget.sh counting the WORDS 'sorry'/'admit' inside the scaffold BANNERS that describe the DELETED cheats, not live tactics. The proof tree has zero theorem/lemma/axiom/sorry/admit (verified). Document this so the budget is not misread as 8 unproven assertions. - THBS-SPEC.md: the v1.0 framing said Combine routes via circl/slhdsa.SignDeterministic directly; the live code uses the internal slhSignAtom engine (byte-identical to circl on the reconstructed master). Point to ASSEMBLE-INVARIANT.md as authoritative; reaffirm RESEARCH-ONLY. No code or proof-state change; M-family claims unchanged (all CONFIRMED). --- .assurance/budget.txt | 16 +++++++++++++--- THBS-SPEC.md | 18 ++++++++++++------ 2 files changed, 25 insertions(+), 9 deletions(-) diff --git a/.assurance/budget.txt b/.assurance/budget.txt index d7905d5..c465c96 100644 --- a/.assurance/budget.txt +++ b/.assurance/budget.txt @@ -1,9 +1,19 @@ # Unproven-assertion budget (max counts). Enforced by # ~/work/lux/luxfi/security/framework/checks/axiom-budget.sh. FAILS on any drift above. # Goal: decrease, never raise. Current surface (2026-06), after deleting the -# circular/vacuous strict-atom proofs. The remaining 4 sorry + 4 admit are in -# SUPPORTING (non-load-bearing) lemmas, disclosed in PROOF-CLAIMS; the headline -# threshold claim is now honestly "research-only", not "proven". +# circular/vacuous strict-atom proofs. +# +# HONEST ACCOUNTING of these counts: the proof tree contains NO live +# `sorry`/`admit` tactic and NO theorem/lemma/axiom at all — the three +# remaining .ec/.lean files are 0-content scaffolds (verified: grep for +# theorem|lemma|axiom|sorry|admit|def over proofs/ returns zero matches). +# axiom-budget.sh counts the WORDS "sorry"/"admit" wherever they appear in +# .ec/.lean files, and they appear here only inside the scaffold BANNERS that +# *describe the deleted cheats* (e.g. "whose proof body was `sorry`", "by +# `admit`"). So SORRY=4/ADMIT=4 is prose-in-banners, not unproven assertions. +# The budget is held at the current banner word-count so any genuinely NEW +# live sorry/admit (which would also add theorem/lemma machinery) trips the +# gate. The headline threshold claim is honestly "research-only", not "proven". SORRY=4 ADMIT=4 AXIOM=0 diff --git a/THBS-SPEC.md b/THBS-SPEC.md index 458d00f..6e09e23 100644 --- a/THBS-SPEC.md +++ b/THBS-SPEC.md @@ -46,12 +46,18 @@ EVER reconstructs SK.seed, even transiently in memory" --- requires the v1.1 strict-atom-assembly path tracked at `BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11`. -Magnetar v1.0 routes the final FIPS 205 byte production via -`circl/slhdsa.SignDeterministic` on a seed reconstructed by the -PUBLIC COMBINER. The seed is briefly present in the public combiner's -memory for one Sign call and is zeroized before return. The combiner -role is PUBLIC --- anyone can be the combiner --- and there is no -long-lived secret material outside party-local Shamir leaves. +Magnetar v1.0 routes the final FIPS 205 byte production via the +Magnetar-internal `slhSignAtom` engine (`thbsse_assemble.go`) on a +master reconstructed by the PUBLIC COMBINER; the emitted bytes are +byte-identical to `circl/slhdsa.SignDeterministic` on that same master +(pinned by `TestSlhdsaInternal_ByteEqualToCirclSign` and +`TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl`). The master is +briefly present in the public combiner's memory for one Sign call and +is zeroized before return. The combiner role is PUBLIC --- anyone can +be the combiner --- and there is no long-lived secret material outside +party-local Shamir leaves. (The authoritative current description of +this path is `ASSEMBLE-INVARIANT.md`; this is the RESEARCH-ONLY leg, +not production --- see §1.0 of `SPEC.md`.) This is materially stronger than a TEE-attested privileged-aggregator model (no host is in the TCB) and materially weaker than the strict