feat: decoder-coverage gate + model Check 6 (a live false accept); MATCH 86→87 - #20
Merged
Merged
Conversation
…ecoded ones
Two of the worst defects here were the same mechanical oversight: march
emits a node kind, `Elab.decodeTerm` has no arm for it, and the node
silently degrades.
ELet no arm -> a `do` block whose sole statement is a `let` DISCARDED
the binding's RHS, blinding all four CapCheck capability walks.
EAnnot no arm -> `Desugar` synthesizes one for every `app` block
(desugar.ml:929), so a `cap` violation in an app body was
invisible.
Both cost expensive hand-probing to find. Both were rationalised away by
reasoning from march's GRAMMAR — "no parser production reaches this kind" —
which is unsound, because `Desugar` sits between the parser and the emitter
and manufactures nodes with no surface syntax. Both would have been caught
for free by diffing "kinds the corpus emits" against "kinds the decoder
handles". This is that diff.
scripts/decoder-coverage.sh sweeps the same four corpora the conformance
harness does (same flags, same argument conventions), collects every "kind"
string --emit-core-ast produces, and fails on any kind the decoder degrades
without that being declared.
How the handled set is derived, and why it is not a list:
A hand-maintained `handledKinds` next to the decoder looks authoritative
and is not — deleting the "ELet" arm would not change it, so the check
would pass while the exact historical bug was reintroduced. Regexing the
match arms out of Elab.lean is the same guess with more rot.
So `march-lean-check --kind-coverage` (MarchLean/KindCoverage.lean) RUNS
the real decoder on a synthetic node bearing the kind under test, at every
kind-dispatching site in Elab.lean, and probes each site twice — once with
the kind, once with a sentinel march can never emit. Comparing the two
separates "has its own arm" from "indistinguishable from a kind that does
not exist". The answer comes from the live match arms and cannot drift
from them.
Four outcomes, and only `modeled` passes unconditionally:
modeled a real modelled constructor
opaque `Term.opaque_` — shape unmodelled, child expressions survive
unsupported an `.unsupported` sentinel — children discarded
fell-through no arm at all
The last three are legitimate for genuinely unmodelled constructs but must
be declared in scripts/decoder-degraded-kinds.txt WITH THEIR CATEGORY.
Keeping the three distinct is what makes the EAnnot regression catchable:
dropping that arm leaves EAnnot degraded either way, but moves it from
`opaque` to `fell-through`, and the declared category stops matching.
Enforced both directions — a listed kind that became `modeled` is a stale
entry and also fails.
Also fails on: a kind recognised at two dispatch sites (the check compares
bare kind strings, which is only sound while march's tag namespaces stay
disjoint), a probe fixture too stale to classify a kind, and any file
--emit-core-ast produces nothing for.
Today: 334 files, 82 distinct kinds — 51 modeled, 8 opaque, 1 unsupported,
22 fell-through. Runs in ~45s at --jobs 10; it re-checks nothing in Lean.
--histogram prints kind -> count so a human can see what is rare: EAnnot
occurs exactly ONCE in 334 files.
Three entries are called out as DEFAULTING fall-throughs (Unrestricted,
UseSingle, UseAll): unlike the rest they reach no `.unsupported` sentinel,
so nothing is marked out of fragment and the file is judged as if the tag
had been understood. UseAll is safe only by accident — its one corpus file
already skips for an unrelated reason.
…cept
march's Check 6 (`typecheck.ml:8091-8140`) rejects any `fn` whose declared
RETURN type mentions a proof capability that its parameters do not, unless
the fn is a PUBLIC function of that cap's own declaring module. Nothing in
`CapCheck` modelled it, and it is reachable with a fully-in-fragment file, so
it was a FALSE ACCEPT — march exit 1, `march-lean-check` exit 0.
Three shapes verified against the binary (all previously exit 0 here):
mod Db4 do proof cap M type Box(a) = Empty | Full(a)
pfn make() : Box(Cap(Db4.M)) do Empty end
fn main() do println("hi") end end
-- march: "private function `make` in `Db4` cannot mint `Cap(Db4.M)`."
... the same with `proof cap M` written AFTER `make` (still rejects: the
entry module's check runs against `final_env`, so it is order-insensitive)
mod Db do proof cap M type Box(a) = Empty | Full(a)
mod Inner do needs Db.M
fn forge() : Box(Cap(Db.M)) do Empty end end
fn main() do println("hi") end end
-- march: "function `forge` returns `Cap(Db.M)` but `Cap(Db.M)` is a
-- proof capability declared in `Db`." (a PUBLIC fn — the
-- `declaring_mod <> mod_name` branch ignores visibility)
The bare-`Cap(P)` return shape stays a skip: producing one needs `mint_cap`,
which is unbound in this fragment. Wrapping it in a user ADT (`Box(Cap(P))`)
is what makes a violating signature satisfiable by an in-fragment body
(`Empty`), and is how the false accept was found.
What this adds:
* `Syntax.Vis` (`pub`/`priv`) as a new FIRST field on `Decl.dfn`, mirroring
march's `Ast.visibility`, emitted on every DFn as `fn.vis`
(`ast_json.ml`'s `visibility_to_json`). Check 6's same-module branch
fires only on `priv`, so the decoder defaults to `pub` on any
unrecognised/missing payload — a decode failure can then only cost a
reject, never manufacture one. Every existing construction site is a
mechanical `.pub`; no other pass reads the field.
* Check 6 in `checkOneModule`, between Check 4 and Check 7, driven by two
caller-supplied sets that encode march's env threading exactly as
Finding I1 already established it: `selfDeclaredCaps` (proof caps this
module itself declares — non-empty ONLY for the entry module) and a new
`foreignProofCaps` (visible proof caps declared elsewhere), accumulated
POSITIONALLY by `checkDecls`'s existing sequential fold, since march
registers `proof cap` inside `check_decl` and a nested `mod` therefore
sees only what precedes it.
* A nested module declaring its OWN proof cap and minting it still reports
**Check 1**, not Check 6 — march's `check_module_needs` for a nested
module runs on the env captured BEFORE that module's decls were folded,
so the cap is not in `env.proof_caps` at all. Verified; unchanged here.
False-reject containment. The check declines to fire unless the module is
ENTIRELY in fragment: its verdict depends on the PARAMETER cap list being
complete, and a param whose surface type failed to decode contributes
nothing to it — march would see a pass-through and accept. Such files skip
downstream anyway, so the gate costs no coverage. Near-misses pinned as
fixtures and verified as march exit 0: the public minting surface, a `pfn`
pass-through, a nested module relaying a received cap, and the
`proof cap`-after-`mod` positional case.
Corpus sweep over all 275 emittable files under `specs/**/accept`,
`examples/`, `stdlib/`: (0,0)=34, (0,2)=213, (1,2)=28 — byte-identical to the
prior audit's baseline. No verdict anywhere changed; the two probe files that
previously skipped on `mint_cap` now agree at (1,1).
Placed ahead of `Run conformance harness` deliberately. It re-checks nothing in Lean — just --emit-core-ast plus a set comparison — so it costs ~2 minutes against the harness's 15-20, and a decoder gap should surface in the first two minutes rather than at the end of a long run. It also catches a failure mode the harness structurally CANNOT. When MarchLean/Elab.lean has no arm for a "kind" march emits, the node decodes to `Term.unsupported`, `hasUnsupported` goes true, and march-lean-check honestly exits 2 — a SKIP, which the harness treats as expected and which the skip ledger records as unchanged. Nothing anywhere reports that the REASON for the skip is a hole in the decoder. That is exactly how ELet and EAnnot survived until hand-probing found them. Gets the same four corpora and the same flag names the harness gets, from the same march-checkout at the same pinned SHA, so the two can never drift onto different inputs. This matters more than it looks: EAnnot is emitted ONLY by specs/lang/grammar/parse, so a run without --lang-dir sees 76 kinds instead of 82 and would have been blind to it. --histogram writes kind -> occurrence counts into the log, because rarity is the signal: EAnnot occurs exactly once across all 334 files. --jobs 4 matches the runner's cores; --emit-core-ast is ~1s of fixed startup per file, so the sweep is process-bound and parallelises linearly.
…t behind it
The `dfn`-only shape of every capability gate has been read as coincidental —
"correct today only because march's own checkers are also DFn-only" — with the
implication that each march widening silently converts a gate into a false
accept. Auditing every cell against the live march source and probing each one
against both binaries shows that reading is wrong, and the actual protection is
worth writing down so the next re-pin can check it:
A march declaration form is either (a) covered here by every ERROR-level
check march applies to it, or (b) decoded to `Decl.unsupported`, whose
`hasUnsupported = true` forces `Compare.inferModule`'s whole-file skip gate
— which every path to exit 0 passes through.
So widening a march walk to a class-(b) form moves our verdict from skip to
skip, never to a false accept. The fragility runs the other way: moving a form
from (b) into (a) without auditing every check that reaches it. That is exactly
how Check 6 was missed (previous commit), and `dfn`/`dlet` are the only forms
currently in class (a).
Adds to `CapCheck`'s module docstring the full check × decl-form table, with
march's scanned forms cited per row and the probe verdict for each gap. Every
class-(b) cell was confirmed individually as (march 1, here 2): `DImpl`,
`DTest`, `DDescribe`, `DSetup`, `DSetupAll`, `DActor` init, `DActor` handler,
`DInterface` default body, and `DActor` handler signatures for Check 1.
Two emitter facts found while probing, both previously mis-documented here:
* `app` blocks are DESUGARED to a real `DFn __app_init__` before
`--emit-core-ast`, so `division_safety.ml`'s `DApp` arm never sees the
shape we are handed — a `10 / 0` in `on_start` under `cap no_panic`
already agrees at (1,1).
* multi-clause `fn`s are desugared to a SINGLE clause with an `EMatch`
body, so `Elab.decodeDecl`'s "0 or 2+ clauses" arm is unreachable from
real emitter output. Two comments claiming a multi-clause fn "escapes"
Check 7 / Check 8 via `Decl.unsupported` described a path that never
happens; both are retracted in place, with the verifying probes recorded.
march's own cross-clause param concatenation is equally vestigial — its
capability checks run post-desugar too (`fn handle(0) … / fn handle(c :
Cap(IO.Network)) …` with no `needs` is march exit 0).
Also records, on `Syntax.Decl`, why a declaration-level `Term.opaque_`
analogue was evaluated and rejected: it closes no false-accept class (all
seven candidate forms already skip), and it would GENERATE false rejects,
because march's division walk passes a per-form parameter environment whose
refinements can discharge a divisor — an actor handler's params explicitly so,
and an `impl` method's params only when `adoptable_impl_methods` says so. A
children-only bag discards exactly the information those decisions need.
No behaviour change. Corpus sweep unchanged at (0,0)=34, (0,2)=213, (1,2)=28
over 275 files.
Combines the two completed queue items into one PR rather than deepening the stack: the decoder-coverage gate (scripts/, KindCoverage.lean) and the capability decl-form audit (CapCheck.lean, Syntax.lean). They touch disjoint files.
… blind spot The allowlist claimed Private/Public are 'read by nobody' and 'Never read'. Both became false when Check 6 landed: Elab.lean:664-666 reads fn.vis.kind directly to build Syntax.Vis, which Check 6 depends on. The decoder-coverage gate did not flag the change because it probes kindOf dispatch sites only; a kind consumed by a direct getObjVal? field read is invisible to it. That blind spot is now documented at the entry, so a PASS is not misread as 'nothing depends on this'. Also records that the decode defaults to Vis.pub on anything but the literal 'Private' — so if march renames the tag, Check 6 silently stops reporting private-mint violations. That is a false accept, not a skip, and the gate cannot see it either. Re-check at each re-pin. Docs only.
…coverage
Modelling Check 6 (proof-capability production) moves
reject/t57_mint_cap_pfn_declaring.march from skip to a real reject, so its
ledger entry is stale. Both implementations now reject it for the same
independently-derived reason:
march: private function `run_migrations` in `Db` cannot mint `Cap(Db.Migrated)`
ours: Check 6: private fn `run_migrations` ... only public functions of its
declaring module can
MATCH 86 -> 87, SKIP 246 -> 245. First corpus movement in this run of work;
every other fix in this stretch was invisible to the corpus.
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
2 participants
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.
1. A decoder-coverage gate (prevention, not another fix)
Two of the worst defects here were the same mechanical oversight: march emits an AST kind,
Elab.leanhas no arm for it, and the decoder silently degrades.ELet— no arm; adoblock whose sole statement is aletdiscarded the binding's RHS, blinding all four capability walks.EAnnot— no arm;Desugarsynthesizes it for everyappblock (desugar.ml:929).Both cost expensive hand-probing to find. Both would have been caught for free by diffing "kinds the corpus emits" against "kinds the decoder handles." This adds
scripts/decoder-coverage.sh+MarchLean/KindCoverage.lean+ a--kind-coveragemode, wired into CI before the harness so a decoder gap fails in ~45s rather than 18 minutes.The handled set is derived by probing the live decoder, not by reading a list. It runs the real decoder against a synthetic node for each kind at all 12
kindOfdispatch sites, twice — once with the kind, once with a sentinel march can never emit — and compares. A hand-maintained list would fail its own first break-test: deleting theELetarm wouldn't change a list. The probe can't drift from the arms because it is the arms.Four categories, only
modeledpasses.opaque/unsupported/fell-throughmust each be declared with their exact category, so a new kind landing in the deliberately-opaque bucket still trips the gate.Current state: 334 files, 82 distinct kinds, 51 modeled, 0 gaps.
Break-tests (all exit 1, tree restored):
ELetGAP — ELet (fell-through; 343 occurrences; not declared)EAnnotCATEGORY DRIFT — declared 'opaque', decoder now reports 'fell-through'ETupleGAP — ETuple (53 occurrences)ERecord(independent check by the reviewer, an arm the author never touched)GAP — ERecord (63 occurrences)--lang-diris effectively mandatory:EAnnotis emitted only bygrammar/parse. Without it the sweep sees 76 kinds and would have missed the defect that motivated this.2. Capability decl-form audit — one live false accept
The premise this started from was wrong, and the correction is the useful part.
I assumed a march checker widening to a new declaration form would convert our gate into a false accept. It doesn't: every decl form march scans but we don't decodes to
Decl.unsupported, forcinghasUnsupportedand the skip gate. All nine such cells probe as(march 1, here 2)— safe skips. Widening moves us skip → skip.The real invariant:
The fragility runs the other way — promoting a form from (b) into (a). Only
dfnanddletare in class (a), and that is exactly where the one real bug was (cfff082, division safety × top-levellet).The false accept: Check 6 was not modelled at all
Proof-capability production (
typecheck.ml) — apfn, or a fn outside the declaring module, returning a type that mentions a registered proof cap without receiving it as a parameter.violate1_entry_pfn—private function `make` in `Db4` cannot mint `Cap(Db4.M)`.violate3_nested_public_fn—function `forge` returns `Cap(Db.M)` but … is a proof capability declared in `Db`.fnminting surface, pass-through, relay)nearmiss1differs fromviolate1by one token (fnvspfn) — a publicfnin the declaring module is the legal minting surface. Fixed by decodingfn.visinto a newSyntax.Visplus a positionally-threadedforeignProofCaps.This is the first change in a long stretch that the corpus can see:
reject/t57_mint_cap_pfn_declaring.marchmoves skip → reject, MATCH 86 → 87. Both implementations reject it for the same independently-derived reason.Declaration-level
opaque_: evaluated and rejectedCarrying children at decl level (as
Term.opaque_does for terms) would close no false-accept class — all seven candidates already skip — and would generate false rejects: march's division walk passes a per-form parameter environment whose refinements discharge divisors (actor handler params explicitly;implmethod params peradoptable_impl_methods). A children-only bag discards exactly that.Two stale comments retracted
appblocks and multi-clausefns are both desugared before--emit-core-ast, soDAppalready agrees at(1,1)as a plaindfn, andElab's "2+ clauses" arm is unreachable.3. The gate caught a stale comment in its own allowlist
Within hours of being written, the allowlist claimed
Private/Publicare "read by nobody". That became false when Check 6 landed —Elab.lean:664-666readsfn.vis.kinddirectly to buildSyntax.Vis.The gate did not flag it, which exposes a real limitation now documented at the entry: the probe only observes kinds routed through a
kindOfdispatch site. A kind consumed by a directgetObjVal?field read is invisible to it and reportsfell-throughhowever heavily it's used. APASSdoes not mean "nothing depends on this kind."Also recorded: the decode defaults to
Vis.pubon anything but the literal"Private"(Elab.lean:666). If march renames the tag or stops emittingvis, Check 6 silently stops reporting private-mint violations — a false accept, not a skip, invisible to both the gate and the corpus. Re-check at each re-pin.Verification
Corpus sweep over 275 march-accepted files:
(0,0)=34,(0,2)=213,(1,2)=28— matches the established baseline. Build clean; all#eval/native_decidehold; nosorry/unsafe/import Mathlib.Knock-on: slice (d) has shrunk
Check 6 is one of the four proof-capability checks scoped for the proof-caps milestone. It is now modelled with live corpus coverage, leaving three: Check 1's self-declaration exemption,
(Cap-Mint), and(Cap-NoNarrowForge).Most likely to break at the next re-pin
Decl.unsupported— every gate becomes a false accept at once, with no mechanical guard.Decl.dlet× the fourdfn-only behavioral gates — precedented; no skip would catch it. Re-probe every re-pin.no_panic's 25 unbound panic-surface names.Vis.pubdefault above.