TOSPLIT fixup IB lifetimes

LateIbInclusion requires keeping IBs around two stages longer for building EBs
and Votes correctly.

This highlighted the fact that the simulator had been diffusing IBs for longer
than it should, since it had been reusing the relay buffer for building Votes
correctly.

This mega-commit does several things.

- Renames `shouldIgnore` to `shouldNotRequest` in order to emphasize that
  `shouldIgnore` only prevents late requests, not late arrivals. (Actually
  either late or early.)
- IBs now stop diffusing when they should, ie after Endorse. Also, the
  `shouldNotRequest` logic for the relay buffer is simpler: just discard IBs
  that would be late if they diffused now. (Actually either late or early.)
- Discards IBs that arrived too late, instead of processing them anyway.
- Introduces a state variable `iBsForEBsAndVotesVar` dedicating to remembering
  IBs even after they stop diffusing, since building EBs and Votes requires
  information about such IBs.
- Only records a classification `IbDeliveryStage` of when an IB arrived,
  instead of recording the low-level `UTCTime`.
- Simplified the logic for choosing&judging IBs within EBs using the new
  `IbDeliveryStage` classification.
- The node no longer ignores certificates when building an RB if it doesn't
  already have all of the IBs the certificate transitively includes---that rule
  is not in the Short Leios specification.

Author: nfrisby

simulation/src/LeiosProtocol/Relay.hs

@@ -498,7 +498,7 @@ data SubmitPolicy = SubmitInOrder | SubmitAll
 
 data RelayConsumerConfig id header body m = RelayConsumerConfig
   { relay :: !RelayConfig
-  , shouldIgnore :: m (header -> Bool)
+  , shouldNotRequest :: m (header -> Bool)
   -- ^ headers to ignore, e.g. already received or coming too late.
   , validateHeaders :: [header] -> m ()
   , headerId :: !(header -> id)
@@ -761,7 +761,7 @@ relayConsumerPipelined config sst =
     if (min (Map.size lst0.available) (fromIntegral config.maxBodiesToRequest)) == 0
       then return (Left lst0)
       else return . Right . TS.Effect $ do
-        isIgnored <- config.shouldIgnore
+        isIgnored <- config.shouldNotRequest
         atomically $ do
           -- New headers are filtered before becoming available, but we have
           -- to filter `lst.available` again in the same STM tx that sets them as
@@ -987,7 +987,7 @@ relayConsumerPipelined config sst =
     m (RelayConsumerLocalState id header body n)
   acknowledgeIds lst idsSeq _ | Seq.null idsSeq = pure lst
   acknowledgeIds lst idsSeq idsMap = do
-    isIgnored <- config.shouldIgnore
+    isIgnored <- config.shouldNotRequest
     inFlight <- readTVarIO sst.inFlightVar
 
     let lst1 =

simulation/src/LeiosProtocol/Short.hs

@@ -467,21 +467,37 @@ isStage cfg stage slot = fromEnum slot >= cfg.sliceLength * fromEnum stage
 newtype PipelineNo = PipelineNo Word64
   deriving (Bounded, Enum, Show, Eq, Ord)
 
+pipelineMonus :: PipelineNo -> Word64 -> PipelineNo
+pipelineMonus (PipelineNo w) i = PipelineNo $ w - min w i
+
 stageRangeOf :: forall p. IsPipeline p => LeiosConfig -> PipelineNo -> Stage p -> (SlotNo, SlotNo)
 stageRangeOf cfg pl stage =
   fromMaybe
     undefined
     (stageRange cfg minBound (toEnum (fromEnum pl * cfg.sliceLength)) stage)
 
+-- | WARNING This fails if the slot is earlier than the beginning of the stage
+-- in the first iteration (ie @'PipelineNo' 0@)
 pipelineOf :: forall p. IsPipeline p => LeiosConfig -> Stage p -> SlotNo -> PipelineNo
 pipelineOf cfg stage sl =
-  toEnum $
-    fromMaybe undefined (fromEnum <$> stageStart cfg stage sl minBound)
-      `div` cfg.sliceLength
+    maybe err cnv $ stageStart cfg stage sl minBound
+  where
+    cnv = toEnum . (`div` cfg.sliceLength) . fromEnum
+
+    err = error $ show (cfg.sliceLength, x, stage, sl)
+
+    x :: String
+    x = case cfg of LeiosConfig{pipeline} -> case pipeline of
+                      SingSingleVote -> "SingleVote"
+                      SingSplitVote -> "SplitVote"
 
 forEachPipeline :: (forall p. Stage p) -> (forall p. IsPipeline p => Stage p -> a) -> [a]
 forEachPipeline s k = [k @SingleVote s, k @SplitVote s]
 
+lastEndorse :: LeiosConfig -> PipelineNo -> SlotNo
+lastEndorse leios@LeiosConfig{pipeline = _ :: SingPipeline p} pipelineNo =
+  snd $ stageRangeOf @p leios pipelineNo Endorse
+
 lastVoteSend :: LeiosConfig -> PipelineNo -> SlotNo
 lastVoteSend leios@LeiosConfig{pipeline} pipelineNo = case pipeline of
   SingSingleVote -> snd (stageRangeOf leios pipelineNo Vote)
@@ -663,48 +679,71 @@ data EndorseBlocksSnapshot = EndorseBlocksSnapshot
   , certifiedEndorseBlocks :: (PipelineNo, PipelineNo) -> [(PipelineNo, [(EndorseBlock, Certificate, UTCTime)])]
   }
 
