feat(Where): add scheduled encrypted backups

[kyleve]

Updated by an AI agent on the author's behalf.

Summary

• User-facing: Add encrypted automatic backups for recording-enabled installations. Weekly is the default; users can choose daily or monthly, or disable backups.
• User-facing: Write to iCloud Drive with an app Documents fallback. List accessible backups, sizes, and storage locations on the Data page.
• User-facing: Provide a hidden, copyable recovery key and onboarding-only encrypted restore. Manual ZIP exports remain plaintext.
• Internal: Add reusable KeychainKit storage, an AES-256-GCM container, and cancellable background processing that waits for first unlock.
• Internal: Check lifecycle, recovery-key publication, and retention protocols with bounded PlusCal models and Swift regression tests.

Why

Residency history is important and difficult to reconstruct. Automatic encrypted copies provide recovery when app data is damaged or lost.

Design decisions

• Each installation pins its active key locally. An append-only iCloud Keychain collection preserves every key under its identifier. Independently created offline keys cannot replace each other when synchronization resumes.
• Restore selects the key named by the archive. A copied alternate key remains ephemeral. The Data page asks users to keep a copy from each recording device.
• A Class C protected-file probe distinguishes first unlock from an ordinary screen lock. The shared launch plan waits for first unlock before loading the installation sidecar. RootView promotion cannot bypass that barrier. Construction performs no sidecar file access; later relocking does not suppress recording.
• One service-owned operation serializes automatic triggers. Background expiration can cancel execution. A disappearing Data page cannot cancel it: that caller waits for the result and records successful metadata, but performs no further view refresh.
• Catalog reads have an independent cancellation context outside the storage actor. Download metadata is checked before content coordination. Evicted iCloud files produce a partial listing without hiding accessible cloud or local files. The view cancels its own pending reads and ignores stale results.
• File commitment and retention are separate. A committed backup advances success metadata even if later maintenance fails; failed maintenance cannot trigger a duplicate fallback write.

Review focus

• Retention authenticates and validates complete archives before counting them toward the newest three. Unknown-key, malformed, and manual files are preserved. Deletion acquires read intents for all three keepers and a delete intent for the candidate together, then compares every digest before deleting.
• The retention model exposed a stale-keeper race: candidate-only revalidation could remove a healthy backup after one of its replacements became damaged. The coordinated keeper checks and Swift regression tests address that counterexample.
• Coordinated operations use the URLs supplied by the coordinator. Cloud read failures remain visible as partial catalog failures; local failures do not appear as an empty successful list.
• Scheduling reconciles the latest preferences and drains outstanding work before a scope shuts down. Reset-generation checks reject late success updates from an erased scope.
• Hiding the recovery key invalidates pending reveals. BackupSettingsSection owns lifecycle actions; its shared display child supplies deterministic snapshots without disabling production hiding behavior.

Formal verification scope

The three backup specifications include Swift mappings, explicit bounds, safety properties, liveness assumptions, and negative controls. All 19 configurations produced their expected verdicts: six passing state-space checks and thirteen counterexample or reachability controls.

The models cover first-unlock admission, cancellation ownership, drain-before-retirement, generation-checked success, independent key creation and synchronization, and authenticated retention. They do not prove the Swift implementation or iOS services. In particular, coordinated retention assumes a consistent local filesystem view; it is not a distributed transaction across delayed iCloud replicas. Cryptography, permanent device loss, and live-service behavior require separate validation.

Compatibility

Manual .zip exports and the inner backup schema are unchanged. Automatic .wherebackup files wrap that ZIP in a versioned authenticated container.

The previous synchronized recovery-key account is preserved and imported into the collection without replacement. Erasing Where data does not erase recovery keys.

Testing

• ./ide --no-open, ./sync-agents, ./swiftformat --lint, ./xcstrings --lint, and ./attribution --check passed. The changed .bumper Swift files also passed explicit formatting lint.
• ./test --all --no-generate passed 2,036 tests against the final code. Coverage includes first-unlock waiters, deferred sidecar loading, cancellation ownership, disappeared views, blocked catalog reads, partial iCloud listings, and changed or missing retention keepers.
• The test driver validated Bumper Bowling configuration, passed all 17 architecture-rule tests, and reported no architecture violations. Backup-upgrade tests passed seven tests with 18 assertions.
• ./tla-check AutomaticBackupLifecycle, ./tla-check RecoveryKeyPublication, and ./tla-check AutomaticBackupRetention passed all 19 expected verdicts. The largest retention case explored 2,661,340 distinct states; the three-device key case explored 863,441.
• ./test --snapshots --no-generate --skip-architecture --review --only WhereUISnapshotTests/BackupSettingsSectionSnapshotTests --only WhereUISnapshotTests/DataSettingsViewSnapshotTests --only WhereUISnapshotTests/RootViewSnapshotTests passed all three suites and 24 captures. A fresh --no-build comparison passed again. No reference images changed in this follow-up. All 20 backup/Data captures matched byte for byte; each run reported one tolerated, one-channel, one-pixel RootView difference.
• mise exec -- tuist test Ledger-macOS-Tests --no-selective-testing -- -destination 'platform=macOS' passed during the earlier feature validation. It was not repeated for this follow-up because Ledger and KeychainKit did not change. Unaffected image-snapshot suites were not repeated.

Release follow-up

Signed-device validation remains required for reboot/first-unlock behavior, later locked recording, background expiration, independent offline key creation and synchronization, cross-device restore, and iCloud Drive download/fallback. Use disposable test data. These hardware and live-service checks cannot be proved by simulator tests or bounded models; they are tracked in Where/TODOs.md.