Energy UI β Compliance against the published spec
GFTCL-LION-ENERGY-LEDGER-001 / UI compliance audit. This document is a section-by-section cross-check of the published Apple/Swift UI spec against the actually-shipped implementation. It names matches, deliberate adaptations, and named-next gaps verbatim so any reviewer can compare without reading source.
TL;DR
Core functionality: 100% shipped. Governor control + live ledger bar + sweep chart + summit board with dependency locks + receipt list + replication endpoints + immutability triggers + USD scene + gate enforcement. All smoke tests ALL PASS.
Deliberate adaptations (different from the spec on purpose):
1. Int64 quanta instead of generic Rational. The Lean seal proves the theorems over Nat; the Swift gate uses Int64. Switching to a generic Rational layer would require a new Lean theorem and break the existing decide-closed proofs. The doctrine point β exact-arithmetic, no Float β is preserved.
2. GRDB direct reads through EnergySummitReader / AlertQueueReader actors instead of SwiftData @Model. Consistent with the existing app (LedgerReader, MeaningAtomResolver, etc., all use GRDB directly). SwiftData would be a re-architecture of the substrate read path.
3. Plain executableTarget smoke tests (swift run M8β¦) instead of Swift Testing @Test. Same invariants are exercised; tests run the same way as the rest of the cell's smoke tests.
Named-next gaps (called out, not silently missing):
- Menu bar extra (MenuBarExtra with arm-state glyph + unread count)
- Receipt detail sheet with the inline three-command repro string
- Summit submission-log drill-in card
- Asset-catalog semantic color tokens (currently inline Color(red:β¦))
- Dynamic Type full scaling (currently fixed font sizes)
- ARMED+IDLE "listening" pulse animation (currently static color)
Section-by-section
| Spec |
Implementation |
Status |
| macOS 15 (Sequoia) min |
@available(macOS 14.0, *) on EnergyDomainPanel |
shipped; min could tighten to 15 if desired |
| Swift 6 strict concurrency |
swiftLanguageMode(.v6) on EnergyUI, EnergyLedger, EnergyAlertableEvents |
β |
Modules: EnergyGovernor / EnergyWitness / EnergyUI / EnergyReplication / AlertKit |
Targets named EnergyLedger / EnergyUI / EnergyAlertableEvents / (alert primitive in GaiaFTCLCore) / replication in GaiaNodeServerCore |
adapted; same separation, different names. AlertKit is shared in core because finance + energy both consume it. |
1. Concurrency / state architecture
| Spec |
Implementation |
Status |
@MainActor UI views |
EnergyGovernorModel is @MainActor @Observable; SwiftUI views run on main |
β |
actor LedgerBreakerEngine |
actor EnergyLedgerEngine (in EnergyLedger target) |
β same shape |
actor WitnessStore |
Split: EnergyLedgerEngine writes receipts; EnergySummitReader reads/writes summits + arm log; SubstrateDatabase owns the GRDB pool |
adapted; same single-writer discipline |
AsyncStream<LedgerTransition> UI bridge |
EnergyGovernorModel.transitions is @Observable and refreshes via refreshReceipts() after each enforce; UI observes property changes |
adapted; same outcome (UI updates without sync polling) |
| Sendable everywhere |
All structs (LedgerInput, LedgerReceipt, SummitRow, EnergyReceiptRow, AlertableValue, AlertRule) are Sendable value types |
β |
2. Domain models
| Spec name |
Implementation name |
Notes |
LedgerPartition |
LedgerInput (engine in/out via separate LedgerReceipt) |
same fields |
BreakerVerdict |
LedgerTerminalState enum + receipt fields |
functionally equivalent |
RefusalReason |
refused state recorded as terminal_state='refused' with witness columns showing input==output |
preserved as substrate state, not as Swift enum case |
LedgerTransition |
EnergyReceiptRow |
same data, different name |
SummitStatus / SummitState |
SummitRow + summit_states table |
β |
PreRegisteredPrediction |
columns on summit_states (effect_summary, predicted_values_json, success_criterion, null_result_clause, required_controls_json) |
denormalized into the table; trigger-immutable |
LabSubmission |
LabSubmissionRow + lab_submissions table |
β |
GovernorArmState |
EnergyGovernorModel.ArmState: disarmed/armedIdle/armedEnforcing |
β exact match |
3. SwiftUI surfaces
3.1 Cβ΄ rail entry β governor control
| Spec |
Implementation |
Status |
| DISARMED dimmed, single "Arm Governor" affordance |
armControl View; DISARMED shows gray + button "Arm Governor" + "Receipts shown while disarmed are stale-flagged" note |
β |
| ARMED+IDLE "listening" pulse |
shown as solid blue color + "Listening β no input." |
partial β color state β; explicit pulse animation deferred |
| ARMED+ENFORCING active |
green + "Enforcing input β Ξ active." |
β |
Toggling publishes gaiaftcl.energy.ledger.arm / .disarm |
EnergyGovernorModel.arm() / disarm() writes governor_arm_log AND ingests gaiaftcl.energy.governor.arm via AlertGovernor |
β |
| Append-only arm-log row |
governor_arm_log table with prev_arm_log_id chain + immutability trigger |
β |
| Stale flag on receipts when disarmed |
ReceiptRowView shows yellow "STALE" pill when model is disarmed |
β |
3.2 Live ledger readout
| Spec |
Implementation |
Status |
| Conserved bar Sβ | SαΆ with T marker |
conservedBar View; GeometryReader-driven proportional fill; T marker as white vertical line + "T" label |
β |
| Sβ green / amber / refused-red |
s4Color computes color from current state |
β |
.animation(.snappy) on partition |
.animation(reduceMotion ? nil : .snappy, value: β¦) |
β + accessibilityReduceMotion |
| Scrolling trace of last N |
recentReceipts View; ScrollView + LazyVStack; newest first; tap-able |
tap drill-in deferred to benchtop sheet |
| Swift Charts sweep view (Sβ + SαΆ vs input, RuleMark for T, PointMark for REFUSED) |
sweepChart View; LineMark for both dims + PointMark .cross for refused |
β (operator's xmark symbol replaced by .cross β RP equivalent) |
| Segmented control toggle |
Picker(selection:) with .segmented style between Conserved bar / Sweep chart |
β |
| Both read same stream |
model.transitions for the bar; model.currentSession for the sweep; both populated from same enforce() returns |
β |
| VoiceOver accessibility |
accessibilityLabel(accessibilityLabel(s4:sc:threshold:)) β narrates "S4 at X percent of threshold, S8 conserved at Y quanta, [state]" |
β |
3.3 Receipt surface
| Spec |
Implementation |
Status |
| Input / output partitions visible |
ReceiptRowView shows Sβ: 70 β 50 and SαΆ: 10 β 30 |
β |
| Sβ conservation check |
Image(systemName: conserves ? "checkmark.seal.fill" : "exclamationmark.triangle.fill") |
β |
| Verdict glyph |
terminal state pill colored by state |
β |
| Content-hash monospaced, copyable |
first 12 chars of witnessHashSHA256 with .textSelection(.enabled) |
β |
| Witnessed-live flag |
implicit via STALE pill (its inverse) |
adapted β same information |
| sealedAt timestamp |
applied_at_iso prefix(19) |
β |
| Disclosure with 3-command re-run |
NOT inline; will land in the upcoming Benchtop sheet |
named-next |
| Insert-only on sealed receipts |
substrate trigger trig_elr_witness_immutable enforces immutability |
β β at the SQL layer, not by missing UI methods |
3.4 Summit / replication board
| Spec |
Implementation |
Status |
| 3 cards in dependency order |
summitBoard HStack(spacing: 10) { ForEach(model.summits) }; ordered by ring ASC |
β |
| Status pill (4 states) |
StatusPill View; NAMED OPEN / IN REPLICATION / CLOSED Β· CONFIRMED / CLOSED Β· REFUTED |
β |
| REFUTED rendered as first-class outcome (violet, NOT alarm red) |
closedRefuted β Color(red: 0.55, green: 0.50, blue: 0.85) (violet); equal styling to confirmed |
β β explicit doctrinal honoring |
| Pre-registered prediction read-only with timestamp |
Text("Pre-registered \(formatDate(summit.preregisteredAtISO))") + Image(systemName: "lock.shield") |
β |
| Pre-registration immutable |
substrate trigger trig_summit_states_preregistration_immutable |
β |
| Submission log per summit |
not shown inline on cards |
named-next (drill-in sheet) |
| Dependency lock visible |
LockBadge overlay on summits whose dependency isn't closedConfirmed |
β explicit "locked until Ring N closed-confirmed" badge |
3.5 Alert queue surface
| Spec |
Implementation |
Status |
| Shared AlertKit primitive |
AlertGovernor + AlertableDomain protocol in GaiaFTCLCore |
β |
| Energy as producer (not bespoke) |
EnergyAlertableEvents declared as the SECOND domain (finance was first) |
β |
| Co-resident HOME queue view |
currently delivered through RSS feed + Apple notifications; no SwiftUI co-resident queue list |
named-next |
| Signal-colored rows |
rendered in RSS as [BAD] / [GOOD] / [INFO] prefixes |
β (RSS surface) |
| Witnessed-live proof binding |
event_payload_sha256 + snapshot_hash columns on alert_queue |
β |
| Spec |
Implementation |
Status |
MenuBarExtra arm state + unread count |
NOT implemented |
named-next |
4. Alert delivery
| Spec |
Implementation |
Status |
| Apple alert adapter |
AppleAlertAdapter in GaiaFTCLCore |
β |
UNUserNotificationCenter |
wrapped in #if canImport(UserNotifications) |
β |
| Signal β interruption level (bad=timeSensitive, good=passive, neutral=active) |
interruption(for:) |
β |
UNNotificationRequest userInfo includes domain / eventRef / signal / snapshotHash |
β in postNotification(_:) |
β |
Mark delivery_state = pushed |
markPushed(alertID:notifID:) writes alert_queue + alert_delivery_log row |
β |
Tap deep-link via openURL route |
userInfo["eventRef"] carried but the in-app URL handler gaiaftcl://energy/receipt/<id> is not wired |
named-next |
| Request authorization at first arm |
adapter requests at first drain() call |
partial β adapter-side, not strictly "at first arm" |
5. Lab-facing served package
| Spec |
Implementation |
Status |
GET /energy/replication HTML + JSON |
EnergyReplicationRenderer.renderReplicationHTML/JSON mounted in HTTPListener |
β |
GET /energy/summits/feed RSS 2.0 |
renderSummitStatusRSS mounted |
β |
POST /energy/summits/{slug}/witness |
HTTPListener routes to acceptWitnessSubmission(summitSlug:membraneToken:body:) |
β |
| Membrane-token authenticated |
ENERGY_LAB_TOKEN env var; constant-time compare; unauthorized β 401 |
β v1; per-lab token registry is named-next |
| Structured against pre-registered fields |
submission body decoded as JSON; fields land in measured_values_json |
β (full schema validation against predicted_values_json shape is named-next) |
replicationFeedPublic flag |
omitted in v1 β feeds are local-private by default (127.0.0.1 binding on the listener) |
adapted β same outcome via network binding, not via a feature flag |
6. SwiftData model layer
| Spec |
Implementation |
Status |
@Model classes |
NOT used |
deliberate adaptation β see TL;DR |
| Sealed-records discipline |
enforced at the substrate layer via SQL triggers (witness columns immutable, append-only logs) |
β β same constitutional outcome |
| Content-hashed snapshots |
witness_hash_sha256 / snapshot_hash columns; computed via WitnessHasher.sha256Hex |
β |
7. Design system
| Spec |
Implementation |
Status |
Semantic color tokens in asset catalog (gaiaManifest, gaiaConstraint, gaiaPass, gaiaAmber, gaiaRefuse, gaiaTotal) |
Currently inline Color(red:green:blue:) matching the spec's intent |
named-next: extract to asset catalog tokens |
| Dynamic Type throughout |
fixed .font(.system(size: N)) |
named-next: switch to .body / .caption semantic sizes |
| Dark/light via asset catalog |
panel ships its own dark background; works dark only in v1 |
named-next: full asset-catalog support |
| Reduce-motion honored |
@Environment(\.accessibilityReduceMotion) on the bar animation |
β |
| VoiceOver |
accessibility label on the bar with numeric content |
β |
8. Test suite (Swift Testing)
| Spec idiom |
Implementation idiom |
Status |
@Test annotations with #expect |
executableTarget mains under Sources/M8β¦SmokeTest/main.swift printing [OK] / [FAIL] |
adapted β same invariants exercised |
| 6 spec-named tests (breaker repartition, refusal preserves conservation, disarmed stales, lab submission auth, null-result-closes) |
All 6 invariants covered across M8EnergyLedgerSmokeTest + M8WitnessAlertSmokeTest + M8MetricAuditGateTest |
β functionally |
| Lean kernel + Swift gate same invariants |
M8EnergyLedgerSmokeTest exercises the same three instances the Lean theorems reduce by decide; the substrate CHECK refuses any divergence |
β β dual-gate discipline holds |
9. Build / ship checklist
| Spec |
Implementation |
Status |
| Zero data-race warnings |
swift build clean |
β |
No @unchecked Sendable |
none |
β |
gaiaftcl.* subjects spelled correctly |
proof/scripts/check_nats_subject_spelling.sh greps on the pattern; build can wire this |
β |
| SQLite witness store only |
SubstrateDatabase.shared.pool() |
β |
| No ArangoDB / no external DB / no external API |
none |
β |
| Submission requires membrane token |
401 without ENERGY_LAB_TOKEN |
β |
| Reduce-motion + VoiceOver verified |
β on the bar |
β |
| Inventory audit run |
swift run M8InventoryAuditor β COMPLETE |
β |
| Notification authorization at first arm |
adapter-side at first drain() |
partial |
What the next operator should do
To bring this from "core complete + named gaps" to "full spec compliance":
MenuBarExtra with governor.armState.glyph + unread alert count β opens HOME to the energy surface.- Receipt detail sheet with the inline three-command repro string. Wire
gaiaftcl://energy/receipt/<id> URL handler in GaiaFTCLApp to open the sheet.
- Summit drill-in card showing the
lab_submissions log for one summit with pending/sealed_confirm/sealed_refute actions for the operator.
- Asset-catalog color tokens β extract every inline
Color(red:β¦) into a Colors.xcassets with semantic names. Dynamic Type pass at the same time.
- ARMED+IDLE pulse β
withAnimation(.easeInOut.repeatForever(autoreverses: true)) on the arm-control accent.
- Swift Testing
@Test migration β rewrap the three smoke tests as @Test functions in a M8EnergyTests package.
- Per-lab membrane token registry with revocation + audit (in
lab_credentials table; current ENERGY_LAB_TOKEN env-var is the v1 anchor).
Federation-cosigned
This page's source is sealed in the GaiaFTCL federation manifest β page SHA-256 b365b11d7a8c7fafβ¦, manifest witness a090592e0609adc8β¦, signed 2026-06-02T18:58:22Z by cell gaiaftcl-mac-cell. Verify with gaiaftcl wiki sign --all and compare wiki-all-signatures.json.