Dijkstra: nested transactions (first phase)

build-tools/static/md/mkdocs/includes/links.md

@@ -11,6 +11,7 @@
 [CERTS]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system
 [CERTS rules]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system
 [CHAIN]: Ledger.Conway.Specification.Chain.md#chain-transition-system
+[CIPs]: https://github.com/cardano-foundation/CIPs
 [DELEG]: Ledger.Conway.Specification.Certs.md#auxiliary-deleg-transition-system
 [ENACT]: Ledger.Conway.Specification.Enact.md#enact-transition-system
 [EPOCH]: Ledger.Conway.Specification.Epoch.md#epoch-transition-system
@@ -70,3 +71,6 @@
 [Epoch.Properties.ConstRwds]: Ledger.Conway.Specification.Epoch.Properties.ConstRwds.md
 [Epoch.Properties.NoPropSameDReps]: Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps.md
 [Certs.Properties.VoteDelegsVDeleg]: Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md
+
+[Transactions]: Ledger.Dijkstra.Specification.Transaction.md##sec:transactions
+[Transaction Levels]: Ledger.Dijkstra.Specification.Transaction.md##sec:transaction-levels

src/Ledger.agda

@@ -3,3 +3,4 @@ module Ledger where
 import Ledger.Introduction
 import Ledger.PreConway
 import Ledger.Conway
+import Ledger.Dijkstra

src/Ledger/Conway/Specification/Gov/Actions.lagda

@@ -244,11 +244,14 @@ record GovVote : Type where
     vote        : Vote
     anchor      : Maybe Anchor
 
+Policy : Type
+Policy = Maybe ScriptHash
+
 record GovProposal : Type where
   field
     action      : GovAction
     prevAction  : NeedsHash (gaType action)
-    policy      : Maybe ScriptHash
+    policy      : Policy
     deposit     : Coin
     returnAddr  : RwdAddr
     anchor      : Anchor
@@ -268,7 +271,28 @@ record GovActionState : Type where
     prevAction  : NeedsHash (gaType action)
 \end{code}
 \begin{code}[hide]
+record HasGovVoter {a} (A : Type a) : Type a where
+  field GovVoterOf : A → GovVoter
+open HasGovVoter ⦃...⦄ public
+
+record HasVote {a} (A : Type a) : Type a where
+  field VoteOf : A → Vote
+open HasVote ⦃...⦄ public
+
+record HasPolicy {a} (A : Type a) : Type a where
+  field PolicyOf : A → Policy
+open HasPolicy ⦃...⦄ public
+
 instance
+  HasGovVoter-GovVote : HasGovVoter GovVote
+  HasGovVoter-GovVote .GovVoterOf = GovVote.voter
+
+  HasVote-GovVote : HasVote GovVote
+  HasVote-GovVote .VoteOf = GovVote.vote
+
+  HasPolicy-GovProposal : HasPolicy GovProposal
+  HasPolicy-GovProposal .PolicyOf = GovProposal.policy
+
   HasGovAction-GovProposal : HasGovAction GovProposal
   HasGovAction-GovProposal .GovActionOf = GovProposal.action
 

src/Ledger/Dijkstra.agda

@@ -0,0 +1,8 @@
+module Ledger.Dijkstra where
+
+--- Cardano ledger in the Dijkstra era
+import Ledger.Dijkstra.Specification
+
+-- TODO:
+-- import Ledger.Dijkstra.Conformance       -- Conformance test reconciliation
+-- import Ledger.Dijkstra.Foreign.HSLedger  -- Haskell code extraction

src/Ledger/Dijkstra/Specification.lagda.md

@@ -0,0 +1,16 @@
+```agda
+{-# OPTIONS --safe #-}
+module Ledger.Dijkstra.Specification where
+
+import Ledger.Core.Specification.Address renaming (RwdAddr to RewardAddress)
+import Ledger.Core.Specification.Epoch
+
+import Ledger.Dijkstra.Specification.Certs
+import Ledger.Dijkstra.Specification.Gov.Base
+import Ledger.Dijkstra.Specification.Gov.Actions
+import Ledger.Dijkstra.Specification.PParams
+import Ledger.Dijkstra.Specification.Script
+import Ledger.Dijkstra.Specification.Script.Validation
+import Ledger.Dijkstra.Specification.TokenAlgebra.Base
+import Ledger.Dijkstra.Specification.Transaction
+```

src/Ledger/Dijkstra/Specification/Abstract.lagda.md

