Reshape the fn-arrow body skeleton so a call is a call: the marshal now emits the Transform carrier node_is_call accepts

dag/gunbc/recurring_failure_mode/check_subject_shape_cannot_represent_the_state_the_check_detects.dag

@@ -15,6 +15,12 @@ data check_subject_shape_cannot_represent_the_state_the_check_detects: Recurring
     "**RECOGNITION RULE, which is DESIGN 4b's own question asked BEFORE the check is written rather than after: name the state the check refuses, then construct a value in the subject's OWN representation that exhibits it.** If you cannot construct one, the check is a decoration over that subject however correct its logic. The construction is cheap and is the whole test: two values differing only in the field the check keys on, asserting it FIRES on one and is BLIND to the other. Both arms passing is the executing record of the gap; when the representation lands, the blind arm reds and names itself. ",
     "**THE REPORTING RULE THAT FOLLOWS: a class's rung is the minimum across its in-scope paths (4b(1)), so a fixture path where the RED is authorable does NOT stand in for a live path where it is not.** Citing the fixture rung while the live path is dark is rung inflation. **AND IT IS NOT A 4b(3) DECLARED DROP -- filing one is its own error**, which is where the specimen nearly went: 4b(3) governs a REGRESSION, with a previous rung and a population that LOST a guarantee. When the shape mismatch predates the check, the wall was never lit through that path, and a capability that was never real cannot be dropped. The honest instruments are 4b(1) rung honesty and 4b(2) an untracked stall made tracked. ",
     "**RUNG: 1 (mitigatable) -- the gap is nameable and, once found, held open by the two-arm control. CEILING: 4, since whether a subject's representation can inhabit the state a check matches on is decidable from two declarations the tree already carries. NEXT-RUNG TRIGGER, a CAPABILITY and not an artifact: a check declares the subject representation it matches over, and a check whose match is unsatisfiable by that representation fails to compile -- so the decoration cannot be authored at all, rather than being found later by someone constructing the value by hand.**)",
+
+    "**THE REPAIR LANDED AND ITS DIRECTION IS NOT SYMMETRIC: RESHAPE THE PRODUCER, NEVER WIDEN THE CHECK** (gunbc#10282, cool-fox-470, the reshape arm of the same specimen this row was filed from). `v1.stage0.coproduct_reflection` `marshal_generic` now returns a `ComputationNode { behavior: Transform }` record for an `ExprCall` with a non-empty authored name -- the case where the callee identity leaf is already the first positional edge -- so the subject representation gained the constructor the check matches on and the RED became authorable over the live substrate. The arm NOT taken is the one that looks equally available and is not: widening `node_is_call` to also accept the Conj spelling would have made the check green again by ratifying the fork, leaving the substrate with two definitions of a call and the compiler's own lowered-body carrier advisory. A check may not be taught the producer's spelling; the producer must emit the substrate's carrier. ",
+
+    "**THE FIELD TELL IS VISIBLE BY READING, BEFORE ANYTHING RUNS: A PRIVATE COPY OF THE SHARED PREDICATE.** `v2.lens.no_dual_representation_test.scan` carried `skeleton_is_call`, `skeleton_is_callee_atom` and `skeleton_call_argument_targets` -- `v2.std.node_query`'s `node_is_call` / `call_callee_target` / `call_argument_targets` respelled against `TypeNode { connective: Conj }` -- because the shared authority could not read its own substrate. A SECOND PREDICATE ANSWERING ONE QUESTION IS EVIDENCE THAT THE FIRST DOES NOT APPLY TO SOMEBODY'S INPUT, and it is a static, greppable symptom of this class that needs no execution to find. The fork and the defect shipped together: the workaround is what let the unrepresentable subject go unnoticed. It is deleted rather than parameterised in #10282, and `replace_param_in_output` in that same module -- which descended `Conj` alone -- would have returned every body containing a call UNSUBSTITUTED the moment the carrier appeared, a fail-open the repair itself would have created. ",
+
+    "**THE EVIDENCE SHAPE THAT SETTLES IT, AND THE ONE A .dag ROW CANNOT PROVIDE.** Two hand-built fixture nodes differing only in kind establish that the LENS discriminates; neither can establish that the PRODUCER emits the accepted shape, because both are constructed by the fixture -- which is the defect in miniature. That fact belongs in the producer's own test path: `marshaled_call_carries_the_transform_call_carrier`, with `marshaled_non_call_stays_a_conj_type_node` as its control, on the required `cargo test -p v1-compiler --lib` lane. Confirmed by mutation with the substitution asserted BEFORE any verdict was read: reverting `marshal_generic` to the unconditional Conj record reddens exactly that one test (4 passed, 1 failed) and restoring returns 5/5. The fixture pair stays enrolled as the 4b(4) regression control rather than retiring on the climb. "
   ],
 
   evidence: [],

