From b64974cad9dced8f8a95d3961685e5110ceb06f0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:18:54 +0000 Subject: [PATCH 1/2] proofs: meet --cubical-compatible; retire waiver W-1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 13 remaining UnsupportedIndexedMatch warnings, in tini, go, confine and confineW, all came from clauses that matched `refl : just s ≡ just t`. Those clauses now take the equation as a variable and use Prelude.just-inj, defined as `cong (from-just a)`. cong matches refl only against a variable, so no clause asks for the injectivity of `just`. Agreement follows by subst/subst₂ or from a store equality (≈-from-≡). No theorem statement changed and the fuel semantics is untouched, so the relational big-step semantics W-1 named as the way out, and its consequence for N-5, are not needed. With the warnings gone, --cubical-compatible joins scripts/proof-flags.sh and the gate runs PROOF-POLICY §2.1's canonical invocation under --double-check -W error, so a new indexed match fails the gate. The receipt records cubical-compatible "met"; PROOF-STATUS and proof-debt keep W-1 as a dated, retired record. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg --- PROOF-STATUS.adoc | 56 +++++++++---------- docs/proof-debt.adoc | 45 ++++++++++----- scripts/grade-receipt.sh | 3 +- scripts/proof-flags.sh | 21 ++++--- src/SecretTypes/Noninterference/Generic.agda | 16 ++++-- src/SecretTypes/Prelude.agda | 26 ++++++--- verification/receipts/agda-grade3_praxis.deed | 13 ++--- 7 files changed, 102 insertions(+), 78 deletions(-) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index da8bfbc4..f6e805e6 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -76,35 +76,30 @@ 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` +=== `--cubical-compatible`: met (W-1 retired) `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 (`scripts/proof-flags.sh`) now runs exactly that, with four stricter +options: `--no-libraries --ignore-interfaces --double-check -W error`. Because +`-W error` makes every `UnsupportedIndexedMatch` warning fatal, the flag is +checked rather than nominal: a later indexed match fails the gate. + +From 2026-11-01 the flag was waived (W-1, link:docs/proof-debt.adoc#waivers[]). +Every clause that matched on an indexed relation needed constructor injectivity, +which Cubical Agda does not support. Two re-representations closed it: + +* *The order* (2026-11-01). `_⊑_` became a computed predicate + (`L ⊑ _ = ⊤`, `H ⊑ L = ⊥`), so the order laws hold by computation. +* *`just`-injectivity* (2026-11-09). The 13 remaining warnings, in `tini`, `go`, + `confine` and `confineW`, came from matching `refl : just s ≡ just t`. The + clauses now take the equation as a variable and use `Prelude.just-inj`, which + is `cong` of a total projection and never matches on that equation. No theorem + statement changed, and the fuel semantics is untouched: the relational + big-step semantics that W-1 named as the way out, and its consequence for N-5, + are not needed. + +The receipt records `cubical-compatible = "met"`. === What the grade is anchored to @@ -118,9 +113,10 @@ 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. +link:docs/proof-debt.adoc[] — all four empty, and enforced rather than asserted. +Its `#waivers` section is empty of open waivers. It keeps W-1 +(`--cubical-compatible`) as retired, with the evidence for the waiver and the +re-representations that closed it. CI: the whole gate — core proofs, expected rejections, the laws certificate, the receipt drift check and the receipt emit — is green on `8e421cc`, run diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc index 015ee881..a3b1c13b 100644 --- a/docs/proof-debt.adoc +++ b/docs/proof-debt.adoc @@ -99,14 +99,16 @@ in the place a reader will look. Each one names the obligation, the tool, and wh 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) — RETIRED 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. +*State.* **Met.** Since 2026-11-09 the gate (`scripts/proof-flags.sh`) runs the +canonical invocation with `--no-libraries --ignore-interfaces --double-check +-W error`, so a new `UnsupportedIndexedMatch` fails the gate rather than being +waived. The record below is kept as the history of the waiver: what was +measured, which arm was taken, and what closed it (*Closed*, after the arms). *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 @@ -165,14 +167,27 @@ report why it would not stay.* The flag was added, the Agda pin was unchanged 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. + +*Closed, 2026-11-09: B2 without the relational semantics.* The 13 warnings did +not need the change B2 described. Each came from a clause that matched +`refl : just s ≡ just t`. Those clauses now take the equation as a variable and +apply `Prelude.just-inj`, defined as `cong (from-just a)` for a total projection +`from-just`. `cong` matches `refl` only against a variable, so no clause asks +for the injectivity of `just`. Agreement then follows by `subst`/`subst₂`, or +from a store equality (`≈-from-≡`). No theorem statement changed, the fuel +semantics is untouched, and N-5 keeps its `nothing`-returning witness. B2's +"threading the result as a variable" probe failed because the clauses still +matched `refl` on two constructor terms inside; the projection is what removes +that match. With all 13 warnings gone, the flag joined the gate: `SecretTypes.All` +checks under the canonical invocation with `--double-check -W error`, and the +receipt records `cubical-compatible = "met"`. + +*What would have made the waiver wrong.* Suppressing `-WUnsupportedIndexedMatch` +in the gate would have made the flag nominally on and the check off. The gate +never did, and it now keeps `-W error` with the flag on, so the same rule now +guards the met obligation. + +*Consequence for the grade.* None at the time. mathesis Grade 3 was "type-checks +locally in Agda under strict flags, not translated", so the waiver did not lower +it. Under PROOF-POLICY §8 the grade is derived from the receipt, which now +records the §2.1 invocation in full. diff --git a/scripts/grade-receipt.sh b/scripts/grade-receipt.sh index d3cf09b8..e8c35cb4 100755 --- a/scripts/grade-receipt.sh +++ b/scripts/grade-receipt.sh @@ -122,8 +122,7 @@ emit() { 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 ' :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 :waiver-history "docs/proof-debt.adoc#waivers (W-1, retired)"\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 ' ')" diff --git a/scripts/proof-flags.sh b/scripts/proof-flags.sh index da3c25fe..e766b668 100755 --- a/scripts/proof-flags.sh +++ b/scripts/proof-flags.sh @@ -20,17 +20,15 @@ # --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. Waived from 2026-11-01 (W-1) until +# the last indexed matches were re-represented: the +# order is a computed predicate, and `just`-injectivity +# goes through `cong` of a total projection +# (Prelude.just-inj), never a match on +# `refl : just s ≡ just t`. -W error makes any +# -WUnsupportedIndexedMatch fatal, so a later indexed +# match fails the gate rather than weakening it. +# History: docs/proof-debt.adoc#waivers. # --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..b4acc624 100644 --- a/src/SecretTypes/Noninterference/Generic.agda +++ b/src/SecretTypes/Noninterference/Generic.agda @@ -44,6 +44,10 @@ module _ (V : Observer 𝓛) where _≈_ : Store → Store → Set s ≈ s' = s ≈[ sees ] s' + -- Equal stores agree for V. + ≈-from-≡ : ∀ {s s'} → s ≡ s' → s ≈ s' + ≈-from-≡ refl _ _ = refl + -- Reverse agreement for V, without requiring the stores to be equal. ≈-sym : ∀ {s s'} → s ≈ s' → s' ≈ s ≈-sym p x v = sym (p x v) @@ -95,8 +99,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 = ≈-from-≡ (sym (just-inj e)) + confine fuel {s} np (assign {x = x} {e = e} ok) r = subst (λ u → u ≈ s) (just-inj r) (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 +112,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 = ≈-from-≡ (sym (just-inj e)) confineL zero np t () confineL {e = g} (suc fuel) {s} np t e = confineW fuel (eval s g) np t e @@ -140,8 +144,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' = subst₂ _≈_ (just-inj e) (just-inj e') eq + tini fuel fuel' (assign {x = x} {e = g} ok) eq e e' = subst₂ _≈_ (just-inj e) (just-inj 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 +174,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' = subst₂ _≈_ (just-inj e) (just-inj 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..8ffa3b72 100644 --- a/src/SecretTypes/Prelude.agda +++ b/src/SecretTypes/Prelude.agda @@ -34,24 +34,36 @@ cong₂ f refl refl = refl -- Transport evidence for the predicate P along an equality of its indices. subst : {A : Set} (P : A → Set) {a b : A} → a ≡ b → P a → P b subst P refl p = p +-- Transport evidence for a two-place predicate along equalities of both indices. +subst₂ : {A B : Set} (P : A → B → Set) {a a' : A} {b b' : B} → a ≡ a' → b ≡ b' → P a b → P a' b' +subst₂ P refl refl p = p 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`, cubical-compatibly. The lemma defined by matching +-- (`just-inj (refl) = refl`, deleted 2026-11-01 as dead code) is refused under +-- the canonical flag set (scripts/proof-flags.sh, --cubical-compatible per +-- PROOF-POLICY §2.1): -- -- 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. +-- and so was every clause of the TINI proof that matched `refl : just s ≡ just t` +-- (docs/proof-debt.adoc W-1, retired). This version never matches on that +-- equation: it applies `cong` to a total projection, and `cong` matches `refl` +-- only against a variable. `from-just d` returns the payload, or d for nothing. +-- Suppressing the warning, or dropping the flag, would have bought a green gate +-- with a weaker check; this is the cubical-compatible formulation instead. +from-just : {A : Set} → A → Maybe A → A +from-just d nothing = d +from-just _ (just a) = a + +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. diff --git a/verification/receipts/agda-grade3_praxis.deed b/verification/receipts/agda-grade3_praxis.deed index 6675ed77..07c6135d 100644 --- a/verification/receipts/agda-grade3_praxis.deed +++ b/verification/receipts/agda-grade3_praxis.deed @@ -13,22 +13,21 @@ :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" :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" + :waiver-history "docs/proof-debt.adoc#waivers (W-1, retired)" :stronger-than-canonical ("--no-libraries" "--ignore-interfaces" "--double-check" "-W error")) (gate :command "bash scripts/check.sh" @@ -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 "f969be56a8ce37526413ea7412c19368c04a018f655e9ca1b7e015323d32ff0c") (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 "efb8be7faab3798ec6da7c315fd9903cc6112bce98194a8463fbae9f52df6eee") (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 fc202817863854a451a8b09ab8d034effe0180f3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:42:46 +0000 Subject: [PATCH 2/2] proofs: cite the --cubical-compatible CI run; derive conformance from the flags PROOF-STATUS cited run 41327614303 on 8e421cc as evidence for the whole gate, but that run predates --cubical-compatible. It now cites run 42633550884 on b64974c (pinned Agda 2.6.4.3, the flag in force) as branch evidence, says the merge run on main is what the receipt rests on, and keeps the earlier run for the two changes it did evidence. grade-receipt.sh wrote :cubical-compatible "met" unconditionally; it now reads the value off the flags the gate runs, so dropping the flag yields "absent" and --check reports the drift (checked: exit 1). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg --- PROOF-STATUS.adoc | 21 +++++++++++++++------ scripts/grade-receipt.sh | 8 +++++++- 2 files changed, 22 insertions(+), 7 deletions(-) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index f6e805e6..683d307f 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -118,12 +118,21 @@ Its `#waivers` section is empty of open waivers. It keeps W-1 (`--cubical-compatible`) as retired, with the evidence for the waiver and the re-representations that closed it. -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. +CI: the whole gate, under the flags above with `--cubical-compatible`, is green +on `b64974c` under the pinned Agda 2.6.4.3, run +link:https://github.com/hyperpolymath/secret-types/actions/runs/42633550884[42633550884]. +The gate covers the core proofs, the expected rejections, the laws certificate, +the receipt drift check and the receipt emit. That run was on the branch of +hyperpolymath/secret-types#30. A later commit on that branch changed only these +records and the receipt generator, not the proof sources or the flags. The first +green `proofs.yml` run on `main` after the merge is the run the receipt rests on. + +Earlier run, kept as the evidence for what it showed: run +link:https://github.com/hyperpolymath/secret-types/actions/runs/41327614303[41327614303] +on `8e421cc`, under the flags *without* `--cubical-compatible`. It is the +evidence for the two Agda changes the 2026-11-01 flag attempt forced (`just-inj` +removed as dead code, `_≟_` re-expressed through `pred`), which is why those +changes are recorded rather than quietly folded in. == Fragment (stated before the claims) diff --git a/scripts/grade-receipt.sh b/scripts/grade-receipt.sh index e8c35cb4..1e114b04 100755 --- a/scripts/grade-receipt.sh +++ b/scripts/grade-receipt.sh @@ -69,6 +69,12 @@ source_commit="${commit_override:-$(git rev-parse --short=12 HEAD 2>/dev/null || agda_version="$(proof_agda_pin)" agda_from="$(proof_agda_provenance)" flag_line="$(proof_flags_line)" +# Conformance is read off the flags the gate actually runs, never written by +# hand: drop the flag and the receipt says "absent", so --check reports drift. +case " $flag_line " in + *" --cubical-compatible "*) cubical_compatible="met" ;; + *) cubical_compatible="absent" ;; +esac # Print the Agda module paths under src/SecretTypes in sorted order. modules() { find src/SecretTypes -name '*.agda' | LC_ALL=C sort; } @@ -122,7 +128,7 @@ emit() { 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 ' :canonical-invocation "agda --safe --without-K --cubical-compatible"\n' - printf ' :cubical-compatible "met"\n :waiver-history "docs/proof-debt.adoc#waivers (W-1, retired)"\n' + printf ' :cubical-compatible "%s"\n :waiver-history "docs/proof-debt.adoc#waivers (W-1, retired)"\n' "$cubical_compatible" 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 ' ')"