{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}

module Test.Cardano.Ledger.Constrained.Conway.TxBodySpec where

-- import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway (Conway)
import Cardano.Ledger.Conway.Rules (CertsEnv (..))
import Cardano.Ledger.Core

-- import Cardano.Ledger.Shelley.LedgerState (AccountState (..))
import Cardano.Ledger.Shelley.TxBody (ShelleyTxBody (..))
import Cardano.Ledger.TxIn (TxIn (..))
import Cardano.Ledger.UTxO (UTxO (..), coinBalance)
import Cardano.Ledger.Val
import Constrained hiding (Value)
import Constrained.Base (Pred (..), hasSize, rangeSize)
import Data.Foldable (toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Data.Word (Word64)

import Data.Sequence.Internal (Seq)
import Lens.Micro

-- , certStateSpec)

import Test.Cardano.Ledger.Constrained.Conway.Cert (EraSpecCert (..), certStateSpec)
import Test.Cardano.Ledger.Constrained.Conway.Certs (certsEnvSpec, projectEnv)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.Instances.TxBody (fromShelleyBody)
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (EraSpecLedger (..))

import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec
import Test.Cardano.Ledger.Generic.Proof (Reflect)
import qualified Test.Cardano.Ledger.Generic.Proof as Proof
import Test.QuickCheck hiding (forAll)
import Prelude hiding (seq)

import Cardano.Ledger.Allegra (Allegra)
import Cardano.Ledger.Alonzo (Alonzo)
import Cardano.Ledger.Babbage (Babbage)
import Cardano.Ledger.Mary (Mary)
import Cardano.Ledger.Shelley (Shelley)
import Cardano.Ledger.Shelley.LedgerState (CertState)
import Data.Text (pack)
import Lens.Micro
import Prettyprinter (sep, vsep)
import Test.Cardano.Ledger.Generic.Fields (
  TxBodyField (..),
  abstractTxBody,
 )
import Test.Cardano.Ledger.Generic.PrettyCore (
  PDoc,
  PrettyA (..),
  pcTxBodyField,
  pcTxBodyWithUTxO,
  pcTxIn,
  pcTxOut,
  ppList,
  ppMap,
  ppRecord,
  ppString,
 )

-- =================================
-- Move these to the MapSpec

subMap ::
  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
  Specification fn (Map k v, Map k v)
subMap :: forall k v (fn :: Univ).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Specification fn (Map k v, Map k v)
subMap = forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (Map k v, Map k v)
[var|pair|] ->
  forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (Map k v, Map k v)
pair forall a b. (a -> b) -> a -> b
$ \ Term fn (Map k v)
[var|sub|] Term fn (Map k v)
[var|super|] ->
    [ forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map k v)
sub Term fn (Map k v)
super
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map k v)
super forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
/=. forall a (fn :: Univ). Show a => a -> Term fn a
lit (forall k a. Map k a
Map.empty)
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map k v)
sub) (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map k v)
super)
    , forall t a (fn :: Univ) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn (Map k v)
sub forall a b. (a -> b) -> a -> b
$ \ Term fn (k, v)
[var|kvpair|] ->
        forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (k, v)
kvpair forall a b. (a -> b) -> a -> b
$ \Term fn k
k Term fn v
v -> [forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn v
v Term fn k
k, forall (fn :: Univ) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn k
k Term fn (Map k v)
super) (\Term fn v
a -> Term fn v
v forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn v
a)]
    ]

subMapSubDependsOnSuper ::
  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
  Term fn (Map k v) ->
  Term fn (Map k v) ->
  Pred fn
subMapSubDependsOnSuper :: forall k v (fn :: Univ).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Term fn (Map k v) -> Term fn (Map k v) -> Pred fn
subMapSubDependsOnSuper Term fn (Map k v)
sub Term fn (Map k v)
super =
  forall (fn :: Univ). [Pred fn] -> Pred fn
Block
    [ forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map k v)
sub Term fn (Map k v)
super
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map k v)
super forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
/=. forall a (fn :: Univ). Show a => a -> Term fn a
lit (forall k a. Map k a
Map.empty)
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map k v)
sub) (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map k v)
super)
    , forall t a (fn :: Univ) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn (Map k v)
