(in-package "ACL2")

; Need to define the "*" package, before (certify-book "main" 7):
; (ld "packages.lisp")

; Include the "*" model.
(include-book "constants")

; Include input-assumptions.
(include-book "inputs")

; Here is the desired relation between input and output, given appropriate
; constraints on other signals.
(defun result (in out)
  (equal out
         (logand (logand (bitn in 0) (bitn in 1))
                 (logand (bitn in 2) (bitn in 3)))))

; We sometimes assume the following relationships between inputs in our two
; models.  Eventually we will functionally instantiate the "*" functions with
; the "ACL2" functions, removing any such assumption from our main result.
(defmacro bindings (n)
  `(and (equal (*::longop) (longop ,n))
        (equal (*::in) (in ,n))))

; The following definition of spec states what must be true of the inputs in
; the "*" model in order to prove the desired result for the "*" model
; (spec-lemma-2 below).  It should be straightforward that spec holds of the
; "ACL2" model inputs (spec-lemma-1).

(defun spec (in longop)
  (declare (ignore in))
  (equal longop 1))

; This should be easy.
(defthm spec-lemma-1
  (implies (input-assumptions n)
           (spec (in n) (longop n))))

; Here is where all the effort goes, in general.  For our toy model the proof
; is very easy simply by enabling all the "*" functions.
(defthm spec-lemma-2
  (implies (spec (*::in) (*::longop))
           (result (*::in) (*::out)))
  :hints (("Goal" :in-theory
           (enable *::S01 *::S01_MUXED *::S01_MUXED_FLOPPED
                   *::S23 *::S23_FLOPPED *::S0123
                   *::LONGOP_FLOPPED *::OUT))))

; The rest of our development requires only the above facts about the functions
; we now disable, together with pipeline-lemma below.
(in-theory (disable result input-assumptions spec))

(encapsulate
 ()
 (local (include-book "pipe"))
 (defthm pipeline-lemma
   (implies (and (input-assumptions n)
                 (bindings n))
            (equal (out (+ 2 n)) (*::out)))
   :hints (("Goal"
            :use ((:definition input-assumptions*))))))

(defthm lemma-to-be-instantiated
  (implies (and (input-assumptions n)
                (bindings n)
                (spec (*::in) (*::longop)))
           (result (*::in)
                   (out (+ 2 n)))))

(defthm correctness-of-pipeline
  (implies (input-assumptions n)
           (result (in n)
                   (out (+ 2 n))))
  :hints (("Goal" :use ((:instance
                         (:functional-instance
                          lemma-to-be-instantiated
                          (*::in     (lambda () (in k)))
                          (*::longop (lambda () (longop k))))
                         (k n))))))