#|
The Imitation Game Lab.

This lab is about encryption. 

Your goal is to decrypt the following two secret messages.

Make sure you are in ACL2s mode.
|#

; This is how we define constants in ACL2s.
; This is an encoded message.
(defconst *code1*
  '((NIL NIL NIL NIL NIL)
    (T NIL T NIL NIL)
    (T NIL T T T)
    (NIL T NIL NIL T)
    (NIL NIL NIL T T)
    (NIL NIL T T T)
    (T T NIL T T)
    (T NIL NIL NIL T)
    (T T NIL NIL T)
    (NIL T NIL NIL T)
    (T NIL NIL T NIL)
    (NIL NIL NIL T NIL)
    (T T T NIL T)
    (NIL NIL T NIL T)
    (T T T T NIL)
    (NIL T NIL NIL T)
    (T NIL T T NIL)
    (T T T NIL T)
    (NIL NIL T NIL NIL)
    (NIL T NIL NIL T)
    (T T NIL T NIL)
    (NIL NIL T T T)
    (T T T T T)
    (T T T NIL NIL)
    (T NIL T T T)
    (T NIL NIL NIL NIL)
    (NIL T NIL NIL T)
    (T T T NIL T)
    (NIL NIL T T NIL)
    (T NIL T T T)
    (NIL NIL NIL T NIL)
    (NIL T NIL NIL T)
    (NIL NIL NIL NIL NIL)
    (T NIL T NIL NIL)
    (T NIL T T T)
    (NIL T NIL NIL T)
    (T T NIL NIL NIL)
    (T NIL NIL T T)
    (NIL T NIL T NIL)
    (NIL T NIL T T)
    (NIL T NIL NIL T)
    (T NIL NIL NIL NIL)
    (T T T NIL T)
    (T NIL T NIL T)
    (NIL T T T NIL)
    (NIL NIL NIL NIL T)
    (NIL T NIL NIL T)
    (T NIL NIL T NIL)
    (T NIL NIL T T)
    (T NIL NIL NIL T)
    (T T NIL NIL T)))

; A second encoded message.
(defconst *code2*
  '((T NIL NIL T NIL)
    (T NIL NIL NIL T)
    (NIL NIL T NIL NIL)
    (T NIL NIL NIL T)
    (NIL T NIL NIL NIL)
    (NIL NIL T T T)
    (NIL T T T T)
    (T NIL NIL T NIL)
    (T NIL NIL NIL T)
    (NIL NIL T NIL NIL)
    (T NIL NIL NIL T)
    (NIL T NIL NIL NIL)
    (NIL NIL T T T)
    (NIL T T T T)
    (NIL NIL T T NIL)
    (T NIL NIL T NIL)
    (T NIL NIL NIL T)
    (NIL T T T T)
    (T NIL T NIL T)
    (T T NIL NIL NIL)
    (NIL NIL T T T)
    (NIL NIL NIL T T)
    (T NIL NIL NIL T)
    (NIL NIL T NIL NIL)
    (NIL T T T T)
    (NIL NIL T T NIL)
    (T T NIL T T)
    (NIL T T T T)
    (NIL NIL T T NIL)
    (T NIL NIL T NIL)
    (T NIL NIL NIL T)
    (NIL T T T T)
    (T T NIL NIL NIL)
    (T NIL NIL NIL T)
    (NIL NIL NIL T NIL)
    (NIL NIL T T NIL)
    (NIL T T T T)
    (NIL NIL T NIL T)
    (NIL NIL NIL NIL T)
    (T T T NIL T)
    (NIL T T NIL NIL)
    (NIL T T T T)
    (NIL T NIL T T)
    (T NIL T T NIL)
    (T NIL NIL NIL T)
    (T NIL NIL NIL NIL)
    (T T T NIL T)
    (T T NIL NIL NIL)
    (T NIL NIL NIL T)
    (T NIL T T T)
    (NIL T T T T)
    (T NIL T NIL T)
    (T NIL T NIL T)
    (T T NIL T NIL)
    (T T NIL T NIL)
    (NIL T T T T)
    (NIL T NIL T T)
    (NIL NIL NIL T NIL)
    (NIL T T T T)
    (NIL T T T NIL)
    (NIL NIL T T NIL)
    (T T T T NIL)
    (NIL T T T T)
    (NIL T T NIL T)
    (NIL T T T T)
    (NIL T T T NIL)
    (NIL NIL T T NIL)
    (T T T T NIL)
    (NIL T NIL T NIL)
    (NIL T T T T)
    (NIL T T T NIL)
    (NIL NIL T T NIL)
    (T T T T NIL)
    (NIL T T T T)
    (NIL T NIL T T)
    (T T T NIL T)
    (T NIL NIL NIL NIL)
    (NIL T T T T)
    (NIL T NIL T T)
    (T NIL NIL NIL T)
    (T T NIL NIL NIL)
    (T NIL T T NIL)
    (T T NIL T NIL)
    (NIL T T T T)
    (NIL NIL NIL T NIL)
    (NIL T NIL T NIL)
    (NIL T T T T)
    (NIL T T NIL T)
    (NIL T T T T)
    (NIL T NIL T T)
    (T NIL T T T)
    (T T NIL T T)
    (T T NIL NIL NIL)
    (NIL NIL T T T)
    (NIL T T T T)
    (NIL T NIL T T)
    (T NIL NIL NIL NIL)
    (T T T NIL T)
    (NIL NIL T NIL NIL)
    (NIL NIL T T T)
    (NIL NIL T T NIL)
    (NIL T T T T)
    (NIL NIL NIL T NIL)
    (NIL T NIL T NIL)
    (NIL T T T T)
    (NIL T NIL T T)
    (T NIL T NIL T)
    (T NIL T NIL T)
    (T T NIL T NIL)
    (T T NIL T NIL)
    (NIL T T T T)
    (NIL T NIL T T)
    (NIL NIL T NIL NIL)
    (T NIL NIL NIL T)
    (NIL NIL T T T)
    (NIL NIL T T NIL)
    (NIL T T T T)
    (NIL NIL NIL T NIL)
    (NIL T NIL T NIL)
    (NIL T T T T)
    (NIL T T NIL T)
    (NIL T NIL T NIL)
    (NIL T NIL T NIL)
    (NIL T NIL T NIL)
    (NIL T NIL T NIL)))

