Initial trace verifier

flake.nix

@@ -7,9 +7,7 @@
       url = "github:input-output-hk/iogx";
     };
 
-    # Agda version 2.7
-    agda-nixpkgs.url = "github:NixOS/nixpkgs?ref=7438ebd9431243aa0b01502fae89c022e4facb0c";
-
+    leios-spec.url = "github:input-output-hk/ouroboros-leios-formal-spec?ref=ee654a42c81f1a2e6290ee13c9c6abcd03b30079";
   };
 
 

leios-trace-verifier/Makefile

@@ -0,0 +1,24 @@
+# Constants
+AGDA?=agda
+AGDA_RUN=$(AGDA) --transliterate
+OUT_DIR?=dist
+HS_DIR=$(OUT_DIR)/haskell
+MALONZO_DIR=MAlonzo/Code
+CABAL_TEST=cabal run test
+
+# Agda -> Haskell
+define agdaToHs
+    @echo "Generating $@"
+    $(eval CABAL_FILE=trace-parser.cabal)
+    $(eval HS_DIST=$(HS_DIR)/src)
+    mkdir -p $(HS_DIST)
+    cp -r hs-src/* $(HS_DIR)/
+    cp hs-src/$(CABAL_FILE) $(HS_DIR)/
+    $(AGDA_RUN) -c --ghc-dont-call-ghc --compile-dir $(HS_DIST) $<
+    find $(HS_DIST)/MAlonzo -name "*.hs" -print\
+      | sed "s#^$(HS_DIST)/#        #;s#\.hs##;s#/#.#g"\
+      >> $(HS_DIR)/$(CABAL_FILE)
+endef
+HS_LEIOS=$(HS_DIST)/$(MALONZO_DIR)/trace-parser.hs
+$(HS_LEIOS): trace-parser.agda
+	$(call agdaToHs,trace-parser)

leios-trace-verifier/Parser.agda

@@ -0,0 +1,88 @@
+open import Leios.Prelude hiding (id)
+
+module Parser where
+
+{-# FOREIGN GHC
+  {-# LANGUAGE OverloadedStrings #-}
+#-}
+
+open import Leios.Foreign.Defaults 2 fzero
+open import Leios.Foreign.Types hiding (EndorserBlock)
+
+{-# FOREIGN GHC
+  import Data.Word
+  import Data.Fixed
+  import Data.Map
+  import qualified Data.ByteString.Lazy.Char8 as BSL8
+  import LeiosEvents
+#-}
+
+postulate
+  Int : Set
+  Word64 : Set
+  Micro : Set
+  Map : Set → Set → Set
+
+{-# COMPILE GHC Word64 = type Data.Word.Word64 #-}
+{-# COMPILE GHC Micro = type Data.Fixed.Micro #-}
+{-# COMPILE GHC Map = type Data.Map.Map #-}
+{-# COMPILE GHC Int = type Int #-}
+
+Bytes = Word64
+SlotNo = Word64
+Time = Micro
+
+data NetworkAction : Type where
+  Sent Received : NetworkAction
+
+{-# COMPILE GHC NetworkAction = data NetworkAction (Sent | Received) #-}
+
+data BlockKind : Type where
+  IB EB VT RB : BlockKind
+
+{-# COMPILE GHC BlockKind = data BlockKind (IB | EB | VT | RB) #-}
+
+Node = String
+
+record BlockRef : Type where
+  field id : String
+
+{-# COMPILE GHC BlockRef = data BlockRef (BlockRef) #-}
+
+record Endorsement : Type where
+  field eb : BlockRef
+
+{-# COMPILE GHC Endorsement = data Endorsement (Endorsement) #-}
+
+data Event : Type where
+  Cpu : String → Time → String → Event
+
+  IBSent EBSent VTBundleSent RBSent IBReceived EBReceived VTBundleReceived RBReceived :
+    Maybe Node → Node → Maybe Bytes → Maybe Time → Maybe String → Maybe (List String) → Event
+
+  IBEnteredState EBEnteredState VTBundleEnteredState RBEnteredState : String → String → Word64 → Event
+
+  IBGenerated : String → String → SlotNo → Maybe Bytes → Maybe Bytes → Maybe String → Event
+
+  EBGenerated : String → String → Word64 → Word64 → List BlockRef → Event
+
+  RBGenerated : String → Maybe String → Maybe Int → Word64 → Maybe Word64 → Maybe Endorsement → Maybe (List Endorsement) → Maybe Word64 → Event
+
+  VTBundleGenerated : String → String → Word64 → Word64 → Map String Word64 → Event
+
+{-# COMPILE GHC Event = data Event (Cpu | IBSent | EBSent | VTBundleSent | RBSent | IBReceived | EBReceived | VTBundleReceived | RBReceived
+                                        | IBEnteredState | EBEnteredState | VTBundleEnteredState | RBEnteredState
+                                        | IBGenerated | EBGenerated | RBGenerated | VTBundleGenerated) #-}
+
+record TraceEvent : Type where
+  field time_s : Time
+        message : Event
+
+{-# COMPILE GHC TraceEvent = data TraceEvent (TraceEvent) #-}
+
+-- FIXME: Implementation
+verifyTrace : List TraceEvent → Bool
+verifyTrace [] = false
+verifyTrace (_ ∷ _) = true
+
+{-# COMPILE GHC verifyTrace as verifyTrace #-}

leios-trace-verifier/hs-src/app/Main.hs

@@ -0,0 +1,11 @@
+module Main where
+
+import LeiosEvents
+import Lib
+import Data.ByteString.Lazy as BSL
+
+logFile :: FilePath
+logFile = "leios-trace.log"
+
+main :: IO ()
+main = BSL.readFile logFile >>= print . verifyTrace . decodeJSONL

leios-trace-verifier/hs-src/src/Lib.hs

@@ -0,0 +1,6 @@
+module Lib (
+  module X,
+  module Lib,
+) where
+
+import MAlonzo.Code.Parser as X

leios-trace-verifier/hs-src/trace-parser.cabal

@@ -0,0 +1,56 @@
+cabal-version:      2.4
+name:               trace-parser
+version:            0.1.0.0
+synopsis:
+
+-- A longer description of the package.
+-- description:
+homepage:
+
+-- A URL where users can report bugs.
+-- bug-reports:
+license:            NONE
+author:             Yves Hauser
+maintainer:         [email protected]
+
+-- A copyright notice.
+-- copyright:
+-- category:
+
+common globalOptions
+    default-language: Haskell2010
+    build-depends:
+        base
+    default-extensions:
+        PolyKinds EmptyDataDecls EmptyCase ExistentialQuantification
+        ScopedTypeVariables NoMonomorphismRestriction RankNTypes
+        PatternSynonyms DeriveGeneric
+    ghc-options:
+        -Wno-overlapping-patterns
+
+executable parser
+    import: globalOptions
+    main-is: app/Main.hs
+    build-depends:
+      , base
+      , bytestring
+      , leios-trace-hs
+      , trace-parser
+
+  default-language: Haskell2010
+  ghc-options:      -Wall
+
+library
+    import: globalOptions
+    hs-source-dirs: src
+    exposed-modules: Lib
+    build-depends:
+      , aeson
+      , base
+      , bytestring
+      , containers
+      , text
+      , ieee
+      , leios-trace-hs
+-- This will be generated automatically when building with nix
+    other-modules:

leios-trace-verifier/trace-parser.agda

@@ -0,0 +1,3 @@
+module trace-parser where
+
+open import Parser

leios-trace-verifier/trace-parser.agda-lib

@@ -0,0 +1,10 @@
+name: trace-parser
+depend:
+  standard-library
+  standard-library-classes
+  standard-library-meta
+  abstract-set-theory
+  iog-prelude
+  leios-spec
+include:
+  .

nix/agda.nix

@@ -11,92 +11,31 @@ let
                      else "";
   };
 
-  customAgda = inputs.agda-nixpkgs.legacyPackages;
+  leiosSpec = inputs.leios-spec;
 
-  agdaStdlib = customAgda.agdaPackages.standard-library;
+  agdaIOGPrelude = leiosSpec.packages.agdaIOGPrelude;
+  agdaSets = leiosSpec.packages.agdaSets;
+  agdaStdlib = leiosSpec.packages.agdaStdlib;
+  agdaStdlibMeta = leiosSpec.packages.agdaStdlibMeta;
+  agdaStdlibClasses = leiosSpec.packages.agdaStdlibClasses;
+  agdaLeiosSpec = leiosSpec.packages.leiosSpec;
+  agdaWithDeps = leiosSpec.packages.agdaWithDeps;
 
-  agdaStdlibClasses = customAgda.agdaPackages.mkDerivation {
-    inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
-    pname = "agda-stdlib-classes";
-    version = "2.0";
-    src = fetchFromGitHub {
-      repo = "agda-stdlib-classes";
-      owner = "omelkonian";
-      rev = "2b42a6043296b4601134b8ab9371b37bda5d4424";
-      sha256 = "sha256-kTqS9p+jjv34d4JIWV9eWAI8cw9frX/K9DHuwv56AHo=";
-    };
-    meta = { };
-    libraryFile = "agda-stdlib-classes.agda-lib";
-    everythingFile = "standard-library-classes.agda";
-    buildInputs = [ agdaStdlib ];
-  };
-
-  agdaStdlibMeta = customAgda.agdaPackages.mkDerivation {
-    inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
-    pname = "agda-stdlib-meta";
-    version = "2.1.1";
-    src = fetchFromGitHub {
-      repo = "stdlib-meta";
-      owner = "omelkonian";
-      rev = "480242a38feb948cafc8bcf673d057c04b0ed347";
-      sha256 = "pa6Zd9O3M1d/JMSvnfgteAbDMgHyelQrR5xyibU0EeM=";
-    };
-    meta = { };
-    libraryFile = "agda-stdlib-meta.agda-lib";
-    everythingFile = "standard-library-meta.agda";
-    buildInputs = [ agdaStdlib agdaStdlibClasses ];
-  };
-
-  agdaSets = customAgda.agdaPackages.mkDerivation {
-    inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
-    pname = "agda-sets";
-    version = "2.1.1";
-    src = pkgs.fetchFromGitHub {
-      repo = "agda-sets";
-      owner = "input-output-hk";
-      rev = "f517d0d0c1ff1fd6dbac8b34309dea0e1aea6fc6";
-      sha256 = "sha256-OsdDNNJp9NWDgDM0pDOGv98Z+vAS1U8mORWF7/B1D7k=";
-    };
-    meta = { };
-    libraryFile = "abstract-set-theory.agda-lib";
-    everythingFile = "src/abstract-set-theory.agda";
-    buildInputs = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta ];
-  };
+  deps = [ agdaStdlib agdaStdlibMeta agdaStdlibClasses agdaSets agdaIOGPrelude agdaLeiosSpec ];
 
-  agdaIOGPrelude = customAgda.agdaPackages.mkDerivation {
+  traceParser = pkgs.agdaPackages.mkDerivation {
     inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
-    pname = "agda-prelude";
-    version = "2.0";
-    src = pkgs.fetchFromGitHub {
-      repo = "iog-agda-prelude";
-      owner = "input-output-hk";
-      rev = "e4f83fa59142baaad4944910217be05ebf6e2f22";
-      sha256 = "sha256-ytTOvz97lTHTiVdpmS3HUfTp/LH1Xey9bSh9zaBuacU=";
-    };
+    pname = "trace-parser";
+    name = "trace-parser";  # FIXME: Why is this entry needed?
+    src = ../trace-parser;
     meta = { };
-    libraryFile = "iog-prelude.agda-lib";
-    everythingFile = "src/Everything.agda";
-    buildInputs = [ agdaStdlib agdaStdlibClasses ];
-  };
-
-  deps = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta agdaSets agdaIOGPrelude ];
-
-  leiosSpec = customAgda.agdaPackages.mkDerivation {
-    inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
-    pname = "leios-spec";
-    name = "leios-spec";  # FIXME: Why is this entry needed?
-    src = ../formal-spec;
-    meta = { };
-    libraryFile = "formal-spec/leios-spec.agda-lib";
-    everythingFile = "Everything.agda";
+    libraryFile = "trace-parser.agda-lib";
+    everythingFile = "trace-parser.agda";
     buildInputs = deps;
   };
-
-  agdaWithPkgs = p: customAgda.agda.withPackages { pkgs = p; ghc = pkgs.ghc; };
-
 in
 {
-  inherit agdaStdlib agdaStdlibClasses agdaStdlibMeta agdaSets agdaIOGPrelude ;
-  agdaWithDeps = agdaWithPkgs deps;
-  leiosSpec = leiosSpec;
+  inherit agdaStdlib agdaStdlibMeta agdaStdlibClasses agdaSets agdaIOGPrelude agdaLeiosSpec;
+  agdaWithDeps = agdaWithDeps.withPackages { pkgs = deps; };
+  traceParser = traceParser;
 }