;; ------------------------------------------------------------------------
;; Installation
;; ------------------------------------------------------------------------
For newest version:
0) Install ACL2, certify the books
1) Remove books/clause-processors/SULFA
2) Download SULFA.tar.gz:
www.cs.utexas.edu/users/reeber/SULFA.tar.gz
3) Unzip and untar into books/clause-processors/SULFA
4) Go into books/clause-processors/SULFA/Makefile:
point SAT_SOLVER_TYPE and SAT_SOLVER at minisat or zchaff
My personal settings:
SAT_SOLVER_TYPE ?= zchaff
SAT_SOLVER ?= /projects/hvg/SAT/solvers/bin/zchaff
5) In books/clause-processors/SULFA
make
The newest version of my SULFA tool should now be installed!
;; ------------------------------------------------------------------------
;; The basics
;; ------------------------------------------------------------------------
1) Make sure you're in a directory that you can write to---SULFA
creates a directory sat-temp-files to hold temporary files.
2) Run the version of ACL2 you just created
/projects/hvg/reeber-local/acl2-sources/saved_acl2
3) Include the SULFA book, with its ttags:
(include-book
"clause-processors/SULFA/books/clause-processors/sat-clause-processor"
:dir :system :ttags (sat sat-cl))
4) See "books/clause-processors/SULFA/books/sat-tests/tutorial.lisp" for some
examples:
;; First, let's prove a propositional formula
(defthm prop-form-1
(or (and a b)
(and (not a) b)
(not b))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; If we give an invalid SULFA formula, then
;; the clause processor produces a counter-example.
#|
;; For example
(defthm prop-invalid
(or (and a b)
(and (not a) b)
b)
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
|# ;|
;; Any function that breaks down into "if" functions
;; can be converted to SAT.
(defthm prop-form-2
(implies (and (iff a b)
(iff b c))
(iff a c))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; We also support equality (though it isn't as efficient as I'd like).
(defthm prop-form-3
(implies (and (equal a b)
(equal b c))
(equal a c))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; ------------------------------------------------------------------------
;; The List Primitives
;; ------------------------------------------------------------------------
;; And we support the list primitives, car, cdr, cons, and consp
;; For example, here's a theorem that might not be intuitively
;; obvious:
(defthm prop-form-4
(implies (and (not (equal (car a) 'nil))
(equal (car a) (car b))
(equal (cdr a) (cdr b))
(equal (car b) (car c))
(equal (cdr b) (cdr c)))
(equal a c))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
#|
;; Note that the first hypothesis is necessary, as
;; the clause processor correctly identifies the
;; counter-example a='nil, b='(nil), c='(nil) in
;; the theorem below
(defthm prop-invalid
(implies (and (equal (car a) (car b))
(equal (cdr a) (cdr b))
(equal (car b) (car c))
(equal (cdr b) (cdr c)))
(equal a c))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
|# ;|
;; We call the functions equal, if, car, cdr, cons, and consp the
;; SULFA primitives.
;; If you try to prove most theorems about other core ACL2 primitives,
;; you get a message saying that the formula is not in SULFA.
#|
;; For example:
(defthm +-failure
(equal (+ a b) (+ b a))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
|# ;|
;; ------------------------------------------------------------------------
;; Uninterpreted Functions
;; ------------------------------------------------------------------------
;; However, we also can handle uninterpreted functions.
;; For example, if we create a symbol "f" using defstub
(defstub f (*) => *)
;; We can prove:
(defthm uninterpreted-prop-1
(implies (and (equal (f x) (f y))
(equal (f y) (f z))
(equal a z))
(equal (f x) (f a)))
:hints (("Goal" :clause-processor
(:function
sat
:hint
'(:check-counter-example nil))))
:rule-classes nil)
;; (the check-counter-example=nil hint tells the clause processor
;; not to execute the any counter-example found, since the formula
;; isn't executable).
;; And we support "treating a function as if it were uninterpreted".
;; For example, in the property below we treat "+" and "<" as
;; uninterpreted:
(defthm uninterpreted-prop-2
(implies (and (equal x a)
(equal y b)
(equal (+ a 4) 25)
(< x y))
(< a b))
:hints (("Goal" :clause-processor
(:function
sat
:hint
'(:uninterpreted-functions (< binary-+)))))
:rule-classes nil)
;; Note that we can't treat macros as uninterpreted functions,
;; so we treat "binary-+" as uninterpreted, rather than +.
#|
;; Of course, if we try to prove something about an uninterpreted
;; function, we are limited to proving that it is true for all functions.
;; Therefore, the following property is not proven
(defthm uninterpreted-failure
(equal (+ a b) (+ b a))
:hints (("Goal" :clause-processor
(:function
sat
:hint
'(:uninterpreted-functions (binary-+)))))
:rule-classes nil)
|# ;|
;; ------------------------------------------------------------------------
;; User-Defined Functions
;; ------------------------------------------------------------------------
;; The power of SULFA though, really comes from user-defined functions.
;; For example, we can define xor as below:
(defun xor (x y)
(if x (if y nil t) (if y t nil)))
;; And now we can prove theorems about xor, using the clause processor:
(defthm xor-thm-1
(iff (xor a0 (xor a1 (xor a2 a3)))
(xor a3 (xor a2 (xor a1 a0))))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; We can also define new functions from xor and prove theorems about them:
(defun xor3 (a b c) (xor a (xor b c)))
(defthm xor-thm-2
(iff (xor3 a b c)
(xor3 c a b))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; We also support the restricted application of functions defined
;; using arbitrary executable functions.
;; For example, consider the following function foo:
(defun foo (a b)
(if (zp a)
b
(cdr b)))
;; Because "zp" only is used on the first argument, we allow
;; applications of "foo" as long as the first argument evaluates
;; to a constant.
(defthm foo-prop-1
(implies (not (equal b 'nil))
(not (equal (cdr (foo (+ 7 6) b)) b)))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; We call the first argument of foo a "ground formal" because
;; it must be grounded in any SULFA formula.
#|
;; To lookup the ground formals of a function, you can use:
(sat-ground-formals 'foo $sat state)
;; Which returns the error quadruple:
(NIL (T NIL) <$sat> )
;; where the second argument is a list of Boolean representing
;; whether the corresponding formal of 'foo is a ground formal.
;; For example, to see that all arguments of 'binary-+
;; must be grounded
(sat-ground-formals 'binary-+ $sat state)
;; returns
(NIL (T T) <$sat> )
;; to see that no arguments of xor3 must be grounded:
(sat-ground-formals 'xor3 $sat state)
;; returns
(NIL (NIL NIL NIL) <$sat> )
;; Note: that these results are always relative to the
;; the last uninterpreted-functions list given to the
;; clause processor. If we attempt to prove:
(defthm uninterpreted-failure
(equal (+ a b) (+ b c))
:hints (("Goal" :clause-processor
(:function
sat
:hint
'(:uninterpreted-functions (binary-+)))))
:rule-classes nil)
;; Then
(sat-ground-formals 'binary-+ $sat state)
;; returns
(NIL (NIL NIL) <$sat> )
;; Since we're treating 'binary-+ as an uninterpreted function.
;; (once you call the clause processor with a new uninterpreted
;; function list, the ground formals will reset).
|# ;|
;; SULFA also contains restricted applications of recursively
;; defined functions. We use the notion of ground formals to
;; force applications of recursive functions to be unrollable.
;; For example, the following defined an n bit, bit-vector adder
(defun maj3 (x y z)
(if x (or y z)
(and y z)))
;; Returns a n+1 length sum of the first
;; n bits of a and b (plus the carry).
(defun v-adder (n c a b)
(if (zp n)
(list c)
(cons (xor3 c (car a) (car b))
(v-adder (1- n)
(maj3 c (car a) (car b))
(cdr a) (cdr b)))))
#|
;; The first formal of v-adder must be a ground formal,
;; both because of its use in (zp n), and its use in
;; the recursive measure of v-adder.
(sat-ground-formals 'v-adder $sat state)
;; =>
(NIL (T NIL NIL NIL) <$sat> )
;; Thus, the "commutativity of an 8 bit v-adder" is in SULFA
(defthm 8-v-adder-commute
(equal (v-adder 8 nil a b)
(v-adder 8 nil b a))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; But the above property isn't a theorem for untyped domains, and
;; SULFA finds a counter-example.
|# ;|
;; One way to fix this is to define an n bit, bit-vector predicate:
(defun n-bvp (n x)
(cond
((zp n)
(equal x nil))
((booleanp (car x))
(n-bvp (1- n) (cdr x)))
(t
nil)))
;; Now we can prove the theorem over bit vectors:
(defthm 8-v-adder-commute
(implies
(and (n-bvp 8 a)
(n-bvp 8 b))
(equal (v-adder 8 nil a b)
(v-adder 8 nil b a)))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; You might ask how big a commute property can we prove with SULFA.
;; The following 1024 bit theorem goes through pretty easily
;; (27 seconds with zChaff on my machine):
(defthm 1024-v-adder-commute
(implies
(and (n-bvp 1024 a)
(n-bvp 1024 b))
(equal (v-adder 1024 nil a b)
(v-adder 1024 nil b a)))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; ------------------------------------------------------------------------
;; Efficiently-Defined Functions
;; ------------------------------------------------------------------------
;; In order to get much bigger with our system, you would want to switch to
;; a bit-vector equality operation, rather than using the n-bit Boolean predicate
;; (remember that equal isn't that efficient) and use a tree representation
;; for bit vectors rather than a list representation (when trees
;; get over a thousand elements deep, like the lists in this bit-vector
;; representation, it puts significant pressure on the conversion algorithm).
;; Another efficiency note, while we're on the subject, is to remember
;; that your functions are unrolled. So don't duplicate recursive applications
;; unnecessarily.
(defun bar (n x ans)
(cond
((zp n)
ans)
(t
(or (bar (1- n) (cdr x) (or (equal (car x) 0) ans))
(bar (1- n) (cdr x) (or (equal (car x) 1) ans))))))
(defthm bar-prop
(implies (equal (nth 5 x) 1)
(bar 10 x nil))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; In the property above, the application of "bar" explodes during
;; unrolling. Thus, an n=10 is about as big as we can get.
;; However, if we a version of "bar" with only one recursive call, it
;; does not explode:
(defun bar-better (n x ans)
(cond
((zp n)
ans)
(t
(bar-better (1- n)
(cdr x)
(or (equal (car x) 0)
(equal (car x) 1)
ans)))))
(defthm bar-better-prop
(implies (equal (nth 50 x) 1)
(bar-better 100 x nil))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
;; ------------------------------------------------------------------------
;; Sudoku
;; ------------------------------------------------------------------------
;; For a more fun example, we can load in our model of the
;; Sudoku puzzle:
(include-book
"clause-processors/SULFA/books/sat-tests/sudoku"
:dir :system
:ttags (sat sat-cl))
;; We've modeled the puzzle constraints using ACL2.
;; Thus, we can represent a puzzle as an ACL2 constant:
(defconst *puzzle*
'((X X 6 7 X X 4 X X)
(9 8 X X X X 3 X X)
(X X X 8 2 X X X X)
(X X X 6 X 2 5 X X)
(3 X X X 5 X X X 6)
(X X 1 4 X 8 X X X)
(X X X X 1 5 X X X)
(X X 2 X X X X 7 8)
(X X 3 X X 7 1 X X)))
#|
;; Now if we try to prove the puzzle has no solution,
;; our clause processor produces a solution as a counter-example:
(thm
(implies (satisfies-constraintsp *puzzle* x)
(not (good-solutionp x)))
:hints (("Goal" :clause-processor (:function sat :hint nil))))
(thm
(not (and (satisfies-constraintsp *puzzle-x* x)
(satisfies-constraintsp *puzzle-x* y)
(not (equal x y))
(good-solutionp x)
(good-solutionp y)))
:hints (("Goal" :clause-processor (:function sat :hint nil))))
|# ;|
;; ----------------------------------------------------------------
;; Hardware Invariants & Debugging
;; ----------------------------------------------------------------
;; Let's look at some proofs from the TRIPS data tile exception protocol
;; The ACL2 model, constructed automatically from the Verilog is in
;; ../dsn_clean/ACL2-dt_lsq_dsn.lisp
;; More of the model, hand generated, is in
;; ../dsn_clean/ACL2v-setup.lisp
;; The bit-vector primitives are in
;; ../DE/flg-eval.lisp
(include-book "dsn_clean/ACL2v-setup" :ttags (sat sat-cl))
;; Strategy
;; We prove the safety property using the standard
;; inductive invariant technique:
;; thm(st(Tau,iota), ins(Tau,iota))
;; is proven by defining an invariant function "inv"
;; satisfying the following finite-step properties
;; (finite-step properties are reducable to SULFA):
;; 1. inv(S_{0})
;; 2. inv(S) -> inv(step(S,I))
;; 3. inv(S) -> thm(S,I)
;; Explain the Exception protocol. We want to prove that exceptions
;; reported by the top tile in the DSN are also reported by the
;; spec machine.
;; Draw the tiles on the white board:
;; Local inputs from the left, flushes from the top
;; Exceptions heading upward.
;; First lets just try to prove it as an inductive invariant:
(include-book "dsn_clean/ACL2v-setup" :ttags (sat sat-cl))
(defun exception-safety-inv (type x st)
(implies
(dsn-st-exceptionp type x 0 (dsn-st st))
(ith x (spec-st-exception-mask type (spec-st st)))))
;; SULFA Proofs
;;(i-am-here)
;; 1. inv(S_{0})
(defthm-sat-for-all exception-safety-inv-init
((int x 0 7))
(exception-safety-inv type x (initial-proof-state)))
;; 2. inv(S) -> inv(step(S,I))
(defthm-sat-for-all exception-safety-inv-step
((int x 0 7))
(implies
(and (valid-inputsp (env-st st) ins)
(exception-safety-inv type x st))
(exception-safety-inv type x (update-proof-state st ins))))
;; Failure!
;; First, let's focus on a single output bit:
;; This means that the failure must occur in instruction block 0:
(defthm-sat-for-all exception-safety-inv-step
((int x 0 0))
(implies
(and (valid-inputsp (env-st st) ins)
(exception-safety-inv type x st))
(exception-safety-inv type x (update-proof-state st ins))))
;; So the DSN is reporting an exeption in tile 0, but the spec machine is not.
;; Why?
;; What about last cycle?
(sat-cl-ce
(let ((x 0))
(dsn-st-exceptionp type x 0 (dsn-st st))))
(sat-cl-ce
(let ((x 0))
(ith x (spec-st-exception-mask type (spec-st st)))))
;; Last cycle neither reported exception.
;; Did the new exception come in from the inputs?
(sat-cl-ce (local-exception-en type 0 ins)))
(sat-cl-ce (local-exception-bid type 0 ins))
;; Nope! It must have come from below then:
(sat-cl-ce (dsn-st-exceptionp type 0 1 (dsn-st st)))
;; Yup! There was an exception in Tile 1 last cycle that wasn't reported
;; by the spec machine last cycle. That's because the invariant isn't strong
;; enough! We need the spec to be reporting every tiles exceptions!
;; --------------------------------------------------------------------
;; Trying again
;; --------------------------------------------------------------------
:ubt! 1
(include-book "dsn_clean/ACL2v-setup" :ttags (sat sat-cl))
(def-for-all exception-safety-inv (type x st)
((int tile 0 3))
(implies
(dsn-st-exceptionp type x tile (dsn-st st))
(ith x (spec-st-exception-mask type (spec-st st))))
:no-theorems t)
;; SULFA Proofs
;;(i-am-here)
;; 1. inv(S_{0})
(defthm-sat-for-all exception-safety-inv-init
((int x 0 7))
(exception-safety-inv type x (initial-proof-state)))
;; 2. inv(S) -> inv(step(S,I))
(defthm-sat-for-all exception-safety-inv-step
((int x 0 7))
(implies
(and (valid-inputsp (env-st st) ins)
(exception-safety-inv type x st))
(exception-safety-inv type x (update-proof-state st ins))))
;; Failure!
;; First, let's focus on a single output bit again:
(defthm-sat-for-all exception-safety-inv-step
((int x 0 0))
(implies
(and (valid-inputsp (env-st st) ins)
(exception-safety-inv type x st))
(exception-safety-inv type x (update-proof-state st ins))))
;; Now figure out which tile is failing:
(sat-cl-ce
(let ((tile 0)
(x 0))
(implies
(dsn-st-exceptionp type x tile (dsn-st (update-proof-state st ins)))
(ith x (spec-st-exception-mask type (spec-st (update-proof-state st
ins)))))))
;; Not tile 0...
;; Aha! It's tile 3!
(sat-cl-ce
(let ((tile 3)
(x 0))
(implies
(dsn-st-exceptionp type x tile (dsn-st (update-proof-state st ins)))
(ith x (spec-st-exception-mask type (spec-st (update-proof-state st
ins)))))))
;; So the DSN is reporting an exeption in tile 3, but the spec machine is not.
;; Why?
;; What about last cycle?
(sat-cl-ce
(let ((tile 3)
(x 0))
(dsn-st-exceptionp type x tile (dsn-st st))))
;; The DSN mask was low last cycle. Did it come in from the inputs?
(sat-cl-ce (local-exception-en type 3 ins)))
(sat-cl-ce (local-exception-bid type 3 ins))
;; Yup! Why didn't the spec report the exception then?
;; Looking at the definition of the spec exception, it must have been
;; a flush was on its way. Let's check:
(sat-cl-ce (flush-mask 0 ins))
;; Yup! A flush is occuring in block 0, tile 0. The invariant is now
;; too strong, because the spec doesn't report exceptions that are
;; "about to be flushed."
;; --------------------------------------------------------------------
;; Trying again
;; --------------------------------------------------------------------
:ubt! 1
(include-book "dsn_clean/ACL2v-setup" :ttags (sat sat-cl))
;; Invariant Definition
(def-for-all exception-safety-inv (type x st)
((int tile 0 3))
(implies
(and (not (dsn-st-flush-comming x tile (dsn-st st)))
(dsn-st-exceptionp type x tile (dsn-st st)))
(ith x (spec-st-exception-mask type (spec-st st))))
:no-theorems t)
;; SULFA Proofs
;;(i-am-here)
;; 1. inv(S_{0})
(defthm-sat-for-all exception-safety-inv-init
((int x 0 7))
(exception-safety-inv type x (initial-proof-state)))
;; 2. inv(S) -> inv(step(S,I))
(defthm-sat-for-all exception-safety-inv-step
((int x 0 7))
(implies
(and (valid-inputsp (env-st st) ins)
(exception-safety-inv type x st))
(exception-safety-inv type x (update-proof-state st ins))))
;; 3. inv(S) -> thm(S,I)
(defthm-sat-for-all exception-safety-imp-thm
((int x 0 7))
(implies
(and (valid-inputsp (env-st st) ins)
(exception-safety-inv type x st)
(ith x (udt-exception-mask type 0 (dsn-st st) ins)))
(ith x (spec-exception-mask type (spec-st st) ins))))
;; Composition
(defthm exception-safety-inv-tth
(implies
(and (integerp x) (<= 0 x) (<= x 7)
(integerp tau) (<= 0 tau)
(Tth-valid-inputsp tau ins-stream))
(exception-safety-inv type x (Tth-proof-state tau ins-stream))))
;; Final Proof
(defthm exception-safety-spec
(implies
(and (integerp tau) (<= 0 tau)
(integerp x) (<= 0 x) (<= x 7)
(Tth-valid-inputsp tau ins-stream)
(ith x (udt-exception-mask
type 0 (Tth-dsn-state tau ins-stream) (ith tau ins-stream))))
(ith x (spec-exception-mask
type (Tth-spec-state tau ins-stream) (ith tau ins-stream)))))
;; -----------------------------------------------------------------------
;; The "Liveness" Theorem
;; -----------------------------------------------------------------------
;; Want to prove that if an exception is reported in the spec, it is eventually
;; reported by the top tile as well.
(include-book "ACL2v-setup" :ttags (sat sat-cl))
;; Strategy
;; We prove a liveness property of the form
;; hyp(st(Tau,iota), ins(Tau,iota))
;; ->
;; (exists Tau': conc(st(Tau',iota),ins(Tau',iota)))
;; by defining an invariant function "inv" and a bound function
;; "bnd" satisfying the following finite-step properties
;; (finite-step properties are reducable to SULFA):
;; 1. inv(S_{0})
;; 2. inv(S) -> inv(step(S,I))
;; 3. inv(step(S,I)) /\ hyp(S,I) /\ not(conc(S,I)) -> bnd(b_{0},step(S,I))
;; 4. forall b 0<=b<=(b_{0}-1): bnd(b+1,S) /\ not(conc(S,I)) -> bnd(b,step(S,I))
;; 5. bnd(0,step(S,I)) -> conc(S,I)
;; hyp(S,I) -> hyp'(step(S,I))
;; conc(S,I) -> conc'(step(S,I))
;; Invariant and Bound Definitions
(in-theory (disable member))
(defund exception-bnd (type x b st)
(if (zp b)
(and (not (ith x (dsn-st-flush-mask 0 (dsn-st st))))
(dsn-st-exceptionp type x 0 (dsn-st st)))
(or (and (not (dsn-st-flush-comming x b (dsn-st st)))
(not (ith x (dsn-st-flush-mask b (dsn-st st))))
(dsn-st-exceptionp type x b (dsn-st st)))
(exception-bnd type x (1- b) st))))
(defund exception-liveness-inv (type x st)
(implies (ith x (spec-st-exception-mask type (spec-st st)))
(exception-bnd type x 3 st)))
;; SULFA Proofs
;; 1. inv(S_{0})
(defthm-sat-for-all arrived-liveness-inv-init
((int x 0 7))
(exception-liveness-inv type x (initial-proof-state)))
;; 2. inv(S) -> inv(step(S,I))
(defthm-sat-for-all arrived-liveness-inv-step
((int x 0 7))
(implies
(and (valid-inputsp (env-st st) ins)
(exception-liveness-inv type x st))
(exception-liveness-inv
type
x
(update-proof-state st ins))))
;; 3. inv(step(S,I)) /\ hyp(S,I) /\ not(conc(S,I)) -> bnd(b_{0},step(S,I))
(defthm-sat-for-all arrived-liveness-inv-bnd
((int x 0 7))
(implies
(and (ith x (spec-exception-mask type (spec-st st) ins))
(exception-liveness-inv type x (update-proof-state st ins)))
(exception-bnd type x 3 (update-proof-state st ins))))
;; 4. forall b 0<=b bnd(b,step(S,I))
(defthm-sat-for-all arrived-bnd-dec
((int x 0 7)
(int b 0 2))
(implies
(and (exception-bnd type x (+ b 1) st)
(valid-inputsp (env-st st) ins)
(not (ith x (flush-mask 0 ins))))
(exception-bnd type x b (update-proof-state st ins))))
;; 5. bnd(0,step(S,I)) -> conc(S,I)
(defthm-sat-for-all arrived-bnd-implies-thm
((int x 0 7))
(implies
(and (exception-bnd type x 0 (update-proof-state st ins))
(not (ith x (flush-mask 0 ins))))
(ith x (udt-exception-mask type 0 (dsn-st st) ins))))
;; Composition
(defthm exception-liveness-inv-tth
(implies
(and (integerp x) (<= 0 x) (<= x 7)
(integerp tau) (<= 0 tau)
(Tth-valid-inputsp tau ins-stream))
(exception-liveness-inv type x (Tth-proof-state tau ins-stream))))
(defun exception-ord (type x st)
(cond
((exception-bnd type x 0 st) 0)
((exception-bnd type x 1 st) 1)
((exception-bnd type x 2 st) 2)
((exception-bnd type x 3 st) 3)
(t 4)))
(defun exception-liveness-witness (tau-prime type x ins-stream)
(declare (xargs :measure
(if (or (not (Tth-valid-inputsp tau-prime ins-stream))
(equal (exception-ord type x (Tth-proof-state (1+ tau-prime) ins-stream))
4)
(ith x (flush-mask 0 (ith tau-prime ins-stream)))
(ith x (udt-exception-mask
type 0
(dsn-st (Tth-proof-state tau-prime ins-stream))
(ith tau-prime ins-stream))))
0
(exception-ord type
x
(Tth-proof-state (1+ tau-prime) ins-stream)))))
(cond
((not
(and (integerp tau-prime) (<= 0 tau-prime)
(integerp x) (<= 0 x) (<= x 7)))
0)
((or (not (Tth-valid-inputsp tau-prime ins-stream))
(equal (exception-ord type x (Tth-proof-state (1+ tau-prime) ins-stream))
4)
(ith x (flush-mask 0 (ith tau-prime ins-stream)))
(ith x (udt-exception-mask
type 0
(dsn-st (tth-proof-state tau-prime ins-stream))
(ith tau-prime ins-stream))))
tau-prime)
(t
(exception-liveness-witness (1+ tau-prime) type x ins-stream))))
(defthm exception-liveness-witness->=tau-prime
(implies
(and (integerp tau-prime) (<= 0 tau-prime)
(integerp x) (<= 0 x) (<= x 7))
(<= tau-prime
(exception-liveness-witness tau-prime type x ins-stream)))
:rule-classes :linear)
(defthmd exception-liveness-witness-thm
(implies
(and (integerp tau) (<= 0 tau)
(integerp x) (<= 0 x) (<= x 7)
(not (equal (exception-ord type x (Tth-proof-state (1+ tau) ins-stream))
4))
(Tth-valid-inputsp (exception-liveness-witness tau type x ins-stream) ins-stream)
(not (ith x
(flush-mask 0 (ith (exception-liveness-witness
tau type x ins-stream) ins-stream)))))
(ith x (udt-exception-mask
type 0
(dsn-st
(tth-proof-state
(exception-liveness-witness tau type x ins-stream) ins-stream))
(ith (exception-liveness-witness tau type x ins-stream) ins-stream)))))
;; ----------------------------------------------------
;; Final Proof
;; ----------------------------------------------------
;; Note that there is "eventually an exception" if there
;; is any invalid input in the input stream after tau.
;; Thus, we better be sure it's possible to have an infinite
;; stream of valid inputs!
;;
;; It might be better to bound tau-prime as being less than tau+4.
;; But the property below is prettier, since it's more abstract.
(defun-sk eventually-exception
(tau type x ins-stream)
(exists
(tau-prime)
(and (integerp tau-prime)
(<= tau tau-prime)
(implies
(Tth-valid-inputsp tau-prime ins-stream)
(or (ith x (flush-mask 0 (ith tau-prime ins-stream)))
(ith x (udt-exception-mask
type 0
(Tth-dsn-state tau-prime ins-stream)
(ith tau-prime ins-stream))))))))
(defthm exception-liveness-thm
(implies
(and (integerp tau) (<= 0 tau)
(integerp x) (<= 0 x) (<= x 7)
(ith x (spec-exception-mask type
(Tth-spec-state tau ins-stream)
(ith tau ins-stream))))
(eventually-exception tau type x ins-stream))
:hints (("Goal"
:use ((:instance eventually-exception-suff
(tau-prime (exception-liveness-witness
tau
type
x
ins-stream)))
(:instance exception-liveness-witness-thm
(tau (1+ tau))))
:do-not-induct t)))
;; -----------------------------------------------------------------------
;; The Future (if only we had infinite resources)
;; -----------------------------------------------------------------------
1) I wish SULFA had used an incremental algorithm
* Could have a drastic effect on uninterpretted functions efficiency.
* Support more general counterexample-finding algorithms.
2) I wish SULFA had common subexpression elimination built-in
* Now I always try to design functions and theorems so that they do not
repeat expressions.
3) I wish SULFA had a more general data structure algorithm built-in
* Cons is nice, but assoc would be better. I don't see any reason why
theorems like the following can't be in SULFA:
(implies
(p x0 x1 a0 b0 ... a1 b1 ...)
(equal (get x0 (set a0 (set b0 (set ...))))
(get x1 (set a1 (set b1 (set ...))))))