caps: verify oracle-sync finding, fix main mixed-param-list MISMATCH - #24
Merged
Merged
Conversation
…nc finding 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.
…ates them 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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Verifies the oracle-sync finding filed 2026-08-10, which predicted
reject/t166_grant_narrow_violated_by_helper(and a since-renumbered sibling) would be hard MISMATCHes against march's grant check. Checked directly against a fresh march build offorigin/main(9d481cb3), since this branch's CI still pins the pre-grant-check6867c783.t166and its stage-C/D siblings (t174_fn_grant_violated_by_helper,t176_main_no_grant_does_io) all usefile_write, a builtinInfer.leandoesn't type — so they honestlyskipbefore the (missing) grant check would matter. Newly-observed skips (these plus a few unrelated SIMD-lane fixtures that landed in the same window) are now ledgered inscripts/expected-skips.txt.reject/t177_main_mixed_param_list(fn main(cap : Cap(IO), n : Int)). R1 stage D's rule thatmain's parameter list is zero-or-more capabilities, never a mix, was entirely unmodeled — the checker fell through every existing check to.ok. Fixed withmainMixedParamsViolationinMarchLean/CapCheck.lean, wired in as checkR1-D, mirroringDesugar.check_main_signature. Verified against march directly; stage-D's multi-cap accept fixtures are unaffected.maingrantedCap(IO.Clock), a helper reachingIO.Consoleviaprintln— the one IO builtinInfer.leanactually types) is a genuine false-accept: march rejects,march-lean-checkaccepts. The transitive grant-reach check (R1 stages A–C) has zero implementation inCapCheck.lean; it's invisible to the corpus only because every corpus witness happens to route through an untyped builtin. Not attempted in this PR — it's comparable in size to several existing checks combined, and a rushed version risks trading a false-accept for a false-reject. Full write-up, probe, and fix shape inspecs/march-findings.md§6.Full conformance harness (383 files incl. grammar/golden extras, run against march
origin/main):MISMATCH: 0,SKIP-LEDGER: OK,RESULT: PASS.Test plan
lake build— cleant177_main_mixed_param_listrejects (was accept)t174-t176accept-side) unaffected, still skip onfile_writescripts/conformance-harness.shrun against marchorigin/main(fresh build) +--lang-dirextras: 383 files,MISMATCH: 0,SKIP-LEDGER: OK,RESULT: PASSspecs/march-findings.md§6, not a corpus file)