pr4.5

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

@@ -522,4 +522,104 @@ mod tests {
         let res = Verifier::verify(&code, &functions).unwrap();
         assert_eq!(res[0], 0);
     }
+
+    #[test]
+    fn test_verifier_ret_too_few_slots() {
+        // Function declares 1 return slot but returns nothing
+        // 0: Ret
+        let mut code = Vec::new();
+        code.push(OpCode::Ret as u8);
+        code.push(0x00);
+
+        let functions = vec![FunctionMeta {
+            code_offset: 0,
+            code_len: 2,
+            return_slots: 1,
+            ..Default::default()
+        }];
+
+        let res = Verifier::verify(&code, &functions);
+        // With too few return slots at RET, the verifier raises StackUnderflow on RET
+        assert_eq!(res, Err(VerifierError::StackUnderflow { pc: 0, opcode: OpCode::Ret }));
+    }
+
+    #[test]
+    fn test_verifier_call_return_mismatch_underflow_in_caller() {
+        // Two functions:
+        // F0 (idx 0): Call F1; PopN 1; Ret   (expects 0 total at return)
+        // F1 (idx 1): Ret                     (returns 0)
+        // Caller tries to pop 1 result that callee did not return → underflow at PopN
+
+        let mut code = Vec::new();
+
+        // F0 @ 0
+        // Call 1
+        code.push(OpCode::Call as u8);
+        code.push(0x00);
+        code.extend_from_slice(&1u32.to_le_bytes());
+        // PopN 1
+        code.push(OpCode::PopN as u8);
+        code.push(0x00);
+        code.extend_from_slice(&1u32.to_le_bytes());
+        // Ret
+        code.push(OpCode::Ret as u8);
+        code.push(0x00);
+
+        let f0_len = code.len() as u32; // 14
+
+        // F1 @ f0_len
+        code.push(OpCode::Ret as u8);
+        code.push(0x00);
+
+        let functions = vec![
+            FunctionMeta { code_offset: 0, code_len: f0_len, return_slots: 0, ..Default::default() },
+            FunctionMeta { code_offset: f0_len, code_len: 2, return_slots: 0, ..Default::default() },
+        ];
+
+        let res = Verifier::verify(&code, &functions);
+        // Underflow at PopN (pc = 6)
+        assert_eq!(res, Err(VerifierError::StackUnderflow { pc: 6, opcode: OpCode::PopN }));
+    }
+
+    #[test]
+    fn test_verifier_call_return_mismatch_bad_ret_in_caller() {
+        // Two functions:
+        // F0 (idx 0): Call F1; Ret        (declares return_slots = 1)
+        // F1 (idx 1): PushI32 1; PushI32 2; Ret  (returns 2)
+        // Caller ends with 2 values but declares 1 → BadRetStackHeight at caller's Ret
+
+        let mut code = Vec::new();
+
+        // F0 @ 0
+        // Call 1
+        code.push(OpCode::Call as u8);
+        code.push(0x00);
+        code.extend_from_slice(&1u32.to_le_bytes());
+        // Ret
+        code.push(OpCode::Ret as u8);
+        code.push(0x00);
+
+        let f0_len = code.len() as u32; // 8
+
+        // F1 @ f0_len
+        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::Ret as u8);
+        code.push(0x00);
+
+        let f1_len = (code.len() as u32) - f0_len;
+
+        let functions = vec![
+            FunctionMeta { code_offset: 0, code_len: f0_len, return_slots: 1, ..Default::default() },
+            FunctionMeta { code_offset: f0_len, code_len: f1_len, return_slots: 2, ..Default::default() },
+        ];
+
+        let res = Verifier::verify(&code, &functions);
+        // Error at caller's RET (pc = 6)
+        assert_eq!(res, Err(VerifierError::BadRetStackHeight { pc: 6, height: 2, expected: 1 }));
+    }
 }

files/TODOs.md

@@ -1,56 +1,3 @@
-# PR-4.5 — Multi-Return (`ret_slots`) Verification
-
-### Briefing
-
-The new ABI supports multi-return via `ret_slots`. The verifier must ensure the stack shape matches the declared return slot count.
-
-### Target
-
-* Validate return slot counts at call and return sites.
-
-### Work items
-
-* For each function:
-
-  * Read declared `ret_slots`.
-* At `RET`:
-
-  * Ensure stack contains exactly the required number of slots.
-* At call sites:
-
-  * Ensure caller expects correct number of return slots.
-
-### Acceptance checklist
-
-* [ ] Mismatched return slot counts are rejected.
-* [ ] Correct programs pass.
-* [ ] `cargo test` passes.
-
-### Tests
-
-* Add tests:
-
-  * Too few return slots → verifier error.
-  * Too many return slots → verifier error.
-  * Correct return slots → passes.
-
-### Junie instructions
-
-**You MAY:**
-
-* Use function metadata to validate returns.
-
-**You MUST NOT:**
-
-* Change calling convention semantics.
-* Modify function metadata layout.
-
-**If unclear:**
-
-* Ask before implementing slot rules.
-
----
-
 # PR-4.6 — Verifier Error Model Consolidation
 
 ### Briefing