/* 

     Alloy version of ACL2 binary adder example

          C. M. Sperberg-McQueen
          10 January 2010
          Minor revisions to prose 12 January 2010

*/

/* 

This Alloy model describes a binary adder; it accepts two
binary numbers and calculates their sum.

The model is based on the binary adder described in section 10.5.1
of Matt Kaufmann, Panagiotis Manolios, and J Strother Moore,
Computer-Aided Reasoning: An Approach ([Austin]: [n.p.], 2002).
They specify the adder in ACL2 and use ACL2 to prove that it does
in fact add numbers correctly.

This Alloy version of the same example is intended to help me
understand better the differences and similarities between Alloy
and ACL2; it has also helped me understand the example better.
The key insight gained here (and the main reason I am writing the
example up with such extensive comments) is that at least some
things naturally specified as recursion can, in Alloy, be
specified naturally as constraints on sequences.  

In the comments, I will describe both my Alloy solution to the
problem and the ACL2 example on which it's based.  (The ACL2 
form I give is the one I created when doing the exercise; in
some cases it diverges slightly from the form given by Kaufmann,
Manolios, and Moore.)

Note: the designers of Alloy make clear that Alloy is not intended
for arithmetic calculations, and it may be pushing things a bit to
try to use Alloy for a problem like this one.  Certainly, mapping
between Alloy's integers and the bit-sequence representation
defined here requires more elaborate machinery than one might
expect (see section 6 below), but it can be done.

*/

/*****************************************************************
 1 The task
******************************************************************/

/* The task is simple: define a binary adder and prove that it adds.
Since Alloy does no proofs, we'll content ourselves with asserting
that it adds and finding no counter-examples within a reasonable
scope. */

/*****************************************************************
 2 Binary data
******************************************************************/

/* First, we define our representation of binary data: bits are ones
and zeros, and numbers will be sequences of bits.  For
convenience, we interpret numbers low-order-bit first.  */

abstract sig Bit {}
one sig Zero, One extends Bit {}
sig Number {
  bits : seq Bit
}{
  #bits > 0
}

/* For comparison: the ACL2 example uses the ACL2 constants T and
NIL to represent bits, and defines the following functions to
operate upon it:

(defun band (x y) (if x (if y t nil) nil))
(defun bor  (x y) (if x t (if y t nil)))
(defun bxor (x y) (if x (if y nil t) (if y t nil)))
(defun bmaj (x y z) (bor (band x y) (bor (band y z) (band x z))))

We could define analogous functions here, or use the library
util/boolean.als, but in this version of the model we won't do so.
*/

/*****************************************************************
 3 A half-adder
******************************************************************/

/* A half-adder takes two bits as input and returns both a value bit
and a carry bit.  (The name appears to be formed to contrast this
form of adder with the 'full' adder needed for adding numbers more
than one bit wide.  Wikipedia has an informative article on
adders.)

It turns out to be convenient to represent the return value as a
sig of its own: a value-carry pair or VC. */

sig VC {
  value : one Bit,
  carry : one Bit
}

fun half_adder[p, q : Bit] : VC {
  { v : VC | 
    (p = Zero and q = Zero) =>
      (v.value = Zero and v.carry = Zero)
    else (p = Zero and q = One) =>
      (v.value = One and v.carry = Zero)
   else (p = One and q = Zero) =>
      (v.value = One and v.carry = Zero)
   else (p = One and q = One) =>
     (v.value = Zero and v.carry = One) 
 }
}

/* The ACL2 textbook does not define a half-adder, but one can
easily be specified, using the same idiom as is used for the
full-adder (for which see below):

(defun half-adder (p q)
  (mv 
   (bxor p q)   ; sum of two inputs is their xor
   (band p q))) ; carry of two inputs is their and

This is so much more compact that it moved me to try a similarly
compact version in Alloy: */

fun half_adder2[p, q : Bit] : VC {
  { v : VC | 
    v.value = ((p = q) => Zero else One)
    and v.carry = ((p = One and q = One) => One else Zero)
  }
}

/* This of course immediately leads to the challenge to show that
the two formulations are the same.  It's easy to confirm that they
are.  (The space here is small enough that even the default Alloy
scope will provide an exhaustive search.  So specifying a scope
of 10, as is done below, is serious overkill.) */

pred show {}
run show

assert half_adders_same {
  all p, q : Bit | all v1, v2 : VC |
    v1 = half_adder[p, q] and v2 = half_adder2[p, q]
    implies v1.value = v2.value and v1.carry = v2.carry 
}
check half_adders_same for 10


/*****************************************************************
  4 A full-adder
******************************************************************/

