Compiles

IntersectMBO · May 17, 2024 · 3544ff6 · 3544ff6
1 parent 355f7ba
commit 3544ff6
Show file tree

Hide file tree

Showing 2 changed files with 72 additions and 26 deletions.
diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda
@@ -207,8 +207,10 @@ open import Ledger.GovernanceActions it using (Vote; GovVote; GovProposal; GovAc
 open import Ledger.GovernanceActions.Properties it
 open import Ledger.Ledger it it
 open import Ledger.Ledger.Properties it it
---open import Ledger.Epoch it it
---open import Ledger.Epoch.Properties it it
+open import Ledger.Epoch it it using (NewEpochEnv; NewEpochState; EpochState)
+open import Ledger.Epoch.Properties it it
+open import Ledger.Chain it it
+open import Ledger.Chain.Properties it it
 
 open import Data.Rational
 
@@ -571,17 +573,27 @@ instance
   Convertible-LState : Convertible LState F.LState
   Convertible-LState = autoConvertible
 
-  --Convertible-NewEpochEnv : Convertible NewEpochEnv F.NewEpochEnv
-  --Convertible-NewEpochEnv = autoConvertible
+  Convertible-NewEpochEnv : Convertible NewEpochEnv F.NewEpochEnv
+  Convertible-NewEpochEnv = autoConvertible
 
   Convertible-Acnt : Convertible Acnt F.Acnt
-  Convertible-Acnt = autoConvertible
+  Convertible-Acnt = λ where
+    .to record { treasury = treasury ; reserves = reserves } →
+      record { treasury = treasury ; reserves = reserves }
+    .from record { treasury = treasury ; reserves = reserves } →
+      record { treasury = treasury ; reserves = reserves }
 
   Convertible-EpochState : Convertible EpochState F.EpochState
   Convertible-EpochState = autoConvertible
 
-  --Convertible-NewEpochState : Convertible NewEpochState F.NewEpochState
-  --Convertible-NewEpochState = autoConvertible
+  Convertible-NewEpochState : Convertible NewEpochState F.NewEpochState
+  Convertible-NewEpochState = autoConvertible
+
+  Convertible-ChainState : Convertible ChainState F.ChainState
+  Convertible-ChainState = autoConvertible
+
+  Convertible-Block : Convertible Block F.Block
+  Convertible-Block = autoConvertible
 
 utxo-step : F.UTxOEnv → F.UTxOState → F.Tx → F.ComputationResult String F.UTxOState
 utxo-step = to (compute Computational-UTXO)
@@ -623,7 +635,22 @@ ledger-step = to (compute Computational-LEDGER)
 
 {-# COMPILE GHC ledger-step as ledgerStep #-}
 
---newepoch-step : F.NewEpochEnv → F.NewEpochState → F.Epoch → F.ComputationResult ⊥ F.NewEpochState
---newepoch-step = to (compute Computational-NEWEPOCH)
---
---{-# COMPILE GHC newepoch-step as newEpochStep #-}
+ledgers-step : F.LEnv → F.LState → List F.Tx → F.ComputationResult String F.LState
+ledgers-step = to (compute Computational-LEDGERS)
+
+{-# COMPILE GHC ledgers-step as ledgersStep #-}
+
+epoch-step : F.NewEpochEnv → F.EpochState → F.Epoch → F.ComputationResult F.Empty F.EpochState
+epoch-step = to (compute Computational-EPOCH)
+
+{-# COMPILE GHC epoch-step as epochStep #-}
+
+newepoch-step : F.NewEpochEnv → F.NewEpochState → F.Epoch → F.ComputationResult F.Empty F.NewEpochState
+newepoch-step = to (compute Computational-NEWEPOCH)
+
+{-# COMPILE GHC newepoch-step as newEpochStep #-}
+
+chain-step : ⊤ → F.ChainState → F.Block → F.ComputationResult String F.ChainState
+chain-step = to (compute Computational-CHAIN)
+
+{-# COMPILE GHC chain-step as chainStep #-}
diff --git a/src/Ledger/Foreign/LedgerTypes.agda b/src/Ledger/Foreign/LedgerTypes.agda
@@ -105,6 +105,7 @@ ProtVer = Pair ℕ ℕ
   type Epoch   = Integer
   type ScriptHash    = Integer
   type PParamsUpdate = Integer
+  type Slot = Integer
 
   type AuxiliaryData = ()
   type DataHash      = ()
@@ -566,9 +567,9 @@ record RatifyState : Set where
         delay           : Bool
 {-# FOREIGN GHC
   data RatifyState = MkRatifyState
-   { es      :: EnactState
-   , removed :: HSSet (GovActionID, GovActionState)
-   , delay   :: Bool
+   { rsEnactState :: EnactState
+   , rsRemoved    :: HSSet (GovActionID, GovActionState)
+   , rsDelay      :: Bool
    }
 #-}
 {-# COMPILE GHC RatifyState = data RatifyState (MkRatifyState) #-}
@@ -580,10 +581,10 @@ record LEnv : Set where
         enactState  : EnactState
 {-# FOREIGN GHC
   data LedgerEnv = MkLedgerEnv
-    { slot       :: Slot
-    , ppolicy    :: Maybe ScriptHash
-    , pparams    :: PParams
-    , enactState :: EnactState
+    { leSlot       :: Slot
+    , lePPolicy    :: Maybe ScriptHash
+    , lePParams    :: PParams
+    , leEnactState :: EnactState
     }
 #-}
 {-# COMPILE GHC LEnv = data LedgerEnv (MkLedgerEnv) #-}
@@ -618,8 +619,7 @@ record Acnt : Set where
   field treasury reserves : Coin
 {-# FOREIGN GHC
   data Acnt = MkAcnt
-    { field :: Coin
-    , treasury :: Coin
+    { treasury :: Coin
     , reserves :: Coin
     }
 #-}
@@ -639,10 +639,10 @@ record EpochState : Set where
         fut        : RatifyState
 {-# FOREIGN GHC
   data EpochState = MkEpochState
-    { acnt :: Acnt
-    , ls   :: LState
-    , es   :: EnactState
-    , fut  :: RatifyState
+    { esAcnt       :: Acnt
+    , esLState     :: LedgerState
+    , esEnactState :: EnactState
+    , esFut        :: RatifyState
     }
 #-}
 {-# COMPILE GHC EpochState = data EpochState (MkEpochState) #-}
@@ -652,9 +652,28 @@ record NewEpochState : Set where
         epochState  : EpochState
 {-# FOREIGN GHC
   data NewEpochState = MkNewEpochState
-    { lastEpoch   : Epoch
-    , epochState  : EpochState
+    { lastEpoch  :: Epoch
+    , epochState :: EpochState
     }
 #-}
 {-# COMPILE GHC NewEpochState = data NewEpochState (MkNewEpochState) #-}
 
+record ChainState : Set where
+  field csNewEpochState : NewEpochState
+{-# FOREIGN GHC
+  newtype ChainState = MkChainState
+    { csNewEpochState :: NewEpochState
+    }
+#-}
+{-# COMPILE GHC ChainState = data ChainState (MkChainState) #-}
+
+record Block : Set where
+  field blockTxs : List Tx
+        blockSlot : Slot
+{-# FOREIGN GHC
+  data Block = MkBlock
+    { blockTxs :: [Tx]
+    , blockSlot :: Slot
+    }
+#-}
+{-# COMPILE GHC Block = data Block (MkBlock) #-}