Glmc
ACL2 interface to AIG-based safety model checking
The GLMC package allows automated proving of safety properties of
state machines defined in ACL2. It uses GL to obtain a representation for the
next-state function, property, etc. as AIGs, and calls on an AIG model checker
such as ABC to verify the property.
Here is a small example:
(include-book "glmc")
(include-book "bfr-mcheck-abc")
(include-book "centaur/gl/bfr-satlink" :dir :system)
;; use abc as the model checking engine
(bfr-mcheck-use-abc-simple)
;; use satlink (glucose) as the SAT checker
(gl-satlink-mode)
;; start the external shell interface
(value-triple (acl2::tshell-start))
;; Definition of a (very) simple machine: machine state is just a 4-bit natural
;; which can be reset to 0 or incremented, but when incremented to exactly 10
;; resets to 0. This is the next-state function:
(defun my-nextst (st incr reset)
(b* (((when reset) 0)
(st (lnfix st))
((unless incr) st)
(next (1+ st))
((when (eql next 10)) 0))
next))
;; We'll check that this machine never reaches a state equal to 14. This function
;; checks the property for any finite run, where st is the initial state and ins
;; is the list of input pairs (incr . reset):
(defund my-run-prop (st ins)
(declare (xargs :measure (len ins)))
(if (atom ins)
t
(and (not (equal st 14))
(my-run-prop (my-nextst st (caar ins) (cdar ins)) (cdr ins)))))
;; Here we prove that if the initial value of the machine state is less than
;; 5, then our property holds:
(defthm my-run-prop-correct
(implies (and (natp st)
(< st 5))
(my-run-prop st ins))
:hints ((glmc-hint
:shape-spec-bindings `((incr ,(g-var 'incr))
(reset ,(g-var 'reset))
(st ,(g-int 0 1 5)))
:state-var st
:initstatep (< st 5)
:nextstate (my-nextst st incr reset)
:frame-input-bindings ((incr (caar ins))
(reset (cdar ins)))
:rest-of-input-bindings ((ins (cdr ins)))
:end-of-inputsp (atom ins)
:measure (len ins)
:run (my-run-prop st ins)
:state-hyp (and (natp st) (< st 16))
:prop (not (equal st 14))
:run-check-hints ('(:expand ((my-run-prop st ins)))))))
The notable thing about this example is that the property, as stated, is not
inductive. The usual way to prove this in ACL2 would be to strengthen the
property into an invariant that is inductive -- either weaken the initial state
assumption so that it is inductive (assume (< i 10) instead of (< i
5)) or strengthen the property (check (< st 10) instead of
(not (equal st 14))). Instead, we leave that task to the external model
checker (in this case ABC). GL transforms the ACL2 conjecture into a
finite-state machine safety property. If we trust ABC when it says the
property was proved, then this produces an ACL2 theorem.
Glmc-hint options
GLMC is invoked by the glmc-hint macro, which takes several keyword options:
- :state-var is the variable containing the current machine
state (as distinguished from the inputs).
- :body-bindings is a list of b* bindings under which to evaluate
the :nextstate, :initstatep :prop, and :constraint terms.
It should only use the state variable and frame inputs.
- :initstatep is a term that must be true for valid initial states,
though it may reference any variables bound in :body-bindings as well as
the state and frame input variables.
- :nextstate is a term giving the next value of the state, in terms of
the state variable, frame inputs, and variables bound by :body-bindings.
- :run is a term calling some function that recursively checks the
property on some finite run, i.e. it checks the property of the current state
and input frame, then recurs after updating the state with the nextstate
function.
- :frame-input-bindings is a binding list (such as in a let),
giving the current-frame inputs in terms of the inputs to the run
function. We'll refer to (e.g.) the list of all remaining frame inputs as the
"run inputs", versus (e.g.) a single element of that list as the "frame
inputs". E.g., if the input to the run function is simply a list of frame
inputs, then this binding might be ((in (car ins))).
- :rest-of-input-bindings is a binding list giving the rest of the
inputs after the current frame, such as is passed to the recursive call of the
run function -- e.g., ((ins (cdr ins))).
- :end-of-inputsp is a term saying when to stop the run; the run
function should always be true when :end-of-inputsp holds, because that
means it has failed to find a frame in which the property is violated. In the
case of a simple list of frame inputs, this would be (atom ins).
- :measure gives a measure for the run function; for technical reasons,
we must reprove the termination of the run function.
- :shape-spec-bindings gives a binding of the state variable and frame
input variables to shape specifier objects; see shape-specs. Unlike the
other arguments, this one is evaluated, so if you don't want to evaluate it,
quote it.
- :input-hyp gives an assumption about the frame inputs that must hold
in each frame or else the run function will return true. (If you want to have a
separate theorem hypothesis saying that the assumption holds for each input,
you may include this in the :run term using implies.) This is used
to prove that the shape-spec given for each non-state input is sufficient to
cover all allowed inputs.
- :state-hyp gives an assumption that must hold of all valid states; it
is used to prove that the shape-spec given for the state variable is sufficient
to cover all possible states. The goal to be proved must assume the state-hyp
holds of the initial state, and it will be proven to hold of all other states
by model checking or inductively; see the :state-hyp-method option
below.
- :state-hyp-method should be one of :inductive-sat,
:inductive-clause, or :mcheck (the default); this determines the
method by which we show that the state hyp is invariant. If it is
:inductive-clause, a proof obligation is generated saying that the state
hyp holds of the next-state if the input hyp and state hyp hold of the current
state. If it is :inductive-sat, a SAT check is issued which proves this
at the Boolean level. If it is :mcheck, then the condition is ANDed with
the property in the model checking problem. This is a more flexible method
(though potentially slower) because the state hyp may be an invariant of all
reachable states without being an inductive invariant.
- :prop gives the property that must be proven to hold in each
frame (i.e., the run function returns false if it is ever violated). It may
reference the state and frame input variables as well as variables bound in the
:body-bindings.
- :constraint gives a constraint that is assumed to hold in each
frame (i.e., the run function returns true if it is ever violated). (This may
be omitted; its default is T.) It may reference the state and frame input
variables as well as variables bound in the :body-bindings.
- :side-goals, if set to T, skips the actual model checking and
simply returns the "side goals" such as coverage and the check that the run
function and input clause are of the expected form. (A theorem with
:side-goals t will always fail to prove, but if everything is successful
only a single subgoal of the form (not (gl-cp-hint 'side-goals-fake-goal))
will remain.)
- :check-vacuity is T by default; when true, GLMC will check that
the state-hyp, input-hyp, initial state predicate, constraint, and property are
each separately satisfiable, since any of these being unsatisfiable likely
indicates something unexpected. Setting this to NIL skips these
checks.
- :clause-check-hints, :run-check-hints, :measure-hints, and
:state-hyp-inductive-hints provide computed hints to various side goals
produced by the clause processor. Each entry should be a list of hints like
the usual :hints provided to a defthm event, but all the hints should be
computed hints, not subgoal hints. The side goals are discussed below.
- :do-not-expand, :cov-theory-add, :cov-hints, and
:cov-hints-position affect the hints given to the coverage side goal; see
coverage-problems. To provide your own hints, completely overriding the
default hints provided for coverage, use :cov-hints to give your hints and
set :cov-hints-position :replace.
Side goals
A few proof obligations are produced by a successful call of the GLMC clause
processor.
- Coverage: Shows that the shape specifiers provided in the
:shape-spec-bindings argument are sufficient to cover all possible states
and inputs allowed by the state and input hyps. This goal has the same form as
any GL coverage proof; see shape-specs and coverage-problems.
- Clause check: This simply shows that the goal clause is of the required
form. Specifically, the original goal must follow from this conjecture, which
is what GLMC actually proves:
(implies (and <initstp> <st-hyp>)
<run>)
- Run check: This checks that the :run term is implied by the recurrence
that is proved by the model check, namely:
(if <end-of-inputs>
t
(let <frame-input-bindings>
(let <rest-of-input-bindings>
(if (not (and <input-hyp>
(b* <body-bindings> <constraint>)))
t
(if (not (b* <body-bindings> <prop>))
nil
(let ((<st-var> (b* <body-bindings> <nextstate>)))
(if (not <state-hyp>)
'nil
<run>)))))))
- Measure check: This rechecks that the run function terminates, which is
necessary for technical reasons.
- State-hyp-inductive check: This only occurs if the :state-hyp-method
is :inductive-clause; it shows that the state hyp is invariant.
Backends
GLMC uses the same method as GL to solve combinational SAT problems, such as
vacuity checks (see modes). GLMC calls its model-checking backend
through an attachable function called bfr-mcheck. The book
"glmc/bfr-mcheck-abc.lisp" provides one backend that can be attached to
bfr-mcheck by calling the macro (bfr-mcheck-use-abc-simple). That
backend requires a trust tag because it calls out to ABC; it also simply trusts
ABC when it claims the conjecture is proved.
Subtopics
- Bfr-mcheck
- Attachable interface for glmc's model-checking backend
- Bfr-mcheck-abc-simple
- Bfr-mcheck interface for ABC model-checking
