Skip to content

Commit 55628e0

Browse files
feat(rust-cli): secure_delete + audit_log real impls + typed-error refactor + 15-25 prop-tests (#72)
- secure_delete (commands::secure_deletion::secure_delete) lifted to a public, documented primitive: 3-pass overwrite (urandom / zeros / 0xFF) with fsync between passes + unlink. Uses /dev/urandom on Unix, falls back to a hash-mixed PRNG elsewhere. CoW / FTL / snapshot limitations documented at the module-level rustdoc. - audit_log: added AuditLog::default_path() and AuditLog::with_default_path() honouring XDG_STATE_HOME / $HOME per the XDG Base Directory spec (XDG_STATE_HOME/valence-shell/audit.log or $HOME/.local/state/valence-shell/audit.log). - Replaced all six `unreachable!()` calls in src/commands.rs with typed `CommandError` (`#[non_exhaustive]`) variants — InternalUnreachableInverseArm, InternalUnreachableIrreversible, InternalUnreachableExplainPathArm — plus a contextual anyhow::bail! for the &str-returning hardware-erase dispatch. Future regressions in upstream filtering now surface as recoverable errors rather than aborting the shell. - Added impl/rust-cli/tests/secure_audit_prop_tests.rs with 20 property tests covering: - mkdir/rmdir reversibility (Lean: FilesystemModel.mkdir_rmdir_reversible) - touch/rm reversibility - writeFileReversible - copyFile_reversible - obliterate_not_injective (no inverse exists) - inverse round-trip well-formedness for all reversible OperationTypes - secure_delete unlink behaviour + EISDIR + ENOENT + edge sizes (0, 1) - audit-log append-only / order-preservation / filter-by-type - audit-entry JSON round-trip - XDG default-path resolution - Implemented the two security_tests.rs stubs (security_gdpr_secure_deletion, security_audit_trail_immutability) which previously held TODO markers. Echo-types audit: filesystem-reversibility properties exercised here are L3 (echo-layer) shape per the prior estate sweep. The implementation does not yet *import* echo-types directly — recorded as relevant-but-not-yet-imported per the cross-doc directive. Local verification: - cargo build --lib : clean - cargo test --workspace : 757 passed / 0 failed (the 21 test-binaries all return "0 failed", including the new 20 prop-tests and the 2 unstubbed security_tests). - cargo clippy --workspace --tests : pre-existing absurd_extreme_comparisons errors in confirmation.rs and e2e_script_execution.rs persist (verified against main via stash). Zero new clippy warnings on changed files. Closes the practice-gap #1 + #2 from #45. Refs #41 Phase 1, #43 prop-test expansion. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 9626ac1 commit 55628e0

5 files changed

Lines changed: 741 additions & 72 deletions

File tree

impl/rust-cli/src/audit_log.rs

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,41 @@ impl AuditLog {
135135
})
136136
}
137137

138+
/// Resolve the default audit-log path following the XDG Base Directory spec.
139+
///
140+
/// Search order:
141+
/// 1. `$XDG_STATE_HOME/valence-shell/audit.log` when `XDG_STATE_HOME` is set.
142+
/// 2. `$HOME/.local/state/valence-shell/audit.log` otherwise.
143+
/// 3. Errors if neither `XDG_STATE_HOME` nor `HOME` is set.
144+
///
145+
/// The directory is *not* created; that is deferred to [`AuditLog::new`].
146+
pub fn default_path() -> Result<PathBuf> {
147+
if let Ok(xdg) = std::env::var("XDG_STATE_HOME") {
148+
if !xdg.is_empty() {
149+
return Ok(PathBuf::from(xdg).join("valence-shell").join("audit.log"));
150+
}
151+
}
152+
if let Ok(home) = std::env::var("HOME") {
153+
if !home.is_empty() {
154+
return Ok(PathBuf::from(home)
155+
.join(".local")
156+
.join("state")
157+
.join("valence-shell")
158+
.join("audit.log"));
159+
}
160+
}
161+
anyhow::bail!(
162+
"Cannot determine default audit-log path: neither XDG_STATE_HOME nor HOME is set"
163+
);
164+
}
165+
166+
/// Open (or create) the audit log at the XDG-default location.
167+
///
168+
/// Convenience wrapper around [`AuditLog::default_path`] + [`AuditLog::new`].
169+
pub fn with_default_path(hmac_key: Option<Vec<u8>>) -> Result<Self> {
170+
Self::new(Self::default_path()?, hmac_key)
171+
}
172+
138173
/// Append audit entry to log
139174
///
140175
/// This is the core append-only operation. Failures are non-fatal
@@ -316,6 +351,36 @@ mod tests {
316351
assert_eq!(entries[1].path, "file1");
317352
}
318353

