From a99b500d83700d973d42b1372d46f21de430f8a9 Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Wed, 4 Jun 2025 16:02:05 +0300
Subject: [PATCH 01/11] fix foundry commit

---
 flake.lock | 8 ++++----
 flake.nix  | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/flake.lock b/flake.lock
index 08793ac4e9..a5f9725a26 100644
--- a/flake.lock
+++ b/flake.lock
@@ -28,16 +28,16 @@
         ]
       },
       "locked": {
-        "lastModified": 1746090613,
-        "narHash": "sha256-Si8nvKH31lzwbJ8aSncgQDYxf3IHreNVJVzSvovnLSM=",
+        "lastModified": 1748682694,
+        "narHash": "sha256-vun3iVnpk5cU6HZsOjpHRpeo9/ztAQWgFOMLR5IyOHE=",
         "owner": "shazow",
         "repo": "foundry.nix",
-        "rev": "2b56cb8bae12b0a0608e5ba6dd4af4a9cf9609b4",
+        "rev": "cefa65c2e3c77e9ee035e2a23188799710bb7cdb",
         "type": "github"
       },
       "original": {
         "owner": "shazow",
-        "ref": "stable",
+        "ref": "cefa65c",
         "repo": "foundry.nix",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index fc72f6dc7c..bc5db0a3f4 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,7 +5,7 @@
     flake-utils.url = "github:numtide/flake-utils";
     nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
     foundry = {
-      url = "github:shazow/foundry.nix/monthly";
+      url = "github:shazow/foundry.nix/cefa65c";
       inputs.flake-utils.follows = "flake-utils";
       inputs.nixpkgs.follows = "nixpkgs";
     };

From 3bdacca3da45d555b99ce467444194e1936d218d Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Wed, 4 Jun 2025 16:04:16 +0300
Subject: [PATCH 02/11] delete
 .github/workflows/handler.publish-pr-packages.yml

---
 .../workflows/handler.publish-pr-packages.yml | 108 ------------------
 1 file changed, 108 deletions(-)
 delete mode 100644 .github/workflows/handler.publish-pr-packages.yml

diff --git a/.github/workflows/handler.publish-pr-packages.yml b/.github/workflows/handler.publish-pr-packages.yml
deleted file mode 100644
index c90c2c0eb3..0000000000
--- a/.github/workflows/handler.publish-pr-packages.yml
+++ /dev/null
@@ -1,108 +0,0 @@
-name: Publish PR Packages
-
-on:
-  workflow_run:
-    workflows: ["CD | Create PR Artifact"]
-    types:
-      - completed
-
-jobs:
-  publish_pr_packages:
-    name: NPM publish PR to Github
-
-    permissions: write-all
-
-    runs-on: ubuntu-22.04
-
-    if: ${{ github.event.workflow_run.conclusion == 'success' }}
-
-    steps:
-      - uses: actions/checkout@v4
-
-      - name: Use Node.js 24.x
-        uses: actions/setup-node@v4
-        with:
-          node-version: 24.x
-
-      - name: Show context
-        env:
-          HEAD_REF: ${{ github.head_ref }}
-          GITHUB_REF: ${{ github.ref }}
-        run: |
-          echo github.event_name: ${{ github.event_name }}
-          echo github.sha: ${{ github.sha }}
-          echo github.repository: ${{ github.repository }}
-          echo github.ref: "$GITHUB_REF"
-          echo github.head_ref: "$HEAD_REF"
-          echo github.base_ref: ${{ github.base_ref }}
-
-      - name: Download artifact
-        continue-on-error: true
-        id: download_artifact
-        uses: dawidd6/action-download-artifact@v6
-        with:
-          workflow: ${{ github.event.workflow_run.workflow_id }}
-          workflow_conclusion: success
-          if_no_artifact_found: fail
-
-      - name: Get PR data
-        if: steps.download_artifact.outcome == 'success'
-        id: pr
-        run: |
-          ls -R pr-packages
-          pr_number=$(ls pr-packages)
-          # find num of files and print a dot for each file and count the dots
-          n_packages=$(find "pr-packages/$pr_number" -maxdepth 1 -type f -printf '.' | wc -c)
-          echo pr_number: "$pr_number"
-          echo n_packages: "$n_packages"
-          echo "pr_number=$pr_number" >> "$GITHUB_OUTPUT"
-          echo "n_packages=$n_packages" >> "$GITHUB_OUTPUT"
-
-      - name: Publish to github
-        if: steps.download_artifact.outcome == 'success'
-        run: |
-          pr_number="${{ steps.pr.outputs.pr_number }}"
-          tasks/npmrc-use-github.sh > pr-packages/$pr_number/.npmrc # using GITHUB_TOKEN
-          cd pr-packages/$pr_number
-          shopt -s nullglob
-          for p in * ; do
-            npm --userconfig .npmrc publish --access public --tag "PR$pr_number" "$p"
-          done
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      - name: Find Comment
-        uses: peter-evans/find-comment@v1
-        if: ${{ steps.pr.outputs.n_packages > 0 && steps.download_artifact.outcome == 'success' }}
-        id: fc
-        with:
-          issue-number: ${{ steps.pr.outputs.pr_number }}
-          comment-author: "github-actions[bot]"
-
-      - name: Create comment
-        if: ${{ steps.pr.outputs.n_packages > 0 && steps.fc.outputs.comment-id == 0 && steps.download_artifact.outcome == 'success'}}
-        uses: peter-evans/create-or-update-comment@v2
-        with:
-          issue-number: ${{ steps.pr.outputs.pr_number }}
-          body: |
-            ### 📦 PR Packages
-
-            Install this PR (you need to setup Github packages):
-
-            ```bash
-            yarn add @superfluid-finance/ethereum-contracts@PR${{ steps.pr.outputs.pr_number }}
-            yarn add @superfluid-finance/sdk-core@PR${{ steps.pr.outputs.pr_number }}
-            yarn add @superfluid-finance/sdk-redux@PR${{ steps.pr.outputs.pr_number }}
-            ```
-
-            <details><summary>:octocat: Click to learn how to use Github packages</summary>
-
-            To use the Github package registry, create a token with "read:packages" permission. See [Creating a personal access token](https://docs.github.com/en/github/authenticating-to-github/creating-a-personal-access-token) for help.
-
-            Next add these lines to your `.npmrc` file, replacing TOKEN with your personal access token. See [Installing a package from Github](https://docs.github.com/en/packages/guides/configuring-npm-for-use-with-github-packages#installing-a-package) if you get stuck.
-
-            ```
-            @superfluid-finance:registry=https://npm.pkg.github.com
-            //npm.pkg.github.com/:_authToken=TOKEN
-            ```
-            </details>

From 555e8549ef145edc4164c5e70c70a76566e8af30 Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Wed, 11 Jun 2025 16:27:55 +0300
Subject: [PATCH 03/11] semantic money: clean up code; separate monetary types
 out

---
 packages/spec-haskell/Makefile                |   6 +-
 ....freeze => all.ghc94.cabal.project.freeze} |   0
 .../pkgs/semantic-money/semantic-money.cabal  |   1 +
 .../src/Money/Theory/MonetaryTypes.hs         |  45 +++
 .../src/Money/Theory/SemanticMoney.hs         | 350 +++++++++---------
 .../test/Money/Theory/SemanticMoney_prop.hs   |  32 +-
 .../test/Money/Theory/TestMonetaryTypes.hs    |  30 +-
 7 files changed, 262 insertions(+), 202 deletions(-)
 rename packages/spec-haskell/{cabal.project.freeze => all.ghc94.cabal.project.freeze} (100%)
 create mode 100644 packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs

diff --git a/packages/spec-haskell/Makefile b/packages/spec-haskell/Makefile
index d017fe5766..70c8776d75 100644
--- a/packages/spec-haskell/Makefile
+++ b/packages/spec-haskell/Makefile
@@ -32,7 +32,7 @@ build:
 build-test:
 	$(CABAL_TEST) v2-build all
 
-build-wasm: 
+build-wasm:
 	$(CABAL_WASM) v2-build -v --with-compiler wasm32-wasi-ghc --with-hc-pkg wasm32-wasi-ghc-pkg semantic-money
 	wasm32-wasi-ghc \
 		-odir $(PWD)/$(WASM_BUILDDIR)/wasm -hidir $(PWD)/$(WASM_BUILDDIR)/wasm -stubdir $(PWD)/$(WASM_BUILDDIR)/wasm \
@@ -58,6 +58,10 @@ test:
 	$(CABAL_TEST) v2-test all --enable-tests \
 		$(TEST_OPTIONS)
 
+test-sm:
+	$(CABAL_TEST) v2-test semantic-money --enable-tests \
+		$(TEST_OPTIONS)
+
 test-coverage:
 	$(CABAL_COVERAGE) v2-build all --enable-tests --enable-coverage
 	$(CABAL_COVERAGE) v2-test all --enable-tests --enable-coverage \
diff --git a/packages/spec-haskell/cabal.project.freeze b/packages/spec-haskell/all.ghc94.cabal.project.freeze
similarity index 100%
rename from packages/spec-haskell/cabal.project.freeze
rename to packages/spec-haskell/all.ghc94.cabal.project.freeze
diff --git a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
index b8e545aa45..dcd7e636ae 100644
--- a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
+++ b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
@@ -22,6 +22,7 @@ library
     import:           optiongs
     hs-source-dirs:   src
     exposed-modules:
+        Money.Theory.MonetaryTypes
         Money.Theory.SemanticMoney
     -- other-modules:
     -- other-extensions:
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
new file mode 100644
index 0000000000..d0d85db2a8
--- /dev/null
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE DefaultSignatures      #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+module Money.Theory.MonetaryTypes where
+-- base
+import           Data.Kind (Type)
+
+
+-- | Type system trite: types used in semantic money
+--
+-- Note:
+--   * Index related types through associated type families.
+--   * Use type family dependencies to make these types to the index type injective.
+class ( Eq (MT_TIME mt), Ord (MT_TIME mt), Num (MT_TIME mt)
+      , Eq (MT_VALUE mt), Ord (MT_VALUE mt), Num (MT_VALUE mt)
+      , Eq (MT_UNIT mt), Ord (MT_UNIT mt), Num (MT_UNIT mt)
+      ) =>
+      MonetaryTypes mt where
+    mt_v_mul_t :: MT_VALUE mt -> MT_TIME mt -> MT_VALUE mt
+    default mt_v_mul_t ::
+        Integral (MT_TIME mt) =>
+        MT_VALUE mt -> MT_TIME mt -> MT_VALUE mt
+    mt_v_mul_t v t = v * (fromInteger . toInteger) t
+
+    mt_v_mul_u :: MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
+    default mt_v_mul_u ::
+        Integral (MT_UNIT mt) =>
+        MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
+    mt_v_mul_u v u = v * (fromInteger . toInteger) u
+
+    mt_v_div_u :: MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
+    default mt_v_div_u ::
+        (Integral (MT_VALUE mt), Integral (MT_UNIT mt)) =>
+        MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
+    mt_v_div_u v u = let u' = (fromInteger . toInteger) u in v `div` u'
+
+    mt_v_mul_u_qr_u :: MT_VALUE mt -> (MT_UNIT mt, MT_UNIT mt) -> (MT_VALUE mt, MT_VALUE mt)
+    default mt_v_mul_u_qr_u ::
+        (Integral (MT_VALUE mt), Integral (MT_UNIT mt)) =>
+        MT_VALUE mt -> (MT_UNIT mt, MT_UNIT mt) -> (MT_VALUE mt, MT_VALUE mt)
+    mt_v_mul_u_qr_u v (u1, u2) = (v * (fromInteger . toInteger) u1) `quotRem` (fromInteger . toInteger) u2
+
+    type family MT_TIME  mt = (t :: Type) | t -> mt
+    type family MT_VALUE mt = (v :: Type) | v -> mt
+    type family MT_UNIT  mt = (u :: Type) | u -> mt
+    -- TODO: Do we need FlowRate type?
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
index 5f39ddcf04..ff75bd6a25 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
@@ -1,229 +1,239 @@
 {-# LANGUAGE DerivingStrategies     #-}
 {-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE TypeFamilyDependencies #-}
-
-module Money.Theory.SemanticMoney where
-
-import           Data.Default (Default (..))
-import           Data.Kind    (Type)
-
-
--- | Type system trite: types used in semantic money
+module Money.Theory.SemanticMoney
+    ( -- * Semantic Money Classes & Primitives
+        MonetaryUnit (settle, settledAt, flowRate, rtb)
+    , IndexedValue (shift1, flow1)
+    , prim2, shift2, flow2, shiftFlow2a, shiftFlow2b
+    , MonetaryParticle (align2)
+      -- * Semantic Money Instances
+    , BasicParticle (..)
+    , UniversalIndex (..)
+    , PDP_Index (..), PDP_Member (..), PDP_MemberMU, pdp_UpdateMember2
+      -- * Re-export Monetary Types
+    , module Money.Theory.MonetaryTypes
+    ) where
 --
--- Note:
---   * Index related types through associated type families.
---   * Use type family dependencies to make these types to the index type injective.
-class ( Integral (MT_TIME  mt)
-      , Integral (MT_VALUE mt)
-      , Integral (MT_UNIT  mt)
-      -- FIXME add FlowRate type
-      ) => MonetaryTypes mt where
-    mt_v_mul_t :: MT_VALUE mt -> MT_TIME mt -> MT_VALUE mt
-    mt_v_mul_t v t = v * (fromInteger . toInteger) t
-    mt_v_mul_u :: MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
-    mt_v_mul_u v u = v * (fromInteger . toInteger) u
-    mt_v_div_u :: MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
-    mt_v_div_u v u = let u' = (fromInteger . toInteger) u in v `div` u'
-    mt_v_mul_u_qr_u :: MT_VALUE mt -> (MT_UNIT mt, MT_UNIT mt) -> (MT_VALUE mt, MT_VALUE mt)
-    mt_v_mul_u_qr_u v (u1, u2) = (v * (fromInteger . toInteger) u1) `quotRem` (fromInteger . toInteger) u2
-
-    type family MT_TIME  mt = (t :: Type) | t -> mt
-    type family MT_VALUE mt = (v :: Type) | v -> mt
-    type family MT_UNIT  mt = (u :: Type) | u -> mt
-
+import           Data.Default               (Default (..))
 --
+import           Money.Theory.MonetaryTypes
+
+
+------------------------------------------------------------------------------------------------------------------------
 -- General Payment Primitives
---
+------------------------------------------------------------------------------------------------------------------------
 
-class ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt
-      ) => MonetaryUnit mt t v mu | mu -> mt where
+-- | A monetary unit and its operators.
+class (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt) =>
+      MonetaryUnit mt t v mu | mu -> mt where
     settle    :: t -> mu -> mu
     settledAt :: mu -> t
     flowRate  :: mu -> v
     rtb       :: mu -> t -> v
 
- -- * On right side biased operations:
- --   1) Right side produces error term with which left side is adjusted accordingly.
- --   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
-
-class ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt
-      , MonetaryUnit mt t v ix, Monoid ix
-      ) => Index mt t v u ix | ix -> mt where
+-- | An indexed monetary value and its 1-primitive operators.
+class (MonetaryUnit mt t v ix, u ~ MT_UNIT mt, Monoid ix) =>
+      IndexedValue mt t v u ix | ix -> mt where
     shift1 :: v -> ix -> (ix, v)
     flow1  :: v -> ix -> (ix, v)
 
-class ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt
-      , MonetaryUnit mt t v mp, Index mt t v u mp
-      ) => MonetaryParticle mt t v u mp where
-    -- align 2-primitive, right side biased
-    align2 :: forall a. Index mt t v u a => u -> u -> (mp, a) -> (mp, a)
-
--- polymorphic 2-primitives
+--
+-- polymorphic 2-primitives for indexed values
 --
 
--- 2-primitive higher order function
-prim2 :: (Index mt t v u a, Index mt t v u b)
-      => ((a, b) -> (a, b)) -> t -> (a, b) -> (a, b)
+-- | 2-primitive higher order function
+prim2 ::
+    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
+    ((a, b) -> (a, b)) -> t -> (a, b) -> (a, b)
 prim2 op t' (a, b) = op (settle t' a, settle t' b)
 
--- shift2, right side biased error term adjustment
-shift2 :: (Index mt t v u a, Index mt t v u b)
-       => v -> t -> (a, b) -> (a, b)
+-- | shift2, right side biased error term adjustment
+shift2 ::
+    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
+    v -> t -> (a, b) -> (a, b)
 shift2 amount = prim2 op
     where op (a, b) = let (b', amount') = shift1 amount b
                           (a', _) = shift1 (-amount') a
                       in  (a', b')
 
--- flow2, right side biased error term adjustment
-flow2 :: (Index mt t v u a, Index mt t v u b)
-      => v -> t -> (a, b) -> (a, b)
+-- | flow2, right side biased error term adjustment
+flow2 ::
+    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
+    v -> t -> (a, b) -> (a, b)
 flow2 r = prim2 op
     where op (a, b) = let (b', r') = flow1 r b
                           (a', _) = flow1 (-r') a
                       in  (a', b')
 
--- shiftFlow2 for the left side (a), right side biased error term adjustment
-shiftFlow2a :: (Index mt t v u a, Index mt t v u b)
-            => v -> t -> (a, b) -> (a, b)
-shiftFlow2a dr t (a, b) = let ( _, b1) = flow2 (flowRate a) t (a, mempty)
-                              (a', b2) = flow2 (-flowRate a + dr) t (a, mempty)
-                          in  (a', b <> b1 <> b2)
+-- | shiftFlow2 for the left side (a), right side biased error term adjustment
+shiftFlow2a ::
+    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
+    v -> t -> (a, b) -> (a, b)
+shiftFlow2a dr t (a, b) =
+    let ( _, b1) = flow2 (flowRate a) t (a, mempty)
+        (a', b2) = flow2 (-flowRate a + dr) t (a, mempty)
+    in  (a', b <> b1 <> b2)
+
+-- | shiftFlow2 for the right side (b), right side biased error term adjustment
+shiftFlow2b ::
+    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
+    v -> t -> (a, b) -> (a, b)
+shiftFlow2b dr t (a, b) =
+    let (a1,  _) = flow2 (-flowRate b) t (mempty, b)
+        (a2, b') = flow2 (flowRate b + dr) t (mempty, b)
+    in  (a <> a1 <> a2, b')
+
+class IndexedValue mt t v u mp =>
+      MonetaryParticle mt t v u mp where
+    -- | Value alignment 2-primitive, right side biased
+    --
+    -- NOTE:
+    -- * On right side biased operations:
+    --   1) Right side produces error term with which left side is adjusted accordingly.
+    --   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
+    align2 :: forall a. IndexedValue mt t v u a => u -> u -> (mp, a) -> (mp, a)
+
+------------------------------------------------------------------------------------------------------------------------
+-- Basic Particle: building block for indexes
+------------------------------------------------------------------------------------------------------------------------
+
+data BasicParticle mt = BasicParticle
+    { bp_settled_at    :: MT_TIME  mt
+    , bp_settled_value :: MT_VALUE mt
+    , bp_flow_rate     :: MT_VALUE mt
+    }
 
--- shiftFlow2 for the right side (b), right side biased error term adjustment
-shiftFlow2b :: (Index mt t v u a, Index mt t v u b)
-            => v -> t -> (a, b) -> (a, b)
-shiftFlow2b dr t (a, b) = let (a1,  _) = flow2 (-flowRate b) t (mempty, b)
-                              (a2, b') = flow2 (flowRate b + dr) t (mempty, b)
-                          in  (a <> a1 <> a2, b')
+deriving stock instance MonetaryTypes mt => Eq (BasicParticle mt)
 
---
+instance MonetaryTypes mt => Semigroup (BasicParticle mt) where
+    a@(BasicParticle t1 _ _) <> b@(BasicParticle t2 _ _) = BasicParticle t' (sv1 + sv2) (r1 + r2)
+        -- The binary operator supports negative time values while abiding the monoidal laws.
+        -- The practical semantics of values of mixed-sign is not of the concern of this specification.
+        where t' | t1 == 0 = t2 | t2 == 0 = t1 | otherwise = max t1 t2
+              (BasicParticle _ sv1 r1) = settle t' a
+              (BasicParticle _ sv2 r2) = settle t' b
+
+instance MonetaryTypes mt => Monoid (BasicParticle mt) where
+    mempty = BasicParticle 0 0 0
+
+instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt) =>
+         MonetaryUnit mt t v (BasicParticle mt) where
+    settle t' a = a { bp_settled_at = t'
+                    , bp_settled_value = rtb a t'
+                    }
+    settledAt = bp_settled_at
+    flowRate = bp_flow_rate
+    rtb (BasicParticle t s r) t' = r `mt_v_mul_t` (t' - t) + s
+
+instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt) =>
+         IndexedValue mt t v u (BasicParticle mt) where
+
+    shift1 x a = (a { bp_settled_value = bp_settled_value a + x }, x)
+    flow1 r' a = (a { bp_flow_rate = r' }, r')
+
+instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt) =>
+         MonetaryParticle mt t v u (BasicParticle mt) where
+    align2 u u' (b, a) = (b', a')
+        where r = flowRate b
+              (r', er') = if u' == 0 then (0, r `mt_v_mul_u` u) else r `mt_v_mul_u_qr_u` (u, u')
+              b' = fst . flow1 r' $ b
+              a' = fst . flow1 (er' + flowRate a) $ a
+
+------------------------------------------------------------------------------------------------------------------------
 -- Univeral Index
---
+------------------------------------------------------------------------------------------------------------------------
 
+-- | A newtype wrapper of an underlying monetary unit @wp@, with a parameterized @mt@.
 newtype UniversalIndex mt wp = UniversalIndex wp
-deriving newtype instance ( MonetaryTypes mt
-                          , Eq wp ) => Eq (UniversalIndex mt wp)
-deriving newtype instance ( MonetaryTypes mt
-                          , Semigroup wp ) => Semigroup (UniversalIndex mt wp)
-deriving newtype instance ( MonetaryTypes mt
-                          , Monoid wp ) => Monoid (UniversalIndex mt wp)
-deriving newtype instance ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt
-                          , MonetaryUnit mt t v wp ) => MonetaryUnit mt t v (UniversalIndex mt wp)
-deriving newtype instance ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt
-                          , Monoid wp
-                          , Index mt t v u wp ) => Index mt t v u (UniversalIndex mt wp)
+
+deriving newtype instance (MonetaryTypes mt, Eq wp) => Eq (UniversalIndex mt wp)
+deriving newtype instance (MonetaryTypes mt, Semigroup wp) => Semigroup (UniversalIndex mt wp)
+deriving newtype instance (MonetaryTypes mt, Monoid wp) => Monoid (UniversalIndex mt wp)
+deriving newtype instance MonetaryUnit mt t v wp => MonetaryUnit mt t v (UniversalIndex mt wp)
+deriving newtype instance IndexedValue mt t v u wp => IndexedValue mt t v u (UniversalIndex mt wp)
+deriving newtype instance MonetaryParticle mt t v u wp => MonetaryParticle mt t v u (UniversalIndex mt wp)
+
+------------------------------------------------------------------------------------------------------------------------
+-- Proportional Distribution Pool (PDP)
+------------------------------------------------------------------------------------------------------------------------
+
+data PDP_Index mt wp = PDP_Index
+    { pdpi_total_units :: MT_UNIT mt
+    , pdpi_wp          :: wp -- wrapped particle
+    }
+
+data PDP_Member mt wp = PDP_Member
+    { pdpm_owned_unit    :: MT_UNIT mt
+    , pdpm_settled_value :: MT_VALUE mt
+    , pdpm_synced_wp     :: wp
+    }
+
+type PDP_MemberMU mt wp = (PDP_Index mt wp, PDP_Member mt wp)
+
+pdp_UpdateMember2 ::
+    ( IndexedValue mt t v u a
+    , MonetaryParticle mt t v u wp
+    , mu ~ PDP_MemberMU mt wp
+    ) =>
+    u -> t -> (a, mu) -> (a, mu)
+pdp_UpdateMember2 u' t' (a, (b, pm)) = (a'', (b'', pm''))
+    where (PDP_Index tu mpi, pm'@(PDP_Member u _ _)) = settle t' (b, pm)
+          tu' = tu + u' - u
+          (mpi', a'') = align2 tu tu' (mpi, settle t' a)
+          b''  = PDP_Index tu' mpi'
+          pm'' = pm' { pdpm_owned_unit = u', pdpm_synced_wp = mpi' }
 
 --
--- Proportional Distribution Pool
+-- PDP_Index as MonetaryIndex
 --
 
-data PDPoolIndex mt wp = PDPoolIndex { pdidx_total_units :: MT_UNIT mt
-                                     , pdidx_wp          :: wp -- wrapped particle
-                                     }
-instance ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt
-         , MonetaryUnit mt t v wp) => MonetaryUnit mt t v (PDPoolIndex mt wp) where
-    settle t' a@(PDPoolIndex _ mpi) = a { pdidx_wp = settle t' mpi }
-    settledAt (PDPoolIndex _ mpi) = settledAt mpi
-    flowRate (PDPoolIndex _ mpi) = flowRate mpi
-    rtb (PDPoolIndex _ mpi) = rtb mpi
-
-instance (MonetaryTypes mt, Semigroup wp) => Semigroup (PDPoolIndex mt wp) where
+instance MonetaryUnit mt t v wp =>
+         MonetaryUnit mt t v (PDP_Index mt wp) where
+    settle t' a@(PDP_Index _ mpi) = a { pdpi_wp = settle t' mpi }
+    settledAt (PDP_Index _ mpi) = settledAt mpi
+    flowRate (PDP_Index _ mpi) = flowRate mpi
+    rtb (PDP_Index _ mpi) = rtb mpi
+
+instance (MonetaryTypes mt, Semigroup wp) => Semigroup (PDP_Index mt wp) where
     -- The binary operator supports negative unit values while abiding the monoidal laws.
     -- The practical semantics of values of mixed-sign is not of the concern of this specification.
