daira · daira · Jul 17, 2026 · Jul 17, 2026 · Jul 17, 2026
diff --git 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
@@ -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/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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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/Meta/AxiomCheck.lean 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/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/CompElliptic/TrustBoundary.lean 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
@@ -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
 

diff --git 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
@@ -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
@@ -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