Verify native behavior creation recovery and source authoring contracts

harness/behavior-creation-contract.rs

@@ -1,5 +1,5 @@
 //! Independent native creation oracle; no desktop producer is imported.
-//! self-check BASE | check STAGE BASE ACTUAL ROLES | same EXPECTED ACTUAL
+//! self-check BASE | check STAGE BASE ACTUAL ROLES | same EXPECTED ACTUAL [UNDO_FROM]
 use oa_core::{source_project::*, *};
 use std::{
     collections::{BTreeMap, BTreeSet},
@@ -41,7 +41,9 @@ impl Stage {
     }
 }
 
-fn source_paths(root: &Path, here: &Path, paths: &mut BTreeSet<String>) {
+type DiskSources = BTreeMap<String, Vec<u8>>;
+
+fn source_paths(root: &Path, here: &Path, paths: &mut DiskSources) {
     for entry in fs::read_dir(here).unwrap() {
         let entry = entry.unwrap();
         let kind = entry.file_type().unwrap();
@@ -61,11 +63,12 @@ fn source_paths(root: &Path, here: &Path, paths: &mut BTreeSet<String>) {
                     .to_str()
                     .unwrap()
                     .replace('\\', "/"),
+                fs::read(entry.path()).unwrap(),
             );
         }
     }
 }
