From 76f84868be4981e78d34b4bda1f6182454446f7e Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:39:04 -0700 Subject: [PATCH 01/14] Add unified ./tla-check runner and migrate TrackingReconciliation Extract a root script that discovers specs via manifest.json, pins TLC and Temurin through mise, and runs pass/fail cases. TrackingReconciliation drops its local check script in favor of the shared runner. Co-authored-by: Cursor --- .agents/skills/tla-verify-protocol/SKILL.md | 7 +- .../TrackingReconciliation/README.md | 16 +- .../TrackingReconciliation/check | 125 -------- .../TrackingReconciliation/manifest.json | 16 ++ tla-check | 270 ++++++++++++++++++ 5 files changed, 302 insertions(+), 132 deletions(-) delete mode 100755 Where/Specifications/TrackingReconciliation/check create mode 100644 Where/Specifications/TrackingReconciliation/manifest.json create mode 100755 tla-check diff --git a/.agents/skills/tla-verify-protocol/SKILL.md b/.agents/skills/tla-verify-protocol/SKILL.md index b5e7698f..28f7262c 100644 --- a/.agents/skills/tla-verify-protocol/SKILL.md +++ b/.agents/skills/tla-verify-protocol/SKILL.md @@ -92,10 +92,15 @@ convention. In this repository, prefer a feature-level - the `.tla` module; - configurations for the relevant current, negative-control, and candidate designs; -- a local executable checker; +- a `manifest.json` declaring each TLC case and its pass/fail expectation; - a short README with the question, correspondence table, bounds, assumptions, exclusions, properties, results, and run command. +Run checks from the repository root with `./tla-check [ ...]` (see +[`Where/Specifications/TrackingReconciliation`](../../../Where/Specifications/TrackingReconciliation/README.md)). +The root script owns TLC/JDK download and pinning; do not add per-spec `check` +scripts or wire TLA+ into CI unless explicitly requested. + Do not force these exact filenames when the protocol needs a different model shape. diff --git a/Where/Specifications/TrackingReconciliation/README.md b/Where/Specifications/TrackingReconciliation/README.md index 5af70cf4..831ba8d4 100644 --- a/Where/Specifications/TrackingReconciliation/README.md +++ b/Where/Specifications/TrackingReconciliation/README.md @@ -58,22 +58,26 @@ launch and foreground reconciliation, authorization observation, and permission completion must all join it. Serializing only the toggle setter would not implement the modeled design. -This is design evidence, not yet the product fix. Implementing the worker should -make the Swift guard pass without `withKnownIssue`; changing the design should -change this model first so its assumptions remain explicit. +This is design evidence that informed the product fix. The coalesced worker is +implemented on ``WhereSession``; the deterministic guard in +[`WhereSessionTrackingTests`](../../WhereUI/Tests/WhereSessionTrackingTests.swift) +(`newerStopWinsOverInFlightStart`) holds the real implementation at the modeled +await and passes without `withKnownIssue`. ## Run it -From this directory: +From the repository root: ```sh -./check +./tla-check TrackingReconciliation ``` +Or run every spec: `./tla-check`. See `./tla-check --help` for options. + The checker pins TLC 1.7.4 by SHA-256 and Eclipse Temurin 21.0.8+9 through `mise`. It caches both under the repository's ignored `.build/tla/` directory. A clean first run needs network access and downloads about 350 MB, almost all of it the JDK. Each run keeps its TLC log and state under `.build/tla/runs/`. A successful run means the broken model failed for the expected invariant and the -coalesced model completed without an error. The pilot is opt-in and is not wired +coalesced model completed without an error. Checks are opt-in and are not wired into CI. diff --git a/Where/Specifications/TrackingReconciliation/check b/Where/Specifications/TrackingReconciliation/check deleted file mode 100755 index 3281de27..00000000 --- a/Where/Specifications/TrackingReconciliation/check +++ /dev/null @@ -1,125 +0,0 @@ -#!/usr/bin/env bash -set -euo pipefail - -script_dir="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" -repo_root="$(cd "$script_dir/../../.." && pwd)" - -tlc_version="1.7.4" -tlc_sha256="936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" -tlc_url="https://github.com/tlaplus/tlaplus/releases/download/v${tlc_version}/tla2tools.jar" -java_version="temurin-21.0.8+9.0.LTS" - -tool_root="$repo_root/.build/tla" -jar_dir="$tool_root/v${tlc_version}" -jar_path="$jar_dir/tla2tools.jar" -runs_dir="$tool_root/runs" - -usage() { - cat <<'EOF' -Usage: ./check - -Check that TLC finds the expected tracking race in Broken.cfg and accepts the -serialized worker in Coalesced.cfg. Downloads pinned tools into .build/tla/. - -Set TLA_JAVA to a Java executable to bypass the pinned mise runtime. -EOF -} - -case "${1:-}" in - "") ;; - -h|--help) - usage - exit 0 - ;; - *) - usage >&2 - exit 2 - ;; -esac - -mkdir -p "$jar_dir" "$runs_dir" -run_dir="$(mktemp -d "$runs_dir/TrackingReconciliation.XXXXXX")" -logs_dir="$run_dir/logs" -states_dir="$run_dir/states" -mkdir -p "$logs_dir" "$states_dir/broken" "$states_dir/coalesced" - -checksum() { - shasum -a 256 "$1" | awk '{print $1}' -} - -if [[ ! -f "$jar_path" ]]; then - download_path="$(mktemp "$jar_dir/tla2tools.jar.download.XXXXXX")" - echo "Downloading TLC ${tlc_version}..." - curl --fail --location --retry 3 --output "$download_path" "$tlc_url" - if [[ "$(checksum "$download_path")" != "$tlc_sha256" ]]; then - echo "TLC download checksum did not match ${tlc_sha256}." >&2 - exit 1 - fi - mv "$download_path" "$jar_path" -fi - -if [[ "$(checksum "$jar_path")" != "$tlc_sha256" ]]; then - echo "Cached TLC checksum did not match ${tlc_sha256}." >&2 - exit 1 -fi - -export MISE_DATA_DIR="$tool_root/mise/data" -export MISE_CACHE_DIR="$tool_root/mise/cache" -export MISE_STATE_DIR="$tool_root/mise/state" -export MISE_CONFIG_DIR="$tool_root/mise/config" - -run_java() { - if [[ -n "${TLA_JAVA:-}" ]]; then - "$TLA_JAVA" "$@" - else - mise --yes --no-config x "java@$java_version" -- java "$@" - fi -} - -run_tlc() { - local config="$1" - local metadir="$2" - run_java \ - -XX:+UseParallelGC \ - -Xmx1g \ - -jar "$jar_path" \ - -cleanup \ - -difftrace \ - -metadir "$metadir" \ - -config "$config" \ - "$script_dir/TrackingReconciliation.tla" -} - -broken_log="$logs_dir/broken.log" -coalesced_log="$logs_dir/coalesced.log" - -echo "Checking that the broken implementation produces the expected counterexample..." -set +e -run_tlc "$script_dir/Broken.cfg" "$states_dir/broken" >"$broken_log" 2>&1 -broken_status=$? -set -e - -if [[ $broken_status -eq 0 ]]; then - echo "Broken.cfg unexpectedly passed; inspect $broken_log." >&2 - exit 1 -fi -if ! grep -Fq "Invariant CorrectAtQuiescence is violated." "$broken_log"; then - echo "Broken.cfg failed for an unexpected reason; inspect $broken_log." >&2 - tail -n 80 "$broken_log" >&2 - exit 1 -fi - -echo "Checking that the coalesced worker satisfies the model..." -if ! run_tlc "$script_dir/Coalesced.cfg" "$states_dir/coalesced" >"$coalesced_log" 2>&1; then - echo "Coalesced.cfg failed; inspect $coalesced_log." >&2 - tail -n 80 "$coalesced_log" >&2 - exit 1 -fi -if ! grep -Fq "Model checking completed. No error has been found." "$coalesced_log"; then - echo "Coalesced.cfg did not report a clean model check; inspect $coalesced_log." >&2 - tail -n 80 "$coalesced_log" >&2 - exit 1 -fi - -echo "TLA+ pilot passed: the race is reproduced and the coalesced design checks clean." -echo "TLC run artifacts: $run_dir" diff --git a/Where/Specifications/TrackingReconciliation/manifest.json b/Where/Specifications/TrackingReconciliation/manifest.json new file mode 100644 index 00000000..f192b0e5 --- /dev/null +++ b/Where/Specifications/TrackingReconciliation/manifest.json @@ -0,0 +1,16 @@ +{ + "module": "TrackingReconciliation.tla", + "cases": [ + { + "name": "broken", + "config": "Broken.cfg", + "expect": "fail", + "outputContains": "Invariant CorrectAtQuiescence is violated." + }, + { + "name": "coalesced", + "config": "Coalesced.cfg", + "expect": "pass" + } + ] +} diff --git a/tla-check b/tla-check new file mode 100755 index 00000000..e3483d34 --- /dev/null +++ b/tla-check @@ -0,0 +1,270 @@ +#!/usr/bin/env bash +set -euo pipefail + +repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +specs_root="$repo_root/Where/Specifications" + +tlc_version="1.7.4" +tlc_sha256="936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" +tlc_url="https://github.com/tlaplus/tlaplus/releases/download/v${tlc_version}/tla2tools.jar" +java_version="temurin-21.0.8+9.0.LTS" + +tool_root="$repo_root/.build/tla" +jar_dir="$tool_root/v${tlc_version}" +jar_path="$jar_dir/tla2tools.jar" +runs_dir="$tool_root/runs" + +usage() { + cat <<'EOF' +Usage: ./tla-check [--list] [SPEC ...] + +Run TLA+ model checks declared under Where/Specifications/*/manifest.json. +With no SPEC names, every discoverable spec is checked. + +Options: + --list Print discoverable spec folder names and exit + --help Show this help + +Downloads pinned TLC and Java into .build/tla/ on first use (~350 MB). +Set TLA_JAVA to a Java executable to bypass the pinned mise runtime. +EOF +} + +checksum() { + shasum -a 256 "$1" | awk '{print $1}' +} + +ensure_tools() { + mkdir -p "$jar_dir" "$runs_dir" + + if [[ ! -f "$jar_path" ]]; then + download_path="$(mktemp "$jar_dir/tla2tools.jar.download.XXXXXX")" + echo "Downloading TLC ${tlc_version}..." + curl --fail --location --retry 3 --output "$download_path" "$tlc_url" + if [[ "$(checksum "$download_path")" != "$tlc_sha256" ]]; then + echo "TLC download checksum did not match ${tlc_sha256}." >&2 + exit 1 + fi + mv "$download_path" "$jar_path" + fi + + if [[ "$(checksum "$jar_path")" != "$tlc_sha256" ]]; then + echo "Cached TLC checksum did not match ${tlc_sha256}." >&2 + exit 1 + fi + + export MISE_DATA_DIR="$tool_root/mise/data" + export MISE_CACHE_DIR="$tool_root/mise/cache" + export MISE_STATE_DIR="$tool_root/mise/state" + export MISE_CONFIG_DIR="$tool_root/mise/config" +} + +run_java() { + if [[ -n "${TLA_JAVA:-}" ]]; then + "$TLA_JAVA" "$@" + else + mise --yes --no-config x "java@$java_version" -- java "$@" + fi +} + +discover_specs() { + find "$specs_root" -mindepth 2 -maxdepth 2 -name manifest.json -print \ + | while IFS= read -r manifest; do + basename "$(dirname "$manifest")" + done \ + | sort +} + +list_specs() { + local names + names="$(discover_specs)" + if [[ -z "$names" ]]; then + echo "No specs found under $specs_root" >&2 + exit 1 + fi + printf '%s\n' "$names" +} + +validate_spec_name() { + local name="$1" + if [[ ! -f "$specs_root/$name/manifest.json" ]]; then + echo "error: unknown spec '$name' (no manifest at $specs_root/$name/manifest.json)" >&2 + exit 1 + fi +} + +run_spec() { + local spec_name="$1" + local spec_dir="$specs_root/$spec_name" + local manifest="$spec_dir/manifest.json" + local run_dir logs_dir states_dir + local module_path module_file case_count + + validate_spec_name "$spec_name" + + module_path="$(python3 - "$manifest" <<'PY' +import json, sys +with open(sys.argv[1]) as f: + print(json.load(f)["module"]) +PY +)" + module_file="$spec_dir/$module_path" + if [[ ! -f "$module_file" ]]; then + echo "error: $spec_name manifest module '$module_path' not found" >&2 + exit 1 + fi + + run_dir="$(mktemp -d "$runs_dir/${spec_name}.XXXXXX")" + logs_dir="$run_dir/logs" + states_dir="$run_dir/states" + mkdir -p "$logs_dir" "$states_dir" + + case_count="$(python3 - "$manifest" <<'PY' +import json, sys +with open(sys.argv[1]) as f: + print(len(json.load(f)["cases"])) +PY +)" + + echo "==> $spec_name" + + python3 - "$manifest" "$spec_dir" "$module_file" "$logs_dir" "$states_dir" "$jar_path" <<'PY' +import json +import os +import subprocess +import sys + +manifest_path, spec_dir, module_file, logs_dir, states_dir, jar_path = sys.argv[1:7] + +with open(manifest_path) as f: + manifest = json.load(f) + +java_cmd = os.environ.get("TLA_JAVA") +if java_cmd: + java_base = [java_cmd] +else: + java_version = "temurin-21.0.8+9.0.LTS" + java_base = ["mise", "--yes", "--no-config", "x", f"java@{java_version}", "--", "java"] + +def run_tlc(config_path: str, metadir: str) -> tuple[int, str]: + os.makedirs(metadir, exist_ok=True) + cmd = java_base + [ + "-XX:+UseParallelGC", + "-Xmx1g", + "-jar", jar_path, + "-cleanup", + "-difftrace", + "-metadir", metadir, + "-config", config_path, + module_file, + ] + result = subprocess.run(cmd, capture_output=True, text=True) + output = result.stdout + result.stderr + return result.returncode, output + +for case in manifest["cases"]: + name = case["name"] + config_name = case["config"] + expect = case["expect"] + config_path = os.path.join(spec_dir, config_name) + log_path = os.path.join(logs_dir, f"{name}.log") + metadir = os.path.join(states_dir, name) + + if not os.path.isfile(config_path): + print(f"error: {manifest_path}: case '{name}' config '{config_name}' not found", file=sys.stderr) + sys.exit(1) + + status, output = run_tlc(config_path, metadir) + with open(log_path, "w") as log: + log.write(output) + + if expect == "pass": + if status != 0: + print(f" FAIL {name}: expected pass, TLC exited {status}; see {log_path}", file=sys.stderr) + print(output[-4000:], file=sys.stderr) + sys.exit(1) + if "Model checking completed. No error has been found." not in output: + print(f" FAIL {name}: TLC did not report a clean check; see {log_path}", file=sys.stderr) + sys.exit(1) + print(f" ok {name} (pass)") + elif expect == "fail": + if status == 0: + print(f" FAIL {name}: expected failure, TLC passed; see {log_path}", file=sys.stderr) + sys.exit(1) + needle = case.get("outputContains") + if needle and needle not in output: + print(f" FAIL {name}: expected output to contain {needle!r}; see {log_path}", file=sys.stderr) + print(output[-4000:], file=sys.stderr) + sys.exit(1) + print(f" ok {name} (expected failure)") + else: + print(f"error: {manifest_path}: case '{name}' has unknown expect {expect!r}", file=sys.stderr) + sys.exit(1) + +print(f" artifacts: {os.path.dirname(logs_dir)}") +PY +} + +main() { + local list_only=false + local specs=() + + while [[ $# -gt 0 ]]; do + case "$1" in + -h|--help) + usage + exit 0 + ;; + --list) + list_only=true + shift + ;; + --) + shift + specs+=("$@") + break + ;; + -*) + echo "error: unknown option '$1'" >&2 + usage >&2 + exit 2 + ;; + *) + specs+=("$1") + shift + ;; + esac + done + + if $list_only; then + list_specs + exit 0 + fi + + if [[ ${#specs[@]} -eq 0 ]]; then + while IFS= read -r name; do + specs+=("$name") + done < <(discover_specs) + if [[ ${#specs[@]} -eq 0 ]]; then + echo "No specs found under $specs_root" >&2 + exit 1 + fi + fi + + ensure_tools + + local spec failed=false + for spec in "${specs[@]}"; do + if ! run_spec "$spec"; then + failed=true + fi + done + + if $failed; then + exit 1 + fi + + echo "All TLA+ checks passed (${#specs[@]} spec(s))." +} + +main "$@" From e8eb3fb2f053c46e824bc614720f27024f7d5892 Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:39:08 -0700 Subject: [PATCH 02/14] Add IntentServicesHandoff TLA+ specification Models the handoff-not-factory contract for App Intent service installation: parked callers await install, clear resumes on the next install, and a later install replaces the cached stack. Cited by IntentServicesTests. Co-authored-by: Cursor --- .../IntentServicesHandoff/Broken.cfg | 10 ++ .../IntentServicesHandoff/Current.cfg | 14 ++ .../IntentServicesHandoff.tla | 123 ++++++++++++++++++ .../IntentServicesHandoff/README.md | 32 +++++ .../IntentServicesHandoff/manifest.json | 16 +++ 5 files changed, 195 insertions(+) create mode 100644 Where/Specifications/IntentServicesHandoff/Broken.cfg create mode 100644 Where/Specifications/IntentServicesHandoff/Current.cfg create mode 100644 Where/Specifications/IntentServicesHandoff/IntentServicesHandoff.tla create mode 100644 Where/Specifications/IntentServicesHandoff/README.md create mode 100644 Where/Specifications/IntentServicesHandoff/manifest.json diff --git a/Where/Specifications/IntentServicesHandoff/Broken.cfg b/Where/Specifications/IntentServicesHandoff/Broken.cfg new file mode 100644 index 00000000..aaa220f7 --- /dev/null +++ b/Where/Specifications/IntentServicesHandoff/Broken.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec + +CONSTANTS + Implementation = "broken" + +INVARIANTS + TypeOK + NoSelfCreate + +CHECK_DEADLOCK FALSE diff --git a/Where/Specifications/IntentServicesHandoff/Current.cfg b/Where/Specifications/IntentServicesHandoff/Current.cfg new file mode 100644 index 00000000..ab498967 --- /dev/null +++ b/Where/Specifications/IntentServicesHandoff/Current.cfg @@ -0,0 +1,14 @@ +SPECIFICATION Spec + +CONSTANTS + Implementation = "current" + +INVARIANTS + TypeOK + NoSelfCreate + AtMostOneAuthoritative + WaiterExactlyOnce + AfterClearMustPark + NoMixedWorld + +CHECK_DEADLOCK FALSE diff --git a/Where/Specifications/IntentServicesHandoff/IntentServicesHandoff.tla b/Where/Specifications/IntentServicesHandoff/IntentServicesHandoff.tla new file mode 100644 index 00000000..93219c33 --- /dev/null +++ b/Where/Specifications/IntentServicesHandoff/IntentServicesHandoff.tla @@ -0,0 +1,123 @@ +---- MODULE IntentServicesHandoff ---- +EXTENDS Integers + +CONSTANTS Implementation + +ASSUME Implementation \in {"current", "broken"} + +Phases == {"idle", "parked", "holding", "cancelled"} +InstallStates == {"none", "installed", "cleared"} + +VARIABLES + installed, + installState, + waiterCount, + consumerPhase, + selfCreated + +vars == <> + +Init == + /\ installed = FALSE + /\ installState = "none" + /\ waiterCount = 0 + /\ consumerPhase = "idle" + /\ selfCreated = FALSE + +IntentFiresEarly == + /\ consumerPhase = "idle" + /\ IF installed + THEN /\ consumerPhase' = "holding" + /\ UNCHANGED <> + ELSE IF Implementation = "broken" + THEN /\ selfCreated' = TRUE + /\ installed' = TRUE + /\ consumerPhase' = "holding" + /\ installState' = "installed" + /\ UNCHANGED waiterCount + ELSE /\ consumerPhase' = "parked" + /\ waiterCount' = waiterCount + 1 + /\ UNCHANGED <> + +Install == + /\ installState \in {"none", "cleared"} + /\ installed' = TRUE + /\ installState' = "installed" + /\ IF waiterCount > 0 + THEN /\ consumerPhase' = "holding" + /\ waiterCount' = waiterCount - 1 + ELSE /\ UNCHANGED <> + /\ UNCHANGED selfCreated + +Clear == + /\ installed + /\ installed' = FALSE + /\ installState' = "cleared" + /\ IF consumerPhase = "holding" + THEN consumerPhase' = "idle" + ELSE UNCHANGED consumerPhase + /\ UNCHANGED <> + +InstallReplace == + /\ installState = "installed" + /\ installed' = TRUE + /\ IF waiterCount > 0 + THEN /\ consumerPhase' = "holding" + /\ waiterCount' = waiterCount - 1 + ELSE /\ UNCHANGED <> + /\ UNCHANGED <> + +CancelWaiter == + /\ consumerPhase = "parked" + /\ waiterCount > 0 + /\ consumerPhase' = "cancelled" + /\ waiterCount' = waiterCount - 1 + /\ UNCHANGED <> + +ConsumerUsesStack == + /\ consumerPhase = "holding" + /\ installed + /\ consumerPhase' = "idle" + /\ UNCHANGED <> + +Next == + \/ IntentFiresEarly + \/ Install + \/ Clear + \/ InstallReplace + \/ CancelWaiter + \/ ConsumerUsesStack + +Fairness == + /\ WF_vars(Install) + /\ WF_vars(Clear) + /\ WF_vars(InstallReplace) + /\ WF_vars(CancelWaiter) + /\ WF_vars(ConsumerUsesStack) + /\ WF_vars(IntentFiresEarly) + +Spec == Init /\ [][Next]_vars /\ Fairness + +TypeOK == + /\ installState \in InstallStates + /\ waiterCount \in 0..2 + /\ consumerPhase \in Phases + /\ selfCreated \in BOOLEAN + /\ installed \in BOOLEAN + +NoSelfCreate == + ~selfCreated + +AtMostOneAuthoritative == + ~installed \/ installState = "installed" + +WaiterExactlyOnce == + consumerPhase /= "parked" \/ waiterCount > 0 + +AfterClearMustPark == + consumerPhase = "holding" => installed + +NoMixedWorld == + consumerPhase = "holding" => installed + +==== diff --git a/Where/Specifications/IntentServicesHandoff/README.md b/Where/Specifications/IntentServicesHandoff/README.md new file mode 100644 index 00000000..43609cd3 --- /dev/null +++ b/Where/Specifications/IntentServicesHandoff/README.md @@ -0,0 +1,32 @@ +# IntentServices handoff + +Models [`IntentServices`](../../WhereIntents/Sources/IntentServices.swift): the App Intents +stack must never self-open a store; at most one installed stack is authoritative; +parked intents resume exactly once; `clear()` forces later callers to park until +the next `install(_:)`. + +## Correspondence + +| Model | Production | +| --- | --- | +| `installed` | `IntentServices.installed` | +| `waiterCount` | parked continuations in `current()` | +| `consumerPhase` | intent awaiting / holding / cancelled | +| `selfCreated` | forbidden fallback store open | + +## Properties + +- `NoSelfCreate` — no self-assembled stack +- `AtMostOneAuthoritative` — single install generation +- `WaiterExactlyOnce` — park has a matching resume or cancel +- `AfterClearMustPark` — holding requires an installed stack +- `NoMixedWorld` — consumers never run against a cleared install + +## Result + +**Verified for these model bounds and assumptions** on `Current.cfg`. +`Broken.cfg` (fallback `make()`) falsifies `NoSelfCreate`. + +Swift guard: [`IntentServicesTests.clearWhileParkedResumesOnTheNextInstall`](../../WhereIntents/Tests/IntentServicesTests.swift). + +Run: `./tla-check IntentServicesHandoff` diff --git a/Where/Specifications/IntentServicesHandoff/manifest.json b/Where/Specifications/IntentServicesHandoff/manifest.json new file mode 100644 index 00000000..373d5e6d --- /dev/null +++ b/Where/Specifications/IntentServicesHandoff/manifest.json @@ -0,0 +1,16 @@ +{ + "module": "IntentServicesHandoff.tla", + "cases": [ + { + "name": "broken", + "config": "Broken.cfg", + "expect": "fail", + "outputContains": "Invariant NoSelfCreate is violated." + }, + { + "name": "current", + "config": "Current.cfg", + "expect": "pass" + } + ] +} From f1bb6bcacdade308795d713fa8982cc1ad10c5f6 Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:39:14 -0700 Subject: [PATCH 03/14] Fix tracking toggle race with coalesced worker Serialize ingestor start/stop on a single worker lane, re-read intent after each await, and let stop preempt an in-flight start without deadlocking. LocationIngestor.start() bails out if stop() ran during LocationSource.start(). newerStopWinsOverInFlightStart passes without withKnownIssue. Co-authored-by: Cursor --- .../Sources/Location/LocationIngestor.swift | 1 + .../WhereUI/Sources/Model/WhereSession.swift | 71 ++++++++++++++++--- .../Tests/WhereSessionTrackingTests.swift | 4 +- 3 files changed, 62 insertions(+), 14 deletions(-) diff --git a/Where/WhereCore/Sources/Location/LocationIngestor.swift b/Where/WhereCore/Sources/Location/LocationIngestor.swift index e0e2e768..da0ff93a 100644 --- a/Where/WhereCore/Sources/Location/LocationIngestor.swift +++ b/Where/WhereCore/Sources/Location/LocationIngestor.swift @@ -125,6 +125,7 @@ public actor LocationIngestor { guard !isMonitoring else { return } isMonitoring = true await locationSource.start() + guard isMonitoring else { return } Self.logger { .monitoringStarted } // Seed the in-memory queue from the durable backlog once, so samples that // failed to persist in a prior launch get retried now. diff --git a/Where/WhereUI/Sources/Model/WhereSession.swift b/Where/WhereUI/Sources/Model/WhereSession.swift index e23c6d28..6d7aaa73 100644 --- a/Where/WhereUI/Sources/Model/WhereSession.swift +++ b/Where/WhereUI/Sources/Model/WhereSession.swift @@ -81,6 +81,12 @@ public final class WhereSession { /// `authorizationTask` — only touched on the main actor except `deinit`. @ObservationIgnored private nonisolated(unsafe) var regionStyleTask: Task? + /// Serialized tracking reconcile: one ingestor start/stop in flight; re-run + /// after each await if intent or authorization no longer matches the target + /// captured for that effect (see `Where/Specifications/TrackingReconciliation`). + @ObservationIgnored private var trackingWorkerTask: Task? + @ObservationIgnored private var trackingReconcilePending = false + /// The user's picked region looks, resolved for the view environment (seeded /// into `whereBroadwayRoot(regionStyles:)` by `RootView`). Loaded at launch /// and kept live on every store change, so a Settings edit or a synced pick @@ -300,15 +306,59 @@ public final class WhereSession { /// current authorization. Tracking only runs with Always authorization. A /// launch step (see `WhereLaunch.plan(for:)`). func reconcileTracking() async { - let wasTracking = isTracking - if wantsTracking, authorizationStatus.allowsBackgroundTracking { - await services.ingestor.start() - isTracking = true - if !wasTracking { Self.logger { .backgroundTrackingStarted } } - } else { - await services.ingestor.stop() - isTracking = false - if wasTracking { Self.logger { .backgroundTrackingStopped } } + await runTrackingReconcile() + } + + /// Apply ingestor start/stop and publish ``isTracking`` on a single lane so + /// a newer stop cannot lose to an older start that resumes after its await. + private func runTrackingReconcile() async { + if let running = trackingWorkerTask { + trackingReconcilePending = true + let targetEffective = wantsTracking && authorizationStatus.allowsBackgroundTracking + if !targetEffective { + // Stop must not await an in-flight `ingestor.start()` — it can be + // parked on `LocationSource.start()` indefinitely. Pause monitoring + // now; the worker reruns after that await and publishes intent. + await services.ingestor.stop() + return + } + await running.value + return + } + + let task = Task { @MainActor in + await trackingWorkerLoop() + } + trackingWorkerTask = task + await task.value + trackingWorkerTask = nil + } + + private func trackingWorkerLoop() async { + while true { + trackingReconcilePending = false + + let targetEffective = wantsTracking && authorizationStatus.allowsBackgroundTracking + let wasTracking = isTracking + + if targetEffective { + await services.ingestor.start() + } else { + await services.ingestor.stop() + } + + let currentEffective = wantsTracking && authorizationStatus.allowsBackgroundTracking + guard currentEffective == targetEffective, !trackingReconcilePending else { + continue + } + + isTracking = currentEffective + if isTracking, !wasTracking { + Self.logger { .backgroundTrackingStarted } + } else if !isTracking, wasTracking { + Self.logger { .backgroundTrackingStopped } + } + return } } @@ -366,8 +416,7 @@ public final class WhereSession { public func stopTracking() async { wantsTracking = false - await services.ingestor.stop() - isTracking = false + await runTrackingReconcile() Self.logger { .stoppedBackgroundTracking } } diff --git a/Where/WhereUI/Tests/WhereSessionTrackingTests.swift b/Where/WhereUI/Tests/WhereSessionTrackingTests.swift index 13e12e94..53e98652 100644 --- a/Where/WhereUI/Tests/WhereSessionTrackingTests.swift +++ b/Where/WhereUI/Tests/WhereSessionTrackingTests.swift @@ -111,9 +111,7 @@ struct WhereSessionTrackingTests { await source.resumeStart() await inFlightStart.value - withKnownIssue("The TLA+ pilot reproduces the stale publication after start resumes") { - #expect(session.isTracking == false) - } + #expect(session.isTracking == false) } @Test func grantingLaterStartsTrackingViaLiveUpdates() async throws { From d4a4fae53ad87e2d0d02af8d1cf4c6525a78fddd Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:39:14 -0700 Subject: [PATCH 04/14] Add IngestorQuiesce TLA+ specification Models reset/erase teardown ordering: quiesce completes before the store wipe and a late GPS sample cannot repopulate an erased store. Co-authored-by: Cursor --- .../Specifications/IngestorQuiesce/Broken.cfg | 10 ++ .../IngestorQuiesce/Current.cfg | 12 ++ .../IngestorQuiesce/IngestorQuiesce.tla | 113 ++++++++++++++++++ .../Specifications/IngestorQuiesce/README.md | 30 +++++ .../IngestorQuiesce/manifest.json | 16 +++ 5 files changed, 181 insertions(+) create mode 100644 Where/Specifications/IngestorQuiesce/Broken.cfg create mode 100644 Where/Specifications/IngestorQuiesce/Current.cfg create mode 100644 Where/Specifications/IngestorQuiesce/IngestorQuiesce.tla create mode 100644 Where/Specifications/IngestorQuiesce/README.md create mode 100644 Where/Specifications/IngestorQuiesce/manifest.json diff --git a/Where/Specifications/IngestorQuiesce/Broken.cfg b/Where/Specifications/IngestorQuiesce/Broken.cfg new file mode 100644 index 00000000..e39904bb --- /dev/null +++ b/Where/Specifications/IngestorQuiesce/Broken.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec + +CONSTANTS + Implementation = "broken" + +INVARIANTS + TypeOK + NoPersistAfterQuiesceDone + +CHECK_DEADLOCK FALSE diff --git a/Where/Specifications/IngestorQuiesce/Current.cfg b/Where/Specifications/IngestorQuiesce/Current.cfg new file mode 100644 index 00000000..a85be29e --- /dev/null +++ b/Where/Specifications/IngestorQuiesce/Current.cfg @@ -0,0 +1,12 @@ +SPECIFICATION Spec + +CONSTANTS + Implementation = "current" + +INVARIANTS + TypeOK + NoAcceptAfterQuiesceBegin + NoPersistAfterQuiesceDone + MonitoringOffAtQuiesceDone + +CHECK_DEADLOCK FALSE diff --git a/Where/Specifications/IngestorQuiesce/IngestorQuiesce.tla b/Where/Specifications/IngestorQuiesce/IngestorQuiesce.tla new file mode 100644 index 00000000..c1f90829 --- /dev/null +++ b/Where/Specifications/IngestorQuiesce/IngestorQuiesce.tla @@ -0,0 +1,113 @@ +---- MODULE IngestorQuiesce ---- +EXTENDS Integers + +CONSTANTS Implementation + +ASSUME Implementation \in {"current", "broken"} + +Phases == {"idle", "begin", "awaiting", "done"} + +VARIABLES + acceptsSamples, + isMonitoring, + inFlightPersist, + quiescePhase, + storeCount, + sampleDelivered, + postQuiescePersist + +vars == <> + +Init == + /\ acceptsSamples = TRUE + /\ isMonitoring = TRUE + /\ inFlightPersist = FALSE + /\ quiescePhase = "idle" + /\ storeCount = 0 + /\ sampleDelivered = FALSE + /\ postQuiescePersist = FALSE + +StreamSample == + /\ quiescePhase = "idle" + /\ ~inFlightPersist + /\ storeCount < 3 + /\ sampleDelivered' = TRUE + /\ IF acceptsSamples + THEN inFlightPersist' = TRUE + ELSE inFlightPersist' = FALSE + /\ UNCHANGED <> + +CompletePersist == + /\ inFlightPersist + /\ inFlightPersist' = FALSE + /\ postQuiescePersist' = (quiescePhase = "done") + /\ IF quiescePhase = "done" /\ Implementation = "current" + THEN UNCHANGED storeCount + ELSE storeCount' = storeCount + 1 + /\ UNCHANGED <> + +BeginQuiesce == + /\ quiescePhase = "idle" + /\ quiescePhase' = "begin" + /\ acceptsSamples' = IF Implementation = "broken" THEN acceptsSamples ELSE FALSE + /\ isMonitoring' = FALSE + /\ UNCHANGED <> + +AwaitInFlight == + /\ quiescePhase = "begin" + /\ quiescePhase' = "awaiting" + /\ UNCHANGED <> + +CompleteQuiesce == + /\ quiescePhase = "awaiting" + /\ ~inFlightPersist + /\ quiescePhase' = "done" + /\ UNCHANGED <> + +LateSampleAfterQuiesce == + /\ quiescePhase = "done" + /\ ~inFlightPersist + /\ sampleDelivered' = TRUE + /\ IF acceptsSamples + THEN inFlightPersist' = TRUE + ELSE inFlightPersist' = FALSE + /\ UNCHANGED <> + +Next == + \/ StreamSample + \/ CompletePersist + \/ BeginQuiesce + \/ AwaitInFlight + \/ CompleteQuiesce + \/ LateSampleAfterQuiesce + +Fairness == + /\ WF_vars(StreamSample) + /\ WF_vars(CompletePersist) + /\ WF_vars(BeginQuiesce) + /\ WF_vars(AwaitInFlight) + /\ WF_vars(CompleteQuiesce) + /\ WF_vars(LateSampleAfterQuiesce) + +Spec == Init /\ [][Next]_vars /\ Fairness + +TypeOK == + /\ acceptsSamples \in BOOLEAN + /\ isMonitoring \in BOOLEAN + /\ inFlightPersist \in BOOLEAN + /\ quiescePhase \in Phases + /\ storeCount \in 0..3 + /\ sampleDelivered \in BOOLEAN + /\ postQuiescePersist \in BOOLEAN + +NoAcceptAfterQuiesceBegin == + quiescePhase \in {"begin", "awaiting", "done"} => ~acceptsSamples + +NoPersistAfterQuiesceDone == + ~postQuiescePersist + +MonitoringOffAtQuiesceDone == + quiescePhase = "done" => ~isMonitoring + +==== diff --git a/Where/Specifications/IngestorQuiesce/README.md b/Where/Specifications/IngestorQuiesce/README.md new file mode 100644 index 00000000..c34d3639 --- /dev/null +++ b/Where/Specifications/IngestorQuiesce/README.md @@ -0,0 +1,30 @@ +# Ingestor quiesce + +Models [`LocationIngestor.quiesce()`](../../WhereCore/Sources/Location/LocationIngestor.swift) +during reset: once quiesce completes, no sample persist may land after teardown. + +## Correspondence + +| Model | Production | +| --- | --- | +| `acceptsSamples` | ingest gate shut by quiesce | +| `inFlightPersist` | persist await boundary | +| `quiescePhase` | idle → begin → awaiting → done | +| `postQuiescePersist` | any persist completing while `done` | + +## Properties + +- `NoAcceptAfterQuiesceBegin` +- `NoPersistAfterQuiesceDone` (`~postQuiescePersist`) +- `MonitoringOffAtQuiesceDone` + +## Result + +**Verified for these model bounds and assumptions** on `Current.cfg`. +`Broken.cfg` (accepts samples through quiesce) falsifies `NoPersistAfterQuiesceDone`. + +Swift guard: [`LocationIngestorTests.quiesceStopsPersistingFurtherSamples`](../../WhereCore/Tests/LocationIngestorTests.swift). + +Exclusions: outbox save failure and retry eviction (see [`Where/TODOs.md`](../../TODOs.md)). + +Run: `./tla-check IngestorQuiesce` diff --git a/Where/Specifications/IngestorQuiesce/manifest.json b/Where/Specifications/IngestorQuiesce/manifest.json new file mode 100644 index 00000000..809901b8 --- /dev/null +++ b/Where/Specifications/IngestorQuiesce/manifest.json @@ -0,0 +1,16 @@ +{ + "module": "IngestorQuiesce.tla", + "cases": [ + { + "name": "broken", + "config": "Broken.cfg", + "expect": "fail", + "outputContains": "Invariant NoPersistAfterQuiesceDone is violated." + }, + { + "name": "current", + "config": "Current.cfg", + "expect": "pass" + } + ] +} From c9a7aa4ade3424426e5cbdee6758e831f7b71820 Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:39:15 -0700 Subject: [PATCH 05/14] Add LogRouting TLA+ specification Models at-most-one active durable log sink per process and scope activation handoff, covering the Flyover sibling-scope exception tracked in TODOs. Co-authored-by: Cursor --- Where/Specifications/LogRouting/Broken.cfg | 11 ++ Where/Specifications/LogRouting/Current.cfg | 13 ++ .../Specifications/LogRouting/LogRouting.tla | 136 ++++++++++++++++++ Where/Specifications/LogRouting/README.md | 30 ++++ Where/Specifications/LogRouting/manifest.json | 16 +++ 5 files changed, 206 insertions(+) create mode 100644 Where/Specifications/LogRouting/Broken.cfg create mode 100644 Where/Specifications/LogRouting/Current.cfg create mode 100644 Where/Specifications/LogRouting/LogRouting.tla create mode 100644 Where/Specifications/LogRouting/README.md create mode 100644 Where/Specifications/LogRouting/manifest.json diff --git a/Where/Specifications/LogRouting/Broken.cfg b/Where/Specifications/LogRouting/Broken.cfg new file mode 100644 index 00000000..1448750a --- /dev/null +++ b/Where/Specifications/LogRouting/Broken.cfg @@ -0,0 +1,11 @@ +SPECIFICATION Spec + +CONSTANTS + Implementation = "broken" + Scopes = {"real", "demo"} + +INVARIANTS + TypeOK + ShadowedScopeNeverRoutes + +CHECK_DEADLOCK FALSE diff --git a/Where/Specifications/LogRouting/Current.cfg b/Where/Specifications/LogRouting/Current.cfg new file mode 100644 index 00000000..c7d8774a --- /dev/null +++ b/Where/Specifications/LogRouting/Current.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec + +CONSTANTS + Implementation = "current" + Scopes = {"real", "demo"} + +INVARIANTS + TypeOK + GlobalSinkSingleOwner + ShadowedScopeNeverRoutes + ActiveScopeRecordsReachSink + +CHECK_DEADLOCK FALSE diff --git a/Where/Specifications/LogRouting/LogRouting.tla b/Where/Specifications/LogRouting/LogRouting.tla new file mode 100644 index 00000000..0cb67e2e --- /dev/null +++ b/Where/Specifications/LogRouting/LogRouting.tla @@ -0,0 +1,136 @@ +---- MODULE LogRouting ---- +EXTENDS Integers + +CONSTANTS Implementation, Scopes + +ASSUME /\ Implementation \in {"current", "broken"} + /\ Scopes = {"real", "demo"} + +RoutingStates == {"pending", "routing", "idleNoStore", "idleWithStore"} +ActiveScopes == Scopes \union {"none"} + +VARIABLES + activeScope, + realRouting, + demoRouting, + globalSinkOwner, + realStoreOpen, + demoStoreOpen + +vars == <> + +Init == + /\ activeScope = "none" + /\ realRouting = "pending" + /\ demoRouting = "pending" + /\ globalSinkOwner = "none" + /\ realStoreOpen = FALSE + /\ demoStoreOpen = FALSE + +ActivateReal == + /\ activeScope' = "real" + /\ IF realStoreOpen + THEN /\ realRouting' = "routing" + /\ globalSinkOwner' = "real" + ELSE /\ realRouting' = "pending" + /\ globalSinkOwner' = IF demoRouting = "routing" THEN "demo" ELSE "none" + /\ IF demoRouting = "routing" + THEN demoRouting' = IF demoStoreOpen THEN "idleWithStore" ELSE "idleNoStore" + ELSE UNCHANGED demoRouting + /\ UNCHANGED <> + +ActivateDemo == + /\ activeScope' = "demo" + /\ IF demoStoreOpen + THEN /\ demoRouting' = "routing" + /\ globalSinkOwner' = "demo" + ELSE /\ demoRouting' = "pending" + /\ globalSinkOwner' = IF realRouting = "routing" THEN "real" ELSE "none" + /\ IF realRouting = "routing" + THEN realRouting' = IF realStoreOpen THEN "idleWithStore" ELSE "idleNoStore" + ELSE UNCHANGED realRouting + /\ UNCHANGED <> + +DeactivateDemo == + /\ activeScope = "demo" + /\ activeScope' = "none" + /\ IF demoRouting = "routing" + THEN demoRouting' = IF demoStoreOpen THEN "idleWithStore" ELSE "idleNoStore" + ELSE UNCHANGED demoRouting + /\ globalSinkOwner' = "none" + /\ UNCHANGED <> + +RealStoreOpensLate == + /\ ~realStoreOpen + /\ realStoreOpen' = TRUE + /\ IF activeScope = "real" + THEN /\ realRouting' = "routing" + /\ globalSinkOwner' = "real" + ELSE IF Implementation = "broken" + THEN /\ realRouting' = "routing" + /\ globalSinkOwner' = "real" + ELSE /\ realRouting' = "idleWithStore" + /\ globalSinkOwner' = IF activeScope = "demo" /\ demoRouting = "routing" + THEN "demo" + ELSE "none" + /\ UNCHANGED <> + +DemoStoreOpensLate == + /\ ~demoStoreOpen + /\ demoStoreOpen' = TRUE + /\ IF activeScope = "demo" + THEN /\ demoRouting' = "routing" + /\ globalSinkOwner' = "demo" + ELSE IF Implementation = "broken" + THEN /\ demoRouting' = "routing" + /\ globalSinkOwner' = "demo" + ELSE /\ demoRouting' = "idleWithStore" + /\ globalSinkOwner' = IF activeScope = "real" /\ realRouting = "routing" + THEN "real" + ELSE "none" + /\ UNCHANGED <> + +EmitRecord == + /\ globalSinkOwner /= "none" + /\ UNCHANGED vars + +Next == + \/ ActivateReal + \/ ActivateDemo + \/ DeactivateDemo + \/ RealStoreOpensLate + \/ DemoStoreOpensLate + \/ EmitRecord + +Fairness == + /\ WF_vars(ActivateReal) + /\ WF_vars(ActivateDemo) + /\ WF_vars(DeactivateDemo) + /\ WF_vars(RealStoreOpensLate) + /\ WF_vars(DemoStoreOpensLate) + /\ WF_vars(EmitRecord) + +Spec == Init /\ [][Next]_vars /\ Fairness + +TypeOK == + /\ activeScope \in ActiveScopes + /\ realRouting \in RoutingStates + /\ demoRouting \in RoutingStates + /\ globalSinkOwner \in ActiveScopes + /\ realStoreOpen \in BOOLEAN + /\ demoStoreOpen \in BOOLEAN + +GlobalSinkSingleOwner == + (realRouting = "routing") \/ (demoRouting = "routing") + => globalSinkOwner \in {"real", "demo"} + +ShadowedScopeNeverRoutes == + /\ activeScope /= "real" => realRouting /= "routing" + /\ activeScope /= "demo" => demoRouting /= "routing" + +ActiveScopeRecordsReachSink == + /\ (activeScope = "real" => (realRouting /= "routing" \/ globalSinkOwner = "real")) + /\ (activeScope = "demo" => (demoRouting /= "routing" \/ globalSinkOwner = "demo")) + +==== diff --git a/Where/Specifications/LogRouting/README.md b/Where/Specifications/LogRouting/README.md new file mode 100644 index 00000000..d0f3da92 --- /dev/null +++ b/Where/Specifications/LogRouting/README.md @@ -0,0 +1,30 @@ +# Log routing + +Models [`WhereScope.LogRouting`](../../WhereUI/Sources/Model/WhereScope.swift): only the +active scope registers on the process-global log sink; a late store for a +shadowed scope is remembered but not attached. + +## Correspondence + +| Model | Production | +| --- | --- | +| `activeScope` | `WhereModel` active real/demo/none | +| `realRouting` / `demoRouting` | per-scope `LogRouting` phase | +| `globalSinkOwner` | `Periscope.shared` registration | + +## Properties + +- `GlobalSinkSingleOwner` +- `ShadowedScopeNeverRoutes` +- `ActiveScopeRecordsReachSink` + +## Result + +**Verified for these model bounds and assumptions** on `Current.cfg`. +`Broken.cfg` (attach on late open while shadowed) falsifies `ShadowedScopeNeverRoutes`. + +Swift guard: [`DemoModeTests.aLogStoreOpeningLateNeverAttachesToAShadowedScope`](../../WhereUI/Tests/DemoModeTests.swift). + +Note: static `WhereLog` bypass in Flyover remains tracked separately in [`Where/TODOs.md`](../../TODOs.md). + +Run: `./tla-check LogRouting` diff --git a/Where/Specifications/LogRouting/manifest.json b/Where/Specifications/LogRouting/manifest.json new file mode 100644 index 00000000..41a78d72 --- /dev/null +++ b/Where/Specifications/LogRouting/manifest.json @@ -0,0 +1,16 @@ +{ + "module": "LogRouting.tla", + "cases": [ + { + "name": "broken", + "config": "Broken.cfg", + "expect": "fail", + "outputContains": "Invariant ShadowedScopeNeverRoutes is violated." + }, + { + "name": "current", + "config": "Current.cfg", + "expect": "pass" + } + ] +} From 1efe26200fe3d47b66393679bbdaa89dd3293159 Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:39:19 -0700 Subject: [PATCH 06/14] Add PostWriteReconcile spec and route ingest through full fan-out DayJournal.ingest, bulk ingest, and addManualSample now call reconcileAfterDayChange() so reminders and widgets stay in sync. TLC model verifies the canonical post-write ordering; tests updated for the extra reconcile on ingest paths. Co-authored-by: Cursor --- .../PostWriteReconcile/Broken.cfg | 10 ++ .../PostWriteReconcile/Current.cfg | 11 ++ .../PostWriteReconcile/PostWriteReconcile.tla | 114 ++++++++++++++++++ .../PostWriteReconcile/README.md | 35 ++++++ .../PostWriteReconcile/manifest.json | 16 +++ .../Sources/Journal/DayJournal.swift | 6 +- Where/WhereCore/Tests/DayJournalTests.swift | 10 +- 7 files changed, 195 insertions(+), 7 deletions(-) create mode 100644 Where/Specifications/PostWriteReconcile/Broken.cfg create mode 100644 Where/Specifications/PostWriteReconcile/Current.cfg create mode 100644 Where/Specifications/PostWriteReconcile/PostWriteReconcile.tla create mode 100644 Where/Specifications/PostWriteReconcile/README.md create mode 100644 Where/Specifications/PostWriteReconcile/manifest.json diff --git a/Where/Specifications/PostWriteReconcile/Broken.cfg b/Where/Specifications/PostWriteReconcile/Broken.cfg new file mode 100644 index 00000000..0d761df0 --- /dev/null +++ b/Where/Specifications/PostWriteReconcile/Broken.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec + +CONSTANTS + Implementation = "broken" + +INVARIANTS + TypeOK + BrokenNoEarlyPing + +CHECK_DEADLOCK FALSE diff --git a/Where/Specifications/PostWriteReconcile/Current.cfg b/Where/Specifications/PostWriteReconcile/Current.cfg new file mode 100644 index 00000000..3add34fa --- /dev/null +++ b/Where/Specifications/PostWriteReconcile/Current.cfg @@ -0,0 +1,11 @@ +SPECIFICATION Spec + +CONSTANTS + Implementation = "current" + +INVARIANTS + TypeOK + NoChangesBeforeReconcileDone + ReaderSeesAppliedSideEffects + +CHECK_DEADLOCK FALSE diff --git a/Where/Specifications/PostWriteReconcile/PostWriteReconcile.tla b/Where/Specifications/PostWriteReconcile/PostWriteReconcile.tla new file mode 100644 index 00000000..02eaf0c3 --- /dev/null +++ b/Where/Specifications/PostWriteReconcile/PostWriteReconcile.tla @@ -0,0 +1,114 @@ +---- MODULE PostWriteReconcile ---- +EXTENDS Integers + +CONSTANTS Implementation + +ASSUME Implementation \in {"current", "broken"} + +WritePhases == {"idle", "inPerform", "committed"} +ReconcilePhases == {"none", "invalidating", "reminders", "widgets", "done"} + +VARIABLES + writePhase, + reconcilePhase, + changesPinged, + sideEffectsApplied, + readerSawPing + +vars == <> + +Init == + /\ writePhase = "idle" + /\ reconcilePhase = "none" + /\ changesPinged = FALSE + /\ sideEffectsApplied = FALSE + /\ readerSawPing = FALSE + +BeginPerform == + /\ writePhase = "idle" + /\ writePhase' = "inPerform" + /\ UNCHANGED <> + +Commit == + /\ writePhase = "inPerform" + /\ writePhase' = "committed" + /\ reconcilePhase' = "invalidating" + /\ UNCHANGED <> + +StepInvalidate == + /\ reconcilePhase = "invalidating" + /\ reconcilePhase' = "reminders" + /\ UNCHANGED <> + +StepReminders == + /\ reconcilePhase = "reminders" + /\ reconcilePhase' = "widgets" + /\ UNCHANGED <> + +StepWidgets == + /\ reconcilePhase = "widgets" + /\ reconcilePhase' = "done" + /\ sideEffectsApplied' = TRUE + /\ UNCHANGED <> + +PingChanges == + /\ writePhase = "committed" + /\ IF Implementation = "broken" + THEN TRUE + ELSE reconcilePhase = "done" + /\ changesPinged' = TRUE + /\ UNCHANGED <> + +ReaderRefresh == + /\ changesPinged + /\ readerSawPing' = TRUE + /\ UNCHANGED <> + +ResetPath == + /\ writePhase = "committed" + /\ writePhase' = "idle" + /\ reconcilePhase' = "none" + /\ changesPinged' = FALSE + /\ sideEffectsApplied' = FALSE + /\ readerSawPing' = FALSE + +Next == + \/ BeginPerform + \/ Commit + \/ StepInvalidate + \/ StepReminders + \/ StepWidgets + \/ PingChanges + \/ ReaderRefresh + \/ ResetPath + +Fairness == + /\ WF_vars(BeginPerform) + /\ WF_vars(Commit) + /\ WF_vars(StepInvalidate) + /\ WF_vars(StepReminders) + /\ WF_vars(StepWidgets) + /\ WF_vars(PingChanges) + /\ WF_vars(ReaderRefresh) + /\ WF_vars(ResetPath) + +Spec == Init /\ [][Next]_vars /\ Fairness + +TypeOK == + /\ writePhase \in WritePhases + /\ reconcilePhase \in ReconcilePhases + /\ changesPinged \in BOOLEAN + /\ sideEffectsApplied \in BOOLEAN + /\ readerSawPing \in BOOLEAN + +NoChangesBeforeReconcileDone == + (Implementation = "current") => + (changesPinged => reconcilePhase = "done") + +BrokenNoEarlyPing == + changesPinged => reconcilePhase = "done" + +ReaderSeesAppliedSideEffects == + readerSawPing => sideEffectsApplied + +==== diff --git a/Where/Specifications/PostWriteReconcile/README.md b/Where/Specifications/PostWriteReconcile/README.md new file mode 100644 index 00000000..9feb36e3 --- /dev/null +++ b/Where/Specifications/PostWriteReconcile/README.md @@ -0,0 +1,35 @@ +# Post-write reconcile + +Models the intended contract in [`DayJournal.reconcileAfterDayChange()`](../../WhereCore/Sources/Journal/DayJournal.swift): +commit, then full fan-out (invalidate → reminders → issue alerts → widgets), then +`changes()` readers observe applied side effects. + +## Correspondence + +| Model | Production | +| --- | --- | +| `writePhase` | `store.perform` transaction | +| `reconcilePhase` | sequential fan-out steps | +| `changesPinged` | `StoreChangeBroadcaster.send()` | +| `sideEffectsApplied` | badge/widgets honest | +| `readerSawPing` | subscriber refresh | + +## Properties + +- `NoChangesBeforeReconcileDone` — canonical path only (`Implementation = "current"`) +- `ReaderSeesAppliedSideEffects` +- `BrokenNoEarlyPing` — negative control + +## Result + +**Verified for these model bounds and assumptions** on `Current.cfg` for the +canonical manual-day path. `Broken.cfg` falsifies `BrokenNoEarlyPing`. + +Swift guards: [`DayJournalTests.addManualDayReconcilesAndPublishes`](../../WhereCore/Tests/DayJournalTests.swift), +[`DayJournalTests.ingestPersistsAndFansOutOnce`](../../WhereCore/Tests/DayJournalTests.swift). + +Out of model until routed: `DailySummaryReconciler`, `setPrimaryRegions` (see +[`Where/TODOs.md`](../../TODOs.md) with links here). Dismiss/restore uses +widget-less `reconcileIssueState()` by design. + +Run: `./tla-check PostWriteReconcile` diff --git a/Where/Specifications/PostWriteReconcile/manifest.json b/Where/Specifications/PostWriteReconcile/manifest.json new file mode 100644 index 00000000..3b73265f --- /dev/null +++ b/Where/Specifications/PostWriteReconcile/manifest.json @@ -0,0 +1,16 @@ +{ + "module": "PostWriteReconcile.tla", + "cases": [ + { + "name": "broken", + "config": "Broken.cfg", + "expect": "fail", + "outputContains": "Invariant BrokenNoEarlyPing is violated." + }, + { + "name": "current", + "config": "Current.cfg", + "expect": "pass" + } + ] +} diff --git a/Where/WhereCore/Sources/Journal/DayJournal.swift b/Where/WhereCore/Sources/Journal/DayJournal.swift index dfd63c04..40c9e60f 100644 --- a/Where/WhereCore/Sources/Journal/DayJournal.swift +++ b/Where/WhereCore/Sources/Journal/DayJournal.swift @@ -73,7 +73,7 @@ public actor DayJournal { public func ingest(_ sample: LocationSample) async throws { try await store.perform { try await store.add(sample: sample) } - await widgets.publishAfterIngest(of: sample) + await reconcileAfterDayChange() } /// Persist many samples in a *single* transaction, rebuilding the widget @@ -91,14 +91,14 @@ public actor DayJournal { } } } - await widgets.publish() + await reconcileAfterDayChange() } // MARK: - Retroactive entry public func addManualSample(_ sample: LocationSample) async throws { try await store.perform { try await store.add(sample: sample) } - await widgets.publish() + await reconcileAfterDayChange() } public func addManualDay( diff --git a/Where/WhereCore/Tests/DayJournalTests.swift b/Where/WhereCore/Tests/DayJournalTests.swift index aad946b6..d7c3cf1b 100644 --- a/Where/WhereCore/Tests/DayJournalTests.swift +++ b/Where/WhereCore/Tests/DayJournalTests.swift @@ -109,16 +109,17 @@ struct DayJournalTests { ) } - @Test func ingestPersistsAndPublishesOnce() async throws { + @Test func ingestPersistsAndFansOutOnce() async throws { let h = try Self.makeHarness(now: { WhereCoreTestSupport.iso("2026-03-15T20:00:00-07:00") }) try await h.journal.ingest(sample(at: "2026-03-15T12:00:00-07:00")) let report = try await h.reader.yearReport(for: 2026) #expect(report.totals == [.california: 1]) + #expect(await h.reminders.reconcileCount == 1) #expect(await h.widgets.publishCount == 1) } - @Test func bulkIngestPersistsEverySampleAndPublishesOnce() async throws { + @Test func bulkIngestPersistsEverySampleAndFansOutOnce() async throws { let h = try Self.makeHarness() try await h.journal.ingest([ sample(at: "2026-01-10T12:00:00-08:00"), @@ -133,6 +134,7 @@ struct DayJournalTests { let report = try await h.reader.yearReport(for: 2026) #expect(report.totals == [.california: 2, .newYork: 1]) + #expect(await h.reminders.reconcileCount == 1) #expect(await h.widgets.publishCount == 1) } @@ -253,7 +255,7 @@ struct DayJournalTests { try await h.journal.clearYear(2026) #expect(try await h.reader.yearReport(for: 2026).days.isEmpty) - #expect(await h.reminders.reconcileCount == 1) + #expect(await h.reminders.reconcileCount == 2) } @Test func eraseAllDataWipesEveryYearAndReconciles() async throws { @@ -266,7 +268,7 @@ struct DayJournalTests { for year in [2024, 2025, 2026] { #expect(try await h.reader.yearReport(for: year).days.isEmpty) } - #expect(await h.reminders.reconcileCount == 1) + #expect(await h.reminders.reconcileCount == 4) } @Test func evidenceRoundTrips() async throws { From c65faf394eadf612686e48e2d6aea92f3115d695 Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:39:19 -0700 Subject: [PATCH 07/14] Add StorePerformSerialization TLA+ specification Confirmatory model for at-most-one outermost perform, same-task nesting, and FIFO waiter ordering. SwiftDataStoreTests cites the AtMostOneOutermost property. Co-authored-by: Cursor --- .../StorePerformSerialization/Broken.cfg | 10 ++ .../StorePerformSerialization/Current.cfg | 11 ++ .../StorePerformSerialization/README.md | 27 ++++ .../StorePerformSerialization.tla | 128 ++++++++++++++++++ .../StorePerformSerialization/manifest.json | 16 +++ .../WhereCore/Tests/SwiftDataStoreTests.swift | 10 +- 6 files changed, 198 insertions(+), 4 deletions(-) create mode 100644 Where/Specifications/StorePerformSerialization/Broken.cfg create mode 100644 Where/Specifications/StorePerformSerialization/Current.cfg create mode 100644 Where/Specifications/StorePerformSerialization/README.md create mode 100644 Where/Specifications/StorePerformSerialization/StorePerformSerialization.tla create mode 100644 Where/Specifications/StorePerformSerialization/manifest.json diff --git a/Where/Specifications/StorePerformSerialization/Broken.cfg b/Where/Specifications/StorePerformSerialization/Broken.cfg new file mode 100644 index 00000000..65d394d6 --- /dev/null +++ b/Where/Specifications/StorePerformSerialization/Broken.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec + +CONSTANTS + Implementation = "broken" + +INVARIANTS + TypeOK + AtMostOneOutermost + +CHECK_DEADLOCK FALSE diff --git a/Where/Specifications/StorePerformSerialization/Current.cfg b/Where/Specifications/StorePerformSerialization/Current.cfg new file mode 100644 index 00000000..445792fe --- /dev/null +++ b/Where/Specifications/StorePerformSerialization/Current.cfg @@ -0,0 +1,11 @@ +SPECIFICATION Spec + +CONSTANTS + Implementation = "current" + +INVARIANTS + TypeOK + AtMostOneOutermost + NestedSameTaskNoWait + +CHECK_DEADLOCK FALSE diff --git a/Where/Specifications/StorePerformSerialization/README.md b/Where/Specifications/StorePerformSerialization/README.md new file mode 100644 index 00000000..2cf33f16 --- /dev/null +++ b/Where/Specifications/StorePerformSerialization/README.md @@ -0,0 +1,27 @@ +# Store perform serialization + +Confirmatory model for [`SwiftDataStore.perform`](../../WhereCore/Sources/Persistence/SwiftDataStore.swift): +at most one outermost transaction, nested same-task reuse, FIFO waiters. + +## Correspondence + +| Model | Production | +| --- | --- | +| `isTransacting` | exclusive gate | +| `waiterCount` | `transactionWaiters` | +| `taskAPhase` / `taskBPhase` | concurrent outer callers | +| `nestedDepth` | `@TaskLocal activeTransactionStores` reuse | + +## Properties + +- `AtMostOneOutermost` +- `NestedSameTaskNoWait` + +## Result + +**Verified for these model bounds and assumptions** on `Current.cfg`. +`Broken.cfg` (concurrent outermost without waiting) falsifies `AtMostOneOutermost`. + +Swift guard: [`SwiftDataStoreTests.concurrentOutermostPerformsSerializeAndAllCommit`](../../WhereCore/Tests/SwiftDataStoreTests.swift). + +Run: `./tla-check StorePerformSerialization` diff --git a/Where/Specifications/StorePerformSerialization/StorePerformSerialization.tla b/Where/Specifications/StorePerformSerialization/StorePerformSerialization.tla new file mode 100644 index 00000000..8394dec6 --- /dev/null +++ b/Where/Specifications/StorePerformSerialization/StorePerformSerialization.tla @@ -0,0 +1,128 @@ +---- MODULE StorePerformSerialization ---- +EXTENDS Integers + +CONSTANTS Implementation + +ASSUME Implementation \in {"current", "broken"} + +TaskPhases == {"idle", "waiting", "inPerform", "committed"} + +VARIABLES + isTransacting, + waiterCount, + taskAPhase, + taskBPhase, + nestedDepth, + aCommitted, + bCommitted + +vars == <> + +Init == + /\ isTransacting = FALSE + /\ waiterCount = 0 + /\ taskAPhase = "idle" + /\ taskBPhase = "idle" + /\ nestedDepth = 0 + /\ aCommitted = FALSE + /\ bCommitted = FALSE + +BeginOuterA == + /\ taskAPhase = "idle" + /\ IF isTransacting + THEN /\ taskAPhase' = "waiting" + /\ waiterCount' = waiterCount + 1 + /\ UNCHANGED <> + ELSE /\ taskAPhase' = "inPerform" + /\ isTransacting' = TRUE + /\ UNCHANGED <> + +BeginOuterB == + /\ taskBPhase = "idle" + /\ IF /\ Implementation = "broken" + /\ taskAPhase = "inPerform" + THEN /\ taskBPhase' = "inPerform" + /\ UNCHANGED <> + ELSE IF isTransacting + THEN /\ taskBPhase' = "waiting" + /\ waiterCount' = waiterCount + 1 + /\ UNCHANGED <> + ELSE /\ taskBPhase' = "inPerform" + /\ isTransacting' = TRUE + /\ UNCHANGED <> + +BeginNestedSameTask == + /\ taskAPhase = "inPerform" + /\ nestedDepth < 1 + /\ nestedDepth' = nestedDepth + 1 + /\ UNCHANGED <> + +CommitA == + /\ taskAPhase = "inPerform" + /\ nestedDepth = 0 + /\ taskAPhase' = "committed" + /\ aCommitted' = TRUE + /\ IF waiterCount > 0 + THEN /\ waiterCount' = waiterCount - 1 + /\ taskBPhase' = "inPerform" + /\ UNCHANGED isTransacting + ELSE /\ isTransacting' = FALSE + /\ UNCHANGED <> + /\ UNCHANGED <> + +CommitB == + /\ taskBPhase = "inPerform" + /\ taskBPhase' = "committed" + /\ bCommitted' = TRUE + /\ IF waiterCount > 0 + THEN /\ waiterCount' = waiterCount - 1 + /\ taskAPhase' = "inPerform" + /\ UNCHANGED isTransacting + ELSE /\ isTransacting' = FALSE + /\ UNCHANGED <> + /\ UNCHANGED <> + +EndNested == + /\ nestedDepth > 0 + /\ nestedDepth' = nestedDepth - 1 + /\ UNCHANGED <> + +Next == + \/ BeginOuterA + \/ BeginOuterB + \/ BeginNestedSameTask + \/ CommitA + \/ CommitB + \/ EndNested + +Fairness == + /\ WF_vars(BeginOuterA) + /\ WF_vars(BeginOuterB) + /\ WF_vars(BeginNestedSameTask) + /\ WF_vars(CommitA) + /\ WF_vars(CommitB) + /\ WF_vars(EndNested) + +Spec == Init /\ [][Next]_vars /\ Fairness + +TypeOK == + /\ isTransacting \in BOOLEAN + /\ waiterCount \in 0..2 + /\ taskAPhase \in TaskPhases + /\ taskBPhase \in TaskPhases + /\ nestedDepth \in 0..1 + /\ aCommitted \in BOOLEAN + /\ bCommitted \in BOOLEAN + +AtMostOneOutermost == + (taskAPhase = "inPerform" /\ nestedDepth = 0) => + taskBPhase \notin {"inPerform"} + +NestedSameTaskNoWait == + nestedDepth > 0 => taskAPhase = "inPerform" + +AllCommit == + aCommitted /\ bCommitted + +==== diff --git a/Where/Specifications/StorePerformSerialization/manifest.json b/Where/Specifications/StorePerformSerialization/manifest.json new file mode 100644 index 00000000..41b11ba6 --- /dev/null +++ b/Where/Specifications/StorePerformSerialization/manifest.json @@ -0,0 +1,16 @@ +{ + "module": "StorePerformSerialization.tla", + "cases": [ + { + "name": "broken", + "config": "Broken.cfg", + "expect": "fail", + "outputContains": "Invariant AtMostOneOutermost is violated." + }, + { + "name": "current", + "config": "Current.cfg", + "expect": "pass" + } + ] +} diff --git a/Where/WhereCore/Tests/SwiftDataStoreTests.swift b/Where/WhereCore/Tests/SwiftDataStoreTests.swift index 641c3eaf..78dfd06f 100644 --- a/Where/WhereCore/Tests/SwiftDataStoreTests.swift +++ b/Where/WhereCore/Tests/SwiftDataStoreTests.swift @@ -56,10 +56,12 @@ struct SwiftDataStoreTests { #expect(await firstPing(stream, within: .seconds(2))) } - /// Two (or more) *outermost* `perform` calls issued from independent tasks - /// must be serialized. Because `perform`'s block is `async` and the store is - /// an `actor`, naive reentrancy once let a concurrent top-level `perform` - /// observe the in-flight peer, take the nested-reuse branch, and then trap in + /// Guards TLC property `AtMostOneOutermost` in + /// `Where/Specifications/StorePerformSerialization`. Two outermost + /// `perform` calls on different tasks must be serialized. Because + /// `perform`'s block is `async` and the store is an `actor`, naive + /// reentrancy once let a concurrent top-level `perform` observe the + /// in-flight peer, take the nested-reuse branch, and then trap in /// `mutationContext()` when the real owner cleared the peer out from under it /// (the shipped crash). Every transaction must now run to completion one at a /// time, and every write must commit. From 86a4df8a1582dfc0d1e40a7cb561456f828a68f4 Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:39:20 -0700 Subject: [PATCH 08/14] Extend IntentServicesTests for handoff clear/resume Add clearWhileParkedResumesOnTheNextInstall, cited by the IntentServicesHandoff TLA+ spec's parked-install contract. Co-authored-by: Cursor --- .../WhereIntents/Tests/IntentServicesTests.swift | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Where/WhereIntents/Tests/IntentServicesTests.swift b/Where/WhereIntents/Tests/IntentServicesTests.swift index 64b02d77..5913d3bf 100644 --- a/Where/WhereIntents/Tests/IntentServicesTests.swift +++ b/Where/WhereIntents/Tests/IntentServicesTests.swift @@ -63,4 +63,20 @@ struct IntentServicesTests { #expect(resolved.journal === second.journal) #expect(resolved.journal !== first.journal) } + + /// TLC property `AfterClearMustPark`: after `clear()`, a parked intent must + /// resume on the next `install(_:)` rather than observing a cleared stack. + @Test func clearWhileParkedResumesOnTheNextInstall() async throws { + let handoff = IntentServices() + let parked = Task { try await handoff.current() } + try await waitUntil { await handoff.waiterCount == 1 } + + await handoff.clear() + + let replacement = try makeStack() + await handoff.install(replacement) + + let resolved = try await parked.value + #expect(resolved.journal === replacement.journal) + } } From 7c09b6b4303c69235db244cc7b0f1936c51c235c Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:39:20 -0700 Subject: [PATCH 09/14] Update Where TODOs and AGENTS for TLA+ expansion Mark tracking worker and ingest fan-out fixes done, cross-link PostWriteReconcile from remaining fan-out gaps, file P2 LaunchLifecycle and scope-exclusion models, and add ./tla-check pointer under Testing. Co-authored-by: Cursor --- Where/AGENTS.md | 4 ++++ Where/TODOs.md | 12 +++++++----- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/Where/AGENTS.md b/Where/AGENTS.md index 97106ed7..e1d76b0e 100644 --- a/Where/AGENTS.md +++ b/Where/AGENTS.md @@ -284,6 +284,10 @@ surfaces survive at near-Release speed. Options: `./Where/install --help`. Root [testing conventions](../AGENTS.md#testing) apply. What's specific here: +- **Formal protocol specs** live under [`Specifications/`](Specifications/); run + them locally with [`./tla-check`](../tla-check) (opt-in, not CI). Each folder + holds a `.tla` model, TLC configs, a `manifest.json`, and a README tying the + model to production code and cited Swift tests. - Test bundles run in `StuffTestHost` via the `unitTests` helper in `Project.swift` and link `TestHostSupport` (`show(_:perform:)`, `waitFor`). - Use `ScriptedLocationSource` and `SwiftDataStore.inMemory()` — never diff --git a/Where/TODOs.md b/Where/TODOs.md index 7c612564..fc6138c6 100644 --- a/Where/TODOs.md +++ b/Where/TODOs.md @@ -17,7 +17,7 @@ The item format and the placement rule live in the root - fix(WhereCore): Nothing gets recorded on a day with no movement — presumably because background updates ride on GPS. Any way to guarantee a daily boot outside of GPS? (human) ## P0s (Must do) -- fix(WhereCore) [needs-design]: `DailySummaryReconciler.reconcile()` is absent from the post-day-change fan-out. Its only caller is `configure` (`DailySummaryReconciler.swift:45`), and `DayJournal.reconcileAfterDayChange()` (`:63`) fans out to issue state and widgets only — so the daily notification body stays stale until a foreground re-`configure`. Add it to the fan-out (the GPS ingest hook, `reconcileAfterDayChange()`, backup `onImport`), or document the foreground-only policy. (audit 2026-07-26) +- fix(WhereCore) [needs-design]: `DailySummaryReconciler.reconcile()` is absent from the post-day-change fan-out. Its only caller is `configure` (`DailySummaryReconciler.swift:45`), and `DayJournal.reconcileAfterDayChange()` (`:63`) fans out to issue state and widgets only — so the daily notification body stays stale until a foreground re-`configure`. Add it to the fan-out (the GPS ingest hook, `reconcileAfterDayChange()`, backup `onImport`), or document the foreground-only policy. Verified canonical fan-out ordering in [`Specifications/PostWriteReconcile`](Specifications/PostWriteReconcile/README.md); summary reconciler still out of model scope until routed. (audit 2026-07-26) - test(WhereCore) [quick-win]: Mutate data and assert the summary notification body updates without a re-`configure`. (audit 2026-07-26) - perf(WhereCore) [needs-design]: Performance pass — how often is the app booting? Can we only do it on changes of, say, 1 km or more? (human) @@ -25,18 +25,18 @@ The item format and the placement rule live in the root - feat(Where) [needs-design]: Add an optional onboarding step that backfills the current year from the GPS metadata of photos in the user's library. `OnboardingView.Phase` currently moves from region selection/customization directly to location permission (`WhereUI/Sources/Onboarding/OnboardingView.swift:30`), while `DayJournal.ingest(_:)` is the existing bulk sample path (`WhereCore/Sources/Journal/DayJournal.swift:82`). Design a PhotoKit-backed importer that requests access only after an explicit opt-in, reads location and capture time locally without uploading photo contents, previews what will be added, records photo-derived provenance rather than treating it as live GPS, deduplicates repeat imports, and makes skipping the screen frictionless. (human 2026-08-03) - refactor(WhereCore) [needs-design]: Scope diagnostic emission so Flyover's unactivated sibling demo world cannot write its activity through the process-global `WhereLog` / `Periscope.shared` facade into the active real scope's durable diagnostic store. `WhereFlyoverWorld.build()` correctly gives the sibling a private `Periscope` and never starts its sink, but static `WhereLog` channels still bypass that injection; carry the scope's logging system through services/models or add a task-/environment-scoped routing context before treating Flyover's diagnostic activity as isolated. Domain data, preferences, widgets, notifications, and location remain in memory/no-op already. (`WhereUI/Sources/Developer/Flyover/WhereFlyoverWorld.swift`, `WhereCore/Sources/Logging/WhereLog.swift`; agent 2026-07-29) - fix(WhereUI) [quick-win]: `CalendarDay.displayDate` resolves through `Calendar.current` (`DateRangeFormatting.swift:33`), so every day label that flows through it — relabel, logged days, resolution details, the region drill-in — renders a wrong date on a non-Gregorian device: `startOfDay(in:)` interprets the day's Gregorian Y-M-D as *that* calendar's components, so a Buddhist-era device resolves 2026-07-26 to a date ~543 years off. `DateRangeFormatting.abbreviated` (`:6`, `:19`) and `PresenceTimeline.stints` (`PresenceTimeline.swift:37`) also *default* to `.current`, and `PresenceTimelineList` (`:12`) doesn't pass `report.calendar`. Take an explicit calendar (Gregorian + current time zone) in the helper and thread the report's calendar from the call sites. The `where.gregorian_calendar` Bumper rule that should catch this is blind to the implicit-member form — filed in the root [`TODOs.md`](../TODOs.md). (audit 2026-07-26) -- fix(WhereCore) [needs-design]: `WhereServices.setPrimaryRegions(_:)` (`:285`) commits atomically but skips `DayJournal.reconcileAfterDayChange()` — widgets/reminders/summary don't refresh until foreground/configure. Route picker commits through the unified fan-out, or document the intentional deferral. (audit 2026-07-26) +- fix(WhereCore) [needs-design]: `WhereServices.setPrimaryRegions(_:)` (`:285`) commits atomically but skips `DayJournal.reconcileAfterDayChange()` — widgets/reminders/summary don't refresh until foreground/configure. Route picker commits through the unified fan-out, or document the intentional deferral. Out of scope for [`PostWriteReconcile`](Specifications/PostWriteReconcile/README.md) until routed. (audit 2026-07-26) - fix(WhereCore) [needs-design]: Soft-delete untracked regions. `SwiftDataStore.setTrackedRegion(false)` (`:756`, in-source TODO at `:773`) and `setPrimaryRegions` (`:833`) hard-delete the row, which drops the region from the attributor's load set — so re-aggregating a past year re-attributes that region's GPS days to `.other`. The `SwiftDataStore` TODO filed this as "when the region picker ships"; it has shipped, and both the onboarding picker and the Settings region editor now reach the delete, so this is user-reachable rather than latent. Retain the row for attribution and hide it from the pickers instead. (audit 2026-07-26) -- fix(WhereCore) [needs-design]: `DayJournal.ingest(_:)` (`:70`), the bulk ingest (`:82`), and `addManualSample` (`:93`) publish widgets but skip the reminder/issue reconcile, so a presence change made through them leaves the badge and reminders stale. Route them through the fan-out, or mark them `@_spi(Testing)` if they aren't production write paths. (audit 2026-07-26) +- fix(WhereCore) [needs-design]: ~~`DayJournal.ingest(_:)` (`:70`), the bulk ingest (`:82`), and `addManualSample` (`:93`) publish widgets but skip the reminder/issue reconcile~~ — **fixed:** all three now route through `reconcileAfterDayChange()` (see [`PostWriteReconcile`](Specifications/PostWriteReconcile/README.md)). Remaining fan-out gaps: `DailySummaryReconciler` (P0 above) and `setPrimaryRegions` (above). (audit 2026-07-26; fixed 2026-08-04) - fix(WhereCore) [needs-design]: A durable outbox save failure is logged and swallowed (`LocationOutbox.swift:86`, `LocationIngestor.swift:344`), so a process death loses the in-memory sample with nothing to replay on relaunch. Handle the degraded state honestly rather than continuing as though the sample were durable. (audit 2026-07-26) - test(WhereCore) [quick-win]: Cover outbox *save* failure with a failing-outbox double; only load failure is covered today. (audit 2026-07-26) - fix(WhereCore) [needs-design]: The retry queue evicts FIFO at capacity and drops samples with a warning only (`LocationIngestor.swift:349`). Decide the capacity policy and whether eviction warrants user-visible degradation, then document it. (audit 2026-07-26) - fix(WhereUI) [quick-win]: `PresenceTimelineList` returns `[]` whenever `report.report` is nil (`:12`), so the Timeline segment of Your Year renders the "no stays" empty state while the year is still loading (and during a year switch) — unlike the Calendar segment beside it, which gates on `loadState`. (audit 2026-07-26) - refactor(WhereUI) [needs-design]: Extract a shared `ReportLoadGate`. The same `YearReportModel.loadState` gate is copy-pasted across `LocationsView.swift:60`, `ElsewhereView.swift:50`, `ResolutionView.swift:58`, and `CalendarContentView.swift:60`, and `PresenceTimelineList` skipped it entirely (above). One gate view would cover all five. (audit 2026-07-26) - fix(WhereUI) [quick-win]: The Elsewhere entry card renders raw inflection markup instead of an agreed region count — it shows literally `^[3 region](inflect: true)`. `locations.elsewhere.subtitle` is authored for automatic grammar agreement (`^[%lld region](inflect: true)`), but the string-catalog compiler passes that markup through **verbatim** into the compiled `Localizable.strings` (unlike a real plural such as `primary.elsewhereOnly.description`, which compiles to an `NSStringLocalizedFormatKey` dict), and flattening the resource to a `String` never runs the inflection engine. Pre-existing — the catalog entry is byte-identical on `main` and predates the String Catalog symbol migration. Fix by either rendering the resource directly so SwiftUI applies inflection (`Text(.locationsElsewhereSubtitle(regionCount))` in `ElsewhereSummaryCard`, dropping the `WhereFormat` hop) or replacing the markup with an explicit plural variation. `WhereFormatTests.elsewhereCardSubtitleInflectsTheRegionCount` pins the expected output behind `withKnownIssue`, so it trips as soon as this is fixed. The bug is also baked into the `locations.Loaded_iPad.png` reference (ledgered in the broken-snapshots cluster below) — re-record that image when this lands. (agent) -- fix(WhereUI) [needs-design]: Serialize `WhereSession.trackingEnabled` mutations. The setter spawns an unserialized `Task` per assignment (`WhereSession.swift:461`), and `reconcileTracking()` reads intent before awaiting `ingestor.start()` then unconditionally publishes `isTracking = true` when the await returns (`:302`), so a newer stop can finish during that await and leave preferences + the ingestor off while the UI mirror says on. The executable [`TrackingReconciliation` TLA+ pilot](Specifications/TrackingReconciliation/README.md) reproduces that counterexample and checks a one-worker coalescing design; implement that design (or a generation token) and re-check intent before publishing. (audit 2026-07-26; modeled 2026-08-02) +- fix(WhereUI) [needs-design]: ~~Serialize `WhereSession.trackingEnabled` mutations.~~ **Fixed:** coalesced tracking worker on ``WhereSession`` (see [`Specifications/TrackingReconciliation`](Specifications/TrackingReconciliation/README.md)). (audit 2026-07-26; fixed 2026-08-04) - fix(WhereUI) [needs-design]: Split the toggle binding — `wantsTracking` for user intent vs `isTracking` for effective GPS state. `wantsTracking` already exists internally and is persisted, but the public `trackingEnabled` binds effective state for both read *and* write, so the switch animates back on its own while a start is in flight. (audit 2026-07-26) - - test(WhereUI) [quick-win]: `WhereSessionTrackingTests.newerStopWinsOverInFlightStart` now holds the location source at the modeled await and deterministically reproduces the stale publication behind `withKnownIssue`; remove the known-issue wrapper when the worker fix lands. (audit 2026-07-26; guarded 2026-08-02) + - test(WhereUI) [quick-win]: ~~`WhereSessionTrackingTests.newerStopWinsOverInFlightStart` … remove the known-issue wrapper when the worker fix lands.~~ **Done** — passes cleanly against the coalesced worker. (audit 2026-07-26; fixed 2026-08-04) - refactor(WhereUI) [needs-design]: Split `WhereSession` into an always-on coordinator + a presentation view-model whose lifetime scopes its subscriptions. **Partial progress (July 2026):** `YearReportModel` is now scene-scoped in `MainTabs` — `activate()` / `deactivate()` on `scenePhase` drive `observeDataChanges()` and refresh, closing the headless-relaunch rescan leak that previously wired the subscription through launch `syncAuth`. `ResolveModel`, `BackupModel`, and `RemindersSettingsModel` are already view-scoped. Remaining: the coordinator is still ~460 lines mixing tracking intent, authorization, reset, and region-style mirrors; finish extracting presentation collaborators and drive any leftover reactive work from scene lifetime. (agent) - test(WhereUI) [quick-win]: `ManualDayView`'s range mode has no test coverage — including its capture-only code. The deleted `manualDayViewHostsAddModes` hosted a *range-prefilled* add (two `DatePicker`s), but the `addPrefill` snapshot case in `ManualDayView.swift` is a single day (`start == end` → `dateSpan = .singleDay`), so no test ever renders the `.range` branch — live or stand-in. The range stand-in code has never executed, and the From/Through picker row rendering is unpinned. Fix: add an `AddRange` snapshot case with a multi-day `MissingDayRange` prefill (the Resolve backfill flow the deleted test existed for). (From the July 2026 snapshot-testing PR review.) - test(WhereUI) [needs-design]: `RegionMapView`'s live `Map` branch is no longer constructed by any test. The deleted `regionMapViewHosts` mounted the real MapKit `Map` (polygon building via `clLocationCoordinates`, `mapStyle`); under capture the view always takes the `SnapshotMapStandIn` branch, so a crash or regression in the production map path — which every real user sees — would ship untested. The stand-in substitution is what the framework carve-out sanctions; the gap is purely coverage. Fix: keep one lightweight hosting test for the live branch in `WhereUITests` (this specific surface is the exception the "no hosting smoke tests" rule shouldn't swallow) — until then, this entry records the accepted gap. (From the July 2026 snapshot-testing PR review.) @@ -65,6 +65,8 @@ The item format and the placement rule live in the root - fix(WhereUI): broken-snapshots: `locations.Loaded_iPad.png` bakes in raw inflection markup — the Elsewhere card's subtitle renders literally as `^[3 region](inflect: true)`. This is the `locations.elsewhere.subtitle` P1 filed above, now pinned as a reference; recorded here so the image isn't mistaken for correct output, and so that reference is re-recorded when the fix lands. (pr#101 review) ## P2s (Nice to have) +- design(WhereUI) [needs-design]: TLA+ — LaunchLifecycle narrow slice (undetermined promotion + single-drive invariant). Fuzz coverage exists; model one claim before broader controller rewrite. (agent 2026-08-04) +- design(WhereUI) [needs-design]: TLA+ — Scope mutual exclusion (at most one live scope / container over a store file). Ties to controller state-machine rewrite. (agent 2026-08-04) - feat(WhereUI) [needs-design]: Give the app a branded launch screen. `UILaunchScreen` is an empty dictionary (`Project.swift`), so the pre-main frame is plain white. Measured from a fresh-install simulator recording, a first run reads as ~1.7s of white → ~0.25s of the dark `LaunchSplashView` → the light onboarding screen, so the splash registers as a quarter-second dark blip between two light screens rather than as the app opening. A launch screen matching the splash's background + icon would make that continuous. Note this is the right layer to fix it at: the splash's own `minimumSplashDuration` hold deliberately gates only the `.ready` reveal, not a gate transition like onboarding, so lengthening the hold would just delay interactive UI. (agent) - refactor(WhereUI) [needs-design]: Make the scene-scoped model wiring compiler-checked rather than an `@Environment` lookup that fails silently. `WhereSession` (the always-on coordinator) is read from the environment, so a screen mounted without a parent injecting it resolves to a runtime fallback/precondition instead of a compile error. The scoped models (`YearReportModel`, `ResolveModel`, `BackupModel`, `RemindersSettingsModel`) are already constructor-injected; explore threading the coordinator the same way (or a non-defaulting typed `EnvironmentKey`) so a broken wiring can't build. Follow-up from the `WhereSession` split. (agent) - refactor(WhereUI) [needs-design]: Split `YearReportModel` further. Post-split it still fuses several roles for the selected year: the loaded report + everything derived from it (ranking, missing days, calendar inputs, tracked-day count), the Resolve badge *count*, the day-write intents (`setManualDay(s)`, `overrideDay`, `clearManualDay`, `clearSelectedYear`), and the Elsewhere drill-in reads (`days(in:)`, `locations(in:)`, `representativeCoordinates()`). The read-only presentation state and the write-intent/drill-in surface could be separate collaborators so a view only holds what it uses. Follow-up from the `WhereSession` split. (agent) From 2566abf4e905f4dc7210a5d07d4ed6b1ff8de9b7 Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:51:32 -0700 Subject: [PATCH 10/14] Add P2 TLA+ specs: LaunchLifecycle and ScopeExclusivity LaunchLifecycle models undetermined promotion, memo-preserving re-drive, and foreground-only capture-today. ScopeExclusivity models at-most-one active scope and live real container (complementing LogRouting sink ownership). Both confirmatory on Current.cfg; ./tla-check now runs eight specs. Co-authored-by: Cursor --- .../Specifications/LaunchLifecycle/Broken.cfg | 7 + .../LaunchLifecycle/Current.cfg | 13 ++ .../LaunchLifecycle/LaunchLifecycle.tla | 141 ++++++++++++++++++ .../Specifications/LaunchLifecycle/README.md | 45 ++++++ .../LaunchLifecycle/manifest.json | 16 ++ .../ScopeExclusivity/Broken.cfg | 7 + .../ScopeExclusivity/Current.cfg | 13 ++ .../Specifications/ScopeExclusivity/README.md | 45 ++++++ .../ScopeExclusivity/ScopeExclusivity.tla | 108 ++++++++++++++ .../ScopeExclusivity/manifest.json | 16 ++ Where/TODOs.md | 3 - 11 files changed, 411 insertions(+), 3 deletions(-) create mode 100644 Where/Specifications/LaunchLifecycle/Broken.cfg create mode 100644 Where/Specifications/LaunchLifecycle/Current.cfg create mode 100644 Where/Specifications/LaunchLifecycle/LaunchLifecycle.tla create mode 100644 Where/Specifications/LaunchLifecycle/README.md create mode 100644 Where/Specifications/LaunchLifecycle/manifest.json create mode 100644 Where/Specifications/ScopeExclusivity/Broken.cfg create mode 100644 Where/Specifications/ScopeExclusivity/Current.cfg create mode 100644 Where/Specifications/ScopeExclusivity/README.md create mode 100644 Where/Specifications/ScopeExclusivity/ScopeExclusivity.tla create mode 100644 Where/Specifications/ScopeExclusivity/manifest.json diff --git a/Where/Specifications/LaunchLifecycle/Broken.cfg b/Where/Specifications/LaunchLifecycle/Broken.cfg new file mode 100644 index 00000000..fc674840 --- /dev/null +++ b/Where/Specifications/LaunchLifecycle/Broken.cfg @@ -0,0 +1,7 @@ +SPECIFICATION Spec +CONSTANTS + Implementation = "broken" +INVARIANT + TypeOK +INVARIANT + MemoNoDoubleRun diff --git a/Where/Specifications/LaunchLifecycle/Current.cfg b/Where/Specifications/LaunchLifecycle/Current.cfg new file mode 100644 index 00000000..33c9aa10 --- /dev/null +++ b/Where/Specifications/LaunchLifecycle/Current.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec +CONSTANTS + Implementation = "current" +INVARIANT + TypeOK +INVARIANT + SingleDrive +INVARIANT + MemoNoDoubleRun +INVARIANT + UndeterminedNoCaptureToday +INVARIANT + ForegroundCaptureBeforeReady diff --git a/Where/Specifications/LaunchLifecycle/LaunchLifecycle.tla b/Where/Specifications/LaunchLifecycle/LaunchLifecycle.tla new file mode 100644 index 00000000..3ed5f195 --- /dev/null +++ b/Where/Specifications/LaunchLifecycle/LaunchLifecycle.tla @@ -0,0 +1,141 @@ +---- MODULE LaunchLifecycle ---- +EXTENDS Integers + +CONSTANTS Implementation + +ASSUME Implementation \in {"current", "broken"} + +Reasons == {"undetermined", "userForeground"} +Phases == {"notStarted", "driving", "ready"} + +VARIABLES + reason, + phase, + driveActive, + memoSyncAuth, + memoReconcile, + captureTodayDone, + syncAuthRuns, + reconcileRuns + +vars == <> + +Init == + /\ reason = "undetermined" + /\ phase = "notStarted" + /\ driveActive = FALSE + /\ memoSyncAuth = FALSE + /\ memoReconcile = FALSE + /\ captureTodayDone = FALSE + /\ syncAuthRuns = 0 + /\ reconcileRuns = 0 + +StartDrive == + /\ phase = "notStarted" + /\ phase' = "driving" + /\ driveActive' = TRUE + /\ UNCHANGED <> + +RunSyncAuth == + /\ phase = "driving" + /\ driveActive + /\ IF Implementation = "current" + THEN memoSyncAuth = FALSE + ELSE TRUE + /\ memoSyncAuth' = TRUE + /\ syncAuthRuns' = syncAuthRuns + 1 + /\ UNCHANGED <> + +RunReconcileTracking == + /\ phase = "driving" + /\ driveActive + /\ IF Implementation = "current" + THEN memoReconcile = FALSE + ELSE TRUE + /\ memoReconcile' = TRUE + /\ reconcileRuns' = reconcileRuns + 1 + /\ UNCHANGED <> + +RunCaptureToday == + /\ phase = "driving" + /\ driveActive + /\ reason = "userForeground" + /\ ~captureTodayDone + /\ captureTodayDone' = TRUE + /\ UNCHANGED <> + +EnterForeground == + /\ reason = "undetermined" + /\ phase \in {"driving", "ready"} + /\ reason' = "userForeground" + /\ phase' = "driving" + /\ driveActive' = TRUE + /\ IF Implementation = "broken" + THEN /\ memoSyncAuth' = FALSE + /\ memoReconcile' = FALSE + ELSE UNCHANGED <> + /\ UNCHANGED <> + +ReachReady == + /\ phase = "driving" + /\ driveActive + /\ memoSyncAuth + /\ memoReconcile + /\ (reason = "undetermined" \/ captureTodayDone) + /\ phase' = "ready" + /\ driveActive' = FALSE + /\ UNCHANGED <> + +Stutter == + phase = "ready" + /\ UNCHANGED vars + +Next == + \/ StartDrive + \/ RunSyncAuth + \/ RunReconcileTracking + \/ RunCaptureToday + \/ EnterForeground + \/ ReachReady + \/ Stutter + +Fairness == + /\ WF_vars(StartDrive) + /\ WF_vars(RunSyncAuth) + /\ WF_vars(RunReconcileTracking) + /\ WF_vars(RunCaptureToday) + /\ WF_vars(EnterForeground) + /\ WF_vars(ReachReady) + +Spec == Init /\ [][Next]_vars /\ Fairness + +TypeOK == + /\ reason \in Reasons + /\ phase \in Phases + /\ driveActive \in BOOLEAN + /\ memoSyncAuth \in BOOLEAN + /\ memoReconcile \in BOOLEAN + /\ captureTodayDone \in BOOLEAN + /\ syncAuthRuns \in 0..4 + /\ reconcileRuns \in 0..4 + +SingleDrive == + ~driveActive \/ phase \in {"driving", "ready"} + +MemoNoDoubleRun == + /\ syncAuthRuns <= 1 + /\ reconcileRuns <= 1 + +UndeterminedNoCaptureToday == + reason = "undetermined" => ~captureTodayDone + +ForegroundCaptureBeforeReady == + phase = "ready" /\ reason = "userForeground" => captureTodayDone + +==== diff --git a/Where/Specifications/LaunchLifecycle/README.md b/Where/Specifications/LaunchLifecycle/README.md new file mode 100644 index 00000000..cdeacfdf --- /dev/null +++ b/Where/Specifications/LaunchLifecycle/README.md @@ -0,0 +1,45 @@ +# Launch lifecycle (narrow slice) + +Models the undetermined → foreground promotion path in +[`LifecycleRunner`](../../../Shared/LifecycleKit/Sources/LifecycleRunner.swift) +and [`RootView`](../../WhereUI/Sources/RootView.swift): a headless drive runs +background-safe trunk steps, `enterForeground()` promotes the reason, and the +re-drive skips memoized steps while running foreground-only work. + +## Correspondence + +| Model | Production | +| --- | --- | +| `reason` | `LifecycleReason` (`.undetermined` / `.userForeground`) | +| `memoSyncAuth`, `memoReconcile` | `LifecycleRunner.memo` — completed step IDs | +| `captureTodayDone` | `CaptureTodayStep` (`.foreground` only) | +| `driveActive` | at most one in-flight `drive()` task | +| `EnterForeground` | `LifecycleRunner.enterForeground()` | + +Background steps stand in for `sync-auth` and `reconcile-tracking`; the +foreground step stands in for `capture-today`. Gates, detached fan-out, and +teardown are out of scope for this narrow slice. + +## Properties + +- `SingleDrive` — one walk in flight at a time +- `MemoNoDoubleRun` — promotion re-drive skips completed background steps +- `UndeterminedNoCaptureToday` — foreground-only work waits for promotion +- `ForegroundCaptureBeforeReady` — promoted launch reaches ready only after + capture-today runs + +## Result + +**Verified for these model bounds and assumptions** on `Current.cfg`. +`Broken.cfg` (promotion clears memo and re-runs background steps) falsifies +`MemoNoDoubleRun`. + +Swift guards: + +- [`WhereLaunchTests.undeterminedLaunchDefersForegroundStepsUntilPromoted`](../../WhereUI/Tests/WhereLaunchTests.swift) +- [`LifecycleRunnerTests.promotionSkipsNodesCompletedInTheHeadlessDrive`](../../../Shared/LifecycleKit/Tests/LifecycleRunnerTests.swift) +- [`LifecycleRunnerTests.undeterminedLaunchRunsBackgroundNodesThenPromotesToForeground`](../../../Shared/LifecycleKit/Tests/LifecycleRunnerTests.swift) + +Broader launch state-machine rewrite remains tracked in [`Where/TODOs.md`](../../TODOs.md). + +Run: `./tla-check LaunchLifecycle` diff --git a/Where/Specifications/LaunchLifecycle/manifest.json b/Where/Specifications/LaunchLifecycle/manifest.json new file mode 100644 index 00000000..28ad5071 --- /dev/null +++ b/Where/Specifications/LaunchLifecycle/manifest.json @@ -0,0 +1,16 @@ +{ + "module": "LaunchLifecycle.tla", + "cases": [ + { + "name": "broken", + "config": "Broken.cfg", + "expect": "fail", + "outputContains": "Invariant MemoNoDoubleRun is violated." + }, + { + "name": "current", + "config": "Current.cfg", + "expect": "pass" + } + ] +} diff --git a/Where/Specifications/ScopeExclusivity/Broken.cfg b/Where/Specifications/ScopeExclusivity/Broken.cfg new file mode 100644 index 00000000..226c12bb --- /dev/null +++ b/Where/Specifications/ScopeExclusivity/Broken.cfg @@ -0,0 +1,7 @@ +SPECIFICATION Spec +CONSTANTS + Implementation = "broken" +INVARIANT + TypeOK +INVARIANT + NoOverlappingRealContainers diff --git a/Where/Specifications/ScopeExclusivity/Current.cfg b/Where/Specifications/ScopeExclusivity/Current.cfg new file mode 100644 index 00000000..b4c8ee34 --- /dev/null +++ b/Where/Specifications/ScopeExclusivity/Current.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec +CONSTANTS + Implementation = "current" +INVARIANT + TypeOK +INVARIANT + AtMostOneActiveScope +INVARIANT + GateBeforeOpen +INVARIANT + NoOverlappingRealContainers +INVARIANT + RealReleasedBeforeRelogin diff --git a/Where/Specifications/ScopeExclusivity/README.md b/Where/Specifications/ScopeExclusivity/README.md new file mode 100644 index 00000000..f3c7f9eb --- /dev/null +++ b/Where/Specifications/ScopeExclusivity/README.md @@ -0,0 +1,45 @@ +# Scope exclusivity + +Models at-most-one active [`WhereScope`](../../WhereUI/Sources/Model/WhereScope.swift) +and at-most-one live real [`SwiftDataStore`](../../WhereCore/Sources/Store/SwiftDataStore.swift) +container over the user's store file. Complements +[`LogRouting`](../LogRouting/README.md), which covers Periscope sink ownership; +this spec covers scope/container *lifetime*. + +## Correspondence + +| Model | Production | +| --- | --- | +| `activeScope` | `WhereModel.activeScope` (real / demo / none) | +| `realContainersAlive` | live disk `ModelContainer` count (0 or 1 in production) | +| `demoContainerOpen` | in-memory demo / Flyover sibling container | +| `onboardingGate` | launch parks before `resolveScope()` until user chooses | +| `flyoverBuilt` | `WhereFlyoverWorld.build()` sibling scope (DEBUG) | + +## Properties + +- `AtMostOneActiveScope` — singleton active scope +- `GateBeforeOpen` — onboarding gate blocks real store open +- `NoOverlappingRealContainers` — at most one live real container at a time +- `RealReleasedBeforeRelogin` — logged-out state has no live real container + +`BuildFlyoverSibling` leaves `activeScope` unchanged (Flyover never calls +`WhereModel.activateDemo`). + +## Result + +**Verified for these model bounds and assumptions** on `Current.cfg`. +`Broken.cfg` (second `ResolveRealScope` without releasing the first container) +falsifies `NoOverlappingRealContainers`. + +Swift guards: + +- [`WhereResetTests.loggingOutReleasesTheScopeBeforeTheNextLoginOpensOne`](../../WhereUI/Tests/WhereResetTests.swift) +- [`WhereLaunchTests.firstRunForegroundLaunchParksOnTheOnboardingGateBeforeOpeningAnything`](../../WhereUI/Tests/WhereLaunchTests.swift) +- [`WhereFlyoverWorldTests.buildsASeededSiblingWithoutActivatingIt`](../../WhereUI/Tests/WhereFlyoverWorldTests.swift) +- [`DemoModeTests.demoingFromAFreshInstallOpensNoRealStore`](../../WhereUI/Tests/DemoModeTests.swift) + +Log sink routing is separately verified by [`LogRouting`](../LogRouting/README.md). +Static `WhereLog` bypass in Flyover remains in [`Where/TODOs.md`](../../TODOs.md). + +Run: `./tla-check ScopeExclusivity` diff --git a/Where/Specifications/ScopeExclusivity/ScopeExclusivity.tla b/Where/Specifications/ScopeExclusivity/ScopeExclusivity.tla new file mode 100644 index 00000000..e0a5f848 --- /dev/null +++ b/Where/Specifications/ScopeExclusivity/ScopeExclusivity.tla @@ -0,0 +1,108 @@ +---- MODULE ScopeExclusivity ---- +EXTENDS Integers + +CONSTANTS Implementation + +ASSUME Implementation \in {"current", "broken"} + +ActiveScopes == {"none", "real", "demo"} + +VARIABLES + activeScope, + realContainersAlive, + demoContainerOpen, + onboardingGate, + flyoverBuilt + +vars == <> + +Init == + /\ activeScope = "none" + /\ realContainersAlive = 0 + /\ demoContainerOpen = FALSE + /\ onboardingGate = TRUE + /\ flyoverBuilt = FALSE + +ClearOnboardingGate == + /\ onboardingGate + /\ onboardingGate' = FALSE + /\ UNCHANGED <> + +ResolveRealScope == + /\ ~onboardingGate + /\ IF Implementation = "current" + THEN /\ activeScope = "none" + /\ realContainersAlive = 0 + ELSE activeScope \in {"none", "real"} + /\ activeScope' = "real" + /\ realContainersAlive' = realContainersAlive + 1 + /\ UNCHANGED <> + +LogOut == + /\ activeScope \in {"real", "demo"} + /\ activeScope' = "none" + /\ IF activeScope = "real" + THEN realContainersAlive' = 0 + ELSE UNCHANGED realContainersAlive + /\ IF activeScope = "demo" + THEN demoContainerOpen' = FALSE + ELSE UNCHANGED demoContainerOpen + /\ onboardingGate' = TRUE + /\ UNCHANGED flyoverBuilt + +ActivateDemo == + /\ ~onboardingGate + /\ activeScope \in {"none", "real"} + /\ activeScope' = "demo" + /\ demoContainerOpen' = TRUE + /\ IF activeScope = "real" + THEN realContainersAlive' = 0 + ELSE UNCHANGED realContainersAlive + /\ UNCHANGED <> + +BuildFlyoverSibling == + /\ demoContainerOpen' = TRUE + /\ flyoverBuilt' = TRUE + /\ UNCHANGED <> + +Stutter == + UNCHANGED vars + +Next == + \/ ClearOnboardingGate + \/ ResolveRealScope + \/ LogOut + \/ ActivateDemo + \/ BuildFlyoverSibling + \/ Stutter + +Fairness == + /\ WF_vars(ClearOnboardingGate) + /\ WF_vars(ResolveRealScope) + /\ WF_vars(LogOut) + /\ WF_vars(ActivateDemo) + /\ WF_vars(BuildFlyoverSibling) + +Spec == Init /\ [][Next]_vars /\ Fairness + +TypeOK == + /\ activeScope \in ActiveScopes + /\ realContainersAlive \in 0..2 + /\ demoContainerOpen \in BOOLEAN + /\ onboardingGate \in BOOLEAN + /\ flyoverBuilt \in BOOLEAN + +AtMostOneActiveScope == + activeScope \in ActiveScopes + +GateBeforeOpen == + onboardingGate => realContainersAlive = 0 + +NoOverlappingRealContainers == + realContainersAlive <= 1 + +RealReleasedBeforeRelogin == + activeScope = "none" => realContainersAlive = 0 + +==== diff --git a/Where/Specifications/ScopeExclusivity/manifest.json b/Where/Specifications/ScopeExclusivity/manifest.json new file mode 100644 index 00000000..f93b75ac --- /dev/null +++ b/Where/Specifications/ScopeExclusivity/manifest.json @@ -0,0 +1,16 @@ +{ + "module": "ScopeExclusivity.tla", + "cases": [ + { + "name": "broken", + "config": "Broken.cfg", + "expect": "fail", + "outputContains": "Invariant NoOverlappingRealContainers is violated." + }, + { + "name": "current", + "config": "Current.cfg", + "expect": "pass" + } + ] +} diff --git a/Where/TODOs.md b/Where/TODOs.md index fc6138c6..388d713f 100644 --- a/Where/TODOs.md +++ b/Where/TODOs.md @@ -65,8 +65,6 @@ The item format and the placement rule live in the root - fix(WhereUI): broken-snapshots: `locations.Loaded_iPad.png` bakes in raw inflection markup — the Elsewhere card's subtitle renders literally as `^[3 region](inflect: true)`. This is the `locations.elsewhere.subtitle` P1 filed above, now pinned as a reference; recorded here so the image isn't mistaken for correct output, and so that reference is re-recorded when the fix lands. (pr#101 review) ## P2s (Nice to have) -- design(WhereUI) [needs-design]: TLA+ — LaunchLifecycle narrow slice (undetermined promotion + single-drive invariant). Fuzz coverage exists; model one claim before broader controller rewrite. (agent 2026-08-04) -- design(WhereUI) [needs-design]: TLA+ — Scope mutual exclusion (at most one live scope / container over a store file). Ties to controller state-machine rewrite. (agent 2026-08-04) - feat(WhereUI) [needs-design]: Give the app a branded launch screen. `UILaunchScreen` is an empty dictionary (`Project.swift`), so the pre-main frame is plain white. Measured from a fresh-install simulator recording, a first run reads as ~1.7s of white → ~0.25s of the dark `LaunchSplashView` → the light onboarding screen, so the splash registers as a quarter-second dark blip between two light screens rather than as the app opening. A launch screen matching the splash's background + icon would make that continuous. Note this is the right layer to fix it at: the splash's own `minimumSplashDuration` hold deliberately gates only the `.ready` reveal, not a gate transition like onboarding, so lengthening the hold would just delay interactive UI. (agent) - refactor(WhereUI) [needs-design]: Make the scene-scoped model wiring compiler-checked rather than an `@Environment` lookup that fails silently. `WhereSession` (the always-on coordinator) is read from the environment, so a screen mounted without a parent injecting it resolves to a runtime fallback/precondition instead of a compile error. The scoped models (`YearReportModel`, `ResolveModel`, `BackupModel`, `RemindersSettingsModel`) are already constructor-injected; explore threading the coordinator the same way (or a non-defaulting typed `EnvironmentKey`) so a broken wiring can't build. Follow-up from the `WhereSession` split. (agent) - refactor(WhereUI) [needs-design]: Split `YearReportModel` further. Post-split it still fuses several roles for the selected year: the loaded report + everything derived from it (ranking, missing days, calendar inputs, tracked-day count), the Resolve badge *count*, the day-write intents (`setManualDay(s)`, `overrideDay`, `clearManualDay`, `clearSelectedYear`), and the Elsewhere drill-in reads (`days(in:)`, `locations(in:)`, `representativeCoordinates()`). The read-only presentation state and the write-intent/drill-in surface could be separate collaborators so a view only holds what it uses. Follow-up from the `WhereSession` split. (agent) @@ -137,7 +135,6 @@ re-recording: - Remove `caption(forRank rank: Int) -> String?`, I don’t want the caption ## P2s (Nice to have) -- fix(WhereUI) [needs-design]: A launch can park indefinitely behind a system permission prompt — claimed `WhereSession.reconcileTracking()` awaits the location-authorization *request*, holding the splash until the user answers the system alert. (Invalidated 2026-07-27: the claim doesn't hold. `reconcileTracking()` (`WhereSession.swift:282–293`) only reads the current `authorizationStatus` and starts/stops the ingestor — it never requests authorization — and `syncAuthorization()` is documented not to prompt. The launch trunk therefore cannot block on the location alert. The unprompted *notification* request at launch is real and remains filed as a P1 above.) (agent) - The `guard let controller else { return }` in the WhereModel in WhereUI is weird — gone with the controller: `WhereModel`'s guards now read as ownership invariants (`attach(services:)` is idempotent, `startSession()` requires attached services), and the type itself is `WhereServices`. - Move test only code behind @_spi — done throughout; test seams are `@_spi(Testing)` in both Where and the shared modules (direct store mutation, failure injection, queue introspection, clock/capacity overrides), and no `…ForTesting`-named API remains (`LifecycleRunner.injectFailureForTesting`, the last one, went with the engine's retry removal). - Move `let calendar = Calendar.current` into a var on the controller? There’s a few of these — the call sites moved onto explicit Gregorian calendars owned by `YearReportModel` / `WhereModel`. What's left isn't a controller-hoisting problem but three helper-level defaults, refiled as a P1 above (`CalendarDay.displayDate`, `DateRangeFormatting.abbreviated`, `PresenceTimeline.stints`). From 8fd615e827822fdcfcf1b4511ae3688106e7b73e Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 12:51:49 -0700 Subject: [PATCH 11/14] Restore completed P2 entry accidentally dropped from TODOs Co-authored-by: Cursor --- Where/TODOs.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Where/TODOs.md b/Where/TODOs.md index 388d713f..a56871e4 100644 --- a/Where/TODOs.md +++ b/Where/TODOs.md @@ -135,6 +135,9 @@ re-recording: - Remove `caption(forRank rank: Int) -> String?`, I don’t want the caption ## P2s (Nice to have) +- fix(WhereUI) [needs-design]: A launch can park indefinitely behind a system permission prompt — claimed `WhereSession.reconcileTracking()` awaits the location-authorization *request*, holding the splash until the user answers the system alert. (Invalidated 2026-07-27: the claim doesn't hold. `reconcileTracking()` (`WhereSession.swift:282–293`) only reads the current `authorizationStatus` and starts/stops the ingestor — it never requests authorization — and `syncAuthorization()` is documented not to prompt. The launch trunk therefore cannot block on the location alert. The unprompted *notification* request at launch is real and remains filed as a P1 above.) (agent) +- design(WhereUI): TLA+ — [`LaunchLifecycle`](Specifications/LaunchLifecycle/README.md) narrow slice (undetermined promotion + memo-preserving re-drive). Confirmatory on `Current.cfg`; broader controller rewrite still open. (agent 2026-08-04) +- design(WhereUI): TLA+ — [`ScopeExclusivity`](Specifications/ScopeExclusivity/README.md) (at most one live scope / real container). Confirmatory on `Current.cfg`; complements [`LogRouting`](Specifications/LogRouting/README.md). (agent 2026-08-04) - The `guard let controller else { return }` in the WhereModel in WhereUI is weird — gone with the controller: `WhereModel`'s guards now read as ownership invariants (`attach(services:)` is idempotent, `startSession()` requires attached services), and the type itself is `WhereServices`. - Move test only code behind @_spi — done throughout; test seams are `@_spi(Testing)` in both Where and the shared modules (direct store mutation, failure injection, queue introspection, clock/capacity overrides), and no `…ForTesting`-named API remains (`LifecycleRunner.injectFailureForTesting`, the last one, went with the engine's retry removal). - Move `let calendar = Calendar.current` into a var on the controller? There’s a few of these — the call sites moved onto explicit Gregorian calendars owned by `YearReportModel` / `WhereModel`. What's left isn't a controller-hoisting problem but three helper-level defaults, refiled as a P1 above (`CalendarDay.displayDate`, `DateRangeFormatting.abbreviated`, `PresenceTimeline.stints`). From ee3eaa2740d4f55f959ba6742d542dfb69807e70 Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 14:54:22 -0700 Subject: [PATCH 12/14] Fix ingest fan-out to preserve redundant-sample widget skip Route single-sample ingest and addManualSample through reconcileIssueState() plus publishAfterIngest(of:) so reminders/issue alerts reconcile without unconditional widget rebuilds. Bulk ingest keeps reconcileAfterDayChange(). Fixes WhereServicesTests.redundantGPSSamplesSkipRepublishingButNewRegionsStillPublish on CI. Co-authored-by: Cursor --- Where/Specifications/PostWriteReconcile/README.md | 7 ++++++- Where/TODOs.md | 2 +- Where/WhereCore/Sources/Journal/DayJournal.swift | 11 +++++++++-- 3 files changed, 16 insertions(+), 4 deletions(-) diff --git a/Where/Specifications/PostWriteReconcile/README.md b/Where/Specifications/PostWriteReconcile/README.md index 9feb36e3..65131f74 100644 --- a/Where/Specifications/PostWriteReconcile/README.md +++ b/Where/Specifications/PostWriteReconcile/README.md @@ -26,7 +26,12 @@ commit, then full fan-out (invalidate → reminders → issue alerts → widgets canonical manual-day path. `Broken.cfg` falsifies `BrokenNoEarlyPing`. Swift guards: [`DayJournalTests.addManualDayReconcilesAndPublishes`](../../WhereCore/Tests/DayJournalTests.swift), -[`DayJournalTests.ingestPersistsAndFansOutOnce`](../../WhereCore/Tests/DayJournalTests.swift). +[`DayJournalTests.ingestPersistsAndFansOutOnce`](../../WhereCore/Tests/DayJournalTests.swift), +[`WhereServicesTests.redundantGPSSamplesSkipRepublishingButNewRegionsStillPublish`](../../WhereCore/Tests/WhereServicesTests.swift). + +Single-sample ingest routes through `reconcileIssueState()` plus +`publishAfterIngest(of:)` (skips redundant widget rebuilds); bulk ingest uses +full `reconcileAfterDayChange()`. Out of model until routed: `DailySummaryReconciler`, `setPrimaryRegions` (see [`Where/TODOs.md`](../../TODOs.md) with links here). Dismiss/restore uses diff --git a/Where/TODOs.md b/Where/TODOs.md index a56871e4..af715a27 100644 --- a/Where/TODOs.md +++ b/Where/TODOs.md @@ -27,7 +27,7 @@ The item format and the placement rule live in the root - fix(WhereUI) [quick-win]: `CalendarDay.displayDate` resolves through `Calendar.current` (`DateRangeFormatting.swift:33`), so every day label that flows through it — relabel, logged days, resolution details, the region drill-in — renders a wrong date on a non-Gregorian device: `startOfDay(in:)` interprets the day's Gregorian Y-M-D as *that* calendar's components, so a Buddhist-era device resolves 2026-07-26 to a date ~543 years off. `DateRangeFormatting.abbreviated` (`:6`, `:19`) and `PresenceTimeline.stints` (`PresenceTimeline.swift:37`) also *default* to `.current`, and `PresenceTimelineList` (`:12`) doesn't pass `report.calendar`. Take an explicit calendar (Gregorian + current time zone) in the helper and thread the report's calendar from the call sites. The `where.gregorian_calendar` Bumper rule that should catch this is blind to the implicit-member form — filed in the root [`TODOs.md`](../TODOs.md). (audit 2026-07-26) - fix(WhereCore) [needs-design]: `WhereServices.setPrimaryRegions(_:)` (`:285`) commits atomically but skips `DayJournal.reconcileAfterDayChange()` — widgets/reminders/summary don't refresh until foreground/configure. Route picker commits through the unified fan-out, or document the intentional deferral. Out of scope for [`PostWriteReconcile`](Specifications/PostWriteReconcile/README.md) until routed. (audit 2026-07-26) - fix(WhereCore) [needs-design]: Soft-delete untracked regions. `SwiftDataStore.setTrackedRegion(false)` (`:756`, in-source TODO at `:773`) and `setPrimaryRegions` (`:833`) hard-delete the row, which drops the region from the attributor's load set — so re-aggregating a past year re-attributes that region's GPS days to `.other`. The `SwiftDataStore` TODO filed this as "when the region picker ships"; it has shipped, and both the onboarding picker and the Settings region editor now reach the delete, so this is user-reachable rather than latent. Retain the row for attribution and hide it from the pickers instead. (audit 2026-07-26) -- fix(WhereCore) [needs-design]: ~~`DayJournal.ingest(_:)` (`:70`), the bulk ingest (`:82`), and `addManualSample` (`:93`) publish widgets but skip the reminder/issue reconcile~~ — **fixed:** all three now route through `reconcileAfterDayChange()` (see [`PostWriteReconcile`](Specifications/PostWriteReconcile/README.md)). Remaining fan-out gaps: `DailySummaryReconciler` (P0 above) and `setPrimaryRegions` (above). (audit 2026-07-26; fixed 2026-08-04) +- fix(WhereCore) [needs-design]: ~~`DayJournal.ingest(_:)` (`:70`), the bulk ingest (`:82`), and `addManualSample` (`:93`) publish widgets but skip the reminder/issue reconcile~~ — **fixed:** single-sample ingest and `addManualSample` now fan out through `reconcileIssueState()` + `publishAfterIngest(of:)`; bulk ingest uses full `reconcileAfterDayChange()` (see [`PostWriteReconcile`](Specifications/PostWriteReconcile/README.md)). Remaining fan-out gaps: `DailySummaryReconciler` (P0 above) and `setPrimaryRegions` (above). (audit 2026-07-26; fixed 2026-08-04) - fix(WhereCore) [needs-design]: A durable outbox save failure is logged and swallowed (`LocationOutbox.swift:86`, `LocationIngestor.swift:344`), so a process death loses the in-memory sample with nothing to replay on relaunch. Handle the degraded state honestly rather than continuing as though the sample were durable. (audit 2026-07-26) - test(WhereCore) [quick-win]: Cover outbox *save* failure with a failing-outbox double; only load failure is covered today. (audit 2026-07-26) - fix(WhereCore) [needs-design]: The retry queue evicts FIFO at capacity and drops samples with a warning only (`LocationIngestor.swift:349`). Decide the capacity policy and whether eviction warrants user-visible degradation, then document it. (audit 2026-07-26) diff --git a/Where/WhereCore/Sources/Journal/DayJournal.swift b/Where/WhereCore/Sources/Journal/DayJournal.swift index 40c9e60f..032fe757 100644 --- a/Where/WhereCore/Sources/Journal/DayJournal.swift +++ b/Where/WhereCore/Sources/Journal/DayJournal.swift @@ -69,11 +69,18 @@ public actor DayJournal { } } + /// Reminder/issue fan-out plus the hot-path widget policy: skip a rebuild + /// when the sample cannot change what widgets show (same day + region). + private func reconcileAfterSampleIngest(_ sample: LocationSample) async { + await reconcileIssueState() + await widgets.publishAfterIngest(of: sample) + } + // MARK: - Ingestion public func ingest(_ sample: LocationSample) async throws { try await store.perform { try await store.add(sample: sample) } - await reconcileAfterDayChange() + await reconcileAfterSampleIngest(sample) } /// Persist many samples in a *single* transaction, rebuilding the widget @@ -98,7 +105,7 @@ public actor DayJournal { public func addManualSample(_ sample: LocationSample) async throws { try await store.perform { try await store.add(sample: sample) } - await reconcileAfterDayChange() + await reconcileAfterSampleIngest(sample) } public func addManualDay( From 29822bb8a68db400e9edb37e73c1a149e9efd127 Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 15:28:52 -0700 Subject: [PATCH 13/14] Credit TLA+/TLC via new developmentTools attribution source Add a developmentTools generator source type for pinned non-SPM tooling, wire TLA+ Tools v1.7.4 through .agents/development-tools.json, and regenerate Where's attribution report. Co-authored-by: Cursor --- .agents/development-tools.json | 7 +++++ AGENTS.md | 15 ++++++---- Shared/CreditKit/AGENTS.md | 4 ++- Shared/CreditKit/README.md | 25 +++++++++++----- .../CreditKit/Tools/generate-attribution.rb | 29 +++++++++++++++---- Where/Where/Resources/attribution.json | 10 +++++++ Where/Where/attribution-sources.json | 5 ++++ attribution | 5 ++-- 8 files changed, 79 insertions(+), 21 deletions(-) create mode 100644 .agents/development-tools.json diff --git a/.agents/development-tools.json b/.agents/development-tools.json new file mode 100644 index 00000000..0fdb7c04 --- /dev/null +++ b/.agents/development-tools.json @@ -0,0 +1,7 @@ +{ + "TLA+ Tools": { + "repo": "tlaplus/tlaplus", + "ref": "5a47802b5c391f59ecdd44117981f4ff8c0656ba", + "version": "1.7.4" + } +} diff --git a/AGENTS.md b/AGENTS.md index 866bdfee..9f7c1298 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -99,17 +99,18 @@ over a build setting Xcode didn't export. An app ships an **attribution report** — every third-party work it is built with, license notices inline. **Re-run `./attribution` and commit the result -whenever you add or bump a package or an agent skill**; `./attribution ---check` fails CI if you forget (offline, sub-second — an app's own tests -can't do this job, since a test bundle can't read `Package.swift`). +whenever you add or bump a package, an agent skill, or a development tool**; +`./attribution --check` fails CI if you forget (offline, sub-second — an app's +own tests can't do this job, since a test bundle can't read `Package.swift`). - [`Shared/CreditKit`](Shared/CreditKit/AGENTS.md) owns the types and the reporting tool and holds **no credits of its own**; each app declares its sources in an `attribution-sources.json` and ships the report in its own resources (for Where, `Where/Where/Resources/attribution.json`). - The report derives from `.product(name:package:)` links (pinned by - `Package.resolved`) and `.agents/external-skills.json`, notices read at the - pinned revision — so tooling-only packages correctly aren't credited. + `Package.resolved`), `.agents/external-skills.json`, and + `.agents/development-tools.json`, notices read at the pinned revision — so + tooling-only packages correctly aren't credited. - **Kind is derived, not declared**: anything reachable from `shippedFrom`'s target closure is a library, any other linked package a development tool — linking is not shipping, and a UI must keep the two apart. @@ -150,7 +151,9 @@ by `./sync-agents`. `.agents/skills/.gitignore` excludes those fetched copies, so anything else under `.agents/skills/` is **repo-owned** and committed. External skills are also an **attribution** input — after adding or updating one, re-run -`./attribution` (see [Attribution](#attribution)). +`./attribution` (see [Attribution](#attribution)). The same applies to +`.agents/development-tools.json` when pinned verification or other non-SPM +tooling changes. **`.agents/skills/` is the real home; edit the source, never the `.claude/skills/` mirror**, and run `./sync-agents` after adding or editing a diff --git a/Shared/CreditKit/AGENTS.md b/Shared/CreditKit/AGENTS.md index 6c9219ee..4d7c80d0 100644 --- a/Shared/CreditKit/AGENTS.md +++ b/Shared/CreditKit/AGENTS.md @@ -41,7 +41,9 @@ the root [`AGENTS.md`](../../AGENTS.md). - **`kind` is derived from reachability, not declared.** `shippedFrom` names the app's root package targets; anything inside that closure is a `library`, any other linked package a `developmentTool` — linking is not shipping. - `shippedFrom` is the only hand-set part. + `shippedFrom` is the only hand-set part for SPM packages. **`agentSkills` and + `developmentTools` declare `kind` in config** — both are development tools in + Where today. ## Testing diff --git a/Shared/CreditKit/README.md b/Shared/CreditKit/README.md index 7004ef0c..5c7c1445 100644 --- a/Shared/CreditKit/README.md +++ b/Shared/CreditKit/README.md @@ -66,17 +66,20 @@ ruby Shared/CreditKit/Tools/generate-attribution.rb # just one { "type": "swiftPackageManager", "manifest": "Package.swift", "resolved": "Package.resolved", "shippedFrom": ["WhereUI"] }, { "type": "agentSkills", "kind": "developmentTool", - "manifest": ".agents/external-skills.json" } + "manifest": ".agents/external-skills.json" }, + { "type": "developmentTools", "kind": "developmentTool", + "manifest": ".agents/development-tools.json" } ] } ``` -Paths are relative to the repository root. Two source types are understood: +Paths are relative to the repository root. Three source types are understood: | Type | Reads | Credits | |------|-------|---------| | `swiftPackageManager` | packages a target links via `.product(name:package:)`, pinned by the resolved file | one per linked package | | `agentSkills` | a `./sync-agents` manifest of `name -> { repo, ref }` | one per vendored skill | +| `developmentTools` | a manifest of `name -> { repo, ref, version? }` for pinned GitHub-hosted tooling the repo uses but does not link as an SPM package | one per entry | Deriving the list rather than maintaining it is the point: a package linked by *any* module shows up the next time the report runs, so no module has to @@ -92,6 +95,12 @@ a test-support target is credited (the repo depends on it) but must not be described as being in the binary. `shippedFrom` is the only part set by hand, so adding a dependency can't quietly land under the wrong kind. +`developmentTools` entries may carry an optional `version` for display; when +omitted, the pinned ref's short prefix is used (as for agent skills). Keep each +entry's `ref` aligned with the revision the repository actually uses — for +example, bump `.agents/development-tools.json` when `./tla-check`'s pinned TLC +version changes. + The tool needs network and an authenticated `gh`. It is idempotent: re-running with nothing changed rewrites the same bytes. @@ -116,9 +125,10 @@ handle at runtime. credit names in a test — a test bundle can't read the manifests, so it can only compare the report to a literal, which a stale report matches too. - **Development tools are not in the binary.** They are credited because the - repository makes copies of them, which permissive licenses ask us to - attribute. Any UI must keep the two kinds visually distinct so a reader isn't - told something untrue about the app they are running. + repository depends on them — vendored agent skills, pinned verification + tooling, and the like — which permissive licenses ask us to attribute. Any UI + must keep the two kinds visually distinct so a reader isn't told something + untrue about the app they are running. - **A missing report is not automatically an error.** Only the app target ships one, so `load` throwing `.reportMissing` is routine in a developer tool or test host. CreditKit reports it and leaves the judgement to the caller. @@ -129,5 +139,6 @@ handle at runtime. is on its own; the type can't check what it can't see. - **Names, versions, and license titles are never localized.** They are proper nouns and legal terms; a UI supplies the translated framing around them. -- **GitHub-hosted sources only.** Both source types resolve notices through the - GitHub API; a dependency hosted elsewhere would need a new source type. +- **GitHub-hosted sources only.** All manifest-based source types resolve + notices through the GitHub API; a dependency hosted elsewhere would need a + new source type. diff --git a/Shared/CreditKit/Tools/generate-attribution.rb b/Shared/CreditKit/Tools/generate-attribution.rb index 47302c0d..aeeafb41 100755 --- a/Shared/CreditKit/Tools/generate-attribution.rb +++ b/Shared/CreditKit/Tools/generate-attribution.rb @@ -17,7 +17,9 @@ # { "type": "swiftPackageManager", "manifest": "Package.swift", # "resolved": "Package.resolved", "shippedFrom": ["WhereUI"] }, # { "type": "agentSkills", "kind": "developmentTool", -# "manifest": ".agents/external-skills.json" } +# "manifest": ".agents/external-skills.json" }, +# { "type": "developmentTools", "kind": "developmentTool", +# "manifest": ".agents/development-tools.json" } # ] # } # @@ -37,6 +39,10 @@ # - `agentSkills` — a `./sync-agents` external-skills manifest of # `name -> { repo, ref }`. These are not in the binary, but the repository # makes copies of them, which is what their licenses ask us to attribute. +# - `developmentTools` — a manifest of pinned GitHub-hosted tooling the +# repository depends on but does not link as an SPM package (e.g. TLA+/TLC +# via `./tla-check`). Entries may carry an optional `version` for display; +# otherwise the pinned ref's short prefix is used. # # Each credit carries its notice **inline**, read at the pinned revision, so one # decode yields everything needed to discharge the attribution and there is no @@ -199,20 +205,28 @@ def swift_package_manager_credits(source) end end -def agent_skills_credits(source) +def manifest_credits(source, source_type) kind = source.fetch("kind") - read_json(source.fetch("manifest"), "agentSkills").map do |name, entry| + read_json(source.fetch("manifest"), source_type).map do |name, entry| ref = entry.fetch("ref") credit( name: name, kind: kind, - version: ref[0, 12], + version: entry["version"] || ref[0, 12], slug: entry.fetch("repo"), ref: ref, ) end end +def agent_skills_credits(source) + manifest_credits(source, "agentSkills") +end + +def development_tools_credits(source) + manifest_credits(source, "developmentTools") +end + SOURCE_TYPES = { "swiftPackageManager" => { required: %w[manifest resolved shippedFrom], @@ -222,6 +236,10 @@ def agent_skills_credits(source) required: %w[manifest kind], generate: method(:agent_skills_credits), }, + "developmentTools" => { + required: %w[manifest kind], + generate: method(:development_tools_credits), + }, }.freeze # Checked for every source before any of them runs, so a config mistake costs a @@ -287,7 +305,8 @@ def write_report(credits, output_path) # # Runs entirely offline, which is the whole reason it can gate CI: every field # it compares is derived from `Package.swift`, `Package.resolved`, and the skills -# manifest. It can't re-read a notice, but it doesn't need to — a notice is +# and development-tools manifests. It can't re-read a notice, but it doesn't need +# to — a notice is # fetched at the pinned revision, so a matching revision means matching text by # construction, and the notice being *present* is checked here directly. def check_report(credits, output_path) diff --git a/Where/Where/Resources/attribution.json b/Where/Where/Resources/attribution.json index 99064336..1f658966 100644 --- a/Where/Where/Resources/attribution.json +++ b/Where/Where/Resources/attribution.json @@ -69,6 +69,16 @@ "name": "MIT License", "text": "MIT License\n\nCopyright (c) 2026 Paul Hudson.\n\nPermission is hereby granted, free of charge, to any person obtaining a copy\nof this software and associated documentation files (the \"Software\"), to deal\nin the Software without restriction, including without limitation the rights\nto use, copy, modify, merge, publish, distribute, sublicense, and/or sell\ncopies of the Software, and to permit persons to whom the Software is\nfurnished to do so, subject to the following conditions:\n\nThe above copyright notice and this permission notice shall be included in all\ncopies or substantial portions of the Software.\n\nTHE SOFTWARE IS PROVIDED \"AS IS\", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR\nIMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,\nFITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE\nAUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER\nLIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,\nOUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE\nSOFTWARE." } + }, + { + "name": "TLA+ Tools", + "kind": "developmentTool", + "version": "1.7.4", + "homepageURL": "https://github.com/tlaplus/tlaplus", + "license": { + "name": "MIT License", + "text": "MIT License\n\nCopyright (c) 2017 Microsoft Corporation\n\nPermission is hereby granted, free of charge, to any person obtaining a copy\nof this software and associated documentation files (the \"Software\"), to deal\nin the Software without restriction, including without limitation the rights\nto use, copy, modify, merge, publish, distribute, sublicense, and/or sell\ncopies of the Software, and to permit persons to whom the Software is\nfurnished to do so, subject to the following conditions:\n\nThe above copyright notice and this permission notice shall be included in all\ncopies or substantial portions of the Software.\n\nTHE SOFTWARE IS PROVIDED \"AS IS\", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR\nIMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,\nFITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE\nAUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER\nLIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,\nOUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE\nSOFTWARE.\n\n" + } } ] } diff --git a/Where/Where/attribution-sources.json b/Where/Where/attribution-sources.json index db51814f..3c8b8704 100644 --- a/Where/Where/attribution-sources.json +++ b/Where/Where/attribution-sources.json @@ -11,6 +11,11 @@ "type": "agentSkills", "kind": "developmentTool", "manifest": ".agents/external-skills.json" + }, + { + "type": "developmentTools", + "kind": "developmentTool", + "manifest": ".agents/development-tools.json" } ] } diff --git a/attribution b/attribution index 5179c310..2063a3dd 100755 --- a/attribution +++ b/attribution @@ -10,8 +10,9 @@ set -euo pipefail # dependency, whereas a re-run picks it up wherever it landed. # # Each app declares its own sources in an attribution-sources.json; the generic -# reporting lives in CreditKit. Re-run after adding or bumping a package, or -# after `./sync-agents --update` moves a pinned skill, and commit the result. +# reporting lives in CreditKit. Re-run after adding or bumping a package, after +# `./sync-agents --update` moves a pinned skill, or after changing +# `.agents/development-tools.json`, and commit the result. # # Needs network and an authenticated `gh` (notices are read at the pinned # revision, so the text shipped is the one governing the code actually in use). From e9c26d650f34c4dd67b661774fecee19566b6ec7 Mon Sep 17 00:00:00 2001 From: Kyle Van Essen Date: Tue, 4 Aug 2026 16:12:25 -0700 Subject: [PATCH 14/14] Rename reconcileAfterDayChange to reconcileAfterDayDataChange Clarifies the method runs after persisted day-level store data changes, not a calendar-day rollover. Co-authored-by: Cursor --- MODULE_AUDIT.md | 4 ++-- .../PostWriteReconcile/README.md | 4 ++-- Where/TODOs.md | 6 ++--- Where/WhereCore/AGENTS.md | 2 +- .../Sources/Journal/DayJournal.swift | 22 +++++++++---------- .../Sources/Logging/DayJournalLog.swift | 4 ++-- Where/WhereCore/Sources/WhereServices.swift | 2 +- 7 files changed, 22 insertions(+), 22 deletions(-) diff --git a/MODULE_AUDIT.md b/MODULE_AUDIT.md index 60780777..f15b4704 100644 --- a/MODULE_AUDIT.md +++ b/MODULE_AUDIT.md @@ -53,7 +53,7 @@ Pointers only — each one's evidence and suggested fix live in the linked file. | 3 | **high** | WhereCore | `DailySummaryReconciler.reconcile()` is absent from the post-day-change fan-out — the notification body stays stale until a foreground re-`configure` | [`Where/TODOs.md`](Where/TODOs.md) P0 | | 4 | **high** | WhereUI | Tracking toggle race — `trackingEnabled`'s setter spawns unserialized `Task`s | [`Where/TODOs.md`](Where/TODOs.md) P1 | | 5 | **high** | LifecycleKit | Cancel during the *last* step's `minVisible` hold isn't observed, so a superseded drive can set `phase = .ready` | [`Shared/LifecycleKit/TODOs.md`](Shared/LifecycleKit/TODOs.md) P0 | -| 6 | **medium** | WhereCore | `setPrimaryRegions(_:)` commits atomically but skips `reconcileAfterDayChange()` | [`Where/TODOs.md`](Where/TODOs.md) P1 | +| 6 | **medium** | WhereCore | `setPrimaryRegions(_:)` commits atomically but skips `reconcileAfterDayDataChange()` | [`Where/TODOs.md`](Where/TODOs.md) P1 | | 7 | **medium** | WhereCore | `setTrackedRegion(false)` hard-deletes the row; the shipped picker now reaches it, so past-year re-attribution risk is live | [`Where/TODOs.md`](Where/TODOs.md) P1 | | 8 | **medium** | PeriscopeCore | Orphan sweep treats an undecodable `SpanBegan` as an orphan-close candidate, silently overriding `survivesRelaunch` | [`Shared/Periscope/TODOs.md`](Shared/Periscope/TODOs.md) P1 | | 9 | **medium** | WhereUI | Load-state UI duplicated across four views; `PresenceTimelineList` renders the *empty* state while the year is still loading | [`Where/TODOs.md`](Where/TODOs.md) P1 | @@ -69,7 +69,7 @@ Pointers only — each one's evidence and suggested fix live in the linked file. ### Reconciliation: same two holes, one now user-reachable -`reconcileAfterDayChange()` still fans out to issue state and widgets only. **Daily summary** remains outside it, and **`setPrimaryRegions(_:)`** still commits without calling it. Related and newly urgent: untracking a region hard-deletes its row, and the shipped onboarding picker plus the Settings region editor both route into that path, so the past-year re-attribution risk the `SwiftDataStore` TODO describes is now something a user can trigger. +`reconcileAfterDayDataChange()` still fans out to issue state and widgets only. **Daily summary** remains outside it, and **`setPrimaryRegions(_:)`** still commits without calling it. Related and newly urgent: untracking a region hard-deletes its row, and the shipped onboarding picker plus the Settings region editor both route into that path, so the past-year re-attribution risk the `SwiftDataStore` TODO describes is now something a user can trigger. ### Presentation-layer calendar drift outlived the fix diff --git a/Where/Specifications/PostWriteReconcile/README.md b/Where/Specifications/PostWriteReconcile/README.md index 65131f74..e098b2bf 100644 --- a/Where/Specifications/PostWriteReconcile/README.md +++ b/Where/Specifications/PostWriteReconcile/README.md @@ -1,6 +1,6 @@ # Post-write reconcile -Models the intended contract in [`DayJournal.reconcileAfterDayChange()`](../../WhereCore/Sources/Journal/DayJournal.swift): +Models the intended contract in [`DayJournal.reconcileAfterDayDataChange()`](../../WhereCore/Sources/Journal/DayJournal.swift): commit, then full fan-out (invalidate → reminders → issue alerts → widgets), then `changes()` readers observe applied side effects. @@ -31,7 +31,7 @@ Swift guards: [`DayJournalTests.addManualDayReconcilesAndPublishes`](../../Where Single-sample ingest routes through `reconcileIssueState()` plus `publishAfterIngest(of:)` (skips redundant widget rebuilds); bulk ingest uses -full `reconcileAfterDayChange()`. +full `reconcileAfterDayDataChange()`. Out of model until routed: `DailySummaryReconciler`, `setPrimaryRegions` (see [`Where/TODOs.md`](../../TODOs.md) with links here). Dismiss/restore uses diff --git a/Where/TODOs.md b/Where/TODOs.md index af715a27..894923eb 100644 --- a/Where/TODOs.md +++ b/Where/TODOs.md @@ -17,7 +17,7 @@ The item format and the placement rule live in the root - fix(WhereCore): Nothing gets recorded on a day with no movement — presumably because background updates ride on GPS. Any way to guarantee a daily boot outside of GPS? (human) ## P0s (Must do) -- fix(WhereCore) [needs-design]: `DailySummaryReconciler.reconcile()` is absent from the post-day-change fan-out. Its only caller is `configure` (`DailySummaryReconciler.swift:45`), and `DayJournal.reconcileAfterDayChange()` (`:63`) fans out to issue state and widgets only — so the daily notification body stays stale until a foreground re-`configure`. Add it to the fan-out (the GPS ingest hook, `reconcileAfterDayChange()`, backup `onImport`), or document the foreground-only policy. Verified canonical fan-out ordering in [`Specifications/PostWriteReconcile`](Specifications/PostWriteReconcile/README.md); summary reconciler still out of model scope until routed. (audit 2026-07-26) +- fix(WhereCore) [needs-design]: `DailySummaryReconciler.reconcile()` is absent from the post-day-change fan-out. Its only caller is `configure` (`DailySummaryReconciler.swift:45`), and `DayJournal.reconcileAfterDayDataChange()` (`:63`) fans out to issue state and widgets only — so the daily notification body stays stale until a foreground re-`configure`. Add it to the fan-out (the GPS ingest hook, `reconcileAfterDayDataChange()`, backup `onImport`), or document the foreground-only policy. Verified canonical fan-out ordering in [`Specifications/PostWriteReconcile`](Specifications/PostWriteReconcile/README.md); summary reconciler still out of model scope until routed. (audit 2026-07-26) - test(WhereCore) [quick-win]: Mutate data and assert the summary notification body updates without a re-`configure`. (audit 2026-07-26) - perf(WhereCore) [needs-design]: Performance pass — how often is the app booting? Can we only do it on changes of, say, 1 km or more? (human) @@ -25,9 +25,9 @@ The item format and the placement rule live in the root - feat(Where) [needs-design]: Add an optional onboarding step that backfills the current year from the GPS metadata of photos in the user's library. `OnboardingView.Phase` currently moves from region selection/customization directly to location permission (`WhereUI/Sources/Onboarding/OnboardingView.swift:30`), while `DayJournal.ingest(_:)` is the existing bulk sample path (`WhereCore/Sources/Journal/DayJournal.swift:82`). Design a PhotoKit-backed importer that requests access only after an explicit opt-in, reads location and capture time locally without uploading photo contents, previews what will be added, records photo-derived provenance rather than treating it as live GPS, deduplicates repeat imports, and makes skipping the screen frictionless. (human 2026-08-03) - refactor(WhereCore) [needs-design]: Scope diagnostic emission so Flyover's unactivated sibling demo world cannot write its activity through the process-global `WhereLog` / `Periscope.shared` facade into the active real scope's durable diagnostic store. `WhereFlyoverWorld.build()` correctly gives the sibling a private `Periscope` and never starts its sink, but static `WhereLog` channels still bypass that injection; carry the scope's logging system through services/models or add a task-/environment-scoped routing context before treating Flyover's diagnostic activity as isolated. Domain data, preferences, widgets, notifications, and location remain in memory/no-op already. (`WhereUI/Sources/Developer/Flyover/WhereFlyoverWorld.swift`, `WhereCore/Sources/Logging/WhereLog.swift`; agent 2026-07-29) - fix(WhereUI) [quick-win]: `CalendarDay.displayDate` resolves through `Calendar.current` (`DateRangeFormatting.swift:33`), so every day label that flows through it — relabel, logged days, resolution details, the region drill-in — renders a wrong date on a non-Gregorian device: `startOfDay(in:)` interprets the day's Gregorian Y-M-D as *that* calendar's components, so a Buddhist-era device resolves 2026-07-26 to a date ~543 years off. `DateRangeFormatting.abbreviated` (`:6`, `:19`) and `PresenceTimeline.stints` (`PresenceTimeline.swift:37`) also *default* to `.current`, and `PresenceTimelineList` (`:12`) doesn't pass `report.calendar`. Take an explicit calendar (Gregorian + current time zone) in the helper and thread the report's calendar from the call sites. The `where.gregorian_calendar` Bumper rule that should catch this is blind to the implicit-member form — filed in the root [`TODOs.md`](../TODOs.md). (audit 2026-07-26) -- fix(WhereCore) [needs-design]: `WhereServices.setPrimaryRegions(_:)` (`:285`) commits atomically but skips `DayJournal.reconcileAfterDayChange()` — widgets/reminders/summary don't refresh until foreground/configure. Route picker commits through the unified fan-out, or document the intentional deferral. Out of scope for [`PostWriteReconcile`](Specifications/PostWriteReconcile/README.md) until routed. (audit 2026-07-26) +- fix(WhereCore) [needs-design]: `WhereServices.setPrimaryRegions(_:)` (`:285`) commits atomically but skips `DayJournal.reconcileAfterDayDataChange()` — widgets/reminders/summary don't refresh until foreground/configure. Route picker commits through the unified fan-out, or document the intentional deferral. Out of scope for [`PostWriteReconcile`](Specifications/PostWriteReconcile/README.md) until routed. (audit 2026-07-26) - fix(WhereCore) [needs-design]: Soft-delete untracked regions. `SwiftDataStore.setTrackedRegion(false)` (`:756`, in-source TODO at `:773`) and `setPrimaryRegions` (`:833`) hard-delete the row, which drops the region from the attributor's load set — so re-aggregating a past year re-attributes that region's GPS days to `.other`. The `SwiftDataStore` TODO filed this as "when the region picker ships"; it has shipped, and both the onboarding picker and the Settings region editor now reach the delete, so this is user-reachable rather than latent. Retain the row for attribution and hide it from the pickers instead. (audit 2026-07-26) -- fix(WhereCore) [needs-design]: ~~`DayJournal.ingest(_:)` (`:70`), the bulk ingest (`:82`), and `addManualSample` (`:93`) publish widgets but skip the reminder/issue reconcile~~ — **fixed:** single-sample ingest and `addManualSample` now fan out through `reconcileIssueState()` + `publishAfterIngest(of:)`; bulk ingest uses full `reconcileAfterDayChange()` (see [`PostWriteReconcile`](Specifications/PostWriteReconcile/README.md)). Remaining fan-out gaps: `DailySummaryReconciler` (P0 above) and `setPrimaryRegions` (above). (audit 2026-07-26; fixed 2026-08-04) +- fix(WhereCore) [needs-design]: ~~`DayJournal.ingest(_:)` (`:70`), the bulk ingest (`:82`), and `addManualSample` (`:93`) publish widgets but skip the reminder/issue reconcile~~ — **fixed:** single-sample ingest and `addManualSample` now fan out through `reconcileIssueState()` + `publishAfterIngest(of:)`; bulk ingest uses full `reconcileAfterDayDataChange()` (see [`PostWriteReconcile`](Specifications/PostWriteReconcile/README.md)). Remaining fan-out gaps: `DailySummaryReconciler` (P0 above) and `setPrimaryRegions` (above). (audit 2026-07-26; fixed 2026-08-04) - fix(WhereCore) [needs-design]: A durable outbox save failure is logged and swallowed (`LocationOutbox.swift:86`, `LocationIngestor.swift:344`), so a process death loses the in-memory sample with nothing to replay on relaunch. Handle the degraded state honestly rather than continuing as though the sample were durable. (audit 2026-07-26) - test(WhereCore) [quick-win]: Cover outbox *save* failure with a failing-outbox double; only load failure is covered today. (audit 2026-07-26) - fix(WhereCore) [needs-design]: The retry queue evicts FIFO at capacity and drops samples with a warning only (`LocationIngestor.swift:349`). Decide the capacity policy and whether eviction warrants user-visible degradation, then document it. (audit 2026-07-26) diff --git a/Where/WhereCore/AGENTS.md b/Where/WhereCore/AGENTS.md index 0357a0d3..2f5ac9ac 100644 --- a/Where/WhereCore/AGENTS.md +++ b/Where/WhereCore/AGENTS.md @@ -78,7 +78,7 @@ internal shape. URL.** Never let another store in the process (notably Periscope) ping `WhereStore.changes()`; guard: `StoreRemoteChangeSourceTests`. - **Post-write reconciliation is defined once.** Every write and import - routes through `DayJournal.reconcileAfterDayChange()` (or its widget-less + routes through `DayJournal.reconcileAfterDayDataChange()` (or its widget-less subset `reconcileIssueState()`) — never copy the fan-out into a new write path. Cross-collaborator hooks take a single closure wired at the composition root (`BackupCoordinator.onImport`). diff --git a/Where/WhereCore/Sources/Journal/DayJournal.swift b/Where/WhereCore/Sources/Journal/DayJournal.swift index 032fe757..c2e9a7e1 100644 --- a/Where/WhereCore/Sources/Journal/DayJournal.swift +++ b/Where/WhereCore/Sources/Journal/DayJournal.swift @@ -44,7 +44,7 @@ public actor DayJournal { /// Recount data issues and reconcile the reminder badge + the "issues to /// resolve" notification off the fresh count. The subset every committed /// write shares; a write that changes *day data* additionally republishes - /// the widget snapshot via `reconcileAfterDayChange()`. + /// the widget snapshot via `reconcileAfterDayDataChange()`. /// /// The scanner is invalidated inline (not just via its async store-change /// observation) so the reconciles below recount from fresh data rather than @@ -62,8 +62,8 @@ public actor DayJournal { /// snapshot. Every day-mutating write funnels through here so the fan-out /// stays in one place — including the backup import, which the composition /// root points at this method via `BackupCoordinator`'s `onImport` hook. - func reconcileAfterDayChange() async { - await Self.logger.measure(.reconcileAfterDayChange, budget: .seconds(5)) { + func reconcileAfterDayDataChange() async { + await Self.logger.measure(.reconcileAfterDayDataChange, budget: .seconds(5)) { await reconcileIssueState() await widgets.publish() } @@ -98,7 +98,7 @@ public actor DayJournal { } } } - await reconcileAfterDayChange() + await reconcileAfterDayDataChange() } // MARK: - Retroactive entry @@ -116,7 +116,7 @@ public actor DayJournal { let day = CalendarDay(from: date, in: aggregator.calendar) let presence = DayPresence(day: day, regions: regions, audit: audit) try await store.perform { try await store.setManualDay(presence) } - await reconcileAfterDayChange() + await reconcileAfterDayDataChange() Self.logger { .addedManualDay(day: String(describing: day), regionCount: regions.count) } } @@ -133,7 +133,7 @@ public actor DayJournal { let day = CalendarDay(from: date, in: aggregator.calendar) let presence = DayPresence(day: day, regions: regions, isAuthoritative: true, audit: audit) try await store.perform { try await store.setManualDay(presence) } - await reconcileAfterDayChange() + await reconcileAfterDayDataChange() Self.logger { .overrodeDay(day: String(describing: day), regionCount: regions.count) } } @@ -144,7 +144,7 @@ public actor DayJournal { public func clearManualDay(date: Date) async throws { let day = CalendarDay(from: date, in: aggregator.calendar) try await store.perform { try await store.clearManualDay(day) } - await reconcileAfterDayChange() + await reconcileAfterDayDataChange() Self.logger { .clearedManualDay(day: String(describing: day)) } } @@ -167,7 +167,7 @@ public actor DayJournal { } } } - await reconcileAfterDayChange() + await reconcileAfterDayDataChange() Self.logger { .clearedManualDays(dayCount: days.count) } } @@ -201,7 +201,7 @@ public actor DayJournal { } } } - await reconcileAfterDayChange() + await reconcileAfterDayDataChange() Self.logger { .backfilledManualDays(dayCount: days.count, regionCount: regions.count) } @@ -215,7 +215,7 @@ public actor DayJournal { try await Self.logger.measure(.clearYear, budget: .seconds(5)) { try await store.perform { try await store.clear(in: interval, manualDays: dayRange) } } - await reconcileAfterDayChange() + await reconcileAfterDayDataChange() Self.logger { .clearedYear(year: year) } } @@ -228,7 +228,7 @@ public actor DayJournal { try await Self.logger.measure(.eraseAllData, budget: .seconds(10)) { try await store.perform { try await store.clearAll() } } - await reconcileAfterDayChange() + await reconcileAfterDayDataChange() Self.logger { .erasedAllData } } diff --git a/Where/WhereCore/Sources/Logging/DayJournalLog.swift b/Where/WhereCore/Sources/Logging/DayJournalLog.swift index 7be239b3..f13aeb29 100644 --- a/Where/WhereCore/Sources/Logging/DayJournalLog.swift +++ b/Where/WhereCore/Sources/Logging/DayJournalLog.swift @@ -26,9 +26,9 @@ enum DayJournalLog: LogEvent { /// scanner, then recount the badge and the issue notification. case reconcileIssueState /// ``reconcileIssueState`` plus the widget republish, for writes that - /// changed day data. Nests the former, so the difference between the two + /// changed persisted day data. Nests the former, so the difference between the two /// spans is what WidgetKit cost. - case reconcileAfterDayChange + case reconcileAfterDayDataChange } case addedManualDay(day: String, regionCount: Int) diff --git a/Where/WhereCore/Sources/WhereServices.swift b/Where/WhereCore/Sources/WhereServices.swift index c7f6203c..b55b3d36 100644 --- a/Where/WhereCore/Sources/WhereServices.swift +++ b/Where/WhereCore/Sources/WhereServices.swift @@ -185,7 +185,7 @@ public struct WhereServices: Sendable { // publish) rather than duplicating that fan-out. let backup = BackupCoordinator( store: store, - onImport: { await journal.reconcileAfterDayChange() }, + onImport: { await journal.reconcileAfterDayDataChange() }, ) let recentActivity = RecentActivitySummarizer( store: store,