File size: 4,296 Bytes
1d3f990 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 | //! Proof Validator — orchestrates checking and rollback
use crate::proof_ir::{ProofTerm, ProofContext, ProofObligation};
use crate::checker::TypeChecker;
use crate::rollback::{RollbackManager, WormCheckpoint};
use crate::schema::{ProofEvent, ViolationEvent};
use anyhow::{Result, Context};
use tracing::{warn, error, info};
pub struct ProofValidator {
checker: TypeChecker,
rollback_mgr: RollbackManager,
proof_context: ProofContext,
violation_count: u64,
}
impl ProofValidator {
pub fn new(rollback_mgr: RollbackManager) -> Self {
Self {
checker: TypeChecker::new(),
rollback_mgr,
proof_context: ProofContext::new(),
violation_count: 0,
}
}
/// Validate a mutation against current proof context
/// Returns Ok(()) if valid, Err with rollback if violated
pub fn validate_mutation(
&mut self,
mutation: &str,
invariants: &[String],
) -> Result<()> {
// 1. Construct proof obligation
let obligation = ProofObligation::InvariantPreservation {
address: 0,
old_value: 0,
new_value: 0,
invariants: invariants.to_vec(),
};
// 2. Type-check the proof term
let proof_term = self.proof_context.construct_proof(&obligation)?;
match self.checker.check(&proof_term) {
Ok(_) => {
// Proof valid — record in context
self.proof_context.add_proof(obligation, proof_term);
self.emit_audit(ProofEvent::Validated {
mutation: mutation.to_string(),
});
Ok(())
}
Err(e) => {
self.violation_count += 1;
error!(?mutation, violation = %e, "Invariant violation detected");
// Emit violation event to audit trail
self.emit_audit(ProofEvent::Violated {
mutation: mutation.to_string(),
error: e.to_string(),
violation_id: self.violation_count,
});
// 3. Rollback to last valid checkpoint
let checkpoint = self.rollback_mgr.last_valid_checkpoint()
.context("No valid checkpoint for rollback")?;
self.rollback_mgr.rollback(&checkpoint)?;
// Emit rollback event
self.emit_audit(ProofEvent::RolledBack {
checkpoint: checkpoint.id,
violation_id: self.violation_count,
});
Err(anyhow::anyhow!("Invariant violated, rolled back: {}", e))
}
}
}
/// Add a WORM checkpoint
pub fn add_checkpoint(&mut self, checkpoint: WormCheckpoint) {
self.rollback_mgr.add_checkpoint(checkpoint);
}
fn emit_audit(&self, event: ProofEvent) {
// In production, this would emit to Bifrost Bridge audit chain
info!("Proof audit: {:?}", event);
}
pub fn violation_count(&self) -> u64 {
self.violation_count
}
}
impl Default for ProofValidator {
fn default() -> Self {
Self::new(RollbackManager::default())
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_validator_creation() {
let validator = ProofValidator::default();
assert_eq!(validator.violation_count(), 0);
}
#[test]
fn test_validate_mutation() {
let mut validator = ProofValidator::default();
let result = validator.validate_mutation("M[0] ← 42", &["M[0] > 0".into()]);
// May succeed or fail depending on proof construction
let _ = result;
}
#[test]
fn test_add_checkpoint() {
let mut validator = ProofValidator::default();
let cp = WormCheckpoint {
id: "cp1".into(),
ip: 0,
step_count: 0,
mutation_log_len: 0,
timestamp: 0,
memory_snapshot: vec![],
};
validator.add_checkpoint(cp);
assert!(validator.rollback_mgr.last_valid_checkpoint().is_some());
}
}
|