pr6.5

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

@@ -25,6 +25,13 @@ pub enum VerifierError {
     /// (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 },
+    // --- Closure-specific errors ---
+    /// Top of stack is not a closure value on CALL_CLOSURE
+    NotAClosureOnCallClosure { pc: usize },
+    /// CALL_CLOSURE used with a closure whose callee function is not known at verify time
+    UnknownClosureCallee { pc: usize },
+    /// User-provided arg_count for CALL_CLOSURE does not match callee signature
+    BadClosureArgCount { pc: usize, expected: u16, got: u16 },
 }
 
 pub struct Verifier;
@@ -101,16 +108,37 @@ impl Verifier {
             return Err(VerifierError::TrailingBytes { func_idx, at_pc: func_start + pc });
         }
 
-        let mut stack_height_in: HashMap<usize, u16> = HashMap::new();
+        // Minimal stack type lattice to validate closure semantics
+        #[derive(Clone, Copy, Debug, PartialEq, Eq)]
+        enum SlotTy {
+            /// Type information not known statically (join of different paths or from loads/calls)
+            Unknown,
+            /// A value that is definitely not a closure (immediates, arithmetic results)
+            NonClosure,
+            /// A closure value whose target function id is known (from MAKE_CLOSURE)
+            Closure(u32),
+        }
+
+        fn join_slot(a: SlotTy, b: SlotTy) -> SlotTy {
+            use SlotTy::*;
+            match (a, b) {
+                (Closure(id1), Closure(id2)) if id1 == id2 => Closure(id1),
+                (NonClosure, NonClosure) => NonClosure,
+                _ => Unknown,
+            }
+        }
+
+        let mut stack_types_in: HashMap<usize, Vec<SlotTy>> = HashMap::new();
         let mut worklist = VecDeque::new();
         let mut max_stack: u16 = 0;
 
         // Start from function entry
-        stack_height_in.insert(0, 0);
+        stack_types_in.insert(0, Vec::new());
         worklist.push_back(0);
 
         while let Some(pc) = worklist.pop_front() {
-            let in_height = *stack_height_in.get(&pc).unwrap();
+            let in_types = stack_types_in.get(&pc).cloned().unwrap();
+            let in_height = in_types.len() as u16;
             let instr = decode_next(pc, func_code).unwrap(); // Guaranteed to succeed due to first pass
             let spec = instr.opcode.spec();
 
@@ -127,6 +155,19 @@ impl Verifier {
                     })?;
                     (callee.param_slots, callee.return_slots)
                 }
+                OpCode::MakeClosure => {
+                    // imm: fn_id (u32), capture_count (u32)
+                    let (_fn_id, capture_count_u32) = instr.imm_u32x2().unwrap();
+                    let capture_count = capture_count_u32 as u16;
+                    (capture_count, 1)
+                }
+                OpCode::CallClosure => {
+                    // imm: arg_count (u32). Pops closure_ref + arg_count, pushes callee returns.
+                    // We can't determine pushes here without looking at TOS type; will validate below.
+                    let arg_count = instr.imm_u32().unwrap() as u16;
+                    // Temporarily set pushes=0; we'll compute real pushes after type checks.
+                    (arg_count + 1, 0)
+                }
                 OpCode::Ret => (func.return_slots, 0),
                 OpCode::Syscall => {
                     let id = instr.imm_u32().unwrap();
@@ -145,7 +186,121 @@ impl Verifier {
                 });
             }
 
