;;; -*-  Mode: Lisp -*-

;  A Correctness Proof of the SECD Machine
;                   by John D. Ramsdell				       
;                  The MITRE Corporation

; Section 1: The Lambda Value Calculus

; A de Bruijn formalization of the Lambda Value Calculus.  Much of
; this is adapted from: `An Annotated Script of A MECHANICAL PROOF OF
; THE CHURCH-ROSSER THEOREM,' by N. Shankar.

; This section defines the notion of evaluation in the Lambda 
; Value Calculus.  The most notable event in this section is EVAL.

(boot-strap nqthm)

; Definitions for lambda terms.

(add-shell
 lambda					; Lambda abstractions
 nil
 lambdap
 ((lbody (none-of) zero)))

(add-shell
 comb					; Combinations
 nil
 combp
 ((fun (none-of) zero)
  (arg (none-of) zero)))

(add-shell
 const					; Constants
 nil					; There are a countable
 constp					; number of them.
 ((const-id (one-of numberp) zero)))
   
; Variables are represented by the positive integers.
; Note: zero is not a variable because zero is often a default value
; in NQTHM.
(defn varp (x) (not (zerop x)))
(defn var-base () 1)
(defn bump-base () (sub1 (var-base)))

(defn valuep (x)
  (or (lambdap x) (constp x)))

; (CLOSEDP X N) when X is a lambda term in which the largest
; free variable is less than N.
(defn closedp (x n)
  (if (lambdap x)
      (closedp (lbody x) (add1 n))
    (if (combp x)
	(and (closedp (fun x) n)
	     (closedp (arg x) n))
      (if (varp x)
	  (lessp x n)
	(constp x)))))

(defn closed-termp (x)
  (closedp x (var-base)))

; The actions of primitives are defined by DELTA
; and (DELTA X Y) is defined iff (DELTA-DEFINEDP X Y).
(defn delta-definedp-witness (x y)
  (and (constp x) (constp y)))

(constrain
 delta-definedp-is-pred-on-consts
 ()
 (and 
  (or (truep (delta-definedp x y))	; DELTA-DEFINEDP is a predicate
      (falsep (delta-definedp x y)))
  (implies (delta-definedp x y)		; DELTA-DEFINED is false
	   (and (constp x)		; on non-constant arguments.
		(constp y))))
 ((delta-definedp delta-definedp-witness)))

(prove-lemma
 delta-definedp-type
 (rewrite)
 (or (truep (delta-definedp x y))
     (falsep (delta-definedp x y)))
 ((use (delta-definedp-is-pred-on-consts))))

(prove-lemma
 not-const-arg1-implies-not-delta-definedp
 (rewrite)
 (implies (not (constp x)) (not (delta-definedp x y)))
 ((use (delta-definedp-is-pred-on-consts))))

; Note that DELTA-DEFINEDP-IMPLIES-CONST-ARG1 contains the free
; variable Y which will be chosen by instantiating the hypothesis
; (DELTA-DEFINEDP X Y).
; This is okay.
(prove-lemma
 delta-definedp-implies-const-arg1
 (rewrite)
 (implies (delta-definedp x y) (constp x))
 ((use (delta-definedp-is-pred-on-consts))))

(prove-lemma
 not-const-arg2-implies-not-delta-definedp
 (rewrite)
 (implies (not (constp y)) (not (delta-definedp x y)))
 ((use (delta-definedp-is-pred-on-consts))))

; See comment for DELTA-DEFINEDP-IMPLIES-CONST-ARG1
(prove-lemma
 delta-definedp-implies-const-arg2
 (rewrite)
 (implies (delta-definedp x y) (constp y))
 ((use (delta-definedp-is-pred-on-consts))))

(defn delta-witness (x y)
  (const (plus (const-id x) (const-id y))))
	       
(constrain
 delta-result
 ()
 (and (valuep (delta x y))		; The result of (DELTA X Y) 
      (closed-termp (delta x y)))	; is a value which is a 
 ((delta delta-witness)))		; closed term.
 
(prove-lemma
 delta-valuep
 (rewrite)
 (or (constp (delta x y))
     (lambdap (delta x y)))
 ((use (delta-result))))

(prove-lemma
 delta-closedp
 (rewrite)
 (closedp (delta x y) 1)
 ((use (delta-result))))

; BUMP increments all variables of stack-level
; greater than N by one.
(defn bump (x n)
  (if (lambdap x)
      (lambda (bump (lbody x) (add1 n)))
    (if (combp x)
	(comb (bump (fun x) n) (bump (arg x) n))
      (if (varp x)
	  (if (lessp n x) (add1 x) x)
	x))))

; (SUBST X Y N) is the result of substituting Y for N in X.
(defn subst (x y n)
  (if (lambdap x)
      (lambda (subst (lbody x) (bump y (bump-base)) (add1 n)))
    (if (combp x)
	(comb (subst (fun x) y n) (subst (arg x) y n))
      (if (varp x)
	  (if (equal x n)	
	      y
	    (if (lessp n x)
		(sub1 x)
	      x))
	x))))

; X goes to value (EVAL X N) with no more than N recursive calls
; otherwise, (EVAL X N) is zero.
(defn eval (x n)
  (if (zerop n)
      0
    (if (valuep x)
	x
      (if (not (combp x))
	  0
	(let ((fn (eval (fun x) (sub1 n)))
	      (ag (eval (arg x) (sub1 n))))
	  (if (and (valuep fn) (valuep ag))
	      (if (lambdap fn)
		  (eval (subst (lbody fn) ag (var-base))
			(sub1 n))
		(if (delta-definedp fn ag)
		    (delta fn ag)
		  0))
	    0))))))

(prove-lemma
 eval-types
 (rewrite)
 (or (numberp (eval x n))
     (lambdap (eval x n))
     (constp (eval x n))))

(prove-lemma
 eval-zero
 (rewrite)
 (implies (numberp (eval x n))
	  (equal (eval x n) 0)))

(prove-lemma
 lambdap-bump
 (rewrite)
 (implies (lambdap x) (lambdap (bump x n))))

(prove-lemma
 lambdap-subst
 (rewrite)
 (implies (lambdap x) (lambdap (subst x y n))))

(prove-lemma 
 bump-lambdap
 (rewrite)
 (implies (lambdap x)
	  (equal (lbody (bump x n)) (bump (lbody x) (add1 n)))))

(prove-lemma 
 subst-lambda
 (rewrite)
 (implies (lambdap x)
	  (equal (lbody (subst x y n))
		 (subst (lbody x) (bump y (bump-base)) (add1 n)))))

; BUMP commutes with itself.
(prove-lemma
 bump-bump
 (rewrite)
 (implies (leq n m)
	  (equal (bump (bump y n) (add1 m))
		 (bump (bump y m) n))))

(defn bump-subst-induct (x y n m)
  (if (lambdap x)
      (bump-subst-induct (lbody x) (bump y (bump-base)) (add1 n) (add1 m))
    (if (combp x)
	(and (bump-subst-induct (fun x) y n m)
	     (bump-subst-induct (arg x) y n m))
      t)))

; BUMP distributes over SUBST.
(prove-lemma
 bump-subst
 (rewrite)
 (implies (lessp m n)
	  (equal (bump (subst x y n) m)
		 (subst (bump x m) (bump y m) (add1 n))))
 ((induct (bump-subst-induct x y n m))))

(defn subst-bump-induct (x y n)
  (if (lambdap x)
      (subst-bump-induct (lbody x) (bump y (bump-base)) (add1 n))
    (if (combp x)
	(and (subst-bump-induct (fun x) y n)
	     (subst-bump-induct (arg x) y n))
      t)))

(prove-lemma
 subst-bump
 (rewrite)
 (equal (subst (bump x n) y (add1 n)) x)
 ((induct (subst-bump-induct x y n))))

; SUBST distributes over SUBST.
(defn subst-subst-induct (x y z n)
  (if (lambdap x)
      (subst-subst-induct (lbody x)
			  (bump y (bump-base))
			  (bump z (bump-base))
			  (add1 n))
    (if (combp x)
	(and (subst-subst-induct (fun x) y z n)
	     (subst-subst-induct (arg x) y z n))
      t)))

(prove-lemma
 subst-subst				; Rewrites a simple
 (rewrite)				; expression into a
 (implies (varp n)			; more complex one.
	  (equal
	   (subst (subst x y n) z n)
	   (subst (subst x (bump z (sub1 n)) (add1 n)) (subst y z n) n)))
 ((induct (subst-subst-induct x y z n))))

; Closed terms are not changed by substitution.
(prove-lemma
 subst-of-closed-plus
 (rewrite)
 (implies (closedp x m)
	  (equal (subst x y (plus m n)) x)))

(prove-lemma
 subst-of-closed
 (rewrite)
 (implies (and (varp n) (closedp x (var-base)))
	  (equal (subst x y n) x))
 ((use (subst-of-closed-plus (x x) (m (var-base)) (y y) (n (sub1 n))))))



; Section 2: Reduction

; This section defines the notion of reduction and relates it to 
; evaluation.  The two most notable events are REAL-SUBST and
; EVAL-REDUCE.

(defn length (x)
  (if (listp x)
      (add1 (length (cdr x)))
    0))

(prove-lemma
 plus-one
 (rewrite)
 (equal (plus 1 x) (add1 x)))

; Defines closures and value environments using fake mutual recursion.
(defn closure-envp (x closure-mode)
  (if closure-mode			; In closurep mode
      (if (nlistp x)
	  f
	(and (valuep (car x))
	     (closedp (car x) (plus (var-base) (length (cdr x))))
	     (closure-envp (cdr x) f)))
    (if (nlistp x)			; In envp mode
	t
      (and (closure-envp (car x) t)
	   (closure-envp (cdr x) f)))))

(defn envp (e)				; A value environment
  (closure-envp e f))

(defn closurep (x)			; A value closure
  (closure-envp x t))

(defn closed-envp (x e)
  (and (envp e)
       (closedp x (plus (var-base) (length e)))))

(defn lookup (n e)
  (if (greaterp n (var-base))
      (lookup (sub1 n) (cdr e))
    (if (equal n (var-base))
	(car e)
      0)))

(prove-lemma
 lookup-is-closure
 (rewrite)
 (implies (and (varp x) (closed-envp x e))
	  (closure-envp (lookup x e) t))
 ((induct (lookup x e))))

; Term X under environment E goes to value closure (REDUCE X E N) 
; with no more than N recursive calls otherwise, (REDUCE X E N) is zero.
(defn reduce (x e n)
  (if (zerop n)
      0
    (if (constp x)
	(list x)
      (if (lambdap x)
	  (cons x e)
	(if (varp x)
	    (lookup x e)
	  (if (not (combp x))
	      0
	    (let ((fn (reduce (fun x) e (sub1 n)))
		  (ag (reduce (arg x) e (sub1 n))))
	      (if (and (closurep fn) (closurep ag))
		  (if (lambdap (car fn))
		      (reduce (lbody (car fn))
			      (cons ag (cdr fn))
			      (sub1 n))
		    (if (delta-definedp (car fn) (car ag))
			(list (delta (car fn) (car ag)))
		      0))
		0))))))))

(prove-lemma
 reduce-zero
 (rewrite)
 (implies
  (and (closed-envp x e)
       (not (closurep (reduce x e n))))
  (equal (reduce x e n) 0)))

(defn butt (x e)
  (if (listp e)
      (bump (butt x (cdr e)) (bump-base))
    x))

; The real value of term X under environment E is (REAL X E).
(defn real (x e)
  (if (listp e)
      (real (subst x
		   (butt (real (caar e) (cdar e)) (cdr e))
		   (var-base))
	    (cdr e))
    x))

(prove-lemma
 real-butt
 (rewrite)
 (equal (real (butt x e) e) x))

(prove-lemma
 real-const
 (rewrite)
 (implies (constp x) (equal (real x e) x)))

(prove-lemma
 real-lambda
 (rewrite)
 (implies (lambdap x)
	  (lambdap (real x e))))

(prove-lemma
 real-comb
 (rewrite)
 (equal (real (comb x y) e) (comb (real x e) (real y e))))

(prove-lemma
 real-error
 (rewrite)
 (implies 
  (and (not (varp x))
       (not (lambdap x))
       (not (combp x)))
  (equal (real x e) x)))

(defn real-subst-induct (x e)
  (if (listp e)
      (real-subst-induct
       (subst x
	      (bump (butt (real (caar e) (cdar e))
			  (cdr e))
		    (bump-base))
	      (add1 (var-base)))
       (cdr e))
    x))

;;; In case your interested, here is what real-subst-induct means.
(prove-lemma
 real-subst-induct-real
 ()
 (equal (lambda (real-subst-induct x e))
	(real (lambda x) e)))

; This lemma is used to show that substitution in the 
; Lambda Value Calculus is correctly implemented by
; concatenation of a closure to an environment.
(prove-lemma
 real-subst
 (rewrite)
 (implies
  (listp w)
  (equal (real x (cons w e))
	 (subst (lbody (real (lambda x) e))
		(real (car w) (cdr w))
		(var-base))))
 ((induct (real-subst-induct x e))))

(prove-lemma
 real-lookup
 (rewrite)
 (implies (varp x) 
	  (equal (real x e)
		 (if (geq (length e) x)
		     (real (car (lookup x e))
			   (cdr (lookup x e)))
		   (difference x (length e)))))
 ((induct (lookup x e))))

(prove-lemma
 var-real
 ()
 (implies
  (and (varp x) (envp e))
  (if (geq (length e) x)
      (valuep (real x e))
    (varp (real x e)))))

(disable real-lookup)

(prove-lemma
 real-lookup-lookup
 (rewrite)
 (implies (and (varp x) (closed-envp x e))
	  (equal (real (car (lookup x e)) (cdr (lookup x e))) (real x e)))
 ((induct (lookup x e))))

(prove-lemma
 real-lambda-closure
 (rewrite)
 (implies (closurep (cons x e))
	  (equal (lambdap (real x e)) (lambdap x))))

(prove-lemma
 real-const-closure
 (rewrite)
 (implies (closurep (cons x e))
	  (equal (constp (real x e)) (constp x)))
 ((use (real-lambda-closure))
  (expand (real x e)
	  (closedp x (add1 (length e))))
  (do-not-induct t)))

(prove-lemma
 real-comb-closed-envp-lambda
 ()
 (implies (lambdap x)
	  (equal (combp (real x e)) (combp x)))
 ((use (real-lambda))))

(prove-lemma
 real-comb-closed-envp
 (rewrite)
 (implies (closed-envp x e)
	  (equal (combp (real x e)) (combp x)))
 ((expand (closedp x (add1 (length e))) (real x e))
  (use (real-comb-closed-envp-lambda)
       (var-real) (real-error))
  (do-not-induct t)))

(prove-lemma
 real-closed-term
 (rewrite)
 (implies (closedp x 1) (equal (real x e) x)))

(prove-lemma
 closedp-subst
 (rewrite)
 (implies
  (and (closurep fn) (lambdap (car fn)))
  (closedp (lbody (car fn)) (add1 (add1 (length (cdr fn)))))))

(prove-lemma
 closure-env
 (rewrite)
 (implies (closure-envp x t)
	  (closure-envp (cdr x) f)))

(prove-lemma
 closed-env-subst
 (rewrite)
 (implies
  (and (closurep fn) (closurep ag) (lambdap (car fn)))
  (closed-envp (lbody (car fn)) (cons ag (cdr fn)))))

(prove-lemma
 eval-reduce-lambdap
 (rewrite)
 (implies
  (and (closed-envp x e)
       (equal (eval (real x e) n)
	      (real (car (reduce x e n))
		    (cdr (reduce x e n)))))
  (equal (lambdap (eval (real x e) n))
	 (lambdap (car (reduce x e n)))))
 ((use (real-lambda-closure (x (car (reduce x e n)))
			    (e (cdr (reduce x e n)))))))

(prove-lemma
 eval-reduce-constp
 (rewrite)
 (implies
  (and (closed-envp x e)
       (equal (eval (real x e) n)
	      (real (car (reduce x e n))
		    (cdr (reduce x e n)))) )
  (equal (constp (eval (real x e) n))
	 (constp (car (reduce x e n)))))
 ((use (real-const-closure
	(x (car (reduce x e n)))
	(e (cdr (reduce x e n)))))))

(prove-lemma
 eval-reduce-ncomb
 (rewrite)
 (implies
  (and (not (combp x)) (closed-envp x e))
  (equal (eval (real x e) n)
	 (real (car (reduce x e n))
	       (cdr (reduce x e n)))))
 ((use (var-real))))

(defn eval-reduce-induct (x e n)
  (if (zerop n)
      t
    (if (not (combp x))
	t
      (let ((fn (reduce (fun x) e (sub1 n))))
	(if (not (closurep fn))
	    (list
	     (eval-reduce-induct (arg x) e (sub1 n))
	     (eval-reduce-induct (fun x) e (sub1 n)))
	  (let ((ag (reduce (arg x) e (sub1 n))))
	    (if (not (closurep ag))
		(list
		 (eval-reduce-induct (arg x) e (sub1 n))
		 (eval-reduce-induct (fun x) e (sub1 n)))
	      (if (not (lambdap (car fn)))
		  (list
		   (eval-reduce-induct (arg x) e (sub1 n))
		   (eval-reduce-induct (fun x) e (sub1 n)))
		(list
		 (eval-reduce-induct (arg x) e (sub1 n))
		 (eval-reduce-induct (fun x) e (sub1 n))
		 (eval-reduce-induct (lbody (car fn))
				     (cons ag (cdr fn))
				     (sub1 n)))))))))))

; EVAL-REDUCE eliminates EVAL in favor of REDUCE.
(prove-lemma
 eval-reduce
 (rewrite)
 (implies (closed-envp x e)
	  (equal (eval (real x e) n)
		 (real (car (reduce x e n))
		       (cdr (reduce x e n)))))
 ((induct (eval-reduce-induct x e n))
  (disable real)))

(disable eval-reduce-ncomb)



; Section 3: The SECD Machine

; This section defines transitions in the SECD Machine via
; the event RUN-STEP.

(add-shell ret nil retp ())

(add-shell call nil callp ())

(add-shell halt nil haltp ())

(add-shell
 dump
 nil
 dumpp
 ((dump-stk (none-of) zero)
  (dump-env (none-of) zero)
  (dump-code (none-of) zero)
  (dump-dump (none-of) zero)))

(defn control-stringp (c e)
  (if (retp c)
      t
    (if (nlistp c)
	f
      (and 
       (or (callp (car c))
	   (closed-envp (car c) e))
       (control-stringp (cdr c) e)))))

(defn proper-dumpp (d)
  (if (dumpp d)
      (and (envp (dump-stk d))
	   (envp (dump-env d))
	   (control-stringp (dump-code d) (dump-env d))
	   (or (haltp (dump-dump d)) (proper-dumpp (dump-dump d))))
    f))

; The rewrite rules below that are derived from RUN-STEP 
; are more readable, and thus a better way to understand
; the SECD machine.   
(defn run-step (d)
  (if (not (dumpp d))
      0
    (if (retp (dump-code d))
	(if (and (listp (dump-stk d))
		 (dumpp (dump-dump d)))
	    (dump
	     (cons (car (dump-stk d)) (dump-stk (dump-dump d)))
	     (dump-env (dump-dump d))
	     (dump-code (dump-dump d))
	     (dump-dump (dump-dump d)))
	  0)
      (if (nlistp (dump-code d))
	  0
	(if (callp (car (dump-code d)))
	    (if (and (listp (dump-stk d))
		     (listp (cdr (dump-stk d))))
		(if (lambdap (caar (dump-stk d)))
		    (dump
		     nil
		     (cons (cadr (dump-stk d)) (cdar (dump-stk d)))
		     (cons (lbody (caar (dump-stk d))) (ret))
		     (dump
		      (cddr (dump-stk d))
		      (dump-env d)
		      (cdr (dump-code d))
		      (dump-dump d)))
		  (if (delta-definedp (caar (dump-stk d))
				      (caadr (dump-stk d)))
		      (dump
		       (cons (cons (delta (caar (dump-stk d))
					  (caadr (dump-stk d)))
				   nil)
			     (cddr (dump-stk d)))
		       (dump-env d)
		       (cdr (dump-code d))
		       (dump-dump d))
		    0))
	      0)
	  (if (lambdap (car (dump-code d)))
	      (dump
	       (cons (cons (car (dump-code d)) (dump-env d))
		     (dump-stk d))
	       (dump-env d)
	       (cdr (dump-code d))
	       (dump-dump d))
	    (if (combp (car (dump-code d)))
		(dump
		 (dump-stk d)
		 (dump-env d)
		 (cons (arg (car (dump-code d)))
		       (cons (fun (car (dump-code d)))
			     (cons (call)
				   (cdr (dump-code d)))))
		 (dump-dump d))
	      (if (varp (car (dump-code d)))
		  (if (geq (length (dump-env d)) (car (dump-code d)))
		      (dump
		       (cons (lookup (car (dump-code d)) (dump-env d))
			     (dump-stk d))
		       (dump-env d)
		       (cdr (dump-code d))
		       (dump-dump d))
		    0)
		(if (constp (car (dump-code d)))
		    (dump
		     (cons (cons (car (dump-code d)) nil)
			   (dump-stk d))
		     (dump-env d)
		     (cdr (dump-code d))
		     (dump-dump d))
		  0)))))))))

(prove-lemma
 run-step-proper
 (rewrite)
 (implies (and (proper-dumpp d) (dumpp (run-step d)))
	  (proper-dumpp (run-step d)))
 ((expand (run-step d))))

(defn run (d n)
  (if (zerop n)
      d
    (run (run-step d) (sub1 n))))

(prove-lemma
 run-run
 (rewrite)
 (equal (run d (plus n m)) (run (run d n) m))
 ((disable run-step)))

(prove-lemma
 run-not-dump
 (rewrite)
 (implies (not (dumpp d))
	  (equal (run d n) (if (zerop n) d 0)))
 ((expand (run d n))))

(defn run-proper-induct (d n)
  (if (zerop n)
      t
    (run-proper-induct (run-step d) (sub1 n))))

; Note that Lemma RUN-PROPER is not used in the remaining proof.
; I found it useful to prove this because the proof failed when there
; were bugs in RUN-STEP.
(prove-lemma
 run-proper
 (rewrite)
 (implies (and (proper-dumpp d) (dumpp (run d n)))
	      (proper-dumpp (run d n)))
 ((disable run-step)
  (induct (run-proper-induct d n))
  (use (run-step-proper))))

;;; Rewrite rules are defined so that RUN-STEP can be disabled.

(prove-lemma
 run-zero
 (rewrite)
 (implies (zerop n)
	  (equal (run d n) d)))

(prove-lemma
 run-ret
 (rewrite)
 (implies
  (retp c)
  (equal (run (dump s e c d) n)
	 (if (zerop n)
	     (dump s e c d)
	   (if (and (listp s) (dumpp d))
	       (run (dump
		     (cons (car s) (dump-stk d))
		     (dump-env d)
		     (dump-code d)
		     (dump-dump d))
		    (sub1 n))
	     0))))
 ((expand (run (dump s e c d) n))))

(prove-lemma
 run-call
 (rewrite)
 (implies
  (callp x)
  (equal (run (dump s e (cons x c) d) n)
	 (if (zerop n)
	     (dump s e (cons x c) d)
	   (if (and (listp s)
		    (listp (cdr s)))
	       (if (lambdap (caar s))
		   (run
		    (dump
		     nil
		     (cons (cadr s) (cdar s))
		     (cons (lbody (caar s)) (ret))
		     (dump
		      (cddr s)
		      e
		      c
		      d))
		    (sub1 n))
		 (if (delta-definedp (caar s)
				     (caadr s))
		     (run
		      (dump
		       (cons (cons (delta (caar s)
					  (caadr s))
				   nil)
			     (cddr s))
		       e
		       c
		       d)
		      (sub1 n))
		   0))
	     0))))
 ((expand (run (dump s e (cons x c) d) n))))

(prove-lemma
 run-lambda
 (rewrite)
 (implies
  (lambdap x)
  (equal (run (dump s e (cons x c) d) n)
	 (if (zerop n)
	     (dump s e (cons x c) d)
	   (run (dump (cons (cons x e) s) e c d) (sub1 n)))))
 ((expand (run (dump s e (cons x c) d) n))))


(prove-lemma
 run-comb
 (rewrite)
 (implies
  (combp x)
  (equal (run (dump s e (cons x c) d) n)
	 (if (zerop n)
	     (dump s e (cons x c) d)
	   (run (dump s
		      e
		      (cons (arg x) (cons (fun x) (cons (call) c)))
		      d)
		(sub1 n)))))
 ((expand (run (dump s e (cons x c) d) n))))

(prove-lemma
 run-var
 (rewrite)
 (implies
  (varp x)
  (equal (run (dump s e (cons x c) d) n)
	 (if (zerop n)
	     (dump s e (cons x c) d)
	   (if (geq (length e) x)
	       (run (dump (cons (lookup x e) s) e c d) (sub1 n))
	     0))))
 ((expand (run (dump s e (cons x c) d) n))))

(prove-lemma
 run-const
 (rewrite)
 (implies
  (constp x)
  (equal (run (dump s e (cons x c) d) n)
	 (if (zerop n)
	     (dump s e (cons x c) d)
	   (run (dump (cons (cons x nil) s) e c d) (sub1 n)))))
 ((expand (run (dump s e (cons x c) d) n))))

(prove-lemma
 run-bad-code-nlisp-c
 (rewrite)
 (implies
  (and (nlistp (dump-code d))
       (not (retp (dump-code d))))
  (equal (run d n) (if (zerop n) d 0)))
 ((expand (run d n))))

(prove-lemma
 run-bad-code-listp-c
 (rewrite)
 (implies
  (and (listp (dump-code d))
       (not (callp (car (dump-code d))))
       (not (lambdap (car (dump-code d))))
       (not (combp (car (dump-code d))))
       (not (varp (car (dump-code d))))
       (not (constp (car (dump-code d)))))
  (equal (run d n) (if (zerop n) d 0)))
 ((expand (run d n))))

(disable run)



; Section 4: Timing

; This section associates SECD run step counts with closures 
; computed by REDUCE.  The event REDUCE-TIMED-REDUCE eliminates
; REDUCE in favor of TIMED-REDUCE.

; Term X under environment E goes to value closure 
; (CAR (TIMED-REDUCE X E N)) with no more than N recursive calls 
; in time (CDR (TIMED-REDUCE X E N)).  The time computed is the
; number of steps required by the SECD machine to do the equivalent
; computation.
(defn timed-reduce (x e n)
  (if (zerop n)
      0
    (if (constp x)
	(cons (list x) 1)
      (if (lambdap x)
	  (cons (cons x e) 1)
	(if (varp x)
	    (cons (lookup x e) 1)
	  (if (not (combp x))
	      0
	    (let ((fn (timed-reduce (fun x) e (sub1 n)))
		  (ag (timed-reduce (arg x) e (sub1 n))))
	      (if (and (closurep (car fn)) (closurep (car ag)))
		  (if (lambdap (caar fn))
		      (let ((ans (timed-reduce (lbody (caar fn))
					       (cons (car ag) (cdar fn))
					       (sub1 n))))
			(if (closurep (car ans))
			    (cons (car ans)
				  (plus 1 (plus
					   (cdr ag)
					   (plus
					    (cdr fn)
					    (plus 1 (plus
						     (cdr ans)
						     1))))))
			  0))
		    (if (delta-definedp (caar fn) (caar ag))
			(cons 
			 (list (delta (caar fn) (caar ag)))
			 (plus 1 (plus (cdr ag) (plus (cdr fn) 1))))
		      0))
		0))))))))

(prove-lemma
 timed-reduce-zero
 (rewrite)
 (implies (numberp (timed-reduce x e n))
	  (equal (timed-reduce x e n) 0)))

(prove-lemma
 timed-reduce-car-closure-is-listp
 (rewrite)
 (implies
  (closed-envp x e)
  (equal
   (closure-envp (car (timed-reduce x e n)) t)
   (listp (timed-reduce x e n)))))

(prove-lemma
 reduce-timed-reduce
 (rewrite)
 (implies
  (closed-envp x e)
  (equal (reduce x e n)
	 (car (timed-reduce x e n))))
 ((induct (reduce x e n))))



; Section 5: The Adequacy Theorem

; The events in this section show that when (EVAL X N) is
; a value, the SECD Machine computes that value.

(defn values-agree-induct (x n s e c d)
  (if (zerop n)
      t
    (if (not (listp (timed-reduce x e n)))
	t
      (if (not (combp x))
	  t
	(let ((ag (car (timed-reduce (arg x) e (sub1 n)))))
	  (if (lambdap (caar (timed-reduce (fun x) e (sub1 n))))
	      (list
	       (values-agree-induct (arg x) (sub1 n) s e
				    (cons (fun x) (cons (call) c))
				    d)
	       (values-agree-induct (fun x) (sub1 n)
				    (cons ag s) e
				    (cons (call) c)
				    d)
	       (let ((fn (car (timed-reduce (fun x) e (sub1 n)))))
		 (values-agree-induct
		  (lbody (car fn)) (sub1 n) nil (cons ag (cdr fn)) (ret)
		  (dump s e c d))))
	    (list
	     (values-agree-induct (arg x) (sub1 n) s e
				  (cons (fun x) (cons (call) c))
				  d)
	     (values-agree-induct (fun x) (sub1 n)
				  (cons ag s) e
				  (cons (call) c)
				  d))))))))

(prove-lemma
 values-agree
 (rewrite)
 (implies
  (closed-envp x e)
  (equal (run (dump s e (cons x c) d)
	      (cdr (timed-reduce x e n)))
	 (if (listp (timed-reduce x e n))
	     (dump (cons (car (timed-reduce x e n)) s)
		   e c d)
	   (dump s e (cons x c) d))))
 ((induct (values-agree-induct x n s e c d))))

(prove-lemma
 adequacy
 ()
 (implies
  (and (closed-termp x)
       (valuep (eval x n)))
  (and (equal (run (dump nil nil (cons x (ret)) (halt))
		   (cdr (timed-reduce x nil n)))
	      (dump (list (reduce x nil n)) nil (ret) (halt)))
       (closurep (reduce x nil n))
       (equal (eval x n)
	      (real (car (reduce x nil n))
		    (cdr (reduce x nil n))))))
 ((use (values-agree (e nil) (s nil) (c (ret)) (d (halt)))
       (eval-reduce (e nil)))
  (do-not-induct t)))



; Section 6: The Faithfulness Theorem

; The events in this section show that when (EVAL X N) is
; not a value, a run of the SECD Machine of length N never 
; reaches an accepting state.  The three most notable events are
; LISTP-RUN-NOT-ACCEPT, NVALUE-AGREE, and FAITHFULNESS.

;;; Some facts about difference from:
;;;
;             A Formal Model of Asynchronous Communication
;                                 and
;      Its Use in Mechanically Verifying a Biphase Mark Protocol
;
;
;                           J Strother Moore
;
;                         Technical Report 68
;                             August, 1991

(prove-lemma 
 difference-is-0
 (rewrite)
 (implies (not (lessp y x))
	  (equal (difference x y) 0)))

(prove-lemma
 difference-plus-cancellation1
             (rewrite)
             (equal (difference (plus i x) i)
                    (fix x)))

(prove-lemma
 difference-plus-cancellation2
             (rewrite)
             (equal (difference (plus i x) (plus i y))
                    (difference x y)))

(prove-lemma 
 difference-difference
 (rewrite)
 (implies (not (lessp b c))
	  (equal (difference a (difference b c))
		 (difference (plus a c) b))))

(prove-lemma
 difference-difference-other
 (rewrite)
 (equal (difference (difference a b) c)
	(difference a (plus b c))))

;;; and one more rule...
(prove-lemma
 plus-difference
 (rewrite)
 (implies (not (lessp n m))
	  (equal (plus m (difference n m)) (fix n))))

; An accepting dump.
(defn acceptp (d)
  (and (dumpp d)
       (listp (dump-stk d))
       (retp (dump-code d))
       (haltp (dump-dump d))))

; RUN-NOT-ACCEPTP is true when the initial N dumps of a run
; are not accepting dumps.
(defn run-not-acceptp (d n)
  (if (zerop n)
      t
    (if (acceptp d)
	f
      (run-not-acceptp (run d 1) (sub1 n)))))

(prove-lemma
 run-not-acceptp-ndumpp
 (rewrite)
 (implies (not (dumpp d))
	  (run-not-acceptp d n)))

(prove-lemma
 dumpp-run-accept
 (rewrite)
 (implies
  (acceptp d)
  (equal (dumpp (run d n)) (zerop n))))

(prove-lemma
 run-one-sub1-elim
 (rewrite)
 (implies
  (not (zerop n))
  (equal (run (run d 1) (sub1 n)) (run d n)))
 ((use (run-run (n 1) (m (sub1 n))))))

(prove-lemma
 dumpp-run-not-accept
 (rewrite)
 (implies (dumpp (run d n))
	  (run-not-acceptp d n)))

(defn run-not-accept-induct (d n)
  (if (zerop n)
      t
    (run-not-accept-induct (run d 1) (sub1 n))))

(prove-lemma
 run-not-accept-plus
 (rewrite)
 (implies
  (run-not-acceptp d n)
  (equal (run-not-acceptp d (plus n m))
	 (run-not-acceptp (run d n) m)))
 ((induct (run-not-accept-induct d n))))

(disable run-one-sub1-elim)

(prove-lemma
 not-accept-run-x-zero
 (rewrite)
 (not (acceptp (dump s e (cons x c) d))))

(prove-lemma
 nvalue-agree-ncomb
 (rewrite)
  (implies
   (and (closed-envp x e)
	(not (combp x))
	(numberp (timed-reduce x e n)))
   (run-not-acceptp (dump s e (cons x c) d) n))
  ((expand (closedp x (add1 (length e))))))

; Force expansion of RUN-NOT-ACCEPTP in certain situations.
(prove-lemma
 run-not-accept-comb
 (rewrite)
 (implies
  (combp x)
  (equal 
   (run-not-acceptp (dump s e (cons x c) d) n)
   (if (zerop n)
       t
     (run-not-acceptp (dump s e
			    (cons (arg x) (cons (fun x) (cons (call) c)))
			    d)
		      (sub1 n))))))

(prove-lemma
 run-not-accept-call
 (rewrite)
 (implies
  (callp x)
  (equal 
   (run-not-acceptp (dump s e (cons x c) d) n)
   (if (zerop n)
       t
     (run-not-acceptp (run (dump s e (cons x c) d) 1)
		      (sub1 n))))))

(prove-lemma
 listp-run-not-accept-equal
 (rewrite)
 (implies
  (and (closed-envp x e)
       (listp (timed-reduce x e n)))
  (run-not-acceptp (dump s e (cons x c) d)
		   (cdr (timed-reduce x e n)))))

(prove-lemma
 run-not-accept-mono-add1
 (rewrite)
 (implies (run-not-acceptp d (add1 n))
	  (run-not-acceptp d n)))

(prove-lemma
 run-not-accept-mono
 (rewrite)
 (implies (run-not-acceptp d n)
	  (run-not-acceptp d (difference n m))))

(prove-lemma
 listp-run-not-accept-nlessp
 (rewrite)
 (implies
  (and (closed-envp x e)
       (listp (timed-reduce x e n))
       (not (lessp (cdr (timed-reduce x e n)) n)))
   (run-not-acceptp (dump s e (cons x c) d) n))
 ((use (run-not-accept-mono
	(d (dump s e (cons x c) d))
	(n (cdr (timed-reduce x e n)))
	(m (difference (cdr (timed-reduce x e n)) n))))))

(prove-lemma
 listp-run-not-accept-lessp
 (rewrite)
 (implies
  (and (closed-envp x e)
       (listp (timed-reduce x e n))
       (lessp (cdr (timed-reduce x e n)) n))
  (equal 
   (run-not-acceptp (dump s e (cons x c) d) n)
   (run-not-acceptp
    (dump (cons (car (timed-reduce x e n)) s) e c d)
    (difference n (cdr (timed-reduce x e n))))))
 ((use (run-not-accept-plus
	(d (dump s e (cons x c) d))
	(n (cdr (timed-reduce x e n)))
	(m (difference n (cdr (timed-reduce x e n))))))))

(prove-lemma
 listp-run-not-accept
 (rewrite)
 (implies
  (and (closed-envp x e)
       (listp (timed-reduce x e n)))
  (equal 
   (run-not-acceptp (dump s e (cons x c) d) n)
   (run-not-acceptp
    (dump (cons (car (timed-reduce x e n)) s) e c d)
    (difference n (cdr (timed-reduce x e n))))))
 ((use (listp-run-not-accept-lessp)
       (listp-run-not-accept-nlessp))))

(disable listp-run-not-accept-lessp)
(disable listp-run-not-accept-nlessp)

(prove-lemma
 nvalue-agree-nlambda
 (rewrite)
 (implies
  (and (not (zerop n))
       (combp x)
       (closed-envp x e)
       (numberp (timed-reduce x e n))
       (listp (timed-reduce (fun x) e (sub1 n)))
       (listp (timed-reduce (arg x) e (sub1 n)))
       (not (lambdap (caar (timed-reduce (fun x) e (sub1 n))))))
  (run-not-acceptp (dump s e (cons x c) d) n))
 ((expand (timed-reduce x e n))
  (disable timed-reduce)))

(prove-lemma
 nvalue-agree-lambda-numberp
 (rewrite)
 (implies
  (and (not (zerop n))
       (combp x)
       (closed-envp x e)
       (listp (timed-reduce (arg x) e (sub1 n)))
       (listp (timed-reduce (fun x) e (sub1 n)))
       (lambdap (caar (timed-reduce (fun x) e (sub1 n))))
       (numberp
	(timed-reduce (lbody (caar (timed-reduce (fun x) e (sub1 n))))
		      (cons (car (timed-reduce (arg x) e (sub1 n)))
			    (cdar (timed-reduce (fun x) e (sub1 n))))
		      (sub1 n)))
       (run-not-acceptp
	(dump nil
	      (cons (car (timed-reduce (arg x) e (sub1 n)))
		    (cdar (timed-reduce (fun x) e (sub1 n))))
	      (cons (lbody (caar (timed-reduce (fun x) e (sub1 n))))
		    (ret))
	      (dump s e c d))
	(sub1 n)))
  (run-not-acceptp
   (dump (cons (car (timed-reduce (arg x) e (sub1 n))) s)
	 e
	 (cons (fun x) (cons (call) c))
	 d)
   (difference (sub1 n)
	       (cdr (timed-reduce (arg x) e (sub1 n))))))
 ((disable timed-reduce)
  (use
   (run-not-accept-mono
    (d (dump (cons (car (timed-reduce (arg x) e (sub1 n))) s)
	     e
	     (cons (fun x) (cons (call) c))
	     d))
    (n (sub1 n))
    (m (cdr (timed-reduce (arg x) e (sub1 n))))))
  (do-not-induct t)))

(prove-lemma
 nvalue-agree-lambda-listp
 (rewrite)
 (implies
  (and (not (zerop n))
       (combp x)
       (closed-envp x e)
       (numberp (timed-reduce x e n))
       (listp (timed-reduce (fun x) e (sub1 n)))
       (listp (timed-reduce (arg x) e (sub1 n)))
       (listp (timed-reduce (lbody (caar (timed-reduce (fun x) e (sub1 n))))
			    (cons (car (timed-reduce (arg x) e (sub1 n)))
				  (cdar (timed-reduce (fun x) e (sub1 n))))
			    (sub1 n)))
       (lambdap (caar (timed-reduce (fun x) e (sub1 n)))))
  (run-not-acceptp (dump s e (cons x c) d) n))
 ((expand (timed-reduce x e n))
  (disable timed-reduce)))

(defn nvalue-agree-induct (x n s e c d)
  (if (zerop n)
      t
    (if (not (combp x))
	t
      (let ((ag (timed-reduce (arg x) e (sub1 n))))
	(if (numberp ag)
	    (nvalue-agree-induct
	     (arg x) (sub1 n) s e (cons (fun x) (cons (call) c)) d)
	  (let ((fn (timed-reduce (fun x) e (sub1 n))))
	    (if (numberp fn)
		(nvalue-agree-induct
		 (fun x) (sub1 n) (cons (car ag) s) e (cons (call) c) d)
	      (if (not (lambdap (caar fn)))
		  t
		(let ((ans (timed-reduce (lbody (caar fn))
					 (cons (car ag) (cdar fn))
					 (sub1 n))))
		  (if (numberp ans)
		      (nvalue-agree-induct
		       (lbody (caar fn)) (sub1 n)
		       nil (cons (car ag) (cdar fn)) (ret)
		       (dump s e c d))
		    t))))))))))

(prove-lemma
 nvalue-agree
 (rewrite)
 (implies
  (and (closed-envp x e)
       (numberp (timed-reduce x e n)))
  (run-not-acceptp (dump s e (cons x c) d) n))
 ((induct (nvalue-agree-induct x n s e c d))
  (expand (timed-reduce x e n))
  (disable timed-reduce)))

; The next four events are used to show that:
; (IMPLIES (NOT (VALUEP (EVAL (REAL X E) N))) 
;          (NUMBERP (TIMED-REDUCE X E N)))
(prove-lemma
 nclosure-nvalue-real
 (rewrite)
 (implies
  (not (valuep (real (car w) (cdr w))))
  (not (closure-envp w t))))

(prove-lemma
 nclosure-number-real
 (rewrite)
 (implies
  (numberp (real (car w) (cdr w)))
  (not (closure-envp w t))))

(prove-lemma
 eval-reduce-numberp
 (rewrite)
 (implies
  (and (closed-envp x e)
       (numberp (eval (real x e) n)))
  (not (closure-envp (reduce x e n) t))))

(prove-lemma
 reduce-timed-reduce-numberp
 (rewrite)
 (implies
  (and (closed-envp x e)
       (not (closure-envp (reduce x e n) t)))
  (numberp (timed-reduce x e n))))

(prove-lemma
 faithfulness
 ()
 (implies
  (and (closed-termp x)
       (not (valuep (eval x n))))
  (run-not-acceptp (dump nil nil (cons x (ret)) (halt)) n))
 ((use (nvalue-agree (s nil) (e nil) (c (ret)) (d (halt))))
  (disable eval-reduce reduce-timed-reduce)))