typed_z3

This module provides a type-level representation of various Z3 constructs, allowing us to define a type-safe interface for Z3, so that well-sortedness of expressions can be statically checked by tools for checking Python type annotations (e.g., mypy). Additionally, the various objects created by this module are transition-system-aware: they can be declared mutable, and produce "next" (post-state) versions of themselves. See examples below.

class Expr(z3.z3.ExprRef, abc.ABC):

A representation of a Z3 logical sort at the type-level. New type-safe sorts are defined by sub-classing this class (either directly or through the Finite, Enum classes).

An instance of the class represents a (transition-system) constant of this sort or a variable.

For example, we can declare a Ticket sort by writing:

class Ticket(Expr): ...

Note the ellipsis (...) are not a placeholder --- this is the literal code for defining a type-level sort.

To create a variable (equivalent to z3.Const) use:

t = Ticket("t")

To create a mutable constant use:

t = Ticket("t", mutable=True)

Note though that this is never needed when creating user-defined transition systems with ts.TransitionSystem.

next: Self

Get the post-state copy of a mutable constant.

The constant must be mutable.

Returns

Post-state copy of the constant.

Example:

service = Ticket("service", mutable=True)
service_next = service.next  # service'

def unchanged(self) -> z3.z3.BoolRef:

Return a formula expressing that a mutable constant is unchanged during a transition.

Returns

Formula expressing that the constant is unchanged.

Example:

service = Ticket("service", mutable=True)
service.unchanged()  # service' == service
# Same as: service.next == service

def update(self, val: Self) -> z3.z3.BoolRef:

Return a formula expressing that a mutable constant equals val in the post-state.

Parameters

val: The value the constant should equal in the post-state.

Returns

Formula expressing the update.

Example:

service = Ticket("service", mutable=True)
next_service = Ticket("next", mutable=True)
service.update(next_service)  # service' == next_service
# Same as: service.next == next_service

type Sort = type[Expr]

Any class derived from Expr.

class Bool(Expr):

Type-level Bool sort for transition-system symbols that operate with Booleans.

Known to be finite.

def neg(self) -> Self:

Type-safe version of z3.Not for type-level Bools.

Returns

Negated boolean value.

Inherited Members

Expr: next; unchanged; update

false: Bool = False

Type-safe equivalent and shorthand for z3.BoolVal(False).

true: Bool = True

Type-safe equivalent and shorthand for z3.BoolVal(True)

class Int(Expr):

Type-level Int sort for transition-system symbols that operate with integers.

Inherited Members

Expr: next; unchanged; update

class Finite(Expr, abc.ABC):

Subclass of Expr for defining sorts that are assumed by the user to be finite.

Example:

class Process(Finite): ...

This declares the Process sort as finite.

Inherited Members

Expr: next; unchanged; update

class Enum(Expr, abc.ABC):

Subclass of Expr for defining enumerated sorts. A type-level equivalent of z3.EnumSort.

Example:

class State(Enum):
    waiting: "State"
    critical: "State"
    neutral: "State"

Each field annotated with the class's type is one variant of the EnumSort, and can be accessed directly as a class field.

Example usage:

server_state = State("server_state", mutable=True)
server_state.update(State.waiting)  # server_state' == waiting

All sorts defined by subclasses of Enum are known to be finite.

Inherited Members

Expr: next; unchanged; update

class Fun(typing.Generic[typing.Unpack[Ts], T]):

A type-level representation of a z3.Function signature. It maintains well-sortedness, allowing to be called only with arguments of the correct sort, and producing a result of the correct sort.

Fun should not be instantiated directly. Instead, it should only be used as annotations inside transition systems (see ts.TransitionSystem).

Example:

class Process(Expr): ...
class Ticket(Expr): ...

has_ticket: Fun[Process, Ticket, Bool]
result = has_ticket(p, t)  # type-checked: p: Process, t: Ticket, result: Bool

def unchanged(self) -> z3.z3.BoolRef:

Return a universal formula expressing that for all inputs, the output of the function remains unchanged between the pre-state and the post-state.

Returns

Universal formula expressing the function is unchanged.

Example:

has_ticket: Fun[Process, Ticket, Bool]
has_ticket.unchanged()  # ForAll([Process1, Ticket2], has_ticket'(Process1, Ticket2) == has_ticket(Process1, Ticket2))

def update(self, places: Mapping[tuple[typing.Unpack[Ts]], T]) -> z3.z3.BoolRef:

Return a universal formula expressing that for all inputs, the output of the function remains unchanged between the pre-state and the post-state, except for inputs equal to keys of places, where the post-state function returns the matching value in places.

Parameters

places: Mapping of input tuples to new output values.

Returns

Universal formula expressing the function update.

Example:

has_ticket: Fun[Process, Ticket, Bool]
has_ticket.update({(p1, t1): true, (p2, t2): false})
# Updates has_ticket'(p1, t1) = true and has_ticket'(p2, t2) = false,
# all other values unchanged

class Rel(Fun[typing.Unpack[Ts], ], typing.Generic[typing.Unpack[Ts]]):

Type-level representation of relations, functions that return Booleans.

def update( self, places: Mapping[tuple[typing.Unpack[Ts]], z3.z3.BoolRef]) -> z3.z3.BoolRef:

Overrides Fun.update to allow arbitrary z3 formulas (z3.BoolRef) in updated values.

Parameters

places: Mapping of input tuples to new output formulas.

Returns

Universal formula expressing the relation update.

Inherited Members

Fun: unchanged

type BiRel = Rel[T, T]

Shorthand for declaring a binary relation.

class WFRel(Rel[T, T], typing.Generic[T]):

Binary relation, assumed by the user to be well-founded.