Fix Extends in formal specification

peras-simulation/src/Peras/Block.hs

@@ -67,4 +67,4 @@ tipHash [] = MkHash emptyBS
 tipHash (x : _) = hash x
 
 instance Hashable Block where
-  hash = \x -> MkHash (bytesS (signature x))
+  hash = MkHash . (\r -> bytesS r) . \r -> signature r

peras-simulation/src/Peras/Conformance/Model.hs

@@ -7,15 +7,14 @@
 module Peras.Conformance.Model where
 
 import Control.Monad (guard)
-import Data.Maybe (mapMaybe)
 import Numeric.Natural (Natural)
 import Peras.Block (Block (MkBlock, certificate, creatorId, leadershipProof, parentBlock, signature, slotNumber), Certificate (MkCertificate, blockRef, round), PartyId, tipHash)
 import Peras.Chain (Chain, Vote (MkVote, blockHash, votingRound), insertCert)
 import Peras.Conformance.Params (PerasParams (MkPerasParams, perasA, perasB, perasK, perasL, perasR, perasU, perasτ), defaultPerasParams)
 import Peras.Crypto (Hash (MkHash), Hashable (hash), emptyBS)
 import Peras.Foreign (checkLeadershipProof, checkSignedBlock, checkSignedVote, createLeadershipProof, createMembershipProof, createSignedBlock, createSignedVote, mkParty)
 import Peras.Numbering (RoundNumber (getRoundNumber), SlotNumber (getSlotNumber), nextRound, nextSlot, slotInRound, slotToRound)
-import Peras.Util (comparing, maximumBy, maybeToList)
+import Peras.Util (comparing, decP, decS, eqDec, ge, gt, isYes, mapMaybe, maximumBy, maybeToList)
 
 import Control.Monad.Identity
 import Data.Function (on)
@@ -271,36 +270,20 @@ hasVoted :: PartyId -> RoundNumber -> NodeModel -> Bool
 hasVoted p r s =
   any (\v -> p == voterId v && r == votingRound v) (allVotes s)
 
-isYes :: Bool -> Bool
-isYes True = True
-isYes False = False
-
-decP :: Bool -> Bool -> Bool
-decP va vb = va && vb
-
-decS :: Bool -> Bool -> Bool
-decS va vb = va || vb
-
 (===) :: RoundNumber -> RoundNumber -> Bool
 x === y = x == y
 
-eq :: Integer -> Integer -> Bool
-eq = (==)
-
-gt :: Integer -> Integer -> Bool
-gt = gtInteger
-
-ge :: Integer -> Integer -> Bool
-ge = geInteger
-
 vr1A :: NodeModel -> Bool
