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 (
MenuBarExtrawith 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
0. Platform / tooling
| 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 |
✓ |
3.6 Menu bar extra
| 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":
1. MenuBarExtra with governor.armState.glyph + unread alert count → opens HOME to the energy surface.
2. Receipt detail sheet with the inline three-command repro string. Wire gaiaftcl://energy/receipt/<id> URL handler in GaiaFTCLApp to open the sheet.
3. Summit drill-in card showing the lab_submissions log for one summit with pending/sealed_confirm/sealed_refute actions for the operator.
4. Asset-catalog color tokens — extract every inline Color(red:…) into a Colors.xcassets with semantic names. Dynamic Type pass at the same time.
5. ARMED+IDLE pulse — withAnimation(.easeInOut.repeatForever(autoreverses: true)) on the arm-control accent.
6. Swift Testing @Test migration — rewrap the three smoke tests as @Test functions in a M8EnergyTests package.
7. Per-lab membrane token registry with revocation + audit (in lab_credentials table; current ENERGY_LAB_TOKEN env-var is the v1 anchor).
Federation cosignature: pending operator signing host (v26).
Witness (sha256 of rendered body):
4a61e11206d5231d87f76cf429d409eb329704dbfc5f6a6c27f352eee627c007.
This page serves with a substrate-honest pending-signature notice until the operator's Franklin signer cosigns it.