diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index da8bfbc..683d307 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,16 +113,26 @@ 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 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, 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/docs/proof-debt.adoc b/docs/proof-debt.adoc index 015ee88..a3b1c13 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 d3cf09b..1e114b0 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,8 +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 "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 "%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 ' ')" diff --git a/scripts/proof-flags.sh b/scripts/proof-flags.sh index da3c25f..e766b66 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 fe0c1d5..b4acc62 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 710fa4e..8ffa3b7 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 6675ed7..07c6135 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")