Proof layer for the capability checker (55 theorems) + march main resync

.github/workflows/conformance.yml

@@ -52,44 +52,81 @@ jobs:
         uses: actions/checkout@v4
 
       # Installs elan + the toolchain pinned in lean-toolchain, then runs
-      # `lake build march-lean-check`. This repo's lakefile.toml has no
-      # defaultTargets, so a bare `lake build` (lean-action's default)
+      # `lake build MarchLean march-lean-check`. This repo's lakefile.toml has
+      # no defaultTargets, so a bare `lake build` (lean-action's default)
       # reports "0 jobs" and silently builds nothing — build-args names the
-      # target explicitly. use-mathlib-cache: false skips the (inapplicable)
+      # targets explicitly. use-mathlib-cache: false skips the (inapplicable)
       # cache-restore step rather than silently no-op'ing through
       # auto-detection (this repo has no Mathlib dependency).
-      - name: Install Lean toolchain and build march-lean-check
+      #
+      # BOTH targets are named on purpose. `MarchLeanCheck.lean` imports the
+      # individual modules it needs, NOT the `MarchLean` library root, so
+      # building only the executable leaves every module outside the exe's
+      # import closure unbuilt — which since P0 includes the proof layer
+      # (`MarchLean/Calculus/Verdicts.lean`, `Concrete.lean`). Those files are
+      # kernel-checked ONLY if `MarchLean` is built, so dropping it here would
+      # let every theorem rot undetected while CI stayed green.
+      - name: Install Lean toolchain and build the library and checker
         uses: leanprover/lean-action@v1
         with:
-          build-args: march-lean-check
+          build-args: MarchLean march-lean-check
           use-mathlib-cache: false
 
+      # Lean treats `sorry` as a WARNING, not an error, so the build above
+      # would pass with unproven theorems. The Calculus/ proof layer (P0,
+      # specs/plans/2026-08-08-calculus-proof-capabilities-design.md) is only
+      # evidence if this gate holds. Source-level grep rather than build-log
+      # parsing, so a failure names the offending file:line.
+      - name: Forbid sorry/admit in Lean sources
+        run: |
+          if grep -rnE '\b(sorry|admit)\b' --include='*.lean' MarchLean/ MarchLean.lean MarchLeanCheck.lean; then
+            echo "::error::sorry/admit found in Lean sources (see matches above)"; exit 1
+          fi
+
       # Pinned to a march main SHA (not a branch) for reproducibility. This
-      # pin (7c1d701c) is march main HEAD as of the post-slice-(c)
-      # re-baseline (2026-08-03); its corpus has grown to 242 files. It
-      # supersedes 0a119c9d, which was 28 commits behind.
+      # pin (6867c783) is march main HEAD as of the capability resync
+      # (2026-08-08); its corpus has grown to 277 files. It supersedes
+      # 7c1d701c, which was 71 commits behind.
+      #
+      # Drift from 7c1d701c was assessed before bumping. Unlike the previous
+      # two bumps this one was NOT inert — it surfaced five real divergences,
+      # four of them false ACCEPTS, all fixed in the commits that accompany
+      # this pin:
+      #   - lib/dump/ast_json.ml: CHANGED, but compatibly. format_version is
+      #     still 3 (bin/main.ml:1934), and DNeeds.paths still emits the same
+      #     array of dotted paths. What is NEW is a parallel `scopes` array
+      #     (see below).
+      #   - Check 1 now reaches TYPE DECLARATIONS (caps_in_type_def, via the
+      #     new lib/caps/cap_surface_ty.ml) and FUNCTION BODIES
+      #     (cap_annots_in_expr). Both were holes here; both are now modeled.
+      #   - R2: root_cap is no longer an ambient global (typecheck.ml:5118).
+      #   - R4a: cap_narrow is now polymorphic and subsumption moved to a
+      #     deferred sweep (check_cap_narrow_sites); modeled by
+      #     CapCheck.capNarrowViolation.
       #
