{-# LANGUAGE DerivingVia #-} module ZkFold.Symbolic.Cardano.Types where import Prelude hiding (Bool, Eq, length, splitAt, (*), (+)) import ZkFold.Base.Algebra.Basic.Number import ZkFold.Base.Data.Vector import ZkFold.Symbolic.Compiler import ZkFold.Symbolic.Data.Bool (Bool) import ZkFold.Symbolic.Data.ByteString import ZkFold.Symbolic.Data.Eq (Eq) import ZkFold.Symbolic.Data.Eq.Structural import ZkFold.Symbolic.Data.UInt import ZkFold.Symbolic.Data.UTCTime newtype Transaction inputs rinputs outputs tokens datum a = Transaction ( Vector rinputs (Input tokens datum a) , (Vector inputs (Input tokens datum a) , (Vector outputs (Output tokens datum a) , (UTCTime a, UTCTime a) ))) deriving instance ( Arithmetic a , KnownNat inputs , KnownNat rinputs , KnownNat outputs , KnownNat tokens ) => SymbolicData a (Transaction inputs rinputs outputs tokens datum (ArithmeticCircuit a)) txInputs :: Transaction inputs rinputs outputs tokens datum a -> Vector inputs (Input tokens datum a) txInputs :: forall {k} (inputs :: Natural) (rinputs :: Natural) (outputs :: Natural) (tokens :: Natural) (datum :: k) a. Transaction inputs rinputs outputs tokens datum a -> Vector inputs (Input tokens datum a) txInputs (Transaction (Vector rinputs (Input tokens datum a) _, (Vector inputs (Input tokens datum a) is, (Vector outputs (Output tokens datum a), (UTCTime a, UTCTime a)) _))) = Vector inputs (Input tokens datum a) is txOutputs :: Transaction inputs rinputs outputs tokens datum a -> Vector outputs (Output tokens datum a) txOutputs :: forall {k} (inputs :: Natural) (rinputs :: Natural) (outputs :: Natural) (tokens :: Natural) (datum :: k) a. Transaction inputs rinputs outputs tokens datum a -> Vector outputs (Output tokens datum a) txOutputs (Transaction (Vector rinputs (Input tokens datum a) _, (Vector inputs (Input tokens datum a) _, (Vector outputs (Output tokens datum a) os, (UTCTime a, UTCTime a) _)))) = Vector outputs (Output tokens datum a) os newtype TxId a = TxId a deriving instance Arithmetic a => SymbolicData a (TxId (ArithmeticCircuit a)) newtype Value n a = Value (Vector n (ByteString 224 a, (ByteString 256 a, UInt 64 a))) deriving instance (Arithmetic a, KnownNat n) => SymbolicData a (Value n (ArithmeticCircuit a)) newtype Input tokens datum a = Input (OutputRef a, Output tokens datum a) txiOutput :: Input tokens datum a -> Output tokens datum a txiOutput :: forall {k} (tokens :: Natural) (datum :: k) a. Input tokens datum a -> Output tokens datum a txiOutput (Input (OutputRef a _, Output tokens datum a txo)) = Output tokens datum a txo txiDatumHash :: Input tokens datum a -> ByteString 256 a txiDatumHash :: forall {k} (tokens :: Natural) (datum :: k) a. Input tokens datum a -> ByteString 256 a txiDatumHash (Input (OutputRef a _, Output tokens datum a txo))= Output tokens datum a -> ByteString 256 a forall {k} (tokens :: Natural) (datum :: k) a. Output tokens datum a -> ByteString 256 a txoDatumHash Output tokens datum a txo deriving instance (Arithmetic a, KnownNat tokens) => SymbolicData a (Input tokens datum (ArithmeticCircuit a)) newtype Output tokens datum a = Output (Address a, (Value tokens a, ByteString 256 a)) txoAddress :: Output tokens datum a -> Address a txoAddress :: forall {k} (tokens :: Natural) (datum :: k) a. Output tokens datum a -> Address a txoAddress (Output (Address a addr, (Value tokens a, ByteString 256 a) _)) = Address a addr txoDatumHash :: Output tokens datum a -> ByteString 256 a txoDatumHash :: forall {k} (tokens :: Natural) (datum :: k) a. Output tokens datum a -> ByteString 256 a txoDatumHash (Output (Address a _, (Value tokens a _, ByteString 256 a dh))) = ByteString 256 a dh deriving instance (Arithmetic a, KnownNat tokens) => SymbolicData a (Output tokens datum (ArithmeticCircuit a)) deriving via (Structural (Output tokens datum (ArithmeticCircuit a))) instance (Arithmetic a, KnownNat tokens) => Eq (Bool (ArithmeticCircuit a)) (Output tokens datum (ArithmeticCircuit a)) newtype OutputRef a = OutputRef (TxId a, UInt 32 a) deriving instance Arithmetic a => SymbolicData a (OutputRef (ArithmeticCircuit a)) newtype Address a = Address (ByteString 4 a, (ByteString 224 a, ByteString 224 a)) paymentCredential :: Address a -> ByteString 224 a paymentCredential :: forall a. Address a -> ByteString 224 a paymentCredential (Address (ByteString 4 a _, (ByteString 224 a pc, ByteString 224 a _))) = ByteString 224 a pc deriving instance Arithmetic a => SymbolicData a (Address (ArithmeticCircuit a)) newtype DatumHash datum a = DatumHash a deriving (SymbolicData i) newtype ScriptHash a = ScriptHash a deriving (SymbolicData i)