mirror of https://github.com/luxfi/pulsar.git synced 2026-09-24 00:25:52 +00:00

Files

T

History

zeekay 357a5a2087 docs(axiom): single canonical phrasing — 22 named axioms total

Harmonise the axiom accounting everywhere:

    22 named axioms total — 17 narrow implementation-refinement
    (14 byte-walk + 1 signature-codec round-trip + 2 honest-
    execution no-reject post-conditions) plus 5 Lean-bridged
    algebraic, each with file:line in EC and Lean.

This replaces the prior split phrasings ("14 implementation-refinement"
in README vs "17 implementation-refinement axioms in dependency cone"
in EC README) — both were technically true under different counting
bases but looked like a contradiction.

- README.md: hard-boundary block + axiom table use canonical phrasing.
- SUBMISSION.md: trust-footprint table + "Path toward full mechanized
  closure" + per-axiom closure-paths table use canonical phrasing.
- docs/proof-axiom-inventory.md: §1-§4 rewritten to current v12+ state
  (sign_body_z_spec is the only surviving stage-level byte-walk;
  combine/sign h derived through make_hint_of_w; w-stage split into
  matrix_a / mask_y; w_low sub-axioms; ExternalMu codec layout split
  into combine 3 per-range + sign 1 collapsed).
- docs/proof-claims.md: scope-boundary framing on adversarial
  robustness section.
- docs/tcb.md: §3.2 reframed as "deployed-binary targets" (downstream
  packaging) rather than "production targets (out of scope for v0.1)".
- docs/cryptographer-sign-off.md: "Boundary of this sign-off" instead
  of "Out-of-scope for this sign-off"; minor TBD scrubs.
- proofs/easycrypt/README.md: trust-boundary table uses canonical
  phrasing.
- proofs/easycrypt/Pulsar_N1_Extracted.ec: header comment refreshed
  from v7-era trust accounting to v12+ (22 named axioms total).
- proofs/lean-easycrypt-bridge.md: "Future work" → "Closure paths";
  summary uses canonical phrasing.
- proofs/easycrypt/extraction/{combine,sign}-byte-walk-roadmap.md:
  "followup B" → "v10 no-reject decomposition".

2026-05-31 11:21:38 -07:00

combine-byte-walk-roadmap.md

docs(axiom): single canonical phrasing — 22 named axioms total

2026-05-31 11:21:38 -07:00

README.md

consolidate: merge pulsar-mptc submission framework into canonical luxfi/pulsar

2026-05-18 19:53:08 -07:00

sign-byte-walk-roadmap.md

docs(axiom): single canonical phrasing — 22 named axioms total

2026-05-31 11:21:38 -07:00

README.md

Jasmin → EasyCrypt extraction artifacts

This directory holds the output of jasmin2ec run over the threshold layer in jasmin/threshold/. The artifact is not vendored — it is regenerated on demand by scripts/extract-jasmin-ec.sh. CI runs that extraction script as part of the high-assurance gate and discards the output between runs.

Why on-demand rather than vendored

The extraction produces ~4000 lines of EC per .jazz function plus ~60 array-support theories shared across the threshold layer and libjade. Vendoring this would (a) be 5+ MB of generated EC drowning human-written proofs in the repo, (b) drift silently if a Jasmin source change isn't followed by a re-extraction, and (c) couple repo bumps to specific jasmin2ec versions.

On-demand reproduction is simpler and more honest:

$ bash scripts/extract-jasmin-ec.sh

…produces proofs/easycrypt/extraction/build/{combine,round1,round2}.ec plus the array-support theories.

What the extraction guarantees

The fact that jasmin2ec produces an EC theory that compiles standalone guarantees:

The Jasmin source is well-typed at every compilation pass jasmin2ec runs (default --after=typing).
The libjade dependencies resolve to EC theories that exist in the libjade-fetched tree at the pinned commit.
The generated EC theory parses + type-checks under the same EasyCrypt version we use for the hand-written proofs.

It does NOT guarantee:

That M.pulsar_combine (the extracted procedure) refines CombineAbs.combine (the abstract spec in Pulsar_N1.ec). That refinement is a separate proof obligation — the byte-level equiv [ M.pulsar_combine ~ CombineAbs.combine : ... ==> ={res} ] — which requires a memory model + the ABI bridge from pointer-based W64 args to the abstract (group_pk, m, ctx, …) tuple.

The refinement obligations are tracked as separate issues (different proof efforts, different reviewers, different failure modes):

#4 — combine_body_axiom refinement: equiv [ M.pulsar_combine ~ CombineAbs.combine : ... ]
#3 — S_functional_spec refinement: equiv [ M.sign ~ FIPS204Sign.sign : ... ] (libjade ML-DSA-65)
#2 — jasmin-ct annotations: add #public / #declassify to 4 .jazz files so the jasmin-ct-leakage CI job flips from advisory to blocking.

Pinning

Jasmin version: from ~/.opam/jasmin/bin/jasminc -version at extract time.
libjade commit: 9426b32 (pinned by jasmin/ml-dsa-65/fetch.sh).
EasyCrypt commit: 909464e (pinned by .github/workflows/ci.yml Install EasyCrypt (source build) step).