pr4.2

crates/console/prometeu-vm/src/verifier.rs

@@ -14,6 +14,7 @@ pub enum VerifierError {
     InvalidJumpTarget { pc: usize, target: usize },
     JumpToMidInstruction { pc: usize, target: usize },
     StackUnderflow { pc: usize, opcode: OpCode },
+    StackOverflow { pc: usize, height: u16, limit: u16 },
     StackMismatchJoin { pc: usize, target: usize, height_in: u16, height_target: u16 },
     BadRetStackHeight { pc: usize, height: u16, expected: u16 },
     FunctionOutOfBounds { func_idx: usize, start: usize, end: usize, code_len: usize },
@@ -143,6 +144,15 @@ impl Verifier {
             let out_height = in_height - pops + pushes;
             max_stack = max_stack.max(out_height);
 
+            // Enforce declared max stack if provided (0 means "no explicit limit")
+            if func.max_stack_slots != 0 && out_height > func.max_stack_slots {
+                return Err(VerifierError::StackOverflow {
+                    pc: func_start + pc,
+                    height: out_height,
+                    limit: func.max_stack_slots,
+                });
+            }
+
             if instr.opcode == OpCode::Ret {
                 if in_height != func.return_slots {
                     return Err(VerifierError::BadRetStackHeight {
@@ -434,6 +444,34 @@ mod tests {
         assert_eq!(res[0], 2);
     }
 
+    #[test]
+    fn test_verifier_stack_overflow_limit() {
+        // Same program as max_stack, but declare max_stack_slots = 1 → should overflow at second push
+        let mut code = Vec::new();
+        code.push(OpCode::PushI32 as u8);
+        code.push(0x00);
+        code.extend_from_slice(&1u32.to_le_bytes());
+        code.push(OpCode::PushI32 as u8);
+        code.push(0x00);
+        code.extend_from_slice(&2u32.to_le_bytes());
+        code.push(OpCode::Add as u8);
+        code.push(0x00);
+        code.push(OpCode::Ret as u8);
+        code.push(0x00);
+
+        let functions = vec![FunctionMeta {
+            code_offset: 0,
+            code_len: 16,
+            return_slots: 1,
+            max_stack_slots: 1,
+            ..Default::default()
+        }];
+
+        let res = Verifier::verify(&code, &functions);
+        // Overflow occurs at pc = 6 (start of second PushI32)
+        assert_eq!(res, Err(VerifierError::StackOverflow { pc: 6, height: 2, limit: 1 }));
+    }
+
     #[test]
     fn test_verifier_invalid_syscall_id() {
         let mut code = Vec::new();

files/TODOs.md

@@ -1,55 +1,3 @@
-# PR-4.2 — Basic Stack Safety Verification (Underflow/Overflow)
-
-### Briefing
-
-The verifier must ensure the stack never underflows or exceeds defined limits during execution.
-
-### Target
-
-* Implement stack safety checks across the control-flow graph.
-
-### Work items
-
-* Simulate stack depth across instructions.
-* Detect:
-
-  * Stack underflow.
-  * Stack overflow beyond declared limits.
-* Emit appropriate verifier errors.
-
-### Acceptance checklist
-
-* [ ] Underflow cases are rejected.
-* [ ] Overflow cases are rejected.
-* [ ] Valid programs pass.
-* [ ] `cargo test` passes.
-
-### Tests
-
-* Add tests:
-
-  * Program with underflow → verifier error.
-  * Program exceeding stack limit → verifier error.
-  * Valid program → passes.
-
-### Junie instructions
-
-**You MAY:**
-
-* Add stack depth simulation.
-* Introduce verifier error types.
-
-**You MUST NOT:**
-
-* Change runtime stack implementation.
-* Introduce dynamic stack resizing.
-
-**If unclear:**
-
-* Ask before choosing stack limit rules.
-
----
-
 # PR-4.3 — Control Flow and Jump Target Verification
 
 ### Briefing