From 3bf7f8e3772572fbf7342af2b953f75a9b104be4 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:28:09 +0000 Subject: [PATCH] =?UTF-8?q?proof(flags):=20canonical=20--cubical-compatibl?= =?UTF-8?q?e=20invocation=20in=20force;=20grades=20as=20PROOF-POLICY=20?= =?UTF-8?q?=C2=A78=20PWG?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PROOF-POLICY §2.1 names `agda --safe --without-K --cubical-compatible` as the canonical invocation; waiver W-1 kept the flag off, on the belief that only a relational big-step semantics could remove the last 13 warnings (`just`-injectivity in Noninterference.Generic). That belief was wrong: - Prelude: `just-inj` defined by `cong` through the computing projection `from-just`, which needs no unification rule. - Noninterference.Generic: the six clauses that matched `refl` against `exec … ≡ just t` now carry agreement along `just-inj` (`just-≈`, `just-≈₂`). No statement, semantics or fixture changed. - scripts/proof-flags.sh: `--cubical-compatible` added. Gate, laws certificate and receipt all run under it. - tests/flag-control/IndexedMatch.agda + scripts/check.sh: a correct proof that only the flag refuses; the gate fails if it is ever accepted. Removing the flag was tested to fail the gate. The relational route would not have sufficed on its own: a probe proving determinism of `c , s ⇓ t` raised 22 UnsupportedIndexedMatch warnings (inverting two derivations of one command needs Cmd injectivity). Grades: "mathesis Grade 3" was the unratified brief's wording. PROOF-POLICY §8 (2026-11-04) supersedes it and makes PWG-3 depend on the §2.1 invocation, so the theorems were `ungraded` while W-1 was open; they are PWG-3 now. The receipt carries the §8.5 fields (pwg, foundation-diverse, per-leg route, token and §2.2 state), derives the grade from leg states (tested: one RECONCILED leg -> 2i, two -> 2ii, BRIDGE-PENDING does not count), pins the PROOF-POLICY commit (§7), and moves from agda-grade3_praxis.deed to agda_praxis.deed because a grade is derived and can change. EXPLAINME listed --cubical-compatible as a checker flag while it was waived; that line is now true. README's Lintel pin corrected (ee01db4 -> d1d843b). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017yYi5JxzXZs6nz1ZSForfP --- .github/workflows/proofs.yml | 2 +- CHANGELOG.adoc | 17 ++ PROOF-STATUS.adoc | 164 +++++++++--------- README.adoc | 21 +-- docs/EXPLAINME.adoc | 8 +- docs/proof-debt.adoc | 42 +++-- scripts/check.sh | 18 ++ scripts/grade-receipt.sh | 88 ++++++---- scripts/proof-flags.sh | 23 ++- src/SecretTypes/Noninterference/Generic.agda | 25 ++- src/SecretTypes/Prelude.agda | 32 ++-- tests/flag-control/IndexedMatch.agda | 14 ++ ...da-grade3_praxis.deed => agda_praxis.deed} | 56 +++--- 13 files changed, 319 insertions(+), 191 deletions(-) create mode 100644 tests/flag-control/IndexedMatch.agda rename verification/receipts/{agda-grade3_praxis.deed => agda_praxis.deed} (56%) diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 116e91a0..38a4947a 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -80,4 +80,4 @@ jobs: - name: Emit the receipt for this commit run: | bash scripts/grade-receipt.sh --write --commit "$(git rev-parse --short=12 HEAD)" - sed -n '1,80p' verification/receipts/agda-grade3_praxis.deed + sed -n '1,80p' verification/receipts/agda_praxis.deed diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 889f9d56..9388d1ec 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -10,6 +10,23 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. ==== Fixed +* **The canonical Agda invocation is in force, and grades follow PROOF-POLICY §8.** +** `--cubical-compatible` (PROOF-POLICY §2.1) is in `scripts/proof-flags.sh`, so + the gate, the laws certificate and the receipt all run under + `--safe --without-K --cubical-compatible`. The thirteen + `just`-injectivity clauses in `Noninterference.Generic` read the run's result + through `Prelude.just-inj`, defined by `cong`, not by matching. No statement, + semantics or fixture changed. Waiver W-1 is closed. +** `tests/flag-control/IndexedMatch.agda` proves the flag is in force: + `scripts/check.sh` fails if that fixture is ever accepted. +** "mathesis Grade 3" was the unratified brief's wording; the theorems are now + recorded as `PWG-3` with the §8.5 fields (`pwg`, `foundation-diverse`, and + each leg's route, token and §2.2 state). The receipt moved from + `agda-grade3_praxis.deed` to `agda_praxis.deed`, because a grade is derived + and can change, and pins the `PROOF-POLICY` commit it reads. +** `docs/EXPLAINME.adoc` listed `--cubical-compatible` among the checker flags + while the flag was waived; that line is now true. + * **The template's gates could not fail, and the toolchain was not minted.** Reported from JuliaPackageSpitter.jl and traced here; see `docs/reports/compliance/RSR-TEMPLATE-DAMAGE-2026-10-30.adoc` for the full diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index da8bfbc4..eb22b47a 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -1,45 +1,48 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 = secret-types — Proof Status -:revdate: 2026-11-01 +:revdate: 2026-11-09 -Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN, with the closed ledger -tokens of `standards/docs/README-EXPLAINME-STANDARD.adoc` §5 in +Statuses are the closed vocabulary of `standards/3-practice/PROOF-POLICY.adoc` +§5 (PROVEN / PROVEN-WITH-AXIOMS / TESTED / ASSUMED / OPEN), with the matching +ledger tokens of `standards/docs/README-EXPLAINME-STANDARD.adoc` §5 in link:docs/EXPLAINME.adoc#proof-ledger[the Proof Ledger]. Every PROVEN line names -its module. All modules are `--safe --without-K --no-libraries`, checked with -`--double-check` and `-W error` by -`scripts/check.sh`, no postulates. The flag set and the Agda pin live in exactly -one place, `scripts/proof-flags.sh`, so this file, the gate and the receipt -cannot disagree. CI: TESTED. `.github/workflows/proofs.yml` (Debian 13, -`agda-bin=2.6.4.3-1+b2`) ran both gates green on f149e08, run -https://github.com/hyperpolymath/secret-types/actions/runs/39289501788[39289501788], -whose log ends `PASS: minimal-laws certificate (3 laws, each needed)`. - -== Grade, and the independent-witness legs - -This repository reports **mathesis Grade 3** and no higher. The grade is not a -claim we invented: it is the estate's own record vocabulary -(`mathesis/estate-mathematical-architecture` §5), and Grade 3 is precisely -"type-checks locally in Agda under strict flags, not translated to an independent -foundational system". - -[cols="1,2,2",options="header"] +its module. Every module is checked by `scripts/check.sh` under the §2.1 +canonical invocation, `agda --safe --without-K --cubical-compatible`, and four +stricter flags (`--no-libraries --ignore-interfaces --double-check -W error`), +with no postulates. The flag set and the Agda pin live in exactly one place, +`scripts/proof-flags.sh`, so this file, the gate and the receipt cannot +disagree, and a flag-control fixture proves the flag is really in force. + +== Proof Witness Grades, and the independent-witness legs + +Grades here are the estate's *Proof Witness Grades*, `PROOF-POLICY.adoc` §8 +(owner ruling 2026-11-04): `PWG-3`, `PWG-2i`, `PWG-2ii`, `PWG-1`, lower is +stronger, `ungraded` below the ladder. They are derived from the receipt, never +asserted (§8.4). This file previously said "mathesis Grade 3", the unratified +brief's wording; §8 supersedes it, and its `PWG-3` additionally needs the §2.1 +invocation, which this repository has met since waiver W-1 closed. + +[cols="1,1,3",options="header"] |=== -| Claim | Grade | Why not higher +| Claim | PWG | Why not higher -| N-1, N-2, N-3, N-7, N-8, N-9 | *Grade 3* | No Rocq leg and no Lean leg exists. Under - `standards/3-practice/PROOF-POLICY.adoc` §2 both are required for Grade 2i/ii, - and `transported`/`re-proved` is the only vocabulary either leg may use. +| N-1, N-2, N-3, N-7, N-8, N-9 | `PWG-3` | The Agda proof is PROVEN under the §2.1 + invocation (receipt below). No Rocq leg and no Lean leg exists, so no leg + counts (§8.2). No axioms: `--safe`, a postulate scan of the import cone, and the + recorded cone. `foundation-diverse`: no. -| N-4, N-5, N-6 | below Grade 3 (`tested-only`) | They are checked demonstrations — - refusals, computed witnesses, a shell-orchestrated law-ablation certificate — - not theorems. Mathesis grades theorems; recording these as Grade 3 would grade - the wrong object. - -| Termination-sensitive noninterference under the current typing rules | REFUTED | N-9 - formalizes the N-5 counterexample when finishing versus non-finishing is - observable. A stronger typing discipline remains open. Declassification is OPEN. +| N-4, N-5, N-6 | `ungraded` | TESTED demonstrations (refusals, computed + witnesses, a law-ablation certificate), not theorems; §8.1 grades theory + theorems only. |=== +N-9 is a proved *refutation*: termination-sensitive noninterference is false for +the current typing rules when finishing versus non-finishing is observable. A +stronger typing discipline is OPEN, and so is declassification. + +A grade is not a discharge (§8.4.1): at `PWG-3` every theorem above still owes +its Rocq and Lean legs (§2). + === The two legs, recorded honestly `PROOF-POLICY.adoc` §2 requires every Agda theory proof to be rechecked in Rocq @@ -52,12 +55,10 @@ would need its own CI receipt. |=== | Claim | Rocq leg | Lean leg | Record -| N-1, N-2, N-3, N-7, N-8 | `unavailable` | `unavailable` -| No Agda→Dedukti transport has been attempted from this repository (the - estate's exchange layer lives in `echidna`, and `PROOF-POLICY` §2.2 names - ECHIDNA as a longer-term destination, not a prerequisite), and no hand - re-proof has been attempted. Nothing was skipped silently: this is the - opening state, stated. +| N-1, N-2, N-3, N-7, N-8, N-9 | `unavailable` (`OPEN`) | `unavailable` (`OPEN`) +| No Agda→Dedukti transport and no hand re-proof has been attempted from this + repository yet. §2.2 state of each: `AGDA-VERIFIED`. Nothing was skipped + silently: this is the opening state, stated. | all rows | — | — | *A leg that does not exist cannot be evidenced by a file that happens to be @@ -70,64 +71,55 @@ would need its own CI receipt. link:docs/reports/audit/consistency-audit-2026-11-01.adoc. |=== -Should a leg ever be attempted, `PROOF-POLICY` §2.2 fixes the record: exact +When a leg is attempted, `PROOF-POLICY` §2.2 fixes the record: exact proposition, assumptions, universe discipline, source revision, compiler and library versions, invocation, observed result, and the bridge or statement -correspondence — *transported* or *re-proved* — and the local statuses +correspondence — *transported* or *re-proved* — and the correspondence states AGDA-VERIFIED / COQ-CHECKED / LEAN-CHECKED / BRIDGE-PENDING before RECONCILED. +Only a RECONCILED leg raises the grade. -=== What the grade does *not* include: `--cubical-compatible` +=== The §2.1 invocation, and how waiver W-1 closed `PROOF-POLICY` §2.1 (dated 2026-11-01) names -`agda --safe --without-K --cubical-compatible` as the canonical invocation. This -repository meets `--safe` and `--without-K`, is stricter in four other dimensions, -and **does not** use `--cubical-compatible`. That was tested, not assumed: the -flag was adopted on 2026-11-01 and the gate refused three times, twice for -construction-injectivity lemmas (fixed: one deleted as dead code, one replaced by -a retraction that computes definitionally) and then at `Lattice.agda:46`, where -every clause matching on `_⊑_` is an *indexed match* — a property of how the -two-point order is represented, not a stray lemma. - -Part of it was then fixed for real: the two-point order was an indexed family -(matching a proof needed injectivity of the index constructors `L`/`H`), and it is -now a **computed predicate** (`L ⊑ _ = ⊤`, `H ⊑ L = ⊥`), so the order laws hold -by computation and those warnings are gone. What remains is one class — -`just`-injectivity in the fuel semantics — which needs the big-step relation -rather than an equality on computed results, and that changes how N-5 states -divergence. Both arms, the two shortcuts that were measured and failed, and that -consequence are in `docs/proof-debt.adoc#waivers`. - -The gap is recorded rather than closed by suppressing the warning: a gate that -says `-WnoUnsupportedIndexedMatch` would be a green gate over a weakened check. -Full evidence, the two arms (keep the waiver, or re-represent the order as a -computed predicate), and what would make the waiver wrong are in -link:docs/proof-debt.adoc#waivers[`docs/proof-debt.adoc` W-1]; the receipt carries -`cubical-compatible = "waived"` so it is machine-visible. The grade is unaffected: -mathesis Grade 3 is "type-checks locally in Agda under strict flags, not -translated", and this gate is strict on the axes that bear on soundness. +`agda --safe --without-K --cubical-compatible` as the canonical invocation. It is +in force. Adopting it took two rounds: + +* *2026-11-01.* Two constructor-injectivity lemmas were removed or re-expressed + (`just-inj` deleted, `_≟_` through `pred`), and the two-point order became a + computed predicate (`L ⊑ _ = ⊤`, `H ⊑ L = ⊥`), which removed every + `L`/`H`-injectivity warning. Thirteen warnings remained, all + `just`-injectivity in `Noninterference.Generic`, from matching `refl` + against `exec … ≡ just t`. The flag was waived (W-1), on the belief that only + a relational big-step semantics could remove them. +* *2026-11-09.* That belief was wrong, and was measured rather than argued. The + thirteen clauses now read the run's result through `Prelude.just-inj`, defined + by `cong` through a computing projection, which needs no unification rule. The + statements, the semantics and every fixture are unchanged. Conversely, a + relational semantics alone would *not* have been enough: a probe proving + determinism of `c , s ⇓ t` raised 22 `UnsupportedIndexedMatch` warnings, + because inverting two derivations of one command needs injectivity of `Cmd`'s + constructors. + +The warning is never suppressed. `tests/flag-control/IndexedMatch.agda` is a +correct proof that only `--cubical-compatible` refuses; `scripts/check.sh` fails +if it is ever accepted, so dropping the flag cannot pass the gate (tested both +ways). W-1 is kept, closed, in link:docs/proof-debt.adoc#waivers[`docs/proof-debt.adoc`]. === What the grade is anchored to -`verification/receipts/agda-grade3_praxis.deed`, generated by -`scripts/grade-receipt.sh` and checked in CI, records the exact source commit, -the Agda pin and provenance, the flag set, the `sha256` of every module, the -claim IDs with their ledger tokens and legs, and the trust-base counts -(`postulates = 0`, `escape-hatches = 0`, `library-dependencies = 0`, -`axioms-assumed = 0`). A change to a proved statement cannot leave the receipt -intact; a claim added here cannot leave the receipt intact either, in either -direction. +`verification/receipts/agda_praxis.deed`, generated by `scripts/grade-receipt.sh` +and checked in CI, records the exact source commit, the Agda pin and provenance, +the flag set, the `PROOF-POLICY` commit it reads (`hyperpolymath/standards` +`9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5`), the `sha256` of every module (the +import cone of `SecretTypes.All`), the trust-base counts (`postulates = 0`, +`escape-hatches = 0`, `library-dependencies = 0`, `axioms-assumed = 0`), and for +each claim its ledger token, its derived `pwg`, `foundation-diverse`, and each +leg's route, token and §2.2 state (§8.5). A change to a proved statement cannot +leave the receipt intact; a claim added here cannot leave the receipt intact +either, in either direction. Proof debt, in the four dispositions the trusted-base policy requires, is -link:docs/proof-debt.adoc[] — all four empty, and enforced rather than asserted — -and that file's `#waivers` section carries the one obligation this repository does -not meet (`--cubical-compatible`), with its evidence and both arms. - -CI: the whole gate — core proofs, expected rejections, the laws certificate, the -receipt drift check and the receipt emit — is green on `8e421cc`, run -link:https://github.com/hyperpolymath/secret-types/actions/runs/41327614303[41327614303]. -That run is also the evidence for the two Agda changes the flag attempt forced -(`just-inj` removed as dead code, `_≟_` re-expressed through `pred`), which is why -they are recorded rather than quietly folded in. +link:docs/proof-debt.adoc[] — all four empty, and enforced rather than asserted. == Fragment (stated before the claims) diff --git a/README.adoc b/README.adoc index bcfcd936..eab38ce0 100644 --- a/README.adoc +++ b/README.adoc @@ -37,7 +37,7 @@ worth stating because it was measured on 2026-11-01: link:https://github.com/metadatastician/lintel[`metadatastician/lintel`] imports `SecretTypes.{Prelude,Vars,Lattice.Record,Lang,Noninterference.Generic}`, defines `reader-sets : Lattice`, and opens the generic TINI at it, so the estate does -have a mechanised consumer of this calculus. It is pinned at `ee01db4`; Lintel's +have a mechanised consumer of this calculus. It is pinned at `d1d843b`; Lintel's own gate was run against this repository's HEAD on 2026-11-01 and passes, so the lattice re-representation described in link:docs/proof-debt.adoc#waivers[the proof-debt record] is non-breaking for it. Recording a consumer that exists is @@ -76,16 +76,17 @@ Echo fibre over its outputs does not separate secret inputs — the Echo reading of noninterference, and the first candidate connection Secret → Echo for `nextgen-typing/docs/TYPE-CONNECTIONS.adoc`. -*Grade.* The proved claims are **mathesis Grade 3** and no higher: they -type-check in Agda under the estate's canonical strict flags -(`scripts/proof-flags.sh`) and have not been translated to an independent -foundational system. The Rocq and Lean recheck legs that `PROOF-POLICY.adoc` §2 -requires for Grade 2 do not exist; they are recorded `unavailable`, not skipped -silently. Per-claim evidence is in link:docs/EXPLAINME.adoc#proof-ledger[the Proof -Ledger], the machine record is -link:verification/receipts/agda-grade3_praxis.deed[`verification/receipts/agda-grade3_praxis.deed`] +*Grade.* The proved theorems are at **`PWG-3`** (a Proof Witness Grade, +`standards/3-practice/PROOF-POLICY.adoc` §8) and no higher: they type-check in +Agda under the canonical §2.1 invocation, `--safe --without-K +--cubical-compatible`, plus four stricter flags (`scripts/proof-flags.sh`), with +no axioms. The Rocq and Lean recheck legs that §2 requires do not exist yet, so +no leg counts; they are recorded `unavailable`, not skipped silently, and a grade +is not a discharge. Per-claim evidence is in +link:docs/EXPLAINME.adoc#proof-ledger[the Proof Ledger], the machine record is +link:verification/receipts/agda_praxis.deed[`verification/receipts/agda_praxis.deed`] (checked in CI), and link:docs/proof-debt.adoc[proof debt] is empty in all four -dispositions. This paragraph states no grade the ledger does not support. +dispositions. This paragraph states no grade the receipt does not support. == Where things belong diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index 41ae5e3e..aa4cd955 100644 --- a/docs/EXPLAINME.adoc +++ b/docs/EXPLAINME.adoc @@ -103,10 +103,10 @@ only tested or still open. Tokens are the standard's closed vocabulary. | Independent recheck in Rocq and in Lean (PROOF-POLICY §2) | open | — -| `PROOF-STATUS.adoc` "Grade and the independent-witness legs", - `verification/receipts/agda-grade3_praxis.deed` +| `PROOF-STATUS.adoc` "Proof Witness Grades, and the independent-witness legs", + `verification/receipts/agda_praxis.deed` | No transport has been attempted and no hand re-proof exists, so every proven - row above is Grade 3 and no higher. The template skeletons under + theorem above is `PWG-3` (PROOF-POLICY §8) and no higher. The template skeletons under `verification/proofs/{coq,lean4}` are *not* these legs and prove nothing here. | Strengthened termination-sensitive typing discipline @@ -123,7 +123,7 @@ only tested or still open. Tokens are the standard's closed vocabulary. | The baseline declassifies nothing, by design. |=== -The machine copy of this ledger is `verification/receipts/agda-grade3_praxis.deed` +The machine copy of this ledger is `verification/receipts/agda_praxis.deed` (generated by `scripts/grade-receipt.sh`; CI fails if it drifts from the tree or from the claim IDs in `PROOF-STATUS.adoc`). diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index 015ee881..e8757a4f 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -18,7 +18,7 @@ empty, and that emptiness is *enforced* rather than asserted. `scripts/check.sh` refuses the build if any `.agda` file under `src/SecretTypes` or `tests` contains `postulate`, and the same tree is compiled with `--safe`, which independently refuses `postulate`, `{-# TERMINATING #-}`, `{-# NON_TERMINATING #-}` -and `--type-in-type`. `verification/receipts/agda-grade3_praxis.deed` records the +and `--type-in-type`. `verification/receipts/agda_praxis.deed` records the counts (`postulates = 0`, `escape-hatches = 0`) *derived from the tree*, and CI fails if they move. @@ -67,12 +67,12 @@ _None in the proof development._ Two items are open *obligations* rather than proof debt, and are listed here so that they are not mistaken for either: -* *Grade 2 legs.* `PROOF-POLICY.adoc` §2 asks for every Agda theory proof to be - rechecked in Rocq and in Lean. Neither leg exists; both are recorded +* *Rocq and Lean legs.* `PROOF-POLICY.adoc` §2 asks for every Agda theory proof + to be rechecked in Rocq and in Lean. Neither leg exists; both are recorded `unavailable` in the receipt and in link:../PROOF-STATUS.adoc[`PROOF-STATUS.adoc`]. An absent recheck is not an - escape hatch in a proof — the proof has no hole — but it does bound the grade - at 3, and that bound is recorded rather than glossed. + escape hatch in a proof — the proof has no hole — but it bounds every theorem + at `PWG-3` (§8), and that bound is recorded rather than glossed. * *Termination-sensitive noninterference.* `Noninterference.OutcomeVisibility.termination-sensitive-fails` refutes TSNI for the current typing rules when finishing versus non-finishing is public. @@ -93,13 +93,34 @@ places is a claim the gate does not support. [[waivers]] == Waivers — obligations this repository does not meet +None open. W-1 below is closed and kept for its evidence. + A waiver is not an escape hatch inside a proof and not proof debt. It is an obligation the *policy* sets that this repository does not yet satisfy, recorded in the place a reader will look. Each one names the obligation, the tool, and why the mapped option was not used (`PROOF-POLICY.adoc` §4 asks for exactly that shape when a mapped prover is not the right fit). -=== W-1 `--cubical-compatible` (PROOF-POLICY §2.1, dated 2026-11-01) +=== W-1 `--cubical-compatible` (PROOF-POLICY §2.1, dated 2026-11-01) — CLOSED 2026-11-09 + +*Closed.* The flag is in force in `scripts/proof-flags.sh`, and therefore in the +gate, the laws certificate and the receipt. The 13 remaining warnings below +(`just`-injectivity in `Noninterference.Generic`) were removed without arm B2: each +clause now reads the run's result through `Prelude.just-inj`, defined by `cong` +through the computing projection `from-just`, which needs no unification rule. +No statement, semantics or fixture changed. The flag is proved to be in force by +`tests/flag-control/IndexedMatch.agda`, a correct proof that only the flag +refuses; `scripts/check.sh` fails if it is ever accepted, and removing the flag +from `scripts/proof-flags.sh` was tested to fail the gate. + +The premise of arm B2 below also turned out to be false. A relational semantics +does not by itself satisfy the flag: a probe proving determinism of +`c , s ⇓ t` raised 22 `UnsupportedIndexedMatch` warnings, because inverting two +derivations of one command needs injectivity of `Cmd`'s constructors. A big-step +relation is still planned, as a second semantics with an adequacy theorem +(`exec` finishes iff `⇓` holds), not as a replacement and not for this flag. + +The record below is kept as it was written, for provenance. *Obligation.* `agda --safe --without-K --cubical-compatible ` is the canonical invocation for first-party Agda theory entrypoints. @@ -171,8 +192,7 @@ nominally on and the check off. The gate does not suppress it, and `scripts/proof-flags.sh` is the single place the flags live, so that change could not happen by accident. -*Consequence for the grade.* None: mathesis Grade 3 is "type-checks locally in -Agda under strict flags, not translated", and mathesis's own example flag set is -`--safe --erasure`, not §2.1's. The grade stays 3. The receipt records -`cubical-compatible = "waived"` so the gap is machine-visible rather than buried -here. +*Consequence for the grade (as written on 2026-11-01, superseded).* It said the +grade was unaffected, under the brief's "Grade 3". `PROOF-POLICY` §8 (2026-11-04) +then required the §2.1 invocation for `PWG-3`, so while W-1 was open the theorems +were `ungraded`. Closing W-1 is what makes them `PWG-3`. diff --git a/scripts/check.sh b/scripts/check.sh index e9c72372..b3f8560b 100755 --- a/scripts/check.sh +++ b/scripts/check.sh @@ -69,3 +69,21 @@ for file in "${rejects[@]}"; do echo "PASS: rejected $name at its invalid declaration" done echo "PASS: core proofs and all ${#rejects[@]} expected rejections" + +# Flag control: the canonical invocation must actually be in force. The +# fixture is a correct proof that only --cubical-compatible refuses (it needs +# constructor injectivity, -WUnsupportedIndexedMatch, fatal under -W error). +# If the flag were dropped from scripts/proof-flags.sh, the fixture would be +# accepted and this step would fail. +control=tests/flag-control/IndexedMatch.agda +log=_build/check-logs/IndexedMatch.log +if "$prover" "${flags[@]}" -i tests/flag-control "$control" >"$log" 2>&1; then + echo 'ERROR: flag control accepted: --cubical-compatible is not in force' >&2 + exit 1 +fi +if ! grep -q 'UnsupportedIndexedMatch' "$log"; then + cat "$log" + echo 'ERROR: flag control failed for a reason other than --cubical-compatible' >&2 + exit 1 +fi +echo 'PASS: flag control (--cubical-compatible is in force: an injectivity match is refused)' diff --git a/scripts/grade-receipt.sh b/scripts/grade-receipt.sh index d3cf09b8..5143d797 100755 --- a/scripts/grade-receipt.sh +++ b/scripts/grade-receipt.sh @@ -4,19 +4,21 @@ # # grade-receipt.sh [--check] # -# Writes (or checks) verification/receipts/agda-grade3_praxis.deed: the machine -# record that this repository's Agda claims are at mathesis Grade 3 and nothing -# more. +# Writes (or checks) verification/receipts/agda_praxis.deed: the machine record +# of this repository's Agda claims, each with its Proof Witness Grade. # -# Grade 3 (mathesis estate-mathematical-architecture §5): the proof -# type-checks locally in Agda under strict flags and has NOT been translated -# to an independent foundational system. +# Proof Witness Grades: standards/3-practice/PROOF-POLICY.adoc §8 (owner +# ruling 2026-11-04). PWG-3: the Agda proof is PROVEN under the §2.1 +# invocation and no Rocq or Lean leg counts yet. The record carries the +# §8.5 fields: pwg, foundation-diverse, and for each leg its route, its §5 +# token and its §2.2 correspondence state. A grade is derived, never +# asserted (§8.4): it is computed below from the legs, not typed in. # # The receipt is DERIVED from the tree, never typed by hand, except for the # claim list below, which is cross-checked against the claim IDs in # PROOF-STATUS.adoc in both directions. That makes two drifts impossible: # * a module added or changed without the receipt following it, and -# * a claim added to PROOF-STATUS.adoc without a ledger token and a grade. +# * a claim added to PROOF-STATUS.adoc without a ledger token and its legs. # # What the receipt deliberately does NOT do: it does not run Agda. It records # the gate, the flags and the pinned versions; the gate itself runs in CI @@ -27,7 +29,7 @@ set -euo pipefail cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." . scripts/proof-flags.sh -out=verification/receipts/agda-grade3_praxis.deed +out=verification/receipts/agda_praxis.deed mode= commit_override= while (( $# )); do @@ -45,30 +47,51 @@ while (( $# )); do done # ── The claim list ──────────────────────────────────────────────────────────── -# id | ledger token (README-EXPLAINME-STANDARD §5 vocabulary) | mathesis grade | -# Rocq leg (PROOF-POLICY §2) | Lean leg. +# id | ledger token (README-EXPLAINME-STANDARD §5 vocabulary) | kind | +# Rocq route | Rocq §2.2 state | Lean route | Lean §2.2 state. # Tokens are the closed vocabulary: proven | proven-with-postulates | tested-only -# | argued | open. Legs are: transported | re-proved | unavailable. +# | argued | open. Kind is theorem (graded, PROOF-POLICY §8.1) or +# demonstration (a checked example, below the ladder: `ungraded`). Leg routes +# are PROOF-POLICY §2 and §8.5: transported | re-proved | waived | unavailable. +# States are §2.2: AGDA-VERIFIED | COQ-CHECKED | LEAN-CHECKED | BRIDGE-PENDING +# | RECONCILED | COUNTEREXAMPLE | QUARANTINED. Only RECONCILED counts (§8.2). claims() { cat <<'ROWS' -N-1|proven|grade-3|unavailable|unavailable -N-2|proven|grade-3|unavailable|unavailable -N-3|proven|grade-3|unavailable|unavailable -N-4|tested-only|below-grade-3|n/a|n/a -N-5|tested-only|below-grade-3|n/a|n/a -N-6|tested-only|below-grade-3|n/a|n/a -N-7|proven|grade-3|unavailable|unavailable -N-8|proven|grade-3|unavailable|unavailable -N-9|proven|grade-3|unavailable|unavailable +N-1|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED +N-2|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED +N-3|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED +N-4|tested-only|demonstration|n/a|n/a|n/a|n/a +N-5|tested-only|demonstration|n/a|n/a|n/a|n/a +N-6|tested-only|demonstration|n/a|n/a|n/a|n/a +N-7|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED +N-8|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED +N-9|proven|theorem|unavailable|AGDA-VERIFIED|unavailable|AGDA-VERIFIED ROWS } +# PROOF-POLICY §8.2: derive the grade from the Agda token and the legs. A leg +# counts only when it is RECONCILED (§2.2); none exists yet, so no leg counts. +# Print the PWG for one claim row's token, kind and two legs' §2.2 states. +pwg_of() { + local token="$1" kind="$2" coq_state="$3" lean_state="$4" counted=0 + [[ "$kind" == theorem ]] || { printf 'ungraded'; return; } + [[ "$token" == proven || "$token" == proven-with-postulates ]] || { printf 'ungraded'; return; } + # A leg counts on its §2.2 state, never on its route: a transported or + # re-proved leg still BRIDGE-PENDING does not count. + [[ "$coq_state" == RECONCILED ]] && counted=$((counted + 1)) + [[ "$lean_state" == RECONCILED ]] && counted=$((counted + 1)) + case "$counted" in 0) printf '3' ;; 1) printf '2i' ;; 2) printf '2ii' ;; esac +} + # ── Derived facts ───────────────────────────────────────────────────────────── repo="hyperpolymath/secret-types" source_commit="${commit_override:-$(git rev-parse --short=12 HEAD 2>/dev/null || printf 'unknown')}" agda_version="$(proof_agda_pin)" agda_from="$(proof_agda_provenance)" flag_line="$(proof_flags_line)" +# The standards commit this receipt reads PROOF-POLICY at (section 7 asks a +# gate to cite the policy by repository, path and full 40-character commit). +policy_commit="9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5" # Print the Agda module paths under src/SecretTypes in sorted order. modules() { find src/SecretTypes -name '*.agda' | LC_ALL=C sort; } @@ -109,8 +132,8 @@ emit() { printf ';; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)\n' printf ';; GENERATED by scripts/grade-receipt.sh; regenerate with --write, check with --check.\n' printf ';; This describes the gate and tree; the CI log is the execution evidence.\n' - printf '(praxis-deed\n :schema-version "1.0.0"\n :canonical-name "secret-types-agda-grade3-receipt"\n' - printf ' (identity\n :project "secret-types"\n :name "agda-grade3 verification receipt"\n' + printf '(praxis-deed\n :schema-version "1.0.0"\n :canonical-name "secret-types-agda-receipt"\n' + printf ' (identity\n :project "secret-types"\n :name "Agda verification receipt with Proof Witness Grades"\n' printf ' :repository "%s"\n :repo-uuid #u5"github.com/%s"\n' "$repo" "$repo" printf ' :uuid-source "uuid5(URL, github.com/%s)"\n' "$repo" printf ' :uuid-note "F-1 remains open: template mint-path cause and local scaffolding sweep; see docs/reports/audit/consistency-audit-2026-11-01.adoc"\n' @@ -120,21 +143,28 @@ emit() { printf ' :flags-source "scripts/proof-flags.sh"\n' printf ' :flags-note "One definition, read by the gate and by this receipt; the receipt cannot describe a gate that did not run")\n' printf ' (conformance\n :policy "standards/3-practice/PROOF-POLICY.adoc"\n' - printf ' :policy-revision "owner ruling 2026-10-26; section 2.1 dated 2026-11-01"\n' + printf ' :policy-repository "hyperpolymath/standards"\n :policy-commit "%s"\n' "$policy_commit" + printf ' :policy-revision "owner ruling 2026-10-26; section 2.1 dated 2026-11-01; section 8 (PWG) 2026-11-04"\n' printf ' :canonical-invocation "agda --safe --without-K --cubical-compatible"\n' - printf ' :cubical-compatible "waived"\n :waiver-ref "docs/proof-debt.adoc#waivers"\n' - printf ' :waiver-reason "Every clause matching on the order relation is an indexed match, which Cubical Agda does not support; suppressing -WUnsupportedIndexedMatch would be a green gate over a weakened check"\n' + printf ' :cubical-compatible "in-force"\n :flag-control "tests/flag-control/IndexedMatch.agda"\n' + printf ' :closed-waiver "W-1, docs/proof-debt.adoc#waivers"\n' printf ' :stronger-than-canonical ("--no-libraries" "--ignore-interfaces" "--double-check" "-W error"))\n' printf ' (gate\n :command "bash scripts/check.sh"\n :laws-certificate "bash scripts/minimal-laws.sh"\n' printf ' :ci ".github/workflows/proofs.yml"\n :module-count %s\n :reject-fixture-count %s)\n' "$(modules | wc -l | tr -d ' ')" "$(fixtures | wc -l | tr -d ' ')" printf ' (trust-base\n :postulates %s\n :escape-hatches %s\n' "$(grep -rlw --include='*.agda' postulate src/SecretTypes tests 2>/dev/null | wc -l | tr -d ' ')" "$(escape_hits | wc -l | tr -d ' ')" printf ' :library-dependencies 0\n :axioms-assumed 0\n' printf ' :note "A non-zero count above fails the gate; the receipt is only meaningful while all four are zero")\n' - printf ' ; Grades apply to theorems; refusal fixtures and leak witnesses are below Grade 3.\n' - printf ' ; Independent Rocq and Lean legs remain unavailable: no transport or hand re-proof.\n' + printf ' ; PROOF-POLICY section 8: grades apply to theory theorems; demonstrations are ungraded.\n' + printf ' ; Rocq and Lean legs are unavailable: no transport or hand re-proof exists yet, so no leg counts.\n' printf ' (claims\n' - while IFS='|' read -r id token grade coq lean; do - printf ' (claim :id "%s" :token "%s" :grade "%s" :coq-leg "%s" :lean-leg "%s")\n' "$id" "$token" "$grade" "$coq" "$lean" + while IFS='|' read -r id token kind coq coq_state lean lean_state; do + if [[ "$kind" == theorem ]]; then + printf ' (claim :id "%s" :token "%s" :kind "%s" :pwg "%s" :foundation-diverse #f\n' "$id" "$token" "$kind" "$(pwg_of "$token" "$kind" "$coq_state" "$lean_state")" + printf ' (leg :prover "rocq" :route "%s" :token "open" :state "%s" :receipts ())\n' "$coq" "$coq_state" + printf ' (leg :prover "lean" :route "%s" :token "open" :state "%s" :receipts ()))\n' "$lean" "$lean_state" + else + printf ' (claim :id "%s" :token "%s" :kind "%s" :pwg "%s")\n' "$id" "$token" "$kind" "$(pwg_of "$token" "$kind" "$coq_state" "$lean_state")" + fi done < <(claims) printf ' )\n ; Every module hash is checked against the current tree.\n (modules\n' while read -r m; do diff --git a/scripts/proof-flags.sh b/scripts/proof-flags.sh index da3c25fe..a0ff8a22 100755 --- a/scripts/proof-flags.sh +++ b/scripts/proof-flags.sh @@ -13,24 +13,22 @@ # Conformance: standards/3-practice/PROOF-POLICY.adoc §2.1 (2026-11-01) sets # agda --safe --without-K --cubical-compatible # as the estate default for first-party Agda theory entrypoints. Every flag -# below is that default, or strictly stronger: +# below is that default, or strictly stronger; all three default flags are in +# force: # # --safe policy default. No postulates, no --type-in-type, # no termination pragmas, no unsafe features. # --without-K policy default. No UIP, no Streicher K. (Implied by # --cubical-compatible; kept explicit so the intent # survives a future flag change.) -# --cubical-compatible WAIVED, not dropped silently. PROOF-POLICY §2.1 -# (2026-11-01) names it; this development cannot meet it -# yet. Evidence and the two arms are in -# docs/proof-debt.adoc#waivers and PROOF-STATUS.adoc -# "Grade and the independent-witness legs". The short -# version: every clause matching on `_⊑_` is an indexed -# match, which Cubical Agda does not support -# (-WUnsupportedIndexedMatch), and -W error makes that -# fatal. Suppressing the warning would be a green gate -# over a weakened check, so the flag is absent and the -# gap is recorded instead. +# --cubical-compatible policy default. In force since W-1 closed: the last +# clauses that needed constructor injectivity (matching +# `refl` against `exec … ≡ just t`) now read the result +# through Prelude.just-inj, which matches nothing. The +# gate does NOT suppress -WUnsupportedIndexedMatch, and +# -W error makes any return of such a clause fatal: a +# planted `refl` match fails the gate (exit 42). +# History: docs/proof-debt.adoc#waivers, W-1 (closed). # --no-libraries stronger. Builtins only; no Agda standard library and # no sibling repository is on the path. The policy's # "no Mathlib" rule (PROOF-POLICY §2) is the Lean form of @@ -58,6 +56,7 @@ proof_flags() { printf '%s\n' \ --safe \ --without-K \ + --cubical-compatible \ --no-libraries \ --ignore-interfaces \ --double-check \ diff --git a/src/SecretTypes/Noninterference/Generic.agda b/src/SecretTypes/Noninterference/Generic.agda index fe0c1d52..69794efe 100644 --- a/src/SecretTypes/Noninterference/Generic.agda +++ b/src/SecretTypes/Noninterference/Generic.agda @@ -52,6 +52,19 @@ module _ (V : Observer 𝓛) where ≈-trans : ∀ {s s' s''} → s ≈ s' → s' ≈ s'' → s ≈ s'' ≈-trans p q x v = trans (p x v) (q x v) + -- Every store agrees with itself. + ≈-refl : ∀ {s} → s ≈ s + ≈-refl x v = refl + + -- Carry agreement along the results of finishing runs, without + -- unifying two just-terms (unsupported under --cubical-compatible). + just-≈ : ∀ {u t s} → just u ≡ just t → u ≈ s → t ≈ s + just-≈ {s = s} e p = subst (λ w → w ≈ s) (just-inj e) p + + -- The same for two runs at once. + just-≈₂ : ∀ {u u' t t'} → just u ≡ just t → just u' ≡ just t' → u ≈ u' → t ≈ t' + just-≈₂ {t = t} e e' p = subst (λ w → t ≈ w) (just-inj e') (subst (λ w → w ≈ _) (just-inj e) p) + -- A program counter V cannot see stays unseen in any branch it guards. unseen-⊔ : ∀ {pc} y → ¬ sees pc → ¬ sees (pc ⊔ y) unseen-⊔ y np v = np (sees-↓ (⊔-upper₁ _ y) v) @@ -95,8 +108,8 @@ module _ (V : Observer 𝓛) where confineL : ∀ {ℓ e c} fuel {s t} → ¬ sees ℓ → ℓ ⊢ c → exec fuel (while e c) s ≡ just t → t ≈ s - confine fuel np skip refl _ _ = refl - confine fuel {s} np (assign {x = x} {e = e} ok) refl = confine-assign x e (eval s e) s np ok + confine fuel {s} np skip e = just-≈ e (≈-refl {s}) + confine fuel {s} np (assign {x = x} {e = e} ok) j = just-≈ j (confine-assign x e (eval s e) s np ok) confine fuel np (seq t₁ t₂) e with bind-just _ _ e ... | s₁ , (e₁ , e₂) = ≈-trans (confine fuel np t₂ e₂) (confine fuel np t₁ e₁) confine fuel np (ifz {e = g} t₁ t₂) e = confineIf fuel (eval _ g) (unseen-⊔ (lab g) np) t₁ t₂ e @@ -108,7 +121,7 @@ module _ (V : Observer 𝓛) where confineW fuel zero np t e with bind-just _ _ e ... | s₁ , (e₁ , e₂) = ≈-trans (confineL fuel np t e₂) (confine fuel np t e₁) - confineW fuel (suc _) np t refl _ _ = refl + confineW fuel (suc _) {s} np t e = just-≈ e (≈-refl {s}) confineL zero np t () confineL {e = g} (suc fuel) {s} np t e = confineW fuel (eval s g) np t e @@ -140,8 +153,8 @@ module _ (V : Observer 𝓛) where → (pc ⊔ lab e) ⊢ c → s ≈ s' → execWhile fuel (eval s e) e c s ≡ just t → execWhile fuel' (eval s' e) e c s' ≡ just t' → t ≈ t' - tini fuel fuel' skip eq refl refl = eq - tini fuel fuel' (assign {x = x} {e = g} ok) eq refl refl = tini-assign x g ok eq + tini fuel fuel' skip eq e e' = just-≈₂ e e' eq + tini fuel fuel' (assign {x = x} {e = g} ok) eq e e' = just-≈₂ e e' (tini-assign x g ok eq) tini fuel fuel' (seq t₁ t₂) eq e e' with bind-just _ _ e | bind-just _ _ e' ... | s₁ , (e₁ , e₂) | s₁' , (e₁' , e₂') = tini fuel fuel' t₂ (tini fuel fuel' t₁ eq e₁ e₁') e₂ e₂' tini fuel fuel' (ifz {pc} {g} t₁ t₂) eq e e' = @@ -170,6 +183,6 @@ module _ (V : Observer 𝓛) where go : ∀ n {m} → n ≡ m → execWhile fuel n g c s ≡ just t → execWhile fuel' m g c s' ≡ just t' → t ≈ t' go zero refl e e' with bind-just _ _ e | bind-just _ _ e' ... | s₁ , (e₁ , e₂) | s₁' , (e₁' , e₂') = tini fuel fuel' (while tc) (tini fuel fuel' tc eq e₁ e₁') e₂ e₂' - go (suc n) refl refl refl = eq + go (suc n) refl e e' = just-≈₂ e e' eq tiniW {pc} {g} fuel fuel' {s} {s'} (no nv) tc eq e e' = ≈-trans (confineW fuel (eval s g) nv tc e) (≈-trans eq (≈-sym (confineW fuel' (eval s' g) nv tc e'))) diff --git a/src/SecretTypes/Prelude.agda b/src/SecretTypes/Prelude.agda index 710fa4ec..efcd38b1 100644 --- a/src/SecretTypes/Prelude.agda +++ b/src/SecretTypes/Prelude.agda @@ -39,19 +39,28 @@ data Maybe (A : Set) : Set where nothing : Maybe A just : A → Maybe A --- NOT provided: an injectivity lemma for `just`. It was here --- (`just-inj : just a ≡ just b → a ≡ b`) until 2026-11-01 and nothing used it. --- Under the canonical flag set (scripts/proof-flags.sh, which includes --- --cubical-compatible per PROOF-POLICY §2.1) it is refused: +-- Injectivity of `just`, stated so that --cubical-compatible accepts it +-- (PROOF-POLICY §2.1). The obvious definition, matching `refl` against +-- `just a ≡ just b`, asks the unifier for constructor injectivity, which +-- Agda 2.6.4.3 refuses under that flag: -- --- warning: -W[no]UnsupportedIndexedMatch --- This clause uses pattern-matching features that are not yet supported by --- Cubical Agda ... Reason: It relies on injectivity of the data constructor --- just, which is not yet supported +-- warning: -W[no]UnsupportedIndexedMatch ... It relies on injectivity of +-- the data constructor just, which is not yet supported -- --- Deleting an unused lemma is the honest fix; disabling the warning, or the --- flag, would have bought a green gate with a weaker check. If a later proof --- needs it, the way in is a cubical-compatible formulation, not a suppression. +-- An earlier copy of that definition was deleted on 2026-11-01 for this +-- reason. This one matches nothing: it projects the equation through +-- `from-just`, which computes, so no unification rule is needed. The +-- TINI proof (Noninterference.Generic) uses it wherever a finishing run's +-- result must be read off `exec … ≡ just t`. + +-- The value inside a `just`, or the default for `nothing`. +from-just : {A : Set} → A → Maybe A → A +from-just d nothing = d +from-just d (just a) = a + +-- Equal `just`s have equal contents. +just-inj : {A : Set} {a b : A} → just a ≡ just b → a ≡ b +just-inj {a = a} e = cong (from-just a) e -- Pass a present value to f and return its result; propagate nothing -- without applying f when the input is absent. @@ -122,3 +131,4 @@ dec-stable (no ¬p) h = ⊥-elim (h ¬p) -- Excluded middle holds under double negation, for every proposition. ¬¬-dec : (P : Set) → ¬ ¬ Dec P ¬¬-dec P k = k (no λ p → k (yes p)) + diff --git a/tests/flag-control/IndexedMatch.agda b/tests/flag-control/IndexedMatch.agda new file mode 100644 index 00000000..a7d53350 --- /dev/null +++ b/tests/flag-control/IndexedMatch.agda @@ -0,0 +1,14 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +module IndexedMatch where +open import SecretTypes.Prelude + +-- Must be refused, and only because --cubical-compatible is in force: this +-- is the definition of just-inj that Prelude deliberately does not use. +-- Matching refl here needs injectivity of `just`, which the flag rejects as +-- -WUnsupportedIndexedMatch, made fatal by -W error. Without the flag it +-- type-checks, so scripts/check.sh fails if this module is ever accepted: +-- that is the evidence the canonical invocation actually ran. +invalid : {A : Set} {a b : A} → just a ≡ just b → a ≡ b +invalid refl = refl diff --git a/verification/receipts/agda-grade3_praxis.deed b/verification/receipts/agda_praxis.deed similarity index 56% rename from verification/receipts/agda-grade3_praxis.deed rename to verification/receipts/agda_praxis.deed index 6675ed77..fb944398 100644 --- a/verification/receipts/agda-grade3_praxis.deed +++ b/verification/receipts/agda_praxis.deed @@ -4,31 +4,33 @@ ;; This describes the gate and tree; the CI log is the execution evidence. (praxis-deed :schema-version "1.0.0" - :canonical-name "secret-types-agda-grade3-receipt" + :canonical-name "secret-types-agda-receipt" (identity :project "secret-types" - :name "agda-grade3 verification receipt" + :name "Agda verification receipt with Proof Witness Grades" :repository "hyperpolymath/secret-types" :repo-uuid #u5"github.com/hyperpolymath/secret-types" :uuid-source "uuid5(URL, github.com/hyperpolymath/secret-types)" :uuid-note "F-1 remains open: template mint-path cause and local scaffolding sweep; see docs/reports/audit/consistency-audit-2026-11-01.adoc" :kind "theory" - :source-commit "c4391fc841f0") + :source-commit "eee4e4038503") (prover :tool "agda" :version "2.6.4.3" :provenance "Debian 13 agda-bin=2.6.4.3-1+b2" :library "none (--no-libraries; Agda builtins only)" - :flags "--safe --without-K --no-libraries --ignore-interfaces --double-check -W error" + :flags "--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -W error" :flags-source "scripts/proof-flags.sh" :flags-note "One definition, read by the gate and by this receipt; the receipt cannot describe a gate that did not run") (conformance :policy "standards/3-practice/PROOF-POLICY.adoc" - :policy-revision "owner ruling 2026-10-26; section 2.1 dated 2026-11-01" + :policy-repository "hyperpolymath/standards" + :policy-commit "9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5" + :policy-revision "owner ruling 2026-10-26; section 2.1 dated 2026-11-01; section 8 (PWG) 2026-11-04" :canonical-invocation "agda --safe --without-K --cubical-compatible" - :cubical-compatible "waived" - :waiver-ref "docs/proof-debt.adoc#waivers" - :waiver-reason "Every clause matching on the order relation is an indexed match, which Cubical Agda does not support; suppressing -WUnsupportedIndexedMatch would be a green gate over a weakened check" + :cubical-compatible "in-force" + :flag-control "tests/flag-control/IndexedMatch.agda" + :closed-waiver "W-1, docs/proof-debt.adoc#waivers" :stronger-than-canonical ("--no-libraries" "--ignore-interfaces" "--double-check" "-W error")) (gate :command "bash scripts/check.sh" @@ -42,18 +44,30 @@ :library-dependencies 0 :axioms-assumed 0 :note "A non-zero count above fails the gate; the receipt is only meaningful while all four are zero") - ; Grades apply to theorems; refusal fixtures and leak witnesses are below Grade 3. - ; Independent Rocq and Lean legs remain unavailable: no transport or hand re-proof. + ; PROOF-POLICY section 8: grades apply to theory theorems; demonstrations are ungraded. + ; Rocq and Lean legs are unavailable: no transport or hand re-proof exists yet, so no leg counts. (claims - (claim :id "N-1" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable") - (claim :id "N-2" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable") - (claim :id "N-3" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable") - (claim :id "N-4" :token "tested-only" :grade "below-grade-3" :coq-leg "n/a" :lean-leg "n/a") - (claim :id "N-5" :token "tested-only" :grade "below-grade-3" :coq-leg "n/a" :lean-leg "n/a") - (claim :id "N-6" :token "tested-only" :grade "below-grade-3" :coq-leg "n/a" :lean-leg "n/a") - (claim :id "N-7" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable") - (claim :id "N-8" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable") - (claim :id "N-9" :token "proven" :grade "grade-3" :coq-leg "unavailable" :lean-leg "unavailable") + (claim :id "N-1" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f + (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) + (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) + (claim :id "N-2" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f + (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) + (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) + (claim :id "N-3" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f + (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) + (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) + (claim :id "N-4" :token "tested-only" :kind "demonstration" :pwg "ungraded") + (claim :id "N-5" :token "tested-only" :kind "demonstration" :pwg "ungraded") + (claim :id "N-6" :token "tested-only" :kind "demonstration" :pwg "ungraded") + (claim :id "N-7" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f + (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) + (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) + (claim :id "N-8" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f + (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) + (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) + (claim :id "N-9" :token "proven" :kind "theorem" :pwg "3" :foundation-diverse #f + (leg :prover "rocq" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ()) + (leg :prover "lean" :route "unavailable" :token "open" :state "AGDA-VERIFIED" :receipts ())) ) ; Every module hash is checked against the current tree. (modules @@ -64,10 +78,10 @@ (module :path "src/SecretTypes/Lattice.agda" :sha256 "119d637de4dd4578c0eb0cd3dbad679f4281db9fa4660833fdd74b8d220ab10e") (module :path "src/SecretTypes/Lattice/Record.agda" :sha256 "25f4ee821b8e245dccb4f5f7eae9c3f1006a4b6eaeab3af14646721f14f83de3") (module :path "src/SecretTypes/Noninterference.agda" :sha256 "944231de8ab05155f2aaa8da6a37edfa32123cac25c29ea5a2e4a2d71f68ab0e") - (module :path "src/SecretTypes/Noninterference/Generic.agda" :sha256 "b57e91faa098eec4136c78fb617c4c6f139ebe175452ffd6dc91547ffe915052") + (module :path "src/SecretTypes/Noninterference/Generic.agda" :sha256 "716de16efc8ded98b0744fd38a5f95ca6e431b07dedb43e12140f5260e28af01") (module :path "src/SecretTypes/Noninterference/OutcomeVisibility.agda" :sha256 "33e63996ccb6ea5ba834dd158584b8a1fb5594d50e79c2ee2c144ffe7588d93a") (module :path "src/SecretTypes/Noninterference/Statement.agda" :sha256 "f76d84eb3a434c2f9f4203303fcf30fb04282afe787ce085d4590855b43e4c45") - (module :path "src/SecretTypes/Prelude.agda" :sha256 "8fe48747ddac6ec990ae2a72f534bdb0054d03d54e0d904a7f932c70aca924bb") + (module :path "src/SecretTypes/Prelude.agda" :sha256 "8ec095409f9424acf26e458e0ff1b129d1ca9525f37afa6d40e66bfcbd2cfed1") (module :path "src/SecretTypes/Typing.agda" :sha256 "f535815d15f4b224a028b01261af8d7f233d8b3c0a26e48ec5c4223f3afe1d42") (module :path "src/SecretTypes/Typing/Generic.agda" :sha256 "adacd5405be17ccbf845c56d2d7980d2b0eae7214a284df2bf5a64d64ccf7718") (module :path "src/SecretTypes/Vars.agda" :sha256 "f188cbc8b630b036daac4720f3cfe492bf78671f87b82850919f09091ead5422")