Behavioural properties in the Anoma specs

The Architecture 1 specification is still in need of behavioral properties that Anoma instances should satisfy. A specific property, in natural language, is

every transaction that user submits will be executed, eventually.

The notion of eventually here is exactly the one from linear temporal logic, assuming that we can fabricate suitable action alphabets. Another property that we would like is unlikability of nullifiers and their respective commitments, maybe via information theory? I just don’t know and that’s why I am writing this…

The purpose of this post is to get a rough delineation between properties that make it into Architecture 1 of the specs, say for Anoma v1, to get started; the delineation might just be two lists, one concerning well understood properties and others that are not yet understood in depth. In other words, I would like to make a collection of such behavioral properties, either in the narrow or wide sense. For the sake of this post, let me hand wave ‘narrow’ and ‘wide’ as follows:

  • narrow: we have an idea which theory would allow us to capture this property slickly, e.g., via differential privacy, information theory, temporal and/or epistemic logics, game theory / mechanism design;
  • wide: properties that are discussed very hot on twitter and social media, but so far have eluded the fangs of STEM, e.g., UX (for want of a better example that my brain refuses to produce right now) and maybe governance, but well, I am just desperate for good examples.

In short, this is just intended as condensation point for properties that have probably been discussed in several places, but never been collected in a single document. The post is a wiki, so please feel free to add properties to the two lists yourself, but I am happy to curate the list:

narrow:

  • inclusion fairness:

    • “every transaction candidate eventually is included in the mempool”
    • LTL
  • unbiased inclusion:

    • "every transaction candidate has a fair probability of being included next¨
    • some kind of Hyper LTL / CTL
  • state machine replication:

    • "under assumptions, Byzantine behavior of a part of the system is not affecting the good properties above¨
    • this requires that the abstraction level is low enough to talk about parts of the system

wide: