crypto/aggregated ThresholdSignature.Verify ignored its message argument and
returned true for any non-empty []byte — a method named Verify that verifies
nothing. Zero importers workspace-wide, so it was never reachable; removing it
before it ever could be. Real threshold verification lives in luxfi/threshold.
Verified: CGO_ENABLED=0 go build ./... clean, no remaining references.
Fixed message-type inconsistencies in the model; '^^' is now boolean-xor
(use '^' = RField.exp via Real); import RealOrder; stricter apply/rewrite.
Reproved mlkem_correctness and IND-CCA2 advantage bound.
Verified: all check under easycrypt (z3 + alt-ergo), 0 admits. Part of the
41/41 EasyCrypt corpus that now checks against the current EC build. Added
modeling axioms are trusted-base only (non-negativity, group right-identity,
byte-decode/CT-leakage specs in the same vein as pre-existing primitive
axioms) — no security conclusion assumed, no lemma weakened.
Co-authored-by: Hanzo Dev <dev@hanzo.ai>
Aligns hqc/slhdsa comments + dudect timing test docs with the canonical
PQ signature family naming:
Pulsar (M-LWE threshold ML-DSA)
Corona (R-LWE / Corona wrapper)
Magnetar (SLH-DSA threshold via GF(257) Shamir)
Old name 'Comet' was the working title for Magnetar during early
development; this commit completes the rename in:
- hqc/hqc.go (family-disjoint gap comment)
- slhdsa/gpu.go (FIPS 205 GPU dispatch header)
- slhdsa/gpu_test.go (test descriptions)
Also includes:
- mlkem/ct/dudect/{decaps,encaps,keygen}_ct.go + .c — timing analysis
harness improvements (decaps is the most CT-critical ML-KEM routine)
- mlkem/ct/dudect/run-m1-overnight.sh — operator runbook for Apple M1
overnight timing analysis
- .gitignore — build artifacts (dudect/, *.dylib, *.so, results/)
zeekay