Weight function

src/Peras/Chain.lagda.md

@@ -164,10 +164,6 @@ module _ ⦃ _ : Hashable Block ⦄
 ```agda
   open Hashable ⦃...⦄
 ```
-```agda
-  pointsInto : Certificate → Chain → Bool
-  pointsInto c ch = any (λ b → (blockRef c == hash b)) ch
-```
 ```agda
   StartOfRound : SlotNumber → RoundNumber → Set
   StartOfRound (MkSlotNumber sl) (MkRoundNumber r) = sl ≡ r * U
@@ -183,15 +179,20 @@ module _ ⦃ _ : Hashable Block ⦄
 ### Chain weight
 
 The weight of a chain is defined with respect of the Peras parameters
-
 ```agda
   weight : Chain → List Certificate → Nat
-  weight ch cts = len ch + len (filter (flip pointsInto ch) cts) * B
+  weight ch cts = chainWeight' 0 ch
     where
-      len : ∀ {a : Set} → List a → Nat
-      len = foldr (const suc) 0
-```
+      isCertified : Block → Bool
+      isCertified block = any (λ cert → hash block == blockRef cert) cts
 
+      chainWeight' : Nat → Chain → Nat
+      chainWeight' accum [] = accum
+      chainWeight' accum (block ∷ blocks) =
+        if isCertified block
+          then chainWeight' (accum + 1 + B) blocks
+          else chainWeight' (accum + 1) blocks
+```
 ### Chain validity
 
 ```agda

src/Peras/Conformance/Soundness.agda

@@ -14,7 +14,7 @@ import Data.List.Relation.Unary.Any as Any
 import Data.List.Relation.Unary.All as All
 
 open import Data.List.Relation.Unary.Any.Properties
-open import Data.Nat using (NonZero; ℕ; _≡ᵇ_; _≥_; _>_; _≥?_; _>?_; _≤?_)
+open import Data.Nat using (NonZero; ℕ; _≡ᵇ_; _≥_; _>_; _≥?_; _>?_; _≤?_; _≤_)
 open import Data.Nat.Properties
 open import Data.Nat.DivMod
 open import Data.Maybe using (maybe; maybe′; nothing; just)
@@ -115,15 +115,6 @@ module _ ⦃ postulates : Postulates ⦄
     open SmallStep using (⦅_,_,_,_⦆)
     open SmallStep.Message
 
-    open import Data.List.Membership.Propositional
-    import Data.List.Relation.Unary.All as All
-
-{-
-    postulate
-      maximumBy-default-or-∈ : ∀ {a : Set} → (d : a) → (o : a → a → Ordering) → (l : List a)
-        → maximumBy d o l ∈ d ∷ l
--}
-
     addChain'' : NodeModel → {c : Chain} → ValidChain c → NodeModel
     addChain'' s {c} _ = addChain' s c
 
@@ -134,7 +125,7 @@ module _ ⦃ postulates : Postulates ⦄
       SmallStep.IsTreeType
         initialModelState
         addChain''
-        allChains -- (λ t → genesisChain ∷ allChains t)
+        allChains -- TODO: (λ t → genesisChain ∷ allChains t)
         pref
         addVote''
         allVotes
@@ -148,12 +139,10 @@ module _ ⦃ postulates : Postulates ⦄
         ; instantiated-votes = refl
         ; extendable-votes = λ _ _ → Any.here refl
         ; extendable-chain = λ _ _ → refl
-        ; self-contained-certs = λ _ _ → {!refl!}
+        ; self-contained-certs = λ _ _ → {!!}
         ; valid = {!!}
-        ; optimal = {!!} -- ok
+        ; optimal = {!!} -- TODO: proof
         ; self-contained = {!!} -- λ t → maximumBy-default-or-∈ genesisChain _ (allChains t)
---        ; unique-votes = {!!}
---        ; no-equivocations = {!!}
 --        ; quorum-cert = {!!} -- invariants
         }
 

src/Peras/SmallStep.lagda.md

@@ -109,11 +109,11 @@ has to fulfil all the properties mentioned below:
   record IsTreeType {T : Set}
                     (tree₀ : T)
                     (addChain : T → {c : Chain} → ValidChain c → T)
-                    (chains : T → List Chain)
+                    (chains : T → List Chain) -- TODO: use Set instead of List
                     (preferredChain : T → Chain)
                     (addVote : T → {v : Vote} → ValidVote v → T)
-                    (votes : T → List Vote)
-                    (certs : T → List Certificate)
+                    (votes : T → List Vote) -- TODO: use Set instead of List
+                    (certs : T → List Certificate) -- TODO: use Set instead of List
                     (cert₀ : Certificate)
          : Set₁ where
 
@@ -144,29 +144,21 @@ Properties that must hold with respect to chains, certificates and votes.
         → ValidChain (preferredChain t)
 
       optimal : ∀ (c : Chain) (t : T)
-        → let
-            b = preferredChain t
-            cts = certs t
-          in
-          ValidChain c
         → c ∈ chains t
-        → weight c cts ≤ weight b cts
+        → weight c (certs t) ≤ weight (preferredChain t) (certs t)
 
       self-contained : ∀ (t : T)
         → preferredChain t ∈ chains t
 
-{-
+{-    -- TODO: use Set instead of List for votes
       unique-votes : ∀ (t : T) {v : Vote} (vv : ValidVote v)
-        → let vs = votes t
-          in
-          v ∈ vs
-        → vs ≡ votes (addVote t vv)
-
+        → v ∈ votes t
+        → votes t ≡ votes (addVote t vv)
+-}
+{-    -- TODO: use Set with `equivocation` as equivalence relation for votes
       no-equivocations : ∀ (t : T) {v : Vote} (vv : ValidVote v)
-        → let vs = votes t
-          in
-          Any (v ∻_) vs
-        → vs ≡ votes (addVote t vv)
+        → Any (v ∻_) (votes t)
+        → votes t ≡ votes (addVote t vv)
 -}
 {-
       quorum-cert : ∀ (t : T) (b : Block) (r : ℕ)