#|
 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.
|#
; An NQTHM Formalization of a Small Machine
; by J Strother Moore II
; May 30, 1991
; This file serves as a good introduction to the Nqthm approach to
; language semantics.  We have carried out this approach on much larger
; examples than presented here.  It is, for example, that used at all
; levels of the CLI short stack (hardware description language, machine
; language, assembly language, high-level language).  The semantics of those
; levels are so large and complicated that it is difficult to see the
; basic ideas.  Those ideas are highlighted here simply by dealing with
; a trivial language.
; This is a list of events to be processed by NQTHM starting from the
; GROUND-ZERO state.  In it I develop
; (a) an operational semantics for a simple programming language
; (b) a program that implements multiplication by repeated addition
; (c) a proof of the correctness of the multiplication program

;     directly from the "operational" semantics
; (d) a program that does exponentiation and uses the multiplier
; (e) a proof of the correctness of the exponentiation program
; (f) the most general correctness theorem about the multiplier
; (g) the definition and correctness of the "McCarthy" functional
;     semantics of the multiplier
; (h) a proof of the correctness of the multiplier by the inductive
;     assertion method.
; (i) May 13, 1992.  a proof of the general theorem that our
;     standard form of a correctness result for a subroutine
;     implies our standard form of a termination result.  This
;     part of the file is not part of the tutorial because the
;     proof is pretty messy.
; The programming language is not particularly elegant.  Its only
; redeeming features are that its semantics is easily written down and
; it lets me illustrate the points I'm trying to make.  This is by no
; means a complete or exemplary "library" for dealing with programs in
; this language; I have in fact kept the facts to a bare minimum.
; We start by defining our "small machine."

Event: Start with the initial nqthm theory.

; States are represented by the following shell objects:

Event: Add the shell st, with recognizer function symbol stp and 5 accessors: pc, with type restriction (none-of) and default value zero; stk, with type restriction (none-of) and default value zero; mem, with type restriction (none-of) and default value zero; haltedp, with type restriction (none-of) and default value zero; defs, with type restriction (none-of) and default value zero.

; Utility Functions

Definition: add1-pc (pc) = cons (car (pc), 1 + cdr (pc))

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

else get (n − 1, cdr (lst)) endif Definition: put (n, v, lst) = if n ≃ 0 then cons (v, cdr (lst))

else cons (car (lst), put (n − 1, v, cdr (lst))) endif

Definition: fetch (pc, defs) = get (cdr (pc), cdr (assoc (car (pc), defs)))

; The Semantics of Individual Instructions
; Move Instructions

Definition: move (addr1 , addr2 , s) = st (add1-pc (pc (s)),

stk (s),

put (addr1 , get (addr2 , mem (s)), mem (s)),

f,

defs (s))

Definition: movi (addr, val, s) = st (add1-pc (pc (s)), stk (s), put (addr, val, mem (s)), f, defs (s))

; Arithmetic Instructions

Definition: add (addr1 , addr2 , s) = st (add1-pc (pc (s)),

stk (s),

put (addr1 , get (addr1 , mem (s)) + get (addr2 , mem (s)), mem (s)), f, defs (s))

Definition: subi (addr, val, s) = st (add1-pc (pc (s)),

stk (s),

put (addr, get (addr, mem (s)) − val, mem (s)),

f,

defs (s))

; Jump Instructions

Definition: jumpz (addr, pc, s) = st (if get (addr, mem (s)) ≃ 0 then cons (car (pc (s)), pc)

else add1-pc (pc (s)) endif, stk (s), mem (s), f, defs (s))

Definition: jump (pc, s) = st (cons (car (pc (s)), pc), stk (s), mem (s), f, defs (s))

; Subroutine Call and Return

Definition: call (subr, s) = st (cons (subr, 0), cons (add1-pc (pc (s)), stk (s)), mem (s), f, defs (s))

Definition: ret (s) = if stk (s) ≃ nil then st (pc (s), stk (s), mem (s), t, defs (s))

else st (car (stk (s)), cdr (stk (s)), mem (s), f, defs (s)) endif

; One can imagine adding new instructions.
; The Interpreter

Definition: execute (ins, s) = if car (ins) = 'move then move (cadr (ins), caddr (ins), s)

elseif car (ins) = 'movi then movi (cadr (ins), caddr (ins), s) elseif car (ins) = 'add then add (cadr (ins), caddr (ins), s) elseif car (ins) = 'subi then subi (cadr (ins), caddr (ins), s) elseif car (ins) = 'jumpz then jumpz (cadr (ins), caddr (ins), s) elseif car (ins) = 'jump then jump (cadr (ins), s) elseif car (ins) = 'call then call (cadr (ins), s) elseif car (ins) = 'ret then ret (s) else s endif

Definition: step (s) = if haltedp (s) then s

else execute (fetch (pc (s), defs (s)), s) endif Definition: sm (s, n) = if n ≃ 0 then s

else sm (step (s), n − 1) endif

; This concludes our formal definition of the intepreter.
; We next prove a small collection of lemmas that tightly control the
; expansion of the the interpreter.  The idea is that we don't want sm
; or step to expand unless we know what the current instruction is and
; have enough time on the clock to execute it.  So we will prove
; certain rewrite rules that manipulate step and sm and then disable
; those functions so that only the rules are available.

