Add some missing explanations and some minor improvements (#391)

src/Ledger/Foreign/HSLedger.agda

@@ -147,12 +147,10 @@ HsGovParams : GovParams
 HsGovParams = record
   { Implementation
   ; ppUpd = let open PParamsDiff in λ where
-      .UpdateT                → ⊤
-      .updateGroups           → λ _ → ∅
-      .applyUpdate            → λ p _ → p
-      .ppdWellFormed          → λ _ → false
-      .ppdWellFormed⇒hasGroup → λ ()
-      .ppdWellFormed⇒WF       → λ _ _ x → x
+      .UpdateT      → ⊤
+      .updateGroups → λ _ → ∅
+      .applyUpdate  → λ p _ → p
+      .ppWF?        → ⁇ yes (λ _ h → h)
   ; ppHashingScheme = it
   }
 

src/Ledger/Gov.lagda

@@ -217,7 +217,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where
                     ; policy = p ; deposit = d ; prevAction = prev }
       s' = addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev
     in
-    ∙ actionWellFormed a ≡ true
+    ∙ actionWellFormed a
     ∙ d ≡ govActionDeposit
     ∙ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy)
     ∙ (∀ {new rem q} → a ≡ NewCommittee new rem q

src/Ledger/Gov/Properties.agda

@@ -111,7 +111,9 @@ instance
           renaming (action to a; deposit to d; policy to p; returnAddr to addr; prevAction to prev)
         open PParams pparams hiding (a)
 
-        H = ¿ actionWellFormed a ≡ true
+        instance _ = actionWellFormed?
+
+        H = ¿ actionWellFormed a
             × d ≡ govActionDeposit
             × validHFAction prop s enactState
             × (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy)

src/Ledger/GovernanceActions.lagda

@@ -9,9 +9,10 @@ We introduce three distinct bodies that have specific functions in the new gover
 \item
   the stake pool operators (henceforth called \SPOs)
 
-In the following figure, \DocHash is equal to any other 32-bit hash
-type (such as \ScriptHash). We use a different name to avoid
-confusion.
+In the following figure, \DocHash is abstract but in the
+implementation it will be instantiated with a 32-bit hash type (like
+e.g. \ScriptHash). We keep it separate because it is used for a
+different purpose.
 
 \end{enumerate}
 \begin{code}[hide]
@@ -57,9 +58,19 @@ data GovAction : Set where
   TreasuryWdrl     : (RwdAddr ⇀ Coin)                         →  GovAction
   Info             :                                             GovAction
 
-actionWellFormed : GovAction → Bool
+actionWellFormed : GovAction → Set
 actionWellFormed (ChangePParams x)  = ppdWellFormed x
-actionWellFormed _                  = true
+actionWellFormed _                  = ⊤
+\end{code}
+\begin{code}[hide]
+actionWellFormed? : ∀ {a} → actionWellFormed a ⁇
+actionWellFormed? {NoConfidence}        = Dec-⊤
+actionWellFormed? {NewCommittee _ _ _}  = Dec-⊤
+actionWellFormed? {NewConstitution _ _} = Dec-⊤
+actionWellFormed? {TriggerHF _}         = Dec-⊤
+actionWellFormed? {ChangePParams x}     = Dec-×
+actionWellFormed? {TreasuryWdrl _}      = Dec-⊤
+actionWellFormed? {Info}                = Dec-⊤
 \end{code}
 \caption{Governance actions}
 \label{defs:governance}

src/Ledger/PParams.lagda

@@ -104,7 +104,6 @@ paramsWellFormed pp =
      0 ∉ fromList  ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize
                    ∷ minUTxOValue ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
                    ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
-  ×  ℕtoEpoch govActionLifetime ≤ drepActivity
   where open PParams pp
 \end{code}
 \end{AgdaMultiCode}
@@ -168,6 +167,8 @@ instance
     ((quote PoolThresholds , DecEq-PoolThresholds) ∷ [])
   unquoteDecl DecEq-PParams        = derive-DecEq
     ((quote PParams , DecEq-PParams) ∷ [])
+  unquoteDecl DecEq-PParamGroup    = derive-DecEq
+    ((quote PParamGroup , DecEq-PParamGroup) ∷ [])
 
 instance
   pvCanFollow? : ∀ {pv} {pv'} → Dec (pvCanFollow pv pv')
@@ -177,17 +178,41 @@ instance
   ... | no ¬p    | yes refl = yes canFollowMinor
   ... | yes refl | no ¬p    = yes canFollowMajor
   ... | 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.
 
+\begin{figure*}[h!]
+\begin{AgdaMultiCode}
+\begin{code}[hide]
 record PParamsDiff : Set₁ where
-  field UpdateT : Set
-        updateGroups : UpdateT → ℙ PParamGroup
-        applyUpdate : PParams → UpdateT → PParams
-        ppdWellFormed : UpdateT → Bool
-        ppdWellFormed⇒hasGroup : ∀ {u} → ppdWellFormed u ≡ true → updateGroups u ≢ ∅
-        ppdWellFormed⇒WF       : ∀ {u} → ppdWellFormed u ≡ true → ∀ pp
-                               → paramsWellFormed pp
-                               → paramsWellFormed (applyUpdate pp u)
+  field
+\end{code}
+\emph{Abstract types \& functions}
+\begin{code}
+    UpdateT : Set
+    applyUpdate : PParams → UpdateT → PParams
+    updateGroups : UpdateT → ℙ PParamGroup
 
+\end{code}
+\begin{code}[hide]
+    ⦃ ppWF? ⦄ : ∀ {u} → (∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u)) ⁇
+\end{code}
+\emph{Well-formedness condition}
+\begin{code}
+
+  ppdWellFormed : UpdateT → Set
+  ppdWellFormed u = updateGroups u ≢ ∅
+    × ∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u)
+\end{code}
+\end{AgdaMultiCode}
+\caption{Abstract type for parameter updates}
+\label{fig:pp-update-type}
+\end{figure*}
+\begin{code}[hide]
 record GovParams : Set₁ where
   field ppUpd : PParamsDiff
   open PParamsDiff ppUpd renaming (UpdateT to PParamsUpdate) public

src/Ledger/Ratify.lagda

@@ -436,7 +436,12 @@ functions (together with some helpers) that are used in the rules of
 RATIFY.
 
 \begin{itemize}
-  \item \getStakeDist computes the stake distribution based on the given governance role and the corresponding delegations;
+  \item \getStakeDist computes the stake distribution based on the
+    given governance role and the corresponding delegations. Note that
+    every constitutional committe member has a stake of 1, giving them
+    equal voting power. However, just as with other delegation, multiple
+    CC members can delegate to the same hot key, giving that hot key
+    the power of those multiple votes with a single actual vote.
 
   \item \acceptedStakeRatio is the ratio of accepted stake. It is
     computed as the ratio of \yes votes over the votes that didn't
@@ -508,7 +513,14 @@ abstract
 Figure~\ref{fig:defs:ratify-defs-ii} defines functions that
 deal with delays. A given action can either be delayed if the action
 contained in \EnactState isn't the one the given action is building on top
-of, or if a previous action was a \delayingAction.
+of, which is checked by \verifyPrev, or if a previous action was a
+\delayingAction. Note that \delayingAction affects the future: whenever a
+\delayingAction is accepted all future actions are delayed. \delayed then
+expresses the condition whether an action is delayed. This happens either
+because the previous action doesn't match the current one, or because the
+previous action was a delaying one. This information is passed in as an
+argument.
+
 \begin{code}[hide]
 private variable
   Γ : RatifyEnv