(in-package "ACL2")

;; Requires ihs-new book
;; Certifies in ~ 1 minute under ACL2 2.5x with nu-rewriter patches 
;
;; The Thread problem

;; This ACL2 proof script solves a puzzle posed by J Moore in May
;; 2001.  (Ruben Gamboa mentioned this problem a few weeks earlier as
;; a J problem as well.)  Consider a machine that has two processes
;; that forever execute a loop containing the line c := c + c.  The
;; line has three atomic operations: two reads of the value c (into
;; temporary local variables) and the setting of c to the sum of the
;; local variables.  Assume that the initial value of c is 1.

;; The challenge is to show that there exists some interleaving of the
;; process tasks such that the operations lead to the placement in C
;; of any arbitrary positive value.

;; This script defines an interpreter for modeling this two-process
;; machine.  The interpreter accepts an initial state and a list of
;; process names that represent the sequence of the two process'
;; atomic instructions that are to be executed.  An ACL2 function that
;; calculates a process execution sequence given a "target" value is
;; proved to lead the two-process machine to the desired value.

;; DAG wants me to make these sequence-generators composable in the
;; sense that that you could run multiple programs, one after another.

;; Matt Wilding - 14 May 2001

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Some miscellaneous rules

(defthm +x-x-as-*2
  (equal (+ x x) (* 2 x)))

(defthm ash-+x-x-pos
  (implies
   (and (integerp x) (integerp n) (<= 0 n))
   (equal
    (ash (+ x x) n)
    (ash x (1+ n))))
  :hints (("goal" :in-theory (enable ash))))

(defthm ash-*2-pos
  (implies
   (and (integerp n) (integerp x)
	(<= 0 n))
  (equal
   (ash (* 2 x) n)
   (* 2 (ash x n))))
  :hints (("goal" :in-theory (enable ash))))

(defthm update-nth-noop
  (implies
   (and
    (equal v (nth n l))
    (< (nfix n) (len l)))
   (equal (update-nth n v l) l))
  :hints (("goal" :in-theory (enable update-nth nth len))))

;; least significant bit
(defun lsb (i)
  (if (zp i)
      0
    (if (equal (logcar i) 1)
	0
      (1+ (lsb (logcdr i))))))

(defthm loghead-1+-lsb
  (implies
   (and (integerp x) (< 0 x))
   (equal (loghead (1+ (lsb x)) x)
	  (ash 1 (lsb x))))
  :hints (("goal" :in-theory (enable logops-recursive-definitions-theory))))

(defthm <-lsb-integer-length
  (implies
   (and (integerp x) (< 0 x))
   (equal (< (lsb x) (integer-length x)) t))
  :hints (("goal" :in-theory (enable integer-length))))

(defthm ash-1-pos
  (implies
   (and (integerp n) (<= 0 n))
   (equal (ash 1 n) (expt 2 n)))
  :hints (("goal" :induct (sub1-induction n)
	   :in-theory (enable logops-recursive-definitions-theory))))
  
(defthm loghead-topbit-set
  (implies
   (and
    (logbitp (1+ n) x)
    (integerp n) (<= 0 n)
    (integerp x))
   (equal
    (loghead (+ 2 n) x)
    (+ (loghead (1+ n) x) (ash 1 (1+ n)))))
  :hints (("goal" :induct (sub1-logcdr-induction n x)
	   :in-theory (enable logops-recursive-definitions-theory))))

(defthm loghead-topbit-unset
  (implies
   (and
    (not (logbitp (1+ n) x))
    (integerp n) (<= 0 n)
    (integerp x))
   (equal
    (loghead (+ 2 n) x)
    (loghead (1+ n) x)))
  :hints (("goal" :induct (sub1-logcdr-induction n x)
	   :in-theory (enable logops-recursive-definitions-theory))))

(defthm loghead-integer-length
  (implies
   (and (integerp x) (<= 0 x))
   (equal (loghead (integer-length x) x)
	  x))
  :hints (("goal" :in-theory (enable integer-length logops-recursive-definitions-theory)
	   :induct (logcdr-induction x))))