src/v1/stage0/src/coproduct_reflection.rs

@@ -1065,6 +1065,41 @@ fn conj_record(ctx: &InterpContext, edges: Vec<Value>) -> Value {
     )
 }
 
+fn nullary_behavior_variant(ctx: &InterpContext, name: &str) -> Value {
+    Value::Variant {
+        type_name: ctx.sym("Behavior"),
+        variant_name: ctx.sym(name),
+        fields: Rc::new(vec![]),
+    }
+}
+
+fn node_kind_computation_node(ctx: &InterpContext, behavior: Value) -> Value {
+    Value::Variant {
+        type_name: ctx.sym("NodeKind"),
+        variant_name: ctx.sym("ComputationNode"),
+        fields: Rc::new(vec![(ctx.sym("behavior"), behavior)]),
+    }
+}
+
+// A CALL IS A CALL IN BOTH REPRESENTATIONS. `v2.std.node_query::node_is_call` recognises a call as
+// a `ComputationNode { behavior: Transform }` whose first positional child is a callee reference --
+// the shape `v2.compiler.body_lowering_fold` produces for the lowered body, and the shape every
+// call-shaped lens matches on. This marshal emitted `TypeNode { connective: Conj }` for EVERY node
+// including calls, so `node_is_call` was false on every skeleton node the corpus can produce, and
+// each lens folding a skeleton through it (`v2.lens.determinism` transitive findings,
+// `v2.lens.machine_shape`, the origin probe's call walk) was GREEN BY CONSTRUCTION: the state it
+// refuses had no constructor on its own input. That is DESIGN §4b's decoration -- worse than an
+// absent check, because it was cited as coverage -- and its §3 receipt was already standing in
+// `v2.lens.no_dual_representation_test.scan`, which carried a SECOND call predicate spelled against
+// the Conj shape because the shared one could not answer here.
+fn transform_record(ctx: &InterpContext, edges: Vec<Value>) -> Value {
+    node_record(
+        ctx,
+        node_kind_computation_node(ctx, nullary_behavior_variant(ctx, "Transform")),
+        edges,
+    )
+}
+
 fn marshal_skeleton(
     ctx: &InterpContext,
     node: &Rc<Node>,
@@ -1188,7 +1223,18 @@ fn marshal_generic(
             refs.remove(&pname);
         }
     }
-    (conj_record(ctx, edges), refs)
+    // The callee atom is `edges[0]` on exactly this condition: an `ExprCall` with a non-empty
+    // authored name takes either the parameter-reference arm or the callee-atom arm above, and both
+    // push the identity leaf before any child skeleton. A call through an unnamed callee expression
+    // stays `Conj` -- it has no callee reference to be first, so `node_is_call` would refuse it
+    // anyway, and claiming the Transform kind without one would be the shape without the fact.
+    let is_call_shaped =
+        matches!(node.expr_data.as_ref(), ExprData::ExprCall { .. }) && !name.is_empty();
+    if is_call_shaped {
+        (transform_record(ctx, edges), refs)
+    } else {
+        (conj_record(ctx, edges), refs)
+    }
 }
 
 // A statement sequence -- a block's children, or a standalone `let` (optional children[1] is
@@ -2340,6 +2386,162 @@ mod parse_only_uppercase_variant_regression_tests {
         );
     }
 