; Let's not worry about failed proofs, so as per the lecture
; notes, we will not require ACL2s to prove function and body
; contracts and we don't want defunc and testing to take more 
; than 5 seconds.
;
; You may see some warnings here and there. Just ignore them. As
; long as the output is green, you are good to go.
(set-defunc-termination-strictp nil)
(set-defunc-function-contract-strictp nil)
(set-defunc-body-contracts-strictp nil)
(set-defunc-timeout 3)
(acl2s-defaults :set cgen-timeout 1)

#|
How are we going to decode the encrypted message?

Well, notice that each encrypted message consists of a list of lists
of Booleans, each of length 5. That is because each list of Booleans
corresponds to a character, as follows.  |#

; This is a data definition for a list of exactly 5 Booleans.
; The name bv is an abbreviation of BitVector.
(defdata bv (list boolean boolean boolean boolean boolean))

; This is a data definition for 32 characters.
(defdata char 
  (enum '(#\A #\B #\C #\D #\E #\F #\G #\H #\I #\J #\K #\L #\M #\N 
          #\O #\P #\Q #\R #\S #\T #\U #\V #\W #\X #\Y #\Z #\Space 
          #\: #\- #\' #\( #\)))) 

; We want a mapping (function) between char and bv. Since char is
; finite, we will use an alist. Here is the data definition
(defdata char-bv (alistof char bv))

; This is our mapping from chars to bvs. 
(defconst *bv-char-map*
  '((#\A . (nil nil nil nil nil))
    (#\B . (nil nil nil nil t))
    (#\C . (nil nil nil t nil))
    (#\D . (nil nil nil t t))
    (#\E . (nil nil t nil nil))
    (#\F . (nil nil t nil t))
    (#\G . (nil nil t t nil))
    (#\H . (nil nil t t t))
    (#\I . (nil t nil nil nil))
    (#\J . (nil t nil nil t))
    (#\K . (nil t nil t nil))
    (#\L . (nil t nil t t))
    (#\M . (nil t t nil nil))
    (#\N . (nil t t nil t))
    (#\O . (nil t t t nil))
    (#\P . (nil t t t t))
    (#\Q . (t nil nil nil nil))
    (#\R . (t nil nil nil t))
    (#\S . (t nil nil t nil))
    (#\T . (t nil nil t t))
    (#\U . (t nil t nil nil))
    (#\V . (t nil t nil t))
    (#\W . (t nil t t nil))
    (#\X . (t nil t t t))
    (#\Y . (t t nil nil nil))
    (#\Z . (t t nil nil t))
    (#\Space . (t t nil t nil))
    (#\: . (t t nil t t))
    (#\- . (t t t nil nil))
    (#\' . (t t t nil t))
    (#\( . (t t t t nil))
    (#\) . (t t t t t))))

; Let's check that *bv-char-map* is really a char-bvp
(check= (char-bvp *bv-char-map*) t)
 
; Define a function that given an element a and an alist l returns
; the cons that has a as its car or nil if no such cons exists.

(definec find-car (a :all l :alist) :list
  ...)

(check= (find-car #\W *bv-char-map*) '(#\W . (t nil t t nil)))

; Define a function that given an element a and an alist l returns
; the cons that has a as its cdr or nil if no such pair exists.

(definec find-cdr (a :all l :alist) :list
  ...)

(check= (find-cdr '(t nil t t nil) *bv-char-map*) '(#\W . (t nil t t nil)))

; Next we want to define functions that given a char return the
; corresponding bv and the other way around. Define these
; functions.
(definec char-bv (c :char) :bv
  ...)
  
(check= (char-bv #\W) '(t nil t t nil))

(definec bv-char (b :bv) :char
  ...)

(check= (bv-char '(t nil t t nil)) #\W)

; Next we have data definitions for a listof bvs and chars.
; This allows us to construct messages out of characters or out
; of bit vectors.

(defdata lobv (listof bv))
(defdata lochar (listof char))

; Here is a definition for a list of booleans.
(defdata lob (listof boolean))

; xor is a builtin function.
; Here is a function that xor's bit vectors.
; The contracts are a little more complicated than we usually
; write, but we really do want that lengths of the input bit
; vectors to be equal.
(defunc xor-bv (b1 b2)
  :input-contract (and (lobp b1) (lobp b2)
                       (equal (len b1) (len b2)))
  :output-contract (and (lobp (xor-bv b1 b2))
                        (equal (len (xor-bv b1 b2)) (len b1)))
  (if (endp b1)
    nil
    (cons (xor (first b1) (first b2))
          (xor-bv (rest b1) (rest b2)))))

; Next we have a test? for sanity checking that claims that if we
; apply xor-bv on bv's then we get bv's back. 
(test? 
  (implies (and (bvp b1) (bvp b2))
           (bvp (xor-bv b1 b2))))

; Ignore this
(in-theory (disable charp bvp xor-bv-definition-rule
                    bv-char-definition-rule
                    char-bv-definition-rule))

; Now let's define a function to encrypt a single character,
; given a bitvector.
(definec encrypt-char (c :char s :bv) :bv 
  ...)

(check= (encrypt-char #\B '(t nil t nil t)) '(t nil t nil nil))

; Ignore this
(in-theory (disable encrypt-char-definition-rule))

; Now, let's define a function to encrypt a message based on the
; lecture notes on one-time pads (the "power of xor")

(defunc encrypt (m s)
  :input-contract (and (locharp m) (lobvp s)
                       (equal (len m) (len s)))
  :output-contract (and (lobvp (encrypt m s))
                        (equal (len (encrypt m s)) (len m)))
  ...)

; Here is a function that makes a list containing n copies of e.
(definec copy (e :all n :nat) :tl
  (if (equal n 0)
    nil
    (cons e (copy e (- n 1)))))

; Here are our (really bad!) keys.
; They are really bad because they should be a random sequence
; of bit vectors!
(defconst *secret1* (copy '(t nil nil t t) (len *code1*)))
(defconst *secret2* (copy '(t nil t nil t) (len *code2*)))

; Here is how we write a function to decode a bv c using the
; secret s. 
(definec decrypt-bv (c :bv s :bv) :char
  (bv-char (xor-bv c s)))

; Write a function to decrypt a encrypted message c, using the
; secret s.
(defunc decrypt (c s)
  :input-contract (and (lobvp c) (lobvp s)
                       (equal (len c) (len s)))
  :output-contract (locharp (decrypt c s))
  ...)


; Write a test? to make sure encrypt and decrypt work 
; as expected
(test? (implies (and (locharp m) (lobvp s) 
                     (equal (len m) (len s)))
                ...))


; Now, let's see what those secret messages say.
; We're going to turn the list of characters into a string for
; better readability as follows.

(coerce (decrypt *code1* *secret1*) 'string)
; The above is an important message. Look up why.

(coerce (decrypt *code2* *secret2*) 'string)
; Read this. It provides useful information.