-    (PDPoolIndex u1 a) <> (PDPoolIndex u2 b) = PDPoolIndex u' (a <> b)
+    (PDP_Index u1 a) <> (PDP_Index u2 b) = PDP_Index u' (a <> b)
         where u' | u1 == 0 = u2 | u2 == 0 = u1 | otherwise = max u1 u2
 
-instance (MonetaryTypes mt, Monoid wp) => Monoid (PDPoolIndex mt wp) where
-    mempty = PDPoolIndex 0 mempty
+instance (MonetaryTypes mt, Monoid wp) => Monoid (PDP_Index mt wp) where
+    mempty = PDP_Index 0 mempty
 
-instance ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt
-         , MonetaryParticle mt t v u wp) => Index mt t v u (PDPoolIndex mt wp) where
-    shift1 x a@(PDPoolIndex tu mpi) = (a { pdidx_wp = mpi' }, x' `mt_v_mul_u` tu)
+instance MonetaryParticle mt t v u wp =>
+         IndexedValue mt t v u (PDP_Index mt wp) where
+    shift1 x a@(PDP_Index tu mpi) = (a { pdpi_wp = mpi' }, x' `mt_v_mul_u` tu)
         where (mpi', x') = if tu == 0 then (mpi, 0) else shift1 (x `mt_v_div_u` tu) mpi
 
-    flow1 r' a@(PDPoolIndex tu mpi) = (a { pdidx_wp = mpi' }, r'' `mt_v_mul_u` tu)
+    flow1 r' a@(PDP_Index tu mpi) = (a { pdpi_wp = mpi' }, r'' `mt_v_mul_u` tu)
         where (mpi', r'') = if tu == 0 then flow1 0 mpi else flow1 (r' `mt_v_div_u` tu) mpi
 
-data PDPoolMember mt wp = PDPoolMember { pdpm_owned_unit    :: MT_UNIT mt
-                                       , pdpm_settled_value :: MT_VALUE mt
-                                       , pdpm_synced_wp     :: wp
-                                       }
-instance ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt
-         , Monoid wp ) => Default (PDPoolMember mt wp) where def = PDPoolMember 0 0 mempty
-type PDPoolMemberMU mt wp = (PDPoolIndex mt wp, PDPoolMember mt wp)
-
-pdpUpdateMember2 :: ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt
-                    , Index mt t v u a
-                    , MonetaryParticle mt t v u wp
-                    , mu ~ PDPoolMemberMU mt wp
-                    ) => u -> t -> (a, mu) -> (a, mu)
-pdpUpdateMember2 u' t' (a, (b, pm))  = (a'', (b'', pm''))
-    where (PDPoolIndex tu mpi, pm'@(PDPoolMember u _ _)) = settle t' (b, pm)
-          tu' = tu + u' - u
-          (mpi', a'') = align2 tu tu' (mpi, settle t' a)
-          b''  = PDPoolIndex tu' mpi'
-          pm'' = pm' { pdpm_owned_unit = u', pdpm_synced_wp = mpi' }
+--
+-- PDP_MemberMU as MonetaryUnit
+--
+
+instance (MonetaryTypes mt, Monoid wp) =>
+         Default (PDP_Member mt wp) where
+    def = PDP_Member 0 0 mempty
 
-instance ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt
-         , MonetaryUnit mt t v wp) => MonetaryUnit mt t v (PDPoolMemberMU mt wp) where
+instance MonetaryUnit mt t v wp =>
+         MonetaryUnit mt t v (PDP_MemberMU mt wp) where
     settle t' (pix, pm) = (pix', pm')
         where sv' = rtb (pix, pm) t'
-              pix'@(PDPoolIndex _ mpi') = settle t' pix
+              pix'@(PDP_Index _ mpi') = settle t' pix
               pm' = pm { pdpm_settled_value = sv', pdpm_synced_wp = mpi' }
 
-    settledAt (_, PDPoolMember _ _ mps) = settledAt mps
+    settledAt (_, PDP_Member _ _ mps) = settledAt mps
 
-    flowRate (PDPoolIndex _ mpi, PDPoolMember u _ _) = flowRate mpi `mt_v_mul_u` u
+    flowRate (PDP_Index _ mpi, PDP_Member u _ _) = flowRate mpi `mt_v_mul_u` u
 
-    rtb (PDPoolIndex _ mpi, PDPoolMember u sv mps) t' = sv +
+    rtb (PDP_Index _ mpi, PDP_Member u sv mps) t' = sv +
         -- let ti = bp_settled_at mpi
         --     ts = bp_settled_at mps
         -- in (rtb mpi t' - rtb mps ti) -- include index's current accruals for the member
         -- +  (rtb mps ti - rtb mps ts) -- cancel out-of-sync member's rtb between [ts:ti]
         -- =>
         (rtb mpi t' - rtb mps (settledAt mps)) `mt_v_mul_u` u
-
---
--- Particles: building block for indexes
---
-
-data BasicParticle mt = BasicParticle { bp_settled_at    :: MT_TIME  mt
-                                      , bp_settled_value :: MT_VALUE mt
-                                      , bp_flow_rate     :: MT_VALUE mt
-                                      }
-
-deriving stock instance MonetaryTypes mt => Eq (BasicParticle mt)
-
-instance MonetaryTypes mt => Semigroup (BasicParticle mt) where
-    a@(BasicParticle t1 _ _) <> b@(BasicParticle t2 _ _) = BasicParticle t' (sv1 + sv2) (r1 + r2)
-        -- The binary operator supports negative time values while abiding the monoidal laws.
-        -- The practical semantics of values of mixed-sign is not of the concern of this specification.
-        where t' | t1 == 0 = t2 | t2 == 0 = t1 | otherwise = max t1 t2
-              (BasicParticle _ sv1 r1) = settle t' a
-              (BasicParticle _ sv2 r2) = settle t' b
-
-instance MonetaryTypes mt => Monoid (BasicParticle mt) where
-    mempty = BasicParticle 0 0 0
-
-instance ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt
-         ) => MonetaryUnit mt t v (BasicParticle mt) where
-    settle t' a = a { bp_settled_at = t'
-                    , bp_settled_value = rtb a t'
-                    }
-    settledAt = bp_settled_at
-    flowRate = bp_flow_rate
-    rtb (BasicParticle t s r) t' = r `mt_v_mul_t` (t' - t) + s
-
-instance ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt
-         ) => Index mt t v u (BasicParticle mt) where
-
-    shift1 x a = (a { bp_settled_value = bp_settled_value a + x }, x)
-    flow1 r' a = (a { bp_flow_rate = r' }, r')
-
-instance ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt
-         ) => MonetaryParticle mt t v u (BasicParticle mt) where
-    align2 u u' (b, a) = (b', a')
-        where r = flowRate b
-              (r', er') = if u' == 0 then (0, r `mt_v_mul_u` u) else r `mt_v_mul_u_qr_u` (u, u')
-              b' = fst . flow1 r' $ b
-              a' = fst . flow1 (er' + flowRate a) $ a
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
index 3c75d928eb..fd1ad18329 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
@@ -33,13 +33,13 @@ bp_settle_idempotency (a :: TesBasicParticle) = mu_settle_idempotency a
 bp_constant_rtb (a :: TesBasicParticle) = mu_constant_rtb a
 uidx_settle_idempotency (a :: TestUniversalIndex) = mu_settle_idempotency a
 uidx_constant_rtb (a :: TestUniversalIndex) = mu_constant_rtb a
-pdidx_settle_idempotency (a :: TestPDPoolIndex) = mu_settle_idempotency a
-pdidx_constant_rtb (a :: TestPDPoolIndex) = mu_constant_rtb a
-pdmb_settle_idempotency (a :: TestPDPoolMemberMU) = mu_settle_idempotency a
-pdmb_constant_rtb (a :: TestPDPoolIndex) t1 u1 t2 u2 = mu_constant_rtb b''
+pdidx_settle_idempotency (a :: TestPDP_Index) = mu_settle_idempotency a
+pdidx_constant_rtb (a :: TestPDP_Index) = mu_constant_rtb a
+pdmb_settle_idempotency (a :: TestPDP_MemberMU) = mu_settle_idempotency a
+pdmb_constant_rtb (a :: TestPDP_Index) t1 u1 t2 u2 = mu_constant_rtb b''
     -- adding two members to an existing index
-    where (a', b') = pdpUpdateMember2 u1 t1 (a, (a, def))
-          (_, b'') = pdpUpdateMember2 u2 t2 (a', b')
+    where (a', b') = pdp_UpdateMember2 u1 t1 (a, (a, def))
+          (_, b'') = pdp_UpdateMember2 u2 t2 (a', b')
 
 mu_laws = describe "monetary unit laws" $ do
     it "bp settle idempotency" $ property bp_settle_idempotency
@@ -59,8 +59,8 @@ bp_monoid_identity (a :: TesBasicParticle) = a == a <> mempty && a == mempty <>
 bp_monoid_assoc (a :: TesBasicParticle) b c = (a <> b) <> c == a <> (b <> c)
 uidx_monoid_identity (a :: TestUniversalIndex) = a == a <> mempty && a == mempty <> a
 uidx_monoid_assoc (a :: TestUniversalIndex) b c = (a <> b) <> c == a <> (b <> c)
-pdidx_monoid_identity (a :: TestPDPoolIndex) = a == a <> mempty && a == mempty <> a
-pdidx_monoid_assoc (a :: TestPDPoolIndex) b c = (a <> b) <> c == a <> (b <> c)
+pdidx_monoid_identity (a :: TestPDP_Index) = a == a <> mempty && a == mempty <> a
+pdidx_monoid_assoc (a :: TestPDP_Index) b c = (a <> b) <> c == a <> (b <> c)
 
 mp_monoid_laws = describe "monetary particles monoidal laws" $ do
     it "bp monoid identity law" $ property bp_monoid_identity
@@ -95,18 +95,18 @@ one2one_tests = describe "1to1 2-primitives" $ do
 --------------------------------------------------------------------------------
 
 updp_u1_f1_u1_f2 f1 f2 t1 u1 t2 {- f1 -} t3 {- f2 -} t4 u2 t5 =
