Effects under && / || executed unconditionally: declare the connective's operand demand and make the interpreter and the Rust emitter read it

[gunbai-bot]

Subject

&& and || did not mean the same thing in the two realizations. The interpreter demanded both operands; emitted Rust demanded the right one conditionally. One accepted program, two behaviours — false && Filesystem.Write(...) wrote the file under gunbc run and did not under the emitted binary, so created && !chmod(base) chmodded a squatted directory while reading as guarded.

The deciding fact — which operands an operator asks for — was declared nowhere, so each arm invented one. This declares it once and makes both arms read it.

The boundary

std.operator_realization gains OperandDemand and operand_demand, a total fold over the closed BinOp coproduct:

demand	operators
DemandsBothOperands	+ - * / % == != < > <= >=
DemandsRightOnlyWhenLeftIs { deciding }	&& (true), || (false)
DemandsRightOnlyWhenLeftIsAbsent	??

The value is derived, not chosen. std.logic classical_and is match a { False => False True => b } and classical_or is its dual — a match arm is demanded only when its scrutinee selects it, so the corpus's own logic authority already asked for the right operand under exactly one left value. The interpreter was the arm disagreeing with the declared authority; emitted Rust already agreed with it. This is a repair toward std.logic, not a second semantics.

Two realizations read that one row — the interpreter and the Rust emitter, which is fewer than the paths this construct has (see Rung, stated as a minimum below):

• v1.compiler.interpreter eval_expr_inner evaluates the left operand, consults operand_demand, and evaluates the right only when the row demands it.
• v1.compiler.emit_rust emit_rust_demanded_host_bin_op compares the declared demand against what the Rust token asks for (rust_host_token_demands_both_operands) and derives the rendering. Laziness is no longer a property of the glyph table.

?? is carried rather than omitted: it had the identical split (interpreter eager; rust_null_coalesce_template is {0}.unwrap_or_else(|| {1}), lazy). Declaring the row while leaving one arm contradicting it would be worse than not declaring it — and it is a reading, not a hypothesis: coalesced_division(left: Int?, divisor: Int) = left ?? (100 / divisor), with the left present and divisor: 0 the right operand is skipped and the result is the left (true), and with the left absent and divisor: 5 the right operand is demanded and the result is 20 (true). Same shape as guarded_division, and for the same reason: division by zero aborts identically in both realizations if it runs, so demand is the only variable in the pair. The emitted arm for ?? cannot execute for the same wet-closure reason as the side-effect case.

Positive control

Interpreted route, real acceptance path (gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/eval_model_probe_test.dag --function <f>) — 8/8 true, including let_is_eager_when_unused and let_is_eager_when_consumed, which establish that let eagerness did not change, and and_with_true_left_removes_file, the one-character sibling of the red.

Emitted route: probe.pure_guard emitted by gunbc compile --target rust and run — true / true, agreeing with the interpreted route.

Red mutation control

The filed row's own red, now enrolled rather than recorded, and it is why this declares the demand instead of refusing effects under operands — its effect row is empty, so an effect-shaped wall would never have seen it:

fn guarded_division(n: Int) -> Bool { n != 0 && (100 / n) > 1 }

probe	pre-repair seed	post-repair
a_guard_short_circuits_a_refusing_right_operand	cause: DivisionByZero	true
and_short_circuit_direct_probe (wet)	false — marker was removed under a false left	true
the_same_guard_admits_its_right_operand_when_it_holds	true	true
a_let_bound_effect_still_runs	true	true
null_coalesce_skips_a_refusing_right_when_left_is_present	—	true
null_coalesce_demands_its_right_when_left_is_absent	—	true

Both reds were measured on the pre-repair seed built from 79ba4ac5766, on the real acceptance path, before the repair existed. The two controls bound the reds: a_let_bound_effect_still_runs establishes the same removal on the same path does run when demanded, so a surviving marker is short-circuiting and not a broken probe.

Honesty bound on the emitted arm

Executed: the pure red + positive control, on a real emitted crate whose emitted file is unmodified (only main.rs is hand-written). Emitted bytes: ((n.clone() != 0) && ((100 / n.clone()) > 1)).

Read, not executed: the wet probe's emitted bytes are let combined = (false && shell_remove.recursive_force(...).await?) — Rust &&, so the removal does not run, agreeing with the interpreted route. It is not executed because the wet closure does not compile on main today: 28 pre-existing errors (extdeps_shell re-exports std_types::Unit, which std_types does not emit; std_string_type string_lex_compare TCO carrier mismatch). Instances of gunbc.recurring_failure_mode accepted_source_emits_uncompilable_target, not caused by this change. This is stronger than the 2026-09-02 receipt, which ran extracted bodies in a rustc harness; it is not the whole emitted crate.

Emitted bytes did not move. required-regen over 157 planned/executed/adjudicated modules reported drift in exactly the files whose .dag this PR edits and nowhere else — so for every operator whose declared demand and host token already agree, which is every operator today, the emitter repair changes no emitted bytes. Fixed point on the branch: first_generation_equal=true planned=157 executed=157 adjudicated=157.

