diff --git a/.github/workflows/formal-spec.yaml b/.github/workflows/formal-spec.yaml deleted file mode 100644 index c222ea771..000000000 --- a/.github/workflows/formal-spec.yaml +++ /dev/null @@ -1,68 +0,0 @@ -name: "formal-spec" - -env: - ALLOWED_URIS: "https://github.com https://api.github.com" - TRUSTED_PUBLIC_KEYS: - "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= - hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=" - SUBSTITUTERS: "https://cache.nixos.org/ https://cache.iog.io" - -on: - pull_request: - paths: - - "flake.lock" - - "flake.nix" - - "formal-spec/**" - - "nix/**" - push: - branches: - - main - paths: - - "flake.lock" - - "flake.nix" - - "formal-spec/**" - - "nix/**" - -jobs: - ################################################################################ - # Formal Specification in Agda - under /formal-spec/ - ################################################################################ - formal-spec-typecheck: - name: "Typecheck" - runs-on: ubuntu-22.04 - steps: - - name: ๐Ÿ“ฅ Checkout repository - uses: actions/checkout@v4 - - - name: ๐Ÿ’พ Cache Nix store - uses: actions/cache@v3.0.8 - id: nix-cache - with: - path: /tmp/nixcache - key: ${{ runner.os }}-nix-typecheck-${{ hashFiles('flake.lock') }} - restore-keys: ${{ runner.os }}-nix-typecheck- - - - name: ๐Ÿ› ๏ธ Install Nix - uses: cachix/install-nix-action@v21 - with: - nix_path: nixpkgs=channel:nixos-unstable - install_url: https://releases.nixos.org/nix/nix-2.10.3/install - extra_nix_config: | - allowed-uris = ${{ env.ALLOWED_URIS }} - trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }} - substituters = ${{ env.SUBSTITUTERS }} - experimental-features = nix-command flakes - - - name: ๐Ÿ’พโžค Import Nix store cache - if: "steps.nix-cache.outputs.cache-hit == 'true'" - run: "nix-store --import < /tmp/nixcache" - - - name: ๐Ÿ—๏ธ Build specification - run: | - nix build --show-trace --accept-flake-config .#leiosSpec - - - name: โžค๐Ÿ’พ Export Nix store cache - if: "steps.nix-cache.outputs.cache-hit != 'true'" - run: - "nix-store --export $(find /nix/store -maxdepth 1 -name '*-*') > - /tmp/nixcache" diff --git a/README.md b/README.md index 784c76764..6f2124221 100644 --- a/README.md +++ b/README.md @@ -119,21 +119,7 @@ Common arguments for Haskell simulation: ## Specification -Build the Agda specification for Leios using either - -```console -$ nix build --no-link --accept-flake-config .#leiosSpec -``` - -or - -```console -$ nix develop - -$ cd formal-spec - -$ agda Leios/SimpleSpec.agda -``` +The formal specification of the Leios protocol in Agda is refrenced from the repository: https://github.com/input-output-hk/ouroboros-leios-formal-spec ## Archive diff --git a/cabal.project b/cabal.project index c705ef415..1e0289c3e 100644 --- a/cabal.project +++ b/cabal.project @@ -14,8 +14,9 @@ index-state: , hackage.haskell.org 2024-10-04T11:45:34Z , cardano-haskell-packages 2024-10-04T09:54:45Z -packages: +packages: simulation + conformance-testing tests: True @@ -57,3 +58,11 @@ source-repository-package --sha256: 0g5hsjm7bixlwy6m6n98bf8s4khcbg832444w19x35jkjznr2yr1 subdir: pango + +source-repository-package + type: git + location: https://github.com/input-output-hk/ouroboros-leios-formal-spec.git + tag: 026256f141acfef7f3d7b2d048d571223bbee30d + --sha256: WFEmGcnCdEXmo2MCC5g+C3laGjFaBnFksgHbFeAZUQo= + subdir: + generated diff --git a/nix/dummy-project/CHANGELOG.md b/conformance-testing/CHANGELOG.md similarity index 65% rename from nix/dummy-project/CHANGELOG.md rename to conformance-testing/CHANGELOG.md index 70acb7d41..0eff1a947 100644 --- a/nix/dummy-project/CHANGELOG.md +++ b/conformance-testing/CHANGELOG.md @@ -1,4 +1,4 @@ -# Revision history for dummy-project +# Revision history for leios-conformance ## 0.1.0.0 -- YYYY-mm-dd diff --git a/conformance-testing/LICENSE b/conformance-testing/LICENSE new file mode 100644 index 000000000..d64569567 --- /dev/null +++ b/conformance-testing/LICENSE @@ -0,0 +1,202 @@ + + 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 + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/conformance-testing/README.md b/conformance-testing/README.md new file mode 100644 index 000000000..c84239c07 --- /dev/null +++ b/conformance-testing/README.md @@ -0,0 +1,28 @@ +# Conformance Testing Leios Protocol + +Here is a sketch design of the conformance testing pipeline envisioned for Leios protocol. + +![](conformance-testing-pipeline.jpg) + +This is inspired by, and takes into account the experience from, the work done in [Peras](https://github.com/input-output-hk/peras-design) project. The _System-Under-Test_ under consideration is a single (honest) node, with the _Test Driver_ modeling the environment, eg. other nodes participating in the protocol. + +* The formal specification is expected to be _executable_: not only are the valid transitions specified as type-level relations, but those transitions should also be computable typically as a state-transition function mapping each `(state, message)` couple to a target state + * This specification is expected to be _total_ in order to account for the possibility of errors and "adversarial" behaviour + * A pending question is the level of determinism of the specification w.r.t possible implementations. The specification should not over-constrain the implementation and in particular should not prevent concurrent execution of unrelated actions in the SUT, which might lead to various possible interleavings observable for some specified inputs +* This specification is converted to Haskell code using the standard Agda compiler and backend generator + * In particular, this won't be using the [Agda2hs]() "transpiler" which we found does not play well with Agda standard library and ecosystem + * This implies the specification should expose some interface to be called by Haskell test driver +* Generators and test "driver" (or test model) are implemented in Haskell, using QuickCheck and possibly quickcheck-dynamic library for state-machine testing + * The test model should be mostly trivial as it delegates the bulk of the work to the generators (for producing interesting traces) and the specification (to drive the transition system) + * Writing good generators is the tricky part as we want them to cover all kind of interesting potential adversarial behaviour: delaying messages, injecting double-spending txs or equivocated blocks and transactions, split-brain situations, etc. + * **Note**: As the generators need to have deep knowledge of the (expected and observed) state of the SUT and the messages flowing between nodes, it might make sense to define them alongside the formal specification +* The _test driver_ is defined as a straightforward state machine representing the behaviour of the environment of the SUT + * Messages are _sent_ to the SUT, from other nodes, and _received_ from it + * The driver could also have access to _logs_ emitted by the SUT, as a non-intrusive way to observe internal behaviour (eg. things which are only observable locally) without depending explicitly on the details of the SUT's state. This is useful to troubleshoot observed conformance failures and to analyse _coverage_ of the generated test sequences +* The _test adapter_, as the name implies, is there to provide the SUT the _pull-based_ interface it expects + * The SUT is expected to decide when to pull messages from its peers, and (when honest) send messages only when requested to do so + * The adapter's job is to: + 1. convert messages "sent" to the SUT into messages that are available for pulling + 2. pull messages "received" from the SUT when they are expected + * The adapter is meant to isolate the test driver and specification from particular choice of technology for the implementation +* To ensure it can be tested, implementation of the Leios node should be structured in such a way as to be insulated from the details of the networking layers diff --git a/conformance-testing/app/External.hs b/conformance-testing/app/External.hs new file mode 100644 index 000000000..fd49e2a4a --- /dev/null +++ b/conformance-testing/app/External.hs @@ -0,0 +1,37 @@ +module Main where + +import Control.Monad (unless) +import Data.Aeson qualified as A +import Data.ByteString.Lazy.Char8 qualified as LBS8 +import Data.List (isPrefixOf, partition) +import Leios.Conformance.ExternalSpec (spec) +import Leios.Conformance.Test.External (NodeRequest (Stop)) +import System.Environment (getArgs, withArgs) +import System.Exit (die) +import System.IO ( + BufferMode (LineBuffering), + IOMode (AppendMode, ReadMode), + hSetBuffering, + openFile, + ) +import Test.Hspec (hspec) + +main :: IO () +main = do + (customArgs, hspecArgs) <- partition (isPrefixOf "--external-") <$> getArgs + unless (length customArgs == 2) $ + die "Required arguments: --external-input=FILE and --external-output=FILE" + simin <- case filter (isPrefixOf "--external-input=") customArgs of + [arg] -> pure $ drop (length "--external-input=") arg + _ -> die "Missing argument: --external-input=FILE" + simout <- case filter (isPrefixOf "--external-output=") customArgs of + [arg] -> pure $ drop (length "--external-output=") arg + _ -> die "Missing argument: --external-output=FILE" + hWriter <- openFile simin AppendMode + hReader <- openFile simout ReadMode + hSetBuffering hWriter LineBuffering + hSetBuffering hReader LineBuffering + withArgs hspecArgs $ + hspec $ + spec hReader hWriter + LBS8.hPutStrLn hWriter $ A.encode Stop diff --git a/conformance-testing/app/Leios/Conformance/ExternalSpec.hs b/conformance-testing/app/Leios/Conformance/ExternalSpec.hs new file mode 100644 index 000000000..61ea7a098 --- /dev/null +++ b/conformance-testing/app/Leios/Conformance/ExternalSpec.hs @@ -0,0 +1,16 @@ +module Leios.Conformance.ExternalSpec where + +import Leios.Conformance.Test.External (prop_node) +import System.IO (Handle) +import Test.Hspec (Spec, describe) +import Test.Hspec.QuickCheck (prop) +import Test.QuickCheck (Blind (Blind), arbitrary, forAll, scale) + +-- | Test an external implementation against the Agda executable specification. +spec :: Handle -> Handle -> Spec +spec hReader hWriter = + describe "External node" + . prop "Implementation respects Leios protocol" + $ forAll + arbitrary + (prop_node hReader hWriter . Blind) diff --git a/conformance-testing/app/Pipe.hs b/conformance-testing/app/Pipe.hs new file mode 100644 index 000000000..3295eba25 --- /dev/null +++ b/conformance-testing/app/Pipe.hs @@ -0,0 +1,106 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TupleSections #-} + +import Control.Concurrent.Class.MonadSTM ( + MonadSTM (atomically, modifyTVar'), + ) +import Control.Monad (void, when) +import Control.Monad.IO.Class (MonadIO (..)) +import Control.Tracer (Tracer, nullTracer) +import Data.Aeson qualified as A +import Data.ByteString.Char8 qualified as BS8 +import Data.ByteString.Lazy qualified as LBS +import Data.ByteString.Lazy.Char8 qualified as LBS8 +import Data.Default (def) +import Data.Map qualified as Map (fromList) +import Data.Set qualified as Set (fromList) +import Data.Text (Text, unpack) +import Data.Version (showVersion) +import Options.Applicative qualified as O +import Paths_leios_conformance (version) + +import Data.List ((\\)) +import Data.Maybe (fromMaybe) +import Leios.Conformance.Model +import Leios.Conformance.Test +import Leios.Conformance.Test.External +import System.Exit (die) +import System.IO +import Prelude hiding (getLine, round) + +main :: IO () +main = + do + Command{..} <- O.execParser commandParser + let hReader = stdin + hWriter = stdout + hSetBuffering hReader LineBuffering + hSetBuffering hWriter LineBuffering + let + go node = + do + -- Verified that this reads UTF-8. + (A.eitherDecode . LBS.fromStrict <$> BS8.hGetLine hReader) + >>= \case + Right req -> do + (res, node') <- handle node req + when verbose $ do + LBS8.hPutStrLn stderr $ A.encode req + LBS8.hPutStrLn stderr $ A.encode res + LBS8.hPutStrLn stderr mempty + case res of + Stopped -> pure () + Failed e -> die e + _ -> do + -- Verified that this writes UTF-8. + LBS8.hPutStrLn hWriter $ A.encode res + go node' + Left e -> die $ show e + in + go =<< pure initialModelState + +makeTxs :: LeiosState -> ComputationResult Text (LeiosOutput, LeiosState) +makeTxs = flip step (I_SUBMIT (Right [0 .. 10])) -- FIXME: where to get txs from? + +handle :: MonadIO m => MonadSTM m => NodeModel -> NodeRequest -> m (NodeResponse, NodeModel) +handle node = + \case + Initialize -> pure (def, initialModelState) + NewSlot i e v -> + let ffd = fFDState node + ffd' = + ffd + { inIBs = inIBs ffd ++ i + , inEBs = inEBs ffd ++ e + , inVTs = inVTs ffd ++ v + } + in case makeStep' (node{fFDState = ffd', toPropose = [0 .. 10]}) of -- FIXME: see makeTxs above + Success (_, node') -> + let ibs' = (outIBs $ fFDState node') \\ (outIBs $ fFDState node) + ebs' = (outEBs $ fFDState node') \\ (outEBs $ fFDState node) + vts' = (outVTs $ fFDState node') \\ (outVTs $ fFDState node) + res = NodeResponse{diffuseIBs = ibs', diffuseEBs = ebs', diffuseVotes = vts'} + in pure (res, node') + Failure m -> pure (Failed{failure = unpack m}, node) + Stop -> pure (Stopped, node) + +newtype Command = Command + { verbose :: Bool + } + deriving (Eq, Ord, Read, Show) + +commandParser :: O.ParserInfo Command +commandParser = + let commandOptions = + Command + <$> O.flag False True (O.long "verbose" <> O.help "Whether to output requests, traces, and responses.") + in O.info + ( O.helper + <*> O.infoOption ("leios-simulation-pipe " <> showVersion version) (O.long "version" <> O.help "Show version.") + <*> commandOptions + ) + ( O.fullDesc + <> O.progDesc "This command-line tool simulates a Leios node, reading JSON input and writing JSON output." + <> O.header "leios-simulation-pipe: simulate a Leios node via pipes" + ) diff --git a/conformance-testing/conformance-testing-pipeline.jpg b/conformance-testing/conformance-testing-pipeline.jpg new file mode 100644 index 000000000..88b29bd9d Binary files /dev/null and b/conformance-testing/conformance-testing-pipeline.jpg differ diff --git a/conformance-testing/leios-conformance.cabal b/conformance-testing/leios-conformance.cabal new file mode 100644 index 000000000..a4f7c78f4 --- /dev/null +++ b/conformance-testing/leios-conformance.cabal @@ -0,0 +1,80 @@ +cabal-version: 3.4 +name: leios-conformance +version: 0.1.0.0 +license: Apache-2.0 +license-file: LICENSE +author: Arnaud Bailly +maintainer: arnaud@pankzsoft.com +category: Testing +build-type: Simple + +common warnings + ghc-options: -Wall + default-extensions: + DuplicateRecordFields + GADTs + ImportQualifiedPost + KindSignatures + NamedFieldPuns + +library + import: warnings + exposed-modules: + Leios.Conformance.Model + Leios.Conformance.Test + Leios.Conformance.Test.External + + build-depends: + , aeson + , base + , bytestring + , containers + , data-default + , leios-spec + , mtl + , pretty + , QuickCheck + , quickcheck-dynamic + , quickcheck-instances + , stm + , text + + hs-source-dirs: src + default-language: Haskell2010 + +executable leios-simulation-pipe + import: warnings + default-language: Haskell2010 + hs-source-dirs: app + main-is: Pipe.hs + other-modules: Paths_leios_conformance + build-depends: + , aeson + , base + , bytestring + , containers + , contra-tracer + , data-default + , io-classes + , leios-conformance + , optparse-applicative + , text + +executable leios-conformance-test + import: warnings + default-language: Haskell2010 + other-modules: + Leios.Conformance.ExternalSpec + Paths_leios_conformance + + hs-source-dirs: app + main-is: External.hs + build-depends: + , aeson + , base + , bytestring + , hspec + , leios-conformance + , QuickCheck + + ghc-options: -rtsopts -threaded diff --git a/conformance-testing/src/Leios/Conformance/Model.hs b/conformance-testing/src/Leios/Conformance/Model.hs new file mode 100644 index 000000000..8c92f6391 --- /dev/null +++ b/conformance-testing/src/Leios/Conformance/Model.hs @@ -0,0 +1,124 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Leios.Conformance.Model ( + module Leios.Conformance.Model, + module Lib, +) where + +import Data.Aeson (FromJSON (..), ToJSON (..)) +import Data.List ((\\)) +import Data.Text (unpack) +import Data.Text.Internal (Text (..)) +import Lib +import Text.PrettyPrint (braces, hang, vcat) +import Text.PrettyPrint.HughesPJClass ( + Pretty (pPrint), + ) + +data EnvAction + = Tick + | NewIB InputBlock + | NewEB EndorserBlock + | NewVote Vote + deriving (Eq, Show) + +instance FromJSON IBHeader +instance FromJSON IBBody +instance FromJSON InputBlock + +instance ToJSON IBHeader +instance ToJSON IBBody +instance ToJSON InputBlock + +instance Pretty Text where + pPrint = pPrint . unpack + +instance Pretty InputBlock where + pPrint (InputBlock{header = IBHeader s p hb, body = IBBody{..}}) = + hang "InputBlock" 2 $ + braces $ + vcat + [ hang "slot number =" 2 $ pPrint s + , hang "producer Id =" 2 $ pPrint p + , hang "body hash =" 2 $ pPrint hb + , hang "transactions =" 2 $ pPrint txs + ] + +instance FromJSON EndorserBlock +instance ToJSON EndorserBlock + +instance Pretty EndorserBlock where + pPrint (EndorserBlock s p ibs) = + hang "EndorserBlock" 2 $ + braces $ + vcat + [ hang "slot number =" 2 $ pPrint s + , hang "producer Id =" 2 $ pPrint p + , hang "IB refs=" 2 $ pPrint ibs + ] + +type Vote = () -- TODO: use Vote extracted from Agda +type NodeModel = LeiosState + +initialModelState :: NodeModel +initialModelState = + LeiosState + { v = () + , sD = MkHSMap [(0, 45000000000000000)] + , fFDState = FFDState [] [] [] [] [] [] + , ledger = [] + , toPropose = [] + , iBs = [] + , eBs = [] + , vs = [] + , slot = 0 + , iBHeaders = [] + , iBBodies = [] + , upkeep = MkHSSet [] + , baseState = () + , votingState = () + } + +makeTx :: LeiosState -> ComputationResult Text (LeiosOutput, LeiosState) +makeTx = flip step (I_SUBMIT (Right [0 .. 10])) -- FIXME: where to get txs from + +makeStep' :: LeiosState -> ComputationResult Text (LeiosOutput, LeiosState) +makeStep' = flip step I_SLOT + +makeStep :: NodeModel -> Maybe NodeModel +makeStep nm = + case makeStep' nm of + Success (_, s) -> Just s + Failure _ -> Nothing + +addIB :: InputBlock -> NodeModel -> NodeModel +addIB ib nm@LeiosState{..} = nm{fFDState = fFDState{inIBs = ib : inIBs fFDState}} + +addEB :: EndorserBlock -> NodeModel -> NodeModel +addEB eb nm@LeiosState{..} = nm{fFDState = fFDState{inEBs = eb : inEBs fFDState}} + +addVote :: Vote -> NodeModel -> NodeModel +addVote x nm@LeiosState{..} = nm{fFDState = fFDState{inVTs = [x] : inVTs fFDState}} + +-- TODO: export from Agda +transition :: NodeModel -> EnvAction -> Maybe (([InputBlock], [EndorserBlock], [[Vote]]), NodeModel) +transition s Tick = do + -- TODO: guards + let ffd = fFDState s + s' <- makeStep (s{toPropose = [0 .. 10]}) -- FIXME: see makeTx above + let ffd' = fFDState s' + pure ((outIBs ffd' \\ outIBs ffd, outEBs ffd' \\ outEBs ffd, outVTs ffd' \\ outVTs ffd), s') +transition nm (NewIB ib) = do + -- TODO: guards + pure (([], [], []), addIB ib nm) +transition nm (NewEB eb) = do + -- TODO: guards + pure (([], [], []), addEB eb nm) +transition nm (NewVote v) = do + -- TODO: guards + pure (([], [], []), addVote v nm) diff --git a/conformance-testing/src/Leios/Conformance/Test.hs b/conformance-testing/src/Leios/Conformance/Test.hs new file mode 100644 index 000000000..c6334fdf3 --- /dev/null +++ b/conformance-testing/src/Leios/Conformance/Test.hs @@ -0,0 +1,128 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Leios.Conformance.Test where + +import Data.List (sort) +import Data.Maybe (isJust) +import Data.Text (Text, intercalate, pack) +import Test.QuickCheck ( + Arbitrary (..), + Gen, + chooseInteger, + frequency, + suchThat, + ) +import Test.QuickCheck.DynamicLogic (DynLogicModel) +import Test.QuickCheck.StateModel ( + Any (Some), + HasVariables (..), + StateModel ( + Action, + arbitraryAction, + initialState, + nextState, + precondition, + shrinkAction + ), + ) +import Text.PrettyPrint ((<+>)) +import Text.PrettyPrint.HughesPJClass ( + Pretty (pPrint), + ) + +import Leios.Conformance.Model ( + EndorserBlock (..), + EnvAction (..), + IBBody (..), + IBHeader (..), + InputBlock (..), + LeiosState (..), + NodeModel (..), + Vote, + initialModelState, + transition, + ) + +data NetworkModel = NetworkModel + { nodeModel :: NodeModel + , initialized :: Bool + } + deriving (Show) + +instance HasVariables NetworkModel where + getAllVariables _ = mempty + +instance DynLogicModel NetworkModel + +instance Show (Action NetworkModel a) where + show (Step a) = show a +deriving instance Eq (Action NetworkModel a) + +instance HasVariables (Action NetworkModel a) where + getAllVariables _ = mempty + +instance Pretty EnvAction where + pPrint Tick = "Tick" + pPrint (NewIB ib) = "NewIB" <+> pPrint ib + pPrint (NewEB eb) = "NewEB" <+> pPrint eb + pPrint (NewVote v) = "NewVote" <+> pPrint v + +genPositiveInteger :: Gen Integer +genPositiveInteger = abs <$> arbitrary + +genSlot :: Gen Integer +genSlot = genPositiveInteger + +genProducer :: Gen Integer +genProducer = pure 0 -- FIXME: different parties + +genSortedList :: Gen [Integer] +genSortedList = sort <$> arbitrary + +instance Arbitrary InputBlock where + arbitrary = do + b <- IBBody <$> genSortedList + let t = hash (txs b) + h <- IBHeader <$> genSlot <*> genProducer <*> pure t + pure $ InputBlock h b + where + hash :: [Integer] -> Text + hash = intercalate "#" . map (pack . show) + +instance Arbitrary EndorserBlock where + arbitrary = + let ibs = arbitrary :: Gen [InputBlock] + ibRefs = map (bodyHash . header) <$> ibs + in EndorserBlock <$> genSlot <*> genProducer <*> ibRefs + +instance StateModel NetworkModel where + data Action NetworkModel a where + Step :: EnvAction -> Action NetworkModel ([InputBlock], [EndorserBlock], [[Vote]]) + + initialState = + NetworkModel + { nodeModel = initialModelState + , initialized = True + } + + arbitraryAction _ NetworkModel{nodeModel = LeiosState{..}} = do + fmap (Some . Step) . frequency $ + [(1, pure Tick)] + ++ fmap (10,) [NewIB <$> arbitrary] + ++ fmap (1,) [NewEB <$> arbitrary] + ++ fmap (1,) [NewVote <$> arbitrary] + + shrinkAction _ _ (Step Tick) = [] + shrinkAction _ _ Step{} = [Some (Step Tick)] + + precondition NetworkModel{nodeModel = s} (Step a) = isJust $ transition s a + + nextState net@NetworkModel{nodeModel = s} (Step a) _ = net{nodeModel = maybe s snd $ transition s a} diff --git a/conformance-testing/src/Leios/Conformance/Test/External.hs b/conformance-testing/src/Leios/Conformance/Test/External.hs new file mode 100644 index 000000000..b6cd644f9 --- /dev/null +++ b/conformance-testing/src/Leios/Conformance/Test/External.hs @@ -0,0 +1,176 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module Leios.Conformance.Test.External where + +import Control.Monad (unless, when) +import Control.Monad.IO.Class () +import Control.Monad.State ( + MonadState (get), + MonadTrans (lift), + StateT, + modify, + ) +import Data.Aeson (FromJSON, ToJSON) +import Data.Aeson qualified as A +import Data.ByteString.Char8 qualified as BS8 +import Data.ByteString.Lazy qualified as LBS +import Data.ByteString.Lazy.Char8 qualified as LBS8 +import Data.Default (Default (def)) +import GHC.Generics (Generic) +import System.IO (Handle) +import Test.QuickCheck ( + Blind (Blind), + Property, + counterexample, + ioProperty, + noShrinking, + ) +import Test.QuickCheck.Extras (runPropertyStateT) +import Test.QuickCheck.Monadic (monadicIO, monitor) +import Test.QuickCheck.StateModel ( + Actions, + Realized, + RunModel (perform, postcondition), + counterexamplePost, + monitorPost, + runActions, + ) + +import Text.PrettyPrint (hang, vcat, (<+>)) +import Text.PrettyPrint.HughesPJClass (Pretty (pPrint)) + +import Prelude hiding (round) + +import Leios.Conformance.Model +import Leios.Conformance.Test + +data NodeRequest + = Initialize + | NewSlot + { newIBs :: [InputBlock] + , newEBs :: [EndorserBlock] + , newVotes :: [[Vote]] + } + | Stop + deriving (Eq, Generic, Show) + +instance FromJSON NodeRequest +instance ToJSON NodeRequest + +data NodeResponse + = NodeResponse + { diffuseIBs :: [InputBlock] + , diffuseEBs :: [EndorserBlock] + , diffuseVotes :: [[Vote]] + } + | Failed + { failure :: String + } + | Stopped + deriving (Eq, Generic, Show) + +instance Default NodeResponse where + def = NodeResponse mempty mempty mempty + +instance FromJSON NodeResponse +instance ToJSON NodeResponse + +data RunState = RunState + { hReader :: Handle + , hWriter :: Handle + , unfetchedIBs :: [InputBlock] + , unfetchedEBs :: [EndorserBlock] + , unfetchedVotes :: [[Vote]] + } + +callSUT :: RunState -> NodeRequest -> IO NodeResponse +callSUT RunState{hReader, hWriter} req = + do + LBS8.hPutStrLn hWriter $ A.encode req + either Failed id . A.eitherDecode' . LBS.fromStrict <$> BS8.hGetLine hReader + +type Runtime = StateT RunState IO + +instance Realized IO ([InputBlock], [EndorserBlock], [[Vote]]) ~ ([InputBlock], [EndorserBlock], [[Vote]]) => RunModel NetworkModel Runtime where + perform NetworkModel{nodeModel = LeiosState{..}} (Step a) _ = case a of + Tick -> do + rs@RunState{..} <- get + modify $ \rs' -> rs'{unfetchedIBs = mempty, unfetchedEBs = mempty, unfetchedVotes = mempty} + lift + ( callSUT + rs + NewSlot + { newIBs = unfetchedIBs + , newEBs = unfetchedEBs + , newVotes = unfetchedVotes + } + ) + >>= \case + NodeResponse{..} -> pure (diffuseIBs, diffuseEBs, diffuseVotes) + _ -> pure (mempty, mempty, mempty) -- FIXME: The state model should define an error type. + NewIB ib -> do + modify $ \rs -> rs{unfetchedIBs = unfetchedIBs rs ++ pure ib} + pure (mempty, mempty, mempty) + NewEB eb -> do + modify $ \rs -> rs{unfetchedEBs = unfetchedEBs rs ++ pure eb} + pure (mempty, mempty, mempty) + NewVote x -> do + modify $ \rs -> rs{unfetchedVotes = unfetchedVotes rs ++ pure [x]} + pure (mempty, mempty, mempty) + + postcondition (NetworkModel{nodeModel = s}, NetworkModel{nodeModel = s'}) (Step a) _ (ibs, ebs, votes) = do + let (expectedIBs, expectedEBs, expectedVotes) = maybe (mempty, mempty, mempty) fst $ transition s a + let ok = (ibs, ebs) == (expectedIBs, expectedEBs) + monitorPost . counterexample . show $ " action $" <+> pPrint a + when (a == Tick && slot s + 1 /= slot s') $ + monitorPost . counterexample $ + " -- new slot: " ++ show (slot s') + unless (null ibs) $ + monitorPost . counterexample . show $ + " -- got InputBlocks:" <+> pPrint ibs + when (ibs /= expectedIBs) $ + counterexamplePost . show $ + " -- expected InputBlocks:" <+> pPrint expectedIBs + unless (null ebs) $ + monitorPost . counterexample . show $ + " -- got EndorserBlocks:" <+> pPrint ebs + when (ebs /= expectedEBs) $ + counterexamplePost . show $ + " -- expected EndorserBlocks:" <+> pPrint expectedEBs + unless (null votes) $ + monitorPost . counterexample . show $ + " -- got Votes:" <+> pPrint votes + when (votes /= expectedVotes) $ + counterexamplePost . show $ + " -- expected Votes:" <+> pPrint expectedVotes + pure ok + +prop_node :: Handle -> Handle -> Blind (Actions NetworkModel) -> Property +prop_node hReader hWriter (Blind as) = noShrinking $ + ioProperty $ do + let unfetchedIBs = mempty + unfetchedEBs = mempty + unfetchedVotes = mempty + callSUT + RunState{..} + Initialize + >>= \case + NodeResponse{} -> + pure $ + monadicIO $ do + monitor $ counterexample "-- Actions:" + monitor $ counterexample "do" + _ <- runPropertyStateT (runActions @_ @Runtime as) RunState{..} + pure True + _ -> pure $ monadicIO $ pure False diff --git a/flake.lock b/flake.lock index 4825972c0..05197e624 100644 --- a/flake.lock +++ b/flake.lock @@ -3,15 +3,15 @@ "CHaP": { "flake": false, "locked": { - "lastModified": 1724604182, - "narHash": "sha256-gQmj2hHwEvS29Gf+juG95T7Qt5LfzDJKzdPajcuHZgs=", - "owner": "input-output-hk", + "lastModified": 1733132525, + "narHash": "sha256-qD1Mo1MUxaNJnJCAQHMo5cfgMoHv6nb7nTS087CPkio=", + "owner": "IntersectMBO", "repo": "cardano-haskell-packages", - "rev": "3a25be01c845e86092e514403882ac74141ac3da", + "rev": "4bd42413109a7935695346cabdf4f528f0e4f36f", "type": "github" }, "original": { - "owner": "input-output-hk", + "owner": "IntersectMBO", "ref": "repo", "repo": "cardano-haskell-packages", "type": "github" @@ -153,11 +153,11 @@ }, "flake-compat": { "locked": { - "lastModified": 1696426674, - "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", + "lastModified": 1733328505, + "narHash": "sha256-NeCCThCEP3eCl2l/+27kNNK7QrwZB1IJCrXfrbv5oqU=", "owner": "edolstra", "repo": "flake-compat", - "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", + "rev": "ff81ac966bb2cae68946d5ed5fc4994f96d0ffec", "type": "github" }, "original": { @@ -222,11 +222,11 @@ "systems": "systems_2" }, "locked": { - "lastModified": 1710146030, - "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", "owner": "numtide", "repo": "flake-utils", - "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", "type": "github" }, "original": { @@ -295,11 +295,11 @@ "hackage": { "flake": false, "locked": { - "lastModified": 1724632371, - "narHash": "sha256-8MKEmQeJ4ft4PEcU85sCr+DqTc7wpLLV3Wt8jC9PZ+Q=", + "lastModified": 1733358616, + "narHash": "sha256-96x1H0cfIX2iMx3FkmFDoXohBCBVUJt5DH3457xAXVM=", "owner": "input-output-hk", "repo": "hackage.nix", - "rev": "28717c62d061f1936eb96b4c5814b7df0c31fa0d", + "rev": "bb0ec3418c4593dd79ed2f5423f8fddd1db726ae", "type": "github" }, "original": { @@ -352,11 +352,11 @@ "stackage": "stackage" }, "locked": { - "lastModified": 1724633441, - "narHash": "sha256-jPVqNPQabeEIGUxyCMyOmer3JwSdHdleGGLwydrPvf0=", + "lastModified": 1733359919, + "narHash": "sha256-5LI4bETTK7fi+nr5nfSEQEBhx8+ZtKHFrH9oEqlj18E=", "owner": "input-output-hk", "repo": "haskell.nix", - "rev": "00ca0e2522e2ec124bf4ed5285685e524fbe38ee", + "rev": "6bfaa3f488a3aa20153d9278a311120a9036459a", "type": "github" }, "original": { @@ -521,16 +521,16 @@ "hls-2.9": { "flake": false, "locked": { - "lastModified": 1718469202, - "narHash": "sha256-THXSz+iwB1yQQsr/PY151+2GvtoJnTIB2pIQ4OzfjD4=", + "lastModified": 1720003792, + "narHash": "sha256-qnDx8Pk0UxtoPr7BimEsAZh9g2WuTuMB/kGqnmdryKs=", "owner": "haskell", "repo": "haskell-language-server", - "rev": "40891bccb235ebacce020b598b083eab9dda80f1", + "rev": "0c1817cb2babef0765e4e72dd297c013e8e3d12b", "type": "github" }, "original": { "owner": "haskell", - "ref": "2.9.0.0", + "ref": "2.9.0.1", "repo": "haskell-language-server", "type": "github" } @@ -595,11 +595,11 @@ "sphinxcontrib-haddock": "sphinxcontrib-haddock" }, "locked": { - "lastModified": 1724699322, - "narHash": "sha256-H+d9HhoKZ7yItB4DqWxTEN+P5xtBnrNTYi3hXMakjzI=", + "lastModified": 1733738060, + "narHash": "sha256-uZZB/JE7ED7QWfsj9UOQriu3E5kDCtgWMvLCVujnqAo=", "owner": "input-output-hk", "repo": "iogx", - "rev": "9720ba9bcaf738f65fbc530e427caea7bcc0d7d1", + "rev": "507209c0acf0aaf607626d73b1711ea0afde7108", "type": "github" }, "original": { @@ -619,11 +619,11 @@ "sodium": "sodium" }, "locked": { - "lastModified": 1721825987, - "narHash": "sha256-PPcma4tjozwXJAWf+YtHUQUulmxwulVlwSQzKItx/n8=", + "lastModified": 1732287300, + "narHash": "sha256-lURsE6HdJX0alscWhbzCWyLRK8GpAgKuXeIgX31Kfqg=", "owner": "input-output-hk", "repo": "iohk-nix", - "rev": "eb61f2c14e1f610ec59117ad40f8690cddbf80cb", + "rev": "262cb2aec2ddd914124bab90b06fe24a1a74d02c", "type": "github" }, "original": { @@ -692,11 +692,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1720642556, - "narHash": "sha256-qsnqk13UmREKmRT7c8hEnz26X3GFFyIQrqx4EaRc1Is=", + "lastModified": 1730479402, + "narHash": "sha256-79NLeNjpCa4mSasmFsE3QA6obURezF0TUO5Pm+1daog=", "owner": "nlewo", "repo": "nix2container", - "rev": "3853e5caf9ad24103b13aa6e0e8bcebb47649fe4", + "rev": "5fb215a1564baa74ce04ad7f903d94ad6617e17a", "type": "github" }, "original": { @@ -835,11 +835,11 @@ }, "nixpkgs-2405": { "locked": { - "lastModified": 1720122915, - "narHash": "sha256-Nby8WWxj0elBu1xuRaUcRjPi/rU3xVbkAt2kj4QwX2U=", + "lastModified": 1729242558, + "narHash": "sha256-VgcLDu4igNT0eYua6OAl9pWCI0cYXhDbR+pWP44tte0=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "835cf2d3f37989c5db6585a28de967a667a75fb1", + "rev": "4a3f2d3195b60d07530574988df92e049372c10e", "type": "github" }, "original": { @@ -883,11 +883,11 @@ }, "nixpkgs-stable_2": { "locked": { - "lastModified": 1720386169, - "narHash": "sha256-NGKVY4PjzwAa4upkGtAMz1npHGoRzWotlSnVlqI40mo=", + "lastModified": 1730741070, + "narHash": "sha256-edm8WG19kWozJ/GqyYx2VjW99EdhjKwbY3ZwdlPAAlo=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "194846768975b7ad2c4988bdb82572c00222c0d7", + "rev": "d063c1dd113c91ab27959ba540c0d9753409edf3", "type": "github" }, "original": { @@ -899,11 +899,11 @@ }, "nixpkgs-unstable": { "locked": { - "lastModified": 1720181791, - "narHash": "sha256-i4vJL12/AdyuQuviMMd1Hk2tsGt02hDNhA0Zj1m16N8=", + "lastModified": 1729980323, + "narHash": "sha256-eWPRZAlhf446bKSmzw6x7RWEE4IuZgAp8NW3eXZwRAY=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "4284c2b73c8bce4b46a6adf23e16d9e2ec8da4bb", + "rev": "86e78d3d2084ff87688da662cf78c2af085d8e73", "type": "github" }, "original": { @@ -930,11 +930,11 @@ }, "nixpkgs_3": { "locked": { - "lastModified": 1719082008, - "narHash": "sha256-jHJSUH619zBQ6WdC21fFAlDxHErKVDJ5fpN0Hgx4sjs=", + "lastModified": 1730768919, + "narHash": "sha256-8AKquNnnSaJRXZxc5YmF/WfmxiHX6MMZZasRP6RRQkE=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "9693852a2070b398ee123a329e68f0dab5526681", + "rev": "a04d33c0c3f1a59a2c1cb0c6e34cd24500e5a1dc", "type": "github" }, "original": { @@ -969,11 +969,11 @@ "nixpkgs-stable": "nixpkgs-stable_2" }, "locked": { - "lastModified": 1724440431, - "narHash": "sha256-9etXEOUtzeMgqg1u0wp+EdwG7RpmrAZ2yX516bMj2aE=", + "lastModified": 1733318908, + "narHash": "sha256-SVQVsbafSM1dJ4fpgyBqLZ+Lft+jcQuMtEL3lQWx2Sk=", "owner": "cachix", "repo": "pre-commit-hooks.nix", - "rev": "c8a54057aae480c56e28ef3e14e4960628ac495b", + "rev": "6f4e2a2112050951a314d2733a994fbab94864c6", "type": "github" }, "original": { @@ -1041,11 +1041,11 @@ "stackage": { "flake": false, "locked": { - "lastModified": 1724631220, - "narHash": "sha256-aXkNOrKlGKFO4BfPMo28Br0+A5arKJYCZvbAyj0d3Yk=", + "lastModified": 1733357539, + "narHash": "sha256-r5B5lCFZC1a/V+banTIYzjOVlP2lIuLrhnC1FnCMAl0=", "owner": "input-output-hk", "repo": "stackage.nix", - "rev": "73edb7f9d4b83b19246ab92592e0e7699faddcd9", + "rev": "d6b9beeb93d98ea98b6ad32f36768cad48177e89", "type": "github" }, "original": { diff --git a/formal-spec/CategoricalCrypto.agda b/formal-spec/CategoricalCrypto.agda deleted file mode 100644 index 76f053d7a..000000000 --- a/formal-spec/CategoricalCrypto.agda +++ /dev/null @@ -1,332 +0,0 @@ -module CategoricalCrypto where - -open import abstract-set-theory.Prelude hiding (id; _โˆ˜_; _โŠ—_; lookup; Dec) - --------------------------------------------------------------------------------- --- Channels, which form the objects - -record Channel : Setโ‚ where - field P : Set - rcvType sndType : P โ†’ Set - -infixr 9 _โŠ—_ - -I : Channel -I .Channel.P = โŠฅ - -_แต€ : Channel โ†’ Channel -_แต€ c = let open Channel c in ฮป where .P โ†’ P ; .rcvType โ†’ sndType ; .sndType โ†’ rcvType - -_โŠ—_ : Channel โ†’ Channel โ†’ Channel -cโ‚ โŠ— cโ‚‚ = let open Channel cโ‚ renaming (P to Pโ‚; rcvType to rcvTypeโ‚; sndType to sndTypeโ‚) - open Channel cโ‚‚ renaming (P to Pโ‚‚; rcvType to rcvTypeโ‚‚; sndType to sndTypeโ‚‚) - open Channel - in ฮป where - .P โ†’ Pโ‚ โŠŽ Pโ‚‚ - .rcvType (injโ‚ a) โ†’ rcvTypeโ‚ a - .rcvType (injโ‚‚ b) โ†’ rcvTypeโ‚‚ b - .sndType (injโ‚ a) โ†’ sndTypeโ‚ a - .sndType (injโ‚‚ b) โ†’ sndTypeโ‚‚ b - -sndโ‚ : โˆ€ {A B} โ†’ โˆƒ (Channel.sndType A) โ†’ โˆƒ (Channel.sndType (A โŠ— B)) -sndโ‚ (p , m) = injโ‚ p , m - -sndโ‚‚ : โˆ€ {A B} โ†’ โˆƒ (Channel.sndType B) โ†’ โˆƒ (Channel.sndType (A โŠ— B)) -sndโ‚‚ (p , m) = injโ‚‚ p , m - --- being lazy here, this should be an iso instead -postulate - โŠ—-assoc : โˆ€ {A B C} โ†’ (A โŠ— B) โŠ— C โ‰ก A โŠ— (B โŠ— C) - --------------------------------------------------------------------------------- --- Machines, which form the morphisms - -record Machine (A B : Channel) : Setโ‚ where - constructor MkMachine - open Channel (A โŠ— B แต€) public - - field State : Set - stepRel : โˆƒ rcvType โ†’ State โ†’ State ร— Maybe (โˆƒ sndType) โ†’ Set - -module _ {A B} (let open Channel (A โŠ— B แต€)) where - MkMachine' : โˆ€ {State} โ†’ (โˆƒ rcvType โ†’ State โ†’ State ร— Maybe (โˆƒ sndType) โ†’ Set) โ†’ Machine A B - MkMachine' = MkMachine _ - - StatelessMachine : (โˆƒ rcvType โ†’ Maybe (โˆƒ sndType) โ†’ Set) โ†’ Machine A B - StatelessMachine R = MkMachine โŠค (ฮป i _ (_ , o) โ†’ R i o) - - FunctionMachine : (โˆƒ rcvType โ†’ Maybe (โˆƒ sndType)) โ†’ Machine A B - FunctionMachine f = StatelessMachine (ฮป i o โ†’ f i โ‰ก o) - -id : โˆ€ {A} โ†’ Machine A A -id .Machine.State = โŠค -id .Machine.stepRel (injโ‚ a , m) _ (_ , m') = m' โ‰ก just (injโ‚‚ a , m) -id .Machine.stepRel (injโ‚‚ a , m) _ (_ , m') = m' โ‰ก just (injโ‚ a , m) - -module Tensor {A B C D} (Mโ‚ : Machine A B) (Mโ‚‚ : Machine C D) where - open Machine Mโ‚ renaming (State to Stateโ‚; stepRel to stepRelโ‚) - open Machine Mโ‚‚ renaming (State to Stateโ‚‚; stepRel to stepRelโ‚‚) - - State = Stateโ‚ ร— Stateโ‚‚ - - AllCs = (A โŠ— B แต€) โŠ— (C โŠ— D แต€) - - data CompRel : โˆƒ (Channel.rcvType AllCs) โ†’ State โ†’ State ร— Maybe (โˆƒ (Channel.sndType AllCs)) โ†’ Set where - Stepโ‚ : โˆ€ {p m m' s s' sโ‚‚} โ†’ stepRelโ‚ (p , m) s (s' , m') - โ†’ CompRel (injโ‚ p , m) (s , sโ‚‚) ((s' , sโ‚‚) , (sndโ‚ <$> m')) - - Stepโ‚‚ : โˆ€ {p m m' s s' sโ‚} โ†’ stepRelโ‚‚ (p , m) s (s' , m') - โ†’ CompRel (injโ‚‚ p , m) (sโ‚ , s) ((sโ‚ , s') , (sndโ‚‚ <$> m')) - - - _โŠ—'_ : Machine (A โŠ— C) (B โŠ— D) - _โŠ—'_ = ฮป where - .Machine.State โ†’ State - .Machine.stepRel m s (s' , m') โ†’ CompRel - (case m of ฮป where - (injโ‚ (injโ‚ p) , m) โ†’ (injโ‚ (injโ‚ p) , m) - (injโ‚ (injโ‚‚ p) , m) โ†’ (injโ‚‚ (injโ‚ p) , m) - (injโ‚‚ (injโ‚ p) , m) โ†’ (injโ‚ (injโ‚‚ p) , m) - (injโ‚‚ (injโ‚‚ p) , m) โ†’ (injโ‚‚ (injโ‚‚ p) , m)) - s - (s' , ((ฮป where - (injโ‚ (injโ‚ p) , m) โ†’ (injโ‚ (injโ‚ p) , m) - (injโ‚ (injโ‚‚ p) , m) โ†’ (injโ‚‚ (injโ‚ p) , m) - (injโ‚‚ (injโ‚ p) , m) โ†’ (injโ‚ (injโ‚‚ p) , m) - (injโ‚‚ (injโ‚‚ p) , m) โ†’ (injโ‚‚ (injโ‚‚ p) , m)) <$> m')) - -open Tensor using (_โŠ—'_) public - -_โŠ—หก_ : โˆ€ {A B} โ†’ (C : Channel) โ†’ Machine A B โ†’ Machine (C โŠ— A) (C โŠ— B) -C โŠ—หก M = id โŠ—' M - -_โŠ—สณ_ : โˆ€ {A B} โ†’ Machine A B โ†’ (C : Channel) โ†’ Machine (A โŠ— C) (B โŠ— C) -M โŠ—สณ C = M โŠ—' id - -module Comp {A B C} (Mโ‚ : Machine B C) (Mโ‚‚ : Machine A B) where - open Machine Mโ‚ renaming (State to Stateโ‚; stepRel to stepRelโ‚) - open Machine Mโ‚‚ renaming (State to Stateโ‚‚; stepRel to stepRelโ‚‚) - - State = Stateโ‚ ร— Stateโ‚‚ - - AllCs = (A โŠ— B แต€) โŠ— (B โŠ— C แต€) - - data CompRel : โˆƒ (Channel.rcvType AllCs) โ†’ State โ†’ State ร— Maybe (โˆƒ (Channel.sndType AllCs)) โ†’ Set where - Stepโ‚ : โˆ€ {p m m' s s' sโ‚‚} โ†’ stepRelโ‚ (p , m) s (s' , m') - โ†’ CompRel (injโ‚‚ p , m) (s , sโ‚‚) ((s' , sโ‚‚) , (sndโ‚‚ <$> m')) - - Stepโ‚‚ : โˆ€ {p m m' s s' sโ‚} โ†’ stepRelโ‚‚ (p , m) s (s' , m') - โ†’ CompRel (injโ‚ p , m) (sโ‚ , s) ((sโ‚ , s') , (sndโ‚ <$> m')) - - Multiโ‚ : โˆ€ {p m m' m'' s s' s''} - โ†’ CompRel m s (s' , just ((injโ‚‚ (injโ‚ p) , m'))) - โ†’ CompRel (injโ‚ (injโ‚‚ p) , m') s' (s'' , m'') - โ†’ CompRel m s (s'' , m'') - - Multiโ‚‚ : โˆ€ {p m m' m'' s s' s''} - โ†’ CompRel m s (s' , just (injโ‚ (injโ‚‚ p) , m')) - โ†’ CompRel (injโ‚‚ (injโ‚ p) , m') s' (s'' , m'') - โ†’ CompRel m s (s'' , m'') - - infixr 9 _โˆ˜_ - - _โˆ˜_ : Machine A C - _โˆ˜_ = ฮป where - .Machine.State โ†’ State - .Machine.stepRel m s (s' , m') โ†’ - CompRel - (case m of ฮป where (injโ‚ x , m) โ†’ injโ‚ (injโ‚ x) , m ; (injโ‚‚ y , m) โ†’ injโ‚‚ (injโ‚‚ y) , m) - s (s' , ((ฮป where (injโ‚ x , m) โ†’ injโ‚ (injโ‚ x) , m ; (injโ‚‚ y , m) โ†’ injโ‚‚ (injโ‚‚ y) , m) <$> m')) - -open Comp using (_โˆ˜_) public - --------------------------------------------------------------------------------- --- Environment model - -โ„ฐ-Out : Channel -โ„ฐ-Out .Channel.P = โŠค -โ„ฐ-Out .Channel.sndType _ = Bool -โ„ฐ-Out .Channel.rcvType _ = โŠฅ - --- Presheaf on the category of channels & machines --- we just take machines that output a boolean --- for now, not on the Kleisli construction -โ„ฐ : Channel โ†’ Setโ‚ -โ„ฐ C = Machine C โ„ฐ-Out - -map-โ„ฐ : โˆ€ {A B} โ†’ Machine A B โ†’ โ„ฐ B โ†’ โ„ฐ A -map-โ„ฐ M E = E โˆ˜ M - --------------------------------------------------------------------------------- --- UC relations - --- perfect equivalence -_โ‰ˆโ„ฐ_ : โˆ€ {A B} โ†’ Machine A B โ†’ Machine A B โ†’ Setโ‚ -_โ‰ˆโ„ฐ_ {B = B} M M' = (E : โ„ฐ B) โ†’ map-โ„ฐ M E โ‰ก map-โ„ฐ M' E - -_โ‰คUC_ : โˆ€ {A B E E''} โ†’ Machine A (B โŠ— E) โ†’ Machine A (B โŠ— E'') โ†’ Setโ‚ -_โ‰คUC_ {B = B} {E} R I = โˆ€ E' (A : Machine E E') โ†’ โˆƒ[ S ] ((B โŠ—หก A) โˆ˜ R) โ‰ˆโ„ฐ ((B โŠ—หก S) โˆ˜ I) - --- equivalent to _โ‰คUC_ by "completeness of the dummy adversary" -_โ‰ค'UC_ : โˆ€ {A B E} โ†’ Machine A (B โŠ— E) โ†’ Machine A (B โŠ— E) โ†’ Setโ‚ -_โ‰ค'UC_ {B = B} R I = โˆƒ[ S ] R โ‰ˆโ„ฐ (B โŠ—หก S โˆ˜ I) - - --------------------------------------------------------------------------------- --- Example functionalities - -module LeakyChannel (M : Set) where - -- authenticated, non-lossy, leaks all messages - - open Channel - - A B E : Channel - - -- can receive messages from Alice (in reverse) - A .P = โŠค - A .sndType _ = M - A .rcvType _ = โŠฅ - - -- can send messages to Bob (in reverse) - B .P = โŠค - B .sndType _ = โŠฅ - B .rcvType _ = M - - -- upon request, can send next message to Eve (in reverse) - E .P = โŠค - E .sndType _ = โŠค - E .rcvType _ = M - - open Machine hiding (rcvType; sndType) - - data R : โˆƒ (rcvType (I โŠ— (A โŠ— B โŠ— E) แต€)) - โ†’ List M - โ†’ List M ร— Maybe (โˆƒ (sndType (I โŠ— (A โŠ— B โŠ— E) แต€))) โ†’ Set where - - Send : โˆ€ {m s} โ†’ R (injโ‚‚ (injโ‚ _) , m) s (s โˆทสณ m , just (injโ‚‚ (injโ‚‚ (injโ‚ _)) , m)) - Req : โˆ€ {m s} โ†’ R (injโ‚‚ (injโ‚‚ (injโ‚‚ _)) , _) (m โˆท s) (s , just (injโ‚‚ (injโ‚‚ (injโ‚‚ _)) , m)) - - Functionality : Machine I (A โŠ— B โŠ— E) - Functionality .State = List M -- queue of messages - Functionality .stepRel = R - - - -module SecureChannel (M : Set) where - -- authenticated, non-lossy, leaks only message length - - open Channel - - A B E : Channel - - -- can receive messages from Alice (in reverse) - A .P = โŠค - A .sndType _ = M - A .rcvType _ = โŠฅ - - -- can send messages to Bob (in reverse) - B .P = โŠค - B .sndType _ = โŠฅ - B .rcvType _ = M - - -- upon request, can send length of the next message to Eve (in reverse) - E .P = โŠค - E .sndType _ = โŠค - E .rcvType _ = โ„• - - module _ (msgLen : M โ†’ โ„•) where - - open Machine hiding (rcvType; sndType) - - data R : โˆƒ (rcvType (I โŠ— (A โŠ— B โŠ— E) แต€)) - โ†’ List M - โ†’ List M ร— Maybe (โˆƒ (sndType (I โŠ— (A โŠ— B โŠ— E) แต€))) โ†’ Set where - Send : โˆ€ {m s} โ†’ R (injโ‚‚ (injโ‚ _) , m) s (s โˆทสณ m , just (injโ‚‚ (injโ‚‚ (injโ‚ _)) , m)) - Req : โˆ€ {m s} โ†’ R (injโ‚‚ (injโ‚‚ (injโ‚‚ _)) , _) (m โˆท s) (s , just (injโ‚‚ (injโ‚‚ (injโ‚‚ _)) , msgLen m)) - - Functionality : Machine I (A โŠ— B โŠ— E) - Functionality .State = List M -- queue of messages - Functionality .stepRel = R - - Functionality' : Machine I ((A โŠ— B) โŠ— E) - Functionality' = subst (Machine I) (sym โŠ—-assoc) Functionality - - - -module Encryption (PlainText CipherText PubKey PrivKey : Set) - โฆƒ _ : DecEq CipherText โฆ„ โฆƒ _ : DecEq PubKey โฆ„ - (genCT : โ„• โ†’ CipherText) (getPubKey : PrivKey โ†’ PubKey) where - open Channel - open Machine hiding (rcvType; sndType) - - C : Channel - C .P = โŠค - C .sndType _ = PlainText ร— PubKey โŠŽ CipherText ร— PrivKey - C .rcvType _ = CipherText โŠŽ Maybe PlainText - - S : Set - S = List (PubKey ร— PlainText ร— CipherText) - - lookup : {A : Set} โ†’ List A โ†’ (A โ†’ Bool) โ†’ Maybe A - lookup [] f = nothing - lookup (x โˆท l) f with f x - ... | true = just x - ... | false = lookup l f - - lookupPlainText : S โ†’ CipherText ร— PubKey โ†’ Maybe PlainText - lookupPlainText s (c , k) = projโ‚ <$> (projโ‚‚ <$> lookup s ฮป where (k' , _ , c') โ†’ ยฟ k โ‰ก k' ร— c โ‰ก c' ยฟแต‡) - - data R : โˆƒ (rcvType (I โŠ— (C แต€))) โ†’ S โ†’ S ร— Maybe (โˆƒ (sndType (I โŠ— (C แต€)))) โ†’ Set where - Enc : โˆ€ {p k s} โ†’ let c = genCT (length s) - in R (injโ‚‚ tt , injโ‚ (p , k)) s ((k , p , c) โˆท s , just (injโ‚‚ tt , injโ‚ c)) - Dec : โˆ€ {c k s} โ†’ let p = lookupPlainText s (c , getPubKey k) - in R (injโ‚‚ tt , injโ‚‚ (c , k)) s (s , just (injโ‚‚ tt , injโ‚‚ p)) - - Functionality : Machine I C - Functionality .State = S - Functionality .stepRel = R - -module EncryptionShim (PlainText CipherText PubKey PrivKey : Set) - โฆƒ _ : DecEq CipherText โฆ„ โฆƒ _ : DecEq PubKey โฆ„ - (genCT : โ„• โ†’ CipherText) (getPubKey : PrivKey โ†’ PubKey) - (pubKey : PubKey) (privKey : PrivKey) where - open Channel - open Machine hiding (rcvType; sndType) - - module L = LeakyChannel CipherText - module S = SecureChannel PlainText - module E = Encryption PlainText CipherText PubKey PrivKey genCT getPubKey - - data R : โˆƒ (rcvType ((L.A โŠ— L.B โŠ— L.E) โŠ— ((S.A โŠ— S.B โŠ— S.E) แต€))) - โ†’ E.Functionality .State - โ†’ E.Functionality .State ร— Maybe (โˆƒ (sndType ((L.A โŠ— L.B โŠ— L.E) โŠ— ((S.A โŠ— S.B โŠ— S.E) แต€)))) - โ†’ Set where - EncSend : โˆ€ {m m' s s'} - โ†’ E.R (injโ‚‚ _ , injโ‚ (m , pubKey)) s (s' , just (injโ‚‚ _ , injโ‚ m')) - โ†’ R (injโ‚‚ (injโ‚ _) , m) s (s' , just (injโ‚ (injโ‚ _) , m')) - DecRcv : โˆ€ {m m' s s'} - โ†’ E.R (injโ‚‚ _ , injโ‚‚ (m , privKey)) s (s' , just (injโ‚‚ _ , injโ‚‚ (just m'))) - โ†’ R (injโ‚ (injโ‚‚ (injโ‚ _)) , m) s (s' , just (injโ‚‚ (injโ‚‚ (injโ‚ _)) , m')) - - Functionality : Machine (L.A โŠ— L.B โŠ— L.E) (S.A โŠ— S.B โŠ— S.E) - Functionality .State = E.Functionality .State - Functionality .stepRel = R - -module SecureFromAuthenticated (PlainText CipherText PubKey PrivKey : Set) - โฆƒ _ : DecEq CipherText โฆ„ โฆƒ _ : DecEq PubKey โฆ„ - (genCT : โ„• โ†’ CipherText) (getPubKey : PrivKey โ†’ PubKey) - (pubKey : PubKey) (privKey : PrivKey) - (msgLength : PlainText โ†’ โ„•) where - - module L = LeakyChannel CipherText - module S = SecureChannel PlainText - module SH = EncryptionShim PlainText CipherText PubKey PrivKey genCT getPubKey pubKey privKey - - Functionality : Machine I (S.A โŠ— S.B โŠ— S.E) - Functionality = SH.Functionality โˆ˜ L.Functionality - - Functionality' : Machine I ((S.A โŠ— S.B) โŠ— S.E) - Functionality' = subst (Machine I) (sym โŠ—-assoc) Functionality - - -- Fโ‰คSecure : Functionality' โ‰ค'UC S.Functionality' msgLength - -- Fโ‰คSecure = {!!} diff --git a/formal-spec/Class/Computational22.agda b/formal-spec/Class/Computational22.agda deleted file mode 100644 index 55149a410..000000000 --- a/formal-spec/Class/Computational22.agda +++ /dev/null @@ -1,46 +0,0 @@ -{-# OPTIONS --safe #-} - --------------------------------------------------------------------------------- --- Variant of `Computational` for relations with two inputs and outputs --------------------------------------------------------------------------------- - -module Class.Computational22 where - -open import Leios.Prelude -open import Class.Computational - -private variable - S I O Err : Type - -module _ (STS : S โ†’ I โ†’ O โ†’ S โ†’ Type) where - record Computational22 Err : Typeโ‚ where - constructor MkComputational - field - computeProof : (s : S) (i : I) โ†’ ComputationResult Err (โˆƒ[ (o , s') ] STS s i o s') - - compute : S โ†’ I โ†’ ComputationResult Err (O ร— S) - compute s i = map projโ‚ $ computeProof s i - - field - completeness : โˆ€ s i o s' โ†’ STS s i o s' โ†’ compute s i โ‰ก success (o , s') - - STS' : S ร— I โ†’ O ร— S โ†’ Type - STS' (s , i) (o , s') = STS s i o s' - - module _ โฆƒ _ : Computational22 Err โฆ„ where - open Computational22 it - instance - comp22โ‡’comp : Computational STS' Err - comp22โ‡’comp .Computational.computeProof (s , i) = computeProof s i - comp22โ‡’comp .Computational.completeness (s , i) (o , s') = completeness s i o s' - -module _ {STS : S โ†’ I โ†’ O โ†’ S โ†’ Type} โฆƒ _ : Computational22 STS Err โฆ„ where - open Computational22 it - - -- basically `traverse` - computeTrace : S โ†’ List I โ†’ ComputationResult Err (List O ร— S) - computeTrace s [] = success ([] , s) - computeTrace s (x โˆท is) = do - (o , s') โ† compute s x - (os , s'') โ† computeTrace s' is - return (o โˆท os , s'') diff --git a/formal-spec/Everything.agda b/formal-spec/Everything.agda deleted file mode 100644 index 41e951cd9..000000000 --- a/formal-spec/Everything.agda +++ /dev/null @@ -1,6 +0,0 @@ -module Everything where - -open import Leios.Simplified -open import Leios.Simplified.Deterministic -open import Leios.Short -open import Leios.Network diff --git a/formal-spec/Leios/Abstract.agda b/formal-spec/Leios/Abstract.agda deleted file mode 100644 index f8fd19395..000000000 --- a/formal-spec/Leios/Abstract.agda +++ /dev/null @@ -1,18 +0,0 @@ -{-# OPTIONS --safe #-} - -module Leios.Abstract where - -open import Leios.Prelude - -record LeiosAbstract : Typeโ‚ where - field Tx : Type - PoolID : Type - โฆƒ DecEq-PoolID โฆ„ : DecEq PoolID - BodyHash VrfPf PrivKey Sig Hash : Type -- these could have been byte strings, but this is safer - โฆƒ DecEq-Hash โฆ„ : DecEq Hash - Vote : Type - vote : PrivKey โ†’ Hash โ†’ Vote - sign : PrivKey โ†’ Hash โ†’ Sig - โฆƒ Hashable-Txs โฆ„ : Hashable (List Tx) Hash - L : โ„• - โฆƒ NonZero-L โฆ„ : NonZero L diff --git a/formal-spec/Leios/Base.agda b/formal-spec/Leios/Base.agda deleted file mode 100644 index fc9cbbb5e..000000000 --- a/formal-spec/Leios/Base.agda +++ /dev/null @@ -1,40 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude -open import Leios.Abstract -open import Leios.VRF - -module Leios.Base (a : LeiosAbstract) (open LeiosAbstract a) (vrf' : LeiosVRF a) - (let open LeiosVRF vrf') where - -open import Leios.Blocks a using (EndorserBlock) - -StakeDistr : Type -StakeDistr = TotalMap PoolID โ„• - -RankingBlock : Type -RankingBlock = These EndorserBlock (List Tx) - -record BaseAbstract : Typeโ‚ where - field Cert : Type - VTy : Type - initSlot : VTy โ†’ โ„• - V-chkCerts : List PubKey โ†’ EndorserBlock ร— Cert โ†’ Bool - - data Input : Type where - INIT : (EndorserBlock ร— Cert โ†’ Bool) โ†’ Input - SUBMIT : RankingBlock โ†’ Input - FTCH-LDG : Input - - data Output : Type where - STAKE : StakeDistr โ†’ Output - EMPTY : Output - BASE-LDG : List RankingBlock โ†’ Output - - record Functionality : Typeโ‚ where - field State : Type - _-โŸฆ_/_โŸงโ‡€_ : State โ†’ Input โ†’ Output โ†’ State โ†’ Type - SUBMIT-total : โˆ€ {s b} โ†’ โˆƒ[ s' ] s -โŸฆ SUBMIT b / EMPTY โŸงโ‡€ s' - - open Input public - open Output public diff --git a/formal-spec/Leios/Blocks.agda b/formal-spec/Leios/Blocks.agda deleted file mode 100644 index 29a211622..000000000 --- a/formal-spec/Leios/Blocks.agda +++ /dev/null @@ -1,210 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude -open import Leios.Abstract -open import Leios.FFD - -module Leios.Blocks (a : LeiosAbstract) (let open LeiosAbstract a) where - --- IsBlock typeclass (could do a closed-world approach instead) --- Q: should votes have an instance of this class? -record IsBlock (B : Type) : Type where - field slotNumber : B โ†’ โ„• - producerID : B โ†’ PoolID - lotteryPf : B โ†’ VrfPf - - infix 4 _โˆˆแดฎ_ - - _โˆˆแดฎ_ : B โ†’ โ„™ โ„• โ†’ Type - b โˆˆแดฎ X = slotNumber b โˆˆ X - -open IsBlock โฆƒ...โฆ„ public - -OSig : Bool โ†’ Type -OSig true = Sig -OSig false = โŠค - -IBRef = Hash -EBRef = Hash - --------------------------------------------------------------------------------- --- Input Blocks --------------------------------------------------------------------------------- - -record IBHeaderOSig (b : Bool) : Type where - field slotNumber : โ„• - producerID : PoolID - lotteryPf : VrfPf - bodyHash : Hash - signature : OSig b - -IBHeader = IBHeaderOSig true -PreIBHeader = IBHeaderOSig false - -record IBBody : Type where - field txs : List Tx - -record InputBlock : Type where - field header : IBHeader - body : IBBody - - open IBHeaderOSig header public - -instance - IsBlock-IBHeaderOSig : โˆ€ {b} โ†’ IsBlock (IBHeaderOSig b) - IsBlock-IBHeaderOSig = record { IBHeaderOSig } - - Hashable-IBBody : Hashable IBBody Hash - Hashable-IBBody .hash b = hash (b .IBBody.txs) - - IsBlock-InputBlock : IsBlock InputBlock - IsBlock-InputBlock = record { InputBlock } - -mkIBHeader : โฆƒ Hashable PreIBHeader Hash โฆ„ โ†’ โ„• โ†’ PoolID โ†’ VrfPf โ†’ PrivKey โ†’ List Tx โ†’ IBHeader -mkIBHeader slot id ฯ€ pKey txs = record { signature = sign pKey (hash h) ; IBHeaderOSig h } - where - h : IBHeaderOSig false - h = record { slotNumber = slot - ; producerID = id - ; lotteryPf = ฯ€ - ; bodyHash = hash txs - ; signature = _ - } - -getIBRef : โฆƒ Hashable IBHeader Hash โฆ„ โ†’ InputBlock โ†’ IBRef -getIBRef = hash โˆ˜ InputBlock.header - --- TODO -record ibHeaderValid (h : IBHeader) : Type where -record ibBodyValid (b : IBBody) : Type where - -ibHeaderValid? : (h : IBHeader) โ†’ Dec (ibHeaderValid h) -ibHeaderValid? _ = yes record {} - -ibBodyValid? : (b : IBBody) โ†’ Dec (ibBodyValid b) -ibBodyValid? _ = yes record {} - -ibValid : InputBlock โ†’ Type -ibValid record { header = h ; body = b } = ibHeaderValid h ร— ibBodyValid b - -ibValid? : (ib : InputBlock) โ†’ Dec (ibValid ib) -ibValid? record { header = h ; body = b } = ibHeaderValid? h ร—-dec ibBodyValid? b - --------------------------------------------------------------------------------- --- Endorser Blocks --------------------------------------------------------------------------------- - -record EndorserBlockOSig (b : Bool) : Type where - field slotNumber : โ„• - producerID : PoolID - lotteryPf : VrfPf - ibRefs : List IBRef - ebRefs : List EBRef - signature : OSig b - -EndorserBlock = EndorserBlockOSig true -PreEndorserBlock = EndorserBlockOSig false - -instance - Hashable-EndorserBlock : โฆƒ Hashable PreEndorserBlock Hash โฆ„ โ†’ Hashable EndorserBlock Hash - Hashable-EndorserBlock .hash b = hash {T = PreEndorserBlock} - record { EndorserBlockOSig b hiding (signature) ; signature = _ } - - IsBlock-EndorserBlockOSig : โˆ€ {b} โ†’ IsBlock (EndorserBlockOSig b) - IsBlock-EndorserBlockOSig {b} = record { EndorserBlockOSig } - -mkEB : โฆƒ Hashable PreEndorserBlock Hash โฆ„ โ†’ โ„• โ†’ PoolID โ†’ VrfPf โ†’ PrivKey โ†’ List IBRef โ†’ List EBRef โ†’ EndorserBlock -mkEB slot id ฯ€ pKey LI LE = record { signature = sign pKey (hash b) ; EndorserBlockOSig b } - where - b : PreEndorserBlock - b = record { slotNumber = slot - ; producerID = id - ; lotteryPf = ฯ€ - ; ibRefs = LI - ; ebRefs = LE - ; signature = _ - } - -getEBRef : โฆƒ Hashable PreEndorserBlock Hash โฆ„ โ†’ EndorserBlock โ†’ EBRef -getEBRef = hash - --- TODO -record ebValid (eb : EndorserBlock) : Type where --- field lotteryPfValid : {!!} --- signatureValid : {!!} --- ibRefsValid : {!!} --- ebRefsValid : {!!} - -ebValid? : (eb : EndorserBlock) โ†’ Dec (ebValid eb) -ebValid? _ = yes record {} - --------------------------------------------------------------------------------- --- Votes --------------------------------------------------------------------------------- - --- TODO -record vsValid (vs : List Vote) : Type where - -vsValid? : (vs : List Vote) โ†’ Dec (vsValid vs) -vsValid? _ = yes record {} - --------------------------------------------------------------------------------- --- FFD for Leios Blocks --------------------------------------------------------------------------------- - -module GenFFD โฆƒ _ : IsBlock (List Vote) โฆ„ where - data Header : Type where - ibHeader : IBHeader โ†’ Header - ebHeader : EndorserBlock โ†’ Header - vHeader : List Vote โ†’ Header - - data Body : Type where - ibBody : IBBody โ†’ Body - - ID : Type - ID = โ„• ร— PoolID - - matchIB : IBHeader โ†’ IBBody โ†’ Type - matchIB h b = bodyHash โ‰ก hash b - where open IBHeaderOSig h; open IBBody b - - matchIB? : โˆ€ (h : IBHeader) โ†’ (b : IBBody) โ†’ Dec (matchIB h b) - matchIB? h b = bodyHash โ‰Ÿ hash b - where open IBHeaderOSig h; open IBBody b - - match : Header โ†’ Body โ†’ Type - match (ibHeader h) (ibBody b) = matchIB h b - match _ _ = โŠฅ - - headerValid : Header โ†’ Type - headerValid (ibHeader h) = ibHeaderValid h - headerValid (ebHeader h) = ebValid h - headerValid (vHeader h) = vsValid h - - headerValid? : (h : Header) โ†’ Dec (headerValid h) - headerValid? (ibHeader h) = ibHeaderValid? h - headerValid? (ebHeader h) = ebValid? h - headerValid? (vHeader h) = vsValid? h - - bodyValid : Body โ†’ Type - bodyValid (ibBody b) = ibBodyValid b - - bodyValid? : (b : Body) โ†’ Dec (bodyValid b) - bodyValid? (ibBody b) = ibBodyValid? b - - isValid : Header โŠŽ Body โ†’ Type - isValid (injโ‚ h) = headerValid h - isValid (injโ‚‚ b) = bodyValid b - - isValid? : โˆ€ (x : Header โŠŽ Body) โ†’ Dec (isValid x) - isValid? (injโ‚ h) = headerValid? h - isValid? (injโ‚‚ b) = bodyValid? b - - -- can we express uniqueness wrt pipelines as a property? - msgID : Header โ†’ ID - msgID (ibHeader h) = (slotNumber h , producerID h) - msgID (ebHeader h) = (slotNumber h , producerID h) -- NOTE: this isn't in the paper - msgID (vHeader h) = (slotNumber h , producerID h) -- NOTE: this isn't in the paper - -ffdAbstract : โฆƒ _ : IsBlock (List Vote) โฆ„ โ†’ FFDAbstract -ffdAbstract = record { GenFFD } diff --git a/formal-spec/Leios/FFD.agda b/formal-spec/Leios/FFD.agda deleted file mode 100644 index 027adaa00..000000000 --- a/formal-spec/Leios/FFD.agda +++ /dev/null @@ -1,27 +0,0 @@ -{-# OPTIONS --safe #-} - -module Leios.FFD where - -open import Leios.Prelude - -record FFDAbstract : Typeโ‚ where - field Header Body ID : Type - match : Header โ†’ Body โ†’ Type - msgID : Header โ†’ ID - - data Input : Type where - Send : Header โ†’ Maybe Body โ†’ Input - Fetch : Input - - data Output : Type where - SendRes : Output - FetchRes : List (Header โŠŽ Body) โ†’ Output - - record Functionality : Typeโ‚ where - field State : Type - initFFDState : State - _-โŸฆ_/_โŸงโ‡€_ : State โ†’ Input โ†’ Output โ†’ State โ†’ Type - FFD-total : โˆ€ {ffds i o} โ†’ โˆƒ[ ffds' ] ffds -โŸฆ i / o โŸงโ‡€ ffds' - - open Input public - open Output public diff --git a/formal-spec/Leios/KeyRegistration.agda b/formal-spec/Leios/KeyRegistration.agda deleted file mode 100644 index 105e336c5..000000000 --- a/formal-spec/Leios/KeyRegistration.agda +++ /dev/null @@ -1,23 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude -open import Leios.Abstract -open import Leios.VRF - -module Leios.KeyRegistration (a : LeiosAbstract) (open LeiosAbstract a) - (vrf : LeiosVRF a) (let open LeiosVRF vrf) where - -record KeyRegistrationAbstract : Typeโ‚ where - - data Input : Typeโ‚ where - INIT : PubKey โ†’ PubKey โ†’ PubKey โ†’ Input - - data Output : Type where - PUBKEYS : List PubKey โ†’ Output - - record Functionality : Typeโ‚ where - field State : Type - _-โŸฆ_/_โŸงโ‡€_ : State โ†’ Input โ†’ Output โ†’ State โ†’ Type - - open Input public - open Output public diff --git a/formal-spec/Leios/Network.agda b/formal-spec/Leios/Network.agda deleted file mode 100644 index c94fc6163..000000000 --- a/formal-spec/Leios/Network.agda +++ /dev/null @@ -1,72 +0,0 @@ -module Leios.Network where - -open import abstract-set-theory.Prelude hiding (_โˆ˜_; _โŠ—_) -open import abstract-set-theory.FiniteSetTheory using (โ„™_; _โˆˆ_; _โˆช_; โด_โต; _โˆ‰_) - -open import CategoricalCrypto - -record Abstract : Setโ‚ where - field Header Body ID : Set - match : Header โ†’ Body โ†’ Set - msgID : Header โ†’ ID - -module Broadcast (M Peer : Set) where - open Channel - - C : Channel - C .P = Peer - C .rcvType _ = Peer ร— M - C .sndType _ = M - - postulate Functionality : Machine I C - - Single : Channel - Single .P = โŠค - Single .rcvType _ = Peer ร— M - Single .sndType _ = M - - postulate SingleFunctionality : Machine I Single - - -- connectWithBroadcast : โˆ€ {A} โ†’ (Peer โ†’ Machine Single A) โ†’ Machine I A - -- connectWithBroadcast = {!!} - -module HeaderDiffusion (a : Abstract) (Peer : Set) (self : Peer) where - open Channel - open Abstract a - module B = Broadcast Header Peer - - data Port : Set where - Send : Port -- we want to send a header - Forward : Port -- we want to forward a header - - C : Channel - C .P = Port - C .sndType _ = Header - C .rcvType Forward = Header - C .rcvType Send = โŠฅ - - data Input : Set where - S : Header โ†’ Input - F : Header โ†’ Input - R : Peer โ†’ Header โ†’ Input - - data Output : Set where - Verify : Header โ†’ Output - - private variable - h : Header - s : โ„™ ID - - data Step : โˆƒ (rcvType (B.Single โŠ— C แต€)) โ†’ โ„™ ID โ†’ โ„™ ID ร— Maybe (โˆƒ (sndType (B.Single โŠ— C แต€))) โ†’ Set where - Init : Step (injโ‚‚ Send , h) s (s โˆช โด msgID h โต , just (injโ‚ _ , h)) - Receive1 : โˆ€ {p} โ†’ Step (injโ‚ _ , p , h) s (s , just (injโ‚‚ Forward , h)) - Receive2 : msgID h โˆ‰ s โ†’ Step (injโ‚‚ Forward , h) s (s โˆช โด msgID h โต , just (injโ‚ _ , h)) - Receive2' : msgID h โˆˆ s โ†’ Step (injโ‚‚ Forward , h) s (s , nothing) - - step : โˆƒ (rcvType (B.Single โŠ— C แต€)) โ†’ โˆƒ (sndType (B.Single โŠ— C แต€)) - step (injโ‚ _ , _ , h) = (injโ‚‚ Forward , h) - step (injโ‚‚ Forward , h) = (injโ‚ _ , h) - step (injโ‚‚ Send , h) = (injโ‚ _ , h) - - Functionality : Machine I C - Functionality = MkMachine' Step โˆ˜ B.SingleFunctionality diff --git a/formal-spec/Leios/Prelude.agda b/formal-spec/Leios/Prelude.agda deleted file mode 100644 index 7c56b2611..000000000 --- a/formal-spec/Leios/Prelude.agda +++ /dev/null @@ -1,45 +0,0 @@ -{-# OPTIONS --safe #-} - -module Leios.Prelude where - -open import abstract-set-theory.FiniteSetTheory public -open import abstract-set-theory.Prelude public -open import Data.List using (upTo) - -open import Class.HasAdd public -open import Class.HasOrder public -open import Class.Hashable public -open import Prelude.InferenceRules public - -module T where - open import Data.These public -open T public using (These; this; that) - -module L where - open import Data.List public -open L public using (List; []; _โˆท_; _++_; catMaybes; head; length; sum; and; or; any) - -module A where - open import Data.List.Relation.Unary.Any public -open A public using (here; there) - -fromTo : โ„• โ†’ โ„• โ†’ List โ„• -fromTo m n = map (_+ m) (upTo (n โˆธ m)) - -slice : (L : โ„•) โ†’ โฆƒ NonZero L โฆ„ โ†’ โ„• โ†’ โ„• โ†’ โ„™ โ„• -slice L s x = fromList (fromTo s' (s' + (L โˆธ 1))) - where s' = ((s / L) โˆธ x) * L -- equivalent to the formula in the paper - -filter : {A : Set} โ†’ (P : A โ†’ Type) โฆƒ _ : P โ‡ยน โฆ„ โ†’ List A โ†’ List A -filter P = L.filter ยฟ P ยฟยน - -instance - IsSet-List : {A : Set} โ†’ IsSet (List A) A - IsSet-List .toSet A = fromList A - -open import Data.List.Relation.Unary.Any -open Properties - -finiteโ‡’Aโ‰กโˆ…โŠŽโˆƒaโˆˆA : {X : Type} โ†’ {A : โ„™ X} โ†’ finite A โ†’ (A โ‰กแต‰ โˆ…) โŠŽ ฮฃ[ a โˆˆ X ] a โˆˆ A -finiteโ‡’Aโ‰กโˆ…โŠŽโˆƒaโˆˆA ([] , h) = injโ‚ (โˆ…-least (ฮป aโˆˆA โ†’ โŠฅ-elim (case Equivalence.to h aโˆˆA of ฮป ()))) -finiteโ‡’Aโ‰กโˆ…โŠŽโˆƒaโˆˆA (x โˆท _ , h) = injโ‚‚ (x , Equivalence.from h (here refl)) diff --git a/formal-spec/Leios/Protocol.agda b/formal-spec/Leios/Protocol.agda deleted file mode 100644 index 9e40070e2..000000000 --- a/formal-spec/Leios/Protocol.agda +++ /dev/null @@ -1,152 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude hiding (id) -open import Leios.FFD -open import Leios.SpecStructure - -module Leios.Protocol {n} (โ‹ฏ : SpecStructure n) (let open SpecStructure โ‹ฏ) (SlotUpkeep : Type) where - -open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot) -open GenFFD - --- High level structure: - - --- (simple) Leios --- / | --- +-------------------------------------+ | --- | Header Diffusion Body Diffusion | | --- +-------------------------------------+ Base Protocol --- \ / --- Network - -data LeiosInput : Type where - INIT : VTy โ†’ LeiosInput - SUBMIT : EndorserBlock โŠŽ List Tx โ†’ LeiosInput - SLOT : LeiosInput - FTCH-LDG : LeiosInput - -data LeiosOutput : Type where - FTCH-LDG : List Tx โ†’ LeiosOutput - EMPTY : LeiosOutput - -record LeiosState : Type where - field V : VTy - SD : StakeDistr - FFDState : FFD.State - Ledger : List Tx - ToPropose : List Tx - IBs : List InputBlock - EBs : List EndorserBlock - Vs : List (List Vote) - slot : โ„• - IBHeaders : List IBHeader - IBBodies : List IBBody - Upkeep : โ„™ SlotUpkeep - BaseState : B.State - votingState : VotingState - - lookupEB : EBRef โ†’ Maybe EndorserBlock - lookupEB r = find (ฮป b โ†’ getEBRef b โ‰Ÿ r) EBs - - lookupIB : IBRef โ†’ Maybe InputBlock - lookupIB r = find (ฮป b โ†’ getIBRef b โ‰Ÿ r) IBs - - lookupTxs : EndorserBlock โ†’ List Tx - lookupTxs eb = do - ebโ€ฒ โ† mapMaybe lookupEB $ ebRefs eb - ib โ† mapMaybe lookupIB $ ibRefs ebโ€ฒ - txs $ body ib - where open EndorserBlockOSig - open IBBody - open InputBlock - - constructLedger : List RankingBlock โ†’ List Tx - constructLedger = L.concat โˆ˜ L.map (T.mergeThese L._++_ โˆ˜ T.mapโ‚ lookupTxs) - - needsUpkeep : SlotUpkeep โ†’ Set - needsUpkeep = _โˆ‰ Upkeep - -addUpkeep : LeiosState โ†’ SlotUpkeep โ†’ LeiosState -addUpkeep s u = let open LeiosState s in record s { Upkeep = Upkeep โˆช โด u โต } -{-# INJECTIVE_FOR_INFERENCE addUpkeep #-} - -initLeiosState : VTy โ†’ StakeDistr โ†’ B.State โ†’ LeiosState -initLeiosState V SD bs = record - { V = V - ; SD = SD - ; FFDState = FFD.initFFDState - ; Ledger = [] - ; ToPropose = [] - ; IBs = [] - ; EBs = [] - ; Vs = [] - ; slot = initSlot V - ; IBHeaders = [] - ; IBBodies = [] - ; Upkeep = โˆ… - ; BaseState = bs - ; votingState = initVotingState - } - --- some predicates about EBs -module _ (s : LeiosState) (eb : EndorserBlock) where - open EndorserBlockOSig eb - open LeiosState s - - allIBRefsKnown : Type - allIBRefsKnown = โˆ€[ ref โˆˆ fromList ibRefs ] ref โˆˆหก map getIBRef IBs - -stake : LeiosState โ†’ โ„• -stake record { SD = SD } = TotalMap.lookup SD id - -module _ (s : LeiosState) where - - open LeiosState s - - upd : Header โŠŽ Body โ†’ LeiosState - upd (injโ‚ (ebHeader eb)) = record s { EBs = eb โˆท EBs } - upd (injโ‚ (vHeader vs)) = record s { Vs = vs โˆท Vs } - upd (injโ‚ (ibHeader h)) with A.any? (matchIB? h) IBBodies - ... | yes p = - record s - { IBs = record { header = h ; body = A.lookup p } โˆท IBs - ; IBBodies = IBBodies A.โ”€ p - } - ... | no _ = - record s - { IBHeaders = h โˆท IBHeaders - } - upd (injโ‚‚ (ibBody b)) with A.any? (flip matchIB? b) IBHeaders - ... | yes p = - record s - { IBs = record { header = A.lookup p ; body = b } โˆท IBs - ; IBHeaders = IBHeaders A.โ”€ p - } - ... | no _ = - record s - { IBBodies = b โˆท IBBodies - } - -module _ {s s'} where - open LeiosState s' - - upd-preserves-Upkeep : โˆ€ {x} โ†’ LeiosState.Upkeep s โ‰ก LeiosState.Upkeep s' - โ†’ LeiosState.Upkeep s โ‰ก LeiosState.Upkeep (upd s' x) - upd-preserves-Upkeep {injโ‚ (ibHeader x)} refl with A.any? (matchIB? x) IBBodies - ... | yes p = refl - ... | no ยฌp = refl - upd-preserves-Upkeep {injโ‚ (ebHeader x)} refl = refl - upd-preserves-Upkeep {injโ‚ (vHeader x)} refl = refl - upd-preserves-Upkeep {injโ‚‚ (ibBody x)} refl with A.any? (flip matchIB? x) IBHeaders - ... | yes p = refl - ... | no ยฌp = refl - -infix 25 _โ†‘_ -_โ†‘_ : LeiosState โ†’ List (Header โŠŽ Body) โ†’ LeiosState -_โ†‘_ = foldr (flip upd) - -โ†‘-preserves-Upkeep : โˆ€ {s x} โ†’ LeiosState.Upkeep s โ‰ก LeiosState.Upkeep (s โ†‘ x) -โ†‘-preserves-Upkeep {x = []} = refl -โ†‘-preserves-Upkeep {s = s} {x = x โˆท xโ‚} = - upd-preserves-Upkeep {s = s} {x = x} (โ†‘-preserves-Upkeep {x = xโ‚}) diff --git a/formal-spec/Leios/Short.lagda.md b/formal-spec/Leios/Short.lagda.md deleted file mode 100644 index a3daf80b9..000000000 --- a/formal-spec/Leios/Short.lagda.md +++ /dev/null @@ -1,182 +0,0 @@ -## Short-Pipeline Leios - -```agda -open import Leios.Prelude hiding (id) -open import Leios.FFD -open import Leios.SpecStructure -open import Data.Fin.Patterns - -open import Tactic.Defaults -open import Tactic.Derive.DecEq -``` -Uniform Short Pipeline: - -1. If elected, propose IB -2. Wait -3. Wait -4. If elected, propose EB -5. If elected, vote - If elected, propose RB -```agda -module Leios.Short (โ‹ฏ : SpecStructure 1) - (let open SpecStructure โ‹ฏ renaming (isVoteCertified to isVoteCertified')) where -``` -```agda -data SlotUpkeep : Type where - Base IB-Role EB-Role V-Role : SlotUpkeep - -unquoteDecl DecEq-SlotUpkeep = derive-DecEq ((quote SlotUpkeep , DecEq-SlotUpkeep) โˆท []) - -allUpkeep : โ„™ SlotUpkeep -allUpkeep = (((โˆ… โˆช โด IB-Role โต) โˆช โด EB-Role โต) โˆช โด V-Role โต) โˆช โด Base โต -``` -```agda -open import Leios.Protocol (โ‹ฏ) SlotUpkeep public -open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot) -open FFD hiding (_-โŸฆ_/_โŸงโ‡€_) -open GenFFD - -isVoteCertified : LeiosState โ†’ EndorserBlock โ†’ Type -isVoteCertified s eb = isVoteCertified' (LeiosState.votingState s) (0F , eb) -``` -```agda -private variable s s' : LeiosState - ffds' : FFD.State - ฯ€ : VrfPf - bs' : B.State - ks ks' : K.State - msgs : List (FFDAbstract.Header ffdAbstract โŠŽ FFDAbstract.Body ffdAbstract) - eb : EndorserBlock - rbs : List RankingBlock - txs : List Tx - V : VTy - SD : StakeDistr - pks : List PubKey -``` -```agda -data _โ†_ : LeiosState โ†’ LeiosState โ†’ Type where -``` -#### Block/Vote production rules -```agda - IB-Role : let open LeiosState s renaming (FFDState to ffds) - b = ibBody (record { txs = ToPropose }) - h = ibHeader (mkIBHeader slot id ฯ€ sk-IB ToPropose) - in - โˆ™ needsUpkeep IB-Role - โˆ™ canProduceIB slot sk-IB (stake s) ฯ€ - โˆ™ ffds FFD.-โŸฆ Send h (just b) / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep record s { FFDState = ffds' } IB-Role -``` -```agda - EB-Role : let open LeiosState s renaming (FFDState to ffds) - LI = map getIBRef $ filter (_โˆˆแดฎ slice L slot 3) IBs - h = mkEB slot id ฯ€ sk-EB LI [] - in - โˆ™ needsUpkeep EB-Role - โˆ™ canProduceEB slot sk-EB (stake s) ฯ€ - โˆ™ ffds FFD.-โŸฆ Send (ebHeader h) nothing / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep record s { FFDState = ffds' } EB-Role -``` -```agda - V-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_โˆˆแดฎ slice L slot 1) EBs - votes = map (vote sk-V โˆ˜ hash) EBs' - in - โˆ™ needsUpkeep V-Role - โˆ™ canProduceV slot sk-V (stake s) - โˆ™ ffds FFD.-โŸฆ Send (vHeader votes) nothing / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep record s { FFDState = ffds' } V-Role -``` -#### Negative Block/Vote production rules -```agda - No-IB-Role : let open LeiosState s in - โˆ™ needsUpkeep IB-Role - โˆ™ (โˆ€ ฯ€ โ†’ ยฌ canProduceIB slot sk-IB (stake s) ฯ€) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep s IB-Role -``` -```agda - No-EB-Role : let open LeiosState s in - โˆ™ needsUpkeep EB-Role - โˆ™ (โˆ€ ฯ€ โ†’ ยฌ canProduceEB slot sk-EB (stake s) ฯ€) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep s EB-Role -``` -```agda - No-V-Role : let open LeiosState s in - โˆ™ needsUpkeep V-Role - โˆ™ ยฌ canProduceV slot sk-V (stake s) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep s V-Role -``` -### Uniform short-pipeline -```agda -data _-โŸฆ_/_โŸงโ‡€_ : Maybe LeiosState โ†’ LeiosInput โ†’ LeiosOutput โ†’ LeiosState โ†’ Type where -``` -#### Initialization -```agda - Init : - โˆ™ ks K.-โŸฆ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks โŸงโ‡€ ks' - โˆ™ initBaseState B.-โŸฆ B.INIT (V-chkCerts pks) / B.STAKE SD โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - nothing -โŸฆ INIT V / EMPTY โŸงโ‡€ initLeiosState V SD bs' -``` -#### Network and Ledger -```agda - Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) in - โˆ™ Upkeep โ‰กแต‰ allUpkeep - โˆ™ bs B.-โŸฆ B.FTCH-LDG / B.BASE-LDG rbs โŸงโ‡€ bs' - โˆ™ ffds FFD.-โŸฆ Fetch / FetchRes msgs โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ record s - { FFDState = ffds' - ; BaseState = bs' - ; Ledger = constructLedger rbs - ; slot = suc slot - ; Upkeep = โˆ… - } โ†‘ L.filter isValid? msgs -``` -```agda - Ftch : - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ FTCH-LDG / FTCH-LDG (LeiosState.Ledger s) โŸงโ‡€ s -``` -#### Base chain - -Note: Submitted data to the base chain is only taken into account - if the party submitting is the block producer on the base chain - for the given slot -```agda - Baseโ‚ : - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SUBMIT (injโ‚‚ txs) / EMPTY โŸงโ‡€ record s { ToPropose = txs } -``` -```agda - Baseโ‚‚a : let open LeiosState s renaming (BaseState to bs) in - โˆ™ needsUpkeep Base - โˆ™ eb โˆˆ filter (ฮป eb โ†’ isVoteCertified s eb ร— eb โˆˆแดฎ slice L slot 2) EBs - โˆ™ bs B.-โŸฆ B.SUBMIT (this eb) / B.EMPTY โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ addUpkeep record s { BaseState = bs' } Base - - Baseโ‚‚b : let open LeiosState s renaming (BaseState to bs) in - โˆ™ needsUpkeep Base - โˆ™ [] โ‰ก filter (ฮป eb โ†’ isVoteCertified s eb ร— eb โˆˆแดฎ slice L slot 2) EBs - โˆ™ bs B.-โŸฆ B.SUBMIT (that ToPropose) / B.EMPTY โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ addUpkeep record s { BaseState = bs' } Base -``` -#### Protocol rules -```agda - Roles : - โˆ™ s โ† s' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ s' -``` diff --git a/formal-spec/Leios/Simplified.agda b/formal-spec/Leios/Simplified.agda deleted file mode 100644 index d5c38ac76..000000000 --- a/formal-spec/Leios/Simplified.agda +++ /dev/null @@ -1,184 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude hiding (id) -open import Leios.FFD -open import Leios.SpecStructure -open import Data.Fin.Patterns - -open import Tactic.Defaults -open import Tactic.Derive.DecEq - -module Leios.Simplified (โ‹ฏ : SpecStructure 2) (let open SpecStructure โ‹ฏ) (ฮ› ฮผ : โ„•) where - -data SlotUpkeep : Type where - Base IB-Role EB-Role V1-Role V2-Role : SlotUpkeep - -unquoteDecl DecEq-SlotUpkeep = derive-DecEq ((quote SlotUpkeep , DecEq-SlotUpkeep) โˆท []) - -allUpkeep : โ„™ SlotUpkeep -allUpkeep = fromList (Base โˆท IB-Role โˆท EB-Role โˆท V1-Role โˆท V2-Role โˆท []) - -open import Leios.Protocol (โ‹ฏ) SlotUpkeep public - -open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot) -open FFD hiding (_-โŸฆ_/_โŸงโ‡€_) -open GenFFD - -isVote1Certified : LeiosState โ†’ EndorserBlock โ†’ Type -isVote1Certified s eb = isVoteCertified (LeiosState.votingState s) (0F , eb) - -isVote2Certified : LeiosState โ†’ EndorserBlock โ†’ Type -isVote2Certified s eb = isVoteCertified (LeiosState.votingState s) (1F , eb) - --- Predicates about EBs -module _ (s : LeiosState) (eb : EndorserBlock) where - open EndorserBlockOSig eb - open LeiosState s - - vote2Eligible : Type - vote2Eligible = length ebRefs โ‰ฅ lengthหข candidateEBs / 2 -- should this be `>`? - ร— fromList ebRefs โŠ† candidateEBs - where candidateEBs : โ„™ Hash - candidateEBs = mapหข getEBRef $ filterหข (_โˆˆแดฎ slice L slot (ฮผ + 3)) (fromList EBs) - -private variable s s' : LeiosState - ffds' : FFD.State - ฯ€ : VrfPf - bs' : B.State - ks ks' : K.State - msgs : List (FFDAbstract.Header ffdAbstract โŠŽ FFDAbstract.Body ffdAbstract) - eb : EndorserBlock - rbs : List RankingBlock - txs : List Tx - V : VTy - SD : StakeDistr - pks : List PubKey - -data _โ†_ : LeiosState โ†’ LeiosState โ†’ Type where - - IB-Role : let open LeiosState s renaming (FFDState to ffds) - b = ibBody (record { txs = ToPropose }) - h = ibHeader (mkIBHeader slot id ฯ€ sk-IB ToPropose) - in - โˆ™ needsUpkeep IB-Role - โˆ™ canProduceIB slot sk-IB (stake s) ฯ€ - โˆ™ ffds FFD.-โŸฆ Send h (just b) / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep record s { FFDState = ffds' } IB-Role - - EB-Role : let open LeiosState s renaming (FFDState to ffds) - LI = map getIBRef $ filter (_โˆˆแดฎ slice L slot (ฮ› + 1)) IBs - LE = map getEBRef $ filter (isVote1Certified s) $ - filter (_โˆˆแดฎ slice L slot (ฮผ + 2)) EBs - h = mkEB slot id ฯ€ sk-EB LI LE - in - โˆ™ needsUpkeep EB-Role - โˆ™ canProduceEB slot sk-EB (stake s) ฯ€ - โˆ™ ffds FFD.-โŸฆ Send (ebHeader h) nothing / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep record s { FFDState = ffds' } EB-Role - - V1-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_โˆˆแดฎ slice L slot (ฮผ + 1)) EBs - votes = map (vote sk-V โˆ˜ hash) EBs' - in - โˆ™ needsUpkeep V1-Role - โˆ™ canProduceV1 slot sk-V (stake s) - โˆ™ ffds FFD.-โŸฆ Send (vHeader votes) nothing / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep record s { FFDState = ffds' } V1-Role - - V2-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (vote2Eligible s) $ filter (_โˆˆแดฎ slice L slot 1) EBs - votes = map (vote sk-V โˆ˜ hash) EBs' - in - โˆ™ needsUpkeep V2-Role - โˆ™ canProduceV2 slot sk-V (stake s) - โˆ™ ffds FFD.-โŸฆ Send (vHeader votes) nothing / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep record s { FFDState = ffds' } V2-Role - - -- Note: Base doesn't need a negative rule, since it can always be invoked - - No-IB-Role : let open LeiosState s in - โˆ™ needsUpkeep IB-Role - โˆ™ (โˆ€ ฯ€ โ†’ ยฌ canProduceIB slot sk-IB (stake s) ฯ€) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep s IB-Role - - No-EB-Role : let open LeiosState s in - โˆ™ needsUpkeep EB-Role - โˆ™ (โˆ€ ฯ€ โ†’ ยฌ canProduceEB slot sk-EB (stake s) ฯ€) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep s EB-Role - - No-V1-Role : let open LeiosState s in - โˆ™ needsUpkeep V1-Role - โˆ™ ยฌ canProduceV1 slot sk-V (stake s) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep s V1-Role - - No-V2-Role : let open LeiosState s in - โˆ™ needsUpkeep V2-Role - โˆ™ ยฌ canProduceV2 slot sk-V (stake s) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep s V2-Role - -data _-โŸฆ_/_โŸงโ‡€_ : Maybe LeiosState โ†’ LeiosInput โ†’ LeiosOutput โ†’ LeiosState โ†’ Type where - - -- Initialization - - Init : - โˆ™ ks K.-โŸฆ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks โŸงโ‡€ ks' - โˆ™ initBaseState B.-โŸฆ B.INIT (V-chkCerts pks) / B.STAKE SD โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - nothing -โŸฆ INIT V / EMPTY โŸงโ‡€ initLeiosState V SD bs' - - -- Network and Ledger - - Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) in - โˆ™ Upkeep โ‰กแต‰ allUpkeep - โˆ™ bs B.-โŸฆ B.FTCH-LDG / B.BASE-LDG rbs โŸงโ‡€ bs' - โˆ™ ffds FFD.-โŸฆ Fetch / FetchRes msgs โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ record s - { FFDState = ffds' - ; Ledger = constructLedger rbs - ; slot = suc slot - ; Upkeep = โˆ… - ; BaseState = bs' - } โ†‘ L.filter isValid? msgs - - Ftch : - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ FTCH-LDG / FTCH-LDG (LeiosState.Ledger s) โŸงโ‡€ s - - -- Base chain - -- - -- Note: Submitted data to the base chain is only taken into account - -- if the party submitting is the block producer on the base chain - -- for the given slot - - Baseโ‚ : - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SUBMIT (injโ‚‚ txs) / EMPTY โŸงโ‡€ record s { ToPropose = txs } - - Baseโ‚‚a : let open LeiosState s renaming (BaseState to bs) in - โˆ™ needsUpkeep Base - โˆ™ eb โˆˆ filter (ฮป eb โ†’ isVote2Certified s eb ร— eb โˆˆแดฎ slice L slot 2) EBs - โˆ™ bs B.-โŸฆ B.SUBMIT (this eb) / B.EMPTY โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ addUpkeep record s { BaseState = bs' } Base - - Baseโ‚‚b : let open LeiosState s renaming (BaseState to bs) in - โˆ™ needsUpkeep Base - โˆ™ [] โ‰ก filter (ฮป eb โ†’ isVote2Certified s eb ร— eb โˆˆแดฎ slice L slot 2) EBs - โˆ™ bs B.-โŸฆ B.SUBMIT (that ToPropose) / B.EMPTY โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ addUpkeep record s { BaseState = bs' } Base - - -- Protocol rules - - Roles : โˆ™ s โ† s' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ s' diff --git a/formal-spec/Leios/Simplified/Deterministic.agda b/formal-spec/Leios/Simplified/Deterministic.agda deleted file mode 100644 index ce06ef832..000000000 --- a/formal-spec/Leios/Simplified/Deterministic.agda +++ /dev/null @@ -1,357 +0,0 @@ ---{-# OPTIONS --safe #-} -{-# OPTIONS --allow-unsolved-metas #-} - --------------------------------------------------------------------------------- --- Deterministic variant of simple Leios --------------------------------------------------------------------------------- - -open import Leios.Prelude hiding (id) -open import Prelude.Init using (โˆƒโ‚‚-syntax) -open import Leios.FFD - -import Data.List as L -open import Data.List.Relation.Unary.Any using (here) - -open import Leios.SpecStructure - -module Leios.Simplified.Deterministic (โ‹ฏ : SpecStructure 2) (let open SpecStructure โ‹ฏ) (ฮ› ฮผ : โ„•) where - -import Leios.Simplified -open import Leios.Simplified โ‹ฏ ฮ› ฮผ hiding (_-โŸฆ_/_โŸงโ‡€_) -module ND = Leios.Simplified โ‹ฏ ฮ› ฮผ - -open import Class.Computational -open import Class.Computational22 -open import StateMachine - -open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot) -open GenFFD - -open FFD hiding (_-โŸฆ_/_โŸงโ‡€_) - -private variable s s' s0 s1 s2 s3 s4 s5 : LeiosState - i : LeiosInput - o : LeiosOutput - ffds' : FFD.State - ฯ€ : VrfPf - bs' : B.State - ks ks' : K.State - msgs : List (FFDAbstract.Header ffdAbstract โŠŽ FFDAbstract.Body ffdAbstract) - eb : EndorserBlock - rbs : List RankingBlock - txs : List Tx - V : VTy - SD : StakeDistr - pks : List PubKey - -lemma : โˆ€ {u} โ†’ u โˆˆ LeiosState.Upkeep (addUpkeep s u) -lemma = to โˆˆ-โˆช (injโ‚‚ (to โˆˆ-singleton refl)) - where open Equivalence - -addUpkeepโ‡’ยฌneedsUpkeep : โˆ€ {u} โ†’ ยฌ LeiosState.needsUpkeep (addUpkeep s u) u -addUpkeepโ‡’ยฌneedsUpkeep {s = s} = ฮป x โ†’ x (lemma {s = s}) - -data _โŠข_ : LeiosInput โ†’ LeiosState โ†’ Type where - Init : - โˆ™ ks K.-โŸฆ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks โŸงโ‡€ ks' - โˆ™ initBaseState B.-โŸฆ B.INIT (V-chkCerts pks) / B.STAKE SD โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - INIT V โŠข initLeiosState V SD bs' - -data _-โŸฆBaseโŸงโ‡€_ : LeiosState โ†’ LeiosState โ†’ Type where - - Baseโ‚‚a : โˆ€ {ebs} โ†’ let open LeiosState s renaming (BaseState to bs) in - โˆ™ eb โˆท ebs โ‰ก filter (ฮป eb โ†’ isVote2Certified s eb ร— eb โˆˆแดฎ slice L slot 2) EBs - โˆ™ bs B.-โŸฆ B.SUBMIT (this eb) / B.EMPTY โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆBaseโŸงโ‡€ addUpkeep record s { BaseState = bs' } Base - - Baseโ‚‚b : let open LeiosState s renaming (BaseState to bs) in - โˆ™ [] โ‰ก filter (ฮป eb โ†’ isVote2Certified s eb ร— eb โˆˆแดฎ slice L slot 2) EBs - โˆ™ bs B.-โŸฆ B.SUBMIT (that ToPropose) / B.EMPTY โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆBaseโŸงโ‡€ addUpkeep record s { BaseState = bs' } Base - -Baseโ‡’ND : LeiosState.needsUpkeep s Base โ†’ s -โŸฆBaseโŸงโ‡€ s' โ†’ just s ND.-โŸฆ SLOT / EMPTY โŸงโ‡€ s' -Baseโ‡’ND u (Baseโ‚‚a xโ‚ xโ‚‚) = Baseโ‚‚a u (subst (_ โˆˆ_) xโ‚ (Equivalence.to โˆˆ-fromList (here refl))) xโ‚‚ -Baseโ‡’ND u (Baseโ‚‚b xโ‚ xโ‚‚) = Baseโ‚‚b u xโ‚ xโ‚‚ - -Base-Upkeep : โˆ€ {u} โ†’ u โ‰ข Base โ†’ LeiosState.needsUpkeep s u โ†’ s -โŸฆBaseโŸงโ‡€ s' - โ†’ LeiosState.needsUpkeep s' u -Base-Upkeep uโ‰ขBase h (Baseโ‚‚a _ _) uโˆˆsu = case Equivalence.from โˆˆ-โˆช uโˆˆsu of ฮป where - (injโ‚ x) โ†’ h x - (injโ‚‚ y) โ†’ uโ‰ขBase (Equivalence.from โˆˆ-singleton y) -Base-Upkeep uโ‰ขBase h (Baseโ‚‚b _ _) uโˆˆsu = case Equivalence.from โˆˆ-โˆช uโˆˆsu of ฮป where - (injโ‚ x) โ†’ h x - (injโ‚‚ y) โ†’ uโ‰ขBase (Equivalence.from โˆˆ-singleton y) - -opaque - Base-total : โˆƒ[ s' ] s -โŸฆBaseโŸงโ‡€ s' - Base-total {s = s} with - (let open LeiosState s in filter (ฮป eb โ†’ isVote2Certified s eb ร— eb โˆˆแดฎ slice L slot 2) EBs) - in eq - ... | [] = -, Baseโ‚‚b (sym eq) (projโ‚‚ B.SUBMIT-total) - ... | x โˆท l = -, Baseโ‚‚a (sym eq) (projโ‚‚ B.SUBMIT-total) - - Base-total' : โฆƒ Computational-B : Computational22 B._-โŸฆ_/_โŸงโ‡€_ String โฆ„ - โ†’ โˆƒ[ bs ] s -โŸฆBaseโŸงโ‡€ addUpkeep record s { BaseState = bs } Base - Base-total' {s = s} = let open LeiosState s in - case โˆƒ[ ebs ] ebs โ‰ก filter (ฮป eb โ†’ isVote2Certified s eb ร— eb โˆˆแดฎ slice L slot 2) EBs โˆ‹ -, refl - of ฮป where - (eb โˆท _ , eq) โ†’ -, Baseโ‚‚a eq (projโ‚‚ B.SUBMIT-total) - ([] , eq) โ†’ -, Baseโ‚‚b eq (projโ‚‚ B.SUBMIT-total) - -data _-โŸฆIB-RoleโŸงโ‡€_ : LeiosState โ†’ LeiosState โ†’ Type where - - IB-Role : let open LeiosState s renaming (FFDState to ffds) - b = ibBody (record { txs = ToPropose }) - h = ibHeader (mkIBHeader slot id ฯ€ sk-IB ToPropose) - in - โˆ™ canProduceIB slot sk-IB (stake s) ฯ€ - โˆ™ ffds FFD.-โŸฆ Send h (just b) / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆIB-RoleโŸงโ‡€ addUpkeep record s { FFDState = ffds' } IB-Role - - No-IB-Role : let open LeiosState s in - โˆ™ (โˆ€ ฯ€ โ†’ ยฌ canProduceIB slot sk-IB (stake s) ฯ€) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆIB-RoleโŸงโ‡€ addUpkeep s IB-Role - -IB-Roleโ‡’ND : LeiosState.needsUpkeep s IB-Role โ†’ s -โŸฆIB-RoleโŸงโ‡€ s' โ†’ just s ND.-โŸฆ SLOT / EMPTY โŸงโ‡€ s' -IB-Roleโ‡’ND u (IB-Role xโ‚ xโ‚‚) = Roles (IB-Role u xโ‚ xโ‚‚) -IB-Roleโ‡’ND u (No-IB-Role xโ‚) = Roles (No-IB-Role u xโ‚) - -IB-Role-Upkeep : โˆ€ {u} โ†’ u โ‰ข IB-Role โ†’ LeiosState.needsUpkeep s u โ†’ s -โŸฆIB-RoleโŸงโ‡€ s' - โ†’ LeiosState.needsUpkeep s' u -IB-Role-Upkeep uโ‰ขIB-Role h (IB-Role _ _) uโˆˆsu = case Equivalence.from โˆˆ-โˆช uโˆˆsu of ฮป where - (injโ‚ x) โ†’ h x - (injโ‚‚ y) โ†’ uโ‰ขIB-Role (Equivalence.from โˆˆ-singleton y) -IB-Role-Upkeep uโ‰ขIB-Role h (No-IB-Role _) uโˆˆsu = case Equivalence.from โˆˆ-โˆช uโˆˆsu of ฮป where - (injโ‚ x) โ†’ h x - (injโ‚‚ y) โ†’ uโ‰ขIB-Role (Equivalence.from โˆˆ-singleton y) - -opaque - IB-Role-total : โˆƒ[ s' ] s -โŸฆIB-RoleโŸงโ‡€ s' - IB-Role-total {s = s} = let open LeiosState s in case Dec-canProduceIB of ฮป where - (injโ‚ (ฯ€ , pf)) โ†’ -, IB-Role pf (projโ‚‚ FFD.FFD-total) - (injโ‚‚ pf) โ†’ -, No-IB-Role pf - - IB-Role-total' : โˆƒ[ ffds ] s -โŸฆIB-RoleโŸงโ‡€ addUpkeep record s { FFDState = ffds } IB-Role - IB-Role-total' {s = s} = let open LeiosState s in case Dec-canProduceIB of ฮป where - (injโ‚ (ฯ€ , pf)) โ†’ -, IB-Role pf (projโ‚‚ FFD.FFD-total) - (injโ‚‚ pf) โ†’ -, No-IB-Role pf - -data _-โŸฆEB-RoleโŸงโ‡€_ : LeiosState โ†’ LeiosState โ†’ Type where - - EB-Role : let open LeiosState s renaming (FFDState to ffds) - LI = map getIBRef $ filter (_โˆˆแดฎ slice L slot (ฮ› + 1)) IBs - LE = map getEBRef $ filter (isVote1Certified s) $ - filter (_โˆˆแดฎ slice L slot (ฮผ + 2)) EBs - h = mkEB slot id ฯ€ sk-EB LI LE - in - โˆ™ canProduceEB slot sk-EB (stake s) ฯ€ - โˆ™ ffds FFD.-โŸฆ Send (ebHeader h) nothing / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆEB-RoleโŸงโ‡€ addUpkeep record s { FFDState = ffds' } EB-Role - - No-EB-Role : let open LeiosState s in - โˆ™ (โˆ€ ฯ€ โ†’ ยฌ canProduceEB slot sk-EB (stake s) ฯ€) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆEB-RoleโŸงโ‡€ addUpkeep s EB-Role - -EB-Roleโ‡’ND : LeiosState.needsUpkeep s EB-Role โ†’ s -โŸฆEB-RoleโŸงโ‡€ s' โ†’ just s ND.-โŸฆ SLOT / EMPTY โŸงโ‡€ s' -EB-Roleโ‡’ND u (EB-Role xโ‚ xโ‚‚) = Roles (EB-Role u xโ‚ xโ‚‚) -EB-Roleโ‡’ND u (No-EB-Role xโ‚) = Roles (No-EB-Role u xโ‚) - -EB-Role-Upkeep : โˆ€ {u} โ†’ u โ‰ข EB-Role โ†’ LeiosState.needsUpkeep s u โ†’ s -โŸฆEB-RoleโŸงโ‡€ s' - โ†’ LeiosState.needsUpkeep s' u -EB-Role-Upkeep uโ‰ขEB-Role h (EB-Role _ _) uโˆˆsu = case Equivalence.from โˆˆ-โˆช uโˆˆsu of ฮป where - (injโ‚ x) โ†’ h x - (injโ‚‚ y) โ†’ uโ‰ขEB-Role (Equivalence.from โˆˆ-singleton y) -EB-Role-Upkeep uโ‰ขEB-Role h (No-EB-Role _) uโˆˆsu = case Equivalence.from โˆˆ-โˆช uโˆˆsu of ฮป where - (injโ‚ x) โ†’ h x - (injโ‚‚ y) โ†’ uโ‰ขEB-Role (Equivalence.from โˆˆ-singleton y) - -opaque - EB-Role-total : โˆƒ[ s' ] s -โŸฆEB-RoleโŸงโ‡€ s' - EB-Role-total {s = s} = let open LeiosState s in case Dec-canProduceEB of ฮป where - (injโ‚ (ฯ€ , pf)) โ†’ -, EB-Role pf (projโ‚‚ FFD.FFD-total) - (injโ‚‚ pf) โ†’ -, No-EB-Role pf - - EB-Role-total' : โˆƒ[ ffds ] s -โŸฆEB-RoleโŸงโ‡€ addUpkeep record s { FFDState = ffds } EB-Role - EB-Role-total' {s = s} = let open LeiosState s in case Dec-canProduceEB of ฮป where - (injโ‚ (ฯ€ , pf)) โ†’ -, EB-Role pf (projโ‚‚ FFD.FFD-total) - (injโ‚‚ pf) โ†’ -, No-EB-Role pf - -data _-โŸฆV1-RoleโŸงโ‡€_ : LeiosState โ†’ LeiosState โ†’ Type where - - V1-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_โˆˆแดฎ slice L slot (ฮผ + 1)) EBs - votes = map (vote sk-V โˆ˜ hash) EBs' - in - โˆ™ canProduceV1 slot sk-V (stake s) - โˆ™ ffds FFD.-โŸฆ Send (vHeader votes) nothing / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆV1-RoleโŸงโ‡€ addUpkeep record s { FFDState = ffds' } V1-Role - - No-V1-Role : let open LeiosState s in - โˆ™ ยฌ canProduceV1 slot sk-V (stake s) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆV1-RoleโŸงโ‡€ addUpkeep s V1-Role - -V1-Roleโ‡’ND : LeiosState.needsUpkeep s V1-Role โ†’ s -โŸฆV1-RoleโŸงโ‡€ s' โ†’ just s ND.-โŸฆ SLOT / EMPTY โŸงโ‡€ s' -V1-Roleโ‡’ND u (V1-Role xโ‚ xโ‚‚) = Roles (V1-Role u xโ‚ xโ‚‚) -V1-Roleโ‡’ND u (No-V1-Role xโ‚) = Roles (No-V1-Role u xโ‚) - -V1-Role-Upkeep : โˆ€ {u} โ†’ u โ‰ข V1-Role โ†’ LeiosState.needsUpkeep s u โ†’ s -โŸฆV1-RoleโŸงโ‡€ s' - โ†’ LeiosState.needsUpkeep s' u -V1-Role-Upkeep uโ‰ขV1-Role h (V1-Role _ _) uโˆˆsu = case Equivalence.from โˆˆ-โˆช uโˆˆsu of ฮป where - (injโ‚ x) โ†’ h x - (injโ‚‚ y) โ†’ uโ‰ขV1-Role (Equivalence.from โˆˆ-singleton y) -V1-Role-Upkeep uโ‰ขV1-Role h (No-V1-Role _) uโˆˆsu = case Equivalence.from โˆˆ-โˆช uโˆˆsu of ฮป where - (injโ‚ x) โ†’ h x - (injโ‚‚ y) โ†’ uโ‰ขV1-Role (Equivalence.from โˆˆ-singleton y) - -opaque - V1-Role-total : โˆƒ[ s' ] s -โŸฆV1-RoleโŸงโ‡€ s' - V1-Role-total {s = s} = let open LeiosState s in case Dec-canProduceV1 of ฮป where - (yes p) โ†’ -, V1-Role p (projโ‚‚ FFD.FFD-total) - (no ยฌp) โ†’ -, No-V1-Role ยฌp - - V1-Role-total' : โˆƒ[ ffds ] s -โŸฆV1-RoleโŸงโ‡€ addUpkeep record s { FFDState = ffds } V1-Role - V1-Role-total' {s = s} = let open LeiosState s in case Dec-canProduceV1 of ฮป where - (yes p) โ†’ -, V1-Role p (projโ‚‚ FFD.FFD-total) - (no ยฌp) โ†’ -, No-V1-Role ยฌp - -data _-โŸฆV2-RoleโŸงโ‡€_ : LeiosState โ†’ LeiosState โ†’ Type where - - V2-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (vote2Eligible s) $ filter (_โˆˆแดฎ slice L slot 1) EBs - votes = map (vote sk-V โˆ˜ hash) EBs' - in - โˆ™ canProduceV2 slot sk-V (stake s) - โˆ™ ffds FFD.-โŸฆ Send (vHeader votes) nothing / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆV2-RoleโŸงโ‡€ addUpkeep record s { FFDState = ffds' } V2-Role - - No-V2-Role : let open LeiosState s in - โˆ™ ยฌ canProduceV2 slot sk-V (stake s) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆV2-RoleโŸงโ‡€ addUpkeep s V2-Role - -V2-Roleโ‡’ND : LeiosState.needsUpkeep s V2-Role โ†’ s -โŸฆV2-RoleโŸงโ‡€ s' โ†’ just s ND.-โŸฆ SLOT / EMPTY โŸงโ‡€ s' -V2-Roleโ‡’ND u (V2-Role xโ‚ xโ‚‚) = Roles (V2-Role u xโ‚ xโ‚‚) -V2-Roleโ‡’ND u (No-V2-Role xโ‚) = Roles (No-V2-Role u xโ‚) - -V2-Role-Upkeep : โˆ€ {u} โ†’ u โ‰ข V2-Role โ†’ LeiosState.needsUpkeep s u โ†’ s -โŸฆV2-RoleโŸงโ‡€ s' - โ†’ LeiosState.needsUpkeep s' u -V2-Role-Upkeep uโ‰ขV2-Role h (V2-Role _ _) uโˆˆsu = case Equivalence.from โˆˆ-โˆช uโˆˆsu of ฮป where - (injโ‚ x) โ†’ h x - (injโ‚‚ y) โ†’ uโ‰ขV2-Role (Equivalence.from โˆˆ-singleton y) -V2-Role-Upkeep uโ‰ขV2-Role h (No-V2-Role _) uโˆˆsu = case Equivalence.from โˆˆ-โˆช uโˆˆsu of ฮป where - (injโ‚ x) โ†’ h x - (injโ‚‚ y) โ†’ uโ‰ขV2-Role (Equivalence.from โˆˆ-singleton y) - -opaque - V2-Role-total : โˆƒ[ s' ] s -โŸฆV2-RoleโŸงโ‡€ s' - V2-Role-total {s = s} = let open LeiosState s in case Dec-canProduceV2 of ฮป where - (yes p) โ†’ -, V2-Role p (projโ‚‚ FFD.FFD-total) - (no ยฌp) โ†’ -, No-V2-Role ยฌp - - V2-Role-total' : โˆƒ[ ffds ] s -โŸฆV2-RoleโŸงโ‡€ addUpkeep record s { FFDState = ffds } V2-Role - V2-Role-total' {s = s} = let open LeiosState s in case Dec-canProduceV2 of ฮป where - (yes p) โ†’ -, V2-Role p (projโ‚‚ FFD.FFD-total) - (no ยฌp) โ†’ -, No-V2-Role ยฌp - -data _-โŸฆ_/_โŸงโ‡€_ : LeiosState โ†’ LeiosInput โ†’ LeiosOutput โ†’ LeiosState โ†’ Type where - - -- Network and Ledger - - Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) - s0 = record s - { FFDState = ffds' - ; Ledger = constructLedger rbs - ; slot = suc slot - ; Upkeep = โˆ… - ; BaseState = bs' - } โ†‘ L.filter isValid? msgs - in - โˆ™ Upkeep โ‰กแต‰ allUpkeep - โˆ™ bs B.-โŸฆ B.FTCH-LDG / B.BASE-LDG rbs โŸงโ‡€ bs' - โˆ™ ffds FFD.-โŸฆ Fetch / FetchRes msgs โŸงโ‡€ ffds' - โˆ™ s0 -โŸฆBaseโŸงโ‡€ s1 - โˆ™ s1 -โŸฆIB-RoleโŸงโ‡€ s2 - โˆ™ s2 -โŸฆEB-RoleโŸงโ‡€ s3 - โˆ™ s3 -โŸฆV1-RoleโŸงโ‡€ s4 - โˆ™ s4 -โŸฆV2-RoleโŸงโ‡€ s5 - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆ SLOT / EMPTY โŸงโ‡€ s5 - - Ftch : - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆ FTCH-LDG / FTCH-LDG (LeiosState.Ledger s) โŸงโ‡€ s - - -- Base chain - -- - -- Note: Submitted data to the base chain is only taken into account - -- if the party submitting is the block producer on the base chain - -- for the given slot - - Baseโ‚ : - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆ SUBMIT (injโ‚‚ txs) / EMPTY โŸงโ‡€ record s { ToPropose = txs } - - -- Protocol rules - -_-โŸฆ_/_โŸงโฟแตˆโ‡€_ : LeiosState โ†’ LeiosInput โ†’ LeiosOutput โ†’ LeiosState โ†’ Type -s -โŸฆ i / o โŸงโฟแตˆโ‡€ s' = just s ND.-โŸฆ i / o โŸงโ‡€ s' - -_-โŸฆ_/_โŸงโฟแตˆ*โ‡€_ : LeiosState โ†’ List LeiosInput โ†’ List LeiosOutput โ†’ LeiosState โ†’ Type -_-โŸฆ_/_โŸงโฟแตˆ*โ‡€_ = ReflexiveTransitiveClosure _-โŸฆ_/_โŸงโฟแตˆโ‡€_ - --- Key fact: stepping with the deterministic relation means we can --- also step with the non-deterministic one --- TODO: this is a lot like a weak simulation, can we do something prettier? --โŸฆ/โŸงโ‡€โ‡’ND : s -โŸฆ i / o โŸงโ‡€ s' โ†’ โˆƒโ‚‚[ i , o ] (s -โŸฆ i / o โŸงโฟแตˆ*โ‡€ s') --โŸฆ/โŸงโ‡€โ‡’ND (Slot {s = s} {msgs = msgs} {s1 = s1} {s2 = s2} {s3 = s3} {s4 = s4} x xโ‚ xโ‚‚ hB hIB hEB hV1 hV2) = replicate 6 SLOT , replicate 6 EMPTY , - let - s0 = _ - upkeepโ‰กโˆ… : LeiosState.Upkeep s0 โ‰ก โˆ… - upkeepโ‰กโˆ… = sym (โ†‘-preserves-Upkeep {x = L.filter isValid? msgs}) - needsAllUpkeep : โˆ€ {u} โ†’ LeiosState.needsUpkeep s0 u - needsAllUpkeep {u} = subst (u โˆ‰_) (sym upkeepโ‰กโˆ…) Properties.โˆ‰-โˆ… - needsUpkeep1 : โˆ€ {u} โ†’ u โ‰ข Base โ†’ LeiosState.needsUpkeep s1 u - needsUpkeep1 h1 = Base-Upkeep h1 needsAllUpkeep hB - needsUpkeep2 : โˆ€ {u} โ†’ u โ‰ข Base โ†’ u โ‰ข IB-Role โ†’ LeiosState.needsUpkeep s2 u - needsUpkeep2 h1 h2 = IB-Role-Upkeep h2 (needsUpkeep1 h1) hIB - needsUpkeep3 : โˆ€ {u} โ†’ u โ‰ข Base โ†’ u โ‰ข IB-Role โ†’ u โ‰ข EB-Role โ†’ LeiosState.needsUpkeep s3 u - needsUpkeep3 h1 h2 h3 = EB-Role-Upkeep h3 (needsUpkeep2 h1 h2) hEB - needsUpkeep4 : โˆ€ {u} โ†’ u โ‰ข Base โ†’ u โ‰ข IB-Role โ†’ u โ‰ข EB-Role โ†’ u โ‰ข V1-Role โ†’ LeiosState.needsUpkeep s4 u - needsUpkeep4 h1 h2 h3 h4 = V1-Role-Upkeep h4 (needsUpkeep3 h1 h2 h3) hV1 - in (BS-ind (ND.Slot x xโ‚ xโ‚‚) $ - BS-ind (Baseโ‡’ND {s = s0} needsAllUpkeep hB) $ - BS-ind (IB-Roleโ‡’ND (needsUpkeep1 (ฮป ())) hIB) $ - BS-ind (EB-Roleโ‡’ND (needsUpkeep2 (ฮป ()) (ฮป ())) hEB) $ - BS-ind (V1-Roleโ‡’ND (needsUpkeep3 (ฮป ()) (ฮป ()) (ฮป ())) hV1) $ - STSโ‡’RTC (V2-Roleโ‡’ND (needsUpkeep4 (ฮป ()) (ฮป ()) (ฮป ()) (ฮป ())) hV2)) --โŸฆ/โŸงโ‡€โ‡’ND Ftch = _ , _ , STSโ‡’RTC Ftch --โŸฆ/โŸงโ‡€โ‡’ND Baseโ‚ = _ , _ , STSโ‡’RTC Baseโ‚ - -open Computational22 โฆƒ...โฆ„ - -module _ โฆƒ Computational-B : Computational22 B._-โŸฆ_/_โŸงโ‡€_ String โฆ„ - โฆƒ Computational-FFD : Computational22 FFD._-โŸฆ_/_โŸงโ‡€_ String โฆ„ where - - instance - Computational--โŸฆ/โŸงโ‡€ : Computational22 _-โŸฆ_/_โŸงโ‡€_ String - Computational--โŸฆ/โŸงโ‡€ .computeProof s (INIT x) = failure "No handling of INIT here" - Computational--โŸฆ/โŸงโ‡€ .computeProof s (SUBMIT (injโ‚ eb)) = failure "Cannot submit EB here" - Computational--โŸฆ/โŸงโ‡€ .computeProof s (SUBMIT (injโ‚‚ txs)) = success (-, Baseโ‚) - Computational--โŸฆ/โŸงโ‡€ .computeProof s* SLOT = let open LeiosState s* in - case (ยฟ Upkeep โ‰กแต‰ allUpkeep ยฟ ,โ€ฒ computeProof BaseState B.FTCH-LDG ,โ€ฒ computeProof FFDState FFD.Fetch) of ฮป where - (yes p , success ((B.BASE-LDG l , bs) , pโ‚) , success ((FFD.FetchRes msgs , ffds) , pโ‚‚)) โ†’ - success ((_ , (Slot p pโ‚ pโ‚‚ (projโ‚‚ Base-total) (projโ‚‚ IB-Role-total) (projโ‚‚ EB-Role-total) (projโ‚‚ V1-Role-total) (projโ‚‚ V2-Role-total)))) - (yes p , _ , _) โ†’ failure "Subsystem failed" - (no ยฌp , _) โ†’ failure "Upkeep incorrect" - Computational--โŸฆ/โŸงโ‡€ .computeProof s FTCH-LDG = success (-, Ftch) - Computational--โŸฆ/โŸงโ‡€ .completeness = {!!} diff --git a/formal-spec/Leios/Simplified/Deterministic/Test.agda b/formal-spec/Leios/Simplified/Deterministic/Test.agda deleted file mode 100644 index a941eef8e..000000000 --- a/formal-spec/Leios/Simplified/Deterministic/Test.agda +++ /dev/null @@ -1,94 +0,0 @@ --------------------------------------------------------------------------------- --- Deterministic variant of simple Leios --------------------------------------------------------------------------------- - -open import Leios.Prelude hiding (id) -open import Prelude.Init using (โˆƒโ‚‚-syntax) -open import Leios.FFD - -import Data.List as L -open import Data.List.Relation.Unary.Any using (here) - -open import Leios.SpecStructure -open import Leios.Trace using (st-2) - -module Leios.Simplified.Deterministic.Test (ฮ› ฮผ : โ„•) where - -open SpecStructure st-2 - -import Leios.Simplified -open import Leios.Simplified st-2 ฮ› ฮผ hiding (_-โŸฆ_/_โŸงโ‡€_) renaming (initLeiosState to initLeiosState') -module ND = Leios.Simplified st-2 ฮ› ฮผ - -open import Class.Computational -open import Class.Computational22 -open import StateMachine - -open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot) -open GenFFD - -open FFD hiding (_-โŸฆ_/_โŸงโ‡€_) - -private variable s s' s0 s1 s2 s3 s4 s5 : LeiosState - i : LeiosInput - o : LeiosOutput - ffds' : FFD.State - ฯ€ : VrfPf - bs' : B.State - ks ks' : K.State - msgs : List (FFDAbstract.Header ffdAbstract โŠŽ FFDAbstract.Body ffdAbstract) - eb : EndorserBlock - rbs : List RankingBlock - txs : List Tx - V : VTy - SD : StakeDistr - pks : List PubKey - -open Computational22 โฆƒ...โฆ„ -open import Leios.Simplified.Deterministic st-2 ฮ› ฮผ - -instance - Computational-B : Computational22 B._-โŸฆ_/_โŸงโ‡€_ String - Computational-B .computeProof s (BaseAbstract.Input.INIT x) = - success ((BaseAbstract.Output.STAKE {!!} , tt) , tt) - Computational-B .computeProof s (BaseAbstract.Input.SUBMIT x) = - success ((BaseAbstract.Output.EMPTY , tt) , tt) - Computational-B .computeProof s BaseAbstract.Input.FTCH-LDG = - success ((BaseAbstract.Output.BASE-LDG [] , tt) , tt) - Computational-B .completeness = {!!} - - Computational-FFD : Computational22 FFD._-โŸฆ_/_โŸงโ‡€_ String - Computational-FFD .computeProof s (FFDAbstract.Send x xโ‚) = success ((FFDAbstract.SendRes , tt) , tt) - Computational-FFD .computeProof s FFDAbstract.Fetch = success ((FFDAbstract.FetchRes [] , tt) , tt) - Computational-FFD .completeness = {!!} - -comp = Computational--โŸฆ/โŸงโ‡€ โฆƒ Computational-B โฆ„ โฆƒ Computational-FFD โฆ„ - -initLeiosState : VTy โ†’ StakeDistr โ†’ B.State โ†’ LeiosState -initLeiosState v sd bs = record (initLeiosState' v sd bs) { Upkeep = allUpkeep } - -module _ v sd bs where opaque - unfolding List-Modelแตˆ V2-Role-total - - computeProofTy : (s : LeiosState) (i : LeiosInput) - โ†’ ComputationResult String (ฮฃ[ (o , s') โˆˆ LeiosOutput ร— LeiosState ] s -โŸฆ i / o โŸงโ‡€ s') - computeProofTy = computeProof โฆƒ comp โฆ„ - - compute-โ‰ก : (s : LeiosState) (i : LeiosInput) - โ†’ compute โฆƒ comp โฆ„ s i โ‰ก map โฆƒ Functor-ComputationResult โฆ„ projโ‚ (computeProof โฆƒ comp โฆ„ s i) - compute-โ‰ก s i = refl - - testโ‚ : โˆ€ tx - โ†’ ฮฃ[ x โˆˆ LeiosOutput ร— LeiosState ] compute (initLeiosState v sd bs) (SUBMIT (injโ‚‚ [ tx ])) - โ‰ก success x - testโ‚ tx = -, refl - - testโ‚‚ : ฮฃ[ x โˆˆ LeiosOutput ร— LeiosState ] compute (initLeiosState v sd bs) SLOT - โ‰ก success x - testโ‚‚ = -, refl - - testโ‚ƒ : Tx โ†’ Set - testโ‚ƒ tx = {!projโ‚ testโ‚‚!} - - trace : ComputationResult String (List LeiosOutput ร— LeiosState) - trace = computeTrace (initLeiosState v sd bs) (SLOT โˆท SLOT โˆท []) diff --git a/formal-spec/Leios/SpecStructure.agda b/formal-spec/Leios/SpecStructure.agda deleted file mode 100644 index 0ab4317ad..000000000 --- a/formal-spec/Leios/SpecStructure.agda +++ /dev/null @@ -1,53 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude hiding (id) -open import Leios.Abstract -open import Leios.FFD -open import Leios.VRF - -import Leios.Base -import Leios.Blocks -import Leios.KeyRegistration -import Leios.Voting - -open import Data.Fin - -module Leios.SpecStructure where - -record SpecStructure (rounds : โ„•) : Typeโ‚ where - field a : LeiosAbstract - - open LeiosAbstract a public - open Leios.Blocks a public - - field โฆƒ IsBlock-Vote โฆ„ : IsBlock (List Vote) - โฆƒ Hashable-IBHeaderOSig โฆ„ : โˆ€ {b} โ†’ Hashable (IBHeaderOSig b) Hash - โฆƒ Hashable-PreEndorserBlock โฆ„ : Hashable PreEndorserBlock Hash - id : PoolID - FFD' : FFDAbstract.Functionality ffdAbstract - vrf' : LeiosVRF a - - open LeiosVRF vrf' public - - field sk-IB sk-EB sk-V : PrivKey - pk-IB pk-EB pk-V : PubKey - - open Leios.Base a vrf' public - - field B' : BaseAbstract - BF : BaseAbstract.Functionality B' - initBaseState : BaseAbstract.Functionality.State BF - - open Leios.KeyRegistration a vrf' public - - field K' : KeyRegistrationAbstract - KF : KeyRegistrationAbstract.Functionality K' - - module B = BaseAbstract.Functionality BF - module K = KeyRegistrationAbstract.Functionality KF - module FFD = FFDAbstract.Functionality FFD' - - open Leios.Voting public - - field va : VotingAbstract (Fin rounds ร— EndorserBlock) - open VotingAbstract va public diff --git a/formal-spec/Leios/Trace.agda b/formal-spec/Leios/Trace.agda deleted file mode 100644 index 72ca81947..000000000 --- a/formal-spec/Leios/Trace.agda +++ /dev/null @@ -1,290 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude -open import Leios.Abstract -open import Leios.SpecStructure -open import Axiom.Set.Properties th - -open import Data.Fin -open import Function.Related.TypeIsomorphisms -open import Relation.Binary.Structures - -import Data.Sum - -open Equivalence - --- The module contains very simple implementations for the functionalities --- that allow to build examples for traces for the different Leios variants -module Leios.Trace where - -instance - htx : Hashable (List โŠค) โŠค - htx = record { hash = ฮป _ โ†’ tt } - -d-Abstract : LeiosAbstract -d-Abstract = - record - { Tx = โŠค - ; PoolID = Fin 1 - ; BodyHash = โŠค - ; VrfPf = โŠค - ; PrivKey = โŠค - ; Sig = โŠค - ; Hash = โŠค - ; Vote = โŠค - ; vote = ฮป _ _ โ†’ tt - ; sign = ฮป _ _ โ†’ tt - ; L = 5 - } - -open LeiosAbstract d-Abstract public - -open import Leios.VRF d-Abstract public - -d-VRF : LeiosVRF -d-VRF = - record - { PubKey = โŠค - ; vrf = record { isKeyPair = ฮป _ _ โ†’ โŠค ; eval = ฮป x xโ‚ โ†’ xโ‚ , x ; verify = ฮป _ _ _ _ โ†’ โŠค } - ; genIBInput = id - ; genEBInput = id - ; genVInput = id - ; genV1Input = id - ; genV2Input = id - } - -open LeiosVRF d-VRF public - -open import Leios.Blocks d-Abstract public -open import Leios.KeyRegistration d-Abstract d-VRF public - -d-KeyRegistration : KeyRegistrationAbstract -d-KeyRegistration = _ - -d-KeyRegistrationFunctionality : KeyRegistrationAbstract.Functionality d-KeyRegistration -d-KeyRegistrationFunctionality = - record - { State = โŠค - ; _-โŸฆ_/_โŸงโ‡€_ = ฮป _ _ _ _ โ†’ โŠค - } - -open import Leios.Base d-Abstract d-VRF public - -d-Base : BaseAbstract -d-Base = - record - { Cert = โŠค - ; VTy = โŠค - ; initSlot = ฮป _ โ†’ 0 - ; V-chkCerts = ฮป _ _ โ†’ true - } - -d-BaseFunctionality : BaseAbstract.Functionality d-Base -d-BaseFunctionality = - record - { State = โŠค - ; _-โŸฆ_/_โŸงโ‡€_ = ฮป _ _ _ _ โ†’ โŠค - ; SUBMIT-total = tt , tt - } - -open import Leios.FFD public - -instance - isb : IsBlock (List โŠค) - isb = - record - { slotNumber = ฮป _ โ†’ 0 - ; producerID = ฮป _ โ†’ zero - ; lotteryPf = ฮป _ โ†’ tt - } - - hhs : โˆ€ {b} โ†’ Hashable (IBHeaderOSig b) โŠค - hhs = record { hash = ฮป _ โ†’ tt } - - hpe : Hashable PreEndorserBlock โŠค - hpe = record { hash = ฮป x โ†’ tt } - -d-FFDFunctionality : FFDAbstract.Functionality ffdAbstract -d-FFDFunctionality = - record - { State = โŠค - ; initFFDState = tt - ; _-โŸฆ_/_โŸงโ‡€_ = ฮป _ _ _ _ โ†’ โŠค - ; FFD-total = tt , tt - } - -open import Leios.Voting public - -d-VotingAbstract : VotingAbstract (Fin 1 ร— EndorserBlock) -d-VotingAbstract = - record - { VotingState = โŠค - ; initVotingState = tt - ; isVoteCertified = ฮป _ _ โ†’ โŠค - } - -d-VotingAbstract-2 : VotingAbstract (Fin 2 ร— EndorserBlock) -d-VotingAbstract-2 = - record - { VotingState = โŠค - ; initVotingState = tt - ; isVoteCertified = ฮป _ _ โ†’ โŠค - } - -st : SpecStructure 1 -st = record - { a = d-Abstract - ; id = zero - ; FFD' = d-FFDFunctionality - ; vrf' = d-VRF - ; sk-IB = tt - ; sk-EB = tt - ; sk-V = tt - ; pk-IB = tt - ; pk-EB = tt - ; pk-V = tt - ; B' = d-Base - ; BF = d-BaseFunctionality - ; initBaseState = tt - ; K' = d-KeyRegistration - ; KF = d-KeyRegistrationFunctionality - ; va = d-VotingAbstract - } - -st-2 : SpecStructure 2 -st-2 = record - { a = d-Abstract - ; id = zero - ; FFD' = d-FFDFunctionality - ; vrf' = d-VRF - ; sk-IB = tt - ; sk-EB = tt - ; sk-V = tt - ; pk-IB = tt - ; pk-EB = tt - ; pk-V = tt - ; B' = d-Base - ; BF = d-BaseFunctionality - ; initBaseState = tt - ; K' = d-KeyRegistration - ; KF = d-KeyRegistrationFunctionality - ; va = d-VotingAbstract-2 - } - -open import Leios.Short st public - -sd : TotalMap (Fin 1) โ„• -sd = record - { rel = singleton (zero , 1) - ; left-unique-rel = ฮป x y โ†’ - let a = cong projโ‚‚ (from โˆˆ-singleton x) - b = cong projโ‚‚ (from โˆˆ-singleton y) - in trans a (sym b) - ; total-rel = total-rel-helper - } - where - total-rel-helper : โˆ€ {a : Fin 1} โ†’ a โˆˆ dom (singleton (zero , 1)) - total-rel-helper {zero} = to domโˆˆ (1 , (to โˆˆ-singleton refl)) - -sโ‚€ : LeiosState -sโ‚€ = initLeiosState tt sd tt - -open import Leios.Traces st _-โŸฆ_/_โŸงโ‡€_ - --- i) Same slot - -ftch-step : sโ‚€ โ‡‰ sโ‚€ -ftch-step = (FTCH-LDG , FTCH-LDG []) , Ftch - -trace : sโ‚€ โ‡‰โ‹† sโ‚€ -trace = 1 , (sโ‚€ , (ftch-step , refl)) - --- ii) Slot transition - -tโ‚ : LeiosState -tโ‚ = addUpkeep sโ‚€ IB-Role - -tโ‚‚ : LeiosState -tโ‚‚ = addUpkeep tโ‚ EB-Role - -tโ‚ƒ : LeiosState -tโ‚ƒ = addUpkeep tโ‚‚ V-Role - -tโ‚„ : LeiosState -tโ‚„ = addUpkeep tโ‚ƒ Base - -sโ‚ : LeiosState -sโ‚ = let open LeiosState tโ‚„ in - record tโ‚„ - { FFDState = tt - ; BaseState = tt - ; Ledger = [] - ; IBs = [] - ; IBHeaders = [] - ; IBBodies = [] - ; EBs = [] - ; Vs = [] - ; slot = suc slot - ; Upkeep = โˆ… - } - -open TotalMap - -stakeโ‰ก1 : TotalMap.lookup (LeiosState.SD sโ‚€) (SpecStructure.id st) โ‰ก 1 -stakeโ‰ก1 = โˆˆ-relโ‡’lookup-โ‰ก (LeiosState.SD sโ‚€) {a = zero} {b = 1} (to โˆˆ-singleton refl) - -ib-step : sโ‚€ โ‡‰ tโ‚ -ib-step = (SLOT , EMPTY) , Roles (IB-Role {ฯ€ = tt} uk ฯ€-IB tt) - where - uk : IB-Role โˆ‰ LeiosState.Upkeep sโ‚€ - uk = ฮป x โ†’ โˆ‰-โˆ… x - - ฯ€-IB : canProduceIB (LeiosState.slot sโ‚€) tt (stake sโ‚€) tt - ฯ€-IB rewrite stakeโ‰ก1 = sโ‰คs zโ‰คn , refl - -lem1 : โˆ€ {A} {a : A} {B C : โ„™ A} โ†’ a โˆ‰ B โ†’ a โˆ‰ C โ†’ a โˆ‰ B โˆช C -lem1 {_} {_} {B} {C} x y = Data.Sum.[ x , y ] โˆ˜ โˆˆ-โˆชโป {X = B} {Y = C} - -lem2 : โˆ€ {A} {a : A} {B : โ„™ A} โ†’ a โˆ‰ B โ†’ a โˆ‰ โˆ… โˆช B -lem2 {_} {_} {B} = lem1 {B = โˆ…} {C = B} โˆ‰-โˆ… - -lem3 : โˆ€ {A} {a b : A} โ†’ a โ‰ข b โ†’ a โˆ‰ singleton b -lem3 = to (ยฌ-cong-โ‡” โˆˆ-singleton) - -eb-step : tโ‚ โ‡‰ tโ‚‚ -eb-step = (SLOT , EMPTY) , Roles (EB-Role {ฯ€ = tt} uk ฯ€-EB tt) - where - uk : EB-Role โˆ‰ โˆ… โˆช โด IB-Role โต - uk = lem2 (lem3 (ฮป ())) - - ฯ€-EB : canProduceEB (LeiosState.slot sโ‚€) tt (stake sโ‚€) tt - ฯ€-EB rewrite stakeโ‰ก1 = sโ‰คs zโ‰คn , refl - -v-step : tโ‚‚ โ‡‰ tโ‚ƒ -v-step = (SLOT , EMPTY) , Roles (V-Role uk ฯ€-V tt) - where - uk : V-Role โˆ‰ (โˆ… โˆช โด IB-Role โต) โˆช โด EB-Role โต - uk = lem1 (lem2 (lem3 ฮป ())) (lem3 ฮป ()) - - ฯ€-V : canProduceV (LeiosState.slot sโ‚€) tt (stake sโ‚€) - ฯ€-V rewrite stakeโ‰ก1 = sโ‰คs zโ‰คn - -base-step : tโ‚ƒ โ‡‰ tโ‚„ -base-step = (SLOT , EMPTY) , Baseโ‚‚b uk refl tt - where - uk : Base โˆ‰ ((โˆ… โˆช โด IB-Role โต) โˆช โด EB-Role โต) โˆช โด V-Role โต - uk = lem1 (lem1 (lem2 (lem3 ฮป ())) (lem3 ฮป ())) (lem3 ฮป ()) - -open IsEquivalence (โ‰กแต‰-isEquivalence {SlotUpkeep}) renaming (refl to โ‰กแต‰-refl) - -slot-step : tโ‚„ โ‡‰ sโ‚ -slot-step = (SLOT , EMPTY) , Slot {rbs = []} {msgs = []} โ‰กแต‰-refl tt tt - -slot-transition-trace : sโ‚€ โ‡‰โ‹† sโ‚ -slot-transition-trace = 5 - , tโ‚ , ib-step - , tโ‚‚ , eb-step - , tโ‚ƒ , v-step - , tโ‚„ , base-step - , sโ‚ , slot-step - , refl diff --git a/formal-spec/Leios/Traces.agda b/formal-spec/Leios/Traces.agda deleted file mode 100644 index b535bf415..000000000 --- a/formal-spec/Leios/Traces.agda +++ /dev/null @@ -1,20 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude -open import Leios.SpecStructure - -import Leios.Protocol - -module Leios.Traces {n} (โ‹ฏ : SpecStructure n) {u : Type} (let open Leios.Protocol โ‹ฏ u) - (_-โŸฆ_/_โŸงโ‡€_ : Maybe LeiosState โ†’ LeiosInput โ†’ LeiosOutput โ†’ LeiosState โ†’ Type) - where - -_โ‡‰_ : LeiosState โ†’ LeiosState โ†’ Type -sโ‚ โ‡‰ sโ‚‚ = ฮฃ[ (i , o) โˆˆ LeiosInput ร— LeiosOutput ] (just sโ‚ -โŸฆ i / o โŸงโ‡€ sโ‚‚) - -_โ‡‰[_]_ : LeiosState โ†’ โ„• โ†’ LeiosState โ†’ Type -sโ‚ โ‡‰[ zero ] sโ‚‚ = sโ‚ โ‰ก sโ‚‚ -sโ‚ โ‡‰[ suc m ] sโ‚™ = ฮฃ[ sโ‚‚ โˆˆ LeiosState ] (sโ‚ โ‡‰ sโ‚‚ ร— sโ‚‚ โ‡‰[ m ] sโ‚™) - -_โ‡‰โ‹†_ : LeiosState โ†’ LeiosState โ†’ Type -sโ‚ โ‡‰โ‹† sโ‚™ = ฮฃ[ n โˆˆ โ„• ] (sโ‚ โ‡‰[ n ] sโ‚™) diff --git a/formal-spec/Leios/UniformShort.agda b/formal-spec/Leios/UniformShort.agda deleted file mode 100644 index ceaedf024..000000000 --- a/formal-spec/Leios/UniformShort.agda +++ /dev/null @@ -1,157 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude hiding (id) -open import Leios.FFD -open import Leios.SpecStructure -open import Data.Fin.Patterns - -module Leios.UniformShort (โ‹ฏ : SpecStructure 1) - (let open SpecStructure โ‹ฏ renaming (isVoteCertified to isVoteCertified')) where - -data SlotUpkeep : Type where - Base IB-Role EB-Role V-Role : SlotUpkeep - -allUpkeep : โ„™ SlotUpkeep -allUpkeep = fromList (Base โˆท IB-Role โˆท EB-Role โˆท V-Role โˆท []) - -open import Leios.Protocol (โ‹ฏ) SlotUpkeep public - -open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot) -open FFD hiding (_-โŸฆ_/_โŸงโ‡€_) -open GenFFD - -isVoteCertified : LeiosState โ†’ EndorserBlock โ†’ Type -isVoteCertified s eb = isVoteCertified' (LeiosState.votingState s) (0F , eb) - -module Protocol where - - private variable s s' : LeiosState - ffds' : FFD.State - ฯ€ : VrfPf - bs' : B.State - ks ks' : K.State - msgs : List (FFDAbstract.Header ffdAbstract โŠŽ FFDAbstract.Body ffdAbstract) - eb : EndorserBlock - rbs : List RankingBlock - txs : List Tx - V : VTy - SD : StakeDistr - pks : List PubKey - - -- Uniform Short Pipeline: - -- - -- 1. If elected, propose IB - -- 2. Wait - -- 3. Wait - -- 4. If elected, propose EB - -- 5. If elected, vote - -- If elected, propose RB - - data _โ†_ : LeiosState โ†’ LeiosState โ†’ Type where - - IB-Role : let open LeiosState s renaming (FFDState to ffds) - b = ibBody (record { txs = ToPropose }) - h = ibHeader (mkIBHeader slot id ฯ€ sk-IB ToPropose) - in - โˆ™ needsUpkeep IB-Role - โˆ™ canProduceIB slot sk-IB (stake s) ฯ€ - โˆ™ ffds FFD.-โŸฆ Send h (just b) / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep record s { FFDState = ffds' } IB-Role - - EB-Role : let open LeiosState s renaming (FFDState to ffds) - LI = map getIBRef $ filter (_โˆˆแดฎ slice L slot 3) IBs - h = mkEB slot id ฯ€ sk-EB LI [] - in - โˆ™ needsUpkeep EB-Role - โˆ™ canProduceEB slot sk-EB (stake s) ฯ€ - โˆ™ ffds FFD.-โŸฆ Send (ebHeader h) nothing / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep record s { FFDState = ffds' } EB-Role - - V-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_โˆˆแดฎ slice L slot 1) EBs - votes = map (vote sk-V โˆ˜ hash) EBs' - in - โˆ™ needsUpkeep V-Role - โˆ™ canProduceV slot sk-V (stake s) - โˆ™ ffds FFD.-โŸฆ Send (vHeader votes) nothing / SendRes โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep record s { FFDState = ffds' } V-Role - - No-IB-Role : let open LeiosState s in - โˆ™ needsUpkeep IB-Role - โˆ™ ยฌ canProduceIB slot sk-IB (stake s) ฯ€ - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep s IB-Role - - No-EB-Role : let open LeiosState s in - โˆ™ needsUpkeep EB-Role - โˆ™ ยฌ canProduceEB slot sk-EB (stake s) ฯ€ - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep s EB-Role - - No-V-Role : let open LeiosState s in - โˆ™ needsUpkeep V-Role - โˆ™ ยฌ canProduceV slot sk-V (stake s) - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s โ† addUpkeep s V-Role - - data _-โŸฆ_/_โŸงโ‡€_ : Maybe LeiosState โ†’ LeiosInput โ†’ LeiosOutput โ†’ LeiosState โ†’ Type where - - -- Initialization - - Init : - โˆ™ ks K.-โŸฆ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks โŸงโ‡€ ks' - โˆ™ initBaseState B.-โŸฆ B.INIT (V-chkCerts pks) / B.STAKE SD โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - nothing -โŸฆ INIT V / EMPTY โŸงโ‡€ initLeiosState V SD bs' - - -- Network and Ledger - - Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) in - โˆ™ Upkeep โ‰กแต‰ allUpkeep - โˆ™ bs B.-โŸฆ B.FTCH-LDG / B.BASE-LDG rbs โŸงโ‡€ bs' - โˆ™ ffds FFD.-โŸฆ Fetch / FetchRes msgs โŸงโ‡€ ffds' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ record s - { FFDState = ffds' - ; BaseState = bs' - ; Ledger = constructLedger rbs - ; slot = suc slot - ; Upkeep = โˆ… - } โ†‘ L.filter isValid? msgs - - Ftch : - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ FTCH-LDG / FTCH-LDG (LeiosState.Ledger s) โŸงโ‡€ s - - -- Base chain - -- - -- Note: Submitted data to the base chain is only taken into account - -- if the party submitting is the block producer on the base chain - -- for the given slot - - Baseโ‚ : - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SUBMIT (injโ‚‚ txs) / EMPTY โŸงโ‡€ record s { ToPropose = txs } - - Baseโ‚‚a : let open LeiosState s renaming (BaseState to bs) in - โˆ™ needsUpkeep Base - โˆ™ eb โˆˆ filter (ฮป eb โ†’ isVoteCertified s eb ร— eb โˆˆแดฎ slice L slot 2) EBs - โˆ™ bs B.-โŸฆ B.SUBMIT (this eb) / B.EMPTY โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ addUpkeep record s { BaseState = bs' } Base - - Baseโ‚‚b : let open LeiosState s renaming (BaseState to bs) in - โˆ™ needsUpkeep Base - โˆ™ [] โ‰ก filter (ฮป eb โ†’ isVoteCertified s eb ร— eb โˆˆแดฎ slice L slot 2) EBs - โˆ™ bs B.-โŸฆ B.SUBMIT (that ToPropose) / B.EMPTY โŸงโ‡€ bs' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ addUpkeep record s { BaseState = bs' } Base - - -- Protocol rules - - Roles : โˆ™ s โ† s' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - just s -โŸฆ SLOT / EMPTY โŸงโ‡€ s' diff --git a/formal-spec/Leios/VRF.agda b/formal-spec/Leios/VRF.agda deleted file mode 100644 index 6888d0363..000000000 --- a/formal-spec/Leios/VRF.agda +++ /dev/null @@ -1,61 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude -open import Leios.Abstract - -module Leios.VRF (a : LeiosAbstract) (let open LeiosAbstract a) where - -record VRF (Dom Range PubKey : Type) : Typeโ‚ where - field isKeyPair : PubKey โ†’ PrivKey โ†’ Type - eval : PrivKey โ†’ Dom โ†’ Range ร— VrfPf - verify : PubKey โ†’ Dom โ†’ Range โ†’ VrfPf โ†’ Type - -record LeiosVRF : Typeโ‚ where - field PubKey : Type - vrf : VRF โ„• โ„• PubKey - - open VRF vrf public - - -- transforming slot numbers into VRF seeds - field genIBInput genEBInput genVInput genV1Input genV2Input : โ„• โ†’ โ„• - - canProduceIB : โ„• โ†’ PrivKey โ†’ โ„• โ†’ VrfPf โ†’ Type - canProduceIB slot k stake ฯ€ = let (val , pf) = eval k (genIBInput slot) in val < stake ร— pf โ‰ก ฯ€ - - Dec-canProduceIB : โˆ€ {slot k stake} โ†’ (โˆƒ[ ฯ€ ] canProduceIB slot k stake ฯ€) โŠŽ (โˆ€ ฯ€ โ†’ ยฌ canProduceIB slot k stake ฯ€) - Dec-canProduceIB {slot} {k} {stake} with eval k (genIBInput slot) - ... | (val , pf) = case ยฟ val < stake ยฟ of ฮป where - (yes p) โ†’ injโ‚ (pf , p , refl) - (no ยฌp) โ†’ injโ‚‚ (ฮป ฯ€ (h , _) โ†’ ยฌp h) - - canProduceIBPub : โ„• โ†’ โ„• โ†’ PubKey โ†’ VrfPf โ†’ โ„• โ†’ Type - canProduceIBPub slot val k pf stake = verify k (genIBInput slot) val pf ร— val < stake - - canProduceEB : โ„• โ†’ PrivKey โ†’ โ„• โ†’ VrfPf โ†’ Type - canProduceEB slot k stake ฯ€ = let (val , pf) = eval k (genEBInput slot) in val < stake ร— pf โ‰ก ฯ€ - - Dec-canProduceEB : โˆ€ {slot k stake} โ†’ (โˆƒ[ ฯ€ ] canProduceEB slot k stake ฯ€) โŠŽ (โˆ€ ฯ€ โ†’ ยฌ canProduceEB slot k stake ฯ€) - Dec-canProduceEB {slot} {k} {stake} with eval k (genEBInput slot) - ... | (val , pf) = case ยฟ val < stake ยฟ of ฮป where - (yes p) โ†’ injโ‚ (pf , p , refl) - (no ยฌp) โ†’ injโ‚‚ (ฮป ฯ€ (h , _) โ†’ ยฌp h) - - canProduceEBPub : โ„• โ†’ โ„• โ†’ PubKey โ†’ VrfPf โ†’ โ„• โ†’ Type - canProduceEBPub slot val k pf stake = verify k (genEBInput slot) val pf ร— val < stake - - canProduceV : โ„• โ†’ PrivKey โ†’ โ„• โ†’ Type - canProduceV slot k stake = projโ‚ (eval k (genVInput slot)) < stake - - canProduceV1 : โ„• โ†’ PrivKey โ†’ โ„• โ†’ Type - canProduceV1 slot k stake = projโ‚ (eval k (genV1Input slot)) < stake - - Dec-canProduceV1 : โˆ€ {slot k stake} โ†’ Dec (canProduceV1 slot k stake) - Dec-canProduceV1 {slot} {k} {stake} with eval k (genV1Input slot) - ... | (val , pf) = ยฟ val < stake ยฟ - - canProduceV2 : โ„• โ†’ PrivKey โ†’ โ„• โ†’ Type - canProduceV2 slot k stake = projโ‚ (eval k (genV2Input slot)) < stake - - Dec-canProduceV2 : โˆ€ {slot k stake} โ†’ Dec (canProduceV2 slot k stake) - Dec-canProduceV2 {slot} {k} {stake} with eval k (genV2Input slot) - ... | (val , pf) = ยฟ val < stake ยฟ diff --git a/formal-spec/Leios/Voting.agda b/formal-spec/Leios/Voting.agda deleted file mode 100644 index b12e7bc5b..000000000 --- a/formal-spec/Leios/Voting.agda +++ /dev/null @@ -1,12 +0,0 @@ -{-# OPTIONS --safe #-} - -open import Leios.Prelude - -module Leios.Voting where - -record VotingAbstract (X : Type) : Typeโ‚ where - field VotingState : Type - initVotingState : VotingState - isVoteCertified : VotingState โ†’ X โ†’ Type - - โฆƒ isVoteCertifiedโ‡ โฆ„ : โˆ€ {vs x} โ†’ isVoteCertified vs x โ‡ diff --git a/formal-spec/StateMachine.agda b/formal-spec/StateMachine.agda deleted file mode 100644 index c8a2c3417..000000000 --- a/formal-spec/StateMachine.agda +++ /dev/null @@ -1,56 +0,0 @@ -{-# OPTIONS --safe #-} - -module StateMachine where - -open import Agda.Primitive using () renaming (Set to Type) - -open import Prelude.Init hiding (map) -open import Prelude.InferenceRules - -open import Class.Bifunctor - -private - variable S I O : Type - s s' s'' : S - i : I - is : List I - o : O - os : List O - STS : S โ†’ I โ†’ O โ†’ S โ†’ Type - -module _ (_-โŸฆ_/_โŸงโ‡€_ : S โ†’ I โ†’ O โ†’ S โ†’ Type) where - data _-โŸฆ_/_โŸง*โ‡€_ : S โ†’ List I โ†’ List O โ†’ S โ†’ Type where - - BS-base : - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆ [] / [] โŸง*โ‡€ s - - BS-ind : - โˆ™ s -โŸฆ i / o โŸงโ‡€ s' - โˆ™ s' -โŸฆ is / os โŸง*โ‡€ s'' - โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ - s -โŸฆ i โˆท is / o โˆท os โŸง*โ‡€ s'' - -ReflexiveTransitiveClosure = _-โŸฆ_/_โŸง*โ‡€_ - -data IdSTS {S} : S โ†’ โŠค โ†’ โŠค โ†’ S โ†’ Type where - Id-nop : IdSTS s _ _ s - -Invariant : (S โ†’ I โ†’ O โ†’ S โ†’ Type) โ†’ (S โ†’ Type) โ†’ Type -Invariant _-โŸฆ_/_โŸงโ‡€_ P = โˆ€ {s i o s'} โ†’ s -โŸฆ i / o โŸงโ‡€ s' โ†’ P s โ†’ P s' - -Total : (S โ†’ I โ†’ O โ†’ S โ†’ Type) โ†’ Type -Total _-โŸฆ_/_โŸงโ‡€_ = โˆ€ {s i} โ†’ โˆƒโ‚‚[ o , s' ] s -โŸฆ i / o โŸงโ‡€ s' - -STSโ‡’RTC : STS s i o s' โ†’ ReflexiveTransitiveClosure STS s (i โˆท []) (o โˆท []) s' -STSโ‡’RTC sts = BS-ind sts BS-base - -RTC-preserves-inv : โˆ€ {P} โ†’ Invariant STS P โ†’ Invariant (ReflexiveTransitiveClosure STS) P -RTC-preserves-inv inv (BS-base) = id -RTC-preserves-inv inv (BS-ind pโ‚ pโ‚‚) = RTC-preserves-inv inv pโ‚‚ โˆ˜ inv pโ‚ - -RTC-total : Total STS โ†’ Total (ReflexiveTransitiveClosure STS) -RTC-total SS-total {s} {[]} = ([] , s , BS-base) -RTC-total SS-total {s} {i โˆท is} = case SS-total of ฮป where - (o , s' , H) โ†’ case RTC-total SS-total of ฮป where - (os , s'' , H') โ†’ (o โˆท os , s'' , BS-ind H H') diff --git a/formal-spec/docs/leios-components-diag.tex b/formal-spec/docs/leios-components-diag.tex deleted file mode 100644 index 92da507b3..000000000 --- a/formal-spec/docs/leios-components-diag.tex +++ /dev/null @@ -1,42 +0,0 @@ -\documentclass{standalone} -\usepackage{tikz-uml} - -\definecolor{bleudefrance}{rgb}{0.19, 0.55, 0.91} -\definecolor{jasper}{rgb}{0.84, 0.23, 0.24} - -\begin{document} - \begin{tikzpicture} - \begin{umlpackage}{Leios} - \begin{umlcomponent}[x=0,y=0]{SpecStructure} - \umlbasiccomponent[x=-6,y=-4, fill=bleudefrance]{LeiosAbstract} - \umlbasiccomponent[y=0]{Blocks} - \umlbasiccomponent[y=-2, fill=bleudefrance]{Base Ledger} - \umlbasiccomponent[y=-4, fill=bleudefrance]{Key Registration Functionality} - \umlbasiccomponent[y=-6, fill=bleudefrance]{VRF Functionality} - \umlbasiccomponent[y=-8, fill=bleudefrance]{FFD Functionality} - - \umlassemblyconnector[with port] {LeiosAbstract}{Blocks} - \umlassemblyconnector[with port] {LeiosAbstract}{Base Ledger} - \umlassemblyconnector[with port] {LeiosAbstract}{Key Registration Functionality} - \umlassemblyconnector[with port] {LeiosAbstract}{VRF Functionality} - \umlassemblyconnector[with port] {LeiosAbstract}{FFD Functionality} - \end{umlcomponent} - - \begin{umlcomponent}[x=6,y=-1]{Protocol} - \umlbasiccomponent[x=2,y=0]{LeiosState} - \umlbasiccomponent[x=0,y=-2]{LeiosInput} - \umlbasiccomponent[x=4,y=-2]{LeiosOutput} - \end{umlcomponent} - - \begin{umlcomponent}[x=6,y=-6]{Simplified Leios} - \end{umlcomponent} - - \begin{umlcomponent}[x=10,y=-6]{Short-Pipeline Leios} - \end{umlcomponent} - - \umlassemblyconnector[with port] {SpecStructure}{Protocol} - \umlassemblyconnector[with port] {Protocol-south-port}{Simplified Leios-north-port} - \umlassemblyconnector[with port] {Protocol-south-port}{Short-Pipeline Leios-north-port} - \end{umlpackage} - \end{tikzpicture} -\end{document} diff --git a/formal-spec/docs/leios-state-transition-diag.tex b/formal-spec/docs/leios-state-transition-diag.tex deleted file mode 100644 index 701aa6a47..000000000 --- a/formal-spec/docs/leios-state-transition-diag.tex +++ /dev/null @@ -1,30 +0,0 @@ -\documentclass[tikz, border=3mm]{standalone} - -\tikzset{->, >=stealth, shorten >=2pt, shorten <=2pt, node distance=4cm } -\definecolor{bleudefrance}{rgb}{0.19, 0.55, 0.91} -\definecolor{jasper}{rgb}{0.84, 0.23, 0.24} - -\begin{document} -\begin{tikzpicture} - \node (init) [circle, draw, align=center] {LeiosState\\$slot_0$}; - \node[right of=init] (prev) [circle, draw, align=center, dotted] {LeiosState\\$slot_{n-1}$}; - \node[right of=prev] (focus) [circle, draw, align=center] {LeiosState\\$slot_n$}; - \node[right of=focus] (next) [circle, draw, align=center, dotted] {LeiosState\\$slot_{n+1}$}; - \node[right of=next] (last) [circle, draw=none, align=center] {}; - \draw[->] (init) edge node[above] {$\cdots$}(prev) [dotted]; - \draw[->] (prev) edge node[above] {Slot} (focus); - \draw[->] (focus) edge node[above] {Slot} (next); - \draw[->] (next) edge node[above] {} (last) [dotted]; - - \path[-stealth] (init) edge[out=45,in=135,looseness=5] node[above] {Init} (init); - \path[-stealth] (focus) edge[out=45,in=135,looseness=5, color=bleudefrance] node[above] {\textcolor{black}{IB Role}} (focus); - \path[-stealth] (focus) edge[out=45,in=135,looseness=10, color=bleudefrance] node[above] {\textcolor{black}{EB Role}} (focus); - \path[-stealth] (focus) edge[out=45,in=135,looseness=15, color=bleudefrance] node[above] {\textcolor{black}{Vote Role}} (focus); - \path[-stealth] (focus) edge[out=45,in=135,looseness=20, color=jasper] node[above] {\textcolor{black}{$Base_{2}$}} (focus); - \path[-stealth] (focus) edge[out=45,in=135,looseness=25, color=jasper, dashed] node[above] {\textcolor{black}{$Base_{1}$}} (focus); - \path[-stealth] (focus) edge[out=45,in=135,looseness=30, dashed] node[above] {\textcolor{black}{Ftch}} (focus); - \path[-stealth] (focus) edge[out=225,in=315,looseness=5] node[above] {\textcolor{black}{Not IB Role}} (focus); - \path[-stealth] (focus) edge[out=225,in=315,looseness=10] node[above] {\textcolor{black}{Not EB Role}} (focus); - \path[-stealth] (focus) edge[out=225,in=315,looseness=15] node[above] {\textcolor{black}{Not Vote Role}} (focus); -\end{tikzpicture} -\end{document} diff --git a/formal-spec/docs/overview.d2 b/formal-spec/docs/overview.d2 deleted file mode 100644 index 8c006cd5c..000000000 --- a/formal-spec/docs/overview.d2 +++ /dev/null @@ -1,110 +0,0 @@ -title: { - label: "Leios Formal Specification - Module Dependencies" - near: top-center - shape: text - style.font-size: 24 - style.bold: true -} - -# Styles -classes: { - module: { - style: { - stroke: "#2a2a2a" - fill: "#f5f5f5" - font-color: "#2a2a2a" - border-radius: 10 - shadow: true - } - } - core: { - style: { - stroke: "#2a2a2a" - fill: "#ffffff" - font-color: "#2a2a2a" - border-radius: 10 - stroke-width: 2 - } - } - abstract: { - style: { - stroke: "#2a2a2a" - fill: "#ffffff" - font-color: "#2a2a2a" - border-radius: 25 - stroke-dash: 5 - } - } -} - -# Core Abstract Modules -Abstract: { - class: abstract - label: "Leios.Abstract\n\nDefines core types and\nprotocol parameters" -} - -VRF: { - class: abstract - label: "Leios.VRF\n\nVerifiable Random\nFunction interface" -} - -FFD: { - class: abstract - label: "Leios.FFD\n\nFreshest First\nDelivery" -} - -# Implementation Modules -Blocks: { - class: module - label: "Leios.Blocks\n\nBlock structures and\nvalidation rules" -} - -Base: { - class: module - label: "Leios.Base\n\nBase chain\ninterface" -} - -Protocol: { - class: module - label: "Leios.Protocol\n\nCore protocol\nstate machine" -} - -KeyReg: { - class: module - label: "Leios.KeyRegistration\n\nKey registration\nfunctionality" -} - -# Protocol Variants -variants: { - class: core - label: "Protocol Variants" - - Simplified: { - class: module - label: "Leios.Simplified\n\nSimplified voting pipeline\nwith single voting phase" - } - - UniformShort: { - class: module - label: "Leios.UniformShort\n\nUniform short pipeline\nwith optimized voting" - } -} - -# Dependencies -Abstract -> VRF -Abstract -> FFD -Abstract -> Blocks -Abstract -> Base -Abstract -> KeyReg - -VRF -> Base -VRF -> KeyReg -VRF -> Protocol - -FFD -> Protocol -Blocks -> Protocol -Base -> Protocol -KeyReg -> Protocol - -Protocol -> variants.Simplified -Protocol -> variants.UniformShort diff --git a/formal-spec/docs/overview.png b/formal-spec/docs/overview.png deleted file mode 100644 index f6b9a688f..000000000 Binary files a/formal-spec/docs/overview.png and /dev/null differ diff --git a/formal-spec/leios-spec.agda-lib b/formal-spec/leios-spec.agda-lib deleted file mode 100644 index 04d720a0a..000000000 --- a/formal-spec/leios-spec.agda-lib +++ /dev/null @@ -1,9 +0,0 @@ -name: leios-spec -depend: - standard-library - standard-library-classes - standard-library-meta - abstract-set-theory - iog-prelude -include: - . diff --git a/nix/agda.nix b/nix/agda.nix index 0174e2d94..e7b5badc3 100644 --- a/nix/agda.nix +++ b/nix/agda.nix @@ -38,12 +38,12 @@ let src = fetchFromGitHub { repo = "stdlib-meta"; owner = "omelkonian"; - rev = "v2.1.1"; - sha256 = "qOoThYMG0dzjKvwmzzVZmGcerfb++MApbaGRzLEq3/4="; + rev = "480242a38feb948cafc8bcf673d057c04b0ed347"; + sha256 = "pa6Zd9O3M1d/JMSvnfgteAbDMgHyelQrR5xyibU0EeM="; }; meta = { }; libraryFile = "agda-stdlib-meta.agda-lib"; - everythingFile = "Main.agda"; + everythingFile = "standard-library-meta.agda"; buildInputs = [ agdaStdlib agdaStdlibClasses ]; }; diff --git a/nix/dummy-project/LICENSE b/nix/dummy-project/LICENSE deleted file mode 100644 index d44656eb0..000000000 --- a/nix/dummy-project/LICENSE +++ /dev/null @@ -1,30 +0,0 @@ -Copyright (c) 2024, Dummy - -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - - * Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - - * Redistributions in binary form must reproduce the above - copyright notice, this list of conditions and the following - disclaimer in the documentation and/or other materials provided - with the distribution. - - * Neither the name of Dummy nor the names of other - contributors may be used to endorse or promote products derived - from this software without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT -OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, -SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT -LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/nix/dummy-project/app/Main.hs b/nix/dummy-project/app/Main.hs deleted file mode 100644 index 65ae4a05d..000000000 --- a/nix/dummy-project/app/Main.hs +++ /dev/null @@ -1,4 +0,0 @@ -module Main where - -main :: IO () -main = putStrLn "Hello, Haskell!" diff --git a/nix/dummy-project/dummy-project.cabal b/nix/dummy-project/dummy-project.cabal deleted file mode 100644 index fa9527f86..000000000 --- a/nix/dummy-project/dummy-project.cabal +++ /dev/null @@ -1,25 +0,0 @@ -cabal-version: 3.0 -name: dummy-project -version: 0.1.0.0 --- synopsis: --- description: -license: BSD-3-Clause -license-file: LICENSE -author: Dummy -maintainer: Dummy --- copyright: -build-type: Simple -extra-doc-files: CHANGELOG.md --- extra-source-files: - -common warnings - ghc-options: -Wall - -executable dummy-project - import: warnings - main-is: Main.hs - -- other-modules: - -- other-extensions: - build-depends: base - hs-source-dirs: app - default-language: Haskell2010 diff --git a/nix/project.nix b/nix/project.nix index 006b06f28..032e7a18a 100644 --- a/nix/project.nix +++ b/nix/project.nix @@ -9,42 +9,14 @@ let isCross = pkgs.stdenv.hostPlatform != pkgs.stdenv.buildPlatform; in { - src = ./dummy-project; - + src = ../.; shell.withHoogle = false; - inputMap = { "https://chap.intersectmbo.org/" = inputs.iogx.inputs.CHaP; }; - name = "ouroboros-leios"; - - compiler-nix-name = lib.mkDefault "ghc96"; - - # flake.variants.profiled = { - # modules = [{ - # enableProfiling = true; - # enableLibraryProfiling = true; - # }]; - # }; - - # flake.variants.ghc928 = { - # compiler-nix-name = "ghc928"; - # }; - - # flake.variants.ghc8107 = { - # compiler-nix-name = "ghc8107"; - # }; - - modules = - [ - { - packages = { }; - } - { - packages = { }; - } - ]; + compiler-nix-name = lib.mkDefault "ghc98"; + # modules = [{ packages = { }; } { packages = { }; } ]; });