fix(transactions): restrict the save's temp file from creation; never remove another writer's

PROOF-NEEDS.adoc

@@ -71,7 +71,7 @@ tables must agree.
 | T-2 | begin, add_operation, commit and mark_rolled_back each preserve the log invariant (given a fresh id for begin) and rewrite only the Active transaction, so a completed one is never modified | PROVEN | `+TransactionAtomicity.lifecycle-preserves-good+`; `+tests/reject-agda/CommitWhenIdle.agda+` refused
 | T-3 | At most one transaction is Active, and exactly one when the active pointer is set | PROVEN | `+TransactionAtomicity.at-most-one-active+`
 | T-4 | A rollback that fails part-way can be retried to completion | TESTED | `+rollback_resume_test+` drives the real `+jk+`: after one undo error and a repair, `+jk rollback+` skips the already undone operation and finishes (before the fix the retry stopped at it every time, reproduced 2026-10-26); fixed in `+cmd_rollback+`
-| T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by write, fsync and rename (a uniquely named temporary file, the old file's permissions kept) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort, because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins)
+| T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by write, fsync and rename (a randomly named temporary file opened with the old file's mode, removed only if this save created it) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort, because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins)
 | T-6 | A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1; single steps are TESTED by `+execute_then_undo_is_identity+`) | ASSUMED | not checked for the failure path
 | T-7 | Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) | ASSUMED | probabilistic, not checked
 | T-8 | The operation metadata log is saved atomically, and an undo whose `+mark_undone+` fails to persist can be retried | OPEN | by inspection: `+MetadataStore::save+` is the same plain `+fs::write+`; `+undo+` runs the undo, then `+mark_undone+` persists, so a failed persist leaves the file undone but the log not
@@ -197,6 +197,9 @@ the status table above.
 |T-5: A save replaces the log by rename, leaves no temporary file, and ignores a torn temporary file from an earlier crash |TESTED |`crates/reversible-core/src/transaction.rs::save_replaces_atomically_and_leaves_no_temporary_file` |`cargo test --locked -p reversible-core --lib save_replaces_atomically_and_leaves_no_temporary_file`
 |T-5: Two saves never share a temporary file, and the open refuses one that exists, so a writer cannot truncate, rename or delete another's |TESTED |`crates/reversible-core/src/transaction.rs::each_save_uses_its_own_temporary_file` |`cargo test --locked -p reversible-core --lib each_save_uses_its_own_temporary_file`
 |T-5: A save keeps the permissions of the log it replaces (rename would otherwise widen a 0640 log to the umask default) |TESTED |`crates/reversible-core/src/transaction.rs::save_preserves_the_logs_permissions` |`cargo test --locked -p reversible-core --lib save_preserves_the_logs_permissions`
+|T-5: A save whose temporary file already exists (another writer's) fails without deleting that file or writing the log |TESTED |`crates/reversible-core/src/transaction.rs::a_save_never_removes_a_temporary_file_it_did_not_create` |`cargo test --locked -p reversible-core --lib a_save_never_removes_a_temporary_file_it_did_not_create`
+|T-5: The temporary file has the log's permissions from creation, before any content is written |TESTED |`crates/reversible-core/src/transaction.rs::the_temporary_file_is_restricted_before_any_content_is_written` |`cargo test --locked -p reversible-core --lib the_temporary_file_is_restricted_before_any_content_is_written`
+|T-5: The temporary file is opened with the log's mode, so it is never more readable than the log at any instant, not only after a later chmod (checked where the umask leaves owner read-write, the usual 022) |TESTED |`crates/reversible-core/src/transaction.rs::the_temporary_file_is_opened_with_the_logs_mode` |`cargo test --locked -p reversible-core --lib the_temporary_file_is_opened_with_the_logs_mode`
 |G-2: The Idris2 IsCNO / ReversibleOp pair corresponds to the Agda ReversiblePair (by transcription) |ASSUMED |`verification/proofs/agda/Reversibility.agda` |-
 |X-1: Hash one-wayness and physical erasure (cryptographic and physical assumptions) |ASSUMED |`src/abi/JanusKey/ABI/Proofs.idr` |-
 |G-3: The FFI bridge preserves grade 𝟙 (a homomorphism; resource-algebra lists homomorphisms as OPEN) |OPEN |`verification/proofs/agda/Reversibility.agda` |-

READINESS.adoc

@@ -8,7 +8,7 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0
 
 === CRG Grade: D (Alpha — Unstable)
 
-*Justification:* 132 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the
+*Justification:* 135 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the
 Idris2 ABI typechecks and 11 proofs are checked (PROVEN ledger rows: ABI, grade and transaction-model lemmas, not the
 security obligations); benchmarks exist (5 Criterion groups). But: no
 fuzz testing, no mutation testing, 225 unwrap() calls, E2E mostly skips,
@@ -65,7 +65,7 @@ handling
 (run by idris-abi.yml, agda-proofs.yml and dashboard-check)
 |===
 
-*Total declared:* 132 tests + 5 benchmark groups; 11 proofs checked (PROVEN ledger rows) *Total
+*Total declared:* 135 tests + 5 benchmark groups; 11 proofs checked (PROVEN ledger rows) *Total
 missing:* Fuzz, mutation, chaos, compatibility
 
 === Aspect Matrix

TOPOLOGY.adoc

@@ -79,7 +79,7 @@ INTERFACES & RESEARCH
   MPR Methodology                   ████░░░░░░  ~40%   Design documented; FORMAL PROOFS PENDING
                                                         (Idris2 ABI typechecks; 11 proofs checked: ABI, grade and transaction-model
                                                         lemmas, not the security obligations; MPR not linked to the Rust)
-  Testing (READINESS matrix)        ██████░░░░  ~60%   132 tests + 5 benches; missing fuzz, mutation,
+  Testing (READINESS matrix)        ██████░░░░  ~60%   135 tests + 5 benches; missing fuzz, mutation,
                                                         chaos, compatibility (Grade D)
 
 REPO INFRASTRUCTURE

crates/reversible-core/src/transaction.rs

@@ -15,7 +15,6 @@ use serde::{Deserialize, Serialize};
 use std::fs;
 use std::io::Write;
 use std::path::{Path, PathBuf};
-use std::sync::atomic::{AtomicU64, Ordering};
 use uuid::Uuid;
 
 /// Transaction state
@@ -107,62 +106,85 @@ impl TransactionLog {
     }
 }
 
