How to assert an operation is idempotent?

Questions
1

I have a toy model attached below that I’m using to introduce some concepts around CRDTs. Right now I’m trying to write a check like “sync is idempotent” but I’m having some trouble. I’m not actually sure how to express this! In words, I’d say “if sync happens two times in a row, the values do not change.” I’m not sure how to grab the value after the first sync but before the second one. Is that even the right way to approach this? I feel pretty stuck right now, even after reading through the spec for actions and searching around on the forums for various things. :grimacing:

enum Bool { True, False }

fun merge[a, b: Bool]: Bool {
  a = True implies True else b
}

check MergeIsCommutative {
  all a, b: Bool | merge[a, b] = merge[b, a]
}

check MergeIsAssociative {
  all a, b, c: Bool | merge[merge[a, b], c] = merge[a, merge[b, c]]
}

check MergeIsIdempotent {
  all a, b: Bool | merge[a, b] = merge[merge[a, b], b]
}

sig Document {
  var value: one Bool,
}

fun bool_not[b: Bool]: Bool {
  b = True implies False else True
}

pred flip[d: Document] {
  value' = value ++ d->bool_not[d.value]
}

pred sync[d1, d2: Document] {
  let merged = merge[d1.value, d2.value] {
    value' = value ++ (d1->merged + d2->merged)
  }
}

pred init {
  value = Document -> False
}

pred do_nothing {
  value' = value
}

fact traces {
  init
  always {
    do_nothing
    or (one d: Document | flip[d])
    or (some d1, d2: Document | sync[d1, d2])
  }
}
2

I’m also having trouble how to say that sync are associative and commutative… but I suspect the answer to any one of these will probably give me the answer for all of them.

3

I sat down again after lunch and maybe this is it?

check SyncIsIdempotent {
  always all d1, d2: Document {
    (sync[d1, d2]; sync[d1, d2]) implies value' = value''
  }
}

I think I’d read that “for all Documents d1 and d2, syncing twice means that value does not change.” But I’m still working on solidifying my understanding of temporal operators, so I’d appreciate if someone could double-check that. :sweat_smile:

It does fail in the way I’d expect if I break idempotence though (by changing the operation to XOR) so I suspect this may work at least well enough.

4

I think that is the correct way to check that sync is idempotent.

1 Like
5

great, thank you so much!

6

You can also specify this check by using only the events:

check SyncIsIdempotent {
  always all d1, d2: Document {
    (sync[d1, d2]; sync[d1, d2]) implies (sync[d1, d2]; do_nothing)
  }
}
7

Oooh, interesting. Does that mean you can “fork” the sequence of events? I didn’t think that was allowed.

8

No, there is no “fork” (time is linear) - this is the same as your version, but just reusing the stuttering event to avoid repeating all the unchanged constraints.

9

Oh, since the “do nothing” and “sync” predicates should look the same at that point? Got it.

1 Like