incorporate Carlos's change requests

and fix bug introduced by rebase

Author: williamdemeo

src/Ledger/Conway/Conformance/Certs.agda

@@ -200,7 +200,7 @@ data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → T
 
 data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
 
-  CERT-init :
+  CERT-pre :
     let open PParams pp
         refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList vs)
         refreshedDReps  = mapValueRestricted (const (e + drepActivity)) dReps refresh
@@ -215,7 +215,7 @@ data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState →
 
 data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
 
-  CERT-last :
+  CERT-post :
       ⟦ e , pp , vs , wdrls , cc ⟧
       ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , ddep ⟧ , stᵖ , stᵍ ⟧
         ⇀⦇ _ ,POST-CERT⦈

src/Ledger/Conway/Conformance/Certs/Properties.agda

@@ -177,18 +177,18 @@ instance
         refreshedDReps  = mapValueRestricted (const (CertEnv.epoch ce + drepActivity)) dreps refresh
     in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
               × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
-      (yes p) → success (-, CERT-init p)
+      (yes p) → success (-, CERT-pre p)
       (no ¬p) → failure (genErrors ¬p)
-  Computational-PRE-CERT .completeness ce st _ st' (CERT-init p)
+  Computational-PRE-CERT .completeness ce st _ st' (CERT-pre p)
     rewrite let dState = CertState.dState st; open DState dState in
       dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs
                 × mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
         p .proj₂ = refl
 
   -- POST-CERT has no premises, so computing always succeeds
-  -- with the unique post-state and proof CERT-last.
+  -- with the unique post-state and proof CERT-post.
   Computational-POST-CERT : Computational _⊢_⇀⦇_,POST-CERT⦈_ String
