Skip to content

Commit

Permalink
Added GOV rule to MAlonzo
Browse files Browse the repository at this point in the history
  • Loading branch information
@Soupstraw
Soupstraw committed Mar 28, 2024
1 parent 981edbc commit 563477c
Show file tree
Hide file tree
Showing 2 changed files with 269 additions and 4 deletions.
114 changes: 111 additions & 3 deletions src/Ledger/Foreign/HSLedger.agda
View file
Expand Up @@ -16,7 +16,7 @@ import Foreign.Haskell as F
import Ledger.Foreign.LedgerTypes as F

open import Ledger.Crypto
open import Ledger.Transaction
open import Ledger.Transaction renaming (Vote to VoteTag)
open import Ledger.Types.Epoch
open import Ledger.Types.GovStructure

Expand Down Expand Up @@ -165,7 +165,6 @@ HSGovStructure = record
}
instance _ = HSGovStructure

open import Ledger.GovernanceActions it hiding (Vote; GovRole; VDeleg; Anchor)
open import Ledger.Deleg it hiding (PoolParams; DCert)

HSTransactionStructure : TransactionStructure
Expand Down Expand Up @@ -202,16 +201,24 @@ HSAbstractFunctions = record
}
instance _ = HSAbstractFunctions

open TransactionStructure it
open TransactionStructure it hiding (GovVote; GovProposal)
open import Ledger.Gov.Properties it
open import Ledger.Utxo it it
open import Ledger.Utxo.Properties it it
open import Ledger.Utxow.Properties it it
open import Data.Rational

instance
_ = Convertible-Refl {⊤}
_ = Convertible-Refl {ℕ}
_ = Convertible-Refl {String}

Convertible-Rational : Convertible ℚ F.Rational
Convertible-Rational = λ where
.to (mkℚ n d _) → n F., d
.from (n F., zero) → 0ℚ -- TODO is there a safer way to do this?
.from (n F., (suc d)) → n Data.Rational./ suc d

-- Since the foreign address is just a number, we do bad stuff here
Convertible-Addr : Convertible Addr F.Addr
Convertible-Addr = λ where
Expand Down Expand Up @@ -391,6 +398,102 @@ instance
Convertible-ComputationResult : ConvertibleType ComputationResult F.ComputationResult
Convertible-ComputationResult = autoConvertible

Convertible-RwdAddr : Convertible (GovStructure.RwdAddr govStructure) F.RwdAddr
Convertible-RwdAddr = λ where
.to record { net = net ; stake = stake } → to net F., to stake
.from (net F., stake) → record { net = from net ; stake = from stake }

open import Ledger.Enact govStructure
Convertible-EnactState : ConvertibleType EnactState F.EnactState
Convertible-EnactState = autoConvertible

Convertible-GovEnv : ConvertibleType GovEnv F.GovEnv
Convertible-GovEnv = autoConvertible

open import Ledger.GovernanceActions govStructure using (Vote; GovVote; GovProposal)
Convertible-Vote : ConvertibleType Vote F.Vote
Convertible-Vote = autoConvertible

Convertible-PParamsUpdate : Convertible (GovStructure.PParamsUpdate govStructure) F.PParamsUpdate
Convertible-PParamsUpdate = record { to = id ; from = id }

Convertible-GovAction : ConvertibleType GovAction F.GovAction
Convertible-GovAction = autoConvertible

toNeedsHash : ∀ {action} → F.GovActionID → NeedsHash action
toNeedsHash {NoConfidence} x = from x
toNeedsHash {NewCommittee _ _ _} x = from x
toNeedsHash {NewConstitution _ _} x = from x
toNeedsHash {TriggerHF _} x = from x
toNeedsHash {ChangePParams _} x = from x
toNeedsHash {TreasuryWdrl _} x = tt
toNeedsHash {Info} x = tt

fromNeedsHash : ∀ {action} → NeedsHash action → F.GovActionID
fromNeedsHash {NoConfidence} x = to x
fromNeedsHash {NewCommittee _ _ _} x = to x
fromNeedsHash {NewConstitution _ _} x = to x
fromNeedsHash {TriggerHF _} x = to x
fromNeedsHash {ChangePParams _} x = to x
fromNeedsHash {TreasuryWdrl _} x = 0 F., 0
fromNeedsHash {Info} x = 0 F., 0

