Block It Out

TODO: Formal Verification & State Machine for Shadow Sync

Problem Statement

The shadow sync system has had multiple critical bugs due to complex state management:

1. Duplicate shadows being created
2. Orphan detection incorrectly deleting valid shadows
3. Store keys vs shadow note mismatches (timestamp handling)
4. Phase transitions between different sync strategies

Required: TLA+ Formal Model

State Machine Definition

Create a formal TLA+ specification that defines:

States

• NONE: No shadow exists for this source event
• CREATED: Shadow created but not yet recorded in store
• SYNCED: Shadow exists and store record matches current inputs
• STALE: Shadow exists but inputs changed (needs update)
• ORPHANED: Store record exists but source event no longer exists
• DELETED: Shadow removed from calendar

State Transitions

NONE -> CREATED: First sync creates shadow
CREATED -> SYNCED: Store record saved successfully
SYNCED -> SYNCED: Inputs unchanged (skip)
SYNCED -> STALE: Source event inputs changed
STALE -> SYNCED: Shadow updated with new inputs
SYNCED -> ORPHANED: Source event deleted/removed
ORPHANED -> DELETED: Orphan cleanup runs
DELETED -> NONE: Cleanup complete

Invariants to Verify

1. No Duplicates: For each (ruleID, sourceEventID, destCalendarID), at most ONE shadow exists
2. Store Consistency: If shadow exists, store MUST have matching record
3. Orphan Correctness: Shadow is orphan IFF source event no longer in sync range
4. Key Format Consistency: Store keys and shadow note IDs must use same format (with or without timestamp)
5. Idempotency: Running sync twice with no changes should result in 0 insertions, 0 deletions

Implementation Requirements

1. Formal Specification

• Write TLA+ spec for shadow lifecycle
• Model check all state transitions
• Verify invariants hold under all conditions
• Test concurrent syncs to multiple destinations
• Model recurring event occurrence handling

2. Code Structure

• Create explicit ShadowState enum matching TLA+ states
• Implement state transition functions with pre/post-condition checks
• Add assertions at each state transition to verify invariants
• Log state transitions for audit trail

3. Testing

• Property-based tests that verify invariants
• Test fixtures for each state transition
• Chaos testing: random event additions/deletions/modifications
• Regression tests for each historical bug:
  • Duplicate shadow creation (v1.4)
  • Orphan detection false positives (v1.6 Phase B)
  • Recurring event ID handling (v1.5)

4. Key Format Standardization

• Document canonical key formats for:
  • Store record keys: {ruleID}-{sourceEventID}@{timestamp}
  • Shadow note IDs: {sourceEventID} (no timestamp)
  • Orphan detection matching: Must strip timestamps before comparing
• Create key manipulation utility functions with tests
• Ensure all code paths use standard formats

Current Bugs Fixed

• v1.6 Phase B Bug (2026-02-24): Orphan detection included timestamps in keep list but shadow notes didn’t have timestamps, causing false orphan deletions and re-creation cycles

References

• Shadow Snapshot Store: BlockItOut/Services/ShadowSnapshotStore.swift
• Sync Engine: BlockItOut/SyncEngine/SyncService.swift
• Shadow Note Manager: BlockItOut/Services/ShadowNoteManager.swift

Priority: HIGH

This must be addressed comprehensively to prevent continued regression bugs in the sync system.