Scripts: Haskell generation now works end-to-end

src/Ledger/Address.lagda

@@ -67,13 +67,14 @@ ScriptAddr  = ScriptBaseAddr  ⊎ ScriptBootstrapAddr
 \emph{Helper functions}
 \AgdaTarget{payCred, isVKeyAddr}
 \begin{code}
-payCred      : Addr → Credential
-netId        : Addr → Network
-isVKeyAddr   : Addr → Set
-isScriptAddr : Addr → Set
-isVKeyAddr   = isVKey ∘ payCred
-isScriptAddr = isScript ∘ payCred
-isScriptRwdAddr = isScript ∘ RwdAddr.stake
+payCred       : Addr → Credential
+netId         : Addr → Network
+isVKeyAddr    : Addr → Set
+isScriptAddr  : Addr → Set
+
+isVKeyAddr       = isVKey ∘ payCred
+isScriptAddr     = isScript ∘ payCred
+isScriptRwdAddr  = isScript ∘ RwdAddr.stake
 \end{code}
 \end{AgdaAlign}
 \caption{Definitions used in Addresses}

src/Ledger/Foreign/HSLedger.agda

@@ -241,7 +241,7 @@ instance
       { txins      = from txins
       ; txouts     = from txouts
       ; txcerts    = []
-      ; mint       = ε -- since simpleTokenAlgebra only contains ada mint will always be empty
+      ; mint       = ε -- tokenAlgebra only contains ada atm, so mint is surely empty
       ; txfee      = txfee
       ; txvldt     = from txvldt
       ; txwdrls    = ∅ᵐ
@@ -349,8 +349,8 @@ instance
       ; minimumAVS        = 0
       ; costmdls            = from costmdls
       ; prices              = prices
-      ; maxTxExUnits        = maxTxExUnits
-      ; maxBlockExUnits     = maxBlockExUnits
+      ; maxTxExUnits        = from maxTxExUnits
+      ; maxBlockExUnits     = from maxBlockExUnits
       ; coinsPerUTxOWord    = coinsPerUTxOWord
       ; maxCollateralInputs = maxCollateralInputs
       }

src/Ledger/Foreign/LedgerTypes.agda

@@ -31,36 +31,45 @@ Addr          = ℕ -- just payment credential
 TxId          = ℕ
 Ix            = ℕ
 Epoch         = ℕ
-AuxiliaryData = ⊤
 
+AuxiliaryData = ⊤
 DataHash      = ⊤
+Datum         = ⊤
+Redeemer      = ⊤
+
 TxIn          = Pair TxId Ix
 TxOut         = Pair Addr $ Pair Coin $ Maybe DataHash
 UTxO          = HSMap TxIn TxOut
 
 Hash          = ℕ
 
-data Tag : Set where
-  Spend Mint Cert Rewrd : Tag
-
+data Tag : Set where Spend Mint Cert Rewrd : Tag
 RdmrPtr = Pair Tag Ix