-            let out_height = in_height - pops + pushes;
+            // Compute out types vector with closure-aware rules
+            use SlotTy::*;
+            let mut out_types = in_types.clone();
+            // Pop first
+            for _ in 0..pops {
+                out_types.pop();
+            }
+
+            // Special handling per opcode that affects types/pushes
+            let mut dynamic_pushes: Option<u16> = None;
+            match instr.opcode {
+                OpCode::MakeClosure => {
+                    let (fn_id, _cap) = instr.imm_u32x2().unwrap();
+                    out_types.push(Closure(fn_id));
+                }
+                OpCode::CallClosure => {
+                    // Validate TOS was a known closure and arg_count matches signature
+                    let tos = in_types.last().copied().unwrap_or(Unknown);
+                    match tos {
+                        Closure(fn_id) => {
+                            let callee = all_functions.get(fn_id as usize).ok_or_else(|| {
+                                VerifierError::InvalidFuncId { pc: func_start + pc, id: fn_id }
+                            })?;
+                            let user_argc = instr.imm_u32().unwrap() as u16;
+                            if callee.param_slots == 0 {
+                                // Hidden arg0 must exist in callee signature
+                                return Err(VerifierError::BadClosureArgCount {
+                                    pc: func_start + pc,
+                                    expected: 0,
+                                    got: user_argc,
+                                });
+                            }
+                            let expected_user = callee.param_slots - 1; // exclude hidden arg0
+                            if expected_user != user_argc {
+                                return Err(VerifierError::BadClosureArgCount {
+                                    pc: func_start + pc,
+                                    expected: expected_user,
+                                    got: user_argc,
+                                });
+                            }
+                            // Push callee returns as Unknown types
+                            for _ in 0..callee.return_slots {
+                                out_types.push(Unknown);
+                            }
+                            dynamic_pushes = Some(callee.return_slots);
+                        }
+                        NonClosure => {
+                            return Err(VerifierError::NotAClosureOnCallClosure { pc: func_start + pc });
+                        }
+                        Unknown => {
+                            // We cannot determine return arity; be strict and reject
+                            return Err(VerifierError::UnknownClosureCallee { pc: func_start + pc });
+                        }
+                    }
+                }
+                // Immediates and known non-closure pushes
+                OpCode::PushConst | OpCode::PushI64 | OpCode::PushF64 | OpCode::PushBool
+                | OpCode::PushI32 | OpCode::PushBounded => {
+                    out_types.push(NonClosure);
+                }
+                // Dup duplicates TOS type
+                OpCode::Dup => {
+                    let tos = in_types.last().copied().unwrap_or(Unknown);
+                    if matches!(tos, Unknown) && in_height == 0 {
+                        // Will already have underflowed on pops check for other ops; for Dup, enforce explicitly
+                        return Err(VerifierError::StackUnderflow { pc: func_start + pc, opcode: OpCode::Dup });
+                    }
+                    out_types.push(tos);
+                }
+                // Swap swaps top-2 types; ensure enough stack
+                OpCode::Swap => {
+                    if in_types.len() < 2 {
+                        return Err(VerifierError::StackUnderflow { pc: func_start + pc, opcode: OpCode::Swap });
+                    }
+                    let len = out_types.len();
+                    out_types.swap(len - 1, len - 2);
+                }
+                // Arithmetic/logic produce NonClosure but we don't strictly need it; mark Unknown conservatively
+                // Calls and syscalls return Unknown
+                OpCode::Call => {
+                    let func_id = instr.imm_u32().unwrap();
+                    let callee = all_functions.get(func_id as usize).unwrap();
+                    for _ in 0..callee.return_slots {
+                        out_types.push(Unknown);
+                    }
+                }
+                OpCode::Syscall => {
+                    let id = instr.imm_u32().unwrap();
+                    let syscall = Syscall::from_u32(id).unwrap();
+                    for _ in 0..(syscall.results_count() as u16) {
+                        out_types.push(Unknown);
+                    }
+                }
+                _ => {
+                    // Default: push Unknown for any declared pushes
+                    if spec.pushes > 0 {
+                        for _ in 0..spec.pushes {
+                            out_types.push(Unknown);
+                        }
+                    }
+                }
+            }
+
+            let pushes_final = dynamic_pushes.unwrap_or_else(|| match instr.opcode {
+                OpCode::MakeClosure => 1,
+                OpCode::CallClosure => {
+                    // If we reached here, we handled it above and set dynamic_pushes
+                    0
+                }
+                OpCode::Syscall => spec.pushes, // already added Unknowns above
+                OpCode::Call => spec.pushes,    // already added Unknowns above
+                _ => spec.pushes,
+            });
+
+            let out_height = (out_types.len()) as u16;
             max_stack = max_stack.max(out_height);
 
             // Enforce declared max stack if provided (0 means "no explicit limit")
