pr7.8

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

@@ -32,6 +32,10 @@ pub enum VerifierError {
     UnknownClosureCallee { pc: usize },
     /// User-provided arg_count for CALL_CLOSURE does not match callee signature
     BadClosureArgCount { pc: usize, expected: u16, got: u16 },
+    /// YIELD executed in an invalid context (minimal safety rule violation)
+    InvalidYieldContext { pc: usize, height: u16 },
+    /// SPAWN arg_count does not match callee param_slots
+    BadSpawnArgCount { pc: usize, expected: u16, got: u16 },
 }
 
 pub struct Verifier;
@@ -168,6 +172,23 @@ impl Verifier {
                     // Temporarily set pushes=0; we'll compute real pushes after type checks.
                     (arg_count + 1, 0)
                 }
+                OpCode::Spawn => {
+                    // imm: fn_id (u32), arg_count (u32)
+                    let (fn_id, arg_count_u32) = instr.imm_u32x2().unwrap();
+                    let callee = all_functions.get(fn_id as usize).ok_or_else(|| {
+                        VerifierError::InvalidFuncId { pc: func_start + pc, id: fn_id }
+                    })?;
+                    let arg_count = arg_count_u32 as u16;
+                    // Enforce exact arity match for safety and determinism
+                    if callee.param_slots != arg_count {
+                        return Err(VerifierError::BadSpawnArgCount {
+                            pc: func_start + pc,
+                            expected: callee.param_slots,
+                            got: arg_count,
+                        });
+                    }
+                    (arg_count, 0)
+                }
                 OpCode::Ret => (func.return_slots, 0),
                 OpCode::Syscall => {
                     let id = instr.imm_u32().unwrap();
@@ -186,6 +207,13 @@ impl Verifier {
                 });
             }
 
+            // Coroutine safety: forbid YIELD when operand stack is not empty (minimal rule)
+            if let OpCode::Yield = instr.opcode {
+                if in_height != 0 {
+                    return Err(VerifierError::InvalidYieldContext { pc: func_start + pc, height: in_height });
+                }
+            }
+
             // Compute out types vector with closure-aware rules
             use SlotTy::*;
             let mut out_types = in_types.clone();

crates/console/prometeu-vm/tests/verifier_coroutines.rs

@@ -0,0 +1,55 @@
+use prometeu_bytecode::FunctionMeta;
+use prometeu_bytecode::isa::core::CoreOpCode as OpCode;
+use prometeu_vm::verifier::{Verifier, VerifierError};
+
+fn enc_op(op: OpCode) -> [u8; 2] { [(op as u8), 0x00] }
+
+#[test]
+fn err_invalid_yield_with_non_empty_stack() {
+    // Program:
+    // 0..2: PUSH_I32 1 (imm 4 bytes)
+    // 6..8: YIELD
+    // 8..10: RET
+    let mut code = Vec::new();
+    code.extend_from_slice(&enc_op(OpCode::PushI32));
+    code.extend_from_slice(&1u32.to_le_bytes());
+    code.extend_from_slice(&enc_op(OpCode::Yield));
+    code.extend_from_slice(&enc_op(OpCode::Ret));
+
+    let functions = vec![FunctionMeta { code_offset: 0, code_len: code.len() as u32, return_slots: 1, ..Default::default() }];
+    let res = Verifier::verify(&code, &functions);
+    assert_eq!(res, Err(VerifierError::InvalidYieldContext { pc: 6, height: 1 }));
+}
+
+#[test]
+fn err_spawn_arg_mismatch() {
+    // Caller at func 0: SPAWN fn_id=1, arg_count=1; RET
+    // Callee at func 1: expects 2 param_slots
+    let mut code = Vec::new();
+    code.extend_from_slice(&enc_op(OpCode::Spawn));
+    code.extend_from_slice(&1u32.to_le_bytes()); // fn_id
+    code.extend_from_slice(&1u32.to_le_bytes()); // arg_count (mismatch: callee expects 2)
+    code.extend_from_slice(&enc_op(OpCode::Ret));
+
+    let caller = FunctionMeta { code_offset: 0, code_len: code.len() as u32, return_slots: 0, ..Default::default() };
+    // Callee has no code here; only signature matters
+    let callee = FunctionMeta { code_offset: code.len() as u32, code_len: 0, param_slots: 2, return_slots: 0, ..Default::default() };
+    let functions = vec![caller, callee];
+
+    let res = Verifier::verify(&code, &functions);
+    assert_eq!(res, Err(VerifierError::BadSpawnArgCount { pc: 0, expected: 2, got: 1 }));
+}
+
+#[test]
+fn err_sleep_truncated_immediate() {
+    // Encode SLEEP but provide only 1 of 4 immediate bytes
+    let mut code = Vec::new();
+    code.extend_from_slice(&enc_op(OpCode::Sleep));
+    code.push(0xAB);
+    let functions = vec![FunctionMeta { code_offset: 0, code_len: code.len() as u32, ..Default::default() }];
+    let res = Verifier::verify(&code, &functions);
+    assert_eq!(
+        res,
+        Err(VerifierError::TruncatedImmediate { pc: 0, opcode: OpCode::Sleep, need: 4, have: 1 })
+    );
+}

files/TODOs.md

@@ -1,32 +1,3 @@
-# PR-7.8 — Verifier Rules
-
-## Briefing
-
-Verifier must enforce coroutine safety.
-
-## Target
-
-Rules:
-
-* YIELD forbidden inside invalid contexts (define minimal safe rule).
-* SPAWN argument validation.
-* SLEEP argument type validation.
-
-## Checklist
-
-* [ ] Invalid YIELD rejected.
-* [ ] SPAWN arg mismatch rejected.
-
-## Tests
-
-* Invalid bytecode rejected.
-
-## Junie Rules
-
-You MUST NOT weaken verifier.
-
----
-
 # PR-7.9 — Determinism & Stress Tests
 
 ## Briefing