Skip to content

feat(rust-cli): secure_delete + audit_log real impls + typed-error refactor + 15-25 prop-tests#72

Merged
hyperpolymath merged 1 commit into
mainfrom
feat/secure-delete-audit-log-impls
Jun 1, 2026
Merged

feat(rust-cli): secure_delete + audit_log real impls + typed-error refactor + 15-25 prop-tests#72
hyperpolymath merged 1 commit into
mainfrom
feat/secure-delete-audit-log-impls

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Closes the practice-gap #1 + #2 from #45. Refs #41 Phase 1, #43 prop-test expansion.

Three things in one PR (~740 LoC added across 5 files — under the split threshold, kept atomic):

Task 1 — secure_delete + audit_log real impls

  • commands::secure_deletion::secure_delete lifted from a private helper to a documented public primitive: 3-pass NIST SP 800-88 Purge-style overwrite (random / zeros / 0xFF), fsync between passes, then unlink. Random bytes drawn from /dev/urandom on Unix (hash-mixed PRNG fallback elsewhere).
  • Filesystem-limitation doc: CoW filesystems (btrfs, ZFS, APFS), log-structured FSes (f2fs, NILFS2), SSDs with FTL remapping, snapshots, and network FSes can all defeat in-place overwrite. Documented at the module-level rustdoc; hardware NIST SP 800-88 Purge via secure_erase is the suggested escalation.
  • AuditLog::default_path() + AuditLog::with_default_path() added, honouring XDG Base Directory: \$XDG_STATE_HOME/valence-shell/audit.log\$HOME/.local/state/valence-shell/audit.log fallback. The existing append-only JSONL writer (already wired with serde_json + chrono + uuid + fsync-per-append) is what the new helpers route into.

Task 2 — unreachable!() → typed errors

