diff --git a/.github/workflows/conformance.yml b/.github/workflows/conformance.yml index e398c61..d6880b5 100644 --- a/.github/workflows/conformance.yml +++ b/.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 diff --git a/MarchLean.lean b/MarchLean.lean index e09749d..b2bea85 100644 --- a/MarchLean.lean +++ b/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 diff --git a/MarchLean/Calculus/CheckCaps.lean b/MarchLean/Calculus/CheckCaps.lean new file mode 100644 index 0000000..e00249e --- /dev/null +++ b/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 diff --git a/MarchLean/Calculus/Concrete.lean b/MarchLean/Calculus/Concrete.lean new file mode 100644 index 0000000..a608f10 --- /dev/null +++ b/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 + diff --git a/MarchLean/Calculus/Lattice.lean b/MarchLean/Calculus/Lattice.lean new file mode 100644 index 0000000..398d161 --- /dev/null +++ b/MarchLean/Calculus/Lattice.lean @@ -0,0 +1,454 @@ +/-! +# Abstract capability-lattice theory + +`CapLattice.lean`'s five operations, parameterized over the `(name, parent)` +table so their metatheory is proved once for ANY well-formed table and +march's concrete 20-entry `hierarchy` is discharged by `decide` +(`Calculus/Concrete.lean`). The shipping `CapLattice` API is the +specialization of these to `hierarchy`, definition for definition — bodies +here are copied verbatim from the pre-P0 `CapLattice.lean`, table made a +parameter, nothing else changed. +-/ +namespace MarchLean.Calculus + +/-- A capability table: `(cap_path, parent_path)` rows. -/ +abbrev Table := List (String × Option String) + +/-- The parent of a capability in `T`, or `none` for a root or an unknown +(FFI) name. -/ +def parentIn (T : Table) (c : String) : Option String := + match T.find? (fun (n, _) => n == c) with + | some (_, p) => p + | none => none + +/-- Fuel-bounded ancestor chain: `c` followed by every ancestor up to the +root, most-specific first. A name absent from `T` returns just itself (the +FFI-cap base case). -/ +def ancestorsInFuel (T : Table) : Nat → String → List String + | 0, c => [c] + | fuel + 1, c => + match parentIn T c with + | some p => c :: ancestorsInFuel T fuel p + | none => [c] + +/-- `ancestorsIn T c` with fuel `T.length` — adequate for any well-formed +table (proved below: `ancestorsIn_fuel_adequate`). -/ +def ancestorsIn (T : Table) (c : String) : List String := + ancestorsInFuel T T.length c + +/-- Is `parent` an ancestor of, or equal to, `child` in `T`? -/ +def subsumesIn (T : Table) (parent child : String) : Bool := + (ancestorsIn T child).contains parent + +/-- Drop any cap subsumed by another cap present, preserving relative order +of survivors. -/ +def normalizeIn (T : Table) (caps : List String) : List String := + caps.filter (fun c => !caps.any (fun other => other != c && subsumesIn T other c)) + +/-- Is `used` covered by some declared cap, via subsumption? The abstract +form of `CapCheck.covered` (bridged in P2). -/ +def coveredIn (T : Table) (declared : List String) (used : String) : Bool := + declared.any (fun need => subsumesIn T need used) + +/-! ## Table well-formedness + +`CapLattice.lean` asserted in prose that the table "is a finite forest with +no cycles, so `hierarchy.length` is a safe fuel bound". `WellFormedB` makes +that a decidable proposition and `ancestorsIn_fuel_adequate` makes the fuel +claim a theorem; `Calculus/Concrete.lean` discharges the real table. -/ + +/-- The names (first components) of a table. -/ +def namesOf (T : Table) : List String := T.map (·.1) + +/-- No two rows share a name (Boolean, so `decide` can discharge it). -/ +def nodupNamesB : Table → Bool + | [] => true + | (n, _) :: rest => !rest.any (fun (m, _) => m == n) && nodupNamesB rest + +/-- Every parent value that occurs is itself a row's name. march's real +table satisfies this; FFI caps are absent from the table entirely, never +dangling parents. -/ +def parentClosedB (T : Table) : Bool := + T.all (fun (_, p?) => match p? with + | none => true + | some p => T.any (fun (n, _) => n == p)) + +/-- Does the parent chain from `c` reach a parentless node within `fuel` +steps? The acyclicity witness: in a well-formed table every name does so +within `T.length` steps. -/ +def reachesRoot (T : Table) : Nat → String → Bool + | 0, c => (parentIn T c).isNone + | fuel + 1, c => + match parentIn T c with + | none => true + | some p => reachesRoot T fuel p + +/-- Well-formed table: unique names, closed parents, acyclic. This is what +`CapLattice.lean`'s old prose comment ("the table is a finite forest with no +cycles, so `hierarchy.length` is a safe fuel bound") asserted; here it is a +decidable proposition, discharged for the real table in `Concrete.lean`. -/ +def WellFormedB (T : Table) : Bool := + nodupNamesB T && parentClosedB T && T.all (fun (n, _) => reachesRoot T T.length n) + +theorem ancestorsInFuel_head (T : Table) (fuel : Nat) (c : String) : + (ancestorsInFuel T fuel c).head? = some c := by + cases fuel with + | zero => rfl + | succ f => simp only [ancestorsInFuel]; cases parentIn T c <;> rfl + +theorem self_mem_ancestorsIn (T : Table) (c : String) : c ∈ ancestorsIn T c := by + have h := ancestorsInFuel_head T T.length c + unfold ancestorsIn + cases he : ancestorsInFuel T T.length c with + | nil => rw [he] at h; simp at h + | cons x xs => rw [he] at h; simp at h; simp [h] + +theorem subsumesIn_refl (T : Table) (c : String) : subsumesIn T c c = true := by + simp [subsumesIn] + exact self_mem_ancestorsIn T c + +theorem parentIn_eq_none_of_not_mem {T : Table} {c : String} + (h : c ∉ namesOf T) : parentIn T c = none := by + unfold parentIn + cases hf : T.find? (fun (n, _) => n == c) with + | none => rfl + | some row => + exfalso + have hmem := List.mem_of_find?_eq_some hf + have hpred := List.find?_some hf + have : row.1 = c := by + cases row; simpa using hpred + exact h (this ▸ List.mem_map_of_mem hmem) + +theorem reachesRoot_mono {T : Table} {c : String} {fuel fuel' : Nat} + (h : fuel ≤ fuel') (hr : reachesRoot T fuel c = true) : + reachesRoot T fuel' c = true := by + induction fuel generalizing c fuel' with + | zero => + have hnone : parentIn T c = none := by + simpa [reachesRoot, Option.isNone_iff_eq_none] using hr + cases fuel' with + | zero => simpa [reachesRoot, Option.isNone_iff_eq_none] + | succ f => simp [reachesRoot, hnone] + | succ f ih => + cases hp : parentIn T c with + | none => + cases fuel' with + | zero => simp [reachesRoot, hp] + | succ f' => simp [reachesRoot, hp] + | some p => + simp only [reachesRoot, hp] at hr + cases fuel' with + | zero => omega + | succ f' => + have : f ≤ f' := by omega + simp only [reachesRoot, hp] + exact ih this hr + +theorem ancestorsInFuel_stable {T : Table} {c : String} {fuel : Nat} + (h : reachesRoot T fuel c = true) {f : Nat} (hf : fuel ≤ f) : + ancestorsInFuel T f c = ancestorsInFuel T fuel c := by + induction fuel generalizing c f with + | zero => + have hnone : parentIn T c = none := by + simpa [reachesRoot, Option.isNone_iff_eq_none] using h + cases f with + | zero => rfl + | succ f' => simp [ancestorsInFuel, hnone] + | succ k ih => + cases hp : parentIn T c with + | none => + cases f with + | zero => omega + | succ f' => simp [ancestorsInFuel, hp] + | some p => + simp only [reachesRoot, hp] at h + cases f with + | zero => omega + | succ f' => + have : k ≤ f' := by omega + simp only [ancestorsInFuel, hp] + rw [ih h this] + +theorem wf_reachesRoot {T : Table} (wf : WellFormedB T = true) (c : String) : + reachesRoot T T.length c = true := by + have h3 : T.all (fun (n, _) => reachesRoot T T.length n) = true := by + unfold WellFormedB at wf + simp only [Bool.and_eq_true] at wf + exact wf.2 + by_cases hmem : c ∈ namesOf T + · obtain ⟨⟨n, p?⟩, hrow, rfl⟩ := List.mem_map.mp hmem + simpa using List.all_eq_true.mp h3 _ hrow + · have hnone := parentIn_eq_none_of_not_mem hmem + cases hl : T.length with + | zero => simp [reachesRoot, hnone] + | succ k => simp [reachesRoot, hnone] + +theorem ancestorsIn_fuel_adequate {T : Table} (wf : WellFormedB T = true) + {f : Nat} (hf : T.length ≤ f) (c : String) : + ancestorsInFuel T f c = ancestorsIn T c := + ancestorsInFuel_stable (wf_reachesRoot wf c) hf + +theorem ancestorsIn_root {T : Table} {c : String} (h : parentIn T c = none) : + ancestorsIn T c = [c] := by + unfold ancestorsIn + cases T.length with + | zero => rfl + | succ k => simp [ancestorsInFuel, h] + +theorem ancestorsIn_cons {T : Table} (wf : WellFormedB T = true) {c p : String} + (h : parentIn T c = some p) : ancestorsIn T c = c :: ancestorsIn T p := by + have hr := wf_reachesRoot wf c + have hlen : T.length ≠ 0 := by + intro hzero + rw [hzero] at hr + simp [reachesRoot, h] at hr + obtain ⟨k, hk⟩ : ∃ k, T.length = k + 1 := by + cases hl : T.length with + | zero => exact absurd hl hlen + | succ k => exact ⟨k, rfl⟩ + have hrp : reachesRoot T k p = true := by + rw [hk] at hr + simpa [reachesRoot, h] using hr + calc ancestorsIn T c + = ancestorsInFuel T (k + 1) c := by rw [ancestorsIn, hk] + _ = c :: ancestorsInFuel T k p := by simp [ancestorsInFuel, h] + _ = c :: ancestorsInFuel T T.length p := by + rw [ancestorsInFuel_stable hrp (f := T.length) (by omega)] + _ = c :: ancestorsIn T p := rfl + +/-! ## Subsumption is a partial order -/ + +/-- Bool/Prop bridge used throughout: subsumption IS ancestor membership. -/ +theorem subsumesIn_iff_mem {T : Table} {p c : String} : + subsumesIn T p c = true ↔ p ∈ ancestorsIn T c := by + simp [subsumesIn] + +/-- A suffix at least as long as its host IS its host. -/ +private theorem suffix_eq_of_length_le {α} {l₁ l₂ : List α} (h : l₁ <:+ l₂) + (hlen : l₂.length ≤ l₁.length) : l₁ = l₂ := by + obtain ⟨t, ht⟩ := h + have hl := congrArg List.length ht + simp [List.length_append] at hl + have ht0 : t = [] := by + have : t.length = 0 := by omega + simpa using this + simpa [ht0] using ht + +/-- The workhorse: an ancestor's chain is a suffix of the descendant's. -/ +theorem mem_ancestorsIn_suffix {T : Table} (wf : WellFormedB T = true) {p c : String} + (h : p ∈ ancestorsIn T c) : ancestorsIn T p <:+ ancestorsIn T c := by + induction hn : (ancestorsIn T c).length using Nat.strongRecOn generalizing c with + | _ n ih => + by_cases hpc : p = c + · subst hpc; exact List.suffix_refl _ + · cases hpar : parentIn T c with + | none => + rw [ancestorsIn_root hpar] at h + simp at h + exact absurd h hpc + | some q => + rw [ancestorsIn_cons wf hpar] at h ⊢ + rcases List.mem_cons.mp h with heq | hq + · exact absurd heq hpc + · have hlt : (ancestorsIn T q).length < n := by + rw [← hn, ancestorsIn_cons wf hpar] + simp + exact (ih _ hlt hq rfl).trans (List.suffix_cons _ _) + +theorem subsumesIn_trans {T : Table} (wf : WellFormedB T = true) {a b c : String} + (h₁ : subsumesIn T a b = true) (h₂ : subsumesIn T b c = true) : + subsumesIn T a c = true := by + rw [subsumesIn_iff_mem] at h₁ h₂ ⊢ + exact (mem_ancestorsIn_suffix wf h₂).subset h₁ + +theorem subsumesIn_antisymm {T : Table} (wf : WellFormedB T = true) {p c : String} + (h₁ : subsumesIn T p c = true) (h₂ : subsumesIn T c p = true) : p = c := by + rw [subsumesIn_iff_mem] at h₁ h₂ + have s₁ := mem_ancestorsIn_suffix wf h₁ + have s₂ := mem_ancestorsIn_suffix wf h₂ + have heq : ancestorsIn T p = ancestorsIn T c := + suffix_eq_of_length_le s₁ s₂.length_le + have hp : (ancestorsIn T p).head? = some p := ancestorsInFuel_head T T.length p + have hc : (ancestorsIn T c).head? = some c := ancestorsInFuel_head T T.length c + rw [heq] at hp + rw [hp] at hc + injection hc + +theorem no_self_parent {T : Table} (wf : WellFormedB T = true) {p : String} : + parentIn T p ≠ some p := by + intro hp + have hfalse : ∀ f, reachesRoot T f p = false := by + intro f + induction f with + | zero => simp [reachesRoot, hp] + | succ k ih => simp [reachesRoot, hp, ih] + have := wf_reachesRoot wf p + rw [hfalse] at this + exact Bool.false_ne_true this + +theorem siblings_incomparable {T : Table} (wf : WellFormedB T = true) {p c q : String} + (hp : parentIn T p = some q) (hc : parentIn T c = some q) (hne : p ≠ c) : + subsumesIn T p c = false := by + cases hs : subsumesIn T p c with + | false => rfl + | true => + exfalso + rw [subsumesIn_iff_mem] at hs + rw [ancestorsIn_cons wf hc] at hs + rcases List.mem_cons.mp hs with heq | hq + · exact hne heq + · have h₁ : subsumesIn T p q = true := subsumesIn_iff_mem.mpr hq + have h₂ : subsumesIn T q p = true := by + rw [subsumesIn_iff_mem, ancestorsIn_cons wf hp] + exact List.mem_cons_of_mem _ (self_mem_ancestorsIn T q) + have hpq : p = q := subsumesIn_antisymm wf h₁ h₂ + subst hpq + exact no_self_parent wf hp + +theorem subsumesIn_of_absent {T : Table} {c p : String} (h : parentIn T c = none) : + subsumesIn T p c = true ↔ p = c := by + rw [subsumesIn_iff_mem, ancestorsIn_root h] + simp + +theorem parentIn_some_mem_names {T : Table} (wf : WellFormedB T = true) {x q : String} + (h : parentIn T x = some q) : q ∈ namesOf T := by + have h2 : parentClosedB T = true := by + unfold WellFormedB at wf + simp only [Bool.and_eq_true] at wf + exact wf.1.2 + unfold parentIn at h + cases hf : T.find? (fun (n, _) => n == x) with + | none => rw [hf] at h; exact absurd h (by simp) + | some row => + rw [hf] at h + obtain ⟨n, p?⟩ := row + simp only at h + have hrow := List.mem_of_find?_eq_some hf + have hcl := List.all_eq_true.mp h2 _ hrow + rw [h] at hcl + simp only at hcl + obtain ⟨⟨n', p?'⟩, hrow', hq⟩ := List.any_eq_true.mp hcl + simp only [beq_iff_eq] at hq + exact hq ▸ List.mem_map_of_mem hrow' + +theorem mem_ancestorsIn_names {T : Table} (wf : WellFormedB T = true) {a x : String} + (h : a ∈ ancestorsIn T x) : a = x ∨ a ∈ namesOf T := by + induction hn : (ancestorsIn T x).length using Nat.strongRecOn generalizing x with + | _ n ih => + cases hpar : parentIn T x with + | none => + rw [ancestorsIn_root hpar] at h + simp at h + exact Or.inl h + | some q => + rw [ancestorsIn_cons wf hpar] at h + rcases List.mem_cons.mp h with heq | hq + · exact Or.inl heq + · have hlt : (ancestorsIn T q).length < n := by + rw [← hn, ancestorsIn_cons wf hpar] + simp + rcases ih _ hlt hq rfl with heq' | hmem + · exact Or.inr (heq' ▸ parentIn_some_mem_names wf hpar) + · exact Or.inr hmem + +theorem absent_subsumesIn {T : Table} (wf : WellFormedB T = true) {c x : String} + (hc : c ∉ namesOf T) (h : subsumesIn T c x = true) : x = c := by + rw [subsumesIn_iff_mem] at h + rcases mem_ancestorsIn_names wf h with heq | hmem + · exact heq.symm + · exact absurd hmem hc + +/-! ## Coverage and normalization -/ + +theorem coveredIn_mono {T : Table} {L L' : List String} {c : String} + (hsub : ∀ x ∈ L, x ∈ L') (h : coveredIn T L c = true) : + coveredIn T L' c = true := by + simp only [coveredIn, List.any_eq_true] at h ⊢ + obtain ⟨need, hmem, hsubm⟩ := h + exact ⟨need, hsub need hmem, hsubm⟩ + +theorem coveredIn_of_subsumes {T : Table} {p c : String} + (h : subsumesIn T p c = true) : coveredIn T [p] c = true := by + simp [coveredIn, h] + +theorem normalizeIn_subset (T : Table) (L : List String) : + ∀ x ∈ normalizeIn T L, x ∈ L := by + intro x hx + exact (List.mem_filter.mp hx).1 + +/-- A PROPER ancestor's chain is strictly shorter — the measure the +`exists_survivor` descent recurses on. -/ +theorem ancestors_length_lt {T : Table} (wf : WellFormedB T = true) {p c : String} + (hmem : p ∈ ancestorsIn T c) (hne : p ≠ c) : + (ancestorsIn T p).length < (ancestorsIn T c).length := by + have hsuf := mem_ancestorsIn_suffix wf hmem + rcases Nat.lt_or_ge (ancestorsIn T p).length (ancestorsIn T c).length with hlt | hge + · exact hlt + · exfalso + have heq := suffix_eq_of_length_le hsuf hge + have hp : (ancestorsIn T p).head? = some p := ancestorsInFuel_head T T.length p + have hc : (ancestorsIn T c).head? = some c := ancestorsInFuel_head T T.length c + rw [heq] at hp + rw [hp] at hc + exact hne (by injection hc) + +/-- Every dropped cap is covered by a survivor: the strict-descent argument +through the "subsumed by" order, terminating because ancestor chains +strictly shorten. -/ +theorem exists_survivor {T : Table} (wf : WellFormedB T = true) {L : List String} + {need : String} (hmem : need ∈ L) : + ∃ m, m ∈ normalizeIn T L ∧ subsumesIn T m need = true := by + induction hn : (ancestorsIn T need).length using Nat.strongRecOn generalizing need with + | _ n ih => + by_cases hkeep : need ∈ normalizeIn T L + · exact ⟨need, hkeep, subsumesIn_refl T need⟩ + · have hdrop : ∃ other, other ∈ L ∧ other ≠ need ∧ subsumesIn T other need = true := by + rw [normalizeIn] at hkeep + cases hany : L.any (fun other => other != need && subsumesIn T other need) with + | true => + obtain ⟨other, homem, hcond⟩ := List.any_eq_true.mp hany + simp only [Bool.and_eq_true, bne_iff_ne, ne_eq] at hcond + exact ⟨other, homem, hcond.1, hcond.2⟩ + | false => + exact absurd (List.mem_filter.mpr ⟨hmem, by simp [hany]⟩) hkeep + obtain ⟨other, homem, hone, hosub⟩ := hdrop + have homem' : other ∈ ancestorsIn T need := subsumesIn_iff_mem.mp hosub + have hlt : (ancestorsIn T other).length < n := + hn ▸ ancestors_length_lt wf homem' hone + obtain ⟨m, hmkeep, hmsub⟩ := ih _ hlt homem rfl + exact ⟨m, hmkeep, subsumesIn_trans wf hmsub hosub⟩ + +/-- `normalize` never changes what is covered — THE lemma that licenses +applying it to a `needs` list at all (P2 consumes this; it fails without +antisymmetry, i.e. on a cyclic table). -/ +theorem coveredIn_normalizeIn {T : Table} (wf : WellFormedB T = true) + (L : List String) (c : String) : + coveredIn T (normalizeIn T L) c = coveredIn T L c := by + cases hL : coveredIn T L c with + | true => + simp only [coveredIn, List.any_eq_true] at hL ⊢ + obtain ⟨need, hmem, hsubm⟩ := hL + obtain ⟨m, hmkeep, hmsub⟩ := exists_survivor wf hmem + exact ⟨m, hmkeep, subsumesIn_trans wf hmsub hsubm⟩ + | false => + cases hN : coveredIn T (normalizeIn T L) c with + | false => rfl + | true => + rw [coveredIn_mono (normalizeIn_subset T L) hN] at hL + exact hL + +/-- `normalize` is a fixpoint after one application (no well-formedness +needed: it follows from survivors being a subset). -/ +theorem normalizeIn_idem (T : Table) (L : List String) : + normalizeIn T (normalizeIn T L) = normalizeIn T L := by + apply List.filter_eq_self.mpr + intro s hs + have hs' := hs + rw [normalizeIn, List.mem_filter] at hs' + obtain ⟨hsL, hpred⟩ := hs' + simp only [Bool.not_eq_eq_eq_not, Bool.not_true, List.any_eq_false] at hpred ⊢ + intro other homem + exact hpred other (normalizeIn_subset T L other homem) + +end MarchLean.Calculus diff --git a/MarchLean/Calculus/Verdicts.lean b/MarchLean/Calculus/Verdicts.lean new file mode 100644 index 0000000..da80c4b --- /dev/null +++ b/MarchLean/Calculus/Verdicts.lean @@ -0,0 +1,114 @@ +import MarchLean.CapCheck + +/-! +# Verdict algebra + +Kernel-checked laws for the two verdict-combination operators the capability +checker folds with: `CapResult.andThen` (`CapCheck.lean`) and +`DivVerdict.join`. What is proved and what is deliberately NOT: + +- `andThen` is associative with identity `ok`; `violation` left-absorbs. It + is NOT commutative — messages are leftmost-wins by design — but the tier + projection (`tierOf`) IS: `tierOf` is a homomorphism onto `Tier.max`, so + which verdict *tier* a fold produces never depends on fold order, only + which *message*. P2's order-independence theorem builds on exactly this. +-/ + +namespace MarchLean.Calculus +open MarchLean.CapCheck + +/-- Verdict severity, forgetting messages: `ok < skip < violation`. -/ +inductive Tier where + | ok | skip | violation + deriving DecidableEq, Repr + +/-- Max in the severity order (violation absorbs, ok is identity). -/ +def Tier.max : Tier → Tier → Tier + | .violation, _ => .violation + | _, .violation => .violation + | .skip, _ => .skip + | _, .skip => .skip + | .ok, .ok => .ok + +/-- The tier of a verdict (forget the message). -/ +def tierOf : CapResult → Tier + | .ok => .ok + | .skip _ => .skip + | .violation _ => .violation + +theorem ok_andThen (r : CapResult) : CapResult.ok.andThen r = r := by + cases r <;> rfl +theorem andThen_ok (r : CapResult) : r.andThen .ok = r := by + cases r <;> rfl +theorem violation_andThen (m : String) (r : CapResult) : + (CapResult.violation m).andThen r = .violation m := rfl +theorem andThen_assoc (a b c : CapResult) : + (a.andThen b).andThen c = a.andThen (b.andThen c) := by + cases a <;> cases b <;> cases c <;> rfl + +theorem Tier.max_comm (a b : Tier) : a.max b = b.max a := by + cases a <;> cases b <;> rfl +theorem Tier.max_assoc (a b c : Tier) : (a.max b).max c = a.max (b.max c) := by + cases a <;> cases b <;> cases c <;> rfl +theorem Tier.max_idem (a : Tier) : a.max a = a := by + cases a <;> rfl +theorem Tier.ok_max (a : Tier) : Tier.ok.max a = a := by + cases a <;> rfl +theorem Tier.max_ok (a : Tier) : a.max .ok = a := by + cases a <;> rfl + +/-- `tierOf` is a monoid homomorphism `(CapResult, andThen, ok) → (Tier, max, ok)`. -/ +theorem tierOf_andThen (a b : CapResult) : + tierOf (a.andThen b) = (tierOf a).max (tierOf b) := by + cases a <;> cases b <;> rfl + +/-- Tiers are fold-order-independent even though messages are not. -/ +theorem tierOf_andThen_comm (a b : CapResult) : + tierOf (a.andThen b) = tierOf (b.andThen a) := by + rw [tierOf_andThen, tierOf_andThen, Tier.max_comm] + +/-! ## `DivVerdict.join`: a bounded join-semilattice + +`safe` is the identity, `divZero` absorbs, and the operator is commutative, +associative, and idempotent — so `joinAll` over a body's division sites is a +pure set operation: `joinAll_perm` below shows traversal order can never +change a division verdict. -/ + +theorem join_comm (a b : DivVerdict) : a.join b = b.join a := by + cases a <;> cases b <;> rfl +theorem join_assoc (a b c : DivVerdict) : (a.join b).join c = a.join (b.join c) := by + cases a <;> cases b <;> cases c <;> rfl +theorem join_idem (a : DivVerdict) : a.join a = a := by + cases a <;> rfl +theorem safe_join (a : DivVerdict) : DivVerdict.safe.join a = a := by + cases a <;> rfl +theorem join_safe (a : DivVerdict) : a.join .safe = a := by + cases a <;> rfl +theorem divZero_join (a : DivVerdict) : DivVerdict.divZero.join a = .divZero := rfl + +/-- Fold with any accumulator = accumulator joined onto the fold from `safe`. +The bridge that lets `joinAll` be reasoned about pointwise. -/ +theorem foldl_join_shift (l : List DivVerdict) (a : DivVerdict) : + l.foldl DivVerdict.join a = a.join (DivVerdict.joinAll l) := by + induction l generalizing a with + | nil => simp [DivVerdict.joinAll, List.foldl_nil, join_safe] + | cons x xs ih => + simp only [DivVerdict.joinAll, List.foldl_cons] + rw [ih (a.join x), ih (DivVerdict.safe.join x), safe_join, join_assoc] + +/-- `joinAll` is permutation-invariant: division-site verdict joins do not +depend on traversal order. P2's order-independence theorem consumes this. -/ +theorem joinAll_perm {l₁ l₂ : List DivVerdict} (h : l₁.Perm l₂) : + DivVerdict.joinAll l₁ = DivVerdict.joinAll l₂ := by + induction h with + | nil => rfl + | cons x _ ih => + simp only [DivVerdict.joinAll, List.foldl_cons] + rw [foldl_join_shift, foldl_join_shift, ih] + | swap x y l => + simp only [DivVerdict.joinAll, List.foldl_cons] + congr 1 + cases x <;> cases y <;> rfl + | trans _ _ ih₁ ih₂ => exact ih₁.trans ih₂ + +end MarchLean.Calculus diff --git a/MarchLean/Calculus/Walks.lean b/MarchLean/Calculus/Walks.lean new file mode 100644 index 0000000..7e00ede --- /dev/null +++ b/MarchLean/Calculus/Walks.lean @@ -0,0 +1,156 @@ +import MarchLean.Syntax + +/-! +# The de-partialized walks are the folds they replaced + +`Syntax.lean`'s tree walks were `partial def`s recursing through +`List.any`/`List.all`. Each is now a `mutual` block pairing the walk with an +explicit `List` helper, which makes the descent structural — the kernel can +unfold and induct on them, so the tests over them moved from `native_decide` +to `decide` and theorems about them became possible at all. + +That refactor needs an argument that behavior did not change. The obvious one +is to keep the old body around and pin `legacy x = new x` on fixtures. This +file does better: each helper is **proved equal to the exact fold it +replaced**, by induction, for every input — not just the ones a corpus +happens to contain. A fixture pin can only ever say "the two agree on what we +thought to try"; these say "the two are the same function". + +Each theorem below is literally the diff of the refactor, stated as an +equation. If a future edit to one of these walks drifts from its fold, the +corresponding theorem stops compiling. +-/ + +namespace MarchLean.Calculus.Walks + +open MarchLean.Syntax + +/-! ## `Ty` -/ + +theorem ty_anyHasUnsupported_eq (ts : List Ty) : + Ty.anyHasUnsupported ts = ts.any Ty.hasUnsupported := by + induction ts with + | nil => rfl + | cons t ts ih => simp [Ty.anyHasUnsupported, List.any_cons, ih] + +theorem ty_anyFieldHasUnsupported_eq (fs : List (String × Ty)) : + Ty.anyFieldHasUnsupported fs = fs.any (fun (_, t) => Ty.hasUnsupported t) := by + induction fs with + | nil => rfl + | cons f fs ih => + obtain ⟨n, t⟩ := f + simp [Ty.anyFieldHasUnsupported, List.any_cons, ih] + +/-- `beqList` is the old `length == length && (zip …).all …`. The length +check is not lost: it is exactly the two `_, _` fall-through arms. -/ +theorem ty_beqList_eq (xs ys : List Ty) : + Ty.beqList xs ys + = (xs.length == ys.length && (xs.zip ys).all (fun (a, b) => Ty.beq a b)) := by + induction xs generalizing ys with + | nil => cases ys <;> simp [Ty.beqList] + | cons x xs ih => + cases ys with + | nil => simp [Ty.beqList] + | cons y ys => + simp only [Ty.beqList, ih, List.length_cons, List.zip_cons_cons, + List.all_cons, beq_iff_eq, Nat.add_right_cancel_iff] + cases Ty.beq x y <;> simp + +/-! ## `Pattern` -/ + +theorem pattern_anyHasUnsupported_eq (ps : List Pattern) : + Pattern.anyHasUnsupported ps = ps.any Pattern.hasUnsupported := by + induction ps with + | nil => rfl + | cons p ps ih => simp [Pattern.anyHasUnsupported, List.any_cons, ih] + +theorem pattern_anyFieldHasUnsupported_eq (fs : List (String × Pattern)) : + Pattern.anyFieldHasUnsupported fs + = fs.any (fun (_, p) => Pattern.hasUnsupported p) := by + induction fs with + | nil => rfl + | cons f fs ih => + obtain ⟨n, p⟩ := f + simp [Pattern.anyFieldHasUnsupported, List.any_cons, ih] + +/-! ## `Term` -/ + +theorem term_anyHasUnsupported_eq (es : List Term) : + Term.anyHasUnsupported es = es.any Term.hasUnsupported := by + induction es with + | nil => rfl + | cons e es ih => simp [Term.anyHasUnsupported, List.any_cons, ih] + +theorem term_anyFieldHasUnsupported_eq (fs : List (String × Term)) : + Term.anyFieldHasUnsupported fs = fs.any (fun (_, e) => Term.hasUnsupported e) := by + induction fs with + | nil => rfl + | cons f fs ih => + obtain ⟨n, e⟩ := f + simp [Term.anyFieldHasUnsupported, List.any_cons, ih] + +theorem term_optHasUnsupported_eq (g : Option Term) : + Term.optHasUnsupported g = (g.map Term.hasUnsupported).getD false := by + cases g <;> rfl + +/-- The match-arm fold, including the pattern component. Dropping that +component was a real false-accept bug once (`Syntax.lean`'s regression +tests); this states the arm walk in full so the shape is checked, not +remembered. -/ +theorem term_anyArmHasUnsupported_eq (arms : List (Pattern × Option Term × Term)) : + Term.anyArmHasUnsupported arms + = arms.any (fun (p, g, e) => + Pattern.hasUnsupported p + || (g.map Term.hasUnsupported).getD false + || Term.hasUnsupported e) := by + induction arms with + | nil => rfl + | cons a arms ih => + obtain ⟨p, g, e⟩ := a + simp [Term.anyArmHasUnsupported, List.any_cons, ih, + term_optHasUnsupported_eq, Bool.or_assoc] + +theorem anyParamAnnotUnsupported_eq (ps : List (String × Lin × Option Ty)) : + anyParamAnnotUnsupported ps = ps.any (fun (_, _, a) => optTyHasUnsupported a) := by + induction ps with + | nil => rfl + | cons p ps ih => + obtain ⟨n, l, a⟩ := p + simp [anyParamAnnotUnsupported, List.any_cons, ih] + +/-! ## `Decl` -/ + +theorem decl_anyHasUnsupported_eq (ds : List Decl) : + Decl.anyHasUnsupported ds = ds.any Decl.hasUnsupported := by + induction ds with + | nil => rfl + | cons d ds ih => simp [Decl.anyHasUnsupported, List.any_cons, ih] + +theorem decl_anyCtorHasUnsupported_eq (cs : List CtorSig) : + Decl.anyCtorHasUnsupported cs + = cs.any (fun c => c.argTys.any Ty.hasUnsupported || Ty.hasUnsupported c.resultTy) := by + induction cs with + | nil => rfl + | cons c cs ih => + simp [Decl.anyCtorHasUnsupported, List.any_cons, ih, ty_anyHasUnsupported_eq] + +/-! ## A property the old definitions could not even state + +With the walks structural, `Ty.hasUnsupported` supports genuine induction. +This is the kind of thing P2's whole-checker theorems will need. -/ + +theorem ty_anyHasUnsupported_append (xs ys : List Ty) : + Ty.anyHasUnsupported (xs ++ ys) + = (Ty.anyHasUnsupported xs || Ty.anyHasUnsupported ys) := by + induction xs with + | nil => simp [Ty.anyHasUnsupported] + | cons x xs ih => simp [Ty.anyHasUnsupported, ih, Bool.or_assoc] + +theorem decl_anyHasUnsupported_append (xs ys : List Decl) : + Decl.anyHasUnsupported (xs ++ ys) + = (Decl.anyHasUnsupported xs || Decl.anyHasUnsupported ys) := by + induction xs with + | nil => simp [Decl.anyHasUnsupported] + | cons x xs ih => simp [Decl.anyHasUnsupported, ih, Bool.or_assoc] + +end MarchLean.Calculus.Walks diff --git a/MarchLean/CapCheck.lean b/MarchLean/CapCheck.lean index 2b43e01..22cd6d2 100644 --- a/MarchLean/CapCheck.lean +++ b/MarchLean/CapCheck.lean @@ -121,14 +121,40 @@ partial def capsInTy : Ty → List String | .lin _ t => capsInTy t | _ => [] -/-- The caps a declaration's PARAMETER signature mentions. Only signatures -matter for Check 1 — body uses are Check 1b, which is warning-only and not -implemented. Return-type caps are handled separately by -`capsInReturnSignature` (they are gated differently — see `checkOneModule`). -/ +/-- The caps a declaration's PARAMETER signature mentions, plus the caps named +inside a TYPE DECLARATION's constructor arguments. Return-type caps are handled +separately by `capsInReturnSignature` (they are gated differently — see +`checkOneModule`). + +**Type declarations.** march's `check_module_needs` builds one `cap_uses` list +over every decl form, and `DType`/`DAlwaysLinearType` contribute +`Cap_surface_ty.caps_in_type_def td` to it (`typecheck.ml:8813-8814`) — a +capability named in a variant constructor argument is a *use* of that +capability, treated exactly like one in a function signature. march's own +comment records that these arms were previously swallowed by a `| _ -> []` +wildcard, so `type Handle = { tok : Cap(IO.FileWrite) }` under `needs +IO.Console` typechecked clean; `reject/t148`-`t150` are the regression tests. +This checker had the same hole and it was a live FALSE ACCEPT on +`reject/t149_cap_variant_arg_undeclared` and +`reject/t144_cap_derive_json_variant_arg`. + +Scanned UNGATED, like parameters and unlike return annotations: the cap is +named concretely in the constructor's argument type, so there is no +unmodeled-machinery escape hatch of the kind `capsInReturnSignature`'s gate +exists to respect. + +Only `argTys` are scanned, matching `caps_in_type_def`'s `TDVariant` arm +(`List.concat_map caps_in_ty v.var_args`) — a constructor's `resultTy` is +this checker's own synthesized `Ty.con name [params]`, not surface syntax the +author wrote, and march has no counterpart to it. `TDRecord` and `TDAlias` +decode to `Decl.unsupported` (`Elab.lean`'s `DType` arm), so those two of +`caps_in_type_def`'s three arms are reached as whole-file skips rather than +here — honest, and why `reject/t148`/`t150` skip instead of matching. -/ def capsInSignature : Decl → List String | .dfn _ params _ _ => params.flatMap (fun (_, _, annot) => match annot with | some t => capsInTy t | none => []) + | .dtype _ _ ctors => ctors.flatMap (fun c => c.argTys.flatMap capsInTy) | _ => [] /-- The caps a declaration's RETURN-type annotation mentions. march's Check 1 @@ -146,6 +172,165 @@ def capsInReturnSignature : Decl → List String match retAnnot with | some t => capsInTy t | none => [] | _ => [] +/-- Every capability named by a type ANNOTATION inside an expression: a `let` +binding's annotation, and a lambda's or local function's parameter +annotations. Mirrors march's `cap_annots_in_expr` (`typecheck.ml:8109-8180`). + +**Why bodies at all.** Check 1 historically read function SIGNATURES only, so +a capability named inside a body escaped `needs` entirely. march's own note +records the route that made it reachable: `root_cap` was ambient, so a module +declaring only `IO.Console` could narrow the root to `Cap(IO.FileWrite)` and +bind it without ever putting a capability in a signature. R2 (see +`checkOneModule`'s root-cap gate) closed that particular route, but not the +hole — a LAMBDA PARAMETER annotation needs no capability VALUE at all, only +the type name, so it survives R2 untouched. That is +`reject/t151_cap_body_annotation_undeclared`, and it was a false ACCEPT here. + +**Total over every `Term` constructor, with no wildcard arm**, matching +`bodyCalls`/`bodyAllocates`/`termMentionsAny`'s discipline in this file and +march's own stated rule for its capability walks: a walk that ends in a +catch-all is a silent hole rather than a visible bug, and adding a `Term` +form must break this build instead of quietly reopening the gap. + +march also walks an `EAnnot` type; march's own comment says the parser never +produces one (desugar synthesizes the single instance, a `SupervisorSpec` on +an `app` block) and there is no reject-witness for it. This `Term` has no +`EAnnot` counterpart at all, so there is nothing to mirror. `Term.letfn` +likewise carries no return annotation, so march's `ELetFn` return arm has no +counterpart here; a local function's return cap is unreachable in this +fragment. -/ +partial def capAnnotsInTerm : Term → List String + | .lit _ _ => [] + | .var _ _ _ => [] + | .app fn args _ => capAnnotsInTerm fn ++ args.flatMap capAnnotsInTerm + | .lam params body _ => + params.flatMap (fun (_, _, annot) => + match annot with | some t => capsInTy t | none => []) ++ capAnnotsInTerm body + | .let_ _ _ annot rhs body _ => + (match annot with | some t => capsInTy t | none => []) ++ + capAnnotsInTerm rhs ++ capAnnotsInTerm body + | .letfn _ _ _ paramAnnot fnBody body _ => + (match paramAnnot with | some t => capsInTy t | none => []) ++ + capAnnotsInTerm fnBody ++ capAnnotsInTerm body + | .ite c t e _ => capAnnotsInTerm c ++ capAnnotsInTerm t ++ capAnnotsInTerm e + | .con _ args _ => args.flatMap capAnnotsInTerm + | .tuple elems _ => elems.flatMap capAnnotsInTerm + | .record fields _ => fields.flatMap (fun (_, e) => capAnnotsInTerm e) + | .field record _ _ _ => capAnnotsInTerm record + | .match_ scrut arms _ => + capAnnotsInTerm scrut ++ + arms.flatMap (fun (_, g, e) => + (g.map capAnnotsInTerm).getD [] ++ capAnnotsInTerm e) + -- `.opaque_` RECURSES, matching every other collector here (`bodyCalls`, + -- `bodyAllocates`, `matchesIn`). `Elab` decodes the nine unmodelled-but- + -- child-carrying march kinds to `opaque_` precisely so their children + -- survive to the cap layer; a `Cap(X)` annotation on a lambda parameter + -- inside, say, an `ECond` arm is exactly as much a `needs` use as one + -- anywhere else. + | .opaque_ children _ => children.flatMap capAnnotsInTerm + | .unsupported _ => [] + +/-- The concrete IO-lattice capability a type denotes, if it is exactly +`Cap(P)` for a nullary `P` that is a NAME IN THE HIERARCHY. Mirrors march's +local `concrete` inside `check_cap_narrow_sites` (`typecheck.ml:9407-9411`), +with one deliberate narrowing: march excludes proof caps explicitly +(`is_proof`), while this additionally requires lattice membership. + +Requiring membership subsumes march's proof-cap exclusion (a proof cap like +`Db.Migrated` is not in the hierarchy) and also excludes FFI caps, which are +their own roots and subsume nothing but themselves — so a `cap_narrow` +between two FFI names would otherwise be flagged. The difference can only +make this checker MORE permissive than march, never less, so it cannot +manufacture a false reject; it is the safe direction for a check whose whole +job is replacing a guarantee that used to live in the type. -/ +def concreteLatticeCap : Ty → Option String + | .con "Cap" [.con p []] => + if MarchLean.CapLattice.hierarchy.any (fun (n, _) => n == p) then some p else none + | _ => none + +/-- R4a: attenuation must move DOWN the lattice, or stay level. + +march's `cap_narrow` is now `∀a b. Cap(a) → Cap(b)` (see `Infer.builtins`), +so the TYPE no longer stops a widen — `check_cap_narrow_sites` +(`typecheck.ml:9406-9432`) does, as a deferred sweep over solved types. This +is the mirror of that sweep, and it is load-bearing rather than defensive: +without it, retyping `cap_narrow` turns `reject/t153` (widen), `t154` +(siblings) and `t155` (widen visible only after later unification) into false +ACCEPTS. Those three currently reject only as a side effect of the old +argument type failing to unify, which is not a lattice check at all. + +The rule, exactly as march states it: an error iff BOTH sides resolve to +concrete lattice capabilities AND the source does not subsume the target. +Reflexivity is allowed — `capSubsumes p p` holds, which is what makes +`accept/t148`'s `same_level` (narrowing `Cap(IO.FileRead)` to itself) legal. +An UNPINNED side is silent: a result never pinned to a concrete capability is +a result never USED as one, so no authority is exercised and there is nothing +to widen into. Failing closed there would reject ordinary code that narrows +into a polymorphic position — march records having considered and rejected +that choice. + +Reading the two sides off the application node rather than off the callee's +instantiated arrow is equivalent here and more robust: the emitter's +`resolved_ty` is POST-solve, verified on `reject/t155`, whose `cap_narrow` +application resolves to `Cap(IO.FileWrite)` with argument `Cap(IO.Console)` — +precisely the deferred widen. -/ +partial def capNarrowViolation : Term → Option (String × String) + | .app (.var "cap_narrow" _ _) [arg] ty => + match concreteLatticeCap arg.ty, concreteLatticeCap ty with + | some src, some dst => + if capSubsumes src dst then capNarrowViolation arg + else some (src, dst) + | _, _ => capNarrowViolation arg + | .app fn args _ => + match capNarrowViolation fn with + | some v => some v + | none => args.findSome? capNarrowViolation + | .lit _ _ => none + | .var _ _ _ => none + | .lam _ body _ => capNarrowViolation body + | .let_ _ _ _ rhs body _ => + match capNarrowViolation rhs with + | some v => some v + | none => capNarrowViolation body + | .letfn _ _ _ _ fnBody body _ => + match capNarrowViolation fnBody with + | some v => some v + | none => capNarrowViolation body + | .ite c t e _ => + match capNarrowViolation c with + | some v => some v + | none => match capNarrowViolation t with + | some v => some v + | none => capNarrowViolation e + | .con _ args _ => args.findSome? capNarrowViolation + | .tuple elems _ => elems.findSome? capNarrowViolation + | .record fields _ => fields.findSome? (fun (_, e) => capNarrowViolation e) + | .field record _ _ _ => capNarrowViolation record + | .match_ scrut arms _ => + match capNarrowViolation scrut with + | some v => some v + | none => arms.findSome? (fun (_, g, e) => + match (g.bind capNarrowViolation) with + | some v => some v + | none => capNarrowViolation e) + -- `.opaque_` RECURSES, same rationale as `capAnnotsInTerm` above: a widening + -- `cap_narrow` buried in an unmodelled-but-child-carrying node is still a + -- widening, and its two sides are still concretely resolved. + | .opaque_ children _ => children.findSome? capNarrowViolation + | .unsupported _ => none + +/-- The first R4a widening in a declaration's body, if any. -/ +def declCapNarrowViolation : Decl → Option (String × String) + | .dfn _ _ _ body => capNarrowViolation body + | .dlet _ rhs => capNarrowViolation rhs + | _ => none + +/-- The caps named by type annotations inside a declaration's body. -/ +def capsInBody : Decl → List String + | .dfn _ _ _ body => capAnnotsInTerm body + | .dlet _ rhs => capAnnotsInTerm rhs + | _ => [] + /-- The caps this module declares via `needs`. -/ def declaredNeeds (decls : List Decl) : List String := decls.flatMap (fun d => match d with | .dneeds ps => ps | _ => []) @@ -1498,7 +1683,49 @@ def checkOneModule (modName : String) (decls : List Decl) -- unconditional so no existing signature-based reject changes. let retCaps := if decls.any Decl.hasUnsupported then [] else decls.flatMap capsInReturnSignature - let sigCaps := decls.flatMap capsInSignature ++ retCaps + -- Body-annotation caps (march's `cap_annots_in_expr`, folded into the same + -- `cap_uses` list Check 1 consumes). Ungated, like parameters: the cap is + -- named concretely by an annotation the author wrote, so the + -- unmodeled-machinery escape `retCaps`'s gate respects does not apply. + let bodyCapUses := decls.flatMap capsInBody + let sigCaps := decls.flatMap capsInSignature ++ retCaps ++ bodyCapUses + -- R2 (march main): `root_cap` cannot be REFERENCED. It remains bound, at + -- type `Cap(IO)` (`Infer.lean` keeps it, exactly as march keeps the name + -- bound at `typecheck.ml:5118-5125` so a single mistake reports one + -- capability error rather than cascading unification failures) — only + -- naming it is refused, because the root is granted to `main` at the + -- boundary rather than taken from an ambient global. + -- + -- march exempts four contexts via `env.root_cap_allowed`: a `DTest` body + -- (`:11741`), `DSetup` (`:11756`), `DSetupAll` (`:11765`), and the REPL + -- entry (`:12795`). **All four decode to `Decl.unsupported` here** (see + -- `Elab.decodeDecl`), so rather than model the flag this gates on the + -- module being entirely in fragment — the same residual gate `retCaps` + -- uses above, and for the same reason. `accept/t146_root_cap_in_test_body` + -- narrows `root_cap` inside `describe`/`test` and is exactly the file this + -- gate protects: cap checks run BEFORE the skip gate (A3 design §4), so + -- without it that file would be a false REJECT instead of a skip. + -- + -- `accept/t147_main_receives_the_root` is unaffected either way: it takes + -- `cap : Cap(IO)` as a parameter and never names `root_cap`. + let fullyInFragment := !decls.any Decl.hasUnsupported + let mentionsRootCap := decls.any (fun d => + match d with + | .dfn _ _ _ body => termMentionsAny ["root_cap"] body + | .dlet _ rhs => termMentionsAny ["root_cap"] rhs + | _ => false) + if fullyInFragment && mentionsRootCap then + .violation s!"R2: `root_cap` cannot be referenced in module `{modName}` — the root capability is granted to `main`, not taken" + else + -- R4a — `cap_narrow` only attenuates. See `capNarrowViolation`: this is + -- what replaces the subsumption the old `Cap(IO)→Cap(a)` argument type used + -- to enforce through unification. Ungated: both sides must already have + -- resolved to concrete lattice capabilities for it to fire at all, so an + -- out-of-fragment neighbour cannot make it misfire. + match decls.findSome? declCapNarrowViolation with + | some (src, dst) => + .violation s!"R4a: `Cap({src})` cannot be widened to `Cap({dst})` in module `{modName}` — `cap_narrow` only attenuates, so the source capability must subsume the target" + | none => -- Finding I1: a cap in `selfDeclaredCaps` is covered regardless of -- `needs` — march's self-declaration exemption (`typecheck.ml:6966-6970`) -- lets a proof cap's own declaring module use it in its own signatures @@ -1971,6 +2198,184 @@ def siblingViolation : Module := { #eval checkCaps siblingViolation -- expect: violation — IO.FileWrite not covered by IO.FileRead +/-! ### R4a — `cap_narrow` only attenuates + +These four pin the guarantee that MOVED when `cap_narrow` was retyped to +`∀a b. Cap(a) → Cap(b)`. Before R4a the argument type enforced it through +unification and `reject/t153`/`t154`/`t155` rejected as a side effect; +`capNarrowViolation` is now the only thing standing between those files and a +false ACCEPT, so it is pinned here as well as in the corpus. -/ + +private def capNarrowApp (src dst : String) : Term := + Term.app (Term.var "cap_narrow" ⟨"f",0,0,0,0⟩ + (Ty.arrow (Ty.con "Cap" [Ty.con src []]) (Ty.con "Cap" [Ty.con dst []]))) + [Term.var "c" ⟨"f",0,0,0,0⟩ (Ty.con "Cap" [Ty.con src []])] + (Ty.con "Cap" [Ty.con dst []]) + +/-- `needs` lists both endpoints, so Check 1 is satisfied by construction and +whatever these fixtures report comes from R4a alone. -/ +private def capNarrowModule (src dst : String) : Module := { + decls := [Decl.dmod "N" [ + Decl.dneeds ["IO", src, dst], + Decl.dfn "f" [("c", Lin.unrestricted, some (Ty.con "Cap" [Ty.con src []]))] + (some (Ty.con "Cap" [Ty.con dst []])) (capNarrowApp src dst)]], + schemes := [], insts := [], moduleCaps := [] } + +-- reject/t153: widening `Cap(IO.Console)` to `Cap(IO.FileWrite)`. +#eval checkCaps (capNarrowModule "IO.Console" "IO.FileWrite") + -- expect: violation — R4a + +-- reject/t154: siblings — `Cap(IO.FileRead)` to `Cap(IO.FileWrite)`. +#eval checkCaps (capNarrowModule "IO.FileRead" "IO.FileWrite") + -- expect: violation — R4a + +-- accept/t148, the attenuating hop: `Cap(IO.FileSystem)` to +-- `Cap(IO.FileRead)` moves DOWN the lattice and is legal. +#eval checkCaps (capNarrowModule "IO.FileSystem" "IO.FileRead") + -- expect: ok + +-- accept/t148's `same_level`: narrowing to the SAME capability is legal, +-- because `capSubsumes p p` holds. A strict-ancestor test would wrongly +-- reject this — which is exactly what that file exists to catch. +#eval checkCaps (capNarrowModule "IO.FileRead" "IO.FileRead") + -- expect: ok + +-- A PROOF cap is not in the IO lattice, so R4a stays silent rather than +-- flagging a narrow it has no authority to judge (march exempts these +-- explicitly via `is_proof`; `concreteLatticeCap` reaches the same +-- conclusion by requiring hierarchy membership). `needs` covers the proof +-- cap here so this isolates R4a from Check 1 — without that, the violation +-- reported is Check 1's uncovered `Cap(Db.Migrated)`, not R4a at all. +#eval checkCaps (capNarrowModule "IO" "Db.Migrated") + -- expect: ok — R4a declines to judge a non-lattice cap + +/-- reject/t151: a LAMBDA PARAMETER annotation names `Cap(IO.FileWrite)` +inside a body, under `needs IO.Console`. Needs no capability value at all — +only the type name — so it survives R2 and is the sharpest witness that +Check 1 must reach inside bodies. -/ +def bodyLamAnnotUncovered : Module := { + decls := [Decl.dmod "BodyAnnCap" [ + Decl.dneeds ["IO.Console"], + Decl.dfn "main" [] none + (Term.let_ "take" Lin.unrestricted none + (Term.lam [("c", Lin.unrestricted, some (Ty.con "Cap" [Ty.con "IO.FileWrite" []]))] + (Term.lit (Lit.int 1) (Ty.con "Int" [])) + (Ty.con "Unit" [])) + (Term.lit Lit.unit (Ty.con "Unit" [])) + (Ty.con "Unit" []))]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps bodyLamAnnotUncovered + -- expect: violation — IO.FileWrite not covered by IO.Console + +/-- accept/t145's shape: the same body annotation, DECLARED. Guards the body +walk against over-rejecting a covered `let` annotation. -/ +def bodyLetAnnotCovered : Module := { + decls := [Decl.dmod "BodyAnnCap" [ + Decl.dneeds ["IO.FileWrite"], + Decl.dfn "main" [] none + (Term.let_ "w" Lin.unrestricted (some (Ty.con "Cap" [Ty.con "IO.FileWrite" []])) + (Term.lit Lit.unit (Ty.con "Unit" [])) + (Term.lit Lit.unit (Ty.con "Unit" [])) + (Ty.con "Unit" []))]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps bodyLetAnnotCovered + -- expect: ok + +/-- The body walk reaches through nesting, not just the outermost node — +a cap annotation buried in a match arm inside a tuple still counts. -/ +def bodyAnnotNestedUncovered : Module := { + decls := [Decl.dmod "Deep" [ + Decl.dneeds ["IO.Console"], + Decl.dfn "f" [] none + (Term.tuple [ + Term.match_ (Term.lit (Lit.int 0) (Ty.con "Int" [])) + [(Pattern.wild, none, + Term.lam [("c", Lin.unrestricted, some (Ty.con "Cap" [Ty.con "IO.Network" []]))] + (Term.lit (Lit.int 1) (Ty.con "Int" [])) + (Ty.con "Unit" []))] + (Ty.con "Unit" [])] + (Ty.con "Unit" []))]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps bodyAnnotNestedUncovered + -- expect: violation — IO.Network, found through tuple + match arm + lambda + +/-- reject/t152: naming `root_cap` in an ordinary function body is an R2 +violation, even in a module whose `needs` are fully declared. -/ +def rootCapReferenced : Module := { + decls := [Decl.dmod "TakesTheRoot" [ + Decl.dneeds ["IO"], + Decl.dfn "main" [] none + (Term.let_ "stolen" Lin.unrestricted none + (Term.var "root_cap" ⟨"f",0,0,0,0⟩ (Ty.con "Cap" [Ty.con "IO" []])) + (Term.lit Lit.unit (Ty.con "Unit" [])) + (Ty.con "Unit" []))]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps rootCapReferenced + -- expect: violation — R2 + +/-- accept/t147: `main` RECEIVES the root as a parameter and never names +`root_cap`. Guards the R2 check against rejecting the legitimate shape. -/ +def rootCapReceived : Module := { + decls := [Decl.dmod "GrantedRoot" [ + Decl.dneeds ["IO"], + Decl.dfn "main" [("cap", Lin.unrestricted, some (Ty.con "Cap" [Ty.con "IO" []]))] + none (Term.lit Lit.unit (Ty.con "Unit" []))]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps rootCapReceived + -- expect: ok + +/-- accept/t146's shape: `root_cap` IS nameable in a test body, which march +permits via `root_cap_allowed`. Here the enclosing `describe`/`test` decodes +to `Decl.unsupported`, so the fragment gate must defer rather than reject — +otherwise this is a false REJECT, since cap checks precede the skip gate. -/ +def rootCapInUnsupportedContext : Module := { + decls := [Decl.dmod "TestBodyCaps" [ + Decl.dneeds ["IO"], + Decl.unsupported, + Decl.dfn "helper" [] none + (Term.var "root_cap" ⟨"f",0,0,0,0⟩ (Ty.con "Cap" [Ty.con "IO" []]))]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps rootCapInUnsupportedContext + -- expect: NOT a violation (defers; the file skips downstream) + +/-- reject/t149: `Cap(IO.NetConnect)` in a VARIANT CONSTRUCTOR ARGUMENT under +`needs IO.Console`. march reports Check 1 here (`typecheck.ml:8813`); before +`capsInSignature` grew its `dtype` arm this was a false ACCEPT. -/ +def typeCtorArgUncovered : Module := { + decls := [Decl.dmod "VariantCap" [ + Decl.dneeds ["IO.Console"], + Decl.dtype "Conn" [] [ + { name := "Idle", argTys := [], resultTy := Ty.con "Conn" [] }, + { name := "Live", argTys := [Ty.con "Cap" [Ty.con "IO.NetConnect" []]], + resultTy := Ty.con "Conn" [] }]]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps typeCtorArgUncovered + -- expect: violation — IO.NetConnect not covered by IO.Console + +/-- accept/t144's shape: the same variant-argument cap, but DECLARED. Guards +against the `dtype` arm over-rejecting a covered type declaration. -/ +def typeCtorArgCovered : Module := { + decls := [Decl.dmod "VariantCap" [ + Decl.dneeds ["IO.NetConnect"], + Decl.dtype "Conn" [] [ + { name := "Live", argTys := [Ty.con "Cap" [Ty.con "IO.NetConnect" []]], + resultTy := Ty.con "Conn" [] }]]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps typeCtorArgCovered + -- expect: ok + +/-- A broader `needs` still covers a narrower cap in a constructor argument — +the `dtype` arm goes through the same subsumption as every other Check 1 use. -/ +def typeCtorArgCoveredByRoot : Module := { + decls := [Decl.dmod "VariantCap" [ + Decl.dneeds ["IO"], + Decl.dtype "Conn" [] [ + { name := "Live", argTys := [Ty.con "Cap" [Ty.con "IO.NetConnect" []]], + resultTy := Ty.con "Conn" [] }]]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps typeCtorArgCoveredByRoot + -- expect: ok + /-- accept/t46: the root `needs IO` covers `Cap(IO.Network)`. -/ def rootCovers : Module := { decls := [Decl.dmod "Server" [ diff --git a/MarchLean/CapLattice.lean b/MarchLean/CapLattice.lean index c5dd428..c71832a 100644 --- a/MarchLean/CapLattice.lean +++ b/MarchLean/CapLattice.lean @@ -1,3 +1,5 @@ +import MarchLean.Calculus.Lattice + /-! # The IO capability lattice @@ -10,12 +12,20 @@ three places and `lang/capabilities.md`'s tree omits two; both are stale. The entries the docs miss are `IO.Signal` and `IO.WebSocket`. Modelling 18 would give wrong subsumption for those two, so this port is taken from the OCaml source, not the prose. + +Since P0 (`specs/plans/2026-08-08-calculus-proof-capabilities-design.md`), +each operation here is the specialization of its abstract counterpart in +`MarchLean.Calculus.Lattice` to `hierarchy` — definitionally, so behavior is +unchanged. The metatheory (subsumption is a partial order, `normalize` is +idempotent and coverage-preserving, fuel `hierarchy.length` is adequate) is +proved there for any well-formed table; `MarchLean.Calculus.Concrete` +discharges `hierarchy`'s well-formedness by `decide`. -/ namespace MarchLean.CapLattice /-- The capability hierarchy: `(cap_path, parent_path)`. Mirrors `cap_lattice.ml`'s `hierarchy` list exactly, including order. -/ -def hierarchy : List (String × Option String) := +def hierarchy : MarchLean.Calculus.Table := [ ("IO", none), ("IO.Console", some "IO"), ("IO.FileSystem", some "IO"), @@ -39,9 +49,7 @@ def hierarchy : List (String × Option String) := /-- The parent of a capability, or `none` for a root or an unknown (FFI) name. -/ def capParent (c : String) : Option String := - match hierarchy.find? (fun (n, _) => n == c) with - | some (_, p) => p - | none => none + MarchLean.Calculus.parentIn hierarchy c /-- `capAncestors c` is `c` followed by every ancestor up to the root, most-specific first: `capAncestors "IO.FileRead" = ["IO.FileRead", @@ -53,29 +61,28 @@ like `LibC` are their own roots with no subtyping relationship to anything. `fuel` is the recursion bound. `hierarchy.length` is a safe bound because the table is a finite forest with no cycles, so no chain can exceed its size; the -parameter exists only to make the function structurally terminating. -/ -def capAncestorsFuel : Nat → String → List String - | 0, c => [c] - | fuel + 1, c => - match capParent c with - | some p => c :: capAncestorsFuel fuel p - | none => [c] +parameter exists only to make the function structurally terminating. Since P0 +this is no longer only a prose claim: `Calculus.ancestorsIn_fuel_adequate` +proves the bound adequate for any well-formed table, and +`Calculus.Concrete.hierarchy_wellFormed` discharges this table by `decide`. -/ +def capAncestorsFuel (fuel : Nat) (c : String) : List String := + MarchLean.Calculus.ancestorsInFuel hierarchy fuel c def capAncestors (c : String) : List String := - capAncestorsFuel hierarchy.length c + MarchLean.Calculus.ancestorsIn hierarchy c /-- `capSubsumes parent child` — is `parent` an ancestor of, or equal to, `child`? **Reflexive** (`capAncestors X` always starts with `X`) and **directional** (a broader declared cap covers a narrower used one, never the reverse). Two siblings never subsume each other. -/ def capSubsumes (parent child : String) : Bool := - (capAncestors child).contains parent + MarchLean.Calculus.subsumesIn hierarchy parent child /-- Drop any cap subsumed by another cap already present, preserving the relative order of the survivors: `normalize ["IO", "IO.FileRead"] = ["IO"]` regardless of the order they were given in. -/ def normalize (caps : List String) : List String := - caps.filter (fun c => !caps.any (fun other => other != c && capSubsumes other c)) + MarchLean.Calculus.normalizeIn hierarchy caps end MarchLean.CapLattice diff --git a/MarchLean/Infer.lean b/MarchLean/Infer.lean index cd1fbee..57676c5 100644 --- a/MarchLean/Infer.lean +++ b/MarchLean/Infer.lean @@ -905,10 +905,35 @@ def builtins (s : Supply) : InferM (List (String × EnvEntry)) := do -- Eq-constrained equality: ∀a:Eq. a→a→Bool for name in ["==", "!="] do out := (name, .scheme (← mkPoly1 s [Class.eq] (fun a => arr a (arr a b)))) :: out - -- Capability-narrowing: ∀a. Cap(IO)→Cap(a) (typecheck.ml:1972) + -- Capability-narrowing: ∀a b. Cap(a)→Cap(b) (march main, R4a). + -- + -- Was `∀a. Cap(IO)→Cap(a)`: the argument was LITERALLY the root, so a + -- holder of anything narrower could not attenuate at all. march's R4a + -- widened the type precisely to allow delegation-with-attenuation + -- (`accept/t148_cap_narrow_chains`), which this checker rejected with + -- "cannot unify IO with IO.FileSystem". + -- + -- **The subsumption guarantee moved, it did not disappear.** Before R4a + -- the argument type enforced it through unification; now nothing in the + -- TYPE does, and `CapCheck.capNarrowViolation` carries it instead — + -- mirroring march's own deferred `check_cap_narrow_sites` sweep + -- (`typecheck.ml:9406-9432`). Retyping here WITHOUT that sweep would turn + -- `reject/t153`/`t154`/`t155` into false accepts: those three reject today + -- only as a side effect of this unification failure, not because anything + -- checks the lattice. See `capNarrowViolation`'s docstring. let cap := fun (t : MTy) => MTy.con "Cap" [t] + -- Still needed by `root_cap` below: R2 keeps the NAME bound at `Cap(IO)` + -- (march does the same, `typecheck.ml:5118-5125`, so one mistake reports a + -- single capability error instead of cascading unification failures); + -- `CapCheck`'s R2 gate is what refuses references to it. let capIO := cap (MTy.con "IO" []) - out := ("cap_narrow", .scheme (← mkPoly1 s [] (fun a => arr capIO (cap a)))) :: out + let capA ← freshMVar s 0 [] + let capB ← freshMVar s 0 [] + let aid := match capA with | .mvar i => i | _ => 0 + let bid := match capB with | .mvar i => i | _ => 0 + out := ("cap_narrow", + .scheme { vars := [aid, bid], classes := [], + body := arr (cap capA) (cap capB) }) :: out -- `println : ∀a. a → ()` — UNCONSTRAINED, and deliberately NOT the -- `Mono (String → ())` that march's builtin table registers at -- `typecheck.ml:1951`. See the `println` note below for why march's own @@ -1054,6 +1079,14 @@ def inferModule' (s : Supply) (m : Module) : InferM (List (Span × MTy)) := do -- `fn f(x : Int) : Age do x end`), and a call to a correctly-typed -- function at the wrong return type. -- + -- It is ALSO load-bearing for R4a. `cap_narrow` is now + -- `∀a b. Cap(a) → Cap(b)` (see its entry in `builtins`), so in + -- `pfn same_level(r : Cap(IO.FileRead)) : Cap(IO.FileRead) do + -- cap_narrow(r) end` the result is pinned ONLY by this annotation. + -- Without this unification the body stays a metavariable, march + -- resolves it to `Cap(IO.FileRead)`, and the per-node cross-check + -- reports types_differ (exit 4) on `accept/t148_cap_narrow_chains`. + -- -- This cannot manufacture a false reject from a mis-decoded -- annotation: `Decl.dfn.retAnnot` is `some` only when the annotation -- is fully IN fragment — `Elab.decodeDecl` forces the whole diff --git a/MarchLean/Syntax.lean b/MarchLean/Syntax.lean index 3300ae3..0cb1d31 100644 --- a/MarchLean/Syntax.lean +++ b/MarchLean/Syntax.lean @@ -39,13 +39,31 @@ inductive Ty where | unsupported deriving Repr, Inhabited +/-! ### Why these walks are `mutual` rather than `partial` + +Every tree walk below recurses through a `List` of children (`args`, `elems`, +`fields`). Written with `List.any`/`List.all` the recursion is *nested* inside +a higher-order call, which Lean's structural-recursion checker cannot see +through — which is why these were all `partial def`. + +`partial def` is not free: it compiles to an opaque constant, so the kernel +can neither unfold it nor induct on it. That is why every test over these +functions had to say `decide` (trusting the compiler) rather than +`decide` (trusting the kernel), and why no theorem about them was possible at +all. Pairing each walk with an explicit `List` helper in a `mutual` block +makes the descent structural, which buys both back. + +Behavior is unchanged: each helper is the fold `List.any`/`List.all` already +performed, in the same order and with the same short-circuiting. -/ + +mutual /-- Does this type contain an `unsupported` node anywhere? -/ -partial def Ty.hasUnsupported : Ty → Bool +def Ty.hasUnsupported : Ty → Bool | .unsupported => true - | .con _ args => args.any Ty.hasUnsupported + | .con _ args => Ty.anyHasUnsupported args | .arrow a b => a.hasUnsupported || b.hasUnsupported - | .tuple ts => ts.any Ty.hasUnsupported - | .record fs => fs.any (fun (_, t) => t.hasUnsupported) + | .tuple ts => Ty.anyHasUnsupported ts + | .record fs => Ty.anyFieldHasUnsupported fs | .lin _ t => t.hasUnsupported | .natOp _ a b => a.hasUnsupported || b.hasUnsupported -- H3: a `TError` should never appear in accept output; if it does, honest-skip @@ -53,14 +71,30 @@ partial def Ty.hasUnsupported : Ty → Bool | .err => true | .var _ | .nat _ => false +/-- `args.any Ty.hasUnsupported`, made structural. -/ +def Ty.anyHasUnsupported : List Ty → Bool + | [] => false + | t :: ts => t.hasUnsupported || Ty.anyHasUnsupported ts + +/-- `fs.any (fun (_, t) => t.hasUnsupported)`, made structural. -/ +def Ty.anyFieldHasUnsupported : List (String × Ty) → Bool + | [] => false + | (_, t) :: fs => t.hasUnsupported || Ty.anyFieldHasUnsupported fs +end + +mutual /-- Structural type equality (NOT canonical — `Check` canonicalizes named -records first, then calls this). -/ -partial def Ty.beq : Ty → Ty → Bool - | .con n1 a1, .con n2 a2 => n1 == n2 && a1.length == a2.length && (a1.zip a2).all (fun (x,y) => x.beq y) +records first, then calls this). + +The list arms fold `length ==` and the zipped element comparison into a single +structural walk: `beqList` returns `false` on a length mismatch by falling +through to its `_, _` arm, which is exactly what `length == length && zip …` +computed before. -/ +def Ty.beq : Ty → Ty → Bool + | .con n1 a1, .con n2 a2 => n1 == n2 && Ty.beqList a1 a2 | .arrow a1 b1, .arrow a2 b2 => a1.beq a2 && b1.beq b2 - | .tuple t1, .tuple t2 => t1.length == t2.length && (t1.zip t2).all (fun (x,y) => x.beq y) - | .record f1, .record f2 => - f1.length == f2.length && (f1.zip f2).all (fun ((n1,t1),(n2,t2)) => n1 == n2 && t1.beq t2) + | .tuple t1, .tuple t2 => Ty.beqList t1 t2 + | .record f1, .record f2 => Ty.beqFields f1 f2 | .var i1, .var i2 => i1 == i2 | .lin l1 t1, .lin l2 t2 => l1 == l2 && t1.beq t2 | .nat n1, .nat n2 => n1 == n2 @@ -69,6 +103,20 @@ partial def Ty.beq : Ty → Ty → Bool | .unsupported, .unsupported => true | _, _ => false +/-- Pointwise `Ty.beq` over two lists; `false` if the lengths differ. -/ +def Ty.beqList : List Ty → List Ty → Bool + | [], [] => true + | x :: xs, y :: ys => x.beq y && Ty.beqList xs ys + | _, _ => false + +/-- Pointwise name-and-type equality over two record field lists; `false` if +the lengths differ. -/ +def Ty.beqFields : List (String × Ty) → List (String × Ty) → Bool + | [], [] => true + | (n1, t1) :: f1, (n2, t2) :: f2 => n1 == n2 && t1.beq t2 && Ty.beqFields f1 f2 + | _, _ => false +end + instance : BEq Ty := ⟨Ty.beq⟩ /-- Typeclass constraint carried by a scheme. -/ @@ -106,16 +154,28 @@ inductive Pattern where | unsupported deriving Repr, Inhabited +mutual /-- Does this pattern contain an `unsupported` node anywhere? -/ -partial def Pattern.hasUnsupported : Pattern → Bool +def Pattern.hasUnsupported : Pattern → Bool | .unsupported => true - | .con _ args => args.any Pattern.hasUnsupported - | .tuple ps => ps.any Pattern.hasUnsupported - | .record fs => fs.any (fun (_, p) => p.hasUnsupported) + | .con _ args => Pattern.anyHasUnsupported args + | .tuple ps => Pattern.anyHasUnsupported ps + | .record fs => Pattern.anyFieldHasUnsupported fs | .as _ p => p.hasUnsupported - | .or_ alts => alts.any Pattern.hasUnsupported + | .or_ alts => Pattern.anyHasUnsupported alts | .wild | .var _ _ | .lit _ => false +/-- `ps.any Pattern.hasUnsupported`, made structural. -/ +def Pattern.anyHasUnsupported : List Pattern → Bool + | [] => false + | p :: ps => p.hasUnsupported || Pattern.anyHasUnsupported ps + +/-- `fs.any (fun (_, p) => p.hasUnsupported)`, made structural. -/ +def Pattern.anyFieldHasUnsupported : List (String × Pattern) → Bool + | [] => false + | (_, p) :: fs => p.hasUnsupported || Pattern.anyFieldHasUnsupported fs +end + /-- Term. Each node carries its resolved type `ty`. `var` and `field` also carry their `span` (for the instantiation join). -/ inductive Term where @@ -188,8 +248,21 @@ def optTyHasUnsupported : Option Ty → Bool | none => false | some t => t.hasUnsupported -/-- Is this term (or any subterm/type) out of fragment? -/ -partial def Term.hasUnsupported : Term → Bool +/-- `ps.any (fun (_, _, a) => optTyHasUnsupported a)` over lambda params. -/ +def anyParamAnnotUnsupported : List (String × Lin × Option Ty) → Bool + | [] => false + | (_, _, a) :: ps => optTyHasUnsupported a || anyParamAnnotUnsupported ps + +mutual +/-- Is this term (or any subterm/type) out of fragment? + +The `| t => t.ty.hasUnsupported || (match t with …)` shape this replaced was +convenient but not structural — the outer catch-all binds the whole term, so +Lean cannot see that the inner `match`'s recursive calls descend. Every +constructor now names its own arm and repeats the node's own `ty` check +explicitly. Same result on every input; `.unsupported` still short-circuits +before the `ty` check, and every other arm still tests `ty` first. -/ +def Term.hasUnsupported : Term → Bool | .unsupported _ => true -- LOAD-BEARING, and deliberately NOT a recursion into `children`: an -- `opaque_` node is out of fragment BY CONSTRUCTION (its own shape is @@ -198,23 +271,51 @@ partial def Term.hasUnsupported : Term → Bool -- gate firing on exactly the files it fired on before this constructor -- existed, which is the entire reason carrying the children costs nothing -- in false-reject exposure. Do not "improve" this to - -- `children.any hasUnsupported`. + -- `Term.anyHasUnsupported children`. | .opaque_ _ _ => true - | t => - t.ty.hasUnsupported || - (match t with - | .app f args _ => f.hasUnsupported || args.any Term.hasUnsupported - | .lam ps b _ => ps.any (fun (_, _, a) => optTyHasUnsupported a) || b.hasUnsupported - | .let_ _ _ annot r b _ => optTyHasUnsupported annot || r.hasUnsupported || b.hasUnsupported - | .letfn _ _ _ pa fb b _ => optTyHasUnsupported pa || fb.hasUnsupported || b.hasUnsupported - | .ite c u v _ => c.hasUnsupported || u.hasUnsupported || v.hasUnsupported - | .con _ args _ => args.any Term.hasUnsupported - | .tuple es _ => es.any Term.hasUnsupported - | .record fs _ => fs.any (fun (_, e) => e.hasUnsupported) - | .field r _ _ _ => r.hasUnsupported - | .match_ s arms _ => s.hasUnsupported || - arms.any (fun (p, g, e) => p.hasUnsupported || (g.map Term.hasUnsupported).getD false || e.hasUnsupported) - | _ => false) + | .lit _ ty => ty.hasUnsupported + | .var _ _ ty => ty.hasUnsupported + | .app f args ty => + ty.hasUnsupported || f.hasUnsupported || Term.anyHasUnsupported args + | .lam ps b ty => + ty.hasUnsupported || anyParamAnnotUnsupported ps || b.hasUnsupported + | .let_ _ _ annot r b ty => + ty.hasUnsupported || optTyHasUnsupported annot || r.hasUnsupported || b.hasUnsupported + | .letfn _ _ _ pa fb b ty => + ty.hasUnsupported || optTyHasUnsupported pa || fb.hasUnsupported || b.hasUnsupported + | .ite c u v ty => + ty.hasUnsupported || c.hasUnsupported || u.hasUnsupported || v.hasUnsupported + | .con _ args ty => ty.hasUnsupported || Term.anyHasUnsupported args + | .tuple es ty => ty.hasUnsupported || Term.anyHasUnsupported es + | .record fs ty => ty.hasUnsupported || Term.anyFieldHasUnsupported fs + | .field r _ _ ty => ty.hasUnsupported || r.hasUnsupported + | .match_ s arms ty => + ty.hasUnsupported || s.hasUnsupported || Term.anyArmHasUnsupported arms + +/-- `es.any Term.hasUnsupported`, made structural. -/ +def Term.anyHasUnsupported : List Term → Bool + | [] => false + | e :: es => e.hasUnsupported || Term.anyHasUnsupported es + +/-- `fs.any (fun (_, e) => e.hasUnsupported)`, made structural. -/ +def Term.anyFieldHasUnsupported : List (String × Term) → Bool + | [] => false + | (_, e) :: fs => e.hasUnsupported || Term.anyFieldHasUnsupported fs + +/-- Match arms: pattern, optional guard, and body all count. The pattern +component is load-bearing — dropping it was a real false-accept bug (see this +file's regression tests). -/ +def Term.anyArmHasUnsupported : List (Pattern × Option Term × Term) → Bool + | [] => false + | (p, g, e) :: arms => + p.hasUnsupported || Term.optHasUnsupported g || e.hasUnsupported + || Term.anyArmHasUnsupported arms + +/-- `(g.map Term.hasUnsupported).getD false`, made structural. -/ +def Term.optHasUnsupported : Option Term → Bool + | none => false + | some e => e.hasUnsupported +end /-- Datatype constructor signature (from a `DType` decl). -/ structure CtorSig where @@ -293,29 +394,40 @@ inductive Decl where | unsupported deriving Repr, Inhabited +mutual /-- Is this declaration (or any term/type it carries) out of fragment? `dtype` carries no terms, but its constructor signatures may reference out-of-fragment types, so those are checked too. The four A3 constructors are IN fragment on their own (`dneeds`/`duse`/`dextern` carry no term/type of their own); `dmod` recurses into its nested decls, since one of those could -still be an unsupported `dfn`/`dlet`/`dtype`. Marked `partial`: the recursion -through `List Decl` inside `dmod` isn't structurally recognized by the -kernel, matching how `Term.hasUnsupported` handles its own nesting. -/ -partial def Decl.hasUnsupported : Decl → Bool +still be an unsupported `dfn`/`dlet`/`dtype`. -/ +def Decl.hasUnsupported : Decl → Bool | .unsupported => true | .dfn _ params retAnnot body => - params.any (fun (_, _, a) => optTyHasUnsupported a) + anyParamAnnotUnsupported params || optTyHasUnsupported retAnnot || body.hasUnsupported | .dlet _ body => body.hasUnsupported - | .dtype _ _ ctors => - ctors.any (fun c => c.argTys.any Ty.hasUnsupported || c.resultTy.hasUnsupported) - | .dmod _ decls => decls.any Decl.hasUnsupported + | .dtype _ _ ctors => Decl.anyCtorHasUnsupported ctors + | .dmod _ decls => Decl.anyHasUnsupported decls | .dneeds _ => false | .duse _ => false | .dextern _ _ => false | .dproofcap _ => false | .dopts _ => false +/-- `decls.any Decl.hasUnsupported`, made structural. -/ +def Decl.anyHasUnsupported : List Decl → Bool + | [] => false + | d :: ds => d.hasUnsupported || Decl.anyHasUnsupported ds + +/-- `ctors.any (fun c => c.argTys.any Ty.hasUnsupported || c.resultTy.hasUnsupported)`. -/ +def Decl.anyCtorHasUnsupported : List CtorSig → Bool + | [] => false + | c :: cs => + Ty.anyHasUnsupported c.argTys || c.resultTy.hasUnsupported + || Decl.anyCtorHasUnsupported cs +end + /-- Splice nested `dmod` decls into a single flat list, for the passes that treat a module as a transparent scope (inference, linearity). Cap checking does NOT use this — `needs` is scoped to its module, so `CapCheck` walks the @@ -324,12 +436,20 @@ tree instead (see `Decl.dmod`'s docstring). This is an approximation of march, which scopes names per module and supports qualified cross-module references. It is sound only while names do not collide across sibling modules; `Elab.decodeModule` refuses files where they do. -Marked `partial`: the recursion through `List Decl` inside `dmod` isn't -structurally recognized by the kernel, matching `Decl.hasUnsupported`. -/ -partial def flattenDecls : List Decl → List Decl + +Unlike the other walks here this one is not structural even with a helper: +the `dmod` arm recurses into `inner`, a list nested *inside* the head element +rather than a tail of the list being consumed. It terminates on the total +size of the declaration forest instead, which `decreasing_by` discharges — +`sizeOf inner` is strictly below `sizeOf (.dmod _ inner :: rest)` because the +list constructor and the `dmod` wrapper each contribute. -/ +def flattenDecls : List Decl → List Decl | [] => [] | .dmod _ inner :: rest => flattenDecls inner ++ flattenDecls rest | d :: rest => d :: flattenDecls rest +termination_by ds => sizeOf ds +decreasing_by + all_goals simp_wf <;> omega structure Scheme where ids : List Int @@ -374,15 +494,19 @@ end MarchLean.Syntax namespace MarchLean.Syntax.Test open MarchLean.Syntax -- A literal-int term annotated Int must be constructible and flagged clean. --- `Ty.hasUnsupported` is a `partial def` (nested recursion through `List.any` --- isn't structurally-recognized by the kernel), so plain `decide` gets stuck --- unfolding it; `native_decide` evaluates via the compiler instead. -example : Ty.hasUnsupported (Ty.con "Int" []) = false := by native_decide +-- +-- These say `decide`, not `native_decide`. They used to say `native_decide`, +-- because the walks below were `partial def`s the kernel could not unfold — +-- so every one of these tests was trusting the compiled evaluator rather than +-- the kernel. Pairing each walk with an explicit `List` helper (see the note +-- above `Ty.hasUnsupported`) made them structural, and the kernel now checks +-- these directly. Do not reintroduce `native_decide` here without saying why. +example : Ty.hasUnsupported (Ty.con "Int" []) = false := by decide -- unsupported propagates through structure. -example : Ty.hasUnsupported (Ty.arrow Ty.unsupported (Ty.con "Int" [])) = true := by native_decide +example : Ty.hasUnsupported (Ty.arrow Ty.unsupported (Ty.con "Int" [])) = true := by decide -- H3: `TError` is a skip trigger — a TError anywhere flags the type. -example : Ty.hasUnsupported Ty.err = true := by native_decide -example : Ty.hasUnsupported (Ty.tuple [Ty.con "Int" [], Ty.err]) = true := by native_decide +example : Ty.hasUnsupported Ty.err = true := by decide +example : Ty.hasUnsupported (Ty.tuple [Ty.con "Int" [], Ty.err]) = true := by decide -- Regression for the false-accept bug where `Term.hasUnsupported`'s -- `match_` arm discarded the `Pattern` component of each arm, so an @@ -397,24 +521,24 @@ private def badNestedArm : Pattern × Option Term × Term := (Pattern.con "Some" [Pattern.unsupported], none, Term.lit (Lit.int 1) intTy) -- A match with only clean patterns/arms is in-fragment. -example : Term.hasUnsupported (Term.match_ okScrut [okArm] intTy) = false := by native_decide +example : Term.hasUnsupported (Term.match_ okScrut [okArm] intTy) = false := by decide -- A match with an `unsupported` pattern directly in an arm must be flagged -- (this is exactly what the old code missed: `fun (_, e) => e.hasUnsupported` -- ignored the pattern). -example : Term.hasUnsupported (Term.match_ okScrut [okArm, badArm] intTy) = true := by native_decide +example : Term.hasUnsupported (Term.match_ okScrut [okArm, badArm] intTy) = true := by decide -- Same, but the `unsupported` is nested inside a constructor pattern. -example : Term.hasUnsupported (Term.match_ okScrut [okArm, badNestedArm] intTy) = true := by native_decide +example : Term.hasUnsupported (Term.match_ okScrut [okArm, badNestedArm] intTy) = true := by decide -- `Pattern.hasUnsupported` itself, standalone: top-level and nested. -example : Pattern.hasUnsupported Pattern.wild = false := by native_decide -example : Pattern.hasUnsupported Pattern.unsupported = true := by native_decide +example : Pattern.hasUnsupported Pattern.wild = false := by decide +example : Pattern.hasUnsupported Pattern.unsupported = true := by decide example : Pattern.hasUnsupported (Pattern.tuple [Pattern.wild, Pattern.unsupported]) = true := by - native_decide -example : Pattern.hasUnsupported (Pattern.as "x" Pattern.unsupported) = true := by native_decide + decide +example : Pattern.hasUnsupported (Pattern.as "x" Pattern.unsupported) = true := by decide -- `Pattern.or_`: clean alternatives are in-fragment; an `unsupported` -- alternative anywhere in the list is not (A3 slice (c) review finding C1). example : Pattern.hasUnsupported (Pattern.or_ [Pattern.con "Red" [], Pattern.con "Green" []]) = false := by - native_decide + decide example : Pattern.hasUnsupported (Pattern.or_ [Pattern.con "Red" [], Pattern.unsupported]) = true := by - native_decide + decide end MarchLean.Syntax.Test diff --git a/scripts/expected-skips.txt b/scripts/expected-skips.txt index 072d104..f261db2 100644 --- a/scripts/expected-skips.txt +++ b/scripts/expected-skips.txt @@ -218,7 +218,32 @@ reject/t131_refine_let_annotation_false.march # out-of-frag reject/t133_refine_trusted_violation_not_rescued.march # out-of-fragment construct in a declaration reject/t134_refine_postcondition_strict_undischarged.march # out-of-fragment construct in a declaration reject/t138_refine_impl_param_remedy_enforced.march # out-of-fragment construct in a declaration - +accept/t141_refine_nth_in_range.march # out of modeled fragment: SKIP: unbound variable `List.nth` +accept/t142_json_ordinary_type_in_cap_module.march # out of modeled fragment: SKIP: unbound variable `from_json` +accept/t143_derive_json_cap_free_in_cap_module.march # out-of-fragment construct in a declaration +accept/t144_cap_type_decl_covered.march # out-of-fragment construct in a declaration +accept/t146_root_cap_in_test_body.march # out-of-fragment construct in a declaration +accept/t149_cap_interface_impl_covered.march # out-of-fragment construct in a declaration +accept/t150_actor_cap_flow.march # out-of-fragment construct in a declaration +accept/t151_ordinary_payload_through_all_send_paths.march # out-of-fragment construct in a declaration +accept/t49_transitive_use_covered.march # REGRESSION (was MATCH): march#209 rewrote this file to add `Vault.new("t")`, the reference the new per-function Check 4 requires. march ACCEPTS it but emits resolved_ty TError for that stdlib call, and H3 honest-skips on TError. See specs/march-findings.md section 4. +reject/t142_refine_nth_out_of_range.march # out of modeled fragment: SKIP: unbound variable `List.nth` +reject/t143_cap_from_json_deferred_zonk.march # out of modeled fragment: SKIP: unbound variable `from_json` +reject/t145_cap_derive_json_record_field.march # out-of-fragment construct in a declaration +reject/t146_cap_to_json_argument.march # out of modeled fragment: SKIP: unbound variable `to_json` +reject/t147_cap_from_json_events.march # out of modeled fragment: SKIP: unbound variable `from_json_events` +reject/t148_cap_record_field_undeclared.march # out-of-fragment construct in a declaration +reject/t150_cap_nested_in_container_undeclared.march # out-of-fragment construct in a declaration +reject/t156_cap_interface_method_signature.march # out-of-fragment construct in a declaration +reject/t157_cap_impl_body_annotation.march # out-of-fragment construct in a declaration +reject/t158_get_cap_is_not_io_authority.march # out of modeled fragment: SKIP: unbound variable `get_cap` +reject/t159_send_checked_bypasses_sendable_check.march # out-of-fragment construct in a declaration +reject/t160_actor_cast_qualified_bypasses_sendable_check.march # out-of-fragment construct in a declaration +reject/t161_actor_cast_bare_bypasses_sendable_check.march # out-of-fragment construct in a declaration +reject/t162_actor_call_qualified_bypasses_sendable_check.march # out-of-fragment construct in a declaration +reject/t163_actor_call_bare_bypasses_sendable_check.march # out-of-fragment construct in a declaration +reject/t164_native_int_arr_not_sendable.march # out-of-fragment construct in a declaration +reject/t165_native_float_arr_not_sendable.march # out-of-fragment construct in a declaration # --- grammar/parse side (21) --- # specs/lang/grammar/parse: 34 files, all march-ACCEPT (a parse-shape # corpus). 13 are judged (accept/accept); the 21 below skip. diff --git a/scripts/known-limitations.txt b/scripts/known-limitations.txt index 47fe887..1f75ed9 100644 --- a/scripts/known-limitations.txt +++ b/scripts/known-limitations.txt @@ -21,3 +21,4 @@ # an INDEPENDENT oracle. reject/t23_derive_unknown_interface.march # rejection reason erased by march's desugarer: `derive Frobnicate for Color` (unknown interface) expands to nothing; emitted Core AST is just `type Color` + `fn main`, well-typed. Invisible to the core AST A2 checks. reject/t49_derive_unknown_type.march # rejection reason erased by march's desugarer: `derive Show for NoSuchType` (unknown type) expands to nothing; emitted Core AST is just `fn main`, well-typed. Invisible to the core AST A2 checks. +reject/t144_cap_derive_json_variant_arg.march # rejection reason erased by march's desugarer: march rejects `derive Json` for a type with a capability position (desugar.ml `| "Json" when caps_in_type_def td <> []`), but the derive expands to nothing, so the emitted Core AST is just `needs IO` + `type Loot = Loot(Cap(IO))` + `fn main`. That residual IS well-typed and its `Cap(IO)` IS covered by `needs IO`, so A2 correctly accepts it. Same mechanism as t23/t49 above. diff --git a/scripts/tailcall-probes/attr.march b/scripts/tailcall-probes/attr.march index 4d52b6a..e19b97e 100644 --- a/scripts/tailcall-probes/attr.march +++ b/scripts/tailcall-probes/attr.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console @[no_warn_recursion] fn loopy(n : Int) : Int do if n == 0 do 0 else loopy(n + 1) + 1 end diff --git a/scripts/tailcall-probes/attr_mutual.march b/scripts/tailcall-probes/attr_mutual.march index 4ade9b3..8b3c2a0 100644 --- a/scripts/tailcall-probes/attr_mutual.march +++ b/scripts/tailcall-probes/attr_mutual.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console @[no_warn_recursion] fn ping(n : Int) : Int do if n == 0 do 0 else pong(n + 1) + 1 end diff --git a/scripts/tailcall-probes/cond_tail.march b/scripts/tailcall-probes/cond_tail.march index 2e6c608..ab8ec95 100644 --- a/scripts/tailcall-probes/cond_tail.march +++ b/scripts/tailcall-probes/cond_tail.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn dec(x : Int) : Int do x - 1 end fn spin(n : Int) : Int do match do diff --git a/scripts/tailcall-probes/fact.march b/scripts/tailcall-probes/fact.march index 50e3d01..75a1fad 100644 --- a/scripts/tailcall-probes/fact.march +++ b/scripts/tailcall-probes/fact.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn fact(n : Int) : Int do if n <= 1 do 1 else fact(n - 1) * n end end diff --git a/scripts/tailcall-probes/go.march b/scripts/tailcall-probes/go.march index b48e7f0..99ce870 100644 --- a/scripts/tailcall-probes/go.march +++ b/scripts/tailcall-probes/go.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn go(n : Int) : Int do if n == 0 do 0 else go(n + 1) + 1 end end diff --git a/scripts/tailcall-probes/lambda_body.march b/scripts/tailcall-probes/lambda_body.march index d8fab7f..620d1e2 100644 --- a/scripts/tailcall-probes/lambda_body.march +++ b/scripts/tailcall-probes/lambda_body.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn spin(n : Int) : Int do let f = fn x -> spin(x + 1) + 1 if n == 0 do 0 else spin(n - 1) end diff --git a/scripts/tailcall-probes/lambda_edge.march b/scripts/tailcall-probes/lambda_edge.march index 95ed7d1..9ebb837 100644 --- a/scripts/tailcall-probes/lambda_edge.march +++ b/scripts/tailcall-probes/lambda_edge.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn peer(n : Int) : Int do if n == 0 do 0 else spin(n + 1) + 1 end end diff --git a/scripts/tailcall-probes/letfn_edge.march b/scripts/tailcall-probes/letfn_edge.march index 413d115..48b1928 100644 --- a/scripts/tailcall-probes/letfn_edge.march +++ b/scripts/tailcall-probes/letfn_edge.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn peer(n : Int) : Int do if n == 0 do 0 else spin(n + 1) + 1 end end diff --git a/scripts/tailcall-probes/letq_tail.march b/scripts/tailcall-probes/letq_tail.march index ac5fd34..02f8c0f 100644 --- a/scripts/tailcall-probes/letq_tail.march +++ b/scripts/tailcall-probes/letq_tail.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn step(x : Int) : Result(Int, String) do if x > 0 do Ok(x - 1) else Err("neg") end end diff --git a/scripts/tailcall-probes/loopy.march b/scripts/tailcall-probes/loopy.march index 30e7345..7246c31 100644 --- a/scripts/tailcall-probes/loopy.march +++ b/scripts/tailcall-probes/loopy.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn loopy(n : Int) : Int do if n == 0 do 0 else loopy(n + 1) + 1 end end diff --git a/scripts/tailcall-probes/match_structural.march b/scripts/tailcall-probes/match_structural.march index ddeca94..af760fb 100644 --- a/scripts/tailcall-probes/match_structural.march +++ b/scripts/tailcall-probes/match_structural.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console type Tree = Leaf | Node(Tree, Tree) fn depth(t : Tree) : Int do match t do diff --git a/scripts/tailcall-probes/mutual.march b/scripts/tailcall-probes/mutual.march index 247ae60..e60183a 100644 --- a/scripts/tailcall-probes/mutual.march +++ b/scripts/tailcall-probes/mutual.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console type Node = Leaf | Branch(Int) fn walk(n : Node) : Int do match n do diff --git a/scripts/tailcall-probes/nested_mod.march b/scripts/tailcall-probes/nested_mod.march index d535630..4ce7cdc 100644 --- a/scripts/tailcall-probes/nested_mod.march +++ b/scripts/tailcall-probes/nested_mod.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console mod Inner do fn boom(n : Int) : Int do if n == 0 do 0 else boom(n + 1) + 1 end diff --git a/scripts/tailcall-probes/nested_mod_flat.march b/scripts/tailcall-probes/nested_mod_flat.march index 0059136..10f9ffc 100644 --- a/scripts/tailcall-probes/nested_mod_flat.march +++ b/scripts/tailcall-probes/nested_mod_flat.march @@ -1,4 +1,5 @@ mod Inner do + needs IO.Console fn boom(n : Int) : Int do if n == 0 do 0 else boom(n + 1) + 1 end end diff --git a/scripts/tailcall-probes/nullary_ctor.march b/scripts/tailcall-probes/nullary_ctor.march index 0eceb40..b63087c 100644 --- a/scripts/tailcall-probes/nullary_ctor.march +++ b/scripts/tailcall-probes/nullary_ctor.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console type Tree = Leaf | Node(Tree, Tree) fn size(t : Tree) : Int do match t do diff --git a/scripts/tailcall-probes/shadow_edge_let.march b/scripts/tailcall-probes/shadow_edge_let.march index c3388c6..d73b363 100644 --- a/scripts/tailcall-probes/shadow_edge_let.march +++ b/scripts/tailcall-probes/shadow_edge_let.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn helper(x : Int) : Int do x + 1 end fn peer(n : Int) : Int do if n == 0 do 0 else spin(n + 1) + 1 end diff --git a/scripts/tailcall-probes/shadow_edge_letfn.march b/scripts/tailcall-probes/shadow_edge_letfn.march index 2938220..c9d8cd7 100644 --- a/scripts/tailcall-probes/shadow_edge_letfn.march +++ b/scripts/tailcall-probes/shadow_edge_letfn.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn peer(n : Int) : Int do if n == 0 do 0 else spin(n + 1) + 1 end end diff --git a/scripts/tailcall-probes/shadow_edge_match.march b/scripts/tailcall-probes/shadow_edge_match.march index c03e450..05a185d 100644 --- a/scripts/tailcall-probes/shadow_edge_match.march +++ b/scripts/tailcall-probes/shadow_edge_match.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console type Box = Wrap(Int -> Int) fn peer(n : Int) : Int do if n == 0 do 0 else spin(n + 1) + 1 end diff --git a/scripts/tailcall-probes/shadow_let.march b/scripts/tailcall-probes/shadow_let.march index f03e560..73d9c3b 100644 --- a/scripts/tailcall-probes/shadow_let.march +++ b/scripts/tailcall-probes/shadow_let.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn helper(x : Int) : Int do x + 1 end fn other(n : Int) : Int do if n == 0 do 0 else spin(n - 1) end diff --git a/scripts/tailcall-probes/shadow_letfn.march b/scripts/tailcall-probes/shadow_letfn.march index 27283b3..e823f59 100644 --- a/scripts/tailcall-probes/shadow_letfn.march +++ b/scripts/tailcall-probes/shadow_letfn.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn other(n : Int) : Int do if n == 0 do 0 else spin(n - 1) end end diff --git a/scripts/tailcall-probes/shadow_match.march b/scripts/tailcall-probes/shadow_match.march index 463f4c5..be59cd1 100644 --- a/scripts/tailcall-probes/shadow_match.march +++ b/scripts/tailcall-probes/shadow_match.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console type Box = Wrap(Int -> Int) fn other(n : Int) : Int do if n == 0 do 0 else spin(n - 1) end diff --git a/scripts/tailcall-probes/tail_ok.march b/scripts/tailcall-probes/tail_ok.march index 2820e7a..36e33a1 100644 --- a/scripts/tailcall-probes/tail_ok.march +++ b/scripts/tailcall-probes/tail_ok.march @@ -1,4 +1,5 @@ mod M do + needs IO.Console fn count(n : Int, acc : Int) : Int do if n == 0 do acc else count(n + 1, acc + 1) end end diff --git a/specs/march-findings.md b/specs/march-findings.md index 7ac0b5c..7215427 100644 --- a/specs/march-findings.md +++ b/specs/march-findings.md @@ -211,3 +211,173 @@ so it keeps `Mono (String → ())` and march rejects `print(1)`. We match. The **Status.** not a march bug; no upstream report. Recorded because our correctness depends on it and the dependency is invisible from our source alone. + +--- + +## Checker gaps against march main 6867c783 that the corpus CANNOT catch + +Unlike every entry above, these are **checker-is-wrong** items, recorded here +by exception because of a property they share: each is a live divergence +against the pinned march with **zero corpus witnesses**, so the conformance +gate is structurally incapable of reporting them. The standing rule that a +green run is weak evidence is usually a caution; here it is a certainty. +Each needs a hand-built probe, not a corpus file. + +Found during the 2026-08-08 capability resync (pin 7c1d701c -> 6867c783), +which fixed five corpus-visible divergences; these three were found by +reading march's diff rather than by running anything. + +### 1. Path-scoped capabilities decode as unscoped — FALSE ACCEPT by construction + +march added scopes: `needs IO.FileRead("/etc/myapp")` narrows a filesystem +capability to a directory subtree (`lib/caps/cap_scope.ml`). The emitter now +carries them in a NEW `scopes` array parallel to `paths`, and march's own +comment on that change says the scope is emitted "so a dumped AST is not a +widened version of the source." + +`Elab.decodeDecl`'s `DNeeds` arm reads only `paths`. The scope is dropped, so +a scoped declaration decodes identically to an unscoped one. Since +`Cap_scope.scope_subsumes` states that `None` (unscoped) subsumes everything +and **a scope never subsumes `None`**, this checker reads a strictly narrower +declaration as the broadest possible one — the exact direction that produces +a false accept. + +Not yet reachable in the corpus: no file under `specs/lang/types` uses the +syntax. That is why it is dangerous rather than reassuring. + +**Fix shape.** Decode `scopes` alongside `paths`, carry the scope on +`Decl.dneeds`, and gate coverage on `scope_subsumes` as well as +`capSubsumes`. Until then this is a known false-accept source. + +### 2. `capsInTy` does not descend into `Tagged` + +march's `Cap_surface_ty.caps_in_ty` recurses into every `TyCon`'s arguments, +including `Tagged`. Its predecessor had an explicit `| Tagged -> []` arm; +that arm is GONE, and march's comment records why: skipping it "also blinded +the walk to `Tagged(R, Cap(IO))`, which is a worse trade." + +`CapCheck.capsInTy` still has `| .con "Tagged" _ => []`, mirroring the arm +march deleted. A capability nested inside a `Tagged` payload is therefore +invisible to Check 1 here and visible to march. No corpus file exercises it. + +### 3. `normalize` does not deduplicate + +march's `Cap_lattice.normalize` now dedupes before filtering; ours does not, +so the two disagree on any input containing repeated caps (ours returns the +duplicates, march returns one). march's change was a performance fix (an env +reused across ~1800 modules grew the list without bound), but it is a +semantic difference in the returned list. + +Latent only because `normalize` is not on this checker's verdict path — it is +defined and proved about (`Calculus/Lattice.lean`) but never consulted by +`checkCaps`. If it is ever wired in, this must be fixed first, and the +`normalizeIn` theorems re-proved against the deduping definition. + +### 4. Check 4 uses the pre-#209 whole-module rule — we are now STRICTER than march + +march#209 ("an importer inherits only the capabilities it actually +references", 8f8c66d6) changed Check 4's semantics. `use M` used to force +every capability `M` declares onto the importer; it now forces only the +capabilities demanded by the functions the importer actually references, via +the new `import_required_caps`. + +`CapCheck.checkOneModule`'s Check 4 still implements the old rule: it takes +`M`'s entire declared `needs` from the `module_caps` table and requires the +importer to cover all of it. march's own commit message states the change is +"strictly loosening by construction: the result is always a subset of what +the import required before" — so this checker is now strictly STRICTER than +march on Check 4, and the divergence direction is FALSE REJECT. + +The witness shape: a module that imports a cap-declaring module but +references only its cap-free functions. march accepts (nothing referenced +demands the cap); this checker rejects (the cap is in `M`'s declared set). + +No corpus witness today. `reject/t39_transitive_use_missing_cap` still +matches, because there the capability is uncovered under either rule. +`accept/t49_transitive_use_covered` was rewritten by the same commit to add +the reference the new rule requires (`let _ = Vault.new("t")`), and now +SKIPS here for an unrelated reason — see below. + +**Corollary finding (march side): an accepted file's emitted AST contains +`TError`.** `accept/t49`'s added `Vault.new("t")` is a call into stdlib +`Vault`. march's `--check` resolves it and ACCEPTS; its own +`--emit-core-ast` emits `resolved_ty: TError` for that call and for the +enclosing `let`, while the envelope's `verdict` field still says `accept`. +This checker honest-skips on `TError` by design (H3: never check a file +built on an elaboration error), which is why t49 regressed MATCH -> SKIP and +why A3 slice (a) is now one file short of the 11 it claimed. The skip is +correct behavior here; the inconsistency is march emitting an +elaboration-error sentinel in a program it accepts. + +**Status.** reported upstream: NOT YET (both halves). + +### 5. Check 1b is now an ERROR in march, and this checker does not implement it — a LIVE false-accept class + +**This one obsoletes a design decision, so it is the most consequential entry +in this section.** + +`specs/plans/2026-07-23-a3-capability-lattice-design.md` §1.3 decided NOT to +implement Checks 1b/1c, and said so plainly: + +> They are WARNING-only in march. §2.8.6 calls this three-tier reality "the +> single most consequential fact for anyone relying on `needs` as a soundness +> guarantee." A checker that rejected on them would manufacture false +> MISMATCHes against a march that accepts. Consequence, stated plainly: the +> oracle inherits march's weaker guarantee here — it will not catch a program +> that uses a builtin requiring an undeclared cap in a function body. + +That reasoning was correct when written. It is now obsolete: march main +(`6867c783`) raises Check 1b with `Err.error_with_fix` +(`typecheck.ml:9098-9106`), not `Err.warning` — + + function body calls a builtin that requires `Cap(IO.Console)` + but `M` does not declare `needs IO.Console`. + +march closed the hole its own docs called the most consequential fact about +`needs`. This checker did not, so the "weaker guarantee" the design accepted +is no longer shared with march — it is a **divergence**, and it points the +false-ACCEPT way: any module calling an IO builtin in a body without declaring +the capability is rejected by march and accepted here. + +**Witness.** Every one of `scripts/tailcall-probes/*.march` before the +accompanying fix: `mod M do fn main() do println("hi") end end` with no +`needs`. march rejects; `march-lean-check` exits 0. + +**How it was found, which matters more than the finding.** The 277-file +conformance corpus reports MISMATCH 0 against this same pin — every corpus +file declares its capabilities properly, so not one of them witnesses this. +It surfaced only because the tail-call probes were hand-written without +capability manifests and the pin bump made march start rejecting them. A +green corpus run said nothing about a whole false-accept class; eighteen +throwaway probes found it immediately. + +**Fix shape.** The machinery already exists: `CapCheck.builtinCaps` maps +builtin name -> required cap path, and `bodyCalls` already walks bodies for +builtin calls (both were built for Check 8 and the behavioral caps). Check 1b +is those two joined to `covered declared`. What needs care is the gating, and it is +not hypothetical care — implementing this slightly too eagerly converts the +false-accept class into a false-REJECT class. Three specific hazards, all +verified against march `6867c783`: + +1. **Shadowing.** `bodyCalls` matches purely by NAME + (`banned.contains n`), with no scope awareness. A module defining its own + `fn println(...)` and calling it would be flagged as calling the builtin. + The corpus already contains shadowing cases + (`accept/t126_entry_module_shadows_list_length`, + `accept/t139_nested_module_shadows_list_length_extern`) and march grew + `shadow_*` tail-call probes, so this WILL fire. +2. **Direct calls only.** march's own comment scopes 1b explicitly: it + catches a direct builtin call in a module body; a stdlib-MEDIATED call + (`File.read` rather than `file_read`) is invisible to it and is handled by + `--cap-strict`'s TIR ceiling instead. Scanning transitively would reject + where march accepts. +3. **1c stays off.** march flipped 1b only — + Check 1c (extern implies `IO.Foreign`) is deliberately still a warning. + Flipping both because they were skipped together would be wrong. + +The self-declaration exemption applies here too: march tests +`not covered && not self_declared` against `env.proof_caps`, which +`checkOneModule` already threads as `selfDeclaredCaps`. + +**Status.** reported upstream: N/A (march is correct here; this checker is +behind). NOT YET FIXED in march-lean. diff --git a/specs/plans/2026-07-23-a3-capability-lattice-design.md b/specs/plans/2026-07-23-a3-capability-lattice-design.md index e906445..e6d1a8c 100644 --- a/specs/plans/2026-07-23-a3-capability-lattice-design.md +++ b/specs/plans/2026-07-23-a3-capability-lattice-design.md @@ -53,6 +53,12 @@ this project comes to a provably-equivalent model of march. emitter already builds the exact structure needed (§2.2), so this surfaces an existing value rather than computing anything new. +> **SUPERSEDED (2026-08-10).** march main `6867c783` promoted Check 1b from +> WARNING to ERROR (`typecheck.ml:9098`, `Err.error_with_fix`). Decision 3 +> below was correct against the march of its time and is now obsolete: not +> implementing 1b is no longer "inheriting march's weaker guarantee", it is a +> live false-ACCEPT divergence. See `specs/march-findings.md` §5. + 3. **Do NOT implement Checks 1b/1c.** They are WARNING-only in march. §2.8.6 calls this three-tier reality "the single most consequential fact for anyone relying on `needs` as a soundness guarantee." A checker that diff --git a/specs/plans/2026-08-08-calculus-p0-verdicts-lattice.md b/specs/plans/2026-08-08-calculus-p0-verdicts-lattice.md new file mode 100644 index 0000000..6f137de --- /dev/null +++ b/specs/plans/2026-08-08-calculus-p0-verdicts-lattice.md @@ -0,0 +1,743 @@ +# Calculus P0 — Verdict Algebra + Lattice Metatheory Implementation Plan + +> **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. + +**Goal:** Land phases P0a + P0b of `specs/plans/2026-08-08-calculus-proof-capabilities-design.md`: kernel-checked theorems for the verdict algebra (`CapResult.andThen`, `DivVerdict.join`) and the capability lattice (parameterized over an abstract table, with march's 20-entry table discharged by `decide`). + +**Architecture:** Three new files — `MarchLean/Calculus/Verdicts.lean` (verdict algebra, purely additive), `MarchLean/Calculus/Lattice.lean` (abstract table defs + metatheory), `MarchLean/Calculus/Concrete.lean` (`WellFormedB hierarchy` by `decide` + shipping-name corollaries). One API-preserving refactor: `MarchLean/CapLattice.lean`'s five defs become specializations of the abstract ones. One CI edit: a sorry/admit grep. + +**Tech Stack:** Lean 4 (toolchain `leanprover/lean4:v4.29.0`, pinned in `lean-toolchain`), no dependencies (no mathlib — core `List.Perm`/`List.IsSuffix`/`List.Nodup` are available and sufficient; verified against this toolchain). Build: `lake build` with `lake` at `~/.elan/bin/lake` (not in default PATH — every shell snippet below exports it). Conformance: `scripts/conformance-harness.sh` with local `march` 0.2.0 (`~/.opam/march/bin/march`) and corpus `~/code/march/specs/lang/types` (122 accept + 120 reject). + +## Global Constraints + +- **No mathlib, no new dependencies.** `lake-manifest.json` stays `"packages": []`. +- **API preservation (design §2):** `capParent`, `capAncestorsFuel`, `capAncestors`, `capSubsumes`, `normalize`, `hierarchy` keep their exact names, signatures, and results. No call site outside `CapLattice.lean` changes. +- **No `sorry`/`admit` in committed code.** Intermediate build checks may use `sorry` to validate statements elaborate; every commit is sorry-free. +- **Theorem-statement fidelity:** later plans (P2) consume these exact names — do not rename while proving. If a statement turns out false as written, STOP and report (that is a design finding, not a proof obstacle to engineer around). +- **Repo proof idiom:** theorems and their `example` smoke tests live in the same file they concern (matches existing inline-`#eval`/`example` convention). No separate test directory exists or is created. +- **Build command everywhere:** `export PATH="$HOME/.elan/bin:$PATH" && lake build` from the repo root. A clean build with zero warnings on new files is the pass criterion (`sorry` is a *warning* in Lean — read the output, don't trust exit 0 alone). + +## Baseline (already verified in this worktree, 2026-08-08) + +- `lake build march-lean-check` — green, 22 jobs. +- Kernel `decide` proves the 20-entry `WellFormedB hierarchy` probe in ~0.5s — plain `decide` is viable for Task 7; `native_decide` fallback should NOT be needed. +- Core has `List.Perm` (with decidable instances), `List.IsSuffix` (`<:+`), `List.Nodup`, `List.filter_subset`. Core does NOT have `List.isSuffix_iff` or `List.mem_of_mem_filter` under those names — use `List.mem_filter` and manual suffix reasoning. + +--- + +### Task 1: Corpus baseline + `Calculus/Verdicts.lean` — `CapResult` algebra + +**Files:** +- Create: `MarchLean/Calculus/Verdicts.lean` +- Modify: `MarchLean.lean` (add `import MarchLean.Calculus.Verdicts` at the end) + +**Interfaces:** +- Consumes: `MarchLean.CapCheck.CapResult` (`ok | violation (msg) | skip (reason)`), `CapResult.andThen` (`MarchLean/CapCheck.lean:39-62`, namespace `MarchLean.CapCheck`). +- Produces (P2 depends on these exact names, all in namespace `MarchLean.Calculus`): + - `inductive Tier | ok | skip | violation` (`DecidableEq, Repr`) + - `Tier.max : Tier → Tier → Tier` + - `tierOf : CapResult → Tier` + - `theorem ok_andThen (r : CapResult) : CapResult.ok.andThen r = r` + - `theorem andThen_ok (r : CapResult) : r.andThen .ok = r` + - `theorem violation_andThen (m : String) (r : CapResult) : (CapResult.violation m).andThen r = .violation m` + - `theorem andThen_assoc (a b c : CapResult) : (a.andThen b).andThen c = a.andThen (b.andThen c)` + - `theorem Tier.max_comm / max_assoc / max_idem / ok_max / max_ok` + - `theorem tierOf_andThen (a b : CapResult) : tierOf (a.andThen b) = (tierOf a).max (tierOf b)` + - `theorem tierOf_andThen_comm (a b : CapResult) : tierOf (a.andThen b) = tierOf (b.andThen a)` + +- [ ] **Step 1: Record the conformance baseline (pre-change, one time for the whole plan)** + +```bash +export PATH="$HOME/.elan/bin:$PATH" && cd "$(git rev-parse --show-toplevel)" && \ +lake build march-lean-check && \ +MARCH_BIN="$HOME/.opam/march/bin/march" \ +CORPUS_DIR="$HOME/code/march/specs/lang/types" \ +MARCH_LEAN_CHECK_BIN=.lake/build/bin/march-lean-check \ +scripts/conformance-harness.sh > /tmp/p0-corpus-baseline.txt 2>&1; \ +echo "exit=$?" >> /tmp/p0-corpus-baseline.txt; tail -20 /tmp/p0-corpus-baseline.txt +``` + +Note: the local `march` may not be at CI's pinned SHA, so the ledger check may fail here — that is fine. **The invariant this plan enforces is that this output is byte-identical before and after every shipping-code change**, not that the local run is green. + +- [ ] **Step 2: Write the failing statements** + +Create `MarchLean/Calculus/Verdicts.lean` with every theorem stated and proved by `sorry`: + +```lean +/-! +# Verdict algebra + +Kernel-checked laws for the two verdict-combination operators the capability +checker folds with: `CapResult.andThen` (`CapCheck.lean`) and +`DivVerdict.join`. What is proved and what is deliberately NOT: + +- `andThen` is associative with identity `ok`; `violation` left-absorbs. It + is NOT commutative — messages are leftmost-wins by design — but the tier + projection (`tierOf`) IS: `tierOf` is a homomorphism onto `Tier.max`, so + which verdict *tier* a fold produces never depends on fold order, only + which *message*. P2's order-independence theorem builds on exactly this. +-/ +import MarchLean.CapCheck + +namespace MarchLean.Calculus +open MarchLean.CapCheck + +/-- Verdict severity, forgetting messages: `ok < skip < violation`. -/ +inductive Tier where + | ok | skip | violation + deriving DecidableEq, Repr + +/-- Max in the severity order (violation absorbs, ok is identity). -/ +def Tier.max : Tier → Tier → Tier + | .violation, _ => .violation + | _, .violation => .violation + | .skip, _ => .skip + | _, .skip => .skip + | .ok, .ok => .ok + +/-- The tier of a verdict (forget the message). -/ +def tierOf : CapResult → Tier + | .ok => .ok + | .skip _ => .skip + | .violation _ => .violation + +theorem ok_andThen (r : CapResult) : CapResult.ok.andThen r = r := sorry +theorem andThen_ok (r : CapResult) : r.andThen .ok = r := sorry +theorem violation_andThen (m : String) (r : CapResult) : + (CapResult.violation m).andThen r = .violation m := sorry +theorem andThen_assoc (a b c : CapResult) : + (a.andThen b).andThen c = a.andThen (b.andThen c) := sorry + +theorem Tier.max_comm (a b : Tier) : a.max b = b.max a := sorry +theorem Tier.max_assoc (a b c : Tier) : (a.max b).max c = a.max (b.max c) := sorry +theorem Tier.max_idem (a : Tier) : a.max a = a := sorry +theorem Tier.ok_max (a : Tier) : Tier.ok.max a = a := sorry +theorem Tier.max_ok (a : Tier) : a.max .ok = a := sorry + +/-- `tierOf` is a monoid homomorphism `(CapResult, andThen, ok) → (Tier, max, ok)`. -/ +theorem tierOf_andThen (a b : CapResult) : + tierOf (a.andThen b) = (tierOf a).max (tierOf b) := sorry + +/-- Tiers are fold-order-independent even though messages are not. -/ +theorem tierOf_andThen_comm (a b : CapResult) : + tierOf (a.andThen b) = tierOf (b.andThen a) := sorry + +end MarchLean.Calculus +``` + +Append to `MarchLean.lean`: `import MarchLean.Calculus.Verdicts` + +- [ ] **Step 3: Build — verify statements elaborate and each `sorry` warns** + +Run: `export PATH="$HOME/.elan/bin:$PATH" && lake build 2>&1 | grep -c "declaration uses 'sorry'"` +Expected: `11`. If instead there are *errors*, a statement doesn't elaborate (wrong name/namespace) — fix the statement, not the definitions. + +- [ ] **Step 4: Prove** + +Every proof here is exhaustive case analysis; message arguments are variables the `andThen` arms never inspect, so each case closes by `rfl`: + +```lean +theorem ok_andThen (r : CapResult) : CapResult.ok.andThen r = r := by cases r <;> rfl +theorem andThen_ok (r : CapResult) : r.andThen .ok = r := by cases r <;> rfl +theorem violation_andThen (m : String) (r : CapResult) : + (CapResult.violation m).andThen r = .violation m := rfl +theorem andThen_assoc (a b c : CapResult) : + (a.andThen b).andThen c = a.andThen (b.andThen c) := by + cases a <;> cases b <;> cases c <;> rfl +``` + +Same shape (`cases … <;> rfl`) for the five `Tier` laws and `tierOf_andThen`. Then: + +```lean +theorem tierOf_andThen_comm (a b : CapResult) : + tierOf (a.andThen b) = tierOf (b.andThen a) := by + rw [tierOf_andThen, tierOf_andThen, Tier.max_comm] +``` + +- [ ] **Step 5: Build — verify clean** + +Run: `export PATH="$HOME/.elan/bin:$PATH" && lake build 2>&1 | tail -3` and `lake build 2>&1 | grep -c sorry` +Expected: "Build completed successfully", grep count `0`. + +- [ ] **Step 6: Commit** + +```bash +git add MarchLean/Calculus/Verdicts.lean MarchLean.lean +git commit -m "feat(calculus): CapResult verdict algebra — andThen monoid, tier homomorphism (P0a)" +``` + +--- + +### Task 2: `DivVerdict` semilattice + `joinAll` permutation invariance + +**Files:** +- Modify: `MarchLean/Calculus/Verdicts.lean` (append) + +**Interfaces:** +- Consumes: `MarchLean.CapCheck.DivVerdict` (`safe | unknown | divZero`, `DecidableEq`), `DivVerdict.join`, `DivVerdict.joinAll` (`CapCheck.lean:638-659`; `joinAll vs = vs.foldl join .safe`). +- Produces (namespace `MarchLean.Calculus`): + - `theorem join_comm / join_assoc / join_idem (on DivVerdict)` + - `theorem safe_join (a) : DivVerdict.safe.join a = a` and `join_safe (a) : a.join .safe = a` + - `theorem divZero_join (a) : DivVerdict.divZero.join a = .divZero` + - `theorem foldl_join_shift (l : List DivVerdict) (a : DivVerdict) : l.foldl DivVerdict.join a = a.join (DivVerdict.joinAll l)` + - `theorem joinAll_perm {l₁ l₂ : List DivVerdict} (h : l₁.Perm l₂) : DivVerdict.joinAll l₁ = DivVerdict.joinAll l₂` + +- [ ] **Step 1: Append the statements with `sorry`, build, expect exactly the new sorry-warnings** + +```lean +theorem join_comm (a b : DivVerdict) : a.join b = b.join a := sorry +theorem join_assoc (a b c : DivVerdict) : (a.join b).join c = a.join (b.join c) := sorry +theorem join_idem (a : DivVerdict) : a.join a = a := sorry +theorem safe_join (a : DivVerdict) : DivVerdict.safe.join a = a := sorry +theorem join_safe (a : DivVerdict) : a.join .safe = a := sorry +theorem divZero_join (a : DivVerdict) : DivVerdict.divZero.join a = .divZero := sorry + +/-- Fold with any accumulator = accumulator joined onto the fold from `safe`. +The bridge that lets `joinAll` be reasoned about pointwise. -/ +theorem foldl_join_shift (l : List DivVerdict) (a : DivVerdict) : + l.foldl DivVerdict.join a = a.join (DivVerdict.joinAll l) := sorry + +/-- `joinAll` is permutation-invariant: division-site verdict joins do not +depend on traversal order. P2's order-independence theorem consumes this. -/ +theorem joinAll_perm {l₁ l₂ : List DivVerdict} (h : l₁.Perm l₂) : + DivVerdict.joinAll l₁ = DivVerdict.joinAll l₂ := sorry +``` + +Run: `lake build 2>&1 | grep -c "declaration uses 'sorry'"` — expected `8`. + +- [ ] **Step 2: Prove the pointwise laws** — all six are `by cases … <;> rfl` (or `rfl` for `divZero_join`). + +- [ ] **Step 3: Prove `foldl_join_shift`** — induction on `l` generalizing the accumulator: + +```lean +theorem foldl_join_shift (l : List DivVerdict) (a : DivVerdict) : + l.foldl DivVerdict.join a = a.join (DivVerdict.joinAll l) := by + induction l generalizing a with + | nil => simp [DivVerdict.joinAll, List.foldl, join_safe] + | cons x xs ih => + simp only [DivVerdict.joinAll, List.foldl] at * + rw [ih (a.join x), ih (DivVerdict.safe.join x), safe_join, join_assoc] +``` + +If the `simp only` set doesn't reduce `joinAll (x :: xs)` to `(xs.foldl join (safe.join x))`, unfold `DivVerdict.joinAll` explicitly first (`show` or `unfold`). Iterate until green — the statement is fixed, the script is not. + +- [ ] **Step 4: Prove `joinAll_perm`** — induction on the `Perm` derivation; `foldl_join_shift` collapses each case: + +```lean +theorem joinAll_perm {l₁ l₂ : List DivVerdict} (h : l₁.Perm l₂) : + DivVerdict.joinAll l₁ = DivVerdict.joinAll l₂ := by + induction h with + | nil => rfl + | cons x _ ih => + simp only [DivVerdict.joinAll, List.foldl] + rw [foldl_join_shift, foldl_join_shift] + exact congrArg _ ih -- both sides are (safe.join x).join (joinAll tail) + | swap x y l => + simp only [DivVerdict.joinAll, List.foldl] + rw [foldl_join_shift, foldl_join_shift] + congr 1 + cases x <;> cases y <;> rfl + | trans _ _ ih₁ ih₂ => exact ih₁.trans ih₂ +``` + +The `ih` shapes in `cons`/`swap` may need massaging (`DivVerdict.joinAll` unfolding, `congrArg` target); iterate until green. + +- [ ] **Step 5: Build clean, then commit** + +Run: `lake build 2>&1 | tail -3` + sorry-grep `0`. + +```bash +git add MarchLean/Calculus/Verdicts.lean +git commit -m "feat(calculus): DivVerdict join semilattice + joinAll permutation invariance (P0a)" +``` + +--- + +### Task 3: `Calculus/Lattice.lean` abstract defs + `CapLattice.lean` specialization refactor + +**Files:** +- Create: `MarchLean/Calculus/Lattice.lean` (defs only in this task; theorems come in Tasks 4-6) +- Modify: `MarchLean/CapLattice.lean` (five defs become specializations; `hierarchy`, docstrings, and all `#eval` pins unchanged) +- Modify: `MarchLean.lean` (add `import MarchLean.Calculus.Lattice` BEFORE `import MarchLean.CapLattice`) + +**Interfaces:** +- Consumes: nothing (leaf file). +- Produces (namespace `MarchLean.Calculus`; Tasks 4-7 and P2 depend on these exact names): + - `abbrev Table := List (String × Option String)` + - `def parentIn (T : Table) (c : String) : Option String` + - `def ancestorsInFuel (T : Table) : Nat → String → List String` + - `def ancestorsIn (T : Table) (c : String) : List String` + - `def subsumesIn (T : Table) (parent child : String) : Bool` + - `def normalizeIn (T : Table) (caps : List String) : List String` + - `def coveredIn (T : Table) (declared : List String) (used : String) : Bool` + - And in `MarchLean.CapLattice`, unchanged signatures: `hierarchy : Table`, `capParent`, `capAncestorsFuel`, `capAncestors`, `capSubsumes`, `normalize`. + +- [ ] **Step 1: Create `MarchLean/Calculus/Lattice.lean`** + +Bodies are copied verbatim from today's `CapLattice.lean` with the table made a parameter — definitional equality with the shipping code is the point: + +```lean +/-! +# Abstract capability-lattice theory + +`CapLattice.lean`'s five operations, parameterized over the `(name, parent)` +table so their metatheory is proved once for ANY well-formed table and +march's concrete 20-entry `hierarchy` is discharged by `decide` +(`Calculus/Concrete.lean`). The shipping `CapLattice` API is the +specialization of these to `hierarchy`, definition for definition — bodies +here are copied verbatim from the pre-P0 `CapLattice.lean`, table made a +parameter, nothing else changed. +-/ +namespace MarchLean.Calculus + +/-- A capability table: `(cap_path, parent_path)` rows. -/ +abbrev Table := List (String × Option String) + +/-- The parent of a capability in `T`, or `none` for a root or an unknown +(FFI) name. -/ +def parentIn (T : Table) (c : String) : Option String := + match T.find? (fun (n, _) => n == c) with + | some (_, p) => p + | none => none + +/-- Fuel-bounded ancestor chain: `c` followed by every ancestor up to the +root, most-specific first. A name absent from `T` returns just itself (the +FFI-cap base case). -/ +def ancestorsInFuel (T : Table) : Nat → String → List String + | 0, c => [c] + | fuel + 1, c => + match parentIn T c with + | some p => c :: ancestorsInFuel T fuel p + | none => [c] + +/-- `ancestorsIn T c` with fuel `T.length` — adequate for any well-formed +table (proved below: `ancestorsIn_fuel_adequate`). -/ +def ancestorsIn (T : Table) (c : String) : List String := + ancestorsInFuel T T.length c + +/-- Is `parent` an ancestor of, or equal to, `child` in `T`? -/ +def subsumesIn (T : Table) (parent child : String) : Bool := + (ancestorsIn T child).contains parent + +/-- Drop any cap subsumed by another cap present, preserving relative order +of survivors. -/ +def normalizeIn (T : Table) (caps : List String) : List String := + caps.filter (fun c => !caps.any (fun other => other != c && subsumesIn T other c)) + +/-- Is `used` covered by some declared cap, via subsumption? The abstract +form of `CapCheck.covered` (bridged in P2). -/ +def coveredIn (T : Table) (declared : List String) (used : String) : Bool := + declared.any (fun need => subsumesIn T need used) + +end MarchLean.Calculus +``` + +- [ ] **Step 2: Refactor `MarchLean/CapLattice.lean`** + +Add `import MarchLean.Calculus.Lattice` at the top (before the module docstring's `/-!` block — imports must precede it). Keep the module docstring and `hierarchy` (retyped as `Table`, same literal). Replace the four operation bodies with specializations, keeping every existing docstring: + +```lean +def hierarchy : MarchLean.Calculus.Table := + [ ("IO", none), ... ] -- the existing 20-entry literal, character for character + +def capParent (c : String) : Option String := + MarchLean.Calculus.parentIn hierarchy c + +def capAncestorsFuel (fuel : Nat) (c : String) : List String := + MarchLean.Calculus.ancestorsInFuel hierarchy fuel c + +def capAncestors (c : String) : List String := + MarchLean.Calculus.ancestorsIn hierarchy c + +def capSubsumes (parent child : String) : Bool := + MarchLean.Calculus.subsumesIn hierarchy parent child + +def normalize (caps : List String) : List String := + MarchLean.Calculus.normalizeIn hierarchy caps +``` + +Signature care: today's `capAncestorsFuel` is `Nat → String → List String` by pattern-matching equations; the specialization above has the same type. `capAncestors` must remain `ancestorsInFuel` at fuel `hierarchy.length` — `ancestorsIn hierarchy` is exactly that. Leave the `#eval` pin block at the bottom of the file untouched. + +- [ ] **Step 3: Wire the import and build** + +`MarchLean.lean`: add `import MarchLean.Calculus.Lattice` (before `import MarchLean.CapLattice`, matching dependency order). +Run: `export PATH="$HOME/.elan/bin:$PATH" && lake build 2>&1 | tail -3` +Expected: clean build. The `#eval` pins in `CapLattice.lean` print during elaboration — eyeball that the printed values still match their `-- expect` comments (reflexivity true, siblings false, `capAncestors "LibC" = ["LibC"]`, etc.). + +- [ ] **Step 4: Behavior-preservation check — corpus re-run must be byte-identical to baseline** + +```bash +export PATH="$HOME/.elan/bin:$PATH" && cd "$(git rev-parse --show-toplevel)" && \ +lake build march-lean-check && \ +MARCH_BIN="$HOME/.opam/march/bin/march" \ +CORPUS_DIR="$HOME/code/march/specs/lang/types" \ +MARCH_LEAN_CHECK_BIN=.lake/build/bin/march-lean-check \ +scripts/conformance-harness.sh > /tmp/p0-corpus-after-task3.txt 2>&1; \ +echo "exit=$?" >> /tmp/p0-corpus-after-task3.txt; \ +diff /tmp/p0-corpus-baseline.txt /tmp/p0-corpus-after-task3.txt && echo IDENTICAL +``` + +Expected: `IDENTICAL`. Any diff at all = the refactor changed behavior — STOP, find the divergence (it is a bug in the refactor or a genuine finding; do not proceed with a diff). + +- [ ] **Step 5: Commit** + +```bash +git add MarchLean/Calculus/Lattice.lean MarchLean/CapLattice.lean MarchLean.lean +git commit -m "refactor(calculus): parameterize the cap lattice over an abstract table (P0b) + +API-preserving: capParent/capAncestorsFuel/capAncestors/capSubsumes/ +normalize become specializations of Calculus.parentIn/ancestorsInFuel/ +ancestorsIn/subsumesIn/normalizeIn at the unchanged 20-entry hierarchy. +Conformance output verified byte-identical against the local corpus." +``` + +--- + +### Task 4: Well-formedness + fuel adequacy + chain shape + +**Files:** +- Modify: `MarchLean/Calculus/Lattice.lean` (append defs + theorems) + +**Interfaces:** +- Consumes: Task 3's defs. +- Produces (namespace `MarchLean.Calculus`): + - `def namesOf (T : Table) : List String` (= `T.map (·.1)`) + - `def nodupNamesB : Table → Bool` + - `def parentClosedB (T : Table) : Bool` + - `def reachesRoot (T : Table) : Nat → String → Bool` + - `def WellFormedB (T : Table) : Bool` (conjunction of the three) + - `theorem ancestorsInFuel_head (T fuel c) : (ancestorsInFuel T fuel c).head? = some c` + - `theorem self_mem_ancestorsIn (T c) : c ∈ ancestorsIn T c` + - `theorem subsumesIn_refl (T c) : subsumesIn T c c = true` + - `theorem parentIn_eq_none_of_not_mem {T c} (h : c ∉ namesOf T) : parentIn T c = none` + - `theorem reachesRoot_mono {T c fuel fuel'} (h : fuel ≤ fuel') : reachesRoot T fuel c = true → reachesRoot T fuel' c = true` + - `theorem ancestorsInFuel_stable {T c fuel} (h : reachesRoot T fuel c = true) {f} (hf : fuel ≤ f) : ancestorsInFuel T f c = ancestorsInFuel T fuel c` + - `theorem wf_reachesRoot {T} (wf : WellFormedB T = true) (c : String) : reachesRoot T T.length c = true` + - `theorem ancestorsIn_fuel_adequate {T} (wf : WellFormedB T = true) {f} (hf : T.length ≤ f) (c) : ancestorsInFuel T f c = ancestorsIn T c` + - `theorem ancestorsIn_root {T c} (h : parentIn T c = none) : ancestorsIn T c = [c]` + - `theorem ancestorsIn_cons {T} (wf : WellFormedB T = true) {c p} (h : parentIn T c = some p) : ancestorsIn T c = c :: ancestorsIn T p` + +- [ ] **Step 1: Append the defs** + +```lean +/-- The names (first components) of a table. -/ +def namesOf (T : Table) : List String := T.map (·.1) + +/-- No two rows share a name (Boolean, so `decide` can discharge it). -/ +def nodupNamesB : Table → Bool + | [] => true + | (n, _) :: rest => !rest.any (fun (m, _) => m == n) && nodupNamesB rest + +/-- Every parent value that occurs is itself a row's name. march's real +table satisfies this; FFI caps are absent from the table entirely, never +dangling parents. -/ +def parentClosedB (T : Table) : Bool := + T.all (fun (_, p?) => match p? with + | none => true + | some p => T.any (fun (n, _) => n == p)) + +/-- Does the parent chain from `c` reach a parentless node within `fuel` +steps? The acyclicity witness: in a well-formed table every name does so +within `T.length` steps. -/ +def reachesRoot (T : Table) : Nat → String → Bool + | 0, c => (parentIn T c).isNone + | fuel + 1, c => + match parentIn T c with + | none => true + | some p => reachesRoot T fuel p + +/-- Well-formed table: unique names, closed parents, acyclic. This is what +`CapLattice.lean`'s old prose comment ("the table is a finite forest with no +cycles, so `hierarchy.length` is a safe fuel bound") asserted; here it is a +decidable proposition, discharged for the real table in `Concrete.lean`. -/ +def WellFormedB (T : Table) : Bool := + nodupNamesB T && parentClosedB T && T.all (fun (n, _) => reachesRoot T T.length n) +``` + +- [ ] **Step 2: State all ten theorems with `sorry`, build, count warnings = 10** + +Statements exactly as in the Interfaces block above. + +- [ ] **Step 3: Prove, easiest first** + +- `ancestorsInFuel_head`: `cases fuel` then `simp [ancestorsInFuel]`; in the successor case `cases h : parentIn T c <;> simp [h]`. +- `self_mem_ancestorsIn` / `subsumesIn_refl`: from `head?` = some via `List.head?_eq_some`-style reasoning (`ancestorsIn` is nonempty with head `c`; `List.contains` of the head is true — `simp [subsumesIn, List.contains]` plus `self_mem_ancestorsIn`). +- `parentIn_eq_none_of_not_mem`: `parentIn` is a `find?`; if it returned `some`, `List.find?_some`/`List.mem_of_find?_eq_some` puts a row with name `c` in `T` (the predicate is `n == c`), contradicting `h` via `namesOf` membership. +- `reachesRoot_mono`: induction on `fuel` generalizing `c` and `fuel'`; case on `parentIn T c`. Note the base case needs `parentIn = none → reachesRoot _ anything = true` — split out as a private helper if the induction gets awkward. +- `ancestorsInFuel_stable`: induction on `fuel` generalizing `c f`; base `fuel = 0` has `(parentIn T c).isNone = true`, so every fuel value returns `[c]`; successor case: if `parentIn T c = none` both sides are `[c]`; if `some p`, peel one constructor off both sides (`f = f' + 1` exists since `f ≥ fuel + 1 ≥ 1`) and apply the IH at `p`. +- `wf_reachesRoot`: split `wf` into its three conjuncts (`Bool.and_eq_true`). Case on `c ∈ namesOf T`: if absent, `parentIn_eq_none_of_not_mem` makes `reachesRoot` true at any fuel (case on `T.length`); if present, `List.mem_map` gives a row `(c, p?) ∈ T` and the third conjunct (`List.all_eq_true`) applied to that row is exactly the goal. +- `ancestorsIn_fuel_adequate`: `ancestorsInFuel_stable` with `wf_reachesRoot`. +- `ancestorsIn_root`: unfold `ancestorsIn`; `cases T.length <;> simp [ancestorsInFuel, h]`. +- `ancestorsIn_cons`: from `h`, `c` is a row name so `T ≠ []`, hence `T.length = k + 1`; unfold one `ancestorsInFuel` step to get `c :: ancestorsInFuel T k p`; `wf_reachesRoot c` at fuel `k + 1` reduces through `h` to `reachesRoot T k p`; `ancestorsInFuel_stable` (with `k ≤ T.length`) rewrites `ancestorsInFuel T k p` to `ancestorsIn T p`. + +Iterate each until green before starting the next — later proofs in this task use earlier lemmas. + +- [ ] **Step 4: Build clean (0 sorries), commit** + +```bash +git add MarchLean/Calculus/Lattice.lean +git commit -m "feat(calculus): table well-formedness, fuel adequacy, ancestor chain shape (P0b) + +WellFormedB (nodup names + closed parents + acyclic) is decidable; fuel +hierarchy.length is proved adequate — the old 'safe bound' prose comment +is now the theorem ancestorsIn_fuel_adequate." +``` + +--- + +### Task 5: Order theorems — suffix, transitivity, antisymmetry, siblings, FFI isolation + +**Files:** +- Modify: `MarchLean/Calculus/Lattice.lean` (append) + +**Interfaces:** +- Consumes: Task 4's lemmas (esp. `ancestorsIn_cons`, `ancestorsIn_root`, `self_mem_ancestorsIn`, `wf_reachesRoot`). +- Produces (namespace `MarchLean.Calculus`): + - `theorem mem_ancestorsIn_suffix {T} (wf : WellFormedB T = true) {p c} (h : p ∈ ancestorsIn T c) : ancestorsIn T p <:+ ancestorsIn T c` + - `theorem subsumesIn_trans {T} (wf : WellFormedB T = true) {a b c} : subsumesIn T a b = true → subsumesIn T b c = true → subsumesIn T a c = true` + - `theorem subsumesIn_antisymm {T} (wf : WellFormedB T = true) {p c} : subsumesIn T p c = true → subsumesIn T c p = true → p = c` + - `theorem no_self_parent {T} (wf : WellFormedB T = true) {p} : parentIn T p ≠ some p` + - `theorem siblings_incomparable {T} (wf : WellFormedB T = true) {p c q} (hp : parentIn T p = some q) (hc : parentIn T c = some q) (hne : p ≠ c) : subsumesIn T p c = false` + - `theorem subsumesIn_of_absent {T c p} (h : parentIn T c = none) : subsumesIn T p c = true ↔ p = c` + - `theorem mem_ancestorsIn_names {T} (wf : WellFormedB T = true) {a x} (h : a ∈ ancestorsIn T x) : a = x ∨ a ∈ namesOf T` + - `theorem absent_subsumesIn {T} (wf : WellFormedB T = true) {c x} (hc : c ∉ namesOf T) (h : subsumesIn T c x = true) : x = c` + +- [ ] **Step 1: State all eight with `sorry`; build; count = 8** + +- [ ] **Step 2: Prove `mem_ancestorsIn_suffix`** — the workhorse. Strong induction on `(ancestorsIn T c).length`, unfolding the chain with Task 4's shape lemmas: + +Skeleton (iterate until green; the structure is the contract, the tactic details are not): + +```lean +theorem mem_ancestorsIn_suffix {T} (wf : WellFormedB T = true) {p c} + (h : p ∈ ancestorsIn T c) : ancestorsIn T p <:+ ancestorsIn T c := by + induction hn : (ancestorsIn T c).length using Nat.strong_induction_on + generalizing c with + | _ n ih => + by_cases hpc : p = c + · subst hpc; exact List.suffix_refl _ + · cases hpar : parentIn T c with + | none => + rw [ancestorsIn_root hpar] at h + simp at h; exact absurd h hpc + | some q => + rw [ancestorsIn_cons wf hpar] at h ⊢ + rcases List.mem_cons.mp h with rfl | hq + · exact absurd rfl hpc + · exact (ih _ (by rw [ancestorsIn_cons wf hpar, hn ▸ rfl] ...) hq rfl).trans + (List.suffix_cons _ _) +``` + +The measure argument: `ancestorsIn_cons` makes `(ancestorsIn T q).length = n - 1 < n`. Wire the `<` fact through however `Nat.strong_induction_on`'s motive wants it (an explicit `have hlt : (ancestorsIn T q).length < n` from `hn` and the cons equation, then `ih _ hlt`). If `Nat.strong_induction_on` fights, an equivalent formulation is a `termination_by`-measured recursive theorem or well-founded `induction … using` variant — any of these is acceptable; the statement may not change. + +- [ ] **Step 3: Prove the consequences** + +- `subsumesIn_trans`: `subsumesIn x y = true ↔ x ∈ ancestorsIn T y` (a `simp [subsumesIn, List.contains]`-style bridge — extract it as a private lemma `subsumesIn_iff_mem`, it gets used everywhere). Then `mem_ancestorsIn_suffix wf h₂` is a suffix, and `(·.subset)` (`List.IsSuffix.subset`) maps `a ∈ ancestorsIn T b` into `ancestorsIn T c`'s membership. +- `subsumesIn_antisymm`: two applications of `mem_ancestorsIn_suffix` give mutual suffixes; `List.IsSuffix.length_le` both ways + `Nat.le_antisymm` give equal lengths; a mutual suffix of equal length forces list equality (prove inline: `l₁ <:+ l₂` means `∃ t, t ++ l₁ = l₂`; equal lengths force `t = []` by `List.length_append` arithmetic); equal lists have equal `head?`, and `ancestorsInFuel_head` turns `some p = some c` into `p = c`. +- `no_self_parent`: intro `hp : parentIn T p = some p`. Private helper: `reachesRoot T f p = false` for every `f` by induction on `f` (base: `hp` makes `isNone` false; step: `hp` reduces to the IH). Contradict `wf_reachesRoot wf p`. +- `siblings_incomparable`: by contradiction from `subsumesIn T p c = true`: `ancestorsIn_cons wf hc` puts `p ∈ c :: ancestorsIn T q`; `p ≠ c` leaves `p ∈ ancestorsIn T q`, which by `subsumesIn_iff_mem` (direction: `x ∈ ancestorsIn T y ↔ subsumesIn T x y = true` — x is the *subsumer*) is `subsumesIn T p q = true`. Symmetrically, `ancestorsIn_cons wf hp` plus `self_mem_ancestorsIn T q` puts `q ∈ ancestorsIn T p`, i.e. `subsumesIn T q p = true`. Antisymmetry on the pair gives `p = q`; rewriting `hp` yields `parentIn T p = some p`; contradict `no_self_parent`. +- `subsumesIn_of_absent`: rewrite with `ancestorsIn_root h`; membership in `[c]` is equality. +- `mem_ancestorsIn_names`: same strong-induction skeleton as `mem_ancestorsIn_suffix` (chain unfold via `ancestorsIn_cons`); in the `some q` case, `q ∈ namesOf T` comes from `parentClosedB` (the second `wf` conjunct: the row that made `parentIn T x = some q` has parent value `q`, and closure finds a row named `q`). Extract `parentIn_some_mem_names {T} (wf) : parentIn T x = some q → q ∈ namesOf T` as a private helper. +- `absent_subsumesIn`: `subsumesIn_iff_mem` + `mem_ancestorsIn_names wf`; the `∈ namesOf` disjunct contradicts `hc`, leaving `c = x`. + +- [ ] **Step 4: Build clean, commit** + +```bash +git add MarchLean/Calculus/Lattice.lean +git commit -m "feat(calculus): subsumption is a partial order — suffix lemma, trans, antisymm, sibling incomparability, FFI isolation (P0b)" +``` + +--- + +### Task 6: `coveredIn` / `normalizeIn` theorems + +**Files:** +- Modify: `MarchLean/Calculus/Lattice.lean` (append) + +**Interfaces:** +- Consumes: Tasks 4-5 (esp. `subsumesIn_trans`, `subsumesIn_antisymm`, `mem_ancestorsIn_suffix`, `subsumesIn_iff_mem`). +- Produces (namespace `MarchLean.Calculus`; P2's normalize-stability and monotonicity theorems consume the last three): + - `theorem coveredIn_mono {T L L' c} (hsub : ∀ x ∈ L, x ∈ L') (h : coveredIn T L c = true) : coveredIn T L' c = true` + - `theorem coveredIn_of_subsumes {T p c} (h : subsumesIn T p c = true) : coveredIn T [p] c = true` + - `theorem normalizeIn_subset (T : Table) (L : List String) : ∀ x ∈ normalizeIn T L, x ∈ L` + - `theorem ancestors_length_lt {T} (wf : WellFormedB T = true) {p c} (hmem : p ∈ ancestorsIn T c) (hne : p ≠ c) : (ancestorsIn T p).length < (ancestorsIn T c).length` + - `theorem exists_survivor {T} (wf : WellFormedB T = true) {L need} (hmem : need ∈ L) : ∃ m ∈ normalizeIn T L, subsumesIn T m need = true` + - `theorem coveredIn_normalizeIn {T} (wf : WellFormedB T = true) (L : List String) (c : String) : coveredIn T (normalizeIn T L) c = coveredIn T L c` + - `theorem normalizeIn_idem (T : Table) (L : List String) : normalizeIn T (normalizeIn T L) = normalizeIn T L` + +- [ ] **Step 1: State all seven with `sorry`; build; count = 7** + +- [ ] **Step 2: Prove the easy four** + +- `coveredIn_mono`: `coveredIn` is `List.any`; `List.any_eq_true` both ways, move the witness through `hsub`. +- `coveredIn_of_subsumes`: `simp [coveredIn, h]`. +- `normalizeIn_subset`: `normalizeIn` is a `filter`; `List.mem_filter.mp`. +- `ancestors_length_lt`: `mem_ancestorsIn_suffix wf hmem` gives `≤` via `List.IsSuffix.length_le`; if lengths were equal the suffix is the whole list (same inline argument as in `subsumesIn_antisymm` — if it was extracted as a private lemma there, reuse it), so heads give `p = c` contradicting `hne`; hence strict. + +- [ ] **Step 3: Prove `exists_survivor`** — the descent argument. Strong induction on `(ancestorsIn T need).length`: + +If `need ∈ normalizeIn T L`: witness `need`, `subsumesIn_refl`. Otherwise `List.mem_filter` says the filter predicate was false: `¬¬(L.any (fun other => other != need && subsumesIn T other need))`, i.e. some `other ∈ L`, `other ≠ need`, `subsumesIn T other need = true`. Then `other ∈ ancestorsIn T need` (`subsumesIn_iff_mem`) and `ancestors_length_lt wf … hne'` (with `hne' : other ≠ need`) gives the measure drop; the IH at `other` yields `m ∈ normalizeIn T L` with `subsumesIn T m other`; `subsumesIn_trans wf` composes it to `need`. Beware Bool/Prop plumbing on the filter predicate (`Bool.not_eq_true`, `bne_iff_ne`, `List.any_eq_true`) — mechanical, iterate until green. + +- [ ] **Step 4: Prove the two headline theorems** + +- `coveredIn_normalizeIn`: prove Bool equality by `Bool.eq_iff_iff`-style case split or two implications: (←, i.e. `coveredIn T L c → coveredIn T (normalizeIn T L) c`): from the covering witness `need ∈ L`, `exists_survivor` gives `m` surviving with `subsumesIn T m need`; `subsumesIn_trans` reaches `c`; `List.any_eq_true` re-packages. (→): `coveredIn_mono (normalizeIn_subset T L)`. +- `normalizeIn_idem`: show the second filter keeps every survivor: for `s ∈ normalizeIn T L`, a dropper `other ∈ normalizeIn T L` with `other ≠ s ∧ subsumesIn T other s` would, via `normalizeIn_subset`, be a dropper in the FIRST round, contradicting `s`'s survival. Implement as `List.filter_eq_self`-style (if that core lemma name doesn't resolve, prove by `List.filter` induction inline). Note this needs no `wf`. + +- [ ] **Step 5: Build clean, commit** + +```bash +git add MarchLean/Calculus/Lattice.lean +git commit -m "feat(calculus): normalize is idempotent and coverage-preserving; covered is monotone (P0b)" +``` + +--- + +### Task 7: `Calculus/Concrete.lean` — the 20-entry table discharged, shipping-name corollaries + +**Files:** +- Create: `MarchLean/Calculus/Concrete.lean` +- Modify: `MarchLean.lean` (add `import MarchLean.Calculus.Concrete` after the CapLattice import) + +**Interfaces:** +- Consumes: everything from Tasks 3-6; `MarchLean.CapLattice` (`hierarchy`, `capParent`, `capAncestors`, `capAncestorsFuel`, `capSubsumes`, `normalize`). +- Produces (namespace `MarchLean.Calculus.Concrete`; P2 consumes these): + - `theorem hierarchy_wellFormed : WellFormedB hierarchy = true` + - `theorem capSubsumes_refl (c : String) : capSubsumes c c = true` + - `theorem capSubsumes_trans {a b c} : capSubsumes a b = true → capSubsumes b c = true → capSubsumes a c = true` + - `theorem capSubsumes_antisymm {p c} : capSubsumes p c = true → capSubsumes c p = true → p = c` + - `theorem capSiblings_incomparable {p c q} : capParent p = some q → capParent c = some q → p ≠ c → capSubsumes p c = false` + - `theorem capAncestors_fuel_adequate {f} (hf : hierarchy.length ≤ f) (c) : capAncestorsFuel f c = capAncestors c` + - `theorem normalize_covered (L c) : coveredIn hierarchy (normalize L) c = coveredIn hierarchy L c` + - `theorem normalize_idem (L) : normalize (normalize L) = normalize L` + +- [ ] **Step 1: Create the file** + +```lean +/-! +# The shipping lattice, discharged + +`WellFormedB hierarchy` by kernel `decide` (measured ~0.5s on this +toolchain), then every abstract theorem instantiated at the shipping 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. +-/ +import MarchLean.CapLattice + +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 + +-- The FFI base case, now consequences of theorems rather than #eval pins: +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 +``` + +Term-mode friction note: `capSubsumes` etc. are *definitionally* `subsumesIn hierarchy` etc. (Task 3 made them so), so the abstract theorems apply directly. If the elaborator balks, `show subsumesIn hierarchy …` or `unfold capSubsumes` first. If `decide` on `hierarchy_wellFormed` exceeds heartbeats (unlikely — probe measured ~0.5s), add `set_option maxHeartbeats 1000000 in`; do NOT switch to `native_decide` without trying that. + +- [ ] **Step 2: Build clean** (`lake build`, 0 sorries, no warnings). + +- [ ] **Step 3: Negative control — verify the discharge actually guards.** Temporarily add a cycle row `("X.Cycle", some "X.Cycle")` to `hierarchy`, run `lake build`, and confirm `hierarchy_wellFormed`'s `decide` FAILS. Revert the row, rebuild green. (Analogue of the repo's forced-relaxation tests: proves the guard is load-bearing, not vacuous.) Do not commit the broken state. + +- [ ] **Step 4: Commit** + +```bash +git add MarchLean/Calculus/Concrete.lean MarchLean.lean +git commit -m "feat(calculus): WellFormedB hierarchy by decide; lattice metatheory instantiated at shipping names (P0b) + +Negative control verified: a self-parent row added to hierarchy fails the +decide at build time, then reverted." +``` + +--- + +### Task 8: CI sorry-guard + final verification + +**Files:** +- Modify: `.github/workflows/` conformance workflow (the single YAML in that directory — add one step after the Lean build step) + +**Interfaces:** +- Consumes: all prior tasks. +- Produces: CI fails on any committed `sorry`/`admit`; P0 done. + +- [ ] **Step 1: Add the guard step** (after the `leanprover/lean-action` build step, before the harness run): + +```yaml + # Lean treats `sorry` as a WARNING, not an error, so `lake build` + # alone 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 the 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 +``` + +- [ ] **Step 2: Verify the guard logic locally** + +Run the same grep in the repo — expected: no matches, exit 1 from grep (so the `if` takes the else path). Then `echo 'example : True := by sorry' >> /tmp/guardcheck.lean` is NOT needed — instead verify positively: `grep -rnE '\b(sorry|admit)\b' --include='*.lean' MarchLean/ MarchLean.lean MarchLeanCheck.lean; echo "grep_exit=$?"` — expected `grep_exit=1` (no matches). + +- [ ] **Step 3: Final full verification** + +```bash +export PATH="$HOME/.elan/bin:$PATH" && cd "$(git rev-parse --show-toplevel)" && \ +lake build && lake build march-lean-check && \ +MARCH_BIN="$HOME/.opam/march/bin/march" \ +CORPUS_DIR="$HOME/code/march/specs/lang/types" \ +MARCH_LEAN_CHECK_BIN=.lake/build/bin/march-lean-check \ +scripts/conformance-harness.sh > /tmp/p0-corpus-final.txt 2>&1; \ +echo "exit=$?" >> /tmp/p0-corpus-final.txt; \ +diff /tmp/p0-corpus-baseline.txt /tmp/p0-corpus-final.txt && echo IDENTICAL +``` + +Expected: clean build, `IDENTICAL`. + +- [ ] **Step 4: Commit** + +```bash +git add .github/workflows/ +git commit -m "ci: fail on sorry/admit in Lean sources — the proof layer is only evidence if this gate holds (P0)" +``` + +--- + +## Out of scope for this plan (later plans) + +- **P1** (de-partialize the 18 walks in `Syntax.lean`/`CapCheck.lean` with legacy-equivalence pins) — planned after P0 lands, against the then-current definitions. +- **P2** (whole-checker theorem/counterexample pairs; bridges `CapCheck.covered` to `coveredIn hierarchy`) — requires P1. +- Migrating existing `native_decide` pins to `decide` — a P1 concern (it needs the de-partialized definitions). diff --git a/specs/plans/2026-08-08-calculus-proof-capabilities-design.md b/specs/plans/2026-08-08-calculus-proof-capabilities-design.md new file mode 100644 index 0000000..9ebb72b --- /dev/null +++ b/specs/plans/2026-08-08-calculus-proof-capabilities-design.md @@ -0,0 +1,266 @@ +# Proof calculus for the capability checker (design) + +> Parent design docs: `specs/plans/2026-07-23-a3-capability-lattice-design.md` +> (the checker this calculus is about), and transitively the A1/A2 docs it +> cites. +> +> This is a **design doc**, not an implementation plan. Implementation plans +> follow via `writing-plans`, one per phase (§6). +> +> Authoritative sources for every claim about current behavior: +> `MarchLean/CapLattice.lean`, `MarchLean/CapCheck.lean`, +> `MarchLean/Syntax.lean`, at the SHA this doc is committed at. + +## 0. What this is + +`march-lean` currently contains **zero theorems**. Validation is three-layered +— 112 `native_decide` pins, `#eval` expectations, and the 242-file +conformance corpus — and all three are *testing*: they check points, not +properties. The project's own findings log shows why that matters: every +major defect found so far hid behind a plausible comment asserting a property +nobody checked ("safe to ignore", "safe bound", "read by"). + +This milestone adds a **proof layer**: machine-checked theorems about the +capability checker's algebraic core, proved in the same Lean codebase and +kernel-checked by the same `lake build` CI already runs. Scope decision, +stated up front: this is **metatheory of what exists** — properties of the +checker's own definitions — not an operational semantics for march programs, +not a soundness theorem about march, and not a spec-vs-implementation +refinement argument. Those are possible later stages; none is prerequisite +for this one and none is smuggled in. + +## 1. Design decisions + +1. **Metatheory of the shipping code, not a shadow model.** The theorems are + about the very definitions `march-lean-check` executes. A clean-room model + would be easier to prove things about, but its theorems would attach to + the model, and the gap between model and shipping code is exactly the kind + of untested "surely equivalent" claim this project exists to distrust. + +2. **No mathlib.** Everything proved here lives in `List String`, `Bool`, and + small inductives. The repo is a zero-dependency oracle whose CI builds + from a cold toolchain on every push; mathlib would dominate that build for + lemmas (`List.Perm`, `foldl` algebra) that are cheap to state and prove + directly. + +3. **Parameterize the lattice over an abstract table.** `capParent` / + `capAncestors` / `capSubsumes` / `normalize` generalize over a + `(name, parent)` table argument; the shipping `CapLattice` API is the + specialization to `hierarchy`, signature-for-signature. The metatheory is + proved once for **any well-formed table** and the concrete table's + well-formedness is discharged by `decide`. Consequences: (a) when march + adds a capability, only the `decide` re-runs — no theorem is touched; + (b) if march ever ships a cycle or a duplicate name, the build fails at + the discharge, loudly — converting `CapLattice.lean:54`'s prose claim + ("the table is a finite forest with no cycles") into a checked invariant; + (c) transitivity/antisymmetry are structural inductions over the ancestor + chain instead of a large kernel computation over concrete strings. + +4. **De-partialization is a prerequisite, done with a runtime safety net.** + Lean gives `partial def` no equation lemmas: the 18 `partial def` tree + walks can be neither inducted on nor `decide`d (which is precisely why the + 112 existing pins say `native_decide`). All 18 become total. A + `partial ≡ total` equivalence is not provable (the partial side is opaque + to the kernel), but both sides *run*: each conversion keeps the old body + as `…Legacy`, pins `legacy x = total x` by `native_decide` across every + existing fixture, passes the full 242-file corpus, and deletes the legacy + in the same PR. Any divergence the pins catch is a finding about the walk, + per the project's standing rule that green corpus runs are weak evidence. + +5. **Theorem-driven, bottom-up sequencing.** Work is ordered by theorem; each + theorem names the definitions it needs, and only those are converted in + that slice. Proof value lands from the first phase; every shipping-code + change is separately corpus-validated; no big-bang diff. + +6. **Boundary failures are stated, not hand-waved.** All three whole-checker + properties chosen for this milestone are **false for the full checker and + true for its subsumption-coverage core** (§5) — the boundary is the + behavioral-cap layer every time. Each lands as a *pair*: a theorem scoped + to the coverage core, plus a machine-checked counterexample (`example : + … := by native_decide` or `decide`) pinning exactly where and why the full + checker breaks the law. The counterexamples are first-class deliverables: + they turn "behavioral caps are different" from a comment into checked + statements of *how*. + +## 2. Shape + +Four new files under `MarchLean/Calculus/`, imported from `MarchLean.lean` so +the existing CI `lake build` kernel-checks every theorem on every push. One +caveat: `sorry` is a *warning* in Lean, not an error, so a bare `lake build` +would pass with unproven theorems. The one CI edit in this milestone is a +line grepping the build output for `declaration uses 'sorry'` and failing on +a hit. + +``` +MarchLean/Calculus/Lattice.lean -- abstract hierarchy theory (any well-formed table) +MarchLean/Calculus/Concrete.lean -- march's 20-entry table discharged by decide +MarchLean/Calculus/Verdicts.lean -- CapResult / DivVerdict algebra +MarchLean/Calculus/CheckCaps.lean -- whole-checker theorem/counterexample pairs +``` + +Shipping behavior is unchanged throughout: every refactor is API-preserving +(same names, same signatures, same results), and every phase that touches +shipping code re-runs the full conformance harness. + +## 3. The abstract lattice (phase P0b) + +`Calculus/Lattice.lean` defines, over a table `T : List (String × Option +String)`: + +- `parentIn T c`, `ancestorsIn T c` (fuel-bounded as today), `subsumesIn T`, + `normalizeIn T`, `coveredIn T` — the generalizations. `CapLattice`'s + public names become `def capParent := parentIn hierarchy` etc.; every + call site and `#eval` pin compiles unchanged. +- `WellFormed T : Prop` — (i) no duplicate names; (ii) acyclic, stated as a + strictly-decreasing depth measure on parent chains (equivalently: every + chain reaches a root in ≤ `T.length` steps, which is also exactly the fuel + adequacy claim). + +Theorems, for any `T` with `WellFormed T`: + +| theorem | content | replaces | +|---|---|---| +| `ancestors_head` | `ancestorsIn T c` begins with `c` | reflexivity pins | +| `ancestors_chain` | each element's successor is its parent | prose at `CapLattice.lean:46-56` | +| `ancestors_fuel_adequate` | fuel `T.length` never truncates | prose "safe bound" claim | +| `subsumes_refl` / `subsumes_trans` / `subsumes_antisymm` | partial order | sibling/directionality pins | +| `siblings_incomparable` | distinct children of one parent never subsume each other | reject/t38-shaped pins | +| `absent_name_isolated` | a name ∉ T subsumes and is subsumed by only itself | FFI/LibC pins | +| `normalize_idempotent` | `normalizeIn T (normalizeIn T L) = normalizeIn T L` | — (new) | +| `normalize_covered` | `coveredIn T L c ↔ coveredIn T (normalizeIn T L) c` | — (new; **the** lemma licensing `normalize`, and the one that dies without antisymmetry) | +| `covered_mono` | `L ⊆ L' → coveredIn T L c → coveredIn T L' c` | — (new; feeds §5 monotonicity) | +| `covered_upward` | `subsumesIn T p c → coveredIn T [p] c` | root-covers-child pins | + +`Calculus/Concrete.lean` proves `WellFormed hierarchy` by `decide` and +instantiates the table above for the shipping lattice. The existing `#eval` +pins in `CapLattice.lean` stay (they are documentation-by-example and cost +nothing); the theorems supersede them as evidence. + +## 4. Verdict algebra (phase P0a) and de-partialization (phase P1) + +**P0a — `Calculus/Verdicts.lean`, purely additive, lands first.** +`CapResult.andThen`: associative; `ok` two-sided identity; `violation` +left-absorbing; and the tier projection `tier : CapResult → Tier` (`ok < +skip < violation`) is a homomorphism onto max — i.e. messages depend on +order (leftmost-wins, by design), tiers never do. `DivVerdict.join`: +commutative, associative, idempotent, `safe` identity, `divZero` absorbing; +hence `joinAll` is permutation-invariant (needed by §5's order-independence). + +**P1 — all 18 `partial def` walks in the two capability files become +total.** They are `partial` only because Lean's structural-recursion checker +doesn't see descent through `List.any`/`List.map`/`flatMap`; the conversions +are the standard nested-recursion idiom (or `termination_by` on term size) — +no well-founded measure beyond structural size is expected anywhere. +Inventory: `Syntax.lean` — `Ty.hasUnsupported`, `Ty.beq`, +`Pattern.hasUnsupported`, `Term.hasUnsupported`, `Decl.hasUnsupported`, +`flattenDecls` (6); `CapCheck.lean` — `capsInTy`, `bodyCalls`, +`bodyAllocates`, `patBinderNames`, `termMentionsAny`, `divisionVerdict`, +`orExpansionSize`, `isCatchAllPattern`, `isModeledArmPattern`, +`patCoveredCtors`, `matchesIn`, `checkDecls` (12). The `partial def`s in +`Elab`/`Infer`/`Compare`/`Result`/`Linearity` are **out of scope**: they +serve inference, which this milestone proves nothing about, so converting +them buys no theorem. + +Migration per function (or tight function group): add total definition → +rename old to `…Legacy` → `native_decide` pins `legacy = total` on every +existing fixture in the repo → full corpus run → delete legacy, same PR. + +Secondary payoff: existing `native_decide` tests over converted functions +migrate to `decide`/`rfl` where kernel reduction is acceptably fast, closing +the trusted-native-evaluator hole for those sites; where `brecOn` reduction +is too slow, the pin stays `native_decide` with a one-line note. No theorem +depends on this migration. + +## 5. Whole-checker theorems (phase P2) + +Pressure-testing the candidate properties against the code shows all three +are **false for the full checker, true for its coverage core** — the +boundary is behavioral caps in every case. Each therefore lands as a +theorem/counterexample pair. "Coverage core" means the subsumption-coverage +checks (Check 1 signatures, Check 4 transitive use, Check 5 extern) — the +part of `checkOneModule` whose only cap reasoning is `covered declared c`. + +1. **Tier order-independence.** Full permutation invariance is *known false + by design*: behavioral-cap inheritance into nested modules is positional + (commit `a647ad1`, march-faithful — a `dopts` before vs. after a nested + `dmod` means different inherited caps). Pair: + - theorem: `tier (checkCaps m)` is invariant under permutations of each + module's decl list that preserve the relative order of `dopts` and + `dmod` declarations (message may change; tier may not); + - counterexample: a two-decl module (`dopts` + `dmod`) whose permutation + flips the tier. + Risk flag (deliberate): the restriction may need further narrowing once + proved against the real `checkDecls`; every narrowing found is documented + in the theorem statement as a discovered semantic dependency, never + absorbed silently. If a narrowing is needed that is *not* march-faithful, + that is a finding and goes to `specs/march-findings.md` instead. + +2. **Normalize-stability.** Pair: + - theorem: replacing `needs L` with `needs (normalize L)` preserves the + verdict of the coverage core (direct corollary of `normalize_covered` + threaded through `checkOneModule`'s Check 1/4/5 arms); + - counterexample: `normalize ["IO", "IO.Foreign"] = ["IO"]` flips + `hasForeignNeed`, so under `opts no_extern` the un-normalized module + violates and the normalized one does not (`CapCheck.lean`'s + `noExternWithForeignNeed` fixture shape). Normalization is **not** a + verdict-preserving operation on full modules, and nothing in the + checker may ever apply it as if it were. + +3. **IO-cap monotonicity.** Pair: + - theorem: adding a cap to `needs` never flips the coverage core from + accept to reject (corollary of `covered_mono`); + - counterexample: adding `needs IO.Foreign` under `opts no_extern` *is* + the violation — declaring a capability is itself observable behavior at + the behavioral layer. + +Determinism and totality of `checkCaps` come free once P1 lands (a Lean +`def` is total and deterministic by construction) — recorded as one-line +remarks in `Calculus/CheckCaps.lean`, not padded into theorems. + +## 6. Sequencing, validation, deliverables + +| phase | content | shipping-code risk | gate | +|---|---|---|---| +| P0a | verdict algebra | none (additive) | `lake build` | +| P0b | lattice parameterization + metatheory + `decide` discharge | API-preserving refactor of `CapLattice.lean` | build + full corpus | +| P1 | de-partialize the 18 walks, legacy-equivalence pins | largest — `Syntax.lean` + `CapCheck.lean` | build + corpus per function group | +| P2 | three theorem/counterexample pairs | none (additive) | build | + +Each phase is one PR. P0a and P0b are independent of P1 and land first; P2 +requires P1. Implementation plans (via `writing-plans`): one per phase, P0a +and P0b possibly combined if the lattice refactor stays as small as +expected. + +The march repo is untouched; no emitter change, no CI-pin dance. The one CI +edit is the `sorry`-grep line (§2). + +## 7. Risks + +- **A P1 conversion could be subtly non-equivalent.** Mitigated by the + legacy pins + corpus; a caught divergence is a finding about the walk, not + a nuisance. Residual risk: both legacy and total agree on all fixtures and + corpus but differ on unexercised shapes — accepted; this is still strictly + better evidence than today (where there is one implementation and zero + cross-checks), and P2's theorems then constrain the total version directly. +- **Kernel reduction through `brecOn` may be too slow** for some + `decide`/`rfl` migrations and possibly for `WellFormed hierarchy` by + `decide`. Fallbacks, in order: `simp`-normalization first, `Nat`-indexed + restatement, or `native_decide` for the concrete discharge only (the + abstract theorems are unaffected). No theorem depends on which fallback is + used. +- **The order-independence restriction may narrow further** (§5.1's risk + flag). Handled by documentation-or-finding, never silent absorption. +- **Refactor churn vs. in-flight work.** P0b/P1 touch the two files every + other capability slice also touches; phases are kept small and + fast-merging to limit conflict windows. + +## 8. Explicit non-goals + +- No operational semantics for march programs; no soundness/completeness + theorem relating the checker to program behavior. +- No spec-vs-implementation refinement against march's OCaml. +- No proofs about `Infer`/`Compare`/`Linearity` (their `partial def`s are + not even converted). +- No claim that a proved checker is a *correct* oracle of march — the + warning-tier fidelity gap (A3 design §1.3) is inherited unchanged and + sits outside every theorem here. diff --git a/specs/plans/2026-08-08-march-main-capability-resync.md b/specs/plans/2026-08-08-march-main-capability-resync.md new file mode 100644 index 0000000..0b5d572 --- /dev/null +++ b/specs/plans/2026-08-08-march-main-capability-resync.md @@ -0,0 +1,98 @@ +# march main capability resync (2026-08-08) + +> Not a design doc and not a plan — a record of a slice that was discovered +> rather than planned. It began as "repin CI to march main" and turned into +> five verdict-changing fixes because the old pin was 71 commits stale and the +> local `march` used for ad-hoc checks was staler still (opam 0.2.0). +> +> Pin moved `7c1d701c` -> `6867c783`. Corpus 242 -> 277. + +## 0. Why this exists + +The A-series has bumped the march pin twice before and both times the drift +was inert: the emitter envelope was unchanged and no new ERROR-level check +landed inside the modeled fragment. That history made "bump the pin" feel +like bookkeeping. This bump was not inert. It surfaced **five** corpus-visible +divergences — four of them false ACCEPTS — plus four more that the corpus +cannot see at all. + +The lesson worth keeping: the previous two bumps' inertness was a property of +those diffs, not of pin bumps. march's capability subsystem grew four new +modules (`cap_ceiling`, `cap_scope`, `cap_surface_ty`, `cap_symbols`) and ++1900 lines of `typecheck.ml` in this window. + +Equally important: the local `march` on PATH was 0.2.0, which reported two +MISMATCHes and four CORPUS_VIOLATIONs — all artifacts. A stale binary does not +merely miss findings, it manufactures them. + +## 1. Fixed (corpus-visible) + +| file | direction | cause | fix | +|---|---|---|---| +| `reject/t149_cap_variant_arg_undeclared` | false accept | `capsInSignature` scanned only `DFn` params | scan `dtype` ctor `argTys` | +| `reject/t151_cap_body_annotation_undeclared` | false accept | Check 1 read signatures only | `capAnnotsInTerm`, mirroring `cap_annots_in_expr` | +| `reject/t152_root_cap_is_ambient_authority` | false accept | modeled the pre-R2 ambient `root_cap` | R2 gate, gated on full-fragment | +| `accept/t148_cap_narrow_chains` | false **reject** | modeled the pre-R4a `cap_narrow : Cap(IO) -> Cap(a)` | retype + `capNarrowViolation` sweep | +| `reject/t144_cap_derive_json_variant_arg` | false accept | rejection erased by the desugarer | known-limitations entry | + +**The R4a fix is the one to re-read before touching any of this.** Retyping +`cap_narrow` alone would have traded one false reject for three false +accepts: `reject/t153`/`t154`/`t155` were rejecting only as a side effect of +the old argument type failing to unify, and nothing anywhere consulted the +lattice. march moved that guarantee into a deferred sweep; this checker had +to move it too, in the same commit. A fix that "makes the failing file pass" +would have silently opened three holes. + +It also exposed a second-order gap: `Infer` was ignoring `dfn` return +annotations. That was invisible while every builtin's result was pinned by +its argument types, and R4a's polymorphic `cap_narrow` removed that pinning. + +## 2. Known gaps (corpus-invisible) + +Recorded in full in `specs/march-findings.md`. Summarized here because the +conformance gate is structurally incapable of reporting them, so a green run +must not be read as evidence about any of them: + +1. **Path-scoped capabilities** — `needs IO.FileRead("/etc")`. The emitter + carries scopes in a new `scopes` array; `Elab`'s `DNeeds` reads only + `paths`. A scope never subsumes unscoped, so a narrow declaration decodes + here as the broadest possible one. A false accept **by construction**, with + zero corpus files using the syntax. +2. **`Tagged`** — march's `caps_in_ty` now recurses into it; `capsInTy` still + mirrors the arm march deleted. +3. **Check 4 semantics (march#209)** — an importer now inherits only the caps + of the functions it references. This checker still uses the whole-module + rule, so it is now strictly STRICTER than march: a false-REJECT direction. +4. **`normalize`** — march's dedupes, ours does not. Latent only because + `normalize` is not on the verdict path. + +Gaps 1 and 3 are the ones with teeth, and they point opposite ways. Neither +has a corpus witness; both need hand-built probes. + +## 3. Coverage change + +`accept/t49_transitive_use_covered` regressed MATCH -> SKIP, so A3 slice (a) +now holds 10 of the 11 files it claimed. The cause is not a checker +regression: march#209 rewrote the file to add `Vault.new("t")` (the reference +the new Check 4 requires), march accepts it, and march's own +`--emit-core-ast` emits `resolved_ty: TError` for that stdlib call. H3 +honest-skips on `TError`, which is correct behavior. The inconsistency — +an accepted program whose emitted AST carries an elaboration-error sentinel — +is march-side and is recorded as a finding. + +## 4. What did NOT change + +`format_version` is still 3, so no emitter-version dance and no two-repo +sequencing. `module_caps` is still emitted. The harness, exit-code contract, +and `Compare` are untouched. + +## 5. If you are bumping the pin again + +- Build march from the target SHA. Do not trust whatever `march` is on PATH. +- Diff `lib/dump/ast_json.ml`, `lib/caps/`, and the corpus file count first; + those three predicted every finding here. +- Read new corpus filenames as a checklist. `reject/t148`-`t152` named their + own subject matter, and each one that skips rather than matches is a + question, not a pass. +- A skip is not a pass. Nine of the 26 new ledger entries are capability + rejects this checker cannot judge.