Proof layer for the capability checker (55 theorems) + march main resync - #23
Merged
Merged
Conversation
Design for a proof layer over the shipping capability checker: abstract lattice metatheory discharged by decide for march's 20-entry table, verdict algebra, de-partialization of the 18 cap-relevant walks with legacy-equivalence pins, and three whole-checker theorem/counterexample pairs (tier order-independence, normalize-stability, IO-cap monotonicity) — each true for the subsumption-coverage core and false at the behavioral-cap boundary.
…le (P0b) API-preserving: capParent/capAncestorsFuel/capAncestors/capSubsumes/ normalize become specializations of Calculus.parentIn/ancestorsInFuel/ ancestorsIn/subsumesIn/normalizeIn at the unchanged 20-entry hierarchy. Adds WellFormedB (nodup names + closed parents + acyclic) and the metatheory over any well-formed table: fuel adequacy, ancestor-chain shape, subsumption partial order (refl/trans/antisymm), sibling incomparability, FFI isolation, covered monotonicity, and normalize idempotence + coverage-preservation. Conformance output verified byte-identical to the pre-change baseline over the local 242-file corpus.
…ng names (P0b)
Kernel decide discharges the real 20-entry table in ~1s, then every
abstract theorem is instantiated at capSubsumes/capAncestors/normalize.
Negative control verified: adding a self-parent row ("X.Cycle", some
"X.Cycle") to hierarchy fails hierarchy_wellFormed's decide and stops
the build, then reverted. Before P0 that same cycle would have made
capAncestors silently truncate with no error anywhere.
Two gaps, both of which would have let the proof layer rot while CI stayed green: 1. CI built only `march-lean-check`, and MarchLeanCheck.lean imports individual modules rather than the MarchLean library root — so Calculus/Verdicts.lean and Calculus/Concrete.lean were outside the built import closure and were never kernel-checked. Both targets are now named. 2. Lean reports `sorry` as a warning, not an error, so `lake build` exits 0 with unproven theorems. Added a source grep gate. Both verified locally: the build succeeds with the CI args, and the guard was confirmed to fire on an injected sorry.
capsInSignature scanned only DFn parameters, so a Cap(X) named in a variant constructor argument escaped needs coverage entirely — a false ACCEPT on reject/t149_cap_variant_arg_undeclared against march main. march builds one cap_uses list over every decl form and DType contributes Cap_surface_ty.caps_in_type_def (typecheck.ml:8813); march's own comment records these arms were previously swallowed by a wildcard, which is the identical hole. Scanned ungated like parameters: the cap is named concretely, so capsInReturnSignature's unmodeled-machinery gate does not apply. TDRecord/TDAlias decode to Decl.unsupported, so reject/t148 and t150 reach the same conclusion as whole-file skips rather than here. Also ledgers reject/t144_cap_derive_json_variant_arg as a known limitation: march rejects the "derive Json" over a capability position, but that derive is erased by the desugarer and the residual (needs IO + type + main) is well-typed with its Cap(IO) covered — verified by inspecting the emitted Core AST, whose decl kinds are only DNeeds/DType/DFn. Same mechanism as the existing t23/t49 entries.
march's R2 made the root capability granted to main at the boundary rather than taken from an ambient global: naming root_cap is now an error (typecheck.ml:5118-5133). This checker still modeled the pre-R2 world, so reject/t152_root_cap_is_ambient_authority was a false ACCEPT — a module could hold Cap(IO) with no diagnostic and narrow freely from there. root_cap stays BOUND at Cap(IO) in Infer, matching march's deliberate choice to keep the name bound so one mistake reports a single capability error instead of cascading unification failures. Only referencing it is refused. march exempts four contexts via env.root_cap_allowed: DTest, DSetup, DSetupAll, and the REPL entry. All four decode to Decl.unsupported here, so the check gates on the module being entirely in fragment — the same residual gate retCaps already uses — rather than modeling the flag. That gate is load-bearing, not defensive: cap checks run BEFORE the skip gate (A3 design section 4), so accept/t146_root_cap_in_test_body would be a false REJECT without it. Pinned by the rootCapInUnsupportedContext fixture. Verified against march main: t152 reject/reject MATCH, t146 skips, accept/t147_main_receives_the_root (which takes cap : Cap(IO) as a parameter and never names root_cap) still accepts.
Check 1 read declaration signatures only, so a capability named by a type annotation inside a body escaped needs coverage entirely — a false ACCEPT on reject/t151_cap_body_annotation_undeclared against march main. capAnnotsInTerm mirrors march's cap_annots_in_expr (typecheck.ml:8109-8180): a let binding's annotation, and lambda / local-function parameter annotations, folded into the same cap_uses list Check 1 already consumes. Ungated like parameters — the cap is named concretely by an annotation the author wrote, so capsInReturnSignature's unmodeled-machinery gate does not apply. A lambda parameter is the sharp case and the reason R2 alone was not enough: naming the type needs no capability VALUE, so closing the ambient-root route (see the preceding commit) does not close this one. Total over every Term constructor with no wildcard arm, matching bodyCalls/bodyAllocates/termMentionsAny here and march's own stated rule for capability walks — a catch-all arm is a silent hole rather than a visible bug, and a new Term form must break this build. march's EAnnot arm has no counterpart (no such Term form); Term.letfn carries no return annotation, so march's ELetFn return arm is likewise unreachable in this fragment. Both noted in the docstring rather than left to be rediscovered. Verified against march main: t151 reject/reject MATCH, and accept/t145_cap_let_annotation_covered still accepts, so the walk does not over-reject a covered annotation. Nested coverage (tuple > match arm > lambda) pinned by the bodyAnnotNestedUncovered fixture.
march's R4a retyped cap_narrow from Cap(IO) -> Cap(a) to a fully polymorphic Cap(a) -> Cap(b), so a holder of something narrower than the root can delegate with attenuation. This checker still demanded the argument be literally Cap(IO) and rejected accept/t148_cap_narrow_chains with "cannot unify IO with IO.FileSystem" — a false REJECT. The dangerous half is what the retype does NOT do. Before R4a the argument type enforced subsumption through unification, and reject/t153 (widen), t154 (siblings) and t155 (widen visible only after later unification) all rejected as a SIDE EFFECT of that unification failure — nothing consulted the lattice. Retyping alone would therefore have converted one false reject into three false accepts. march moved the guarantee into a deferred sweep (check_cap_narrow_sites, typecheck.ml:9406-9432); CapCheck.capNarrowViolation is the mirror, and all three files now reject because the lattice says so. The rule as march states it: an error iff BOTH sides resolve to concrete lattice capabilities AND the source does not subsume the target. Reflexivity is allowed, which is what makes t148's same_level legal. An unpinned side is silent — a result never pinned to a concrete capability is never USED as one. concreteLatticeCap requires hierarchy membership, which subsumes march's explicit proof-cap exemption and also excludes FFI caps; that difference can only make this checker more permissive, never less, so it cannot manufacture a false reject. Reading both sides off the application node works because the emitter's resolved_ty is POST-solve — verified on t155, whose cap_narrow application resolves to Cap(IO.FileWrite) with argument Cap(IO.Console), exactly the deferred widen march's sweep waits for. Also makes Infer honor a dfn's surface RETURN annotation, as it already honors parameter annotations. march CHECKS a body against its declared return type, so an annotated return has that type by definition. Skipping it was invisible while every builtin's result was pinned by its arguments; R4a broke that, and in `pfn same_level(r : Cap(IO.FileRead)) : Cap(IO.FileRead) do cap_narrow(r) end` the result is pinned ONLY by the annotation, leaving a metavariable where march resolved a concrete type (exit 4, types_differ). Verified against march main: t148 accept/accept, t153/t154/t155 reject/reject, accept/t52_cap_narrow_multi still accepts. The five R4a fixtures pin widen, siblings, attenuate, same-level, and the proof-cap exemption independently of the corpus.
…iles
Bumps the pin 71 commits, from 7c1d701c. Unlike the previous two bumps this
drift was NOT inert: it surfaced five corpus-visible divergences, four of
them false ACCEPTS, each fixed in the four commits preceding this one. The
pin comment now records the assessment in full.
format_version is still 3 and module_caps is still emitted, so there is no
emitter-version dance and no two-repo sequencing — the checker reads main's
output as-is.
Ledger: 177 -> 203 entries, purely additive (zero stale entries), tracking
the corpus's growth from 242 to 277 files. Nine of the 26 additions are
capability rejects this checker still cannot judge; a skip is not a pass.
One entry is a REGRESSION rather than a new file and is annotated as such:
accept/t49_transitive_use_covered was MATCH and now skips, so A3 slice (a)
holds 10 of the 11 files it claimed. Not a checker regression — march#209
rewrote the file to add the reference its new per-function Check 4 requires,
march ACCEPTS the result, and march's own --emit-core-ast emits resolved_ty
TError for that stdlib call. H3 honest-skips on TError, which is correct.
The inconsistency is march-side.
Also records four gaps against this pin that the corpus is structurally
incapable of catching, so a green run is NOT evidence about any of them
(specs/march-findings.md, and summarized in
specs/plans/2026-08-08-march-main-capability-resync.md):
- path-scoped capabilities decode as unscoped — a false accept BY
CONSTRUCTION, with zero corpus files using the syntax;
- capsInTy still skips Tagged, mirroring an arm march deleted;
- Check 4 still uses the pre-march#209 whole-module rule, making this
checker strictly STRICTER than march — a false-reject direction;
- normalize does not dedupe (latent: not on the verdict path).
The first and third have teeth and point opposite ways. Both need
hand-built probes.
Verified against march main: MATCH 71, MISMATCH 0, ERROR 0,
CORPUS_VIOLATION 0, MARCH_SELF_INCONSISTENT 0, SKIP 203, ledger OK.
…vioral layer (P2)
Two properties that sound like they should hold of checkCaps — replacing
needs L by needs (normalize L) never changes the verdict, and adding a
capability to needs never flips accept into reject — are TRUE for the
subsumption-coverage core and FALSE for the full checker. This proves both
halves of each.
The boundary is the same mechanism twice: cap no_extern reads the needs list
for a property of the LIST ITSELF (hasForeignNeed) rather than asking what
the list covers. A check that inspects the syntax of a declaration set rather
than its denotation cannot be stable under an operation that preserves only
the denotation — and normalize is exactly such an operation
(coveredIn_normalizeIn).
So these are not curiosities to work around. They say: normalize may never be
applied to a needs list before a behavioral-cap check runs. Nothing does that
today; this makes it a checked invariant rather than an accident.
The counterexamples are sharper than "the verdict differs":
- normalize ["IO", "IO.Foreign"] = ["IO"], because IO.Foreign's parent is
IO. The two lists are coverage-EQUIVALENT (proved, not asserted), so no
coverage-based check could tell them apart — yet the verdict moves
violation -> ok.
- For monotonicity, the ADDED capability is already covered by IO
(added_cap_was_already_covered), so it grants no new authority
whatsoever, and the verdict still flips ok -> violation. Declaring a
capability is itself observable behavior at the behavioral layer:
no_extern objects to the DECLARATION of foreign authority, not to
holding it.
Proof-strength split, deliberate and documented in the file: the mechanism is
kernel-checked with no axioms at all (normalize_absorbs_foreign,
added_cap_was_already_covered are pure computation over the total
CapLattice), while the end-to-end checkCaps verdicts are pinned by
native_decide, because checkCaps runs through partial defs and has no
equation lemmas for the kernel to unfold. hasForeignNeed also needs
native_decide: it splits on ".", and String.splitOn does not reduce in the
kernel. The mechanism is the part that generalizes; the end-to-end pin is
what proves the mechanism actually reaches a verdict.
Repo theorem count 55 -> 64. Additive only: no shipping definition changes,
so the conformance corpus is unaffected.
The remaining P2 theorem — verdict-tier order-independence — still needs P1
(de-partializing the tree walks), since it must induct over checkDecls.
…ctor (P1)
Syntax.lean's tree walks were partial defs recursing through List.any/List.all
— nested inside a higher-order call, which Lean's structural-recursion checker
cannot see through. Each is now a mutual block pairing the walk with an
explicit List helper, which makes the descent structural.
partial def is not free. It compiles to an opaque constant, so the kernel can
neither unfold it nor induct on it. Two consequences this commit removes:
- Every test over these walks said native_decide, i.e. trusted the compiled
evaluator rather than the kernel. All 15 in this file now say decide.
That is a trust hole closed, not a style change.
- No theorem about them was possible at all. P2's whole-checker properties
need induction over exactly these walks.
Term.hasUnsupported needed more than a helper: its
`| t => t.ty.hasUnsupported || (match t with …)` shape binds the whole term in
the catch-all, so Lean cannot see the inner match's calls descending. Every
constructor now names its own arm and repeats the node's ty check explicitly.
flattenDecls is the one genuine non-structural case — the dmod arm recurses
into a list nested INSIDE the head element, not a tail — so it terminates on
sizeOf instead, via termination_by/decreasing_by.
MarchLean/Calculus/Walks.lean argues the refactor is behavior-preserving, and
argues it more strongly than planned. The design called for keeping each old
body as a legacy twin and pinning `legacy x = new x` on fixtures. Instead each
helper is PROVED equal to the exact fold it replaced, by induction, for every
input:
Ty.anyHasUnsupported ts = ts.any Ty.hasUnsupported
Ty.beqList xs ys = (xs.length == ys.length && (xs.zip ys).all …)
Term.anyArmHasUnsupported arms = arms.any (fun (p, g, e) => …)
Decl.anyCtorHasUnsupported cs = cs.any (fun c => …)
… 15 in total
A fixture pin can only say "the two agree on what we thought to try"; these
say the two are the same function. Each theorem is literally the diff of the
refactor stated as an equation, so a future edit that drifts from its fold
stops compiling.
Two of these deserve their names read carefully. ty_beqList_eq shows the
length check was not lost when `length == length && zip` became a structural
walk — it is exactly the two fall-through arms. term_anyArmHasUnsupported_eq
states the arm walk INCLUDING its pattern component, which was dropped once
before and was a real false accept.
Also updates the stale comment in the test block that still explained why
these tests needed native_decide. It had become false, which is the precise
failure mode this project keeps paying for.
Repo theorem count 64 -> 78. Syntax.lean now has zero partial defs;
CapCheck.lean's 14 are the next step. Conformance re-verified: no shipping
behavior change.
Five conflicts, three of them semantic rather than textual. How each was resolved, since "took both sides" would be wrong for most of them: MarchLean.lean — import list. Kept both (TailCall plus the three Calculus modules). Infer.lean, hunk 1 — main kept the pre-R4a `cap_narrow : Cap(IO) -> Cap(a)` and added `println : forall a. a -> ()`. BOTH are needed: this branch retypes cap_narrow to `forall a b. Cap(a) -> Cap(b)` (R4a), and main's println fix is unrelated and correct. `capIO` stays defined because `root_cap` still uses it. Infer.lean, hunk 2 — main and this branch independently made the SAME fix (check a fn body against its declared return type), from opposite directions: main found it as a false-accept class across return-position mismatches (`: String` over an Int body, nominal aliases, and five more, each verified against march); this branch hit it because R4a's polymorphic cap_narrow leaves `same_level`'s body pinned only by the annotation. Took main's comment — it documents far more verified cases — and added the R4a interaction, which main's version does not mention and which `accept/t148` now depends on. Syntax.lean — the substantive one. main added a `Term.opaque_` constructor; this branch replaced Term.hasUnsupported's catch-all with explicit per-constructor arms (P1 de-partialization). Kept the structural version plus main's `.opaque_ => true` arm and its rationale. That resolution then FAILED TO BUILD, which is the point: CapCheck's two new exhaustive walks (capAnnotsInTerm, capNarrowViolation) had no `.opaque_` case, so a new constructor broke the build instead of silently falling through a wildcard. Both now recurse into `children`, matching the convention main's own walks use (bodyCalls, bodyAllocates, matchesIn) — which is the whole point of decoding EAnnot to opaque_ so its children survive to the cap layer. march-findings.md — main marked the march#82 finding FIXED UPSTREAM (merged as 9a373001), superseding this branch's stale "reported upstream: NOT YET". Took main's status and appended this branch's "gaps the corpus CANNOT catch" section after it. expected-skips.txt — main added ledger sections for the three corpora its new --lang-dir option sweeps (grammar/parse, grammar/reject, golden); this branch added 26 entries for the 277-file types corpus. Unioned, then re-baselined against a real run rather than trusting the union, since main's fixes (opaque_ decoding, exhaustiveness, println, EAnnot) and this branch's P1 change both move which files skip. Verified after resolving: all four gaps this branch records in march-findings.md are still accurate (Elab still drops `scopes`, capsInTy still has `| .con "Tagged" _ => []`, Check 4 still uses the whole-module rule), so none became stale across the merge. All 13 capability fixtures (Check 1 type-decl and body-annotation, R2, the five R4a cases) report unchanged verdicts. CI pin 6867c783 and the sorry/admit guard both survived the auto-merge.
…to ERROR The tail-call probes were authored against pin 7c1d701c, where a builtin call in a function body requiring an undeclared capability was a WARNING. This branch bumps the pin to 6867c783, where march made it an ERROR (typecheck.ml:9098, Err.error_with_fix: "function body calls a builtin that requires Cap(IO.Console) but M does not declare needs IO.Console"). Every probe calls println and none declared needs, so under the new pin march rejected all 22. The probe harness reported it exactly as designed — "march exit 1, expected 0 — probe has rotted" — 18 times. The other four are the more interesting half. They are the tailcall-class probes, which EXPECT march to reject, so they kept passing — for the wrong reason. march was rejecting them on the capability error, not on tail-call enforcement, so the thing they exist to test was no longer being tested at all. Adding needs IO.Console restores that: they now reject on tail calls again, and the clean probes accept. Probes are about tail-call enforcement; their lack of a capability manifest was incidental, so declaring it is the minimal fix and does not weaken them. Local run against march 6867c783: pass=22 fail=0. The promotion itself is a finding about THIS checker, not just about the probes — march-lean does not implement Check 1b at all, by an explicit A3 design decision that is now obsolete. Recorded separately in specs/march-findings.md.
march main 6867c783 raises Check 1b with Err.error_with_fix, not Err.warning (typecheck.ml:9098). A3 design decision 1.3 deliberately skipped 1b/1c on the grounds that they were WARNING-only and implementing them "would manufacture false MISMATCHes against a march that accepts". That reasoning was correct when written and is now obsolete: march closed the hole its own docs called "the single most consequential fact for anyone relying on needs as a soundness guarantee", and this checker did not follow. So what the design recorded as a shared weakness is now a DIVERGENCE, in the false-ACCEPT direction: a module calling an IO builtin in a body without declaring the capability is rejected by march and accepted here. Annotates the A3 decision in place rather than only recording the finding elsewhere — a superseded decision that still reads as current is exactly how this codebase has been bitten before. Worth reading the "how it was found" note. The 277-file corpus reports MISMATCH 0 against this same pin, because every corpus file declares its capabilities properly. The class surfaced only because the tail-call probes were hand-written WITHOUT capability manifests. A green corpus run said nothing at all about it; eighteen throwaway probes found it immediately. Not fixed here. The machinery exists (builtinCaps maps builtin -> cap, bodyCalls already walks bodies), but march's exact gating needs care: implementing it slightly too eagerly turns a false-accept class into a false-reject class.
The fix shape said implementing 1b too eagerly would flip a false-accept class into a false-reject one. That was true but vague enough to be useless to whoever picks it up. Names the three concrete hazards instead, each verified against march 6867c783: bodyCalls matches by NAME with no scope awareness (and the corpus already has shadowing cases that would fire); march scopes 1b to DIRECT builtin calls, so a stdlib-mediated call must not be scanned; and 1c stays a warning, so the two must not be flipped together.
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.
Two things, in this order: a proof layer over the capability checker, and a march-main resync that the proof work's CI change happened to expose.
1. A proof layer (P0)
march-leanhad zero theorems. Validation was 112native_decidepins,#evalexpectations, and the corpus — all of which check points, not properties. This adds 55 kernel-checked theorems and a CI gate so they stay honest.The capability lattice is now parameterized over an abstract
(name, parent)table (MarchLean/Calculus/Lattice.lean), with the shippingCapLatticeAPI as its specialization tohierarchy— same names, same signatures, definitionally equal. Consequences: the metatheory is proved once for any well-formed table, so adding a capability to march's table re-runs onedecideand touches no proof; and transitivity/antisymmetry are structural inductions rather than an 8,000-triple computation over strings.What is proved:
subsumesIn_refl,_trans,_antisymm, plussiblings_incomparableand the FFI base case (a name absent from the table subsumes only itself).ancestorsIn_fuel_adequate.CapLattice.leanasserted in prose thathierarchy.lengthis safe "because the table is a finite forest with no cycles." Nothing verified that. NowWellFormedB(no duplicate names, closed parents, acyclic) is a decidable proposition,Calculus/Concrete.leandischarges it for march's 20 entries bydecide, and if march ever ships a cycle or a duplicate the build fails there, loudly. Verified by negative control: adding a self-parent row makes thedecidefail; reverted.normalizepreserves coverage —coveredIn_normalizeIn, the lemma that licenses applyingnormalizeto aneedslist at all. It depends on antisymmetry, so it dies exactly when the table gains a cycle. PlusnormalizeIn_idem,coveredIn_mono.andThenis a monoid withviolationabsorbing;tierOfis a homomorphism ontoTier.max, i.e. verdict tiers are fold-order-independent even though messages are leftmost-wins by design.DivVerdict.joinis a bounded semilattice, sojoinAllis permutation-invariant.No mathlib, no new dependencies —
lake-manifest.jsonstays"packages": [].CI:
sorryis a warning in Lean, not an error, solake buildalone would pass with unproven theorems. Added a source grep that fails the run, plus building theMarchLeanlibrary (the workflow only built the executable, so proof files would not have been compiled at all).Axiom audit — all theorems depend only on
propext/Quot.sound, neversorryAx;hierarchy_wellFormeddepends on no axioms at all.2. march main resync
The CI pin was 71 commits stale (
7c1d701c), and themarchbinary on PATH locally was staler still (opam 0.2.0). Repinning to6867c783surfaced five verdict-changing divergences, four of them false ACCEPTS. All fixed here.reject/t149_cap_variant_arg_undeclaredcapsInSignaturescanned onlyDFnparams, so aCap(X)in a variant constructor argument escapedneedsentirelyreject/t151_cap_body_annotation_undeclaredreject/t152_root_cap_is_ambient_authorityroot_capwas an ambient globalaccept/t148_cap_narrow_chainscap_narrow : Cap(IO) -> Cap(a), so no non-root holder could attenuatereject/t144_cap_derive_json_variant_argThe R4a fix is the one to read carefully. march retyped
cap_narrowto∀a b. Cap(a) → Cap(b)and moved subsumption into a deferred sweep. Retyping alone here would have traded one false reject for three false accepts:reject/t153(widen),t154(siblings) andt155(deferred widen) were rejecting only as a side effect of the old argument type failing to unify — nothing anywhere consulted the lattice.CapCheck.capNarrowViolationnow carries that guarantee explicitly, and the three still reject for the right reason.That also exposed a second-order gap:
Inferwas ignoringdfnreturn annotations, invisible while every builtin's result was pinned by its argument types.3. Four gaps the corpus cannot catch
Recorded in
specs/march-findings.md. These are live divergences against the pinned march with zero corpus witnesses, so a green run is not evidence about any of them:needs IO.FileRead("/etc")) — march emits scopes in a newscopesarray; ourDNeedsdecoder reads onlypaths. A scope never subsumes unscoped, so a narrow declaration decodes as the broadest possible one: a false accept by construction.Tagged— march'scaps_in_tynow recurses into it; ours still mirrors the arm march deleted.normalize— march's dedupes, ours does not. Latent: not on the verdict path.Gaps 1 and 3 have teeth and point opposite ways. Both need hand-built probes.
Verification
Against march
6867c783built from source, 277 files:Ledger 177 → 203 entries, purely additive (zero stale).
accept/t49_transitive_use_coveredregressed MATCH → SKIP and is annotated as such: march#209 rewrote it to add a stdlib call, march accepts it, and march's own--emit-core-astemitsresolved_ty: TErrorfor that call — H3 honest-skips onTError, which is correct. A3 slice (a) now holds 10 of the 11 files it claimed; the inconsistency is march-side.Not done
P1 (de-partializing the 20 tree walks) and P2 (the three whole-checker theorem/counterexample pairs) from the design doc are outstanding. P2 depends on P1.