#|

Lab 11

In this lab we will explore observational equivalence.  Make sure you
have read and you understand section 8.3 of the lecture notes, as most
of the code in this file is from that section.

First, here is the definition of in, a function we have seen numerous
times.

|#

(definec in (a :all X :tl) :bool
  (and (consp X)
       (or (equal a (car X))
           (in a (cdr X)))))

#|

Next, recall the representation of stacks from the lecture notes.

|#

(defdata element all)

; Data definition of a stack: a list of elements
(defdata stack (listof element))

; Data definition of an empty stack
(defdata empty-stack nil)

; Data definition of a non-empty stack
(defdata non-empty-stack (cons element stack))

; Empty, non-empty stacks are stacks
(defdata-subtype empty-stack stack)
(defdata-subtype non-empty-stack stack)

; Stack creation: returns an empty stack
(definec new-stack () :empty-stack 
  nil)

; The push operation inserts e on the top of the stack s
(definec stack-push (e :element s :stack) :non-empty-stack
  (cons e s))

; The pop operation removes the top element of a non-empty stack 
(definec stack-pop (s :non-empty-stack) :stack
  (rest s))

; The head of a non-empty stack
(definec stack-head (s :non-empty-stack) :element
  (first s))

#|

Next we have the definitions from 8.3 of the lecture notes, where we
defined what an external observer of our stack library can see.

|#

(defdata operation
  (oneof 'empty? (list 'push element) 'pop 'head))

