mirror of
https://github.com/luxfi/pulsar.git
synced 2026-10-30 14:45:29 +00:00
36 lines
2.0 KiB
Plaintext
36 lines
2.0 KiB
Plaintext
# 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
|