Add leios-late-ib-inclusion to the Haskell simulator #413
Conversation
| , leiosLateIbInclusion :: Bool | ||
| -- ^ Whether an EB also includes IBs from the two previous iterations. | ||
| -- | ||
| -- TODO Merely one previous iteration if 'pipeline' is 'SingleVote'? |
There was a problem hiding this comment.
The Haskell simulator is configurable to use a single stage for voting (Vote) instead of two stages (VoteSend and VoteRecv).
The Short-to-Full spec only considers the two stage variant, when it specifies to include 3 iterations' IBs in each EB.
Would the Short-to-Full spec only include 2 iterations' IBs if Vote were a single stage? Should the Haskell simulator do that? @pagio @SupernaviX
There was a problem hiding this comment.
@nfrisby I don't think we care about supporting the behavior when leios-vote-send-recv-stages is false, we've been assuming the uniform leios variant for a long time.
nfrisby
force-pushed
the
nfrisby/issue-410-LateIbs
branch
3 times, most recently
from
e964fed to
a1c11f2
Compare
|
FYI, I did some force pushes that.
|
nfrisby
force-pushed
the
nfrisby/issue-410-LateIbs
branch
from
a1c11f2 to
18f5c46
Compare
| * Extends Leios so that EB producers include IBs directly from previous pipelines. | ||
| * Due to casuality, the EB must always include them, even if those IBs end up being | ||
| * certified in their own pipeline. | ||
| */ |
There was a problem hiding this comment.
Taking another look at the extension, the behavior you describe looks correct. It's also the behavior that the rust simulation follows. I don't know why I wrote this comment.
There was a problem hiding this comment.
Oh good .Yeah, I was confident it was nothing more than a typo 👍
There was a problem hiding this comment.
If it were IBs from more than 3 iterations, then we could start making decisions based on whether we see the EB certificate. However, it's not clear we'd want to do that even though we could.
nfrisby
force-pushed
the
nfrisby/issue-410-LateIbs
branch
from
18f5c46 to
310070d
Compare
nfrisby
force-pushed
the
nfrisby/issue-410-LateIbs
branch
from
305acdb to
1d826bf
Compare
|
I'm now expecting CI to build green. |
| | ibTable' <- shrinkList (const []) testSetup.ibTable | ||
| ] | ||
|
|
||
| test_leiosLateIbInclusion :: Test_leiosLateIbInclusion -> Property |
There was a problem hiding this comment.
Interesting use of an ad-hoc data type! I would have reached for two functions and forAllShrink, but this is something I see the first time and I think I like it.
There was a problem hiding this comment.
The "TestSetup data type" approach is something ouroboros-consensus has used since before I joined. I like it a lot.
| $ Q.counterexample ("on " <> show (map (.num) on)) | ||
| $ Q.counterexample | ||
| (unlines $ ("off" :) $ map (show . map (.num) . off) $ iterations) | ||
| $ on Q.=== concatMap off iterations |
There was a problem hiding this comment.
This is kind of testing using the implementation. Maybe other interesting properties to write here instead (e.g. using conjoin):
- When on, equal or more IBs are picked
- When on, the oldest IB is before stageStart of current - 2 * capL (not sure what functions we can use here)
- When off, all selected IBs are from the current pipeline
There was a problem hiding this comment.
Yes, that's true. I was very much thinking of the old behavior being correct, and "code review" being sufficient to establish that new code didn't change the old behavior.
But, to your point, the old behavior wasn't being tested.
On the other hand, I do think "the new behavior is just the union of the old behavior on three pipelines" is essentially the specification of this feature. So I like the test I've written here, but what's missing is a test for the old behavior, in my opinion.
| @@ -680,6 +686,26 @@ inputBlocksToEndorse cfg@LeiosConfig{pipeline = _ :: SingPipeline p} current buf | |||
| , receivedBy | |||
| } | |||
|
|
|||
| -- | Invokes 'inputBlocksToEndorse1' as many times as 'lateIbInclusion' | |||
There was a problem hiding this comment.
TODO this isn't going to work, since the IBs will have been pruned.
I'll need to relax the pruning logic
There was a problem hiding this comment.
TODO also, adoptEB as currently written isn't going to realize the IBs are already available, since it only looks in the relay buffer---and the node will not still be relaying these older IBs.
There was a problem hiding this comment.
TODO also shouldVoteOnEB only votes for EBs whose IBs all come from the same iteration.
|
I converted this to a Draft PR because my study of the whole simulator has turned up at least three reasons this current diff is insufficient (see #413 (comment)). |
| @@ -9,4 +10,5 @@ main = | |||
| defaultMain . testGroup "ouroboros-leios-sim" $ | |||
| [ Test.Topology.tests | |||
| , Test.Config.tests | |||
| , Test.ShortToFull.tests | |||
There was a problem hiding this comment.
I don't have a global enough understanding of the implementation's inclusion logic to fully assess this, but changes seem to have the basics correct.
I'd very much like it if we could cite the specs as comments in the Haskell and Rust code. That direct link would make reviews much easier. Our use of google docs is not aligned very well with this style of commenting/citation.
Closes #410.