test(folio): replace tautological properties with 4 domain invariants (#28)

* test(folio): replace tautological properties with 4 domain invariants

Drop properties that can't fail (e.g. List.size >= 0, balances are Long
integers) or that just check the extractor itself (account_count equals
accounts.length). Keep auth routing liveness, error-clear liveness, and
reachability goals.

Add four properties that target the real code paths:
- balanceMatchesTransactionDelta: a new ledger row shifts the balance
  by exactly its signed amount (credit +, debit -).
- totalEqualsSumOfAccounts: home total equals sum of per-account
  balances at every state, not only on home.
- balanceChangeRequiresActiveAccount: an account's balance can only
  change while that account is the active one in the navigator.
- duplicateAccountNamesRejected: account names are unique under the
  app's actual dedup rule (case-insensitive after trim).

* chore(folio): upgrade sdk-android to io.github.priyanshujain.sanderling:0.0.1-rc4

Group id moved from io.github.priyanshujain to
io.github.priyanshujain.sanderling in the rc4 publish.

* chore(folio): pin @sanderling/spec to 0.0.1-rc4

examples/folio/gradle.properties

@@ -7,4 +7,4 @@ android.nonTransitiveRClass=true
 
 # Pin the sanderling SDK version consumed by this app. Override with
 # `-Psanderling.version=<version>`.
-sanderling.version=0.0.0-dev
+sanderling.version=0.0.1-rc4

examples/folio/sanderling/package-lock.json

@@ -6,13 +6,13 @@
     "": {
       "name": "folio",
       "devDependencies": {
-        "@sanderling/spec": "next"
+        "@sanderling/spec": "^0.0.1-rc4"
       }
     },
     "node_modules/@sanderling/spec": {
-      "version": "0.0.1-rc3",
-      "resolved": "https://registry.npmjs.org/@sanderling/spec/-/spec-0.0.1-rc3.tgz",
-      "integrity": "sha512-mCayssOqM2wfzrQDnFGE8FAlUlDzBl1fx2L/MLDIuPrQHBMlUC350xBB8Z7I/DYI98eCWJMqjtw3iU6yVWKtIQ==",
+      "version": "0.0.1-rc4",
+      "resolved": "https://registry.npmjs.org/@sanderling/spec/-/spec-0.0.1-rc4.tgz",
+      "integrity": "sha512-iv08d2duxQMowqEnDtOeWRGLmiv7188D68g/5ei+cU1BL33cVXwGscLYznfsUv4PgK7XI5Vihwbnp7ME4+Lh1w==",
       "dev": true,
       "license": "Apache-2.0"
     }

examples/folio/sanderling/package.json

@@ -3,6 +3,6 @@
   "private": true,
   "description": "Minimal sanderling integration example.",
   "devDependencies": {
-    "@sanderling/spec": "next"
+    "@sanderling/spec": "^0.0.1-rc4"
   }
 }

examples/folio/sanderling/spec.ts

@@ -34,9 +34,6 @@ interface LedgerRow {
 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) ?? "",
 );
@@ -46,9 +43,6 @@ const accounts = extract<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,
 );
@@ -64,9 +58,6 @@ const focusedInput = extract<string | 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) ?? "",
 );
@@ -94,81 +85,45 @@ const allAccountCards = extract((state) =>
   state.ax.findAll("descPrefix:account_card:"),
 );
 
-const accountCountNonNegative = always(() => accountCount.current >= 0);
+const balanceMatchesTransactionDelta = always(
+  now(() => activeAccountId.current !== null).implies(
+    next(() => {
+      const prevActive = activeAccountId.previous;
+      if (prevActive === null || prevActive === undefined) return true;
+      if (prevActive !== activeAccountId.current) return true;
+      const prevRows = ledgerRows.previous ?? [];
+      const curRows = ledgerRows.current;
+      if (curRows.length !== prevRows.length + 1) return true;
+      const prevIds = new Set(prevRows.map((r) => r.id));
+      const added = curRows.filter((r) => !prevIds.has(r.id));
+      if (added.length !== 1) return true;
+      const delta = ledgerBalance.current - (ledgerBalance.previous ?? 0);
+      return delta === added[0].signed;
+    }),
+  ),
+);
 
-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 totalEqualsSumOfAccounts = always(() => {
   const sum = accounts.current.reduce((acc, a) => acc + a.balance, 0);
   return sum === totalBalance.current;
+});
+
+const balanceChangeRequiresActiveAccount = always(
+  now(() => true).implies(
+    next(() => {
+      const prevAccounts = accounts.previous ?? [];
+      const prevActive = activeAccountId.previous ?? null;
+      for (const cur of accounts.current) {
+        const prev = prevAccounts.find((a) => a.id === cur.id);
+        if (!prev) continue;
+        if (cur.balance !== prev.balance && prevActive !== cur.id) return false;
+      }
+      return true;
     }),
   ),
 );
 
-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 duplicateAccountNamesRejected = always(() => {
   const seen = new Set<string>();
   for (const a of accounts.current) {
     const key = a.name.trim().toLowerCase();
@@ -178,48 +133,13 @@ const uniqueAccountNames = always(() => {
   return true;
 });
 
-const accountingInvariants = {
-  totalBalanceMatchesAccounts,
-  ledgerBalanceMatchesRows,
-  ledgerRowsWellFormed,
-  balancesAreIntegerCents,
-  accountCountMatchesList,
-  ledgerCountMatchesRows,
-  zeroTxnsMeansZeroBalance,
-  noOrphanTransactions,
-  uniqueAccountNames,
+const domainInvariants = {
+  balanceMatchesTransactionDelta,
+  totalEqualsSumOfAccounts,
+  balanceChangeRequiresActiveAccount,
+  duplicateAccountNamesRejected,
 };
 
-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"),
@@ -232,11 +152,7 @@ const loggedOutReachesLogin = always(
   ),
 );
 
-const stateMachine = {
-  accountsOnlyGrow,
-  ledgerOnlyGrowsPerAccount,
-  authStatusIsKnown,
-  routeIsKnown,
+const authRouting = {
   loggedInLeavesLogin,
   loggedOutReachesLogin,
 };
@@ -410,9 +326,8 @@ const openAddTxn = actions(() => {
 });
 
 export const properties = {
-  accountCountNonNegative,
-  ...accountingInvariants,
-  ...stateMachine,
+  ...domainInvariants,
+  ...authRouting,
   ...liveness,
   noUncaughtExceptions,
 };