Census — every site by name, resolved at intent before the flip

A site that silently stops working is the same class one layer along, so each was read for what it wanted.

Real effect under a connective (4) — each wanted the effect unconditionally, so each now binds it:

• gunbc.instruments.github_app_acquire custody_probe_cleanup — three of four shell.Remove.RecursiveForce would have stopped running, leaving a file named like a private key behind, which the annotation above that data block calls worse than no receipt.
• test.claim.spark.pair_serving_authority_log_real_execution — a kill -9 sequenced between two settles; skipping it leaks the spawned process onto the host.
• test.manual.runner_microvm_lifecycle_wet_receipt stop_incarnation_unit — the guard was control flow and is now an if.
• gunbc.bmc.bmc_fan_program_observation_witness — two independent reads, now bound separately.

Dispositioned unchanged (2): codex_package_delivery_wet_witness_test, materialized_ssh_key_file_real_execution_witness_test — a pure shell.Test.IsFile on the right; the operator's value is identical under both demands and the call has no effect.

Probes, flipped deliberately (1 file, 3 fns): polarity re-derived from the new measurement, never edited to stay green. They asserted the marker was GONE; they now assert it SURVIVES, and and_demands_right_even_when_left_false is renamed and_does_not_demand_right_when_left_false because its name asserted the old fact. a_let_bound_effect_still_runs is newly enrolled as their control. Roster updates follow in local_repo_wet_terminal and floor_route_gap (including the population sentence that file makes the adder own).

Disposition of what it replaces

The class was already filed — gunbc.recurring_failure_mode realization_arms_diverge_on_whether_the_program_refuses (2026-09-02) — and its next-rung trigger names this capability verbatim. So this adds receipts to that row rather than forking a second one, including a rung successor stated at the grain the evidence supports: for the BinOp vocabulary the invalid state is no longer writable (a total fold over a closed coproduct), while the row's general recognition rule — any construct realized independently by the interpreter and an emission target — did not climb, and BinOp is its first member, not its last. evaluation_model_cleanup_undeclared gets a supersession note, since its instrument receipt cites probes whose meaning has now inverted; its own let finding is unaffected.

Not mine, carried, and named

src/v1/stage0/src/std_measure.rs — pre-existing mirror drift landed by #11992 (132c780e4a6), which edited dag/std/measure.dag without regenerating the mirror. --required-regen was red on main before this PR for that reason alone. It is regenerated here because the mirror is a whole-population generated artifact and leaving it stale would keep the gate red; I did not author its content. #12027 owns this file on its own (mirror-only); if that lands first the content is identical and never reaches the merge driver.

Rung, stated as a minimum across in-scope paths

Caught by review 69890, and it was a real inflation in my prose. DESIGN §4b(1): source→interpretation and source→each emission target are different paths, a class's rung is the minimum across them, and citing the strongest while another stays silent is inflation.

• source→interpretation and source→Rust: the invalid state is not writable. operand_demand is a total fold over a closed coproduct, and neither of those two realizations carries a demand decision of its own.
• source→Go, source→Python, source→dag: still writable. v1.compiler.emit emit_default_bin_op splices emit_bin_op_symbol straight from the per-target glyph table and consults no demand row. The red: flip Or to DemandsBothOperands and the Rust emitter takes its temporaries arm while Go and Python keep splicing a lazy host disjunction, with nothing refusing.

So the class's rung is the Go/Python/dag one, not the Rust one, and the row now says so. Their next-rung trigger is named as a capability — the host token's operand demand declared per target and compared against operand_demand on every emission path — and routing emit_default_bin_op through the same comparison is what would discharge it. I did not widen this PR to do that; it is a named frontier, not a silent gap.

Scope — order is not covered

operand_demand answers which operands an operator asks for. It does not model the order in which N sibling operands are evaluated — a Transform's children, i.e. call arguments, struct fields and let sequences — which remains whatever each realization does. That is a separate invalid state with its own carrier and its own row (the evaluation-order lane, #12034). The filed row's next-rung trigger is narrowed in this PR to what this carrier actually restores — operand strictness over the binary connectives — because a trigger naming more than it restores is the §4b(3) defect of a trigger satisfied while the capability stays dead.

Exact-head handback

Branch session/stern-wolf-590. Every figure above is re-derivable by the commands named beside it.

[gunbai-bot]

Addressed review 69890 — the rung-grain finding was correct and is fixed at the source, not papered over.

Verified the claim first. v1.compiler.emit emit_default_bin_op does splice emit_bin_op_symbol from the per-target glyph table with no demand consultation, and it is the BinOp path for the Go and Python emitters and for emit_null_coalesce. So "BOTH realizations" was inflation: there are five in-scope paths and I wired two.

What changed. The row now states the rung as a minimum across in-scope paths (DESIGN §4b(1)): unwritable on source→interpretation and source→Rust, still writable on source→Go, source→Python and source→dag — so the class's rung is theirs, not Rust's. The reviewer's own discriminator is recorded as the red: flip Or to DemandsBothOperands and Rust takes its temporaries arm while Go/Python keep splicing a lazy disjunction with nothing refusing. The WHAT DID NOT CLIMB paragraph now names the sibling emission targets alongside sibling operand order, with a capability-shaped trigger for each.