sub forall a b. (a -> b) -> a -> b
$ \ Term fn (k, v)
[var|kvpair|] ->
        forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (k, v)
kvpair forall a b. (a -> b) -> a -> b
$ \Term fn k
k Term fn v
v -> [forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn v
v Term fn k
k, forall (fn :: Univ) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn k
k Term fn (Map k v)
super) (\Term fn v
a -> Term fn v
v forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn v
a)]
    ]

subMapSuperDependsOnSub ::
  (Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
  Term fn (Map k v) ->
  Term fn (Map k v) ->
  Pred fn
subMapSuperDependsOnSub :: forall k v (fn :: Univ).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Term fn (Map k v) -> Term fn (Map k v) -> Pred fn
subMapSuperDependsOnSub Term fn (Map k v)
sub Term fn (Map k v)
super =
  forall (fn :: Univ). [Pred fn] -> Pred fn
Block
    [ forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map k v)
super Term fn (Map k v)
sub
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map k v)
super forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
/=. forall a (fn :: Univ). Show a => a -> Term fn a
lit (forall k a. Map k a
Map.empty)
    , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasSpec fn a, Ord a) =>
Term fn (Set a) -> Term fn (Set a) -> Term fn Bool
subset_ (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map k v)
sub) (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map k v)
super)
    , forall t a (fn :: Univ) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn (Map k v)
sub forall a b. (a -> b) -> a -> b
$ \ Term fn (k, v)
[var|kvpair|] ->
        forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (k, v)
kvpair forall a b. (a -> b) -> a -> b
$ \Term fn k
k Term fn v
v -> [forall (fn :: Univ) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn k
k Term fn (Map k v)
super) (\Term fn v
a -> Term fn v
v forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn v
a)]
    ]

putPretty :: PrettyA t => [Char] -> t -> IO ()
putPretty :: forall t. PrettyA t => String -> t -> IO ()
putPretty String
nm t
x = String -> IO ()
putStrLn (String
nm forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall t. PrettyA t => t -> PDoc
prettyA t
x))

test1 :: IO ()
test1 :: IO ()
test1 = do
  Map Int Int
super <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(Map Int Int) (forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
5 Integer
7))
  Map Int Int
sub <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(Map Int Int)
        ( forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term ConwayFn (Map Int Int)
sub ->
            [ forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term ConwayFn (Map Int Int)
sub) forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<. forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ (forall a (fn :: Univ). Show a => a -> Term fn a
lit Map Int Int
super))
            , forall k v (fn :: Univ).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Term fn (Map k v) -> Term fn (Map k v) -> Pred fn
subMapSubDependsOnSuper Term ConwayFn (Map Int Int)
sub (forall a (fn :: Univ). Show a => a -> Term fn a
lit Map Int Int
super)
            ]
        )
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"\nsuper" Map Int Int
super
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"sub" Map Int Int
sub

test2 :: IO ()
test2 :: IO ()
test2 = do
  Map Int Int
sub <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(Map Int Int) (forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
4 Integer
4))
  Map Int Int
super <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(Map Int Int)
        ( forall a (fn :: Univ) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term ConwayFn (Map Int Int)
super ->
            [ forall k v (fn :: Univ).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Term fn (Map k v) -> Term fn (Map k v) -> Pred fn
subMapSuperDependsOnSub (forall a (fn :: Univ). Show a => a -> Term fn a
lit Map Int Int
sub) Term ConwayFn (Map Int Int)
super
            , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term ConwayFn (Map Int Int)
super) forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof (Oneof SetFn OrdFn) (Oneof MapFn FunFn))
           (Oneof
              (Oneof TreeFn MapFn) (Oneof ListFn (Oneof CoerceFn PairFn))))
        (Oneof
           (Oneof (Oneof EqFn IntFn) (Oneof StringFn SizeFn))
           (Oneof
              (Oneof FunFn SumFn) (Oneof GenericsFn (Oneof CoinFn BoolFn))))))
  Integer
6
            ]
        )
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"\nsuper" Map Int Int
super
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"sub" Map Int Int
sub

