#|
Copyright (C) 1985 by Warren A. Hunt, Jr.  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) 1985 by Warren A. Hunt, Jr.  All
Rights Reserved."
NO WARRANTY
Warren A. Hunt, Jr. PROVIDES 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 Warren A. Hunt, Jr. 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.
|#
;;; -*- Mode: LISP; Base: 10; Syntax: Zetalisp -*-
;   The Mechanical Verification of the FM8501 Microprocessor
;                             by
;                       Warren A. Hunt, Jr.

Event: Start with the initial thm theory.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                             lemmas about PLUS                                ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Event: For efficiency, compile those definitions not yet compiled.

Theorem: plus-1 (1 + x) = (1 + x)

Theorem: plus-right-id (y ∉ N) → ((x + y) = fix (x))

Theorem: plus-add1 (x + (1 + y)) = if y ∈ N then 1 + (x + y)

else 1 + x endif

Theorem: commutativity2-of-plus (x + (y + z)) = (y + (x + z))

Theorem: commutativity-of-plus (x + y) = (y + x)

Theorem: associativity-of-plus ((x + y) + z) = (x + (y + z))

Theorem: plus-equal-0 ((a + b) = 0) = ((a ≃ 0) ∧ (b ≃ 0))

Theorem: plus-cancellation ((a + b) = (a + c)) = (fix (b) = fix (c))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                             lemmas about TIMES                               ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: times-zero2 (y ∉ N) → ((x ∗ y) = 0)

Theorem: distributivity-of-times-over-plus (x ∗ (y + z)) = ((x ∗ y) + (x ∗ z))

Theorem: times-add1 (x ∗ (1 + y)) = if y ∈ N then x + (x ∗ y)

else fix (x) endif Theorem: commutativity-of-times (x ∗ y) = (y ∗ x)

Theorem: commutativity2-of-times (x ∗ (y ∗ z)) = (y ∗ (x ∗ z))

Theorem: associativity-of-times ((x ∗ y) ∗ z) = (x ∗ (y ∗ z))

Theorem: equal-times-0 ((x ∗ y) = 0) = ((x ≃ 0) ∨ (y ≃ 0))

Theorem: times-1 (1 ∗ x) = fix (x)

Theorem: equal-bools (((bool1 = t) ∨ (bool1 = f)) ∧ ((bool2 = t) ∨ (bool2 = f))) → ((bool1 = bool2 ) = ((bool1 → bool2 ) ∧ (bool2 → bool1 )))

Event: Disable equal-bools.

Theorem: lessp-times ((y ∗ x) < (x ∗ z)) = ((x ≄ 0) ∧ (y < z))

Theorem: times-2-not-1 (2 ∗ x) ≠ 1

Theorem: lessp-crock1 ((z + (2 ∗ v ∗ w)) < w) = ((v ≃ 0) ∧ (z < w))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                             lemmas about EXP                                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: exp (i, j ) = if j ≃ 0 then 1

else i ∗ exp (i, j − 1) endif

Theorem: exp-plus exp (i, j + k) = (exp (i, j ) ∗ exp (i, k))

Theorem: exp-of-0 exp (0, k) = if k ≃ 0 then 1

else 0 endif

Theorem: exp-of-1 exp (1, k) = 1

Theorem: exp-by-0 exp (x, 0) = 1

Theorem: exp-times exp (i ∗ j , k) = (exp (i, k) ∗ exp (j , k))

Theorem: exp-2-never-0 0 < exp (2, i)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                           lemmas about DIFFERENCE                            ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: difference-elim ((y ∈ N) ∧ (y ≮ x)) → ((x + (y − x)) = y)

Theorem: difference-2 (x − 2) = ((x − 1) − 1)

Theorem: difference-x-x (x − x) = 0

Theorem: difference-plus ((j + x) − j ) = fix (x)

Theorem: difference-plus-cancellation ((a + x) − (a + y)) = (x − y)

Theorem: pathological-difference (x < y) → ((x − y) = 0)

Theorem: difference-crock1 ((x + (y − z)) − y) = if y < z then x − y

else x − z endif Theorem: difference-difference ((x − y) − z) = (x − (y + z))

Theorem: lessp-difference ((x − y) < x) = ((x ≄ 0) ∧ (y ≄ 0))

Theorem: difference-add1 ((1 + x) − y) = if y < (1 + x) then 1 + (x − y)

else 0 endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                       lemmas about QUOTIENT and REMAINDER                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: remainder-quotient ((x mod y) + (y ∗ (x ÷ y))) = fix (x)

Theorem: remainder-by-1 (y mod 1) = 0

Theorem: remainder-by-nonnumber (x ∉ N) → ((y mod x) = fix (y))

Theorem: lessp-remainder ((x mod y) < y) = (y ≄ 0)

Theorem: remainder-quotient-elim ((y ≄ 0) ∧ (x ∈ N)) → (((x mod y) + (y ∗ (x ÷ y))) = x)

Theorem: remainder-x-x (x mod x) = 0

Theorem: remainder-plus ((j + x) mod j ) = (x mod j )

Theorem: remainder-plus-times ((x + (i ∗ j )) mod j ) = (x mod j )

Theorem: remainder-plus-times-commuted ((x + (j ∗ i)) mod j ) = (x mod j )

Theorem: remainder-times ((j ∗ i) mod j ) = 0 Theorem: remainder-add1-times ((1 + (j ∗ i)) mod j ) = (1 mod j )

Theorem: quotient-plus-times ((x + (i ∗ j )) ÷ j ) = if j ≃ 0 then 0

else i + (x ÷ j ) endif

Theorem: quotient-plus-times-commuted ((x + (j ∗ i)) ÷ j ) = if j ≃ 0 then 0

else i + (x ÷ j ) endif

Theorem: quotient-times ((j ∗ i) ÷ j ) = if j ≃ 0 then 0

else fix (i) endif

Theorem: quotient-add1-times ((1 + (j ∗ i)) ÷ j ) = if j ≃ 0 then 0

else i + (1 ÷ j ) endif

Event: Disable times.

Theorem: times-distributes-over-remainder ((x ∗ y) mod (x ∗ z)) = (x ∗ (y mod z))

Theorem: remainder-of-1 (1 mod x) = if x = 1 then 0

else 1 endif

Theorem: remainder-crock1 ((x ∈ N) ∧ (x < z) ∧ (v ∈ N) ∧ (z ∈ N) ∧ (z ≠ 0)) → (((1 + ((2 ∗ x) + (2 ∗ v ∗ z))) mod (2 ∗ z))

= (1 + (2 ∗ x)))

Theorem: times-2-distributes-over-remainder-add1 ((1 + (2 ∗ y)) mod (2 ∗ z)) = (1 + (2 ∗ (y mod z)))

Theorem: remainder-crock2 (v < exp (2, size − 1)) → ((((2 ∗ v) + (2 ∗ w ∗ exp (2, size − 1)))

mod (2 ∗ exp (2, size − 1))) = (2 ∗ v))

Theorem: remainder-crock3 ((x + (y − z)) mod y) = if (x + (y − z)) < y then x + (y − z)

elseif y < z then x mod y else (x − z) mod y endif

Theorem: remainder-of-0 (0 mod x) = 0

Theorem: remainder-crock4 ((1 + (x + (y − z))) mod y) = if (1 + (x + (y − z))) < y then 1 + (x + (y − z))

elseif y < z then (1 + x) mod y

elseif z < (1 + x) then (1 + (x − z)) mod y else 0 endif

Theorem: quotient-2i-by-2 (((1 + (i + i)) ÷ 2) = fix (i)) ∧ (((i + i) ÷ 2) = fix (i))

Theorem: remainder-2i-by-2 (((1 + (i + i)) mod 2) = 1) ∧ (((i + i) mod 2) = 0)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                           boolean operations                                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: xor (x, y) = if x

then if y then f

else t endif elseif y then t else f endif

Definition: b-not (x) = if x then f

else t endif

Definition: b-nand (x, y) = if x

then if y then f

else t endif else t endif Definition: b-nor (x, y) = if x then f

elseif y then f else t endif

Definition: b-and (x, y) = (x ∧ y)

Definition: b-or (x, y) = (x ∨ y)

Definition: b-xor (x, y) = if x

then if y then f

else t endif elseif y then t else f endif

Definition: b-equv (x, y) = if x

then if y then t

else f endif elseif y then f else t endif

Definition: boolp (x) = (truep (x) ∨ falsep (x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                          primitive bit vector operations                     ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Event: Add the shell bitv, with bottom object function symbol btm, with recognizer function symbol bitvp, and 2 accessors: bit, with type restriction (one-of truep falsep) and default value false; vec, with type restriction (one-of bitvp) and default value btm.

Theorem: boolp-bit boolp (bit (x))

Definition: fix-bv (x) = if bitvp (x) then x

else btm endif Definition: carry (c) = if c then 1

else 0 endif

Definition: size (a) = if bitvp (a)

then if a = btm then 0

else 1 + size (vec (a)) endif else 0 endif

Definition: trunc (a, n) = if n ≃ 0 then btm

else bitv (bit (a), trunc (vec (a), n − 1)) endif

Definition: compl (x) = if bitvp (x)

then if x = btm then btm

else bitv (¬ bit (x), compl (vec (x))) endif else btm endif

; IT MAY BE POSSIBLE TO ELIMINATE THE C FLG.

Definition: incr (c, x) = if bitvp (x)

then if x = btm then btm

else bitv (xor (c, bit (x)), incr (c ∧ bit (x), vec (x))) endif else btm endif

Definition: bitn (x, n) = if n ≃ 0 then f

elseif n = 1 then bit (x) else bitn (vec (x), n − 1) endif

Definition: btmp (a) = if bitvp (a) then a = btm

else t endif Definition: all-zerosp (a) = if bitvp (a)

then if a = btm then t

else (¬ bit (a)) ∧ all-zerosp (vec (a)) endif else t endif

Definition: all-onesp (a) = if bitvp (a)

then if a = btm then t

else bit (a) ∧ all-onesp (vec (a)) endif else t endif

Theorem: size-of-trunc size (trunc (a, n)) = fix (n)

Theorem: size-of-compl size (compl (a)) = size (a)

Theorem: size-of-incr size (incr (c, a)) = size (a)

Theorem: incr-f-noop incr (f, a) = fix-bv (a)

Theorem: size-0 (size (x) = 0) = btmp (x)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Definitions about logical functions                               ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: v-not (a) = if bitvp (a)

then if a = btm then btm

else bitv (¬ bit (a), v-not (vec (a))) endif else btm endif Definition: v-or (a, b) = if bitvp (a)

then if a = btm then btm

else bitv (bit (a) ∨ bit (b), v-or (vec (a), vec (b))) endif else btm endif

Definition: v-and (a, b) = if bitvp (a)

then if a = btm then btm

else bitv (bit (a) ∧ bit (b), v-and (vec (a), vec (b))) endif else btm endif

Definition: v-xor (a, b) = if bitvp (a)

then if a = btm then btm

else bitv (xor (bit (a), bit (b)), v-xor (vec (a), vec (b))) endif else btm endif

Definition: bv-not (a) = if bitvp (a)

then if a = btm then btm

else bitv (b-not (bit (a)), bv-not (vec (a))) endif else btm endif

Definition: bv-or (a, b) = if bitvp (a)

then if a = btm then btm

else bitv (b-or (bit (a), bit (b)), bv-or (vec (a), vec (b))) endif else btm endif

Definition: bv-and (a, b) = if bitvp (a)

then if a = btm then btm

else bitv (b-and (bit (a), bit (b)), bv-and (vec (a), vec (b))) endif else btm endif

Definition: bv-xor (a, b) = if bitvp (a) then if a = btm then btm

else bitv (b-xor (bit (a), bit (b)), bv-xor (vec (a), vec (b))) endif else btm endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                 TC numbers and their operations                              ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: tcp (x) = ((x ∈ N) ∨ (negativep (x) ∧ (negative-guts (x) ≄ 0)))

Definition: tc-in-rangep (x, n) = if n ≃ 0 then f

elseif negativep (x) then exp (2, n − 1) ≮ negative-guts (x)

else x < exp (2, n − 1) endif

Definition: add (x, y) = if negativep (x)

then if negativep (y) then − (negative-guts (x) + negative-guts (y)) elseif y < negative-guts (x) then − (negative-guts (x) − y) else y − negative-guts (x) endif

elseif negativep (y)

then if x < negative-guts (y) then − (negative-guts (y) − x)

else x − negative-guts (y) endif else x + y endif

Theorem: commutativity2-of-add add (x, add (y, z)) = add (y, add (x, z))

Theorem: commutativity-of-add add (x, y) = add (y, x)

Theorem: associativity-of-add add (add (x, y), z) = add (x, add (y, z))

Theorem: add-with-carry-of-negatives-is-negative (tcp (x) ∧ tcp (y) ∧ negativep (x) ∧ negativep (y)) → negativep (add (x, add (y, carry (c))))

Theorem: add-with-carry-of-non-negatives-is-non-negative (tcp (x) ∧ tcp (y) ∧ (¬ negativep (x)) ∧ (¬ negativep (y))) → (¬ negativep (add (x, add (y, carry (c)))))

Theorem: overflow-lemma1 (tcp (x) ∧ tcp (y) ∧ tc-in-rangep (x, n) ∧ tc-in-rangep (y, n) ∧ negativep (add (x, add (y, carry (c))))) → (¬ negativep (add (x, add (y, add (carry (c), exp (2, n))))))

Theorem: overflow-lemma2 (tcp (x) ∧ tcp (y) ∧ tc-in-rangep (x, n) ∧ tc-in-rangep (y, n) ∧ (¬ negativep (add (x, add (y, carry (c)))))) → negativep (add (x, add (y, add (carry (c), − exp (2, n)))))

Theorem: opposite-signs-implies-tc-in-rangep (tcp (x) ∧ tcp (y) ∧ tc-in-rangep (x, n) ∧ tc-in-rangep (y, n) ∧ negativep (x) ∧ (¬ negativep (y))) → tc-in-rangep (add (x, add (y, carry (c))), n)

Theorem: opposite-signs-implies-tc-in-rangep-commuted (tcp (x) ∧ tcp (y) ∧ tc-in-rangep (x, n) ∧ tc-in-rangep (y, n) ∧ negativep (x) ∧ (¬ negativep (y))) → tc-in-rangep (add (y, add (x, carry (c))), n)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;             Mapping Functions between BV, NAT, and TC                        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: nat-to-bv (n, size) = if size ≃ 0 then btm

else bitv (if (n mod 2) ≃ 0 then f else t endif, nat-to-bv (n ÷ 2, size − 1)) endif

Definition: bv-to-nat (x) = if bitvp (x)

then if x = btm then 0

else if bit (x) then 1 else 0 endif + (2 ∗ bv-to-nat (vec (x))) endif

else 0 endif

Definition: tc-to-bv (x, size) = if negativep (x) then incr (t, compl (nat-to-bv (negative-guts (x), size)))

else nat-to-bv (x, size) endif

Definition: bv-to-tc (x) = if bitn (x, size (x)) then − bv-to-nat (incr (t, compl (x)))

else bv-to-nat (x) endif

Definition: nat-to-tc (n, size) = if n < exp (2, size − 1) then n

else − (exp (2, size) − n) endif

Definition: tc-to-nat (n, size) = if negativep (n) then exp (2, size) − negative-guts (n)

else n endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                   Elementary Properties of Mapping Functions                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: size-of-nat-to-bv size (nat-to-bv (n, size)) = fix (size)

Theorem: size-of-tc-to-bv size (tc-to-bv (x, size)) = fix (size)

Theorem: bv-to-nat-of-incr bv-to-nat (incr (t, a)) = if all-onesp (a) then 0

else 1 + bv-to-nat (a) endif

Theorem: bitn-implies-compl-not-all-onesp bitn (a, i) → (¬ all-onesp (compl (a)))

Theorem: upper-bound-on-bv-to-nat bv-to-nat (a) < exp (2, size (a))

Theorem: bv-to-nat-of-compl bv-to-nat (compl (a)) = ((exp (2, size (a)) − 1) − bv-to-nat (a))

Theorem: bv-to-nat-to-tc-lemma1 bitn (a, size (a)) → (bv-to-nat (incr (t, compl (a))) = (exp (2, size (a)) − bv-to-nat (a)))

Theorem: bv-to-nat-to-tc-lemma2 bitn (a, size (a)) = if size (a) ≃ 0 then f

else bv-to-nat (a) ≮ exp (2, size (a) − 1) endif

Theorem: bv-to-nat-of-trunc bv-to-nat (trunc (a, n)) = (bv-to-nat (a) mod exp (2, n))

Theorem: all-onesp-of-compl all-onesp (compl (a)) = (bv-to-nat (a) = 0)

Theorem: tcp-bv-to-tc tcp (bv-to-tc (a))

Theorem: upper-bound-on-non-negative-bv-to-nat (bitvp (a) ∧ (a ≠ btm) ∧ (¬ bitn (a, size (a)))) → (bv-to-nat (a) < exp (2, size (a) − 1))

Theorem: lower-bound-on-negative-bv-to-nat (bitvp (a) ∧ (a ≠ btm) ∧ bitn (a, size (a))) → (bv-to-nat (a) ≮ exp (2, size (a) − 1))

Theorem: tc-in-rangep-of-bv-to-tc (n = size (a)) → (tc-in-rangep (bv-to-tc (a), n) = (bitvp (a) ∧ (a ≠ btm)))

Theorem: bitn-means-negativep (n = size (a)) → (bitn (a, n) = negativep (bv-to-tc (a)))

Event: Disable bitn-means-negativep.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Relationship between TC and NAT addition                          ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: plus-to-add (tcp (x) ∧ tcp (y) ∧ tc-in-rangep (x, n) ∧ tc-in-rangep (y, n)) → (nat-to-tc ((carry (c) + tc-to-nat (x, n) + tc-to-nat (y, n))

mod exp (2, n), n)

= if tc-in-rangep (add (x, add (y, carry (c))), n) then add (x, add (y, carry (c))) elseif negativep (add (x, add (y, carry (c)))) then add (x, add (y, add (carry (c), exp (2, n)))) else add (x, add (y, add (carry (c), − exp (2, n)))) endif)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;      Fundamental Relationships between the Mapping Functions                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: bv-to-nat-to-bv (size = size (a)) → (nat-to-bv (bv-to-nat (a), size) = fix-bv (a))

Theorem: bv-to-nat-to-tc bv-to-tc (a) = nat-to-tc (bv-to-nat (a), size (a))

Event: Disable bv-to-nat-to-tc.

Theorem: nat-to-bv-to-nat bv-to-nat (nat-to-bv (n, size)) = (n mod exp (2, size))

Theorem: tc-to-bv-to-nat (tcp (x) ∧ tc-in-rangep (x, n)) → (tc-to-nat (x, n) = bv-to-nat (tc-to-bv (x, n)))

Event: Disable tc-to-bv-to-nat.

Theorem: bv-to-tc-to-nat (n = size (a)) → (tc-to-nat (bv-to-tc (a), n) = bv-to-nat (a))

Event: Disable bv-to-tc-to-nat.

Theorem: incr-compl-nat-to-bv-0 incr (t, compl (nat-to-bv (0, size (x)))) = nat-to-bv (0, size (x))

Theorem: bitn-on-implies-non-0 bitn (a, n) → (bv-to-nat (a) ≠ 0)

Theorem: bv-to-tc-to-bv (size = size (a)) → (tc-to-bv (bv-to-tc (a), size) = fix-bv (a))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                                   Bridge Lemmas                              ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: embed-in-nat-to-bv (x = y) → (nat-to-bv (x, n) = nat-to-bv (y, n))

Theorem: embed-in-tc-to-bv (x = y) → (tc-to-bv (x, n) = tc-to-bv (y, n))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                                   BV-ADDER                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: bv-adder (c, a, b) = if bitvp (a)

then if a = btm then bitv (c, btm)

else bitv (b-xor (c, b-xor (bit (a), bit (b))),

bv-adder (b-or (b-and (bit (a), bit (b)), b-or (b-and (bit (a), c),

b-and (bit (b), c))),

vec (a),

vec (b))) endif

else bitv (c, btm) endif

Definition: bv-adder-output (c, a, b) = trunc (bv-adder (c, a, b), size (a))

Definition: bv-adder-carry-out (c, a, b) = bitn (bv-adder (c, a, b), 1 + size (a))

Definition: bv-adder-overflowp (c, a, b) = b-and (b-equv (bitn (a, size (a)), bitn (b, size (b))),

b-xor (bitn (a, size (a)), bitn (bv-adder-output (c, a, b), size (a))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                    Fundamental Properties of BV-ADDER                        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: size-of-bv-adder size (bv-adder (c, a, b)) = (1 + size (a))

Theorem: bv-to-nat-of-bv-adder (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-to-nat (bv-adder (c, a, b))

= (bv-to-nat (a) + bv-to-nat (b) + carry (c)))

; From here on we use only the above two lemmas about BV-ADDER
; The definition of BV-ADDER is disabled and henceforth any adder
; with the two properties above would suffice.

Event: Disable bv-adder.

Theorem: bv-adder-non-btm bv-adder (c, a, b) ≠ btm

Theorem: size-bv-adder-output size (bv-adder-output (c, a, b)) = size (a)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                 NAT view of BV-ADDER                                         ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: nat-interpretation-of-bv-adder-output (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-to-nat (bv-adder-output (c, a, b))

= if (bv-to-nat (a) + bv-to-nat (b) + carry (c))

< exp (2, size (a)) then bv-to-nat (a) + bv-to-nat (b) + carry (c) else (bv-to-nat (a) + bv-to-nat (b) + carry (c))

mod exp (2, size (a)) endif)

Event: Disable nat-interpretation-of-bv-adder-output.

Theorem: nat-bv-adder-output-seen-as-bit-vector (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-adder-output (c, a, b)

= if (bv-to-nat (a) + bv-to-nat (b) + carry (c))

< exp (2, size (a)) then nat-to-bv (bv-to-nat (a) + bv-to-nat (b) + carry (c),

size (a))

else nat-to-bv ((bv-to-nat (a)

+ bv-to-nat (b) + carry (c)) mod exp (2, size (a)), size (a)) endif)

Event: Disable nat-bv-adder-output-seen-as-bit-vector.

Theorem: nat-interpretation-of-bv-adder-carry-out (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-adder-carry-out (c, a, b)

= ((bv-to-nat (a) + bv-to-nat (b) + carry (c)) ≮ exp (2, size (a))))

Event: Disable nat-interpretation-of-bv-adder-carry-out.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;                                                                              ;;
;;                      TC view of BV-ADDER                                     ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: tc-interpretation-of-bv-adder-output-lemma1 (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-to-tc (trunc (bv-adder (c, a, b), size (a)))

= nat-to-tc ((carry (c) + bv-to-nat (a) + bv-to-nat (b)) mod exp (2, size (a)), size (a)))

Theorem: tc-interpretation-of-bv-adder-output (bitvp (a) ∧ bitvp (b) ∧ (a ≠ btm) ∧ (b ≠ btm) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-to-tc (bv-adder-output (c, a, b))

= if tc-in-rangep (add (bv-to-tc (a), add (bv-to-tc (b), carry (c))),

size (a))

then add (bv-to-tc (a), add (bv-to-tc (b), carry (c)))

elseif negativep (add (bv-to-tc (a), add (bv-to-tc (b), carry (c)))) then add (bv-to-tc (a),

add (bv-to-tc (b), add (carry (c), exp (2, size (a)))))

else add (bv-to-tc (a),

add (bv-to-tc (b), add (carry (c), − exp (2, size (a))))) endif)

Event: Disable tc-interpretation-of-bv-adder-output-lemma1.

Event: Disable tc-interpretation-of-bv-adder-output.

Theorem: tc-bv-adder-output-seen-as-bit-vector-lemma1 (bitvp (a) ∧ bitvp (b) ∧ (a ≠ btm) ∧ (b ≠ btm) ∧ (size (a) = size (b)) ∧ boolp (c)) → (tc-to-bv (bv-to-tc (bv-adder-output (c, a, b)),

size (bv-adder-output (c, a, b)))

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (a),

add (bv-to-tc (b), carry (c))), size (a))

then add (bv-to-tc (a), add (bv-to-tc (b), carry (c))) elseif negativep (add (bv-to-tc (a),

add (bv-to-tc (b), carry (c))))

then add (bv-to-tc (a),

add (bv-to-tc (b),

add (carry (c), exp (2, size (a)))))

else add (bv-to-tc (a),

add (bv-to-tc (b),

add (carry (c), − exp (2, size (a))))) endif,

size (a)))

Event: Disable tc-bv-adder-output-seen-as-bit-vector-lemma1.

Theorem: tc-bv-adder-output-seen-as-bit-vector (bitvp (a) ∧ bitvp (b) ∧ (a ≠ btm) ∧ (b ≠ btm) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-adder-output (c, a, b)

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (a),

add (bv-to-tc (b), carry (c))), size (a))

then add (bv-to-tc (a), add (bv-to-tc (b), carry (c))) elseif negativep (add (bv-to-tc (a),

add (bv-to-tc (b), carry (c))))

then add (bv-to-tc (a),

add (bv-to-tc (b),

add (carry (c), exp (2, size (a)))))

else add (bv-to-tc (a),

add (bv-to-tc (b),

add (carry (c), − exp (2, size (a))))) endif,

size (a)))

Event: Disable tc-bv-adder-output-seen-as-bit-vector.

Theorem: tc-interpretation-of-bv-adder-overflowp (bitvp (a) ∧ bitvp (b)

∧ (size (a) = size (b)) ∧ boolp (c) ∧ (a ≠ btm) ∧ (b ≠ btm)) → (bv-adder-overflowp (c, a, b)

= (¬ tc-in-rangep (add (bv-to-tc (a), add (bv-to-tc (b), carry (c))), size (a))))