-      # Drift from 0a119c9d was assessed before bumping:
-      #   - lib/dump/ast_json.ml: UNCHANGED. The emitter envelope is
-      #     identical; format_version and module_caps keys untouched.
-      #   - typecheck.ml +599, refine_check.ml +870, new precond_infer.ml
-      #     (580) — but exactly ONE new Err.error-level check across all of
-      #     it: `cap verified` (undischarged return-type constraint). That
-      #     is a sixth behavioral capability cap and it is NOT modeled here,
-      #     because it requires refinement-obligation discharge, which is
-      #     out of fragment. Its corpus files (accept/t132, accept/t135,
-      #     reject/t133) skip today for unrelated refinement-syntax reasons
-      #     — so we are currently safe by accident, not by design. If those
-      #     files ever stop skipping, `cap verified` becomes a live
-      #     false-accept source. See specs/march-findings.md.
-      #   - march#136 (calls_in_expr now total over Ast.expr) IS included in
-      #     this pin. It fixes the blind spot that made our deliberately
-      #     total bodyCalls disagree with march on calls nested in tuples,
-      #     records, and lambdas.
+      # THREE KNOWN GAPS remain against this pin. None is corpus-visible, so
+      # a green run is NOT evidence about them — each needs a hand-built
+      # probe (see specs/march-findings.md):
+      #   - PATH-SCOPED CAPABILITIES. march added `needs IO.FileRead("/etc")`
+      #     and emits the scope in a new `scopes` array; Elab's DNeeds
+      #     decoder reads only `paths` and drops it. Since scope_subsumes
+      #     says a scope never subsumes unscoped, a narrow declaration
+      #     decodes here as broad — a FALSE ACCEPT by construction. Zero
+      #     corpus files use the syntax today, which is exactly why this is
+      #     dangerous rather than reassuring.
+      #   - Tagged: march's caps_in_ty now RECURSES into Tagged (its old
+      #     `| Tagged -> []` arm is gone, deliberately: skipping it blinded
+      #     the walk to Tagged(R, Cap(IO))). CapCheck.capsInTy still mirrors
+      #     the old behavior. No corpus witness.
+      #   - normalize: march's now dedupes before filtering; ours does not,
+      #     so the two differ on duplicate cap lists. Latent only because
+      #     normalize is not on this checker's verdict path.
       #
-      # Corpus grew 233 -> 242; all 9 new files skip (refinement-typed) and
-      # every pre-existing skip is unchanged, so the ledger delta is purely
-      # additive.
+      # Corpus grew 242 -> 277 (+35, heavily capability-focused). The ledger
+      # delta is NOT purely additive this time: accept/t49_transitive_use_
+      # covered regressed from MATCH to SKIP, and the four CORPUS_VIOLATION
+      # entries seen against the old local march 0.2.0 were artifacts of that
+      # stale binary and are gone.
       #
       # Bump periodically; no need to chase every push. setup-march builds
       # march from source and caches the result keyed on this SHA (actions/
@@ -99,7 +136,7 @@ jobs:
         id: setup-march
         uses: march-language/setup-march@main
         with:
-          march-version: 7c1d701cf561c13ad094845f52175f449e1c1892
+          march-version: 6867c783fbde7fb8ab58bae4b4fbe36703b626a1
 
       # Only the conformance corpora are needed from march's own repo (the
       # binary itself came from setup-march above); pinned to the exact

MarchLean.lean

@@ -5,6 +5,11 @@ import MarchLean.Result
 import MarchLean.Linearity
 import MarchLean.Infer
 import MarchLean.Compare
+import MarchLean.Calculus.Lattice
+import MarchLean.Calculus.Walks
 import MarchLean.CapLattice
 import MarchLean.CapCheck
 import MarchLean.TailCall
+import MarchLean.Calculus.Verdicts
+import MarchLean.Calculus.Concrete
+import MarchLean.Calculus.CheckCaps

MarchLean/Calculus/CheckCaps.lean

