Fix computation of commonPrefix from Agda

It's been a lengthy process but I finally nailed down the issue with
commonPrefix computation, shaving a few yaks related to Read/Show
instances consistency in the process.

peras-hs/peras-hs.cabal

@@ -42,9 +42,10 @@ test-suite test
     other-modules:    Peras.ChainSpec
     build-depends:
                       base >= 4.9 && <5
-                    , QuickCheck
-                    , hspec
-                    , peras-hs
+                  , QuickCheck
+                  , hspec
+                  , peras-hs
+                  , quickcheck-classes
 
     build-tool-depends:
        hspec-discover:hspec-discover

peras-hs/src/Peras/Arbitraries.hs

@@ -10,7 +10,13 @@ import GHC.Generics (Generic)
 import Generic.Random (genericArbitrary, uniform)
 import Peras.Block (Block (..), PartyId (..), Tx (..))
 import Peras.Chain (Chain (..), asChain)
-import Peras.Crypto (Hash (..), LeadershipProof (..), Signature (..), VerificationKey (..))
+import Peras.Crypto (
+  Hash (..),
+  LeadershipProof (..),
+  MembershipProof (..),
+  Signature (..),
+  VerificationKey (..),
+ )
 import Peras.Orphans ()
 import Test.QuickCheck (Arbitrary (..), Gen, choose, vectorOf)
 import Test.QuickCheck.Instances.Natural ()
@@ -27,6 +33,9 @@ instance Arbitrary Signature where
 instance Arbitrary LeadershipProof where
   arbitrary = LeadershipProof <$> genByteString 4
 
+instance Arbitrary MembershipProof where
+  arbitrary = MembershipProof <$> genByteString 4
+
 instance Arbitrary VerificationKey where
   arbitrary = VerificationKey <$> genByteString 4
 
