diff --git a/ref/go/cmd/genkat/main.go b/ref/go/cmd/genkat/main.go index dd79653..1ada21c 100644 --- a/ref/go/cmd/genkat/main.go +++ b/ref/go/cmd/genkat/main.go @@ -257,7 +257,9 @@ func main() { r1s[i] = r1 r2s[i] = r2 } - sig, evidences, err := pm.Combine(pm.ThbsSeCombineInput{ + // genkat is a research/KAT-vector tool; the seed-reconstructing + // combiner requires the explicit runtime acknowledgement. + sig, evidences, err := pm.Combine(pm.AckThbsSeReconstructsSeed, pm.ThbsSeCombineInput{ Key: key, Binding: binding, Message: msg, diff --git a/ref/go/pkg/magnetar/kat_test.go b/ref/go/pkg/magnetar/kat_test.go index 931edeb..f511402 100644 --- a/ref/go/pkg/magnetar/kat_test.go +++ b/ref/go/pkg/magnetar/kat_test.go @@ -314,7 +314,7 @@ func TestKAT_ThbsSe(t *testing.T) { r2s[i] = r2 } - sig, evidences, err := Combine(ThbsSeCombineInput{ + sig, evidences, err := Combine(AckThbsSeReconstructsSeed, ThbsSeCombineInput{ Key: key, Binding: binding, Message: msg, diff --git a/ref/go/pkg/magnetar/pvss_dkg_test.go b/ref/go/pkg/magnetar/pvss_dkg_test.go index 6daf3ef..36a31f1 100644 --- a/ref/go/pkg/magnetar/pvss_dkg_test.go +++ b/ref/go/pkg/magnetar/pvss_dkg_test.go @@ -802,7 +802,7 @@ func TestPVSS_DKG_EndToEnd_SignAndVerify(t *testing.T) { r2s = append(r2s, r2) } - sig, _, err := Combine(ThbsSeCombineInput{ + sig, _, err := Combine(AckThbsSeReconstructsSeed, ThbsSeCombineInput{ Key: key, Binding: binding, Message: msg, diff --git a/ref/go/pkg/magnetar/thbsse.go b/ref/go/pkg/magnetar/thbsse.go index 111c53a..3f5e0ae 100644 --- a/ref/go/pkg/magnetar/thbsse.go +++ b/ref/go/pkg/magnetar/thbsse.go @@ -799,6 +799,26 @@ type ThbsSeCombineInput struct { Round2 []ThbsSeRound2Msg } +// ThbsSeReconstructAck is the explicit hazard acknowledgement required by +// Combine. The THBS-SE combine path reconstructs the FIPS 205 master seed at +// the public combiner — it is RESEARCH-ONLY; production finality uses the +// standalone per-validator leg aggregated via STARK-QC (no seed ever formed). +// This is a RUNTIME barrier (no build tags — one native binary), greppable in +// review (grep for IUnderstandThisReconstructsTheSeed). +type ThbsSeReconstructAck struct{ ack string } + +// AckThbsSeReconstructsSeed is the only value Combine accepts; its single +// field documents the hazard at the call site. +var AckThbsSeReconstructsSeed = ThbsSeReconstructAck{ack: "IUnderstandThisReconstructsTheSeed"} + +// ErrThbsSeResearchOnly is returned when Combine is invoked without the +// explicit AckThbsSeReconstructsSeed acknowledgement. +var ErrThbsSeResearchOnly = errors.New( + "magnetar/thbsse: seed-reconstructing Combine is RESEARCH-ONLY (it " + + "reconstructs the FIPS 205 master seed at the combiner); pass " + + "AckThbsSeReconstructsSeed to confirm, or use the standalone " + + "per-validator leg aggregated via STARK-QC for production") + // Combine is the PUBLIC combiner. It is a pure function of its // inputs — anyone with the public ThbsSeKey, the slot binding, the // message, and >= t valid Round-1/Round-2 pairs can produce the @@ -838,7 +858,13 @@ type ThbsSeCombineInput struct { // return. The returned Signature is the FIPS 205 wire-format // bytes; it verifies under unmodified slhdsa.Verify against // (key.PublicKey, msg, ctx=ctxFromSlot(binding)). -func Combine(input ThbsSeCombineInput) (*Signature, []ThbsSeShareEvidence, error) { +func Combine(ack ThbsSeReconstructAck, input ThbsSeCombineInput) (*Signature, []ThbsSeShareEvidence, error) { + // Runtime research-only barrier (mirrors OpenRevealAck; NO build tags — + // one native binary). The THBS-SE combiner reconstructs the FIPS 205 + // master seed; refuse unless the caller explicitly acknowledges it. + if ack != AckThbsSeReconstructsSeed { + return nil, nil, ErrThbsSeResearchOnly + } if input.Key == nil { return nil, nil, errors.New("magnetar/thbsse: nil key") } diff --git a/ref/go/pkg/magnetar/thbsse_assemble.go b/ref/go/pkg/magnetar/thbsse_assemble.go index 6221122..8710526 100644 --- a/ref/go/pkg/magnetar/thbsse_assemble.go +++ b/ref/go/pkg/magnetar/thbsse_assemble.go @@ -3,7 +3,18 @@ package magnetar -// thbsse_assemble.go — THBS-SE Combine emit path. +// thbsse_assemble.go — THBS-SE Combine emit path (RESEARCH-ONLY at RUNTIME). +// +// This path reconstructs the FIPS 205 master seed at the combiner; it is +// gated at RUNTIME by the `AckThbsSeReconstructsSeed` acknowledgement in +// Combine (no build tags — one native binary). Without the ack, Combine +// refuses with ErrThbsSeResearchOnly. It is +// the seed-reconstructing emit path: it Lagrange-RECONSTRUCTS the full FIPS +// 205 master into the combiner's process memory for one Sign call. That is +// research-grade, not no-leak, so the "research-only" status is ENFORCED by +// the build constraint above — not by prose. The production counterpart is +// thbsse_assemble_production.go, whose assembleSignatureBytes refuses with +// ErrThbsSeResearchOnly and never reconstructs the master. // // ===================================================================== // HONEST SUMMARY: THIS PATH RECONSTRUCTS THE FIPS 205 MASTER diff --git a/ref/go/pkg/magnetar/thbsse_assemble_test.go b/ref/go/pkg/magnetar/thbsse_assemble_test.go index 5fcbb91..ebefca0 100644 --- a/ref/go/pkg/magnetar/thbsse_assemble_test.go +++ b/ref/go/pkg/magnetar/thbsse_assemble_test.go @@ -344,7 +344,7 @@ func TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl(t *testing.T) { Round1: r1s, Round2: r2s, } - sig, evidences, err := Combine(input) + sig, evidences, err := Combine(AckThbsSeReconstructsSeed, input) if err != nil { t.Fatalf("Combine: %v", err) } @@ -401,7 +401,7 @@ func TestThbsSE_StrictAtom_Combine_DerivedPkSeedCrossCheck(t *testing.T) { Round1: r1s, Round2: r2s, } - _, _, err = Combine(input) + _, _, err = Combine(AckThbsSeReconstructsSeed, input) if err == nil { t.Fatalf("Combine accepted a tampered pkSeed in the PublicKey") } @@ -537,7 +537,7 @@ func benchStrictAtomSignMode(b *testing.B, mode Mode, n, t int) { r1s = append(r1s, r1) r2s = append(r2s, r2) } - sig, _, err := Combine(ThbsSeCombineInput{ + sig, _, err := Combine(AckThbsSeReconstructsSeed, ThbsSeCombineInput{ Key: key, Binding: binding, Message: msg, diff --git a/ref/go/pkg/magnetar/thbsse_test.go b/ref/go/pkg/magnetar/thbsse_test.go index 29d780e..3f9bc7d 100644 --- a/ref/go/pkg/magnetar/thbsse_test.go +++ b/ref/go/pkg/magnetar/thbsse_test.go @@ -120,7 +120,7 @@ func TestThbsSE_Wire_FIPS205Verifiable(t *testing.T) { Round1: r1s, Round2: r2s, } - sig, evidences, err := Combine(input) + sig, evidences, err := Combine(AckThbsSeReconstructsSeed, input) if err != nil { t.Fatalf("Combine: %v", err) } @@ -227,7 +227,7 @@ func TestThbsSE_RejectSeedReveal(t *testing.T) { Round1: r1s, Round2: r2s, } - sig, evidences, err := Combine(input) + sig, evidences, err := Combine(AckThbsSeReconstructsSeed, input) if err == nil { // 2 of 3 shares are honest — Combine succeeded because we // over-provisioned. Check that exactly one evidence was emitted @@ -293,7 +293,7 @@ func TestThbsSE_RejectOversizedShareWireSize(t *testing.T) { Round1: r1s, Round2: r2s, } - sig, evidences, err := Combine(input) + sig, evidences, err := Combine(AckThbsSeReconstructsSeed, input) if err == nil { t.Fatalf("Combine accepted a tampered (extra-bytes) share, sig=%v evidences=%+v", sig, evidences) } @@ -351,7 +351,7 @@ func TestThbsSE_RejectTamperedShareCommitMismatch(t *testing.T) { Round1: r1s, Round2: r2s, } - sig, evidences, err := Combine(input) + sig, evidences, err := Combine(AckThbsSeReconstructsSeed, input) if err == nil { t.Fatalf("Combine accepted a tampered WOTS reveal, sig=%v evidences=%+v", sig, evidences) } @@ -465,7 +465,7 @@ func TestThbsSE_OverselectedCommittee(t *testing.T) { Round1: r1s, Round2: r2s, } - sig, evidences, err := Combine(input) + sig, evidences, err := Combine(AckThbsSeReconstructsSeed, input) if err != nil { t.Fatalf("Combine with 4 honest of 7 (t=3): %v", err) } @@ -516,11 +516,11 @@ func TestThbsSE_PublicCombiner_Determinism(t *testing.T) { Round1: []ThbsSeRound1Msg{r1s[1], r1s[3], r1s[5]}, Round2: []ThbsSeRound2Msg{r2s[1], r2s[3], r2s[5]}, } - sigA, _, err := Combine(subA) + sigA, _, err := Combine(AckThbsSeReconstructsSeed, subA) if err != nil { t.Fatalf("Combine A: %v", err) } - sigB, _, err := Combine(subB) + sigB, _, err := Combine(AckThbsSeReconstructsSeed, subB) if err != nil { t.Fatalf("Combine B: %v", err) } @@ -556,11 +556,11 @@ func TestThbsSE_SlotBindingDomainSeparation(t *testing.T) { r1sA, r2sA := runRound1Across(t, params, key, bindingA, msg, []int{0, 1, 2}) r1sB, r2sB := runRound1Across(t, params, key, bindingB, msg, []int{0, 1, 2}) - sigA, _, err := Combine(ThbsSeCombineInput{Key: key, Binding: bindingA, Message: msg, Round1: r1sA, Round2: r2sA}) + sigA, _, err := Combine(AckThbsSeReconstructsSeed, ThbsSeCombineInput{Key: key, Binding: bindingA, Message: msg, Round1: r1sA, Round2: r2sA}) if err != nil { t.Fatalf("Combine A: %v", err) } - sigB, _, err := Combine(ThbsSeCombineInput{Key: key, Binding: bindingB, Message: msg, Round1: r1sB, Round2: r2sB}) + sigB, _, err := Combine(AckThbsSeReconstructsSeed, ThbsSeCombineInput{Key: key, Binding: bindingB, Message: msg, Round1: r1sB, Round2: r2sB}) if err != nil { t.Fatalf("Combine B: %v", err) } @@ -635,7 +635,7 @@ func benchThbsSeSignMode(b *testing.B, mode Mode, n, t int) { r1s = append(r1s, r1) r2s = append(r2s, r2) } - sig, _, err := Combine(ThbsSeCombineInput{ + sig, _, err := Combine(AckThbsSeReconstructsSeed, ThbsSeCombineInput{ Key: key, Binding: binding, Message: msg, @@ -662,3 +662,21 @@ func makeThbsSeBindingBench(slot uint64) *ThbsSeSlotBinding { MessageDomain: []byte("polaris-cert"), } } + +// TestThbsSE_Combine_ResearchOnlyRuntimeBarrier pins the RUNTIME research-only +// gate on the seed-reconstructing combiner — NO build tags, one native binary. +// Without the explicit AckThbsSeReconstructsSeed acknowledgement, Combine +// refuses immediately (before any reconstruction); with it, the barrier is +// passed (and the call then fails only on the empty input). +func TestThbsSE_Combine_ResearchOnlyRuntimeBarrier(t *testing.T) { + // Zero-value ack (the only ack an outside caller can forge — the field is + // unexported) is refused. + if _, _, err := Combine(ThbsSeReconstructAck{}, ThbsSeCombineInput{}); !errors.Is(err, ErrThbsSeResearchOnly) { + t.Fatalf("Combine without ack: got %v, want ErrThbsSeResearchOnly", err) + } + // With the ack the runtime barrier is passed: the error is the nil-key + // validation, NOT the research refusal — proving the ack let it through. + if _, _, err := Combine(AckThbsSeReconstructsSeed, ThbsSeCombineInput{}); err == nil || errors.Is(err, ErrThbsSeResearchOnly) { + t.Fatalf("Combine with ack should pass the barrier and fail on empty input, got %v", err) + } +} diff --git a/scripts/checks/easycrypt-smoke.sh b/scripts/checks/easycrypt-smoke.sh index 21fd233..d4ea818 100755 --- a/scripts/checks/easycrypt-smoke.sh +++ b/scripts/checks/easycrypt-smoke.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash # easycrypt-smoke.sh --- per-push EasyCrypt theory smoke check. # -# Verifies the v1.1 EasyCrypt theory shells exist + parse-cleanly at -# the require/import level. The FULL EC re-run is a release-time gate -# (1+ hour); the per-push smoke check ensures the theory files are -# present and structurally well-formed. +# Verifies the EasyCrypt scaffold files exist + are well-formed. Per +# proofs/easycrypt/README.md the Magnetar EC track is HONESTLY two +# 0-content scaffolds; this smoke ensures they are present and carry the +# scaffold banner. The FULL EC re-run is a release-time gate (1+ hour). # # If EasyCrypt (`easycrypt`) is installed on the runner, the script # runs the EC `check` command on each file. If not installed, the @@ -22,14 +22,17 @@ if [[ ! -d "$EC_DIR" ]]; then exit 2 fi -# Expected theory files at v1.1. +# Expected theory files. Per proofs/easycrypt/README.md the Magnetar EC +# track is HONESTLY two 0-content scaffolds — the earlier non-empty track +# (Magnetar_N1_SHAKE_Expand.ec, Magnetar_N1_Atom_Refinement.ec, +# Magnetar_N4_KeyDeriveStable.ec, lemmas/SLHDSA_Functional.ec, +# lemmas/Magnetar_CT.ec) was DELETED because its theorems were vacuous +# (X=X rewrites, admit-discharged CT, an axiom restating the headline). +# This list tracks what actually exists; it must not resurrect the +# deleted shells. EXPECTED=( "Magnetar_N1_StrictAtom.ec" - "Magnetar_N1_SHAKE_Expand.ec" - "Magnetar_N1_Atom_Refinement.ec" - "Magnetar_N4_KeyDeriveStable.ec" - "lemmas/SLHDSA_Functional.ec" - "lemmas/Magnetar_CT.ec" + "Magnetar_N5_PVSS_DKG.ec" ) for f in "${EXPECTED[@]}"; do @@ -38,18 +41,16 @@ for f in "${EXPECTED[@]}"; do exit 2 fi done -echo " [ok] all v1.1 theory files present" +echo " [ok] all expected theory files present" -# Per-file structural check: every file must have at least one -# `require import` line and at least one `(* ... *)` comment block -# (the file-header status banner). +# Per-file structural check. These are deliberately 0-content scaffolds +# (no axiom/admit/lemma/theorem, no `require import` — see README.md), so +# the only structural marker we assert is the file-header banner comment +# that identifies a real EC scaffold rather than an empty placeholder. for f in "${EXPECTED[@]}"; do - if ! grep -q "^require import" "$EC_DIR/$f"; then - echo " [fail] $f missing 'require import' line" - exit 2 - fi if ! grep -q "(\* --" "$EC_DIR/$f"; then - echo " [warn] $f missing standard banner comment (low-severity)" + echo " [fail] $f missing standard banner comment (not a valid scaffold)" + exit 2 fi done echo " [ok] structural checks pass"