foo :: IO (Map Int Int, Map Int Int)
foo :: IO (Map Int Int, Map Int Int)
foo = forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec forall a b. (a -> b) -> a -> b
$ forall k v (fn :: Univ).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Specification fn (Map k v, Map k v)
subMap @Int @Int @ConwayFn

-- ===================================================================

bodyspec ::
  forall era fn.
  ( EraSpecTxOut era fn
  , EraSpecCert era fn
  ) =>
  UTxO era ->
  CertsEnv era ->
  CertState era ->
  Specification
    fn
    ( ShelleyTxBody era
    , Map (TxIn (EraCrypto era)) (TxOut era)
    , TxIn (EraCrypto era)
    )
bodyspec :: forall era (fn :: Univ).
(EraSpecTxOut era fn, EraSpecCert era fn) =>
UTxO era
-> CertsEnv era
-> CertState era
-> Specification
     fn
     (ShelleyTxBody era, Map (TxIn (EraCrypto era)) (TxOut era),
      TxIn (EraCrypto era))
bodyspec UTxO era
utxo CertsEnv era
certsenv CertState era
certstate =
  forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term fn (ShelleyTxBody era)
[var|shelleyBody|] Term fn (Map (TxIn StandardCrypto) (TxOut era))
[var|inputUtxo|] Term fn (TxIn StandardCrypto)
[var|feeInput|] ->
    forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (ShelleyTxBody era)
shelleyBody forall a b. (a -> b) -> a -> b
$
      \ Term fn (Set (TxIn StandardCrypto))
[var|inputs|] Term fn [TxOut era]
[var|outputs|] Term fn [TxCert era]
[var|certs|] Term fn (Map (RewardAccount StandardCrypto) Coin)
[var|rewAcct|] Term fn Coin
[var|fee|] Term fn SlotNo
_ Term fn (Maybe (Update era))
[var|update|] Term fn (Maybe (AuxiliaryDataHash StandardCrypto))
_ ->
        [ forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ShelleyTxBody era)
shelleyBody Term fn Coin
fee
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ShelleyTxBody era)
shelleyBody Term fn (Set (TxIn StandardCrypto))
inputs
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ShelleyTxBody era)
shelleyBody Term fn [TxOut era]
outputs
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (TxIn StandardCrypto)
feeInput Term fn (Map (TxIn StandardCrypto) (TxOut era))
inputUtxo
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Set (TxIn StandardCrypto))
inputs Term fn (Map (TxIn StandardCrypto) (TxOut era))
inputUtxo
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn [TxOut era]
outputs Term fn (Map (TxIn StandardCrypto) (TxOut era))
inputUtxo
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn Coin
fee Term fn (TxIn StandardCrypto)
feeInput
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn [TxOut era]
outputs Term fn (Map (TxIn StandardCrypto) (TxOut era))
inputUtxo
        , forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Map (TxIn StandardCrypto) (TxOut era))
inputUtxo (forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
2 Integer
4))
        , forall k v (fn :: Univ).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Term fn (Map k v) -> Term fn (Map k v) -> Pred fn
subMapSubDependsOnSuper Term fn (Map (TxIn StandardCrypto) (TxOut era))
inputUtxo (forall a (fn :: Univ). Show a => a -> Term fn a
lit (forall era. UTxO era -> Map (TxIn (EraCrypto era)) (TxOut era)
unUTxO UTxO era
utxo))
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Maybe (Update era))
update forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: Univ). Show a => a -> Term fn a
lit forall a. Maybe a
Nothing
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (TxIn StandardCrypto)
feeInput (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (TxIn StandardCrypto) (TxOut era))
inputUtxo)
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn (TxIn StandardCrypto)
feeInput (forall a (fn :: Univ). Show a => a -> Term fn a
lit (forall era. UTxO era -> Map (TxIn (EraCrypto era)) (TxOut era)
unUTxO UTxO era
utxo))) (\ Term fn (TxOut era)
[var|txout|] -> Term fn Coin
fee forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall era (fn :: Univ).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ Term fn (TxOut era)
txout)
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Set (TxIn StandardCrypto))
inputs forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (TxIn StandardCrypto) (TxOut era))
inputUtxo
        , forall (fn :: Univ) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Map (TxIn StandardCrypto) (TxOut era))
inputUtxo (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
Map.toList) forall a b. (a -> b) -> a -> b
$
            \ Term fn [TxOut era]
[var|txouts|] ->
              [ forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn [TxOut era]
outputs Term fn [TxOut era]
txouts
              , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ (forall (fn :: Univ) era.
EraSpecTxOut era fn =>
Term fn [TxOut era] -> Term fn Coin
sumCoin_ @fn @era Term fn [TxOut era]
outputs) forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: Univ) era.
EraSpecTxOut era fn =>
Term fn [TxOut era] -> Term fn Coin
sumCoin_ @fn @era Term fn [TxOut era]
txouts forall a. Num a => a -> a -> a
- Term fn Coin
fee
              ]
        , forall t a (fn :: Univ) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn [TxCert era]
certs forall a b. (a -> b) -> a -> b
$ \ Term fn (TxCert era)
[var|oneCert|] -> forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (TxCert era)
oneCert (forall era (fn :: Univ).
EraSpecCert era fn =>
CertEnv era -> CertState era -> Specification fn (TxCert era)
txCertSpec (forall era. CertsEnv era -> CertEnv era
projectEnv CertsEnv era
certsenv) CertState era
certstate)
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn [TxCert era]
certs forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Integer
4
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map (RewardAccount StandardCrypto) Coin)
rewAcct forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: Univ). Show a => a -> Term fn a
lit forall k a. Map k a
Map.empty
        ]

seqToList :: IsConwayUniv fn => HasSpec fn t => Specification fn (Data.Sequence.Internal.Seq t, [t])
seqToList :: forall (fn :: Univ) t.
(IsConwayUniv fn, HasSpec fn t) =>
Specification fn (Seq t, [t])
seqToList = forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term fn (Seq t)
[var|seq|] Term fn [t]
[var|list|] -> forall (fn :: Univ) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn (Seq t)
seq forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (\Term fn [t]
x -> Term fn [t]
list forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn [t]
x)

testUTxO ::
  forall era. (Era era, HasSpec ConwayFn (TxOut era)) => IO (Map (TxIn (EraCrypto era)) (TxOut era))
testUTxO :: forall era.
(Era era, HasSpec ConwayFn (TxOut era)) =>
IO (Map (TxIn (EraCrypto era)) (TxOut era))
testUTxO =
  forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
    forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(Map (TxIn (EraCrypto era)) (TxOut era)) (forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
7 Integer
15))

-- | Exercise the 'bodyspec'
go ::
  forall era.
  ( EraSpecTxOut era ConwayFn
  , EraSpecCert era ConwayFn
  , HasSpec ConwayFn (Tx era)
  ) =>
  IO ()
go :: forall era.
(EraSpecTxOut era ConwayFn, EraSpecCert era ConwayFn,
 HasSpec ConwayFn (Tx era)) =>
IO ()
go = do
  UTxO era
utxo <- forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era.
(Era era, HasSpec ConwayFn (TxOut era)) =>
IO (Map (TxIn (EraCrypto era)) (TxOut era))
testUTxO @era
  CertState era
certState <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertState era)
        (forall (fn :: Univ) era.
(IsConwayUniv fn, EraSpecDeleg era) =>
Specification fn (CertState era)
certStateSpec @ConwayFn @era) -- (lit (AccountState (Coin 1000) (Coin 100))) (lit (EpochNo 100)))
        -- error "STOP"
  CertsEnv era
certsEnv <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertsEnv era) forall era (fn :: Univ).
(EraSpecPParams era, HasSpec fn (Tx era), IsConwayUniv fn) =>
Specification fn (CertsEnv era)
certsEnvSpec

  (ShelleyTxBody era
basic, Map (TxIn StandardCrypto) (TxOut era)
subutxo, TxIn StandardCrypto
feeinput) <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec (forall era (fn :: Univ).
(EraSpecTxOut era fn, EraSpecCert era fn) =>
UTxO era
-> CertsEnv era
-> CertState era
-> Specification
     fn
     (ShelleyTxBody era, Map (TxIn (EraCrypto era)) (TxOut era),
      TxIn (EraCrypto era))
bodyspec @era @ConwayFn UTxO era
utxo CertsEnv era
certsEnv CertState era
certState)

  String -> IO ()
putStrLn
    (String
"Input UTxO, total " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era. EraTxOut era => UTxO era -> Coin
coinBalance @era UTxO era
utxo) forall a. [a] -> [a] -> [a]
++ String
", size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Int
Map.size (forall era. UTxO era -> Map (TxIn (EraCrypto era)) (TxOut era)
unUTxO UTxO era
utxo)))
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"\nSubMap of Utxo" (forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn StandardCrypto) (TxOut era)
subutxo)
  String -> IO ()
putStrLn (String
"SubMap of UTxO, total Coin " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era. EraTxOut era => UTxO era -> Coin
coinBalance @era (forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn StandardCrypto) (TxOut era)
subutxo)))
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"\nfeeInput" TxIn StandardCrypto
feeinput
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"\nTxBody" ShelleyTxBody era
basic

sumCoin_ :: forall fn era. EraSpecTxOut era fn => Term fn [TxOut era] -> Term fn Coin
sumCoin_ :: forall (fn :: Univ) era.
EraSpecTxOut era fn =>
Term fn [TxOut era] -> Term fn Coin
sumCoin_ Term fn [TxOut era]
x = forall (fn :: Univ) a b.
(BaseUniverse fn, Foldy fn b, HasSpec fn a) =>
(Term fn a -> Term fn b) -> Term fn [a] -> Term fn b
foldMap_ (forall era (fn :: Univ).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn) Term fn [TxOut era]
x

-- ===============================================================

bodyspec2 ::
  forall era fn.
  ( EraSpecTxOut era fn
  , EraSpecCert era fn
  ) =>
  CertsEnv era ->
  CertState era ->
  Specification
    fn
    ( ShelleyTxBody era
    , Map (TxIn (EraCrypto era)) (TxOut era)
    , TxIn (EraCrypto era)
    )
bodyspec2 :: forall era (fn :: Univ).
(EraSpecTxOut era fn, EraSpecCert era fn) =>
CertsEnv era
-> CertState era
-> Specification
     fn
     (ShelleyTxBody era, Map (TxIn (EraCrypto era)) (TxOut era),
      TxIn (EraCrypto era))
bodyspec2 CertsEnv era
certsenv CertState era
certstate =
  forall a (fn :: Univ) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term fn (ShelleyTxBody era)
[var|shelleyBody|] Term fn (Map (TxIn StandardCrypto) (TxOut era))
[var|utxo|] Term fn (TxIn StandardCrypto)
[var|feeInput|] ->
    forall (fn :: Univ) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (ShelleyTxBody era)
shelleyBody forall a b. (a -> b) -> a -> b
$
      \ Term fn (Set (TxIn StandardCrypto))
[var|inputs|] Term fn [TxOut era]
[var|outputs|] Term fn [TxCert era]
[var|certs|] Term fn (Map (RewardAccount StandardCrypto) Coin)
[var|rewAcct|] Term fn Coin
[var|fee|] Term fn SlotNo
_ Term fn (Maybe (Update era))
[var|update|] Term fn (Maybe (AuxiliaryDataHash StandardCrypto))
_ ->
        [ forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ShelleyTxBody era)
shelleyBody Term fn Coin
fee
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ShelleyTxBody era)
shelleyBody (Term fn (Set (TxIn StandardCrypto))
inputs :: Term fn (Set (TxIn (EraCrypto era))))
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ShelleyTxBody era)
shelleyBody Term fn [TxOut era]
outputs
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ShelleyTxBody era)
shelleyBody Term fn [TxCert era]
certs
        , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxo Term fn (Set (TxIn StandardCrypto))
inputs
        , -- , exists (\eval -> undefined) $ \ [var|feeInput|] ->
          forall a p (fn :: Univ).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists (\forall b. Term fn b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys (forall b. Term fn b -> b
eval Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxo) (forall b. Term fn b -> b
eval Term fn (Set (TxIn StandardCrypto))
inputs))) forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (TxIn StandardCrypto) (TxOut era))
[var|utxosubset|] ->
            forall a p (fn :: Univ).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists (\forall b. Term fn b -> b
_eval -> forall a. HasCallStack => a
undefined) forall a b. (a -> b) -> a -> b
$ \ Term fn (Map (TxIn StandardCrypto) (TxOut era))
[var|tempUtxo|] ->
              [ forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Set (TxIn StandardCrypto))