@@ -41,7 +50,7 @@ instance (Arbitrary t, Generic t) => Arbitrary (Block t) where
   shrink block@Block{payload} =
     [block{payload = payload'} | payload' <- shrink payload]
 
-instance (Arbitrary t, Generic t) => Arbitrary (Chain t) where
+instance (Eq t, Arbitrary t, Generic t) => Arbitrary (Chain t) where
   arbitrary = asChain <$> arbitrary
 
   shrink = \case

peras-hs/src/Peras/Block.hs

@@ -9,8 +9,8 @@ import Data.ByteString as BS
 data PartyId = MkPartyId{vkey :: VerificationKey}
                  deriving (Eq)
 
-data Tx = Tx{tx :: ByteString}
-            deriving Eq
+newtype Tx = Tx{tx :: ByteString}
+               deriving Eq
 
 type Slot = Natural
 

peras-hs/src/Peras/Chain.hs

@@ -1,44 +1,44 @@
 {-# LANGUAGE ScopedTypeVariables #-}
-
 module Peras.Chain where
 
 import Peras.Block (Block)
 
-data Chain t
-  = Genesis
-  | Cons (Block t) (Chain t)
-  deriving (Eq)
+data Chain t = Genesis
+             | Cons (Block t) (Chain t)
+                 deriving (Eq)
 
 foldl1Maybe :: (a -> a -> a) -> [a] -> Maybe a
-foldl1Maybe f xs =
-  foldl
-    ( \m y ->
-        Just
-          ( case m of
-              Nothing -> y
-              Just x -> f x y
-          )
-    )
-    Nothing
-    xs
-
-asList :: forall t. Eq t => Chain t -> [Block t]
+foldl1Maybe f xs
+  = foldl
+      (\ m y ->
+         Just
+           (case m of
+                Nothing -> y
+                Just x -> f x y))
+      Nothing
+      xs
+
+asList :: forall t . Eq t => Chain t -> [Block t]
 asList Genesis = []
 asList (Cons x c) = x : asList c
 
-asChain :: forall t. Eq t => [Block t] -> Chain t
+asChain :: forall t . Eq t => [Block t] -> Chain t
 asChain [] = Genesis
 asChain (x : bs) = Cons x (asChain bs)
 
-prefix :: forall t. Eq t => [Block t] -> [Block t] -> [Block t]
-prefix (x : xs) (y : ys) = if x == y then x : prefix xs ys else []
-prefix _ _ = []
-
-commonPrefix :: forall t. Eq t => [Chain t] -> Chain t
-commonPrefix chains =
-  case listPrefix of
-    Nothing -> Genesis
-    Just bs -> asChain bs
- where
-  listPrefix :: Maybe [Block t]
-  listPrefix = foldl1Maybe prefix (reverse (map asList chains))
+prefix ::
+       forall t . Eq t => [Block t] -> [Block t] -> [Block t] -> [Block t]
+prefix acc (x : xs) (y : ys)
+  = if x == y then prefix (x : acc) xs ys else reverse acc
+prefix acc _ _ = reverse acc
+
+commonPrefix :: forall t . Eq t => [Chain t] -> Chain t
+commonPrefix chains
+  = case listPrefix of
+        Nothing -> Genesis
+        Just bs -> asChain (reverse bs)
+  where
+    listPrefix :: Maybe [Block t]
+    listPrefix
+      = foldl1Maybe (prefix []) (map (\ l -> reverse (asList l)) chains)
+

peras-hs/src/Peras/Crypto.hs

@@ -2,20 +2,19 @@ module Peras.Crypto where
 
 import Data.ByteString as BS
 
-newtype Hash = Hash {hash :: ByteString}
-  deriving (Eq)
+newtype Hash = Hash{hash :: ByteString}
+                 deriving Eq
 
-newtype MembershipProof = MembershipProof {proofM :: ByteString}
-  deriving (Eq)
+newtype MembershipProof = MembershipProof{proofM :: ByteString}
+                            deriving Eq
 
-newtype LeadershipProof = LeadershipProof {proof :: ByteString}
-  deriving (Eq)
+newtype LeadershipProof = LeadershipProof{proof :: ByteString}
+                            deriving Eq
 
-newtype Signature = Signature {signature :: ByteString}
-  deriving (Eq)
+newtype Signature = Signature{signature :: ByteString}
+                      deriving Eq
+
+newtype VerificationKey = VerificationKey{verificationKey ::
+                                          ByteString}
+                            deriving Eq
 
-newtype VerificationKey = VerificationKey
-  { verificationKey ::
-      ByteString
-  }
-  deriving (Eq)

peras-hs/src/Peras/Orphans.hs

@@ -7,16 +7,13 @@
 {-# LANGUAGE TupleSections #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
-module Peras.Orphans (
-  fromBlocks,
-  toBlocks,
-) where
+module Peras.Orphans where
 
 import Data.Bifunctor (first)
 import Data.String (IsString (..))
 import GHC.Generics (Generic)
 import Peras.Block (Block (..), PartyId (..), Tx (..))
-import Peras.Chain (Chain (..))
+import Peras.Chain (Chain (..), asChain, asList)
 import Peras.Crypto (Hash (..), LeadershipProof (..), MembershipProof (..), Signature (..), VerificationKey (..))
 import Peras.Message (Message (..), NodeId (..))
 
@@ -26,18 +23,21 @@ import qualified Data.ByteString as BS
 import qualified Data.ByteString.Base16 as B16
 import qualified Data.ByteString.Char8 as BS8
 import qualified Data.Text as T
+import Text.Read (Read (readPrec), readListDefault)
 
 -- Only used for deriving instances of similar types.
 newtype Bytes = Bytes {getBytes :: BS.ByteString}
 
 instance Read Bytes where
-  readsPrec _ = either mempty (pure . (,"") . Bytes) . B16.decode . BS8.pack
+  readPrec = do
+    Right bs <- B16.decode . BS8.pack <$> readPrec
+    pure $ Bytes bs
 
 instance Show Bytes where
-  show = BS8.unpack . B16.encode . getBytes
+  show = show . BS8.unpack . B16.encode . getBytes
 
 instance IsString Bytes where
-  fromString = read
+  fromString = either error Bytes . B16.decode . BS8.pack
 
 instance A.FromJSON Bytes where
   parseJSON = A.withText "Base 16 Bytes" $ either A.parseFail (pure . Bytes) . B16.decode . BS8.pack . T.unpack
@@ -81,26 +81,15 @@ deriving stock instance Ord v => Ord (Chain v)
 deriving stock instance Read v => Read (Chain v)
 deriving stock instance Show v => Show (Chain v)
 
-fromBlocks ::
-  [Block v] ->
-  Chain v
-fromBlocks = foldr Cons Genesis
-
-toBlocks ::
-  Chain v ->
-  [Block v]
-toBlocks Genesis = []
-toBlocks (Cons block chain) = toBlocks chain <> pure block
-
-instance A.FromJSON v => A.FromJSON (Chain v) where
+instance (A.FromJSON v, Eq v) => A.FromJSON (Chain v) where
   parseJSON =
     A.withObject "Chain" $
-      \o -> fromBlocks <$> o A..: "blocks"
+      \o -> asChain <$> o A..: "blocks"
 
-instance A.ToJSON v => A.ToJSON (Chain v) where
+instance (A.ToJSON v, Eq v) => A.ToJSON (Chain v) where
   toJSON chain =
     A.object
-      [ "blocks" A..= toBlocks chain
+      [ "blocks" A..= asList chain
       ]
 
 deriving stock instance Generic Hash
@@ -117,7 +106,7 @@ deriving stock instance Ord v => Ord (Message v)
 deriving stock instance Read v => Read (Message v)
 deriving stock instance Show v => Show (Message v)
 
-instance A.FromJSON v => A.FromJSON (Message v) where
+instance (A.FromJSON v, Eq v) => A.FromJSON (Message v) where
   parseJSON =
     A.withObject "Message" $
       \o ->
@@ -129,7 +118,7 @@ instance A.FromJSON v => A.FromJSON (Message v) where
             "NewChain" -> NewChain <$> o A..: "chain"
             _ -> A.parseFail $ "Illegal input: " <> input
 
-instance A.ToJSON v => A.ToJSON (Message v) where
+instance (A.ToJSON v, Eq v) => A.ToJSON (Message v) where
   toJSON (NextSlot slot) =
     A.object
       [ "input" A..= ("NextSlot" :: String)
@@ -173,7 +162,7 @@ instance Show NodeId where
   show = nodeId
 
 instance IsString NodeId where
-  fromString = read
+  fromString = MkNodeId
 
 instance A.FromJSON NodeId where
   parseJSON = A.withText "NodeId" $ pure . MkNodeId . T.unpack
@@ -196,6 +185,9 @@ instance Read PartyId where
 instance Show PartyId where
   show = show . vkey
 
+instance IsString PartyId where
+  fromString = MkPartyId . fromString
+
 instance A.FromJSON PartyId where
   parseJSON = fmap MkPartyId . A.parseJSON
 
@@ -218,21 +210,11 @@ deriving via Bytes instance A.ToJSON Signature
 
 deriving stock instance Generic Tx
 deriving stock instance Ord Tx
-
-instance Read Tx where
-  readsPrec _ = either mempty (pure . (,"") . Tx) . B16.decode . BS8.pack
-
-instance Show Tx where
-  show = BS8.unpack . B16.encode . tx
-
-instance IsString Tx where
-  fromString = read
-
-instance A.FromJSON Tx where
-  parseJSON = A.withText "Base 16 Bytes" $ either A.parseFail (pure . Tx) . B16.decode . BS8.pack . T.unpack
-
-instance A.ToJSON Tx where
-  toJSON = A.String . T.pack . show
+deriving via Bytes instance Read Tx
+deriving via Bytes instance Show Tx
+deriving via Bytes instance IsString Tx
+deriving via Bytes instance A.FromJSON Tx
+deriving via Bytes instance A.ToJSON Tx
 
 deriving stock instance Generic VerificationKey
 deriving stock instance Ord VerificationKey

peras-hs/test/Peras/ChainSpec.hs

@@ -1,18 +1,57 @@
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeApplications #-}
 
 module Peras.ChainSpec where
 
+import Data.Data (Proxy (..))
 import Peras.Arbitraries ()
-import Peras.Chain (Chain, asChain, asList, commonPrefix)
+import Peras.Block (Block (..), PartyId, Slot, Tx)
+import Peras.Chain (Chain (..), asChain, asList, commonPrefix, prefix)
+import Peras.Crypto (Hash, LeadershipProof, MembershipProof)
 import Peras.Orphans ()
-import Test.Hspec (Spec)
+import Test.Hspec (Spec, describe, it, shouldBe)
 import Test.Hspec.QuickCheck (prop)
-import Test.QuickCheck (Arbitrary (..), Property, forAllShrink, (===))
+import Test.QuickCheck (Arbitrary (..), Property, forAll, forAllShrink, (===), (==>))
+import Test.QuickCheck.Classes (lawsCheck, showReadLaws)
+import Test.QuickCheck.Property (once)
 
 spec :: Spec
 spec = do
-  prop "asChain is inverse to asList" propAsChainInverseAsList
-  prop "(c₁ ≡ c₂) -> (commonPrefix (c₁ ∷ c₂ ∷ []) ≡ c₁)" propCommonPrefixSelf
+  describe "Read/Show instances" $ do
+    it "can read a simple Chain" $ do
+      let v = read @(Chain ()) "Cons (Block {slotNumber = 1, creatorId = \"00010000\", parentBlock = \"00000000\", includedVotes = (), leadershipProof = \"01000101\", payload = [], signature = \"00000100\"}) Genesis"
+      v `shouldBe` Cons (Block{slotNumber = 1, creatorId = "00010000", parentBlock = "00000000", includedVotes = (), leadershipProof = "01000101", payload = [], signature = "00000100"}) Genesis
+    prop "read is inverse to show: Chain ()" $ lawsCheck $ showReadLaws (Proxy @(Chain ()))
+    prop "read is inverse to show: PartyId" $ lawsCheck $ showReadLaws (Proxy @PartyId)
+    prop "read is inverse to show: Slot" $ lawsCheck $ showReadLaws (Proxy @Slot)
+    prop "read is inverse to show: Hash" $ lawsCheck $ showReadLaws (Proxy @Hash)
+    prop "read is inverse to show: LeadershipProof" $ lawsCheck $ showReadLaws (Proxy @LeadershipProof)
+    prop "read is inverse to show: MembershipProof" $ lawsCheck $ showReadLaws (Proxy @MembershipProof)
+    prop "read is inverse to show: Tx" $ lawsCheck $ showReadLaws (Proxy @Tx)
+  describe "Common Prefix" $ do
+    prop "asChain is inverse to asList" propAsChainInverseAsList
+    prop "selfPrefix: (c₁ ≡ c₂) -> (commonPrefix (c₁ ∷ c₂ ∷ []) ≡ c₁)" propCommonPrefixSelf
+    prop "prefixExtended : (c : Chain) -> (b1, b2 : Block) -> (commonPrefix (Cons b1 c ∷ Cons b2  c ∷ []) ≡ c)" propCommonPrefixExtended
+    prop "Sample chain" $
+      once $
+        commonPrefix sampleChains === Cons (Block{slotNumber = 44, creatorId = "ece20dec9edc", parentBlock = "", includedVotes = (), leadershipProof = "0faf57e3c126", payload = [], signature = "c63cff5266ee"}) Genesis
+
+sampleChains =
+  [ chain1
+  , chain2
+  , chain1
+  , chain1
+  , chain1
+  , chain2
+  , chain1
+  , chain1
+  , chain1
+  , chain1
+  ]
+
+chain1 = Cons (Block{slotNumber = 49, creatorId = "7392b2bd2853", parentBlock = "", includedVotes = (), leadershipProof = "f2a6ab5f8122", payload = [], signature = "06f34b7da9fd"}) (Cons (Block{slotNumber = 44, creatorId = "ece20dec9edc", parentBlock = "", includedVotes = (), leadershipProof = "0faf57e3c126", payload = [], signature = "c63cff5266ee"}) Genesis)
+
+chain2 = Cons (Block{slotNumber = 44, creatorId = "ece20dec9edc", parentBlock = "", includedVotes = (), leadershipProof = "0faf57e3c126", payload = [], signature = "c63cff5266ee"}) Genesis
 
 propAsChainInverseAsList :: Chain () -> Property
 propAsChainInverseAsList c =
@@ -23,3 +62,7 @@ propCommonPrefixSelf :: Property
 propCommonPrefixSelf =
   forAllShrink arbitrary shrink $ \c ->
     commonPrefix @() [c, c] === c
+
+propCommonPrefixExtended :: Chain () -> Block () -> Block () -> Property
+propCommonPrefixExtended c b1 b2 =
+  b1 /= b2 ==> commonPrefix [Cons b1 c, Cons b2 c] === c