From 2f342bced31234e03dbbb6379c8eace11c39ee35 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 12:58:36 +0000 Subject: [PATCH 1/7] proof: meet the canonical Agda invocation (--cubical-compatible); grades as PWG-3 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, and §8.2 (owner ruling 2026-11-04) makes PWG-3 conditional on it. The gate lacked the flag (waiver W-1), so the proved rows were `ungraded` under §8, although PROOF-STATUS said "mathesis Grade 3". The last blocker was 13 `-WUnsupportedIndexedMatch` warnings: the proofs matched `exec fuel c s ≡ just t` against `refl`, which needs injectivity of `just`. W-1 said only a relational semantics would remove them, at the cost of restating N-5. That was unnecessary. SecretTypes.Prelude now defines `from-just` and `just-injective e = cong (from-just a) e`, a retraction (the same move `suc-dec` makes with `pred`), and Noninterference.Generic routes the six affected clauses through one helper, `≈-just`. The semantics, N-5 and every theorem statement are unchanged. - scripts/proof-flags.sh: adds --cubical-compatible to the single flag set. check.sh, minimal-laws.sh and the receipt all read it. - Receipt renamed agda-grade3_praxis.deed to agda-pwg_praxis.deed. It records `cubical-compatible "met"` and a §8.5 `:pwg` per claim: 3 for the theorems, n/a for the checked demonstrations (§8.1). - PROOF-STATUS, README, EXPLAINME and proof-debt now say PWG-3, never a bare grade. W-1 is recorded closed, with the history and the corrected arm. The Rocq and Lean legs stay `unavailable`, and PWG-3 is stated not to discharge them (§8.4). Checked locally on Agda 2.6.4.3: scripts/check.sh (core proofs, all 4 expected rejections at their intended declarations), scripts/minimal-laws.sh (3 laws, each needed), grade-receipt.sh --check (15 modules), and DEED lint of the new receipt against standards@8e48b1c. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs --- .github/workflows/proofs.yml | 2 +- PROOF-STATUS.adoc | 114 +++++++-------- README.adoc | 15 +- build/just/proofs.just | 2 +- docs/EXPLAINME.adoc | 8 +- docs/proof-debt.adoc | 134 +++++++----------- scripts/grade-receipt.sh | 51 +++---- scripts/proof-flags.sh | 20 ++- src/SecretTypes/Noninterference/Generic.agda | 23 ++- src/SecretTypes/Prelude.agda | 29 ++-- ...rade3_praxis.deed => agda-pwg_praxis.deed} | 39 +++-- 11 files changed, 209 insertions(+), 228 deletions(-) rename verification/receipts/{agda-grade3_praxis.deed => agda-pwg_praxis.deed} (69%) diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 116e91a0..7a8540ed 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-pwg_praxis.deed diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index da8bfbc4..dea8ce18 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -1,6 +1,6 @@ // 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 @@ -14,45 +14,50 @@ cannot disagree. CI: TESTED. `.github/workflows/proofs.yml` (Debian 13, 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 +== Proof Witness Grades, 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". +Grades here are `PROOF-POLICY.adoc` §8 Proof Witness Grades (owner ruling +2026-11-04), always written with their `PWG-` prefix. Until 2026-11-09 this file +said "mathesis Grade 3". §8 replaced that wording, and §8.2 makes `PWG-3` +conditional on the §2.1 invocation, which this repository did not meet until +W-1 closed (below). Before 2026-11-09 the honest grade of every row was +therefore `ungraded`, not 3. [cols="1,2,2",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`* | PROVEN under the canonical + invocation `agda --safe --without-K --cubical-compatible`, with stronger flags + besides (`scripts/proof-flags.sh`). No Rocq leg and no Lean leg counts, so + `PWG-2i` is not reached. `PWG-3` is not a discharge (§8.4): each of these + theorems still owes both §2 legs. -| 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. +| N-4, N-5, N-6 | n/a | They are checked demonstrations (refusals, computed + witnesses, a shell-orchestrated law-ablation certificate), not theory + theorems. §8.1 grades theorems only. | 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. |=== +No theorem rests on an axiom: `postulates = 0` and `escape-hatches = 0` in the +receipt, under `--safe` (§8.4, "axioms travel with the grade"). + === The two legs, recorded honestly `PROOF-POLICY.adoc` §2 requires every Agda theory proof to be rechecked in Rocq and in Lean, by transport through Dedukti first and by hand re-proof as the fallback, with the route named per theorem. Neither leg exists here, and the -policy is explicit that a policy's adoption is not an execution: each row below +policy is explicit that adopting a policy does not execute it: each row below would need its own CI receipt. [cols="1,1,1,3",options="header"] |=== | Claim | Rocq leg | Lean leg | Record -| N-1, N-2, N-3, N-7, N-8 | `unavailable` | `unavailable` +| N-1, N-2, N-3, N-7, N-8, N-9 | `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 @@ -76,58 +81,45 @@ library versions, invocation, observed result, and the bridge or statement correspondence — *transported* or *re-proved* — and the local statuses AGDA-VERIFIED / COQ-CHECKED / LEAN-CHECKED / BRIDGE-PENDING before RECONCILED. -=== What the grade does *not* include: `--cubical-compatible` +=== The canonical invocation is met: `--cubical-compatible` (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. The +gate now runs it, with `--no-libraries --ignore-interfaces --double-check -W +error` besides, so any `-WUnsupportedIndexedMatch` is fatal rather than +suppressed. + +Two changes made the flag hold; neither changes a statement. The two-point +order became a computed predicate on 2026-11-01 (W-1 arm B1). On 2026-11-09 the +last class of warnings went: the proofs used to match an equation +`exec fuel c s ≡ just t` against `refl`, which needs injectivity of `just`. They +now read the result through `just-injective`, a retraction +(`cong (from-just a)`, `SecretTypes.Prelude`), the same move `suc-dec` makes with +`pred`. W-1 had said only a relational semantics would do (arm B2), at the cost +of restating N-5; that turned out to be unnecessary, and the semantics, N-5 and +every theorem statement are unchanged. The record is in +link:docs/proof-debt.adoc#waivers[`docs/proof-debt.adoc` W-1]. === What the grade is anchored to -`verification/receipts/agda-grade3_praxis.deed`, generated by +`verification/receipts/agda-pwg_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. +the Agda pin and provenance, the flag set, the `sha256` of every module (the +import cone: builtins only), the claim IDs with their ledger tokens, PWGs 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. 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. +Its `#waivers` section now carries no open waiver; W-1 is kept there, closed, +as the record of how the flag came to hold. + +CI history: the gate without `--cubical-compatible` was green on `8e421cc`, run +link:https://github.com/hyperpolymath/secret-types/actions/runs/41327614303[41327614303], +which is also the evidence for the two Agda changes the first flag attempt +forced (`just-inj` removed as dead code, `_≟_` re-expressed through `pred`). == Fragment (stated before the claims) diff --git a/README.adoc b/README.adoc index bcfcd936..82744c2f 100644 --- a/README.adoc +++ b/README.adoc @@ -76,14 +76,15 @@ 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 +*Grade.* The proved claims are at Proof Witness Grade **`PWG-3`** +(`PROOF-POLICY.adoc` §8) and no higher: they type-check in Agda under the +canonical §2.1 invocation, `--cubical-compatible` included, with stronger flags +besides (`scripts/proof-flags.sh`). The Rocq and Lean recheck legs that §2 +requires, and that `PWG-2i`/`PWG-2ii` count, do not exist; they are recorded +`unavailable`, not skipped silently. `PWG-3` is not a discharge: those legs are +still owed. 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`] +link:verification/receipts/agda-pwg_praxis.deed[`verification/receipts/agda-pwg_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. diff --git a/build/just/proofs.just b/build/just/proofs.just index 605f71d5..fb4db237 100644 --- a/build/just/proofs.just +++ b/build/just/proofs.just @@ -40,7 +40,7 @@ proof-check-coq: proof-scan-dangerous: @bash scripts/scan-dangerous.sh -# Regenerate the Grade-3 verification receipt (mathesis §6; PROOF-STATUS +# Regenerate the verification receipt (PROOF-POLICY §8 Proof Witness Grades; PROOF-STATUS # "Grade, and the independent-witness legs"). CI runs the --check form, so a # committed receipt that no longer matches the tree fails the gate. proof-receipt: diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index 41ae5e3e..16f80b2f 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-pwg_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 + row above is at `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-pwg_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..84430526 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-pwg_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 - `unavailable` in the receipt and in +* *Recheck legs (`PWG-2i`/`PWG-2ii`).* `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 the grade at + `PWG-3`, 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,86 +93,62 @@ places is a claim the gate does not support. [[waivers]] == Waivers — obligations this repository does not meet +None is open. W-1 is kept below, closed, as the record of how the obligation +came to be met. + 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 *Obligation.* `agda --safe --without-K --cubical-compatible ` is the canonical invocation for first-party Agda theory entrypoints. -*State.* `--safe` and `--without-K` are in the gate. `--cubical-compatible` is -**not**, and cannot be added without changing the development or weakening the -check. - -*Evidence, from three CI runs on 2026-11-01 that adopted the flag and then had to -report why it would not stay.* The flag was added, the Agda pin was unchanged -(`2.6.4.3`, `agda-bin=2.6.4.3-1+b2`), and the gate went red three times: - -. `Prelude.agda:43` `just-inj` — *"relies on injectivity of the data constructor - `just`, which is not yet supported"*. **Fixed**: the lemma was dead code and - was deleted. -. `Prelude.agda:91` `_≟_` — *"relies on injectivity of the data constructor - `suc`"*. **Fixed**: `suc-dec` decides the predecessors and pulls the answer - back along `pred`, which computes definitionally, so no injectivity rule is - needed. -. `Lattice.agda:46` `⊑-trans` — the same warning class, this time because every - clause that matches on the two-point order is an **indexed match** on `_⊑_`. - **Not fixed.** This is not incidental: `_⊑_` is an indexed family with three - constructors and no elimination principle other than matching, and `⊑-trans`, - `⊔-upper₁`, `⊔-upper₂` and the `principal` observer all match on it. Cubical - Agda does not support indexed matching; the warning says so and offers - `-W[no]UnsupportedIndexedMatch`. - -*Two arms, labelled — and one of them has since been taken part of the way.* - -* *Arm A — keep the flag off and record this waiver.* The gate stays at - `--safe --without-K --no-libraries --ignore-interfaces --double-check -W error`: - four dimensions stricter than the canonical invocation, one flag absent. The - absent flag is the one whose absence cannot hide an unsoundness here — it - constrains compatibility with cubical transports, not the truth of the present - theorems. The waiver stands, but it is **narrower than it was** (see below). -* *Arm B — re-represent so that nothing needs index unification.* Two parts: - * *B1, done 2026-11-01.* `_⊑_` was an indexed family - (`data _⊑_ : Label → Label → Set where L⊑L; L⊑H; H⊑H`), so matching any - proof asked for injectivity of the index constructors `L`/`H`. It is now a - **computed predicate** — `L ⊑ _ = ⊤`, `H ⊑ H = ⊤`, `H ⊑ L = ⊥` — with the - laws proved by computation. The order still says exactly what it said, an - impossible flow is still `⊥` (so the three expected-rejection fixtures still - fail at their `⊑` obligation, checked), and the `H`-injectivity warnings are - **gone**: 16 → 13. One cost, recorded at the refutation that needs it: a - witness such as `L⊑H` no longer *pins* its target label by its type (since - `L ⊑ y` is `⊤` for every `y`), so `Countermodels.NoDownClosure` names its - indices explicitly (`h {x = L} {y = H}`). - * *B2, not attempted.* The 13 remaining warnings are all - `injectivity of the data constructor just`, in `tini`, `go`, `confine` and - `confineW`. They come from matching an equation of the form - `exec fuel c s ≡ just t`, where `exec` computes to `just v` and Agda must - solve `t := v` — constructor injectivity, and the cubical-unsupported step. - Two shortcuts were measured and do not work: a record-returning semantics - warns on the *record* constructor instead (probe file, 2026-11-01), and - threading the result as a variable fixes the equations it touches but not - the ones inside the clauses. The technique that does work is to stop putting - computed results in equality at all: restate the big-step semantics as a - **relation** (`data c , s ⇓ t`) and match derivations, which unify a variable - index against a constructor term instead of two constructor terms. That is a - research change with a named consequence: **N-5** (termination-insensitivity - is not vacuous) currently exhibits a program whose run returns `nothing`, - a computation; under a relational semantics divergence is the *absence* of a - derivation, so N-5 would need a new non-derivability argument. It also - changes the shape of N-1/N-7. That is an owner decision about the statement - of the theorem, not a refactor to slip into a flag change. -*What would make the waiver wrong.* If `-WUnsupportedIndexedMatch` were ever -suppressed in the gate, this waiver would become a lie — the flag would be -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. +*State.* **Met.** `scripts/proof-flags.sh` carries `--cubical-compatible` beside +`--safe --without-K --no-libraries --ignore-interfaces --double-check -W error`, +and `scripts/check.sh` and `scripts/minimal-laws.sh` pass under it: core proofs, +all four expected rejections at their intended declarations, and the +laws certificate. With `-W error`, any `-WUnsupportedIndexedMatch` fails the +gate, so the flag cannot be nominally on while the check is off. + +*History.* Three CI runs on 2026-11-01 adopted the flag and then reported why it +would not stay (Agda `2.6.4.3`, `agda-bin=2.6.4.3-1+b2`): + +. `Prelude.agda:43` `just-inj`: injectivity of `just`. Fixed then: dead code, + deleted. +. `Prelude.agda:91` `_≟_`: injectivity of `suc`. Fixed then: `suc-dec` pulls + the answer back along `pred`, which computes definitionally. +. `Lattice.agda:46` `⊑-trans`: every clause matching the two-point order was an + indexed match on `_⊑_`. Fixed then (arm B1): `_⊑_` became a computed + predicate (`L ⊑ _ = ⊤`, `H ⊑ H = ⊤`, `H ⊑ L = ⊥`). Its one cost is that a + witness such as `L⊑H` no longer pins its target label by its type, so + `Countermodels.NoDownClosure` names its indices (`h {x = L} {y = H}`). + +That left 13 warnings, all `injectivity of the data constructor just`, in `tini`, +`go`, `confine` and `confineW`. They came from matching an equation +`exec fuel c s ≡ just t` against `refl`. This record used to say that only a +relational big-step semantics would remove them (arm B2), and that this would +restate N-5 and reshape N-1/N-7, an owner decision about the theorem. + +*How it closed (2026-11-09).* That was not necessary. The proofs no longer match +such an equation. `SecretTypes.Prelude` defines `from-just` and +`just-injective e = cong (from-just a) e`, a retraction: both sides of +`cong (from-just a) e` reduce to the two values, so no injectivity rule is used. +This is the same technique `suc-dec` already uses with `pred`. In +`Noninterference.Generic` the six affected clauses go through one helper, +`≈-just : just s ≡ just t → just s′ ≡ just t′ → s ≈ s′ → t ≈ t′`, built from +`just-injective` and `subst`. The semantics, N-5 and every theorem statement are +unchanged, and the receipt's module hashes record the two changed modules. + +*What would make this record wrong.* If `-WUnsupportedIndexedMatch` were +suppressed in the gate, the flag would be nominally on and the check off. The +gate does not suppress it, and `scripts/proof-flags.sh` is the single place the +flags live. + +*Consequence for the grade.* Before this closed, the proved rows were +`ungraded` under `PROOF-POLICY` §8.2, which makes `PWG-3` conditional on the §2.1 +invocation; this file said "Grade 3" at the time. They are now `PWG-3`. The +receipt records `cubical-compatible = "met"`. diff --git a/scripts/grade-receipt.sh b/scripts/grade-receipt.sh index d3cf09b8..47d2ea93 100755 --- a/scripts/grade-receipt.sh +++ b/scripts/grade-receipt.sh @@ -4,13 +4,14 @@ # # 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-pwg_praxis.deed: the machine +# record of this repository's Agda claims and their Proof Witness Grades +# (standards/3-practice/PROOF-POLICY.adoc §8, owner ruling 2026-11-04). # -# 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. +# PWG-3 (§8.2): the Agda proof is PROVEN under the canonical §2.1 invocation +# (agda --safe --without-K --cubical-compatible, here with stronger flags +# besides) and no Rocq or Lean recheck leg counts yet. PWG-3 is not a +# discharge (§8.4): every PWG-3 theorem still owes both legs. # # 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 @@ -27,7 +28,7 @@ set -euo pipefail cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." . scripts/proof-flags.sh -out=verification/receipts/agda-grade3_praxis.deed +out=verification/receipts/agda-pwg_praxis.deed mode= commit_override= while (( $# )); do @@ -45,21 +46,22 @@ 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) | PWG (PROOF-POLICY +# §8.5: 3 | 2i | 2ii | 1 | ungraded; n/a for a checked demonstration, which +# is not a theory theorem and so not on the ladder, §8.1) | Rocq leg (§2) | Lean leg. # Tokens are the closed vocabulary: proven | proven-with-postulates | tested-only # | argued | open. Legs are: transported | re-proved | unavailable. 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|3|unavailable|unavailable +N-2|proven|3|unavailable|unavailable +N-3|proven|3|unavailable|unavailable +N-4|tested-only|n/a|n/a|n/a +N-5|tested-only|n/a|n/a|n/a +N-6|tested-only|n/a|n/a|n/a +N-7|proven|3|unavailable|unavailable +N-8|proven|3|unavailable|unavailable +N-9|proven|3|unavailable|unavailable ROWS } @@ -109,8 +111,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-pwg-receipt"\n' + printf ' (identity\n :project "secret-types"\n :name "agda verification receipt (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 +122,20 @@ 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-revision "owner ruling 2026-10-26; section 2.1 dated 2026-11-01; section 8 (PWG) dated 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 "met"\n :met-since "2026-11-09; W-1 closed, 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 ' ; PWGs apply to theory theorems (PROOF-POLICY section 8.1); refusal fixtures and leak witnesses are n/a.\n' printf ' ; Independent Rocq and Lean legs remain unavailable: no transport or hand re-proof.\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" + printf ' (claim :id "%s" :token "%s" :pwg "%s" :coq-leg "%s" :lean-leg "%s")\n' "$id" "$token" "$grade" "$coq" "$lean" 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..397c8941 100755 --- a/scripts/proof-flags.sh +++ b/scripts/proof-flags.sh @@ -20,17 +20,14 @@ # --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. Met since 2026-11-09: no clause relies +# on constructor injectivity. The `just` results of +# finishing runs are read through `just-injective`, a +# retraction (SecretTypes.Prelude), and the two-point +# order is a computed predicate. -W error makes any +# -WUnsupportedIndexedMatch fatal, so a regression fails +# the gate rather than weakening it. 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 +55,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..4eb90da7 100644 --- a/src/SecretTypes/Noninterference/Generic.agda +++ b/src/SecretTypes/Noninterference/Generic.agda @@ -52,6 +52,17 @@ 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 _ _ = refl + + -- Carry an agreement to the stores two finishing runs returned. The runs' + -- results are read through `just-injective`, a retraction, never by matching + -- `just a ≡ just b` against `refl`: that match needs constructor injectivity, + -- which `--cubical-compatible` refuses (PROOF-POLICY §2.1). + ≈-just : ∀ {s s' t t'} → just s ≡ just t → just s' ≡ just t' → s ≈ s' → t ≈ t' + ≈-just e e' eq = subst (λ u → _ ≈ u) (just-injective e') (subst (λ u → u ≈ _) (just-injective e) eq) + -- 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 +106,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 np skip e = ≈-just e refl ≈-refl + confine fuel {s} np (assign {x = x} {e = g} ok) e = ≈-just e refl (confine-assign x g (eval s g) 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 +119,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 _) np t e = ≈-just e refl ≈-refl confineL zero np t () confineL {e = g} (suc fuel) {s} np t e = confineW fuel (eval s g) np t e @@ -140,8 +151,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 +181,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..e1b9fd5d 100644 --- a/src/SecretTypes/Prelude.agda +++ b/src/SecretTypes/Prelude.agda @@ -39,19 +39,22 @@ 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: --- --- 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 --- --- 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. +-- The value inside a `just`, with a default for `nothing`. `just` is a +-- constructor, so `from-just d (just a)` computes to `a` definitionally. +from-just : {A : Set} → A → Maybe A → A +from-just d nothing = d +from-just d (just a) = a + +-- Injectivity of `just`, as a retraction rather than a rule. Matching +-- `just a ≡ just b` against `refl` asks for constructor injectivity, which +-- Cubical Agda does not support (`-WUnsupportedIndexedMatch`; fatal under the +-- canonical flags, scripts/proof-flags.sh). Here `cong (from-just a) e : +-- from-just a (just a) ≡ from-just a (just b)`, and both sides *reduce* to `a` +-- and `b` — the same move as `suc-dec` below makes with `pred`. Every proof +-- that needs the value out of a finishing run goes through this lemma and +-- never matches such an equation directly. +just-injective : {A : Set} {a b : A} → just a ≡ just b → a ≡ b +just-injective {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. diff --git a/verification/receipts/agda-grade3_praxis.deed b/verification/receipts/agda-pwg_praxis.deed similarity index 69% rename from verification/receipts/agda-grade3_praxis.deed rename to verification/receipts/agda-pwg_praxis.deed index 6675ed77..6da221af 100644 --- a/verification/receipts/agda-grade3_praxis.deed +++ b/verification/receipts/agda-pwg_praxis.deed @@ -4,31 +4,30 @@ ;; 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-pwg-receipt" (identity :project "secret-types" - :name "agda-grade3 verification receipt" + :name "agda verification receipt (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-revision "owner ruling 2026-10-26; section 2.1 dated 2026-11-01; section 8 (PWG) dated 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 "met" + :met-since "2026-11-09; W-1 closed, docs/proof-debt.adoc#waivers" :stronger-than-canonical ("--no-libraries" "--ignore-interfaces" "--double-check" "-W error")) (gate :command "bash scripts/check.sh" @@ -42,18 +41,18 @@ :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. + ; PWGs apply to theory theorems (PROOF-POLICY section 8.1); refusal fixtures and leak witnesses are n/a. ; Independent Rocq and Lean legs remain unavailable: no transport or hand re-proof. (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" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") + (claim :id "N-2" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") + (claim :id "N-3" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") + (claim :id "N-4" :token "tested-only" :pwg "n/a" :coq-leg "n/a" :lean-leg "n/a") + (claim :id "N-5" :token "tested-only" :pwg "n/a" :coq-leg "n/a" :lean-leg "n/a") + (claim :id "N-6" :token "tested-only" :pwg "n/a" :coq-leg "n/a" :lean-leg "n/a") + (claim :id "N-7" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") + (claim :id "N-8" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") + (claim :id "N-9" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") ) ; Every module hash is checked against the current tree. (modules @@ -64,10 +63,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 "7c86fcc801e256a2c4869c5ccc8302a93daa0a882e2493056e68b329ff79602a") (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 "5fea408acc63e0c91a293463913ef8f167a722cc1665f7a7010b26c8520c4072") (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") From efb9aa9ab39093e493ed793de53a02490d981c88 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:11:13 +0000 Subject: [PATCH 2/7] chore(canon): adopt canon 2.1.5 (port of the secret-types canon PR, so Canon lockstep goes green here) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Canon lockstep is red on main. standards' canon.lock records 2.1.5 (#1424: gate table 0.3.1 and the applicability policy changed; the criteria did not), and this deed declared 2.1.3. Port of hyperpolymath/rsr-template-repo#298, the spine's adoption. - secret-types_chora.deed (canon): :version 2.1.3 to 2.1.5, and :gates-sha256 2f31f46d… to 5c510bba…. The criteria hash is unchanged. The (provenance) clause keeps 2.1.3: it records the canon this repository was minted against, which is history. - tests/workflows/governance_policy_test.sh expects the 2.1.5 tuple. That test already fails on main earlier, on the governance.yml pull_request filter that #15's caller carries; this does not change that. canon.lock marks 2.1.5 status "draft"; this adopts the identity the lock records, which is what the lockstep gate compares. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs --- secret-types_chora.deed | 4 ++-- tests/workflows/governance_policy_test.sh | 12 +++++++----- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/secret-types_chora.deed b/secret-types_chora.deed index 8c4a14d1..bbcb71b7 100644 --- a/secret-types_chora.deed +++ b/secret-types_chora.deed @@ -30,9 +30,9 @@ ; equal canon.lock [canon.artifacts]; canon.lock [canon.lockstep].order is ; spine-adopts-then-canon-releases, so this clause moves FIRST. (canon - :version "2.1.3" + :version "2.1.5" :criteria-sha256 "6a5aa8857bd0d0d58ef48827938ca17c251b6b854dacf59d306388d61694d82a" - :gates-sha256 "2f31f46d4753432e0aa8c9c28f339e18e062c98dc6e6ef4ecbb76993cf37638b" + :gates-sha256 "5c510bba025be718deebb12d0333bfe7db2da43c66578b728b1a334df65290b1" :lockstep-since "2026-09-17" ; A canon change this repo cannot satisfy is a change made in the WRONG ; ORDER, not a rejected change: land the spine's adoption first, then the diff --git a/tests/workflows/governance_policy_test.sh b/tests/workflows/governance_policy_test.sh index bab332eb..a2fe91f5 100644 --- a/tests/workflows/governance_policy_test.sh +++ b/tests/workflows/governance_policy_test.sh @@ -4,7 +4,9 @@ # PR #244 configuration regressions: the retired runtime policy must not ship, # and governance must run for pull requests targeting any branch with a locked # checkout of metadatastician/standards at a full 40-hex SHA. -# PR #257 adds the proof-policy mapping and adopts canon 2.1.3. Since that +# PR #257 adds the proof-policy mapping and adopts canon 2.1.3; canon 2.1.5 (a +# PATCH: the gate table 0.3.1 and the applicability policy changed, the +# criteria did not) is adopted here, after 2.1.4 (editorial). Since that # change is documentation and configuration only, check its published contract # here without invoking any proof compiler or making network requests. # Usage: bash tests/workflows/governance_policy_test.sh @@ -191,9 +193,9 @@ console.log("PASS: new proof instructions require needs, verification, rechecks const field = (key) => execFileSync("bash", [resolve(root, "scripts/deed-field.sh"), resolve(root, "secret-types_chora.deed"), "canon", key], { encoding: "utf8" }).trim(); assert.deepEqual([field("version"), field("criteria-sha256"), field("gates-sha256")], [ - "2.1.3", + "2.1.5", "6a5aa8857bd0d0d58ef48827938ca17c251b6b854dacf59d306388d61694d82a", - "2f31f46d4753432e0aa8c9c28f339e18e062c98dc6e6ef4ecbb76993cf37638b", -], "canon 2.1.3 must retain the criteria identity and adopt the new gates identity"); -console.log("PASS: the deed adopts the complete canon 2.1.3 identity"); + "5c510bba025be718deebb12d0333bfe7db2da43c66578b728b1a334df65290b1", +], "canon 2.1.5 keeps the criteria identity and adopts the gate table 0.3.1 identity"); +console.log("PASS: the deed adopts the complete canon 2.1.5 identity"); JS From c7c0719f56df50ddc2ce1329a86ce6a55ac5b1b2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:56:34 +0000 Subject: [PATCH 3/7] Add the Rocq and Lean recheck legs: N-1..3, N-7..9 at PWG-2ii MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PROOF-POLICY §2 asks for every Agda theory proof to be rechecked in Rocq and in Lean, transport first and hand re-proof as the fallback. Transport is not available: Agda2Dedukti is an Agda backend pinned to a fork of Agda and cannot run on the pinned 2.6.4.3, and there is no released Dedukti/Lambdapi exporter to Lean 4. So both legs are hand re-proofs: - verification/legs/rocq/SecretTypes.v: Coq 8.18.0, prelude only (no Require); 11 theorems, Print Assumptions "Closed under the global context" for each. - verification/legs/lean/: Lean 4.24.0, core only (no require, no Mathlib); 11 theorems, #print axioms "does not depend on any axioms". exec is defined structurally through run, so no well-founded recursion brings in propext. - scripts/check-legs.sh pins both checkers, refuses any library, any sorry/admit/Admitted/Axiom/Parameter, and any axiom line that is not clean. CI runs it as the new legs job (Coq by Ubuntu package version, Lean by release tarball sha256). - verification/legs/README.adoc is the §2.2 correspondence record: route and reason, versions, invocations, universe discipline, the statement comparison (exec, Option, the Signature/Lattice split, Observer, Vars) and the claim-by-claim name map, state RECONCILED. The comparison is provisional until owner review. - The receipt gains a (legs) block (pins, invocations, axioms, sha256 of every leg input) and the claims move to re-proved/re-proved at PWG-2ii; grade-receipt.sh refuses a counted leg without a correspondence row, and the reverse. - PROOF-STATUS, README, EXPLAINME and proof-debt follow. Not PWG-1: no per-commit receipt of each checker's observed result yet. Not +foundation-diverse: all three provers are dependent type theories. No Agda module or statement changes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs --- .github/workflows/proofs.yml | 31 + PROOF-STATUS.adoc | 67 ++- README.adoc | 18 +- docs/EXPLAINME.adoc | 18 +- docs/proof-debt.adoc | 14 +- scripts/check-legs.sh | 63 +++ scripts/grade-receipt.sh | 67 ++- verification/legs/README.adoc | 183 ++++++ verification/legs/lean/.gitignore | 4 + verification/legs/lean/Axioms.lean | 15 + verification/legs/lean/SecretTypes.lean | 4 + .../legs/lean/SecretTypes/Countermodels.lean | 216 +++++++ .../legs/lean/SecretTypes/Generic.lean | 411 ++++++++++++++ verification/legs/lean/SecretTypes/Two.lean | 158 ++++++ verification/legs/lean/lakefile.toml | 8 + verification/legs/lean/lean-toolchain | 1 + verification/legs/rocq/.gitignore | 6 + verification/legs/rocq/SecretTypes.v | 535 ++++++++++++++++++ verification/receipts/agda-pwg_praxis.deed | 36 +- 19 files changed, 1789 insertions(+), 66 deletions(-) create mode 100755 scripts/check-legs.sh create mode 100644 verification/legs/README.adoc create mode 100644 verification/legs/lean/.gitignore create mode 100644 verification/legs/lean/Axioms.lean create mode 100644 verification/legs/lean/SecretTypes.lean create mode 100644 verification/legs/lean/SecretTypes/Countermodels.lean create mode 100644 verification/legs/lean/SecretTypes/Generic.lean create mode 100644 verification/legs/lean/SecretTypes/Two.lean create mode 100644 verification/legs/lean/lakefile.toml create mode 100644 verification/legs/lean/lean-toolchain create mode 100644 verification/legs/rocq/.gitignore create mode 100644 verification/legs/rocq/SecretTypes.v diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 7a8540ed..931dcac4 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -81,3 +81,34 @@ jobs: run: | bash scripts/grade-receipt.sh --write --commit "$(git rev-parse --short=12 HEAD)" sed -n '1,80p' verification/receipts/agda-pwg_praxis.deed + # The Rocq and Lean recheck legs (PROOF-POLICY §2), re-proved by hand from + # the Agda statements (verification/legs/README.adoc gives the route and the + # statement correspondence). Both provers are pinned: Coq by its Ubuntu + # package version, Lean by its release tarball's sha256. Neither leg may use + # an axiom or a library; scripts/check-legs.sh refuses either. + legs: + name: Rocq and Lean recheck legs (no axioms, no libraries) + runs-on: ubuntu-24.04 + timeout-minutes: 30 + steps: + - name: Install the pinned Coq + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -y coq=8.18.0+dfsg-1build2 zstd + - name: Install the pinned Lean (release tarball, sha256-checked) + env: + LEAN_URL: https://github.com/leanprover/lean4/releases/download/v4.24.0/lean-4.24.0-linux.tar.zst + LEAN_SHA256: b14f5e5159219dd1a1956c3b806813319f5e94ccd5bdfd56f54520609a5bb5ec + run: | + set -euo pipefail + curl --proto '=https' --proto-redir '=https' --tlsv1.2 -fsSL "$LEAN_URL" -o "$RUNNER_TEMP/lean.tar.zst" + echo "$LEAN_SHA256 $RUNNER_TEMP/lean.tar.zst" | sha256sum --check --strict + mkdir -p "$RUNNER_TEMP/lean" + tar --zstd -xf "$RUNNER_TEMP/lean.tar.zst" -C "$RUNNER_TEMP/lean" + echo "$RUNNER_TEMP/lean/lean-4.24.0-linux/bin" >> "$GITHUB_PATH" + - name: Checkout + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Both legs check, with no axioms + run: bash scripts/check-legs.sh diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index dea8ce18..4205ca63 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -27,11 +27,13 @@ therefore `ungraded`, not 3. |=== | Claim | PWG | Why not higher -| N-1, N-2, N-3, N-7, N-8, N-9 | *`PWG-3`* | PROVEN under the canonical +| N-1, N-2, N-3, N-7, N-8, N-9 | *`PWG-2ii`* | PROVEN under the canonical invocation `agda --safe --without-K --cubical-compatible`, with stronger flags - besides (`scripts/proof-flags.sh`). No Rocq leg and no Lean leg counts, so - `PWG-2i` is not reached. `PWG-3` is not a discharge (§8.4): each of these - theorems still owes both §2 legs. + besides (`scripts/proof-flags.sh`), and both §2 legs count: re-proved in Rocq + and in Lean, kernel-checked with no axioms, `RECONCILED` (below). Not + `PWG-1`: that needs a per-commit receipt of each checker's observed result, + and the receipt records the gate, not its result. `foundation_diverse` is + false: Agda, Rocq and Lean are all dependent type theories (§8.3). | N-4, N-5, N-6 | n/a | They are checked demonstrations (refusals, computed witnesses, a shell-orchestrated law-ablation certificate), not theory @@ -42,44 +44,51 @@ therefore `ungraded`, not 3. observable. A stronger typing discipline remains open. Declassification is OPEN. |=== -No theorem rests on an axiom: `postulates = 0` and `escape-hatches = 0` in the -receipt, under `--safe` (§8.4, "axioms travel with the grade"). +No theorem rests on an axiom (§8.4, "axioms travel with the grade"). In Agda: +`postulates = 0` and `escape-hatches = 0` in the receipt, under `--safe`. In +Rocq, `Print Assumptions` reports `Closed under the global context` for every +leg theorem; in Lean, `#print axioms` reports `does not depend on any axioms`. -=== The two legs, recorded honestly +=== The two legs `PROOF-POLICY.adoc` §2 requires every Agda theory proof to be rechecked in Rocq and in Lean, by transport through Dedukti first and by hand re-proof as the -fallback, with the route named per theorem. Neither leg exists here, and the -policy is explicit that adopting a policy does not execute it: each row below -would need its own CI receipt. +fallback, with the route named per theorem. Both legs exist since 2026-11-09. +Their §2.2 record (statements, universe discipline, versions, invocations, +assumptions) is link:verification/legs/README.adoc[`verification/legs/README.adoc`]; +`bash scripts/check-legs.sh` checks them, and CI runs it as the `legs` job. -[cols="1,1,1,3",options="header"] +[cols="1,1,1,1,3",options="header"] |=== -| Claim | Rocq leg | Lean leg | Record - -| N-1, N-2, N-3, N-7, N-8, N-9 | `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. - -| all rows | — | — -| *A leg that does not exist cannot be evidenced by a file that happens to be - present.* `verification/proofs/coq/TypeSafety.v`, +| Claim | Rocq leg | Lean leg | §2.2 state | Record + +| N-1, N-2, N-3, N-7, N-8, N-9 | `re-proved`, PROVEN | `re-proved`, PROVEN +| `RECONCILED` +| Transport is not available: Agda2Dedukti is an Agda backend pinned to a fork + of Agda and cannot run on 2.6.4.3, and there is no released Dedukti or + Lambdapi exporter to Lean 4. So each leg restates the Agda theorem and proves + it by hand: Coq 8.18.0 with the prelude only, Lean 4.24.0 with core only (no + Mathlib). The statement comparison was written by Claude Code and is + provisional until the owner reviews it (estate doctrine 4). + +| N-4, N-5, N-6 | n/a | n/a | n/a +| Checked demonstrations, not theorems (§8.1). + +| all rows | — | — | — +| *A file that happens to be present is not a leg.* + `verification/proofs/coq/TypeSafety.v`, `verification/proofs/lean4/ApiTypes.lean` and the other skeletons under `verification/proofs/` are RSR template boilerplate ("replace with your project's …"). They prove nothing, they are not the legs, and their - `MANIFEST` lines claiming `gated` are false — no workflow invokes + `MANIFEST` lines claiming `gated` are false: no workflow invokes `scripts/check-proofs.sh`. Recorded as finding F-4 in link:docs/reports/audit/consistency-audit-2026-11-01.adoc. |=== -Should a leg ever be 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 -AGDA-VERIFIED / COQ-CHECKED / LEAN-CHECKED / BRIDGE-PENDING before RECONCILED. +The receipt's `(legs)` block records each leg's pinned checker, invocation and +axiom check, and the `sha256` of every leg source, so a change to a leg cannot +leave the receipt intact. `scripts/grade-receipt.sh` also refuses a claim that +counts a leg without a row in the correspondence record, and the reverse. === The canonical invocation is met: `--cubical-compatible` (W-1, closed) diff --git a/README.adoc b/README.adoc index 82744c2f..5e34580f 100644 --- a/README.adoc +++ b/README.adoc @@ -76,14 +76,18 @@ 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 at Proof Witness Grade **`PWG-3`** -(`PROOF-POLICY.adoc` §8) and no higher: they type-check in Agda under the +*Grade.* The proved claims are at Proof Witness Grade **`PWG-2ii`** +(`PROOF-POLICY.adoc` §8) and no higher. They type-check in Agda under the canonical §2.1 invocation, `--cubical-compatible` included, with stronger flags -besides (`scripts/proof-flags.sh`). The Rocq and Lean recheck legs that §2 -requires, and that `PWG-2i`/`PWG-2ii` count, do not exist; they are recorded -`unavailable`, not skipped silently. `PWG-3` is not a discharge: those legs are -still owed. Per-claim evidence is in link:docs/EXPLAINME.adoc#proof-ledger[the Proof -Ledger], the machine record is +besides (`scripts/proof-flags.sh`). Each is also re-proved by hand in Rocq +(Coq 8.18.0, prelude only) and in Lean (4.24.0, core only, no Mathlib), with no +axioms in either, and the statements are compared in +link:verification/legs/README.adoc[`verification/legs/README.adoc`]. That +comparison was written by Claude Code and is provisional until the owner reviews +it. Not `PWG-1`: no per-commit receipt captures each checker's observed result +yet. Not `+foundation-diverse`: no witness outside dependent type theory. +Per-claim evidence is in link:docs/EXPLAINME.adoc#proof-ledger[the Proof Ledger], +the machine record is link:verification/receipts/agda-pwg_praxis.deed[`verification/receipts/agda-pwg_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. diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index 16f80b2f..357191cb 100644 --- a/docs/EXPLAINME.adoc +++ b/docs/EXPLAINME.adoc @@ -100,13 +100,17 @@ only tested or still open. Tokens are the standard's closed vocabulary. the public result for finishing. This refutes the current rules, not every possible termination-sensitive typing discipline. -| Independent recheck in Rocq and in Lean (PROOF-POLICY §2) -| open -| — -| `PROOF-STATUS.adoc` "Proof Witness Grades, and the independent-witness legs", - `verification/receipts/agda-pwg_praxis.deed` -| No transport has been attempted and no hand re-proof exists, so every proven - row above is at `PWG-3` (PROOF-POLICY §8) and no higher. The template skeletons under +| Independent recheck of N-1, N-2, N-3, N-7, N-8 and N-9 in Rocq and in Lean + (PROOF-POLICY §2) +| proven +| `bash scripts/check-legs.sh` (Coq 8.18.0 and Lean 4.24.0, each pinned; no + library; every theorem printed with its axioms, and there are none) +| `verification/legs/rocq/SecretTypes.v`, `verification/legs/lean/`; + correspondence in `verification/legs/README.adoc` +| Re-proved by hand, not transported: Agda2Dedukti cannot run on the pinned + Agda. The statement comparison was written by Claude Code and is provisional + until the owner reviews it. With it, every proven row above is at `PWG-2ii` + (PROOF-POLICY §8). The template skeletons under `verification/proofs/{coq,lean4}` are *not* these legs and prove nothing here. | Strengthened termination-sensitive typing discipline diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index 84430526..cc69c05d 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -67,12 +67,14 @@ _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: -* *Recheck legs (`PWG-2i`/`PWG-2ii`).* `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 bounds the grade at - `PWG-3`, and that bound is recorded rather than glossed. +* *Recheck legs (`PWG-2ii`, met 2026-11-09).* `PROOF-POLICY.adoc` §2 asks for + every Agda theory proof to be rechecked in Rocq and in Lean. Both legs now + exist, re-proved by hand without a library or an axiom + (link:../verification/legs/README.adoc[`verification/legs/README.adoc`]), + and the receipt records them. The obligation that remains is review: the + statement comparison was written by Claude Code and is provisional until the + owner reviews it. `PWG-1` (a per-commit receipt of each checker's observed + result) is not met. * *Termination-sensitive noninterference.* `Noninterference.OutcomeVisibility.termination-sensitive-fails` refutes TSNI for the current typing rules when finishing versus non-finishing is public. diff --git a/scripts/check-legs.sh b/scripts/check-legs.sh new file mode 100755 index 00000000..b615d688 --- /dev/null +++ b/scripts/check-legs.sh @@ -0,0 +1,63 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-legs.sh — the Rocq and Lean recheck legs (PROOF-POLICY §2). +# +# Checks verification/legs/rocq (Coq, prelude only) and verification/legs/lean +# (Lean core only, no Mathlib, no `require`), then refuses any axiom: +# * every `Print Assumptions` line must read "Closed under the global context"; +# * every `#print axioms` line must read "does not depend on any axioms". +# A leg that does not check, or that rests on an axiom, fails this gate: a +# witness with axioms would have to be recorded PROVEN-WITH-AXIOMS and the +# receipt says it is not (PROOF-POLICY §8.4). +# +# Pins: COQ_VERSION and LEAN_VERSION below, fixed (no environment override); +# scripts/grade-receipt.sh reads them from here into the receipt. +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." +export LC_ALL="${LC_ALL:-C.UTF-8}" + +COQ_VERSION=8.18.0 +LEAN_VERSION=4.24.0 +fail=0 + +got="$(coqc --version | sed -n 's/^The Coq Proof Assistant, version \([0-9.]*\).*/\1/p')" +[ "$got" = "$COQ_VERSION" ] || { echo "ERROR: expected Coq $COQ_VERSION, found '${got:-none}'" >&2; exit 2; } +got="$(lean --version | sed -n 's/^Lean (version \([0-9.]*\),.*/\1/p')" +[ "$got" = "$LEAN_VERSION" ] || { echo "ERROR: expected Lean $LEAN_VERSION, found '${got:-none}'" >&2; exit 2; } + +# The Lean leg may not depend on anything: no `require` in the lakefile. +if grep -nE '^\s*\[\[require\]\]|^\s*require\b' verification/legs/lean/lakefile.toml; then + echo 'FAIL: the Lean leg declares a dependency (no Mathlib, no libraries)' >&2; fail=1 +fi +# The Rocq leg may not load the standard library. +if grep -nE '^\s*(From\s+\S+\s+)?Require\b' verification/legs/rocq/*.v; then + echo 'FAIL: the Rocq leg loads a library (prelude only)' >&2; fail=1 +fi +# No escape hatches in either leg. +if grep -nE '\b(sorry|admit|Admitted|Axiom|Parameter|axiom)\b' verification/legs/rocq/*.v verification/legs/lean/SecretTypes/*.lean; then + echo 'FAIL: an escape hatch in a leg' >&2; fail=1 +fi + +rocq_out="$(cd verification/legs/rocq && coqc -q SecretTypes.v 2>&1)" || { echo "$rocq_out" >&2; echo 'FAIL: the Rocq leg does not check' >&2; exit 1; } +n_closed="$(grep -c '^Closed under the global context$' <<< "$rocq_out" || true)" +n_print="$(grep -c '^Print Assumptions ' verification/legs/rocq/SecretTypes.v)" +if [ "$n_closed" != "$n_print" ] || grep -vq '^Closed under the global context$' <<< "$rocq_out"; then + echo "$rocq_out" >&2; echo "FAIL: the Rocq leg rests on an axiom ($n_closed of $n_print closed)" >&2; fail=1 +else + echo "PASS: Rocq leg (Coq $COQ_VERSION), $n_print theorems closed under the global context" +fi + +lean_out="$(cd verification/legs/lean && lake build >/dev/null && lake env lean Axioms.lean 2>&1)" \ + || { echo "$lean_out" >&2; echo 'FAIL: the Lean leg does not check' >&2; exit 1; } +n_free="$(grep -c 'does not depend on any axioms$' <<< "$lean_out" || true)" +n_ax="$(grep -c '^#print axioms ' verification/legs/lean/Axioms.lean)" +if [ "$n_free" != "$n_ax" ] || grep -vq 'does not depend on any axioms$' <<< "$lean_out"; then + echo "$lean_out" >&2; echo "FAIL: the Lean leg rests on an axiom ($n_free of $n_ax free)" >&2; fail=1 +else + echo "PASS: Lean leg (Lean $LEAN_VERSION, core only), $n_ax theorems depend on no axioms" +fi + +(( fail == 0 )) || exit 1 +echo 'PASS: both recheck legs' diff --git a/scripts/grade-receipt.sh b/scripts/grade-receipt.sh index 47d2ea93..d395b046 100755 --- a/scripts/grade-receipt.sh +++ b/scripts/grade-receipt.sh @@ -10,8 +10,11 @@ # # PWG-3 (§8.2): the Agda proof is PROVEN under the canonical §2.1 invocation # (agda --safe --without-K --cubical-compatible, here with stronger flags -# besides) and no Rocq or Lean recheck leg counts yet. PWG-3 is not a -# discharge (§8.4): every PWG-3 theorem still owes both legs. +# besides). PWG-2ii: PWG-3, and both the Rocq and the Lean leg count: +# kernel-checked (scripts/check-legs.sh, no axioms) and RECONCILED against +# the Agda statement (verification/legs/README.adoc). Not PWG-1: that needs +# a per-commit receipt of each checker's observed result, which this file +# is not (see below). # # 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 @@ -53,15 +56,15 @@ done # | argued | open. Legs are: transported | re-proved | unavailable. claims() { cat <<'ROWS' -N-1|proven|3|unavailable|unavailable -N-2|proven|3|unavailable|unavailable -N-3|proven|3|unavailable|unavailable +N-1|proven|2ii|re-proved|re-proved +N-2|proven|2ii|re-proved|re-proved +N-3|proven|2ii|re-proved|re-proved N-4|tested-only|n/a|n/a|n/a N-5|tested-only|n/a|n/a|n/a N-6|tested-only|n/a|n/a|n/a -N-7|proven|3|unavailable|unavailable -N-8|proven|3|unavailable|unavailable -N-9|proven|3|unavailable|unavailable +N-7|proven|2ii|re-proved|re-proved +N-8|proven|2ii|re-proved|re-proved +N-9|proven|2ii|re-proved|re-proved ROWS } @@ -105,6 +108,35 @@ check_claim_ids() { fi } +# The leg sources, in sorted order: everything a leg's kernel reads. +leg_sources() { + find verification/legs/rocq -name '*.v' | LC_ALL=C sort + find verification/legs/lean -name '*.lean' -not -path '*/.lake/*' | LC_ALL=C sort + printf '%s\n' verification/legs/lean/lakefile.toml verification/legs/lean/lean-toolchain +} + +# Print the (legs) block: per leg, the pinned checker, its invocation, the +# axiom check, and the sha256 of every input. The pins are read from +# scripts/check-legs.sh, the one place the gate takes them from. +emit_legs() { + local coq lean + coq="$(sed -n 's/^COQ_VERSION=\(.*\)$/\1/p' scripts/check-legs.sh)" + lean="$(sed -n 's/^LEAN_VERSION=\(.*\)$/\1/p' scripts/check-legs.sh)" + printf ' (legs\n :gate "bash scripts/check-legs.sh"\n :ci ".github/workflows/proofs.yml (job legs)"\n' + printf ' :correspondence "verification/legs/README.adoc"\n' + printf ' :route "re-proved"\n' + printf ' :route-reason "Agda2Dedukti is an Agda backend pinned to a fork (b026db1, GHC 8.10) and cannot run on Agda %s; no released Dedukti/Lambdapi exporter to Lean 4, and no pinned route to Rocq"\n' "$agda_version" + printf ' :state "RECONCILED"\n' + printf ' :review "statement comparison written by Claude Code; provisional until owner review (estate doctrine 4)"\n' + printf ' (leg :prover "rocq" :checker "coqc" :version "%s" :invocation "coqc -q SecretTypes.v (in verification/legs/rocq)" :libraries "none (no Require)" :axioms "none (Print Assumptions: Closed under the global context)")\n' "$coq" + printf ' (leg :prover "lean" :checker "lean" :version "%s" :invocation "lake build; lake env lean Axioms.lean (in verification/legs/lean)" :libraries "none (lakefile has no require; no Mathlib)" :axioms "none (#print axioms: does not depend on any axioms)")\n' "$lean" + printf ' (inputs\n' + while read -r p; do + printf ' (input :path "%s" :sha256 "%s")\n' "$p" "$(sha256sum "$p" | cut -d' ' -f1)" + done < <(leg_sources) + printf ' ))\n' +} + # Print the derived receipt, including claim rows, module hashes and fixtures. emit() { printf ';; SPDX-License-Identifier: CC-BY-SA-4.0\n' @@ -132,7 +164,8 @@ emit() { 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 ' ; PWGs apply to theory theorems (PROOF-POLICY section 8.1); refusal fixtures and leak witnesses are n/a.\n' - printf ' ; Independent Rocq and Lean legs remain unavailable: no transport or hand re-proof.\n' + printf ' ; Rocq and Lean legs: re-proved by hand (Agda2Dedukti cannot run on the pinned Agda), RECONCILED in verification/legs/README.adoc.\n' + emit_legs printf ' (claims\n' while IFS='|' read -r id token grade coq lean; do printf ' (claim :id "%s" :token "%s" :pwg "%s" :coq-leg "%s" :lean-leg "%s")\n' "$id" "$token" "$grade" "$coq" "$lean" @@ -148,7 +181,23 @@ emit() { printf ' )\n)\n' } +# A leg counted for a claim must have a row in the correspondence record, and a +# claim with a correspondence row must count its legs: the grade is derived +# from the §2.2 record, not typed beside it (PROOF-POLICY §8.4). +check_leg_records() { + local rec=verification/legs/README.adoc counted recorded + counted="$(claims | awk -F'|' '$4=="re-proved"||$5=="re-proved"{print $1}' | LC_ALL=C sort)" + recorded="$(grep -oE '^\| N-[0-9]+$' "$rec" 2>/dev/null | tr -d '| ' | LC_ALL=C sort -u || true)" + if [[ "$counted" != "$recorded" ]]; then + echo "ERROR: claims with a counted leg differ from the rows of $rec" >&2 + diff <(printf '%s\n' "$recorded") <(printf '%s\n' "$counted") \ + | grep -E '^[<>]' | sed "s|^<| only in $rec:|; s/^>/ only in grade-receipt.sh:/" >&2 + exit 1 + fi +} + check_claim_ids +check_leg_records case "$mode" in --write|"") diff --git a/verification/legs/README.adoc b/verification/legs/README.adoc new file mode 100644 index 00000000..dbff753f --- /dev/null +++ b/verification/legs/README.adoc @@ -0,0 +1,183 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += The Rocq and Lean recheck legs +:revdate: 2026-11-09 + +`standards/3-practice/PROOF-POLICY.adoc` §2 requires every Agda theory proof to +be rechecked in Rocq and in Lean. Transport through Dedukti comes first, and a +hand re-proof without Mathlib is the fallback. This directory holds both legs +for N-1, N-2, N-3, N-7, N-8 and N-9, and this file is their §2.2 +correspondence record. + +`bash scripts/check-legs.sh` checks both. CI runs it as the `legs` job of +`.github/workflows/proofs.yml`. + +== Route: `re-proved`, and why not `transported` + +Transport was tried first, as the policy orders, and is not available today: + +* Agda2Dedukti, the only Agda→Dedukti translator, builds against its own fork + of Agda (pinned commit `b026db1`, GHC 8.10, Stackage LTS 18.21). It is an Agda + backend, so it cannot run on Agda 2.6.4.3, the version the gate pins. +* Even with a Dedukti term, there is no released exporter from Dedukti or + Lambdapi to Lean 4, and no released route to Rocq that this repository + could pin and run in CI. + +So both legs are hand re-proofs of the Agda statements. Each leg was written +from the Agda module, statement by statement and proof by proof, and checked by +its own kernel. Nothing is translated mechanically, so the statements are +compared by hand below. + +== Versions and invocations + +[cols="1,2,3",options="header"] +|=== +| Leg | Version | Invocation + +| Rocq +| Coq 8.18.0 (Ubuntu 24.04 package `coq=8.18.0+dfsg-1build2`) +| `coqc -q SecretTypes.v`, in `rocq/`. + The file loads no library, not even with `Require`: only Coq's prelude. + +| Lean +| Lean 4.24.0 (release tarball, sha256 + `b14f5e5159219dd1a1956c3b806813319f5e94ccd5bdfd56f54520609a5bb5ec`) +| `lake build`, then `lake env lean Axioms.lean`, in `lean/`. `lakefile.toml` + declares no `require`, so there is no Mathlib and no other package: only + Lean core. +|=== + +`scripts/check-legs.sh` refuses the run if either version differs, if a +`require` or a `Require` appears, or if any source contains `sorry`, `admit`, +`Admitted`, `Axiom` or `Parameter`. + +== Assumptions: none + +Every theorem below is printed with its axioms (§8.4): + +* Rocq: `Print Assumptions` reports `Closed under the global context` for all + 11. The prelude's classical axioms are not loaded, so none can enter. +* Lean: `#print axioms` (in `lean/Axioms.lean`) reports + `does not depend on any axioms` for all 11. In particular, no `propext`, + `Quot.sound` or `Classical.choice`. + +`check-legs.sh` fails unless every one of the 22 lines says so. + +== Universe discipline + +Agda's `Set` is `Type` in both legs. The order `_⊑_`, an observer's `sees` and +the typing derivations are `Type`-valued in both, as in Agda, so a proof of +`x ⊑ y` is data in all three systems. A store agreement is an equation between +naturals: `Prop` in the legs and a set in Agda. The naturals have decidable +equality, so the two readings hold the same information. + +The Agda proof of N-7 splits on whether the observer sees a branch label, +under double negation, because agreement is stable (`¬¬ (s ≈ s') → s ≈ s'`). +Both legs make the same move (`agree_stable`, `by_cases_sees`), so neither leg +uses excluded middle. + +== Statement correspondence + +The legs keep the Agda names where the syntax allows. Lean writes `₁`/`₂` and +`'`, Rocq writes `1`/`2` and `0`/`1`. The statements are compared on the +following points; any other difference is notation. + +`exec`:: Agda defines `exec` with two helpers, `execIf` and `execWhile`. Both +legs define one function, `run prev`, structural in the command, with `prev` +the run at one less fuel (`none` at fuel zero), and set `exec 0 = run none` +and `exec (f + 1) = run (some (exec f))`. Clause by clause this is Agda's +definition: sequence and `ifz` keep the fuel, a loop at `f + 1` runs its body +and re-enters at `f`, and a loop at `0` is `nothing`. The legs prove the +clauses as lemmas (`exec_skip`, `exec_assign`, `exec_seq`, `exec_ifz`, +`exec_while_zero` in Lean, `exec_while_succ`), each by `rfl` or by cases. The +split exists so that Lean needs no well-founded recursion. Well-founded +recursion would bring in `propext`. + +`Maybe`:: `Option` in Lean and `option` in Rocq, with `nothing`/`just` as +`none`/`some`. + +The record:: Agda has one record, `Lattice` (`SecretTypes.Lattice.Record`), with +the carrier, `_⊑_`, `_⊔_`, `⊥ₗ` and exactly three laws: `⊑-trans`, +`⊔-upper₁` and `⊔-upper₂`. The legs split it into `Signature`, with the +operations and no laws, and `Lattice`, which extends it with the same three +laws. `TINI` and the typing rules are stated over `Signature`. That is what +the Agda `Statement` and `Typing.Generic` modules are parameterised by, and the +N-8 countermodels need it to state `TINI` where a law fails. The generic proof +(`tini`) takes a `Lattice`. The laws are the same three, so neither leg is +weaker or stronger than Agda here. + +`Observer`:: `sees : Carrier → Type` and down-closure, as in Agda. +`principal L o` sees `· ⊑ o`, and its down-closure is `le_trans`, as in Agda. + +`Vars`:: a type with decidable equality. In Lean, `DecidableEq Var`; in +Rocq, `{x = y} + {x <> y}`. Agda uses `Dec`. All three are the same choice +data. + +== Claim by claim + +The state of every row is `RECONCILED` (§2.2): AGDA-VERIFIED by +`scripts/check.sh`, COQ-CHECKED and LEAN-CHECKED by `scripts/check-legs.sh`, +and the statements compared above with no bridge pending. + +[cols="1,2,2,2",options="header"] +|=== +| Claim | Agda | Lean | Rocq + +| N-1 +| `Noninterference.tini` +| `SecretTypes.Two.tini_two` +| `Two.tini_two` + +| N-2 +| `Noninterference.Generic.eval-low`; `Noninterference.eval-low` +| `SecretTypes.eval_low`; `SecretTypes.Two.eval_low_two` +| `eval_low`; `Two.eval_low_two` + +| N-3 +| `Noninterference.Generic.confine`; `Noninterference.confine` +| `SecretTypes.confine` (with `confine_loop`); `SecretTypes.Two.confine_two` +| `confine` (with `confine_loop`); `Two.confine_two` + +| N-7 +| `Noninterference.Generic.tini : (V : Observer 𝓛) → TINI (Observer.sees V)` +| `SecretTypes.tini` +| `tini : TINI L label (sees O)` + +| N-8 +| `Countermodels.NoUpper₁.refutes`, `NoUpper₂.refutes`, + `NoDownClosure.refutes`, `NoTrans.refutes`, each `¬ TINI _` +| `SecretTypes.Countermodels.NoUpper₁.refutes`, `NoUpper₂.refutes`, + `NoDownClosure.refutes`, `NoTrans.refutes`, each `TINI … → False` +| `Countermodels.NoUpper1.refutes`, `NoUpper2.refutes`, + `NoDownClosure.refutes`, `NoTrans.refutes` + +| N-9 +| `Noninterference.OutcomeVisibility.termination-sensitive-fails : ¬ TSNI` +| `SecretTypes.Two.termination_sensitive_fails : TSNI → False` +| `Two.termination_sensitive_fails : TSNI -> False` +|=== + +Each N-8 countermodel is the Agda one: the same carrier, the same failing law, +the same typed program and the same two stores. For `NoTrans`, the +five-point order and its `join` are Agda's, case by case. N-9 uses the same +`secret-loop`, the same stores `s₀ = (0, 0)` and `s₁ = (0, 1)`, and the same +outcome at fuel 3. + +N-4, N-5 and N-6 have no leg. They are checked demonstrations, not theorems +(§8.1). + +== What the legs do not establish + +* They are re-proofs, not transports. The match between each leg statement + and its Agda statement rests on the comparison above. Claude Code wrote it, + and it is provisional until the owner reviews it (estate doctrine 4). No + tool checks it. +* `foundation_diverse` (§8.3) stays false. Lean's and Rocq's kernels are + independent of Agda's, but all three are dependent type theories. The tag + needs a witness in a different foundation, such as Isabelle/HOL, and none + exists. +* The grade is `PWG-2ii`, not `PWG-1`. `PWG-1` needs a receipt per witness, + per commit, recording the observed result of a pinned checker run on that + commit (§8.2). The receipt here records the legs' versions, invocations and + input digests; the CI log of the `legs` job is the observed result, and it + is not yet captured as a receipt. diff --git a/verification/legs/lean/.gitignore b/verification/legs/lean/.gitignore new file mode 100644 index 00000000..6009e03c --- /dev/null +++ b/verification/legs/lean/.gitignore @@ -0,0 +1,4 @@ +.lake/ +# Written by `lake build`; with no `require` it lists no package, and it is not +# JCS-serialised (estate JSON policy), so it is not committed. +lake-manifest.json diff --git a/verification/legs/lean/Axioms.lean b/verification/legs/lean/Axioms.lean new file mode 100644 index 00000000..34b07abc --- /dev/null +++ b/verification/legs/lean/Axioms.lean @@ -0,0 +1,15 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Prints the axioms every Lean-leg theorem rests on (PROOF-POLICY §8.4). +-- scripts/check-legs.sh requires each line to read "does not depend on any axioms". +import SecretTypes +#print axioms SecretTypes.eval_low +#print axioms SecretTypes.confine +#print axioms SecretTypes.tini +#print axioms SecretTypes.Two.eval_low_two +#print axioms SecretTypes.Two.confine_two +#print axioms SecretTypes.Two.tini_two +#print axioms SecretTypes.Two.termination_sensitive_fails +#print axioms SecretTypes.Countermodels.NoUpper₁.refutes +#print axioms SecretTypes.Countermodels.NoUpper₂.refutes +#print axioms SecretTypes.Countermodels.NoDownClosure.refutes +#print axioms SecretTypes.Countermodels.NoTrans.refutes diff --git a/verification/legs/lean/SecretTypes.lean b/verification/legs/lean/SecretTypes.lean new file mode 100644 index 00000000..3fba1f32 --- /dev/null +++ b/verification/legs/lean/SecretTypes.lean @@ -0,0 +1,4 @@ +-- SPDX-License-Identifier: MPL-2.0 +import SecretTypes.Generic +import SecretTypes.Two +import SecretTypes.Countermodels diff --git a/verification/legs/lean/SecretTypes/Countermodels.lean b/verification/legs/lean/SecretTypes/Countermodels.lean new file mode 100644 index 00000000..3cf88848 --- /dev/null +++ b/verification/legs/lean/SecretTypes/Countermodels.lean @@ -0,0 +1,216 @@ +/- +SPDX-License-Identifier: MPL-2.0 +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +Lean leg (PROOF-POLICY §2, route `re-proved`) of secret-types N-8: each law +generic TINI uses is necessary. Mirrors src/SecretTypes/Countermodels.agda +module by module: drop one law, keep the typing rules, and a well-typed +program leaks, so `TINI` is refuted at that signature. Lean core only, no +axioms. +-/ +import SecretTypes.Two + +namespace SecretTypes.Countermodels +open SecretTypes SecretTypes.Two Label Var + +/-- `std`: `lo` public, `hi` secret. -/ +def std : two.Var → Label + | lo => L + | hi => H + +/-- The two-point signature with a given join. -/ +def withJoin (j : Label → Label → Label) : Signature where + Carrier := Label + le := le + join := j + bot := L + +/-- Seen by the observer at `L`: exactly the labels below `L`. -/ +def belowL : Label → Type := fun x => le x L + +theorem agree_s₀_s₁ (S : Signature) (hS : S.Carrier = Label) (lab' : two.Var → S.Carrier) + (sees : S.Carrier → Type) (hhi : sees (lab' hi) → False) : + Agree S lab' sees s₀ s₁ := fun + | lo, _ => rfl + | hi, v => (hhi v).elim + +/-! `NoUpper₁`: the join `x ⊔ʳ y = y` keeps `⊔-upper₂` and drops `⊔-upper₁`. -/ +namespace NoUpper₁ + +def joinR : Label → Label → Label := fun _ y => y + +def S : Signature := withJoin joinR + +def upper₂ : ∀ x y : Label, le y (joinR x y) + | _, L => () + | _, H => () + +theorem not_upper₁ : (∀ x y : Label, le x (joinR x y)) → False := + fun h => nomatch (h H L : Empty) + +/-- `implicit = ifz (var hi) (lo ≔ lit 0) (lo ≔ lit 1)`, typed at `L`. -/ +def implicitFlow : Cmd two := .ifz (.var hi) (.assign lo (.lit 0)) (.assign lo (.lit 1)) + +def typed : Typed S std L implicitFlow := .ifz (.assign ()) (.assign ()) + +theorem refutes : TINI S std belowL → False := fun tini => + nomatch (tini 1 1 typed (agree_s₀_s₁ S rfl std belowL (fun v => nomatch (v : Empty))) + rfl rfl lo () : 0 = 1) + +end NoUpper₁ + +/-! `NoUpper₂`: the join `x ⊔ˡ y = x` keeps `⊔-upper₁` and drops `⊔-upper₂`. -/ +namespace NoUpper₂ + +def joinL : Label → Label → Label := fun x _ => x + +def S : Signature := withJoin joinL + +def upper₁ : ∀ x y : Label, le x (joinL x y) + | L, _ => () + | H, _ => () + +theorem not_upper₂ : (∀ x y : Label, le y (joinL x y)) → False := + fun h => nomatch (h L H : Empty) + +/-- `explicit = lo ≔ var hi`, typed at `L`. -/ +def explicitFlow : Cmd two := .assign lo (.var hi) + +def typed : Typed S std L explicitFlow := .assign () + +theorem refutes : TINI S std belowL → False := fun tini => + nomatch (tini 1 1 typed (agree_s₀_s₁ S rfl std belowL (fun v => nomatch (v : Empty))) + rfl rfl lo () : 0 = 1) + +end NoUpper₂ + +/-! `NoDownClosure`: the observer that sees exactly `H` is not down-closed. -/ +namespace NoDownClosure + +def sees : Label → Type := fun x => PLift (x = H) + +theorem not_down_closed : (∀ {x y : Label}, le x y → sees y → sees x) → False := + fun h => nomatch (h (x := L) (y := H) () ⟨rfl⟩).down + +def S : Signature := withJoin join + +/-- `up = hi ≔ var lo`, typed at `L`. -/ +def up : Cmd two := .assign hi (.var lo) + +def typed : Typed S std L up := .assign () + +def t₀ : Store two := pair 0 0 +def t₁ : Store two := pair 1 0 + +theorem agree : Agree S std sees t₀ t₁ := fun + | lo, v => nomatch v.down + | hi, _ => rfl + +theorem refutes : TINI S std sees → False := fun tini => + nomatch (tini 1 1 typed agree rfl rfl hi ⟨rfl⟩ : 0 = 1) + +end NoDownClosure + +/-! `NoTrans`: without `⊑-trans`, "flows to `o`" can fail to be down-closed, +and TINI fails for that principal observer. -/ +namespace NoTrans + +inductive P where + | B | H' | M | L' | T + +open P + +inductive Le : P → P → Type where + | refl {x} : Le x x + | bot {x} : Le B x + | top {x} : Le x T + | HM : Le H' M + | ML : Le M L' + +def join : P → P → P + | B, y => y + | T, _ => T + | H', B => H' + | H', H' => H' + | H', M => M + | H', L' => T + | H', T => T + | M, B => M + | M, H' => M + | M, M => M + | M, L' => L' + | M, T => T + | L', B => L' + | L', H' => T + | L', M => L' + | L', L' => L' + | L', T => T + +def upper₁ : ∀ x y : P, Le x (join x y) + | B, _ => .bot + | T, _ => .refl + | H', B => .refl + | H', H' => .refl + | H', M => .HM + | H', L' => .top + | H', T => .top + | M, B => .refl + | M, H' => .refl + | M, M => .refl + | M, L' => .ML + | M, T => .top + | L', B => .refl + | L', H' => .top + | L', M => .refl + | L', L' => .refl + | L', T => .top + +def upper₂ : ∀ x y : P, Le y (join x y) + | B, _ => .refl + | T, _ => .top + | H', B => .bot + | H', H' => .refl + | H', M => .refl + | H', L' => .top + | H', T => .refl + | M, B => .bot + | M, H' => .HM + | M, M => .refl + | M, L' => .refl + | M, T => .refl + | L', B => .bot + | L', H' => .top + | L', M => .ML + | L', L' => .refl + | L', T => .refl + +theorem not_trans : (∀ {x y z : P}, Le x y → Le y z → Le x z) → False := + fun t => nomatch (t Le.HM Le.ML : Le H' L') + +def S : Signature where + Carrier := P + le := Le + join := join + bot := B + +def label : two.Var → P + | lo => M + | hi => H' + +/-- `explicit = lo ≔ var hi`, typed at `B` (needs only `H′ ≤ M`). -/ +def explicitFlow : Cmd two := .assign lo (.var hi) + +def typed : Typed S label B explicitFlow := .assign .HM + +def belowL' : P → Type := fun x => Le x L' + +theorem agree : Agree S label belowL' s₀ s₁ := fun + | lo, _ => rfl + | hi, v => nomatch (v : Le H' L') + +theorem refutes : TINI S label belowL' → False := fun tini => + nomatch (tini 1 1 typed agree rfl rfl lo Le.ML : 0 = 1) + +end NoTrans + +end SecretTypes.Countermodels diff --git a/verification/legs/lean/SecretTypes/Generic.lean b/verification/legs/lean/SecretTypes/Generic.lean new file mode 100644 index 00000000..d2e078f1 --- /dev/null +++ b/verification/legs/lean/SecretTypes/Generic.lean @@ -0,0 +1,411 @@ +/- +SPDX-License-Identifier: MPL-2.0 +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +Lean leg (PROOF-POLICY §2, route `re-proved`) of secret-types N-2, N-3 and N-7: +termination-insensitive noninterference over any lattice record and any +down-closed observer. The statements mirror, line for line: + src/SecretTypes/Vars.agda, Lang.agda, Lattice/Record.agda, + Typing/Generic.agda, Noninterference/Statement.agda, Noninterference/Generic.agda. +Lean core only: no Mathlib, no Std, no classical axioms +(see the `#print axioms` lines at the end of this file). + +Universe discipline: Agda's `Set` is Lean's `Type`. The order, an +observer's `sees` and the typing derivations are `Type`-valued here, as in +Agda, so a proof may not use proof irrelevance that the Agda statement does +not grant. Equality of naturals is `Prop` in Lean and a set in Agda; +naturals have decidable equality, so the two readings coincide. +-/ +namespace SecretTypes + +/-- `SecretTypes.Vars`: variables with decidable equality. -/ +structure Vars where + Var : Type + deq : DecidableEq Var + +/-- What `SecretTypes.Noninterference.Statement` and `Typing.Generic` are +parameterised by: a carrier, an order, a join and the label of a literal, with +no laws. The countermodels (N-8) instantiate the statement at signatures +that lack a law, so the statement cannot ask for one. -/ +structure Signature where + Carrier : Type + le : Carrier → Carrier → Type + join : Carrier → Carrier → Carrier + bot : Carrier + +/-- `SecretTypes.Lattice.Record.Lattice`: a signature with the three laws +generic TINI uses (the certified census, N-6). -/ +structure Lattice extends Signature where + le_trans : ∀ {x y z : Carrier}, le x y → le y z → le x z + upper₁ : ∀ x y : Carrier, le x (join x y) + upper₂ : ∀ x y : Carrier, le y (join x y) + +/-- `SecretTypes.Lattice.Record.Observer`: a down-closed set of labels. -/ +structure Observer (L : Lattice) where + sees : L.Carrier → Type + down : ∀ {x y : L.Carrier}, L.le x y → sees y → sees x + +/-- `principal`: the observer at level `o` sees exactly the labels below it. -/ +def principal (L : Lattice) (o : L.Carrier) : Observer L where + sees x := L.le x o + down h v := L.le_trans h v + +section Lang +variable (V : Vars) + +/-- `Store = Var → Nat`. -/ +abbrev Store := V.Var → Nat + +inductive Expr where + | lit : Nat → Expr + | var : V.Var → Expr + | plus : Expr → Expr → Expr + +inductive Cmd where + | skip : Cmd + | assign : V.Var → Expr V → Cmd + | seq : Cmd → Cmd → Cmd + | ifz : Expr V → Cmd → Cmd → Cmd + | «while» : Expr V → Cmd → Cmd + +variable {V} + +def eval (s : Store V) : Expr V → Nat + | .lit n => n + | .var x => s x + | .plus a b => eval s a + eval s b + +/-- `update x n s y = select (x ≟ᵥ y) n (s y)`. -/ +def update (x : V.Var) (n : Nat) (s : Store V) : Store V := fun y => + match V.deq x y with + | .isTrue _ => n + | .isFalse _ => s y + +/-- `bind` of `SecretTypes.Prelude`. -/ +def bind {A : Type} : Option A → (A → Option A) → Option A + | none, _ => none + | some a, f => f a + +/-- One step of fuel: run a command, using `prev` (the run at one less fuel) +to re-enter a loop. `none` is fuel zero, where a loop does not finish. +Structural in the command, so `exec` below is structural in both fuel and +command and its equations hold by `rfl` (no well-founded recursion, hence no +`propext` or `funext` in the proofs). -/ +def run (prev : Option (Cmd V → Store V → Option (Store V))) : + Cmd V → Store V → Option (Store V) + | .skip, s => some s + | .assign x e, s => some (update x (eval s e) s) + | .seq c₁ c₂, s => bind (run prev c₁ s) (run prev c₂) + | .ifz e c₁ c₂, s => + match eval s e with + | 0 => run prev c₁ s + | _ + 1 => run prev c₂ s + | .«while» e c, s => + match prev with + | none => none + | some p => + match eval s e with + | 0 => bind (p c s) (p (.«while» e c)) + | _ + 1 => some s + +/-- `exec` of `SecretTypes.Lang`: `exec fuel c s` is `some t` if `c` finishes +within `fuel`, else `none`. Equal to Agda's `exec`, `execIf` and +`execWhile` clause by clause: sequence and `ifz` keep the fuel, a loop at +`fuel + 1` runs its body and re-enters at `fuel`, a loop at `0` is `none`. -/ +def exec : Nat → Cmd V → Store V → Option (Store V) + | 0 => run none + | f + 1 => run (some (exec f)) + +end Lang + +section Typing +variable {V : Vars} (L : Signature) (label : V.Var → L.Carrier) + +/-- `lab` of `SecretTypes.Typing.Generic`. -/ +def lab : Expr V → L.Carrier + | .lit _ => L.bot + | .var x => label x + | .plus a b => L.join (lab a) (lab b) + +/-- `_⊢_` of `SecretTypes.Typing.Generic`: Volpano–Smith typing with a +program-counter label. -/ +inductive Typed : L.Carrier → Cmd V → Type where + | skip {pc} : Typed pc .skip + | assign {pc x e} : L.le (L.join pc (lab L label e)) (label x) → Typed pc (.assign x e) + | seq {pc c₁ c₂} : Typed pc c₁ → Typed pc c₂ → Typed pc (.seq c₁ c₂) + | ifz {pc e c₁ c₂} : Typed (L.join pc (lab L label e)) c₁ → + Typed (L.join pc (lab L label e)) c₂ → Typed pc (.ifz e c₁ c₂) + | «while» {pc e c} : Typed (L.join pc (lab L label e)) c → Typed pc (.«while» e c) + +/-- `_≈[_]_` of `SecretTypes.Noninterference.Statement`. -/ +def Agree (sees : L.Carrier → Type) (s s' : Store V) : Prop := + ∀ x, sees (label x) → s x = s' x + +/-- `TINI` of `SecretTypes.Noninterference.Statement`. -/ +def TINI (sees : L.Carrier → Type) : Prop := + ∀ {pc : L.Carrier} {c : Cmd V} (fuel fuel' : Nat) {s s' t t' : Store V}, + Typed L label pc c → Agree L label sees s s' → + exec fuel c s = some t → exec fuel' c s' = some t' → Agree L label sees t t' + +end Typing + +section Proof +variable {V : Vars} {L : Lattice} {label : V.Var → L.Carrier} (O : Observer L) + +/-! Unfolding equations for `exec`, one per command form. -/ + +/-- The branch an `ifz` takes on guard value `n`. -/ +def branch (n : Nat) (c₁ c₂ : Cmd V) : Cmd V := + match n with + | 0 => c₁ + | _ + 1 => c₂ + +theorem exec_skip (f : Nat) (s : Store V) : exec f .skip s = some s := by + cases f <;> rfl + +theorem exec_assign (f : Nat) (x : V.Var) (e : Expr V) (s : Store V) : + exec f (.assign x e) s = some (update x (eval s e) s) := by + cases f <;> rfl + +theorem exec_seq (f : Nat) (c₁ c₂ : Cmd V) (s : Store V) : + exec f (.seq c₁ c₂) s = bind (exec f c₁ s) (exec f c₂) := by + cases f <;> rfl + +theorem exec_ifz (f : Nat) (e : Expr V) (c₁ c₂ : Cmd V) (s : Store V) : + exec f (.ifz e c₁ c₂) s = exec f (branch (eval s e) c₁ c₂) s := by + cases f <;> (show run _ _ _ = run _ _ _; simp only [run]; cases eval s e <;> rfl) + +theorem exec_while_zero (e : Expr V) (c : Cmd V) (s : Store V) : + exec 0 (.«while» e c) s = none := rfl + +theorem exec_while_succ (f : Nat) (e : Expr V) (c : Cmd V) (s : Store V) : + exec (f + 1) (.«while» e c) s = + (match eval s e with + | 0 => bind (exec f c s) (exec f (.«while» e c)) + | _ + 1 => some s) := rfl + +theorem bind_some {A : Type} {m : Option A} {f : A → Option A} {t : A} : + bind m f = some t → ∃ a, m = some a ∧ f a = some t := by + cases m with + | none => intro h; cases h + | some a => intro h; exact ⟨a, rfl, h⟩ + +/-- A branch typed under a counter is typed under it, whichever is taken. -/ +def branch_typed {pc : L.Carrier} (n : Nat) {c₁ c₂ : Cmd V} + (d₁ : Typed L.toSignature label pc c₁) (d₂ : Typed L.toSignature label pc c₂) : + Typed L.toSignature label pc (branch n c₁ c₂) := + match n with + | 0 => d₁ + | _ + 1 => d₂ + +/-- `unseen-⊔`. -/ +theorem unseen_join {pc : L.Carrier} (y : L.Carrier) (np : O.sees pc → False) : + O.sees (L.join pc y) → False := + fun v => np (O.down (L.upper₁ pc y) v) + +/-- N-2, `eval-low`: an expression whose label the observer sees reads the +same in agreeing stores. -/ +theorem eval_low : ∀ (e : Expr V) {s s' : Store V}, O.sees (lab L.toSignature label e) → + Agree L.toSignature label O.sees s s' → eval s e = eval s' e + | .lit _, _, _, _, _ => rfl + | .var x, _, _, v, eq => eq x v + | .plus a b, _, _, v, eq => by + show eval _ a + eval _ b = eval _ a + eval _ b + rw [eval_low a (O.down (L.upper₁ _ _) v) eq, eval_low b (O.down (L.upper₂ _ _) v) eq] + +theorem agree_refl {s : Store V} : Agree L.toSignature label O.sees s s := fun _ _ => rfl + +theorem agree_symm {s s' : Store V} (h : Agree L.toSignature label O.sees s s') : + Agree L.toSignature label O.sees s' s := fun x v => (h x v).symm + +theorem agree_trans {s s' s'' : Store V} (h : Agree L.toSignature label O.sees s s') + (k : Agree L.toSignature label O.sees s' s'') : Agree L.toSignature label O.sees s s'' := + fun x v => (h x v).trans (k x v) + +/-- `confine-assign`: an assignment allowed under an unseen counter leaves +every seen variable alone. -/ +theorem confine_assign {pc : L.Carrier} (x : V.Var) (e : Expr V) (n : Nat) (s : Store V) + (np : O.sees pc → False) (ok : L.le (L.join pc (lab L.toSignature label e)) (label x)) : + Agree L.toSignature label O.sees (update x n s) s := by + intro y v + show (match V.deq x y with | .isTrue _ => n | .isFalse _ => s y) = s y + cases V.deq x y with + | isTrue hxy => subst hxy; exact (unseen_join O (lab L.toSignature label e) np (O.down ok v)).elim + | isFalse _ => rfl + +/-- N-3, `confine`: under a program counter the observer cannot see, a +finishing run changes nothing the observer sees. -/ +theorem confine : ∀ (fuel : Nat) {pc : L.Carrier} {c : Cmd V} {s t : Store V}, + (O.sees pc → False) → Typed L.toSignature label pc c → exec fuel c s = some t → + Agree L.toSignature label O.sees t s := by + intro fuel + induction fuel with + | zero => + intro pc c s t np d + induction d generalizing s t with + | skip => intro h; rw [exec_skip] at h; cases h; exact agree_refl O + | @assign pc x e ok => + intro h; rw [exec_assign] at h; cases h; exact confine_assign O x e _ s np ok + | seq d₁ d₂ ih₁ ih₂ => + intro h; rw [exec_seq] at h + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + exact agree_trans O (ih₂ np h₂) (ih₁ np h₁) + | @ifz pc e c₁ c₂ d₁ d₂ ih₁ ih₂ => + intro h; rw [exec_ifz] at h + have np' := unseen_join O (lab L.toSignature label e) np + cases hv : eval s e with + | zero => rw [hv] at h; exact ih₁ np' h + | succ _ => rw [hv] at h; exact ih₂ np' h + | «while» d ih => intro h; rw [exec_while_zero] at h; cases h + | succ f ihf => + intro pc c s t np d + induction d generalizing s t with + | skip => intro h; rw [exec_skip] at h; cases h; exact agree_refl O + | @assign pc x e ok => + intro h; rw [exec_assign] at h; cases h; exact confine_assign O x e _ s np ok + | seq d₁ d₂ ih₁ ih₂ => + intro h; rw [exec_seq] at h + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + exact agree_trans O (ih₂ np h₂) (ih₁ np h₁) + | @ifz pc e c₁ c₂ d₁ d₂ ih₁ ih₂ => + intro h; rw [exec_ifz] at h + have np' := unseen_join O (lab L.toSignature label e) np + cases hv : eval s e with + | zero => rw [hv] at h; exact ih₁ np' h + | succ _ => rw [hv] at h; exact ih₂ np' h + | @«while» pc e c d ih => + intro h; rw [exec_while_succ] at h + have np' := unseen_join O (lab L.toSignature label e) np + cases hv : eval s e with + | zero => + rw [hv] at h + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + exact agree_trans O (ihf np (Typed.«while» d) h₂) (ihf np' d h₁) + | succ _ => rw [hv] at h; cases h; exact agree_refl O + +/-- `confineL`: re-entering a loop whose body is typed under an unseen +counter changes nothing the observer sees. The loop is not re-typed: `ℓ` is +the body's counter, which need not type the loop itself. -/ +theorem confine_loop : ∀ (fuel : Nat) {ℓ : L.Carrier} {e : Expr V} {c : Cmd V} + {s t : Store V}, (O.sees ℓ → False) → Typed L.toSignature label ℓ c → + exec fuel (.«while» e c) s = some t → Agree L.toSignature label O.sees t s := by + intro fuel + induction fuel with + | zero => intro ℓ e c s t _ _ h; rw [exec_while_zero] at h; cases h + | succ f ihf => + intro ℓ e c s t np d h + rw [exec_while_succ] at h + cases hv : eval s e with + | zero => + rw [hv] at h + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + exact agree_trans O (ihf np d h₂) (confine O f np d h₁) + | succ _ => rw [hv] at h; cases h; exact agree_refl O + +/-- Agreement is a family of equations between naturals, hence stable under +double negation: what lets the proof split on whether the observer sees a +branch label without deciding it (as the Agda proof does). -/ +theorem agree_stable {s s' : Store V} + (h : (Agree L.toSignature label O.sees s s' → False) → False) : Agree L.toSignature label O.sees s s' := + fun x v => Decidable.byContradiction fun ne => h fun a => ne (a x v) + +/-- `¬¬-dec`: excluded middle under double negation, for any type. -/ +theorem nn_em (P : Type) (k : PSum P (P → False) → False) : False := + k (.inr fun p => k (.inl p)) + +/-- Either the observer sees label `j` or it does not, under double +negation: the shape the `ifz` and `while` cases use. -/ +theorem by_cases_sees {s s' : Store V} (j : L.Carrier) + (yes : O.sees j → Agree L.toSignature label O.sees s s') + (no : (O.sees j → False) → Agree L.toSignature label O.sees s s') : + Agree L.toSignature label O.sees s s' := + agree_stable O fun bad => nn_em (O.sees j) fun + | .inl v => bad (yes v) + | .inr nv => bad (no nv) + +/-- N-7, `tini`: termination-insensitive noninterference for every +down-closed observer of every lattice record. -/ +theorem tini : TINI L.toSignature label O.sees := by + intro pc c fuel + induction fuel generalizing pc c with + | zero => + intro fuel' s s' t t' d + induction d generalizing s s' t t' fuel' with + | skip => + intro eq h h'; rw [exec_skip] at h h'; cases h; cases h'; exact eq + | @assign pc x e ok => + intro eq h h'; rw [exec_assign] at h h'; cases h; cases h' + intro y v + show (match V.deq x y with | .isTrue _ => eval s e | .isFalse _ => s y) = + (match V.deq x y with | .isTrue _ => eval s' e | .isFalse _ => s' y) + cases V.deq x y with + | isTrue hxy => subst hxy; exact eval_low O e (O.down (L.upper₂ _ _) (O.down ok v)) eq + | isFalse _ => exact eq y v + | seq d₁ d₂ ih₁ ih₂ => + intro eq h h'; rw [exec_seq] at h h' + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + obtain ⟨s₁', h₁', h₂'⟩ := bind_some h' + exact ih₂ fuel' (ih₁ fuel' eq h₁ h₁') h₂ h₂' + | @ifz pc e c₁ c₂ d₁ d₂ ih₁ ih₂ => + intro eq h h'; rw [exec_ifz] at h h' + refine by_cases_sees O (L.join pc (lab L.toSignature label e)) (fun v => ?_) (fun nv => ?_) + · have ge := eval_low O e (O.down (L.upper₂ _ _) v) eq + rw [← ge] at h' + cases hv : eval s e with + | zero => rw [hv] at h h'; exact ih₁ fuel' eq h h' + | succ _ => rw [hv] at h h'; exact ih₂ fuel' eq h h' + · exact agree_trans O + (confine O _ nv (branch_typed _ d₁ d₂) h) + (agree_trans O eq (agree_symm O (confine O _ nv (branch_typed _ d₁ d₂) h'))) + | «while» d ih => intro eq h; rw [exec_while_zero] at h; cases h + | succ f ihf => + intro fuel' s s' t t' d + induction d generalizing s s' t t' fuel' with + | skip => + intro eq h h'; rw [exec_skip] at h h'; cases h; cases h'; exact eq + | @assign pc x e ok => + intro eq h h'; rw [exec_assign] at h h'; cases h; cases h' + intro y v + show (match V.deq x y with | .isTrue _ => eval s e | .isFalse _ => s y) = + (match V.deq x y with | .isTrue _ => eval s' e | .isFalse _ => s' y) + cases V.deq x y with + | isTrue hxy => subst hxy; exact eval_low O e (O.down (L.upper₂ _ _) (O.down ok v)) eq + | isFalse _ => exact eq y v + | seq d₁ d₂ ih₁ ih₂ => + intro eq h h'; rw [exec_seq] at h h' + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + obtain ⟨s₁', h₁', h₂'⟩ := bind_some h' + exact ih₂ fuel' (ih₁ fuel' eq h₁ h₁') h₂ h₂' + | @ifz pc e c₁ c₂ d₁ d₂ ih₁ ih₂ => + intro eq h h'; rw [exec_ifz] at h h' + refine by_cases_sees O (L.join pc (lab L.toSignature label e)) (fun v => ?_) (fun nv => ?_) + · have ge := eval_low O e (O.down (L.upper₂ _ _) v) eq + rw [← ge] at h' + cases hv : eval s e with + | zero => rw [hv] at h h'; exact ih₁ fuel' eq h h' + | succ _ => rw [hv] at h h'; exact ih₂ fuel' eq h h' + · exact agree_trans O + (confine O _ nv (branch_typed _ d₁ d₂) h) + (agree_trans O eq (agree_symm O (confine O _ nv (branch_typed _ d₁ d₂) h'))) + | @«while» pc e c d ih => + intro eq h h' + cases fuel' with + | zero => rw [exec_while_zero] at h'; cases h' + | succ f' => + rw [exec_while_succ] at h h' + refine by_cases_sees O (L.join pc (lab L.toSignature label e)) (fun v => ?_) (fun nv => ?_) + · have ge := eval_low O e (O.down (L.upper₂ _ _) v) eq + rw [← ge] at h' + cases hv : eval s e with + | zero => + rw [hv] at h h' + obtain ⟨s₁, h₁, h₂⟩ := bind_some h + obtain ⟨s₁', h₁', h₂'⟩ := bind_some h' + exact ihf f' (Typed.«while» d) (ihf f' d eq h₁ h₁') h₂ h₂' + | succ _ => rw [hv] at h h'; cases h; cases h'; exact eq + · rw [← exec_while_succ] at h h' + exact agree_trans O (confine_loop O _ nv d h) + (agree_trans O eq (agree_symm O (confine_loop O _ nv d h'))) + +end Proof +end SecretTypes diff --git a/verification/legs/lean/SecretTypes/Two.lean b/verification/legs/lean/SecretTypes/Two.lean new file mode 100644 index 00000000..ef8c410d --- /dev/null +++ b/verification/legs/lean/SecretTypes/Two.lean @@ -0,0 +1,158 @@ +/- +SPDX-License-Identifier: MPL-2.0 +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +Lean leg (PROOF-POLICY §2, route `re-proved`) of secret-types N-1, N-2, N-3 +at the two-point lattice and N-9. Mirrors src/SecretTypes/Lattice.agda, +Lang/Two.agda, Typing.agda, Noninterference.agda, Witness.agda and +Noninterference/OutcomeVisibility.agda. Lean core only, no axioms. +-/ +import SecretTypes.Generic + +namespace SecretTypes.Two +open SecretTypes + +/-- `Label` of `SecretTypes.Lattice`: `L` public, `H` secret. -/ +inductive Label where + | L + | H +open Label + +/-- `_⊑_` of `SecretTypes.Lattice`: a computed predicate, as there. -/ +def le : Label → Label → Type + | L, _ => Unit + | H, L => Empty + | H, H => Unit + +def join : Label → Label → Label + | L, y => y + | H, _ => H + +def le_trans : ∀ {x y z : Label}, le x y → le y z → le x z + | L, _, _, _, _ => () + | H, H, H, _, _ => () + | H, H, L, _, k => k + | H, L, _, h, _ => nomatch h + +def upper₁ : ∀ x y : Label, le x (join x y) + | L, _ => () + | H, _ => () + +def upper₂ : ∀ x y : Label, le y (join x y) + | L, L => () + | L, H => () + | H, L => () + | H, H => () + +/-- `two-point` of `SecretTypes.Lattice`. -/ +def twoPoint : Lattice where + Carrier := Label + le := le + join := join + bot := L + le_trans := le_trans + upper₁ := upper₁ + upper₂ := upper₂ + +/-- `Var` of `SecretTypes.Lang.Two`. -/ +inductive Var where + | lo + | hi +deriving DecidableEq +open Var + +/-- `two : Vars`. -/ +def two : Vars where + Var := Var + deq := inferInstance + +/-- `label` of `SecretTypes.Typing`. -/ +def label : two.Var → twoPoint.Carrier + | lo => L + | hi => H + +/-- `⟨_,_⟩`, `low` and `_≈_` of `SecretTypes.Lang.Two`. -/ +def pair (l h : Nat) : Store two + | lo => l + | hi => h + +def low (s : Store two) : Nat := s lo + +def LowEq (s s' : Store two) : Prop := low s = low s' + +/-- `public-observer = principal two-point L`. -/ +def publicObserver : Observer twoPoint := principal twoPoint L + +theorem lowEq_agree {s s' : Store two} (eq : LowEq s s') : + Agree twoPoint.toSignature label publicObserver.sees s s' := fun + | lo, _ => eq + | hi, v => Empty.elim (show Empty from v) + +theorem agree_lowEq {s s' : Store two} + (f : Agree twoPoint.toSignature label publicObserver.sees s s') : LowEq s s' := + f lo () + +/-- N-2 at the two-point lattice: a public expression reads the same in +low-equivalent stores. -/ +theorem eval_low_two (e : Expr two) {s s' : Store two} + (p : lab twoPoint.toSignature label e = L) (eq : LowEq s s') : eval s e = eval s' e := + eval_low publicObserver e (p ▸ (() : le L L)) (lowEq_agree eq) + +/-- N-3 at the two-point lattice: under a secret counter the public variable +is unchanged, loops included. -/ +theorem confine_two {c : Cmd two} (fuel : Nat) {s t : Store two} + (d : Typed twoPoint.toSignature label H c) (h : exec fuel c s = some t) : low t = low s := + confine publicObserver fuel (pc := H) (fun v => Empty.elim (show Empty from v)) d h lo () + +/-- N-1, `tini` of `SecretTypes.Noninterference`: TINI at the two-point +lattice, fuels independent. -/ +theorem tini_two {pc : Label} {c : Cmd two} (fuel fuel' : Nat) {s s' t t' : Store two} + (d : Typed twoPoint.toSignature label pc c) (eq : LowEq s s') + (h : exec fuel c s = some t) (h' : exec fuel' c s' = some t') : LowEq t t' := + agree_lowEq (tini publicObserver fuel fuel' d (lowEq_agree eq) h h') + +/-! N-9, `SecretTypes.Noninterference.OutcomeVisibility`. -/ + +/-- `secret-loop = while (var hi) skip` and its typing at `L`. -/ +def secretLoop : Cmd two := .«while» (.var hi) .skip + +def secretLoopTyped : Typed twoPoint.toSignature label L secretLoop := .«while» .skip + +def s₀ : Store two := pair 0 0 +def s₁ : Store two := pair 0 1 + +theorem lowEquivalent : LowEq s₀ s₁ := rfl + +/-- `publicOutcome`: whether a run finished, and if so its public result. -/ +def publicOutcome (fuel : Nat) (c : Cmd two) (s : Store two) : Option Nat := + match exec fuel c s with + | none => none + | some t => some (low t) + +theorem secretLoop_never_finishes : ∀ fuel, exec fuel secretLoop s₀ = none + | 0 => rfl + | f + 1 => by + show bind (exec f .skip s₀) (exec f secretLoop) = none + rw [exec_skip] + exact secretLoop_never_finishes f + +theorem secretLoop_stops (fuel : Nat) : exec (fuel + 1) secretLoop s₁ = some s₁ := rfl + +theorem outcome_spins : publicOutcome 3 secretLoop s₀ = none := rfl +theorem outcome_stops : publicOutcome 3 secretLoop s₁ = some 0 := rfl + +theorem outcome_different : publicOutcome 3 secretLoop s₀ ≠ publicOutcome 3 secretLoop s₁ := + fun h => nomatch h + +/-- `TSNI`: the stronger two-run statement, with termination observable. -/ +def TSNI : Prop := + ∀ {pc : Label} {c : Cmd two} (fuel : Nat) {s s' : Store two}, + Typed twoPoint.toSignature label pc c → LowEq s s' → + publicOutcome fuel c s = publicOutcome fuel c s' + +/-- N-9, `termination-sensitive-fails`: TSNI is false for the current +typing rules. -/ +theorem termination_sensitive_fails : TSNI → False := + fun h => outcome_different (h 3 secretLoopTyped lowEquivalent) + +end SecretTypes.Two diff --git a/verification/legs/lean/lakefile.toml b/verification/legs/lean/lakefile.toml new file mode 100644 index 00000000..51a6b71e --- /dev/null +++ b/verification/legs/lean/lakefile.toml @@ -0,0 +1,8 @@ +# SPDX-License-Identifier: MPL-2.0 +# The Lean recheck leg of secret-types (PROOF-POLICY §2). Lean core only: +# no Mathlib and no other dependency (no `require` entries). +name = "secret-types-lean-leg" +defaultTargets = ["SecretTypes"] + +[[lean_lib]] +name = "SecretTypes" diff --git a/verification/legs/lean/lean-toolchain b/verification/legs/lean/lean-toolchain new file mode 100644 index 00000000..8e51ca6c --- /dev/null +++ b/verification/legs/lean/lean-toolchain @@ -0,0 +1 @@ +lean-4.24.0 diff --git a/verification/legs/rocq/.gitignore b/verification/legs/rocq/.gitignore new file mode 100644 index 00000000..4e2d09e2 --- /dev/null +++ b/verification/legs/rocq/.gitignore @@ -0,0 +1,6 @@ +*.vo +*.vok +*.vos +*.glob +.*.aux +.lia.cache diff --git a/verification/legs/rocq/SecretTypes.v b/verification/legs/rocq/SecretTypes.v new file mode 100644 index 00000000..2374e2c1 --- /dev/null +++ b/verification/legs/rocq/SecretTypes.v @@ -0,0 +1,535 @@ +(* SPDX-License-Identifier: MPL-2.0 + SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + + Rocq leg (PROOF-POLICY §2, route `re-proved`) of secret-types + N-1, N-2, N-3, N-7, N-8 and N-9. Mirrors src/SecretTypes/Vars.agda, + Lang.agda, Lattice/Record.agda, Typing/Generic.agda, + Noninterference/Statement.agda, Noninterference/Generic.agda, + Lattice.agda, Lang/Two.agda, Noninterference.agda, Countermodels.agda and + Noninterference/OutcomeVisibility.agda. + + Prelude only: no `Require` of the standard library, the counterpart of the + Agda gate's --no-libraries. No axioms: the `Print Assumptions` commands + at the end must report "Closed under the global context". + + Universe discipline: Agda's `Set` is `Type` here. The order, an + observer's `sees` and the typing derivations are `Type`-valued, as in + Agda. Equality of naturals is `Prop` here and a set in Agda; naturals + have decidable equality, so the two readings coincide. *) + +(* ---------------------------------------------------------------------- *) +(* SecretTypes.Vars and SecretTypes.Lattice.Record *) + +Record Vars := { Var : Type; deq : forall x y : Var, {x = y} + {x <> y} }. + +(* What Statement and Typing.Generic are parameterised by: no laws, so the + countermodels (N-8) can instantiate the statement where a law fails. *) +Record Signature := { + Carrier : Type; + le : Carrier -> Carrier -> Type; + join : Carrier -> Carrier -> Carrier; + bot : Carrier +}. + +Record Lattice := { + sig :> Signature; + le_trans : forall x y z, le sig x y -> le sig y z -> le sig x z; + upper1 : forall x y, le sig x (join sig x y); + upper2 : forall x y, le sig y (join sig x y) +}. + +Record Observer (L : Lattice) := { + sees : Carrier L -> Type; + down : forall x y, le L x y -> sees y -> sees x +}. +Arguments sees {L} o _. +Arguments down {L} o {x y} _ _. + +Definition principal (L : Lattice) (o : Carrier L) : Observer L := + {| sees := fun x => le L x o; + down := fun x y h v => le_trans L x y o h v |}. + +(* ---------------------------------------------------------------------- *) +(* SecretTypes.Lang *) + +Section Lang. +Variable V : Vars. + +Definition Store := Var V -> nat. + +Inductive Expr := lit (n : nat) | var (x : Var V) | plus (a b : Expr). + +Inductive Cmd := +| skip +| assign (x : Var V) (e : Expr) +| seq (c1 c2 : Cmd) +| ifz (e : Expr) (c1 c2 : Cmd) +| while (e : Expr) (c : Cmd). + +Fixpoint eval (s : Store) (e : Expr) : nat := + match e with + | lit n => n + | var x => s x + | plus a b => eval s a + eval s b + end. + +(* update x n s y = select (x ≟ᵥ y) n (s y) *) +Definition update (x : Var V) (n : nat) (s : Store) : Store := + fun y => if deq V x y then n else s y. + +Definition bind {A : Type} (m : option A) (f : A -> option A) : option A := + match m with None => None | Some a => f a end. + +(* One step of fuel, structural in the command; `prev` is the run at one + less fuel, None at fuel zero (where a loop does not finish). *) +Fixpoint run (prev : option (Cmd -> Store -> option Store)) (c : Cmd) (s : Store) + : option Store := + match c with + | skip => Some s + | assign x e => Some (update x (eval s e) s) + | seq c1 c2 => bind (run prev c1 s) (run prev c2) + | ifz e c1 c2 => match eval s e with 0 => run prev c1 s | S _ => run prev c2 s end + | while e c => + match prev with + | None => None + | Some p => match eval s e with + | 0 => bind (p c s) (p (while e c)) + | S _ => Some s + end + end + end. + +(* exec of SecretTypes.Lang, clause by clause: sequence and ifz keep the + fuel; a loop at S f runs its body and re-enters at f; at 0 it is None. *) +Fixpoint exec (f : nat) : Cmd -> Store -> option Store := + match f with 0 => run None | S f' => run (Some (exec f')) end. + +End Lang. + +Arguments lit {V} n. +Arguments var {V} x. +Arguments plus {V} a b. +Arguments skip {V}. +Arguments assign {V} x e. +Arguments seq {V} c1 c2. +Arguments ifz {V} e c1 c2. +Arguments while {V} e c. +Arguments eval {V} s e. +Arguments update {V} x n s _. +Arguments exec {V} f _ _. + +(* ---------------------------------------------------------------------- *) +(* SecretTypes.Typing.Generic and Noninterference.Statement *) + +Section Typing. +Context {V : Vars} (S : Signature) (label : Var V -> Carrier S). + +Fixpoint lab (e : Expr V) : Carrier S := + match e with + | lit _ => bot S + | var x => label x + | plus a b => join S (lab a) (lab b) + end. + +Inductive Typed : Carrier S -> Cmd V -> Type := +| t_skip : forall pc, Typed pc skip +| t_assign : forall pc x e, le S (join S pc (lab e)) (label x) -> Typed pc (assign x e) +| t_seq : forall pc c1 c2, Typed pc c1 -> Typed pc c2 -> Typed pc (seq c1 c2) +| t_ifz : forall pc e c1 c2, Typed (join S pc (lab e)) c1 -> + Typed (join S pc (lab e)) c2 -> Typed pc (ifz e c1 c2) +| t_while : forall pc e c, Typed (join S pc (lab e)) c -> Typed pc (while e c). + +Definition Agree (sees : Carrier S -> Type) (s s' : Store V) : Prop := + forall x, sees (label x) -> s x = s' x. + +Definition TINI (sees : Carrier S -> Type) : Prop := + forall pc c fuel fuel' s s' t t', Typed pc c -> Agree sees s s' -> + exec fuel c s = Some t -> exec fuel' c s' = Some t' -> Agree sees t t'. + +End Typing. + +Arguments t_skip {V S label pc}. +Arguments t_assign {V S label pc x e} _. +Arguments t_seq {V S label pc c1 c2} _ _. +Arguments t_ifz {V S label pc e c1 c2} _ _. +Arguments t_while {V S label pc e c} _. + +(* ---------------------------------------------------------------------- *) +(* SecretTypes.Noninterference.Generic *) + +Section Proof. +Context {V : Vars} (L : Lattice) (label : Var V -> Carrier L) (O : Observer L). + +Notation agree := (Agree L label (sees O)). +Notation typed := (Typed L label). +Notation labe := (lab L label). + +Lemma bind_some {A : Type} (m : option A) (f : A -> option A) t : + bind m f = Some t -> {a : A & (m = Some a) * (f a = Some t)}%type. +Proof. destruct m as [a|]; simpl; intro h; [exists a; split; auto | discriminate]. Defined. + +Definition branch (n : nat) (c1 c2 : Cmd V) : Cmd V := + match n with 0 => c1 | S _ => c2 end. + +Lemma exec_skip f (s : Store V) : exec f skip s = Some s. +Proof. destruct f; reflexivity. Qed. + +Lemma exec_assign f x e (s : Store V) : exec f (assign x e) s = Some (update x (eval s e) s). +Proof. destruct f; reflexivity. Qed. + +Lemma exec_seq f (c1 c2 : Cmd V) (s : Store V) : exec f (seq c1 c2) s = bind (exec f c1 s) (exec f c2). +Proof. destruct f; reflexivity. Qed. + +Lemma exec_ifz f e (c1 c2 : Cmd V) (s : Store V) : exec f (ifz e c1 c2) s = exec f (branch (eval s e) c1 c2) s. +Proof. destruct f; simpl; destruct (eval s e); reflexivity. Qed. + +Lemma exec_while_succ f e (c : Cmd V) (s : Store V) : + exec (S f) (while e c) s = + match eval s e with 0 => bind (exec f c s) (exec f (while e c)) | S _ => Some s end. +Proof. reflexivity. Qed. + +Definition branch_typed pc n c1 c2 (d1 : typed pc c1) (d2 : typed pc c2) + : typed pc (branch n c1 c2) := + match n with 0 => d1 | S _ => d2 end. + +Lemma unseen_join pc y : (sees O pc -> False) -> sees O (join L pc y) -> False. +Proof. intros np v. exact (np (down O (upper1 L pc y) v)). Qed. + +(* N-2, eval-low *) +Lemma eval_low : forall (e : Expr V) (s s' : Store V), sees O (labe e) -> agree s s' -> eval s e = eval s' e. +Proof. + induction e as [n|x|a IHa b IHb]; intros s s' v eq; simpl. + - reflexivity. + - exact (eq x v). + - rewrite (IHa s s' (down O (upper1 L _ _) v) eq). + rewrite (IHb s s' (down O (upper2 L _ _) v) eq). reflexivity. +Qed. + +Lemma agree_refl (s : Store V) : agree s s. +Proof. intros x _; reflexivity. Qed. +Lemma agree_symm (s s' : Store V) : agree s s' -> agree s' s. +Proof. intros h x v; symmetry; exact (h x v). Qed. +Lemma agree_trans (s s' s'' : Store V) : agree s s' -> agree s' s'' -> agree s s''. +Proof. intros h k x v; rewrite (h x v); exact (k x v). Qed. + +Lemma confine_assign pc x e n (s : Store V) : + (sees O pc -> False) -> le L (join L pc (labe e)) (label x) -> agree (update x n s) s. +Proof. + intros np ok y v. unfold update. destruct (deq V x y) as [hxy|hxy]. + - subst y. destruct (unseen_join pc (labe e) np (down O ok v)). + - reflexivity. +Qed. + +(* N-3, confine *) +Lemma confine : forall fuel pc (c : Cmd V) (s t : Store V), + (sees O pc -> False) -> typed pc c -> exec fuel c s = Some t -> agree t s. +Proof. + induction fuel as [|f IHf]; intros pc c s t np d; revert s t np; + induction d as [pc|pc x e ok|pc c1 c2 d1 IH1 d2 IH2|pc e c1 c2 d1 IH1 d2 IH2|pc e c d IH]; + intros s t np h. + all: try (rewrite exec_skip in h; injection h as <-; apply agree_refl). + all: try (rewrite exec_assign in h; injection h as <-; exact (confine_assign pc x e _ s np ok)). + all: try (rewrite exec_seq in h; destruct (bind_some _ _ _ h) as [s1 [h1 h2]]; + exact (agree_trans _ _ _ (IH2 _ _ np h2) (IH1 _ _ np h1))). + all: try (rewrite exec_ifz in h; pose proof (unseen_join pc (labe e) np) as np'; + destruct (eval s e); [exact (IH1 _ _ np' h) | exact (IH2 _ _ np' h)]). + - discriminate h. + - rewrite exec_while_succ in h. pose proof (unseen_join pc (labe e) np) as np'. + destruct (eval s e). + + destruct (bind_some _ _ _ h) as [s1 [h1 h2]]. + exact (agree_trans _ _ _ (IHf _ _ _ _ np (t_while d) h2) (IHf _ _ _ _ np' d h1)). + + injection h as <-; apply agree_refl. +Qed. + +(* confineL: a loop whose body is typed under an unseen counter, re-entered + without re-typing the loop. *) +Lemma confine_loop : forall fuel l (e : Expr V) (c : Cmd V) (s t : Store V), + (sees O l -> False) -> typed l c -> exec fuel (while e c) s = Some t -> agree t s. +Proof. + induction fuel as [|f IHf]; intros l e c s t np d h. + - discriminate h. + - rewrite exec_while_succ in h. destruct (eval s e). + + destruct (bind_some _ _ _ h) as [s1 [h1 h2]]. + exact (agree_trans _ _ _ (IHf _ _ _ _ _ np d h2) (confine f _ _ _ _ np d h1)). + + injection h as <-; apply agree_refl. +Qed. + +Fixpoint nat_eq_dec (n m : nat) : {n = m} + {n <> m}. +Proof. decide equality. Defined. + +(* Agreement is a family of equations between naturals, hence stable under + double negation (as in the Agda proof). *) +Lemma agree_stable (s s' : Store V) : ((agree s s' -> False) -> False) -> agree s s'. +Proof. + intros h x v. destruct (nat_eq_dec (s x) (s' x)) as [e|ne]; [exact e|]. + destruct (h (fun a => ne (a x v))). +Qed. + +Lemma by_cases_sees (s s' : Store V) j : + (sees O j -> agree s s') -> ((sees O j -> False) -> agree s s') -> agree s s'. +Proof. + intros yes no. apply agree_stable. intro bad. + apply bad. apply no. intro v. apply bad. exact (yes v). +Qed. + +(* N-7, tini *) +Theorem tini : TINI L label (sees O). +Proof. + intros pc c fuel. revert pc c. + induction fuel as [|f IHf]; intros pc c fuel' s s' t t' d; revert fuel' s s' t t'; + induction d as [pc|pc x e ok|pc c1 c2 d1 IH1 d2 IH2|pc e c1 c2 d1 IH1 d2 IH2|pc e c d IH]; + intros fuel' s s' t t' eq h h'. + all: try (rewrite exec_skip in h, h'; injection h as <-; injection h' as <-; exact eq). + all: try (rewrite exec_assign in h, h'; injection h as <-; injection h' as <-; + intros y v; unfold update; destruct (deq V x y) as [hxy|hxy]; + [subst y; exact (eval_low e s s' (down O (upper2 L _ _) (down O ok v)) eq) + | exact (eq y v)]). + all: try (rewrite exec_seq in h, h'; + destruct (bind_some _ _ _ h) as [s1 [h1 h2]]; + destruct (bind_some _ _ _ h') as [s1' [h1' h2']]; + exact (IH2 _ _ _ _ _ (IH1 _ _ _ _ _ eq h1 h1') h2 h2')). + all: try (rewrite exec_ifz in h, h'; + apply (by_cases_sees _ _ (join L pc (labe e))); + [ intro v; pose proof (eval_low e s s' (down O (upper2 L _ _) v) eq) as ge; + rewrite <- ge in h'; destruct (eval s e); + [exact (IH1 _ _ _ _ _ eq h h') | exact (IH2 _ _ _ _ _ eq h h')] + | intro nv; + exact (agree_trans _ _ _ (confine _ _ _ _ _ nv (branch_typed _ _ _ _ d1 d2) h) + (agree_trans _ _ _ eq + (agree_symm _ _ (confine _ _ _ _ _ nv (branch_typed _ _ _ _ d1 d2) h')))) ]). + - discriminate h. + - destruct fuel' as [|f']; [discriminate h'|]. + apply (by_cases_sees _ _ (join L pc (labe e))). + + intro v. pose proof (eval_low e s s' (down O (upper2 L _ _) v) eq) as ge. + rewrite exec_while_succ in h, h'. rewrite <- ge in h'. destruct (eval s e). + * destruct (bind_some _ _ _ h) as [s1 [h1 h2]]. + destruct (bind_some _ _ _ h') as [s1' [h1' h2']]. + exact (IHf _ _ _ _ _ _ _ (t_while d) (IHf _ _ _ _ _ _ _ d eq h1 h1') h2 h2'). + * injection h as <-; injection h' as <-; exact eq. + + intro nv. + exact (agree_trans _ _ _ (confine_loop _ _ _ _ _ _ nv d h) + (agree_trans _ _ _ eq (agree_symm _ _ (confine_loop _ _ _ _ _ _ nv d h')))). +Qed. + +End Proof. + +(* ---------------------------------------------------------------------- *) +(* The two-point lattice (SecretTypes.Lattice, Lang.Two, Typing, *) +(* Noninterference): N-1, and N-2/N-3 at that lattice *) + +Module Two. + +Inductive Label := L | H. + +(* A computed predicate, as in SecretTypes.Lattice. *) +Definition le2 (x y : Label) : Type := + match x, y with L, _ => unit | H, L => Empty_set | H, H => unit end. + +Definition join2 (x y : Label) : Label := match x with L => y | H => H end. + +Definition le2_trans x y z : le2 x y -> le2 y z -> le2 x z := + match x, y, z with + | L, _, _ => fun _ _ => tt + | H, H, H => fun _ _ => tt + | H, H, L => fun _ k => k + | H, L, _ => fun h _ => match h with end + end. + +Definition up1 x y : le2 x (join2 x y) := match x with L => match y with L => tt | H => tt end | H => tt end. +Definition up2 x y : le2 y (join2 x y) := + match x, y with L, L => tt | L, H => tt | H, L => tt | H, H => tt end. + +Definition twoSig : Signature := {| Carrier := Label; le := le2; join := join2; bot := L |}. +Definition twoPoint : Lattice := {| sig := twoSig; le_trans := le2_trans; upper1 := up1; upper2 := up2 |}. + +Inductive TVar := lo | hi. +Definition tdeq (x y : TVar) : {x = y} + {x <> y}. +Proof. decide equality. Defined. +Definition two : Vars := {| Var := TVar; deq := tdeq |}. + +Definition label (x : Var two) : Carrier twoPoint := match x with lo => L | hi => H end. + +Definition pair (l h : nat) : Store two := fun x => match x with lo => l | hi => h end. +Definition low (s : Store two) : nat := s lo. +Definition LowEq (s s' : Store two) : Prop := low s = low s'. + +Definition publicObserver : Observer twoPoint := principal twoPoint L. + +Lemma lowEq_agree s s' : LowEq s s' -> Agree twoPoint label (sees publicObserver) s s'. +Proof. intros eq [|] v; [exact eq | destruct v]. Qed. + +Lemma agree_lowEq s s' : Agree twoPoint label (sees publicObserver) s s' -> LowEq s s'. +Proof. intro f. exact (f lo tt). Qed. + +(* N-2 at the two-point lattice *) +Lemma eval_low_two (e : Expr two) s s' : + lab twoPoint label e = L -> LowEq s s' -> eval s e = eval s' e. +Proof. + intros p eq. apply (eval_low twoPoint label publicObserver e s s'). + - change (le2 (lab twoPoint label e) L). rewrite p. exact tt. + - exact (lowEq_agree _ _ eq). +Qed. + +(* N-3 at the two-point lattice *) +Lemma confine_two (c : Cmd two) fuel s t : + Typed twoPoint label H c -> exec fuel c s = Some t -> low t = low s. +Proof. + intros d h. exact (confine twoPoint label publicObserver fuel H c s t + (fun v : Empty_set => match v with end) d h lo tt). +Qed. + +(* N-1, tini of SecretTypes.Noninterference *) +Theorem tini_two pc (c : Cmd two) fuel fuel' s s' t t' : + Typed twoPoint label pc c -> LowEq s s' -> + exec fuel c s = Some t -> exec fuel' c s' = Some t' -> LowEq t t'. +Proof. + intros d eq h h'. apply agree_lowEq. + exact (tini twoPoint label publicObserver pc c fuel fuel' s s' t t' d (lowEq_agree _ _ eq) h h'). +Qed. + +(* N-9, SecretTypes.Noninterference.OutcomeVisibility *) +Definition secretLoop : Cmd two := while (@var two hi) skip. +Definition secretLoopTyped : Typed twoPoint label L secretLoop := t_while t_skip. +Definition s0 : Store two := pair 0 0. +Definition s1 : Store two := pair 0 1. +Lemma lowEquivalent : LowEq s0 s1. +Proof. reflexivity. Qed. + +Definition publicOutcome fuel (c : Cmd two) s : option nat := + match exec fuel c s with None => None | Some t => Some (low t) end. + +Lemma secretLoop_never_finishes : forall fuel, exec fuel secretLoop s0 = None. +Proof. + induction fuel as [|f IH]; [reflexivity|]. + change (bind (exec f skip s0) (exec f secretLoop) = None). + rewrite exec_skip. exact IH. +Qed. + +Lemma secretLoop_stops fuel : exec (S fuel) secretLoop s1 = Some s1. +Proof. reflexivity. Qed. + +Lemma outcome_different : publicOutcome 3 secretLoop s0 <> publicOutcome 3 secretLoop s1. +Proof. discriminate. Qed. + +Definition TSNI : Prop := + forall pc (c : Cmd two) fuel s s', Typed twoPoint label pc c -> LowEq s s' -> + publicOutcome fuel c s = publicOutcome fuel c s'. + +Theorem termination_sensitive_fails : TSNI -> False. +Proof. intro h. exact (outcome_different (h L secretLoop 3 s0 s1 secretLoopTyped lowEquivalent)). Qed. + +End Two. + +(* ---------------------------------------------------------------------- *) +(* N-8, SecretTypes.Countermodels *) + +Module Countermodels. +Import Two. + +Definition std (x : Var two) : Label := match x with lo => L | hi => H end. +Definition withJoin (j : Label -> Label -> Label) : Signature := + {| Carrier := Label; le := le2; join := j; bot := L |}. +Definition belowL (x : Label) : Type := le2 x L. + +Lemma agree01 (S : Signature) (lb : Var two -> Carrier S) (sees : Carrier S -> Type) : + (sees (lb hi) -> False) -> Agree S lb sees s0 s1. +Proof. intros n [|] v; [reflexivity | destruct (n v)]. Qed. + +Module NoUpper1. + Definition joinR (x y : Label) : Label := y. + Definition S := withJoin joinR. + Lemma not_upper1 : (forall x y, le2 x (joinR x y)) -> False. + Proof. intro h. destruct (h H L). Qed. + Definition implicitFlow : Cmd two := ifz (@var two hi) (@assign two lo (lit 0)) (@assign two lo (lit 1)). + Definition typed : Typed S std L implicitFlow. + Proof. apply t_ifz; apply t_assign; exact tt. Defined. + Theorem refutes : TINI S std belowL -> False. + Proof. + intro tini. pose proof (tini L implicitFlow 1 1 s0 s1 _ _ typed + (agree01 S std belowL (fun v : Empty_set => match v with end)) eq_refl eq_refl lo tt) as e. + discriminate e. + Qed. +End NoUpper1. + +Module NoUpper2. + Definition joinL (x y : Label) : Label := x. + Definition S := withJoin joinL. + Lemma not_upper2 : (forall x y, le2 y (joinL x y)) -> False. + Proof. intro h. destruct (h L H). Qed. + Definition explicitFlow : Cmd two := @assign two lo (@var two hi). + Definition typed : Typed S std L explicitFlow. + Proof. apply t_assign; exact tt. Defined. + Theorem refutes : TINI S std belowL -> False. + Proof. + intro tini. pose proof (tini L explicitFlow 1 1 s0 s1 _ _ typed + (agree01 S std belowL (fun v : Empty_set => match v with end)) eq_refl eq_refl lo tt) as e. + discriminate e. + Qed. +End NoUpper2. + +Module NoDownClosure. + Definition seesH (x : Label) : Type := x = H. + Lemma not_down_closed : (forall x y, le2 x y -> seesH y -> seesH x) -> False. + Proof. intro h. discriminate (h L H tt eq_refl). Qed. + Definition S := withJoin join2. + Definition up : Cmd two := @assign two hi (@var two lo). + Definition typed : Typed S std L up. + Proof. apply t_assign; exact tt. Defined. + Definition t0 : Store two := pair 0 0. + Definition t1 : Store two := pair 1 0. + Lemma agree : Agree S std seesH t0 t1. + Proof. intros [|] v; [discriminate v | reflexivity]. Qed. + Theorem refutes : TINI S std seesH -> False. + Proof. + intro tini. pose proof (tini L up 1 1 t0 t1 _ _ typed agree eq_refl eq_refl hi eq_refl) as e. + discriminate e. + Qed. +End NoDownClosure. + +Module NoTrans. + Inductive P := B | H' | M | L' | T. + Inductive Le : P -> P -> Type := + | le_refl : forall x, Le x x + | le_bot : forall x, Le B x + | le_top : forall x, Le x T + | le_HM : Le H' M + | le_ML : Le M L'. + Definition joinP (x y : P) : P := + match x, y with + | B, y => y | T, _ => T + | H', B => H' | H', H' => H' | H', M => M | H', L' => T | H', T => T + | M, B => M | M, H' => M | M, M => M | M, L' => L' | M, T => T + | L', B => L' | L', H' => T | L', M => L' | L', L' => L' | L', T => T + end. + Lemma not_trans : (forall x y z, Le x y -> Le y z -> Le x z) -> False. + Proof. intro t. pose proof (t _ _ _ le_HM le_ML) as k. inversion k. Qed. + Definition S : Signature := {| Carrier := P; le := Le; join := joinP; bot := B |}. + Definition labelP (x : Var two) : P := match x with lo => M | hi => H' end. + Definition explicitFlow : Cmd two := @assign two lo (@var two hi). + Definition typed : Typed S labelP B explicitFlow. + Proof. apply t_assign; exact le_HM. Defined. + Definition belowL' (x : P) : Type := Le x L'. + Lemma agree : Agree S labelP belowL' s0 s1. + Proof. intros [|] v; [reflexivity | inversion v]. Qed. + Theorem refutes : TINI S labelP belowL' -> False. + Proof. + intro tini. pose proof (tini B explicitFlow 1 1 s0 s1 _ _ typed agree eq_refl eq_refl lo le_ML) as e. + discriminate e. + Qed. +End NoTrans. + +End Countermodels. + +(* Axioms each theorem rests on (PROOF-POLICY §8.4): every line must read + "Closed under the global context". *) +Print Assumptions eval_low. +Print Assumptions confine. +Print Assumptions tini. +Print Assumptions Two.eval_low_two. +Print Assumptions Two.confine_two. +Print Assumptions Two.tini_two. +Print Assumptions Two.termination_sensitive_fails. +Print Assumptions Countermodels.NoUpper1.refutes. +Print Assumptions Countermodels.NoUpper2.refutes. +Print Assumptions Countermodels.NoDownClosure.refutes. +Print Assumptions Countermodels.NoTrans.refutes. diff --git a/verification/receipts/agda-pwg_praxis.deed b/verification/receipts/agda-pwg_praxis.deed index 6da221af..b28d6493 100644 --- a/verification/receipts/agda-pwg_praxis.deed +++ b/verification/receipts/agda-pwg_praxis.deed @@ -13,7 +13,7 @@ :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 "eee4e4038503") + :source-commit "efb9aa9ab390") (prover :tool "agda" :version "2.6.4.3" @@ -42,17 +42,37 @@ :axioms-assumed 0 :note "A non-zero count above fails the gate; the receipt is only meaningful while all four are zero") ; PWGs apply to theory theorems (PROOF-POLICY section 8.1); refusal fixtures and leak witnesses are n/a. - ; Independent Rocq and Lean legs remain unavailable: no transport or hand re-proof. + ; Rocq and Lean legs: re-proved by hand (Agda2Dedukti cannot run on the pinned Agda), RECONCILED in verification/legs/README.adoc. + (legs + :gate "bash scripts/check-legs.sh" + :ci ".github/workflows/proofs.yml (job legs)" + :correspondence "verification/legs/README.adoc" + :route "re-proved" + :route-reason "Agda2Dedukti is an Agda backend pinned to a fork (b026db1, GHC 8.10) and cannot run on Agda 2.6.4.3; no released Dedukti/Lambdapi exporter to Lean 4, and no pinned route to Rocq" + :state "RECONCILED" + :review "statement comparison written by Claude Code; provisional until owner review (estate doctrine 4)" + (leg :prover "rocq" :checker "coqc" :version "8.18.0" :invocation "coqc -q SecretTypes.v (in verification/legs/rocq)" :libraries "none (no Require)" :axioms "none (Print Assumptions: Closed under the global context)") + (leg :prover "lean" :checker "lean" :version "4.24.0" :invocation "lake build; lake env lean Axioms.lean (in verification/legs/lean)" :libraries "none (lakefile has no require; no Mathlib)" :axioms "none (#print axioms: does not depend on any axioms)") + (inputs + (input :path "verification/legs/rocq/SecretTypes.v" :sha256 "acffaa9b4884b46c61fae6f2c91a34e7005b5d4b6158ebcc83bde25bc573b75e") + (input :path "verification/legs/lean/Axioms.lean" :sha256 "078d9a566e80b9f9701ba1b3f12bd5897e372c41f7d2dcfdf13c2f6d07159ae7") + (input :path "verification/legs/lean/SecretTypes.lean" :sha256 "48d02eea6800f9655c1a1d968cbeb9b8d8aa2594f6ad47915cbc8247e4157b8d") + (input :path "verification/legs/lean/SecretTypes/Countermodels.lean" :sha256 "ef2dc1f54aa0ac76acea9c020c9fa0adecfb864e27caa184339090d233bd6ed5") + (input :path "verification/legs/lean/SecretTypes/Generic.lean" :sha256 "13b10fd744828bc5ea3551346aeaa7795b51f24e8585e26c9dc737805c054cfa") + (input :path "verification/legs/lean/SecretTypes/Two.lean" :sha256 "74387c6eec74dbbfada1c08d5ef96451740c37e439db8aa5a17ece44e4cf318a") + (input :path "verification/legs/lean/lakefile.toml" :sha256 "75b8b79a27ec284d2c383302c88c90248ab56ee9902664068140d014b45bcf34") + (input :path "verification/legs/lean/lean-toolchain" :sha256 "387019dd5f6d8213249f99bfe1bd9f346678bf0d4612938c1e7feae386665335") + )) (claims - (claim :id "N-1" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") - (claim :id "N-2" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") - (claim :id "N-3" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") + (claim :id "N-1" :token "proven" :pwg "2ii" :coq-leg "re-proved" :lean-leg "re-proved") + (claim :id "N-2" :token "proven" :pwg "2ii" :coq-leg "re-proved" :lean-leg "re-proved") + (claim :id "N-3" :token "proven" :pwg "2ii" :coq-leg "re-proved" :lean-leg "re-proved") (claim :id "N-4" :token "tested-only" :pwg "n/a" :coq-leg "n/a" :lean-leg "n/a") (claim :id "N-5" :token "tested-only" :pwg "n/a" :coq-leg "n/a" :lean-leg "n/a") (claim :id "N-6" :token "tested-only" :pwg "n/a" :coq-leg "n/a" :lean-leg "n/a") - (claim :id "N-7" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") - (claim :id "N-8" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") - (claim :id "N-9" :token "proven" :pwg "3" :coq-leg "unavailable" :lean-leg "unavailable") + (claim :id "N-7" :token "proven" :pwg "2ii" :coq-leg "re-proved" :lean-leg "re-proved") + (claim :id "N-8" :token "proven" :pwg "2ii" :coq-leg "re-proved" :lean-leg "re-proved") + (claim :id "N-9" :token "proven" :pwg "2ii" :coq-leg "re-proved" :lean-leg "re-proved") ) ; Every module hash is checked against the current tree. (modules From 45046c2c0f92ddae2ff73c8c05555bed419f46ad Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:56:56 +0000 Subject: [PATCH 4/7] Legs: SPDX header on the two new .gitignore files lean-toolchain cannot carry one: Lean reads the whole file as the toolchain name. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs --- verification/legs/lean/.gitignore | 1 + verification/legs/rocq/.gitignore | 1 + 2 files changed, 2 insertions(+) diff --git a/verification/legs/lean/.gitignore b/verification/legs/lean/.gitignore index 6009e03c..a2524e9c 100644 --- a/verification/legs/lean/.gitignore +++ b/verification/legs/lean/.gitignore @@ -1,3 +1,4 @@ +# SPDX-License-Identifier: MPL-2.0 .lake/ # Written by `lake build`; with no `require` it lists no package, and it is not # JCS-serialised (estate JSON policy), so it is not committed. diff --git a/verification/legs/rocq/.gitignore b/verification/legs/rocq/.gitignore index 4e2d09e2..683abf2a 100644 --- a/verification/legs/rocq/.gitignore +++ b/verification/legs/rocq/.gitignore @@ -1,3 +1,4 @@ +# SPDX-License-Identifier: MPL-2.0 *.vo *.vok *.vos From 3bf7f8e3772572fbf7342af2b953f75a9b104be4 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:28:09 +0000 Subject: [PATCH 5/7] =?UTF-8?q?proof(flags):=20canonical=20--cubical-compa?= =?UTF-8?q?tible=20invocation=20in=20force;=20grades=20as=20PROOF-POLICY?= =?UTF-8?q?=20=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") From 18cbabfa6bd0ff2060cdb764e90a8b818f4367d9 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:29:55 +0000 Subject: [PATCH 6/7] Legs README: do not start a continuation line with '11.' A list-item continuation beginning "11. The prelude's ..." parsed as an ordered list (asciidoctor: list item index: expected 1, got 11), which check-adoc-renders.sh fails. Rewrapped; the text is unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs --- verification/legs/README.adoc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/verification/legs/README.adoc b/verification/legs/README.adoc index dbff753f..6c748fd5 100644 --- a/verification/legs/README.adoc +++ b/verification/legs/README.adoc @@ -55,8 +55,9 @@ compared by hand below. Every theorem below is printed with its axioms (§8.4): -* Rocq: `Print Assumptions` reports `Closed under the global context` for all - 11. The prelude's classical axioms are not loaded, so none can enter. +* Rocq: `Print Assumptions` reports `Closed under the global context` for + all 11 theorems. The prelude's classical axioms are not loaded, so none can + enter. * Lean: `#print axioms` (in `lean/Axioms.lean`) reports `does not depend on any axioms` for all 11. In particular, no `propext`, `Quot.sound` or `Classical.choice`. From 10cd0162a3a4b929abeeaad3b2d997433153cbb7 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 19:06:13 +0000 Subject: [PATCH 7/7] fix(legs): clear the 5 SonarCloud shell findings on #34 S7688 (4, check-legs.sh): the version-pin and axiom-count tests use [[ ]] instead of [ ]. S7679 (grade-receipt.sh): leg_token reads its argument into a local variable. Behaviour is unchanged. Checked: check-legs.sh passes (Coq 8.18.0, Lean 4.24.0), and with the Lean pin set to a wrong version it still exits 2. grade-receipt.sh --check passes (15 modules). Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_0136P7ZmAsYpFA9gxfQLF3F6 Signed-off-by: Claude --- scripts/check-legs.sh | 8 ++++---- scripts/grade-receipt.sh | 5 ++++- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/scripts/check-legs.sh b/scripts/check-legs.sh index b615d688..eeabcec9 100755 --- a/scripts/check-legs.sh +++ b/scripts/check-legs.sh @@ -23,9 +23,9 @@ LEAN_VERSION=4.24.0 fail=0 got="$(coqc --version | sed -n 's/^The Coq Proof Assistant, version \([0-9.]*\).*/\1/p')" -[ "$got" = "$COQ_VERSION" ] || { echo "ERROR: expected Coq $COQ_VERSION, found '${got:-none}'" >&2; exit 2; } +[[ "$got" == "$COQ_VERSION" ]] || { echo "ERROR: expected Coq $COQ_VERSION, found '${got:-none}'" >&2; exit 2; } got="$(lean --version | sed -n 's/^Lean (version \([0-9.]*\),.*/\1/p')" -[ "$got" = "$LEAN_VERSION" ] || { echo "ERROR: expected Lean $LEAN_VERSION, found '${got:-none}'" >&2; exit 2; } +[[ "$got" == "$LEAN_VERSION" ]] || { echo "ERROR: expected Lean $LEAN_VERSION, found '${got:-none}'" >&2; exit 2; } # The Lean leg may not depend on anything: no `require` in the lakefile. if grep -nE '^\s*\[\[require\]\]|^\s*require\b' verification/legs/lean/lakefile.toml; then @@ -43,7 +43,7 @@ fi rocq_out="$(cd verification/legs/rocq && coqc -q SecretTypes.v 2>&1)" || { echo "$rocq_out" >&2; echo 'FAIL: the Rocq leg does not check' >&2; exit 1; } n_closed="$(grep -c '^Closed under the global context$' <<< "$rocq_out" || true)" n_print="$(grep -c '^Print Assumptions ' verification/legs/rocq/SecretTypes.v)" -if [ "$n_closed" != "$n_print" ] || grep -vq '^Closed under the global context$' <<< "$rocq_out"; then +if [[ "$n_closed" != "$n_print" ]] || grep -vq '^Closed under the global context$' <<< "$rocq_out"; then echo "$rocq_out" >&2; echo "FAIL: the Rocq leg rests on an axiom ($n_closed of $n_print closed)" >&2; fail=1 else echo "PASS: Rocq leg (Coq $COQ_VERSION), $n_print theorems closed under the global context" @@ -53,7 +53,7 @@ lean_out="$(cd verification/legs/lean && lake build >/dev/null && lake env lean || { echo "$lean_out" >&2; echo 'FAIL: the Lean leg does not check' >&2; exit 1; } n_free="$(grep -c 'does not depend on any axioms$' <<< "$lean_out" || true)" n_ax="$(grep -c '^#print axioms ' verification/legs/lean/Axioms.lean)" -if [ "$n_free" != "$n_ax" ] || grep -vq 'does not depend on any axioms$' <<< "$lean_out"; then +if [[ "$n_free" != "$n_ax" ]] || grep -vq 'does not depend on any axioms$' <<< "$lean_out"; then echo "$lean_out" >&2; echo "FAIL: the Lean leg rests on an axiom ($n_free of $n_ax free)" >&2; fail=1 else echo "PASS: Lean leg (Lean $LEAN_VERSION, core only), $n_ax theorems depend on no axioms" diff --git a/scripts/grade-receipt.sh b/scripts/grade-receipt.sh index 258e571c..82205d6f 100755 --- a/scripts/grade-receipt.sh +++ b/scripts/grade-receipt.sh @@ -161,7 +161,10 @@ emit_legs() { # A leg's §5 token: a RECONCILED re-proof is kernel-checked with no axiom # (scripts/check-legs.sh), so it is proven; any other state is still open. -leg_token() { [[ "$1" == RECONCILED ]] && printf 'proven' || printf 'open'; } +leg_token() { + local state="$1" + [[ "$state" == RECONCILED ]] && printf 'proven' || printf 'open' +} # Print the derived receipt, including claim rows, module hashes and fixtures. emit() {