inputs Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset
              , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxo Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset
              , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (TxIn StandardCrypto)
feeInput Term fn (Set (TxIn StandardCrypto))
inputs
              , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn Coin
fee Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset
              , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn Coin
fee Term fn (TxIn StandardCrypto)
feeInput
              , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn [TxOut era]
outputs Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset
              , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn [TxOut era]
outputs Term fn Coin
fee
              , forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxo Term fn (Map (TxIn StandardCrypto) (TxOut era))
tempUtxo
              , forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset (forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
3 Integer
4))
              , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (TxIn StandardCrypto)
feeInput Term fn (Set (TxIn StandardCrypto))
inputs
              , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Set (TxIn StandardCrypto))
inputs forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset
              , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust (forall (fn :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k, IsNormalType v) =>
Term fn k -> Term fn (Map k v) -> Term fn (Maybe v)
lookup_ Term fn (TxIn StandardCrypto)
feeInput Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset) (\ Term fn (TxOut era)
[var|txout|] -> Term fn Coin
fee forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall era (fn :: Univ).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn Term fn (TxOut era)
txout)
              , forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: Univ) k v.
(HasSpec fn (Map k v), HasSpec fn k, Ord k) =>
Term fn (Map k v) -> Term fn (Set k)
dom_ Term fn (Map (TxIn StandardCrypto) (TxOut era))
tempUtxo) (forall (fn :: Univ) t.
(HasSpec fn t, Sized t) =>
SizeSpec fn -> Specification fn t
hasSize (forall (fn :: Univ). Integer -> Integer -> SizeSpec fn
rangeSize Integer
8 Integer
10))
              , forall k v (fn :: Univ).
(Ord k, IsNormalType v, HasSpec fn k, HasSpec fn v) =>
Term fn (Map k v) -> Term fn (Map k v) -> Pred fn
subMapSuperDependsOnSub Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset Term fn (Map (TxIn StandardCrypto) (TxOut era))
tempUtxo
              , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ (forall (fn :: Univ) era.
EraSpecTxOut era fn =>
Term fn [TxOut era] -> Term fn Coin
sumCoin_ @fn @era Term fn [TxOut era]
outputs) forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: Univ) era.
EraSpecTxOut era fn =>
Term fn [TxOut era] -> Term fn Coin
sumCoin_ @fn @era (forall (fn :: Univ) k v.
(HasSpec fn k, HasSpec fn v, Ord k) =>
Term fn (Map k v) -> Term fn [v]
rng_ Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxosubset) forall a. Num a => a -> a -> a
- Term fn Coin
fee
              , forall t a (fn :: Univ) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn [TxOut era]
outputs forall a b. (a -> b) -> a -> b
$ \Term fn (TxOut era)
x -> forall era (fn :: Univ).
EraSpecTxOut era fn =>
Term fn (TxOut era) -> Term fn Coin
txOutCoin_ @era @fn Term fn (TxOut era)
x forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
>=. forall a (fn :: Univ). Show a => a -> Term fn a
lit (Integer -> Coin
Coin Integer
0)
              , forall (fn :: Univ) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify
                  (forall (fn :: Univ) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Term fn (a, b)
pair_ Term fn (Map (TxIn StandardCrypto) (TxOut era))
tempUtxo Term fn (TxIn StandardCrypto)
feeInput)
                  (\(Map (TxIn StandardCrypto) (TxOut era)
m, TxIn StandardCrypto
i) -> forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust forall era. EraTxOut era => TxOut era -> TxOut era
baz TxIn StandardCrypto
i Map (TxIn StandardCrypto) (TxOut era)
m)
                  (\Term fn (Map (TxIn StandardCrypto) (TxOut era))
u -> Term fn (Map (TxIn StandardCrypto) (TxOut era))
utxo forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (Map (TxIn StandardCrypto) (TxOut era))
u)
              ]
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Maybe (Update era))
update forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: Univ). Show a => a -> Term fn a
lit forall a. Maybe a
Nothing
        , forall t a (fn :: Univ) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn [TxCert era]
