From d3a9ccb51d7b367d450099ff6a0622a81505ac0a Mon Sep 17 00:00:00 2001 From: Matthew Gilliam Date: Thu, 13 Aug 2026 17:21:41 -0400 Subject: [PATCH 1/2] fix(caps): main mixed-param-list check; ledger + verify the oracle-sync finding MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Verified the 2026-08-10 oracle-sync finding directly against march origin/main (a fresh build, since this branch's CI still pins the pre-grant-check 6867c783): the specific predicted MISMATCHes (reject/t166 and its stage-C/D siblings) don't happen — every one of those witnesses uses `file_write`, a builtin Infer.lean doesn't type, so they honestly skip before the missing grant check would matter. Ledgered in expected-skips.txt. The full run against current march did turn up a real, different hard MISMATCH: reject/t177_main_mixed_param_list (`fn main(cap: Cap(IO), n: Int)`) — R1 stage D's main-signature rule was entirely unmodeled. Fixed with mainMixedParamsViolation (CapCheck.lean, wired in as R1-D), mirroring Desugar.check_main_signature. The deeper gap remains open: a hand-built probe (main granted Cap(IO.Clock), a helper reaching IO.Console via the one IO builtin Infer.lean does type, println) confirms the transitive grant-reach check itself is a live false-accept, not just corpus-masked. Not attempted here — write-up and fix shape in specs/march-findings.md §6. --- MarchLean/CapCheck.lean | 36 +++++++++++++++ scripts/expected-skips.txt | 11 +++++ specs/march-findings.md | 90 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 137 insertions(+) diff --git a/MarchLean/CapCheck.lean b/MarchLean/CapCheck.lean index 22cd6d2..3e58f53 100644 --- a/MarchLean/CapCheck.lean +++ b/MarchLean/CapCheck.lean @@ -1645,6 +1645,35 @@ def bodyHasNonExhaustiveMatch (userCtors : List (String × List String)) (t : Te def covered (declared : List String) (used : String) : Bool := declared.any (fun need => capSubsumes need used) +/-- R1 stage D (`specs/2026-08-10-r1-stage-d-grant-required-design.md`, +mirrors `Desugar.check_main_signature`): `main` may take zero parameters, or +ANY NUMBER of capability parameters (the grant is their union), but never a +MIXED list — a parameter with no `Cap(IO...)` type has no erased value for +the runtime to supply and no meaning in the grant, so a signature naming one +alongside real capabilities is rejected outright, before grant-tracking ever +runs. `reject/t177_main_mixed_param_list` (`fn main(cap : Cap(IO), n : Int)`) +is exactly this: every other check in this fragment passes, so without this +gate the file was a hard MISMATCH (march rejects, this checker fell through +to `.ok`) rather than the honest skip a genuinely unmodeled construct earns. + +Reuses `concreteLatticeCap` for the per-parameter test, so it accepts +precisely the IO-lattice points `Desugar.is_cap_io_ty` does (`Cap(IO)` and +its narrower points) and nothing else — an unannotated parameter (`none`) +counts as non-capability, matching `is_cap_io_ty None = false`. -/ +def mainMixedParamsViolation (decls : List Decl) : Option (Nat × Nat) := + decls.findSome? (fun d => + match d with + | .dfn "main" params _ _ => + let isCapParam : String × Lin × Option Ty → Bool := fun (_, _, tyOpt) => + match tyOpt with + | some ty => (concreteLatticeCap ty).isSome + | none => false + if params.isEmpty then none + else + let nCaps := (params.filter isCapParam).length + if nCaps == params.length then none else some (params.length, nCaps) + | _ => none) + /-- Check one module (not recursing into nested modules — the caller does that, since each module is checked against its OWN declared needs). `selfDeclaredCaps` is the list of fully-qualified cap paths (e.g. @@ -2062,6 +2091,13 @@ def checkOneModule (modName : String) (decls : List Decl) match divVerdicts.find? (fun (_, v) => v == DivVerdict.unknown) with | some (name, _) => .skip s!"cap no_panic: fn `{name}` in module `{modName}` divides by an expression this checker cannot resolve — march's policy is reject-unless-proven-non-zero, but a refinement type or a Z3 discharge may still prove it non-zero, so no verdict is rendered" + | none => + match mainMixedParamsViolation decls with + | some (n, nCaps) => + let nNonCap := n - nCaps + let plural := if n == 1 then "" else "s" + let verb := if nNonCap == 1 then "is" else "are" + .violation s!"R1-D: `main` in module `{modName}` must take zero arguments, or only arguments of type `Cap(IO)` (or a narrower IO-lattice point) — found {n} parameter{plural}, {nNonCap} of which {verb} not a capability" | none => .ok /-- The behavioral caps march inherits down into a nested `dmod` (Finding diff --git a/scripts/expected-skips.txt b/scripts/expected-skips.txt index f261db2..928c2c8 100644 --- a/scripts/expected-skips.txt +++ b/scripts/expected-skips.txt @@ -226,6 +226,10 @@ accept/t146_root_cap_in_test_body.march # out-of-fragm 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/t173_simd_extract_last_legal_lane.march # out of modeled fragment: SKIP: unbound variable `Simd.make_f32x4` +accept/t174_fn_grant_proven_narrow.march # out of modeled fragment: SKIP: unbound variable `file_write` +accept/t175_main_grant_fix_applied.march # out of modeled fragment: SKIP: unbound variable `file_write` +accept/t176_main_multi_cap_grant.march # out of modeled fragment: SKIP: unbound variable `file_write` 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` @@ -244,6 +248,13 @@ reject/t162_actor_call_qualified_bypasses_sendable_check.march # out-of-fragm 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 +reject/t166_grant_narrow_violated_by_helper.march # out of modeled fragment: SKIP: unbound variable `file_write` (R1 stage A/B grant-narrow violation still unmodeled in CapCheck.lean — see specs/march-findings.md) +reject/t169_native_f32_arr_not_sendable.march # out-of-fragment construct in a declaration +reject/t170_native_u8_arr_not_sendable.march # out-of-fragment construct in a declaration +reject/t171_simd_extract_f32x4_lane_out_of_range.march # out of modeled fragment: SKIP: unbound variable `Simd.make_f32x4` +reject/t172_simd_extract_u8x16_lane_out_of_range.march # out of modeled fragment: SKIP: unbound variable `Simd.splat_u8x16` +reject/t174_fn_grant_violated_by_helper.march # out of modeled fragment: SKIP: unbound variable `file_write` (R1 stage C per-function grant violation still unmodeled in CapCheck.lean — see specs/march-findings.md) +reject/t176_main_no_grant_does_io.march # out of modeled fragment: SKIP: unbound variable `file_write` (R1 stage D missing-grant check still unmodeled in CapCheck.lean — see specs/march-findings.md) # --- 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/specs/march-findings.md b/specs/march-findings.md index 7215427..d1a4f51 100644 --- a/specs/march-findings.md +++ b/specs/march-findings.md @@ -381,3 +381,93 @@ The self-declaration exemption applies here too: march tests **Status.** reported upstream: N/A (march is correct here; this checker is behind). NOT YET FIXED in march-lean. + +### 6. No grant check at all — confirmed live false-accept, one instance fixed, the transitive-reach core is not + +The 2026-08-10 sync-drift note (below the corpus this checker runs against +was rebuilt against march main HEAD `9d481cb3`, well past the CI pin — +see "Status" for what that means for THIS repo's gate) predicted that +`reject/t166_grant_narrow_violated_by_helper` and a since-renumbered sibling +would be hard MISMATCHes: march rejects a grant-narrowing violation, +`CapCheck.lean` has no grant-tracking at all, so it would accept. That +specific prediction was **verified false** — checked directly against a +march binary built from origin/main HEAD. Every corpus fixture built to +witness R1 stages A–D (`t166`, `t174_fn_grant_violated_by_helper`, +`t176_main_no_grant_does_io`, and their `t173`/`t175` SIMD/accept +neighbors — SIMD landed alongside grant-checking in the same window) uses a +builtin (`file_write`, `Simd.make_f32x4`, `Simd.splat_u8x16`) this checker's +`Infer.lean` does not type at all, so every one of them SKIPs with `unbound +variable` before the missing grant check would ever matter. Ledgered in +`scripts/expected-skips.txt`. + +**But the full-corpus run this predicate ran under DID find a real, +different hard MISMATCH**: `reject/t177_main_mixed_param_list.march` +(`fn main(cap : Cap(IO), n : Int)`) — R1 stage D's rule that `main`'s +parameter list is zero-or-more capabilities, never a mix. march rejects it +outright, at signature-validation time, before grant-tracking runs at all. +`CapCheck.lean` had nothing checking `main`'s signature shape, so it fell +through every existing check to `.ok`. **Fixed**: `mainMixedParamsViolation` +(`MarchLean/CapCheck.lean`, wired into `checkOneModule` as `R1-D`) mirrors +`Desugar.check_main_signature` — reuses the existing `concreteLatticeCap` +IO-lattice predicate per parameter, `none`/non-`Cap(IO...)` counts as +non-capability. Verified: `t177` now correctly rejects, and the stage-D +multi-cap accept fixtures (`t174`–`t176` accept-side) are unaffected (they +still skip on `file_write`, unchanged). + +**What is NOT fixed, and is a live false-accept: the transitive grant-reach +check itself** (R1 stages A/B/C — "the whole program's IO reach is held +under the union of `main`'s (or a function's) `Cap(...)` parameters"). +`CapCheck.lean` has zero code implementing this — no call-graph closure, no +per-function grant discharge, nothing. It is invisible to the corpus purely +because every corpus witness happens to reach the violation through an +untyped builtin. It is NOT invisible in general — hand-built probe, run +directly against march origin/main HEAD and this checker: + +```march +mod Main do + needs IO.Clock + needs IO.Console + + fn helper() : () do + println("leak") + end + + fn main(cap : Cap(IO.Clock)) : () do + helper() + end +end +``` + +`println` IS a typed builtin (`Infer.lean:941`, required cap +`IO.Console` per `CapCheck.builtinCaps`) — no `unbound variable` skip fires. +march rejects: `` `main` is granted `Cap(IO.Clock)`, but the program reaches +`IO.Console` (reached in `helper`) ``. `march-lean-check` exits 0 (accept). +This is the exact false-accept class the sync-drift finding warned about, +just witnessed through `println`/`IO.Console` rather than the corpus's +`file_write`/`IO.FileWrite` fixtures, because `println`/`print` are the +only two IO builtins `Infer.lean` types at all (every other entry in +`CapCheck.builtinCaps` — the `file_*`/`tcp_*`/`process_*`/... families +— is `unbound variable` to `Infer.lean` and skips first). + +**Fix shape**, not attempted here: mirroring `check_main_grant` / +`check_fn_grants` (`typecheck.ml:12921-` onward) needs a call-graph closure +over which builtins/needs each function transitively reaches, held against +each grant point (`main`'s parameter union for stage A/B, each +`Cap`-parameter function's own parameters for stage C), plus stage D's +"performs IO but `main` takes no capability parameter" rule. This is +comparable in size to `CapCheck.lean`'s existing Check 1/4/5/8 machinery +combined, not a small addition, and a rushed version of a soundness-relevant +check risks trading a false-accept for a false-reject (see finding 5's three +hazards for the shape of that risk). Tracked as an open gap, not attempted +in this pass. + +**Status.** reported upstream: N/A (march is correct; this checker is +behind). `t177`'s specific MISMATCH: **fixed in march-lean**. The general +transitive grant-reach check: **NOT YET FIXED**, confirmed live via the +probe above. Separately: **this repo's CI (`conformance.yml:139`) still +pins march at `6867c783`**, which predates the grant check entirely (R1 +stages A/B landed in `78143049`/`759368b4`/`fb9a8c90`, all after that pin) — +so today's CI corpus doesn't contain `t166`–`t177` at all and this whole +finding is invisible to it either way. Bumping that pin is a separate, +larger action (full-corpus revalidation against everything march landed +since `6867c783`, not just the grant fixtures) and was not attempted here. From 883fe8d434bf15c4690b8ff0e766cff02a5809c2 Mon Sep 17 00:00:00 2001 From: Matthew Gilliam Date: Thu, 13 Aug 2026 18:02:06 -0400 Subject: [PATCH 2/2] =?UTF-8?q?fix(caps):=20revert=20premature=20skip-ledg?= =?UTF-8?q?er=20entries=20=E2=80=94=20CI's=20march=20pin=20predates=20them?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PR #24's first CI run failed: I'd ledgered t166/t169-t172/t174/t176 (reject) and t173-t176 (accept) as expected skips, but this repo's CI (conformance.yml:139) still pins march at 6867c783, which predates every one of those fixtures entirely — they don't exist in CI's checkout, so the ledger entries were stale by construction. Verified against the exact pinned commit (built march at 6867c783 directly, ran the harness with --lang-dir exactly as CI does): 369 files, MATCH 94, MISMATCH 0, SKIP-LEDGER OK, RESULT PASS — matches CI's own MATCH/MISMATCH counts from the failed run. The mainMixedParamsViolation fix (previous commit) is unaffected and still verified: t177 doesn't exist at this pin either, so the check is simply inert here, not wrong. march-findings.md corrected to say these skips are NOT ledgered yet, and why. --- scripts/expected-skips.txt | 11 ----------- specs/march-findings.md | 11 +++++++++-- 2 files changed, 9 insertions(+), 13 deletions(-) diff --git a/scripts/expected-skips.txt b/scripts/expected-skips.txt index 928c2c8..f261db2 100644 --- a/scripts/expected-skips.txt +++ b/scripts/expected-skips.txt @@ -226,10 +226,6 @@ accept/t146_root_cap_in_test_body.march # out-of-fragm 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/t173_simd_extract_last_legal_lane.march # out of modeled fragment: SKIP: unbound variable `Simd.make_f32x4` -accept/t174_fn_grant_proven_narrow.march # out of modeled fragment: SKIP: unbound variable `file_write` -accept/t175_main_grant_fix_applied.march # out of modeled fragment: SKIP: unbound variable `file_write` -accept/t176_main_multi_cap_grant.march # out of modeled fragment: SKIP: unbound variable `file_write` 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` @@ -248,13 +244,6 @@ reject/t162_actor_call_qualified_bypasses_sendable_check.march # out-of-fragm 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 -reject/t166_grant_narrow_violated_by_helper.march # out of modeled fragment: SKIP: unbound variable `file_write` (R1 stage A/B grant-narrow violation still unmodeled in CapCheck.lean — see specs/march-findings.md) -reject/t169_native_f32_arr_not_sendable.march # out-of-fragment construct in a declaration -reject/t170_native_u8_arr_not_sendable.march # out-of-fragment construct in a declaration -reject/t171_simd_extract_f32x4_lane_out_of_range.march # out of modeled fragment: SKIP: unbound variable `Simd.make_f32x4` -reject/t172_simd_extract_u8x16_lane_out_of_range.march # out of modeled fragment: SKIP: unbound variable `Simd.splat_u8x16` -reject/t174_fn_grant_violated_by_helper.march # out of modeled fragment: SKIP: unbound variable `file_write` (R1 stage C per-function grant violation still unmodeled in CapCheck.lean — see specs/march-findings.md) -reject/t176_main_no_grant_does_io.march # out of modeled fragment: SKIP: unbound variable `file_write` (R1 stage D missing-grant check still unmodeled in CapCheck.lean — see specs/march-findings.md) # --- 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/specs/march-findings.md b/specs/march-findings.md index d1a4f51..83741c4 100644 --- a/specs/march-findings.md +++ b/specs/march-findings.md @@ -397,8 +397,15 @@ witness R1 stages A–D (`t166`, `t174_fn_grant_violated_by_helper`, neighbors — SIMD landed alongside grant-checking in the same window) uses a builtin (`file_write`, `Simd.make_f32x4`, `Simd.splat_u8x16`) this checker's `Infer.lean` does not type at all, so every one of them SKIPs with `unbound -variable` before the missing grant check would ever matter. Ledgered in -`scripts/expected-skips.txt`. +variable` before the missing grant check would ever matter. **Not** ledgered +in `scripts/expected-skips.txt`: this repo's CI (`conformance.yml:139`) +still pins march at `6867c783`, which predates every one of these fixtures +(`t166`–`t177` don't exist in that checkout at all), so adding ledger +entries for them is a stale-entry SKIP-LEDGER MISMATCH against CI's actual +corpus — confirmed the hard way, in +[march-lean#24](https://github.com/march-language/march-lean/pull/24)'s +first CI run. Re-add them (and re-verify this whole entry) when that pin +bumps past the R1 stage A–D commits. **But the full-corpus run this predicate ran under DID find a real, different hard MISMATCH**: `reject/t177_main_mixed_param_list.march`