Final computational instances

Update Computational record in Introduction

Remove unnecessary abstracts

Decidable comparison of rationals

Computational instance for RATIFY and fix minor bug in rule

Computational instance for NEWEPOCH

Computational for NEWPP and fix NEWPP-Reject rule

Computational instance for CHAIN and fix rule

import NewPP.Properties in Everything.agda

Go back to the old Computational in the Introduction

Remove minimumAVS check from Ratify.accepted

Remove spurious blank line

Abstract definitions for cleaner Ratify.Properties (#247)

Co-authored-by: Orestis Melkonian <[email protected]>

src/Everything.agda

@@ -4,6 +4,7 @@ import Ledger.PDF
 import Ledger.Foreign.HSLedger
 
 import Ledger.NewPP
+import Ledger.NewPP.Properties
 -- ^ deprecated in Conway, but keep it around for eventual earlier eras
 
 import MidnightExample.PDF

src/Interface/ComputationalRelation.agda

@@ -55,6 +55,9 @@ module _ (STS : C → S → Sig → S → Set) where
     nothing⇒∀¬STS comp≡nothing s' h rewrite ≡-just⇔STS .Equivalence.from h =
       case comp≡nothing of λ ()
 
+    recomputeProof : ∀ {Γ s sig s'} → STS Γ s sig s' → Maybe (∃[ s'' ] STS Γ s sig s'')
+    recomputeProof _ = computeProof _ _ _
+
 module _ {STS : C → S → Sig → S → Set} (comp : Computational STS) where
 
   open Computational comp

src/Interface/Decidable/Instance.agda

@@ -11,6 +11,8 @@ open import Data.Maybe using (Maybe; just; nothing; Is-just)
 open import Data.Maybe.Relation.Unary.Any using (just)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Sum.Relation.Unary.All using (inj₁; inj₂) renaming (All to All⊎)
+import Data.Rational as ℚ using (_≤_)
+import Data.Rational.Properties as ℚ using (_≤?_)
 
 open import Relation.Binary renaming (Decidable to Decidable²)
 open import Relation.Binary.PropositionalEquality using (_≡_)
@@ -87,3 +89,6 @@ instance
     with ¿ Q y ¿
   ... | yes qy = yes (inj₂ qy)
   ... | no ¬qy = no  λ where (inj₂ qy) → ¬qy qy
+
+  Dec-ℚ≤ : ∀ {q r} → Dec (q ℚ.≤ r)
+  Dec-ℚ≤ = Decidable²⇒Dec ℚ._≤?_

src/Ledger/Chain.lagda

@@ -181,11 +181,11 @@ data
 \begin{figure*}[h]
 \begin{code}
   CHAIN :
-    let open ChainState s; open Block b; open NewEpochState nes; open EnactState es in
-       record { stakeDistrs = calculateStakeDistrs ls }
+    let open ChainState s; open Block b; open EnactState (newEpochState .NewEpochState.es) in
+       record { stakeDistrs = calculateStakeDistrs (newEpochState .NewEpochState.ls) }
          ⊢ newEpochState ⇀⦇ epoch slot ,NEWEPOCH⦈ nes
     →  ⟦ slot , constitution .proj₁ .proj₂ , pparams .proj₁ ⟧ˡᵉ
-         ⊢ ls ⇀⦇ ts ,LEDGERS⦈ ls'
+         ⊢ nes .NewEpochState.ls ⇀⦇ ts ,LEDGERS⦈ ls'
     ────────────────────────────────
     _ ⊢ s ⇀⦇ b ,CHAIN⦈ record s { newEpochState = record nes { ls = ls' } }
 \end{code}

src/Ledger/Chain/Properties.agda

@@ -5,35 +5,58 @@ open import Data.Nat.Properties hiding (_≟_)
 open import Ledger.Prelude
 open import Ledger.Transaction
 open import Ledger.Abstract
+import Data.Maybe
 
 module Ledger.Chain.Properties
   (txs : _) (open TransactionStructure txs)
   (abs : AbstractFunctions txs) (open AbstractFunctions abs)
   where
 
 open import Ledger.Ratify txs
+open import Ledger.Ledger.Properties txs abs
 open import Ledger.Ratify.Properties txs
 open import Ledger.Chain txs abs
 open import Ledger.Ledger txs abs
 
--- TODO: get rid of all of those arguments once we have them globally
-
-module _ (accepted? : ∀ Γ es st → Dec (accepted Γ es st))
-         (expired? : ∀ e st → Dec (expired e st))
-         (delayed? : ∀ a p es d → Dec (delayed a p es d))
-         (Computational-ENACT : Computational _⊢_⇀⦇_,ENACT⦈_) where
-
-  NEWEPOCH-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,NEWEPOCH⦈ s'
-  NEWEPOCH-total {Γ} {nes} {e} =
-    let open NewEpochState nes hiding (es)
-        open RatifyState fut using (removed) renaming (es to esW)
-        open LState ls; open CertState certState; open Acnt acnt
-        es         = record esW { withdrawals = ∅ᵐ }
-        govSt'     = filter (λ x → ¿ ¬ proj₁ x ∈ mapˢ proj₁ removed ¿) govSt
-        (_ , pFut) = RATIFY-total accepted? expired? delayed? Computational-ENACT
-          {record { currentEpoch = e ; treasury = treasury
-                  ; GState gState ; NewEpochEnv Γ }} {⟦ es , ∅ , false ⟧ʳ} {govSt'}
-    in
+open Computational ⦃...⦄
+
+module _ {Γ : NewEpochEnv} {nes : NewEpochState} {e : Epoch} where
+
+  open NewEpochState nes hiding (es)
+  open RatifyState fut using (removed) renaming (es to esW)
+  open LState ls; open CertState certState; open Acnt acnt
+  es         = record esW { withdrawals = ∅ᵐ }
+  govSt'     = filter (λ x → ¿ ¬ proj₁ x ∈ mapˢ proj₁ removed ¿) govSt
+
+  NEWEPOCH-total : ∃[ nes' ] Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes'
+  NEWEPOCH-total =
     case e ≟ sucᵉ lastEpoch of λ where
       (no ¬p) → -, NEWEPOCH-Not-New ¬p
-      (yes p) → -, NEWEPOCH-New p pFut
+      (yes p) → -, NEWEPOCH-New p (pFut .proj₂)
+    where pFut = RATIFY-total {record { currentEpoch = e ; treasury = treasury
+                                      ; GState gState ; NewEpochEnv Γ }}
+                              {⟦ es , ∅ , false ⟧ʳ} {govSt'}
+
+  NEWEPOCH-complete : ∀ nes' → Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes' → NEWEPOCH-total .proj₁ ≡ nes'
+  NEWEPOCH-complete nes' h with h | e ≟ sucᵉ lastEpoch
+  ... | NEWEPOCH-New next _    | no ¬next = ⊥-elim (¬next next)
+  ... | NEWEPOCH-Not-New _     | no _     = refl
+  ... | NEWEPOCH-New _ h       | yes _    = cong ⟦ _ , _ , _ , _ ,_⟧ⁿᵉ (RATIFY-complete h)
+  ... | NEWEPOCH-Not-New ¬next | yes next = ⊥-elim (¬next next)
+
+instance
+  Computational-NEWEPOCH : Computational _⊢_⇀⦇_,NEWEPOCH⦈_
+  Computational-NEWEPOCH .computeProof Γ s sig = just NEWEPOCH-total
+  Computational-NEWEPOCH .completeness Γ s sig s' h = cong just (NEWEPOCH-complete s' h)
+
+  Computational-CHAIN : Computational _⊢_⇀⦇_,CHAIN⦈_
+  Computational-CHAIN .computeProof Γ s b = do
+    _ , neStep ← computeProof _ _ _
+    _ , lsStep ← computeProof _ _ _
+    just (_ , CHAIN neStep lsStep)
+    where open Data.Maybe using (_>>=_)
+  Computational-CHAIN .completeness Γ s b s' (CHAIN neStep lsStep)
+    with recomputeProof neStep | completeness _ _ _ _ neStep
+  ... | _      | refl
+    with recomputeProof lsStep | completeness _ _ _ _ lsStep
+  ... | just _ | refl = refl

src/Ledger/Introduction.lagda

@@ -5,6 +5,9 @@
 module Ledger.Introduction where
 
 open import Prelude
+import Data.Maybe as Maybe
+open import Data.Maybe.Properties
+open import Relation.Binary.PropositionalEquality
 \end{code}
 
 Repository: https://github.com/input-output-hk/formal-ledger-specifications
@@ -39,7 +42,7 @@ other, forming a directed graph that is almost a tree.
 
 Since all such state machines need to be evaluated by the node and all
 nodes should compute the same states, the relations specified by them
-should be computable by functions. This is captured by the following
+should be computable by functions. This can be captured by the following
 record, which is parametrized over the step relation.
 
 \begin{code}[hide]
@@ -55,8 +58,14 @@ record Computational (_⊢_⇀⦇_,X⦈_ : C → S → Sig → S → Set) : Set
   field
     compute     : C → S → Sig → Maybe S
     ≡-just⇔STS  : compute Γ s b ≡ just s' ⇔ Γ ⊢ s ⇀⦇ b ,X⦈ s'
+
+  nothing⇒∀¬STS : compute Γ s b ≡ nothing → ∀ s' → ¬ Γ ⊢ s ⇀⦇ b ,X⦈ s'
 \end{code}
 \end{figure*}
+\begin{code}[hide]
+  nothing⇒∀¬STS comp≡nothing s' h rewrite ≡-just⇔STS .Equivalence.from h =
+    case comp≡nothing of λ ()
+\end{code}
 
 \subsection{Sets \& maps}
 

src/Ledger/Ledger/Properties.agda

@@ -64,6 +64,9 @@ instance
       ... | just (govSt' , _) | refl
         rewrite dec-yes (LEDGER-premises? certSt') h .proj₂ = refl
 
+Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_
+Computational-LEDGERS = it
+
 instance
   HasCoin-LState : HasCoin LState
   HasCoin-LState .getCoin s = getCoin (LState.utxoSt s)

src/Ledger/NewPP.lagda

@@ -40,7 +40,6 @@ votedValue pup pparams quorum =
 private variable
   Γ : NewPParamEnv
   s s' : NewPParamState
-  newpp : PParams
   upd : PParamsUpdate
 
 data _⊢_⇀⦇_,NEWPP⦈_ : NewPParamEnv → NewPParamState → Maybe PParamsUpdate → NewPParamState → Set where
@@ -52,8 +51,8 @@ data _⊢_⇀⦇_,NEWPP⦈_ : NewPParamEnv → NewPParamState → Maybe PParamsU
     ────────────────────────────────
     Γ ⊢ s ⇀⦇ just upd ,NEWPP⦈ ⟦ newpp , updatePPUp newpp ppup ⟧ⁿᵖ
 
-  NEWPP-Reject : ∀ {Γ} → let open NewPParamState s in
-    Γ ⊢ s ⇀⦇ nothing ,NEWPP⦈ ⟦ pparams , updatePPUp newpp ppup ⟧ⁿᵖ
+  NEWPP-Reject : ∀ {Γ} →
+    Γ ⊢ s ⇀⦇ nothing ,NEWPP⦈ s
 \end{code}
 \caption{NEWPP transition system}
 \end{figure*}

src/Ledger/NewPP/Properties.agda

@@ -0,0 +1,29 @@
+{-# OPTIONS --safe #-}
+
+open import Relation.Nullary.Decidable
+
+open import Ledger.Prelude
+open import Ledger.Transaction
+
+module Ledger.NewPP.Properties (txs : _) (open TransactionStructure txs) where
+
+open import Ledger.PPUp txs
+open import Ledger.NewPP txs
+
+instance
+  Computational-NEWPP : Computational _⊢_⇀⦇_,NEWPP⦈_
+  Computational-NEWPP = record {M} where module M Γ s (open NewPParamState s) where
+    computeProof = λ where
+      nothing → just (_ , NEWPP-Reject)
+      (just upd) → let newpp = applyUpdate pparams upd in
+        case ¿ viablePParams newpp ¿ of λ where
+          (yes p) → just (_ , NEWPP-Accept p)
+          (no _)  → nothing
+
+    completeness : _
+    completeness sig s' h with sig | h
+    ... | nothing  | NEWPP-Reject   = refl
+    ... | just upd | NEWPP-Accept p
+      rewrite let newpp = applyUpdate pparams upd in
+              dec-yes (¿ viablePParams newpp ¿) p .proj₂
+              = refl

src/Ledger/Ratify.lagda

@@ -343,46 +343,43 @@ participatingHashes votes r = votedYesHashes votes r ∪ votedHashes Vote.no vot
 The code in Figure~\ref{fig:defs:ratify-ii} defines \votedHashes, which returns the set of delegates who voted a certain way on the given governance role.
 \begin{figure*}[h!]
 {\small
+\begin{code}[hide]
+abstract
+\end{code}
 \begin{code}
-getStakeDist : GovRole → ℙ VDeleg → StakeDistrs → VDeleg ⇀ Coin
-getStakeDist CC    cc  _                             = constMap (filterˢ isCCProp cc) 1
-getStakeDist DRep  _   record { stakeDistr = dist }  = filterᵐ (sp-∘ isDRepProp  proj₁) dist
-getStakeDist SPO   _   record { stakeDistr = dist }  = filterᵐ (sp-∘ isSPOProp   proj₁) dist
-
-acceptedStake : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
-acceptedStake r cc dists votes =
-  Σᵐᵛ[ x ← (getStakeDist r cc dists ∣ votedYesHashes votes r) ᶠᵐ ] x
-
-totalStake : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
-totalStake r cc dists votes =
-  Σᵐᵛ[ x  ← getStakeDist r cc dists ∣ votedAbstainHashes votes r ᶜ ᶠᵐ ] x
-
-activeVotingStake : ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
-activeVotingStake cc dists votes =
-  Σᵐᵛ[ x  ← getStakeDist DRep cc dists ∣ dom votes ᶜ ᶠᵐ ] x
-
-accepted' : RatifyEnv → EnactState → GovActionState → Set
-accepted' Γ (record { cc = cc , _ ; pparams = pparams , _ }) gs =
-  acceptedBy CC ∧ acceptedBy DRep ∧ acceptedBy SPO ∧ meetsMinAVS
-  where
-    open RatifyEnv Γ; open GovActionState gs; open PParams pparams
-
-    votes' = actualVotes Γ cc votes action pparams
-    cc' = dom votes'
-    redStakeDistr = restrictedDists coinThreshold rankThreshold stakeDistrs
-
-    meetsMinAVS : Set
-    meetsMinAVS = activeVotingStake cc' redStakeDistr votes' ≥ minimumAVS
-
-    acceptedBy : GovRole → Set
-    acceptedBy role =
-      let t = maybe id 0ℚ $ threshold pparams (proj₂ <$> cc) action role in
-      case totalStake role cc' redStakeDistr votes' of λ where
-        0 → t ≡ 0ℚ -- if there's no stake, accept only if threshold is zero
-        x@(suc _) → ℤ.+ acceptedStake role cc' redStakeDistr votes' ℚ./ x ℚ.≥ t
-
-expired : Epoch → GovActionState → Set
-expired current record { expiresIn = expiresIn } = expiresIn < current
+  getStakeDist : GovRole → ℙ VDeleg → StakeDistrs → VDeleg ⇀ Coin
+  getStakeDist CC    cc  _                             = constMap (filterˢ isCCProp cc) 1
+  getStakeDist DRep  _   record { stakeDistr = dist }  = filterᵐ (sp-∘ isDRepProp  proj₁) dist
+  getStakeDist SPO   _   record { stakeDistr = dist }  = filterᵐ (sp-∘ isSPOProp   proj₁) dist
+
+  acceptedStake : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
+  acceptedStake r cc dists votes =
+    Σᵐᵛ[ x ← (getStakeDist r cc dists ∣ votedYesHashes votes r) ᶠᵐ ] x
+
+  totalStake : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
+  totalStake r cc dists votes =
+    Σᵐᵛ[ x  ← getStakeDist r cc dists ∣ votedAbstainHashes votes r ᶜ ᶠᵐ ] x
+
+  activeVotingStake : ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
+  activeVotingStake cc dists votes =
+    Σᵐᵛ[ x  ← getStakeDist DRep cc dists ∣ dom votes ᶜ ᶠᵐ ] x
+
+  acceptedBy : (Γ : RatifyEnv) (es : EnactState) (gs : GovActionState) → GovRole → Set
+  acceptedBy Γ (record { cc = cc , _; pparams = pparams , _ }) gs role =
+    let open RatifyEnv Γ; open GovActionState gs; open PParams pparams
+        votes'         = actualVotes Γ cc votes action pparams
+        cc'            = dom votes'
+        redStakeDistr  = restrictedDists coinThreshold rankThreshold stakeDistrs
+        t              = maybe id ℚ.0ℚ $ threshold pparams (proj₂ <$> cc) action role in
+    case totalStake role cc' redStakeDistr votes' of λ where
+      0 → t ≡ ℚ.0ℚ -- if there's no stake, accept only if threshold is zero
+      x@(suc _) → ℤ.+ acceptedStake role cc' redStakeDistr votes' ℚ./ x ℚ.≥ t
+
+  accepted : (Γ : RatifyEnv) (es : EnactState) (gs : GovActionState) → Set
+  accepted Γ es gs = acceptedBy Γ es gs CC ∧ acceptedBy Γ es gs DRep ∧ acceptedBy Γ es gs SPO
+
+  expired : Epoch → GovActionState → Set
+  expired current record { expiresIn = expiresIn } = expiresIn < current
 \end{code}
 } %% end small
 \caption{%%Ratify iii:
@@ -426,6 +423,38 @@ delayingAction Info                   = false
 delayed : (a : GovAction) → NeedsHash a → EnactState → Bool → Set
 delayed a h es d = ¬ verifyPrev a h es ⊎ d ≡ true
 \end{code}
+\begin{code}[hide]
+abstract
+  verifyPrev? : ∀ a h es → Dec (verifyPrev a h es)
+  verifyPrev? NoConfidence           h es = it
+  verifyPrev? (NewCommittee x x₁ x₂) h es = it
+  verifyPrev? (NewConstitution x x₁) h es = it
+  verifyPrev? (TriggerHF x)          h es = it
+  verifyPrev? (ChangePParams x)      h es = it
+  verifyPrev? (TreasuryWdrl x)       h es = it
+  verifyPrev? Info                   h es = it
+
+  delayed? : ∀ a h es d → Dec (delayed a h es d)
+  delayed? a h es d = let instance _ = verifyPrev? a h es in it
+
+  acceptedBy? : ∀ Γ es st role → Dec (acceptedBy Γ es st role)
+  acceptedBy? Γ record{ cc = cc , _ ; pparams = pparams , _ } st role
+    with (let open RatifyEnv Γ; open GovActionState st; open PParams pparams
+              votes' = actualVotes Γ cc votes action pparams
+              cc' = dom votes'
+              redStakeDistr = restrictedDists coinThreshold rankThreshold stakeDistrs
+          in totalStake role cc' redStakeDistr votes')
+  ... | zero  = it
+  ... | suc n = it
+
+  accepted? : ∀ Γ es st → Dec (accepted Γ es st)
+  accepted? Γ es st =
+    let instance _ = λ {role} → acceptedBy? Γ es st role
+    in it
+
+  expired? : ∀ e st → Dec (expired e st)
+  expired? e st = ¿ expired e st ¿
+\end{code}
 } %% end small
 \caption{%Ratify iv:
 Determination of the status of ratification of the governance action}
@@ -446,11 +475,6 @@ private variable
   removed : ℙ (GovActionID × GovActionState)
   d : Bool
 
--- having `accepted` abstract speeds up type checking of RATIFY' a lot
-abstract
-  accepted : RatifyEnv → EnactState → GovActionState → Set
-  accepted = accepted'
-
 data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × GovActionState → RatifyState → Set where
 
 \end{code}
@@ -473,10 +497,9 @@ data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × Gov
 
   RATIFY-Continue : let open RatifyEnv Γ; st = a .proj₂; open GovActionState st in
        ¬ accepted Γ es st × ¬ expired currentEpoch st
-    ⊎  delayed action prevAction es d
     ⊎  accepted Γ es st
-       × ¬ delayed action prevAction es d
-       × (∀ es' → ¬ ⟦ a .proj₁ , treasury , currentEpoch ⟧ᵉ ⊢ es ⇀⦇ action ,ENACT⦈ es')
+       × (delayed action prevAction es d ⊎
+          (∀ es' → ¬ ⟦ a .proj₁ , treasury , currentEpoch ⟧ᵉ ⊢ es ⇀⦇ action ,ENACT⦈ es'))
     ────────────────────────────────
     Γ ⊢ ⟦ es , removed , d ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es , removed , d ⟧ʳ