(defdata observation
  (oneof (list boolean) (list element) nil 'error))

(definec external-observation (s :stack o :operation) :observation 
  (cond ((equal o 'empty?)
         (list (empty-stackp s)))
        ((consp o) (list (second o)))
        ((equal o 'pop) (if (empty-stackp s) 'error nil))
        (t (if (empty-stackp s) 'error (list (stack-head s))))))

(check= (external-observation '(1 2) '(push 4))
        '(4))

(check= (external-observation '(1 2) 'pop)
        '())

(check= (external-observation '(1 2) 'head)
        '(1))

(check= (external-observation '(1 2) 'empty?)
        '(nil))

(test? (implies (and (stackp s) (elementp e))
                (equal (external-observation s (list 'push e))
                       (list e))))

(test? (implies (and (non-empty-stackp s))
                (equal (external-observation s 'pop)
                       nil)))

(test? (implies (empty-stackp s)
                (equal (external-observation s 'pop)
                       'error)))

(test? (implies (empty-stackp s)
                (equal (external-observation s 'head)
                       'error)))

(test? (implies (and (stackp s) (elementp e))
                (equal (external-observation (stack-push e s) 'head)
                       (list e))))

(test? (implies (non-empty-stackp s)
                (equal (external-observation s 'empty?)
                       (list nil))))

(test? (implies (empty-stackp s)
                (equal (external-observation s 'empty?)
                       (list t))))

(defdata lop (listof operation))

(defdata lob (listof observation))

(definec update-stack (s :stack op :operation) :stack
  (cond ((in op '(empty? head))
         s)
        ((equal op 'pop)
         (if (empty-stackp s)
             (new-stack)
           (stack-pop s)))
        (t (stack-push (second op) s))))

(definec external-observations (s :stack l :lop) :lob
  (if (endp l) 
      nil
    (let* ((op (first l))
           (ob (external-observation s op)))
      (if (equal ob 'error)
          '(error)
        (cons ob (external-observations
                  (update-stack s op) (rest l)))))))

(check= (external-observations 
         (new-stack) 
         '(head ))
        '(error))

(check= (external-observations 
         (new-stack)
         '( (push 1)
            pop
            (push 2)
            (push 3)
            pop
            head
            empty?
            pop
            empty? ))
        '( (1)
           ()
           (2)
           (3)
           ()
           (2)
           (nil)
           ()
           (t) ))

(check= (external-observations 
         (new-stack)
         '( (push 1)
            pop
            pop
            pop
            empty? ))
        '( (1)
           ()
           error))

(check= (external-observations 
         (new-stack)
         '( (push nil)
            (push error)
            (push pop)
            empty?
            head
            pop
            empty?
            head
            pop
            empty?
            head
            pop
            empty?
            head
            pop))
        '( (nil)
           (error)
           (pop)
           (nil)
           (pop)
           ()
           (nil)
           (error)
           ()
           (nil)
           (nil)
           ()
           (t)
           error))

#|

Q1.

We will change the representation of stacks so that the size is
recorded in the stack.  Therefore, we define a new datatype stack-sz
that is a cons whose car is a nat, the size of the stack, and whose
cdr is a stack.

|#

(defdata stack-sz (cons nat stack))

; An empty stack-sz (recall that (cons 0 nil) = (0)
(defdata empty-stack-sz '(0))

; Data definition of a non-empty stack-sz
(defdata non-empty-stack-sz (cons pos non-empty-stack))

; Empty, non-empty stacks are stacks
(defdata-subtype empty-stack-sz stack-sz)
(defdata-subtype non-empty-stack-sz stack-sz)

#|

Next, we define all the other operations that modify the stack so that
they correctly update the size. This will allow us to determine the
size without traversing the stack.

|#

#|
Q1A.

Finish the definition.
|#

; Stack creation: returns an empty stack
(definec new-stack-sz () ...
   ...)

#|
Q1B.

Finish the definition.
|#

; The size of a stack
(definec stack-sz-size (s ...) ...
  ...)

#|
Q1C.

Finish the definition.
|#

; The head of a non-empty stack
(definec stack-sz-head (s ...) ...
  ...)

#|

We want any functions that modify our stack to preserve the invariant
that the size is correct and we want to put that into the contracts.

First, we define the invariant.

|#

(definec stack-sz-invariant (s :all) :bool
  (and (stack-szp s)
       (equal (car s) (len (cdr s)))))

#|
Q1D.

Finish the definition.
|#

; The push operation inserts e on the top of the stack s
(defunc stack-sz-push (e s)
  :input-contract (and (elementp e)
                       (stack-sz-invariant s))
  :output-contract (and (non-empty-stack-szp (stack-sz-push e s))
                        (stack-sz-invariant (stack-sz-push e s)))
  ...)

#|
Q1E.

Finish the definition.
|#

; The pop operation removes the top element of a non-empty stack 
(defunc stack-sz-pop (s) 
  :input-contract (and (stack-sz-invariant s) (non-empty-stack-szp s))
  :output-contract (stack-sz-invariant (stack-sz-pop s))
  ...)


#|

Q2.

Next we define what an external observer of our stack-sz library can
see.

|#

(defdata operation-sz (oneof operation 'size))

(defdata observation-sz (oneof observation (list nat)))


#|
Q2A.

Finish the definition.
|#

(defunc external-observation-sz (s o)
  :input-contract (and (stack-sz-invariant s)
                       (operation-szp o))
  :output-contract (observation-szp (external-observation-sz s o))
  ...)

(defdata lop-sz (listof operation-sz))

(defdata lob-sz (listof observation-sz))


#|
Q2B.

Finish the definition.
|#

(defunc update-stack-sz (s op)
  :input-contract (and (stack-sz-invariant s)
                       (operation-szp op))
  :output-contract (stack-sz-invariant (update-stack-sz s op))
  ...)


#|
Q2C.

Finish the definition.
|#

(defunc external-observations-sz (s l)
  :input-contract (and (stack-sz-invariant s)
                       (lop-szp l))
  :output-contract (lob-szp (external-observations-sz s l))
  ...)


#|

Q3.

Write a property claiming that the two stack implementations are
observationally equivalent if there are no size operations.

Make sure ACL2s does not complain.

|#

(test?
 (implies ...
          ...))

#|
Q4.

Write a property claiming that the two stack implementations are
observationally equivalent even if there are size operations.

Make sure ACL2s does complain.

|#

(test?
 (implies ...
          ...))

#|

Extra problem: Prove the property in Q3.

...

|#