fix(docs): Correct archive path in ovsm-language.html

Update legacy documentation link to point to the correct
-DEPRECATED directory name for archived planning language docs.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <[email protected]>

Author: 0xrinegade

crates/ovsm/src/compiler/formal_verification.rs

@@ -0,0 +1,321 @@
+//! # Formal Verification Module (Z3 Integration Design)
+//!
+//! This module provides compile-time formal verification of memory safety
+//! using SMT solving (Z3 or similar). The goal is to prove, at compile time,
+//! that a program has no out-of-bounds memory accesses.
+//!
+//! ## Design Overview
+//!
+//! ### 1. Verification Pipeline
+//!
+//! ```text
+//! OVSM Source → IR Generator → IrProgram → SMT Encoder → Z3 Solver → Verdict
+//!                    │                          │
+//!                    │                          ├── SAFE: No violations found
+//!                    │                          ├── UNSAFE: Counter-example provided
+//!                    ▼                          └── UNKNOWN: Timeout/complexity
+//!               TypeEnv (pointer provenance)
+//! ```
+//!
+//! ### 2. SMT Encoding Strategy
+//!
+//! **Variables:**
+//! - Each virtual register `Ri` becomes an SMT bitvector `r_i: BitVec(64)`
+//! - Memory regions become SMT arrays `mem_acct[k]: Array(BitVec(64), BitVec(64))`
+//! - Bounds become symbolic pairs `bounds_ptr_i: (start: BitVec(64), len: BitVec(64))`
+//!
+//! **Instructions → SMT Assertions:**
+//! ```lisp
+//! ; ConstI64(Ri, v) →
+//! (assert (= r_i #x0000000000000001))
+//!
+//! ; Add(Rd, Ra, Rb) →
+//! (assert (= r_d (bvadd r_a r_b)))
+//!
+//! ; Load(Rd, Rbase, offset) →
+//! (assert (and
+//!   (bvuge (bvadd r_base offset) bounds_base_start)
+//!   (bvult (bvadd r_base offset 8) (bvadd bounds_base_start bounds_base_len))
+//! ))
+//! (assert (= r_d (select mem_region r_base_plus_offset)))
+//!
+//! ; Store(Rbase, Rval, offset) →
+//! (assert (and
+//!   (bvuge (bvadd r_base offset) bounds_base_start)
+//!   (bvult (bvadd r_base offset 8) (bvadd bounds_base_start bounds_base_len))
+//!   writable_region
+//! ))
+//! ```
+//!
+//! ### 3. Verification Checks
+//!
+//! For each memory access (Load/Store), we generate:
+//! 1. **In-bounds assertion**: offset + access_size ≤ region_size
+//! 2. **Alignment assertion**: offset % alignment == 0
+//! 3. **Writability assertion** (for Store): region.writable == true
+//!
+//! We then check:
+//! ```lisp
+//! (check-sat)
+//! ; If UNSAT, the access is always safe
+//! ; If SAT, we have a counter-example (input that causes violation)
+//! ```
+//!
+//! ### 4. Loop Handling
+//!
+//! Loops require special treatment:
+//! - **Bounded loops**: Unroll up to a limit, verify each iteration
+//! - **Unbounded loops**: Use loop invariants (manual annotation or inference)
+//! - **Conservative approach**: Treat loop-dependent values as unconstrained
+//!
+//! ### 5. Integration Points
+//!
+//! **TypeEnv provides:**
+//! - Register types (Value/Pointer/Bool)
+//! - Pointer provenance (which region, what bounds)
+//! - Accumulated memory errors (for reporting)
+//!
+//! **Z3 proves:**
+//! - No execution path leads to out-of-bounds access
+//! - All alignment constraints are satisfied
+//! - No writes to read-only regions
+//!
+//! ### 6. API Design
+//!
+//! ```rust,ignore
+//! pub struct Verifier {
+//!     solver: z3::Solver,
+//!     ctx: z3::Context,
+//! }
+//!
+//! impl Verifier {
+//!     pub fn verify(&self, program: &IrProgram, type_env: &TypeEnv) -> VerificationResult {
+//!         // 1. Encode IR instructions as SMT assertions
+//!         let smt_program = self.encode(program, type_env);
+//!
+//!         // 2. Add safety properties to check
+//!         self.add_memory_safety_properties(&smt_program);
+//!
+//!         // 3. Solve and interpret result
+//!         match self.solver.check() {
+//!             SatResult::Unsat => VerificationResult::Safe,
+//!             SatResult::Sat => {
+//!                 let model = self.solver.get_model();
+//!                 VerificationResult::Unsafe(self.extract_counterexample(model))
+//!             }
+//!             SatResult::Unknown => VerificationResult::Unknown("timeout or complexity".into()),
+//!         }
+//!     }
+//! }
+//! ```
+//!
+//! ### 7. Practical Considerations
+//!
+//! **Performance:**
+//! - Verification is O(expensive) but runs at compile time
+//! - Can be opt-in: `osvm ovsm compile --verify`
+//! - Cache verification results for unchanged code
+//!
+//! **Soundness:**
+//! - Must correctly model Solana sBPF semantics
+//! - Account data sizes are symbolic (dynamic)
+//! - CPI effects are conservatively modeled (may clobber memory)
+//!
+//! **Limitations:**
+//! - Undecidable in general (halting problem)
+//! - Loops may require manual invariants
+//! - External calls (syscalls) modeled conservatively
+//!
+//! ### 8. Future Enhancements
+//!
+//! - **Property annotations**: `(assert-safe expr)` in OVSM code
+//! - **Incremental verification**: Only re-verify changed functions
+//! - **Counter-example guided refinement**: Learn from failed proofs
+//! - **Parallel solving**: Use multiple Z3 instances for different paths
+
+/// Verification result from formal analysis
+#[derive(Debug, Clone)]
+pub enum VerificationResult {
+    /// Program proven memory-safe
+    Safe,
+    /// Found input that causes memory violation
+    Unsafe(CounterExample),
+    /// Verification incomplete (timeout/complexity)
+    Unknown(String),
+}
+
+/// Counter-example showing how a memory violation can occur
+#[derive(Debug, Clone)]
+pub struct CounterExample {
+    /// Register values that trigger the violation
+    pub register_values: Vec<(u32, u64)>,
+    /// The instruction that violates memory safety
+    pub violating_instruction: String,
+    /// The memory access that would be out of bounds
+    pub access: MemoryAccess,
+}
+
+/// Details of a memory access
+#[derive(Debug, Clone)]
+pub struct MemoryAccess {
+    pub base_register: u32,
+    pub offset: i64,
+    pub size: i64,
+    pub is_write: bool,
+}
+
+/// SMT constraint representing a memory safety check
+#[derive(Debug, Clone)]
+pub enum SmtConstraint {
+    /// Register equals constant
+    Const { reg: u32, value: i64 },
+    /// Register equals sum of two registers
+    Add { dst: u32, lhs: u32, rhs: u32 },
+    /// Memory access within bounds
+    InBounds { base: u32, offset: i64, size: i64, max_len: u32 },
+    /// Memory region is writable
+    Writable { base: u32 },
+    /// Branch condition
+    Branch { cond: u32, target: String },
+}
+
+/// Placeholder for Z3 integration
+/// Full implementation requires z3 crate as dependency
+pub struct Verifier {
+    /// Accumulated constraints from IR analysis
+    constraints: Vec<SmtConstraint>,
+    /// Counter for memory access checks
+    access_count: usize,
+}
+
+impl Verifier {
+    pub fn new() -> Self {
+        Verifier {
+            constraints: Vec::new(),
+            access_count: 0,
+        }
+    }
+
+    /// Add a constraint for a memory load
+    pub fn add_load_constraint(&mut self, base: u32, offset: i64, size: i64, max_len_reg: Option<u32>) {
+        self.access_count += 1;
+        if let Some(max_len) = max_len_reg {
+            self.constraints.push(SmtConstraint::InBounds { base, offset, size, max_len });
+        }
+    }
+
+    /// Add a constraint for a memory store
+    pub fn add_store_constraint(&mut self, base: u32, offset: i64, size: i64, max_len_reg: Option<u32>) {
+        self.access_count += 1;
+        self.constraints.push(SmtConstraint::Writable { base });
+        if let Some(max_len) = max_len_reg {
+            self.constraints.push(SmtConstraint::InBounds { base, offset, size, max_len });
+        }
+    }
+
+    /// Export constraints as SMT-LIB format (for external Z3 invocation)
+    pub fn to_smtlib(&self) -> String {
+        let mut smt = String::new();
+        smt.push_str("; OVSM Memory Safety Verification\n");
+        smt.push_str("(set-logic QF_BV)\n\n");
+
+        // Declare registers as bitvectors
+        let max_reg = self.constraints.iter()
+            .filter_map(|c| match c {
+                SmtConstraint::Const { reg, .. } => Some(*reg),
+                SmtConstraint::Add { dst, lhs, rhs } => Some(*dst.max(lhs).max(rhs)),
+                SmtConstraint::InBounds { base, max_len, .. } => Some(*base.max(max_len)),
+                SmtConstraint::Writable { base } => Some(*base),
+                SmtConstraint::Branch { cond, .. } => Some(*cond),
+            })
+            .max()
+            .unwrap_or(0);
+
+        for i in 0..=max_reg {
+            smt.push_str(&format!("(declare-const r{} (_ BitVec 64))\n", i));
+        }
+        smt.push('\n');
+
+        // Add constraints
+        for constraint in &self.constraints {
+            match constraint {
+                SmtConstraint::Const { reg, value } => {
+                    smt.push_str(&format!(
+                        "(assert (= r{} #x{:016x}))\n",
+                        reg, *value as u64
+                    ));
+                }
+                SmtConstraint::Add { dst, lhs, rhs } => {
+                    smt.push_str(&format!(
+                        "(assert (= r{} (bvadd r{} r{})))\n",
+                        dst, lhs, rhs
+                    ));
+                }
+                SmtConstraint::InBounds { base, offset, size, max_len } => {
+                    // Access must end before max_len
+                    let end_offset = *offset + *size;
+                    smt.push_str(&format!(
+                        "; Bounds check: base=r{}, offset={}, size={}\n",
+                        base, offset, size
+                    ));
+                    smt.push_str(&format!(
+                        "(assert (bvult (bvadd r{} #x{:016x}) r{}))\n",
+                        base, end_offset as u64, max_len
+                    ));
+                }
+                SmtConstraint::Writable { base } => {
+                    smt.push_str(&format!(
+                        "; Writability check for region at r{}\n",
+                        base
+                    ));
+                    // In practice, this would check against known writable regions
+                }
+                SmtConstraint::Branch { cond, target } => {
+                    smt.push_str(&format!(
+                        "; Branch on r{} to {}\n",
+                        cond, target
+                    ));
+                }
+            }
+        }
+
+        smt.push_str("\n(check-sat)\n");
+        smt.push_str("(get-model)\n");
+        smt
+    }
+
+    /// Get number of memory accesses verified
+    pub fn access_count(&self) -> usize {
+        self.access_count
+    }
+}
+
+impl Default for Verifier {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_verifier_basic() {
+        let mut v = Verifier::new();
+        v.add_load_constraint(1, 0, 8, Some(2));
+        assert_eq!(v.access_count(), 1);
+    }
+
+    #[test]
+    fn test_smtlib_output() {
+        let mut v = Verifier::new();
+        v.constraints.push(SmtConstraint::Const { reg: 0, value: 100 });
+        v.constraints.push(SmtConstraint::InBounds { base: 1, offset: 0, size: 8, max_len: 0 });
+
+        let smt = v.to_smtlib();
+        assert!(smt.contains("(set-logic QF_BV)"));
+        assert!(smt.contains("(declare-const r0"));
+        assert!(smt.contains("(check-sat)"));
+    }
+}