mirror of
https://github.com/luxfi/corona.git
synced 2026-07-27 02:50:34 +00:00
Hanzo AI
72af1f2099
- 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.
99 lines
2.7 KiB
Bash
Executable File
99 lines
2.7 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# scripts/checks/jasmin.sh -- Jasmin type-check + jasmin-ct gates for Corona.
|
|
#
|
|
# Two independent obligations:
|
|
#
|
|
# 1. The threshold-layer .jazz files (round1, round2, combine) MUST
|
|
# type-check under jasminc and MUST pass jasmin-ct (without
|
|
# --infer). Failure of either is BLOCKING; this script exits 2.
|
|
#
|
|
# 2. The centralized rlwe/sign.jazz is run through jasmin-ct
|
|
# --infer as ADVISORY. Findings are reported but do not fail the
|
|
# gate.
|
|
#
|
|
# Skip-friendly: exits 0 with [skip] message when jasminc is not on
|
|
# PATH, so the orchestrator gate stays additive.
|
|
|
|
set -euo pipefail
|
|
|
|
REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
|
|
cd "$REPO_ROOT"
|
|
|
|
JASMIN_ROOT="$REPO_ROOT/jasmin"
|
|
|
|
if ! command -v jasminc >/dev/null 2>&1; then
|
|
echo "==> jasmin"
|
|
echo " [skip] jasminc not on PATH (opam install jasmin)"
|
|
exit 0
|
|
fi
|
|
echo "==> jasminc found ($(jasminc -version 2>&1 | head -1))"
|
|
|
|
JAZZ_FILES=(
|
|
"$JASMIN_ROOT/threshold/round1.jazz"
|
|
"$JASMIN_ROOT/threshold/round2.jazz"
|
|
"$JASMIN_ROOT/threshold/combine.jazz"
|
|
)
|
|
|
|
# ----- threshold layer: type check -----
|
|
JASMIN_FAIL=0
|
|
for f in "${JAZZ_FILES[@]}"; do
|
|
if [[ ! -f "$f" ]]; then
|
|
echo " [warn] missing: $f"
|
|
continue
|
|
fi
|
|
echo " [check] $f"
|
|
if ! jasminc -until_typing -I "Corona=$JASMIN_ROOT/lib" "$f" 2>&1 | grep -E "^.*error" ; then
|
|
echo " [ok] $f type-checks"
|
|
else
|
|
echo " [FAIL] $f"
|
|
JASMIN_FAIL=1
|
|
fi
|
|
done
|
|
if [[ $JASMIN_FAIL -ne 0 ]]; then
|
|
echo
|
|
echo " Jasmin type-check gate FAILED."
|
|
exit 2
|
|
fi
|
|
|
|
# ----- threshold layer: jasmin-ct BLOCKING -----
|
|
if ! command -v jasmin-ct >/dev/null 2>&1; then
|
|
echo " [skip] jasmin-ct not on PATH"
|
|
exit 0
|
|
fi
|
|
|
|
echo
|
|
echo "==> jasmin-ct (BLOCKING -- threshold layer)"
|
|
CT_FAIL=0
|
|
for f in "${JAZZ_FILES[@]}"; do
|
|
[[ -f "$f" ]] || continue
|
|
CT_OUT=$(jasmin-ct -I "Corona=$JASMIN_ROOT/lib" "$f" 2>&1)
|
|
if [[ -z "$CT_OUT" ]]; then
|
|
echo " [ok] $f"
|
|
else
|
|
echo " [FAIL] $f"
|
|
echo "$CT_OUT" | sed 's/^/ /'
|
|
CT_FAIL=1
|
|
fi
|
|
done
|
|
if [[ $CT_FAIL -ne 0 ]]; then
|
|
echo
|
|
echo " jasmin-ct gate FAILED -- threshold layer no longer CT-clean."
|
|
exit 2
|
|
fi
|
|
|
|
# ----- rlwe centralized: jasmin-ct ADVISORY -----
|
|
RLWE_SIGN="$JASMIN_ROOT/rlwe/sign.jazz"
|
|
if [[ -f "$RLWE_SIGN" ]]; then
|
|
echo
|
|
echo "==> jasmin-ct (advisory -- Corona rlwe/sign)"
|
|
CT_OUT=$(jasmin-ct --infer -I "Corona=$JASMIN_ROOT/lib" "$RLWE_SIGN" 2>&1 | tail -2 || true)
|
|
if [[ -z "$CT_OUT" ]]; then
|
|
echo " [advisory-ok] $RLWE_SIGN"
|
|
else
|
|
echo " [advisory-note] $RLWE_SIGN"
|
|
echo "$CT_OUT" | sed 's/^/ /'
|
|
fi
|
|
fi
|
|
|
|
exit 0
|