@@ -220,7 +375,8 @@ impl Verifier {
                         });
                     }
 
-                    if let Some(&existing_height) = stack_height_in.get(&target_rel) {
+                    if let Some(existing_types) = stack_types_in.get_mut(&target_rel) {
+                        let existing_height = existing_types.len() as u16;
                         if existing_height != out_height {
                             return Err(VerifierError::StackMismatchJoin {
                                 pc: func_start + pc,
@@ -228,9 +384,22 @@ impl Verifier {
                                 height_in: out_height,
                                 height_target: existing_height,
                             });
+                        } else {
+                            // Merge types pointwise; if any slot changes, re-enqueue
+                            let mut changed = false;
+                            for i in 0..existing_types.len() {
+                                let joined = join_slot(existing_types[i], out_types[i]);
+                                if joined != existing_types[i] {
+                                    existing_types[i] = joined;
+                                    changed = true;
+                                }
+                            }
+                            if changed {
+                                worklist.push_back(target_rel);
+                            }
                         }
                     } else {
-                        stack_height_in.insert(target_rel, out_height);
+                        stack_types_in.insert(target_rel, out_types.clone());
                         worklist.push_back(target_rel);
                     }
                 }
@@ -240,7 +409,8 @@ impl Verifier {
                 let next_pc = instr.next_pc;
                 let func_len = layouts.get(func_idx).map(|l| l.end - l.start).unwrap_or_else(|| 0);
                 if next_pc < func_len {
-                    if let Some(&existing_height) = stack_height_in.get(&next_pc) {
+                    if let Some(existing_types) = stack_types_in.get_mut(&next_pc) {
+                        let existing_height = existing_types.len() as u16;
                         if existing_height != out_height {
                             return Err(VerifierError::StackMismatchJoin {
                                 pc: func_start + pc,
@@ -248,9 +418,21 @@ impl Verifier {
                                 height_in: out_height,
                                 height_target: existing_height,
                             });
+                        } else {
+                            let mut changed = false;
+                            for i in 0..existing_types.len() {
+                                let joined = join_slot(existing_types[i], out_types[i]);
+                                if joined != existing_types[i] {
+                                    existing_types[i] = joined;
+                                    changed = true;
+                                }
+                            }
+                            if changed {
+                                worklist.push_back(next_pc);
+                            }
                         }
                     } else {
-                        stack_height_in.insert(next_pc, out_height);
+                        stack_types_in.insert(next_pc, out_types);
                         worklist.push_back(next_pc);
                     }
                 } else if next_pc == func_len {

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

@@ -0,0 +1,129 @@
+use prometeu_bytecode::FunctionMeta;
+use prometeu_bytecode::isa::core::CoreOpCode as OpCode;
+use crate::prometeu_vm::verifier::{Verifier, VerifierError};
+
+// Re-export path shim for tests since this file is in integration tests crate scope
+mod prometeu_vm { pub use prometeu_vm::*; }
+
+#[test]
+fn closure_call_valid_passes() {
+    // F0: PushI32 7; MakeClosure(fn=1, cap=0); CallClosure argc=1; PopN 1; Ret
+    // F1: PushI32 1; Ret   (param_slots=2: hidden arg0 + 1 user arg; returns 1)
+    let mut code = Vec::new();
+    // F0 @ 0
+    code.push(OpCode::PushI32 as u8); code.push(0x00);
+    code.extend_from_slice(&7u32.to_le_bytes());
+    code.push(OpCode::MakeClosure as u8); code.push(0x00);
+    code.extend_from_slice(&1u32.to_le_bytes()); // fn id
+    code.extend_from_slice(&0u32.to_le_bytes()); // cap count
+    code.push(OpCode::CallClosure as u8); code.push(0x00);
+    code.extend_from_slice(&1u32.to_le_bytes()); // argc = 1 (excludes hidden)
+    code.push(OpCode::PopN as u8); code.push(0x00);
+    code.extend_from_slice(&1u32.to_le_bytes());
+    code.push(OpCode::Ret as u8); code.push(0x00);
+
+    let f0_len = code.len() as u32;
+
+    // F1 @ f0_len
+    code.push(OpCode::PushI32 as u8); code.push(0x00);
+    code.extend_from_slice(&1u32.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: 0, ..Default::default() },
+        FunctionMeta { code_offset: f0_len, code_len: f1_len, param_slots: 2, return_slots: 1, ..Default::default() },
+    ];
+
+    let res = Verifier::verify(&code, &functions).unwrap();
+    // Max stack in F0: PushI32 (1), MakeClosure (2), CallClosure pops 2 pushes 1 => (1), PopN to 0
+    assert!(res[0] >= 2);
+}
+
+#[test]
+fn closure_call_wrong_argc_fails() {
+    // Same as previous but argc = 0 while callee expects 1 user arg
+    let mut code = Vec::new();
+    // F0 @ 0
+    code.push(OpCode::PushI32 as u8); code.push(0x00);
+    code.extend_from_slice(&7u32.to_le_bytes());
+    code.push(OpCode::MakeClosure as u8); code.push(0x00);
+    code.extend_from_slice(&1u32.to_le_bytes()); // fn id
+    code.extend_from_slice(&0u32.to_le_bytes()); // cap count
+    code.push(OpCode::CallClosure as u8); code.push(0x00);
+    code.extend_from_slice(&0u32.to_le_bytes()); // argc = 0 (mismatch)
+    code.push(OpCode::Ret as u8); code.push(0x00);
+
+    let f0_len = code.len() as u32;
+
+    // F1 @ f0_len
+    code.push(OpCode::PushI32 as u8); code.push(0x00);
+    code.extend_from_slice(&1u32.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: 0, ..Default::default() },
+        FunctionMeta { code_offset: f0_len, code_len: f1_len, param_slots: 2, return_slots: 1, ..Default::default() },
+    ];
+
+    let res = Verifier::verify(&code, &functions);
+    assert!(matches!(res, Err(VerifierError::BadClosureArgCount { .. })));
+}
+
+#[test]
+fn call_closure_on_non_closure_fails() {
+    // F0: PushI32 7; CallClosure argc=0; Ret
+    let mut code = Vec::new();
+    code.push(OpCode::PushI32 as u8); code.push(0x00);
+    code.extend_from_slice(&7u32.to_le_bytes());
+    code.push(OpCode::CallClosure as u8); code.push(0x00);
+    code.extend_from_slice(&0u32.to_le_bytes());
+    code.push(OpCode::Ret as u8); code.push(0x00);
+
+    let functions = vec![FunctionMeta { code_offset: 0, code_len: code.len() as u32, return_slots: 0, ..Default::default() }];
+    let res = Verifier::verify(&code, &functions);
+    assert!(matches!(res, Err(VerifierError::NotAClosureOnCallClosure { .. })));
+}
+
+#[test]
+fn nested_closure_calls_verify() {
+    // F0: MakeClosure(fn=1,0); CallClosure argc=0; PopN 1; Ret
+    // F1: MakeClosure(fn=2,0); CallClosure argc=0; Ret        (param=1 hidden, ret=1)
+    // F2: PushI32 5; Ret                                      (param=1 hidden, ret=1)
+    let mut code = Vec::new();
+    // F0 @ 0
+    code.push(OpCode::MakeClosure as u8); code.push(0x00);
+    code.extend_from_slice(&1u32.to_le_bytes()); // F1
+    code.extend_from_slice(&0u32.to_le_bytes()); // cap=0
+    code.push(OpCode::CallClosure as u8); code.push(0x00);
+    code.extend_from_slice(&0u32.to_le_bytes()); // argc=0
+    code.push(OpCode::PopN as u8); code.push(0x00);
+    code.extend_from_slice(&1u32.to_le_bytes());
+    code.push(OpCode::Ret as u8); code.push(0x00);
+    let f0_len = code.len() as u32;
+
+    // F1 @ f0_len
+    code.push(OpCode::MakeClosure as u8); code.push(0x00);
+    code.extend_from_slice(&2u32.to_le_bytes()); // F2
+    code.extend_from_slice(&0u32.to_le_bytes()); // cap=0
+    code.push(OpCode::CallClosure as u8); code.push(0x00);
+    code.extend_from_slice(&0u32.to_le_bytes()); // argc=0
+    code.push(OpCode::Ret as u8); code.push(0x00);
+    let f1_len = (code.len() as u32) - f0_len;
+
+    // F2 @ f0_len + f1_len
+    code.push(OpCode::PushI32 as u8); code.push(0x00);
+    code.extend_from_slice(&5u32.to_le_bytes());
+    code.push(OpCode::Ret as u8); code.push(0x00);
+    let f2_len = (code.len() as u32) - f0_len - f1_len;
+
+    let functions = vec![
+        FunctionMeta { code_offset: 0, code_len: f0_len, return_slots: 0, ..Default::default() },
+        FunctionMeta { code_offset: f0_len, code_len: f1_len, param_slots: 1, return_slots: 1, ..Default::default() },
+        FunctionMeta { code_offset: f0_len + f1_len, code_len: f2_len, param_slots: 1, return_slots: 1, ..Default::default() },
+    ];
+
+    let res = Verifier::verify(&code, &functions).unwrap();
+    assert!(res[0] >= 1);
+}

files/TODOs.md

@@ -1,83 +1,3 @@
-# PR-6.5 — Verifier Support for Closures (Model B)
-
-## Briefing
-
-The verifier must understand closure values and enforce safe invocation rules.
-
-Under Model B:
-
-* `CALL_CLOSURE` injects hidden `arg0`.
-* User-visible arg_count excludes hidden arg.
-* Captures are accessed via explicit instructions (future PR).
-
----
-
-## Target
-
-Extend verifier to:
-
-1. Introduce stack type: `ClosureValue`.
-2. Validate MAKE_CLOSURE effects.
-3. Validate CALL_CLOSURE semantics:
-
-  * Ensure top of stack is ClosureValue.
-  * Ensure sufficient args present.
-  * Validate `arg_count` matches function signature expectations.
-  * Account for hidden arg0 when checking callee arg arity.
-4. Validate ret_slots against function metadata.
-
----
-
-## Work Items
-
-1. Extend type lattice with ClosureValue.
-2. Define stack transitions for MAKE_CLOSURE.
-3. Define stack transitions for CALL_CLOSURE.
-4. Enforce strict failure on mismatch.
-
----
-
-## Acceptance Checklist
-
-* [ ] ClosureValue type exists.
-* [ ] Invalid CALL_CLOSURE rejected.
-* [ ] Hidden arg0 accounted for.
-* [ ] ret_slots validated.
-* [ ] All verifier tests pass.
-
----
-
-## Tests
-
-1. Valid closure call passes verification.
-2. CALL_CLOSURE with wrong arg_count fails.
-3. CALL_CLOSURE on non-closure fails verification.
-4. Nested closure calls verify correctly.
-
----
-
-## Junie Instructions
-
-You MAY:
-
-* Extend verifier model.
-* Add tests.
-
-You MUST NOT:
-
-* Weaken verification rules.
-* Replace verifier checks with runtime-only traps.
-
-If function metadata (arg_slots/ret_slots) is insufficient, STOP and request clarification.
-
----
-
-## Definition of Done
-
-Verifier fully supports closure creation and invocation under Model B semantics.
-
----
-
 # PR-7 — Coroutines (Cooperative, Deterministic, No Mailbox)
 
 Coroutines are the **only concurrency model** in the Prometeu VM.
@@ -413,3 +333,495 @@ Tests must not depend on wall clock or randomness.
 * No mailbox.
 * GC and verifier fully integrated.
 * All tests pass.
+
+---
+
+# PR-8 — Tooling & Test Harness (JVM-Grade Discipline)
+
+This phase establishes tooling and test discipline required to keep the Prometeu VM at JVM-grade quality.
+
+Goals:
+
+* Deterministic execution
+* Reproducible tests
+* Strong disassembler guarantees
+* Layered test coverage
+* Zero legacy artifacts enforcement
+
+Each PR below is self-contained and must compile independently.
+
+---
+
+# PR-8.1 — Disassembler (Roundtrip + Snapshot Reliability)
+
+## Briefing
+
+The disassembler must be:
+
+* Deterministic
+* Complete
+* Roundtrip-safe (encode → decode → encode)
+* Snapshot-friendly
+
+It must fully support:
+
+* New opcodes (MAKE_CLOSURE, CALL_CLOSURE, SPAWN, YIELD, SLEEP)
+* Updated syscall representation
+* Closure and coroutine instructions
+
+## Target
+
+1. Update disassembler to support all new opcodes.
+2. Guarantee stable formatting.
+3. Add roundtrip validation tests.
+
+Formatting rules:
+
+* No unstable ordering.
+* No implicit formatting differences across platforms.
+* Explicit numeric representation where required.
+
+## Acceptance Checklist
+
+* [ ] All opcodes supported.
+* [ ] Deterministic formatting.
+* [ ] Roundtrip encode/decode test passes.
+* [ ] Snapshot tests stable.
+
+## Tests
+
+1. Encode → disasm → reassemble → byte-equal check.
+2. Snapshot test for representative programs.
+3. Closure/coroutine disasm coverage.
+
+## Junie Instructions
+
+You MAY:
+
+* Modify disassembler module.
+* Add snapshot tests.
+
+You MUST NOT:
+
+* Change bytecode encoding format.
+* Introduce formatting randomness.
+
+If any opcode semantics unclear, STOP and ask.
+
+---
+
+# PR-8.2 — Deterministic Execution Harness
+
+## Briefing
+
+The VM must be testable deterministically.
+
+Requirements:
+
+* No wall-clock time.
+* Controlled tick progression.
+* Fixed seed where randomness exists (if any).
+
+## Target
+
+Introduce a test harness wrapper:
+
+* Controlled `tick` counter.
+* Deterministic scheduler stepping.
+* Explicit run_budget boundaries.
+
+Provide utilities:
+
+* `run_until_halt()`
+* `run_ticks(n)`
+* `run_frames(n)`
+
+No external timing.
+
+## Acceptance Checklist
+
+* [ ] No real-time dependencies.
+* [ ] Deterministic coroutine wake order.
+* [ ] Repeatable runs produce identical traces.
+
+## Tests
+
+1. Same program run twice produces identical state traces.
+2. Sleep/wake ordering stable.
+
+## Junie Instructions
+
+You MAY:
+
+* Extend test harness.
+* Add deterministic trace utilities.
+
+You MUST NOT:
+
+* Introduce randomness.
+* Use system time.
+
+If current VM depends on real time, STOP and refactor before proceeding.
+
+---
+
+# PR-8.3 — Layered Test Suite Architecture
+
+## Briefing
+
+Tests must be structured by layer to isolate failures.
+
+Layers:
+
+1. Bytecode encode/decode
+2. Verifier
+3. VM execution
+4. GC behavior
+5. Scheduler behavior
+
+## Target
+
+Organize tests into modules per layer.
+
+Enforce:
+
+* No cross-layer assumptions.
+* Verifier tests do not execute VM.
+* VM tests assume verified input.
+
+Add minimal coverage per layer.
+
+## Acceptance Checklist
+
+* [ ] Tests grouped logically.
+* [ ] No duplicated logic.
+* [ ] Clear separation of concerns.
+
+## Tests
+
+Add representative tests per layer:
+
+* Encode/decode edge cases.
+* Verifier rejects invalid closures.
+* VM executes valid programs.
+* GC collects unreachable closures.
+* Scheduler deterministic ordering.
+
+## Junie Instructions
+
+You MAY:
+
+* Refactor test layout.
+* Add missing coverage.
+
+You MUST NOT:
+
+* Merge unrelated layers.
+* Hide verifier failures inside runtime traps.
+
+If a test spans layers, STOP and split appropriately.
+
+---
+
+# PR-8.4 — No Legacy Artifacts Enforcement
+
+## Briefing
+
+The codebase must not contain legacy RC/HIP artifacts.
+
+Forbidden patterns:
+
+* retain
+* release
+* hip
+* gate
+* borrow
+* scope (legacy usage context)
+* RC-related modules
+
+## Target
+
+Implement automated check:
+
+* Script or test that scans source tree for forbidden symbols.
+* Fails CI if found.
+
+Also:
+
+* Remove dead modules/files.
+* Remove unused features.
+
+## Acceptance Checklist
+
+* [ ] Automated legacy scan exists.
+* [ ] No legacy symbols present.
+* [ ] Dead modules removed.
+
+## Tests
+
+1. Intentionally insert forbidden symbol in test branch → test fails.
+2. Scan passes on clean tree.
+
+## Junie Instructions
+
+You MAY:
+
+* Add static scan test.
+* Remove dead code.
+
+You MUST NOT:
+
+* Suppress warnings instead of fixing code.
+* Leave deprecated modules commented out.
+
+If unsure whether a symbol is legacy or valid, STOP and ask.
+
+---
+
+## Final Definition of Done
+
+* Disassembler roundtrip-safe.
+* Deterministic harness in place.
+* Layered test suite established.
+* No legacy artifacts remain.
+* All tests reproducible and stable.
+
+---
+
+# PR-9 — Final Hardening & Baseline Documentation
+
+This phase finalizes the new Prometeu VM baseline after the architectural reset (GC, closures, coroutines, unified syscall ABI, deterministic scheduler).
+
+Goals:
+
+* Consolidated architecture documentation (short, precise, authoritative)
+* Minimal and controlled public surface area
+* Removal of temporary feature flags
+* Final cleanup: dead code, warnings, outdated docs/examples
+
+All PRs below are self-contained and must compile independently.
+
+---
+
+# PR-9.1 — Consolidated Architecture Documentation
+
+## Briefing
+
+The project must include a short, authoritative architecture document in English describing the new baseline.
+
+It must reflect the current state only (no legacy, no transitional wording).
+
+This document becomes the canonical reference for contributors.
+
+## Target
+
+Create `ARCHITECTURE.md` at repository root with sections:
+
+1. Overview
+
+    * Stack-based VM
+    * GC-managed heap (mark-sweep, non-compacting)
+    * Closures (Model B, hidden arg0)
+    * Cooperative coroutines (FRAME_SYNC safepoints)
+    * Unified syscall ABI
+
+2. Memory Model
+
+    * Stack vs heap
+    * Heap object kinds
+    * GC roots (VM + suspended coroutines)
+
+3. Execution Model
+
+    * Interpreter loop
+    * Safepoints
+    * Scheduler behavior
+
+4. Verification Model
+
+    * Verifier responsibilities
+    * Runtime vs verifier guarantees
+
+5. Non-Goals
+
+    * No RC
+    * No HIP
+    * No preemption
+    * No mailbox
+
+The document must be concise (no more than ~4–6 pages equivalent).
+
+## Acceptance Checklist
+
+* [ ] ARCHITECTURE.md exists.
+* [ ] No mention of RC/HIP.
+* [ ] Reflects actual implementation.
+* [ ] Reviewed for consistency with code.
+
+## Tests
+
+Manual review required.
+
+## Junie Instructions
+
+You MAY:
+
+* Create new documentation files.
+
+You MUST NOT:
+
+* Invent features not implemented.
+* Reference legacy behavior.
+
+If architecture details are unclear, STOP and request clarification.
+
+---
+
+# PR-9.2 — Public Surface Area Minimization
+
+## Briefing
+
+The public API must be minimal and intentional.
+
+Internal modules must not leak implementation details.
+
+## Target
+
+1. Audit all `pub` items.
+2. Reduce visibility to `pub(crate)` where possible.
+3. Hide internal modules behind private boundaries.
+4. Ensure only intended API is exported.
+
+Focus areas:
+
+* VM core
+* Heap internals
+* Scheduler internals
+* GC internals
+
+## Acceptance Checklist
+
+* [ ] No unnecessary `pub` items.
+* [ ] Public API documented.
+* [ ] Internal types hidden.
+* [ ] `cargo doc` shows clean public surface.
+
+## Tests
+
+* Build documentation.
+* Ensure no accidental public modules remain.
+
+## Junie Instructions
+
+You MAY:
+
+* Restrict visibility.
+* Refactor module structure.
+
+You MUST NOT:
+
+* Break existing internal usage.
+* Expose new APIs casually.
+
+If removing `pub` causes architectural issue, STOP and escalate.
+
+---
+
+# PR-9.3 — Remove Temporary Feature Flags
+
+## Briefing
+
+During refactor phases, temporary feature flags or conditional compilation may have been introduced.
+
+These must not remain in the final baseline.
+
+## Target
+
+1. Identify all feature flags related to transitional behavior.
+2. Remove obsolete `cfg` gates.
+3. Remove commented legacy branches.
+4. Ensure single authoritative execution path.
+
+## Acceptance Checklist
+
+* [ ] No transitional feature flags remain.
+* [ ] No commented-out legacy logic.
+* [ ] Single execution model.
+* [ ] All tests pass.
+
+## Tests
+
+* Full test suite passes without feature toggles.
+
+## Junie Instructions
+
+You MAY:
+
+* Remove obsolete flags.
+* Simplify code paths.
+
+You MUST NOT:
+
+* Remove legitimate platform flags.
+* Leave partial dead branches.
+
+If unsure whether a flag is temporary or architectural, STOP and ask.
+
+---
+
+# PR-9.4 — Final Cleanup & Quality Sweep
+
+## Briefing
+
+This PR performs the final cleanup pass.
+
+Goal: Zero warnings. No dead code. No outdated examples.
+
+## Target
+
+1. Remove dead modules/files.
+2. Remove unused imports and code.
+3. Eliminate compiler warnings.
+4. Update outdated examples.
+5. Remove stale TODOs referencing removed architecture.
+
+Optional (if present):
+
+* Enforce `cargo clippy` clean baseline.
+* Ensure `rustfmt` compliance.
+
+## Acceptance Checklist
+
+* [ ] No dead code.
+* [ ] Zero compiler warnings.
+* [ ] Clippy clean (if configured).
+* [ ] Examples reflect new baseline.
+* [ ] No TODO referencing RC/HIP.
+
+## Tests
+
+* Full test suite passes.
+* Clean build with warnings denied (if configured).
+
+## Junie Instructions
+
+You MAY:
+
+* Remove unused code.
+* Refactor minor clarity issues.
+
+You MUST NOT:
+
+* Introduce new features.
+* Change runtime semantics.
+
+If cleanup requires semantic change, STOP and split into new PR.
+
+---
+
+## Final Definition of Done
+
+* Architecture documented clearly.
+* Public API minimal and controlled.
+* No temporary flags remain.
+* Codebase clean, warning-free, and aligned with the new VM baseline.

files/VM RESET.md

@@ -1,8 +0,0 @@
-vamos as PR9s todas em um unico canvas markdown ingles, devem ser auto contidas com briefing, alvo, checklist, test quando necessario e comandos do que a Junie pode ou nao fazer (Junie eh task operator nao arquiteta ou assume nada, questiona quando necessario).
-
-9 — Hardening final e documentação do novo baseline
-
-9.1. Consolidar documentação de arquitetura (curta, objetiva, em inglês).
-9.2. Garantir que o “surface area” público está minimalista (APIs internas escondidas).
-9.3. Remover qualquer feature flag temporária que tenha sobrado.
-9.4. Rodar limpeza final: dead code, warnings, docs desatualizadas, exemplos antigos.