Repository navigation
ci(proofs): gate T-RECEIPT in CI and record the two deliberate hatches #196
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
hyperpolymath
wants to merge
6
commits into
main
Choose a base branch
from
claude/new-session-th4e9w-proof-honesty
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from all commits
Commits
Show all changes
6 commits
Select commit
Hold shift + click to select a range
7f673e7
ci(proofs): gate T-RECEIPT in CI and record the two deliberate hatches
claude 9c6eb1b
ci(proofs): restrict the toolchain downloads to HTTPS, redirects incl…
claude 92bb6f7
docs(proofs): record the §2.2 statement comparison for T-RECEIPT
claude f30f629
ci(proofs): check each Rocq theorem's closure; record the Coq package
claude 97b19a6
ci(proofs): fail the rocq job unless the kernel is Coq 8.18.x
claude 5d375a3
ci(proofs): check the Coq version without a pipe that pipefail could …
claude File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,136 @@ | ||
| // SPDX-License-Identifier: CC-BY-SA-4.0 | ||
| = T-RECEIPT: statement correspondence (PROOF-POLICY §2.2) | ||
| :toc: | ||
|
|
||
| This record compares the Agda statement of T-RECEIPT with its Rocq and Lean | ||
| re-proofs, as PROOF-POLICY §2.2 requires before a recheck leg can count | ||
| toward a grade. It records the comparison only. A leg is `RECONCILED` when | ||
| this comparison exists *and* its kernel has accepted it, so each leg's state | ||
| below depends on an observed run, not on this text. | ||
|
|
||
| == Sources | ||
|
|
||
| [cols="1,3,2",options="header"] | ||
| |=== | ||
| |Prover |File |Mode | ||
|
|
||
| |Agda (source of truth) | ||
| |`proofs/agda/ReceiptBoundary.agda` | ||
| |`--safe --without-K --cubical-compatible --exact-split --no-sized-types | ||
| --no-guardedness`, no libraries | ||
|
|
||
| |Rocq | ||
| |`proofs/theory/rocq/ReceiptBoundary.v` | ||
| |`re-proved`, no libraries beyond the prelude loaded by default | ||
|
|
||
| |Lean | ||
| |`proofs/theory/lean/ReceiptBoundary.lean` | ||
| |`re-proved`, core only, no Mathlib | ||
| |=== | ||
|
|
||
| Both legs are independent re-proofs. Neither is transported, so neither | ||
| depends on a translator. | ||
|
|
||
| == Universe and type discipline | ||
|
|
||
| [cols="2,2,2,2",options="header"] | ||
| |=== | ||
| |Notion |Agda |Rocq |Lean | ||
|
|
||
| |Claims and evidence | ||
| |`Set` (`Set₀`) | ||
| |`Set`, predicative (no `-impredicative-set`) | ||
| |`Type` (`Sort 1`) | ||
|
|
||
| |The warrant record | ||
| |`Warrant : Set → Set₁` | ||
| |`ReceiptWarrant : Set → Type`, a universe above `Set` | ||
| |`ReceiptWarrant : Type → Type 1` | ||
|
|
||
| |The soundness record | ||
| |`SoundWarrant w : Set` | ||
| |`SoundReceiptWarrant w : Type` | ||
| |`SoundReceiptWarrant w : Type` | ||
|
|
||
| |Empty claim | ||
| |`data Empty : Set` (no constructors) | ||
| |`Empty_set : Set` (prelude, no constructors) | ||
| |`Empty : Type` (core, no constructors) | ||
|
|
||
| |Unit evidence | ||
| |`record Unit : Set` (eta holds) | ||
| |`unit : Set` (inductive, no definitional eta) | ||
| |`Unit` = `PUnit.{1}` (structure eta holds) | ||
| |=== | ||
|
|
||
| None of the three uses `Prop`. That is deliberate: a `Prop`-only | ||
| reformulation would quantify over a different class of claims, and §2.2 asks | ||
| for the same proposition, not a weaker one. | ||
|
|
||
| == Propositions compared | ||
|
|
||
| Implicit arguments are shown in braces in every column. | ||
|
|
||
| [cols="1,3",options="header"] | ||
| |=== | ||
| |Theorem |Statement in all three provers | ||
|
|
||
| |`receive-with-soundness` / `receive_with_soundness` / `receiveWithSoundness` | ||
| |For every claim `{Claim}` in the base universe, every warrant `w` for it and | ||
| every soundness witness for `w`, there is an inhabitant of `Claim`. | ||
|
|
||
| |`empty-claim-token` / `empty_claim_token` / `emptyClaimToken` | ||
| |A warrant for the empty claim whose evidence type is the unit type and whose | ||
| evidence is its constructor. This is a definition, compared so that the next | ||
| two theorems refer to the same object. | ||
|
|
||
| |`no-unconditional-reflection` / `no_unconditional_reflection` / | ||
| `noUnconditionalReflection` | ||
| |A function that, for every claim in the base universe, turns any warrant for | ||
| it into an inhabitant of the claim, yields an inhabitant of the empty type. | ||
|
|
||
| |`no-soundness-for-empty-token` / `no_soundness_for_empty_token` / | ||
| `noSoundnessForEmptyToken` | ||
| |A soundness witness for `empty-claim-token` yields an inhabitant of the empty | ||
| type. | ||
| |=== | ||
|
|
||
| The quantifier structure, the argument order and the result type match | ||
| term for term. The proofs are also the same terms: application of the | ||
| soundness field to the evidence field, and instantiation of the reflection | ||
| function at the empty claim. | ||
|
|
||
| == Residual assumptions and differences | ||
|
|
||
| * *Unit eta.* Rocq's `unit` has no definitional eta, while Agda's `Unit` and | ||
| Lean's `Unit` do. No statement or proof here inspects or compares unit | ||
| values, so the difference is not used. | ||
| * *Prelude.* Rocq loads `Init` by default, and Lean loads its core. Both | ||
| supply only inductive definitions here (`Empty_set`, `unit`, `Empty`, | ||
| `PUnit`). The files print their assumption sets: Rocq with | ||
| `Print Assumptions`, Lean with `#print axioms`. | ||
| * *Equality and K.* No statement uses identity types, so `--without-K` in | ||
| Agda has no counterpart obligation in either target. | ||
| * *No claim about Rust.* As in the Agda source, nothing here describes the | ||
| Rust receipt parser or any network behaviour. | ||
|
|
||
| == Correspondence state | ||
|
|
||
| [cols="1,2,3",options="header"] | ||
| |=== | ||
| |Leg |State |What moves it | ||
|
|
||
| |Rocq | ||
| |`BRIDGE-PENDING` | ||
| |The comparison above is recorded. It becomes `RECONCILED` when the `rocq` | ||
| job in `.github/workflows/proof-safety.yml` records a kernel acceptance with | ||
| all three `Print Assumptions` closed, on the commit that carries this record. | ||
|
|
||
| |Lean | ||
| |`BRIDGE-PENDING` | ||
| |The comparison above is recorded. No pinned Lean run exists yet, so there is | ||
| no kernel result to reconcile against. | ||
| |=== | ||
|
|
||
| A leg still `BRIDGE-PENDING` does not count toward a Proof Witness Grade | ||
| (PROOF-POLICY §8.2). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,22 +1,36 @@ | ||
| == Proof Debt | ||
|
|
||
| Tracks soundness-relevant escape hatches in `+echidnabot+` that the | ||
| trusted-base reducer flags as undocumented. Each is retained pending | ||
| dedicated cleanup; new occurrences should land with an inline | ||
| `+// TRUSTED:+` annotation or an entry below. | ||
| trusted-base reducer flags. New occurrences land with an inline | ||
| `+// TRUSTED:+` annotation or an entry below, following the estate | ||
| `TRUSTED-BASE-REDUCTION-POLICY.adoc`. | ||
|
|
||
| === Current entries (placeholder) | ||
| === Current entries | ||
|
|
||
| The current 2 escape hatches were inherited from earlier scaffolding and | ||
| have not yet been individually classified. Tracking issue: filed | ||
| alongside this PR. | ||
| Both hatches are deliberate negative fixtures. They are not debt to be | ||
| repaid: removing either escape hatch would break the test that proves the | ||
| detector sees it. They are excluded from every proof count and grade. | ||
|
|
||
| * Hatch 1: TBD (file:line) | ||
| * Hatch 2: TBD (file:line) | ||
| [cols="2,1,4",options="header"] | ||
| |=== | ||
| |Location |Hatch |Rationale | ||
|
|
||
| === How to populate | ||
| |`proofs/coq/admitted_stub.v:11` | ||
| |`Admitted.` | ||
| |Negative fixture. `tests/protocol_contract.rs` | ||
| (`checked_in_negative_proofs_are_detected`) asserts that echidnabot's axiom | ||
| scanner reports it. Keep the hatch intact. | ||
|
|
||
| Run the standards trusted-base reducer locally; it lists the offending | ||
| file:line tuples. Move each from "`TBD`" to a real entry with a one-line | ||
| rationale. When all entries have rationale + cleanup-issue link, this | ||
| file is fully load-bearing instead of a placeholder. | ||
| |`proofs/lean/sorry_stub.lean:7` | ||
| |`sorry` | ||
| |Negative fixture, same test. Carries an inline | ||
| `hypatia: allow code_safety/sorry` directive with this rationale. | ||
| |=== | ||
|
|
||
| === Not hatches, but not proofs either | ||
|
|
||
| `src/abi/{Types,Layout,Foreign}.idr` is unfilled template scaffolding | ||
| (`{{PROJECT}}` module names and open holes). It contains no | ||
| `believe_me`, `assert_total` or `postulate`, so the reducer does not list | ||
| it, but it is not a verified ABI. See `docs/PROOF-STATUS.adoc`, | ||
| "ABI scaffold debt". |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.