I-13's one rule for the stack: net = binds − k, total for every opcode, with no unstated scope — and it is checked in a single linear pass.
source I-13 (rev 2 teaching brief; H1.0-FINAL freeze, verified 10/10), David Lee Wise / ROOT0 / TriPod LLC. Room THE LAW. The runnable validator/VM below is the flagship; every number is exact (integer arithmetic). Rendered, not asserted.
Every opcode moves the stack by a fixed amount, and that amount is nothing but its two counts:
net = binds − k
k = operands it consumes off the stack; binds = 1 if it pushes a result, else 0. The law is total — it holds for all 14 fixed opcodes and for Call(n) — and there is no unstated scope: the number is the same wherever the opcode appears. computed
"Axiom XIII" names the rule in the brief; the framing is the author's, the arithmetic is checked here. framing
The instruction set. k in, binds out, net = binds − k:
| op | k | binds | net |
|---|
Call(n) binds 1 with k = n+1 (the n args and the callee slot), so net = −n. measured
Assert the whole table at once: binds − k must equal the expected net for every fixed opcode, and Call(n) = −n for n in {0,1,2,3}.
Control is depth-indexed — Block/If/Else/End ride a ctrl-stack of entry heights — so a target height is a number already in hand. There is no branch opcode, no address to resolve. The validator visits exactly len(code) slots: one linear pass, no backpatch, no fixpoint.
Stack height starts at 0. Each row consumes k, pushes binds, so height moves by net. A balanced region ends at height 0; a consumer with too few operands underflows. runnable
VALID means exactly two things were checked — and nothing more:
COVERED proved
• stack balance (ends at height 0, never underflows)
• control pairing (every Block/If closes; depth-indexed)
NOT COVERED out of scope
• types · termination · arithmetic result · dead/wasted values
• call arity: f(1,2,3) for def f(a) counts fine, then dies in the VM honest gap
☠ "control needs branch addresses" — cut. I-13 has no br opcode; control is depth-indexed over entry heights, so the target is always a number in hand. disproven
⚠ Op::effect is bypassed for Block/If/Else/End/Ret — their effect is re-derived by hand in the walker. The two encodings agree today; nothing enforces that they agree tomorrow. unenforced
I-13 keeps a MEASURED DEAD register. These stay on the page; a caveat laundered away is a lie. DEAD kept
Set Call(n)'s k to n — drop the +1 for the callee slot. Then net = −(n−1), not −n. A once-balanced call now mis-balances its region.