Luigit
repositories / termux-janitor

termux-janitor

Interactive cleanup assistant for Termux: transparent, safe, confirmed disk reclamation.

owned by admin

spec/EXPERIMENTAL_EVIDENCE.md

Raw
Rendered preview

Experimental evidence

This index connects platform observations to normative requirements. An experiment supports only the stated conclusion on the recorded environment. It does not replace deterministic product tests or extend a claim beyond its observed scope.

Evidence rules

  • Product behavior remains defined by PRODUCT.md.
  • An observed capability is evidence for the tested operation, filesystem, version, and effective configuration only.
  • A failed capability probe produces an unknown or unavailable capability, not a universal platform claim.
  • Safety policy may use a counterexample to reject an unsafe inference across environments.
  • Versioned package-manager evidence must be repeated before supporting another operation, version, or effective configuration.
  • Throwaway feasibility code is not product coverage unless promoted into a repository test gate.

Requirement evidence map

Weak inactivity and namespace evidence

Evidence: candidate_inactivity_and_namespace.md

Supports:

  • PRODUCT.md section 6.2: age, pathname, a missing target, and negative descriptor observations do not establish disposability.
  • PRODUCT.md section 6.3: mapped files are live evidence, while no observed reference is not proof of inactivity.
  • PRODUCT.md sections 5.1 and 8: package ownership must be established before generic deletion or broken-link eligibility.
  • PRODUCT.md section 8: absolute targets inside a proot root require that root's namespace.

Limits:

  • The experiment supplies counterexamples, not a complete producer-evidence taxonomy.
  • It does not define observation windows or prove that every old or dangling object is live.

Private-storage accounting

Evidence: private_storage_accounting.md

Supports:

  • PRODUCT.md section 7: apparent bytes cannot substitute for allocated blocks.
  • spec/CODING_STYLE.md: hard-link tests need injected metadata or a probed capable filesystem when Android denies fixture creation.

Limits:

  • The allocation observations apply to the recorded F2FS environment.
  • Hard-link creation failure does not imply that hard links cannot be encountered.

Shared-storage capabilities

Evidence: shared_storage_capabilities.md

Supports:

  • PRODUCT.md section 4.1: configured shared-storage aliases may be resolved during root initialization and deduplicated when physical root and runtime identity agree.
  • PRODUCT.md sections 4.1 and 7: filesystem type, stable identity checks, and one successful metadata operation do not prove reliable allocated-block or mutation semantics.
  • PRODUCT.md section 15.21: unsupported or untrusted capabilities remain visible and fail closed.

Limits:

  • The experiment did not enumerate or mutate operator shared storage.
  • It does not establish allocation, lifecycle-stable identity, or mutation capabilities.

Descendant ancestry

Evidence: descendant_ancestry_race.md

Supports:

  • PRODUCT.md sections 10 and 11.1: a retained descendant-parent descriptor is not ancestry evidence.
  • PRODUCT.md section 11.1: every reviewed ancestor must be re-established from the selected-root identity before mutation.
  • PRODUCT.md section 11.1: a same-permission process can move an ancestor after the final check.

Limits:

  • The experiment demonstrates one deterministic rename interleaving.
  • It does not demonstrate symlink traversal or eliminate the residual post-check race.

Root open denial

Evidence: android_root_open_denied.md

Supports:

  • PRODUCT.md section 11.1: mutation ancestry revalidation anchors at the configured selected root and reopens every reviewed ancestor below it descriptor-relative; the filesystem root itself is never opened and no prefix above a configured root is traversable.
  • PRODUCT.md section 15.1 PL-ROOT-OPEN: the application domain cannot open /.

Limits:

  • One device, one kernel, one application domain; no SELinux policy enumeration was performed.
  • The probe does not generalize to other Android versions or vendor configurations.

Identity-conditional deletion

Evidence: filesystem_revalidation_race.md

Supports:

  • PRODUCT.md section 11.1: metadata revalidation followed by unlinkat is not atomic deletion by reviewed identity.
  • PRODUCT.md section 11.1: replacement observed before mutation blocks the action, but replacement after the final check remains a disclosed residual race.
  • PRODUCT.md section 11.1: deleting a substituted symlink entry does not delete its target.
  • Quarantine and mode 0700 are not isolation from another process with the same UID and therefore do not justify a stronger version 1 safety claim.

Limits:

  • The experiment records the tested Android kernel and researched Linux interfaces.
  • Future identity-conditional unlink interfaces require a new capability decision and evidence.

Package-manager planning purity

