WIP

src/Ledger/Foreign/HSLedger/Address.agda

@@ -2,6 +2,10 @@ module Ledger.Foreign.HSLedger.Address where
 
 open import Ledger.Foreign.HSLedger.BaseTypes
 
+{-# FOREIGN GHC
+  import qualified MAlonzo.Code.Ledger.Foreign.HSTypes
+#-}
+
 instance
   HsTy-Credential = autoHsType Credential
   Conv-Credential = autoConvert Credential
@@ -17,3 +21,4 @@ instance
 
 unquoteDecl = do
   hsTypeAlias Addr
+  hsTypeAlias Wdrl

src/Ledger/Foreign/HSLedger/Certs.agda

@@ -1,12 +1,12 @@
 module Ledger.Foreign.HSLedger.Certs where
 
 open import Ledger.Foreign.HSLedger.Address
-open import Ledger.Foreign.HSLedger.BaseTypes hiding (DState; CertEnv; GState)
+open import Ledger.Foreign.HSLedger.BaseTypes hiding (DState; CertEnv; GState; CertState)
 open import Ledger.Foreign.HSLedger.Gov
 open import Ledger.Foreign.HSLedger.PParams
 
 open import Ledger.Certs.Properties govStructure
-open import Ledger.Certs.Haskell govStructure using (⟦_,_,_,_⟧ᵈ; DState; GState)
+open import Ledger.Certs.Haskell govStructure using (⟦_,_,_,_⟧ᵈ; DState; GState; CertState)
 
 open import Ledger.Certs.Haskell.Properties govStructure
   renaming ( Computational-DELEG   to Computational-DELEG'
@@ -65,6 +65,9 @@ instance
     • fieldPrefix "gs"
   Conv-GState = autoConvert GState
 
+  HsTy-CertState' = autoHsType CertState ⊣ withConstructor "MkCertState"
+  Conv-CertState' = autoConvert CertState
+
 -- deleg-step : HsType (DelegEnv → DState → DCert → ComputationResult String DState)
 -- deleg-step = to (compute Computational-DELEG)
 

src/Ledger/Foreign/HSLedger/Core.agda

@@ -56,7 +56,7 @@ module Implementation where
   toData : ∀ {A : Type} → A → Data
   toData _ = tt
 
-  PlutusScript = ⊤
+  PlutusScript = ScriptHash
   ExUnits      = ℕ × ℕ
   ExUnit-CommutativeMonoid = IsCommutativeMonoid' 0ℓ 0ℓ ExUnits ∋ (toCommMonoid' record
     { Carrier = ExUnits
@@ -132,12 +132,9 @@ instance
     { hashRespectsUnion = hashRespectsUnion
     ; ps = HSP2ScriptStructure }
     where
-    postulate
-      instance Hashable-Timelock : Hashable Timelock ℕ
-
-      hashRespectsUnion : ∀ {A B ℍ}
-        → Hashable A ℍ → Hashable B ℍ
-        → Hashable (A ⊎ B) ℍ
+    hashRespectsUnion : {A B Hash : Type} → Hashable A Hash → Hashable B Hash → Hashable (A ⊎ B) Hash
+    hashRespectsUnion record { hash = hash₁ } record { hash = hash₂ } =
+      record { hash = λ where (inj₁ x) → hash₁ x; (inj₂ y) → hash₂ y }
 
     HSP2ScriptStructure : PlutusStructure
     HSP2ScriptStructure = record
@@ -217,3 +214,14 @@ instance
     }
 
 open import Ledger.Address Network KeyHash ScriptHash using () public
+
+-- * Aliases
+unquoteDecl = do
+  hsTypeAlias Coin
+  hsTypeAlias ExUnits
+  hsTypeAlias Data
+  hsTypeAlias Redeemer
+  hsTypeAlias AuxiliaryData
+  hsTypeAlias Epoch
+  hsTypeAlias ScriptHash
+  hsTypeAlias GovActionID

src/Ledger/Foreign/HSLedger/Gov.agda

@@ -110,6 +110,10 @@ instance
   HsTy-GovActionState = MkHsType GovActionState (HsType GovActionState')
   Conv-GovActionState = mkGovActionState' ⨾ Conv-GovActionState'
 
+unquoteDecl = do
+  hsTypeAlias Voter
+  hsTypeAlias GovState
+
 -- Computational function
 
 gov-step : HsType (GovEnv → GovState → List (GovVote ⊎ GovProposal) → ComputationResult String GovState)

src/Ledger/Foreign/HSLedger/Ledger.agda

@@ -2,6 +2,7 @@ module Ledger.Foreign.HSLedger.Ledger where
 
 open import Ledger.Foreign.HSLedger.Address
 open import Ledger.Foreign.HSLedger.BaseTypes
+  hiding (CertState)
 open import Ledger.Foreign.HSLedger.Certs
 open import Ledger.Foreign.HSLedger.Enact
 open import Ledger.Foreign.HSLedger.Gov
@@ -10,19 +11,21 @@ open import Ledger.Foreign.HSLedger.Transaction
 open import Ledger.Foreign.HSLedger.Utxo
 
 open import Ledger.Ledger it it
-open import Ledger.Ledger.Properties it it
+  hiding (LState)
+open import Ledger.Ledger.Haskell it it
+open import Ledger.Ledger.Haskell.Properties it it
 
 instance
   -- These are "duplicate" because of the duplicate STSs
-  HsTy-GState' = autoHsType GState ⊣ withConstructor "MkGState"
+  HsTy-GState' = autoHsType GState
+    ⊣ withName "GState'"
+    • withConstructor "MkGState'"
+    • fieldPrefix "gs'"
   Conv-GState' = autoConvert GState
 
   HsTy-DState' = autoHsType DState ⊣ withConstructor "MkDState"
   Conv-DState' = autoConvert DState
 
-  HsTy-CertState' = autoHsType CertState ⊣ withConstructor "MkCertState"
-  Conv-CertState' = autoConvert CertState
-
   HsTy-LEnv = autoHsType LEnv ⊣ withConstructor "MkLEnv"
                               • fieldPrefix "le"
   Conv-LEnv = autoConvert LEnv

src/Ledger/Foreign/HSLedger/Transaction.agda

@@ -17,6 +17,9 @@ instance
   {-# TERMINATING #-}
   Conv-Timelock = autoConvert Timelock
 
+  HsTy-HashedTimelock = autoHsType HashedTimelock ⊣ withConstructor "MkHashedTimelock"
+  Conv-HashedTimelock = autoConvert HashedTimelock
+
   HsTy-TxWitnessess = autoHsType TxWitnesses ⊣ withConstructor "MkTxWitnesses"
   Conv-TxWitnessess = autoConvert TxWitnesses
 
@@ -37,3 +40,4 @@ unquoteDecl = do
   hsTypeAlias DataHash ⊣ withName "DataHash"
   hsTypeAlias Value
   hsTypeAlias TxOut
+  hsTypeAlias RdmrPtr

src/Ledger/Gov.lagda

@@ -365,3 +365,4 @@ and some conditions depending on the type of the action:
   epoch are allowed, and candidates cannot be added and removed at the same time;
 \item and we check the validity of hard-fork actions via \validHFAction.
 \end{itemize}
+

src/Ledger/Ledger/Haskell.agda

@@ -0,0 +1,59 @@
+{-# OPTIONS --safe #-}
+
+open import Ledger.Prelude
+open import Ledger.Types.GovStructure
+open import Ledger.Transaction
+open import Ledger.Abstract
+
+module Ledger.Ledger.Haskell
+  (txs : _) (open TransactionStructure txs using (govStructure; Tx; TxBody; epoch))
+  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
+  where
+
+open import Ledger.Utxo txs abs
+open import Ledger.Utxow txs abs
+open import Ledger.Gov txs
+open import Ledger.Certs.Haskell govStructure
+open import Ledger.Ledger txs abs
+  using (LEnv; txgov)
+open import Ledger.Types.Epoch
+
+record LState : Type where
+  constructor ⟦_,_,_⟧ˡ
+  field
+    utxoSt     : UTxOState
+    govSt      : GovState
+    certState  : CertState
+
+private variable
+  Γ : LEnv
+  s s' s'' : LState
+  utxoSt' : UTxOState
+  govSt' : GovState
+  certState' : CertState
+  tx : Tx
+
+open Tx
+
+data
+  _⊢_⇀⦇_,LEDGER⦈_ : LEnv → LState → Tx → LState → Type
+  where
+  LEDGER-V : let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ in
+    ∙  isValid tx ≡ true
+    ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
+    ∙  ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
+    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState ⟧ᵍ ⊢ govSt ⇀⦇ txgov txb ,GOV⦈ govSt'
+       ────────────────────────────────
+       Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState' ⟧ˡ
+
+  LEDGER-I : let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ in
+    ∙  isValid tx ≡ false
+    ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
+       ────────────────────────────────
+       Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt , certState ⟧ˡ
+
+pattern LEDGER-V⋯ w x y z = LEDGER-V (w , x , y , z)
+pattern LEDGER-I⋯ y z     = LEDGER-I (y , z)
+
+_⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type
+_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,LEDGER⦈_

src/Ledger/Ledger/Haskell/Properties.agda

@@ -0,0 +1,75 @@
+{-# OPTIONS --safe #-}
+
+open import Ledger.Prelude
+open import Ledger.Transaction
+open import Ledger.Abstract
+
+module Ledger.Ledger.Haskell.Properties
+  (txs : _) (open TransactionStructure txs using (Tx; TxBody; epoch; govStructure))
+  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
+  where
+
+open import Ledger.Ledger.Haskell txs abs
+open import Ledger.Certs.Haskell govStructure
+open import Ledger.Certs.Haskell.Properties govStructure
+open import Ledger.Utxow txs abs
+open import Ledger.Utxow.Properties txs abs
+open import Ledger.Gov txs
+open import Ledger.Gov.Properties txs
+open import Ledger.Ledger txs abs
+  using (LEnv; ⟦_,_,_,_,_⟧ˡᵉ; txgov)
+open import Ledger.Utxo txs abs
+open import Ledger.Utxo.Properties txs abs
+open import Data.Bool.Properties using (¬-not)
+
+instance
+  _ = Monad-ComputationResult
+
+  Computational-LEDGER : Computational _⊢_⇀⦇_,LEDGER⦈_ String
+  Computational-LEDGER = record {go}
+    where
+    open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete)
+    computeUtxow = comp {STS = _⊢_⇀⦇_,UTXOW⦈_}
+    computeCerts = comp {STS = _⊢_⇀⦇_,CERTS⦈_}
+    computeGov   = comp {STS = _⊢_⇀⦇_,GOV⦈_}
+
+    module go
+      (Γ : LEnv)   (let ⟦ slot , ppolicy , pparams , enactState , _ ⟧ˡᵉ = Γ)
+      (s : LState) (let ⟦ utxoSt , govSt , certSt ⟧ˡ = s)
+      (tx : Tx)    (let open Tx tx renaming (body to txb); open TxBody txb)
+      where
+      utxoΓ = UTxOEnv ∋ record { LEnv Γ }
+      certΓ = CertEnv ∋ ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ
+      govΓ  = GovEnv  ∋ ⟦ txid , epoch slot , pparams , ppolicy , enactState ⟧ᵍ
+
+      computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s')
+      computeProof = case isValid ≟ true of λ where
+        (yes p) → do
+          (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
+          (certSt' , certStep) ← computeCerts certΓ certSt txcerts
+          (govSt'  , govStep)  ← computeGov   govΓ  govSt  (txgov txb)
+          success (_ , LEDGER-V⋯ p utxoStep certStep govStep)
+        (no ¬p) → do
+          (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
+          success (_ , LEDGER-I⋯ (¬-not ¬p) utxoStep)
+
+      completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s'
+      completeness ⟦ utxoSt' , govSt' , certState' ⟧ˡ (LEDGER-V⋯ v utxoStep certStep govStep)
+        with isValid ≟ true
+      ... | no ¬v = contradiction v ¬v
+      ... | yes refl
+        with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep
+      ... | success (utxoSt' , _) | refl
+        with computeCerts certΓ certSt txcerts | complete _ _ _ _ certStep
+      ... | success (certSt' , _) | refl
+        with computeGov govΓ govSt (txgov txb) | complete govΓ _ _ _ govStep
+      ... | success (govSt' , _) | refl = refl
+      completeness ⟦ utxoSt' , govSt' , certState' ⟧ˡ (LEDGER-I⋯ i utxoStep)
+        with isValid ≟ true
+      ... | yes refl = case i of λ ()
+      ... | no ¬v
+        with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep
+      ... | success (utxoSt' , _) | refl = refl
+
+Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String
+Computational-LEDGERS = it

src/Ledger/Script.lagda

@@ -152,15 +152,25 @@ instance
         (RequireTimeExpire a) → mapDec evalTEx evalTEx˘ dec
         (RequireMOf m xs)     → mapDec evalMOf evalMOf˘ (MOf-go? m xs)
 
-P1ScriptStructure-TL : ⦃ Hashable Timelock ScriptHash ⦄ → P1ScriptStructure
+record HashedTimelock : Type where
+  field
+    script : Timelock
+    h : ScriptHash
+
+unquoteDecl DecEq-HashedTimelock = derive-DecEq ((quote HashedTimelock , DecEq-HashedTimelock) ∷ [])
+instance
+  Hashable-HashedTimelock : Hashable HashedTimelock ScriptHash
+  Hashable-HashedTimelock = record { hash = HashedTimelock.h }
+
+P1ScriptStructure-TL : P1ScriptStructure
 P1ScriptStructure-TL = record
-  { P1Script = Timelock
-  ; validP1Script = evalTimelock }
+  { P1Script = HashedTimelock
+  ; validP1Script = λ kh I tl → evalTimelock kh I (tl .HashedTimelock.script)
+  }
 
 record ScriptStructure : Type₁ where
   field hashRespectsUnion :
           {A B Hash : Type} → Hashable A Hash → Hashable B Hash → Hashable (A ⊎ B) Hash
-        ⦃ Hash-Timelock ⦄ : Hashable Timelock ScriptHash
 
   p1s : P1ScriptStructure
   p1s = P1ScriptStructure-TL

src/Ledger/ScriptValidation.agda

@@ -180,5 +180,5 @@ open Tx
 evalScripts : Tx → List (Script × List Data × ExUnits × CostModel) → Bool
 evalScripts tx [] = true
 evalScripts tx ((inj₁ tl , d , eu , cm) ∷ Γ) =
-  ¿ evalTimelock (reqSigHash (body tx)) (txvldt (body tx)) tl ¿ᵇ ∧ evalScripts tx Γ
+  ¿ evalTimelock (reqSigHash (body tx)) (txvldt (body tx)) (tl .HashedTimelock.script) ¿ᵇ ∧ evalScripts tx Γ
 evalScripts tx ((inj₂ ps , d , eu , cm) ∷ Γ) = ⟦ ps ⟧, cm , eu , d ∧ evalScripts tx Γ

src/Ledger/hs-src/Lib.hs

@@ -4,14 +4,18 @@ module Lib
   ) where
 
 import MAlonzo.Code.Ledger.Foreign.HSTypes              as X
-  (HSSet(..), HSMap(..), ComputationResult(..))
+  (HSSet(..), HSMap(..), ComputationResult(..), Rational(..))
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Address     as X
-  (Credential(..), BaseAddr(..), BootstrapAddr(..), RwdAddr(..), Addr)
+  ( Credential(..), BaseAddr(..), BootstrapAddr(..), RwdAddr(..)
+  , Addr, Wdrl)
 import MAlonzo.Code.Ledger.Foreign.HSLedger.PParams     as X
   (DrepThresholds(..), PoolThresholds(..), Acnt(..), PParams(..), PParamsUpdate(..))
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Transaction as X
-  ( Tag(..), Timelock(..), TxWitnesses(..), TxBody(..), Tx(..), TxId, Ix, TxIn, P1Script, P2Script
-  , Script, Datum, DataHash, Value, TxOut)
+  ( Tag(..), Timelock(..), TxWitnesses(..), TxBody(..)
+  , Tx(..), TxId, Ix, TxIn, P1Script, P2Script, Script
+  , Datum, DataHash, Value, TxOut, HashedTimelock(..)
+  , RdmrPtr
+  )
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Cert        as X
   (certStep', certsStep')
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Chain       as X
@@ -25,12 +29,16 @@ import MAlonzo.Code.Ledger.Foreign.HSLedger.Epoch       as X
   (Snapshot(..), Snapshots(..), EpochState(..), epochStep)
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Gov         as X
   ( GovRole(..), Anchor(..), VDeleg(..), Vote(..), GovVote(..), GovEnv(..), GovProposal(..)
-  , GovActionState(..), govStep)
+  , GovActionState(..), govStep, Voter, GovState)
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Ledger      as X
-  (LEnv(..), LState(..), ledgerStep, CertState(..), DState(..))
+  ( LEnv(..), LState(..), ledgerStep, CertState(..), DState(..)
+  , GState'(..))
 import MAlonzo.Code.Ledger.Foreign.HSLedger.NewEpoch    as X
   (NewEpochState(..), newEpochStep, HsRewardUpdate(..))
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Ratify      as X
   (StakeDistrs(..), RatifyEnv(..), RatifyState(..), ratifyStep)
 import MAlonzo.Code.Ledger.Foreign.HSLedger.Utxo        as X
   (UTxOEnv(..), UTxOState(..), UTxO, utxoStep, utxowStep)
+import MAlonzo.Code.Ledger.Foreign.HSLedger.Core        as X
+  ( Coin, ExUnits, Redeemer, AuxiliaryData, Epoch
+  , ScriptHash, GovActionID)

src/ScriptVerification/LedgerImplementation.agda

@@ -123,17 +123,12 @@ instance _ = SVCrypto
 
 open import Ledger.Script it it
 
-
-
 SVScriptStructure : ScriptStructure
 SVScriptStructure = record
   { hashRespectsUnion = hashRespectsUnion
-  ; ps = SVP2ScriptStructure }
+  ; ps = SVP2ScriptStructure
+  }
   where
-
-    instance Hashable-Timelock : Hashable Timelock ℕ
-             Hashable-Timelock = record { hash = λ x → 0 }
-
     instance Hashable-PlutusScript : Hashable Implementation.PlutusScript ℕ
              Hashable-PlutusScript = record { hash = λ x → proj₁ x }