// SPDX-License-Identifier: CC-BY-SA-4.0 = Hyperpolymath Proof and Verification Policy Jonathan D.A. Jewell :toc: :toc-placement: preamble Which prover carries which kind of obligation, how theory proofs are rechecked, and when another tool is allowed. Owner ruling of 2026-10-26; it records the policy half of standards#692; the enforcing gate and the rollout are tracked there. Every hyperpolymath repository follows this file, and the repositories' `CLAUDE.md` files point here. A `CLAUDE.md` may carry a short summary of the mapping for agents arriving there; it names this file as normative and changes in the same change as this file. This policy decides *where a proof lives*. What counts as an escape hatch in a proof, and how such debt is recorded, stays with link:../docs/TRUSTED-BASE-REDUCTION-POLICY.adoc[`docs/TRUSTED-BASE-REDUCTION-POLICY.adoc`]. == 1. The mapping [cols="1,1,2",options="header"] |=== |Code or obligation |Verifier |Scope |Rust code |*Creusot* |Contracts and proofs on first-party Rust. Verification sits on the code itself, not in a parallel model of it. |Ada code |*SPARK* |SPARK applies where the code is Ada. It is not the verifier for Rust. |APIs, ABIs and engineering properties |*Idris2* |Interface and ABI contracts, totality, serialisation round-trips, dispatch and ordering invariants, bounds, and other properties of a system as built. |Theory |*Agda*, rechecked in *Rocq* and *Lean* |Mathematical content that does not depend on one system's code: lattices, orders, convergence, completeness, soundness of a calculus. Agda is the source of truth; the recheck is §2. |=== The word "Rust" in estate documents means Rust. The 2026-04-10 note that read "Rust always means Rust/SPARK" is withdrawn: SPARK belongs to Ada code, and Rust is verified with Creusot. Deciding between *engineering* and *theory*: if the statement names a type, function or wire format of one repository, it is engineering (Idris2). If it would be true of any implementation, it is theory (Agda). When an engineering property is about the behaviour of first-party Rust or Ada code (a function's pre- and postconditions, a loop invariant, absence of run-time errors), the code mapping takes precedence: it is verified with Creusot or SPARK on that code, not restated in Idris2. Idris2 carries the *interface* contract that stands apart from any one implementation: types, ABI layouts, wire formats, and the protocols several languages share. === 1.1 Third-party code This policy binds first-party code: what the estate writes and owns. Code the estate depends on but does not own (crates such as Bevy, libraries, vendored or forked upstream code) is not converted, re-proved, or annotated to meet it, and is never edited to add contracts. Where a first-party proof relies on a dependency's behaviour, state that reliance at the boundary as an assumption: a trusted specification of the called function (Creusot `#[trusted]` extern specs, a SPARK `Import` contract, an Idris2 FFI type), recorded in the repo's proof-status file as `ASSUMED` with the dependency and version it describes. A row is only as strong as the weakest step it depends on (link:../docs/README-EXPLAINME-STANDARD.adoc[`README-EXPLAINME-STANDARD.adoc`]), so a caller whose obligations were discharged using that contract is recorded as proved *relative to the assumption*: its row names the `ASSUMED` contract it rests on and is never counted as unconditionally `PROVEN` until the contract itself is checked. When choosing between dependencies that fit equally well, prefer one that carries its own checking: published proofs (Creusot, Kani, Verus, Aeneas, SPARK, or kernel-checked Lean or Rocq), a model-checked or formally specified core, or at least sustained fuzzing. Record that choice where the dependency is added. This is a preference, not a gate: a dependency with no verified alternative is still allowed, and its absence of proofs is an assumption to record, not a reason to fork and convert it. == 2. Rechecking theory proofs Every Agda theory proof is rechecked in Rocq and in Lean: . *Transport first.* The Agda proof term is carried across through Dedukti (Agda → Dedukti/Lambdapi → Rocq and Lean). echidna's exchange layer (`src/rust/exchange/`) already speaks Dedukti. A transported witness that the target kernel accepts is the strongest recheck, but the kernel checks the term only against the *translated* statement. So compare the translated statement with the Agda one (by reading it, or by a round trip back through Dedukti) and record how. Until that comparison is made, the translator is part of the trusted base for that theorem and the leg is `ASSUMED`, not `PROVEN`. . *Re-proof as fallback.* Where a construct does not translate (for example, a feature Agda2Dedukti does not cover), or where the pinned exporter has no route into the target, restate the theorem in the target prover and prove it there by hand. Check the pinned Lambdapi release for a Lean exporter before planning a transported Lean leg; until a released one exists, the Lean leg is re-proved. The statement must match the Agda statement; say how that was checked. . *Record which.* Each rechecked theorem lists, next to it in the repo's proof-status file, which route each target used: `transported` or `re-proved`, with the reason for any re-proof. No Mathlib, in Lean or elsewhere: a missing tactic or lemma is reproved by hand in the core library. A proof that needs a large external library to compile is a dependency, not a proof the estate owns. === 2.1 Canonical Agda invocation (2026-11-01) First-party Agda theory proof entrypoints shall use the following default, explicitly in local recipes and CI: [source,shell] ---- agda --safe --without-K --cubical-compatible ---- The Agda CLI option is \`--without-K\` with a capital K. \`--cubical-compatible\` is not the same as full \`--cubical\`. Pin and record the Agda version and standard library with each source commit and proof result. Missing tools, incompatible dependencies or failed theorems are open obligations: do not silently skip proofs or weaken compiler flags to make a check green. Theory proofs genuinely needing full Cubical Agda or incompatible options require an explicit, separately reviewed proof profile. Prior \`--safe\` or \`--safe --without-K\` successes are historical evidence, not receipts for this new combined profile. Existing Idris2 source/ABI proofs, Rust/Creusot and Ada/SPARK engineering checks remain active as their source repos reconcile theory: a translated model does not prove runtime refinement. === 2.2 Lean and Rocq/Coq correspondence evidence The independent witness policy in section 2 operates per *theorem*, not on matching filenames. Record for the Agda source and each target prover: exact proposition, assumptions, type/universe discipline, source revision, compiler/library versions, invocation and observed result. Declare \`transported\`, \`re-proved\` or \`unavailable\` and record the separate justification connecting their semantics and statements. A successful compilation in each prover does not establish that all proved the same proposition. Keep distinguishable statuses: AGDA-PENDING, AGDA-VERIFIED, COQ-CHECKED, LEAN-CHECKED, BRIDGE-PENDING, RECONCILED, COUNTEREXAMPLE, QUARANTINED. A reconciled claim requires a checked bridge or justified statement correspondence, independent kernel results and explicit residual assumptions. A prover cannot inspect an arbitrary Agda witness by name alone. Mathesis may catalogue proof receipts, but source projects retain local proof ownership. ECHIDNA is the longer-term automation destination, not a prerequisite for current independent checks. Do not force independent type, trope or identity projects into a Hypatia-specific proof architecture. === 2.3 Evidence-first event-chain rollout . Preserve and test existing proof gates before any migration. . Enforce this Agda invocation in the actual project scripts and CI. . Recover an exact theory theorem, port or independently reprove it faithfully in Agda and retain all assumptions. . Check a semantically matched statement in Rocq and Lean. . Establish and record the bridge, including unresolved assumptions. . Retain OPEN statuses and revalidation triggers rather than claiming estate-wide reconciliation from policy adoption. This text records a policy, not successful proof executions. The implementation PRs and their CI receipts establish those separately. == 3. Existing proofs Proofs written before this ruling are re-homed by kind, not rewritten for their own sake: * An existing Lean or Rocq proof of a *theory* statement keeps its value. The Agda statement becomes the source. The existing file counts as that prover's leg under §2 only once the Agda proof itself is `PROVEN` or `PROVEN-WITH-AXIOMS` and the file's theorem statement and assumptions have been compared with the Agda statement, with the comparison recorded. Any axioms the Agda proof rests on are listed in that leg's trust boundary too. Until then it is target-only evidence, recorded with its own status, and the Agda row stays `OPEN`. * An existing Isabelle proof of a *theory* statement is supplementary evidence. It satisfies neither the Rocq leg nor the Lean leg. * An existing proof of an *engineering* statement in a theorem prover other than Idris2 moves to Idris2 when it is next touched. Until then it stays, labelled with its prover. * Corpora that exist to exercise provers are not obligations. echidna's `proofs//` trees and similar fixtures are test material for a multi-prover system and are outside this policy. == 4. Exceptions Use another tool where it is plainly the right one: when the mapped prover would take far longer, or cannot express the property at all. Isabelle/HOL, F*, TLA+, an SMT solver or anything else is allowed on that basis. In every reasonable case, follow §1. An exception is recorded beside the artefact (a header comment) and in the repo's proof-status file. The record names the obligation, the tool used, and why the mapped prover was not the right fit. Where the reason is that a theory statement cannot be expressed in Rocq or Lean, the recorded exception stands in for that recheck leg. The leg gets no status token; instead its row carries a `waiver` field pointing to the exception record, so the closed vocabulary of §5 is unchanged. The theorem is complete when the Agda proof is `PROVEN` or `PROVEN-WITH-AXIOMS` and every leg that is not waived is too. Worked exception: *TLA+ model checking* of concurrency protocols, as in hypatia's `verification/proofs/tlaplus/KinGate.tla`. A finite model check is reported as `TESTED`, with its bounds, not as `PROVEN`. === 4.1 Standing exceptions for Rust Two tools are standing exceptions for Rust. Each one runs alongside Creusot and never replaces it. The record in the repo's proof-status file still names the obligation; the reason below need not be restated. *Kani* (bounded model checking) covers `unsafe` blocks and FFI seams, the code where Creusot's safe-Rust assumptions can fail. A Kani harness is reported as `TESTED`, with its unwinding and size bounds, as in the TLA+ case above. *Aeneas* is used only where Rust code implements a theorem proved in Agda. It translates the Rust into a Lean (or Rocq) model, and the proof about that model is checked by the target kernel. Its statement is compared with the Agda theorem's Lean or Rocq recheck as in §2. Two rows are recorded: the theorem about the model is `PROVEN`, and the correspondence between the model and the Rust code (Aeneas's translation) is a separate `ASSUMED` row, so the implementation is never counted as proved on the model alone. The backend's own axioms are part of the trust base. A backend with an axiom from which `False` is derivable cannot support any status above `ASSUMED`; Aeneas's Rocq backend is in that state (its `mk_array` axiom, Aeneas issue #1116, and it is unmaintained). Its Lean backend depends on Mathlib, which §2 rules out. Until a backend qualifies on both counts, the Rust-to-model correspondence row is recorded as `ASSUMED`. The model theorem remains `PROVEN` because its proof must be independently checked by the target kernel without those disallowed backend axioms or libraries. Adopting a backend needs a recorded owner decision. Verus is not a standing exception: it shares Creusot's SMT trust base, so it adds no independent assurance for the cost of rewriting code in its dialect. == 5. Status vocabulary Proof-status files use the closed proof-ledger vocabulary of link:../docs/README-EXPLAINME-STANDARD.adoc[`docs/README-EXPLAINME-STANDARD.adoc`]. The uppercase names below are this policy's labels for those terms. A machine-readable proof ledger records the canonical lowercase token; prose and tables may use either. * `PROVEN` is `proven`: machine-checked with no escape hatch. Either a kernel accepted a proof term, or a mapped verifier (Creusot through Why3, GNATprove, or a §4 exception tool such as F* or a direct SMT run) discharged every generated obligation with its automatic provers. In the second case the trust boundary names the tool, the provers and their versions. For a direct SMT result under §4, `PROVEN` additionally requires an independently checked certificate or an explicitly trusted checking boundary documented in that record. Without either, record `ASSUMED`; a bounded check is `TESTED`, with its bounds. * `PROVEN-WITH-AXIOMS` is `proven-with-postulates`: a kernel checked the proof, and it rests on named necessary axioms as link:../docs/TRUSTED-BASE-REDUCTION-POLICY.adoc[`TRUSTED-BASE-REDUCTION-POLICY.adoc`] allows. List the axioms. * `TESTED` is `tested-only`: checked on a bounded or sampled domain, such as property tests or model checking. Give the bounds. * `ASSUMED` is `argued`: a stated hypothesis, or a transcription that no kernel checked. * `OPEN` is `open`: not done. == 6. Toolchains The proof toolchains must be installable where the work runs: * *CI:* through the repo's Guix manifest or its container, per link:LANGUAGE-POLICY.adoc[`LANGUAGE-POLICY.adoc`] §2. * *Agent sessions:* through the cloud environment's setup script. Versions follow what each repo pins: Agda and its standard library as in CI, and Lean per project `lean-toolchain`. Creusot builds from its own repository with Cargo (its `INSTALL` script), which then uses opam for the Why3 and Why3find back ends. Lambdapi and Dedukti build through opam, and SPARK's `gnatprove` comes from Alire or its release bundles. A session or runner without access to those hosts cannot run those legs; say so instead of reporting the leg as passing. == 7. Amending this document Change the mapping only by owner ruling, and update the repositories' `CLAUDE.md` pointers in the same campaign. A gate that enforces this policy cites this file. Verify any such gate both ways, as link:LANGUAGE-POLICY.adoc[`LANGUAGE-POLICY.adoc`] §3 requires: it passes on conforming input and fails on a planted violation.