Theorem: step-opener (haltedp (s) → (step (s) = s)) ∧ (listp (fetch (pc (s), defs (s)))

→ (step (s)

= if haltedp (s) then s else execute (fetch (pc (s), defs (s)), s) endif))

Event: Disable step.

Theorem: sm-plus sm (s, i + j ) = sm (sm (s, i), j )

Theorem: sm-add1 sm (s, 1 + i) = sm (step (s), i)

Theorem: sm-0 sm (s, 0) = s

Event: Disable sm.

; Now we move to our first example program.  We will define a program
; that multiplies two naturals by successive addition.  We will then
; prove it correct.
; The program we have in mind is:
; (times (movi 2 0)
;        (jumpz 0 5)
;        (add 2 1)

;        (subi 0 1)
;        (jump 1)
;        (ret))
; Observe that the program multiplies the contents of reg 0 by the
; contents of reg 1 and leaves the result in reg 2.  At the end, reg 0
; is 0 and reg 1 is unchanged.  If we start at a (call times) this
; program requires 2+4i+2 instructions, where i is the initial
; contents of reg 0.  To keep the proof incredibly simple, we will
; prove the program correct only for the 5 register version of our
; machine!  (Why 5?  Why not 3?  Because eventually we will use times
; in another program that uses 5 registers.  In general we should
; prove it for an arbitrarily large memory -- and we will -- but that
; just complicates the statement without contributing to the example.)
; We start by defining the constant that is this program:

Definition: times-program

= '(times
      (movi 2 0)
      (jumpz 0 5)
      (add 2 1)
      (subi 0 1)
      (jump 1)
      (ret))
; 5  Return
; and a function that multiplies the "same way."

Definition: times-fn (i, j , ans) = if i ≃ 0 then ans

else times-fn (i − 1, j , ans + j ) endif

; In some sense, the following mathematical fact completely captures
; the correctness of the program:

Theorem: times-fn-is-times (ans ∈ N) → (times-fn (i, j , ans) = ((i ∗ j ) + ans))

; at least if one also understands

Theorem: plus-right-id (x + 0) = fix (x)

; The real problem is proving that the program has this semantics.
; First, how much time does the program need?  It takes one tick to do
; the CALL, one for the MOVI at pc 0, then 4 ticks for each iteration
; of the loop at pc 1, and then 2 more ticks to get out of the loop
; and do the RET.  So:

Definition: times-clock (i) = (2 + (i ∗ 4) + 2)

; We could have written (plus 4 (times i 4)) but by using this
; algebraically odd expression we make sm-plus, above, immediately
; applicable.
; We next address ourselves to the loop from pc 1 through 4.  Consider
; an arbitary arrival at pc 1 and suppose you have (times i 4) ticks.
; The following theorem tells us what you get:

Theorem: times-correct-lemma ((i ∈ N) ∧ (assoc ('times, defs) = times-program)) → (sm (st ('(times . 1), stk1 , list (i, j , ans, r3 , r4 ), f, defs), i ∗ 4)

     = st ('(times . 1),

stk1 ,

list (0, j , times-fn (i, j , ans), r3 , r4 ), f, defs))

; It is then trivial to construct the entire correctness proof:

Theorem: times-correct ((fetch (pc, defs) = '(call times)) ∧ (assoc ('times, defs) = times-program) ∧ (i ∈ N)) → (sm (st (pc, stk, list (i, j , r2 , r3 , r4 ), f, defs), times-clock (i))

= st (add1-pc (pc), stk, list (0, j , i ∗ j , r3 , r4 ), f, defs))

; We disable the clock function so that subsequent programs can
; use it without its expansion messing up their algebraic
; form.

Event: Disable times-clock.

; It is worth noting that this file has been rather carefully crafted
; to make the above proof go through with a minimum of fuss.  In
; general, we will have to prove lots of lemmas about the utility
; functions GET and PUT to handle arbitrarily sized memories.  And we
; have to prove lots of lemmas about arithmetic to explain the data
; handling in our programs.  To some extent those arithmetic facts get
; in the way of our desired treatment of the clock in our proofs,
; e.g., if the theorem prover knows the usual facts about PLUS and
; TIMES then (PLUS 2 (TIMES I 4) 2) would become (PLUS 4 (TIMES 4 I))
; and we'd then have to take special care to force sm to open the way
; we want in this proof.  One avenue that has been used to avoid this
; problem is to define the clock functions with special arithmetic
; primitives, e.g., CLK-PLUS and CLK-TIMES (which are in fact just the
; familiar functions) but which we then disable and isolate from the
; free-wheeling arithmetic simplifications.
; We now consider the role of subroutine call and return in this
; language.  To illustrate it we'll implement exponentiation, which
; will CALL our TIMES program.  The proof of the correctness of the
; exponentiation program will rely on the correctness of TIMES, not on
; re-analysis of the code for TIMES.
; The mathematical function we wish to implement is:

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

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

; The program we have in mind is:

Definition: exp-program

