diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 116e91a..7a8540e 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 da8bfbc..dea8ce1 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 bcfcd93..82744c2 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 605f71d..fb4db23 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 41ae5e3..16f80b2 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 015ee88..8443052 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 d3cf09b..47d2ea9 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 da3c25f..397c894 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/secret-types_chora.deed b/secret-types_chora.deed index 8c4a14d..bbcb71b 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/src/SecretTypes/Noninterference/Generic.agda b/src/SecretTypes/Noninterference/Generic.agda index fe0c1d5..4eb90da 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 710fa4e..e1b9fd5 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/tests/workflows/governance_policy_test.sh b/tests/workflows/governance_policy_test.sh index bab332e..a2fe91f 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 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 6675ed7..6da221a 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")