Properties #
Structural Properties #
There is a main difference with the unordered version of lists:
- these lists are sorted
- they accept a new operation
Insert.
So subtracing is not easy to define, but all reachable states of ordered list, there is an "equivalent" state reachable using unordered lists. In other words, there may be notions of simulations here, but not really useful for us, so we do not focus on that. We do not really need to prove it, since unoreded lists do not really have properties based on reachable states. In the case of needing this notions, we can think about something that enable us to define them, but it may just be easier to define and prove those properties at this level.
One thing that's required to add is that keys are unique. If not, we do not have nice properties like "connected lists" or deterministic traversals.
Axiomatized props were checked with Plausible (property-based testing) see
file List.SortedCheckProp.
Some properties require a lot of effort and they may be wrong (but fixable) so
we would like to have counter-examples.
When representing Ordered lists in Plausible, we employed an interval/skip list representation. To complete proving this module (i.e. removing all axioms), it may be a good idea to show that it is bisimilar/equivalent to range/interval lists.
Sorted #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Checked with Plausible
Reachable Statements #
Since Ordered lists have more requirements than Unordered lists, we have
properties requiring the use of the Ordered lists interface.
That is not every ListST is an instance of oredered lists.
Keys are unique.
No element is anchor of itself. Checked with Plausible.
If we have an anchor of a key, then the tokens are different.
List empty is empty
The following axioms stablishes a relationship between witnessing non membership and membership in Ordered Lists.
The intuition is high, and we just wrote Plausible tests to check them.
Check Test.MidgardLists.SimProp.split_tokens.
Witnessing non-membership locally implies not membership globally. This is a propetry of well-built ordered lists.
Same as before, but unfolded membership
Enabled/Disable Prop #
Insert Properties #
We can always insert elements that are not in the list
Same as before but using the relation instead of the computation
Inserted then non_member
In Midgard Ordered Lists, we have membership and non-membership local checks and they behave properly. We need to be sure we are using the ordered lists.
We cannot insert an element for which we have a witness proving its inclusion.
We can prove that since there are no dups, this should be trivial, but here I am
testing the model itself.
When running, the model could be wrong, and we only have is_member operations.
The key just inserted is in the list and the witness is the just created token.
Inserting element iff
After inserting, we (at least) keep the keys that were before.
All keys that are in the list after inserting are in the previous list but the key just inserted.
We can always remove elments with an anchor.
Ordered Remove unordered removes an element. This is mainly to reuse all removes properties.
Remove removes the element.
See PoC/Blaster.lean
The element removed is not an element of the list anymore.
Element in the list after removing an elements are elements of the original list
Enable remove but its computational part instead of using the relation.