641-incorporate-feedback-from-the-second-audit (#662)

* Highlight txid

* Rename Enact-NewComm to UpdComm

* Rename pp Q5e to Q5

* Add security-group parameters to figure

* Add reference to definition of Deposits

* Clarify that a voter needs to be registered to vote

* Combine sec. 8.1-8.3 and emphasize 8.1 more; add clarification about deposit in cert.

* Clarify the role of UpdateT in updating parameters

* Clarify the threshold of votes

---------

Co-authored-by: Andre Knispel <andre.knispel@iohk.io>

Author: carlostome

src/Ledger/Certs.lagda

@@ -31,6 +31,7 @@ instance
     ((quote DepositPurpose , DecEq-DepositPurpose) ∷ [])
 \end{code}
 \caption{Deposit types}
+\label{fig:certs:deposit-types}
 \end{figure*}
 
 \begin{figure*}[h!]
@@ -184,9 +185,22 @@ private variable
   cc : ℙ Credential
 \end{code}
 
-\subsection{Removal of Pointer Addresses, Genesis Delegations and MIR Certificates}
+\subsection{Changes Introduced in Conway Era}
 
-In the Conway era, support for pointer addresses, genesis delegations
+\subsubsection{Delegation}
+
+Registered credentials can now delegate to a DRep as well as to a
+stake pool. This is achieved by giving the \delegate certificate two
+optional fields, corresponding to a DRep and stake pool.
+
+Stake can be delegated for voting and block production simultaneously,
+since these are two separate features. In fact, preventing this could
+weaken the security of the chain, since security relies on high
+participation of honest stake holders.
+
+\subsubsection{Removal of Pointer Addresses, Genesis Delegations and MIR Certificates}
+
+Support for pointer addresses, genesis delegations
 and MIR certificates is removed. In \DState, this means that the four
 fields relating to those features are no longer present, and \DelegEnv
 contains none of the fields it used to in the Shelley era.
@@ -198,25 +212,18 @@ stake distribution anymore. Genesis delegations and MIR certificates
 have been superceded by the new governance mechanisms, in particular
 the \TreasuryWdrl governance action in case of the MIR certificates.
 
-\subsection{Explicit Deposits}
+\subsubsection{Explicit Deposits}
 
 Registration and deregistration of staking credentials are now
 required to explicitly state the deposit that is being paid or
-refunded. This aligns them better with other design decisions such as
-having explicit transaction fees and helps make this information
-visible to light clients and hardware wallets. While not shown in the
-figures, the old certificates without explicit deposits will still be
-supported for some time for backwards compatibility.
-
-\subsection{Delegation}
-
-Registered credentials can now delegate to a DRep as well as to a
-stake pool. This is achieved by giving the \delegate certificate two
-optional fields, corresponding to a DRep and stake pool. Stake can be
-delegated for voting and block production simultaneously, since these
-are two separate features. In fact, preventing this could weaken the
-security of the chain, since security relies on high participation of
-honest stake holders.
+refunded. This deposit is used for checking correctness of transactions
+with certificates. Including the deposit aligns better with other
+design decisions such as having explicit transaction fees and helps
+make this information visible to light clients and hardware wallets.
+
+While not shown in the figures, the old certificates without explicit
+deposits will still be supported for some time for backwards
+compatibility.
 
 \subsection{Governance Certificate Rules}
 

src/Ledger/Enact.lagda

@@ -128,7 +128,7 @@ data _⊢_⇀⦇_,ENACT⦈_ where
     ───────────────────────────────────────
     ⟦ gid , t , e ⟧ᵉ ⊢ s ⇀⦇ NoConfidence ,ENACT⦈ record s { cc = nothing , gid }
 
-  Enact-NewComm : let old      = maybe proj₁ ∅ (s .cc .proj₁)
+  Enact-UpdComm : let old      = maybe proj₁ ∅ (s .cc .proj₁)
                       maxTerm  = s .pparams .proj₁ .ccMaxTermLength +ᵉ e
                   in
     ∀[ term ∈ range new ] term ≤ maxTerm

src/Ledger/Gov.lagda

@@ -438,13 +438,11 @@ The GOV transition system is now given as the reflexitive-transitive
 closure of the system GOV', described in
 Figure~\ref{defs:gov-rules}.
 
-For \GOVVote{}, we check that the governance action being voted on
-exists and the role is allowed to vote. \canVote{} is defined in
-Figure~\ref{fig:ratification-requirements}. Note that there are no
-checks on whether the credential is actually associated with the
-role. This means that anyone can vote for, e.g., the \CC{} role. However,
-during ratification those votes will only carry weight if they are
-properly associated with members of the constitutional committee.
+For \GOVVote, we check that the governance action being voted on
+exists; that the voter's role is allowed to vote (see \canVote{} in
+Figure~\ref{fig:ratification-requirements}); and that the voter's
+credential is actually associated with their role (see
+\isRegistered{} in Figure~\ref{defs:gov-defs}).
 
 For \GOVPropose{}, we check the correctness of the deposit along with some
 and some conditions that ensure the action is well-formed and valid;

