Repository navigation
MQ-2/3: body-lowering application views (#12199) + node_query call-reader cutover, readers deleted - #12202
Conversation
…d arguments no longer refuse the whole module gunbc#12145 stopped the operand reader narrowing a sequence to its left element, which had read h(q: a) as h and [a] as [. body_lower_call_arg_value read every argument with that reader alone, so a nested call, record, caret symbol or parenthesised group became call_argument_unread and its whole module refused normalize. An argument's value is now lowered by body_lower_value_lowered (the field-initializer / if-condition reader), with the operand reader as fallback. A parenthesised group lowers to its inner expression instead of its first atom. A list literal anywhere in an argument value still refuses, at the list (body_lowering_reason_list_literal_unlowered): body lowering has no lowered form for a list literal yet, so reading it would trade a refusal for a silent drop. Witness: v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…e no longer refuses the whole match
body_lower_match_scrutinee_optional read the scrutinee with the operand reader
alone: before gunbc#12145 match t(p: x) {..} narrowed to t, after it the match
refused as match_arm_navigation_refused (64 of the 133 still-refusing sample
modules). The scrutinee now goes through body_lower_value_lowered, operand reader
as fallback, refusal propagated. Witness claim: an undeclared name inside a call
scrutinee refuses at resolve at its atom.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-read' into session/deep-bear-733
…oduction-fed shape contracts Views live beside their constructors in v2.std.compilers.body_lowering and refuse, typed and located, on any partial shape (wrong arity, unexpected edge, surface residue). Claims in v2.test.claim.namespace_xl0.body_shape_contract read source text through the real front end. Bind/branch are red on the producer and enrolled expected-red. Presence-only call rows renamed to reachability names. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…istinct not-this/refused arms; view_at fallback removed; declared frontier for the node_query cutover Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…clared once), empty residue still refuses Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…er constant, seed-growth row, operand typing, real-marshal inhabitance claim
…arker declared once), empty residue still refuses" This reverts commit f0a42a0.
…marker declared once), empty residue still refuses" This reverts commit 622c714.
|
Blocking source finding on draft head
Please make the distinction unforgeable through an existing provenance/branded carrier or keep it at a route-specific skeleton boundary rather than globally recognizing a shape. Add a discriminator constructing the same ordinary shape outside the host marshal and require that it is not accepted as the seed opaque leaf. Also census/qualify the full The production-consumer cutover should remain draft until that boundary is resolved; MQ-5 can still own eventual deletion of the seed representation. |
…y, not source-to-lowered completeness Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…perand (marker declared once), empty residue still refuses"" This reverts commit 3e1f97a.
… input type per gentle-koi-724)
…ment keyed on FnArrowDecl; head-only lenses on the base read
…ruct-tag and call spellings, patterns exempt); wall test with production-fed FnArrowDecl RED/GREEN
… module (single-constructor rule)
|
Probe for the failing export GUNBC_MEMORY_BUDGET_BYTES=24000000000
cat > src/v2/test/claim/machine_shape_destructure_probe.dag <<'PROBE'
module v2.test.claim.machine_shape_destructure_probe
import v2.compiler.reference_conservation_admission { conserved_normalize, no_explained_drops }
import v2.lens.machine_shape { machine_shape_compile_gate }
import v2.std.compilers.lexing { symbol_lexeme }
import v2.std.diagnostic { Accepted, Diagnostic, Rejected }
import v2.std.text { String }
import v2.test.claim.machine_shape_construction_wall { machine_shape_destructured_subject }
fn diag_text(acc: String, d: Diagnostic) -> String {
concat(acc, concat(symbol_lexeme(sym: d.reason), "; "))
}
fn machine_shape_destructure_probe() -> String {
match conserved_normalize(subject: machine_shape_destructured_subject(), explained: no_explained_drops()) {
Rejected { diagnostics: d } => concat("NORMALIZE REFUSED: ", fold(d.tail, init: diag_text(acc: "", d: d.head), f: fn(a, x) { diag_text(acc: a, d: x) }))
Accepted { value: tree, diagnostics: _ } =>
match machine_shape_compile_gate(node: tree.root) {
Accepted { value: _, diagnostics: _ } => "GATE ACCEPTED"
Rejected { diagnostics: d } => concat("GATE REFUSED: ", fold(d.tail, init: diag_text(acc: "", d: d.head), f: fn(a, x) { diag_text(acc: a, d: x) }))
}
}
}
PROBE
cargo build --release -p v1-compiler --bin gunbc 2>&1 | tail -1
B=target/release/gunbc; [ -x $B ] || B=/cargo-target/release/gunbc
timeout 1200 $B run --source-root dag --source-root src/v2 --entry src/v2/test/claim/machine_shape_destructure_probe.dag --function machine_shape_destructure_probe 2>&1 | grep -vE 'floor-phase|floor-drain|memory-cgroup' | tail -8 |
… control (patterns don't reach the admitted route: conservation drops their references, probed on srv1)
…d per edge) and partitions once
…erand classification); fn_index, determinism and machine_shape read heads through it; an Atom head skips the residue probe
briansrls
left a comment
There was a problem hiding this comment.
Exact-head review of d6e449a75a76022fc7dd5cc793f3b42bd1effc7a: the prior forgeable-unprojected-leaf blocker is closed. The seed marker/change is gone; the real marshal probe supports the two-layer application_head_read / application_slots split; the old node_query readers are deleted in the same transition; the internal-Node-consistency boundary from #12199 is preserved.
One blocking consumer defect remains in src/v2/lens/no_dual_representation_test/scan.dag.
argument_value_read returns FirstArgName { name: "" } for every value that is neither an Atom nor a single-positional-child Conj, and first_call_arg_read returns the same arm when there is no operand. It also reads operand 0 without establishing that the application has exactly one operand. classify_application_lhs then treats all of those as a successfully read argument name and may conclude “no violation” (or run the single-argument alpha-equivalence judgment while silently ignoring extra operands).
That reintroduces the exact conflation this cutover is intended to remove: unsupported/unreadable structure is represented as a plausible value rather than a typed frontier. The new FirstArgUnreadable / EqOperandUnreadable path covers the empty-Conj specimen, but not the rest of the reader's unsupported domain.
Please make the result total at this consumer's actual grain, for example by distinguishing absent/not-single-argument from a readable name and from unreadable value structure. Require exactly one operand before applying body_alpha_equivalent_to_single_arg_call; route a non-Atom value or a wrapper with non-single-positional structure to the typed unreadable arm unless a real value-substitution judgment is implemented. Add discriminators for: zero arguments (not a single-arg subject), one wrapped Atom (readable), one wrapped empty/non-Atom value (unreadable), and two operands (must not be judged by silently reading only operand 0).
After that repair, re-run the affected no-dual-representation claims and a mutation that restores the empty-string fallback. The rest of this exact-head source direction is acceptable. Non-blocking integration note: when #12208 rebases, its canonical list-introduction Transform is explicitly not an application, so the application reader/consumer stack must not report that known form as a malformed application.
…rs -- NotSingleArgument (not judged), a readable name, unreadable (EqOperandUnreadable); exactly one operand required; no empty-name fallback; controls for 0/2 operands, wrapped atom, wrapped empty, wrapped structured
|
Claim-run script for head 1ebb12d (review 5311472065 fix). It adds M4, which restores the empty-name fallback for a structured argument and must turn one_wrapped_structured_argument_is_unreadable red. The main run picks up the five new single-argument controls through the grep. set -u
export GUNBC_MEMORY_BUDGET_BYTES=24000000000
T0=$(date +%s)
echo "### build $(date -u +%T)"
cargo build --release -p v1-compiler --bin claim_batch 2>&1 | tail -2
B=target/release/claim_batch
[ -x $B ] || B=/cargo-target/release/claim_batch
echo "### built in $(( $(date +%s)-T0 ))s"
# Fixture-grain claims of the touched modules; live corpus walks (names with _live_ or roster_gate/live integration) are excluded by name.
FILES="
src/v2/test/claim/enforcement/skeleton_call_route_witness_test.dag
src/v2/test/claim/machine_shape_construction_wall_test.dag
src/v2/test/claim/manual/call_carrier_node_query_test.dag
src/v2/test/claim/manual/body_lowering_infix_test.dag
src/v2/test/claim/body_lowering_block_body_call_test.dag
src/v2/test/lens_determinism/reach_witness_test.dag
src/v2/test/claim/enforcement/determinism_transitive_witness_test.dag
src/v2/test/claim/long/effect_reach_test.dag
src/v2/test/claim/long/live_read_classification_test.dag
src/v2/test/claim/self_host/production_qualification_origin_probe_witness_test.dag
src/v2/test/claim/no_dual_representation_test/lens_unit/controls_test.dag
src/v2/test/claim/namespace_xl0/body_shape_contract_test.dag
src/v2/test/lens_registry/sg_claims_test.dag
src/v2/test/claim/namespace_xl0/value_position_whole_read_test.dag
"
args() {
for f in $FILES; do
fns=$(grep -oE '^test fn [a-z0-9_]+' $f | awk '{print $3}' | grep -vE "$1" | paste -sd, -)
[ -n "$fns" ] && printf -- '--entry %s --functions %s ' "$f" "$fns"
done
}
EXCL='live|roster_gate'
echo "### MAIN RUN $(date -u +%T)"
timeout 2400 $B --source-root dag --source-root src/v2 $(args "$EXCL") 2>&1 | grep -vE 'floor-phase|floor-drain|memory-cgroup' | tail -250
echo "### main exit=$? elapsed $(( $(date +%s)-T0 ))s"
echo "### MUTATION RUN (each mutation must turn its named control RED)"
# M1 scan treats an unprojected (empty) argument as a value; M2 machine_shape stops reading the record-literal construct tag; M3 body route admits residue operands
sed -i 's/^ FirstArgUnreadable$/ FirstArgName { name: "" }/' src/v2/lens/no_dual_representation_test/scan.dag
grep -c '^ FirstArgName { name: "" }$' src/v2/lens/no_dual_representation_test/scan.dag # M1 applied: must print 1
# M4 restores the empty-name fallback for a structured value
sed -i 's/^ _ => FirstArgUnreadable$/ _ => FirstArgName { name: "" }/' src/v2/lens/no_dual_representation_test/scan.dag
sed -i 's/ match construct_tag_optional(n: n) {/ match optional_absent() {/' src/v2/lens/machine_shape.dag
sed -i 's/ ResidueOperand { node: n } => view_refusal(reason: ^body_view_operand_residue, at: n)/ ResidueOperand { node: n } => outcome_accepted(value: list_snoc_item(xs: xs, item: n))/' src/v2/std/compilers/body_lowering.dag
git diff --stat
timeout 1800 $B --source-root dag --source-root src/v2 \
--entry src/v2/test/claim/enforcement/skeleton_call_route_witness_test.dag --functions argument_value_read_refuses_a_wrapped_unprojected_value,one_wrapped_structured_argument_is_unreadable,the_real_skeleton_call_reads_through_application_read_with_the_declared_callee,body_route_refuses_an_empty_conj_operand \
--entry src/v2/test/claim/machine_shape_construction_wall_test.dag --functions gate_red_machine_shape_record_literal_outside_its_home \
2>&1 | grep -vE 'floor-phase|floor-drain|memory-cgroup' | tail -60
git checkout -- src
echo "### done elapsed $(( $(date +%s)-T0 ))s" |
|
Corrected claim-run script for head 1ebb12d. The main run is no longer truncated by tail -250: it writes main.log, prints PASS/FAIL counts against the selected count, lists FAILs, and reports each of the five new single-argument controls by name. Mutations are unchanged (M1–M4). set -u
export GUNBC_MEMORY_BUDGET_BYTES=24000000000
T0=$(date +%s)
echo "### build $(date -u +%T)"
cargo build --release -p v1-compiler --bin claim_batch 2>&1 | tail -2
B=target/release/claim_batch
[ -x $B ] || B=/cargo-target/release/claim_batch
echo "### built in $(( $(date +%s)-T0 ))s"
# Fixture-grain claims of the touched modules; live corpus walks (names with _live_ or roster_gate/live integration) are excluded by name.
FILES="
src/v2/test/claim/enforcement/skeleton_call_route_witness_test.dag
src/v2/test/claim/machine_shape_construction_wall_test.dag
src/v2/test/claim/manual/call_carrier_node_query_test.dag
src/v2/test/claim/manual/body_lowering_infix_test.dag
src/v2/test/claim/body_lowering_block_body_call_test.dag
src/v2/test/lens_determinism/reach_witness_test.dag
src/v2/test/claim/enforcement/determinism_transitive_witness_test.dag
src/v2/test/claim/long/effect_reach_test.dag
src/v2/test/claim/long/live_read_classification_test.dag
src/v2/test/claim/self_host/production_qualification_origin_probe_witness_test.dag
src/v2/test/claim/no_dual_representation_test/lens_unit/controls_test.dag
src/v2/test/claim/namespace_xl0/body_shape_contract_test.dag
src/v2/test/lens_registry/sg_claims_test.dag
src/v2/test/claim/namespace_xl0/value_position_whole_read_test.dag
"
args() {
for f in $FILES; do
fns=$(grep -oE '^test fn [a-z0-9_]+' $f | awk '{print $3}' | grep -vE "$1" | paste -sd, -)
[ -n "$fns" ] && printf -- '--entry %s --functions %s ' "$f" "$fns"
done
}
EXCL='live|roster_gate'
echo "### MAIN RUN $(date -u +%T)"
SEL=0; for f in $FILES; do SEL=$(( SEL + $(grep -oE '^test fn [a-z0-9_]+' $f | awk '{print $3}' | grep -vcE "$EXCL") )); done
echo "### selected claims: $SEL"
timeout 2400 $B --source-root dag --source-root src/v2 $(args "$EXCL") > main.log 2>&1
echo "### PASS $(grep -c '^PASS ' main.log) FAIL $(grep -c '^FAIL ' main.log) (PASS+FAIL must equal selected)"
grep '^FAIL ' main.log
for c in a_call_with_no_argument_is_not_a_single_argument_call a_call_with_two_arguments_is_not_a_single_argument_call one_wrapped_atom_argument_reads_its_name one_wrapped_empty_argument_is_unreadable one_wrapped_structured_argument_is_unreadable; do grep -E "^(PASS|FAIL) $c\b" main.log || echo "ABSENT $c"; done
echo "### main exit=$? elapsed $(( $(date +%s)-T0 ))s"
echo "### MUTATION RUN (each mutation must turn its named control RED)"
# M1 scan treats an unprojected (empty) argument as a value; M2 machine_shape stops reading the record-literal construct tag; M3 body route admits residue operands
sed -i 's/^ FirstArgUnreadable$/ FirstArgName { name: "" }/' src/v2/lens/no_dual_representation_test/scan.dag
grep -c '^ FirstArgName { name: "" }$' src/v2/lens/no_dual_representation_test/scan.dag # M1 applied: must print 1
# M4 restores the empty-name fallback for a structured value
sed -i 's/^ _ => FirstArgUnreadable$/ _ => FirstArgName { name: "" }/' src/v2/lens/no_dual_representation_test/scan.dag
sed -i 's/ match construct_tag_optional(n: n) {/ match optional_absent() {/' src/v2/lens/machine_shape.dag
sed -i 's/ ResidueOperand { node: n } => view_refusal(reason: ^body_view_operand_residue, at: n)/ ResidueOperand { node: n } => outcome_accepted(value: list_snoc_item(xs: xs, item: n))/' src/v2/std/compilers/body_lowering.dag
git diff --stat
timeout 1800 $B --source-root dag --source-root src/v2 \
--entry src/v2/test/claim/enforcement/skeleton_call_route_witness_test.dag --functions argument_value_read_refuses_a_wrapped_unprojected_value,one_wrapped_structured_argument_is_unreadable,the_real_skeleton_call_reads_through_application_read_with_the_declared_callee,body_route_refuses_an_empty_conj_operand \
--entry src/v2/test/claim/machine_shape_construction_wall_test.dag --functions gate_red_machine_shape_record_literal_outside_its_home \
2>&1 | grep -vE 'floor-phase|floor-drain|memory-cgroup' | tail -60
git checkout -- src
echo "### done elapsed $(( $(date +%s)-T0 ))s" |
…d every site matches on OperandSlot (the Bool predicate is gone); operator roster membership uses v2.std.algebra contains
|
Review 71101 addressed in e219364.
Behaviour is unchanged: every refusal keeps its reason and its locus. CI will re-run on the new head. |
briansrls
left a comment
There was a problem hiding this comment.
APPROVED at exact head e2193642fcde08ab2337c7a3eacd9541800178a6.
Review 5311472065 is closed. The no-dual-representation consumer now has the required three-way result: NotSingleArgument, FirstArgName, or FirstArgUnreadable; it requires exactly one operand, and no unsupported shape or absence is encoded as the plausible name "". The zero-argument, two-argument, wrapped-atom, wrapped-empty, and wrapped-structured controls exercise the partition, and restoring the empty-name fallback reddens the structured control.
The earlier forgeable opaque-leaf/seed change remains absent. operand_slot_of is now the single residue classifier used by the view stack, while the old node_query call readers are deleted in the same transition and every production consumer carries a typed refusal channel. All five checks completed successfully on this exact head.
No remaining blocker in #12202. The stated landing order with #12208 is acceptable: when #12208 rebases second, its flat FreeMonoid introduction must add the specialized non-application classification without weakening this application-reader cutover, and that new exact head needs its own review.
…d = main's projection + the callees_from_decl rename
… bare-provider gate)
…as ImportsFixed (the explicit v2.std.live_read import discharges them)
|
CI at 96b3a13: floor is the only real failure (witnesses just aggregates it), and its single refusal is a main-side seed defect from #12205, not this PR. required_floor_runner.rs unimported_bare_provider_roster_at_base accepts only a record, but the .dag authority returns the variant BaseRosterShown / BaseRosterUnreadable. The failure reads 'returned Variant(BaseRosterShown), expected UnimportedBareProviderBaseRoster'. It fires on any PR that edits the bare-provider debt roster, and this PR must retire 23 rows there because of its explicit v2.std.live_read import. The fix is #12278 (swift-owl-708). Per the MQ lane (gentle-koi-724), this PR does not carry a copy: it waits for #12278, then merges main and re-runs. — sent from warm-ram-650 |
briansrls
left a comment
There was a problem hiding this comment.
Re-review of exact head dfd2331b0e1d384978dbb3664f9423891a53a3d5: APPROVED.
The MQ-2/3 cutover previously approved at e2193642fcde08ab2337c7a3eacd9541800178a6 is semantically unchanged. The branch-native delta is limited to:
- explicit
v2.std.live_read { LiveReadUnestablished }imports inlive_read_classification.dagand its long witness, satisfying #12205's import-closure rule; and - retirement of the 23 corresponding
(file,name)debt rows asImportsFixed.
That retirement is coherent with #12205's model: adding the provider module to the file's import closure discharges every rostered provider identity from that module, and the exact-head floor re-derived and accepted those retirements. The remaining commits are main merges; the cutover implementation, deleted-reader transition, typed refusal channels, single-argument three-way read, and mutation discriminators are unchanged.
Exact-head evidence is complete: PR is CLEAN/mergeable; workflow run 36133361807 has all five jobs green, including the required floor's nominal witness fold plus D0 receipt adjudication and both emitted-build subjects; srv1 reports 122 selected, 119 PASS, only the three enrolled expected-reds, and all five mutation controls red.
No remaining blocker at this head.
…reads as NOT an application - application_head_read: a Transform the list reader recognises answers NotApplicationHead before its head is classified, so application_slots / application_read and the head-only readers never read a list as a malformed call (agreed with warm-ram-650: the second of #12202/#12208 to land adds it). - list_introduction_elements_optional reads the head in BOTH forms: the marked declaration reference (post-resolve, #12220) and the bare qualified-name spine body lowering writes, since application_read also runs over lowered bodies. Safe because the path is compared for exact equality with the FreeMonoid path. - Controls: a lowered list argument and a resolved list introduction read as NotApplication; the call enclosing the list still reads as an Application. - Import conflicts resolved as unions with the moved fns from std.algebra. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Carries #12199 to main (per review 70865, §3 delete-first): the views land in the same transition that deletes the node_query readers. #12199 does not land alone. Synced to #12199 head
d06a6b6053d. #12206 lands first; this PR is then brought up to date with it and gets a fresh exact-head review. Child of the MQ pass (gentle-koi-724), work item "MQ-2 cutover: node_query call readers -> application_read".What changes
The six production consumers of
v2.std.node_querynode_is_call/call_callee_target/call_argument_targetsnow read calls throughv2.std.compilers.body_lowering. Those three readers,node_is_callee_reference, and the two privatenode_callee_symbolcopies (in the determinism and machine_shape lenses) are deleted in this PR, so no partial cutover is left standing (DESIGN §3). A refused application is never read as "not a call" (DESIGN §5): each consumer surfaces it, typed and located.application_head_read/application_slots(new, under MQ-2/3: admitted Call/Operator/Match/Bind/Branch views over Node + production-fed shape contracts #12199'sapplication_read) are the two layers of one base read. The head layer checks positional edges and a callee head and classifies no operands; it is used by fn_index, determinism and machine_shape, whose question is the head. The slots layer adds operand classification for the scan.application_slotsIt refuses a named edge, a missing or non-callee head, and a residue head. It marks residue operands instead of refusing them, for readers whose question is only the head.application_readisapplication_slotsplus: the first residue operand refuses, located. Its behaviour is unchanged. It is the one call reader for lowered bodies and host fn-arrow skeletons.v2.std.fn_indexapplication_readCalleeTextRead,callees_from_decl→CalleeScan { texts, refusals },call_reachable_decls*→CallReach { reached, refusals }. An Arrow head refuses with^fn_index_callee_head_unnamed.v2.lens.effect_reachEffectReachRefused { refusals }, its own arm rather than a widening.v2.lens.live_read_classificationLiveReadUnestablished { refusals }, which projects toLiveReadSelectionRefusedand never decides a skip.v2.lens.determinismapplication_slots(head only)DeterminismRead { axis, unread }.v2.lens.machine_shapeapplication_slots+ construct tagv2.lens.fn_index_depth_agreementapplication_readrefused_applicationsis counted, and the verdict refuses when it is non-zero.v2.lens.production_qualification_origin_probeMintSiteScan { sites, refusals }; admission refuses while refusals stand.v2.lens.no_dual_representation_test.scanapplication_slots+ argument value readEqOperandUnreadable.Correction: the premise this PR carried earlier was wrong
Earlier revisions said that a host skeleton call such as
f(1)would be refused as residue byapplication_read, because the marshal emits an empty Conj for an expression it does not project. On that basis I built first a seed-side marker leaf and then a skeleton-only reader (skeleton_application_read/SkeletonUnprojected) with anFnArrowDeclconstructor gate for provenance.A probe of the real marshal (
gunbc runoverfn_arrow_decl_facts_liveon a one-file fixture) shows that no producer makes that state.count(x), withxan unprojected data reference, marshals toTransform[Atom:count, Conj[Conj[]]]. EveryExprCallargument, named or positional, is a wrapper node that the marshal projects. The empty Conj sits inside the wrapper and never stands directly in an operand slot. The skeleton arm was therefore decoration (§4b), and it is deleted, together with theFnArrowDeclgate row whose only purpose was to support it. There is no seed change and no marker.Skeleton consumers that read argument CONTENT, not only callees
Skeleton arguments are wrappers over values that may be unprojected. Of the six consumers:
argument_value_read, and an empty Conj at the bottom isFirstArgUnreadable→EqOperandUnreadable, never inlined as a name.machine_shape: record-literal fix (a real bug found on the way)
The gate recognised only the call spelling
MachineShape(..). A real record literalMachineShape { .. }lowers to a construct, a Conj tagged by its first edge, so it passed unseen. The gate now also readsconstruct_tag_optional. Destructuring patterns (below amatch_arm_patternedge) are exempt. There are no existing violations.Controls
v2.test.claim.enforcement.skeleton_call_route_witnessbody_route_refuses_an_empty_conj_operand: residue directly in an operand slot refuses.the_real_skeleton_call_reads_through_application_read_with_the_declared_calleeis the route claim over the real marshal: exactly one application, 0 refusals, head equal to the declared calleecount, and the argument read as unprojected through its wrapper.the_real_skeleton_call_walk_names_the_callee_without_refusal.argument_value_read_reads_a_wrapped_nameandargument_value_read_refuses_a_wrapped_unprojected_value.v2.test.claim.machine_shape_construction_wallgate_red_machine_shape_record_literal_outside_its_homeis production-fed: real source, parsed and normalized.gate_green_machine_shape_record_literal_in_its_homeandgate_green_machine_shape_destructuring_pattern.application_read, with names kept because the floor roster keys them:manual/call_carrier_node_query_test,manual/body_lowering_infix_test, and the production-fedbody_lowering_block_body_call_test.Execution record
Current head
e2193642fcd(adds the review 71101 fix:operand_slot_ofis the one residue classifier):body_shape_bind_is_key_value_body_holds(MQ-2/3: admitted Call/Operator/Match/Bind/Branch views over Node + production-fed shape contracts #12199), plus #12145 follow-up: value-position regression controls, lambda-argument frontier enrolled expected-red, RFM receipts (no compiler change) #12198's two lambda claims.argument_value_read_refuses_a_wrapped_unprojected_value,one_wrapped_structured_argument_is_unreadable,the_real_skeleton_call_reads_through_application_read_with_the_declared_callee,body_route_refuses_an_empty_conj_operandandgate_red_machine_shape_record_literal_outside_its_home.Head
1ebb12d480efixes review 5311472065: the scan's single-argument read has three answers (NotSingleArgument/FirstArgName/FirstArgUnreadable), requires exactly one operand, and has no empty-name fallback.skeleton_call_route_witness_testrun on its own: 10/10 PASS, including the five new controls: zero args, two args, wrapped atom, wrapped empty, wrapped structured.one_wrapped_structured_argument_is_unreadableunder M4, which restores the empty-name fallback.tail -250, which dropped the first entry groups. The "106 PASS" figures are therefore counts of visible results, not totals: the script selects 122 claims. A FAIL in a dropped group would also have been hidden. The dropped groups wereskeleton_call_route_witness_test(since run on its own: 10/10 PASS) andmachine_shape_construction_wall_test, which CI's floor runs. The script in comment 5824233234 keeps the full log and counts against the selection.Current head
d6e449a75a7:body_shape_bind_is_key_value_body_holds(MQ-2/3: admitted Call/Operator/Match/Bind/Branch views over Node + production-fed shape contracts #12199's roster), plusa_lambda_argument_whose_body_uses_its_parameter_resolvesandan_undeclared_name_inside_a_lambda_argument_body_refuses_at_resolve_at_its_atom(#12145 follow-up: value-position regression controls, lambda-argument frontier enrolled expected-red, RFM receipts (no compiler change) #12198's frontier).long/live_read_classification_testpasses now that v1 infer: a qualified function name in value position is typed by its arrow, not its return (#12143 exposure) #12231 (the seed fix for roster_gate) is merged.argument_value_read_refuses_a_wrapped_unprojected_value,the_real_skeleton_call_reads_through_application_read_with_the_declared_callee,body_route_refuses_an_empty_conj_operandandgate_red_machine_shape_record_literal_outside_its_home.Earlier heads, for the record:
CI does not run on a PR stacked on a non-main base. Claims are run with the script in the latest PR comment; srv runs are by neat-boar-16.
Head
f602bad1e18(previous design): 105 PASS, 3 FAIL.body_shape_bind_is_key_value_body_holdsandbody_shape_branch_is_condition_then_else_holds.Head
3cfff08c075(current design), run on srv1 by neat-boar-16 (private clone, MemoryMax=40G) with the script in comment 5808521461:body_shape_bind_is_key_value_body_holdsandbody_shape_branch_is_condition_then_else_holds.argument_value_read_refuses_a_wrapped_unprojected_valueandthe_real_skeleton_call_reads_through_application_read_with_the_declared_calleewent RED.gate_red_machine_shape_record_literal_outside_its_homewent RED.body_route_refuses_an_empty_conj_operandwent RED.Head
1fa90917fac(merged with main after MQ-6: reference conservation as admission (fixture route + changed-scope receipt); repair XL-2 #12206; carries MQ-2/3: admitted Call/Operator/Match/Bind/Branch views over Node + production-fed shape contracts #12199 atd06a6b6), srv1, script in comment 5814088203. The run addedvalue_position_whole_read_test, a new-on-main user of the deleted readers, now cut over.body_shape_bind/branch(MQ-2/3: admitted Call/Operator/Match/Bind/Branch views over Node + production-fed shape contracts #12199) and the two lambda claims (#12145 follow-up: value-position regression controls, lambda-argument frontier enrolled expected-red, RFM receipts (no compiler change) #12198's frontier).long/live_read_classification_test.dag, failing at entry resolve insrc/v2/lens/complexity_accumulator_copy/roster_gate.dag(162:137, 163:137, 247:58: expected Node(fn), got Coproduct(Bool)). This is a pre-existing main defect: a control run on main1eda053f5f2fails identically, and this PR touches no file in that module or undersrc/v2/compilerorsrc/v1. neat-boar-16 is routing it to its own owner.CI at
ea79e5058e3: clippy, compiler and emit-build pass. The floor's only blocker is the pre-existingroster_gate.dagresolve defect (162:137, 163:137, 247:58). The floor is affected-set scoped, and this PR reaches that file throughlive_read_classification, so main's green floor does not. The defect is in the seed (v104_infertypes a qualified fn path in value position as its returnBool). It is owned by still-seal-357, and per neat-boar-16 it is not worked around here (§5). This PR waits on that fix, then merges main and re-runs.Two further stale callers of the renamed walk (
content_hash_combine_preimage_witness_test,text_egress_ambient_builtin_bypass_witness_test) are fixed oncallee_texts_in_decl. Their absence claims now also require zero refusals.Witness headroom note, for its owner:
test.claim.text_egress_ambient_builtin_bypass_witnessswitched_emit_orchestration_reaches_no_ambient_text_builtinmeasures 72,197 eval steps on main53828ae4b22, 103 under the 72,300 new-witness budget (srv1, neat-boar-16). Any change whose affected set reaches it re-judges it against that budget. This PR does not narrow it. Whether it needs a lane with its own ceiling is the owner's call. On this PR it went 105.5k → 92.3k → 71,709 atd6e449a75a7, below main (srv1, neat-boar-16). The cut was to the call walk, not to the witness: the head-only layerapplication_head_readclassifies no operands, an Atom head skips the residue probe, and the walk carries one tagged list per edge.🤖 Generated with Claude Code