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

.github/workflows/ci.yml

@@ -153,6 +153,19 @@ jobs:
         # superlinear on nested comprehensions (see `ci_test` / `debug_typecheck`).
         run: DEEP_TYPECHECK=1 ./ci.sh test
 
+      - name: Test (reversed refinement order)
+        if: steps.filter.outputs.code == 'true' && (success() || failure())
+        # A claim set is unordered by contract, but two classes of
+        # order-dependence survive a compile-clean rewrite and only running the
+        # suite both ways exercises them: a consumer that iterates the set and
+        # lets the order reach something observable, and a dedup that keeps the
+        # first-inserted of two `eq`-equal claims whose predicate terms carry
+        # different embedded type slots. Nothing in the type system catches
+        # either, so an unrun knob would rot exactly as an uncompiled feature
+        # does. The env var is read at *runtime*, so this reuses the binaries
+        # the step above already built.
+        run: CAMBRA_REFINEMENT_ORDER=reverse ./ci.sh test
+
         # 4. Success Signal for noops
       - name: No-op for docs
         if: steps.filter.outputs.code == 'false'

ci.sh

@@ -39,6 +39,14 @@ ci_clippy_lib() { cargo clippy --lib -- -D warnings; }
 # `deep-typecheck` feature). The GitHub workflow sets it so automated runs keep
 # exercising that check; it stays off for a bare local `./ci.sh` because it is
 # superlinear on nested comprehensions (that cost is why it is gated).
