Use of agda2hs to generate model in Haskell

Makefile

@@ -1,17 +1,22 @@
 # Inspired by https://git.app.uib.no/hott/agda-unimath/-/blob/6f6a48c92912da3f1245b846c5439c63d1461792/Makefile
 AGDAFILES := $(wildcard src/**/*.agda)
 AGDAIFILES := $(patsubst %.agda,%.agdai,$(AGDAFILES))
+HSFILES := $(patsubst %.agda,%.hs,$(AGDAFILES))
 AGDAFLAGS := -i src
 AGDA ?= agda
+AGDA2HS ?= agda2hs
 
 .PHONY: typecheck
 
-typecheck: $(AGDAIFILES)
+typecheck: $(AGDAIFILES) $(HSFILES)
 
 # From https://stackoverflow.com/questions/34621364/makefile-compile-o-from-c-files
 $(AGDAIFILES): %.agdai: %.agda
 	@$(AGDA) $(AGDAFLAGS) $^
 
+$(HSFILES): %.hs: %.agda
+	@$(AGDA2HS) $^
+
 .PHONY : clean
 clean:
 	@echo "Removing .agdai files"

flake.nix

@@ -8,9 +8,10 @@
       systems = ["x86_64-linux" "aarch64-darwin"];
       perSystem = {pkgs, ...}: let
         agda = pkgs.agda.withPackages (p: [p.standard-library]);
+        agda2hs = pkgs.haskellPackages.agda2hs;
       in {
         devShells.default = pkgs.mkShell {
-          buildInputs = [agda];
+          buildInputs = [agda agda2hs];
         };
       };
     };

src/Peras/Block.agda

@@ -7,7 +7,17 @@ open import Data.List
 open import Data.Tree.AVL.Sets renaming (⟨Set⟩ to set)
 open import Relation.Binary using (StrictTotalOrder)
 
