Event: Start with the library "c1".

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                   THE ASSEMBLY LANGUAGE                     ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The fields of the p-state are to be interpreted as follows:
;;    pc is the 0-based program counter;
;;    temp-stk is a stack for moving variables and computing values
;;    ctrl-stk is a list of frames with the local variables;
;;    data-segment is a var alist of global variables
;;    psw is 'run, 'halt, or some indication of error

Event: Add the shell p-state, with recognizer function symbol p-statep and 9 accessors: p-pc, with type restriction (none-of) and default value zero; p-ctrl-stk, with type restriction (none-of) and default value zero; p-temp-stk, with type restriction (none-of) and default value zero; p-prog-segment, with type restriction (none-of) and default value zero; p-data-segment, with type restriction (noneof) and default value zero; p-max-ctrl-stk-size, with type restriction (none-of) and default value zero; p-max-temp-stk-size, with type restriction (none-of) and default value zero; p-word-size, with type restriction (none-of) and default value zero; p-psw, with type restriction (none-of) and default value zero.

Definition: p-halt (p, psw) = p-state (p-pc (p),

p-ctrl-stk (p), p-temp-stk (p), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p), psw)

;;(defn errorp (psw)
;;  (and (not (equal psw 'run))
;;       (not (equal psw 'halt))))

Definition: definition (name, alist) = assoc (name, alist)

Definition: put-value (val, name, alist) = put-assoc (val, name, alist)

Definition: formal-vars (d) = cadr (d)

Definition: temp-var-dcls (d) = caddr (d)

Definition: program-body (d) = cdddr (d)

;;(defn local-vars (d) (append (formal-vars d) (listcars (temp-var-dcls d))))
;; Addresses are tagged "address pairs".  This differs from the earlier formulation
;; in having to worry about the tags.  Thus the pc is now (pc (subr . foo)).

Definition: adp-name (adp) = car (adp)

Event: Disable adp-name.

Definition: adp-offset (adp) = cdr (adp)

Event: Disable adp-offset.

Theorem: adp-name-cons adp-name (cons (x, y)) = x

Theorem: adp-offset-cons adp-offset (cons (x, y)) = y

Definition: adpp (x, segment) = (listp (x)

∧ (adp-offset (x) ∈ N)

∧ definedp (adp-name (x), segment)

∧ (adp-offset (x) < length (value (adp-name (x), segment))))

Definition: pcpp (x, segment) = (listp (x)

∧ (adp-offset (x) ∈ N)

∧ definedp (adp-name (x), segment)

∧ (adp-offset (x)

< length (program-body (definition (adp-name (x), segment)))))

Definition: add-adp (adp, n) = cons (adp-name (adp), adp-offset (adp) + n)

Definition: add1-adp (adp) = add-adp (adp, 1)

Definition: sub-adp (adp, n) = cons (adp-name (adp), adp-offset (adp) − n)

;;(defn sub1-adp (adp) (sub-adp adp 1))
;;
;;(defn add1-adp-adpp (x segment)
;;      (adpp (add1-adp x) segment))
;;
;;(defn add-adp-adpp (x n segment)
;;      (adpp (add-adp x n) segment))

Definition: fetch-adp (adp, segment) = get (adp-offset (adp), value (adp-name (adp), segment))

;; Puts val in the named segment at addr.

Definition: deposit-adp (val, adp, segment) = put-value (put (val, adp-offset (adp), value (adp-name (adp), segment)),

adp-name (adp), segment)

;; These two functions are the analogues of get and put counting from
;; the right.  They are used in the definition of fetch and deposit on the
;; temp-stk.

Definition: rget (n, lst) = get ((length (lst) − n) − 1, lst)

Definition: rput (val, n, lst) = put (val, (length (lst) − n) − 1, lst)

Theorem: rput-preserves-length (y < length (z)) → (length (rput (x, y, z)) = length (z))

Event: Disable rget.

Event: Disable rput.

;; Tagged objects
;; All Piton objects are tagged with their "type".  The form is (tag obj)

Definition: tag (type, obj ) = list (type, obj ) Definition: type (const) = car (const) Definition: untag (const) = cadr (const) Theorem: type-expansion type (cons (x, y)) = x Theorem: type-tag type (tag (x, y)) = x Theorem: untag-tag untag (tag (x, y)) = y Theorem: untag-cons untag (list (x, y)) = y

;;(prove-lemma tag-length-2 (rewrite)
;;      (equal (cddr (tag x y)) nil)
;;     ((enable tag)))

Event: Disable type.

Event: Disable tag.

Event: Disable untag.

;; Tagged addresses
;;(defn addressp (x segment) (adpp (untag x) segment))

Definition: area-name (x) = adp-name (untag (x)) Definition: offset (x) = adp-offset (untag (x)) Definition: add-addr (addr, n) = tag (type (addr), add-adp (untag (addr), n)) Definition: add1-addr (addr) = add-addr (addr, 1) Definition: sub-addr (addr, n) = tag (type (addr), sub-adp (untag (addr), n))

Definition: sub1-addr (addr) = sub-addr (addr, 1)

Definition: fetch (addr, segment) = fetch-adp (untag (addr), segment)

Definition: deposit (val, addr, segment) = deposit-adp (val, untag (addr), segment)

Definition: add1-nat (nat) = tag ('nat, 1 + untag (nat))

Theorem: untag-add1-nat untag (add1-nat (nat)) = (1 + untag (nat))

;; Booleans
;; Piton uses the litatoms 't and 'f for the truth values.

Definition: booleanp (x) = ((x = 't) ∨ (x = 'f))

Definition: bool (x) = tag ('bool,

if x then 't else 'f endif)

Definition: or-bool (x, y) = if x = 'f then y

else 't endif

Definition: and-bool (x, y) = if x = 'f then 'f

else y endif

Definition: not-bool (x) = if x = 'f then 't

else 'f endif

;; Naturals
;; Notice that, where full Piton allows word-size to be a parameter, I am making it
;; a constant.

Definition: small-naturalp (i, word-size) = ((i ∈ N) ∧ (i < exp (2, word-size)))

Event: Disable small-naturalp.

Definition: bool-to-nat (flg) = if flg = 'f then 0

else 1 endif

;; Integers
;; These functions are defined so that if given integerps they return integerps.
;; In particular, they never return (minus 0) though they may pass one through.

Definition: small-integerp (i, word-size) = (integerp (i)

∧ (¬ ilessp (i, − exp (2, word-size − 1)))

∧ ilessp (i, exp (2, word-size − 1)))

Event: Disable small-integerp.

Definition: fix-small-integer (i, word-size) = if small-integerp (i, word-size) then i

elseif negativep (i) then iplus (i, exp (2, word-size))

else iplus (i, − exp (2, word-size)) endif

;; I don't currently know which Piton integer ops I'll need on integers so I'm
;; leaving these out.
;; stacks

Definition: push (x, stk) = cons (x, stk)

Definition: top (stk) = car (stk)

Definition: pop (stk) = cdr (stk)

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

else popn (n − 1, cdr (x)) endif

Theorem: popn-add1 (popn (1 + n, push (x, y)) = popn (n, y)) ∧ (popn (1 + n, cons (x, y)) = popn (n, y))

Theorem: popn-zero popn (0, x) = x

Theorem: popn-length (n = length (lst)) → (popn (n, append (lst, stk)) = stk)

Theorem: popn-plus (m = length (lst1 )) → (popn (m + n, append (lst1 , lst2 )) = popn (n, lst2 ))

Definition: top1 (stk) = top (pop (stk))

Definition: top2 (stk) = top (pop (pop (stk)))

Theorem: pop-push pop (push (x, y)) = y

Theorem: pop-cons pop (cons (x, y)) = y

Theorem: car-cdr-push (car (push (x, y)) = x) ∧ (cdr (push (x, y)) = y)

Theorem: push-listp listp (push (x, y)) ∧ ((push (x, y) ≃ nil) = f)

Theorem: top-push top (push (x, y)) = x

Theorem: top1-push top1 (push (x, push (y, z))) = y

Theorem: top2-push top2 (push (x, push (y, push (z, w)))) = z

Theorem: length-push length (push (x, y)) = (1 + length (y))

Theorem: top-cons top (cons (x, y)) = x

;;(prove-lemma top1-cons (rewrite)
;;      (equal (top1 (cons x (cons y z))) y))
;;
;;(prove-lemma top2-cons (rewrite)
;;      (equal (top2 (cons x (cons y (cons z w)))) z))

Event: Disable pop.

Event: Disable push.

Event: Disable top.

Event: Disable top1.

Event: Disable top2.

Event: Disable popn.

;; Labels
;; Notice that labelled instructions now have comments associated with them.
;;(defn dl (lab comment ins) (list 'dl lab comment ins))

Definition: labelledp (x) = (car (x) = 'dl)

Theorem: labelledp-expansion labelledp (cons ('dl, args)) = t

Definition: unlabel (x) = if labelledp (x) then cadddr (x)

else x endif

Theorem: unlabel-expansion unlabel (cons ('dl, args)) = caddr (args)

Theorem: unlabel-unlabelledp (x ≠ 'dl) → (unlabel (cons (x, y)) = cons (x, y))

Event: Disable unlabel.

Definition: find-labelp (x, lst) = if lst ≃ nil then f

elseif labelledp (car (lst)) ∧ (x = cadr (car (lst))) then t else find-labelp (x, cdr (lst)) endif

;; This function counts the number of items in the list before the first one
;; labelled with x.  This is my get-pc function.

Definition: find-label (x, lst) = if lst ≃ nil then 0

elseif labelledp (car (lst)) ∧ (x = cadr (car (lst))) then 0 else 1 + find-label (x, cdr (lst)) endif

;;(defn all-find-labelp (lab-lst lst)
;;  (if (nlistp lab-lst)
;;      t
;;      (and (find-labelp (car lab-lst) lst)
;;           (all-find-labelp (cdr lab-lst) lst))))

Definition: pc (label, program) = tag ('pc, cons (car (program), find-label (label, program-body (program))))

;; Piton primitive objects

Definition: p-objectp (x, p) = (listp (x)

∧ (cddr (x) = nil) ∧ case on type (x): case = nat then small-naturalp (untag (x), p-word-size (p)) case = int then small-integerp (untag (x), p-word-size (p)) case = bool then booleanp (untag (x)) case = addr then adpp (untag (x), p-data-segment (p)) case = pc then pcpp (untag (x), p-prog-segment (p)) case = subr then definedp (untag (x), p-prog-segment (p)) otherwise f endcase)

Definition: p-objectp-type (type, x, p) = ((type (x) = type) ∧ p-objectp (x, p))

Definition: add1-p-pc (p) = add1-addr (p-pc (p))

Definition: p-current-program (p) = definition (area-name (p-pc (p)), p-prog-segment (p))

Definition: p-current-instruction (p) = unlabel (get (offset (p-pc (p)), program-body (p-current-program (p))))

Definition: p-frame (bindings, ret-pc) = list (bindings, ret-pc)

Definition: bindings (frame) = car (frame)

Definition: ret-pc (frame) = cadr (frame)

Theorem: bindings-frame (bindings (cons (x, y)) = x) ∧ (bindings (p-frame (x, y)) = x)

Theorem: ret-pc-frame (ret-pc (list (x, y)) = y) ∧ (ret-pc (p-frame (x, y)) = y)

Event: Disable p-frame.

Event: Disable bindings.

Event: Disable ret-pc.

Definition: p-frame-size (frame) = (2 + length (bindings (frame)))

Event: Disable p-frame-size.

Definition: p-ctrl-stk-size (ctrl-stk) = if ctrl-stk ≃ nil then 0

else p-frame-size (top (ctrl-stk)) + p-ctrl-stk-size (cdr (ctrl-stk)) endif

;;(defn local-varp (var ctrl-stk)
;;  (definedp var (bindings (top ctrl-stk))))

Definition: local-var-value (var, ctrl-stk) = value (var, bindings (top (ctrl-stk)))

Definition: set-local-var-value (val, var, ctrl-stk) = push (p-frame (put-value (val, var, bindings (top (ctrl-stk))),

ret-pc (top (ctrl-stk))), pop (ctrl-stk))

Definition: first-n (n, x) = if n ≃ 0 then nil

else cons (car (x), first-n (n − 1, cdr (x))) endif

Theorem: first-n-add1 (first-n (1 + n, push (x, y)) = cons (x, first-n (n, y))) ∧ (first-n (1 + n, cons (x, y)) = cons (x, first-n (n, y))) ∧ (first-n (0, y) = nil)

Theorem: first-n-plus-append (n = length (lst1 )) → (first-n (n + m, append (lst1 , lst2 )) = append (lst1 , first-n (m, lst2 )))

Event: Disable first-n-plus-append.

Theorem: first-n-append2 (plistp (lst1 ) ∧ (n = length (lst1 ))) → (first-n (n, append (lst1 , lst2 )) = lst1 )

Event: Disable first-n-append2.

Definition: pairlist (lst1 , lst2 ) = if lst1 ≃ nil then nil

else cons (cons (car (lst1 ), car (lst2 )), pairlist (cdr (lst1 ), cdr (lst2 ))) endif

Theorem: pairlist-plistp plistp (pairlist (x, y))

Theorem: length-pairlist length (pairlist (x, y)) = length (x)

Theorem: pairlist-distributes (length (lst1 ) = length (lst3 )) → (pairlist (append (lst1 , lst2 ), append (lst3 , lst4 ))

= append (pairlist (lst1 , lst3 ), pairlist (lst2 , lst4 )))

Event: Disable pairlist-distributes.

;; Given formal-vars '(X Y Z) we first push X, then Y, then Z.

Definition: pair-formal-vars-with-actuals (formal-vars, temp-stk) = pairlist (formal-vars, reverse (first-n (length (formal-vars), temp-stk)))

;; This function converts from the external form of the temp-alists to
;; the internal.  That is, in programs, the temp alist is written as
;; (... (tempi vali) ...).  Internally, this is stored as
;; (... (temp1 . vali) ...) to allow them to be accessed as all the
;; other alists.

Definition: pair-temps-with-initial-values (temp-var-dcls) = if temp-var-dcls ≃ nil then nil

else cons (cons (caar (temp-var-dcls), cadar (temp-var-dcls)), pair-temps-with-initial-values (cdr (temp-var-dcls))) endif

Theorem: length-pair-temps-with-initial-values length (pair-temps-with-initial-values (lst)) = length (lst)

Definition: make-p-call-frame (formal-vars, temp-stk, temp-var-dcls, ret-pc) = p-frame (append (pair-formal-vars-with-actuals (formal-vars, temp-stk),

pair-temps-with-initial-values (temp-var-dcls)), ret-pc)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                   THE PITON INSTRUCTIONS                    ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;  (CALL subr)          Push a new frame onto the ctrl-stk binding the
;                       formals and temps of the subroutine subr to their
;                       actual values and saving the current return pc.
;                       Transfer control to the beginning of subr.

Definition: p-call-okp (ins, p) = ((p-max-ctrl-stk-size (p)

≮ p-ctrl-stk-size (push (make-p-call-frame (formal-vars (definition (cadr (ins),

p-prog-segment (p))),

p-temp-stk (p),

temp-var-dcls (definition (cadr (ins),

p-prog-segment (p))),

add1-addr (p-pc (p))),

p-ctrl-stk (p))))

∧ (length (p-temp-stk (p))

≮ length (formal-vars (definition (cadr (ins), p-prog-segment (p))))))

Definition: p-call-step (ins, p) = p-state (tag ('pc, cons (cadr (ins), 0)),

push (make-p-call-frame (formal-vars (definition (cadr (ins),

p-prog-segment (p))),

p-temp-stk (p),

temp-var-dcls (definition (cadr (ins),

p-prog-segment (p))),

add1-addr (p-pc (p))),

p-ctrl-stk (p)), popn (length (formal-vars (definition (cadr (ins),

p-prog-segment (p)))),

p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;  (RET)              Return from the current subroutine, leaving temp-stk
;                     untouched but restoring ctrl-stk.  We make a special
;                     case out of top-level RETs:  halt the machine with the
;                     distinguished, non-erroneous psw HALT.

Definition: p-ret-okp (ins, p) = t

Definition: p-ret-step (ins, p) = if listp (pop (p-ctrl-stk (p))) then p-state (ret-pc (top (p-ctrl-stk (p))),

pop (p-ctrl-stk (p)), p-temp-stk (p), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

               'run)

else p-halt (p, 'halt) endif

;  (PUSH-CONSTANT c)    Push c onto temp-stk.  c is normally a tagged
;                       constant but we permit two abbreviations.
;                       If c is the atom 'pc, it denotes the pc
;                       of the instruction following this one.
;                       If c is a non-LISTP that is defined in
;                       the current program with a DL, it
;                       denotes the pc of that label.

Definition: p-push-constant-okp (ins, p) = (length (p-temp-stk (p)) < p-max-temp-stk-size (p))

;  First I define the ``unabbreviate'' function.  Observe that the
;  abbreviation depends upon the current state, p, since it permits the
;  abbreviation of the current p-pc.

Definition: unabbreviate-constant (c, p) = if c = 'pc then add1-p-pc (p)

elseif c ≃ nil then pc (c, p-current-program (p))

else c endif

Definition: p-push-constant-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (unabbreviate-constant (cadr (ins), p), p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)

;  (PUSH-LOCAL var)     Push the value of the local variable var onto
;                       the temp-stk.

Definition: p-push-local-okp (ins, p) = (length (p-temp-stk (p)) < p-max-temp-stk-size (p))

Definition: p-push-local-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (local-var-value (cadr (ins), p-ctrl-stk (p)), p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;  (PUSH-GLOBAL var)    Push the value of the global variable var onto
;                       temp-stk.

Definition: p-push-global-okp (ins, p) = (length (p-temp-stk (p)) < p-max-temp-stk-size (p))

Definition: p-push-global-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (fetch (tag ('addr, cons (cadr (ins), 0)), p-data-segment (p)),

p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;  (PUSH-TEMP-STK-INDEX n)
;                       Push onto temp-stk the temp stk index of the

;                       slot n below the current top.  n must be a
;                       natural number less than the length of the
;                       stack.  The object pushed is a NAT.
;                       Below is a picture of a temp-stk with
;                       of length 6, A being at the top:
;                       temp-stk:   (A B C D E F)
;                       index:       5 4 3 2 1 0
;                       n:           0 1 2 3 4 5
;                       The index returned is suitable for use by
;                       FETCH-TEMP-STK and DEPOSIT-TEMP-STK.

Definition: p-push-temp-stk-index-okp (ins, p) = ((length (p-temp-stk (p)) < p-max-temp-stk-size (p))

∧ (cadr (ins) < length (p-temp-stk (p))))

Definition: p-push-temp-stk-index-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (tag ('nat, (length (p-temp-stk (p)) − cadr (ins)) − 1),

p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;  (POP)                Pop top of temp-stk and discard

Definition: p-pop-okp (ins, p) = listp (p-temp-stk (p))

Definition: p-pop-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

pop (p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

'run)
;  (POP* n)                Pop temp-stk n times.

Definition: p-pop*-okp (ins, p) = (length (p-temp-stk (p)) ≮ cadr (ins))

Definition: p-pop*-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p), popn (cadr (ins), p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

'run)
;  (POP-LOCAL var)      Pop top of temp-stk and put the value into the local
;                       variable var.

Definition: p-pop-local-okp (ins, p) = listp (p-temp-stk (p))

Definition: p-pop-local-step (ins, p) = p-state (add1-p-pc (p),

set-local-var-value (top (p-temp-stk (p)), cadr (ins), p-ctrl-stk (p)),

pop (p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

'run)
;  (POP-GLOBAL var)     Pop top of temp-stk and put the value into the global
;                       variable var.

Definition: p-pop-global-okp (ins, p) = listp (p-temp-stk (p))

Definition: p-pop-global-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

pop (p-temp-stk (p)), p-prog-segment (p), deposit (top (p-temp-stk (p)),

tag ('addr, cons (cadr (ins), 0)), p-data-segment (p)),

p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;   (FETCH-TEMP-STK)    Pop top of temp-stk.  The result must
;                       be an index into the temp-stk, that is,
;                       a NAT less than the length of temp-stk.
;                       Push onto the temp-stk the contents of
;                       the indexed cell of temp-stk.

Definition: p-fetch-temp-stk-okp (ins, p) = (listp (p-temp-stk (p))

∧ p-objectp-type ('nat, top (p-temp-stk (p)), p)

∧ (untag (top (p-temp-stk (p))) < length (p-temp-stk (p))))

Definition: p-fetch-temp-stk-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (rget (untag (top (p-temp-stk (p))), p-temp-stk (p)),

pop (p-temp-stk (p))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;   (DEPOSIT-TEMP-STK)  Pop top and top1 off of temp-stk.  top must be
;                       an index into temp-stk.  Deposit top1 into the indexed
;                       cell of temp-stk.

Definition: p-deposit-temp-stk-okp (ins, p) = (listp (p-temp-stk (p))

∧ listp (pop (p-temp-stk (p))) ∧ p-objectp-type ('nat, top (p-temp-stk (p)), p) ∧ (untag (top (p-temp-stk (p)))

< length (pop (pop (p-temp-stk (p))))))

Definition: p-deposit-temp-stk-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p), rput (top1 (p-temp-stk (p)),

untag (top (p-temp-stk (p))), pop (pop (p-temp-stk (p)))),

p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

'run)
;  (JUMP lab)           Jump to the location named by lab in the current
;                       program.

Definition: p-jump-okp (ins, p) = t

Definition: p-jump-step (ins, p) = p-state (pc (cadr (ins), p-current-program (p)),

p-ctrl-stk (p), p-temp-stk (p), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

'run)
;   (JUMP-CASE lab0 lab1 ... labn)
;                       Pop top of temp-stk.  It must be a some nat, i.
;                       Jump to labi.

Definition: p-jump-case-okp (ins, p) = (listp (p-temp-stk (p))

∧ p-objectp-type ('nat, top (p-temp-stk (p)), p) ∧ (untag (top (p-temp-stk (p))) < length (cdr (ins))))

Definition: p-jump-case-step (ins, p) = p-state (pc (get (untag (top (p-temp-stk (p))), cdr (ins)),

p-current-program (p)), p-ctrl-stk (p), pop (p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;  (SET-LOCAL var)      Set the local variable var to the top of the temp-stk
;                       but do not pop the temp-stk.

Definition: p-set-local-okp (ins, p) = listp (p-temp-stk (p))

Definition: p-set-local-step (ins, p) = p-state (add1-p-pc (p),

set-local-var-value (top (p-temp-stk (p)), cadr (ins), p-ctrl-stk (p)),

p-temp-stk (p), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
; (TEST-type-AND-JUMP flg lab)
;                       Each instruction in this family pops one item, x, off
;                       temp-stk.  The item must be of the indicated type.
;                       The item is tested as indicated by the flg.  If the
;                       test is satisfied, we jump to the indicated label, lab.
;                       Otherwise, the next instruction is executed.  The

;                       flags and tests available depend upon the type.
;                       We enumerate them in the documentation for each
;                       test-and-jump instruction.
;  For each member of the family I define p-test-xxx-and-jump-okp,
;  which approves the execution of the instruction.  Then I define
;  p-test-xxx-and-jump-step and
;  icode-test-xxx-and-jump.  Both the -okp and the
;  -step function are defined in terms of more general purpose functions.

Definition: p-test-and-jump-okp (ins, type, test, p) = (listp (p-temp-stk (p)) ∧ p-objectp-type (type, top (p-temp-stk (p)), p))

Definition: p-test-and-jump-step (test, lab, p) = if test

then p-state (pc (lab, p-current-program (p)), p-ctrl-stk (p), pop (p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

               'run)

else p-state (add1-p-pc (p), p-ctrl-stk (p), pop (p-temp-stk (p)), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p), 'run) endif

; (TEST-NAT-AND-JUMP flg lab)
;                          flg                test
;                          ZERO          jump if x is 0
;                      NOT-ZERO          jump if x is not 0

Definition: p-test-natp (flg, x) = case on flg:

case = zero then x = 0 otherwise x ≠ 0 endcase

Definition: p-test-nat-and-jump-okp (ins, p) = p-test-and-jump-okp (ins,

                      'nat,

p-test-natp (cadr (ins), untag (top (p-temp-stk (p)))), p)

Definition: p-test-nat-and-jump-step (ins, p) = p-test-and-jump-step (p-test-natp (cadr (ins), untag (top (p-temp-stk (p)))),

caddr (ins), p)

; (TEST-INT-AND-JUMP flg lab)
;                          flg                test
;                          ZERO          jump if x is 0
;                      NOT-ZERO          jump if x is not 0
;                          NEG           jump if x is negative
;                      NOT-NEG           jump if x is not negative
;                          POS           jump if x is positive
;                      NOT-POS           jump if x is not positive

Definition: p-test-intp (flg, x) = case on flg:

case = zero then x = 0 case = not-zero then x ≠ 0 case = neg then negativep (x) case = not-neg then ¬ negativep (x) case = pos then (x ∈ N) ∧ (x ≠ 0) otherwise (x = 0) ∨ negativep (x) endcase Definition: p-test-int-and-jump-okp (ins, p) = p-test-and-jump-okp (ins,

                      'int,

p-test-intp (cadr (ins), untag (top (p-temp-stk (p)))), p)

Definition: p-test-int-and-jump-step (ins, p) = p-test-and-jump-step (p-test-intp (cadr (ins), untag (top (p-temp-stk (p)))),

caddr (ins), p)

; (TEST-BOOL-AND-JUMP flg lab)
;                          flg                test
;                          T            jump if x is T
;                          F            jump if x is F

Definition: p-test-boolp (flg, x) = case on flg:

case = t then x = 't otherwise x = 'f endcase

Definition: p-test-bool-and-jump-okp (ins, p) = p-test-and-jump-okp (ins,

                      'bool,

p-test-boolp (cadr (ins), untag (top (p-temp-stk (p)))), p)

Definition: p-test-bool-and-jump-step (ins, p) = p-test-and-jump-step (p-test-boolp (cadr (ins), untag (top (p-temp-stk (p)))),

caddr (ins), p)

;   (NO-OP)             Do nothing.  Advance the pc to the next instruction.

Definition: p-no-op-okp (ins, p) = t

Definition: p-no-op-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p), p-temp-stk (p), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;   (EQ)                Pop top and top1 off of temp-stk.  If they
;                       are both of the same type, push T or F according
;                       to whether they are equal.

Definition: p-eq-okp (ins, p) = (listp (p-temp-stk (p))

∧ listp (pop (p-temp-stk (p)))

∧ (type (top (p-temp-stk (p))) = type (top1 (p-temp-stk (p)))))

Definition: p-eq-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (bool (untag (top1 (p-temp-stk (p)))

= untag (top (p-temp-stk (p)))), pop (pop (p-temp-stk (p)))),

p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;   (ADD-INT-WITH-CARRY)
;                       Pop three things off temp stack, top, top1 and
;                       top2.  Top and top1 must be INTs.  Top2 must
;                       be Boolean.  Add top+top1+top2 -- coercing T to 1
;                       and F to 0.  Push two results.  First, a boolean
;                       indicating whether top+top1+top2 is not small.
;                       On top of that, push the corrected sum.  The corrected
;                       sum is the sum, if that is a small-integerp; the
;                       sum+2**word-size, if the sum is not small and is

;                       negative; and the sum-2**word-size, if the sum is
;                       not small and not negative.

Definition: p-add-int-with-carry-okp (ins, p) = (listp (p-temp-stk (p))

∧ listp (pop (p-temp-stk (p)))

∧ listp (pop (pop (p-temp-stk (p))))

∧ p-objectp-type ('int, top (p-temp-stk (p)), p) ∧ p-objectp-type ('int, top1 (p-temp-stk (p)), p) ∧ p-objectp-type ('bool, top2 (p-temp-stk (p)), p))

Definition: p-add-int-with-carry-step (ins, p) = let sum be iplus (bool-to-nat (untag (top2 (p-temp-stk (p)))),

iplus (untag (top1 (p-temp-stk (p))),

untag (top (p-temp-stk (p)))))

in

p-state (add1-p-pc (p), p-ctrl-stk (p), push (tag ('int, fix-small-integer (sum, p-word-size (p))),

push (bool (¬ small-integerp (sum, p-word-size (p))),

pop (pop (pop (p-temp-stk (p)))))),

p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p), 'run) endlet

;;  (SUB-INT)

Definition: p-sub-int-okp (ins, p) = (listp (p-temp-stk (p))

∧ listp (pop (p-temp-stk (p)))

∧ p-objectp-type ('int, top (p-temp-stk (p)), p) ∧ p-objectp-type ('int, top1 (p-temp-stk (p)), p) ∧ small-integerp (idifference (untag (top1 (p-temp-stk (p))),

untag (top (p-temp-stk (p)))),

p-word-size (p)))

Definition: p-sub-int-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p), push (tag ('int,

idifference (untag (top1 (p-temp-stk (p))),

untag (top (p-temp-stk (p))))),

pop (pop (p-temp-stk (p)))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;   (SUB-INT-WITH-CARRY)
;                       Pop three things off temp stack, top, top1 and
;                       top2.  Top and top1 must be INTs.  Top2 must
;                       be Boolean.  Form top1-(top+top2) -- coercing T to 1
;                       and F to 0.  Push two results.  First, a boolean
;                       indicating whether top1-(top+top2) is not small.
;                       On top of that, push the corrected diff. The corrected
;                       diff is the diff, if that is a small-integerp; the
;                       diff+2**word-size, if the diff is not small and is
;                       negative; and the diff-2**word-size, if the diff is
;                       not small and not negative.

Definition: p-sub-int-with-carry-okp (ins, p) = (listp (p-temp-stk (p))

∧ listp (pop (p-temp-stk (p)))

∧ listp (pop (pop (p-temp-stk (p))))

∧ p-objectp-type ('int, top (p-temp-stk (p)), p) ∧ p-objectp-type ('int, top1 (p-temp-stk (p)), p) ∧ p-objectp-type ('bool, top2 (p-temp-stk (p)), p))

Definition: p-sub-int-with-carry-step (ins, p) = let diff be idifference (untag (top1 (p-temp-stk (p))),

iplus (untag (top (p-temp-stk (p))),

bool-to-nat (untag (top2 (p-temp-stk (p))))))

in

p-state (add1-p-pc (p), p-ctrl-stk (p), push (tag ('int, fix-small-integer (diff , p-word-size (p))), push (bool (¬ small-integerp (diff , p-word-size (p))), pop (pop (pop (p-temp-stk (p)))))),

p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p), 'run) endlet

;   (NEG-INT)           Pop top of temp-stk.  It must be an INT.
;                       Negate it and push the result provided it is
;                       representable as an INT.

Definition: p-neg-int-okp (ins, p) = (listp (p-temp-stk (p))

∧ p-objectp-type ('int, top (p-temp-stk (p)), p) ∧ small-integerp (inegate (untag (top (p-temp-stk (p)))),

p-word-size (p)))

Definition: p-neg-int-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p), push (tag ('int, inegate (untag (top (p-temp-stk (p))))),

pop (p-temp-stk (p))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

'run)
;   (LT-INT)            Pop top and top1 off of temp-stk, and push T or F
;                       according to whether top1 < top.

Definition: p-lt-int-okp (ins, p) = (listp (p-temp-stk (p))

∧ listp (pop (p-temp-stk (p))) ∧ p-objectp-type ('int, top (p-temp-stk (p)), p) ∧ p-objectp-type ('int, top1 (p-temp-stk (p)), p))

Definition: p-lt-int-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (bool (ilessp (untag (top1 (p-temp-stk (p))),

untag (top (p-temp-stk (p))))),

pop (pop (p-temp-stk (p)))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;   (INT-TO-NAT)        Pop top off of temp-stk.  Top should
;                       be of type INT and be nonnegative.
;                       Push the NAT corresponding to top.

Definition: p-int-to-nat-okp (ins, p) = (listp (p-temp-stk (p))

∧ p-objectp-type ('int, top (p-temp-stk (p)), p) ∧ (¬ negativep (untag (top (p-temp-stk (p))))))

Definition: p-int-to-nat-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (tag ('nat, untag (top (p-temp-stk (p)))), pop (p-temp-stk (p))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;   (ADD-NAT)           Pop top and top1 off of temp-stk.
;                       Both top and top1 must be NATs.  Push
;                       their NAT sum.

Definition: p-add-nat-okp (ins, p) = (listp (p-temp-stk (p))

∧ listp (pop (p-temp-stk (p)))

∧ p-objectp-type ('nat, top (p-temp-stk (p)), p) ∧ p-objectp-type ('nat, top1 (p-temp-stk (p)), p) ∧ small-naturalp (untag (top1 (p-temp-stk (p)))

+ untag (top (p-temp-stk (p))), p-word-size (p)))

Definition: p-add-nat-step (ins, p) = let sum be untag (top1 (p-temp-stk (p)))

+ untag (top (p-temp-stk (p)))

in

p-state (add1-p-pc (p), p-ctrl-stk (p), push (tag ('nat, sum), pop (pop (p-temp-stk (p)))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p), 'run) endlet

;   (SUB-NAT)           Pop top, top1 off of temp-stk.
;                       Both top and top1 must be NATs.
;                       If top1 >= top
;                          then push top1-top.
;                       Else, error.

Definition: p-sub-nat-okp (ins, p) = (listp (p-temp-stk (p))

∧ listp (pop (p-temp-stk (p)))

∧ p-objectp-type ('nat, top (p-temp-stk (p)), p) ∧ p-objectp-type ('nat, top1 (p-temp-stk (p)), p) ∧ (untag (top1 (p-temp-stk (p))) ≮ untag (top (p-temp-stk (p)))))

Definition: p-sub-nat-step (ins, p) = let y be untag (top (p-temp-stk (p))),

x be untag (top1 (p-temp-stk (p))) in p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (tag ('nat, x − y), pop (pop (p-temp-stk (p)))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p), 'run) endlet

;   (SUB1-NAT)          Pop top off of temp-stk.
;                       Top must be a NAT other than
;                       0.  Push top-1.

Definition: p-sub1-nat-okp (ins, p) = (listp (p-temp-stk (p))

∧ p-objectp-type ('nat, top (p-temp-stk (p)), p) ∧ (untag (top (p-temp-stk (p))) ≄ 0))

Definition: p-sub1-nat-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (tag ('nat, untag (top (p-temp-stk (p))) − 1),

pop (p-temp-stk (p))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;   (OR-BOOL)           Pop top and top1 off of temp-stk, or them together
;                       and push the result.

Definition: p-or-bool-okp (ins, p) = (listp (p-temp-stk (p))

∧ listp (pop (p-temp-stk (p)))

∧ p-objectp-type ('bool, top (p-temp-stk (p)), p) ∧ p-objectp-type ('bool, top1 (p-temp-stk (p)), p))

Definition: p-or-bool-step (ins, p) = p-state (add1-p-pc (p), p-ctrl-stk (p), push (tag ('bool,

or-bool (untag (top1 (p-temp-stk (p))),

untag (top (p-temp-stk (p))))),

pop (pop (p-temp-stk (p)))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

'run)
;   (AND-BOOL)          Pop top and top1 off of temp-stk, and them together
;                       and push the result.
;

Definition: p-and-bool-okp (ins, p) = (listp (p-temp-stk (p))

∧ listp (pop (p-temp-stk (p))) ∧ p-objectp-type ('bool, top (p-temp-stk (p)), p) ∧ p-objectp-type ('bool, top1 (p-temp-stk (p)), p))

Definition: p-and-bool-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p), push (tag ('bool,

and-bool (untag (top1 (p-temp-stk (p))),

untag (top (p-temp-stk (p))))),

pop (pop (p-temp-stk (p)))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

'run)
;   (NOT-BOOL)          Pop top of temp-stk, not it, and push the result.

Definition: p-not-bool-okp (ins, p) = (listp (p-temp-stk (p))

∧ p-objectp-type ('bool, top (p-temp-stk (p)), p))

Definition: p-not-bool-step (ins, p) = p-state (add1-p-pc (p),

p-ctrl-stk (p),

push (tag ('bool, not-bool (untag (top (p-temp-stk (p))))),

pop (p-temp-stk (p))), p-prog-segment (p), p-data-segment (p), p-max-ctrl-stk-size (p), p-max-temp-stk-size (p), p-word-size (p),

          'run)
;;(defn piton-opcodes nil
;;  '(call ret push-constant push-local push-global
;;    push-temp-stk-index pop pop* pop-local pop-global
;;    fetch-temp-stk deposit-temp-stk jump jump-case set-local
;;    test-nat-and-jump test-int-and-jump test-bool-and-jump no-op
;;    eq add-int-with-carry sub-int sub-int-with-carry neg-int
;;    lt-int int-to-nat add-nat sub-nat sub1-nat lt-nat or-bool and-bool
;;    not-bool))
; The following function generates the name of the error
; message produced when an illegal instruction is hit.  The
; first argument is the ``level'' name, e.g., 'P or 'R.
; the (cdr (unpack 'g-instruction)) is used instead of
; (unpack '-instruction) only because '-instruction is an
; illegal evg in the logic, since it does not start with an
; alphabetic character.

Definition: x-y-error-msg (x, y) = pack (append (unpack ('illegal-),

append (unpack (y), cdr (unpack ('g-instruction)))))

; The function checks that it is legal to execute ins in state
; p:

Definition: p-ins-okp (ins, p) = case on car (ins):

case = call

then p-call-okp (ins, p) case = ret then p-ret-okp (ins, p) case = push-constant then p-push-constant-okp (ins, p) case = push-local then p-push-local-okp (ins, p) case = push-global then p-push-global-okp (ins, p) case = push-temp-stk-index then p-push-temp-stk-index-okp (ins, p) case = pop then p-pop-okp (ins, p) case = pop* then p-pop*-okp (ins, p) case = pop-local then p-pop-local-okp (ins, p) case = pop-global then p-pop-global-okp (ins, p) case = fetch-temp-stk then p-fetch-temp-stk-okp (ins, p) case = deposit-temp-stk then p-deposit-temp-stk-okp (ins, p) case = jump then p-jump-okp (ins, p) case = jump-case then p-jump-case-okp (ins, p) case = set-local then p-set-local-okp (ins, p) case = test-nat-and-jump then p-test-nat-and-jump-okp (ins, p) case = test-int-and-jump then p-test-int-and-jump-okp (ins, p) case = test-bool-and-jump then p-test-bool-and-jump-okp (ins, p) case = no-op then p-no-op-okp (ins, p) case = eq then p-eq-okp (ins, p) case = add-int-with-carry then p-add-int-with-carry-okp (ins, p) case = sub-int then p-sub-int-okp (ins, p) case = sub-int-with-carry then p-sub-int-with-carry-okp (ins, p) case = neg-int then p-neg-int-okp (ins, p) case = lt-int then p-lt-int-okp (ins, p) case = int-to-nat then p-int-to-nat-okp (ins, p) case = add-nat then p-add-nat-okp (ins, p) case = sub-nat then p-sub-nat-okp (ins, p) case = sub1-nat then p-sub1-nat-okp (ins, p) case = or-bool then p-or-bool-okp (ins, p) case = and-bool then p-and-bool-okp (ins, p) case = not-bool then p-not-bool-okp (ins, p) otherwise f endcase

; If ins is legal, the following function steps the state forward one.

Definition: p-ins-step (ins, p) = case on car (ins):

case = call then p-call-step (ins, p) case = ret then p-ret-step (ins, p) case = push-constant then p-push-constant-step (ins, p) case = push-local then p-push-local-step (ins, p) case = push-global then p-push-global-step (ins, p) case = push-temp-stk-index then p-push-temp-stk-index-step (ins, p) case = pop then p-pop-step (ins, p) case = pop* then p-pop*-step (ins, p) case = pop-local then p-pop-local-step (ins, p) case = pop-global then p-pop-global-step (ins, p) case = fetch-temp-stk then p-fetch-temp-stk-step (ins, p) case = deposit-temp-stk then p-deposit-temp-stk-step (ins, p) case = jump then p-jump-step (ins, p) case = jump-case then p-jump-case-step (ins, p) case = set-local then p-set-local-step (ins, p) case = test-nat-and-jump then p-test-nat-and-jump-step (ins, p) case = test-int-and-jump then p-test-int-and-jump-step (ins, p) case = test-bool-and-jump then p-test-bool-and-jump-step (ins, p) case = no-op then p-no-op-step (ins, p) case = eq then p-eq-step (ins, p) case = add-int-with-carry then p-add-int-with-carry-step (ins, p) case = sub-int then p-sub-int-step (ins, p) case = sub-int-with-carry then p-sub-int-with-carry-step (ins, p) case = neg-int then p-neg-int-step (ins, p) case = lt-int then p-lt-int-step (ins, p) case = int-to-nat then p-int-to-nat-step (ins, p) case = add-nat then p-add-nat-step (ins, p) case = sub-nat then p-sub-nat-step (ins, p) case = sub1-nat then p-sub1-nat-step (ins, p) case = or-bool then p-or-bool-step (ins, p) case = and-bool then p-and-bool-step (ins, p) case = not-bool then p-not-bool-step (ins, p) otherwise p-halt (p, 'run) endcase

; We now package these up into a single function that takes an
; instruction and a state and returns the result of executing the
; given instruction in the state or causing an error.

Definition: p-step1 (ins, p) = if p-ins-okp (ins, p) then p-ins-step (ins, p)

else p-halt (p, x-y-error-msg ('p, car (ins))) endif

; Of course, we are only interested in executing the current
; instruction of a state.  That is what we call stepping the state.

Definition: p-step (p) = if p-psw (p) = 'run then p-step1 (p-current-instruction (p), p)

else p endif

Event: Disable p-step.

; Note that p-step is a no-op if the psw is anything besides RUN.
; And given the ability to step a state, here is how you step it n
; times.

Definition: p (p, n) = if n ≃ 0 then p

else p (p-step (p), n − 1) endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                       Lemmas on Piton                       ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Event: Disable p-step.

Event: Disable p-halt.

Event: Disable p-ins-step.

Event: Disable p-ins-okp.

Event: Disable p-step1.

Event: Disable x-y-error-msg.

Theorem: p-step-expansion p-step (p-state (pc,

ctr-stk, temp-stk, prog-seg, data-seg, p-max-ctrl-stk-size, p-max-temp-stk-size, p-word-size, psw))

= if psw = 'run

then p-step1 (p-current-instruction (p-state (pc, ctr-stk, temp-stk, prog-seg, data-seg, p-max-ctrl-stk-size, p-max-temp-stk-size, p-word-size, psw)),

p-state (pc, ctr-stk, temp-stk, prog-seg, data-seg, p-max-ctrl-stk-size, p-max-temp-stk-size, p-word-size, psw))

else p-state (pc, ctr-stk, temp-stk, prog-seg, data-seg, p-max-ctrl-stk-size, p-max-temp-stk-size, p-word-size, psw) endif

Theorem: p-ins-step-expansion p-ins-step (cons (pack (opr), args), p) = case on pack (opr):

case = call then p-call-step (cons (pack (opr), args), p) case = ret then p-ret-step (cons (pack (opr), args), p) case = push-constant then p-push-constant-step (cons (pack (opr), args), p) case = push-local then p-push-local-step (cons (pack (opr), args), p) case = push-global then p-push-global-step (cons (pack (opr), args), p) case = push-temp-stk-index then p-push-temp-stk-index-step (cons (pack (opr), args), p) case = pop then p-pop-step (cons (pack (opr), args), p) case = pop* then p-pop*-step (cons (pack (opr), args), p) case = pop-local then p-pop-local-step (cons (pack (opr), args), p) case = pop-global then p-pop-global-step (cons (pack (opr), args), p) case = fetch-temp-stk then p-fetch-temp-stk-step (cons (pack (opr), args), p) case = deposit-temp-stk then p-deposit-temp-stk-step (cons (pack (opr), args), p) case = jump then p-jump-step (cons (pack (opr), args), p) case = jump-case then p-jump-case-step (cons (pack (opr), args), p) case = set-local then p-set-local-step (cons (pack (opr), args), p) case = test-nat-and-jump then p-test-nat-and-jump-step (cons (pack (opr), args), p) case = test-int-and-jump then p-test-int-and-jump-step (cons (pack (opr), args), p) case = test-bool-and-jump then p-test-bool-and-jump-step (cons (pack (opr), args), p) case = no-op then p-no-op-step (cons (pack (opr), args), p) case = eq then p-eq-step (cons (pack (opr), args), p) case = add-int-with-carry then p-add-int-with-carry-step (cons (pack (opr), args), p) case = sub-int then p-sub-int-step (cons (pack (opr), args), p) case = sub-int-with-carry then p-sub-int-with-carry-step (cons (pack (opr), args), p) case = neg-int then p-neg-int-step (cons (pack (opr), args), p) case = lt-int then p-lt-int-step (cons (pack (opr), args), p) case = int-to-nat then p-int-to-nat-step (cons (pack (opr), args), p) case = add-nat then p-add-nat-step (cons (pack (opr), args), p) case = sub-nat then p-sub-nat-step (cons (pack (opr), args), p) case = sub1-nat then p-sub1-nat-step (cons (pack (opr), args), p) case = or-bool then p-or-bool-step (cons (pack (opr), args), p) case = and-bool then p-and-bool-step (cons (pack (opr), args), p) case = not-bool then p-not-bool-step (cons (pack (opr), args), p) otherwise p-halt (p, 'run) endcase

Theorem: p-ins-okp-expansion p-ins-okp (cons (pack (opr), args), p) = case on pack (opr):

case = call then p-call-okp (cons (pack (opr), args), p) case = ret then p-ret-okp (cons (pack (opr), args), p) case = push-constant then p-push-constant-okp (cons (pack (opr), args), p) case = push-local then p-push-local-okp (cons (pack (opr), args), p) case = push-global then p-push-global-okp (cons (pack (opr), args), p) case = push-temp-stk-index then p-push-temp-stk-index-okp (cons (pack (opr), args), p) case = pop then p-pop-okp (cons (pack (opr), args), p) case = pop* then p-pop*-okp (cons (pack (opr), args), p) case = pop-local then p-pop-local-okp (cons (pack (opr), args), p) case = pop-global then p-pop-global-okp (cons (pack (opr), args), p) case = fetch-temp-stk then p-fetch-temp-stk-okp (cons (pack (opr), args), p) case = deposit-temp-stk then p-deposit-temp-stk-okp (cons (pack (opr), args), p) case = jump then p-jump-okp (cons (pack (opr), args), p) case = jump-case then p-jump-case-okp (cons (pack (opr), args), p) case = set-local then p-set-local-okp (cons (pack (opr), args), p) case = test-nat-and-jump then p-test-nat-and-jump-okp (cons (pack (opr), args), p) case = test-int-and-jump then p-test-int-and-jump-okp (cons (pack (opr), args), p) case = test-bool-and-jump then p-test-bool-and-jump-okp (cons (pack (opr), args), p) case = no-op then p-no-op-okp (cons (pack (opr), args), p) case = eq then p-eq-okp (cons (pack (opr), args), p) case = add-int-with-carry then p-add-int-with-carry-okp (cons (pack (opr), args), p) case = sub-int then p-sub-int-okp (cons (pack (opr), args), p) case = sub-int-with-carry then p-sub-int-with-carry-okp (cons (pack (opr), args), p) case = neg-int then p-neg-int-okp (cons (pack (opr), args), p) case = lt-int then p-lt-int-okp (cons (pack (opr), args), p) case = int-to-nat then p-int-to-nat-okp (cons (pack (opr), args), p) case = add-nat then p-add-nat-okp (cons (pack (opr), args), p) case = sub-nat then p-sub-nat-okp (cons (pack (opr), args), p) case = sub1-nat then p-sub1-nat-okp (cons (pack (opr), args), p) case = or-bool then p-or-bool-okp (cons (pack (opr), args), p) case = and-bool then p-and-bool-okp (cons (pack (opr), args), p) case = not-bool then p-not-bool-okp (cons (pack (opr), args), p) otherwise f endcase

Theorem: p-0-unwinding-lemma p (s, 0) = s

Theorem: p-plus-lemma p (state, j + k) = p (p (state, j ), k)

Theorem: p-add1 p (state, 1 + x) = p (p (state, x), 1)

Event: Disable p-add1.

Theorem: p-rearrange-times-lemma p (p (state, k), j ) = p (p (state, j ), k)

Event: Disable p-rearrange-times-lemma.

Theorem: p-add1-3 p (state, 1 + x) = p (p-step (state), x)

Theorem: find-label-append (¬ find-labelp (label, code1 )) → (find-label (label, append (code1 , code2 ))

= (length (code1 ) + find-label (label, code2 )))

Event: Disable find-label-append.

Theorem: find-labelp-append2 find-labelp (n, append (lst1 , lst2 )) = (find-labelp (n, lst1 ) ∨ find-labelp (n, lst2 ))

Event: Disable find-labelp-append2. Theorem: rget-inverts-rput rget (n, rput (value, n, lst)) = value Theorem: rput-same-value-doesnt-disturb-temp-stk (n = length (temp-stk)) → (rput (value, n, append (lst, cons (value, temp-stk)))

= append (lst, cons (value, temp-stk))) Event: Disable ilessp. Event: Disable not-bool. Event: Disable and-bool. Event: Disable or-bool. Event: Disable inegate. Event: Disable fix-small-integer. Event: Disable iplus. Event: Disable idifference. Event: Make the library "c2".

Index

add-addr, 4 add-adp, 2–4 add1-addr, 4, 10, 13 add1-adp, 3 add1-nat, 5 add1-p-pc, 10, 14–21, 24–32 adp-name, 2–4 adp-name-cons, 2 adp-offset, 2–4 adp-offset-cons, 2 adpp, 2, 9 and-bool, 5, 31 area-name, 4, 10

bindings, 10, 11 bindings-frame, 10 bool, 5, 24, 25, 27, 28 bool-to-nat, 6, 25, 26 booleanp, 5, 9

car-cdr-push, 7

definedp, 2, 9 definition, 1, 2, 10, 13 deposit, 5, 18 deposit-adp, 3, 5

exp, 5, 6

fetch, 5, 15 fetch-adp, 3, 5 find-label, 9, 41 find-label-append, 41 find-labelp, 8, 41 find-labelp-append2, 41 first-n, 11, 12 first-n-add1, 11 first-n-append2, 11 first-n-plus-append, 11 fix-small-integer, 6, 25, 26 formal-vars, 2, 13 get, 3, 10, 20

idifference, 25, 26

ilessp, 6, 28 inegate, 27 integerp, 6 iplus, 6, 25, 26

labelledp, 8, 9

labelledp-expansion, 8

length, 2, 3, 7, 10–20, 41, 42 length-pair-temps-with-initial-v

alues, 12 length-pairlist, 11 length-push, 7 local-var-value, 10, 15

make-p-call-frame, 12, 13

not-bool, 5, 32

offset, 4, 10 or-bool, 5, 31

p, 36, 41

p-0-unwinding-lemma, 41

p-add-int-with-carry-okp, 25, 33, 40 p-add-int-with-carry-step, 25, 35, 39 p-add-nat-okp, 28, 34, 41 p-add-nat-step, 29, 35, 39 p-add1, 41 p-add1-3, 41 p-and-bool-okp, 31, 34, 41 p-and-bool-step, 31, 35, 39 p-call-okp, 13, 32, 39 p-call-step, 13, 34, 38 p-ctrl-stk, 1, 13–21, 24–32 p-ctrl-stk-size, 10, 13 p-current-instruction, 10, 36, 37 p-current-program, 10, 14, 19–21 p-data-segment, 1, 9, 13–21, 24–32 p-deposit-temp-stk-okp, 19, 33, 40 p-deposit-temp-stk-step, 19, 35, 38 p-eq-okp, 24, 33, 40 p-eq-step, 24, 35, 39 p-fetch-temp-stk-okp, 18, 33, 40 p-fetch-temp-stk-step, 18, 35, 38 p-frame, 10–12 p-frame-size, 10 p-halt, 1, 14, 36, 39 p-ins-okp, 32, 36, 39 p-ins-okp-expansion, 39 p-ins-step, 34, 36, 38 p-ins-step-expansion, 38 p-int-to-nat-okp, 28, 34, 40 p-int-to-nat-step, 28, 35, 39 p-jump-case-okp, 20, 33, 40 p-jump-case-step, 20, 35, 38 p-jump-okp, 19, 33, 40 p-jump-step, 19, 35, 38 p-lt-int-okp, 27, 34, 40 p-lt-int-step, 28, 35, 39 p-max-ctrl-stk-size, 1, 13–21, 24–32 p-max-temp-stk-size, 1, 13–21, 24–

32 p-neg-int-okp, 27, 34, 40 p-neg-int-step, 27, 35, 39 p-no-op-okp, 23, 33, 40 p-no-op-step, 23, 24, 35, 39 p-not-bool-okp, 31, 34, 41 p-not-bool-step, 32, 36, 39 p-objectp, 9 p-objectp-type, 9, 18–21, 25–31 p-or-bool-okp, 30, 34, 41 p-or-bool-step, 30, 35, 39 p-pc, 1, 10, 13 p-plus-lemma, 41 p-pop*-okp, 17, 33, 40 p-pop*-step, 17, 34, 38 p-pop-global-okp, 18, 33, 40 p-pop-global-step, 18, 35, 38 p-pop-local-okp, 17, 33, 40 p-pop-local-step, 17, 34, 38 p-pop-okp, 16, 33, 40 p-pop-step, 16, 34, 38 p-prog-segment, 1, 9, 10, 13–21, 24–

32 p-psw, 36 p-push-constant-okp, 14, 33, 39 p-push-constant-step, 14, 34, 38 p-push-global-okp, 15, 33, 40 p-push-global-step, 15, 34, 38 p-push-local-okp, 15, 33, 39 p-push-local-step, 15, 34, 38 p-push-temp-stk-index-okp, 16, 33,

40 p-push-temp-stk-index-step, 16, 34,

38 p-rearrange-times-lemma, 41 p-ret-okp, 13, 33, 39 p-ret-step, 13, 34, 38 p-set-local-okp, 20, 33, 40 p-set-local-step, 20, 35, 38 p-state, 1, 13–21, 24–32, 37, 38 p-step, 36, 37, 41 p-step-expansion, 37 p-step1, 36, 37 p-sub-int-okp, 25, 33, 40 p-sub-int-step, 25, 26, 35, 39 p-sub-int-with-carry-okp, 26, 33, 40 p-sub-int-with-carry-step, 26, 35, 39 p-sub-nat-okp, 29, 34, 41 p-sub-nat-step, 29, 35, 39 p-sub1-nat-okp, 30, 34, 41 p-sub1-nat-step, 30, 35, 39 p-temp-stk, 1, 13–32 p-test-and-jump-okp, 21–23 p-test-and-jump-step, 21–23 p-test-bool-and-jump-okp, 23, 33, 40 p-test-bool-and-jump-step, 23, 35, 39 p-test-boolp, 23 p-test-int-and-jump-okp, 23, 33, 40 p-test-int-and-jump-step, 23, 35, 39 p-test-intp, 22, 23 p-test-nat-and-jump-okp, 22, 33, 40 p-test-nat-and-jump-step, 22, 35, 38 p-test-natp, 22 p-word-size, 1, 9, 13–21, 24–32 pair-formal-vars-with-actuals, 12 pair-temps-with-initial-values, 12 pairlist, 11 pairlist-distributes, 11 pairlist-plistp, 11 pc, 9, 14, 19–21 pcpp, 2, 9 plistp, 11 pop, 6, 7, 11, 13, 14, 16–21, 24–32 pop-cons, 7 pop-push, 7 popn, 6, 7, 13, 17 popn-add1, 6 popn-length, 7 popn-plus, 7 popn-zero, 7 program-body, 2, 9, 10 push, 6, 7, 11, 13–16, 18, 24–32 push-listp, 7 put, 3 put-assoc, 2 put-value, 2, 3, 11

ret-pc, 10, 11, 14 ret-pc-frame, 10 reverse, 12 rget, 3, 18, 42 rget-inverts-rput, 42 rput, 3, 19, 42 rput-preserves-length, 3 rput-same-value-doesnt-disturb-te

mp-stk, 42

set-local-var-value, 11, 17, 20 small-integerp, 6, 9, 25, 27 small-naturalp, 5, 9, 29 sub-addr, 4, 5 sub-adp, 3, 4 sub1-addr, 5

tag, 4, 5, 9, 13, 15, 16, 18, 25–32 temp-var-dcls, 2, 13 top, 6, 7, 10, 11, 14, 17–32 top-cons, 7 top-push, 7 top1, 7, 19, 24–31 top1-push, 7 top2, 7, 25, 26 top2-push, 7 type, 4, 9, 24 type-expansion, 4 type-tag, 4

unabbreviate-constant, 14 unlabel, 8, 10 unlabel-expansion, 8 unlabel-unlabelledp, 8 untag, 4, 5, 9, 18–20, 22–32 untag-add1-nat, 5 untag-cons, 4 untag-tag, 4

value, 2, 3, 10

x-y-error-msg, 32, 36