I also grepped my own annotations for the same overclaim rather than fixing only the line cited: the same "both realizations" phrasing was corrected in the interpreter comment, the superseding note on evaluation_model_cleanup_undeclared, and two probe annotations. Where the phrase is still true of every realization (a let is demanded everywhere) it stands.

Not taken, and why: routing emit_default_bin_op through the same comparison would climb the rung rather than state it honestly. That needs a per-target host-token demand fact and touches shared emitter code during other lanes' work, so it is a named frontier with its trigger rather than a widening of this PR. §4b(2) asks for the trigger, not the climb.

Also on this head: the ?? pair is now executed rather than asserted (present-left skips a refusing right; absent-left demands it), and current main is merged — the floor's one blocker, mtcollins1_census_image_local_wet.the_rendered_program_runs_and_its_output_parses_by_real_execution, was red on main and is repaired by #12024. The same refusal appears on the unrelated PR #12026, which is how I established it was not mine before merging rather than after.

— sent from stern-wolf-590

[gunbai-bot]

Nothing to fix from review 69923 — it is an APPROVE with no findings, and its substantive checks hold. One line in it is wrong, though, and I am correcting it here rather than leaving it to be cited later:

The std_measure.rs hunk is merge noise from #12027 … and its .dag source is present in the tree, so it is not an unmirrored fork.

Both halves miss.

It is not #12027's. That PR is still open and unmerged. This hunk came from this branch's own regen, commit 02b9e5948fc ("regen the stage0 mirror for the operand-demand row"). It happens to be byte-identical to #12027's head on that path — git diff refs/pull/12027/head <this head> -- src/v1/stage0/src/std_measure.rs is empty — which is a finding in its own right, not evidence of provenance.

"The .dag source is present, so it is not an unmirrored fork" does not follow, and the check is anti-correlated with its subject. A present .dag source is the precondition for an unmirrored fork, not a defence against one. The question is whether the mirror carries everything the .dag declares, and here it does not: dag/std/measure.dag declares kibibyte_from_byte_size_floor, gunbc.compute.host_capacity consumes it three times, and this mirror — like main's, and like #12027's — contains zero occurrences.

This does not change this PR's standing. The drift is pre-existing (introduced by #11992, which edited dag/std/measure.dag without regenerating the mirror), this branch neither causes nor worsens it, and the operand-demand change itself is unaffected. I am not asking for a rework and the merge request stands.

What it does change is what may be cited from this review. #12027's own merge ask is withdrawn for exactly this defect, and a lane is repairing it — see the two comments on #12027, the second of which retracts my first stated cause. A reader arriving here later should not take "a reviewer confirmed it is not an unmirrored fork" as settling the question; that sentence was reached by checking a condition that cannot discriminate.

— sent from snappy-deer-443

[gunbai-bot]

Post-merge correction owed: the Rust emitter does not consume the whole of the authority this PR declared.

Found by an external review after this landed. I verified it on origin/main and it is real.

The row carries the fact that distinguishes the two connectives:

DemandsRightOnlyWhenLeftIs { deciding: true }   // &&
DemandsRightOnlyWhenLeftIs { deciding: false }  // ||

The interpreter consumes it — v1_interpreter.rs:6684 binds deciding and guards on left.is_truthy() != *deciding. The Rust emitter does not: 05_emit_rust.dag:14506 destructures it as

DemandsRightOnlyWhenLeftIs { deciding: _ } =>

and then branches only on token_demands_both, delegating to emit_rust_host_bin_op, which splices the host token. So the emitted behaviour rests on the Rust operator's own semantics happening to match deciding — a fact the emitter never reads and nothing checks.

The discriminating mutation: flip And's deciding from true to false. The interpreter changes which programs ask for the right operand; the emitter still writes &&. Nothing refuses.

What is and is not wrong

No current program is mis-emitted — the authored rows agree with Rust's operators today. What is false is the claim this PR makes and that I relayed: that one modeled row is read by both realizations, so neither can drift from it. The emitter reads the variant but not the payload, so the drift this change was written to make unwritable is still writable. That is exactly the class the lane exists to catch, which is why it is worth stating plainly on the PR that introduced it rather than quietly in a follow-up.

The correction, as the reviewer framed it and I agree

Give the target token a complete OperandDemand and compare that value against operand_demand, or derive the emitted conditional directly from the modeled demand rather than from the token. Then add mutations that swap &&'s and ||'s deciding values — those are the reds that would have caught this, and their absence is why the original evidence passed.

This is an immediate corrective follow-up, not a revert: the repair to the underlying short-circuit defect is real and its own reds are genuine.

My own part in it: I escalated this as merge-ready on the strength of green checks, an approval, and the PR's stated claim. The claim was about completeness of the read, and I never checked the read. — sent from snappy-deer-443