All six unreachable!() sites in src/commands.rs replaced with a new CommandError enum (#[non_exhaustive]):

  • InternalUnreachableInverseArm { op_type } — two sites where the inverse-type dispatch reaches an arm whose handling lives in an earlier branch (FileTruncatedWriteFile, CopyFileDeleteFile).
  • InternalUnreachableIrreversible { op_type } — two sites where filter logic for Obliterate/HardwareErase (whose inverse() returns None) is supposed to skip them.
  • InternalUnreachableExplainPathArmexplain_command extracting path from a {Chmod, Chown} outer arm.
  • The hardware-erase &str dispatch reaches a contextual anyhow::bail! describing which sentinel was unexpected.

Regressions in upstream filtering now surface as recoverable errors rather than aborting the shell.

Task 3 — 20 property-correspondence tests

New impl/rust-cli/tests/secure_audit_prop_tests.rs:

Group A — Filesystem reversibility (L3 echo-layer shape)

  • mkdir_rmdir_reversible (Lean: FilesystemModel.mkdir_rmdir_reversible)
  • mkdir_distinct_paths_both_exist
  • touch_rm_reversible
  • writefile_reversible
  • copyfile_reversible
  • mkdir_preserves_other_paths
  • mkdir_rmdir_mkdir_equals_mkdir

Group B — Irreversibility

  • obliterate_has_no_inverse (and HardwareErase)
  • inverse_round_trip_for_reversible — for every reversible OperationType, inverse(inverse(t)) is itself reversible
  • secure_delete_removes_file
  • secure_delete_refuses_directories (EISDIR)
  • secure_delete_refuses_missing (ENOENT)
  • secure_delete_handles_tiny_files (1-byte edge of chunked loop)
  • secure_delete_handles_empty_files (0-byte edge)

Group C — Audit-log append-only

  • audit_log_append_only (every successful append increments by 1)
  • audit_log_preserves_order
  • audit_log_filter_by_type
  • audit_log_records_errors
  • audit_entry_json_roundtrip

Group D — XDG default-path resolution (single sanity test)

Plus the two pre-existing TODO-marked security_tests.rs stubs (security_gdpr_secure_deletion, security_audit_trail_immutability) now have real bodies routed through the new public APIs.

Echo-types audit

The filesystem-reversibility properties exercised here are L3 (echo-layer) shape per the prior estate sweep finding. The implementation does not yet import echo-types directly — recorded as relevant-but-not-yet-imported per the cross-doc directive. A later echo-layer integration can lift these property statements one-for-one into the echo carriers.

Test plan

  • cargo build --lib — clean
  • cargo test --workspace757 passed / 0 failed (21 test binaries, all 0 failed; includes the new 20 prop-tests and the 2 unstubbed security_tests)
  • cargo clippy --workspace --tests — zero new warnings on changed files. The 2 pre-existing absurd_extreme_comparisons errors in src/confirmation.rs and tests/e2e_script_execution.rs were verified against main via stash; not introduced by this PR.
  • GPG-signed commit (key 4A03639C1EB1F86C7F0C97A91835A14A2867091E)
  • Doctest compilation green for all changed docstrings

🤖 Generated with Claude Code

…factor + 15-25 prop-tests

- 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>
@hyperpolymath hyperpolymath enabled auto-merge (squash) June 1, 2026 18:54
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Jun 1, 2026

🔍 Hypatia Security Scan

Findings: 133 issues detected

Severity Count
🔴 Critical 10
🟠 High 23
🟡 Medium 100

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "lean-verification.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "rust-cli.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in compilation_tests.yml",
    "type": "missing_timeout_minutes",
    "file": "compilation_tests.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath merged commit 55628e0 into main Jun 1, 2026
28 of 59 checks passed
@hyperpolymath hyperpolymath deleted the feat/secure-delete-audit-log-impls branch June 1, 2026 18:56
hyperpolymath added a commit that referenced this pull request Jun 1, 2026
The Rust CLI Tests workflow runs `cargo fmt --check` and was failing on
the bench files (`benches/operation_benchmarks.rs`, `benches/performance_benchmarks.rs`)
plus accumulated format drift across 42 other files in the crate. The
workflow's path filter (`impl/rust-cli/**`) means main pushes that don't
touch those paths skip the job, so the drift went unnoticed until PR #72
exercised the workflow.

Running `cargo fmt` once across the whole crate to clear the backlog.
Pure whitespace + reordering of use-imports; no semantic change. Future
PRs touching `impl/rust-cli/` will hit fmt-check on a clean base.
hyperpolymath added a commit that referenced this pull request Jun 2, 2026
After PRs #105 / #106 / #108 / #109 admin-merged closing #60 / #61 /
#70 / #89, several files held stale claims:

- PROOF-NEEDS.md: Idris2 listed "23 holes + 8 partial across 4 files"
  pre-#108/#109 — partial count is now 0 (10 dropped: 2 in RMO from
  IO-totality reclassification, 8 in Composition from primitive-call
  refactor). Coq admit detail rewritten: the single_op_reversible
  OpRmdir admit was Qed-closed by PR #67 (2026-06-01); 3 new admits
  surfaced from PR #55's design-gap pass tracked as #56/#57/#58.

- proofs/idris2/README.md: 21 holes -> 23 holes; "Known oracle status
  2026-06-01" -> 2026-06-02, with partial-count reference corrected.

- ROADMAP.adoc: last-refreshed bumped + post-merge attribution.

- CHANGELOG.adoc: new "Added -- 2026-06-02" section recording the
  Idris2 cleanup wave + branch sweep + #111 salvage decision.

- .machine_readable/6a2/STATE.a2ml: last-updated 2026-04-19 -> 2026-06-02
  (6-week drift); admitted 1 -> 3 with per-admit detail (#56/#57/#58);
  session-history bullets added for 2026-06-01 + 2026-06-02.

- 0-AI-MANIFEST.a2ml: last-updated bumped; tests 736 -> 757 (PR #72);
  proof-holes-remaining split into coq-admits + idris2 totals.

Issue #111 filed during the sweep for `.github/copilot/coding-agent.yml`
salvaged from the deleted `claude/safedom-res-stale-sweep` branch.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant