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

.github/workflows/lean.yml

@@ -0,0 +1,40 @@
+name: Lean
+
+on:
+  push:
+    branches:
+      - master
+      - rewrite
+  pull_request:
+    paths:
+      - 'lean/**'
+      - '.github/workflows/lean.yml'
+
+# Not a required status check. If it becomes one, the workflow-level `paths:` filter
+# above has to go and be replaced with the job-level `dorny/paths-filter` pattern
+# used by `rust.yml` -- see the comment at the top of that file for why.
+
+permissions:
+  contents: read
+
+jobs:
+  lean:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1
+
+      # Installs the toolchain named in `lean/lean-toolchain` and caches the build.
+      # `lake test` runs the same binary (see `testDriver` in `lean/lakefile.toml`);
+      # the explicit step below is kept so the check names appear in the log.
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
+        with:
+          lake-package-directory: lean
+          build: true
+          test: false
+          use-mathlib-cache: false
+
+      # The model checks itself and exits nonzero on any disagreement, so this step
+      # is the one that makes the job mean something.
+      - name: run the reference model
+        working-directory: lean
+        run: lake exe oracle

REWRITE.md

@@ -204,13 +204,13 @@ definition for everyone else.
 ```
 ic_principal                    (existing; unchanged, already correctly split)
    ↑
-candid_types      Type, Label, Field, Function, TypeEnv, field-id hash.
-                  no_std-capable. No serde, no binary, NO GLOBAL STATE.
+candid_types      Slot, Composite, TypeTable, TypeRef, FieldId, ClosedType,
+                  field-id hash. no_std-capable. No serde, no binary, NO GLOBAL STATE.
    ↑
 candid_subtype    Subtyping + coercion decision procedures. Mirrors Lean 1:1.
    ↑               The verified core: small, pure, Aeneas-shaped.
 candid_wire       Type table + memory encoding, untyped:
-   ↑               bytes <-> (TypeEnv, Vec<Type>, values). Cost metering.
+   ↑               bytes <-> (TypeTable, Vec<Slot>, values). Cost metering.
    ├───────────────────────────┐
 candid_value                candid (facade) + derive macro
    IDLValue equivalent,     CandidType trait, native decode trait (no serde),
@@ -325,17 +325,18 @@ serde-style generic traits, so today's decoder is out of reach regardless. But
 
 ## 5. Proposed working model
 
-**Everything is additive.** New code goes in the three new directories. Existing
-files are not modified. This is not a style preference — it is the property that
-makes everything else work:
+**Everything is additive.** Work is confined to the three new directories — plus this
+document, which is where the plan itself gets corrected. **Nothing under `rust/`,
+`spec/`, `test/`, `coq/` or `tools/` is touched.** This is not a style preference — it
+is the property that makes everything else work:
 
 - Nothing on `master` can break, because nothing on `master` references the new
   directories.
 - There are **structurally zero merge conflicts** with a `master` that keeps
   shipping 0.10.x releases.
-- Therefore review of a merge is *"adds files under `lean/`, `crates/`,
-  `conformance/`; touches nothing existing; nothing published depends on it"* —
-  approvable in minutes without deep review.
+- Therefore review of a merge is *"changes only `lean/`, `crates/`, `conformance/` and
+  `REWRITE.md`; nothing published depends on any of it"* — approvable in minutes
+  without deep review.
 
 **Working branch, merged fortnightly.** Day-to-day work happens on a working
 branch pushed directly, so iteration is not gated on review latency. It merges to
@@ -347,10 +348,24 @@ this experiment and lost. The `next` branch in this repository is **1 commit ahe
 of `master` and 109 behind.** It was the same plan. It died from merge cadence, not
 from a bad idea. A missed merge is a bug.
 
-**Policy lands on `master` through normal PRs.** Anything that is policy, or that
-`master` needs to know about — directory reservations, this document, CI jobs,
-CONTRIBUTING changes — goes through the standard process. Only code churn lives on
-the branch.
+**The three new directories belong to the working branch, in full.** Everything under
+[lean/](lean/), [crates/](crates/) and [conformance/](conformance/) is working-branch
+material — not only code, but the `README.md` and `CLAUDE.md` files in them. Design
+decisions get recorded next to the thing they constrain, at the moment they are made,
+because a decision that has to wait for a policy review is a decision that gets made
+in someone's head and written down later, or not at all.
+
+**Policy is what lives outside those three directories.** This document, `.github/`,
+`CONTRIBUTING`, and the deletion PRs in §6 go to `master` through the standard
+process. One carve-out: a CI workflow that gates only the new directories may ride the
+working branch so that it actually runs while the code is being written, and reach
+`master` with the next merge — it cannot affect any existing check, because its path
+filter matches nothing that exists on `master` today.
+
+The boundary is *location*, not subject matter, which makes it decidable by looking at
+a diff rather than by arguing about what counts as policy. It is also the same property
+the rest of this section rests on: a merge that only adds files under the three new
+directories cannot break `master`.
 
 **Unstable means unstable.** Nothing under the new directories is published, and
 nothing in it carries a compatibility promise until v1. Ugly intermediate states
@@ -365,11 +380,32 @@ Deletion is a normal PR against `master` with the evidence in the description.
 
 | Delete | When | Caveat |
 |---|---|---|
-| [coq/](coq/) | Lean reproduces every MiniCandid theorem **and** the two models have been diffed | If Lean disagrees with MiniCandid anywhere, that disagreement is the most valuable thing this project will find. Investigate before deleting. |
+| [coq/](coq/) | Every MiniCandid theorem's *purpose* is covered — see below | Not a model-to-model diff; the two are not comparable artifacts. |
 | [spec/](spec/) | Verso output covers all normative content | `spec/Candid.md` is externally linked from docs sites, other implementations, and papers. Needs a redirect stub, not a `git rm`. |
 | [test/](test/) | All 471 assertions exist as conformance vectors and pass | — |
 | [rust/](rust/) | `candid` v1 published and icp-cli + ic-cdk migrated | Long horizon. Expect 0.10.x maintenance in parallel throughout. |
 
+### What the `coq/` condition means
+
+An earlier version of this table asked that Lean "reproduce every MiniCandid theorem
+**and** the two models have been diffed." That was wrong on both halves, because it
+treated the two as the same kind of artifact differing only in coverage.
+
+MiniCandid is not an incomplete implementation. It is a **justification** device: it
+exists to show that non-obvious design decisions — the `opt` coercion rule above all —
+are sound, and to check that a proposed spec change can be accommodated by the existing
+system. The Lean model answers a different question: given this input, what happens?
+
+So the condition is that each MiniCandid theorem's *purpose* is discharged. For each
+one, either the property is stated and proved about the Lean definitions, or it is
+recorded as a justification the Lean model subsumes. And because the two use different
+representations — MiniCandid's types are `CoInductive` infinite trees, Lean's are finite
+with an explicit type table — there is no structural diff to perform.
+
+What is still worth doing, and is *not* a deletion gate: checking the two against each
+other on the nine constructors they share. A disagreement there would be a finding about
+the spec, and finding it is worth more than the deletion.
+
 ### Tools
 
 `tools/` is not on the ratchet above; each entry has its own disposition.

crates/CLAUDE.md

@@ -58,7 +58,7 @@ Name uniquification uses an incrementing counter, so generated `.did` type names
 depend on the order types were first derived in that thread.
 
 Type derivation must be a pure function. Types are built into an explicit
-`TypeEnv` passed by the caller; recursion uses arena indices, not thread-local
+`TypeTable` passed by the caller; recursion uses arena indices, not thread-local
 interning.
 
 The derive crate has the same defect in a worse place: `candid_method` /
@@ -101,6 +101,12 @@ decode_one_with_skipping_quota, decode_one_with_decoding_and_skipping_quota,
 Write names out. Options go in a config struct or a builder, never into the
 function name.
 
+The core type names are already settled, and are shared with [`lean/`](../lean/) so the
+two read alike — see [README.md](README.md#naming). In particular `TypeTable` is the
+index-keyed table and `TypeEnv` is reserved for the name-keyed `.did` declaration
+environment; do not reuse `TypeEnv` for the former, which is the mistake `rust/`
+makes.
+
 ### 5. No `unsafe` in `candid_subtype` or `candid_wire`
 
 These two crates are the verification target. No `unsafe`, no interior

crates/README.md

@@ -19,13 +19,13 @@ crates below are new, and they use `_` to match the existing family.
 ```
 ic_principal                    (existing crate; unchanged, already correctly split)
    ↑
