;; ------------------------------------------------------------------------
;; 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> <state>)
;; 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> <state>)

;; to see that no arguments of xor3 must be grounded:
(sat-ground-formals 'xor3 $sat state)
;; returns
(NIL (NIL NIL NIL) <$sat> <state>)

;; 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> <state>)
;; 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> <state>)

;; 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<b_{0}: bnd(b+1,S) /\ not(conc(S,I)) -> 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 ...))))))