docs(findings): verify the choreography fixtures; record the --emit-core-ast verdict drift - #25
Merged
Merged
Conversation
…ct drift A full conformance run against march main HEAD (3ebe6c17) while mirroring the new choreography/endpoints corpus fixtures turned up two things. 1. march's --emit-core-ast computes its JSON "verdict" field before the --check path lowers to TIR for `cap no_alloc` and stdlib-mediated ceiling checks, so three reject fixtures emit verdict=accept while --check rejects them. That is MARCH_SELF_INCONSISTENT, a hard harness failure with no ledger to absorb it. Recorded as a march-is-wrong finding. 2. The choreography fixtures (t270, t273, t271/t272, t274-t279, t263 reject, p38, r17) all SKIP cleanly -- no MISMATCH, no known-limitation needed -- but cannot be added to scripts/expected-skips.txt yet: conformance.yml still pins march at 6867c783, which predates all of them, so an entry for any of them is a stale-entry SKIP-LEDGER MISMATCH (the same trap PR #24 hit). The verified ledger lines are recorded verbatim for the pin bump, along with the measured cost of that bump (+125 skips, 1 stale rename) and its two blockers: the t262 module-level-let-annotation MISMATCH (a real checker gap, not a known-limitation candidate) and the three files in (1). Ledgers unchanged; no behavior change.
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
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.
What this is
Docs only. No ledger change, no checker change.
I set out to mirror march's new choreography/endpoints fixtures into
scripts/expected-skips.txt. They cannot be added yet, for a reason this repoalready documented and PR #24 already hit:
conformance.ymlpins march(binary and corpus) at
6867c783(2026-08-08, now 1057 commits back), andnone of these files exist in that checkout, so a ledger entry for any of them
is a stale-entry SKIP-LEDGER MISMATCH against CI's actual corpus.
So instead of a ledger edit that would turn CI red, this records the
verification and the measured cost of the pin bump that would let it land.
Fixtures verified (march main HEAD
3ebe6c17,march-lean-checkat this repo's HEAD)Every one SKIPs cleanly. None is a MISMATCH; none needs a
known-limitations.txtentry.accept/t270_endpoints_labelled_stepsaccept/t273_crash_branches_loggingreject/t271_endpoints_label_on_branch_headreject/t272_endpoints_label_msg_prefixreject/t274_crash_receive_without_branchreject/t275_crash_branch_on_reliable_senderreject/t276_crashed_role_in_own_crash_branchreject/t277_crash_third_party_not_toldreject/t278_crash_choose_two_detectorsreject/t279_may_crash_unknown_rolereject/t263_endpoints_payload_without_json_codecgrammar/parse/p38_protocol_labelled_message_stepgrammar/reject/r17_protocol_label_after_arrowThere is no
accept/t263_…payload-codec fixture — accept-sidet263ist263_linear_opt_in_second_param, unrelated. The payload-codec fixture is thereject-side one above.
The ledger lines are recorded verbatim in
specs/march-findings.md, padded tothe file's column, ready to paste when the pin bumps.
New march-is-wrong finding:
--emit-core-ast'sverdictdisagrees with--checkbin/main.mlbindshas_user_errorsfrom the diagnostic set and hands it toEmit_core_ast.runas~rejected:before the--checkpath lowers to TIRto judge
cap no_allocallocation contracts and the stdlib-mediatedcapability-ceiling checks. Three reject fixtures therefore emit
"verdict": "accept"whilemarch --checkon the same file errors out:Also
reject/t180_ceiling_stdlib_mediated_under_checkandreject/t182_ceiling_module_let_stdlib_mediated. The hoist comment at thatbinding claims it is "the same accept/reject condition
--checkuses below";for these three it is not. The harness's step-4 self-consistency cross-check
is precisely what caught it — it reports
MARCH_SELF_INCONSISTENT, a hardfailure with no ledger to absorb it. Not yet reported upstream.
Measured cost of a pin bump to HEAD
Full run,
--corpus-dir+--lang-dirat march main3ebe6c17:The single stale entry is
accept/t77_refine_hof_bypass_limitation.march,which march renamed to
accept/t77_refine_hof_pass_site_rejected.march.Two blockers beyond the ledger:
reject/t262_toplevel_let_annotation_mismatch— hard MISMATCH. march nowchecks a module-level
let's annotation against its RHS(
let x : Int = "hello"); this checker's inference does not. Theannotation is present in the Core AST, so it is not a
known-limitations.txtcandidate (that file is gated to rejections erasedfrom the Core AST) — it is a real checker gap to fix.
MARCH_SELF_INCONSISTENTfiles above. No ledger category existsfor them and the cause is march-side, so nothing in this repo clears them.
A green bump therefore needs a checker fix for (1) and an upstream fix for
(2). Both are out of scope here.
CI
Docs-only diff, so the gate runs against the unchanged pin and stays green.