From abd5cf1cd0749e0198b13e4b38083d47641bc2f5 Mon Sep 17 00:00:00 2001
From: "g. nicholas d'andrea" <gnidan@users.noreply.github.com>
Date: Thu, 23 Jul 2026 22:12:16 -0400
Subject: [PATCH] format: fix the program example's pre-execution stack
 pointers

The Incrementer example annotated its stack-resident local against
post-execution machine state, contradicting the pointer convention the
instruction schema declares: a context's pointers describe the state a
debugger observes when stopped at the instruction, before it executes.

Reworked the example to that convention. localValue (produced by the
SLOAD at offset 1) is first observable at offset 2, where the
pre-execution stack holds it at the top (slot 0); at offset 4 it sits
one below the PUSH1 result (slot 1) and is then consumed by ADD, so it
is no longer in scope at offsets 5-6. Previously it was shown live on
the stack after ADD, which would have made a debugger display it off by
one. Also drops a stale 'value = tmp;' line left over from an earlier
naming of the pseudo-code.
---
 schemas/program.schema.yaml | 40 +++++++++++++++++++++----------------
 1 file changed, 23 insertions(+), 17 deletions(-)

diff --git a/schemas/program.schema.yaml b/schemas/program.schema.yaml
index 1426dd577d..3ba4e6774e 100644
--- a/schemas/program.schema.yaml
+++ b/schemas/program.schema.yaml
@@ -71,7 +71,6 @@ examples:
     # code {
     #   let localValue = storedValue;
     #   storedValue += 1;
-    #   value = tmp;
     # };
     # ```
     contract:
@@ -90,16 +89,32 @@ examples:
           pointer:
             location: storage
             slot: 0
+    # Each instruction's pointers describe the machine state the
+    # debugger observes when stopped at that instruction, i.e.
+    # before it executes; stack `slot` counts from the top of
+    # that pre-execution stack.
     instructions:
       - offset: 0
+        # about to PUSH0; stack: (empty)
         operation:
           mnemonic: PUSH0
         context:
           variables:
             - *stored-value
       - offset: 1
+        # about to SLOAD the slot pushed by PUSH0; stack: [0x00].
+        # localValue is not observable until SLOAD produces it, so
+        # it first appears at offset 2.
         operation:
           mnemonic: SLOAD
+        context:
+          variables:
+            - *stored-value
+      - offset: 2
+        # about to PUSH1; stack: [localValue] (top is slot 0)
+        operation:
+          mnemonic: PUSH1
+          arguments: ["0x01"]
         context:
           variables:
             - *stored-value
@@ -111,10 +126,11 @@ examples:
               pointer:
                 location: stack
                 slot: 0
-      - offset: 2
+      - offset: 4
+        # about to ADD; stack: [localValue, 0x01], so localValue is
+        # one below the top (slot 1). ADD then consumes it.
         operation:
-          mnemonic: PUSH1
-          arguments: ["0x01"]
+          mnemonic: ADD
         context:
           variables:
             - *stored-value
@@ -122,26 +138,16 @@ examples:
               pointer:
                 location: stack
                 slot: 1
-
-      - offset: 4
-        operation:
-          mnemonic: ADD
-        context:
-          variables:
-            - *stored-value
-            - *local-value
       - offset: 5
+        # about to PUSH0; stack: [storedValue + 1]. localValue was
+        # consumed by ADD and is no longer in scope.
         operation:
           mnemonic: PUSH0
         context:
           variables:
             - *stored-value
-            - <<: *local-value
-              pointer:
-                location: stack
-                slot: 1
-
       - offset: 6
+        # about to SSTORE; stack: [storedValue + 1, 0x00]
         operation:
           mnemonic: SSTORE
         context: