Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Test.Cardano.Ledger.Constrained.Conway.TxBodySpec
Synopsis
- subMap ∷ (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) ⇒ Specification (Map k v, Map k v)
- subMapSubDependsOnSuper ∷ (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) ⇒ Term (Map k v) → Term (Map k v) → Pred
- subMapSuperDependsOnSub ∷ (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) ⇒ Term (Map k v) → Term (Map k v) → Pred
- sumTxOut_ ∷ ∀ era. EraSpecTxOut era ⇒ Term [TxOut era] → Term Coin
- sumCoin_ ∷ Term [Coin] → Term Coin
- adjustTxOutCoin ∷ EraTxOut era ⇒ DeltaCoin → TxOut era → TxOut era
- getDepositRefund ∷ ∀ era. (EraTxCert era, ConwayEraCertState era) ⇒ PParams era → CertState era → [TxCert era] → (DeltaCoin, DeltaCoin)
- reifyX ∷ (HasSpec a, HasSpec b, IsPred p) ⇒ Term a → (a → b) → (Term b → p) → Pred
- bodyspec ∷ ∀ era. (EraSpecTxOut era, EraSpecCert era, EraSpecTxCert era, ConwayEraCertState era) ⇒ WitUniv era → CertsEnv era → CertState era → Specification (ShelleyTxBody era, Map TxIn (TxOut era), TxIn)
- putPretty ∷ ToExpr t ⇒ [Char] → t → IO ()
- go2 ∷ ∀ era. (ToExpr (TxOut era), EraSpecTxOut era, EraSpecCert era, EraSpecTxCert era, HasSpec (Tx era), HasSpec (CertState era), ConwayEraCertState era) ⇒ IO ()
- testBody ∷ IO ()
Documentation
subMap ∷ (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) ⇒ Specification (Map k v, Map k v) Source #
subMapSubDependsOnSuper ∷ (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) ⇒ Term (Map k v) → Term (Map k v) → Pred Source #
subMapSuperDependsOnSub ∷ (Ord k, IsNormalType v, IsNormalType k, HasSpec k, HasSpec v) ⇒ Term (Map k v) → Term (Map k v) → Pred Source #
getDepositRefund ∷ ∀ era. (EraTxCert era, ConwayEraCertState 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 a, HasSpec b, IsPred p) ⇒ Term a → (a → b) → (Term b → p) → Pred Source #
This is exactly the same as reify, except it names the existential varaible for better error messages
bodyspec ∷ ∀ era. (EraSpecTxOut era, EraSpecCert era, EraSpecTxCert era, ConwayEraCertState era) ⇒ WitUniv era → CertsEnv era → CertState era → Specification (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_ @era outputs) ==. inputS + with + refund - deposit - f
go2 ∷ ∀ era. (ToExpr (TxOut era), EraSpecTxOut era, EraSpecCert era, EraSpecTxCert era, HasSpec (Tx era), HasSpec (CertState era), ConwayEraCertState era) ⇒ IO () Source #