354+
#[test]
355+
fn test_default_path_uses_xdg_state_home_when_set() {
356+
// Snapshot env, set XDG_STATE_HOME, query, restore.
357+
// Use a process-unique key to keep parallel tests independent.
358+
let prev_xdg = std::env::var_os("XDG_STATE_HOME");
359+
let prev_home = std::env::var_os("HOME");
360+
// SAFETY: these env vars are read elsewhere in this crate only via
361+
// AuditLog::default_path; we restore before exiting the test.
362+
// Test runner is single-threaded for env mutations per-process; we
363+
// accept the parallel-test caveat documented at module level.
364+
unsafe {
365+
std::env::set_var("XDG_STATE_HOME", "/tmp/proptest-xdg-state");
366+
}
367+
let path = AuditLog::default_path().unwrap();
368+
assert_eq!(
369+
path,
370+
PathBuf::from("/tmp/proptest-xdg-state/valence-shell/audit.log")
371+
);
372+
unsafe {
373+
match prev_xdg {
374+
Some(v) => std::env::set_var("XDG_STATE_HOME", v),
375+
None => std::env::remove_var("XDG_STATE_HOME"),
376+
}
377+
match prev_home {
378+
Some(v) => std::env::set_var("HOME", v),
379+
None => std::env::remove_var("HOME"),
380+
}
381+
}
382+
}
383+
319384
#[test]
320385
fn test_audit_log_filter_by_type() {
321386
let temp_file = NamedTempFile::new().unwrap();

impl/rust-cli/src/commands.rs

Lines changed: 67 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
use anyhow::{Context, Result};
88
use colored::Colorize;
99
use std::fs;
10+
use thiserror::Error;
1011

1112
use crate::proof_refs;
1213
use crate::state::{Operation, OperationType, ShellState};
@@ -15,6 +16,39 @@ use crate::verification;
1516
// Secure deletion (RMO - Remove-Match-Obliterate)
1617
pub mod secure_deletion;
1718

19+
/// Typed errors raised by the command layer.
20+
///
21+
/// Previously several branches in the inverse/undo dispatch reached
22+
/// `unreachable!()` after upstream filters were supposed to exclude them.
23+
/// Those panics have been replaced with typed `CommandError::Internal*`
24+
/// variants so that any future regression in the filtering logic surfaces
25+
/// as a *recoverable* error rather than aborting the shell.
26+
#[derive(Debug, Error)]
27+
#[non_exhaustive]
28+
pub enum CommandError {
29+
/// An `OperationType` whose inverse is dispatched by an earlier match arm
30+
/// (e.g. `FileTruncated` → `WriteFile`, `CopyFile` → `DeleteFile`) reached
31+
/// a branch that should have been pre-handled.
32+
///
33+
/// Encountering this in the wild indicates a bug in
34+
/// [`OperationType::inverse`](crate::state::OperationType::inverse)
35+
/// or in the surrounding match dispatch.
36+
#[error("internal invariant violated: inverse-type arm reached for {op_type:?} which should have been handled by an earlier branch (expected WriteFile / DeleteFile)")]
37+
InternalUnreachableInverseArm { op_type: OperationType },
38+
39+
/// An irreversible operation (`Obliterate`, `HardwareErase`) reached the
40+
/// inverse dispatch despite `inverse()` returning `None` for these types.
41+
/// The filter at the top of `undo`/`rollback` is supposed to skip them.
42+
#[error("internal invariant violated: irreversible operation {op_type:?} reached inverse dispatch — `OperationType::inverse` should have returned None and the caller should have filtered")]
43+
InternalUnreachableIrreversible { op_type: OperationType },
44+
45+
/// `explain_command` extracted the path-bearing arm of a pattern that
46+
/// only contains `Chmod` or `Chown`, but the inner re-match observed a
47+
/// different variant.
48+
#[error("internal invariant violated: explain_command path-extraction reached a non-{{Chmod,Chown}} arm")]
49+
InternalUnreachableExplainPathArm,
50+
}
51+
1852
/// Create a directory at the specified path.
1953
///
2054
/// This operation is reversible via [`undo`] and corresponds to the Lean 4 theorem
@@ -949,12 +983,18 @@ pub fn undo(state: &mut ShellState, count: usize, verbose: bool) -> Result<()> {
949983
}
950984
OperationType::FileTruncated | OperationType::CopyFile => {
951985
// FileTruncated inverse is WriteFile, CopyFile inverse is DeleteFile
952-
// Both handled by earlier arms
953-
unreachable!("Inverse type should be WriteFile or DeleteFile, handled above");
986+
// Both handled by earlier arms — surface as typed error if reached.
987+
return Err(CommandError::InternalUnreachableInverseArm {
988+
op_type: inverse_type,
989+
}
990+
.into());
954991
}
955992
OperationType::HardwareErase | OperationType::Obliterate => {
956-
// These have no inverse (inverse() returns None), so we never get here
957-
unreachable!("Irreversible operations filtered out above");
993+
// These have no inverse (inverse() returns None), so we never get here.
994+
return Err(CommandError::InternalUnreachableIrreversible {
995+
op_type: inverse_type,
996+
}
997+
.into());
958998
}
959999
}
9601000