Evidence: package_manager_dry_run.md

Supports:

  • PRODUCT.md sections 10 and 14.6: an option named --dry-run is not evidence of read-only planning.
  • PRODUCT.md sections 10 and 14.6: capability evidence includes manager and runtime startup and shutdown behavior under the effective configuration.
  • PRODUCT.md section 10: an operation without established read-only planning remains unavailable.

Limits:

  • The result applies to the recorded npm version, operations, and isolated configuration.
  • It does not establish capabilities for other npm operations, versions, or managers.

Run-log flush capability

Evidence: run_log_flush.md

Supports:

  • PRODUCT.md section 11.3: append with no-follow and close-on-exec flags, fdatasync on intent and result, and fsync on the parent directory are accepted on tested Termux private storage.
  • spec/TESTING.md: capable-platform syscall traces can verify open, write, and flush ordering.

Limits:

  • Success reports kernel acceptance, not guaranteed persistence across power loss or dishonest storage layers.
  • The result does not establish capability on shared, removable, remote, or other filesystems.
  • Runtime failures must still fail closed.

Testing-strategy feasibility

Evidence: testing_strategy_core.md

Supports:

  • spec/TESTING.md: fixed-capacity state-machine tests, typed effect ledgers, allocator sealing, and cell-grid oracles are practical with the pinned Zig generation.
  • spec/TESTING.md: golden grids require independent dimension and structural assertions.

Limits:

  • The throwaway suite is not production code and is not reachable through zig build test.
  • It does not cover PTY behavior, filesystem races, process control, or production-scale suites.

Evidence still required

The following claims need decisions or new experiments before they can be closed:

  • capable-platform evidence for each supported filesystem capability tuple;
  • run-log flush capability on every supported logging filesystem;
  • operation/version/configuration matrices for every package adapter;
  • terminal input, restoration, mouse, and backpressure behavior in the production terminal layer;
  • measured validation of event-loop, cancellation, worker, process, and rendering bounds;
  • assistive-technology evidence at the required terminal dimensions;
  • production tests for the configuration, classification, adapter, and limit tables.
# Experimental evidence

This index connects platform observations to normative requirements.
An experiment supports only the stated conclusion on the recorded environment.
It does not replace deterministic product tests or extend a claim beyond its observed scope.

## Evidence rules

- Product behavior remains defined by [`PRODUCT.md`](PRODUCT.md).
- An observed capability is evidence for the tested operation, filesystem, version, and effective
  configuration only.
- A failed capability probe produces an unknown or unavailable capability, not a universal platform
  claim.
- Safety policy may use a counterexample to reject an unsafe inference across environments.
- Versioned package-manager evidence must be repeated before supporting another operation, version,
  or effective configuration.
- Throwaway feasibility code is not product coverage unless promoted into a repository test gate.

## Requirement evidence map

### Weak inactivity and namespace evidence

Evidence: [`candidate_inactivity_and_namespace.md`](experiments/candidate_inactivity_and_namespace.md)

Supports:

- `PRODUCT.md` section 6.2: age, pathname, a missing target, and negative descriptor observations do not
  establish disposability.
- `PRODUCT.md` section 6.3: mapped files are live evidence, while no observed reference is not proof of
  inactivity.
- `PRODUCT.md` sections 5.1 and 8: package ownership must be established before generic deletion or
  broken-link eligibility.
- `PRODUCT.md` section 8: absolute targets inside a proot root require that root's namespace.

Limits:

- The experiment supplies counterexamples, not a complete producer-evidence taxonomy.
- It does not define observation windows or prove that every old or dangling object is live.

### Private-storage accounting

Evidence: [`private_storage_accounting.md`](experiments/private_storage_accounting.md)

Supports:

- `PRODUCT.md` section 7: apparent bytes cannot substitute for allocated blocks.
- `spec/CODING_STYLE.md`: hard-link tests need injected metadata or a probed capable filesystem when
  Android denies fixture creation.

Limits:

- The allocation observations apply to the recorded F2FS environment.
- Hard-link creation failure does not imply that hard links cannot be encountered.

### Shared-storage capabilities

Evidence: [`shared_storage_capabilities.md`](experiments/shared_storage_capabilities.md)

Supports:

- `PRODUCT.md` section 4.1: configured shared-storage aliases may be resolved during root
  initialization and deduplicated when physical root and runtime identity agree.
- `PRODUCT.md` sections 4.1 and 7: filesystem type, stable identity checks, and one successful metadata
  operation do not prove reliable allocated-block or mutation semantics.