Event: Disable tc-interpretation-of-bv-adder-overflowp.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Definitions and lemmas about subtraction functions                ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;(defn bv-subtracter (c a b)    ; B - A - C
;  (bv-adder (b-not c)
;            (bv-not a)
;            b))

Definition: bv-subtracter-output (c, a, b) = bv-adder-output (b-not (c), bv-not (a), b)

Definition: bv-subtracter-carry-out (c, a, b) = b-not (bv-adder-carry-out (b-not (c), bv-not (a), b))

Definition: bv-subtracter-overflowp (c, a, b) = bv-adder-overflowp (b-not (c), bv-not (a), b)

Theorem: bv-not-is-compl bv-not (a) = compl (a)

Theorem: subtract-lemma1 (size (b) = size (a)) → (((bv-to-nat (b) − bv-to-nat (a)) < exp (2, size (a))) = t)

Theorem: subtract-lemma2 ((b ≄ 0) ∧ ((b − 1) ≮ a)) → (((b + ((n − 1) − a)) < n) = f)

Theorem: subtract-lemma3 ((b ≄ 0) ∧ ((b − 1) ≮ a) ∧ (a < n)) → (((b + ((n − 1) − a)) − n) = ((b − 1) − a))

Theorem: subtract-lemma4 (size (b) = size (a)) → ((((bv-to-nat (b) − 1) − bv-to-nat (a)) < exp (2, size (a))) = t)

Theorem: size-bv-subtracter-output size (bv-subtracter-output (c, a, b)) = size (a)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                 NAT view of BV-SUBTRACTER                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: nat-interpretation-of-bv-subtracter-output (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-to-nat (bv-subtracter-output (c, a, b))

= if bv-to-nat (b) ≮ (bv-to-nat (a) + carry (c)) then bv-to-nat (b) − (bv-to-nat (a) + carry (c)) else exp (2, size (a))

− ((bv-to-nat (a) + carry (c)) − bv-to-nat (b)) endif)

Event: Disable nat-interpretation-of-bv-subtracter-output.

Theorem: nat-bv-subtracter-output-seen-as-bit-vector (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-subtracter-output (c, a, b)

= if bv-to-nat (b) ≮ (bv-to-nat (a) + carry (c))

then nat-to-bv (bv-to-nat (b) − (bv-to-nat (a) + carry (c)),

size (a))

else nat-to-bv (exp (2, size (a))

− ((bv-to-nat (a) + carry (c)) − bv-to-nat (b)),

size (a)) endif)

Event: Disable nat-bv-subtracter-output-seen-as-bit-vector.

Theorem: equal-lessp-hack ((x < y) = z) = if x < y then z = t

else z = f endif Theorem: nat-interpretation-of-bv-subtracter-carry-out (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-subtracter-carry-out (c, a, b)

= (bv-to-nat (b) < (bv-to-nat (a) + carry (c))))

Event: Disable nat-interpretation-of-bv-subtracter-carry-out.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                      TC view of BV-SUBTRACTER                                ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: tc-minus (x) = if negativep (x) then negative-guts (x)

elseif x ≃ 0 then 0 else − x endif

Theorem: tc-minus-add tc-minus (add (x, y)) = add (tc-minus (x), tc-minus (y))

Theorem: bitn-compl ((n ≄ 0) ∧ (size (a) ≮ n)) → (bitn (compl (a), n) = (¬ bitn (a, n)))

;(prove-lemma bitn-on-implies-non-0 (rewrite)
;  (implies (bitn a n) (not (equal (bv-to-nat a) 0))))

Theorem: equal-difference-0 ((x − y) = 0) = (y ≮ x)

Theorem: top-bit-off-implies-smaller (bitvp (a) ∧ (a ≠ btm) ∧ (¬ bitn (a, size (a)))) → (bv-to-nat (a) < (exp (2, size (a)) − 1))

Theorem: tc-minus-bv-to-tc (bitvp (a) ∧ (a ≠ btm)) → (tc-minus (bv-to-tc (a))

= if bv-to-tc (a) = 0 then 0 else add (1, bv-to-tc (compl (a))) endif)

Definition: tc-fix (x) = if tcp (x) then x

else 0 endif

Theorem: tcp-add (tcp (x) → tcp (add (x, y))) ∧ (tcp (y) → tcp (add (x, y)))

Theorem: add-0 add (0, x) = tc-fix (x)

Theorem: add-1-1 add (1, add (-1, x)) = tc-fix (x)

Theorem: bv-to-tc-compl-0 (bitvp (a) ∧ (a ≠ btm) ∧ (bv-to-tc (a) = 0)) → (bv-to-tc (compl (a)) = -1)

Theorem: tc-minus-add-carry (bitvp (a) ∧ (a ≠ btm)) → (tc-minus (add (bv-to-tc (a), carry (c)))

= add (bv-to-tc (compl (a)), carry (¬ c)))

Theorem: boolp-b-not boolp (b-not (x))

Theorem: compl-not-btm (compl (a) = btm) = ((¬ bitvp (a)) ∨ (a = btm))

Theorem: tc-interpretation-of-bv-subtracter-output (bitvp (a) ∧ bitvp (b) ∧ (a ≠ btm) ∧ (b ≠ btm) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-to-tc (bv-subtracter-output (c, a, b))

= if tc-in-rangep (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a), carry (c)))), size (a))

then add (bv-to-tc (b), tc-minus (add (bv-to-tc (a), carry (c)))) elseif negativep (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a), carry (c)))))

then add (bv-to-tc (b), add (exp (2, size (a)),

tc-minus (add (bv-to-tc (a), carry (c)))))

else add (bv-to-tc (b),

add (− exp (2, size (a)), tc-minus (add (bv-to-tc (a), carry (c))))) endif)

Event: Disable tc-interpretation-of-bv-subtracter-output.

Theorem: tc-bv-subtracter-output-seen-as-bit-vector-lemma1 (bitvp (a) ∧ bitvp (b) ∧ (a ≠ btm) ∧ (b ≠ btm) ∧ (size (a) = size (b)) ∧ boolp (c)) → (tc-to-bv (bv-to-tc (bv-subtracter-output (c, a, b)),

size (bv-subtracter-output (c, a, b)))

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a),

carry (c)))),

size (a))

then add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a), carry (c))))

elseif negativep (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a),

carry (c)))))

then add (bv-to-tc (b),

add (exp (2, size (a)),

tc-minus (add (bv-to-tc (a), carry (c)))))

else add (bv-to-tc (b),

add (− exp (2, size (a)),

tc-minus (add (bv-to-tc (a), carry (c))))) endif,

size (a)))

Event: Disable tc-bv-subtracter-output-seen-as-bit-vector-lemma1.

Theorem: tc-bv-subtracter-output-seen-as-bit-vector (bitvp (a) ∧ bitvp (b) ∧ (a ≠ btm) ∧ (b ≠ btm) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-subtracter-output (c, a, b)

= if tc-in-rangep (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a), carry (c)))), size (a))

then tc-to-bv (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a), carry (c)))), size (a)) elseif negativep (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a), carry (c)))))

then tc-to-bv (add (bv-to-tc (b),

add (exp (2, size (a)),

tc-minus (add (bv-to-tc (a), carry (c))))),

size (a))

else tc-to-bv (add (bv-to-tc (b),

add (− exp (2, size (a)),

tc-minus (add (bv-to-tc (a), carry (c))))),

size (a)) endif)

Event: Disable tc-bv-subtracter-output-seen-as-bit-vector.

Theorem: tc-interpretation-of-bv-subtracter-overflowp (bitvp (a) ∧ bitvp (b) ∧ (a ≠ btm) ∧ (b ≠ btm) ∧ (size (a) = size (b)) ∧ boolp (c)) → (bv-subtracter-overflowp (c, a, b)

= (¬ tc-in-rangep (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a), carry (c)))), size (a))))

Event: Disable tc-interpretation-of-bv-subtracter-overflowp.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Definitions and lemmas for shift and rotate functions             ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: v-append (a, b) = if bitvp (a) then if a = btm then b

else bitv (bit (a), v-append (vec (a), b)) endif else b endif

Definition: v-lsr (a) = if bitvp (a)

then if a = btm then btm

else v-append (vec (a), bitv (f, btm)) endif else btm endif

Definition: v-lsl (a) = if bitvp (a)

then if a = btm then btm

else v-append (bitv (f, btm), trunc (a, size (a) − 1)) endif else btm endif

Definition: v-asr (a) = if bitvp (a)

then if a = btm then btm

else v-append (vec (a), bitv (bitn (a, size (a)), btm)) endif else btm endif

Definition: v-asl (a) = v-lsl (a)

Definition: v-ror (a, c) = if bitvp (a)

then if a = btm then btm

else v-append (vec (a), bitv (c, btm)) endif else btm endif

Definition: v-rol (a, c) = if bitvp (a)

then if a = btm then btm

else v-append (bitv (c, btm), trunc (a, size (a) − 1)) endif else btm endif

Definition: bv-append (a, b) = v-append (a, b)

Definition: bv-lsr (a) = v-lsr (a)

Definition: bv-asr (a) = v-asr (a)

Definition: bv-ror (a, c) = v-ror (a, c)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Natural and two's complement interpretation of shifters           ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: bv-to-nat-v-append bv-to-nat (v-append (a, b)) = (bv-to-nat (a) + (bv-to-nat (b) ∗ exp (2, size (a))))

Theorem: bv-lsr-divides-by-two-lemma v-lsr (a) = nat-to-bv (bv-to-nat (a) ÷ 2, size (a))

Definition: mod2 (x) = if negativep (x) then − ((1 + negative-guts (x)) ÷ 2)

else x ÷ 2 endif

Theorem: bitvp-v-append bitvp (v-append (a, b)) = if bitvp (a) then (a ≠ btm) ∨ bitvp (b)

else bitvp (b) endif

Theorem: bitn-v-append bitn (v-append (a, b), n) = if size (a) < n then bitn (b, n − size (a))

else bitn (a, n) endif

Theorem: size-v-append size (v-append (a, b)) = (size (a) + size (b))

Theorem: difference-x-x-1 (x − (x − 1)) = if x ≃ 0 then 0

else 1 endif

Theorem: bv-to-nat-of-twos-compl bv-to-nat (incr (t, compl (a))) = if bv-to-nat (a) = 0 then 0

else exp (2, size (a)) − bv-to-nat (a) endif

Theorem: difference-2x-x ((2 ∗ y) − (x + y)) = (y − x)

Theorem: quotient-crock1 ((1 + ((2 ∗ y) − (2 ∗ x))) ÷ 2) = (y − x)

Theorem: add1-difference-sub1 (1 + ((x − 1) − y)) = if y < x then x − y

else 1 endif

Theorem: quotient-crock2 (((2 ∗ y) − (2 ∗ x)) ÷ 2) = (y − x)

Theorem: bv-asr-divides-by-two bv-to-tc (bv-asr (a)) = mod2 (bv-to-tc (a))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            Definitions and lemmas about hardware if                          ;;
;;            and constructor for ALU result                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: b-if (c, a, b) = b-nand (b-nand (c, a), b-nand (b-not (c), b))

Definition: bv-if (c, a, b) = if bitvp (a)

then if a = btm then btm

else bitv (b-if (c, bit (a), bit (b)), bv-if (c, vec (a), vec (b))) endif else btm endif

Theorem: bv-if-works bv-if (c, a, b) = if c

then if bitvp (a) then a else btm endif else trunc (b, size (a)) endif

Event: Add the shell bv-cv, with recognizer function symbol bv-cvp and 3 accessors: bv, with type restriction (one-of bitvp) and default value btm; c, with type restriction (one-of truep falsep) and default value false; v, with type restriction (one-of truep falsep) and default value false.

Definition: bv-cv-if (c, a, b) = bv-cv (bv-if (c, bv (a), bv (b)), b-if (c, c (a), c (b)), b-if (c, v (a), v (b)))

Theorem: trunc-size (bitvp (b) ∧ (size (b) = size (a))) → (trunc (b, size (a)) = b)

Theorem: bv-cv-if-works (bv-cvp (a) ∧ bv-cvp (b) ∧ (size (bv (a)) = size (bv (b)))) → ((bv-cv-if (t, a, b) = a) ∧ (bv-cv-if (f, a, b) = b))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            SIZE lemmas                                                       ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: size-bv-bv-cv-if size (bv (bv-cv-if (c, a, b))) = size (bv (a))

; We rewrite "bv-not" to "v-not", etc., and so we need these size lemmas about
; the v-functions.

Theorem: size-v-not size (v-not (a)) = size (a)

Theorem: size-v-and size (v-and (a, b)) = size (a)

Theorem: size-v-or size (v-or (a, b)) = size (a)

Theorem: size-v-xor size (v-xor (a, b)) = size (a)

Theorem: size-v-append-1 size (if bitvp (a)

then if a = btm then btm

else v-append (vec (a), bitv (x, btm)) endif else btm endif)

= size (a)

Theorem: size-v-append-2 size (v-append (vec (a), bitv (x, btm))) = if bitvp (a)

then if a = btm then 1 else size (a) endif

else 1 endif

;  We have already proved (SIZE (BV-ADDER-OUTPUT C A B)) = (SIZE A) and
;                         (SIZE (BV-SUBTRACTER-OUTPUT C A B)) = (SIZE A).

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            ALU definition                                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Event: Disable bv-cv-if.

Definition: bv-alu-cv (a, b, c, op-code) = bv-cv-if (bitn (op-code, 4),

bv-cv-if (bitn (op-code, 3),

bv-cv-if (bitn (op-code, 2),

bv-cv-if (bitn (op-code, 1), bv-cv (a, f, f), bv-cv (bv-not (a), f, f)),

bv-cv-if (bitn (op-code, 1), bv-cv (bv-and (a, b), f, f), bv-cv (bv-or (a, b), f, f))),

bv-cv-if (bitn (op-code, 2),

bv-cv-if (bitn (op-code, 1), bv-cv (bv-xor (a, b), f, f), bv-cv (bv-lsr (a), bitn (a, 1), f)),

bv-cv-if (bitn (op-code, 1), bv-cv (bv-asr (a), bitn (a, 1), f), bv-cv (bv-ror (a, c),

if size (a) ≃ 0 then c else bitn (a, 1) endif, f)))),

bv-cv-if (bitn (op-code, 3),

bv-cv-if (bitn (op-code, 2),

bv-cv-if (bitn (op-code, 1),

bv-cv (bv-subtracter-output (f, a, b),

bv-subtracter-carry-out (f, a, b),

bv-subtracter-overflowp (f, a, b)),

bv-cv (bv-subtracter-output (c, a, b), bv-subtracter-carry-out (c, a, b),

bv-subtracter-overflowp (c, a, b))),

bv-cv-if (bitn (op-code, 1),

bv-cv (bv-subtracter-output (t,

nat-to-bv (0,

size (a)),

a),

bv-subtracter-carry-out (t,

nat-to-bv (0,

size (a)),

a),

bv-subtracter-overflowp (t,

nat-to-bv (0,

size (a)),

a)),

bv-cv (bv-subtracter-output (f, a, nat-to-bv (0,

size (a))),

bv-subtracter-carry-out (f, a, nat-to-bv (0,

size (a))),

bv-subtracter-overflowp (f, a, nat-to-bv (0,

size (a)))))),

bv-cv-if (bitn (op-code, 2),

bv-cv-if (bitn (op-code, 1),

bv-cv (bv-adder-output (f, a, b), bv-adder-carry-out (f, a, b), bv-adder-overflowp (f, a, b)),

bv-cv (bv-adder-output (c, a, b), bv-adder-carry-out (c, a, b), bv-adder-overflowp (c, a, b))),

bv-cv-if (bitn (op-code, 1),

bv-cv (bv-adder-output (t, a, nat-to-bv (0,

size (a))),

bv-adder-carry-out (t, a, nat-to-bv (0,

size (a))),

bv-adder-overflowp (t, a, nat-to-bv (0,

size (a)))),

bv-cv (a, f, f)))))

Theorem: v-not-is-compl v-not (a) = compl (a)

Theorem: bv-and-is-v-and bv-and (a, b) = v-and (a, b)

Theorem: bv-or-is-v-or bv-or (a, b) = v-or (a, b)

Theorem: bv-xor-is-v-xor bv-xor (a, b) = v-xor (a, b)

Theorem: bv-cv-if-reduce bv-cv-if (c, bv-cv (x, y, z), bv-cv (x, y, z)) = bv-cv (x, y, z)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           BV-ALU with theorem-prover "ifs".  This was done to speed the      ;;
;;           rewriting when proving the large lemmas that follow.               ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: bv-alu-cv-with-ifs (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b))) → (bv-alu-cv (a, b, c, op-code)

= if bitn (op-code, 4)

then if bitn (op-code, 3)

then if bitn (op-code, 2)

then if bitn (op-code, 1) then bv-cv (a, f, f) else bv-cv (bv-not (a), f, f) endif

elseif bitn (op-code, 1) then bv-cv (bv-and (a, b), f, f) else bv-cv (bv-or (a, b), f, f) endif

elseif bitn (op-code, 2)

then if bitn (op-code, 1) then bv-cv (bv-xor (a, b), f, f)

else bv-cv (bv-lsr (a), bitn (a, 1), f) endif elseif bitn (op-code, 1) then bv-cv (bv-asr (a), bitn (a, 1), f) else bv-cv (bv-ror (a, c),

if size (a) ≃ 0 then c else bitn (a, 1) endif,

f) endif

elseif bitn (op-code, 3) then if bitn (op-code, 2)

then if bitn (op-code, 1)

then bv-cv (bv-subtracter-output (f, a, b), bv-subtracter-carry-out (f, a, b), bv-subtracter-overflowp (f, a, b))

else bv-cv (bv-subtracter-output (c, a, b), bv-subtracter-carry-out (c, a, b), bv-subtracter-overflowp (c, a, b)) endif

elseif bitn (op-code, 1) then bv-cv (bv-subtracter-output (t,

nat-to-bv (0, size (a)), a),

bv-subtracter-carry-out (t, nat-to-bv (0, size (a)), a),

bv-subtracter-overflowp (t, nat-to-bv (0, size (a)), a))

else bv-cv (bv-subtracter-output (f, a, nat-to-bv (0,

size (a))),

bv-subtracter-carry-out (f, a, nat-to-bv (0,

size (a))),

bv-subtracter-overflowp (f, a, nat-to-bv (0,

size (a)))) endif

elseif bitn (op-code, 2) then if bitn (op-code, 1)

then bv-cv (bv-adder-output (f, a, b), bv-adder-carry-out (f, a, b), bv-adder-overflowp (f, a, b))

else bv-cv (bv-adder-output (c, a, b), bv-adder-carry-out (c, a, b), bv-adder-overflowp (c, a, b)) endif

elseif bitn (op-code, 1)

then bv-cv (bv-adder-output (t, a, nat-to-bv (0, size (a))), bv-adder-carry-out (t, a, nat-to-bv (0, size (a))), bv-adder-overflowp (t, a, nat-to-bv (0, size (a))))

else bv-cv (a, f, f) endif)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Boolean ALU help lemmas                                            ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: nat-to-bv-of-2i boolp (c) → (nat-to-bv (carry (c) + (i + i), n)

= if n ≃ 0 then btm else bitv (c, nat-to-bv (i, n − 1)) endif)

Theorem: nat-to-bv-to-nat-wrong-size nat-to-bv (bv-to-nat (a), n) = trunc (a, n)

Theorem: nat-to-bv-ignores-remainder nat-to-bv (i mod exp (2, n), n) = nat-to-bv (i, n)

Event: Disable nat-to-bv-ignores-remainder.

Theorem: bv-adder-as-shifter (bitvp (a) ∧ boolp (c)) → (bv-adder (c, a, a)

= nat-to-bv (bv-to-nat (a) + bv-to-nat (a) + carry (c), 1 + size (a)))

Theorem: bv-adder-output-used-as-asl (bitvp (a) ∧ boolp (c)) → (bv-adder-output (c, a, a)

= if a = btm then btm else bitv (c, trunc (a, size (a) − 1)) endif)

Event: Disable bv-adder-output-used-as-asl.

Theorem: bitn-equiv-lessp bitvp (a) → (bitn (a, size (a)) = (bv-to-nat (a) ≮ exp (2, size (a) − 1)))

Theorem: bv-adder-carry-out-used-as-asl (bitvp (a) ∧ boolp (c)) → (bv-adder-carry-out (c, a, a)

= if size (a) ≃ 0 then c else bitn (a, size (a)) endif)

Event: Disable bv-adder-carry-out-used-as-asl.

Event: Disable bv-adder-as-shifter.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Boolean operation of ALU                                           ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: bv-alu-cv-correct-boolean (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b)) ∧ boolp (c)) → ((bv-alu-cv (a, b, c, nat-to-bv (15, 4)) = bv-cv (a, f, f))

∧ (bv-alu-cv (a, b, c, nat-to-bv (14, 4)) = bv-cv (v-not (a), f, f)) ∧ (bv-alu-cv (a, b, c, nat-to-bv (13, 4)) = bv-cv (v-and (a, b), f, f)) ∧ (bv-alu-cv (a, b, c, nat-to-bv (12, 4)) = bv-cv (v-or (a, b), f, f)) ∧ (bv-alu-cv (a, b, c, nat-to-bv (11, 4)) = bv-cv (v-xor (a, b), f, f)) ∧ (bv-alu-cv (a, b, c, nat-to-bv (10, 4)) = bv-cv (v-lsr (a), bitn (a, 1), f)) ∧ (bv-alu-cv (a, b, c, nat-to-bv (9, 4)) = bv-cv (v-asr (a), bitn (a, 1), f)) ∧ (bv-alu-cv (a, b, c, nat-to-bv (8, 4))

= bv-cv (v-ror (a, c), if size (a) ≃ 0 then c else bitn (a, 1) endif, f))

∧ ((a = b)

→ ((bv (bv-alu-cv (a, b, c, nat-to-bv (3, 4))) = v-lsl (a)) ∧ (c (bv-alu-cv (a, b, c, nat-to-bv (3, 4)))

= bitn (a, size (a)))))

∧ ((a = b)

→ ((bv (bv-alu-cv (a, b, c, nat-to-bv (3, 4))) = v-asl (a)) ∧ (c (bv-alu-cv (a, b, c, nat-to-bv (3, 4)))

= bitn (a, size (a)))))

∧ ((a = b)

→ ((bv (bv-alu-cv (a, b, c, nat-to-bv (2, 4))) = v-rol (a, c))

∧ (c (bv-alu-cv (a, b, c, nat-to-bv (2, 4)))

= if size (a) ≃ 0 then c else bitn (a, size (a)) endif))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Natural number ALU help lemmas                                     ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: v-append-quotient (bitvp (a) ∧ (a ≠ btm)) → (nat-to-bv (bv-to-nat (a) ÷ 2, size (a))

= v-append (vec (a), bitv (f, btm)))

Theorem: bit-interpretation-of-even-and-odd ((bv-to-nat (a) mod 2) = 0) = (¬ bit (a))

Theorem: nat-to-bv-to-nat-hidden-to-accomodate-hands-off (x − bv-to-nat (nat-to-bv (0, n))) = fix (x)

Theorem: zero-not-less-than-anything (bv-to-nat (a) − 1) ≮ bv-to-nat (nat-to-bv (0, size (a)))

Theorem: nat-interpretation-of-inc-bit-vector bitvp (a) → (bv-adder-output (t, a, nat-to-bv (0, size (a)))

= if (1 + bv-to-nat (a)) < exp (2, size (a)) then nat-to-bv (1 + bv-to-nat (a), size (a)) else nat-to-bv (0, size (a)) endif)

Event: Disable nat-interpretation-of-inc-bit-vector.

Theorem: nat-interpretation-of-inc-carry-out bitvp (a) → (bv-adder-carry-out (t, a, nat-to-bv (0, size (a)))

= ((1 + bv-to-nat (a)) ≮ exp (2, size (a))))

Event: Disable nat-interpretation-of-inc-carry-out.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Natural number operation of ALU                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: bv-alu-cv-correct-natural-number (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b)) ∧ boolp (c)) → ((bv-alu-cv (a, b, c, nat-to-bv (10, 4))

= bv-cv (nat-to-bv (bv-to-nat (a) ÷ 2, size (a)), (bv-to-nat (a) mod 2) ≄ 0, f))

∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (7, 4)))

= if bv-to-nat (b) ≮ bv-to-nat (a)

then nat-to-bv (bv-to-nat (b) − bv-to-nat (a), size (a)) else nat-to-bv (exp (2, size (a))

− (bv-to-nat (a)

− bv-to-nat (b)), size (a)) endif)

∧ (c (bv-alu-cv (a, b, c, nat-to-bv (7, 4)))

= (bv-to-nat (b) < bv-to-nat (a))) ∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (6, 4)))

= if bv-to-nat (b) ≮ (bv-to-nat (a) + carry (c))

then nat-to-bv (bv-to-nat (b)

− (bv-to-nat (a) + carry (c)), size (a))

else nat-to-bv (exp (2, size (a))

− ((bv-to-nat (a) + carry (c)) − bv-to-nat (b)),

size (a)) endif)

∧ (c (bv-alu-cv (a, b, c, nat-to-bv (6, 4)))

= (bv-to-nat (b) < (bv-to-nat (a) + carry (c)))) ∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (5, 4)))

= if bv-to-nat (a) ≃ 0 then nat-to-bv (exp (2, size (a)) − 1, size (a)) else nat-to-bv (bv-to-nat (a) − 1, size (a)) endif)

