diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 90eb0cc7..07521dfe 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -77,9 +77,6 @@ jobs: trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }} substituters = ${{ env.SUBSTITUTERS }} experimental-features = nix-command flakes - - name: πŸ”¬ Test with `peras-hs-test` - run: | - nix run .#peras-hs-test - name: πŸ”¬ Test with `peras-simulation-test` run: | nix run .#peras-simulation-test diff --git a/Makefile b/Makefile index 8082f369..472e1527 100644 --- a/Makefile +++ b/Makefile @@ -2,7 +2,7 @@ AGDAFILES := $(shell find src -name *.agda -exec grep -l AGDA2HS {} \;) LAGDAFILES := $(shell find src -name *.lagda.md -exec grep -l AGDA2HS {} \;) SIMAGDAFILES := $(shell find sim_src -name *.agda -exec grep -l AGDA2HS {} \;) -HSDIR=peras-hs +HSDIR=peras-simulation HSFILES := $(patsubst %.agda,$(HSDIR)/%.hs,$(AGDAFILES)) LHSFILES := $(patsubst %.lagda.md,$(HSDIR)/%.hs,$(LAGDAFILES)) SIMHSFILES := $(patsubst sim_src/%.agda,peras-simulation/src/%.hs,$(SIMAGDAFILES)) @@ -18,29 +18,22 @@ $(info $(LHSFILES)) .PHONY: typecheck all: typecheck - cabal update cabal build all typecheck: $(HSFILES) $(LHSFILES) $(SIMHSFILES) - @rm -f $(BADSIMHSFILES) -# From https://stackoverflow.com/questions/34621364/makefile-compile-o-from-c-files $(HSDIR)/%.hs: %.agda + @$(AGDA) --local-interfaces --library-file=$(AGDA_LIBS) $^ @$(AGDA2HS) --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src --config $(AGDA2HS_CONFIG) $^ - @$(AGDA) --compile --ghc-dont-call-ghc --no-main --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src $^ $(HSDIR)/%.hs: %.lagda.md + @$(AGDA) --local-interfaces --library-file=$(AGDA_LIBS) $^ @$(AGDA2HS) --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src --config $(AGDA2HS_CONFIG) $^ - @$(AGDA) --compile --ghc-dont-call-ghc --no-main --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src $^ -peras-simulation/src/%.hs : sim_src/%.agda - @$(AGDA2HS) --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=peras-simulation/src $^ +.PHONY : clean -.PHONY : clean veryclean clean: @echo "Removing .agdai files" @find src -name \*.agdai -delete; - -veryclean: clean - @echo "Removing generated.hs files" - @rm $(HSFILES) $(LHSFILES) + @echo "Removing generated .hs files" + @rm -f $(HSFILES) $(LHSFILES) diff --git a/cabal.project b/cabal.project index 3c67cf77..9b99c86a 100644 --- a/cabal.project +++ b/cabal.project @@ -15,7 +15,6 @@ index-state: , cardano-haskell-packages 2024-05-29T10:15:00Z packages: - peras-hs peras-simulation peras-markov peras-server diff --git a/nix/agda-project.nix b/nix/agda-project.nix index 2b9368cc..67c53ff9 100644 --- a/nix/agda-project.nix +++ b/nix/agda-project.nix @@ -3,7 +3,7 @@ pkgs.haskell-nix.hackage-project { name = "Agda"; - version = "2.6.4.1"; + version = "2.6.4.3"; compiler-nix-name = "ghc96"; diff --git a/peras-hs/LICENSE b/peras-hs/LICENSE deleted file mode 100644 index 1a9893b4..00000000 --- a/peras-hs/LICENSE +++ /dev/null @@ -1,176 +0,0 @@ - Apache License - Version 2.0, January 2004 - http://www.apache.org/licenses/ - - TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION - - 1. Definitions. - - "License" shall mean the terms and conditions for use, reproduction, - and distribution as defined by Sections 1 through 9 of this document. - - "Licensor" shall mean the copyright owner or entity authorized by - the copyright owner that is granting the License. - - "Legal Entity" shall mean the union of the acting entity and all - other entities that control, are controlled by, or are under common - control with that entity. For the purposes of this definition, - "control" means (i) the power, direct or indirect, to cause the - direction or management of such entity, whether by contract or - otherwise, or (ii) ownership of fifty percent (50%) or more of the - outstanding shares, or (iii) beneficial ownership of such entity. - - "You" (or "Your") shall mean an individual or Legal Entity - exercising permissions granted by this License. - - "Source" form shall mean the preferred form for making modifications, - including but not limited to software source code, documentation - source, and configuration files. - - "Object" form shall mean any form resulting from mechanical - transformation or translation of a Source form, including but - not limited to compiled object code, generated documentation, - and conversions to other media types. - - "Work" shall mean the work of authorship, whether in Source or - Object form, made available under the License, as indicated by a - copyright notice that is included in or attached to the work - (an example is provided in the Appendix below). - - "Derivative Works" shall mean any work, whether in Source or Object - form, that is based on (or derived from) the Work and for which the - editorial revisions, annotations, elaborations, or other modifications - represent, as a whole, an original work of authorship. For the purposes - of this License, Derivative Works shall not include works that remain - separable from, or merely link (or bind by name) to the interfaces of, - the Work and Derivative Works thereof. - - "Contribution" shall mean any work of authorship, including - the original version of the Work and any modifications or additions - to that Work or Derivative Works thereof, that is intentionally - submitted to Licensor for inclusion in the Work by the copyright owner - or by an individual or Legal Entity authorized to submit on behalf of - the copyright owner. For the purposes of this definition, "submitted" - means any form of electronic, verbal, or written communication sent - to the Licensor or its representatives, including but not limited to - communication on electronic mailing lists, source code control systems, - and issue tracking systems that are managed by, or on behalf of, the - Licensor for the purpose of discussing and improving the Work, but - excluding communication that is conspicuously marked or otherwise - designated in writing by the copyright owner as "Not a Contribution." - - "Contributor" shall mean Licensor and any individual or Legal Entity - on behalf of whom a Contribution has been received by Licensor and - subsequently incorporated within the Work. - - 2. Grant of Copyright License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - copyright license to reproduce, prepare Derivative Works of, - publicly display, publicly perform, sublicense, and distribute the - Work and such Derivative Works in Source or Object form. - - 3. Grant of Patent License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - (except as stated in this section) patent license to make, have made, - use, offer to sell, sell, import, and otherwise transfer the Work, - where such license applies only to those patent claims licensable - by such Contributor that are necessarily infringed by their - Contribution(s) alone or by combination of their Contribution(s) - with the Work to which such Contribution(s) was submitted. If You - institute patent litigation against any entity (including a - cross-claim or counterclaim in a lawsuit) alleging that the Work - or a Contribution incorporated within the Work constitutes direct - or contributory patent infringement, then any patent licenses - granted to You under this License for that Work shall terminate - as of the date such litigation is filed. - - 4. Redistribution. You may reproduce and distribute copies of the - Work or Derivative Works thereof in any medium, with or without - modifications, and in Source or Object form, provided that You - meet the following conditions: - - (a) You must give any other recipients of the Work or - Derivative Works a copy of this License; and - - (b) You must cause any modified files to carry prominent notices - stating that You changed the files; and - - (c) You must retain, in the Source form of any Derivative Works - that You distribute, all copyright, patent, trademark, and - attribution notices from the Source form of the Work, - excluding those notices that do not pertain to any part of - the Derivative Works; and - - (d) If the Work includes a "NOTICE" text file as part of its - distribution, then any Derivative Works that You distribute must - include a readable copy of the attribution notices contained - within such NOTICE file, excluding those notices that do not - pertain to any part of the Derivative Works, in at least one - of the following places: within a NOTICE text file distributed - as part of the Derivative Works; within the Source form or - documentation, if provided along with the Derivative Works; or, - within a display generated by the Derivative Works, if and - wherever such third-party notices normally appear. The contents - of the NOTICE file are for informational purposes only and - do not modify the License. You may add Your own attribution - notices within Derivative Works that You distribute, alongside - or as an addendum to the NOTICE text from the Work, provided - that such additional attribution notices cannot be construed - as modifying the License. - - You may add Your own copyright statement to Your modifications and - may provide additional or different license terms and conditions - for use, reproduction, or distribution of Your modifications, or - for any such Derivative Works as a whole, provided Your use, - reproduction, and distribution of the Work otherwise complies with - the conditions stated in this License. - - 5. Submission of Contributions. Unless You explicitly state otherwise, - any Contribution intentionally submitted for inclusion in the Work - by You to the Licensor shall be under the terms and conditions of - this License, without any additional terms or conditions. - Notwithstanding the above, nothing herein shall supersede or modify - the terms of any separate license agreement you may have executed - with Licensor regarding such Contributions. - - 6. Trademarks. This License does not grant permission to use the trade - names, trademarks, service marks, or product names of the Licensor, - except as required for reasonable and customary use in describing the - origin of the Work and reproducing the content of the NOTICE file. - - 7. Disclaimer of Warranty. Unless required by applicable law or - agreed to in writing, Licensor provides the Work (and each - Contributor provides its Contributions) on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or - implied, including, without limitation, any warranties or conditions - of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A - PARTICULAR PURPOSE. You are solely responsible for determining the - appropriateness of using or redistributing the Work and assume any - risks associated with Your exercise of permissions under this License. - - 8. Limitation of Liability. In no event and under no legal theory, - whether in tort (including negligence), contract, or otherwise, - unless required by applicable law (such as deliberate and grossly - negligent acts) or agreed to in writing, shall any Contributor be - liable to You for damages, including any direct, indirect, special, - incidental, or consequential damages of any character arising as a - result of this License or out of the use or inability to use the - Work (including but not limited to damages for loss of goodwill, - work stoppage, computer failure or malfunction, or any and all - other commercial damages or losses), even if such Contributor - has been advised of the possibility of such damages. - - 9. Accepting Warranty or Additional Liability. While redistributing - the Work or Derivative Works thereof, You may choose to offer, - and charge a fee for, acceptance of support, warranty, indemnity, - or other liability obligations and/or rights consistent with this - License. However, in accepting such obligations, You may act only - on Your own behalf and on Your sole responsibility, not on behalf - of any other Contributor, and only if You agree to indemnify, - defend, and hold each Contributor harmless for any liability - incurred by, or claims asserted against, such Contributor by reason - of your accepting any such warranty or additional liability. - - END OF TERMS AND CONDITIONS diff --git a/peras-hs/ReadMe.md b/peras-hs/ReadMe.md deleted file mode 100644 index d4413a99..00000000 --- a/peras-hs/ReadMe.md +++ /dev/null @@ -1 +0,0 @@ -Haskell source files generated by `agda2hs`, plus orphans. diff --git a/peras-hs/peras-hs.cabal b/peras-hs/peras-hs.cabal deleted file mode 100644 index 8207d7e3..00000000 --- a/peras-hs/peras-hs.cabal +++ /dev/null @@ -1,69 +0,0 @@ -cabal-version: 3.0 -name: peras-hs -version: 0.1.0.0 -synopsis: Peras types from Agda -license: Apache-2.0 -license-file: LICENSE -author: Brian W Bush -maintainer: Brian W Bush -category: Network -build-type: Simple -extra-source-files: ReadMe.md - -data-dir: golden -data-files: *.json - -library - exposed-modules: - Peras.Arbitraries - Peras.Block - Peras.Chain - Peras.Crypto - Peras.Event - Peras.Message - Peras.Numbering - Peras.Orphans - other-modules: - hs-source-dirs: src - build-depends: - aeson - , QuickCheck - , base >=4.9 && <5 - , base16-bytestring - , bytestring - , generic-random - , hashable - , io-classes - , quickcheck-instances - , text - , time - default-extensions: StrictData - default-language: Haskell2010 - ghc-options: -Wall -Wunused-packages - -fno-warn-missing-pattern-synonym-signatures - -fno-warn-missing-signatures - -fno-warn-name-shadowing - -fno-warn-type-defaults - -fno-warn-unused-imports - -fno-warn-unused-matches - -test-suite peras-hs-test - default-language: Haskell2010 - type: exitcode-stdio-1.0 - hs-source-dirs: test - main-is: Main.hs - other-modules: Peras.ChainSpec - Peras.OrphansSpec - Paths_peras_hs - build-depends: - base >= 4.9 && <5 - , QuickCheck - , hspec - , hspec-golden-aeson - , peras-hs - , quickcheck-classes - - build-tool-depends: - hspec-discover:hspec-discover - - ghc-options: -Wall -Wunused-packages -rtsopts -threaded diff --git a/peras-hs/test/Main.hs b/peras-hs/test/Main.hs deleted file mode 100644 index a824f8c3..00000000 --- a/peras-hs/test/Main.hs +++ /dev/null @@ -1 +0,0 @@ -{-# OPTIONS_GHC -F -pgmF hspec-discover #-} diff --git a/peras-hs/golden/Event.json b/peras-simulation/golden/Event.json similarity index 100% rename from peras-hs/golden/Event.json rename to peras-simulation/golden/Event.json diff --git a/peras-hs/golden/[Block].json b/peras-simulation/golden/[Block].json similarity index 100% rename from peras-hs/golden/[Block].json rename to peras-simulation/golden/[Block].json diff --git a/peras-simulation/peras-simulation.cabal b/peras-simulation/peras-simulation.cabal index d3ebe29f..f83d0b53 100644 --- a/peras-simulation/peras-simulation.cabal +++ b/peras-simulation/peras-simulation.cabal @@ -7,6 +7,11 @@ author: Arnaud Bailly maintainer: arnaud.bailly@iohk.io category: Testing build-type: Simple +extra-source-files: ReadMe.md +extra-doc-files: CHANGELOG.md +data-dir: golden +data-files: *.json + custom-setup setup-depends: base , directory @@ -14,10 +19,15 @@ custom-setup , process , Cabal -extra-doc-files: CHANGELOG.md common warnings - ghc-options: -Wall -Wunused-packages + ghc-options: -Wall -Wunused-packages -Werror + -fno-warn-missing-pattern-synonym-signatures + -fno-warn-missing-signatures + -fno-warn-name-shadowing + -fno-warn-type-defaults + -fno-warn-unused-imports + -fno-warn-unused-matches library import: warnings @@ -38,6 +48,15 @@ library Peras.Abstract.Protocol.Types Peras.Abstract.Protocol.Visualizer Peras.Abstract.Protocol.Voting + Peras.Arbitraries + Peras.Block + Peras.Chain + Peras.Crypto + Peras.Event + Peras.Message + Peras.Numbering + Peras.Orphans + Peras.Util -- details of voting Peras.Voting.Vote Peras.Voting.Arbitraries @@ -45,6 +64,7 @@ library build-depends: QuickCheck, aeson, base ^>=4.18.1.0, + base16-bytestring, bytestring, cardano-binary, cardano-crypto-class ^>= 2.1, @@ -54,18 +74,19 @@ library contra-tracer, data-default, deepseq, + generic-random, hashable, io-classes, io-sim, language-dot, mtl, --- non-integral, - peras-hs, + pretty, quickcheck-dynamic, - text, + quickcheck-instances, + statistics, stm, - pretty, - statistics + text, + time, hs-source-dirs: src default-language: Haskell2010 @@ -103,6 +124,9 @@ test-suite peras-simulation-test Peras.Abstract.Protocol.Node.ModelSpec Peras.Abstract.Protocol.NodeSpec Peras.Abstract.Protocol.VotingSpec + Peras.ChainSpec + Peras.OrphansSpec + Paths_peras_simulation -- voting Peras.Voting.VoteSpec type: exitcode-stdio-1.0 @@ -116,10 +140,11 @@ test-suite peras-simulation-test , contra-tracer , data-default , hspec + , hspec-golden-aeson , io-classes , mtl - , peras-hs , peras-simulation + , quickcheck-classes , quickcheck-dynamic build-tool-depends: hspec-discover:hspec-discover diff --git a/peras-simulation/src/Peras/Abstract/Protocol/Conformance/Model.hs b/peras-simulation/src/Peras/Abstract/Protocol/Conformance/Model.hs index e251cdf9..05a8a083 100644 --- a/peras-simulation/src/Peras/Abstract/Protocol/Conformance/Model.hs +++ b/peras-simulation/src/Peras/Abstract/Protocol/Conformance/Model.hs @@ -5,17 +5,17 @@ module Peras.Abstract.Protocol.Conformance.Model where import Control.Monad (guard) +import Numeric.Natural (Natural) import Peras.Abstract.Protocol.Params (PerasParams (MkPerasParams, perasA, perasB, perasK, perasL, perasR, perasT, perasU, perasΟ„), defaultPerasParams) -import Peras.Block (Block (MkBlock), Certificate (MkCertificate, round), PartyId) -import Peras.Chain (Chain, Vote (creatorId)) -import Peras.Crypto (Hash (MkHash), replicateBS) +import Peras.Block (Block (MkBlock), Certificate (MkCertificate, blockRef, round), PartyId) +import Peras.Chain (Chain, Vote) +import Peras.Crypto (Hash (MkHash), Hashable (hash), emptyBS) import Peras.Numbering (RoundNumber (MkRoundNumber, getRoundNumber), SlotNumber (MkSlotNumber, getSlotNumber)) +import Peras.Util (comparing, maximumBy) import Control.Monad.Identity import Data.Function (on) -import Data.List (maximumBy) import Data.Maybe (catMaybes, listToMaybe, maybeToList) -import Data.Ord (comparing) import Data.Set (Set) import qualified Data.Set as Set import Peras.Abstract.Protocol.Crypto (createMembershipProof, createSignedCertificate, createSignedVote, mkCommitteeMember, mkParty) @@ -41,7 +41,7 @@ data EnvAction deriving (Eq, Show) genesisHash :: Hash Block -genesisHash = MkHash (replicateBS 8 0) +genesisHash = MkHash emptyBS genesisChain :: Chain genesisChain = [] @@ -61,7 +61,7 @@ initialModelState = 1 1 (perasB defaultPerasParams) - 1 + 0 0 ) [genesisChain] @@ -97,21 +97,24 @@ seenBeforeStartOfRound :: seenBeforeStartOfRound params r (c, s) = getSlotNumber s <= getRoundNumber r * perasU params -preferredChain :: PerasParams -> [Certificate] -> [Chain] -> Chain -preferredChain MkPerasParams{..} certs chains = - maximumBy (compare `on` chainWeight perasB (Set.fromList certs)) (Set.fromList $ genesisChain : chains) +chainWeight :: Natural -> [Certificate] -> Chain -> Natural +chainWeight boost certs = chainWeight' 0 + where + isCertified :: Block -> Bool + isCertified block = + filter (\cert -> hash block == blockRef cert) certs == [] + chainWeight' :: Natural -> [Block] -> Natural + chainWeight' accum [] = accum + chainWeight' accum (block : blocks) = + if isCertified block + then chainWeight' (accum + 1 + boost) blocks + else chainWeight' (accum + 1) blocks -chainWeight :: Integer -> Set Certificate -> Chain -> Integer -chainWeight boost certs blocks = - let - -- Block hashes certified by any certificate. - certifiedBlocks = Set.map blockRef certs :: Set (Hash Block) - -- Block hashes on the chain. - chainBlocks = Set.fromList $ hash <$> blocks :: Set (Hash Block) - in - -- Length of the chain plus the boost times the count of certified blocks. - fromIntegral (length blocks) - + boost * fromIntegral (Set.size $ certifiedBlocks `Set.intersection` chainBlocks) +preferredChain :: PerasParams -> [Certificate] -> [Chain] -> Chain +preferredChain params certs = + maximumBy + genesisChain + (comparing (chainWeight (fromIntegral (perasB params)) certs)) makeVote :: PerasParams -> SlotNumber -> Block -> Maybe Vote makeVote protocol@MkPerasParams{perasT} slot block = do @@ -149,10 +152,15 @@ makeVote'' s = pref :: Chain pref = preferredChain params (allSeenCerts s) (allChains s) cert' :: Certificate - cert' = maximumBy (comparing (\r -> round r)) (allSeenCerts s) + cert' = + maximumBy + genesisCert + (comparing (\r -> round r)) + (allSeenCerts s) certS :: Certificate certS = maximumBy + genesisCert (comparing (\r -> round r)) (genesisCert : catMaybes (map certificate pref)) @@ -180,10 +188,15 @@ makeVote' s = pref :: Chain pref = preferredChain params (allSeenCerts s) (allChains s) cert' :: Certificate - cert' = maximumBy (comparing (\r -> round r)) (allSeenCerts s) + cert' = + maximumBy + genesisCert + (comparing (\r -> round r)) + (allSeenCerts s) certS :: Certificate certS = maximumBy + genesisCert (comparing (\r -> round r)) (genesisCert : catMaybes (map certificate pref)) @@ -255,7 +268,6 @@ transition s (NewVote v) = guard (checkVoteSignature v) checkVotingRules <- makeVote'' s guard checkVotingRules - guard (creatorId v == sutId) Just ( [] , NodeModel diff --git a/peras-hs/src/Peras/Arbitraries.hs b/peras-simulation/src/Peras/Arbitraries.hs similarity index 100% rename from peras-hs/src/Peras/Arbitraries.hs rename to peras-simulation/src/Peras/Arbitraries.hs diff --git a/peras-hs/src/Peras/Block.hs b/peras-simulation/src/Peras/Block.hs similarity index 100% rename from peras-hs/src/Peras/Block.hs rename to peras-simulation/src/Peras/Block.hs diff --git a/peras-hs/src/Peras/Chain.hs b/peras-simulation/src/Peras/Chain.hs similarity index 100% rename from peras-hs/src/Peras/Chain.hs rename to peras-simulation/src/Peras/Chain.hs diff --git a/peras-hs/src/Peras/Crypto.hs b/peras-simulation/src/Peras/Crypto.hs similarity index 96% rename from peras-hs/src/Peras/Crypto.hs rename to peras-simulation/src/Peras/Crypto.hs index 573ff63d..5d78e893 100644 --- a/peras-hs/src/Peras/Crypto.hs +++ b/peras-simulation/src/Peras/Crypto.hs @@ -12,6 +12,8 @@ eqBS :: ByteString -> ByteString -> Bool eqBS = (==) replicateBS :: Int -> Word8 -> ByteString replicateBS = BS.replicate +emptyBS :: ByteString +emptyBS = mempty newtype Hash a = MkHash {hashBytes :: ByteString} deriving (Generic) diff --git a/peras-hs/src/Peras/Event.hs b/peras-simulation/src/Peras/Event.hs similarity index 100% rename from peras-hs/src/Peras/Event.hs rename to peras-simulation/src/Peras/Event.hs diff --git a/peras-hs/src/Peras/Message.hs b/peras-simulation/src/Peras/Message.hs similarity index 100% rename from peras-hs/src/Peras/Message.hs rename to peras-simulation/src/Peras/Message.hs diff --git a/peras-hs/src/Peras/Numbering.hs b/peras-simulation/src/Peras/Numbering.hs similarity index 100% rename from peras-hs/src/Peras/Numbering.hs rename to peras-simulation/src/Peras/Numbering.hs diff --git a/peras-hs/src/Peras/Orphans.hs b/peras-simulation/src/Peras/Orphans.hs similarity index 100% rename from peras-hs/src/Peras/Orphans.hs rename to peras-simulation/src/Peras/Orphans.hs diff --git a/peras-simulation/src/Peras/Util.hs b/peras-simulation/src/Peras/Util.hs new file mode 100644 index 00000000..97727fac --- /dev/null +++ b/peras-simulation/src/Peras/Util.hs @@ -0,0 +1,11 @@ +module Peras.Util where + +maximumBy :: a -> (a -> a -> Ordering) -> [a] -> a +maximumBy candidate _ [] = candidate +maximumBy candidate f (x : xs) = + case f candidate x of + GT -> maximumBy x f xs + _ -> maximumBy candidate f xs + +comparing :: Ord b => (a -> b) -> a -> a -> Ordering +comparing f x y = compare (f x) (f y) diff --git a/peras-hs/test/Peras/ChainSpec.hs b/peras-simulation/test/Peras/ChainSpec.hs similarity index 97% rename from peras-hs/test/Peras/ChainSpec.hs rename to peras-simulation/test/Peras/ChainSpec.hs index 9d02d686..577f1ec3 100644 --- a/peras-hs/test/Peras/ChainSpec.hs +++ b/peras-simulation/test/Peras/ChainSpec.hs @@ -6,7 +6,7 @@ module Peras.ChainSpec where import Data.Data (Proxy (..)) import Peras.Arbitraries () import Peras.Block (Block (..), PartyId, Tx) -import Peras.Chain (Chain (..), commonPrefix, prefix) +import Peras.Chain (Chain, commonPrefix, prefix) import Peras.Crypto (Hash (..), LeadershipProof, MembershipProof) import Peras.Numbering (SlotNumber) import Peras.Orphans () diff --git a/peras-hs/test/Peras/OrphansSpec.hs b/peras-simulation/test/Peras/OrphansSpec.hs similarity index 93% rename from peras-hs/test/Peras/OrphansSpec.hs rename to peras-simulation/test/Peras/OrphansSpec.hs index 3d94cf2d..6f9cef9b 100644 --- a/peras-hs/test/Peras/OrphansSpec.hs +++ b/peras-simulation/test/Peras/OrphansSpec.hs @@ -2,7 +2,7 @@ module Peras.OrphansSpec where -import Paths_peras_hs (getDataDir) +import Paths_peras_simulation (getDataDir) import Peras.Arbitraries () import Peras.Block (Block) import Peras.Chain (Chain) diff --git a/sim_src/Peras/Abstract/Protocol/Conformance/Model.agda b/src/Peras/Abstract/Protocol/Conformance/Model.agda similarity index 90% rename from sim_src/Peras/Abstract/Protocol/Conformance/Model.agda rename to src/Peras/Abstract/Protocol/Conformance/Model.agda index f5b2f3cd..d24620ad 100644 --- a/sim_src/Peras/Abstract/Protocol/Conformance/Model.agda +++ b/src/Peras/Abstract/Protocol/Conformance/Model.agda @@ -26,8 +26,6 @@ open import Protocol.Peras using () import Peras.Block (certificate, blockRef) import Peras.Crypto (hash) import Data.Maybe (catMaybes, listToMaybe, maybeToList) - import Data.List (maximumBy) - import Data.Ord (comparing) import Data.Function (on) import qualified Data.Set as Set import Data.Set (Set) @@ -147,26 +145,33 @@ seenBeforeStartOfRound params r (c , s) = getSlotNumber s <= getRoundNumber r * perasU params {-# COMPILE AGDA2HS seenBeforeStartOfRound #-} -postulate - preferredChain : PerasParams β†’ List Certificate β†’ List Chain β†’ Chain +instance + hashBlock : Hashable Block + hashBlock = record + { hash = Ξ» b β†’ + (let record { bytesS = s } = signature b + in record { hashBytes = s }) + } -{-# FOREIGN AGDA2HS -preferredChain :: PerasParams -> [Certificate] -> [Chain] -> Chain -preferredChain MkPerasParams{..} certs chains = - maximumBy (compare `on` chainWeight perasB (Set.fromList certs)) (Set.fromList $ genesisChain : chains) - -chainWeight :: Integer -> Set Certificate -> Chain -> Integer -chainWeight boost certs blocks = - let - -- Block hashes certified by any certificate. - certifiedBlocks = Set.map blockRef certs :: Set (Hash Block) - -- Block hashes on the chain. - chainBlocks = Set.fromList $ hash <$> blocks :: Set (Hash Block) - in - -- Length of the chain plus the boost times the count of certified blocks. - fromIntegral (length blocks) - + boost * fromIntegral (Set.size $ certifiedBlocks `Set.intersection` chainBlocks) -#-} +chainWeight : Nat β†’ List Certificate -> Chain β†’ Nat +chainWeight boost certs = chainWeight' 0 + where + isCertified : Block β†’ Bool + isCertified block = filter (Ξ» cert β†’ Hashable.hash hashBlock block == blockRef cert) certs == [] + chainWeight' : Nat β†’ List Block β†’ Nat + chainWeight' accum [] = accum + chainWeight' accum (block ∷ blocks) = + if isCertified block + then chainWeight' (accum + 1 + boost) blocks + else chainWeight' (accum + 1) blocks + +{-# COMPILE AGDA2HS chainWeight #-} + +preferredChain : PerasParams β†’ List Certificate β†’ List Chain β†’ Chain +preferredChain params certs = + maximumBy genesisChain (comparing (chainWeight (fromNat (perasB params)) certs)) + +{-# COMPILE AGDA2HS preferredChain #-} postulate makeVote : PerasParams β†’ SlotNumber β†’ Block β†’ Maybe Vote diff --git a/sim_src/Peras/Abstract/Protocol/Conformance/Soundness.agda b/src/Peras/Abstract/Protocol/Conformance/Soundness.agda similarity index 100% rename from sim_src/Peras/Abstract/Protocol/Conformance/Soundness.agda rename to src/Peras/Abstract/Protocol/Conformance/Soundness.agda diff --git a/sim_src/Peras/Abstract/Protocol/Params.agda b/src/Peras/Abstract/Protocol/Params.agda similarity index 100% rename from sim_src/Peras/Abstract/Protocol/Params.agda rename to src/Peras/Abstract/Protocol/Params.agda diff --git a/src/Peras/Crypto.agda b/src/Peras/Crypto.agda index 069a060c..cfbffa19 100644 --- a/src/Peras/Crypto.agda +++ b/src/Peras/Crypto.agda @@ -28,6 +28,8 @@ eqBS :: ByteString -> ByteString -> Bool eqBS = (==) replicateBS :: Int -> Word8 -> ByteString replicateBS = BS.replicate +emptyBS :: ByteString +emptyBS = mempty #-} {-# FOREIGN GHC diff --git a/src/Peras/Util.agda b/src/Peras/Util.agda index 7c7fe336..307cf5c6 100644 --- a/src/Peras/Util.agda +++ b/src/Peras/Util.agda @@ -13,3 +13,4 @@ maximumBy {a} candidate f (x ∷ xs) = comparing : ⦃ Ord b ⦄ β†’ (a β†’ b) β†’ a β†’ a β†’ Ordering comparing f x y = compare (f x) (f y) +{-# COMPILE AGDA2HS comparing #-}