(defthm logbitp-integer-length
  (implies
   (and (integerp x) (< 0 x))
   (logbitp (1- (integer-length x)) x))
  :hints (("goal" :in-theory (enable integer-length logops-recursive-definitions-theory)
	   :induct (logcdr-induction x))))

(defthm integer-length-pos
  (equal 
   (< 0 (integer-length x))
   (and (not (zip x)) (not (equal x -1))))
  :hints (("goal" :in-theory (enable integer-length))))

(defthm top-bit-must-be-set
  (implies
   (and
    (not (logbitp n x))
    (integerp n) (integerp x) (<= 0 x) (<= 0 n))
   (equal
    (equal (integer-length x) (1+ n))
    nil))
  :hints (("goal" :in-theory (enable integer-length logops-recursive-definitions-theory)
	   :induct (sub1-logcdr-induction n x))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; We define m, a machine with 2 simple processes

(defun a0 (st) (nth 0 st)) (defun update-a0 (v st) (update-nth 0 v st))
(defun a1 (st) (nth 1 st)) (defun update-a1 (v st) (update-nth 1 v st))
(defun apc (st) (nth 2 st)) (defun update-apc (v st) (update-nth 2 v st))
(defun b0 (st) (nth 3 st)) (defun update-b0 (v st) (update-nth 3 v st))
(defun b1 (st) (nth 4 st)) (defun update-b1 (v st) (update-nth 4 v st))
(defun bpc (st) (nth 5 st)) (defun update-bpc (v st) (update-nth 5 v st))
(defun c (st) (nth 6 st)) (defun update-c (v st) (update-nth 6 v st))

(defun ticka (st)
  (case (apc st)
	(0 (update-apc 1 (update-a0 (c st) st)))
	(1 (update-apc 2 (update-a1 (c st) st)))
	(t (update-apc 0 (update-c (+ (a0 st) (a1 st)) st)))))

(defun tickb (st)
  (case (bpc st)
	(0 (update-bpc 1 (update-b0 (c st) st)))
	(1 (update-bpc 2 (update-b1 (c st) st)))
	(t (update-bpc 0 (update-c (+ (b0 st) (b1 st)) st)))))

(defun tick (st p)
  (if (equal p 'a)
      (ticka st)
    (tickb st)))

(defun m (st o)
  (if (not (consp o))
      st
    (m (tick st (car o)) (cdr o))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Rules about m
(defun st-p (st)
  (and
   (equal (len st) 7)
   (true-listp st)
   (integerp (nth 0 st))
   (integerp (nth 1 st))
   (integerp (nth 2 st))
   (integerp (nth 3 st))
   (integerp (nth 4 st))
   (integerp (nth 5 st))
   (integerp (nth 6 st))))

(defthm len-m
  (implies
   (equal (len st) 7)
   (equal (len (m st o)) 7))
  :hints (("goal" :in-theory (enable len))))

(defthm true-listp-m
  (implies
   (true-listp st)
   (true-listp (m st o))))

(defthm m-preserves-element-types
  (implies
   (st-p st)
   (and
    (integerp (nth 0 (m st o)))
    (integerp (nth 1 (m st o)))
    (integerp (nth 2 (m st o)))
    (integerp (nth 3 (m st o)))
    (integerp (nth 4 (m st o)))
    (integerp (nth 5 (m st o)))
    (integerp (nth 6 (m st o))))))

(defthm m-append
  (equal
   (m st (append x y))
   (m (m st x) y))
  :hints (("goal" :in-theory (disable tick))))

(defthm m-cons
  (equal
   (m st (cons x y))
   (m (tick st x) y))
  :hints (("goal" :in-theory (disable tick))))

(defthm m-nlistp
  (implies
   (not (consp l))
   (equal (m st l) st)))

(in-theory (disable m))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; We define code, a function that calculates an oracle that leads m
;; to a specified "target" value.  (Note that cur is the bit position
;; of target currently accounted for in the machine.)

(defun loopcode (cur target)
  (declare (xargs :measure (max 0 (- (integer-length target) (nfix cur)))
		  :hints (("goal" :in-theory (enable max)))))
  (if (and (integerp cur) (<= 0 cur) (< (1+ cur) (integer-length target)))
      (append
       '(b b b)
       (if (logbitp (1+ cur) target) '(a a a) nil)
       (loopcode (1+ cur) target))
    nil))

(defun repeat-list (n l)
  (if (zp n)
      nil
    (append l (repeat-list (1- n) l))))

(defun code (target)
  (append
   (append (repeat-list (lsb target) '(a a a)) '(a b b))
   (loopcode (lsb target) target)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; An invariant that holds before every execution of the execution
;; sequence generated by loopcode

(defun invariant (cur target st)
  (and
   (st-p st)
   (equal (c st) (if (logbitp cur target) (a0 st) (b0 st)))
   (equal (a0 st) (loghead (1+ cur) target))
   (equal (b0 st) (b1 st))
   (equal (b0 st) (expt 2 cur))
   (equal (bpc st) 2)
   (equal (apc st) 1)
   (integerp target) (< 0 target)
   (integerp cur) (<= 0 cur)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; We prove that the invariant is established by the initialization
;; sequence generated by code

(defun m-repeat-list-aaa-induction (n st)
  (if (zp n) st
    (m-repeat-list-aaa-induction 
     (1- n)
     (m st '(a a a)))))

(defthm m-repeat-list-aaa
  (implies
   (and
    (equal (apc st) 0)
    (st-p st))
   (equal 
    (m st (repeat-list n '(a a a)))
    (if (zp n)
	st
      (update-c 
       (ash (c st) (nfix n))
       (update-a0
	(ash (c st) (1- n))
	(update-a1
	 (ash (c st) (1- n)) st))))))
  :hints (("goal" :induct (m-repeat-list-aaa-induction n st)
	   :in-theory (enable logops-recursive-definitions-theory))))

;; Assumptions about the initial state: pcs initialized and register
;; set to 1.
(defun init-p (st)
  (and
   (equal (apc st) 0)
   (equal (bpc st) 0)
   (equal (c st) 1)))

(defthm init-establishes-invariant
  (implies
   (and
    (st-p st)
    (init-p st)
    (integerp target) (< 0 target))
   (invariant (lsb target) target (m (m st (repeat-list (lsb target) '(a a a))) '(a b b)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Invariant is preserved during computation

(defun loopcode-preserves-invariant-induction (cur target st)
  (declare (xargs :measure (max 0 (- (integer-length target) (nfix cur)))
		  :hints (("goal" :in-theory (enable max)))))
  (if (and (integerp cur) (<= 0 cur) (< (1+ cur) (integer-length target)))
      (loopcode-preserves-invariant-induction 
       (1+ cur)
       target
       (m st
	  (append '(b b b)
		  (if (logbitp (1+ cur) target) '(a a a) nil))))
    (c st)))

(defthm loopcode-preserves-invariant
  (implies
   (and
    (invariant cur target st)
    (< cur (integer-length target)))
   (invariant (1- (integer-length target)) target (m st (loopcode cur target))))
  :hints (("goal" :induct (loopcode-preserves-invariant-induction cur target st))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The invariant leads directly to the final theorem

(defthm invariant-implies-target-computed
  (implies
   (invariant (1- (integer-length target)) target st)
   (equal (equal (c st) target) t)))

(defthm code-works
  (implies (and (st-p st) (init-p st)
		(integerp target) (< 0 target))
	   (equal (c (m st (code target))) target))
  :hints (("goal" :in-theory 
	   (union-theories 
	    (current-theory 'ground-zero)
	    '(init-establishes-invariant
	      loopcode-preserves-invariant
	      code m-append <-lsb-integer-length
	      invariant-implies-target-computed)))))

#| 
For example...

(defun init () '(0 0 0 0 0 0 1))

ACL2 !>(st-p (init))
T
ACL2 !>(init-p (init))
T
ACL2 !>(m (init) (code 39))
(39 32 1 32 32 2 39)
ACL2 !>

|#