Add a Lean model of the CCL type system and fuzz the solver against it by dpmills · Pull Request #79 · cambra-dev/cambra

dpmills · 2026-08-11T02:55:57Z

constrain_go implements a subtype relation that nothing in the repo states, and no test covers the solver's order-independence claims about KindMerge's transitive force propagation and one-sided var-var bound propagation. This PR adds formal/, a Lean 4 lake project that states the ground fragment of the type system declaratively and proves its metatheory, an oracle binary that answers subtype verdicts, and two #[cfg(test)] Rust fuzz harnesses that diff the solver against the model and against itself under permuted constraint order. A semantic divergence between constrain/coalesce and the stated relation becomes a test failure instead of a doc claim.

The diff is additions only. Outside formal/ and the two new test modules it is four lines of mod declarations in src/ccl/infer/solver/mod.rs.

Reading order

formal/design.md is the plan of record: the oracle stance (the model checks, it does not reproduce), milestones M0–M6, every adjudicated rule, and the findings the model has produced so far. Read it before the Lean. formal/README.md has the build commands.

Then the library:

Ty.lean, Sub.lean — the ground grammar with the uniquely-keyed invariant Ty.WF, and Sub, the declarative relation. Sub.lean's module doc lists its two departures from constrain_go: no trivial-equality short-circuit, no partition-collapse arm.
Equiv.lean, Props.lean, Decide.lean — decidability (sub_of_subCheck, subCheck_of_sub), Sub.refl as a theorem rather than a rule, and the #guard spec examples pinning each adjudicated rule.
Transitivity.lean — sub_trans / sub_trans_id: transitivity for the canonical (__pi{d}) fragment, over six independent identity-acting rename environments.
Term.lean, Safety.lean — the pure-core term calculus and the safety battery: progress (value, steps, or filter-blocked), preservation, refinement_soundness, case_binder_sound.
Merge.lean — the ground fragment of compact.rs's bound merging: eqv an equivalence, merge_comm, merge_idem, merge_congr, merge_assoc_cf, foldMerge_perm.

No file carries a sorry.

The harnesses

differential.rs generates biased ground type pairs with a seeded xorshift (deterministic, no new dev-dependency), serializes them to the wire schema Json.lean defines, and diffs constrain_subtype's verdict against the subverdict oracle case by case (differential_ground_subtype_vs_lean_model). It skips loudly when formal/.lake/build/bin/subverdict is absent, so a machine without a Lean toolchain stays green. transitivity_chain_fuzz needs no oracle: it builds chains the solver accepts and fails on any direct edge the solver then rejects. Knobs: CAMBRA_DIFF_SEED, CAMBRA_DIFF_N.

confluence.rs applies one constraint set in permuted orders against fresh variables and asserts the coalesced outcomes agree (bound_order_permutation_fuzz), plus two pinned cases — refinement_claims_are_arrival_order_independent and vintage_claims_render_alike_but_do_not_dedup. The outcome excludes which constraint trips the rejection of an unsatisfiable set, since that is order-relative under record-then-sweep; a set flipping between accepted and rejected across orders is a hard violation.

What to be suspicious of

./ci.sh is untouched, so nothing gates the Lean half. lake build would put a Lean toolchain on everyone's gate; design.md records that as a pending decision rather than an oversight.
The pair generator excludes duplicate record/variant keys — the one type shape where the model and constrain_go are known to disagree, outside Ty.WF.
merge_not_assoc is an open finding: the mixed-kind merge arm makes arrival order decide accept-versus-reject, and whether a real program can put those three bounds on one variable is a Rust-side question the confluence generator's vocabulary does not reach.

dpmills · 2026-08-11T02:56:23Z

This change is part of the following stack:

Freshening asks a different question than type_level, so it needs its own #71
- SharedHole: let lowering state that two type positions are the same #72
  - Traits: state what an operator requires of its operands, not that they are the same #73
    - Mutable-variable typing: an honest seed, a fixed history read-through, and a polarity-directed base #52
      - Annotations stop standing in for binder structure, and stop outliving inference #60
        
        Four defects in how Mut is typed: message polarity, an unclosable refinement, and op= as a rebind #63
        
        A mutable variable read is an explicit operation, not a subtyping rule #64
        
        Exact and bounded binder annotations: x: T fixes the type, x <: T bounds it #62
        
        constrain_go asserts the uniquely-keyed invariant it rests on #74
        
        Update the value-Case fan-out's prose to the DisjointJoin it builds #75
        Canonicalize each arrow's Pi binder as the solver flattens types #76
        Hold a refined type's refinements in one unordered set instead of nested layers #77
        Derive a Cast's refinements from its term instead of overwriting the target #78
        Add a Lean model of the CCL type system and fuzz the solver against it #79 ◀

_{Change managed by git-spice.}

A coalesced type's refinement layers stacked in constraint *arrival* order: two refined upper bounds meeting at one variable produced `{{T | q} | p}` or `{{T | p} | q}` depending on which arrived first. Subtyping never cared — the deficit machinery compares layers as a set — but `Type`'s equality did, and structural equality is load-bearing wherever a type is an *identity*: the trivial-equality short-circuit, cache keys, and the recorded-vs-recomputed walls. One `Vec` was serving three incompatible readings: a set to subtyping, a stack to planning, an identity to `SpecKey` and the walls. The repair is the representation rather than a canonical order. `Type::Refinement` now carries a `RefinementSet` — unordered, deduplicated, with set-semantic `Eq`/`Hash` — and `Type::refined` flattens, so `{{T | p} | q}` is unrepresentable and "which layer is outermost" cannot be asked. Sorting the `Vec` canonically was tried and rejected twice: it pins the ambiguity instead of deleting it, and it denies planning the freedom to apply filters in whatever order it likes. Two things the change forces into the open, both previously implicit. **Materializing claims is a pipeline, and a pipeline is ordered.** Planning emits one `restrict` per claim, and stage `k` reads elements already narrowed by stages `1..k-1`. The set is unordered as a fact; planning *chooses* an application order. Which order is free; choosing differently in two places is not, so `ccl::application_order` is the single place that choice is made — keyed on the claims' content, never on the set's physical order. **Partition collapse was unsound under flattening.** `partition_domain` peeled one gate layer per leg; peeling a whole claim set drops a genuine domain refinement, normalizing `⧺ᵢ({{E | p} | π̂ᵢ})` to `E` and accepting a demand for all of `E`. Gates are per-leg by construction, so a claim *every* leg carries is domain: the common claims are the intersection. Consumers that read a chain positionally now ask what a claim *says* — `groupby` finds the claim shaped like its key equation, `join` tries each claim as the join condition. `CAMBRA_REFINEMENT_ORDER=reverse` (debug builds) flips the set's physical order globally, because two classes survive a compile-clean rewrite and only running the suite both ways exercises them.

