Integrate anti-diff prototype in consensus packages

[jorisdral]

Description

Resolves #4010. This is a follow-up PR to #3997.

This PR integrates the anti-diff diff sequences in consensus. In addition to integration, this PR includes two major changes:

• Anti-diff invariants are now enforced through non-empty sequences.
• The DiffSeq datatype now checks more slot-related invariants.

The need for these changes only became apparent during integration. The invariants are now more heavily enforced, and should prevent misuse of the datatypes.

My advice is to look at the changes on a per-commit basis, which should make the diffs easier to parse.

Checklist

• Branch
  • Commit sequence broadly makes sense
  • Commits have useful messages
  • New tests are added if needed and existing tests are updated
  • If this branch changes Consensus and has any consequences for downstream repositories or end users, said changes must be documented in interface-CHANGELOG.md
  • If this branch changes Network and has any consequences for downstream repositories or end users, said changes must be documented in interface-CHANGELOG.md
  • If serialization changes, user-facing consequences (e.g. replay from genesis) are confirmed to be intentional.
• Pull Request
  • Self-reviewed the diff
  • Useful pull request description at least containing the following information:
    • What does this PR change?
    • Why these changes were needed?
    • How does this affect downstream repositories and/or end-users?
    • Which ticket does this PR close (if any)? If it does, is it linked?
  • Reviewer requested

[jasagredo]

Linked #3943 as WithoutLedgerTables becomes obsolete once this is merged

[jasagredo]

I am in general concerned that we are loosing the previous implementation. We might as well just delete the HD module right?

Would it be possible to unify the interface and define a CPP flag that switches implementations? Is it even worth? Ping @dnadales

[jasagredo]

I'm unsure why are these Eq constraints propagated if we are not comparing the values in the end?

[jorisdral]

Good catch, I will remove them again.

This might be a bit of tangent, but I was wondering if it is necessary to have this Rank-2 type here, and why we could not have k and v mentioned in the header of TableStuff. It's somewhat cumbersome that we have to add new constraints on k and v in pureLedgerTables every time we want to apply pureLedgerTables to some new function that places these additional constraints on k and v. Would that be an alternative, or would other parts of the code break?

[jorisdral]

Good catch, I will remove them again.

I was wrong. The constraints are there because there are other anti-diff functions that require the equality constraint, such as diff and the Semigroup, Monoid and Group instance functions.

[dnadales]