∧ (c (bv-alu-cv (a, b, c, nat-to-bv (5, 4))) = (bv-to-nat (a) ≃ 0)) ∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (3, 4)))

= if (bv-to-nat (a) + bv-to-nat (b)) < exp (2, size (a))

then nat-to-bv (bv-to-nat (a) + bv-to-nat (b), size (a)) else nat-to-bv ((bv-to-nat (a) + bv-to-nat (b))

mod exp (2, size (a)), size (a)) endif)

∧ (c (bv-alu-cv (a, b, c, nat-to-bv (3, 4)))

= ((bv-to-nat (a) + bv-to-nat (b)) ≮ exp (2, size (a)))) ∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (2, 4)))

= if (bv-to-nat (a) + bv-to-nat (b) + carry (c))

< exp (2, size (a)) then nat-to-bv (bv-to-nat (a)

+ bv-to-nat (b) + carry (c), size (a))

else nat-to-bv ((bv-to-nat (a)

+ bv-to-nat (b) + carry (c)) mod exp (2, size (a)), size (a)) endif)

∧ (c (bv-alu-cv (a, b, c, nat-to-bv (2, 4)))

= ((bv-to-nat (a) + bv-to-nat (b) + carry (c))

≮ exp (2, size (a)))) ∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (1, 4)))

= if (1 + bv-to-nat (a)) < exp (2, size (a))

then nat-to-bv (1 + bv-to-nat (a), size (a))

else nat-to-bv (0, size (a)) endif)

∧ (c (bv-alu-cv (a, b, c, nat-to-bv (1, 4))) = ((1 + bv-to-nat (a)) ≮ exp (2, size (a)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Two's complement ALU help lemmas                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: twos-complement-twos-complement bitvp (a) → (incr (t, compl (incr (t, compl (a)))) = a)

Theorem: tc-to-bv-to-tc-negative (bitvp (a) ∧ (size (a) = n)) → (tc-to-bv (bv-to-tc (a), n) = a)

Theorem: v-asr-is-a-bitv bitvp (v-asr (a))

Theorem: size-of-v-asr size (v-asr (a)) = size (a)

Theorem: bv-asr-divides-by-two-bridge bitvp (a) → (tc-to-bv (mod2 (bv-to-tc (a)), size (a)) = bv-asr (a))

Theorem: bv-to-tc-to-bv-of-zero-is-zero bv-to-tc (tc-to-bv (0, n)) = 0

Theorem: tc-to-bv-is-not-btm-for-non-zero-size (n ≄ 0) → ((tc-to-bv (0, n) = btm) = f)

Theorem: nat-of-zero-is-tc-of-zero nat-to-bv (0, size) = tc-to-bv (0, size)

Theorem: tc-fix-of-add tc-fix (add (a, b)) = add (tc-fix (a), b)

Theorem: tc-to-bv-of-bitv-not-btm ((a ≠ btm) ∧ bitvp (a)) → (tc-to-bv (0, size (a)) ≠ btm)

Theorem: tc-interpretation-of-inc-bit-vector (bitvp (a) ∧ (a ≠ btm)) → (bv-adder-output (t, a, nat-to-bv (0, size (a)))

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (a), 1), size (a)) then add (bv-to-tc (a), 1) elseif negativep (add (bv-to-tc (a), 1)) then add (bv-to-tc (a), add (1, exp (2, size (a)))) else add (bv-to-tc (a),

add (1, − exp (2, size (a)))) endif,

size (a)))

Event: Disable tc-interpretation-of-inc-bit-vector.

Theorem: tc-interpretation-of-dec-bit-vector (bitvp (a) ∧ (a ≠ btm)) → (bv-subtracter-output (t, nat-to-bv (0, size (a)), a)

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (a), -1), size (a)) then add (bv-to-tc (a), -1) elseif negativep (add (bv-to-tc (a), -1)) then add (bv-to-tc (a), add (-1, exp (2, size (a)))) else add (bv-to-tc (a),

add (-1, − exp (2, size (a)))) endif,

size (a)))

Event: Disable tc-interpretation-of-dec-bit-vector.

Theorem: tc-interpretation-of-inc-overflowp (bitvp (a) ∧ (a ≠ btm)) → (bv-adder-overflowp (t, a, nat-to-bv (0, size (a)))

= (¬ tc-in-rangep (add (bv-to-tc (a), 1), size (a))))

Event: Disable tc-interpretation-of-inc-overflowp.

Theorem: tc-interpretation-of-dec-overflowp (bitvp (a) ∧ (a ≠ btm)) → (bv-subtracter-overflowp (t, nat-to-bv (0, size (a)), a)

= (¬ tc-in-rangep (add (bv-to-tc (a), -1), size (a))))

Event: Disable tc-interpretation-of-dec-overflowp.

Theorem: tc-interpretation-of-negation-output (bitvp (a) ∧ (a ≠ btm)) → (bv-subtracter-output (f, a, nat-to-bv (0, size (a)))

= tc-to-bv (if tc-in-rangep (tc-minus (bv-to-tc (a)), size (a)) then tc-minus (bv-to-tc (a)) elseif negativep (tc-minus (bv-to-tc (a))) then add (exp (2, size (a)), tc-minus (bv-to-tc (a))) else add (− exp (2, size (a)),

tc-minus (bv-to-tc (a))) endif,

size (a)))

Event: Disable tc-interpretation-of-negation-output.

Theorem: tc-interpretation-of-negation-overflowp (bitvp (a) ∧ (a ≠ btm)) → (bv-subtracter-overflowp (f, a, nat-to-bv (0, size (a)))

= (¬ tc-in-rangep (tc-minus (bv-to-tc (a)), size (a))))

Event: Disable tc-interpretation-of-negation-overflowp.

Event: Disable nat-of-zero-is-tc-of-zero.

Event: Disable tc-fix-of-add.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;           Two's complement operation of ALU                                  ;;
;;                                                                              ;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: alu-correct-twos-complement (bitvp (a) ∧ (a ≠ btm) ∧ bitvp (b) ∧ (b ≠ btm) ∧ (size (a) = size (b)) ∧ boolp (c)) → ((bv (bv-alu-cv (a, b, c, nat-to-bv (9, 4)))

= tc-to-bv (mod2 (bv-to-tc (a)), size (a))) ∧ (v (bv-alu-cv (a, b, c, nat-to-bv (9, 4))) = f) ∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (7, 4)))

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (b),

tc-minus (bv-to-tc (a))), size (a))

then add (bv-to-tc (b), tc-minus (bv-to-tc (a))) elseif negativep (add (bv-to-tc (b),

tc-minus (bv-to-tc (a))))

then add (bv-to-tc (b),

add (exp (2, size (a)),

tc-minus (bv-to-tc (a))))

else add (bv-to-tc (b),

add (− exp (2, size (a)),

tc-minus (bv-to-tc (a)))) endif,

size (a)))

∧ (v (bv-alu-cv (a, b, c, nat-to-bv (7, 4)))

= (¬ tc-in-rangep (add (bv-to-tc (b),

tc-minus (bv-to-tc (a))), size (a))))

∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (6, 4)))

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a),

carry (c)))),

size (a))

then add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a), carry (c))))

elseif negativep (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a),

carry (c)))))

then add (bv-to-tc (b), add (exp (2, size (a)), tc-minus (add (bv-to-tc (a),

carry (c)))))

else add (bv-to-tc (b),

add (− exp (2, size (a)),

tc-minus (add (bv-to-tc (a),

carry (c))))) endif,

size (a)))

∧ (v (bv-alu-cv (a, b, c, nat-to-bv (6, 4)))

= (¬ tc-in-rangep (add (bv-to-tc (b),

tc-minus (add (bv-to-tc (a),

carry (c)))),

size (a))))

∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (5, 4)))

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (a), -1), size (a)) then add (bv-to-tc (a), -1) elseif negativep (add (bv-to-tc (a), -1)) then add (bv-to-tc (a), add (-1, exp (2, size (a)))) else add (bv-to-tc (a),

add (-1, − exp (2, size (a)))) endif,

size (a)))

∧ (v (bv-alu-cv (a, b, c, nat-to-bv (5, 4)))

= (¬ tc-in-rangep (add (bv-to-tc (a), -1), size (a)))) ∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (4, 4)))

= tc-to-bv (if tc-in-rangep (tc-minus (bv-to-tc (a)),

size (a))

then tc-minus (bv-to-tc (a)) elseif negativep (tc-minus (bv-to-tc (a))) then add (exp (2, size (a)),

tc-minus (bv-to-tc (a)))

else add (− exp (2, size (a)),

tc-minus (bv-to-tc (a))) endif,

size (a)))

∧ (v (bv-alu-cv (a, b, c, nat-to-bv (4, 4)))

= (¬ tc-in-rangep (tc-minus (bv-to-tc (a)), size (a)))) ∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (3, 4)))

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (a), bv-to-tc (b)),

size (a))

then add (bv-to-tc (a), bv-to-tc (b)) elseif negativep (add (bv-to-tc (a), bv-to-tc (b))) then add (bv-to-tc (a),

add (bv-to-tc (b), exp (2, size (a))))

else add (bv-to-tc (a),

add (bv-to-tc (b), − exp (2, size (a)))) endif,

size (a)))

∧ (v (bv-alu-cv (a, b, c, nat-to-bv (3, 4)))

= (¬ tc-in-rangep (add (bv-to-tc (a), bv-to-tc (b)),

size (a))))

∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (2, 4)))

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (a),

add (bv-to-tc (b), carry (c))), size (a))

then add (bv-to-tc (a),

add (bv-to-tc (b), carry (c)))

elseif negativep (add (bv-to-tc (a),

add (bv-to-tc (b), carry (c))))

then add (bv-to-tc (a),

add (bv-to-tc (b),

add (carry (c), exp (2, size (a)))))

else add (bv-to-tc (a),

add (bv-to-tc (b),

add (carry (c),

− exp (2, size (a))))) endif,

size (a)))

∧ (v (bv-alu-cv (a, b, c, nat-to-bv (2, 4)))

= (¬ tc-in-rangep (add (bv-to-tc (a),

add (bv-to-tc (b), carry (c))), size (a))))

∧ (bv (bv-alu-cv (a, b, c, nat-to-bv (1, 4)))

= tc-to-bv (if tc-in-rangep (add (bv-to-tc (a), 1), size (a)) then add (bv-to-tc (a), 1) elseif negativep (add (bv-to-tc (a), 1)) then add (bv-to-tc (a), add (1, exp (2, size (a)))) else add (bv-to-tc (a),

add (1, − exp (2, size (a)))) endif,

size (a)))

∧ (v (bv-alu-cv (a, b, c, nat-to-bv (1, 4))) = (¬ tc-in-rangep (add (bv-to-tc (a), 1), size (a)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          This file contains definitions and lemmas concerning the            ;;
;;          hardware necessary to build "big-machine".                          ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Miscellaneous lemmas                                                ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: size-bv-bv-alu-cv size (bv (bv-alu-cv (a, b, c, op-code))) = size (a)

Event: Disable bv-alu-cv.

Event: Disable bv-alu-cv-with-ifs.

Definition: fix-bool (x) = if x then t

else f endif

Definition: properp (x) = if x ≃ nil then x = nil

else properp (cdr (x)) endif

Definition: append (x, y) = if x ≃ nil then y

else cons (car (x), append (cdr (x), y)) endif

Theorem: assoc-of-append append (append (a, b), c) = append (a, append (b, c))

Theorem: length-0 (length (x) = 0) = (x ≃ nil)

Definition: v-nat-dec (a) = if bv-to-nat (a) ≃ 0 then nat-to-bv (exp (2, size (a)) − 1, size (a))

else nat-to-bv (bv-to-nat (a) − 1, size (a)) endif

; around is received.

Definition: v-nat-inc (a) = nat-to-bv (1 + bv-to-nat (a), size (a))

Theorem: size-v-nat-dec size (v-nat-dec (x)) = size (x)

Theorem: size-v-nat-inc size (v-nat-inc (x)) = size (x)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Memory accessors                                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: nth (n, lst) = if n ≃ 0 then car (lst)

else nth (n − 1, cdr (lst)) endif

Definition: v-nth (v-n, lst) = nth (bv-to-nat (v-n), lst)

Definition: update-v (c, cell, value) = if truep (c) then value

else cell endif

Definition: update-nth (c, n, lst, value) = if truep (c) ∧ listp (lst)

then if n ≃ 0 then cons (value, cdr (lst))

else cons (car (lst), update-nth (c, n − 1, cdr (lst), value)) endif else lst endif

Definition: update-v-nth (c, v-n, lst, value) = update-nth (c, bv-to-nat (v-n), lst, value)

Theorem: length-update-nth length (update-nth (c, n, lst, value)) = length (lst)

Theorem: length-update-v-nth length (update-v-nth (c, n, lst, value)) = length (lst)

Theorem: listp-update-nth listp (update-nth (c, n, lst, value)) = listp (lst)

Theorem: listp-update-v-nth listp (update-v-nth (c, n, lst, value)) = listp (lst)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Zero and Negative flag interpretation lemmas                        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: b-bv-nzerop (a) = if bitvp (a)

then if a = btm then f

else b-or (bit (a), b-bv-nzerop (vec (a))) endif else f endif

Definition: b-bv-zerop (a) = b-not (b-bv-nzerop (a))

Definition: v-zerop (a) = if bitvp (a)

then if a = btm then t

else (bit (a) = f) ∧ v-zerop (vec (a)) endif else t endif

Theorem: b-bv-zerop-equal-v-zerop b-bv-zerop (a) = v-zerop (a)

;  The following are the natural number and tc intepretation lemmas for
;  the zero flag.

Theorem: v-zerop-equal-bv-to-nat-zero v-zerop (a) = (bv-to-nat (a) ≃ 0)

Theorem: v-zerop-equal-bv-to-tc-zero v-zerop (a) = (0 = bv-to-tc (a))

Event: Disable v-zerop-equal-bv-to-nat-zero.

Event: Disable v-zerop-equal-bv-to-tc-zero.

;  The following is the tc interpretation lemma for the negative flag.

Theorem: n-flag-equals-negativep bitn (a, size (a)) = negativep (bv-to-tc (a))

Event: Disable n-flag-equals-negativep.

Definition: bv-equal (a, b) = if bitvp (a)

then if a = btm then t

else b-and (b-equv (bit (a), bit (b)), bv-equal (vec (a), vec (b))) endif else f endif

Theorem: bv-equal-is-equal (bitvp (a) ∧ bitvp (b) ∧ (size (a) = size (b))) → (bv-equal (a, b) = (a = b))

Event: Disable bv-equal-is-equal.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Assumptions made about the various registers                        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: nxsz = 4

; width of micro address reg

Definition: machine-size = 16

; Word width of micro-processor

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Register, RAMP, and ROMP recognizer                                 ;;
;;                                                                              ;;
;;          A ram and rom checker are presented below and is used to ensure     ;;
;;          that RAM and ROM (constant function) have certain properties.       ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: sizep (register, width) = (size (register) = width)

Definition: every-member-sizep (lst, n) = if lst ≃ nil then t

else sizep (car (lst), n) ∧ every-member-sizep (cdr (lst), n) endif

Definition: ramp (ram, width, locations) = ((length (ram) = locations) ∧ every-member-sizep (ram, width))

Definition: romp (rom, width, locations) = ((length (rom) = locations) ∧ every-member-sizep (rom, width))

Theorem: every-member-sizep-implies-size-nth ((n < length (lst)) ∧ every-member-sizep (lst, width)) → (size (nth (n, lst)) = width)

Theorem: every-member-sizep-implies-size-nth-machine-size ((n < length (lst)) ∧ every-member-sizep (lst, machine-size)) → (size (nth (n, lst)) = machine-size)

Theorem: every-member-sizep-implies-size-nth-0 (every-member-sizep (lst, width) ∧ (0 < length (lst))) → (size (car (lst)) = width)

Event: Disable boolp.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Op-code accessors                                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: bv-op-code (i-reg) = bitv (bitn (i-reg, 13),

bitv (bitn (i-reg, 14), bitv (bitn (i-reg, 15), bitv (bitn (i-reg, 16), btm))))

Definition: b-move-op (i-reg) = bitn (i-reg, 12)

Definition: b-cc-set (i-reg) = bitn (i-reg, 11)

Definition: b-direct-reg-b (i-reg) = b-nor (bitn (i-reg, 9), bitn (i-reg, 10))

Definition: b-indirect-reg-b (i-reg) = b-and (bitn (i-reg, 9), b-not (bitn (i-reg, 10)))

Definition: b-indirect-reg-b-dec (i-reg) = b-and (b-not (bitn (i-reg, 9)), bitn (i-reg, 10))

Definition: b-indirect-reg-b-inc (i-reg) = b-and (bitn (i-reg, 9), bitn (i-reg, 10))

Definition: bv-oprd-b (i-reg) = bitv (bitn (i-reg, 6), bitv (bitn (i-reg, 7), bitv (bitn (i-reg, 8), btm)))

Definition: b-direct-reg-a (i-reg) = b-nor (bitn (i-reg, 4), bitn (i-reg, 5))

Definition: b-indirect-reg-a (i-reg) = b-and (bitn (i-reg, 4), b-not (bitn (i-reg, 5)))

Definition: b-indirect-reg-a-dec (i-reg) = b-and (b-not (bitn (i-reg, 4)), bitn (i-reg, 5))

Definition: b-indirect-reg-a-inc (i-reg) = b-and (bitn (i-reg, 4), bitn (i-reg, 5))

Definition: bv-oprd-a (i-reg) = bitv (bitn (i-reg, 1), bitv (bitn (i-reg, 2), bitv (bitn (i-reg, 3), btm)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Sub-functions for FM8501                                            ;;
;;                                                                              ;;
;;          NOTE:  Many definitions below are presented in pairs.  A hardware   ;;

;;                 version is presented along with a version that is more       ;;
;;                 agreeable to the theorem-prover.  The second of these        ;;
;;                 paired definitions is has a "WITH-IFS" ending.  Not all      ;;
;;                 of the hardware functions have a "WITH-IFS" pair.            ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: bv-alu-op-code (i-reg) = bv-if (b-move-op (i-reg), nat-to-bv (0, 4), bv-op-code (i-reg))

Definition: b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg) = b-or (b-or (b-not (b-move-op (i-reg)), bitn (bv-op-code (i-reg), 4)),

b-or (b-or (b-or (b-and (b-not (c-flag),

bv-equal (bv-op-code (i-reg), nat-to-bv (0, 4))), b-and (c-flag,

bv-equal (bv-op-code (i-reg), nat-to-bv (1, 4)))),

b-or (b-and (b-not (v-flag),

bv-equal (bv-op-code (i-reg), nat-to-bv (2, 4))), b-and (v-flag,

bv-equal (bv-op-code (i-reg), nat-to-bv (3, 4))))),

b-or (b-or (b-and (b-not (z-flag),

bv-equal (bv-op-code (i-reg), nat-to-bv (4, 4))), b-and (z-flag,

bv-equal (bv-op-code (i-reg), nat-to-bv (5, 4)))),

b-or (b-and (b-not (n-flag),

bv-equal (bv-op-code (i-reg), nat-to-bv (6, 4))), b-and (n-flag,

bv-equal (bv-op-code (i-reg), nat-to-bv (7, 4)))))))

Definition: b-store-alu-result-with-ifs (c-flag, v-flag, z-flag, n-flag, i-reg) = ((¬ b-move-op (i-reg))

∨ bitn (bv-op-code (i-reg), 4)

∨ (bv-op-code (i-reg)

= nat-to-bv (if c-flag then 1 else 0 endif, 4))

∨ (bv-op-code (i-reg)

= nat-to-bv (if v-flag then 3 else 2 endif, 4))

∨ (bv-op-code (i-reg)

= nat-to-bv (if z-flag then 5 else 4 endif, 4))

∨ (bv-op-code (i-reg)

= nat-to-bv (if n-flag then 7 else 6 endif, 4)))

Theorem: b-store-alu-result-ifs b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg) = b-store-alu-result-with-ifs (c-flag, v-flag, z-flag, n-flag, i-reg)

Event: Disable b-store-alu-result.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Micro-rom                                                           ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: make-micro-word (l) = if l ≃ nil then btm

elseif cdr (l) ≃ nil then nat-to-bv (car (l), nxsz)

else bitv (if car (l) = 't then t else f endif, make-micro-word (cdr (l))) endif

Definition: make-micro-rom (l) = if l ≃ nil then nil

else cons (make-micro-word (car (l)), make-micro-rom (cdr (l))) endif

Definition: micro-store

= make-micro-rom ('((f f f f f f f f f t f f f f f f 1)
                    (f t f t f t f f f t f t f f f f 2)
                    (f f f t f f f f t f f f f f f f 3)
                    (f f f f f f f f f t f f f f t f 4)
                    (f f f f t f f t f t f t f f f f 5)
                    (f f f f t f f f t f f f f f f f 6)

                    (f f f f t f f f f t t f f f f f 7)
                    (f f f f f f f t f t f t f f f f 8)
                    (f f f f f f f f t f f f f f f f 9)
                    (f f f f f f f f f t f f t f f f 10)
                    (f f f f f f f f f t f f f t f f 11)
                    (t f t f f f f f f f f f f f f t 12)
                    (f f f f t f t f f t f f f f f f 13)
                    (f f f f f f t f f t f f f f f f 1)
                    (f f f f f f f f f t f f f f f f 0)
                    (f f f f f f f f f t f f f f f f 0)))

Definition: micro-rom (addr) = v-nth (addr, micro-store)

;  Accessors for data in the ROM named "micro-store".

Definition: b-dout-incdec (x) = bitn (x, 1)

; Data out reg or address unit

Definition: b-force-inc (x) = bitn (x, 2)

; Force increment for address

Definition: b-en-no-store (x) = bitn (x, 3)

; Let "NO-STORE" effect sequencer

Definition: b-ir-mem-ref (x) = bitn (x, 4)

; Memory reference for instruction

Definition: b-oprda-oprdb (x) = bitn (x, 5)

; Select operand A or operand B

Definition: b-pc-regnum (x) = bitn (x, 6)

; Select PC or register in file

Definition: b-postinc (x) = bitn (x, 7)

; Post-increment address mode

Definition: b-predec (x) = bitn (x, 8)

; Pre-decrement address mode

Definition: b-rd (x) = bitn (x, 9)

; Read cycle

Definition: b-seq (x) = bitn (x, 10)

; Sequence micro-address register

Definition: b-we-a-reg (x) = bitn (x, 11)

; Write enable A register

Definition: b-we-addr-out (x) = bitn (x, 12)

; Write enable address-out register

Definition: b-we-b-reg (x) = bitn (x, 13)

; Write enable B register

Definition: b-we-alu-result (x) = bitn (x, 14)

; WE DATA-OUT, CC-REG, NO-STORE

Definition: b-we-ir (x) = bitn (x, 15)

; Write enable instruction register

Definition: b-wr (x) = bitn (x, 16)

; Write cycle

Definition: bv-next (x) = bitv (bitn (x, 17),

bitv (bitn (x, 18), bitv (bitn (x, 19), bitv (bitn (x, 20), btm))))

Definition: right-bv-next-size (lst) = if lst ≃ nil then t

else (size (bv-next (car (lst))) = nxsz)

∧ right-bv-next-size (cdr (lst)) endif

Theorem: size-bv-next-micro-rom-lemma size (bv-next (x)) = 4 Event: Disable micro-rom.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Hardware variable and constant assumptions for FM8501.              ;;
;;                                                                              ;;
;;      The following definition describes the assumptions about the various    ;;
;;      registers (variables) and the ROM used in the construction of the       ;;
;;      FM8501 microprocessor.                                                  ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: standard-hyps (mar,

read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem)

= (romp (micro-store, 20, exp (2, nxsz))

∧ sizep (mar, nxsz) ∧ boolp (read) ∧ boolp (write) ∧ boolp (dtack) ∧ boolp (reset) ∧ boolp (no-store) ∧ sizep (data-out, machine-size) ∧ ramp (reg-file, machine-size, 8) ∧ sizep (addr-out, machine-size) ∧ boolp (c-flag) ∧ boolp (v-flag) ∧ boolp (z-flag)

∧ boolp (n-flag)

∧ sizep (a-reg, machine-size) ∧ sizep (b-reg, machine-size) ∧ sizep (i-reg, machine-size) ∧ sizep (visual-mem, machine-size) ∧ ramp (real-mem, machine-size, exp (2, 16)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Miscellanous lemmas                                                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: every-member-sizep-implies-bitvp (every-member-sizep (lst, width) ∧ (n < length (lst)) ∧ (width ≄ 0)) → bitvp (nth (n, lst))

Theorem: every-member-sizep-implies-bitvp-machine-size (every-member-sizep (lst, machine-size) ∧ (n < length (lst))) → bitvp (nth (n, lst))

Theorem: sizep-implies-bitvp (size (a) = (1 + n)) → bitvp (a)

;  The following lemma subsumes trunc-size.

Theorem: trunc-size-bridge (bitvp (a) ∧ (n = size (a))) → (trunc (a, n) = a)

Theorem: b-if-works (boolp (c) ∧ boolp (a) ∧ boolp (b)) → (b-if (c, a, b)

= if c then a else b endif)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Functions for composing the micro-processor                         ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: bv-reg-select (i-reg, mar, reset) = bv-if (b-or (reset, b-pc-regnum (micro-rom (mar))),

nat-to-bv (0, 3),

bv-if (b-oprda-oprdb (micro-rom (mar)), bv-oprd-a (i-reg), bv-oprd-b (i-reg)))

Definition: bv-reg-select-with-ifs (i-reg, mar, reset) = if b-or (reset, b-pc-regnum (micro-rom (mar))) then nat-to-bv (0, 3)

elseif b-oprda-oprdb (micro-rom (mar)) then bv-oprd-a (i-reg)

else bv-oprd-b (i-reg) endif

Theorem: bv-reg-select-ifs bv-reg-select (i-reg, mar, reset) = bv-reg-select-with-ifs (i-reg, mar, reset)

Definition: b-oprd-mem-ref (mar, i-reg) = b-if (b-oprda-oprdb (micro-rom (mar)),

b-not (b-direct-reg-a (i-reg)), b-not (b-direct-reg-b (i-reg)))

Definition: b-oprd-mem-ref-with-ifs (mar, i-reg) = if b-oprda-oprdb (micro-rom (mar)) then b-not (b-direct-reg-a (i-reg))

else b-not (b-direct-reg-b (i-reg)) endif

Theorem: b-oprd-mem-ref-ifs b-oprd-mem-ref (mar, i-reg) = b-oprd-mem-ref-with-ifs (mar, i-reg)

Event: Disable b-oprd-mem-ref.

; This disable was not here when FM8501 proved.
;  Next micro-address

Definition: mar (mar, i-reg, dtack, reset, no-store) = update-v (b-or (b-or (reset, b-or (dtack, b-seq (micro-rom (mar)))),

b-or (b-and (b-en-no-store (micro-rom (mar)), no-store), b-and (b-not (b-oprd-mem-ref (mar, i-reg)),

b-not (b-ir-mem-ref (micro-rom (mar)))))),

mar,

bv-if (reset, nat-to-bv (0, nxsz), bv-next (micro-rom (mar))))

;  Read register

Definition: read (mar, i-reg) = b-and (b-or (b-oprd-mem-ref (mar, i-reg), b-ir-mem-ref (micro-rom (mar))),

b-rd (micro-rom (mar)))

;  Write register

Definition: write (mar, i-reg, no-store) = b-and (b-wr (micro-rom (mar)),

b-and (b-oprd-mem-ref (mar, i-reg), b-not (no-store)))

;  Data acknowledgement

Definition: dtack (current-oracle-entry) = fix-bool (car (current-oracle-entry))

;  Reset function

Definition: reset (current-oracle-entry) = fix-bool (cadr (current-oracle-entry))

;  No-store -- defines the flag which allows FM8501 to do conditional stores.

Definition: no-store (no-store, c-flag, v-flag, z-flag, n-flag, i-reg, mar) = update-v (b-we-alu-result (micro-rom (mar)),

no-store,

b-not (b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg)))

Definition: no-store-with-ifs (no-store, c-flag, v-flag, z-flag, n-flag, i-reg, mar) = if b-we-alu-result (micro-rom (mar))

then ¬ b-store-alu-result-with-ifs (c-flag, v-flag, z-flag, n-flag, i-reg)

else no-store endif Theorem: no-store-ifs no-store (no-store, c-flag, v-flag, z-flag, n-flag, i-reg, mar) = no-store-with-ifs (no-store, c-flag, v-flag, z-flag, n-flag, i-reg, mar)

Event: Disable no-store.

;  Bit-vector result of the ALU

Definition: data-out (data-out, a-reg, b-reg, c-flag, i-reg, mar) = update-v (b-we-alu-result (micro-rom (mar)),

data-out,

bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))))

Definition: data-out-with-ifs (data-out, a-reg, b-reg, c-flag, i-reg, mar) = if b-we-alu-result (micro-rom (mar))

then bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))) else data-out endif

