proofs

This module contains the framework for proving temporal properties over transition systems. A temporal-property proof is a subclass of the Proof class, which, given a transition system (ts.TransitionSystem) and a temporal property (temporal.Prop), constructs the intersection transition system between the original system and the timer transition system for the negated property. Validity of the temporal property is then shown by proving termination of the intersection system with a rank function (constructed using implicit rankings).

When running an example you can turn on quiet mode, and only get the bottom line result by setting the environment variable QUIET to true:

make examples/ticket.py QUIET=true
class Proof(ts.BaseTransitionSystem, abc.ABC, typing.Generic[T]):

Base class for proving temporal properties over transition systems.

A proof constructs an intersection transition system between the original system and a timer transition system for the negated property. The temporal property is proven by showing termination of the intersection system using a rank function constructed with implicit rankings.

Subclasses must:

Example:

class Thread(Finite): ...

class System(TransitionSystem):
    waiting: Rel[Thread]

class WaitingProp(Prop[System]):
    def prop(self) -> BoolRef:
        return F(ForAll([t: Thread], Not(self.sys.waiting(t))))

class WaitingProof(Proof[System], prop=WaitingProp):
    @invariant
    def no_waiting_implies_termination(self) -> BoolRef:
        T = Thread("T")
        return ForAll(T, Not(self.sys.waiting(T)))

    def rank(self) -> Rank:
        return self.timer_rank(self.sys.waiting(self.sys.first), None, None)
@abstractmethod
def rank(self) -> ranks.Rank:

Return the ranking function for proving termination.

This method must be implemented by all subclasses. The returned rank is used to prove that the intersection transition system terminates, which in turn proves the temporal property.

The rank should be closed (no free parameters). Common rank constructors include timer_rank, BinRank, LexRank, PointwiseRank, and combinations thereof.

Returns

A ranks.Rank object that decreases on all fair execution paths.

Example:

class Thread(Finite): ...

class System(TransitionSystem):
    waiting: Rel[Thread]

class SysProof(Proof[System], prop=...):
    def rank(self) -> Rank:
        return self.timer_rank(self.sys.waiting(self.sys.first), None, None)

Example with multiple ranks:

class Thread(Finite): ...

class System(TransitionSystem):
    waiting: Rel[Thread]
    first: Immutable[Thread]
    second: Immutable[Thread]

class SysProof(Proof[System], prop=...):
    def rank(self) -> Rank:
        return PointwiseRank(
            self.timer_rank(self.sys.waiting(self.sys.first), None, None),
            self.timer_rank(self.sys.waiting(self.sys.second), None, None),
            LexRank(
                self.timer_rank(self.sys.some_condition(), None, None),
                self.timer_rank(self.sys.other_condition(), None, None)
            )
        )
def t(self, temporal_formula: z3.z3.BoolRef) -> timers.TimeFun:

Get the timer function associated with a temporal formula.

Parameters
Returns

The timer function for this temporal formula.

def timer_rank( self, phi: FormulaLike, alpha: FormulaLike | None, finite_lemma: ranks.FiniteLemma | None) -> ranks.Rank:

Create a timer-based rank from a formula.

Automatically calculates the timer for phi and returns a TimerRank. This is the recommended way to create timer-based ranks.

Parameters
  • phi: The formula to create a timer rank for.
  • alpha: Optional conditional formula. If provided, the rank is conditional.
  • finite_lemma: Optional lemma for proving finiteness.
Returns

A TimerRank that ranks by the timer for phi.

Example:

class Thread(Finite): ...

class System(TransitionSystem):
    waiting: Rel[Thread]

class SysProof(Proof[System], prop=...):
    def my_rank(self, t: Thread) -> Rank:
        return self.timer_rank(self.sys.waiting(t), None, None)
def timer_pos_in_order_rank(self, phi: FormulaLike) -> ranks.Rank:

Create a timer position-in-order rank from a formula.

Automatically calculates the timer for phi and returns a TimerPosInOrderRank. This can be used when more control is needed (over timer_rank).

Parameters
  • phi: The formula to create a timer rank for.
Returns

A TimerPosInOrderRank that ranks by the timer for phi.

Example:

class Thread(Finite): ...

class System(TransitionSystem):
    waiting: Rel[Thread]

class SysProof(Proof[System], prop=...):
    def my_rank(self, t: Thread) -> Rank:
        return self.timer_pos_in_order(self.sys.waiting(t))
def check(self, *, check_conserved: bool = False) -> bool:

Check all proof obligations for the temporal property.

Verifies:

  • System sanity (initial state and transitions are satisfiable)
  • Invariant inductiveness (invariants hold initially and are preserved)
  • Rank is closed (no free parameters)
  • Rank is conserved (optional, if check_conserved=True)
  • Rank decreases in all transitions
  • Soundness conditions hold