+#
+# `CAMBRA_REFINEMENT_ORDER=reverse` (read at runtime, debug builds only) flips
+# the physical order of every refinement claim set. The workflow runs the suite
+# both ways: set semantics makes that order meaningless by contract, but a
+# consumer that lets it become observable — or a dedup keeping the
+# first-inserted of two `eq`-equal claims — compiles clean either way. Same
+# argument as `ci_clippy_serde`: a configuration nothing runs is a
+# configuration that rots.
 ci_test() { cargo test -q ${DEEP_TYPECHECK:+--features deep-typecheck}; }
 ci_doc() {
   RUSTDOCFLAGS="-A warnings -D rustdoc::broken_intra_doc_links" \

formal/.gitignore

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

formal/CclFormal.lean

@@ -0,0 +1,10 @@
+import CclFormal.Ty
+import CclFormal.Merge
+import CclFormal.Term
+import CclFormal.Safety
+import CclFormal.Sub
+import CclFormal.Decide
+import CclFormal.Json
+import CclFormal.Props
+import CclFormal.Equiv
+import CclFormal.Transitivity

formal/CclFormal/Decide.lean

@@ -0,0 +1,206 @@
+import CclFormal.Sub
+
+/-!
+# The executable ground subtype checker
+
+`subCheck` is the Bool-valued decision procedure for `Sub` — the mirror of
+`constrain_go`'s ground control flow, and the executable half of the M1
+differential oracle (`subCheck` vs `constrain_subtype` on ground pairs).
+Soundness and completeness against `Sub` are proved in
+`CclFormal/Equiv.lean`, so the relation is decidable and every `#guard`
+below is a fact about `Sub` itself.
+-/
+
+namespace CclFormal
+
+/-- Bool form of `kindOk`. -/
+def kindOkB : FunKind → FunKind → Bool
+  | .compute, .data => false
+  | _, _ => true
+
+mutual
+
+/-- Decide `Sub ρl ρr lhs rhs`, arm for arm with `constrain_go`'s ground
+fragment. -/
+def subCheck (ρl ρr : Ren) (lhs rhs : Ty) : Bool :=
+  match lhs, rhs with
+  | .base a, .base b => a == b
+  | .uintRange a, .uintRange b => a == b
+  | .dataSource a, .dataSource b => a == b
+  | .txn, .txn => true
+  | .fn n0 k0 d0 c0, .fn n1 k1 d1 c1 =>
+      kindOkB k0 k1 &&
+      (if k0 == .data && k1 == .data then
+        subCheck ρr ρl d1 d0 && subCheck ρl ρr d0 d1
+      else
+        subCheck ρr ρl d1 d0) &&
+      subCheck (codRen n0 n1 ρl) ρr c0 c1
+  | .tuple a, .tuple b => subSeq ρl ρr a b
+  | .record a, .record b => subFields ρl ρr a b
+  | .variant a, .variant b => subTags ρl ρr b a
+  | lhs, rhs =>
+      -- The refinement arm doubles as the mismatch catch-all: with no
+      -- refinement layer on either side this is `constrain_go`'s final
+      -- `Mismatch`.
+      if _h : lhs.peel.2 = [] ∧ rhs.peel.2 = [] then false
+      else
+        (deficit ρl ρr lhs.peel.2 rhs.peel.2).isEmpty &&
+        subCheck ρl ρr lhs.peel.1 rhs.peel.1
+termination_by sizeOf lhs + sizeOf rhs
+decreasing_by
+  all_goals simp_wf
+  all_goals first
+    | omega
+    | exact Ty.peel_sum_lt _ _ _h
+
+/-- Tuple positions, in demand (rhs) order. -/
+def subSeq (ρl ρr : Ren) (a b : List Ty) : Bool :=
+  match a, b with
+  | _, [] => true
+  | [], _ :: _ => false
+  | t0 :: a', t1 :: b' => subCheck ρl ρr t0 t1 && subSeq ρl ρr a' b'
+termination_by sizeOf a + sizeOf b
+decreasing_by all_goals (simp_wf; omega)
+
+/-- Record fields the rhs demands, looked up find-first in the lhs. -/
+def subFields (ρl ρr : Ren) (a b : List (String × Ty)) : Bool :=
+  match b with
+  | [] => true
+  | (n, t1) :: rest =>
+      (match _h : lookupBy a n with
+        | some t0 => subCheck ρl ρr t0 t1
+        | none => false) &&
+      subFields ρl ρr a rest
+termination_by sizeOf a + sizeOf b
+decreasing_by
+  all_goals simp_wf
+  · have := lookupBy_sizeOf _h
+    omega
+  · omega
+
+
+/-- Variant tags the lhs may produce, looked up find-first in the rhs. -/
+def subTags (ρl ρr : Ren) (b a : List (FieldKey × Ty)) : Bool :=
+  match a with
+  | [] => true
+  | (k, t0) :: rest =>
+      (match _h : lookupBy b k with
+        | some t1 => subCheck ρl ρr t0 t1
+        | none => false) &&
+      subTags ρl ρr b rest
+termination_by sizeOf b + sizeOf a
+decreasing_by
+  all_goals simp_wf
+  · have := lookupBy_sizeOf _h
+    omega
+  · omega
+
+end
+
+/-!
+## Executable spec examples
+
+One `#guard` per adjudicated behavior (see `formal/design.md`, "M0 status
+and adjudicated decisions") — the checker refusing to build is the cheapest
+regression net for the rules' shape.
+-/
+
+/- `{Int | p} <: Int` — dropping a refinement is subsumption. -/
+#guard subCheck .id .id (.refined (.base .int) [.elem]) (.base .int) = true
+
+/- `Int ⊀ {Int | p}` — a refinement cannot be conjured (that is `Restrict`). -/
+#guard subCheck .id .id (.base .int) (.refined (.base .int) [.elem]) = false
+
+/- `{T | p} <: {U | p}` iff `T <: U` — the refined base is covariant:
+`{{a, b} | p} <: {{a} | p}` by record width under the shared predicate. -/
+#guard subCheck .id .id
+  (.refined (.record [("a", .base .int), ("b", .base .bool)]) [.elem])
+  (.refined (.record [("a", .base .int)]) [.elem]) = true
+
+/- `UIntRange` is equality-only: `[0,3) ⊀ [0,4)` despite the inclusion. -/
+#guard subCheck .id .id (.uintRange 3) (.uintRange 4) = false
+#guard subCheck .id .id (.uintRange 3) (.uintRange 3) = true
+
+/- Record width: more fields flow to fewer, never the reverse. -/
+#guard subCheck .id .id
+  (.record [("a", .base .int), ("b", .base .bool)])
+  (.record [("a", .base .int)]) = true
+#guard subCheck .id .id
+  (.record [("a", .base .int)])
+  (.record [("a", .base .int), ("b", .base .bool)]) = false
+
+/- Variant width is the dual: fewer tags flow to more. -/
+#guard subCheck .id .id
+  (.variant [(.name "some", .base .int)])
+  (.variant [(.name "some", .base .int), (.name "none", .base .unit)]) = true
+
+/- The kind lattice `data ⊑ compute`: a collection satisfies a capability
+demand, a capability never satisfies a collection demand. -/
+#guard subCheck .id .id
+  (.fn none .data (.uintRange 2) (.base .int))
+  (.fn none .compute (.uintRange 2) (.base .int)) = true
+#guard subCheck .id .id
+  (.fn none .compute (.uintRange 2) (.base .int))
+  (.fn none .data (.uintRange 2) (.base .int)) = false
+
+/- Compute domains are contravariant; **data-data domains are invariant**
+(the domain *is* the data), so the same domain widening data-to-data fails. -/
+#guard subCheck .id .id
+  (.fn none .compute (.record [("a", .base .int)]) (.base .int))
+  (.fn none .compute (.record [("a", .base .int), ("b", .base .bool)])
+    (.base .int)) = true
+#guard subCheck .id .id
+  (.fn none .data (.record [("a", .base .int)]) (.base .int))
+  (.fn none .data (.record [("a", .base .int), ("b", .base .bool)])
+    (.base .int)) = false
+
+/- The Pi-binder correspondence: a dependent codomain refinement matches its
+α-renamed twin (`(x: [0,3)) ⤇ {Int | __elem == x}` vs the same under `y`). -/
+#guard subCheck .id .id
+  (.fn (some "x") .data (.uintRange 3)
+    (.refined (.base .int) [(.binop "eq" .elem (.var "x"))]))
+  (.fn (some "y") .data (.uintRange 3)
+    (.refined (.base .int) [(.binop "eq" .elem (.var "y"))])) = true
+
+/- ...and a genuinely different binder reference does not match. -/
+#guard subCheck .id .id
+  (.fn (some "x") .data (.uintRange 3)
+    (.refined (.base .int) [(.binop "eq" .elem (.var "x"))]))
+  (.fn (some "y") .data (.uintRange 3)
+    (.refined (.base .int) [(.binop "eq" .elem (.var "z"))])) = false
+
+/- No partition collapse: a `Variant` domain is below only a `Variant`
+domain, so a fan-out-shaped supplier does not satisfy a plain-domain demand.
+The fan-out never presents this pair — it is a `DisjointJoin` over the one
+domain its arms share — so the relation needs no arm for it. -/
+#guard subCheck .id .id
+  (.fn none .data
+    (.variant [(.idx 0, .refined (.uintRange 3) [(.litInt 0)]),
+               (.idx 1, .refined (.uintRange 3) [(.litInt 1)])])
+    (.base .int))
+  (.fn none .data (.uintRange 3) (.base .int)) = false
+
+/- α-equivalent dependent codomains reconcile through the Pi correspondence
+the function arm mints, at every domain shape. -/
+#guard subCheck .id .id
+  (.fn (some "x") .data (.uintRange 3)
+    (.refined (.base .int) [(.binop "eq" .elem (.var "x"))]))
+  (.fn (some "y") .data (.uintRange 3)
+    (.refined (.base .int) [(.binop "eq" .elem (.var "y"))])) = true
+
+/- A chain whose two hops use different rules — the kind lattice at the
+first, contravariant record width at the second — composes: the executable
+face of `sub_trans_id`. -/
+#guard subCheck .id .id
+  (.fn none .data (.record [("a", .base .int)]) (.base .int))
+  (.fn none .compute (.record [("a", .base .int)]) (.base .int)) = true
+#guard subCheck .id .id
+  (.fn none .compute (.record [("a", .base .int)]) (.base .int))
+  (.fn none .compute (.record [("a", .base .int), ("b", .base .bool)])
+    (.base .int)) = true
+#guard subCheck .id .id
+  (.fn none .data (.record [("a", .base .int)]) (.base .int))
+  (.fn none .compute (.record [("a", .base .int), ("b", .base .bool)])
+    (.base .int)) = true
+
+end CclFormal