-fn load(entry: &Path) -> CompiledSourceProject {
+fn load_checkpoint(entry: &Path) -> (CompiledSourceProject, DiskSources) {
     let files = source_files::load_project(entry, ProjectLimits::default()).unwrap();
     let raw = files.reachable_bundle();
     let compiled = compile_bundle(&raw, ProjectLimits::default()).unwrap();
@@ -74,13 +77,30 @@ fn load(entry: &Path) -> CompiledSourceProject {
         "No migration, normalization or implicit identity insertion"
     );
     execute_batch(&compiled.decoded.project, &[]).unwrap();
-    let mut disk = BTreeSet::new();
+    let mut disk = BTreeMap::new();
     let root = entry.parent().unwrap();
     source_paths(root, root, &mut disk);
+    (compiled, disk)
+}
+fn predicted_disk(reachable: &SourceBundle, undo_from: Option<&DiskSources>) -> DiskSources {
+    // Saving Undo writes the restored reachable files and deliberately keeps
+    // detached files from the previously saved checkpoint. Never infer their
+    // bytes from the actual Undo directory: its explicit origin is the oracle.
+    let mut expected = undo_from.cloned().unwrap_or_default();
+    expected.extend(
+        reachable
+            .files
+            .iter()
+            .map(|(path, source)| (path.clone(), source.as_bytes().to_vec())),
+    );
+    expected
+}
+fn load(entry: &Path) -> CompiledSourceProject {
+    let (compiled, disk) = load_checkpoint(entry);
     assert_eq!(
         disk,
-        raw.files.keys().cloned().collect(),
-        "Reject detached extra source files too"
+        predicted_disk(&compiled.bundle, None),
+        "Ordinary checkpoints must contain exactly their reachable source files; retained Undo files require an explicit origin"
     );
     compiled
 }
@@ -526,6 +546,76 @@ fn self_check(base: &CompiledSourceProject) {
         "Reject an altered baseline before use"
     );
     assert_equal(&original, base);
+    let before = predict(base, Stage::Scenario, &carrier);
+    let created = predict(base, Stage::Machine, &carrier);
+    let origin = predicted_disk(&created.bundle, None);
+    let detached: Vec<_> = created
+        .bundle
+        .files
+        .keys()
+        .filter(|path| !before.bundle.files.contains_key(*path))
+        .cloned()
+        .collect();
+    assert_eq!(
+        detached.len(),
+        1,
+        "A machine creation adds one source module"
+    );
+    // Independently simulate the saver's observable result: restored reachable
+    // bytes plus the one new module left on disk by the prior creation.
+    let mut retained = predicted_disk(&before.bundle, None);
+    retained.insert(
+        detached[0].clone(),
+        created.bundle.files[&detached[0]].as_bytes().to_vec(),
+    );
+    assert_eq!(
+        retained[&detached[0]], origin[&detached[0]],
+        "Retained bytes must come from the exact created checkpoint"
+    );
+    assert_ne!(
+        retained,
+        predicted_disk(&before.bundle, None),
+        "Ordinary comparison must not accept detached history files"
+    );
+    assert_eq!(
+        retained,
+        predicted_disk(&before.bundle, Some(&origin)),
+        "Explicit Undo origin permits only the expected retained bytes"
+    );
+    let mut unknown = retained.clone();
+    unknown.insert("unknown.arcadia".into(), b"// Unclaimed file\n".to_vec());
+    assert_ne!(
+        unknown,
+        predicted_disk(&before.bundle, Some(&origin)),
+        "Reject unknown detached files"
+    );
+    let mut changed = retained.clone();
+    changed.get_mut(&detached[0]).unwrap().push(b' ');
+    assert_ne!(
+        changed,
+        predicted_disk(&before.bundle, Some(&origin)),
+        "Reject changed detached bytes"
+    );
+    let mut missing = retained.clone();
+    missing.remove(&detached[0]);
+    assert_ne!(
+        missing,
+        predicted_disk(&before.bundle, Some(&origin)),
+        "The retained file set is exact, not optional"
+    );
+    let mut reachable_drift = retained.clone();
+    reachable_drift
+        .get_mut("rationale.arcadia")
+        .unwrap()
+        .push(b' ');
+    assert_ne!(
+        reachable_drift,
+        predicted_disk(&before.bundle, Some(&origin)),
+        "An Undo exemption cannot hide reachable-source changes"
+    );
+    println!(
+        "PASS explicit Undo disk contract: known detached retention accepted; unknown, changed, missing and reachable drift rejected"
+    );
     println!("PASS baseline retained unchanged; no native acceptance claimed");
 }
 fn main() {
@@ -554,15 +644,33 @@ fn main() {
             );
         }
         Some("same") => {
-            assert_eq!(args.len(), 4, "same EXPECTED_CHECKPOINT ACTUAL_CHECKPOINT");
+            assert!(
+                matches!(args.len(), 4 | 5),
+                "same EXPECTED_CHECKPOINT ACTUAL_CHECKPOINT [UNDO_FROM_CHECKPOINT]"
+            );
             let expected = load(Path::new(&args[2]));
-            let actual = load(Path::new(&args[3]));
+            let (actual, disk) = load_checkpoint(Path::new(&args[3]));
             assert_equal(&expected, &actual);
+            let origin = args.get(4).map(|entry| {
+                // The first committed checkpoint is itself exact. This keeps
+                // arbitrary pre-existing detached files out of the exception.
+                let committed = load(Path::new(entry));
+                predicted_disk(&committed.bundle, None)
+            });
+            assert_eq!(
+                disk,
+                predicted_disk(&expected.bundle, origin.as_ref()),
+                "Disk source files differ from the exact checkpoint plus explicitly proven retained Undo files"
+            );
             println!(
-                "PASS exact checkpoint identity/model/{}-file SourceBundle equality",
-                actual.bundle.files.len()
+                "PASS exact checkpoint identity/model/{}-file SourceBundle equality; {} exact disk files ({} known retained)",
+                actual.bundle.files.len(),
+                disk.len(),
+                disk.len() - actual.bundle.files.len()
             );
         }
-        _ => panic!("self-check BASE | check STAGE BASE ACTUAL ROLES | same EXPECTED ACTUAL"),
+        _ => panic!(
+            "self-check BASE | check STAGE BASE ACTUAL ROLES | same EXPECTED ACTUAL [UNDO_FROM]"
+        ),
     }
 }