feat(caps): close the coverage gap opened by march#136 — Term.opaque_ over nine AST kinds - #14
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).
This was referenced Aug 3, 2026
Merged
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.
Close the capability coverage gap opened by march#136
march made
calls_in_exprtotal overAst.expr(march#136 — the fix for the blind spot this oracle reported). That function is the shared body-walk behindcheck_pure_module,check_deterministic_module,check_no_panic_module, and Check 8.Consequence: march now detects capability violations inside AST constructs our decoder maps to
Term.unsupported, so we skip where march rejects. Safe — never a false accept — but a skip detects nothing, and march was ahead of us on nine constructs.The nine gaps
ECond,ERecordUpdate,EAtom,EAssert,EDbg,ELetFn,ELetQ,ESend,ESpawn— each confirmed by probe to reject for the capability reason (not an incidental type error) while we exited 2.Deliberately excluded, with reasons:
EPipe,ESigil— not gaps. Desugar eliminates them before emission (desugar.ml:543-586,:733-744); both tools already reject those shapes. Decoder arms would be dead code.EAnnot,EResultRef— no parser productions; unreachable from source files.EHole— a leaf incalls_in_expr; no capability can hide in it.Mechanism: one cap-transparent constructor
The naive fix — decode these into fully modelled
Termconstructors — was rejected. It would makeDecl.hasUnsupportedfalse, soCompare.lean:286stops skipping the file,Inferthen judges constructs it has no typing rules for,Infer.lean:870throws, andCompare.lean:296-300converts that throw into a false reject. That is the exact regression mechanism from the previous slice.Instead this adds a single
Term.opaque_ (children : List Term) (ty : Ty)that:bodyCalls,bodyAllocates,divisionVerdict,matchesIn) recurse into them and can render a violation; andhasUnsupported = true, so the file still skips atCompare.lean:286exactly as today — inference and linearity never see it.This works because
MarchLeanCheck.leanrunscheckCapsbeforeinferModule, and a.violationreturns exit 1 immediately. Net: skip→reject for violations, everything else unchanged, zero false-reject exposure.The ordering dependency is now load-bearing for nine checks rather than one. The comment at
CapCheck.lean:396-405has been updated to say so explicitly: reorder the driver andopaque_degrades to silent, not conservative.Walk-arm reasoning
Governing rule: walks running before the skip gate recurse into
children; walks running after it are unreachable and mirror.unsupported.bodyCalls→children.any. Mirrorscalls_in_expr; can only ever add atrue, i.e. only ever turn a skip into a reject march also renders. This is the arm that closes the gap.bodyAllocates→children.any; the node itself allocates nothing. Verified againstno_alloc.ml: march deliberately does not flagERecordUpdate(unlikeERecord), so this must not copy.record'strue.divisionVerdict→ recurses with both channels emptied. march'siter_div_sitesretiresELetFn/ELetQbinders and pushesECondpath conditions;opaque_records neither, so carrying outer facts in would be unsound toward false reject (a staled = 0leaking into a rebinding body).matchesIn→children.flatMap(pure collector;matchExhaustiveremains the judgement site).divisorVerdict→.unknown;Compare.termSpanTys→[];Linearity.uses→0;capturedInLam→false;checkTerm→.ok;Infer.infer→ throw. All judgement sites or unreachable behind the gate.Testing
The corpus cannot regression-test any of this. A census of all 242 files found none combining a
capdirective with a capability violation inside any of these constructors — the harness numbers are identical before and after this change. The 23 newnative_decidefixtures are the only coverage that exists. (Third time this pattern has held for this repo.)Probe table — each construct, violating variant and near-miss (same construct, no banned call):
ECondERecordUpdateEAtomEAssertEDbgELetFnELetQESendESpawnControls unchanged:
printlnin a plain block undercap pure→ reject;10 / 0underno_panic→ reject;10 / 2→ accept. No near-miss returns 1.Known residuals (all conservative — lose detection, never risk a wrong verdict)
opaque_in application-function position is not reached ({ p with … }()), so march rejects and we skip. Argument position is fine. Being fixed as a follow-up.divisorVerdict→.unknownfor an opaque divisor:10 / dbg(x)underno_panicis a march reject, our skip.ECondpath conditions are not recorded, so a guard in acondarm cannot discharge a divisor in that arm — weakerno_paniccoverage insidecondthan insideif/match.ESpawn's violating shape isn't reachable in well-typed code (march requires a bare actor name); included becausecalls_in_exprwalks it.