Theorem: data-out-ifs data-out (data-out, a-reg, b-reg, c-flag, i-reg, mar) = data-out-with-ifs (data-out, a-reg, b-reg, c-flag, i-reg, mar)

Event: Disable data-out.

;  Calculates the next value of the register file.

Definition: reg-file (reg-file, data-out, i-reg, mar, no-store, reset) = update-v-nth (b-or (b-or (reset, b-force-inc (micro-rom (mar))),

b-or (b-or (b-pc-regnum (micro-rom (mar)),

b-and (b-wr (micro-rom (mar)),

b-and (b-not (no-store),

b-direct-reg-b (i-reg)))),

b-or (b-and (b-predec (micro-rom (mar)),

b-if (b-oprda-oprdb (micro-rom (mar)), b-indirect-reg-a-dec (i-reg), b-indirect-reg-b-dec (i-reg))),

b-and (b-postinc (micro-rom (mar)),

b-if (b-oprda-oprdb (micro-rom (mar)), b-indirect-reg-a-inc (i-reg),

b-indirect-reg-b-inc (i-reg)))))),

bv-reg-select (i-reg, mar, reset),

reg-file,

bv-if (b-or (b-dout-incdec (micro-rom (mar)), reset), bv-if (reset, nat-to-bv (0, machine-size), data-out), bv-if (b-or (b-force-inc (micro-rom (mar)),

b-if (b-oprda-oprdb (micro-rom (mar)), b-indirect-reg-a-inc (i-reg), b-indirect-reg-b-inc (i-reg))),

bv-adder-output (t, nat-to-bv (0, machine-size), v-nth (bv-reg-select (i-reg,

mar, reset),

reg-file)),

bv-subtracter-output (t,

nat-to-bv (0,

machine-size),

v-nth (bv-reg-select (i-reg, mar, reset),

reg-file)))))

;  Defines the output address presented by FM8501.

Definition: addr-out (addr-out, reg-file, i-reg, mar, reset) = update-v (b-we-addr-out (micro-rom (mar)),

addr-out,

bv-if (b-and (b-predec (micro-rom (mar)),

b-if (b-oprda-oprdb (micro-rom (mar)), b-indirect-reg-a-dec (i-reg), b-indirect-reg-b-dec (i-reg))),

bv-subtracter-output (t, nat-to-bv (0, machine-size), v-nth (bv-reg-select (i-reg,

mar, reset),

reg-file)),

v-nth (bv-reg-select (i-reg, mar, reset), reg-file)))

;  Carry flag

Definition: c-flag (c-flag, a-reg, b-reg, i-reg, mar) = update-v (b-and (b-we-alu-result (micro-rom (mar)), b-cc-set (i-reg)),

c-flag,

c (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))))

Definition: c-flag-with-ifs (c-flag, a-reg, b-reg, i-reg, mar) = if b-and (b-we-alu-result (micro-rom (mar)), b-cc-set (i-reg))

then c (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg)))

else c-flag endif

Theorem: c-flag-ifs c-flag (c-flag, a-reg, b-reg, i-reg, mar) = c-flag-with-ifs (c-flag, a-reg, b-reg, i-reg, mar)

Event: Disable c-flag.

;  The overflow flag

Definition: v-flag (v-flag, a-reg, b-reg, c-flag, i-reg, mar) = update-v (b-and (b-we-alu-result (micro-rom (mar)), b-cc-set (i-reg)),

v-flag,

v (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))))

Definition: v-flag-with-ifs (v-flag, a-reg, b-reg, c-flag, i-reg, mar) = if b-and (b-we-alu-result (micro-rom (mar)), b-cc-set (i-reg))

then v (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg)))

else v-flag endif

Theorem: v-flag-ifs v-flag (v-flag, a-reg, b-reg, c-flag, i-reg, mar) = v-flag-with-ifs (v-flag, a-reg, b-reg, c-flag, i-reg, mar)

Event: Disable v-flag.

;  The zero flag

Definition: z-flag (z-flag, a-reg, b-reg, c-flag, i-reg, mar)

= update-v (b-and (b-we-alu-result (micro-rom (mar)), b-cc-set (i-reg)), z-flag, b-bv-zerop (bv (bv-alu-cv (a-reg,

b-reg, c-flag, bv-alu-op-code (i-reg)))))

Definition: z-flag-with-ifs (z-flag, a-reg, b-reg, c-flag, i-reg, mar) = if b-and (b-we-alu-result (micro-rom (mar)), b-cc-set (i-reg))

then b-bv-zerop (bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg)))) else z-flag endif

Theorem: z-flag-ifs z-flag (z-flag, a-reg, b-reg, c-flag, i-reg, mar) = z-flag-with-ifs (z-flag, a-reg, b-reg, c-flag, i-reg, mar)

Event: Disable z-flag.

;  Two's complement negative flag

Definition: n-flag (n-flag, a-reg, b-reg, c-flag, i-reg, mar) = update-v (b-and (b-we-alu-result (micro-rom (mar)), b-cc-set (i-reg)),

n-flag,

bitn (bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))), machine-size))

Definition: n-flag-with-ifs (n-flag, a-reg, b-reg, c-flag, i-reg, mar) = if b-and (b-we-alu-result (micro-rom (mar)), b-cc-set (i-reg))

then bitn (bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))),

machine-size)

else n-flag endif

Theorem: n-flag-ifs n-flag (n-flag, a-reg, b-reg, c-flag, i-reg, mar) = n-flag-with-ifs (n-flag, a-reg, b-reg, c-flag, i-reg, mar)

Event: Disable n-flag.

;  Operand A for the ALU

Definition: a-reg (a-reg, visual-mem, reg-file, i-reg, mar, reset) = update-v (b-we-a-reg (micro-rom (mar)),

a-reg,

bv-if (b-direct-reg-a (i-reg), v-nth (bv-reg-select (i-reg, mar, reset), reg-file), visual-mem))

;  Operand B for the ALU

Definition: b-reg (b-reg, visual-mem, reg-file, i-reg, mar, reset) = update-v (b-we-b-reg (micro-rom (mar)),

b-reg,

bv-if (b-direct-reg-b (i-reg), v-nth (bv-reg-select (i-reg, mar, reset), reg-file), visual-mem))

;  Fills the instruction register

Definition: i-reg (i-reg, visual-mem, mar) = update-v (b-we-ir (micro-rom (mar)), i-reg, visual-mem)

Definition: i-reg-with-ifs (i-reg, visual-mem, mar) = if b-we-ir (micro-rom (mar)) then visual-mem

else i-reg endif

Theorem: i-reg-ifs i-reg (i-reg, visual-mem, mar) = i-reg-with-ifs (i-reg, visual-mem, mar)

Event: Disable i-reg.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Memory process                                                      ;;
;;                                                                              ;;
;;          The memory process is interesting as it requires history to         ;;
;;          operate.  VISUAL-MEM is the description of how a memory that        ;;
;;          FM8501 reads is expected to act.  A "correct" memory value is       ;;
;;          only returned after the READ line has been on for two clock "ticks",;;
;;          the WRITE line is off, DTACK is on, RESET is off, and DATA-OUT      ;;

;;          and ADDR-OUT have been stable for two clock "ticks".  VISUAL-MEM    ;;
;;          embodies the assumptions made about reading memory.  REAL-MEM       ;;
;;          is a function that actually updates the memory.  Its assumptions    ;;
;;          are expressed similarily as VISUAL-MEM.  The WATCH-DOG allows       ;;
;;          one tick's worth of state to be kept concerning READ, WRITE,        ;;
;;          DTACK, DATA-OUT, and ADDR-OUT.                                      ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Event: Add the shell watch-dog, with recognizer function symbol watch-dogp and 5 accessors: read-1 , with type restriction (none-of) and default value false; write-1 , with type restriction (none-of) and default value false; dtack-1-oracle, with type restriction (none-of) and default value false; data-out-1 , with type restriction (one-of bitvp) and default value btm; addr-out-1 , with type restriction (one-of bitvp) and default value btm.

Event: Introduce the function symbol default-visual-mem-value of 0 arguments.

; Default value from memory when memory
                                        ; has not been selected to return a value.

Definition: visual-mem (real-mem,

read, write, addr-out, memory-watch-dog-history, dtack-oracle, reset-oracle)

= trunc (if (read ∧ read-1 (memory-watch-dog-history))

∧ ((¬ write)

∧ (¬ write-1 (memory-watch-dog-history))) ∧ (addr-out = addr-out-1 (memory-watch-dog-history)) ∧ (dtack-oracle ∧ dtack-1-oracle (memory-watch-dog-history)) ∧ (¬ reset-oracle) then v-nth (addr-out, real-mem)

else default-visual-mem-value endif, machine-size)

Definition: real-mem (real-mem, read, write, addr-out, data-out, memory-watch-dog-history, dtack-oracle, reset-oracle)

= update-v-nth ((write ∧ write-1 (memory-watch-dog-history))

∧ ((¬ read)

∧ (¬ read-1 (memory-watch-dog-history))) ∧ (addr-out = addr-out-1 (memory-watch-dog-history)) ∧ (dtack-oracle ∧ (¬ dtack-1-oracle (memory-watch-dog-history))) ∧ (¬ reset-oracle), addr-out, real-mem, data-out)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          "big-machine" -- the definition of the microprocessor               ;;
;;                                                                              ;;
;;          This function is the definition of the FM8501 microprocessor.       ;;
;;          BIG-MACHINE executes as along as there are clock "ticks".  Clock    ;;
;;          "ticks" are characterized by there being elements left in the       ;;
;;          ORACLE.  Otherwise, this function just stops, effectively           ;;
;;          freezing the value of its variables (registers).                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: big-machine (mar,

read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, oracle)

= if oracle ≃ nil

then list (mar, read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history)

else big-machine (mar (mar, i-reg, dtack, reset, no-store), read (mar, i-reg), write (mar, i-reg, no-store), dtack (car (oracle)), reset (car (oracle)), no-store (no-store,

c-flag, v-flag, z-flag, n-flag, i-reg, mar),

data-out (data-out, a-reg, b-reg, c-flag, i-reg, mar), reg-file (reg-file,

data-out, i-reg, mar, no-store, reset),

addr-out (addr-out, reg-file, i-reg, mar, reset), c-flag (c-flag, a-reg, b-reg, i-reg, mar), v-flag (v-flag, a-reg, b-reg, c-flag, i-reg, mar), z-flag (z-flag, a-reg, b-reg, c-flag, i-reg, mar), n-flag (n-flag, a-reg, b-reg, c-flag, i-reg, mar), a-reg (a-reg,

visual-mem, reg-file, i-reg, mar, reset),

b-reg (b-reg, visual-mem, reg-file, i-reg, mar, reset),

i-reg (i-reg, visual-mem, mar), visual-mem (real-mem,

read, write, addr-out, memory-watch-dog-history, dtack (car (oracle)), reset (car (oracle))),

real-mem (real-mem, read, write, addr-out, data-out, memory-watch-dog-history, dtack (car (oracle)), reset (car (oracle))),

watch-dog (read, write, dtack (car (oracle)), data-out, addr-out),

cdr (oracle)) endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;                                                                              ;;
;;          "big-machine" operation on lists and empty lists                    ;;
;;                                                                              ;;
;;          The following two lemmas describe what BIG-MACHINE does when        ;;
;;          clock "ticks" are available or the clock has been exhausted.        ;;
;;          This information is easily available by looking at the definition   ;;
;;          BIG-MACHINE; however, these formulations make it easier for the     ;;
;;          theorem-prover to reason about BIG-MACHINE.                         ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: open-big-machine-on-nlistp (¬ listp (oracle)) → (big-machine (mar,

read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, oracle)

= list (mar, read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history))

Theorem: open-big-machine-on-listp listp (oracle) → (big-machine (mar,

read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, oracle)

= big-machine (mar (mar, i-reg, dtack, reset, no-store), read (mar, i-reg), write (mar, i-reg, no-store), dtack (car (oracle)), reset (car (oracle)), no-store-with-ifs (no-store,

c-flag, v-flag, z-flag, n-flag, i-reg,

mar),

data-out-with-ifs (data-out, a-reg, b-reg, c-flag, i-reg, mar),

reg-file (reg-file, data-out, i-reg, mar, no-store, reset),

addr-out (addr-out, reg-file, i-reg, mar, reset), c-flag-with-ifs (c-flag, a-reg, b-reg, i-reg, mar), v-flag-with-ifs (v-flag,

a-reg, b-reg, c-flag, i-reg, mar),

z-flag-with-ifs (z-flag, a-reg, b-reg, c-flag, i-reg, mar),

n-flag-with-ifs (n-flag, a-reg, b-reg, c-flag, i-reg, mar),

a-reg (a-reg, visual-mem, reg-file, i-reg, mar, reset), b-reg (b-reg, visual-mem, reg-file, i-reg, mar, reset), i-reg-with-ifs (i-reg, visual-mem, mar), visual-mem (real-mem,

read, write, addr-out, memory-watch-dog-history, dtack (car (oracle)), reset (car (oracle))),

real-mem (real-mem, read, write, addr-out, data-out, memory-watch-dog-history, dtack (car (oracle)), reset (car (oracle))),

watch-dog (read, write, dtack (car (oracle)), data-out, addr-out),

cdr (oracle)))

Event: Disable big-machine.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          This file contains definitions and lemmas concerning the            ;;
;;          sequencing of big-machine.  The proofs for the correctness of       ;;
;;          the micro-code are given here.                                      ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Lemma used to tear apart "append"ed oracles                         ;;
;;          This is the fundamental lemma for sequencing big-machine.           ;;
;;          It permits us to express computations on a (append a b) in terms    ;;
;;          of a computation on b applied to the state produced by a.  We can   ;;
;;          then get results about long computations by composing them from     ;;
;;          simple ones.                                                        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: big-machine-append (m = big-machine (mar,

read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, oracle1 ))

→ (big-machine (mar, read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, append (oracle1 , oracle2 ))

= big-machine (car (m), cadr (m), caddr (m), cadddr (m), caddddr (m), cadddddr (m), caddddddr (m), cadddddddr (m), caddddddddr (m), cadddddddddr (m), caddddddddddr (m), cadddddddddddr (m), caddddddddddddr (m), cadddddddddddddr (m), caddddddddddddddr (m), cadddddddddddddddr (m), caddddddddddddddddr (m), cadddddddddddddddddr (m), caddddddddddddddddddr (m), oracle2 ))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Miscellaneous lemmas about inc/dec and updating                     ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: bv-incrementer-truncates-to-machine-size ((zero = nat-to-bv (0, machine-size)) ∧ bitvp (bit-vec) ∧ (size (bit-vec) = machine-size)) → (bv-adder-output (t, zero, bit-vec) = v-nat-inc (bit-vec))

Event: Disable bv-incrementer-truncates-to-machine-size.

Theorem: bv-decrementer-truncates-to-machine-size-help ((bv-to-nat (bit-vec) ≮ 1) ∧ bitvp (bit-vec) ∧ (size (bit-vec) = 16) ∧ (bv-to-nat (bit-vec) ≠ 0)) → (nat-to-bv (bv-to-nat (bit-vec) − 1, 16)

= nat-to-bv (bv-to-nat (bit-vec) − 1, 16))

Theorem: bv-decrementer-truncates-to-machine-size ((zero = nat-to-bv (0, machine-size)) ∧ bitvp (bit-vec) ∧ (size (bit-vec) = machine-size)) → (bv-subtracter-output (t, zero, bit-vec) = v-nat-dec (bit-vec))

Event: Disable bv-decrementer-truncates-to-machine-size-help.

Event: Disable bv-decrementer-truncates-to-machine-size.

Theorem: trunc-size-1 (n = size (a)) → (trunc (a, n)

= if bitvp (a) then a else btm endif)

Theorem: size-v-nth ((size (a) = 3) ∧ (length (reg-file) = 8) ∧ every-member-sizep (reg-file, machine-size)) → (size (v-nth (a, reg-file)) = machine-size)

Theorem: update-update-nth update-nth (c, n, update-nth (c, n, lst, value2 ), value1 ) = update-nth (c, n, lst, value1 )

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Resetting "big-machine"                                              ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: mar-on-reset mar (mar, i-reg, dtack, t, no-store) = nat-to-bv (0, nxsz)

Theorem: reg-file-on-reset reg-file (reg-file, data-out, i-reg, mar, no-store, t) = update-nth (t, 0, reg-file, nat-to-bv (0, machine-size))

Theorem: listp-reg-file listp (reg-file (reg-file, data-out, i-reg, mar, no-store, reset)) = listp (reg-file)

;  The following lemma describes the first three clock "ticks" after a
;  reset occurs.  The memory-address register (MAR) is set to zero, the
;  read and write outputs are set to "false", and the reset latch is set
;  to "true".  Since nothing is know about the WATCH-DOG-HISTORY, it is
;  not possible to characterize what the memory state is.  However, after

;  these three clock "ticks" everything is stable (unchanging) until reset
;  is turned off.

Theorem: reset-to-state-0 (standard-hyps (mar,

read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem)

∧ (m = big-machine (mar, read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, list (list (dt1 , t), list (dt2 , t), list (dt3 , t)))))

→ ((car (m) = nat-to-bv (0, nxsz))

∧ (cadr (m) = f) ∧ (caddr (m) = f) ∧ (caddddr (m) = t) ∧ (nth (0, cadddddddr (m)) = nat-to-bv (0, machine-size)))

Event: Disable reset-to-state-0.

Definition: list-of-n-plus-1-dtack-off-reset-on (count) = if count ≃ 0 then list (list (f, t))

else cons (list (f, t), list-of-n-plus-1-dtack-off-reset-on (count − 1)) endif

Theorem: state-0-to-0-wait-help (mar0 = nat-to-bv (0, nxsz)) → (big-machine (mar0 ,

f, f, dtack, t, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, cons (list (dt-any, t), oracle))

= big-machine (mar0 , f, f, fix-bool (dt-any), t, no-store, data-out, update-nth (t,

              0,

reg-file,

nat-to-bv (0, machine-size)),

addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, machine-size), real-mem, watch-dog (f, f, fix-bool (dt-any), data-out, addr-out), oracle))

Event: Disable state-0-to-0-wait-help.

Definition: state-0-to-0-induction (dtack,

data-out, reg-file, addr-out, visual-mem, watch-dog, n)

= if n ≃ 0 then t

else state-0-to-0-induction (f, data-out, update-nth (t,

                 0,

reg-file, nat-to-bv (0,

machine-size)),

addr-out,

trunc (default-visual-mem-value,

machine-size), watch-dog (f, f, f, data-out, addr-out), n − 1) endif

Theorem: state-0-to-0-wait (mar0 = nat-to-bv (0, nxsz)) → (big-machine (mar0 ,

f, f, dtack, t, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list-of-n-plus-1-dtack-off-reset-on (n))

= list (nat-to-bv (0, nxsz), f, f, f, t, no-store, data-out, update-nth (t, 0, reg-file, nat-to-bv (0, machine-size)), addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, machine-size), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Event: Disable state-0-to-0-wait.

Theorem: state-0-to-1 (mar0 = nat-to-bv (0, nxsz)) → (big-machine (mar0 ,

f, f, dtack, t, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, list (list (dt-any1 , f), list (dt-any2 , f)))

= list (nat-to-bv (1, nxsz), f, f, fix-bool (dt-any2 ), f, no-store, data-out, update-nth (t, 0, reg-file, nat-to-bv (0, machine-size)), addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, fix-bool (dt-any2 ), data-out, addr-out)))

Event: Disable state-0-to-1.

Definition: state-0-to-0-wait-to-1-oracle (n) = append (list-of-n-plus-1-dtack-off-reset-on (n),

list (list (f, f), list (f, f)))

;  After the MAR has been set to zero, this lemma describes the steps taken by
;  FM8501 to prepare itself for executing instructions.