…etermined `coalesce_node` overwrote a `Cast`'s `target` wholesale with the occurrence's coalesced view (`expr.ty`). Which claims an occurrence's variable accumulates depends on the route bounds took through the graph, so two copies of one embedded cast — a comprehension source cloned into a filter predicate has its own variable per copy — could coalesce carrying different claim sets: one bare, one decorated with a sibling layer's filter. Refinement equality is deliberately cast-target-aware, so the copies refused to dedup, and which copy a position ended up holding depended on bound arrival order. That was the mechanism behind the open vintage-dedup finding, pinned down by structurally diffing the surviving twins under `CAMBRA_REFINEMENT_ORDER=reverse`. The overwrite becomes `canonical_cast_ty`: the coalesced view contributes its *shape and bases*; the claims are determined by the *term*. A cast is an assertion — `cast(value, {D | p} ⇒ V)` claims exactly `p` on top of whatever its value already established — so its `target` keeps its **born claims** (fixed when lowering wrote the cast; inference resolves bases, never rewrites claims), and the node's *type* is the value's own domain claims joined with them (the walk is bottom-up, so the value's type is already canonical by induction). Target and type must stay distinct: the post-inference check recomputes a cast's type as value-claims ∪ target-claims, and a target that also carried the value's claims would double-book them — any divergence between the value's copy and the target's copy of one claim then surfaces as a duplicated claim in the recomputation. On deterministic routes the term-determined claims equal what the view accumulated, so the forward suite is behaviour-identical (fully green). Under the reverse-order stress the change repairs all but one residue: `comprehensions::case_6` still trips the post-planning wall, with the collision now between the *compiled* and *uncompiled* copies of one claim inside the planned tree — recorded in `formal/design.md` as the next diff target.

…onical split The reverse-order stress (`CAMBRA_REFINEMENT_ORDER=reverse`) had one residue left: `comprehensions::case_6` tripped the post-planning wall with render-alike claims that refused to dedup. Structural diffing (a tree-wide sweep grouping every claim by render and comparing eq-classes) localized the manufacture to `insert_iterate_markers`' per-site predicate compile, and from there to a chain of three defects, each an instance of the same rule the coalesce-time canonicalization already established — **a rebuild pass resolves a cast's bases; it never decides its claims**: - `simplify`'s collapse-a-chain-to-one-element rewrite stamped the chain's interface type wholesale onto a surviving `Cast`. The interface type is derived from neighbour types, which are route-dependent where inference left route-dependent types in eq-blind slots (a lambda param annotation inside a still-pointful predicate), so the stamp desynced the cast's recorded type from its term-determined claims. The rewrite now restores the canonical type (`canonical_cast_ty`) at construction. - `sync_cast_targets` (at the tails of `lambda_elim::run`, `planning::run`, and inlining) then copied that route-dependent `expr.ty` into the cast's `target` — promoting a benign, eq-invisible divergence into the one slot `eq_refinement_predicate` deliberately compares, so two copies of one claim stopped dedup'ing. The pass is retired; `ccl_utils::canonicalize_cast_types` replaces it (`target` = born claims on the rebuilt view's bases, `expr.ty` = value-claims ∪ born, and a chain headed by a cast follows its head's domain when the two differ only in claims on one base — the post-pass check's reconcile is exact on domain claims, so the recorded chain type must track its head). `canonical_cast_ty` moves to `ccl_utils` and is shared with coalesce. - `compile_refinement_predicates` compiled a cast target's claims against the target's bare base. A target holds only the cast's *born* claims, so its sole claim compiled with a bare `__elem` stamp — failing the checker's argument edge once the predicate function's domain carries the value's claims. Target claims are assertions on the cast's **value**: they now compile against the value's domain (matching `emit_cast`, which types target predicates with `__elem` bound at the value's domain). With these, the full suite is green under the reverse-order stress for the first time. Refinement equality still distinguishes *genuinely* different cast targets — that behaviour is correct and deliberate; the pipeline just no longer manufactures divergent copies of one claim.

… against `constrain` `formal/` is a Lean 4 lake project (toolchain pinned, zero external deps) modeling the **ground fragment** of the subtype relation `constrain_go` implements — stated declaratively for the first time (`Sub`, one constructor per arm with rule-level provenance comments), alongside an executable checker (`subCheck`, termination proved), a hand-written JSON wire codec, and executable spec `#guard`s (one per adjudicated rule: `UIntRange` equality-only, refinement base covariance with predicate-set width, the `data ⊑ compute` kind lattice, data-data domain invariance, product/sum width, the Pi-binder correspondence). First metatheory: **reflexivity is a theorem, not a rule** (`Sub.refl`) — the model omits `constrain_go`'s trivial-equality short-circuit and proves it derivable, which goes through exactly under the unique-key invariant `Ty.WF` names (the short-circuit and the find-first record/variant arms genuinely disagree on duplicate-keyed products). The gated-partition bridge arm is modeled faithfully (`fnBridge` + deep `stripRefinements` + negated guards preserving the Rust `match`'s commit-to-first-arm determinism); `Sub.refl` survives via `isIndexPartitionOf_irrefl`, a `sizeOf` argument that no type is a partition of itself. The differential oracle: `lake build` also produces `subverdict` (JSONL `{"lhs","rhs"}` pairs in, verdicts out), and `src/ccl/infer/solver/differential.rs` generates biased ground pairs with a seeded dependency-free PRNG (identical, edited, deeply-correlated, and bridge-aimed modes), streams them through the oracle, and diffs against `constrain_subtype` case by case. **~800k cases across nine seeds: zero verdict mismatches.** The test skips loudly when the oracle binary is absent, so machines and CI without a Lean toolchain stay green; `CAMBRA_DIFF_SEED` / `CAMBRA_DIFF_N` control runs. Two findings from the modeling, pinned as unit tests: - `dup_key_record_reflexivity_diverges_from_model` — on a duplicate-keyed record, `t <: t` holds only via the trivial-equality short-circuit; the record arm it shadows would demand cross-subtyping between the duplicates. - `bridge_arm_skips_pi_correspondence` — the bridge arm's codomain edge recurses under the *unchanged* lhs morphism where the general `Fun` arm extends it with the binder correspondence, so α-equivalent dependent codomains match through the general arm but **not** through the bridge: the verdict on the same value flips purely on whether the supplier's domain is partition-shaped. Flagged for the `strip_refinements`/bridge cleanup. Plan of record, adjudicated decisions, and milestone status live in `formal/design.md`; build/run instructions in `formal/README.md`. `formal/` is deliberately not wired into `./ci.sh` yet (it would add a Lean toolchain dependency to the gate) — tracked in the design doc as a pending decision.

