#|
Copyright (C) 1994 by Alex Bronstein and Carolyn Talcott.  All Rights
Reserved.
You may copy and distribute verbatim copies of this Nqthm-1992 event script as
you receive it, in any medium, including embedding it verbatim in derivative
works, provided that you conspicuously and appropriately publish on each copy
a valid copyright notice "Copyright (C) 1994 by Alex Bronstein and Carolyn
Talcott.  All Rights Reserved."
NO WARRANTY
Alex Bronstein and Carolyn Talcott PROVIDE ABSOLUTELY NO WARRANTY.  THE EVENT
SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR
IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO
THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT
PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR
CORRECTION.
IN NO EVENT WILL Alex Bronstein or Carolyn Talcott BE LIABLE TO YOU FOR ANY
DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR
CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT
(INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE
OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE
POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the library "mlp" using the compiled version.

; sadder.bm: a serial adder (adds the last 2 values of the input)
; This is Paillet example 4, which has a totally fuzzy, and almost
; meaningless SPECIFICATION (verification condition).  Instead, we
; provide our OWN specs, in many different tastes:
; - in terms of stringfuns: correct-1-S
; - in terms of Lastchars (more intuitive):
; - with a "Done" line
; - or predicting "good" times (len x = 0 modulo 2)
;
;;; CIRCUIT in SUGARED form:

#|
(setq sysd '(sy-SADDER (x)
(Y1 R 'a0 x) ; arbitrary initial value
(Y2 S plus Y1 x)
(Ydone R 1 Y4) ; specific initial value
(Y4 S bnot Ydone)
(Yout S bmux Ydone x Y2)
))
(setq sadder '(  |#
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_plus.bm: Plus combinational element.
; U7-DONE
;   no character function definition since BM already knows about Plus..
; Everything below generated by:     (bmcomb 'plus '() '(x y))

Definition: s-plus (x, y) = if empty (x) then e

else a (s-plus (p (x), p (y)), l (x) + l (y)) endif

;; A2-Begin-S-PLUS

Theorem: a2-empty-s-plus empty (s-plus (x, y)) = empty (x)

Theorem: a2-e-s-plus (s-plus (x, y) = e) = empty (x)

Theorem: a2-lp-s-plus len (s-plus (x, y)) = len (x)

Theorem: a2-lpe-s-plus eqlen (s-plus (x, y), x)

Theorem: a2-ic-s-plus (len (x) = len (y)) → (s-plus (i (c x, x), i (c y, y)) = i (c x + c y, s-plus (x, y)))

Theorem: a2-lc-s-plus (¬ empty (x)) → (l (s-plus (x, y)) = (l (x) + l (y)))

Theorem: a2-pc-s-plus p (s-plus (x, y)) = s-plus (p (x), p (y))

Theorem: a2-hc-s-plus ((¬ empty (x)) ∧ (len (x) = len (y))) → (h (s-plus (x, y)) = (h (x) + h (y)))

Theorem: a2-bc-s-plus (len (x) = len (y)) → (b (s-plus (x, y)) = s-plus (b (x), b (y)))

Theorem: a2-bnc-s-plus (len (x) = len (y)) → (bn (n, s-plus (x, y)) = s-plus (bn (n, x), bn (n, y)))

;; A2-End-S-PLUS
; eof:comb_plus.bm
; comb_bnot.bm: Binary Not combinational element
; U7-DONE

Definition: bnot (u) = if u = 0 then 1

else 0 endif

; Everything below generated by: (bmcomb 'bnot '() '(x))

Definition: s-bnot (x) = if empty (x) then e

else a (s-bnot (p (x)), bnot (l (x))) endif

;; A2-Begin-S-BNOT

Theorem: a2-empty-s-bnot empty (s-bnot (x)) = empty (x)

Theorem: a2-e-s-bnot (s-bnot (x) = e) = empty (x)

Theorem: a2-lp-s-bnot len (s-bnot (x)) = len (x)

Theorem: a2-lpe-s-bnot eqlen (s-bnot (x), x)

Theorem: a2-ic-s-bnot s-bnot (i (c x, x)) = i (bnot (c x), s-bnot (x))

Theorem: a2-lc-s-bnot (¬ empty (x)) → (l (s-bnot (x)) = bnot (l (x)))

Theorem: a2-pc-s-bnot p (s-bnot (x)) = s-bnot (p (x))

Theorem: a2-hc-s-bnot (¬ empty (x)) → (h (s-bnot (x)) = bnot (h (x)))

Theorem: a2-bc-s-bnot b (s-bnot (x)) = s-bnot (b (x))

Theorem: a2-bnc-s-bnot bn (n, s-bnot (x)) = s-bnot (bn (n, x))

;; A2-End-S-BNOT
; eof:comb_bnot.bm
; comb_mux.bm: Mux combinational element, i.e. "if", but with
; U7-DONE
;      control input binary-encoded (i.e. 0=F or 1=T) hardwired, no ref to bobi

Definition: bmux (u1 , u2 , u3 ) = if u1 = 1 then u2

else u3 endif

; everything below generated by: (bmcomb 'bmux '() '(x1 x2 x3))
; with the EXCEPTIONS/HAND-MODIFICATIONS given below.

Definition: s-bmux (x1 , x2 , x3 ) = if empty (x1 ) then e

else a (s-bmux (p (x1 ), p (x2 ), p (x3 )), bmux (l (x1 ), l (x2 ), l (x3 ))) endif

; SBMUX-is-SIF can make things much simpler on occasions:

Theorem: sbmux-is-sif s-bmux (x1 , x2 , x3 ) = s-if (s-equal (x1 , s-const (1, x1 )), x2 , x3 )

Event: Disable sbmux-is-sif.

; We take advantage of SBMUX-is-SIF for all inductive proofs. To do so we
; HAND-MODIFY the code generated by Sugar to replace all the hints by:
;   - A2-EMPTY, A2-PC replace hint with: ((enable sbmux-is-sif))
;   - A2-LP, A2-IC, A2-HC, A2-BC: ((enable sbmux-is-sif) (disable len))
;   - A2-BNC: ((enable sbmux-is-sif) (disable bn len))
;; A2-Begin-S-BMUX

Theorem: a2-empty-s-bmux empty (s-bmux (x1 , x2 , x3 )) = empty (x1 )

Theorem: a2-e-s-bmux (s-bmux (x1 , x2 , x3 ) = e) = empty (x1 )

Theorem: a2-lp-s-bmux len (s-bmux (x1 , x2 , x3 )) = len (x1 )

Theorem: a2-lpe-s-bmux eqlen (s-bmux (x1 , x2 , x3 ), x1 )

Theorem: a2-ic-s-bmux ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 ))) → (s-bmux (i (c x1 , x1 ), i (c x2 , x2 ), i (c x3 , x3 ))

= i (bmux (c x1 , c x2 , c x3 ), s-bmux (x1 , x2 , x3 )))

Theorem: a2-lc-s-bmux (¬ empty (x1 )) → (l (s-bmux (x1 , x2 , x3 )) = bmux (l (x1 ), l (x2 ), l (x3 )))

Theorem: a2-pc-s-bmux p (s-bmux (x1 , x2 , x3 )) = s-bmux (p (x1 ), p (x2 ), p (x3 ))

Theorem: a2-hc-s-bmux ((¬ empty (x1 )) ∧ ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 )))) → (h (s-bmux (x1 , x2 , x3 )) = bmux (h (x1 ), h (x2 ), h (x3 )))

