Figure 5 — Non-Nestable LAMBDA with CALL-Mediated Nesting

Sequence diagram showing how CALL saves LAMBDA state to permit a nested LAMBDA in the called domain, with LAMBDA-active flag state annotated at every step

Step Instruction Caller Domain A Called Domain B LAMBDA-active Stack Notes 0 (initial state) Active — 0 (clear) empty No LAMBDA in progress 1 LAMBDA CR2, x X perm verified Executing — 1 (SET) PC+4 → LAMBDA_PC empty Save return PC to machine status No stack push 2 body executes Body A — 1 (SET) empty DRs hold args CR6,CR14 unchanged ! LAMBDA CR3, y FAULT! — 1 (SET) already active! — Non-nestable! Second LAMBDA while active = FAULT 3 CALL CR5 E perm verified domain crossing Suspended Active 0 (CLEARED) CALL clears flag Push frame Tag=0 +LAMBDA st CALL saves: CR5,CR6,CR14 PC, LAMBDA_PC LAMBDA-active=1 Then clears flag 4 LAMBDA CR3, y X perm verified permitted! — Body B 1 (SET) new LAMBDA_PC 1 frame Flag was cleared by CALL → nested LAMBDA permitted 5 body executes — Body B 1 (SET) 1 frame Nested LAMBDA body runs in B 6 RETURN fast path — Continues B 0 (CLEARED) PC ← LAMBDA_PC flag cleared 1 frame no pop! FAST PATH LAMBDA-active=1 → restore from machine status Zero stack access 7 B continues — Active B 0 (clear) 1 frame Domain B code after nested LAMBDA 8 RETURN stack path (tag=0) returns to A Resumed A Done 1 (RESTORED) from stack frame LAMBDA_PC restored flag re-set to 1 Pop frame Tag=0 STACK PATH Pop CALL frame Tag=0 → full Restore CR5,6,7 via mLoad Restore LAMBDA st 9 body A continues Body A — 1 (SET) empty Outer LAMBDA body resumes 10 RETURN fast path Caller — 0 (CLEARED) PC ← LAMBDA_PC flag cleared empty no pop! FAST PATH LAMBDA-active=1 → restore PC from machine status Zero stack access LAMBDA-ACTIVE FLAG TRACE Step: 0 1 2 ! 3 4 5 6 7 8 9 10 Flag: 0 1 1 1 0 1 1 0 0 1 1 0 Event: LAMBDA sets CALL clears nested LAMBDA fast RETURN CALL RETURN fast RETURN flag=1 (saves to stack) sets flag=1 clears flag restores flag=1 clears flag Key: LAMBDA is non-nestable (step !) but CALL mediates nesting by saving/clearing the flag (step 3) and restoring it on RETURN (step 8). Both LAMBDA RETURNs (steps 6 and 10) use the fast path: zero stack access, ~1 cycle. The CALL RETURN (step 8) uses the stack path: 5+ cycles.
LAMBDA (X permission, same domain)
CALL (E permission, domain crossing)
RETURN fast path (zero stack)
RETURN stack path (mLoad revalidation)
FAULT (non-nestable violation)