mirror of
https://github.com/luxfi/corona.git
synced 2026-09-24 00:25:54 +00:00
zeekay
90e96df805
- proofs/easycrypt/: 13 EC files mirroring Pulsar layout, admit budget 0/0 statically pinned by scripts/checks/ec-admits.sh
- proofs/lean-easycrypt-bridge.md: 5-axiom Lean ↔ EC bridge (lagrange_inverse_eval, threshold_partial_response_identity, reconstruct_linear, shamir_correct, add_share_zeroR)
- jasmin/{lib,rlwe,threshold}/: round1/round2/combine .jazz with #ct annotations
- ct/dudect/: Verify + Combine harness (arm64 + x86_64 build tags)
- scripts/check-high-assurance.sh + scripts/checks/{ec-admits,ec-regressions,ec-refinement-scaffold,ec-compile,jasmin,extraction}.sh + check-lean-bridge.sh
- AXIOM-INVENTORY: residual axioms enumerated with closure pathways
- CRYPTOGRAPHER-SIGN-OFF: APPROVED WITH ROADMAP GATES; GATE-1+2+3a CLOSED; GATE-3b (dudect 10⁹ pinned CPU) + GATE-4 (external audit) + GATE-5 (Jasmin extraction filling out byte-walk) roadmap v0.8.0
Tier label: Tier A full closure scaffold landed; matches Pulsar v1.0.7 posture (admit 0/0 + Lean bridges + Jasmin + dudect harness wired). The submission-grade dudect run + external audit are v0.8.0 audit-track items.
3.0 KiB
3.0 KiB
Corona dudect constant-time harness
Statistical CT validation for Corona's threshold path, mirroring ~/work/lux/pulsar/ct/dudect/.
What's here
| File | Purpose |
|---|---|
verify_ct.go |
cgo bridge: corona threshold.Verify |
combine_ct.go |
cgo bridge: corona threshold Signer.Finalize (Combine) |
dudect_verify.c |
dudect main loop driving Verify |
dudect_combine.c |
dudect main loop driving Combine |
dudect_compat.h |
AArch64 compat shim for x86 intrinsics |
Makefile |
build verify + combine binaries |
fetch.sh |
clone upstream dudect at the pinned commit |
Build + run
./fetch.sh # first time only -- clones dudect
make # builds dudect_verify + dudect_combine
./dudect_verify # smoke test (10000 samples/batch * 4 batches)
./dudect_combine # smoke test (2000 samples/batch * 4 batches)
Submission run
# 10^9 samples per target on a pinned-CPU quiet host:
DUDECT_SAMPLES=1000000 DUDECT_MAX_BATCHES=1000 ./dudect_verify
DUDECT_SAMPLES=1000000 DUDECT_MAX_BATCHES=1000 ./dudect_combine
CT-population framing
Both harnesses use the valid-signature class framing:
- Verify: both class A and class B are valid Corona signatures on the same (group_pk, message). They differ only in the per-signing rejection-loop randomness. Any timing difference detected is a signature-content-dependent code path in Verify.
- Combine: both class A and class B are valid R2-data tuples. The Combine path has NO secret inputs (every input is broadcast on the wire), so any timing difference is an unexpected content-dependent code path in Finalize.
The valid-class framing differs from the simpler garbage-bytes-vs- random-bytes pattern because Corona Verify has no secret state to leak; the empirically meaningful CT property is the valid-population constancy.
Hosts
- x86_64 Linux/macOS: builds against upstream dudect.h directly.
- aarch64 Linux/macOS:
dudect_compat.his force-included to supply AArch64 cycle-counter equivalents (CNTVCT_EL0 on Linux,mach_absolute_time()on Darwin).
Limitations
- 10000-sample smoke runs are NOT statistically meaningful for CT certification. The smoke-test pass is "the harness compiles and runs without obvious leakage signal." The submission-grade verdict requires the full 10^9-sample run on pinned, quiet hardware.
- Combine's CT property is trivially true (no secret inputs); the Combine harness is a SANITY CHECK on the Finalize pipeline, not a property test.
Refinement
The dudect harnesses provide EMPIRICAL CT evidence for the modules:
Verify: corona/threshold/threshold.go:Verify + corona/sign/sign.go:VerifyCombine: corona/threshold/threshold.go:Signer.Finalize + corona/sign/sign.go:SignFinalize
The Jasmin-CT theoretical CT proof for the threshold layer is in
~/work/lux/corona/jasmin/threshold/{round1,round2,combine}.jazz and
scripts/checks/jasmin.sh enforces it as a per-push blocking gate.