Migrate.destination_validated: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/transfer/Migrate.bend as Migrate
Lines 252-268 of mylsm-lsm-store@0.6.0.1/src/transfer/Migrate.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/Migrate.bend&start_line=252&end_line=268

import Base

# Marks the staged database verified only when count, digest, and order agree.
def destination_validated(
  state: Publication,
  counts: Nat & Nat,
  checks: Bool & Bool
) -> PublicationDecision:
  match state:
    case RecordsCopied{}:
      match counts:
        case (source_entries, destination_entries):
          match checks:
            case (digest_equal, canonical_order):
              Bool.pick(PublicationDecision,
                Nat.is_eq(source_entries, destination_entries) && digest_equal && canonical_order,
                PublicationAdvanced{DestinationValidated{}},
                PublicationRejected{})
    case _: PublicationRejected{}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/Migrate.bend&name=Publication
  https://jend.leeeet.dev/definition.txt?path=mylsm-lsm-store@0.6.0.1/src/transfer/Migrate.bend&name=PublicationDecision