-vr1A s = nextRound (round (cert' s)) === rFromSlot s
+vr1A s = rFromSlot s === nextRound (round (cert' s))
 
 vr1B' :: NodeModel -> Bool
 vr1B' s = extends (votingBlockHash s) (cert' s) (allChains s)
 
+extendsDec :: Hash Block -> Certificate -> [Chain] -> Bool
+extendsDec h c ch = extends h c ch
+
 vr1B :: NodeModel -> Bool
-vr1B s = vr1B' s
+vr1B s = extendsDec (votingBlockHash s) (cert' s) (allChains s)
 
 vr2A :: NodeModel -> Bool
 vr2A s =
@@ -315,9 +298,15 @@ vr2B s =
         (getRoundNumber (rFromSlot s))
         (getRoundNumber (round (certS s)))
     )
-    ( eq
-        (mod (getRoundNumber (rFromSlot s)) (perasK (protocol s)))
-        (mod (getRoundNumber (round (certS s))) (perasK (protocol s)))
+    ( eqDec
+        ( mod
+            (fromIntegral (getRoundNumber (rFromSlot s)))
+            (fromIntegral (perasK (protocol s)))
+        )
+        ( mod
+            (fromIntegral (getRoundNumber (round (certS s))))
+            (fromIntegral (perasK (protocol s)))
+        )
     )
 
 checkVotingRules :: NodeModel -> Bool

peras-simulation/src/Peras/Util.hs

@@ -1,5 +1,9 @@
 module Peras.Util where
 
+import Numeric.Natural (Natural)
+
+import GHC.Integer
+
 maybeToList :: Maybe a -> [a]
 maybeToList Nothing = []
 maybeToList (Just x) = [x]
@@ -17,3 +21,32 @@ maximumBy candidate f (x : xs) =
 
 comparing :: Ord b => (a -> b) -> a -> a -> Ordering
 comparing f x y = compare (f x) (f y)
+
+mapMaybe :: (a -> Maybe b) -> [a] -> [b]
+mapMaybe p [] = []
+mapMaybe p (x : xs) =
+  case p x of
+    Just y -> y : mapMaybe p xs
+    Nothing -> mapMaybe p xs
+
+isYes :: Bool -> Bool
+isYes True = True
+isYes False = False
+
+decP :: Bool -> Bool -> Bool
+decP va vb = va && vb
+
+decS :: Bool -> Bool -> Bool
+decS va vb = va || vb
+
+eqDec :: Natural -> Natural -> Bool
+eqDec x y = x == y
+
+eq :: Integer -> Integer -> Bool
+eq = (==)
+
+gt :: Integer -> Integer -> Bool
+gt = gtInteger
+
+ge :: Integer -> Integer -> Bool
+ge = geInteger

rewrites.yaml

@@ -2,7 +2,3 @@ rewrites:
   - from: "Peras.Crypto.ByteString"
     to: "ByteString"
     importing: "Data.ByteString"
-
-  - from: "Data.List.Base.mapMaybe"
-    to: "mapMaybe"
-    importing: "Data.Maybe"

src/Peras/Block.lagda.md

@@ -4,25 +4,9 @@ module Peras.Block where
 
 <!--
 ```agda
-open import Data.Bool using (Bool; true; false)
-open import Data.List using (List; null; head; filter)
-open import Data.List.Membership.Propositional using (_∈_; _∉_)
-open import Data.Maybe using (Maybe; maybe′; just; nothing)
-open import Data.Nat using (ℕ)
-open import Data.Nat.Properties using (<-strictTotalOrder)
-open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax; _×_; proj₁; proj₂)
-open import Data.Unit using (⊤)
-open import Function using (_∘_)
-open import Haskell.Prelude as Haskell using (Eq; _==_; True; False; _&&_)
-open import Level using (0ℓ)
-open import Relation.Binary using (StrictTotalOrder; DecidableEquality)
-open import Relation.Nullary using (yes; no; ¬_)
-
-open import Data.Nat.Properties using (≤-totalOrder)
-open import Data.List.Extrema (≤-totalOrder) using (argmax)
-
-import Relation.Binary.PropositionalEquality as Equ
-open Equ using (_≡_; _≢_; cong)
+open import Haskell.Prelude
+
+open import Data.Product using (∃; ∃-syntax)
 
 open import Peras.Crypto
 open import Peras.Numbering
@@ -44,7 +28,7 @@ import qualified Peras.Block as G
 ## PartyId
 
 ```agda
-PartyId = ℕ  -- FIXME: Data.Fin ?
+PartyId = Nat
 ```
 
 <!--
@@ -68,7 +52,7 @@ open Party public
 
 instance
   iPartyEq : Eq Party
-  iPartyEq .Haskell._==_ x y = pid x Haskell.== pid y && pkey x Haskell.== pkey y
+  iPartyEq ._==_ x y = pid x == pid y && pkey x == pkey y
 ```
 
 <!--
@@ -90,23 +74,12 @@ data Honesty : PartyId → Set where
   Corrupt : ∀ {p : PartyId}
     → Honesty p
 ```
+
 ```agda
 PartyTup = ∃[ p ] (Honesty p)
 Parties = List PartyTup
 ```
 
-```agda
-postulate
-  Honest≢Corrupt : ∀ {p₁ p₂} {h₁ : Honesty p₁} {h₂ : Honesty p₂}
-    → h₁ ≡ Honest
-    → h₂ ≡ Corrupt
-    → p₁ ≢ p₂
-
-isHonest : ∀ {p : PartyId} → Honesty p → Bool
-isHonest {p} Honest = true
-isHonest {p} Corrupt = false
-```
-
 ## Transactions
 
 ```agda
@@ -136,10 +109,11 @@ Payload = List Tx
 
 record Certificate where
   constructor MkCertificate
+  pattern
   field round : RoundNumber
         blockRef : Hash Block
 
-  roundNumber : ℕ
+  roundNumber : Nat
   roundNumber = getRoundNumber round
 
 open Certificate public
@@ -157,31 +131,18 @@ record Block where
         signature : Signature
         bodyHash : Hash Payload
 
-  slotNumber' : ℕ
+  slotNumber' : Nat
   slotNumber' = getSlotNumber slotNumber
 
 open Block public
 
-_≟-BlockHash_ : DecidableEquality (Hash Block)
-(MkHash b₁) ≟-BlockHash (MkHash b₂) with b₁ ≟-BS b₂
-... | yes p = yes (cong MkHash p)
-... | no ¬p =  no (¬p ∘ cong hashBytes)
-
 record BlockBody where
   constructor MkBlockBody
   field blockHash : Hash Payload
         payload : Payload
 
 open BlockBody public
 ```
-```agda
-data HonestBlock : Block → Set where
-
-  HonestParty : ∀ {p : PartyId} {h : Honesty p} {b : Block}
-    → creatorId b ≡ p
-    → h ≡ Honest {p}
-    → HonestBlock b
-```
 <!--
 ```agda
 {-# COMPILE AGDA2HS Payload #-}
@@ -191,19 +152,10 @@ data HonestBlock : Block → Set where
 {-# COMPILE GHC BlockBody = data G.BlockBody (G.MkBlockBody) #-}
 {-# COMPILE AGDA2HS Certificate deriving (Generic) #-}
 {-# COMPILE GHC Certificate = data G.Certificate (G.MkCertificate) #-}
-
-instance
-  iMaybeEq : {a : Set} → ⦃ i : Eq a ⦄ → Eq (Maybe a)
-  iMaybeEq {{i}} ._==_ x y =
-    maybe′
-      (λ x' → maybe′ (λ y' → x' == y') False y)
-      (maybe′ (λ _ → False) True y)
-      x
 ```
 -->
 
 ```agda
-
 instance
   iCertificateEq : Eq Certificate
   iCertificateEq ._==_ x y = round x == round y && blockRef x == blockRef y
@@ -229,25 +181,18 @@ module _ {a : Set} ⦃ _ : Hashable a ⦄
   open Hashable ⦃...⦄
 
   tipHash : List a → Hash a
-  tipHash Data.List.[] = MkHash emptyBS
-  tipHash (x Data.List.∷ _) = hash x
-
-{-# COMPILE AGDA2HS tipHash #-}
+  tipHash [] = MkHash emptyBS
+  tipHash (x ∷ _) = hash x
 
 private
   open Hashable
-
   instance
     hashBlock : Hashable Block
     hashBlock .hash = MkHash ∘ bytesS ∘ signature
-```
 
-<!--
-```agda
+{-# COMPILE AGDA2HS tipHash #-}
 {-# COMPILE AGDA2HS iCertificateEq #-}
 {-# COMPILE AGDA2HS iBlockEq #-}
 {-# COMPILE AGDA2HS iBlockBodyEq #-}
-
 {-# COMPILE AGDA2HS hashBlock #-}
 ```
--->