experiment: syntax-directed typing judgement (computed by recursion on Cmd) instead of an indexed family #31

Why

The typing judgement _⊢_ : Carrier → Cmd → Set (SecretTypes.Typing.Generic) is an indexed family. The type system is syntax-directed (one rule per command form), so the judgement could instead be a computed predicate, defined by recursion on the command:

_⊢_ : Carrier → Cmd → Set
pc ⊢ skip          = ⊤
pc ⊢ (x ≔ e)       = (pc ⊔ lab e) ⊑ label x
pc ⊢ (c₁ ﹔ c₂)    = pc ⊢ c₁ × pc ⊢ c₂
pc ⊢ (ifz e c₁ c₂) = (pc ⊔ lab e) ⊢ c₁ × (pc ⊔ lab e) ⊢ c₂
pc ⊢ (while e c)   = (pc ⊔ lab e) ⊢ c

This is the same move that turned _⊑_ into a computed predicate (W-1, arm B1).

What prompted it

#30 retires W-1, and the --cubical-compatible work in its downstream consumer metadatastician/lintel hit the indexed judgement directly. lintel's writes-flow walks a typing derivation together with another family indexed by the same command (Writes x k c). Lining the two up needs injectivity of the Cmd constructors (_≔_), which Cubical Agda does not support. lintel works around it locally with an inversion function inv : pc ⊢ c → Inv pc c, whose result type is computed by recursion on the command. That workaround is a hand-written copy of the computed judgement above. A syntax-directed judgement in secret-types would make it unnecessary for every consumer.

Owner's framing (2026-11-09)

Recorded as an experiment with some priority, because in the long term it could be powerful. It is not a change to slip into a flag fix.

Why it might be powerful (to test, not assume)

• No indexed matching anywhere. Derivations become tuples and witnesses of the order, so every proof over typing is cubical-compatible by construction, and stays computing under transports.
• Typing becomes decidable for free. _⊢?_ follows from _⊑?_ by structural recursion, so a type checker is a proof term and needs no separate soundness argument.
• Consumers get inversion for free. lintel's inv and Inv disappear, and so would any other consumer's.
• It may transport better to Rocq and Lean, as Fixpoint/def rather than an inductive predicate, and that is the §2 recheck path to PWG-2i/PWG-2ii. Unverified; part of the experiment.

Costs and risks to measure

• Witnesses lose their constructor names (assign ok becomes ok, and seq t₁ t₂ becomes t₁ , t₂), much as B1 cost Countermodels.NoDownClosure its index pinning. The four rejection fixtures must still fail at their invalid declaration, for the stated reason.
• Inference. A computed pc ⊢ c is not injective, so implicit pc/c may stop being inferred at call sites. Count the annotations needed.
• Proof shape. tini and confine recurse on the derivation today. They would recurse on c and project, which is a different induction principle, and termination must still be structural.
• Downstream. lintel is the known consumer. Its writes-flow, link-written-to-client and accept/reject fixtures must keep passing, with inv deleted.

Proposed experiment (bounded, before any merge)

1. On a branch, define the computed _⊢_ beside the indexed one, plus a two-way equivalence ⊢-iso : (pc ⊢ᵢ c) ↔ (pc ⊢ c). That shows the two say the same thing before anything switches.
2. Port Noninterference.Generic to the computed judgement. Record the diff size, the annotations added, and whether --double-check -W error stays green under --cubical-compatible.
3. Re-run lintel's gate against the branch with inv removed.
4. Report a table: lines changed, annotations, gate results, fixture behaviour, and an assessment of the Rocq/Lean transport. Then a go/no-go for the owner.

Acceptance for the experiment (not for adoption)

• The equivalence lemma is proved, --safe --without-K --cubical-compatible -W error.
• Measurements recorded on this issue, both arms labelled (keep the indexed family, or switch), with the most elegant and correct arm marked, per doctrine 15.

Not in scope

Changing any theorem statement (N-1…N-9) or the fuel semantics.