-  Computational-POST-CERT .computeProof ce cs tt = success ( cs' , CERT-last)
+  Computational-POST-CERT .computeProof ce cs tt = success ( cs' , CERT-post)
     where
       dreps : DReps
       dreps = GState.dreps (CertState.gState cs)
@@ -199,7 +199,7 @@ instance
 
   -- Completeness: the relational proof pins s' to exactly `post`,
   -- and computeProof returns success at that same state; so refl.
-  Computational-POST-CERT .completeness ce cs _ cs' CERT-last = refl
+  Computational-POST-CERT .completeness ce cs _ cs' CERT-post = refl
 
 
 Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String

src/Ledger/Conway/Conformance/Equivalence.agda

@@ -217,7 +217,7 @@ getValidCertDepositsC : ∀ Γ s {s'} tx
                      → isValid tx ≡ true
                      → ⟦ epoch slot , pparams , txGovVotes , txWithdrawals , cc ⟧ C.⊢ certState ⇀⦇ txCerts ,CERTS⦈ s'
                      → L.ValidCertDeposits pparams deposits txCerts
-getValidCertDepositsC Γ s tx wf refl (run {s' = s'} (C.CERT-init _ , cert-post)) =
+getValidCertDepositsC Γ s tx wf refl (run {s' = s'} (C.CERT-pre _ , cert-post)) =
   getValidCertDepositsCERTS (C.UTxOState.deposits ((C.LState.utxoSt s))) wf cert-post
 
 lemUtxowDeposits : ∀ {Γ s s' tx}
@@ -266,7 +266,7 @@ open IsEquivalence ≡ᵈ-isEquivalence renaming (refl to ≡ᵈ-refl; sym to 
 lemCERTS'DepositsC : ∀ {Γ s dcerts s'} (open C.CertEnv Γ using (pp))
                    → RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ s dcerts s'
                    → certDepositsC s' ≡ ⟨ updateDDeps pp dcerts , updateGDeps pp dcerts ⟩ (certDepositsC s)
-lemCERTS'DepositsC (run-[] C.CERT-last) = refl
+lemCERTS'DepositsC (run-[] C.CERT-post) = refl
 lemCERTS'DepositsC (run-∷ (C.CERT-deleg  (C.DELEG-delegate     _)) rs) = lemCERTS'DepositsC rs
 lemCERTS'DepositsC (run-∷ (C.CERT-deleg  (C.DELEG-dereg        _)) rs) = lemCERTS'DepositsC rs
 lemCERTS'DepositsC (run-∷ (C.CERT-deleg  (C.DELEG-reg          _)) rs) = lemCERTS'DepositsC rs
@@ -279,7 +279,7 @@ lemCERTS'DepositsC (run-∷ (C.CERT-vdel   (C.GOVCERT-ccreghot   _)) rs) = lemCE
 lemCERTSDepositsC : ∀ {Γ s txCerts s'} (open C.CertEnv Γ using (pp))
                   → Γ C.⊢ s ⇀⦇ txCerts ,CERTS⦈ s'
                   → certDepositsC s' ≡ ⟨ updateDDeps pp txCerts , updateGDeps pp txCerts ⟩ (certDepositsC s)
-lemCERTSDepositsC (run (C.CERT-init _ , step)) = lemCERTS'DepositsC step
+lemCERTSDepositsC (run (C.CERT-pre _ , step)) = lemCERTS'DepositsC step
 
 lemWellformed : ∀ {Γ s tx s'} → WellformedLState s → Γ C.⊢ s ⇀⦇ tx ,LEDGER⦈ s' → WellformedLState s'
 lemWellformed {Γ} {s = ls} {tx} {s' = ls'} wf (C.LEDGER-V⋯ refl utxo certs gov) = goal
@@ -327,9 +327,6 @@ setCertDeposits (ddeps , gdeps) cs =
   let open C.CertState cs in
   ⟦ record dState {deposits = ddeps} , pState , record gState {deposits = gdeps} ⟧
 
--- _⊢_⇀⦇_,CERTS'⦈_ : C.CertEnv → C.CertState → List L.DCert → C.CertState → Type
--- _⊢_⇀⦇_,CERTS'⦈_ = ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_}
-
 updateCDep : PParams → L.DCert → L.Deposits × L.Deposits → L.Deposits × L.Deposits
 updateCDep pp cert (ddep , gdep) = updateDDep pp cert ddep , updateGDep pp cert gdep
 
@@ -339,7 +336,7 @@ opaque
              → RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ (deps₁ ⊢conv s) certs (deps₁' ⊢conv s')
              → ∃[ deps₂' ] deps₁' ≡ᵈ deps₂'
                            × RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ (deps₂ ⊢conv s) certs (deps₂' ⊢conv s')
-  castCERTS' deps₁ deps₂ deps₁' eqd (run-[] C.CERT-last) = deps₂ , eqd , run-[] C.CERT-last
+  castCERTS' deps₁ deps₂ deps₁' eqd (run-[] C.CERT-post) = deps₂ , eqd , run-[] C.CERT-post
   castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-deleg {dCert = cert} (C.DELEG-delegate h))    rs)
     = let
         open C.CertEnv Γ using (pp)
@@ -389,9 +386,9 @@ opaque
             → deps₁ ≡ᵈ deps₂
             → Γ C.⊢ deps₁ ⊢conv s ⇀⦇ certs ,CERTS⦈ (deps₁' ⊢conv s')
             → ∃[ deps₂' ] deps₁' ≡ᵈ deps₂' × Γ C.⊢ deps₂ ⊢conv s ⇀⦇ certs ,CERTS⦈ (deps₂' ⊢conv s')
-  castCERTS deps₁ deps₂ deps₁' eqd (run (C.CERT-init h , step)) =
+  castCERTS deps₁ deps₂ deps₁' eqd (run (C.CERT-pre h , step)) =
     let deps₂' , eqd' , step' = castCERTS' deps₁ deps₂ deps₁' eqd step
-    in  deps₂' , eqd' , run (C.CERT-init h , step')
+    in  deps₂' , eqd' , run (C.CERT-pre h , step')
 
 _⊢_⇀⦇_,GOVn⦈_ : L.GovEnv × ℕ → L.GovState → List (GovVote ⊎ GovProposal) → L.GovState → Type
 _⊢_⇀⦇_,GOVn⦈_ = _⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS} {_⊢_⇀⟦_⟧_ = L._⊢_⇀⦇_,GOV⦈_}

src/Ledger/Conway/Conformance/Equivalence/Certs.agda

@@ -153,13 +153,13 @@ instance
                  → L.Deposits × L.Deposits
                    ⊢ Γ L.⊢ s ⇀⦇ _ ,PRE-CERT⦈ s' ⭆ⁱ λ deposits _ →
                      Γ C.⊢ (deposits ⊢conv s) ⇀⦇ _ ,PRE-CERT⦈ (deposits ⊢conv s')
-  PRE-CERTToConf .convⁱ deposits (L.CERT-init h) = C.CERT-init h
+  PRE-CERTToConf .convⁱ deposits (L.CERT-pre h) = C.CERT-pre h
 
   POST-CERTToConf : ∀ {Γ s s'}
                  → L.Deposits × L.Deposits
                    ⊢ Γ L.⊢ s ⇀⦇ _ ,POST-CERT⦈ s' ⭆ⁱ λ deposits _ →
                      Γ C.⊢ (deposits ⊢conv s) ⇀⦇ _ ,POST-CERT⦈ (deposits ⊢conv s')
-  POST-CERTToConf .convⁱ deposits L.CERT-last = C.CERT-last
+  POST-CERTToConf .convⁱ deposits L.CERT-post = C.CERT-post
 
   DELEGToConf : ∀ {Γ s dcert dcerts s'}
                   (open L.DelegEnv Γ renaming (pparams to pp))
@@ -242,12 +242,12 @@ instance
   PRE-CERTFromConf : ∀ {Γ s s'}
                    → Γ C.⊢ s ⇀⦇ _ ,PRE-CERT⦈ s' ⭆
                      Γ L.⊢ (conv s) ⇀⦇ _ ,PRE-CERT⦈ (conv s')
-  PRE-CERTFromConf .convⁱ _ (C.CERT-init h) = L.CERT-init h
+  PRE-CERTFromConf .convⁱ _ (C.CERT-pre h) = L.CERT-pre h
 
   POST-CERTFromConf : ∀ {Γ s s'}
                    → Γ C.⊢ s ⇀⦇ _ ,POST-CERT⦈ s' ⭆
                      Γ L.⊢ (conv s) ⇀⦇ _ ,POST-CERT⦈ (conv s')
-  POST-CERTFromConf .convⁱ _ C.CERT-last = L.CERT-last
+  POST-CERTFromConf .convⁱ _ C.CERT-post = L.CERT-post
 
 
   CERT-POST-CERTFromConf : ∀ {Γ s dcerts s'}

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

@@ -63,17 +63,30 @@ instance
 
 ## Miscellaneous Type Aliases
 
-
 ```agda
-CCHotKeys DReps PoolEnv Pools Retiring Rewards Stake StakeDelegs : Type
-CCHotKeys    = Credential ⇀ Maybe Credential
-DReps        = Credential ⇀ Epoch
-PoolEnv      = PParams
-Pools        = KeyHash ⇀ StakePoolParams
-Retiring     = KeyHash ⇀ Epoch
-Rewards      = Credential ⇀ Coin
-Stake        = Credential ⇀ Coin
-StakeDelegs  = Credential ⇀ KeyHash
+CCHotKeys : Type
+CCHotKeys = Credential ⇀ Maybe Credential
+
+DReps : Type
+DReps = Credential ⇀ Epoch
+
+PoolEnv : Type
+PoolEnv = PParams
+
+Pools : Type
+Pools = KeyHash ⇀ StakePoolParams
+
+Retiring : Type
+Retiring = KeyHash ⇀ Epoch
+
+Rewards : Type
+Rewards = Credential ⇀ Coin
+
+Stake : Type
+Stake = Credential ⇀ Coin
+
+StakeDelegs : Type
+StakeDelegs = Credential ⇀ KeyHash
 ```
 
 <!--
@@ -356,10 +369,10 @@ private variable
 
 ### Delegation
 
-Registered credentials can now delegate to a DRep as well as to a stake
-pool. This is achieved by giving the
+Registered credentials can now delegate to a `DRep`{.AgdaInductiveConstructor}
+as well as to a stake pool.  This is achieved by giving the
 `delegate`{.AgdaInductiveConstructor} certificate two optional fields,
-corresponding to a DRep and stake pool.
+corresponding to a `DRep`{.AgdaInductiveConstructor} and stake pool.
 
 Stake can be delegated for voting and block production simultaneously,
 since these are two separate features. In fact, preventing this could
@@ -405,13 +418,15 @@ Sections [Auxiliary `DELEG`{.AgdaDatatype} Transition System](#auxiliary-deleg-t
 [Auxiliary `GOVCERT`{.AgdaDatatype} transition system](#auxiliary-govcert-transition-system).
 
 `GOVCERT`{.AgdaDatatype} deals with the new certificates relating to
-DReps and the constitutional committee.
+`DRep`{.AgdaInductiveConstructor}s and the constitutional committee.
 
 +  `GOVCERT-regdrep`{.AgdaInductiveConstructor} registers (or
-   re-registers) a DRep. In case of registration, a deposit needs to be
-   paid. Either way, the activity period of the DRep is reset.
+   re-registers) a `DRep`{.AgdaInductiveConstructor}.  In case of registration,
+   a deposit needs to be paid.  Either way, the activity period of the
+   `DRep`{.AgdaInductiveConstructor} is reset.
 
-+  `GOVCERT-deregdrep`{.AgdaInductiveConstructor} deregisters a DRep.
++  `GOVCERT-deregdrep`{.AgdaInductiveConstructor} deregisters a
+   `DRep`{.AgdaInductiveConstructor}.
 
 +  `GOVCERT-ccreghot`{.AgdaInductiveConstructor} registers a "hot"
    credential for constitutional committee members.[^1] We check that the
@@ -522,13 +537,13 @@ data _⊢_⇀⦇_,CERT⦈_  : CertEnv → CertState → DCert → CertState →
 Here we define the `CERTBASE`{.AgdaFunction} function which handles the following
 important housekeeping tasks:
 
-- check the correctness of withdrawals and ensure that withdrawals only
-  happen from credentials that have delegated their voting power;
++  check the correctness of withdrawals and ensure that withdrawals only
+   happen from credentials that have delegated their voting power;
 
-- set the rewards of the credentials that withdrew funds to zero;
++  set the rewards of the credentials that withdrew funds to zero;
 
-- and set the activity timer of all DReps that voted to `drepActivity`{.AgdaField}
-  epochs in the future.
++  and set the activity timer of all `DRep`{.AgdaInductiveConstructor}s that voted
+   to `drepActivity`{.AgdaField} epochs in the future.
 
 <!--
 ```agda
@@ -539,7 +554,7 @@ open GovVote using (voter)
 ```agda
 data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
 
-  CERT-init :
+  CERT-pre :
     let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList vs)
         refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
         wdrlCreds       = mapˢ stake (dom wdrls)
@@ -553,7 +568,7 @@ data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState →
 
 data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
 
-  CERT-last :
+  CERT-post :
     ⟦ e , pp , vs , wdrls , cc ⟧
     ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ , stᵖ , stᵍ ⟧
       ⇀⦇ _ ,POST-CERT⦈

src/Ledger/Conway/Specification/Certs/Properties/Computational.agda

@@ -143,21 +143,37 @@ instance
     with computeProof ce (gState cs) dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
 
-  Computational-CERTBASE : Computational _⊢_⇀⦇_,CERTBASE⦈_ String
-  Computational-CERTBASE .computeProof ce cs _ =
+  Computational-PRE-CERT : Computational _⊢_⇀⦇_,PRE-CERT⦈_ String
+  Computational-PRE-CERT .computeProof ce cs _ =
     let open CertEnv ce; open PParams pp
         open GState (gState cs); open DState (dState cs)
         refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList votes)
         refreshedDReps  = mapValueRestricted (const (CertEnv.epoch ce + drepActivity)) dreps refresh
     in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
               × mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
-      (yes p) → success (-, CERT-base p)
+      (yes p) → success (-, CERT-pre p)
       (no ¬p) → failure (genErrors ¬p)
-  Computational-CERTBASE .completeness ce st _ st' (CERT-base p)
+  Computational-PRE-CERT .completeness ce st _ st' (CERT-pre p)
     rewrite let dState = CertState.dState st; open DState dState in
       dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs
                 × mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
         p .proj₂ = refl
 
+  -- POST-CERT has no premises, so computing always succeeds
+  -- with the unique post-state and proof CERT-post.
+  Computational-POST-CERT : Computational _⊢_⇀⦇_,POST-CERT⦈_ String
+  Computational-POST-CERT .computeProof ce cs tt = success ( cs' , CERT-post)
+    where
+      dreps : DReps
+      dreps = GState.dreps (gState cs)
+      validVoteDelegs : VoteDelegs
+      validVoteDelegs = (VoteDelegsOf cs) ∣^ ( mapˢ vDelegCredential (dom dreps) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []) )
+      cs' : CertState
+      cs' = ⟦ ⟦ validVoteDelegs , StakeDelegsOf cs , RewardsOf cs ⟧ , PStateOf cs , GStateOf cs ⟧
+
+  -- Completeness: the relational proof pins s' to exactly `post`,
+  -- and computeProof returns success at that same state; so refl.
+  Computational-POST-CERT .completeness ce cs _ cs' CERT-post = refl
+
 Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
 Computational-CERTS = it

src/Ledger/Conway/Specification/Ledger.lagda.md

@@ -199,15 +199,15 @@ process governance action proposals and votes.
 ??? note
 
     The governance state used as input to `GOVS`{.AgdaDatatype} is filtered to
-    remove votes from DReps that are no longer
+    remove votes from `DRep`{.AgdaInductiveConstructor}s that are no longer
     registered (see function `rmOrphanDRepVotes`{.AgdaFunction}).
 
     This mechanism serves to prevent attacks where malicious adversaries could
     submit transactions that
 
-    1.  register a fraudulent DRep,
-    2.  cast numerous votes utilizing that DRep,
-    3.  deregisters the DRep thereby recovering the deposit.
+    1.  register a fraudulent `DRep`{.AgdaInductiveConstructor},
+    2.  cast numerous votes utilizing that `DRep`{.AgdaInductiveConstructor},
+    3.  deregisters the `DRep`{.AgdaInductiveConstructor} thereby recovering the deposit.
 
 <!--
 ```agda

src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md

@@ -13,12 +13,11 @@ module Ledger.Conway.Specification.Ledger.Properties.PoV
 
 open import Ledger.Conway.Specification.Certs govStructure
 open import Ledger.Conway.Specification.Chain txs abs
-open import Ledger.Conway.Specification.Certs.Properties govStructure
+open import Ledger.Conway.Specification.Certs.Properties.Computational govStructure
 open import Ledger.Conway.Specification.Certs.Properties.PoV govStructure
 open import Ledger.Conway.Specification.Ledger txs abs
 open import Ledger.Prelude
 open import Ledger.Conway.Specification.Utxo txs abs
-open import Ledger.Conway.Specification.Utxo.Properties txs abs using (χ; module DepositHelpers)
 open import Ledger.Conway.Specification.Utxo.Properties.PoV txs abs
 open import Ledger.Conway.Specification.Utxow txs abs
 

src/Ledger/Conway/Specification/Ratify.lagda

@@ -534,7 +534,7 @@ definitions:
   \item \AgdaFunction{defaultVote}: This map sets a default vote to
   all SPOs who didn't vote, with the default depending on the given
   action, and whether the SPO has delegated their vote to one of the
-  default DReps.
+  default \DRep{}s.
 
   \item \AgdaFunction{actualVotes}: This map combines the votes cast
   by SPOs with \AgdaBound{defaultVote} using a left-biased union
@@ -557,20 +557,20 @@ be counted as having voted \abstain{} by default. Members of the SPO
 community found this behavior counterintuitive and requested that
 non-voters be assigned a \no{} vote by default, with the caveat that
 an SPO could change its default setting by delegating its reward
-account credential to an \texttt{AlwaysNoConfidence} DRep or an
-\texttt{AlwaysAbstain} DRep. (This change applies only after the
+account credential to an \texttt{AlwaysNoConfidence} \DRep{} or an
+\texttt{AlwaysAbstain} \DRep{}. (This change applies only after the
 bootstrap period; during the bootstrap period the logic is unchanged;
 see \cref{sec:conway-bootstrap-gov}.)  To be precise, the agreed upon
 specification is the following: an SPO that did not vote is assumed to
 have voted \no{}, except under the following circumstances:
 %
 \begin{itemize}
   \item if the SPO has delegated its reward credential to an
-    \texttt{AlwaysNoConfidence} DRep, then their default vote is
+    \texttt{AlwaysNoConfidence} \DRep{}, then their default vote is
     \yes{} for \NoConfidence{} proposals and \no{} for other
     proposals;
   \item if the SPO has delegated its reward credential to an
-    \texttt{AlwaysAbstain} DRep, then its default vote is \abstain{}
+    \texttt{AlwaysAbstain} \DRep{}, then its default vote is \abstain{}
     for all proposals.
 \end{itemize}
 

src/Ledger/Introduction.lagda.md

@@ -218,7 +218,7 @@ formally defined.
 
 - [DELEG][] handles registering stake addresses and delegating to a stake pool.
 
-- [GOVCERT][] handles registering and delegating to DReps.
+- [GOVCERT][] handles registering and delegating to `DRep`{.AgdaInductiveConstructor}s.
 
 - [POOL][] handles registering and retiring stake pools.