Add pool-vote witnesses for BLS-authorized SPO governance votes

build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs

@@ -11,7 +11,7 @@ import MAlonzo.Code.Ledger.Dijkstra.Foreign.PParams           as X
   (LanguageCostModels(..), DrepThresholds(..), PoolThresholds(..), Acnt(..), PParams(..), PParamsUpdate(..))
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Transaction       as X
   ( TxBodyTop(..), TxTop(..), TxBodySub(..), TxSub(..)
-  , Tag(..), TxWitnesses(..)
+  , Tag(..), TxWitnesses(..), PoolVoteWitness(..)
   , TxId, Ix, TxIn, ExUnits, P1Script, P2Script
   , Script, Datum, DataHash, Value, TxOut, ScriptHash, AuxiliaryData, Withdrawals
   , Redeemer, RedeemerPtr

src/Ledger/Dijkstra/Foreign/ExternalStructures.agda

@@ -73,6 +73,7 @@ instance
     ; cryptoStructure = it
     ; govParams       = HsGovParams
     ; txidBytes       = id
+    ; poolVoteBytes   = suc  -- disjoint from txidBytes in the ℕ mock
     ; scriptStructure = it
     ; adHashingScheme = isHashableSet-ℕ
     ; Hashable-ScriptIntegrity = record { hash = λ x → 0 }

src/Ledger/Dijkstra/Foreign/Transaction.agda

@@ -35,6 +35,9 @@ instance
   HsTy-HSPlutusScript = autoHsType HSPlutusScript
   Conv-HSPlutusScript = autoConvert HSPlutusScript
 
+  HsTy-PoolVoteWitness = autoHsType PoolVoteWitness ⊣ withName "PoolVoteWitness"
+  Conv-PoolVoteWitness = autoConvert PoolVoteWitness
+
   HsTy-TxWitnesses = autoHsType TxWitnesses ⊣ withConstructor "MkTxWitnesses"
                                               • fieldPrefix "txw"
   Conv-TxWitnesses = autoConvert TxWitnesses

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

@@ -468,6 +468,13 @@ poolVrfs ps = mapˢ (vrf ∘ params) (range ps)
 poolBlsKey : Pools → KeyHash → Maybe BlsKeyState
 poolBlsKey ps kh = lookupᵐ? ps kh >>= blsKey
 
+-- A registered voting key is honoured until maxKeyAgeEpochs epochs after its
+-- registration, judged against the epoch the key is used in.
+honouredBlsKey : ℕ → Epoch → Maybe BlsKeyState → Maybe BlsVKey
+honouredBlsKey maxAge e nothing   = nothing
+honouredBlsKey maxAge e (just k)  =
+  if e < BlsKeyState.registered k + ℕtoEpoch maxAge then just (BlsKeyState.key k) else nothing
+
 installBlsKey : KeyHash → BlsKeyState → Pools → Pools
 installBlsKey kh k = mapWithKey λ kh' s → if kh' ≡ kh then record s { blsKey = just k } else s
 

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

@@ -148,6 +148,10 @@ isGovVoterDRep : GovVoter → Maybe Credential
 isGovVoterDRep ⟦ DRep , c ⟧ᵍᵛ = just c
 isGovVoterDRep _ = nothing
 
+isGovVoterSPO : GovVoter → Maybe KeyHash
+isGovVoterSPO ⟦ SPO , kh ⟧ᵍᵛ = just kh
+isGovVoterSPO _ = nothing
+
 govVoterCredential : GovVoter → Credential
 govVoterCredential ⟦ CC   , c  ⟧ᵍᵛ = c
 govVoterCredential ⟦ DRep , c  ⟧ᵍᵛ = c

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

@@ -45,6 +45,7 @@ record SubLedgerEnv : Type where
     enactState       : EnactState
     treasury         : Treasury
     utxo₀            : UTxO
+    pools₀           : Pools
     rewards₀         : Rewards
     allScripts       : ℙ Script
     isTopLevelValid  : Bool
@@ -212,6 +213,7 @@ private variable
   isTopLevelValid                   : Bool
   allScripts                        : ℙ Script
   rewards₀                          : Rewards
+  pools₀                            : Pools
 ```
 -->
 
@@ -285,17 +287,17 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx 
 
   SUBLEDGER-V :
       ∙ isTopLevelValid ≡ true
-      ∙ ⟦ slot , pp , treasury , utxo₀ , allScripts , isTopLevelValid ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
+      ∙ ⟦ slot , pp , treasury , utxo₀ , pools₀ , allScripts , isTopLevelValid ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
       ∙ ⟦ epoch slot , pp , allColdCreds govState₀ enactState , rewards₀ ⟧ ⊢ certState₀ ⇀⦇ stx ,SUBENTITIES⦈ certState₁
       ∙ ⟦ TxIdOf stx , epoch slot , pp , ppolicy , enactState , certState₁ , dom (RewardsOf certState₁) ⟧ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁
         ────────────────────────────────
-        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
+        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , pools₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
 
   SUBLEDGER-I :
       ∙ isTopLevelValid ≡ false
-      ∙ ⟦ slot , pp , treasury , utxo₀ , allScripts , isTopLevelValid  ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
+      ∙ ⟦ slot , pp , treasury , utxo₀ , pools₀ , allScripts , isTopLevelValid  ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
         ────────────────────────────────
-        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
+        ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , pools₀ , rewards₀ , allScripts , isTopLevelValid ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
 
 _⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LedgerState → List SubLevelTx → LedgerState → Type
 _⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_}
@@ -317,7 +319,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
          legacyMode = isLegacyMode utxo₀ allScripts tx
     in
       ∙ IsValidFlagOf tx ≡ true
-      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
+      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , PoolsOf certState₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
       ∙ ⟦ epoch slot , pp , allColdCreds govState₁ enactState , legacyMode , rewards₀ ⟧ ⊢ certState₁ ⇀⦇ tx ,ENTITIES⦈ certState₂
       ∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState₂ , dom (RewardsOf certState₂) ⟧ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂
       ∙ ⟦ slot , pp , treasury , utxo₀ , PoolsOf certState₀ , allScripts , legacyMode ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
@@ -338,7 +340,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
          legacyMode = isLegacyMode utxo₀ allScripts tx
     in
       ∙ IsValidFlagOf tx ≡ false
-      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
+      ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , PoolsOf certState₀ , rewards₀ , allScripts , IsValidFlagOf tx ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
       ∙ ⟦ slot , pp , treasury , utxo₀ , PoolsOf certState₀ , allScripts , legacyMode ⟧ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁
         ────────────────────────────────
         ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₁ , govState₀ , certState₀ ⟧

src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md

@@ -44,7 +44,7 @@ private
     → IsTopLevelValidFlagOf Γ ≡ false
     → Γ ⊢ s ⇀⦇ stx ,SUBUTXOW⦈ s'
     → s' ≡ s
-  SUBUTXOW-noop isI (SUBUTXOW (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , SUBUTXO _)) rewrite isI = refl
+  SUBUTXOW-noop isI (SUBUTXOW (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , SUBUTXO _)) rewrite isI = refl
   -- After `rewrite isI`, `IsTopLevelValidFlagOf Γ` reduces to `false`,
   -- so the SUBUTXO post-state index reduces to `⟦ UTxOOf s , FeesOf s , DonationsOf s ⟧`
   -- which is s by eta-expansion of the UTxOState record, giving refl.
@@ -111,7 +111,7 @@ instance
       (stx : SubLevelTx)
       where
       subUtxoΓ : SubUTxOEnv
-      subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , allScripts , isTopLevelValid ⟧
+      subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , pools₀ , allScripts , isTopLevelValid ⟧
 
       subentitiesΓ : SubEntitiesEnv
       subentitiesΓ = ⟦ epoch slot , pparams , allColdCreds govSt enactState , rewards₀  ⟧
@@ -223,7 +223,7 @@ instance
       legacyMode = isLegacyMode utxo₀ allScripts txTop
 
       subΓ : SubLedgerEnv
-      subΓ = ⟦ slot , ppolicy , pparams , enactState , treasury , utxo₀ , RewardsOf (CertStateOf s) , allScripts , IsValidFlagOf txTop ⟧
+      subΓ = ⟦ slot , ppolicy , pparams , enactState , treasury , utxo₀ , PoolsOf (CertStateOf s) , RewardsOf (CertStateOf s) , allScripts , IsValidFlagOf txTop ⟧
 
       entitiesΓ : GovState → CertState → EntitiesEnv
       entitiesΓ govSt certSt = ⟦ epoch slot , pparams , allColdCreds govSt enactState , legacyMode , RewardsOf certSt ⟧

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

@@ -57,21 +57,15 @@ instance
 -->
 
 A registered voting key is honoured until `maxKeyAgeEpochs`{.AgdaFunction}
-epochs — a bound derived from the KES setup — after its registration.  Expiry
-is judged against the epoch the committee is
-selected for, not the epoch its stake snapshot was taken in: the seat's key
+epochs — a bound derived from the KES setup — after its registration
+(`honouredBlsKey`{.AgdaFunction}, defined in the `Certs`{.AgdaModule} module).
+Expiry is judged against the epoch the committee is selected for, not the
+epoch its stake snapshot was taken in: the seat's key
 comes from a snapshot and may therefore have been registered several epochs
 ago, while the age bound is applied afresh at each epoch boundary.  A committee
 thus has a stable set of usable keys throughout its epoch, and a key that ages
 out does so on a boundary rather than mid-epoch.
 
-```agda
-honouredBlsKey : ℕ → Epoch → Maybe BlsKeyState → Maybe BlsVKey
-honouredBlsKey maxAge e nothing   = nothing
-honouredBlsKey maxAge e (just k)  =
-  if e < BlsKeyState.registered k + ℕtoEpoch maxAge then just (BlsKeyState.key k) else nothing
-```
-
 The committee for an epoch consists of the `leiosCommitteeSize`{.AgdaField}
 pools with the most active stake, ties broken by ascending pool id.  Instead of
 sorting, a pool's seat index is *defined* as the number of pools strictly ahead

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

@@ -144,14 +144,23 @@ txOutToP2Script : ℙ Script → TxOut → Maybe P2Script
 txOutToP2Script scripts txOut = credentialToP2Script (payCred (proj₁ txOut)) scripts
 ```
 
+An SPO vote covered by a pool-vote witness needs no credential here — it is
+authorized by the pool's registered voting key instead, checked in the
+`Utxow`{.AgdaModule} module.  All other voters contribute their credential.
+
 ```agda
+voterCredNeeded : (KeyHash ⇀ PoolVoteWitness) → GovVoter → Maybe Credential
+voterCredNeeded pvs v = case isGovVoterSPO v of λ where
+  (just kh)  → if kh ∈ dom pvs then nothing else just (KeyHashObj kh)
+  nothing    → just (govVoterCredential v)
+
 credsNeeded : UTxO → Tx ℓ → ℙ (ScriptPurpose × Credential)
 credsNeeded utxo tx =
     mapˢ        (λ (i , o) → (⟦ Spend  , i ⟧ˢᵖ , payCred (proj₁ o)))     ((utxo ∣ (SpendInputsOf tx ∪ collateralInputs tx)) ˢ)
   ∪ mapˢ        (λ a       → (⟦ Reward , a ⟧ˢᵖ , CredentialOf a))        (dom ∣ WithdrawalsOf tx ∣)
   ∪ mapPartial  (λ c       → ((⟦ Cert  , c ⟧ˢᵖ ,_) <$> cwitness c))      (fromList (DCertsOf tx))
   ∪ mapˢ        (λ x       → (⟦ Mint   , x ⟧ˢᵖ , ScriptObj x))           (policies (MintedValueOf tx))
-  ∪ mapˢ        (λ v       → (⟦ Vote   , v ⟧ˢᵖ , govVoterCredential v))  (fromList (map GovVoterOf (ListOfGovVotesOf tx)))
+  ∪ mapPartial  (λ v       → ((⟦ Vote  , v ⟧ˢᵖ ,_) <$> voterCredNeeded (PoolVoteSigsOf tx) v))  (fromList (map GovVoterOf (ListOfGovVotesOf tx)))
   ∪ mapPartial  (λ p       →  if PolicyOf p
                                  then (λ {sh} → just (⟦ Propose , p ⟧ˢᵖ , ScriptObj sh))
                                  else nothing)                           (fromList (ListOfGovProposalsOf tx))

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

@@ -136,6 +136,9 @@ record TransactionStructure : Type₁ where
     govParams              : GovParams
     tokenAlgebra           : TokenAlgebra
     txidBytes              : TxId → Ser
+    -- Pool-vote message: the tx id under the "cardano-pool-vote" augmentation
+    -- context, domain-separating governance votes from Leios votes (CIP-0164).
+    poolVoteBytes          : TxId → Ser
 ```
 <!--
 ```agda
@@ -197,6 +200,19 @@ record TransactionStructure : Type₁ where
   open HasUTxO ⦃...⦄ public
 ```
 
+## Pool-Vote Witnesses
+
+A pool-vote witness authorizes an SPO governance vote with the pool's
+registered Leios voting key (CIP-0164) instead of the pool cold key.  The type
+is a tagged sum so that future authorization schemes extend it with new
+constructors rather than new witness-set fields; for now the only scheme is a
+BLS signature over `poolVoteBytes`{.AgdaField} of the transaction id.
+
+```agda
+  data PoolVoteWitness : Type where
+    blsW : BlsSig → PoolVoteWitness
+```
+
 ## The Main Transaction Types
 
 Transactions are represented as three mutually recursive record types that are
@@ -283,10 +299,11 @@ Of particular note in the Dijkstra era are
     record TxWitnesses : Type where
       inductive
       field
-        vKeySigs     : VKey ⇀ Sig
-        scripts      : ℙ Script
-        txData       : ℙ Datum
-        txRedeemers  : RedeemerPtr ⇀ Redeemer × ExUnits
+        vKeySigs      : VKey ⇀ Sig
+        poolVoteSigs  : KeyHash ⇀ PoolVoteWitness
+        scripts       : ℙ Script
+        txData        : ℙ Datum
+        txRedeemers   : RedeemerPtr ⇀ Redeemer × ExUnits
 
       scriptsP1 : ℙ P1Script
       scriptsP1 = mapPartial isInj₁ scripts
@@ -322,6 +339,10 @@ could be either of them.
     field TxWitnessesOf : A → TxWitnesses
   open HasTxWitnesses ⦃...⦄ public
 
+  record HasPoolVoteSigs {a} (A : Type a) : Type a where
+    field PoolVoteSigsOf : A → KeyHash ⇀ PoolVoteWitness
+  open HasPoolVoteSigs ⦃...⦄ public
+
   record HasRedeemers {a} (A : Type a) : Type a where
     field RedeemersOf : A → RedeemerPtr ⇀ Redeemer × ExUnits
   open HasRedeemers ⦃...⦄ public
@@ -535,6 +556,11 @@ could be either of them.
     HasData-Tx : HasData (Tx txLevel)
     HasData-Tx .DataOf = DataOf ∘ TxWitnessesOf
 
+    HasPoolVoteSigs-TxWitnesses : HasPoolVoteSigs TxWitnesses
+    HasPoolVoteSigs-TxWitnesses .PoolVoteSigsOf = TxWitnesses.poolVoteSigs
+    HasPoolVoteSigs-Tx : HasPoolVoteSigs (Tx txLevel)
+    HasPoolVoteSigs-Tx .PoolVoteSigsOf = PoolVoteSigsOf ∘ TxWitnessesOf
+
     HasGuards-TxBody : HasGuards (TxBody txLevel)
     HasGuards-TxBody .GuardsOf = TxBody.txGuards
     HasGuards-Tx : HasGuards (Tx txLevel)

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

@@ -87,6 +87,7 @@ record SubUTxOEnv : Type where
     pparams          : PParams
     treasury         : Treasury
     utxo₀            : UTxO
+    pools₀           : Pools
     allScripts       : ℙ Script
     isTopLevelValid  : Bool
 ```
@@ -202,6 +203,9 @@ instance
   HasPools-UTxOEnv : HasPools UTxOEnv
   HasPools-UTxOEnv .PoolsOf = UTxOEnv.pools₀
 
+  HasPools-SubUTxOEnv : HasPools SubUTxOEnv
+  HasPools-SubUTxOEnv .PoolsOf = SubUTxOEnv.pools₀
+
   unquoteDecl HasCast-UTxOEnv
               HasCast-SubUTxOEnv
               HasCast-UTxOState = derive-HasCast