Cryptography

Write a program that encodes messages by summing adjacent pairs of characters and decodes messages encoded in this way.

Purpose of exercise

• Practice writing equation-based programs
• Practice specifying correctness properties
• Use DrACuLa DoubleCheck for predicate-based, random testing
• Certify correctness properties using ACL2
• Practice using ACL2 file i/o

Activities

• Define the functions and predicates required below (here are some predefined functions that you might find helpful)
• Package the functions marked "service" in a book and certify it
• Package the other functions and predicates in another book (the "test book")
• DoubleCheck the properties stated below using the test book
• Convert the DoubleCheck predicates to ACL2 theorems, package them in another book (the "verification book"), and certify it
• Add the required i/o operations to the program

Terminology

Visible character: a character whose ASCII character code is a number in range 32 to 126, inclusive
Plaintext message: a list of visible characters
Viscode: the viscode of a visible character is its ASCII character code minus 32
Plainvis message: the list of viscodes for the characters in a plaintext message
Codevis message: the encoding of a plainvis message by the method described in the linear encoding project
Codetext message: the list of visible characters represented by the viscodes in a codevis message

Requirements

1. visiblize-txt: converts a list of characters into a new list that is identical except that non-visible characters are changed to spaces
2. txt->vis: converts a list of visible characters to the corresponding a list of viscodes
3. vis->txt: converts a list of viscodes into the corresponding list of visible characters
4. plainvis->codevis: converts a plainvis message to the corresponding codevis message
5. codevis->plainvis: converts a codevis message to the corresponding plainvis message

Properties

1. visiblize-txt delivers a list of visible chararacters
2. txt->vis delivers a list of viscodes
3. The viscode of the n-th character in cs is the n-th element of (txt->vis cs)
4. vis->txt delivers a list of viscodes
5. The character corresponding to the n-th viscode in vs is the n-th element of (vis->txt vs)
6. (codevis->plainvis (plainvis->codevis plainvis-msg)) reproduces plainvis-vsg

File I/O

• Write a command that, given a path to an input file, creates a new file with the same path, but with "-enc" added as a suffix to the filename, that contains the codetext message represented by the sequence of characters in the input file, interspersed with newline characters every 80 characters.
• Write a command that, given a path to an input file containing codetext message with added newline characters, creates a new file with the same path, but with "-dec" added as a suffix to the filename, that contains the plaintext message represented by the characters in the input file with newlines inserted at least every 80 characters, but never inserted between a less-than sign and the next character that is neither a greater-than sign nor a whitespace character.

ACL2 intrinsics and other functions useful in this exercise

• Nth
• chrs->str   -- in list-utilities teachpack
• str->chrs   -- in list-utilities teahcpack
• file->str   -- in io-utilities teachpack
• string-list->file   -- in io-utilities teachpack

Useful books of theorems

• arithmetic-3/top
• ariithmetic-3/floor-mod/floor-mod