Linear Encoding

Encoding integer sequences by summing adjacent pairs, modulo a given base ... and decoding them

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

Activities

• Define the functions required below (here are some predefined functions that you might find helpful)
• Package the functions in a book and certify it
• Define the predicates required below and package them in another book (the "predicate book")
• Express the properties stated below in DoubleCheck form, package them in another book (the "test book"), and run the tests
• Convert the properties from Double-Check form to ACL2 theorems, package them in another book (the "verification book"), and certify it

Terminology

• encoding base: an integer that is two or greater
• encodable integer: a nonnegative integer that is smaller than the encoding base
• true-list: nil or (cons x xs), where xs is a true-list
  (Note: if xs is a true-list, then xs must be nil if it is an atom, and  (cdr xs) must be a true-list if xs isn't an atom)

Requirements

1. Define a function, encode, that, given an encoding base m and a non-empty sequence x₀, x₁, ... x_n-1 of encodable integers, delivers the sequence of encodable integers y₀, y₁, ... y_n-1, with y_i = (x_i + x_i+1) mod m, where x_n = m-1
2. Define a function, decode, that inverts encode: (decode m (encode m xs)) = xs
3. Define a predicate, basep, such that (basep m) is true if and only if m is an encoding base
4. Define a predicate, encodable-integerp, such that (encodable-integerp m x) is true if and only if x is an encodable integer
5. Define a predicate, encodable-listp, such that (encodable-listp m xs) is true if and only if m is an encoding base and xs is a true-list, all of whose elements are encodable integers

Properties

1. If m is an encoding base and xs is a true-list of encodable integers, then (encode m xs) is a true-list of encodable integers
2. If m is an encoding base and ys is a true-list of encodable integers, then (decode m ys) is a true-list of encodable integers
3. If m is an encoding base and xs is a true-list of encodable integers, then (a) the last element of (encode m xs) is the difference, mod m, of the last element of xs and 1, and (b) the i-th element of (encode m xs) is the sum, mod m, of the i-th and i-plus-first element of xs
4. If m is an encoding base and xs is a true-list of encodable integers, then (decode (encode xs)) = xs

ACL2 intrinsics useful in this exercise

• mod
• natp
• Nth

Useful books of theorems

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