diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml new file mode 100644 index 00000000..56dd6c96 --- /dev/null +++ b/.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 diff --git a/REWRITE.md b/REWRITE.md index 95a50de1..dcd074f5 100644 --- a/REWRITE.md +++ b/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, values). Cost metering. + ↑ bytes <-> (TypeTable, Vec, 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. diff --git a/crates/CLAUDE.md b/crates/CLAUDE.md index 70f4bb5a..6e7bf2cf 100644 --- a/crates/CLAUDE.md +++ b/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 diff --git a/crates/README.md b/crates/README.md index 04d84f0d..0c58a849 100644 --- a/crates/README.md +++ b/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, values). Cost metering. + ↑ bytes <-> (TypeTable, Vec, 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 `` where the wire format writes `I`: a primitive or a `TypeRef`, never an inline composite | +| `Composite` | a ``: 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` +([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(&self, e: E) -> Result<(), E::Error>; /// Returns Ok(None) when the wire value cannot be coerced to Self. diff --git a/lean/.gitignore b/lean/.gitignore new file mode 100644 index 00000000..4080d07d --- /dev/null +++ b/lean/.gitignore @@ -0,0 +1 @@ +/.lake/ diff --git a/lean/Candid.lean b/lean/Candid.lean new file mode 100644 index 00000000..76d819a3 --- /dev/null +++ b/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 diff --git a/lean/Candid/Hash.lean b/lean/Candid/Hash.lean new file mode 100644 index 00000000..8585b2cf --- /dev/null +++ b/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 diff --git a/lean/Candid/Subtype.lean b/lean/Candid/Subtype.lean new file mode 100644 index 00000000..ae41ea7c --- /dev/null +++ b/lean/Candid/Subtype.lean @@ -0,0 +1,296 @@ +/- +Candid subtyping, as a decision procedure over two independent type tables. + +Rules are from `spec/Candid.md`, "Upgrading and Subtyping". Three things shape +everything here: two from that section, and one from how types are represented. + +**The negative premises are eliminable.** The spec states four rules for `opt`, two +of them with negative premises: + +``` + <: not ( <: ) +------------------------ --------------------------- +opt <: opt opt <: opt +``` + +Together those two say `opt t <: opt t'` unconditionally. The same pairing on the +other two rules says `t <: opt t'` whenever `not (null <: t)`, and the remaining +cases (`t` is `null`, `reserved`, or an `opt`) are covered by their own rules. So +**`t <: opt t'` holds for every `t` and `t'`** -- which the spec itself notes at the +top of those rules ("allow, in fact, *any* type to be regarded as a subtype of an +option"), and which `rust/candid/src/types/subtype.rs:293` implements as a catch-all +that only warns. + +That collapse is what makes this relation definable as a greatest fixed point at +all: negative premises are non-monotone, so the rule functional would have no gfp. +Restating them as one premise-free rule keeps the relation monotone. + +**Two tables, not one.** A `Slot` holding a `ref` is meaningless without its table, +and the case that matters most compares a type table that arrived on the wire against +the receiver's own type graph -- two unrelated tables. The current Rust signature +takes a single `env` for both types (`rust/candid/src/types/subtype.rs:19`), which +works only because callers merge tables first. + +**The table bounds the recursion.** A composite's children are slots, and composites +live only in the table (`Types.lean`), so the only way to recurse is through a pair of +*references*: every other slot pair is decided outright. The procedure carries `seen`, +the reference pairs this path has already assumed -- the coinductive hypothesis, since +meeting a recorded pair again is an obligation the greatest fixed point discharges +rather than one that failed. + +Termination is then `remaining`, the number of reference pairs `seen` has *not* +recorded. It is mentioned only by `termination_by`, so the `|A| x |B|` pair space it +counts over is never built when the procedure runs: `seen` grows by one cons per +descent and is read by a scan no longer than the current path. The two facts the +measure needs are produced where the decision is made -- the guard says the pair is +fresh, and the table lookups say its indices are in range -- so no invariant is +threaded through the recursion. +-/ + +import Candid.Types + +namespace Candid + +/-- Is this slot a type in this table at all? A primitive always is; a reference is +one exactly when it resolves. -/ +def TypeTable.resolves (t : TypeTable) : Slot → Bool + | .prim _ => true + | .ref r => (t.lookup? r).isSome + +/-- `null <: t`, decided syntactically. + +The spec's premise `not (null <: )` is only ever applied to a concrete +type, and `null` is a subtype of exactly `null`, `reserved`, and any `opt` -- so this +needs no recursion, just one step through the table. -/ +def TypeTable.acceptsNull (t : TypeTable) : Slot → Bool + | .prim .null | .prim .reserved => true + | .prim _ => false + | .ref r => match t.lookup? r with + | some (.opt _) => true + | _ => false + +/-- Label a positional list the way the spec's function rule does: "`NI*` is the +`` sequence `1`..`|*|`". -/ +def indexedFrom (i : Nat) : List Slot → List (FieldId × Slot) + | [] => [] + | t :: ts => (UInt32.ofNat i, t) :: indexedFrom (i + 1) ts + +/-- Function annotations must be equal *as sets*. The spec identifies annotation +lists "up to reordering" (`spec/Candid.md:207`); comparing them as sets also ignores +repetition, which no `.did` source produces and which changes no answer. -/ +def annotsAgree (xs ys : List FuncAnnot) : Bool := + xs.all (ys.contains ·) && ys.all (xs.contains ·) + +/-- Look up a label. -/ +def fieldAt (fs : List (FieldId × Slot)) (id : FieldId) : Option Slot := + (fs.find? (·.1 == id)).map (·.2) + +/-- Look up a method. -/ +def methodAt (ms : List (String × Slot)) (name : String) : Option Slot := + (ms.find? (·.1 == name)).map (·.2) + +/-! ## The measure + +Nothing below this heading runs. `termination_by` measures are erased, so `allPairs` +is a proof device: the procedure never materialises the pair space, it only records +the pairs it actually assumes. -/ + +/-- Every reference pair of two tables. -/ +def allPairs (A B : TypeTable) : List (TypeRef × TypeRef) := + (List.range A.size).flatMap fun i => (List.range B.size).map fun j => (i, j) + +theorem mem_allPairs {A B : TypeTable} {i j : TypeRef} + (hi : i < A.size) (hj : j < B.size) : (i, j) ∈ allPairs A B := by + simp only [allPairs, List.mem_flatMap, List.mem_map, List.mem_range] + exact ⟨i, hi, j, hj, rfl⟩ + +/-- Reference pairs of `A` against `B` that `seen` does not record. -/ +def unseen (A B : TypeTable) (seen : List (TypeRef × TypeRef)) : Nat := + (allPairs A B).countP fun p => !seen.contains p + +/-- Recording one more pair cannot raise the count. -/ +theorem unseen_cons_le (A B : TypeTable) (a : TypeRef × TypeRef) + (seen : List (TypeRef × TypeRef)) : unseen A B (a :: seen) ≤ unseen A B seen := by + apply List.countP_mono_left + intro x _ hx + simp only [List.contains_cons, Bool.not_eq_true', Bool.or_eq_false_iff] at hx ⊢ + exact hx.2 + +/-- The general fact the descent needs: a `countP` over a list drops when the +predicate flips to `false` on one member that is present, and nowhere gains. -/ +theorem countP_cons_lt [BEq α] [LawfulBEq α] {a : α} {s : List α} + (hfresh : s.contains a = false) : + ∀ {l : List α}, a ∈ l → + (l.countP fun x => !(a :: s).contains x) < (l.countP fun x => !s.contains x) + | b :: t, hmem => by + have hmono : ∀ (u : List α), + (u.countP fun x => !(a :: s).contains x) ≤ (u.countP fun x => !s.contains x) := by + intro u + apply List.countP_mono_left + intro x _ hx + simp only [List.contains_cons, Bool.not_eq_true', Bool.or_eq_false_iff] at hx ⊢ + exact hx.2 + rcases List.mem_cons.1 hmem with rfl | hmem' + · -- the head is the fresh member: now recorded, so its indicator drops 1 -> 0 + rw [List.countP_cons_of_neg (by simp), List.countP_cons_of_pos (by simpa using hfresh)] + exact Nat.lt_succ_of_le (hmono t) + · -- the fresh member is further in; the head counts on both sides or on neither + rw [List.countP_cons, List.countP_cons] + refine Nat.add_lt_add_of_lt_of_le (countP_cons_lt hfresh hmem') ?_ + by_cases hs : b ∈ s + · simp [hs] + · by_cases hab : b = a + · simp [hab] + · simp [hs, hab] + +/-- The measure `sub` descends on: reference pairs not yet assumed, counted in both +orientations. Counting both is what makes the function rule's table swap leave the +measure alone -- see `remaining_swap`. -/ +def remaining (A B : TypeTable) (seen : List (TypeRef × TypeRef)) : Nat := + unseen A B seen + unseen B A (seen.map Prod.swap) + +theorem remaining_swap (A B : TypeTable) (seen : List (TypeRef × TypeRef)) : + remaining B A (seen.map Prod.swap) = remaining A B seen := by + simp only [remaining, List.map_map, Prod.swap_swap_eq, List.map_id] + omega + +theorem remaining_cons_lt {A B : TypeTable} {i j : TypeRef} {seen : List (TypeRef × TypeRef)} + (hi : i < A.size) (hj : j < B.size) (hfresh : seen.contains (i, j) = false) : + remaining A B ((i, j) :: seen) < remaining A B seen := by + have hlt : unseen A B ((i, j) :: seen) < unseen A B seen := + countP_cons_lt hfresh (mem_allPairs hi hj) + have hle : unseen B A (((i, j) :: seen).map Prod.swap) ≤ unseen B A (seen.map Prod.swap) := by + simpa using unseen_cons_le B A (j, i) (seen.map Prod.swap) + simp only [remaining] + omega + +/-! ## The procedure + +`sub A B seen a b` decides `a <: b`, where `a`'s references resolve in `A` and `b`'s +in `B`, and `seen` holds the reference pairs this path has already assumed. `subC` is +the same +question one step in, on the composites that two references name, and `subLabels` is +the record rule, which the function rule reuses on its positional arguments and +results. + +The measures below are lexicographic on (`remaining`, phase), where the phase orders +the three so that a step which does not record a pair still descends: `subC` (2) may +call `subLabels` (1), which may call `sub` (0), which records a pair before calling +`subC` again. -/ +mutual + +def sub (A B : TypeTable) (seen : List (TypeRef × TypeRef)) : Slot → Slot → Bool + -- ` <: reserved` and `empty <: `: the top and bottom types. + -- Each checks that the *other* side is a type at all. A dangling reference is not + -- one, and granting a subtype relation without looking is the dangerous direction + -- for a compatibility gate. + | a, .prim .reserved => A.resolves a + | .prim .empty, b => B.resolves b + + -- ` <: `, plus `nat <: int`. `principal` is a primitive + -- (spec/Candid.md:80), so `principal <: principal` needs no rule of its own. + | .prim p, .prim q => p == q || (p == .nat && q == .int) + + -- A primitive against a composite: only the `opt` rule can apply, since `empty` + -- and `reserved` are decided above. + | .prim _, .ref j => + match B.lookup? j with + | some (.opt _) => true + | _ => false + + -- A composite against a primitive: only `service <: principal`. + | .ref i, .prim q => + match q, A.lookup? i with + | .principal, some (.service _) => true + | _, _ => false + + -- Two references: the only recursive case, and the only place `seen` grows. A pair + -- already in `seen` is one this path has descended through, so the coinductive + -- hypothesis discharges it rather than the recursion repeating it. + | .ref i, .ref j => + -- The three names below are underscored because the *value* ignores them: they + -- exist for the termination proof, which the unused-variable linter does not see. + match _hx : A.lookup? i, _hy : B.lookup? j with + | some x, some y => + if _hs : seen.contains (i, j) then true + else subC A B ((i, j) :: seen) x y + | _, _ => false -- dangling: not well formed +termination_by (remaining A B seen, 0) +decreasing_by + -- The three facts the measure needs, all produced by the branch itself: the pair + -- is fresh (`hs`), and each index resolves, so each is in range (`hx`, `hy`). + simp only [TypeTable.lookup?] at _hx _hy + exact Prod.Lex.left _ _ + (remaining_cons_lt (Array.getElem?_eq_some_iff.1 _hx).1 + (Array.getElem?_eq_some_iff.1 _hy).1 (by simpa using _hs)) + +/-- The rules on the composites that a pair of references names. -/ +def subC (A B : TypeTable) (seen : List (TypeRef × TypeRef)) : Composite → Composite → Bool + -- Any type is a subtype of an option. See the header: this single rule is the + -- spec's four `opt` rules with their negative premises eliminated. + | _, .opt _ => true + + | .vec x, .vec y => sub A B seen x y + + -- A record may specialise a field's type or add a field. It may also *omit* a + -- field the supertype has, provided that field accepts `null`. + | .record fs, .record gs => subLabels A B seen fs gs + + -- A variant may specialise a tag's type or drop a tag. Every tag it does carry + -- must exist in the supertype. + | .variant fs, .variant gs => + fs.all fun (id, f) => + match fieldAt gs id with + | some g => sub A B seen f g + | none => false + + -- Parameters generalise, results specialise, and both behave like tuple-shaped + -- records -- so arguments may be dropped and results added. + -- + -- The parameter premise swaps the tables, so it swaps `seen` with them: a pair + -- `(i, j)` is about `A`'s `i` and `B`'s `j`, and reading it unswapped would assert + -- something about the transposed pair -- a different, and generally false, question. + | .func args rets ann, .func args' rets' ann' => + annotsAgree ann ann' + && subLabels B A (seen.map Prod.swap) (indexedFrom 1 args') (indexedFrom 1 args) + && subLabels A B seen (indexedFrom 1 rets) (indexedFrom 1 rets') + + -- Services are records of functions: a method may be specialised or added. + | .service ms, .service ms' => + ms'.all fun (name, g) => + match methodAt ms name with + | some f => sub A B seen f g + | none => false + + | _, _ => false +termination_by (remaining A B seen, 2) +decreasing_by + -- The parameter premise swaps the tables, and `remaining` counts both orientations + -- precisely so that the swap leaves it alone. + all_goals (try rw [remaining_swap]) + all_goals exact Prod.Lex.right _ (by omega) + +/-- The record rule: every label the supertype declares is either specialised by the +subtype or omitted, and omitting it requires that it accept `null`. -/ +def subLabels (A B : TypeTable) (seen : List (TypeRef × TypeRef)) + (fs gs : List (FieldId × Slot)) : Bool := + gs.all fun (id, g) => + match fieldAt fs id with + | some f => sub A B seen f g + | none => B.acceptsNull g +termination_by (remaining A B seen, 1) +decreasing_by exact Prod.Lex.right _ (by omega) + +end + +/-- Decide `a <: b` for two types carrying their own tables. Total: along any path a +reference pair is recorded at most once, and there are finitely many. -/ +def decSubtype (a b : ClosedType) : Bool := + sub a.table b.table [] a.root b.root + +/- Note the argument order flip in the `func` case above: parameters are +contravariant, so the tables swap with the types -- and `seen` swaps with the tables. +Getting either wrong is invisible when both types share one table, which is the +second reason the two-table signature is worth the extra parameter. -/ + +end Candid diff --git a/lean/Candid/SubtypeSpec.lean b/lean/Candid/SubtypeSpec.lean new file mode 100644 index 00000000..8535ef33 --- /dev/null +++ b/lean/Candid/SubtypeSpec.lean @@ -0,0 +1,151 @@ +/- +Subtyping as a relation, mirroring `spec/Candid.md` rule for rule. + +`Subtype.lean` holds the decision procedure; this file holds what it is supposed to +decide. Keeping them apart is the point: the relation is the specification, the +procedure is the implementation, and the theorem connecting them is the obligation +that keeps them honest. `coq/MiniCandid.v` has only the relation, which is why it +cannot be a test oracle. + +The relation is a **greatest** fixed point. Recursive types are infinite when +unfolded, so `record { next : S } <: record { next : S }` must hold by consistency +rather than by a finite derivation -- exactly why MiniCandid declares +`CoInductive Subtype`. Lean 4.32 supports coinductive *predicates* (not coinductive +data types, which is why types are finite with explicit references), so the same +construction is available here. + +That is only possible because the negative premises in the spec's `opt` rules are +eliminable -- see the header of `Subtype.lean`. A rule functional with negative +premises is non-monotone and has no greatest fixed point, so `toOpt` below stands in +for all four of the spec's `opt` rules. + +Two predicates, because there are two syntactic categories: `Subty` relates `Slot`s +and `SubtyC` relates the `Composite`s that a pair of references names. The split is +not bureaucracy -- it is where the model's finiteness lives, since `SubtyC` can only +be reached through `unfold`, one reference pair at a time. + +The type tables are *indices* rather than parameters because the `func` rule swaps +them: parameter subtyping is contravariant. +-/ + +import Candid.Subtype + +namespace Candid + +mutual + +coinductive Subty : TypeTable → TypeTable → Slot → Slot → Prop where + /-- ` <: ` -/ + | prim {A B p} : Subty A B (.prim p) (.prim p) + /-- `nat <: int` -/ + | natInt {A B} : Subty A B (.prim .nat) (.prim .int) + /-- ` <: reserved` -/ + | toReserved {A B a} : Subty A B a (.prim .reserved) + /-- `empty <: ` -/ + | fromEmpty {A B b} : Subty A B (.prim .empty) b + /-- `service <: principal`. `principal` is a `` + (`spec/Candid.md:80`), so `principal <: principal` follows from `prim`. -/ + | serviceToPrincipal {A B i ms} : + A.lookup? i = some (.service ms) → Subty A B (.ref i) (.prim .principal) + /-- All four `opt` rules of the spec, collapsed: any type is a subtype of any + option, and a receiver that cannot decode the value sees `null`. Stated at both + levels because an option is reachable either as the right slot of any pair (here) + or as the right composite of a reference pair (`SubtyC.toOpt`). -/ + | toOpt {A B a j y} : B.lookup? j = some (.opt y) → Subty A B a (.ref j) + /-- References are transparent: two of them are related through their entries. + This is the only rule that reaches `SubtyC`, and the only one that consumes a + reference pair -- which is what makes the procedure's `remaining` a measure. -/ + | unfold {A B i j x y} : + A.lookup? i = some x → B.lookup? j = some y → SubtyC A B x y → + Subty A B (.ref i) (.ref j) + +coinductive SubtyC : TypeTable → TypeTable → Composite → Composite → Prop where + /-- See `Subty.toOpt`. -/ + | toOpt {A B x y} : SubtyC A B x (.opt y) + /-- `vec <: vec ` when ` <: ` -/ + | vec {A B x y} : Subty A B x y → SubtyC A B (.vec x) (.vec y) + /-- A field may be specialised or added; a field the supertype declares may be + omitted only if it accepts `null`. -/ + | record {A B fs gs} : + (∀ id g, fieldAt gs id = some g → + (∃ f, fieldAt fs id = some f ∧ Subty A B f g) ∨ + (fieldAt fs id = none ∧ B.acceptsNull g = true)) → + SubtyC A B (.record fs) (.record gs) + /-- A tag may be specialised or dropped; every tag carried must exist in the + supertype. -/ + | variant {A B fs gs} : + (∀ id f, fieldAt fs id = some f → + ∃ g, fieldAt gs id = some g ∧ Subty A B f g) → + SubtyC A B (.variant fs) (.variant gs) + /-- Parameters generalise, results specialise, both as tuple-shaped records. Note + the swapped tables in the parameter premise. The two record composites here are + synthesised, not table entries: the rule is about labelled slot lists, and + `.record` is how the spec says to compare them. -/ + | func {A B args rets ann args' rets' ann'} : + annotsAgree ann ann' = true → + SubtyC B A (.record (indexedFrom 1 args')) (.record (indexedFrom 1 args)) → + SubtyC A B (.record (indexedFrom 1 rets)) (.record (indexedFrom 1 rets')) → + SubtyC A B (.func args rets ann) (.func args' rets' ann') + /-- Services are records of functions: a method may be specialised or added. -/ + | service {A B ms ms'} : + (∀ name g, methodAt ms' name = some g → + ∃ f, methodAt ms name = some f ∧ Subty A B f g) → + SubtyC A B (.service ms) (.service ms') + +end + +/-! Smoke checks that the constructors apply as intended. These are not the +interesting theorems; they exist so that a definition which typechecks but cannot be +used gets caught here rather than when the first proof is attempted. -/ + +example (A B : TypeTable) : Subty A B .nat .int := Subty.natInt + +example (A B : TypeTable) (a : Slot) : Subty A B a (.prim .reserved) := Subty.toReserved + +/-- Any type is a subtype of an `opt`, reached through the supertype's table. -/ +example (A B : TypeTable) (a : Slot) (y : Slot) (j : TypeRef) + (h : B.lookup? j = some (.opt y)) : Subty A B a (.ref j) := Subty.toOpt h + +example (A B : TypeTable) : SubtyC A B (.vec .nat) (.vec .int) := SubtyC.vec Subty.natInt + +/-- Two references are related through their entries. -/ +example (A B : TypeTable) (i j : TypeRef) + (hi : A.lookup? i = some (.vec .nat)) (hj : B.lookup? j = some (.vec .int)) : + Subty A B (.ref i) (.ref j) := + Subty.unfold hi hj (SubtyC.vec Subty.natInt) + +/-- The empty record is a supertype of every record: the field premise is vacuous. -/ +example (A B : TypeTable) (fs : List (FieldId × Slot)) : + SubtyC A B (.record fs) (.record []) := by + apply SubtyC.record + intro id g h + simp [fieldAt] at h + +/- +The obligation this file exists to create, and the first theorem to prove: + + theorem decSubtype_iff (a b : ClosedType) : + decSubtype a b = true <-> Subty a.table b.table a.root b.root + +The statement carries no side condition, because `decSubtype` is total: every +question it is asked, it answers. + +Soundness (`true` implies `Subty`) should follow by coinduction on the procedure's +recursion, with the pairs recorded in `seen` as the coinductive hypothesis -- that is +what `seen` means, and stating it this way is what will confirm the accounting is +right. Completeness is the converse, and needs that assuming a pair already descended +through cannot manufacture a relation that the greatest fixed point excludes. + +Well-formedness may turn out to be unnecessary as a hypothesis: a dangling reference +makes the procedure answer `false`, and it equally leaves the relation with no +applicable rule, since `unfold` demands `lookup? = some`. Whether the two agree on +duplicate labels is the same question about `fieldAt` on both sides. + +Deliberately not stated with `sorry`: an unproved `theorem` in the build reads as +established once it scrolls past. The properties `coq/MiniCandid.v` establishes +(`subtyping_refl`, `subtyping_trans`, `coerce_roundtrip`, `soundness`, +`transitive_coherence`) attach to `Subty`, and are worth restating here over the full +type language rather than over MiniCandid's nine constructors. +-/ + +end Candid diff --git a/lean/Candid/Types.lean b/lean/Candid/Types.lean new file mode 100644 index 00000000..8531d0aa --- /dev/null +++ b/lean/Candid/Types.lean @@ -0,0 +1,256 @@ +/- +The Candid type language, represented finitely -- and flatly. + +`coq/MiniCandid.v` models types as a `CoInductive T` -- infinite type trees, with +recursion needing no constructor. Lean 4 accepts `coinductive` only for predicates, +and this model takes no mathlib dependency, so that representation is unavailable. It +would also be the wrong one: it cannot be executed, and it is unlike every +implementation. + +Instead recursion is explicit, through a `TypeTable` -- which is what the binary +format calls it (`spec/Candid.md`: "type definition table") and what `candid_types` +is specified to do with arena indices. + +**Nothing here is recursive except the table.** A table entry is a `Composite`; its +children are `Slot`s; and a `Slot` is a primitive or an index -- never an inline +composite. That is the wire format's own shape, not an invention of this model +(`spec/Candid.md:1208`): + +``` +I : -> i8* +I() = T() +I() = sleb128(i) where type definition i defines T() +``` + +and the spec draws the conclusion this model is built on: "Because recursion goes +through `T`, this format by construction rules out non-well-founded definitions like +`type t = t`" (`spec/Candid.md:1225`). Two things follow. + +- The rule that "the type table may only contain composite types (no ``)" + (`spec/Candid.md:1227`) is a property of the representation rather than a + well-formedness check. A decoder still has to reject a primitive opcode in an entry + position; nothing downstream has to re-check it. +- Every recursive call in the subtype procedure passes through a slot pair, so a pair + of *references* is the only way to recurse -- and the finite set of reference pairs + bounds the recursion. See `Subtype.lean`. + +The price is that a type means nothing without its table, and even `vec nat` needs an +entry. `intern`/`close` below build tables for hand-written types. The surface `.did` +syntax is nested, so the parser will produce a nested AST and flatten it here; that +flattening is also what an encoder does, so it is a component this model needs rather +than a translation it pays for. + +On the name: the implementation in `rust/` calls this a `TypeEnv`, but that `TypeEnv` +is a `BTreeMap` (`rust/candid/src/types/type_env.rs:7`) -- a *name*-keyed +environment of `.did` type declarations, which is a different structure from this +index-keyed table. Both will exist here eventually, so `TypeEnv` is reserved for the +one where "environment" is the accurate word. +-/ + +import Candid.Hash + +namespace Candid + +/-- Index into a `TypeTable`. -/ +abbrev TypeRef := Nat + +/-- ``, per the grammar at `spec/Candid.md:80` -- which includes +`principal`. Only `func` and `service` are ``s. -/ +inductive Prim where + | null | bool | nat | int + | nat8 | nat16 | nat32 | nat64 + | int8 | int16 | int32 | int64 + | float32 | float64 + | text | reserved | empty + | principal + deriving DecidableEq, Repr, Inhabited + +/-- ``. Annotations are part of a function's type, not decoration. -/ +inductive FuncAnnot where + | query | oneway | compositeQuery + deriving DecidableEq, Repr + +/-- A `` in the position where the wire format writes `I`: a primitive, or +an index into the accompanying `TypeTable`. + +This is a leaf. Composites live in the table and only in the table, so the whole +type graph is the table -- which is what bounds every recursion over types. -/ +inductive Slot where + | prim (p : Prim) + | ref (target : TypeRef) + deriving DecidableEq, Repr, Inhabited + +/-- A ``: what a table entry is. + +Not a recursive type. Its children are `Slot`s, so a composite is one flat node. -/ +inductive Composite where + | opt (inner : Slot) + | vec (inner : Slot) + | record (fields : List (FieldId × Slot)) + | variant (alts : List (FieldId × Slot)) + | func (args rets : List Slot) (annots : List FuncAnnot) + | service (methods : List (String × Slot)) + deriving Repr, Inhabited + +/-- A type table: `TypeRef` -> `Composite`. -/ +structure TypeTable where + entries : Array Composite + deriving Repr, Inhabited + +namespace TypeTable + +def size (t : TypeTable) : Nat := t.entries.size + +def lookup? (t : TypeTable) (r : TypeRef) : Option Composite := t.entries[r]? + +/-- The empty table, for types that contain no references. -/ +def empty : TypeTable := { entries := #[] } + +end TypeTable + +/-- No duplicates, by `BEq`. Used for field ids and for method names. -/ +def noDups [BEq α] : List α → Bool + | [] => true + | x :: xs => !xs.contains x && noDups xs + +/-! ## Well-formedness + +Nothing recursive is left to check. A slot's reference must resolve, and no record, +variant or service may repeat a label -- the spec is explicit that a hash collision +between field names in one record is *disallowed* rather than resolved, so duplicate +ids make a type malformed rather than ambiguous. + +Two further rules are not structural: a `oneway` function may not have results, and a +service's method type must denote a function. The second is the only rule here that +has to look through the table, since a method's type is a slot like any other. + +One rule is deliberately left out. "The list of parameters must be shorter than 2^32 +values; the same restriction apply to the result list" (`spec/Candid.md:209`) cannot +be violated by anything that fits in memory, but it is not idle: `indexedFrom` labels +positional arguments with `UInt32`, which wraps, so it is that bound that keeps the +labels of a function's arguments distinct. -/ + +/-- Does this slot's reference resolve below `bound`? -/ +def Slot.wellFormed (bound : Nat) : Slot → Bool + | .prim _ => true + | .ref r => r < bound + +/-- The slots a composite holds, in no particular order: what has to resolve. -/ +def Composite.slots : Composite → List Slot + | .opt t | .vec t => [t] + | .record fs | .variant fs => fs.map (·.2) + | .func args rets _ => args ++ rets + | .service ms => ms.map (·.2) + +/-- Labels must not repeat. Vacuous for the unlabelled composites. -/ +def Composite.labelsOk : Composite → Bool + | .record fs | .variant fs => noDups (fs.map (·.1)) + | .service ms => noDups (ms.map (·.1)) + | .opt _ | .vec _ | .func _ _ _ => true + +/-- `spec/Candid.md:211`: "The result list of a `oneway` function must be empty." -/ +def Composite.annotsOk : Composite → Bool + | .func _ rets ann => !ann.contains .oneway || rets.isEmpty + | .opt _ | .vec _ | .record _ | .variant _ | .service _ => true + +def Composite.wellFormed (bound : Nat) (c : Composite) : Bool := + c.labelsOk && c.annotsOk && c.slots.all (Slot.wellFormed bound) + +/-- `spec/Candid.md:1223`: "The serialised data type representing a method type must +denote a function type." -/ +def TypeTable.methodsDenoteFuncs (t : TypeTable) : Composite → Bool + | .service ms => ms.all fun (_, s) => + match s with + | .ref r => match t.lookup? r with + | some (.func _ _ _) => true + | _ => false + | .prim _ => false + | .opt _ | .vec _ | .record _ | .variant _ | .func _ _ _ => true + +def TypeTable.wellFormed (t : TypeTable) : Bool := + t.entries.all fun c => c.wellFormed t.size && t.methodsDenoteFuncs c + +/-- A type together with the table its references resolve in. + +This is the unit the public API speaks in, because a `Slot` holding a `ref` means +nothing without its table. The first draft of `decSubtype` took one table and two +types, which silently assumed both came from the same table -- false in the case that +matters most, where a type table that arrived on the wire is compared against the +receiver's own type graph. -/ +structure ClosedType where + table : TypeTable + root : Slot + deriving Repr, Inhabited + +namespace ClosedType + +def wellFormed (c : ClosedType) : Bool := + c.table.wellFormed && c.root.wellFormed c.table.size + +/-- A type that needs no table. Primitives are the only types that need none, so +every type this builds is well formed. -/ +def ofPrim (p : Prim) : ClosedType := { table := .empty, root := .prim p } + +end ClosedType + +/-! ## Building tables + +A hand-written type has to have its composites interned, since only the table can +hold them. This is the same interning an encoder does when it emits a type table. -/ + +/-- Table construction: append entries, taking back the slot that names each. -/ +abbrev TableM := StateM (Array Composite) + +/-- Add an entry, and return the slot that names it. -/ +def intern (c : Composite) : TableM Slot := do + let entries ← get + set (entries.push c) + return .ref entries.size + +/-- Run a construction into the type its resulting slot names. -/ +def close (m : TableM Slot) : ClosedType := + let (root, entries) := m.run #[] + { table := { entries := entries }, root := root } + +/-- The common case: one entry, named by the root. -/ +def closeOne (c : Composite) : ClosedType := close (intern c) + +/-! Abbreviations for the primitives, so examples read like Candid rather than +like an AST. -/ + +namespace Slot + +def null : Slot := .prim .null +def bool : Slot := .prim .bool +def nat : Slot := .prim .nat +def int : Slot := .prim .int +def nat8 : Slot := .prim .nat8 +def nat16 : Slot := .prim .nat16 +def nat32 : Slot := .prim .nat32 +def nat64 : Slot := .prim .nat64 +def int8 : Slot := .prim .int8 +def int16 : Slot := .prim .int16 +def int32 : Slot := .prim .int32 +def int64 : Slot := .prim .int64 +def float32 : Slot := .prim .float32 +def float64 : Slot := .prim .float64 +def text : Slot := .prim .text +def reserved : Slot := .prim .reserved +def empty : Slot := .prim .empty +def principal : Slot := .prim .principal + +end Slot + +namespace Composite + +/-- A record from named fields, hashing the names. -/ +def recordOf (fs : List (String × Slot)) : Composite := + .record (fs.map fun (n, t) => (hashFieldName n, t)) + +/-- A variant from named alternatives, hashing the names. -/ +def variantOf (fs : List (String × Slot)) : Composite := + .variant (fs.map fun (n, t) => (hashFieldName n, t)) + +end Composite + +end Candid diff --git a/lean/Main.lean b/lean/Main.lean new file mode 100644 index 00000000..e56822f3 --- /dev/null +++ b/lean/Main.lean @@ -0,0 +1,406 @@ +/- +The reference executable. + +It runs a fixed set of checks and exits nonzero on any failure, so CI is actually +verifying behaviour rather than only that the model compiles. It will grow into the +differential oracle that reads conformance vectors -- at which point these checks +become the first vectors. + +Every type here carries a table, because composites live only in the table +(`Types.lean`). `atom` is a primitive, `entry` is a single composite, and +`close do ... intern ...` builds the two-or-more-entry cases. +-/ + +import Candid + +open Candid +open Candid.Slot +open Candid.Composite + +structure Check where + name : String + ok : Bool + detail : String + /-- A gap the model is known to have. Reported, but not a build failure -- and if + it starts passing, *that* is a failure, so a fix cannot land unnoticed. Nothing is + marked at the moment; the field exists so that a gap can be recorded as a check + that runs rather than as prose that does not. -/ + known : Bool := false + +/-- Record a check as a known gap rather than a requirement. -/ +def Check.asKnown (c : Check) : Check := { c with known := true } + +/-- A type that needs no table: a primitive. -/ +def atom (p : Prim) : ClosedType := .ofPrim p + +/-- A type that is one composite, named by the root. -/ +def entry (c : Composite) : ClosedType := closeOne c + +def relStr (b : Bool) : String := if b then "<:" else "!<:" + +/-- A subtype question about two types, each carrying its own table. -/ +def expectSub (a b : ClosedType) (want : Bool) (name : String) : Check := + let got := decSubtype a b + { name := name + ok := got == want + detail := s!"got {relStr got}, want {relStr want}" } + +def expectHash (input : String) (want : UInt32) : Check := + let got := hashFieldName input + { name := s!"hash {repr input} = {want}" + ok := got == want + detail := s!"got {got}" } + +def expectWellFormed (c : ClosedType) (want : Bool) (name : String) : Check := + { name := name + ok := c.wellFormed == want + detail := s!"got {c.wellFormed}, want {want}" } + +/-! ## Field-id hash + +Values computed independently from the spec formula. `"é"` is the discriminating +case: hashing UTF-8 bytes gives 43654, hashing characters would give 233. -/ + +def hashChecks : List Check := + [ expectHash "" 0 + , expectHash "Ok" 17724 + , expectHash "Err" 3456837 + , expectHash "id" 23515 + , expectHash "value" 834174833 + , expectHash "é" 43654 ] + +/-! ## Primitives, top and bottom -/ + +def primChecks : List Check := + [ expectSub (atom .nat) (atom .nat) true "nat <: nat" + , expectSub (atom .nat) (atom .int) true "nat <: int" + , expectSub (atom .int) (atom .nat) false "int !<: nat" + , expectSub (atom .nat8) (atom .nat) false "nat8 !<: nat (no width subtyping)" + , expectSub (atom .nat) (atom .nat8) false "nat !<: nat8" + , expectSub (atom .nat32) (atom .int32) false "nat32 !<: int32" + , expectSub (atom .text) (atom .reserved) true "text <: reserved" + , expectSub (entry (.func [] [] [])) (atom .reserved) true "func <: reserved" + , expectSub (atom .empty) (atom .text) true "empty <: text" + , expectSub (atom .empty) (entry (.vec nat)) true "empty <: vec nat" + , expectSub (atom .text) (atom .nat) false "text !<: nat" + , expectSub (entry (.service [])) (atom .principal) true "service <: principal" + , expectSub (atom .principal) (entry (.service [])) false "principal !<: service" ] + +/-! ## Options + +Every type is a subtype of every option -- the spec's four `opt` rules with their +negative premises eliminated. The `text <: opt nat` case is the surprising one, and +it is deliberate: a receiver that cannot decode the value sees `null`. -/ + +def optChecks : List Check := + [ expectSub (atom .nat) (entry (.opt nat)) true "nat <: opt nat" + , expectSub (atom .null) (entry (.opt nat)) true "null <: opt nat" + , expectSub (atom .reserved) (entry (.opt nat)) true "reserved <: opt nat" + , expectSub (atom .text) (entry (.opt nat)) true "text <: opt nat (special opt rule)" + , expectSub (entry (.opt text)) (entry (.opt nat)) true + "opt text <: opt nat (special opt rule)" + , expectSub (entry (.opt nat)) (atom .nat) false "opt nat !<: nat" + , expectSub (entry (.opt nat)) (atom .reserved) true "opt nat <: reserved" ] + +/-! ## Vectors -/ + +def vecChecks : List Check := + [ expectSub (entry (.vec nat)) (entry (.vec int)) true "vec nat <: vec int" + , expectSub (entry (.vec int)) (entry (.vec nat)) false "vec int !<: vec nat" + , expectSub (entry (.vec nat)) (atom .nat) false "vec nat !<: nat" ] + +/-! ## Records + +A subtype may add fields and specialise field types. It may also *omit* a field the +supertype declares, provided that field accepts `null` -- the rule that makes records +extensible in both inbound and outbound position. -/ + +/-- `record { x : nat; y : opt text }`. Two entries: the `opt` needs one of its own. -/ +def recordWithOptField : ClosedType := close do + let o ← intern (.opt text) + intern (recordOf [("x", nat), ("y", o)]) + +def recordChecks : List Check := + [ expectSub (entry (recordOf [("x", nat)])) (entry (recordOf [])) true + "record {x:nat} <: record {}" + , expectSub (entry (recordOf [("x", nat), ("y", text)])) (entry (recordOf [("x", nat)])) + true "record {x;y} <: record {x} (field added)" + , expectSub (entry (recordOf [("x", nat)])) (entry (recordOf [("x", int)])) true + "record {x:nat} <: record {x:int} (field specialised)" + , expectSub (entry (recordOf [("x", int)])) (entry (recordOf [("x", nat)])) false + "record {x:int} !<: record {x:nat}" + , expectSub (entry (recordOf [("x", nat)])) recordWithOptField true + "record {x} <: record {x; y:opt text} (omitted field accepts null)" + , expectSub (entry (recordOf [("x", nat)])) (entry (recordOf [("x", nat), ("y", reserved)])) + true "record {x} <: record {x; y:reserved}" + , expectSub (entry (recordOf [("x", nat)])) (entry (recordOf [("x", nat), ("y", text)])) + false "record {x} !<: record {x; y:text} (omitted field rejects null)" + , expectSub (entry (recordOf [("x", nat)])) (entry (recordOf [("y", nat)])) false + "record {x} !<: record {y}" ] + +/-! ## Variants + +Dual to records: a subtype may *drop* tags, and every tag it carries must exist in +the supertype. Adding tags is only sound behind an `opt`. -/ + +/-- `opt variant { ... }`. -/ +def optVariant (alts : List (String × Slot)) : ClosedType := close do + let v ← intern (variantOf alts) + intern (.opt v) + +def variantChecks : List Check := + [ expectSub (entry (variantOf [])) (entry (variantOf [("a", nat)])) true + "variant {} <: variant {a}" + , expectSub (entry (variantOf [("a", nat)])) (entry (variantOf [("a", nat), ("b", text)])) + true "variant {a} <: variant {a; b} (tag dropped)" + , expectSub (entry (variantOf [("a", nat), ("b", text)])) (entry (variantOf [("a", nat)])) + false "variant {a; b} !<: variant {a} (tag added)" + , expectSub (entry (variantOf [("a", nat)])) (entry (variantOf [("a", int)])) true + "variant {a:nat} <: variant {a:int}" + , expectSub (optVariant [("a", nat), ("b", text)]) (optVariant [("a", nat)]) true + "opt variant {a; b} <: opt variant {a} (tag added behind opt)" ] + +/-! ## Functions + +Parameters generalise, results specialise, and both behave like tuple-shaped +records. Because the parameter premise is contravariant, the two directions are not +symmetric, and it is worth spelling out which is which: + +- **Dropping** a parameter is always allowed. The premise is + `record{args'} <: record{args}`, so the supertype's parameters sit on the subtype + side of that record comparison, making a shorter parameter list the *wider* record. + A callee that ignores what the caller sends cannot break. +- **Adding** a parameter requires it to accept `null`, since the premise then omits + a field the supertype declares. +- Results mirror this exactly: adding is free, dropping requires accepting `null`. + +Annotations must match as sets. -/ + +/-- `func (opt nat) -> ()`. -/ +def funcOptParam : ClosedType := close do + let o ← intern (.opt nat) + intern (.func [o] [] []) + +/-- `func () -> (opt nat)`. -/ +def funcOptResult : ClosedType := close do + let o ← intern (.opt nat) + intern (.func [] [o] []) + +def funcChecks : List Check := + [ expectSub (entry (.func [int] [nat] [])) (entry (.func [nat] [int] [])) true + "func (int) -> (nat) <: func (nat) -> (int)" + , expectSub (entry (.func [nat] [int] [])) (entry (.func [int] [nat] [])) false + "func (nat) -> (int) !<: func (int) -> (nat)" + -- Parameters: dropping is free, adding needs to accept null. + , expectSub (entry (.func [] [] [])) (entry (.func [nat] [] [])) true + "func () -> () <: func (nat) -> () (parameter dropped, always allowed)" + , expectSub funcOptParam (entry (.func [] [] [])) true + "func (opt nat) -> () <: func () -> () (optional parameter added)" + , expectSub (entry (.func [nat] [] [])) (entry (.func [] [] [])) false + "func (nat) -> () !<: func () -> () (added parameter rejects null)" + -- Results: adding is free, dropping needs to accept null. + , expectSub (entry (.func [] [nat] [])) (entry (.func [] [] [])) true + "func () -> (nat) <: func () -> () (result added, always allowed)" + , expectSub (entry (.func [] [] [])) funcOptResult true + "func () -> () <: func () -> (opt nat) (optional result dropped)" + , expectSub (entry (.func [] [] [])) (entry (.func [] [nat] [])) false + "func () -> () !<: func () -> (nat) (dropped result rejects null)" + , expectSub (entry (.func [] [] [.query])) (entry (.func [] [] [])) false + "annotations must agree" + , expectSub (entry (.func [] [] [.query])) (entry (.func [] [] [.query])) true + "matching annotations agree" ] + +/-! ## Services + +A method's type is a reference like any other -- the spec is explicit that "the +serialised data type representing a method type must denote a function type" +(`spec/Candid.md:1223`), so it is an index into the table, not an inline function. -/ + +/-- A service, interning each method type first. -/ +def serviceOf (ms : List (String × Composite)) : ClosedType := close do + let slots ← ms.mapM fun (name, c) => do return (name, ← intern c) + intern (.service slots) + +def serviceChecks : List Check := + [ expectSub (serviceOf [("m", .func [] [] [])]) (serviceOf []) true + "service {m} <: service {}" + , expectSub (serviceOf []) (serviceOf [("m", .func [] [] [])]) false + "service {} !<: service {m}" + , expectSub (serviceOf [("m", .func [] [nat] [])]) (serviceOf [("m", .func [] [] [])]) true + "service method specialised" ] + +/-! ## Well-formedness rules that are not structural + +Two rules from the spec that the shape of a `Composite` does not enforce on its own. +The second is the only rule that has to look through the table, since a method's type +is a slot like any other. -/ + +/-- `spec/Candid.md:211`: "The result list of a `oneway` function must be empty." -/ +def onewayWithResult : ClosedType := entry (.func [] [nat] [.oneway]) + +def onewayWithoutResult : ClosedType := entry (.func [nat] [] [.oneway]) + +/-- `spec/Candid.md:1223`: "The serialised data type representing a method type must +denote a function type." -/ +def serviceWithPrimMethod : ClosedType := entry (.service [("m", nat)]) + +def serviceWithVecMethod : ClosedType := close do + let v ← intern (.vec nat) + intern (.service [("m", v)]) + +def wellFormedChecks : List Check := + [ expectWellFormed onewayWithResult false "oneway with a result is malformed" + , expectWellFormed onewayWithoutResult true "oneway without results is well formed" + , expectWellFormed (entry (.func [] [nat] [.query])) true + "query with a result is well formed" + , expectWellFormed serviceWithPrimMethod false + "service method that is a primitive is malformed" + , expectWellFormed serviceWithVecMethod false + "service method that is not a function is malformed" + , expectWellFormed (serviceOf [("m", .func [] [] [])]) true + "service method that is a function is well formed" ] + +/-! ## Recursive types across two independent tables + +These are the cases the reference-pair accounting exists for. `selfLoop` and +`twoCycle` denote the same infinite type through different table shapes, so the +recursion only stops because descending through a pair of references records it in +`seen`, and meeting that pair again means the obligation is already assumed. -/ + +/-- `type S = record { next : S }`, as one self-referential entry. -/ +def selfLoop : ClosedType := + { table := { entries := #[ recordOf [("next", .ref 0)] ] }, root := .ref 0 } + +/-- The same type unrolled across two entries. -/ +def twoCycle : ClosedType := + { table := { entries := #[ recordOf [("next", .ref 1)], recordOf [("next", .ref 0)] ] } + root := .ref 0 } + +/-- `type S = record { next : S; extra : nat }`. -/ +def selfLoopWith (extra : Slot) : ClosedType := + { table := { entries := #[ recordOf [("next", .ref 0), ("extra", extra)] ] }, root := .ref 0 } + +/-- A reference with no entry to resolve to. -/ +def danglingRef : ClosedType := { table := .empty, root := .ref 3 } + +/- No check here for a primitive or a bare reference used as a table entry: an entry +is a `Composite`, so neither is representable. The spec's rule +(`spec/Candid.md:1227`) still has force, but it belongs to the decoder, which has to +reject a primitive opcode in an entry position when it parses wire bytes. -/ + +def recursiveChecks : List Check := + [ expectSub selfLoop selfLoop true + "self-loop <: itself (the reference pair is consumed once)" + , expectSub selfLoop twoCycle true + "self-loop <: two-cycle (same type, different table shape)" + , expectSub twoCycle selfLoop true + "two-cycle <: self-loop" + , expectSub (selfLoopWith nat) (selfLoopWith int) true + "recursive record, field specialised" + , expectSub (selfLoopWith int) (selfLoopWith nat) false + "recursive record, field not specialised" + , expectSub (selfLoopWith nat) selfLoop true + "recursive record with extra field <: without it" + , expectWellFormed selfLoop true "self-loop is well formed" + , expectWellFormed twoCycle true "two-cycle is well formed" + , expectWellFormed (atom .principal) true "principal is a primitive, not a reftype" + , expectWellFormed danglingRef false "dangling reference is malformed" + -- A dangling reference is not a type, so it gets neither the top nor the bottom + -- rule for free. Deliberate: `<:` reported without looking is the dangerous + -- direction for a compatibility gate. + , expectSub danglingRef (atom .reserved) false "dangling reference !<: reserved" + , expectSub (atom .empty) danglingRef false "empty !<: dangling reference" + , expectWellFormed (entry (.record [(0, nat), (0, text)])) false + "duplicate field id is malformed" ] + +/-! ## `vec`-omega: a cycle that alternates sides + +`T.0 = vec T.1` and `T.1 = vec T.0`, so both entries denote the same infinite type, +`vec (vec (vec ...))`, and the answer is `true` in both directions. + +Neither side is ever the same entry twice running, so the recursion goes `(0, 1)`, +then `(1, 0)`, then back to `(0, 1)`. Nothing is getting structurally smaller along +the way: the pair accounting is the only thing that can stop it, and it does -- the +third state finds its pair already recorded in `seen`. -/ + +def vecOmegaTable : TypeTable := { entries := #[ .vec (.ref 1), .vec (.ref 0) ] } + +def vecOmegaEven : ClosedType := { table := vecOmegaTable, root := .ref 0 } +def vecOmegaOdd : ClosedType := { table := vecOmegaTable, root := .ref 1 } + +def vecOmegaChecks : List Check := + [ expectWellFormed vecOmegaEven true "vec-omega: T.0 is well formed" + , expectWellFormed vecOmegaOdd true "vec-omega: T.1 is well formed" + , expectSub vecOmegaEven vecOmegaOdd true "vec-omega <: its own unrolling" + , expectSub vecOmegaOdd vecOmegaEven true "vec-omega's unrolling <: it" ] + +/-! ## Contravariance: `seen` swaps with the tables + +The parameter premise of the function rule swaps the two tables, so it must swap the +pair accounting with them. A pair `(i, j)` is about `A`'s `i` and `B`'s `j`; read +unswapped inside the swapped call it is about `B`'s `i` and `A`'s `j`, which is a +different question, and subtyping is not symmetric. + +The witness below reduces `contraOuter <: contraOuter'` to `contraFuncs <: +contraFuncs'`, two functions whose parameter premise asks `contraB.1 <: contraA.2`, +i.e. `vec text <: vec nat` -- false. Reaching that premise records `(1, 2)` in +`seen`, so a procedure that read `seen` unswapped would answer the premise from the +accounting instead, and both queries would come out `true`. -/ + +/-- `A.0 = record { f : A.1 }`, `A.1 = func (A.2) -> ()`, `A.2 = vec nat`. -/ +def contraA : TypeTable := + { entries := #[ recordOf [("f", .ref 1)], .func [.ref 2] [] [], .vec nat ] } + +/-- `B.0 = record { f : B.2 }`, `B.1 = vec text`, `B.2 = func (B.1) -> ()`. The +indices are deliberately transposed against `contraA`. -/ +def contraB : TypeTable := + { entries := #[ recordOf [("f", .ref 2)], .vec text, .func [.ref 1] [] [] ] } + +def contraOuter : ClosedType := { table := contraA, root := .ref 0 } +def contraOuter' : ClosedType := { table := contraB, root := .ref 0 } +def contraFuncs : ClosedType := { table := contraA, root := .ref 1 } +def contraFuncs' : ClosedType := { table := contraB, root := .ref 2 } + +def contraChecks : List Check := + [ expectWellFormed contraOuter true "contravariance witness: subtype side is well formed" + , expectWellFormed contraOuter' true "contravariance witness: supertype side is well formed" + , expectSub contraFuncs contraFuncs' false + "func (vec nat) -> () !<: func (vec text) -> () (parameter premise fails)" + , expectSub contraOuter contraOuter' false + "record { f : func (vec nat) -> () } !<: record { f : func (vec text) -> () }" ] + +/-! ## Transitivity spot-check + +The spec keeps transitivity as a design goal, and the unusual `opt` rules exist to +preserve it. This is not a proof -- it is the shape the eventual property test and +the Lean theorem take. -/ + +def transitivityChecks : List Check := + let a := entry (recordOf [("x", nat)]) + let b := recordWithOptField + let c := entry (recordOf [("x", int)]) + [ expectSub a b true "transitivity: a <: b" + , expectSub b c true "transitivity: b <: c" + , expectSub a c true "transitivity: therefore a <: c" ] + +def allChecks : List Check := + hashChecks ++ primChecks ++ optChecks ++ vecChecks ++ recordChecks ++ + variantChecks ++ funcChecks ++ serviceChecks ++ wellFormedChecks ++ + recursiveChecks ++ vecOmegaChecks ++ contraChecks ++ transitivityChecks + +def main : IO UInt32 := do + let failures := allChecks.filter (fun c => if c.known then c.ok else !c.ok) + let known := allChecks.filter (·.known) + for c in allChecks do + match c.known, c.ok with + | false, true => IO.println s!"ok {c.name}" + | false, false => IO.println s!"FAIL {c.name} -- {c.detail}" + | true, false => IO.println s!"known {c.name} -- {c.detail}" + | true, true => IO.println s!"FAIL {c.name} -- known gap now passes; promote it" + IO.println "" + if failures.isEmpty then + IO.println s!"{allChecks.length - known.length} checks passed, {known.length} known gaps" + return 0 + else + IO.eprintln s!"{failures.length} of {allChecks.length} checks failed" + return 1 diff --git a/lean/README.md b/lean/README.md index 094a2f3b..60dbb745 100644 --- a/lean/README.md +++ b/lean/README.md @@ -1,25 +1,31 @@ # `lean/` — Lean 4 reference model and specification -**Status: reserved, empty.** No content yet. See [REWRITE.md](../REWRITE.md) for -why this exists. +**Status: first slice.** Types, the field-id hash, and subtyping — as both a relation +and a decision procedure — with a self-checking executable. "Slice" is a label for +what landed in a merge window, applied after the fact; the forward-looking plan is the +coverage checklist below and the tiers in [REWRITE.md §3](../REWRITE.md#3-lean-honestly). Nothing is published and +nothing carries a compatibility promise. See [REWRITE.md](../REWRITE.md) for why this +exists. + +Eventually replaces [coq/](../coq/) and [spec/](../spec/), on the conditions in +[REWRITE.md §6](../REWRITE.md#6-the-ratchet). + +``` +lake build # build the library and the executable +lake exe oracle # run the checks; exits nonzero on any disagreement +``` ## What goes here A Lean 4 model of Candid that serves as both the **reference implementation** and, via [Verso](https://github.com/leanprover/verso), the **specification document**. -Eventually replaces [coq/](../coq/) and [spec/](../spec/). See the ratchet in -[REWRITE.md §6](../REWRITE.md#6-the-ratchet) for the conditions under which those -are deleted — in particular, `coq/` is not removed until the two models have been -diffed, because a disagreement between them would be the most valuable finding of -this project. - ## The ordering rule **Executable first, proved second.** -1. `Ty`, `Value`, `subtype`, `coerce`, and the wire format as plain Lean functions - with `Decidable` instances. +1. The type language, `Value`, `subtype`, `coerce`, and the wire format as plain + Lean functions with `Decidable` instances. 2. A `lake`-built binary that reads a conformance vector file and reports results. 3. CI wiring: that binary as a differential oracle against the Rust implementation. 4. *Only then*, proofs about those definitions. @@ -33,31 +39,164 @@ The rule that keeps it honest: > Every Lean definition must be either (a) reachable from the reference > executable, or (b) a proof about something that is. No orphan formalisation. +## What slice 1 established + +**Coinductive predicates are available; coinductive data types are not.** Lean 4.32 +accepts `coinductive` only for `Prop`-valued definitions — `coinductive T : Type` +fails with "`coinductive` keyword can only be used to define predicates." So +MiniCandid's `CoInductive Subtype : T -> T -> Prop` ports directly and lives in +[Candid/SubtypeSpec.lean](Candid/SubtypeSpec.lean), while its `CoInductive T` does +not. Types are therefore finite, with recursion through explicit references into a +type table — which is what the binary format does anyway, and what `candid_types` is +specified to do with arena indices. + +**The spec's negative premises are eliminable.** Two of the four `opt` rules in +`spec/Candid.md` carry negative premises, and a rule functional with negative +premises is non-monotone, so it has no greatest fixed point — 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'`. The spec +notes this in prose and `rust/candid/src/types/subtype.rs:293` implements it as a +catch-all that only warns. Recording it as one premise-free rule is what makes the +relation monotone. + +**Composites live only in the type table.** A table entry is a `Composite`, its +children are `Slot`s, and a `Slot` is a primitive or an index — never an inline +composite. That is not a modelling choice so much as 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`." + +What it bought: the only way for the subtype procedure to recurse is through a pair +of *references*, so the finite set of reference pairs bounds the recursion. The +procedure carries `seen` — the pairs this path has already assumed — and descends by +recording one. The measure is `remaining`, the number of pairs `seen` does *not* +record; it is named only by `termination_by`, so the `|A| x |B|` pair space it counts +over is never built at run time. No fuel, no `Option Bool`, and no "unanswered" state +in the public API. The first version of this model, with +composites nested inside each other, had no such measure: a cycle alternating which +side holds the reference dodged the memo entirely, so no budget decided it. + +What it cost: a type means nothing without its table, and even `vec nat` needs an +entry, so hand-written types are built through `intern`/`close`. The `.did` surface +syntax *is* nested, so the parser will produce a nested AST and flatten it — which is +also what an encoder does when it emits a type table, so the flattening pass is a +component this model owes rather than a translation it pays for. + +**Naming.** `Type` is unavailable in Lean (it is the universe), and abbreviating it +to `Ty` would reproduce exactly the defect +[crates/CLAUDE.md](../crates/CLAUDE.md) anti-pattern 4 names. So "Type" is the family +prefix and never the whole name: `TypeTable`, `TypeRef`, with `CandidType` left for +the Rust trait. These identifiers are meant to be **the same in Lean and in Rust**, +which is what makes "`candid_subtype` reads as a transcription of its Lean +counterpart" achievable rather than aspirational. + +The two names the flat representation introduced are borrowed from the spec's grammar +instead: a `Composite` is a ``, and a `Slot` is the `` position +that the wire format's `I` fills with either a primitive opcode or an index. Neither +is a "type" — a slot cannot express one and a composite is not meaningful without its +table — so neither takes the `Type` prefix. +[crates/README.md](../crates/README.md#naming) records the same two names for the +Rust side, since the point of sharing identifiers is that they name the same thing. + +`TypeTable` rather than `TypeEnv`, the name used in `rust/`, for two reasons. The spec +calls it a table ("type definition table", `spec/Candid.md:1311`), so the prose and the +identifier now agree — they did not when this was a `TypeEnv` described everywhere as +a table. And `TypeEnv` in `rust/` is a `BTreeMap` +(`rust/candid/src/types/type_env.rs:7`), a *name*-keyed environment of `.did` +declarations, which is a genuinely different structure from this index-keyed table. +Both will exist here eventually, so `TypeEnv` stays reserved for the one where +"environment" is the accurate word. The same names are recorded for the Rust side in +[crates/README.md](../crates/README.md#naming), because +[crates/CLAUDE.md](../crates/CLAUDE.md) asks `candid_subtype` to read as a +transcription of its Lean counterpart, and shared identifiers are most of what makes +that checkable. + +**Subtyping relates two type tables, not one.** A `Slot` holding a `ref` means +nothing without its table, so the unit the API speaks in is `ClosedType` — a table +and a root together. The case that matters most compares a type table that arrived on +the wire against the receiver's own type graph, and those are unrelated tables; +`rust/candid/src/types/subtype.rs:19` takes a single `env` for both types, which works +only because callers merge tables first. + +The consequence to keep hold of: the `func` rule's contravariance swaps the *tables* +along with the types, and therefore swaps the reference-pair accounting with the +tables — a pair `(i, j)` is about `A`'s `i` and `B`'s `j`, so reading it unswapped +asserts something about the transposed pair. Both mistakes are invisible when there +is only one table to swap, and the second one shipped in this model before the +`contra` checks in [Main.lean](Main.lean) caught it: it reported `<:` for two types +that are not related. + ## Constraints - **No mathlib.** We do not need it, and depending on it would dominate build times and breakage surface. - **Pin `lean-toolchain`.** Lean's toolchain moves faster than Coq's. Upgrades are - scheduled work, not incidental. + scheduled work, not incidental. Currently `v4.32.2`. - **Verso is young.** Expect to read its source rather than its documentation. +- **No `sorry`.** An unproved `theorem` in the build reads as established once it + scrolls past. Obligations are written as prose next to the definitions they + constrain, and become `theorem`s when they are proved. ## Coverage target The Coq model covers nine type constructors and no binary format. This model must cover what actually breaks in production: -- [ ] Primitive types, including the numeric tower and float edge cases -- [ ] Records, variants, vectors, text -- [ ] Recursive types and the type-table graph -- [ ] Subtyping, as a relation with a derived decision procedure +- [x] Primitive types — the constructors, including the numeric tower's *lack* of + width subtyping. Float edge cases belong to `Value`, which does not exist yet. +- [x] Records, variants, vectors, text — as types +- [x] Recursive types and the type-table graph +- [x] Well-formedness of types — references resolve, labels do not repeat, a `oneway` + function has no results, and a method type denotes a function +- [x] Subtyping, as a relation with a derived decision procedure - [ ] Coercion, including the `opt` backtracking rule - [ ] Binary wire format: type table, memory section, LEB128/SLEB128 - [ ] Cost model / resource exhaustion - [ ] Textual value syntax -## Prior art in this repo - -[coq/MiniCandid.v](../coq/MiniCandid.v) proves `subtyping_refl`, -`subtyping_trans`, `coerce_roundtrip`, `coerce_well_defined`, `soundness`, and -`transitive_coherence`. These are real theorems about the genuinely subtle part of -the language and they should be ported, not discarded. Read it before starting. +## Deferred, deliberately + +Named here so they are obligations rather than oversights. + +- **`decSubtype_iff`** — that the procedure decides the relation. Stated in + [Candid/SubtypeSpec.lean](Candid/SubtypeSpec.lean). Soundness should follow by + coinduction, with the pairs recorded in `seen` as the coinductive hypothesis, which + is what `seen` means. There is no longer a budget premise to discharge: the + procedure returns `Bool` and is total. +- **The pair accounting is path-scoped, and membership is a scan.** `seen` is + threaded down a path rather than shared between siblings, which is a faithful + reading of the coinductive hypothesis and is what lets the measure need no side + conditions. The cost is that `seen.contains` walks the current path, so a table of + *n* entries in one long cycle costs O(n²): measured 70 ms at 10,000 entries, 1.6 s + at 50,000, and 113 s at 400,000, with no stack overflow at any of those depths. + Sharing the accounting across siblings in a set is also sound for a greatest fixed + point and is how an implementation gets a polynomial bound; the reference model + keeps the simpler structure until a conformance vector makes that a problem. +- **Flattening the surface syntax.** A `.did` type is nested; a `Composite`'s + children are slots. The parser will need the pass that interns nested composites + into a table, and textual aliases (`type A = B;`) have to be resolved by it — + `intern`/`close` are only the hand-written-example half of that. +- **Verso.** Deliberately not yet: bundling an undocumented doc toolchain into the + work whose purpose was de-risking the build would have doubled the unknowns. + +## Relationship to `coq/` + +MiniCandid is not an incomplete implementation — it is a *justification* device. It +exists to show that non-obvious design decisions are sound, and to check that a +proposed spec change can be accommodated by the existing system. This model answers a +different question: given this input, what happens? + +[REWRITE.md §6](../REWRITE.md#what-the-coq-condition-means) now states the deletion +condition accordingly — each MiniCandid theorem's *purpose* discharged, rather than a +model-to-model diff, which is not available anyway once one side has finite types and +an explicit table. + +What remains worth doing, and is not a deletion gate: checking this model against +MiniCandid on the nine constructors they share. A disagreement there would be a +finding about the spec. + +[coq/MiniCandid.v](../coq/MiniCandid.v) proves `subtyping_refl`, `subtyping_trans`, +`coerce_roundtrip`, `coerce_well_defined`, `soundness`, and `transitive_coherence`. +These are real theorems about the genuinely subtle part of the language, they attach +to `Subty` here, and they are worth restating over records, variants, vectors and +recursion rather than over nine constructors. Read it before starting. diff --git a/lean/lake-manifest.json b/lean/lake-manifest.json new file mode 100644 index 00000000..8cfd296e --- /dev/null +++ b/lean/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "candid", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean/lakefile.toml b/lean/lakefile.toml new file mode 100644 index 00000000..fef02f3b --- /dev/null +++ b/lean/lakefile.toml @@ -0,0 +1,17 @@ +name = "candid" +version = "0.1.0" +defaultTargets = ["Candid", "oracle"] +# `lake test` runs the oracle: the model checking itself *is* the test suite. +testDriver = "oracle" + +# No mathlib, deliberately. See README.md -- it would dominate build times and +# breakage surface, and nothing here needs it. + +[[lean_lib]] +name = "Candid" + +# The reference executable. Slice 1 runs built-in examples; it will grow into the +# differential oracle that reads conformance vectors. +[[lean_exe]] +name = "oracle" +root = "Main" diff --git a/lean/lean-toolchain b/lean/lean-toolchain new file mode 100644 index 00000000..0ec5999c --- /dev/null +++ b/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.32.2