@@ -1435,12 +1475,18 @@ pub fn rollback_transaction(state: &mut ShellState) -> Result<()> {
14351475
}
14361476
OperationType::FileTruncated | OperationType::CopyFile => {
14371477
// FileTruncated inverse is WriteFile, CopyFile inverse is DeleteFile
1438-
// Both handled by earlier arms
1439-
unreachable!("Inverse type should be WriteFile or DeleteFile, handled above");
1478+
// Both handled by earlier arms — return typed error instead of panicking.
1479+
Err(CommandError::InternalUnreachableInverseArm {
1480+
op_type: inverse_type,
1481+
}
1482+
.into())
14401483
}
14411484
OperationType::HardwareErase | OperationType::Obliterate => {
1442-
// This should never happen - these have no inverse (inverse() returns None)
1443-
unreachable!("Irreversible operations should not reach here");
1485+
// These have no inverse (inverse() returns None), so we never get here.
1486+
Err(CommandError::InternalUnreachableIrreversible {
1487+
op_type: inverse_type,
1488+
}
1489+
.into())
14441490
}
14451491
};
14461492

@@ -1952,7 +1998,15 @@ pub fn hardware_erase(
19521998
println!("{}", "✓ Device securely erased".bright_green().bold());
19531999
}
19542000

1955-
_ => unreachable!(),
2001+
other => {
2002+
// The earlier `match (drive_type, method)` block can only emit one of
2003+
// "ata-secure-erase" / "nvme-format" / "nvme-sanitize"; reaching this
2004+
// arm means that block grew a new method without updating us.
2005+
anyhow::bail!(
2006+
"internal invariant violated: erase_method dispatch received unrecognised value '{}'",
2007+
other
2008+
);
2009+
}
19562010
}
19572011

19582012
// Record operation (NOT reversible)
@@ -2074,10 +2128,13 @@ pub fn explain_command(cmd: &crate::parser::Command, state: &ShellState) -> Resu
20742128
);
20752129
}
20762130
crate::parser::Command::Chmod { path, .. } | crate::parser::Command::Chown { path, .. } => {
2131+
// Outer arm guarantees we are in {Chmod, Chown}; the inner match
2132+
// exists only to extract the `path` field uniformly. Any other
2133+
// variant here is a structural bug, surfaced as typed error.
20772134
let p = match cmd {
20782135
crate::parser::Command::Chmod { path, .. } => path,
20792136
crate::parser::Command::Chown { path, .. } => path,
2080-
_ => unreachable!(),
2137+
_ => return Err(CommandError::InternalUnreachableExplainPathArm.into()),
20812138
};
20822139
let expanded = crate::parser::expand_variables(p, state);
20832140
let resolved = state.resolve_path(&expanded);

0 commit comments

Comments
 (0)