GOV Conformance

src/Ledger/Foreign/HSLedger.agda

@@ -65,7 +65,7 @@ module Implementation where
     }) where open import Algebra.PairOp ℕ zero _≡_ _+_
   _≥ᵉ_ : ExUnits → ExUnits → Set
   _≥ᵉ_ = _≡_
-  CostModel    = ⊥
+  CostModel    = ⊤
   Language     = ⊤
   LangDepView  = ⊤
   Prices       = ⊤
@@ -142,16 +142,23 @@ HSScriptStructure = record
 instance _ = HSScriptStructure
 
 open import Ledger.PParams it it it hiding (PParams)
+open import Axiom.Set.Properties List-Model using (∉-∅)
+
+opaque 
+  unfolding List-Model
+
+  singleton-≢-∅ : ∀ {a} {x : a} → ⦃ DecEq a ⦄ → singleton x ≢ ∅
+  singleton-≢-∅ {x = x} ()
 
 HsGovParams : GovParams
 HsGovParams = record
   { Implementation
   ; ppUpd = let open PParamsDiff in λ where
-      .UpdateT                → ⊤
-      .updateGroups           → λ _ → ∅
-      .applyUpdate            → λ p _ → p
-      .ppdWellFormed          → λ _ → false
-      .ppdWellFormed⇒hasGroup → λ ()
+      .UpdateT                → ℕ -- cost parameter `a`
+      .updateGroups           → λ _ → ❴ EconomicGroup ❵
+      .applyUpdate            → λ p a → record p { a = a }
+      .ppdWellFormed          → λ _ → true
+      .ppdWellFormed⇒hasGroup → λ _ → singleton-≢-∅
       .ppdWellFormed⇒WF       → λ _ _ x → x
   ; ppHashingScheme = it
   }
@@ -255,6 +262,11 @@ instance
   Convertible-DCert : Convertible DCert F.TxCert
   Convertible-DCert = autoConvertible
 
+  Convertible-TxId : Convertible ℕ F.TxId
+  Convertible-TxId = λ where
+    .to x → record { txid = x }
+    .from → F.TxId.txid
+
   Convertible-TxBody : Convertible TxBody F.TxBody
   Convertible-TxBody = λ where
     .to txb → let open TxBody txb in record
@@ -264,7 +276,7 @@ instance
       ; txfee  = txfee
       ; txvldt = to txvldt
       ; txsize = txsize
-      ; txid   = txid
+      ; txid   = to txid
       ; collateral = to collateral
       ; reqSigHash = to reqSigHash
       ; scriptIntHash = nothing
@@ -283,7 +295,7 @@ instance
       ; txADhash   = nothing
       ; netwrk     = nothing
       ; txsize     = txsize
-      ; txid       = txid
+      ; txid       = from txid
       ; txvote     = []
       ; txprop     = []
       ; txdonation = ε
@@ -440,8 +452,8 @@ 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
+fromNeedsHash {TreasuryWdrl _} x = to 0 F., 0
+fromNeedsHash {Info} x = to 0 F., 0
 
 instance
   Convertible-GovActionState : Convertible GovActionState F.GovActionState

src/Ledger/Foreign/LedgerTypes.agda