@@ -0,0 +1,28 @@
+```agda
+{-# OPTIONS --safe #-}
+
+open import Ledger.Prelude
+open import Ledger.Dijkstra.Specification.Transaction
+
+module Ledger.Dijkstra.Specification.Abstract (txs : TransactionStructure) where
+
+open TransactionStructure txs
+open import Ledger.Dijkstra.Specification.Certs govStructure
+
+record indexOf : Type where
+  field
+    indexOfDCert    : DCert → List DCert → Maybe Ix
+    indexOfRwdAddr  : RewardAddress → Withdrawals → Maybe Ix
+    indexOfTxIn     : TxIn → ℙ TxIn → Maybe Ix
+    indexOfPolicyId : ScriptHash → ℙ ScriptHash → Maybe Ix
+    indexOfVote     : GovVoter → List GovVoter → Maybe Ix
+    indexOfProposal : GovProposal → List GovProposal → Maybe Ix
+    indexOfGuard    : TxId × ScriptHash → ℙ (TxId × ScriptHash) → Maybe Ix
+
+record AbstractFunctions : Type where
+  field txScriptFee     : Prices → ExUnits → Fees
+        serializedSize  : Value → MemoryEstimate
+        indexOfImp      : indexOf
+        runPLCScript    : CostModel → P2Script → ExUnits → List Data → Bool
+        scriptSize      : Script → ℕ
+```

src/Ledger/Dijkstra/Specification/Certs.lagda.md

@@ -0,0 +1,14 @@
+---
+source_branch: master
+source_path: src/Ledger/Dijkstra/Specification/Certs.lagda.md
+---
+```agda
+{-# OPTIONS --safe #-}
+open import Ledger.Conway.Specification.Gov.Base
+  using (GovStructure)
+
+module Ledger.Dijkstra.Specification.Certs
+  (gs : GovStructure) where
+
+open import Ledger.Conway.Specification.Certs gs public
+```

src/Ledger/Dijkstra/Specification/Gov/Actions.lagda.md

@@ -0,0 +1,13 @@
+---
+source_branch: master
+source_path: src/Ledger/Dijkstra/Specification/Gov/Actions.lagda.md
+---
+```agda
+{-# OPTIONS --safe #-}
+open import Ledger.Conway.Specification.Gov.Base
+  using (GovStructure)
+module Ledger.Dijkstra.Specification.Gov.Actions
+  (gs : GovStructure) where
+
+open import Ledger.Conway.Specification.Gov.Actions gs public
+```

src/Ledger/Dijkstra/Specification/Gov/Base.lagda.md

@@ -0,0 +1,10 @@
+---
+source_branch: master
+source_path: src/Ledger/Dijkstra/Specification/Gov/Base.lagda.md
+---
+```agda
+{-# OPTIONS --safe #-}
+module Ledger.Dijkstra.Specification.Gov.Base where
+
+open import Ledger.Conway.Specification.Gov.Base public
+```

src/Ledger/Dijkstra/Specification/PParams.lagda.md

@@ -0,0 +1,21 @@
+---
+source_branch: master
+source_path: src/Ledger/Dijkstra/Specification/PParams.lagda.md
+---
+```agda
+{-# OPTIONS --safe #-}
+open import Ledger.Core.Specification.Crypto
+  using (CryptoStructure)
+open import Ledger.Dijkstra.Specification.Script
+  using (ScriptStructure)
+open import Ledger.Core.Specification.Epoch
+  using (EpochStructure)
+
+module Ledger.Dijkstra.Specification.PParams
+  (crypto : CryptoStructure )
+  (es     : EpochStructure)
+  (ss     : ScriptStructure crypto es)
+  where
+
+open import Ledger.Conway.Specification.PParams crypto es ss public
+```

src/Ledger/Dijkstra/Specification/Script.lagda.md

@@ -0,0 +1,16 @@
+---
+source_branch: master
+source_path: src/Ledger/Dijkstra/Specification/Script.lagda.md
+---
+```agda
+{-# OPTIONS --safe #-}
+
+open import Ledger.Core.Specification.Crypto using (CryptoStructure)
+open import Ledger.Core.Specification.Epoch using (EpochStructure)
+
+module Ledger.Dijkstra.Specification.Script
+  (crypto : CryptoStructure)
+  (es     : EpochStructure) where
+
+open import Ledger.Conway.Specification.Script crypto es public
+```

src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md

