From 8cb19066624988f55a25dce17e0e12f0900b696f Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Fri, 17 Jul 2026 11:05:02 +0100 Subject: [PATCH 1/2] docs: build-check the trust boundary; fix trust-discipline wording MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add `assert_axioms`, a concise sibling of `assert_no_sorry` that pins a declaration's trusted base to a tier — standard axioms, or standard plus `native_decide` — by matching on the axiom kind rather than its toolchain-dependent name. Use it in a new `CompElliptic.TrustBoundary` census, imported by the library root so `lake build` enforces it. Correct the README: drop the stale `Lean.ofReduceBool` claim (current toolchains add a per-declaration `native_decide` axiom instead), and hedge that independent re-checking catches a bad oracle only if someone performs the check. Co-authored-by: Claude Opus 4.8 --- CompElliptic.lean | 1 + CompElliptic/Meta/AxiomCheck.lean | 49 +++++++++++++++++++++++++ CompElliptic/TrustBoundary.lean | 60 +++++++++++++++++++++++++++++++ README.md | 24 +++++++------ 4 files changed, 124 insertions(+), 10 deletions(-) create mode 100644 CompElliptic/Meta/AxiomCheck.lean create mode 100644 CompElliptic/TrustBoundary.lean diff --git a/CompElliptic.lean b/CompElliptic.lean index 24cd793..3100304 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -17,3 +17,4 @@ import CompElliptic.CurveForms.ShortWeierstrass import CompElliptic.CurveOrder import CompElliptic.Curves.Pasta import CompElliptic.Curves.PastaOrder +import CompElliptic.TrustBoundary diff --git a/CompElliptic/Meta/AxiomCheck.lean b/CompElliptic/Meta/AxiomCheck.lean new file mode 100644 index 0000000..64b9a03 --- /dev/null +++ b/CompElliptic/Meta/AxiomCheck.lean @@ -0,0 +1,49 @@ +/- +Copyright (c) 2026 CompElliptic Contributors. +Released under the Apache License, Version 2.0, or the MIT license, at your option, +as described in the files LICENSE-APACHE and LICENSE-MIT. +Authors: Daira-Emma Hopwood +-/ +import Lean.Util.CollectAxioms +import Lean.Elab.Command + +/-! +# `assert_axioms` — a concise, build-checked trust-boundary pin + +A sibling of Mathlib's `assert_no_sorry` (same `collectAxioms` machinery) that asserts an *upper +bound* on a declaration's trusted base. Unlike a `#guard_msgs`-pinned `#print axioms`, it does not +hard-code the pretty-printed axiom list, so it stays green across toolchain bumps that rename the +`native_decide` axiom — while still failing the build the moment a declaration reaches beyond its +declared tier (a `sorry`, an unexpected axiom, or `native_decide` where none was permitted). +-/ + +open Lean Elab Command + +namespace CompElliptic.Meta + +/-- The standard axioms of Lean's trusted base — the whole budget for a general theorem. -/ +def standardAxioms : Array Name := #[``propext, ``Classical.choice, ``Quot.sound] + +/-- An axiom introduced by `native_decide`: its name carries a `native_decide` component +(e.g. `…_native.native_decide.ax_1_1`). Matching on the component rather than the full name keeps +the check stable across the toolchain-dependent axiom naming. -/ +def isNativeDecideAxiom (n : Name) : Bool := + n.components.any (· == `native_decide) + +/-- +`assert_axioms foo` fails the build unless `foo` depends only on the standard axioms +(`propext`, `Classical.choice`, `Quot.sound`) — in particular, no `sorry` and no `native_decide`. + +`assert_axioms foo +native` additionally permits `native_decide` compiler-trust axioms, whose exact +names are toolchain-dependent. Any other axiom (including `sorryAx`) is still rejected. +-/ +elab "assert_axioms " n:ident native:("+native")? : command => do + let name ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo n + let axs ← collectAxioms name + let allowNative := native.isSome + let unexpected := axs.filter fun ax => + !standardAxioms.contains ax && !(allowNative && isNativeDecideAxiom ax) + unless unexpected.isEmpty do + throwError "{n} depends on unexpected axiom(s): {unexpected.toList}" + +end CompElliptic.Meta diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean new file mode 100644 index 0000000..bb55b25 --- /dev/null +++ b/CompElliptic/TrustBoundary.lean @@ -0,0 +1,60 @@ +/- +Copyright (c) 2026 CompElliptic Contributors. +Released under the Apache License, Version 2.0, or the MIT license, at your option, +as described in the files LICENSE-APACHE and LICENSE-MIT. +Authors: Daira-Emma Hopwood +-/ +import CompElliptic.Curves.PastaOrder +import CompElliptic.Fields.Sqrt +import CompElliptic.Meta.AxiomCheck + +/-! +# Trust boundary, build-checked + +The library-wide census that makes the *independently re-checkable trust* principle (see the +README) a build-time check rather than a prose claim. Each `assert_axioms` below pins an *upper +bound* on a declaration's trusted base, so a change that widens it — a `sorry`, a new axiom in a +general theorem, or `native_decide` creeping into a quantified result — fails this file rather than +passing silently. The declarations are grouped by trust tier: + +* **General theorems** rest only on `propext` / `Classical.choice` / `Quot.sound`. A quantified + result has no independent spot-check, so it must not reach beyond Lean's standard axioms. +* **Concrete closed facts checked by the kernel** (Pratt primality certificates) add nothing beyond + those same axioms: the kernel evaluates them directly, trusting only its GMP bignum arithmetic + (which even ordinary `decide` relies on and which axiom collection does not surface). +* **Concrete closed facts trusting the compiler** (`native_decide`, marked `+native`) each add a + per-declaration compiler-trust axiom. This is the whole compiler-trust surface, confined to + falsifiable numeric facts about the Pasta fields and curves — chiefly the order of the + Tonelli–Shanks roots of unity (`pallasBase`/`vestaBase`) and the two prime-order witnesses behind + the group orders. Each such fact is reproducible by an independent tool, so a miscompiled oracle + could in principle be caught by disagreement (the catch requires someone actually performing the + independent check). + +`assert_axioms` matches on the axiom *tier*, not the exact `native_decide` axiom name (which is +toolchain-dependent), so this census stays green across toolchain bumps while still catching any +tier violation. +-/ + +open CompElliptic.Meta + +/-! ## General theorems — standard axioms only -/ + +assert_axioms CompElliptic.CurveOrder.card_fibre_le_two +assert_axioms CompElliptic.CurveOrder.card_eq_of_prime_witness_of_card_lt_two_mul +assert_axioms CompElliptic.CurveOrder.card_eq_of_prime_witness_of_card_lt_three_mul +assert_axioms CompElliptic.Fields.TonelliShanks.sqrt?_mul_self +assert_axioms CompElliptic.Fields.TonelliShanks.sqrt?_isSome_of_isSquare + +/-! ## Concrete closed facts checked by the kernel (Pratt certificates) — standard axioms only -/ + +assert_axioms CompElliptic.Fields.Pasta.PALLAS_BASE_is_prime +assert_axioms CompElliptic.Fields.Pasta.PALLAS_SCALAR_is_prime + +/-! ## Concrete closed facts trusting the compiler (`native_decide`) -/ + +assert_axioms CompElliptic.Fields.Pasta.pallasBase +native +assert_axioms CompElliptic.Fields.Pasta.vestaBase +native +assert_axioms CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt +native +assert_axioms CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt +native +assert_axioms CompElliptic.Curves.Pasta.Pallas.card_eq +native +assert_axioms CompElliptic.Curves.Pasta.Vesta.card_eq +native diff --git a/README.md b/README.md index 52fe5e2..7ddb894 100644 --- a/README.md +++ b/README.md @@ -64,15 +64,15 @@ The available API should precisely reflect only what is intended to be modelled. The *independently re-checkable trust* principle rests on a few specifics. The trust extensions that arise in practice in Lean are `native_decide` —which discharges a goal by running compiled -native code and adds the `Lean.ofReduceBool` axiom— and, unavoidably for numbers of this size, the -kernel's own GMP-backed bignum arithmetic, on which even ordinary `decide` depends. +native code, adding a per-declaration compiler-trust axiom— and, unavoidably for numbers of this +size, the kernel's own GMP-backed bignum arithmetic, on which even ordinary `decide` depends. In CompElliptic, we allow these extensions to be used only for concrete, closed facts with no free variables: a Pratt primality certificate, a field's cardinality, the multiplicative order of a fixed root of unity, a (non-)residuosity check. These facts are easily reproducible: another computer-algebra system, proof assistant, bignum library, or hand computation would compute the -same result, so a miscompiled or buggy oracle is caught by disagreement rather than silently -believed. +same result, so a miscompiled or buggy oracle could in principle be caught by disagreement rather +than silently believed — the catch requires someone actually performing the independent check. A general, quantified theorem ranging over many objects (for example, the correctness of a square-root algorithm for all finite fields it supports) has no analogous independent spot-check, @@ -84,7 +84,11 @@ implementation: not GMP) from the trusted base; * state each computational fact in a form an independent tool could re-verify. -The *Status* section below records how this split appears in the actual axiom dependencies. +This split is not just documented but checked at build time: `CompElliptic/TrustBoundary.lean` is a +census of representative declarations, each pinned with `assert_axioms` (a sibling of +`assert_no_sorry`) to the tier it is allowed to sit in. A general theorem that reaches for +`native_decide`, or a concrete fact that acquires an unexpected axiom, fails that file. The *Status* +section below summarizes how the split appears in the actual axiom dependencies. ## Status @@ -110,11 +114,11 @@ Early work in progress. Present so far: Uses of `sorry` are kept minimal and limited to work-in-progress. The library's general theorems depend only on the standard `propext` / `Classical.choice` / `Quot.sound` axioms. Facts specific to -concrete fields and curves also depend on `Lean.ofReduceBool`, the axiom behind `native_decide`, -now confined (per the *Independently re-checkable trust* principle) to checks the kernel cannot -feasibly run, chiefly the order of the Tonelli–Shanks roots of unity. Further coordinate systems -(projective and Jacobian), curve forms, the represented-group bridge, and the circuit model are -tracked in [TODO.md](TODO.md). +concrete fields and curves additionally depend on `native_decide`'s per-declaration compiler-trust +axiom, confined (per the *Independently re-checkable trust* principle) to checks the kernel cannot +feasibly run, chiefly the order of the Tonelli–Shanks roots of unity. The tier of each is pinned in +`CompElliptic/TrustBoundary.lean`. Further coordinate systems (projective and Jacobian), curve +forms, the represented-group bridge, and the circuit model are tracked in [TODO.md](TODO.md). ## License From da0452bcd9f525e149a300c69900db2c990d0e17 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Fri, 17 Jul 2026 11:15:37 +0100 Subject: [PATCH 2/2] docs: drop the legally meaningless "All rights reserved." The phrase was required under the 1910 Buenos Aires convention but has no effect under Berne; every Buenos Aires signatory has been a Berne signatory since 2000. Remove it from all file headers, including the copyright line the field-file generators emit (so regeneration still reproduces the committed files). Co-authored-by: Claude Opus 4.8 --- CompElliptic.lean | 2 +- CompElliptic/Basic.lean | 2 +- CompElliptic/CoordinateSystem.lean | 2 +- CompElliptic/CurveForms/ShortWeierstrass.lean | 2 +- CompElliptic/CurveOrder.lean | 2 +- CompElliptic/Curves/Pasta.lean | 2 +- CompElliptic/Curves/PastaOrder.lean | 2 +- CompElliptic/Encoding.lean | 2 +- CompElliptic/Encodings/Common.lean | 2 +- CompElliptic/Encodings/Pasta.lean | 2 +- CompElliptic/Fields/Jubjub.lean | 2 +- CompElliptic/Fields/Pasta.lean | 2 +- CompElliptic/Fields/Residue.lean | 2 +- CompElliptic/Fields/Sqrt.lean | 2 +- CompElliptic/ScalarMul.lean | 2 +- scripts/gen_jubjub.py | 4 ++-- scripts/gen_pasta.py | 4 ++-- scripts/pratt.py | 2 +- 18 files changed, 20 insertions(+), 20 deletions(-) diff --git a/CompElliptic.lean b/CompElliptic.lean index 3100304..c668161 100644 --- a/CompElliptic.lean +++ b/CompElliptic.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/Basic.lean b/CompElliptic/Basic.lean index 69b1b55..b11a574 100644 --- a/CompElliptic/Basic.lean +++ b/CompElliptic/Basic.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/CoordinateSystem.lean b/CompElliptic/CoordinateSystem.lean index d9261bc..9de605e 100644 --- a/CompElliptic/CoordinateSystem.lean +++ b/CompElliptic/CoordinateSystem.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/CurveForms/ShortWeierstrass.lean b/CompElliptic/CurveForms/ShortWeierstrass.lean index f0c938c..d4cea87 100644 --- a/CompElliptic/CurveForms/ShortWeierstrass.lean +++ b/CompElliptic/CurveForms/ShortWeierstrass.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/CurveOrder.lean b/CompElliptic/CurveOrder.lean index 2afc445..e403105 100644 --- a/CompElliptic/CurveOrder.lean +++ b/CompElliptic/CurveOrder.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood, Gregor Mitscha-Baude diff --git a/CompElliptic/Curves/Pasta.lean b/CompElliptic/Curves/Pasta.lean index c4ee51a..d20b855 100644 --- a/CompElliptic/Curves/Pasta.lean +++ b/CompElliptic/Curves/Pasta.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/Curves/PastaOrder.lean b/CompElliptic/Curves/PastaOrder.lean index 85834de..9d08407 100644 --- a/CompElliptic/Curves/PastaOrder.lean +++ b/CompElliptic/Curves/PastaOrder.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood, Gregor Mitscha-Baude diff --git a/CompElliptic/Encoding.lean b/CompElliptic/Encoding.lean index 88b8fc6..e3dfaf3 100644 --- a/CompElliptic/Encoding.lean +++ b/CompElliptic/Encoding.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/Encodings/Common.lean b/CompElliptic/Encodings/Common.lean index 4f68b30..a3bc84c 100644 --- a/CompElliptic/Encodings/Common.lean +++ b/CompElliptic/Encodings/Common.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/Encodings/Pasta.lean b/CompElliptic/Encodings/Pasta.lean index 3ccfb56..b62fbec 100644 --- a/CompElliptic/Encodings/Pasta.lean +++ b/CompElliptic/Encodings/Pasta.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/Fields/Jubjub.lean b/CompElliptic/Fields/Jubjub.lean index c6dd939..6f9dcd8 100644 --- a/CompElliptic/Fields/Jubjub.lean +++ b/CompElliptic/Fields/Jubjub.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/Fields/Pasta.lean b/CompElliptic/Fields/Pasta.lean index dd7db07..d0ea181 100644 --- a/CompElliptic/Fields/Pasta.lean +++ b/CompElliptic/Fields/Pasta.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/Fields/Residue.lean b/CompElliptic/Fields/Residue.lean index 3cde54e..870d91e 100644 --- a/CompElliptic/Fields/Residue.lean +++ b/CompElliptic/Fields/Residue.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Gregor Mitscha-Baude diff --git a/CompElliptic/Fields/Sqrt.lean b/CompElliptic/Fields/Sqrt.lean index 0cc08cd..0351698 100644 --- a/CompElliptic/Fields/Sqrt.lean +++ b/CompElliptic/Fields/Sqrt.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/CompElliptic/ScalarMul.lean b/CompElliptic/ScalarMul.lean index 27c3795..e063b2e 100644 --- a/CompElliptic/ScalarMul.lean +++ b/CompElliptic/ScalarMul.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/scripts/gen_jubjub.py b/scripts/gen_jubjub.py index e2f37d4..be21966 100644 --- a/scripts/gen_jubjub.py +++ b/scripts/gen_jubjub.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -# Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +# Copyright (c) 2026 CompElliptic Contributors. # Released under the Apache License, Version 2.0, or the MIT license, at your option, # as described in the files LICENSE-APACHE and LICENSE-MIT. # Authors: Daira-Emma Hopwood @@ -26,7 +26,7 @@ HEADER = """\ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/scripts/gen_pasta.py b/scripts/gen_pasta.py index 263bbdf..1b7052f 100644 --- a/scripts/gen_pasta.py +++ b/scripts/gen_pasta.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -# Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +# Copyright (c) 2026 CompElliptic Contributors. # Released under the Apache License, Version 2.0, or the MIT license, at your option, # as described in the files LICENSE-APACHE and LICENSE-MIT. # Authors: Daira-Emma Hopwood @@ -22,7 +22,7 @@ HEADER = """\ /- -Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +Copyright (c) 2026 CompElliptic Contributors. Released under the Apache License, Version 2.0, or the MIT license, at your option, as described in the files LICENSE-APACHE and LICENSE-MIT. Authors: Daira-Emma Hopwood diff --git a/scripts/pratt.py b/scripts/pratt.py index 9c61f02..a3cba3a 100644 --- a/scripts/pratt.py +++ b/scripts/pratt.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -# Copyright (c) 2026 CompElliptic Contributors. All rights reserved. +# Copyright (c) 2026 CompElliptic Contributors. # Released under the Apache License, Version 2.0, or the MIT license, at your option, # as described in the files LICENSE-APACHE and LICENSE-MIT. # Authors: Daira-Emma Hopwood