Correctness by Construction – a Carry-Ripple Adder

I dedided to to try out Ivor’s new pattern matching gadgetry by implementing a program I’ve been wanting to write for ages. This is a carry-ripple adder for binary numbers, where the representation of binary numbers is indexed over its meaning (i.e. the natural number it represents). Doing this has the advantage that any program written over the binary numbers must satisfy the appropriate invariant properties; a carry-ripple adder really must implement addition corresponding to addition of the natural numbers.

For reference, natural number addition is implemented as follows:

Data Nat : * = O : Nat | S : (k:Nat)Nat;

Patt plus : Nat -> Nat -> Nat =
    plus O y = k
  | plus (S k) y = S (plus k y)

A bit on its own represents either one or zero:

Data Bit : Nat -> * = On : Bit (S O) | Off : Bit O;

A number is then a sequence of binary digits where the meaning is computed in the type. Note that the bit constructor extends an n-bit representation of the number v by one bit, b, giving a new number representing 2^n*b+v:

Data Number : (len:Nat)(val:Nat)*
  = none : Number O O
  | bit : (bv:Nat)(b:Bit bv)->
          (len:Nat)(val:Nat)(num:Number len val)->
	  (Number (S len) (plus (mult (power (S (S O)) len) bv) val));

Indexing the binary representation this way means that we can give a precise specification to the add with carry function which guarantees that any well-typed function really does implement addition corresponding to addition of naturals:

Data NumCarry : (len:Nat)(val:Nat)*
  = numcarry : (cv:Nat)(carry:Bit cv)->
               (len:Nat)(val:Nat)(n:Number len val)->
               (NumCarry len (plus (mult (power (S (S O)) len) cv) val));

addNumber : (len:Nat)(cv:Nat)(carry:Bit cv)->
                          (lv:Nat)(l:Number len lv)->
                          (rv:Nat)(r:Number len rv)->
			  (NumCarry len (plus (plus lv rv) cv))

Actually getting a function which works is somewhat involved, since at each stage you need to convince the typechecker that what you’re doing is sound. The full script is available here. I think the proof script (which is doing no more than high school algebra) looks more scary than it needs to though. It’d be interesting to find a way for the machine to give more help with these.