Trait Protocol 

pub trait Protocol {
    type Public;

    // Required methods
    fn public(self) -> Self::Public;
    fn protocol(self) -> bool;
}

A variant of Invariant for use in AtomicInvariantSCs, AtomicInvariants and NonAtomicInvariants.

This allows specifying an invariant that depends on some public data (AtomicInvariantSC::public, AtomicInvariant::public, NonAtomicInvariant::public).

Required Associated Types

type Public

Required Methods

fn public(self) -> Self::Public

The public data of the invariant, derived from the inner content.

It is called public, because it is visible simply by holding the invariant, without needing to open it.

Because of this, calls to open must not modify this value.

logic

fn protocol(self) -> bool

The protocol for the invariant.

When opening the invariant (AtomicInvariantSC::open, AtomicInvariant::open, NonAtomicInvariant::open), the data in guaranteed to respect this protocol; then, you must ensure that it is still verified when the invariant is closed.

logic(prophetic)

Implementors