#|
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.

; srccpu.bm is the BIG ONE!
;
; Notes:
; . As in pplfadd, some A2-PCs trigger a BM bug and blow up
;   (here A2-PC-SY-I) so we declare it as axiom (point that out in
;   Personal Confessions section in thesis).
; . Constants:  Initial PC (pci) has to be declared and axiomatized
;   as a numberp, because we do defined arithmetic (add1) on it.
;   Others: initial program and initial register file are quoted
;   constants, because only undefined (dcl) functions act on them.
; . We code "NoAd" (inexistant address) as F, because it makes life

;   easier by avoiding needless equalities around.  As a general
;   principle (at least in BM), boolean flags should be coded as
;   booleans in the model!  It also means that "small k" and
;   "big k" in Saxe's picture are now the same thing:
;   (k ctl leftinput) = (if ctl F leftinput).

;;; (Sugared) Circuits:
#|
(setq sy-S '(sy-S (x)
(Ypc R (pci) Ypcn)
(Ypcn S mux Ybc Ybt Ypcp1)
(Ypcp1 S inc Ypc)
(Ybc S eql0 Ywd)
(Ypr R 'pro Ypr)
(Ybt S Umb Ypc Ypr)
(Ywa S Umw Ypc Ypr)
(Yra S Umr Ypc Ypr)
(Yf S Umf Ypc Ypr)
(Ywd S Ualu Yf Yrd)
(Yrd S Ulk Yra Yrf)
(Yrf R 'rfi Yrfn)
(Yrfn S Upd Ywa Ywd Yrf)
))
; pipeline elements are indicated by visual offset (and digits):
; Initial values (originally inspired by Lamport):
;
; The branch target (bt) don't matter, they get 0
; The branch control (bc) DO matter, they must start w/ False: F
; The write address (wa) also matter, they must start w/ "NoAd": F
(setq sy-I '(sy-I (x)
(Ypc R (pci) Ypcn)
(Ypcn S mux Ybc0 Ybt0 Ypcp1)
  (Ybt0 R 0 Ybt1)
  (Ybt1 R 0 Ybt2)
  (Ybt2 R 0 Ybt3)
  (Ybt3 R 0 Ybt4)
  (Ybc0 R F Ybc1k)
  (Ybc1k S k Ybc0 Ybc1)
  (Ybc1 R F Ybc2k)

(Ybc2k S k Ybc0 Ybc2)
(Ybc2 R F Ybc3k)
(Ybc3k S k Ybc0 Ybc3)
(Ybc3 R F Ybc4k)
(Ybc4k S k Ybc0 Ybc4)
(Ypcp1 S inc Ypc)
(Ybc4 S eql0 Ywd4)
(Ypr R 'pro Ypr)
(Ybt4 S Umb Ypc Ypr)
(Ywa4 S Umw Ypc Ypr)
(Yra S Umr Ypc Ypr)
(Yf S Umf Ypc Ypr)
(Ywd4 S Ualu Yf Yrd3)
(Yrd3 S mux Yrb3 Ywd3 Yrd2)
(Yrd2 S mux Yrb2 Ywd2 Yrd1)
(Yrd1 S mux Yrb1 Ywd1 Yrd)
(Yrb3 S equal Yra Ywa3)
(Yrb2 S equal Yra Ywa2)
(Yrb1 S equal Yra Ywa1)
(Ywa3 R F Ywa4k)
(Ywa2 R F Ywa3k)
(Ywa1 R F Ywa2k)
(Ywa4k S k Ybc0 Ywa4)
(Ywa3k S k Ybc0 Ywa3)
(Ywa2k S k Ybc0 Ywa2)
(Ywa1k S k Ybc0 Ywa1)
(Yrd S Ulk Yra Yrf)
(Yrf R 'rfi Yrfn)
(Yrfn S Upd Ywa1k Ywd1 Yrf)
(Ywd1 R 0 Ywd2)
(Ywd2 R 0 Ywd3)
(Ywd3 R 0 Ywd4)
))
(setq srccpu '( |#
; Constants are hand-declared and axiomatized:

Event: Introduce the function symbol pci of 0 arguments.

Axiom: pci-numberp pci ∈ N

; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_mux.bm: Mux combinational element, i.e. "if".
; U7-DONE

Definition: mux (u1 , u2 , u3 ) = if u1 then u2

else u3 endif

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

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

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

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

Theorem: smux-is-sif s-mux (x1 , x2 , x3 ) = s-if (x1 , x2 , x3 )

Event: Disable smux-is-sif.

; We take advantage of SMUX-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 smux-is-sif))
;   - A2-LP, A2-IC, A2-HC, A2-BC: ((enable smux-is-sif) (disable len))
;   - A2-BNC: ((enable smux-is-sif) (disable bn len))
;; A2-Begin-S-MUX

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

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

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

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

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

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

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

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

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

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

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

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

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

;old: ((DISABLE MUX S-MUX))
;; A2-End-S-MUX
; eof:comb_mux.bm
; comb_inc.bm: INCrement combinational element
; U7-DONE

Definition: inc (u) = (1 + u)

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

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

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

;; A2-Begin-S-INC

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-INC
; eof:comb_inc.bm
; Comb_eql0.bm: equal to 0 test, without zerop (in contrast to eq0).
; U7-DONE

Definition: eql0 (u) = (u = 0)

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

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

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

;; A2-Begin-S-EQL0

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-EQL0
; eof:comb_eq0.bm
; comb_umb.bm: Umb combinational element (= fun2)
; U7-DONE
; arbitrary Char-Fun of arity 2:

Event: Introduce the function symbol umb of 2 arguments.

; Everything below generated by: (bmcomb 'Umb '() '(x y))

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

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

;; A2-Begin-S-UMB

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-UMB
; eof:comb_umb.bm
; comb_umw.bm: Umw combinational element (= fun2)
; U7-DONE
; arbitrary Char-Fun of arity 2:

Event: Introduce the function symbol umw of 2 arguments.

; Everything below generated by: (bmcomb 'Umw '() '(x y))

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

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

;; A2-Begin-S-UMW

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-UMW
; eof:comb_umw.bm
; comb_umr.bm: Umr combinational element (= fun2)
; U7-DONE
; arbitrary Char-Fun of arity 2:

Event: Introduce the function symbol umr of 2 arguments.

; Everything below generated by: (bmcomb 'Umr '() '(x y))

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

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

;; A2-Begin-S-UMR

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-UMR
; eof:comb_umr.bm
; comb_umf.bm: Umf combinational element (= fun2)
; U7-DONE
; arbitrary Char-Fun of arity 2:

Event: Introduce the function symbol umf of 2 arguments.

; Everything below generated by: (bmcomb 'Umf '() '(x y))

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

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

;; A2-Begin-S-UMF

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-UMF
; eof:comb_umf.bm
; comb_ualu.bm: Ualu combinational element
; U7-DONE
; arbitrary Char-Fun of arity 2:

Event: Introduce the function symbol ualu of 2 arguments.

; Everything below generated by: (bmcomb 'Ualu '() '(x y))

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

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

;; A2-Begin-S-UALU

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-UALU
; eof:comb_ualu.bm
; comb_ulk.bm: Ulk combinational element
; U7-DONE
; arbitrary Char-Fun of arity 2:

Event: Introduce the function symbol ulk of 2 arguments.

; Everything below generated by: (bmcomb 'Ulk '() '(x y))

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

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

;; A2-Begin-S-ULK

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-ULK
; eof:comb_ulk.bm
; comb_upd.bm: Upd combinational element
; U7-DONE
; arbitrary Char-Fun of arity 3:

Event: Introduce the function symbol upd of 3 arguments.

; AXIOM characterising Upd:  (or at least some): see _s .
; Everything below generated by: (bmcomb 'Upd '() '(x1 x2 x3))

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

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

;; A2-Begin-S-UPD

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

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-UPD
; eof:comb_upd.bm

Definition: topor-sy-s (ln) = if ln = 'ypc then 0

elseif ln = 'ypcn then 5 elseif ln = 'ypcp1 then 1 elseif ln = 'ybc then 4 elseif ln = 'ypr then 0 elseif ln = 'ybt then 1 elseif ln = 'ywa then 1 elseif ln = 'yra then 1 elseif ln = 'yf then 1 elseif ln = 'ywd then 3 elseif ln = 'yrd then 2 elseif ln = 'yrf then 0 elseif ln = 'yrfn then 4 else 0 endif

Definition: sy-s (ln, x) = if ln = 'ypc

then if empty (x) then e

else i (pci, sy-s ('ypcn, p (x))) endif elseif ln = 'ypcn then s-mux (sy-s ('ybc, x), sy-s ('ybt, x), sy-s ('ypcp1, x)) elseif ln = 'ypcp1 then s-inc (sy-s ('ypc, x)) elseif ln = 'ybc then s-eql0 (sy-s ('ywd, x)) elseif ln = 'ypr then if empty (x) then e

else i ('pro, sy-s ('ypr, p (x))) endif elseif ln = 'ybt then s-umb (sy-s ('ypc, x), sy-s ('ypr, x)) elseif ln = 'ywa then s-umw (sy-s ('ypc, x), sy-s ('ypr, x)) elseif ln = 'yra then s-umr (sy-s ('ypc, x), sy-s ('ypr, x)) elseif ln = 'yf then s-umf (sy-s ('ypc, x), sy-s ('ypr, x)) elseif ln = 'ywd then s-ualu (sy-s ('yf, x), sy-s ('yrd, x)) elseif ln = 'yrd then s-ulk (sy-s ('yra, x), sy-s ('yrf, x)) elseif ln = 'yrf then if empty (x) then e

else i ('rfi, sy-s ('yrfn, p (x))) endif elseif ln = 'yrfn then s-upd (sy-s ('ywa, x), sy-s ('ywd, x), sy-s ('yrf, x)) else sfix (x) endif

;; A2-Begin-SY-S

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

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

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

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

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

;; A2-End-SY-S
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
; comb_k.bm: K combinational element. Semantics by Saxe in rn395 Notes 3.
; Our "k" is his "k" (i.e. little k).
; U7-DONE

Definition: k (u, v) = if u then f

else v endif

; Everything below generated by: (bmcomb 'K '() '(x y))

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

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

;; A2-Begin-S-K

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-K
; eof:comb_k.bm

Definition: topor-sy-i (ln) = if ln = 'ypc then 0

elseif ln = 'ypcn then 2 elseif ln = 'ybt0 then 0 elseif ln = 'ybt1 then 0 elseif ln = 'ybt2 then 0 elseif ln = 'ybt3 then 0 elseif ln = 'ybc0 then 0 elseif ln = 'ybc1k then 1 elseif ln = 'ybc1 then 0 elseif ln = 'ybc2k then 1 elseif ln = 'ybc2 then 0 elseif ln = 'ybc3k then 1 elseif ln = 'ybc3 then 0 elseif ln = 'ybc4k then 8 elseif ln = 'ypcp1 then 1 elseif ln = 'ybc4 then 7 elseif ln = 'ypr then 0 elseif ln = 'ybt4 then 1 elseif ln = 'ywa4 then 1 elseif ln = 'yra then 1 elseif ln = 'yf then 1 elseif ln = 'ywd4 then 6 elseif ln = 'yrd3 then 5 elseif ln = 'yrd2 then 4 elseif ln = 'yrd1 then 3 elseif ln = 'yrb3 then 2 elseif ln = 'yrb2 then 2 elseif ln = 'yrb1 then 2 elseif ln = 'ywa3 then 0 elseif ln = 'ywa2 then 0 elseif ln = 'ywa1 then 0 elseif ln = 'ywa4k then 2 elseif ln = 'ywa3k then 1 elseif ln = 'ywa2k then 1 elseif ln = 'ywa1k then 1 elseif ln = 'yrd then 2 elseif ln = 'yrf then 0 elseif ln = 'yrfn then 2 elseif ln = 'ywd1 then 0 elseif ln = 'ywd2 then 0 elseif ln = 'ywd3 then 0 else 0 endif

Definition: sy-i (ln, x) = if ln = 'ypc

then if empty (x) then e

else i (pci, sy-i ('ypcn, p (x))) endif elseif ln = 'ypcn then s-mux (sy-i ('ybc0, x), sy-i ('ybt0, x), sy-i ('ypcp1, x)) elseif ln = 'ybt0 then if empty (x) then e

else i (0, sy-i ('ybt1, p (x))) endif elseif ln = 'ybt1 then if empty (x) then e

else i (0, sy-i ('ybt2, p (x))) endif elseif ln = 'ybt2 then if empty (x) then e

else i (0, sy-i ('ybt3, p (x))) endif elseif ln = 'ybt3 then if empty (x) then e

else i (0, sy-i ('ybt4, p (x))) endif elseif ln = 'ybc0 then if empty (x) then e

else i (f, sy-i ('ybc1k, p (x))) endif elseif ln = 'ybc1k then s-k (sy-i ('ybc0, x), sy-i ('ybc1, x)) elseif ln = 'ybc1 then if empty (x) then e

else i (f, sy-i ('ybc2k, p (x))) endif elseif ln = 'ybc2k then s-k (sy-i ('ybc0, x), sy-i ('ybc2, x)) elseif ln = 'ybc2 then if empty (x) then e

else i (f, sy-i ('ybc3k, p (x))) endif elseif ln = 'ybc3k then s-k (sy-i ('ybc0, x), sy-i ('ybc3, x)) elseif ln = 'ybc3 then if empty (x) then e

else i (f, sy-i ('ybc4k, p (x))) endif elseif ln = 'ybc4k then s-k (sy-i ('ybc0, x), sy-i ('ybc4, x)) elseif ln = 'ypcp1 then s-inc (sy-i ('ypc, x)) elseif ln = 'ybc4 then s-eql0 (sy-i ('ywd4, x)) elseif ln = 'ypr then if empty (x) then e

else i ('pro, sy-i ('ypr, p (x))) endif elseif ln = 'ybt4 then s-umb (sy-i ('ypc, x), sy-i ('ypr, x)) elseif ln = 'ywa4 then s-umw (sy-i ('ypc, x), sy-i ('ypr, x)) elseif ln = 'yra then s-umr (sy-i ('ypc, x), sy-i ('ypr, x)) elseif ln = 'yf then s-umf (sy-i ('ypc, x), sy-i ('ypr, x)) elseif ln = 'ywd4 then s-ualu (sy-i ('yf, x), sy-i ('yrd3, x)) elseif ln = 'yrd3 then s-mux (sy-i ('yrb3, x), sy-i ('ywd3, x), sy-i ('yrd2, x)) elseif ln = 'yrd2 then s-mux (sy-i ('yrb2, x), sy-i ('ywd2, x), sy-i ('yrd1, x)) elseif ln = 'yrd1 then s-mux (sy-i ('yrb1, x), sy-i ('ywd1, x), sy-i ('yrd, x)) elseif ln = 'yrb3 then s-equal (sy-i ('yra, x), sy-i ('ywa3, x)) elseif ln = 'yrb2 then s-equal (sy-i ('yra, x), sy-i ('ywa2, x)) elseif ln = 'yrb1 then s-equal (sy-i ('yra, x), sy-i ('ywa1, x)) elseif ln = 'ywa3 then if empty (x) then e

else i (f, sy-i ('ywa4k, p (x))) endif elseif ln = 'ywa2 then if empty (x) then e

else i (f, sy-i ('ywa3k, p (x))) endif elseif ln = 'ywa1 then if empty (x) then e

else i (f, sy-i ('ywa2k, p (x))) endif elseif ln = 'ywa4k then s-k (sy-i ('ybc0, x), sy-i ('ywa4, x)) elseif ln = 'ywa3k then s-k (sy-i ('ybc0, x), sy-i ('ywa3, x)) elseif ln = 'ywa2k then s-k (sy-i ('ybc0, x), sy-i ('ywa2, x)) elseif ln = 'ywa1k then s-k (sy-i ('ybc0, x), sy-i ('ywa1, x)) elseif ln = 'yrd then s-ulk (sy-i ('yra, x), sy-i ('yrf, x)) elseif ln = 'yrf then if empty (x) then e

else i ('rfi, sy-i ('yrfn, p (x))) endif elseif ln = 'yrfn then s-upd (sy-i ('ywa1k, x), sy-i ('ywd1, x), sy-i ('yrf, x)) elseif ln = 'ywd1 then if empty (x) then e

else i (0, sy-i ('ywd2, p (x))) endif elseif ln = 'ywd2 then if empty (x) then e

else i (0, sy-i ('ywd3, p (x))) endif elseif ln = 'ywd3 then if empty (x) then e

else i (0, sy-i ('ywd4, p (x))) endif else sfix (x) endif

;; A2-Begin-SY-I

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

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

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

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

; blows up, as usual.
;(PROVE-LEMMA A2-PC-SY-I (REWRITE)

;    (EQUAL (P (SY-I LN X)) (SY-I LN (P X)))
;    ((DISABLE S-INC S-EQL0 S-UMB S-UMW S-UMR S-UMF S-UALU S-MUX S-EQUAL
;              S-K S-ULK S-UPD A2-IC-S-INC A2-IC-S-EQL0 A2-IC-S-UMB
;              A2-IC-S-UMW A2-IC-S-UMR A2-IC-S-UMF A2-IC-S-UALU
;              A2-IC-S-MUX A2-IC-S-EQUAL A2-IC-S-K A2-IC-S-ULK
;              A2-IC-S-UPD)))

Axiom: a2-pc-sy-i p (sy-i (ln, x)) = sy-i (ln, p (x))

;; A2-End-SY-I

; CORRECTNESS PROOF:
;;; Get STUTTER theory:
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  TH_STUTTER.BM
;;;
;;; This file contains Stutter theory for BM.  It is supposed to be
;;; loaded directly when needed (i.e. not general enough to be
;;; stored in Lib/mlp).
;;;
;;; Our current double P-recursive def. of Stutter:
;;; Originally, it came from THETA-PRF-79 (done while babysitting
;;; for Caroline...) followed by MUCH experimentation and fiddling.

Definition: stut-r (x, y) = if empty (y) then x

elseif empty (p (y)) then b (x) elseif l (p (y)) then stut-r (x, p (y)) else b (stut-r (x, p (y))) endif

Definition: stut (x, y) = if empty (y) then e

elseif empty (p (y)) then a (e, h (x))

elseif l (p (y)) then a (stut (p (x), p (y)), l (stut (p (x), p (y))))

else a (stut (p (x), p (y)), h (stut-r (x, p (y)))) endif

; Stut-Induct inducts like stut, but without the case disjunction
; on LPx which is useless when we stutter on a line rather than an
; input. The resulting induction is not very different from a
; straight P induction, but it takes care of the empty Px case
; separately, and without bringing an elimination.

Definition: stut-induct (x) = if empty (x) then 0

elseif empty (p (x)) then 1 else stut-induct (p (x)) endif

;; Properties of Stut:

Theorem: stut-empty empty (stut (x, y)) = empty (y)

Theorem: stut-e (stut (x, y) = e) = empty (y)

Theorem: stut-p p (stut (x, y)) = stut (p (x), p (y))

;; Properties of Stut-R:
; Stut-R-E maybe shouldn't be enabled all the time, but when we're
; doing P inductions on Stut-R, this gives the base case.  The
; induction step is given by Stut-R-P.  Note that we don't have a
; full empty x hyp because Stut-R returns x and not sfix x in case
; y is empty...  Maybe we want to fix that at some point.

Theorem: stut-r-e stut-r (e, y) = e

Theorem: stut-r-p p (stut-r (x, y)) = stut-r (p (x), y)

Theorem: stut-r-len len (x) < (1 + (len (y) + len (stut-r (x, y))))

Theorem: stut-r-not-empty (len (y) < len (x)) → (¬ empty (stut-r (x, y)))

; Stut-Rem removes the trailing Ts of y, but ignores Ly (like R)
; and leaves one T: this weird def, so it works like Stut-R needs!

Definition: stut-rem (y) = if empty (y) then e

elseif empty (p (y)) then y

elseif l (p (y)) then stut-rem (p (y))

else y endif

Theorem: stut-rem-empty empty (stut-rem (x)) = empty (x)

Theorem: stut-rem-len len (stut-rem (x)) < (1 + len (x))

Theorem: stut-rem-len2 ((¬ empty (p (x))) ∧ l (p (x))) → (len (stut-rem (x)) < len (x))

; Stut-Num counts the number of F in y, ignoring Ly, and starts
; w/ 1, like Stut.

Definition: stut-num (y) = if empty (y) then 0

elseif empty (p (y)) then 1

elseif l (p (y)) then stut-num (p (y))

else 1 + stut-num (p (y)) endif

Theorem: stut-num-lessp stut-num (x) < (1 + len (x))

Theorem: stut-num-eq-0 (stut-num (x) = 0) = empty (x)

; Requires a small induction.

Theorem: stut-num-rem-len (¬ empty (x)) → (stut-num (p (stut-rem (x))) < len (x))

; From Stut-Num and Bn we get a CLOSED FORM for Stut-R !!!

Theorem: stut-r-closed stut-r (x, y) = bn (stut-num (y), x)

; Stut-inv is the key invariant property during Stuttering:

Theorem: stut-inv ((¬ empty (y)) ∧ (len (x) ≮ len (y))) → (l (stut (x, y)) = h (stut-r (x, p (stut-rem (y)))))

; but we only want to use it during the non-stuttering induction
; step, and not in general so:

Theorem: stut-inv0 ((¬ empty (y)) ∧ (len (x) ≮ len (y)) ∧ (¬ l (y))) → (l (stut (x, y)) = h (stut-r (x, p (stut-rem (y)))))

Event: Disable stut-inv.

; Now we relate Stut-R for Py and P Rem Py, to get the key to the
; induction step on main Stut inductions, in the non-stuttering
; case.
;
; It's a BAD rewrite (i.e. expanding, potentially self-applicable),
; and so are the preliminary lemmas needed to build to it.  This
; is not just an unfortunate construction.  It's inherent, because
; we're essentially giving an alternate definition via a Stut-Rem
; recursion.  And definitions are expanding, self-applicable,
; rewrites.  We get around the problem by lucking out: the
; hypotheses are sufficient to prevent successful self-applic.

Theorem: stut-r-indstep-num ((¬ empty (x)) ∧ l (x)) → (stut-num (x) = (1 + stut-num (p (stut-rem (x)))))

Event: Disable stut-r-indstep-num.

; OLD induction step prereq: not needed anymore.
;
;(prove-lemma Stut-R-indstep-Num-Rem (rewrite)
;(implies (and (not (empty y))
;       (not (empty (P y)))
;       (not (L (P y)))
;       )
;  (equal (Stut-Num (P (Stut-Rem (P y))))

; (sub1 (Stut-Num (P (Stut-Rem y))))
; ))
;((enable Stut-R-indstep-Num))
;)
;(disable Stut-R-indstep-Num-Rem)
; OLD induction step: not needed anymore.
;
;(prove-lemma Stut-indstep (rewrite)
;(implies (and (not (empty y))
;       (not (empty (P y)))
;       (not (L (P y)))
;       )
;  (equal (Stut-R x (P y))
; (B (Stut-R x (P (Stut-Rem (P y)))))
; ))
;((enable Stut-R-indstep-Num-Rem B-Bn-sub1)
; (disable Bn)
; )
;)
;(disable Stut-indstep) ; potentially self-looping...
;                       ; so we enable explicitely.

; NEW & GENERALIZED induction step hack , note: needs just ONE
; prereq! We're getting cleaner...

Theorem: stut-r-indstep ((¬ empty (y)) ∧ (¬ l (y))) → (stut-r (x, y) = b (stut-r (x, p (stut-rem (y)))))

Event: Disable stut-r-indstep.

; all the internal stuff shouldn't be needed outside:

Event: Disable stut-r.

Event: Disable stut-num.

Event: Disable stut-rem.

; Note: by leaving Stut, Stut-inv0, Stut-R-closed enabled, we get
;   the effect of an alternate recursive definition of Stut in the
;   most convenient form.  The remaining uncleanliness is that
;   Stut-R-indstep and Stut-R-closed match the same stuff, and need
;   to be used at different places in the main proof.  So far, we
;   survive by extreme cunning: they are in the right order, and
;   the hypothesis on Stut-R-indstep prevents wrong occurences.
;   This is neither clear nor robust...
;; eof: th_stutter.bm

;;; ALL DOWN TO HERE IN SRCDEF.{LIB,LISP}
;;; The circuit is mostly undefined.  Here are the axioms which
;;; give it its meaning:
; Umb-numberp: all branch targets are numbers; necessary since we
; do Add1 and Sub1 on them, and want that to work out.

Axiom: umb-numberp umb (x, y) ∈ N

; NoAd axiomatization:
; Supplying NoAddress (here: F) as the address to Wsel (here: Upd)
; leaves the RFile unchanged.  NoAd is never issued by the memory
; either as a Write or as a Read:

Axiom: upd-noad upd (f, x, y) = y

Axiom: umw-noad umw (x, y) ≠ f

Axiom: umr-noad umr (x, y) ≠ f

; axiom to characterize Update and Lookup (with any non-F address
; valid):
; Note that if we don't use the hypothesis restricting the address,
; we get an inconsistency in the theory!

Axiom: ulk-upd (ad1 ≠ f) → (ulk (ad1 , upd (ad2 , dat, rf ))

= if ad1 = ad2 then dat else ulk (ad1 , rf ) endif)

;;; Miscellaneous facts, simplifications, etc... about the
;;; circuits:
; Corr-S-PR expresses that the program (Ypr) is constant in S:

Theorem: corr-s-pr (¬ empty (x)) → (l (sy-s ('ypr, x)) = 'pro)

; Corr-I-PR expresses that the program (Ypr) is constant in I:

Theorem: corr-i-pr (¬ empty (x)) → (l (sy-i ('ypr, x)) = 'pro)

;;; Stuttering Correctness:
; StutCorr-rf-T expresses correctness WHEN stuttering, and only
; Upd-NoAd is needed in order to prove it.

Theorem: stutcorr-rf-t ((¬ empty (x)) ∧ (¬ empty (p (x))) ∧ (¬ l (sy-i ('ywa1k, p (x))))) → (l (sy-i ('yrf, x)) = l (sy-i ('yrf, p (x))))

Event: Disable stutcorr-rf-t.

; self-expanding, enable when needed

;; for PC in sy-I though, there is a fundamental difference. It
;; does NOT stutter sy-S PC, instead, there is a "virtual PC" in
;; sy-I which is a true stuttering of sy-S YPC, and which is
;; derivable from sy-I's global view, and with which sy-I RF is
;; in sync:
; comb_sub1.bm: SUB1 combinational element
; U7-DONE

; no charfun def, already defined in BM.
; Everything below generated by: (bmcomb 'sub1 '() '(x))

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

else a (s-sub1 (p (x)), l (x) − 1) endif

;; A2-Begin-S-SUB1

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

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

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

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

Theorem: a2-ic-s-sub1 s-sub1 (i (c x, x)) = i (c x − 1, s-sub1 (x))

Theorem: a2-lc-s-sub1 (¬ empty (x)) → (l (s-sub1 (x)) = (l (x) − 1))

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

Theorem: a2-hc-s-sub1 (¬ empty (x)) → (h (s-sub1 (x)) = (h (x) − 1))

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

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

;; A2-End-S-SUB1
; eof:comb_sub1.bm
 ; needed for def of ivPC

Definition: ivpc (x) = s-if (sy-i ('ybc0, x),

sy-i ('ybt0, x),

s-if (s-not (sy-i ('ywa3, x)), sy-i ('ypc, x), s-if (s-not (sy-i ('ywa2, x)), s-sub1 (sy-i ('ypc, x)), s-if (s-not (sy-i ('ywa1, x)),

s-sub1 (s-sub1 (sy-i ('ypc, x))),

s-sub1 (s-sub1 (s-sub1 (sy-i ('ypc, x))))))))

Event: Disable ivpc.

; we'll enable when needed

; sy-I-PC-numberp is a type lemma about I-PC and the branch targets
; needed for future add1-sub1 manipulation.

Theorem: sy-i-pc-numberp (¬ empty (x)) → ((l (sy-i ('ypc, x)) ∈ N)

∧ (l (sy-i ('ybt0, x)) ∈ N) ∧ (l (sy-i ('ybt1, x)) ∈ N) ∧ (l (sy-i ('ybt2, x)) ∈ N) ∧ (l (sy-i ('ybt3, x)) ∈ N) ∧ (l (sy-i ('ybt4, x)) ∈ N))

; Useful abbreviations about the semantics of the circuit:

Definition: res (pc, rf ) = ualu (umf (pc, 'pro), ulk (umr (pc, 'pro), rf ))

Event: Disable res.

; n-pc is "Next PC"

Definition: n-pc (pc, rf ) = mux (eql0 (res (pc, rf )), umb (pc, 'pro), 1 + pc)

Event: Disable n-pc.

; n-rf is "Next RF"

Definition: n-rf (pc, rf ) = upd (umw (pc, 'pro), res (pc, rf ), rf )

Event: Disable n-rf.

; Now we prove that they are "correct", with respect to our intent.
; Even though we don't use the next 3 lemmas anywhere else, they
; are a useful check - and during the development, help raise my
; confidence level! Moreover, they would be useful if we ever
; wanted to prove properties of the specification circuit (sy-S).

Theorem: corr-n-pc ((¬ empty (x)) ∧ (¬ empty (p (x)))) → (l (sy-s ('ypc, x)) = n-pc (l (sy-s ('ypc, p (x))), l (sy-s ('yrf, p (x)))))

Event: Disable corr-n-pc.

Theorem: corr-n-rf ((¬ empty (x)) ∧ (¬ empty (p (x)))) → (l (sy-s ('yrf, x)) = n-rf (l (sy-s ('ypc, p (x))), l (sy-s ('yrf, p (x)))))

Event: Disable corr-n-rf.

; Corr-S-PR-H and Corr-I-PR-H could be earlier, with the rest of
; the constant treatment for PR, but here is where they were
; needed & proved.

Theorem: corr-s-pr-h (¬ empty (x)) → (h (sy-s ('ypr, x)) = 'pro)

Theorem: corr-i-pr-h (¬ empty (x)) → (h (sy-i ('ypr, x)) = 'pro)

; REVERSAL PROPERTies for sy-S:
;  The SAME EXPAND hint as for Corr-n-pc and Corr-n-rf work.
; sy-S-reversal-pr is FUNDAMENTALLY DIFFERENT because we don't want
; to keep PR as part of the global state, so we deduce an equality
; by induction:

Theorem: sy-s-reversal-pr (¬ empty (bn (n, sy-s ('ypr, x)))) → (h (bn (n, sy-s ('ypr, x))) = 'pro)

; we need a few simple props of ivPC for the main induction,
; because we have to run with ivPC disabled there:

Theorem: ivpc-e empty (x) → (ivpc (x) = e)

Event: Disable ivpc-e.

; enable as needed

Theorem: ivpc-1 ((¬ empty (x)) ∧ empty (p (x))) → (l (ivpc (x)) = pci)

Event: Disable ivpc-1.

; enable as needed

; Junction (hack) lemma between the 2 hyps to get the reversals:

Theorem: sy-s-reversal-hyp-hack (¬ empty (bn (n, sy-s ('ypc, x)))) → (¬ empty (bn (n, sy-s ('ypr, x))))

Event: Disable sy-s-reversal-hyp-hack.

Theorem: sy-s-reversal-pc ((¬ empty (bn (n, sy-s ('ypc, p (x))))) ∧ (¬ empty (bn (n, sy-s ('yrf, p (x)))))) → (h (b (bn (n, sy-s ('ypc, x))))

= n-pc (h (bn (n, sy-s ('ypc, p (x)))), h (bn (n, sy-s ('yrf, p (x))))))

Theorem: sy-s-reversal-rf ((¬ empty (bn (n, sy-s ('ypc, p (x))))) ∧ (¬ empty (bn (n, sy-s ('yrf, p (x)))))) → (h (b (bn (n, sy-s ('yrf, x))))

= n-rf (h (bn (n, sy-s ('ypc, p (x)))), h (bn (n, sy-s ('yrf, p (x))))))

;; Now we develop the FUNDAMENTAL INVARIANT for sy-I :
; Level is the only one which needs RES enabled, and it's also
; a bit different from the others, because it's never "reset".

; sy-I-Yra-noad tells BM Yra is always an OK address, in a usable
; way.

Theorem: sy-i-yra-noad (¬ empty (x)) → (ulk (l (sy-i ('yra, x)), upd (ad, dat, rf ))

= if l (sy-i ('yra, x)) = ad then dat else ulk (l (sy-i ('yra, x)), rf ) endif)

; We prove the equalities for YRD lines separately, to minimize
; the mess!

Theorem: sy-i-yrd1 (¬ empty (x)) → (l (sy-i ('yrd1, x))

= ulk (l (sy-i ('yra, x)),

upd (l (sy-i ('ywa1, x)), l (sy-i ('ywd1, x)), l (sy-i ('yrf, x)))))

Theorem: sy-i-yrd2 (¬ empty (x)) → (l (sy-i ('yrd2, x))

= ulk (l (sy-i ('yra, x)),

upd (l (sy-i ('ywa2, x)), l (sy-i ('ywd2, x)), upd (l (sy-i ('ywa1, x)), l (sy-i ('ywd1, x)), l (sy-i ('yrf, x))))))

Theorem: sy-i-yrd3 (¬ empty (x)) → (l (sy-i ('yrd3, x))

= ulk (l (sy-i ('yra, x)),

upd (l (sy-i ('ywa3, x)), l (sy-i ('ywd3, x)), upd (l (sy-i ('ywa2, x)), l (sy-i ('ywd2, x)), upd (l (sy-i ('ywa1, x)), l (sy-i ('ywd1, x)), l (sy-i ('yrf, x)))))))

; now we do the invariants, per level:

Theorem: sy-i-inv-4 (¬ empty (x)) → ((l (sy-i ('ybc4, x)) = eql0 (l (sy-i ('ywd4, x))))

∧ (l (sy-i ('ybt4, x)) = umb (l (sy-i ('ypc, x)), 'pro)) ∧ (l (sy-i ('ywa4, x)) = umw (l (sy-i ('ypc, x)), 'pro)) ∧ (l (sy-i ('ywd4, x))

= res (l (sy-i ('ypc, x)),

upd (l (sy-i ('ywa3, x)), l (sy-i ('ywd3, x)), upd (l (sy-i ('ywa2, x)), l (sy-i ('ywd2, x)), upd (l (sy-i ('ywa1, x)), l (sy-i ('ywd1, x)), l (sy-i ('yrf, x)))))))

∧ (l (sy-i ('yrd3, x))

= ulk (l (sy-i ('yra, x)),

upd (l (sy-i ('ywa3, x)), l (sy-i ('ywd3, x)), upd (l (sy-i ('ywa2, x)), l (sy-i ('ywd2, x)), upd (l (sy-i ('ywa1, x)), l (sy-i ('ywd1, x)), l (sy-i ('yrf, x))))))))

Event: Disable sy-i-yrd1.

Event: Disable sy-i-yrd2.

Event: Disable sy-i-yrd3.

; Note that we repeat sy-I-Yrdn for each n, and this may be costly
; later. On the other hand, it's nice to have one property which
; expresses the "complete" correctness of a stage.

Theorem: sy-i-inv-3 (¬ empty (x)) → if ¬ l (sy-i ('ywa3, x))

then (¬ l (sy-i ('ybc3, x))) ∧ (¬ l (sy-i ('ywa2, x))) else (l (sy-i ('ybc3, x)) = eql0 (l (sy-i ('ywd3, x))))

∧ (l (sy-i ('ybt3, x))

= umb (l (sy-i ('ypc, x)) − 1, 'pro)) ∧ (l (sy-i ('ywa3, x))

= umw (l (sy-i ('ypc, x)) − 1, 'pro)) ∧ (l (sy-i ('ywd3, x))

= res (l (sy-i ('ypc, x)) − 1,

upd (l (sy-i ('ywa2, x)), l (sy-i ('ywd2, x)), upd (l (sy-i ('ywa1, x)), l (sy-i ('ywd1, x)), l (sy-i ('yrf, x))))))

∧ (l (sy-i ('yrd2, x))

= ulk (l (sy-i ('yra, x)),

upd (l (sy-i ('ywa2, x)), l (sy-i ('ywd2, x)), upd (l (sy-i ('ywa1, x)), l (sy-i ('ywd1, x)), l (sy-i ('yrf, x)))))) endif

Theorem: sy-i-inv-2 (¬ empty (x)) → if ¬ l (sy-i ('ywa2, x))

then (¬ l (sy-i ('ybc2, x))) ∧ (¬ l (sy-i ('ywa1, x))) else (l (sy-i ('ybc2, x)) = eql0 (l (sy-i ('ywd2, x))))

∧ (l (sy-i ('ybt2, x))

= umb ((l (sy-i ('ypc, x)) − 1) − 1, 'pro)) ∧ (l (sy-i ('ywa2, x))

= umw ((l (sy-i ('ypc, x)) − 1) − 1, 'pro)) ∧ (l (sy-i ('ywd2, x))

= res ((l (sy-i ('ypc, x)) − 1) − 1, upd (l (sy-i ('ywa1, x)), l (sy-i ('ywd1, x)), l (sy-i ('yrf, x)))))

∧ (l (sy-i ('yrd1, x))

= ulk (l (sy-i ('yra, x)),

upd (l (sy-i ('ywa1, x)), l (sy-i ('ywd1, x)), l (sy-i ('yrf, x))))) endif

Theorem: sy-i-inv-1 (¬ empty (x)) → if ¬ l (sy-i ('ywa1, x)) then ¬ l (sy-i ('ybc1, x))

else (l (sy-i ('ybc1, x)) = eql0 (l (sy-i ('ywd1, x))))

∧ (l (sy-i ('ybt1, x))

= umb (((l (sy-i ('ypc, x)) − 1) − 1) − 1, 'pro)) ∧ (l (sy-i ('ywa1, x))

= umw (((l (sy-i ('ypc, x)) − 1) − 1) − 1, 'pro)) ∧ (l (sy-i ('ywd1, x))

= res (((l (sy-i ('ypc, x)) − 1) − 1) − 1,

l (sy-i ('yrf, x))))

∧ (l (sy-i ('yrd, x)) = ulk (l (sy-i ('yra, x)), l (sy-i ('yrf, x)))) endif

; NOTES:
; .  Having the invariants written as above entail the cost of
; carrying lots of irrelevant information in each proof, and
; potentially crushing BM.  So instead we'll phrase each needed
; property later as a good rewrite, and prove it by instantiating
; the right invariant(s).
; .  What we did is a hand-induction on the DEPTH of the pipeline.
; Notice that NO explicit induction was necessary, simply proving
; the thms in the right order (4-3-2-1)..

; StutCorr-pc-T expresses correctness of ivPC WHEN stuttering.
; We rewrite just the portions of the invariants we need for
; StutCorr-pc-T so that BM will get that proof in finite time...

Theorem: sc-pc-t-1 (¬ l (sy-i ('ywa1, x))) → (¬ l (sy-i ('ybc1, x)))

Event: Disable sc-pc-t-1.

Theorem: sc-pc-t-2 (¬ l (sy-i ('ywa2, x))) → (¬ l (sy-i ('ybc2, x)))

Event: Disable sc-pc-t-2.

Theorem: sc-pc-t-3 (¬ l (sy-i ('ywa3, x))) → (¬ l (sy-i ('ybc3, x)))

Event: Disable sc-pc-t-3.

Theorem: stutcorr-pc-t ((¬ empty (x)) ∧ (¬ empty (p (x))) ∧ (¬ l (sy-i ('ywa1k, p (x))))) → (l (ivpc (x)) = l (ivpc (p (x))))

Event: Disable stutcorr-pc-t.

; self-expanding, enable when needed

; Now we express the "on the right also" invariants in a useful
; manner...

Theorem: sc-pc-f-3 (¬ l (sy-i ('ywa3, x))) → (¬ l (sy-i ('ywa2, x)))

Event: Disable sc-pc-f-3.

Theorem: sc-pc-f-2 (¬ l (sy-i ('ywa2, x))) → (¬ l (sy-i ('ywa1, x)))

Event: Disable sc-pc-f-2.

; In order to get the arithmetic to work out, we have to prove that
; we never subtract from zero...

Theorem: sc-pcn0-0 ((¬ empty (x)) ∧ (¬ l (sy-i ('ywa2, x))) ∧ l (sy-i ('ywa3, x))) → (l (sy-i ('ypc, x)) ≠ 0)

Theorem: sc-pcn0-1 ((¬ empty (x)) ∧ (¬ l (sy-i ('ywa1, x))) ∧ l (sy-i ('ywa2, x)) ∧ l (sy-i ('ywa3, x))) → ((l (sy-i ('ypc, x)) − 1) ≠ 0)

Theorem: sc-pcn0-2 ((¬ empty (x)) ∧ l (sy-i ('ywa1, x)) ∧ l (sy-i ('ywa3, x)) ∧ l (sy-i ('ywa2, x))) → (((l (sy-i ('ypc, x)) − 1) − 1) ≠ 0)

; Now it goes through:

Theorem: stutcorr-pc-f ((¬ empty (x)) ∧ (¬ empty (p (x))) ∧ l (sy-i ('ywa1k, p (x)))) → (l (ivpc (x)) = n-pc (l (ivpc (p (x))), l (sy-i ('yrf, p (x)))))

Event: Disable stutcorr-pc-f.

Theorem: stutcorr-rf-f ((¬ empty (x)) ∧ (¬ empty (p (x))) ∧ l (sy-i ('ywa1k, p (x)))) → (l (sy-i ('yrf, x)) = n-rf (l (ivpc (p (x))), l (sy-i ('yrf, p (x)))))

Event: Disable stutcorr-rf-f.

; We have to simultaneously prove stuttering of RF and ivPC:

Theorem: stutcorr-l (l (stut (sy-s ('ypc, x), s-not (sy-i ('ywa1k, x)))) = l (ivpc (x))) ∧ (l (stut (sy-s ('yrf, x), s-not (sy-i ('ywa1k, x)))) = l (sy-i ('yrf, x)))

; Now standard passage to strings:

Theorem: apl-split-irf (¬ empty (x)) → (sy-i ('yrf, x) = a (p (sy-i ('yrf, x)), l (sy-i ('yrf, x))))

Theorem: apl-split-stut (¬ empty (x)) → (stut (sy-s ('yrf, x), s-not (sy-i ('ywa1k, x)))

= a (p (stut (sy-s ('yrf, x), s-not (sy-i ('ywa1k, x)))), l (stut (sy-s ('yrf, x), s-not (sy-i ('ywa1k, x))))))

; YEEEEAHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHH!

Theorem: src-cpu-correct stut (sy-s ('yrf, x), s-not (sy-i ('ywa1k, x))) = sy-i ('yrf, x)

; eof: srccpu.bm
;))

Index

a, 4, 6–13, 15, 17, 22, 29, 38 a2-bc-s-eql0, 7 a2-bc-s-inc, 6 a2-bc-s-k, 18 a2-bc-s-mux, 5 a2-bc-s-sub1, 29 a2-bc-s-ualu, 13 a2-bc-s-ulk, 14 a2-bc-s-umb, 8 a2-bc-s-umf, 12 a2-bc-s-umr, 11 a2-bc-s-umw, 10 a2-bc-s-upd, 15 a2-bnc-s-eql0, 7 a2-bnc-s-inc, 6 a2-bnc-s-k, 18 a2-bnc-s-mux, 5 a2-bnc-s-sub1, 29 a2-bnc-s-ualu, 13 a2-bnc-s-ulk, 14 a2-bnc-s-umb, 8 a2-bnc-s-umf, 12 a2-bnc-s-umr, 11 a2-bnc-s-umw, 10 a2-bnc-s-upd, 15 a2-e-s-eql0, 7 a2-e-s-inc, 6 a2-e-s-k, 18 a2-e-s-mux, 4 a2-e-s-sub1, 29 a2-e-s-ualu, 13 a2-e-s-ulk, 14 a2-e-s-umb, 8 a2-e-s-umf, 11 a2-e-s-umr, 10 a2-e-s-umw, 9 a2-e-s-upd, 15 a2-e-sy-i, 21 a2-e-sy-s, 17 a2-empty-s-eql0, 7 a2-empty-s-inc, 6 a2-empty-s-k, 17 a2-empty-s-mux, 4 a2-empty-s-sub1, 29 a2-empty-s-ualu, 12 a2-empty-s-ulk, 14 a2-empty-s-umb, 8 a2-empty-s-umf, 11 a2-empty-s-umr, 10 a2-empty-s-umw, 9 a2-empty-s-upd, 15 a2-empty-sy-i, 21 a2-empty-sy-s, 17 a2-hc-s-eql0, 7 a2-hc-s-inc, 6 a2-hc-s-k, 18 a2-hc-s-mux, 5 a2-hc-s-sub1, 29 a2-hc-s-ualu, 13 a2-hc-s-ulk, 14 a2-hc-s-umb, 8 a2-hc-s-umf, 12 a2-hc-s-umr, 11 a2-hc-s-umw, 9 a2-hc-s-upd, 15 a2-ic-s-eql0, 7 a2-ic-s-inc, 6 a2-ic-s-k, 18 a2-ic-s-mux, 5 a2-ic-s-sub1, 29 a2-ic-s-ualu, 13 a2-ic-s-ulk, 14 a2-ic-s-umb, 8 a2-ic-s-umf, 12 a2-ic-s-umr, 10 a2-ic-s-umw, 9 a2-ic-s-upd, 15 a2-lc-s-eql0, 7 a2-lc-s-inc, 6 a2-lc-s-k, 18 a2-lc-s-mux, 5 a2-lc-s-sub1, 29 a2-lc-s-ualu, 13 a2-lc-s-ulk, 14 a2-lc-s-umb, 8 a2-lc-s-umf, 12 a2-lc-s-umr, 10 a2-lc-s-umw, 9 a2-lc-s-upd, 15 a2-lp-s-eql0, 7 a2-lp-s-inc, 6 a2-lp-s-k, 18 a2-lp-s-mux, 4 a2-lp-s-sub1, 29 a2-lp-s-ualu, 13 a2-lp-s-ulk, 14 a2-lp-s-umb, 8 a2-lp-s-umf, 11 a2-lp-s-umr, 10 a2-lp-s-umw, 9 a2-lp-s-upd, 15 a2-lp-sy-i, 21 a2-lp-sy-s, 17 a2-lpe-s-eql0, 7 a2-lpe-s-inc, 6 a2-lpe-s-k, 18 a2-lpe-s-mux, 5 a2-lpe-s-sub1, 29 a2-lpe-s-ualu, 13 a2-lpe-s-ulk, 14 a2-lpe-s-umb, 8 a2-lpe-s-umf, 11 a2-lpe-s-umr, 10 a2-lpe-s-umw, 9 a2-lpe-s-upd, 15 a2-lpe-sy-i, 21 a2-lpe-sy-s, 17 a2-pc-s-eql0, 7 a2-pc-s-inc, 6 a2-pc-s-k, 18 a2-pc-s-mux, 5 a2-pc-s-sub1, 29 a2-pc-s-ualu, 13 a2-pc-s-ulk, 14 a2-pc-s-umb, 8 a2-pc-s-umf, 12 a2-pc-s-umr, 11 a2-pc-s-umw, 9 a2-pc-s-upd, 15 a2-pc-sy-i, 22 a2-pc-sy-s, 17 apl-split-irf, 38 apl-split-stut, 38

b, 5–8, 10–15, 18, 22, 26, 29, 32 bn, 5–8, 10–15, 18, 24, 29, 32

corr-i-pr, 28 corr-i-pr-h, 31 corr-n-pc, 31 corr-n-rf, 31 corr-s-pr, 28 corr-s-pr-h, 31

e, 4, 6–24, 29, 32 empty, 4–26, 28–38 eql0, 6, 7, 30, 34–36 eqlen, 5–11, 13–15, 17, 18, 21, 29

h, 5–9, 11–15, 18, 22, 25, 29, 31, 32

i, 5–10, 12–16, 18–21, 29

inc, 5, 6

ivpc, 30, 32, 37, 38

ivpc-1, 32 ivpc-e, 32

k, 17, 18

l, 4–15, 17, 18, 22, 24–26, 28–38 len, 4–15, 17, 18, 21, 23–25, 29

mux, 4, 5, 30

n-pc, 30–32, 38 n-rf, 31, 32, 38

p, 4–26, 28, 29, 31, 32, 37, 38

pci, 3, 4, 16, 19, 32 pci-numberp, 4

res, 30, 31, 34–36 s-eql0, 7, 16, 20 s-equal, 20 s-if, 4, 30 s-inc, 6, 16, 20 s-k, 17, 18, 20, 21 s-mux, 4, 5, 16, 19, 20 s-not, 30, 38 s-sub1, 29, 30 s-ualu, 12, 13, 16, 20 s-ulk, 13, 14, 16, 21 s-umb, 8, 16, 20 s-umf, 11, 12, 16, 20 s-umr, 10, 11, 16, 20 s-umw, 9, 10, 16, 20 s-upd, 15, 17, 21 sc-pc-f-2, 37 sc-pc-f-3, 37 sc-pc-t-1, 36 sc-pc-t-2, 36 sc-pc-t-3, 36 sc-pcn0-0, 37 sc-pcn0-1, 37 sc-pcn0-2, 37 sfix, 17, 21 smux-is-sif, 4 src-cpu-correct, 38 stut, 22, 23, 25, 38 stut-e, 23 stut-empty, 23 stut-induct, 23 stut-inv, 25 stut-inv0, 25 stut-num, 24, 25 stut-num-eq-0, 24 stut-num-lessp, 24 stut-num-rem-len, 24 stut-p, 23 stut-r, 22–26 stut-r-closed, 24 stut-r-e, 23 stut-r-indstep, 26 stut-r-indstep-num, 25 stut-r-len, 23 stut-r-not-empty, 23 stut-r-p, 23 stut-rem, 24–26 stut-rem-empty, 24 stut-rem-len, 24 stut-rem-len2, 24 stutcorr-l, 38 stutcorr-pc-f, 38 stutcorr-pc-t, 37 stutcorr-rf-f, 38 stutcorr-rf-t, 28 sy-i, 19–22, 28, 30, 31, 33–38 sy-i-inv-1, 36 sy-i-inv-2, 35 sy-i-inv-3, 35 sy-i-inv-4, 34 sy-i-pc-numberp, 30 sy-i-yra-noad, 33 sy-i-yrd1, 33 sy-i-yrd2, 33 sy-i-yrd3, 33 sy-s, 16, 17, 28, 31, 32, 38 sy-s-reversal-hyp-hack, 32 sy-s-reversal-pc, 32 sy-s-reversal-pr, 32 sy-s-reversal-rf, 32

topor-sy-i, 18 topor-sy-s, 16

ualu, 12, 13, 30

ulk, 13, 14, 28, 30, 33–36

ulk-upd, 28

umb, 8, 27, 30, 34–36 umb-numberp, 27 umf, 11, 12, 30 umr, 10, 11, 27, 30 umr-noad, 27 umw, 9, 27, 31, 34–36 umw-noad, 27 upd, 14, 15, 27, 28, 31, 33–35 upd-noad, 27