|
6 | 6 |
|
7 | 7 | use januskey::content_store::ContentStore; |
8 | 8 | use januskey::obliteration::{ObliterationManager, ObliterationProof}; |
| 9 | +use januskey::operations::{FileOperation, OperationExecutor}; |
9 | 10 | use proptest::prelude::*; |
10 | 11 | use reversible_core::content_store::ContentHash; |
| 12 | +use reversible_core::metadata::MetadataStore; |
| 13 | +use std::collections::BTreeMap; |
| 14 | +use std::path::{Path, PathBuf}; |
11 | 15 | use tempfile::TempDir; |
12 | 16 |
|
13 | 17 | // --- Obliteration properties --- |
@@ -54,3 +58,107 @@ proptest! { |
54 | 58 | prop_assert_eq!(h1, h2); |
55 | 59 | } |
56 | 60 | } |
| 61 | + |
| 62 | +// --- CNO round-trip law: execute ∘ undo ≡ identity on the filesystem --- |
| 63 | +// |
| 64 | +// This is the load-bearing, runnable evidence for JanusKey's reversibility |
| 65 | +// claim (the honest substitute for the "formal proofs pending" badge): for |
| 66 | +// every supported operation, executing it and then undoing it must return the |
| 67 | +// working tree to exactly its pre-execute state (bytes + existence). |
| 68 | +// |
| 69 | +// Chown is excluded: its undo is unimplemented (operations.rs). We test the |
| 70 | +// filesystem effect, not OperationType::inverse() (which is deliberately NOT an |
| 71 | +// involution — Copy⁻¹ = Delete — so double-inverse is not the law here). |
| 72 | + |
| 73 | +/// What operation to exercise, plus the content it needs. |
| 74 | +#[derive(Debug, Clone)] |
| 75 | +enum OpSpec { |
| 76 | + Delete(Vec<u8>), |
| 77 | + Modify(Vec<u8>, Vec<u8>), |
| 78 | + Move(Vec<u8>), |
| 79 | + Copy(Vec<u8>), |
| 80 | + Create(Vec<u8>), |
| 81 | +} |
| 82 | + |
| 83 | +fn op_strategy() -> impl Strategy<Value = OpSpec> { |
| 84 | + let bytes = || proptest::collection::vec(any::<u8>(), 0..256); |
| 85 | + prop_oneof![ |
| 86 | + bytes().prop_map(OpSpec::Delete), |
| 87 | + (bytes(), bytes()).prop_map(|(a, b)| OpSpec::Modify(a, b)), |
| 88 | + bytes().prop_map(OpSpec::Move), |
| 89 | + bytes().prop_map(OpSpec::Copy), |
| 90 | + bytes().prop_map(OpSpec::Create), |
| 91 | + ] |
| 92 | +} |
| 93 | + |
| 94 | +/// Recursive {relative-path -> bytes} snapshot of a directory (no external deps). |
| 95 | +fn snapshot(dir: &Path, base: &Path, out: &mut BTreeMap<PathBuf, Vec<u8>>) { |
| 96 | + for entry in std::fs::read_dir(dir).unwrap() { |
| 97 | + let path = entry.unwrap().path(); |
| 98 | + if path.is_dir() { |
| 99 | + snapshot(&path, base, out); |
| 100 | + } else { |
| 101 | + let rel = path.strip_prefix(base).unwrap().to_path_buf(); |
| 102 | + out.insert(rel, std::fs::read(&path).unwrap()); |
| 103 | + } |
| 104 | + } |
| 105 | +} |
| 106 | + |
| 107 | +fn snapshot_of(work: &Path) -> BTreeMap<PathBuf, Vec<u8>> { |
| 108 | + let mut out = BTreeMap::new(); |
| 109 | + snapshot(work, work, &mut out); |
| 110 | + out |
| 111 | +} |
| 112 | + |
| 113 | +proptest! { |
| 114 | + /// execute(op) then undo restores the working tree exactly (the CNO law). |
| 115 | + #[test] |
| 116 | + fn execute_then_undo_is_identity(spec in op_strategy()) { |
| 117 | + let tmp = TempDir::new().unwrap(); |
| 118 | + // Keep user files (snapshotted) separate from the store internals. |
| 119 | + let work = tmp.path().join("work"); |
| 120 | + std::fs::create_dir_all(&work).unwrap(); |
| 121 | + let content_store = ContentStore::new(tmp.path().join("content"), false).unwrap(); |
| 122 | + let mut metadata_store = |
| 123 | + MetadataStore::new(tmp.path().join("metadata.json")).unwrap(); |
| 124 | + |
| 125 | + let a = work.join("a.bin"); |
| 126 | + let b = work.join("b.bin"); |
| 127 | + |
| 128 | + // Establish the pre-state and choose the operation. |
| 129 | + let op = match &spec { |
| 130 | + OpSpec::Delete(c) => { |
| 131 | + std::fs::write(&a, c).unwrap(); |
| 132 | + FileOperation::Delete { path: a.clone() } |
| 133 | + } |
| 134 | + OpSpec::Modify(orig, new) => { |
| 135 | + std::fs::write(&a, orig).unwrap(); |
| 136 | + FileOperation::Modify { path: a.clone(), new_content: new.clone() } |
| 137 | + } |
| 138 | + OpSpec::Move(c) => { |
| 139 | + std::fs::write(&a, c).unwrap(); |
| 140 | + FileOperation::Move { source: a.clone(), destination: b.clone() } |
| 141 | + } |
| 142 | + OpSpec::Copy(c) => { |
| 143 | + std::fs::write(&a, c).unwrap(); |
| 144 | + FileOperation::Copy { source: a.clone(), destination: b.clone() } |
| 145 | + } |
| 146 | + OpSpec::Create(c) => { |
| 147 | + FileOperation::Create { path: a.clone(), content: c.clone() } |
| 148 | + } |
| 149 | + }; |
| 150 | + |
| 151 | + let before = snapshot_of(&work); |
| 152 | + |
| 153 | + // execute — mutates the tree and records inversion metadata. |
| 154 | + let mut exec = OperationExecutor::new(&content_store, &mut metadata_store); |
| 155 | + let meta = exec.execute(op).unwrap(); |
| 156 | + |
| 157 | + // undo — a fresh executor, exactly as the CLI unlocks a later session. |
| 158 | + let mut exec2 = OperationExecutor::new(&content_store, &mut metadata_store); |
| 159 | + exec2.undo(&meta.id).unwrap(); |
| 160 | + |
| 161 | + let after = snapshot_of(&work); |
| 162 | + prop_assert_eq!(before, after, "execute∘undo must restore the tree (CNO law)"); |
| 163 | + } |
| 164 | +} |
0 commit comments