hyperpolymath · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026
@@ -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)
 

@@ -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 <module>` 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.
@@ -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 ' ')"

@@ -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 \

@@ -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')))
@@ -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.