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

.github/workflows/ci.yml

@@ -75,6 +75,22 @@ jobs:
         if: steps.filter.outputs.code == 'true'
         uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
 
+      # The Lean development in `formal/` is checked by *building* it: `lake
+      # build` elaborates every theorem and evaluates every `#guard`, so without
+      # a toolchain on the runner the `Formal model` step below would skip and
+      # gate nothing. elan is pinned by release and verified by hash, the same
+      # discipline as pinning the actions above by SHA, and it installs the
+      # version `formal/lean-toolchain` names rather than a floating one.
+      - name: Setup Lean
+        if: steps.filter.outputs.code == 'true'
+        run: |
+          curl -sSfL -o /tmp/elan.tar.gz \
+            https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz
+          echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2  /tmp/elan.tar.gz" \
+            | sha256sum -c -
+          tar xzf /tmp/elan.tar.gz -C /tmp
+          /tmp/elan-init -y --default-toolchain "$(cat formal/lean-toolchain)" >/dev/null
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
       # 3. Run Checks (Only if code changed)
       - name: Shellcheck
@@ -137,6 +153,15 @@ jobs:
         if: steps.filter.outputs.code == 'true' && (success() || failure())
         run: ./ci.sh doc
 
+      - name: Formal model
+        # Builds the Lean model, which is what checks its proofs, then diffs the
+        # model's verdicts against the solver's. Placed before `Test` so the
+        # oracle binary exists by the time the suite runs: the differential tests
+        # skip themselves without it, and skipping is the failure mode this step
+        # exists to remove.
+        if: steps.filter.outputs.code == 'true' && (success() || failure())
+        run: ./ci.sh formal
+
       - name: Test
         # Run even if earlier steps failed so we see all errors in one run.
         # (Steps default to `if: success()`, which skips on prior failure.)

ci.sh

@@ -48,6 +48,26 @@ ci_clippy_lib() { cargo clippy --lib -- -D warnings; }
 # argument as `ci_clippy_serde`: a configuration nothing runs is a
 # configuration that rots.
 ci_test() { cargo test -q ${DEEP_TYPECHECK:+--features deep-typecheck}; }
+# The formal model (`formal/`): building it is what elaborates every theorem and
+# evaluates every `#guard` in the Lean development, and the differential tests
+# then diff the model's verdicts against the solver's. Those tests skip
+# themselves when the oracle binary is absent, so without this gate nothing
+# notices the model drifting from the solver — the same rot argument as
+# `ci_clippy_serde`, and the drift is silent in both directions. A machine with
+# no Lean toolchain skips, loudly; under CI a missing toolchain is a broken gate
+# rather than a local convenience, so it fails instead.
+ci_formal() {
+  if ! command -v lake >/dev/null 2>&1; then
+    if [[ -n "${CI:-}" ]]; then
+      echo "ci_formal: no Lean toolchain (lake) under CI — this gate would be a no-op" >&2
+      return 1
+    fi
+    echo "ci_formal: no Lean toolchain (lake) — formal model not checked" >&2
+    return 0
+  fi
+  (cd formal && lake build) || return 1
+  cargo test -q --test differential_oracle
+}
 ci_doc() {
   RUSTDOCFLAGS="-A warnings -D rustdoc::broken_intra_doc_links" \
     cargo doc --no-deps
@@ -120,6 +140,9 @@ ci_all() {
   # shellcheck disable=SC2310
   # intentional: || captures failure without exiting
   ci_test || failed=1
+  # shellcheck disable=SC2310
+  # intentional: || captures failure without exiting
+  ci_formal || failed=1
   exit "${failed}"
 }
 

formal/.gitignore

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

formal/CclFormal.lean

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