feat(core): the API and the isolation of the bound removal, test-support only (#445)

Merged
QN
3d ago
+701-3

Part of #359 (R-15 Gate 4, slice H1a-2), part 1 of 4. Admitted by the maintainer on 2026-10-15 for test-support only: no production caller, no production deletion release. Builds on the merged seam of #1067.

The first draft was one PR of 2,172 meaningful lines (over the 1,200 hard-advisory tier; the green size job was not a licence). It is cut along proof boundaries into four stacked PRs, each with the tests of its own behaviour; the full draft is preserved locally and its commit stays in this branch's history.

PartContentPrerequisite
1 (this PR)API + isolation proofs + contract; every removal answers Unsupportedmain
2Unix file removal (quarantine, identification of the open object, unlink, rollback, Stranded, Disturbed)1
3Unix directory removal, leftover recovery, crash cases2
4Windows delete handle (relative lookup, read-only sharing, POSIX disposition on the handle)3

What this PR adds

PinnedDir::{remove_authenticated_file, remove_empty_dir, remove_leftover_file}, RemovalOutcome, RemovalStage, Observer, QUARANTINE_PREFIX behind the test-only test-support feature; PinnedDir::sync (no deletion) in every build. No new unsafe, no new dependency feature, Cargo.lock untouched.

  • feature_isolation_removal_test: scan of the sources (the modules are declared under the gate on every platform, nothing else names the primitives, no other removal module), with a scan that proves it sees an ungated declaration and export.
  • feature_isolation_compile_test: the crate is built the way a dependent gets it and with the feature; a small crate calling a removal method / importing RemovalOutcome fails with E0599 / E0432 against the first and compiles against the second; a control compiles against both (~100 s, own target dir).

The contract's limit, to be decided before H1b

No Unix primitive unlinks "this inode". The quarantine directory is not exclusive (mode 0700 and a random name do not stop the same user), so between the last identification and the unlink an actor that wins one race can have its own object removed instead. That is detected after the fact, not prevented (Disturbed, a heuristic by link count) and never counted as a success. "The same user could delete it anyway" is a threat-model statement, not an identity guarantee; whether the residual is acceptable for a production sweep is for the maintainer to decide before H1b. Part 2 forces the window in a test and pins the outcome.

Review findings of the first draft

The 12 threads on the first draft concern the Unix removal and move with it to parts 2 and 3 (rollback after a failed inspection, a restrictive umask, directory verification, strict leftover-name grammar, sync after a put-back, the honesty of the link-count check, the CodeScene argument counts); each is answered on its thread with the commit that fixes it once that part is pushed.

Status: H1A_2_REMOVAL=API_AND_ISOLATION_ONLY, H1_PROVED=NO, R1_PRODUCTION_RECLAMATION=NOT_ADMITTED, GATE4_TERMINAL=NO.