/* A full adder takes two input bits and a carry-in bit as input, 
and again returns a VC, i.e. a value bit and a carry-out bit. */

fun full_adder[p, q, Cin : Bit] : VC {
  { v : VC | 
    (p = Zero and q = Zero and Cin = Zero) =>
      (v.value = Zero and v.carry = Zero)
    else (p = Zero and q = Zero and Cin = One) =>
      (v.value = One and v.carry = Zero)
    else (p = Zero and q = One and Cin = Zero) =>
      (v.value = One and v.carry = Zero)
    else (p = Zero and q = One and Cin = One) =>
      (v.value = Zero and v.carry = One)
    else (p = One and q = Zero and Cin = Zero) =>
      (v.value = One and v.carry = Zero)
    else (p = One and q = Zero and Cin = One) =>
      (v.value = Zero and v.carry = One)
    else (p = One and q = One and Cin = Zero) =>
      (v.value = Zero and v.carry = One)
    else (p = One and q = One and Cin = One) =>
      (v.value = One and v.carry = One)
 }
} 

/* The Alloy definition is, again, more compact:

(defun full-adder (p q cin)
  (mv 
   (bxor p (bxor q cin)) ; sum 
   (bmaj p q cin)))

We might define full_adder more compactly using xor, etc., but it
seems simpler and clearer just to lay out all the cases.  We
aren't trying to save transistors, here.  */


/*****************************************************************
 5 A serial adder (for multiple bits)
******************************************************************/

/* A serial adder sums two binary numbers of arbitrary length.
Before we define it, however, we have some preliminary work to
take care of.

It simplifies the definitions if we specify an addition-like
operation which produces not a sequence of bits but a sequence of
value-bit + carry-bit pairs (VCs).

The VC sequence will be as long as the longer of a and b, so we
will need a max function. */

fun max[a, b : Int] : Int {
  (a > b) => a else b
}

/* Now we define the relation between two numbers and the
corresponding sequence of VCs.  

(Alloy note: it's instructive to try to define this as a function
instead of a predicate.  I did not find a way to do so: I used a
set-comprehension in the body, of the form { svc : seq VC | ... },
but of course Alloy does not have sets of sets, so it cannot have
sets of sequences, either.  if there is another way, I have not
found it yet.  So it's defined here as a predicate of three
arguments.)  */

