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.
62 lines
1.7 KiB
Bash
Executable File
62 lines
1.7 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# Corona submission-grade dudect run.
|
|
#
|
|
# Runs the verify + combine harnesses with the full submission budget
|
|
# (10^9 samples per target). Designed for a quiet, CPU-pinned host
|
|
# (cpuset.cpus, governor=performance, no other workload).
|
|
#
|
|
# Mirrors ~/work/lux/pulsar/ct/dudect/run-submission.sh.
|
|
|
|
set -euo pipefail
|
|
|
|
SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
|
cd "$SCRIPT_DIR"
|
|
|
|
# Submission-grade budget.
|
|
SAMPLES_PER_BATCH="${SAMPLES_PER_BATCH:-1000000}"
|
|
MAX_BATCHES="${MAX_BATCHES:-1000}"
|
|
|
|
# Pre-flight checks.
|
|
if ! command -v make >/dev/null 2>&1; then
|
|
echo "==> make not found"
|
|
exit 1
|
|
fi
|
|
|
|
if [[ ! -f "dudect/src/dudect.h" ]]; then
|
|
echo "==> dudect.h missing -- running fetch.sh"
|
|
bash ./fetch.sh
|
|
fi
|
|
|
|
echo "==> Building harnesses"
|
|
make clean
|
|
make
|
|
|
|
# Run verify.
|
|
echo
|
|
echo "==> dudect_verify ($SAMPLES_PER_BATCH samples * $MAX_BATCHES batches)"
|
|
DUDECT_SAMPLES="$SAMPLES_PER_BATCH" DUDECT_MAX_BATCHES="$MAX_BATCHES" \
|
|
./dudect_verify 2>&1 | tee verify.log
|
|
verify_rc="${PIPESTATUS[0]}"
|
|
echo "==> dudect_verify exit code: $verify_rc"
|
|
|
|
# Run combine.
|
|
echo
|
|
echo "==> dudect_combine ($SAMPLES_PER_BATCH samples * $MAX_BATCHES batches)"
|
|
DUDECT_SAMPLES="$SAMPLES_PER_BATCH" DUDECT_MAX_BATCHES="$MAX_BATCHES" \
|
|
./dudect_combine 2>&1 | tee combine.log
|
|
combine_rc="${PIPESTATUS[0]}"
|
|
echo "==> dudect_combine exit code: $combine_rc"
|
|
|
|
echo
|
|
echo "==> SUMMARY"
|
|
echo " verify exit: $verify_rc (0 = no leakage evidence; 2 = leakage found)"
|
|
echo " combine exit: $combine_rc (0 = no leakage evidence; 2 = leakage found)"
|
|
echo
|
|
echo " Submission verdict: PASS only when BOTH exit 0."
|
|
|
|
# Exit non-zero if either failed.
|
|
if [[ "$verify_rc" -ne 0 || "$combine_rc" -ne 0 ]]; then
|
|
exit 2
|
|
fi
|
|
exit 0
|