fix(v4.0.0): LEAVE follows FORTH-79

LEAVE sets the limit equal to the index: the rest of the body runs with
the index unchanged and the loop ends at the next LOOP or +LOOP.  v3's
left the loop at once, which is FORTH-83's.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

docs/v4.0.0/DECOMPOSITION.md

@@ -726,7 +726,7 @@ The storage service belongs to the Artemis role, now a device node.
 | `(?DO)` | IN | `over over xor if SKIP  drop (DO)  … body and loop end …  jump PAST   SKIP: drop drop drop   PAST:` — skips the loop when index = limit, as v3. Executed on the golden model (2026-10-03). |
 | `(LOOP)` | IN | See below. Adds 1 and goes round again while index < limit, signed, as v3. Executed on the golden model (2026-10-03) against C on every pair of 14 loop ends, and sequences recorded from the v3 binary. |
 | `(+LOOP)` | IN | See below. `( n -- )`: adds `n` and goes round again while index < limit for `n >= 0`, while index >= limit for `n < 0`, as v3. Executed on the golden model (2026-10-03) against C on every pair of 14 loop ends with 11 steps, and sequences recorded from the v3 binary. Clobbers `A`. |
-| `(LEAVE)` | IN | `pop drop pop drop  jump PAST` — discards the limit and index and leaves the loop at once. In a single loop this is what v3 does. v3 left the two on its return stack (index set to limit) and jumped past the loop, so a `LEAVE` in an inner loop made the outer `LOOP` count the inner loop's leftovers and stop: `: T 3 0 DO 10 0 DO I . I 1 = IF LEAVE THEN LOOP I . LOOP ;` prints `0 1 10` in v3 and `0 1 0 0 1 1 0 1 2` here. Executed on the golden model (2026-10-03) in `LOOP` and `+LOOP`, including sequences recorded from the v3 binary. |
+| `(LEAVE)` | IN | `pop pop drop dup push push` — FORTH-79 (ruled 2026-10-04): the limit is set equal to the index, so the loop ends at the next `LOOP` or `+LOOP`; the index is unchanged and the rest of the body still runs. v3's `LEAVE` left the loop at once (FORTH-83's behaviour) and, having set the index to the limit, left both on its return stack, so a `LEAVE` in an inner loop made the outer `LOOP` count the inner loop's leftovers and stop: `: T 3 0 DO 10 0 DO I . I 1 = IF LEAVE THEN LOOP I . LOOP ;` prints `0 1 10` in v3 and `0 1 0 0 1 1 0 1 2` here. Executed on the golden model (2026-10-04) in `LOOP` and `+LOOP`, up, down and with a step of 0. |
 | `I` | IN | `pop dup push` — executed on the golden model (2026-10-03). |
 | `J` | IN | `pop pop  pop dup push a!  push push  a` — the outer index waits in `A` while the inner pair goes back, so `J` needs no return entry beyond the two loops' own (with two in-line `SWAP`s it needed one more). Executed on the golden model (2026-10-03), including a sequence recorded from the v3 binary. Clobbers `A`. |
 | `UNLOOP` | IN | `pop drop pop drop` — executed on the golden model (2026-10-03) as `UNLOOP EXIT`, including a sequence recorded from the v3 binary. |