pred vc_sum[a, b : Number, svc : seq VC]  {
  // svc is the vc_sum of a and b iff:

  // 1 it is as long as the longer of a and b
  #svc = max[#bits[a], #bits[b]]

  // 2 its first member is the half-add sum of the zero bits
  // of a and b.  (It could also be the full-add sum, with
  // a zero carry-in, obviously.)
  svc[0] = half_adder[a.bits[0], b.bits[0]]

  // 3 every other member of svc is the full-add sum
  // of the corresponding bits in a and b, with a 
  // carry-in bit from the previous member of svc.
  // There are three cases:
  all n : Int | (
    // Case 1:  a and b both have bits at this position
    (n > 0 and n < #a.bits and n < #b.bits) =>
      svc[n] = full_adder[a.bits[n], b.bits[n], svc[n-1].carry]

    // Case 2:  a has bits, but b does not.  Use Zero.
    else (n > 0 and n < #a.bits and n >= #b.bits) =>
      svc[n] = full_adder[a.bits[n], Zero, svc[n-1].carry]

    // Case 3:  b has bit and a has none.  
    else (n > 0 and n >= #a.bits and n < #b.bits) =>
      svc[n] = full_adder[Zero, b.bits[n], svc[n-1].carry])
}

/* A predicate for sanity-checking the definition of vc_sum */
pred show_vc_sum {
  some a, b : Number | some svc : seq VC | 
    vc_sum[a, b, svc]
}
run show_vc_sum 

/* It also simplifies things if we specify in a separate predicate
just how sequences of VCs relate to numbers: the bit sequence of
the number is the same as the value fields of the VCs, taken in
order, plus if necessary an additional high-order bit for the
final carry. */

pred vcseq_num[svc : seq VC, n : Number] {
  // the length is correct, and if the last VC has a carry,
  // then the last (high-order) bit of the number is One.
  (svc.last.carry = Zero) => 
    #n.bits = #svc
  else (
    #n.bits = #svc + 1
    and n.bits.last = One
  )

  // All the other bits are the value bits of the VC sequence
  all i : n.bits.inds | n.bits[i] = svc[i].value
}

/* With those preliminaries out of the way, we can specify the
serial adder by saying c is the serial addition of a and b iff
there is some sequence of VCs svc such that svc is the vc_sum of a
and b, and c is the Number equivalent of svc. */

pred serial_add[a, b, c : Number] {
  some svc : seq VC |
    vc_sum[a, b, svc]
    and 
    vcseq_num[svc, c]
}

/* Some visualization and testing predicates.  These helped
clarify what went wrong in earlier versions of the specification,
when expressions like #a and #b were used by mistake instead of
the correct #a.bits and #b.bits. */

pred show_serial_add {
  some a, b, c : Number | serial_add[a,b,c]
}
run show_serial_add for 4 
pred test_serial_add {
  some a, b, c : Number |
    number_value[a,0]
    and number_value[b,2]
    and serial_add[a,b,c]
}
run test_serial_add

/* The ACL2 version of the serial adder is:

(defun serial-adder (p q c)
  (declare (xargs :measure (+ (len p) (len q))))
  (if (and (endp p) (endp q))
      (list c)
    (mv-let (sum cout)
	    (full-adder (car p) (car q) c)
	    (cons sum 
		  (serial-adder (cdr p) (cdr q) cout)))))

The recursive call passes the carry-out (cout) result from the
full-adder to the next digit; it is the logical equivalent of the
reference to svc[n-1].carry in the definition of vc_sum above. Or,
put the other way around: a naive attempt to render this recursive
function into Alloy fails, because Alloy does not allow recursive
functions.  To create an Alloy expression of the idea, the modeler
must find some other formulation.  Often transitive closure or the
sum operator can be used, or (as here) sequences.  There is a 1:1
correspondence between the sequence of VCs svc in serial_add and
the recursive invocations of serial-adder in the ACL2
formulation. */

/*****************************************************************
 6 Evaluating a binary Number as an Alloy Int
******************************************************************/

/* So far, so good.  Can we test whether the serial_add predicate
adds correctly?  To do so, it would be handy to be able to map
from a Number to the corresponding Alloy integer.  More than
handy, really: to assert the correctness of the serial_add
predicate is to claim that it gives the same results as some
accepted arithmetic.  Here, that means Alloy's arithmetic.

We do so by first specifying a sequence of powers of two
represented by the number n, then summing them.

There may be a simpler way to do this, but we'll use a
construction similar in spirit to the VC sequence used above.

To represent the numeric value of a particular digit, we define a
DigitValue signature, which indicates the bit number, the
potential value (i.e. the value represented by a one in the
position represented), and the actual value in a particular
number.  The 'exponent' field is redundant but helpful in checking
that instances of the model take the form expected for them. */

sig DigitValue {
  exponent : Int,
  potential : Int,
  actual : Int
}

/* Digit values are useful to us only if we have a sequence of
them with suitable values for exponent and potential value.  So we
define a PowerSeq signature which imposes those constraints. */

sig PowerSeq {
  powers : seq DigitValue 
}{
  // In a powerseq, item n has exponent n.
  all n : powers.inds | powers[n].exponent = n

  // And each item n has potential = 2**n.
  // So the potential of the first digit is 1,
  powers[0].potential = 1

  // And the potential of all others is twice the potential of
  // their predecessor
  all n : powers.inds |
    (n > 0) =>
      int[powers[n].potential] = int[powers[n-1].potential] 
                               + int[powers[n-1].potential]

  all n : powers.inds |
    powers[n].actual = 0 or powers[n].actual = powers[n].potential
}
pred show_ps {
  some p : PowerSeq | #(p.powers) > 1
}
run show_ps for 4

/* To any given Number (sequence of bits) there corresponds a
PowerSeq (sequence of integers which are powers of two).  The
number_powerseq predicate defines the correspondence: when the
number has a One in a given position, the power sequence has its
full potential value there; if the number has a Zero, the power
sequence has 0 as its actual value.*/

pred number_powerseq [ n : Number, s : PowerSeq ] {
  #(n.bits) = #(s.powers)
  all i : n.bits.inds |
    ( (n.bits)[i] = One) => 
      s.powers[i].actual = s.powers[i].potential
    else
      s.powers[i].actual = 0
}

/* With the aid of power sequences we can specify the predicate
number_value, which holds between (the bit sequence of) a binary
Number and an integer value. */

pred number_value [ n : Number, v : Int ] {
  some p : PowerSeq | 
    number_powerseq[n, p] 
    and v = ( sum univ.(p.powers.actual) )
}
pred show_num_val {
  some n : Number | some v : Int | number_value[n,v]
    and #(n.bits) > 1
    and v = 5
}
run show_num_val for 3
run show_num_val for 3 but 6 int

/* The ACL2 equivalent is given by a 'naturalize' function, which
takes a sequences of bits and turns it into a natural number.

(defun naturalize (x)
  (cond
   ((endp x) 0)
   ((car x) (+ 1 (* 2 (naturalize (cdr x)))))
   (t (* 2 (naturalize (cdr x))))))

*/


/*****************************************************************
 7 Correctness
******************************************************************/

/* And now we can specify the correctness property for the 
serial_add predicate. */

assert serial_adder_correct {
  all a, b, c : Number |
    all i, j, k : Int |
      ( (number_value[a,i]
        and number_value[b,j]
        and number_value[c,k]
        and serial_add[a, b, c])
      implies
        (int[k] = int[i] + int[j]) )
}


/* The ACL2 form of the property is more compact, in part because
all along the ACL2 formulation has used functions where the Alloy
form has used predicates.

(defthm serial-adder-correct
  (equal (naturalize (serial-adder p q c))
	 (+ (naturalize p)
	    (naturalize q)
	    (if c 1 0))))
*/

/* Actually checking the property turns out to have some cost in
both systems. */

/* In Alloy, the cost of checking the serial_adder_correct
predicate goes up sharply as the scope increases:
On my machine, the default scope of 3 takes 9.7 seconds to check,
a scope of 4 takes 45.2 seconds, and a scope of 5 takes 312 seconds.
A scope of 5 with bitwidth 8 ran for an hour or so before I stopped it.
 */
check serial_adder_correct
check serial_adder_correct for 4
check serial_adder_correct for 5
check serial_adder_correct for 5 but 8 int

/* So we want to specify the scope carefully.  To add two n-bit 
numbers, we need 3 Number atoms, 3 PowerSeq atoms, and 2n
DigitalValue atoms (a Zero and a One in each of n positions).
The addition itself requires a sequence of n VCs, but they need
not be distinct; we can never need more than four VCs, since
VCs are essentially two-bit numbers.  And of course, 'int' needs
to be set to n. */
/* n = 3: CNF in 2.2 sec, solve in 51.8 sec */
check serial_adder_correct for 3 but 4 VC, 3 int, 6 DigitValue
/* n = 4: CNF in 2.7 sec, solve in 1183.4 sec  */
check serial_adder_correct for 3 but 4 VC, 4 int, 8 DigitValue
/* n = 5: CNF in 2.8 sec, solve in ... sec */
check serial_adder_correct for 3 but 4 VC, 5 int, 10 DigitValue
/* n = 6 */
check serial_adder_correct for 3 but 4 VC, 6 int, 12 DigitValue

/* In ACL2, the cost of checking takes a different form.  The
proof of correctness goes nowhere until the user guides the system
by asking it first to prove the following two lemmas, which
(roughly) say that if serial-adder is called with a second
argument of zero and a carry of zero or one, the result is the
first argumet, or the first argument plus one.

(defthm aux-serial-adder-nil-nil
  (equal (naturalize (serial-adder x nil nil))
	 (naturalize x)))
(defthm aux-serial-adder-nil-t
  (equal (naturalize (serial-adder x nil t))
	 (+ 1 (naturalize x))))

Once those are proved, ACL2 proves the main theorem without
assistance. */

/* Can conclusions be drawn?  Maybe.  

In many cases, Alloy is easier to use than ACL2 for verifying
assertions, because the Alloy Analyzer proceeds without human
intervention while ACL2's theorem prover often requires human
intervention.  But in cases where the modeler's first formulation
of a concept involves recursion, an Alloy formulation of the
concept may require more effort than an ACL2 formulation.  In this
case, of course, the recursive formulation feels more 'natural' at
least in part because I encountered it first; if I had done the
Alloy version first, perhaps the use of recursion in the ACL2
version would have felt awkward and unmotivated.  But it would be
rash to assume no problems will ever feel as if their natural
solution is recursive.

At the moment, I'm uncertain which of two possible lessons
to be drawn here is more important: 

  (1) The absence of recursion in Alloy can make some things
      just plain awkward. The designers of Alloy make a point of
      suggesting that Alloy is not necessarily the right tool for
      all jobs ("if you have a heavily numerical problem ... Alloy
      is probably not suitable anyway" -- I'm not sure whether
      this problem counts as heavily numerical or not.)

  (2) Despite the absence of recursion and its non-numerical
      leanings, Alloy does provide a language powerful enough to
      describe the concepts needed here.  In particular, the use
      of sequences to eliminate the need for recursive definitions
      is a technique worth mastering.

Perhaps both are important, perhaps at different times; it will be
the task of the modeler to decide which lesson is applicable at
which times.

*/