;old: ((DISABLE BMUX S-BMUX) (ENABLE H LEN) (INDUCT (S-BMUX X1 X2 X3)))

Theorem: a2-bc-s-bmux ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 ))) → (b (s-bmux (x1 , x2 , x3 )) = s-bmux (b (x1 ), b (x2 ), b (x3 )))

;old: ((DISABLE BMUX) (ENABLE B LEN) (INDUCT (S-BMUX X1 X2 X3)))

Theorem: a2-bnc-s-bmux ((len (x1 ) = len (x2 )) ∧ (len (x2 ) = len (x3 ))) → (bn (n, s-bmux (x1 , x2 , x3 )) = s-bmux (bn (n, x1 ), bn (n, x2 ), bn (n, x3 )))

;old: ((DISABLE BMUX S-BMUX))
;; A2-End-S-BMUX
; eof:comb_bmux.bm

Definition: topor-sy-sadder (ln) = if ln = 'y1 then 0

elseif ln = 'y2 then 1 elseif ln = 'ydone then 0 elseif ln = 'y4 then 1 elseif ln = 'yout then 2 else 0 endif

Definition: sy-sadder (ln, x) = if ln = 'y1

then if empty (x) then e

else i ('a0, p (x)) endif elseif ln = 'y2 then s-plus (sy-sadder ('y1, x), x) elseif ln = 'ydone then if empty (x) then e

else i (1, sy-sadder ('y4, p (x))) endif elseif ln = 'y4 then s-bnot (sy-sadder ('ydone, x)) elseif ln = 'yout then s-bmux (sy-sadder ('ydone, x), x, sy-sadder ('y2, x)) else sfix (x) endif

;; A2-Begin-SY-SADDER

Theorem: a2-empty-sy-sadder empty (sy-sadder (ln, x)) = empty (x)

Theorem: a2-e-sy-sadder (sy-sadder (ln, x) = e) = empty (x)

Theorem: a2-lp-sy-sadder len (sy-sadder (ln, x)) = len (x)

Theorem: a2-lpe-sy-sadder eqlen (sy-sadder (ln, x), x)

Theorem: a2-pc-sy-sadder p (sy-sadder (ln, x)) = sy-sadder (ln, p (x))

;; A2-End-SY-SADDER
;;; Circuit CORRECTNESS /Paillet:
;; we can do the actual Deroulement, which is a very WEAK spec
;; indeed..

Theorem: sadder-paillet (len (x) = 2) → (l (sy-sadder ('yout, x)) = (l (p (x)) + l (x)))

;; or we can prove the natural spec:

Theorem: sadder-correct-1 (¬ empty (p (x))) → (l (sy-sadder ('yout, x))

= if l (sy-sadder ('ydone, x)) = 1 then l (x) else l (p (x)) + l (x) endif)

Theorem: sadder-but-wiser

 'horning-said-that
;; There are 2 lessons from the above lemma:
;; 1) if you're reading this in the thesis, congratulations
;;    for reading so far.
;; 2) if someone claims he proved some formula mechanically,
;;    make sure the formula means something...

;; we could look at it in terms of STRING-FUNS:

Definition: sadder-spec-s (x) = s-if (s-equal (sy-sadder ('ydone, x), s-const (1, sy-sadder ('ydone, x))),

x,

s-plus (p (x), x))

; one "trick" which makes this weird (non-MLP looking) spec work:

Theorem: s-plus-one-off (¬ empty (x)) → (s-plus (i (u, p (x)), x) = i (u + h (x), s-plus (p (x), x)))

; and the second "trick" is that the off-by-one sum, and the
; toggling contribute to working things out:

Theorem: sadder-correct-1-s-key s-if (s-equal (sy-sadder ('ydone, x), s-const (1, sy-sadder ('ydone, x))),

x,

i (u, s-plus (p (x), x))) = s-if (s-equal (sy-sadder ('ydone, x), s-const (1, sy-sadder ('ydone, x))),

x,

s-plus (p (x), x))

Theorem: sadder-correct-1-s sy-sadder ('yout, x) = sadder-spec-s (x)

;; Going back to looking in terms of Last-chars, we would most
;; likely only specify (more partially):

Theorem: sadder-correct-2 ((¬ empty (x)) ∧ (¬ empty (p (x))) ∧ (l (sy-sadder ('ydone, x)) = 0)) → (l (sy-sadder ('yout, x)) = (l (p (x)) + l (x)))

; Note: sadder-correct-2 is proved immediately from correct-1 or
; correct-1-S, or can be obtained from scratch with the same hints
; as correct-1.
; The fact that such a partial spec is BM-provable probably depends
; on the fact that it requires NO induction.  In cases with
; induction, too weak a spec would probably not go through.  In
; other words, we might have to specify a second property which
; also specifies what happens in the "previous" or "uninteresting"
; (Done not raised) cases.
; Another way to look at the spec is to PREDICT the timing of the
; output, as opposed to just looking at the Done (Ydone) line.
; This of course will not always be possible. The key to the
; prediction is:

Theorem: sadder-correct-3-ydone (¬ empty (x)) → (l (sy-sadder ('ydone, x))

= if (len (x) mod 2) = 0 then 0 else 1 endif)

; or with a bit more work we can prove the 2-tick rhythm:

Theorem: sadder-correct-3 ((¬ empty (x)) ∧ ((len (x) mod 2) = 0)) → (l (sy-sadder ('yout, x)) = (l (p (x)) + l (x)))

; Note: removing the hyp: (not (empty (P x))) is not harmful,
; but it just forces BM into a couple of cases and 1 elimination
; before it gets to the real meat.
; eof: sadder.bm
;))

Index

a, 2–4 a2-bc-s-bmux, 5 a2-bc-s-bnot, 4 a2-bc-s-plus, 3 a2-bnc-s-bmux, 6 a2-bnc-s-bnot, 4 a2-bnc-s-plus, 3 a2-e-s-bmux, 5 a2-e-s-bnot, 3 a2-e-s-plus, 2 a2-e-sy-sadder, 6 a2-empty-s-bmux, 5 a2-empty-s-bnot, 3 a2-empty-s-plus, 2 a2-empty-sy-sadder, 6 a2-hc-s-bmux, 5 a2-hc-s-bnot, 4 a2-hc-s-plus, 3 a2-ic-s-bmux, 5 a2-ic-s-bnot, 4 a2-ic-s-plus, 2 a2-lc-s-bmux, 5 a2-lc-s-bnot, 4 a2-lc-s-plus, 2 a2-lp-s-bmux, 5 a2-lp-s-bnot, 3 a2-lp-s-plus, 2 a2-lp-sy-sadder, 7 a2-lpe-s-bmux, 5 a2-lpe-s-bnot, 4 a2-lpe-s-plus, 2 a2-lpe-sy-sadder, 7 a2-pc-s-bmux, 5 a2-pc-s-bnot, 4 a2-pc-s-plus, 3 a2-pc-sy-sadder, 7

b, 3–5 bmux, 4, 5 bn, 3, 4, 6 bnot, 3, 4 e, 2–6 empty, 2–9 eqlen, 2, 4, 5, 7

h, 3–5, 8

i, 2, 4–6, 8

l, 2–5, 7–9 len, 2, 3, 5–7, 9

p, 2–9

s-bmux, 4–6 s-bnot, 3, 4, 6 s-const, 5, 7, 8 s-equal, 5, 7, 8 s-if, 5, 7, 8 s-plus, 2, 3, 6–8 s-plus-one-off, 8 sadder-but-wiser, 7 sadder-correct-1, 7 sadder-correct-1-s, 8 sadder-correct-1-s-key, 8 sadder-correct-2, 8 sadder-correct-3, 9 sadder-correct-3-ydone, 9 sadder-paillet, 7 sadder-spec-s, 7, 8 sbmux-is-sif, 5 sfix, 6 sy-sadder, 6–9

topor-sy-sadder, 6