@@ -0,0 +1,170 @@
+---
+source_branch: master
+source_path: src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md
+---
+
+<!--
+```agda
+{-# OPTIONS --safe #-}
+
+open import Ledger.Dijkstra.Specification.Transaction
+open import Ledger.Dijkstra.Specification.Abstract
+
+module Ledger.Dijkstra.Specification.Script.Validation
+  (txs : _) (open TransactionStructure txs)
+  (abs : AbstractFunctions txs) (open AbstractFunctions abs) (open indexOf indexOfImp)
+  where
+
+open import Ledger.Prelude
+open import Ledger.Dijkstra.Specification.Certs govStructure
+```
+-->
+
+```agda
+data ScriptPurpose : Type where
+  Cert     : DCert               → ScriptPurpose
+  Rwrd     : RewardAddress       → ScriptPurpose
+  Mint     : ScriptHash          → ScriptPurpose
+  Spend    : TxIn                → ScriptPurpose
+  Vote     : GovVoter            → ScriptPurpose
+  Propose  : GovProposal         → ScriptPurpose
+  Guard    : (TxId × ScriptHash) → ScriptPurpose
+```
+
+<!--
+```agda
+private variable
+  ℓ : TxLevel
+
+rdptr : (Tx ℓ) → ScriptPurpose → Maybe (RedeemerPtr ℓ)
+rdptr tx = λ where
+  (Cert h)              → map (Cert    ,_) $ indexOfDCert    h txCerts
+  (Rwrd h)              → map (Reward  ,_) $ indexOfRwdAddr  h txWithdrawals
+  (Mint h)              → map (Mint    ,_) $ indexOfPolicyId h (policies mint)
+  (Spend h)             → map (Spend   ,_) $ indexOfTxIn     h txIns
+  (Vote h)              → map (Vote    ,_) $ indexOfVote     h (map GovVote.voter txGovVotes)
+  (Propose h)           → map (Propose ,_) $ indexOfProposal h txGovProposals
+  (Guard h)             → map (Guard   ,_) $ indexOfGuard    h (getTxScripts tx)
+ where open TxBody (TxBodyOf tx)
+-- getSubTxScripts : TopLevelTx → ℙ (TxId × ScriptHash)
+
+indexedRdmrs : (Tx ℓ) → ScriptPurpose → Maybe (Redeemer × ExUnits)
+indexedRdmrs tx sp = maybe (λ x → lookupᵐ? txRedeemers x) nothing (rdptr tx sp)
+  where open Tx tx; open TxWitnesses txWitnesses
+
+getDatum : Tx ℓ → UTxO → ScriptPurpose → Maybe Datum
+getDatum tx utxo (Spend txin) =
+  do (_ , _ , just d , _) ← lookupᵐ? utxo txin where
+                            (_ , _ , nothing , _) → nothing
+     case d of λ where
+       (inj₁ d) → just d
+       (inj₂ h) → lookupᵐ? (setToMap (mapˢ < hash , id > (DataOf tx))) h
+getDatum tx utxo _ = nothing
+```
+-->
+
+```agda
+record TxInfo : Type where
+  field realizedInputs : UTxO
+        txOuts         : Ix ⇀ TxOut
+        txFee          : Maybe Fees
+        mint           : Value
+        txCerts        : List DCert
+        txWithdrawals  : Withdrawals
+        txVldt         : Maybe Slot × Maybe Slot
+        vkKey          : ℙ KeyHash
+        txData         : ℙ Datum
+        txId           : TxId
+
+
+txInfo : (ℓ : TxLevel) → UTxO → Tx ℓ → TxInfo
+
+txInfo TxLevelTop utxo tx =
+  record  { realizedInputs = utxo ∣ txIns
+          ; txOuts = txOuts
+          ; txFee = just txFee
+          ; mint = mint
+          ; txCerts = txCerts
+          ; txWithdrawals = txWithdrawals
+          ; txVldt = txVldt
+          ; vkKey = txRequiredGuards -- ?
+          ; txData = DataOf tx
+          ; txId = txId
+          } where open Tx tx; open TxBody txBody
+
+txInfo TxLevelSub utxo tx =
+  record  { realizedInputs = utxo ∣ txIns
+          ; txOuts = txOuts
+          ; txFee = nothing
+          ; mint = mint
+          ; txCerts = txCerts
+          ; txWithdrawals = txWithdrawals
+          ; txVldt = txVldt
+          ; vkKey = txRequiredGuards  -- ?
+          ; txData = DataOf tx
+          ; txId = txId
+          } where open Tx tx; open TxBody txBody
+```
+
+<!--
+```agda
+credsNeededMinusCollateral : {ℓ : TxLevel} → TxBody ℓ → ℙ (ScriptPurpose × Credential)
+credsNeededMinusCollateral txb = a ∪ b ∪ c ∪ d ∪ e
+  where
+  a b c d e : ℙ (ScriptPurpose × Credential)
+  a = mapˢ (λ a → (Rwrd a , CredentialOf a)) (dom ∣ WithdrawalsOf txb ∣)
+  b = mapPartial (λ c → (Cert c ,_) <$> cwitness c) (fromList (DCertsOf txb))
+  c = mapˢ (λ x → (Mint x , ScriptObj x)) (policies (ValueOf txb))
+  d = mapPartial (λ v → if isGovVoterCredential v then (λ {c} → just (Vote v , c)) else nothing)
+                 (fromList (map GovVoterOf (GovVotesOf txb)))
+  e = mapPartial (λ p → if PolicyOf p then (λ {sh} → just (Propose  p , ScriptObj sh)) else nothing)
+                 (fromList (GovProposalsOf txb))
+
+credsNeeded : (ℓ : TxLevel) → UTxO → (TxBody ℓ) → ℙ (ScriptPurpose × Credential)
+credsNeeded TxLevelTop utxo txb = credsNeededMinusCollateral txb
+  ∪ mapˢ (λ (i , o) → (Spend  i , payCred (proj₁ o))) ((utxo ∣ (txIns ∪ collateralInputs)) ˢ)
+  where open TxBody txb
+
+credsNeeded TxLevelSub utxo txb = credsNeededMinusCollateral txb
+  ∪ mapˢ (λ (i , o) → (Spend  i , payCred (proj₁ o))) ((utxo ∣ txIns) ˢ)
+  where open TxBody txb
+
+valContext : TxInfo → ScriptPurpose → Data
+valContext txinfo sp = toData (txinfo , sp)
+
+txOutToDataHash : TxOut → Maybe DataHash
+txOutToDataHash (_ , _ , d , _) = d >>= isInj₂
+
+txOutToP2Script
+  : UTxO → (Tx ℓ)
+  → TxOut → Maybe P2Script
+txOutToP2Script utxo tx (a , _) =
+  do sh ← isScriptObj (payCred a)
+     s  ← lookupScriptHash sh tx utxo
+     toP2Script s
+-- opaque
+--   collectP2ScriptsWithContext
+--     : PParams → (Tx ℓ) → UTxO
+--     → List (P2Script × List Data × ExUnits × CostModel)
+--   collectP2ScriptsWithContext pp tx utxo
+--     = setToList
+--     $ mapPartial (λ (sp , c) → if isScriptObj c
+--                                 then (λ {sh} → toScriptInput sp sh)
+--                                 else nothing)
+--     $ credsNeeded utxo (TxBodyOf tx)
+--     where
+--       toScriptInput
+--         : ScriptPurpose → ScriptHash
+--         → Maybe (P2Script × List Data × ExUnits × CostModel)
+--       toScriptInput sp sh =
+--         do s ← lookupScriptHash sh tx utxo
+--            p2s ← toP2Script s
+--            (rdmr , exunits) ← indexedRdmrs tx sp
+--            let data'     = maybe [_] [] (getDatum tx utxo sp) ++ rdmr ∷ [ valContext (txInfo (language p2s) pp utxo tx) sp ]
+--                costModel = PParams.costmdls pp
+--            just (p2s , data' , exunits , costModel)
+
+evalP2Scripts : List (P2Script × List Data × ExUnits × CostModel) → Bool
+evalP2Scripts = all (λ (s , d , eu , cm) → runPLCScript cm s eu d)
+```
+-->

src/Ledger/Dijkstra/Specification/TokenAlgebra/Base.lagda.md

@@ -0,0 +1,11 @@
+---
+source_branch: master
+source_path: src/Ledger/Dijkstra/Specification/TokenAlgebra/Base.lagda.md
+---
+```agda
+{-# OPTIONS --safe #-}
+open import Prelude using (Type)
+module Ledger.Dijkstra.Specification.TokenAlgebra.Base (PolicyId : Type) where
+
+open import Ledger.Conway.Specification.TokenAlgebra.Base PolicyId public
+```