feat(sample-app): ledger spec parity (#18)

* feat(sample-app): add FocusTracker

* feat(sample-app): support description on TextInput

* feat(sample-app): support description on AppButton and Segmented

* feat(sample-app): stable ids on login screen

* feat(sample-app): stable ids on add-account screen

* feat(sample-app): stable ids on add-transaction screen

* feat(sample-app): stable ids on home and ledger screens

* feat(sample-app): hoist error + form state into UiState

* feat(sample-app): register auth_status + accounts snapshots

* feat(sample-app): register ledger_rows + ledger_balance snapshots

* feat(sample-app): register error + focused_input snapshots

* refactor(sample-app): scaffold spec.ts extractors + safety

* feat(sample-app): spec accounting invariants

* feat(sample-app): spec state-machine monotonicity

* feat(sample-app): spec liveness properties

* feat(sample-app): spec auth + account action generators

* feat(sample-app): spec transaction action generators

* feat(sample-app): spec weighted workflow

* feat(sample-app): publish login form input snapshots

* feat(sample-app): publish account + txn input snapshots

* feat(sample-app): register form input snapshots

* fix(sample-app): sequence login + idempotent text inputs in spec

* fix(sample-app): clear UiState on page dispose

* fix(sample-app): tighten adversarial login, allow retype on error

* test(verifier): update sample-app spec integration for new selectors

* feat(sidecar): clear focused field before InputText types

* refactor(sample-app): simplify loginHelper to focus-driven sequencing

* refactor(sample-app): drop input-value UiState mirrors

* refactor(sample-app): drop input-value snapshot registrations

* test(verifier): adjust sample-app integration for replace-on-type

examples/sample-app/composeApp/src/androidMain/kotlin/dev/uatu/sample/SampleApplication.kt

@@ -22,6 +22,64 @@ class SampleApplication : Application() {
                 is Route.AddTransaction -> "add-transaction"
             }
         }
+        Uatu.extract("auth_status") {
+            if (Repository.session.value != null) "logged-in" else "logged-out"
+        }
+        Uatu.extract("accounts") {
+            val txns = Repository.transactions.value
+            Repository.accounts.value.map { a ->
+                val rows = txns.filter { it.accountId == a.id }
+                mapOf(
+                    "id" to a.id,
+                    "name" to a.name,
+                    "balance" to balanceOf(rows),
+                    "txnCount" to rows.size,
+                )
+            }
+        }
+        Uatu.extract("active_account_id") {
+            when (val r = Navigator.current.value) {
+                is Route.Ledger -> r.accountId
+                is Route.AddTransaction -> r.accountId
+                else -> null
+            }
+        }
+        Uatu.extract("ledger_rows") {
+            val active = when (val r = Navigator.current.value) {
+                is Route.Ledger -> r.accountId
+                is Route.AddTransaction -> r.accountId
+                else -> null
+            }
+            if (active == null) emptyList()
+            else Repository.transactions.value
+                .filter { it.accountId == active }
+                .map {
+                    mapOf(
+                        "id" to it.id,
+                        "accountId" to it.accountId,
+                        "type" to if (it.type == TxnType.credit) "credit" else "debit",
+                        "amount" to it.amount,
+                        "signed" to signedAmount(it),
+                    )
+                }
+        }
+        Uatu.extract("ledger_balance") {
+            val active = when (val r = Navigator.current.value) {
+                is Route.Ledger -> r.accountId
+                is Route.AddTransaction -> r.accountId
+                else -> null
+            }
+            if (active == null) 0L
+            else balanceOf(Repository.transactions.value.filter { it.accountId == active })
+        }
+        Uatu.extract("focused_input") { FocusTracker.current.value }
+        Uatu.extract("txn_form_type") { UiState.txnFormType.value }
+        Uatu.extract("txn_form_account_id") {
+            (Navigator.current.value as? Route.AddTransaction)?.accountId
+        }
+        Uatu.extract("login_error") { UiState.loginError.value }
+        Uatu.extract("add_account_error") { UiState.addAccountError.value }
+        Uatu.extract("txn_error") { UiState.txnError.value }
         maybeInjectDebugError()
     }
 

examples/sample-app/composeApp/src/commonMain/kotlin/dev/uatu/sample/FocusTracker.kt

@@ -0,0 +1,18 @@
+package dev.uatu.sample
+
+import kotlinx.coroutines.flow.MutableStateFlow
+import kotlinx.coroutines.flow.StateFlow
+import kotlinx.coroutines.flow.asStateFlow
+
+object FocusTracker {
+    private val _current = MutableStateFlow<String?>(null)
+    val current: StateFlow<String?> = _current.asStateFlow()
+
+    fun enter(id: String) {
+        _current.value = id
+    }
+
+    fun leave(id: String) {
+        if (_current.value == id) _current.value = null
+    }
+}

examples/sample-app/composeApp/src/commonMain/kotlin/dev/uatu/sample/UiState.kt