-candid_types      Type, Label, Field, Function, TypeEnv, field-id hash.
-                  no_std-capable. No serde, no binary, no global state.
+candid_types      Slot, Composite, TypeTable, TypeRef, FieldId, ClosedType,
+                  field-id hash. no_std-capable. No serde, no binary, no global state.
    ↑
 candid_subtype    Subtyping + coercion decision procedures.
    ↑              Mirrors lean/ 1:1. The verified core.
 candid_wire       Type table + memory encoding, untyped:
-   ↑              bytes <-> (TypeEnv, Vec<Type>, values). Cost metering.
+   ↑              bytes <-> (TypeTable, Vec<Slot>, values). Cost metering.
    ├───────────────────────────┐
 candid_value                candid (facade) + derive macro
    Dynamic value repr,      CandidType trait, native decode trait (no serde),
@@ -45,7 +45,7 @@ out of tree:      candid_bindgen_{rust,js,ts,motoko}
   ([rust/candid/src/types/internal.rs:692](../rust/candid/src/types/internal.rs#L692)),
   which makes `CandidType::ty()` impure and makes generated `.did` type names
   depend on the order types were first derived. Here, types are built into an
-  explicit `TypeEnv` passed by the caller, with recursion handled by arena indices.
+  explicit `TypeTable` passed by the caller, with recursion handled by arena indices.
 - **`candid_subtype` is a separate crate** specifically so the Lean-mirrored
   surface has a crate boundary. As a module inside something larger, the
   correspondence rots silently.
@@ -58,6 +58,43 @@ out of tree:      candid_bindgen_{rust,js,ts,motoko}
   fine-grained without forcing ten dependencies into every canister's
   `Cargo.toml`.
 
+## Naming
+
+Identifiers are shared with [lean/](../lean/) wherever they name the same thing. That
+is what turns "`candid_subtype` should read as a transcription of its Lean
+counterpart" into a checkable property rather than an aspiration.
+
+| | |
+|---|---|
+| `Slot` | a `<datatype>` where the wire format writes `I`: a primitive or a `TypeRef`, never an inline composite |
+| `Composite` | a `<comptype>`: what a table entry is. Its children are `Slot`s, so it is one flat node |
+| `TypeTable` | `TypeRef` → `Composite`, index-keyed — what the spec calls the type definition table |
+| `TypeRef` | index into a `TypeTable` |
+| `ClosedType` | a `TypeTable` and a root `Slot` together |
+| `FieldId` | a record or variant label: a 32-bit id |
+| `CandidType` | the derive trait |
+| `TypeEnv` | **reserved**, see below |
+
+`Type` cannot be used in Lean (it is the universe) and `Ty` would violate
+[CLAUDE.md](CLAUDE.md) anti-pattern 4, so "Type" is a family prefix and never a whole
+name.
+
+`Slot` and `Composite` take no such prefix, because neither is a type: a slot cannot
+express one, and a composite means nothing without the table its children index into.
+Both are named after the grammar position they occupy in `spec/Candid.md`. Nothing
+here is a nested tree — the type table is the only recursion, which is what the wire
+format already does (`spec/Candid.md:1208`) and what makes the subtype procedure in
+[lean/](../lean/) terminate without a depth limit.
+
+`TypeEnv` is deliberately *not* this crate's table. In `rust/` it is a
+`BTreeMap<String, Type>`
+([rust/candid/src/types/type_env.rs:7](../rust/candid/src/types/type_env.rs#L7)) — a
+*name*-keyed environment of `.did` type declarations, which is a different structure
+from an index-keyed table, and both will exist here. The name stays reserved for the
+`candid_syntax` one, where "environment" is accurate. Spending it on the table is how
+the earlier draft of this document ended up describing a "type table" that no
+identifier called a table.
+
 ## The serde divorce
 
 This is the change that motivates the version bump, so it is worth stating
@@ -76,7 +113,7 @@ The replacement makes backtracking first-class:
 
 ```rust
 pub trait CandidType: Sized {
-    fn ty(env: &mut TypeEnv) -> TypeRef;
+    fn ty(table: &mut TypeTable) -> TypeRef;
     fn encode<E: Encoder>(&self, e: E) -> Result<(), E::Error>;
 
     /// Returns Ok(None) when the wire value cannot be coerced to Self.

lean/.gitignore

@@ -0,0 +1 @@
+/.lake/

lean/Candid.lean

@@ -0,0 +1,11 @@
+/-
+Candid reference model.
+
+The ordering rule from README.md: executable first, proved second. Every definition
+here is reachable from the `oracle` executable, or a proof about something that is.
+-/
+
+import Candid.Hash
+import Candid.Types
+import Candid.Subtype
+import Candid.SubtypeSpec

lean/Candid/Hash.lean

@@ -0,0 +1,34 @@
+/-
+Field identifiers and the Candid field-id hash.
+-/
+
+namespace Candid
+
+/-- A record or variant field identifier.
+
+Fields are identified by a 32-bit number. In the textual syntax that number may be
+written literally or as a name that hashes to it, and the two forms are
+*indistinguishable at the type level* -- `record { 24860 : nat }` and
+`record { ok : nat }` are the same type. So the model keys fields on `FieldId` and
+leaves names to the syntax layer, which is also what keeps field equality honest:
+two fields are equal exactly when their ids are.
+-/
+abbrev FieldId := UInt32
+
+/-- The normative field-id hash, from `spec/Candid.md`:
+
+```
+hash(id) = ( Sum_(i=0..k) utf8(id)[i] * 223^(k-i) ) mod 2^32   where k = |utf8(id)|-1
+```
+
+Evaluated in Horner form over the UTF-8 *bytes* of the name -- not its characters,
+which differ for any name outside ASCII. `UInt32` arithmetic in Lean is modular, so
+the `mod 2^32` is the type, not an operation. -/
+def hashFieldName (name : String) : FieldId :=
+  name.toUTF8.foldl (fun acc byte => acc * 223 + byte.toUInt32) 0
+
+/- The spec notes that this hash makes collisions within one record disallowed
+rather than resolved, so a record type carrying two fields with equal ids is
+malformed. Checking that is `Composite.wellFormed`'s job, not the hash's. -/
+
+end Candid