lux/pulsar
2
0
Fork 0
mirror of https://github.com/luxfi/pulsar.git synced 2026-09-24 00:25:52 +00:00
Code Issues Packages Projects Releases Wiki Activity
Files
main
pulsar/proofs/easycrypt/extraction/README.md
T
zeekay c79fe61d62 consolidate: merge pulsar-mptc submission framework into canonical luxfi/pulsar 
Single repo, one canonical impl + spec + proofs + KAT + cut tool.

Per "ONE and ONLY ONE way to do things" the prior dual-repo split
(luxfi/pulsar = production library, luxfi/pulsar-mptc = NIST MPTC
submission framework) is collapsed into a single canonical home at
github.com/luxfi/pulsar. SINGLE-IMPL-PLAN.md (now marked COMPLETED)
describes the steps; this commit lands the final step.

Files moved (89 new):
  16 submission docs (SUBMISSION, NIST-SUBMISSION, SPEC, SUITE,
     PATENTS, AXIOM-INVENTORY, PROOF-CLAIMS, FIPS-TRACEABILITY,
     TRUSTED-COMPUTING-BASE, HANZO-CRYPTO-SUITE, INFORMATION-
     ARCHITECTURE, ROADMAP, CHANGELOG, SYNC-STATUS, STATUS-
     SUBMISSION-READINESS, SINGLE-IMPL-PLAN)
  10 docs/ supplements (ietf-draft-skeleton, magnetar, evaluation,
     patent-claims, x-wing-sig, design-decisions, family-architecture,
     threat-model, nist-mptc-category, patent-notes-draft)
  19 proofs/ (13 EC theories + 2 EC lemmas + 4 metadata/READMEs +
     lean-easycrypt-bridge.md)
  14 jasmin/ (lib/* + ml-dsa-65 fetch + threshold/{combine,round1,
     round2}.jazz + READMEs)
  10 ct/dudect/ (Makefile, combine_ct.go, dudect_combine.c,
     dudect_compat.h, dudect_verify.c, fetch.sh, README, run-
     submission.sh, verify_ct.go) + ct/jasmin-ct-libjade.md
  1 .github/workflows/ci.yml
  1 test/interoperability/n1_class_test.go (19/19 N1 subtests)
  1 bench/results/REPORT.md
  11 scripts/ (cut-submission, check-high-assurance, check-lean-
     bridge, nightly, extract-jasmin-ec, checks/{ec-admits, ec-
     compile, ec-refinement-scaffold, ec-regressions, extraction,
     jasmin}, checks/test/{go-unit, interop, kat, no-secret-logs})

Files merged (16 overlapping, mptc-canonical chosen because newer +
post-rewire-correct; pulsar versions still bore stale "Pulsar-M" /
"pulsarm" branding):
  README.md, BLOCKERS.md, CONTRIBUTING.md, LICENSE, LICENSING.md,
  SECURITY.md, .gitignore, bench/run_all.sh, vectors/dkg.json (v1.0.7
  regen), scripts/{bench,build,gen_vectors,sbom,test}.sh,
  spec/{pulsar,parameters,system-model}.tex,
  CRYPTOGRAPHER-SIGN-OFF.md (path refs).

Pulsar-only spec supplements preserved:
  spec/{blockers,design-decisions,family-architecture,nist-mptc-
  category,patent-notes,threat-model}.tex.

Path rewrites applied: 158 occurrences across 26 files
  github.com/luxfi/pulsar-mptc -> github.com/luxfi/pulsar
  ~/work/lux/pulsar-mptc/      -> ~/work/lux/pulsar/
  luxfi/pulsar-mptc            -> luxfi/pulsar
  pulsar-mptc/                  -> ./

Narrative collapses (no more two-repo framing):
  SUBMISSION.md "At a glance" — single Repository row
  SYNC-STATUS.md — rewritten to single-repo state
  SINGLE-IMPL-PLAN.md — marked COMPLETED 2026-05-18
  HANZO-CRYPTO-SUITE.md — tier 1 row = single canonical home
  scripts/cut-submission.sh — replace/vendor dance removed; cuts
  directly from in-tree canonical sources

go.mod: dropped mptc's replace directive (no longer needed since this
IS the canonical pulsar repo). Module path is github.com/luxfi/pulsar.
Deps: cloudflare/circl v1.6.3, golang.org/x/crypto v0.32.0.

Verification:
  GOWORK=off go build ./...              PASS
  GOWORK=off go test -count=1 ./...      PASS (1.4s)
  GOWORK=off go test -race ./ref/...     PASS (14.7s)
  go test ./test/interoperability/       PASS (19/19 N1 subtests)
  scripts/check-high-assurance.sh        PASS
  scripts/check-lean-bridge.sh           PASS (5/5 bridges)
  scripts/gen_vectors.sh                 byte-identical replay
  scripts/cut-submission.sh --help       PASS
2026-05-18 19:53:08 -07:00

2.7 KiB
Raw Permalink Blame History

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:

  1. The Jasmin source is well-typed at every compilation pass jasmin2ec runs (default --after=typing).
  2. The libjade dependencies resolve to EC theories that exist in the libjade-fetched tree at the pinned commit.
  3. 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):

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).
Reference in New Issue View Git Blame Copy Permalink