Cryptography

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

Purpose of exercise

Activities

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

ACL2 intrinsics and other functions useful in this exercise

Useful books of theorems