#|
The Imitation Game Lab.

This lab is about encryption. Not the kind Turing had to deal
with, but with the kind we saw in class.

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.