# Axioms that a LOAD-BEARING lemma rests on, reviewed and justified.
# Format: AXIOM_NAME  <bucket> -- <justification>
#
# An entry here is an explicit, disclosed trust assumption. The framework
# (~/work/lux/luxfi/security/framework/checks/circular-proof.sh) HARD-requires only
# the axioms that a load-bearing-named lemma discharges via apply/exact in a
# <=12-line proof; today that is `lagrange_inverse_eval` alone. We list MORE
# than the mechanical minimum on purpose: every axiom in the dependency cone
# of the headline byte-equality lemma is part of the trust surface and is
# written down here with its bucket. This is full disclosure, NOT a blanket
# allow -- only load-bearing / security-cone axioms appear; the pure
# layout/length B-axioms and the standard-fact A-axioms that feed only
# structural lemmas are inventoried in AXIOM-INVENTORY.md, not blanket-listed
# here. Buckets: A standard-math-fact | B serialization/layout | C OPEN
# security assumption (reconstruct-then-sign; see BLOCKERS.md).

# --- A: load-bearing standard-math-fact (mechanically flagged) ---
lagrange_inverse_eval  A -- Lagrange interpolation: P(0) recovered from any t distinct evaluations over a field of order > committee size (spec/pulsar.tex eq. 476). EasyCrypt lacks this over abstract share_t; Lean-bridged to Crypto.Pulsar.Shamir.shamir_correct_at_target (Mathlib polynomial-Lagrange). The algebraic core the threshold reduction USES, NOT the threshold security claim. Used by reconstruct_of_share via `exact:`.
threshold_partial_response_identity  A -- Lagrange-aggregation of per-party partial responses = centralised z on the reconstructed share. Lean-bridged. Load-bearing for combine_body_z_spec (the z-stage derived lemma) -> pulsar_n1_byte_equality.
reconstruct_linear  A -- reconstruction is linear over share-list addition (LinearMap.map_add). Lean-bridged. Load-bearing for the N4 reshare-preservation lemmas.
shamir_correct  A -- reconstruction is a left inverse of fresh sharing (Lagrange-at-zero). Lean-bridged. Load-bearing for honest_reshare_reconstructs / reshare_preserves_secret_honest (N4).
add_share_zeroR  A -- additive identity on share_t (AddCommMonoid). Lean-bridged. Load-bearing for the N4 reshare zero-sharing argument.

# --- C: OPEN security assumptions in the IDEALISED-CORRECTNESS byte-equality cone
#        (reconstruct-then-sign). DISCLOSED, NOT closed. These prove the threshold
#        OUTPUT bit-equals central sign on the reconstructed secret -- an idealised
#        CORRECTNESS statement, NOT how production runs. The production no-leak
#        path's residual is the STANDARD-ASSUMPTION reduction in the next block
#        (Pulsar_N1_NoLeak.ec), not these. See BLOCKERS.md PULSAR-EC-RECON-MODEL. ---
combine_body_axiom  C -- OPEN. declare axiom: T.combine ~ CombineAbs.combine on honest-quorum inputs == the extracted threshold combine equals the centralised ML-DSA sign of the LAGRANGE-RECONSTRUCTED secret. Module-contract form of the whole byte-walk; pulsar_n1_byte_equality rests on it via `call combine_body_axiom`. IDEALISED CORRECTNESS model only. Closure = the Jasmin byte-walk (issue #4). NOT proven.
S_functional_spec  C -- OPEN. declare axiom: S.sign ~ FIPS204Sign.sign on accepted inputs == the single-party module is a faithful FIPS 204 signer. pulsar_n1_byte_equality rests on it via single_party_run_refines_fips204. Closure = the libjade byte-walk (issue #3). NOT proven.
algebraic_aggregate_ctx_body_axiom  C -- OPEN. The v0.4 reconstruct-then-sign axiom: AlgebraicAggregateCtx output = FIPS 204 SignCtx(sk_master, ctx, M) where sk_master is the existentially-quantified RECONSTRUCTED master secret. threshold_sign_ctx_equiv_fips204_sign_with_ctx rests on it. Go-discharged by test + AST sweep, NOT by EC. NOT proven.

# --- The NO-LEAK model (Pulsar_N1_NoLeak.ec) -- the HONEST production residual.
#     Replaces reconstruct-then-sign as the load-bearing path: the masked Lagrange
#     aggregate equals central z WITHOUT forming the master secret, the hint is
#     recovered from PUBLIC w', and the ONLY open assumption is a STANDARD
#     Module-LWE/MSIS reduction (no implementation reconstruct). The algebraic core
#     is MACHINE-CHECKED in Lean (Crypto.Pulsar.NoLeak / .Boundary; lake build green). ---
public_hint_roundtrip  B -- standard/Lean-backed. Procedure-level lift of the MACHINE-CHECKED (Lean) Crypto.Pulsar.Boundary.boundary_clearance + findHintCoeff_sound/_unique: on a boundary-clear nonce, FindHint over the PUBLIC (w', w1) returns a hint UseHint maps back to w1. References ONLY public quantities (w'=A*z-c*t1*2^d, w1) -- no c*s2/c*t0/r0. Load-bearing for no-leak hint correctness. Recheck pending ec-compile.
no_leak_reduction  C -- OPEN, but STANDARD-ASSUMPTION (NOT reconstruct-then-sign). Under Module-LWE + Module-SIS the public threshold transcript (w1, commit(w), clearance proof, c_tilde, z, h) is simulatable from one single-party FIPS 204 signature's leakage == leaks nothing extra about (s1,s2,t0). The honest replacement for combine_body_axiom: a reduction to the SAME lattice assumptions ML-DSA's EUF-CMA already uses, with the secret NEVER reconstructed. no_leak_under_standard_assumptions rests on it. EC mirror of MACHINE-CHECKED Lean Crypto.Pulsar.NoLeak.NoLeakReduction. Full simulation proof = v0.8 artifact. NOT proven (but a standard reduction, not an impl reconstruct).