- `PRODUCT.md` section 15.21: unsupported or untrusted capabilities remain visible and fail closed.

Limits:

- The experiment did not enumerate or mutate operator shared storage.
- It does not establish allocation, lifecycle-stable identity, or mutation capabilities.

### Descendant ancestry

Evidence: [`descendant_ancestry_race.md`](experiments/descendant_ancestry_race.md)

Supports:

- `PRODUCT.md` sections 10 and 11.1: a retained descendant-parent descriptor is not ancestry evidence.
- `PRODUCT.md` section 11.1: every reviewed ancestor must be re-established from the selected-root
  identity before mutation.
- `PRODUCT.md` section 11.1: a same-permission process can move an ancestor after the final check.

Limits:

- The experiment demonstrates one deterministic rename interleaving.
- It does not demonstrate symlink traversal or eliminate the residual post-check race.

### Root open denial

Evidence: [`android_root_open_denied.md`](experiments/android_root_open_denied.md)

Supports:

- `PRODUCT.md` section 11.1: mutation ancestry revalidation anchors at the configured selected root
  and reopens every reviewed ancestor below it descriptor-relative; the filesystem root itself is
  never opened and no prefix above a configured root is traversable.
- `PRODUCT.md` section 15.1 `PL-ROOT-OPEN`: the application domain cannot open `/`.

Limits:

- One device, one kernel, one application domain; no SELinux policy enumeration was performed.
- The probe does not generalize to other Android versions or vendor configurations.

### Identity-conditional deletion

Evidence: [`filesystem_revalidation_race.md`](experiments/filesystem_revalidation_race.md)

Supports:

- `PRODUCT.md` section 11.1: metadata revalidation followed by `unlinkat` is not atomic deletion by
  reviewed identity.
- `PRODUCT.md` section 11.1: replacement observed before mutation blocks the action, but replacement
  after the final check remains a disclosed residual race.
- `PRODUCT.md` section 11.1: deleting a substituted symlink entry does not delete its target.
- Quarantine and mode `0700` are not isolation from another process with the same UID and therefore
  do not justify a stronger version 1 safety claim.

Limits:

- The experiment records the tested Android kernel and researched Linux interfaces.
- Future identity-conditional unlink interfaces require a new capability decision and evidence.

### Package-manager planning purity

Evidence: [`package_manager_dry_run.md`](experiments/package_manager_dry_run.md)

Supports:

- `PRODUCT.md` sections 10 and 14.6: an option named `--dry-run` is not evidence of read-only planning.
- `PRODUCT.md` sections 10 and 14.6: capability evidence includes manager and runtime startup and
  shutdown behavior under the effective configuration.
- `PRODUCT.md` section 10: an operation without established read-only planning remains unavailable.

Limits:

- The result applies to the recorded npm version, operations, and isolated configuration.
- It does not establish capabilities for other npm operations, versions, or managers.

### Run-log flush capability

Evidence: [`run_log_flush.md`](experiments/run_log_flush.md)

Supports:

- `PRODUCT.md` section 11.3: append with no-follow and close-on-exec flags, `fdatasync` on intent and
  result, and `fsync` on the parent directory are accepted on tested Termux private storage.
- `spec/TESTING.md`: capable-platform syscall traces can verify open, write, and flush ordering.

Limits:

- Success reports kernel acceptance, not guaranteed persistence across power loss or dishonest
  storage layers.
- The result does not establish capability on shared, removable, remote, or other filesystems.
- Runtime failures must still fail closed.

### Testing-strategy feasibility

Evidence: [`testing_strategy_core.md`](experiments/testing_strategy_core.md)

Supports:

- `spec/TESTING.md`: fixed-capacity state-machine tests, typed effect ledgers, allocator sealing, and
  cell-grid oracles are practical with the pinned Zig generation.
- `spec/TESTING.md`: golden grids require independent dimension and structural assertions.

Limits:

- The throwaway suite is not production code and is not reachable through `zig build test`.
- It does not cover PTY behavior, filesystem races, process control, or production-scale suites.

## Evidence still required

The following claims need decisions or new experiments before they can be closed:

- capable-platform evidence for each supported filesystem capability tuple;
- run-log flush capability on every supported logging filesystem;
- operation/version/configuration matrices for every package adapter;
- terminal input, restoration, mouse, and backpressure behavior in the production terminal layer;
- measured validation of event-loop, cancellation, worker, process, and rendering bounds;
- assistive-technology evidence at the required terminal dimensions;
- production tests for the configuration, classification, adapter, and limit tables.