Input language

Lambda reads a profile of VMT-LIB: standard SMT-LIB 2 with annotations that mark the parts of a transition system, extended for parameterized systems. The main extension is that state variables can be functions from uninterpreted index sorts into a codomain, and formulas can quantify over the index sorts. Lambda checks that a safety property holds for every cardinality of the index sorts.

The model

A system consists of:


index sorts	uninterpreted sorts, `(declare-sort Process 0)`; the parameters of the system
state variables	functions from index sorts into a codomain, each paired with a next-state copy
rigid symbols	constants, functions and relations that never change (topologies, quorums, orders)
inputs	constants that take a fresh value at every step
initial formula	the initial states
transition formula	`T = (⋁ actions) ∧ (⋀ trans constraints)`
axioms	background assumptions that hold in every state
property	the safety property to prove

Sorts

Quantifiers range over the index sorts only, never over integers or reals; any nesting and alternation of ∀ and ∃ is allowed. The codomain of a state variable or rigid function is one of:

Bool;
Int or Real, with linear arithmetic;
an enumeration, declared with nullary constructors: (declare-datatypes ((Color 0)) (((red) (green) (blue))));
an index sort, for example a successor function next : node → node.

Index sorts and enumerations support equality only. Bit-vectors, strings, the SMT array theory and non-enumerative datatypes are not supported; use functions from index sorts instead of arrays.

Symbols

State variables are declared as a pair of symbols, the current and the next copy, tied by annotating the current one with :next. A state variable of arity 0 is a scalar:

(declare-fun Ticket (Process) Int)
(declare-fun Ticket.next (Process) Int)
(define-fun Ticket.sv ((p Process)) Int (! (Ticket p) :next Ticket.next))

Rigid symbols of any arity are marked with :global (or :rigid true):

(declare-fun member (node quorum) Bool)
(define-fun member.sv ((n node) (q quorum)) Bool (! (member n q) :global true))

A symbol without :next and without :global is rigid if its arity is at least 1, and an input if it is a constant: it then takes an unconstrained value at every step, for example the time elapsed by a transition. A constant that must keep its value has to be marked :global.

Formulas

Annotation	Meaning
`:init true`	initial states (no next-state symbols); several are conjoined
`:action NAME`	a transition rule; the actions are the disjuncts of the transition formula
`:trans true`	a two-state constraint that holds on every step; several are conjoined
`:axiom` or `:invar true`	a background assumption that holds in every state
`:invar-property N`	the safety property; with several, choose one with `--vmt-property N`

At least one :action or :trans is required. Frames are explicit: each action must state the next value of every state variable, including the ones it does not change, for example with (ite (= p q) new old). Lambda never adds frame conditions.

Example

The bakery protocol, from benchs/collection/misc/paper/vmt/bakery.vmt: processes take increasing tickets, and the process whose ticket is served may enter the critical section.

(declare-sort Process 0)                     ; unboundedly many processes
(declare-datatypes ((Location 0))            ; control location of a process
  (((Idle) (Waiting) (Critical))))
(declare-fun State (Process) Location)       ; state variables: one per process
(declare-fun State.next (Process) Location)
(declare-fun Ticket (Process) Int)
(declare-fun Ticket.next (Process) Int)
(declare-const NextTicket Int)               ; scalars: 0-ary state variables
(declare-const NextTicket.next Int)
(declare-const Serving Int)
(declare-const Serving.next Int)
(define-fun State.sv ((p Process)) Location  ; :next pairs a symbol with its
  (! (State p) :next State.next))            ; next-state copy: this is what
(define-fun Ticket.sv ((p Process)) Int      ; makes it a state variable
  (! (Ticket p) :next Ticket.next))
(define-fun NextTicket.sv () Int (! NextTicket :next NextTicket.next))
(define-fun Serving.sv () Int (! Serving :next Serving.next))
(define-fun init () Bool                     ; both counters start at one and
  (! (and (= NextTicket 1) (= Serving 1)     ; every process is idle, holding
          (forall ((p Process))              ; no ticket
            (and (= (State p) Idle) (= (Ticket p) 0)))) :init true))
(define-fun request () Bool                  ; an idle process takes a ticket
  (! (exists ((p Process))                   ; p is the process that moves
       (and (= (State p) Idle)
            (= NextTicket.next (+ NextTicket 1))
            (= Serving.next Serving)
            (forall ((q Process))            ; frame condition: every other
              (and (= (State.next q)         ; process q keeps its location
                      (ite (= p q) Waiting (State q)))
                   (= (Ticket.next q)        ; and its ticket
                      (ite (= p q) NextTicket (Ticket q)))))))
     :action true))                          ; one disjunct of T
(define-fun enter () Bool                    ; a waiting process whose ticket
  (! (exists ((p Process))                   ; is served becomes critical
       (and (= (State p) Waiting) (= (Ticket p) Serving)
            (= NextTicket.next NextTicket) (= Serving.next Serving)
            (forall ((q Process))
              (and (= (State.next q)
                      (ite (= p q) Critical (State q)))
                   (= (Ticket.next q) (Ticket q)))))) :action true))
(define-fun leave () Bool                    ; a critical process goes idle and
  (! (exists ((p Process))                   ; hands the turn to the next one
       (and (= (State p) Critical)
            (= NextTicket.next NextTicket)
            (= Serving.next (+ Serving 1))
            (forall ((q Process))
              (and (= (State.next q)
                      (ite (= p q) Idle (State q)))
                   (= (Ticket.next q)
                      (ite (= p q) 0 (Ticket q))))))) :action true))
(define-fun safety () Bool                   ; mutual exclusion: no two
  (! (forall ((p Process) (q Process))       ; distinct processes are
       (=> (and (= (State p) Critical)       ; critical at the same time
                (= (State q) Critical))
           (= p q))) :invar-property 0))

python3 -m lambda_pmc --show-witness -l vmt benchs/collection/misc/paper/vmt/bakery.vmt

Other formats

MCMT files are read natively (-l mcmt). mypyvy and IC3PO models are translated to this profile (-l mypyvy, -l ic3po), and Ivy models through Ivy's convert_to_mypyvy. All translators emit explicit frames, and the converters in lambda_pmc/translators/ write the VMT file, which can then be inspected or edited.