#|
Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Computational Logic, Inc. 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 Computational Logic, Inc. 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.
|#
; The Correctness of a Piton Big Number Addition Program
; J Strother Moore
; This file corresponds to Chapter 3 of CLI Tech Report 22,
; "Piton:  A Verified Assembly Level Language".

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

Event: Enable plus-0.

Event: Enable commutativity-of-plus.

Event: Enable commutativity2-of-plus.

Event: Enable associativity-of-plus.

Theorem: plus-add1-1 ((1 + x) + y) = (1 + (x + y)) Theorem: plus-add1-2 (x + (1 + y)) = (1 + (x + y)) Event: Enable equal-plus-0. Event: Enable times-0. Event: Enable times-add1. Event: Enable times-distributes-over-plus. Event: Enable commutativity-of-times. Event: Enable commutativity2-of-times. Event: Enable associativity-of-times. Event: Enable equal-times-0. Event: Enable difference-elim. Theorem: difference-elim-rewrite1 ((x ∈ N) ∧ (x ≮ y)) → ((y + (x − y)) = x) Event: Enable lessp-remainder. Theorem: lessp-remainder-linear (y ≄ 0) → ((x mod y) < y) Event: Enable remainder-quotient-elim. Event: Enable plus-remainder-times-quotient. Event: Enable lessp-quotient. Theorem: lessp-quotient-linear ((x ≄ 0) ∧ (y ≠ 1)) → ((x ÷ y) < x)

Event: Enable not-lessp-quotient.

Theorem: not-lessp-times (x ≄ 0) → ((x ∗ y) ≮ y)

Definition: nat->bign (n, base, size) = if size ≃ 0 then nil