= '(exp
      (move 3 0)
      (move 4 1)
      (movi 1 1)
      (jumpz 4 9)
      (move 0 3)
      (call times)

      (move 1 2)
      (subi 4 1)
      (jump 3)
      (ret))
; 9  return
; A recursive description of the loop (pc 3 through 8) in this
; algorithm is:

Definition: exp-fn (r0 , r1 , r2 , r3 , r4 ) = if r4 ≃ 0 then r1

else exp-fn (0, r3 ∗ r1 , r3 ∗ r1 , r3 , r4 − 1) endif

; Pretty weird.
; We need a little more arithmetic than we have, namely
; associativity and right identity for times:

Theorem: associativity-of-times ((i ∗ j ) ∗ k) = (i ∗ (j ∗ k))

Theorem: times-right-id (i ∗ 1) = fix (i)

; So now the system can prove that the weird exp-fn is just exp (in a
; generalized sense that accomodates the initial value of r1).

Theorem: exp-fn-is-exp (r1 ∈ N) → (exp-fn (r0 , r1 , r2 , r3 , r4 ) = (exp (r3 , r4 ) ∗ r1 ))

; Here is the clock function for exp.  Again we use an algebraically
; odd form simply to gain instant access to the desired sm-plus
; decomposition.  The "4" gets us past the CALL and the first 3
; initialization instructions; the times expression takes us around
; the exp loop j times, and the final "2" gets us out through the RET.
; Note that as we go around the loop we make explicit reference to
; TIMES-CLOCK to explain the CALL of TIMES.

Definition: exp-clock (i, j ) = (4 + (j ∗ (2 + times-clock (i) + 3)) + 2)

; Now we prove the "loop invariant" for the EXP program.  We simply
; tell the system to induct according to exp-fn.  We could "trick" it
; into doing that by using exp-fn in place of the (times (exp r3 r4)
; r1) expressions, but that is devious and doesn't always work.