@@ -0,0 +1,10 @@
+package dev.uatu.sample
+
+import kotlinx.coroutines.flow.MutableStateFlow
+
+object UiState {
+    val loginError = MutableStateFlow("")
+    val addAccountError = MutableStateFlow("")
+    val txnError = MutableStateFlow("")
+    val txnFormType = MutableStateFlow<String?>(null)
+}

examples/sample-app/composeApp/src/commonMain/kotlin/dev/uatu/sample/ui/AddAccount.kt

@@ -6,6 +6,8 @@ import androidx.compose.foundation.layout.fillMaxWidth
 import androidx.compose.foundation.layout.padding
 import androidx.compose.material3.Text
 import androidx.compose.runtime.Composable
+import androidx.compose.runtime.DisposableEffect
+import androidx.compose.runtime.collectAsState
 import androidx.compose.runtime.getValue
 import androidx.compose.runtime.mutableStateOf
 import androidx.compose.runtime.remember
@@ -15,28 +17,34 @@ import androidx.compose.ui.unit.dp
 import dev.uatu.sample.Navigator
 import dev.uatu.sample.Repository
 import dev.uatu.sample.Route
+import dev.uatu.sample.UiState
 
 @Composable
 fun AddAccountPage() {
     val t = LocalTokens.current
     var name by remember { mutableStateOf("") }
-    var err by remember { mutableStateOf<String?>(null) }
+    val err by UiState.addAccountError.collectAsState()
 
     BackHandler { Navigator.back(Route.Home) }
 
+    DisposableEffect(Unit) {
+        onDispose { UiState.addAccountError.value = "" }
+    }
+
     fun submit() {
         val trimmed = name.trim()
         if (trimmed.isEmpty()) {
-            err = "Account name is required"; return
+            UiState.addAccountError.value = "Account name is required"; return
         }
         if (trimmed.length > 40) {
-            err = "Name is too long (max 40 characters)"; return
+            UiState.addAccountError.value = "Name is too long (max 40 characters)"; return
         }
         try {
             Repository.createAccount(trimmed)
+            UiState.addAccountError.value = ""
             Navigator.replace(Route.Home)
         } catch (e: IllegalArgumentException) {
-            err = e.message ?: "Could not create account"
+            UiState.addAccountError.value = e.message ?: "Could not create account"
         }
     }
 
@@ -50,6 +58,7 @@ fun AddAccountPage() {
                 onClick = ::submit,
                 style = ButtonStyle.Primary,
                 enabled = name.trim().isNotEmpty(),
+                description = "add_account_submit",
             )
         },
     ) {
@@ -61,10 +70,11 @@ fun AddAccountPage() {
                 FieldLabel("Account name")
                 TextInput(
                     value = name,
-                    onChange = { name = it; err = null },
+                    onChange = { name = it; UiState.addAccountError.value = "" },
                     placeholder = "e.g. Checking",
-                    invalid = err != null,
+                    invalid = err.isNotEmpty(),
                     label = "Account name",
+                    description = "account_name_field",
                 )
             }
             ErrorText(err)

examples/sample-app/composeApp/src/commonMain/kotlin/dev/uatu/sample/ui/AddTransaction.kt

@@ -5,6 +5,7 @@ import androidx.compose.foundation.layout.Column
 import androidx.compose.foundation.layout.fillMaxWidth
 import androidx.compose.foundation.layout.padding
 import androidx.compose.runtime.Composable
+import androidx.compose.runtime.DisposableEffect
 import androidx.compose.runtime.getValue
 import androidx.compose.runtime.collectAsState
 import androidx.compose.runtime.mutableStateOf
@@ -18,6 +19,7 @@ import dev.uatu.sample.Navigator
 import dev.uatu.sample.Repository
 import dev.uatu.sample.Route
 import dev.uatu.sample.TxnType
+import dev.uatu.sample.UiState
 import dev.uatu.sample.parseCents
 
 private val AMOUNT_REGEX = Regex("""^\d*(\.\d{0,2})?$""")
@@ -48,21 +50,31 @@ fun AddTransactionPage(accountId: String) {
     var type by remember { mutableStateOf(TxnType.credit) }
     var amount by remember { mutableStateOf("") }
     var note by remember { mutableStateOf("") }
-    var err by remember { mutableStateOf<String?>(null) }
+    val err by UiState.txnError.collectAsState()
+
+    DisposableEffect(type) {
+        UiState.txnFormType.value = if (type == TxnType.credit) "credit" else "debit"
+        onDispose { UiState.txnFormType.value = null }
+    }
+
+    DisposableEffect(Unit) {
+        onDispose { UiState.txnError.value = "" }
+    }
 
     fun submit() {
         val cents = parseCents(amount)
         if (cents == null) {
-            err = "Enter a valid amount (e.g. 12.34)"; return
+            UiState.txnError.value = "Enter a valid amount (e.g. 12.34)"; return
         }
         if (cents <= 0) {
-            err = "Amount must be greater than zero"; return
+            UiState.txnError.value = "Amount must be greater than zero"; return
         }
         try {
             Repository.createTransaction(accountId, type, cents, note)
+            UiState.txnError.value = ""
             Navigator.back(Route.Home)
         } catch (e: IllegalArgumentException) {
-            err = e.message ?: "Could not save transaction"
+            UiState.txnError.value = e.message ?: "Could not save transaction"
         }
     }
 
@@ -80,6 +92,7 @@ fun AddTransactionPage(accountId: String) {
                 onClick = ::submit,
                 style = ButtonStyle.Primary,
                 enabled = amount.isNotBlank(),
+                description = "txn_submit",
             )
         },
     ) {
@@ -91,6 +104,7 @@ fun AddTransactionPage(accountId: String) {
                 selected = if (type == TxnType.credit) 0 else 1,
                 labels = listOf("Credit", "Debit"),
                 onSelect = { type = if (it == 0) TxnType.credit else TxnType.debit },
+                descriptions = listOf("txn_credit", "txn_debit"),
             )
             Column(verticalArrangement = Arrangement.spacedBy(6.dp)) {
                 FieldLabel("Amount")
@@ -98,15 +112,17 @@ fun AddTransactionPage(accountId: String) {
                     value = amount,
                     onChange = {
                         if (AMOUNT_REGEX.matches(it) || it.isEmpty()) {
-                            amount = it; err = null
+                            amount = it
+                            UiState.txnError.value = ""
                         }
                     },
                     placeholder = "0.00",
-                    invalid = err != null,
+                    invalid = err.isNotEmpty(),
                     keyboardType = KeyboardType.Decimal,
                     textAlign = TextAlign.Center,
                     textStyle = Type.amountInput,
                     label = "Amount",
+                    description = "txn_amount",
                 )
             }
             Column(verticalArrangement = Arrangement.spacedBy(6.dp)) {
@@ -116,6 +132,7 @@ fun AddTransactionPage(accountId: String) {
                     onChange = { note = it.take(80) },
                     placeholder = "What's this for?",
                     label = "Note",
+                    description = "txn_note",
                 )
             }
             ErrorText(err)

examples/sample-app/composeApp/src/commonMain/kotlin/dev/uatu/sample/ui/Home.kt

@@ -44,7 +44,7 @@ fun HomePage(user: String, onLogout: () -> Unit) {
                 title = "Accounts",
                 subtitle = user,
                 right = {
-                    IconButton(onClick = onLogout, description = "Sign out", icon = Icons.Logout)
+                    IconButton(onClick = onLogout, description = "logout_button", icon = Icons.Logout)
                 },
             )
         },
