Merge #1506

1506: Fix cloneBlockchainTime r=nfrisby a=nfrisby

Fixes #1489. Fixes #1524.

Fixing Issue #1489 (let nodes lead when they join) and letting k vary in the
range [2 .. 10] since the dual-ledger tests do that now revealed several
Issues.

Issues in the library, not just the test infrastructure:

  * Issue #1505 -- `removeTxs` cannot use the fast path when validating after
    removing or else we might have dangling tx inputs references. Was fixed
    by #1565.

  * Issue #1511, bullet 1 (closed) -- The `Empty` cases in
    `prevPointAndBlockNo` were wrong. Recent PRs have addressed this: #1544 and
    #1589.

  * Issue #1543 (closed) -- A bracket in `registeredStream` was spoiled by an
    interruptible operation. Thomas' PR re-designed the vulnerability away. I
    think this is unrelated to the other changes; it was lurking and happened
    to pop up here just because I've been running hundreds of thousands of
    tests.

Issues only in the test infrastructure:

  * Issue #1489: let nodes lead when they join. This bug slipped in recently,
    when I added cloning of `BlockchainTime`s as part of the
    restarting/rekeying loop in the test infrastructure.

  * _PBFT reference simulator_. (Was masked by 1489.) Model competing 1-block
    chains in Ref.PBFT and use its results where applicable instead of the
    .Expectations module. Check that the PBFT threadnet and Ref.PBFT.simulate
    results agree on `Ref.Nominal` slots.

    The Ref.PBFT module had been making assumptions that were accurate given
    the guards in RealPBFT generators, given the `k >= n` regime. But outside
    of that regime, when the security parameter exceeds the node count, it
    wasn't enough. Also, it couldn't be compared against the PBFT threadnet
    because of those assumptions.

  * _PBFT reference simulator_. (Cascade of above.) Add
    `definitelyEnoughBlocks` to confirm the "at least k blocks in 2k slots"
    invariant in `genRealPBFTNodeJoinPlan`. The existing guards in the RealPBFT
    generators are intentionally insufficient by themselves; this way we can
    optimize them to avoid O(n^2) complexity without risking divergence from
    the `suchThat`s.

  * _Origin corner-case_. (Was masked by 1489.) Discard DualPBFT tests that
    forge in slot 0. The current `cardano-ledger-specs` doesn't allow for that.
    My hypothesis is that `cvsLastSlot` would need to be able to represent
    origin.

  * _Dlg cert tx_. Adjust `genNodeRekeys` to respect "If node X rekeys in slot
    S and Y leads slot S+1, then either the topology must connect X and Y
    directly, or Y must join before slot S."

  * _Dlg cert tx_. (Was (statistically?) masked by relatively large k.) Add
    `rekeyOracle` and use it to determine which epoch number to record in the
    dlg cert. The correct value depends on which block the dlg cert tx will end
    up in, not when we first add it to our mempool.

  * _Dlg cert tx_. (Was (statistically?) masked by relatively large k.) Add the
    dlg cert tx to the mempool each time the ledger changes.

Co-authored-by: Nicolas Frisby <nick.frisby@iohk.io>

ouroboros-consensus-byron/ouroboros-consensus-byron.cabal

@@ -79,7 +79,6 @@ test-suite test
                        Test.Consensus.Byron.Ledger
                        Test.ThreadNet.DualPBFT
                        Test.ThreadNet.RealPBFT
-                       Test.ThreadNet.Ref.RealPBFT
                        Test.ThreadNet.TxGen.Byron
 
                        Ouroboros.Consensus.ByronDual.Ledger

ouroboros-consensus-byron/test/Test/ThreadNet/DualPBFT.hs

@@ -57,6 +57,7 @@ import           Ouroboros.Consensus.ByronDual.Node
 
 import           Test.ThreadNet.General
 import qualified Test.ThreadNet.RealPBFT as RealPBFT
+import qualified Test.ThreadNet.Ref.PBFT as Ref
 import           Test.ThreadNet.TxGen
 import           Test.ThreadNet.Util
 import           Test.ThreadNet.Util.NodeRestarts
@@ -72,13 +73,45 @@ tests = testGroup "DualPBFT" [
 -- We limit it to 10 tests for now.
 prop_convergence :: SetupDualPBft -> Property
 prop_convergence setup = withMaxSuccess 10 $
+    (\prop -> if mightForgeInSlot0 then discard else prop) $
+    tabulate "Ref.PBFT result" [Ref.resultConstrName refResult] $
     prop_general
       (countByronGenTxs . dualBlockMain)
       (setupSecurityParam      setup)
-      (setupConfig             setup)
+      cfg
       (setupSchedule           setup)
+      (Just $ NumBlocks $ case refResult of
+         Ref.Forked{} -> 1
+         _            -> 0)
       (setupExpectedRejections setup)
+      1
       (setupTestOutput         setup)
+  where
+    cfg = setupConfig setup
+
+    refResult :: Ref.Result
+    refResult =
+      Ref.simulate (setupParams setup) (nodeJoinPlan cfg) (numSlots cfg)
+
+    -- The test infrastructure allows nodes to forge in slot 0; however, the
+    -- cardano-ledger-specs code causes @PBFTFailure (SlotNotAfterLastBlock
+    -- (Slot 0) (Slot 0))@ in that case. So we discard such tests.
+    --
+    -- This is ultimately due to the spec not modeling EBBs, while Byron
+    -- requires that successor of the genesis block is always the epoch 0 EBB.
+    -- As a result, the PBFT implementation tests the slot progression with
+    -- @<=@ to accomodate EBBs whereas the executable STS spec uses @<@.
+    mightForgeInSlot0 :: Bool
+    mightForgeInSlot0 = case refResult of
+      Ref.Forked _ m        -> any (0 `Set.member`) m
+      Ref.Nondeterministic  -> True
+      Ref.Outcomes outcomes -> case outcomes of
+        []    -> False
+        o : _ -> case o of
+          Ref.Absent  -> False
+          Ref.Nominal -> True
+          Ref.Unable  -> True
+          Ref.Wasted  -> True
 
 {-------------------------------------------------------------------------------
   Test setup
@@ -107,13 +140,13 @@ setupSchedule setup@SetupDualPBft{..} = Just $
 setupTestOutput :: SetupDualPBft -> TestOutput DualByronBlock
 setupTestOutput SetupDualPBft{..} =
     runTestNetwork setupConfig $ TestConfigBlock {
-        forgeEBB = Nothing -- spec does not model EBBs
-      , rekeying = Nothing -- TODO
-      , nodeInfo = \coreNodeId ->
-                      protocolInfoDualByron
-                        setupGenesis
-                        setupParams
-                        (Just coreNodeId)
+        forgeEbbEnv = Nothing -- spec does not model EBBs
+      , rekeying    = Nothing -- TODO
+      , nodeInfo    = \coreNodeId ->
+          protocolInfoDualByron
+            setupGenesis
+            setupParams
+            (Just coreNodeId)
       }
 
 -- | Override 'TestConfig'