@@ -22,7 +22,6 @@ data Empty : Set where
 
 {-# FOREIGN GHC
   data AgdaEmpty deriving (Show, Generic)
-  instance ToExpr AgdaEmpty
 #-}
 
 data ComputationResult E A : Set where
@@ -41,8 +40,6 @@ data ComputationResult E A : Set where
     return = pure
     (Success a) >>= m = m a
     (Failure e) >>= _ = Failure e
-
-  instance (ToExpr e, ToExpr a) => ToExpr (ComputationResult e a)
 #-}
 {-# COMPILE GHC ComputationResult = data ComputationResult (Success | Failure) #-}
 
@@ -52,10 +49,12 @@ HSMap : Set → Set → Set
 HSMap K V = List (Pair K V)
 Rational = Pair ℤ ℕ
 
+record TxId : Set where
+  field txid : ℕ
+
 Coin          = ℕ
 Addr          = ℕ -- just payment credential
 
-TxId          = ℕ
 Ix            = ℕ
 Epoch         = ℕ
 ScriptHash    = ℕ
@@ -66,7 +65,7 @@ Datum         = ⊤
 Redeemer      = ⊤
 Anchor        = ⊤
 Network       = ⊤
-PParamsUpdate = ⊤
+PParamsUpdate = ℕ
 Script        = ⊤
 
 TxIn          = Pair TxId Ix
@@ -94,6 +93,7 @@ ProtVer = Pair ℕ ℕ
   type Ix      = Integer
   type Epoch   = Integer
   type ScriptHash    = Integer
+  type PParamsUpdate = Integer
 
   type AuxiliaryData = ()
   type DataHash      = ()
@@ -109,20 +109,20 @@ ProtVer = Pair ℕ ℕ
   type Hash  = Integer
 
   data Tag     = Spend | Mint | Cert | Rewrd | Vote | Propose deriving (Show, Generic)
-  instance ToExpr Tag
   type RdmrPtr = (Tag, Ix)
   type ExUnits = (Integer, Integer)
   type ProtVer = (Integer, Integer)
   type GovActionID = (TxId, Integer)
+  newtype TxId = MkTxId Integer
 #-}
 {-# COMPILE GHC Tag = data Tag (Spend | Mint | Cert | Rewrd | Vote | Propose) #-}
+{-# COMPILE GHC TxId = data TxId (MkTxId) #-}
 
 {-# FOREIGN GHC
   data Credential
     = ScriptObj Integer
     | KeyHashObj Integer
     deriving (Show, Eq, Generic)
-  instance ToExpr Credential
 #-}
 data Credential : Set where
   ScriptObj  : Hash → Credential
@@ -141,7 +141,6 @@ RwdAddr = Pair Network Credential
     | DRep
     | SPO
     deriving (Show, Eq, Generic)
-  instance ToExpr GovRole
 #-}
 data GovRole : Set where
   CC DRep SPO : GovRole
@@ -153,7 +152,6 @@ data GovRole : Set where
     | AbstainRep
     | NoConfidenceRep
     deriving (Show, Eq, Generic)
-  instance ToExpr VDeleg
 #-}
 data VDeleg : Set where
   CredVoter        : GovRole → Credential →  VDeleg
@@ -171,7 +169,6 @@ data VDeleg : Set where
     | DeRegDRep Credential
     | CCRegHot Credential (Maybe Credential)
     deriving (Show, Eq, Generic)
-  instance ToExpr TxCert
 #-}
 data TxCert : Set where
   Delegate    : Credential → Maybe VDeleg → Maybe Credential → Coin → TxCert
@@ -212,7 +209,6 @@ record TxBody : Set where
     , scriptIntHash :: Maybe Hash
     , txcerts :: [TxCert]
     } deriving (Show, Generic)
-  instance ToExpr TxBody
 #-}
 {-# COMPILE GHC TxBody = data TxBody (MkTxBody) #-}
 
@@ -228,7 +224,6 @@ record TxWitnesses : Set where
     , txdats  :: [(DataHash, Datum)]
     , txrdmrs :: [(RdmrPtr, (Redeemer, ExUnits))]
     } deriving (Show, Generic)
-  instance ToExpr TxWitnesses
 #-}
 {-# COMPILE GHC TxWitnesses = data TxWitnesses (MkTxWitnesses) #-}
 
@@ -242,7 +237,6 @@ record Tx : Set where
     , wits :: TxWitnesses
     , txAD :: Maybe AuxiliaryData
     } deriving (Show, Generic)
-  instance ToExpr Tx
 #-}
 {-# COMPILE GHC Tx = data Tx (MkTx) #-}
 
@@ -265,7 +259,7 @@ record PParams : Set where
         drepActivity        : Epoch
         ccMinSize           : ℕ
         ccMaxTermLength     : ℕ
-        costmdls            : Empty
+        costmdls            : ⊤
         prices              : ⊤
         maxTxExUnits        : ExUnits
         maxBlockExUnits     : ExUnits
@@ -292,14 +286,13 @@ record PParams : Set where
     , drepActivity        :: Epoch
     , ccMinSize           :: Integer
     , ccMaxTermLength     :: Integer
-    , costmdls            :: AgdaEmpty
+    , costmdls            :: ()
     , prices              :: ()
     , maxTxExUnits        :: ExUnits
     , maxBlockExUnits     :: ExUnits
     , coinsPerUTxOWord    :: Coin
     , maxCollateralInputs :: Integer
     } deriving (Show, Generic)
-  instance ToExpr PParams
 #-}
 {-# COMPILE GHC PParams = data PParams (MkPParams) #-}
 
@@ -311,7 +304,6 @@ record UTxOEnv : Set where
     { slot    :: Integer
     , pparams :: PParams
     } deriving (Show, Generic)
-  instance ToExpr UTxOEnv
 #-}
 {-# COMPILE GHC UTxOEnv = data UTxOEnv (MkUTxOEnv) #-}
 
@@ -323,7 +315,6 @@ record UTxOState : Set where
     { utxo :: UTxO
     , fees :: Coin
     } deriving (Show, Generic)
-  instance ToExpr UTxOState
 #-}
 {-# COMPILE GHC UTxOState = data UTxOState (MkUTxOState) #-}
 
@@ -412,7 +403,7 @@ GovState = List (Pair GovActionID GovActionState)
     | NewCommittee [(Credential, Epoch)] [Credential] Rational
     | NewConstitution DataHash (Maybe ScriptHash)
     | TriggerHF ProtVer
-    | ChangePParams ()
+    | ChangePParams PParamsUpdate
     | TreasuryWdrl [(RwdAddr, Coin)]
     | Info
 

src/Ledger/PParams.lagda

@@ -168,6 +168,8 @@ instance
     ((quote PoolThresholds , DecEq-PoolThresholds) ∷ [])
   unquoteDecl DecEq-PParams        = derive-DecEq
     ((quote PParams , DecEq-PParams) ∷ [])
+  unquoteDecl DecEq-PParamGroup    = derive-DecEq
+    ((quote PParamGroup , DecEq-PParamGroup) ∷ [])
 
 instance
   pvCanFollow? : ∀ {pv} {pv'} → Dec (pvCanFollow pv pv')