lean: the type model, subtyping, and a self-checking oracle

[lwshang]

Adds lean/: a Lean 4 model of Candid's type language and subtyping, as both a
relation and an executable decision procedure, with a self-checking binary that CI
runs. Additive only — nothing on master references any of it.

What is here

Candid/Types.lean	Slot, Composite, TypeTable, ClosedType, well-formedness
Candid/Hash.lean	the normative field-id hash
Candid/Subtype.lean	decSubtype, the decision procedure
Candid/SubtypeSpec.lean	Subty/SubtyC, the same rules as a coinductive relation
Main.lean	the oracle binary: 85 checks, nonzero exit on any disagreement
.github/workflows/lean.yml	builds and runs it (§5's CI carve-out)

lake test runs the oracle.

The three decisions that shaped it

The type table is the only recursion. A table entry is a Composite, its children
are Slots, and a Slot is a primitive or an index — never an inline composite. That
is the wire format's own shape (spec/Candid.md:1208), and the spec draws the
conclusion the model is built on: "Because recursion goes through T, this format by
construction rules out non-well-founded definitions like type t = t."

It pays for itself in the procedure. The only way to recurse is through a pair of
references, so decSubtype carries seen — the pairs this path has assumed — and
descends by recording one. Termination is remaining, the count of pairs seen does
not record; it is named only by termination_by, so the |A| × |B| pair space is
never built at run time. No fuel, no Option Bool, no "unanswered" state in the API,
and the two facts the measure needs are produced by the branch that makes the
decision. The one general lemma required is countP_cons_lt; no mathlib.

Subtyping relates two type tables, not one. A Slot holding a ref means nothing
without its table, and the case that matters most compares a table that arrived on the
wire against the receiver's own type graph. rust/candid/src/types/subtype.rs:19 takes
a single env for both, which works only because callers merge tables first.

The spec's negative premises are eliminable. Two of the four opt rules carry
negative premises, and a non-monotone rule functional has no greatest fixed point — so
the relation would not be definable coinductively at all. Pairing each negative rule
with its positive counterpart collapses them: t <: opt t' holds for every t and
t', which is what subtype.rs:293 implements as a warning-only catch-all.

Two bugs the model found in itself

The memo did not swap with the tables. The function rule's parameter premise is
contravariant, so it swaps the two tables — but it passed seen through unchanged, so
a memo of (A-index, B-index) pairs was read as (B-index, A-index). Since subtyping is
not symmetric, that answered a transposed question from the memo and reported <: for
unrelated types. The contra checks are the witness and fail without the fix.

decSubtype was roughly cubic. An earlier iteration carried the complement of
the memo, seeded with all |A| × |B| pairs and narrowed with List.erase, which
copies up to the erased element. Compiled, on a table of n entries in one cycle:
23 ms at n=100, 370 ms at n=300, 14.3 s at n=1000 — and a 1000-entry type table is
2–3 KB on the wire. Recording assumed pairs instead of carrying their complement makes
the same query <10 ms, 70 ms at n=10,000, 1.6 s at n=50,000, with no stack overflow at
400,000.

What it is checked against

• 85 checks in the oracle, covering primitives and the numeric tower's lack of
  width subtyping, the four opt rules collapsed, records, variants, functions in
  both variance directions, services, recursive types across two independent tables,
  and well-formedness.
• A differential against the pre-flat iteration of the same model: 50,000 random
  flat type pairs (expressible in both representations, so the answers must agree
  exactly) and 20,000 random nested pairs flattened into the new form. Zero mismatches
  in answers and in well-formedness.
• Properties over 20,000 random well-formed types: reflexivity, t <: reserved,
  empty <: t, and transitivity on every triple that satisfied both premises.

Well-formedness

References resolve, labels do not repeat, and two rules the shape of a Composite
does not enforce on its own: a oneway function has no results
(spec/Candid.md:211), and a service's method type denotes a function
(spec/Candid.md:1223) — the only rule that has to look through the table. The 2^32
bound on parameter lists (spec/Candid.md:209) is deliberately not checked, with the
reason recorded: it cannot be violated by anything that fits in memory, but it is what
keeps indexedFrom's UInt32 argument labels distinct.

Deliberately not here

• A type generator and conformance-vector I/O — Tiers 1–2 of REWRITE.md §3, and
  the next PR from its own branch. The generator used for the differential above lives
  outside the repo today, which is exactly why it should land as a module.
• Coercion, the binary wire format, the cost model, textual value syntax.
• Proofs. decSubtype_iff is stated as prose next to the relation, not as a sorry.
• Verso.

Files outside lean/

REWRITE.md (§5's policy boundary and what slice 1 disproved), crates/README.md and
crates/CLAUDE.md (the candid_types naming table now records Slot and
Composite), and .github/workflows/lean.yml, which §5 explicitly allows to ride the
working branch so that it runs while the code is being written.