diff --git a/packages/spec-haskell/Makefile b/packages/spec-haskell/Makefile index d017fe5766..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)" @@ -32,7 +33,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 +59,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 \ @@ -144,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/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/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/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 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal index b8e545aa45..7a275becd5 100644 --- a/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal +++ b/packages/spec-haskell/pkgs/semantic-money/semantic-money.cabal @@ -22,11 +22,16 @@ library import: optiongs hs-source-dirs: src exposed-modules: + Money.Theory.MonetaryTypes Money.Theory.SemanticMoney + Money.Theory.TokenModel + Money.Theory.TokenModel.NaiveTokenModel + Money.Theory.TokenModel.TwoPhaseTokenModel -- other-modules: -- 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 new file mode 100644 index 0000000000..8ca8f7223f --- /dev/null +++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/MonetaryTypes.hs @@ -0,0 +1,78 @@ +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +module Money.Theory.MonetaryTypes + ( MonetaryTypes + ( MT_TIME, MT_VALUE, MT_FLOWRATE, MT_UNIT + , mt_fr_mul_t + , 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 +-- 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_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_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 :: + 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_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_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 :: + (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 + + 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_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_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 :: + (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 + +type MonetaryTypes'tv mt t v = (MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE 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 5f39ddcf04..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 @@ -1,229 +1,260 @@ -{-# 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) + , 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 + -- * Semantic Money Instances + , BasicParticle (..) + , 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 (..)) -- --- 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 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 - 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 - 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 --- --- 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) -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 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 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 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') +------------------------------------------------------------------------------------------------------------------------ +-- General Payment Primitives +------------------------------------------------------------------------------------------------------------------------ -- --- Univeral Index +-- Monetary value and its laws. -- -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) +-- | 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 + +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 + +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 -- --- Proportional Distribution Pool +-- Monetary particle and its laws. -- -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 - -- 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) - 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, 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) - 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) - 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' } - -instance ( MonetaryTypes mt, t ~ MT_TIME mt, v ~ MT_VALUE mt - , MonetaryUnit mt t v wp) => MonetaryUnit mt t v (PDPoolMemberMU mt wp) where - settle t' (pix, pm) = (pix', pm') - where sv' = rtb (pix, pm) t' - pix'@(PDPoolIndex _ mpi') = settle t' pix - pm' = pm { pdpm_settled_value = sv', pdpm_synced_wp = mpi' } - - settledAt (_, PDPoolMember _ _ mps) = settledAt mps - - flowRate (PDPoolIndex _ mpi, PDPoolMember u _ _) = flowRate mpi `mt_v_mul_u` u - - rtb (PDPoolIndex _ mpi, PDPoolMember 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 +-- | 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' -- --- Particles: building block for indexes +-- Polymorphic 2-primitives of monetary particles. -- -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) +-- $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, 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) + -- 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 :: + (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) + (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)) + +-- | Flow rates alignment on unit changes for the left side (a) or right side (b). +align2a, align2b :: + (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 + (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 t) b) +align2b u u' t (a, b) = swap (align2a u u' t (b, 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_FLOWRATE 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) -- 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' = if (abs t2) > (abs t1) then t2 else t1 (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 +instance MonetaryTypes mt => + MonetaryUnit mt (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 + flowRate = const . bp_flow_rate + rtb (BasicParticle t s r) t' = r `mt_fr_mul_t` (t' - t) + s +instance MonetaryTypes mt => + 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') -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 +------------------------------------------------------------------------------------------------------------------------ +-- 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 :: + ( u ~ MT_UNIT mt, t ~ MT_TIME mt + , MonetaryParticle mt a + , MonetaryParticle mt 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'') = align2b tu tu' t' (mpi, settle t' a) + b'' = PDP_Index tu' mpi' + pm'' = pm' { pdpm_owned_unit = u', pdpm_synced_wp = mpi' } + +-- +-- PDP_Index as MonetaryIndex +-- + +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. + -- The practical semantics of values of mixed-sign is not of the concern of this specification. + (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 (PDP_Index mt wp) where + mempty = PDP_Index 0 mempty + +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 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 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_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_quot_u` tu) mpi + +-- +-- 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 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 + pm' = pm { pdpm_settled_value = sv', pdpm_synced_wp = mpi' } + + settledAt (_, PDP_Member _ _ mps) = settledAt mps + + 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 + -- 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 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..62117499f7 --- /dev/null +++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE FunctionalDependencies #-} +module Money.Theory.TokenModel + ( TokenEvent (..) + , TokenModel (initToken, tokenAccounts, processOneTokenEvent, processTokenEvents, isTokenSolvent) + ) where +-- +import Money.Theory.SemanticMoney + + +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} {fr}. + MonetaryTypes'tr mt t fr => + t -> acc -> acc -> fr -> TokenEvent mt acc + +class MonetaryUnit mt mu => + TokenModel mt mu acc token | token -> mu acc where + initToken :: token + + tokenAccounts :: token -> [mu] + + processOneTokenEvent :: token -> TokenEvent mt acc -> token + + processTokenEvents :: token -> [TokenEvent mt acc] -> token + processTokenEvents = foldl' processOneTokenEvent + + 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/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..73b56ca7d3 --- /dev/null +++ b/packages/spec-haskell/pkgs/semantic-money/src/Money/Theory/TokenModel/TwoPhaseTokenModel.hs @@ -0,0 +1,34 @@ +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 = TwoPhaseParticle + { confirmedParticle :: BasicParticle mt + , pendingParticle :: BasicParticle mt + } + deriving Eq + +instance MonetaryTypes mt => MonetaryUnit mt (TwoPhaseParticle mt) where + settle t (TwoPhaseParticle p_c p_p) = TwoPhaseParticle p_c (settle t p_p) + settledAt = settledAt . pendingParticle + 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 + +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 3c75d928eb..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 @@ -13,62 +13,78 @@ import Money.Theory.TestMonetaryTypes -------------------------------------------------------------------------------- --- Monetary Units Laws: settle-idempotency, constant-rtb +-- Monetary Units Laws -------------------------------------------------------------------------------- -mu_settle_idempotency :: ( MonetaryUnit TestMonetaryTypes TestTime TestMValue mu - , Eq mu - ) => mu -> TestTime -> 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 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 -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'' +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 + 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') = 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') + +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 "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 "pdmb settle idempotency" $ property pdmb_settle_idempotency - it "pdmb contant rtb" $ property pdmb_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 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) -pdidx_monoid_identity (a :: TestPDPoolIndex) = a == a <> mempty && a == mempty <> a -pdidx_monoid_assoc (a :: TestPDPoolIndex) 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) +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 "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 + it "pdpidx monoid identity law" $ property pdpidx_monoid_identity + it "pdpidx monoid associativity law" $ property pdpidx_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 @@ -76,13 +92,13 @@ mp_monoid_laws = describe "monetary particles monoidal laws" $ do 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 (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 @@ -95,90 +111,85 @@ 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 :: TestBasicParticle, (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_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 = - 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 :: TestBasicParticle, (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) -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_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')) = pdpUpdateMember2 1 t1 (a, (mempty :: TestPDPoolIndex, def)) - (a'', b'') = flow2 r2 t2 (flow2 r1 t1 (a', b')) - -uu_shiftFlow2a (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 = - flowRate b' - flowRate b == r1 + r2 && flowRate a' - flowRate a == -r1 -r2 && +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_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)) + 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_shiftFlow2b (a :: TestUniversalIndex) (b :: TestUniversalIndex) t1 r1 t2 r2 t3 = - flowRate b' - flowRate b == r1 + r2 && flowRate a' - flowRate a == -r1 -r2 && +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 - 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)) + 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_shiftFlow2a is an invalid property due to right side biansed error term adjustment. +-- NOTE: updp_flow2a is an invalid property due to right side biased error term adjustment. -updp_shiftFlow2b (a :: TestUniversalIndex) t1 r1 t2 r2 t3 = - flowRate b'' - flowRate b' == r1 + r2 && flowRate a'' - flowRate a' == -r1 -r2 && - flowRate (b'', b1') == r1 + r2 && +-- 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_flow2b (a :: TestBasicParticle) 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)) - (a'', b'') = shiftFlow2b r2 t2 (shiftFlow2b r1 t1 (a', b')) + 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) && + 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')) 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 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 e68fbd5242..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 @@ -1,10 +1,10 @@ {-# LANGUAGE TypeFamilies #-} - module Money.Theory.TestMonetaryTypes where - +-- quickcheck import Test.QuickCheck - +-- import Money.Theory.SemanticMoney +import Money.Theory.TokenModel.TwoPhaseTokenModel -- TestMonetaryTypes @@ -12,51 +12,50 @@ 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 <$> 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 <$> choose (-(2 ^ (32 :: Integer)), 2 ^ (32 :: Integer)) newtype TestMUnit = TestMUnit Integer deriving (Enum, Eq, Ord, Num, Real, Integral, Show) instance Arbitrary TestMUnit where - arbitrary = TestMUnit <$> arbitrary + arbitrary = TestMUnit <$> 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) --- TesBasicParticle +-- TestBasicParticle -- -type TesBasicParticle = BasicParticle TestMonetaryTypes -instance Arbitrary TesBasicParticle where +type TestBasicParticle = BasicParticle TestMonetaryTypes +instance Arbitrary TestBasicParticle where arbitrary = BasicParticle <$> arbitrary <*> arbitrary <*> arbitrary --- TesBasicParticle +-- TestPDP_Index, TestPDP_Member, TestPDP_MemberMU -- -type TestUniversalIndex = UniversalIndex TestMonetaryTypes TesBasicParticle -deriving instance Show TestUniversalIndex -instance Arbitrary TestUniversalIndex where - arbitrary = UniversalIndex <$> arbitrary - --- PDPoolIndex --- -type TestPDPoolIndex = PDPoolIndex TestMonetaryTypes TesBasicParticle -deriving instance Show TestPDPoolIndex -deriving instance Eq TestPDPoolIndex -instance Arbitrary TestPDPoolIndex where - arbitrary = PDPoolIndex <$> arbitrary <*> arbitrary - --- PDPoolMember --- - -type TestPDPoolMember = PDPoolMember TestMonetaryTypes TesBasicParticle -deriving instance Show TestPDPoolMember -deriving instance Eq TestPDPoolMember -instance Arbitrary TestPDPoolMember where - arbitrary = PDPoolMember <$> arbitrary <*> arbitrary <*> arbitrary - -type TestPDPoolMemberMU = PDPoolMemberMU 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 TestBasicParticle +deriving instance Show TestPDP_Member +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