+-- | In which contemporary stage was an IB delivered
+data IbDeliveryStage =
+    IbDuringProposeOrDeliver1
+    -- ^ The node will not vote for an EB that excludes IBs that arrived during
+    -- Propose or Deliver1.
+    --
+    -- The node will include IBs that arrived during Propose or Deliver1 in an
+    -- EB it makes.
+  |
+    IbDuringDeliver2
+    -- ^ The node will include IBs that arrived during Deliver2 in an EB it makes.
+  |
+    IbDuringEndorse
+    -- ^ The node will not vote for an EB that includes IBs that arrived later
+    -- than Endorse.
+  deriving (Bounded, Enum, Eq, Ord, Show)
+
 -- | Both constraints are inclusive.
 data InputBlocksQuery = InputBlocksQuery
-  { generatedBetween :: (SlotNo, SlotNo)
-  , receivedBy :: SlotNo
+  { generatedBetween :: (PipelineNo, PipelineNo)
+  , receivedBy :: IbDeliveryStage
   -- ^ This is checked against time the body is downloaded, before validation.
   }
 
-inputBlocksToEndorse1 ::
-  LeiosConfig ->
-  -- | current slot
-  SlotNo ->
-  InputBlocksSnapshot ->
-  [InputBlockId]
-inputBlocksToEndorse1 cfg@LeiosConfig{pipeline = _ :: SingPipeline p} current buffer = fromMaybe [] $ do
-  generatedBetween <- stageRange @p cfg Endorse current Propose
-  receivedBy <- stageEnd @p cfg Endorse current Deliver2
-  pure $
-    buffer.validInputBlocks
-      InputBlocksQuery
-        { generatedBetween
-        , receivedBy
-        }
+ibWasDeliveredLate :: LeiosConfig -> SlotConfig -> SlotNo -> UTCTime -> Bool
+ibWasDeliveredLate cfg slotCfg sl deliveryTime =
+  case ibDeliveryStage cfg slotCfg sl deliveryTime of
+    Nothing -> True
+    Just{} -> False
+
+ibDeliveryStage :: LeiosConfig -> SlotConfig -> SlotNo -> UTCTime -> Maybe IbDeliveryStage
+ibDeliveryStage
+    cfg@LeiosConfig {pipeline = _ :: SingPipeline p}
+    slotCfg
+    ibSlot
+    deliveryTime
+  | before loPropose = Nothing   -- TODO future blocks?
+  | before loDeliver2 = Just IbDuringProposeOrDeliver1
+  | before loEndorse = Just IbDuringDeliver2
+  | before (succ hiEndorse) = Just IbDuringEndorse
+  | otherwise = Nothing   -- TODO late blocks?
+  where
+    p = pipelineOf @p cfg Propose ibSlot
+
+    before sl = deliveryTime < slotTime slotCfg sl
+
+    (loPropose, _) = stageRangeOf @p cfg p Propose
+    (loDeliver2, _) = stageRangeOf @p cfg p Deliver2
+    (loEndorse, hiEndorse) = stageRangeOf @p cfg p Endorse
 
--- | Invokes 'inputBlocksToEndorse1' as many times as 'lateIbInclusion'
--- requires
 inputBlocksToEndorse ::
   LeiosConfig ->
   -- | current slot
   SlotNo ->
   InputBlocksSnapshot ->
   [InputBlockId]
-inputBlocksToEndorse cfg current buffer =
-  concatMap each iterations
- where
-  each sl = inputBlocksToEndorse1 cfg sl buffer
-  capL = fromIntegral cfg.sliceLength
-  iterations =
-    if not cfg.lateIbInclusion
-      then [current]
-      else
-        -- discard underflows
-        dropWhile (> current) [current - 2 * capL, current - capL, current]
+inputBlocksToEndorse cfg@LeiosConfig{pipeline = _ :: SingPipeline p} current buffer =
+    let hi = pipelineOf @p cfg Endorse current in
+            let lo = if cfg.lateIbInclusion then pipelineMonus hi 2 else hi
+            in
+            buffer.validInputBlocks
+              InputBlocksQuery
+                { generatedBetween = (lo, hi)
+                , receivedBy = IbDuringDeliver2
+                }
 
 -- | Returns possible EBs to reference from current pipeline EB.
 endorseBlocksToReference ::
@@ -760,21 +799,24 @@ shouldVoteOnEB ::
 shouldVoteOnEB cfg@LeiosConfig{voteSendStage} _ slot _buffers _
   -- checks whether a pipeline has been started before.
   | Nothing <- stageRange cfg voteSendStage slot Propose = const False
-shouldVoteOnEB cfg@LeiosConfig{voteSendStage} slotConfig slot buffers ebuffers = cond
+shouldVoteOnEB cfg@LeiosConfig{voteSendStage = voteSendStage :: Stage p} slotConfig slot buffers ebuffers = cond
  where
-  generatedBetween = fromMaybe (error "impossible") $ stageRange cfg voteSendStage slot Propose
+  generatedBetween = (lo, hi)
+    where
+      hi = pipelineOf @p cfg voteSendStage slot
+      lo = if cfg.lateIbInclusion then pipelineMonus hi 2 else hi
   receivedByEndorse =
     buffers.validInputBlocks
       InputBlocksQuery
         { generatedBetween
-        , receivedBy = fromMaybe (error "impossible") $ stageEnd cfg voteSendStage slot Endorse
+        , receivedBy = IbDuringEndorse
         }
   receivedByDeliver1 = buffers.validInputBlocks q
    where
     q =
       InputBlocksQuery
         { generatedBetween
-        , receivedBy = fromMaybe (error "impossible") $ stageEnd cfg voteSendStage slot Deliver1
+        , receivedBy = IbDuringProposeOrDeliver1
         }
   -- Order of references in EndorseBlock matters for ledger state, so we stick to lists.
   -- Note: maybe order on (slot, subSlot, vrf proof) should be used instead?