Theorem: exp-correct-lemma ((r3 ∈ N) ∧ (r4 ∈ N) ∧ (assoc ('exp, defs) = exp-program) ∧ (assoc ('times, defs) = times-program)) → (sm (st ('(exp . 3), stk, list (r0 , r1 , r2 , r3 , r4 ), f, defs),

r4 ∗ (2 + times-clock (r3 ) + 3))

     = st ('(exp . 3),

stk,

if r4 ≃ 0 then list (r0 , r1 , r2 , r3 , r4 )

else list (0, exp (r3 , r4 ) ∗ r1 , exp (r3 , r4 ) ∗ r1 , r3 ,

0) endif,

f, defs))

; The theorem prover is now set up to prove that exp is correct
; without further assistance.  (But you must not underestimate how
; clever this assistance has been to make this possible!)

Theorem: exp-correct ((i ∈ N) ∧ (j ∈ N) ∧ (fetch (pc, defs) = '(call exp)) ∧ (assoc ('exp, defs) = exp-program) ∧ (assoc ('times, defs) = times-program)) → (sm (st (pc, stk, list (i, j , r2 , r3 , r4 ), f, defs), exp-clock (i, j ))

= st (add1-pc (pc), stk, if j ≃ 0 then list (i, exp (i, j ), r2 , i, 0) else list (0, exp (i, j ), exp (i, j ), i, 0) endif, f, defs))

; Ok, enough of this.  Presumably the point has been made:  correctness
; proofs can be "stacked."

; Recall that we have been dealing with an unnecessarily restricted
; view of the machine, namely that it only have 5 memory locations.
; Before leaving this approach and pursuing some others, let us
; quickly prove the most general form of the correctness result for
; TIMES.
; We start with the basic normalization rules for get and put.

Definition: length (lst) = if lst ≃ nil then 0

else 1 + length (cdr (lst)) endif

Theorem: put-put-0 ((addr < length (mem)) ∧ (get (addr, mem) = val)) → (put (addr, val, mem) = mem)

Theorem: put-put-1 put (addr, v2 , put (addr, v1 , mem)) = put (addr, v2 , mem)

Theorem: put-put-2 ((addr1 ∈ N) ∧ (addr2 ∈ N) ∧ (addr1 ≠ addr2 )) → (put (addr2 , v2 , put (addr1 , v1 , mem)) = put (addr1 , v1 , put (addr2 , v2 , mem)))

Theorem: get-put ((addr1 ∈ N) ∧ (addr2 ∈ N)) → (get (addr1 , put (addr2 , val, mem))

= if addr1 = addr2 then val else get (addr1 , mem) endif)

Theorem: length-put (addr < length (mem)) → (length (put (addr, val, mem)) = length (mem))

Event: Disable get.

Event: Disable put.

; And a few basic arithmetic facts.

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

Theorem: difference-elim ((i ∈ N) ∧ (i ≮ j )) → ((j + (i − j )) = i)

Theorem: associativity-of-plus ((i + j ) + k) = (i + (j + k))

Theorem: commutativity-of-plus (i + j ) = (j + i)

Theorem: commutativity2-of-plus (i + (k + j )) = (k + (i + j ))

; Ok, now we get specific to the TIMES program.  The following function
; "is" loop in the TIMES program vis-a-vis its effect on a completely
; arbitrary memory mem.  If a program is run entirely for its effect on
; memory (as opposed to the subroutine stack or the haltedp flag, then
; this program "is" the McCarthy-esque functional analogue of the loop.

Definition: times-mem-fn-loop (mem) = if get (0, mem) ≃ 0 then mem

else times-mem-fn-loop (put (0, get (0, mem) − 1, put (2, get (2, mem) + get (1, mem), mem))) endif

Definition: times-mem-fn (mem) = times-mem-fn-loop (put (2, 0, mem))

; In proving this functional analogue correct we essentially carry
; our McCarthy's functional semantics approach.  The theorem below
; establishes that times-mem-fn-loop just does two puts into mem:  it
; 0's r0 and it puts (r0*r1)+r2 into location r2:

Theorem: times-mem-fn-loop-is-times ((get (0, mem) ∈ N) ∧ (get (2, mem) ∈ N) ∧ (2 < length (mem))) → (times-mem-fn-loop (mem)

= put (0,

             0,

put (2, (get (0, mem) ∗ get (1, mem)) + get (2, mem), mem)))

Theorem: times-mem-fn-is-correct ((get (0, mem) ∈ N) ∧ (2 < length (mem))) → (times-mem-fn (mem)

= put (0, 0, put (2, get (0, mem) ∗ get (1, mem), mem)))

; Our aim, in the revisited times-correct theorem, is to establish that
; executing a CALL of TIMES has the following effect on an almost arbitrary
; state s:

Definition: times-step (s) = st (add1-pc (pc (s)),

stk (s),

put (0, 0, put (2, get (0, mem (s)) ∗ get (1, mem (s)), mem (s))), f, defs (s))

; The proof proceeds, as we have seen twice before, first by an
; inductive analysis of the loop itself.  Note that we induct
; according to times-mem-fn-loop.

Theorem: times-correct-lemma-revisited ((get (0, mem) ∈ N) ∧ (assoc ('times, defs) = times-program)) → (sm (st ('(times . 1), stk1 , mem, f, defs), get (0, mem) ∗ 4)

= st ('(times . 1), stk1 , times-mem-fn-loop (mem), f, defs))

; Unfortunately, the above lemma is not quite applicable in our use below
; because the mem that occurs in the state in the lhs of the conclusion is
; not going to be syntactically identical to the mem that occurs in the
; (times (get 0 mem) 4) in the clock.  The reason is that the clock mem is
; the original mem while the state mem is the one produced by moving a 0
; into r2.  Of course, they have the same r0 value.  So, having proved
; the inductive fact we need, we now "generalize" it.

Theorem: times-correct-lemma-revisited-and-generalized ((r0 = get (0, mem)) ∧ (get (0, mem) ∈ N) ∧ (assoc ('times, defs) = times-program)) → (sm (st ('(times . 1), stk1 , mem, f, defs), r0 ∗ 4)

= st ('(times . 1), stk1 , times-mem-fn-loop (mem), f, defs))

; And now we can prove the most general form of the correctness of our
; TIMES program.  It tells us that if you are interested in (sm s n),
; where the pc points to a CALL of TIMES, the definition of 'TIMES is
; ours, memory is at least 3 long, r0 is numeric, the halt flag is
; off, and there are at least (times-clock r0) ticks on the clock,
; then you can just take a times-step and decrease the clock by
; (times-clock r0).  What more could you want?

Theorem: times-correct-revisited ((fetch (pc (s), defs (s)) = '(call times)) ∧ (assoc ('times, defs (s)) = times-program) ∧ (2 < length (mem (s))) ∧ (r0 = get (0, mem (s))) ∧ (r0 ∈ N) ∧ (n ≮ times-clock (r0 )) ∧ (¬ haltedp (s))) → (sm (s, n) = sm (times-step (s), n − times-clock (r0 )))

; The Inductive Assertion Approach
; First, we simply prove the hand-generated verification
; conditions from an informal annotation of our TIMES
; program.

Theorem: verification-conditions-for-times (((i0 ∈ N) ∧ (i1 ∈ N)) → ((0 ∈ N) ∧ ((i0 ∗ i1 ) = (0 + (i0 ∗ i1 ))))) ∧ (((r2 ∈ N) ∧ ((i0 ∗ i1 ) = (r2 + (r0 ∗ r1 ))) ∧ (r0 ≄ 0))

→ (((r2 + r1 ) ∈ N)

∧ ((i0 ∗ i1 ) = ((r2 + r1 ) + ((r0 − 1) ∗ r1 )))))

∧ (((r2 ∈ N) ∧ ((i0 ∗ i1 ) = (r2 + (r0 ∗ r1 ))) ∧ (r0 ≃ 0)) → (r2 = (i0 ∗ i1 )))

; Now we develop the analogue of the inductive assertion
; method formally.
; Introduce p as an arbitrary invariant under stepping.  The
; everywhere true predicate witnesses this constraint.

Conservative Axiom: p-step p (s) → p (step (s))

Simultaneously, we introduce the new function symbol p.

; Observe that such a p is invariant under arbitrary length runs of the
; machine.

Theorem: p-invariant p (s0 ) → p (sm (s0 , n))

; That's it.  It is really deep isn't it?
; Now we'll define a p that suits our specification for TIMES.  We call
; it timesp.

Definition: r0 (s) = get (0, mem (s))

Definition: r1 (s) = get (1, mem (s))

Definition: r2 (s) = get (2, mem (s))

Definition: timesp (i0 , i1 , s) = ((i0 ∈ N)

∧ (i1 ∈ N) ∧ stp (s) ∧ (stk (s) ≃ nil) ∧ (assoc ('times, defs (s)) = times-program) ∧ (i1 = r1 (s)) ∧ if pc (s) = '(times . 0) then i0 = r0 (s)

elseif pc (s) = '(times . 1)

then (r2 (s) ∈ N)

∧ ((i0 ∗ i1 ) = (r2 (s) + (r0 (s) ∗ r1 (s)))) elseif pc (s) = '(times . 2) then (r0 (s) ≄ 0)

∧ (r2 (s) ∈ N)

∧ ((i0 ∗ i1 ) = (r2 (s) + (r0 (s) ∗ r1 (s)))) elseif pc (s) = '(times . 3) then (r0 (s) ≄ 0)

∧ (r2 (s) ∈ N)
∧ ((i1 + (i0 ∗ i1 ))

= (r2 (s) + (r0 (s) ∗ r1 (s))))

elseif pc (s) = '(times . 4)

then (r2 (s) ∈ N)

∧ ((i0 ∗ i1 ) = (r2 (s) + (r0 (s) ∗ r1 (s)))) elseif pc (s) = '(times . 5) then r2 (s)

= (i0 ∗ i1 )

else f endif)

; Since timesp is preserved by step:

Theorem: timesp-step timesp (i0 , i1 , s) → timesp (i0 , i1 , step (s))

; we can immediately conclude by functional instantiation that
; it is preserved under arbitrary runs of the machine:

Theorem: timesp-invariant timesp (i0 , i1 , s0 ) → timesp (i0 , i1 , sm (s0 , n))

; By additionally assuming that the initial and final pcs
; are at 0 and 5 respectively in TIMES, we derive the
; desired theorem.

Theorem: times-correct-revisited-again (stp (s0 ) ∧ (stk (s0 ) ≃ nil) ∧ (assoc ('times, defs (s0 )) = times-program) ∧ (i0 = get (0, mem (s0 ))) ∧ (i1 = get (1, mem (s0 ))) ∧ (i0 ∈ N) ∧ (i1 ∈ N)

 ∧ (pc (s0 ) = '(times . 0))

∧ (pc (sm (s0 , n)) = '(times . 5))) → (get (2, mem (sm (s0 , n))) = (i0 ∗ i1 ))

; The following events are not at all easy to follow and should not be
; considered part of the tutorial.  They are included in this file to
; justify the sentence, in the second edition of the Handbook, that
; our standard form of correctness theorem for a subroutine implies
; the standard form of the termination theorem for that subroutine.
; In particular, we lead the system the proof of the following
; theorem.  Suppose s is a state poised to execute a CALL of some
; subroutine fn (and the halt flag of s is F).  Suppose that some
; non-zero number of steps, n, later the stack is the same as it is in
; s.  Intuitively, this means that the subroutine was called and
; eventually returned.  Then if the subroutine is called as the
; top-level program the halt flag is eventually set.  That is to say,
; let s' be obtained from s by setting the pc to (fn . 0), the first
; instruction in fn, and let the stack be nil, i.e., this is the
; top-level, main program.  Then by running s' n steps we obtain a
; state with the halt flag set.  That is the theorem
; standard-correctness-implies-termination, below.
; It is a fairly difficult theorem for two reasons.  First, it
; considers running fn in two different states: as part of a
; continuing computation and as the top-level main program.  We

; therefore have to develop lemmas that let us modify the state, e.g.,
; change the stack, without damaging some aspects of the computation.
; Second, the hypothesis that the stack eventually (at tick n) is the
; same as before the CALL means that a balanced RET was executed.  But
; it does not mean the balancing RET was executed at tick n.  For all
; we know, the CALL returned immediately and during the remaining
; ticks we possibly called other routines or even returned from the
; caller and eventually re-entered!  But we can convert that
; hypothesis into one that says for some k<n the balancing RET was
; executed on the kth tick and if we considered the top-level
; computation at that tick, we'll see that it sets the halt flag.  The
; remaining ticks at the top-level computation just leave the halt
; flag on.
; This proof took several days to construct and I found it frustrating
; in its complexity.  Perhaps someone can simplify it.  That said,
; here are the events with which I proved it.
; Because the tutorial has left the data base in a state designed to
; prove things of individual programs, there is a fair amount of
; enabling and disabling to get access to the guts of the machine.
; First we prove that once the machine halts, it stays halted.

Theorem: step-preserves-haltedp (¬ haltedp (step (s))) → (¬ haltedp (s))

Theorem: sm-preserves-haltedp (¬ haltedp (sm (s, n))) → (¬ haltedp (s))

; And that only RET sets the halt flag, i.e., if it becomes halted,
; then the current pc points to a RET.

Theorem: only-ret-sets-haltedp ((¬ haltedp (s)) ∧ (haltedp (step (s)) ∧ (defs = defs (s)))) → (car (get (cdr (pc (s)), cdr (assoc (car (pc (s)), defs)))) = 'ret)

; This function finds the k<n at which the balancing RET is
; executed.  Imagine that s is the state immediately after the
; CALL and that d is the depth of the stack in that state.
; Then we count ticks until we are poised to execute a RET from
; a state with stack depth d.

Definition: k (s, d, n) = if n ≃ 0 then 0

elseif (length (stk (s)) = d)

∧ (car (fetch (pc (s), defs (s))) = 'ret) then 0 else 1 + k (step (s), d, n − 1) endif

; Because we'll keep step disabled, we'll need the following to
; analyze what it does to the stack depth.

Theorem: length-stk-step length (stk (step (s))) = if haltedp (s) then length (stk (s))

elseif car (fetch (pc (s), defs (s))) = 'ret then length (stk (s)) − 1 elseif car (fetch (pc (s), defs (s))) = 'call then 1 + length (stk (s)) else length (stk (s)) endif

; The following theorem establishes that if, within n, the
; stack depth falls below d then the computed k is less than n.

Theorem: exists-terminating-ret ((d ∈ N) ∧ (length (stk (s0 )) ≮ d) ∧ (length (stk (sm (s0 , n))) < d)) → (k (s0 , d, n) < n)

; We now want to prove that if the computed k is less than n, then
; various things are true of the state at tick k.  We need the
; obvious fact that the defs field never changes.

Theorem: defs-step defs (step (s)) = defs (s)

; So here are some important properties of our k (when it is less than
; n), namely, that the stack depth of the kth state is d and that it
; is poised to execute a RET.

Theorem: properties-of-k (k (s0 , d, n) < n) → ((length (stk (sm (s0 , k (s0 , d, n)))) = d)

∧ (car (fetch (pc (sm (s0 , k (s0 , d, n))), defs (s0 ))) = 'ret))

; We also need that the kth state is still running, i.e., not itself halted.
; This takes a bit of work.

Theorem: haltedp-persists haltedp (s) → haltedp (sm (s, n))

Theorem: haltedp-k haltedp (s) → (k (s, d, n)

= if (length (stk (s)) = d)

∧ (car (fetch (pc (s), defs (s))) = 'ret) then 0 else fix (n) endif)

Theorem: halting-preserves-stk haltedp (step (s0 )) → (length (stk (step (s0 ))) = length (stk (s0 )))

; With that preamble, we can get that the kth state is still running.

Theorem: another-property-of-k ((¬ haltedp (s0 )) ∧ (k (s0 , d, n) < n)) → (¬ haltedp (sm (s0 , k (s0 , d, n))))

; We assemble the two lemmas establishing properties of k into one: if
; s0 is not halted and within n ticks the stack is less than its
; current size then (a) k exists, i.e., is less than n, (b) the kth
; state has the same stack size as s0, (c) the kth state is poised to
; execute a RET and (d) it is not halted.

Theorem: decreasing-stk-means-ret-exists ((¬ haltedp (s0 )) ∧ (length (stk (sm (s0 , n))) < length (stk (s0 )))) → ((k (s0 , length (stk (s0 )), n) < n)

∧ (length (stk (sm (s0 , k (s0 , length (stk (s0 )), n))))

= length (stk (s0 ))) ∧ (car (fetch (pc (sm (s0 , k (s0 , length (stk (s0 )), n))), defs (s0 )))

          = 'ret)

∧ (¬ haltedp (sm (s0 , k (s0 , length (stk (s0 )), n)))))

; Now we'll disable the two independently proved lemmas about k.

Event: Disable properties-of-k.

Event: Disable another-property-of-k.

; Next, we develop the idea that under some conditions we can mess around with

; the stack of a computation without changing the outcome in some sense.  The only
; way we'll mess around is by growing the stack at the deep end by adding some
; arbitrary additional cells.

Definition: grow-stk (s, stk) = st (pc (s), append (stk (s), stk), mem (s), haltedp (s), defs (s))

; The lemma sm-grow-stk, just below, is the key result.  The intervening
; lemmas are just helpers.

Theorem: listp-append listp (append (a, b)) = (listp (a) ∨ listp (b))

Theorem: step-grow-stk (¬ haltedp (step (s))) → (step (grow-stk (s, stk)) = grow-stk (step (s), stk))

Theorem: sm-grow-stk (¬ haltedp (sm (s, n))) → (sm (grow-stk (s, stk), n) = grow-stk (sm (s, n), stk))

; The above lemma is really nice.  It says that if a computation
; doesn't halt within n then growing the stack commutes with the
; computation, i.e., you can grow the stack before you start or after
; you finish.  This lets us consider a computation in either of two
; states, one with a shallow stack or one with a deep stack.  If s has
; a stack of nil then it is in top-level execution and thus (grow-stk
; s stk) is some continuing execution of the same program.
; A key fact we'll need is that if k is less than or equal to n and the
; computation halts in k then it halts in n.  This explains why the
; halt flag is set at the end of the long top-level computation, even if
; it became set fairly early.

Theorem: lessp-haltedp ((n ≮ k) ∧ haltedp (sm (s, k))) → haltedp (sm (s, n))

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

; Again, because step will be disabled later, we need to expose the
; behavior of a halting RET.

Theorem: step-is-ret ((¬ haltedp (s)) ∧ (car (fetch (pc (s), defs (s))) = 'ret) ∧ (stk (s) ≃ nil)) → haltedp (step (s))

; Oddly enough, though we proved that defs is preserved by step, above,
; we only now need that it is preserved by sm.

Theorem: defs-sm defs (sm (s, n)) = defs (s)

; In a sense, the following theorem is the real key to our proof.  It
; gives us a way to show that the halted flag is on in the nth step of
; s, namely find some k less than n-1 such that the kth state is not
; yet halted but has a stack of length 0 and is poised to execute a
; RET.  If you imagine that s is the top-level run of our subroutine,
; then this focusses our attention on the k at which the halt flag first
; becomes set.

Theorem: expand-sm-n ((k < (n − 1)) ∧ (¬ haltedp (sm (s, k))) ∧ (car (fetch (pc (sm (s, k)), defs (s))) = 'ret) ∧ (length (stk (sm (s, k))) = 0)) → haltedp (sm (s, n))

; Now there are various details to be worked out, and I never found a
; really nice way to handle them except by brute force.  The basic
; theme of these details is that from the hypothesis that the
; ``continuing computation'' eventually returns to the same stack
; depth we can get some information about the pc and stack depth in
; the continuing computation.  But we have to convert that to
; information about the pc and stack depth in the top-level
; computation.  We can get these results from our sm-grow-stk lemma,
; namely, we know that if a short stacked computation doesn't halt we
; can grow its stack either before or after.  If the short stacked
; computation is the top-level one, where the stack is nil, then we
; can grow the stack to whatever stack we have in the continuing
; computation.  From the equality of the two final states we can learn
; that the pc of the top-level computation is the same as that of the
; continuing one.  While I find this proof very neat, what with its
; use of sm-grow-stk, I find the event below ugly because of the

; explict hint and the explicit states involved.  But it just wasn't
; worth my time to figure out an elegant rewrite rule that would
; normalize the pc.

Theorem: pc-equiv (¬ haltedp (sm (st (cons (prog, 0), nil, mem (s), f, defs (s)), k))) → (pc (sm (st (cons (prog, 0), nil, mem (s), f, defs (s)), k))

= pc (sm (st (cons (prog, 0), cons (cons (car (pc (s)), 1 + cdr (pc (s))), stk (s)), mem (s), f, defs (s)),

k)))

; We need to know a similar fact about the stacks after k steps.  In particular,
; we know from the continuing computation that at step k it is poised to RET on
; a stack of a certain depth.  We need to convert that to a fact about the top-level
; state at step k, namely that the stack there is nil -- so the RET will set the halt
; flag.  At first sight, this is a problem very similar to that above and one is
; tempted to try to solve it the same way.  But the problem above is insensitive to
; the value of k, as long as the computation is still running, while the one we
; are talking about now is our special k, the tick at which we execute the RET that
; balances the initial CALL.  But that raises a problem.  That existential k
; is computed with a given state.  Is that state from the continuing computation
; or from the top-level one?  What we prove below is that it doesn't matter, they
; are the same!  This is pretty subtle.  We need a few lemmas...

Theorem: length-append length (append (a, b)) = (length (a) + length (b))

Theorem: grow-stk-props (pc (grow-stk (s, stk)) = pc (s)) ∧ (stk (grow-stk (s, stk)) = append (stk (s), stk)) ∧ (mem (grow-stk (s, stk)) = mem (s)) ∧ (haltedp (grow-stk (s, stk)) = haltedp (s)) ∧ (defs (grow-stk (s, stk)) = defs (s))

Theorem: step-grow-stk-revisited-1 (0 < length (stk (s))) → (step (grow-stk (s, stk)) = grow-stk (step (s), stk))

Theorem: step-grow-stk-revisited-2 (car (fetch (pc (s), defs (s))) ≠ 'ret) → (step (grow-stk (s, stk)) = grow-stk (step (s), stk))

; So here is the key fact: k produces the same answer on the top-level
; state (here, s) and the continuing state, provided you bump the d
; appropriately.

Theorem: k-grow-stk ((d ∈ N) ∧ (length (stk (s)) ≮ d)) → (k (grow-stk (s, stk), d + length (stk), n) = k (s, d, n))

; Once again, I couldn't find a useful rewrite rule, since grow-stk isn't
; really in our problem, and so I make this lemma of class nil and instantiate
; it when I need to show that the two states produce the same k.  Given that,
; we can now infer that the final, top-level stack is nil at step k,
; just by using properties of k on the top-level state, but appealing to
; the existence of k from the continuing state.  We then repeat the exercise
; to extract the information that the halt flag is still off at step k in
; the top-level state.

Theorem: stk-is-nil (k (st (cons (prog, 0),

cons (cons (car (pc (s)), 1 + cdr (pc (s))), stk (s)), mem (s), f, defs (s)), 1 + length (stk (s)), n − 1)

< (n − 1)) → (listp (stk (sm (st (cons (prog, 0), nil, mem (s), f, defs (s)),

k (st (cons (prog, 0), cons (cons (car (pc (s)), 1 + cdr (pc (s))), stk (s)), mem (s), f, defs (s)), 1 + length (stk (s)), n − 1))))

= f)

Theorem: haltedp-is-off (k (st (cons (prog, 0),

cons (cons (car (pc (s)), 1 + cdr (pc (s))), stk (s)), mem (s), f, defs (s)), 1 + length (stk (s)),

n − 1) < (n − 1)) → (haltedp (sm (st (cons (prog, 0), nil, mem (s), f, defs (s)),

k (st (cons (prog, 0), cons (cons (car (pc (s)), 1 + cdr (pc (s))), stk (s)), mem (s), f, defs (s)), 1 + length (stk (s)), n − 1)))

= f)

; So, if you've followed all that, you are ready to get the main theorem:

Theorem: standard-correctness-implies-termination ((¬ haltedp (s)) ∧ (fetch (pc (s), defs (s)) = list ('call, prog)) ∧ (n ≄ 0) ∧ (stk (sm (s, n)) = stk (s))) → haltedp (sm (st (cons (prog, 0), nil, mem (s), f, defs (s)), n))

; As I said, the proof is not at all easy to follow.  I invite
; readers to find a better one!

; The next theorem establishes the effect of a one-instruction infinite loop.
; It says that if you have a running state and when you fetch the current
; instruction you get (JUMP i) where i is the location of the current program
; counter, then the halt flag is never set.

Theorem: infinite-loop ((¬ haltedp (s)) ∧ (fetch (pc (s), defs (s)) = list ('jump, i)) ∧ (i ∈ N) ∧ (cdr (pc (s)) = i)) → (¬ haltedp (sm (s, n)))

Index

add, 3, 4 add1-pc, 2–4, 7, 10, 13 another-property-of-k, 19 associativity-of-plus, 12 associativity-of-times, 9

call, 4 commutativity-of-plus, 12 commutativity2-of-plus, 12

decreasing-stk-means-ret-exists, 19 defs, 3–5, 13–24 defs-sm, 21 defs-step, 18 difference-1, 11 difference-elim, 12

equal-length-0, 20 execute, 4, 5 exists-terminating-ret, 18 exp, 8–10 exp-clock, 9, 10 exp-correct, 10 exp-correct-lemma, 10 exp-fn, 9 exp-fn-is-exp, 9 exp-program, 8, 10 expand-sm-n, 21

fetch, 3–5, 7, 10, 14, 18, 19, 21, 22, 24

get, 2–4, 11–17 get-put, 11 grow-stk, 20, 22, 23 grow-stk-props, 22

haltedp, 4, 5, 14, 17–22, 24 haltedp-is-off, 23 haltedp-k, 19 haltedp-persists, 19 halting-preserves-stk, 19 infinite-loop, 24

jump, 4 jumpz, 4

k, 18, 19, 23, 24 k-grow-stk, 23

length, 11, 12, 14, 18–24 length-append, 22 length-put, 11 length-stk-step, 18 lessp-haltedp, 20 listp-append, 20

mem, 3, 4, 13–16, 20, 22–24 move, 3, 4 movi, 3, 4

only-ret-sets-haltedp, 17

p, 14

p-invariant, 14 p-step, 14 pc, 3–5, 13–24 pc-equiv, 22 plus-right-id, 7 properties-of-k, 18 put, 3, 11–13 put-put-0, 11 put-put-1, 11 put-put-2, 11

r0, 15 r1, 15 r2, 15 ret, 4

sm, 5, 7, 10, 13, 14, 16–24 sm-0, 5 sm-add1, 5 sm-grow-stk, 20 sm-plus, 5 sm-preserves-haltedp, 17 st, 2–4, 7, 10, 13, 20, 22–24 standard-correctness-implies-te

rmination, 24 step, 4, 5, 14, 15, 17–22 step-grow-stk, 20 step-grow-stk-revisited-1, 22 step-grow-stk-revisited-2, 22 step-is-ret, 21 step-opener, 5 step-preserves-haltedp, 17 stk, 3, 4, 13, 15, 16, 18–24 stk-is-nil, 23 stp, 15, 16 subi, 3, 4

times-clock, 7, 9, 10, 14 times-correct, 7 times-correct-lemma, 7 times-correct-lemma-revisited, 13 times-correct-lemma-revisited-a

nd-generalized, 13 times-correct-revisited, 14 times-correct-revisited-again, 16 times-fn, 6, 7 times-fn-is-times, 6 times-mem-fn, 12 times-mem-fn-is-correct, 12 times-mem-fn-loop, 12, 13 times-mem-fn-loop-is-times, 12 times-program, 6, 7, 10, 13–16 times-right-id, 9 times-step, 13, 14 timesp, 15, 16 timesp-invariant, 16 timesp-step, 15

verification-conditions-for-time s, 14