meta: port ironwood's extended AxiomCheck

[daira]

Replaces the minimal assert_axioms/assert_computable with ironwood's extended version (Zcash/Meta/AxiomCheck.lean), which the two repos now share up to repo-specific references. This is groundwork for re-checking the build with an independent kernel implementation (nanoda): the owner-naming census makes the exact per-use native_decide axiom names a build-checked artifact, which is what an external checker's permitted-axiom list needs to pin.

What the extended version adds:

• +native(D₁, ...) owner lists — a bare +native permitted a native_decide axiom brought in by any declaration entering the dependency cone; entries now name the owning declarations of exactly the axioms reached, and a stale or incomplete list fails the build with the list to write.
• Provenance checks — an alleged native auxiliary must sit in the owner's own footprint, come from the same module, and start strictly inside the owner's declaration range. This rejects hand-written or macro-emitted axioms merely named like compiler auxiliaries.
• Compiled-body override rejection — @[implemented_by]/@[extern] swap what runs without changing the axiom footprint; both commands reject a censused target carrying one, and any override anywhere in the non-ambient import closure.
• Native evaluated-surface check — a native_decide certificate must not have evaluated a partial declaration (the kernel constant has no body at all). The walk follows @[csimp] replacements, so a future registration of padd_eq_paddFast cannot open a gap.
• assert_computable hardening — rejects unsafe definitions (which can inhabit any type by bare self-reference) and an over-broad +choice.
• Fully qualified entry names — entries no longer depend on the census file's opens.

The regression tests for forged axioms, doctored @[implemented_by] bodies, and partial-backed certificates are ported to a new MetaCheck library outside CompElliptic/: they never enter the production import graph, the source-level sweeps (check_csimp_census.sh, check_native_optin.py) do not scan them, and a plain lake build still runs them.

TrustBoundary's six +native entries now name their owners, build-checked as exact: each Tonelli–Shanks datum owns the two certificates of its primitivity check (ax_1, ax_2), and the curve-order entries reach exactly the nsmul witnesses' axioms (ax_1_1).

🤖 Claude Fable 5

[daira]

Self-ACK

[TalDerei]

ACK port

[daira]

Self-reACK