Repository navigation
docs(proofs): align Hypatia proof evidence with Agda reconciliation policy #994
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -10,8 +10,29 @@ neurosymbolic CI/CD platform. | |
| `+Admitted+` | ||
| * All proofs are constructive | ||
| * `+%default total+` in all Idris2 files | ||
| * Idris2 for cross-language interface and ABI contracts; runtime code | ||
| obligations follow the estate's Creusot-for-Rust/SPARK-for-Ada mapping | ||
| * For implementation-independent theory, Agda is the primary proof target. | ||
| Convert an earlier proof where possible; otherwise re-prove the theorem | ||
| in Agda, then transport the witness to Rocq/Coq and Lean. Re-prove the | ||
| same statement only when transport is unavailable or unsupported. A | ||
| translation alone is not a proof. | ||
| * Every Agda check runs: agda --safe --without-K --cubical-compatible | ||
| against a pinned toolchain. Capital K is required. | ||
| * For each target recheck, record the statement/assumption correspondence, | ||
| checker version, exact invocation, receipt and source/witness digest. | ||
| Missing tools, unchecked transports and unsuccessful checks are not | ||
| promoted to PROVEN. An unsuccessful translation does not refute or | ||
| delete the earlier theorem. | ||
| * Canonical estate policy: | ||
| https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[Proof and Verification Policy]. | ||
| This file is a proof inventory, not an independent alternative policy. | ||
|
Comment on lines
+27
to
+29
There was a problem hiding this comment.
Once this line makes the canonical policy authoritative, the inventory below remains incompatible with its closed Useful? React with 👍 / 👎.
Comment on lines
+27
to
+29
There was a problem hiding this comment.
When work resumes on the PageRank or echo-state obligations, this declaration sends contributors to the canonical policy while the same inventory still says both theorems are in progress with Mathlib (lines 123 and 127, repeated in the summary near line 385). The canonical rechecking policy explicitly disallows Mathlib in Lean or elsewhere and requires missing lemmas to be reproved in the core library, so leaving those plans in the now-canonical inventory directs future work toward a noncompliant proof dependency. Useful? React with 👍 / 👎. |
||
|
|
||
| NOTE: This repo currently verifies Idris2, Lean and TLA+ artefacts in CI. | ||
| It does not yet run an Agda + Rocq + Lean reconciliation pipeline. | ||
| The pre-existing Lean files below retain their documented scope; they | ||
| must not be represented as independently rechecking Agda proofs until | ||
| the checked Agda source and correspondence evidence actually exist. | ||
|
|
||
| === Proof Inventory | ||
|
|
||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For repository-specific engineering obligations that are neither cross-language contracts nor properties of first-party Rust or Ada code—such as the pipeline-state, quarantine, and rollback properties already inventoried below—this summary provides no mapped verifier and can misclassify them as Agda theory. The canonical policy §1 explicitly assigns APIs, ABIs, and engineering properties to Idris2, deferring only Rust/Ada implementation behavior to Creusot/SPARK; retain that engineering-property category here.
Useful? React with 👍 / 👎.