probe: pin overflow law for SUM-over-add scheduler rewrite

[AdaWorldAPI]

Smallest scheduler falsifier after #1258/#1259. This does not add a scheduler or a rewrite. It pins one legality law against the shipped mask-risc executor: SUM(wrapping_i32(a+b)) is not generally equal to SUM(a)+SUM(b) because the row expression wraps in i32 while MaskedSumI32 widens each selected value to i64. One overflow-row negative case and one no-overflow positive control. The result decides the planner contract: distribute only with a per-selected-row no-overflow proof, or under a separately defined widened-add semantic. New standalone test file only, so it does not stack edits onto #1259's row_bridge.rs.

Ruling from the falsifier

The default implementation path is not to license SUM(a+b) -> SUM(a)+SUM(b) with a range proof. That rewrite remains a conditional optimization only.

The semantics-preserving materialisation-free lowering is to fuse the row operation into the reduction itself:

SUM(mask, wrapping_i32(a+b))
  -> masked_sum_wrapping_add_i32(mask, a, b)

That preserves row-level wrapping even on overflow while still erasing the derived lane. The ndarray primitive is now isolated in AdaWorldAPI/ndarray#319; lance-graph should consume it only after that PR lands, because this repository's CI intentionally checks ndarray master.

[coderabbitai]

Warning

Review limit reached

Next included review available in 38 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used all 2 included reviews currently available. Your 53 included PR review attempts over the past 7 days set your current allowance at 2 reviews per hour.

Your organization has reached its usage spending cap. Adjust your spending cap in the billing tab.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Essentials

Run ID: 9edb0e9a-189f-44c1-bad1-180ecf350b70

📥 Commits

Reviewing files that changed from the base of the PR and between 6a3c7d4 and 5bab3b0.

📒 Files selected for processing (1)

• crates/r2il-mask-abi-probe/tests/scheduler_sum_rewrite.rs

---

_{Comment @coderabbitai help to get the list of available commands.}

[cursor]

Bugbot couldn't run - usage limit reached

Bugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit.

A user or team admin can review and increase usage limits in the Cursor dashboard.

(requestId: serverGenReqId_a1d51a2d-c313-4563-bb77-47c4d45fdd41)

[AdaWorldAPI]

@coderabbitai review

This is deliberately a one-law probe, not a scheduler implementation. Please attack two claims rather than reviewing for style:

1. Does sum_all really execute the shipped Terminal::MaskedSumI32 semantics over every row, with no scratch/mask accident that could make the comparison vacuous? In particular the program has zero ops / zero scratch slots and reads an all-selected resident Operand::Plane(0).
2. Is the counterexample sufficient to prove that SUM(wrapping_i32(a+b)) -> SUM(a)+SUM(b) is not generally semantics-preserving? The intended distinction is row-level wrapping i32 arithmetic versus per-value widening to i64 in MaskedSumI32; both final totals fit i64, so this should not be a terminal carry-bound issue.

The positive control is meant to keep the ruling narrow: when each selected row's add is exact in i32, the distribution should agree.

[coderabbitai]

Tip

For best results, initiate chat on the files or code changes.

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
set -euo pipefail

echo '=== PR diff summary ==='
git diff --stat HEAD^ HEAD
echo '=== Changed files ==='
git diff --name-only HEAD^ HEAD
echo '=== PR patch ==='
git diff --unified=80 HEAD^ HEAD

echo '=== Candidate executor and test files ==='
fd -t f -e rs . | rg '(row_bridge|mask|exec|executor|terminal|sum|scheduler)'
echo '=== MaskedSumI32 references ==='
rg -n -C 8 '\bMaskedSumI32\b' --glob '*.rs' .
echo '=== sum_all references ==='
rg -n -C 8 '\bsum_all\b' --glob '*.rs' .

Length of output: 56446

---

🏁 Script executed:

#!/bin/bash
set -euo pipefail

