| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Cardano.Ledger.Constrained.Spec
Description
A Spec is a first order data structure that denotes a random generator
For example
(MapSpec era dom rng) denotes Gen(Map dom rng)
(RngSpec era t) denotes Gen[t] where the [t] has some Summing properties
(RelSep era t) denotes Gen(Set t) where the set meets some relational properties
(Size) denotes Gen Int, the size of some Map, Set, List etc.
(PairSpec era d r) denotes (([d],[r]) -> ([d],[r])) a transformer
Synopsis
- data SomeLens era t where
- maxSize ∷ Size → Int
- minSize ∷ Size → Int
- genSize ∷ Gen Size
- genSizeRange ∷ Gen Size
- genBigSize ∷ Int → Gen Size
- testSoundSize ∷ Gen Bool
- testNonNegSize ∷ Gen Bool
- testMergeSize ∷ Gen Bool
- genSizeByRep ∷ ∀ t era. Adds t ⇒ Rep era t → Gen Size
- genFromSizeByRep ∷ ∀ t era. Adds t ⇒ Rep era t → Size → Gen Int
- data SomeAdd era where
- genAddsRep ∷ Gen (SomeAdd era)
- testMergeSize2 ∷ Gen Property
- data RelSpec era dom where
- relSubset ∷ Ord t ⇒ Rep era t → Set t → RelSpec era t
- relSuperset ∷ Ord t ⇒ Rep era t → Set t → RelSpec era t
- relDisjoint ∷ Ord t ⇒ Rep era t → Set t → RelSpec era t
- relEqual ∷ Ord t ⇒ Rep era t → Set t → RelSpec era t
- showRelSpec ∷ RelSpec era dom → String
- mergeRelSpec ∷ RelSpec era d → RelSpec era d → RelSpec era d
- interSectM ∷ Ord a ⇒ Maybe (Set a) → Maybe (Set a) → Maybe (Set a)
- univSubset ∷ Ord a ⇒ Set a → Maybe (Set a) → Bool
- okSize ∷ RelSpec era d → Bool
- sizeForRel ∷ RelSpec era dom → Size
- maybeSynopsis ∷ Rep e t → Maybe t → String
- synSet ∷ Ord t ⇒ Rep era t → Set t → String
- relOper ∷ Ord d ⇒ Rep era d → Set d → Maybe (Set d) → Set d → Typed (RelSpec era d)
- runRelSpec ∷ Ord t ⇒ Set t → RelSpec era t → Bool
- genFromRelSpec ∷ ∀ era t. (Era era, Ord t) ⇒ [String] → Gen t → Int → RelSpec era t → Gen (Set t)
- genRelSpec ∷ Ord dom ⇒ [String] → Gen dom → Rep era dom → Int → Gen (RelSpec era dom)
- genDisjoint ∷ Ord a ⇒ Set a → Gen a → Gen (Set a)
- genConsistentRelSpec ∷ [String] → Gen dom → RelSpec era dom → Gen (RelSpec era dom)
- testConsistentRel ∷ Gen Property
- testSoundRelSpec ∷ Gen Property
- testMergeRelSpec ∷ Gen Property
- consistent ∷ (LiftT a, Semigroup a) ⇒ a → a → Maybe a
- manyMergeRelSpec ∷ Gen (Int, Int, [String])
- reportManyMergeRelSpec ∷ IO ()
- data RngSpec era rng where
- showRngSpec ∷ RngSpec era t → String
- mergeRngSpec ∷ ∀ r era. RngSpec era r → RngSpec era r → RngSpec era r
- sizeForRng ∷ ∀ dom era. RngSpec era dom → Size
- genFromRngSpec ∷ ∀ era r. Era era ⇒ [String] → Gen r → Int → RngSpec era r → Gen [r]
- genRngSpec ∷ ∀ w era. (Ord w, Adds w) ⇒ Gen w → Rep era w → SomeLens era w → Int → Gen (RngSpec era w)
- runRngSpec ∷ [r] → RngSpec era r → Bool
- genConsistentRngSpec ∷ ∀ era w c. (Ord w, Adds w) ⇒ Int → Gen w → Rep era w → Rep era c → SomeLens era w → Gen (RngSpec era w, RngSpec era w)
- word64CoinL ∷ Lens' Word64 Coin
- testConsistentRng ∷ Gen Property
- testSoundRngSpec ∷ Gen Property
- testMergeRngSpec ∷ Gen Property
- intDeltaCoinL ∷ Lens' Int DeltaCoin
- manyMergeRngSpec ∷ Gen (Int, Int, [String])
- reportManyMergeRngSpec ∷ IO ()
- data MapSpec era dom rng where
- showMapSpec ∷ MapSpec era dom rng → String
- mergeMapSpec ∷ Ord dom ⇒ MapSpec era dom rng → MapSpec era dom rng → MapSpec era dom rng
- mapSpec ∷ Ord d ⇒ Size → RelSpec era d → PairSpec era d r → RngSpec era r → Typed (MapSpec era d r)
- runMapSpec ∷ (Ord d, Eq r) ⇒ Map d r → MapSpec era d r → Bool
- sizeForMapSpec ∷ MapSpec era d r → Size
- genMapSpec ∷ ∀ era dom w. (Ord dom, Era era, Ord w, Adds w) ⇒ Gen dom → Rep era dom → Rep era w → SomeLens era w → Int → Gen (MapSpec era dom w)
- genFromMapSpec ∷ ∀ era w dom. (Era era, Ord dom) ⇒ String → [String] → Gen dom → Gen w → MapSpec era dom w → Gen (Map dom w)
- pairSpecTransform ∷ (Ord d, Eq r) ⇒ PairSide → Rep era d → Rep era r → Map d r → ([d], [r]) → [(d, r)]
- remove ∷ Eq a ⇒ PairSide → String → Rep era a → a → [a] → [a]
- genMapSpecIsSound ∷ Gen Property
- manyMergeMapSpec ∷ Gen (Int, Int, [String])
- reportManyMergeMapSpec ∷ IO ()
- data SetSpec era a where
- showSetSpec ∷ SetSpec era a → String
- mergeSetSpec ∷ Ord a ⇒ SetSpec era a → SetSpec era a → SetSpec era a
- setSpec ∷ Ord t ⇒ Size → RelSpec era t → Typed (SetSpec era t)
- runSetSpec ∷ Set a → SetSpec era a → Bool
- sizeForSetSpec ∷ SetSpec era a → Size
- genSetSpec ∷ Ord s ⇒ [String] → Gen s → Rep era s → Int → Gen (SetSpec era s)
- genFromSetSpec ∷ ∀ era a. Era era ⇒ [String] → Gen a → SetSpec era a → Gen (Set a)
- genSetSpecIsSound ∷ Gen Property
- manyMergeSetSpec ∷ Gen (Int, Int, [String])
- reportManyMergeSetSpec ∷ IO ()
- data ElemSpec era t where
- showElemSpec ∷ ElemSpec era a → String
- mergeElemSpec ∷ Era era ⇒ ElemSpec era a → ElemSpec era a → ElemSpec era a
- sizeForElemSpec ∷ ∀ a era. ElemSpec era a → Size
- runElemSpec ∷ [a] → ElemSpec era a → Bool
- genElemSpec ∷ ∀ w era. Adds w ⇒ Rep era w → SomeLens era w → Size → Gen (ElemSpec era w)
- genFromElemSpec ∷ ∀ era r. [String] → Gen r → Int → ElemSpec era r → Gen [r]
- manyMergeElemSpec ∷ Gen (Size, Int, [String])
- reportManyMergeElemSpec ∷ IO ()
- data ListSpec era t where
- showListSpec ∷ ListSpec era a → String
- mergeListSpec ∷ Era era ⇒ ListSpec era a → ListSpec era a → ListSpec era a
- listSpec ∷ Size → ElemSpec era t → Typed (ListSpec era t)
- sizeForListSpec ∷ ListSpec era t → Size
- runListSpec ∷ [a] → ListSpec era a → Bool
- genListSpec ∷ ∀ w era. Adds w ⇒ Rep era w → SomeLens era w → Size → Gen (ListSpec era w)
- genFromListSpec ∷ ∀ era r. [String] → Gen r → ListSpec era r → Gen [r]
- testSoundElemSpec ∷ Gen Property
- testSoundListSpec ∷ Gen Property
- manyMergeListSpec ∷ Gen (Size, Int, [String])
- reportManyMergeListSpec ∷ IO ()
- class (Arbitrary t, Adds t) ⇒ TestAdd t where
- genSet ∷ Ord t ⇒ Int → Gen t → Gen (Set t)
- testSet ∷ (Ord t, TestAdd t) ⇒ Gen (Set t)
- someSet ∷ Ord t ⇒ Gen t → Gen (Set t)
- someMap ∷ ∀ era t d. (Ord d, TestAdd t) ⇒ Rep era d → Gen (Map d t)
- aMap ∷ Era era ⇒ Gen (MapSpec era Int Word64)
- testm ∷ Gen (MapSpec BabbageEra Int Word64)
- aList ∷ Gen (ListSpec era Word64)
- testl ∷ Gen (ListSpec BabbageEra Word64)
- testV ∷ Era era ⇒ V era DeltaCoin
- genSumsTo ∷ Era era ⇒ Gen (Pred era)
- solveSumsTo ∷ Pred era → AddsSpec DeltaCoin
- condReverse ∷ Gen Property
- genAddsSpec ∷ ∀ c. Adds c ⇒ Gen (AddsSpec c)
- genNonNegAddsSpec ∷ ∀ c. Adds c ⇒ Gen (AddsSpec c)
- genOrdCond ∷ Gen OrdCond
- runAddsSpec ∷ ∀ c. Adds c ⇒ c → AddsSpec c → Bool
- sizeForAddsSpec ∷ AddsSpec c → Size
- tryManyAddsSpec ∷ Gen (AddsSpec Int) → ([String] → AddsSpec Int → Gen Int) → Gen (Int, [String])
- reportManyAddsSpec ∷ IO ()
- reportManyNonNegAddsSpec ∷ IO ()
- testSoundNonNegAddsSpec ∷ Gen Property
- testSoundAddsSpec ∷ Gen Property
- allSpecTests ∷ TestTree
- main ∷ IO ()
- data PairSide
- data PairSpec era a b where
- anyPairSpec ∷ PairSpec era d r → Bool
- showPairSpec ∷ PairSpec era dom rng → String
- mergePairSpec ∷ PairSpec era a b → PairSpec era a b → PairSpec era a b
- sizeForPairSpec ∷ PairSpec era dom rng → Size
- runPairSpec ∷ (Ord dom, Eq rng) ⇒ Map dom rng → PairSpec era dom rng → Bool
- genPairSpec ∷ ∀ era dom rng. (Ord dom, Eq rng) ⇒ Rep era dom → Rep era rng → Gen (PairSpec era dom rng)
- fixSide ∷ PairSide → PairSpec era a b → PairSpec era a b
- genConsistentPairSpec ∷ (Ord dom, Eq rng) ⇒ Rep era dom → Rep era rng → PairSpec era dom rng → Gen (PairSpec era dom rng)
- genFromPairSpec ∷ ∀ era dom rng. Ord dom ⇒ [String] → PairSpec era dom rng → Gen (Map dom rng)
- testConsistentPair ∷ Gen Property
- testSoundPairSpec ∷ Gen Property
- testMergePairSpec ∷ Gen Property
- manyMergePairSpec ∷ Gen (Int, [String])
- reportManyMergePairSpec ∷ IO ()
Documentation
Generate a Size with all positive numbers, This is used where we want Size to denote things that must be >= 0. Coin, Word64, Natural
genSizeRange ∷ Gen Size Source #
Generate a Size denoting an Int range, across both positive and negative numbers. DeltaCoin, Int, Rational. This is used when we use Size to denote OrdCond on types with negative values
genAddsRep ∷ Gen (SomeAdd era) Source #
data RelSpec era dom where Source #
Constructors
| RelAny | |
Fields
| |
| RelNever | |
| RelOper | Denotes things like: (x == y) equality, (x ⊆ y) subset, ( x ∩ y = ∅) disjointness, (x ⊇ y) superset. Invariants of r@(RepOper must (Just may) cant) 1) must is a subset of may 2) must and may are disjoint from cant 3) (sizeFromRel r) is realizable E.g. (SzRng 10 3) is NOT realizable |
| RelLens ∷ Ord b ⇒ Lens' dom b → Rep era dom → Rep era b → RelSpec era b → RelSpec era dom | |
Instances
showRelSpec ∷ RelSpec era dom → String Source #
interSectM ∷ Ord a ⇒ Maybe (Set a) → Maybe (Set a) → Maybe (Set a) Source #
The interpretation of (Just set) is set, and of Nothing is the universe (all possible sets)
univSubset ∷ Ord a ⇒ Set a → Maybe (Set a) → Bool Source #
Test if s1 is a subset of s2
Recall, if s2==Nothing, then it denotes the universe
and every set is a subset of the universe.
sizeForRel ∷ RelSpec era dom → Size Source #
Compute the Size that bounds the Size of a set generated from a RelSpec
relOper ∷ Ord d ⇒ Rep era d → Set d → Maybe (Set d) → Set d → Typed (RelSpec era d) Source #
Check that RelSpec invariants on the constructor RelOper hold on: spec@(RelOper must may cant) 1) must ⊆ may, checked by 'univSubset must may' 2) (must ∩ cant = ∅), checked by 'Set.disjoint must cant' 3) Set.size must <= Set.size (Set.difference may cant), checked by 'okSize spec'
genFromRelSpec ∷ ∀ era t. (Era era, Ord t) ⇒ [String] → Gen t → Int → RelSpec era t → Gen (Set t) Source #
return a generator that always generates things that meet the RelSpec
genRelSpec ∷ Ord dom ⇒ [String] → Gen dom → Rep era dom → Int → Gen (RelSpec era dom) Source #
Generate a random RelSpec We deliberately do NOT generate RelLens, as it is inconsistent with everything.
genDisjoint ∷ Ord a ⇒ Set a → Gen a → Gen (Set a) Source #
Generate another set which is disjoint from the input set
Note that the empty set is always a solution.
These sets tend to be rather small (size <= atLeastDelta)
genConsistentRelSpec ∷ [String] → Gen dom → RelSpec era dom → Gen (RelSpec era dom) Source #
Generate another RelSpec, guaranteed to be consistent with the input
Where (consistent a b) means: (a <> b) =/= (RelNever _)
See the property test genConsistent
reportManyMergeRelSpec ∷ IO () Source #
data RngSpec era rng where Source #
Indicates which constraints (if any) the range of a Map must adhere to There are 3 cases RngSum, RngProj, and RngRel. They are all mutually inconsistent. So while any Map may constrain its range, it can only choose ONE of the cases.
Constructors
| RngSum ∷ Adds rng ⇒ rng → Size → RngSpec era rng | The set must have Adds instance and add up to |
| RngProj ∷ Adds c ⇒ c → Rep era x → Lens' x c → Size → RngSpec era x | |
| RngElem ∷ Eq r ⇒ Rep era r → [r] → RngSpec era r | The range has exactly these elements |
| RngRel ∷ Ord x ⇒ RelSpec era x → RngSpec era x | The range must hold on the relation specified |
| RngAny ∷ RngSpec era rng | There are no constraints on the range (random generator will do) |
| RngNever ∷ [String] → RngSpec era rng | Something was inconsistent |
Instances
showRngSpec ∷ RngSpec era t → String Source #
sizeForRng ∷ ∀ dom era. RngSpec era dom → Size Source #
Compute the Size that is appropriate for a RngSpec
genFromRngSpec ∷ ∀ era r. Era era ⇒ [String] → Gen r → Int → RngSpec era r → Gen [r] Source #
Generate an arbitrary size [r] for a particular size n
The generated list is consistent with the RngSpec given as input.
genRngSpec ∷ ∀ w era. (Ord w, Adds w) ⇒ Gen w → Rep era w → SomeLens era w → Int → Gen (RngSpec era w) Source #
Generate a random RngSpec, appropriate for a given size. In order to accomodate any OrdCond
(EQL, LTH, LTE, GTE, GTH) in RngSum and RngProj, we make the total a bit larger than n
runRngSpec ∷ [r] → RngSpec era r → Bool Source #
genConsistentRngSpec ∷ ∀ era w c. (Ord w, Adds w) ⇒ Int → Gen w → Rep era w → Rep era c → SomeLens era w → Gen (RngSpec era w, RngSpec era w) Source #
reportManyMergeRngSpec ∷ IO () Source #
data MapSpec era dom rng where Source #
Indicates which constraints (if any) a Map must adhere to
Constructors
| MapSpec ∷ Size → RelSpec era dom → PairSpec era dom rng → RngSpec era rng → MapSpec era dom rng | The map may be constrained 3 ways. 1) Its size(Size) 2) its domain(RelSpec) 3) its range(RngSpec) |
| MapNever ∷ [String] → MapSpec era dom rng | Something is inconsistent |
Instances
showMapSpec ∷ MapSpec era dom rng → String Source #
mapSpec ∷ Ord d ⇒ Size → RelSpec era d → PairSpec era d r → RngSpec era r → Typed (MapSpec era d r) Source #
Use mapSpec instead of MapSpec to check size and PairSpec consistency at creation time.
Runs in the type monad, so errors are caught and reported as Solver-time errors.
This should avoid many Gen-time errors, as many of those are cause by size
inconsistencies. We can also use this in mergeMapSpec, to catch size
inconsistencies there as well as ( a b c -> dropT (mapSpec a b c)) has the same
type as MapSpec, but pushes the reports of inconsistencies into MapNever.
sizeForMapSpec ∷ MapSpec era d r → Size Source #
compute a Size that bounds a MapSpec
genMapSpec ∷ ∀ era dom w. (Ord dom, Era era, Ord w, Adds w) ⇒ Gen dom → Rep era dom → Rep era w → SomeLens era w → Int → Gen (MapSpec era dom w) Source #
Generate a random MapSpec
genFromMapSpec ∷ ∀ era w dom. (Era era, Ord dom) ⇒ String → [String] → Gen dom → Gen w → MapSpec era dom w → Gen (Map dom w) Source #
Generate a (Map d t) from a (MapSpec era d r) genFromMapSpec :: forall era w dom. (Era era, Ord dom) => (V era (Map dom w)) -> [String] -> Gen dom -> Gen w -> MapSpec era dom w -> Gen (Map dom w) genFromMapSpec nm _ _ _ (MapNever xs) = errorMess ("genFromMapSpec " ++ (show nm) ++ " (MapNever _) fails") xs genFromMapSpec nm msgs genD genR ms@(MapSpec size rel pair rng) = do n <- genFromSize size dom <- genFromRelSpec (("GenFromMapSpec " ++ (show nm) ++ "n " ++ show ms) : msgs) genD n rel rangelist <- genFromRngSpec (("genFromMapSpec " ++ (show nm) ++ "n " ++ show ms) : msgs) genR n rng pure (Map.fromList (zip (Set.toList dom) rangelist))
pairSpecTransform ∷ (Ord d, Eq r) ⇒ PairSide → Rep era d → Rep era r → Map d r → ([d], [r]) → [(d, r)] Source #
Transform the domain and range lists by removing the (domain,range) pairs from m.
for each pair (domain,range) remove domain from dlist and range from rlist,
then zip together the two remaining lists. The pairs in this list are extra
pairs which might me useful.
Strategy depends on which term to (SubMap t1 t2) are variables.
(SubMap xvar yexp) Break value of yexp into (x + extra), then answer: xvar = x
(SubMap xexp yvar) Break value of xexp into (x + extra), then answer: yvar == x + extra
reportManyMergeMapSpec ∷ IO () Source #
data SetSpec era a where Source #
Constructors
| SetSpec ∷ Ord a ⇒ Size → RelSpec era a → SetSpec era a | |
| SetNever ∷ [String] → SetSpec era a |
Instances
showSetSpec ∷ SetSpec era a → String Source #
setSpec ∷ Ord t ⇒ Size → RelSpec era t → Typed (SetSpec era t) Source #
Test the size consistency while building a SetSpec
sizeForSetSpec ∷ SetSpec era a → Size Source #
reportManyMergeSetSpec ∷ IO () Source #
data ElemSpec era t where Source #
Constructors
| ElemSum ∷ Adds t ⇒ t → Size → ElemSpec era t | The set must add up to |
| ElemProj ∷ Adds c ⇒ c → Rep era x → Lens' x c → Size → ElemSpec era x | The range must sum upto |
| ElemEqual ∷ Eq t ⇒ Rep era t → [t] → ElemSpec era t | The range has exactly these elements |
| ElemNever ∷ [String] → ElemSpec era t | |
| ElemAny ∷ ElemSpec era t |
Instances
showElemSpec ∷ ElemSpec era a → String Source #
sizeForElemSpec ∷ ∀ a era. ElemSpec era a → Size Source #
runElemSpec ∷ [a] → ElemSpec era a → Bool Source #
reportManyMergeElemSpec ∷ IO () Source #
data ListSpec era t where Source #
Specs for lists have two parts, the Size, and the elements
Instances
showListSpec ∷ ListSpec era a → String Source #
listSpec ∷ Size → ElemSpec era t → Typed (ListSpec era t) Source #
Test the size consistency while building a ListSpec
sizeForListSpec ∷ ListSpec era t → Size Source #
runListSpec ∷ [a] → ListSpec era a → Bool Source #
reportManyMergeListSpec ∷ IO () Source #
sizeForAddsSpec ∷ AddsSpec c → Size Source #
Not sure how to interpret this? As the possible totals that make the implicit OrdCond True?
tryManyAddsSpec ∷ Gen (AddsSpec Int) → ([String] → AddsSpec Int → Gen Int) → Gen (Int, [String]) Source #
reportManyAddsSpec ∷ IO () Source #
data PairSpec era a b where Source #
A map m1 meets the '(PairSpec _ _ m2)' specification if every
(key,value) pair in m2 is in m1.
Constructors
| PairSpec ∷ (Ord a, Eq b) ⇒ Rep era a → Rep era b → PairSide → Map a b → PairSpec era a b | |
| PairNever ∷ [String] → PairSpec era a b | |
| PairAny ∷ PairSpec era a b |
Instances
anyPairSpec ∷ PairSpec era d r → Bool Source #
showPairSpec ∷ PairSpec era dom rng → String Source #
sizeForPairSpec ∷ PairSpec era dom rng → Size Source #
genPairSpec ∷ ∀ era dom rng. (Ord dom, Eq rng) ⇒ Rep era dom → Rep era rng → Gen (PairSpec era dom rng) Source #
genConsistentPairSpec ∷ (Ord dom, Eq rng) ⇒ Rep era dom → Rep era rng → PairSpec era dom rng → Gen (PairSpec era dom rng) Source #
genFromPairSpec ∷ ∀ era dom rng. Ord dom ⇒ [String] → PairSpec era dom rng → Gen (Map dom rng) Source #
reportManyMergePairSpec ∷ IO () Source #