certs forall a b. (a -> b) -> a -> b
$ \ Term fn (TxCert era)
[var|oneCert|] -> forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (TxCert era)
oneCert (forall era (fn :: Univ).
EraSpecCert era fn =>
CertEnv era -> CertState era -> Specification fn (TxCert era)
txCertSpec (forall era. CertsEnv era -> CertEnv era
projectEnv CertsEnv era
certsenv) CertState era
certstate)
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn [TxCert era]
certs forall a (fn :: Univ).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term fn Integer
4
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (Map (RewardAccount StandardCrypto) Coin)
rewAcct forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: Univ). Show a => a -> Term fn a
lit forall k a. Map k a
Map.empty
        , forall (fn :: Univ) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: Univ).
(HasSpec fn a, Sized a) =>
Term fn a -> Term fn Integer
sizeOf_ Term fn [TxOut era]
outputs forall (fn :: Univ) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn Integer
4
        ]

baz :: EraTxOut era => TxOut era -> TxOut era
baz :: forall era. EraTxOut era => TxOut era -> TxOut era
baz TxOut era
x = TxOut era
x forall a b. a -> (a -> b) -> b
& forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
coinTxOutL forall s t a b. ASetter s t a b -> b -> s -> t
.~ ((TxOut era
x forall s a. s -> Getting a s a -> a
^. forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
coinTxOutL) forall t. Val t => t -> t -> t
<+> (Integer -> Coin
Coin Integer
100))

go2 ::
  forall era.
  ( EraSpecTxOut era ConwayFn
  , EraSpecCert era ConwayFn
  , HasSpec ConwayFn (Tx era)
  ) =>
  IO ()
go2 :: forall era.
(EraSpecTxOut era ConwayFn, EraSpecCert era ConwayFn,
 HasSpec ConwayFn (Tx era)) =>
IO ()
go2 = do
  CertState era
certState <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
      forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertState era)
        (forall (fn :: Univ) era.
(IsConwayUniv fn, EraSpecDeleg era) =>
Specification fn (CertState era)
certStateSpec @ConwayFn @era) -- (lit (AccountState (Coin 1000) (Coin 100))) (lit (EpochNo 100)))
        -- error "STOP"
  CertsEnv era
certsEnv <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @ConwayFn @(CertsEnv era) forall era (fn :: Univ).
(EraSpecPParams era, HasSpec fn (Tx era), IsConwayUniv fn) =>
Specification fn (CertsEnv era)
certsEnvSpec

  (ShelleyTxBody era
body, Map (TxIn StandardCrypto) (TxOut era)
utxomap, TxIn StandardCrypto
feeinput) <-
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall (fn :: Univ) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec (forall era (fn :: Univ).
(EraSpecTxOut era fn, EraSpecCert era fn) =>
CertsEnv era
-> CertState era
-> Specification
     fn
     (ShelleyTxBody era, Map (TxIn (EraCrypto era)) (TxOut era),
      TxIn (EraCrypto era))
bodyspec2 @era @ConwayFn CertsEnv era
certsEnv CertState era
certState)
  let utxo :: UTxO era
utxo = forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO Map (TxIn StandardCrypto) (TxOut era)
utxomap

  String -> IO ()
putStrLn
    (String
"Input UTxO, total " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era. EraTxOut era => UTxO era -> Coin
coinBalance @era UTxO era
utxo) forall a. [a] -> [a] -> [a]
++ String
", size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Int
Map.size Map (TxIn StandardCrypto) (TxOut era)
utxomap))
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"UTxO" UTxO era
utxo
  forall t. PrettyA t => String -> t -> IO ()
putPretty String
"\nfeeInput" TxIn StandardCrypto
feeinput
  String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall era. Reflect era => UTxO era -> TxBody era -> PDoc
pcTxBodyWithUTxO UTxO era
utxo (forall era. EraTxBody era => ShelleyTxBody era -> TxBody era
fromShelleyBody ShelleyTxBody era
body)))