Skip to main content

archimedes_kernel/verification/
mod.rs

1use serde::{Deserialize, Serialize};
2use sha2::{Digest, Sha256};
3
4use crate::movement::{Event, HashValue, MovementComposition, MovementMemory};
5use crate::primitives::{Boundary, Identity, Law, Reality, State};
6
7fn write_bytes(hasher: &mut Sha256, bytes: &[u8]) {
8    hasher.update((bytes.len() as u64).to_le_bytes());
9    hasher.update(bytes);
10}
11
12fn write_str(hasher: &mut Sha256, s: &str) {
13    write_bytes(hasher, s.as_bytes());
14}
15
16fn write_string_vec(hasher: &mut Sha256, items: &[String]) {
17    hasher.update((items.len() as u64).to_le_bytes());
18    for item in items {
19        write_str(hasher, item);
20    }
21}
22
23fn write_transition_vec(hasher: &mut Sha256, items: &[(String, String)]) {
24    hasher.update((items.len() as u64).to_le_bytes());
25    for (from, to) in items {
26        write_str(hasher, from);
27        write_str(hasher, to);
28    }
29}
30
31#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
32pub struct Inspection {
33    pub initial_state: State,
34    pub memory: MovementMemory,
35    pub current_state: State,
36}
37
38#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
39pub struct Replay {
40    pub replayed_state: State,
41    pub passed: bool,
42}
43
44#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
45pub struct Continuity {
46    pub preserved: bool,
47}
48
49#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
50pub struct DriftCheck {
51    pub hidden_state_mutation_detected: bool,
52    pub hidden_boundary_growth_detected: bool,
53    pub hidden_law_growth_detected: bool,
54    pub permission_drift_detected: bool,
55    pub hidden_drift_required: bool,
56}
57
58#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
59pub struct ProofResult {
60    pub reality_exists: bool,
61    pub identity_confirmed: bool,
62    pub active_boundary_confirmed: bool,
63    pub active_law_confirmed: bool,
64    pub state_confirmed: bool,
65    pub event_received: bool,
66    pub event_directly_mutated_state: bool,
67    pub law_check_performed: bool,
68    pub law_check_result: bool,
69    pub transition_recorded: bool,
70    pub transition_grounded_in_law_check: bool,
71    pub movement_memory_recorded: bool,
72    pub inspection_available: bool,
73    pub replay_result: bool,
74    pub continuity_result: bool,
75    pub hidden_state_mutation_detected: bool,
76    pub hidden_boundary_growth_detected: bool,
77    pub hidden_law_growth_detected: bool,
78    pub permission_drift_detected: bool,
79    pub hidden_drift_required: bool,
80    pub proof_status: bool,
81}
82
83#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
84pub enum MovementError {
85    RealityMissing,
86    IdentityMissingOrUnstable,
87    BoundaryMissing,
88    LawMissing,
89    StateMissing,
90    StateOutsideBoundary,
91    EventMutatesStateDirectly,
92    LawCheckMissing,
93    TransitionBeforeLawCheck,
94    TransitionUnrecorded,
95    TransitionNotGroundedInLawCheck,
96    MovementMemoryMissing,
97    InspectionHidesProofPath,
98    ReplayChecksOnlyFinalState,
99    ContinuityAssertedWithoutReplay,
100    DriftCheckDetectedHiddenStateMutation,
101    DriftCheckDetectedHiddenBoundaryGrowth,
102    DriftCheckDetectedHiddenLawGrowth,
103    DriftCheckDetectedPermissionDrift,
104    ProofResultDeclaresPassWithoutEvidence,
105}
106
107impl std::fmt::Display for MovementError {
108    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
109        write!(f, "{:?}", self)
110    }
111}
112
113impl std::error::Error for MovementError {}
114
115pub fn detect_drift(
116    original_boundary: &Boundary,
117    original_law: &Law,
118    current_boundary: &Boundary,
119    current_law: &Law,
120    replay_result: bool,
121) -> DriftCheck {
122    let hidden_state_mutation_detected = !replay_result;
123    let hidden_boundary_growth_detected = original_boundary != current_boundary;
124    let hidden_law_growth_detected = original_law != current_law;
125    let permission_drift_detected = hidden_law_growth_detected;
126    let hidden_drift_required = hidden_state_mutation_detected
127        || hidden_boundary_growth_detected
128        || hidden_law_growth_detected
129        || permission_drift_detected;
130
131    DriftCheck {
132        hidden_state_mutation_detected,
133        hidden_boundary_growth_detected,
134        hidden_law_growth_detected,
135        permission_drift_detected,
136        hidden_drift_required,
137    }
138}
139
140#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
141pub struct VerificationReport {
142    pub inspection: Inspection,
143    pub replay: Replay,
144    pub continuity: Continuity,
145    pub memory_integrity: bool,
146}
147
148#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
149pub struct PlannedSequence {
150    pub final_state: State,
151    pub transition_count: usize,
152    pub proofs: Vec<ProofResult>,
153}
154
155#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
156pub struct RealityFingerprint(pub [u8; 32]);
157
158#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
159pub struct IntegrityReport {
160    pub fingerprint: RealityFingerprint,
161    pub drift: DriftCheck,
162    pub memory_integrity: bool,
163    pub replay: Replay,
164    pub continuity: Continuity,
165    pub state: State,
166    pub transition_count: usize,
167}
168
169#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
170pub struct SimulationReport {
171    pub planned: PlannedSequence,
172    pub integrity: IntegrityReport,
173    pub composition: Option<MovementComposition>,
174    pub fingerprint: RealityFingerprint,
175}
176
177#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
178pub struct RealityDiff {
179    pub identity_same: bool,
180    pub boundary_same: bool,
181    pub law_same: bool,
182    pub state_same: bool,
183    pub initial_state_same: bool,
184    pub birth_boundary_same: bool,
185    pub birth_law_same: bool,
186    pub memory_hash_same: bool,
187    pub transition_count_same: bool,
188    pub fingerprint_same: bool,
189}
190
191#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
192pub struct PreflightReport {
193    pub results: Vec<bool>,
194    pub sequence_lawful: bool,
195    pub final_state: Option<State>,
196    pub transition_count: usize,
197}
198
199#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
200pub struct RealitySnapshot {
201    pub identity: Identity,
202    pub boundary: Boundary,
203    pub law: Law,
204    pub state: State,
205    pub initial_state: State,
206    pub birth_boundary: Boundary,
207    pub birth_law: Law,
208    pub memory_hash: HashValue,
209    pub transition_count: usize,
210    pub fingerprint: RealityFingerprint,
211    pub integrity: IntegrityReport,
212}
213
214impl RealitySnapshot {
215    pub fn matches_current(&self, reality: &Reality) -> bool {
216        let diff = self.diff_against(reality);
217        diff.identity_same
218            && diff.boundary_same
219            && diff.law_same
220            && diff.state_same
221            && diff.initial_state_same
222            && diff.birth_boundary_same
223            && diff.birth_law_same
224            && diff.memory_hash_same
225            && diff.transition_count_same
226            && diff.fingerprint_same
227    }
228
229    pub fn diff_against(&self, reality: &Reality) -> RealityDiff {
230        RealityDiff {
231            identity_same: self.identity == reality.identity,
232            boundary_same: self.boundary == reality.boundary,
233            law_same: self.law == reality.law,
234            state_same: self.state == reality.state,
235            initial_state_same: self.initial_state == reality.initial_state,
236            birth_boundary_same: self.birth_boundary == reality.birth_boundary,
237            birth_law_same: self.birth_law == reality.birth_law,
238            memory_hash_same: self.memory_hash == reality.memory.current_hash(),
239            transition_count_same: self.transition_count == reality.memory.transitions.len(),
240            fingerprint_same: self.fingerprint == reality.fingerprint(),
241        }
242    }
243}
244
245impl Reality {
246    pub fn inspect(&self) -> Inspection {
247        Inspection {
248            initial_state: self.initial_state.clone(),
249            memory: self.memory.clone(),
250            current_state: self.state.clone(),
251        }
252    }
253    pub fn replay(&self) -> Replay {
254        if !self.memory.verify_integrity() {
255            return Replay {
256                replayed_state: self.initial_state.clone(),
257                passed: false,
258            };
259        }
260        let mut replayed_state = self.initial_state.clone();
261        for t in &self.memory.transitions {
262            if !t.law_check_valid {
263                return Replay {
264                    replayed_state,
265                    passed: false,
266                };
267            }
268            replayed_state = t.after.clone();
269        }
270        let passed = replayed_state == self.state;
271        Replay {
272            replayed_state,
273            passed,
274        }
275    }
276    pub fn continuity(&self) -> Continuity {
277        Continuity {
278            preserved: self.replay().passed,
279        }
280    }
281    pub fn memory_integrity(&self) -> bool {
282        self.memory.verify_integrity()
283    }
284    pub fn verify(&self) -> VerificationReport {
285        VerificationReport {
286            inspection: self.inspect(),
287            replay: self.replay(),
288            continuity: self.continuity(),
289            memory_integrity: self.memory_integrity(),
290        }
291    }
292    pub fn drift_check(&self) -> DriftCheck {
293        detect_drift(
294            &self.birth_boundary,
295            &self.birth_law,
296            &self.boundary,
297            &self.law,
298            self.replay().passed,
299        )
300    }
301    pub fn fingerprint(&self) -> RealityFingerprint {
302        let mut hasher = Sha256::new();
303        write_str(&mut hasher, &self.identity.0);
304        write_string_vec(&mut hasher, &self.birth_boundary.allowed_values);
305        write_transition_vec(&mut hasher, &self.birth_law.allowed_transitions);
306        write_str(&mut hasher, &self.state.field);
307        write_str(&mut hasher, &self.initial_state.field);
308        hasher.update(self.memory.current_hash().0);
309
310        let result = hasher.finalize();
311        let mut bytes = [0u8; 32];
312        bytes.copy_from_slice(&result);
313        RealityFingerprint(bytes)
314    }
315    pub fn integrity_report(&self) -> IntegrityReport {
316        IntegrityReport {
317            fingerprint: self.fingerprint(),
318            drift: self.drift_check(),
319            memory_integrity: self.memory_integrity(),
320            replay: self.replay(),
321            continuity: self.continuity(),
322            state: self.state().clone(),
323            transition_count: self.memory().transitions.len(),
324        }
325    }
326    pub fn would_accept(&self, event: &Event) -> bool {
327        if event.proposed_field.is_empty() {
328            return false;
329        }
330        if !self.boundary.allowed_values.contains(&self.state.field) {
331            return false;
332        }
333        self.law.check(&self.state, event)
334    }
335    pub fn diff(&self, other: &Reality) -> RealityDiff {
336        RealityDiff {
337            identity_same: self.identity == other.identity,
338            boundary_same: self.boundary == other.boundary,
339            law_same: self.law == other.law,
340            state_same: self.state == other.state,
341            initial_state_same: self.initial_state == other.initial_state,
342            birth_boundary_same: self.birth_boundary == other.birth_boundary,
343            birth_law_same: self.birth_law == other.birth_law,
344            memory_hash_same: self.memory.current_hash() == other.memory.current_hash(),
345            transition_count_same: self.memory.transitions.len() == other.memory.transitions.len(),
346            fingerprint_same: self.fingerprint() == other.fingerprint(),
347        }
348    }
349    pub fn preflight_sequence(&self, events: &[Event]) -> PreflightReport {
350        let mut clone = self.clone();
351        let mut results = Vec::with_capacity(events.len());
352        let mut accepted = 0usize;
353
354        for event in events {
355            if clone.would_accept(event) {
356                results.push(true);
357                let _ = crate::perform_movement(&mut clone, event.clone());
358                accepted += 1;
359            } else {
360                results.push(false);
361                return PreflightReport {
362                    results,
363                    sequence_lawful: false,
364                    final_state: None,
365                    transition_count: accepted,
366                };
367            }
368        }
369
370        PreflightReport {
371            results,
372            sequence_lawful: true,
373            final_state: Some(clone.state().clone()),
374            transition_count: accepted,
375        }
376    }
377    pub fn snapshot(&self) -> RealitySnapshot {
378        RealitySnapshot {
379            identity: self.identity.clone(),
380            boundary: self.boundary.clone(),
381            law: self.law.clone(),
382            state: self.state.clone(),
383            initial_state: self.initial_state.clone(),
384            birth_boundary: self.birth_boundary.clone(),
385            birth_law: self.birth_law.clone(),
386            memory_hash: self.memory.current_hash(),
387            transition_count: self.memory.transitions.len(),
388            fingerprint: self.fingerprint(),
389            integrity: self.integrity_report(),
390        }
391    }
392}
393
394pub fn plan_sequence(
395    reality: &Reality,
396    events: Vec<Event>,
397) -> Result<PlannedSequence, MovementError> {
398    let mut clone = reality.clone();
399    let proofs = crate::perform_movement_sequence(&mut clone, events)?;
400    Ok(PlannedSequence {
401        final_state: clone.state().clone(),
402        transition_count: clone.memory().transitions.len(),
403        proofs,
404    })
405}
406
407pub fn simulate_sequence(
408    reality: &Reality,
409    events: Vec<Event>,
410) -> Result<SimulationReport, MovementError> {
411    let mut clone = reality.clone();
412    let proofs = crate::perform_movement_sequence(&mut clone, events)?;
413
414    let planned = PlannedSequence {
415        final_state: clone.state().clone(),
416        transition_count: clone.memory().transitions.len(),
417        proofs,
418    };
419    let integrity = clone.integrity_report();
420    let composition = if !clone.memory().transitions.is_empty() {
421        clone
422            .memory()
423            .compose(0, clone.memory().transitions.len() - 1)
424    } else {
425        None
426    };
427    let fingerprint = clone.fingerprint();
428
429    Ok(SimulationReport {
430        planned,
431        integrity,
432        composition,
433        fingerprint,
434    })
435}
436
437#[cfg(test)]
438mod tests {
439    use super::*;
440
441    #[test]
442    fn detect_drift_no_change() {
443        let boundary = Boundary {
444            allowed_values: vec!["a".into(), "b".into()],
445        };
446        let law = Law {
447            allowed_transitions: vec![("a".to_string(), "b".to_string())],
448        };
449        let drift = detect_drift(&boundary, &law, &boundary, &law, true);
450        assert!(!drift.hidden_drift_required);
451    }
452
453    #[test]
454    fn detect_drift_boundary_change() {
455        let b1 = Boundary {
456            allowed_values: vec!["a".into(), "b".into()],
457        };
458        let b2 = Boundary {
459            allowed_values: vec!["a".into(), "b".into(), "c".into()],
460        };
461        let law = Law {
462            allowed_transitions: vec![("a".to_string(), "b".to_string())],
463        };
464        let drift = detect_drift(&b1, &law, &b2, &law, true);
465        assert!(drift.hidden_boundary_growth_detected);
466        assert!(drift.hidden_drift_required);
467    }
468
469    #[test]
470    fn detect_drift_law_change() {
471        let boundary = Boundary {
472            allowed_values: vec!["a".into(), "b".into()],
473        };
474        let law1 = Law {
475            allowed_transitions: vec![("a".to_string(), "b".to_string())],
476        };
477        let law2 = Law {
478            allowed_transitions: vec![
479                ("a".to_string(), "b".to_string()),
480                ("b".to_string(), "c".to_string()),
481            ],
482        };
483        let drift = detect_drift(&boundary, &law1, &boundary, &law2, true);
484        assert!(drift.hidden_law_growth_detected);
485        assert!(drift.permission_drift_detected);
486    }
487
488    #[test]
489    fn detect_drift_state_mutation() {
490        let boundary = Boundary {
491            allowed_values: vec!["a".into(), "b".into()],
492        };
493        let law = Law {
494            allowed_transitions: vec![("a".to_string(), "b".to_string())],
495        };
496        let drift = detect_drift(&boundary, &law, &boundary, &law, false);
497        assert!(drift.hidden_state_mutation_detected);
498    }
499}