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.
71 lines
2.0 KiB
Bash
Executable File
71 lines
2.0 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# scripts/checks/ec-compile.sh -- EasyCrypt compile gate for all
|
|
# tracked EC files (Corona).
|
|
#
|
|
# Runs `easycrypt compile` on each file in EC_FILES and fails the
|
|
# gate on any non-zero exit. Skips silently if easycrypt is not
|
|
# installed.
|
|
|
|
set -euo pipefail
|
|
|
|
REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
|
|
EC_ROOT="$REPO_ROOT/proofs/easycrypt"
|
|
|
|
EC_FILES=(
|
|
"$EC_ROOT/Corona_N1.ec"
|
|
"$EC_ROOT/Corona_N4.ec"
|
|
"$EC_ROOT/lemmas/Corona_CT.ec"
|
|
"$EC_ROOT/lemmas/RLWE_Functional.ec"
|
|
"$EC_ROOT/Corona_N1_Memory.ec"
|
|
"$EC_ROOT/Corona_N1_Signature_Codec.ec"
|
|
"$EC_ROOT/Corona_N1_Combine_Layout.ec"
|
|
"$EC_ROOT/Corona_N1_Sign_Layout.ec"
|
|
"$EC_ROOT/Corona_N1_Combine_Refinement.ec"
|
|
"$EC_ROOT/Corona_N1_Sign_Refinement.ec"
|
|
"$EC_ROOT/Corona_N1_Combine_Wrapper.ec"
|
|
"$EC_ROOT/Corona_N1_Sign_Wrapper.ec"
|
|
"$EC_ROOT/Corona_N1_Extracted.ec"
|
|
)
|
|
|
|
if ! command -v easycrypt >/dev/null 2>&1; then
|
|
echo "==> EasyCrypt compile gate"
|
|
echo " [skip] easycrypt not on PATH"
|
|
echo " install (source build): https://github.com/EasyCrypt/easycrypt"
|
|
exit 0
|
|
fi
|
|
|
|
EC_HASH=$(easycrypt config 2>&1 | grep "git-hash" | head -1)
|
|
echo "==> easycrypt found ($EC_HASH)"
|
|
|
|
EC_FAIL=0
|
|
EC_FAIL_LIST=()
|
|
for f in "${EC_FILES[@]}"; do
|
|
if [[ ! -f "$f" ]]; then
|
|
echo " [warn] missing: $f"
|
|
continue
|
|
fi
|
|
log="/tmp/ec-compile-$$.$(basename "$f").log"
|
|
rc=0
|
|
easycrypt compile -I "$EC_ROOT" -I "$EC_ROOT/lemmas" "$f" \
|
|
> "$log" 2>&1 || rc=$?
|
|
if [[ $rc -eq 0 ]]; then
|
|
echo " [ok] $f compiles"
|
|
rm -f "$log"
|
|
else
|
|
echo " [FAIL] $f (rc=$rc):"
|
|
tr '\r' '\n' < "$log" | grep -E "\[critical\]|^[[:space:]]*unknown|error" | head -5 | sed 's/^/ /'
|
|
EC_FAIL=1
|
|
EC_FAIL_LIST+=("$f")
|
|
fi
|
|
done
|
|
|
|
if [[ $EC_FAIL -ne 0 ]]; then
|
|
echo
|
|
echo " EasyCrypt compile gate FAILED on ${#EC_FAIL_LIST[@]} file(s):"
|
|
for f in "${EC_FAIL_LIST[@]}"; do
|
|
echo " $f"
|
|
done
|
|
exit 2
|
|
fi
|
|
exit 0
|