; ****************** BEGIN INITIALIZATION FOR ACL2s MODE ****************** ;
; (Nothing to see here!  Your actual file is after this initialization code);
(make-event
 (er-progn
  (set-deferred-ttag-notes t state)
  (value '(value-triple :invisible))))

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading the CCG book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "acl2s/ccg/ccg" :uncertified-okp nil :dir :system :ttags ((:ccg)) :load-compiled-file nil);v4.0 change

;Common base theory for all modes.
#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s base theory book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "acl2s/base-theory" :dir :system :ttags :all)


#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s customizations book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "acl2s/custom" :dir :system :ttags :all)

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem setting up ACL2s mode.") (value :invisible))

;Settings common to all ACL2s modes
(acl2s-common-settings)
;(acl2::xdoc acl2s::defunc) ;; 3 seconds is too much time to spare -- commenting out [2015-02-01 Sun]

(acl2::xdoc acl2s::defunc) ; almost 3 seconds

; Non-events:
;(set-guard-checking :none)

(acl2::in-package "ACL2S")

; ******************* END INITIALIZATION FOR ACL2s MODE ******************* ;
;$ACL2s-SMode$;ACL2s
#|

CS 2800 Homework 3 - Spring 2019

This homework is done in groups. 

 * Groups should consist of 2-3 people.

 * One group member will create a group in BlackBoard. See the class Webpage for
   instructions on how to do that.
 
 * Other group members then join the group. 

 * Homework is submitted by only one person per group. Therefore make sure the
   person responsible for submitting actually does so. If that person forgets to
   submit, your team gets 0.

   - We recommend that groups email confirmation messages and submit early and
     often. 

 * Submit the homework file (this file) on Blackboard.  Do not rename 
   this file.  There will be a 10 point penalty for this.
   When done, save your file and submit it as hwk03.lisp.

 * You must list the names of ALL group members below, using the given
   format. This way we can confirm group membership with the BB groups.  If you
   fail to follow these instructions, it costs us time and it will cost you
   points, so please read carefully.

The format should be: FirstName1 LastName1, FirstName2 LastName2, ...
For example:
Names of ALL group members: Frank Sinatra, Billy Holiday

There will be a 10 pt penalty if your names do not follow this format.

Replace "..." below with the names as explained above.

Names of ALL group members: ...

* Later in the term if you want to change groups, the person who created the
  group should stay in the group. Other people can leave and create other groups
  or change memberships.  See the class Webpage.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

For this homework you will need to use ACL2s.

Technical instructions:

- Open this file in ACL2s.

- Make sure you are in ACL2s mode. This is essential! Note that you can
  only change the mode when the session is not running, so set the correct
  mode before starting the session.

- Insert your solutions into this file where indicated (usually as "...").
  Sometimes we require textual explanations (e.g., complexity analysis below)
  so just add your explanation inside the ACL2s comments.

- Only add to the file. Do not remove or comment out anything pre-existing.

- Make sure the entire file is accepted by ACL2s. In particular, there must
  be no "..." left in the code. If you don't finish all problems, comment
  the unfinished ones out. Comments should also be used for any English
  text that you may add. This file already contains many comments, so you
  can see what the syntax is. We will deduct points for files that are
  not accepted by ACL2s: we sometimes ask explicitly to insert your
  answer in the comments, when the answer is not to be accepted by ACL2s.
  When asked to insert your answer in the comments, do so.

- Do not submit the session file (which shows your interaction with the theorem
  prover). This is not part of your solution. Only submit the lisp file.

Instructions for programming problems:

For each function definition, you must provide both contracts and a body.

You must also ALWAYS supply your own tests. This is in addition to the
tests sometimes provided. Make sure you produce sufficiently many new test
cases. This means: cover at least the possible scenarios according to the
data definitions of the involved types. For example, a function taking two
lists should have at least 4 tests: all combinations of each list being
empty and non-empty.

Beyond that, the number of tests should reflect the difficulty of the
function. For very simple ones, the above coverage of the data definition
cases may be sufficient. For complex functions with numerical output, you
want to test whether it produces the correct output on a reasonable
number of inputs.

Use good judgment. For unreasonably few test cases we will deduct points.

We will use ACL2s' check= function for tests. This is a two-argument
function that rejects two inputs that do not evaluate equal. You can think
of check= roughly as defined like this:

(defunc check= (x y)
  :input-contract (equal x y)
  :output-contract (equal (check= x y) t)
  t)

That is, check= only accepts two inputs with equal value. For such inputs, t
(or "pass") is returned. For other inputs, you get an error. If any check=
test in your file does not pass, your file will be rejected.

We will again use the following directives to allow ACL2s to proceed 
even if a proof fails (do not remove them):

|#

(set-defunc-termination-strictp nil)
(set-defunc-function-contract-strictp nil)
(set-defunc-body-contracts-strictp nil)

#|
This homework focuses on property-based testing.

IMPORTANT!
Go over the entire homework once before you start, as some later
parts build upon earlier ones.

Part I: Modeling a memory

A memory can be seen as a table of pairs of the form (address, data).

1.
Define using defdata an address which should be a natural number,
a piece of data which could be anything, and finally a memory, 
which is a list of (address, data) pairs.

|#

(defdata address ...
(defdata data ...
(defdata mem ...

(check= (addressp 0) t)
(check= (addressp "st") nil)

(check= (datap '(1 2/3 3)) t)
(check= (datap '(1 "2/3" 3)) t)
(check= (datap nil) t)

(check= (memp '((1 . "stavros") (2 . "pete"))) t)
(check= (memp '((1 . "stavros") (2 ))) t)
(check= (memp ()) t)


#|

2.
Define a function "readmem" which takes a memory and an address
and returns the data associated with that address.
In the contracts of the function use the recognizers automatically
generated by the data definitions above, e.g., addressp, datap, etc.
Beware: what should happen if the given address is not in the given
memory? Treat this case as forbidden by strengthening the input
contract appropriately. Feel free to add helper functions as needed.

|#

(defunc readmem (m a)
  :input-contract ...
  :output-contract ...
  ...

(check= (readmem '((1 . "stavros") (2 )) 1) "stavros")
(check= (readmem '((1 . "stavros") (2 )) 2) nil)
;; should fail: (check= (readmem '((1 . "stavros") (2 )) 0) nil)


#|
3.
Define a function "writemem" which takes a memory m, an address a, and
a piece of data d, and returns a new memory where the data at address
a has been updated to d. 
Beware: there are two cases: (1) either m already has address a in it, 
or (2) it doesn't. Your code should handle both these cases correctly.
In particular, in case (1) the data at a should be overwritten with d.
In case (2) a new pair (a,d) should be added (somewhere) in m.

The function acons is useful. 
(acons x y z) is equivalent to (cons (cons x y) z)
|#

(definec writemem (m :mem a :address d :data) :mem
  ...

(check= (writemem '((1 . "stavros") (2 )) 1 "pete") ...
(check= (writemem '((1 . "stavros") (2 )) 2 "pete") ...
(check= (writemem '((1 . "stavros") (2 )) 0 "pete") ...
...

#|
Part 2: Property-based testing

Now that our memory implementation is complete, we would like to
test it. We (you should) have already written several tests, but
have we written enough tests? ACL2s offers a powerful mechanism
called property-based testing that we've seen in class. This
mechanism, implemented with "test?", allows us to write properties
that we want to test, and to let ACL2s generate tests to check these
properties automatically.

Before we test our memory implementation, let's warm up:

4.
Write property-based tests for the following properties:
A: if x > 1 then x > 0
B: if l is a non-empty true list, then l is not () (the empty list)
C: the concatenation of a true list l with the empty list () gives l
|#

; answers
;A:
(test? ...
;B:
(test? ...
;C:
(test? ...


#|
Now let's start testing our memory. We will provide the properties
in English.
You will have to write property-based tests for these properties
using test?.

5.
One reasonable property is that "if readmem succeeds for an
address a on a given memory m, then m cannot be empty (i.e., m
cannot be the empty list)". Express this property using test?:
|#

; answer
(test? (implies ...

#|
6.
Another reasonable property is that "if we write data x at address a
on memory m, and then immediately afterwards we read from m at the same
address a, then we should get back x". Express this property using
test?:
|#

; answer
(test? ...

#|
7.
Another reasonable property is that "if we write data x at address a,
and we also write data y at address b, and the addresses a and b differ,
then the order of the writes doesn't matter". That is, writing first
x at a and then y at b, produces the same final memory, as if writing
first y at b and then x at a (because a and b are different addresses).

Write property-based tests using test? to check whether your 
implementation satisfies this property. Does it?
NOTE: do not worry if your implementation does not satisfy the property.
It's fine. Read the rest of the homework and do not get stuck here.
For now we only want you to be able to write down the right property.
|#

; answer:
#|
Complete the test? below:
(test? ...

... explain here in English whether the test fails or not and why ...
|#


#|
8.
If your memory implementation already satisfies the property above, you
can skip this question. You will get the points, don't worry.

If your implementation does not satisfy the property above, again don't
worry. You can still get the max amount of points for this homework.
You will just have to fix your implementation.
That's the whole point of testing. To find bugs in our code and fix them.

First, if your implementation doesn't satisfy the property, explain why:

... write your answer in English here ...

Then, fix your implementation so that it satisfies the property. 
IMPORTANT: KEEP the "buggy" version of your functions that you wrote
above. DO NOT DELETE IT! 
For every function f which is buggy, add a new fixed version called
f-fixed.
Remember to re-run all property-based testings, to make sure your new
implementation still satisfies all of them!
|#

; answer (if your memory implementation was already correct
       ; just define writemem-fixed as writemem)

(defunc writemem-fixed (m a d)
  :input-contract ...
  :output-contract ...
  ...

(check= (writemem-fixed '((1 . "stavros") (2 )) 1 "pete")  ...
(check= (writemem-fixed '((1 . "stavros") (2 )) 2 "pete")  ...
(check= (writemem-fixed '((1 . "stavros") (2 )) 10 "pete") ...

; do not forget to repeat all the tests above, including the
        ; latest test from question 7:
(test? ... 
(test? ...
       
#|
Another reasonable property to expect from memories is that
"the memory cannot have two elements with the same address".
Let's try to express this property using test?. First, we
define some helper functions.
|#

; counts how many times a given address appears in memory:
(definec count-address-occurrences (m :mem a :address) :nat
  (cond ((endp m) 0)
        ((equal a (caar m))
         (+ 1 (count-address-occurrences (rest m) a)))
        (t (count-address-occurrences (rest m) a))))

(check= (count-address-occurrences
         '((1 . "stavros") (2 . "pete")) 1) 1)
(check= (count-address-occurrences () 1) 0)
(check= (count-address-occurrences
         '((1 . "stavros") (1 . "pete")) 1) 2)

; checks whether given address appears multiple times in
; given memory:
(definec has-duplicate-addresses (m :mem) :bool
  (and (consp m)
       (or (> (count-address-occurrences m (caar m)) 1)
           (has-duplicate-addresses (rest m)))))

(check= (has-duplicate-addresses
         '((1 . "stavros") (2 . "pete"))) nil)
(check= (has-duplicate-addresses ()) nil)
(check= (has-duplicate-addresses
         '((1 . "stavros") (1 . "pete"))) t)

#|
9.
We now write the property-based test below. BEFORE executing
the test on ACL2s, think:
Does the test? succeed or fail? If it fails, why does it fail?
|#

#|
(test? (implies
        (memp m)
        (not (has-duplicate-addresses m))))
|#

#|
... write your answer here ...

If the test? above fails, comment it out in order to proceed. Again: we
will deduct points for homework files that are not accepted by ACL2s.
|#

#|
10.
Assuming the property-based test above fails, fix it so that it
doesn't fail. For example, you might want to make the property
more specific: "every memory that can be obtained by the (fixed)
writemem operation defined above has no duplicates".
Is it possible to express such a general property? If not, express
something more specific, along the same lines.

...write your answer in English here...

...then write the property below, outside the comments, using test?.
(you may want to write more than just one "test?" statements):
|#

; answer:
(test? ...

(test? ...