src/Ledger/GovernanceActions/Properties.agda

@@ -23,7 +23,7 @@ instance
     (UpdateCommittee new rem q) →
       case ¿ ∀[ term ∈ range new ]
                term ≤ s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ' e ¿ of λ where
-      (yes p) → success (-, Enact-NewComm
+      (yes p) → success (-, Enact-UpdComm
         (subst (λ x → ∀[ term ∈ range new ] term ≤ x) (sym +ᵉ≡+ᵉ') p))
       (no ¬p) → failure "ENACT failed at ∀[ term ∈ range new ] term ≤ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e)"
     (NewConstitution dh sh)  → success (-, Enact-NewConst)
@@ -37,7 +37,7 @@ instance
   Computational-ENACT .completeness ⟦ _ , t , e ⟧ᵉ s action _ p
     with action | p
   ... | .NoConfidence           | Enact-NoConf   = refl
-  ... | .UpdateCommittee new rem q | Enact-NewComm p
+  ... | .UpdateCommittee new rem q | Enact-UpdComm p
     rewrite dec-yes
       (¿ ∀[ term ∈ range new ] term
            ≤ s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ' e ¿)

src/Ledger/PDF/ConwayBootstrap.lagda

@@ -16,7 +16,7 @@ be made to the ledger described in this document.
 \item Transactions containing a vote other than a \CC vote,
       a \SPO vote on a \TriggerHF action or any vote on an \Info
       action will be rejected.
-\item \Qfour, \Pfive and \Qfivee are set to $0$.
+\item \Qfour, \Pfive and \Qfive are set to $0$.
 \item An SPO that does not vote is assumed to have voted \abstain.
 \end{itemize}
 

src/Ledger/PParams.lagda

@@ -76,7 +76,7 @@ record DrepThresholds : Type where
 
 record PoolThresholds : Type where
   field
-    Q1 Q2a Q2b Q4 Q5e : ℚ
+    Q1 Q2a Q2b Q4 Q5 : ℚ
 
 record PParams : Type where
   field
@@ -136,6 +136,11 @@ record PParams : Type where
         drepActivity                  : Epoch
 \end{code}
 \end{AgdaMultiCode}
+\emph{Security group}
+
+\maxBlockSize{} \maxTxSize{} \maxHeaderSize{} \maxValSize{}
+\maxBlockExUnits{} \AgdaField{a}{} \AgdaField{b}{}
+\minFeeRefScriptCoinsPerByte{} \coinsPerUTxOByte{} \govActionDeposit{}
 \caption{Protocol parameter definitions}
 \label{fig:protocol-parameter-declarations}
 \end{figure*}
@@ -404,7 +409,7 @@ following concepts.
 \begin{itemize}
   \item \drepThresholds: governance thresholds for \DReps; these are rational numbers
   named \Pone, \Ptwoa, \Ptwob, \Pthree, \Pfour, \Pfivea, \Pfiveb, \Pfivec, \Pfived, and \Psix;
-  \item \poolThresholds: pool-related governance thresholds; these are rational numbers named \Qone, \Qtwoa, \Qtwob, \Qfour and \Qfivee;
+  \item \poolThresholds: pool-related governance thresholds; these are rational numbers named \Qone, \Qtwoa, \Qtwob, \Qfour and \Qfive;
   \item \ccMinSize: minimum constitutional committee size;
   \item \ccMaxTermLength: maximum term limit (in epochs) of constitutional committee members;
   \item \govActionLifetime: governance action expiration;
@@ -429,10 +434,21 @@ instance
   ... | yes refl | yes p    = ⊥-elim $ m+1+n≢m m $ ×-≡,≡←≡ p .proj₁
 \end{code}
 
-Finally, to update parameters we introduce an abstract type. An update
-can be applied and it has a set of groups associated with it. An
-update is well formed if it has at least one group (i.e. if it updates
-something) and if it preserves well-formedness.
+Figure~\ref{fig:pp-update-type} defines types and functions to update
+parameters. These consist of an abstract type \AgdaField{UpdateT} and
+two functions \AgdaField{applyUpdate} and \AgdaField{updateGroups}.
+The type \AgdaField{UpdateT} is to be instantiated by a type that
+%
+\begin{itemize}
+  \item can be used to update parameters, via the
+    function~\AgdaField{applyUpdate}
+  \item can be queried about what parameter groups it updates, via the
+    function~\AgdaField{updateGroups}
+\end{itemize}
+%
+An element of the type~\AgdaField{UpdateT} is well formed if it
+updates at least one group and applying the update preserves
+well-formedness.
 
 \begin{figure*}[ht]
 \begin{AgdaMultiCode}

src/Ledger/Ratify.lagda

@@ -50,7 +50,9 @@ in that order.
 The symbols mean the following:
 \begin{itemize}
 \item
-  \AgdaFunction{vote} x: For an action to pass, the stake associated with the yes votes must exceed the threshold x.
+  \AgdaFunction{vote} x: For an action to pass, the fraction of stake
+  associated with yes votes with respect to that associated
+  with yes and no votes must exceed the threshold x.
 \item
   \AgdaFunction{─}: The body of governance does not participate in voting.
 \item
@@ -151,7 +153,7 @@ threshold pp ccThreshold =
         pparamThreshold EconomicGroup    = (vote P5b  , ─         )
         pparamThreshold TechnicalGroup   = (vote P5c  , ─         )
         pparamThreshold GovernanceGroup  = (vote P5d  , ─         )
-        pparamThreshold SecurityGroup    = (─         , vote Q5e  )
+        pparamThreshold SecurityGroup    = (─         , vote Q5   )
 
         P/Q5 : PParamsUpdate → Maybe ℚ × Maybe ℚ
         P/Q5 ppu = maxThreshold (mapˢ (proj₁ ∘ pparamThreshold) (updateGroups ppu))

src/Ledger/Transaction.lagda

@@ -51,8 +51,8 @@ Ingredients of the transaction body introduced in the Conway era are the followi
 \begin{itemize}
   \item \txvote, the list of votes for goverance actions;
   \item \txprop, the list of governance proposals;
-  \item \txdonation, the treasury donation amount;
-  \item \curTreasury, the current value of the treasury.
+  \item \txdonation, amount of \Coin to donate to treasury, e.g., to return money to the treasury after a governance action;
+  \item \curTreasury, the current value of the treasury. This field serves as a precondition to executing Plutus scripts that access the value of the treasury;
   \item \txsize and \txid, the size and hash of the serialized form of the transaction that was included in the block.
 \end{itemize}
 \end{Conway}

src/Ledger/Utxo.lagda

@@ -145,7 +145,8 @@ is gone with the new design.
 
 Similar to \ScriptPurpose, \DepositPurpose carries the information
 what the deposit is being made for. The deposits are stored in the
-\deposits field of \UTxOState. \updateDeposits is responsible for
+\deposits field of \UTxOState (the type \Deposits{} is defined in
+Figure~\ref{fig:certs:deposit-types}). \updateDeposits is responsible for
 updating this map, which is split into \updateCertDeposits and
 \updateProposalDeposits, responsible for certificates and proposals
 respectively. Both of these functions iterate over the relevant fields

src/ScriptVerification/Lib.agda

@@ -65,7 +65,7 @@ createEnv s = record { slot = s ; treasury = 0 ;
                                                     ; Q2a = ½
                                                     ; Q2b = ½
                                                     ; Q4 = ½
-                                                    ; Q5e = ½
+                                                    ; Q5 = ½
                                                     }
                                ; govActionLifetime = 10 -- unknown
                                ; govActionDeposit = 1000000 -- unknown (set to 1 ada)