[ascandone]

Stacked on #225.

Problem

A pull debits its source at once; the posting only exists once a send drains the queue. Two shapes pass vm.Verify and go wrong at run time:

• Funds still queued when set_current_asset runs are posted under the new asset.
• Funds still queued when the run ends are a debit that never becomes a posting.

Whether a capped send empties the queue depends on the balances, so on today's bytecode this is not decidable. For example, pull(cap: 100) then send(cap: 50) is fine with a balance of 40 and leaves 30 queued with a balance of 80. The compiler empties the queue with a chain of capped sends whose caps add up to the amount pulled, which the verifier cannot prove.

Fix

Make draining the queue something the bytecode shows, then check it.

• Compiler. Every send statement ends with an uncapped send: the last clause of an allotment, the trailing remaining of an inorder, each oneof branch, and a lone account or kept. The inorder branch that skips a zero remaining drains with an uncapped kept (send_to_account()), which only clears zero-amount entries and emits no posting. Postings are unchanged: zero-amount postings are already dropped, so an uncapped tail sends what the capped one did.
• Verifier. checkQueueDrained keeps one bool per instruction, "may hold pulled funds". A pull sets it, an uncapped send clears it, and capped sends and rewinds leave it alone. The program is rejected if the bool can be true at set_current_asset or at the end of the run. Jumps only go forward, so this is one pass over the instructions, and it never looks at amounts.

The rule is conservative. It rejects some programs that would be fine: capped chains that add up, send(cap: $pulled), and regions that are always rewound. The rejected and accepted shapes are listed in TestIRVerifierRequiresAnUncappedSendAfterEveryPull and in bytecode-verifier.md.

Exec does not check the queue. The two TODO crashes comments in vm.go are removed, since Verify already rejects a truncated two-word instruction.

Open: bytecode version

Bytecode from the previous compiler ends allotments with capped sends, so it fails the new rule. Bumping CurrentBytecodeVersion to 0.2 would make old blobs fail at decode instead, since a 0.x reader accepts only its exact version. This PR does not bump it.

Tests

• New verifier tests: 7 rejected and 5 accepted shapes, written as IR.
• Hand-written IR tests now end with an uncapped send. One compiler snapshot (TestDestInorder) changes.
• go test ./..., the difftest module (which verifies every generated program) and TestCompiledCorpusPassesVerify pass.

Performance

BenchmarkCompiledVM*, minimum of 5 runs: allotment benchmarks use 3 fewer allocs (42 → 39, 58 → 55) and are about 1.5% faster. The others are within noise.

[NumaryBot]

The required automated review completed with no remaining findings.

The base branch was changed.

[NumaryBot]

The required automated review completed with no remaining findings.