…ired, machine-checked Three layers of metatheory on top of the M0/M1 base, tracking the solver change in the previous commit: **Decidability** (`CclFormal/Ty.lean`, `CclFormal/Equiv.lean`): hand-written structural equality bridged to propositional equality (`Ty.beq_iff`, yielding lawful `BEq` and `DecidableEq` — the deriving handlers cannot touch the nested inductive), then checker soundness (`sub_of_subCheck`) and completeness (`subCheck_of_sub`), giving `subCheck_iff_sub` and the instance `Decidable (Sub ρl ρr lhs rhs)`. Every `#guard` spec example is thereby a fact about the relation, not just the checker. **Transitivity, refuted then repaired** (`CclFormal/Trans.lean`): modeling the bridge arm faithfully produced a machine-checked counterexample to transitivity (`sub_not_trans`, in this file's history) — the finding that motivated the normalize-then-recurse rewrite. Under the rewrite the model's `fnBridge` rule becomes `fnNorm` (mirroring `partition_domain` / `normalized_partition_fun`), and this file now machine-checks the formerly-broken triangle composing: `transCex.sub_a_b`, `sub_b_c`, and `sub_a_c`. Transitivity in general is a live conjecture (chain fuzz: zero violations at 200k chains); the proof's obligations are rename composition through Pi correspondences and refinement-set containment. The model sync deletes `stripRefinements`, `IsIndexPartitionOf`, and the `subBridge` machinery outright, and `Sub.refl` no longer needs a partition-irreflexivity size argument — a partition is reflexively below itself through its normal form. `formal/design.md` records both findings as repaired, the repair's design (kind-agnostic, bare-leg-tolerant, `Infer`-excluded normalization), and the updated fuzz status.

… in arrival order The solver leans on constraint arrival order not mattering — `KindMerge`'s "forces propagate transitively along links as they arrive, so ordering does not matter", and the one-sided var-var bound propagation recorded as an open question in `design/type-inference.md` — but nothing tested it as a property. `src/ccl/infer/solver/confluence.rs` does: the same constraint *set* (ground bounds, var-var edges, kind-variable functions) is applied in permuted orders against fresh variables, every variable is coalesced, and the outcomes must agree — acceptance through coalesce plus the canonicalized per-variable types. *Which* constraint trips the rejection of an unsatisfiable set is intrinsically order-relative under record-then-sweep and deliberately not part of the outcome; kind variables carry mutable force/link state, so specs are regenerated per permutation from a fixed sub-seed rather than cloned. **Finding, pinned as `refinement_layer_order_depends_on_arrival_order`:** a coalesced type's refinement layers stack in constraint arrival order — `{{𝑇 | 𝑞} | 𝑝}` vs `{{𝑇 | 𝑝} | 𝑞}` depending on which bound arrived first (≈1 in 10k generated sets). Subtyping is indifferent (the deficit machinery compares layers as a set), but `Type`'s derived `PartialEq` is order-sensitive, and structural equality is load-bearing where types are identities: `SpecKey`, the trivial-equality short-circuit, cache keys — two uses that should share a specialization can split on arrival order. The obvious fix (canonically sorting `CompactType::refinements`) was tried and reverted, which sharpened the finding twice over. It fails exactly one test, and the root cause is not ordering mechanics but **predicate vintages**: a dependent-application discharge embeds the argument *term* into refinement predicates, so one filter exists as `𝑝(xs)` / `𝑝(cast(xs))` / `𝑝(cast(cast(xs)))` across comprehension layers; `eq_refinement_predicate` deliberately distinguishes vintages (a cast target carries a semantic filter), and layer order *selects which vintage* each type carries — the recorded-vs-recomputed wall demands the two derivation paths select consistently, which arrival order happens to deliver. Two vintages of one predicate are **not** the same predicate — they happen to be equivalent in the cases at hand — so the repair is some form of canonical discharge (normalizing what discharge embeds), whose exact shape needs care; vintage-blind equality is non-transitive as stated, and full cast-transparency conflates semantically distinct embedded collections (see `refinement_eq_distinguishes_cast_target_predicates`). With the known class quarantined in the comparator (canonical layer sorting before comparison — any new class still fails), the fuzz is clean at 100k constraint sets × 8 permutations across seeds: acceptance, coalesced structure, and kind-var resolution are confluent within the generated vocabulary, giving `KindMerge`'s comment and the var-var open question their first property-test backing. Analysis recorded in `formal/design.md`.

…ndent case's obstruction stated Transitivity was refuted while the gated-partition bridge arm was a target-relative comparison, and became a live conjecture once the collapse was re-homed as a normalization. This proves it — `CclFormal/Transitivity.lean :: sub_trans` — for the **non-dependent fragment** (`NoPi`: no function type carries a Pi binder), under a single ambient rename environment. No `sorry`: `#print axioms` reports only `propext`, `Classical.choice`, `Quot.sound`. The counterexample triangle that refuted transitivity under the old arm is re-derived as an instance of the general theorem rather than by hand. The proof is a fuel-bounded strong induction on the summed size — fuel rather than well-founded recursion so the induction hypothesis is an ordinary function that helper lemmas can take — split into two routes: - **Peel route** (some side carries a refinement layer): peel all three types, recurse on the bases, re-wrap. Refinement-set containment composes by a membership chase (`deficit_trans`), and the measure decreases because at least one peel is strict. - **Head-constructor route**: one case per rule. The three ways to conclude a function edge are factored into `sub_trans_fn`, which takes the induction hypothesis explicitly, so `fnNorm`/`fnCompute`/`fnData` are handled once rather than per caller. Kind-lattice bookkeeping falls out: `data`-to-`data` conclusions force the middle kind to `data` (and both premises to `fnData`, supplying the second domain direction invariance needs), and the mixed `fnCompute`/`fnData` chain is vacuous because its own kind edge would be `compute <: data`. Two lemmas carry most of the weight: `sub_peel_inv` (universal peel inversion — *every* rule leaves the peeled bases related and the peeled refinement sets contained, trivially so for the head-constructor rules) and `sub_normFun` (every function edge relates the two sides' normal forms, since the general rules only fire when both sides are already normal). **The dependent case is stated, not proved** (`TransitivityConjecture`), with its obstruction pinned down. Chaining two function edges yields codomain premises under `codRen 𝑛₀ 𝑛ₘ ρl`/`ρm` and `codRen 𝑛ₘ 𝑛₁ ρm`/`ρr` while the conclusion needs `codRen 𝑛₀ 𝑛₁ ρl`/`ρr`: the two premises disagree about the **middle view** of the middle type's codomain, and compose only through the rename `σ = [𝑛ₘ ↦ 𝑛₁]` relating those views — `Sub ρl ρm 𝑥 𝑦 → Sub (σ ∘ ρm) ρr 𝑦 𝑧 → Sub (σ ∘ ρl) ρr 𝑥 𝑧`. That is exactly the reconciliation `constrain.rs :: bridge_holder_gap` performs when two bounds recorded under different morphisms meet at one variable: the implementation already invented this step, and the metatheory needs the same one, plus the freshness discipline the Rust gets for free from globally-uniquified `Name`s and never writes down. Also in this change: `Ty.beq`-free `not_and_or'` and `one_le_sizeOf` helpers (this development has no Mathlib), and the analysis recorded in `formal/design.md`.

… merge) The transitivity proof isolated Pi binders as the sole remaining obstruction to pure transitivity (the σ-gap), which raised the question whether α-variance is already biting the implementation. It is — two findings, both pinned in `confluence.rs`: - **`SpecKey` splits on α-variant dependent types** (`spec_key_splits_on_alpha_variant_dependent_types`). The key deliberately excludes the Pi binder name, but the name survives through the predicates that reference it, which the key compares structurally — so `(𝑥: 𝐷) ⤇ {Int | __elem == 𝑥}` at one call site and its `𝑦`-twin at another key apart, and uses that should share a specialization get one clone each (over-splitting: wasted clones, not a miscompile). The key's stated rationale for excluding the name — per-site fresh solver binders "would split every use into its own key" — is re-imported through exactly this leak. - **α-variant bound merge is order-dependent and dangles** (`alpha_variant_bound_merge_is_order_dependent`). Two α-variant upper bounds meeting at one variable merge into a fun shape keeping the *first arrival's* binder (`compact.rs`: `a.name.or_else(|| b.name)`) while the refinement sets union, coalescing to `(𝑥: 𝐷) ⤇ {{Int | __elem == 𝑥} | __elem == 𝑦}` — arrival-order-dependent *and* carrying a predicate that references a binder the type no longer binds. The two predicates are α-copies of one constraint that structural dedup cannot collapse. Also surveyed: `without_pi_names`' three call sites all patch the `Some`-vs-`None` erasure on rebuilt arrows for same-derivation copies, per its own doc — cross-derivation α-variance was never its job, and is exactly the unguarded case above. `formal/design.md` files this as the third member of the non-canonical-identity family (duplicate record keys, refinement-layer order, Pi binders), with the repair direction the codebase already applied to refinements themselves: canonical Pi binder names, which would collapse both defects, retire `without_pi_names` and the rename half of `bridge_holder_gap`, and make the transitivity proof's `NoPi` restriction vacuous. One correction recorded: `SpecKey` is *not* exposed to refinement-layer order (it compares refinement sets as sets); its exposure is specifically α-variance via predicates.

…solved With canonical Pi binders in the solver's flattening layer, the transitivity proof's `NoPi` restriction is retired. `CclFormal/Transitivity.lean` now proves `sub_trans` for the **canonical fragment** — `Canon d`, the depth-indexed mirror of what `compact_go` emits (every arrow's binder absent or `__pi{d}`, codomains one deeper) — with `sub_trans_id` as the pure statement at the identity environment, the form the ground oracle exercises. The former `NoPi` fragment is the all-binders-`none` special case. No `sorry`; `#print axioms` reports only `propext`, `Classical.choice`, `Quot.sound`; the counterexample triangle that once refuted transitivity is re-derived as an instance. The generalization that makes it work: the induction hypothesis carries **six independent identity-acting environments** (each premise pair and the conclusion pair are free). The σ-gap was the observation that chained codomain premises view the middle type under different renames; for canonical types every correspondence an edge mints is *diagonal* (`__piK ↦ __piK`), and diagonal extensions preserve `IsId` (`codRen_canon_isId`) — while under identity-acting environments the refinement deficit reduces to plain set containment (`deficit_isId_nil_iff`), making the environments interchangeable everywhere they appear. So no reconciliation morphism is ever needed: where the σ-generalized statement would compose views, the canonical proof simply picks whichever environment the conclusion wants. The σ-indexed statement remains the honest formulation for *non-canonical* (pre-coalesce, source-named) types; it retires entirely with the minting-level stratum (`emit_lambda` producing canonical binders), recorded in `formal/design.md`.