Parameters
  • check_conserved: If True, also check that the rank is conserved.
Returns

True if all checks pass, False otherwise.

Inherited Members
ts.BaseTransitionSystem
next
sanity_check
def system_invariant(fun: typing.Any | None = None, /, *, leaf: bool = False) -> Any:

Decorator for defining system invariants.

System invariants are proven over the original system (without timers). They must not contain temporal operators.

Parameters
  • fun: The invariant formula function (if used as decorator).
  • leaf: If True, mark as a leaf invariant (not used in proving other invariants).

Example:

class System(TransitionSystem):
    x: Int

class SysProof(Proof[System], prop=...):
    @system_invariant
    def x_non_negative(self) -> BoolRef:
        return self.sys.x >= 0

    @system_invariant(leaf=True)
    def x_bounded(self) -> BoolRef:
        return self.sys.x <= 100
def temporal_invariant(fun: typing.Any | None = None, /, *, leaf: bool = False) -> Any:

Decorator for defining temporal invariants.

Temporal invariants express properties about temporal formulas and timers. They are automatically converted to assertions that timers are zero.

Parameters
  • fun: The temporal invariant formula function (if used as decorator).
  • leaf: If True, mark as a leaf invariant (not used in proving other invariants).

Example:

class System(TransitionSystem):
    waiting: Rel[Thread]

class SysProof(Proof[System], prop=...):
    @temporal_invariant
    def eventually_not_waiting(self, t: Thread) -> BoolRef:
        return F(Not(self.sys.waiting(t)))
def invariant( fun: typing.Any | None = None, /, *, leaf: bool = False, omit_timer_axioms_in_init: bool = False) -> Any:

Decorator for defining invariants.

Invariants are proven over the intersection system (with timers). They express properties about the system state that are preserved across transitions. They must not contain temporal operators.

Parameters
  • fun: The invariant formula function (if used as decorator).
  • leaf: If True, mark as a leaf invariant (not used in proving other invariants).
  • omit_timer_axioms_in_init: If True, do not use the timer axioms when checking the invariant in init.

Example:

class Round(Finite): ...
class Value(Finite): ...

class System(TransitionSystem):
    proposal: Rel[Round, Value]

class SysProof(Proof[System], prop=...):
    @invariant
    def proposal_uniqueness(self, R: Round, V1: Value, V2: Value) -> BoolRef:
        return Implies(
            And(self.sys.proposal(R, V1), self.sys.proposal(R, V2)),
            V1 == V2
        )
def witness(fun: TypedProofFormula[T, W]) -> W:

Decorator for defining witnesses.

A witness provides an existential witness for a formula. The witness is a constant that can be used in invariants and ranks.

Parameters
  • fun: A formula function that takes exactly one parameter (the witness sort).

Example:

class Thread(Finite): ...

class System(TransitionSystem):
    waiting: Rel[Thread]

class SysProof(Proof[System], prop=...):
    @witness
    def waiting_thread(self, t: Thread) -> BoolRef:
        return self.sys.waiting(t)

    @invariant
    def witness_invariant(self) -> BoolRef:
        # self.waiting_thread is the witness constant
        return Not(self.sys.waiting(self.waiting_thread))
def temporal_witness(fun: TypedProofFormula[T, W]) -> W:

Decorator for defining temporal witnesses.

A temporal witness provides an existential witness for a temporal formula. The witness is a constant that can be used in invariants and ranks. Often used together with @track to ensure the temporal formula is tracked.

Parameters
  • fun: A temporal formula function that takes exactly one parameter (the witness sort).

Example:

class Round(Finite): ...
class Value(Finite): ...

class System(TransitionSystem):
    proposal: Rel[Round, Value]
    r0: Immutable[Round]

class SysProof(Proof[System], prop=...):
    @temporal_witness
    @track
    def eventually_proposed_value(self, V: Value) -> BoolRef:
        return F(self.sys.proposal(self.sys.r0, V))

    @invariant
    def witness_invariant(self) -> BoolRef:
        # self.eventually_proposed_value is the witness constant
        return self.sys.proposal(self.sys.r0, self.eventually_proposed_value)
def track( fun: TypedProofFormula[T, typing.Unpack[Ts]]) -> TypedProofFormula[T, typing.Unpack[Ts]]:

Decorator for marking temporal formulas to track.

Tracked formulas are used to create timers that are added to the timer transition system. This is useful for formulas that do not necessarily appear in the property but are needed for invariants.

Parameters
  • fun: The temporal formula function to track.

Example:

class System(TransitionSystem):
    waiting: Rel[Thread]

class SysProof(Proof[System], prop=...):
    @track
    def eventually_done(self, t: Thread) -> BoolRef:
        return F(Not(self.sys.waiting(t)))