echo '=== exec.rs structure ==='
ast-grep outline crates/lance-graph-mask-risc/src/exec.rs --items all --type function --match 'execute|masked_sum_i32|read|lane_i32|validate' --view expanded
echo '=== ir.rs structure ==='
ast-grep outline crates/lance-graph-mask-risc/src/ir.rs --items all --type function,struct,impl --match 'Program|new' --view expanded
echo '=== scratch definitions ==='
rg -n -C 12 'fn for_program|struct Scratch|impl.*Scratch|fn all\b' crates/lance-graph-mask-risc/src
echo '=== execution and operand helpers ==='
sed -n '760,1030p' crates/lance-graph-mask-risc/src/exec.rs
echo '=== Program construction and scratch-slot computation ==='
sed -n '350,490p' crates/lance-graph-mask-risc/src/ir.rs
echo '=== validation relevant to planes, terminals, and tail bits ==='
rg -n -C 10 'fn validate|PlaneTail|check_operand|MaskedSumI32|scratch_slots' crates/lance-graph-mask-risc/src/exec.rs crates/lance-graph-mask-risc/src/reference.rs

Length of output: 1761

---

🏁 Script executed:

#!/bin/bash
set -u

echo '=== exec.rs selected functions ==='
ast-grep outline crates/lance-graph-mask-risc/src/exec.rs --items all --type function --match 'execute|masked_sum_i32|read|lane_i32' --view expanded || true
echo '=== execution and operand helpers ==='
sed -n '430,740p' crates/lance-graph-mask-risc/src/exec.rs
sed -n '860,1025p' crates/lance-graph-mask-risc/src/exec.rs
echo '=== Program construction and Scratch references ==='
rg -n -C 14 'pub struct Program|impl Program|pub fn new|scratch_slots|pub struct Scratch|impl.*Scratch|fn for_program|fn all\b' crates/lance-graph-mask-risc/src
echo '=== Program implementation range ==='
sed -n '350,490p' crates/lance-graph-mask-risc/src/ir.rs
echo '=== Scratch implementation range ==='
rg -n -C 20 'for_program' crates/lance-graph-mask-risc/src
echo '=== validation, terminal, and tail checks ==='
rg -n -C 12 'fn check_operand|fn validate|PlaneTail|tail|MaskedSumI32|SumRowBound' crates/lance-graph-mask-risc/src/reference.rs crates/lance-graph-mask-risc/src/exec.rs
exit 0

Length of output: 217273

---

@AdaWorldAPI No findings.

1. sum_all executes the intended terminal path.

   • Program::new(vec![], Terminal::MaskedSumI32 { mask: Operand::Plane(0), lane: 0 }) has zero operations.
   • It has zero scratch slots because it names no Operand::Scratch.
   • Operand::Plane(0) reads directly from Planes::masks[0].
   • The executor dispatches Terminal::MaskedSumI32 to masked_sum_i32 for each tile and returns Value::SumI64.
   • Validation requires the mask and lane lengths to match n_rows. It also rejects dirty tail bits.
   • sum_all creates all-one mask words and clears the final-word tail. Therefore, it selects every lane row.
   • The positive control makes this selection observable. Its nonzero rows and assert_eq!(literal, 74) prevent an empty or partial mask from passing unnoticed.

2. The overflow case is sufficient.

   • The literal row expression computes i32::MAX.wrapping_add(1) == i32::MIN.
   • MaskedSumI32 then widens that selected value to i64, so the literal total is -2^31.
   • The distributed form independently widens i32::MAX and 1, then adds the terminal results. Its total is 2^31.
   • Both totals fit in i64. The difference is caused by row-level i32 wrapping, not terminal carry behavior.
   • The positive control limits the ruling correctly. When every selected checked_add succeeds, the row expression equals the mathematical i64 sum and the two forms agree.

The test establishes the intended planner contract: distribution requires a no-overflow proof for each selected row, unless the planner uses a separately specified widened-add operation.

You are interacting with an AI system.

[cursor]

Bugbot couldn't run - usage limit reached

Bugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit.

A user or team admin can review and increase usage limits in the Cursor dashboard.

(requestId: serverGenReqId_664ffd43-f621-4121-83b6-b22cf5a3053c)

[cursor]

Bugbot couldn't run - usage limit reached

Bugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit.

A user or team admin can review and increase usage limits in the Cursor dashboard.

(requestId: serverGenReqId_397ed878-0730-428b-b810-f590c83d6e9d)