pr4.4

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

@@ -21,6 +21,10 @@ pub enum VerifierError {
     InvalidSyscallId { pc: usize, id: u32 },
     TrailingBytes { func_idx: usize, at_pc: usize },
     InvalidFuncId { pc: usize, id: u32 },
+    /// Execution can fall through past the end of the function without a valid terminator
+    /// (e.g., RET, JMP to end, HALT/TRAP). Verifier requires every reachable path to end
+    /// in a terminator.
+    UnterminatedPath { func_idx: usize, at_pc: usize },
 }
 
 pub struct Verifier;
@@ -250,6 +254,12 @@ impl Verifier {
                         stack_height_in.insert(next_pc, out_height);
                         worklist.push_back(next_pc);
                     }
+                } else if next_pc == func_len {
+                    // Reaching end of function by falling through (no terminator) is invalid.
+                    return Err(VerifierError::UnterminatedPath {
+                        func_idx,
+                        at_pc: func_start + pc,
+                    });
                 }
             }
         }
@@ -483,4 +493,33 @@ mod tests {
         let res = Verifier::verify(&code, &functions);
         assert_eq!(res, Err(VerifierError::InvalidSyscallId { pc: 0, id: 0xDEADBEEF }));
     }
+
+    #[test]
+    fn test_function_without_terminator_is_rejected() {
+        // Single NOP with no RET/JMP/TRAP/HALT at the end → fallthrough to end
+        let mut code = Vec::new();
+        code.push(OpCode::Nop as u8);
+        code.push(0x00);
+
+        let functions = vec![FunctionMeta { code_offset: 0, code_len: 2, ..Default::default() }];
+        let res = Verifier::verify(&code, &functions);
+        assert_eq!(res, Err(VerifierError::UnterminatedPath { func_idx: 0, at_pc: 0 }));
+    }
+
+    #[test]
+    fn test_function_with_proper_terminator_passes() {
+        // Minimal function that returns immediately
+        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: 0,
+            ..Default::default()
+        }];
+        let res = Verifier::verify(&code, &functions).unwrap();
+        assert_eq!(res[0], 0);
+    }
 }

files/TODOs.md

@@ -1,53 +1,3 @@
-# PR-4.4 — Function Boundary and Terminator Verification
-
-### Briefing
-
-Functions must follow canonical entry and exit rules. The verifier must enforce valid terminators and boundaries.
-
-### Target
-
-* Ensure functions start and end correctly.
-* Ensure terminator instructions are valid.
-
-### Work items
-
-* Verify function entry points are valid instruction boundaries.
-* Verify function exit instructions:
-
-  * Proper `RET` usage.
-  * Proper `FRAME_SYNC` placement (as per spec).
-* Reject functions without valid termination.
-
-### Acceptance checklist
-
-* [ ] All functions have valid entry and exit.
-* [ ] Invalid termination is rejected.
-* [ ] `cargo test` passes.
-
-### Tests
-
-* Add tests:
-
-  * Function without terminator → verifier error.
-  * Properly terminated function → passes.
-
-### Junie instructions
-
-**You MAY:**
-
-* Add boundary validation logic.
-
-**You MUST NOT:**
-
-* Redefine function semantics.
-* Change terminator opcode behavior.
-
-**If unclear:**
-
-* Ask before enforcing termination rules.
-
----
-
 # PR-4.5 — Multi-Return (`ret_slots`) Verification
 
 ### Briefing