else cons (tag ('nat, n mod base), nat->bign (n ÷ base, base, size − 1)) endif

Definition: bign->nat (a, base) = if a ≃ nil then 0

else untag (car (a)) + (base ∗ bign->nat (cdr (a), base)) endif

Definition: bignp (a, base) = if a ≃ nil then a = nil

else listp (car (a))

∧ (type (car (a)) = 'nat) ∧ (untag (car (a)) ∈ N) ∧ (untag (car (a)) < base) ∧ (cddr (car (a)) = nil) ∧ bignp (cdr (a), base) endif

Theorem: bignp-nat->bign (base ≄ 0) → bignp (nat->bign (n, base, size), base)

Theorem: length-nat->bign (base ≄ 0) → (length (nat->bign (n, base, size)) = fix (size))

Theorem: lessp-quotient-times (n < (b ∗ e)) → (((n ÷ b) < e) = t)

Theorem: bign->nat->bign ((n ∈ N) ∧ (1 < base) ∧ (n < exp (base, size))) → (bign->nat (nat->bign (n, base, size), base) = n)

Definition: tv->nat (c) = if c then 1

else 0 endif Definition: big-add-array (a, b, c, base) = if a ≃ nil then nil

else cons (tag ('nat, (untag (car (a)) + untag (car (b)) + tv->nat (c)) mod base), big-add-array (cdr (a),

cdr (b),

(untag (car (a)) + untag (car (b)) + tv->nat (c)) ≮ base, base)) endif

Definition: big-add-carry-out (a, b, c, base) = if a ≃ nil then bool (c)

else big-add-carry-out (cdr (a), cdr (b), (untag (car (a)) + untag (car (b)) + tv->nat (c)) ≮ base, base) endif

Event: Enable difference-x-x.

Theorem: remainder-carryout1 ((i < base) ∧ (j < base) ∧ ((1 + (i + j )) ≮ base)) → (((1 + (i + j )) mod base) = ((1 + (i + j )) − base))

Theorem: remainder-carryout0 ((i < base) ∧ (j < base) ∧ ((i + j ) ≮ base)) → (((i + j ) mod base) = ((i + j ) − base))

Theorem: interpretation-of-big-add-results (bignp (a, base) ∧ bignp (b, base) ∧ (length (a) = length (b)) ∧ (base ∈ N) ∧ (1 < base)) → (bign->nat (append (big-add-array (a, b, c, base),

list (tag ('nat, bool-to-nat (untag (big-add-carry-out (a, b, c, base)))))),

base)

= (bign->nat (a, base) + bign->nat (b, base) + tv->nat (c)))

; The above theorem is just about all of the mathematical content of
; this exercise.  It remains relate the functions big-add-array and big-add-carry-out
; to a Piton program.

Event: Disable tv->nat.

Theorem: equal-lessp-n-1 (n < 1) = (n ≃ 0)

Definition: big-add-array-loop (i, a-array, b-array, n, c, base) = if (n − 1) ≃ 0

then put (tag ('nat, (untag (get (i, a-array)) + untag (get (i, b-array)) + tv->nat (c)) mod base),

i,

a-array) else big-add-array-loop (1 + i,

put (tag ('nat, (untag (get (i, a-array)) + untag (get (i, b-array)) + tv->nat (c)) mod base),

i,

a-array), b-array, n − 1, (untag (get (i, a-array)) + untag (get (i, b-array)) + tv->nat (c)) ≮ base, base) endif Definition: big-add-carry-out-loop (i, a-array, b-array, n, c, base) = if (n − 1) ≃ 0

then bool ((untag (get (i, a-array)) + untag (get (i, b-array)) + tv->nat (c)) ≮ base) else big-add-carry-out-loop (1 + i,

put (tag ('nat, (untag (get (i, a-array)) + untag (get (i, b-array)) + tv->nat (c)) mod base),

i,

a-array), b-array, n − 1, (untag (get (i, a-array)) + untag (get (i, b-array)) + tv->nat (c)) ≮ base, base) endif

Definition: nth-cdr (i, a) = if i ≃ 0 then a

else nth-cdr (i − 1, cdr (a)) endif

Theorem: get-is-car-nth-cdr get (i, a) = car (nth-cdr (i, a))

Event: Enable length-put.

Theorem: nth-cdr-add1 nth-cdr (1 + i, x) = cdr (nth-cdr (i, x))

Theorem: nth-cdr-put-at (i < length (a)) → (nth-cdr (i, put (val, i, a)) = cons (val, cdr (nth-cdr (i, a))))

Definition: hint1 (i, a, b, c, base) = if i < length (a)

then hint1 (1 + i, put (tag ('nat,

(untag (get (i, a)) + untag (get (i, b)) + tv->nat (c)) mod base),

i, a),

b,

(untag (get (i, a)) + untag (get (i, b)) + tv->nat (c)) ≮ base, base)

else t endif

Theorem: listp-nth-cdr listp (nth-cdr (i, a)) = (i < length (a))

Theorem: nth-cdr-put-before ((j < i) ∧ (j < length (a))) → (nth-cdr (i, put (val, j , a)) = nth-cdr (i, a))

Theorem: difference-equal-1 ((i < length (a)) ∧ (i ≮ (length (a) − 1))) → ((length (a) − i) = 1)

Theorem: big-add-array-loop-on-list-of-length-1 big-add-array-loop (i, a, b, 1, c, base) = put (tag ('nat,

(untag (get (i, a)) + untag (get (i, b)) + tv->nat (c)) mod base),

i, a)

Event: Enable equal-length-0.

Theorem: equal-length-1 (length (a) = 1) = (listp (a) ∧ (cdr (a) ≃ nil))

Theorem: nlistp-cdr-nth-cdr listp (cdr (nth-cdr (i, a))) = (i < (length (a) − 1))

Theorem: big-add-array-on-list-of-length-1 (listp (a) ∧ (cdr (a) ≃ nil)) → (big-add-array (a, b, c, base)

= list (tag ('nat, (untag (car (a)) + untag (car (b)) + tv->nat (c)) mod base)))

; The following lemma is intended only for use in the inductive step
; of mathematical-big-add-v-big-add-array-loop-generalized, where we
; replace i by (add1 i) and need to transform the lhs difference to
; the rhs sub1.

Theorem: difference-add1-new (length (a) − (1 + i)) = ((length (a) − i) − 1)

Theorem: length-big-add-array-loop ((i < length (a)) ∧ (length (a) ≮ (i + n))) → (length (big-add-array-loop (i, a, b, n, c, base)) = length (a))

Theorem: car-nth-cdr-put ((i ∈ N) ∧ (j ∈ N)) → (car (nth-cdr (i, put (val, j , a)))

= if i = j then val else car (nth-cdr (i, a)) endif)

Theorem: car-nth-cdr-big-add-array-loop ((k ∈ N) ∧ (i ∈ N) ∧ (k < i)) → (car (nth-cdr (k, big-add-array-loop (i, a, b, n, c, base)))

= car (nth-cdr (k, a)))

Theorem: equal-nth-cdr-nil bignp (a, base) → ((nil = nth-cdr (i, a)) = (fix (i) = length (a)))

Theorem: equal-cddr-nth-cdr-nil bignp (a, base) → ((nil = cddr (nth-cdr (i, a))) = ((1 + (1 + i)) = length (a)))

Theorem: bignp-put ((i ∈ N) ∧ (i < length (a)) ∧ bignp (a, base) ∧ (val ∈ N) ∧ (val < base)) → bignp (put (list ('nat, val), i, a), base)

Theorem: cons-car-cdr-hack (cons (a, cdr (x)) = x) = (listp (x) ∧ (a = car (x)))

Theorem: big-add-array-is-big-add-array-loop-generalized ((i ∈ N) ∧ (i < length (a)) ∧ bignp (a, base)

∧ (base ∈ N) ∧ (1 < base)) → (big-add-array (nth-cdr (i, a), nth-cdr (i, b), c, base)

= nth-cdr (i, big-add-array-loop (i, a, b, length (a) − i, c, base)))

Theorem: big-add-array-is-big-add-array-loop (listp (a) ∧ bignp (a, base) ∧ (base ∈ N) ∧ (1 < base)) → (big-add-array (a, b, c, base)

= big-add-array-loop (0, a, b, length (a), c, base))

Theorem: big-add-carry-out-on-list-of-length-1 (listp (a) ∧ (cdr (a) ≃ nil)) → (big-add-carry-out (a, b, c, base)

= bool ((untag (car (a)) + untag (car (b)) + tv->nat (c)) ≮ base))

Theorem: big-add-carry-out-is-big-add-carry-out-loop-generalized ((i ∈ N) ∧ (i < length (a))) → (big-add-carry-out (nth-cdr (i, a), nth-cdr (i, b), c, base)

= big-add-carry-out-loop (i, a, b, length (a) − i, c, base))

Theorem: big-add-carry-out-is-big-add-carry-out-loop listp (a) → (big-add-carry-out (a, b, c, base)

= big-add-carry-out-loop (0, a, b, length (a), c, base))

Definition: big-add-program

= '(big-add
(a b n)
nil
(push-constant (bool f))
(push-local a)
(dl loop nil (fetch))
(push-local b)
(fetch)
(add-nat-with-carry)
(push-local a)
(deposit)
(push-local n)
(sub1-nat)
(set-local n)
(test-nat-and-jump zero done)
(push-local b)
(push-constant (nat 1))

      (add-addr)
      (pop-local b)
      (push-local a)
      (push-constant (nat 1))
      (add-addr)
      (set-local a)
      (jump loop)
      (dl done nil (ret)))

Definition: big-add-loop-clock (n) = if n ≃ 0 then 0

elseif n = 1 then 11

else 19 + big-add-loop-clock (n − 1) endif

; The following clock function includes one tick for the CALL.  That is,
; BIG-ADD-CLOCK is the amount of time it takes to execute a CALL of BIG-ADD,
; not just the body of BIG-ADD.

Definition: big-add-clock (n) = (3 + big-add-loop-clock (n))

; The concept of value in the defs.events is at odds with the
; use of the term in the report.

Definition: array (name, segment) = cdr (assoc (name, segment))

Definition: put-array (a, name, segment) = put-assoc (a, name, segment)

Event: Disable booleanp.

Definition: tv (b) = (b = 't)

Event: Enable assoc-put-assoc-2.

Event: Disable get-is-car-nth-cdr.

Theorem: p-step1-opener p-step1 (cons (opcode, operands), p) = if p-ins-okp (cons (opcode, operands), p)

then p-ins-step (cons (opcode, operands), p) else p-halt (p, x-y-error-msg ('p, opcode)) endif Event: Disable p-step1.

Theorem: p-opener (p (s, 0) = s) ∧ (p (p-state (pc, ctrl, temp, prog, data, max-ctrl, max-temp, word-size, psw),

1 + n) = p (p-step (p-state (pc,

ctrl, temp, prog, data, max-ctrl, max-temp, word-size, psw)),

n))

Event: Disable p.

Theorem: bignp-implies-p-objectp-get (bignp (a, exp (2, word-size)) ∧ (i < length (a))) → (listp (get (i, a))

∧ (cddr (get (i, a)) = nil) ∧ (car (get (i, a)) = 'nat) ∧ (cadr (get (i, a)) ∈ N) ∧ (cadr (get (i, a)) < exp (2, word-size)))

Theorem: booleanp-not-f (booleanp (c) ∧ (c ≠ 'f)) → ((c = 't) = t)

Theorem: lessp-1-base (word-size ≄ 0) → (1 < exp (2, word-size))

Theorem: assoc-put-assoc-2-new (a ≠ b) → (assoc (a, put-assoc (val, b, segment)) = assoc (a, segment))

Event: Enable definedp-put-assoc.

; ??? I am here.  The db is here.  The comment above is wrong.  Since then
; I have changed the theorem by eliminating the hyp (equal p (p-state ...)).
; I see no alternative to simply starting the proof of the thm below over again.
; That is what I have done.  The comment above remains just as a reminder of where
; I was.  It should be deleted when I start afresh.

Theorem: booleanp-not-f-tv->nat (booleanp (c) ∧ (c ≠ 'f)) → (tv->nat (c) = 1)

Definition: big-add-loop-correct-hint (a, b, i, data-segment, c, word-size) = if definedp (a, data-segment)

∧ (i < length (array (a, data-segment))) then if ((length (array (a, data-segment)) − i) − 1) ≃ 0 then t

else big-add-loop-correct-hint (a, b, 1 + i, put-assoc (put (tag ('nat,

(untag (get (i,

array (a,

data-segment)))

+ untag (get (i,

array (b,

data-segment)))

+ bool-to-nat (c)) mod exp (2,

word-size)),

i,

array (a,

data-segment)),

a,

data-segment),

if (untag (get (i,

array (a,

data-segment)))

+ untag (get (i,

array (b,

data-segment)))

+ bool-to-nat (c)) < exp (2, word-size)

then 'f

else 't endif, word-size) endif

else t endif

Event: Enable put-assoc-put-assoc.

; I have proved 2 of the 3 cases of this.  I think the remaining case is
; trivial.  I will add it as an axiom and proceed.  The proof takes about
; 3 hours, judging from the two cases I did.

Theorem: big-add-loop-correct-generalized ((length (array (a, data-segment)) < exp (2, word-size)) ∧ (word-size ≄ 0) ∧ listp (ctrl-stk) ∧ bignp (array (a, data-segment), exp (2, word-size)) ∧ bignp (array (b, data-segment), exp (2, word-size)) ∧ (max-temp-stk-size ≮ (1 + (1 + (1 + length (temp-stk))))) ∧ (definition ('big-add, prog-segment) = big-add-program) ∧ definedp (a, data-segment) ∧ definedp (b, data-segment) ∧ (a ≠ b) ∧ (i ∈ N) ∧ (i < n) ∧ (n = length (array (a, data-segment))) ∧ (n = length (array (b, data-segment))) ∧ booleanp (c))

→ (p (p-state ('(pc (big-add . 2)),

cons (list (list (cons ('a, list ('addr, cons (a, i))), cons ('b, list ('addr, cons (b, i))), cons ('n, list ('nat, n − i))),

ret-pc), ctrl-stk),

cons (list ('addr, cons (a, i)), cons (list ('bool, c), temp-stk)), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

             'run),

big-add-loop-clock (n − i)) = p-state (ret-pc,

ctrl-stk,

cons (big-add-carry-out-loop (i, array (a, data-segment), array (b, data-segment), n − i, tv (c), exp (2, word-size)),

temp-stk), prog-segment, put-assoc (big-add-array-loop (i,

array (a, data-segment), array (b, data-segment), n − i, tv (c), exp (2, word-size)),

a,

data-segment),

max-ctrl-stk-size, max-temp-stk-size, word-size,

              'run))

Theorem: big-add-loop-correct ((length (array (a, data-segment)) < exp (2, word-size)) ∧ (word-size ≄ 0) ∧ listp (ctrl-stk) ∧ bignp (array (a, data-segment), exp (2, word-size)) ∧ bignp (array (b, data-segment), exp (2, word-size)) ∧ (max-temp-stk-size ≮ (1 + (1 + (1 + length (temp-stk))))) ∧ (definition ('big-add, prog-segment) = big-add-program) ∧ definedp (a, data-segment) ∧ definedp (b, data-segment) ∧ (a ≠ b) ∧ (n ≄ 0) ∧ (n = length (array (a, data-segment))) ∧ (n = length (array (b, data-segment))) ∧ booleanp (c))

→ (p (p-state ('(pc (big-add . 2)),

cons (list (list (cons ('a, list ('addr, cons (a, 0))), cons ('b, list ('addr, cons (b, 0))), cons ('n, list ('nat, n))),

ret-pc), ctrl-stk),

cons (list ('addr, cons (a, 0)),

cons (list ('bool, c), temp-stk)), prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

             'run),

big-add-loop-clock (n)) = p-state (ret-pc,

ctrl-stk,

cons (big-add-carry-out-loop (0, array (a, data-segment), array (b, data-segment), n, tv (c), exp (2, word-size)),

temp-stk), prog-segment, put-assoc (big-add-array-loop (0,

array (a, data-segment), array (b, data-segment), n, tv (c), exp (2, word-size)),

a,

data-segment),

max-ctrl-stk-size, max-temp-stk-size, word-size,

           'run))

Definition: big-add-input-conditionp (a, b, n, p0 ) = (definedp (a, p-data-segment (p0 ))

∧ definedp (b, p-data-segment (p0 )) ∧ (a ≠ b) ∧ bignp (array (a, p-data-segment (p0 )), exp (2, p-word-size (p0 ))) ∧ bignp (array (b, p-data-segment (p0 )), exp (2, p-word-size (p0 ))) ∧ (n = length (array (a, p-data-segment (p0 )))) ∧ (n = length (array (b, p-data-segment (p0 )))) ∧ (p-max-ctrl-stk-size (p0 )

≮ (5 + p-ctrl-stk-size (p-ctrl-stk (p0 )))) ∧ (p-max-temp-stk-size (p0 ) ≮ (3 + length (p-temp-stk (p0 )))) ∧ (n ≄ 0) ∧ (n < exp (2, p-word-size (p0 ))) ∧ listp (p-ctrl-stk (p0 )))

Theorem: not-zerop-wordsize-hack ((n < exp (2, word-size)) ∧ (n ≄ 0)) → (((word-size ∈ N) = t) ∧ (word-size ≠ 0))

Theorem: big-add-correct ((p0 = p-state (pc,

ctrl-stk,

append (list (tag ('nat, n), tag ('addr, cons (b, 0)),

tag ('addr, cons (a, 0))), temp-stk),

prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (p-current-instruction (p0 ) = '(call big-add)) ∧ (definition ('big-add, prog-segment) = big-add-program) ∧ big-add-input-conditionp (a, b, n, p0 )) → (p (p0 , big-add-clock (n))

= p-state (add1-addr (pc), ctrl-stk, push (big-add-carry-out (array (a, data-segment),

array (b, data-segment), f, exp (2, word-size)),

temp-stk), prog-segment, put-array (big-add-array (array (a, data-segment),

array (b, data-segment), f, exp (2, word-size)),

a,

data-segment),

max-ctrl-stk-size,

max-temp-stk-size,

word-size,

  'run))
; The above thm is not useful as a rewrite rule because p0 occurs
; in the lhs and pc, ctrl-stk, etc., are all free vars.  So to make it
; a rewrite rule we actually substitute (p-state pc ...) for p0 into the
; lhs.  In addition, the append in that initial state is going to be
; conses in applications, so we expand it in the lhs.  In addition,
; the tags are expanded to lists.

Theorem: big-add-correct-rewrite-version ((p0 = p-state (pc,

ctrl-stk, append (list (tag ('nat, n),

tag ('addr, cons (b, 0)),

tag ('addr, cons (a, 0))), temp-stk),

prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run))

∧ (p-current-instruction (p0 ) = '(call big-add)) ∧ (definition ('big-add, prog-segment) = big-add-program) ∧ big-add-input-conditionp (a, b, n, p0 )) → (p (p-state (pc,

ctrl-stk, cons (list ('nat, n),

cons (list ('addr, cons (b, 0)),

cons (list ('addr, cons (a, 0)), temp-stk))),

prog-segment, data-segment, max-ctrl-stk-size, max-temp-stk-size, word-size,

'run),

big-add-clock (n)) = p-state (add1-addr (pc),

ctrl-stk, push (big-add-carry-out (array (a, data-segment),

array (b, data-segment), f, exp (2, word-size)),

temp-stk), prog-segment, put-array (big-add-array (array (a, data-segment),

array (b, data-segment), f, exp (2, word-size)),

a,

data-segment),

max-ctrl-stk-size, max-temp-stk-size, word-size,

 'run))

Event: Disable not-zerop-wordsize-hack.

;  That says all we need to say about BIG-ADD except for how we connect
; this thm to our FM8502 correctness result.  The question is: what has
; to be true about a state p in order for the hyp of
#|
(IMPLIES (AND (PROPER-P-STATEP P0)
              (P-LOADABLEP P0)
              (EQUAL (P-WORD-SIZE P0) 32)
              (EQUAL PN (P P0 N))
              (NOT (ERRORP (P-PSW PN)))
              (EQUAL TS (TYPE-SPECIFICATION (P-DATA-SEGMENT PN))))
         (EQUAL (P-DATA-SEGMENT PN)
                (DISPLAY-M-DATA-SEGMENT
                  (FM8502 (LOAD P0) (FM8502-CLOCK P0 N))
                  TS
                  (LINK-TABLES P0))))
|#
; to be true?
; Let us first identify a state that is suitable for running BIG-ADD.

Definition: main-program

= '(main nil nil
      (push-constant (addr (bna . 0)))
      (push-constant (addr (bnb . 0)))
      (push-global n)
      (call big-add)
      (pop-global c)
      (ret))

Definition: system-initial-state (a, b)

= p-state ('(pc (main . 0)),
          '((nil (pc (main . 0)))),

nil,

list (main-program, big-add-program), list (cons ('bna, a), cons ('bnb, b), cons ('n, list (tag ('nat, length (a)))), cons ('c, list (tag ('nat, 0)))),

          10,

          32,
          'run)
; This state takes the following number of clock ticks:

Definition: system-initial-state-clock (a, b) = (5 + big-add-clock (length (a)))

; The condition under which big-add-initial-state produces a acceptable state for
; the abstract computation to work is

Event: Disable exp.

Event: Disable *1*exp.

Definition: system-initial-state-okp (a, b) = (bignp (a, exp (2, 32))

∧ bignp (b, exp (2, 32)) ∧ (length (a) = length (b)) ∧ (length (a) ≄ 0) ∧ (length (a) < exp (2, 32)))

; We prove that system-initial-state-okp lives up to the above claim:

Theorem: restructure-system-initial-state-clock system-initial-state-clock (a, b) = (3 + big-add-clock (length (a)) + 2)

Event: Disable system-initial-state-clock.

Event: Disable plus-add1-2.

Event: Disable commutativity-of-plus.

Theorem: p-plus p (p, i + j ) = p (p (p, i), j )

Theorem: system-correct system-initial-state-okp (a, b)

→ (p (system-initial-state (a, b), system-initial-state-clock (a, b))

     = p-state ('(pc (main . 5)),
                '((nil (pc (main . 0)))),

nil,

list (main-program, big-add-program),

list (cons ('bna, big-add-array (a, b, f, exp (2, 32))), cons ('bnb, b), cons ('n, list (tag ('nat, length (a)))), cons ('c,

list (big-add-carry-out (a, b, f, exp (2, 32))))),

                10,
                8,
                32,
                'halt))
; Furthermore, if system-initial-state-okp is true then the initial state is
; proper-p-state and its word size is 32, as required by our FM8502 correctness
; result.

Theorem: bignp-implies-all-p-objectps (bignp (a, base) ∧ (base = exp (2, p-word-size (p)))) → all-p-objectps (a, p)

Theorem: initial-correctness-conditions system-initial-state-okp (a, b) → (proper-p-statep (system-initial-state (a, b))

∧ (p-word-size (system-initial-state (a, b)) = 32))

; In addition, the final state is not an error and its type-specification is
; easily computed from the input:

Definition: nat-lst (n) = if n ≃ 0 then nil

else cons ('nat, nat-lst (n − 1)) endif

Theorem: type-lst-big-add-array type-lst (big-add-array (a, b, c, base)) = nat-lst (length (a))

Theorem: type-lst-bignp bignp (a, base) → (type-lst (a) = nat-lst (length (a)))

Theorem: car-big-add-carry-out car (big-add-carry-out (a, b, c, base)) = 'bool Theorem: final-correctness-conditions system-initial-state-okp (a, b) → ((¬ errorp (p-psw (p (system-initial-state (a, b),

system-initial-state-clock (a, b)))))

∧ (type-specification (p-data-segment (p (system-initial-state (a, b),

system-initial-state-clock (a,

b))))

= list (cons ('bna, nat-lst (length (a))), cons ('bnb, nat-lst (length (a))), cons ('n, list ('nat)), cons ('c, list ('bool)))))

; This leaves only the question, is the system-initial-state loadable?  That all depends on
; how much room you take up with the data.  It is certainly loadable for some
; values of a and b and some load addresses.  Below we use the load address 0.

Theorem: loadable-for-bigns-up-to-length-1000 (system-initial-state-okp (a, b) ∧ (length (a) < 1000)) → p-loadablep (system-initial-state (a, b), 0)

; Oh, there is one more thing we might ask, which is whether there are
; any system-initial-state-okps.  There are.

Theorem: example-is-system-initial-state-okp system-initial-state-okp ('((nat 246838082)

                       (nat 3116233281)
                       (nat 42632655)
                       (nat 0)),
                     '((nat 3579363592)
                       (nat 3979696680)
                       (nat 7693250)
                       (nat 0)))

Theorem: type-specification-hack system-initial-state-okp (a, b) → (type-lst (b) = nat-lst (length (b)))

; We need to refer to the link tables for a state without knowing
; the actual data, just the size of the data.  So we define the
; function below which constructs the link tables from a generic
; state of the right size.  This will turn out to be EQUAL to the
; link table for any state of that size.

Definition: big-zero (n) = if n ≃ 0 then nil

else cons ('(nat 0), big-zero (n − 1)) endif

; We link for load address 0.

Definition: system-link-tables (n, m) = link-tables (system-initial-state (big-zero (n), big-zero (m)), 0)

Theorem: length-big-zero length (big-zero (n)) = fix (n)

Theorem: link-tables-length link-tables (system-initial-state (a, b), 0) = system-link-tables (length (a), length (b))

Theorem: system-initial-state-okp-length-hack system-initial-state-okp (a, b) → (length (b) = length (a))

Definition: display-answers (m-state, n) = let alist be display-fm9001-data-segment (m-state,

list (cons ('bna,

nat-lst (n)), cons ('bnb,

nat-lst (n)), cons ('n, list ('nat)), cons ('c,

list ('bool))),

system-link-tables (n, n))

in

list (cdr (assoc ('bna, alist)), cadr (assoc ('c, alist))) endlet

Theorem: type-big-add-carry-out type (big-add-carry-out (a, b, c, base)) = 'bool

Theorem: eliminate-piton (system-initial-state-okp (a, b) ∧ (length (a) < 1000)) → (display-answers (fm9001 (load (system-initial-state (a, b), nil, 0),

fm9001-clock (system-initial-state (a, b),

system-initial-state-clock (a, b))),

length (a)) = list (big-add-array (a, b, f, exp (2, 32)),

big-add-carry-out (a, b, f, exp (2, 32))))

Theorem: clock-for-concrete-data

let a be '((nat 246838082)
           (nat 3116233281)
           (nat 42632655)
           (nat 0)),
   b be '((nat 3579363592)
           (nat 3979696680)
           (nat 7693250)
           (nat 0))

in fm9001-clock (system-initial-state (a, b),

system-initial-state-clock (a, b)) endlet

= 190

Index

add1-addr, 16, 17 all-p-objectps, 20 array, 10, 12–17 assoc-put-assoc-2-new, 11

big-add-array, 4, 7, 9, 16, 17, 20, 22 big-add-array-is-big-add-array-

loop, 9 loop-generalized, 8

big-add-array-loop, 5, 7–9, 14, 15 big-add-array-loop-on-list-of-le

ngth-1, 7 big-add-array-on-list-of-length

-1, 7 big-add-carry-out, 4, 5, 9, 16, 17,

20, 22 big-add-carry-out-is-big-add-ca

rry-out-loop, 9 rry-out-loop-generalized, 9

big-add-carry-out-loop, 6, 9, 13, 15 big-add-carry-out-on-list-of-le

ngth-1, 9 big-add-clock, 10, 16, 17, 19 big-add-correct, 15 big-add-correct-rewrite-version, 16 big-add-input-conditionp, 15–17 big-add-loop-clock, 10, 13, 14 big-add-loop-correct, 14 big-add-loop-correct-generalize

d, 13 big-add-loop-correct-hint, 12 big-add-program, 9, 13, 14, 16–18,

20 big-zero, 22 bign->nat, 3, 5 bign->nat->bign, 3 bignp, 3, 4, 8, 9, 11, 13–15, 19, 20 bignp-implies-all-p-objectps, 20 bignp-implies-p-objectp-get, 11 bignp-nat->bign, 3 bignp-put, 8 bool, 4, 6, 9 bool-to-nat, 5, 12 booleanp, 11–14 booleanp-not-f, 11 booleanp-not-f-tv->nat, 12

car-big-add-carry-out, 20 car-nth-cdr-big-add-array-loop, 8 car-nth-cdr-put, 8 clock-for-concrete-data, 23 cons-car-cdr-hack, 8

definedp, 12–15 definition, 13, 14, 16, 17 difference-add1-new, 8 difference-elim-rewrite1, 2 difference-equal-1, 7 display-answers, 22 display-fm9001-data-segment, 22

eliminate-piton, 22 equal-cddr-nth-cdr-nil, 8 equal-length-1, 7 equal-lessp-n-1, 5 equal-nth-cdr-nil, 8 errorp, 21 example-is-system-initial-state

-okp, 21 exp, 3, 11–17, 19, 20, 22

final-correctness-conditions, 21 fm9001, 22 fm9001-clock, 22, 23

get, 5–7, 11, 12 get-is-car-nth-cdr, 6

hint1, 6, 7

initial-correctness-conditions, 20 interpretation-of-big-add-result

s, 4 length, 3, 4, 6–9, 11–15, 18–22 length-big-add-array-loop, 8 length-big-zero, 22 length-nat->bign, 3 lessp-1-base, 11 lessp-quotient-linear, 2 lessp-quotient-times, 3 lessp-remainder-linear, 2 link-tables, 22 link-tables-length, 22 listp-nth-cdr, 7 load, 22 loadable-for-bigns-up-to-length

-1000, 21

main-program, 18, 20

nat->bign, 3 nat-lst, 20–22 nlistp-cdr-nth-cdr, 7 not-lessp-times, 3 not-zerop-wordsize-hack, 15 nth-cdr, 6–9 nth-cdr-add1, 6 nth-cdr-put-at, 6 nth-cdr-put-before, 7

p, 11, 13, 14, 16, 17, 19–21 p-ctrl-stk, 15 p-ctrl-stk-size, 15 p-current-instruction, 16, 17 p-data-segment, 15, 21 p-halt, 10 p-ins-okp, 10 p-ins-step, 10 p-loadablep, 21 p-max-ctrl-stk-size, 15 p-max-temp-stk-size, 15 p-opener, 11 p-plus, 19 p-psw, 21 p-state, 11, 13–17, 19, 20 p-step, 11 p-step1, 10 p-step1-opener, 10 p-temp-stk, 15 p-word-size, 15, 20 plus-add1-1, 2 plus-add1-2, 2 proper-p-statep, 20 push, 16, 17 put, 5–8, 12 put-array, 10, 16, 17 put-assoc, 10–12, 14, 15

remainder-carryout0, 4 remainder-carryout1, 4 restructure-system-initial-state

-clock, 19

system-correct, 19

system-initial-state, 18, 20–23 system-initial-state-clock, 19–23 system-initial-state-okp, 19–22 system-initial-state-okp-length

-hack, 22 system-link-tables, 22

tag, 3–7, 12, 15–18, 20

tv, 10, 13–15

tv->nat, 3–7, 9, 12

type, 3, 22

type-big-add-carry-out, 22

type-lst, 20, 21

type-lst-big-add-array, 20

type-lst-bignp, 20 type-specification, 21 type-specification-hack, 21

untag, 3–7, 9, 12

x-y-error-msg, 10