-    pdidx_total_units b'' == u2 &&
+    pdpi_total_units b'' == u2 &&
     0 == rtb a'' t5 + rtb (b'', b1') t5
-    where (a, (b, b1)) = pdpUpdateMember2 u1 t1 (mempty :: TestUniversalIndex, (mempty :: TestPDPoolIndex, def))
+    where (a, (b, b1)) = pdp_UpdateMember2 u1 t1 (mempty :: TestUniversalIndex, (mempty :: TestPDP_Index, def))
           (a', b') = f2 t3 (f1 t2 (a, b))
-          (a'', (b'', b1')) = pdpUpdateMember2 u2 t4 (a', (b', b1))
+          (a'', (b'', b1')) = pdp_UpdateMember2 u2 t4 (a', (b', b1))
 
 updp_u1_f1_u2_f2 f1 f2 t1 u1 t2 {- f1 -} t3 u2 t4 {- f2 -} t5 =
-    pdidx_total_units b''' == u1 + u2 &&
+    pdpi_total_units b''' == u1 + u2 &&
     0 == rtb a''' t5 + rtb (b''', b1) t5 + rtb (b''', b2) t5
-    where (a, (b, b1)) = pdpUpdateMember2 u1 t1 (mempty :: TestUniversalIndex, (mempty :: TestPDPoolIndex, def))
+    where (a, (b, b1)) = pdp_UpdateMember2 u1 t1 (mempty :: TestUniversalIndex, (mempty :: TestPDP_Index, def))
           (a', b') = f1 t2 (a, b)
-          (a'', (b'', b2)) = pdpUpdateMember2 u2 t3 (a', (b', def :: TestPDPoolMember))
+          (a'', (b'', b2)) = pdp_UpdateMember2 u2 t3 (a', (b', def :: TestPDP_Member))
           (a''', b''') = f2 t4 (a'', b'')
 
 updp_u1_shift2_u1_shift2 x1 x2 = updp_u1_f1_u1_f2 (shift2 x1) (shift2 x2)
@@ -141,7 +141,7 @@ updp_flow2 (a :: TestUniversalIndex) t1 r1 t2 r2 t3 =
     flowRate b'' == r2 && flowRate a'' == -r2 &&
     flowRate (b'', b1') == r2 &&
     r1 `mt_v_mul_t` (t2 - t1) + r2 `mt_v_mul_t` (t3 - t2) == rtb (b'', b1') t3 - rtb (b', b1') t1
-    where (a', (b', b1')) = pdpUpdateMember2 1 t1 (a, (mempty :: TestPDPoolIndex, def))
+    where (a', (b', b1')) = pdp_UpdateMember2 1 t1 (a, (mempty :: TestPDP_Index, def))
           (a'', b'') = flow2 r2 t2 (flow2 r1 t1 (a', b'))
 
 uu_shiftFlow2a (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
@@ -166,7 +166,7 @@ updp_shiftFlow2b (a :: TestUniversalIndex) t1 r1 t2 r2 t3 =
     rtb (b'', b1') t3 - rtb (b', b1') t3 == rtb a' t3 - rtb a'' t3 &&
     -- ditto
     r1 `mt_v_mul_t` (t2 - t1) + (r1 + r2) `mt_v_mul_t` (t3 - t2) == rtb (b'', b1') t3 - rtb (b', b1') t3
-    where (a', (b', b1')) = pdpUpdateMember2 1 t1 (a, (mempty :: TestPDPoolIndex, def))
+    where (a', (b', b1')) = pdp_UpdateMember2 1 t1 (a, (mempty :: TestPDP_Index, def))
           (a'', b'') = shiftFlow2b r2 t2 (shiftFlow2b r1 t1 (a', b'))
 
 flow2_tests = describe "flow2 tests" $ do
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
index e68fbd5242..226601f398 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
@@ -1,9 +1,9 @@
 {-# LANGUAGE TypeFamilies #-}
 
 module Money.Theory.TestMonetaryTypes where
-
+-- quickcheck
 import           Test.QuickCheck
-
+--
 import           Money.Theory.SemanticMoney
 
 
@@ -42,21 +42,21 @@ deriving instance Show TestUniversalIndex
 instance Arbitrary TestUniversalIndex where
     arbitrary = UniversalIndex <$> arbitrary
 
--- PDPoolIndex
+-- PDP_Index
 --
-type TestPDPoolIndex = PDPoolIndex TestMonetaryTypes TesBasicParticle
-deriving instance Show TestPDPoolIndex
-deriving instance Eq TestPDPoolIndex
-instance Arbitrary TestPDPoolIndex where
-    arbitrary = PDPoolIndex <$> arbitrary <*> arbitrary
+type TestPDP_Index = PDP_Index TestMonetaryTypes TesBasicParticle
+deriving instance Show TestPDP_Index
+deriving instance Eq TestPDP_Index
+instance Arbitrary TestPDP_Index where
+    arbitrary = PDP_Index <$> arbitrary <*> arbitrary
 
--- PDPoolMember
+-- PDP_Member
 --
 
-type TestPDPoolMember = PDPoolMember TestMonetaryTypes TesBasicParticle
-deriving instance Show TestPDPoolMember
-deriving instance Eq TestPDPoolMember
-instance Arbitrary TestPDPoolMember where
-    arbitrary = PDPoolMember <$> arbitrary <*> arbitrary <*> arbitrary
+type TestPDP_Member = PDP_Member TestMonetaryTypes TesBasicParticle
+deriving instance Show TestPDP_Member
+deriving instance Eq TestPDP_Member
+instance Arbitrary TestPDP_Member where
+    arbitrary = PDP_Member <$> arbitrary <*> arbitrary <*> arbitrary
 
-type TestPDPoolMemberMU = PDPoolMemberMU TestMonetaryTypes TesBasicParticle
+type TestPDP_MemberMU = PDP_MemberMU TestMonetaryTypes TesBasicParticle

From 447d3e98fd19d7dfa53a0f15ea7dec16131d0eb0 Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Thu, 12 Jun 2025 13:08:19 +0300
Subject: [PATCH 04/11] primitives refactored before modeling zkoracle

---
 packages/spec-haskell/Makefile                |   2 +
 packages/spec-haskell/default.nix             |   2 +-
 .../pkgs/semantic-money/semantic-money.cabal  |   1 +
 .../src/Money/Theory/MonetaryTypes.hs         |  14 +-
 .../src/Money/Theory/SemanticMoney.hs         | 154 +++++++-----------
 .../src/Money/Theory/TokenModel.hs            |  14 ++
 .../test/Money/Theory/SemanticMoney_prop.hs   |  81 +++++----
 .../test/Money/Theory/TestMonetaryTypes.hs    |  14 +-
 8 files changed, 132 insertions(+), 150 deletions(-)
 create mode 100644 packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs

diff --git a/packages/spec-haskell/Makefile b/packages/spec-haskell/Makefile
index 70c8776d75..bae41d7aff 100644
--- a/packages/spec-haskell/Makefile
+++ b/packages/spec-haskell/Makefile
@@ -16,6 +16,7 @@ CABAL_DOCS     = $(CABAL) --builddir=$(DOCS_BUILDDIR)
 CABAL_WASM     = $(CABAL) --builddir=$(WASM_BUILDDIR)
 
 TEST_OPTIONS = \
+	-O0 \
 	--test-show-details=$(TEST_SHOW_DETAILS_MODE) \
 	--test-options="--maximum-generated-tests=$(TEST_PROP_NUM_RUNS)"
 
@@ -148,6 +149,7 @@ dev:
 	nodemon \
 		-e lhs,hs,cabal \
 		-i dist-newstyle/ -i "$(TEST_BUILDDIR)/" -i "$(TEST_COVERAGE_BUILDDIR)/" \
+		-i "#*" -i "flycheck_*.hs" \
 		-x "make $(DEV_TARGETS) || exit 1"
 
 freeze:
diff --git a/packages/spec-haskell/default.nix b/packages/spec-haskell/default.nix
index 1e78d2a40f..8096c659e8 100644
--- a/packages/spec-haskell/default.nix
+++ b/packages/spec-haskell/default.nix
@@ -9,7 +9,7 @@
       ../../flake.nix
       ../../flake.lock
       ./cabal.project
-      ./cabal.project.freeze
+      ./all.ghc94.cabal.project.freeze
       ./Makefile
       ./pkgs
     ];
diff --git a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
index dcd7e636ae..989fee5c84 100644
--- a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
+++ b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
@@ -24,6 +24,7 @@ library
     exposed-modules:
         Money.Theory.MonetaryTypes
         Money.Theory.SemanticMoney
+        Money.Theory.TokenModel
     -- other-modules:
     -- other-extensions:
     build-depends:
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
index d0d85db2a8..6a1e4ef1c8 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
@@ -1,6 +1,13 @@
 {-# LANGUAGE DefaultSignatures      #-}
+{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
-module Money.Theory.MonetaryTypes where
+module Money.Theory.MonetaryTypes
+    ( MonetaryTypes
+      ( MT_TIME, MT_VALUE, MT_UNIT
+      , mt_v_mul_t, mt_v_mul_u, mt_v_div_u, mt_v_mul_u_qr_u
+      )
+    , MonetaryTypes'tv, MonetaryTypes'tvu
+    ) where
 -- base
 import           Data.Kind (Type)
 
@@ -42,4 +49,7 @@ class ( Eq (MT_TIME mt), Ord (MT_TIME mt), Num (MT_TIME mt)
     type family MT_TIME  mt = (t :: Type) | t -> mt
     type family MT_VALUE mt = (v :: Type) | v -> mt
     type family MT_UNIT  mt = (u :: Type) | u -> mt
-    -- TODO: Do we need FlowRate type?
+    -- TODO: type family MT_FLOWRATE mt = (fr :: Type) | fr -> mt
+
+type MonetaryTypes'tv mt t v = (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt)
+type MonetaryTypes'tvu mt t v u = (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt)
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
index ff75bd6a25..db3bb21781 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
@@ -1,19 +1,19 @@
-{-# LANGUAGE DerivingStrategies     #-}
 {-# LANGUAGE FunctionalDependencies #-}
 module Money.Theory.SemanticMoney
     ( -- * Semantic Money Classes & Primitives
         MonetaryUnit (settle, settledAt, flowRate, rtb)
     , IndexedValue (shift1, flow1)
-    , prim2, shift2, flow2, shiftFlow2a, shiftFlow2b
-    , MonetaryParticle (align2)
+    , shift2b, flow2a, flow2b, align2a, align2b
       -- * Semantic Money Instances
     , BasicParticle (..)
-    , UniversalIndex (..)
     , PDP_Index (..), PDP_Member (..), PDP_MemberMU, pdp_UpdateMember2
       -- * Re-export Monetary Types
     , module Money.Theory.MonetaryTypes
     ) where
---
+-- base
+import           Control.Exception          (assert)
+import           Data.Tuple                 (swap)
+-- default
 import           Data.Default               (Default (..))
 --
 import           Money.Theory.MonetaryTypes
@@ -24,7 +24,7 @@ import           Money.Theory.MonetaryTypes
 ------------------------------------------------------------------------------------------------------------------------
 
 -- | A monetary unit and its operators.
-class (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt) =>
+class MonetaryTypes'tv mt t v =>
       MonetaryUnit mt t v mu | mu -> mt where
     settle    :: t -> mu -> mu
     settledAt :: mu -> t
@@ -32,66 +32,51 @@ class (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt) =>
     rtb       :: mu -> t -> v
 
 -- | An indexed monetary value and its 1-primitive operators.
-class (MonetaryUnit mt t v ix, u ~ MT_UNIT mt, Monoid ix) =>
-      IndexedValue mt t v u ix | ix -> mt where
-    shift1 :: v -> ix -> (ix, v)
-    flow1  :: v -> ix -> (ix, v)
+class (MonetaryUnit mt t v iv, u ~ MT_UNIT mt, Monoid iv, Eq iv) =>
+      IndexedValue mt t v u iv | iv -> mt where
+    shift1 :: v -> iv -> (iv, v)
+    flow1  :: v -> iv -> (iv, v)
 
 --
 -- polymorphic 2-primitives for indexed values
 --
 
--- | 2-primitive higher order function
-prim2 ::
-    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
-    ((a, b) -> (a, b)) -> t -> (a, b) -> (a, b)
-prim2 op t' (a, b) = op (settle t' a, settle t' b)
-
--- | shift2, right side biased error term adjustment
-shift2 ::
+-- | Shift value for the left side (a) or right side (b).
+shift2a, shift2b ::
     (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
     v -> t -> (a, b) -> (a, b)
-shift2 amount = prim2 op
-    where op (a, b) = let (b', amount') = shift1 amount b
-                          (a', _) = shift1 (-amount') a
-                      in  (a', b')
-
--- | flow2, right side biased error term adjustment
-flow2 ::
+shift2a v t (a, b) =
+    let (a', v') = shift1 v (settle t a)
+        -- we assume second flow1 produces no more error term.
+        (b', v'') = shift1 (-v') (settle t b)
+    in assert (v'' == -v') (a', b')
+shift2b v t (a, b) = swap (shift2a (-v) t (b, a))
+
+-- | Shifting flow for the left side (a) or right side (b).
+flow2a, flow2b ::
     (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
     v -> t -> (a, b) -> (a, b)
-flow2 r = prim2 op
-    where op (a, b) = let (b', r') = flow1 r b
-                          (a', _) = flow1 (-r') a
-                      in  (a', b')
-
--- | shiftFlow2 for the left side (a), right side biased error term adjustment
-shiftFlow2a ::
-    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
-    v -> t -> (a, b) -> (a, b)
-shiftFlow2a dr t (a, b) =
-    let ( _, b1) = flow2 (flowRate a) t (a, mempty)
-        (a', b2) = flow2 (-flowRate a + dr) t (a, mempty)
-    in  (a', b <> b1 <> b2)
-
--- | shiftFlow2 for the right side (b), right side biased error term adjustment
-shiftFlow2b ::
+flow2a dfr t (a, b) =
+    let (b1, fr_a) = flow1 (flowRate a) (settle t mempty)
+        (b2, fr_a') = flow1 (-fr_a + dfr) (settle t mempty)
+        (a', fr_a'') = flow1 (-fr_a') (settle t a)
+    in assert (fr_a' == -fr_a'') (a', b <> b1 <> b2)
+flow2b dfr t (a, b) = swap (flow2a (-dfr) t (b, a))
+
+-- | Value alignment 2-primitive, left-biased (a) or right-biased (b).
+--
+-- Note on side-biased operations:
+--   1) Left side produces error term with which right side is adjusted accordingly, and vice versa.
+--   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
+align2a, align2b ::
     (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
-    v -> t -> (a, b) -> (a, b)
-shiftFlow2b dr t (a, b) =
-    let (a1,  _) = flow2 (-flowRate b) t (mempty, b)
-        (a2, b') = flow2 (flowRate b + dr) t (mempty, b)
-    in  (a <> a1 <> a2, b')
-
-class IndexedValue mt t v u mp =>
-      MonetaryParticle mt t v u mp where
-    -- | Value alignment 2-primitive, right side biased
-    --
-    -- NOTE:
-    -- * On right side biased operations:
-    --   1) Right side produces error term with which left side is adjusted accordingly.
-    --   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
-    align2 :: forall a. IndexedValue mt t v u a => u -> u -> (mp, a) -> (mp, a)
+    MT_UNIT mt -> MT_UNIT mt -> (a, b) -> (a, b)
+align2a u u' (a, b) = (a', b')
+    where fr = flowRate a
+          (fr', e) = if u' == 0 then (0, fr `mt_v_mul_u` u) else fr `mt_v_mul_u_qr_u` (u, u')
+          a' = fst (flow1 fr' a)
+          b' = fst (flow1 (e + flowRate b) b)
+align2b u u' (a, b) = swap (align2a u u' (b, a))
 
 ------------------------------------------------------------------------------------------------------------------------
 -- Basic Particle: building block for indexes
@@ -103,7 +88,7 @@ data BasicParticle mt = BasicParticle
     , bp_flow_rate     :: MT_VALUE mt
     }
 
-deriving stock instance MonetaryTypes mt => Eq (BasicParticle mt)
+deriving instance MonetaryTypes mt => Eq (BasicParticle mt)
 
 instance MonetaryTypes mt => Semigroup (BasicParticle mt) where
     a@(BasicParticle t1 _ _) <> b@(BasicParticle t2 _ _) = BasicParticle t' (sv1 + sv2) (r1 + r2)
@@ -116,7 +101,7 @@ instance MonetaryTypes mt => Semigroup (BasicParticle mt) where
 instance MonetaryTypes mt => Monoid (BasicParticle mt) where
     mempty = BasicParticle 0 0 0
 
-instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt) =>
+instance MonetaryTypes'tv mt t v =>
          MonetaryUnit mt t v (BasicParticle mt) where
     settle t' a = a { bp_settled_at = t'
                     , bp_settled_value = rtb a t'
@@ -125,34 +110,11 @@ instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt) =>
     flowRate = bp_flow_rate
     rtb (BasicParticle t s r) t' = r `mt_v_mul_t` (t' - t) + s
 
-instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt) =>
+instance MonetaryTypes'tvu mt t v u =>
          IndexedValue mt t v u (BasicParticle mt) where
-
     shift1 x a = (a { bp_settled_value = bp_settled_value a + x }, x)
     flow1 r' a = (a { bp_flow_rate = r' }, r')
 
-instance (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt) =>
-         MonetaryParticle mt t v u (BasicParticle mt) where
-    align2 u u' (b, a) = (b', a')
-        where r = flowRate b
-              (r', er') = if u' == 0 then (0, r `mt_v_mul_u` u) else r `mt_v_mul_u_qr_u` (u, u')
-              b' = fst . flow1 r' $ b
-              a' = fst . flow1 (er' + flowRate a) $ a
-
-------------------------------------------------------------------------------------------------------------------------
--- Univeral Index
-------------------------------------------------------------------------------------------------------------------------
-
--- | A newtype wrapper of an underlying monetary unit @wp@, with a parameterized @mt@.
-newtype UniversalIndex mt wp = UniversalIndex wp
-
-deriving newtype instance (MonetaryTypes mt, Eq wp) => Eq (UniversalIndex mt wp)
-deriving newtype instance (MonetaryTypes mt, Semigroup wp) => Semigroup (UniversalIndex mt wp)
-deriving newtype instance (MonetaryTypes mt, Monoid wp) => Monoid (UniversalIndex mt wp)
-deriving newtype instance MonetaryUnit mt t v wp => MonetaryUnit mt t v (UniversalIndex mt wp)
-deriving newtype instance IndexedValue mt t v u wp => IndexedValue mt t v u (UniversalIndex mt wp)
-deriving newtype instance MonetaryParticle mt t v u wp => MonetaryParticle mt t v u (UniversalIndex mt wp)
-
 ------------------------------------------------------------------------------------------------------------------------
 -- Proportional Distribution Pool (PDP)
 ------------------------------------------------------------------------------------------------------------------------
@@ -172,14 +134,14 @@ type PDP_MemberMU mt wp = (PDP_Index mt wp, PDP_Member mt wp)
 
 pdp_UpdateMember2 ::
     ( IndexedValue mt t v u a
-    , MonetaryParticle mt t v u wp
+    , IndexedValue mt t v u wp
     , mu ~ PDP_MemberMU mt wp
     ) =>
     u -> t -> (a, mu) -> (a, mu)
 pdp_UpdateMember2 u' t' (a, (b, pm)) = (a'', (b'', pm''))
     where (PDP_Index tu mpi, pm'@(PDP_Member u _ _)) = settle t' (b, pm)
           tu' = tu + u' - u
-          (mpi', a'') = align2 tu tu' (mpi, settle t' a)
+          (mpi', a'') = align2b tu tu' (mpi, settle t' a)
           b''  = PDP_Index tu' mpi'
           pm'' = pm' { pdpm_owned_unit = u', pdpm_synced_wp = mpi' }
 
@@ -187,12 +149,7 @@ pdp_UpdateMember2 u' t' (a, (b, pm)) = (a'', (b'', pm''))
 -- PDP_Index as MonetaryIndex
 --
 
-instance MonetaryUnit mt t v wp =>
-         MonetaryUnit mt t v (PDP_Index mt wp) where
-    settle t' a@(PDP_Index _ mpi) = a { pdpi_wp = settle t' mpi }
-    settledAt (PDP_Index _ mpi) = settledAt mpi
-    flowRate (PDP_Index _ mpi) = flowRate mpi
-    rtb (PDP_Index _ mpi) = rtb mpi
+deriving instance (MonetaryTypes mt, Eq wp) => Eq (PDP_Index mt wp)
 
 instance (MonetaryTypes mt, Semigroup wp) => Semigroup (PDP_Index mt wp) where
     -- The binary operator supports negative unit values while abiding the monoidal laws.
@@ -203,7 +160,14 @@ instance (MonetaryTypes mt, Semigroup wp) => Semigroup (PDP_Index mt wp) where
 instance (MonetaryTypes mt, Monoid wp) => Monoid (PDP_Index mt wp) where
     mempty = PDP_Index 0 mempty
 
-instance MonetaryParticle mt t v u wp =>
+instance MonetaryUnit mt t v wp =>
+         MonetaryUnit mt t v (PDP_Index mt wp) where
+    settle t' a@(PDP_Index _ mpi) = a { pdpi_wp = settle t' mpi }
+    settledAt (PDP_Index _ mpi) = settledAt mpi
+    flowRate (PDP_Index _ mpi) = flowRate mpi
+    rtb (PDP_Index _ mpi) = rtb mpi
+
+instance IndexedValue mt t v u wp =>
          IndexedValue mt t v u (PDP_Index mt wp) where
     shift1 x a@(PDP_Index tu mpi) = (a { pdpi_wp = mpi' }, x' `mt_v_mul_u` tu)
         where (mpi', x') = if tu == 0 then (mpi, 0) else shift1 (x `mt_v_div_u` tu) mpi
@@ -212,13 +176,19 @@ instance MonetaryParticle mt t v u wp =>
         where (mpi', r'') = if tu == 0 then flow1 0 mpi else flow1 (r' `mt_v_div_u` tu) mpi
 
 --
--- PDP_MemberMU as MonetaryUnit
+-- PDP_Member
 --
 
 instance (MonetaryTypes mt, Monoid wp) =>
          Default (PDP_Member mt wp) where
     def = PDP_Member 0 0 mempty
 
+deriving instance (MonetaryTypes mt, Eq wp) => Eq (PDP_Member mt wp)
+
+--
+-- PDP_MemberMU as MonetaryUnit
+--
+
 instance MonetaryUnit mt t v wp =>
          MonetaryUnit mt t v (PDP_MemberMU mt wp) where
     settle t' (pix, pm) = (pix', pm')
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
new file mode 100644
index 0000000000..ebdb70ca13
--- /dev/null
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
@@ -0,0 +1,14 @@
+module Money.Theory.TokenModel where
+--
+import           Money.Theory.SemanticMoney
+
+
+data TokenEvent mt acc where
+    TransferEvent :: forall mt acc {t} {v} {u}.
+        MonetaryTypes'tvu mt t v u =>
+        t -> acc -> acc -> v -> TokenEvent mt acc
+    -- UpdateFlowEvent :: forall mt acc {t} {v} {u}.
+    --     MonetaryTypes'tvu mt t v u =>
+    --     t -> acc -> acc -> v -> TokenEvent mt acc
+
+data TokenModel mt acc
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
index fd1ad18329..91d652cdf5 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
@@ -79,10 +79,10 @@ uu_f1_f2 f1 f2 t1 {- f1 -} t2 {- f2 -} t3 =
     where (a, b) = (mempty :: TestUniversalIndex, mempty :: TestUniversalIndex)
           (a', b') = f2 t2 (f1 t1 (a, b))
 
-uu_shift2_shift2 x1 x2 = uu_f1_f2 (shift2 x1) (shift2 x2)
-uu_flow2_flow2 r1 r2 = uu_f1_f2 (flow2 r1) (flow2 r2)
-uu_shift2_flow2 x r = uu_f1_f2 (shift2 x) (flow2 r)
-uu_flow2_shift2 r x = uu_f1_f2 (flow2 r) (shift2 x)
+uu_shift2_shift2 x1 x2 = uu_f1_f2 (shift2b x1) (shift2b x2)
+uu_flow2_flow2 r1 r2 = uu_f1_f2 (flow2b r1) (flow2b r2)
+uu_shift2_flow2 x r = uu_f1_f2 (shift2b x) (flow2b r)
+uu_flow2_shift2 r x = uu_f1_f2 (flow2b r) (shift2b x)
 
 one2one_tests = describe "1to1 2-primitives" $ do
     it "uidx:uidx shift2 shift2" $ property uu_shift2_shift2
@@ -109,72 +109,65 @@ updp_u1_f1_u2_f2 f1 f2 t1 u1 t2 {- f1 -} t3 u2 t4 {- f2 -} t5 =
           (a'', (b'', b2)) = pdp_UpdateMember2 u2 t3 (a', (b', def :: TestPDP_Member))
           (a''', b''') = f2 t4 (a'', b'')
 
-updp_u1_shift2_u1_shift2 x1 x2 = updp_u1_f1_u1_f2 (shift2 x1) (shift2 x2)
-updp_u1_flow2_u1_flow2 r1 r2 = updp_u1_f1_u1_f2 (flow2 r1) (flow2 r2)
-updp_u1_shift2_u1_flow2 x r = updp_u1_f1_u1_f2 (shift2 x) (flow2 r)
-updp_u1_flow2_u1_shift2 r x = updp_u1_f1_u1_f2 (shift2 r) (flow2 x)
-updp_u1_shift2_u2_shift2 x1 x2 = updp_u1_f1_u2_f2 (shift2 x1) (shift2 x2)
-updp_u1_flow2_u2_flow2 r1 r2 = updp_u1_f1_u2_f2 (flow2 r1) (flow2 r2)
-updp_u1_flow2_u2_shift2 r x = updp_u1_f1_u2_f2 (flow2 r) (shift2 x)
-updp_u1_shift2_u2_flow2 x r = updp_u1_f1_u2_f2 (shift2 x) (flow2 r)
+updp_u1_shift2_u1_shift2 x1 x2 = updp_u1_f1_u1_f2 (shift2b x1) (shift2b x2)
+updp_u1_flow2_u1_flow2 r1 r2 = updp_u1_f1_u1_f2 (flow2a r1) (flow2a r2)
+updp_u1_shift2_u1_flow2 x r = updp_u1_f1_u1_f2 (shift2b x) (flow2a r)
+updp_u1_flow2_u1_shift2 r x = updp_u1_f1_u1_f2 (shift2b r) (flow2a x)
+updp_u1_shift2_u2_shift2 x1 x2 = updp_u1_f1_u2_f2 (shift2b x1) (shift2b x2)
+updp_u1_flow2_u2_flow2 r1 r2 = updp_u1_f1_u2_f2 (flow2a r1) (flow2a r2)
+updp_u1_flow2_u2_shift2 r x = updp_u1_f1_u2_f2 (flow2a r) (shift2b x)
+updp_u1_shift2_u2_flow2 x r = updp_u1_f1_u2_f2 (shift2b x) (flow2a r)
 
 one2n_pd_tests = describe "1toN proportional distribution 2-primitives" $ do
-    it "uidx:pdidx u1 shift2 u1 shift2" $ property updp_u1_shift2_u1_shift2
-    it "uidx:pdidx u1 flow2  u1 flow2"  $ property updp_u1_flow2_u1_flow2
-    it "uidx:pdidx u1 shift2 u1 flow2"  $ property updp_u1_shift2_u1_flow2
-    it "uidx:pdidx u1 flow2  u1 shift2" $ property updp_u1_flow2_u1_shift2
-    it "uidx:pdidx u1 shift2 u2 shift2" $ property updp_u1_shift2_u2_shift2
-    it "uidx:pdidx u1 flow2  u2 flow2"  $ property updp_u1_flow2_u2_flow2
-    it "uidx:pdidx u1 flow2  u2 shift2" $ property updp_u1_flow2_u2_shift2
-    it "uidx:pdidx u1 shift2 u2 flow2"  $ property updp_u1_shift2_u2_flow2
+    it "uidx:pdp u1 shift2 u1 shift2" $ property updp_u1_shift2_u1_shift2
+    it "uidx:pdp u1 flow2  u1 flow2"  $ property updp_u1_flow2_u1_flow2
+    it "uidx:pdp u1 shift2 u1 flow2"  $ property updp_u1_shift2_u1_flow2
+    it "uidx:pdp u1 flow2  u1 shift2" $ property updp_u1_flow2_u1_shift2
+    it "uidx:pdp u1 shift2 u2 shift2" $ property updp_u1_shift2_u2_shift2
+    it "uidx:pdp u1 flow2  u2 flow2"  $ property updp_u1_flow2_u2_flow2
+    it "uidx:pdp u1 flow2  u2 shift2" $ property updp_u1_flow2_u2_shift2
+    it "uidx:pdp u1 shift2 u2 flow2"  $ property updp_u1_shift2_u2_flow2
 
 --------------------------------------------------------------------------------
 -- (Constant Rate) Flow 2-Primitive
 --------------------------------------------------------------------------------
 
-uu_flow2 (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
-    flowRate b' == r2 && flowRate a' == -r2 &&
-    r1 `mt_v_mul_t` (t2 - t1) + r2 `mt_v_mul_t` (t3 - t2) == rtb b' t3 - rtb b t1
-    where (a', b') = flow2 r2 t2 (flow2 r1 t1 (a, b))
-
-updp_flow2 (a :: TestUniversalIndex) t1 r1 t2 r2 t3 =
-    flowRate b'' == r2 && flowRate a'' == -r2 &&
-    flowRate (b'', b1') == r2 &&
-    r1 `mt_v_mul_t` (t2 - t1) + r2 `mt_v_mul_t` (t3 - t2) == rtb (b'', b1') t3 - rtb (b', b1') t1
-    where (a', (b', b1')) = pdp_UpdateMember2 1 t1 (a, (mempty :: TestPDP_Index, def))
-          (a'', b'') = flow2 r2 t2 (flow2 r1 t1 (a', b'))
-
-uu_shiftFlow2a (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
+uu_flow2a (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
     flowRate b' - flowRate b == r1 + r2 && flowRate a' - flowRate a == -r1 -r2 &&
     rtb b' t3 - rtb b t3 == rtb a t3 - rtb a' t3 &&
     -- for shift flow semantics: rtb b' t3 - (rtb b t3 - rtb b t1) - rtb b t1 == rtb b' t3 - rtb b t3
     r1 `mt_v_mul_t` (t2 - t1) + (r1 + r2) `mt_v_mul_t` (t3 - t2) == rtb b' t3 - rtb b t3
-    where (a', b') = shiftFlow2a r2 t2 (shiftFlow2a r1 t1 (a, b))
+    where (a', b') = flow2a r2 t2 (flow2a r1 t1 (a, b))
 
-uu_shiftFlow2b (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
+uu_flow2b (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
     flowRate b' - flowRate b == r1 + r2 && flowRate a' - flowRate a == -r1 -r2 &&
     rtb b' t3 - rtb b t3 == rtb a t3 - rtb a' t3 &&
     -- ditto
     r1 `mt_v_mul_t` (t2 - t1) + (r1 + r2) `mt_v_mul_t` (t3 - t2) == rtb b' t3 - rtb b t3
-    where (a', b') = shiftFlow2b r2 t2 (shiftFlow2b r1 t1 (a, b))
+    where (a', b') = flow2b r2 t2 (flow2b r1 t1 (a, b))
+
+-- NOTE: updp_flow2a is an invalid property due to right side biased error term adjustment.
 
--- NOTE: updp_shiftFlow2a is an invalid property due to right side biansed error term adjustment.
+-- updp_flow2a (a :: TestUniversalIndex) t1 r1 t2 r2 t3 =
+--     flowRate b'' == r2 && flowRate a'' == -r2 &&
+--     flowRate (b'', b1') == r2 &&
+--     r1 `mt_v_mul_t` (t2 - t1) + r2 `mt_v_mul_t` (t3 - t2) == rtb (b'', b1') t3 - rtb (b', b1') t1
+--     where (a', (b', b1')) = pdp_UpdateMember2 1 t1 (a, (mempty :: TestPDP_Index, def))
+--           (a'', b'') = flow2a r2 t2 (flow2a r1 t1 (a', b'))
 
-updp_shiftFlow2b (a :: TestUniversalIndex) t1 r1 t2 r2 t3 =
+updp_flow2b (a :: TestUniversalIndex) t1 r1 t2 r2 t3 =
     flowRate b'' - flowRate b' == r1 + r2 && flowRate a'' - flowRate a' == -r1 -r2 &&
     flowRate (b'', b1') == r1 + r2 &&
     rtb (b'', b1') t3 - rtb (b', b1') t3 == rtb a' t3 - rtb a'' t3 &&
     -- ditto
     r1 `mt_v_mul_t` (t2 - t1) + (r1 + r2) `mt_v_mul_t` (t3 - t2) == rtb (b'', b1') t3 - rtb (b', b1') t3
     where (a', (b', b1')) = pdp_UpdateMember2 1 t1 (a, (mempty :: TestPDP_Index, def))
-          (a'', b'') = shiftFlow2b r2 t2 (shiftFlow2b r1 t1 (a', b'))
+          (a'', b'') = flow2b r2 t2 (flow2b r1 t1 (a', b'))
 
 flow2_tests = describe "flow2 tests" $ do
-    it "uidx:uidx flow2" $ property uu_flow2
-    it "uidx:pdidx flow2" $ property updp_flow2
-    it "uidx:uidx shiftFlow2a" $ property uu_shiftFlow2a
-    it "uidx:uidx shiftFlow2b" $ property uu_shiftFlow2b
-    it "uidx:pdidx shiftFlow2b" $ property updp_shiftFlow2b
+    it "uidx:uidx flow2a" $ property uu_flow2a
+    it "uidx:uidx flow2b" $ property uu_flow2b
+    it "uidx:pdp flow2b" $ property updp_flow2b
 
 tests = describe "Semantic money properties" $ do
     mu_laws
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
index 226601f398..bea1b8e4a3 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
@@ -35,27 +35,19 @@ type TesBasicParticle = BasicParticle TestMonetaryTypes
 instance Arbitrary TesBasicParticle where
     arbitrary = BasicParticle <$> arbitrary <*> arbitrary <*> arbitrary
 
--- TesBasicParticle
+-- TestUniversalIndex
 --
-type TestUniversalIndex = UniversalIndex TestMonetaryTypes TesBasicParticle
-deriving instance Show TestUniversalIndex
-instance Arbitrary TestUniversalIndex where
-    arbitrary = UniversalIndex <$> arbitrary
+type TestUniversalIndex = TesBasicParticle
 
--- PDP_Index
+-- TestPDP_Index, TestPDP_Member, TestPDP_MemberMU
 --
 type TestPDP_Index = PDP_Index TestMonetaryTypes TesBasicParticle
 deriving instance Show TestPDP_Index
-deriving instance Eq TestPDP_Index
 instance Arbitrary TestPDP_Index where
     arbitrary = PDP_Index <$> arbitrary <*> arbitrary
 
--- PDP_Member
---
-
 type TestPDP_Member = PDP_Member TestMonetaryTypes TesBasicParticle
 deriving instance Show TestPDP_Member
-deriving instance Eq TestPDP_Member
 instance Arbitrary TestPDP_Member where
     arbitrary = PDP_Member <$> arbitrary <*> arbitrary <*> arbitrary
 

From 7facce88356754f4bd9f83ec10fb9f1363275ee3 Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Thu, 12 Jun 2025 18:09:59 +0300
Subject: [PATCH 05/11] add MT_FLOWRATE to the MonetaryTypes

---
 .../src/Money/Theory/MonetaryTypes.hs         | 42 ++++++++++----
 .../src/Money/Theory/SemanticMoney.hs         | 58 +++++++++----------
 .../src/Money/Theory/TokenModel.hs            |  4 +-
 .../test/Money/Theory/SemanticMoney_prop.hs   | 37 ++++++------
 .../test/Money/Theory/TestMonetaryTypes.hs    | 11 +++-
 5 files changed, 89 insertions(+), 63 deletions(-)

diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
index 6a1e4ef1c8..cafbae15ab 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
@@ -3,10 +3,12 @@
 {-# LANGUAGE TypeFamilyDependencies #-}
 module Money.Theory.MonetaryTypes
     ( MonetaryTypes
-      ( MT_TIME, MT_VALUE, MT_UNIT
-      , mt_v_mul_t, mt_v_mul_u, mt_v_div_u, mt_v_mul_u_qr_u
+      ( MT_TIME, MT_VALUE, MT_FLOWRATE, MT_UNIT
+      , mt_fr_mul_t
+      , mt_v_mul_u, mt_v_div_u, mt_v_mul_u_qr_u
+      , mt_fr_mul_u, mt_fr_div_u, mt_fr_mul_u_qr_u
       )
-    , MonetaryTypes'tv, MonetaryTypes'tvu
+    , MonetaryTypes'tv, MonetaryTypes'tvr, MonetaryTypes'tvru
     ) where
 -- base
 import           Data.Kind (Type)
@@ -19,14 +21,15 @@ import           Data.Kind (Type)
 --   * Use type family dependencies to make these types to the index type injective.
 class ( Eq (MT_TIME mt), Ord (MT_TIME mt), Num (MT_TIME mt)
       , Eq (MT_VALUE mt), Ord (MT_VALUE mt), Num (MT_VALUE mt)
+      , Eq (MT_FLOWRATE mt), Ord (MT_FLOWRATE mt), Num (MT_FLOWRATE mt)
       , Eq (MT_UNIT mt), Ord (MT_UNIT mt), Num (MT_UNIT mt)
       ) =>
       MonetaryTypes mt where
-    mt_v_mul_t :: MT_VALUE mt -> MT_TIME mt -> MT_VALUE mt
-    default mt_v_mul_t ::
-        Integral (MT_TIME mt) =>
-        MT_VALUE mt -> MT_TIME mt -> MT_VALUE mt
-    mt_v_mul_t v t = v * (fromInteger . toInteger) t
+    mt_fr_mul_t :: MT_FLOWRATE mt -> MT_TIME mt -> MT_VALUE mt
+    default mt_fr_mul_t ::
+        (Integral (MT_TIME mt), Integral (MT_FLOWRATE mt))=>
+        MT_FLOWRATE mt -> MT_TIME mt -> MT_VALUE mt
+    mt_fr_mul_t fr t = fromInteger (toInteger fr * toInteger t)
 
     mt_v_mul_u :: MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
     default mt_v_mul_u ::
@@ -46,10 +49,29 @@ class ( Eq (MT_TIME mt), Ord (MT_TIME mt), Num (MT_TIME mt)
         MT_VALUE mt -> (MT_UNIT mt, MT_UNIT mt) -> (MT_VALUE mt, MT_VALUE mt)
     mt_v_mul_u_qr_u v (u1, u2) = (v * (fromInteger . toInteger) u1) `quotRem` (fromInteger . toInteger) u2
 
+    mt_fr_mul_u :: MT_FLOWRATE mt -> MT_UNIT mt -> MT_FLOWRATE mt
+    default mt_fr_mul_u ::
+        Integral (MT_UNIT mt) =>
+        MT_FLOWRATE mt -> MT_UNIT mt -> MT_FLOWRATE mt
+    mt_fr_mul_u fr u = fr * (fromInteger . toInteger) u
+
+    mt_fr_div_u :: MT_FLOWRATE mt -> MT_UNIT mt -> MT_FLOWRATE mt
+    default mt_fr_div_u ::
+        (Integral (MT_FLOWRATE mt), Integral (MT_UNIT mt)) =>
+        MT_FLOWRATE mt -> MT_UNIT mt -> MT_FLOWRATE mt
+    mt_fr_div_u fr u = let u' = (fromInteger . toInteger) u in fr `div` u'
+
+    mt_fr_mul_u_qr_u :: MT_FLOWRATE mt -> (MT_UNIT mt, MT_UNIT mt) -> (MT_FLOWRATE mt, MT_FLOWRATE mt)
+    default mt_fr_mul_u_qr_u ::
+        (Integral (MT_FLOWRATE mt), Integral (MT_UNIT mt)) =>
+        MT_FLOWRATE mt -> (MT_UNIT mt, MT_UNIT mt) -> (MT_FLOWRATE mt, MT_FLOWRATE mt)
+    mt_fr_mul_u_qr_u fr (u1, u2) = (fr * (fromInteger . toInteger) u1) `quotRem` (fromInteger . toInteger) u2
+
     type family MT_TIME  mt = (t :: Type) | t -> mt
     type family MT_VALUE mt = (v :: Type) | v -> mt
+    type family MT_FLOWRATE mt = (fr :: Type) | fr -> mt
     type family MT_UNIT  mt = (u :: Type) | u -> mt
-    -- TODO: type family MT_FLOWRATE mt = (fr :: Type) | fr -> mt
 
 type MonetaryTypes'tv mt t v = (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt)
-type MonetaryTypes'tvu mt t v u = (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt, u ~ MT_UNIT mt)
+type MonetaryTypes'tvr mt t v fr = (MonetaryTypes'tv mt t v, fr ~ MT_FLOWRATE mt)
+type MonetaryTypes'tvru mt t v fr u = (MonetaryTypes'tvr mt t v fr, u ~ MT_UNIT mt)
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
index db3bb21781..878bbe0ec5 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
@@ -24,18 +24,18 @@ import           Money.Theory.MonetaryTypes
 ------------------------------------------------------------------------------------------------------------------------
 
 -- | A monetary unit and its operators.
-class MonetaryTypes'tv mt t v =>
-      MonetaryUnit mt t v mu | mu -> mt where
+class (MonetaryTypes'tvr mt t v fr, Eq mu) =>
+      MonetaryUnit mt t v fr mu | mu -> mt where
     settle    :: t -> mu -> mu
     settledAt :: mu -> t
-    flowRate  :: mu -> v
+    flowRate  :: mu -> fr
     rtb       :: mu -> t -> v
 
 -- | An indexed monetary value and its 1-primitive operators.
-class (MonetaryUnit mt t v iv, u ~ MT_UNIT mt, Monoid iv, Eq iv) =>
-      IndexedValue mt t v u iv | iv -> mt where
+class (MonetaryUnit mt t v fr iv, u ~ MT_UNIT mt, Monoid iv, Eq iv) =>
+      IndexedValue mt t v fr u iv | iv -> mt where
     shift1 :: v -> iv -> (iv, v)
-    flow1  :: v -> iv -> (iv, v)
+    flow1  :: fr -> iv -> (iv, fr)
 
 --
 -- polymorphic 2-primitives for indexed values
@@ -43,7 +43,7 @@ class (MonetaryUnit mt t v iv, u ~ MT_UNIT mt, Monoid iv, Eq iv) =>
 
 -- | Shift value for the left side (a) or right side (b).
 shift2a, shift2b ::
-    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
+    (IndexedValue mt t v fr u a, IndexedValue mt t v fr u b) =>
     v -> t -> (a, b) -> (a, b)
 shift2a v t (a, b) =
     let (a', v') = shift1 v (settle t a)
@@ -54,8 +54,8 @@ shift2b v t (a, b) = swap (shift2a (-v) t (b, a))
 
 -- | Shifting flow for the left side (a) or right side (b).
 flow2a, flow2b ::
-    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
-    v -> t -> (a, b) -> (a, b)
+    (IndexedValue mt t v fr u a, IndexedValue mt t v fr u b) =>
+    fr -> t -> (a, b) -> (a, b)
 flow2a dfr t (a, b) =
     let (b1, fr_a) = flow1 (flowRate a) (settle t mempty)
         (b2, fr_a') = flow1 (-fr_a + dfr) (settle t mempty)
@@ -69,11 +69,11 @@ flow2b dfr t (a, b) = swap (flow2a (-dfr) t (b, a))
 --   1) Left side produces error term with which right side is adjusted accordingly, and vice versa.
 --   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
 align2a, align2b ::
-    (IndexedValue mt t v u a, IndexedValue mt t v u b) =>
+    (IndexedValue mt t v fr u a, IndexedValue mt t v fr u b) =>
     MT_UNIT mt -> MT_UNIT mt -> (a, b) -> (a, b)
 align2a u u' (a, b) = (a', b')
     where fr = flowRate a
-          (fr', e) = if u' == 0 then (0, fr `mt_v_mul_u` u) else fr `mt_v_mul_u_qr_u` (u, u')
+          (fr', e) = if u' == 0 then (0, fr `mt_fr_mul_u` u) else fr `mt_fr_mul_u_qr_u` (u, u')
           a' = fst (flow1 fr' a)
           b' = fst (flow1 (e + flowRate b) b)
 align2b u u' (a, b) = swap (align2a u u' (b, a))
@@ -83,9 +83,9 @@ align2b u u' (a, b) = swap (align2a u u' (b, a))
 ------------------------------------------------------------------------------------------------------------------------
 
 data BasicParticle mt = BasicParticle
-    { bp_settled_at    :: MT_TIME  mt
+    { bp_settled_at    :: MT_TIME mt
     , bp_settled_value :: MT_VALUE mt
-    , bp_flow_rate     :: MT_VALUE mt
+    , bp_flow_rate     :: MT_FLOWRATE mt
     }
 
 deriving instance MonetaryTypes mt => Eq (BasicParticle mt)
@@ -101,17 +101,17 @@ instance MonetaryTypes mt => Semigroup (BasicParticle mt) where
 instance MonetaryTypes mt => Monoid (BasicParticle mt) where
     mempty = BasicParticle 0 0 0
 
-instance MonetaryTypes'tv mt t v =>
-         MonetaryUnit mt t v (BasicParticle mt) where
+instance MonetaryTypes'tvr mt t v fr =>
+         MonetaryUnit mt t v fr (BasicParticle mt) where
     settle t' a = a { bp_settled_at = t'
                     , bp_settled_value = rtb a t'
                     }
     settledAt = bp_settled_at
     flowRate = bp_flow_rate
-    rtb (BasicParticle t s r) t' = r `mt_v_mul_t` (t' - t) + s
+    rtb (BasicParticle t s r) t' = r `mt_fr_mul_t` (t' - t) + s
 
-instance MonetaryTypes'tvu mt t v u =>
-         IndexedValue mt t v u (BasicParticle mt) where
+instance MonetaryTypes'tvru mt t v fr u =>
+         IndexedValue mt t v fr u (BasicParticle mt) where
     shift1 x a = (a { bp_settled_value = bp_settled_value a + x }, x)
     flow1 r' a = (a { bp_flow_rate = r' }, r')
 
@@ -133,8 +133,8 @@ data PDP_Member mt wp = PDP_Member
 type PDP_MemberMU mt wp = (PDP_Index mt wp, PDP_Member mt wp)
 
 pdp_UpdateMember2 ::
-    ( IndexedValue mt t v u a
-    , IndexedValue mt t v u wp
+    ( IndexedValue mt t v fr u a
+    , IndexedValue mt t v fr u wp
     , mu ~ PDP_MemberMU mt wp
     ) =>
     u -> t -> (a, mu) -> (a, mu)
@@ -160,20 +160,20 @@ instance (MonetaryTypes mt, Semigroup wp) => Semigroup (PDP_Index mt wp) where
 instance (MonetaryTypes mt, Monoid wp) => Monoid (PDP_Index mt wp) where
     mempty = PDP_Index 0 mempty
 
-instance MonetaryUnit mt t v wp =>
-         MonetaryUnit mt t v (PDP_Index mt wp) where
+instance MonetaryUnit mt t v fr wp =>
+         MonetaryUnit mt t v fr (PDP_Index mt wp) where
     settle t' a@(PDP_Index _ mpi) = a { pdpi_wp = settle t' mpi }
     settledAt (PDP_Index _ mpi) = settledAt mpi
     flowRate (PDP_Index _ mpi) = flowRate mpi
     rtb (PDP_Index _ mpi) = rtb mpi
 
-instance IndexedValue mt t v u wp =>
-         IndexedValue mt t v u (PDP_Index mt wp) where
+instance IndexedValue mt t v fr u wp =>
+         IndexedValue mt t v fr u (PDP_Index mt wp) where
     shift1 x a@(PDP_Index tu mpi) = (a { pdpi_wp = mpi' }, x' `mt_v_mul_u` tu)
         where (mpi', x') = if tu == 0 then (mpi, 0) else shift1 (x `mt_v_div_u` tu) mpi
 
-    flow1 r' a@(PDP_Index tu mpi) = (a { pdpi_wp = mpi' }, r'' `mt_v_mul_u` tu)
-        where (mpi', r'') = if tu == 0 then flow1 0 mpi else flow1 (r' `mt_v_div_u` tu) mpi
+    flow1 r' a@(PDP_Index tu mpi) = (a { pdpi_wp = mpi' }, r'' `mt_fr_mul_u` tu)
+        where (mpi', r'') = if tu == 0 then flow1 0 mpi else flow1 (r' `mt_fr_div_u` tu) mpi
 
 --
 -- PDP_Member
@@ -189,8 +189,8 @@ deriving instance (MonetaryTypes mt, Eq wp) => Eq (PDP_Member mt wp)
 -- PDP_MemberMU as MonetaryUnit
 --
 
-instance MonetaryUnit mt t v wp =>
-         MonetaryUnit mt t v (PDP_MemberMU mt wp) where
+instance MonetaryUnit mt t v fr wp =>
+         MonetaryUnit mt t v fr (PDP_MemberMU mt wp) where
     settle t' (pix, pm) = (pix', pm')
         where sv' = rtb (pix, pm) t'
               pix'@(PDP_Index _ mpi') = settle t' pix
@@ -198,7 +198,7 @@ instance MonetaryUnit mt t v wp =>
 
     settledAt (_, PDP_Member _ _ mps) = settledAt mps
 
-    flowRate (PDP_Index _ mpi, PDP_Member u _ _) = flowRate mpi `mt_v_mul_u` u
+    flowRate (PDP_Index _ mpi, PDP_Member u _ _) = flowRate mpi `mt_fr_mul_u` u
 
     rtb (PDP_Index _ mpi, PDP_Member u sv mps) t' = sv +
         -- let ti = bp_settled_at mpi
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
index ebdb70ca13..70c10bd2ab 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
@@ -4,8 +4,8 @@ import           Money.Theory.SemanticMoney
 
 
 data TokenEvent mt acc where
-    TransferEvent :: forall mt acc {t} {v} {u}.
-        MonetaryTypes'tvu mt t v u =>
+    TransferEvent :: forall mt acc {t} {v}.
+        MonetaryTypes'tv mt t v =>
         t -> acc -> acc -> v -> TokenEvent mt acc
     -- UpdateFlowEvent :: forall mt acc {t} {v} {u}.
     --     MonetaryTypes'tvu mt t v u =>
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
index 91d652cdf5..b6919fc20f 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
@@ -16,14 +16,12 @@ import           Money.Theory.TestMonetaryTypes
 -- Monetary Units Laws: settle-idempotency, constant-rtb
 --------------------------------------------------------------------------------
 
-mu_settle_idempotency :: ( MonetaryUnit TestMonetaryTypes TestTime TestMValue mu
-                      , Eq mu
-                      ) => mu -> TestTime -> Bool
+mu_settle_idempotency :: MonetaryUnit mt t v fr mu => mu -> t -> Bool
 mu_settle_idempotency a t =
     settledAt (settle t a) == t &&
     settle t a == settle t (settle t a)
-mu_constant_rtb :: ( MonetaryUnit TestMonetaryTypes TestTime TestMValue mu
-                   ) => mu -> TestTime -> TestTime -> TestTime -> Bool
+
+mu_constant_rtb :: MonetaryUnit mt t v fr mu => mu -> t -> t -> t -> Bool
 mu_constant_rtb a t1 t2 t3 =
     rtb (settle t1 a) t3 == rtb a t3 &&
     rtb (settle t2 a) t3 == rtb a t3 &&
@@ -33,8 +31,8 @@ bp_settle_idempotency (a :: TesBasicParticle) = mu_settle_idempotency a
 bp_constant_rtb (a :: TesBasicParticle) = mu_constant_rtb a
 uidx_settle_idempotency (a :: TestUniversalIndex) = mu_settle_idempotency a
 uidx_constant_rtb (a :: TestUniversalIndex) = mu_constant_rtb a
-pdidx_settle_idempotency (a :: TestPDP_Index) = mu_settle_idempotency a
-pdidx_constant_rtb (a :: TestPDP_Index) = mu_constant_rtb a
+pdpidx_settle_idempotency (a :: TestPDP_Index) = mu_settle_idempotency a
+pdpidx_constant_rtb (a :: TestPDP_Index) = mu_constant_rtb a
 pdmb_settle_idempotency (a :: TestPDP_MemberMU) = mu_settle_idempotency a
 pdmb_constant_rtb (a :: TestPDP_Index) t1 u1 t2 u2 = mu_constant_rtb b''
     -- adding two members to an existing index
@@ -46,8 +44,8 @@ mu_laws = describe "monetary unit laws" $ do
     it "bp constant rtb" $ property bp_constant_rtb
     it "uidx settle idempotency" $ property uidx_settle_idempotency
     it "uidx constant rtb" $ property uidx_constant_rtb
-    it "pdidx settle idempotency" $ property pdidx_settle_idempotency
-    it "pdidx constant rtb" $ property pdidx_constant_rtb
+    it "pdpidx settle idempotency" $ property pdpidx_settle_idempotency
+    it "pdpidx constant rtb" $ property pdpidx_constant_rtb
     it "pdmb settle idempotency" $ property pdmb_settle_idempotency
     it "pdmb contant rtb" $ property pdmb_constant_rtb
 
@@ -101,6 +99,11 @@ updp_u1_f1_u1_f2 f1 f2 t1 u1 t2 {- f1 -} t3 {- f2 -} t4 u2 t5 =
           (a', b') = f2 t3 (f1 t2 (a, b))
           (a'', (b'', b1')) = pdp_UpdateMember2 u2 t4 (a', (b', b1))
 
+updp_u1_shift2_u1_shift2 x1 x2 = updp_u1_f1_u1_f2 (shift2b x1) (shift2b x2)
+updp_u1_flow2_u1_flow2 r1 r2 = updp_u1_f1_u1_f2 (flow2a r1) (flow2a r2)
+updp_u1_shift2_u1_flow2 x r = updp_u1_f1_u1_f2 (shift2b x) (flow2a r)
+updp_u1_flow2_u1_shift2 r x = updp_u1_f1_u1_f2 (flow2a x) (shift2b r)
+
 updp_u1_f1_u2_f2 f1 f2 t1 u1 t2 {- f1 -} t3 u2 t4 {- f2 -} t5 =
     pdpi_total_units b''' == u1 + u2 &&
     0 == rtb a''' t5 + rtb (b''', b1) t5 + rtb (b''', b2) t5
@@ -109,10 +112,6 @@ updp_u1_f1_u2_f2 f1 f2 t1 u1 t2 {- f1 -} t3 u2 t4 {- f2 -} t5 =
           (a'', (b'', b2)) = pdp_UpdateMember2 u2 t3 (a', (b', def :: TestPDP_Member))
           (a''', b''') = f2 t4 (a'', b'')
 
-updp_u1_shift2_u1_shift2 x1 x2 = updp_u1_f1_u1_f2 (shift2b x1) (shift2b x2)
-updp_u1_flow2_u1_flow2 r1 r2 = updp_u1_f1_u1_f2 (flow2a r1) (flow2a r2)
-updp_u1_shift2_u1_flow2 x r = updp_u1_f1_u1_f2 (shift2b x) (flow2a r)
-updp_u1_flow2_u1_shift2 r x = updp_u1_f1_u1_f2 (shift2b r) (flow2a x)
 updp_u1_shift2_u2_shift2 x1 x2 = updp_u1_f1_u2_f2 (shift2b x1) (shift2b x2)
 updp_u1_flow2_u2_flow2 r1 r2 = updp_u1_f1_u2_f2 (flow2a r1) (flow2a r2)
 updp_u1_flow2_u2_shift2 r x = updp_u1_f1_u2_f2 (flow2a r) (shift2b x)
@@ -136,14 +135,14 @@ uu_flow2a (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
     flowRate b' - flowRate b == r1 + r2 && flowRate a' - flowRate a == -r1 -r2 &&
     rtb b' t3 - rtb b t3 == rtb a t3 - rtb a' t3 &&
     -- for shift flow semantics: rtb b' t3 - (rtb b t3 - rtb b t1) - rtb b t1 == rtb b' t3 - rtb b t3
-    r1 `mt_v_mul_t` (t2 - t1) + (r1 + r2) `mt_v_mul_t` (t3 - t2) == rtb b' t3 - rtb b t3
+    r1 `mt_fr_mul_t` (t2 - t1) + (r1 + r2) `mt_fr_mul_t` (t3 - t2) == rtb b' t3 - rtb b t3
     where (a', b') = flow2a r2 t2 (flow2a r1 t1 (a, b))
 
 uu_flow2b (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
     flowRate b' - flowRate b == r1 + r2 && flowRate a' - flowRate a == -r1 -r2 &&
     rtb b' t3 - rtb b t3 == rtb a t3 - rtb a' t3 &&
     -- ditto
-    r1 `mt_v_mul_t` (t2 - t1) + (r1 + r2) `mt_v_mul_t` (t3 - t2) == rtb b' t3 - rtb b t3
+    r1 `mt_fr_mul_t` (t2 - t1) + (r1 + r2) `mt_fr_mul_t` (t3 - t2) == rtb b' t3 - rtb b t3
     where (a', b') = flow2b r2 t2 (flow2b r1 t1 (a, b))
 
 -- NOTE: updp_flow2a is an invalid property due to right side biased error term adjustment.
@@ -156,11 +155,11 @@ uu_flow2b (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
 --           (a'', b'') = flow2a r2 t2 (flow2a r1 t1 (a', b'))
 
 updp_flow2b (a :: TestUniversalIndex) t1 r1 t2 r2 t3 =
-    flowRate b'' - flowRate b' == r1 + r2 && flowRate a'' - flowRate a' == -r1 -r2 &&
-    flowRate (b'', b1') == r1 + r2 &&
     rtb (b'', b1') t3 - rtb (b', b1') t3 == rtb a' t3 - rtb a'' t3 &&
-    -- ditto
-    r1 `mt_v_mul_t` (t2 - t1) + (r1 + r2) `mt_v_mul_t` (t3 - t2) == rtb (b'', b1') t3 - rtb (b', b1') t3
+    rtb (b'', b1') t3 - rtb (b', b1') t3 == r1 `mt_fr_mul_t` (t2 - t1) + (r1 + r2) `mt_fr_mul_t` (t3 - t2) &&
+    flowRate a'' - flowRate a' == -(r1 + r2) &&
+    flowRate b'' - flowRate b' == r1 + r2 &&
+    flowRate (b'', b1') == r1 + r2
     where (a', (b', b1')) = pdp_UpdateMember2 1 t1 (a, (mempty :: TestPDP_Index, def))
           (a'', b'') = flow2b r2 t2 (flow2b r1 t1 (a', b'))
 
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
index bea1b8e4a3..2846323f4d 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
@@ -12,20 +12,25 @@ import           Money.Theory.SemanticMoney
 
 newtype TestTime = TestTime Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestTime where
-    arbitrary = TestTime <$> arbitrary
+    arbitrary = TestTime <$> arbitrary -- choose (0, 2 ^ (32 :: Integer))
 
 newtype TestMValue = TestMValue Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestMValue where
-    arbitrary = TestMValue <$> arbitrary
+    arbitrary = TestMValue <$> arbitrary -- choose (0, 2 ^ (32 :: Integer))
+
+newtype TestMFlowRate = TestMFlowRate Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
+instance Arbitrary TestMFlowRate where
+    arbitrary = TestMFlowRate <$> arbitrary -- choose (0, 2 ^ (32 :: Integer))
 
 newtype TestMUnit = TestMUnit Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestMUnit where
-    arbitrary = TestMUnit <$> arbitrary
+    arbitrary = TestMUnit <$> arbitrary -- choose (0, 2 ^ (32 :: Integer))
 
 data TestMonetaryTypes
 instance MonetaryTypes TestMonetaryTypes where
     type MT_TIME  TestMonetaryTypes = TestTime
     type MT_VALUE TestMonetaryTypes = TestMValue
+    type MT_FLOWRATE TestMonetaryTypes = TestMFlowRate
     type MT_UNIT  TestMonetaryTypes = TestMUnit
 deriving instance Show (BasicParticle TestMonetaryTypes)
 

From 5015f46b7801cd2b387b886ae8ac2200a6dc9717 Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Thu, 12 Jun 2025 19:33:16 +0300
Subject: [PATCH 06/11] added NaiveTokenModel

---
 .../pkgs/semantic-money/semantic-money.cabal  |  1 +
 .../src/Money/Theory/MonetaryTypes.hs         |  5 +-
 .../src/Money/Theory/SemanticMoney.hs         |  2 +-
 .../src/Money/Theory/TokenModel.hs            | 49 +++++++++++++++++--
 4 files changed, 50 insertions(+), 7 deletions(-)

diff --git a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
index 989fee5c84..3b9ca9e0da 100644
--- a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
+++ b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
@@ -29,6 +29,7 @@ library
     -- other-extensions:
     build-depends:
         base >=4.16.0.0 && <5,
+        containers >= 0.8,
         data-default
 
 test-suite semantic-money-test-suite
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
index cafbae15ab..c41d0934b7 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
@@ -8,7 +8,7 @@ module Money.Theory.MonetaryTypes
       , mt_v_mul_u, mt_v_div_u, mt_v_mul_u_qr_u
       , mt_fr_mul_u, mt_fr_div_u, mt_fr_mul_u_qr_u
       )
-    , MonetaryTypes'tv, MonetaryTypes'tvr, MonetaryTypes'tvru
+    , MonetaryTypes'tv, MonetaryTypes'tr, MonetaryTypes'tvr, MonetaryTypes'tvru
     ) where
 -- base
 import           Data.Kind (Type)
@@ -73,5 +73,6 @@ class ( Eq (MT_TIME mt), Ord (MT_TIME mt), Num (MT_TIME mt)
     type family MT_UNIT  mt = (u :: Type) | u -> mt
 
 type MonetaryTypes'tv mt t v = (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt)
-type MonetaryTypes'tvr mt t v fr = (MonetaryTypes'tv mt t v, fr ~ MT_FLOWRATE mt)
+type MonetaryTypes'tr mt t fr = (MonetaryTypes mt, t ~ MT_TIME mt, fr ~ MT_FLOWRATE mt)
+type MonetaryTypes'tvr mt t v fr = (MonetaryTypes'tv mt t v, MonetaryTypes'tr mt t fr)
 type MonetaryTypes'tvru mt t v fr u = (MonetaryTypes'tvr mt t v fr, u ~ MT_UNIT mt)
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
index 878bbe0ec5..e80e71153e 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
@@ -3,7 +3,7 @@ module Money.Theory.SemanticMoney
     ( -- * Semantic Money Classes & Primitives
         MonetaryUnit (settle, settledAt, flowRate, rtb)
     , IndexedValue (shift1, flow1)
-    , shift2b, flow2a, flow2b, align2a, align2b
+    , shift2a, shift2b, flow2a, flow2b, align2a, align2b
       -- * Semantic Money Instances
     , BasicParticle (..)
     , PDP_Index (..), PDP_Member (..), PDP_MemberMU, pdp_UpdateMember2
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
index 70c10bd2ab..4b98bcda77 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
@@ -1,4 +1,7 @@
+{-# LANGUAGE LambdaCase #-}
 module Money.Theory.TokenModel where
+-- containers
+import qualified Data.IntMap                as IntMap
 --
 import           Money.Theory.SemanticMoney
 
@@ -7,8 +10,46 @@ data TokenEvent mt acc where
     TransferEvent :: forall mt acc {t} {v}.
         MonetaryTypes'tv mt t v =>
         t -> acc -> acc -> v -> TokenEvent mt acc
-    -- UpdateFlowEvent :: forall mt acc {t} {v} {u}.
-    --     MonetaryTypes'tvu mt t v u =>
-    --     t -> acc -> acc -> v -> TokenEvent mt acc
+    UpdateFlowEvent :: forall mt acc {t} {fr}.
+        MonetaryTypes'tr mt t fr =>
+        t -> acc -> acc -> fr -> TokenEvent mt acc
 
-data TokenModel mt acc
+type Account = Int
+
+------------------------------------------------------------------------------------------------------------------------
+-- NaiveTokenModel
+------------------------------------------------------------------------------------------------------------------------
+
+data NaiveTokenModel mt acc = MkNaiveTokenModel
+    { accounts :: IntMap.IntMap (BasicParticle mt) -- ^ accounts indexed by Int
+    , pools    :: IntMap.IntMap (PDP_Index mt (BasicParticle mt)) -- ^ pools indexed by Int
+    }
+
+naiveProcessOneEvent ::
+    MonetaryTypes mt =>
+    NaiveTokenModel mt Account ->
+    TokenEvent mt Account ->
+    NaiveTokenModel mt Account
+naiveProcessOneEvent (MkNaiveTokenModel accs pools) = \case
+    TransferEvent t from to amount -> go2 from to (shift2a amount t)
+    UpdateFlowEvent t from to rate -> go2 from to (flow2a rate t)
+    where go2 from to op =
+              let sender = IntMap.findWithDefault mempty from accs
+                  receiver = IntMap.findWithDefault mempty from accs
+                  (sender', receiver') = op (sender, receiver)
+                  accs' = IntMap.insert from sender'
+                          $ IntMap.insert to receiver'
+                          $ accs
+              in MkNaiveTokenModel accs' pools
+
+naiveProcessEvents ::
+    MonetaryTypes mt =>
+    [TokenEvent mt Account] ->
+    NaiveTokenModel mt Account
+naiveProcessEvents = foldl' naiveProcessOneEvent (MkNaiveTokenModel IntMap.empty IntMap.empty)
+
+naiveSystemSnapshot ::
+    MonetaryTypes'tv mt t v =>
+    NaiveTokenModel mt Account ->
+    IntMap.IntMap (t -> v)
+naiveSystemSnapshot = (rtb <$>) . accounts

From da80a60b52e0efebbc8c4d65d2ac7b6c761a1d10 Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Fri, 13 Jun 2025 17:08:47 +0300
Subject: [PATCH 07/11] refactor SemanticMoney module continues; sepraate
 NaiveTokenModel

---
 .../pkgs/semantic-money/semantic-money.cabal  |  1 +
 .../src/Money/Theory/SemanticMoney.hs         | 59 ++++++++++---------
 .../src/Money/Theory/TokenModel.hs            | 53 +++++------------
 .../Theory/TokenModel/NaiveTokenModel.hs      | 33 +++++++++++
 .../test/Money/Theory/SemanticMoney_prop.hs   |  4 +-
 .../test/Money/Theory/TestMonetaryTypes.hs    |  1 -
 6 files changed, 80 insertions(+), 71 deletions(-)
 create mode 100644 packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/NaiveTokenModel.hs

diff --git a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
index 3b9ca9e0da..8f38d6be22 100644
--- a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
+++ b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
@@ -25,6 +25,7 @@ library
         Money.Theory.MonetaryTypes
         Money.Theory.SemanticMoney
         Money.Theory.TokenModel
+        Money.Theory.TokenModel.NaiveTokenModel
     -- other-modules:
     -- other-extensions:
     build-depends:
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
index e80e71153e..31d85619b8 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
@@ -23,27 +23,27 @@ import           Money.Theory.MonetaryTypes
 -- General Payment Primitives
 ------------------------------------------------------------------------------------------------------------------------
 
--- | A monetary unit and its operators.
-class (MonetaryTypes'tvr mt t v fr, Eq mu) =>
-      MonetaryUnit mt t v fr mu | mu -> mt where
-    settle    :: t -> mu -> mu
-    settledAt :: mu -> t
-    flowRate  :: mu -> fr
-    rtb       :: mu -> t -> v
-
--- | An indexed monetary value and its 1-primitive operators.
-class (MonetaryUnit mt t v fr iv, u ~ MT_UNIT mt, Monoid iv, Eq iv) =>
-      IndexedValue mt t v fr u iv | iv -> mt where
-    shift1 :: v -> iv -> (iv, v)
-    flow1  :: fr -> iv -> (iv, fr)
+-- | A monetary unit and its operators (0-primitives).
+class (MonetaryTypes mt, Eq mu) =>
+      MonetaryUnit mt mu | mu -> mt where
+    settle    :: t ~ MT_TIME mt => t -> mu -> mu
+    settledAt :: t ~ MT_TIME mt => mu -> t
+    flowRate  :: fr ~ MT_FLOWRATE mt => mu -> fr
+    rtb       :: MonetaryTypes'tvr mt t v fr => mu -> t -> v
+
+-- | An indexed monetary value and its operators (1-primitives).
+class (MonetaryUnit mt iv, Monoid iv, Eq iv) =>
+      IndexedValue mt iv | iv -> mt where
+    shift1 :: v ~ MT_VALUE mt => v -> iv -> (iv, v)
+    flow1  :: fr ~ MT_FLOWRATE mt => fr -> iv -> (iv, fr)
 
 --
--- polymorphic 2-primitives for indexed values
+-- polymorphic 2-primitives for indexed values.
 --
 
 -- | Shift value for the left side (a) or right side (b).
 shift2a, shift2b ::
-    (IndexedValue mt t v fr u a, IndexedValue mt t v fr u b) =>
+    (MonetaryTypes'tv mt t v, IndexedValue mt a, IndexedValue mt b) =>
     v -> t -> (a, b) -> (a, b)
 shift2a v t (a, b) =
     let (a', v') = shift1 v (settle t a)
@@ -54,7 +54,7 @@ shift2b v t (a, b) = swap (shift2a (-v) t (b, a))
 
 -- | Shifting flow for the left side (a) or right side (b).
 flow2a, flow2b ::
-    (IndexedValue mt t v fr u a, IndexedValue mt t v fr u b) =>
+    (MonetaryTypes'tr mt t fr, IndexedValue mt a, IndexedValue mt b) =>
     fr -> t -> (a, b) -> (a, b)
 flow2a dfr t (a, b) =
     let (b1, fr_a) = flow1 (flowRate a) (settle t mempty)
@@ -69,7 +69,7 @@ flow2b dfr t (a, b) = swap (flow2a (-dfr) t (b, a))
 --   1) Left side produces error term with which right side is adjusted accordingly, and vice versa.
 --   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
 align2a, align2b ::
-    (IndexedValue mt t v fr u a, IndexedValue mt t v fr u b) =>
+    (IndexedValue mt a, IndexedValue mt b) =>
     MT_UNIT mt -> MT_UNIT mt -> (a, b) -> (a, b)
 align2a u u' (a, b) = (a', b')
     where fr = flowRate a
@@ -101,8 +101,8 @@ instance MonetaryTypes mt => Semigroup (BasicParticle mt) where
 instance MonetaryTypes mt => Monoid (BasicParticle mt) where
     mempty = BasicParticle 0 0 0
 
-instance MonetaryTypes'tvr mt t v fr =>
-         MonetaryUnit mt t v fr (BasicParticle mt) where
+instance MonetaryTypes mt =>
+         MonetaryUnit mt (BasicParticle mt) where
     settle t' a = a { bp_settled_at = t'
                     , bp_settled_value = rtb a t'
                     }
@@ -110,8 +110,8 @@ instance MonetaryTypes'tvr mt t v fr =>
     flowRate = bp_flow_rate
     rtb (BasicParticle t s r) t' = r `mt_fr_mul_t` (t' - t) + s
 
-instance MonetaryTypes'tvru mt t v fr u =>
-         IndexedValue mt t v fr u (BasicParticle mt) where
+instance MonetaryTypes mt =>
+         IndexedValue mt (BasicParticle mt) where
     shift1 x a = (a { bp_settled_value = bp_settled_value a + x }, x)
     flow1 r' a = (a { bp_flow_rate = r' }, r')
 
@@ -133,8 +133,9 @@ data PDP_Member mt wp = PDP_Member
 type PDP_MemberMU mt wp = (PDP_Index mt wp, PDP_Member mt wp)
 
 pdp_UpdateMember2 ::
-    ( IndexedValue mt t v fr u a
-    , IndexedValue mt t v fr u wp
+    ( u ~ MT_UNIT mt, t ~ MT_TIME mt
+    , IndexedValue mt a
+    , IndexedValue mt wp
     , mu ~ PDP_MemberMU mt wp
     ) =>
     u -> t -> (a, mu) -> (a, mu)
@@ -160,15 +161,15 @@ instance (MonetaryTypes mt, Semigroup wp) => Semigroup (PDP_Index mt wp) where
 instance (MonetaryTypes mt, Monoid wp) => Monoid (PDP_Index mt wp) where
     mempty = PDP_Index 0 mempty
 
-instance MonetaryUnit mt t v fr wp =>
-         MonetaryUnit mt t v fr (PDP_Index mt wp) where
+instance MonetaryUnit mt wp =>
+         MonetaryUnit mt (PDP_Index mt wp) where
     settle t' a@(PDP_Index _ mpi) = a { pdpi_wp = settle t' mpi }
     settledAt (PDP_Index _ mpi) = settledAt mpi
     flowRate (PDP_Index _ mpi) = flowRate mpi
     rtb (PDP_Index _ mpi) = rtb mpi
 
-instance IndexedValue mt t v fr u wp =>
-         IndexedValue mt t v fr u (PDP_Index mt wp) where
+instance IndexedValue mt wp =>
+         IndexedValue mt (PDP_Index mt wp) where
     shift1 x a@(PDP_Index tu mpi) = (a { pdpi_wp = mpi' }, x' `mt_v_mul_u` tu)
         where (mpi', x') = if tu == 0 then (mpi, 0) else shift1 (x `mt_v_div_u` tu) mpi
 
@@ -189,8 +190,8 @@ deriving instance (MonetaryTypes mt, Eq wp) => Eq (PDP_Member mt wp)
 -- PDP_MemberMU as MonetaryUnit
 --
 
-instance MonetaryUnit mt t v fr wp =>
-         MonetaryUnit mt t v fr (PDP_MemberMU mt wp) where
+instance MonetaryUnit mt wp =>
+         MonetaryUnit mt (PDP_MemberMU mt wp) where
     settle t' (pix, pm) = (pix', pm')
         where sv' = rtb (pix, pm) t'
               pix'@(PDP_Index _ mpi') = settle t' pix
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
index 4b98bcda77..62117499f7 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs
@@ -1,7 +1,8 @@
-{-# LANGUAGE LambdaCase #-}
-module Money.Theory.TokenModel where
--- containers
-import qualified Data.IntMap                as IntMap
+{-# LANGUAGE FunctionalDependencies #-}
+module Money.Theory.TokenModel
+    ( TokenEvent (..)
+    , TokenModel (initToken, tokenAccounts, processOneTokenEvent, processTokenEvents, isTokenSolvent)
+    ) where
 --
 import           Money.Theory.SemanticMoney
 
@@ -14,42 +15,16 @@ data TokenEvent mt acc where
         MonetaryTypes'tr mt t fr =>
         t -> acc -> acc -> fr -> TokenEvent mt acc
 
-type Account = Int
+class MonetaryUnit mt mu =>
+      TokenModel mt mu acc token | token -> mu acc where
+    initToken :: token
 
-------------------------------------------------------------------------------------------------------------------------
--- NaiveTokenModel
-------------------------------------------------------------------------------------------------------------------------
+    tokenAccounts :: token -> [mu]
 
-data NaiveTokenModel mt acc = MkNaiveTokenModel
-    { accounts :: IntMap.IntMap (BasicParticle mt) -- ^ accounts indexed by Int
-    , pools    :: IntMap.IntMap (PDP_Index mt (BasicParticle mt)) -- ^ pools indexed by Int
-    }
+    processOneTokenEvent :: token -> TokenEvent mt acc -> token
 
-naiveProcessOneEvent ::
-    MonetaryTypes mt =>
-    NaiveTokenModel mt Account ->
-    TokenEvent mt Account ->
-    NaiveTokenModel mt Account
-naiveProcessOneEvent (MkNaiveTokenModel accs pools) = \case
-    TransferEvent t from to amount -> go2 from to (shift2a amount t)
-    UpdateFlowEvent t from to rate -> go2 from to (flow2a rate t)
-    where go2 from to op =
-              let sender = IntMap.findWithDefault mempty from accs
-                  receiver = IntMap.findWithDefault mempty from accs
-                  (sender', receiver') = op (sender, receiver)
-                  accs' = IntMap.insert from sender'
-                          $ IntMap.insert to receiver'
-                          $ accs
-              in MkNaiveTokenModel accs' pools
+    processTokenEvents :: token -> [TokenEvent mt acc] -> token
+    processTokenEvents = foldl' processOneTokenEvent
 
-naiveProcessEvents ::
-    MonetaryTypes mt =>
-    [TokenEvent mt Account] ->
-    NaiveTokenModel mt Account
-naiveProcessEvents = foldl' naiveProcessOneEvent (MkNaiveTokenModel IntMap.empty IntMap.empty)
-
-naiveSystemSnapshot ::
-    MonetaryTypes'tv mt t v =>
-    NaiveTokenModel mt Account ->
-    IntMap.IntMap (t -> v)
-naiveSystemSnapshot = (rtb <$>) . accounts
+    isTokenSolvent :: token -> Bool
+    isTokenSolvent = (== 0) . length . (rtb <$>) . tokenAccounts
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/NaiveTokenModel.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/NaiveTokenModel.hs
new file mode 100644
index 0000000000..9f76c6ee61
--- /dev/null
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/NaiveTokenModel.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE LambdaCase #-}
+module Money.Theory.TokenModel.NaiveTokenModel where
+-- containers
+import qualified Data.IntMap.Lazy           as IntMap
+--
+import           Money.Theory.SemanticMoney
+import           Money.Theory.TokenModel
+
+
+type Account = Int
+
+data NaiveTokenModel mt = MkNaiveTokenModel
+    { accounts :: IntMap.IntMap (BasicParticle mt) -- ^ accounts indexed by Int
+    , pools    :: IntMap.IntMap (PDP_Index mt (BasicParticle mt)) -- ^ pools indexed by Int
+    }
+
+instance MonetaryTypes mt =>
+         TokenModel mt (BasicParticle mt) Account (NaiveTokenModel mt) where
+    initToken = MkNaiveTokenModel IntMap.empty IntMap.empty
+
+    tokenAccounts = (snd <$>) . IntMap.toList . accounts
+
+    processOneTokenEvent (MkNaiveTokenModel accs pools) = \case
+        TransferEvent t from to amount -> go2 from to (shift2a amount t)
+        UpdateFlowEvent t from to rate -> go2 from to (flow2a rate t)
+        where go2 from to op =
+                  let sender = IntMap.findWithDefault mempty from accs
+                      receiver = IntMap.findWithDefault mempty from accs
+                      (sender', receiver') = op (sender, receiver)
+                      accs' = IntMap.insert from sender'
+                              $ IntMap.insert to receiver'
+                              $ accs
+                  in MkNaiveTokenModel accs' pools
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
index b6919fc20f..3007ee76cf 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
@@ -16,12 +16,12 @@ import           Money.Theory.TestMonetaryTypes
 -- Monetary Units Laws: settle-idempotency, constant-rtb
 --------------------------------------------------------------------------------
 
-mu_settle_idempotency :: MonetaryUnit mt t v fr mu => mu -> t -> Bool
+mu_settle_idempotency :: (MonetaryUnit mt mu, t ~ MT_TIME mt) => mu -> t -> Bool
 mu_settle_idempotency a t =
     settledAt (settle t a) == t &&
     settle t a == settle t (settle t a)
 
-mu_constant_rtb :: MonetaryUnit mt t v fr mu => mu -> t -> t -> t -> Bool
+mu_constant_rtb :: (MonetaryUnit mt mu, t ~ MT_TIME mt) => mu -> t -> t -> t -> Bool
 mu_constant_rtb a t1 t2 t3 =
     rtb (settle t1 a) t3 == rtb a t3 &&
     rtb (settle t2 a) t3 == rtb a t3 &&
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
index 2846323f4d..f716673571 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE TypeFamilies #-}
-
 module Money.Theory.TestMonetaryTypes where
 -- quickcheck
 import           Test.QuickCheck

From ac9208c33a54713a329b654c9dd3c26ba8da5cd7 Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Mon, 16 Jun 2025 14:32:35 +0300
Subject: [PATCH 08/11] TwoPhaseParticle

---
 .../pkgs/semantic-money/semantic-money.cabal  |  1 +
 .../src/Money/Theory/SemanticMoney.hs         | 24 ++++++-------
 .../Theory/TokenModel/TwoPhaseTokenModel.hs   | 35 +++++++++++++++++++
 .../test/Money/Theory/SemanticMoney_prop.hs   | 10 +++---
 .../test/Money/Theory/TestMonetaryTypes.hs    |  2 +-
 5 files changed, 54 insertions(+), 18 deletions(-)
 create mode 100644 packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/TwoPhaseTokenModel.hs

diff --git a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
index 8f38d6be22..7a275becd5 100644
--- a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
+++ b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal
@@ -26,6 +26,7 @@ library
         Money.Theory.SemanticMoney
         Money.Theory.TokenModel
         Money.Theory.TokenModel.NaiveTokenModel
+        Money.Theory.TokenModel.TwoPhaseTokenModel
     -- other-modules:
     -- other-extensions:
     build-depends:
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
index 31d85619b8..f4805a232a 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
@@ -28,11 +28,11 @@ class (MonetaryTypes mt, Eq mu) =>
       MonetaryUnit mt mu | mu -> mt where
     settle    :: t ~ MT_TIME mt => t -> mu -> mu
     settledAt :: t ~ MT_TIME mt => mu -> t
-    flowRate  :: fr ~ MT_FLOWRATE mt => mu -> fr
+    flowRate  :: MonetaryTypes'tr mt t fr => mu -> t -> fr
     rtb       :: MonetaryTypes'tvr mt t v fr => mu -> t -> v
 
 -- | An indexed monetary value and its operators (1-primitives).
-class (MonetaryUnit mt iv, Monoid iv, Eq iv) =>
+class (MonetaryUnit mt iv, Monoid iv) =>
       IndexedValue mt iv | iv -> mt where
     shift1 :: v ~ MT_VALUE mt => v -> iv -> (iv, v)
     flow1  :: fr ~ MT_FLOWRATE mt => fr -> iv -> (iv, fr)
@@ -57,7 +57,7 @@ flow2a, flow2b ::
     (MonetaryTypes'tr mt t fr, IndexedValue mt a, IndexedValue mt b) =>
     fr -> t -> (a, b) -> (a, b)
 flow2a dfr t (a, b) =
-    let (b1, fr_a) = flow1 (flowRate a) (settle t mempty)
+    let (b1, fr_a) = flow1 (flowRate a t) (settle t mempty)
         (b2, fr_a') = flow1 (-fr_a + dfr) (settle t mempty)
         (a', fr_a'') = flow1 (-fr_a') (settle t a)
     in assert (fr_a' == -fr_a'') (a', b <> b1 <> b2)
@@ -70,13 +70,13 @@ flow2b dfr t (a, b) = swap (flow2a (-dfr) t (b, a))
 --   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
 align2a, align2b ::
     (IndexedValue mt a, IndexedValue mt b) =>
-    MT_UNIT mt -> MT_UNIT mt -> (a, b) -> (a, b)
-align2a u u' (a, b) = (a', b')
-    where fr = flowRate a
+    MT_UNIT mt -> MT_UNIT mt -> MT_TIME mt -> (a, b) -> (a, b)
+align2a u u' t (a, b) = (a', b')
+    where fr = flowRate a t
           (fr', e) = if u' == 0 then (0, fr `mt_fr_mul_u` u) else fr `mt_fr_mul_u_qr_u` (u, u')
           a' = fst (flow1 fr' a)
-          b' = fst (flow1 (e + flowRate b) b)
-align2b u u' (a, b) = swap (align2a u u' (b, a))
+          b' = fst (flow1 (e + flowRate b t) b)
+align2b u u' t (a, b) = swap (align2a u u' t (b, a))
 
 ------------------------------------------------------------------------------------------------------------------------
 -- Basic Particle: building block for indexes
@@ -94,7 +94,7 @@ instance MonetaryTypes mt => Semigroup (BasicParticle mt) where
     a@(BasicParticle t1 _ _) <> b@(BasicParticle t2 _ _) = BasicParticle t' (sv1 + sv2) (r1 + r2)
         -- The binary operator supports negative time values while abiding the monoidal laws.
         -- The practical semantics of values of mixed-sign is not of the concern of this specification.
-        where t' | t1 == 0 = t2 | t2 == 0 = t1 | otherwise = max t1 t2
+        where t' = max t1 t2
               (BasicParticle _ sv1 r1) = settle t' a
               (BasicParticle _ sv2 r2) = settle t' b
 
@@ -107,7 +107,7 @@ instance MonetaryTypes mt =>
                     , bp_settled_value = rtb a t'
                     }
     settledAt = bp_settled_at
-    flowRate = bp_flow_rate
+    flowRate = const . bp_flow_rate
     rtb (BasicParticle t s r) t' = r `mt_fr_mul_t` (t' - t) + s
 
 instance MonetaryTypes mt =>
@@ -142,7 +142,7 @@ pdp_UpdateMember2 ::
 pdp_UpdateMember2 u' t' (a, (b, pm)) = (a'', (b'', pm''))
     where (PDP_Index tu mpi, pm'@(PDP_Member u _ _)) = settle t' (b, pm)
           tu' = tu + u' - u
-          (mpi', a'') = align2b tu tu' (mpi, settle t' a)
+          (mpi', a'') = align2b tu tu' t' (mpi, settle t' a)
           b''  = PDP_Index tu' mpi'
           pm'' = pm' { pdpm_owned_unit = u', pdpm_synced_wp = mpi' }
 
@@ -199,7 +199,7 @@ instance MonetaryUnit mt wp =>
 
     settledAt (_, PDP_Member _ _ mps) = settledAt mps
 
-    flowRate (PDP_Index _ mpi, PDP_Member u _ _) = flowRate mpi `mt_fr_mul_u` u
+    flowRate (PDP_Index _ mpi, PDP_Member u _ _) t = flowRate mpi t `mt_fr_mul_u` u
 
     rtb (PDP_Index _ mpi, PDP_Member u sv mps) t' = sv +
         -- let ti = bp_settled_at mpi
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/TwoPhaseTokenModel.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/TwoPhaseTokenModel.hs
new file mode 100644
index 0000000000..42f86962ba
--- /dev/null
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/TwoPhaseTokenModel.hs
@@ -0,0 +1,35 @@
+module Money.Theory.TokenModel.TwoPhaseTokenModel where
+-- containers
+import qualified Data.IntMap.Lazy           as IntMap
+--
+import           Money.Theory.SemanticMoney
+import           Money.Theory.TokenModel
+
+
+data TwoPhaseParticle mt = MkTwoPhaseParticle
+    { confirmedParticle :: BasicParticle mt
+    , pendingParticle   :: BasicParticle mt
+    }
+    deriving Eq
+
+instance MonetaryTypes mt => MonetaryUnit mt (TwoPhaseParticle mt) where
+    settle t (MkTwoPhaseParticle p_c p_p) = MkTwoPhaseParticle p_c (settle t p_p)
+    settledAt = settledAt . pendingParticle
+    flowRate mu t =
+        flowRate (confirmedParticle mu) t +
+        if t > settledAt (confirmedParticle mu) then flowRate (pendingParticle mu) t else 0
+    rtb mu t =
+        rtb (confirmedParticle mu) t +
+        if t > settledAt (confirmedParticle mu) then rtb (pendingParticle mu) t else 0
+
+type Account = Int
+
+data TwoPhaseTokenModel mt = MkTwoPhaseTokenModel
+    { accounts :: IntMap.IntMap (TwoPhaseParticle mt) -- ^ accounts indexed by Int
+    , pools    :: IntMap.IntMap (PDP_Index mt (TwoPhaseParticle mt)) -- ^ pools indexed by Int
+    }
+
+instance MonetaryTypes mt => TokenModel mt (TwoPhaseParticle mt) Account (TwoPhaseTokenModel mt) where
+    -- initToken
+    -- tokenAccounts
+    -- processOneTokenEvent
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
index 3007ee76cf..d150294e7d 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
@@ -132,14 +132,14 @@ one2n_pd_tests = describe "1toN proportional distribution 2-primitives" $ do
 --------------------------------------------------------------------------------
 
 uu_flow2a (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
-    flowRate b' - flowRate b == r1 + r2 && flowRate a' - flowRate a == -r1 -r2 &&
+    flowRate b' t3 - flowRate b t3 == r1 + r2 && flowRate a' t3 - flowRate a t3 == -r1 -r2 &&
     rtb b' t3 - rtb b t3 == rtb a t3 - rtb a' t3 &&
     -- for shift flow semantics: rtb b' t3 - (rtb b t3 - rtb b t1) - rtb b t1 == rtb b' t3 - rtb b t3
     r1 `mt_fr_mul_t` (t2 - t1) + (r1 + r2) `mt_fr_mul_t` (t3 - t2) == rtb b' t3 - rtb b t3
     where (a', b') = flow2a r2 t2 (flow2a r1 t1 (a, b))
 
 uu_flow2b (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
-    flowRate b' - flowRate b == r1 + r2 && flowRate a' - flowRate a == -r1 -r2 &&
+    flowRate b' t3 - flowRate b t3 == r1 + r2 && flowRate a' t3 - flowRate a t3 == -r1 -r2 &&
     rtb b' t3 - rtb b t3 == rtb a t3 - rtb a' t3 &&
     -- ditto
     r1 `mt_fr_mul_t` (t2 - t1) + (r1 + r2) `mt_fr_mul_t` (t3 - t2) == rtb b' t3 - rtb b t3
@@ -157,9 +157,9 @@ uu_flow2b (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
 updp_flow2b (a :: TestUniversalIndex) t1 r1 t2 r2 t3 =
     rtb (b'', b1') t3 - rtb (b', b1') t3 == rtb a' t3 - rtb a'' t3 &&
     rtb (b'', b1') t3 - rtb (b', b1') t3 == r1 `mt_fr_mul_t` (t2 - t1) + (r1 + r2) `mt_fr_mul_t` (t3 - t2) &&
-    flowRate a'' - flowRate a' == -(r1 + r2) &&
-    flowRate b'' - flowRate b' == r1 + r2 &&
-    flowRate (b'', b1') == r1 + r2
+    flowRate a'' t3 - flowRate a' t3 == -(r1 + r2) &&
+    flowRate b'' t3 - flowRate b' t3 == r1 + r2 &&
+    flowRate (b'', b1') t3 == r1 + r2
     where (a', (b', b1')) = pdp_UpdateMember2 1 t1 (a, (mempty :: TestPDP_Index, def))
           (a'', b'') = flow2b r2 t2 (flow2b r1 t1 (a', b'))
 
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
index f716673571..809b62548b 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
@@ -11,7 +11,7 @@ import           Money.Theory.SemanticMoney
 
 newtype TestTime = TestTime Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestTime where
-    arbitrary = TestTime <$> arbitrary -- choose (0, 2 ^ (32 :: Integer))
+    arbitrary = TestTime <$> choose (0, 2 ^ (32 :: Integer))
 
 newtype TestMValue = TestMValue Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestMValue where

From 33aefb558dd7b4a4192366c6dccfcdf11caff21a Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Thu, 3 Jul 2025 18:28:00 +0300
Subject: [PATCH 09/11] WIP: rename to MonetaryParticle and its laws

---
 .../diagrams/semantic-money.drawio            | 478 ++++++++++++++++++
 .../src/Money/Theory/MonetaryTypes.hs         |  16 +-
 .../src/Money/Theory/SemanticMoney.hs         |  95 +++-
 .../test/Money/Theory/SemanticMoney_prop.hs   |  67 ++-
 .../test/Money/Theory/TestMonetaryTypes.hs    |  24 +-
 5 files changed, 596 insertions(+), 84 deletions(-)
 create mode 100644 packages/spec-haskell/diagrams/semantic-money.drawio

diff --git a/packages/spec-haskell/diagrams/semantic-money.drawio b/packages/spec-haskell/diagrams/semantic-money.drawio
new file mode 100644
index 0000000000..6f2785585d
--- /dev/null
+++ b/packages/spec-haskell/diagrams/semantic-money.drawio
@@ -0,0 +1,478 @@
+<mxfile host="Electron" agent="Mozilla/5.0 (X11; Linux x86_64) AppleWebKit/537.36 (KHTML, like Gecko) draw.io/26.1.1 Chrome/134.0.6998.205 Electron/35.3.0 Safari/537.36" version="26.1.1" pages="4">
+  <diagram id="H8HOQLwfiVH_24s6MfBu" name="Monetary Particles">
+    <mxGraphModel dx="925" dy="740" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="1169" pageHeight="827" math="0" shadow="0">
+      <root>
+        <mxCell id="0" />
+        <mxCell id="1" parent="0" />
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-2" value="money flow: A -&amp;gt; B" style="edgeStyle=orthogonalEdgeStyle;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;orthogonalLoop=1;jettySize=auto;html=1;entryX=0;entryY=0.5;entryDx=0;entryDy=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" edge="1" parent="1" source="6wfqHezWVOzMsqbXbEDX-1" target="VceYx_KpcEU2AsOnJ9CC-1">
+          <mxGeometry x="-0.0769" y="10" relative="1" as="geometry">
+            <mxPoint as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-6" value="shift value" style="edgeStyle=orthogonalEdgeStyle;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;orthogonalLoop=1;jettySize=auto;html=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;dashed=1;exitX=0.5;exitY=0;exitDx=0;exitDy=0;" edge="1" parent="1" source="VceYx_KpcEU2AsOnJ9CC-5" target="6wfqHezWVOzMsqbXbEDX-1">
+          <mxGeometry relative="1" as="geometry" />
+        </mxCell>
+        <mxCell id="6wfqHezWVOzMsqbXbEDX-1" value="Monetary Particle&lt;div&gt;A&lt;/div&gt;" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" vertex="1" parent="1">
+          <mxGeometry x="160" y="120" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-4" value="money flow: B -&amp;gt; C" style="edgeStyle=orthogonalEdgeStyle;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;orthogonalLoop=1;jettySize=auto;html=1;entryX=0;entryY=0.5;entryDx=0;entryDy=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" edge="1" parent="1" source="VceYx_KpcEU2AsOnJ9CC-1" target="VceYx_KpcEU2AsOnJ9CC-3">
+          <mxGeometry y="10" relative="1" as="geometry">
+            <mxPoint as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-1" value="Monetary Particle&lt;div&gt;B&lt;/div&gt;" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" vertex="1" parent="1">
+          <mxGeometry x="400" y="120" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-3" value="Monetary Particle&lt;div&gt;C&lt;/div&gt;" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" vertex="1" parent="1">
+          <mxGeometry x="640" y="120" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-5" value="Monetary Particle&lt;div&gt;D&lt;/div&gt;" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" vertex="1" parent="1">
+          <mxGeometry x="160" y="320" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-7" value="" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;exitX=1;exitY=0.5;exitDx=0;exitDy=0;" edge="1" parent="1" source="VceYx_KpcEU2AsOnJ9CC-9">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="530" y="230" as="sourcePoint" />
+            <mxPoint x="580" y="180" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-8" value="" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;exitX=0;exitY=0.5;exitDx=0;exitDy=0;" edge="1" parent="1" source="VceYx_KpcEU2AsOnJ9CC-9">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="370" y="230" as="sourcePoint" />
+            <mxPoint x="340" y="180" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-9" value="Composable flows" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" vertex="1" parent="1">
+          <mxGeometry x="400" y="220" width="120" height="20" as="geometry" />
+        </mxCell>
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-10" value="Traditional &quot;transfer&quot;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" vertex="1" parent="1">
+          <mxGeometry x="400" y="340" width="160" height="20" as="geometry" />
+        </mxCell>
+        <mxCell id="VceYx_KpcEU2AsOnJ9CC-11" value="" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;exitX=0;exitY=0.5;exitDx=0;exitDy=0;" edge="1" parent="1" source="VceYx_KpcEU2AsOnJ9CC-10">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="390" y="350" as="sourcePoint" />
+            <mxPoint x="260" y="260" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="pC6EmT1mO1-7I_UVn7CZ-1" value="Monetary Particles" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=24;fontStyle=1" vertex="1" parent="1">
+          <mxGeometry x="280" y="40" width="400" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="pC6EmT1mO1-7I_UVn7CZ-3" value="Account" style="html=1;verticalLabelPosition=bottom;align=center;labelBackgroundColor=#ffffff;verticalAlign=top;strokeWidth=2;strokeColor=#0080F0;shadow=0;dashed=0;shape=mxgraph.ios7.icons.wallet;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" vertex="1" parent="1">
+          <mxGeometry x="160" y="480" width="290" height="160" as="geometry" />
+        </mxCell>
+        <mxCell id="pC6EmT1mO1-7I_UVn7CZ-4" value="Monetary Particle C" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=10;" vertex="1" parent="1">
+          <mxGeometry x="180" y="560" width="70" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="pC6EmT1mO1-7I_UVn7CZ-5" value="Monetary Particle&amp;nbsp;&lt;span style=&quot;background-color: transparent; color: light-dark(rgb(0, 0, 0), rgb(255, 255, 255));&quot;&gt;A&lt;/span&gt;" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=10;" vertex="1" parent="1">
+          <mxGeometry x="180" y="520" width="70" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="pC6EmT1mO1-7I_UVn7CZ-6" value="Monetary Particle B" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=10;" vertex="1" parent="1">
+          <mxGeometry x="260" y="520" width="70" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="pC6EmT1mO1-7I_UVn7CZ-7" value="Real-time Balance&lt;div&gt;$100&lt;/div&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontStyle=0" vertex="1" parent="1">
+          <mxGeometry x="340" y="500" width="110" height="60" as="geometry" />
+        </mxCell>
+      </root>
+    </mxGraphModel>
+  </diagram>
+  <diagram id="0rCbPjwfmgLRCS_IVyrk" name="PDP">
+    <mxGraphModel dx="1282" dy="1110" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="1169" pageHeight="827" math="0" shadow="0">
+      <root>
+        <mxCell id="0" />
+        <mxCell id="1" parent="0" />
+        <mxCell id="HKeCEY93-fwBorTPO6O0-1" value="Pool Index" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;verticalAlign=top;fontSize=16;fontStyle=1" vertex="1" parent="1">
+          <mxGeometry x="280" y="160" width="200" height="160" as="geometry" />
+        </mxCell>
+        <mxCell id="HKeCEY93-fwBorTPO6O0-4" value="Pool Member A" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;verticalAlign=top;fontSize=16;fontStyle=1" vertex="1" parent="1">
+          <mxGeometry x="800" y="160" width="280" height="160" as="geometry" />
+        </mxCell>
+        <mxCell id="HKeCEY93-fwBorTPO6O0-8" value="sync" style="edgeStyle=orthogonalEdgeStyle;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;orthogonalLoop=1;jettySize=auto;html=1;exitX=0.5;exitY=1;exitDx=0;exitDy=0;entryX=0.5;entryY=1;entryDx=0;entryDy=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=12;dashed=1;" edge="1" parent="1" source="HKeCEY93-fwBorTPO6O0-2" target="HKeCEY93-fwBorTPO6O0-5">
+          <mxGeometry relative="1" as="geometry">
+            <Array as="points">
+              <mxPoint x="340" y="340" />
+              <mxPoint x="860" y="340" />
+            </Array>
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="HKeCEY93-fwBorTPO6O0-2" value="Wrapped&lt;br&gt;Particle" style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#d5e8d4;strokeColor=#82b366;" vertex="1" parent="1">
+          <mxGeometry x="300" y="200" width="80" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="HKeCEY93-fwBorTPO6O0-3" value="Total Units" style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" vertex="1" parent="1">
+          <mxGeometry x="385" y="200" width="80" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="HKeCEY93-fwBorTPO6O0-5" value="Synced Particle" style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#d5e8d4;strokeColor=#82b366;" vertex="1" parent="1">
+          <mxGeometry x="820" y="200" width="80" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="HKeCEY93-fwBorTPO6O0-6" value="Settled&lt;br&gt;Value" style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" vertex="1" parent="1">
+          <mxGeometry x="980" y="200" width="80" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="HKeCEY93-fwBorTPO6O0-7" value="Owned Units" style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" vertex="1" parent="1">
+          <mxGeometry x="900" y="200" width="80" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="HKeCEY93-fwBorTPO6O0-9" value="Pool Member B" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;verticalAlign=top;fontSize=16;fontStyle=1" vertex="1" parent="1">
+          <mxGeometry x="800" y="360" width="200" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="HKeCEY93-fwBorTPO6O0-10" value="Pool Member C" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;verticalAlign=top;fontSize=16;fontStyle=1" vertex="1" parent="1">
+          <mxGeometry x="840" y="400" width="200" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="HKeCEY93-fwBorTPO6O0-11" value="Pool Members ..." style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;verticalAlign=middle;fontSize=16;fontStyle=1" vertex="1" parent="1">
+          <mxGeometry x="880" y="440" width="200" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="TdF20CzyUirmw_IOGbW3-1" value="Proportional Distribution Pool" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=24;fontStyle=1" vertex="1" parent="1">
+          <mxGeometry x="360" y="40" width="400" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="TdF20CzyUirmw_IOGbW3-3" value="shift value (One-to-N distribute)" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=12;" edge="1" parent="1">
+          <mxGeometry y="20" width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="500" y="200" as="sourcePoint" />
+            <mxPoint x="780" y="200" as="targetPoint" />
+            <mxPoint as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="TdF20CzyUirmw_IOGbW3-5" value="money flow (One-to-N distribute flow)" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=12;" edge="1" parent="1">
+          <mxGeometry y="20" width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="500" y="280" as="sourcePoint" />
+            <mxPoint x="780" y="280" as="targetPoint" />
+            <mxPoint as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="AtXUpiw5PIPHphmbWL_G-1" value="shift value" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=12;" edge="1" parent="1">
+          <mxGeometry y="20" width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="80" y="199" as="sourcePoint" />
+            <mxPoint x="260" y="199" as="targetPoint" />
+            <mxPoint as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="AtXUpiw5PIPHphmbWL_G-2" value="money flow" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=12;" edge="1" parent="1">
+          <mxGeometry y="20" width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="80" y="280" as="sourcePoint" />
+            <mxPoint x="260" y="280" as="targetPoint" />
+            <mxPoint as="offset" />
+          </mxGeometry>
+        </mxCell>
+      </root>
+    </mxGraphModel>
+  </diagram>
+  <diagram id="fZaOFZF0WYeOhrvYBxzz" name="Solvency-Phase Synchronization">
+    <mxGraphModel dx="1336" dy="952" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="1169" pageHeight="827" math="0" shadow="0">
+      <root>
+        <mxCell id="0" />
+        <mxCell id="1" parent="0" />
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-1" value="solvency-confirmed time" style="endArrow=none;dashed=1;html=1;dashPattern=1 3;strokeWidth=2;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=12;" parent="1" edge="1">
+          <mxGeometry x="1" y="20" width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="500" y="260" as="sourcePoint" />
+            <mxPoint x="500" y="160" as="targetPoint" />
+            <mxPoint x="20" y="-20" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-2" value="Confirmed" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#d5e8d4;strokeColor=#82b366;" parent="1" vertex="1">
+          <mxGeometry x="240" y="160" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-6" style="edgeStyle=orthogonalEdgeStyle;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;orthogonalLoop=1;jettySize=auto;html=1;entryX=0;entryY=0.5;entryDx=0;entryDy=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" source="Nm9Qbvf9_YvpDp5B0Lr9-3" target="Nm9Qbvf9_YvpDp5B0Lr9-5" edge="1">
+          <mxGeometry relative="1" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-3" value="Pending" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;dashed=1;fillColor=#f8cecc;strokeColor=#b85450;opacity=60;" parent="1" vertex="1">
+          <mxGeometry x="600" y="160" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-5" value="Pending" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="760" y="160" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-10" value="Solvency Confirmed Phase" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontStyle=2;fillColor=#d5e8d4;strokeColor=#82b366;" parent="1" vertex="1">
+          <mxGeometry x="200" y="120" width="200" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-11" value="Solvency-Phase Synchronization" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=24;fontStyle=1" parent="1" vertex="1">
+          <mxGeometry x="400" y="20" width="400" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-12" value="Solvency Unconfirmed Phase" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontStyle=2;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="600" y="120" width="280" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-14" value="1." style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=20;" parent="1" vertex="1">
+          <mxGeometry x="40" y="80" width="40" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-15" value="2." style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=20;" parent="1" vertex="1">
+          <mxGeometry x="40" y="280" width="40" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-16" value="Updates are accumulated as pending-phase particles." style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="100" y="80" width="420" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-18" value="Confirmed" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#d5e8d4;strokeColor=#82b366;" parent="1" vertex="1">
+          <mxGeometry x="240" y="360" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-21" value="Pending" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#d5e8d4;strokeColor=#82b366;" parent="1" vertex="1">
+          <mxGeometry x="480" y="360" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-22" value="Solvency Confirmed Phase" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#d5e8d4;strokeColor=#82b366;" parent="1" vertex="1">
+          <mxGeometry x="200" y="320" width="200" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-23" value="Solvency Unconfirmed Phase" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="760" y="320" width="280" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-24" value="Solvency confirmations may add pending-phase particles to the real-time balances." style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="100" y="280" width="550" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-25" value="solvency-confirmed time" style="endArrow=none;dashed=1;html=1;dashPattern=1 3;strokeWidth=2;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=12;" parent="1" edge="1">
+          <mxGeometry x="1" y="20" width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="659.66" y="460" as="sourcePoint" />
+            <mxPoint x="659.66" y="360" as="targetPoint" />
+            <mxPoint x="20" y="-20" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-26" value="&lt;div&gt;particles&lt;/div&gt;included in&lt;div&gt;real-time balances&lt;/div&gt;" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#d5e8d4;strokeColor=#82b366;" parent="1" vertex="1">
+          <mxGeometry x="1040" y="20" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-27" value="&lt;div&gt;particles&lt;/div&gt;excluded from&lt;div&gt;real-time balances&lt;/div&gt;" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="1040" y="100" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-28" value="3." style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=20;" parent="1" vertex="1">
+          <mxGeometry x="40" y="480" width="40" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-37" style="edgeStyle=orthogonalEdgeStyle;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;orthogonalLoop=1;jettySize=auto;html=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" source="Nm9Qbvf9_YvpDp5B0Lr9-29" target="Nm9Qbvf9_YvpDp5B0Lr9-32" edge="1">
+          <mxGeometry relative="1" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-29" value="Confirmed" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#d5e8d4;strokeColor=#82b366;dashed=1;opacity=60;" parent="1" vertex="1">
+          <mxGeometry x="240" y="560" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-32" value="&lt;strike&gt;Pending&lt;/strike&gt;&lt;br&gt;Confirmed" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#d5e8d4;strokeColor=#82b366;" parent="1" vertex="1">
+          <mxGeometry x="480" y="560" width="120" height="80" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-33" value="Solvency Confirmed Phase" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#d5e8d4;strokeColor=#82b366;" parent="1" vertex="1">
+          <mxGeometry x="200" y="520" width="200" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-34" value="Solvency Unconfirmed Phase" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="760" y="520" width="280" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-35" value="Future update will first merge confirmed particles with earlier pending particles." style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="100" y="480" width="460" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-36" value="solvency-confirmed time" style="endArrow=none;dashed=1;html=1;dashPattern=1 3;strokeWidth=2;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=12;" parent="1" edge="1">
+          <mxGeometry x="1" y="20" width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="659.6600000000001" y="660" as="sourcePoint" />
+            <mxPoint x="659.6600000000001" y="560" as="targetPoint" />
+            <mxPoint x="20" y="-20" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="Nm9Qbvf9_YvpDp5B0Lr9-40" value="(New)&lt;br&gt;Pending" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="840" y="560" width="120" height="80" as="geometry" />
+        </mxCell>
+      </root>
+    </mxGraphModel>
+  </diagram>
+  <diagram id="KBzsFtPUgiBp7If7WtaC" name="ZKSolvencyOracle">
+    <mxGraphModel dx="1195" dy="797" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="1169" pageHeight="827" math="1" shadow="0">
+      <root>
+        <mxCell id="0" />
+        <mxCell id="1" parent="0" />
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-24" value="..." style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="244.5" y="1200" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-23" value="Particle&lt;br&gt;Shard" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="224.5" y="1180" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-2" value="Token Data" style="rounded=1;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;verticalAlign=top;" parent="1" vertex="1">
+          <mxGeometry x="680" y="160" width="320.5" height="360" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-1" value="Token Events" style="rounded=1;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;verticalAlign=top;" parent="1" vertex="1">
+          <mxGeometry x="39.5" y="160" width="160" height="360" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-4" value="Transfer" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#fff2cc;strokeColor=#d6b656;" parent="1" vertex="1">
+          <mxGeometry x="59.5" y="200" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-5" value="UpdateFlow" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#fff2cc;strokeColor=#d6b656;" parent="1" vertex="1">
+          <mxGeometry x="59.5" y="240" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-6" value="Distribute" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#fff2cc;strokeColor=#d6b656;" parent="1" vertex="1">
+          <mxGeometry x="59.5" y="280" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-7" value="DistributeFlow" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#fff2cc;strokeColor=#d6b656;" parent="1" vertex="1">
+          <mxGeometry x="59.5" y="320" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-8" value="..." style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#fff2cc;strokeColor=#d6b656;" parent="1" vertex="1">
+          <mxGeometry x="59.5" y="360" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="MzWbwr8QKQwlvLbBZxQm-1" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;orthogonalLoop=1;jettySize=auto;html=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="WVFnKjtCS6OQHrKyCmlB-9" target="3EYo8ui7tVXBns0FO4iS-1">
+          <mxGeometry relative="1" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-9" value="&lt;div&gt;&lt;span style=&quot;background-color: transparent; color: light-dark(rgb(0, 0, 0), rgb(255, 255, 255));&quot;&gt;\(acc_{bob}\)&lt;/span&gt;&lt;/div&gt;" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="700" y="200" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-10" value="\(acc_{alice}\)" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="700" y="240" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-11" value="" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" edge="1">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="220" y="279.71000000000004" as="sourcePoint" />
+            <mxPoint x="300" y="279.71000000000004" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-13" value="" style="shape=umlDestroy;whiteSpace=wrap;html=1;strokeWidth=3;targetShapes=umlLifeline;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="250" y="369.71" width="30" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-14" value="" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" edge="1">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="300" y="399.71" as="sourcePoint" />
+            <mxPoint x="220" y="399.71" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-16" value="Log" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#fff2cc;strokeColor=#d6b656;" parent="1" vertex="1">
+          <mxGeometry x="39.5" y="80" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-18" value="&lt;font face=&quot;Architects Daughter&quot;&gt;&lt;b&gt;Real-time balance formular:&lt;/b&gt;&lt;/font&gt;&amp;nbsp;\( RTB(acc, t) = RTB(acc_u, t) + \sum_i RTB((pool_i, acc), t) \)" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;" parent="1" vertex="1">
+          <mxGeometry x="39.5" y="560" width="560.5" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-19" value="\(acc_{carol}\)" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="700" y="280" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-22" value="hash" style="shape=parallelogram;html=1;strokeWidth=2;perimeter=parallelogramPerimeter;whiteSpace=wrap;rounded=1;arcSize=12;size=0.23;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="800" y="520" width="80" height="20" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-25" value="\(acc_{bob}\)" style="endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;exitX=1;exitY=0.25;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" parent="1" source="WVFnKjtCS6OQHrKyCmlB-26" target="3EYo8ui7tVXBns0FO4iS-1" edge="1">
+          <mxGeometry x="0.7508" y="15" width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="760.5" y="335" as="sourcePoint" />
+            <mxPoint x="800" y="215" as="targetPoint" />
+            <Array as="points">
+              <mxPoint x="840.5" y="328" />
+              <mxPoint x="840.5" y="215" />
+            </Array>
+            <mxPoint as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-26" value="\(acc_{dan}\)" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="700" y="320" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="WVFnKjtCS6OQHrKyCmlB-27" value="\(acc_{dan}\)" style="endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;exitX=1;exitY=0.5;exitDx=0;exitDy=0;entryX=0;entryY=0.5;entryDx=0;entryDy=0;" parent="1" source="WVFnKjtCS6OQHrKyCmlB-26" target="3EYo8ui7tVXBns0FO4iS-2" edge="1">
+          <mxGeometry x="-0.4895" y="-10" width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="860" y="380" as="sourcePoint" />
+            <mxPoint x="860" y="260" as="targetPoint" />
+            <Array as="points">
+              <mxPoint x="850.5" y="335" />
+              <mxPoint x="850.5" y="255" />
+            </Array>
+            <mxPoint x="-1" y="5" as="offset" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="JBmhGo-e2T5PNSWM-v_n-1" value="Oracularized Solvency Proof" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=24;fontStyle=1" parent="1" vertex="1">
+          <mxGeometry x="359.5" y="20" width="440.5" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="MVs8Bv-dsu1i4Li3OOU4-1" value="1." style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=20;" parent="1" vertex="1">
+          <mxGeometry x="39.5" y="680" width="40" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="MVs8Bv-dsu1i4Li3OOU4-2" value="2." style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=20;" parent="1" vertex="1">
+          <mxGeometry x="39.5" y="720" width="40" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="MVs8Bv-dsu1i4Li3OOU4-3" value="Remove technical uncertainties:" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontStyle=1" parent="1" vertex="1">
+          <mxGeometry x="39.5" y="640" width="200" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="MVs8Bv-dsu1i4Li3OOU4-4" value="Account snapshots indexing (c1, c2, etc.) to calculate RTB." style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontStyle=0" parent="1" vertex="1">
+          <mxGeometry x="98.5" y="680" width="380" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="MVs8Bv-dsu1i4Li3OOU4-5" value="Memory require as the account snapshots table grows." style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontStyle=0" parent="1" vertex="1">
+          <mxGeometry x="98.5" y="720" width="380" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="MVs8Bv-dsu1i4Li3OOU4-8" value="3." style="ellipse;whiteSpace=wrap;html=1;aspect=fixed;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=20;" parent="1" vertex="1">
+          <mxGeometry x="39.5" y="760" width="40" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="MVs8Bv-dsu1i4Li3OOU4-9" value="Modeling the data structures and algorithms." style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontStyle=0" parent="1" vertex="1">
+          <mxGeometry x="98.5" y="760" width="380" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="MVs8Bv-dsu1i4Li3OOU4-11" value="&lt;font face=&quot;Architects Daughter&quot; style=&quot;font-weight: bold;&quot;&gt;Goal of the oracle: &lt;/font&gt;&lt;font face=&quot;Architects Daughter&quot; style=&quot;&quot;&gt;To a&lt;/font&gt;&lt;font face=&quot;Architects Daughter&quot; style=&quot;&quot;&gt;ssert that&lt;/font&gt;&lt;font face=&quot;Architects Daughter&quot; style=&quot;&quot;&gt;&amp;nbsp;it is safe to move forward the time:&amp;nbsp;&lt;/font&gt;&lt;font face=&quot;Architects Daughter&quot;&gt;(\(\forall u. RTB(u, t&#39;) &amp;gt;= 0\))&lt;/font&gt;" style="text;html=1;align=left;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Helvetica;" parent="1" vertex="1">
+          <mxGeometry x="39.5" y="600" width="560.5" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="IiPUnJblGAQ3UKNwHVqQ-1" value="..." style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="700" y="360" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-1" value="&lt;div&gt;&lt;span style=&quot;background-color: transparent; color: light-dark(rgb(0, 0, 0), rgb(255, 255, 255));&quot;&gt;\(pool_0\)&lt;/span&gt;&lt;/div&gt;" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="859.5" y="200" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-2" value="&lt;div&gt;&lt;span style=&quot;background-color: transparent; color: light-dark(rgb(0, 0, 0), rgb(255, 255, 255));&quot;&gt;\(pool_1\)&lt;/span&gt;&lt;/div&gt;" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" parent="1" vertex="1">
+          <mxGeometry x="859.5" y="240" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-3" value="Previous&lt;br&gt;Event Logs" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;opacity=60;fillColor=#f5f5f5;fontColor=#333333;strokeColor=#666666;" parent="1" vertex="1">
+          <mxGeometry x="84.5" y="880" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-4" value="New&lt;br&gt;Event Logs" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="204.5" y="920" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-5" value="Particle Updates" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="204.5" y="1040" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-6" value="Particle Snapshots" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="84.5" y="1000" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-7" value="" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" edge="1">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="244.5" y="970" as="sourcePoint" />
+            <mxPoint x="244.5" y="1030" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-8" value="" style="shape=orEllipse;perimeter=ellipsePerimeter;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="174.5" y="930" width="20" height="20" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-9" value="New Hash" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="324.5" y="920" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-10" value="" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" edge="1">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="74.5" y="1020" as="sourcePoint" />
+            <mxPoint x="194.5" y="1180" as="targetPoint" />
+            <Array as="points">
+              <mxPoint x="44.5" y="1020" />
+              <mxPoint x="44.5" y="1180" />
+            </Array>
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-11" value="Previous&lt;div&gt;Hash&lt;/div&gt;" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="84.5" y="920" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-13" value="=" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=24;" parent="1" vertex="1">
+          <mxGeometry x="284.5" y="930" width="40" height="17.5" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-14" value="Previous&lt;div&gt;Hash&lt;/div&gt;" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="84.5" y="1040" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-15" value="New Hash" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="324.5" y="1040" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-16" value="=" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fontSize=24;" parent="1" vertex="1">
+          <mxGeometry x="284.5" y="1051.25" width="40" height="17.5" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-17" value="validate hash" style="sketch=0;html=1;aspect=fixed;strokeColor=none;shadow=0;align=center;fillColor=#2D9C5E;verticalAlign=top;labelPosition=center;verticalLabelPosition=bottom;shape=mxgraph.gcp2.check;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="414.5" y="928.75" width="25" height="20" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-18" value="validate hash" style="sketch=0;html=1;aspect=fixed;strokeColor=none;shadow=0;align=center;fillColor=#2D9C5E;verticalAlign=top;labelPosition=center;verticalLabelPosition=bottom;shape=mxgraph.gcp2.check;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="414.5" y="1050" width="25" height="20" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-20" value="" style="shape=orEllipse;perimeter=ellipsePerimeter;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="174.5" y="1048.75" width="20" height="20" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-21" value="Particle&lt;br&gt;Shard" style="ellipse;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="204.5" y="1160" width="80" height="40" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-22" value="" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" edge="1">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="244.5" y="1090" as="sourcePoint" />
+            <mxPoint x="244.5" y="1150" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-26" value="check solvency" style="sketch=0;html=1;aspect=fixed;strokeColor=none;shadow=0;align=center;fillColor=#2D9C5E;verticalAlign=top;labelPosition=center;verticalLabelPosition=bottom;shape=mxgraph.gcp2.check;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="232" y="1240" width="25" height="20" as="geometry" />
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-28" value="" style="shape=flexArrow;endArrow=classic;html=1;rounded=0;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" edge="1">
+          <mxGeometry width="50" height="50" relative="1" as="geometry">
+            <mxPoint x="334.5" y="1200" as="sourcePoint" />
+            <mxPoint x="394.5" y="1200" as="targetPoint" />
+          </mxGeometry>
+        </mxCell>
+        <mxCell id="3EYo8ui7tVXBns0FO4iS-29" value="validate hashes&lt;br&gt;&lt;div&gt;of the shards&lt;/div&gt;" style="sketch=0;html=1;aspect=fixed;strokeColor=none;shadow=0;align=center;fillColor=#2D9C5E;verticalAlign=top;labelPosition=center;verticalLabelPosition=bottom;shape=mxgraph.gcp2.check;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;" parent="1" vertex="1">
+          <mxGeometry x="414.5" y="1190" width="25" height="20" as="geometry" />
+        </mxCell>
+        <mxCell id="dLmMYud2xTZIYCg3WTve-2" value="Token Events" style="rounded=1;whiteSpace=wrap;html=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;verticalAlign=top;" vertex="1" parent="1">
+          <mxGeometry x="318.5" y="160" width="160" height="360" as="geometry" />
+        </mxCell>
+        <mxCell id="dLmMYud2xTZIYCg3WTve-3" value="Universal" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#fff2cc;strokeColor=#d6b656;" vertex="1" parent="1">
+          <mxGeometry x="338.5" y="200" width="120" height="30" as="geometry" />
+        </mxCell>
+        <mxCell id="dLmMYud2xTZIYCg3WTve-4" value="&lt;div&gt;&lt;span style=&quot;background-color: transparent; color: light-dark(rgb(0, 0, 0), rgb(255, 255, 255));&quot;&gt;Storage&lt;/span&gt;&lt;/div&gt;" style="shape=process;whiteSpace=wrap;html=1;backgroundOutline=1;sketch=1;hachureGap=4;jiggle=2;curveFitting=1;fontFamily=Architects Daughter;fontSource=https%3A%2F%2Ffonts.googleapis.com%2Fcss%3Ffamily%3DArchitects%2BDaughter;fillColor=#f8cecc;strokeColor=#b85450;" vertex="1" parent="1">
+          <mxGeometry x="159.5" y="80" width="120" height="30" as="geometry" />
+        </mxCell>
+      </root>
+    </mxGraphModel>
+  </diagram>
+</mxfile>
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
index c41d0934b7..8ca8f7223f 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs
@@ -5,8 +5,8 @@ module Money.Theory.MonetaryTypes
     ( MonetaryTypes
       ( MT_TIME, MT_VALUE, MT_FLOWRATE, MT_UNIT
       , mt_fr_mul_t
-      , mt_v_mul_u, mt_v_div_u, mt_v_mul_u_qr_u
-      , mt_fr_mul_u, mt_fr_div_u, mt_fr_mul_u_qr_u
+      , mt_v_mul_u, mt_v_quot_u, mt_v_mul_u_qr_u
+      , mt_fr_mul_u, mt_fr_quot_u, mt_fr_mul_u_qr_u
       )
     , MonetaryTypes'tv, MonetaryTypes'tr, MonetaryTypes'tvr, MonetaryTypes'tvru
     ) where
@@ -37,11 +37,11 @@ class ( Eq (MT_TIME mt), Ord (MT_TIME mt), Num (MT_TIME mt)
         MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
     mt_v_mul_u v u = v * (fromInteger . toInteger) u
 
-    mt_v_div_u :: MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
-    default mt_v_div_u ::
+    mt_v_quot_u :: MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
+    default mt_v_quot_u ::
         (Integral (MT_VALUE mt), Integral (MT_UNIT mt)) =>
         MT_VALUE mt -> MT_UNIT mt -> MT_VALUE mt
-    mt_v_div_u v u = let u' = (fromInteger . toInteger) u in v `div` u'
+    mt_v_quot_u v u = let u' = (fromInteger . toInteger) u in v `quot` u'
 
     mt_v_mul_u_qr_u :: MT_VALUE mt -> (MT_UNIT mt, MT_UNIT mt) -> (MT_VALUE mt, MT_VALUE mt)
     default mt_v_mul_u_qr_u ::
@@ -55,11 +55,11 @@ class ( Eq (MT_TIME mt), Ord (MT_TIME mt), Num (MT_TIME mt)
         MT_FLOWRATE mt -> MT_UNIT mt -> MT_FLOWRATE mt
     mt_fr_mul_u fr u = fr * (fromInteger . toInteger) u
 
-    mt_fr_div_u :: MT_FLOWRATE mt -> MT_UNIT mt -> MT_FLOWRATE mt
-    default mt_fr_div_u ::
+    mt_fr_quot_u :: MT_FLOWRATE mt -> MT_UNIT mt -> MT_FLOWRATE mt
+    default mt_fr_quot_u ::
         (Integral (MT_FLOWRATE mt), Integral (MT_UNIT mt)) =>
         MT_FLOWRATE mt -> MT_UNIT mt -> MT_FLOWRATE mt
-    mt_fr_div_u fr u = let u' = (fromInteger . toInteger) u in fr `div` u'
+    mt_fr_quot_u fr u = let u' = (fromInteger . toInteger) u in fr `quot` u'
 
     mt_fr_mul_u_qr_u :: MT_FLOWRATE mt -> (MT_UNIT mt, MT_UNIT mt) -> (MT_FLOWRATE mt, MT_FLOWRATE mt)
     default mt_fr_mul_u_qr_u ::
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
index f4805a232a..ad0b669ece 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
@@ -1,8 +1,10 @@
 {-# LANGUAGE FunctionalDependencies #-}
 module Money.Theory.SemanticMoney
     ( -- * Semantic Money Classes & Primitives
-        MonetaryUnit (settle, settledAt, flowRate, rtb)
-    , IndexedValue (shift1, flow1)
+      MonetaryUnit (settle, settledAt, flowRate, rtb)
+    , any_mu_settle_idempotency, any_mu_constant_rtb
+    , MonetaryParticle (shift1, flow1)
+    , any_mp_shift1_reversible, any_mp_flow1_reversible
     , shift2a, shift2b, flow2a, flow2b, align2a, align2b
       -- * Semantic Money Instances
     , BasicParticle (..)
@@ -23,27 +25,70 @@ import           Money.Theory.MonetaryTypes
 -- General Payment Primitives
 ------------------------------------------------------------------------------------------------------------------------
 
--- | A monetary unit and its operators (0-primitives).
+--
+-- Monetary value and its laws.
+--
+
+-- | A monetary unit and its operators.
 class (MonetaryTypes mt, Eq mu) =>
       MonetaryUnit mt mu | mu -> mt where
+    -- | Settle the monetary unit @mu@ at time @t@.
     settle    :: t ~ MT_TIME mt => t -> mu -> mu
+    -- | Get the settled time of the monetary unit @mu@.
     settledAt :: t ~ MT_TIME mt => mu -> t
+    -- | Get the flow rate of the monetary unit @mu@ at time @t@.
     flowRate  :: MonetaryTypes'tr mt t fr => mu -> t -> fr
+    -- | Get the real-time balance of the monetary unit @mu@ at time @t@.
     rtb       :: MonetaryTypes'tvr mt t v fr => mu -> t -> v
 
--- | An indexed monetary value and its operators (1-primitives).
-class (MonetaryUnit mt iv, Monoid iv) =>
-      IndexedValue mt iv | iv -> mt where
-    shift1 :: v ~ MT_VALUE mt => v -> iv -> (iv, v)
-    flow1  :: fr ~ MT_FLOWRATE mt => fr -> iv -> (iv, fr)
+any_mu_settle_idempotency :: (MonetaryUnit mt mu, t ~ MT_TIME mt) => mu -> t -> Bool
+any_mu_settle_idempotency a t =
+    settledAt (settle t a) == t &&
+    settle t a == settle t (settle t a)
+
+any_mu_constant_rtb :: (MonetaryUnit mt mu, t ~ MT_TIME mt) => mu -> t -> t -> t -> Bool
+any_mu_constant_rtb a t1 t2 t3 =
+    rtb (settle t1 a) t3 == rtb a t3 &&
+    rtb (settle t2 a) t3 == rtb a t3 &&
+    rtb (settle t2 (settle t1 a)) t3 == rtb a t3
 
 --
--- polymorphic 2-primitives for indexed values.
+-- Monetary particle, and its polymorphic 2-primitives.
 --
 
+-- | A monetary particle and its operators (1-primitives).
+class (MonetaryUnit mt mp, Monoid mp) =>
+      MonetaryParticle mt mp | mp -> mt where
+    shift1 :: v ~ MT_VALUE mt => v -> mp -> (mp, v)
+    flow1  :: fr ~ MT_FLOWRATE mt => fr -> mp -> (mp, fr)
+
+any_mp_shift1_reversible :: (MonetaryParticle mt mp, t ~ MT_TIME mt, v ~ MT_VALUE mt) => mp -> v -> Bool
+any_mp_shift1_reversible a v =
+    rtb a t + v' == rtb a' t &&
+    a'' == a &&
+    v'' == -v'
+    where t = settledAt a
+          (a', v') = shift1 v a
+          (a'', v'') = shift1 (-v') a'
+
+any_mp_flow1_reversible :: (MonetaryParticle mt mp, t ~ MT_TIME mt, fr ~ MT_FLOWRATE mt) => mp -> fr -> Bool
+any_mp_flow1_reversible a fr =
+    fr' == flowRate a' t &&
+    a'' == a &&
+    fr'' == flowRate a t
+    where t = settledAt a
+          (a', fr') = flow1 fr a
+          (a'', fr'') = flow1 (flowRate a t) a'
+
+-- $SideBiasedOps
+--
+-- == Note on side-biased operations:
+--   1) Left side produces error term with which right side is adjusted accordingly, and vice versa.
+--   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
+
 -- | Shift value for the left side (a) or right side (b).
 shift2a, shift2b ::
-    (MonetaryTypes'tv mt t v, IndexedValue mt a, IndexedValue mt b) =>
+    (MonetaryTypes'tv mt t v, MonetaryParticle mt a, MonetaryParticle mt b) =>
     v -> t -> (a, b) -> (a, b)
 shift2a v t (a, b) =
     let (a', v') = shift1 v (settle t a)
@@ -54,7 +99,7 @@ shift2b v t (a, b) = swap (shift2a (-v) t (b, a))
 
 -- | Shifting flow for the left side (a) or right side (b).
 flow2a, flow2b ::
-    (MonetaryTypes'tr mt t fr, IndexedValue mt a, IndexedValue mt b) =>
+    (MonetaryTypes'tr mt t fr, MonetaryParticle mt a, MonetaryParticle mt b) =>
     fr -> t -> (a, b) -> (a, b)
 flow2a dfr t (a, b) =
     let (b1, fr_a) = flow1 (flowRate a t) (settle t mempty)
@@ -63,13 +108,9 @@ flow2a dfr t (a, b) =
     in assert (fr_a' == -fr_a'') (a', b <> b1 <> b2)
 flow2b dfr t (a, b) = swap (flow2a (-dfr) t (b, a))
 
--- | Value alignment 2-primitive, left-biased (a) or right-biased (b).
---
--- Note on side-biased operations:
---   1) Left side produces error term with which right side is adjusted accordingly, and vice versa.
---   2) The adjustment must not produce new error term, or otherwise it would require recursive adjustments.
+-- | Flow rates alignment on unit changes for the left side (a) or right side (b).
 align2a, align2b ::
-    (IndexedValue mt a, IndexedValue mt b) =>
+    (MonetaryParticle mt a, MonetaryParticle mt b) =>
     MT_UNIT mt -> MT_UNIT mt -> MT_TIME mt -> (a, b) -> (a, b)
 align2a u u' t (a, b) = (a', b')
     where fr = flowRate a t
@@ -94,7 +135,7 @@ instance MonetaryTypes mt => Semigroup (BasicParticle mt) where
     a@(BasicParticle t1 _ _) <> b@(BasicParticle t2 _ _) = BasicParticle t' (sv1 + sv2) (r1 + r2)
         -- The binary operator supports negative time values while abiding the monoidal laws.
         -- The practical semantics of values of mixed-sign is not of the concern of this specification.
-        where t' = max t1 t2
+        where t' = if (abs t2) > (abs t1) then t2 else t1
               (BasicParticle _ sv1 r1) = settle t' a
               (BasicParticle _ sv2 r2) = settle t' b
 
@@ -111,7 +152,7 @@ instance MonetaryTypes mt =>
     rtb (BasicParticle t s r) t' = r `mt_fr_mul_t` (t' - t) + s
 
 instance MonetaryTypes mt =>
-         IndexedValue mt (BasicParticle mt) where
+         MonetaryParticle mt (BasicParticle mt) where
     shift1 x a = (a { bp_settled_value = bp_settled_value a + x }, x)
     flow1 r' a = (a { bp_flow_rate = r' }, r')
 
@@ -134,8 +175,8 @@ type PDP_MemberMU mt wp = (PDP_Index mt wp, PDP_Member mt wp)
 
 pdp_UpdateMember2 ::
     ( u ~ MT_UNIT mt, t ~ MT_TIME mt
-    , IndexedValue mt a
-    , IndexedValue mt wp
+    , MonetaryParticle mt a
+    , MonetaryParticle mt wp
     , mu ~ PDP_MemberMU mt wp
     ) =>
     u -> t -> (a, mu) -> (a, mu)
@@ -165,16 +206,16 @@ instance MonetaryUnit mt wp =>
          MonetaryUnit mt (PDP_Index mt wp) where
     settle t' a@(PDP_Index _ mpi) = a { pdpi_wp = settle t' mpi }
     settledAt (PDP_Index _ mpi) = settledAt mpi
-    flowRate (PDP_Index _ mpi) = flowRate mpi
-    rtb (PDP_Index _ mpi) = rtb mpi
+    flowRate (PDP_Index tu mpi) t = flowRate mpi t `mt_fr_mul_u` tu
+    rtb (PDP_Index tu mpi) t = rtb mpi t `mt_v_mul_u` tu
 
-instance IndexedValue mt wp =>
-         IndexedValue mt (PDP_Index mt wp) where
+instance MonetaryParticle mt wp =>
+         MonetaryParticle mt (PDP_Index mt wp) where
     shift1 x a@(PDP_Index tu mpi) = (a { pdpi_wp = mpi' }, x' `mt_v_mul_u` tu)
-        where (mpi', x') = if tu == 0 then (mpi, 0) else shift1 (x `mt_v_div_u` tu) mpi
+        where (mpi', x') = if tu == 0 then (mpi, 0) else shift1 (x `mt_v_quot_u` tu) mpi
 
     flow1 r' a@(PDP_Index tu mpi) = (a { pdpi_wp = mpi' }, r'' `mt_fr_mul_u` tu)
-        where (mpi', r'') = if tu == 0 then flow1 0 mpi else flow1 (r' `mt_fr_div_u` tu) mpi
+        where (mpi', r'') = if tu == 0 then flow1 0 mpi else flow1 (r' `mt_fr_quot_u` tu) mpi
 
 --
 -- PDP_Member
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
index d150294e7d..a79d42abc8 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
@@ -13,28 +13,15 @@ import           Money.Theory.TestMonetaryTypes
 
 
 --------------------------------------------------------------------------------
--- Monetary Units Laws: settle-idempotency, constant-rtb
+-- Monetary Units Laws
 --------------------------------------------------------------------------------
 
-mu_settle_idempotency :: (MonetaryUnit mt mu, t ~ MT_TIME mt) => mu -> t -> Bool
-mu_settle_idempotency a t =
-    settledAt (settle t a) == t &&
-    settle t a == settle t (settle t a)
-
-mu_constant_rtb :: (MonetaryUnit mt mu, t ~ MT_TIME mt) => mu -> t -> t -> t -> Bool
-mu_constant_rtb a t1 t2 t3 =
-    rtb (settle t1 a) t3 == rtb a t3 &&
-    rtb (settle t2 a) t3 == rtb a t3 &&
-    rtb (settle t2 (settle t1 a)) t3 == rtb a t3
-
-bp_settle_idempotency (a :: TesBasicParticle) = mu_settle_idempotency a
-bp_constant_rtb (a :: TesBasicParticle) = mu_constant_rtb a
-uidx_settle_idempotency (a :: TestUniversalIndex) = mu_settle_idempotency a
-uidx_constant_rtb (a :: TestUniversalIndex) = mu_constant_rtb a
-pdpidx_settle_idempotency (a :: TestPDP_Index) = mu_settle_idempotency a
-pdpidx_constant_rtb (a :: TestPDP_Index) = mu_constant_rtb a
-pdmb_settle_idempotency (a :: TestPDP_MemberMU) = mu_settle_idempotency a
-pdmb_constant_rtb (a :: TestPDP_Index) t1 u1 t2 u2 = mu_constant_rtb b''
+bp_settle_idempotency (a :: TestBasicParticle) = any_mu_settle_idempotency a
+bp_constant_rtb (a :: TestBasicParticle) = any_mu_constant_rtb a
+pdpidx_settle_idempotency (a :: TestPDP_Index) = any_mu_settle_idempotency a
+pdpidx_constant_rtb (a :: TestPDP_Index) = any_mu_constant_rtb a
+pdmb_settle_idempotency (a :: TestPDP_MemberMU) = any_mu_settle_idempotency a
+pdmb_constant_rtb (a :: TestPDP_Index) t1 u1 t2 u2 = any_mu_constant_rtb b''
     -- adding two members to an existing index
     where (a', b') = pdp_UpdateMember2 u1 t1 (a, (a, def))
           (_, b'') = pdp_UpdateMember2 u2 t2 (a', b')
@@ -42,39 +29,48 @@ pdmb_constant_rtb (a :: TestPDP_Index) t1 u1 t2 u2 = mu_constant_rtb b''
 mu_laws = describe "monetary unit laws" $ do
     it "bp settle idempotency" $ property bp_settle_idempotency
     it "bp constant rtb" $ property bp_constant_rtb
-    it "uidx settle idempotency" $ property uidx_settle_idempotency
-    it "uidx constant rtb" $ property uidx_constant_rtb
     it "pdpidx settle idempotency" $ property pdpidx_settle_idempotency
     it "pdpidx constant rtb" $ property pdpidx_constant_rtb
     it "pdmb settle idempotency" $ property pdmb_settle_idempotency
     it "pdmb contant rtb" $ property pdmb_constant_rtb
 
 --------------------------------------------------------------------------------
--- Monoidal Laws For Basic Particles and Indexes
+-- Monoidal Laws
 --------------------------------------------------------------------------------
 
-bp_monoid_identity (a :: TesBasicParticle) = a == a <> mempty && a == mempty <> a
-bp_monoid_assoc (a :: TesBasicParticle) b c = (a <> b) <> c == a <> (b <> c)
-uidx_monoid_identity (a :: TestUniversalIndex) = a == a <> mempty && a == mempty <> a
-uidx_monoid_assoc (a :: TestUniversalIndex) b c = (a <> b) <> c == a <> (b <> c)
+bp_monoid_identity (a :: TestBasicParticle) = a == a <> mempty && a == mempty <> a
+bp_monoid_assoc (a :: TestBasicParticle) b c = (a <> b) <> c == a <> (b <> c)
 pdidx_monoid_identity (a :: TestPDP_Index) = a == a <> mempty && a == mempty <> a
 pdidx_monoid_assoc (a :: TestPDP_Index) b c = (a <> b) <> c == a <> (b <> c)
 
 mp_monoid_laws = describe "monetary particles monoidal laws" $ do
     it "bp monoid identity law" $ property bp_monoid_identity
     it "bp monoid associativity law" $ property bp_monoid_assoc
-    it "uidx monoid identity law" $ property uidx_monoid_identity
-    it "uidx monoid associativity law" $ property uidx_monoid_assoc
     it "pdidx monoid identity law" $ property pdidx_monoid_identity
     it "pdidx monoid associativity law" $ property pdidx_monoid_assoc
 
+--------------------------------------------------------------------------------
+-- Monetary particle laws
+--------------------------------------------------------------------------------
+
+bp_shift1_reversible (a :: TestBasicParticle) = any_mp_shift1_reversible a
+bp_flow1_reversible (a :: TestBasicParticle) = any_mp_flow1_reversible a
+pdpidx_shift1_reversible (a :: TestPDP_Index) = any_mp_shift1_reversible a
+pdpidx_flow1_reversible (a :: TestPDP_Index) = any_mp_flow1_reversible a
+
+mp_laws = describe "monetary particle laws" $ do
+    it "bp shift1 reversible law" $ property bp_shift1_reversible
+    it "bp flow1 reversible law" $ property bp_flow1_reversible
+    it "pdpidx shift1 reversible law" $ property pdpidx_shift1_reversible
+    it "pdpidx flow1 reversible law" $ property pdpidx_flow1_reversible
+
 --------------------------------------------------------------------------------
 -- 1to1 2-primitives
 --------------------------------------------------------------------------------
 
 uu_f1_f2 f1 f2 t1 {- f1 -} t2 {- f2 -} t3 =
     0 == rtb a' t3 + rtb b' t3
-    where (a, b) = (mempty :: TestUniversalIndex, mempty :: TestUniversalIndex)
+    where (a, b) = (mempty :: TestBasicParticle, mempty :: TestBasicParticle)
           (a', b') = f2 t2 (f1 t1 (a, b))
 
 uu_shift2_shift2 x1 x2 = uu_f1_f2 (shift2b x1) (shift2b x2)
@@ -95,7 +91,7 @@ one2one_tests = describe "1to1 2-primitives" $ do
 updp_u1_f1_u1_f2 f1 f2 t1 u1 t2 {- f1 -} t3 {- f2 -} t4 u2 t5 =
     pdpi_total_units b'' == u2 &&
     0 == rtb a'' t5 + rtb (b'', b1') t5
-    where (a, (b, b1)) = pdp_UpdateMember2 u1 t1 (mempty :: TestUniversalIndex, (mempty :: TestPDP_Index, def))
+    where (a, (b, b1)) = pdp_UpdateMember2 u1 t1 (mempty :: TestBasicParticle, (mempty :: TestPDP_Index, def))
           (a', b') = f2 t3 (f1 t2 (a, b))
           (a'', (b'', b1')) = pdp_UpdateMember2 u2 t4 (a', (b', b1))
 
@@ -107,7 +103,7 @@ updp_u1_flow2_u1_shift2 r x = updp_u1_f1_u1_f2 (flow2a x) (shift2b r)
 updp_u1_f1_u2_f2 f1 f2 t1 u1 t2 {- f1 -} t3 u2 t4 {- f2 -} t5 =
     pdpi_total_units b''' == u1 + u2 &&
     0 == rtb a''' t5 + rtb (b''', b1) t5 + rtb (b''', b2) t5
-    where (a, (b, b1)) = pdp_UpdateMember2 u1 t1 (mempty :: TestUniversalIndex, (mempty :: TestPDP_Index, def))
+    where (a, (b, b1)) = pdp_UpdateMember2 u1 t1 (mempty :: TestBasicParticle, (mempty :: TestPDP_Index, def))
           (a', b') = f1 t2 (a, b)
           (a'', (b'', b2)) = pdp_UpdateMember2 u2 t3 (a', (b', def :: TestPDP_Member))
           (a''', b''') = f2 t4 (a'', b'')
@@ -131,14 +127,14 @@ one2n_pd_tests = describe "1toN proportional distribution 2-primitives" $ do
 -- (Constant Rate) Flow 2-Primitive
 --------------------------------------------------------------------------------
 
-uu_flow2a (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
+uu_flow2a (a :: TestBasicParticle) (b :: TestBasicParticle) t1 r1 t2 r2 t3 =
     flowRate b' t3 - flowRate b t3 == r1 + r2 && flowRate a' t3 - flowRate a t3 == -r1 -r2 &&
     rtb b' t3 - rtb b t3 == rtb a t3 - rtb a' t3 &&
     -- for shift flow semantics: rtb b' t3 - (rtb b t3 - rtb b t1) - rtb b t1 == rtb b' t3 - rtb b t3
     r1 `mt_fr_mul_t` (t2 - t1) + (r1 + r2) `mt_fr_mul_t` (t3 - t2) == rtb b' t3 - rtb b t3
     where (a', b') = flow2a r2 t2 (flow2a r1 t1 (a, b))
 
-uu_flow2b (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
+uu_flow2b (a :: TestBasicParticle) (b :: TestBasicParticle) t1 r1 t2 r2 t3 =
     flowRate b' t3 - flowRate b t3 == r1 + r2 && flowRate a' t3 - flowRate a t3 == -r1 -r2 &&
     rtb b' t3 - rtb b t3 == rtb a t3 - rtb a' t3 &&
     -- ditto
@@ -154,7 +150,7 @@ uu_flow2b (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 =
 --     where (a', (b', b1')) = pdp_UpdateMember2 1 t1 (a, (mempty :: TestPDP_Index, def))
 --           (a'', b'') = flow2a r2 t2 (flow2a r1 t1 (a', b'))
 
-updp_flow2b (a :: TestUniversalIndex) t1 r1 t2 r2 t3 =
+updp_flow2b (a :: TestBasicParticle) t1 r1 t2 r2 t3 =
     rtb (b'', b1') t3 - rtb (b', b1') t3 == rtb a' t3 - rtb a'' t3 &&
     rtb (b'', b1') t3 - rtb (b', b1') t3 == r1 `mt_fr_mul_t` (t2 - t1) + (r1 + r2) `mt_fr_mul_t` (t3 - t2) &&
     flowRate a'' t3 - flowRate a' t3 == -(r1 + r2) &&
@@ -171,6 +167,7 @@ flow2_tests = describe "flow2 tests" $ do
 tests = describe "Semantic money properties" $ do
     mu_laws
     mp_monoid_laws
+    mp_laws
     one2one_tests
     one2n_pd_tests
     flow2_tests
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
index 809b62548b..59a3f08ac5 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
@@ -11,19 +11,19 @@ import           Money.Theory.SemanticMoney
 
 newtype TestTime = TestTime Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestTime where
-    arbitrary = TestTime <$> choose (0, 2 ^ (32 :: Integer))
+    arbitrary = TestTime <$> arbitrary -- choose (0, 2 ^ (32 :: Integer))
 
 newtype TestMValue = TestMValue Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestMValue where
-    arbitrary = TestMValue <$> arbitrary -- choose (0, 2 ^ (32 :: Integer))
+    arbitrary = TestMValue <$> arbitrary
 
 newtype TestMFlowRate = TestMFlowRate Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestMFlowRate where
-    arbitrary = TestMFlowRate <$> arbitrary -- choose (0, 2 ^ (32 :: Integer))
+    arbitrary = TestMFlowRate <$> arbitrary
 
 newtype TestMUnit = TestMUnit Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestMUnit where
-    arbitrary = TestMUnit <$> arbitrary -- choose (0, 2 ^ (32 :: Integer))
+    arbitrary = TestMUnit <$> choose (0, 2 ^ (32 :: Integer))
 
 data TestMonetaryTypes
 instance MonetaryTypes TestMonetaryTypes where
@@ -33,26 +33,22 @@ instance MonetaryTypes TestMonetaryTypes where
     type MT_UNIT  TestMonetaryTypes = TestMUnit
 deriving instance Show (BasicParticle TestMonetaryTypes)
 
--- TesBasicParticle
+-- TestBasicParticle
 --
-type TesBasicParticle = BasicParticle TestMonetaryTypes
-instance Arbitrary TesBasicParticle where
+type TestBasicParticle = BasicParticle TestMonetaryTypes
+instance Arbitrary TestBasicParticle where
     arbitrary = BasicParticle <$> arbitrary <*> arbitrary <*> arbitrary
 
--- TestUniversalIndex
---
-type TestUniversalIndex = TesBasicParticle
-
 -- TestPDP_Index, TestPDP_Member, TestPDP_MemberMU
 --
-type TestPDP_Index = PDP_Index TestMonetaryTypes TesBasicParticle
+type TestPDP_Index = PDP_Index TestMonetaryTypes TestBasicParticle
 deriving instance Show TestPDP_Index
 instance Arbitrary TestPDP_Index where
     arbitrary = PDP_Index <$> arbitrary <*> arbitrary
 
-type TestPDP_Member = PDP_Member TestMonetaryTypes TesBasicParticle
+type TestPDP_Member = PDP_Member TestMonetaryTypes TestBasicParticle
 deriving instance Show TestPDP_Member
 instance Arbitrary TestPDP_Member where
     arbitrary = PDP_Member <$> arbitrary <*> arbitrary <*> arbitrary
 
-type TestPDP_MemberMU = PDP_MemberMU TestMonetaryTypes TesBasicParticle
+type TestPDP_MemberMU = PDP_MemberMU TestMonetaryTypes TestBasicParticle

From 3eb38cfb4781b5ab8889f1ba0d4a012df6e9ff5f Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Fri, 4 Jul 2025 14:26:05 +0300
Subject: [PATCH 10/11] any_mu_constant_flow

---
 .../src/Money/Theory/SemanticMoney.hs         |  7 +++++-
 .../test/Money/Theory/SemanticMoney_prop.hs   | 25 +++++++++++++------
 2 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
index ad0b669ece..4b306c29de 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
@@ -2,7 +2,7 @@
 module Money.Theory.SemanticMoney
     ( -- * Semantic Money Classes & Primitives
       MonetaryUnit (settle, settledAt, flowRate, rtb)
-    , any_mu_settle_idempotency, any_mu_constant_rtb
+    , any_mu_settle_idempotency, any_mu_constant_rtb, any_mu_constant_flow
     , MonetaryParticle (shift1, flow1)
     , any_mp_shift1_reversible, any_mp_flow1_reversible
     , shift2a, shift2b, flow2a, flow2b, align2a, align2b
@@ -52,6 +52,11 @@ any_mu_constant_rtb a t1 t2 t3 =
     rtb (settle t2 a) t3 == rtb a t3 &&
     rtb (settle t2 (settle t1 a)) t3 == rtb a t3
 
+any_mu_constant_flow :: (MonetaryUnit mt mu, t ~ MT_TIME mt) => mu -> t -> Bool
+any_mu_constant_flow a dt =
+    rtb a t + flowRate a t `mt_fr_mul_t` dt == rtb a (t + dt)
+    where t = settledAt a
+
 --
 -- Monetary particle, and its polymorphic 2-primitives.
 --
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
index a79d42abc8..559f37e97b 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
@@ -18,10 +18,16 @@ import           Money.Theory.TestMonetaryTypes
 
 bp_settle_idempotency (a :: TestBasicParticle) = any_mu_settle_idempotency a
 bp_constant_rtb (a :: TestBasicParticle) = any_mu_constant_rtb a
+bp_constant_flow (a :: TestBasicParticle) = any_mu_constant_flow a
 pdpidx_settle_idempotency (a :: TestPDP_Index) = any_mu_settle_idempotency a
 pdpidx_constant_rtb (a :: TestPDP_Index) = any_mu_constant_rtb a
-pdmb_settle_idempotency (a :: TestPDP_MemberMU) = any_mu_settle_idempotency a
-pdmb_constant_rtb (a :: TestPDP_Index) t1 u1 t2 u2 = any_mu_constant_rtb b''
+pdpidx_constant_flow (a :: TestPDP_Index) = any_mu_constant_flow a
+pdpmb_settle_idempotency (a :: TestPDP_MemberMU) = any_mu_settle_idempotency a
+pdpmb_2m_constant_rtb (a :: TestPDP_Index) t1 u1 t2 u2 = any_mu_constant_rtb b''
+    -- adding two members to an existing index
+    where (a', b') = pdp_UpdateMember2 u1 t1 (a, (a, def))
+          (_, b'') = pdp_UpdateMember2 u2 t2 (a', b')
+pdpmb_2m_constant_flow (a :: TestPDP_Index) t1 u1 t2 u2 = any_mu_constant_flow b''
     -- adding two members to an existing index
     where (a', b') = pdp_UpdateMember2 u1 t1 (a, (a, def))
           (_, b'') = pdp_UpdateMember2 u2 t2 (a', b')
@@ -29,10 +35,13 @@ pdmb_constant_rtb (a :: TestPDP_Index) t1 u1 t2 u2 = any_mu_constant_rtb b''
 mu_laws = describe "monetary unit laws" $ do
     it "bp settle idempotency" $ property bp_settle_idempotency
     it "bp constant rtb" $ property bp_constant_rtb
+    it "bp constant flow" $ property bp_constant_flow
     it "pdpidx settle idempotency" $ property pdpidx_settle_idempotency
     it "pdpidx constant rtb" $ property pdpidx_constant_rtb
-    it "pdmb settle idempotency" $ property pdmb_settle_idempotency
-    it "pdmb contant rtb" $ property pdmb_constant_rtb
+    it "pdpidx constant flow" $ property pdpidx_constant_flow
+    it "pdmb settle idempotency" $ property pdpmb_settle_idempotency
+    it "pdmb 2-members contant rtb" $ property pdpmb_2m_constant_rtb
+    it "pdmb 2-members contant flow" $ property pdpmb_2m_constant_flow
 
 --------------------------------------------------------------------------------
 -- Monoidal Laws
@@ -40,14 +49,14 @@ mu_laws = describe "monetary unit laws" $ do
 
 bp_monoid_identity (a :: TestBasicParticle) = a == a <> mempty && a == mempty <> a
 bp_monoid_assoc (a :: TestBasicParticle) b c = (a <> b) <> c == a <> (b <> c)
-pdidx_monoid_identity (a :: TestPDP_Index) = a == a <> mempty && a == mempty <> a
-pdidx_monoid_assoc (a :: TestPDP_Index) b c = (a <> b) <> c == a <> (b <> c)
+pdpidx_monoid_identity (a :: TestPDP_Index) = a == a <> mempty && a == mempty <> a
+pdpidx_monoid_assoc (a :: TestPDP_Index) b c = (a <> b) <> c == a <> (b <> c)
 
 mp_monoid_laws = describe "monetary particles monoidal laws" $ do
     it "bp monoid identity law" $ property bp_monoid_identity
     it "bp monoid associativity law" $ property bp_monoid_assoc
-    it "pdidx monoid identity law" $ property pdidx_monoid_identity
-    it "pdidx monoid associativity law" $ property pdidx_monoid_assoc
+    it "pdpidx monoid identity law" $ property pdpidx_monoid_identity
+    it "pdpidx monoid associativity law" $ property pdpidx_monoid_assoc
 
 --------------------------------------------------------------------------------
 -- Monetary particle laws

From 21511eac16e111ad452f6fe306c673373d25b55c Mon Sep 17 00:00:00 2001
From: "Miao, ZhiCheng" <zhicheng.miao@gmail.com>
Date: Fri, 4 Jul 2025 15:42:41 +0300
Subject: [PATCH 11/11] test two phase particle

---
 .../src/Money/Theory/SemanticMoney.hs             |  6 +++++-
 .../Money/Theory/TokenModel/TwoPhaseTokenModel.hs | 15 +++++++--------
 .../test/Money/Theory/SemanticMoney_prop.hs       | 13 +++++++++++++
 .../test/Money/Theory/TestMonetaryTypes.hs        | 13 ++++++++++---
 4 files changed, 35 insertions(+), 12 deletions(-)

diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
index 4b306c29de..a725d5a0c9 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/SemanticMoney.hs
@@ -58,7 +58,7 @@ any_mu_constant_flow a dt =
     where t = settledAt a
 
 --
--- Monetary particle, and its polymorphic 2-primitives.
+-- Monetary particle and its laws.
 --
 
 -- | A monetary particle and its operators (1-primitives).
@@ -85,6 +85,10 @@ any_mp_flow1_reversible a fr =
           (a', fr') = flow1 fr a
           (a'', fr'') = flow1 (flowRate a t) a'
 
+--
+-- Polymorphic 2-primitives of monetary particles.
+--
+
 -- $SideBiasedOps
 --
 -- == Note on side-biased operations:
diff --git a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/TwoPhaseTokenModel.hs b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/TwoPhaseTokenModel.hs
index 42f86962ba..73b56ca7d3 100644
--- a/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/TwoPhaseTokenModel.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/TwoPhaseTokenModel.hs
@@ -6,21 +6,20 @@ import           Money.Theory.SemanticMoney
 import           Money.Theory.TokenModel
 
 
-data TwoPhaseParticle mt = MkTwoPhaseParticle
+data TwoPhaseParticle mt = TwoPhaseParticle
     { confirmedParticle :: BasicParticle mt
     , pendingParticle   :: BasicParticle mt
     }
     deriving Eq
 
 instance MonetaryTypes mt => MonetaryUnit mt (TwoPhaseParticle mt) where
-    settle t (MkTwoPhaseParticle p_c p_p) = MkTwoPhaseParticle p_c (settle t p_p)
+    settle t (TwoPhaseParticle p_c p_p) = TwoPhaseParticle p_c (settle t p_p)
     settledAt = settledAt . pendingParticle
-    flowRate mu t =
-        flowRate (confirmedParticle mu) t +
-        if t > settledAt (confirmedParticle mu) then flowRate (pendingParticle mu) t else 0
-    rtb mu t =
-        rtb (confirmedParticle mu) t +
-        if t > settledAt (confirmedParticle mu) then rtb (pendingParticle mu) t else 0
+    flowRate mu t = flowRate (confirmedParticle mu) t + flowRate (pendingParticle mu) t
+    rtb mu t = rtb (confirmedParticle mu) t + rtb (pendingParticle mu) t
+
+syncPhase :: t ~ MT_TIME mt => TwoPhaseParticle mt -> t -> TwoPhaseParticle mt
+syncPhase = undefined
 
 type Account = Int
 
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
index 559f37e97b..1864331e5a 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/SemanticMoney_prop.hs
@@ -19,9 +19,11 @@ import           Money.Theory.TestMonetaryTypes
 bp_settle_idempotency (a :: TestBasicParticle) = any_mu_settle_idempotency a
 bp_constant_rtb (a :: TestBasicParticle) = any_mu_constant_rtb a
 bp_constant_flow (a :: TestBasicParticle) = any_mu_constant_flow a
+
 pdpidx_settle_idempotency (a :: TestPDP_Index) = any_mu_settle_idempotency a
 pdpidx_constant_rtb (a :: TestPDP_Index) = any_mu_constant_rtb a
 pdpidx_constant_flow (a :: TestPDP_Index) = any_mu_constant_flow a
+
 pdpmb_settle_idempotency (a :: TestPDP_MemberMU) = any_mu_settle_idempotency a
 pdpmb_2m_constant_rtb (a :: TestPDP_Index) t1 u1 t2 u2 = any_mu_constant_rtb b''
     -- adding two members to an existing index
@@ -32,17 +34,28 @@ pdpmb_2m_constant_flow (a :: TestPDP_Index) t1 u1 t2 u2 = any_mu_constant_flow b
     where (a', b') = pdp_UpdateMember2 u1 t1 (a, (a, def))
           (_, b'') = pdp_UpdateMember2 u2 t2 (a', b')
 
+twopp_settle_idempotency (a :: TestTwoPhaseParticle) = any_mu_settle_idempotency a
+twopp_constant_rtb (a :: TestTwoPhaseParticle) = any_mu_constant_rtb a
+twopp_constant_flow (a :: TestTwoPhaseParticle) = any_mu_constant_flow a
+
+
 mu_laws = describe "monetary unit laws" $ do
     it "bp settle idempotency" $ property bp_settle_idempotency
     it "bp constant rtb" $ property bp_constant_rtb
     it "bp constant flow" $ property bp_constant_flow
+
     it "pdpidx settle idempotency" $ property pdpidx_settle_idempotency
     it "pdpidx constant rtb" $ property pdpidx_constant_rtb
     it "pdpidx constant flow" $ property pdpidx_constant_flow
+
     it "pdmb settle idempotency" $ property pdpmb_settle_idempotency
     it "pdmb 2-members contant rtb" $ property pdpmb_2m_constant_rtb
     it "pdmb 2-members contant flow" $ property pdpmb_2m_constant_flow
 
+    it "2pp settle idempotency" $ property twopp_settle_idempotency
+    it "2pp constant rtb" $ property twopp_constant_rtb
+    it "2pp constant flow" $ property twopp_constant_flow
+
 --------------------------------------------------------------------------------
 -- Monoidal Laws
 --------------------------------------------------------------------------------
diff --git a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
index 59a3f08ac5..59f403d170 100644
--- a/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
+++ b/packages/spec-haskell/pkgs/semantic-money/test/Money/Theory/TestMonetaryTypes.hs
@@ -4,6 +4,7 @@ module Money.Theory.TestMonetaryTypes where
 import           Test.QuickCheck
 --
 import           Money.Theory.SemanticMoney
+import           Money.Theory.TokenModel.TwoPhaseTokenModel
 
 
 -- TestMonetaryTypes
@@ -11,15 +12,15 @@ import           Money.Theory.SemanticMoney
 
 newtype TestTime = TestTime Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestTime where
-    arbitrary = TestTime <$> arbitrary -- choose (0, 2 ^ (32 :: Integer))
+    arbitrary = TestTime <$> choose (-(2 ^ (32 :: Integer)), 2 ^ (32 :: Integer))
 
 newtype TestMValue = TestMValue Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestMValue where
-    arbitrary = TestMValue <$> arbitrary
+    arbitrary = TestMValue <$> choose (-(2 ^ (32 :: Integer)), 2 ^ (32 :: Integer))
 
 newtype TestMFlowRate = TestMFlowRate Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestMFlowRate where
-    arbitrary = TestMFlowRate <$> arbitrary
+    arbitrary = TestMFlowRate <$> choose (-(2 ^ (32 :: Integer)), 2 ^ (32 :: Integer))
 
 newtype TestMUnit = TestMUnit Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show)
 instance Arbitrary TestMUnit where
@@ -52,3 +53,9 @@ instance Arbitrary TestPDP_Member where
     arbitrary = PDP_Member <$> arbitrary <*> arbitrary <*> arbitrary
 
 type TestPDP_MemberMU = PDP_MemberMU TestMonetaryTypes TestBasicParticle
+
+-- TestTwoPhaseParticle
+type TestTwoPhaseParticle = TwoPhaseParticle TestMonetaryTypes
+deriving instance Show TestTwoPhaseParticle
+instance Arbitrary TestTwoPhaseParticle where
+    arbitrary = TwoPhaseParticle <$> arbitrary <*> arbitrary