@@ -65,6 +65,7 @@ fun HomePage(user: String, onLogout: () -> Unit) {
                 text = "+ Add account",
                 onClick = { Navigator.push(Route.AddAccount) },
                 style = ButtonStyle.Primary,
+                description = "add_account_button",
             )
         },
     ) {
@@ -80,6 +81,7 @@ fun HomePage(user: String, onLogout: () -> Unit) {
                     val bal = txns.filter { it.accountId == a.id }.sumOf { signedAmount(it) }
                     val count = txns.count { it.accountId == a.id }
                     AccountCard(
+                        id = a.id,
                         name = a.name,
                         initials = initialsOf(a.name),
                         count = count,
@@ -94,6 +96,7 @@ fun HomePage(user: String, onLogout: () -> Unit) {
 
 @Composable
 private fun AccountCard(
+    id: String,
     name: String,
     initials: String,
     count: Int,
@@ -102,14 +105,13 @@ private fun AccountCard(
 ) {
     val t = LocalTokens.current
     val txnLabel = if (count == 1) "1 transaction" else "$count transactions"
-    val a11y = "$name account, balance ${formatCents(balance)}, $txnLabel"
     Row(
         modifier = Modifier
             .fillMaxWidth()
             .clip(RoundedCornerShape(RadiusLg))
             .background(t.surface)
             .border(1.dp, t.border, RoundedCornerShape(RadiusLg))
-            .semantics(mergeDescendants = true) { contentDescription = a11y }
+            .semantics(mergeDescendants = true) { contentDescription = "account_card:$id" }
             .clickable(role = Role.Button, onClick = onClick)
             .padding(16.dp),
         verticalAlignment = Alignment.CenterVertically,

examples/sample-app/composeApp/src/commonMain/kotlin/dev/uatu/sample/ui/Ledger.kt

@@ -74,6 +74,7 @@ fun LedgerPage(accountId: String) {
                 text = "+ Add transaction",
                 onClick = { Navigator.push(Route.AddTransaction(accountId)) },
                 style = ButtonStyle.Primary,
+                description = "add_txn_button",
             )
         },
     ) {
@@ -103,7 +104,7 @@ fun LedgerPage(accountId: String) {
                     .padding(horizontal = 16.dp),
             ) {
                 txns.forEachIndexed { i, txn ->
-                    TxnRow(txn.type, txn.amount, txn.note, formatDate(txn.createdAt))
+                    TxnRow(txn.id, txn.type, txn.amount, txn.note, formatDate(txn.createdAt))
                     if (i != txns.lastIndex) {
                         Box(Modifier.fillMaxWidth().height(1.dp).background(t.border))
                     }
@@ -114,16 +115,14 @@ fun LedgerPage(accountId: String) {
 }
 
 @Composable
-private fun TxnRow(type: TxnType, amount: Long, note: String, date: String) {
+private fun TxnRow(id: String, type: TxnType, amount: Long, note: String, date: String) {
     val t = LocalTokens.current
     val signed = if (type == TxnType.credit) amount else -amount
-    val label = "${if (type == TxnType.credit) "Credit" else "Debit"} ${formatCents(signed, signed = true)}" +
-        (if (note.isNotEmpty()) ", $note" else "") + ", $date"
     Row(
         modifier = Modifier
             .fillMaxWidth()
             .padding(vertical = 14.dp)
-            .semantics(mergeDescendants = true) { contentDescription = label },
+            .semantics(mergeDescendants = true) { contentDescription = "txn_row:$id" },
         verticalAlignment = Alignment.CenterVertically,
         horizontalArrangement = Arrangement.spacedBy(12.dp),
     ) {

examples/sample-app/composeApp/src/commonMain/kotlin/dev/uatu/sample/ui/Login.kt

@@ -8,6 +8,8 @@ import androidx.compose.foundation.layout.height
 import androidx.compose.foundation.layout.padding
 import androidx.compose.material3.Text
 import androidx.compose.runtime.Composable
+import androidx.compose.runtime.DisposableEffect
+import androidx.compose.runtime.collectAsState
 import androidx.compose.runtime.getValue
 import androidx.compose.runtime.mutableStateOf
 import androidx.compose.runtime.remember
@@ -18,6 +20,7 @@ import androidx.compose.ui.unit.dp
 import dev.uatu.sample.DEMO_EMAIL
 import dev.uatu.sample.DEMO_PASSWORD
 import dev.uatu.sample.Repository
+import dev.uatu.sample.UiState
 import dev.uatu.sample.checkCredentials
 
 @Composable
@@ -25,15 +28,20 @@ fun LoginPage(onLoggedIn: (String) -> Unit) {
     val t = LocalTokens.current
     var email by remember { mutableStateOf("") }
     var password by remember { mutableStateOf("") }
-    var err by remember { mutableStateOf<String?>(null) }
+    val err by UiState.loginError.collectAsState()
+
+    DisposableEffect(Unit) {
+        onDispose { UiState.loginError.value = "" }
+    }
 
     fun submit() {
         if (email.isBlank() || password.isEmpty()) {
-            err = "Enter email and password"; return
+            UiState.loginError.value = "Enter email and password"; return
         }
         if (!checkCredentials(email, password)) {
-            err = "Invalid email or password"; return
+            UiState.loginError.value = "Invalid email or password"; return
         }
+        UiState.loginError.value = ""
         val user = email.trim().lowercase()
         Repository.setSession(user)
         onLoggedIn(user)
@@ -49,23 +57,25 @@ fun LoginPage(onLoggedIn: (String) -> Unit) {
                 FieldLabel("Email")
                 TextInput(
                     value = email,
-                    onChange = { email = it; err = null },
+                    onChange = { email = it; UiState.loginError.value = "" },
                     placeholder = DEMO_EMAIL,
-                    invalid = err != null,
+                    invalid = err.isNotEmpty(),
                     keyboardType = KeyboardType.Email,
                     label = "Email",
+                    description = "login_email",
                 )
             }
             Column(verticalArrangement = Arrangement.spacedBy(6.dp)) {
                 FieldLabel("Password")
                 TextInput(
                     value = password,
-                    onChange = { password = it; err = null },
+                    onChange = { password = it; UiState.loginError.value = "" },
                     placeholder = "••••••••",
                     password = true,
-                    invalid = err != null,
+                    invalid = err.isNotEmpty(),
                     keyboardType = KeyboardType.Password,
                     label = "Password",
+                    description = "login_password",
                 )
             }
             ErrorText(err)
@@ -73,6 +83,7 @@ fun LoginPage(onLoggedIn: (String) -> Unit) {
                 text = "Sign in",
                 onClick = ::submit,
                 style = ButtonStyle.Primary,
+                description = "login_submit",
             )
             Spacer(Modifier.height(4.dp))
             Card(dashed = true) {

examples/sample-app/composeApp/src/commonMain/kotlin/dev/uatu/sample/ui/Widgets.kt

@@ -36,6 +36,7 @@ import androidx.compose.ui.text.input.PasswordVisualTransformation
 import androidx.compose.ui.text.input.VisualTransformation
 import androidx.compose.ui.text.style.TextAlign
 import androidx.compose.ui.unit.dp
+import dev.uatu.sample.FocusTracker
 
 enum class ButtonStyle { Primary, Secondary, Ghost }
 
@@ -46,6 +47,7 @@ fun AppButton(
     modifier: Modifier = Modifier,
     style: ButtonStyle = ButtonStyle.Secondary,
     enabled: Boolean = true,
+    description: String? = null,
 ) {
     val t = LocalTokens.current
     val (bg, fg, border) = when (style) {
@@ -59,6 +61,10 @@ fun AppButton(
             .clip(RoundedCornerShape(RadiusMd))
             .background(if (enabled) bg else t.surface3)
             .border(BorderStroke(1.dp, if (enabled) border else t.border), RoundedCornerShape(RadiusMd))
+            .then(
+                if (description != null) Modifier.semantics { contentDescription = description }
+                else Modifier
+            )
             .clickable(enabled = enabled, role = Role.Button, onClick = onClick)
             .padding(vertical = 14.dp, horizontal = 16.dp),
         contentAlignment = Alignment.Center,
@@ -84,6 +90,7 @@ fun TextInput(
     textAlign: TextAlign = TextAlign.Start,
     textStyle: TextStyle = Type.body,
     label: String? = null,
+    description: String? = null,
     modifier: Modifier = Modifier,
 ) {
     val t = LocalTokens.current
@@ -116,9 +123,16 @@ fun TextInput(
             cursorBrush = SolidColor(t.text),
             modifier = Modifier
                 .fillMaxWidth()
-                .onFocusChanged { focused = it.isFocused }
+                .onFocusChanged {
+                    focused = it.isFocused
+                    if (description != null) {
+                        if (it.isFocused) FocusTracker.enter(description)
+                        else FocusTracker.leave(description)
+                    }
+                }
                 .semantics {
-                    if (label != null) contentDescription = label
+                    val desc = description ?: label
+                    if (desc != null) contentDescription = desc
                     if (invalid) stateDescription = "Invalid"
                 },
         )
@@ -155,7 +169,12 @@ fun ErrorText(err: String?) {
 }
 
 @Composable
-fun Segmented(selected: Int, labels: List<String>, onSelect: (Int) -> Unit) {
+fun Segmented(
+    selected: Int,
+    labels: List<String>,
+    onSelect: (Int) -> Unit,
+    descriptions: List<String>? = null,
+) {
     val t = LocalTokens.current
     Row(
         modifier = Modifier
@@ -168,12 +187,16 @@ fun Segmented(selected: Int, labels: List<String>, onSelect: (Int) -> Unit) {
     ) {
         labels.forEachIndexed { i, label ->
             val active = i == selected
+            val desc = descriptions?.getOrNull(i)
             Box(
                 modifier = Modifier
                     .weight(1f)
                     .clip(RoundedCornerShape(RadiusSm))
                     .background(if (active) t.surface3 else t.surface)
-                    .semantics { this.selected = active }
+                    .semantics {
+                        this.selected = active
+                        if (desc != null) contentDescription = desc
+                    }
                     .clickable(role = Role.Tab) { onSelect(i) }
                     .padding(vertical = 10.dp),
                 contentAlignment = Alignment.Center,

examples/sample-app/spec.ts

@@ -14,89 +14,424 @@ import {
   waitOnce,
   weighted,
 } from "@uatu/spec";
-import { noUncaughtExceptions } from "@uatu/spec/defaults/properties";
+import { noLogcatErrors, noUncaughtExceptions } from "@uatu/spec/defaults/properties";
+
+interface AccountSnapshot {
+  id: string;
+  name: string;
+  balance: number;
+  txnCount: number;
+}
+
+interface LedgerRow {
+  id: string;
+  accountId: string;
+  type: "credit" | "debit";
+  amount: number;
+  signed: number;
+}
 
-// ── Snapshot extractors (fed by SampleApplication.kt) ──────────
 const loggedIn = extract<boolean>(
   (state) => (state.snapshots.logged_in as boolean) ?? false,
 );
+const authStatus = extract<string>(
+  (state) => (state.snapshots.auth_status as string) ?? "",
+);
 const route = extract<string>(
   (state) => (state.snapshots.route as string) ?? "",
 );
+const accounts = extract<AccountSnapshot[]>(
+  (state) => (state.snapshots.accounts as AccountSnapshot[]) ?? [],
+);
+const totalBalance = extract<number>(
+  (state) => (state.snapshots.total_balance as number) ?? 0,
+);
 const accountCount = extract<number>(
   (state) => (state.snapshots.account_count as number) ?? 0,
 );
+const activeAccountId = extract<string | null>(
+  (state) => (state.snapshots.active_account_id as string | null) ?? null,
+);
+const ledgerRows = extract<LedgerRow[]>(
+  (state) => (state.snapshots.ledger_rows as LedgerRow[]) ?? [],
+);
+const ledgerBalance = extract<number>(
+  (state) => (state.snapshots.ledger_balance as number) ?? 0,
+);
+const focusedInput = extract<string | null>(
+  (state) => (state.snapshots.focused_input as string | null) ?? null,
+);
+const txnFormType = extract<string | null>(
+  (state) => (state.snapshots.txn_form_type as string | null) ?? null,
+);
+const txnFormAccountId = extract<string | null>(
+  (state) => (state.snapshots.txn_form_account_id as string | null) ?? null,
+);
+const loginError = extract<string>(
+  (state) => (state.snapshots.login_error as string) ?? "",
+);
+const addAccountError = extract<string>(
+  (state) => (state.snapshots.add_account_error as string) ?? "",
+);
+const txnError = extract<string>(
+  (state) => (state.snapshots.txn_error as string) ?? "",
+);
+const loginEmailField = extract((state) => state.ax.find("desc:login_email"));
+const loginPasswordField = extract((state) => state.ax.find("desc:login_password"));
+const loginSubmitButton = extract((state) => state.ax.find("desc:login_submit"));
+const addAccountButton = extract((state) => state.ax.find("desc:add_account_button"));
+const logoutButton = extract((state) => state.ax.find("desc:logout_button"));
+const accountNameField = extract((state) => state.ax.find("desc:account_name_field"));
+const addAccountSubmit = extract((state) => state.ax.find("desc:add_account_submit"));
+const addTxnButton = extract((state) => state.ax.find("desc:add_txn_button"));
+const txnAmountField = extract((state) => state.ax.find("desc:txn_amount"));
+const txnNoteField = extract((state) => state.ax.find("desc:txn_note"));
+const txnCredit = extract((state) => state.ax.find("desc:txn_credit"));
+const txnDebit = extract((state) => state.ax.find("desc:txn_debit"));
+const txnSubmit = extract((state) => state.ax.find("desc:txn_submit"));
+const backButton = extract((state) => state.ax.find("desc:Back"));
+const anyAccountCard = extract((state) => state.ax.find("descPrefix:account_card:"));
 
-// ── UI elements ────────────────────────────────────────────────
-const phoneField = extract((state) => state.ax.find("desc:phone_field"));
-const continueButton = extract((state) => state.ax.find("text:Continue"));
-const addAccountButton = extract((state) => state.ax.find("text:Add account"));
-const nameField = extract((state) => state.ax.find("desc:account_name"));
-const createButton = extract((state) => state.ax.find("text:Create"));
-
-// ── Properties ─────────────────────────────────────────────────
-// accountCountNonNegative: the trivial safety property.
 const accountCountNonNegative = always(() => accountCount.current >= 0);
 
-// addAccountAdvances: once we land on add-account, the next step must be on
-// a different screen. Exercises now(x).implies(next(y)).
-const addAccountAdvances = always(
-  now(() => route.current === "add-account").implies(
-    next(() => route.current !== "add-account"),
+const onHome = () => route.current === "home";
+const onLedger = () =>
+  route.current === "ledger" || route.current === "add-transaction";
+const isInteger = (n: number) => Number.isFinite(n) && Math.floor(n) === n;
+
+const totalBalanceMatchesAccounts = always(
+  now(onHome).implies(
+    now(() => {
+      const sum = accounts.current.reduce((acc, a) => acc + a.balance, 0);
+      return sum === totalBalance.current;
+    }),
   ),
 );
 
-// eventuallyLoggedIn: within 30 seconds of the run starting, we expect to
-// reach home. Exercises eventually(p).within(n, unit).
-const eventuallyLoggedIn = eventually(() => loggedIn.current).within(
-  30,
-  "seconds",
+const ledgerBalanceMatchesRows = always(
+  now(onLedger).implies(
+    now(() => {
+      const sum = ledgerRows.current.reduce((acc, r) => acc + r.signed, 0);
+      return sum === ledgerBalance.current;
+    }),
+  ),
 );
 
+const ledgerRowsWellFormed = always(() => {
+  for (const row of ledgerRows.current) {
+    if (row.type !== "credit" && row.type !== "debit") return false;
+    if (!(row.amount > 0)) return false;
+    const expected = row.type === "credit" ? row.amount : -row.amount;
+    if (row.signed !== expected) return false;
+  }
+  return true;
+});
+
+const balancesAreIntegerCents = always(() => {
+  if (!isInteger(totalBalance.current)) return false;
+  if (!isInteger(ledgerBalance.current)) return false;
+  for (const a of accounts.current) if (!isInteger(a.balance)) return false;
+  for (const r of ledgerRows.current) {
+    if (!isInteger(r.amount) || !isInteger(r.signed)) return false;
+  }
+  return true;
+});
+
+const accountCountMatchesList = always(
+  () => accountCount.current === accounts.current.length,
+);
+
+const ledgerCountMatchesRows = always(
+  now(onLedger).implies(
+    now(() => {
+      const active = activeAccountId.current;
+      if (active === null) return true;
+      const fromAccounts = accounts.current.find((a) => a.id === active);
+      if (!fromAccounts) return true;
+      return fromAccounts.txnCount === ledgerRows.current.length;
+    }),
+  ),
+);
+
+const zeroTxnsMeansZeroBalance = always(() => {
+  for (const a of accounts.current) {
+    if (a.txnCount === 0 && a.balance !== 0) return false;
+  }
+  return true;
+});
+
+const noOrphanTransactions = always(() => {
+  const active = activeAccountId.current;
+  if (active === null) return ledgerRows.current.length === 0;
+  return ledgerRows.current.every((r) => r.accountId === active);
+});
+
+const uniqueAccountNames = always(() => {
+  const seen = new Set<string>();
+  for (const a of accounts.current) {
+    const key = a.name.trim().toLowerCase();
+    if (seen.has(key)) return false;
+    seen.add(key);
+  }
+  return true;
+});
+
+const accountingInvariants = {
+  totalBalanceMatchesAccounts,
+  ledgerBalanceMatchesRows,
+  ledgerRowsWellFormed,
+  balancesAreIntegerCents,
+  accountCountMatchesList,
+  ledgerCountMatchesRows,
+  zeroTxnsMeansZeroBalance,
+  noOrphanTransactions,
+  uniqueAccountNames,
+};
+
+const accountsOnlyGrow = always(
+  now(() => true).implies(
+    next(() => accounts.current.length >= (accounts.previous?.length ?? 0)),
+  ),
+);
+
+const ledgerOnlyGrowsPerAccount = always(
+  now(() => activeAccountId.current !== null).implies(
+    next(() => {
+      if (activeAccountId.current !== activeAccountId.previous) return true;
+      return ledgerRows.current.length >= (ledgerRows.previous?.length ?? 0);
+    }),
+  ),
+);
+
+const authStatusIsKnown = always(
+  () => authStatus.current === "logged-in" || authStatus.current === "logged-out",
+);
+
+const routeIsKnown = always(() => {
+  const r = route.current;
+  return (
+    r === "login" ||
+    r === "home" ||
+    r === "add-account" ||
+    r === "ledger" ||
+    r === "add-transaction"
+  );
+});
+
+const loggedInLeavesLogin = always(
+  now(() => loggedIn.current).implies(
+    eventually(() => route.current !== "login").within(3, "seconds"),
+  ),
+);
+
+const loggedOutReachesLogin = always(
+  now(() => !loggedIn.current).implies(
+    eventually(() => route.current === "login").within(3, "seconds"),
+  ),
+);
+
+const stateMachine = {
+  accountsOnlyGrow,
+  ledgerOnlyGrowsPerAccount,
+  authStatusIsKnown,
+  routeIsKnown,
+  loggedInLeavesLogin,
+  loggedOutReachesLogin,
+};
+
+const loginReachable = eventually(() => loggedIn.current).within(90, "seconds");
+const accountCreationReachable = eventually(
+  () => accounts.current.length > 0,
+).within(180, "seconds");
+const someTransactionExists = eventually(() =>
+  accounts.current.some((a) => a.txnCount > 0),
+).within(300, "seconds");
+
+const loginErrorClears = always(
+  now(() => loginError.current !== "").implies(
+    eventually(() => loginError.current === "").within(30, "seconds"),
+  ),
+);
+const addAccountErrorClears = always(
+  now(() => addAccountError.current !== "").implies(
+    eventually(() => addAccountError.current === "").within(30, "seconds"),
+  ),
+);
+const txnErrorClears = always(
+  now(() => txnError.current !== "").implies(
+    eventually(() => txnError.current === "").within(30, "seconds"),
+  ),
+);
+
+const liveness = {
+  loginReachable,
+  accountCreationReachable,
+  someTransactionExists,
+  loginErrorClears,
+  addAccountErrorClears,
+  txnErrorClears,
+};
+
+const DEMO_EMAIL = "[email protected]";
+const DEMO_PASSWORD = "ledger123";
+
+const loginHelper = actions(() => {
+  if (loggedIn.current) return [];
+  const focus = focusedInput.current;
+  const email = loginEmailField.current;
+  const password = loginPasswordField.current;
+  const submit = loginSubmitButton.current;
+
+  if (focus === "login_password") {
+    return submit ? [Tap({ on: submit })] : [];
+  }
+  if (focus === "login_email") {
+    return password ? [InputText({ into: password, text: DEMO_PASSWORD })] : [];
+  }
+  return email ? [InputText({ into: email, text: DEMO_EMAIL })] : [];
+});
+
+const adversarialLogin = actions(() => {
+  if (loggedIn.current) return [];
+  if (focusedInput.current !== null) return [];
+  const submit = loginSubmitButton.current;
+  if (!submit) return [];
+  return [Tap({ on: submit })];
+});
+
+const accountNameSampler = from([
+  "Checking",
+  "Savings",
+  "Travel",
+  "Rent",
+  "Emergency Fund",
+  "Investments",
+  "Groceries",
+  "  ",
+  "Checking",
+  "A".repeat(41),
+  "Petty Cash",
+]);
+
+const typeAccountName = actions(() => {
+  if (route.current !== "add-account") return [];
+  const field = accountNameField.current;
+  if (!field) return [];
+  return [InputText({ into: field, text: accountNameSampler.generate() })];
+});
+
+const submitAddAccount = actions(() => {
+  if (route.current !== "add-account") return [];
+  const submit = addAccountSubmit.current;
+  return submit ? [Tap({ on: submit })] : [];
+});
+
+const openAddAccount = actions(() => {
+  if (route.current !== "home") return [];
+  const button = addAccountButton.current;
+  return button ? [Tap({ on: button })] : [];
+});
+
+const openRandomAccount = actions(() => {
+  if (route.current !== "home") return [];
+  const card = anyAccountCard.current;
+  return card ? [Tap({ on: card })] : [];
+});
+
+const logoutAction = actions(() => {
+  if (route.current !== "home") return [];
+  const button = logoutButton.current;
+  return button ? [Tap({ on: button })] : [];
+});
+
+const goBack = actions(() => {
+  const button = backButton.current;
+  return button ? [Tap({ on: button })] : [];
+});
+
+const amountSampler = from([
+  "12.34",
+  "100",
+  "0.01",
+  "999.99",
+  "5.5",
+  "42",
+  "0",
+  "",
+  "1e4",
+  "0.001",
+  "-5",
+]);
+
+const typeAmount = actions(() => {
+  if (route.current !== "add-transaction") return [];
+  const field = txnAmountField.current;
+  if (!field) return [];
+  return [InputText({ into: field, text: amountSampler.generate() })];
+});
+
+const noteSampler = from([
+  "Coffee",
+  "Paycheck",
+  "Gas",
+  "Refund",
+  "",
+  "Groceries for the week",
+]);
+
+const typeNote = actions(() => {
+  if (route.current !== "add-transaction") return [];
+  const field = txnNoteField.current;
+  if (!field) return [];
+  return [InputText({ into: field, text: noteSampler.generate() })];
+});
+
+const toggleTxnType = actions(() => {
+  if (route.current !== "add-transaction") return [];
+  const current = txnFormType.current;
+  const target = current === "credit" ? txnDebit.current : txnCredit.current;
+  return target ? [Tap({ on: target })] : [];
+});
+
+const submitTxn = actions(() => {
+  if (route.current !== "add-transaction") return [];
+  const submit = txnSubmit.current;
+  return submit ? [Tap({ on: submit })] : [];
+});
+
+const openAddTxn = actions(() => {
+  if (route.current !== "ledger") return [];
+  const button = addTxnButton.current;
+  return button ? [Tap({ on: button })] : [];
+});
+
 export const properties = {
   accountCountNonNegative,
-  addAccountAdvances,
-  eventuallyLoggedIn,
+  ...accountingInvariants,
+  ...stateMachine,
+  ...liveness,
   noUncaughtExceptions,
+  noLogcatErrors,
 };
 
-// ── Actions ────────────────────────────────────────────────────
-// Sampling: random phone numbers for the login screen.
-const phoneSampler = from(["+919876543210", "+15555550100", "+442071234567"]);
-
-const typePhone = actions(() => {
-  const field = phoneField.current;
-  if (!field) return [];
-  return [InputText({ into: field, text: phoneSampler.generate() })];
-});
-
-const tapContinue = actions(() =>
-  continueButton.current ? [Tap({ on: continueButton.current })] : [],
-);
-const tapAddAccount = actions(() =>
-  addAccountButton.current ? [Tap({ on: addAccountButton.current })] : [],
-);
-
-const nameSampler = from(["Alice", "Bob", "Charlie", "Dana"]);
-const fillName = actions(() => {
-  const field = nameField.current;
-  if (!field) return [];
-  return [InputText({ into: field, text: nameSampler.generate() })];
-});
-const tapCreate = actions(() =>
-  createButton.current ? [Tap({ on: createButton.current })] : [],
-);
-
 export const actionsRoot = weighted(
-  [30, typePhone],
-  [30, tapContinue],
-  [20, tapAddAccount],
-  [20, fillName],
-  [20, tapCreate],
-  [10, taps],
-  [5, swipes],
-  [5, waitOnce],
-  [5, pressKey],
+  [30, loginHelper],
+  [2, adversarialLogin],
+  [18, typeAccountName],
+  [14, submitAddAccount],
+  [18, typeAmount],
+  [8, typeNote],
+  [6, toggleTxnType],
+  [16, submitTxn],
+  [14, openAddAccount],
+  [14, openRandomAccount],
+  [12, openAddTxn],
+  [6, goBack],
+  [1, logoutAction],
+  [4, taps],
+  [2, swipes],
+  [2, waitOnce],
+  [2, pressKey],
 );
 
 (globalThis as { actions?: unknown; properties?: unknown }).actions = actionsRoot;