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       = ⊤
@@ -147,9 +147,9 @@ HsGovParams : GovParams
 HsGovParams = record
   { Implementation
   ; ppUpd = let open PParamsDiff in λ where
-      .UpdateT      → ⊤
-      .updateGroups → λ _ → ∅
-      .applyUpdate  → λ p _ → p
+      .UpdateT      → ℕ -- cost parameter `a`
+      .updateGroups → λ _ → ❴ EconomicGroup ❵
+      .applyUpdate  → λ p a → record p { a = a }
       .ppWF?        → ⁇ yes (λ _ h → h)
   ; ppHashingScheme = it
   }
@@ -253,6 +253,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
@@ -262,7 +267,7 @@ instance
       ; txfee  = txfee
       ; txvldt = to txvldt
       ; txsize = txsize
-      ; txid   = txid
+      ; txid   = to txid
       ; collateral = to collateral
       ; reqSigHash = to reqSigHash
       ; scriptIntHash = nothing
@@ -281,7 +286,7 @@ instance
       ; txADhash   = nothing
       ; netwrk     = nothing
       ; txsize     = txsize
-      ; txid       = txid
+      ; txid       = from txid
       ; txvote     = []
       ; txprop     = []
       ; txdonation = ε
@@ -438,8 +443,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

@@ -14,15 +14,13 @@ open import Data.Rational.Base
 
 {-# FOREIGN GHC
   import GHC.Generics (Generic)
-  import Data.TreeDiff
   import Prelude hiding (Rational)
 #-}
 
 data Empty : Set where
 
 {-# FOREIGN GHC
   data AgdaEmpty deriving (Show, Generic)
-  instance ToExpr AgdaEmpty
 #-}
 
 data ComputationResult E A : Set where
@@ -41,8 +39,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 +48,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 +64,7 @@ Datum         = ⊤
 Redeemer      = ⊤
 Anchor        = ⊤
 Network       = ⊤
-PParamsUpdate = ⊤
+PParamsUpdate = ℕ
 Script        = ⊤
 
 TxIn          = Pair TxId Ix
@@ -90,10 +88,12 @@ ProtVer = Pair ℕ ℕ
   type Coin  = Integer
   type Addr  = Integer
 
-  type TxId    = Integer
+  newtype TxId = MkTxId Integer
+    deriving (Generic, Show, Eq, Ord)
   type Ix      = Integer
   type Epoch   = Integer
   type ScriptHash    = Integer
+  type PParamsUpdate = Integer
 
   type AuxiliaryData = ()
   type DataHash      = ()
@@ -109,20 +109,19 @@ 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)
 #-}
 {-# 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 +140,6 @@ RwdAddr = Pair Network Credential
     | DRep
     | SPO
     deriving (Show, Eq, Generic)
-  instance ToExpr GovRole
 #-}
 data GovRole : Set where
   CC DRep SPO : GovRole
@@ -153,7 +151,6 @@ data GovRole : Set where
     | AbstainRep
     | NoConfidenceRep
     deriving (Show, Eq, Generic)
-  instance ToExpr VDeleg
 #-}
 data VDeleg : Set where
   CredVoter        : GovRole → Credential →  VDeleg
@@ -171,7 +168,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 +208,6 @@ record TxBody : Set where
     , scriptIntHash :: Maybe Hash
     , txcerts :: [TxCert]
     } deriving (Show, Generic)
-  instance ToExpr TxBody
 #-}
 {-# COMPILE GHC TxBody = data TxBody (MkTxBody) #-}
 
@@ -228,7 +223,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 +236,6 @@ record Tx : Set where
     , wits :: TxWitnesses
     , txAD :: Maybe AuxiliaryData
     } deriving (Show, Generic)
-  instance ToExpr Tx
 #-}
 {-# COMPILE GHC Tx = data Tx (MkTx) #-}
 
@@ -265,7 +258,7 @@ record PParams : Set where
         drepActivity        : Epoch
         ccMinSize           : ℕ
         ccMaxTermLength     : ℕ
-        costmdls            : Empty
+        costmdls            : ⊤
         prices              : ⊤
         maxTxExUnits        : ExUnits
         maxBlockExUnits     : ExUnits
@@ -292,14 +285,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 +303,6 @@ record UTxOEnv : Set where
     { slot    :: Integer
     , pparams :: PParams
     } deriving (Show, Generic)
-  instance ToExpr UTxOEnv
 #-}
 {-# COMPILE GHC UTxOEnv = data UTxOEnv (MkUTxOEnv) #-}
 
@@ -323,7 +314,6 @@ record UTxOState : Set where
     { utxo :: UTxO
     , fees :: Coin
     } deriving (Show, Generic)
-  instance ToExpr UTxOState
 #-}
 {-# COMPILE GHC UTxOState = data UTxOState (MkUTxOState) #-}
 
@@ -412,7 +402,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/Set/Theory.agda

@@ -126,3 +126,9 @@ indexedSum' f s = indexedSum ⦃ fromCommMonoid' it ⦄ f (s ᶠˢ)
 
 syntax indexedSumᵛ' (λ a → x) m = ∑[ a ← m ] x
 syntax indexedSum'  (λ a → x) m = ∑ˢ[ a ← m ] x
+
+opaque 
+  unfolding List-Model
+
+  singleton-≢-∅ : ∀ {a} {x : a} → ⦃ DecEq a ⦄ → singleton x ≢ ∅
+  singleton-≢-∅ {x = x} ()

src/Ledger/hs-src/cardano-ledger-executable-spec.cabal

@@ -53,7 +53,6 @@ library
         Lib
     build-depends:
         text,
-        ieee,
-        tree-diff
+        ieee
 -- This will be generated automatically when building with nix
     other-modules:

src/Ledger/hs-src/test/UtxowSpec.hs

@@ -42,7 +42,7 @@ a2 :: Addr
 a2 = 2
 
 initUTxO :: UTxO
-initUTxO = [ (0,  0) .-> (a0, (1000, (Nothing, Nothing))) ]
+initUTxO = [ (MkTxId 0,  0) .-> (a0, (1000, (Nothing, Nothing))) ]
 
 initState :: UTxOState
 initState = MkUTxOState {utxo = initUTxO, fees = 0}
@@ -68,12 +68,12 @@ bodyFromSimple pp stxb = let s = 5 in MkTxBody
 
 testTxBody1 :: TxBody
 testTxBody1 = bodyFromSimple initParams $ MkSimpleTxBody
-  { stxins     = [(0, 0)]
+  { stxins     = [(MkTxId 0, 0)]
   , srefInputs = []
   , stxouts    = [ 0 .-> (a0, (890, (Nothing, Nothing)))
                  , 1 .-> (a1, (100, (Nothing, Nothing))) ]
   , stxvldt    = (Nothing, Just 10)
-  , stxid      = 1
+  , stxid      = MkTxId 1
   , stxcerts   = []}
 
 testTx1 :: Tx
@@ -84,12 +84,12 @@ testTx1 = MkTx
 
 testTxBody2 :: TxBody
 testTxBody2 = bodyFromSimple initParams $ MkSimpleTxBody
-  { stxins     = [(1, 1)]
-  , srefInputs = [(1, 0)]
+  { stxins     = [(MkTxId 1, 1)]
+  , srefInputs = [(MkTxId 1, 0)]
   , stxouts    = [ 0 .-> (a2, (10, (Nothing, Nothing)))
                  , 1 .-> (a1, (80, (Nothing, Nothing))) ]
   , stxvldt    = (Nothing, Just 10)
-  , stxid      = 2
+  , stxid      = MkTxId 2
   , stxcerts   = []}
 
 testTx2 :: Tx
@@ -108,8 +108,8 @@ spec = do
   describe "utxowSteps" $
     it "results in the expected state" $
       utxowSteps initEnv initState [testTx1, testTx2] @?= Success (MkUTxOState
-        { utxo = [ (1,0) .-> (a0, (890, (Nothing, Nothing)))
-                 , (2,0) .-> (a2, (10,  (Nothing, Nothing)))
-                 , (2,1) .-> (a1, (80,  (Nothing, Nothing))) ]
+        { utxo = [ (MkTxId 1,0) .-> (a0, (890, (Nothing, Nothing)))
+                 , (MkTxId 2,0) .-> (a2, (10,  (Nothing, Nothing)))
+                 , (MkTxId 2,1) .-> (a1, (80,  (Nothing, Nothing))) ]
         , fees = 20
         })

src/MidnightExample/hs-src/midnight-example.cabal

@@ -52,7 +52,6 @@ library
         Lib
     build-depends:
         text,
-        tree-diff,
         ieee
 -- This will be generated automatically when building with nix
     other-modules: