Added GOV rule to MAlonzo

src/Ledger/Foreign/LedgerTypes.agda

@@ -48,6 +48,8 @@ data ComputationResult E A : Set where
 HSMap : Set → Set → Set
 HSMap K V = List (Pair K V)
 
+AgdaRational  = Pair ℕ ℕ
+
 Coin          = ℕ
 Addr          = ℕ -- just payment credential
 
@@ -57,21 +59,29 @@ Epoch         = ℕ
 
 AuxiliaryData = ⊤
 DataHash      = ⊤
+ScriptHash    = ⊤
 Datum         = ⊤
 Redeemer      = ⊤
 Anchor        = ⊤
+Network       = ⊤
 
 TxIn          = Pair TxId Ix
 TxOut         = Pair Addr $ Pair Coin $ Maybe DataHash
 UTxO          = HSMap TxIn TxOut
 
 Hash          = ℕ
+GovActionId   = Pair TxId ℕ
+
+HashProtected : Set → Set
+HashProtected A = Pair A GovActionId
 
-data Tag : Set where Spend Mint Cert Rewrd Vote Propose : Tag
+data Tag : Set where Spend Mint Cert Rewrd VoteTag Propose : Tag
 RdmrPtr = Pair Tag Ix
 ExUnits = Pair ℕ ℕ
+ProtVer = Pair ℕ ℕ
 
 {-# FOREIGN GHC
+  type AgdaRational = (Integer, Integer)
   type Coin  = Integer
   type Addr  = Integer
 
@@ -81,9 +91,11 @@ ExUnits = Pair ℕ ℕ
 
   type AuxiliaryData = ()
   type DataHash      = ()
+  type ScriptHash    = ()
   type Datum         = ()
   type Redeemer      = ()
   type Anchor        = ()
+  type Network       = ()
 
   type TxIn  = (TxId, Ix)
   type TxOut = (Addr, (Coin, Maybe DataHash))
@@ -94,6 +106,9 @@ ExUnits = Pair ℕ ℕ
   instance ToExpr Tag
   type RdmrPtr = (Tag, Ix)
   type ExUnits = (Integer, Integer)
+  type ProtVer = (Integer, Integer)
+
+  type GovActionId = (TxId, Integer)
 #-}
 {-# COMPILE GHC Tag = data Tag (Spend | Mint | Cert | Rewrd | Vote | Propose) #-}
 
@@ -110,9 +125,11 @@ data Credential : Set where
 {-# COMPILE GHC Credential = data Credential (ScriptObj | KeyHashObj) #-}
 
 PoolParams = Credential
+RwdAddr = Pair Network Credential
 
 {-# FOREIGN GHC
   type PoolParams = Credential
+  type RwdAddr = (Network, Credential)
 
   data GovRole
     = CC
@@ -302,3 +319,99 @@ record UTxOState : Set where
   instance ToExpr UTxOState
 #-}
 {-# COMPILE GHC UTxOState = data UTxOState (MkUTxOState) #-}
+
+record EnactState : Set where
+  field esCC           : HashProtected (Maybe (Pair (HSMap Credential Epoch) AgdaRational))
+        esConstitution : HashProtected (Pair DataHash (Maybe ScriptHash))
+        esPV           : HashProtected ProtVer
+        esPParams      : HashProtected PParams
+        esWithdrawals  : HSMap RwdAddr Coin
+{-# FOREIGN GHC
+  data EnactState = MkEnactState
+    { esCC           :: (Maybe ([(Credential, Epoch)], AgdaRational), GovActionId)
+    , esConstitution :: ((DataHash, Maybe ScriptHash), GovActionId)
+    , esPV           :: (ProtVer, GovActionId)
+    , esPParams      :: (PParams, GovActionId)
+    , esWithdrawals  :: [(RwdAddr, Coin)]
+    }
+#-}
+{-# COMPILE GHC EnactState = data EnactState (MkEnactState) #-}
+
+record GovEnv : Set where
+  field geTxId       : TxId
+        geEpoch      : Epoch
+        gePparams    : PParams
+        gePpolicy    : Maybe ScriptHash
+        geEnactState : EnactState
+{-# FOREIGN GHC
+  data GovEnv = MkGovEnv
+    { geTxId :: TxId
+    , geEpoch :: Epoch
+    , gePParams :: PParams
+    , gePPolicy :: Maybe ScriptHash
+    , geEnactState :: EnactState
+    }
+#-}
+{-# COMPILE GHC GovEnv = data GovEnv (MkGovEnv) #-}
+
+Voter = GovRole × Credential
+
+data GovAction : Set where
+  NoConfidence     :                                                             GovAction
+  NewCommittee     : (HSMap Credential Epoch) → List Credential → AgdaRational → GovAction
+  NewConstitution  : DataHash → Maybe ScriptHash                               → GovAction
+  TriggerHF        : ProtVer                                                   → GovAction
+  ChangePParams    : PParams                                                   → GovAction
+  TreasuryWdrl     : HSMap RwdAddr Coin                                        → GovAction
+  Info             :                                                             GovAction
+
+data Vote : Set where
+  VoteYes     : Vote
+  VoteNo      : Vote
+  VoteAbstain : Vote
+
+record GovActionState : Set where
+  --field gasVotes       : HSMap Voter Vote
+        --gasReturnAddr  : RwdAddr
+        --gasExpiresIn   : Epoch
+        --gasAction      : GovAction
+        --gasPrevAction  : Maybe GovActionId
+
+GovState = List (Pair GovActionId GovActionState)
+{-# FOREIGN GHC
+  type GovState = [(GovActionId, GovActionState)]
+
+  data GovAction
+    = NoConfidence
+    | NewCommittee [(Credential, Epoch)] [Credential] AgdaRational
+    | NewConstitution DataHash (Maybe ScriptHash)
+    | TriggerHF ProtVer
+    | ChangePParams PParams
+    | TreasuryWdrl [(RwdAddr, Coin)]
+    | Info
+
+  data Vote
+    = VoteYes
+    | VoteNo
+    | VoteAbstain
+
+  data GovActionState = MkGovActionState
+    --{ gasVotes :: [(Voter, Vote)]
+    --, gasReturnAddr :: RwdAddr
+    --, gasExpiresIn :: Epoch
+    --, gasAction :: GovAction
+    --, gasPrevAction :: Maybe GovActionId
+    --}
+#-}
+{-# COMPILE GHC GovAction = data GovAction
+  ( NoConfidence
+  | NewCommittee
+  | NewConstitution
+  | TriggerHF
+  | ChangePParams
+  | TreasuryWdrl
+  | Info
+  )
+ #-}
+{-# COMPILE GHC Vote = data Vote (VoteYes|VoteNo|VoteAbstain) #-}
+{-# COMPILE GHC GovActionState = data GovActionState (MkGovActionState) #-}