mirror of
https://github.com/hanzo-docs/docs.git
synced 2026-10-24 20:09:02 +00:00
feat(pulsar-docs): add Fumadocs site for luxfi/pulsar at apps/pulsar-docs
Scaffold cloned from apps/zen-docs. Port 3008. Content authored from the settled state of ~/work/lux/pulsar/main (README, EC README, bridge doc, extraction roadmaps, NIST-SUBMISSION, SUBMISSION, CHANGELOG, SECURITY, postmortem). Math rendered with KaTeX. Information architecture: intro -> getting-started -> protocol -> reference -> proofs -> security -> nist-mptc -> postmortem -> changelog. Build clean: pnpm --filter=pulsar-docs build && pnpm --filter=pulsar-docs dev.
This commit is contained in:
@@ -0,0 +1,34 @@
|
||||
# Dependencies
|
||||
node_modules/
|
||||
.pnpm-store/
|
||||
|
||||
# Build
|
||||
.next/
|
||||
.turbo/
|
||||
out/
|
||||
dist/
|
||||
|
||||
# IDE
|
||||
.idea/
|
||||
.vscode/
|
||||
*.swp
|
||||
*.swo
|
||||
|
||||
# OS
|
||||
.DS_Store
|
||||
Thumbs.db
|
||||
|
||||
# Env
|
||||
.env
|
||||
.env.local
|
||||
.env.*.local
|
||||
|
||||
# Logs
|
||||
*.log
|
||||
npm-debug.log*
|
||||
yarn-debug.log*
|
||||
yarn-error.log*
|
||||
|
||||
# Types
|
||||
*.tsbuildinfo
|
||||
next-env.d.ts
|
||||
@@ -0,0 +1,200 @@
|
||||
Apache License
|
||||
Version 2.0, January 2004
|
||||
http://www.apache.org/licenses/
|
||||
|
||||
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
|
||||
|
||||
1. Definitions.
|
||||
|
||||
"License" shall mean the terms and conditions for use, reproduction,
|
||||
and distribution as defined by Sections 1 through 9 of this document.
|
||||
|
||||
"Licensor" shall mean the copyright owner or entity authorized by
|
||||
the copyright owner that is granting the License.
|
||||
|
||||
"Legal Entity" shall mean the union of the acting entity and all
|
||||
other entities that control, are controlled by, or are under common
|
||||
control with that entity. For the purposes of this definition,
|
||||
"control" means (i) the power, direct or indirect, to cause the
|
||||
direction or management of such entity, whether by contract or
|
||||
otherwise, or (ii) ownership of fifty percent (50%) or more of the
|
||||
outstanding shares, or (iii) beneficial ownership of such entity.
|
||||
|
||||
"You" (or "Your") shall mean an individual or Legal Entity
|
||||
exercising permissions granted by this License.
|
||||
|
||||
"Source" form shall mean the preferred form for making modifications,
|
||||
including but not limited to software source code, documentation
|
||||
source, and configuration files.
|
||||
|
||||
"Object" form shall mean any form resulting from mechanical
|
||||
transformation or translation of a Source form, including but
|
||||
not limited to compiled object code, generated documentation,
|
||||
and conversions to other media types.
|
||||
|
||||
"Work" shall mean the work of authorship, whether in Source or
|
||||
Object form, made available under the License, as indicated by a
|
||||
copyright notice that is included in or attached to the work
|
||||
(an example is provided in the Appendix below).
|
||||
|
||||
"Derivative Works" shall mean any work, whether in Source or Object
|
||||
form, that is based on (or derived from) the Work and for which the
|
||||
editorial revisions, annotations, elaborations, or other modifications
|
||||
represent, as a whole, an original work of authorship. For the purposes
|
||||
of this License, Derivative Works shall not include works that remain
|
||||
separable from, or merely link (or bind by name) to the interfaces of,
|
||||
the Work and Derivative Works thereof.
|
||||
|
||||
"Contribution" shall mean any work of authorship, including
|
||||
the original version of the Work and any modifications or additions
|
||||
to that Work or Derivative Works thereof, that is intentionally
|
||||
submitted to the Licensor for inclusion in the Work by the copyright owner
|
||||
or by an individual or Legal Entity authorized to submit on behalf of
|
||||
the copyright owner. For the purposes of this definition, "submitted"
|
||||
means any form of electronic, verbal, or written communication sent
|
||||
to the Licensor or its representatives, including but not limited to
|
||||
communication on electronic mailing lists, source code control systems,
|
||||
and issue tracking systems that are managed by, or on behalf of, the
|
||||
Licensor for the purpose of discussing and improving the Work, but
|
||||
excluding communication that is conspicuously marked or otherwise
|
||||
designated in writing by the copyright owner as "Not a Contribution."
|
||||
|
||||
"Contributor" shall mean Licensor and any individual or Legal Entity
|
||||
on behalf of whom a Contribution has been received by the Licensor and
|
||||
subsequently incorporated within the Work.
|
||||
|
||||
2. Grant of Copyright License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
copyright license to reproduce, prepare Derivative Works of,
|
||||
publicly display, publicly perform, sublicense, and distribute the
|
||||
Work and such Derivative Works in Source or Object form.
|
||||
|
||||
3. Grant of Patent License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
(except as stated in this section) patent license to make, have made,
|
||||
use, offer to sell, sell, import, and otherwise transfer the Work,
|
||||
where such license applies only to those patent claims licensable
|
||||
by such Contributor that are necessarily infringed by their
|
||||
Contribution(s) alone or by combination of their Contribution(s)
|
||||
with the Work to which such Contribution(s) was submitted. If You
|
||||
institute patent litigation against any entity (including a
|
||||
cross-claim or counterclaim in a lawsuit) alleging that the Work
|
||||
or a Contribution incorporated within the Work constitutes direct
|
||||
or contributory patent infringement, then any patent licenses
|
||||
granted to You under this License for that Work shall terminate
|
||||
as of the date such litigation is filed.
|
||||
|
||||
4. Redistribution. You may reproduce and distribute copies of the
|
||||
Work or Derivative Works thereof in any medium, with or without
|
||||
modifications, and in Source or Object form, provided that You
|
||||
meet the following conditions:
|
||||
|
||||
(a) You must give any other recipients of the Work or
|
||||
Derivative Works a copy of this License; and
|
||||
|
||||
(b) You must cause any modified files to carry prominent notices
|
||||
stating that You changed the files; and
|
||||
|
||||
(c) You must retain, in the Source form of any Derivative Works
|
||||
that You distribute, all copyright, patent, trademark, and
|
||||
attribution notices from the Source form of the Work,
|
||||
excluding those notices that do not pertain to any part of
|
||||
the Derivative Works; and
|
||||
|
||||
(d) If the Work includes a "NOTICE" text file as part of its
|
||||
distribution, then any Derivative Works that You distribute must
|
||||
include a readable copy of the attribution notices contained
|
||||
within such NOTICE file, excluding any notices that do not
|
||||
pertain to any part of the Derivative Works, in at least one
|
||||
of the following places: within a NOTICE text file distributed
|
||||
as part of the Derivative Works; within the Source form or
|
||||
documentation, if provided along with the Derivative Works; or,
|
||||
within a display generated by the Derivative Works, if and
|
||||
wherever such third-party notices normally appear. The contents
|
||||
of the NOTICE file are for informational purposes only and
|
||||
do not modify the License. You may add Your own attribution
|
||||
notices within Derivative Works that You distribute, alongside
|
||||
or as an addendum to the NOTICE text from the Work, provided
|
||||
that such additional attribution notices cannot be construed
|
||||
as modifying the License.
|
||||
|
||||
You may add Your own copyright statement to Your modifications and
|
||||
may provide additional or different license terms and conditions
|
||||
for use, reproduction, or distribution of Your modifications, or
|
||||
for any such Derivative Works as a whole, provided Your use,
|
||||
reproduction, and distribution of the Work otherwise complies with
|
||||
the conditions stated in this License.
|
||||
|
||||
5. Submission of Contributions. Unless You explicitly state otherwise,
|
||||
any Contribution intentionally submitted for inclusion in the Work
|
||||
by You to the Licensor shall be under the terms and conditions of
|
||||
this License, without any additional terms or conditions.
|
||||
Notwithstanding the above, nothing herein shall supersede or modify
|
||||
the terms of any separate license agreement you may have executed
|
||||
with Licensor regarding such Contributions.
|
||||
|
||||
6. Trademarks. This License does not grant permission to use the trade
|
||||
names, trademarks, service marks, or product names of the Licensor,
|
||||
except as required for reasonable and customary use in describing the
|
||||
origin of the Work and reproducing the content of the NOTICE file.
|
||||
|
||||
7. Disclaimer of Warranty. Unless required by applicable law or
|
||||
agreed to in writing, Licensor provides the Work (and each
|
||||
Contributor provides its Contributions) on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
|
||||
implied, including, without limitation, any warranties or conditions
|
||||
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
|
||||
PARTICULAR PURPOSE. You are solely responsible for determining the
|
||||
appropriateness of using or redistributing the Work and assume any
|
||||
risks associated with Your exercise of permissions under this License.
|
||||
|
||||
8. Limitation of Liability. In no event and under no legal theory,
|
||||
whether in tort (including negligence), contract, or otherwise,
|
||||
unless required by applicable law (such as deliberate and grossly
|
||||
negligent acts) or agreed to in writing, shall any Contributor be
|
||||
liable to You for damages, including any direct, indirect, special,
|
||||
incidental, or consequential damages of any character arising as a
|
||||
result of this License or out of the use or inability to use the
|
||||
Work (including but not limited to damages for loss of goodwill,
|
||||
work stoppage, computer failure or malfunction, or any and all
|
||||
other commercial damages or losses), even if such Contributor
|
||||
has been advised of the possibility of such damages.
|
||||
|
||||
9. Accepting Warranty or Additional Liability. While redistributing
|
||||
the Work or Derivative Works thereof, You may choose to offer,
|
||||
and charge a fee for, acceptance of support, warranty, indemnity,
|
||||
or other liability obligations and/or rights consistent with this
|
||||
License. However, in accepting such obligations, You may act only
|
||||
on Your own behalf and on Your sole responsibility, not on behalf
|
||||
of any other Contributor, and only if You agree to indemnify,
|
||||
defend, and hold each Contributor harmless for any liability
|
||||
incurred by, or claims asserted against, such Contributor by reason
|
||||
of your accepting any such warranty or additional liability.
|
||||
|
||||
END OF TERMS AND CONDITIONS
|
||||
|
||||
APPENDIX: How to apply the Apache License to your work.
|
||||
|
||||
To apply the Apache License to your work, attach the following
|
||||
boilerplate notice, with the fields enclosed by brackets "[]"
|
||||
replaced with your own identifying information. (Don't include
|
||||
the brackets!) The text should be enclosed in the appropriate
|
||||
comment syntax for the file format. Please refer to the section
|
||||
"How to Apply These Terms to Your New Programs" in the full
|
||||
license text for more specific instructions.
|
||||
|
||||
Copyright 2024 Zen LM
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License");
|
||||
you may not use this file except in compliance with the License.
|
||||
You may obtain a copy of the License at
|
||||
|
||||
http://www.apache.org/licenses/LICENSE-2.0
|
||||
|
||||
Unless required by applicable law or agreed to in writing, software
|
||||
distributed under the License is distributed on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
See the License for the specific language governing permissions and
|
||||
limitations under the License.
|
||||
@@ -0,0 +1,44 @@
|
||||
# Pulsar Documentation
|
||||
|
||||
Documentation site for [Pulsar](https://github.com/luxfi/pulsar) — threshold ML-DSA-65, the NIST MPTC submission package by Lux Industries.
|
||||
|
||||
Built with [Hanzo Docs](https://docs.hanzo.ai) (fumadocs-based).
|
||||
|
||||
## Development
|
||||
|
||||
```bash
|
||||
pnpm install
|
||||
pnpm --filter=pulsar-docs dev # http://localhost:3008
|
||||
pnpm --filter=pulsar-docs build # static export to ./out
|
||||
```
|
||||
|
||||
## Structure
|
||||
|
||||
```
|
||||
apps/pulsar-docs/
|
||||
├── app/ Next.js app directory
|
||||
│ ├── (home)/ Landing page
|
||||
│ └── docs/ Documentation pages
|
||||
├── content/docs/ MDX content
|
||||
│ ├── index.mdx
|
||||
│ ├── getting-started.mdx
|
||||
│ ├── protocol/ 2-round threshold, FIPS 204, DKG, parameters
|
||||
│ ├── proofs/ EasyCrypt, Lean bridge, axiom inventory, extraction
|
||||
│ ├── reference/ API, KAT, interop
|
||||
│ ├── security.mdx
|
||||
│ ├── nist-mptc.mdx
|
||||
│ ├── postmortem.mdx
|
||||
│ └── changelog.mdx
|
||||
├── lib/ Utilities
|
||||
└── source.config.ts MDX configuration (KaTeX wired)
|
||||
```
|
||||
|
||||
## Source of truth
|
||||
|
||||
Content is authored from `~/work/lux/pulsar/main` (README, EasyCrypt README, Lean ↔ EC bridge, byte-walk roadmaps, BLOCKERS, CHANGELOG, SUBMISSION, SECURITY). Math is rendered with KaTeX.
|
||||
|
||||
## Links
|
||||
|
||||
- [GitHub: luxfi/pulsar](https://github.com/luxfi/pulsar)
|
||||
- [Spec PDF](https://github.com/luxfi/pulsar/blob/main/spec/pulsar.pdf)
|
||||
- [luxfi/corona — R-LWE sibling](https://github.com/luxfi/corona)
|
||||
@@ -0,0 +1,19 @@
|
||||
import { HomeLayout } from '@hanzo/docs-base-ui/layouts/home';
|
||||
import type { ReactNode } from 'react';
|
||||
|
||||
export default function Layout({ children }: { children: ReactNode }) {
|
||||
return (
|
||||
<HomeLayout
|
||||
nav={{
|
||||
title: 'Pulsar',
|
||||
url: '/',
|
||||
}}
|
||||
links={[
|
||||
{ text: 'Docs', url: '/docs' },
|
||||
{ text: 'GitHub', url: 'https://github.com/luxfi/pulsar' },
|
||||
]}
|
||||
>
|
||||
{children}
|
||||
</HomeLayout>
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,299 @@
|
||||
import Link from 'next/link';
|
||||
import { ArrowRight, ExternalLink, Github, BookOpen } from 'lucide-react';
|
||||
|
||||
export default function HomePage() {
|
||||
return (
|
||||
<main className="min-h-screen">
|
||||
{/* Hero */}
|
||||
<section className="relative border-b border-fd-border overflow-hidden">
|
||||
<div className="absolute inset-0 bg-gradient-to-b from-fd-primary/5 to-transparent pointer-events-none" />
|
||||
<div className="relative mx-auto max-w-4xl px-6 py-24 md:py-36 text-center">
|
||||
<div className="inline-flex items-center rounded-full border border-fd-border px-4 py-1.5 text-xs text-fd-muted-foreground mb-8 font-mono">
|
||||
NIST MPTC submission package
|
||||
</div>
|
||||
<h1 className="text-5xl md:text-7xl font-bold tracking-tight mb-6 leading-none">
|
||||
Pulsar
|
||||
</h1>
|
||||
<p className="text-lg md:text-xl text-fd-muted-foreground max-w-2xl mx-auto mb-4 leading-relaxed">
|
||||
Threshold ML-DSA-65.
|
||||
</p>
|
||||
<p className="text-base md:text-lg text-fd-muted-foreground max-w-3xl mx-auto mb-12 leading-relaxed">
|
||||
A 2-round threshold signing and DKG system whose per-party-aggregated
|
||||
signature is bit-identical to a single-party FIPS 204 ML-DSA
|
||||
signature on the same message and group public key.
|
||||
</p>
|
||||
<div className="flex flex-col sm:flex-row gap-4 justify-center mb-8">
|
||||
<Link
|
||||
href="/docs"
|
||||
className="inline-flex items-center justify-center gap-2.5 rounded-2xl bg-fd-primary px-8 py-4 text-base font-semibold text-fd-primary-foreground hover:opacity-90 transition shadow-lg"
|
||||
>
|
||||
<BookOpen className="h-5 w-5" />
|
||||
Read the docs
|
||||
</Link>
|
||||
<a
|
||||
href="https://github.com/luxfi/pulsar"
|
||||
target="_blank"
|
||||
rel="noopener noreferrer"
|
||||
className="inline-flex items-center justify-center gap-2.5 rounded-2xl border border-fd-border bg-fd-background px-8 py-4 text-base font-semibold hover:bg-fd-muted transition"
|
||||
>
|
||||
<Github className="h-5 w-5" />
|
||||
luxfi/pulsar
|
||||
</a>
|
||||
</div>
|
||||
<p className="text-sm text-fd-muted-foreground">
|
||||
Apache-2.0 · Module-LWE · targeting NIST MPTC Class N1 + N4
|
||||
</p>
|
||||
</div>
|
||||
</section>
|
||||
|
||||
{/* Headline claim */}
|
||||
<section className="mx-auto max-w-5xl px-6 py-20">
|
||||
<div className="grid md:grid-cols-3 gap-8">
|
||||
<FactCard
|
||||
label="Output interchange"
|
||||
title="Byte-equal to FIPS 204"
|
||||
body="Every signature produced by a Pulsar threshold ceremony verifies under unmodified FIPS 204 ML-DSA.Verify — same wire bytes, no verifier changes."
|
||||
/>
|
||||
<FactCard
|
||||
label="Trust footprint"
|
||||
title="22 named axioms"
|
||||
body="17 narrow implementation-refinement axioms (14 byte-walk + 1 codec round-trip + 2 honest-execution no-reject) plus 5 Lean-bridged algebraic axioms. Zero admits across 13 EasyCrypt files."
|
||||
/>
|
||||
<FactCard
|
||||
label="Side channels"
|
||||
title="Jasmin-CT blocking"
|
||||
body="Threshold layer (round1, round2, combine) is constant-time clean under the verified Jasmin compiler. libjade single-party ML-DSA-65 baseline is pinned."
|
||||
/>
|
||||
</div>
|
||||
</section>
|
||||
|
||||
{/* Quick navigation */}
|
||||
<section className="border-t border-fd-border bg-fd-muted/30">
|
||||
<div className="mx-auto max-w-5xl px-6 py-20">
|
||||
<div className="text-center mb-12">
|
||||
<h2 className="text-3xl font-bold tracking-tight mb-3">Start here</h2>
|
||||
<p className="text-fd-muted-foreground">
|
||||
The docs are sourced from the pulsar repository at HEAD.
|
||||
</p>
|
||||
</div>
|
||||
<div className="grid sm:grid-cols-2 lg:grid-cols-3 gap-4">
|
||||
<NavCard
|
||||
href="/docs/getting-started"
|
||||
title="Getting started"
|
||||
body="Install the Go reference, sign with a single party, then run a 3-of-5 threshold ceremony locally."
|
||||
/>
|
||||
<NavCard
|
||||
href="/docs/protocol/overview"
|
||||
title="Protocol"
|
||||
body="2-round threshold sketch, system model, FIPS 204 relationship, Pedersen DKG, parameter sets."
|
||||
/>
|
||||
<NavCard
|
||||
href="/docs/proofs/overview"
|
||||
title="Proofs"
|
||||
body="EasyCrypt theories, Lean Mathlib bridge, byte-walk extraction roadmaps, the 22-axiom inventory."
|
||||
/>
|
||||
<NavCard
|
||||
href="/docs/reference/api"
|
||||
title="Reference"
|
||||
body="Go API surface, KAT format, interoperability harness against cloudflare/circl and pq-crystals."
|
||||
/>
|
||||
<NavCard
|
||||
href="/docs/security"
|
||||
title="Security"
|
||||
body="Disclosure policy, in-scope vs out-of-scope findings, CVE assignment, MPTC public analysis."
|
||||
/>
|
||||
<NavCard
|
||||
href="/docs/nist-mptc"
|
||||
title="NIST MPTC"
|
||||
body="Cover sheet: what NIST receives, target dates (2026-Jul-20 preview, 2026-Nov-16 submission), how to evaluate."
|
||||
/>
|
||||
</div>
|
||||
</div>
|
||||
</section>
|
||||
|
||||
{/* Why */}
|
||||
<section className="mx-auto max-w-5xl px-6 py-20">
|
||||
<div className="text-center mb-12">
|
||||
<h2 className="text-3xl font-bold tracking-tight mb-3">Why threshold ML-DSA</h2>
|
||||
</div>
|
||||
<div className="space-y-6 max-w-3xl mx-auto text-fd-muted-foreground leading-relaxed">
|
||||
<p>
|
||||
NIST FIPS 204 (ML-DSA) is the only NIST-approved post-quantum
|
||||
digital signature in 2026. Threshold variants are not yet
|
||||
standardized; NIST's Multi-Party Threshold Cryptography project is
|
||||
collecting them now (IR 8214C, January 2026), with the first call
|
||||
package deadline expected 2026-Nov-16.
|
||||
</p>
|
||||
<p>
|
||||
Pulsar enters that process with a credible, output-interchangeable
|
||||
threshold ML-DSA candidate. The 2-round protocol skeleton is the
|
||||
same one Lux ships in production for Ring-LWE in luxfi/corona,
|
||||
retargeted to ML-DSA's polynomial-vector algebra. The resulting
|
||||
per-party-aggregated signature (under the v0.3 algebraic
|
||||
aggregator) is bit-identical to a single-party FIPS 204 ML-DSA
|
||||
signature on the same message and public key.
|
||||
</p>
|
||||
<p className="text-fd-foreground font-medium">
|
||||
The win, if Pulsar's Sign output is byte-equal to FIPS 204 Sign:
|
||||
threshold-produced signatures verify under unmodified FIPS 204
|
||||
verifiers, existing FIPS-validated ML-DSA modules consume Pulsar
|
||||
certs without code changes, and the threshold layer can be
|
||||
Class-N-claimed at NIST without a parallel algorithm standardization
|
||||
track.
|
||||
</p>
|
||||
</div>
|
||||
</section>
|
||||
|
||||
{/* Repository tour */}
|
||||
<section className="border-t border-fd-border bg-fd-muted/30">
|
||||
<div className="mx-auto max-w-5xl px-6 py-20">
|
||||
<div className="text-center mb-10">
|
||||
<h2 className="text-3xl font-bold tracking-tight mb-3">What ships in the submission</h2>
|
||||
<p className="text-fd-muted-foreground">
|
||||
The pulsar repository is the single canonical home for the
|
||||
submission: code, spec, proofs, KAT, tarball-cut tooling.
|
||||
</p>
|
||||
</div>
|
||||
<div className="rounded-xl border border-fd-border bg-fd-background overflow-hidden">
|
||||
<table className="w-full text-sm">
|
||||
<thead className="bg-fd-muted/50 border-b border-fd-border">
|
||||
<tr>
|
||||
<th className="text-left px-4 py-3 font-semibold">Element</th>
|
||||
<th className="text-left px-4 py-3 font-semibold">Location</th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody className="divide-y divide-fd-border">
|
||||
<RepoRow element="Technical specification" path="spec/pulsar.{tex,pdf}" />
|
||||
<RepoRow element="Reference implementation (Go)" path="ref/go/pkg/pulsar/" />
|
||||
<RepoRow element="KAT vectors" path="vectors/{dkg,keygen,sign,threshold-sign,verify}.json" />
|
||||
<RepoRow element="Class N1 interop harness" path="test/interoperability/n1_class_test.go" />
|
||||
<RepoRow element="EasyCrypt theories (13 files)" path="proofs/easycrypt/" />
|
||||
<RepoRow element="Lean ↔ EC bridge" path="proofs/lean-easycrypt-bridge.md" />
|
||||
<RepoRow element="Jasmin sources" path="jasmin/threshold/{round1,round2,combine}.jazz" />
|
||||
<RepoRow element="Constant-time evidence" path="ct/dudect/" />
|
||||
<RepoRow element="Lattice estimator scripts" path="estimator/" />
|
||||
<RepoRow element="Benchmark harness" path="bench/" />
|
||||
<RepoRow element="Per-push gate orchestrator" path="scripts/check-high-assurance.sh" />
|
||||
<RepoRow element="Tarball cut tool" path="scripts/cut-submission.sh" />
|
||||
</tbody>
|
||||
</table>
|
||||
</div>
|
||||
</div>
|
||||
</section>
|
||||
|
||||
{/* Footer */}
|
||||
<footer className="border-t border-fd-border">
|
||||
<div className="mx-auto max-w-6xl px-6 py-12">
|
||||
<div className="grid sm:grid-cols-2 lg:grid-cols-4 gap-8 mb-10">
|
||||
<div className="lg:col-span-2">
|
||||
<div className="text-lg font-bold mb-3">Pulsar</div>
|
||||
<p className="text-sm text-fd-muted-foreground mb-4 max-w-md">
|
||||
Threshold ML-DSA-65 by Lux Industries. Apache-2.0. Targeting
|
||||
NIST MPTC Class N1 (signing) + N4 (key generation).
|
||||
</p>
|
||||
<div className="flex gap-4 text-sm">
|
||||
<a
|
||||
href="https://github.com/luxfi/pulsar"
|
||||
target="_blank"
|
||||
rel="noopener noreferrer"
|
||||
className="text-fd-muted-foreground hover:text-fd-foreground inline-flex items-center gap-1"
|
||||
>
|
||||
<Github className="h-3.5 w-3.5" /> luxfi/pulsar
|
||||
</a>
|
||||
<a
|
||||
href="https://github.com/luxfi/corona"
|
||||
target="_blank"
|
||||
rel="noopener noreferrer"
|
||||
className="text-fd-muted-foreground hover:text-fd-foreground inline-flex items-center gap-1"
|
||||
>
|
||||
<ExternalLink className="h-3.5 w-3.5" /> luxfi/corona (R-LWE sibling)
|
||||
</a>
|
||||
</div>
|
||||
</div>
|
||||
<FooterColumn
|
||||
title="Read"
|
||||
links={[
|
||||
{ text: 'Getting started', href: '/docs/getting-started' },
|
||||
{ text: 'Protocol overview', href: '/docs/protocol/overview' },
|
||||
{ text: 'API reference', href: '/docs/reference/api' },
|
||||
{ text: 'KAT format', href: '/docs/reference/kat' },
|
||||
]}
|
||||
/>
|
||||
<FooterColumn
|
||||
title="Audit"
|
||||
links={[
|
||||
{ text: 'Axiom inventory', href: '/docs/proofs/axiom-inventory' },
|
||||
{ text: 'Lean ↔ EC bridge', href: '/docs/proofs/lean-bridge' },
|
||||
{ text: 'Security policy', href: '/docs/security' },
|
||||
{ text: 'NIST MPTC cover', href: '/docs/nist-mptc' },
|
||||
]}
|
||||
/>
|
||||
</div>
|
||||
<div className="flex flex-wrap items-center justify-between gap-4 border-t border-fd-border pt-6 text-xs text-fd-muted-foreground">
|
||||
<span>© 2026 Lux Industries, Inc. Apache-2.0.</span>
|
||||
<div className="flex gap-4">
|
||||
<a href="https://github.com/luxfi/pulsar/blob/main/LICENSE" target="_blank" rel="noopener noreferrer" className="hover:text-fd-foreground">License</a>
|
||||
<a href="https://github.com/luxfi/pulsar/blob/main/SECURITY.md" target="_blank" rel="noopener noreferrer" className="hover:text-fd-foreground">Security</a>
|
||||
</div>
|
||||
</div>
|
||||
</div>
|
||||
</footer>
|
||||
</main>
|
||||
);
|
||||
}
|
||||
|
||||
function FactCard({ label, title, body }: { label: string; title: string; body: string }) {
|
||||
return (
|
||||
<div className="rounded-xl border border-fd-border bg-fd-background p-6">
|
||||
<div className="text-[10px] font-semibold tracking-widest uppercase text-fd-primary mb-2">
|
||||
{label}
|
||||
</div>
|
||||
<h3 className="text-lg font-bold mb-3">{title}</h3>
|
||||
<p className="text-sm text-fd-muted-foreground leading-relaxed">{body}</p>
|
||||
</div>
|
||||
);
|
||||
}
|
||||
|
||||
function NavCard({ href, title, body }: { href: string; title: string; body: string }) {
|
||||
return (
|
||||
<Link
|
||||
href={href}
|
||||
className="group rounded-xl border border-fd-border bg-fd-background p-5 hover:bg-fd-muted/30 transition block"
|
||||
>
|
||||
<div className="flex items-start justify-between mb-2">
|
||||
<h3 className="font-semibold">{title}</h3>
|
||||
<ArrowRight className="h-4 w-4 text-fd-muted-foreground group-hover:translate-x-1 transition-transform" />
|
||||
</div>
|
||||
<p className="text-sm text-fd-muted-foreground leading-relaxed">{body}</p>
|
||||
</Link>
|
||||
);
|
||||
}
|
||||
|
||||
function RepoRow({ element, path }: { element: string; path: string }) {
|
||||
return (
|
||||
<tr>
|
||||
<td className="px-4 py-2.5">{element}</td>
|
||||
<td className="px-4 py-2.5 font-mono text-xs text-fd-muted-foreground">{path}</td>
|
||||
</tr>
|
||||
);
|
||||
}
|
||||
|
||||
function FooterColumn({ title, links }: { title: string; links: { text: string; href: string }[] }) {
|
||||
return (
|
||||
<div>
|
||||
<h4 className="font-semibold text-sm mb-3">{title}</h4>
|
||||
<ul className="space-y-2">
|
||||
{links.map((link) => (
|
||||
<li key={link.text}>
|
||||
<Link
|
||||
href={link.href}
|
||||
className="text-sm text-fd-muted-foreground hover:text-fd-foreground transition"
|
||||
>
|
||||
{link.text}
|
||||
</Link>
|
||||
</li>
|
||||
))}
|
||||
</ul>
|
||||
</div>
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,46 @@
|
||||
import { source } from '@/lib/source';
|
||||
import {
|
||||
DocsPage,
|
||||
DocsBody,
|
||||
DocsDescription,
|
||||
DocsTitle,
|
||||
} from '@hanzo/docs-ui/page';
|
||||
import { notFound } from 'next/navigation';
|
||||
import defaultMdxComponents from '@hanzo/docs-ui/mdx';
|
||||
|
||||
export default async function Page(props: {
|
||||
params: Promise<{ slug?: string[] }>;
|
||||
}) {
|
||||
const params = await props.params;
|
||||
const page = source.getPage(params.slug);
|
||||
if (!page) notFound();
|
||||
|
||||
const MDX = page.data.body;
|
||||
|
||||
return (
|
||||
<DocsPage toc={page.data.toc}>
|
||||
<DocsTitle>{page.data.title}</DocsTitle>
|
||||
<DocsDescription>{page.data.description}</DocsDescription>
|
||||
<DocsBody>
|
||||
<MDX components={{ ...defaultMdxComponents }} />
|
||||
</DocsBody>
|
||||
</DocsPage>
|
||||
);
|
||||
}
|
||||
|
||||
export async function generateStaticParams() {
|
||||
return source.generateParams();
|
||||
}
|
||||
|
||||
export async function generateMetadata(props: {
|
||||
params: Promise<{ slug?: string[] }>;
|
||||
}) {
|
||||
const params = await props.params;
|
||||
const page = source.getPage(params.slug);
|
||||
if (!page) notFound();
|
||||
|
||||
return {
|
||||
title: page.data.title,
|
||||
description: page.data.description,
|
||||
};
|
||||
}
|
||||
@@ -0,0 +1,21 @@
|
||||
import { DocsLayout } from '@hanzo/docs-ui/layouts/docs';
|
||||
import type { ReactNode } from 'react';
|
||||
import { source } from '@/lib/source';
|
||||
|
||||
export default function Layout({ children }: { children: ReactNode }) {
|
||||
return (
|
||||
<DocsLayout
|
||||
tree={source.pageTree}
|
||||
nav={{
|
||||
title: 'Pulsar',
|
||||
url: '/',
|
||||
}}
|
||||
links={[
|
||||
{ text: 'GitHub', url: 'https://github.com/luxfi/pulsar' },
|
||||
{ text: 'Spec PDF', url: 'https://github.com/luxfi/pulsar/blob/main/spec/pulsar.pdf' },
|
||||
]}
|
||||
>
|
||||
{children}
|
||||
</DocsLayout>
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,66 @@
|
||||
@import 'tailwindcss';
|
||||
@import '@hanzo/docs-base-ui/css/neutral.css';
|
||||
@import '@hanzo/docs-base-ui/css/preset.css';
|
||||
|
||||
@theme {
|
||||
/* ── Zen LM brand — purple, dark bg ───────────────────────── */
|
||||
--color-brand: #a855f7;
|
||||
--color-brand-foreground: #ffffff;
|
||||
--color-brand-hover: #9333ea;
|
||||
--color-brand-muted: rgba(168, 85, 247, 0.08);
|
||||
|
||||
--color-bg: #000000;
|
||||
--color-bg-card: rgba(10, 10, 10, 0.95);
|
||||
--color-bg-elevated: #111111;
|
||||
--color-border: rgba(255, 255, 255, 0.10);
|
||||
--color-text: #fafafa;
|
||||
--color-text-muted: #a3a3a3;
|
||||
--color-text-dim: #737373;
|
||||
|
||||
/* ── Fumadocs vars — monochrome base, purple primary ─────── */
|
||||
--color-fd-background: #000000;
|
||||
--color-fd-foreground: #fafafa;
|
||||
--color-fd-card: #0a0a0a;
|
||||
--color-fd-card-foreground: #fafafa;
|
||||
--color-fd-muted: #111111;
|
||||
--color-fd-muted-foreground: #8c8c8c;
|
||||
--color-fd-popover: #0d0d0d;
|
||||
--color-fd-popover-foreground: #f0f0f0;
|
||||
--color-fd-border: rgba(255, 255, 255, 0.10);
|
||||
--color-fd-primary: #a855f7;
|
||||
--color-fd-primary-foreground: #ffffff;
|
||||
--color-fd-secondary: #1a1a1a;
|
||||
--color-fd-secondary-foreground: #ebebeb;
|
||||
--color-fd-accent: rgba(168, 85, 247, 0.08);
|
||||
--color-fd-accent-foreground: #e5e5e5;
|
||||
--color-fd-ring: #a855f7;
|
||||
--color-fd-overlay: rgba(0, 0, 0, 0.5);
|
||||
|
||||
/* Neutralize warning/idea amber */
|
||||
--color-fd-warning: #a855f7;
|
||||
--color-fd-idea: #a855f7;
|
||||
--color-fd-info: #a855f7;
|
||||
--color-fd-error: #ef4444;
|
||||
--color-fd-success: #22c55e;
|
||||
}
|
||||
|
||||
html {
|
||||
scrollbar-gutter: stable;
|
||||
color-scheme: dark;
|
||||
}
|
||||
|
||||
body {
|
||||
background-color: var(--color-bg);
|
||||
color: var(--color-text);
|
||||
}
|
||||
|
||||
#nd-sidebar {
|
||||
--color-fd-muted: #1a1a1a;
|
||||
--color-fd-secondary: #1a1a1a;
|
||||
--color-fd-muted-foreground: #8c8c8c;
|
||||
}
|
||||
|
||||
::selection {
|
||||
background-color: rgba(168, 85, 247, 0.25);
|
||||
color: white;
|
||||
}
|
||||
@@ -0,0 +1,33 @@
|
||||
import './global.css';
|
||||
import 'katex/dist/katex.min.css';
|
||||
import type { Viewport } from 'next';
|
||||
import { baseUrl, createMetadata } from '@/lib/metadata';
|
||||
import { RootProvider } from '@hanzo/docs-base-ui/provider/next';
|
||||
import type { ReactNode } from 'react';
|
||||
|
||||
export const metadata = createMetadata({
|
||||
title: {
|
||||
template: '%s | Pulsar',
|
||||
default: 'Pulsar — Threshold ML-DSA-65',
|
||||
},
|
||||
description:
|
||||
'A 2-round threshold ML-DSA-65 signing and DKG system whose per-party-aggregated signature is bit-identical to a single-party FIPS 204 signature. NIST MPTC Class N1 + N4 submission package by Lux Industries.',
|
||||
metadataBase: baseUrl,
|
||||
});
|
||||
|
||||
export const viewport: Viewport = {
|
||||
themeColor: [
|
||||
{ media: '(prefers-color-scheme: dark)', color: '#0A0A0A' },
|
||||
{ media: '(prefers-color-scheme: light)', color: '#fff' },
|
||||
],
|
||||
};
|
||||
|
||||
export default function Layout({ children }: { children: ReactNode }) {
|
||||
return (
|
||||
<html lang="en" className="dark" suppressHydrationWarning>
|
||||
<body className="antialiased">
|
||||
<RootProvider>{children}</RootProvider>
|
||||
</body>
|
||||
</html>
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,43 @@
|
||||
import Link from 'next/link';
|
||||
|
||||
export default function NotFound() {
|
||||
return (
|
||||
<main className="flex min-h-screen flex-col items-center justify-center px-4 text-center">
|
||||
<p className="text-xs font-mono uppercase tracking-[0.3em] text-fd-muted-foreground mb-4">
|
||||
404
|
||||
</p>
|
||||
<h1 className="text-3xl font-semibold mb-3">Page not found</h1>
|
||||
<p className="text-fd-muted-foreground max-w-sm mb-10">
|
||||
That page doesn't exist or has moved. Try the documentation or head
|
||||
home.
|
||||
</p>
|
||||
|
||||
<div className="flex flex-wrap gap-3 justify-center">
|
||||
<Link
|
||||
href="/"
|
||||
className="inline-flex items-center gap-2 rounded-lg bg-fd-primary text-fd-primary-foreground px-4 py-2 text-sm font-medium hover:opacity-90 transition"
|
||||
>
|
||||
Go home
|
||||
</Link>
|
||||
<Link
|
||||
href="/docs"
|
||||
className="inline-flex items-center gap-2 rounded-lg border border-fd-border bg-fd-background px-4 py-2 text-sm font-medium hover:bg-fd-muted transition"
|
||||
>
|
||||
Documentation
|
||||
</Link>
|
||||
<a
|
||||
href="https://github.com/luxfi/pulsar"
|
||||
target="_blank"
|
||||
rel="noopener noreferrer"
|
||||
className="inline-flex items-center gap-2 rounded-lg border border-fd-border bg-fd-background px-4 py-2 text-sm font-medium hover:bg-fd-muted transition"
|
||||
>
|
||||
GitHub
|
||||
</a>
|
||||
</div>
|
||||
|
||||
<p className="mt-16 text-xs font-mono text-fd-muted-foreground opacity-50">
|
||||
pulsar — threshold ML-DSA-65
|
||||
</p>
|
||||
</main>
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,193 @@
|
||||
---
|
||||
title: Changelog
|
||||
description: Substantive changes to the EasyCrypt proof artifact, the spec, and the residual trust footprint.
|
||||
---
|
||||
|
||||
This page tracks substantive changes to the EasyCrypt proof artifact,
|
||||
the specification, and the residual trust footprint. For
|
||||
implementation-level changes see `git log` on the
|
||||
[`luxfi/pulsar`](https://github.com/luxfi/pulsar) repository.
|
||||
|
||||
For the full release-by-release file, see
|
||||
[`CHANGELOG.md` on GitHub](https://github.com/luxfi/pulsar/blob/main/CHANGELOG.md).
|
||||
|
||||
## v1.0.22 — AST regression guard hardening
|
||||
|
||||
Tag `29094a7`. Hardened `TestAlgebraic_NoSkAccess` to walk
|
||||
`*ast.SelectorExpr.Sel.Name` and `*ast.Ident`, so an indirect dispatch
|
||||
cannot bypass the banned-call check on `AlgebraicAggregate`. Closes the
|
||||
indirect-dispatch hole flagged during the v0.3 graduation sweep.
|
||||
|
||||
## v1.0.21 — v0.3 regression guard hardening (`km.a` NTT-domain invariant)
|
||||
|
||||
Tag `267ec04`. Pinned the FIPS 204 §3.5 `ExpandA` convention byte-for-byte
|
||||
against `cloudflare/[email protected]`:
|
||||
|
||||
- `TestAMatrix_IsAlreadyInNTTDomain` compares `km.a` at corners.
|
||||
- `TestCirclInternalShape_VsPulsar` mirrors circl's `PublicKey` via
|
||||
unsafe-pointer and asserts `km.a == pk.A`.
|
||||
|
||||
## v1.0.20 — Close PULSAR-V03-1 (v0.3 algebraic byte-equality)
|
||||
|
||||
Tag `023a3ed`. Fix `deriveKeyMaterial` in
|
||||
`ref/go/pkg/pulsar/mldsa_keyderive.go` to drop the spurious forward-NTT
|
||||
loop that double-rotated $\mathbf{A}$ after `polyDeriveUniform` had
|
||||
already sampled it directly into the NTT representation. v0.3 algebraic
|
||||
sign is now byte-equal to single-party `circl.mldsa65.Sign` on the
|
||||
Lagrange-reconstructed group secret.
|
||||
|
||||
Full root cause and graduation gate in [postmortem](/docs/postmortem).
|
||||
|
||||
## v1.0.14 — v0.2 honesty rename (Algebraic → Transitional)
|
||||
|
||||
The v0.2 API previously named `Algebraic*` was materially misleading:
|
||||
the file-header docstring claimed `AlgebraicCombine is a pure function
|
||||
of public-only material` while the implementation calls
|
||||
`mldsaSign(setup.SkBytes, message, ...)` against the master sk packed in
|
||||
`AlgebraicSetup.SkBytes`. The aggregator TCB at sign time was therefore
|
||||
identical to v0.1 reconstruct-and-sign — only the parties' side of the
|
||||
protocol was honestly algebraic.
|
||||
|
||||
v1.0.14 fixes the honesty defect without changing the algorithm.
|
||||
|
||||
### API rename (forward-only, no compat aliases)
|
||||
|
||||
- `AlgebraicThresholdSigner` → `TransitionalThresholdSigner`
|
||||
- `NewAlgebraicThresholdSigner` → `NewTransitionalThresholdSigner`
|
||||
- `AlgebraicCombine` → `TransitionalAggregate`
|
||||
- `AlgebraicSetup` → `TransitionalSetup`
|
||||
- `AlgebraicRound1Message` → `TransitionalRound1Message`
|
||||
- `AlgebraicRound2Message` → `TransitionalRound2Message`
|
||||
- `DealAlgebraicShares` → `DealTransitionalShares`
|
||||
- All `ErrAlg*` sentinels → `ErrTransitional*`
|
||||
- All `TestV02_*` test functions → `TestTransitional_*`
|
||||
|
||||
### Honesty docstrings rewritten
|
||||
|
||||
- `threshold_v02.go` file header now opens with HONEST SCOPE declaring
|
||||
the aggregator-side SkBytes dependency.
|
||||
- `TransitionalAggregate` docstring spells out the TCB equivalence with
|
||||
v0.1 at sign time.
|
||||
- `TransitionalSetup` docstring declares SkBytes as the v0.2 TCB defect
|
||||
and the v0.3 graduation gate.
|
||||
|
||||
### New load-bearing test
|
||||
|
||||
`TestTransitional_DependsOnSkBytes` — runs the full Round1/Round2 cycle
|
||||
then sets `setup.SkBytes = nil` and asserts `TransitionalAggregate`
|
||||
returns `ErrTransitionalNoSetup`. The test currently PASSES (because v0.2
|
||||
indeed depends on SkBytes). When v0.3 ships and removes the SkBytes
|
||||
dependency, this test starts FAILING — that failure is the load-bearing
|
||||
red flag documenting the v0.3 graduation.
|
||||
|
||||
The wire protocol is byte-for-byte unchanged: protocol constants
|
||||
(`PULSAR-ALG-*` customisation strings) are preserved so any existing v0.2
|
||||
test vectors continue to verify.
|
||||
|
||||
## v0.1.0 — proof-artifact progression (v4 → v13)
|
||||
|
||||
Target tag `submission-2026-11-16`.
|
||||
|
||||
| Version | Change | Trust-footprint effect |
|
||||
| --- | --- | --- |
|
||||
| v4 | byte-walk: factor through `pack_n1_signature` | Component-triple axioms with codec roundtrip in `Pulsar_N1.ec` |
|
||||
| v4b | per-stage split | 2 component-triple → 6 stage-level axioms |
|
||||
| v5 | c_tilde stage decomposition | `*_body_c_tilde_spec` → derived lemmas |
|
||||
| v6 | mu sub-stage decomposed via SHAKE/byte-layout | `*_body_mu_spec` → derived lemmas |
|
||||
| v7 | w1 sub-stage via HighBits structural split | `*_body_w1_spec` → derived lemmas |
|
||||
| v8 | combine z-stage via Lean Lagrange bridge | `combine_body_z_spec` → derived lemma; new Lean-bridged `threshold_partial_response_identity` |
|
||||
| v9 | `mu_shake_input_t = int list` concretization + 3-agent parallel close | `*_body_{mu_input,h}_spec` → derived lemmas |
|
||||
| v10 | full submission package: patents, axiom inventory, proof claims, FIPS traceability, TCB, NIST submission, evaluation | submission-grade documentation |
|
||||
| v11 | sign z-stage via $z = y + c \cdot s_1$ split + codec axiom elimination | `sign_body_z_spec` → derived lemma; **3 codec axioms ELIMINATED** |
|
||||
| v12 | w-stage via `ExpandA` + `ExpandMask` + `mat_vec_mul` structural split | `*_body_w_spec` × 2 → derived lemmas |
|
||||
| v13 | per-R1/R2/R3/R4 accept bridge axiom | +1 bridge axiom; connects bundled predicate to 4 per-R conditions |
|
||||
|
||||
### Derived lemmas added (previously primitive axioms)
|
||||
|
||||
After v10, the following primitive axioms have been **converted to
|
||||
derived lemmas** (the original obligation now follows from narrower
|
||||
sub-axioms + structural composition):
|
||||
|
||||
- v5: `{combine,sign}_body_c_tilde_spec`
|
||||
- v6: `{combine,sign}_body_mu_spec`
|
||||
- v7: `{combine,sign}_body_w1_spec`
|
||||
- v8: `combine_body_z_spec` (Lean-bridged)
|
||||
- v9: `{combine,sign}_body_mu_input_spec`
|
||||
- v10: `{combine,sign}_body_h_spec`
|
||||
- v11: `sign_body_z_spec` (z = y + c·s1 structural split)
|
||||
- v12: `{combine,sign}_body_w_spec` (A·y structural split)
|
||||
|
||||
Total: 14 axioms re-classified into derived lemmas across v5–v13.
|
||||
|
||||
### Actual axiom eliminations (v11 codec, real closure)
|
||||
|
||||
In addition to the 14 re-classifications, v11 delivered 3 PRIMITIVE
|
||||
AXIOM ELIMINATIONS in `Pulsar_N1_Signature_Codec.ec` (no replacement
|
||||
axiom on that path):
|
||||
|
||||
- `encode_decode_signature` (removed)
|
||||
- `decode_encode_signature_wf` (removed)
|
||||
- `encode_signature_wf` (kept, narrowed to a length-only axiom)
|
||||
- `encode_signature_len` → DERIVED via record-wrap structure
|
||||
|
||||
### Gate properties maintained throughout
|
||||
|
||||
- 13/13 EC files compile clean
|
||||
- jasmin-ct 3/3 blocking on threshold layer (round1, round2, combine)
|
||||
- Lean ↔ EC bridge guard 5/5
|
||||
- Admit budget 0/0
|
||||
- Lean bridge doc + check-script entry per bridged axiom
|
||||
- Refinement scaffold (no stray `declare axiom`) clean
|
||||
|
||||
### Submission documentation added (v10)
|
||||
|
||||
- `SUBMISSION.md` — NIST MPTC cover sheet
|
||||
- `docs/patents.md` — royalty-free patent grant + defensive termination
|
||||
- `docs/proof-axiom-inventory.md` — per-axiom residual trust accounting
|
||||
- `docs/proof-claims.md` — narrow EC/Lean refinement claim with explicit
|
||||
non-claims
|
||||
- `docs/fips-204-traceability.md` — op/lemma → FIPS 204 § map
|
||||
- `docs/tcb.md` — EC/Jasmin/OCaml/Lean TCB with per-layer risk
|
||||
- `docs/patent-claims.md` — numbered claim drafts for attorney review
|
||||
- `docs/evaluation.md` — experimental evaluation report per NIST IR 8214C
|
||||
§6
|
||||
|
||||
## Out-of-scope for v0.1
|
||||
|
||||
- Full κ-loop probabilistic Hoare model (multi-week)
|
||||
- Full bit-level FIPS 204 codec mechanization (multi-month,
|
||||
Barbosa–Barthe–Dupressoir scale)
|
||||
- Lean ↔ EC checked translation tooling (multi-month research)
|
||||
- ACVP/CAVP algorithm validation certificate (lab work)
|
||||
- FIPS 140-3 module validation (downstream)
|
||||
- Threshold SLH-DSA experimental profile (Tier 3, not in v0.1)
|
||||
- Production Rust / C / WASM implementations (Tier 1 priorities for v0.2+)
|
||||
- External cryptographic audit (engagement scheduled post-submission)
|
||||
|
||||
## What this submission DOES claim (precise)
|
||||
|
||||
> Under the trusted-computing base in `docs/tcb.md` and the residual
|
||||
> axioms enumerated in `docs/proof-axiom-inventory.md`, every signature
|
||||
> byte string produced by the Pulsar Combine procedure on inputs
|
||||
> satisfying the protocol's threshold-interpolation well-formedness
|
||||
> invariants is bit-identical to a signature produced by single-party
|
||||
> FIPS 204 ML-DSA-65 Sign on the Lagrange-reconstructed group secret.
|
||||
|
||||
This is an implementation-correctness result. It does NOT prove
|
||||
post-quantum hardness of ML-DSA itself; ML-DSA hardness is inherited
|
||||
from NIST FIPS 204's analysis.
|
||||
|
||||
## Known limitations
|
||||
|
||||
- No identifiable abort under network partition (synchronous only).
|
||||
- No 1-round signing (FIPS 204 rejection sampling precludes).
|
||||
- DKG bias resistance under collusion requires external randomness
|
||||
beacon.
|
||||
- v0.1 cross-committee reshare without external state binding is not
|
||||
supported.
|
||||
|
||||
## See also
|
||||
|
||||
- [Postmortem](/docs/postmortem) — closed-finding registry.
|
||||
- [Proofs overview](/docs/proofs/overview) — the three-prover stack.
|
||||
- [Axiom inventory](/docs/proofs/axiom-inventory) — the 22 named axioms.
|
||||
@@ -0,0 +1,194 @@
|
||||
---
|
||||
title: Getting started
|
||||
description: Install the Go reference, run a single-party FIPS 204 sign, then run a 3-of-5 threshold ceremony with byte-equal output.
|
||||
---
|
||||
|
||||
The reference implementation lives in `ref/go/pkg/pulsar/`. A single Go module
|
||||
serves as both the production library and the NIST MPTC submission artifact;
|
||||
the module path is `github.com/luxfi/pulsar`.
|
||||
|
||||
## Prerequisites
|
||||
|
||||
- Go 1.26 or newer (`go.mod` pins toolchain semantics; tested on 1.26.2).
|
||||
- `git`. Network egress is only required to clone — the submission tarball is
|
||||
self-contained and `vendor/` is populated.
|
||||
|
||||
Optional, for the high-assurance gate:
|
||||
|
||||
- EasyCrypt (source build, commit pinned by `.github/workflows/ci.yml`).
|
||||
- Jasmin compiler and `jasmin-ct` (`opam install jasmin`).
|
||||
- TeX Live or MacTeX for `spec/pulsar.pdf`.
|
||||
|
||||
The per-push gate skips any tool that isn't installed; Go-only contributors
|
||||
can keep moving without the proof-tool dependencies.
|
||||
|
||||
## Clone and build
|
||||
|
||||
```bash
|
||||
git clone https://github.com/luxfi/pulsar
|
||||
cd pulsar
|
||||
./scripts/build.sh
|
||||
```
|
||||
|
||||
`scripts/build.sh` builds the Go reference and (if TeX Live is present)
|
||||
`spec/pulsar.pdf`. It exits non-zero on any failure — reproducibility is the
|
||||
load-bearing CI invariant.
|
||||
|
||||
## Run the per-push gates
|
||||
|
||||
```bash
|
||||
./scripts/test.sh # Go unit + DD-007 linter + KAT replay + N1 interop
|
||||
./scripts/check-high-assurance.sh # Jasmin + EasyCrypt + Lean↔EC bridge guard
|
||||
```
|
||||
|
||||
Both finish under 60 seconds on a fresh clone. The unit suite includes:
|
||||
|
||||
- `TestN1_SinglePartySignatures_VerifyUnderFIPS204`
|
||||
- `TestN1_ThresholdSignatures_VerifyUnderFIPS204`
|
||||
- `TestN1_TamperedSignatures_Rejected`
|
||||
- `TestN1_WrongMessage_Rejected`
|
||||
|
||||
across `test/interoperability/n1_class_test.go` — 19 subtests vs.
|
||||
`cloudflare/circl` FIPS 204 verifier, all PASS.
|
||||
|
||||
## Single-party sign — sanity check
|
||||
|
||||
The single-party flow validates the Go reference against the FIPS 204
|
||||
specification without any threshold layer in the way.
|
||||
|
||||
```go
|
||||
package main
|
||||
|
||||
import (
|
||||
"fmt"
|
||||
|
||||
"github.com/luxfi/pulsar/ref/go/pkg/pulsar"
|
||||
)
|
||||
|
||||
func main() {
|
||||
seed := [48]byte{1, 2, 3 /* ... 48 bytes ... */}
|
||||
sk, pk, err := pulsar.KeyFromSeed(seed)
|
||||
if err != nil {
|
||||
panic(err)
|
||||
}
|
||||
|
||||
msg := []byte("hello, pulsar")
|
||||
sig, err := pulsar.Sign(sk, msg, nil) // nil ctx
|
||||
if err != nil {
|
||||
panic(err)
|
||||
}
|
||||
|
||||
ok := pulsar.Verify(pk, msg, nil, sig)
|
||||
fmt.Println("verify:", ok) // true
|
||||
}
|
||||
```
|
||||
|
||||
The signature `sig` is wire-identical to what `cloudflare/circl`'s
|
||||
`mldsa65.Sign` produces from the same seed and message. The byte-equality
|
||||
guard test
|
||||
[`TestN1_ByteEquality_*`](https://github.com/luxfi/pulsar/blob/main/ref/go/pkg/pulsar/n1_byte_equality_test.go)
|
||||
pins this property at HEAD.
|
||||
|
||||
## Threshold ceremony — 3-of-5
|
||||
|
||||
The v0.3 algebraic aggregator is the recommended path: aggregator-side TCB
|
||||
contains only public material, and the per-party-aggregated signature is
|
||||
bit-identical to a centralized FIPS 204 signature.
|
||||
|
||||
```go
|
||||
package main
|
||||
|
||||
import (
|
||||
"fmt"
|
||||
|
||||
"github.com/luxfi/pulsar/ref/go/pkg/pulsar"
|
||||
)
|
||||
|
||||
func main() {
|
||||
// DKG: 5-party Pedersen DKG over R_q^k, threshold t = 3.
|
||||
parties, groupPK, err := pulsar.DealAlgebraicShares(5, 3, sessionID)
|
||||
if err != nil {
|
||||
panic(err)
|
||||
}
|
||||
|
||||
msg := []byte("threshold-signed")
|
||||
ctx := []byte{}
|
||||
|
||||
// Round 1: per-party commitments.
|
||||
r1Msgs := make([]pulsar.AlgebraicRound1Message, len(parties))
|
||||
for i, p := range parties {
|
||||
r1Msgs[i], err = p.Round1(msg, ctx)
|
||||
if err != nil { panic(err) }
|
||||
}
|
||||
|
||||
// Round 2: per-party partial responses, conditioned on R1 transcript.
|
||||
r2Msgs := make([]pulsar.AlgebraicRound2Message, len(parties))
|
||||
for i, p := range parties {
|
||||
r2Msgs[i], err = p.Round2(r1Msgs)
|
||||
if err != nil { panic(err) }
|
||||
}
|
||||
|
||||
// Combine: public-only Lagrange aggregation, byte-equal to FIPS 204 Sign.
|
||||
sig, err := pulsar.AlgebraicAggregate(groupPK, msg, ctx, r1Msgs, r2Msgs)
|
||||
if err != nil {
|
||||
panic(err)
|
||||
}
|
||||
|
||||
ok := pulsar.Verify(groupPK, msg, ctx, sig)
|
||||
fmt.Println("verify:", ok) // true
|
||||
}
|
||||
```
|
||||
|
||||
The `AlgebraicAggregate` function has no `*PrivateKey`, no `SkBytes`, and no
|
||||
`seed` parameter — its public-BFT safety contract is enforced by a Go AST
|
||||
walk in `TestAlgebraic_NoSkAccess` that fails if any sk-bearing primitive is
|
||||
reachable from `AlgebraicAggregate`'s body, including indirect dispatch
|
||||
(hardened in v1.0.22).
|
||||
|
||||
## Cross-validate against FIPS 204
|
||||
|
||||
The interoperability harness verifies every Pulsar signature under three
|
||||
independent ML-DSA implementations:
|
||||
|
||||
1. The Pulsar reference itself (`luxfi/pulsar`).
|
||||
2. The FIPS 204 reference (`pq-crystals/dilithium`).
|
||||
3. A third independent implementation (`cloudflare/circl` FIPS 204 verifier;
|
||||
BoringSSL FIPS or OpenSSL 3.0 PQ provider when available).
|
||||
|
||||
```bash
|
||||
cd ref/go
|
||||
GOWORK=off go test -count=1 -short -timeout 300s ./pkg/pulsar/
|
||||
```
|
||||
|
||||
## Per-check scripts
|
||||
|
||||
For fast iteration on a specific gate:
|
||||
|
||||
```bash
|
||||
bash scripts/checks/ec-compile.sh # EasyCrypt compile
|
||||
bash scripts/checks/ec-admits.sh # admit budget enforced 0/0
|
||||
bash scripts/checks/ec-refinement-scaffold.sh # no stray declare axiom in scaffolds
|
||||
bash scripts/checks/jasmin.sh # jasminc + jasmin-ct
|
||||
bash scripts/check-lean-bridge.sh # Lean ↔ EC bridge guard
|
||||
bash scripts/checks/test/kat.sh # KAT replay
|
||||
bash scripts/checks/test/interop.sh # N1 interop suite
|
||||
bash scripts/checks/test/no-secret-logs.sh # DD-007 linter
|
||||
```
|
||||
|
||||
## Nightly (multi-hour)
|
||||
|
||||
Real-budget side-channel and fuzz coverage runs from the cron-scheduled
|
||||
`scripts/nightly.sh`:
|
||||
|
||||
- 1h-per-target Go native fuzz
|
||||
- 1h-per-target differential fuzz against cloudflare/circl
|
||||
- $10^9$-sample dudect per CT-relevant target
|
||||
|
||||
Results land in `ct/dudect/results/`.
|
||||
|
||||
## Next
|
||||
|
||||
- [Protocol overview](/docs/protocol/overview) — the 2-round threshold sketch.
|
||||
- [FIPS 204 relationship](/docs/protocol/fips-204) — what changes vs.
|
||||
single-party ML-DSA-65.
|
||||
- [API reference](/docs/reference/api) — exported types and functions.
|
||||
@@ -0,0 +1,121 @@
|
||||
---
|
||||
title: Pulsar
|
||||
description: Threshold ML-DSA-65 — a 2-round threshold signing and DKG system whose per-party-aggregated signature is bit-identical to a single-party FIPS 204 ML-DSA signature.
|
||||
---
|
||||
|
||||
Pulsar is the NIST MPTC submission package for **threshold ML-DSA-65**, the
|
||||
post-quantum digital signature standardized by FIPS 204. The submission targets
|
||||
**Class N1** (single-party-compatible threshold signing) and **Class N4**
|
||||
(multi-party key generation with public-key preservation across resharing).
|
||||
|
||||
The headline claim:
|
||||
|
||||
> Every signature produced by a Pulsar threshold ceremony
|
||||
> (DKG → Round-1 → Round-2 → Combine) is **bit-identical** to a signature
|
||||
> produced by single-party FIPS 204 ML-DSA-65 on the same message and group
|
||||
> public key.
|
||||
|
||||
A FIPS-validated ML-DSA verifier (BoringSSL FIPS, AWS-LC, OpenSSL 3.0 PQ
|
||||
provider) accepts a Pulsar signature without modification. Cross-validation
|
||||
against `cloudflare/circl` is wired into the per-push gate at
|
||||
`test/interoperability/n1_class_test.go` (19/19 N1 subtests PASS).
|
||||
|
||||
## At a glance
|
||||
|
||||
| Field | Value |
|
||||
| --- | --- |
|
||||
| Algorithm | Threshold ML-DSA-65 (Module-LWE, FIPS 204-aligned) |
|
||||
| Target NIST MPTC classes | **N1** (signing) + **N4** (DKG with public-key preservation) |
|
||||
| Round count | 2 rounds per signature |
|
||||
| Signature output | **Byte-identical** to single-party FIPS 204 ML-DSA-65 |
|
||||
| Underlying ring | $R_q = \mathbb{Z}_q[X] / (X^{256} + 1)$, $q = 8\,380\,417$ |
|
||||
| Hash family | SHAKE-256 / cSHAKE-256 / KMAC-256 / TupleHash-256 |
|
||||
| Repository | [luxfi/pulsar](https://github.com/luxfi/pulsar) |
|
||||
| License | Apache-2.0 |
|
||||
| Submission tag | `submission-2026-11-16` (cut from `main` at NIST deadline) |
|
||||
|
||||
## 90-second pitch
|
||||
|
||||
NIST FIPS 204 (ML-DSA) is the only NIST-approved post-quantum digital signature
|
||||
in 2026. NIST's Multi-Party Threshold Cryptography project is collecting
|
||||
threshold variants now (IR 8214C, January 2026; first call package deadline
|
||||
expected 2026-Nov-16).
|
||||
|
||||
Pulsar's 2-round threshold protocol skeleton is the same one Lux ships in
|
||||
production for Ring-LWE in [`luxfi/corona`](https://github.com/luxfi/corona),
|
||||
retargeted to ML-DSA's polynomial-vector-over-$R_q^k$ algebra. The
|
||||
per-party-aggregated signature (under the v0.3 algebraic aggregator) is
|
||||
bit-identical to a single-party FIPS 204 ML-DSA signature on the same message
|
||||
and public key — no verifier modifications, no new validation track.
|
||||
|
||||
Two aggregator variants ship in the same module:
|
||||
|
||||
- **v0.3 algebraic** (`AlgebraicAggregate` in `ref/go/pkg/pulsar/threshold_v03.go`)
|
||||
— public-only material at sign time; no master-secret reconstruction. **This is
|
||||
the N1 submission target.**
|
||||
- **v0.2 transitional** (`TransitionalAggregate` in `threshold_v02.go`) —
|
||||
reconstructs the master ML-DSA secret in aggregator memory and calls
|
||||
`mldsaSign(setup.SkBytes, ...)`. Output byte-equality holds, but the TCB at
|
||||
sign time includes the aggregator. Documented for protocol-evolution
|
||||
traceability; not the recommended deployment.
|
||||
|
||||
## Quickstart
|
||||
|
||||
A fresh clone runs the full per-push submission gate in under 60 seconds.
|
||||
|
||||
```bash
|
||||
git clone https://github.com/luxfi/pulsar
|
||||
cd pulsar
|
||||
./scripts/build.sh # Go ref + spec PDF
|
||||
./scripts/test.sh # Go unit + DD-007 linter + KAT replay + N1 interop
|
||||
./scripts/gen_vectors.sh # deterministic KAT regen
|
||||
./scripts/check-high-assurance.sh # Jasmin + EasyCrypt + Lean↔EC bridge guard
|
||||
./scripts/bench.sh # signing / verification benchmarks
|
||||
```
|
||||
|
||||
Each per-push script is an **orchestrator** sequencing per-check scripts under
|
||||
`scripts/checks/`. Per-check scripts are independently runnable for fast
|
||||
iteration:
|
||||
|
||||
```bash
|
||||
bash scripts/checks/ec-compile.sh # just the EC compile gate
|
||||
bash scripts/checks/jasmin.sh # just jasminc + jasmin-ct
|
||||
bash scripts/checks/test/kat.sh # just KAT replay
|
||||
```
|
||||
|
||||
Per-push gates run real-budget checks only. The 1h-per-target fuzz +
|
||||
$10^9$-sample dudect runs live in the cron-scheduled `scripts/nightly.sh`.
|
||||
|
||||
## Where to start
|
||||
|
||||
- [Getting started](/docs/getting-started) — install, single-party sign,
|
||||
threshold ceremony.
|
||||
- [Protocol overview](/docs/protocol/overview) — 2-round sketch, system model,
|
||||
the byte-equality argument.
|
||||
- [FIPS 204 relationship](/docs/protocol/fips-204) — what changes vs.
|
||||
single-party ML-DSA-65; why aggregation is wire-shape-preserving.
|
||||
- [Proofs overview](/docs/proofs/overview) — EasyCrypt + Lean + Jasmin tracks,
|
||||
what's mechanized vs. axiomatic.
|
||||
- [Axiom inventory](/docs/proofs/axiom-inventory) — the canonical list of 22
|
||||
named axioms with file:line in EC and Lean.
|
||||
- [Reference API](/docs/reference/api) — exported Go types and functions from
|
||||
`ref/go/pkg/pulsar`.
|
||||
- [KAT format](/docs/reference/kat) — vector schema, regeneration, cross-impl
|
||||
validation.
|
||||
- [Security policy](/docs/security) — disclosure, CVE assignment, MPTC public
|
||||
analysis window.
|
||||
- [NIST MPTC cover](/docs/nist-mptc) — submission cover sheet, target dates,
|
||||
what NIST reviewers should read first.
|
||||
|
||||
## Related libraries
|
||||
|
||||
| Repository | Lattice basis | Role |
|
||||
| --- | --- | --- |
|
||||
| [luxfi/pulsar](https://github.com/luxfi/pulsar) | Module-LWE ($R_q^k$) | This NIST MPTC submission package. |
|
||||
| [luxfi/corona](https://github.com/luxfi/corona) | Ring-LWE ($R_q$) | Production R-LWE threshold ML-DSA library — same 2-round skeleton, different lattice. |
|
||||
|
||||
Pulsar and Corona are independent libraries with no shared types. A downstream
|
||||
consumer may combine the two as a **Double Lattice** PQ pair so a break in one
|
||||
lattice family does not break finality — that layered combination is the
|
||||
consumer's design choice and is not part of this submission. Pulsar stands
|
||||
alone as an MPTC Class N1 + N4 candidate.
|
||||
@@ -0,0 +1,18 @@
|
||||
{
|
||||
"title": "Pulsar",
|
||||
"pages": [
|
||||
"index",
|
||||
"getting-started",
|
||||
"---Protocol---",
|
||||
"protocol",
|
||||
"---Reference---",
|
||||
"reference",
|
||||
"---Proofs---",
|
||||
"proofs",
|
||||
"---Submission---",
|
||||
"security",
|
||||
"nist-mptc",
|
||||
"postmortem",
|
||||
"changelog"
|
||||
]
|
||||
}
|
||||
@@ -0,0 +1,198 @@
|
||||
---
|
||||
title: NIST MPTC cover
|
||||
description: Submission cover sheet — what NIST receives, target dates, how to evaluate.
|
||||
---
|
||||
|
||||
This page is the public face of the NIST MPTC submission. For the
|
||||
authoritative cover sheet shipped with the submission tarball, see
|
||||
[`SUBMISSION.md` in the repository](https://github.com/luxfi/pulsar/blob/main/SUBMISSION.md).
|
||||
|
||||
## At a glance
|
||||
|
||||
| Field | Value |
|
||||
| --- | --- |
|
||||
| Submission name | **Pulsar** |
|
||||
| Submitting organisation | Lux Industries, Inc. |
|
||||
| Algorithm | Threshold ML-DSA-65 (Module-LWE, FIPS 204-aligned) |
|
||||
| Target NIST MPTC classes | **N1** (single-party-compatible threshold signing) + **N4** (multi-party key generation with public-key preservation across resharing) |
|
||||
| Underlying primitive | FIPS 204 ML-DSA-65 |
|
||||
| Round count | 2 rounds per signature |
|
||||
| Signature output | **Byte-identical** to single-party FIPS 204 ML-DSA-65 |
|
||||
| Repository | [luxfi/pulsar](https://github.com/luxfi/pulsar) |
|
||||
| Spec PDF | [`spec/pulsar.pdf`](https://github.com/luxfi/pulsar/blob/main/spec/pulsar.pdf) (built via `scripts/build.sh`) |
|
||||
| License | Apache-2.0 |
|
||||
| Patent posture | Royalty-free grant ([`docs/patents.md`](https://github.com/luxfi/pulsar/blob/main/docs/patents.md)) |
|
||||
| Tier | **Tier 1** — Threshold ML-DSA-65 (this submission). Tier 2 — SLH-DSA single-party compat (consumes FIPS 205 directly). Tier 3 — Threshold SLH-DSA, research-only. |
|
||||
|
||||
## Headline claim
|
||||
|
||||
> Every signature produced by a Pulsar threshold ceremony
|
||||
> (DKG → Round-1 → Round-2 → Combine) is **bit-identical** to a signature
|
||||
> produced by single-party FIPS 204 ML-DSA-65 on the same message and
|
||||
> group public key.
|
||||
|
||||
A FIPS-validated ML-DSA verifier (BoringSSL FIPS, AWS-LC, OpenSSL 3.0 PQ
|
||||
provider) accepts a Pulsar signature without modification.
|
||||
|
||||
### Two-variant disclosure
|
||||
|
||||
The submission ships **both**:
|
||||
|
||||
- The **v0.1 reveal-and-aggregate flow** — the runnable Go reference +
|
||||
KAT vectors + 19/19 N1 interop subtests.
|
||||
- The **v0.2 FSwA Lagrange-linearity flow** — the Jasmin sources
|
||||
type-check against this; the EasyCrypt N1 reduction is stated against
|
||||
this.
|
||||
|
||||
Both variants produce a FIPS 204 byte-equal $\sigma = (\tilde{c},
|
||||
\mathbf{z}, \mathbf{h})$. The v0.1 path carries a documented
|
||||
reconstruction-aggregator trust caveat; v0.2 avoids the reconstruction
|
||||
via Lagrange-linearity but is not yet the reference runtime.
|
||||
|
||||
The Class N1 byte-equality theorem in EasyCrypt is stated and proved
|
||||
against the centralized recovery model; both wire variants emit
|
||||
$\sigma = (\tilde{c}, \mathbf{z}, \mathbf{h})$ byte-equal to single-party
|
||||
FIPS 204.
|
||||
|
||||
### Theorem framing — accepted-path correctness
|
||||
|
||||
The Class N1 byte-equality theorem is **conditional on acceptance**:
|
||||
*if* the threshold combine (and the single-party comparator) accepts —
|
||||
i.e., passes the ML-DSA norm and rejection checks and the kappa
|
||||
rejection-sampling loop converged — *then* the produced byte string
|
||||
equals the centralized ML-DSA-65 signature on the same protocol-level
|
||||
inputs, under the stated layout, algebraic, and byte-walk assumptions.
|
||||
|
||||
ML-DSA rejection sampling remains probabilistic per FIPS 204; the
|
||||
deterministic EC model captures the accepted-path conditioning via the
|
||||
`accept_signing_attempt` predicate rather than via probabilistic Hoare
|
||||
logic.
|
||||
|
||||
## Target dates
|
||||
|
||||
| Date | Event |
|
||||
| --- | --- |
|
||||
| 2026-Jul-20 | NIST third preview deadline — preview writeup |
|
||||
| **2026-Nov-16** | NIST first call package submission — `submission-2026-11-16` tag cut from `main` |
|
||||
|
||||
## What NIST receives
|
||||
|
||||
The tarball includes:
|
||||
|
||||
- `SUBMISSION.md` — this cover sheet (extended).
|
||||
- `README.md` — repository layout, reproduction commands.
|
||||
- `LICENSE` — Apache-2.0.
|
||||
- `SECURITY.md` — threat model + responsible disclosure.
|
||||
- `CONTRIBUTING.md` — external-contribution policy.
|
||||
- `spec/pulsar.{tex,pdf}` — full algorithm specification (1633-line
|
||||
LaTeX, 577 KB PDF).
|
||||
- `ref/go/pkg/pulsar/` — canonical Go reference implementation (83.9%
|
||||
statement coverage).
|
||||
- `vectors/{dkg,keygen,sign,threshold-sign,verify}.json` — KAT vectors,
|
||||
deterministic from seed.
|
||||
- `test/interoperability/` — cross-validation harness (19/19 N1
|
||||
subtests PASS).
|
||||
- `proofs/easycrypt/` — 13 EasyCrypt files, 0/0 admits, 22 axioms.
|
||||
- `proofs/lean-easycrypt-bridge.md` — Lean↔EC bridge correspondence.
|
||||
- `ct/dudect/` — constant-time analysis (results in
|
||||
`ct/dudect/results/`).
|
||||
- `jasmin/` — high-assurance Jasmin sources (libjade pinned at
|
||||
`9426b32`; ~2600 lines of threshold layer).
|
||||
- `bench/results/REPORT.md` — performance evaluation (M1 Max, Go 1.26.2,
|
||||
KeyGen / Sign / Verify medians per parameter set).
|
||||
- `docs/patent-notes-draft.md`, `docs/patents.md` — patent posture.
|
||||
- `scripts/` — build, test, vector generation, cut tooling.
|
||||
|
||||
## What to read first
|
||||
|
||||
A NIST reviewer with limited time should read in this order:
|
||||
|
||||
1. **`SUBMISSION.md`** — cover sheet, metadata, headline claim.
|
||||
2. **`spec/pulsar.pdf`** — full algorithm specification.
|
||||
3. **`docs/proof-claims.md`** — what's proved vs. what's not (narrow
|
||||
claim).
|
||||
4. **`docs/proof-axiom-inventory.md`** — residual EC trust base, per-axiom
|
||||
closure plan ([rendered here](/docs/proofs/axiom-inventory)).
|
||||
5. **`docs/tcb.md`** — EC/Jasmin/OCaml TCB.
|
||||
6. **`docs/fips-204-traceability.md`** — op/lemma → FIPS 204 § map.
|
||||
7. **`docs/evaluation.md`** — performance + correctness + CT + sec-param
|
||||
evidence.
|
||||
8. **`docs/patents.md`** — royalty-free patent grant text.
|
||||
9. **`README.md`** — repository layout and how to reproduce.
|
||||
10. **`vectors/README.md`** — KAT format + cross-validation gates
|
||||
([rendered here](/docs/reference/kat)).
|
||||
11. **[`BLOCKERS.md`](https://github.com/luxfi/pulsar/blob/main/BLOCKERS.md)**
|
||||
— what the construction does NOT claim. Load-bearing entries:
|
||||
"Spec ↔ Go-reference protocol drift" (two-variant submission
|
||||
disclosure), "Class N1 byte-equal output" (v0.1 aggregator trust
|
||||
caveat), "EUF-CMA under adaptive corruption" (static-corruption
|
||||
only in v0.1).
|
||||
12. **`docs/cryptographer-sign-off.md`** — independent cryptographer
|
||||
review (APPROVED WITH GATES) covering construction soundness, proof-
|
||||
artifact verification, test surface, and pre-publish disclosure
|
||||
gates.
|
||||
|
||||
## What to run
|
||||
|
||||
The reproducibility gate is `scripts/build.sh` against the tarball
|
||||
extract — the entire submission is self-contained, so no network access
|
||||
is required:
|
||||
|
||||
```bash
|
||||
tar xzf submission-YYYY-MM-DD.tar.gz
|
||||
cd pulsar
|
||||
scripts/build.sh # builds Go ref + spec PDF
|
||||
scripts/test.sh # runs unit + KAT + interoperability tests
|
||||
scripts/bench.sh # produces signature/verification benchmarks
|
||||
scripts/gen_vectors.sh # regenerates KAT vectors (deterministic)
|
||||
```
|
||||
|
||||
`scripts/build.sh` exits non-zero on any failure. CI runs the same
|
||||
script on every commit; the reproducibility property is the load-bearing
|
||||
one for the submission.
|
||||
|
||||
## Class N1 — output interchangeability
|
||||
|
||||
The N1 claim is asserted at four levels of evidence:
|
||||
|
||||
| Evidence | Where |
|
||||
| --- | --- |
|
||||
| Algorithmic argument | `spec/pulsar.tex` §6, Theorem 6.1 |
|
||||
| Symbolic / Lean proof | `~/work/lux/proofs/lean/Crypto/Pulsar/OutputInterchange.lean` |
|
||||
| Test harness | `test/interoperability/` runs every KAT through 3 independent verifiers |
|
||||
| Cross-implementation KATs | `vectors/sign.json` shares vectors with FIPS 204 reference |
|
||||
|
||||
## Class N4 — public-key preservation across resharing
|
||||
|
||||
Multi-party proactive resharing preserves the group public key across
|
||||
committee rotations (epoch boundaries), so a single long-lived public
|
||||
identity persists while the secret-share custodians rotate.
|
||||
|
||||
| Evidence | Where |
|
||||
| --- | --- |
|
||||
| Algorithmic argument | `spec/pulsar.tex` §4.5 (Reshare protocol) |
|
||||
| Symbolic / Lean proof | `~/work/lux/proofs/lean/Crypto/Pulsar/Shamir.lean` |
|
||||
| Test harness | `vectors/transcripts/n*-t*-reshare.jsonl` carry pre/post-reshare public keys + verify both verify under unmodified ML-DSA |
|
||||
|
||||
## Comparison to related submissions
|
||||
|
||||
| Submission | Round count | Output interchange | Underlying lattice |
|
||||
| --- | --- | --- | --- |
|
||||
| **Pulsar** (this) | 2 | Byte-equal to FIPS 204 ML-DSA | Module-LWE |
|
||||
| Lux Corona (R-LWE sibling) | 2 | Byte-equal to FIPS 204 ML-DSA | Ring-LWE |
|
||||
| Raccoon | 3 | Compatible verification | Module-LWE |
|
||||
| Corona (upstream academic) | 2 | Not interchange-tested at submission time | R-LWE |
|
||||
|
||||
## Contact
|
||||
|
||||
- Primary: `[email protected]` (Lux Industries, Inc.)
|
||||
- Submission coordination: `[email protected]`
|
||||
- Security disclosure: see [security policy](/docs/security)
|
||||
- Public discussion: [github.com/luxfi/pulsar/discussions](https://github.com/luxfi/pulsar/discussions)
|
||||
|
||||
## Reproducibility commitment
|
||||
|
||||
The build, test, vector-generation, and benchmark scripts are
|
||||
deterministic from a 48-byte seed. A reviewer reproducing the submission
|
||||
tarball from `submission-YYYY-MM-DD` should obtain byte-identical
|
||||
artifacts. Drift is a build bug — please open an issue.
|
||||
@@ -0,0 +1,136 @@
|
||||
---
|
||||
title: Postmortem
|
||||
description: Closed-finding registry — v1.0.20 ExpandA-convention fix that closed PULSAR-V03-1 (the v0.3 algebraic-sign byte-equality bug).
|
||||
---
|
||||
|
||||
This page is the closed-finding registry. New findings open under the
|
||||
`Open` section in [`BLOCKERS.md`](https://github.com/luxfi/pulsar/blob/main/BLOCKERS.md);
|
||||
on fix they move to `Closed` with commit + tag. IDs are cited from
|
||||
source-code comments and from `docs/cryptographer-sign-off.md`,
|
||||
`docs/deployment.md`, `SUBMISSION.md`, `spec/blockers.tex`.
|
||||
|
||||
## Status
|
||||
|
||||
**Submission-ready. No open items.**
|
||||
|
||||
Earlier IDs `CR-6` / `CR-7` / `CR-8` (KEM-wrap of DKG envelopes, ephemeral
|
||||
per-pair session keys, identity-bound MAC layer) survive only as
|
||||
source-code references. They closed in the luxfi/pulsar-mptc →
|
||||
luxfi/pulsar consolidation (commit `7be057b`, v1.0.7 sign-off); the
|
||||
canonical narrative lives in `CHANGELOG.md` and the v1.0.7 sign-off.
|
||||
|
||||
## PULSAR-V03-1 — v0.3 algebraic sign byte-equality
|
||||
|
||||
**Status**: CLOSED in v1.0.20 (commit `023a3ed`).
|
||||
**Regression-guard hardening**: v1.0.21 (`267ec04`), v1.0.22 (`29094a7`).
|
||||
**Owner**: cryptographer.
|
||||
|
||||
### Root cause
|
||||
|
||||
`deriveKeyMaterial` in `ref/go/pkg/pulsar/mldsa_keyderive.go` was
|
||||
applying a spurious forward NTT to the public matrix $\mathbf{A}$ AFTER
|
||||
sampling it via `polyDeriveUniform`:
|
||||
|
||||
```go
|
||||
// BEFORE (buggy, v1.0.19 and earlier), per (i,j) over K×L:
|
||||
polyDeriveUniform(&km.a[i][j], &km.rho, ...) // already NTT-domain
|
||||
// ... later, separate K×L pass over the same matrix:
|
||||
km.a[i][j].ntt() // EXTRA NTT — wrong
|
||||
```
|
||||
|
||||
Per FIPS 204 §3.5 Algorithm 32 (`ExpandA`), $\mathbf{A}$ is sampled
|
||||
**directly** into the NTT representation; no separate forward-NTT step
|
||||
exists. `polyDeriveUniform` is exactly that algorithm — byte-identical
|
||||
to `cloudflare/[email protected]`'s `PolyDeriveUniform`. The post-step
|
||||
produced double-NTT'd values.
|
||||
|
||||
### Why the bug was invisible before v0.3
|
||||
|
||||
- **v0.1** calls `circl.SignTo`, which maintains its own
|
||||
$\mathbf{A}$ — never touches the contaminated `km.a`.
|
||||
- **v0.2** emits via `circl.SignTo(setup.SkBytes, ...)`; the wrong
|
||||
$\mathbf{A}$ only entered transcript-level commits, which are
|
||||
self-consistent across parties.
|
||||
- **Keygen** consumes `km.a` BEFORE the spurious NTT step (in
|
||||
$\mathbf{t} = \mathbf{A} \mathbf{s}_1 + \mathbf{s}_2$), so the public
|
||||
key matched circl byte-for-byte. Only the post-step contaminated the
|
||||
cached `km.a` that v0.3 sign later consumed as `setup.A`.
|
||||
|
||||
v0.3 was the first mode that propagated the wrong $\mathbf{A}$ all the
|
||||
way to the output signature.
|
||||
|
||||
### Fix
|
||||
|
||||
Drop the post-sample NTT loop in `deriveKeyMaterial`. The same redundant
|
||||
`.ntt()` in `manualVerifyOnce` (`threshold_v03_bytediff_test.go`) and in
|
||||
`TestPrimDiff_VerifyPipeline_OnCirclSig` was removed.
|
||||
|
||||
Regression guards pin the convention byte-for-byte against circl's
|
||||
stored `pk.A`:
|
||||
|
||||
- `TestAMatrix_IsAlreadyInNTTDomain` compares `km.a` (the previously-
|
||||
contaminated field) at corners `[0][0]` and `[K-1][L-1]`.
|
||||
- `TestCirclInternalShape_VsPulsar` mirrors circl's `PublicKey` via
|
||||
unsafe-pointer and asserts `km.a == pk.A`.
|
||||
|
||||
v1.0.22 hardened the AST guard in `TestAlgebraic_NoSkAccess` to walk
|
||||
`*ast.SelectorExpr.Sel.Name` and `*ast.Ident`, so an indirect dispatch
|
||||
(`var fn = polyDeriveUniformLeqEta; fn(...)`) cannot bypass the
|
||||
banned-call check on `AlgebraicAggregate`.
|
||||
|
||||
### Graduation gate
|
||||
|
||||
All currently TRUE on the tip of `main` at v1.0.22:
|
||||
|
||||
1. `TestAlgebraic_FullCycle_n5_t3` PASS — v0.3 sig verifies under
|
||||
stock `mldsa65.Verify`.
|
||||
2. `TestAlgebraic_NoSkAccess` PASS — public-BFT safety contract:
|
||||
`AlgebraicAggregate` has no `*PrivateKey`/`SkBytes`/`seed`
|
||||
parameter; AST walks confirm no sk-bearing primitive is reachable
|
||||
from its body (including indirect dispatch).
|
||||
3. `TestAMatrix_IsAlreadyInNTTDomain` and
|
||||
`TestCirclInternalShape_VsPulsar` PASS — byte-equality vs circl
|
||||
`pk.A`.
|
||||
4. `TestTransitional_DependsOnSkBytes` PASS — v0.2 still declares
|
||||
its `SkBytes` dependency honestly. (The original gate expected this
|
||||
to FAIL on the assumption v0.2 would be edited in place; the actual
|
||||
closure shipped v0.3 as a parallel track and left v0.2 honest. Both
|
||||
paths now coexist.)
|
||||
5. Class N1 byte-equality preserved: `TestN1_ByteEquality_*` PASS.
|
||||
6. Full suite green under `-race`:
|
||||
`cd ref/go && GOWORK=off go test -count=1 -short -timeout 300s ./pkg/pulsar/`.
|
||||
|
||||
### Lessons
|
||||
|
||||
- **Cross-impl byte-walks catch convention drift early.** The
|
||||
`TestN1_ByteEquality_*` and `TestCirclInternalShape_VsPulsar` tests
|
||||
pinned the FIPS 204 convention against `cloudflare/[email protected]`. The
|
||||
v0.3 cycle stopped byte-matching the moment the spurious post-sample
|
||||
NTT silently double-rotated the matrix — the regression surface was
|
||||
obvious and the diagnosis went from `git bisect` to root cause in
|
||||
hours rather than days.
|
||||
- **AST guards prevent invariant erosion.** The
|
||||
`TestAlgebraic_NoSkAccess` AST walk is a stronger contract than a
|
||||
comment that says "this function must not see SkBytes". v1.0.22's
|
||||
hardening (walking `SelectorExpr.Sel.Name` and `*ast.Ident`) prevents
|
||||
indirect dispatch — a future refactor cannot accidentally re-introduce
|
||||
the v0.2 reconstruction defect in v0.3 territory.
|
||||
- **Two-variant disclosure works.** Keeping v0.2 alive as a documented
|
||||
transitional aggregator made the v0.3 graduation surface visible
|
||||
rather than hidden. The `TestTransitional_DependsOnSkBytes` gate
|
||||
documents the contract publicly.
|
||||
|
||||
### Source pointers
|
||||
|
||||
- `ref/go/pkg/pulsar/mldsa_keyderive.go` — fixed `deriveKeyMaterial`.
|
||||
- `ref/go/pkg/pulsar/threshold_v03_bytediff_test.go` — removed redundant
|
||||
`manualVerifyOnce` `.ntt()`.
|
||||
- `ref/go/pkg/pulsar/threshold_v03_*_test.go` — regression tests.
|
||||
- `BLOCKERS.md` §Closed — original closure record.
|
||||
|
||||
## See also
|
||||
|
||||
- [BLOCKERS.md](https://github.com/luxfi/pulsar/blob/main/BLOCKERS.md) —
|
||||
authoritative closed-finding registry.
|
||||
- [CHANGELOG](/docs/changelog) — release-by-release narrative.
|
||||
- [Security policy](/docs/security) — disclosure and CVE assignment.
|
||||
@@ -0,0 +1,162 @@
|
||||
---
|
||||
title: Axiom inventory
|
||||
description: The canonical 22 named axioms in the extracted N1 byte-equality theorem's dependency cone, with file:line citations and closure paths.
|
||||
---
|
||||
|
||||
The extracted Class N1 byte-equality theorem
|
||||
`pulsar_n1_byte_equality_extracted` in
|
||||
`proofs/easycrypt/Pulsar_N1_Extracted.ec` reduces to **22 named axioms**.
|
||||
Each axiom is cited inline with its EasyCrypt location, with closure-path
|
||||
notes and (for the Lean-bridged five) a pointer to the discharging Lean
|
||||
theorem.
|
||||
|
||||
## At a glance
|
||||
|
||||
| Category | Count |
|
||||
| --- | ---: |
|
||||
| Implementation refinement — combine side | 9 |
|
||||
| Implementation refinement — sign side | 7 |
|
||||
| Implementation refinement — Pulsar_N1 codec round-trip | 1 |
|
||||
| **Subtotal — implementation refinement** | **17** |
|
||||
| Lean-bridged algebraic | 5 |
|
||||
| **Total named axioms** | **22** |
|
||||
|
||||
Authoritative source: `Pulsar_N1_Extracted.ec:34-92` and the per-file
|
||||
accounting blocks at the end of each `*_Refinement.ec`.
|
||||
|
||||
## Combine-side refinement axioms
|
||||
|
||||
All in `Pulsar_N1_Combine_Refinement.ec`.
|
||||
|
||||
| Axiom | Line | Category | Closure path |
|
||||
| --- | ---: | --- | --- |
|
||||
| `combine_body_mu_input_prefix_spec` | 504 | codec layout (FIPS 204 §5.4.1 prefix bytes) | byte-level layout proof — mechanical |
|
||||
| `combine_body_mu_input_ctx_bytes_spec` | 517 | codec layout (ctx-bytes slice) | byte-level layout proof — mechanical |
|
||||
| `combine_body_mu_input_m_bytes_spec` | 531 | codec layout (M-bytes suffix) | byte-level layout proof — mechanical |
|
||||
| `combine_body_matrix_a_spec` | 616 | w-stage sub-axiom (matrix A) | reduces to `MLDSA65_Functional.expand_a` byte-walk |
|
||||
| `combine_body_mask_y_spec` | 629 | w-stage sub-axiom (mask y at accepting kappa) | reduces to `MLDSA65_Functional.expand_mask` + accepted-kappa selection |
|
||||
| `combine_body_z_via_aggregation_spec` | 725 | z-stage structural (Lagrange aggregation shape) | mechanical structural identity |
|
||||
| `combine_body_partial_responses_spec` | 745 | z-stage byte-walk (per-party PR extraction) | narrow byte-walk through round-2 message parsing |
|
||||
| `combine_body_w_low_spec` | 810 | h-stage sub-axiom (w_low decompose output) | reduces to `decompose_vec_k` byte-walk |
|
||||
| `combine_no_reject_on_accepted_honest_layout` | 950 | accepted-path companion: layout + accept event ⇒ status = 0 | probabilistic Hoare logic on the kappa rejection loop |
|
||||
|
||||
## Sign-side refinement axioms
|
||||
|
||||
All in `Pulsar_N1_Sign_Refinement.ec`.
|
||||
|
||||
| Axiom | Line | Category | Closure path |
|
||||
| --- | ---: | --- | --- |
|
||||
| `sign_layout_m_buffer_external_mu` | 510 | wrapper byte-layout (`load_bytes` ↔ `external_mu`) | byte-layout proof — mechanical |
|
||||
| `sign_body_matrix_a_spec` | 560 | w-stage sub-axiom (matrix A) | reduces to `MLDSA65_Functional.expand_a` byte-walk |
|
||||
| `sign_body_mask_y_spec` | 570 | w-stage sub-axiom (mask y at accepting kappa) | reduces to `MLDSA65_Functional.expand_mask` + accepted-kappa selection |
|
||||
| `sign_body_y_spec` | 649 | z-stage sub-axiom (central y at accepting kappa) | reduces to `expand_mask` at accepted kappa |
|
||||
| `sign_body_cs1_spec` | 662 | z-stage sub-axiom (c · s1 mixed product) | reduces to `apply_c_to_s1` byte-walk |
|
||||
| `sign_body_w_low_spec` | 704 | h-stage sub-axiom (w_low decompose output) | reduces to `decompose_vec_k` byte-walk |
|
||||
| `sign_no_reject_on_accepted_honest_layout` | 826 | accepted-path companion: layout + accept event ⇒ status = 0 | probabilistic Hoare logic on the kappa rejection loop |
|
||||
|
||||
## Pulsar_N1 codec round-trip axiom
|
||||
|
||||
In `Pulsar_N1.ec`:
|
||||
|
||||
| Axiom | Line | Category | Closure path |
|
||||
| --- | ---: | --- | --- |
|
||||
| `pack_unpack_n1_signature_roundtrip` | 817 | FIPS 204 §3.5.5 packed-signature codec round-trip | bridge to `MLDSA65_Functional.pack_signature` when bit-level mechanization lands (Barbosa–Barthe–Dupressoir scale) |
|
||||
|
||||
## Lean-bridged algebraic axioms
|
||||
|
||||
Each axiom below is stated in EasyCrypt and discharged by a proved Lean
|
||||
theorem. The correspondence is pinned in
|
||||
`proofs/lean-easycrypt-bridge.md` and operationally guarded by
|
||||
`scripts/check-lean-bridge.sh`. See [Lean ↔ EC bridge](/docs/proofs/lean-bridge)
|
||||
for the full statements and proofs.
|
||||
|
||||
| EC axiom | EC file:line | Lean theorem |
|
||||
| --- | --- | --- |
|
||||
| `lagrange_inverse_eval` | `Pulsar_N1.ec:339` | `Crypto/Pulsar/Shamir.lean::shamir_correct_at_target` |
|
||||
| `add_share_zeroR` | `Pulsar_N4.ec:155` | structural (Mathlib `AddCommMonoid`) |
|
||||
| `reconstruct_linear` | `Pulsar_N4.ec:162` | `Crypto/Threshold_Lagrange.lean::combine_distributes_over_sum` |
|
||||
| `shamir_correct` | `Pulsar_N4.ec:176` | `Crypto/Pulsar/Shamir.lean::shamir_correct_at_target` (different specialization) |
|
||||
| `threshold_partial_response_identity` | `Pulsar_N1.ec:789` | `Crypto/Threshold_Lagrange.lean::threshold_partial_response_identity` |
|
||||
|
||||
## Closure-path summary
|
||||
|
||||
The 22 axioms decompose into four closure strategies:
|
||||
|
||||
### Mechanical byte-level (8 axioms)
|
||||
|
||||
The byte-layout axioms (`*_mu_input_*_spec`, `sign_layout_m_buffer_external_mu`)
|
||||
and the structural-shape axioms (`combine_body_z_via_aggregation_spec`,
|
||||
`combine_body_partial_responses_spec`) are pure byte-walk arguments. They
|
||||
close by bridging extracted procedure regions to FIPS 204 byte-format
|
||||
specifications. Estimated effort per axiom: days.
|
||||
|
||||
### FIPS 204 functional-op bridges (8 axioms)
|
||||
|
||||
The w-stage, z-stage sub-axioms and `pack_unpack_n1_signature_roundtrip`
|
||||
reduce to bit-level pack/unpack identities on the abstract types. Closing
|
||||
them means concretizing the abstract types against
|
||||
`MLDSA65_Functional.pack_signature` / `MLDSA65_Functional.encode_sk` once
|
||||
the FIPS 204 bit-level mechanization is in place. That mechanization is a
|
||||
multi-month research project comparable to Barbosa–Barthe–Dupressoir's
|
||||
Dilithium mechanization (CRYPTO 2023).
|
||||
|
||||
### Probabilistic Hoare (2 axioms)
|
||||
|
||||
The accepted-path no-reject axioms condition `status = 0` on the protocol-
|
||||
level `accept_signing_attempt` event. Closing them requires a probabilistic
|
||||
Hoare-logic chain that proves the kappa rejection-sampling loop terminates
|
||||
on honest inputs. The accompanying `mldsa_accept_lower_bound` operational
|
||||
bound — approximately $1 - 2^{-128}$ after the kappa-bounded loop — is
|
||||
operational rather than mechanized.
|
||||
|
||||
### Lean bridge (5 axioms)
|
||||
|
||||
The five Lean-bridged algebraic axioms are mechanized on the Lean side and
|
||||
connected by a CI-guarded citation bridge. **Replacing the bridges with
|
||||
checked translation artifacts** is the right step toward 100% mechanized.
|
||||
A translation layer that ingests both the Lean theorem statement and the
|
||||
EC axiom statement and machine-verifies their semantic equivalence is its
|
||||
own multi-week-to-multi-month project.
|
||||
|
||||
Alternatively, ported the Lean polynomial-Lagrange theory into EC itself
|
||||
(estimated 3–4 weeks for a minimal interpolation theory sufficient to
|
||||
discharge the five axioms).
|
||||
|
||||
## Derived lemmas (no longer axioms)
|
||||
|
||||
For traceability against the proof-artifact progression, the following
|
||||
axioms have been **converted to derived lemmas** since the original
|
||||
extraction (v3 → v12+). Each lemma now follows from narrower sub-axioms
|
||||
plus structural composition:
|
||||
|
||||
- `{combine,sign}_body_c_tilde_spec` (v5)
|
||||
- `{combine,sign}_body_mu_spec` (v6)
|
||||
- `{combine,sign}_body_w1_spec` (v7)
|
||||
- `combine_body_z_spec` (v8 — Lean-bridged)
|
||||
- `{combine,sign}_body_mu_input_spec` (v9)
|
||||
- `{combine,sign}_body_h_spec` (v10)
|
||||
- `sign_body_z_spec` (v11 — z = y + c·s1 structural split)
|
||||
- `{combine,sign}_body_w_spec` (v12 — A·y structural split)
|
||||
|
||||
Total: 14 axioms re-classified into derived lemmas across v5–v13. v11
|
||||
additionally eliminated 3 codec axioms outright by concretizing
|
||||
`signature_t` as a record-wrapper structure.
|
||||
|
||||
See [Extraction roadmap](/docs/proofs/extraction) for the per-version
|
||||
decomposition history.
|
||||
|
||||
## What this is not
|
||||
|
||||
The 22 axioms enumerate the **trust footprint** of the byte-equality
|
||||
chain. They are not the only EasyCrypt declarations in the dependency cone;
|
||||
the per-file accounting blocks distinguish axioms (trusted) from lemmas
|
||||
(derived). The headline byte-equality theorem
|
||||
`pulsar_n1_byte_equality_extracted` is itself a **proved lemma**, not an
|
||||
axiom — its proof composes the wrapper-bridge equivs with the body-spec
|
||||
lemmas, and trust reduces to the 22 axioms listed above.
|
||||
|
||||
## See also
|
||||
|
||||
- [Proofs overview](/docs/proofs/overview) — the three-prover stack.
|
||||
- [Lean ↔ EC bridge](/docs/proofs/lean-bridge) — the 5 algebraic axioms in detail.
|
||||
- [Extraction roadmap](/docs/proofs/extraction) — byte-walk decomposition history.
|
||||
@@ -0,0 +1,173 @@
|
||||
---
|
||||
title: Extraction roadmap
|
||||
description: How combine_body_compute_sig_spec and sign_body_compute_sig_spec moved from single bundled axioms to proved lemmas through versions v3 → v12+.
|
||||
---
|
||||
|
||||
The byte-equality theorem
|
||||
`pulsar_n1_byte_equality_extracted` reduces, on each side, to a
|
||||
`*_body_compute_sig_spec` obligation. In the original extraction these
|
||||
were single bundled axioms; both are now **proved lemmas**:
|
||||
|
||||
| Side | File:line | Status |
|
||||
| --- | --- | --- |
|
||||
| Combine | `proofs/easycrypt/Pulsar_N1_Combine_Refinement.ec:893` | Proved lemma |
|
||||
| Sign | `proofs/easycrypt/Pulsar_N1_Sign_Refinement.ec:776` | Proved lemma |
|
||||
|
||||
This page documents how the decomposition landed (v3 → v12+) and why
|
||||
each version moved trust into strictly narrower axioms.
|
||||
|
||||
## Version timeline
|
||||
|
||||
| Version | SHA | Change | Trust-footprint effect |
|
||||
| --- | --- | --- | --- |
|
||||
| v4 | `2eae979` | byte-walk: factor through `pack_n1_signature` | Component-triple axioms with codec roundtrip in `Pulsar_N1.ec` |
|
||||
| v4b | `564a330` | per-stage split | 2 component-triple → 6 stage-level axioms; broader surface but per-FIPS-stage |
|
||||
| v5 | `58af7b4` | c_tilde stage decomposition | `*_body_c_tilde_spec` → derived lemmas via mu + w1 sub-axioms |
|
||||
| v6 | `18d01af` | mu sub-stage decomposed via SHAKE/byte-layout | `*_body_mu_spec` → derived lemmas |
|
||||
| v7 | `76eae80` | w1 sub-stage via HighBits structural split | `*_body_w1_spec` → derived lemmas |
|
||||
| v8 | `835c176` | combine z-stage via Lean Lagrange bridge | `combine_body_z_spec` → derived lemma; new Lean-bridged `threshold_partial_response_identity` |
|
||||
| v9 | `01bdbc3` | `mu_shake_input_t = int list` concretization | constructive prep |
|
||||
| v9 + v10 | `83e3c38` | 3-agent parallel: sign mu_input close + combine mu_input decomp + h-stage MakeHint bridge | `*_body_{mu_input,h}_spec` → derived lemmas |
|
||||
| v11 sign z | `02c29f2` | sign z-stage via $z = y + c \cdot s_1$ structural split | `sign_body_z_spec` → derived lemma; 2 new sub-axioms `sign_body_y_spec` + `sign_body_cs1_spec` |
|
||||
| v11 codec | `81da17b` | `signature_t` concretization as record wrapping `int list` | **3 codec axioms ELIMINATED** (real closure, not decomposition) |
|
||||
| v12 w_spec | `02798c7` | w-stage via ExpandA + ExpandMask + mat_vec_mul structural split | `*_body_w_spec` × 2 → derived lemmas; 4 new sub-axioms (matrix_a + mask_y on each side) |
|
||||
| v13 accept | `02798c7` | per-R1/R2/R3/R4 accept bridge axiom | +1 bridge axiom (`accept_signing_attempt_iff_R1234`) connects bundled predicate to 4 per-R conditions |
|
||||
|
||||
## What's a decomposition vs. what's a closure
|
||||
|
||||
Most of the version moves are **decompositions**: a single broader axiom
|
||||
is replaced by narrower sub-axioms plus a proved structural composition.
|
||||
Trust moves to smaller, independently-attackable obligations; total
|
||||
axiom count typically stays the same or grows by 1.
|
||||
|
||||
A few moves are **real closures** where an axiom is removed without
|
||||
replacement:
|
||||
|
||||
- **v11 codec** eliminated 3 codec axioms outright by concretizing
|
||||
`signature_t` as a record-wrapper structure
|
||||
(`encode_decode_signature`, `decode_encode_signature_wf` removed;
|
||||
`encode_signature_wf` narrowed to a length-only axiom;
|
||||
`encode_signature_len` derived via record-wrap structure).
|
||||
|
||||
## Combine-side stage map
|
||||
|
||||
Mapping the FIPS 204 §6.2 inner-loop stages to extracted procedure regions
|
||||
in `combine.ec:3245-3617`. The Jasmin → EC extraction lives at
|
||||
`proofs/easycrypt/extraction/build/combine.ec` after running
|
||||
`scripts/extract-jasmin-ec.sh`.
|
||||
|
||||
| Stage | Extracted lines | Functional op | Current state |
|
||||
| --- | --- | --- | --- |
|
||||
| 1. Read c_tilde from input pointer | `combine.ec:3413-3416` | identity (wire input) | folded into `layout_combine_args` |
|
||||
| 2. Read t0 from t0 pointer | `combine.ec:3417-3426` | identity (wire input) | folded into `layout_combine_args` |
|
||||
| 3. Read & aggregate Round-2 messages | `combine.ec:3430-3505` | `vec_l_add`, `vec_k_add` | `combine_body_z_via_aggregation_spec` + `combine_body_partial_responses_spec` + `threshold_partial_response_identity` ⇒ `combine_body_z_spec` (lemma) |
|
||||
| 4. SampleInBall on c_tilde | `combine.ec:3506` | `sample_in_ball` | structural `central_c_from_c_tilde` shared by both sides |
|
||||
| 5. Compute $\mathbf{w}' = \mathbf{w}_{\mathrm{agg}} + c \mathbf{t}_0$ | `combine.ec:3530-3545` | `vec_k_add` + decompose math | `combine_body_matrix_a_spec` + `combine_body_mask_y_spec` ⇒ `combine_body_w_spec` (lemma) |
|
||||
| 6. Decompose $\mathbf{w}'$ | `combine.ec:3560` | `decompose_vec_k` | factored through structural `high_bits_of_w` ⇒ `combine_body_w1_spec` (lemma) |
|
||||
| 7. MakeHint(v0, v1) | `combine.ec:3550` | `vec_k_make_hint` | `combine_body_w_spec` + `combine_body_w_low_spec` ⇒ `combine_body_h_spec` (lemma) via structural `make_hint_of_w` |
|
||||
| 8. Rejection checks R1–R4 | `combine.ec:3562-3594` | norm bounds | `combine_no_reject_on_accepted_honest_layout` (axiom) |
|
||||
| 9. Pack signature | `combine.ec:3604` | `pack_signature` | folded into structural `pack_n1_signature` + `pack_unpack_n1_signature_roundtrip` (axiom in `Pulsar_N1.ec:817`) |
|
||||
| 10. Write sig_packed at sig_out_ptr | `combine.ec:3606-3611` | `write_signature_at` | proved in `Pulsar_N1_Combine_Layout.ec` |
|
||||
|
||||
## Sign-side stage map
|
||||
|
||||
Mapping the FIPS 204 §6.2 stages to extracted procedure regions in
|
||||
`sign.ec:3603-3641` (with `sign_inner` at `sign.ec:3469`). The kappa
|
||||
rejection-sampling loop wraps stages 5–8.
|
||||
|
||||
| Stage | Functional op | Current state |
|
||||
| --- | --- | --- |
|
||||
| 1. ExternalMu derivation | `external_mu_layout` | `sign_layout_m_buffer_external_mu` (axiom) → `sign_body_mu_input_spec` (lemma) → `sign_body_mu_spec` (lemma) |
|
||||
| 2. SampleInBall on c_tilde | `sample_in_ball` | structural |
|
||||
| 3. Compute $\mathbf{w} = \mathbf{A} \mathbf{y}$ at accepted κ | `mat_vec_mul` + `expand_a` + `expand_mask` | `sign_body_matrix_a_spec` + `sign_body_mask_y_spec` ⇒ `sign_body_w_spec` (lemma) |
|
||||
| 4. HighBits($\mathbf{w}$) → $\mathbf{w}_1$ | `high_bits_of_w` | structural |
|
||||
| 5. Compute $\mathbf{z} = \mathbf{y} + c \cdot \mathbf{s}_1$ at accepted κ | (vec ops) | `sign_body_y_spec` + `sign_body_cs1_spec` ⇒ `sign_body_z_spec` (lemma) |
|
||||
| 6. LowBits → $\mathbf{w}_\mathrm{low}$ | `decompose_vec_k` | `sign_body_w_low_spec` ⇒ `sign_body_h_spec` (lemma) via `make_hint_of_w` |
|
||||
| 7. Rejection checks R1–R4 | norm bounds | `sign_no_reject_on_accepted_honest_layout` (axiom) |
|
||||
| 8. Pack signature | `pack_signature` | folded into `pack_n1_signature` + codec round-trip axiom |
|
||||
|
||||
The sign side does **not** consume `threshold_partial_response_identity` —
|
||||
that bridge is only required on the combine side (Lagrange aggregation
|
||||
across the quorum). The sign-side z-stage uses the structural
|
||||
`add_response_vec` composition shared with `Pulsar_N1.mldsa_compute_z`.
|
||||
|
||||
## Accept-event conditioning (v13)
|
||||
|
||||
The v13 accept-bridge axiom `accept_signing_attempt_iff_R1234` connects
|
||||
the bundled protocol-level `accept_signing_attempt` predicate to the four
|
||||
per-rejection-condition predicates ($R_1, R_2, R_3, R_4$) used inside the
|
||||
byte-walks. Each per-stage lemma after v10 is **conditioned on
|
||||
`status = 0`** (the accepted-path precondition); the no-reject companion
|
||||
axioms discharge the status bit from the protocol-level accept event.
|
||||
|
||||
This sidesteps the prior framing — "the sign-side proof is harder because
|
||||
of the kappa loop" — by introducing `combine_body_compute_status` /
|
||||
`sign_body_compute_status` and threading the accept event through each
|
||||
per-stage lemma rather than over-the-loop.
|
||||
|
||||
## Per-version derived lemmas
|
||||
|
||||
The following obligations have been **converted from primitive axioms to
|
||||
derived lemmas** across the v5–v13 progression. The original obligation
|
||||
follows from narrower sub-axioms plus structural composition:
|
||||
|
||||
- v5: `{combine,sign}_body_c_tilde_spec`
|
||||
- v6: `{combine,sign}_body_mu_spec`
|
||||
- v7: `{combine,sign}_body_w1_spec`
|
||||
- v8: `combine_body_z_spec` (Lean-bridged)
|
||||
- v9: `{combine,sign}_body_mu_input_spec`
|
||||
- v10: `{combine,sign}_body_h_spec`
|
||||
- v11: `sign_body_z_spec`
|
||||
- v12: `{combine,sign}_body_w_spec`
|
||||
|
||||
Total: **14 axioms re-classified into derived lemmas** across v5–v13.
|
||||
|
||||
## Real-closure summary
|
||||
|
||||
In addition to the 14 re-classifications, **3 codec axioms** were
|
||||
**eliminated outright** in v11 (no replacement axiom):
|
||||
|
||||
- `encode_decode_signature` (removed)
|
||||
- `decode_encode_signature_wf` (removed)
|
||||
- `encode_signature_wf` (kept, narrowed to a length-only axiom)
|
||||
- `encode_signature_len` → derived via record-wrap structure
|
||||
|
||||
## Gate properties maintained throughout
|
||||
|
||||
- 13/13 EC files compile clean
|
||||
- jasmin-ct 3/3 blocking on threshold layer (round1, round2, combine)
|
||||
- Lean ↔ EC bridge guard 5/5
|
||||
- Admit budget 0/0
|
||||
- Lean bridge doc + check-script entry per bridged axiom
|
||||
- Refinement scaffold (no stray `declare axiom`) clean
|
||||
|
||||
## What's still axiomatic
|
||||
|
||||
See [Axiom inventory](/docs/proofs/axiom-inventory) for the 22 named
|
||||
axioms that remain in the dependency cone after the v12+ decompositions.
|
||||
Each has a documented closure path.
|
||||
|
||||
## Recommended next proof work (post-submission)
|
||||
|
||||
Per the user's review prioritization (revised after v7):
|
||||
|
||||
1. `*_body_z_spec` — likely easier than full `w_spec` with the Lean
|
||||
Lagrange bridge already stable. Use
|
||||
`Crypto.Threshold.Lagrange.threshold_partial_response_identity` for
|
||||
combine; reduce via vec ops + accepted-κ model for sign.
|
||||
2. `*_body_mu_input_spec` — byte-layout proof, mechanical and
|
||||
high-confidence once the FIPS 204 §5.4.1 byte serialization is
|
||||
concretised.
|
||||
3. `*_body_h_spec` — bridge toward `vec_k_make_hint`.
|
||||
4. `*_body_w_spec` — the hardest target; requires the loop/fixed-point
|
||||
accepted-κ model + `ExpandA` / `ExpandMask` / `mat_vec_mul`.
|
||||
|
||||
This reverses the earlier ordering (which had `w` as the natural next
|
||||
target after `w1`'s HighBits decomposition). The revised ordering
|
||||
optimizes for fastest residual-trust reduction.
|
||||
|
||||
## See also
|
||||
|
||||
- [Axiom inventory](/docs/proofs/axiom-inventory) — the 22 axioms after v12+.
|
||||
- [Lean ↔ EC bridge](/docs/proofs/lean-bridge) — the 5 algebraic axioms.
|
||||
- [Proofs overview](/docs/proofs/overview) — the three-prover stack.
|
||||
@@ -0,0 +1,292 @@
|
||||
---
|
||||
title: Lean ↔ EasyCrypt bridge
|
||||
description: The five algebraic axioms in the EasyCrypt dependency cone are discharged by proved Lean theorems. This page pins the correspondence.
|
||||
---
|
||||
|
||||
Pulsar's machine-checked proof stack uses **two complementary provers**:
|
||||
|
||||
- **EasyCrypt** drives the procedure-level refinement / equiv proofs for
|
||||
the threshold layer (`proofs/easycrypt/`). EasyCrypt is the right tool
|
||||
for procedural Hoare/equiv goals with side-channel-aware semantics —
|
||||
but its first-order theory of finite fields and polynomial interpolation
|
||||
is comparatively thin.
|
||||
- **Lean 4 + Mathlib** carries the algebraic content: Shamir
|
||||
reconstruction, Lagrange interpolation linearity, finite-field
|
||||
polynomial uniqueness. Mathlib has the field theory we would
|
||||
otherwise have to re-axiomatize in EC.
|
||||
|
||||
The bridge is currently **conceptual** — the EC side states the algebraic
|
||||
identities it needs as **named axioms** that correspond 1:1 to **proved
|
||||
Lean theorems** in the sibling repository
|
||||
`~/work/lux/proofs/lean/Crypto/`. This page pins the 1:1 correspondence so
|
||||
a reviewer can verify the math content is discharged elsewhere and not
|
||||
silently hand-waved.
|
||||
|
||||
The honest framing: **the EasyCrypt axioms named below are not unproved
|
||||
obligations in the strict sense — they are imports from the Lean proof
|
||||
artifact**. The audit gap is operational (no mechanical proof-object
|
||||
exchange across the two provers, no shared serialization format) rather
|
||||
than mathematical.
|
||||
|
||||
## Repository pin-points
|
||||
|
||||
- **EasyCrypt side**: `~/work/lux/pulsar/proofs/easycrypt/`.
|
||||
- **Lean side**: `~/work/lux/proofs/lean/Crypto/`, commit `923dc84` at
|
||||
bridge revision.
|
||||
|
||||
## Axiom 1: `lagrange_inverse_eval`
|
||||
|
||||
**EasyCrypt statement** (`proofs/easycrypt/Pulsar_N1.ec:177`):
|
||||
|
||||
```ec
|
||||
op poly_degree : share_t -> int.
|
||||
axiom poly_degree_nonneg (s : share_t) : 0 <= poly_degree s.
|
||||
|
||||
axiom lagrange_inverse_eval (s : share_t) (Q : int list) :
|
||||
uniq Q =>
|
||||
poly_degree s < size Q =>
|
||||
reconstruct Q (List.map (poly_eval s) Q) = s.
|
||||
```
|
||||
|
||||
The `poly_degree s < size Q` precondition matches the Lean theorem's
|
||||
`f.degree < s.card`. Earlier versions used the weaker `1 <= size Q` which
|
||||
permitted unsound instantiations on a short quorum reconstructing a
|
||||
non-constant polynomial.
|
||||
|
||||
**Lean proof** (`lean/Crypto/Pulsar/Shamir.lean:76`):
|
||||
|
||||
```lean
|
||||
theorem shamir_correct_at_target
|
||||
{F : Type*} [Field F] [DecidableEq F]
|
||||
(f : Polynomial F) {ι : Type*} [DecidableEq ι]
|
||||
(s : Finset ι) (v : ι → F)
|
||||
(hvs : Set.InjOn v s) (degree_f_lt : f.degree < s.card) :
|
||||
f = Lagrange.interpolate s v (fun i => f.eval (v i)) :=
|
||||
Crypto.Threshold.Lagrange.threshold_reconstructs_secret f s v hvs degree_f_lt
|
||||
```
|
||||
|
||||
**Correspondence**
|
||||
|
||||
| Symbol | EC | Lean |
|
||||
| --- | --- | --- |
|
||||
| Shamir polynomial | `s : share_t` (abstracted as its constant term) | `f : Polynomial F` |
|
||||
| Quorum / evaluation set | `Q : int list` (with `uniq Q`) | `s : Finset ι` + `v : ι → F` injective on `s` |
|
||||
| Per-party share | `poly_eval s i` | `f.eval (v i)` |
|
||||
| Reconstruction | `reconstruct Q shares` | `(Lagrange.interpolate s v shares).eval 0` |
|
||||
| Identity at quorum | `reconstruct Q (map (poly_eval s) Q) = s` | `f = Lagrange.interpolate s v (fun i => f.eval (v i))` then evaluate at 0 |
|
||||
|
||||
The Lean theorem is **stronger** (polynomial-level equality, not just
|
||||
constant-term recovery). Specializing to evaluation at 0 yields the
|
||||
EC-side identity via
|
||||
`Crypto.Threshold.Lagrange.secret_recovery_at_zero` (file
|
||||
`lean/Crypto/Threshold_Lagrange.lean:62`).
|
||||
|
||||
**Degree bound**. The Lean side requires `f.degree < s.card`. On the EC
|
||||
side this is implicit in the abstract `share_t` type (Pulsar's Shamir
|
||||
polynomial has degree exactly $t - 1$ over a $t$-of-$n$ committee, and
|
||||
`size Q ≥ 1` plus `uniq Q` plus the implicit `t ≤ size Q` from the
|
||||
protocol layer gives the degree bound).
|
||||
|
||||
## Axiom 2: `reconstruct_linear`
|
||||
|
||||
**EasyCrypt statement** (`proofs/easycrypt/Pulsar_N4.ec:133`):
|
||||
|
||||
```ec
|
||||
axiom reconstruct_linear :
|
||||
forall (q : int list) (a b : share_t list),
|
||||
size a = size q => size b = size q =>
|
||||
reconstruct q (zip_add a b) =
|
||||
add_share (reconstruct q a) (reconstruct q b).
|
||||
```
|
||||
|
||||
**Lean proof** (`lean/Crypto/Threshold_Lagrange.lean:81`):
|
||||
|
||||
```lean
|
||||
theorem combine_distributes_over_sum
|
||||
{ι : Type*} [DecidableEq ι] (s : Finset ι) (v : ι → F) (a b : ι → F) :
|
||||
Lagrange.interpolate s v (a + b) =
|
||||
Lagrange.interpolate s v a + Lagrange.interpolate s v b :=
|
||||
(Lagrange.interpolate s v).map_add a b
|
||||
```
|
||||
|
||||
**Correspondence**
|
||||
|
||||
| Symbol | EC | Lean |
|
||||
| --- | --- | --- |
|
||||
| Quorum | `q : int list` | `s : Finset ι` |
|
||||
| Per-party value | `a, b : share_t list` | `a, b : ι → F` |
|
||||
| Pointwise sum | `zip_add a b` | `a + b` (pointwise) |
|
||||
| Combination | `reconstruct q (...)` | `(Lagrange.interpolate s v (...)).eval 0` |
|
||||
| Linearity | `reconstruct (a + b) = reconstruct a + reconstruct b` | `interpolate (a + b) = interpolate a + interpolate b` |
|
||||
|
||||
The Lean theorem follows from `LinearMap.map_add` applied to
|
||||
`Lagrange.interpolate s v`, which Mathlib expresses as an $F$-linear map.
|
||||
Evaluating at 0 (an $R$-linear operation) preserves the equation. This
|
||||
is exactly the algebraic content the EC axiom states.
|
||||
|
||||
## Axiom 3: `shamir_correct`
|
||||
|
||||
**EasyCrypt statement** (`proofs/easycrypt/Pulsar_N4.ec:141`):
|
||||
|
||||
```ec
|
||||
axiom shamir_correct :
|
||||
forall (q : int list) (s : share_t),
|
||||
uniq q => 1 <= size q =>
|
||||
reconstruct q (fresh_sharing q s) = s.
|
||||
```
|
||||
|
||||
**Lean proof** (same as Axiom 1):
|
||||
|
||||
```lean
|
||||
theorem shamir_correct_at_target ... -- Crypto/Pulsar/Shamir.lean:76
|
||||
```
|
||||
|
||||
Plus the auxiliary `secret_recovery_at_zero`
|
||||
(`lean/Crypto/Threshold_Lagrange.lean:62`).
|
||||
|
||||
**Correspondence**. `fresh_sharing q s` is the Pulsar adapter that
|
||||
constructs the per-party shares of `s` along quorum `q` (= mapping
|
||||
$q \mapsto \mathrm{poly\_eval}(s)$ on each `q[i]`, modulo the internal
|
||||
randomness of the polynomial above degree 0). After Lagrange-recovery via
|
||||
`reconstruct`, the constant term `s` returns. Same theorem as Axiom 1,
|
||||
applied differently.
|
||||
|
||||
## Axiom 4: `add_share_zeroR`
|
||||
|
||||
**EasyCrypt statement** (`proofs/easycrypt/Pulsar_N4.ec:130`):
|
||||
|
||||
```ec
|
||||
axiom add_share_zeroR : forall (s : share_t), add_share s zero_share = s.
|
||||
```
|
||||
|
||||
This is an algebraic identity on the `share_t` ring (right-identity of
|
||||
addition). Mathlib provides this for any `AddCommMonoid`-instance type,
|
||||
but the EC side keeps `share_t` abstract and so axiomatizes the property
|
||||
directly. On the Lean side this is implicit in the `Ring` /
|
||||
`Polynomial`-coefficient instances and never needs an explicit theorem.
|
||||
|
||||
## Axiom 5: `threshold_partial_response_identity`
|
||||
|
||||
**EasyCrypt statement** (`proofs/easycrypt/Pulsar_N1.ec`, v8):
|
||||
|
||||
```ec
|
||||
axiom threshold_partial_response_identity :
|
||||
forall (Q : int list) (shares : share_t list)
|
||||
(c_tilde : c_tilde_n1_t) (rho_rnd : randomness_t) (mu_val : mu_t),
|
||||
uniq Q =>
|
||||
size shares = size Q =>
|
||||
poly_degree (reconstruct Q shares) < size Q =>
|
||||
shares = List.map (poly_eval (reconstruct Q shares)) Q =>
|
||||
lagrange_aggregate_responses Q
|
||||
(List.map (per_party_partial_response c_tilde rho_rnd mu_val) shares)
|
||||
= mldsa_compute_z
|
||||
(unpack_sk (reconstruct Q shares))
|
||||
mu_val rho_rnd.
|
||||
```
|
||||
|
||||
**Lean counterpart**
|
||||
(`~/work/lux/proofs/lean/Crypto/Threshold_Lagrange.lean:121`,
|
||||
theorem `threshold_partial_response_identity`):
|
||||
|
||||
```lean
|
||||
theorem threshold_partial_response_identity
|
||||
(f : F[X]) {ι : Type*} [DecidableEq ι] (s : Finset ι) (v : ι → F)
|
||||
(hvs : Set.InjOn v s) (degree_f_lt : f.degree < s.card)
|
||||
(y : ι → F) (c : F)
|
||||
(z : ι → F) (hz : z = y + c • fun i => f.eval (v i)) :
|
||||
(Lagrange.interpolate s v z).eval 0 =
|
||||
(Lagrange.interpolate s v y).eval 0 + c * f.eval 0
|
||||
```
|
||||
|
||||
**Type correspondence**
|
||||
|
||||
| Lean | EasyCrypt | Meaning |
|
||||
| --- | --- | --- |
|
||||
| `F[X]` | (abstracted into `share_t`) | secret-sharing polynomial |
|
||||
| `s : Finset ι` | `Q : int list` (with `uniq Q`) | quorum |
|
||||
| `v : ι → F` (with `Set.InjOn v s`) | implicit in `uniq Q` | party indexing |
|
||||
| `degree_f_lt : f.degree < s.card` | `poly_degree (reconstruct Q shares) < size Q` | sharing-polynomial degree bound |
|
||||
| `z = y + c • fun i => f.eval (v i)` (per party) | `per_party_partial_response c_tilde rho_rnd mu_val (poly_eval (reconstruct Q shares) i)` | per-party response |
|
||||
| `Lagrange.interpolate s v z .eval 0` | `lagrange_aggregate_responses Q [per_party_PR_i]` | quorum aggregation at 0 |
|
||||
| `+ c * f.eval 0` | folded into the abstract `mldsa_compute_z` on the reconstructed share | centralised z |
|
||||
|
||||
**Used by**
|
||||
`Pulsar_N1_Combine_Refinement.combine_body_z_spec` (v8, now a derived
|
||||
lemma) — bridges the combine-side z-stage byte-walk to the Lean Lagrange
|
||||
theorem. The `combine_body_partial_responses_spec` narrow axiom +
|
||||
`combine_body_z_via_aggregation_spec` structural axiom + this bridge
|
||||
compose to derive `combine_body_z_spec`.
|
||||
|
||||
**Honest framing**
|
||||
|
||||
The EC axiom integrates three facts:
|
||||
|
||||
1. The Lean theorem's algebraic identity (`interpolate-z = interpolate-y + c·f(0)`);
|
||||
2. The implicit y-aggregation: `mldsa_compute_z`'s `y_central` equals
|
||||
the Lagrange-aggregation of the per-party `y_i` values used in
|
||||
`per_party_partial_response`;
|
||||
3. The structural decomposition `mldsa_compute_z = y_central + c · s_central`.
|
||||
|
||||
Facts (2) and (3) are not separately mechanized — they are folded into
|
||||
the EC axiom's RHS via the abstract `mldsa_compute_z` op. Future narrowing
|
||||
would expose y_aggregation as a separate identity and split this bridge
|
||||
into smaller pieces.
|
||||
|
||||
## What this bridge does NOT do
|
||||
|
||||
It does **not** provide a mechanical proof-object exchange. The EC axioms
|
||||
are still trusted in the EC dependency cone — the bridge is a
|
||||
code-review-level mapping, not a formal-method-level one.
|
||||
|
||||
The honest closure path is:
|
||||
|
||||
1. **Either** mechanize the four (now five — Axiom 5 added v8) axioms
|
||||
inside EasyCrypt itself (would require importing or rebuilding a
|
||||
finite-field polynomial-interpolation library in EC; multi-week
|
||||
project),
|
||||
2. **Or** prove the same statements in a tool whose proof object EC can
|
||||
consume (no current standard format),
|
||||
3. **Or** keep the conceptual bridge and pin the Lean commit in the EC
|
||||
file headers (which we do, see "Citation comments" below).
|
||||
|
||||
Option (3) is what we do today. It is honest — the EC axiom statements
|
||||
correspond 1:1 to Lean theorems we have proved — but it is not strict
|
||||
closure inside the EC dependency cone.
|
||||
|
||||
## Citation comments
|
||||
|
||||
Each of the five EC axioms above has an inline comment immediately
|
||||
preceding it that names the Lean theorem and file. Updating the EC axiom
|
||||
statement without updating the Lean side (or vice versa) trips the
|
||||
per-push test for "axiom signature change without bridge comment update"
|
||||
— operationally guarded by `scripts/check-lean-bridge.sh`.
|
||||
|
||||
## Future work
|
||||
|
||||
1. **Mechanical close in EC**. Build out a minimal polynomial-
|
||||
interpolation theory inside EasyCrypt (just enough to discharge the
|
||||
five axioms). This removes the bridge entirely. Estimated effort: 3–4
|
||||
weeks.
|
||||
2. **Bridge guard in CI**. `scripts/check-lean-bridge.sh` already asserts
|
||||
each EC axiom in the bridge has an unchanged signature AND a citation
|
||||
comment naming a Lean theorem that still exists.
|
||||
3. **Lean → EC tactic translation**. Long-term: if the EasyCrypt community
|
||||
adds a Lean-proof-object consumer, the bridge becomes a one-line
|
||||
`import` rather than five axiom statements.
|
||||
|
||||
## Honest summary
|
||||
|
||||
The trust footprint of the extracted N1 byte-equality theorem, including
|
||||
the bridge (v8):
|
||||
|
||||
- Implementation-refinement axioms (EC, byte-walks): **17**, decomposed
|
||||
into stage-level + sub-stage + codec-layout + no-reject pieces. See
|
||||
[Axiom inventory](/docs/proofs/axiom-inventory).
|
||||
- Algebraic-content axioms bridged to Lean: **5** (Axioms 1–5 above).
|
||||
Each has a corresponding Lean theorem cited inline. Axiom 5
|
||||
(`threshold_partial_response_identity`) was added in v8 to discharge
|
||||
the combine z-stage aggregation.
|
||||
- Module-contract axioms in the extracted N1 corollary: **0**.
|
||||
|
||||
The full per-version per-axiom inventory lives in
|
||||
`proofs/easycrypt/Pulsar_N1_Extracted.ec` and the submission cover sheet.
|
||||
@@ -0,0 +1,4 @@
|
||||
{
|
||||
"title": "Proofs",
|
||||
"pages": ["overview", "axiom-inventory", "lean-bridge", "extraction"]
|
||||
}
|
||||
@@ -0,0 +1,211 @@
|
||||
---
|
||||
title: Proofs overview
|
||||
description: The Pulsar high-assurance stack — Jasmin, EasyCrypt, Lean Mathlib bridge, and what's mechanized vs. axiomatic.
|
||||
---
|
||||
|
||||
Pulsar ships a Jasmin + EasyCrypt high-assurance track aimed at the same
|
||||
formal-method footing libjade gives the single-party ML-DSA implementation:
|
||||
Jasmin sources whose verified compiler produces bit-identical assembly, and
|
||||
EasyCrypt theories that machine-check both functional correctness and
|
||||
constant-time against the Barthe–Grégoire–Laporte leakage model.
|
||||
|
||||
The Lean side carries the algebraic content (Shamir reconstruction,
|
||||
Lagrange interpolation linearity, finite-field polynomial uniqueness)
|
||||
that EasyCrypt's first-order field theory cannot ergonomically reach.
|
||||
|
||||
## Headline
|
||||
|
||||
All local EasyCrypt theorem bodies are admit-free, per-push gates are green,
|
||||
threshold Jasmin CT is blocking, fuzz / KAT / interop / dudect gates are
|
||||
wired at documented budgets, and the extracted N1 theorem has no
|
||||
section-local module-contract axioms. The remaining implementation-refinement
|
||||
assumptions are progressively decomposed into strictly narrower axioms with a
|
||||
committed proof roadmap; the Lean↔EC algebraic bridge is named, cited, and
|
||||
CI-guarded.
|
||||
|
||||
| Item | Count |
|
||||
| --- | ---: |
|
||||
| Section-local module-contract axioms in extracted N1 corollary | **0** |
|
||||
| Implementation-refinement axioms in dependency cone | **17** |
|
||||
| Lean-bridged algebraic axioms | **5** |
|
||||
| EasyCrypt `admit` budget | **0 / 0** |
|
||||
| EC files in the per-push gate | **13** |
|
||||
| `declare axiom` in refinement scaffolds | **0** |
|
||||
|
||||
Authoritative source: the accounting block at
|
||||
`Pulsar_N1_Extracted.ec:34-92` and the per-file accounting blocks at the
|
||||
end of each `*_Refinement.ec`.
|
||||
|
||||
## The three provers
|
||||
|
||||
### EasyCrypt
|
||||
|
||||
Procedure-level refinement and equivalence proofs for the threshold layer:
|
||||
|
||||
- `Pulsar_N1.ec` — Class N1 protocol-level spec + generic byte-equality theorem
|
||||
- `Pulsar_N4.ec` — Class N4 reshare public-key preservation
|
||||
- `Pulsar_N1_Memory.ec` — byte-memory model (zero axioms)
|
||||
- `Pulsar_N1_Signature_Codec.ec` — FIPS 204 §3.5.5 signature codec
|
||||
- `Pulsar_N1_Combine_Layout.ec` — combine ABI byte layout
|
||||
- `Pulsar_N1_Sign_Layout.ec` — libjade Sign ABI byte layout
|
||||
- `Pulsar_N1_Combine_Refinement.ec` — combine refinement scaffold
|
||||
- `Pulsar_N1_Sign_Refinement.ec` — sign refinement scaffold + ctx/rho_rnd ghost contract
|
||||
- `Pulsar_N1_Combine_Wrapper.ec` — combine wrapper module + bridge lemma
|
||||
- `Pulsar_N1_Sign_Wrapper.ec` — sign wrapper module + bridge lemma
|
||||
- `Pulsar_N1_Extracted.ec` — concrete extracted N1 byte-equality corollary
|
||||
- `lemmas/MLDSA65_Functional.ec` — FIPS 204 functional ops
|
||||
- `lemmas/Pulsar_CT.ec` — constant-time obligations
|
||||
|
||||
The dependency graph is acyclic; each file owns one concern.
|
||||
|
||||
### Lean 4 + Mathlib
|
||||
|
||||
Algebraic content for Shamir / Lagrange identities:
|
||||
|
||||
- `~/work/lux/proofs/lean/Crypto/Pulsar/Shamir.lean` — Shamir correctness
|
||||
at the target (degree bound matched).
|
||||
- `~/work/lux/proofs/lean/Crypto/Threshold_Lagrange.lean` — linearity of
|
||||
interpolation, threshold partial-response identity.
|
||||
- `~/work/lux/proofs/lean/Crypto/Pulsar/OutputInterchange.lean` —
|
||||
symbolic-level byte-interchange argument.
|
||||
- `~/work/lux/proofs/lean/Crypto/Pulsar/dkg2.lean` and `Unforgeability.lean`
|
||||
— DKG soundness and unforgeability statements.
|
||||
|
||||
### Jasmin
|
||||
|
||||
Constant-time-aware low-level sources whose verified compiler produces
|
||||
bit-identical assembly:
|
||||
|
||||
- `jasmin/ml-dsa-65/` — libjade single-party baseline (pinned at commit
|
||||
`9426b32`, fetched on demand).
|
||||
- `jasmin/threshold/round1.jazz` (~400 lines)
|
||||
- `jasmin/threshold/round2.jazz` (~600 lines)
|
||||
- `jasmin/threshold/combine.jazz` (~400 lines)
|
||||
|
||||
`jasmin-ct` is **blocking** on the threshold layer (round1, round2, combine
|
||||
all CT-clean). The libjade single-party sign side carries an upstream
|
||||
annotation gap tracked as advisory (`ct/jasmin-ct-libjade.md`).
|
||||
|
||||
## Dependency layering
|
||||
|
||||
```
|
||||
Pulsar_N1 ──┐
|
||||
│
|
||||
Memory ── Signature_Codec
|
||||
│ │
|
||||
├── Combine_Layout Sign_Layout
|
||||
│ │ │
|
||||
│ Combine_Refinement Sign_Refinement
|
||||
│ │ │
|
||||
│ Combine_Wrapper Sign_Wrapper
|
||||
│ │_________ Extracted ____│
|
||||
│
|
||||
└── (Pulsar_N1: protocol types + module types + generic theorem)
|
||||
```
|
||||
|
||||
`Sign_Layout` does not transitively depend on combine-specific encoders;
|
||||
the two layouts are siblings sharing Memory + Signature_Codec.
|
||||
|
||||
## What's proved
|
||||
|
||||
| Object | Status | Location |
|
||||
| --- | --- | --- |
|
||||
| Class N1 byte-equality (concrete) | **Proven as a lemma** (`pulsar_n1_byte_equality_extracted`) | `Pulsar_N1_Extracted.ec` |
|
||||
| Class N1 byte-equality (generic) | **Proven as a theorem** (`pulsar_n1_byte_equality`) | `Pulsar_N1.ec` |
|
||||
| Class N4 public-key preservation | **Proven** (concrete `ReshareHonest` module + lemma) | `Pulsar_N4.ec` |
|
||||
| Wrapper bridges (combine + sign) | **Proven as lemmas** (both — neither is an axiom) | `Pulsar_N1_{Combine,Sign}_Wrapper.ec` |
|
||||
| Body separation (combine + sign) | **Proven as lemmas** | `Pulsar_N1_{Combine,Sign}_Refinement.ec` |
|
||||
| Memory frame laws | **Proven** (0 axioms) | `Pulsar_N1_Memory.ec` |
|
||||
| Combine `compute_sig` byte-walk | **Proven as a lemma** (composed of narrower stage-level facts) | `Pulsar_N1_Combine_Refinement.ec:893` |
|
||||
| Sign `compute_sig` byte-walk | **Proven as a lemma** (composed of narrower stage-level facts) | `Pulsar_N1_Sign_Refinement.ec:776` |
|
||||
|
||||
## What's axiomatic — the 22 named axioms
|
||||
|
||||
The trust footprint of the extracted N1 byte-equality theorem decomposes
|
||||
into **22 named axioms**, each cited with file:line in EasyCrypt and (for
|
||||
the Lean-bridged five) in Lean:
|
||||
|
||||
| Category | Count | Notes |
|
||||
| --- | ---: | --- |
|
||||
| Stage-level byte-walks (post v12) | 1 | `sign_body_z_spec` |
|
||||
| w-stage matrix_a / mask_y sub-axioms (v12) | 4 | combine + sign × \{matrix_a, mask_y\} |
|
||||
| Combine-side z extraction (v8) | 2 | `combine_body_z_via_aggregation_spec` + `combine_body_partial_responses_spec` |
|
||||
| w_low sub-axioms (h-stage, v10) | 2 | `{combine,sign}_body_w_low_spec` |
|
||||
| Codec mu_input layout (v9) | 4 | combine: 3 per-range; sign: 1 collapsed |
|
||||
| Accepted-path no-reject | 2 | `{combine,sign}_no_reject_on_accepted_honest_layout` |
|
||||
| Codec roundtrip | 1 | `pack_unpack_n1_signature_roundtrip` |
|
||||
| **Subtotal — implementation refinement** | **17** | byte-walk + codec round-trip + honest-execution no-reject |
|
||||
| Lean-bridged algebraic | 5 | `lagrange_inverse_eval`, `reconstruct_linear`, `shamir_correct`, `add_share_zeroR`, `threshold_partial_response_identity` |
|
||||
| **Total named axioms** | **22** | each with file:line in EC and Lean |
|
||||
|
||||
See [Axiom inventory](/docs/proofs/axiom-inventory) for each axiom's
|
||||
statement, citation, and closure path. See [Lean ↔ EC bridge](/docs/proofs/lean-bridge)
|
||||
for the Lean theorems backing the five algebraic axioms. See
|
||||
[Extraction roadmap](/docs/proofs/extraction) for the byte-walk
|
||||
decomposition history (v3 → v12+).
|
||||
|
||||
## Conventions
|
||||
|
||||
- `admit` is banned (budget 0/0; enforced by
|
||||
`scripts/checks/ec-admits.sh`).
|
||||
- `declare axiom` is banned in refinement scaffolds (enforced by
|
||||
`scripts/checks/ec-refinement-scaffold.sh`).
|
||||
- Lean-bridged axioms carry an inline citation comment naming the Lean
|
||||
theorem and file (enforced by `scripts/check-lean-bridge.sh`).
|
||||
- Per-push gate is real-budget: `scripts/check-high-assurance.sh` runs
|
||||
every check at the budget that matters (jasmin-ct, EC admit budget,
|
||||
EC regression guards, refinement-scaffold guard, Lean bridge guard,
|
||||
Jasmin→EC extraction, EC compile). No smoke gates.
|
||||
- Real-budget dudect ($10^9$ samples per target) + 1h-per-target fuzz run
|
||||
from the nightly gate: `scripts/nightly.sh`.
|
||||
|
||||
## How to check
|
||||
|
||||
Per-push:
|
||||
|
||||
```bash
|
||||
./scripts/check-high-assurance.sh # proof gate
|
||||
./scripts/test.sh # Go test gate
|
||||
```
|
||||
|
||||
Nightly (multi-hour, cron-scheduled):
|
||||
|
||||
```bash
|
||||
./scripts/nightly.sh
|
||||
```
|
||||
|
||||
Per-check (independently runnable):
|
||||
|
||||
```bash
|
||||
bash scripts/checks/ec-compile.sh
|
||||
bash scripts/checks/jasmin.sh
|
||||
bash scripts/checks/ec-admits.sh
|
||||
bash scripts/check-lean-bridge.sh
|
||||
```
|
||||
|
||||
## What this submission does NOT yet claim
|
||||
|
||||
The Class N1 byte-equality theorem is **proven in EasyCrypt as a lemma**;
|
||||
the headline byte-equality corollary follows from it via the wrapper
|
||||
bridges. Closing the gap to fully mechanized correctness requires closing
|
||||
the named obligations enumerated in [Axiom inventory](/docs/proofs/axiom-inventory):
|
||||
|
||||
- 17 implementation-refinement axioms (byte-walks + codec round-trip +
|
||||
honest-execution no-reject)
|
||||
- 5 Lean-bridged algebraic axioms (replace the conceptual bridge with a
|
||||
machine-checked translation artifact, or port the Lean polynomial-
|
||||
Lagrange theory into EC)
|
||||
- The libjade jasmin-ct annotation gap (advisory, upstream issue #2)
|
||||
|
||||
Each axiom is **independently attackable** with a documented closure path.
|
||||
|
||||
## Citations
|
||||
|
||||
- Barthe, Grégoire, Laporte. *Secure compilation of side-channel
|
||||
countermeasures: The case of cryptographic constant-time.* CSF 2018.
|
||||
- Barbosa, Barthe, Doczkal, Don, Fehr, Grégoire, Huang, Hülsing,
|
||||
Lee, Wu. *Fixing and Mechanizing the Security Proof of
|
||||
Fiat–Shamir with Aborts and Dilithium.* CRYPTO 2023.
|
||||
- Almeida et al. *Formally verifying Kyber.* CRYPTO 2024.
|
||||
- libjade ML-DSA EasyCrypt theories —
|
||||
https://github.com/formosa-crypto/libjade/tree/main/proof
|
||||
@@ -0,0 +1,131 @@
|
||||
---
|
||||
title: DKG and proactive resharing
|
||||
description: Pedersen DKG over R_q^k, with proactive resharing under a beacon-randomized quorum.
|
||||
---
|
||||
|
||||
Pulsar distributes key generation via a Pedersen DKG over the M-LWE module
|
||||
ring $R_q^k$, with the Feldman-style verifiable secret sharing replaced by
|
||||
the module-shaped Pedersen commitment scheme. The construction inherits
|
||||
its soundness argument from the Ring-LWE version that ships in
|
||||
[`luxfi/corona`](https://github.com/luxfi/corona), ported to the module
|
||||
shape with constant overhead per coefficient slot.
|
||||
|
||||
## Why Pedersen, not trusted-dealer
|
||||
|
||||
The academic 2-round threshold ML-DSA literature largely assumes a
|
||||
**trusted dealer**: a single party samples the master secret and hands out
|
||||
shares. That model is incompatible with open public chains.
|
||||
|
||||
Pulsar's Pedersen DKG removes the trusted dealer: each party samples a
|
||||
random polynomial over $R_q^k$, broadcasts a hiding commitment to it, and
|
||||
emits shares of its polynomial to every other party. The aggregate group
|
||||
secret is the sum of all parties' polynomials evaluated at zero; no single
|
||||
party (and no proper subset of fewer than $t$ parties) ever holds the
|
||||
group secret in clear.
|
||||
|
||||
## Round structure (sketch)
|
||||
|
||||
### Per-party setup
|
||||
|
||||
Party $i$ samples a degree-$(t-1)$ polynomial
|
||||
$f_i: R_q^k \to R_q^k$ (one polynomial per module slot) with
|
||||
$f_i(0) = \mathbf{a}_i \cdot \chi$ where $\chi$ is the M-LWE error
|
||||
distribution and $\mathbf{a}_i$ is sampled uniformly. Party $i$ commits
|
||||
to $f_i$ via the module-shaped Pedersen commitment scheme and broadcasts
|
||||
the commitment.
|
||||
|
||||
### Share delivery
|
||||
|
||||
Party $i$ emits to each other party $j$ the share $f_i(j)$ via an
|
||||
encrypted, authenticated point-to-point channel. The encryption uses an
|
||||
ML-KEM-768 wrapper bound to the recipient's long-term identity key
|
||||
(CR-6 closure, see [postmortem references in BLOCKERS.md](https://github.com/luxfi/pulsar/blob/main/BLOCKERS.md)).
|
||||
|
||||
### Verification
|
||||
|
||||
Each party $j$ verifies that every received share is consistent with the
|
||||
broadcasted commitment. Inconsistent shares trigger an identifiable abort
|
||||
with signed evidence.
|
||||
|
||||
### Aggregation
|
||||
|
||||
The group secret share at party $j$ is $s_j = \sum_i f_i(j)$. The group
|
||||
public key is
|
||||
|
||||
$$
|
||||
\mathbf{t} = \mathbf{A} \cdot \mathbf{s_1} + \mathbf{s_2}
|
||||
$$
|
||||
|
||||
where $\mathbf{s_1}, \mathbf{s_2}$ are the Lagrange-reconstructed group
|
||||
secrets at quorum-evaluation points 0.
|
||||
|
||||
## Class N4 — public-key preservation across resharing
|
||||
|
||||
Proactive resharing rotates the share custodians without changing the
|
||||
group public key. For long-lived deployments (multi-epoch validator set),
|
||||
the relevant adversary model is mobile (HJKY97): the adversary may corrupt
|
||||
up to $t-1$ parties **per epoch**, with the corruption set varying.
|
||||
|
||||
Pulsar's reshare:
|
||||
|
||||
1. The outgoing quorum samples fresh randomness and emits re-shared
|
||||
contributions for the incoming quorum.
|
||||
2. The incoming quorum aggregates the contributions to form fresh shares
|
||||
of the same group secret.
|
||||
3. Public-key continuity is verified: the new shares Lagrange-reconstruct
|
||||
to the same $\mathbf{s_1}$ as the previous epoch.
|
||||
|
||||
The Class N4 theorem `reshare_preserves_secret_honest` in
|
||||
`proofs/easycrypt/Pulsar_N4.ec` proves public-key continuity over the
|
||||
abstract reshare module under the honest-execution model. The Lean-bridged
|
||||
algebraic axioms `add_share_zeroR`, `reconstruct_linear`, and
|
||||
`shamir_correct` discharge the additive structure on shares; see
|
||||
[Lean ↔ EC bridge](/docs/proofs/lean-bridge).
|
||||
|
||||
## Beacon-randomized quorum selection
|
||||
|
||||
For the proactive resharing path specifically, the **quorum selection** must
|
||||
not be deterministic. A mobile adversary that knows the deterministic
|
||||
quorum-selection rule can pre-position corruptions to land in the
|
||||
selected quorum every epoch, defeating the mobile-adversary security
|
||||
argument.
|
||||
|
||||
Pulsar's reshare selects the per-epoch quorum via a beacon-derived
|
||||
randomness commit at the epoch boundary (HIP-0077 §"reshare quorum" F10
|
||||
fix). Production deployments bind this to the consensus layer's existing
|
||||
randomness beacon.
|
||||
|
||||
## Identifiable abort
|
||||
|
||||
If any party deviates during DKG or reshare — emits an inconsistent
|
||||
share, omits a round message, broadcasts an invalid commitment — the
|
||||
remaining honest parties identify the deviating party and produce signed
|
||||
evidence suitable for slashing.
|
||||
|
||||
Pulsar identifies deviations under synchronous network assumptions only;
|
||||
asynchronous identifiable abort is out of scope for this submission.
|
||||
|
||||
## Out-of-scope adversary capabilities
|
||||
|
||||
- Compromise of the cryptographic hash function (SHAKE-256 / cSHAKE-256 /
|
||||
KMAC-256). NIST FIPS 202 + SP 800-185 are taken as building blocks.
|
||||
- Side-channel attacks on the physical hardware running a party (power
|
||||
analysis, EM, fault injection). Handled at the deployed-binary layer;
|
||||
the algorithm-correctness chain is independent.
|
||||
- Compromise of the BIP-32/BIP-39 mnemonic from which device-specific
|
||||
keys are derived.
|
||||
|
||||
## Source pointers
|
||||
|
||||
- DKG: `ref/go/pkg/pulsar/dkg.go`, `dkg_parallel.go` (GPU fan-out path,
|
||||
honestly labelled per v1.0.x rename), `large_dkg.go`.
|
||||
- Reshare: `ref/go/pkg/pulsar/reshare.go`, `large_reshare.go`.
|
||||
- Pedersen commitment scheme over $R_q^k$: see spec `spec/pulsar.tex` §4.5.
|
||||
- Class N4 proof: `proofs/easycrypt/Pulsar_N4.ec`.
|
||||
|
||||
## See also
|
||||
|
||||
- [Parameters](/docs/protocol/parameters) — module dimension $k$, secret
|
||||
dimension $\ell$, threshold $(n, t)$ per parameter set.
|
||||
- [Axiom inventory](/docs/proofs/axiom-inventory) — the N4 cone's
|
||||
Lean-bridged algebraic axioms.
|
||||
@@ -0,0 +1,162 @@
|
||||
---
|
||||
title: FIPS 204 relationship
|
||||
description: What the threshold layer changes vs. single-party ML-DSA-65, and why the wire shape is preserved.
|
||||
---
|
||||
|
||||
Pulsar's headline claim is **output interchangeability** with FIPS 204: a
|
||||
signature produced by an $n$-of-$t$ threshold ceremony verifies under
|
||||
unmodified FIPS 204 `ML-DSA.Verify(pk, message, signature)`. This page
|
||||
explains what changes versus single-party ML-DSA-65 and why those changes
|
||||
do not alter the wire shape.
|
||||
|
||||
## What is shared with FIPS 204
|
||||
|
||||
| Element | Source |
|
||||
| --- | --- |
|
||||
| Ring `R_q = Z_q[X] / (X^256 + 1)`, `q = 8380417` | FIPS 204 §3.1 |
|
||||
| Parameters `(k, ℓ, η, τ, ω, …)` per ML-DSA-65 | FIPS 204 §4 |
|
||||
| Public matrix sampling (`ExpandA`) | FIPS 204 §3.5 Algorithm 32 |
|
||||
| Per-session masking sampling (`ExpandMask`) | FIPS 204 §3.6 |
|
||||
| Challenge derivation (`SampleInBall`, c̃) | FIPS 204 §3.7 |
|
||||
| External-mu hashing (`ExternalMu`, μ) | FIPS 204 §5.4.1 |
|
||||
| Hint derivation (`MakeHint`) | FIPS 204 §6.2 |
|
||||
| Norm and rejection checks | FIPS 204 §6.2 |
|
||||
| Signature packing σ = (c̃, z, h) | FIPS 204 §3.5.5 |
|
||||
|
||||
The wire shape and packed-signature codec are inherited verbatim. The
|
||||
EasyCrypt formalization names each FIPS 204 building block via the abstract
|
||||
ops in `lemmas/MLDSA65_Functional.ec` and ties them back to FIPS 204
|
||||
section references in `docs/fips-204-traceability.md`.
|
||||
|
||||
## What the threshold layer adds
|
||||
|
||||
The 2-round threshold protocol replaces the centralized computation of
|
||||
$\mathbf{z} = \mathbf{y} + c \cdot \mathbf{s_1}$ with a distributed
|
||||
computation that recovers the same $\mathbf{z}$ via Lagrange aggregation
|
||||
across the per-party partial responses.
|
||||
|
||||
Per-party partial response, abstractly:
|
||||
|
||||
$$
|
||||
\mathbf{z}_i = \mathbf{y}_i + c \cdot \mathbf{s}_{1,i}
|
||||
$$
|
||||
|
||||
where $\mathbf{s}_{1,i}$ is party $i$'s share of $\mathbf{s_1}$ from the
|
||||
Pedersen DKG.
|
||||
|
||||
Lagrange aggregation across the quorum $Q$:
|
||||
|
||||
$$
|
||||
\mathbf{z} = \sum_{i \in Q} \lambda_{i,Q} \cdot \mathbf{z}_i
|
||||
$$
|
||||
|
||||
where $\lambda_{i,Q}$ are the Lagrange coefficients for evaluating at $X = 0$
|
||||
on the quorum's index set.
|
||||
|
||||
By linearity of the Lagrange interpolation (Axiom 2,
|
||||
[`reconstruct_linear`](/docs/proofs/axiom-inventory)), the aggregated
|
||||
**z** equals:
|
||||
|
||||
$$
|
||||
\sum_{i \in Q} \lambda_{i,Q} \cdot (\mathbf{y}_i + c \cdot \mathbf{s}_{1,i})
|
||||
= \mathbf{y} + c \cdot \mathbf{s_1}
|
||||
$$
|
||||
|
||||
where **y** is the implicit quorum aggregation of the per-party masks
|
||||
and **s_1** is the Lagrange-reconstructed group secret. The aggregated
|
||||
**z** is the **same wire bytes** as the centralized FIPS 204
|
||||
computation.
|
||||
|
||||
## What the threshold layer leaves unchanged
|
||||
|
||||
All the **shape-preserving** stages — $\mathbf{w}$ derivation,
|
||||
$\mathbf{w_1}$ HighBits decomposition, $\tilde{c}$ derivation,
|
||||
$\mathbf{h}$ MakeHint computation, the FIPS 204 §6.2 norm and rejection
|
||||
checks — operate on the same polynomial-vector-over-$R_q^k$ algebra as
|
||||
single-party ML-DSA-65, with the per-party computations summed
|
||||
under Lagrange weights. The accepting kappa selection in the
|
||||
rejection-sampling loop is the same predicate
|
||||
(`accept_signing_attempt`) as the centralized model.
|
||||
|
||||
The result: the threshold combine and the centralized FIPS 204 Sign
|
||||
produce **the same 3309-byte ML-DSA-65 signature** on the same protocol
|
||||
inputs.
|
||||
|
||||
## What this gives a FIPS-validated verifier
|
||||
|
||||
A FIPS-validated ML-DSA-65 verifier (BoringSSL FIPS, AWS-LC, OpenSSL 3.0 PQ
|
||||
provider) consumes a Pulsar signature without code changes. The verifier
|
||||
sees:
|
||||
|
||||
- A 3309-byte payload with the FIPS 204 §3.5.5 layout.
|
||||
- A public key derived from the Pedersen-DKG group $\mathbf{t} = \mathbf{A} \mathbf{s_1} + \mathbf{s_2}$ — same wire shape as centralized FIPS 204 keygen.
|
||||
- The same FIPS 204 verification path.
|
||||
|
||||
This means:
|
||||
|
||||
1. Threshold-produced signatures verify under unmodified FIPS 204 verifiers.
|
||||
2. Existing FIPS-validated ML-DSA modules consume Pulsar certs without code
|
||||
changes.
|
||||
3. The threshold layer can be Class-N-claimed at NIST without a parallel
|
||||
algorithm standardization track.
|
||||
|
||||
## v0.2 vs v0.3 — aggregator-honesty caveat
|
||||
|
||||
Bit-identity to a single-party FIPS 204 signature is achieved without
|
||||
master-secret reconstruction only by the **v0.3 algebraic** aggregator:
|
||||
|
||||
| Variant | File | TCB at sign time |
|
||||
| --- | --- | --- |
|
||||
| v0.3 algebraic | `ref/go/pkg/pulsar/threshold_v03.go` | public-only material |
|
||||
| v0.2 transitional | `ref/go/pkg/pulsar/threshold_v02.go` | aggregator + master sk |
|
||||
|
||||
The v0.2 transitional aggregator reconstructs the master ML-DSA secret in
|
||||
aggregator memory and calls `mldsaSign(setup.SkBytes, ...)`. Output
|
||||
byte-equality holds, but the TCB at sign time includes the aggregator.
|
||||
v0.2 is documented for protocol-evolution traceability; **the N1 submission
|
||||
targets v0.3**.
|
||||
|
||||
The PULSAR-V03-1 closure record — the v0.3 byte-equality fix in
|
||||
v1.0.20 — lives in [`postmortem`](/docs/postmortem).
|
||||
|
||||
## Theorem framing — accepted-path correctness
|
||||
|
||||
The Class N1 byte-equality theorem is **conditional on acceptance**: *if*
|
||||
the threshold combine (and the single-party comparator) accepts — i.e.,
|
||||
passes the ML-DSA norm and rejection checks and the kappa rejection-sampling
|
||||
loop converged — *then* the produced byte string equals the centralized
|
||||
ML-DSA-65 signature on the same protocol-level inputs, under the stated
|
||||
layout, algebraic, and byte-walk assumptions.
|
||||
|
||||
Acceptance probability is tracked separately through the
|
||||
`accept_signing_attempt` predicate and the `mldsa_accept_lower_bound`
|
||||
operational bound; ML-DSA rejection sampling remains probabilistic per
|
||||
FIPS 204, and the deterministic EC model captures the accepted-path
|
||||
conditioning via the predicate rather than via probabilistic Hoare logic.
|
||||
|
||||
## Cross-validation evidence
|
||||
|
||||
Every KAT vector in `vectors/` is verified by three independent ML-DSA
|
||||
implementations (`test/interoperability/`):
|
||||
|
||||
1. The canonical Pulsar reference implementation (`github.com/luxfi/pulsar`).
|
||||
2. The FIPS 204 reference (`pq-crystals/dilithium` C reference).
|
||||
3. A third independent implementation (`cloudflare/circl` FIPS 204 verifier;
|
||||
BoringSSL FIPS or OpenSSL 3.0 PQ provider when available).
|
||||
|
||||
The 19/19 N1 subtests in `test/interoperability/n1_class_test.go`:
|
||||
|
||||
- `TestN1_SinglePartySignatures_VerifyUnderFIPS204`
|
||||
- `TestN1_ThresholdSignatures_VerifyUnderFIPS204`
|
||||
- `TestN1_TamperedSignatures_Rejected`
|
||||
- `TestN1_WrongMessage_Rejected`
|
||||
|
||||
all PASS as of `main` HEAD.
|
||||
|
||||
## See also
|
||||
|
||||
- [Protocol overview](/docs/protocol/overview) — system model, 2-round
|
||||
sketch.
|
||||
- [Axiom inventory](/docs/proofs/axiom-inventory) — the formal byte-equality
|
||||
chain.
|
||||
- [Postmortem](/docs/postmortem) — v1.0.20 ExpandA-convention fix.
|
||||
@@ -0,0 +1,4 @@
|
||||
{
|
||||
"title": "Protocol",
|
||||
"pages": ["overview", "fips-204", "dkg", "parameters"]
|
||||
}
|
||||
@@ -0,0 +1,182 @@
|
||||
---
|
||||
title: Protocol overview
|
||||
description: 2-round threshold ML-DSA sketch, system model, the byte-equality argument.
|
||||
---
|
||||
|
||||
Pulsar is a 2-round threshold construction over Module-LWE. The protocol
|
||||
skeleton is the same one Lux ships in production for Ring-LWE in
|
||||
[`luxfi/corona`](https://github.com/luxfi/corona), retargeted to the
|
||||
polynomial-vector-over-$R_q^k$ algebra that ML-DSA-65 uses natively.
|
||||
|
||||
## Notation
|
||||
|
||||
- $R_q = \mathbb{Z}_q[X] / (X^{256} + 1)$, $q = 8\,380\,417$.
|
||||
- Module dimension $k$, secret dimension $\ell$ (see [parameters](/docs/protocol/parameters)).
|
||||
- A single-party ML-DSA-65 keypair is $(\mathbf{s_1} \in R_q^\ell, \mathbf{s_2} \in R_q^k)$
|
||||
with public matrix $\mathbf{A} \in R_q^{k \times \ell}$ and public key
|
||||
$\mathbf{t} = \mathbf{A}\mathbf{s_1} + \mathbf{s_2}$.
|
||||
- A FIPS 204 signature has shape $\sigma = (\tilde{c}, \mathbf{z}, \mathbf{h})$.
|
||||
- A threshold ceremony has $n$ parties and reconstruction threshold $t$.
|
||||
|
||||
## System model
|
||||
|
||||
| Channel | Property | Purpose |
|
||||
| --- | --- | --- |
|
||||
| Broadcast | authenticated, eventual-delivery | round transcripts, public coins |
|
||||
| Point-to-point | authenticated, encrypted | private share / blind delivery |
|
||||
| Public bulletin | authenticated, append-only | DKG commitments, reshare records |
|
||||
|
||||
Channels are realized over TCP + TLS in the reference implementation.
|
||||
Production deployments (Lux consensus + Quasar) bind these to their existing
|
||||
P2P transport.
|
||||
|
||||
## Trusted parameters
|
||||
|
||||
The cyclotomic ring $R_q = \mathbb{Z}_q[X] / (X^{256} + 1)$ and parameters
|
||||
$(q, k, \ell, \eta, \beta, \omega, \dots)$ are inherited verbatim from FIPS 204
|
||||
ML-DSA-65. The hash family is SHAKE-256 (FIPS 202) + cSHAKE-256 / KMAC-256 /
|
||||
TupleHash-256 (NIST SP 800-185). Customization tags are pinned in
|
||||
`spec/pulsar.tex`.
|
||||
|
||||
No trusted setup beyond NIST primitives.
|
||||
|
||||
## Adversary model
|
||||
|
||||
### Static corruption (default)
|
||||
|
||||
The adversary $\mathcal{A}$ selects up to $t-1$ parties to corrupt **before**
|
||||
protocol start. From start to end, those $t-1$ parties are controlled; the
|
||||
remaining honest parties run the protocol faithfully.
|
||||
|
||||
$\mathcal{A}$ sees all broadcast messages and all authenticated point-to-point
|
||||
messages into corrupted parties. $\mathcal{A}$ learns each corrupted party's
|
||||
full state (secret share, per-round randomness, session values).
|
||||
$\mathcal{A}$ can selectively delay messages within the round window but cannot
|
||||
forge messages from honest parties on authenticated channels.
|
||||
|
||||
### Adaptive corruption (stronger)
|
||||
|
||||
$\mathcal{A}$ can corrupt up to $t-1$ parties at any time during the protocol,
|
||||
including mid-round, conditioned on the transcript so far. Once corrupted,
|
||||
a party remains corrupted. Adaptive security is a stretch goal for the first
|
||||
MPTC submission and a hard requirement for the second-round response.
|
||||
|
||||
### Mobile corruption (proactive resharing)
|
||||
|
||||
For long-lived deployments where the validator set rotates between epochs,
|
||||
the relevant model is HJKY97 mobile adversary: $\mathcal{A}$ can corrupt up
|
||||
to $t-1$ parties **per epoch**, with the corruption set varying across
|
||||
epochs. The MPTC submission documents the mobile-adversary game explicitly.
|
||||
|
||||
## Security goals
|
||||
|
||||
### Threshold unforgeability (TS-UF)
|
||||
|
||||
For any PPT adversary $\mathcal{A}$ controlling up to $t-1$ parties,
|
||||
$\mathcal{A}$ cannot produce a valid Pulsar signature $\sigma^*$ on any message
|
||||
$\mu^*$ that an honest signing ceremony has not produced.
|
||||
|
||||
### Output indistinguishability from FIPS 204
|
||||
|
||||
A Pulsar signature $\sigma$ on message $\mu$ against group public key $pk$ is
|
||||
computationally indistinguishable from a FIPS 204 ML-DSA signature on the
|
||||
same $(pk, \mu)$. **Pulsar achieves the stronger property of byte-equality**
|
||||
under the v0.3 algebraic aggregator.
|
||||
|
||||
### Robustness / identifiable abort
|
||||
|
||||
If a corrupted party deviates from the protocol, the honest parties:
|
||||
|
||||
1. Detect the deviation.
|
||||
2. Identify the deviating party.
|
||||
3. Produce signed evidence of the deviation suitable for
|
||||
slashing / reputation reduction.
|
||||
|
||||
Pulsar identifies aborting parties under synchronous network assumptions;
|
||||
asynchronous identifiable abort is out of scope for this submission.
|
||||
|
||||
### Bias resistance
|
||||
|
||||
The randomness used in each party's contribution (Gaussian samples, challenge
|
||||
polynomials) is statistically indistinguishable from uniform even given the
|
||||
adversary's view of corrupted parties' randomness.
|
||||
|
||||
### DKG soundness
|
||||
|
||||
Pedersen DKG over $R_q^k$ produces a public key $pk$ distributed uniformly
|
||||
over the valid M-LWE public-key space, with no party holding more than $1/n$
|
||||
partial information about the corresponding secret key.
|
||||
|
||||
## The 2-round signing protocol
|
||||
|
||||
The two rounds, in sketch (full spec: `spec/pulsar.tex` §4):
|
||||
|
||||
### Round 1 — commit
|
||||
|
||||
Each party $i$ in the quorum $Q$ samples its per-session masking values
|
||||
($\mathbf{y}_i \in R_q^\ell$ via ExpandMask) and emits a commitment to its
|
||||
contribution to $\mathbf{w} = \mathbf{A}\mathbf{y}$. The commitment carries the
|
||||
session identifier and the long-term identity public key for replay
|
||||
resistance.
|
||||
|
||||
### Round 2 — respond
|
||||
|
||||
After receiving the full Round-1 transcript and computing $\tilde{c}$ via
|
||||
ExpandH on the aggregated $\mathbf{w}_1 = \mathrm{HighBits}(\mathbf{w})$, each
|
||||
party $i$ emits its partial response $\mathbf{z}_i = \mathbf{y}_i + c \cdot
|
||||
\mathbf{s}_{1,i}$ where $\mathbf{s}_{1,i}$ is its share of $\mathbf{s}_1$.
|
||||
|
||||
### Combine — public-only aggregation
|
||||
|
||||
The aggregator performs Lagrange aggregation on the per-party responses to
|
||||
recover the centralized $\mathbf{z}$, then packs the FIPS 204 signature
|
||||
$\sigma = (\tilde{c}, \mathbf{z}, \mathbf{h})$. No master secret is ever
|
||||
reconstructed in aggregator memory.
|
||||
|
||||
## The byte-equality argument
|
||||
|
||||
The combine-side aggregation identity is, abstractly:
|
||||
|
||||
$$
|
||||
\mathrm{Lagrange}_Q\bigl(\{z_i\}_{i \in Q}\bigr) = \mathbf{y} + c \cdot \mathbf{s_1}
|
||||
$$
|
||||
|
||||
where $\mathbf{s_1}$ is the Lagrange-reconstructed group secret, $\mathbf{y}$
|
||||
is the implicit aggregation of the per-party masks, and $c$ is the challenge
|
||||
derived from the joint transcript via ExpandH. This is the algebraic content
|
||||
of [Axiom 5](/docs/proofs/axiom-inventory) (`threshold_partial_response_identity`)
|
||||
in the EasyCrypt proof, discharged by a proved Lean theorem
|
||||
(`Crypto/Threshold_Lagrange.lean::threshold_partial_response_identity`).
|
||||
|
||||
The signature is then packed via the FIPS 204 §3.5.5 packed-signature codec
|
||||
shared by both the threshold combine path and the centralized FIPS 204 Sign
|
||||
path; the codec round-trip is [Axiom 17](/docs/proofs/axiom-inventory)
|
||||
(`pack_unpack_n1_signature_roundtrip` in `Pulsar_N1.ec:817`).
|
||||
|
||||
Combining these two facts with the FIPS 204 §6.2 stage-level byte-walks
|
||||
yields the headline byte-equality theorem
|
||||
`pulsar_n1_byte_equality_extracted` in
|
||||
`proofs/easycrypt/Pulsar_N1_Extracted.ec`.
|
||||
|
||||
## Out of scope
|
||||
|
||||
Read [BLOCKERS.md](https://github.com/luxfi/pulsar/blob/main/BLOCKERS.md) for
|
||||
the authoritative list. Highlights:
|
||||
|
||||
- **No identifiable abort under network partition** — Pulsar identifies
|
||||
aborting parties under synchronous network assumptions only. Asynchronous
|
||||
identifiable abort requires a separate accountability layer.
|
||||
- **No 1-round signing** — the construction is 2-round by design. The
|
||||
rejection-sampling step inherent to FIPS 204 ML-DSA precludes a 1-round
|
||||
threshold variant without a non-NIST-standard preprocessing oracle.
|
||||
- **DKG without external randomness beacon** — Pulsar DKG produces unbiased
|
||||
coefficients under honest-majority assumptions but does not provide bias
|
||||
resistance under collusion. Production deployments bind a randomness beacon
|
||||
at the consensus layer.
|
||||
|
||||
## Next
|
||||
|
||||
- [FIPS 204 relationship](/docs/protocol/fips-204) — the byte-equality story
|
||||
in detail.
|
||||
- [DKG](/docs/protocol/dkg) — Pedersen DKG over $R_q^k$, proactive resharing.
|
||||
- [Parameters](/docs/protocol/parameters) — concrete parameter sets.
|
||||
@@ -0,0 +1,115 @@
|
||||
---
|
||||
title: Concrete parameters
|
||||
description: Pulsar-44 / -65 / -87 parameter sets, lattice estimator inputs, NIST MPTC compliance.
|
||||
---
|
||||
|
||||
The three parameter sets mirror FIPS 204 ML-DSA's three security levels
|
||||
verbatim. Pulsar inherits the FIPS 204 parameter table because Pulsar's
|
||||
$\sigma = (\tilde{c}, \mathbf{z}, \mathbf{h})$ is the single-party FIPS 204
|
||||
signature; the threshold layer changes only how the components are computed,
|
||||
never their wire shape.
|
||||
|
||||
## Parameter sets
|
||||
|
||||
| Parameter | Pulsar-44 | Pulsar-65 | Pulsar-87 |
|
||||
| --- | ---: | ---: | ---: |
|
||||
| NIST PQ category | 2 | 3 | 5 |
|
||||
| Classical security (bits) | $\geq 123$ | $\geq 182$ | $\geq 252$ |
|
||||
| Quantum security (bits) | $\geq 111$ | $\geq 165$ | $\geq 229$ |
|
||||
| Modulus $q$ | 8 380 417 | 8 380 417 | 8 380 417 |
|
||||
| Ring degree $n$ | 256 | 256 | 256 |
|
||||
| Module dimension $k$ | 4 | 6 | 8 |
|
||||
| Secret dimension $\ell$ | 4 | 5 | 7 |
|
||||
| Secret coefficient bound $\eta$ | 2 | 4 | 2 |
|
||||
| Challenge weight $\tau$ | 39 | 49 | 60 |
|
||||
| Hint bound $\omega$ | 80 | 55 | 75 |
|
||||
| Threshold $(n, t)$ | runtime | runtime | runtime |
|
||||
| Signature size (bytes) | 2420 | 3309 | 4627 |
|
||||
| Public key size (bytes) | 1312 | 1952 | 2592 |
|
||||
|
||||
Bit-security bounds come from FIPS 204 Appendix B (NIST's M-LWE / M-SIS
|
||||
analysis); Pulsar adopts them verbatim and does not independently re-derive
|
||||
lattice hardness.
|
||||
|
||||
The NIST MPTC submission targets **Pulsar-65** as the primary parameter set
|
||||
(category 3, recommended for the NIST classical $\geq 192$ bits tier);
|
||||
Pulsar-44 satisfies the required tier with margin, and Pulsar-87 covers
|
||||
category 5 for full ML-DSA coverage.
|
||||
|
||||
## Lattice-estimator inputs
|
||||
|
||||
`estimator/` restates the M-LWE instance for each parameter set so an
|
||||
auditor can plug it into a public estimator (e.g.,
|
||||
[`leaky-LWE-estimator`](https://github.com/lducas/leaky-LWE-Estimator)) and
|
||||
reproduce NIST's analysis. The estimator commit hash is pinned in
|
||||
`estimator/README.md`; `estimator/params.sage` generates the per-parameter
|
||||
instance files.
|
||||
|
||||
For a single parameter set, the estimator inputs are:
|
||||
|
||||
- $q$ (modulus)
|
||||
- $n$ (ring degree)
|
||||
- $k, \ell$ (module dimensions)
|
||||
- $\eta$ (secret coefficient bound)
|
||||
- $\sigma$ (Gaussian width — derived from $\eta$ per FIPS 204 §3.3)
|
||||
- Sample count $m = k \cdot n$ (M-LWE sample budget per public key)
|
||||
|
||||
The estimator reports per-attack-strategy lattice complexity (uSVP, primal,
|
||||
dual, BKZ) with adversary cost metrics matching NIST's FIPS 204 analysis.
|
||||
|
||||
## NIST MPTC compliance
|
||||
|
||||
From NIST IR 8214C §4.5:
|
||||
|
||||
**Required parameterization**: at least one parameter set with classical
|
||||
$\geq 128$ bits, NIST PQ category $\geq 1$, statistical $\geq 40$ bits.
|
||||
Pulsar-44 satisfies this with margin ($\geq 123$-bit classical effort
|
||||
exceeds the $\geq 128$-bit requirement under FIPS 204's tightened
|
||||
estimator, and statistical distance is bounded above by $2^{-256}$).
|
||||
|
||||
**Suggested parameterization**: at least one parameter set with classical
|
||||
$\geq 192$ bits, NIST PQ category $\geq 3$, statistical $\geq 64$ bits.
|
||||
**Pulsar-65 satisfies this**.
|
||||
|
||||
Pulsar-87 covers NIST PQ category 5 for full ML-DSA coverage.
|
||||
|
||||
## Threshold parameters $(n, t)$
|
||||
|
||||
Unlike $(k, \ell, \eta, \tau, \omega, \dots)$, the threshold $(n, t)$ is
|
||||
**runtime configurable**. The reference implementation accepts any
|
||||
$1 \leq t \leq n$ with $n$ bounded by deployment constraints:
|
||||
|
||||
- $n \leq 256$ — small-committee path (`shamir.go`, `largeshamir.go`
|
||||
via the small-path branch). Uses GF(257) for Lagrange interpolation.
|
||||
- $n > 256$ — large-committee path (`large_dkg.go`, `large_threshold.go`,
|
||||
`large_reshare.go`). Uses GF($q$) for Lagrange interpolation.
|
||||
|
||||
Both paths produce the same FIPS 204 byte-equal signature. The KAT vectors
|
||||
in `vectors/` exercise the small-committee path; the large-committee path
|
||||
has its own test suite (`large_e2e_test.go`, `largeshamir_test.go`) but no
|
||||
committed KAT vectors in this submission package.
|
||||
|
||||
The v1.0.7 release made both paths **uniform under the identity stage**
|
||||
(CR-6, CR-7, CR-8 closures on both paths) so the same identity layer at
|
||||
`pulsar.GenerateIdentity` / `IdentityKey` / `IdentityDirectory` covers
|
||||
both committee sizes.
|
||||
|
||||
## Cyclotomic ring
|
||||
|
||||
All parameter sets share the same cyclotomic ring:
|
||||
|
||||
$$
|
||||
R_q = \mathbb{Z}_q[X] / (X^{256} + 1), \quad q = 8\,380\,417 = 2^{23} - 2^{13} + 1
|
||||
$$
|
||||
|
||||
This is the FIPS 204 ML-DSA ring. The NTT (Number-Theoretic Transform) is
|
||||
the same one libjade uses for the single-party ML-DSA-65 baseline;
|
||||
$2n$-th root of unity exists in $\mathbb{Z}_q$, so the NTT is exact (no
|
||||
embedding overhead).
|
||||
|
||||
## See also
|
||||
|
||||
- [Protocol overview](/docs/protocol/overview) — system model and 2-round sketch.
|
||||
- [FIPS 204 relationship](/docs/protocol/fips-204) — what the threshold
|
||||
layer changes vs. centralized ML-DSA-65.
|
||||
- [KAT format](/docs/reference/kat) — vectors and regeneration.
|
||||
@@ -0,0 +1,283 @@
|
||||
---
|
||||
title: Go API reference
|
||||
description: Exported types and functions in github.com/luxfi/pulsar/ref/go/pkg/pulsar.
|
||||
---
|
||||
|
||||
The reference implementation is a single flat package at
|
||||
`github.com/luxfi/pulsar/ref/go/pkg/pulsar`. This page covers the
|
||||
load-bearing exports. Full godoc:
|
||||
[`pkg.go.dev/github.com/luxfi/pulsar/ref/go/pkg/pulsar`](https://pkg.go.dev/github.com/luxfi/pulsar/ref/go/pkg/pulsar).
|
||||
|
||||
**Status — pre-spec-freeze.** The exported API will change up to the spec
|
||||
encoding freeze (target end of August 2026). After freeze the API is fixed
|
||||
and a `v0.1` tag is cut.
|
||||
|
||||
All cryptographic operations route through:
|
||||
|
||||
- `hash` — NIST SP 800-185 (cSHAKE256 / KMAC256 / TupleHash256) only
|
||||
- `primitives` — Module-LWE polynomial-vector arithmetic
|
||||
- `sign` — 2-round threshold sign protocol
|
||||
- `dkg` — Pedersen DKG over $R_q^k$
|
||||
- `reshare` — proactive resharing with beacon-randomized quorum
|
||||
- `fmt` — wire encoding / KAT format
|
||||
|
||||
All logging — including for any error path — uses `github.com/luxfi/log`.
|
||||
The standard library's `log` package is **forbidden** in this module:
|
||||
a secret-correlated value reaching stdout is a side channel even at debug
|
||||
level (HIP-0077 red review F8). Enforced by a CI lint, not just convention
|
||||
(`scripts/checks/test/no-secret-logs.sh`).
|
||||
|
||||
## Parameter modes
|
||||
|
||||
```go
|
||||
type Mode uint8
|
||||
|
||||
const (
|
||||
ModeUnspecified Mode = 0
|
||||
ModeP44 Mode = 44 // NIST PQ Category 2
|
||||
ModeP65 Mode = 65 // NIST PQ Category 3 (production target)
|
||||
ModeP87 Mode = 87 // NIST PQ Category 5
|
||||
)
|
||||
```
|
||||
|
||||
`Pulsar-65` is the production target for Lux consensus (`SigSchemePulsar65`).
|
||||
|
||||
```go
|
||||
type Params struct {
|
||||
Mode Mode
|
||||
|
||||
// FIPS 204 module-LWE shape.
|
||||
K int // module dimension
|
||||
L int // secret dimension (ℓ)
|
||||
Eta int // secret coefficient bound η
|
||||
Tau int // challenge weight τ
|
||||
Omega int // hint bound ω
|
||||
Q uint64 // 8 380 417 — FIPS 204 prime modulus
|
||||
N int // 256 — ring degree
|
||||
|
||||
PublicKeySize int
|
||||
PrivateKeySize int
|
||||
SignatureSize int
|
||||
|
||||
ShamirPrime uint64
|
||||
MaxRestart uint32
|
||||
}
|
||||
|
||||
func ParamsFor(mode Mode) (*Params, error)
|
||||
func MustParamsFor(mode Mode) *Params
|
||||
```
|
||||
|
||||
Source: `ref/go/pkg/pulsar/params.go`.
|
||||
|
||||
## Single-party signing
|
||||
|
||||
```go
|
||||
func GenerateKey(params *Params, rng io.Reader) (*PrivateKey, error)
|
||||
func KeyFromSeed(params *Params, seed [SeedSize]byte) (*PrivateKey, error)
|
||||
|
||||
const SeedSize = 32
|
||||
|
||||
type PrivateKey struct { /* ... */ }
|
||||
type PublicKey struct { /* ... */ }
|
||||
|
||||
func (sk *PrivateKey) Public() *PublicKey
|
||||
func (pk *PublicKey) Equal(other *PublicKey) bool
|
||||
|
||||
func Sign(
|
||||
params *Params,
|
||||
sk *PrivateKey,
|
||||
message, ctx []byte,
|
||||
randomized bool,
|
||||
rng io.Reader,
|
||||
) (*Signature, error)
|
||||
```
|
||||
|
||||
`Sign` produces a 3309-byte (for Pulsar-65) `*Signature` wire-identical to
|
||||
`cloudflare/circl`'s `mldsa65.Sign` from the same seed and message.
|
||||
`randomized=true` (the default for production) uses the FIPS 204 hedged
|
||||
variant; `randomized=false` is deterministic and KAT-reproducible. If
|
||||
`rng` is `nil` and `randomized=true`, `crypto/rand.Reader` is used.
|
||||
|
||||
Source: `ref/go/pkg/pulsar/sign.go`, `keygen.go`.
|
||||
|
||||
## Threshold signing — v0.3 algebraic (recommended)
|
||||
|
||||
The algebraic aggregator is **public-only at sign time** — no master
|
||||
secret reconstruction in aggregator memory. This is the N1 submission
|
||||
target.
|
||||
|
||||
```go
|
||||
type AlgebraicSetup struct { /* ... */ }
|
||||
type AlgebraicKeyShare struct { /* ... */ }
|
||||
|
||||
func DealAlgebraicV03Shares(
|
||||
params *Params,
|
||||
rng io.Reader,
|
||||
quorum []NodeID,
|
||||
n, t int,
|
||||
) (*AlgebraicSetup, []*AlgebraicKeyShare, error)
|
||||
|
||||
type AlgebraicRound1Message struct { /* ... */ }
|
||||
type AlgebraicRound2Message struct { /* ... */ }
|
||||
|
||||
type AlgebraicThresholdSigner struct { /* ... */ }
|
||||
|
||||
func NewAlgebraicThresholdSigner(
|
||||
params *Params,
|
||||
setup *AlgebraicSetup,
|
||||
share *AlgebraicKeyShare,
|
||||
sid [16]byte,
|
||||
message []byte,
|
||||
) (*AlgebraicThresholdSigner, error)
|
||||
|
||||
func (s *AlgebraicThresholdSigner) Round1() (*AlgebraicRound1Message, error)
|
||||
func (s *AlgebraicThresholdSigner) Round2W(
|
||||
round1 []*AlgebraicRound1Message,
|
||||
) (*AlgebraicRound2Message, *AbortEvidence, error)
|
||||
func (s *AlgebraicThresholdSigner) Round2Sign(
|
||||
round1 []*AlgebraicRound1Message,
|
||||
peerW map[NodeID]polyVec,
|
||||
) (*AlgebraicRound2Message, *AbortEvidence, error)
|
||||
|
||||
func AlgebraicAggregate(
|
||||
params *Params,
|
||||
setup *AlgebraicSetup, // public-only material
|
||||
sid [16]byte,
|
||||
message []byte,
|
||||
round1 []*AlgebraicRound1Message,
|
||||
round2 []*AlgebraicRound2Message,
|
||||
) (*Signature, error)
|
||||
```
|
||||
|
||||
`AlgebraicAggregate` has **no** `*PrivateKey`, **no** `SkBytes`, **no**
|
||||
`seed` parameter — its public-BFT safety contract is enforced by a Go AST
|
||||
walk in `TestAlgebraic_NoSkAccess` that fails if any sk-bearing primitive
|
||||
is reachable from `AlgebraicAggregate`'s body, including indirect dispatch
|
||||
(hardened in v1.0.22).
|
||||
|
||||
Source: `ref/go/pkg/pulsar/threshold_v03.go`.
|
||||
|
||||
## Threshold signing — v0.2 transitional (legacy)
|
||||
|
||||
The transitional aggregator reconstructs the master ML-DSA secret in
|
||||
aggregator memory and calls `mldsaSign(setup.SkBytes, ...)`. Output
|
||||
byte-equality holds, but the TCB at sign time includes the aggregator.
|
||||
v0.2 is documented for protocol-evolution traceability; the N1 submission
|
||||
targets v0.3.
|
||||
|
||||
```go
|
||||
type TransitionalSetup struct {
|
||||
/* SkBytes — present; declared as v0.2 TCB defect */
|
||||
/* ... */
|
||||
}
|
||||
type TransitionalThresholdSigner struct { /* ... */ }
|
||||
|
||||
func DealTransitionalShares(/* ... */) (*TransitionalSetup, []*PolyKeyShare, error)
|
||||
func NewTransitionalThresholdSigner(/* ... */) (*TransitionalThresholdSigner, error)
|
||||
|
||||
func (s *TransitionalThresholdSigner) Round1() (*TransitionalRound1Message, error)
|
||||
func (s *TransitionalThresholdSigner) Round2(
|
||||
round1 []*TransitionalRound1Message,
|
||||
) (*TransitionalRound2Message, *AbortEvidence, error)
|
||||
|
||||
func TransitionalAggregate(/* SkBytes-dependent */) (*Signature, error)
|
||||
```
|
||||
|
||||
`TestTransitional_DependsOnSkBytes` runs the full Round1/Round2 cycle
|
||||
then sets `setup.SkBytes = nil` and asserts `TransitionalAggregate`
|
||||
returns `ErrTransitionalNoSetup`. The test currently PASSES (because v0.2
|
||||
indeed depends on SkBytes); the original gate expected this to FAIL once
|
||||
v0.3 shipped — the actual closure shipped v0.3 as a parallel track and
|
||||
left v0.2 honest. Both paths now coexist.
|
||||
|
||||
Source: `ref/go/pkg/pulsar/threshold_v02.go`.
|
||||
|
||||
## DKG
|
||||
|
||||
Pedersen DKG over $R_q^k$ with identity-bound coefficient commitments and
|
||||
KEM-wrapped share envelopes (CR-6 + CR-8 closures via the identity layer).
|
||||
|
||||
```go
|
||||
type DKGSession struct { /* ... */ }
|
||||
type DKGRound1Msg struct { /* ... */ }
|
||||
type DKGRound2Msg struct { /* ... */ }
|
||||
type DKGOutput struct { /* ... */ }
|
||||
|
||||
func (s *DKGSession) Round1() (*DKGRound1Msg, error)
|
||||
func (s *DKGSession) Round2(round1 []*DKGRound1Msg) (*DKGRound2Msg, error)
|
||||
func (s *DKGSession) Round3(
|
||||
round1 []*DKGRound1Msg,
|
||||
round2 []*DKGRound2Msg,
|
||||
) (*DKGOutput, error)
|
||||
```
|
||||
|
||||
Source: `ref/go/pkg/pulsar/dkg.go`. Large-committee variant
|
||||
(beyond $n = 256$ — GF($q$) instead of GF(257)) at
|
||||
`ref/go/pkg/pulsar/large_dkg.go`.
|
||||
|
||||
## Identity layer (mandatory)
|
||||
|
||||
Per CR-6, CR-7, CR-8 closures:
|
||||
|
||||
```go
|
||||
type IdentityKey struct { /* ML-DSA-65 long-term identity */ }
|
||||
type IdentityPublicKey struct { /* ... */ }
|
||||
type IdentityDirectory map[NodeID]*IdentityPublicKey
|
||||
|
||||
func GenerateIdentity(rng io.Reader) (*IdentityKey, error)
|
||||
func NewIdentityDirectory(entries map[NodeID]*IdentityPublicKey) (IdentityDirectory, error)
|
||||
func (k *IdentityKey) PublicKey() *IdentityPublicKey
|
||||
|
||||
// Per-pair authenticated channel with ML-KEM-768 wrapping.
|
||||
func EstablishSession(/* ... */) (/* ... */, error)
|
||||
func SymmetricSession (/* ... */) (/* ... */, error)
|
||||
func DeriveSessionKey(myID, peerID NodeID, sid [16]byte, mySS, peerSS []byte) ([32]byte, error)
|
||||
```
|
||||
|
||||
Source: `ref/go/pkg/pulsar/identity.go`.
|
||||
|
||||
## Proactive resharing
|
||||
|
||||
```go
|
||||
type ReshareSession struct { /* ... */ }
|
||||
type KeyShare struct { /* ... */ }
|
||||
|
||||
func (s *ReshareSession) SetPriorGroupPubkey(pk *PublicKey)
|
||||
func (s *ReshareSession) InReshareQuorum() bool
|
||||
func (s *ReshareSession) Round1() (*DKGRound1Msg, error)
|
||||
func (s *ReshareSession) Round2(round1 []*DKGRound1Msg) (*DKGRound2Msg, error)
|
||||
func (s *ReshareSession) Round3(
|
||||
round1 []*DKGRound1Msg,
|
||||
round2 []*DKGRound2Msg,
|
||||
) (*KeyShare, *AbortEvidence, error)
|
||||
```
|
||||
|
||||
Source: `ref/go/pkg/pulsar/reshare.go`.
|
||||
|
||||
## Errors
|
||||
|
||||
Each subsystem declares its own sentinel errors with descriptive names
|
||||
that match the failure mode:
|
||||
|
||||
- `ErrNilKey`, `ErrModeMismatch`, `ErrCtxTooLong` (`sign.go:30`)
|
||||
- `ErrTransitionalNoSetup`, `ErrTransitionalRound1MACBad`,
|
||||
`ErrTransitionalRound2MACBad`, `ErrTransitionalRound2CommitBad`,
|
||||
`ErrTransitionalRestart` (`threshold_v02.go`)
|
||||
- DKG, reshare, identity sentinels in their respective files
|
||||
|
||||
`*AbortEvidence` carries signed evidence of an identifiable abort
|
||||
suitable for slashing.
|
||||
|
||||
## Determinism for KAT replay
|
||||
|
||||
The KAT regen pipeline (`scripts/gen_vectors.sh`) seeds all randomness
|
||||
from a 48-byte master seed. Calling `Sign` with `randomized=false` and
|
||||
the corresponding deterministic reader produces a byte-identical
|
||||
signature on every architecture. CI runs the regen on every commit and
|
||||
compares against the committed vectors.
|
||||
|
||||
## See also
|
||||
|
||||
- [Getting started](/docs/getting-started) — end-to-end usage.
|
||||
- [KAT format](/docs/reference/kat) — vector schema and regen.
|
||||
- [Interop](/docs/reference/interop) — cross-validation harness.
|
||||
@@ -0,0 +1,129 @@
|
||||
---
|
||||
title: Interoperability harness
|
||||
description: Cross-validation of every Pulsar signature against the FIPS 204 reference (pq-crystals/dilithium) and a third independent implementation (cloudflare/circl).
|
||||
---
|
||||
|
||||
The Class N1 byte-equality claim is **load-bearing**: a Pulsar signature
|
||||
must verify under any FIPS 204-conformant ML-DSA verifier without
|
||||
modification. The interoperability harness at `test/interoperability/`
|
||||
makes this verifiable in CI.
|
||||
|
||||
## Two verifier targets
|
||||
|
||||
| Verifier | File | Linkage |
|
||||
| --- | --- | --- |
|
||||
| `cloudflare/circl` FIPS 204 | `test/interoperability/n1_class_test.go` | Direct Go import |
|
||||
| `pq-crystals/dilithium` reference | `test/interoperability/pq_crystals/pq_crystals_class_test.go` | C reference compiled to cgo bindings |
|
||||
|
||||
`cloudflare/circl` is the in-tree differential target for fast iteration
|
||||
on a Go-only test stack. `pq-crystals/dilithium` is the FIPS 204
|
||||
**editor's reference** implementation; cross-validation against it is the
|
||||
authoritative test for FIPS 204 conformance.
|
||||
|
||||
When `BoringSSL FIPS` or `OpenSSL 3.0 PQ provider` is available in the
|
||||
test environment, a third verifier is added to the comparison.
|
||||
|
||||
## Subtests under `n1_class_test.go`
|
||||
|
||||
```text
|
||||
TestN1_SinglePartySignatures_VerifyUnderFIPS204
|
||||
TestN1_ThresholdSignatures_VerifyUnderFIPS204
|
||||
TestN1_TamperedSignatures_Rejected
|
||||
TestN1_WrongMessage_Rejected
|
||||
```
|
||||
|
||||
19 subtests total across the four top-level tests, all PASS on the tip
|
||||
of `main`. The mirror suite under `test/interoperability/pq_crystals/`
|
||||
covers the same cases against the FIPS 204 C reference.
|
||||
|
||||
## Running the harness
|
||||
|
||||
Whole interop:
|
||||
|
||||
```bash
|
||||
bash scripts/checks/test/interop.sh
|
||||
```
|
||||
|
||||
Just the circl subtests:
|
||||
|
||||
```bash
|
||||
cd ref/go
|
||||
GOWORK=off go test -count=1 -short -timeout 300s ./test/interoperability/...
|
||||
```
|
||||
|
||||
The full `cgo` build (pq-crystals) requires the C reference checked out
|
||||
under `test/interoperability/pq_crystals/dilithium-ref/` and is gated by
|
||||
a Go build tag (`interop_cgo`).
|
||||
|
||||
## What each subtest proves
|
||||
|
||||
### `TestN1_SinglePartySignatures_VerifyUnderFIPS204`
|
||||
|
||||
Drives `Sign(params, sk, message, ctx, deterministic, rng)` for each of
|
||||
the three Pulsar parameter sets, then verifies the resulting signature
|
||||
under `circl.mldsa{44,65,87}.Verify`. Asserts byte-equality of the Pulsar
|
||||
signature with the circl output on the same seed.
|
||||
|
||||
### `TestN1_ThresholdSignatures_VerifyUnderFIPS204`
|
||||
|
||||
Runs the full v0.3 algebraic threshold ceremony (DKG → R1 → R2 → Combine)
|
||||
for a small $(n, t)$ sweep, then verifies each combined signature under
|
||||
`circl.mldsa65.Verify`. Asserts the combined signature is the same byte
|
||||
string as a centralized FIPS 204 sign on the Lagrange-reconstructed group
|
||||
secret.
|
||||
|
||||
### `TestN1_TamperedSignatures_Rejected`
|
||||
|
||||
Flips a bit in the combined signature at each of three positions
|
||||
(challenge, response, hint) and asserts `circl.mldsa65.Verify` returns
|
||||
`false`.
|
||||
|
||||
### `TestN1_WrongMessage_Rejected`
|
||||
|
||||
Verifies a valid signature against a different message and asserts the
|
||||
verifier rejects.
|
||||
|
||||
## Cross-impl differential testing
|
||||
|
||||
The per-push gate also runs a **differential fuzz** between Pulsar's
|
||||
single-party `Sign` and `circl.mldsa65.Sign` on randomized inputs. Any
|
||||
byte-level divergence is a fuzz-discovered bug and a release blocker.
|
||||
|
||||
Nightly:
|
||||
|
||||
```bash
|
||||
./scripts/nightly.sh
|
||||
# 1h-per-target Go native fuzz
|
||||
# 1h-per-target differential fuzz against cloudflare/circl
|
||||
```
|
||||
|
||||
## What this does not cover
|
||||
|
||||
- **ACVP / CAVP**: lab-validated algorithm conformance against the NIST
|
||||
ACVP ML-DSA harness is a downstream track. The reference implementation
|
||||
produces ACVP-compatible JSON; the lab engagement is downstream of this
|
||||
submission.
|
||||
- **FIPS 140-3 module validation**: applies to a packaged crypto module,
|
||||
not to this reference implementation.
|
||||
- **Negative validity beyond the four subtests** — see `test/negative/`
|
||||
for malformed pk / sk / sig / ctx-length / message-length boundary
|
||||
cases, run on every per-push gate.
|
||||
|
||||
## Source pointers
|
||||
|
||||
- `test/interoperability/n1_class_test.go` — circl cross-validation.
|
||||
- `test/interoperability/pq_crystals/` — pq-crystals C reference
|
||||
bindings.
|
||||
- `test/interoperability/pq_crystals/dilithium-ref/` — pinned upstream
|
||||
C reference (fetched on demand).
|
||||
- `test/negative/` — boundary and malformed-input tests.
|
||||
- `test/fuzz/` — Go native fuzz harnesses.
|
||||
- `bench/` — performance benchmarks (M1 Max, Go 1.26.2; KeyGen / Sign /
|
||||
Verify medians per parameter set).
|
||||
|
||||
## See also
|
||||
|
||||
- [KAT format](/docs/reference/kat) — vectors driven through the harness.
|
||||
- [Postmortem](/docs/postmortem) — the v1.0.20 ExpandA-convention fix was
|
||||
caught by this harness when the tip-of-`main` v0.3 cycle stopped
|
||||
byte-matching `circl.mldsa65.Sign`.
|
||||
@@ -0,0 +1,155 @@
|
||||
---
|
||||
title: KAT format
|
||||
description: Known-answer test vectors — schema, regeneration, and cross-validation.
|
||||
---
|
||||
|
||||
The `vectors/` directory holds Pulsar's known-answer test (KAT) vectors.
|
||||
Every entry is **deterministic from a 48-byte master seed** —
|
||||
reproducibility is the load-bearing CI invariant. `scripts/gen_vectors.sh`
|
||||
must produce byte-identical output on any fresh checkout; drift is a CI
|
||||
failure.
|
||||
|
||||
## File layout
|
||||
|
||||
| File | Format | Purpose |
|
||||
| --- | --- | --- |
|
||||
| `vectors/kat-v1.json` | NIST MPTC §IO-Testing | Full per-ceremony vectors |
|
||||
| `vectors/kat-v1.rsp` | CAVS-style response file | Legacy ACVP-inspired tooling compat |
|
||||
| `vectors/dkg.json` | per-DKG-run | DKG transcripts |
|
||||
| `vectors/keygen.json` | per-keypair | Key-generation vectors |
|
||||
| `vectors/sign.json` | per-single-party-sign | Single-party signing vectors for cross-validation |
|
||||
| `vectors/threshold-sign.json` | per-ceremony | Threshold-signing vectors |
|
||||
| `vectors/verify.json` | per-signature | FIPS 204 verification vectors |
|
||||
| `vectors/transcripts/n*-t*.jsonl` | per-line ceremony | Full-protocol KATs per $(n, t)$ sweep |
|
||||
|
||||
## Per-entry schema (`kat-v1.json`)
|
||||
|
||||
Each entry in `kat-v1.json` is a single threshold ceremony with the full
|
||||
deterministic transcript:
|
||||
|
||||
```json
|
||||
{
|
||||
"n": 5,
|
||||
"t": 3,
|
||||
"party_seeds": ["..."],
|
||||
"public_params": {"mode": "Pulsar-65", "...": "..."},
|
||||
"shares": ["..."],
|
||||
"commitments": ["..."],
|
||||
"preprocessing_transcript": {"...": "..."},
|
||||
"message": "0xdeadbeef...",
|
||||
"per_party_messages": [{"round1": "...", "round2": "..."}],
|
||||
"final_signature": "0x...",
|
||||
"verify_result": true,
|
||||
"abort_evidence": null
|
||||
}
|
||||
```
|
||||
|
||||
A `null` `abort_evidence` indicates the ceremony completed without
|
||||
identifying any party as deviating from the protocol.
|
||||
|
||||
## $(n, t)$ sweep coverage
|
||||
|
||||
The committed transcript vectors cover:
|
||||
|
||||
| $(n, t)$ | File |
|
||||
| --- | --- |
|
||||
| (3, 2) | `vectors/transcripts/n3-t2.jsonl` |
|
||||
| (5, 3) | `vectors/transcripts/n5-t3.jsonl` |
|
||||
| (7, 5) | `vectors/transcripts/n7-t5.jsonl` |
|
||||
| (10, 7) | `vectors/transcripts/n10-t7.jsonl` |
|
||||
| (16, 11) | `vectors/transcripts/n16-t11.jsonl` |
|
||||
| (32, 21) | `vectors/transcripts/n32-t21.jsonl` |
|
||||
|
||||
Each line in a `.jsonl` file is a complete protocol run.
|
||||
|
||||
The small-committee path covers $n \leq 256$. The large-committee path
|
||||
(`large_e2e_test.go`, `largeshamir_test.go`) is exercised separately and
|
||||
has no committed KAT vectors in this submission package — the byte stream
|
||||
is identical to the small-committee path up to the wire encoding of the
|
||||
$(n, t)$ field.
|
||||
|
||||
## Determinism
|
||||
|
||||
Every entry in `kat-v1.json` is reproducible from a `master_seed` (a
|
||||
48-byte hex value at the head of the file):
|
||||
|
||||
```bash
|
||||
./scripts/gen_vectors.sh
|
||||
# emits vectors/kat-v1.json byte-identical to the committed file
|
||||
```
|
||||
|
||||
The KAT generator binary lives at `ref/go/cmd/genkat/`. It imports the
|
||||
canonical algorithm sources from `ref/go/pkg/pulsar/` and runs each
|
||||
ceremony with the deterministic randomness reader seeded from
|
||||
`master_seed`. CI runs the regen on every commit and compares against the
|
||||
committed vectors:
|
||||
|
||||
```bash
|
||||
bash scripts/checks/test/kat.sh
|
||||
```
|
||||
|
||||
A KAT mismatch on this gate is a release blocker.
|
||||
|
||||
## Cross-validation against FIPS 204
|
||||
|
||||
The headline Class N1 interchangeability claim requires every
|
||||
`final_signature` in `kat-v1.json` to verify against unmodified FIPS 204
|
||||
`ML-DSA.Verify(pk, message, signature)` returning `accept`. The
|
||||
cross-validation harness at `test/interoperability/` runs each KAT
|
||||
through three independent ML-DSA implementations:
|
||||
|
||||
1. The canonical Pulsar reference (`github.com/luxfi/pulsar`).
|
||||
2. The FIPS 204 reference (`pq-crystals/dilithium` C reference).
|
||||
3. A third independent implementation
|
||||
([`cloudflare/circl`](https://github.com/cloudflare/circl) FIPS 204
|
||||
verifier; BoringSSL FIPS or OpenSSL 3.0 PQ provider when available).
|
||||
|
||||
A KAT mismatch with any of the three is a release blocker.
|
||||
|
||||
```bash
|
||||
bash scripts/checks/test/interop.sh
|
||||
```
|
||||
|
||||
## ACVP / CAVP positioning
|
||||
|
||||
The reference implementation produces ACVP-compatible JSON via
|
||||
`scripts/gen_vectors.sh`. The ACVP test vector format
|
||||
([NIST ACVP ML-DSA draft](https://pages.nist.gov/ACVP/draft-celi-acvp-ml-dsa.html))
|
||||
is a downstream lab-validation track and not part of the MPTC
|
||||
algorithm-level submission.
|
||||
|
||||
The `kat-v1.rsp` CAVS-style response file ships alongside the JSON for
|
||||
legacy ACVP-inspired tooling that expects the older CAVS format.
|
||||
|
||||
## Status (per `vectors/README.md`)
|
||||
|
||||
- KAT generator at `ref/go/cmd/genkat` — shipped.
|
||||
- First v1 KAT set — shipped.
|
||||
- FIPS 204 cross-validation — wired in `test/interoperability/`, 19/19 N1
|
||||
subtests PASS.
|
||||
- Independent-impl cross-validation — circl wired; pq-crystals C ref
|
||||
wired; BoringSSL/OpenSSL when available.
|
||||
- Transcript coverage at $(n, t) \in \{(3, 2), (5, 3), (7, 5), (10, 7),
|
||||
(16, 11), (32, 21)\}$.
|
||||
|
||||
## Regenerating after a source change
|
||||
|
||||
When `ref/go/pkg/pulsar/` semantics change, `scripts/gen_vectors.sh`
|
||||
regenerates the KATs from the in-tree sources. The cut-submission
|
||||
workflow includes the regen:
|
||||
|
||||
```bash
|
||||
./scripts/cut-submission.sh # dry-run; no tarball
|
||||
./scripts/cut-submission.sh submission-2026-11-16 # production cut + tag
|
||||
```
|
||||
|
||||
The cut script verifies a clean tree, verifies all proof gates are green,
|
||||
regenerates the KATs from the in-tree canonical implementation, re-runs
|
||||
the round-trip replay tests, tars the entire submission checkout, and
|
||||
prints the SHA-256.
|
||||
|
||||
## See also
|
||||
|
||||
- [Interop](/docs/reference/interop) — cross-validation harness details.
|
||||
- [API reference](/docs/reference/api) — `KeyFromSeed`, `Sign` for
|
||||
reproducing single-party KATs locally.
|
||||
@@ -0,0 +1,4 @@
|
||||
{
|
||||
"title": "Reference",
|
||||
"pages": ["api", "kat", "interop"]
|
||||
}
|
||||
@@ -0,0 +1,113 @@
|
||||
---
|
||||
title: Security policy
|
||||
description: Vulnerability disclosure, in-scope vs out-of-scope findings, CVE assignment, MPTC public-analysis process.
|
||||
---
|
||||
|
||||
## Reporting vulnerabilities
|
||||
|
||||
Report cryptographic or implementation vulnerabilities privately to
|
||||
**[email protected]** — encrypted with the team key at
|
||||
[`lux.network/security/key.asc`](https://lux.network/security/key.asc).
|
||||
Public disclosure happens after a fix lands and downstream consumers
|
||||
have had a 14-day private window.
|
||||
|
||||
## In-scope
|
||||
|
||||
- Specification ambiguity that leads to exploitable verifier behaviour.
|
||||
- Threshold-protocol soundness gaps (forgery, key recovery, share
|
||||
extraction, rogue-key, adaptive-corruption breaks).
|
||||
- Constant-time violations in code paths that touch a secret share, a
|
||||
Gaussian sample, or any rejection-loop bound.
|
||||
- KAT mismatches with the FIPS 204 reference — output interchangeability
|
||||
is the headline claim, so KAT divergence is high-severity.
|
||||
- Information leaks via logging, panics on secret-correlated paths, or
|
||||
variable-time equality.
|
||||
|
||||
## Out of scope
|
||||
|
||||
- Performance or implementation efficiency complaints — file an issue.
|
||||
- DoS attacks against the reference implementation that don't affect the
|
||||
threshold-correctness invariants.
|
||||
- Issues exclusively in upstream `luxfi/corona` (R-LWE sibling) — file
|
||||
there.
|
||||
- Pre-spec-freeze API ergonomics — the API will change up to the spec
|
||||
encoding freeze (target end of August 2026). After freeze the API is
|
||||
fixed.
|
||||
|
||||
## CVE assignment
|
||||
|
||||
Pulsar maintainers will request CVEs for any in-scope vulnerability
|
||||
prior to public disclosure. CVE numbers will be embedded in the ePrint
|
||||
changelog and the release tag's commit message.
|
||||
|
||||
## NIST MPTC submission disclosures
|
||||
|
||||
Findings discovered after the 2026-Nov-16 MPTC package submission
|
||||
deadline will be added to the submission's "known limitations" appendix
|
||||
and disclosed publicly per NIST's MPTC public-analysis process. There is
|
||||
no embargo window for findings against actively-submitted MPTC packages.
|
||||
|
||||
## Threat model summary
|
||||
|
||||
For the full threat model, see
|
||||
[`docs/threat-model.md` in the repository](https://github.com/luxfi/pulsar/blob/main/docs/threat-model.md).
|
||||
Highlights:
|
||||
|
||||
### Adversary classes
|
||||
|
||||
- **Static corruption (default)**: up to $t-1$ parties corrupted before
|
||||
protocol start. All other capabilities — broadcast view, p2p view into
|
||||
corrupted parties, full per-party state — included.
|
||||
- **Adaptive corruption (stronger)**: up to $t-1$ parties corruptible at
|
||||
any point during the protocol, conditioned on the transcript.
|
||||
Stretch goal for the first MPTC submission.
|
||||
- **Mobile corruption (proactive resharing)**: HJKY97 mobile adversary,
|
||||
up to $t-1$ parties per epoch with varying corruption set.
|
||||
|
||||
### Trusted parameters
|
||||
|
||||
- The cyclotomic ring $R_q = \mathbb{Z}_q[X] / (X^{256} + 1)$ and
|
||||
parameters $(q, k, \ell, \eta, \beta, \omega, \dots)$ exactly as in
|
||||
FIPS 204 ML-DSA-65.
|
||||
- The hash family: SHAKE-256 (FIPS 202), cSHAKE-256 / KMAC-256 /
|
||||
TupleHash-256 (NIST SP 800-185).
|
||||
- Gaussian sampler parameters from FIPS 204 §3.3 / §4.2.
|
||||
|
||||
No trusted setup beyond NIST primitives.
|
||||
|
||||
### Out-of-scope adversary capabilities
|
||||
|
||||
- Compromise of the cryptographic hash function (SHAKE-256 / cSHAKE-256
|
||||
/ KMAC-256). NIST FIPS 202 + SP 800-185 are taken as building blocks.
|
||||
- Side-channel attacks on the physical hardware running a party (power
|
||||
analysis, EM, fault injection). Handled at the deployed-binary layer;
|
||||
the algorithm-correctness chain is independent.
|
||||
- Compromise of the BIP-32/BIP-39 mnemonic from which device-specific
|
||||
keys are derived.
|
||||
|
||||
## Failure modes addressed
|
||||
|
||||
Pulsar's design closes specific failure modes that broke earlier
|
||||
threshold-lattice schemes:
|
||||
|
||||
- **Rejection-sampling restart leaking secret information across rounds**
|
||||
— per-round PRNG-key domain separation (CRIT-1 fix from upstream's
|
||||
2026-05-03 amendment, ported forward).
|
||||
- **Constant-time share comparison** — `dkg2.constTimePolyEqual` pattern
|
||||
ported from upstream (`reshare/commit.go` F9 fix).
|
||||
- **Information leaks via logging** — zero stdlib `log` use in any
|
||||
secret-touching path; all logging via `luxfi/log` at fields that are
|
||||
explicitly public. Enforced by `scripts/checks/test/no-secret-logs.sh`.
|
||||
- **Deterministic quorum selection in resharing leaking adversary
|
||||
positioning** — beacon-derived per-reshare quorum selection (HIP-0077
|
||||
§"reshare quorum" F10 fix).
|
||||
- **Cross-mode hash-suite confusion** — NIST profile is exclusively
|
||||
SHA-3 family; no BLAKE3 in Pulsar ever.
|
||||
|
||||
## See also
|
||||
|
||||
- [Postmortem](/docs/postmortem) — closed-finding registry; v1.0.20
|
||||
ExpandA-convention fix.
|
||||
- [BLOCKERS.md on GitHub](https://github.com/luxfi/pulsar/blob/main/BLOCKERS.md)
|
||||
— load-bearing entries on protocol drift, byte-equal output caveats,
|
||||
EUF-CMA scope.
|
||||
@@ -0,0 +1,12 @@
|
||||
// @ts-nocheck
|
||||
import { browser } from '@hanzo/docs-mdx/runtime/browser';
|
||||
import type * as Config from '../source.config';
|
||||
|
||||
const create = browser<typeof Config, import("@hanzo/docs-mdx/runtime/types").InternalTypeConfig & {
|
||||
DocData: {
|
||||
}
|
||||
}>();
|
||||
const browserCollections = {
|
||||
docs: create.doc("docs", {"changelog.mdx": () => import("../content/docs/changelog.mdx?collection=docs"), "getting-started.mdx": () => import("../content/docs/getting-started.mdx?collection=docs"), "index.mdx": () => import("../content/docs/index.mdx?collection=docs"), "nist-mptc.mdx": () => import("../content/docs/nist-mptc.mdx?collection=docs"), "postmortem.mdx": () => import("../content/docs/postmortem.mdx?collection=docs"), "security.mdx": () => import("../content/docs/security.mdx?collection=docs"), "proofs/axiom-inventory.mdx": () => import("../content/docs/proofs/axiom-inventory.mdx?collection=docs"), "proofs/extraction.mdx": () => import("../content/docs/proofs/extraction.mdx?collection=docs"), "proofs/lean-bridge.mdx": () => import("../content/docs/proofs/lean-bridge.mdx?collection=docs"), "proofs/overview.mdx": () => import("../content/docs/proofs/overview.mdx?collection=docs"), "protocol/dkg.mdx": () => import("../content/docs/protocol/dkg.mdx?collection=docs"), "protocol/fips-204.mdx": () => import("../content/docs/protocol/fips-204.mdx?collection=docs"), "protocol/overview.mdx": () => import("../content/docs/protocol/overview.mdx?collection=docs"), "protocol/parameters.mdx": () => import("../content/docs/protocol/parameters.mdx?collection=docs"), "reference/api.mdx": () => import("../content/docs/reference/api.mdx?collection=docs"), "reference/interop.mdx": () => import("../content/docs/reference/interop.mdx?collection=docs"), "reference/kat.mdx": () => import("../content/docs/reference/kat.mdx?collection=docs"), }),
|
||||
};
|
||||
export default browserCollections;
|
||||
@@ -0,0 +1,8 @@
|
||||
// @ts-nocheck
|
||||
import { dynamic } from '@hanzo/docs-mdx/runtime/dynamic';
|
||||
import * as Config from '../source.config';
|
||||
|
||||
const create = await dynamic<typeof Config, import("@hanzo/docs-mdx/runtime/types").InternalTypeConfig & {
|
||||
DocData: {
|
||||
}
|
||||
}>(Config, {"configPath":"source.config.ts","environment":"next","outDir":"docs"}, {"doc":{"passthroughs":["extractedReferences"]}});
|
||||
@@ -0,0 +1,31 @@
|
||||
// @ts-nocheck
|
||||
import * as __fd_glob_20 from "../content/docs/reference/kat.mdx?collection=docs"
|
||||
import * as __fd_glob_19 from "../content/docs/reference/interop.mdx?collection=docs"
|
||||
import * as __fd_glob_18 from "../content/docs/reference/api.mdx?collection=docs"
|
||||
import * as __fd_glob_17 from "../content/docs/protocol/parameters.mdx?collection=docs"
|
||||
import * as __fd_glob_16 from "../content/docs/protocol/overview.mdx?collection=docs"
|
||||
import * as __fd_glob_15 from "../content/docs/protocol/fips-204.mdx?collection=docs"
|
||||
import * as __fd_glob_14 from "../content/docs/protocol/dkg.mdx?collection=docs"
|
||||
import * as __fd_glob_13 from "../content/docs/proofs/overview.mdx?collection=docs"
|
||||
import * as __fd_glob_12 from "../content/docs/proofs/lean-bridge.mdx?collection=docs"
|
||||
import * as __fd_glob_11 from "../content/docs/proofs/extraction.mdx?collection=docs"
|
||||
import * as __fd_glob_10 from "../content/docs/proofs/axiom-inventory.mdx?collection=docs"
|
||||
import * as __fd_glob_9 from "../content/docs/security.mdx?collection=docs"
|
||||
import * as __fd_glob_8 from "../content/docs/postmortem.mdx?collection=docs"
|
||||
import * as __fd_glob_7 from "../content/docs/nist-mptc.mdx?collection=docs"
|
||||
import * as __fd_glob_6 from "../content/docs/index.mdx?collection=docs"
|
||||
import * as __fd_glob_5 from "../content/docs/getting-started.mdx?collection=docs"
|
||||
import * as __fd_glob_4 from "../content/docs/changelog.mdx?collection=docs"
|
||||
import { default as __fd_glob_3 } from "../content/docs/protocol/meta.json?collection=docs"
|
||||
import { default as __fd_glob_2 } from "../content/docs/reference/meta.json?collection=docs"
|
||||
import { default as __fd_glob_1 } from "../content/docs/proofs/meta.json?collection=docs"
|
||||
import { default as __fd_glob_0 } from "../content/docs/meta.json?collection=docs"
|
||||
import { server } from '@hanzo/docs-mdx/runtime/server';
|
||||
import type * as Config from '../source.config';
|
||||
|
||||
const create = server<typeof Config, import("@hanzo/docs-mdx/runtime/types").InternalTypeConfig & {
|
||||
DocData: {
|
||||
}
|
||||
}>({"doc":{"passthroughs":["extractedReferences"]}});
|
||||
|
||||
export const docs = await create.docs("docs", "content/docs", {"meta.json": __fd_glob_0, "proofs/meta.json": __fd_glob_1, "reference/meta.json": __fd_glob_2, "protocol/meta.json": __fd_glob_3, }, {"changelog.mdx": __fd_glob_4, "getting-started.mdx": __fd_glob_5, "index.mdx": __fd_glob_6, "nist-mptc.mdx": __fd_glob_7, "postmortem.mdx": __fd_glob_8, "security.mdx": __fd_glob_9, "proofs/axiom-inventory.mdx": __fd_glob_10, "proofs/extraction.mdx": __fd_glob_11, "proofs/lean-bridge.mdx": __fd_glob_12, "proofs/overview.mdx": __fd_glob_13, "protocol/dkg.mdx": __fd_glob_14, "protocol/fips-204.mdx": __fd_glob_15, "protocol/overview.mdx": __fd_glob_16, "protocol/parameters.mdx": __fd_glob_17, "reference/api.mdx": __fd_glob_18, "reference/interop.mdx": __fd_glob_19, "reference/kat.mdx": __fd_glob_20, });
|
||||
@@ -0,0 +1,24 @@
|
||||
// source.config.ts
|
||||
import { applyMdxPreset, defineConfig, defineDocs, frontmatterSchema, metaSchema } from "@hanzo/docs-mdx/config";
|
||||
var docs = defineDocs({
|
||||
dir: "content/docs",
|
||||
docs: {
|
||||
schema: frontmatterSchema,
|
||||
async mdxOptions(environment) {
|
||||
const { default: remarkMath } = await import("remark-math");
|
||||
const { default: rehypeKatex } = await import("rehype-katex");
|
||||
return applyMdxPreset({
|
||||
remarkPlugins: (v) => [remarkMath, ...v],
|
||||
rehypePlugins: (v) => [rehypeKatex, ...v]
|
||||
})(environment);
|
||||
}
|
||||
},
|
||||
meta: {
|
||||
schema: metaSchema
|
||||
}
|
||||
});
|
||||
var source_config_default = defineConfig();
|
||||
export {
|
||||
source_config_default as default,
|
||||
docs
|
||||
};
|
||||
Binary file not shown.
|
After Width: | Height: | Size: 1.7 KiB |
@@ -0,0 +1,11 @@
|
||||
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 64 64" fill="none">
|
||||
<!-- Simplified lotus for favicon -->
|
||||
<!-- Center petal -->
|
||||
<path d="M32 8 C32 8 27 22 27 34 C27 39 29 44 32 48 C35 44 37 39 37 34 C37 22 32 8 32 8Z" fill="#9333EA"/>
|
||||
<!-- Left petal -->
|
||||
<path d="M32 48 C29 44 22 40 17 38 C12 36 7 37 4 40 C7 47 14 52 21 52 C27 52 31 50 32 48Z" fill="#A855F7" opacity="0.9"/>
|
||||
<!-- Right petal -->
|
||||
<path d="M32 48 C35 44 42 40 47 38 C52 36 57 37 60 40 C57 47 50 52 43 52 C37 52 33 50 32 48Z" fill="#A855F7" opacity="0.9"/>
|
||||
<!-- Base -->
|
||||
<path d="M10 55 C18 52 26 50 32 50 C38 50 46 52 54 55" stroke="#7C3AED" stroke-width="1.5" fill="none" stroke-linecap="round"/>
|
||||
</svg>
|
||||
|
After Width: | Height: | Size: 695 B |
@@ -0,0 +1,5 @@
|
||||
import { twMerge } from 'tailwind-merge';
|
||||
|
||||
export function cn(...inputs: (string | undefined | null | false)[]) {
|
||||
return twMerge(inputs.filter(Boolean).join(' '));
|
||||
}
|
||||
@@ -0,0 +1,24 @@
|
||||
import type { Metadata } from 'next';
|
||||
|
||||
export const baseUrl = new URL(
|
||||
process.env.NEXT_PUBLIC_SITE_URL ?? 'https://pulsar.lux.network',
|
||||
);
|
||||
|
||||
export function createMetadata(override: Metadata): Metadata {
|
||||
return {
|
||||
...override,
|
||||
openGraph: {
|
||||
title: override.title ?? undefined,
|
||||
description: override.description ?? undefined,
|
||||
url: baseUrl,
|
||||
siteName: 'Pulsar',
|
||||
type: 'website',
|
||||
...override.openGraph,
|
||||
},
|
||||
twitter: {
|
||||
card: 'summary_large_image',
|
||||
...override.twitter,
|
||||
},
|
||||
metadataBase: baseUrl,
|
||||
};
|
||||
}
|
||||
@@ -0,0 +1,23 @@
|
||||
import { docs } from '@/docs/server';
|
||||
import { type InferPageType, loader } from '@hanzo/docs-core/source';
|
||||
import { lucideIconsPlugin } from '@hanzo/docs-core/source/lucide-icons';
|
||||
|
||||
export const source = loader({
|
||||
baseUrl: '/docs',
|
||||
source: docs.toSource(),
|
||||
plugins: [lucideIconsPlugin()],
|
||||
});
|
||||
|
||||
|
||||
export function getPageImage(page: InferPageType<typeof source>) {
|
||||
const segments = [...page.slugs, 'image.png'];
|
||||
return {
|
||||
segments,
|
||||
url: `/og/docs/${segments.join('/')}`,
|
||||
};
|
||||
}
|
||||
|
||||
export async function getLLMText(page: InferPageType<typeof source>) {
|
||||
const processed = await page.data.getText('processed');
|
||||
return `# ${page.data.title}\n\n${processed}`;
|
||||
}
|
||||
@@ -0,0 +1,15 @@
|
||||
import type { MDXComponents } from 'mdx/types';
|
||||
import defaultComponents from '@hanzo/docs-ui/mdx';
|
||||
|
||||
export function useMDXComponents(components: MDXComponents): MDXComponents {
|
||||
return {
|
||||
...defaultComponents,
|
||||
...components,
|
||||
};
|
||||
}
|
||||
|
||||
export function getMDXComponents(): MDXComponents {
|
||||
return {
|
||||
...defaultComponents,
|
||||
};
|
||||
}
|
||||
@@ -0,0 +1,14 @@
|
||||
import { createMDX } from '@hanzo/docs-mdx/next';
|
||||
|
||||
const withMDX = createMDX();
|
||||
|
||||
/** @type {import('next').NextConfig} */
|
||||
const config = {
|
||||
output: 'export',
|
||||
reactStrictMode: true,
|
||||
images: {
|
||||
unoptimized: true,
|
||||
},
|
||||
};
|
||||
|
||||
export default withMDX(config);
|
||||
@@ -0,0 +1,36 @@
|
||||
{
|
||||
"name": "pulsar-docs",
|
||||
"version": "0.1.0",
|
||||
"private": true,
|
||||
"scripts": {
|
||||
"build": "next build",
|
||||
"dev": "next dev --port 3008",
|
||||
"start": "next start",
|
||||
"types:check": "@hanzo/docs-mdx && next typegen && tsc --noEmit"
|
||||
},
|
||||
"dependencies": {
|
||||
"@hanzo/docs-core": "workspace:*",
|
||||
"@hanzo/docs-mdx": "workspace:*",
|
||||
"@hanzo/docs-ui": "workspace:*",
|
||||
"@hanzo/docs-base-ui": "workspace:*",
|
||||
"katex": "^0.16.11",
|
||||
"lucide-react": "^0.562.0",
|
||||
"next": "16.1.6",
|
||||
"react": "^19.2.3",
|
||||
"react-dom": "^19.2.3",
|
||||
"rehype-katex": "^7.0.1",
|
||||
"remark-math": "^6.0.0",
|
||||
"tailwind-merge": "^3.4.0",
|
||||
"zod": "^4.3.6"
|
||||
},
|
||||
"devDependencies": {
|
||||
"@tailwindcss/postcss": "^4.1.18",
|
||||
"@types/mdx": "^2.0.13",
|
||||
"@types/node": "25.0.5",
|
||||
"@types/react": "^19.2.8",
|
||||
"@types/react-dom": "^19.2.3",
|
||||
"postcss": "^8.5.6",
|
||||
"tailwindcss": "^4.1.18",
|
||||
"typescript": "^5.9.3"
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,5 @@
|
||||
export default {
|
||||
plugins: {
|
||||
'@tailwindcss/postcss': {},
|
||||
},
|
||||
};
|
||||
@@ -0,0 +1,21 @@
|
||||
import { applyMdxPreset, defineConfig, defineDocs, frontmatterSchema, metaSchema } from '@hanzo/docs-mdx/config';
|
||||
|
||||
export const docs = defineDocs({
|
||||
dir: 'content/docs',
|
||||
docs: {
|
||||
schema: frontmatterSchema,
|
||||
async mdxOptions(environment) {
|
||||
const { default: remarkMath } = await import('remark-math');
|
||||
const { default: rehypeKatex } = await import('rehype-katex');
|
||||
return applyMdxPreset({
|
||||
remarkPlugins: (v) => [remarkMath, ...v],
|
||||
rehypePlugins: (v) => [rehypeKatex, ...v],
|
||||
})(environment);
|
||||
},
|
||||
},
|
||||
meta: {
|
||||
schema: metaSchema,
|
||||
},
|
||||
});
|
||||
|
||||
export default defineConfig();
|
||||
@@ -0,0 +1,41 @@
|
||||
{
|
||||
"compilerOptions": {
|
||||
"target": "ESNext",
|
||||
"lib": [
|
||||
"dom",
|
||||
"dom.iterable",
|
||||
"esnext"
|
||||
],
|
||||
"allowJs": true,
|
||||
"skipLibCheck": true,
|
||||
"strict": true,
|
||||
"noEmit": true,
|
||||
"esModuleInterop": true,
|
||||
"module": "esnext",
|
||||
"moduleResolution": "bundler",
|
||||
"resolveJsonModule": true,
|
||||
"isolatedModules": true,
|
||||
"jsx": "react-jsx",
|
||||
"incremental": true,
|
||||
"plugins": [
|
||||
{
|
||||
"name": "next"
|
||||
}
|
||||
],
|
||||
"paths": {
|
||||
"@/*": [
|
||||
"./*"
|
||||
]
|
||||
}
|
||||
},
|
||||
"include": [
|
||||
"next-env.d.ts",
|
||||
"**/*.ts",
|
||||
"**/*.tsx",
|
||||
".next/types/**/*.ts",
|
||||
".next/dev/types/**/*.ts"
|
||||
],
|
||||
"exclude": [
|
||||
"node_modules"
|
||||
]
|
||||
}
|
||||
Generated
+67
-100
@@ -1184,6 +1184,73 @@ importers:
|
||||
specifier: ^5.9.3
|
||||
version: 5.9.3
|
||||
|
||||
apps/pulsar-docs:
|
||||
dependencies:
|
||||
'@hanzo/docs-base-ui':
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/base-ui
|
||||
'@hanzo/docs-core':
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/core
|
||||
'@hanzo/docs-mdx':
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/mdx
|
||||
'@hanzo/docs-ui':
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/radix-ui
|
||||
katex:
|
||||
specifier: ^0.16.11
|
||||
version: 0.16.41
|
||||
lucide-react:
|
||||
specifier: ^0.562.0
|
||||
version: 0.562.0([email protected])
|
||||
next:
|
||||
specifier: 16.1.6
|
||||
version: 16.1.6(@babel/[email protected])(@opentelemetry/[email protected])([email protected]([email protected]))([email protected])
|
||||
react:
|
||||
specifier: ^19.2.3
|
||||
version: 19.2.4
|
||||
react-dom:
|
||||
specifier: ^19.2.3
|
||||
version: 19.2.4([email protected])
|
||||
rehype-katex:
|
||||
specifier: ^7.0.1
|
||||
version: 7.0.1
|
||||
remark-math:
|
||||
specifier: ^6.0.0
|
||||
version: 6.0.0
|
||||
tailwind-merge:
|
||||
specifier: ^3.4.0
|
||||
version: 3.5.0
|
||||
zod:
|
||||
specifier: ^4.3.6
|
||||
version: 4.3.6
|
||||
devDependencies:
|
||||
'@tailwindcss/postcss':
|
||||
specifier: ^4.1.18
|
||||
version: 4.2.2
|
||||
'@types/mdx':
|
||||
specifier: ^2.0.13
|
||||
version: 2.0.13
|
||||
'@types/node':
|
||||
specifier: 25.0.5
|
||||
version: 25.0.5
|
||||
'@types/react':
|
||||
specifier: ^19.2.8
|
||||
version: 19.2.14
|
||||
'@types/react-dom':
|
||||
specifier: ^19.2.3
|
||||
version: 19.2.3(@types/[email protected])
|
||||
postcss:
|
||||
specifier: ^8.5.6
|
||||
version: 8.5.8
|
||||
tailwindcss:
|
||||
specifier: ^4.1.18
|
||||
version: 4.2.2
|
||||
typescript:
|
||||
specifier: ^5.9.3
|
||||
version: 5.9.3
|
||||
|
||||
apps/tasks-docs:
|
||||
dependencies:
|
||||
'@hanzo/docs':
|
||||
@@ -1448,106 +1515,6 @@ importers:
|
||||
specifier: ^5.9.3
|
||||
version: 5.9.3
|
||||
|
||||
apps/zap-docs:
|
||||
dependencies:
|
||||
'@hanzo/docs':
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/hanzo-docs
|
||||
'@hanzo/docs-base-ui':
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/base-ui
|
||||
'@hanzo/docs-core':
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/core
|
||||
'@hanzo/docs-mdx':
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/mdx
|
||||
'@hanzo/mdx-runtime':
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/mdx-runtime
|
||||
'@radix-ui/react-tooltip':
|
||||
specifier: ^1.2.8
|
||||
version: 1.2.8(@types/[email protected](@types/[email protected]))(@types/[email protected])([email protected]([email protected]))([email protected])
|
||||
'@shikijs/rehype':
|
||||
specifier: ^3.21.0
|
||||
version: 3.23.0
|
||||
'@shikijs/transformers':
|
||||
specifier: ^3.21.0
|
||||
version: 3.23.0
|
||||
class-variance-authority:
|
||||
specifier: ^0.7.1
|
||||
version: 0.7.1
|
||||
lucide-react:
|
||||
specifier: ^0.562.0
|
||||
version: 0.562.0([email protected])
|
||||
next:
|
||||
specifier: 16.1.6
|
||||
version: 16.1.6(@babel/[email protected])(@opentelemetry/[email protected])([email protected]([email protected]))([email protected])
|
||||
next-themes:
|
||||
specifier: ^0.4.6
|
||||
version: 0.4.6([email protected]([email protected]))([email protected])
|
||||
react:
|
||||
specifier: ^19.2.3
|
||||
version: 19.2.4
|
||||
react-dom:
|
||||
specifier: ^19.2.3
|
||||
version: 19.2.4([email protected])
|
||||
shiki:
|
||||
specifier: ^3.21.0
|
||||
version: 3.23.0
|
||||
tailwind-merge:
|
||||
specifier: ^3.4.0
|
||||
version: 3.5.0
|
||||
zod:
|
||||
specifier: ^4.3.5
|
||||
version: 4.3.6
|
||||
devDependencies:
|
||||
'@hanzo/docs-cli':
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/cli
|
||||
'@next/bundle-analyzer':
|
||||
specifier: 16.1.1
|
||||
version: 16.1.1
|
||||
'@next/env':
|
||||
specifier: 16.1.1
|
||||
version: 16.1.1
|
||||
'@next/eslint-plugin-next':
|
||||
specifier: 16.1.1
|
||||
version: 16.1.1
|
||||
'@tailwindcss/postcss':
|
||||
specifier: ^4.1.18
|
||||
version: 4.2.2
|
||||
'@types/node':
|
||||
specifier: 25.0.5
|
||||
version: 25.0.5
|
||||
'@types/react':
|
||||
specifier: ^19.2.8
|
||||
version: 19.2.14
|
||||
'@types/react-dom':
|
||||
specifier: ^19.2.3
|
||||
version: 19.2.3(@types/[email protected])
|
||||
browserslist-config-baseline:
|
||||
specifier: ^0.5.0
|
||||
version: 0.5.0
|
||||
eslint-config-custom:
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/eslint-config-custom
|
||||
postcss:
|
||||
specifier: ^8.5.6
|
||||
version: 8.5.8
|
||||
tailwindcss:
|
||||
specifier: ^4.1.18
|
||||
version: 4.2.2
|
||||
tailwindcss-animate:
|
||||
specifier: ^1.0.7
|
||||
version: 1.0.7([email protected])
|
||||
tsconfig:
|
||||
specifier: workspace:*
|
||||
version: link:../../packages/tsconfig
|
||||
typescript:
|
||||
specifier: ^5.9.3
|
||||
version: 5.9.3
|
||||
|
||||
apps/zen-docs:
|
||||
dependencies:
|
||||
'@hanzo/docs-base-ui':
|
||||
|
||||
Reference in New Issue
Block a user