-ExUnits = ℕ × ℕ
+ExUnits = Pair ℕ ℕ
 
 {-# FOREIGN GHC
   type Coin  = Integer
   type Addr  = Integer
 
   type TxId  = Integer
   type Ix    = Integer
+  type Epoch = Integer
+
+  type AuxiliaryData = ()
+  type DataHash      = ()
+  type Datum         = ()
+  type Redeemer      = ()
+
   type TxIn  = (TxId, Ix)
-  type TxOut = (Addr, Coin)
+  type TxOut = (Addr, (Coin, Maybe DataHash))
   type UTxO  = [(TxIn, TxOut)]
   type Hash  = Integer
 
   data Tag     = Spend | Mint | Cert | Rewrd
   type RdmrPtr = (Tag, Ix)
   type ExUnits = (Integer, Integer)
 #-}
+{-# COMPILE GHC Tag = data Tag (Spend | Mint | Cert | Rewrd) #-}
 
 record TxBody : Set where
   field txins    : List TxIn
@@ -75,40 +84,48 @@ record TxBody : Set where
         collateral     : List TxIn
         reqSigHash     : List Hash
         scriptIntHash  : Maybe Hash
-
 {-# FOREIGN GHC
   data TxBody = MkTxBody
     { txins  :: [TxIn]
     , txouts :: [(Ix, TxOut)]
     , txfee  :: Coin
     , txvldt :: (Maybe Integer, Maybe Integer)
     , txsize :: Integer
-    , txid   :: TxId } deriving (Show, Generic)
+    , txid   :: TxId
+    , collateral    :: [TxIn]
+    , reqSigHash    :: [Hash]
+    , scriptIntHash :: Maybe Hash
+    } deriving (Show, Generic)
   instance ToExpr TxBody
 #-}
 {-# COMPILE GHC TxBody = data TxBody (MkTxBody) #-}
 
 record TxWitnesses : Set where
   field vkSigs  : List (Pair ℕ ℕ)
         scripts : List Empty
-        txdats  : HSMap DataHash ⊤
-        txrdmrs : HSMap RdmrPtr (Pair ⊤ ExUnits)
-
+        txdats  : HSMap DataHash Datum
+        txrdmrs : HSMap RdmrPtr (Pair Redeemer ExUnits)
 {-# FOREIGN GHC
   data TxWitnesses = MkTxWitnesses
-    { vkSigs :: [(Integer, Integer)], scripts :: [AgdaEmpty] } deriving (Show, Generic)
+    { vkSigs  :: [(Integer, Integer)]
+    , scripts :: [AgdaEmpty]
+    , txdats  :: [(DataHash, Datum)]
+    , txrdmrs :: [(RdmrPtr, (Redeemer, ExUnits))]
+    } deriving (Show, Generic)
   instance ToExpr TxWitnesses
 #-}
 {-# COMPILE GHC TxWitnesses = data TxWitnesses (MkTxWitnesses) #-}
 
 record Tx : Set where
   field body : TxBody
         wits : TxWitnesses
-        txAD : Maybe ⊤
-
+        txAD : Maybe AuxiliaryData
 {-# FOREIGN GHC
   data Tx = MkTx
-    { body :: TxBody, wits :: TxWitnesses, txAD :: Maybe () } deriving (Show, Generic)
+    { body :: TxBody
+    , wits :: TxWitnesses
+    , txAD :: Maybe AuxiliaryData
+    } deriving (Show, Generic)
   instance ToExpr Tx
 #-}
 {-# COMPILE GHC Tx = data Tx (MkTx) #-}
@@ -139,8 +156,6 @@ record PParams : Set where
         coinsPerUTxOWord    : Coin
         -- collateralPercent   : ℕ
         maxCollateralInputs : ℕ
-
-
 {-# FOREIGN GHC
   data PParams = MkPParams
     { a                   :: Integer
@@ -149,23 +164,23 @@ record PParams : Set where
     , maxTxSize           :: Integer
     , maxHeaderSize       :: Integer
     , maxValSize          :: Integer
-    , minUTxOValue        :: Integer
-    , poolDeposit         :: Integer
-    , emax                :: Integer
+    , minUTxOValue        :: Coin
+    , poolDeposit         :: Coin
+    , emax                :: Epoch
     , pv                  :: (Integer, Integer)
     , votingThresholds    :: ()
     , govActionLifetime   :: Integer
-    , govActionDeposit    :: Integer
-    , drepDeposit         :: Integer
-    , drepActivity        :: Integer
+    , govActionDeposit    :: Coin
+    , drepDeposit         :: Coin
+    , drepActivity        :: Epoch
     , ccMinSize           :: Integer
     , ccMaxTermLength     :: Integer
-    , minimumAVS          :: Integer
+    , minimumAVS          :: Coin
     , costmdls            :: Empty
     , prices              :: ()
     , maxTxExUnits        :: ExUnits
     , maxBlockExUnits     :: ExUnits
-    , coinsPerUTxOWord    :: Integer
+    , coinsPerUTxOWord    :: Coin
     , maxCollateralInputs :: Integer
     } deriving (Show, Generic)
   instance ToExpr PParams
@@ -175,21 +190,23 @@ record PParams : Set where
 record UTxOEnv : Set where
   field slot    : ℕ
         pparams : PParams
-
 {-# FOREIGN GHC
   data UTxOEnv = MkUTxOEnv
-    { slot :: Integer, pparams :: PParams } deriving (Show, Generic)
+    { slot    :: Integer
+    , pparams :: PParams
+    } deriving (Show, Generic)
   instance ToExpr UTxOEnv
 #-}
 {-# COMPILE GHC UTxOEnv = data UTxOEnv (MkUTxOEnv) #-}
 
 record UTxOState : Set where
   field utxo : UTxO
         fees : Coin
-
 {-# FOREIGN GHC
   data UTxOState = MkUTxOState
-    { utxo :: UTxO, fees :: Coin } deriving (Show, Generic)
+    { utxo :: UTxO
+    , fees :: Coin
+    } deriving (Show, Generic)
   instance ToExpr UTxOState
 #-}
 {-# COMPILE GHC UTxOState = data UTxOState (MkUTxOState) #-}

src/Ledger/Transaction.lagda

@@ -109,8 +109,6 @@ the transaction body are:
   UTxO  = TxIn ⇀ TxOut
   Wdrl  = RwdAddr ⇀ Coin
 
-  Index = Ix
-
   RdmrPtr : Set
   RdmrPtr = Tag × Ix
 

src/Ledger/Utxo.lagda

@@ -33,14 +33,17 @@ instance
   HasCoin-Map .getCoin s = Σᵐᵛ[ x ← s ᶠᵐ ] x
 
 isPhaseTwoScriptAddress : Tx → Addr → Bool
-isPhaseTwoScriptAddress tx a with isScriptAddr? a
-... | no ¬p = false
-... | yes p with lookupScriptHash (getScriptHash a p) tx
+isPhaseTwoScriptAddress tx a
+  with isScriptAddr? a
+... | no  _ = false
+... | yes p
+  with lookupScriptHash (getScriptHash a p) tx
 ... | nothing = false
-... | just s = isP2Script s
+... | just s  = isP2Script s
 
 totExUnits : Tx → ExUnits
-totExUnits tx = Σᵐ[ x ← TxWitnesses.txrdmrs (Tx.wits tx) ᶠᵐ ] (proj₂ (proj₂ x))
+totExUnits tx = Σᵐ[ x ← tx .wits .txrdmrs ᶠᵐ ] (x .proj₂ .proj₂)
+  where open Tx; open TxWitnesses
 
 -- utxoEntrySizeWithoutVal = 27 words (8 bytes)
 utxoEntrySizeWithoutVal : MemoryEstimate
@@ -133,11 +136,10 @@ open HasDecPartialOrder ⦃...⦄ -- remove after #237 is merged
 
 -- Boolean Implication
 _=>ᵇ_ : Bool → Bool → Bool
-_=>ᵇ_ a b = if a then b else true
+a =>ᵇ b = if a then b else true
 
-_≤ᵇ_ : ℕ → ℕ → Bool
+_≤ᵇ_ _≥ᵇ_ : ℕ → ℕ → Bool
 m ≤ᵇ n = ⌊ m ≤? n ⌋
-
 _≥ᵇ_ = flip _≤ᵇ_
 
 ≟-∅ᵇ : {A : Set} ⦃ _ : DecEq A ⦄ → (X : ℙ A) → Bool
@@ -147,15 +149,14 @@ _≥ᵇ_ = flip _≤ᵇ_
 
 feesOK : PParams → Tx → UTxO → Bool
 feesOK pp tx utxo = minfee pp tx ≤ᵇ txfee
-                  ∧ not (≟-∅ᵇ ((TxWitnesses.txrdmrs wits) ˢ))
+                  ∧ not (≟-∅ᵇ (txrdmrs ˢ))
                   =>ᵇ ( allᵇ (isVKeyAddr? ∘ proj₁) collateralRange
                       ∧ isAdaOnlyᵇ bal
                       ∧ (coin bal * 100) ≥ᵇ (txfee * pp .collateralPercent)
                       ∧ not (≟-∅ᵇ collateral)
                       )
   where
-    open Tx tx; open TxBody body
-    open PParams pp
+    open Tx tx; open TxBody body; open TxWitnesses wits; open PParams pp
     collateralRange = range $ (utxo ∣ collateral) .proj₁
     bal             = balance (utxo ∣ collateral)
 \end{code}