…bservable Tracks the Rust representation change into `formal/`, restoring the differential oracle to full coverage and re-establishing every prior result over the new grammar. `Ty.refined` now holds a `List Pred`, mirroring `Type::Refinement(base, RefinementSet)`. `Ty.WF` names the same two invariants `Type::refined` establishes — the claims are non-empty, and the base is not itself refined, so layers never nest. `Canon` carries the non-emptiness too, and that is not bookkeeping: a degenerate `refined b []` would peel to nothing while remaining a distinct term, which makes `peel_nil_self` false outright. The solver's flattening layer never emits one, so excluding it is the model naming another invariant the Rust holds by construction. **Claim order is unobservable — a theorem, not a reading of the rules.** The claims are *represented* as a list and `Ty.beq` compares them positionally, which is what keeps `beq` propositional equality and therefore keeps `DecidableEq`, the bridge every proof rests on. That is only faithful to an unordered `RefinementSet` if the relation cannot see the list structure, so the model now proves it: `sub_claims_left` and `sub_claims_right` (widening the supplied claims, narrowing the demanded ones), with `sub_claims_perm` / `sub_claims_perm_right` as corollaries. They are stated as **containment** rather than permutation because containment is what `deficit` actually uses — it asks whether each demanded claim has *some* supplier, so a supplier list may be reordered, duplicated, or widened freely. Reorder- and dedup-invariance both fall out, which is exactly the latitude the Rust takes. `partitionDomain` follows `constrain.rs` to the intersection rule, with the per-leg part split out as `legNormal` so its size bound is stated once (`legNormal_sizeOf_le`, needing only that filtering never grows a list). The Rust's "all legs claim the same" test moves from slice equality to set equality in the same change — it was asking whether the legs listed their claims in the same order, not whether they agreed on them. Everything prior is re-established sorry-free over the new grammar: `Sub.refl`, `subCheck` soundness and completeness (hence `Decidable (Sub …)`), and `sub_trans` / `sub_trans_id` for the canonical fragment. The wire schema's `refined` node carries a `claims` array, so the emitter no longer refuses a multi-claim refinement and the harness no longer skips. The generator's nested refinements flatten into multi-claim positions, so the new shape is exercised throughout: **140k cases across five seeds, zero verdict mismatches**, and green again under `CAMBRA_REFINEMENT_ORDER=reverse` — the empirical counterpart of `sub_claims_perm`.

