splice 2.6.3

Span-safe refactoring kernel for 7 languages with Magellan code graph integration
Documentation 
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

//! Proof-based refactoring support.
//!
//! This module provides machine-checkable behavioral equivalence proofs
//! for refactoring operations. A proof captures before/after graph state
//! and validates that structural invariants are preserved.

pub mod checksums;
pub mod comparison;
/// Data structures for proof snapshots and invariants.
pub mod data_structures;
pub mod generation;
pub mod storage;
pub mod validation;

pub use checksums::{
    compute_proof_checksums, compute_snapshot_hash, validate_proof_checksums, validate_proof_file,
};

pub use data_structures::{
    GraphSnapshot, GraphStats, InvariantCheck, InvariantViolation, ProofChecksums, ProofMetadata,
    RefactoringProof, SymbolInfo, ViolationSeverity,
};

pub use generation::{create_metadata, generate_snapshot, write_proof};

pub use storage::{RestoreResult, SnapshotMetadata, SnapshotStorage};

pub use validation::validate_invariants;

pub use comparison::{compare_snapshots, ChangeType, EdgeDiff, SnapshotDiff, SymbolDiff};

use crate::error::Result;
use std::path::Path;

/// Generate a proof for a refactoring operation.
///
/// This function should be called before and after a refactoring
/// to capture the graph state and validate invariants.
///
/// # Arguments
/// * `operation` - The type of refactoring operation (e.g., "rename", "delete")
/// * `db_path` - Path to the Magellan database
/// * `before_snapshot` - Graph state before the refactoring
/// * `after_snapshot` - Graph state after the refactoring
///
/// # Returns
/// A complete refactoring proof with invariant validation results and checksums.
///
/// # Examples
///
/// ```no_run
/// use splice::proof::{generate_proof, generate_snapshot};
/// use std::path::Path;
///
/// # fn main() -> splice::error::Result<()> {
/// let db_path = Path::new(".magellan/splice.db");
///
/// // Capture before state
/// let before = generate_snapshot(db_path)?;
///
/// // Perform refactoring...
///
/// // Capture after state
/// let after = generate_snapshot(db_path)?;
///
/// // Generate proof with checksums
/// let proof = generate_proof("rename", db_path, before, after)?;
///
/// // Validate invariants
/// for check in &proof.invariants {
///     if !check.passed {
///         eprintln!("Invariant violation: {}", check.invariant_name);
///         for violation in &check.violations {
///             eprintln!("  - {}: {}", violation.subject, violation.message);
///         }
///     }
/// }
///
/// // Write proof to file
/// let output_dir = Path::new(".splice/proofs/");
/// let proof_path = splice::proof::write_proof(&proof, output_dir)?;
/// println!("Proof written to: {}", proof_path.display());
///
/// // Later, validate the proof file
/// let is_valid = splice::proof::validate_proof_file(&proof_path)?;
/// assert!(is_valid, "Proof checksums are invalid!");
///
/// # Ok(())
/// # }
/// ```
pub fn generate_proof(
    operation: &str,
    db_path: &Path,
    before_snapshot: GraphSnapshot,
    after_snapshot: GraphSnapshot,
) -> Result<RefactoringProof> {
    // Validate invariants
    let invariants = validate_invariants(&before_snapshot, &after_snapshot)?;

    // Create metadata
    let metadata = create_metadata(operation, db_path);

    // Create proof without checksums first
    let mut proof = RefactoringProof {
        metadata,
        before: before_snapshot,
        after: after_snapshot,
        invariants,
        checksums: None,
    };

    // Compute and set checksums for audit trail integrity
    let checksums = compute_proof_checksums(&proof)?;
    proof.checksums = Some(checksums);

    Ok(proof)
}