Lecture 10: Itemizations

1 Purpose

Show OneOf, Constant, talk about filtering.

2 Outline

Not all properties can be expressed as dependent signatures

While expressing invariants directly in the signatures is usually preferable, when possible, sometimes it’s difficult to do so. For example, consider a function that reverses a list. There are certainly some properties we could assert about the output: for example, that it has the same length. Let’s do that:

(define-contract Any (lambda (x) #t))

(define-contract (SameLength l1) (lambda (l2) (= (length l2) (length l1))))

(: my-rev (Function (arguments [l (List Any)]) (result (AllOf (List Any) (SameLength l)))))

(define (my-rev l) (reverse l))

But there are functions that clearly are not reverse that satisfy that – for example, a function that just returns a list of all 0s, but the right number to have the lengths match! Of course, we could also check that all the elements are there, but then a function that just returned the same list would pass. And to make the contract check that the list is reversed is somewhat circular: as if we could write that correctly, we could write the function correctly, and wouldn’t need the contract!

Instead, what we might realize is that if my-rev is correct, then given two lists, l1 and l2, (my-rev (append l1 l2)) is the same as (append (my-rev l2) (my-rev l1)). This requires we trust append (or check it some other way), but otherwise it is a clear and concise invariant on the behavior of my-rev, but it is about multiple calls, so it has to be written is a separate property, which is fine.

Error correction

Now, let’s look at another example. Let’s consider an important problem: how to recover data that is corrupted. This is incredibly important for radio transmission, as wireless signals are prone to interference, but there are many other applications.

This is always done by introducing some amount of redundancy in the data. A simple way to do this, known as a repetition code, involves repeating the data multiple times.

Let’s say we have a sequence of bits, represented as:

; A Bit is one of:

;  - 0

;  - 1

; A Packet is a Bit

; A Message is a [List-of Packet]

How do we express those as contracts? LSL has built-in support for creating contracts for single constant values, and also for itemizations of a number of possible different contracts. We can combine those two features together to define what a Bit is, and then use what we already know to define Packet and Message.

(define-contract Bit (OneOf (Constant 0) (Constant 1)))

(define-contract Packet Bit)

(define-contract Message (List Packet))

We want to be able to correct some amount of errors. In particular, by considering the individual Packets that make up a Message, our goal will be to be able to introduce up to a single error (randomly) into each packet. If we did this without changing the data, there would be no way of recovering, as a single change would change the entire packet. But, we will first encode the packets into a larger packet (of size 3), then introduce the error, and then decode. Our goal is to be able to recover the original message regardless of how (or if) the errors are introduced.

In order to do that, we need a notion of a "list of length exactly three". If you remember, the built-in Tuple exists to support this.

(define-contract TripletPacket (Tuple Bit Bit Bit))

(define-contract TripletMessage (List TripletPacket))

Now we can formally specify all that we just described in English:

(: encode (-> Message TripletMessage))

(: decode (-> TripletMessage Message))

(: message-recovery-prop (-> Message True))

(define (message-recovery-prop msg)   (local [(define (mutate c b) (if c (if (= b 0) 1 0) b))           (define (introduce-error triplet)             (local [(define idx (random 4))]               (list (mutate (= idx 0) (list-ref triplet 0))                     (mutate (= idx 1) (list-ref triplet 1))                     (mutate (= idx 2) (list-ref triplet 2)))))]   (equal? (decode (map introduce-error (encode msg))) msg)))

Note that at this point, we’ve described the data (that we’ll allow three bits), and how we want encoding / decoding to be able to handle errors (up to one bit mutation without any loss of information), but we haven’t said anything about the implementation.

In this case, the implementation is pretty straightforward: we simply duplicate the bit, and to decode, take the majority. We can then check that the property holds with a few examples.

(define (encode msg)   (map (lambda (p) (list p p p)) msg))

(define (decode msg)     (map (lambda (t) (if (> (foldr + 0 t) 1) 1 0)) msg))

At this point, we can use check-contract to validate that out encoding / decoding do, indeed, work. Like reverse, this is an example where we could not express this correctness property in the signature of either function, because it is the interaction of the two that we wish to behave in a certain way. But once we have expressed that (as message-recovery-prop), we can use check-contract to ensure that it works.

(check-contract message-recovery-prop 1)

1 success(es) 0 failure(s) 0 error(s) 1 test(s) run