ranks

This module provides constructors for implicit rankings.

class Rank(abc.ABC):

Abstract base class for all ranking constructors.

A ranking constructor defines how to rank states in a transition system, typically used for proving termination or other liveness properties. Each rank has:

A spec defining free parameters
A conserved formula describing when the rank doesn't increase
A decreases formula describing when the rank decreases
A minimal formula describing minimal states
A condition for soundness checking

Example:

class Ticket(Expr): ...

class System(TransitionSystem):
    zero: Immutable[Ticket]
    service: Ticket

class SysProof(Proof[System], prop=...):
    def is_zero(self, t: Ticket) -> BoolRef:
        return t == self.sys.zero

    def my_rank(self) -> Rank:
        return BinRank(self.is_zero)

@dataclass(frozen=True)

class BinRank(Rank):

Binary implicit ranking constructor. Corresponds to a rank function that maps states where the formula alpha holds to 1 and states where it does not to 0.

Example:

class Ticket(Expr): ...
class System(TransitionSystem):
    zero: Immutable[Ticket]

class SysProof(Proof[System], prop=...):
    def my_formula(self, a: Ticket) -> BoolRef:
        return a == self.sys.zero

    def my_bin_rank(self) -> Rank:
        return BinRank(self.my_formula)  # rank with free variable "a"

alpha: ts.FormulaLike

Formula that determines when rank is 1 (True) vs 0 (False).

@dataclass(frozen=True)

class PosInOrderRank(Rank, typing.Generic[T]):

Position-in-order implicit ranking constructor.

Example:

class Index(Finite): ...

class System(TransitionSystem):
    lt: Immutable[Rel[Index, Index]]
    ptr: Index

class SysProof(Proof[System], prop=...):
    def my_pos_rank(self) -> Rank:
        return PosInOrderRank(self.sys.ptr, self.sys.lt)

term: TermLike[T]

Term representing the element whose position in the order is ranked.

order: RelLike[T, T]

Binary relation defining the order over elements.

@dataclass(frozen=True)

class CondRank(Rank):

Conditional rank. Uses rank when alpha is true, otherwise maps to minimum.

Example:

class Index(Finite): ...

class System(TransitionSystem):
    lt: Immutable[Rel[Index, Index]]
    ptr: Index

    waiting: Bool

class SysProof(Proof[System], prop=...):
    def my_cond_rank(self) -> Rank:
        return CondRank(PosInOrderRank(self.sys.ptr, self.sys.lt), self.sys.waiting)

rank: Rank

The inner rank used when condition is true.

alpha: ts.FormulaLike

Conditional formula: when true, use rank; when false, rank is minimal.

@dataclass(frozen=True)

class DomainPointwiseRank(Rank):

Domain-pointwise rank, decreases whenever the inner rank decreases for any tuple of elements (that we quantify over, see quant_spec).

Example:

class Thread(Finite): ...
class System(TransitionSystem):
    on: Rel[Thread]

class SysProof(Proof[System], prop=...):
    def is_on(self, t: Thread) -> BoolRef:
        return self.sys.on(t)

    def dom_pw_rank(self) -> Rank:
        return DomainPointwiseRank(BinRank(self.is_on), ParamSpec(t=Thread))

rank: Rank

The inner rank applied to each element in the quantified domain.

quant_spec: ts.ParamSpec

Parameters to quantify over (domain elements), removed from free parameters.

finite_lemma: FiniteLemma | None

Lemma for proving finiteness of the domain. Should be provided unless all sorts in quant_spec are declared finite.

decreases_hints: DomainPointwiseHints | None = None

Hints for instantiating the existential quantification over quant_spec.

@classmethod

def close( cls, rank: Rank, finite_lemma: FiniteLemma | None, decreases_hints: DomainPointwiseHints | None = None) -> Rank:

Shorthand for creating a DomainPointwiseRank that closes over all free variables in rank.

Example:

class Thread(Finite): ...
class System(TransitionSystem):
    on: Rel[Thread]

class SysProof(Proof[System], prop=...):
    def is_on(self, t: Thread) -> BoolRef:
        return self.sys.on(t)

    def dom_pw_rank(self) -> Rank:
        return DomainPointwiseRank.close(BinRank(self.is_on))

@dataclass(frozen=True)

class DomainLexRank(Rank):

Domain lexicographic ranking constructor.

Quantifies over a domain ordered by order, and uses lexicographic ordering based on the order relation. The inner rank is evaluated at all domain elements, ordered lexicographically.

Example:

class Thread(Finite): ...
class Ticket(Expr): ...

class System(TransitionSystem):
    ticket: Rel[Thread, Ticket]
    lt: Immutable[WFRel[Ticket]]

class SysProof(Proof[System], prop=...):
    def has_ticket(self, t: Thread, tick: Ticket) -> BoolRef:
        return self.sys.ticket(t, tick)

    def my_dom_lex_rank(self) -> Rank:
        return DomainLexRank(BinRank(self.has_ticket), self.sys.lt)

rank: Rank

The inner rank to apply at each domain element.