`gen_bridge_pair` perturbs a partition leg's index to probe the contiguity guard, but it applied the shift to *any* leg — and shifting an interior leg lands it on its successor's index, producing a duplicate-keyed `Variant`. Duplicate keys are the one class the harness documents itself as excluding, because it is where `constrain_go` and the model deliberately disagree: the trivial-equality short-circuit accepts `t <: t` while the find-first arm it shadows — and therefore the model, which has no short-circuit — rejects it. Generating that class manufactures mismatches instead of finding them, and it is outside `Ty.WF`, under which `Sub.refl` is proved. Confining the shift to the last leg keeps the near-miss doing its job — an index of `n` where `n-1` is expected still breaks contiguity — while every key stays unique.

`formal/design.md` claimed the α-machinery in `constrain` — and the rename environments the model mirrors it with — could be retired by a "minting-level stratum": having `emit_lambda` produce canonical binders directly. That is wrong, and leaving it in the plan of record would send someone down it. The canonical index counts enclosing **codomain** arrows, including unnamed ones, so it is a property of a binder's *position in a finished type* rather than of the binder. Emit types an inner lambda before knowing what will wrap it, and any type placed in a codomain shifts every Pi binder inside it. The shape is ordinary source, not a corner: `\s -> groupby([1,2,3,4], \x -> x // 2)` infers with the group-by's binder at `__pi1`, where standing alone it is `__pi0`. A footnote in the M0 status records that, the live consequence (`Type` equality is not α-invariant before coalesce, so identity comparisons across that boundary must normalize explicitly — the same family as the retired refinement-layer-order bug), and the one change that *would* enable minting: indexing binders from the inside out, so an index is fixed within a binder's own subtree and stable under wrapping. Its open question is that such indices are not unique within a type, and `Subst` keys on names globally. Noted as a possibility, explicitly not planned.

…y, idempotence `formal/CclFormal/Merge.lean` mirrors the ground fragment of `compact.rs`'s bound-merging: `CTy` (atoms, the optional record/variant maps with the load-bearing `none` vs `some []` distinction, the function slot, the claim set, an error flag), the polar `merge` (`CompactType::merge` / `CompactFun::merge` / `merge_refinements` / `merge_keyed`), and `eqv` — the model's mirror of `CompactType`'s `PartialEq`, set-semantic at every layer. The dedup gate in the positive `data ⊔ data` arm is `eqv` itself, exactly as `union_domains` dedups with `PartialEq` — which is what makes the algebra quotient-compatible by construction. Adjudications (all recorded in the module docs): inference variables, history slots, the Pi binder (canonicalized to agreement by `canonical_pi_binder` before any merge sees it), and `reduce_error`'s payload are dropped; domain alternatives beyond one are modeled as `none` ("many") because every path that could read a second alternative ends in a coalesce error — if Σ ever materializes multi-domain joins, that adjudication must be revisited. There is deliberately **no identity element**: `compact_go` folds bounds from the first bound, never from `default()`, because an empty claim set is absorbing under the positive intersect. Proved so far, all sorry-free: - `eqv` is an equivalence relation (`eqv_refl`, `eqv_symm`, `eqv_trans`), with the map slots read pointwise through `lookup` (`subKeys_iff`, `mapClause_iff`) so shadowed duplicate bindings are unobservable — mirroring `BTreeMap`. - `merge_comm` (with `mergeFun_comm`): the merge is commutative at both polarities, unconditionally. - `merge_idem`: merging a bound with itself is the bound — under `wf`, the input-bound invariant (no `conflict` kinds, every function slot carries exactly one domain), which is exactly what `compact_go` produces from a `Type`. Idempotence genuinely fails on non-`wf` states: the conflict arm canonicalizes the diagnostic payload away. Next (same milestone): congruence, associativity on the kind-uniform fragment, the mixed-kind association counterexample (`(D{d₁} ⊔ D{d₂}) ⊔ C{c}` conflicts while `(D{d₁} ⊔ C{c}) ⊔ D{d₂}` is accepted — arrival order deciding accept-vs-reject), and the fold theorems.