-open import Peras.Crypto
+open import Peras.Crypto hiding (ByteString; emptyBS; _isInfixOf_)
+
+-- TODO: ByteString is not exported from Peras.Crypto in Haskell
+postulate
+  ByteString : Set
+  emptyBS : ByteString
+  _isInfixOf_ : ByteString → ByteString → Bool
+
+{-# FOREIGN AGDA2HS import Data.ByteString as BS #-}
+{-# FOREIGN GHC import qualified Data.ByteString as BS #-}
+{-# COMPILE GHC ByteString = type BS.ByteString #-}
 
 record PartyId : Set where
   constructor MkPartyId
@@ -20,14 +30,20 @@ open PartyId public
 record Tx : Set where
   field tx : ByteString
 
+open Tx public
+
+{-# COMPILE AGDA2HS Tx #-}
+
 Slot = Word64
 
-record Block : Set where
+{-# COMPILE AGDA2HS Slot #-}
+
+record Block (t : Set) : Set where
   field slotNumber : Slot
         -- blockHeight : Word64
         creatorId : PartyId
         parentBlock : Hash
-        includedVotes : set HashO
+        includedVotes : t -- set HashO
         leadershipProof : LeadershipProof
         payload : List Tx
         signature : Signature  
@@ -36,18 +52,19 @@ open Block public
 
 {-# COMPILE AGDA2HS Block #-}
 
+Block⁺ = Block (set HashO)
+
 postulate
-  blEq : Relation.Binary.Rel Block 0ℓ
-  blLt : Relation.Binary.Rel Block 0ℓ
+  blEq : Relation.Binary.Rel Block⁺ 0ℓ
+  blLt : Relation.Binary.Rel Block⁺ 0ℓ
   blIs : Relation.Binary.IsStrictTotalOrder blEq blLt
 
 BlockO : StrictTotalOrder 0ℓ 0ℓ 0ℓ
 BlockO = record {
-  Carrier            = Block ;
+  Carrier            = Block⁺ ;
   _≈_                = blEq ;
   _<_                = blLt ;
   isStrictTotalOrder = blIs }
 
 postulate
-  isValidBlock : Block -> Bool
-
+  isValidBlock : Block⁺ -> Bool

src/Peras/Chain.agda

@@ -28,13 +28,13 @@ record Vote msg : Set where
         signature                : Signature
 
 postulate
-  vblEq : Relation.Binary.Rel (Vote Block) 0ℓ
-  vblLt : Relation.Binary.Rel (Vote Block) 0ℓ
+  vblEq : Relation.Binary.Rel (Vote Block⁺) 0ℓ
+  vblLt : Relation.Binary.Rel (Vote Block⁺) 0ℓ
   vblIs : Relation.Binary.IsStrictTotalOrder vblEq vblLt
 
 VoteBlockO : StrictTotalOrder 0ℓ 0ℓ 0ℓ
 VoteBlockO = record {
-  Carrier            = (Vote Block) ;
+  Carrier            = (Vote Block⁺) ;
   _≈_                = vblEq ;
   _<_                = vblLt ;
   isStrictTotalOrder = vblIs }
@@ -52,16 +52,24 @@ isValid v@(vote _ (MkPartyId vkey) committeeMembershipProof _ signature) =
   isCommitteeMember vkey committeeMembershipProof
     ∧ verify vkey signature (toSignable v)
 
+{-
 record Chain : Set where
   constructor MkChain
   field blocks : set BlockO
         tip : Block -- The tip of this chain, must be a member of `blocks`
         votes : set VoteBlockO -- The set of "pending" votes, eg. which have not been included in a `Block`.
+-}
+
+data Chain t : Set where
+  Genesis : Chain t
+  Cons : Block t → Chain t → Chain t
 
 open Chain public
 
 {-# COMPILE AGDA2HS Chain #-}
 
+Chain⁺ = Chain (set BlockO)
+
 -- | Chain validity
 --
 -- A chain is valid iff:
@@ -80,10 +88,10 @@ open Chain public
 
 
 postulate
-  verifyLeadershipProof : Block → Bool
+  verifyLeadershipProof : Block⁺ → Bool
 
-  properlyLinked : Chain → Bool
-  decreasingSlots : Chain → Bool
+  properlyLinked : Chain⁺ → Bool
+  decreasingSlots : Chain⁺ → Bool
 
 {-
 correctBlocks : Chain → Bool
@@ -93,7 +101,7 @@ correctBlocks (MkChain blocks _ _) =
 -}
 
 postulate
-  isValidChain : Chain -> Bool
+  isValidChain : Chain⁺ -> Bool
 
 
 {-
@@ -111,9 +119,9 @@ module _ {T : Set} where
 
     field
       tree0 : T
-      extendTree : T → Block → T
-      allBlocks : T → List Block
-      bestChain : Slot → T → Chain
+      extendTree : T → Block⁺ → T
+      allBlocks : T → List Block⁺
+      bestChain : Slot → T → Chain⁺
 
   open TreeType
 

src/Peras/Crypto.agda

@@ -2,28 +2,38 @@
 --
 -- We don't use real cryptography here, just a bunch of newtypes and
 -- simple functions that represent various cryptographic operations
--- one can do when running the protocol
+-- one can do when running the protocol 
 module Peras.Crypto where
 
 open import Level
 open import Relation.Binary using (StrictTotalOrder)
 open import Data.Unit
 open import Data.Bool
 
+-- open import Haskell.Prelude
+
 postulate
   ByteString : Set
   emptyBS : ByteString
   _isInfixOf_ : ByteString → ByteString → Bool
 
+{-# FOREIGN AGDA2HS import Data.ByteString as BS #-}
+{-# FOREIGN GHC import qualified Data.ByteString as BS #-}
+{-# COMPILE GHC ByteString = type BS.ByteString #-}
+
 record Hash : Set where
   field hash : ByteString
 
+open Hash public
+
+{-# COMPILE AGDA2HS Hash newtype #-}
+
 postulate
-  hsEq : Relation.Binary.Rel Hash zero
-  hsLt : Relation.Binary.Rel Hash zero
+  hsEq : Relation.Binary.Rel Hash 0ℓ
+  hsLt : Relation.Binary.Rel Hash 0ℓ
   hsIs : Relation.Binary.IsStrictTotalOrder hsEq hsLt
 
-HashO : StrictTotalOrder zero zero zero
+HashO : StrictTotalOrder 0ℓ 0ℓ 0ℓ
 HashO = record {
   Carrier            = Hash ;
   _≈_                = hsEq ;
@@ -32,12 +42,20 @@ HashO = record {
 
 -- should use normal VRF algorithm like leadership membership
 record MembershipProof : Set where
-  constructor membershipProof
-  field proof : ByteString
+  field proofM : ByteString
+
+open MembershipProof public
+
+{-# COMPILE AGDA2HS MembershipProof newtype #-}
 
 record LeadershipProof : Set where
   field proof : ByteString
 
+open LeadershipProof public
+
+{-# COMPILE AGDA2HS LeadershipProof newtype #-}
+
+
 {-
 -- use KES-based signatures which weighs about 600 bytes (could be
 -- down to 400)
@@ -46,14 +64,21 @@ record LeadershipProof : Set where
 record Signature : Set where
   field signature : ByteString
 
+open Signature public
+
+{-# COMPILE AGDA2HS Signature newtype #-}
+
 record VerificationKey : Set where
-  constructor verificationKey
-  field verKey : ByteString
+  field verificationKey : ByteString
+
+open VerificationKey public
+
+{-# COMPILE AGDA2HS VerificationKey newtype #-}
 
 -- | a fake membership "proof" is simply a concatenation of all the
 -- members' verification keys.
 isCommitteeMember : VerificationKey -> MembershipProof -> Bool
-isCommitteeMember (verificationKey verKey) (membershipProof proof) =
+isCommitteeMember (record {verificationKey = verKey}) (record { proofM = proof }) =
   verKey isInfixOf proof
 
 postulate verify : VerificationKey -> Signature -> ByteString -> Bool

src/Peras/Message.agda

@@ -11,30 +11,34 @@ data Message msg : Set where
   NewChain : msg → Message msg
 
 record NodeId : Set where
-  constructor mkNodeId
+  constructor MkNodeId
   field
     nodeId : String
 
+open NodeId public
+
+{-# COMPILE AGDA2HS NodeId #-}
+
 -- | Messages sent to the node.
-data Input : Set where
+data Input t : Set where
 
   -- | New slot occurs (represents the passage of time)
-  NextSlot : Slot → Input
+  NextSlot : Slot → Input t
 
   -- | Some `NodeId` has sent a requested `Block` to this node.
-  SomeBlock : NodeId → Block → Input
+  SomeBlock : NodeId → Block t → Input t
 
   -- | Some `NodeId` is notifying us their best chain has changed.
-  UpdatedChain : NodeId → Chain → Input
+  UpdatedChain : NodeId → Chain t → Input t
 
-{-# COMPILE AGDA2HS Input deriving ( Show, Eq ) #-}
+{-# COMPILE AGDA2HS Input #-}
 
-data Output : Set where
+data Output t : Set where
 
   -- | Node needs some block from given `NodeId`.
-  FetchBlock : NodeId → Block → Output
+  FetchBlock : NodeId → Block t → Output t
 
   -- | Node changed its best chain
-  NewChain : Chain → Output
+  NewChain : Chain t → Output t
 
-{-# COMPILE AGDA2HS Output deriving ( Show, Eq ) #-}
+{-# COMPILE AGDA2HS Output #-}

src/Peras/Nakamoto.agda

@@ -24,7 +24,7 @@ record ConsensusConfig : Set where
 -- already referenced by blocks in C, and is not an equivocation of a
 -- vote referenced by blocks in C.
 
-postulate chainWeight : ConsensusConfig -> Block -> set VoteBlockO -> Word64
+postulate chainWeight : ConsensusConfig -> Block⁺ -> set VoteBlockO -> Word64
 {-
 chainWeight ConsensusConfig{roundLength} Block{blockHeight, slotNumber} pendingVotes =
   let chainWeight = blockHeight
@@ -47,13 +47,13 @@ WordO = record {
 
 record ConsensusState : Set where
   constructor consensusState
-  field currentChain  : Block
+  field currentChain  : Block⁺
         seenChains    : set BlockO
         votesReceived : Map WordO (Map BlockO (set VoteBlockO))
 
 data Decision : Set where
-  Tally : Vote Block → Decision
-  Seen  : Block → Decision
+  Tally : Vote Block⁺ → Decision
+  Seen  : Block⁺ → Decision
 
 {-
 nakamotoLayer :: ConsensusConfig -> ConsensusState -> Message Block -> Decision