corona/.assurance/budget.txt

# Unproven-assertion budget (max counts). Enforced by
# ~/work/lux/luxfi/security/framework/checks/axiom-budget.sh. FAILS on any drift above.
# Goal: decrease, never raise.
#
# Current surface. The axioms are fully bucketed in AXIOM-INVENTORY.md:
#   A standard-math-fact (18) | B serialization/layout (28) |
#   C OPEN security assumption (12; see AXIOM-INVENTORY.md / BLOCKERS.md).
#   (Per-bucket counts are hand-maintained; the AXIOM=59 total is the
#   machine-enforced authority — sub-bucket drift never gates.)
#
# EC TOOLCHAIN IS LIVE ON THIS HOST. EasyCrypt (opam switch `proofs`:
# easycrypt + why3 + alt-ergo, z3 as solver) machine-checks all 14 corona
# theories via `easycrypt compile`; the framework gate runs
# checks/ec-machine-check.sh on every invocation. A `.ec` that does not
# compile is never counted green. (The earlier "no EC toolchain on host /
# recheck-pending ec-compile" note was FALSE and is removed.)
#
# Machine-check fixes landed this pass (all surfaced by ec-machine-check.sh):
#   * Corona_N1.ec: `type R_q_xi` declared after first use (moved up);
#     `op w_low_t : Type` (EC has no Type sort, dead) removed.
#   * Corona_N1_Sign_Wrapper.ec / _Combine_Wrapper.ec: over-introduced
#     `skip => /> &m1 &m2 ? ...` corrected to the real binder count.
#   * lemmas/RLWE_Functional.ec: `sigma_*)` prematurely closed its comment.
#   * Corona_N1_Combine_Wrapper.ec: the `smt(combine_abs_op_lifted_bridge)`
#     close did not hold (the bridge stops at the byte-level combine_abs_op,
#     not rlwe). Closed CONDITIONAL on a DISCLOSED OPEN bridge -- see below.
#
# NET +0 axioms this pass: the Corona combine bridge was DISCHARGED and its
# residual SHRUNK (one C axiom removed, one narrower C axiom added; total 59
# unchanged):
#   DISCHARGED -> LEMMA:  combine_abs_op_lifted_eq_rlwe
#     Was the whole-bridge reconstruct-then-sign axiom (combine_abs_op_lifted
#     = rlwe_sign_op on the Lagrange-reconstructed secret). combine_abs_op_
#     lifted is now a CONCRETE threshold definition (the no-leak assembly), and
#     the bridge is a PROVEN LEMMA on honest, well-formed quorums. The
#     load-bearing z-leg (where the secret enters) goes through the MACHINE-
#     CHECKED keystone Corona_N1_NoLeak.no_leak_z_aggregate (= Lean threshold_
#     partial_response_identity) -- verified load-bearing (removing it fails
#     the proof). The master secret is never reconstructed.
#   NEW NARROW RESIDUAL:  threshold_public_commitment_eq_central  (C, PUBLIC-ONLY)
#     The threshold-assembled PUBLIC Fiat-Shamir commitment w = A*y (mask-sum,
#     no c*s) equals the central commitment central_w on the reconstructed
#     share. References PUBLIC data ONLY -- the c-leg + Delta-leg residual. This
#     is the SHRUNK replacement for the secret-bearing whole-bridge axiom: it
#     is about the public commitment, not the whole signature.
#   -> AXIOM 59 -> 59 (count flat; residual surface dramatically narrowed).
#
# The no-leak production model (Corona_N1_NoLeak.ec) remains the load-bearing
# residual: per-party masked responses aggregate to R*u + c*s because the
# pairwise-PRF masks TELESCOPE TO ZERO (master secret never formed), and the
# ONLY open assumption is a STANDARD Module-LWE/Module-SIS reduction. Its
# correctness core is MACHINE-CHECKED in Lean (Crypto.Corona.NoLeakAggregate
# + Crypto.Threshold_Lagrange; lake build green). The combine bridge is now a
# LEMMA; the sign-side reconstruct-then-sign bridge (sign_abs_op_lifted_eq_rlwe)
# remains IDEALISED CORRECTNESS only.
#
# Counts below are the comment-aware machine counts (axiom-budget.sh strips
# (* *) comments first): real `admit`/`abort` tactics = 0; AXIOM is the real
# declaration count.
SORRY=0
ADMIT=0
AXIOM=59
VACUOUS=0