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

Closed

dpmills wants to merge 23 commits into

dmills/canonical-dischargefrom

dmills/formal-ground-model-restacked

Commits on Aug 18, 2026

Canonical Pi binders at the solver's flattening layer
dpmills
committed
9385b27
The canonical Pi-binder rule lives in one place
dpmills
committed
80b9b8d
Rebase fallout: the bounded-annotation marker is `BoundedHole` now
dpmills
committed
9be5020
State the canonical-Pi-binder invariant, and make the codomain depth un-derivable
dpmills
committed
2194bc3
Refinements are an unordered set, not a stack of layers
dpmills
committed
3f0a369
Canonical discharge: a cast's claims are term-determined, not route-determined
dpmills
committed
91f6cc0
Retire the wholesale cast-target sync: rebuild passes restore the canonical split
dpmills
committed
f54190c
formal/: Lean 4 model of ground subtyping, with a differential oracle against `constrain`
dpmills
committed
0d3add5
formal/: decidability of ground subtyping; transitivity refuted, repaired, machine-checked
dpmills
committed
e392347
Confluence fuzz for the bound graph; finding: refinement layers stack in arrival order
dpmills
committed
eb33fba
formal/: transitivity proved for the non-dependent fragment; the dependent case's obstruction stated
dpmills
committed
005f6ad
Probe: α-variant dependent types split identity sites (SpecKey, bound merge)
dpmills
committed
ecda39b
formal/: pure transitivity for the canonical fragment — the σ-gap dissolved
dpmills
committed
4a4b166
formal/: the model carries a claim set, and claim order is proved unobservable
dpmills
committed
62d06e8
differential: keep the bridge near-miss inside `Ty.WF`
dpmills
committed
934a78f
Record why minting canonical Pi binders does not work
dpmills
committed
5a0bf00
Merge algebra (M4b), part 1: the model, its equivalence, commutativity, idempotence
dpmills
committed
c388f38
Merge algebra (M4b), part 2: congruence, guarded associativity, the mixed-kind counterexample, fold invariance
dpmills
committed
4269811
M2, part 1: the definitional core — terms, values, small-step, typing
dpmills
committed
83c1f18
Plan M3b: dependent-fragment transitivity — canonical fragment now, α-aware as a bug hunt
dpmills
committed
ccccd96
M2 safety: progress, preservation, refinement soundness (sorry-free) — plus a partition-collapse finding
dpmills
committed
069384e
Retire the partition-collapse modeling; the rule it mirrors is gone
dpmills
committed
6bd2db5
Retire the refuted inside-out-indexing footnote for a citation
dpmills
committed
30405ba

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

Commits on Aug 18, 2026

Canonical Pi binders at the solver's flattening layer

The canonical Pi-binder rule lives in one place

Rebase fallout: the bounded-annotation marker is `BoundedHole` now

State the canonical-Pi-binder invariant, and make the codomain depth un-derivable

Refinements are an unordered set, not a stack of layers

Canonical discharge: a cast's claims are term-determined, not route-determined

Retire the wholesale cast-target sync: rebuild passes restore the canonical split

formal/: Lean 4 model of ground subtyping, with a differential oracle against `constrain`

formal/: decidability of ground subtyping; transitivity refuted, repaired, machine-checked

Confluence fuzz for the bound graph; finding: refinement layers stack in arrival order

formal/: transitivity proved for the non-dependent fragment; the dependent case's obstruction stated

Probe: α-variant dependent types split identity sites (SpecKey, bound merge)

formal/: pure transitivity for the canonical fragment — the σ-gap dissolved

formal/: the model carries a claim set, and claim order is proved unobservable

differential: keep the bridge near-miss inside `Ty.WF`

Record why minting canonical Pi binders does not work

Merge algebra (M4b), part 1: the model, its equivalence, commutativity, idempotence

Merge algebra (M4b), part 2: congruence, guarded associativity, the mixed-kind counterexample, fold invariance

M2, part 1: the definitional core — terms, values, small-step, typing

Plan M3b: dependent-fragment transitivity — canonical fragment now, α-aware as a bug hunt

M2 safety: progress, preservation, refinement soundness (sorry-free) — plus a partition-collapse finding

Retire the partition-collapse modeling; the rule it mirrors is gone

Retire the refuted inside-out-indexing footnote for a citation