Theorem: state-0-to-0-wait-to-1 (standard-hyps (mar0 ,

f, f, dtack, t, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem)

∧ (mar0 = nat-to-bv (0, nxsz))) → (big-machine (mar0 ,

f, f, dtack, t, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, state-0-to-0-wait-to-1-oracle (n))

= list (nat-to-bv (1, nxsz), f, f, f, f, no-store, data-out, update-nth (t, 0, reg-file, nat-to-bv (0, machine-size)), addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Event: Disable state-0-to-0-wait-to-1.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          "big-machine" instruction loop -- micro-state by micro-state        ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Fetch the instruction, and increment the PC                         ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; We are about to embark on a litany of lemmas that move us from one microcode
; state to another.  By inspection of the oracles used below one can deduce the
; timing diagrams.  For example, the lemma below moves us from microcode state
; 1, where mar=1, and read, write, and reset are f, to microcode state 2, where
; mar=2, read, write, dtack and reset are f, the pc has been incremented,
; and addr-out contains the old pc.  To move from state 1 to 2, we need
; one clock tick with both dtack and reset f.
; We will similarly move through every state, some of which have several
; substates as we set lines, wait for acknowledgment, and then move.

; Once we get all the way through the microcode, we will append together
; the oracles to get an oracle that moves us all the way around from state 1
; to state 1.
; These lemmas make it perfectly clear what each state in the microcode does
; and how long each takes.

Theorem: state-1-to-2 (ramp (reg-file, machine-size, 8) ∧ (mar1 = nat-to-bv (1, nxsz))) → (big-machine (mar1 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, list (list (f, f)))

= list (nat-to-bv (2, nxsz), f, f, f, f, no-store, data-out, update-nth (t, 0, reg-file, v-nat-inc (nth (0, reg-file))), nth (0, reg-file), c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Event: Disable state-1-to-2.

Theorem: state-2-to-3-init (mar2 = nat-to-bv (2, nxsz)) → (big-machine (mar2 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f)))

= list (nat-to-bv (2, nxsz), t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Definition: list-of-n-plus-1-dtack-reset-off (count) = if count ≃ 0 then list (list (f, f))

else cons (list (f, f), list-of-n-plus-1-dtack-reset-off (count − 1)) endif

Theorem: state-2-to-2-wait-help (mar2 = nat-to-bv (2, nxsz)) → (big-machine (mar2 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, cons (list (f, f), oracle))

= big-machine (mar2 , t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, machine-size), real-mem, watch-dog (t, f, f, data-out, addr-out), oracle))

Definition: state-2-to-2-induction (dtack,

data-out,

addr-out,

visual-mem,

watch-dog-history, n)

= if n ≃ 0 then t

else state-2-to-2-induction (f, data-out, addr-out, trunc (default-visual-mem-value,

machine-size), watch-dog (t, f, f, data-out, addr-out), n − 1) endif

Theorem: state-2-to-3-wait (mar2 = nat-to-bv (2, nxsz)) → (big-machine (mar2 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list-of-n-plus-1-dtack-reset-off (n))

= list (nat-to-bv (2, nxsz), t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (t, f, f, data-out, addr-out)))

Event: Disable state-2-to-3-wait.

Theorem: upper-bound-bridge (n = exp (2, size (a))) → (bv-to-nat (a) < n)

Theorem: state-2-to-3-step3 (ramp (real-mem, machine-size, exp (2, machine-size)) ∧ sizep (addr-out, machine-size) ∧ (mar2 = nat-to-bv (2, nxsz)) ∧ (visual-mem = v-nth (addr-out, real-mem))) → (big-machine (mar2 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (t, f, f, data-out, addr-out), list (list (t, f), list (t, f)))

= list (nat-to-bv (3, nxsz), t, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, v-nth (addr-out, real-mem), real-mem, watch-dog (t, f, t, data-out, addr-out)))

Event: Disable state-2-to-3-step3.

Theorem: state-3-to-4 (ramp (real-mem, machine-size, exp (2, machine-size)) ∧ sizep (addr-out, machine-size) ∧ (mar3 = nat-to-bv (3, nxsz)) ∧ (visual-mem = v-nth (addr-out, real-mem))) → (big-machine (mar3 ,

t, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (t, f, t, data-out, addr-out), list (list (t, f)))

= list (nat-to-bv (4, nxsz), f, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, v-nth (addr-out, real-mem), v-nth (addr-out, real-mem), real-mem, watch-dog (t, f, t, data-out, addr-out)))

Event: Disable state-3-to-4.

;  This proof is required because it is impossible to keep "APPEND"
;  from opening up on constants.  The opening does not allow
;  "BIG-MACHINE-APPEND" to apply because the 'append' will have
;  disappeared before it get a chance to apply.

Theorem: state-2-to-3-step3-to-4 (ramp (real-mem, machine-size, exp (2, machine-size)) ∧ sizep (addr-out, machine-size)

∧ (mar2 = nat-to-bv (2, nxsz))) → (big-machine (mar2 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (t, f, f, data-out, addr-out), list (list (t, f), list (t, f), list (t, f)))

= list (nat-to-bv (4, nxsz), f, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, v-nth (addr-out, real-mem), v-nth (addr-out, real-mem), real-mem, watch-dog (t, f, t, data-out, addr-out)))

Event: Disable state-2-to-3-step3-to-4.

Definition: fetch-ir-oracle (n) = append (list (list (f, f)),

append (list (list (f, f)),

append (list-of-n-plus-1-dtack-reset-off (n), list (list (t, f), list (t, f), list (t, f)))))

Theorem: state-1-to-4 (ramp (reg-file, machine-size, 8) ∧ sizep (addr-out, machine-size) ∧ ramp (real-mem, machine-size, exp (2, machine-size)) ∧ (mar1 = nat-to-bv (1, nxsz))) → (big-machine (mar1 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, fetch-ir-oracle (n))

= list (nat-to-bv (4, nxsz), f, f, t, f, no-store, data-out, update-nth (t, 0, reg-file, v-nat-inc (nth (0, reg-file))), nth (0, reg-file), c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, v-nth (nth (0, reg-file), real-mem), v-nth (nth (0, reg-file), real-mem), real-mem, watch-dog (t, f, t, data-out, nth (0, reg-file))))

Event: Disable state-1-to-4.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Some size lemmas                                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: size-bv-reg-select size (bv-reg-select (i-reg, mar, reset)) = 3

Theorem: size-bv-oprd-a size (bv-oprd-a (i-reg)) = 3

Theorem: size-bv-oprd-b size (bv-oprd-b (i-reg)) = 3

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Fetch operand A, doing pre-decrement if necessary                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: fetch-oprd-a-reg-file (i-reg, reg-file) = update-v-nth (b-indirect-reg-a-dec (i-reg),

bv-oprd-a (i-reg),

reg-file,

v-nat-dec (v-nth (bv-oprd-a (i-reg), reg-file)))

Theorem: every-member-sizep-update-nth ((size (x) = width) ∧ every-member-sizep (lst, width)) → every-member-sizep (update-nth (bool, n, lst, x), width)

;  Both of the following two lemmas are needed, as we sometimes have RAMP enabled.

Theorem: ramp-fetch-oprd-a-reg-file ((m = machine-size) ∧ ramp (reg-file, machine-size, 8)) → ((length (fetch-oprd-a-reg-file (i-reg, reg-file)) = 8)

∧ every-member-sizep (fetch-oprd-a-reg-file (i-reg, reg-file), m))

Theorem: ramp-fetch-oprd-a-reg-file-2 ((m = machine-size) ∧ ramp (reg-file, machine-size, 8)) → ramp (fetch-oprd-a-reg-file (i-reg, reg-file), m, 8)

Definition: fetch-oprd-a-addr-out (i-reg, reg-file) = if b-indirect-reg-a-dec (i-reg)

then v-nat-dec (v-nth (bv-oprd-a (i-reg), reg-file)) else v-nth (bv-oprd-a (i-reg), reg-file) endif

Theorem: sizep-fetch-oprd-a-addr-out ((m = machine-size) ∧ ramp (reg-file, machine-size, 8)) → (size (fetch-oprd-a-addr-out (i-reg, reg-file)) = m)

Theorem: state-4-to-5 (ramp (reg-file, machine-size, 8) ∧ (mar4 = nat-to-bv (4, nxsz))) → (big-machine (mar4 ,

f, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog, list (list (f, f)))

= list (nat-to-bv (5, nxsz), f, f, f, f, no-store, data-out, fetch-oprd-a-reg-file (i-reg, reg-file), fetch-oprd-a-addr-out (i-reg, reg-file), c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Event: Disable state-4-to-5.

;  The next two prove-lemmas are of type nil -- we never use them as
;  rewrite rules.  Ideally we would like to append together the two clocks
;  for state-5-to-6-reg and state-6-to-7-reg.  But the two clocks are both
;  constant so the append computes and big-machine-append will not apply.
;  So we will actually prove state-4-to-5-to-6-to-7-reg as one rewrite rule.
;  But for the sake of exposition, we prove individual lemmas about each
;  state transition.

Theorem: state-5-to-6-reg (ramp (reg-file, machine-size, 8) ∧ (mar5 = nat-to-bv (5, nxsz)) ∧ b-direct-reg-a (i-reg)) → (big-machine (mar5 ,

f, f, dt-any, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f)))

= list (nat-to-bv (6, nxsz), f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Theorem: state-6-to-7-reg (ramp (reg-file, machine-size, 8) ∧ (mar6 = nat-to-bv (6, nxsz)) ∧ b-direct-reg-a (i-reg)) → (big-machine (mar6 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f)))

= list (nat-to-bv (7, nxsz), f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, v-nth (bv-oprd-a (i-reg), reg-file), b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Theorem: state-5-to-6-mem-init ((mar5 = nat-to-bv (5, nxsz)) ∧ (¬ b-direct-reg-a (i-reg))) → (big-machine (mar5 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, list (list (f, f)))

= list (nat-to-bv (5, nxsz), t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Event: Disable state-5-to-6-mem-init.

Theorem: state-5-to-6-mem-help ((mar5 = nat-to-bv (5, nxsz)) ∧ (¬ b-direct-reg-a (i-reg))) → (big-machine (mar5 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, cons (list (f, f), oracle))

= big-machine (mar5 , t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, machine-size), real-mem, watch-dog (t, f, f, data-out, addr-out), oracle))

Event: Disable state-5-to-6-mem-help.

Theorem: state-5-to-6-mem-wait ((mar5 = nat-to-bv (5, nxsz)) ∧ (¬ b-direct-reg-a (i-reg))) → (big-machine (mar5 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list-of-n-plus-1-dtack-reset-off (n))

= list (nat-to-bv (5, nxsz), t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (t, f, f, data-out, addr-out)))

Event: Disable state-5-to-6-mem-wait.

; The next two lemmas we never use as rewrite rules, for the same reasons
; explained above.

Theorem: state-5-to-6-mem-dtack ((mar5 = nat-to-bv (5, nxsz)) ∧ ramp (reg-file, machine-size, 8) ∧ sizep (addr-out, machine-size) ∧ (¬ b-direct-reg-a (i-reg))) → (big-machine (mar5 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (t, f, f, data-out, addr-out), list (list (t, f), list (t, f)))

= list (nat-to-bv (6, nxsz), t, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (v-nth (addr-out, real-mem), machine-size), real-mem, watch-dog (t, f, t, data-out, addr-out)))

Theorem: state-6-to-7-mem ((mar6 = nat-to-bv (6, nxsz)) ∧ ramp (reg-file, machine-size, 8) ∧ sizep (visual-mem, machine-size) ∧ sizep (addr-out, machine-size) ∧ (¬ b-direct-reg-a (i-reg))) → (big-machine (mar6 ,

t, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (t, f, t, data-out, addr-out), list (list (t, f)))

= list (nat-to-bv (7, nxsz), f, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, visual-mem, b-reg, i-reg, trunc (v-nth (addr-out, real-mem), machine-size), real-mem, watch-dog (t, f, t, data-out, addr-out)))

; We now piece together states 4, 5, 6, and 7 for the reg case:

Theorem: state-4-to-5-to-6-to-7-reg (ramp (reg-file, machine-size, 8) ∧ (mar4 = nat-to-bv (4, nxsz))

∧ b-direct-reg-a (i-reg)) → (big-machine (mar4 ,

f, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog, list (list (f, f), list (f, f), list (f, f)))

= list (nat-to-bv (7, nxsz), f, f, f, f, no-store, data-out, fetch-oprd-a-reg-file (i-reg, reg-file), fetch-oprd-a-addr-out (i-reg, reg-file), c-flag, v-flag, z-flag, n-flag, v-nth (bv-oprd-a (i-reg),

fetch-oprd-a-reg-file (i-reg, reg-file)), b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f,

f, f, data-out,

fetch-oprd-a-addr-out (i-reg, reg-file))))

Event: Disable state-4-to-5-to-6-to-7-reg.

; and now we do the same thing for 5, 6, and 7 in the mem case:

Theorem: state-5-to-6-to-7-mem-dtack ((mar5 = nat-to-bv (5, nxsz)) ∧ ramp (reg-file, machine-size, 8) ∧ sizep (addr-out, machine-size) ∧ (¬ b-direct-reg-a (i-reg))) → (big-machine (mar5 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (t, f, f, data-out, addr-out), list (list (t, f), list (t, f), list (t, f)))

= list (nat-to-bv (7, nxsz), f, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, trunc (v-nth (addr-out, real-mem), machine-size), b-reg, i-reg, trunc (v-nth (addr-out, real-mem), machine-size), real-mem, watch-dog (t, f, t, data-out, addr-out)))

Event: Disable state-5-to-6-to-7-mem-dtack.

; Finally, we do the entire transition from state 4 to state 7.  We first
; define the oracle necessary to drive the machine through the sequence.

Definition: fetch-oprd-a-oracle (i-reg, n) = if b-direct-reg-a (i-reg) then list (list (f, f), list (f, f), list (f, f))

else append (list (list (f, f)),

append (list (list (f, f)),

append (list-of-n-plus-1-dtack-reset-off (n), list (list (t, f), list (t, f), list (t, f))))) endif

Theorem: every-member-sizep-update-nth-machine-size ((size (x) = 16) ∧ every-member-sizep (lst, 16)) → every-member-sizep (update-nth (bool, n, lst, x), 16)

Event: Disable every-member-sizep-update-nth.

Theorem: state-4-to-7 (ramp (reg-file, machine-size, 8) ∧ sizep (addr-out, machine-size) ∧ ramp (real-mem, machine-size, exp (2, machine-size)) ∧ (mar4 = nat-to-bv (4, nxsz))) → (big-machine (mar4 ,

f, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog, fetch-oprd-a-oracle (i-reg, n))

= list (nat-to-bv (7, nxsz), f, f, ¬ b-direct-reg-a (i-reg), f, no-store, data-out, fetch-oprd-a-reg-file (i-reg, reg-file), fetch-oprd-a-addr-out (i-reg, reg-file), c-flag, v-flag, z-flag, n-flag, if b-direct-reg-a (i-reg) then v-nth (bv-oprd-a (i-reg),

fetch-oprd-a-reg-file (i-reg, reg-file))

else v-nth (fetch-oprd-a-addr-out (i-reg, reg-file),

real-mem) endif,

b-reg, i-reg, if b-direct-reg-a (i-reg) then trunc (default-visual-mem-value, 16) else v-nth (fetch-oprd-a-addr-out (i-reg, reg-file),

real-mem) endif,

real-mem, watch-dog (¬ b-direct-reg-a (i-reg),

f,

¬ b-direct-reg-a (i-reg),

data-out,

fetch-oprd-a-addr-out (i-reg, reg-file))))

Event: Disable state-4-to-7.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;

;;          Fetch operand B, doing pre-decrement if necessary                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: fetch-oprd-b-reg-file (i-reg, reg-file) = update-v-nth (b-indirect-reg-b-dec (i-reg),

bv-oprd-b (i-reg),

reg-file,

v-nat-dec (v-nth (bv-oprd-b (i-reg), reg-file)))

; Both of the following lemmas are needed, as RAMP is enabled sometimes

Theorem: ramp-fetch-oprd-b-reg-file ((m = machine-size) ∧ ramp (reg-file, machine-size, 8)) → ((length (fetch-oprd-b-reg-file (i-reg, reg-file)) = 8)

∧ every-member-sizep (fetch-oprd-b-reg-file (i-reg, reg-file), m))

Theorem: ramp-fetch-oprd-b-reg-file-2 ((m = machine-size) ∧ ramp (reg-file, machine-size, 8)) → ramp (fetch-oprd-b-reg-file (i-reg, reg-file), m, 8)

Definition: fetch-oprd-b-addr-out (i-reg, reg-file) = if b-indirect-reg-b-dec (i-reg)

then v-nat-dec (v-nth (bv-oprd-b (i-reg), reg-file))

else v-nth (bv-oprd-b (i-reg), reg-file) endif

Theorem: sizep-fetch-oprd-b-addr-out ((m = machine-size) ∧ ramp (reg-file, machine-size, 8)) → (size (fetch-oprd-b-addr-out (i-reg, reg-file)) = m)

Theorem: state-7-to-8 (ramp (reg-file, machine-size, 8) ∧ (mar7 = nat-to-bv (7, nxsz))) → (big-machine (mar7 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog, list (list (f, f)))

= list (nat-to-bv (8, nxsz), f, f, f, f, no-store, data-out, fetch-oprd-b-reg-file (i-reg, reg-file), fetch-oprd-b-addr-out (i-reg, reg-file), c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Event: Disable state-7-to-8.

; The next two lemmas are never used as rewrite rules.

Theorem: state-8-to-9-reg (ramp (reg-file, machine-size, 8) ∧ (mar8 = nat-to-bv (8, nxsz)) ∧ b-direct-reg-b (i-reg)) → (big-machine (mar8 ,

f, f, dt-any, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f)))

= list (nat-to-bv (9, nxsz), f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Theorem: state-9-to-10-reg (ramp (reg-file, machine-size, 8) ∧ (mar9 = nat-to-bv (9, nxsz)) ∧ b-direct-reg-b (i-reg)) → (big-machine (mar9 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f)))

= list (nat-to-bv (10, nxsz), f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, v-nth (bv-oprd-b (i-reg), reg-file), i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Theorem: state-8-to-9-mem-init ((mar8 = nat-to-bv (8, nxsz)) ∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar8 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, list (list (f, f)))

= list (nat-to-bv (8, nxsz), t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Event: Disable state-8-to-9-mem-init.

Theorem: state-8-to-9-mem-help ((mar8 = nat-to-bv (8, nxsz)) ∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar8 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, cons (list (f, f), oracle))

= big-machine (mar8 , t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, machine-size), real-mem, watch-dog (t, f, f, data-out, addr-out), oracle))

Event: Disable state-8-to-9-mem-help.

Theorem: state-8-to-9-mem-wait ((mar8 = nat-to-bv (8, nxsz)) ∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar8 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list-of-n-plus-1-dtack-reset-off (n))

= list (nat-to-bv (8, nxsz), t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (t, f, f, data-out, addr-out)))

Event: Disable state-8-to-9-mem-wait.

; the next two are never used as rewrites.

Theorem: state-8-to-9-mem-dtack ((mar8 = nat-to-bv (8, nxsz))

∧ ramp (reg-file, machine-size, 8) ∧ sizep (addr-out, machine-size) ∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar8 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (t, f, f, data-out, addr-out), list (list (t, f), list (t, f)))

= list (nat-to-bv (9, nxsz), t, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (v-nth (addr-out, real-mem), machine-size), real-mem, watch-dog (t, f, t, data-out, addr-out)))

Theorem: state-9-to-10-mem ((mar9 = nat-to-bv (9, nxsz)) ∧ ramp (reg-file, machine-size, 8) ∧ sizep (visual-mem, machine-size) ∧ sizep (addr-out, machine-size) ∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar9 ,

t, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (t, f, t, data-out, addr-out), list (list (t, f)))

= list (nat-to-bv (10, nxsz), f, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, visual-mem, i-reg, trunc (v-nth (addr-out, real-mem), machine-size), real-mem, watch-dog (t, f, t, data-out, addr-out)))

; We now piece together states 7, 8, 9, and 10 for the reg case:

Theorem: state-7-to-8-to-9-to-10-reg (ramp (reg-file, machine-size, 8) ∧ (mar7 = nat-to-bv (7, nxsz)) ∧ b-direct-reg-b (i-reg)) → (big-machine (mar7 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog, list (list (f, f), list (f, f), list (f, f)))

= list (nat-to-bv (10, nxsz), f, f, f, f, no-store, data-out, fetch-oprd-b-reg-file (i-reg, reg-file), fetch-oprd-b-addr-out (i-reg, reg-file), c-flag, v-flag, z-flag, n-flag, a-reg, v-nth (bv-oprd-b (i-reg),

fetch-oprd-b-reg-file (i-reg, reg-file)), i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f,

f, f, data-out, fetch-oprd-b-addr-out (i-reg, reg-file))))

Event: Disable state-7-to-8-to-9-to-10-reg.

; and now we do the same thing for 8, 9 and 10 in the mem case.

Theorem: state-8-to-9-to-10-mem-dtack ((mar8 = nat-to-bv (8, nxsz)) ∧ ramp (reg-file, machine-size, 8) ∧ sizep (addr-out, machine-size) ∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar8 ,

t, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (t, f, f, data-out, addr-out), list (list (t, f), list (t, f), list (t, f)))

= list (nat-to-bv (10, nxsz), f, f, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, trunc (v-nth (addr-out, real-mem), machine-size), i-reg, trunc (v-nth (addr-out, real-mem), machine-size), real-mem, watch-dog (t, f, t, data-out, addr-out)))

Event: Disable state-5-to-6-to-7-mem-dtack.

; Finally, we do the entire transition from state 7 to state 10.  We first
; define the oracle necessary to drive the machine through the sequence.

Definition: fetch-oprd-b-oracle (i-reg, n) = if b-direct-reg-b (i-reg) then list (list (f, f), list (f, f), list (f, f))

else append (list (list (f, f)),

append (list (list (f, f)),

append (list-of-n-plus-1-dtack-reset-off (n), list (list (t, f), list (t, f), list (t, f))))) endif

Theorem: state-7-to-10 (ramp (reg-file, machine-size, 8) ∧ sizep (addr-out, machine-size) ∧ ramp (real-mem, machine-size, exp (2, machine-size)) ∧ (mar7 = nat-to-bv (7, nxsz))) → (big-machine (mar7 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog, fetch-oprd-b-oracle (i-reg, n))

= list (nat-to-bv (10, nxsz), f, f, ¬ b-direct-reg-b (i-reg), f, no-store, data-out, fetch-oprd-b-reg-file (i-reg, reg-file), fetch-oprd-b-addr-out (i-reg, reg-file), c-flag, v-flag, z-flag, n-flag, a-reg, if b-direct-reg-b (i-reg) then v-nth (bv-oprd-b (i-reg),

fetch-oprd-b-reg-file (i-reg, reg-file))

else v-nth (fetch-oprd-b-addr-out (i-reg, reg-file),

real-mem) endif,

i-reg, if b-direct-reg-b (i-reg) then trunc (default-visual-mem-value, 16) else v-nth (fetch-oprd-b-addr-out (i-reg, reg-file),

real-mem) endif,

real-mem, watch-dog (¬ b-direct-reg-b (i-reg),

f,

¬ b-direct-reg-b (i-reg),

data-out,

fetch-oprd-b-addr-out (i-reg, reg-file))))

Event: Disable state-7-to-10.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;

;;                   ALU, results to memory or register                         ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: alu-c-flag (i-reg, a-reg, b-reg, c-flag) = if b-cc-set (i-reg)

then c (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg)))

else c-flag endif

Definition: alu-v-flag (i-reg, a-reg, b-reg, c-flag, v-flag) = if b-cc-set (i-reg)

then v (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg)))

else v-flag endif

Definition: alu-z-flag (i-reg, a-reg, b-reg, c-flag, z-flag) = if b-cc-set (i-reg)

then b-bv-zerop (bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))))

else z-flag endif

Definition: alu-n-flag (i-reg, a-reg, b-reg, c-flag, n-flag) = if b-cc-set (i-reg)

then bitn (bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))),

machine-size)

else n-flag endif

Theorem: boolp-alu-c-flag boolp (c-flag) → boolp (alu-c-flag (i-reg, a-reg, b-reg, c-flag))

Theorem: boolp-alu-v-flag boolp (v-flag) → boolp (alu-v-flag (i-reg, a-reg, b-reg, c-flag, v-flag))

Theorem: boolp-alu-z-flag boolp (z-flag) → boolp (alu-z-flag (i-reg, a-reg, b-reg, c-flag, z-flag))

Theorem: boolp-alu-n-flag boolp (n-flag) → boolp (alu-n-flag (i-reg, a-reg, b-reg, c-flag, n-flag))

Theorem: state-10-to-11 ((mar10 = nat-to-bv (10, nxsz)) ∧ boolp (no-store)

∧ boolp (c-flag) ∧ boolp (v-flag) ∧ boolp (n-flag) ∧ boolp (z-flag) ∧ sizep (data-out, machine-size)) → (big-machine (mar10 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f)))

= list (nat-to-bv (11, nxsz), f, f, f, f, ¬ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg), bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))), reg-file, addr-out, alu-c-flag (i-reg, a-reg, b-reg, c-flag), alu-v-flag (i-reg, a-reg, b-reg, c-flag, v-flag), alu-z-flag (i-reg, a-reg, b-reg, c-flag, z-flag), alu-n-flag (i-reg, a-reg, b-reg, c-flag, n-flag), a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Event: Disable state-10-to-11.

Event: Disable alu-c-flag.

Event: Disable alu-v-flag.

Event: Disable alu-z-flag.

Event: Disable alu-n-flag.

Theorem: state-11-to-12-reg (ramp (reg-file, machine-size, 8) ∧ sizep (data-out, machine-size) ∧ (mar11 = nat-to-bv (11, nxsz)) ∧ b-direct-reg-b (i-reg)) → (big-machine (mar11 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f)))

= list (nat-to-bv (12, nxsz), f, f, f, f, no-store, data-out, update-v-nth (¬ no-store,

bv-oprd-b (i-reg), reg-file, data-out),

addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Theorem: state-11-to-12-mem-no-store ((mar11 = nat-to-bv (11, nxsz)) ∧ (no-store = t) ∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar11 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f)))

= list (nat-to-bv (12, nxsz), f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Theorem: state-11-to-12-mem-init-store ((mar11 = nat-to-bv (11, nxsz)) ∧ (no-store = f) ∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar11 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f)))

= list (nat-to-bv (11, nxsz), f, t, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Event: Disable state-11-to-12-mem-init-store.

Theorem: state-11-to-12-mem-help ((mar11 = nat-to-bv (11, nxsz)) ∧ (no-store = f) ∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar11 ,

f, t, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, cons (list (f, f), oracle))

= big-machine (mar11 , f, t, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, machine-size), real-mem, watch-dog (f, t, f, data-out, addr-out), oracle))

Event: Disable state-11-to-12-mem-help.

Definition: state-11-to-11-induction (dtack,

data-out, addr-out, visual-mem, watch-dog-history, n)

= if n ≃ 0 then t

else state-11-to-11-induction (f, data-out, addr-out, trunc (default-visual-mem-value,

machine-size), watch-dog (f, t, f, data-out, addr-out), n − 1) endif

Theorem: state-11-to-12-mem-wait-store ((mar11 = nat-to-bv (11, nxsz)) ∧ (no-store = f) ∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar11 ,

f, t, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list-of-n-plus-1-dtack-reset-off (n))

= list (nat-to-bv (11, nxsz), f, t, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, t, f, data-out, addr-out)))

Event: Disable state-11-to-12-mem-wait-store.

Theorem: state-11-to-12-mem-dtack-store (sizep (addr-out, machine-size) ∧ (mar11 = nat-to-bv (11, nxsz)) ∧ (no-store = f)

∧ (¬ b-direct-reg-b (i-reg))) → (big-machine (mar11 ,

f, t, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (f, t, f, data-out, addr-out), list (list (t, f), list (t, f)))

= list (nat-to-bv (12, nxsz), f, t, t, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), update-v-nth (t, addr-out, real-mem, data-out), watch-dog (f, t, t, data-out, addr-out)))

