From d9e0ec468ab598fd1fd73c454423cf378ac49f54 Mon Sep 17 00:00:00 2001 From: Daira-Emma Hopwood Date: Mon, 10 Aug 2026 03:43:46 +0100 Subject: [PATCH] meta: port ironwood's extended AxiomCheck MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the minimal assert_axioms/assert_computable with ironwood's extended version. The `+native` flag now requires naming the owning declaration(s) of exactly the native_decide axioms the entry reaches, with provenance checks that reject an axiom merely named like a compiler auxiliary. Both commands also reject compiled-body overrides (`@[implemented_by]`, `@[extern]`) anywhere in the import closure, reject `partial` declarations inside a certificate's evaluated term, and require fully qualified entry names. The regression tests live in a new MetaCheck library outside CompElliptic/, so their forged axioms never enter the production import graph and the source-level sweep scripts do not scan them. TrustBoundary's `+native` entries now name their owners: each Tonelli–Shanks datum owns the two certificates of its primitivity check, and the curve-order entries reach exactly the nsmul witnesses. Co-authored-by: Claude Fable 5 --- CompElliptic/Meta/AxiomCheck.lean | 442 ++++++++++++++++++++++++++++-- CompElliptic/TrustBoundary.lean | 30 +- MetaCheck/AxiomCheck.lean | 223 +++++++++++++++ MetaCheck/CompiledOverride.lean | 116 ++++++++ MetaCheck/NativeSurface.lean | 112 ++++++++ lakefile.toml | 11 +- 6 files changed, 898 insertions(+), 36 deletions(-) create mode 100644 MetaCheck/AxiomCheck.lean create mode 100644 MetaCheck/CompiledOverride.lean create mode 100644 MetaCheck/NativeSurface.lean diff --git a/CompElliptic/Meta/AxiomCheck.lean b/CompElliptic/Meta/AxiomCheck.lean index 141a1e6..000c58e 100644 --- a/CompElliptic/Meta/AxiomCheck.lean +++ b/CompElliptic/Meta/AxiomCheck.lean @@ -2,10 +2,15 @@ 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 +Authors: Daira-Emma Hopwood, Tal Derei -/ import Lean.Util.CollectAxioms import Lean.Elab.Command +import Lean.DeclarationRange +import Lean.Compiler.ImplementedByAttr +import Lean.Compiler.ExternAttr +import Lean.Compiler.CSimpAttr +import Mathlib.Util.AssertNoSorry /-! # `assert_axioms` and `assert_computable` — concise, build-checked trust assertions @@ -15,8 +20,28 @@ bound* on a declaration's trusted base. Unlike a `#guard_msgs`-pinned `#print ax hard-code the pretty-printed axiom list, so they stay 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). + The `#guard_msgs`-pinned form remains the right tool when the *exact* axiom set is the claim. +Both commands also police the *compiled* side of the trusted base: an axiom footprint says nothing +about what compiled code runs, and the census's `+native` entries are `native_decide` proofs that +run it. Two sections below cover the two ways compiled behaviour comes apart from kernel meaning — +a substituted body (`@[implemented_by]`, `@[extern]`) and a `partial` declaration inside a +certificate's evaluated term. + +Scope: these commands catch *inadvertent* drift — an entry silently reaching more than it +claims. They are not a full defence against a deliberately deceptive author. The provenance +check (`rangeStartsInside`) does reject the cheapest deliberate attack, a macro that emits an +auxiliary-named `axiom` alongside the theorem using it; what it cannot reject is code that +manipulates declaration ranges outright (`Lean.addDeclarationRanges` under `run_cmd`), which has +no innocuous reading in a diff. Treat any declaration-emitting metaprogram entering this +repository as census-relevant on review. + +Both commands require their argument to be written fully qualified (`checkFullyQualified`): +an unqualified name resolves through the census file's `open`s, so a same-base-name cousin in +an opened namespace can silently capture an entry meant for a declaration that is not in scope +at all — the assertion then reads as covering one theorem while checking another. + These commands are also used in ironwood (`Zcash/Meta/AxiomCheck.lean`); changes here should be reflected there and vice versa. -/ @@ -28,60 +53,429 @@ 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. -/ +/-! ## Compiled-body overrides + +`@[implemented_by f]` and `@[extern "sym"]` instruct the compiler to run a *different body* than the +one the kernel reduces, and Lean checks no relation between the two (`@[csimp]` is the checked +counterpart: it demands a proof that the replacement equals the original). Neither attribute changes +the safety flag, the `noncomputable` flag, or the axiom footprint, so nothing the rest of this file +inspects can see the substitution: a censused `def` can carry `@[implemented_by doctored]` and +`assert_computable` will still call it genuinely computed data while the executed value is the +attacker's. That matters here because the census's `+native` entries are `native_decide` proofs, +which *run the compiled bodies* — a doctored body makes such a certificate report a fact that the +kernel value refutes. + +The check below is deliberately not cone-scoped. `collectAxioms` no longer walks imported bodies +(it reads a per-module precomputed footprint), so a transitive walk over a certificate's cone would +be the expensive traversal Lean stopped doing — and what it would mostly find is the *ambient* +surface: at the pinned toolchain, `Init`/`Std`/`Lean`/`Mathlib` carry on the order of a thousand of +these attributes between them, all of them compiled code every `native_decide` in existence already +runs. So the census splits the two rather than walking terms. On the ambient surface it claims +nothing new. Outside it, it enumerates *every* override in the import closure, reachable or not: +the attribute extensions are indexed by declaring module, so this is a scan of the module list +rather than of any term, and it catches an override before the commit that puts it in a cone. +Stating it over the whole closure is sound because `ParametricAttribute`'s `add` refuses a +declaration from an imported module (`Lean.Attributes`, `throwAttrDeclInImportedModule`) — a commit +can only attach either attribute inside the module that declares the constant, so every override a +commit here can introduce lives in a module this repository owns, and none of them can hide behind +an ambient root. -/ + +/-- Package roots whose compiled-body overrides are *ambient*: the Lean toolchain and the pinned +dependency stack (CompPoly and the mathlib stack it version-pins), whose compiled code every +`native_decide` runs no matter what this repository does, and which a commit here cannot add an +override to (attributes cannot be attached to an imported declaration). Everything else is +censused, so a *new* dependency fails the build until its root is classified — a new package in +the import closure is a trusted-base change, unlike a version bump of one already listed. This is +where the `@[extern]` `Task.spawn` / `Task.get` reached through +`CompElliptic.Curves.Pasta.Fast.Msm.parMap` land: the kernel sees their reference bodies, and +`parMap_eq_map` closes by `rfl`. -/ +def ambientPackageRoots : Array Name := + #[`Init, `Lean, `Std, `Lake, `Batteries, `Mathlib, `Aesop, `Qq, `Plausible, `ProofWidgets, + `ImportGraph, `LeanSearchClient, `Cli, `CompPoly] + +/-- The attribute substituting `decl`'s compiled body, if any. -/ +def compiledBodyOverride? (env : Environment) (decl : Name) : Option Name := + if (Lean.Compiler.getImplementedBy? env decl).isSome then some `implemented_by + else if Lean.isExtern env decl then some `extern + else none + +/-- Every declaration outside `ambientPackageRoots` that carries a compiled-body override, paired +with the attribute responsible. + +There is deliberately no allowlist to sit alongside `ambientPackageRoots`, because the two would not +be the same kind of thing. `ambientPackageRoots` is trust inherited from the toolchain and the +pinned dependency stack — no commit here can add to it, since an attribute cannot be attached to an +imported declaration — whereas an admitted override would be trust this repository chose to add, +which is exactly what the prohibition is about. A substitution in a declaration this repository owns +is therefore rejected outright rather than admitted with a disclosure, and +`CompElliptic.Curves.Pasta.Fast.Projective` records the convention that a kernel-checked equality +(`padd_eq_paddFast`, registrable as `@[csimp]`) is used instead. + +Imported declarations are read off the two attribute extensions' per-module entry arrays — the same +arrays `ParametricAttribute.getParam?`, and hence the compiler, reads, so an override the compiler +acts on cannot be invisible here. The entry arrays are fetched first and the module root classified +only for the few modules that have any, so the scan costs a pair of array lookups per imported +module. Declarations of the module currently being elaborated have no module index, so they are read +from stage 2 of the constant map — exactly the current module's constants — through +`compiledBodyOverride?`, which is that same compiler-facing query. -/ +def undisclosedCompiledBodyOverrides (env : Environment) : Array (Name × Name) := Id.run do + let mods := env.header.moduleNames + let mut found : Array (Name × Name) := #[] + for i in [0:mods.size] do + let idx : ModuleIdx := i + let impls := Lean.Compiler.implementedByAttr.ext.getModuleEntries env idx + let externs := Lean.externAttr.ext.getModuleEntries env idx + unless impls.isEmpty && externs.isEmpty do + unless ambientPackageRoots.contains mods[i]!.getRoot do + found := impls.foldl (fun acc (d, _) => acc.push (d, `implemented_by)) found + found := externs.foldl (fun acc (d, _) => acc.push (d, `extern)) found + found := env.constants.foldStage2 (fun acc d _ => + match compiledBodyOverride? env d with + | some attr => acc.push (d, attr) + | none => acc) found + -- Sorted: the current module's constants come out of a hash map, so the report — which is pinned + -- by `#guard_msgs` in the regression suite — would otherwise have no fixed order. The attribute + -- breaks ties, since a declaration can in principle carry both and sorting on the name alone + -- would leave those two rows unordered. + return found.qsort (fun a b => Name.lt a.1 b.1 || (a.1 == b.1 && Name.lt a.2 b.2)) + +/-- Render `(declaration, attribute)` pairs as the text of the offending attributes. -/ +def overridesText (overrides : Array (Name × Name)) : String := + ", ".intercalate (overrides.toList.map fun (d, attr) => s!"{d} (@[{attr}])") + +/-- The censused declaration must not have its own compiled body substituted. Checked even for an +ambient-root target, because here the substitution is not background compiler trust but the entry's +own subject: everything the census goes on to verify is about the kernel term, which for such a +declaration is not what runs. -/ +def checkNoCompiledBodyOverride (n : Ident) (name : Name) : CommandElabM Unit := do + if let some attr := compiledBodyOverride? (← getEnv) name then + throwError "{n} carries '@[{attr}]', so its compiled body is not the body the kernel reduces \ + and Lean checks no relation between the two. Nothing this census verifies about the kernel \ + term constrains what compiled code — a `native_decide` over it in particular — computes." + +/-- No declaration in the census's own scope may have its compiled body substituted. This is a +property of the whole import closure rather than of `n`, so it fails every entry in the file at +once; that is the intent — an override anywhere is undisclosed compiler trust that the census, as +the artifact's statement of its trusted base, must not certify around. -/ +def checkCompiledBodyDisclosure (n : Ident) : CommandElabM Unit := do + let overrides := undisclosedCompiledBodyOverrides (← getEnv) + unless overrides.isEmpty do + throwError "{n} cannot be censused: {overridesText overrides} \ + substitute(s) a compiled body Lean never checks against the kernel body, so the value the \ + compiler runs is unconstrained by anything proved about it. If you must, use `@[csimp]` \ + instead, but be aware that `@[csimp]` still substantially increases the trust surface." + +/-- The declaration an alleged `native_decide` axiom names as its owner. The compiler-generated +name has an `_native.native_decide` marker after the owning declaration; only the tail after that +marker is toolchain-dependent. Taking the last marker also handles an owner whose own name contains +those components. -/ +def nativeAxiomOwner? (ax : Name) : Option Name := + let rec go (prefixRev rest : List Name) (ownerRev? : Option (List Name)) : Option Name := + match rest with + | a :: b :: tail => + let ownerRev? := if a == `_native && b == `native_decide then some prefixRev else ownerRev? + go (a :: prefixRev) (b :: tail) ownerRev? + | _ => ownerRev?.map fun ownerRev => + ownerRev.reverse.foldl Name.append Name.anonymous + go [] ax.components none + +/-- A syntactically plausible `native_decide` auxiliary axiom. `checkNativeAllowance` additionally +checks its owner, dependency, module, and source range before permitting it. -/ def isNativeDecideAxiom (n : Name) : Bool := - n.components.any (· == `native_decide) + (nativeAxiomOwner? n).isSome + +/-- Assertion names must be written fully qualified. Resolution through `open`s is +context-dependent: a same-base-name cousin in an opened namespace can silently capture an +entry meant for a declaration that is not even in scope, so the assertion reads as covering +one theorem while checking another. Requiring the written name to equal the resolved +constant's full name (an optional `_root_.` prefix is accepted) makes every entry +independent of the file's `open`s and turns the wrong-cousin case into a loud error. -/ +def checkFullyQualified (n : Syntax) (resolved : Name) : CommandElabM Unit := do + let written := n.getId + unless written == resolved || written == rootNamespace ++ resolved do + throwError "{n} is not written fully qualified: it resolves to '{resolved}'. \ + Write the full name so the entry does not depend on this file's `open`s." + +/-- Render a list of owners as the text to write inside `+native(...)`. -/ +def ownersText (owners : List Name) : String := + ", ".intercalate (owners.map toString) + +/-- Lexicographic source-position comparison. -/ +def positionLE (a b : Position) : Bool := + decide (a.line < b.line ∨ (a.line = b.line ∧ a.column ≤ b.column)) + +/-- Strict lexicographic source-position comparison. -/ +def positionLT (a b : Position) : Bool := + decide (a.line < b.line ∨ (a.line = b.line ∧ a.column < b.column)) + +/-- Whether `inner` *starts* strictly inside `outer`. Only the start position is compared against +the owner's end: Lean records an auxiliary's end position at the start of the next token, so it +runs past the end of the declaration that emitted it whenever the emitting syntax is followed by +whitespace or a comment — the shape a `native_decide` auto-param discharged inside a structure +instance always has. The start is still a faithful witness of where the auxiliary was elaborated, +and that is all the check needs: a hand-written `axiom` is a top-level command of its own, and one +the owner depends on must be declared before the owner, so its start never lands inside the owner's +range. + +The leading comparison is **strict**, and the strictness is load-bearing. A declaration produced by +macro expansion inherits the macro *invocation site* as its declaration range, so a macro emitting +both an `axiom` named like an auxiliary and a theorem using it gives the two identical ranges — +which satisfies a non-strict test automatically, laundering an arbitrary axiom (up to `False`) past +the census as a compiler-trust certificate. `MetaCheck.AxiomCheck.MacroForged` pins the rejection. +A genuine auxiliary is always emitted by elaborating syntax *within* the owner's declaration — a +tactic in its proof body, or an auto-param inside a structure instance — so in both shapes its +start is strictly after the owner's first token. -/ +def rangeStartsInside (outer inner : DeclarationRange) : Bool := + positionLT outer.pos inner.pos && positionLE inner.pos outer.endPos + +/-- The `native_decide` axioms genuinely owned by `owner`: each must occur in the owner's own +transitive axiom footprint, have the compiler-generated owner prefix, come from the same module, +and start inside the owner's declaration. The range condition distinguishes an auxiliary emitted +while elaborating the owner from an arbitrary axiom merely given the same name. -/ +def nativeAxiomsOwnedBy (owner : Name) : CommandElabM (Array Name) := do + let env ← getEnv + let ownerAxioms ← collectAxioms owner + let alleged := ownerAxioms.filter fun ax => nativeAxiomOwner? ax == some owner + let mut owned := #[] + for ax in alleged do + let sameModule := env.getModuleIdxFor? owner == env.getModuleIdxFor? ax + let ownerRanges? ← findDeclarationRanges? owner + let axRanges? ← findDeclarationRanges? ax + let rangeValid := match ownerRanges?, axRanges? with + | some ownerRanges, some axRanges => rangeStartsInside ownerRanges.range axRanges.range + | _, _ => false + unless sameModule && rangeValid do + throwError "'{ax}' looks like a native_decide axiom owned by '{owner}', but it was not \ + emitted inside that declaration" + owned := owned.push ax + return owned + +/-- `+native` must name the owning declaration(s) of exactly the `native_decide` axioms the +entry actually reaches, fully qualified. A bare `+native` would permit a `native_decide` +axiom brought in by *any* declaration entering the dependency cone; naming the owners makes +the census state precisely which native certificates are trusted, and a new native axiom — +or a stale annotation — fails the build with the list to write. -/ +def checkNativeAllowance (n : Ident) (axs : Array Name) (allowed : Option (Array Name)) : + CommandElabM Unit := do + let nativeAxioms := axs.filter isNativeDecideAxiom + let owners := (nativeAxioms.filterMap nativeAxiomOwner?).toList.eraseDups + match allowed with + | none => + unless owners.isEmpty do + throwError "{n} depends on native_decide axiom(s); name their owning declaration(s): \ + write '+native({ownersText owners})'" + | some allowedArr => + let allowedL := allowedArr.toList.eraseDups + if owners.isEmpty then + throwError "{n} reaches no native_decide axiom; drop the '+native(...)' flag" + let mut permitted := #[] + for owner in allowedL do + let owned ← nativeAxiomsOwnedBy owner + if owned.isEmpty then + throwError "{n}: '+native' names '{owner}', but that declaration owns no \ + native_decide axiom" + permitted := permitted.append owned + let presentL := nativeAxioms.toList.eraseDups + let permittedL := permitted.toList.eraseDups + unless presentL.all permittedL.contains && permittedL.all presentL.contains do + throwError "{n}: '+native' names {allowedL} but the native_decide axiom(s) present \ + are owned by {owners}; write '+native({ownersText owners})'" + +/-! ## `partial` inside a native certificate + +The other shape of compiled-versus-kernel divergence, and the one the attribute sweep above cannot +see. `partial def f` elaborates to an `opaque` constant plus an `unsafe` `f._unsafe_rec` that the +compiler substitutes for it: the kernel gets a constant it will not unfold and no equation relating +it to anything, while the compiled body is unsafe code with the termination check lifted — the +`unsafe def r : Break := r` shape `assert_computable`'s safety check rejects, re-entering through a +declaration that is neither `unsafe` nor a `def`. A `native_decide` over such a constant is an +assertion about something the kernel could not have evaluated even in principle. + +`assert_computable` rejects a `partial` target already (it is not a `def`), but the entry that +launders one is the `assert_axioms` on the certificate *consuming* it, whose own declaration is +clean. So this is checked where it bites: inside what a `native_decide` certificate actually +evaluated. That surface is exact and cheap, because a `native_decide` auxiliary axiom is +`@Eq Bool e Bool.true` with `e` the closed term the compiler ran (`Lean.Meta.nativeEqTrue`) — +walking `e` walks the data, not the proof. + +`e` is the term as the *kernel* records it, though, and the compiler does not run it verbatim: a +`@[csimp]` lemma replaces a constant wholesale in compiled code, so a certificate whose statement +says `padd` would run `paddFast` under such a registration. The walk therefore follows those +replacements. Without that step a `partial` reachable only through a replacement target would be +invisible here; this repository registers no `@[csimp]` today, but keeps the proven equality +(`CompElliptic.Curves.Pasta.Fast.Projective.PVes.padd_eq_paddFast`) for a future registration, +which the walk's following of the map already covers. That step is owed entirely to `@[csimp]` +being permitted: prohibiting it retires the replacement map, and the walk collapses back to +following the term the axiom states. + +Plain `opaque` is deliberately not reported. Its compiled body *is* its declared body, so it cannot +make a certificate disagree with the source; and the sealed-subtype idiom +(`opaque h : {x // x = source} := ⟨source, rfl⟩`, whose acceptance `MetaCheck.NativeSurface` pins) +keeps the value kernel-recoverable through the type. An `opaque` that *is* body-substituted carries +`@[implemented_by]` and is caught by the sweep above. -/ + +/-- Whether `decl` is the `opaque` constant a `partial def` leaves behind, recognized by the +`_unsafe_rec` implementation the compiler substitutes for it (`Lean.Compiler.mkUnsafeRecName`). -/ +def isPartialDecl (env : Environment) (decl : Name) : Bool := + env.find? decl matches some (.opaqueInfo _) && + env.contains (Lean.Compiler.mkUnsafeRecName decl) + +/-- `partial` declarations outside `ambientPackageRoots` that a `native_decide` certificate +evaluated. Walks the auxiliary axioms' types, which are the terms that ran, following the +`@[csimp]` replacements the compiler applies to them. -/ +def nativeEvaluatedPartials (env : Environment) (nativeAxioms : Array Name) : Array Name := Id.run do + let mods := env.header.moduleNames + let csimp := (Lean.Compiler.CSimp.ext.getState env).map + let mut seen : Std.HashSet Name := {} + let mut found : Array Name := #[] + let mut todo := nativeAxioms + while todo.size > 0 do + let c := todo.back! + todo := todo.pop + unless seen.contains c do + seen := seen.insert c + if let some info := env.find? c then + let ambient := match env.getModuleIdxFor? c with + | some idx => ambientPackageRoots.contains mods[idx.toNat]!.getRoot + | none => false + if !ambient && isPartialDecl env c then + found := found.push c + -- An axiom contributes only its type: for a native auxiliary that type *is* the evaluated + -- term. A theorem contributes only its type too — its proof is erased before compilation, + -- so a `partial` reachable only through one is never run. Everything else contributes its + -- value, which is what evaluation unfolds into. + todo := todo ++ info.type.getUsedConstants + unless info matches .axiomInfo _ | .thmInfo _ do + todo := todo ++ (info.value?.map Expr.getUsedConstants).getD #[] + -- An inductive's constructors, as `Lean.CollectAxioms.collect` does: they carry no value, + -- but reaching them keeps the traversal's notion of "mentioned" the same as the census's. + if let .inductInfo v := info then + todo := todo ++ v.ctors.toArray + -- `@[csimp]` replaces `c` with `e.toDeclName` in compiled code, so where the kernel term + -- says `c` the compiler runs the replacement's body. Following it is what makes this a + -- walk of what actually ran rather than of what the axiom's statement mentions. + if let some e := csimp.find? c then + todo := todo.push e.toDeclName + return found.qsort Name.lt + +/-- A `native_decide` certificate must not have evaluated a `partial` declaration: the auxiliary +axiom asserts that the compiler's evaluation is the kernel's, and here the kernel has no body to +have evaluated — the certificate becomes a statement about an abstract constant backed by an +unsafe implementation. -/ +def checkNativeEvaluatedSurface (n : Ident) (axs : Array Name) : CommandElabM Unit := do + let nativeAxioms := axs.filter isNativeDecideAxiom + if nativeAxioms.isEmpty then return + let partials := nativeEvaluatedPartials (← getEnv) nativeAxioms + unless partials.isEmpty do + throwError "{n}: the native_decide certificate evaluated the `partial` declaration(s) \ + {partials.toList}, whose compiled body is an unsafe implementation the kernel never sees and \ + whose kernel constant has no body at all. Nothing relates what ran to what the certificate \ + says. Give the evaluated data an ordinary `def`." + +/-- The `+native(A, B)` flag: the parenthesized, comma-separated owner list is required. -/ +syntax nativeFlag := "+native" "(" ident,+ ")" + +/-- Extract the identifiers from an optional `+native(A, B)` flag. -/ +def nativeAnnotation (native : Option (TSyntax ``nativeFlag)) : Option (Array Ident) := + native.map fun stx => stx.raw[2].getSepArgs.map fun arg => ⟨arg⟩ + +/-- Resolve and fully qualify every owner named by `+native`. Besides preventing namespace +capture, resolution rejects an annotation that names a nonexistent owner whose text happens +to prefix an arbitrary axiom. -/ +def resolveNativeAnnotation (native : Option (TSyntax ``nativeFlag)) : + CommandElabM (Option (Array Name)) := do + let some ids := nativeAnnotation native | return none + let names ← ids.mapM fun id => do + let name ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id + checkFullyQualified id name + return name + return some names /-- `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. +`assert_axioms foo +native(D₁, ...)` additionally permits `native_decide` compiler-trust axioms — +exactly those owned by the named declarations, written fully qualified. The axiom names' tails are +toolchain-dependent, so entries name the owning declarations rather than the axioms themselves. +Any other axiom (including `sorryAx`) is still rejected, as is a stale or incomplete list. + +Independently of the axiom budget, the entry fails if `foo` or any censused-scope declaration +carries a compiled-body override (`checkCompiledBodyDisclosure`), or if a permitted certificate +evaluated a `partial` declaration (`checkNativeEvaluatedSurface`); `MetaCheck.NativeSurface` +pins the latter. -/ -elab "assert_axioms " n:ident native:("+native")? : command => do +elab "assert_axioms " n:ident native:(nativeFlag)? : command => do let name ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo n + checkFullyQualified n name + checkNoCompiledBodyOverride n name let axs ← collectAxioms name - let allowNative := native.isSome + let allowed ← resolveNativeAnnotation native + checkNativeAllowance n axs allowed + checkNativeEvaluatedSurface n axs let unexpected := axs.filter fun ax => - !standardAxioms.contains ax && !(allowNative && isNativeDecideAxiom ax) + !standardAxioms.contains ax && !(allowed.isSome && isNativeDecideAxiom ax) unless unexpected.isEmpty do throwError "{n} depends on unexpected axiom(s): {unexpected.toList}" + checkCompiledBodyDisclosure n /-- -`assert_computable foo` fails the build unless `foo` is a plain `def` — an actual -definition, not marked `noncomputable` — depending on no axioms beyond `propext` / `Quot.sound`. -This is the breaks-as-computed-data check: the data is genuinely computed, and with -`Classical.choice` excluded it cannot have been conjured from mere propositional existence even -in erased positions. +`assert_computable foo` fails the build unless `foo` is a plain `def` — an actual definition, +marked neither `unsafe`/`partial` nor `noncomputable` — depending on no axioms beyond +`propext` / `Quot.sound`. This is the breaks-as-computed-data check: the data is genuinely +computed, and with `Classical.choice` excluded it cannot have been conjured from mere +propositional existence even in erased positions. `assert_computable foo +choice` additionally permits `Classical.choice`. Together with the plain-`def` check this asserts choice enters only through erased `Prop` fields: had it touched the -data, the definition could not have compiled as a plain `def`. `+native` likewise permits -`native_decide` compiler-trust axioms. +data, the definition could not have compiled as a plain `def`. `+native(D₁, ...)` likewise permits +the named declarations' `native_decide` compiler-trust axioms. + +Declaring `+choice` when `foo` does not actually reach `Classical.choice` fails the build (drop the +flag), as an over-broad `+native` does: the census states exactly the trust assumed, nothing more. The plain-`def` check guards a gap in "computability is compiler-enforced": marking a reduction `noncomputable` later would still build, silently voiding the convention; this assertion catches -it. +it. The definition-safety check closes the same gap from the other side. An `unsafe` def is a +`.defnInfo` like any other and is not `noncomputable`, so neither the kind check nor +`isNoncomputable` sees it — yet `unsafe` lifts the termination check, so such a definition can +inhabit its result type by bare self-reference (`unsafe def r : Break := r`) while computing +nothing. The kernel does refuse to let a safe declaration depend on an unsafe one, which confines +the forgery to a reduction no safe proof consumes; that is exactly the shape of a deliverable +endpoint reduction, which is why the assertion checks safety itself rather than leaning on the +kernel. `MetaCheck.AxiomCheck.ComputableSafety` pins the rejection. + +"Genuinely computed" is a claim about the *compiled* body, which none of the checks above can see, +so the assertion additionally rejects a definition whose compiled body is substituted and any +censused-scope declaration that substitutes one (`checkNoCompiledBodyOverride`, +`checkCompiledBodyDisclosure`); `MetaCheck.CompiledOverride` pins both rejections. -/ -elab "assert_computable " n:ident choice:("+choice")? native:("+native")? : command => do +elab "assert_computable " n:ident choice:("+choice")? native:(nativeFlag)? : command => do let name ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo n + checkFullyQualified n name let env ← getEnv - let info ← liftCoreM <| getConstInfo name - unless info matches .defnInfo _ do - throwError "{n} is not a def" + let .defnInfo val ← liftCoreM <| getConstInfo name + | throwError "{n} is not a def" + match val.safety with + | .safe => pure () + | .unsafe => throwError "{n} is marked unsafe" + | .partial => throwError "{n} is marked partial" if Lean.isNoncomputable env name then throwError "{n} is marked noncomputable" + checkNoCompiledBodyOverride n name let axs ← collectAxioms name let allowChoice := choice.isSome - let allowNative := native.isSome + if allowChoice && !axs.contains ``Classical.choice then + throwError "{n} does not depend on Classical.choice; drop the '+choice' flag" + let allowed ← resolveNativeAnnotation native + checkNativeAllowance n axs allowed + checkNativeEvaluatedSurface n axs let unexpected := axs.filter fun ax => !(ax == ``propext || ax == ``Quot.sound || (allowChoice && ax == ``Classical.choice) - || (allowNative && isNativeDecideAxiom ax)) + || (allowed.isSome && isNativeDecideAxiom ax)) unless unexpected.isEmpty do throwError "{n} depends on unexpected axiom(s): {unexpected.toList}" + checkCompiledBodyDisclosure n end CompElliptic.Meta diff --git a/CompElliptic/TrustBoundary.lean b/CompElliptic/TrustBoundary.lean index cc1c508..a8bea1d 100644 --- a/CompElliptic/TrustBoundary.lean +++ b/CompElliptic/TrustBoundary.lean @@ -25,17 +25,19 @@ passing silently. The declarations are grouped by trust tier: * **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 +* **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. +`assert_axioms` matches a permitted `native_decide` axiom by its owning declaration — named inside +`+native(...)` — rather than by the exact axiom name (whose tail is toolchain-dependent). The +census therefore stays green across toolchain bumps while still catching any tier violation, and +it states exactly which native certificates each entry trusts: a new certificate entering a cone, +or a stale owner list, fails the build with the list to write. -/ open CompElliptic.Meta @@ -65,12 +67,18 @@ assert_computable CompElliptic.Curves.Pasta.Vesta.fintypePoints +choice /-! ## 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 +assert_axioms CompElliptic.Fields.Pasta.pallasBase +native( + CompElliptic.Fields.Pasta.pallasBase) +assert_axioms CompElliptic.Fields.Pasta.vestaBase +native( + CompElliptic.Fields.Pasta.vestaBase) +assert_axioms CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt +native( + CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt) +assert_axioms CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt +native( + CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt) +assert_axioms CompElliptic.Curves.Pasta.Pallas.card_eq +native( + CompElliptic.Curves.Pasta.Pallas.q_nsmul_Gpt) +assert_axioms CompElliptic.Curves.Pasta.Vesta.card_eq +native( + CompElliptic.Curves.Pasta.Vesta.p_nsmul_Gpt) /-! ## Fast Vesta arithmetic — proven against the affine group law, standard axioms only diff --git a/MetaCheck/AxiomCheck.lean b/MetaCheck/AxiomCheck.lean new file mode 100644 index 0000000..8cb0ad5 --- /dev/null +++ b/MetaCheck/AxiomCheck.lean @@ -0,0 +1,223 @@ +/- +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, Tal Derei +-/ +import CompElliptic.Meta.AxiomCheck + +/-! +# Regression tests for `CompElliptic.Meta.AxiomCheck` + +Two rejection families. The native-axiom provenance cases deliberately impersonate Lean's +`native_decide` auxiliaries: most declare an axiom named like an auxiliary, and one instead names a +*theorem* so that its own genuine auxiliary imitates the marker path. The `assert_computable` cases +pin the declaration checks that stand behind "the reduction data is genuinely computed". Both live +in this test-only library so the production `CompElliptic` library never imports them. +-/ + +namespace MetaCheck.AxiomCheck + +namespace Genuine + +theorem owner : (123456 : Nat) < 123457 := by native_decide + +assert_axioms MetaCheck.AxiomCheck.Genuine.owner +native( + MetaCheck.AxiomCheck.Genuine.owner) + +end Genuine + +namespace GenuineAutoParam + +/-- The certificate lives in an auto-param, so the axiom is emitted while elaborating the +structure instance below rather than a tactic block of its own. Lean then records the auxiliary's +end position at the start of the *next* token — past the end of the owning declaration — which is +why ownership is decided by the auxiliary's start position. The Tonelli–Shanks data of this +repository (`CompElliptic.Fields.Pasta.pallasBase`, `vestaBase`) is the census entry with this +shape. -/ +structure Certified where + value : Nat + small : value < 123457 := by native_decide + +def owner : Certified where + value := 123456 + +assert_axioms MetaCheck.AxiomCheck.GenuineAutoParam.owner +native( + MetaCheck.AxiomCheck.GenuineAutoParam.owner) + +end GenuineAutoParam + +namespace NonexistentOwner + +axiom owner._native.native_decide.ax_1_1 : False +theorem target : False := owner._native.native_decide.ax_1_1 + +/-- error: Unknown constant `MetaCheck.AxiomCheck.NonexistentOwner.owner` -/ +#guard_msgs (whitespace := lax) in +assert_axioms MetaCheck.AxiomCheck.NonexistentOwner.target +native( + MetaCheck.AxiomCheck.NonexistentOwner.owner) + +end NonexistentOwner + +namespace UnrelatedOwner + +theorem owner : True := True.intro +axiom owner._native.native_decide.ax_1_1 : False +theorem target : False := owner._native.native_decide.ax_1_1 + +/-- error: MetaCheck.AxiomCheck.UnrelatedOwner.target: '+native' names 'MetaCheck.AxiomCheck.UnrelatedOwner.owner', but that declaration owns no native_decide axiom -/ +#guard_msgs (whitespace := lax) in +assert_axioms MetaCheck.AxiomCheck.UnrelatedOwner.target +native( + MetaCheck.AxiomCheck.UnrelatedOwner.owner) + +end UnrelatedOwner + +namespace ForgedDependency + +axiom owner._native.native_decide.ax_1_1 : False +theorem owner : False := owner._native.native_decide.ax_1_1 + +/-- error: 'MetaCheck.AxiomCheck.ForgedDependency.owner._native.native_decide.ax_1_1' looks like a native_decide axiom owned by 'MetaCheck.AxiomCheck.ForgedDependency.owner', but it was not emitted inside that declaration -/ +#guard_msgs (whitespace := lax) in +assert_axioms MetaCheck.AxiomCheck.ForgedDependency.owner +native( + MetaCheck.AxiomCheck.ForgedDependency.owner) + +end ForgedDependency + +namespace MacroForged + +/-! The forgery `ForgedDependency` cannot express. A top-level `axiom` command is necessarily its +own command, so its start lands *before* the owner's — which is what makes that case detectable. +Macro expansion removes exactly that tell: every declaration a macro emits inherits the macro +*invocation site* as its declaration range, so the axiom and the theorem using it share one +identical range. A non-strict start comparison accepts that automatically, and the census would +then certify an arbitrary axiom — here `False` — as a `native_decide` compiler-trust certificate. +`rangeStartsInside` therefore requires the auxiliary to start *strictly* after the owner, which no +macro-emitted sibling can do while both genuine shapes (`Genuine`, `GenuineAutoParam`) still can. -/ + +macro "forge " n:ident " : " t:term : command => + `(axiom $(Lean.mkIdent (n.getId ++ `_native ++ `native_decide ++ `ax_1_1)) : $t + theorem $n : $t := $(Lean.mkIdent (n.getId ++ `_native ++ `native_decide ++ `ax_1_1))) + +forge owner : False + +/-- error: 'MetaCheck.AxiomCheck.MacroForged.owner._native.native_decide.ax_1_1' looks like a native_decide axiom owned by 'MetaCheck.AxiomCheck.MacroForged.owner', but it was not emitted inside that declaration -/ +#guard_msgs (whitespace := lax) in +assert_axioms MetaCheck.AxiomCheck.MacroForged.owner +native( + MetaCheck.AxiomCheck.MacroForged.owner) + +end MacroForged + +namespace SecondCertificate + +/-! Two genuine certificates in one cone. The allowance compares the exact *set* of native axioms +reached against the set the named owners actually own, so an annotation that names only the first +owner goes stale the moment a second certificate enters the cone. Comparing owner sets alone would +not suffice: distinct axioms can share an owner name (see `AliasedOwner`). -/ + +theorem first : (234567 : Nat) < 234568 := by native_decide + +theorem second : (345678 : Nat) < 345679 := by native_decide + +theorem target : (234567 : Nat) < 234568 ∧ (345678 : Nat) < 345679 := ⟨first, second⟩ + +/-- error: MetaCheck.AxiomCheck.SecondCertificate.target: '+native' names [MetaCheck.AxiomCheck.SecondCertificate.first] but the native_decide axiom(s) present are owned by [MetaCheck.AxiomCheck.SecondCertificate.first, MetaCheck.AxiomCheck.SecondCertificate.second]; write '+native(MetaCheck.AxiomCheck.SecondCertificate.first, MetaCheck.AxiomCheck.SecondCertificate.second)' -/ +#guard_msgs (whitespace := lax) in +assert_axioms MetaCheck.AxiomCheck.SecondCertificate.target +native( + MetaCheck.AxiomCheck.SecondCertificate.first) + +assert_axioms MetaCheck.AxiomCheck.SecondCertificate.target +native( + MetaCheck.AxiomCheck.SecondCertificate.first, + MetaCheck.AxiomCheck.SecondCertificate.second) + +end SecondCertificate + +namespace AliasedOwner + +/-! A certifying declaration whose *own* name contains the marker components. Its auxiliary is +`owner.native_decide.smuggled._native.native_decide.ax_1_1`, so reading ownership off the prefix +before the *first* `_native`/`native_decide` component would credit it to `owner` — collapsing it +onto the legitimate certificate, where a pre-existing `+native(owner)` would cover both and admit +an undisclosed compiler-trust dependency. Ownership is decided by the *last* marker instead, so the +smuggled certificate keeps its own owner and the stale annotation fails the build. -/ + +theorem owner : (456789 : Nat) < 456790 := by native_decide + +namespace owner.native_decide + +theorem smuggled : (567890 : Nat) < 567891 := by native_decide + +end owner.native_decide + +theorem target : (456789 : Nat) < 456790 ∧ (567890 : Nat) < 567891 := + ⟨owner, owner.native_decide.smuggled⟩ + +/-- error: MetaCheck.AxiomCheck.AliasedOwner.target: '+native' names [MetaCheck.AxiomCheck.AliasedOwner.owner] but the native_decide axiom(s) present are owned by [MetaCheck.AxiomCheck.AliasedOwner.owner, MetaCheck.AxiomCheck.AliasedOwner.owner.native_decide.smuggled]; write '+native(MetaCheck.AxiomCheck.AliasedOwner.owner, MetaCheck.AxiomCheck.AliasedOwner.owner.native_decide.smuggled)' -/ +#guard_msgs (whitespace := lax) in +assert_axioms MetaCheck.AxiomCheck.AliasedOwner.target +native( + MetaCheck.AxiomCheck.AliasedOwner.owner) + +/-! The disclosure the census demands: the smuggled certificate is attributed to its own +declaration, not aliased onto `owner`. -/ +assert_axioms MetaCheck.AxiomCheck.AliasedOwner.target +native( + MetaCheck.AxiomCheck.AliasedOwner.owner, + MetaCheck.AxiomCheck.AliasedOwner.owner.native_decide.smuggled) + +end AliasedOwner + +namespace ComputableSafety + +/-! The `assert_computable` declaration checks. `unsafe` lifts the termination check, so the +reduction below inhabits `False` by bare self-reference while computing nothing — and it is a +`.defnInfo` that is not `noncomputable`, so the kind and computability checks both pass it. Only +the definition-safety check rejects it. The kernel independently refuses to let a safe declaration +depend on an unsafe one, so what the check has to catch is a reduction no safe proof consumes: +precisely a deliverable endpoint, which the census pins directly for that same reason. -/ + +unsafe def unsafeReduction : False := unsafeReduction + +/-- error: MetaCheck.AxiomCheck.ComputableSafety.unsafeReduction is marked unsafe -/ +#guard_msgs (whitespace := lax) in +assert_computable MetaCheck.AxiomCheck.ComputableSafety.unsafeReduction + +/-! `partial def` elaborates to an `opaque` constant carrying an unsafe implementation, so it is +rejected one check earlier — as not a `def` at all. Pinned so a toolchain that instead emits a +`.defnInfo` with `partial` safety is caught by the safety check rather than passing silently. -/ + +partial def partialReduction (n : Nat) : Nat := + if n = 0 then 0 else partialReduction (n - 1) + +/-- error: MetaCheck.AxiomCheck.ComputableSafety.partialReduction is not a def -/ +#guard_msgs (whitespace := lax) in +assert_computable MetaCheck.AxiomCheck.ComputableSafety.partialReduction + +/-! The positive case, so the rejections above are not passing vacuously. -/ + +def safeReduction (n : Nat) : Nat := n + 1 + +assert_computable MetaCheck.AxiomCheck.ComputableSafety.safeReduction + +end ComputableSafety + +namespace UnneededChoice + +/-! An over-broad `+choice` is rejected: the flag on a reduction that never reaches +`Classical.choice` would silently over-state the trusted base, mirroring how a stale +`+native` owner list is rejected. The choice-free reduction is the positive case's shape. -/ + +def choiceFreeReduction (n : Nat) : Nat := n + 1 + +/-- error: MetaCheck.AxiomCheck.UnneededChoice.choiceFreeReduction does not depend on Classical.choice; drop the '+choice' flag -/ +#guard_msgs (whitespace := lax) in +assert_computable MetaCheck.AxiomCheck.UnneededChoice.choiceFreeReduction +choice + +/-! The genuine-`+choice` positive case: choice entering through an erased `Prop` field. -/ + +def choiceUsingReduction (n : Nat) : { m : Nat // ∃ k, m = n + k } := + ⟨n + 1, Classical.choice ⟨⟨1, rfl⟩⟩⟩ + +assert_computable MetaCheck.AxiomCheck.UnneededChoice.choiceUsingReduction +choice + +end UnneededChoice + +end MetaCheck.AxiomCheck diff --git a/MetaCheck/CompiledOverride.lean b/MetaCheck/CompiledOverride.lean new file mode 100644 index 0000000..3bd98cc --- /dev/null +++ b/MetaCheck/CompiledOverride.lean @@ -0,0 +1,116 @@ +/- +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, Tal Derei +-/ +import CompElliptic.Meta.AxiomCheck + +/-! +# Regression tests for the compiled-body-override checks + +`@[implemented_by]` and `@[extern]` swap the body the compiler runs while the kernel keeps +reducing the original, and Lean checks no relation between the two. A declaration carrying either +is still a `.safe` `.defnInfo`, is not `noncomputable`, and introduces no axiom, so every other +check in `CompElliptic.Meta.AxiomCheck` passes it — which is what makes this the one census bypass +that reaches a *value*: a `native_decide` certificate over doctored data reports a match against +data the kernel refutes. + +The declarations here are deliberately doctored, so they live in this test-only library, out of the +production `CompElliptic` import graph, alongside the forged axioms of `MetaCheck.AxiomCheck` — +and in a module of their own, because `checkCompiledBodyDisclosure` is a property of the whole +import closure: once an override exists here, every later census entry in this module fails, which +is exactly the third case below but would swamp the unrelated entries of the sibling file. + +The order of this file is therefore load-bearing: the clean entries come first, while the module +still has nothing to report. +-/ + +namespace MetaCheck.CompiledOverride + +/-! ## Clean module + +Both commands pass while nothing in the closure substitutes a compiled body — so the rejections +below are not passing vacuously, and the disclosure check is not simply always-on. -/ + +def cleanReduction (n : Nat) : Nat := n + 1 + +assert_computable MetaCheck.CompiledOverride.cleanReduction + +theorem cleanTheorem : (2 : Nat) + 2 = 4 := rfl + +assert_axioms MetaCheck.CompiledOverride.cleanTheorem + +/-! ## An ambient-package target + +The disclosure sweep exempts the ambient roots — the toolchain and the pinned dependency stack, not +the toolchain alone. `Nat.add` is `@[extern]`, as are most of the arithmetic and container +primitives whose compiled code every `native_decide` runs regardless. Censusing one *directly* is a +different claim, though: there the substitution is the entry's own subject rather than background +compiler trust, and `assert_computable`'s "genuinely computed" would be asserted of a body that +never runs. The per-declaration check therefore applies to any target. -/ + +/-- error: Nat.add carries '@[extern]', so its compiled body is not the body the kernel reduces and Lean checks no relation between the two. Nothing this census verifies about the kernel term constrains what compiled code — a `native_decide` over it in particular — computes. -/ +#guard_msgs (whitespace := lax) in +assert_computable Nat.add + +/-! ## The bypass + +`capturedData` stands in for natively-certified data: `assert_computable` sees a plain safe `def` +whose axioms are empty, `native_decide` evaluates the *compiled* body and certifies the match, and +the kernel disagrees — `refutesAtKernel` proves the negation of what `fingerprintMatch` proves, +both about the same constant. Every check that predates this file accepts the pair. -/ + +def honestCaptured : List Nat := [1, 2, 3] + +unsafe def doctoredImpl : List Nat := [9, 9, 9] + +@[implemented_by doctoredImpl] def capturedData : List Nat := honestCaptured + +def target : List Nat := [9, 9, 9] + +theorem fingerprintMatch : capturedData = target := by native_decide + +theorem refutesAtKernel : capturedData ≠ target := by decide + +/-- error: MetaCheck.CompiledOverride.capturedData carries '@[implemented_by]', so its compiled body is not the body the kernel reduces and Lean checks no relation between the two. Nothing this census verifies about the kernel term constrains what compiled code — a `native_decide` over it in particular — computes. -/ +#guard_msgs (whitespace := lax) in +assert_computable MetaCheck.CompiledOverride.capturedData + +/-! ## The certificate that consumes it + +Pinning the doctored data is only half the bypass: the entry that actually launders it is the +`assert_axioms` on the `native_decide` certificate, whose own declaration is clean. What that entry +reaches is a compiled body, which no axiom footprint records — so it is caught by the closure-wide +disclosure check, naming the declaration responsible. -/ + +/-- error: MetaCheck.CompiledOverride.fingerprintMatch cannot be censused: MetaCheck.CompiledOverride.capturedData (@[implemented_by]) substitute(s) a compiled body Lean never checks against the kernel body, so the value the compiler runs is unconstrained by anything proved about it. If you must, use `@[csimp]` instead, but be aware that `@[csimp]` still substantially increases the trust surface. -/ +#guard_msgs (whitespace := lax) in +assert_axioms MetaCheck.CompiledOverride.fingerprintMatch +native( + MetaCheck.CompiledOverride.fingerprintMatch) + +/-! An entry with no connection at all to the doctored declaration fails too. The census states the +artifact's trusted base, and an unchecked compiled body inside it is undisclosed compiler trust +wherever it sits; scoping the check to each entry's dependency cone would let the same commit that +adds the override keep every unrelated entry green. -/ + +/-- error: MetaCheck.CompiledOverride.honestCaptured cannot be censused: MetaCheck.CompiledOverride.capturedData (@[implemented_by]) substitute(s) a compiled body Lean never checks against the kernel body, so the value the compiler runs is unconstrained by anything proved about it. If you must, use `@[csimp]` instead, but be aware that `@[csimp]` still substantially increases the trust surface. -/ +#guard_msgs (whitespace := lax) in +assert_computable MetaCheck.CompiledOverride.honestCaptured + +/-! ## `@[extern]` + +The same swap without an `unsafe` helper: the compiled body becomes a foreign symbol, about which +nothing at all is known. Both checks report it exactly as they report `@[implemented_by]`. -/ + +@[extern "compelliptic_metacheck_doctored_symbol"] def externData : List Nat := honestCaptured + +/-- error: MetaCheck.CompiledOverride.externData carries '@[extern]', so its compiled body is not the body the kernel reduces and Lean checks no relation between the two. Nothing this census verifies about the kernel term constrains what compiled code — a `native_decide` over it in particular — computes. -/ +#guard_msgs (whitespace := lax) in +assert_computable MetaCheck.CompiledOverride.externData + +/-- error: MetaCheck.CompiledOverride.cleanTheorem cannot be censused: MetaCheck.CompiledOverride.capturedData (@[implemented_by]), MetaCheck.CompiledOverride.externData (@[extern]) substitute(s) a compiled body Lean never checks against the kernel body, so the value the compiler runs is unconstrained by anything proved about it. If you must, use `@[csimp]` instead, but be aware that `@[csimp]` still substantially increases the trust surface. -/ +#guard_msgs (whitespace := lax) in +assert_axioms MetaCheck.CompiledOverride.cleanTheorem + +end MetaCheck.CompiledOverride diff --git a/MetaCheck/NativeSurface.lean b/MetaCheck/NativeSurface.lean new file mode 100644 index 0000000..d3d8c57 --- /dev/null +++ b/MetaCheck/NativeSurface.lean @@ -0,0 +1,112 @@ +/- +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, Tal Derei +-/ +import CompElliptic.Meta.AxiomCheck + +/-! +# Regression tests for the native-certificate evaluated surface + +A `native_decide` auxiliary axiom asserts that the compiler's evaluation of a closed `Bool` term is +the kernel's. `partial def` breaks the premiss: the kernel constant is `opaque` with no body, and +what the compiler runs in its place is an `unsafe` implementation with the termination check lifted. +A certificate over such a constant therefore says nothing about anything the kernel could have +checked — and the entry that would launder it is the `assert_axioms` on the certificate, whose own +declaration is clean, so no per-declaration check reaches it. + +These declarations live in the test-only library for the same reason as `MetaCheck.AxiomCheck` and +`MetaCheck.CompiledOverride`: the production `CompElliptic` import graph must never reach them. +This is a module of its own so the closure-wide compiled-body sweep, which the sibling file +deliberately trips, does not mask the checks pinned here. +-/ + +namespace MetaCheck.NativeSurface + +/-! ## The honest shape + +A certificate over ordinary `def` data passes, so the rejections below are not vacuous and the +check is not simply refusing every `+native` entry. -/ + +def honestCaptured : List Nat := [1, 2, 3] + +theorem honestMatch : honestCaptured = [1, 2, 3] := by native_decide + +assert_axioms MetaCheck.NativeSurface.honestMatch +native( + MetaCheck.NativeSurface.honestMatch) + +/-! ## `partial` data under a certificate + +`capturedPartial` needs a parameter only because `partial` requires a function type; the compiled +body still ignores it and returns the attacker's list. The kernel cannot confirm the certificate, +and — unlike the `@[implemented_by]` bypass, where the kernel value refutes the compiled one — it +cannot refute it either, because there is no kernel value at all. -/ + +partial def capturedPartial (_ : Unit) : List Nat := + if 0 = 0 then [9, 9, 9] else capturedPartial () + +def target : List Nat := [9, 9, 9] + +theorem partialMatch : capturedPartial () = target := by native_decide + +/-- error: MetaCheck.NativeSurface.partialMatch: the native_decide certificate evaluated the `partial` declaration(s) [MetaCheck.NativeSurface.capturedPartial], whose compiled body is an unsafe implementation the kernel never sees and whose kernel constant has no body at all. Nothing relates what ran to what the certificate says. Give the evaluated data an ordinary `def`. -/ +#guard_msgs (whitespace := lax) in +assert_axioms MetaCheck.NativeSurface.partialMatch +native( + MetaCheck.NativeSurface.partialMatch) + +/-! The data itself was already rejected — a `partial def` is not a `def` — which is what makes the +certificate entry the one that has to catch this. Pinned so the two halves stay distinguishable. -/ + +/-- error: MetaCheck.NativeSurface.capturedPartial is not a def -/ +#guard_msgs (whitespace := lax) in +assert_computable MetaCheck.NativeSurface.capturedPartial + +/-! ## A sealed `opaque` is not reported + +The reduction-barrier idiom: the opaque's *type* carries the equation to its source, so the kernel +can recover the value, and its compiled body is the declared one. The certificate below is +therefore honest, and the check leaves it alone. -/ + +def sealedSource : List Nat := [1, 2, 3] + +opaque sealed : { xs : List Nat // xs = sealedSource } := ⟨sealedSource, rfl⟩ + +theorem sealedMatch : sealed.val = [1, 2, 3] := by rw [sealed.property]; native_decide + +assert_axioms MetaCheck.NativeSurface.sealedMatch +native( + MetaCheck.NativeSurface.sealedMatch) + +/-! ## `partial` behind a `@[csimp]` replacement + +The auxiliary axiom records the term as the *kernel* sees it, and `@[csimp]` replaces a constant +wholesale in compiled code — so the certificate below runs `csimpFast` where its own statement says +`csimpSlow`, and a walk of the statement alone would never reach `hiddenBehindCsimp`. This is the +routing the fast lane anticipates: `CompElliptic.Curves.Pasta.Fast.Projective` keeps the proven +equality `padd_eq_paddFast` for a future registration, and the replacement target's cone is where +a `partial` would sit unnoticed. + +The csimp lemma stays at the end of the file: a replacement applies to code compiled after it, and +the honest certificates above must be elaborated without it to keep their own coverage meaningful. -/ + +partial def hiddenBehindCsimp (_ : Unit) : Nat := hiddenBehindCsimp () + +def csimpSlow (n : Nat) : Nat := n + +/-- Equal to `csimpSlow` — the `partial` call sits in an argument the body discards, which is what +lets the replacement be *proved* while still putting `hiddenBehindCsimp` in the compiled cone. -/ +def csimpFast (n : Nat) : Nat := (fun _ => n) (hiddenBehindCsimp ()) + +@[csimp] theorem csimpSlow_eq_csimpFast : @csimpSlow = @csimpFast := by + funext n; rfl + +assert_axioms MetaCheck.NativeSurface.csimpSlow_eq_csimpFast + +theorem csimpCert : csimpSlow 7 = 7 := by native_decide + +/-- error: MetaCheck.NativeSurface.csimpCert: the native_decide certificate evaluated the `partial` declaration(s) [MetaCheck.NativeSurface.hiddenBehindCsimp], whose compiled body is an unsafe implementation the kernel never sees and whose kernel constant has no body at all. Nothing relates what ran to what the certificate says. Give the evaluated data an ordinary `def`. -/ +#guard_msgs (whitespace := lax) in +assert_axioms MetaCheck.NativeSurface.csimpCert +native( + MetaCheck.NativeSurface.csimpCert) + +end MetaCheck.NativeSurface diff --git a/lakefile.toml b/lakefile.toml index 829b6b4..3621260 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,6 +1,6 @@ name = "CompElliptic" version = "0.1.0" -defaultTargets = ["CompElliptic"] +defaultTargets = ["CompElliptic", "MetaCheck"] [leanOptions] pp.unicode.fun = true # pretty-prints `fun a ↦ b` @@ -20,6 +20,15 @@ rev = "d458e5cebd364b15660ff8de20ec964dcd52c120" name = "CompElliptic" globs = ["CompElliptic.*"] +# Regression-test-only declarations for `CompElliptic.Meta.AxiomCheck`: forged axioms and +# doctored compiled bodies exercising the census's rejection paths. A separate library outside +# `CompElliptic/`, so they never enter the production import graph and the source-level sweeps +# (`scripts/check_csimp_census.sh`, `scripts/check_native_optin.py`) do not scan them; a default +# target, so a plain `lake build` still runs the regression checks. +[[lean_lib]] +name = "MetaCheck" +globs = ["MetaCheck.+"] + # Native-compiles the Montgomery arithmetic, which is meant to be run (`#eval`, `native_decide`), # not only proven about. Every module here must import nothing outside Lean core: codegen runs over # the whole import closure, so one mathlib-side import silently makes the build enormous -- hence