…ixed-kind counterexample, fold invariance Completes the join/merge property battery in `CclFormal/Merge.lean`, all sorry-free: - **Congruence**: `merge` respects `eqv` (`merge_congr_left`/`_right`/`merge_congr`). This holds *because* the one gate inside the merge — the positive `Data ⊔ Data` domain dedup — is `eqv` itself, mirroring `union_domains`' use of `PartialEq`; a gate keyed on anything finer would break it. - **Associativity on the compute-free fragment** (`merge_assoc_cf`): with every function bound `Data`, the merge is associative at both polarities. The gate algebra (`if eqv x y …` chains) closes by `eqv`'s equivalence lemmas; the negative direction's missing-domain conflicts absorb identically under either association. - **The counterexample** (`merge_not_assoc`, with the readable exhibits `merge_mixed_left_conflicts` / `merge_mixed_right_accepts`): two `Data` bounds over distinct domains plus one `Compute` bound merge to `Conflict` in one association and to an accepted `Compute` meet in another. `compact_go` folds bounds in arrival order, so if this bound-set is reachable, arrival order decides accept-vs-reject. Recorded in `formal/design.md` as an open finding needing Rust-side validation (the confluence fuzz's generator has not covered mixed function kinds over distinct domains at one variable). - **Fold invariance** (`foldMerge_perm`, `foldMerge_dup`, via `computeFree_merge_pos` preservation and `foldMerge_congr`): on compute-free bounds, the positive fold `compact_go` performs is invariant under permutation and duplication of the bound list — the proved form of the confluence fuzz's sampled claim, and the "uniqueness" half of the merge-algebra question: the coalesced outcome is a function of the bound *set*, not the arrival sequence. `formal/design.md` gains the "M4b — the merge algebra" section: the adjudication list, the theorem battery, and the mixed-kind finding with its follow-up (extend the fuzz vocabulary; determine whether `constrain_go`'s kind links already exclude the state).

