From 70434b81324c11deb5fb52dbcc9dc8a2bd719896 Mon Sep 17 00:00:00 2001 From: Linwei Shang Date: Tue, 11 Aug 2026 09:47:09 -0400 Subject: [PATCH 1/7] lean: slice 1 -- types, field-id hash, subtyping, and a self-checking oracle First code of the rewrite. A Lean 4 model with no mathlib dependency, pinned to v4.32.2, building a library and an executable that checks itself and exits nonzero on disagreement -- so CI verifies behaviour rather than only that the model compiles. 71 checks pass. Types are finite, with recursion through an explicit TypeTable. MiniCandid represents types as a CoInductive T; Lean 4 accepts `coinductive` only for predicates, and the infinite-tree representation cannot be executed anyway. The table is what the binary format does and what candid_types is specified to do with arena indices. Subtyping is written twice, deliberately. Candid/SubtypeSpec.lean holds the coinductive relation, mirroring spec/Candid.md rule for rule; Candid/Subtype.lean holds the decision procedure. The theorem connecting them is stated in prose and is the next slice's first obligation. Keeping them apart is what makes the model a specification and an oracle at once, rather than one or the other. Three things the spec turned out to say that the design had to follow: - The negative premises in the four `opt` rules are eliminable. Pairing each negative rule with its positive twin collapses them to `t <: opt t'` for every t and t'. This is not a shortcut -- a rule functional with negative premises is non-monotone and has no greatest fixed point, so the relation would not be coinductively definable at all. - `principal` is a (spec:80), not a reference type. It lives in Prim, which also makes `principal <: principal` follow from prim reflexivity. - The type table may only hold composite types (spec:1227, "no "), which is stronger than the no-bare-references invariant it replaces and rules out unbounded reference walks for a reason that is cited rather than derived. Subtyping relates two tables, not one. A TypeExpr holding a ref means nothing without its table, and the case that matters most compares a wire type table against the receiver's own type graph. Separating them forces the memo onto reference pairs -- bounded by |A|x|B|, where unfolded expressions are not -- and exposes that func contravariance swaps the tables along with the types. Deferred and named in lean/README.md rather than left implicit: `fuel` bounds recursion depth instead of a termination measure, and returns none rather than false when exhausted so the model never reports an answer it did not compute; decSubtype_iff; productive-recursion checking; Verso. Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/lean.yml | 39 +++++ lean/.gitignore | 1 + lean/Candid.lean | 11 ++ lean/Candid/Hash.lean | 34 +++++ lean/Candid/Subtype.lean | 233 +++++++++++++++++++++++++++++ lean/Candid/SubtypeSpec.lean | 119 +++++++++++++++ lean/Candid/TypeExpr.lean | 195 ++++++++++++++++++++++++ lean/Main.lean | 281 +++++++++++++++++++++++++++++++++++ lean/README.md | 139 ++++++++++++++--- lean/lake-manifest.json | 6 + lean/lakefile.toml | 15 ++ lean/lean-toolchain | 1 + 12 files changed, 1053 insertions(+), 21 deletions(-) create mode 100644 .github/workflows/lean.yml create mode 100644 lean/.gitignore create mode 100644 lean/Candid.lean create mode 100644 lean/Candid/Hash.lean create mode 100644 lean/Candid/Subtype.lean create mode 100644 lean/Candid/SubtypeSpec.lean create mode 100644 lean/Candid/TypeExpr.lean create mode 100644 lean/Main.lean create mode 100644 lean/lake-manifest.json create mode 100644 lean/lakefile.toml create mode 100644 lean/lean-toolchain diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml new file mode 100644 index 00000000..157a33c2 --- /dev/null +++ b/.github/workflows/lean.yml @@ -0,0 +1,39 @@ +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` is not configured yet; the reference executable is the test. + - 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/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..6c42ad0c --- /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.TypeExpr +import Candid.Subtype +import Candid.SubtypeSpec diff --git a/lean/Candid/Hash.lean b/lean/Candid/Hash.lean new file mode 100644 index 00000000..151ef1a5 --- /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 `TypeExpr.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..4e5995d5 --- /dev/null +++ b/lean/Candid/Subtype.lean @@ -0,0 +1,233 @@ +/- +Candid subtyping, as a decision procedure over two independent type tables. + +Rules are from `spec/Candid.md`, "Upgrading and Subtyping". Two things about that +section shape everything here. + +**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 `TypeExpr` 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. +-/ + +import Candid.TypeExpr + +namespace Candid + +/-- The result of a subtype question. `none` means the recursion budget ran out. + +Returning `Bool` here would mean reporting "not a subtype" for a question the model +never actually answered. -/ +abbrev Verdict := Option Bool + +namespace Verdict + +/-- Short-circuiting conjunction that preserves "unanswered". -/ +def and (x : Verdict) (y : Unit → Verdict) : Verdict := + match x with + | some true => y () + | some false => some false + | none => none + +/-- `f` holds of every element. Stops at the first `false` or unanswered. -/ +def all (f : α → Verdict) : List α → Verdict + | [] => some true + | x :: xs => match f x with + | some true => all f xs + | r => r + +/-- `f` holds of some element. Stops at the first `true`; an unanswered question +anywhere makes the whole disjunction unanswered, since a later `true` cannot be +ruled out. -/ +def any (f : α → Verdict) : List α → Verdict + | [] => some false + | x :: xs => match f x with + | some false => any f xs + | some true => some true + | none => none + +end Verdict + +/-- `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 (e : TypeTable) (t : TypeExpr) : Bool := + match e.resolve t with + | some (.prim .null) | some (.prim .reserved) | 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 TypeExpr → List (FieldId × TypeExpr) + | [] => [] + | t :: ts => (UInt32.ofNat i, t) :: indexedFrom (i + 1) ts + +/-- Function annotations must be equal *as sets*, per the spec. -/ +def annotsAgree (xs ys : List FuncAnnot) : Bool := + xs.all (ys.contains ·) && ys.all (xs.contains ·) + +/-- Look up a label. -/ +def fieldAt (fs : List (FieldId × TypeExpr)) (id : FieldId) : Option TypeExpr := + (fs.find? (·.1 == id)).map (·.2) + +/-- Look up a method. -/ +def methodAt (ms : List (String × TypeExpr)) (name : String) : Option TypeExpr := + (ms.find? (·.1 == name)).map (·.2) + +/- Structural depth, used only to seed the recursion budget. -/ +mutual + +/-- Structural depth. A `ref` counts as a leaf; unfolding is budgeted separately. -/ +def TypeExpr.depth : TypeExpr → Nat + | .prim _ | .ref _ => 1 + | .opt t | .vec t => 1 + t.depth + | .record fs | .variant fs => 1 + TypeExpr.depthFields fs + | .func args rets _ => 1 + Nat.max (TypeExpr.depthList args) (TypeExpr.depthList rets) + | .service ms => 1 + TypeExpr.depthMethods ms + +def TypeExpr.depthList : List TypeExpr → Nat + | [] => 0 + | t :: ts => Nat.max t.depth (TypeExpr.depthList ts) + +def TypeExpr.depthFields : List (FieldId × TypeExpr) → Nat + | [] => 0 + | (_, t) :: fs => Nat.max t.depth (TypeExpr.depthFields fs) + +def TypeExpr.depthMethods : List (String × TypeExpr) → Nat + | [] => 0 + | (_, t) :: ms => Nat.max t.depth (TypeExpr.depthMethods ms) + +end + +/-- `sub A B seen fuel a b` decides `a <: b`, where `a`'s references resolve in `A` +and `b`'s in `B`. + +`seen` is the coinductive hypothesis: a pair of *references* already under +consideration. Recursive types make the relation a greatest fixed point, so +re-encountering a pair means the obligation is discharged, not that it failed. The +memo must be keyed on reference pairs and not on expressions -- unfolded expressions +can nest without bound, while reference pairs are bounded by `|A| x |B|`. + +`fuel` bounds recursion depth. It is a device, not the real argument: the intended +termination measure is lexicographic on (reference pairs not yet in `seen`, +structural size), which needs `TypeTable.wellFormed`'s "every entry is composite" +invariant carried in the type to prove that resolving a reference makes progress. +Replacing `fuel` with that measure is the first proof obligation of the next slice. +-/ +def sub (A B : TypeTable) (seen : List (TypeRef × TypeRef)) : Nat → TypeExpr → TypeExpr → Verdict + | 0, _, _ => none + | fuel + 1, a, b => + match a, b with + -- Both sides are references: the memo point. + | .ref i, .ref j => + if seen.contains (i, j) then some true + else match A.lookup? i, B.lookup? j with + | some a', some b' => sub A B ((i, j) :: seen) fuel a' b' + | _, _ => some false -- dangling: not well formed + -- One side is a reference. Well-formed tables hold only composite types, so this + -- unfolds at most once before making structural progress. + | .ref i, _ => + match A.lookup? i with + | some a' => sub A B seen fuel a' b + | none => some false + | _, .ref j => + match B.lookup? j with + | some b' => sub A B seen fuel a b' + | none => some false + + -- ` <: reserved` and `empty <: `: the top and bottom types. + | _, .prim .reserved => some true + | .prim .empty, _ => some true + + -- 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 _ => some true + + | .prim p, .prim q => + -- ` <: `, plus `nat <: int`. `principal` is a primitive + -- (spec/Candid.md:80), so `principal <: principal` needs no rule of its own. + some (p == q || (p == .nat && q == .int)) + + -- `service <: principal`. + | .service _, .prim .principal => some true + + | .vec t, .vec t' => sub A B seen fuel t t' + + -- 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 => + Verdict.all (fun (id, g) => + match fieldAt fs id with + | some f => sub A B seen fuel f g + | none => some (B.acceptsNull g)) 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 => + Verdict.all (fun (id, f) => + match fieldAt gs id with + | some g => sub A B seen fuel f g + | none => some false) fs + + -- Parameters generalise, results specialise, and both behave like tuple-shaped + -- records -- so arguments may be dropped and results added. + | .func args rets ann, .func args' rets' ann' => + if annotsAgree ann ann' then + Verdict.and + (sub B A seen fuel (.record (indexedFrom 1 args')) (.record (indexedFrom 1 args))) + fun _ => sub A B seen fuel (.record (indexedFrom 1 rets)) (.record (indexedFrom 1 rets')) + else some false + + -- Services are records of functions: a method may be specialised or added. + | .service ms, .service ms' => + Verdict.all (fun (name, g) => + match methodAt ms name with + | some f => sub A B seen fuel f g + | none => some false) ms' + + | _, _ => some false + +/-- A budget that is generous rather than tight: every path may unfold each +reference pair once (`|A| x |B|`), descending the structure between unfoldings. -/ +def budgetFor (a b : ClosedType) : Nat := + let pairs := (a.table.size + 1) * (b.table.size + 1) + pairs * (a.root.depth + b.root.depth + 2) + 2 + +/-- Decide `a <: b` for two types carrying their own tables. + +`none` means the budget was exhausted, which a well-formed input should never +provoke -- `budgetFor` is derived from the inputs. -/ +def decSubtype (a b : ClosedType) : Verdict := + sub a.table b.table [] (budgetFor a b) a.root b.root + +/- Note the argument order flip in the `func` case above: parameters are +contravariant, so the tables swap with the types. Getting this 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..34da4e10 --- /dev/null +++ b/lean/Candid/SubtypeSpec.lean @@ -0,0 +1,119 @@ +/- +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 `TypeExpr` is 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. + +The type tables are *indices* rather than parameters because the `func` rule swaps +them: parameter subtyping is contravariant. +-/ + +import Candid.Subtype + +namespace Candid + +coinductive Subty : TypeTable → TypeTable → TypeExpr → TypeExpr → 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 ms} : Subty A B (.service ms) (.prim .principal) + /-- All four `opt` rules of the spec, collapsed. Any type is a subtype of any + option; a receiver that cannot decode the value sees `null`. -/ + | toOpt {A B a b} : Subty A B a (.opt b) + /-- `vec <: vec ` when ` <: ` -/ + | vec {A B t t'} : Subty A B t t' → Subty A B (.vec t) (.vec t') + /-- 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)) → + Subty 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) → + Subty A B (.variant fs) (.variant gs) + /-- Parameters generalise, results specialise, both as tuple-shaped records. Note + the swapped tables in the parameter premise. -/ + | func {A B args rets ann args' rets' ann'} : + annotsAgree ann ann' = true → + Subty B A (.record (indexedFrom 1 args')) (.record (indexedFrom 1 args)) → + Subty A B (.record (indexedFrom 1 rets)) (.record (indexedFrom 1 rets')) → + Subty 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) → + Subty A B (.service ms) (.service ms') + /-- References are transparent: a type is related through its table entry. -/ + | unfoldLeft {A B i a' b} : + A.lookup? i = some a' → Subty A B a' b → Subty A B (.ref i) b + | unfoldRight {A B a j b'} : + B.lookup? j = some b' → Subty A B a b' → Subty A B a (.ref j) + +/-! 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 in slice 2. -/ + +example (A B : TypeTable) : Subty A B (.prim .nat) (.prim .int) := Subty.natInt + +example (A B : TypeTable) (t : TypeExpr) : Subty A B (.prim .text) (.opt t) := Subty.toOpt + +example (A B : TypeTable) (a : TypeExpr) : Subty A B a (.prim .reserved) := Subty.toReserved + +example (A B : TypeTable) : Subty A B (.vec (.prim .nat)) (.vec (.prim .int)) := + Subty.vec Subty.natInt + +/-- The empty record is a supertype of every record: the field premise is vacuous. -/ +example (A B : TypeTable) (fs : List (FieldId × TypeExpr)) : + Subty A B (.record fs) (.record []) := by + apply Subty.record + intro id g h + simp [fieldAt] at h + +/- +The obligation this file exists to create, and the first proof of the next slice: + + theorem decSubtype_iff (a b : ClosedType) + (ha : a.wellFormed = true) (hb : b.wellFormed = true) : + decSubtype a b = some true <-> Subty a.table b.table a.root b.root + +Soundness (`some true` implies `Subty`) should follow by coinduction on the +procedure's recursion, with `seen` as the coinductive hypothesis -- that is what +`seen` *means*, and stating it this way is what will confirm the memo is keyed +correctly. Completeness additionally needs that the budget never runs out on +well-formed input, which is the same fact that would let `fuel` be replaced by a +proper termination measure. + +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/TypeExpr.lean b/lean/Candid/TypeExpr.lean new file mode 100644 index 00000000..78c204a0 --- /dev/null +++ b/lean/Candid/TypeExpr.lean @@ -0,0 +1,195 @@ +/- +The Candid type language, represented finitely. + +`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. + +On the name: the old implementation calls this a `TypeEnv`, but its `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 Candid type, possibly containing references into an accompanying `TypeTable`. -/ +inductive TypeExpr where + | prim (p : Prim) + | opt (inner : TypeExpr) + | vec (inner : TypeExpr) + | record (fields : List (FieldId × TypeExpr)) + | variant (alts : List (FieldId × TypeExpr)) + | func (args rets : List TypeExpr) (annots : List FuncAnnot) + | service (methods : List (String × TypeExpr)) + | ref (target : TypeRef) + deriving Repr, Inhabited + +/-- A type table: `TypeRef` -> `TypeExpr`. -/ +structure TypeTable where + entries : Array TypeExpr + deriving Repr, Inhabited + +namespace TypeTable + +def size (t : TypeTable) : Nat := t.entries.size + +def lookup? (t : TypeTable) (r : TypeRef) : Option TypeExpr := t.entries[r]? + +/-- The empty table, for types that contain no references. -/ +def empty : TypeTable := { entries := #[] } + +end TypeTable + +def TypeExpr.isRef : TypeExpr → Bool + | .ref _ => true + | _ => false + +/-- Is this a ``, i.e. a `` or a ``? + +`spec/Candid.md:1227` -- "The type table may only contain composite types (no +``)". So this is exactly what may appear as a table entry, and it excludes +both primitives and bare references. -/ +def TypeExpr.isComposite : TypeExpr → Bool + | .opt _ | .vec _ | .record _ | .variant _ | .func _ _ _ | .service _ => true + | .prim _ | .ref _ => false + +/-- 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 of a type expression against a table of `bound` entries: +every reference resolves, and no record, variant or service repeats 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. -/ +mutual + +/-- Every reference resolves below `bound`, and no label is repeated. -/ +def TypeExpr.wellFormed (bound : Nat) : TypeExpr → Bool + | .prim _ => true + | .ref r => r < bound + | .opt t | .vec t => t.wellFormed bound + | .record fs | .variant fs => noDups (fs.map (·.1)) && TypeExpr.wfFields bound fs + | .func args rets _ => TypeExpr.wfList bound args && TypeExpr.wfList bound rets + | .service ms => noDups (ms.map (·.1)) && TypeExpr.wfMethods bound ms + +def TypeExpr.wfList (bound : Nat) : List TypeExpr → Bool + | [] => true + | t :: ts => t.wellFormed bound && TypeExpr.wfList bound ts + +def TypeExpr.wfFields (bound : Nat) : List (FieldId × TypeExpr) → Bool + | [] => true + | (_, t) :: fs => t.wellFormed bound && TypeExpr.wfFields bound fs + +def TypeExpr.wfMethods (bound : Nat) : List (String × TypeExpr) → Bool + | [] => true + | (_, t) :: ms => t.wellFormed bound && TypeExpr.wfMethods bound ms + +end + +/-- A table is well formed when every entry is well formed **and composite**. + +The second condition is the spec's own (`spec/Candid.md:1227`), and it is load-bearing +here: since no entry is a primitive or a bare reference, following a reference is a +single step, which is what bounds the subtype recursion. Textual `.did` aliases +(`type A = B;`) must therefore be resolved before they reach this model. -/ +def TypeTable.wellFormed (t : TypeTable) : Bool := + t.entries.all fun e => e.wellFormed t.size && e.isComposite + +/-- Follow at most one reference. Returns `none` on a dangling index. + +In a well-formed table the result is never itself a `ref`. That is not yet expressed +in the type, so `Subtype.lean` bounds unfolding explicitly instead of relying on it. -/ +def TypeTable.resolve (t : TypeTable) (e : TypeExpr) : Option TypeExpr := + match e with + | .ref r => t.lookup? r + | _ => some e + +/-- A type together with the table its references resolve in. + +This is the unit the public API speaks in, because a `TypeExpr` containing a `ref` +means nothing without its table. The first draft of `decSubtype` took one table and +two `TypeExpr`s, which silently assumed both types 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 : TypeExpr + deriving Repr, Inhabited + +namespace ClosedType + +def wellFormed (c : ClosedType) : Bool := + c.table.wellFormed && c.root.wellFormed c.table.size + +/-- A type containing no references. -/ +def ofExpr (e : TypeExpr) : ClosedType := { table := .empty, root := e } + +end ClosedType + +/-! Abbreviations for the primitives, so examples read like Candid rather than +like an AST. -/ + +namespace TypeExpr + +def null : TypeExpr := .prim .null +def bool : TypeExpr := .prim .bool +def nat : TypeExpr := .prim .nat +def int : TypeExpr := .prim .int +def nat8 : TypeExpr := .prim .nat8 +def nat16 : TypeExpr := .prim .nat16 +def nat32 : TypeExpr := .prim .nat32 +def nat64 : TypeExpr := .prim .nat64 +def int8 : TypeExpr := .prim .int8 +def int16 : TypeExpr := .prim .int16 +def int32 : TypeExpr := .prim .int32 +def int64 : TypeExpr := .prim .int64 +def float32 : TypeExpr := .prim .float32 +def float64 : TypeExpr := .prim .float64 +def text : TypeExpr := .prim .text +def reserved : TypeExpr := .prim .reserved +def empty : TypeExpr := .prim .empty +def principal : TypeExpr := .prim .principal + +/-- A record from named fields, hashing the names. -/ +def recordOf (fs : List (String × TypeExpr)) : TypeExpr := + .record (fs.map fun (n, t) => (hashFieldName n, t)) + +/-- A variant from named alternatives, hashing the names. -/ +def variantOf (fs : List (String × TypeExpr)) : TypeExpr := + .variant (fs.map fun (n, t) => (hashFieldName n, t)) + +end TypeExpr + +end Candid diff --git a/lean/Main.lean b/lean/Main.lean new file mode 100644 index 00000000..b69903e4 --- /dev/null +++ b/lean/Main.lean @@ -0,0 +1,281 @@ +/- +The reference executable. + +Slice 1 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. +-/ + +import Candid + +open Candid +open Candid.TypeExpr + +structure Check where + name : String + ok : Bool + detail : String + +def verdictStr : Verdict → String + | some true => "<:" + | some false => "!<:" + | none => "budget exhausted" + +/-- A subtype question about two types that carry no references. -/ +def expectSub (a b : TypeExpr) (want : Bool) (name : String) : Check := + let got := decSubtype (.ofExpr a) (.ofExpr b) + { name := name + ok := got == some want + detail := s!"got {verdictStr got}, want {verdictStr (some want)}" } + +/-- A subtype question about two types with their own type tables. -/ +def expectSubIn (a b : ClosedType) (want : Bool) (name : String) : Check := + let got := decSubtype a b + { name := name + ok := got == some want + detail := s!"got {verdictStr got}, want {verdictStr (some 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 nat nat true "nat <: nat" + , expectSub nat int true "nat <: int" + , expectSub int nat false "int !<: nat" + , expectSub nat8 nat false "nat8 !<: nat (no width subtyping)" + , expectSub nat nat8 false "nat !<: nat8" + , expectSub nat32 int32 false "nat32 !<: int32" + , expectSub text reserved true "text <: reserved" + , expectSub (.func [] [] []) reserved true "func <: reserved" + , expectSub empty text true "empty <: text" + , expectSub empty (.vec nat) true "empty <: vec nat" + , expectSub text nat false "text !<: nat" + , expectSub (.service []) .principal true "service <: principal" + , expectSub .principal (.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 nat (.opt nat) true "nat <: opt nat" + , expectSub null (.opt nat) true "null <: opt nat" + , expectSub reserved (.opt nat) true "reserved <: opt nat" + , expectSub text (.opt nat) true "text <: opt nat (special opt rule)" + , expectSub (.opt text) (.opt nat) true "opt text <: opt nat (special opt rule)" + , expectSub (.opt nat) nat false "opt nat !<: nat" + , expectSub (.opt nat) reserved true "opt nat <: reserved" ] + +/-! ## Vectors -/ + +def vecChecks : List Check := + [ expectSub (.vec nat) (.vec int) true "vec nat <: vec int" + , expectSub (.vec int) (.vec nat) false "vec int !<: vec nat" + , expectSub (.vec nat) 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. -/ + +def recordChecks : List Check := + [ expectSub (recordOf [("x", nat)]) (recordOf []) true + "record {x:nat} <: record {}" + , expectSub (recordOf [("x", nat), ("y", text)]) (recordOf [("x", nat)]) true + "record {x;y} <: record {x} (field added)" + , expectSub (recordOf [("x", nat)]) (recordOf [("x", int)]) true + "record {x:nat} <: record {x:int} (field specialised)" + , expectSub (recordOf [("x", int)]) (recordOf [("x", nat)]) false + "record {x:int} !<: record {x:nat}" + , expectSub (recordOf [("x", nat)]) (recordOf [("x", nat), ("y", .opt text)]) true + "record {x} <: record {x; y:opt text} (omitted field accepts null)" + , expectSub (recordOf [("x", nat)]) (recordOf [("x", nat), ("y", reserved)]) true + "record {x} <: record {x; y:reserved}" + , expectSub (recordOf [("x", nat)]) (recordOf [("x", nat), ("y", text)]) false + "record {x} !<: record {x; y:text} (omitted field rejects null)" + , expectSub (recordOf [("x", nat)]) (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`. -/ + +def variantChecks : List Check := + [ expectSub (variantOf []) (variantOf [("a", nat)]) true + "variant {} <: variant {a}" + , expectSub (variantOf [("a", nat)]) (variantOf [("a", nat), ("b", text)]) true + "variant {a} <: variant {a; b} (tag dropped)" + , expectSub (variantOf [("a", nat), ("b", text)]) (variantOf [("a", nat)]) false + "variant {a; b} !<: variant {a} (tag added)" + , expectSub (variantOf [("a", nat)]) (variantOf [("a", int)]) true + "variant {a:nat} <: variant {a:int}" + , expectSub (.opt (variantOf [("a", nat), ("b", text)])) (.opt (variantOf [("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. -/ + +def funcChecks : List Check := + [ expectSub (.func [int] [nat] []) (.func [nat] [int] []) true + "func (int) -> (nat) <: func (nat) -> (int)" + , expectSub (.func [nat] [int] []) (.func [int] [nat] []) false + "func (nat) -> (int) !<: func (int) -> (nat)" + -- Parameters: dropping is free, adding needs to accept null. + , expectSub (.func [] [] []) (.func [nat] [] []) true + "func () -> () <: func (nat) -> () (parameter dropped, always allowed)" + , expectSub (.func [.opt nat] [] []) (.func [] [] []) true + "func (opt nat) -> () <: func () -> () (optional parameter added)" + , expectSub (.func [nat] [] []) (.func [] [] []) false + "func (nat) -> () !<: func () -> () (added parameter rejects null)" + -- Results: adding is free, dropping needs to accept null. + , expectSub (.func [] [nat] []) (.func [] [] []) true + "func () -> (nat) <: func () -> () (result added, always allowed)" + , expectSub (.func [] [] []) (.func [] [.opt nat] []) true + "func () -> () <: func () -> (opt nat) (optional result dropped)" + , expectSub (.func [] [] []) (.func [] [nat] []) false + "func () -> () !<: func () -> (nat) (dropped result rejects null)" + , expectSub (.func [] [] [.query]) (.func [] [] []) false + "annotations must agree" + , expectSub (.func [] [] [.query]) (.func [] [] [.query]) true + "matching annotations agree" ] + +/-! ## Services -/ + +def serviceChecks : List Check := + [ expectSub (.service [("m", .func [] [] [])]) (.service []) true + "service {m} <: service {}" + , expectSub (.service []) (.service [("m", .func [] [] [])]) false + "service {} !<: service {m}" + , expectSub (.service [("m", .func [] [nat] [])]) (.service [("m", .func [] [] [])]) true + "service method specialised" ] + +/-! ## Recursive types across two independent tables + +These are the cases the reference-pair memo exists for. `selfLoop` and `twoCycle` +denote the same infinite type through different table shapes, which is why the memo +has to be keyed on reference pairs rather than on unfolded expressions -- the +expressions never repeat, the reference pairs do. -/ + +/-- `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 : TypeExpr) : ClosedType := + { table := { entries := #[ recordOf [("next", .ref 0), ("extra", extra)] ] }, root := .ref 0 } + +/-- A table entry that is a bare reference: rejected, and it is the reference case +that would otherwise make following a reference an unbounded walk. -/ +def bareRefEntry : ClosedType := + { table := { entries := #[ .ref 0 ] }, root := .ref 0 } + +/-- A table entry that is a primitive: also rejected. `spec/Candid.md:1227` -- "The +type table may only contain composite types (no ``)." -/ +def primEntry : ClosedType := + { table := { entries := #[ nat ] }, root := .ref 0 } + +/-- A reference with no entry to resolve to. -/ +def danglingRef : ClosedType := + { table := { entries := #[] }, root := .ref 3 } + +def recursiveChecks : List Check := + [ expectSubIn selfLoop selfLoop true + "self-loop <: itself (memo terminates)" + , expectSubIn selfLoop twoCycle true + "self-loop <: two-cycle (same type, different table shape)" + , expectSubIn twoCycle selfLoop true + "two-cycle <: self-loop" + , expectSubIn (selfLoopWith nat) (selfLoopWith int) true + "recursive record, field specialised" + , expectSubIn (selfLoopWith int) (selfLoopWith nat) false + "recursive record, field not specialised" + , expectSubIn (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 bareRefEntry false "bare reference as a table entry is malformed" + , expectWellFormed primEntry false "primitive as a table entry is malformed" + , expectWellFormed (.ofExpr principal) true "principal is a primitive, not a reftype" + , expectWellFormed danglingRef false "dangling reference is malformed" + , expectWellFormed (.ofExpr (.record [(0, nat), (0, text)])) false + "duplicate field id is malformed" ] + +/-! ## 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 := recordOf [("x", nat)] + let b := recordOf [("x", nat), ("y", .opt text)] + let c := 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 ++ recursiveChecks ++ + transitivityChecks + +def main : IO UInt32 := do + let failures := allChecks.filter (fun c => !c.ok) + for c in allChecks do + if c.ok then + IO.println s!"ok {c.name}" + else + IO.println s!"FAIL {c.name} -- {c.detail}" + IO.println "" + if failures.isEmpty then + IO.println s!"{allChecks.length} checks passed" + 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..29ce094e 100644 --- a/lean/README.md +++ b/lean/README.md @@ -1,25 +1,29 @@ # `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. 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. `TypeExpr`, `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 +37,124 @@ 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. + +**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: `TypeExpr`, `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. + +`TypeTable` rather than the old implementation's `TypeEnv` 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 `TypeExpr` 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. Two consequences fall out of separating +them: the memo must be keyed on **reference pairs**, since unfolded expressions nest +without bound while reference pairs are bounded by `|A| x |B|`; and the `func` rule's +contravariance swaps the *tables* along with the types, which is invisible when there +is only one table to swap. + ## 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] 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. + +- **`fuel` in `Candid/Subtype.lean`.** The procedure bounds recursion depth with a + budget instead of a termination measure, and returns `none` — not `false` — when it + runs out, so the model never reports an answer it did not compute. The intended + measure is lexicographic on (reference pairs not yet in `seen`, structural size); + proving it needs `TypeTable.wellFormed`'s "every entry is composite" invariant + carried in the type rather than checked separately. +- **`decSubtype_iff`** — that the procedure decides the relation. Stated in + [Candid/SubtypeSpec.lean](Candid/SubtypeSpec.lean). Soundness should follow by + coinduction with `seen` as the coinductive hypothesis, which is what `seen` means; + completeness additionally needs the budget never to run out. +- **Unguarded recursion.** `TypeTable.wellFormed` requires every entry to be a + `` — the spec's own rule (`spec/Candid.md:1227`), which rules out both + primitives and bare references — but it does not yet require recursion to be + *productive*. Textual `.did` aliases (`type A = B;`) must be resolved before + reaching this model. +- **Verso.** Deliberately not in slice 1: bundling an undocumented doc toolchain into + the slice 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..4f9c7889 --- /dev/null +++ b/lean/lakefile.toml @@ -0,0 +1,15 @@ +name = "candid" +version = "0.1.0" +defaultTargets = ["Candid", "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 From 4eefc457ed072798a46c723745978ddcd0a324c1 Mon Sep 17 00:00:00 2001 From: Linwei Shang Date: Tue, 11 Aug 2026 09:47:25 -0400 Subject: [PATCH 2/7] docs: relax the policy boundary to location, and correct what slice 1 disproved MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three corrections that writing the first slice forced, none of which were visible from the plan alone. **The policy boundary was in the wrong place.** §5 said "only code churn lives on the branch" and listed directory reservations as policy, which made every README inside a reserved directory a master-PR item -- so recording a design decision cost a review round trip. 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. The boundary is now location: everything under lean/, crates/ and conformance/ belongs to the working branch, including their README.md and CLAUDE.md; policy is what sits outside them. Location is decidable from a diff, where "is this policy?" is arguable. Two claims in §5 were also simply false once we started editing: "existing files are not modified" and a review criterion of "touches nothing existing". Both now name the real constraint -- nothing under rust/, spec/, test/, coq/ or tools/ is touched, and REWRITE.md is in scope because it is where the plan gets corrected. **§6's coq/ deletion condition was wrong on both halves.** It asked that Lean reproduce every MiniCandid theorem and that the two models be diffed, which treats them as the same kind of artifact differing in coverage. MiniCandid is a justification device: it shows that non-obvious design decisions are sound and that a proposed spec change can be accommodated. The Lean model answers what happens to a given input. So the condition is that each theorem's purpose is discharged, and there is no structural diff to perform once one side has finite types and an explicit table. The scoped nine-constructor comparison survives as a finding worth hunting, not a gate. **The layering diagram named a structure that does not exist.** candid_types listed TypeEnv, but rust/'s TypeEnv is a BTreeMap -- a name-keyed environment of .did declarations, not an index-keyed table, and both will exist. The diagram now names TypeExpr/TypeTable/TypeRef/FieldId/ClosedType, matching the Lean identifiers so that "candid_subtype reads as a transcription of its Lean counterpart" is checkable rather than aspirational, with a naming table in crates/README.md and the rule restated in crates/CLAUDE.md. TypeEnv stays reserved for candid_syntax, where "environment" is the accurate word. Co-Authored-By: Claude Opus 5 (1M context) --- REWRITE.md | 62 ++++++++++++++++++++++++++++++++++++++---------- crates/CLAUDE.md | 8 ++++++- crates/README.md | 37 +++++++++++++++++++++++++---- 3 files changed, 89 insertions(+), 18 deletions(-) diff --git a/REWRITE.md b/REWRITE.md index 95a50de1..b406c42d 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. +candid_types TypeExpr, 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..f8ca5d4f 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. +candid_types TypeExpr, 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,35 @@ 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. + +| | | +|---|---| +| `TypeExpr` | one structural node; may contain references | +| `TypeTable` | `TypeRef` → `TypeExpr`, index-keyed — what the spec calls the type definition table | +| `TypeRef` | index into a `TypeTable` | +| `ClosedType` | a `TypeTable` and a root `TypeExpr` 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. + +`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 +105,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. From bbc767b5fda20b3e9be8bfdaf4b3465a759499f4 Mon Sep 17 00:00:00 2001 From: Linwei Shang Date: Tue, 25 Aug 2026 11:44:53 -0400 Subject: [PATCH 3/7] fix(lean): swap the subtype memo with the tables in the parameter premise The function rule's parameter premise is contravariant, so it swaps the two type tables -- but it passed `seen` through unchanged. A memo of (A-index, B-index) pairs was then read as (B-index, A-index), which asserts a transposed and generally different question, since subtyping is not symmetric. The result was `<:` reported for unrelated types. The new `contra` checks in Main.lean are the witness: `record { f : func (vec nat) -> () }` against `record { f : func (vec text) -> () }` reaches its parameter premise with `(1, 2)` in the memo, reads it transposed, and answers `<:` where the answer is `!<:`. Both checks fail without the one-line fix. Also records a second gap, which this does not fix. `T.0 = vec (vec T.0)` makes `ref 0` and `vec (ref 0)` the same infinite type, but every state on that cycle has a reference on exactly one side, so the reference-pair memo never fires and no budget suffices. That makes the completeness half of the `decSubtype_iff` obligation false of the current procedure rather than merely unproved, so the comments claiming a termination measure exists are corrected too. The two `vecOmega` checks state the answer the model owes and are marked as known gaps: reported, not build failures -- and a known gap that starts passing is itself a failure, so the fix cannot land unnoticed. Co-Authored-By: Claude Opus 5 (1M context) --- lean/Candid/Subtype.lean | 42 ++++++++++------ lean/Candid/SubtypeSpec.lean | 11 ++-- lean/Main.lean | 98 ++++++++++++++++++++++++++++++++---- 3 files changed, 123 insertions(+), 28 deletions(-) diff --git a/lean/Candid/Subtype.lean b/lean/Candid/Subtype.lean index 4e5995d5..70f39fd7 100644 --- a/lean/Candid/Subtype.lean +++ b/lean/Candid/Subtype.lean @@ -129,15 +129,20 @@ and `b`'s in `B`. `seen` is the coinductive hypothesis: a pair of *references* already under consideration. Recursive types make the relation a greatest fixed point, so -re-encountering a pair means the obligation is discharged, not that it failed. The -memo must be keyed on reference pairs and not on expressions -- unfolded expressions -can nest without bound, while reference pairs are bounded by `|A| x |B|`. - -`fuel` bounds recursion depth. It is a device, not the real argument: the intended -termination measure is lexicographic on (reference pairs not yet in `seen`, -structural size), which needs `TypeTable.wellFormed`'s "every entry is composite" -invariant carried in the type to prove that resolving a reference makes progress. -Replacing `fuel` with that measure is the first proof obligation of the next slice. +re-encountering a pair means the obligation is discharged, not that it failed. + +**Keying the memo on reference pairs is not enough**, and the `vecOmega` checks in +`Main.lean` are the witness: a cycle whose states always have a reference on exactly one side +never reaches this memo point, so `seen` stays empty and no `fuel` value suffices. +Rust keys on *expression* pairs and inserts whenever either side is a variable +(`rust/candid/src/types/subtype.rs:214`), which closes that cycle -- and unfolded +expressions do not in fact nest without bound, since unfolding only ever replaces a +reference at the top, leaving every state a subterm of a root or of an entry. + +So `fuel` is not a placeholder for a measure that exists: for this algorithm there +is none. Either the memo is keyed on expression pairs -- terminating, but the proof +then needs "all reachable states lie in a finite set" threaded through -- or the +representation changes so that every recursive call passes through a reference pair. -/ def sub (A B : TypeTable) (seen : List (TypeRef × TypeRef)) : Nat → TypeExpr → TypeExpr → Verdict | 0, _, _ => none @@ -196,10 +201,16 @@ def sub (A B : TypeTable) (seen : List (TypeRef × TypeRef)) : Nat → TypeExpr -- 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 must swap the memo with them: an + -- entry `(i, j)` means "A's `i` against B's `j`", and reading it unswapped in the + -- swapped call asserts `B`'s `i` against `A`'s `j` -- a different, and generally + -- false, question. See the `contra` checks in `Main.lean`. | .func args rets ann, .func args' rets' ann' => if annotsAgree ann ann' then Verdict.and - (sub B A seen fuel (.record (indexedFrom 1 args')) (.record (indexedFrom 1 args))) + (sub B A (seen.map Prod.swap) fuel + (.record (indexedFrom 1 args')) (.record (indexedFrom 1 args))) fun _ => sub A B seen fuel (.record (indexedFrom 1 rets)) (.record (indexedFrom 1 rets')) else some false @@ -220,14 +231,15 @@ def budgetFor (a b : ClosedType) : Nat := /-- Decide `a <: b` for two types carrying their own tables. -`none` means the budget was exhausted, which a well-formed input should never -provoke -- `budgetFor` is derived from the inputs. -/ +`none` means the budget was exhausted. Well-formed input *can* provoke it -- see +the `vecOmega` checks in `Main.lean` -- so `none` is a real answer callers must handle, not a +theoretical one. -/ def decSubtype (a b : ClosedType) : Verdict := sub a.table b.table [] (budgetFor a b) a.root b.root /- Note the argument order flip in the `func` case above: parameters are -contravariant, so the tables swap with the types. Getting this wrong is invisible -when both types share one table, which is the second reason the two-table signature -is worth the extra parameter. -/ +contravariant, so the tables swap with the types -- and the memo 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 index 34da4e10..2c731a6e 100644 --- a/lean/Candid/SubtypeSpec.lean +++ b/lean/Candid/SubtypeSpec.lean @@ -105,9 +105,14 @@ The obligation this file exists to create, and the first proof of the next slice Soundness (`some true` implies `Subty`) should follow by coinduction on the procedure's recursion, with `seen` as the coinductive hypothesis -- that is what `seen` *means*, and stating it this way is what will confirm the memo is keyed -correctly. Completeness additionally needs that the budget never runs out on -well-formed input, which is the same fact that would let `fuel` be replaced by a -proper termination measure. +correctly. + +The completeness direction is **false of the current procedure**, not merely +unproved: the `vecOmega` pair in `Main.lean` is well formed and satisfies `Subty` +(close the +consistent set under `unfoldLeft`, `unfoldRight` and `vec`), while `decSubtype` +returns `none` on it for every budget. Stating the theorem is therefore blocked on +the procedure, not on the proof -- see the header of `Subtype.lean`. Deliberately not stated with `sorry`: an unproved `theorem` in the build reads as established once it scrolls past. The properties `coq/MiniCandid.v` establishes diff --git a/lean/Main.lean b/lean/Main.lean index b69903e4..36c4746d 100644 --- a/lean/Main.lean +++ b/lean/Main.lean @@ -16,6 +16,12 @@ 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. -/ + known : Bool := false + +/-- Record a check as a known gap rather than a requirement. -/ +def Check.asKnown (c : Check) : Check := { c with known := true } def verdictStr : Verdict → String | some true => "<:" @@ -193,9 +199,10 @@ def serviceChecks : List Check := /-! ## Recursive types across two independent tables These are the cases the reference-pair memo exists for. `selfLoop` and `twoCycle` -denote the same infinite type through different table shapes, which is why the memo -has to be keyed on reference pairs rather than on unfolded expressions -- the -expressions never repeat, the reference pairs do. -/ +denote the same infinite type through different table shapes, and every state on +their cycle has a reference on *both* sides, so the memo fires and the recursion +stops. `vecOmega` below is the same idea with the references on alternating sides, +where it does not. -/ /-- `type S = record { next : S }`, as one self-referential entry. -/ def selfLoop : ClosedType := @@ -246,6 +253,75 @@ def recursiveChecks : List Check := , expectWellFormed (.ofExpr (.record [(0, nat), (0, text)])) false "duplicate field id is malformed" ] +/-! ## `vec`-omega: a cycle the reference-pair memo does not catch + +`T.0 = vec (vec T.0)`, so `ref 0` and `vec (ref 0)` denote the same infinite type, +`vec (vec (vec ...))`. Both are well formed and both directions are `true`. + +The memo never fires, because every state on the cycle has a reference on exactly +one side: + + (ref 0, vec (ref 0)) + -> (vec (vec (ref 0)), vec (ref 0)) unfold left + -> (vec (ref 0), ref 0) descend + -> (vec (ref 0), vec (vec (ref 0))) unfold right + -> (ref 0, vec (ref 0)) descend -- back to the start + +`seen` stays empty, so `decSubtype` returns `none` and no larger `fuel` helps. These +two are recorded as known gaps: `expectSubIn` states the answer the model owes, and +the run reports it as `known` until the representation or the memo keying changes. -/ + +def vecOmegaTable : TypeTable := { entries := #[ .vec (.vec (.ref 0)) ] } + +/-- `vec`-omega as a reference. -/ +def vecOmegaRef : ClosedType := { table := vecOmegaTable, root := .ref 0 } + +/-- The same type, one `vec` unrolled ahead of the reference. -/ +def vecOmegaUnrolled : ClosedType := { table := vecOmegaTable, root := .vec (.ref 0) } + +def vecOmegaChecks : List Check := + [ expectWellFormed vecOmegaRef true "vec-omega: ref 0 is well formed" + , expectWellFormed vecOmegaUnrolled true "vec-omega: vec (ref 0) is well formed" + , (expectSubIn vecOmegaRef vecOmegaUnrolled true + "vec-omega <: its own unrolling").asKnown + , (expectSubIn vecOmegaUnrolled vecOmegaRef true + "vec-omega's unrolling <: it").asKnown ] + +/-! ## Contravariance: the memo swaps with the tables + +The parameter premise of the function rule swaps the two tables, so it must swap the +memo with them. An entry `(i, j)` asserts `A`'s `i` against `B`'s `j`; read unswapped +inside the swapped call it asserts `B`'s `i` against `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 puts `(1, 2)` in the memo, +so an unswapped read answers it `true` from the memo and both queries 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" + , expectSubIn contraFuncs contraFuncs' false + "func (vec nat) -> () !<: func (vec text) -> () (parameter premise fails)" + , expectSubIn 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 @@ -263,18 +339,20 @@ def transitivityChecks : List Check := def allChecks : List Check := hashChecks ++ primChecks ++ optChecks ++ vecChecks ++ recordChecks ++ variantChecks ++ funcChecks ++ serviceChecks ++ recursiveChecks ++ - transitivityChecks + vecOmegaChecks ++ contraChecks ++ transitivityChecks def main : IO UInt32 := do - let failures := allChecks.filter (fun c => !c.ok) + 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 - if c.ok then - IO.println s!"ok {c.name}" - else - IO.println s!"FAIL {c.name} -- {c.detail}" + 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} checks passed" + 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" From 47cf13e10ebf1f4baa45f40fb511541646801f12 Mon Sep 17 00:00:00 2001 From: Linwei Shang Date: Tue, 25 Aug 2026 21:25:04 -0400 Subject: [PATCH 4/7] lean: flatten the type language so the table is the only recursion A table entry is now 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 rather than an invention of this model (`spec/Candid.md:1207`), and the spec draws the conclusion the change is built on: "Because recursion goes through `T`, this format by construction rules out non-well-founded definitions like `type t = t`." What it buys: - The subtype procedure can only recurse through a pair of *references*; every other slot pair is decided outright. So it carries `todo` -- the reference pairs it has not yet assumed -- descends by removing one, and `todo.length` is a termination measure. The membership test that decides the branch is exactly the fact the measure needs, so no invariant is threaded through the recursion. - `fuel`, `budgetFor`, `TypeExpr.depth` and the whole `Verdict` (`Option Bool`) layer are gone. `decSubtype` returns `Bool` and is total, and the public API has no "unanswered" state to explain. - The two `vecOmega` checks recorded as known gaps in the previous commit now pass. A cycle whose states hold a reference on alternating sides used to dodge the reference-pair memo entirely; flat, the inner composite has to be an entry of its own, so the same cycle passes through `(0, 1)` and `(1, 0)` and stops. - Both `mutual` blocks in the type language collapse: well-formedness is now a per-entry check over one flat node, and "the type table may only contain composite types" (`spec/Candid.md:1227`) holds by construction. That rule still has force at the decoder, which must reject a primitive opcode in an entry position. - `Subty` splits into two mutually coinductive predicates, `Subty` on slots and `SubtyC` on composites, mirroring the procedure. `decSubtype_iff` can now be stated with no side condition about a budget. What it costs: a type means nothing without its table, and even `vec nat` needs an entry, so hand-written types are built with `intern`/`close`. The `.did` surface syntax is nested, so the parser will need a flattening pass -- which is also what an encoder does when it emits a type table. Verified beyond the 79 checks by differencing against the previous model over 250,000 random pairs -- 200,000 flat (expressible in both representations, so the answers must agree exactly) and 50,000 nested and flattened. Zero mismatches in answers and in well-formedness. Also: `ClosedType.ofPrim` replaces `ofSlot`, so the helper cannot build a type whose root is a dangling reference; `simp_wf` is dropped from the termination proofs, unnecessary since Lean 4.12; and a dangling reference is no longer handed the top or bottom rule without being resolved first, which `<:` reported without looking would be the dangerous direction for a compatibility gate. Co-Authored-By: Claude Opus 5 (1M context) --- lean/Candid/Hash.lean | 2 +- lean/Candid/Subtype.lean | 335 ++++++++++++++++------------------- lean/Candid/SubtypeSpec.lean | 111 +++++++----- lean/Candid/TypeExpr.lean | 229 ++++++++++++++---------- lean/Main.lean | 294 +++++++++++++++--------------- lean/README.md | 83 ++++++--- 6 files changed, 569 insertions(+), 485 deletions(-) diff --git a/lean/Candid/Hash.lean b/lean/Candid/Hash.lean index 151ef1a5..8585b2cf 100644 --- a/lean/Candid/Hash.lean +++ b/lean/Candid/Hash.lean @@ -29,6 +29,6 @@ def hashFieldName (name : String) : FieldId := /- 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 `TypeExpr.wellFormed`'s job, not the hash's. -/ +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 index 70f39fd7..346330a6 100644 --- a/lean/Candid/Subtype.lean +++ b/lean/Candid/Subtype.lean @@ -1,8 +1,8 @@ /- Candid subtyping, as a decision procedure over two independent type tables. -Rules are from `spec/Candid.md`, "Upgrading and Subtyping". Two things about that -section shape everything here. +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: @@ -25,65 +25,52 @@ 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 `TypeExpr` 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. +**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 (`TypeExpr.lean`), so the only way to recurse is through a +pair of *references*: every other slot pair is decided outright. The procedure +therefore carries `todo`, the reference pairs it has not yet assumed, and descending +through a pair removes it. `todo.length` is the termination measure, and the +membership test that decides the branch is exactly the fact that measure needs -- so +the obligation is discharged where the decision is made, and no invariant has to be +threaded through the recursion. + +`todo` is the coinductive hypothesis, carried as a complement: a pair this path has +already descended through is one the greatest fixed point lets us assume. Seeding it +costs `|A| x |B|` pairs, and an implementation that carries the assumptions +themselves rather than what is left is bounded by the same count. -/ import Candid.TypeExpr namespace Candid -/-- The result of a subtype question. `none` means the recursion budget ran out. - -Returning `Bool` here would mean reporting "not a subtype" for a question the model -never actually answered. -/ -abbrev Verdict := Option Bool - -namespace Verdict - -/-- Short-circuiting conjunction that preserves "unanswered". -/ -def and (x : Verdict) (y : Unit → Verdict) : Verdict := - match x with - | some true => y () - | some false => some false - | none => none - -/-- `f` holds of every element. Stops at the first `false` or unanswered. -/ -def all (f : α → Verdict) : List α → Verdict - | [] => some true - | x :: xs => match f x with - | some true => all f xs - | r => r - -/-- `f` holds of some element. Stops at the first `true`; an unanswered question -anywhere makes the whole disjunction unanswered, since a later `true` cannot be -ruled out. -/ -def any (f : α → Verdict) : List α → Verdict - | [] => some false - | x :: xs => match f x with - | some false => any f xs - | some true => some true - | none => none - -end Verdict +/-- 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 (e : TypeTable) (t : TypeExpr) : Bool := - match e.resolve t with - | some (.prim .null) | some (.prim .reserved) | some (.opt _) => true - | _ => false +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 TypeExpr → List (FieldId × TypeExpr) +def indexedFrom (i : Nat) : List Slot → List (FieldId × Slot) | [] => [] | t :: ts => (UInt32.ofNat i, t) :: indexedFrom (i + 1) ts @@ -92,154 +79,140 @@ def annotsAgree (xs ys : List FuncAnnot) : Bool := xs.all (ys.contains ·) && ys.all (xs.contains ·) /-- Look up a label. -/ -def fieldAt (fs : List (FieldId × TypeExpr)) (id : FieldId) : Option TypeExpr := +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 × TypeExpr)) (name : String) : Option TypeExpr := +def methodAt (ms : List (String × Slot)) (name : String) : Option Slot := (ms.find? (·.1 == name)).map (·.2) -/- Structural depth, used only to seed the recursion budget. -/ -mutual +/-- Every reference pair of two tables: what `decSubtype` starts out permitted to +assume. -/ +def allPairs (A B : TypeTable) : List (TypeRef × TypeRef) := + (List.range A.size).flatMap fun i => (List.range B.size).map fun j => (i, j) -/-- Structural depth. A `ref` counts as a leaf; unfolding is budgeted separately. -/ -def TypeExpr.depth : TypeExpr → Nat - | .prim _ | .ref _ => 1 - | .opt t | .vec t => 1 + t.depth - | .record fs | .variant fs => 1 + TypeExpr.depthFields fs - | .func args rets _ => 1 + Nat.max (TypeExpr.depthList args) (TypeExpr.depthList rets) - | .service ms => 1 + TypeExpr.depthMethods ms +/-! ## The procedure -def TypeExpr.depthList : List TypeExpr → Nat - | [] => 0 - | t :: ts => Nat.max t.depth (TypeExpr.depthList ts) +`sub A B todo a b` decides `a <: b`, where `a`'s references resolve in `A` and `b`'s +in `B`, and `todo` holds the reference pairs not yet 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. -def TypeExpr.depthFields : List (FieldId × TypeExpr) → Nat - | [] => 0 - | (_, t) :: fs => Nat.max t.depth (TypeExpr.depthFields fs) +The measures below are lexicographic on (`todo.length`, phase), where the phase +orders the three so that a step which does not shrink `todo` still descends: +`subC` (2) may call `subLabels` (1), which may call `sub` (0), which shrinks `todo` +before calling `subC` again. -/ +mutual -def TypeExpr.depthMethods : List (String × TypeExpr) → Nat - | [] => 0 - | (_, t) :: ms => Nat.max t.depth (TypeExpr.depthMethods ms) +def sub (A B : TypeTable) (todo : 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 `todo` shrinks. A + -- pair no longer in `todo` is one this path has already descended through, so the + -- coinductive hypothesis discharges it. A pair that was never in `todo` is out of + -- range, and the lookups catch that first. + | .ref i, .ref j => + match A.lookup? i, B.lookup? j with + | some x, some y => + -- `_hp` is underscored because the value ignores it and the termination proof + -- below does not: it is the whole argument that this recursion stops. + if _hp : (i, j) ∈ todo then subC A B (todo.erase (i, j)) x y else true + | _, _ => false -- dangling: not well formed +termination_by (todo.length, 0) +decreasing_by + exact Prod.Lex.left _ _ (by + rw [List.length_erase_of_mem _hp] + exact Nat.sub_lt (List.length_pos_of_mem _hp) Nat.one_pos) + +/-- The rules on the composites that a pair of references names. -/ +def subC (A B : TypeTable) (todo : 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 todo 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 todo 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 todo 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 `todo` 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 (todo.map Prod.swap) (indexedFrom 1 args') (indexedFrom 1 args) + && subLabels A B todo (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 todo f g + | none => false + + | _, _ => false +termination_by (todo.length, 2) +decreasing_by + -- The parameter premise hands on a swapped `todo`, which is the same length. + all_goals (try simp only [List.length_map]) + 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) (todo : List (TypeRef × TypeRef)) + (fs gs : List (FieldId × Slot)) : Bool := + gs.all fun (id, g) => + match fieldAt fs id with + | some f => sub A B todo f g + | none => B.acceptsNull g +termination_by (todo.length, 1) +decreasing_by exact Prod.Lex.right _ (by omega) end -/-- `sub A B seen fuel a b` decides `a <: b`, where `a`'s references resolve in `A` -and `b`'s in `B`. - -`seen` is the coinductive hypothesis: a pair of *references* already under -consideration. Recursive types make the relation a greatest fixed point, so -re-encountering a pair means the obligation is discharged, not that it failed. - -**Keying the memo on reference pairs is not enough**, and the `vecOmega` checks in -`Main.lean` are the witness: a cycle whose states always have a reference on exactly one side -never reaches this memo point, so `seen` stays empty and no `fuel` value suffices. -Rust keys on *expression* pairs and inserts whenever either side is a variable -(`rust/candid/src/types/subtype.rs:214`), which closes that cycle -- and unfolded -expressions do not in fact nest without bound, since unfolding only ever replaces a -reference at the top, leaving every state a subterm of a root or of an entry. - -So `fuel` is not a placeholder for a measure that exists: for this algorithm there -is none. Either the memo is keyed on expression pairs -- terminating, but the proof -then needs "all reachable states lie in a finite set" threaded through -- or the -representation changes so that every recursive call passes through a reference pair. --/ -def sub (A B : TypeTable) (seen : List (TypeRef × TypeRef)) : Nat → TypeExpr → TypeExpr → Verdict - | 0, _, _ => none - | fuel + 1, a, b => - match a, b with - -- Both sides are references: the memo point. - | .ref i, .ref j => - if seen.contains (i, j) then some true - else match A.lookup? i, B.lookup? j with - | some a', some b' => sub A B ((i, j) :: seen) fuel a' b' - | _, _ => some false -- dangling: not well formed - -- One side is a reference. Well-formed tables hold only composite types, so this - -- unfolds at most once before making structural progress. - | .ref i, _ => - match A.lookup? i with - | some a' => sub A B seen fuel a' b - | none => some false - | _, .ref j => - match B.lookup? j with - | some b' => sub A B seen fuel a b' - | none => some false - - -- ` <: reserved` and `empty <: `: the top and bottom types. - | _, .prim .reserved => some true - | .prim .empty, _ => some true - - -- 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 _ => some true - - | .prim p, .prim q => - -- ` <: `, plus `nat <: int`. `principal` is a primitive - -- (spec/Candid.md:80), so `principal <: principal` needs no rule of its own. - some (p == q || (p == .nat && q == .int)) - - -- `service <: principal`. - | .service _, .prim .principal => some true - - | .vec t, .vec t' => sub A B seen fuel t t' - - -- 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 => - Verdict.all (fun (id, g) => - match fieldAt fs id with - | some f => sub A B seen fuel f g - | none => some (B.acceptsNull g)) 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 => - Verdict.all (fun (id, f) => - match fieldAt gs id with - | some g => sub A B seen fuel f g - | none => some false) fs - - -- 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 must swap the memo with them: an - -- entry `(i, j)` means "A's `i` against B's `j`", and reading it unswapped in the - -- swapped call asserts `B`'s `i` against `A`'s `j` -- a different, and generally - -- false, question. See the `contra` checks in `Main.lean`. - | .func args rets ann, .func args' rets' ann' => - if annotsAgree ann ann' then - Verdict.and - (sub B A (seen.map Prod.swap) fuel - (.record (indexedFrom 1 args')) (.record (indexedFrom 1 args))) - fun _ => sub A B seen fuel (.record (indexedFrom 1 rets)) (.record (indexedFrom 1 rets')) - else some false - - -- Services are records of functions: a method may be specialised or added. - | .service ms, .service ms' => - Verdict.all (fun (name, g) => - match methodAt ms name with - | some f => sub A B seen fuel f g - | none => some false) ms' - - | _, _ => some false - -/-- A budget that is generous rather than tight: every path may unfold each -reference pair once (`|A| x |B|`), descending the structure between unfoldings. -/ -def budgetFor (a b : ClosedType) : Nat := - let pairs := (a.table.size + 1) * (b.table.size + 1) - pairs * (a.root.depth + b.root.depth + 2) + 2 - -/-- Decide `a <: b` for two types carrying their own tables. - -`none` means the budget was exhausted. Well-formed input *can* provoke it -- see -the `vecOmega` checks in `Main.lean` -- so `none` is a real answer callers must handle, not a -theoretical one. -/ -def decSubtype (a b : ClosedType) : Verdict := - sub a.table b.table [] (budgetFor a b) a.root b.root +/-- Decide `a <: b` for two types carrying their own tables. Total: along any path a +reference pair may be assumed at most once, and there are finitely many. -/ +def decSubtype (a b : ClosedType) : Bool := + sub a.table b.table (allPairs 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 the memo 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. -/ +contravariant, so the tables swap with the types -- and `todo` 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 index 2c731a6e..ecd14e47 100644 --- a/lean/Candid/SubtypeSpec.lean +++ b/lean/Candid/SubtypeSpec.lean @@ -11,7 +11,7 @@ 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 `TypeExpr` is finite with explicit references), so the same +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 @@ -19,6 +19,11 @@ 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. -/ @@ -27,7 +32,9 @@ import Candid.Subtype namespace Candid -coinductive Subty : TypeTable → TypeTable → TypeExpr → TypeExpr → Prop where +mutual + +coinductive Subty : TypeTable → TypeTable → Slot → Slot → Prop where /-- ` <: ` -/ | prim {A B p} : Subty A B (.prim p) (.prim p) /-- `nat <: int` -/ @@ -38,81 +45,101 @@ coinductive Subty : TypeTable → TypeTable → TypeExpr → TypeExpr → Prop w | 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 ms} : Subty A B (.service ms) (.prim .principal) - /-- All four `opt` rules of the spec, collapsed. Any type is a subtype of any - option; a receiver that cannot decode the value sees `null`. -/ - | toOpt {A B a b} : Subty A B a (.opt b) + | 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 `todo` 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 t t'} : Subty A B t t' → Subty A B (.vec t) (.vec t') + | 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)) → - Subty A B (.record fs) (.record gs) + 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) → - Subty A B (.variant fs) (.variant gs) + 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 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 → - Subty B A (.record (indexedFrom 1 args')) (.record (indexedFrom 1 args)) → - Subty A B (.record (indexedFrom 1 rets)) (.record (indexedFrom 1 rets')) → - Subty A B (.func args rets ann) (.func args' rets' ann') + 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) → - Subty A B (.service ms) (.service ms') - /-- References are transparent: a type is related through its table entry. -/ - | unfoldLeft {A B i a' b} : - A.lookup? i = some a' → Subty A B a' b → Subty A B (.ref i) b - | unfoldRight {A B a j b'} : - B.lookup? j = some b' → Subty A B a b' → Subty A B a (.ref j) + 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 in slice 2. -/ -example (A B : TypeTable) : Subty A B (.prim .nat) (.prim .int) := Subty.natInt +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 -example (A B : TypeTable) (t : TypeExpr) : Subty A B (.prim .text) (.opt t) := Subty.toOpt +/-- 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) (a : TypeExpr) : Subty A B a (.prim .reserved) := Subty.toReserved +example (A B : TypeTable) : SubtyC A B (.vec .nat) (.vec .int) := SubtyC.vec Subty.natInt -example (A B : TypeTable) : Subty A B (.vec (.prim .nat)) (.vec (.prim .int)) := - Subty.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 × TypeExpr)) : - Subty A B (.record fs) (.record []) := by - apply Subty.record +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 proof of the next slice: - theorem decSubtype_iff (a b : ClosedType) - (ha : a.wellFormed = true) (hb : b.wellFormed = true) : - decSubtype a b = some true <-> Subty a.table b.table a.root b.root - -Soundness (`some true` implies `Subty`) should follow by coinduction on the -procedure's recursion, with `seen` as the coinductive hypothesis -- that is what -`seen` *means*, and stating it this way is what will confirm the memo is keyed -correctly. - -The completeness direction is **false of the current procedure**, not merely -unproved: the `vecOmega` pair in `Main.lean` is well formed and satisfies `Subty` -(close the -consistent set under `unfoldLeft`, `unfoldRight` and `vec`), while `decSubtype` -returns `none` on it for every budget. Stating the theorem is therefore blocked on -the procedure, not on the proof -- see the header of `Subtype.lean`. + 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 *missing* from `todo` as the coinductive hypothesis -- that +is what `todo` 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 diff --git a/lean/Candid/TypeExpr.lean b/lean/Candid/TypeExpr.lean index 78c204a0..a675ef02 100644 --- a/lean/Candid/TypeExpr.lean +++ b/lean/Candid/TypeExpr.lean @@ -1,5 +1,5 @@ /- -The Candid type language, represented finitely. +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, @@ -11,8 +11,37 @@ 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. -On the name: the old implementation calls this a `TypeEnv`, but its `TypeEnv` is a -`BTreeMap` (`rust/candid/src/types/type_env.rs:7`) -- a *name*-keyed +**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:1207`): + +``` +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. @@ -41,111 +70,90 @@ inductive FuncAnnot where | query | oneway | compositeQuery deriving DecidableEq, Repr -/-- A Candid type, possibly containing references into an accompanying `TypeTable`. -/ -inductive TypeExpr where +/-- 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) - | opt (inner : TypeExpr) - | vec (inner : TypeExpr) - | record (fields : List (FieldId × TypeExpr)) - | variant (alts : List (FieldId × TypeExpr)) - | func (args rets : List TypeExpr) (annots : List FuncAnnot) - | service (methods : List (String × TypeExpr)) | 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` -> `TypeExpr`. -/ +/-- A type table: `TypeRef` -> `Composite`. -/ structure TypeTable where - entries : Array TypeExpr + entries : Array Composite deriving Repr, Inhabited namespace TypeTable def size (t : TypeTable) : Nat := t.entries.size -def lookup? (t : TypeTable) (r : TypeRef) : Option TypeExpr := t.entries[r]? +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 -def TypeExpr.isRef : TypeExpr → Bool - | .ref _ => true - | _ => false - -/-- Is this a ``, i.e. a `` or a ``? - -`spec/Candid.md:1227` -- "The type table may only contain composite types (no -``)". So this is exactly what may appear as a table entry, and it excludes -both primitives and bare references. -/ -def TypeExpr.isComposite : TypeExpr → Bool - | .opt _ | .vec _ | .record _ | .variant _ | .func _ _ _ | .service _ => true - | .prim _ | .ref _ => false - /-- 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 of a type expression against a table of `bound` entries: -every reference resolves, and no record, variant or service repeats a label. +/-! ## Well-formedness -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. -/ -mutual +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. -/ -/-- Every reference resolves below `bound`, and no label is repeated. -/ -def TypeExpr.wellFormed (bound : Nat) : TypeExpr → Bool +/-- Does this slot's reference resolve below `bound`? -/ +def Slot.wellFormed (bound : Nat) : Slot → Bool | .prim _ => true | .ref r => r < bound - | .opt t | .vec t => t.wellFormed bound - | .record fs | .variant fs => noDups (fs.map (·.1)) && TypeExpr.wfFields bound fs - | .func args rets _ => TypeExpr.wfList bound args && TypeExpr.wfList bound rets - | .service ms => noDups (ms.map (·.1)) && TypeExpr.wfMethods bound ms - -def TypeExpr.wfList (bound : Nat) : List TypeExpr → Bool - | [] => true - | t :: ts => t.wellFormed bound && TypeExpr.wfList bound ts - -def TypeExpr.wfFields (bound : Nat) : List (FieldId × TypeExpr) → Bool - | [] => true - | (_, t) :: fs => t.wellFormed bound && TypeExpr.wfFields bound fs -def TypeExpr.wfMethods (bound : Nat) : List (String × TypeExpr) → Bool - | [] => true - | (_, t) :: ms => t.wellFormed bound && TypeExpr.wfMethods bound ms +/-- 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) -end +/-- 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 -/-- A table is well formed when every entry is well formed **and composite**. +def Composite.wellFormed (bound : Nat) (c : Composite) : Bool := + c.labelsOk && c.slots.all (Slot.wellFormed bound) -The second condition is the spec's own (`spec/Candid.md:1227`), and it is load-bearing -here: since no entry is a primitive or a bare reference, following a reference is a -single step, which is what bounds the subtype recursion. Textual `.did` aliases -(`type A = B;`) must therefore be resolved before they reach this model. -/ def TypeTable.wellFormed (t : TypeTable) : Bool := - t.entries.all fun e => e.wellFormed t.size && e.isComposite - -/-- Follow at most one reference. Returns `none` on a dangling index. - -In a well-formed table the result is never itself a `ref`. That is not yet expressed -in the type, so `Subtype.lean` bounds unfolding explicitly instead of relying on it. -/ -def TypeTable.resolve (t : TypeTable) (e : TypeExpr) : Option TypeExpr := - match e with - | .ref r => t.lookup? r - | _ => some e + t.entries.all (Composite.wellFormed t.size) /-- A type together with the table its references resolve in. -This is the unit the public API speaks in, because a `TypeExpr` containing a `ref` -means nothing without its table. The first draft of `decSubtype` took one table and -two `TypeExpr`s, which silently assumed both types 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. -/ +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 : TypeExpr + root : Slot deriving Repr, Inhabited namespace ClosedType @@ -153,43 +161,70 @@ namespace ClosedType def wellFormed (c : ClosedType) : Bool := c.table.wellFormed && c.root.wellFormed c.table.size -/-- A type containing no references. -/ -def ofExpr (e : TypeExpr) : ClosedType := { table := .empty, root := e } +/-- 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 TypeExpr - -def null : TypeExpr := .prim .null -def bool : TypeExpr := .prim .bool -def nat : TypeExpr := .prim .nat -def int : TypeExpr := .prim .int -def nat8 : TypeExpr := .prim .nat8 -def nat16 : TypeExpr := .prim .nat16 -def nat32 : TypeExpr := .prim .nat32 -def nat64 : TypeExpr := .prim .nat64 -def int8 : TypeExpr := .prim .int8 -def int16 : TypeExpr := .prim .int16 -def int32 : TypeExpr := .prim .int32 -def int64 : TypeExpr := .prim .int64 -def float32 : TypeExpr := .prim .float32 -def float64 : TypeExpr := .prim .float64 -def text : TypeExpr := .prim .text -def reserved : TypeExpr := .prim .reserved -def empty : TypeExpr := .prim .empty -def principal : TypeExpr := .prim .principal +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 × TypeExpr)) : TypeExpr := +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 × TypeExpr)) : TypeExpr := +def variantOf (fs : List (String × Slot)) : Composite := .variant (fs.map fun (n, t) => (hashFieldName n, t)) -end TypeExpr +end Composite end Candid diff --git a/lean/Main.lean b/lean/Main.lean index 36c4746d..38830b4f 100644 --- a/lean/Main.lean +++ b/lean/Main.lean @@ -5,42 +5,45 @@ Slice 1 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 +(`TypeExpr.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.TypeExpr +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. -/ + 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 } -def verdictStr : Verdict → String - | some true => "<:" - | some false => "!<:" - | none => "budget exhausted" +/-- A type that needs no table: a primitive. -/ +def atom (p : Prim) : ClosedType := .ofPrim p -/-- A subtype question about two types that carry no references. -/ -def expectSub (a b : TypeExpr) (want : Bool) (name : String) : Check := - let got := decSubtype (.ofExpr a) (.ofExpr b) - { name := name - ok := got == some want - detail := s!"got {verdictStr got}, want {verdictStr (some want)}" } +/-- A type that is one composite, named by the root. -/ +def entry (c : Composite) : ClosedType := closeOne c -/-- A subtype question about two types with their own type tables. -/ -def expectSubIn (a b : ClosedType) (want : Bool) (name : String) : Check := +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 == some want - detail := s!"got {verdictStr got}, want {verdictStr (some want)}" } + ok := got == want + detail := s!"got {relStr got}, want {relStr want}" } def expectHash (input : String) (want : UInt32) : Check := let got := hashFieldName input @@ -69,19 +72,19 @@ def hashChecks : List Check := /-! ## Primitives, top and bottom -/ def primChecks : List Check := - [ expectSub nat nat true "nat <: nat" - , expectSub nat int true "nat <: int" - , expectSub int nat false "int !<: nat" - , expectSub nat8 nat false "nat8 !<: nat (no width subtyping)" - , expectSub nat nat8 false "nat !<: nat8" - , expectSub nat32 int32 false "nat32 !<: int32" - , expectSub text reserved true "text <: reserved" - , expectSub (.func [] [] []) reserved true "func <: reserved" - , expectSub empty text true "empty <: text" - , expectSub empty (.vec nat) true "empty <: vec nat" - , expectSub text nat false "text !<: nat" - , expectSub (.service []) .principal true "service <: principal" - , expectSub .principal (.service []) false "principal !<: service" ] + [ 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 @@ -90,20 +93,21 @@ negative premises eliminated. The `text <: opt nat` case is the surprising one, it is deliberate: a receiver that cannot decode the value sees `null`. -/ def optChecks : List Check := - [ expectSub nat (.opt nat) true "nat <: opt nat" - , expectSub null (.opt nat) true "null <: opt nat" - , expectSub reserved (.opt nat) true "reserved <: opt nat" - , expectSub text (.opt nat) true "text <: opt nat (special opt rule)" - , expectSub (.opt text) (.opt nat) true "opt text <: opt nat (special opt rule)" - , expectSub (.opt nat) nat false "opt nat !<: nat" - , expectSub (.opt nat) reserved true "opt nat <: reserved" ] + [ 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 (.vec nat) (.vec int) true "vec nat <: vec int" - , expectSub (.vec int) (.vec nat) false "vec int !<: vec nat" - , expectSub (.vec nat) nat false "vec nat !<: nat" ] + [ 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 @@ -111,22 +115,27 @@ A subtype may add fields and specialise field types. It may also *omit* a field 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 (recordOf [("x", nat)]) (recordOf []) true + [ expectSub (entry (recordOf [("x", nat)])) (entry (recordOf [])) true "record {x:nat} <: record {}" - , expectSub (recordOf [("x", nat), ("y", text)]) (recordOf [("x", nat)]) true - "record {x;y} <: record {x} (field added)" - , expectSub (recordOf [("x", nat)]) (recordOf [("x", int)]) true + , 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 (recordOf [("x", int)]) (recordOf [("x", nat)]) false + , expectSub (entry (recordOf [("x", int)])) (entry (recordOf [("x", nat)])) false "record {x:int} !<: record {x:nat}" - , expectSub (recordOf [("x", nat)]) (recordOf [("x", nat), ("y", .opt text)]) true + , expectSub (entry (recordOf [("x", nat)])) recordWithOptField true "record {x} <: record {x; y:opt text} (omitted field accepts null)" - , expectSub (recordOf [("x", nat)]) (recordOf [("x", nat), ("y", reserved)]) true - "record {x} <: record {x; y:reserved}" - , expectSub (recordOf [("x", nat)]) (recordOf [("x", nat), ("y", text)]) false - "record {x} !<: record {x; y:text} (omitted field rejects null)" - , expectSub (recordOf [("x", nat)]) (recordOf [("y", nat)]) false + , 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 @@ -134,16 +143,21 @@ def recordChecks : List Check := 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 (variantOf []) (variantOf [("a", nat)]) true + [ expectSub (entry (variantOf [])) (entry (variantOf [("a", nat)])) true "variant {} <: variant {a}" - , expectSub (variantOf [("a", nat)]) (variantOf [("a", nat), ("b", text)]) true - "variant {a} <: variant {a; b} (tag dropped)" - , expectSub (variantOf [("a", nat), ("b", text)]) (variantOf [("a", nat)]) false - "variant {a; b} !<: variant {a} (tag added)" - , expectSub (variantOf [("a", nat)]) (variantOf [("a", int)]) true + , 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 (.opt (variantOf [("a", nat), ("b", text)])) (.opt (variantOf [("a", nat)])) true + , expectSub (optVariant [("a", nat), ("b", text)]) (optVariant [("a", nat)]) true "opt variant {a; b} <: opt variant {a} (tag added behind opt)" ] /-! ## Functions @@ -162,47 +176,65 @@ symmetric, and it is worth spelling out which is which: 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 (.func [int] [nat] []) (.func [nat] [int] []) true + [ expectSub (entry (.func [int] [nat] [])) (entry (.func [nat] [int] [])) true "func (int) -> (nat) <: func (nat) -> (int)" - , expectSub (.func [nat] [int] []) (.func [int] [nat] []) false + , 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 (.func [] [] []) (.func [nat] [] []) true + , expectSub (entry (.func [] [] [])) (entry (.func [nat] [] [])) true "func () -> () <: func (nat) -> () (parameter dropped, always allowed)" - , expectSub (.func [.opt nat] [] []) (.func [] [] []) true + , expectSub funcOptParam (entry (.func [] [] [])) true "func (opt nat) -> () <: func () -> () (optional parameter added)" - , expectSub (.func [nat] [] []) (.func [] [] []) false + , expectSub (entry (.func [nat] [] [])) (entry (.func [] [] [])) false "func (nat) -> () !<: func () -> () (added parameter rejects null)" -- Results: adding is free, dropping needs to accept null. - , expectSub (.func [] [nat] []) (.func [] [] []) true + , expectSub (entry (.func [] [nat] [])) (entry (.func [] [] [])) true "func () -> (nat) <: func () -> () (result added, always allowed)" - , expectSub (.func [] [] []) (.func [] [.opt nat] []) true + , expectSub (entry (.func [] [] [])) funcOptResult true "func () -> () <: func () -> (opt nat) (optional result dropped)" - , expectSub (.func [] [] []) (.func [] [nat] []) false + , expectSub (entry (.func [] [] [])) (entry (.func [] [nat] [])) false "func () -> () !<: func () -> (nat) (dropped result rejects null)" - , expectSub (.func [] [] [.query]) (.func [] [] []) false + , expectSub (entry (.func [] [] [.query])) (entry (.func [] [] [])) false "annotations must agree" - , expectSub (.func [] [] [.query]) (.func [] [] [.query]) true + , expectSub (entry (.func [] [] [.query])) (entry (.func [] [] [.query])) true "matching annotations agree" ] -/-! ## Services -/ +/-! ## 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:1221`), 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 (.service [("m", .func [] [] [])]) (.service []) true + [ expectSub (serviceOf [("m", .func [] [] [])]) (serviceOf []) true "service {m} <: service {}" - , expectSub (.service []) (.service [("m", .func [] [] [])]) false + , expectSub (serviceOf []) (serviceOf [("m", .func [] [] [])]) false "service {} !<: service {m}" - , expectSub (.service [("m", .func [] [nat] [])]) (.service [("m", .func [] [] [])]) true + , expectSub (serviceOf [("m", .func [] [nat] [])]) (serviceOf [("m", .func [] [] [])]) true "service method specialised" ] /-! ## Recursive types across two independent tables -These are the cases the reference-pair memo exists for. `selfLoop` and `twoCycle` -denote the same infinite type through different table shapes, and every state on -their cycle has a reference on *both* sides, so the memo fires and the recursion -stops. `vecOmega` below is the same idea with the references on alternating sides, -where it does not. -/ +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 removes it from +`todo`, and meeting that pair again means the obligation is already assumed. -/ /-- `type S = record { next : S }`, as one self-referential entry. -/ def selfLoop : ClosedType := @@ -214,91 +246,75 @@ def twoCycle : ClosedType := root := .ref 0 } /-- `type S = record { next : S; extra : nat }`. -/ -def selfLoopWith (extra : TypeExpr) : ClosedType := +def selfLoopWith (extra : Slot) : ClosedType := { table := { entries := #[ recordOf [("next", .ref 0), ("extra", extra)] ] }, root := .ref 0 } -/-- A table entry that is a bare reference: rejected, and it is the reference case -that would otherwise make following a reference an unbounded walk. -/ -def bareRefEntry : ClosedType := - { table := { entries := #[ .ref 0 ] }, root := .ref 0 } - -/-- A table entry that is a primitive: also rejected. `spec/Candid.md:1227` -- "The -type table may only contain composite types (no ``)." -/ -def primEntry : ClosedType := - { table := { entries := #[ nat ] }, root := .ref 0 } - /-- A reference with no entry to resolve to. -/ -def danglingRef : ClosedType := - { table := { entries := #[] }, root := .ref 3 } +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 := - [ expectSubIn selfLoop selfLoop true - "self-loop <: itself (memo terminates)" - , expectSubIn selfLoop twoCycle true + [ 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)" - , expectSubIn twoCycle selfLoop true + , expectSub twoCycle selfLoop true "two-cycle <: self-loop" - , expectSubIn (selfLoopWith nat) (selfLoopWith int) true + , expectSub (selfLoopWith nat) (selfLoopWith int) true "recursive record, field specialised" - , expectSubIn (selfLoopWith int) (selfLoopWith nat) false + , expectSub (selfLoopWith int) (selfLoopWith nat) false "recursive record, field not specialised" - , expectSubIn (selfLoopWith nat) selfLoop true + , 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 bareRefEntry false "bare reference as a table entry is malformed" - , expectWellFormed primEntry false "primitive as a table entry is malformed" - , expectWellFormed (.ofExpr principal) true "principal is a primitive, not a reftype" + , expectWellFormed (atom .principal) true "principal is a primitive, not a reftype" , expectWellFormed danglingRef false "dangling reference is malformed" - , expectWellFormed (.ofExpr (.record [(0, nat), (0, text)])) false + -- 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 the reference-pair memo does not catch - -`T.0 = vec (vec T.0)`, so `ref 0` and `vec (ref 0)` denote the same infinite type, -`vec (vec (vec ...))`. Both are well formed and both directions are `true`. - -The memo never fires, because every state on the cycle has a reference on exactly -one side: - - (ref 0, vec (ref 0)) - -> (vec (vec (ref 0)), vec (ref 0)) unfold left - -> (vec (ref 0), ref 0) descend - -> (vec (ref 0), vec (vec (ref 0))) unfold right - -> (ref 0, vec (ref 0)) descend -- back to the start +/-! ## `vec`-omega: a cycle that alternates sides -`seen` stays empty, so `decSubtype` returns `none` and no larger `fuel` helps. These -two are recorded as known gaps: `expectSubIn` states the answer the model owes, and -the run reports it as `known` until the representation or the memo keying changes. -/ +`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. -def vecOmegaTable : TypeTable := { entries := #[ .vec (.vec (.ref 0)) ] } +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 taken out of `todo`. -/ -/-- `vec`-omega as a reference. -/ -def vecOmegaRef : ClosedType := { table := vecOmegaTable, root := .ref 0 } +def vecOmegaTable : TypeTable := { entries := #[ .vec (.ref 1), .vec (.ref 0) ] } -/-- The same type, one `vec` unrolled ahead of the reference. -/ -def vecOmegaUnrolled : ClosedType := { table := vecOmegaTable, root := .vec (.ref 0) } +def vecOmegaEven : ClosedType := { table := vecOmegaTable, root := .ref 0 } +def vecOmegaOdd : ClosedType := { table := vecOmegaTable, root := .ref 1 } def vecOmegaChecks : List Check := - [ expectWellFormed vecOmegaRef true "vec-omega: ref 0 is well formed" - , expectWellFormed vecOmegaUnrolled true "vec-omega: vec (ref 0) is well formed" - , (expectSubIn vecOmegaRef vecOmegaUnrolled true - "vec-omega <: its own unrolling").asKnown - , (expectSubIn vecOmegaUnrolled vecOmegaRef true - "vec-omega's unrolling <: it").asKnown ] + [ 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: the memo swaps with the tables +/-! ## Contravariance: `todo` swaps with the tables The parameter premise of the function rule swaps the two tables, so it must swap the -memo with them. An entry `(i, j)` asserts `A`'s `i` against `B`'s `j`; read unswapped -inside the swapped call it asserts `B`'s `i` against `A`'s `j`, which is a different -question, and subtyping is not symmetric. +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 puts `(1, 2)` in the memo, -so an unswapped read answers it `true` from the memo and both queries come out -`true`. -/ +i.e. `vec text <: vec nat` -- false. Reaching that premise takes `(1, 2)` out of +`todo`, so a procedure that read `todo` 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 := @@ -317,9 +333,9 @@ 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" - , expectSubIn contraFuncs contraFuncs' false + , expectSub contraFuncs contraFuncs' false "func (vec nat) -> () !<: func (vec text) -> () (parameter premise fails)" - , expectSubIn contraOuter contraOuter' false + , expectSub contraOuter contraOuter' false "record { f : func (vec nat) -> () } !<: record { f : func (vec text) -> () }" ] /-! ## Transitivity spot-check @@ -329,9 +345,9 @@ preserve it. This is not a proof -- it is the shape the eventual property test a the Lean theorem take. -/ def transitivityChecks : List Check := - let a := recordOf [("x", nat)] - let b := recordOf [("x", nat), ("y", .opt text)] - let c := recordOf [("x", int)] + 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" ] diff --git a/lean/README.md b/lean/README.md index 29ce094e..4166e17c 100644 --- a/lean/README.md +++ b/lean/README.md @@ -22,8 +22,8 @@ via [Verso](https://github.com/leanprover/verso), the **specification document** **Executable first, proved second.** -1. `TypeExpr`, `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. @@ -57,15 +57,44 @@ notes this in prose and `rust/candid/src/types/subtype.rs:293` implements it as 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:1207`), 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 `todo` — the pairs it has not yet assumed — descends by removing +one, and `todo.length` is the termination measure. 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: `TypeExpr`, `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 +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. -`TypeTable` rather than the old implementation's `TypeEnv` for two reasons. The spec +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` still records +`TypeExpr` for "one structural node; may contain references", which is the shape this +model just abandoned; deciding whether the Rust crates follow is a separate call. + +`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` @@ -78,16 +107,20 @@ Both will exist here eventually, so `TypeEnv` stays reserved for the one where transcription of its Lean counterpart, and shared identifiers are most of what makes that checkable. -**Subtyping relates two type tables, not one.** A `TypeExpr` holding a `ref` means +**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. Two consequences fall out of separating -them: the memo must be keyed on **reference pairs**, since unfolded expressions nest -without bound while reference pairs are bounded by `|A| x |B|`; and the `func` rule's -contravariance swaps the *tables* along with the types, which is invisible when there -is only one table to swap. +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 @@ -119,21 +152,21 @@ cover what actually breaks in production: Named here so they are obligations rather than oversights. -- **`fuel` in `Candid/Subtype.lean`.** The procedure bounds recursion depth with a - budget instead of a termination measure, and returns `none` — not `false` — when it - runs out, so the model never reports an answer it did not compute. The intended - measure is lexicographic on (reference pairs not yet in `seen`, structural size); - proving it needs `TypeTable.wellFormed`'s "every entry is composite" invariant - carried in the type rather than checked separately. - **`decSubtype_iff`** — that the procedure decides the relation. Stated in [Candid/SubtypeSpec.lean](Candid/SubtypeSpec.lean). Soundness should follow by - coinduction with `seen` as the coinductive hypothesis, which is what `seen` means; - completeness additionally needs the budget never to run out. -- **Unguarded recursion.** `TypeTable.wellFormed` requires every entry to be a - `` — the spec's own rule (`spec/Candid.md:1227`), which rules out both - primitives and bare references — but it does not yet require recursion to be - *productive*. Textual `.did` aliases (`type A = B;`) must be resolved before - reaching this model. + coinduction, with the pairs *missing* from `todo` as the coinductive hypothesis, + which is what `todo` means. There is no longer a budget premise to discharge: the + procedure returns `Bool` and is total. +- **The pair accounting is path-scoped and seeded eagerly.** `decSubtype` starts from + all `|A| x |B|` reference pairs, and `todo` is threaded down a path rather than + shared between siblings. That is a faithful reading of the coinductive hypothesis + and it is what makes the termination measure need no side conditions, but sharing + the accounting across siblings is also sound for a greatest fixed point and is how + an implementation gets a polynomial bound with no eager allocation. +- **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 in slice 1: bundling an undocumented doc toolchain into the slice whose purpose was de-risking the build would have doubled the unknowns. From 28a6ecd893b83aea9c0d83a0d1c045ead928323a Mon Sep 17 00:00:00 2001 From: Linwei Shang Date: Tue, 25 Aug 2026 21:26:37 -0400 Subject: [PATCH 5/7] lean: rename TypeExpr.lean to Types.lean, and record Slot/Composite in crates/ The module was named after a type it no longer defines. It holds `Slot`, `Composite`, `TypeTable` and `ClosedType`, so `Types.lean` is what it is. `crates/README.md` and `REWRITE.md` carried the same stale name in the planned `candid_types` layer, still describing `TypeExpr` as "one structural node; may contain references" -- the shape the model dropped. Identifiers are shared between `lean/` and `crates/` precisely so that "candid_subtype reads as a transcription of its Lean counterpart" stays checkable, so the naming table now records `Slot` and `Composite` with the reason neither takes the `Type` prefix: neither is a type, and both are named after the grammar position they occupy in the spec. Co-Authored-By: Claude Opus 5 (1M context) --- REWRITE.md | 6 +++--- crates/README.md | 20 ++++++++++++++------ lean/Candid.lean | 2 +- lean/Candid/Subtype.lean | 4 ++-- lean/Candid/{TypeExpr.lean => Types.lean} | 0 lean/Main.lean | 2 +- lean/README.md | 6 +++--- 7 files changed, 24 insertions(+), 16 deletions(-) rename lean/Candid/{TypeExpr.lean => Types.lean} (100%) diff --git a/REWRITE.md b/REWRITE.md index b406c42d..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 TypeExpr, TypeTable, TypeRef, FieldId, ClosedType, 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 <-> (TypeTable, 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), diff --git a/crates/README.md b/crates/README.md index f8ca5d4f..865dcf0c 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 TypeExpr, TypeTable, TypeRef, FieldId, ClosedType, 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 <-> (TypeTable, 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), @@ -66,10 +66,11 @@ counterpart" into a checkable property rather than an aspiration. | | | |---|---| -| `TypeExpr` | one structural node; may contain references | -| `TypeTable` | `TypeRef` → `TypeExpr`, index-keyed — what the spec calls the type definition table | +| `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 `TypeExpr` together | +| `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 | @@ -78,6 +79,13 @@ counterpart" into a checkable property rather than an aspiration. [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:1207`) 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 diff --git a/lean/Candid.lean b/lean/Candid.lean index 6c42ad0c..76d819a3 100644 --- a/lean/Candid.lean +++ b/lean/Candid.lean @@ -6,6 +6,6 @@ here is reachable from the `oracle` executable, or a proof about something that -/ import Candid.Hash -import Candid.TypeExpr +import Candid.Types import Candid.Subtype import Candid.SubtypeSpec diff --git a/lean/Candid/Subtype.lean b/lean/Candid/Subtype.lean index 346330a6..162a64ba 100644 --- a/lean/Candid/Subtype.lean +++ b/lean/Candid/Subtype.lean @@ -32,7 +32,7 @@ takes a single `env` for both types (`rust/candid/src/types/subtype.rs:19`), whi 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 (`TypeExpr.lean`), so the only way to recurse is through a +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 therefore carries `todo`, the reference pairs it has not yet assumed, and descending through a pair removes it. `todo.length` is the termination measure, and the @@ -46,7 +46,7 @@ costs `|A| x |B|` pairs, and an implementation that carries the assumptions themselves rather than what is left is bounded by the same count. -/ -import Candid.TypeExpr +import Candid.Types namespace Candid diff --git a/lean/Candid/TypeExpr.lean b/lean/Candid/Types.lean similarity index 100% rename from lean/Candid/TypeExpr.lean rename to lean/Candid/Types.lean diff --git a/lean/Main.lean b/lean/Main.lean index 38830b4f..b188f9e9 100644 --- a/lean/Main.lean +++ b/lean/Main.lean @@ -7,7 +7,7 @@ into the differential oracle that reads conformance vectors -- at which point th checks become the first vectors. Every type here carries a table, because composites live only in the table -(`TypeExpr.lean`). `atom` is a primitive, `entry` is a single composite, and +(`Types.lean`). `atom` is a primitive, `entry` is a single composite, and `close do ... intern ...` builds the two-or-more-entry cases. -/ diff --git a/lean/README.md b/lean/README.md index 4166e17c..f230a030 100644 --- a/lean/README.md +++ b/lean/README.md @@ -90,9 +90,9 @@ The two names the flat representation introduced are borrowed from the spec's gr 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` still records -`TypeExpr` for "one structural node; may contain references", which is the shape this -model just abandoned; deciding whether the Rust crates follow is a separate call. +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 From 78983a22dddc152258fc9ae912dea424ee2b697c Mon Sep 17 00:00:00 2001 From: Linwei Shang Date: Wed, 26 Aug 2026 16:48:24 -0400 Subject: [PATCH 6/7] lean: record assumed pairs instead of carrying their complement `decSubtype` was roughly cubic. The procedure carried `todo`, the reference pairs not yet assumed, seeded with all `|A| x |B|` of them and narrowed by `todo.erase (i, j)` at each descent -- and `List.erase` copies the list up to the erased element. Compiled, on a table of `n` entries in one long cycle: n=100 23 ms n=300 370 ms n=1000 14.3 s n=2000 >100 s A 1000-entry type table is 2-3 KB on the wire, so that is the same shape as a cheap-bytes/expensive-work bug, in the artifact meant to become a differential fuzzing oracle. The complement was only ever there to be a termination measure. So the procedure now carries `seen` -- the pairs this path *has* assumed, one cons per descent, membership by a scan no longer than the path -- and the measure moves into `remaining`, which counts the pairs `seen` does not record. `termination_by` measures are erased, so the pair space is never built when the procedure runs. Same total process time on the same tables: n=1000 <10 ms n=10000 70 ms n=50000 1.6 s n=400000 113 s, and no stack overflow at that depth The two facts the measure needs are produced by the branch that makes the decision: the guard says the pair is fresh, and the table lookups say its indices are in range. So there is still no invariant threaded through the recursion. `remaining` counts both orientations of the pair space, which is what makes the function rule's table swap leave the measure alone -- proved as `remaining_swap` rather than assumed. The one general lemma this needs is `countP_cons_lt`: a `countP` over a list drops when the predicate flips to `false` on one member that is present, and nowhere gains. That is the whole of the proof obligation; no pigeonhole argument and no mathlib. Verified unchanged by differencing against the pre-rewrite model again: 50,000 random flat pairs and 20,000 random nested pairs, zero mismatches, plus reflexivity, top, bottom and transitivity over 20,000 random well-formed types. Co-Authored-By: Claude Opus 5 (1M context) --- lean/Candid/Subtype.lean | 174 +++++++++++++++++++++++++---------- lean/Candid/SubtypeSpec.lean | 6 +- lean/Main.lean | 12 +-- lean/README.md | 27 +++--- 4 files changed, 150 insertions(+), 69 deletions(-) diff --git a/lean/Candid/Subtype.lean b/lean/Candid/Subtype.lean index 162a64ba..73d06cf2 100644 --- a/lean/Candid/Subtype.lean +++ b/lean/Candid/Subtype.lean @@ -32,18 +32,19 @@ takes a single `env` for both types (`rust/candid/src/types/subtype.rs:19`), whi 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 -therefore carries `todo`, the reference pairs it has not yet assumed, and descending -through a pair removes it. `todo.length` is the termination measure, and the -membership test that decides the branch is exactly the fact that measure needs -- so -the obligation is discharged where the decision is made, and no invariant has to be +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. - -`todo` is the coinductive hypothesis, carried as a complement: a pair this path has -already descended through is one the greatest fixed point lets us assume. Seeding it -costs `|A| x |B|` pairs, and an implementation that carries the assumptions -themselves rather than what is left is bounded by the same count. -/ import Candid.Types @@ -86,26 +87,97 @@ def fieldAt (fs : List (FieldId × Slot)) (id : FieldId) : Option Slot := def methodAt (ms : List (String × Slot)) (name : String) : Option Slot := (ms.find? (·.1 == name)).map (·.2) -/-- Every reference pair of two tables: what `decSubtype` starts out permitted to -assume. -/ +/-! ## 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 todo a b` decides `a <: b`, where `a`'s references resolve in `A` and `b`'s -in `B`, and `todo` holds the reference pairs not yet assumed. `subC` is the same +`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 (`todo.length`, phase), where the phase -orders the three so that a step which does not shrink `todo` still descends: -`subC` (2) may call `subLabels` (1), which may call `sub` (0), which shrinks `todo` -before calling `subC` again. -/ +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) (todo : List (TypeRef × TypeRef)) : Slot → Slot → Bool +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 @@ -130,88 +202,92 @@ def sub (A B : TypeTable) (todo : List (TypeRef × TypeRef)) : Slot → Slot → | .principal, some (.service _) => true | _, _ => false - -- Two references: the only recursive case, and the only place `todo` shrinks. A - -- pair no longer in `todo` is one this path has already descended through, so the - -- coinductive hypothesis discharges it. A pair that was never in `todo` is out of - -- range, and the lookups catch that first. + -- 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 => - match A.lookup? i, B.lookup? j with + -- 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 => - -- `_hp` is underscored because the value ignores it and the termination proof - -- below does not: it is the whole argument that this recursion stops. - if _hp : (i, j) ∈ todo then subC A B (todo.erase (i, j)) x y else true + if _hs : seen.contains (i, j) then true + else subC A B ((i, j) :: seen) x y | _, _ => false -- dangling: not well formed -termination_by (todo.length, 0) +termination_by (remaining A B seen, 0) decreasing_by - exact Prod.Lex.left _ _ (by - rw [List.length_erase_of_mem _hp] - exact Nat.sub_lt (List.length_pos_of_mem _hp) Nat.one_pos) + -- 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) (todo : List (TypeRef × TypeRef)) : Composite → Composite → Bool +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 todo x y + | .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 todo fs gs + | .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 todo f g + | 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 `todo` with them: a pair + -- 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 (todo.map Prod.swap) (indexedFrom 1 args') (indexedFrom 1 args) - && subLabels A B todo (indexedFrom 1 rets) (indexedFrom 1 rets') + && 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 todo f g + | some f => sub A B seen f g | none => false | _, _ => false -termination_by (todo.length, 2) +termination_by (remaining A B seen, 2) decreasing_by - -- The parameter premise hands on a swapped `todo`, which is the same length. - all_goals (try simp only [List.length_map]) + -- 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) (todo : List (TypeRef × TypeRef)) +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 todo f g + | some f => sub A B seen f g | none => B.acceptsNull g -termination_by (todo.length, 1) +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 may be assumed at most once, and there are finitely many. -/ +reference pair is recorded at most once, and there are finitely many. -/ def decSubtype (a b : ClosedType) : Bool := - sub a.table b.table (allPairs a.table b.table) a.root b.root + 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 `todo` swaps with the tables. +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. -/ diff --git a/lean/Candid/SubtypeSpec.lean b/lean/Candid/SubtypeSpec.lean index ecd14e47..d0407c07 100644 --- a/lean/Candid/SubtypeSpec.lean +++ b/lean/Candid/SubtypeSpec.lean @@ -54,7 +54,7 @@ coinductive Subty : TypeTable → TypeTable → Slot → Slot → Prop where | 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 `todo` a measure. -/ + 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) @@ -131,8 +131,8 @@ 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 *missing* from `todo` as the coinductive hypothesis -- that -is what `todo` means, and stating it this way is what will confirm the accounting is +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. diff --git a/lean/Main.lean b/lean/Main.lean index b188f9e9..3d6684d8 100644 --- a/lean/Main.lean +++ b/lean/Main.lean @@ -233,8 +233,8 @@ def serviceChecks : List Check := 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 removes it from -`todo`, and meeting that pair again means the obligation is already assumed. -/ +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 := @@ -290,7 +290,7 @@ def recursiveChecks : List Check := 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 taken out of `todo`. -/ +third state finds its pair already recorded in `seen`. -/ def vecOmegaTable : TypeTable := { entries := #[ .vec (.ref 1), .vec (.ref 0) ] } @@ -303,7 +303,7 @@ def vecOmegaChecks : List Check := , expectSub vecOmegaEven vecOmegaOdd true "vec-omega <: its own unrolling" , expectSub vecOmegaOdd vecOmegaEven true "vec-omega's unrolling <: it" ] -/-! ## Contravariance: `todo` swaps with the tables +/-! ## 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 @@ -312,8 +312,8 @@ 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 takes `(1, 2)` out of -`todo`, so a procedure that read `todo` unswapped would answer the premise from the +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`. -/ diff --git a/lean/README.md b/lean/README.md index f230a030..3db08e1d 100644 --- a/lean/README.md +++ b/lean/README.md @@ -66,9 +66,11 @@ 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 `todo` — the pairs it has not yet assumed — descends by removing -one, and `todo.length` is the termination measure. No fuel, no `Option Bool`, and no -"unanswered" state in the public API. The first version of this model, with +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. @@ -154,15 +156,18 @@ 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 *missing* from `todo` as the coinductive hypothesis, - which is what `todo` means. There is no longer a budget premise to discharge: the + 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 seeded eagerly.** `decSubtype` starts from - all `|A| x |B|` reference pairs, and `todo` is threaded down a path rather than - shared between siblings. That is a faithful reading of the coinductive hypothesis - and it is what makes the termination measure need no side conditions, but sharing - the accounting across siblings is also sound for a greatest fixed point and is how - an implementation gets a polynomial bound with no eager allocation. +- **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 — From 639d16f5162fc92947fe4acdb0da6b0d4056114e Mon Sep 17 00:00:00 2001 From: Linwei Shang Date: Wed, 26 Aug 2026 16:51:43 -0400 Subject: [PATCH 7/7] lean: enforce two spec rules, fix two citations, wire `lake test` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit **Well-formedness.** The model accepted two kinds of type the spec forbids: oneway with a result: wellFormed = true -- spec/Candid.md:211 service with a prim method: wellFormed = true -- spec/Candid.md:1223 `Composite.annotsOk` covers the first. The second needs the table, since a method's type is a slot like any other, so it lives in `TypeTable.wellFormed` as `methodsDenoteFuncs` -- the only well-formedness rule here that looks through the table. Six checks pin both, including the cases that must stay well formed (`query` with a result, `oneway` without one, a method that is a function). One rule is left out on purpose, with the reason recorded: "The list of parameters must be shorter than 2^32 values" (`spec/Candid.md:209`) cannot be violated by anything that fits in memory. It is not idle, though -- `indexedFrom` labels positional arguments with `UInt32`, which wraps, so that bound is what keeps a function's argument labels distinct. **Citations.** `spec/Candid.md:1207` is a bare code fence; the `I` block it introduces starts at 1208. `spec/Candid.md:1221` is the note about multiple representations, not the method-type rule, which is 1223. All ten citations in `lean/` were checked against the spec; the rest were exact. **Vocabulary.** "Slice" was used seven times and defined nowhere, and REWRITE.md does not use the word at all. It now has a one-line definition where it first appears -- a label for what landed in a merge window, applied after the fact -- and the two forward-looking uses in the sources are gone, since the plan is the coverage checklist and the tiers in REWRITE.md §3. **`lake test`.** `testDriver = "oracle"`, so the model checking itself is reachable the ordinary way. CI keeps running the binary explicitly so the check names show up in the log. Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/lean.yml | 3 ++- crates/README.md | 2 +- lean/Candid/Subtype.lean | 4 +++- lean/Candid/SubtypeSpec.lean | 4 ++-- lean/Candid/Types.lean | 34 +++++++++++++++++++++++---- lean/Main.lean | 45 ++++++++++++++++++++++++++++++------ lean/README.md | 12 ++++++---- lean/lakefile.toml | 2 ++ 8 files changed, 86 insertions(+), 20 deletions(-) diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml index 157a33c2..56dd6c96 100644 --- a/.github/workflows/lean.yml +++ b/.github/workflows/lean.yml @@ -24,7 +24,8 @@ jobs: - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 # Installs the toolchain named in `lean/lean-toolchain` and caches the build. - # `lake test` is not configured yet; the reference executable is the test. + # `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 diff --git a/crates/README.md b/crates/README.md index 865dcf0c..0c58a849 100644 --- a/crates/README.md +++ b/crates/README.md @@ -83,7 +83,7 @@ name. 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:1207`) and what makes the subtype procedure in +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 diff --git a/lean/Candid/Subtype.lean b/lean/Candid/Subtype.lean index 73d06cf2..ae41ea7c 100644 --- a/lean/Candid/Subtype.lean +++ b/lean/Candid/Subtype.lean @@ -75,7 +75,9 @@ 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*, per the spec. -/ +/-- 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 ·) diff --git a/lean/Candid/SubtypeSpec.lean b/lean/Candid/SubtypeSpec.lean index d0407c07..8535ef33 100644 --- a/lean/Candid/SubtypeSpec.lean +++ b/lean/Candid/SubtypeSpec.lean @@ -96,7 +96,7 @@ 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 in slice 2. -/ +used gets caught here rather than when the first proof is attempted. -/ example (A B : TypeTable) : Subty A B .nat .int := Subty.natInt @@ -122,7 +122,7 @@ example (A B : TypeTable) (fs : List (FieldId × Slot)) : simp [fieldAt] at h /- -The obligation this file exists to create, and the first proof of the next slice: +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 diff --git a/lean/Candid/Types.lean b/lean/Candid/Types.lean index a675ef02..8531d0aa 100644 --- a/lean/Candid/Types.lean +++ b/lean/Candid/Types.lean @@ -14,7 +14,7 @@ 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:1207`): +(`spec/Candid.md:1208`): ``` I : -> i8* @@ -118,7 +118,17 @@ def noDups [BEq α] : List α → Bool 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. -/ +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 @@ -138,11 +148,27 @@ def Composite.labelsOk : Composite → Bool | .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.slots.all (Slot.wellFormed bound) + 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 (Composite.wellFormed t.size) + t.entries.all fun c => c.wellFormed t.size && t.methodsDenoteFuncs c /-- A type together with the table its references resolve in. diff --git a/lean/Main.lean b/lean/Main.lean index 3d6684d8..e56822f3 100644 --- a/lean/Main.lean +++ b/lean/Main.lean @@ -1,10 +1,10 @@ /- The reference executable. -Slice 1 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. +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 @@ -214,7 +214,7 @@ def funcChecks : List Check := 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:1221`), so it is an index into the table, not an inline function. -/ +(`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 @@ -229,6 +229,37 @@ def serviceChecks : List Check := , 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 @@ -354,8 +385,8 @@ def transitivityChecks : List Check := def allChecks : List Check := hashChecks ++ primChecks ++ optChecks ++ vecChecks ++ recordChecks ++ - variantChecks ++ funcChecks ++ serviceChecks ++ recursiveChecks ++ - vecOmegaChecks ++ contraChecks ++ transitivityChecks + 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) diff --git a/lean/README.md b/lean/README.md index 3db08e1d..60dbb745 100644 --- a/lean/README.md +++ b/lean/README.md @@ -1,7 +1,9 @@ # `lean/` — Lean 4 reference model and specification **Status: first slice.** Types, the field-id hash, and subtyping — as both a relation -and a decision procedure — with a self-checking executable. Nothing is published and +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. @@ -60,7 +62,7 @@ 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:1207`), and the spec draws the conclusion the model is built on: +(`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`." @@ -144,6 +146,8 @@ cover what actually breaks in production: 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 @@ -172,8 +176,8 @@ Named here so they are obligations rather than oversights. 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 in slice 1: bundling an undocumented doc toolchain into - the slice whose purpose was de-risking the build would have doubled the unknowns. +- **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/` diff --git a/lean/lakefile.toml b/lean/lakefile.toml index 4f9c7889..fef02f3b 100644 --- a/lean/lakefile.toml +++ b/lean/lakefile.toml @@ -1,6 +1,8 @@ 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.