order: orders.OrderLike

The order relation over the domain elements.

finite_lemma: FiniteLemma | None = None

Lemma for proving finiteness if domain sorts are not declared finite.

conserved_hints: DomainLexConservedHints | None = None

Hints for instantiating conserved formulas.

decreases_hints: DomainLexDecreasesHints | None = None

Hints for instantiating decreases formulas.

@dataclass(frozen=True)

class LexRank(Rank):

Lexicographic combination of multiple ranks.

The rank decreases when the first rank decreases, or when the first rank is conserved and the second decreases, and so on. All ranks must use the same parameter specification.

Example:

class Index(Finite): ...

class System(TransitionSystem):
    lt: Immutable[Rel[Index, Index]]
    ptr1: Index
    ptr2: Index

class SysProof(Proof[System], prop=...):
    def my_lex_rank(self) -> Rank:
        rank1 = PosInOrderRank(self.sys.ptr1, self.sys.lt)
        rank2 = PosInOrderRank(self.sys.ptr2, self.sys.lt)
        return LexRank(rank1, rank2)

ranks: tuple[Rank, ...]

The component ranks combined lexicographically.

@dataclass(frozen=True)

class PointwiseRank(Rank):

Pointwise combination of multiple ranks.

The rank decreases when any component rank decreases (and all are conserved). All ranks must use the same parameter specification.

Example:

class Thread(Finite): ...
class System(TransitionSystem):
    on: Rel[Thread]

class SysProof(Proof[System], prop=...):
    def is_on(self, t: Thread) -> BoolRef:
        return self.sys.on(t)

    def my_pw_rank(self) -> Rank:
        rank1 = BinRank(lambda t: self.is_on(t))
        rank2 = BinRank(lambda t: Not(self.is_on(t)))
        return PointwiseRank(rank1, rank2)

ranks: tuple[Rank, ...]

The component ranks combined pointwise.

@dataclass(frozen=True)

class DomainPermutedRank(Rank):

Domain permuted ranking constructor.

Quantifies over domain elements and allows permutation of k pairs of elements. The rank decreases if there exists a permutation where the inner rank decreases.

Example:

class Thread(Finite): ...
class System(TransitionSystem):
    on: Rel[Thread]

class SysProof(Proof[System], prop=...):
    def is_on(self, t: Thread) -> BoolRef:
        return self.sys.on(t)

    def my_perm_rank(self) -> Rank:
        inner_rank = BinRank(self.is_on)
        return DomainPermutedRank(
            inner_rank,
            ParamSpec(t=Thread),
            k=2,  # allow permuting 2 pairs
            finite_lemma=None
        )

rank: Rank

The inner rank to apply.

quant_spec: ts.ParamSpec

The parameters to quantify over (domain elements).

k: int

Number of pairs of elements that can be permuted.

finite_lemma: FiniteLemma | None

Lemma for proving finiteness if domain sorts are not declared finite.

conserved_hints: DomainPermutedConservedHints | None = None

Hints for instantiating conserved formulas.

decreases_hints: DomainPermutedDecreasesHints | None = None

Hints for instantiating decreases formulas.

@dataclass(frozen=True)

class TimerRank(Rank):

Ranking constructor based on timer values.

Creates a rank from a timer term (of sort timers.Time). The rank decreases when the timer decreases, and is minimal when the timer is zero. If alpha is provided, the rank is conditional: it only applies when alpha is true, otherwise it's minimal.

This rank is typically used through proofs.Proof.timer_rank, which automatically creates timers from temporal formulas.

Example (using proofs.Proof.timer_rank method, recommended):

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

class SysProof(Proof[System], prop=...):
    def my_timer_rank(self, t: Thread) -> Rank:
        # Creates a timer rank from the formula
        return self.timer_rank(self.sys.waiting(t), None, None)

term: TermLike[timers.Time]

The timer term to rank by.

alpha: FormulaLike | None = None

Optional condition: when provided, rank is conditional on this formula.

finite_lemma: FiniteLemma | None = None

Lemma for proving finiteness if needed.

@dataclass(frozen=True)

class FiniteLemma:

Helper lemma for proving finiteness of sets.

Provides a formula beta that over-approximates elements that can be added to a set, and bounds the number of elements that can be added initially and in each transition.

Example:

class Thread(Finite): ...
class System(TransitionSystem):
    queue: Rel[Thread]

class SysProof(Proof[System], prop=...):
    def in_queue(self, t: Thread) -> BoolRef:
        return self.sys.queue(t)

    def finite_lemma(self) -> FiniteLemma:
        return FiniteLemma(
            beta=self.in_queue,
            m=2,  # at most 2 threads added initially and per transition
            init_hints=[...],  # optional hints
            tr_hints=[...]  # optional hints
        )

beta: ts.FormulaLike

Formula over-approximating added elements.

m: int = 1

Number of elements added initially and in each transition.

init_hints: FiniteSCHints | None = None

Hints for initial state finiteness check.

tr_hints: FiniteSCHints | None = None

Hints for transition finiteness check.