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.
48 lines
1.8 KiB
Bash
Executable File
48 lines
1.8 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# scripts/checks/ec-refinement-scaffold.sh -- Refinement-scaffold guard.
|
|
#
|
|
# The two refinement files (Combine_Refinement, Sign_Refinement) carry
|
|
# the byte-walk + memory-separation + layout-frame axioms today. CI
|
|
# surfaces declare-axiom shapes in them as warnings (they should be
|
|
# zero -- top-level `axiom` is fine; `declare axiom` is for the
|
|
# section-local module-contract axioms which live only in Corona_N1.ec).
|
|
#
|
|
# Separately: the same files MUST NOT contain top-level `declare axiom`
|
|
# statements -- this script flags any other declare axiom shape as a
|
|
# hard fail to prevent silent obligation drift.
|
|
|
|
set -euo pipefail
|
|
|
|
REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
|
|
EC_ROOT="$REPO_ROOT/proofs/easycrypt"
|
|
|
|
REFINE_FILES=(
|
|
"$EC_ROOT/Corona_N1_Combine_Refinement.ec"
|
|
"$EC_ROOT/Corona_N1_Sign_Refinement.ec"
|
|
)
|
|
|
|
echo "==> Refinement-scaffold status"
|
|
|
|
# Section-local declare-axioms live in Corona_N1.ec.
|
|
if grep -RE "^[[:space:]]*declare axiom[[:space:]]+combine_body_axiom" \
|
|
"$EC_ROOT" >/dev/null 2>&1 ; then
|
|
echo " [warn] combine_body_axiom remains a section-local"
|
|
echo " refinement-boundary axiom (closed by Wrapper)"
|
|
fi
|
|
if grep -RE "^[[:space:]]*declare axiom[[:space:]]+S_functional_spec" \
|
|
"$EC_ROOT" >/dev/null 2>&1 ; then
|
|
echo " [warn] S_functional_spec remains a section-local"
|
|
echo " refinement-boundary axiom (closed by Wrapper)"
|
|
fi
|
|
|
|
# The refinement files themselves should have zero declare axioms.
|
|
REFINE_DECLARE_AXIOMS=$(grep -RE "^[[:space:]]*declare axiom" \
|
|
"${REFINE_FILES[@]}" 2>/dev/null || true)
|
|
if [[ -n "$REFINE_DECLARE_AXIOMS" ]]; then
|
|
echo " [FAIL] refinement scaffolds contain declare axioms:"
|
|
echo "$REFINE_DECLARE_AXIOMS" | sed 's/^/ /'
|
|
exit 2
|
|
fi
|
|
echo " [ok] no declare axiom in refinement scaffolds"
|
|
exit 0
|