Event: Disable state-11-to-12-mem-dtack-store.

Theorem: state-10-to-12-reg ((mar10 = nat-to-bv (10, nxsz)) ∧ boolp (no-store) ∧ boolp (c-flag) ∧ boolp (v-flag) ∧ boolp (n-flag) ∧ boolp (z-flag) ∧ sizep (data-out, machine-size) ∧ sizep (a-reg, machine-size) ∧ ramp (reg-file, machine-size, 8) ∧ b-direct-reg-b (i-reg)) → (big-machine (mar10 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f), list (f, f)))

= list (nat-to-bv (12, nxsz), f, f, f, f, ¬ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg), bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))), update-v-nth (b-store-alu-result (c-flag,

v-flag, z-flag, n-flag, i-reg),

bv-oprd-b (i-reg), reg-file, bv (bv-alu-cv (a-reg,

b-reg, c-flag, bv-alu-op-code (i-reg)))),

addr-out, alu-c-flag (i-reg, a-reg, b-reg, c-flag), alu-v-flag (i-reg, a-reg, b-reg, c-flag, v-flag), alu-z-flag (i-reg, a-reg, b-reg, c-flag, z-flag), alu-n-flag (i-reg, a-reg, b-reg, c-flag, n-flag), a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f,

f, f, bv (bv-alu-cv (a-reg,

b-reg, c-flag, bv-alu-op-code (i-reg))),

addr-out)))

Event: Disable state-10-to-12-reg.

Theorem: state-10-to-12-mem-no-store ((mar10 = nat-to-bv (10, nxsz)) ∧ boolp (c-flag) ∧ boolp (v-flag) ∧ boolp (n-flag) ∧ boolp (z-flag) ∧ sizep (data-out, machine-size) ∧ sizep (a-reg, machine-size) ∧ (¬ b-direct-reg-b (i-reg)) ∧ (¬ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg))) → (big-machine (mar10 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f), list (f, f)))

= list (nat-to-bv (12, nxsz), f, f, f, f, ¬ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg), bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))), reg-file, addr-out, alu-c-flag (i-reg, a-reg, b-reg, c-flag), alu-v-flag (i-reg, a-reg, b-reg, c-flag, v-flag), alu-z-flag (i-reg, a-reg, b-reg, c-flag, z-flag), alu-n-flag (i-reg, a-reg, b-reg, c-flag, n-flag), a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f,

f, f, bv (bv-alu-cv (a-reg,

b-reg, c-flag, bv-alu-op-code (i-reg))),

addr-out)))

Event: Disable state-10-to-12-mem-no-store.

Theorem: state-10-to-12-mem-store ((mar10 = nat-to-bv (10, nxsz)) ∧ boolp (no-store) ∧ boolp (c-flag)

∧ boolp (v-flag) ∧ boolp (n-flag) ∧ boolp (z-flag) ∧ sizep (data-out, machine-size) ∧ sizep (addr-out, machine-size) ∧ sizep (a-reg, machine-size) ∧ (¬ b-direct-reg-b (i-reg)) ∧ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg)) → (big-machine (mar10 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, append (list (list (f, f)),

append (list (list (f, f)),

append (list-of-n-plus-1-dtack-reset-off (n), list (list (t, f), list (t, f))))))

= list (nat-to-bv (12, nxsz), f, t, t, f, ¬ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg), bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))), reg-file, addr-out, alu-c-flag (i-reg, a-reg, b-reg, c-flag), alu-v-flag (i-reg, a-reg, b-reg, c-flag, v-flag), alu-z-flag (i-reg, a-reg, b-reg, c-flag, z-flag), alu-n-flag (i-reg, a-reg, b-reg, c-flag, n-flag), a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), update-v-nth (t,

addr-out, real-mem, bv (bv-alu-cv (a-reg,

b-reg, c-flag, bv-alu-op-code (i-reg)))),

watch-dog (f, t, t, bv (bv-alu-cv (a-reg,

b-reg, c-flag, bv-alu-op-code (i-reg))),

addr-out)))

Event: Disable state-10-to-12-mem-store.

Definition: alu-oracle (i-reg, c-flag, v-flag, z-flag, n-flag, n) = if b-direct-reg-b (i-reg) then list (list (f, f), list (f, f))

elseif b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg)

then append (list (list (f, f)),

append (list (list (f, f)),

append (list-of-n-plus-1-dtack-reset-off (n), list (list (t, f), list (t, f)))))

else list (list (f, f), list (f, f)) endif

Theorem: update-nth-f update-nth (f, n, lst, val) = lst

Definition: mem-store-flag (i-reg, c-flag, v-flag, z-flag, n-flag) = if b-direct-reg-b (i-reg) then f

else b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg) endif

Theorem: state-10-to-12 (boolp (no-store) ∧ boolp (c-flag) ∧ boolp (v-flag)

∧ boolp (n-flag) ∧ boolp (z-flag) ∧ sizep (data-out, machine-size) ∧ sizep (a-reg, machine-size) ∧ sizep (addr-out, machine-size) ∧ ramp (reg-file, machine-size, 8) ∧ (mar10 = nat-to-bv (10, nxsz))) → (big-machine (mar10 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, alu-oracle (i-reg, c-flag, v-flag, z-flag, n-flag, n))

= list (nat-to-bv (12, nxsz), f, mem-store-flag (i-reg, c-flag, v-flag, z-flag, n-flag), mem-store-flag (i-reg, c-flag, v-flag, z-flag, n-flag), f, ¬ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg), bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))), update-v-nth (b-direct-reg-b (i-reg)

∧ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg),

bv-oprd-b (i-reg),

reg-file,

bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg)))),

addr-out, alu-c-flag (i-reg, a-reg, b-reg, c-flag), alu-v-flag (i-reg, a-reg, b-reg, c-flag, v-flag), alu-z-flag (i-reg, a-reg, b-reg, c-flag, z-flag), alu-n-flag (i-reg, a-reg, b-reg, c-flag, n-flag), a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), update-v-nth ((¬ b-direct-reg-b (i-reg))

∧ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg),

addr-out, real-mem, bv (bv-alu-cv (a-reg,

b-reg, c-flag, bv-alu-op-code (i-reg)))),

watch-dog (f,

mem-store-flag (i-reg, c-flag, v-flag, z-flag, n-flag),

mem-store-flag (i-reg, c-flag, v-flag, z-flag, n-flag),

bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))),

addr-out)))

Event: Disable state-10-to-12.

Event: Disable mem-store-flag.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                  Post-increment operations                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: state-12-to-13 (ramp (reg-file, machine-size, 8) ∧ (truep (mem-store-flag) ∨ falsep (mem-store-flag)) ∧ (mar12 = nat-to-bv (12, nxsz))) → (big-machine (mar12 ,

f, mem-store-flag, mem-store-flag, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (f,

mem-store-flag, mem-store-flag, data-out, addr-out),

list (list (mem-store-flag, f)))

= list (nat-to-bv (13, nxsz), f, f, mem-store-flag, f, no-store, data-out, update-v-nth (b-indirect-reg-a-inc (i-reg), bv-oprd-a (i-reg), reg-file, v-nat-inc (v-nth (bv-oprd-a (i-reg), reg-file))),

addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f,

mem-store-flag, mem-store-flag, data-out, addr-out)))

Theorem: state-13-to-1 (ramp (reg-file, machine-size, 8) ∧ (mar13 = nat-to-bv (13, nxsz))) → (big-machine (mar13 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, list (list (f, f)))

= list (nat-to-bv (1, nxsz), f, f, f, f, no-store, data-out, update-v-nth (b-indirect-reg-b-inc (i-reg),

bv-oprd-b (i-reg),

reg-file,

v-nat-inc (v-nth (bv-oprd-b (i-reg), reg-file))),

addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Definition: reg-file-post-inc (i-reg, reg-file) = update-v-nth (b-indirect-reg-b-inc (i-reg),

bv-oprd-b (i-reg),

update-v-nth (b-indirect-reg-a-inc (i-reg), bv-oprd-a (i-reg), reg-file, v-nat-inc (v-nth (bv-oprd-a (i-reg), reg-file))),

v-nat-inc (v-nth (bv-oprd-b (i-reg),

update-v-nth (b-indirect-reg-a-inc (i-reg), bv-oprd-a (i-reg), reg-file, v-nat-inc (v-nth (bv-oprd-a (i-reg),

reg-file))))))

Theorem: state-12-to-1 (ramp (reg-file, machine-size, 8) ∧ (truep (mem-store-flag) ∨ falsep (mem-store-flag)) ∧ (mar12 = nat-to-bv (12, nxsz))) → (big-machine (mar12 ,

f,

mem-store-flag, mem-store-flag, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog (f,

mem-store-flag, mem-store-flag, data-out, addr-out), list (list (mem-store-flag, f), list (f, f)))

= list (nat-to-bv (1, nxsz), f, f, f, f, no-store, data-out, reg-file-post-inc (i-reg, reg-file), addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem, watch-dog (f, f, f, data-out, addr-out)))

Event: Disable state-12-to-1.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;                  Pasting together the steps                                  ;;

;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; In state-4-to-7 we rewrite to something of the form (list ... (if a b c) ...).
; When applying big-machine-append the variable M is bound to the rewritten version
; of this form.  But the rewriter moves the if's out, producing
; (if a (list ... b ...) (list ... c ...)).  We then, in simplifying the rhs of
; big-machine-append, rewrite (cadr M) to get the new read.  We want it to rewrite to
; f but in fact it rewrites to (cadr (if a (list mar7 f ...) (list mar7 f ...))).
; Then, state-7-to-10 doesn't unify.  So we prove the following two facts.
; Because of these, we don't really care whether our state steppers return
; lists with if's inside or outside.

Theorem: car-if car (if a then b

else c endif) = if a then car (b)

else car (c) endif

Theorem: cdr-if cdr (if a then b

else c endif) = if a then cdr (b)

else cdr (c) endif

Definition: reg-file-after-a-b (reg-file, real-mem) = fetch-oprd-b-reg-file (v-nth (nth (0, reg-file), real-mem),

fetch-oprd-a-reg-file (v-nth (nth (0, reg-file),

real-mem), update-nth (t,

                                                 0,

reg-file,

v-nat-inc (nth (0, reg-file)))))

Definition: addr-out-after-a-b (reg-file, real-mem) = fetch-oprd-b-addr-out (v-nth (nth (0, reg-file), real-mem),

fetch-oprd-a-reg-file (v-nth (nth (0, reg-file),

real-mem), update-nth (t,

                                                  0,

reg-file,

v-nat-inc (nth (0, reg-file)))))

Definition: a-reg-after-a-b (reg-file, real-mem) = if b-direct-reg-a (v-nth (nth (0, reg-file), real-mem))

then v-nth (bv-oprd-a (v-nth (nth (0, reg-file), real-mem)),

fetch-oprd-a-reg-file (v-nth (nth (0, reg-file), real-mem), update-nth (t,

                                          0,

reg-file,

v-nat-inc (nth (0, reg-file)))))

else v-nth (fetch-oprd-a-addr-out (v-nth (nth (0, reg-file),

real-mem), update-nth (t,

                                           0,

reg-file,

v-nat-inc (nth (0,

reg-file)))),

real-mem) endif

Definition: b-reg-after-a-b (reg-file, real-mem) = if b-direct-reg-b (v-nth (nth (0, reg-file), real-mem))

then v-nth (bv-oprd-b (v-nth (nth (0, reg-file), real-mem)),

fetch-oprd-b-reg-file (v-nth (nth (0, reg-file), real-mem),

fetch-oprd-a-reg-file (v-nth (nth (0,

reg-file), real-mem),

update-nth (t,

                                                           0,

reg-file,

v-nat-inc (nth (0,

reg-file))))))

else v-nth (fetch-oprd-b-addr-out (v-nth (nth (0, reg-file),

real-mem), fetch-oprd-a-reg-file (v-nth (nth (0,

reg-file), real-mem),

update-nth (t,

                                                            0,

reg-file,

v-nat-inc (nth (0,

reg-file))))),

real-mem) endif

Definition: visual-mem-after-a-b (reg-file, real-mem) = if b-direct-reg-b (v-nth (nth (0, reg-file), real-mem))

then trunc (default-visual-mem-value, 16)

else v-nth (fetch-oprd-b-addr-out (v-nth (nth (0, reg-file),

real-mem), fetch-oprd-a-reg-file (v-nth (nth (0,

reg-file), real-mem),

update-nth (t,

                                                            0,

reg-file,

v-nat-inc (nth (0,

reg-file))))),

real-mem) endif

Definition: dtack-after-a-b (reg-file, real-mem) = (¬ b-direct-reg-b (v-nth (nth (0, reg-file), real-mem)))

Definition: a-b-oracle (reg-file, real-mem, i, n, m) = append (fetch-ir-oracle (i),

append (fetch-oprd-a-oracle (v-nth (nth (0, reg-file), real-mem), n), fetch-oprd-b-oracle (v-nth (nth (0, reg-file), real-mem), m)))

Theorem: state-1-to-10 (ramp (reg-file, machine-size, 8) ∧ sizep (addr-out, machine-size) ∧ ramp (real-mem, machine-size, exp (2, machine-size)) ∧ (mar1 = nat-to-bv (1, nxsz))) → (big-machine (mar1 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog, a-b-oracle (reg-file, real-mem, i, n, m))

= list (nat-to-bv (10, nxsz), f, f, dtack-after-a-b (reg-file, real-mem), f, no-store, data-out, reg-file-after-a-b (reg-file, real-mem), addr-out-after-a-b (reg-file, real-mem), c-flag, v-flag, z-flag, n-flag, a-reg-after-a-b (reg-file, real-mem), b-reg-after-a-b (reg-file, real-mem), v-nth (nth (0, reg-file), real-mem), visual-mem-after-a-b (reg-file, real-mem), real-mem, watch-dog (dtack-after-a-b (reg-file, real-mem),

f,

dtack-after-a-b (reg-file, real-mem), data-out, addr-out-after-a-b (reg-file, real-mem))))

Definition: reg-file-alu (i-reg, c-flag, v-flag, z-flag, n-flag, reg-file, a-reg, b-reg) = update-v-nth (b-direct-reg-b (i-reg)

∧ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg),

bv-oprd-b (i-reg),

reg-file,

bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))))

Definition: reg-file-from-alu-thru-post-inc (i-reg,

c-flag, v-flag, z-flag, n-flag, reg-file, a-reg, b-reg)

= update-v-nth (b-indirect-reg-b-inc (i-reg), bv-oprd-b (i-reg), update-v-nth (b-indirect-reg-a-inc (i-reg),

bv-oprd-a (i-reg), reg-file-alu (i-reg,

c-flag, v-flag, z-flag, n-flag, reg-file, a-reg, b-reg),

v-nat-inc (v-nth (bv-oprd-a (i-reg),

reg-file-alu (i-reg, c-flag, v-flag, z-flag, n-flag, reg-file, a-reg, b-reg)))),

v-nat-inc (v-nth (bv-oprd-b (i-reg),

update-v-nth (b-indirect-reg-a-inc (i-reg), bv-oprd-a (i-reg), reg-file-alu (i-reg,

c-flag, v-flag, z-flag, n-flag, reg-file, a-reg, b-reg),

v-nat-inc (v-nth (bv-oprd-a (i-reg),

reg-file-alu (i-reg, c-flag, v-flag, z-flag, n-flag, reg-file, a-reg, b-reg)))))))

Definition: real-mem-thru-post-inc (i-reg,

c-flag, v-flag, z-flag, n-flag, addr-out, real-mem, a-reg, b-reg)

= update-v-nth ((¬ b-direct-reg-b (i-reg))

∧ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg),

addr-out, real-mem, bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))))

Definition: alu-post-inc-oracle (i-reg, c-flag, v-flag, z-flag, n-flag, n) = append (alu-oracle (i-reg, c-flag, v-flag, z-flag, n-flag, n),

list (list (mem-store-flag (i-reg, c-flag, v-flag, z-flag, n-flag), f), list (f, f)))

Theorem: ramp-if ramp (if c then a

else b endif, i, j )

= if c then ramp (a, i, j ) else ramp (b, i, j ) endif

Theorem: ramp-update-nth (ramp (reg-file, width, number) ∧ sizep (value, width) ∧ boolp (boolean)

∧ (number ≮ place)) → ramp (update-nth (boolean, place, reg-file, value), width, number)

Theorem: state-10-to-1 (boolp (no-store) ∧ boolp (c-flag) ∧ boolp (v-flag) ∧ boolp (n-flag) ∧ boolp (z-flag) ∧ sizep (data-out, machine-size) ∧ sizep (a-reg, machine-size) ∧ sizep (addr-out, machine-size) ∧ ramp (reg-file, machine-size, 8) ∧ (mar10 = nat-to-bv (10, nxsz))) → (big-machine (mar10 ,

f, f, dtack, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog-history, alu-post-inc-oracle (i-reg, c-flag, v-flag, z-flag, n-flag, n))

= list (nat-to-bv (1, nxsz), f, f, f, f, ¬ b-store-alu-result (c-flag, v-flag, z-flag, n-flag, i-reg), bv (bv-alu-cv (a-reg, b-reg, c-flag, bv-alu-op-code (i-reg))), reg-file-from-alu-thru-post-inc (i-reg,

c-flag, v-flag, z-flag, n-flag, reg-file, a-reg, b-reg),

addr-out, alu-c-flag (i-reg, a-reg, b-reg, c-flag), alu-v-flag (i-reg, a-reg, b-reg, c-flag, v-flag), alu-z-flag (i-reg, a-reg, b-reg, c-flag, z-flag), alu-n-flag (i-reg, a-reg, b-reg, c-flag, n-flag), a-reg, b-reg, i-reg, trunc (default-visual-mem-value, 16), real-mem-thru-post-inc (i-reg,

c-flag, v-flag, z-flag, n-flag, addr-out, real-mem, a-reg, b-reg),

watch-dog (f, f, f, bv (bv-alu-cv (a-reg,

b-reg, c-flag, bv-alu-op-code (i-reg))),

addr-out)))