`CclFormal/Term.lean` lands the pure-core term language and its semantics: `Tm` (literals, variables, λ, application, `let`, tuples, projection, variants, `case`, `cast`), values, capture-free de Bruijn substitution, partial predicate evaluation (`Pred.eval`, interpreting the wire emitter's `BinOpKind` vocabulary), the call-by-value small-step `Step`, the filter-blocked judgment `Blocked`, and the declarative typing `HasTy Γ e T` with subsumption through the M0 `Sub` relation. Values neither step nor block (`IsVal.not_step`, `IsVal.not_blocked`). Adjudications on contact, recorded in `formal/design.md` ("M2 status and adjudicated decisions"): - **Terms are de Bruijn; types keep their named Pi binders.** Subtyping never moves a binder, so names-with-renames mirrored the Rust there; reduction duplicates and re-scopes binders, where names buy only α-conversion obligations — and the Rust's term binders are uniquified, hence α-irrelevant. The M3 bridge maps names to indices mechanically. - **Non-dependent fragment first** (`Pred.elemOnly`): every refinement predicate is over the reserved `__elem`, so types are closed under term substitution — the same fragment the transitivity proof covers. - **`cast` checks its claims at runtime; progress is stated modulo filtering.** A cast is CCL's refinement introduction and its runtime face (`Restrict`) drops elements; the scalar small-step mirrors that by passing a value through exactly when every claim holds and marking the term `Blocked` otherwise. Refinement soundness will hold because the cast is the only door into a refined type. Next: progress + preservation, then the two corollaries — refinement soundness, and case-binder preservation (the calibration test targeting the known `case _:` payload-binder defect).

…-aware as a bug hunt The transitivity proof covers `NoPi`; extending through Pi binders splits into two pushes with different purposes, now planned as milestone M3b. The canonical fragment (`__pi{n}` binders, identity renames — the discipline the Rust relies on from compaction onward) is the near-term step: the `NoPi` proof plus a `CanonPi` invariant through peel/normalization. The α-aware statement (rename composition through the middle type, claim containment modulo rename, environment injectivity invariants) is the milestone's main body, deliberately framed as a bug hunt — the `NoPi` attempt found the bridge-arm defect, and the recorded α-smells live exactly where this proof treads. Sequenced after M3 so rule gaps get an executable reproduction path; the M2 safety extension to dependent types (type-level substitution / the §6.2 discharge) is tracked under M2 instead.

…— plus a partition-collapse finding `formal/CclFormal/Safety.lean` (new, ~1250 lines, no sorries) proves the M2 battery over `Term.lean`'s judgment: weakening and the substitution lemma (the de Bruijn payoff — no value restriction, no fragment hypothesis, types closed under term substitution), canonical forms modulo refinement peeling, **progress** (a well-typed closed term is a value, steps, or is filter-blocked at a cast), **preservation**, multi-step preservation, **refinement soundness** (`⊢ e : {T | claims}` and `e ⇓ v` imply every claim evaluates true on `v`), and `case_binder_sound` (the tag-arm case-binder statement — a theorem, as it should be; the `case _:` calibration needs the wildcard-arm extension, recorded). Two structural choices keep the proofs out of transitivity's territory: - **`Sub` inversions are case analyses, not inductions**: every constructor pins both sides' head constructors and the `refined` arm recurses on fully-peeled bases, so `Sub.to_peel` plus one non-recursive `cases` per head is the whole inversion story. - **Typing inversions absorb subsumption chains by typing transport** (`TyImp X Y := ∀ Δ a, HasTy Δ a X → HasTy Δ a Y`), not `Sub` composition — reflexive without `Sub.refl`'s `WF` side condition, composable link-by-link, each link re-entering `HasTy.sub` after `Sub.rename_invariant` brings its morphisms back to identity (where the non-dependent fragment earns its keep). Sketching preservation surfaced two counterexamples to the naive statement, which force two judgment-level changes in `Term.lean`: - **`Ty.TermFrag`, the fragment enforced in the judgment**: all refinement predicates `elemOnly`, and no `fn` domain partition-shaped — premised on the rules that choose types freely (`lam`'s domain, `variant`'s tags, `sub`'s target, `caseE`'s result, the last free only in the degenerate empty-tags elimination). Hypothesizing the fragment at the theorem boundary cannot confine a derivation's internal types; `hasTy_frag` states the invariant. - **`refineV`, checked values inhabit the refinement**: `cast p v` steps to `v` and `Sub` forbids refinement conjuring, so without a value-level introduction preservation is false at `castV` for every cast. The rule types a value at `{T | claims}` when the claims evaluate true on it — the term-model face of "a refinement is a fact about a value". **Finding (open, needs Rust-side validation)**: `constrain_go`'s partition-normalize arm deliberately fires at any kind, and at compute kind it breaks preservation under the tagged-value reading of `Variant` — `λ x : P → …` typed at `P ⇒ c` collapses to `Int ⇒ c`, a bare `5` flows in where the body expects a variant, and `lit 5` has no typing at `P`. Rust-side soundness rests on an implicit invariant: index-contiguous same-base variants are fan-out descriptors, never value-variant types — `Variant` is two concepts told apart by an unwritten tag convention. Follow-up mirrors the mixed-kind merge finding's: determine reachability, then either fix or assert + document. Details in `formal/design.md`'s M2 status.

Splitting `CollectionUnion` into `Copair` and `DisjointJoin` deleted `is_index_partition_of` and the subtyping arm that related a `Variant` of refined legs to the plain domain they share. The model still carried that arm, re-homed as a normalization (`Sub.fnNorm`, `partitionDomain`, `legNormal`, `normFun`), so the oracle and `constrain` disagreed on 632 of 20000 generated pairs at seed 7 — every one a partition-shaped supplier the model accepts and `constrain` rejects. `Sub` now relates a `Variant` domain only to a `Variant` domain. `Sub.fnNorm` and the normalization machinery go; `fnCompute` and `fnData` lose the guards that kept them disjoint from it; `subCheck` loses its normalization branch and the size-decrease lemmas that branch needed; `sub_trans_fn` loses two of its three routes. `Trans.lean` held nothing but the counterexample triangle and goes with them, its composing-chain content restated as `Decide.lean` guards. Two findings close by construction rather than by argument: - Ground subtyping was not transitive, because the arm connected a partition only to literally-same-domain demands. With no arm there is no non-composing edge. - Partition collapse fired at compute kind, where the tagged-value reading of `Variant` makes it a preservation violation at beta. `Ty.TermFrag` and `HasTy.lam` drop the premise that excluded partition-shaped `fn` domains, so preservation now holds on the wider fragment. The harness loses `gen_bridge_pair` and the two partition-shaped partners in `partner`, which aimed at a rule that no longer exists. After the removal: 90k pairs across three seeds with zero verdict mismatches, and 90k chains with zero transitivity violations.

The footnote proposed indexing Pi binders from the inside out so an index survives wrapping, and claimed that would let emit mint canonical binders and collapse `extended_rename` to the identity. A probe over the suite refutes it: a dependent refinement rides a bound edge, and the variable holding it need not sit under the binder its predicate references — every group-by produces that shape — so no index exists to write under either direction of counting. Wrapping was never the obstruction. The decision and the four alternatives measured against it now live in `type-inference.md`, next to the code they constrain; the footnote cites that section and keeps only what bears on this model: `Ren` stays, and `Type` equality is not α-invariant before coalesce.

dpmills · 2026-08-18T22:00:13Z

Superseded: the formal model was rebuilt directly on dmills/scoped-infer-vars over the index coordinate — the Ren rename machinery this edition carried is deleted there, transitivity is proved with no fragment restriction, and the differential oracle re-ran green (150k pairs) after catching a real capture in the solver's Fun/Fun opening. This branch keeps the model's development history; the confluence harness rides dmills/refinement-set's lineage where its assertions hold.

dpmills · 2026-08-18T22:49:11Z

Follow-up: the rebuilt model now lands as #109, at the top of the restructured stack (#108 → #77 → #78 → #109), where every finding its design doc records is about the code beneath it.

…ound merge against it The ground subtype relation and the solver's bound merge exist only operationally — `constrain_go` and `CompactType::merge` implement them without ever writing them down — so their properties (is subtyping transitive? is the merge associative? does the checker decide the relation?) have been readings of code, not statements. This PR adds `formal/`, a Lean 4 model that states both declaratively over the index coordinate the stack below establishes, proves the metatheory sorry-free, and pins the model to the implementation with a differential oracle per operation. The headline theorem for subtyping is **transitivity with no fragment restriction and no environment side conditions**: earlier editions of this model (developed on the retired name-coordinate stack, #79) proved it only for a canonical-spelling fragment under six identity-acting rename environments, and the σ-gap they reconciled never forms here — the measured sense in which the coordinate below is the right design. For the merge it is **associativity with no side condition**, and uniqueness: the merge is the only way the induced order admits of combining two bounds. Each oracle earned its keep before landing. The subtype oracle's first sweep caught a real capture in the solver's Fun/Fun opening, fixed below in the telescope PR with the mechanism it repairs. The merge oracle's first sweep caught the model intersecting away refinements a hole should have passed through, fixed here. ### The model `Ty`/`Pred` mirror the ground fragment of `Type`, with `Pred.piBound` mirroring `Name::PiBound` and `refined` carrying a refinement set ([grammar and adjudications](https://github.com/cambra-dev/cambra/blob/dmills/formal-model/formal/design.md)). `Sub` is one constructor per `constrain_go` arm; deliberate departures (no trivial-equality short-circuit, no partition-collapse arm, no binder-correspondence edge) are each recorded as tracked decisions in `CclFormal/Sub.lean`. Proved: `Sub.refl` under the uniquely-keyed `Ty.WF` (naming a builder invariant the Rust leaves implicit), checker soundness/completeness giving decidability (`Equiv.lean`), `sub_trans` for well-formed types (`Transitivity.lean`), refinement-order unobservability, and the M2 safety battery — progress, preservation, refinement soundness (`Safety.lean`). ### The merge algebra `Merge.lean` mirrors `compact.rs`'s bound-merging: `CTy` for the ground fragment of `CompactType`, `merge` for the polar `CompactType::merge`/`CompactFun::merge`, and `eqv` for `CompactType`'s own `PartialEq`, so every theorem is quotient-compatible by construction. Proved: `eqv` is an equivalence, `merge` is commutative, idempotent under the input-bound invariant `wf`, a congruence, and **associative unconditionally at both polarities** — the kinds join in the flat semilattice `unknown < {data, compute} < conflict` (`joinKind`) and the domains are combined by polarity alone, so no fold step reads a value a later step can change. The fold is therefore invariant under permutation and duplication of the bound list, and `merge pol` is the least upper bound of the order it induces (`le`) and the only one up to `eqv` (`join_unique`), with the empty position as the least element. Associativity was a *non*-theorem when this model first stated it, and the counterexample was real: the solver selected a function slot's domain combination from a kind that was not settled, so bound arrival order decided accept-vs-reject and one association accepted a collection whose domain was the meet of two others'. The PR below defers that choice to the resolved kind at coalesce, which is what removes the side condition here. ### The differential oracles `lake build` produces the oracle binary; each case is one JSONL line tagged by `"op"`, and `tests/differential_oracle.rs` generates cases with the seeded generator it shares with the type-merge fuzz (`tests/type_gen/mod.rs`), computes the solver's answer, and diffs. The harness is an integration test rather than a `#[cfg(test)]` module in the library: it is a test, and the only solver internal it cannot otherwise reach is `CompactType::merge`, which the `test-helpers` feature opens for it. - `"sub"`: seeded ground pairs, each closed into the ground fragment (`close_all` — every arrow's own-binder references as indices), diffed against `subCheck`. 150k pairs across five seeds, zero mismatches, roughly one pair in twelve index-bearing. - `"merge"`: bound lists folded through `CompactType::merge` exactly as `compact_go` folds a variable's bounds, every step diffed against `merge` up to `eqv`. Each step's left operand is the previous step's result, so the conflicted and multi-alternative states only merging produces are operands too; operands sometimes carry a kind *variable*, the only route to `KindMerge::Unknown`. Clean at 40k steps. `CoErr` has no `emptyProduct`: the empty product is `IncompatibleBounds` on both sides, since bounds with no common shape is what that error already says. Both skip loudly when the oracle binary is absent, so machines without a Lean toolchain stay green, and `./ci.sh oracle` builds the model and runs them where `lake` exists — without that gate nothing notices the model drifting from the solver, in either direction. `CAMBRA_DIFF_SEED`/`CAMBRA_DIFF_N`/`CAMBRA_DIFF_DUMP` control runs. ### Reading order `formal/design.md` (the plan, adjudications, and findings — every claim in it is true of the code beneath this PR), then `Ty.lean` → `Sub.lean` → `Decide.lean`/`Equiv.lean` → `Transitivity.lean`, with `Term.lean`/`Safety.lean` and `Merge.lean` as independent limbs. In `Merge.lean`, read the refinement-slot laws and `joinKind` before the `merge` theorems that use them; the order and uniqueness section is last and depends only on the semilattice laws. The model's development history, including the name-coordinate editions this replaces, is on closed #79.

dpmills force-pushed the dmills/canonical-discharge branch from 3b73c4e to 92f97be Compare August 11, 2026 22:34

dpmills force-pushed the dmills/formal-ground-model-restacked branch from 157940a to a778809 Compare August 11, 2026 22:48

dpmills force-pushed the dmills/canonical-discharge branch from 92f97be to a46740f Compare August 12, 2026 00:09

dpmills force-pushed the dmills/formal-ground-model-restacked branch 2 times, most recently from 4336f6b to 0e14866 Compare August 12, 2026 00:38

dpmills force-pushed the dmills/canonical-discharge branch 2 times, most recently from 193bc2f to 9da26b7 Compare August 12, 2026 21:00

dpmills force-pushed the dmills/formal-ground-model-restacked branch from 0e14866 to 0a86cab Compare August 12, 2026 21:02

dpmills force-pushed the dmills/canonical-discharge branch from 9da26b7 to cedc80e Compare August 12, 2026 22:36

dpmills force-pushed the dmills/formal-ground-model-restacked branch from 0a86cab to be76c76 Compare August 12, 2026 22:36

dpmills force-pushed the dmills/canonical-discharge branch from cedc80e to 7bd7b54 Compare August 12, 2026 22:45

dpmills force-pushed the dmills/formal-ground-model-restacked branch from be76c76 to fbbd4ff Compare August 12, 2026 22:45

dpmills force-pushed the dmills/canonical-discharge branch from 7bd7b54 to 0148d4f Compare August 13, 2026 05:39

dpmills force-pushed the dmills/formal-ground-model-restacked branch from fbbd4ff to 6e89114 Compare August 13, 2026 05:39

dpmills force-pushed the dmills/canonical-discharge branch from 0148d4f to b92238a Compare August 13, 2026 06:01

dpmills force-pushed the dmills/formal-ground-model-restacked branch from 6e89114 to 95c8d69 Compare August 13, 2026 06:01

dpmills force-pushed the dmills/formal-ground-model-restacked branch from 2301e7b to 1061e8f Compare August 18, 2026 05:22

dpmills force-pushed the dmills/canonical-discharge branch from 5a8606f to d297c1a Compare August 18, 2026 05:22

dpmills added 19 commits August 17, 2026 22:43

dpmills force-pushed the dmills/canonical-discharge branch from d297c1a to f54190c Compare August 18, 2026 05:47

dpmills force-pushed the dmills/formal-ground-model-restacked branch from 1061e8f to 30405ba Compare August 18, 2026 05:47

dpmills force-pushed the dmills/canonical-discharge branch from f54190c to aa94554 Compare August 18, 2026 21:59

dpmills closed this Aug 18, 2026

dpmills mentioned this pull request Aug 18, 2026

Model the type system in Lean, and check the solver's subtyping and bound merge against it #109

Draft

Navigation Menu

Uh oh!

Add a Lean model of the CCL type system and fuzz the solver against it - #79

Add a Lean model of the CCL type system and fuzz the solver against it#79
dpmills wants to merge 23 commits into
dmills/canonical-dischargefrom
dmills/formal-ground-model-restacked

dpmills commented Aug 11, 2026 •

edited

Loading

Uh oh!

dpmills commented Aug 11, 2026

Uh oh!

dpmills commented Aug 18, 2026

Uh oh!

dpmills commented Aug 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

dpmills commented Aug 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Reading order

The harnesses

What to be suspicious of

Uh oh!

dpmills commented Aug 11, 2026

Uh oh!

dpmills commented Aug 18, 2026

Uh oh!

dpmills commented Aug 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

dpmills commented Aug 11, 2026 •

edited

Loading