instance
Convertible-GovActionState : Convertible GovActionState F.GovActionState
Convertible-GovActionState = λ where
.to record { votes = votes ; returnAddr = returnAddr ; expiresIn = expiresIn ; action = action ; prevAction = prevAction } →
record
{ gasVotes = to votes
; gasReturnAddr = to returnAddr
; gasExpiresIn = to expiresIn
; gasAction = to action
; gasPrevAction = fromNeedsHash prevAction
}
.from record { gasVotes = gasVotes ; gasReturnAddr = gasReturnAddr ; gasExpiresIn = gasExpiresIn ; gasAction = gasAction ; gasPrevAction = gasPrevAction } →
record
{ votes = from gasVotes
; returnAddr = from gasReturnAddr
; expiresIn = from gasExpiresIn
; action = from gasAction
; prevAction = toNeedsHash gasPrevAction
}

Convertible-GovVote : ConvertibleType GovVote F.GovVote
Convertible-GovVote = autoConvertible

Convertible-GovProposal : Convertible GovProposal F.GovProposal
Convertible-GovProposal = λ where
.to record { action = action ; prevAction = prevAction ; policy = policy ; deposit = deposit ; returnAddr = returnAddr ; anchor = anchor } →
record
{ gpAction = to action
; gpPrevAction = fromNeedsHash prevAction
; gpPolicy = to policy
; gpDeposit = to deposit
; gpReturnAddr = to returnAddr
; gpAnchor = to anchor
}
.from record { gpAction = gpAction ; gpPrevAction = gpPrevAction ; gpPolicy = gpPolicy ; gpDeposit = gpDeposit ; gpReturnAddr = gpReturnAddr ; gpAnchor = gpAnchor } →
record
{ action = from gpAction
; prevAction = toNeedsHash gpPrevAction
; policy = from gpPolicy
; deposit = from gpDeposit
; returnAddr = from gpReturnAddr
; anchor = from gpAnchor
}

Convertible-GovSignal : Convertible (GovVote ⊎ GovProposal) F.GovSignal
Convertible-GovSignal = λ where
.to (inj₁ x) → F.GovSignalVote (to x)
.to (inj₂ y) → F.GovSignalProposal (to y)
.from (F.GovSignalVote x) → inj₁ (from x)
.from (F.GovSignalProposal x) → inj₂ (from x)

Convertible-⊥⊎ : ∀ {A} → Convertible (⊥ ⊎ A) A
Convertible-⊥⊎ = λ where
.to (inj₂ y) → y
.from → inj₂

utxo-step : F.UTxOEnv → F.UTxOState → F.Tx → F.ComputationResult String F.UTxOState
utxo-step = to UTXO-step

Expand All @@ -400,3 +503,8 @@ utxow-step : F.UTxOEnv → F.UTxOState → F.Tx → F.ComputationResult String F
utxow-step = to (compute Computational-UTXOW)