Event: Disable state-10-to-1.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;            The lemmas that follow culminate in lemma STATE-1-to-1            ;;
;;            which is a statement of what FM8501 does upon executing           ;;
;;            an instruction.  FM8501 executes one memory based instruction     ;;
;;            by starting in a state where the MAR is "1", executing some       ;;
;;            of micro-states eventually taking it back to a place where        ;;
;;            MAR is equal to "1".                                              ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: sizep-a-reg-after-a-b (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (size (a-reg-after-a-b (reg-file, real-mem)) = machine-size)

Theorem: sizep-addr-out-after-a-b ramp (reg-file, machine-size, 8) → (size (addr-out-after-a-b (reg-file, real-mem)) = machine-size)

Theorem: ramp-reg-file-after-a-b ((m = machine-size) ∧ ramp (reg-file, machine-size, 8)) → ramp (reg-file-after-a-b (reg-file, real-mem), m, 8)

Definition: state-1-to-1-oracle (reg-file,

real-mem, c-flag, v-flag, z-flag, n-flag, ir-wait, a-wait, b-wait, store-wait)

= append (a-b-oracle (reg-file, real-mem, ir-wait, a-wait, b-wait),

alu-post-inc-oracle (v-nth (nth (0, reg-file), real-mem), c-flag, v-flag, z-flag, n-flag, store-wait))

Theorem: state-1-to-1 (boolp (no-store) ∧ boolp (c-flag) ∧ boolp (v-flag) ∧ boolp (n-flag) ∧ boolp (z-flag) ∧ ramp (reg-file, machine-size, 8) ∧ sizep (data-out, machine-size) ∧ sizep (addr-out, machine-size) ∧ ramp (real-mem, machine-size, exp (2, machine-size))

∧ (mar1 = nat-to-bv (1, nxsz))) → (big-machine (mar1 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog, state-1-to-1-oracle (reg-file,

real-mem, c-flag, v-flag, z-flag, n-flag, ir-wait, a-wait, b-wait, store-wait))

= list (nat-to-bv (1, nxsz), f, f, f, f, ¬ b-store-alu-result (c-flag,

v-flag, z-flag, n-flag, v-nth (nth (0, reg-file), real-mem)),

bv (bv-alu-cv (a-reg-after-a-b (reg-file, real-mem), b-reg-after-a-b (reg-file, real-mem), c-flag, bv-alu-op-code (v-nth (nth (0, reg-file),

real-mem)))),

reg-file-from-alu-thru-post-inc (v-nth (nth (0, reg-file),

real-mem), c-flag, v-flag, z-flag, n-flag, reg-file-after-a-b (reg-file,

real-mem),

a-reg-after-a-b (reg-file,

real-mem),

b-reg-after-a-b (reg-file,

real-mem)),

addr-out-after-a-b (reg-file, real-mem), alu-c-flag (v-nth (nth (0, reg-file), real-mem),

a-reg-after-a-b (reg-file, real-mem), b-reg-after-a-b (reg-file, real-mem), c-flag),

alu-v-flag (v-nth (nth (0, reg-file), real-mem), a-reg-after-a-b (reg-file, real-mem), b-reg-after-a-b (reg-file, real-mem), c-flag, v-flag),

alu-z-flag (v-nth (nth (0, reg-file), real-mem), a-reg-after-a-b (reg-file, real-mem), b-reg-after-a-b (reg-file, real-mem), c-flag, z-flag),

alu-n-flag (v-nth (nth (0, reg-file), real-mem), a-reg-after-a-b (reg-file, real-mem), b-reg-after-a-b (reg-file, real-mem), c-flag, n-flag),

a-reg-after-a-b (reg-file, real-mem), b-reg-after-a-b (reg-file, real-mem), v-nth (nth (0, reg-file), real-mem), trunc (default-visual-mem-value, 16), real-mem-thru-post-inc (v-nth (nth (0, reg-file), real-mem),

c-flag, v-flag, z-flag, n-flag, addr-out-after-a-b (reg-file,

real-mem), real-mem, a-reg-after-a-b (reg-file, real-mem), b-reg-after-a-b (reg-file, real-mem)),

watch-dog (f, f, f, bv (bv-alu-cv (a-reg-after-a-b (reg-file, real-mem),

b-reg-after-a-b (reg-file, real-mem), c-flag, bv-alu-op-code (v-nth (nth (0,

reg-file), real-mem)))),

addr-out-after-a-b (reg-file, real-mem))))

Event: Disable state-1-to-1.

Theorem: nth-update-nth nth (i, update-nth (c, j , lst, x)) = if truep (c) ∧ (fix (i) = fix (j )) ∧ (j < length (lst)) then x

else nth (i, lst) endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Software specification of FM8501.                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Helping definitions for the specification of the software           ;;
;;          machine.  Function SOFT is the actual definition defining           ;;
;;          the operation of the FM8501.                                        ;;
;;                                                                              ;;
;;          When programming the FM8501 the user see eight general purpose      ;;
;;          registers (register file), four flag bits (carry, overflow,         ;;
;;          negative, and zero), and the memory.  Instruction execution         ;;
;;          is accomplished by reading the memory value pointed to by the       ;;
;;          program counter (register 0), and interpreting this memory word     ;;
;;          as an instruction to be executed.  The execution of an instruction  ;;
;;          may modify all visable registers.  The flag registers may be        ;;
;;          updated only once per instruction.  The memory may be updated       ;;
;;          only once per instruction.  The register file may be updated a      ;;
;;          maximum of four times in six opportunities.  The first update to    ;;

;;          the register file, which always occurs, is the incrementing of      ;;
;;          the program counter.  Next comes the possible pre-decrement         ;;
;;          operation of both operands.  The result of the ALU may be next      ;;
;;          stored into the register file.  Lastly, there may be two            ;;
;;          post-increment operations.  An operand cannot be both               ;;
;;          pre-decremented and post-incremented.                               ;;
;;                                                                              ;;
;;          The functions below generate the next state for the memory and      ;;
;;          the register file given an instruction.  These are grouped          ;;
;;          together into an interpreter called SOFT.  SOFT executed one        ;;
;;          instruction per recursive call.                                     ;;
;;                                                                              ;;
;;          The next state for the register file (REG-FILE) is created by       ;;
;;          the composition of several functions.  Each function describes      ;;
;;          the state of the register file at some point through the execution  ;;
;;          of an instruction.  Below are described the operation of the        ;;
;;          functions that update the register file.  All of these functions    ;;
;;          return a complete register file, which they may or may not of       ;;
;;          updated.                                                            ;;
;;                                                                              ;;
;;          reg-file-after-pc-increment --                                      ;;
;;               increments the PC (register 0)                                 ;;
;;                                                                              ;;
;;          reg-file-after-oprd-a-pre-decrement --                              ;;
;;               performs a pre-decrement operation for operand A if required,  ;;
;;               and included is the reg-file-after-pc-increment operation      ;;
;;                                                                              ;;
;;          reg-file-after-oprd-b-pre-decrement --                              ;;
;;               performs a pre-decrement operation for operand B if required,  ;;
;;               and included is the reg-file-after-oprd-a-pre-decrement        ;;
;;               operation                                                      ;;
;;                                                                              ;;
;;          reg-file-after-alu-write --                                         ;;
;;               writes the output of the ALU to the reg-file if required,      ;;
;;               and included is the reg-file-after-oprd-b-pre-decrement        ;;
;;               operation                                                      ;;
;;                                                                              ;;
;;          reg-file-after-oprd-a-post-increment --                             ;;
;;               performs a post-increment operation for operand A if required, ;;
;;               and included is the reg-file-after-alu-write operation         ;;
;;                                                                              ;;
;;          reg-file-after-oprd-b-post-increment --                             ;;
;;               performs a post-increment operation for operand B if required, ;;
;;               and included is the reg-file-after-oprd-a-post-increment       ;;

;;               operation                                                      ;;
;;                                                                              ;;
;;          The ALU requires three operands so its result can be calculated.    ;;
;;          The C-FLAG is readily available, but the A and B value for the      ;;
;;          ALU must be generated under instruction control.  The A value is    ;;
;;          fetched either from the register file or the memory, but not until  ;;
;;          both the PC has been incremented and the operand A pre-decrement    ;;
;;          performed.  The function A-VALUE-FOR-ALU-AFTER-OPRD-A-PRE-DECREMENT ;;
;;          generates the appropriate value.  The B value for the ALU is        ;;
;;          fetched from either the register file or memory, but not until the  ;;
;;          PC has been incremented and the possible operand A pre-decrement    ;;
;;          and operand B pre-decrement operations performed.  The function     ;;
;;          B-VALUE-FOR-ALU-AFTER-OPRD-B-PRE-DECREMENT generates the correct    ;;
;;          operand B value.                                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;  This function increments the Program Counter (PC) by one.  The PC is
;  stored in register 0 in the register file.

Definition: reg-file-after-pc-increment (reg-file) = update-nth (t, 0, reg-file, v-nat-inc (nth (0, reg-file)))

;  This function extracts the current instruction from memory.

Definition: current-instruction (reg-file, real-mem) = v-nth (nth (0, reg-file), real-mem)

;  The result of this function are the contents of the register file after
;  the possible pre-decrement for operand A and the increment of PC.

Definition: reg-file-after-oprd-a-pre-decrement (reg-file, real-mem) = update-v-nth (b-indirect-reg-a-dec (current-instruction (reg-file,

real-mem)),

bv-oprd-a (current-instruction (reg-file, real-mem)), reg-file-after-pc-increment (reg-file), v-nat-dec (v-nth (bv-oprd-a (current-instruction (reg-file,

real-mem)),

reg-file-after-pc-increment (reg-file))))

;  The result of this function are the contents of the register file after
;  the possible pre-decrement for operand B, the possible pre-decrement for
;  operand A and the increment of PC.

Definition: reg-file-after-oprd-b-pre-decrement (reg-file, real-mem) = update-v-nth (b-indirect-reg-b-dec (current-instruction (reg-file,

real-mem)),

bv-oprd-b (current-instruction (reg-file, real-mem)), reg-file-after-oprd-a-pre-decrement (reg-file, real-mem), v-nat-dec (v-nth (bv-oprd-b (current-instruction (reg-file,

real-mem)),

reg-file-after-oprd-a-pre-decrement (reg-file, real-mem))))

;  This function returns operand A for use in the ALU after the PC has been
;  incremented and the possible operand A pre-decrement has occured.

Definition: a-value-for-alu-after-oprd-a-pre-decrement (reg-file, real-mem) = if b-direct-reg-a (current-instruction (reg-file, real-mem))

then v-nth (bv-oprd-a (current-instruction (reg-file, real-mem)), reg-file-after-pc-increment (reg-file))

elseif b-indirect-reg-a-dec (current-instruction (reg-file, real-mem)) then v-nth (v-nat-dec (v-nth (bv-oprd-a (current-instruction (reg-file,

real-mem)),

reg-file-after-pc-increment (reg-file))),

real-mem)

else v-nth (v-nth (bv-oprd-a (current-instruction (reg-file,

real-mem)),

reg-file-after-pc-increment (reg-file)), real-mem) endif

;  This function returns operand B for use in the ALU after the PC has been
;  incremented, the possible operand A pre-decrement has occured, and the
;  possible operand B pre-decrement has occured.

Definition: b-value-for-alu-after-oprd-b-pre-decrement (reg-file, real-mem) = if b-direct-reg-b (current-instruction (reg-file, real-mem))

then v-nth (bv-oprd-b (current-instruction (reg-file, real-mem)), reg-file-after-oprd-a-pre-decrement (reg-file, real-mem)) elseif b-indirect-reg-b-dec (current-instruction (reg-file, real-mem)) then v-nth (v-nat-dec (v-nth (bv-oprd-b (current-instruction (reg-file,

real-mem)),

reg-file-after-oprd-a-pre-decrement (reg-file,

real-mem))),

real-mem)

else v-nth (v-nth (bv-oprd-b (current-instruction (reg-file,

real-mem)),

reg-file-after-oprd-a-pre-decrement (reg-file,

real-mem)),

real-mem) endif

;  This function returns the result of the ALU on operand A, operand B, and
;  the carry flag.

Definition: bv-alu-cv-results (reg-file, real-mem, c-flag) = bv-alu-cv (a-value-for-alu-after-oprd-a-pre-decrement (reg-file,

real-mem),

b-value-for-alu-after-oprd-b-pre-decrement (reg-file,

real-mem),

c-flag,

bv-alu-op-code (current-instruction (reg-file, real-mem)))

;  This function returns the result of a possible storing of the ALU result
;  into the register file.  Note that this function takes into account the
;  possible changes that may have been inflicted on the register file by some
;  pre-decrement operations and the PC increment.

Definition: reg-file-after-alu-write (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag) = update-v-nth (b-store-alu-result-with-ifs (c-flag,

v-flag, z-flag, n-flag, current-instruction (reg-file,

real-mem))

∧ b-direct-reg-b (current-instruction (reg-file,

real-mem)),

bv-oprd-b (current-instruction (reg-file, real-mem)), reg-file-after-oprd-b-pre-decrement (reg-file, real-mem), bv (bv-alu-cv-results (reg-file, real-mem, c-flag)))

;  This function returns the result of a possible storing of the ALU result
;  into the memory.

Definition: real-mem-after-alu-write (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag) = update-v-nth (b-store-alu-result-with-ifs (c-flag,

v-flag, z-flag, n-flag, current-instruction (reg-file,

real-mem))

∧ (¬ b-direct-reg-b (current-instruction (reg-file,

real-mem))),

v-nth (bv-oprd-b (current-instruction (reg-file, real-mem)), reg-file-after-oprd-b-pre-decrement (reg-file,

real-mem)),

real-mem,

bv (bv-alu-cv-results (reg-file, real-mem, c-flag)))

;  This function returns the result of a possible post-increment of operand A
;  after the possible storing of the ALU result, the pre-decrements of A and B,
;  and the PC increment.

Definition: reg-file-after-oprd-a-post-increment (reg-file,

real-mem, c-flag, v-flag, z-flag, n-flag)

= update-v-nth (b-indirect-reg-a-inc (current-instruction (reg-file,

real-mem)),

bv-oprd-a (current-instruction (reg-file, real-mem)), reg-file-after-alu-write (reg-file,

real-mem, c-flag, v-flag, z-flag, n-flag), v-nat-inc (v-nth (bv-oprd-a (current-instruction (reg-file,

real-mem)),

reg-file-after-alu-write (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag))))

;  This function returns the result of a possible post-increment of operand B
;  after the possible post-increment of A, the storing of the ALU result, etc.

Definition: reg-file-after-oprd-b-post-increment (reg-file,

real-mem, c-flag, v-flag, z-flag, n-flag)

= update-v-nth (b-indirect-reg-b-inc (current-instruction (reg-file,

real-mem)),

bv-oprd-b (current-instruction (reg-file, real-mem)), reg-file-after-oprd-a-post-increment (reg-file,

real-mem, c-flag, v-flag, z-flag, n-flag),

v-nat-inc (v-nth (bv-oprd-b (current-instruction (reg-file,

real-mem)),

reg-file-after-oprd-a-post-increment (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Function SOFT is the programmer's interpreter for FM8501.           ;;
;;          This function completely defines the effect of all instructions     ;;
;;          on the programmer visable state.                                    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;  This function returns the result of executing n instructions, where
;  n is the length of lst.

Definition: soft (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag, lst) = if lst ≃ nil then list (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag)

else soft (reg-file-after-oprd-b-post-increment (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag),

real-mem-after-alu-write (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag),

update-v (b-cc-set (current-instruction (reg-file,

real-mem)),

c-flag,

c (bv-alu-cv-results (reg-file, real-mem, c-flag))),

update-v (b-cc-set (current-instruction (reg-file,

real-mem)),

v-flag,

v (bv-alu-cv-results (reg-file, real-mem, c-flag))),

update-v (b-cc-set (current-instruction (reg-file,

real-mem)),

z-flag,

bv-to-nat (bv (bv-alu-cv-results (reg-file, real-mem, c-flag))) ≃ 0),

update-v (b-cc-set (current-instruction (reg-file,

real-mem)),

n-flag,

negativep (bv-to-tc (bv (bv-alu-cv-results (reg-file, real-mem, c-flag))))),

cdr (lst)) endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Function SOFT-RESET specifies what the programmer sees after        ;;
;;          reset has occured.  Note that SOFT-RESET calls the function         ;;
;;          SOFT.  After a reset, the software instruction interpreter is       ;;

;;          is the function SOFT.                                               ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: soft-reset (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag, oracle) = if oracle ≃ nil

then list (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag)

else soft (update-nth (t, 0, reg-file, nat-to-bv (0, machine-size)), real-mem, c-flag, v-flag, z-flag, n-flag, cdr (oracle)) endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          This file contains the events leading up to and including           ;;
;;          the proof that an abstraction, containing the programmer            ;;
;;          visable registers, of BIG-MACHINE is equivalent to SOFT.            ;;
;;          This equivalence is the main result of this work; this result       ;;
;;          proves the correctness of a large piece of hardware with            ;;
;;          respect to a high-level description.                                ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Help lemmas for proving the correctness of "soft-machine"           ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: a-reg-after-a-b-is-a-value-for-alu-after-oprd-a-pre-decrement (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (a-reg-after-a-b (reg-file, real-mem)

= a-value-for-alu-after-oprd-a-pre-decrement (reg-file, real-mem))

Theorem: b-reg-after-a-b-is-b-value-for-alu-after-oprd-b-pre-decrement (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (b-reg-after-a-b (reg-file, real-mem)

= b-value-for-alu-after-oprd-b-pre-decrement (reg-file, real-mem))

Theorem: hard-c-flag-is-soft-c-flag (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size)) ∧ boolp (c-flag)) → (alu-c-flag (nth (bv-to-nat (nth (0, reg-file)), real-mem),

a-value-for-alu-after-oprd-a-pre-decrement (reg-file,

real-mem),

b-value-for-alu-after-oprd-b-pre-decrement (reg-file,

real-mem),

c-flag)

= update-v (b-cc-set (current-instruction (reg-file, real-mem)), c-flag, c (bv-alu-cv-results (reg-file, real-mem, c-flag))))

Theorem: hard-v-flag-is-soft-v-flag (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size)) ∧ boolp (v-flag)) → (alu-v-flag (nth (bv-to-nat (nth (0, reg-file)), real-mem),

a-value-for-alu-after-oprd-a-pre-decrement (reg-file,

real-mem),

b-value-for-alu-after-oprd-b-pre-decrement (reg-file,

real-mem),

c-flag, v-flag)

= update-v (b-cc-set (current-instruction (reg-file, real-mem)), v-flag, v (bv-alu-cv-results (reg-file, real-mem, c-flag))))

Theorem: hard-z-flag-is-soft-z-flag (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size)) ∧ boolp (z-flag)) → (alu-z-flag (nth (bv-to-nat (nth (0, reg-file)), real-mem),

a-value-for-alu-after-oprd-a-pre-decrement (reg-file,

real-mem),

b-value-for-alu-after-oprd-b-pre-decrement (reg-file,

real-mem),

c-flag,

z-flag)

= update-v (b-cc-set (current-instruction (reg-file, real-mem)), z-flag, bv-to-nat (bv (bv-alu-cv-results (reg-file,

real-mem, c-flag))) ≃ 0))

Theorem: sizep-a-value-for-alu-after-oprd-a-pre-decrement (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (size (a-value-for-alu-after-oprd-a-pre-decrement (reg-file, real-mem))

= machine-size)

Theorem: hard-n-flag-is-soft-n-flag (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size)) ∧ boolp (n-flag)) → (alu-n-flag (nth (bv-to-nat (nth (0, reg-file)), real-mem),

a-value-for-alu-after-oprd-a-pre-decrement (reg-file,

real-mem),

b-value-for-alu-after-oprd-b-pre-decrement (reg-file,

real-mem),

c-flag, n-flag)

= update-v (b-cc-set (current-instruction (reg-file, real-mem)), n-flag, negativep (bv-to-tc (bv (bv-alu-cv-results (reg-file,

real-mem, c-flag))))))