-/// Distinguishes the temporary files of saves made by one process.
-static SAVE_SEQ: AtomicU64 = AtomicU64::new(0);
-
-/// Build a sibling temporary pathname using the process ID and save sequence.
+/// Build a sibling temporary pathname that is unique to this save.
 ///
-/// Does not create or reserve the path; [`create_tmp`] checks for existing files.
+/// A random component, not a process id, so writers in different PID
+/// namespaces that share the repository cannot pick the same name. Does not
+/// create or reserve the path; [`create_tmp`] refuses one that exists.
 fn unique_tmp_path(path: &Path) -> PathBuf {
     let mut tmp = path.as_os_str().to_owned();
-    tmp.push(format!(
-        ".{}.{}.tmp",
-        std::process::id(),
-        SAVE_SEQ.fetch_add(1, Ordering::Relaxed)
-    ));
+    tmp.push(format!(".{}.tmp", Uuid::new_v4().simple()));
     PathBuf::from(tmp)
 }
 
-/// Create the temporary file, failing if it exists: never truncate or adopt a
-/// file another writer may be using.
+/// Open the temporary file, failing if it exists: never truncate or adopt a
+/// file another writer may be using. On Unix, if `like` exists the file is
+/// created with its mode (less whatever the umask clears), so at no instant is
+/// it more readable than `like`; a descriptor opened in some earlier window
+/// could otherwise outlive a later `chmod` and read the content written after.
+fn open_tmp(tmp: &Path, like: &Path) -> std::io::Result<fs::File> {
+    let mut options = fs::OpenOptions::new();
+    options.write(true).create_new(true);
+    #[cfg(unix)]
+    if let Ok(existing) = fs::metadata(like) {
+        use std::os::unix::fs::{OpenOptionsExt, PermissionsExt};
+        options.mode(existing.permissions().mode() & 0o7777);
+    }
+    #[cfg(not(unix))]
+    let _ = like;
+    options.open(tmp)
+}
+
+/// Create the temporary file with the permissions of `like`, exactly, before
+/// any content is written (see [`open_tmp`]).
 ///
 /// # Errors
 ///
