fix(thbsse): gate the seed-reconstructing Combine at RUNTIME (AckThbsSeReconstructsSeed, mirrors OpenRevealAck) — NO build tags, one native binary; refuses without the ack. + runtime-barrier test; fix easycrypt-smoke dangling theory refs

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,

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,

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,

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")
 	}

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

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,

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)
+	}
+}

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"