I wonder if we can remove some of the Eq constraints. For instance, does the patch below make sense? (ouroboros-consensus compiles with it, but I haven't tried the rest of the code, however, the question is rather about the purpose of the Eq constraint).

diff --git a/anti-diff/src/Data/Map/Diff/Strict.hs b/anti-diff/src/Data/Map/Diff/Strict.hs
index 0ea9cf480..e63cf065b 100644
--- a/anti-diff/src/Data/Map/Diff/Strict.hs
+++ b/anti-diff/src/Data/Map/Diff/Strict.hs
@@ -88,7 +88,7 @@ import           NoThunks.Class (NoThunks (..), noThunksInValues)
 -- @'DiffHistory'@ is non-empty. This prevents the @'Map'@ from getting bloated with
 -- empty diff histories.
 newtype Diff k v = Diff (Map k (NEDiffHistory v))
-  deriving stock (Generic, Show, Eq, Functor)
+  deriving stock (Generic, Show, Functor)
   deriving anyclass (NoThunks)
 
 -- | A history of changes to a value in a key-value store.
@@ -101,20 +101,20 @@ newtype UnsafeDiffHistory t v = UnsafeDiffHistory (t (DiffEntry v))
 
 deriving stock instance Show v => Show (UnsafeDiffHistory Seq v)
 deriving stock instance Show v => Show (UnsafeDiffHistory NESeq v)
-deriving stock instance Eq v => Eq (UnsafeDiffHistory Seq v)
-deriving stock instance Eq v => Eq (UnsafeDiffHistory NESeq v)
+-- deriving stock instance Eq v => Eq (UnsafeDiffHistory Seq v)
+-- deriving stock instance Eq v => Eq (UnsafeDiffHistory NESeq v)
 
 {-# COMPLETE DiffHistory #-}
 
 newtype DiffHistory v = MkDiffHistory (UnsafeDiffHistory Seq v)
-  deriving stock (Generic, Show, Eq, Functor)
+  deriving stock (Generic, Show, Functor)
   deriving newtype (NoThunks, Foldable)
 
 {-# COMPLETE NEDiffHistory #-}
 
 -- | A non-empty diff history.
 newtype NEDiffHistory v = MkNEDiffHistory (UnsafeDiffHistory NESeq v)
-  deriving stock (Generic, Show, Eq, Functor)
+  deriving stock (Generic, Show, Functor)
   deriving newtype (NoThunks, Foldable)
 
 pattern DiffHistory :: Seq (DiffEntry v) -> DiffHistory v
@@ -142,7 +142,7 @@ data DiffEntry v =
     | Delete !v
     | UnsafeAntiInsert !v
     | UnsafeAntiDelete !v
-  deriving stock (Generic, Show, Eq, Functor, Foldable)
+  deriving stock (Generic, Show, Functor, Foldable)
   deriving anyclass (NoThunks)
 
 {------------------------------------------------------------------------------
@@ -290,8 +290,17 @@ invertDiffEntry = \case
 --
 -- For simplicity, we simply compare the inverse of the first argument to the
 -- second argument. That is, inversion should be invertible.
+--
+-- TODO: we only use this in teststing code it seems. I wonder if we can make
+-- this def local.
 areInverses :: Eq v => DiffEntry v -> DiffEntry v -> Bool
-areInverses e1 e2 = invertDiffEntry e1 == e2
+areInverses (Insert x) (UnsafeAntiInsert y) = x == y
+  -- Delete x           -> UnsafeAntiDelete x
+  -- UnsafeAntiInsert x -> Insert x
+  -- UnsafeAntiDelete x -> Delete x
+
+
+-- e1 e2 = invertDiffEntry e1 == e2
 
 {------------------------------------------------------------------------------
   Values and keys
@@ -399,7 +408,7 @@ data ApplyDiffError k v =
   | BadDelMatchingKey k v v (NEDiffHistory v)
   | BadDelInsMatchingKey k v v v (NEDiffHistory v)
   | InsDelMatchingKey k v (NEDiffHistory v)
-  deriving (Show, Eq)
+  deriving (Show)
 
 -- | Applies a diff to values, performs sanity checks.
 --
diff --git a/ouroboros-consensus/src/Ouroboros/Consensus/Ledger/Basics.hs b/ouroboros-consensus/src/Ouroboros/Consensus/Ledger/Basics.hs
index a635f81f3..ec7e4296c 100644
--- a/ouroboros-consensus/src/Ouroboros/Consensus/Ledger/Basics.hs
+++ b/ouroboros-consensus/src/Ouroboros/Consensus/Ledger/Basics.hs
@@ -821,16 +821,16 @@ mapValuesAppliedMK f = \case
   ApplyQueryAllMK      -> ApplyQueryAllMK
   ApplyQuerySomeMK vs  -> ApplyQuerySomeMK (fmap f vs)
 
-instance (Ord k, Eq v) => Eq (ApplyMapKind' mk k v) where
-  ApplyEmptyMK          == _                     = True
-  ApplyKeysMK   l       == ApplyKeysMK   r       = l == r
-  ApplyValuesMK l       == ApplyValuesMK r       = l == r
-  ApplyTrackingMK l1 l2 == ApplyTrackingMK r1 r2 = l1 == r1 && l2 == r2
-  ApplyDiffMK l         == ApplyDiffMK r         = l == r
-  ApplySeqDiffMK l      == ApplySeqDiffMK r      = l == r
-  ApplyQueryAllMK       == ApplyQueryAllMK       = True
-  ApplyQuerySomeMK l    == ApplyQuerySomeMK r    = l == r
-  _                     == _                     = False
+-- instance (Ord k, Eq v) => Eq (ApplyMapKind' mk k v) where
+--   ApplyEmptyMK          == _                     = True
+--   ApplyKeysMK   l       == ApplyKeysMK   r       = l == r
+--   ApplyValuesMK l       == ApplyValuesMK r       = l == r
+--   ApplyTrackingMK l1 l2 == ApplyTrackingMK r1 r2 = l1 == r1 && l2 == r2
+--   ApplyDiffMK l         == ApplyDiffMK r         = l == r
+--   ApplySeqDiffMK l      == ApplySeqDiffMK r      = l == r
+--   ApplyQueryAllMK       == ApplyQueryAllMK       = True
+--   ApplyQuerySomeMK l    == ApplyQuerySomeMK r    = l == r
+--   _                     == _                     = False
 
 instance (Ord k, NoThunks k, NoThunks v) => NoThunks (ApplyMapKind' mk k v) where
   wNoThunks ctxt   = NoThunks.allNoThunks . \case
diff --git a/ouroboros-consensus/src/Ouroboros/Consensus/Storage/LedgerDB/HD/DiffSeq.hs b/ouroboros-consensus/src/Ouroboros/Consensus/Storage/LedgerDB/HD/DiffSeq.hs
index 82e502a85..559f88865 100644
--- a/ouroboros-consensus/src/Ouroboros/Consensus/Storage/LedgerDB/HD/DiffSeq.hs
+++ b/ouroboros-consensus/src/Ouroboros/Consensus/Storage/LedgerDB/HD/DiffSeq.hs
@@ -138,7 +138,7 @@ newtype DiffSeq k v =
       (InternalMeasure k v)
       (Element k v)
     )
-  deriving stock (Generic, Show, Eq)
+  deriving stock (Generic, Show)
   deriving anyclass (NoThunks)
 
 -- The @'SlotNo'@ is not included in the root measure, since it is
@@ -149,7 +149,7 @@ data RootMeasure k v = RootMeasure {
     -- | Cumulative diff
   , rmDiff   :: !(Diff k v)
   }
-  deriving stock (Generic, Show, Eq, Functor)
+  deriving stock (Generic, Show, Functor)
   deriving anyclass (NoThunks)
 
 data InternalMeasure k v = InternalMeasure {
@@ -173,7 +173,7 @@ data Element k v = Element {
     elSlotNo :: {-# UNPACK #-} !Slot.SlotNo
   , elDiff   ::                !(Diff k v)
   }
-  deriving stock (Generic, Show, Eq, Functor)
+  deriving stock (Generic, Show, Functor)
   deriving anyclass (NoThunks)
 
 -- | Length of a sequence of differences.

[dnadales]

The test suite will fail to compile with the patch above, but maybe the question is how to test the root measure semigroup laws without requiring a Eq constraint in the package that does not use them (only the test do).

test-storage/Test/Ouroboros/Storage/LedgerDB/HD/DiffSeq.hs:23:9: error:
    • No instance for (Eq (RootMeasure Key Val))
        arising from a use of ‘testSemigroupLaws’
    • In the expression: testSemigroupLaws
      In the second argument of ‘testGroupWithProxy’, namely
        ‘[testSemigroupLaws, testMonoidLaws, testGroupLaws]’
      In the expression:
        testGroupWithProxy
          (Proxy @(RootMeasure Key Val))
          [testSemigroupLaws, testMonoidLaws, testGroupLaws]
   |
23 |         testSemigroupLaws
   |         ^^^^^^^^^^^^^^^^^

[dnadales]

The patch I proposed will also break this:

src/Ouroboros/Consensus/Shelley/Ledger/Ledger.hs:269:10: error:
    • Could not deduce (Eq
                          (ApplyMapKind'
                             'Ouroboros.Consensus.Ledger.Basics.EmptyMK'
                             (SL.TxIn (Core.Crypto era))
                             (Core.TxOut era)))
        arising from the superclasses of an instance declaration
      from the context: ShelleyBasedEra era
        bound by the instance declaration
        at src/Ouroboros/Consensus/Shelley/Ledger/Ledger.hs:269:10-81
    • In the instance declaration for
        ‘TableStuff (LedgerState (ShelleyBlock proto era))’
    |
269 | instance ShelleyBasedEra era => TableStuff (LedgerState (ShelleyBlock proto era)) where

[dnadales]

What I don't get is why the Eq constraints that I removed are not needed in ouroboros-consensus, where the core logic of the LedgerDB is implemented, but they are needed by the clients.

[dnadales]

I hope you guys don't mind that I mark this as unresolved for now.

[dnadales]

Sorry for the extra noise. One important aspect that I overlooked is that at the moment you need the equality constraints to be able to invert values, eg:

areInverses :: Eq v => DiffEntry v -> DiffEntry v -> Bool
areInverses (Insert x) (UnsafeAntiInsert y) = x == y

So this means that we can only use anti-diffs with values that have an Eq instance, right? In that case that is an argument for keeping the old implementation around.

Coming back to the original question of this thread, I wonder if it'd be possible to re-engineer this in such a way that:

• define table stuff independently of the Eq constraint.
• if client code wants to use the anti-diff implementation they will need to provide these Eq instances.

[jasagredo]

The groupoid laws seem to fail on Hydra? https://hydra.iohk.io/build/19760053/nixlog/8

[jorisdral]

The groupoid laws seem to fail on Hydra? https://hydra.iohk.io/build/19760053/nixlog/8

You're right, and it should fail as far as I can tell with the current Arbitrary instances. I'll have to look into whether this is a bug or a feature

[jorisdral]

I am in general concerned that we are loosing the previous implementation. We might as well just delete the HD module right?

Would it be possible to unify the interface and define a CPP flag that switches implementations? Is it even worth? Ping @dnadales

If you consider it a risk to remove the previous implementation, we could keep it around for a while on the feature branch at least

[dnadales]

I am in general concerned that we are loosing the previous implementation. We might as well just delete the HD module right?
Would it be possible to unify the interface and define a CPP flag that switches implementations? Is it even worth? Ping @dnadales

If you consider it a risk to remove the previous implementation, we could keep it around for a while on the feature branch at least

I'd say we should keep HD around definitely during the prototyping phase. @jorisdral can you remind me if anti-diffs are guaranteed to exist for any choice of k v? If so I do not see a reason why we should keep the old implementation around afterwards.

[jorisdral]

I am in general concerned that we are loosing the previous implementation. We might as well just delete the HD module right?
Would it be possible to unify the interface and define a CPP flag that switches implementations? Is it even worth? Ping @dnadales

If you consider it a risk to remove the previous implementation, we could keep it around for a while on the feature branch at least

I'd say we should keep HD around definitely during the prototyping phase. @jorisdral can you remind me if anti-diffs are guaranteed to exist for any choice of k v? If so I do not see a reason why we should keep the old implementation around afterwards.

Anti-diffs are guaranteed to exist for any choice of k v (modulo some constraints like Ord)