+    fn call_expr(
+        callee: &str,
+        args: Vec<Rc<crate::v1_std_core::Node>>,
+    ) -> Rc<crate::v1_std_core::Node> {
+        make_named_expr_node(
+            Rc::new(crate::std_occurrence_identity::NodeOccurrenceIdentity::OccurrenceSynthetic),
+            callee.to_string(),
+            Rc::new(ExprData::ExprCall {
+                call_semantics: None,
+                descent_evidence: None,
+            }),
+            Rc::new(args.into()),
+            None,
+            dummy_span(),
+            dummy_span(),
+        )
+    }
+
+    fn var_expr(name: &str) -> Rc<crate::v1_std_core::Node> {
+        make_named_expr_node(
+            Rc::new(crate::std_occurrence_identity::NodeOccurrenceIdentity::OccurrenceSynthetic),
+            name.to_string(),
+            Rc::new(ExprData::ExprVar { binding_kind: None }),
+            empty_node_list(),
+            None,
+            dummy_span(),
+            dummy_span(),
+        )
+    }
+
+    fn field(ctx: &InterpContext, value: &Value, key: &str) -> Option<Value> {
+        match value {
+            Value::Record { fields, .. } => {
+                let k = ctx.sym(key);
+                fields
+                    .iter()
+                    .find(|(fk, _)| *fk == k)
+                    .map(|(_, v)| v.clone())
+            }
+            _ => None,
+        }
+    }
+
+    fn variant_field(ctx: &InterpContext, value: &Value, name: &str) -> Option<Value> {
+        match value {
+            Value::Variant { fields, .. } => {
+                let key = ctx.sym(name);
+                fields
+                    .iter()
+                    .find(|(k, _)| *k == key)
+                    .map(|(_, v)| v.clone())
+            }
+            _ => None,
+        }
+    }
+
+    fn variant_is(ctx: &InterpContext, value: Option<&Value>, expected: &str) -> bool {
+        matches!(
+            value,
+            Some(Value::Variant { variant_name, .. }) if *variant_name == ctx.sym(expected)
+        )
+    }
+
+    // THE WHOLE ACCEPTED SHAPE, NOT ITS OUTER TAG. `node_is_call` reads two nested variants -- the
+    // kind's `behavior` and the callee child's `connective` -- so a probe asserting only
+    // `ComputationNode` and `TypeNode` is satisfied by a marshal emitting `behavior: Loop` over a
+    // `connective: Conj` child, which `node_is_call` refuses. That is the §5 tell in this module's
+    // own test: an assertion that passes while the realization lies. These two read the full path.
+    fn is_transform_computation_node(ctx: &InterpContext, skel: &Value) -> bool {
+        match field(ctx, skel, "kind") {
+            Some(kind) => {
+                variant_is(ctx, Some(&kind), "ComputationNode")
+                    && variant_is(
+                        ctx,
+                        variant_field(ctx, &kind, "behavior").as_ref(),
+                        "Transform",
+                    )
+            }
+            None => false,
+        }
+    }
+
+    fn is_atom_type_node(ctx: &InterpContext, skel: &Value) -> bool {
+        match field(ctx, skel, "kind") {
+            Some(kind) => {
+                variant_is(ctx, Some(&kind), "TypeNode")
+                    && variant_is(
+                        ctx,
+                        variant_field(ctx, &kind, "connective").as_ref(),
+                        "Atom",
+                    )
+            }
+            None => false,
+        }
+    }
+
+    fn is_conj_type_node(ctx: &InterpContext, skel: &Value) -> bool {
+        match field(ctx, skel, "kind") {
+            Some(kind) => {
+                variant_is(ctx, Some(&kind), "TypeNode")
+                    && variant_is(
+                        ctx,
+                        variant_field(ctx, &kind, "connective").as_ref(),
+                        "Conj",
+                    )
+            }
+            None => false,
+        }
+    }
+
+    fn first_child_target(ctx: &InterpContext, skel: &Value) -> Option<Value> {
+        match field(ctx, skel, "children") {
+            Some(Value::List(items)) => items
+                .iter()
+                .next()
+                .and_then(|edge| field(ctx, edge, "target")),
+            _ => None,
+        }
+    }
+
+    // THE DISCRIMINATING PAIR FOR THE CALL CARRIER. `v2.std.node_query::node_is_call` accepts a
+    // node only when its kind is `ComputationNode { behavior: Transform }` AND its first positional
+    // child is a callee reference. Before this marshal emitted the carrier, the first assertion
+    // below read `TypeNode` for every node the corpus could produce, so every call-shaped lens over
+    // a skeleton was green with no reachable red. The second row is the control that keeps the fix
+    // from degenerating into "everything is a call".
+    #[test]
+    fn marshaled_call_carries_the_transform_call_carrier() {
+        let ctx = test_ctx();
+        let si = ctx.source_indices();
+        let (skel, _) =
+            marshal_generic(&ctx, &call_expr("map_keys", vec![var_expr("m")]), &[], &si);
+        assert!(
+            is_transform_computation_node(&ctx, &skel),
+            "a marshaled call must carry ComputationNode {{ behavior: Transform }} -- the exact \
+             kind node_is_call matches, behavior included"
+        );
+        let callee = first_child_target(&ctx, &skel).expect("call skeleton has a first child");
+        assert!(
+            is_atom_type_node(&ctx, &callee),
+            "the first positional child must be TypeNode {{ connective: Atom }} -- node_is_call's \
+             second predicate, node_is_callee_reference, accepts only Atom or Arrow"
+        );
+    }
+
+    #[test]
+    fn marshaled_non_call_stays_a_conj_type_node() {
+        let ctx = test_ctx();
+        let si = ctx.source_indices();
+        let (skel, _) = marshal_generic(&ctx, &var_expr("m"), &[], &si);
+        assert!(
+            is_conj_type_node(&ctx, &skel),
+            "only a call node may carry the call carrier; everything else stays TypeNode {{ connective: Conj }}"
+        );
+    }
+
     #[test]
     fn capitalization_heuristic_not_used_on_parse_only_path() {
         let source = include_str!("coproduct_reflection.rs");

src/v2/lens/determinism.dag

@@ -241,38 +241,42 @@ data construction_justification: ConstructionJustification = ConstructionJustifi
 // its own entry file, which is both the substrate declaration and what makes it unskippable by
 // affected-set selection; it reads exactly the roots it names, since fn_arrow_decl_facts_live now
 // takes pool_roots and the same roots bind the closure it walks; and it is an ordinary
-// required-floor row, not a long-lane or cadence one. IT HAS NO FAILURE THAT REACHES ANYTHING,
-// because through this substrate it cannot fail at all, and a consumer that cannot fail does not
-// discharge a clause about where its failure lands.
+// required-floor row, not a long-lane or cadence one. THE FOURTH -- that its failure reaches the
+// floor -- WAS UNMET FOR THE STRONGEST POSSIBLE REASON UNTIL gunbc#10282: through this substrate it
+// could not fail at all, and a consumer that cannot fail does not discharge a clause about where
+// its failure lands. That reason is gone; what remains open is stated two paragraphs down and is a
+// reachability question rather than a representation one.
 //
-// THE MECHANISM, named at the symbols rather than described, because "the wall is dark" is the kind
-// of claim that has to be checkable. `v1_compiler.coproduct_reflection` `marshal_skeleton` returns
-// `conj_record` at both of its return sites, and `conj_record` builds every node as
-// `TypeNode { connective: Conj }`. `v2.std.node_query` `node_is_call` matches
-// `ComputationNode { behavior: Transform }` and answers false on everything else. A Conj TypeNode
-// cannot satisfy that match, so `node_callee_symbol` is Absent at every node of every fn-arrow body
-// skeleton, `local_determinism_axis` returns Deterministic unconditionally, and
-// `determinism_transitive_holds` over a `fn_arrow_decl_facts_live` population is GREEN BY
-// CONSTRUCTION. This is DESIGN §4b's own question asked too late: the check's RED is not authorable
-// over this subject shape, so the row carries no information while looking exactly like coverage.
+// THE MECHANISM THAT MADE IT UNFAILABLE, named at the symbols, AND THE REPAIR THAT CLOSED IT.
+// `v1_compiler.coproduct_reflection` `marshal_skeleton` returned `conj_record` at both of its
+// return sites, and `conj_record` builds every node as `TypeNode { connective: Conj }`.
+// `v2.std.node_query` `node_is_call` matches `ComputationNode { behavior: Transform }` and answers
+// false on everything else. A Conj TypeNode cannot satisfy that match, so `node_callee_symbol` was
+// Absent at every node of every fn-arrow body skeleton, `local_determinism_axis` returned
+// Deterministic unconditionally, and `determinism_transitive_holds` over a
+// `fn_arrow_decl_facts_live` population was GREEN BY CONSTRUCTION -- DESIGN §4b's own question
+// asked too late, a row carrying no information while looking exactly like coverage.
 //
-// THIS IS NOT A §4b(3) DECLARED DROP, and calling it one would be its own dishonesty. Nothing
-// regressed. Both symbols above predate gunbc#10245 unchanged, so the wall was never lit through
-// this path -- and a capability that was never real is not a capability that was dropped. The
-// honest instruments are §4b(1) and §4b(2): the class's rung is the MINIMUM across its in-scope
-// paths, and through the live path it is none, so the fixture rows' rung does not stand in for it;
-// and the stall is tracked by naming the NEXT-RUNG TRIGGER AS A CAPABILITY -- the fn-arrow body
-// skeleton represents a call at a shape `node_is_call` accepts. Re-shaping `conj_record` is a
-// corpus-wide cut, since every lens reading these skeletons consumes that shape, and it is tracked
-// as its own item rather than carried here.
+// THE §4b(2) STALL FILED HERE NAMED THE CAPABILITY AND THE CAPABILITY LANDED, SO THE STALL IS
+// RETIRED BY ITS TRIGGER RATHER THAN BY THIS PARAGRAPH BEING REWRITTEN. The trigger read: the
+// fn-arrow body skeleton represents a call at a shape `node_is_call` accepts. gunbc#10282 reshaped
+// the PRODUCER -- `marshal_generic` emits `ComputationNode { behavior: Transform }` for an
+// `ExprCall` with a non-empty authored name, whose first positional child is already the callee
+// identity leaf -- rather than widening this lens to accept the Conj spelling, which would have
+// left the substrate with two definitions of a call. It was NOT the corpus-wide cut this paragraph
+// anticipated: every other skeleton consumer reads atoms or folds kind-agnostically, and the single
+// consumer that matched on the kind was a private fork of `node_is_call` in
+// `v2.lens.no_dual_representation_test.scan`, which the same change deleted in favour of the
+// authority.
 //
-// THE STALL IS RETIRED BY EXECUTION, NOT BY MEMORY. The two-arm discriminator in
-// v2.test.claim.enforcement.determinism_transitive_witness holds the gap open: one synthetic Node
-// shaped `ComputationNode { behavior: Transform }` and one shaped `TypeNode { connective: Conj }`,
-// same callee atom, asserting that this lens FIRES on the first and is BLIND to the second. Both
-// arms pass today, which is the executing record that the lens is correct and live while the
-// subject shape cannot express what it detects. When the capability lands, the blind arm reds and
-// names itself for removal.
+// WHAT THAT DOES AND DOES NOT DISCHARGE, kept apart because the difference is the whole of clause 2.
+// It discharges the SHAPE half: this lens's refusal is now authorable over the live substrate, so
+// the live consumer's green is a statement about its closure rather than about the representation.
+// It does NOT establish that a live RED is constructible end-to-end today, and no such claim is
+// made here. `v2.std.fn_index` `atom_identities_in_node` reads callees at DEPTH ONE from
+// `decl.output`, so a call inside a block body sits below the horizon `call_reachable_decls` seeds
+// from; whether that narrows the live path is undecided by execution and is tracked at work item
+// adhoc-6af6a225-11d. Clause 2 therefore stands on the reachability question, not on the shape one.
 //
 // WHAT gunbc#10245 DID BUY, stated without letting it stand in for the clause. The acquisition had
 // no caller-named subject, so no live-tree consumer of this producer could reach the floor's