lateIbInclusion flag from config

Author: yveshauser

flake.lock

@@ -7,7 +7,7 @@
       url = "github:input-output-hk/iogx";
     };
 
-      leios-spec.url = "github:input-output-hk/ouroboros-leios-formal-spec?rev=eff49274ed5e8dced0906cb6c7bff0f0bab1712d";
+      leios-spec.url = "github:input-output-hk/ouroboros-leios-formal-spec?rev=e39a1568e55f7c52b6419e7dec3c0ab63da83f15";
   };
 
 

flake.nix

@@ -99,6 +99,7 @@ data Config = Config
   , leiosStageActiveVotingSlots :: Word
   , leiosVoteSendRecvStages :: Bool
   , leiosVariant :: LeiosVariant
+  , leiosLateIbInclusion :: Bool
   , leiosHeaderDiffusionTimeMs :: DurationMs
   , praosChainQuality :: Double
   , txGenerationDistribution :: Distribution
@@ -171,6 +172,7 @@ instance Default Config where
       , leiosStageActiveVotingSlots = 1
       , leiosVoteSendRecvStages = False
       , leiosVariant = Short
+      , leiosLateIbInclusion = False
       , leiosHeaderDiffusionTimeMs = 1000
       , praosChainQuality = 40
       , txGenerationDistribution = Exp{lambda = 0.85, scale = Just 1000}
@@ -243,6 +245,7 @@ configToKVsWith getter cfg =
     , get @"treatBlocksAsFull" getter cfg
     , get @"cleanupPolicies" getter cfg
     , get @"leiosVariant" getter cfg
+    , get @"leiosLateIbInclusion" getter cfg
     , get @"leiosHeaderDiffusionTimeMs" getter cfg
     , get @"praosChainQuality" getter cfg
     , get @"simulateTransactions" getter cfg
@@ -329,6 +332,7 @@ instance FromJSON Config where
     treatBlocksAsFull <- parseFieldOrDefault @Config @"treatBlocksAsFull" obj
     cleanupPolicies <- parseFieldOrDefault @Config @"cleanupPolicies" obj
     leiosVariant <- parseFieldOrDefault @Config @"leiosVariant" obj
+    leiosLateIbInclusion <- parseFieldOrDefault @Config @"leiosLateIbInclusion" obj
     leiosHeaderDiffusionTimeMs <- parseFieldOrDefault @Config @"leiosHeaderDiffusionTimeMs" obj
     praosChainQuality <- parseFieldOrDefault @Config @"praosChainQuality" obj
     simulateTransactions <- parseFieldOrDefault @Config @"simulateTransactions" obj

leios-trace-hs/src/LeiosConfig.hs

@@ -104,13 +104,20 @@ record TraceEvent : Type where
 
 {-# COMPILE GHC TraceEvent = data TraceEvent (TraceEvent) #-}
 
-module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String ℕ)) (sl : ℕ) (eta : ℕ) where
+module _
+  (numberOfParties : ℕ)
+  (sutId : ℕ)
+  (stakeDistr : List (Pair String ℕ))
+  (stageLength : ℕ)
+  (ledgerQuality : ℕ)
+  (lateIBInclusion : Bool) -- TODO: Pass config and topology instead
+  where
 
   from-id : ℕ → Fin numberOfParties
   from-id n =
     case n <? numberOfParties of λ where
       (yes p) → #_ n {numberOfParties} {fromWitness p}
-      (no _) → error "Conversion to Fin not possible!"
+      (no _) → error $ "Conversion to Fin not possible! " ◇ show n ◇ " / " ◇ show numberOfParties
 
   nodePrefix : String
   nodePrefix = "node-"
@@ -119,13 +126,13 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String 
   SUT-id = from-id sutId
 
   instance
-    sl-NonZero : NonZero sl
-    sl-NonZero with sl ≟ 0
+    stageLength-NonZero : NonZero stageLength
+    stageLength-NonZero with stageLength ≟ 0
     ... | yes _ = error "Stage length is 0"
     ... | no ¬p = ≢-nonZero ¬p
 
-    np-NonZero : NonZero numberOfParties
-    np-NonZero with numberOfParties ≟ 0
+    numberOfParties-NonZero : NonZero numberOfParties
+    numberOfParties-NonZero with numberOfParties ≟ 0
     ... | yes _ = error "Number of parties is 0"
     ... | no ¬p = ≢-nonZero ¬p
 
@@ -137,8 +144,8 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String 
 
   open FunTot (completeFin numberOfParties) (maximalFin numberOfParties)
 
-  sd : TotalMap (Fin numberOfParties) ℕ
-  sd =
+  stakeDistribution : TotalMap (Fin numberOfParties) ℕ
+  stakeDistribution =
     let (r , l) = fromListᵐ (L.map (λ (x , y) → (nodeId x , y)) stakeDistr)
     in case (¿ total r ¿) of λ where
          (yes p) → record { rel = r ; left-unique-rel = l ; total-rel = p }
@@ -192,10 +199,10 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String 
         { networkParams =
             record
               { numberOfParties   = numberOfParties
-              ; eta               = eta
-              ; stakeDistribution = sd
-              ; stageLength       = sl
-              ; lateIBInclusion   = false
+              ; ledgerQuality     = ledgerQuality
+              ; stakeDistribution = stakeDistribution
+              ; stageLength       = stageLength
+              ; lateIBInclusion   = lateIBInclusion
               }
         ; sutId         = SUT-id
         ; winning-slots = fromList (L.catMaybes $ L.map winningSlot l)
@@ -385,7 +392,7 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String 
     unquoteDecl Show-LeiosInput    = derive-Show [ (quote LeiosInput , Show-LeiosInput) ]
 
     s₀ : LeiosState
-    s₀ = initLeiosState tt sd tt ((SUT-id , tt) ∷ [])
+    s₀ = initLeiosState tt stakeDistribution tt ((SUT-id , tt) ∷ [])
 
     format-Err-verifyAction :  ∀ {α i s} → Err-verifyAction α i s → Pair String String
     format-Err-verifyAction {α} {i} {s} (E-Err e) =

leios-trace-verifier/Parser.agda

@@ -22,16 +22,22 @@ main :: IO ()
 main =
   do
     Command{..} <- execParser commandParser
+
+    -- Prameters from topology
     (top :: Topology COORD2D) <- decodeFileThrow topologyFile
-    (config :: Config) <- decodeFileThrow configFile
     let nrNodes = toInteger $ Prelude.length (elems $ nodes top)
     let nodeNames = Prelude.map unNodeName (keys $ nodes top)
     let stakes = Prelude.map (toInteger . stake . nodeInfo) (elems $ nodes top)
     let stakeDistribution = Prelude.zip nodeNames stakes
+
+    -- Parameters from config
+    (config :: Config) <- decodeFileThrow configFile
     let stageLength = toInteger (leiosStageLengthSlots config)
-    let tau = 0 -- TODO: get tau from config
+    let ledgerQuality = ceiling (praosChainQuality config) -- TODO: int in schema?
+    let lateIBInclusion = leiosLateIbInclusion config
+
     result <-
-      verifyTrace nrNodes idSut stakeDistribution stageLength tau
+      verifyTrace nrNodes idSut stakeDistribution stageLength ledgerQuality lateIBInclusion
         . decodeJSONL
         <$> BSL.readFile logFile
     hPutStrLn stderr $ "Applying " <> show (fst result) <> " actions"