# How to assert an operation is idempotent?

**URL:** <https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405>\
**Category:** Questions\
**Created:** [October 6, 2023, 4:06pm UTC](https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405 "2023-10-06T16:06:57Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 6, 2023, 4:06pm UTC](https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405/1 "2023-10-06T16:06:57Z")

</div>

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. 😬

```plaintext
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])
  }
}

```

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 6, 2023, 6:25pm UTC](https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405/2 "2023-10-06T18:25:07Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 6, 2023, 6:29pm UTC](https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405/3 "2023-10-06T18:29:37Z")

</div>

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

```plaintext
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. 😅

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.

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [October 8, 2023, 6:56am UTC](https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405/4 "2023-10-08T06:56:24Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 9, 2023, 2:10pm UTC](https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405/5 "2023-10-09T14:10:03Z")

</div>

great, thank you so much!

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [October 10, 2023, 6:05am UTC](https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405/6 "2023-10-10T06:05:05Z")

</div>

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

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

```

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 10, 2023, 10:22am UTC](https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405/7 "2023-10-10T10:22:00Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [October 10, 2023, 2:22pm UTC](https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405/8 "2023-10-10T14:22:01Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 10, 2023, 3:03pm UTC](https://alloytools.discourse.group/t/how-to-assert-an-operation-is-idempotent/405/9 "2023-10-10T15:03:57Z")

</div>

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