2 files changed, 157 insertions, 8 deletions

diff --git a/pbt/ts/src/bank.test.ts b/pbt/ts/src/bank.test.ts
index 2944e4c..d750d05 100644
--- a/pbt/ts/src/bank.test.ts
+++ b/pbt/ts/src/bank.test.ts
@@ -1,5 +1,10 @@
 import {toNullable} from 'fp-ts/lib/Option';
-import {Account, Operation, SimpleBank} from './bank';
+import {
+  Account,
+  Operation,
+  SimpleBank,
+  bankImplementationMatchesModel,
+} from './bank';
 import {
   Gen,
   Property,
@@ -111,6 +116,32 @@ const correctBalance =
   };
 
 describe('Bank Simulator', () => {
+  test('level-db bank conforms to model', async () => {
+    const prop = forall(genAccounts, async accounts => {
+      return property(genOperations(accounts), async ops => {
+        const levelBank = await withTempFile(
+          filename => new LevelBank(filename),
+        ).then(bank => bank.populateWith(accounts));
+
+        return bankImplementationMatchesModel(accounts)(levelBank)(ops);
+      });
+    });
+
+    const result = await Property.run(prop);
+
+    console.log(result);
+    console.log(JSON.stringify(result.counterexample));
+
+    expect(result.result).toBe('OK');
+  });
+
+  //
+  //
+  //
+  //
+  //
+  //
+
   test('can retrieve balance given account exists', async () => {
     const prop = forall(genAccounts, async accounts => {
       const api = new SimpleBank(accounts);
diff --git a/pbt/ts/src/bank.ts b/pbt/ts/src/bank.ts
index f5981a4..bf14e43 100644
--- a/pbt/ts/src/bank.ts
+++ b/pbt/ts/src/bank.ts
@@ -1,9 +1,17 @@
-import {Option, fromNullable, matchW} from 'fp-ts/lib/Option';
+import {Option, fromNullable, matchW, toNullable} from 'fp-ts/lib/Option';
 
 // keep it simple
 export type Account = string;
 
+/// A basic "Adapter" to a banking system
+///
+/// NOTE: we make the functions Promise-aware in order to support
+/// async/await easily.
 export interface Bank {
+  /// Retrieve the balance of given account.
+  ///
+  /// @param account The account to retrieve balance of
+  /// @return: nothing if account is unknown, its balance otherwise
   balance: (account: Account) => Promise<Option<number>>;
 
   /// Deposit amount into account
@@ -16,9 +24,125 @@ export interface Bank {
   /// @param account The account to deposit into
   /// @param amt The amount to deposit
   deposit: (account: Account, amt: number) => Promise<void>;
+
+  /// Withdraw amount from given `account`.
+  ///
+  /// This function decreases the balance of the given account by the
+  /// specified amount.
+  ///
+  /// @param account The account to deposit into
+  /// @param amt The amount to withdraw
   withdraw: (account: Account, amt: number) => Promise<void>;
 }
 
+/// All possible operations
+export type Operation = GetBalance | Withdraw | Deposit;
+
+export type GetBalance = {op: 'GetBalance'; account: Account};
+
+export type Withdraw = {op: 'Withdraw'; account: Account; amount: number};
+
+export type Deposit = {op: 'Deposit'; account: Account; amount: number};
+
+//
+//
+//
+//
+//
+//
+
+/// A model interpreting bank operations on a simple in-memory map.
+/// Interpreting a sequence of operations on the model will return an
+/// updated state (map of accounts) and a sequence of observed outputs.
+export function model(
+  accounts: Map<Account, number>,
+): (ops: Operation[]) => [Map<Account, number>, (number | null)[]] {
+  return (ops: Operation[]) => {
+    const current = new Map(accounts);
+    const outputs: (number | null)[] = [];
+    for (const op of ops) {
+      switch (op.op) {
+        case 'GetBalance': {
+          outputs.push(current.get(op.account) || null);
+          break;
+        }
+        case 'Deposit': {
+          const bal = current.get(op.account);
+          if (bal) {
+            current.set(op.account, bal + op.amount);
+          }
+          break;
+        }
+        case 'Withdraw': {
+          const bal = current.get(op.account);
+          if (bal) {
+            current.set(op.account, bal - op.amount);
+          }
+          break;
+        }
+      }
+    }
+    return [current, outputs];
+  };
+}
+
+/// A predicate asserting that some `Bank` implementation matches
+/// our model.
+export const bankImplementationMatchesModel =
+  (
+    initialAccounts: Map<Account, number>, // Some initial dataset to work with
+  ) =>
+  (
+    bank: Bank, // The actual bank implementation we want to test
+  ) =>
+  async (
+    ops: Operation[], // an (arbitrary) sequence of operations
+  ): Promise<boolean> => {
+    // run operations on bank implementation
+    const observedOutputs: (number | null)[] = [];
+
+    for (const op of ops) {
+      switch (op.op) {
+        case 'Deposit':
+          await bank.deposit(op.account, op.amount);
+          break;
+        case 'Withdraw':
+          await bank.withdraw(op.account, op.amount);
+          break;
+        case 'GetBalance':
+          observedOutputs.push(await bank.balance(op.account).then(toNullable));
+          break;
+      }
+    }
+
+    // evaluate operations on model
+    const [endBalances, outputs] = model(initialAccounts)(ops);
+
+    // compare outputs
+    for (const [expected, actual] of outputs.map((v, i) => [
+      v,
+      observedOutputs[i],
+    ])) {
+      if (expected !== actual) {
+        console.log(`Output mismatch: expected ${expected}, got ${actual}`);
+        return false;
+      }
+    }
+
+    // compare end balances
+    for (const [account, expected] of endBalances.entries()) {
+      const actual = await bank.balance(account).then(toNullable);
+      if (actual !== expected) {
+        console.log(
+          `Final balance mismatch for account ${account}: expected ${expected}, got ${actual}`,
+        );
+        return false;
+      }
+    }
+
+    return true;
+  };
+
 export class SimpleBank implements Bank {
   private accounts: Map<Account, number>;
 
@@ -57,9 +181,3 @@ export class SimpleBank implements Bank {
     return Promise.resolve();
   }
 }
-
-export type Operation = GetBalance | Withdraw | Deposit;
-
-export type GetBalance = {op: 'GetBalance'; account: Account};
-export type Withdraw = {op: 'Withdraw'; account: Account; amount: number};
-export type Deposit = {op: 'Deposit'; account: Account; amount: number};