Land PRs #14-#16: opaque_ coverage, ELet decode fix, println fix, 334-file harness - #17
Merged
Merged
Conversation
march made `calls_in_expr` total over `Ast.expr` (march#136). It is the
shared body-walk behind `check_pure_module`, `check_deterministic_module`,
`check_no_panic_module` and Check 8, so a capability violation can hide
inside an AST construct this fragment does not model. Nine such kinds were
decoding to `Term.unsupported`, which DISCARDS the children: the cap layer
could not see the violation and the file exited 2 where march exited 1.
Naively decoding these into real modelled `Term` constructors is the wrong
fix and is what produced the previous slice's false rejects: it makes
`Decl.hasUnsupported` false, `Compare.lean`'s skip gate stops firing, `Infer`
then judges constructs it has no typing rules for, throws, and
`Compare.inferModule` converts that throw into a REJECT march never renders.
Instead this exploits the driver ordering. `MarchLeanCheck.run` invokes
`CapCheck.checkCaps` BEFORE `Compare.inferModule`, and a `.violation` returns
exit 1 immediately. So a new constructor
Term.opaque_ (children : List Term) (ty : Ty)
carries exactly the sub-expression list march's own walk descends into, while
`Term.hasUnsupported` HARD-CODES `true` for it. The file therefore still hits
the whole-file skip gate exactly as before — `Infer` and `Linearity` never
see an `opaque_` node — so the change has zero false-reject exposure, and the
only pass that can act on it is the cap layer that runs ahead of the gate.
Kinds decoded (child fields read off the emitter `lib/dump/ast_json.ml`
:379-503, not guessed; table in `decodeTerm`'s docstring):
ECond, ERecordUpdate, EAtom, EAssert, EDbg, ELetFn, ELetQ, ESend, ESpawn.
Deliberately NOT included: EPipe/ESigil (desugar eliminates both before
emission, `desugar.ml:543-586`/`:733-744` — arms would be dead code);
EAnnot/EHole/EResultRef (no reachable parser production / leaf nodes with no
sub-expression a capability could hide in).
Per-site reasoning for the new walk arms. The governing rule: a walk that
runs BEFORE the skip gate recurses into `children`; a walk that runs AFTER it
is unreachable on any module containing an `opaque_`, so it mirrors
`.unsupported` exactly and provably changes nothing.
BEFORE the gate (recurse):
* `CapCheck.bodyCalls` — `children.any`. This is the direct mirror of march's
`calls_in_expr`, which walks all nine kinds (`typecheck.ml:7734-7750`).
Recursing can only ADD a `true`, i.e. only turn a skip into a reject march
also renders.
* `CapCheck.bodyAllocates` — `children.any`, contributing NO allocation of its
own. Verified against `no_alloc.ml`: its four allocating arms are
ETuple(_::_)/ERecord/ECon(_,_::_)/ELam, none of the nine, and it has an
explicit recurse-only arm for each (`no_alloc.ml:41-63`). Note march does
NOT treat ERecordUpdate as an allocation even though ERecord is one, so
this arm must not answer `true` the way `.record` does.
* `CapCheck.termMentionsAny` — `children.any`. This is the deliberately
over-approximate `expr_mentions`, used only to DISCARD a path fact on a
rebinding; over-approximating loses information rather than inventing a
proof, so recursing moves strictly in the safe direction. Leaving it
`false` would let a stale guard survive a rebinding hidden in an
ELetQ/ELetFn child and license a WRONG non-zero proof.
* `CapCheck.divisionVerdict` — recurses with BOTH channels EMPTIED. march's
`iter_div_sites` walks all nine but knows their shape: ELetFn/ELetQ retire
the names they bind, ECond pushes each arm's condition onto `path`.
`opaque_` records neither, so carrying the outer facts/path in unchanged
would be unsound toward false REJECT (a stale `d = 0` surviving into a
rebinding ELetFn body would manufacture a divZero). Empty facts + empty
path is conservative both ways: what survives is exactly march's two
unconditional judgements — literal-zero divisor (arm 1) and complex divisor
(arm 4).
* `CapCheck.matchesIn` — `children.flatMap`. Pure collector; a non-exhaustive
match nested in a `cond` arm is as much a panic surface as a top-level one,
and `matchExhaustive` remains the conservative judgement site.
JUDGEMENT site, held back:
* `CapCheck.divisorVerdict` (`.opaque_` AS the divisor, e.g. `10 / dbg(x)`) —
`.unknown`. All nine do land in march's arm-4 catch-all today, so rejecting
would be right, but this is a judgement, not a collector, and answering
`unknown` keeps the verdict identical to pre-`opaque_`. Tightening it is a
separate, separately-verified change.
AFTER the gate (unreachable; mirror `.unsupported`):
* `Compare.termSpanTys` — `[]`. Runs in `inferModule` step (3), after the
step-(1) skip gate. Recursing would also be harmless but would imply these
spans participate in the resolved_ty cross-check; they never can, since
their children are never inferred.
* `Linearity.uses` — `0`. Unreachable (skip gate precedes `checkLinearity`),
and additionally the SAFE half of the unreachable pair: `opaque_`'s children
are an unordered bag with no recorded mutual-exclusivity (an ECond's arms
are mutually exclusive like a match's, but nothing records that), so summing
would over-count a linear binder used once per arm into a bogus reject.
* `Linearity.capturedInLam` — `false`, consistent with `uses`'s 0.
* `Linearity.checkTerm` — `.ok`; cannot mask anything, the file exits 2 first.
* `Infer.infer` — `throw`, identical to `.unsupported`: reaching it would mean
the gate had failed, and a loud failure is what that wants.
The load-bearing comment on `bodyCalls`'s `.unsupported` arm is extended to
restate the ordering dependency, which this slice DEEPENS rather than merely
inherits: if the driver is reordered so the skip gate precedes `checkCaps`,
`Term.opaque_` stops detecting anything — it does not degrade to
conservative, it degrades to silent.
The 242-file conformance corpus cannot regression-test any of this: a census found NO file combining a `cap` directive with a capability violation inside `ECond`/`ERecordUpdate`/`EAtom`/`EAssert`/`EDbg`/`ELetFn`/`ELetQ`/`ESend`/ `ESpawn`. A green harness run is no evidence here, so these hand-built, self-contained `#eval`/`native_decide` pins are the only coverage. Each fixture reproduces the exact CHILD-LIST ARRANGEMENT `Elab.decodeTerm` produces for that `kind` — that arrangement, not the node's shape (which is not modelled), is the whole contract between decoder and cap layer. Every violating shape was verified end to end against the real march binary (march rejects naming the capability; `--emit-core-ast | march-lean-check` now exits 1 where it exited 2). Every near-miss counterpart was verified to be ACCEPTED by march and must NOT produce a violation — a violation there would be a false reject. Also pinned beyond the nine: * `Term.opaque_ _ _ |>.hasUnsupported = true` — the invariant the whole design rests on. If this ever flips, `Infer`/`Linearity` start judging these nodes and every fixture above becomes a false-reject risk. * `no_panic`: a literal-zero divisor inside a child rejects; a non-zero one does not. * `no_panic`: an outer `let d = 0` fact is NOT carried into an `opaque_` child — `10 / d` there is a SKIP, not a reject. This pins the empty-facts/empty-path recursion, whose whole purpose is that `opaque_` records no binders and a child kind (ELetFn/ELetQ) may rebind `d`. * `no_alloc`: an allocation nested in a child is found, and the `opaque_` node itself allocates nothing — the ERecordUpdate case, where march flags `ERecord` but deliberately not `ERecordUpdate`. * `no_panic`: a non-exhaustive match nested in a child is reached. Regression controls re-verified against the built binary: `println` in a plain block under `cap pure` still rejects (1/1); `10 / 0` under `no_panic` still rejects (1/1); `10 / 2` still accepts (0/0).
`Elab.decodeTerm` had no `"ELet"` arm. The docstring asserted march's
grammar "only produces `ELet` as one element of an `EBlock`'s expr list";
that was false on two counts:
* march's emitter does NOT wrap a single-statement `do` block in an
`EBlock` — a fn body that is one `ELet` is emitted as a bare `ELet`;
* `decodeBlockStmts` routes an `EBlock`'s FINAL element straight back to
`decodeTerm` (`[last] => decodeTerm last`).
Both shapes fell to `| _ => Term.unsupported`, DISCARDING the binding's
right-hand side. Every cap walk went blind at once — `bodyCalls`,
`bodyAllocates`, `divisionVerdict` and `matchesIn` — so march rejected
`fn f() : Unit do let q = println("leak") end` while we exited 2 (skip).
Same for `let q = [1,2,3]` under `no_alloc`, `let q = 10 / 0` under
`no_panic`, and a non-exhaustive `match` in a trailing let's RHS.
This is NOT an `opaque_` bug and not specific to the app-fn position that
surfaced it: `bodyCalls`'s generic `.app fn args` arm was always right, it
simply never received a term to walk.
`decodeTerm` now has an `"ELet"` arm. A trailing let has no continuation,
so `Term.unsupported` becomes the `let_`'s BODY — `hasUnsupported` stays
true (the file still skips, `Infer`/`Linearity` still never judge it) while
the RHS sits on a real `let_`, so `divisionVerdict`'s fact/path retirement
still applies to the bound name. A non-`PatVar`/`PatWild` pattern decodes to
`Term.opaque_ [rhs]` instead, which empties those channels and so cannot let
a stale fact about a rebound name manufacture a false reject.
Sibling of the same class, fixed here too: a non-`PatVar`/`PatWild` `ELet`
binder in NON-tail position made `decodeBlockStmts` answer
`Term.unsupported` for the whole element, throwing away both the RHS and the
entire remainder of the block. It now answers `Term.opaque_ [rhs, rest]`.
Verified against the real march binary — every violating shape flips 2 -> 1
and every clean counterpart march accepts stays at 2 or 0 (no false
rejects). Pinned by `native_decide` fixtures in `CapCheck.lean` and decoder
`#eval`s in `Elab`'s `Test` namespace.
ROOT CAUSE. march's builtin env does register
`("println", Mono (TArrow (t_string, t_unit)))` (typecheck.ml:1951), and this
checker transcribed that entry faithfully — but the entry is DEAD for any real
program. march's stdlib prelude defines an ordinary
fn println(x) do print(show(x)) ; print("\n") end
at stdlib/prelude.march:243, and bin/main.ml:214-217 UNWRAPS prelude.march's
`mod` body into the entry module's own top-level scope (prelude.march is the
head of stdlib_file_list, bin/main.ml:236), so that declaration SHADOWS the
builtin binding at every call site.
That shadowing binding is UNCONSTRAINED `∀a. a → ()`, not
`∀a. Show(a) => a → ()`. march attaches only DECLARED constraints to a function
scheme — bound_constraints from fn_bounds (typecheck.ml:6926) and
class_constraints from a `when` clause (typecheck.ml:7051), spliced on at
typecheck.ml:7139-7165. The CInterface("Show", _) raised by the body's `show(x)`
never enters the scheme: it goes to env.pending_constraints and is discharged at
the declaration boundary, where its type is still an unresolved TVar and
`discharge` takes the `| TVar _ -> () (* Still polymorphic *)` branch
(typecheck.ml:7530-7531) and drops it.
Verified directly against march --check (exit 0 = accept): println(1),
println(true), println((1, "a")), println({x: 1, y: 2}), println(Red) for a
`type Color = Red | Green` with NO impl Show, and println(some_fn_name) all
accept. A Show-CONSTRAINED scheme modeled here would therefore be a false-reject
source in its own right — this checker models no `impl` declarations at all, so
every user ADT would look Show-less. Unconstrained is both march-faithful and
the only direction that cannot manufacture false rejects.
Fixes 8 confirmed FALSE REJECTS, all specs/lang/grammar/parse, all
"infer: cannot unify String with Int|Bool": p01, p03, p04, p08, p09, p12, p15,
p22 — march=0/lean=1 before, march=0/lean=0 after.
specs/lang/types/accept/t86_bare_none_unpinned.march is unaffected: lean=2
(skip) before AND after. The builtinCtorSigs decision it belongs to is NOT
touched — still reverted — but its `println : String → ()` half is now moot,
noted inline.
SIBLING BUILTINS checked: `print` is NOT prelude-shadowed (prelude defines no
`fn print`), so it keeps Mono String → () — march rejects print(1) with
"expected `String` but got `Int`", verified, and so must this checker. Ditto
print_int/print_float. `println` is the only prelude-shadowed name among the
builtins registered here.
Fixtures: println of Int/Bool/Float/String/tuple accept, result is (), two
call sites instantiate independently, and print(1) still rejects. They THROW on
regression (failing the build) rather than only printing. native_decide is not
available for these — InferM = ExceptT String IO, so every Infer/Compare entry
point is IO-bound with no pure Decidable proposition to discharge; the repo's
native_decide fixtures all live in the pure Syntax/CapCheck code.
The harness only ever scanned {accept,reject} under --corpus-dir
(specs/lang/types). Three corpora had never been tested. Adds an OPTIONAL
--lang-dir PATH (env LANG_DIR) pointing at march's specs/lang, which adds:
specs/lang/grammar/parse 34 files, accept-side
specs/lang/grammar/reject 12 files, reject-side
specs/lang/golden 46 files, accept-side (INDEX.md is not *.march
and so is never matched by the glob)
The directory-derived expected-verdict check — the CORPUS_VIOLATION mechanism
— is preserved exactly: expected verdict still comes solely from the file's
parent DIRECTORY NAME, and `parse`/`golden` simply join `accept` in the
accept-side arm of that same case statement while grammar/reject's own
`reject` basename already lands in the reject-side arm. Accept-side vs
reject-side skip bucketing now keys off that expected verdict rather than a
literal "accept" directory name.
The --corpus-dir sweep is untouched and its behavior is byte-identical;
without --lang-dir the script scans exactly what it always has, and the
summary then prints "extra corpora: NOT SCANNED" so the missing coverage is
loud rather than silent. CI passes the flag and its sparse-checkout now
fetches specs/lang/{types,grammar,golden}.
LEDGER. One file, four sections, not a second file: the harness compares ONE
observed-skip set against ONE ledger, and splitting it would mean duplicating
the both-directions diff logic per corpus for no gain. New entries are
DIRECTORY-QUALIFIED (grammar/parse/…, grammar/reject/…, golden/…) so they can
never collide with the historical two-segment accept/… and reject/… paths.
Post-println-fix scan of the 92 new files: 23 MATCH, 69 SKIP, 0 MISMATCH,
0 CORPUS_VIOLATION. Notably all 12 grammar/reject files skip, 11 of them
because march's --emit-core-ast emits an envelope with no module at all for a
SYNTAX error — an AST-level checker has nothing to judge. That corpus is
structurally out of reach for A2 today; the ledger records it as such rather
than pretending coverage.
Our println : forall a. a -> () is bug-for-bug faithful to march only because march DROPS the Show constraint its own prelude body raises (typecheck.ml:7530-7531, discharged while still a TVar). The builtin Mono (String -> ()) at typecheck.ml:1951 is dead code, shadowed by stdlib/prelude.march:243 via bin/main.ml:214-217's prelude unwrapping. If march ever propagates inferred CInterface constraints into schemes, we flip from faithful to false-ACCEPTING, and no corpus file would catch it. Recorded so the next re-pin re-checks it. Docs only.
…eported march#136 merged as 9a373001, making both copies of calls_in_expr total over Ast.expr and removing the catch-all. The entry still claimed 'reported upstream: NOT YET', which is now wrong in the direction that matters — it would send someone to re-file a fixed bug. Also records that the fix briefly inverted the coverage relationship (march's total walk vs our unsupported-mapped decoder), closed by Term.opaque_ and the ELet decode fix. Docs only.
…intln fix(infer): println is ∀a. a → () — 8 false rejects; sweep 92 previously-untested corpus files
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.
Land PRs #14, #15, #16 — they merged into each other, not into
mainWhat happened
All four of #13–#16 show as MERGED, but
mainonly ever received #13.They were a four-deep stack, each based on the one below:
repin-march-baselinemain✅cap-opaque-coverageclaude/repin-march-baselineopaque-app-fnclaude/cap-opaque-coverageshow-polymorphic-printlnclaude/opaque-app-fn#13 merged into
mainwhilerepin-march-baselinewas still at3bd4664— i.e. before #14 landed on it. From then on the chain kept resolving among the intermediate branches and never reachedmain. Nothing was lost; it just never arrived.This PR merges
maininto the fullest branch (claude/opaque-app-fn, which transitively contains #14, #15 and #16) and lands the whole thing in one go.Why it matters
Until this merges,
main's CI runs the old 242-file harness without the false-reject fixes — quietly weaker than the PR history suggests.What
mainis missing (8 commits, ~1,130 lines)Term.opaque_(feat(caps): close the coverage gap opened by march#136 — Term.opaque_ over nine AST kinds #14) — closes nine capability coverage gaps opened by march#136 (ECond,ERecordUpdate,EAtom,EAssert,EDbg,ELetFn,ELetQ,ESend,ESpawn), without exposing any of them to the inference layer.ELetdecode fix (fix(decode): decodeTerm dropped a trailing ELet's RHS, blinding all four cap walks #15) —decodeTermhad noELetarm, so adoblock whose sole statement is aletdiscarded the binding's RHS, blinding all four capability walks at once. A docstring asserting march "only producesELetinside anEBlock" made the missing arm look deliberate; it was false on two counts.println : ∀a. a → ()(fix(infer): println is ∀a. a → () — 8 false rejects; sweep 92 previously-untested corpus files #16) — 8 false rejects on ordinary code (println(10 - 3 - 2)). march's builtinMono (String → ())is dead code, shadowed by an unconstrained prelude binding whoseShowconstraint march drops attypecheck.ml:7530-7531.grammar/parse,grammar/reject, andgoldenvia--lang-dir. Corpus 242 → 334, real verdicts 63 → 86.specs/march-findings.mdupdates, including correcting a stale entry that still claimed march#82's second-calls_in_exprdefect was unreported after march#136 had fixed it.Verification (re-run on this exact merge, not inherited)
Build clean; all
#eval/native_decidefixtures hold.Process note
The stacked structure caused this. Landing each piece directly to
mainas it went green would have avoided it. Future slices should merge tomainone at a time rather than stacking.Known, unfixed (verified, carried forward)
matchon anIntscrutinee undercap no_panic— march rejects, we accept.--lang-diris opt-in; the summary printsextra corpora: NOT SCANNEDwhen omitted, but nothing enforces it.grammar/rejectis 12 files but ~1 file of real signal — 11 are syntax errors that emit no module to judge.