{-# COMPILE GHC utxow-step as utxowStep #-}

gov-step : F.GovEnv → F.GovState → List F.GovSignal → F.ComputationResult String F.GovState
gov-step = to (compute Computational-GOV)

{-# COMPILE GHC gov-step as govStep #-}
159 changes: 158 additions & 1 deletion src/Ledger/Foreign/LedgerTypes.agda
View file
Expand Up @@ -9,10 +9,12 @@ open import Prelude

open import Foreign.Haskell
open import Foreign.Haskell.Coerce
open import Data.Rational.Base

{-# FOREIGN GHC
import GHC.Generics (Generic)
import Data.TreeDiff
import Prelude hiding (Rational)
#-}

data Empty : Set where
Expand Down Expand Up @@ -47,43 +49,56 @@ data ComputationResult E A : Set where

HSMap : Set → Set → Set
HSMap K V = List (Pair K V)
Rational = Pair ℤ ℕ

Coin = ℕ
Addr = ℕ -- just payment credential

TxId = ℕ
Ix = ℕ
Epoch = ℕ
ScriptHash = ℕ

AuxiliaryData = ⊤
DataHash = ⊤
Datum = ⊤
Redeemer = ⊤
Anchor = ⊤
Network = ⊤
PParamsUpdate = ⊤

TxIn = Pair TxId Ix
TxOut = Pair Addr $ Pair Coin $ Maybe DataHash
UTxO = HSMap TxIn TxOut

Hash = ℕ

data Tag : Set where Spend Mint Cert Rewrd Vote Propose : Tag
GovActionID = Pair TxId ℕ

HashProtected : Set → Set
HashProtected A = Pair A GovActionID

data Tag : Set where Spend Mint Cert Rewrd VoteTag Propose : Tag
RdmrPtr = Pair Tag Ix
ExUnits = Pair ℕ ℕ
ProtVer = Pair ℕ ℕ

{-# FOREIGN GHC
type Rational = (Integer, Integer)
type Coin = Integer
type Addr = Integer
type TxId = Integer
type Ix = Integer
type Epoch = Integer
type ScriptHash = Integer
type AuxiliaryData = ()
type DataHash = ()
type Datum = ()
type Redeemer = ()
type Anchor = ()
type Network = ()
type TxIn = (TxId, Ix)
type TxOut = (Addr, (Coin, Maybe DataHash))
Expand All @@ -94,6 +109,8 @@ 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) #-}

Expand All @@ -110,9 +127,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
Expand Down Expand Up @@ -302,3 +321,141 @@ 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) Rational))
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)], Rational), 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 = Pair GovRole Credential

data GovAction : Set where
NoConfidence : GovAction
NewCommittee : (HSMap Credential Epoch) → List Credential → Rational → GovAction
NewConstitution : DataHash → Maybe ScriptHash → GovAction
TriggerHF : ProtVer → GovAction
ChangePParams : PParamsUpdate → 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 : GovActionID

record GovVote : Set where
field gvGid : GovActionID
gvVoter : Voter
gvVote : Vote
gvAnchor : Maybe Anchor

record GovProposal : Set where
field gpAction : GovAction
gpPrevAction : GovActionID
gpPolicy : Maybe ScriptHash
gpDeposit : Coin
gpReturnAddr : RwdAddr
gpAnchor : Anchor

data GovSignal : Set where
GovSignalVote : GovVote → GovSignal
GovSignalProposal : GovProposal → GovSignal

GovState = List (Pair GovActionID GovActionState)
{-# FOREIGN GHC
type Voter = (GovRole, Credential)
type GovState = [(GovActionID, GovActionState)]
data GovAction
= NoConfidence
| NewCommittee [(Credential, Epoch)] [Credential] Rational
| NewConstitution DataHash (Maybe ScriptHash)
| TriggerHF ProtVer
| ChangePParams ()
| TreasuryWdrl [(RwdAddr, Coin)]
| Info
data Vote
= VoteYes
| VoteNo
| VoteAbstain
data GovActionState = MkGovActionState
{ gasVotes :: [(Voter, Vote)]
, gasReturnAddr :: RwdAddr
, gasExpiresIn :: Epoch
, gasAction :: GovAction
, gasPrevAction :: GovActionID
}
data GovVote = MkGovVote
{ gvGid :: GovActionID
, gvVoter :: Voter
, gvVote :: Vote
, gvAnchor :: Maybe Anchor
}
data GovProposal = MkGovProposal
{ gpAction :: GovAction
, gpPrevAction :: GovActionID
, gpPolicy :: Maybe ScriptHash
, gpDeposit :: Coin
, gpReturnAddr :: RwdAddr
, gpAnchor :: Anchor
}
data GovSignal
= GovSignalVote GovVote
| GovSignalProposal GovProposal
#-}
{-# 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) #-}
{-# COMPILE GHC GovVote = data GovVote (MkGovVote) #-}
{-# COMPILE GHC GovProposal = data GovProposal (MkGovProposal) #-}
{-# COMPILE GHC GovSignal = data GovSignal (GovSignalVote|GovSignalProposal) #-}

0 comments on commit 563477c

Please sign in to comment.