;;;-*-Lisp-*-

(BG_PUSH
 (AND
  (FORALL (i N)
    (IMPLIES (AND (>= i 0) (< i N)) (EQ (mod1 i N) i)))
  (FORALL (i N)
    (IMPLIES (>= i N) (EQ (mod1 i N) (- i N))))
  (FORALL (i N)
    (IMPLIES (< i 0) (EQ (mod1 i N) (+ i N))))
  ))

(DEFPRED (RepInv l r s n)
  (AND
   (LBL PhysQueueSize (> n 0))
   (LBL RInRange (AND (<= 0 r) (< r n)))
   (LBL LInRange (AND (<= 0 l) (< l n)))
   (OR
    (LBL FullQueue
      (AND (EQ r (mod1 (+ l 1) n))
	   (FORALL (i)
	     (IMPLIES
	      (AND (<= 0 i) (< i n))
	      (NEQ (select s i) 0))))
      )
    (LBL Wrapped
      (AND (<= r l)
	   (FORALL (i)
	     (IMPLIES
	      (AND (<= 0 i) (< i n))
	      (IFF (AND (>= i r) (<= i l))
		   (EQ (select s i) 0)))
	     )))
    (LBL NotWrapped
      (AND (> r l)
	   (FORALL (i)
	     (IMPLIES
	      (AND (<= 0 i) (< i n))
	      (IFF (AND (> i l) ( < i r))
		   (NEQ (select s i) 0)))
	     )))
    )))

;;; abs-queue.simp

(BG_PUSH
 ;; Forget about normal forms!
 ;; We will consider EmptyQ, singleton, and concat as the constructors.
 ;; All the non-constructors will be defined over these constructors. 

 ;; As distinct constructors that are normal forms, they are distinct.
 (FORALL (v) (NEQ (singleton v) EmptyQ))
 (FORALL (q1 q2)
   (PATS (NEQ (concat q1 q2) EmptyQ))
   (IMPLIES (NEQ q1 EmptyQ) (NEQ (concat q1 q2) EmptyQ)))
 (FORALL (q1 q2)
   (PATS (NEQ (concat q1 q2) EmptyQ))
   (IMPLIES (NEQ q2 EmptyQ) (NEQ (concat q1 q2) EmptyQ)))

 ;; EmptyQ is a left and right identity for concat.
 (FORALL (q) (EQ (concat q EmptyQ) q))
 (FORALL (q) (EQ (concat EmptyQ q) q))

 ;; concat is associative.
 (FORALL (q1 q2 q3) (EQ (concat q1 (concat q2 q3))
			(concat (concat q1 q2) q3)))

 ;; Define pushL and pushR
 (FORALL (q v)
   (PATS (pushL q v))
   (EQ (pushL q v) (concat (singleton v) q)))
 (FORALL (q v)
   (PATS (pushR q v))
   (EQ (pushR q v) (concat q (singleton v))))

 ;; Now define the peek observers, peekR and peekL.  Neither is defined on
 ;; empty queues.
 (FORALL (v)
   (PATS (peekR (singleton v)))
   (EQ (peekR (singleton v)) v))
 (FORALL (q1 q2)
   (PATS (peekR (concat q1 q2)))
   (IMPLIES (NEQ q2 EmptyQ)
	    (EQ (peekR (concat q1 q2)) (peekR q2))))

 (FORALL (v)
   (PATS (peekL (singleton v)))
   (EQ (peekL (singleton v)) v))
 (FORALL (q1 q2)
   (PATS (peekL (concat q1 q2)))
   (IMPLIES (NEQ q1 EmptyQ)
	    (EQ (peekL (concat q1 q2)) (peekL q1))))

 ;; Now we define "pop" mutators.
 (FORALL (v)
   (PATS (popR (singleton v)))
   (EQ (popR (singleton v)) EmptyQ))
 (FORALL (q1 q2)
   (PATS (popR (concat q1 q2)))
   (IMPLIES (NEQ q2 EmptyQ)
	    (EQ (popR (concat q1 q2)) (concat q1 (popR q2))))) 

 (FORALL (v)
   (PATS (popL (singleton v)))
   (EQ (popL (singleton v)) EmptyQ))
 (FORALL (q1 q2)
   (PATS (popL (concat q1 q2)))
   (IMPLIES (NEQ q1 EmptyQ)
	    (EQ (popL (concat q1 q2)) (concat (popL q1) q2))))

 ;; We define a len function, for use in induction.
 (EQ (len EmptyQ) 0)
 (FORALL (v) (EQ (len (singleton v)) 1))
 (FORALL (q1 q2)
   (PATS (len (concat q1 q2)))
   (EQ (len (concat q1 q2)) (+ (len q1) (len q2))))
)

;; Now we will attempt to prove some derived fact about pushL by data
;; type induction, then assume them for all queues, namely:
;;   (FORALL (q v) (NEQ (pushL q v) EmptyQ))
;(FORALL (v) (NEQ (pushL EmptyQ v) EmptyQ))
;(FORALL (q v1 v2) (NEQ (pushL (pushR q v1) v2) EmptyQ))
;; From these we conclude:
;(BG_PUSH (FORALL (q v) (NEQ (pushL q v) EmptyQ)))

;(LEMMA
(BG_PUSH
 (FORALL (q v)
   (PATS (len (pushL q v)))
   (EQ (len (pushL q v)) (+ (len q) 1)))
 )

(>= (len EmptyQ) 0)
(FORALL (v) (>= (len (singleton v)) 0))
(FORALL (q1 q2)
  (IMPLIES (AND (>= (len q1) 0)
		(>= (len q2) 0))
	   (>= (len (concat q1 q2)) 0)))


;; Therefore we can assume by data type induction:
(BG_PUSH
 (FORALL (q) (PATS (len q)) (>= (len q) 0)))

;;; end of abs-queue.simp

(BG_PUSH
 ;; Define AbsFuncContig
 (FORALL (s i)
   (EQ (AbsFuncContig s i i) EmptyQ))
 ;; We introduce AbsFuncContigRest here to control the matching...
 (FORALL (i j s)
   (PATS (AbsFuncContig s i j))
   (IMPLIES (< i j)
	    (EQ (AbsFuncContig s i j)
		(pushR (AbsFuncContigRest s i (- j 1))
		       (select s (- j 1))))))
 ;; ...but it's really just another name for the same function.
 (FORALL (i j s)
   (PATS (AbsFuncContig s i j))
   (EQ (AbsFuncContig s i j) (AbsFuncContigRest s i j)))

 (FORALL (s i)
   (EQ (AbsFuncContigRest s i i) EmptyQ))

 ;; Now define AbsFunc in terms of AbsFuncContig.

 ;; Full case
 (FORALL (s l r n)
   (PATS (AbsFunc s l r n))
   (IMPLIES (AND (NEQ (select s l) 0)
		 (EQ r (mod1 (+ l 1) n)))
	    (EQ (AbsFunc s l r n)
		(concat (AbsFuncContig s r n)
			(AbsFuncContig s 0 r)
			))))

 ;; Empty case
 (FORALL (s l r n)
   (PATS (AbsFunc s l r n))
   (IMPLIES (AND (EQ (select s l) 0)
		 (EQ r (mod1 (+ l 1) n)))
	    (EQ (AbsFunc s l r n) EmptyQ)))

 ;; Non-wrapped.
 (FORALL (s r l n)
   (PATS (AbsFunc s l r n))
   (IMPLIES
    (AND (NEQ r (mod1 (+ l 1) n))
	 (> r l))
    (EQ (AbsFunc s l r n) (AbsFuncContig s (+ l 1) r))))

 ;; Wrapped case.
 (FORALL (s r l n)
   (PATS (AbsFunc s l r n))
   (IMPLIES
    (AND (NEQ r (mod1 (+ l 1) n))
	 (<= r l))
    (EQ (AbsFunc s l r n)
	(concat (AbsFuncContig s (+ l 1) n)
		(AbsFuncContig s 0 r)))))
 )

;; We wish to prove the formula in the next BG_PUSH.
;; We do so by induction over the natural numbers; that is, prove instead
;(FORALL (s l k i v)
;  (IMPLIES (>= k 0)
;	   (IMPLIES (OR (< i l) (>= i (+ l k)))
;		    (EQ (AbsFuncContig (store s i v) l (+ l k))
;			(AbsFuncContig s l (+ l k))))))
;
; First the base case:
(FORALL (s l k i v)
  (IMPLIES (EQ k 0)
	   (IMPLIES (OR (< i l) (>= i (+ l k)))
		    (EQ (AbsFuncContig (store s i v) l (+ l k))
			(AbsFuncContig s l (+ l k))))))

;; Now the induction step.
(FORALL (n)
  (IMPLIES
   (>= n 0)
   (IMPLIES
    ;; As it happens, we need to use "AbsFuncContigRest" here, to make
    ;; the recursion work out right.  But there's no semantic difference.
    (FORALL (s l r i v)
      (IMPLIES (AND (>= r l) (<= (- r l) n))
	       (IMPLIES (OR (< i l) (>= i r))
			(EQ (AbsFuncContigRest (store s i v) l r)
			    (AbsFuncContigRest s l r)))))
    (FORALL (s l r i v)
      (IMPLIES (AND (>= r l) (<= (- r l) (+ n 1)))
	       (IMPLIES (OR (< i l) (>= i r))
			(EQ (AbsFuncContig (store s i v) l r)
			    (AbsFuncContig s l r)))))
    )))


;; We we are justified in concluding the following:      
(BG_PUSH
 (FORALL (s l r i v)
   (IMPLIES (AND (>= r l) (OR (< i l) (>= i r)))
	    (EQ (AbsFuncContig (store s i v) l r)
		(AbsFuncContig s l r))))

 ;; And we assume the same thing for AbsFuncContigRest.
 (FORALL (s l r i v)
   (IMPLIES (AND (>= r l) (OR (< i l) (>= i r)))
	    (EQ (AbsFuncContigRest (store s i v) l r)
		(AbsFuncContigRest s l r))))

 )

;; The next BG_PUSH is another fact we prove by induction.
(FORALL (s l)
   (PATS (len (AbsFuncContig s l (+ l 0))))
   (EQ (len (AbsFuncContig s l (+ l 0))) (- (+ l 0) l)))

(FORALL (s l n)
  (IMPLIES
   (AND
    (>= n 0)
    (>= l 0)
    (FORALL (k)
      ;; This is done in terms of "AbsFuncContigRest" to get necessary
      ;; matching.
      (PATS (len (AbsFuncContigRest s l k)))
      (IMPLIES (AND
		(>= k l)
		(<= (- k l) n))
	       (EQ (len (AbsFuncContigRest s l k)) (- k l)))))
   (EQ (len (AbsFuncContig s l (+ l (+ n 1)))) (- (+ l (+ n 1)) l))))

;; From this we can assume the above for all n:
(BG_PUSH
 (FORALL (s l r)
   (PATS (len (AbsFuncContig s l r)))
   (IMPLIES (>= r l)
	    (EQ (len (AbsFuncContig s l r)) (- r l))))
 )

;; Finally (I hope!) we need a rule that exposes the left side of an
;; AbsFuncContig; namely the fact in the next BG_PUSH.  We prove this
;; by induction.

;; Base case
(FORALL (i s)
  (IMPLIES (AND (>= i 0) (< i (+ (+ i 1) 0)))
	   (EQ (AbsFuncContig s i (+ (+ i 1) 0))
	       (pushL (AbsFuncContigRest s (+ i 1) (+ (+ i 1) 0))
		      (select s i)))))
(FORALL (n)
  (IMPLIES
   (AND (>= n 0)
	(FORALL (i j s)
	  (PATS (AbsFuncContigRest s i j))
	  (IMPLIES (AND (< i j) (<= (- j i) n))
		   (EQ (AbsFuncContigRest s i j)
		       (pushL (AbsFuncContigRest s (+ i 1) j)
			      (select s i))))))
   (FORALL (s i)
     (EQ (AbsFuncContig s i (+ i (+ n 1)))
	 (pushL (AbsFuncContig s (+ i 1) (+ i (+ n 1)))
		(select s i))))))

;; Since the above is true for all n, we can assume the general form.
(BG_PUSH
 (FORALL (i j s)
   (PATS (AbsFuncContig s i j))
   (IMPLIES (< i j)
	    (EQ (AbsFuncContig s i j)
		(pushL (AbsFuncContigRest s (+ i 1) j)
		       (select s i)))))
)

;; Now, the proof obligations.

;; The initial conditions satisfy the rep invariant and represent the
;; empty abstract queue.
(FORALL (S n)
  (IMPLIES
   (AND
    (>= n 1)
    (FORALL (i)
      (IMPLIES
       (AND (<= 0 i) (< i n))
       (EQ (select S i) 0)))
    )
   (AND
    (RepInv 0 (mod1 1 n) S n)
    (EQ (AbsFunc S 0 (mod1 1 n) n) EmptyQ)
    )))

;; PopR line 8; return at line 10
;; also, same VC for
;; PopR line 14 unsuccessful; return at line 18
(FORALL (r l s n)
  (IMPLIES (AND
	    (RepInv l r s n)
	    (EQ (select s (mod1 (- r 1) n)) 0))
	   (EQ (AbsFunc s l r n) EmptyQ))
   )
;; PopR line 14 successful; return at line 16
(FORALL (r l s n)
  (IMPLIES
   (AND (RepInv l r s n)
	(NEQ (select s (mod1 (- r 1) n)) 0)
	)
   (AND
    (LBL RepInvPreserved
      (RepInv l (mod1 (- r 1) n) (store s (mod1 (- r 1) n) 0) n)
      )
    (LBL QNotEmpty
      (NEQ (AbsFunc s l r n) EmptyQ))
    (LBL ProperTransition
      (EQ (AbsFunc (store s (mod1 (- r 1) n) 0)
		   l (mod1 (- r 1) n) n)
	  (popR (AbsFunc s l r n))))
    (LBL ProperReturnVal
      (EQ (peekR (AbsFunc s l r n)) (select s (mod1 (- r 1) n))))
    )))

;; PushR line 8 successful; return at line 10
(FORALL (r l s n)
  (IMPLIES (AND (RepInv l r s n)
		(NEQ (select s r) 0)
		)
	   (EQ (len (AbsFunc s l r n)) n)))

;; PushR line 14 successful; return at line 16
(FORALL (r l s n v)
  (IMPLIES (AND (RepInv l r s n)
		(EQ (select s r) 0)
		(NEQ v 0)
		)
	   (AND
	    (LBL RepInvPreserved
	      (RepInv l (mod1 (+ r 1) n) (store s r v) n))
	    (LBL QNotFull
	      (< (len (AbsFunc s l r n)) n))
	    (LBL ProperTransition
	      (EQ (AbsFunc (store s r v)
			   l (mod1 (+ r 1) n) n)
		  (pushR (AbsFunc s l r n) v)))
	    )))

;; PopL line 8; return at line 10
;; also, same VC for
;; PopL line 14 unsuccessful; return at line 18
(FORALL (r l s n)
  (IMPLIES (AND
	    (RepInv l r s n)
	    (EQ (select s (mod1 (+ l 1) n)) 0))
	   (EQ (AbsFunc s l r n) EmptyQ))
  )

;; PopL line 14 successful; return at line 16
(FORALL (r l s n)
  (IMPLIES (AND (RepInv l r s n)
		(NEQ (select s (mod1 (+ l 1) n)) 0)
		)
	   (AND
	    (LBL RepInvPreserved
	      (RepInv (mod1 (+ l 1) n) r (store s (mod1 (+ l 1) n) 0) n))
	    (LBL QNotEmpty
	      (NEQ (AbsFunc s l r n) EmptyQ))
	    (OR FALSE
		(LBL ProperTransition
		  (EQ (AbsFunc (store s (mod1 (+ l 1) n) 0)
			       (mod1 (+ l 1) n) r n)
		      (popL (AbsFunc s l r n))))
		)
	    (OR TRUE
		(LBL ProperReturnVal
		  (EQ (peekL (AbsFunc s l r n)) (select s (mod1 (+ l 1) n))))
		)
	    )))

;; PushL line 8 successful; return at line 10
(FORALL (r l s n)
  (IMPLIES (AND (RepInv l r s n)
		(NEQ (select s l) 0)
		)
	   (EQ (len (AbsFunc s l r n)) n)))

;; PushL line 14 successful; return at line 16
(FORALL (r l s n v)
  (IMPLIES (AND (RepInv l r s n)
		(EQ (select s l) 0)
		(NEQ v 0)
		)
	   (AND
	    (LBL RepInvPreserved
	      (RepInv (mod1 (- l 1) n) r (store s l v) n))
	    (LBL QNotFull
	      (< (len (AbsFunc s l r n)) n))
	    (LBL ProperTransition
	      (EQ (AbsFunc (store s l v)
			   (mod1 (- l 1) n) r n)
		  (pushL (AbsFunc s l r n) v)))
	    )))