feat(Throw): add ceiling flight projection app

[kyleve]

Posted by an AI agent on kve's behalf.

Summary

• Add Throw, an iPhone and iPad app that projects live aircraft onto a ceiling, external display, or on-device preview.
• Provide geographic Map and altitude-aware True Sky projection modes with one shared calibration model.
• Support adsb.lol, local readsb, ADS-B Exchange Personal through RapidAPI, and Flightradar24.
• Add offline geography, regional Map centers, aircraft silhouettes, route labels, motion prediction, quiet hours, onboarding, and source diagnostics.
• Harden the original implementation for a real personal beta with typed launch, persistence, source, projection, and lifecycle state.
• Add bounded TLA+ models for the concurrent state machines that cannot be proved by Swift's type system alone.

Product behavior

• Map uses great-circle distance and bearing around a selected regional center. A dim observer ring preserves the actual location.
• True Sky uses WGS84 ECEF and ENU geometry to derive aircraft azimuth and elevation.
• Preview, full-screen output, and external displays use the same opaque-black projection surface.
• Quiet standby keeps output black and stops physical polling. Foreground output demand controls the idle timer and polling lifecycle.
• Cloud sources receive a center rounded to 0.1 degrees. Throw applies exact local filtering after every response.
• Throw never changes providers automatically after a failure and never combines observations from different source contexts.
• One playlist controls every output. Air & Space is the only runnable View in this release; Transit remains planned and unavailable.

Shipping hardening

• The process now owns one typed cold-launch state and gates every controller and projection surface until preferences and credentials load.
• Controller-scene lifecycle is aggregated across windows. External-display scenes affect output demand but cannot impersonate controller foreground state.
• Final-background preference flushing waits for active mutations and admitted async producers, retains an iOS background lease, and handles cancellation.
• Source, observer, onboarding, and ordinary preference changes use failure-atomic transactions with retry or compensating publication behavior.
• Source and observer context changes retire the exact coordinator lease, invalidate staged frames, and mint a fresh lease when demand remains.
• Geography-only and layer-disabled states suspend physical polling without destroying the coordinator's experience lease.
• Polling publications carry an exact activation token and a strictly increasing per-token revision. Delayed updates cannot be relabeled or regress state.
• Prepared transitions carry one typed context generation. Old prepare, fade, commit, and completion callbacks cannot publish after invalidation.
• Durable logging attaches once at process composition. Typed pre-attachment failures remain available for postmortem diagnostics.
• The privacy manifest declares the required UserDefaults reason, and a built-product test verifies the shipped declaration.

Compiler-proved boundaries

• Stored preferences remain validated domain aggregates. Views commit raw drafts only after validation succeeds.
• Source validation uses closed credential-free and credential-bearing requests. Unsupported secret and provider combinations cannot compile.
• Runnable projection identity is closed. Production code cannot make planned Transit executable through a catalog or playlist shortcut.
• Semantic and projected layer frames carry exact element and line-style families. Aircraft, stars, satellites, Geography, Transit routes, and vehicles cannot cross families.
• Prepared Transit network data pairs its source revision with its projected frame in one value.
• Production rendered projections require a coordinator lease and keep semantic input, projected output, observer context, effects, and health in one atomic state.
• Projected frame erasure occurs once at the ThrowUI presentation boundary. Bumper Bowling guards this boundary and the runtime composition rules.

These changes follow Where's main architecture patterns: create shared resources once, inject them, publish closed state, and keep persistence behind typed transactions.

Formal verification

The PR adds five Throw concerns to the repository's pinned TLC runner. Each concern includes historical broken controls and anti-vacuity reachability checks.

• ProjectionActivation checks scene demand, quiet and calibration gates, coordinator leases, context renewal, physical polling suspension, stale teardown, and convergence.
• PreferenceTransactions checks source and observer commits, credential alignment, retry behavior, exact lease retirement, delayed callbacks, and observer/frame consistency.
• ProjectionContextTransition checks prepared context invalidation, the black-only frame exchange, exact semantic/projected pairing, and writer exclusion during fade-in.
• PollingPublication checks exact Core tokens, per-token revision order, recovery reads, stale frame rejection, query replacement, and final deactivation.
• BackgroundPreferencePersistence checks producer admission, quiescent flush completion, cancellation-aware waiters, retry work, and controller-scene lifecycle generations.

All current configurations are verified for their documented finite bounds and assumptions. Every broken control fails its named current invariant.

Compatibility and rollout

• Throw uses a separate persistence domain. This change does not modify Where data, backups, or CloudKit data.
• Version-one Throw preferences migrate to the current typed format without repeating onboarding.
• Existing RapidAPI and Flightradar24 Keychain identifiers remain unchanged.
• Invalid preferences enter setup repair. Missing credentials never trigger provider fallback.
• This PR targets a personal beta. Throw/TODOs.md retains the required physical projector, provider-contract, iOS 27 GM, and overnight acceptance work.
• Public distribution still requires provider authorization and a provider-approved credential architecture.

Review focus

• Review exact lease renewal across source, observer, quiet, calibration, layer, and scene changes.
• Review source cancellation, polling token/revision acceptance, and physical polling suspension.
• Review preference transaction compensation and the final-background quiescence barrier.
• Review atomic visible projection publication and frame exchange at black.
• Review typed source, runnable catalog, layer-family, and presentation-erasure boundaries.
• Review the documented TLA+ source correspondence, assumptions, exclusions, and broken controls.

Testing

• ./test --everything --review — passed: 2,470 iOS unit tests and all 61 snapshot suites.
• ./test --no-generate ThrowCoreTests ThrowUITests — passed: 466 tests.
• ./test --no-generate ThrowTests — passed: 17 tests.
• ./test --no-generate ThrowUISnapshotTests --review — passed: 13 tests with byte-for-byte matching captures.
• ./test --architecture-only — passed: 30 rule tests and no violations.
• ./tla-check ProjectionActivation — passed all 31 cases; largest current bound explored 82,983 generated states.
• ./tla-check PreferenceTransactions — passed all 13 cases; largest current bound explored 181,368 generated states.
• ./tla-check ProjectionContextTransition — passed all 13 cases; largest current bound explored 102,734 generated states.
• ./tla-check PollingPublication — passed all 14 cases; largest current bound explored 79,350 generated states.
• ./tla-check BackgroundPreferencePersistence — passed all 7 cases; largest reachability bound explored 5,122,617 generated states.
• TLA tooling tests — passed: 16 Python tests and 7 Ruby tests with 68 assertions.
• ./swiftformat --lint, ./sf-symbols --lint, ./xcstrings --lint, ./shellcheck, and ./attribution --check — passed.
• git diff --check — passed.

[kyleve]

Posted by an AI agent on kve’s behalf.

Review focus: this registration path compiles against the installed iOS 27 beta SDK, but the final UISceneAccessory lifecycle contract still needs GM-SDK and physical connect/disconnect plus controller-window recreation validation. That release gate is recorded in Throw/TODOs.md.