Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.Cardano.Ledger.Constrained.Conway.TxBodySpec

Synopsis

subMap ∷ (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) ⇒ Specification fn (Map k v, Map k v)
subMapSubDependsOnSuper ∷ (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) ⇒ Term fn (Map k v) → Term fn (Map k v) → Pred fn
subMapSuperDependsOnSub ∷ (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) ⇒ Term fn (Map k v) → Term fn (Map k v) → Pred fn
sumTxOut_ ∷ ∀ fn era. EraSpecTxOut era fn ⇒ Term fn [TxOut era] → Term fn Coin
sumCoin_ ∷ ∀ fn. IsConwayUniv fn ⇒ Term fn [Coin] → Term fn Coin
adjustTxOutCoin ∷ EraTxOut era ⇒ DeltaCoin → TxOut era → TxOut era
getDepositRefund ∷ ∀ era. EraTxCert era ⇒ PParams era → CertState era → [TxCert era] → (DeltaCoin, DeltaCoin)
reifyX ∷ (HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → (Term fn b → p) → Pred fn
bodyspec ∷ ∀ era fn. (EraSpecTxOut era fn, EraSpecCert era fn, EraSpecTxCert fn era) ⇒ WitUniv era → CertsEnv era → CertState era → Specification fn (ShelleyTxBody era, Map TxIn (TxOut era), TxIn)
putPretty ∷ PrettyA t ⇒ [Char] → t → IO ()
go2 ∷ ∀ era. (EraSpecTxOut era ConwayFn, EraSpecCert era ConwayFn, EraSpecTxCert ConwayFn era, HasSpec ConwayFn (Tx era)) ⇒ IO ()
testBody ∷ IO ()

Documentation

subMap ∷ (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) ⇒ Specification fn (Map k v, Map k v) Source #

subMapSubDependsOnSuper ∷ (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) ⇒ Term fn (Map k v) → Term fn (Map k v) → Pred fn Source #

subMapSuperDependsOnSub ∷ (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) ⇒ Term fn (Map k v) → Term fn (Map k v) → Pred fn Source #

sumTxOut_ ∷ ∀ fn era. EraSpecTxOut era fn ⇒ Term fn [TxOut era] → Term fn Coin Source #

sumCoin_ ∷ ∀ fn. IsConwayUniv fn ⇒ Term fn [Coin] → Term fn Coin Source #

adjustTxOutCoin ∷ EraTxOut era ⇒ DeltaCoin → TxOut era → TxOut era Source #

getDepositRefund ∷ ∀ era. EraTxCert era ⇒ PParams era → CertState era → [TxCert era] → (DeltaCoin, DeltaCoin) Source #

Extract the total deposits and refunds from a list of TxCerts. This a kind of AdaPot relative to the Certs in a Transaction body It depends on the PParams (deposit ammounts for registering a staking key, a ppol, and registering a Drep) and on the CertState (what deposits were made in the past)

reifyX ∷ (HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → (Term fn b → p) → Pred fn Source #

This is exactly the same as reify, except it names the existential varaible for better error messages

bodyspec ∷ ∀ era fn. (EraSpecTxOut era fn, EraSpecCert era fn, EraSpecTxCert fn era) ⇒ WitUniv era → CertsEnv era → CertState era → Specification fn (ShelleyTxBody era, Map TxIn (TxOut era), TxIn) Source #

This is the first step to generating balanced TxBodies. It illustrates several techniques 1) Generate a tuple of related types. Previously we relied on generating one type and then passing the actual generated value as the input of the next generator. This is an alternative to that. But note we still rely partly on the old technique because we take CertsEnv and CertState values as input. 2) Carefully using dependsOn, to make explicit the order the code writer thinks the the variables should be solved in. This makes failures less mysterious. Because variable ordering failures are mysterious and hard to solve 3) The use of nested reify (here reifyX which just makes error messages better). This supports using complicated Haskell functions to extract one random value, from a previous solved variable using a pure function. Examples of this are getDepositRefund and adjustTxOutCoin 4) How complicated balancing constraints can be solved declaratively, rather than algorithmically i.e. toDelta_ (sumTxOut_ fn era outputs) ==. inputS + with + refund - deposit - f

putPretty ∷ PrettyA t ⇒ [Char] → t → IO () Source #

go2 ∷ ∀ era. (EraSpecTxOut era ConwayFn, EraSpecCert era ConwayFn, EraSpecTxCert ConwayFn era, HasSpec ConwayFn (Tx era)) ⇒ IO () Source #

testBody ∷ IO () Source #