-/// Returns an I/O error if the path already exists or the file cannot be created.
-fn create_tmp(tmp: &Path) -> std::io::Result<fs::File> {
-    fs::OpenOptions::new()
-        .write(true)
-        .create_new(true)
-        .open(tmp)
+/// Returns an I/O error if the path already exists, the file cannot be created
+/// or its permissions cannot be set. On a permissions error the file created
+/// here is removed.
+fn create_tmp(tmp: &Path, like: &Path) -> std::io::Result<fs::File> {
+    let file = open_tmp(tmp, like)?;
+    if let Ok(existing) = fs::metadata(like) {
+        if let Err(e) = file.set_permissions(existing.permissions()) {
+            let _ = fs::remove_file(tmp);
+            return Err(e);
+        }
+    }
+    Ok(file)
 }
 
 /// Replace `path` with `content` so a reader sees the old file or the new one,
 /// never a torn write: write a uniquely named sibling temporary file, flush it
-/// to disk, then rename it over `path`. Copies the existing file's permissions
-/// when its metadata can be read; otherwise keeps the new file's permissions.
+/// to disk, then rename it over `path`. The file keeps the permissions of the
+/// one it replaces, from the moment it is created.
 ///
 /// # Errors
 ///
-/// Returns temporary-file creation, write, permission-setting, sync or rename
-/// errors, attempting to remove the temporary file on failure. Metadata lookup,
-/// cleanup and parent-directory sync errors are ignored, so success does not
-/// guarantee the rename will survive a crash.
+/// Returns temporary-file creation, write, sync or rename errors. A temporary
+/// file this call created is removed on failure; one it did not create is left
+/// alone. Cleanup and parent-directory sync errors are ignored, so success does
+/// not guarantee the rename will survive a crash.
 fn write_atomic(path: &Path, content: &[u8]) -> std::io::Result<()> {
-    let tmp = unique_tmp_path(path);
+    write_atomic_via(path, &unique_tmp_path(path), content)
+}
+
+/// [`write_atomic`] with the temporary file named by the caller.
+fn write_atomic_via(path: &Path, tmp: &Path, content: &[u8]) -> std::io::Result<()> {
+    // If this fails the name may belong to another writer's live file, so
+    // nothing is removed: only a file created by this call is cleaned up.
+    let mut file = create_tmp(tmp, path)?;
 
     let written = (|| {
-        let mut file = create_tmp(&tmp)?;
         file.write_all(content)?;
-        if let Ok(existing) = fs::metadata(path) {
-            file.set_permissions(existing.permissions())?;
-        }
         file.sync_all()?;
-        fs::rename(&tmp, path)
+        drop(file);
+        fs::rename(tmp, path)
     })();
     if written.is_err() {
         // Best effort: nothing reads a stray temporary file, but there is no
         // reason to leave one behind.
-        let _ = fs::remove_file(&tmp);
+        let _ = fs::remove_file(tmp);
     }
     written?;
 
@@ -655,10 +677,69 @@ mod tests {
         let dir = TempDir::new().expect("failed to create temp dir");
         let taken = dir.path().join("taken.tmp");
         fs::write(&taken, b"another writer's bytes").expect("plant");
-        assert!(create_tmp(&taken).is_err());
+        assert!(create_tmp(&taken, &dir.path().join("transactions.json")).is_err());
         assert_eq!(fs::read(&taken).expect("read"), b"another writer's bytes");
     }
 
+    /// T-5: the temporary file is created with the log's mode at the `open`
+    /// itself, so a restricted log is never exposed through its copy even for
+    /// an instant. This sees the file before any permissions call. It tells the
+    /// two apart only when the umask leaves owner read-write (the usual 022).
+    #[cfg(unix)]
+    #[test]
+    fn the_temporary_file_is_opened_with_the_logs_mode() {
+        use std::os::unix::fs::PermissionsExt;
+
+        let dir = TempDir::new().expect("failed to create temp dir");
+        let path = dir.path().join("transactions.json");
+        fs::write(&path, b"{}").expect("existing log");
+        fs::set_permissions(&path, fs::Permissions::from_mode(0o600)).expect("chmod");
+
+        let file = open_tmp(&dir.path().join("transactions.json.new.tmp"), &path).expect("open");
+
+        let mode = file.metadata().expect("stat").permissions().mode() & 0o777;
+        assert_eq!(mode, 0o600, "owner-only from the open, before any chmod");
+    }
+
+    /// T-5: a save that cannot create its temporary file (the name is another
+    /// writer's live file) fails without deleting that file or touching the log.
+    #[test]
+    fn a_save_never_removes_a_temporary_file_it_did_not_create() {
+        let dir = TempDir::new().expect("failed to create temp dir");
+        let path = dir.path().join("transactions.json");
+        let theirs = dir.path().join("transactions.json.theirs.tmp");
+        fs::write(&theirs, b"another writer's bytes").expect("plant");
+
+        assert!(write_atomic_via(&path, &theirs, b"mine").is_err());
+
+        assert_eq!(
+            fs::read(&theirs).expect("their file survives"),
+            b"another writer's bytes"
+        );
+        assert!(!path.exists(), "the failed save wrote nothing");
+    }
+
+    /// T-5: the temporary file has the log's permissions the moment it exists,
+    /// before any content is written, so a restricted log is never exposed
+    /// through its copy.
+    #[cfg(unix)]
+    #[test]
+    fn the_temporary_file_is_restricted_before_any_content_is_written() {
+        use std::os::unix::fs::PermissionsExt;
+
+        let dir = TempDir::new().expect("failed to create temp dir");
+        let path = dir.path().join("transactions.json");
+        fs::write(&path, b"{}").expect("existing log");
+        fs::set_permissions(&path, fs::Permissions::from_mode(0o640)).expect("chmod");
+
+        let tmp = dir.path().join("transactions.json.new.tmp");
+        let file = create_tmp(&tmp, &path).expect("create");
+
+        let mode = file.metadata().expect("stat").permissions().mode() & 0o777;
+        assert_eq!(mode, 0o640, "restricted at creation");
+        assert_eq!(file.metadata().expect("stat").len(), 0, "and still empty");
+    }
+
     /// T-5: replacing the log by rename keeps the permissions of the log it
     /// replaces; an in-place write did, and a fresh file would silently widen them.
     #[cfg(unix)]