@@ -0,0 +1,158 @@
+import MarchLean.Calculus.Concrete
+import MarchLean.Calculus.Verdicts
+import MarchLean.CapCheck
+
+/-!
+# Whole-checker properties, and where they stop being true
+
+Two properties that sound like they should hold of `CapCheck.checkCaps`:
+
+1. **Normalize-stability** — replacing `needs L` by `needs (normalize L)`
+   never changes the verdict.
+2. **IO-cap monotonicity** — adding a capability to `needs` never flips
+   accept into reject.
+
+Both are **true for the subsumption-coverage core** (Checks 1/4/5, whose only
+cap reasoning is `covered declared c`) and **false for the full checker**. The
+boundary is the behavioral-cap layer in both cases, and it is the same
+mechanism twice: `cap no_extern` reads the `needs` list for a *property of the
+list itself* (`hasForeignNeed`) rather than asking what the list covers. A
+check that inspects the syntax of a declaration set, rather than its
+denotation, is not stable under any operation that preserves only the
+denotation — and `normalize` is exactly such an operation
+(`Calculus.coveredIn_normalizeIn`).
+
+So the counterexamples are not curiosities to be worked around. They say:
+**`normalize` may never be applied to a `needs` list before a behavioral-cap
+check runs.** Nothing in the checker does that today; these theorems are what
+make it a checked invariant rather than an accident.
+
+Each pair below is stated so the *mechanism* is kernel-checked (`decide` over
+`CapLattice` and `hasForeignNeed`, both total), with the end-to-end
+`checkCaps` verdict pinned separately by `native_decide` — `checkCaps` runs
+through `partial def`s and so has no equation lemmas for the kernel to unfold.
+The mechanism is the part that generalizes; the end-to-end pin is the part
+that proves the mechanism actually reaches a verdict.
+-/
+
+namespace MarchLean.Calculus.CheckCaps
+
+open MarchLean.Calculus MarchLean.CapLattice MarchLean.CapCheck MarchLean.Syntax
+
+/-! ## 1. Normalize-stability
+
+Positive direction, already proved for any well-formed table:
+`Calculus.coveredIn_normalizeIn` — normalizing a declared set never changes
+what it covers. Instantiated at the shipping lattice as
+`Concrete.normalize_covered`. That is the whole coverage core. -/
+
+/-- Restated here so the pair reads together: on the coverage core,
+normalizing `needs` is invisible. -/
+theorem coverage_core_normalize_stable (L : List String) (c : String) :
+    coveredIn hierarchy (normalize L) c = coveredIn hierarchy L c :=
+  Concrete.normalize_covered L c
+
+/-! ### The counterexample
+
+`IO.Foreign`'s parent is `IO`, so `normalize` absorbs it. -/
+
+theorem normalize_absorbs_foreign : normalize ["IO", "IO.Foreign"] = ["IO"] := by
+  decide
+
+/-- …and `hasForeignNeed` — which `cap no_extern` consults — cannot see the
+absorbed entry, because it tests the *spelling* of each path rather than what
+the set covers. This is the whole defect in two lines. -/
+theorem foreign_need_lost_by_normalize :
+    (["IO", "IO.Foreign"].any hasForeignNeed) = true ∧
+    ((normalize ["IO", "IO.Foreign"]).any hasForeignNeed) = false := by
+  -- `native_decide` rather than `decide`: `hasForeignNeed` splits on ".",
+  -- and `String.splitOn` does not reduce in the kernel. The lattice half of
+  -- this counterexample (`normalize_absorbs_foreign`) IS kernel-checked.
+  native_decide
+
+/-- The same two `needs` lists are coverage-equivalent, which is precisely why
+this is a defect and not merely a difference: no coverage-based check could
+tell them apart, and `no_extern` is not a coverage-based check. -/
+theorem normalize_foreign_coverage_equivalent (c : String) :
+    coveredIn hierarchy ["IO", "IO.Foreign"] c
+      = coveredIn hierarchy (normalize ["IO", "IO.Foreign"]) c :=
+  (coverage_core_normalize_stable ["IO", "IO.Foreign"] c).symm
+
+/-- End-to-end: the un-normalized module violates `no_extern`… -/
+private def foreignNeedUnnormalized : Module := {
+  decls := [Decl.dmod "NoFFI" [
+    Decl.dopts ["no_extern"],
+    Decl.dneeds ["IO", "IO.Foreign"],
+    Decl.dfn "ping" [("host", Lin.unrestricted, some (Ty.con "String" []))] none
+      (Term.lit (Lit.int 1) (Ty.con "Int" []))]],
+  schemes := [], insts := [], moduleCaps := [] }
+
+/-- …and the normalized one does not. -/
+private def foreignNeedNormalized : Module := {
+  decls := [Decl.dmod "NoFFI" [
+    Decl.dopts ["no_extern"],
+    Decl.dneeds (normalize ["IO", "IO.Foreign"]),
+    Decl.dfn "ping" [("host", Lin.unrestricted, some (Ty.con "String" []))] none
+      (Term.lit (Lit.int 1) (Ty.con "Int" []))]],
+  schemes := [], insts := [], moduleCaps := [] }
+
+/-- **Normalize-stability is FALSE for the full checker.** Same module, same
+coverage, `needs` replaced by its own normalization — and the verdict tier
+moves from `violation` to `ok`. -/
+theorem normalize_not_verdict_preserving :
+    tierOf (checkCaps foreignNeedUnnormalized) = .violation ∧
+    tierOf (checkCaps foreignNeedNormalized) = .ok := by
+  native_decide
+
+/-! ## 2. IO-cap monotonicity
+
+Positive direction, already proved for any well-formed table:
+`Calculus.coveredIn_mono` — enlarging the declared set never removes
+coverage, so no coverage-core check can turn accept into reject. -/
+
+/-- Restated at the shipping lattice: on the coverage core, adding a `needs`
+entry only ever helps. -/
+theorem coverage_core_monotone {L L' : List String} {c : String}
+    (hsub : ∀ x ∈ L, x ∈ L') (h : coveredIn hierarchy L c = true) :
+    coveredIn hierarchy L' c = true :=
+  coveredIn_mono hsub h
+
+/-! ### The counterexample -/
+
+private def noExternPlain : Module := {
+  decls := [Decl.dmod "NoFFI" [
+    Decl.dopts ["no_extern"],
+    Decl.dneeds ["IO"],
+    Decl.dfn "ping" [("host", Lin.unrestricted, some (Ty.con "String" []))] none
+      (Term.lit (Lit.int 1) (Ty.con "Int" []))]],
+  schemes := [], insts := [], moduleCaps := [] }
+
+private def noExternPlusForeign : Module := {
+  decls := [Decl.dmod "NoFFI" [
+    Decl.dopts ["no_extern"],
+    Decl.dneeds ["IO", "IO.Foreign"],
+    Decl.dfn "ping" [("host", Lin.unrestricted, some (Ty.con "String" []))] none
+      (Term.lit (Lit.int 1) (Ty.con "Int" []))]],
+  schemes := [], insts := [], moduleCaps := [] }
+
+/-- **IO-cap monotonicity is FALSE for the full checker.** `["IO"]` is a
+subset of `["IO", "IO.Foreign"]`, the added cap is already covered by `IO`
+(so it grants no new authority whatsoever), and yet the verdict flips
+`ok → violation`.
+
+Declaring a capability is itself observable behavior at the behavioral layer:
+`no_extern` objects to the *declaration* of foreign authority, not to holding
+it. That is why monotonicity has no chance here, and why the coverage-core
+theorem above is the strongest true form of it. -/
+theorem monotonicity_fails_at_behavioral_layer :
+    tierOf (checkCaps noExternPlain) = .ok ∧
+    tierOf (checkCaps noExternPlusForeign) = .violation := by
+  native_decide
+
+/-- The added capability is redundant for coverage — `IO` already subsumes
+`IO.Foreign` — so the flip above cannot be explained as new authority. -/
+theorem added_cap_was_already_covered :
+    coveredIn hierarchy ["IO"] "IO.Foreign" = true := by
+  decide
+
+end MarchLean.Calculus.CheckCaps

MarchLean/Calculus/Concrete.lean

@@ -0,0 +1,56 @@
+import MarchLean.CapLattice
+
+/-!
+# The shipping lattice, discharged
+
+`WellFormedB hierarchy` by kernel `decide` (~1s on this toolchain), then
+every abstract theorem of `Calculus/Lattice.lean` instantiated at the
+shipping `CapLattice` names.
+
+If march ever adds a duplicate name, a dangling parent, or a cycle to
+`cap_lattice.ml` and the port follows, **the `decide` below is what fails** —
+loudly, at build time. That failure mode is the point of this file: before
+P0 the table's forest-ness was a comment, and a cycle would have made
+`capAncestors` silently truncate with no error anywhere.
+-/
+
+namespace MarchLean.Calculus.Concrete
+open MarchLean.Calculus MarchLean.CapLattice
+
+theorem hierarchy_wellFormed : WellFormedB hierarchy = true := by decide
+
+theorem capSubsumes_refl (c : String) : capSubsumes c c = true :=
+  subsumesIn_refl hierarchy c
+
+theorem capSubsumes_trans {a b c : String}
+    (h₁ : capSubsumes a b = true) (h₂ : capSubsumes b c = true) :
+    capSubsumes a c = true :=
+  subsumesIn_trans hierarchy_wellFormed h₁ h₂
+
+theorem capSubsumes_antisymm {p c : String}
+    (h₁ : capSubsumes p c = true) (h₂ : capSubsumes c p = true) : p = c :=
+  subsumesIn_antisymm hierarchy_wellFormed h₁ h₂
+
+theorem capSiblings_incomparable {p c q : String}
+    (hp : capParent p = some q) (hc : capParent c = some q) (hne : p ≠ c) :
+    capSubsumes p c = false :=
+  siblings_incomparable hierarchy_wellFormed hp hc hne
+
+theorem capAncestors_fuel_adequate {f : Nat} (hf : hierarchy.length ≤ f)
+    (c : String) : capAncestorsFuel f c = capAncestors c :=
+  ancestorsIn_fuel_adequate hierarchy_wellFormed hf c
+
+theorem normalize_covered (L : List String) (c : String) :
+    coveredIn hierarchy (normalize L) c = coveredIn hierarchy L c :=
+  coveredIn_normalizeIn hierarchy_wellFormed L c
+
+theorem normalize_idem (L : List String) : normalize (normalize L) = normalize L :=
+  normalizeIn_idem hierarchy L
+
+example : capSubsumes "LibC" "LibC" = true := capSubsumes_refl _
+example (p : String) : capSubsumes p "LibC" = true ↔ p = "LibC" :=
+  subsumesIn_of_absent (by decide)
+example : capSubsumes "IO" "LibC" = false := by decide
+
+end MarchLean.Calculus.Concrete
+