Skip to content

Append-only list RA

Hai Dang requested to merge append_list into master

This closes #391. It depends on stdpp!239 (merged).

This adds an RA max_listR for lists where composition is only valid if one list is a prefix of the other, a derived RA mono_listR using auth that only allows lists to grow by appending, and a set of logic-level assertions for mono_list.

The logic-level assertions are:

  • an authoritative assertion for the full list
  • a persistent assertion for some list which is a prefix of the auth list
  • a persistent ownership that index i in the auth list is some particular value.

This, to my understanding after some inspection, should support the needs of the various versions mentioned in #391.

Edited by Hai Dang

Merge request reports