# Unproven-assertion budget (max counts). Enforced by
# ~/work/lux/luxfi/security/framework/checks/axiom-budget.sh -- the gate FAILS if any
# count drifts ABOVE these. The honest goal is to DECREASE them (discharge
# axioms/admits into proved lemmas), never to raise the ceiling.
#
# Per-bucket breakdown is authoritative in AXIOM-INVENTORY.md:
#   A standard-math-fact | B serialization/layout | C OPEN security assumption (19).
#
# EC TOOLCHAIN IS LIVE ON THIS HOST. EasyCrypt (opam switch `proofs`) +
# z3/alt-ergo machine-check all top-level + lemmas/ theories via
# `easycrypt compile`; the framework gate runs checks/ec-machine-check.sh
# every invocation, and pulsar passes 14/14. (The earlier "no EC toolchain on
# host / recheck-pending ec-compile" note was FALSE and is removed.)
#
# Two things changed the count since the no-leak pass:
#   * Deleted proofs/easycrypt/V04_Sign_Ctx.ec -- a stale orphan for the v0.4
#     ctx-bound AlgebraicAggregate leaking path (sibling of the removed v0.3
#     path). It never compiled (missing FIPS204_Axioms theory, no .eco). This
#     removes 5 axiom declarations (empty_bytes_len/byte_of_zero/bytes_cat_empty_l
#     [was B41], mldsa_sign_ctx_axiom [was C15], algebraic_aggregate_ctx_body_axiom
#     [was C16 -- the reconstruct-then-sign axiom in its starkest form]).
#   * The no-leak production model (Pulsar_N1_NoLeak.ec) remains: the masked
#     Lagrange aggregate equals central z WITHOUT forming the master secret;
#     hint from PUBLIC w'; the only open assumption is a STANDARD Module-LWE/MSIS
#     reduction. Correctness core MACHINE-CHECKED in Lean (Crypto.Pulsar.
#     NoLeakAggregate + BoundaryClearance + Crypto.Threshold_Lagrange).
#
# Counts below are the comment-aware machine counts (axiom-budget.sh strips
# (* *) comments first, so prose like "DISCHARGED (no admit)" no longer
# inflates): real `admit`/`abort` tactics = 0; AXIOM = real declaration count
# (was 80 hand-counted; 80 - 5 deleted V04 axioms = 75).
SORRY=0
ADMIT=0
AXIOM=75
VACUOUS=0