Theorem: addr-out-after-a-b-is-v-nth-of-reg-file-after-oprd-b-pre-decrement (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (addr-out-after-a-b (reg-file, real-mem)

= v-nth (bv-oprd-b (current-instruction (reg-file, real-mem)), reg-file-after-oprd-b-pre-decrement (reg-file, real-mem)))

Theorem: hard-real-mem-is-soft-real-mem (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (real-mem-thru-post-inc (nth (bv-to-nat (nth (0, reg-file)), real-mem),

c-flag, v-flag, z-flag, n-flag, nth (bv-to-nat (bv-oprd-b (current-instruction (reg-file,

real-mem))),

reg-file-after-oprd-b-pre-decrement (reg-file,

real-mem)),

real-mem, a-value-for-alu-after-oprd-a-pre-decrement (reg-file,

real-mem),

b-value-for-alu-after-oprd-b-pre-decrement (reg-file,

real-mem))

= real-mem-after-alu-write (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag))

Theorem: reg-file-after-a-b-is-reg-file-after-oprd-b-pre-decrement (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (reg-file-after-a-b (reg-file, real-mem)

= reg-file-after-oprd-b-pre-decrement (reg-file, real-mem))

Theorem: hard-reg-file-is-soft-reg-file (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (reg-file-from-alu-thru-post-inc (nth (bv-to-nat (nth (0, reg-file)),

real-mem), c-flag, v-flag, z-flag, n-flag, reg-file-after-oprd-b-pre-decrement (reg-file,

real-mem),

a-value-for-alu-after-oprd-a-pre-decrement (reg-file,

real-mem),

b-value-for-alu-after-oprd-b-pre-decrement (reg-file,

real-mem))

= reg-file-after-oprd-b-post-increment (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;                                                                              ;;
;;          Oracle generation function for BIG-MACHINE given the oracle         ;;
;;          for SOFT.  The SOFT machine oracle is a list, each element of       ;;
;;          the list contains four arbitrary values.  This values are "fixed"   ;;
;;          into numbers and used to construct a BIG-MACHINE oracle.  These     ;;
;;          four-tuples describe the possible delay when BIG-MACHINE accesses   ;;
;;          memory.  The values are the number of waits to be inserted in       ;;
;;          memory accesses.  The four-tuples meaning is as follows:            ;;
;;                                                                              ;;
;;          (ir-wait fetch-oprd-a-wait fetch-oprd-b-wait store-oprd-b-wait)     ;;
;;                                                                              ;;
;;          ir-wait -- number of wait states for fetching an instruction        ;;
;;          fetch-oprd-a-wait -- number of wait states for fetching OPERAND-A   ;;
;;          fetch-oprd-b-wait -- number of wait states for fetching OPERAND-B   ;;
;;          store-oprd-b-wait -- number of wait states for storing OPERAND-B    ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: oracle (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag, lst) = if lst ≃ nil then nil

else append (state-1-to-1-oracle (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag, car (car (lst)), cadr (car (lst)), caddr (car (lst)), cadddr (car (lst))),

oracle (reg-file-after-oprd-b-post-increment (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag),

real-mem-after-alu-write (reg-file, real-mem, c-flag, v-flag, z-flag,

n-flag),

update-v (b-cc-set (current-instruction (reg-file,

real-mem)),

c-flag,

c (bv-alu-cv-results (reg-file, real-mem, c-flag))),

update-v (b-cc-set (current-instruction (reg-file,

real-mem)),

v-flag,

v (bv-alu-cv-results (reg-file, real-mem, c-flag))),

update-v (b-cc-set (current-instruction (reg-file,

real-mem)),

z-flag,

bv-to-nat (bv (bv-alu-cv-results (reg-file, real-mem, c-flag))) ≃ 0),

update-v (b-cc-set (current-instruction (reg-file,

real-mem)),

n-flag,

negativep (bv-to-tc (bv (bv-alu-cv-results (reg-file, real-mem, c-flag))))),

cdr (lst))) endif

Definition: big-machine-induction (no-store,

data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog, lst)

= if lst ≃ nil then t else big-machine-induction (¬ b-store-alu-result (c-flag,

v-flag, z-flag, n-flag, v-nth (nth (0,

reg-file), real-mem)),

bv (bv-alu-cv (a-reg-after-a-b (reg-file,

real-mem),

b-reg-after-a-b (reg-file,

real-mem),

c-flag, bv-alu-op-code (v-nth (nth (0,

reg-file), real-mem)))),

reg-file-from-alu-thru-post-inc (v-nth (nth (0,

reg-file), real-mem),

c-flag, v-flag, z-flag, n-flag, reg-file-after-a-b (reg-file,

real-mem),

a-reg-after-a-b (reg-file,

real-mem),

b-reg-after-a-b (reg-file,

real-mem)),

addr-out-after-a-b (reg-file, real-mem), alu-c-flag (v-nth (nth (0, reg-file),

real-mem), a-reg-after-a-b (reg-file,

real-mem),

b-reg-after-a-b (reg-file,

real-mem),

c-flag),

alu-v-flag (v-nth (nth (0, reg-file),

real-mem), a-reg-after-a-b (reg-file,

real-mem),

b-reg-after-a-b (reg-file,

real-mem),

c-flag, v-flag), alu-z-flag (v-nth (nth (0, reg-file),

real-mem), a-reg-after-a-b (reg-file,

real-mem),

b-reg-after-a-b (reg-file,

real-mem),

c-flag, z-flag),

alu-n-flag (v-nth (nth (0, reg-file),

real-mem), a-reg-after-a-b (reg-file,

real-mem),

b-reg-after-a-b (reg-file,

real-mem),

c-flag, n-flag),

a-reg-after-a-b (reg-file, real-mem), b-reg-after-a-b (reg-file, real-mem), v-nth (nth (0, reg-file), real-mem), trunc (default-visual-mem-value, 16), real-mem-thru-post-inc (v-nth (nth (0,

reg-file), real-mem),

c-flag, v-flag, z-flag, n-flag, addr-out-after-a-b (reg-file,

real-mem),

real-mem,

a-reg-after-a-b (reg-file,

real-mem),

b-reg-after-a-b (reg-file,

real-mem)),

watch-dog (f, f, f, bv (bv-alu-cv (a-reg-after-a-b (reg-file,

real-mem),

b-reg-after-a-b (reg-file,

real-mem),

c-flag,

bv-alu-op-code (v-nth (nth (0, reg-file),

real-mem)))),

addr-out-after-a-b (reg-file,

real-mem)),

cdr (lst)) endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Abstraction for looking at certian registers in BIG-MACHINE.        ;;
;;          Specifically, the definition below allows us to view the registers  ;;
;;          REG-FILE, REAL-MEM, C-FLAG, V-FLAG, Z-FLAG, and N-FLAG, which       ;;
;;          are the registers used in SOFT machine.                             ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: abstract (m) = list (cadddddddr (m),

cadddddddddddddddddr (m), cadddddddddr (m), caddddddddddr (m), cadddddddddddr (m), caddddddddddddr (m))

; n-flag

Theorem: abstract-list (abstract (list (mar,

read, write, dtack, reset, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog))

= list (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag)) = t

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          The following lemmas ensure SOFT machine does not change the        ;;
;;          size of any registers.                                              ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: ramp-reg-file-after-oprd-a-pre-decrement ((m = machine-size) ∧ ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (every-member-sizep (reg-file-after-oprd-a-pre-decrement (reg-file,

real-mem),

m)

∧ (length (reg-file-after-oprd-a-pre-decrement (reg-file, real-mem)) = 8))

Theorem: ramp-reg-file-after-oprd-b-pre-decrement ((m = machine-size) ∧ ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (every-member-sizep (reg-file-after-oprd-b-pre-decrement (reg-file,

real-mem),

m)

∧ (length (reg-file-after-oprd-b-pre-decrement (reg-file, real-mem)) = 8))

Theorem: size-bv-alu-cv-results size (bv (bv-alu-cv-results (reg-file, real-mem, c-flag))) = size (a-value-for-alu-after-oprd-a-pre-decrement (reg-file, real-mem))

Theorem: ramp-reg-file-after-oprd-b-post-increment ((m = machine-size) ∧ ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → ramp (reg-file-after-oprd-b-post-increment (reg-file,

real-mem, c-flag, v-flag, z-flag, n-flag),

m,

          8)

Theorem: sizep-b-value-for-alu-after-oprd-b-pre-decrement (ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → (size (b-value-for-alu-after-oprd-b-pre-decrement (reg-file, real-mem))

= machine-size)

Theorem: ramp-real-mem-after-alu-write ((m = machine-size) ∧ (x = exp (2, machine-size)) ∧ ramp (reg-file, machine-size, 8) ∧ ramp (real-mem, machine-size, exp (2, machine-size))) → ramp (real-mem-after-alu-write (reg-file,

real-mem, c-flag, v-flag, z-flag, n-flag),

m, x)

Theorem: size-nth (ramp (lst, 16, n) ∧ (i < n)) → (size (nth (i, lst)) = 16)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          The proof of equivalence between the hardware definition of         ;;
;;          FM8501 and the software definition of FM8501.  This lemma proves    ;;
;;          that BIG-MACHINE executes instructions in the same way as the       ;;
;;          interpreter SOFT.                                                   ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: big-machine-is-soft-machine ((mar1 = nat-to-bv (1, nxsz)) ∧ standard-hyps (mar1 ,

f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem))

→ (abstract (big-machine (mar1 , f, f, f, f, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, watch-dog, oracle (reg-file,

real-mem, c-flag, v-flag, z-flag, n-flag, lst)))

= soft (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag, lst))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          The following events are concerning with the programmer's view      ;;
;;          of FM8501 during a reset operation.                                 ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: oracle-reset (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag, lst) = if lst ≃ nil then nil

else append (state-0-to-0-wait-to-1-oracle (car (car (lst))),

oracle (update-nth (t,

                               0,

reg-file,

nat-to-bv (0, machine-size)),

real-mem, c-flag, v-flag, z-flag, n-flag, cdr (lst))) endif

Theorem: ramp-reg-file-after-reset (ramp (reg-file, machine-size, 8) ∧ (m = machine-size)) → ramp (update-nth (t, 0, reg-file, nat-to-bv (0, m)), m, 8)

Theorem: sizep-trunc-at-machine-size (m = machine-size) → sizep (trunc (x, m), m)

;  Proof that reseting FM8501 sets register 0 to zero.

Theorem: soft-reset-works ((mar0 = nat-to-bv (0, nxsz)) ∧ standard-hyps (mar0 ,

f, f, dtack, t, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem))

→ (abstract (big-machine (mar0 , f, f, dtack, t, no-store, data-out, reg-file, addr-out, c-flag, v-flag, z-flag, n-flag, a-reg, b-reg, i-reg, visual-mem, real-mem, memory-watch-dog-history, oracle-reset (reg-file,

real-mem, c-flag, v-flag, z-flag, n-flag, lst)))

= soft-reset (reg-file, real-mem, c-flag, v-flag, z-flag, n-flag, lst))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                              ;;
;;          Flag interpretation lemmas                                          ;;
;;                                                                              ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Event: Disable bv-alu-cv-results.

Theorem: bit-vector-interpretation-of-z-flag (bv-to-nat (bv (bv-alu-cv-results (reg-file, real-mem, c-flag))) ≃ 0) = v-zerop (bv (bv-alu-cv-results (reg-file, real-mem, c-flag)))

Theorem: integer-interpretation-of-z-flag (bv-to-nat (bv (bv-alu-cv-results (reg-file, real-mem, c-flag))) ≃ 0) = (0 = bv-to-tc (bv (bv-alu-cv-results (reg-file, real-mem, c-flag))))

Theorem: bit-vector-interpretation-of-n-flag negativep (bv-to-tc (bv (bv-alu-cv-results (reg-file, real-mem, c-flag)))) = bitn (bv (bv-alu-cv-results (reg-file, real-mem, c-flag)),

size (bv (bv-alu-cv-results (reg-file, real-mem, c-flag))))

Index

a-b-oracle, 142, 143, 148 a-reg, 65, 69, 72 a-reg-after-a-b, 141, 143, 148–151,

159, 165, 166 a-reg-after-a-b-is-a-value-for-

alu-after-oprd-a-pre-decrement,

159 a-value-for-alu-after-oprd-a-pre

-decrement, 154, 155, 159–162,

168 abstract, 167, 168, 170, 172 abstract-list, 167 add, 12, 13, 16, 20–22, 24–27, 42–46 add-0, 25 add-1-1, 25 add-with-carry-of-negatives-is-

negative, 12 add-with-carry-of-non-negatives

-is-non-negative, 13 add1-difference-sub1, 30 addr-out, 62, 69, 72 addr-out-1, 66, 67 addr-out-after-a-b, 140, 143, 148, 150,

151, 161, 165–167 addr-out-after-a-b-is-v-nth-of-

reg-file-after-oprd-b-pre-decrement,

161 all-onesp, 10, 15 all-onesp-of-compl, 15 all-zerosp, 10 alu-c-flag, 120, 121, 130–132, 135,

147, 150, 160, 165 alu-correct-twos-complement, 44 alu-n-flag, 120, 121, 130–132, 135,

147, 150, 161, 166 alu-oracle, 133, 134, 145 alu-post-inc-oracle, 145, 146, 148 alu-v-flag, 120, 121, 130–132, 135,

147, 150, 160, 165 alu-z-flag, 120, 121, 130–132, 135,

147, 150, 161, 166 append, 47 assoc-of-append, 47 associativity-of-add, 12 associativity-of-plus, 2 associativity-of-times, 3

b-and, 8, 11, 17, 18, 50, 52, 53, 59–

64 b-bv-nzerop, 49 b-bv-zerop, 49, 64, 120 b-bv-zerop-equal-v-zerop, 49 b-cc-set, 52, 63, 64, 120, 158, 160,

161, 164 b-direct-reg-a, 52, 59, 65, 95–101,

103–106, 141, 154 b-direct-reg-b, 52, 59, 61, 65, 108–

112, 114–119, 122–126, 128– 130, 132–135, 141–143, 145, 154–156

b-dout-incdec, 55, 62 b-en-no-store, 55, 59 b-equv, 8, 18, 50 b-force-inc, 55, 61, 62 b-if, 30, 31, 58, 59, 61, 62 b-if-works, 58 b-indirect-reg-a, 52 b-indirect-reg-a-dec, 52, 61, 62, 93,

94, 153, 154 b-indirect-reg-a-inc, 52, 61, 62, 136,

138, 144, 156 b-indirect-reg-b, 52 b-indirect-reg-b-dec, 52, 61, 62, 107,

154, 155 b-indirect-reg-b-inc, 52, 62, 138, 144,

157 b-ir-mem-ref, 55, 59, 60 b-move-op, 52, 53 b-nand, 7, 30 b-nor, 8, 52 b-not, 7, 11, 22, 25, 30, 49, 52, 53,

59–61 b-oprd-mem-ref, 59, 60 b-oprd-mem-ref-ifs, 59 b-oprd-mem-ref-with-ifs, 59 b-oprda-oprdb, 55, 59, 61, 62 b-or, 8, 11, 18, 49, 53, 59–62 b-pc-regnum, 55, 59, 61 b-postinc, 55, 61 b-predec, 55, 61, 62 b-rd, 56, 60 b-reg, 65, 69, 72 b-reg-after-a-b, 141, 143, 149–151,

160, 165, 166 b-reg-after-a-b-is-b-value-for-

alu-after-oprd-b-pre-decrement,

160 b-seq, 56, 59 b-store-alu-result, 53, 54, 60, 121,

129–135, 143, 145, 146, 149, 165

b-store-alu-result-ifs, 54 b-store-alu-result-with-ifs, 53, 54, 60,

155, 156 b-value-for-alu-after-oprd-b-pre

-decrement, 154, 155, 160–162,

169 b-we-a-reg, 56, 65 b-we-addr-out, 56, 62 b-we-alu-result, 56, 60, 61, 63, 64 b-we-b-reg, 56, 65 b-we-ir, 56, 65 b-wr, 56, 60, 61 b-xor, 8, 12, 17, 18 big-machine, 67–71, 73–75, 77–82,

84–92, 94, 96–104, 106, 108– 117, 119, 121–129, 131, 132, 134, 136, 137, 139, 143, 146, 149, 170, 172

big-machine-append, 73 big-machine-induction, 164, 167 big-machine-is-soft-machine, 169 bit, 8–12, 14, 17, 18, 28, 30, 39, 49,

50 bit-interpretation-of-even-and-

odd, 39 bit-vector-interpretation-of-n-

flag, 173 bit-vector-interpretation-of-z-

flag, 173 bitn, 9, 14–18, 24, 28, 29, 33–39, 50,

52, 53, 55, 56, 64, 120, 173 bitn-compl, 24 bitn-equiv-lessp, 38 bitn-implies-compl-not-all-onesp, 15 bitn-means-negativep, 16 bitn-on-implies-non-0, 17 bitn-v-append, 29 bitv, 8–12, 14, 17, 18, 28, 30–32, 37, 39, 52, 54, 56 bitvp, 8–11, 14, 15, 17–21, 23–32,

35, 37–44, 49, 50, 58, 75, 76 bitvp-v-append, 29 boolp, 8, 18–27, 37, 38, 40, 44, 57,

58, 120, 121, 129–134, 145, 146, 148, 160, 161

boolp-alu-c-flag, 120 boolp-alu-n-flag, 120 boolp-alu-v-flag, 120 boolp-alu-z-flag, 120 boolp-b-not, 25 boolp-bit, 8 btm, 8–12, 14, 15, 17, 18, 20–22, 24–

32, 37, 39, 42–44, 49, 50, 52, 54, 56, 76

btmp, 9, 10

bv, 31, 38–41, 44–47, 61, 64, 120, 121, 129–135, 143, 145–147, 150, 151, 155, 156, 158, 161, 164, 165, 167, 168, 173

bv-adder, 17, 18, 20, 37 bv-adder-as-shifter, 37 bv-adder-carry-out, 18, 19, 22, 34–

39 bv-adder-carry-out-used-as-asl, 38 bv-adder-non-btm, 18 bv-adder-output, 18–22, 34, 36, 37, 39, 42, 62, 75 bv-adder-output-used-as-asl, 37 bv-adder-overflowp, 18, 22, 34–37,

43 bv-alu-cv, 33, 35, 38–41, 44–47, 61,

63, 64, 120, 121, 129–135, 143, 145–147, 150, 151, 155, 165, 167

bv-alu-cv-correct-boolean, 38 bv-alu-cv-correct-natural-numbe

r, 40 bv-alu-cv-results, 155, 156, 158, 160,

161, 164, 168, 173 bv-alu-cv-with-ifs, 35 bv-alu-op-code, 53, 61, 63, 64, 120,

121, 129–135, 143, 145–147, 150, 151, 155, 165, 167

bv-and, 11, 33, 35 bv-and-is-v-and, 35 bv-append, 28 bv-asr, 28, 30, 33, 36, 42 bv-asr-divides-by-two, 30 bv-asr-divides-by-two-bridge, 42 bv-cv, 30, 31, 33–38, 40 bv-cv-if, 31, 33–35 bv-cv-if-reduce, 35 bv-cv-if-works, 31 bv-cvp, 31 bv-decrementer-truncates-to-mac

hine-size, 75 hine-size-help, 75

bv-equal, 50, 53 bv-equal-is-equal, 50 bv-if, 30, 31, 53, 59, 62, 65 bv-if-works, 30 bv-incrementer-truncates-to-mac

hine-size, 75 bv-lsr, 28, 33, 36 bv-lsr-divides-by-two-lemma, 29 bv-next, 56, 59 bv-not, 11, 22, 33, 35 bv-not-is-compl, 22 bv-op-code, 52–54 bv-oprd-a, 52, 59, 93, 94, 97, 103,

106, 137, 138, 141, 144, 153, 154, 156 bv-oprd-b, 52, 59, 93, 107, 110, 116,

119, 123, 129, 134, 138, 141, 143, 144, 154–157, 161, 162

bv-or, 11, 33, 35 bv-or-is-v-or, 35 bv-reg-select, 59, 62, 65, 93 bv-reg-select-ifs, 59 bv-reg-select-with-ifs, 59 bv-ror, 29, 33, 36 bv-subtracter-carry-out, 22, 24, 33,

34, 36 bv-subtracter-output, 22, 23, 25, 26,

33, 34, 36, 42, 43, 62, 75 bv-subtracter-overflowp, 22, 27, 33,

34, 36, 43 bv-to-nat, 14–20, 22–24, 29, 37–41,

47–49, 75, 88, 158, 160–162, 164, 173

bv-to-nat-of-bv-adder, 18 bv-to-nat-of-compl, 15 bv-to-nat-of-incr, 15 bv-to-nat-of-trunc, 15 bv-to-nat-of-twos-compl, 29 bv-to-nat-to-bv, 16 bv-to-nat-to-tc, 16 bv-to-nat-to-tc-lemma1, 15 bv-to-nat-to-tc-lemma2, 15 bv-to-nat-v-append, 29 bv-to-tc, 14–17, 20–22, 24–27, 30,

41–46, 49, 50, 158, 161, 164, 173

bv-to-tc-compl-0, 25 bv-to-tc-to-bv, 17 bv-to-tc-to-bv-of-zero-is-zero, 42 bv-to-tc-to-nat, 17 bv-xor, 11, 12, 33, 35 bv-xor-is-v-xor, 35

c, 31, 38–41, 63, 120, 158, 160, 164 c-flag, 63, 69 c-flag-ifs, 63 c-flag-with-ifs, 63, 72 car-if, 140 carry, 9, 12, 13, 16, 18–27, 37, 40,

41, 44–46 cdr-if, 140 commutativity-of-add, 12 commutativity-of-plus, 2 commutativity-of-times, 3 commutativity2-of-add, 12 commutativity2-of-plus, 2 commutativity2-of-times, 3 compl, 9, 10, 14, 15, 17, 22, 24, 25,

29, 35, 41 compl-not-btm, 25 current-instruction, 153–158, 160–162,

164

data-out, 61, 68 data-out-ifs, 61 data-out-with-ifs, 61, 72 default-visual-mem-value, 66, 79–81,

83, 85–88, 95–100, 103, 106, 108–113, 117, 119, 121, 123– 128, 130, 131, 133, 135, 137– 139, 142, 147, 150, 166

difference-2, 4 difference-2x-x, 29 difference-add1, 5 difference-crock1, 4 difference-difference, 5 difference-elim, 4 difference-plus, 4 difference-plus-cancellation, 4 difference-x-x, 4 difference-x-x-1, 29 distributivity-of-times-over-pl

us, 2 dtack, 60, 68, 69, 71–73 dtack-1-oracle, 66, 67 dtack-after-a-b, 142, 143

embed-in-nat-to-bv, 17 embed-in-tc-to-bv, 17 equal-bools, 3 equal-difference-0, 24 equal-lessp-hack, 23 equal-times-0, 3 every-member-sizep, 51, 58, 76, 93, 94, 105, 107, 168 every-member-sizep-implies-bitvp, 58

-machine-size, 58 every-member-sizep-implies-size

-nth, 51 -nth-0, 51 -nth-machine-size, 51 every-member-sizep-update-nth, 93 every-member-sizep-update-nth-m

achine-size, 105 exp, 3, 4, 6, 12–16, 19–27, 29, 37–47,

57, 58, 88–90, 92, 105, 118, 142, 148, 159–162, 168, 169

exp-2-never-0, 4 exp-by-0, 4 exp-of-0, 4 exp-of-1, 4 exp-plus, 3 exp-times, 4

fetch-ir-oracle, 91, 92, 142

fetch-oprd-a-addr-out, 94, 95, 103, 104, 106, 141 fetch-oprd-a-oracle, 105, 106, 142 fetch-oprd-a-reg-file, 93–95, 103, 106,

140–142 fetch-oprd-b-addr-out, 107, 108, 116, 117, 119, 141, 142 fetch-oprd-b-oracle, 118, 119, 142 fetch-oprd-b-reg-file, 107, 108, 116, 119, 140, 141 fix-bool, 47, 60, 78, 79, 81 fix-bv, 8, 10, 16, 17

hard-c-flag-is-soft-c-flag, 160 hard-n-flag-is-soft-n-flag, 161 hard-real-mem-is-soft-real-mem, 161 hard-reg-file-is-soft-reg-file, 162 hard-v-flag-is-soft-v-flag, 160 hard-z-flag-is-soft-z-flag, 160

i-reg, 65, 69 i-reg-ifs, 65 i-reg-with-ifs, 65, 72 incr, 9, 10, 14, 15, 17, 29, 41 incr-compl-nat-to-bv-0, 17 incr-f-noop, 10 integer-interpretation-of-z-fla

g, 173

length, 47, 48, 51, 58, 76, 94, 107,

151, 168 length-0, 47 length-update-nth, 48 length-update-v-nth, 48 lessp-crock1, 3 lessp-difference, 5 lessp-remainder, 5 lessp-times, 3 list-of-n-plus-1-dtack-off-reset

-on, 78, 80, 81 list-of-n-plus-1-dtack-reset-of

f, 86, 88, 92, 100, 105, 113, 118,

127, 132, 133 listp-reg-file, 76 listp-update-nth, 48 listp-update-v-nth, 49 lower-bound-on-negative-bv-to-n

at, 15

machine-size, 50, 51, 57, 58, 62, 64, 66, 75, 76, 78–81, 83, 84, 87–90, 92, 94–96, 99–102, 104, 105, 107–109, 112, 114– 118, 120–122, 126, 127, 129, 130, 132, 134, 136–138, 142, 146, 148, 159–162, 168, 169, 171

make-micro-rom, 54, 55 make-micro-word, 54 mar, 59, 68, 71, 76 mar-on-reset, 76 mem-store-flag, 133–135, 145 micro-rom, 55, 59–65 micro-store, 54, 55, 57 mod2, 29, 30, 42, 44 n-flag, 64, 69 n-flag-equals-negativep, 50 n-flag-ifs, 64 n-flag-with-ifs, 64, 72 nat-bv-adder-output-seen-as-bit

-vector, 19 nat-bv-subtracter-output-seen-a

s-bit-vector, 23 nat-interpretation-of-bv-adder-

carry-out, 19 output, 19

nat-interpretation-of-bv-subtra cter-carry-out, 24 cter-output, 23

nat-interpretation-of-inc-bit-ve

ctor, 39 nat-interpretation-of-inc-carry

-out, 39 nat-of-zero-is-tc-of-zero, 42 nat-to-bv, 14, 16, 17, 19, 23, 29, 34–

48, 53, 54, 59, 62, 75–92, 94–132, 134, 136–139, 142, 143, 146, 149, 159, 169, 171

nat-to-bv-ignores-remainder, 37 nat-to-bv-of-2i, 37 nat-to-bv-to-nat, 16 nat-to-bv-to-nat-hidden-to-acco modate-hands-off, 39 nat-to-bv-to-nat-wrong-size, 37 nat-to-tc, 14, 16, 20 no-store, 60, 61, 68 no-store-ifs, 61 no-store-with-ifs, 60, 61, 72 nth, 48, 51, 58, 78, 84, 92, 93, 140–

143, 148–151, 153, 160–162, 165, 166, 169

nth-update-nth, 151

nxsz, 50, 54, 56, 57, 59, 76–92, 94– 132, 134, 136–139, 142, 143, 146, 149, 169, 171

open-big-machine-on-listp, 71 open-big-machine-on-nlistp, 70 opposite-signs-implies-tc-in-ra ngep, 13 ngep-commuted, 13

oracle, 163, 164, 170, 171 oracle-reset, 171, 172 overflow-lemma1, 13 overflow-lemma2, 13

pathological-difference, 4 plus-1, 2 plus-add1, 2 plus-cancellation, 2 plus-equal-0, 2 plus-right-id, 2 plus-to-add, 16 properp, 47

quotient-2i-by-2, 7 quotient-add1-times, 6 quotient-crock1, 30 quotient-crock2, 30 quotient-plus-times, 6 quotient-plus-times-commuted, 6 quotient-times, 6

ramp, 51, 57, 58, 84, 88–90, 92, 94– 96, 100–102, 104, 105, 107– 109, 114–118, 122, 129, 134, 136–138, 142, 145, 146, 148, 159–162, 168, 169, 171

ramp-fetch-oprd-a-reg-file, 94 ramp-fetch-oprd-a-reg-file-2, 94 ramp-fetch-oprd-b-reg-file, 107 ramp-fetch-oprd-b-reg-file-2, 107 ramp-if, 145 ramp-real-mem-after-alu-write, 169 ramp-reg-file-after-a-b, 148 ramp-reg-file-after-oprd-a-pre-

decrement, 168 ramp-reg-file-after-oprd-b-post

-increment, 168 ramp-reg-file-after-oprd-b-pre-

decrement, 168 ramp-reg-file-after-reset, 171 ramp-update-nth, 145 read, 60, 68, 71 read-1, 66, 67 real-mem, 66, 67, 69, 73 real-mem-after-alu-write, 156, 158,

162, 164, 169 real-mem-thru-post-inc, 145, 147, 151,

162, 166 reg-file, 61, 69, 72, 76 reg-file-after-a-b, 140, 143, 148, 150,

162, 165 reg-file-after-a-b-is-reg-file-

after-oprd-b-pre-decrement, 162 reg-file-after-alu-write, 155–157 reg-file-after-oprd-a-post-incre

ment, 156, 157 reg-file-after-oprd-a-pre-decre

ment, 153–155, 168 reg-file-after-oprd-b-post-incre

ment, 157, 158, 162, 163, 169 reg-file-after-oprd-b-pre-decre

ment, 154–156, 161, 162, 168 reg-file-after-pc-increment, 153, 154 reg-file-alu, 143–145 reg-file-from-alu-thru-post-inc, 144,

147, 150, 162, 165 reg-file-on-reset, 76 reg-file-post-inc, 138, 139 remainder-2i-by-2, 7 remainder-add1-times, 6 remainder-by-1, 5 remainder-by-nonnumber, 5 remainder-crock1, 6 remainder-crock2, 6 remainder-crock3, 7 remainder-crock4, 7 remainder-of-0, 7 remainder-of-1, 6 remainder-plus, 5 remainder-plus-times, 5 remainder-plus-times-commuted, 5 remainder-quotient, 5 remainder-quotient-elim, 5 remainder-times, 5 remainder-x-x, 5 reset, 60, 68, 69, 71–73 reset-to-state-0, 77 right-bv-next-size, 56 romp, 51, 57

size, 9, 10, 14–48, 50, 51, 56, 58, 75, 76, 88, 93, 94, 105, 107, 148, 161, 168, 169, 173

size-0, 10 size-bv-adder-output, 18 size-bv-alu-cv-results, 168 size-bv-bv-alu-cv, 47 size-bv-bv-cv-if, 31 size-bv-next-micro-rom-lemma, 56 size-bv-oprd-a, 93 size-bv-oprd-b, 93 size-bv-reg-select, 93 size-bv-subtracter-output, 23 size-nth, 169 size-of-bv-adder, 18 size-of-compl, 10 size-of-incr, 10 size-of-nat-to-bv, 14 size-of-tc-to-bv, 15 size-of-trunc, 10 size-of-v-asr, 41 size-v-and, 31 size-v-append, 29 size-v-append-1, 31 size-v-append-2, 32 size-v-nat-dec, 48 size-v-nat-inc, 48 size-v-not, 31 size-v-nth, 76 size-v-or, 31 size-v-xor, 31 sizep, 51, 57, 58, 88–90, 92, 100,

101, 104, 105, 114, 115, 117, 118, 121, 122, 127, 129, 130, 132, 134, 142, 145, 146, 148, 171

sizep-a-reg-after-a-b, 148 sizep-a-value-for-alu-after-opr

d-a-pre-decrement, 161 sizep-addr-out-after-a-b, 148 sizep-b-value-for-alu-after-opr

d-b-pre-decrement, 169 sizep-fetch-oprd-a-addr-out, 94 sizep-fetch-oprd-b-addr-out, 107 sizep-implies-bitvp, 58 sizep-trunc-at-machine-size, 171 soft, 158, 159, 170 soft-reset, 159, 172 soft-reset-works, 171 standard-hyps, 57, 77, 82, 170, 172 state-0-to-0-induction, 79 state-0-to-0-wait, 79 state-0-to-0-wait-help, 78 state-0-to-0-wait-to-1, 82 state-0-to-0-wait-to-1-oracle, 81, 82,

171 state-0-to-1, 80 state-1-to-1, 148 state-1-to-1-oracle, 148, 149, 163 state-1-to-10, 142 state-1-to-2, 84 state-1-to-4, 92 state-10-to-1, 146 state-10-to-11, 120 state-10-to-12, 133 state-10-to-12-mem-no-store, 130 state-10-to-12-mem-store, 131 state-10-to-12-reg, 129 state-11-to-11-induction, 126 state-11-to-12-mem-dtack-store, 127 state-11-to-12-mem-help, 125 state-11-to-12-mem-init-store, 124 state-11-to-12-mem-no-store, 123 state-11-to-12-mem-wait-store, 126 state-11-to-12-reg, 122 state-12-to-1, 138 state-12-to-13, 136 state-13-to-1, 137 state-2-to-2-induction, 87 state-2-to-2-wait-help, 86 state-2-to-3-init, 85 state-2-to-3-step3, 88 state-2-to-3-step3-to-4, 90 state-2-to-3-wait, 87 state-3-to-4, 89 state-4-to-5, 94 state-4-to-5-to-6-to-7-reg, 102 state-4-to-7, 105 state-5-to-6-mem-dtack, 100 state-5-to-6-mem-help, 98 state-5-to-6-mem-init, 97 state-5-to-6-mem-wait, 99 state-5-to-6-reg, 95 state-5-to-6-to-7-mem-dtack, 104 state-6-to-7-mem, 101 state-6-to-7-reg, 96 state-7-to-10, 118 state-7-to-8, 107 state-7-to-8-to-9-to-10-reg, 116 state-8-to-9-mem-dtack, 113 state-8-to-9-mem-help, 111 state-8-to-9-mem-init, 110 state-8-to-9-mem-wait, 112 state-8-to-9-reg, 108 state-8-to-9-to-10-mem-dtack, 117 state-9-to-10-mem, 115 state-9-to-10-reg, 109 subtract-lemma1, 22 subtract-lemma2, 22 subtract-lemma3, 22 subtract-lemma4, 23

tc-bv-adder-output-seen-as-bit-ve ctor, 21 ctor-lemma1, 20

tc-bv-subtracter-output-seen-as -bit-vector, 26 -bit-vector-lemma1, 26

tc-fix, 25, 42 tc-fix-of-add, 42 tc-in-rangep, 12, 13, 15, 16, 20–22,

25–27, 42–46 tc-in-rangep-of-bv-to-tc, 15 tc-interpretation-of-bv-adder-o

utput, 20

utput-lemma1, 20 tc-interpretation-of-bv-adder-ove

rflowp, 21 tc-interpretation-of-bv-subtracte

r-output, 25 r-overflowp, 27

tc-interpretation-of-dec-bit-ve

ctor, 42 tc-interpretation-of-dec-overfl

owp, 43 tc-interpretation-of-inc-bit-ve

ctor, 42 tc-interpretation-of-inc-overfl

owp, 43 tc-interpretation-of-negation-o

utput, 43 tc-interpretation-of-negation-ove

rflowp, 43 tc-minus, 24–27, 43–45 tc-minus-add, 24 tc-minus-add-carry, 25 tc-minus-bv-to-tc, 24 tc-to-bv, 14–17, 20, 21, 26, 27, 41–

46 tc-to-bv-is-not-btm-for-non-zer

o-size, 42 tc-to-bv-of-bitv-not-btm, 42 tc-to-bv-to-nat, 16 tc-to-bv-to-tc-negative, 41 tc-to-nat, 14, 16, 17 tcp, 12, 13, 15, 16, 25 tcp-add, 25 tcp-bv-to-tc, 15 times-1, 3 times-2-distributes-over-remain

der-add1, 6 times-2-not-1, 3 times-add1, 2 times-distributes-over-remainde

r, 6 times-zero2, 2 top-bit-off-implies-smaller, 24 trunc, 9, 10, 15, 18, 20, 28, 30, 31,

37, 58, 66, 76, 79–81, 83, 85–88, 95–103, 105, 106, 108– 115, 117–119, 121, 123–128, 130, 131, 133, 135, 137–139, 142, 147, 150, 166, 171

trunc-size, 31 trunc-size-1, 76 trunc-size-bridge, 58 twos-complement-twos-complement,

41

update-nth, 48, 76, 79–81, 83, 84, 92, 93, 105, 133, 140–142, 146, 151, 153, 159, 171

update-nth-f, 133 update-update-nth, 76 update-v, 48, 59–65, 158, 160, 161,

164 update-v-nth, 48, 49, 62, 67, 93, 107,

123, 128, 130, 133, 135, 137, 138, 143–145, 153–157

upper-bound-bridge, 88 upper-bound-on-bv-to-nat, 15 upper-bound-on-non-negative-bv-t

o-nat, 15

v, 31, 44–46, 63, 120, 158, 160, 164 v-and, 11, 31, 35, 38 v-append, 27–29, 31, 32, 39 v-append-quotient, 39 v-asl, 28, 38 v-asr, 28, 38, 41 v-asr-is-a-bitv, 41 v-flag, 63, 69 v-flag-ifs, 63 v-flag-with-ifs, 63, 72 v-lsl, 28, 38 v-lsr, 28, 29, 38 v-nat-dec, 47, 48, 75, 93, 94, 107,

153–155 v-nat-inc, 48, 75, 84, 92, 137, 138,

140–142, 144, 145, 153, 157 v-not, 10, 31, 35, 38 v-not-is-compl, 35 v-nth, 48, 55, 62, 65, 66, 76, 88–91,

93, 94, 97, 101–103, 105– 107, 110, 114–116, 118, 119, 137, 138, 140–145, 148–151, 153–157, 161, 165–167

v-or, 11, 31, 35, 38

v-rol, 28, 39 v-ror, 28, 29, 38 v-xor, 11, 31, 35, 38 v-zerop, 49, 173 v-zerop-equal-bv-to-nat-zero, 49 v-zerop-equal-bv-to-tc-zero, 49 vec, 9–12, 14, 18, 28, 30–32, 39, 49,

50 visual-mem, 66, 69, 72 visual-mem-after-a-b, 142, 143

watch-dog, 66, 69, 73, 79–81, 83, 85–91, 93, 95–102, 104–106, 108–115, 117–119, 121, 123– 128, 130, 131, 133, 135–139, 143, 147, 151, 167

write, 60, 68, 71 write-1, 66, 67

xor, 7, 9, 11

z-flag, 63, 64, 69 z-flag-ifs, 64 z-flag-with-ifs, 64, 72 zero-not-less-than-anything, 39