feat(rust-cli): secure_delete + audit_log real impls + typed-error refactor + 15-25 prop-tests#72
Merged
Conversation
…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>
🔍 Hypatia Security ScanFindings: 133 issues detected
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 |
3 tasks
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.
This was referenced Jun 1, 2026
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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_logreal implscommands::secure_deletion::secure_deletelifted from a private helper to a documented public primitive: 3-pass NIST SP 800-88 Purge-style overwrite (random / zeros /0xFF),fsyncbetween passes, thenunlink. Random bytes drawn from/dev/urandomon Unix (hash-mixed PRNG fallback elsewhere).secure_eraseis 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.logfallback. The existing append-only JSONL writer (already wired withserde_json+chrono+uuid+fsync-per-append) is what the new helpers route into.Task 2 —
unreachable!()→ typed errorsAll six
unreachable!()sites insrc/commands.rsreplaced with a newCommandErrorenum (#[non_exhaustive]):InternalUnreachableInverseArm { op_type }— two sites where the inverse-type dispatch reaches an arm whose handling lives in an earlier branch (FileTruncated→WriteFile,CopyFile→DeleteFile).InternalUnreachableIrreversible { op_type }— two sites where filter logic forObliterate/HardwareErase(whoseinverse()returnsNone) is supposed to skip them.InternalUnreachableExplainPathArm—explain_commandextracting path from a{Chmod, Chown}outer arm.&strdispatch reaches a contextualanyhow::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_existtouch_rm_reversiblewritefile_reversiblecopyfile_reversiblemkdir_preserves_other_pathsmkdir_rmdir_mkdir_equals_mkdirGroup B — Irreversibility
obliterate_has_no_inverse(andHardwareErase)inverse_round_trip_for_reversible— for every reversibleOperationType,inverse(inverse(t))is itself reversiblesecure_delete_removes_filesecure_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_orderaudit_log_filter_by_typeaudit_log_records_errorsaudit_entry_json_roundtripGroup D — XDG default-path resolution (single sanity test)
Plus the two pre-existing
TODO-markedsecurity_tests.rsstubs (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-typesdirectly — 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— cleancargo test --workspace— 757 passed / 0 failed (21 test binaries, all0 failed; includes the new 20 prop-tests and the 2 unstubbedsecurity_tests)cargo clippy --workspace --tests— zero new warnings on changed files. The 2 pre-existingabsurd_extreme_comparisonserrors insrc/confirmation.rsandtests/e2e_script_execution.rswere verified againstmainvia stash; not introduced by this PR.4A03639C1EB1F86C7F0C97A91835A14A2867091E)🤖 Generated with Claude Code