audit(decode): 3 false accepts from unconsumed fields; disprove the EAnnot comment - #19
Merged
Merged
Conversation
…just `dfn`
march's `refinecheck/division_safety.ml` walk is exhaustive over `A.decl`
with no wildcard and names `A.DLet (_, b, _) -> expr b.bind_expr` (:574) —
an arm added because omitting it was a march bug that shipped (see
specs/lang/types/reject/t120's header). `checkOneModule` scanned `dfn`
bodies only, reproducing march's OLD behavior.
Verified FALSE ACCEPT:
mod M do cap no_panic let bad = 10 / 0 ... end
march exit 1 ("division by zero literal in `cap no_panic` module."),
this checker exit 0. Now exit 1.
Scope is deliberately division-safety ONLY. Verified directly that march
ACCEPTS `cap pure` + `let bad = println("leak")` and `cap no_alloc` +
`let bad = (1, 2)` — `check_pure_module`/`check_deterministic_module`/
`check_no_panic_module`/`no_alloc.ml` all filter `Ast.DFn` alone. Both
near-misses are pinned as fixtures so a future widening breaks the build.
275 march-accepted files under specs/**/accept, examples/, stdlib/: verdicts
byte-identical before and after; zero rejects among them.
…fragment
`fn_def.bounds` (`fn f[a : SomeADT](...)`, parser.mly:386/414, ast.ml:231,
emitted at ast_json.ml:830 as `[{name, ty}]`) was never read by the decoder.
march does not merely record it: `typecheck.ml:6926-6959` VALIDATES every
bound and errors when it names neither a known ADT, a known interface, nor
`Nat`.
Two verified FALSE ACCEPTS (march exit 1, this checker exit 0):
fn f[a : NoSuchThing](x : Int) : Int do x end
-> "Bound `NoSuchThing` is not a known ADT or interface name."
fn f[a : Int -> Int](x : Int) : Int do x end
-> "Bound `Int -> Int` on type variable `a` must be an ADT name,
interface name, or `Nat`."
A bound also pre-registers a type variable for param annotations to
reference, which this fragment cannot represent at all (`decodeSurfaceTy`
maps every `TyVar` to `Ty.unsupported`). So the honest answer is the same
one a guarded clause already gets: `Decl.unsupported`, i.e. an honest
whole-file skip. Fails conservative by construction — this can only move a
verdict toward skip, never toward a confident one.
Costs nothing: zero of the 490 emittable .march files under march's specs/,
examples/ and stdlib/ carry a non-empty `bounds`.
…cap layer
The `decodeTerm` docstring claimed `EAnnot` was safe to omit because "no
parser production reaches" it. The premise is true and the conclusion is
FALSE: `Desugar` synthesizes an `EAnnot` for every `app` block
(`desugar.ml:929` wraps the app body in `EAnnot (body', SupervisorSpec, _)`),
and the resulting `DFn __app_init__` IS emitted. `EAnnot` is in fact the
ONLY unhandled expression `kind` present anywhere in a sweep of all 490
emittable .march files under march's specs/, examples/ and stdlib/.
Falling to `| _ => Term.unsupported` discarded the child expression, so a
`cap` violation inside an app body was invisible to every `CapCheck` walk —
the exact shape of the `ELet` defect. Verified divergences:
cap no_panic + app body `panic("boom")` -> march 1 (`__app_init__` ...
calls `panic`), this checker 2
cap pure + app body `println(...)` -> march 1 (`__app_init__` ...
calls `println`), this checker 2
Both are exit 1 now.
Zero false-reject exposure: `opaque_` models no typing rule and
`Term.hasUnsupported` is hard-coded `true` for it, so `Infer` and
`Linearity` still never see the node — identical contract to the nine
`opaque_` kinds already decoded this way. Only the child expression is
carried; the ascribed type is deliberately dropped.
The docstring is corrected in place, including the general lesson: "no
parser production reaches X" is not the claim "X is not emitted", because
Desugar runs between them and manufactures nodes of its own.
This was referenced Aug 8, 2026
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.
Audit: decoded-but-unconsumed fields — 3 more false accepts, 1 false comment
A systematic sweep for a specific defect signature that produced the three worst bugs found in this project:
That signature previously produced:
retAnnot(function return types were never checked — 8 false accepts),println(dead builtin-table entry — 8 false rejects), andELet(discarded aletRHS, blinding all four capability walks).The audit traced every decoder-populated field to its consumers, distinguishing "read by" from "acted on by" — the distinction is the whole point.
retAnnotwas read in several places and acted on in none that mattered, so a "is this referenced?" grep would have cleared it.Confirmed divergences (all verified against march's actual diagnostic)
fn f[a : NoSuchThing](x : Int) : Int do x endBound `NoSuchThing` is not a known ADT or interface name.fn f[a : Int -> Int](…)Bound `Int -> Int` … must be an ADT name, interface name, or `Nat`.cap no_panic+let bad = 10 / 0division by zero literal in `cap no_panic` module.cap no_panic/cap pure+appblock callingpanic/println`__app_init__` … calls `panic`The first two share one cause:
fn.boundswas never decoded at all — march emits it, we never looked. The third is the recurringdfn-only assumption: division safety scanned function bodies but not top-levelletbodies.The false comment
Elab.decodeTermasserted: "EAnnot/EHole/EResultRef… no parser production reaches them here."The premise is true and the conclusion is false.
DesugarsynthesizesEAnnotfor everyappblock (desugar.ml:929, annotating the spec field so the type checker verifies it returnsSupervisorSpec), inside aDFn __app_init__that is emitted. Confirmed onspecs/lang/grammar/parse/p19_app_on_start_supervisor_spec.march, which emitsEAnnot— the only unhandled expressionkindacross a sweep of all 490 emittable corpus files.Parser coverage ≠ emitter coverage. Desugar sits between them. That lesson is now written into the code.
Claims that held under the same scrutiny:
PatVarcarries nolin;EPipe/ESigilare never emitted;ELetFnnever decodes; Check-8's shared-blind-spot note.Notable non-gaps
DLet.binding.ty(a top-levellet x : String = 42) — march ignores it too (0/0). Decoding it would have created false rejects.fnlet annotations, lambda param annotations,retAnnot, and match-arm guards all verified as genuinely acted on.Verification
Build clean 24/24, no warnings, no
sorry/unsafe/import Mathlib; all pre-existing fixtures hold. New fixtures for all three fixes, including four near-misses pinning that the other cap gates staydfn-only.Regression sweep over 275 march-accepted files (
specs/**/accept,examples/,stdlib/): verdict tuples byte-identical before and after —(0,0)=34,(0,2)=213,(1,2)=28. Zero false rejects, zero false accepts introduced.Unchanged by these fixes — the corpus exercises none of these shapes. Fifth consecutive time.
Where the next defect of this shape lives (reported, not fixed)
Decl.dletin the remaining cap gates. They aredfn-only, and correct only because march's checkers areDFn-only today — a dependency on a moving target, and march is widening them one at a time.DImpl/DActor/DTest/DApp/DDescribe/DSetup*). Theopaque_"carry the children anyway" move has been made for terms but never for declarations.visis unmodelled (masked today by the qualified-call gap);Module.instsis decode-only, its docstring naming a consumer that was never written (costs exit-4 precision only, never soundness).Cheapest standing defence
A corpus
kind-histogram diffed againstdecodeTerm/decodeDecl's handled sets would have caught bothELetandEAnnotfor free — mechanically, with no probing. Worth building: it converts this entire defect class from "hope someone audits" into a check.