#| Copyright (C) 1993 by Matt Wilding. This script is hereby placed in the public domain, and therefore unlimited editing and redistribution is permitted. NO WARRANTY Matt Wilding 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 Matt Wilding 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. |# (note-lib "piton" t) ;; NIM Piton proof ;; Matt Wilding 4-15-92 ;; modified 7-92 to work on Piton library ;; This script takes 10 hours to run on a 64 meg Sparc2 ;; This work is described in Technical Report #78. A presentation ;; about this work was made at the CLI research review in April 92. #| Nim is a game played with piles of matches. Two opponents alternate taking at least one match from exactly one pile until there are no matches left. The player who takes the last match loses. Piton is an assembly-level language with a formal semantics and a verified compiler. Piton is described in CLI tech report #22. One of the machines to which Piton is targeted is FM9001, a microprocessor that has a formal semantics and that has been fabricated. This proof script leads NQTHM to a proof that a Piton program that "plays" Nim does so optimally. Informally, this means a) A Piton program (see function CM-PROG) when run on the Piton interpreter and given as input a reasonable Nim state yields a new Nim state equal to what is calculated by function COMPUTER-MOVE. (See event COMPUTER-MOVE-IMPLEMENTED.) b) COMPUTER-MOVE generates valid moves. That is, it removes at least one match from exactly one pile. (VALID-MOVEP-COMPUTER-MOVE) c) Depth-first search of the state space of all possible moves is used to define what is meant by optimal Nim play. Exhaustive search is used to find if there is a strategy for a Nim player to ensures eventual victory from the current Nim state. An optimal strategy transforms any state for which there exists such a winning strategy into a state from which exhaustive search can find no winning strategy. Exhaustive search of all possible moves from a NIM state is formalized in the function WSP. The optimalilty of the strategy COMPUTER-MOVE is proved in the event COMPUTER-MOVE-WORKS. d) The FM9001 Piton compiler correctness theorem assumes that the Piton state that is to be run contains valid Piton code, fit into an FM9001's memory, and use constants of word size 32. A Piton state (used in the Indiana test described below) was constructed that contains the Nim program, and is proved to meet the compiler correctness constraints (CM-PROG-FM9001-LOADABLE) The algorithm used by the program is non-obvious and very efficient, avoiding the need to search. (I invented the programming trick only to subsequently discover that it has been known since the beginning of the century.) See tech report #78 for a description. (Constant bounds on the number of Piton instructions executed while running this program have been proved using PC-NQTHM. These events are not included in this NQTHM-processable script, but the theorem is included in comments later in this file for completeness.) This script was developed using only those events from the Piton library necessary to define the interpreter and the naturals library. In July 92 it was modified somewhat to "fit" onto the Piton library that sits on top of the FM9001 library. The immediate motivation was to make it easier to include in the upcoming NQTHM-1992 proveall release being put together by Boyer. The Piton library contains the events of the FM9001 library. The FM9001 library contains an older version of the naturals library (though not explicitly with a note-lib). Thus, this script requires only the Piton library. In May 92, in consultation with researchers at Indiana University, I compiled the Nim Piton program for the FM9001 and sent the image to Indiana. They ran the image and generated an optimal NIM move on a fabricated FM9001 they had wired up. The intial image and part of the resulting image is included in a comment at the end of this script. A non-trivial program compiled using a reasonably-complex compiler for a small microprocessor worked without any conventional testing done on any of the components, and everyone was pleased but not surprised. |# (set-status addition-on addition ((otherwise enable))) (set-status multiplication-on multiplication ((otherwise enable))) (set-status remainders-on remainders ((otherwise enable))) (set-status quotients-on quotients ((otherwise enable))) (set-status exponentiation-on exponentiation ((otherwise enable))) (set-status logs-on logs ((otherwise enable))) (set-status gcds-on gcds ((otherwise enable))) (defn clock-plus (x y) (plus x y)) (prove-lemma p-add1 (rewrite) (equal (p p0 (add1 n)) (p (p-step p0) n)) ((disable p-step))) (prove-lemma p-0 (rewrite) (implies (zerop n) (equal (p p0 n) p0))) (prove-lemma clock-plus-function (rewrite) (equal (p p0 (clock-plus x y)) (p (p p0 x) y)) ((induct (p p0 x)) (disable p p-step))) (disable p-add1) (prove-lemma clock-plus-add1 (rewrite) (equal (p p0 (clock-plus (add1 x) y)) (p p0 (add1 (clock-plus x y))))) (disable clock-plus) (prove-lemma clock-plus-0 (rewrite) (implies (zerop x) (equal (clock-plus x y) (fix y))) ((enable clock-plus))) (prove-lemma fix-clock-plus (rewrite) (equal (fix (clock-plus x y)) (clock-plus x y)) ((enable clock-plus))) (prove-lemma p-step1-opener (rewrite) (equal (p-step1 (cons opcode operands) p) (if (p-ins-okp (cons opcode operands) p) (p-ins-step (cons opcode operands) p) (p-halt p (x-y-error-msg 'p opcode)))) ((disable p-ins-okp p-ins-step))) (disable p-step1) (prove-lemma p-opener (rewrite) (and (equal (p s 0) s) (equal (p (p-state pc ctrl temp prog data max-ctrl max-temp word-size psw) (add1 n)) (p (p-step (p-state pc ctrl temp prog data max-ctrl max-temp word-size psw)) n))) ((disable p-step))) (disable p) (defn at-least-morep (base delta value) (not (lessp value (plus base delta)))) (prove-lemma at-least-morep-normalize (rewrite) (and (equal (at-least-morep (add1 base) delta value) (at-least-morep base (add1 delta) value)) (equal (at-least-morep base (add1 delta) (add1 value)) (at-least-morep base delta value)))) (prove-lemma at-least-morep-linear (rewrite) (implies (and (at-least-morep base d1 value) (not (lessp d1 d2))) (at-least-morep base d2 value))) (prove-lemma lessp-as-at-least-morep (rewrite) (implies (at-least-morep base delta value) (and (equal (lessp value x) (not (at-least-morep x 0 value))) (equal (lessp x value) (at-least-morep x 1 value))))) (disable at-least-morep) (defn nat-to-bv (nat size) (if (zerop size) nil (if (lessp nat (exp 2 (sub1 size))) (cons 0 (nat-to-bv nat (sub1 size))) (cons 1 (nat-to-bv (difference nat (exp 2 (sub1 size))) (sub1 size)))))) (defn nat-to-bv-state (state size) (if (listp state) (cons (nat-to-bv (car state) size) (nat-to-bv-state (cdr state) size)) nil)) ;; a more elegant way to write this program would be to use the ;; bit-vector of all 0's initially, then xor all the elements of ;; the array. But we don't want a pointer to memory to ;; ever have an improper value, so we write things this way (defn xor-bvs-program nil '(xor-bvs (vecs-addr numvecs) nil (push-local vecs-addr) (fetch) (push-local numvecs) (sub1-nat) (pop-local numvecs) (dl loop () (push-local numvecs)) (test-nat-and-jump zero done) (push-local numvecs) (sub1-nat) (pop-local numvecs) (push-local vecs-addr) (push-constant (nat 1)) (add-addr) (set-local vecs-addr) (fetch) (xor-bitv) (jump loop) (dl done () (ret)))) (defn bit-vectors-piton (array size) (if (listp array) (and (listp (car array)) (equal (caar array) 'bitv) (bit-vectorp (cadar array) size) (equal (cddar array) nil) (bit-vectors-piton (cdr array) size)) (equal array nil))) (defn array (name segment) (cdr (assoc name segment))) ;; vecs is name of state (defn xor-bvs-input-conditionp (p0) (and (equal (car (top (p-temp-stk p0))) 'nat) (equal (car (top (cdr (p-temp-stk p0)))) 'addr) (equal (cdadr (top (cdr (p-temp-stk p0)))) 0) (listp (cadr (top (cdr (p-temp-stk p0))))) (equal (cddr (top (p-temp-stk p0))) nil) (equal (cddr (top (cdr (p-temp-stk p0)))) nil) (definedp (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0)) (bit-vectors-piton (array (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0)) (p-word-size p0)) (equal (cadr (top (p-temp-stk p0))) (length (array (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0)))) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 4 (p-max-ctrl-stk-size p0)) (at-least-morep (length (p-temp-stk p0)) 2 (p-max-temp-stk-size p0)) (not (zerop (untag (top (p-temp-stk p0))))) (lessp (untag (top (p-temp-stk p0))) (exp 2 (p-word-size p0))) (listp (p-ctrl-stk p0)))) ; time to run loop (defn xor-bvs-clock-loop (numvecs) (if (zerop numvecs) 3 (plus 12 (xor-bvs-clock-loop (sub1 numvecs))))) ; time to run xor-bvs, including call and ret (defn xor-bvs-clock (numvecs) (plus 6 (xor-bvs-clock-loop (sub1 numvecs)))) (defn xor-bvs-array (current array n array-size) (if (zerop n) current (xor-bvs-array (xor-bitv current (untag (get (difference array-size n) array))) array (sub1 n) array-size))) (prove-lemma lessp-1-exp (rewrite) (equal (lessp 1 (exp a b)) (and (lessp 1 a) (not (zerop b)))) ((enable exp))) (prove-lemma bit-vectors-piton-means (rewrite) (implies (and (bit-vectors-piton state size) (lessp p (length state))) (and (equal (car (get p state)) 'bitv) (listp (get p state)) (bit-vectorp (cadr (get p state)) size) (equal (cddr (get p state)) nil)))) (defn xor-bvs-loop-correctness-general-induct (i current n s data-segment) (if (zerop i) t (xor-bvs-loop-correctness-general-induct (sub1 i) (xor-bitv current (cadr (get (difference n i) (array s data-segment)))) n s data-segment))) ;; in Piton library ;(prove-lemma bit-vectorp-xor-bitv (rewrite) ; (implies ; (and ; (bit-vectorp x size) ; (bit-vectorp y size)) ; (bit-vectorp (xor-bitv x y) size))) (enable bit-vectorp-xor-bitv) (prove-lemma xor-bvs-loop-correctness-general nil (implies (and (lessp (length (array s data-segment)) (exp 2 word-size)) (not (zerop word-size)) (listp ctrl-stk) (bit-vectors-piton (array s data-segment) word-size) (at-least-morep (length temp-stk) 3 max-temp-stk-size) (equal (definition 'xor-bvs prog-segment) (xor-bvs-program)) (definedp s data-segment) (numberp i) (lessp i n) (bit-vectorp current word-size) (equal n (length (array s data-segment)))) (equal (p (p-state '(pc (xor-bvs . 5)) (cons (list (list (cons 'vecs-addr (list 'addr (cons s (sub1 (difference n i))))) (cons 'numvecs (list 'nat i))) ret-pc) ctrl-stk) (cons (list 'bitv current) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (xor-bvs-clock-loop i)) (p-state ret-pc ctrl-stk (cons (list 'bitv (xor-bvs-array current (array s data-segment) i n)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((induct (xor-bvs-loop-correctness-general-induct i current n s data-segment)))) (prove-lemma difference-x-sub1-x-better (rewrite) (equal (difference x (sub1 x)) (if (lessp 0 x) 1 0))) (prove-lemma xor-bvs-loop-correctness nil (implies (and (lessp (length (array s data-segment)) (exp 2 word-size)) (not (zerop word-size)) (listp ctrl-stk) (bit-vectors-piton (array s data-segment) word-size) (at-least-morep (length temp-stk) 3 max-temp-stk-size) (equal (definition 'xor-bvs prog-segment) (xor-bvs-program)) (definedp s data-segment) (lessp 0 n) (bit-vectorp current word-size) (equal n (length (array s data-segment)))) (equal (p (p-state '(pc (xor-bvs . 5)) (cons (list (list (cons 'vecs-addr (list 'addr (cons s 0))) (cons 'numvecs (list 'nat (sub1 n)))) ret-pc) ctrl-stk) (cons (list 'bitv current) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (xor-bvs-clock-loop (sub1 n))) (p-state ret-pc ctrl-stk (cons (list 'bitv (xor-bvs-array current (array s data-segment) (sub1 n) n)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((use (xor-bvs-loop-correctness-general (i (sub1 n)))))) (prove-lemma exp-0 (rewrite) (implies (zerop x) (and (equal (exp x y) (if (zerop y) 1 0)) (equal (exp y x) 1))) ((enable exp))) (prove-lemma bit-vectors-piton-means-more (rewrite) (implies (and (listp x) (bit-vectors-piton x size)) (equal (LIST 'BITV (CADAR x)) (car x)))) ;; xor-bvs of an array of at least one bit vector (defn xor-bvs (array) (if (listp array) (xor-bitv (car array) (xor-bvs (cdr array))) nil)) (defn untag-array (array) (if (listp array) (cons (untag (car array)) (untag-array (cdr array))) nil)) (prove-lemma bit-vectorp-get (rewrite) (implies (bit-vectors-piton array size) (equal (bit-vectorp (untag (get n array)) size) (lessp n (length array))))) ;(prove-lemma difference-sub1-arg2 (rewrite) ; (equal ; (difference a (sub1 n)) ; (if (zerop n) (fix a) ; (if (lessp a n) 0 (add1 (difference a n)))))) (enable difference-sub1-arg2) (prove-lemma xor-bitv-commutative (rewrite) (implies (equal (length a) (length b)) (equal (xor-bitv a b) (xor-bitv b a)))) (prove-lemma xor-bitv-commutative2 (rewrite) (implies (equal (length a) (length b)) (equal (xor-bitv a (xor-bitv b c)) (xor-bitv b (xor-bitv a c))))) (prove-lemma xor-bitv-associative (rewrite) (implies (equal (length a) (length b)) (equal (xor-bitv (xor-bitv a b) c) (xor-bitv a (xor-bitv b c))))) (prove-lemma length-from-bit-vectorp (rewrite) (implies (bit-vectorp x s) (equal (length x) (fix s)))) (prove-lemma length-xor-bitv (rewrite) (equal (length (xor-bitv a b)) (length a))) (prove-lemma length-cadr-get-bit-vectors-piton (rewrite) (implies (and (bit-vectors-piton x l) (lessp i (length x))) (equal (length (cadr (get i x))) (fix l)))) (prove-lemma equal-xor-bitv-x-x (rewrite) (implies (and (bit-vectorp b (length a)) (bit-vectorp c (length a))) (equal (equal (xor-bitv a b) (xor-bitv a c)) (equal b c)))) (defn bit-vectorp-induct (size a b) (if (zerop size) t (bit-vectorp-induct (sub1 size) (cdr a) (cdr b)))) (prove-lemma bit-vectorp-xor-bitv2 (rewrite) (equal (bit-vectorp (xor-bitv a b) size) (equal (length a) (fix size))) ((induct (bit-vectorp-induct size a b)))) (defn bit-vectorsp (bvs size) (if (listp bvs) (and (bit-vectorp (car bvs) size) (bit-vectorsp (cdr bvs) size)) (equal bvs nil))) (prove-lemma length-xor-bvs (rewrite) (implies (bit-vectorsp bvs (length (car bvs))) (equal (length (xor-bvs bvs)) (length (car bvs))))) (prove-lemma bit-vectorsp-untag (rewrite) (implies (bit-vectors-piton x s) (bit-vectorsp (untag-array x) s))) (prove-lemma bit-vectorsp-cdr-untag (rewrite) (implies (bit-vectors-piton (cdr x) s) (bit-vectorsp (cdr (untag-array x)) s))) ;; actually part of npiton-defs, but not supporter of p ;; ;(DEFN NTHCDR ; (N L) ; (IF (ZEROP N) ; L ; (NTHCDR (SUB1 N) (CDR L)))) (enable nthcdr) (prove-lemma bit-vectorsp-nthcdr (rewrite) (implies (and (bit-vectorsp x s) (lessp n (length x))) (bit-vectorsp (nthcdr n x) s)) ((enable nthcdr))) (prove-lemma bit-vectorp-xor-bvs (rewrite) (implies (and (bit-vectorsp x size) (listp x)) (bit-vectorp (xor-bvs x) size))) (prove-lemma length-untag-array (rewrite) (equal (length (untag-array x)) (length x))) ;(prove-lemma listp-nthcdr (rewrite) ; (equal ; (listp (nthcdr n x)) ; (lessp n (length x))) ; ((enable nthcdr))) (enable listp-nthcdr) (prove-lemma nthcdr-open (rewrite) (implies (lessp n (length x)) (equal (nthcdr n x) (cons (get n x) (nthcdr (add1 n) x)))) ((enable nthcdr))) (prove-lemma get-untag-array (rewrite) (implies (lessp n (length x)) (equal (get n (untag-array x)) (cadr (get n x))))) (prove-lemma equal-xor-bitv-x-x-special (rewrite) (implies (and (bit-vectorp b (length a)) (bit-vectorp (xor-bitv z c) (length a))) (equal (equal (xor-bitv a b) (xor-bitv z (xor-bitv a c))) (equal b (xor-bitv z c))))) (defn fix-bit (b) (if (equal b 0) 0 1)) (prove-lemma xor-bitv-0 (rewrite) (and (equal (xor-bit x 0) (fix-bit x)) (equal (xor-bit 0 x) (fix-bit x)))) (prove-lemma xor-bitv-nlistp (rewrite) (implies (not (listp c)) (equal (xor-bitv a (xor-bitv b c)) (xor-bitv a b)))) (prove-lemma xor-bitv-nlistp2 (rewrite) (implies (and (bit-vectorp a b) (not (listp c))) (equal (xor-bitv a c) a))) (prove-lemma xor-bvs-array-rewrite (rewrite) (implies (and (bit-vectors-piton array (length current)) (bit-vectorp current (length current)) (lessp n (length array)) (equal (length array) as)) (equal (xor-bvs-array current array n as) (xor-bitv current (xor-bvs (nthcdr (difference as n) (untag-array array)))))) ((induct (xor-bvs-array current array n as)) (enable nthcdr))) ;; in npiton-defs but not a supporter of p ;(PROVE-LEMMA EQUAL-LENGTH-0 ; (REWRITE) ; (EQUAL (EQUAL (LENGTH X) '0) ; (NLISTP X))) (enable equal-length-0) (prove-lemma correctness-of-xor-bvs-helper (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (append (list (tag 'nat numvecs) (tag 'addr (cons state 0))) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call xor-bvs)) (equal (definition 'xor-bvs prog-segment) (xor-bvs-program)) (xor-bvs-input-conditionp p0)) (equal (p p0 (xor-bvs-clock numvecs)) (p-state (add1-addr pc) ctrl-stk (cons (list 'bitv (xor-bvs-array (untag (car (array state data-segment))) (array state data-segment) (sub1 numvecs) numvecs)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((use (xor-bvs-loop-correctness (current (untag (car (array state data-segment)))) (s state) (n numvecs) (ret-pc (add-addr pc 1)))))) (prove-lemma length-cadar-bvs (rewrite) (implies (and (bit-vectors-piton x s) (listp x)) (equal (length (cadar x)) (fix s)))) (prove-lemma bit-vectorp-from-bit-vectors-piton (rewrite) (implies (bit-vectors-piton x s) (and (equal (bit-vectorp (cadar x) s) (listp x)) (equal (bit-vectorp (cadr (get n x)) s) (lessp n (length x)))))) (prove-lemma nthcdr-1 (rewrite) (equal (nthcdr 1 a) (cdr a)) ((enable nthcdr))) (prove-lemma listp-untag-array (rewrite) (equal (listp (untag-array x)) (listp x))) (prove-lemma xor-bvs-input-conditionp-means-xor-bvs-hack (rewrite) (implies (and (xor-bvs-input-conditionp (p-state pc ctrl-stk (cons (list 'nat numvecs) (cons (list 'addr (cons state 0)) temp-stk)) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (lessp 0 word-size)) (equal (xor-bvs-array (untag (car (array state data-segment))) (array state data-segment) (sub1 numvecs) numvecs) (xor-bvs (untag-array (array state data-segment))))) ((enable nthcdr))) (prove-lemma correctness-of-xor-bvs (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons n (cons s temp-stk)) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (lessp 0 word-size) (equal (p-current-instruction p0) '(call xor-bvs)) (equal (definition 'xor-bvs prog-segment) (xor-bvs-program)) (xor-bvs-input-conditionp p0)) (equal (p (p-state pc ctrl-stk (cons n (cons s temp-stk)) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (xor-bvs-clock (cadr n))) (p-state (add1-addr pc) ctrl-stk (cons (list 'bitv (xor-bvs (untag-array (array (caadr s) data-segment)))) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((disable xor-bvs-clock) (use (correctness-of-xor-bvs-helper (state (caadr s)) (numvecs (cadr n))) (xor-bvs-input-conditionp-means-xor-bvs-hack (state (caadr s)) (numvecs (cadr n)))))) (defn example-xor-bvs-p-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (addr (arr . 0))) (push-constant (nat 3)) (call xor-bvs) (ret)) (xor-bvs-program)) '((arr (bitv (0 1 0 1 1 0 0 1)) (bitv (0 0 0 0 0 0 0 1)) (bitv (0 1 1 0 1 0 0 1)))) 10 8 8 'run)) ;;;; push-1-vector ;; Piton currently does not provide any mechanism for creating a ;; bit vector except as an operation on other bit vectors. Until ;; this apparent flaw is fixed, we'll write our program as a ;; function of the word size. (defn one-bit-vector (wordsize) (if (lessp wordsize 2) (list 1) (cons 0 (one-bit-vector (sub1 wordsize))))) (defn push-1-vector-program (wordsize) (list 'push-1-vector nil nil (list 'push-constant (list 'bitv (one-bit-vector wordsize))) (list 'ret))) (defn example-push-1-vector-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (call push-1-vector) (ret)) (push-1-vector-program 8)) nil 10 8 8 'run)) (defn push-1-vector-input-conditionp (p0) (and (not (lessp (p-max-ctrl-stk-size p0) (plus 2 (p-ctrl-stk-size (p-ctrl-stk p0))))) (not (lessp (p-max-temp-stk-size p0) (plus 1 (length (p-temp-stk p0))))) (listp (p-ctrl-stk p0)))) ;(prove-lemma length-append (rewrite) ; (equal ; (length (append a b)) ; (plus (length a) (length b)))) (enable length-append) (prove-lemma equal-assoc-cons (rewrite) (implies (equal (assoc k a) (cons x y)) (and (equal (car (assoc k a)) x) (equal (cdr (assoc k a)) y)))) (prove-lemma correctness-of-push-1-vector (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk temp-stk prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call push-1-vector)) (equal (definition 'push-1-vector prog-segment) (push-1-vector-program word-size)) (push-1-vector-input-conditionp p0)) (equal (p p0 3) (p-state (add1-addr pc) ctrl-stk (cons (list 'bitv (one-bit-vector word-size)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)))) ;;;; nat-to-bv (defn nat-to-bv-program nil '(nat-to-bv (value) ((current-bit (nat 0)) (temp (nat 0))) (call push-1-vector) (pop-local current-bit) (call push-1-vector) (rsh-bitv) (dl loop () (push-local value)) (test-nat-and-jump zero done) (push-local value) (div2-nat) (pop-local temp) (pop-local value) (push-local temp) (test-nat-and-jump zero lab) (push-local current-bit) (xor-bitv) (dl lab () (push-local current-bit)) (lsh-bitv) (pop-local current-bit) (jump loop) (dl done () (ret)))) (defn example-nat-to-bv-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (nat 86)) (call nat-to-bv) (ret)) (push-1-vector-program 8) (nat-to-bv-program)) nil 10 8 8 'run)) (defn zero-bit-vector (size) (if (zerop size) nil (cons 0 (zero-bit-vector (sub1 size))))) (defn nat-to-bv2-helper (value current-bit bit-vector) (if (zerop value) bit-vector (nat-to-bv2-helper (quotient value 2) (append (cdr current-bit) (list 0)) (if (equal (remainder value 2) 1) (xor-bitv current-bit bit-vector) bit-vector)))) (defn nat-to-bv2 (value size) (nat-to-bv2-helper value (one-bit-vector size) (zero-bit-vector size))) (defn nat-to-bv-loop-clock (value) (if (zerop value) 3 (plus (if (equal (remainder value 2) 0) 12 14) (nat-to-bv-loop-clock (quotient value 2))))) (defn correctness-of-nat-to-bv-general-induct (value cb temp bv) (if (zerop value) t (correctness-of-nat-to-bv-general-induct (quotient value 2) (append (cdr cb) (list 0)) (list 'nat (remainder value 2)) (if (equal (remainder value 2) 0) bv (xor-bitv bv cb))))) (prove-lemma lessp-remainder-simple (rewrite) (implies (not (zerop y)) (lessp (remainder x y) y))) (prove-lemma lessp-exp-simple (rewrite) (implies (and (lessp x y) (not (zerop z))) (lessp x (exp y z))) ((enable exp))) (prove-lemma lessp-1 (rewrite) (equal (lessp x 1) (zerop x))) (prove-lemma lessp-remainder-x-exp-x (rewrite) (equal (lessp (remainder x y) (exp y z)) (or (and (zerop z) (equal (remainder x y) 0)) (and (not (zerop z)) (not (zerop y))))) ((enable exp))) (prove-lemma bit-vectorp-append (rewrite) (implies (bit-vectorp x x-size) (equal (bit-vectorp (append x y) size) (and (bit-vectorp y (difference size x-size)) (not (lessp size x-size)))))) (prove-lemma correctness-of-nat-to-bv-general (rewrite) (implies (and (listp ctrl-stk) (at-least-morep (length temp-stk) 3 max-temp-stk-size) (equal (definition 'nat-to-bv prog-segment) (nat-to-bv-program)) (numberp value) (lessp 0 word-size) (lessp value (exp 2 word-size)) (bit-vectorp bv word-size) (bit-vectorp cb word-size)) (equal (p (p-state '(pc (nat-to-bv . 4)) (cons (list (list (cons 'value (list 'nat value)) (cons 'current-bit (list 'bitv cb)) (cons 'temp temp)) ret-pc) ctrl-stk) (cons (list 'bitv bv) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (nat-to-bv-loop-clock value)) (p-state ret-pc ctrl-stk (cons (list 'bitv (nat-to-bv2-helper value cb bv)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((induct (correctness-of-nat-to-bv-general-induct value cb temp bv)))) (defn nat-to-bv-clock (value) (plus 9 (nat-to-bv-loop-clock value))) (defn nat-to-bv-input-conditionp (p0) (and (lessp (cadr (top (p-temp-stk p0))) (exp 2 (p-word-size p0))) (numberp (cadr (top (p-temp-stk p0)))) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 7 (p-max-ctrl-stk-size p0)) (lessp 0 (p-word-size p0)) (at-least-morep (length (p-temp-stk p0)) 2 (p-max-temp-stk-size p0)) (listp (p-ctrl-stk p0)))) (prove-lemma bit-vectorp-one-bit-vector (rewrite) (equal (bit-vectorp (one-bit-vector s) s) (lessp 0 s))) (prove-lemma bit-vectorp-zero-bit-vector (rewrite) (bit-vectorp (zero-bit-vector s) s)) (prove-lemma all-but-last-one-bit-vector (rewrite) (equal (all-but-last (one-bit-vector s)) (zero-bit-vector (sub1 s)))) (prove-lemma correctness-of-nat-to-bv-helper nil (implies (and (equal p0 (p-state pc ctrl-stk (cons (list 'nat value) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call nat-to-bv)) (equal (definition 'nat-to-bv prog-segment) (nat-to-bv-program)) (equal (definition 'push-1-vector prog-segment) (push-1-vector-program word-size)) (nat-to-bv-input-conditionp p0)) (equal (p p0 (nat-to-bv-clock value)) (p-state (add1-addr pc) ctrl-stk (cons (list 'bitv (nat-to-bv2 value word-size)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)))) (defn bv-to-nat (bv) (if (listp bv) (plus (times (fix-bit (car bv)) (exp 2 (length (cdr bv)))) (bv-to-nat (cdr bv))) 0)) (prove-lemma length-nat-to-bv (rewrite) (equal (length (nat-to-bv nat size)) (fix size))) (prove-lemma bv-to-nat-nat-to-bv (rewrite) (equal (bv-to-nat (nat-to-bv nat size)) (if (lessp nat (exp 2 size)) (fix nat) (sub1 (exp 2 size)))) ((enable exp))) (enable exp) (prove-lemma nat-to-bv-simple (rewrite) (implies (zerop x) (and (equal (nat-to-bv x y) (zero-bit-vector y)) (equal (nat-to-bv y x) nil)))) (prove-lemma nat-to-bv-bv-to-nat (rewrite) (implies (bit-vectorp bv size) (equal (nat-to-bv (bv-to-nat bv) size) bv))) (prove-lemma bv-to-nat-append (rewrite) (equal (bv-to-nat (append x y)) (plus (bv-to-nat y) (times (exp 2 (length y)) (bv-to-nat x))))) (prove-lemma lessp-plus-hacks (rewrite) (and (equal (lessp (plus a (plus b (plus c (plus (times d e) (times d e))))) (plus e e)) (and (zerop d) (lessp (plus a (plus b c)) (plus e e)))) (equal (lessp (plus a (plus b (plus c (plus e (plus (times d g) h))))) g) (and (zerop d) (lessp (plus a (plus b (plus c (plus e h)))) g))))) (prove-lemma bv-to-nat-xor-bitv (rewrite) (implies (and (bit-vectorp x size) (bit-vectorp y size) (equal (and-bitv x y) (zero-bit-vector size))) (equal (bv-to-nat (xor-bitv x y)) (plus (bv-to-nat x) (bv-to-nat y))))) (prove-lemma lessp-bv-to-nat-exp-2 (rewrite) (implies (bit-vectorp x size) (equal (lessp (bv-to-nat x) (exp 2 size)) t))) (prove-lemma equal-nat-to-bv (rewrite) (implies (and (bit-vectorp bv size) (lessp y (exp 2 size))) (and (equal (equal (nat-to-bv y size) bv) (equal (bv-to-nat bv) (fix y))) (equal (equal bv (nat-to-bv y size)) (equal (fix y) (bv-to-nat bv)))))) (defn least-bit-higher-than-high-bit (x y) (if (listp x) (and (equal (length x) (length y)) (if (not (equal (car y) 0)) (all-zero-bitvp x) (least-bit-higher-than-high-bit (cdr x) (cdr y)))) (nlistp y))) (prove-lemma least-bit-higher-means-and-0 (rewrite) (implies (and (bit-vectorp x size) (bit-vectorp y size) (least-bit-higher-than-high-bit x y)) (and (equal (and-bitv x y) (zero-bit-vector size)) (equal (and-bitv y x) (zero-bit-vector size))))) (prove-lemma all-zero-bitvp-zero-bit-vector (rewrite) (all-zero-bitvp (zero-bit-vector size))) (prove-lemma bv-to-nat-one-bit-vector (rewrite) (equal (bv-to-nat (one-bit-vector size)) 1)) ;; renamed from firstn to avoid conflict with similar but different ;; definition in piton library (defn make-list-from (n list) (if (zerop n) nil (cons (car list) (make-list-from (sub1 n) (cdr list))))) (prove-lemma length-make-list-from (rewrite) (equal (length (make-list-from n list)) (fix n))) (prove-lemma make-list-from-1 (rewrite) (equal (make-list-from 1 x) (list (car x)))) (prove-lemma listp-make-list-from (rewrite) (equal (listp (make-list-from n x)) (not (zerop n)))) (defn double-cdr-induct (x z) (if (listp x) (double-cdr-induct (cdr x) (cdr z)) t)) (prove-lemma all-zero-bitvp-append (rewrite) (equal (all-zero-bitvp (append x y)) (and (all-zero-bitvp x) (all-zero-bitvp y)))) (prove-lemma least-bit-higher-than-high-bit-append-0s (rewrite) (implies (and (all-zero-bitvp y) (equal (length z) (length (append x y)))) (equal (least-bit-higher-than-high-bit (append x y) z) (least-bit-higher-than-high-bit x (make-list-from (length x) z)))) ((induct (double-cdr-induct x z)))) (prove-lemma equal-xor-bitv-x-y-1 (rewrite) (equal (equal (xor-bitv a b) b) (and (bit-vectorp b (length a)) (all-zero-bitvp a)))) (prove-lemma equal-xor-bitv-x-y-2 (rewrite) (equal (equal (xor-bitv a b) a) (and (all-zero-bitvp (make-list-from (length a) b)) (bit-vectorp a (length a))))) (prove-lemma least-bit-higher-than-high-bit-simple (rewrite) (implies (all-zero-bitvp x) (equal (least-bit-higher-than-high-bit x y) (equal (length x) (length y))))) (prove-lemma make-list-from-is-all-but-last (rewrite) (implies (equal (length x) (add1 n)) (equal (make-list-from n x) (all-but-last x)))) (prove-lemma least-bit-higher-all-but-last (rewrite) (implies (least-bit-higher-than-high-bit a b) (equal (least-bit-higher-than-high-bit a (cons 0 (all-but-last b))) (listp a)))) (defn at-most-one-bit-on (bv) (if (listp bv) (if (equal (car bv) 0) (at-most-one-bit-on (cdr bv)) (all-zero-bitvp (cdr bv))) t)) ; ;(prove-lemma length-all-but-last (rewrite) ; (equal ; (length (all-but-last x)) ; (if (listp x) (sub1 (length x)) 0))) (enable length-all-but-last) (prove-lemma listp-xor-bitv (rewrite) (equal (listp (xor-bitv a b)) (listp a))) (prove-lemma all-zero-bitvp-means-at-most-one-bit-on (rewrite) (implies (all-zero-bitvp x) (at-most-one-bit-on x))) (prove-lemma at-most-one-bit-on-append (rewrite) (equal (at-most-one-bit-on (append a b)) (or (and (all-zero-bitvp a) (at-most-one-bit-on b)) (and (at-most-one-bit-on a) (all-zero-bitvp b))))) (defn fix-bitv (list) (if (listp list) (cons (if (equal (car list) 0) 0 1) (fix-bitv (cdr list))) nil)) (prove-lemma xor-bitv-nlistp3 (rewrite) (implies (not (listp x)) (and (equal (xor-bitv x y) nil) (equal (xor-bitv y x) (fix-bitv y))))) (disable xor-bitv-nlistp) (disable xor-bitv-nlistp2) (prove-lemma fix-bitv-all-but-last (rewrite) (equal (fix-bitv (all-but-last x)) (all-but-last (fix-bitv x)))) (prove-lemma all-but-last-xor-bitv (rewrite) (equal (all-but-last (xor-bitv a b)) (if (lessp (length b) (length a)) (xor-bitv (all-but-last a) b) (xor-bitv (all-but-last a) (all-but-last b))))) (prove-lemma least-bit-higher-cons-xor-bitv-hack (rewrite) (implies (and (least-bit-higher-than-high-bit (cdr x) a) (least-bit-higher-than-high-bit (cdr x) b)) (equal (least-bit-higher-than-high-bit x (cons 0 (xor-bitv a b))) (listp x)))) (prove-lemma least-bit-higher-cdr-all-but-last (rewrite) (implies (least-bit-higher-than-high-bit a b) (least-bit-higher-than-high-bit (cdr a) (all-but-last b)))) (prove-lemma least-bit-higher-x-all-but-last-x (rewrite) (implies (at-most-one-bit-on x) (least-bit-higher-than-high-bit (cdr x) (all-but-last x)))) (prove-lemma nat-to-bv-equiv-helper nil (implies (and (bit-vectorp cb size) (bit-vectorp bv size) (lessp 0 size) (lessp (plus (bv-to-nat bv) (times (bv-to-nat cb) value)) (exp 2 size)) (at-most-one-bit-on cb) (least-bit-higher-than-high-bit cb bv)) (equal (nat-to-bv2-helper value cb bv) (nat-to-bv (plus (times (bv-to-nat cb) value) (bv-to-nat bv)) size))) ((induct (nat-to-bv2-helper value cb bv)))) (prove-lemma at-most-one-bit-on-one-bit-vector (rewrite) (at-most-one-bit-on (one-bit-vector size))) (prove-lemma bv-to-nat-all-zero-bitvp (rewrite) (implies (all-zero-bitvp x) (equal (bv-to-nat x) 0))) (prove-lemma least-bit-higher-than-high-bit-simple2 (rewrite) (implies (all-zero-bitvp x) (equal (least-bit-higher-than-high-bit y x) (equal (length x) (length y))))) (prove-lemma length-zero-bit-vector (rewrite) (equal (length (zero-bit-vector size)) (fix size))) (prove-lemma length-one-bit-vector (rewrite) (equal (length (one-bit-vector size)) (if (zerop size) 1 size))) (prove-lemma nat-to-bv-equivalence (rewrite) (implies (and (lessp value (exp 2 size)) (lessp 0 size)) (equal (nat-to-bv2 value size) (nat-to-bv value size))) ((use (nat-to-bv-equiv-helper (cb (one-bit-vector size)) (bv (zero-bit-vector size)))))) (prove-lemma correctness-of-nat-to-bv (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons v temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (car v) 'nat) (equal (cddr v) nil) (equal (p-current-instruction p0) '(call nat-to-bv)) (equal (definition 'nat-to-bv prog-segment) (nat-to-bv-program)) (equal (definition 'push-1-vector prog-segment) (push-1-vector-program word-size)) (equal num (cadr v)) (nat-to-bv-input-conditionp p0)) (equal (p (p-state pc ctrl-stk (cons v temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (nat-to-bv-clock num)) (p-state (add1-addr pc) ctrl-stk (cons (list 'bitv (nat-to-bv (cadr v) word-size)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((disable-theory t) (enable nat-to-bv-input-conditionp p-state p-word-size-p-state p-temp-stk-p-state top) (enable-theory ground-zero) (use (correctness-of-nat-to-bv-helper (value (cadr v))) (nat-to-bv-equivalence (size word-size) (value (cadr v)))))) ;;;; bv-to-nat (defn bv-to-nat-program nil '(bv-to-nat (bv) ((current-bit (nat 0)) (current-2power (nat 0))) (push-constant (nat 1)) (pop-local current-2power) (call push-1-vector) (pop-local current-bit) (push-constant (nat 0)) (dl loop () (push-local bv)) (push-local current-bit) (and-bitv) (test-bitv-and-jump all-zero lab) (push-local current-2power) (add-nat) (dl lab () (push-local current-bit)) (lsh-bitv) (set-local current-bit) (test-bitv-and-jump all-zero done) (push-local current-2power) (mult2-nat) (pop-local current-2power) (jump loop) (dl done () (ret)))) (defn example-bv-to-nat-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (bitv (1 0 1 1 0 0 0 1))) (call bv-to-nat) (ret)) (push-1-vector-program 8) (bv-to-nat-program)) nil 10 8 8 'run)) (defn trailing-zeros-helper (list acc) (if (listp list) (trailing-zeros-helper (cdr list) (if (equal (car list) 0) (add1 acc) 0)) (fix acc))) (defn trailing-zeros (list) (trailing-zeros-helper list 0)) (prove-lemma trailing-zeros-of-all-zero-bitvp (rewrite) (implies (all-zero-bitvp bv) (equal (trailing-zeros-helper bv n) (plus (length bv) n)))) (prove-lemma non-zero-means-acc-irrelevant-spec (rewrite) (implies (not (all-zero-bitvp bv)) (equal (trailing-zeros-helper bv (add1 x)) (trailing-zeros-helper bv x)))) (prove-lemma non-zero-means-acc-irrelevant (rewrite) (implies (and (not (all-zero-bitvp bv)) (not (equal x 0))) (equal (trailing-zeros-helper bv x) (trailing-zeros-helper bv 0)))) (prove-lemma trailing-zeros-helper-append (rewrite) (equal (trailing-zeros-helper (append x y) acc) (if (all-zero-bitvp y) (plus (trailing-zeros-helper x acc) (length y)) (trailing-zeros-helper y acc)))) (prove-lemma trailing-zeros-append (rewrite) (equal (trailing-zeros (append x y)) (if (all-zero-bitvp y) (plus (trailing-zeros x) (length y)) (trailing-zeros y)))) (prove-lemma lessp-trailing-zeros-helper (rewrite) (implies (not (lessp n (plus acc (length x)))) (equal (lessp n (trailing-zeros-helper x acc)) f))) (defn last (list) (if (listp list) (if (listp (cdr list)) (last (cdr list)) (car list)) 0)) (prove-lemma equal-trailing-zeros-helper-0 (rewrite) (equal (equal (trailing-zeros-helper x acc) 0) (or (and (zerop acc) (nlistp x)) (not (equal (last x) 0))))) (prove-lemma lessp-length-cdr-trailing (rewrite) (implies (and (lessp (length (cdr x)) (trailing-zeros-helper x acc)) (listp x)) (and (all-zero-bitvp x) (all-zero-bitvp (cdr x))))) (prove-lemma not-all-zero-bitvp-cdr-means (rewrite) (implies (not (all-zero-bitvp (cdr x))) (equal (trailing-zeros-helper x acc) (trailing-zeros-helper (cdr x) 0)))) (defn bv-to-nat2-helper (bv cb current-2power) (if (all-zero-bitvp cb) 0 (plus (if (all-zero-bitvp (and-bitv bv cb)) 0 current-2power) (bv-to-nat2-helper bv (append (cdr cb) (list 0)) (times 2 current-2power)))) ((lessp (difference (length cb) (trailing-zeros cb))))) (defn bv-to-nat2 (bv) (bv-to-nat2-helper bv (one-bit-vector (length bv)) 1)) (prove-lemma lessp-length-trailing-zeros-hack (rewrite) (implies (zerop acc) (not (lessp (length x) (trailing-zeros-helper x acc))))) (defn bv-to-nat-loop-clock (cb bv) (if (all-zero-bitvp (cdr cb)) (if (or (equal (car cb) 0) (equal (car bv) 0)) 9 11) (plus (if (all-zero-bitvp (and-bitv cb bv)) 12 14) (bv-to-nat-loop-clock (append (cdr cb) '(0)) bv))) ((lessp (difference (length cb) (trailing-zeros cb))))) (defn bv-to-nat-induct (value bv cb current-2power) (if (all-zero-bitvp cb) 0 (bv-to-nat-induct (plus (if (all-zero-bitvp (and-bitv bv cb)) 0 current-2power) value) bv (append (cdr cb) (list 0)) (times 2 current-2power))) ((lessp (difference (length cb) (trailing-zeros cb))))) (defn double-cdr-with-sub1-induct (x y n) (if (listp x) (double-cdr-with-sub1-induct (cdr x) (cdr y) (sub1 n)) t)) (prove-lemma bit-vectorp-and-bitv-better (rewrite) (equal (bit-vectorp (and-bitv x y) size) (equal (length x) (fix size))) ((induct (double-cdr-with-sub1-induct x y size)))) (prove-lemma lessp-bv-to-nat-exp (rewrite) (implies (bit-vectorp x size) (lessp (bv-to-nat x) (exp 2 size)))) (prove-lemma equal-bv-to-nat-0 (rewrite) (implies (bit-vectorp x size) (equal (equal (bv-to-nat x) 0) (all-zero-bitvp x)))) ;(prove-lemma commutativity-of-and-bitv (rewrite) ; (implies ; (equal (length x) (length y)) ; (equal (and-bitv x y) (and-bitv y x)))) (enable commutativity-of-and-bitv) (prove-lemma commutativity2-of-and-bitv (rewrite) (implies (equal (length x) (length y)) (equal (and-bitv x (and-bitv y z)) (and-bitv y (and-bitv x z))))) (prove-lemma associativity-of-and-bitv (rewrite) (implies (equal (length x) (length y)) (equal (and-bitv (and-bitv x y) z) (and-bitv x (and-bitv y z))))) (prove-lemma all-zero-bitvp-and-bitv (rewrite) (implies (all-zero-bitvp x) (and (all-zero-bitvp (and-bitv x y)) (all-zero-bitvp (and-bitv y x))))) (prove-lemma bv-to-nat-loop-clock-open (rewrite) (implies (all-zero-bitvp x) (equal (bv-to-nat-loop-clock x y) 9))) (prove-lemma bv-to-nat2-helper-hack (rewrite) (implies (and (all-zero-bitvp z) (equal (length d) (length z))) (equal (bv-to-nat2-helper (cons 1 d) (cons 1 z) v) (fix v))) ((expand (bv-to-nat2-helper (cons 1 d) (cons 1 z) v)))) (prove-lemma bv-to-nat2-helper-hack2 (rewrite) (implies (and (all-zero-bitvp z) (equal (length d) (length z))) (equal (bv-to-nat2-helper (cons 0 d) (cons 1 z) v) 0)) ((expand (bv-to-nat2-helper (cons 0 d) (cons 1 z) v)))) (prove-lemma correctness-of-bv-to-nat-general (rewrite) (implies (and (listp ctrl-stk) (at-least-morep (length temp-stk) 3 max-temp-stk-size) (equal (definition 'bv-to-nat prog-segment) (bv-to-nat-program)) (numberp c2p) (lessp 0 word-size) (at-most-one-bit-on cb) (equal c2p (bv-to-nat cb)) (bit-vectorp bv word-size) (bit-vectorp cb word-size) (numberp value) (lessp value c2p)) (equal (p (p-state '(pc (bv-to-nat . 5)) (cons (list (list (cons 'bv (list 'bitv bv)) (cons 'current-bit (list 'bitv cb)) (cons 'current-2power (list 'nat c2p))) ret-pc) ctrl-stk) (cons (list 'nat value) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (bv-to-nat-loop-clock cb bv)) (p-state ret-pc ctrl-stk (cons (list 'nat (plus (bv-to-nat2-helper bv cb c2p) value)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((induct (bv-to-nat-induct value bv cb c2p)))) (defn bv-to-nat-clock (word-size bv) (plus 8 (bv-to-nat-loop-clock (one-bit-vector word-size) bv))) (defn bv-to-nat-input-conditionp (p0) (and (equal (car (top (p-temp-stk p0))) 'bitv) (equal (cddr (top (p-temp-stk p0))) nil) (bit-vectorp (cadr (top (p-temp-stk p0))) (p-word-size p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 7 (p-max-ctrl-stk-size p0)) (lessp 0 (p-word-size p0)) (at-least-morep (length (p-temp-stk p0)) 2 (p-max-temp-stk-size p0)) (listp (p-ctrl-stk p0)))) (prove-lemma correctness-of-bv-to-nat-helper nil (implies (and (equal p0 (p-state pc ctrl-stk (cons (list 'bitv bv) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call bv-to-nat)) (equal (definition 'bv-to-nat prog-segment) (bv-to-nat-program)) (equal (definition 'push-1-vector prog-segment) (push-1-vector-program word-size)) (bv-to-nat-input-conditionp p0)) (equal (p p0 (bv-to-nat-clock word-size bv)) (p-state (add1-addr pc) ctrl-stk (cons (list 'nat (bv-to-nat2 bv)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)))) (prove-lemma bit-vectorp-append-better (rewrite) (implies (bit-vectorp x (length x)) (equal (bit-vectorp (append x y) size) (and (bit-vectorp y (length y)) (equal (fix size) (plus (length x) (length y)))))) ((induct (make-list-from size x)))) (prove-lemma bit-vectorp-hack (rewrite) (equal (bit-vectorp x (plus a (length (cdr x)))) (and (if (listp x) (equal a 1) (zerop a)) (bit-vectorp x (length x)))) ((use (length-from-bit-vectorp (x x) (s (plus a (length (cdr x)))))) (disable length-from-bit-vectorp))) (prove-lemma bv-to-nat-one-bit (rewrite) (implies (and (not (all-zero-bitvp x)) (at-most-one-bit-on x) (bit-vectorp x size)) (equal (bv-to-nat x) (exp 2 (trailing-zeros x))))) (prove-lemma lessp-sub1-plus-hack (rewrite) (equal (lessp (sub1 x) (plus y x)) (or (not (zerop x)) (not (zerop y))))) (prove-lemma quotient-plus-hack (rewrite) (equal (quotient (plus a b b) 2) (plus (quotient a 2) b))) (prove-lemma bv-to-nat-all-but-last (rewrite) (implies (bit-vectorp x size) (equal (bv-to-nat (all-but-last x)) (quotient (bv-to-nat x) 2)))) (prove-lemma make-list-from-cons (rewrite) (equal (make-list-from n (cons a b)) (if (zerop n) nil (cons a (make-list-from (sub1 n) b))))) (prove-lemma equal-plus-times-hack (rewrite) (equal (equal (plus a (times a b) (times a c)) (times a d)) (or (zerop a) (equal (plus 1 b c) d))) ((use (equal-times-arg1 (a a) (x (plus 1 b c)) (y d))))) ;(defn nth (n list) ; (if (zerop n) ; (car list) ; (nth (sub1 n) (cdr list)))) (enable nth) (prove-lemma last-make-list-from (rewrite) (equal (last (make-list-from n x)) (if (zerop n) 0 (nth (sub1 n) x)))) (prove-lemma make-list-from-nlistp (rewrite) (implies (nlistp x) (equal (make-list-from n x) (zero-bit-vector n)))) (prove-lemma nth-nlistp (rewrite) (implies (nlistp x) (equal (nth n x) 0))) (prove-lemma bit-vectorp-make-list-from (rewrite) (implies (bit-vectorp x size) (bit-vectorp (make-list-from n x) n))) (prove-lemma equal-bv-to-nat-0-2 (rewrite) (implies (bit-vectorp x (length x)) (equal (equal (bv-to-nat x) 0) (all-zero-bitvp x)))) (prove-lemma bv-to-nat-make-list-from-from-sub1-make-list-from (rewrite) (implies (equal (bv-to-nat (make-list-from (sub1 n) v)) 0) (equal (bv-to-nat (make-list-from n v)) (if (zerop n) 0 (fix-bit (nth (sub1 n) v)))))) (prove-lemma plus-bv-to-nat-make-list-from (rewrite) (equal (plus (bv-to-nat (make-list-from (sub1 z) v)) (bv-to-nat (make-list-from (sub1 z) v))) (difference (bv-to-nat (make-list-from z v)) (fix-bit (last (make-list-from z v))))) ((induct (make-list-from z v)))) (prove-lemma equal-bv-to-nat-1 (rewrite) (implies (bit-vectorp x (length x)) (equal (equal (bv-to-nat x) 1) (and (all-zero-bitvp (all-but-last x)) (equal (last x) 1)))) ((induct (all-but-last x)))) (prove-lemma lessp-1-hack (rewrite) (equal (lessp 1 a) (and (not (zerop a)) (not (equal a 1))))) (prove-lemma not-equal-nth-0-means (rewrite) (implies (and (not (equal (nth n v) 0)) (lessp n s)) (not (all-zero-bitvp (make-list-from s v))))) (prove-lemma all-zero-bitvp-all-but-last-means nil (implies (and (all-zero-bitvp (all-but-last x)) (equal (length x) (length y)) (lessp 0 (trailing-zeros-helper y acc))) (all-zero-bitvp (and-bitv x y)))) (prove-lemma all-zero-bitvp-all-but-last-means-spec (rewrite) (implies (and (all-zero-bitvp (all-but-last x)) (equal (length x) (length y)) (lessp 0 (trailing-zeros-helper y 0))) (all-zero-bitvp (and-bitv x y))) ((use (all-zero-bitvp-all-but-last-means (acc 0))))) (prove-lemma all-zero-means-to-and-bitv (rewrite) (implies (all-zero-bitvp x) (and (equal (and-bitv x y) (zero-bit-vector (length x))) (equal (and-bitv y x) (zero-bit-vector (length y)))))) (prove-lemma trailing-zeros-nth-proof nil (implies (and (equal n (sub1 (difference (length x) (trailing-zeros-helper x acc)))) (not (all-zero-bitvp x))) (not (equal (nth n x) 0)))) (prove-lemma trailing-zeros-nth-spec (rewrite) (implies (and (equal n (sub1 (difference (length x) (trailing-zeros-helper x 0)))) (not (all-zero-bitvp x))) (not (equal (nth n x) 0))) ((use (trailing-zeros-nth-proof (acc 0))))) (prove-lemma and-bitv-special (rewrite) (implies (and (equal (nth n w) 0) (not (equal (nth n x) 0)) (equal (length x) (length x)) (at-most-one-bit-on x)) (equal (and-bitv w x) (zero-bit-vector (length w))))) (prove-lemma equal-trailing-zeros-length-spec nil (equal (equal (trailing-zeros-helper x acc) (plus acc (length x))) (all-zero-bitvp x))) (prove-lemma equal-trailing-zeros-length (rewrite) (implies (zerop acc) (equal (equal (trailing-zeros-helper x acc) (length x)) (all-zero-bitvp x))) ((use (equal-trailing-zeros-length-spec)))) (prove-lemma bit-vectorp-trailing-zeros (rewrite) (equal (bit-vectorp x (trailing-zeros-helper x acc)) (and (all-zero-bitvp x) (bit-vectorp x (length x)) (zerop acc))) ((use (equal-trailing-zeros-length-spec) (length-from-bit-vectorp (s (trailing-zeros-helper x acc)))) (disable length-from-bit-vectorp))) (prove-lemma quotient-exp-hack (rewrite) (implies (not (zerop b)) (equal (quotient (plus x (exp b y)) b) (if (zerop y) (quotient (add1 x) b) (plus (exp b (sub1 y)) (quotient x b)))))) ;(defn properp (list) ; (if (listp list) ; (properp (cdr list)) ; (equal list nil))) (prove-lemma bit-vectorp-means-properp (rewrite) (implies (bit-vectorp x (length x)) (properp x))) (prove-lemma make-list-from-simplify (rewrite) (implies (and (equal n (length x)) (properp x)) (equal (make-list-from n x) x))) (prove-lemma equal-add1-plus-hack (rewrite) (and (equal (equal (add1 (plus a b)) (plus c (plus d a))) (equal (add1 b) (plus c d))) (equal (equal (add1 (plus a b)) (plus c a)) (equal (add1 b) (fix c))) (equal (equal (add1 a) (plus b a)) (equal 1 (fix b))))) (prove-lemma plus-quotient-bv-to-nat (rewrite) (equal (plus (quotient (bv-to-nat x) 2) (quotient (bv-to-nat x) 2)) (difference (bv-to-nat x) (fix-bit (last x))))) (prove-lemma equal-plus-times-hack2 (rewrite) (equal (equal (plus (times a b) (times a c)) (times a d)) (or (zerop a) (equal (plus b c) (fix d)))) ((use (equal-times-arg1 (a a) (x (plus b c)) (y d))))) (prove-lemma and-bitv-special-special (rewrite) (implies (and (equal (last w) 0) (not (equal (last x) 0)) (equal (length x) (length w)) (at-most-one-bit-on x)) (equal (and-bitv w x) (zero-bit-vector (length w))))) (prove-lemma and-bitv-special-3 (rewrite) (implies (and (equal (length x) (length y)) (not (equal (last x) 0)) (not (equal (last y) 0))) (not (all-zero-bitvp (and-bitv x y))))) (prove-lemma and-bitv-special-4 (rewrite) (implies (and (not (equal (nth n w) 0)) (not (equal (nth n x) 0)) (equal (length x) (length x))) (not (all-zero-bitvp (and-bitv w x))))) (prove-lemma and-bitv-special-5 (rewrite) (implies (and (equal (last w) 0) (not (equal (last x) 0)) (equal (add1 (length x)) (length w)) (at-most-one-bit-on x)) (equal (and-bitv w (cons 0 x)) (zero-bit-vector (length w))))) (prove-lemma and-bitv-special-6 (rewrite) (implies (and (not (equal (last w) 0)) (not (equal (last x) 0)) (equal (add1 (length x)) (length w))) (not (all-zero-bitvp (and-bitv w (cons 0 x)))))) (prove-lemma not-last-0-means-not-all-0 (rewrite) (implies (not (equal (last x) 0)) (not (all-zero-bitvp x)))) (prove-lemma bit-vectorp-plus-length-hack (rewrite) (and (equal (bit-vectorp x (plus z (length x))) (and (bit-vectorp x (length x)) (zerop z))) (equal (bit-vectorp x (plus (add1 z) (length (cdr x)))) (and (bit-vectorp x (length x)) (listp x) (zerop z))))) (prove-lemma last-append (rewrite) (equal (last (append x y)) (if (listp y) (last y) (last x)))) (prove-lemma bv-to-nat2-helper-bv-to-nat (rewrite) (implies (and (at-most-one-bit-on cb) (bit-vectorp cb size) (bit-vectorp bv size) (equal c2 (bv-to-nat cb))) (equal (bv-to-nat2-helper bv cb c2) (bv-to-nat (append (make-list-from (difference (length bv) (trailing-zeros cb)) bv) (zero-bit-vector (trailing-zeros cb))))))) (prove-lemma bv-to-nat2-helper-bv-to-nat-better (rewrite) (implies (and (at-most-one-bit-on cb) (bit-vectorp cb (length cb)) (bit-vectorp bv (length cb)) (equal c2 (bv-to-nat cb))) (equal (bv-to-nat2-helper bv cb c2) (bv-to-nat (append (make-list-from (difference (length bv) (trailing-zeros cb)) bv) (zero-bit-vector (trailing-zeros cb))))))) (prove-lemma nlistp-bv-to-nat2 (rewrite) (implies (not (listp x)) (equal (bv-to-nat2-helper x a b) 0))) (prove-lemma bv-to-nat2-bv-to-nat-helper nil (implies (nlistp x) (equal (bv-to-nat2 x) (bv-to-nat x)))) (prove-lemma bit-vectorp-one-bit-vector-rewrite (rewrite) (equal (bit-vectorp (one-bit-vector s) n) (if (zerop s) (equal n 1) (equal (fix s) (fix n)))) ((induct (lessp s n)))) (prove-lemma trailing-zeros-helper-one-bit-vector (rewrite) (equal (trailing-zeros-helper (one-bit-vector n) acc) 0)) (prove-lemma bv-to-nat2-bv-to-nat (rewrite) (implies (bit-vectorp x (length x)) (equal (bv-to-nat2 x) (bv-to-nat x))) ((use (bv-to-nat2-bv-to-nat-helper)))) (prove-lemma bv-length-weaker (rewrite) (implies (bit-vectorp x s) (bit-vectorp x (length x)))) (prove-lemma correctness-of-bv-to-nat (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons b temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call bv-to-nat)) (equal (definition 'bv-to-nat prog-segment) (bv-to-nat-program)) (equal (definition 'push-1-vector prog-segment) (push-1-vector-program word-size)) (equal bv (cadr b)) (bv-to-nat-input-conditionp p0)) (equal (p (p-state pc ctrl-stk (cons b temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (bv-to-nat-clock word-size bv)) (p-state (add1-addr pc) ctrl-stk (cons (list 'nat (bv-to-nat bv)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((use (correctness-of-bv-to-nat-helper) (bv-to-nat2-bv-to-nat (x bv))) (disable-theory t) (enable bv-to-nat-input-conditionp p-state p-word-size-p-state bv-length-weaker top p-temp-stk-p-state) (enable-theory ground-zero))) ;;;; number-with-at-least (defn number-with-at-least-program nil '(number-with-at-least (nums-addr numnums min) ((i (nat 0))) (push-constant (nat 0)) (set-local i) (dl loop () (push-local nums-addr)) (fetch) (push-local min) (lt-nat) (test-bool-and-jump t lab) (add1-nat) (dl lab () (push-local numnums)) (push-local i) (add1-nat) (set-local i) (sub-nat) (test-nat-and-jump zero done) (push-local nums-addr) (push-constant (nat 1)) (add-addr) (pop-local nums-addr) (jump loop) (dl done () (ret)))) (defn example-number-with-at-least-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (addr (nums . 0))) (push-constant (nat 5)) (push-constant (nat 3)) (call number-with-at-least) (ret)) (number-with-at-least-program)) '((nums (nat 3) (nat 8) (nat 9) (nat 2) (nat 100))) 10 8 8 'run)) (defn number-with-at-least (numlist min) (if (listp numlist) (if (lessp (car numlist) min) (number-with-at-least (cdr numlist) min) (add1 (number-with-at-least (cdr numlist) min))) 0)) (defn nat-list-piton (array word-size) (if (listp array) (and (listp (car array)) (equal (caar array) 'nat) (numberp (cadar array)) (equal (cddar array) nil) (lessp (cadar array) (exp 2 word-size)) (nat-list-piton (cdr array) word-size)) (equal array nil))) (defn number-with-at-least-general-induct (i current n s min data-segment) (if (lessp i n) (number-with-at-least-general-induct (add1 i) (if (lessp (cadr (get i (array s data-segment))) min) current (add1 current)) n s min data-segment) t) ((lessp (difference n i)))) (defn number-with-at-least-clock-loop (i min array) (if (not (lessp i (length array))) 0 (plus (if (lessp (cadr (get i array)) min) 0 1) (if (equal (add1 i) (length array)) 12 (plus 16 (number-with-at-least-clock-loop (add1 i) min array))))) ((lessp (difference (length array) i)))) (prove-lemma equal-difference-1 (rewrite) (equal (equal (difference x y) 1) (equal x (add1 y)))) (prove-lemma nat-list-piton-means (rewrite) (implies (and (nat-list-piton state size) (lessp p (length state))) (and (equal (car (get p state)) 'nat) (listp (get p state)) (numberp (cadr (get p state))) (lessp (cadr (get p state)) (exp 2 size)) (equal (cddr (get p state)) nil)))) (prove-lemma number-with-at-least-nlistp (rewrite) (implies (not (listp x)) (equal (number-with-at-least x min) 0))) (prove-lemma equal-add1-length (rewrite) (equal (equal (add1 x) (length y)) (and (listp y) (equal (fix x) (length (cdr y)))))) (disable number-with-at-least-clock-loop) (prove-lemma length-cdr-untag-array (rewrite) (equal (length (cdr (untag-array x))) (length (cdr x)))) (prove-lemma number-with-at-least-correctness-general nil (implies (and (lessp (length (array s data-segment)) (exp 2 word-size)) (not (zerop word-size)) (listp ctrl-stk) (nat-list-piton (array s data-segment) word-size) (at-least-morep (length temp-stk) 3 max-temp-stk-size) (equal (definition 'number-with-at-least prog-segment) (number-with-at-least-program)) (definedp s data-segment) (lessp min (exp 2 word-size)) (numberp min) (lessp i n) (numberp i) (lessp n (exp 2 word-size)) (numberp current) (not (lessp i current)) (equal n (length (array s data-segment)))) (equal (p (p-state '(pc (number-with-at-least . 2)) (cons (list (list (cons 'nums-addr (list 'addr (cons s i))) (cons 'numnums (list 'nat n)) (cons 'min (list 'nat min)) (cons 'i (list 'nat i))) ret-pc) ctrl-stk) (cons (list 'nat current) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (number-with-at-least-clock-loop i min (array s data-segment))) (p-state ret-pc ctrl-stk (cons (list 'nat (plus current (number-with-at-least (nthcdr i (untag-array (array s data-segment))) min))) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((induct (number-with-at-least-general-induct i current n s min data-segment)) (expand (NUMBER-WITH-AT-LEAST-CLOCK-LOOP I MIN (CDR (ASSOC S DATA-SEGMENT)))))) (defn number-with-at-least-clock (min array) (plus 3 (number-with-at-least-clock-loop 0 min array))) (defn number-with-at-least-input-conditionp (p0) (and (equal (car (car (p-temp-stk p0))) 'nat) (equal (cddr (car (p-temp-stk p0))) nil) (equal (car (cadr (p-temp-stk p0))) 'nat) (equal (cddr (cadr (p-temp-stk p0))) nil) (equal (car (caddr (p-temp-stk p0))) 'addr) (equal (cdadr (caddr (p-temp-stk p0))) 0) (equal (cddr (caddr (p-temp-stk p0))) nil) (listp (cadr (caddr (p-temp-stk p0)))) (lessp (length (array (car (cadr (caddr (p-temp-stk p0)))) (p-data-segment p0))) (exp 2 (p-word-size p0))) (not (zerop (p-word-size p0))) (listp (p-ctrl-stk p0)) (nat-list-piton (array (car (cadr (caddr (p-temp-stk p0)))) (p-data-segment p0)) (p-word-size p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 6 (p-max-ctrl-stk-size p0)) (at-least-morep (length (p-temp-stk p0)) 0 (p-max-temp-stk-size p0)) (equal (definition 'number-with-at-least (p-prog-segment p0)) (number-with-at-least-program)) (definedp (car (cadr (caddr (p-temp-stk p0)))) (p-data-segment p0)) (lessp (cadr (car (p-temp-stk p0))) (exp 2 (p-word-size p0))) (numberp (cadr (car (p-temp-stk p0)))) (lessp 0 (cadr (cadr (p-temp-stk p0)))) (equal (cadr (cadr (p-temp-stk p0))) (length (array (car (cadr (caddr (p-temp-stk p0)))) (p-data-segment p0)))))) (prove-lemma correctness-of-number-with-at-least (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons m (cons n (cons s temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call number-with-at-least)) (number-with-at-least-input-conditionp p0) (equal minc (cadr m)) (equal arrayc (array (car (cadr s)) data-segment))) (equal (p (p-state pc ctrl-stk (cons m (cons n (cons s temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (number-with-at-least-clock minc arrayc)) (p-state (add1-addr pc) ctrl-stk (cons (list 'nat (number-with-at-least (untag-array (array (car (cadr s)) data-segment)) (cadr m))) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((use (number-with-at-least-correctness-general (i 0) (current 0) (s (car (cadr s))) (ret-pc (add1-addr pc)) (n (cadr n)) (min (cadr m)))) (disable number-with-at-least-clock-loop))) ;; highest-bit (defn highest-bit-program nil '(highest-bit (bv) ((cb (nat 0))) (call push-1-vector) (set-local cb) (rsh-bitv) (dl loop () (push-local cb)) (test-bitv-and-jump all-zero done) (push-local bv) (push-local cb) (and-bitv) (test-bitv-and-jump all-zero lab) (pop) (push-local cb) (dl lab () (push-local cb)) (lsh-bitv) (pop-local cb) (jump loop) (dl done () (ret)))) (defn example-highest-bit-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (bitv (0 0 0 0 0 0 0 0))) (call highest-bit) (push-constant (bitv (0 0 1 1 0 1 0 0))) (call highest-bit) (push-constant (bitv (1 0 1 1 0 1 0 0))) (call highest-bit) (ret)) (highest-bit-program) (push-1-vector-program 8)) nil 10 8 8 'run)) (defn highest-bit (x) (if (listp x) (if (equal (car x) 0) (cons 0 (highest-bit (cdr x))) (cons 1 (zero-bit-vector (length (cdr x))))) nil)) (prove-lemma listp-highest-bit (rewrite) (equal (listp (highest-bit x)) (listp x))) (prove-lemma length-highest-bit (rewrite) (equal (length (highest-bit x)) (length x))) (defn highest-bit-loop-clock (cb bv) (if (all-zero-bitvp cb) 3 (plus 10 (if (all-zero-bitvp (and-bitv cb bv)) 0 2) (highest-bit-loop-clock (append (cdr cb) '(0)) bv))) ((lessp (difference (length cb) (trailing-zeros cb))))) (defn highest-bit-induct (current bv cb) (if (all-zero-bitvp cb) t (highest-bit-induct (if (all-zero-bitvp (and-bitv cb bv)) current cb) bv (append (cdr cb) '(0)))) ((lessp (difference (length cb) (trailing-zeros cb))))) (prove-lemma bit-vectorp-simple-not (rewrite) (implies (not (equal (length x) (fix y))) (not (bit-vectorp x y)))) (prove-lemma at-most-one-bit-on-cdr (rewrite) (implies (at-most-one-bit-on x) (at-most-one-bit-on (cdr x)))) (prove-lemma equal-one-bit-vector (rewrite) (equal (equal x (one-bit-vector z)) (or (and (zerop z) (equal x '(1))) (and (bit-vectorp x z) (all-zero-bitvp (all-but-last x)) (not (equal (last x) 0)))))) (prove-lemma at-most-one-bit-is-all-zeros (rewrite) (implies (not (equal (last x) 0)) (equal (at-most-one-bit-on x) (all-zero-bitvp (all-but-last x))))) (defn highest-bit2-helper (current cb bv) (if (all-zero-bitvp cb) current (highest-bit2-helper (if (all-zero-bitvp (and-bitv bv cb)) current cb) (append (cdr cb) '(0)) bv)) ((lessp (difference (length cb) (trailing-zeros cb))))) (prove-lemma equal-x-zero-bit-vector (rewrite) (equal (equal x (zero-bit-vector y)) (and (all-zero-bitvp x) (bit-vectorp x y)))) (prove-lemma all-zero-bitvp-all-but-last-simple (rewrite) (implies (all-zero-bitvp x) (all-zero-bitvp (all-but-last x)))) (prove-lemma equal-trailing-zeros-acc-irrelevant (rewrite) (equal (equal (trailing-zeros-helper x acc1) (trailing-zeros-helper x acc2)) (or (equal (fix acc1) (fix acc2)) (not (all-zero-bitvp x))))) (prove-lemma lessp-trailing-zeros (rewrite) (implies (not (all-zero-bitvp z)) (lessp (trailing-zeros-helper z acc) (length z)))) (prove-lemma nthcdr-append (rewrite) (equal (nthcdr n (append x y)) (if (lessp (length x) n) (nthcdr (difference n (length x)) y) (append (nthcdr n x) y)))) (prove-lemma listp-zero-bit-vector (rewrite) (equal (listp (zero-bit-vector x)) (not (zerop x)))) (prove-lemma and-bitv-append (rewrite) (equal (and-bitv (append x y) z) (append (and-bitv x (make-list-from (length x) z)) (and-bitv y (nthcdr (length x) z)))) ((induct (double-cdr-induct x z)))) (prove-lemma and-bitv-append2 (rewrite) (implies (equal (length (append x y)) (length z)) (equal (and-bitv z (append x y)) (append (and-bitv x (make-list-from (length x) z)) (and-bitv y (nthcdr (length x) z))))) ((induct (double-cdr-induct x z)))) (prove-lemma all-zero-bitvp-and-bitv-append (rewrite) (equal (all-zero-bitvp (and-bitv z (append x y))) (and (all-zero-bitvp (and-bitv (make-list-from (length x) z) x)) (all-zero-bitvp (and-bitv (nthcdr (length x) z) y)))) ((induct (double-cdr-induct x z)))) (prove-lemma length-cdr-zero-bit-vector (rewrite) (equal (length (cdr (zero-bit-vector x))) (sub1 x))) (prove-lemma length-nthcdr (rewrite) (equal (length (nthcdr n x)) (difference (length x) n))) (disable and-bitv-special) (disable and-bitv-special-special) (disable and-bitv-special-3) (disable and-bitv-special-4) (disable and-bitv-special-5) (disable and-bitv-special-6) (prove-lemma bit-vectorp-zero-bit-vector-better (rewrite) (equal (bit-vectorp (zero-bit-vector x) size) (equal (fix x) (fix size)))) (prove-lemma highest-bit-correctness-general nil (implies (and (not (zerop word-size)) (at-most-one-bit-on cb) (listp ctrl-stk) (at-least-morep (length temp-stk) 3 max-temp-stk-size) (equal (definition 'highest-bit prog-segment) (highest-bit-program)) (bit-vectorp bv word-size) (bit-vectorp cb word-size) (bit-vectorp current word-size)) (equal (p (p-state '(pc (highest-bit . 3)) (cons (list (list (cons 'bv (list 'bitv bv)) (cons 'cb (list 'bitv cb))) ret-pc) ctrl-stk) (cons (list 'bitv current) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (highest-bit-loop-clock cb bv)) (p-state ret-pc ctrl-stk (cons (list 'bitv (highest-bit2-helper current cb bv)) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((induct (highest-bit-induct current bv cb)))) (prove-lemma make-list-from-simple (rewrite) (implies (zerop n) (equal (make-list-from n x) nil))) (prove-lemma not-all-zero-bitvp-make-list-from (rewrite) (implies (and (all-zero-bitvp (make-list-from n1 x)) (not (lessp n1 n2))) (all-zero-bitvp (make-list-from n2 x)))) (disable nthcdr-open) ;(prove-lemma listp-append (rewrite) ; (equal ; (listp (append x y)) ; (or (listp x) (listp y)))) (enable listp-append) (prove-lemma highest-bit2-helper-cons-1 (rewrite) (implies (and (not (all-zero-bitvp cb)) (at-most-one-bit-on cb) (equal (length cb) (length bv)) (bit-vectorp cb (length cb)) (equal (car bv) 1)) (equal (highest-bit2-helper current cb bv) (cons 1 (zero-bit-vector (length (cdr bv))))))) (prove-lemma bit-vectorp-append-cdr-hack (rewrite) (implies (bit-vectorp x n) (equal (bit-vectorp (append (cdr x) '(0)) n) (listp x)))) (defn triple-cdr-with-sub1-induct (x y z n) (if (zerop n) t (triple-cdr-with-sub1-induct (cdr x) (cdr y) (cdr z) (sub1 n)))) (prove-lemma car-append-better (rewrite) (equal (car (append x y)) (if (listp x) (car x) (car y)))) (prove-lemma open-highest-when-and-not-0 (rewrite) (implies (and (not (all-zero-bitvp (and-bitv x y))) (equal (length x) (length y))) (equal (highest-bit2-helper c x y) (highest-bit2-helper x (append (cdr x) '(0)) y)))) ;(prove-lemma cdr-append (rewrite) ; (equal ; (cdr (append x y)) ; (if (listp x) ; (append (cdr x) y) ; (cdr y)))) (enable cdr-append) (prove-lemma highest-bit2-helper-cons-0 (rewrite) (implies (and (not (all-zero-bitvp cb)) (at-most-one-bit-on cb) (bit-vectorp cb size) (bit-vectorp bv size) (bit-vectorp current size) (equal (car bv) 0) (equal (car current) 0)) (equal (highest-bit2-helper current cb bv) (cons 0 (highest-bit2-helper (cdr current) (cdr cb) (cdr bv))))) ((expand (highest-bit2-helper z x v)))) (prove-lemma highest-bit2-helper-cons-0-rewrite (rewrite) (implies (and (not (all-zero-bitvp cb)) (at-most-one-bit-on cb) (bit-vectorp cb (length cb)) (bit-vectorp bv (length cb)) (bit-vectorp current (length cb)) (equal (car bv) 0) (equal (car current) 0)) (equal (highest-bit2-helper current cb bv) (cons 0 (highest-bit2-helper (cdr current) (cdr cb) (cdr bv))))) ((use (highest-bit2-helper-cons-0 (size (length cb)))))) (prove-lemma append-zeros-0 (rewrite) (implies (and (all-zero-bitvp x) (properp x)) (equal (append x '(0)) (cons 0 x)))) (prove-lemma highest-bit2-helper-cons-helper nil (implies (and (bit-vectorp bv size) (bit-vectorp cb size) (at-most-one-bit-on cb) (at-most-one-bit-on current) (not (all-zero-bitvp cb)) (or (all-zero-bitvp current) (lessp (trailing-zeros current) (trailing-zeros cb))) (bit-vectorp current size) (not (zerop size))) (equal (highest-bit2-helper current cb bv) (if (equal (car bv) 0) (cons 0 (highest-bit2-helper (cdr current) (cdr cb) (cdr bv))) (cons 1 (zero-bit-vector (sub1 size)))))) ((induct (triple-cdr-with-sub1-induct bv cb current size)))) (prove-lemma highest-bit2-helper-cons-helper-rewrite (rewrite) (implies (and (bit-vectorp bv (length bv)) (bit-vectorp cb (length bv)) (at-most-one-bit-on cb) (at-most-one-bit-on current) (not (all-zero-bitvp cb)) (or (all-zero-bitvp current) (lessp (trailing-zeros current) (trailing-zeros cb))) (bit-vectorp current (length bv)) (listp bv)) (equal (highest-bit2-helper current cb bv) (if (equal (car bv) 0) (cons 0 (highest-bit2-helper (cdr current) (cdr cb) (cdr bv))) (cons 1 (zero-bit-vector (sub1 (length bv))))))) ((use (highest-bit2-helper-cons-helper (size (length bv)))) (disable-theory t) (enable equal-length-0) (enable-theory ground-zero))) (prove-lemma bit-vectorp-cdr-from-free (rewrite) (implies (bit-vectorp x n) (equal (bit-vectorp (cdr x) s) (equal (add1 s) n)))) (prove-lemma all-zero-bitvp-one-bit-vector (rewrite) (not (all-zero-bitvp (one-bit-vector x)))) (prove-lemma trailing-zeros-one-bit-vector (rewrite) (equal (trailing-zeros (one-bit-vector n)) 0)) (prove-lemma cdr-zero-one-bit-vector (rewrite) (and (equal (cdr (one-bit-vector x)) (if (lessp x 2) nil (one-bit-vector (sub1 x)))) (equal (cdr (zero-bit-vector x)) (if (zerop x) 0 (zero-bit-vector (sub1 x)))))) (prove-lemma highest-bit2-helper-highest-bit (rewrite) (implies (and (bit-vectorp bv word-size) (not (zerop word-size))) (equal (highest-bit2-helper (zero-bit-vector word-size) (one-bit-vector word-size) bv) (highest-bit bv))) ((induct (bit-vectorp bv word-size)) (disable-theory t) (enable-theory ground-zero naturals) (enable highest-bit2-helper-cons-helper-rewrite bv-length-weaker LENGTH-FROM-BIT-VECTORP at-most-one-bit-on-one-bit-vector *1*zero-bit-vector *1*one-bit-vector *1*highest-bit2-helper bitp bit-vectorp cdr-zero-one-bit-vector ALL-ZERO-BITVP-ZERO-BIT-VECTOR bit-vectorp-simple-not length highest-bit TRAILING-ZEROS-OF-ALL-ZERO-BITVP bit-vectorp-zero-bit-vector-better length-zero-bit-vector trailing-zeros-one-bit-vector all-zero-bitvp-one-bit-vector ALL-ZERO-BITVP-MEANS-AT-MOST-ONE-BIT-ON bit-vectorp-one-bit-vector-rewrite))) (defn highest-bit-input-conditionp (p0) (and (equal (car (top (p-temp-stk p0))) 'bitv) (equal (cddr (top (p-temp-stk p0))) nil) (not (zerop (p-word-size p0))) (listp (p-ctrl-stk p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 6 (p-max-ctrl-stk-size p0)) (at-least-morep (length (p-temp-stk p0)) 2 (p-max-temp-stk-size p0)) (equal (definition 'highest-bit (p-prog-segment p0)) (highest-bit-program)) (equal (definition 'push-1-vector (p-prog-segment p0)) (push-1-vector-program (p-word-size p0))) (bit-vectorp (cadr (top (p-temp-stk p0))) (p-word-size p0)))) (defn highest-bit-clock (bv) (plus 6 (highest-bit-loop-clock (one-bit-vector (length bv)) bv))) (prove-lemma cons-0-zero-bit-vector (rewrite) (equal (cons 0 (zero-bit-vector x)) (zero-bit-vector (add1 x)))) (disable cons-0-zero-bit-vector) (prove-lemma correctness-of-highest-bit (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons b temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call highest-bit)) (equal bc (cadr b)) (highest-bit-input-conditionp p0)) (equal (p (p-state pc ctrl-stk (cons b temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (highest-bit-clock bc)) (p-state (add1-addr pc) ctrl-stk (cons (list 'bitv (highest-bit (cadr b))) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((use (highest-bit-correctness-general (ret-pc (add1-addr pc)) (current (zero-bit-vector word-size)) (cb (one-bit-vector word-size)) (bv (cadr b)))) (expand (highest-bit-clock (cadr b))) (enable cons-0-zero-bit-vector) (disable highest-bit-loop-clock zero-bit-vector))) ;; match-and-xor (defn match-and-xor-program () '(match-and-xor (vecs numvecs match xor-vector) ((i (nat 0))) (push-constant (nat 0)) (pop-local i) (dl loop () (push-local vecs)) (fetch) (push-local match) (and-bitv) (test-bitv-and-jump not-all-zeros found) (push-local i) (add1-nat) (set-local i) (push-local numvecs) (lt-nat) (test-bool-and-jump f done) (push-local vecs) (push-constant (nat 1)) (add-addr) (pop-local vecs) (jump loop) (dl found () (push-local vecs)) (fetch) (push-local xor-vector) (xor-bitv) (push-local vecs) (deposit) (dl done () (ret)))) (defn example-match-and-xor-p-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (addr (arr . 0))) (push-constant (nat 6)) (push-constant (bitv (0 0 0 1 0 0 0 0))) (push-constant (bitv (1 1 1 1 1 1 1 1))) (call match-and-xor) (ret)) (match-and-xor-program)) '((arr (bitv (0 1 0 0 1 0 0 1)) (bitv (0 0 0 0 0 0 0 1)) (bitv (0 0 0 1 0 0 0 1)) (bitv (0 0 0 0 0 0 0 1)) (bitv (0 0 0 1 0 0 0 1)) (bitv (0 1 1 0 1 0 0 1)))) 10 8 8 'run)) (defn match-and-xor (bvs match xor-vector) (if (listp bvs) (if (all-zero-bitvp (and-bitv (car bvs) match)) (cons (car bvs) (match-and-xor (cdr bvs) match xor-vector)) (cons (xor-bitv (car bvs) xor-vector) (cdr bvs))) nil)) (defn match-and-xor-loop-clock (bvs match) (if (listp bvs) (if (all-zero-bitvp (and-bitv (car bvs) match)) (if (listp (cdr bvs)) (plus 16 (match-and-xor-loop-clock (cdr bvs) match)) 12) 12) 0)) (defn tag-array (tag array) (if (listp array) (cons (tag tag (car array)) (tag-array tag (cdr array))) nil)) (defn match-and-xor-general-induct (numvecs i) (if (lessp i numvecs) (match-and-xor-general-induct numvecs (add1 i)) t) ((lessp (difference numvecs i)))) (prove-lemma tag-array-untag-array (rewrite) (implies (bit-vectors-piton x (length (untag (car x)))) (equal (tag-array 'bitv (untag-array x)) x))) (prove-lemma bit-vectors-piton-free-means (rewrite) (implies (bit-vectors-piton x size) (and (bit-vectors-piton x (length (cadr (car x)))) (equal (bit-vectors-piton (cdr x) (length (cadr (cadr x)))) (listp x))))) (prove-lemma listp-cdr-nthcdr (rewrite) (equal (listp (cdr (nthcdr i x))) (lessp i (length (cdr x))))) (prove-lemma nthcdr-untag-array (rewrite) (equal (nthcdr i (untag-array x)) (if (lessp i (length x)) (untag-array (nthcdr i x)) (if (equal (fix i) (length x)) nil 0)))) (prove-lemma put-length-cdr (rewrite) (implies (properp x) (equal (put val (length (cdr x)) x) (append (all-but-last x) (list val))))) (prove-lemma nthcdr-length-cdr (rewrite) (implies (properp x) (equal (nthcdr (length (cdr x)) x) (if (listp x) (list (last x)) nil)))) (prove-lemma get-length-cdr (rewrite) (equal (get (length (cdr x)) x) (if (listp x) (last x) 0))) (prove-lemma append-all-but-last-last (rewrite) (implies (properp x) (equal (append (all-but-last x) (list (last x))) (if (nlistp x) (list (last x)) x)))) (prove-lemma listp-cdr-untag-array (rewrite) (equal (listp (cdr (untag-array x))) (listp (cdr x)))) (prove-lemma bit-vectorp-last (rewrite) (implies (bit-vectors-piton bvs s) (equal (bit-vectorp (cadr (last bvs)) s) (listp bvs)))) (prove-lemma bit-vectors-piton-means-properp (rewrite) (implies (bit-vectors-piton x s) (properp x))) (prove-lemma bit-vectors-piton-means-last (rewrite) (implies (and (bit-vectors-piton state size) (listp state)) (and (equal (car (last state)) 'bitv) (listp (last state)) (bit-vectorp (cadr (last state)) size) (equal (cddr (last state)) nil) (equal (length (cadr (last state))) (fix size)))) ((disable bit-vectorp-last))) (prove-lemma list-bitv-cadr-bitvp (rewrite) (implies (and (equal (car x) 'bitv) (equal (cddr x) nil)) (equal (list 'bitv (cadr x)) x))) (prove-lemma equal-x-put-assoc-x (rewrite) (equal (equal x (put-assoc val name x)) (or (not (definedp name x)) (equal (assoc name x) (cons name val))))) (prove-lemma cons-n-assoc-n (rewrite) (implies (listp (assoc n d)) (equal (cons n (cdr (assoc n d))) (if (definedp n d) (assoc n d) (cons n 0))))) (prove-lemma cons-n-cadr-list-assoc-n (rewrite) (implies (equal (cddr (assoc n d)) nil) (equal (list n (cadr (assoc n d))) (if (definedp n d) (assoc n d) (cons n 0))))) (prove-lemma cons-n-assoc-n-hack (rewrite) (implies (listp (cdr (assoc n d))) (equal (cons n (cdr (assoc n d))) (if (definedp n d) (assoc n d) (cons n 0))))) (prove-lemma car-untag-array (rewrite) (equal (car (untag-array x)) (untag (car x)))) (prove-lemma car-nthcdr (rewrite) (equal (car (nthcdr i x)) (get i x))) (prove-lemma tag-array-cdr-untag-array-hack (rewrite) (implies (bit-vectors-piton x (length (untag (car x)))) (equal (tag-array 'bitv (cdr (untag-array x))) (if (listp x) (cdr x) nil)))) (prove-lemma bit-vectors-piton-means-car (rewrite) (implies (and (bit-vectors-piton state size) (listp state)) (and (equal (caar state) 'bitv) (listp (car state)) (bit-vectorp (cadr (car state)) size) (equal (cddr (car state)) nil) (equal (length (cadr (car state))) (fix size))))) (prove-lemma equal-put-assoc (rewrite) (equal (equal (put-assoc v1 n s) (put-assoc v2 n s)) (or (not (definedp n s)) (equal v1 v2)))) (prove-lemma get-nlistp-better (rewrite) (implies (not (lessp i (length x))) (equal (get i x) 0))) (prove-lemma equal-append-zero-bit-vector-zero-bit-vector (rewrite) (equal (equal (append (zero-bit-vector n1) x) (append (zero-bit-vector n2) y)) (if (lessp n1 n2) (equal x (append (zero-bit-vector (difference n2 n1)) y)) (equal y (append (zero-bit-vector (difference n1 n2)) x))))) (prove-lemma append-make-list-from-cons-get-hack (rewrite) (equal (append (make-list-from i x) (cons (get i x) y)) (append (make-list-from (add1 i) x) y))) (prove-lemma cdr-untag-array-nthcdr (rewrite) (implies (lessp i (length x)) (equal (cdr (untag-array (nthcdr i x))) (untag-array (nthcdr i (cdr x)))))) (prove-lemma equal-nil-nthcdr-length (rewrite) (equal (equal nil (nthcdr (length x) x)) (properp x))) (prove-lemma lessp-0-length-better (rewrite) (implies (zerop x) (equal (lessp x (length y)) (listp y)))) (prove-lemma bit-vectors-piton-means-get-cdr (rewrite) (implies (bit-vectors-piton state size) (and (equal (car (get i (cdr state))) (if (lessp i (length (cdr state))) 'bitv 0)) (equal (listp (get i (cdr state))) (lessp i (length (cdr state)))) (equal (bit-vectorp (cadr (get i (cdr state))) size) (lessp i (length (cdr state)))) (equal (cddr (get i (cdr state))) (if (lessp i (length (cdr state))) nil 0)) (equal (length (cadr (get i (cdr state)))) (if (lessp i (length (cdr state))) (fix size) 0)))) ((induct (get i state)))) (prove-lemma bit-vectors-piton-nthcdr (rewrite) (implies (bit-vectors-piton x s1) (and (equal (bit-vectors-piton (nthcdr i x) s) (or (and (lessp i (length x)) (equal (fix s1) (fix s))) (equal (fix i) (length x)))) (equal (bit-vectors-piton (nthcdr i (cdr x)) s) (and (lessp i (length x)) (or (equal (fix s) (fix s1)) (equal (fix i) (length (cdr x))))))))) (prove-lemma tag-array-untag-array-nthcdr-cddr-hack (rewrite) (implies (and (lessp i (length x)) (bit-vectors-piton x s)) (equal (tag-array 'bitv (untag-array (nthcdr i (cdr x)))) (nthcdr i (cdr x)))) ((use (tag-array-untag-array (x (nthcdr i (cdr x))))))) (prove-lemma append-make-list-from-put-hack (rewrite) (implies (lessp i (length x)) (equal (append (make-list-from i x) (cons v (nthcdr i (cdr x)))) (put v i x)))) (enable lessp-sub1-x-x) (enable lessp-x-x) (prove-lemma correctness-of-match-and-xor-general nil (implies (and (listp ctrl-stk) (at-least-morep (p-ctrl-stk-size ctrl-stk) 7 max-ctrl-stk-size) (at-least-morep (length temp-stk) 4 max-temp-stk-size) (equal (definition 'match-and-xor prog-segment) (match-and-xor-program)) (bit-vectorp match word-size) (bit-vectorp xor-vector word-size) (equal numvecs (length (array vecs data-segment))) (bit-vectors-piton (array vecs data-segment) word-size) (definedp vecs data-segment) (numberp i) (lessp i numvecs) (lessp (length (array vecs data-segment)) (exp 2 word-size))) (equal (p (p-state '(pc (match-and-xor . 2)) (cons (list (list (cons 'vecs (list 'addr (cons vecs i))) (cons 'numvecs (list 'nat numvecs)) (cons 'match (list 'bitv match)) (cons 'xor-vector (list 'bitv xor-vector)) (cons 'i (list 'nat i))) ret-pc) ctrl-stk) temp-stk prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (match-and-xor-loop-clock (nthcdr i (untag-array (array vecs data-segment))) match)) (p-state ret-pc ctrl-stk temp-stk prog-segment (put-assoc (append (make-list-from i (array vecs data-segment)) (tag-array 'bitv (match-and-xor (untag-array (nthcdr i (array vecs data-segment))) match xor-vector))) vecs data-segment) max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((induct (match-and-xor-general-induct numvecs i)) (disable bit-vectors-piton) (expand (match-and-xor-loop-clock (untag-array (nthcdr i (cdr (assoc vecs data-segment)))) match) (match-and-xor-loop-clock (untag-array (nthcdr (length (cddr (assoc vecs data-segment))) (cdr (assoc vecs data-segment)))) match)))) (defn match-and-xor-clock (bvs match) (plus 3 (match-and-xor-loop-clock bvs match))) (defn match-and-xor-input-conditionp (p0) (and (equal (car (top (p-temp-stk p0))) 'bitv) (equal (cddr (top (p-temp-stk p0))) nil) (equal (car (top (cdr (p-temp-stk p0)))) 'bitv) (equal (cddr (top (cdr (p-temp-stk p0)))) nil) (equal (car (top (cddr (p-temp-stk p0)))) 'nat) (equal (cddr (top (cddr (p-temp-stk p0)))) nil) (equal (car (top (cdddr (p-temp-stk p0)))) 'addr) (equal (cdr (cadr (top (cdddr (p-temp-stk p0))))) 0) (listp (cadr (top (cdddr (p-temp-stk p0))))) (equal (cddr (top (cdddr (p-temp-stk p0)))) nil) (not (zerop (cadr (top (cddr (p-temp-stk p0)))))) (listp (p-ctrl-stk p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 7 (p-max-ctrl-stk-size p0)) (at-least-morep (length (p-temp-stk p0)) 0 (p-max-temp-stk-size p0)) (equal (definition 'match-and-xor (p-prog-segment p0)) (match-and-xor-program)) (bit-vectorp (cadr (top (cdr (p-temp-stk p0)))) (p-word-size p0)) (bit-vectorp (cadr (top (p-temp-stk p0))) (p-word-size p0)) (equal (cadr (top (cddr (p-temp-stk p0)))) (length (array (car (cadr (top (cdddr (p-temp-stk p0))))) (p-data-segment p0)))) (definedp (car (cadr (top (cdddr (p-temp-stk p0))))) (p-data-segment p0)) (lessp (length (array (car (cadr (top (cdddr (p-temp-stk p0))))) (p-data-segment p0))) (exp 2 (p-word-size p0))) (bit-vectors-piton (array (car (cadr (top (cdddr (p-temp-stk p0))))) (p-data-segment p0)) (p-word-size p0)))) (prove-lemma correctness-of-match-and-xor (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons x (cons m (cons n (cons v temp-stk)))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call match-and-xor)) (match-and-xor-input-conditionp p0) (equal match (cadr m)) (equal vecs-to-match (untag-array (array (caadr v) data-segment)))) (equal (p (p-state pc ctrl-stk (cons x (cons m (cons n (cons v temp-stk)))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (match-and-xor-clock vecs-to-match match)) (p-state (add1-addr pc) ctrl-stk temp-stk prog-segment (put-assoc (tag-array 'bitv (match-and-xor (untag-array (array (caadr v) data-segment)) (cadr m) (cadr x))) (caadr v) data-segment) max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((disable match-and-xor-loop-clock) (use (correctness-of-match-and-xor-general (ret-pc (add1-addr pc)) (i 0) (xor-vector (cadr x)) (match (cadr m)) (numvecs (cadr n)) (vecs (caadr v)))))) ;;; nat-to-bv-list (defn nat-to-bv-list-program () '(nat-to-bv-list (nat-list bv-list length) ((i (nat 0))) (dl loop () (push-local nat-list)) (fetch) (call nat-to-bv) (push-local bv-list) (deposit) (push-local i) (add1-nat) (set-local i) (push-local length) (eq) (test-bool-and-jump t done) (push-local nat-list) (push-constant (nat 1)) (add-addr) (pop-local nat-list) (push-local bv-list) (push-constant (nat 1)) (add-addr) (pop-local bv-list) (jump loop) (dl done () (ret)))) (defn example-nat-to-bv-list-p-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (addr (arr . 0))) (push-constant (addr (arr2 . 0))) (push-constant (nat 6)) (call nat-to-bv-list) (ret)) (nat-to-bv-list-program) (nat-to-bv-program) (push-1-vector-program 8)) '((arr (nat 3) (nat 5) (nat 8) (nat 0) (nat 23) (nat 9)) (arr2 nil nil nil nil nil nil)) 100 80 8 'run)) (defn nat-to-bv-list (nat-list size) (if (listp nat-list) (cons (nat-to-bv (car nat-list) size) (nat-to-bv-list (cdr nat-list) size)) nil)) (defn nat-to-bv-list-loop-clock (i nats) (if (lessp i (length nats)) (clock-plus '2 (clock-plus (nat-to-bv-clock (untag (get i nats))) (if (lessp i (length (cdr nats))) (clock-plus '17 (nat-to-bv-list-loop-clock (add1 i) nats)) '9))) '0) ((lessp (difference (length nats) i)))) (defn nat-to-bv-list-loop-induct (i nats bvs-name word-size data-segment) (if (and (lessp i (length nats)) (lessp i (length (cdr nats)))) (nat-to-bv-list-loop-induct (add1 i) nats bvs-name word-size (put-assoc (append (make-list-from i (cdr (assoc bvs-name data-segment))) (cons (list 'bitv (nat-to-bv (untag (get i nats)) word-size)) (nthcdr (add1 i) (cdr (assoc bvs-name data-segment))))) bvs-name data-segment)) t) ((lessp (difference (length nats) i)))) (prove-lemma nat-list-piton-means-car (rewrite) (implies (and (nat-list-piton state size) (listp state)) (and (equal (caar state) 'nat) (listp (car state)) (numberp (cadr (car state))) (lessp (cadr (car state)) (exp 2 size)) (equal (lessp (cadr (car state)) (exp 2 size)) t) (equal (cddr (car state)) nil)))) (defn array-pitonp (array length) (if (listp array) (and (not (zerop length)) (array-pitonp (cdr array) (sub1 length))) (and (equal array nil) (zerop length)))) (prove-lemma nat-list-piton-means-last (rewrite) (implies (nat-list-piton state size) (and (equal (car (last state)) (if (listp state) 'nat 0)) (equal (listp (last state)) (listp state)) (numberp (cadr (last state))) (equal (lessp (cadr (last state)) (exp 2 size)) t) (equal (cddr (last state)) (if (listp state) nil 0))))) (prove-lemma nat-list-piton-means-last-cdr (rewrite) (implies (and (nat-list-piton state size) (listp state)) (and (equal (car (last (cdr state))) (if (listp (cdr state)) 'nat 0)) (equal (listp (last (cdr state))) (listp (cdr state))) (numberp (cadr (last (cdr state)))) (equal (lessp (cadr (last (cdr state))) (exp 2 size)) t) (equal (cddr (last (cdr state))) (if (listp (cdr state)) nil 0))))) ;(prove-lemma definedp-put-assoc (rewrite) ; (equal ; (definedp n (put-assoc v n1 a)) ; (definedp n a))) (enable definedp-put-assoc) (prove-lemma assoc-put-assoc-better (rewrite) (equal (assoc n1 (put-assoc v n2 a)) (if (definedp n1 a) (if (equal n1 n2) (cons n1 v) (assoc n1 a)) f))) (disable nat-to-bv-list-loop-clock) (prove-lemma get-add1 (rewrite) (implies (lessp n 4) (equal (get (add1 n) x) (get n (cdr x))))) (prove-lemma get-0-better (rewrite) (implies (zerop n) (equal (get n x) (car x)))) (prove-lemma length-cdr-tag-array (rewrite) (equal (length (cdr (tag-array l x))) (length (cdr x)))) (prove-lemma length-nat-to-bv-list (rewrite) (equal (length (nat-to-bv-list x s)) (length x))) (prove-lemma length-cdr-nat-to-bv-list (rewrite) (equal (length (cdr (nat-to-bv-list x s))) (length (cdr x)))) (prove-lemma length-tag-array (rewrite) (equal (length (tag-array l x)) (length x))) (prove-lemma listp-tag-array (rewrite) (equal (listp (tag-array l x)) (listp x))) (prove-lemma listp-nat-to-bv-list (rewrite) (equal (listp (nat-to-bv-list x s)) (listp x))) (prove-lemma array-pitonp-tag-array (rewrite) (equal (array-pitonp (tag-array l x) length) (equal (length x) (fix length))) ((induct (array-pitonp x length)))) (prove-lemma array-pitonp-append (rewrite) (equal (array-pitonp (append x y) size) (and (not (lessp size (length x))) (array-pitonp y (difference size (length x))))) ((induct (get size x)))) (prove-lemma nat-list-piton-means-cadr (rewrite) (implies (and (nat-list-piton state size) (listp (cdr state))) (and (equal (caadr state) 'nat) (listp (cadr state)) (numberp (cadr (cadr state))) (lessp (cadr (cadr state)) (exp 2 size)) (equal (lessp (cadr (cadr state)) (exp 2 size)) t) (equal (cddr (cadr state)) nil)))) (prove-lemma array-pitonp-add1 (rewrite) (equal (array-pitonp x (add1 n)) (and (listp x) (array-pitonp (cdr x) n)))) ;(prove-lemma put-assoc-put-assoc (rewrite) ; (equal ; (put-assoc v n (put-assoc v2 n a)) ; (put-assoc v n a))) (enable put-assoc-put-assoc) (prove-lemma length-cdr-nlistp (rewrite) (implies (not (listp (cdr x))) (equal (length x) (if (listp x) 1 0)))) (prove-lemma equal-nil-cdr-tag-array-hack (rewrite) (equal (equal nil (cdr (tag-array l x))) (equal (length x) 1))) (prove-lemma length-from-array-pitonp (rewrite) (implies (array-pitonp x s) (equal (length x) (fix s)))) (disable nat-to-bv-clock) (disable nat-to-bv-list-loop-clock) (prove-lemma nat-list-piton-means-get (rewrite) (implies (nat-list-piton state size) (and (equal (car (get p state)) (if (lessp p (length state)) 'nat 0)) (equal (listp (get p state)) (lessp p (length state))) (numberp (cadr (get p state))) (equal (lessp (cadr (get p state)) (exp 2 size)) t) (equal (cddr (get p state)) (if (lessp p (length state)) nil 0))))) (prove-lemma nat-list-piton-means-get-cdr (rewrite) (implies (and (nat-list-piton state size) (listp state)) (and (equal (car (get p (cdr state)) ) (if (lessp p (length (cdr state))) 'nat 0)) (equal (listp (get p (cdr state))) (lessp p (length (cdr state)))) (numberp (cadr (get p (cdr state)))) (equal (lessp (cadr (get p (cdr state))) (exp 2 size)) t) (equal (cddr (get p (cdr state))) (if (lessp p (length (cdr state))) nil 0))))) (disable nat-list-piton-means) (prove-lemma length-put-better (rewrite) (equal (length (put v n a)) (if (lessp n (length a)) (length a) (add1 n)))) (prove-lemma cons-car-x-put-append-make-list-from-hack (rewrite) (equal (cons (car (put v x b)) (append (make-list-from x (cdr (put v x b))) y)) (append (make-list-from x b) (cons v y)))) (prove-lemma array-pitonp-put (rewrite) (implies (and (array-pitonp a l) (equal (fix l) (fix length))) (equal (array-pitonp (put v n a) length) (lessp n (length a))))) (prove-lemma array-pitonp-means-properp (rewrite) (and (implies (array-pitonp x s) (properp x)) (implies (array-pitonp (cdr x) s) (properp x)))) (prove-lemma put-length-cdr-general (rewrite) (implies (and (properp x) (equal (length x) (length y))) (equal (put val (length (cdr y)) x) (append (all-but-last x) (list val))))) (prove-lemma nthcdr-x-cdr-put-x (rewrite) (implies (properp a) (equal (nthcdr x (cdr (put val x a))) (if (lessp x (length a)) (nthcdr x (cdr a)) nil)))) (prove-lemma equal-append-a-append-a (rewrite) (equal (equal (append a b) (append a c)) (equal b c))) ;The correctness lemma of nat-to-bv-list could be more general - ;the proof assumes the data areas are distinct, though the program ;works when they're not. I did it this way because I had assumed ;I'd need distinct arrays in NIM, and designed the proof accordingly. ;This is a weakness I should correct in this proof as it will lead ;to sloppy use of memory in the program, but it takes so long ;to do these proofs I'll wait. (prove-lemma correctness-of-nat-to-bv-list-general nil (implies (and (listp ctrl-stk) (at-least-morep (p-ctrl-stk-size ctrl-stk) 13 max-ctrl-stk-size) (at-least-morep (length temp-stk) 3 max-temp-stk-size) (equal (definition 'nat-to-bv-list prog-segment) (nat-to-bv-list-program)) (equal (definition 'nat-to-bv prog-segment) (nat-to-bv-program)) (equal (definition 'push-1-vector prog-segment) (push-1-vector-program word-size)) (equal length (length (array nats data-segment))) (array-pitonp (array bvs data-segment) length) (nat-list-piton (array nats data-segment) word-size) (definedp nats data-segment) (definedp bvs data-segment) (not (zerop word-size)) (numberp i) (lessp i length) (lessp length (exp 2 word-size)) (not (equal nats bvs)) (equal natlist (array nats data-segment))) (equal (p (p-state '(pc (nat-to-bv-list . 0)) (cons (list (list (cons 'nat-list (list 'addr (cons nats i))) (cons 'bv-list (list 'addr (cons bvs i))) (cons 'length (list 'nat length)) (cons 'i (list 'nat i))) ret-pc) ctrl-stk) temp-stk prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (nat-to-bv-list-loop-clock i natlist)) (p-state ret-pc ctrl-stk temp-stk prog-segment (put-assoc (append (make-list-from i (array bvs data-segment)) (tag-array 'bitv (nat-to-bv-list (untag-array (nthcdr i (array nats data-segment))) word-size))) bvs data-segment) max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((induct (nat-to-bv-list-loop-induct i natlist bvs word-size data-segment)) (disable nat-list-piton) (expand (ARRAY-PITONP (CDR (ASSOC BVS DATA-SEGMENT)) 1) (UNTAG-ARRAY (CDR (ASSOC NATS DATA-SEGMENT))) (UNTAG-ARRAY (CDR (ASSOC BVS DATA-SEGMENT))) (NAT-TO-BV-LIST-LOOP-CLOCK 0 (CDR (ASSOC NATS DATA-SEGMENT))) (nat-to-bv-list-loop-clock i natlist) (NAT-TO-BV-LIST-LOOP-CLOCK i (CDR (ASSOC NATS DATA-SEGMENT)))))) (defn nat-to-bv-list-clock (natlist) (clock-plus 1 (nat-to-bv-list-loop-clock 0 natlist))) (defn nat-to-bv-list-input-conditionp (p0) (and (listp (p-ctrl-stk p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 13 (p-max-ctrl-stk-size p0)) (at-least-morep (length (p-temp-stk p0)) 0 (p-max-temp-stk-size p0)) (equal (definition 'nat-to-bv-list (p-prog-segment p0)) (nat-to-bv-list-program)) (equal (definition 'nat-to-bv (p-prog-segment p0)) (nat-to-bv-program)) (equal (definition 'push-1-vector (p-prog-segment p0)) (push-1-vector-program (p-word-size p0))) (equal (cadr (top (p-temp-stk p0))) (length (array (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0)))) (array-pitonp (array (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0)) (cadr (top (p-temp-stk p0)))) (nat-list-piton (array (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0)) (p-word-size p0)) (definedp (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0)) (definedp (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0)) (equal (p-current-instruction p0) '(call nat-to-bv-list)) (not (zerop (p-word-size p0))) (not (equal (caadr (top (cddr (p-temp-stk p0)))) (caadr (top (cdr (p-temp-stk p0)))))) (equal (car (top (p-temp-stk p0))) 'nat) (not (zerop (cadr (top (p-temp-stk p0))))) (lessp (cadr (top (p-temp-stk p0))) (exp 2 (p-word-size p0))) (equal (cddr (top (p-temp-stk p0))) nil) (equal (car (top (cdr (p-temp-stk p0)))) 'addr) (listp (cadr (top (cdr (p-temp-stk p0))))) (equal (cdadr (top (cdr (p-temp-stk p0)))) 0) (equal (cddr (top (cdr (p-temp-stk p0)))) nil) (equal (car (top (cddr (p-temp-stk p0)))) 'addr) (listp (cadr (top (cddr (p-temp-stk p0))))) (equal (cdadr (top (cddr (p-temp-stk p0)))) 0) (equal (cddr (top (cddr (p-temp-stk p0)))) nil))) (prove-lemma correctness-of-nat-to-bv-list (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons l (cons b (cons n temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (nat-to-bv-list-input-conditionp p0) (equal natlist (array (caadr n) data-segment))) (equal (p (p-state pc ctrl-stk (cons l (cons b (cons n temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (nat-to-bv-list-clock natlist)) (p-state (add1-addr pc) ctrl-stk temp-stk prog-segment (put-assoc (tag-array 'bitv (nat-to-bv-list (untag-array (array (caadr n) data-segment)) word-size)) (caadr b) data-segment) max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((use (correctness-of-nat-to-bv-list-general (i 0) (ret-pc (LIST (CAR PC) (CONS (CAADR PC) (ADD1 (CDADR PC))))) (nats (caadr n)) (bvs (caadr b)) (length (cadr l)))))) (disable nat-to-bv-list-program) (disable match-and-xor-program) (disable highest-bit-program) (disable number-with-at-least-program) (disable bv-to-nat-program) (disable nat-to-bv-program) (disable push-1-vector-program) (disable xor-bvs-program) ;; bv-to-nat-list (defn bv-to-nat-list-program () '(bv-to-nat-list (bv-list nat-list length) ((i (nat 0))) (dl loop () (push-local bv-list)) (fetch) (call bv-to-nat) (push-local nat-list) (deposit) (push-local i) (add1-nat) (set-local i) (push-local length) (eq) (test-bool-and-jump t done) (push-local nat-list) (push-constant (nat 1)) (add-addr) (pop-local nat-list) (push-local bv-list) (push-constant (nat 1)) (add-addr) (pop-local bv-list) (jump loop) (dl done () (ret)))) (defn example-bv-to-nat-list-p-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (addr (arr . 0))) (push-constant (addr (arr2 . 0))) (push-constant (nat 6)) (call bv-to-nat-list) (ret)) (bv-to-nat-list-program) (bv-to-nat-program) (push-1-vector-program 8)) '((arr (bitv (0 1 0 1 0 1 0 0)) (bitv (1 1 1 1 1 1 1 1)) (bitv (0 1 0 1 0 1 0 0)) (bitv (0 1 0 1 0 1 0 0)) (bitv (0 0 0 0 0 0 0 0)) (bitv (0 1 0 1 0 1 0 0))) (arr2 nil nil nil nil nil nil)) 100 80 8 'run)) (defn bv-to-nat-list-input-conditionp (p0) (and (listp (p-ctrl-stk p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 13 (p-max-ctrl-stk-size p0)) (at-least-morep (length (p-temp-stk p0)) 0 (p-max-temp-stk-size p0)) (equal (definition 'bv-to-nat-list (p-prog-segment p0)) (bv-to-nat-list-program)) (equal (definition 'bv-to-nat (p-prog-segment p0)) (bv-to-nat-program)) (equal (definition 'push-1-vector (p-prog-segment p0)) (push-1-vector-program (p-word-size p0))) (equal (cadr (top (p-temp-stk p0))) (length (array (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0)))) (array-pitonp (array (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0)) (cadr (top (p-temp-stk p0)))) (bit-vectors-piton (array (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0)) (p-word-size p0)) (definedp (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0)) (definedp (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0)) (equal (p-current-instruction p0) '(call bv-to-nat-list)) (not (zerop (p-word-size p0))) (not (equal (caadr (top (cddr (p-temp-stk p0)))) (caadr (top (cdr (p-temp-stk p0)))))) (equal (car (top (p-temp-stk p0))) 'nat) (not (zerop (cadr (top (p-temp-stk p0))))) (lessp (cadr (top (p-temp-stk p0))) (exp 2 (p-word-size p0))) (equal (cddr (top (p-temp-stk p0))) nil) (equal (car (top (cdr (p-temp-stk p0)))) 'addr) (listp (cadr (top (cdr (p-temp-stk p0))))) (equal (cdadr (top (cdr (p-temp-stk p0)))) 0) (equal (cddr (top (cdr (p-temp-stk p0)))) nil) (equal (car (top (cddr (p-temp-stk p0)))) 'addr) (listp (cadr (top (cddr (p-temp-stk p0))))) (equal (cdadr (top (cddr (p-temp-stk p0)))) 0) (equal (cddr (top (cddr (p-temp-stk p0)))) nil))) (defn bv-to-nat-list-loop-clock (wordsize i bvs) (if (lessp i (length bvs)) (clock-plus '2 (clock-plus (bv-to-nat-clock wordsize (untag (get i bvs))) (if (lessp i (length (cdr bvs))) (clock-plus '17 (bv-to-nat-list-loop-clock wordsize (add1 i) bvs)) '9))) '0) ((lessp (difference (length bvs) i)))) (defn bv-to-nat-list (bv-list) (if (listp bv-list) (cons (bv-to-nat (car bv-list)) (bv-to-nat-list (cdr bv-list))) nil)) (defn bv-to-nat-list-loop-induct (i bvs nats-name data-segment) (if (and (lessp i (length bvs)) (lessp i (length (cdr bvs)))) (bv-to-nat-list-loop-induct (add1 i) bvs nats-name (put-assoc (append (make-list-from i (cdr (assoc nats-name data-segment))) (cons (list 'nat (bv-to-nat (untag (get i bvs)))) (nthcdr (add1 i) (cdr (assoc nats-name data-segment))))) nats-name data-segment)) t) ((lessp (difference (length bvs) i)))) (disable bv-to-nat-clock) (prove-lemma correctness-of-bv-to-nat-list-general nil (implies (and (listp ctrl-stk) (at-least-morep (p-ctrl-stk-size ctrl-stk) 13 max-ctrl-stk-size) (at-least-morep (length temp-stk) 3 max-temp-stk-size) (equal (definition 'bv-to-nat-list prog-segment) (bv-to-nat-list-program)) (equal (definition 'bv-to-nat prog-segment) (bv-to-nat-program)) (equal (definition 'push-1-vector prog-segment) (push-1-vector-program word-size)) (equal length (length (array bvs data-segment))) (bit-vectors-piton (array bvs data-segment) word-size) (array-pitonp (array nats data-segment) length) (definedp nats data-segment) (definedp bvs data-segment) (not (zerop word-size)) (numberp i) (lessp i length) (lessp length (exp 2 word-size)) (not (equal nats bvs)) (equal bvlist (array bvs data-segment))) (equal (p (p-state '(pc (bv-to-nat-list . 0)) (cons (list (list (cons 'bv-list (list 'addr (cons bvs i))) (cons 'nat-list (list 'addr (cons nats i))) (cons 'length (list 'nat length)) (cons 'i (list 'nat i))) ret-pc) ctrl-stk) temp-stk prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (bv-to-nat-list-loop-clock word-size i bvlist)) (p-state ret-pc ctrl-stk temp-stk prog-segment (put-assoc (append (make-list-from i (array nats data-segment)) (tag-array 'nat (bv-to-nat-list (untag-array (nthcdr i (array bvs data-segment)))))) nats data-segment) max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((induct (bv-to-nat-list-loop-induct i bvlist nats data-segment)) (disable bit-vectors-piton) (expand (ARRAY-PITONP (CDR (ASSOC BVS DATA-SEGMENT)) 1) (UNTAG-ARRAY (CDR (ASSOC NATS DATA-SEGMENT))) (UNTAG-ARRAY (CDR (ASSOC BVS DATA-SEGMENT))) (BV-TO-NAT-LIST-LOOP-CLOCK wordsize 0 (CDR (ASSOC NATS DATA-SEGMENT))) (bv-to-nat-list-loop-clock wordsize i bvlist) (BV-TO-NAT-LIST-LOOP-CLOCK wordsize i (CDR (ASSOC NATS DATA-SEGMENT)))))) (defn bv-to-nat-list-clock (word-size natlist) (clock-plus 1 (bv-to-nat-list-loop-clock word-size 0 natlist))) (disable bv-to-nat-list-loop-clock) (disable bv-to-nat-list-program) (prove-lemma correctness-of-bv-to-nat-list (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons l (cons n (cons b temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (bv-to-nat-list-input-conditionp p0) (equal bvlist (array (caadr b) data-segment))) (equal (p (p-state pc ctrl-stk (cons l (cons n (cons b temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (bv-to-nat-list-clock word-size bvlist)) (p-state (add1-addr pc) ctrl-stk temp-stk prog-segment (put-assoc (tag-array 'nat (bv-to-nat-list (untag-array (array (caadr b) data-segment)))) (caadr n) data-segment) max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((use (correctness-of-bv-to-nat-list-general (i 0) (ret-pc (LIST (CAR PC) (CONS (CAADR PC) (ADD1 (CDADR PC))))) (nats (caadr n)) (bvs (caadr b)) (length (cadr l)))))) ;; max-nat (defn max-nat-program () '(max-nat (nat-list length) ((i (nat 0)) (j (nat 0))) (push-constant (nat 0)) (dl loop () (set-local j)) (push-local j) (push-local nat-list) (fetch) (set-local j) (lt-nat) (test-bool-and-jump f lab) (pop) (push-local j) (dl lab () (push-local i)) (add1-nat) (set-local i) (push-local length) (eq) (test-bool-and-jump t done) (push-local nat-list) (push-constant (nat 1)) (add-addr) (pop-local nat-list) (jump loop) (dl done () (ret)))) (defn example-max-nat-p-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (addr (arr . 0))) (push-constant (nat 6)) (call max-nat) (ret)) (max-nat-program)) '((arr (nat 3) (nat 10) (nat 3) (nat 6) (nat 9) (nat 0)) (arr2 nil nil nil nil nil nil)) 100 80 8 'run)) (defn max-list-helper (val x) (if (listp x) (if (lessp val (car x)) (max-list-helper (car x) (cdr x)) (max-list-helper val (cdr x))) (fix val))) (defn max-list (x) (if (listp x) (if (lessp (max-list (cdr x)) (car x)) (car x) (max-list (cdr x))) 0)) (prove-lemma max-list-helper-max-list (rewrite) (equal (max-list-helper val x) (if (lessp (max-list x) val) val (max-list x)))) (prove-lemma max-list-helper-max-list-0 (rewrite) (equal (max-list-helper 0 x) (max-list x))) (disable max-list-helper-max-list) (defn max-nat-loop-clock (val i nats) (if (lessp i (length nats)) (if (lessp val (untag (get i nats))) (if (lessp i (length (cdr nats))) (clock-plus 20 (max-nat-loop-clock (untag (get i nats)) (add1 i) nats)) 16) (if (lessp i (length (cdr nats))) (clock-plus 18 (max-nat-loop-clock val (add1 i) nats)) 14)) 0) ((lessp (difference (length nats) i)))) (defn max-nat-loop-induct (i j x natlist length) (if (lessp i length) (max-nat-loop-induct (add1 i) (get i natlist) (if (lessp (untag (get i natlist)) (untag x)) (list 'nat (untag x)) (list 'nat (untag (get i natlist)))) natlist length) t) ((lessp (difference length i)))) (prove-lemma list-nat-from-assoc-nat-list-piton-hack (rewrite) (implies (nat-list-piton nl s) (and (implies (lessp z (length (cdr nl))) (equal (list 'nat (cadr (get z (cdr nl)))) (get z (cdr nl)))) (implies (listp nl) (and (equal (list 'nat (cadr (last nl))) (last nl)) (equal (list 'nat (cadr (car nl))) (car nl)))))) ((induct (get z nl)))) (prove-lemma correctness-of-max-nat-general nil (implies (and (listp ctrl-stk) (at-least-morep (p-ctrl-stk-size ctrl-stk) 4 max-ctrl-stk-size) (at-least-morep (length temp-stk) 4 max-temp-stk-size) (equal (definition 'max-nat prog-segment) (max-nat-program)) (equal length (length (array nats data-segment))) (nat-list-piton (array nats data-segment) word-size) (definedp nats data-segment) (not (zerop word-size)) (numberp i) (lessp i length) (numberp (untag x)) (lessp (untag x) (exp 2 word-size)) (equal (car x) 'nat) (equal (cddr x) nil) (lessp length (exp 2 word-size)) (equal natlist (array nats data-segment))) (equal (p (p-state '(pc (max-nat . 1)) (cons (list (list (cons 'nat-list (list 'addr (cons nats i))) (cons 'length (list 'nat length)) (cons 'i (list 'nat i)) (cons 'j j)) ret-pc) ctrl-stk) (cons x temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (max-nat-loop-clock (untag x) i (array nats data-segment))) (p-state ret-pc ctrl-stk (cons (list 'nat (max-list-helper (untag x) (untag-array (nthcdr i (array nats data-segment))))) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((expand (MAX-NAT-LOOP-CLOCK (cadr X) I (CDR (ASSOC NATS DATA-SEGMENT)))) (induct (max-nat-loop-induct i j x natlist length)))) (defn max-nat-clock (natlist) (clock-plus 2 (max-nat-loop-clock 0 0 natlist))) (defn max-nat-input-conditionp (p0) (and (listp (p-ctrl-stk p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 6 (p-max-ctrl-stk-size p0)) (at-least-morep (length (p-temp-stk p0)) 2 (p-max-temp-stk-size p0)) (equal (definition 'max-nat (p-prog-segment p0)) (max-nat-program)) (equal (untag (top (p-temp-stk p0))) (length (array (car (untag (top (cdr (p-temp-stk p0))))) (p-data-segment p0)))) (nat-list-piton (array (car (untag (top (cdr (p-temp-stk p0))))) (p-data-segment p0)) (p-word-size p0)) (definedp (car (untag (top (cdr (p-temp-stk p0))))) (p-data-segment p0)) (not (zerop (p-word-size p0))) (not (zerop (untag (top (p-temp-stk p0))))) (equal (car (top (p-temp-stk p0))) 'nat) (equal (car (top (cdr (p-temp-stk p0)))) 'addr) (listp (untag (top (cdr (p-temp-stk p0))))) (lessp (untag (top (p-temp-stk p0))) (exp 2 (p-word-size p0))) (equal (cddr (top (cdr (p-temp-stk p0)))) nil) (equal (cddr (top (p-temp-stk p0))) nil) (equal (cdr (untag (top (cdr (p-temp-stk p0))))) 0))) (prove-lemma correctness-of-max-nat (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons n (cons s temp-stk)) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call max-nat)) (max-nat-input-conditionp p0) (equal natlist (array (car (untag s)) data-segment))) (equal (p (p-state pc ctrl-stk (cons n (cons s temp-stk)) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (max-nat-clock natlist)) (p-state (add1-addr pc) ctrl-stk (cons (list 'nat (max-list (untag-array natlist))) temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((use (correctness-of-max-nat-general (i 0) (j '(nat 0)) (x (list 'nat 0)) (nats (caadr s)) (ret-pc (add1-addr pc)) (length (cadr n)))))) (disable max-nat-program) ;; replace-value ;; replace the first occurrence of oldval by newval in list ;; of naturals (assumes oldval occurs in list) (defn replace-value-program () '(replace-value (list oldval newval) () (dl loop () (push-local list)) (fetch) (push-local oldval) (eq) (test-bool-and-jump t done) (push-local list) (push-constant (nat 1)) (add-addr) (pop-local list) (jump loop) (dl done () (push-local newval)) (push-local list) (deposit) (ret))) (defn example-replace-value-p-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (addr (arr . 0))) (push-constant (nat 3)) (push-constant (nat 4)) (call replace-value) (ret)) (replace-value-program)) '((arr (nat 9) (nat 10) (nat 3) (nat 6) (nat 9) (nat 0))) 100 80 8 'run)) (defn replace-value-loop-clock (i list oldvalue) (if (lessp i (length list)) (if (equal (get i list) oldvalue) 9 (clock-plus 10 (replace-value-loop-clock (add1 i) list oldvalue))) 0) ((lessp (difference (length list) i)))) (defn replace-value-loop-induct (i list list-addr) (if (lessp i (length list)) (replace-value-loop-induct (add1 i) list (add1-addr list-addr)) t) ((lessp (difference (length list) i)))) (defn replace-value (list oldvalue newvalue) (if (listp list) (if (equal (car list) oldvalue) (cons newvalue (cdr list)) (cons (car list) (replace-value (cdr list) oldvalue newvalue))) nil)) (prove-lemma member-nthcdr-means (rewrite) (implies (member x (nthcdr i y)) (member x y))) (prove-lemma member-of-natlist-means (rewrite) (implies (and (nat-list-piton y s) (member x y)) (and (listp x) (equal (car x) 'nat) (numberp (cadr x)) (lessp (cadr x) (exp 2 s)) (equal (cddr x) nil)))) (prove-lemma replace-value-nthcdr-open (rewrite) (implies (and (not (equal (get x a) old)) (lessp x (length a))) (equal (replace-value (nthcdr x a) old new) (cons (get x a) (replace-value (nthcdr x (cdr a)) old new))))) (prove-lemma list-nat-cadr-get-hack (rewrite) (implies (and (nat-list-piton y s) (lessp x (length y))) (equal (list 'nat (cadr (get x y))) (get x y)))) (prove-lemma member-nthcdr-simplify (rewrite) (implies (and (lessp i (length x)) (not (member a (nthcdr i (cdr x))))) (equal (member a (nthcdr i x)) (equal a (get i x))))) (PROVE-LEMMA APPEND-MAKE-LIST-FROM-CONS-CDR (REWRITE) (IMPLIES (LESSP I (LENGTH Y)) (EQUAL (APPEND (MAKE-LIST-FROM I Y) (CONS V (CDR (NTHCDR I Y)))) (PUT V I Y)))) (prove-lemma correctness-of-replace-value-general nil (implies (and (listp ctrl-stk) (at-least-morep (length temp-stk) 2 max-temp-stk-size) (equal (definition 'replace-value prog-segment) (replace-value-program)) (nat-list-piton (array list data-segment) word-size) (definedp list data-segment) (not (zerop word-size)) (numberp i) (equal vallist (array list data-segment)) (equal (car list-addr) 'addr) (equal (cddr list-addr) nil) (listp (untag list-addr)) (equal (car (untag list-addr)) list) (equal (cdr (untag list-addr)) i) (equal (car newvalue) 'nat) (equal (cddr newvalue) nil) (equal (car oldvalue) 'nat) (equal (cddr oldvalue) nil) (numberp (cadr oldvalue)) (lessp (cadr oldvalue) (exp 2 word-size)) (numberp (untag newvalue)) (lessp (untag newvalue) (exp 2 word-size)) (member oldvalue (nthcdr i vallist))) (equal (p (p-state '(pc (replace-value . 0)) (cons (list (list (cons 'list list-addr) (cons 'oldval oldvalue) (cons 'newval newvalue)) ret-pc) ctrl-stk) temp-stk prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (replace-value-loop-clock i vallist oldvalue)) (p-state ret-pc ctrl-stk temp-stk prog-segment (put-assoc (append (make-list-from i (array list data-segment)) (replace-value (nthcdr i (array list data-segment)) oldvalue newvalue)) list data-segment) max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((expand (REPLACE-VALUE-LOOP-CLOCK (CDADR LIST-ADDR) (CDR (ASSOC (CAADR LIST-ADDR) DATA-SEGMENT)) OLDVALUE)) (induct (replace-value-loop-induct i vallist list-addr)) (disable member-of-natlist-means))) (defn replace-value-clock (list ov) (clock-plus 1 (replace-value-loop-clock 0 list ov))) (defn replace-value-input-conditionp (p0) (and (listp (p-ctrl-stk p0)) (at-least-morep (length (p-temp-stk p0)) 0 (p-max-temp-stk-size p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 5 (p-max-ctrl-stk-size p0)) (equal (definition 'replace-value (p-prog-segment p0)) (replace-value-program)) (nat-list-piton (array (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0)) (p-word-size p0)) (definedp (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0)) (not (zerop (p-word-size p0))) (equal (car (top (cddr (p-temp-stk p0)))) 'addr) (equal (cddr (top (cddr (p-temp-stk p0)))) nil) (listp (untag (top (cddr (p-temp-stk p0))))) (equal (cdr (untag (top (cddr (p-temp-stk p0))))) 0) (equal (car (top (p-temp-stk p0))) 'nat) (equal (cddr (top (p-temp-stk p0))) nil) (numberp (untag (top (p-temp-stk p0)))) (lessp (untag (top (p-temp-stk p0))) (exp 2 (p-word-size p0))) (member (top (cdr (p-temp-stk p0))) (array (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0))))) (prove-lemma correctness-of-replace-value (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons nv (cons ov (cons nats temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call replace-value)) (replace-value-input-conditionp p0) (equal natlist (array (car (untag nats)) data-segment)) (equal ov ov2)) (equal (p (p-state pc ctrl-stk (cons nv (cons ov (cons nats temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (replace-value-clock natlist ov2)) (p-state (add1-addr pc) ctrl-stk temp-stk prog-segment (put-assoc (replace-value natlist ov nv) (caadr nats) data-segment) max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((disable replace-value-loop-clock nat-list-piton-means-car) (use (correctness-of-replace-value-general (newvalue nv) (oldvalue ov) (list-addr nats) (i 0) (vallist natlist) (list (caadr nats)) (ret-pc (add1-addr pc)))))) (disable replace-value-program) ;; smart-move (defn smart-move-program () '(smart-move (state numpiles work-area) ((i (nat 0))) (push-local state) (push-local numpiles) (push-constant (nat 2)) (call number-with-at-least) (push-constant (nat 2)) (lt-nat) (test-bool-and-jump t lab) (push-local state) (push-local work-area) (push-local numpiles) (call nat-to-bv-list) (push-local work-area) (push-local numpiles) (push-local work-area) (push-local numpiles) (call xor-bvs) (set-local i) (call highest-bit) (push-local i) (call match-and-xor) (push-local work-area) (push-local state) (push-local numpiles) (call bv-to-nat-list) (ret) (dl lab () (push-local state)) (push-local state) (push-local numpiles) (call max-nat) (push-local state) (push-local numpiles) (push-constant (nat 1)) (call number-with-at-least) (div2-nat) (pop-local i) (pop) (push-local i) (call replace-value) (ret))) (defn example-smart-move-p-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (addr (arr . 0))) (push-constant (nat 4)) (push-constant (addr (arr5 . 0))) (call smart-move) (push-constant (addr (arr2 . 0))) (push-constant (nat 4)) (push-constant (addr (arr5 . 0))) (call smart-move) (push-constant (addr (arr3 . 0))) (push-constant (nat 4)) (push-constant (addr (arr5 . 0))) (call smart-move) (push-constant (addr (arr4 . 0))) (push-constant (nat 4)) (push-constant (addr (arr5 . 0))) (call smart-move) (ret)) (replace-value-program) (max-nat-program) (bv-to-nat-list-program) (nat-to-bv-list-program) (match-and-xor-program) (highest-bit-program) (number-with-at-least-program) (bv-to-nat-program) (nat-to-bv-program) (push-1-vector-program 8) (xor-bvs-program) (smart-move-program)) '((arr (nat 3) (nat 4) (nat 2) (nat 1)) (arr2 (nat 1) (nat 1) (nat 1) (nat 9)) (arr3 (nat 1) (nat 1) (nat 0) (nat 9)) (arr4 (nat 0) (nat 0) (nat 0) (nat 0)) (arr5 (nat 3) (nat 4) (nat 2) (nat 1))) 100 80 8 'run)) (defn smart-move (state wordsize) (if (lessp (number-with-at-least state 2) 2) (replace-value state (max-list state) (remainder (number-with-at-least state 1) 2)) (bv-to-nat-list (match-and-xor (nat-to-bv-list state wordsize) (highest-bit (xor-bvs (nat-to-bv-list state wordsize))) (xor-bvs (nat-to-bv-list state wordsize)))))) (defn smart-move-clock (state wordsize) (clock-plus 4 (clock-plus (number-with-at-least-clock 2 (tag-array 'nat state)) (clock-plus 3 (if (lessp (number-with-at-least state 2) 2) (clock-plus 3 (clock-plus (max-nat-clock (tag-array 'nat state)) (clock-plus 3 (clock-plus (number-with-at-least-clock 1 (tag-array 'nat state)) (clock-plus 4 (clock-plus (replace-value-clock (tag-array 'nat state) (list 'nat (max-list state))) 1)))))) (clock-plus 3 (clock-plus (nat-to-bv-list-clock (tag-array 'nat state)) (clock-plus 4 (clock-plus (xor-bvs-clock (length state)) (clock-plus 1 (clock-plus (highest-bit-clock (xor-bvs (nat-to-bv-list state wordsize))) (clock-plus 1 (clock-plus (match-and-xor-clock (nat-to-bv-list state wordsize) (highest-bit (xor-bvs (nat-to-bv-list state wordsize)))) (clock-plus 3 (clock-plus (bv-to-nat-list-clock wordsize (tag-array 'bitv (match-and-xor (nat-to-bv-list state wordsize) (highest-bit (xor-bvs (nat-to-bv-list state wordsize))) (xor-bvs (nat-to-bv-list state wordsize))))) 1))))))))))))))) (disable replace-value-clock) (disable max-nat-clock) (disable bv-to-nat-list-clock) (disable nat-to-bv-list-clock) (disable match-and-xor-clock) (disable highest-bit-clock) (disable number-with-at-least-clock) (disable bv-to-nat-clock) (disable nat-to-bv-clock) (disable xor-bvs-clock) (disable replace-value-program) (disable max-nat-program) (disable bv-to-nat-list-program) (disable nat-to-bv-list-program) (disable match-and-xor-program) (disable highest-bit-program) (disable number-with-at-least-program) (disable bv-to-nat-program) (disable nat-to-bv-program) (disable push-1-vector-program) (disable *1*xor-bvs-program) (disable *1*replace-value-program) (disable *1*max-nat-program) (disable *1*bv-to-nat-list-program) (disable *1*nat-to-bv-list-program) (disable *1*match-and-xor-program) (disable *1*highest-bit-program) (disable *1*number-with-at-least-program) (disable *1*bv-to-nat-program) (disable *1*nat-to-bv-program) (disable *1*push-1-vector-program) (disable *1*xor-bvs-program) (defn nat-listp (list size) (if (listp list) (and (numberp (car list)) (lessp (car list) (exp 2 size)) (nat-listp (cdr list) size)) (equal list nil))) (prove-lemma bv-to-nat-list-nat-to-bv-list (rewrite) (implies (nat-listp x size) (equal (bv-to-nat-list (nat-to-bv-list x size)) x))) (prove-lemma bit-vectorsp-nat-to-bv-list (rewrite) (bit-vectorsp (nat-to-bv-list x size) size)) (prove-lemma nat-to-bv-list-bv-to-nat-list (rewrite) (implies (bit-vectorsp x size) (equal (nat-to-bv-list (bv-to-nat-list x) size) x))) (prove-lemma bit-vectorsp-match-and-xor (rewrite) (implies (bit-vectorsp x size) (bit-vectorsp (match-and-xor x y z) size))) (prove-lemma equal-sub1-add1 (rewrite) (and (equal (equal (sub1 x) (add1 y)) (equal x (add1 (add1 y)))) (equal (equal (sub1 x) 0) (or (zerop x) (equal x 1))))) ;; part of more recent naturals library that's missing from Piton library (PROVE-LEMMA EQUAL-TIMES-X-X (REWRITE) (AND (EQUAL (EQUAL (TIMES X Y) X) (OR (AND (NUMBERP X) (EQUAL Y 1)) (EQUAL X 0))) (EQUAL (EQUAL (TIMES Y X) X) (OR (AND (NUMBERP X) (EQUAL Y 1)) (EQUAL X 0)))) ((INDUCT (TIMES Y X)))) (prove-lemma equal-exp-x-y-x (rewrite) (equal (equal (exp x y) x) (or (equal x 1) (and (equal x 0) (not (zerop y))) (and (numberp x) (equal y 1))))) (prove-lemma lessp-number-with-at-least (rewrite) (not (lessp (length x) (number-with-at-least x min)))) (prove-lemma bit-vectors-piton-tag-array (rewrite) (implies (bit-vectorsp x size) (bit-vectors-piton (tag-array 'bitv x) size))) (prove-lemma tag-array-untag-array-of-nat-list-piton (rewrite) (implies (nat-list-piton x size) (equal (tag-array 'nat (untag-array x)) x))) (prove-lemma tag-array-untag-array-of-bit-vectors-piton (rewrite) (implies (bit-vectors-piton x size) (equal (tag-array 'bitv (untag-array x)) x))) (prove-lemma bit-vectorp-xor-bvs-nat-to-bv-list (rewrite) (equal (bit-vectorp (xor-bvs (nat-to-bv-list x s)) s) (or (listp x) (zerop s)))) (prove-lemma listp-cdr-assoc-hack-from-free (rewrite) (implies (and (equal (length (cdr (assoc x y))) free) (not (zerop free))) (listp (cdr (assoc x y))))) (prove-lemma bit-vectorp-highest-bit (rewrite) (implies (bit-vectorp x s) (bit-vectorp (highest-bit x) s))) (prove-lemma length-match-and-xor (rewrite) (equal (length (match-and-xor list m v)) (length list))) (prove-lemma array-pitonp-from-nat-list-piton (rewrite) (implies (nat-list-piton x s) (equal (array-pitonp x length) (equal (fix length) (length x))))) (prove-lemma untag-array-tag-array-of-bit-vectorsp (rewrite) (implies (bit-vectorsp x size) (equal (untag-array (tag-array l x)) x))) (prove-lemma untag-array-tag-array-of-nat-to-bv-list (rewrite) (equal (untag-array (tag-array l (nat-to-bv-list x size))) (nat-to-bv-list x size))) (prove-lemma untag-array-tag-array-of-match-and-xor-hack (rewrite) (equal (untag-array (tag-array l (match-and-xor (nat-to-bv-list x s) y z))) (match-and-xor (nat-to-bv-list x s) y z))) (prove-lemma member-list-max-list (rewrite) (implies (nat-list-piton x s) (equal (member (list 'nat (max-list (untag-array x))) x) (listp x)))) (prove-lemma tag-array-replace-value-untag-array (rewrite) (implies (nat-list-piton x s) (equal (tag-array 'nat (replace-value (untag-array x) y z)) (replace-value x (list 'nat y) (list 'nat z))))) (defn smart-move-input-conditionp (p0) (and (listp (p-ctrl-stk p0)) (at-least-morep (length (p-temp-stk p0)) 3 (p-max-temp-stk-size p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 19 (p-max-ctrl-stk-size p0)) (lessp 1 (p-word-size p0)) (equal (cddr (top (p-temp-stk p0))) nil) (equal (cddr (top (cdr (p-temp-stk p0)))) nil) (equal (cddr (top (cddr (p-temp-stk p0)))) nil) (equal (car (top (p-temp-stk p0))) 'addr) (equal (car (top (cdr (p-temp-stk p0)))) 'nat) (lessp (untag (top (cdr (p-temp-stk p0)))) (exp 2 (p-word-size p0))) (not (zerop (untag (top (cdr (p-temp-stk p0)))))) (equal (car (top (cddr (p-temp-stk p0)))) 'addr) (listp (untag (top (p-temp-stk p0)))) (listp (untag (top (cddr (p-temp-stk p0))))) (equal (cdr (untag (top (p-temp-stk p0)))) 0) (equal (cdr (untag (top (cddr (p-temp-stk p0))))) 0) (definedp (car (untag (top (p-temp-stk p0)))) (p-data-segment p0)) (definedp (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0)) (not (equal (car (untag (top (p-temp-stk p0)))) (car (untag (top (cddr (p-temp-stk p0))))))) (nat-list-piton (array (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0)) (p-word-size p0)) (array-pitonp (array (car (untag (top (p-temp-stk p0)))) (p-data-segment p0)) (untag (top (cdr (p-temp-stk p0))))) (equal (length (array (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0))) (untag (top (cdr (p-temp-stk p0))))) (equal (assoc 'smart-move (p-prog-segment p0)) (smart-move-program)) (equal (assoc 'replace-value (p-prog-segment p0)) (replace-value-program)) (equal (assoc 'max-nat (p-prog-segment p0)) (max-nat-program)) (equal (assoc 'bv-to-nat-list (p-prog-segment p0)) (bv-to-nat-list-program)) (equal (assoc 'nat-to-bv-list (p-prog-segment p0)) (nat-to-bv-list-program)) (equal (assoc 'match-and-xor (p-prog-segment p0)) (match-and-xor-program)) (equal (assoc 'highest-bit (p-prog-segment p0)) (highest-bit-program)) (equal (assoc 'number-with-at-least (p-prog-segment p0)) (number-with-at-least-program)) (equal (assoc 'bv-to-nat (p-prog-segment p0)) (bv-to-nat-program)) (equal (assoc 'nat-to-bv (p-prog-segment p0)) (nat-to-bv-program)) (equal (assoc 'push-1-vector (p-prog-segment p0)) (push-1-vector-program (p-word-size p0))) (equal (assoc 'xor-bvs (p-prog-segment p0)) (xor-bvs-program)))) (prove-lemma correctness-of-smart-move (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons wa (cons np (cons s temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call smart-move)) (equal state (untag-array (array (car (untag s)) data-segment))) (equal word-size word-size2) (smart-move-input-conditionp p0)) (equal (p (p-state pc ctrl-stk (cons wa (cons np (cons s temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (smart-move-clock state word-size2)) (p-state (add1-addr pc) ctrl-stk temp-stk prog-segment (put-assoc (tag-array 'nat (smart-move state word-size)) (car (untag s)) (if (lessp (number-with-at-least state 2) 2) data-segment (put-assoc (tag-array 'bitv (nat-to-bv-list (smart-move state word-size) word-size)) (car (untag wa)) data-segment))) max-ctrl-stk-size max-temp-stk-size word-size 'run)))) (disable smart-move-clock) (disable smart-move-program) (disable *1*smart-move-program) ;; delay (defn delay-program () '(delay (time) () (dl lab () (push-local time)) (sub1-nat) (set-local time) (no-op) (no-op) (no-op) (no-op) (test-nat-and-jump zero done) (no-op) (jump lab) (dl done () (ret)))) (defn example-delay-p-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (nat 4)) (call delay) (ret)) (delay-program)) nil 100 80 8 'run)) (defn delay-loop-clock (time) (if (lessp time 2) 9 (plus 10 (delay-loop-clock (sub1 time))))) (prove-lemma correctness-of-delay-general nil (implies (and (listp ctrl-stk) (equal (definition 'delay prog-segment) (delay-program)) (at-least-morep (length temp-stk) 1 max-temp-stk-size) (lessp 0 time) (lessp time (exp 2 word-size))) (equal (p (p-state '(pc (delay . 0)) (cons (list (list (cons 'time (list 'nat time))) ret-pc) ctrl-stk) temp-stk prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (delay-loop-clock time)) (p-state ret-pc ctrl-stk temp-stk prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((induct (times time y)))) (defn delay-input-conditionp (p0) (and (listp (p-ctrl-stk p0)) (equal (definition 'delay (p-prog-segment p0)) (delay-program)) (equal (car (top (p-temp-stk p0))) 'nat) (at-least-morep (length (p-temp-stk p0)) 0 (p-max-temp-stk-size p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 3 (p-max-ctrl-stk-size p0)) (lessp 0 (cadr (top (p-temp-stk p0)))) (lessp (cadr (top (p-temp-stk p0))) (exp 2 (p-word-size p0))) (equal (cddr (top (p-temp-stk p0))) nil))) (defn delay-clock (time) (add1 (delay-loop-clock time))) (prove-lemma correctness-of-delay (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons n temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call delay)) (delay-input-conditionp p0) (equal time (cadr n))) (equal (p (p-state pc ctrl-stk (cons n temp-stk) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (delay-clock time)) (p-state (add1-addr pc) ctrl-stk temp-stk prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((use (correctness-of-delay-general (time (cadr n)) (ret-pc (add1-addr pc)))))) ;; computer-move (defn computer-move-program () '(computer-move (state numpiles work-area) ((i (nat 0))) (push-constant (nat 250)) (call delay) (push-constant (nat 250)) (call delay) (push-constant (nat 250)) (call delay) (push-constant (nat 250)) (call delay) (push-local state) (push-local numpiles) (push-constant (nat 2)) (call number-with-at-least) (test-nat-and-jump zero lab) (push-local state) (push-local work-area) (push-local numpiles) (call nat-to-bv-list) (push-local work-area) (push-local numpiles) (call xor-bvs) (test-bitv-and-jump all-zero lab) (push-local state) (push-local numpiles) (push-local work-area) (call smart-move) (ret) (dl lab () (push-local state)) (push-local state) (push-local numpiles) (call max-nat) (pop-local i) (push-local i) (push-local i) (sub1-nat) (call replace-value) (ret))) (defn example-computer-move-p-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (list '(main nil nil (push-constant (addr (arr . 0))) (push-constant (nat 4)) (push-constant (addr (arr5 . 0))) (call computer-move) (push-constant (addr (arr2 . 0))) (push-constant (nat 4)) (push-constant (addr (arr5 . 0))) (call computer-move) (push-constant (addr (arr3 . 0))) (push-constant (nat 4)) (push-constant (addr (arr5 . 0))) (call computer-move) (push-constant (addr (arr4 . 0))) (push-constant (nat 4)) (push-constant (addr (arr5 . 0))) (call computer-move) (ret)) (computer-move-program) (delay-program) (replace-value-program) (max-nat-program) (bv-to-nat-list-program) (nat-to-bv-list-program) (match-and-xor-program) (highest-bit-program) (number-with-at-least-program) (bv-to-nat-program) (nat-to-bv-program) (push-1-vector-program 8) (xor-bvs-program) (smart-move-program)) '((arr (nat 3) (nat 4) (nat 2) (nat 1)) (arr2 (nat 1) (nat 1) (nat 1) (nat 0)) (arr3 (nat 1) (nat 1) (nat 0) (nat 9)) (arr4 (nat 7) (nat 4) (nat 2) (nat 2)) (arr5 (nat 3) (nat 4) (nat 2) (nat 1))) 100 80 8 'run)) (defn computer-move (state wordsize) (if (or (equal (number-with-at-least state 2) 0) (all-zero-bitvp (xor-bvs (nat-to-bv-list state wordsize)))) (replace-value state (max-list state) (sub1 (max-list state))) (smart-move state wordsize))) (disable delay-clock) (defn computer-move-clock (state wordsize) (clock-plus 2 (clock-plus (delay-clock 250) (clock-plus 1 (clock-plus (delay-clock 250) (clock-plus 1 (clock-plus (delay-clock 250) (clock-plus 1 (clock-plus (delay-clock 250) (clock-plus 3 (clock-plus (number-with-at-least-clock 2 (tag-array 'nat state)) (clock-plus 1 (if (equal (number-with-at-least state 2) 0) (clock-plus 3 (clock-plus (max-nat-clock (tag-array 'nat state)) (clock-plus 4 (clock-plus (replace-value-clock (tag-array 'nat state) (list 'nat (max-list state))) 1)))) (clock-plus 3 (clock-plus (nat-to-bv-list-clock (tag-array 'nat state)) (clock-plus 2 (clock-plus (xor-bvs-clock (length state)) (clock-plus 1 (if (all-zero-bitvp (xor-bvs (nat-to-bv-list state wordsize))) (clock-plus 3 (clock-plus (max-nat-clock (tag-array 'nat state)) (clock-plus 4 (clock-plus (replace-value-clock (tag-array 'nat state) (list 'nat (max-list state))) 1)))) (clock-plus 3 (clock-plus (smart-move-clock state wordsize) 1))))))))))))))))))))) (defn computer-move-input-conditionp (p0) (and (not (all-zero-bitvp (untag-array (array (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0))))) (listp (p-ctrl-stk p0)) (at-least-morep (length (p-temp-stk p0)) 3 (p-max-temp-stk-size p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) 25 (p-max-ctrl-stk-size p0)) (lessp 7 (p-word-size p0)) (not (zerop (p-word-size p0))) (not (equal (p-word-size p0) 1)) (equal (cddr (top (p-temp-stk p0))) nil) (equal (cddr (top (cdr (p-temp-stk p0)))) nil) (equal (cddr (top (cddr (p-temp-stk p0)))) nil) (equal (car (top (p-temp-stk p0))) 'addr) (equal (car (top (cdr (p-temp-stk p0)))) 'nat) (lessp (untag (top (cdr (p-temp-stk p0)))) (exp 2 (p-word-size p0))) (not (zerop (untag (top (cdr (p-temp-stk p0)))))) (equal (car (top (cddr (p-temp-stk p0)))) 'addr) (listp (untag (top (p-temp-stk p0)))) (listp (untag (top (cddr (p-temp-stk p0))))) (equal (cdr (untag (top (p-temp-stk p0)))) 0) (equal (cdr (untag (top (cddr (p-temp-stk p0))))) 0) (definedp (car (untag (top (p-temp-stk p0)))) (p-data-segment p0)) (definedp (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0)) (not (equal (car (untag (top (p-temp-stk p0)))) (car (untag (top (cddr (p-temp-stk p0))))))) (nat-list-piton (array (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0)) (p-word-size p0)) (array-pitonp (array (car (untag (top (p-temp-stk p0)))) (p-data-segment p0)) (untag (top (cdr (p-temp-stk p0))))) (equal (length (array (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0))) (untag (top (cdr (p-temp-stk p0))))) (equal (assoc 'delay (p-prog-segment p0)) (delay-program)) (equal (assoc 'computer-move (p-prog-segment p0)) (computer-move-program)) (equal (assoc 'smart-move (p-prog-segment p0)) (smart-move-program)) (equal (assoc 'replace-value (p-prog-segment p0)) (replace-value-program)) (equal (assoc 'max-nat (p-prog-segment p0)) (max-nat-program)) (equal (assoc 'bv-to-nat-list (p-prog-segment p0)) (bv-to-nat-list-program)) (equal (assoc 'nat-to-bv-list (p-prog-segment p0)) (nat-to-bv-list-program)) (equal (assoc 'match-and-xor (p-prog-segment p0)) (match-and-xor-program)) (equal (assoc 'highest-bit (p-prog-segment p0)) (highest-bit-program)) (equal (assoc 'number-with-at-least (p-prog-segment p0)) (number-with-at-least-program)) (equal (assoc 'bv-to-nat (p-prog-segment p0)) (bv-to-nat-program)) (equal (assoc 'nat-to-bv (p-prog-segment p0)) (nat-to-bv-program)) (equal (assoc 'push-1-vector (p-prog-segment p0)) (push-1-vector-program (p-word-size p0))) (equal (assoc 'xor-bvs (p-prog-segment p0)) (xor-bvs-program)))) (prove-lemma numberp-max-list (rewrite) (numberp (max-list x))) (prove-lemma max-0-means (rewrite) (implies (nat-list-piton x s) (equal (equal (max-list (untag-array x)) 0) (all-zero-bitvp (untag-array x))))) (prove-lemma max-list-not-too-big (rewrite) (implies (and (nat-list-piton x s) (not (zerop s))) (and (lessp (max-list (untag-array x)) (exp 2 s)) (equal (lessp (sub1 (max-list (untag-array x))) (exp 2 s)) t)))) (disable delay-clock) (disable *1*delay-clock) (prove-lemma lessp-exp-2-8-hack (rewrite) (implies (and (lessp 7 free) (equal x free) (lessp val 256)) (equal (lessp val (exp 2 x)) t))) (prove-lemma correctness-of-computer-move (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons wa (cons np (cons s temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call computer-move)) (equal state (untag-array (array (car (untag s)) data-segment))) (equal word-size word-size2) (computer-move-input-conditionp p0)) (equal (p (p-state pc ctrl-stk (cons wa (cons np (cons s temp-stk))) prog-segment data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run) (computer-move-clock state word-size2)) (p-state (add1-addr pc) ctrl-stk temp-stk prog-segment (put-assoc (tag-array 'nat (computer-move state word-size)) (car (untag s)) (if (equal (number-with-at-least state 2) 0) data-segment (put-assoc (if (or (all-zero-bitvp (xor-bvs (nat-to-bv-list state word-size))) (lessp (number-with-at-least state 2) 2)) (tag-array 'bitv (nat-to-bv-list state word-size)) (tag-array 'bitv (nat-to-bv-list (computer-move state word-size) word-size))) (car (untag wa)) data-segment))) max-ctrl-stk-size max-temp-stk-size word-size 'run))) ((disable smart-move))) ;;;; ;;;; ;;;; ;;;; ;;;; Having proved the behavior of the programs, we now introduce ;;;; the spec to which we've been writing code. ;;;; ;;;; ;;;; (defn sum (list) (if (listp list) (plus (car list) (sum (cdr list))) 0)) (prove-lemma sum-append (rewrite) (equal (sum (append x y)) (plus (sum x) (sum y)))) ;; returns a list of states that are valid moves from (defn all-valid-moves-helper (old val origval new) (if (zerop val) (if (nlistp new) nil (all-valid-moves-helper (append old (list origval)) (car new) (car new) (cdr new))) (cons (append old (cons (sub1 val) new)) (all-valid-moves-helper old (sub1 val) origval new))) ((ord-lessp (cons (add1 (length new)) (fix val))))) (defn all-valid-moves (x) (all-valid-moves-helper nil (car x) (car x) (cdr x))) (defn max-sum (list) (if (listp list) (if (lessp (sum (car list)) (max-sum (cdr list))) (max-sum (cdr list)) (sum (car list))) 0)) (prove-lemma nat-listp-append (rewrite) (implies (properp x) (equal (nat-listp (append x y) size) (and (nat-listp x size) (nat-listp y size))))) ;(prove-lemma properp-append (rewrite) ; (equal ; (properp (append x y)) ; (properp y))) (enable properp-append) (defn nat-listp-simple (list) (if (listp list) (and (numberp (car list)) (nat-listp-simple (cdr list))) (equal list nil))) (prove-lemma nat-listp-simple-append (rewrite) (implies (properp x) (equal (nat-listp-simple (append x y)) (and (nat-listp-simple x) (nat-listp-simple y))))) (prove-lemma lessp-max-sum-helper nil (implies (and (not (lessp c temp)) (properp x) (nat-listp-simple (append x (cons c y))) (not (all-zero-bitvp (append x (cons c y))))) (lessp (max-sum (all-valid-moves-helper x temp c y)) (sum (append x (cons c y)))))) (prove-lemma lessp-max-sum-all-valid-moves (rewrite) (implies (and (nat-listp-simple s) (not (all-zero-bitvp s))) (equal (lessp (max-sum (all-valid-moves s)) (sum s)) t)) ((use (lessp-max-sum-helper (c (car s)) (temp (car s)) (x nil) (y (cdr s)))))) (prove-lemma lessp-sum-max-sum (rewrite) (not (lessp (max-sum x) (sum (car x))))) (disable all-valid-moves) (defn wsp-measure (state flag) (cons (if flag (add1 (sum state)) (add1 (max-sum state))) (if flag 0 (length state)))) ;; wsp searchs for a successor to the current state on ;; a path to a guaranteed win. ;; if flag ;; state is a nim state - return state if all zeros. ;; Return a successor state not wsp if one exists, f otherwise ;; if not flag ;; state is a list of states - return member of list if it is ;; not wsp, f is no such member. (defn wsp (state flag) (if flag (if (or (all-zero-bitvp state) (not (nat-listp-simple state))) state (wsp (all-valid-moves state) f)) (if (listp state) (if (not (wsp (car state) t)) (car state) (wsp (cdr state) f)) f)) ((ord-lessp (wsp-measure state flag)))) (defn green-statep (state wordsize) (equal (zerop (number-with-at-least state 2)) (all-zero-bitvp (xor-bvs (nat-to-bv-list state wordsize))))) (defn non-green-in-list (list wordsize) (if (listp list) (or (not (green-statep (car list) wordsize)) (non-green-in-list (cdr list) wordsize)) f)) (prove-lemma nat-listp-means-nat-listp-simple (rewrite) (implies (nat-listp x s) (nat-listp-simple x))) (prove-lemma xor-bitv-zero-bit-vector (rewrite) (implies (all-zero-bitvp x) (equal (xor-bitv x y) (make-list-from (length x) (fix-bitv y))))) (prove-lemma fix-bitv-xor-bitv (rewrite) (equal (fix-bitv (xor-bitv x y)) (xor-bitv x y))) (prove-lemma fix-bitv-and-bitv (rewrite) (equal (fix-bitv (and-bitv x y)) (and-bitv x y))) (prove-lemma fix-bitv-xor-bvs (rewrite) (equal (fix-bitv (xor-bvs x)) (xor-bvs x))) (prove-lemma all-zero-bitvp-make-list-from-simple (rewrite) (implies (all-zero-bitvp x) (all-zero-bitvp (make-list-from n x)))) (prove-lemma all-zero-bitvp-xor-bvs-nat-to-bv-list-zeros (rewrite) (implies (all-zero-bitvp x) (all-zero-bitvp (xor-bvs (nat-to-bv-list x s))))) (prove-lemma number-with-at-least-of-all-zeros (rewrite) (implies (all-zero-bitvp x) (equal (number-with-at-least x m) (if (zerop m) (length x) 0)))) (defn nat-listp-listp (list wordsize) (if (listp list) (and (nat-listp (car list) wordsize) (nat-listp-listp (cdr list) wordsize)) t)) (prove-lemma nat-listp-listp-all-valid-moves-helper (rewrite) (implies (and (nat-listp a s) (lessp b (exp 2 s)) (lessp c (exp 2 s)) (numberp b) (numberp c) (nat-listp d s) (properp a)) (nat-listp-listp (all-valid-moves-helper a b c d) s))) (prove-lemma nat-listp-listp-all-valid-moves (rewrite) (implies (nat-listp a s) (nat-listp-listp (all-valid-moves a) s)) ((enable all-valid-moves))) (prove-lemma listp-all-valid-move-helper (rewrite) (implies (nat-listp-simple d) (equal (listp (all-valid-moves-helper a b c d)) (or (not (all-zero-bitvp d)) (not (zerop b)))))) (prove-lemma listp-all-valid-move (rewrite) (implies (nat-listp-simple x) (equal (listp (all-valid-moves x)) (not (all-zero-bitvp x)))) ((enable all-valid-moves))) (prove-lemma number-with-at-least-append (rewrite) (equal (number-with-at-least (append x y) m) (plus (number-with-at-least x m) (number-with-at-least y m)))) (prove-lemma length-xor-bvs2 (rewrite) (implies (bit-vectorsp x s) (equal (length (xor-bvs x)) (if (listp x) (fix s) 0)))) (prove-lemma xor-bitv-xor-bvs-hack (rewrite) (implies (bit-vectorsp z (length y)) (equal (xor-bitv (xor-bitv y (xor-bvs z)) x) (if (listp z) (xor-bitv y (xor-bitv (xor-bvs z) x)) (xor-bitv y x))))) (prove-lemma xor-bitv-fix-bitv (rewrite) (and (equal (xor-bitv (fix-bitv x) y) (xor-bitv x y)) (equal (xor-bitv x (fix-bitv y)) (xor-bitv x y)))) (prove-lemma xor-bvs-append (rewrite) (implies (and (bit-vectorsp x s) (bit-vectorsp y s) (numberp s)) (equal (xor-bvs (append x y)) (if (listp x) (xor-bitv (xor-bvs x) (xor-bvs y)) (xor-bvs y))))) (prove-lemma xor-bvs-append-hack (rewrite) (implies (bit-vectorsp y ws) (equal (xor-bvs (append (nat-to-bv-list a ws) y)) (if (listp a) (xor-bitv (xor-bvs (nat-to-bv-list a ws)) (xor-bvs y)) (xor-bvs y)))) ((use (xor-bvs-append (x (nat-to-bv-list a ws)) (s ws))))) (prove-lemma nat-to-bv-list-append (rewrite) (equal (nat-to-bv-list (append x y) s) (append (nat-to-bv-list x s) (nat-to-bv-list y s)))) (prove-lemma bit-vectorp-nat-to-bv (rewrite) (equal (bit-vectorp (nat-to-bv x s) s2) (equal (fix s) (fix s2)))) (prove-lemma fix-bitv-nat-to-bv (rewrite) (equal (fix-bitv (nat-to-bv x s)) (nat-to-bv x s))) (prove-lemma fix-bitv-zero-bit-vector (rewrite) (equal (fix-bitv (zero-bit-vector x)) (zero-bit-vector x))) (prove-lemma all-zero-bitvp-nat-to-bv (rewrite) (equal (all-zero-bitvp (nat-to-bv x s)) (or (zerop x) (zerop s)))) (prove-lemma all-zero-bitvp-xor-bitv-better (rewrite) (equal (all-zero-bitvp (xor-bitv x y)) (equal (fix-bitv x) (make-list-from (length x) (fix-bitv y))))) (prove-lemma length-xor-bvs-nat-to-bv-list (rewrite) (equal (length (xor-bvs (nat-to-bv-list x s))) (if (listp x) (fix s) 0))) (prove-lemma fix-bitv-make-list-from (rewrite) (equal (fix-bitv (make-list-from s x)) (make-list-from s (fix-bitv x)))) (defn double-sub1-cdr (n1 n2 l) (if (or (zerop n1) (zerop n2)) t (double-sub1-cdr (sub1 n1) (sub1 n2) (cdr l)))) (prove-lemma make-list-from-make-list-from (rewrite) (equal (make-list-from s1 (make-list-from s2 x)) (if (lessp s2 s1) (append (make-list-from s2 x) (zero-bit-vector (difference s1 s2))) (make-list-from s1 x)))) ;(prove-lemma associativity-of-append (rewrite) ; (equal ; (append (append a b) c) ; (append a (append b c)))) (enable associativity-of-append) ;(prove-lemma append-cons (rewrite) ; (equal ; (append (cons a b) c) ; (cons a (append b c)))) (enable append-cons) (prove-lemma properp-xor-bvs (rewrite) (properp (xor-bvs x))) (prove-lemma properp-xor-bitv (rewrite) (properp (xor-bitv x y))) (defn member-number-with-at-least (x min) (if (listp x) (if (not (zerop (number-with-at-least (car x) min))) (car x) (member-number-with-at-least (cdr x) min)) f)) (prove-lemma xor-bvs-nat-to-bv-list-zerop-ws (rewrite) (implies (zerop ws) (equal (xor-bvs (nat-to-bv-list x ws)) nil))) (defn nat-listp-listp-simple (x) (if (listp x) (and (nat-listp-simple (car x)) (nat-listp-listp-simple (cdr x))) (equal x nil))) (prove-lemma non-green-in-list-zerop-ws (rewrite) (implies (and (zerop ws) (nat-listp-listp-simple x)) (iff (non-green-in-list x ws) (member-number-with-at-least x 2)))) (prove-lemma nat-listp-listp-simple-means-properp (rewrite) (implies (nat-listp-listp-simple x) (properp x))) (prove-lemma nat-listp-simple-means-properp (rewrite) (implies (nat-listp-simple x) (properp x))) (prove-lemma make-list-from-xor-bvs-nat-to-bv-list (rewrite) (implies (equal (fix ws) (fix s)) (equal (make-list-from ws (xor-bvs (nat-to-bv-list x s))) (if (listp x) (xor-bvs (nat-to-bv-list x s)) (zero-bit-vector ws))))) (prove-lemma last-xor-bitv (rewrite) (equal (last (xor-bitv x y)) (if (listp x) (xor-bit (last x) (nth (sub1 (length x)) y)) 0))) (prove-lemma last-one-bit-vector (rewrite) (equal (last (one-bit-vector x)) 1)) (prove-lemma nth-as-last (rewrite) (implies (equal (add1 n) (length x)) (equal (nth n x) (last x)))) (prove-lemma listp-nat-to-bv (rewrite) (equal (listp (nat-to-bv x s)) (not (zerop s)))) ;(prove-lemma remainder-plus-x-x-2 (rewrite) ; (equal (remainder (plus x x) 2) 0)) (enable remainder-plus-x-x-2) (prove-lemma last-nat-to-bv (rewrite) (equal (last (nat-to-bv x s)) (if (or (zerop s) (and (lessp x (exp 2 s)) (equal (remainder x 2) 0))) 0 1))) (prove-lemma fix-bitv-one-bit-vector (rewrite) (equal (fix-bitv (one-bit-vector x)) (one-bit-vector x))) (prove-lemma nat-to-bv-1 (rewrite) (equal (nat-to-bv 1 x) (if (zerop x) nil (one-bit-vector x)))) (prove-lemma last-zero-bit-vector (rewrite) (equal (last (zero-bit-vector x)) 0)) (prove-lemma nat-to-bv-2 (rewrite) (equal (nat-to-bv x 2) (if (zerop x) (list 0 0) (if (equal x 1) (list 0 1) (if (equal x 2) (list 1 0) (list 1 1))))) ((expand (nat-to-bv x 2)))) (prove-lemma all-zero-bitvp-all-but-last-nat-to-bv (rewrite) (equal (all-zero-bitvp (all-but-last (nat-to-bv x s))) (or (lessp x 2) (lessp s 2)))) (prove-lemma xor-bvs-of-list-of-0s-and-1s (rewrite) (implies (zerop (number-with-at-least c 2)) (equal (xor-bvs (nat-to-bv-list c ws)) (if (or (nlistp c) (zerop ws)) nil (if (equal (remainder (sum c) 2) 0) (zero-bit-vector ws) (one-bit-vector ws)))))) (prove-lemma equal-nat-to-bv-nlistp (rewrite) (implies (nlistp x) (equal (equal x (nat-to-bv y s)) (and (equal x nil) (zerop s))))) (prove-lemma different-lengths-means-different-hack nil (implies (not (equal (fix s1) (fix s2))) (not (equal (length (nat-to-bv x s1)) (length (nat-to-bv y s2)))))) (prove-lemma different-lengths-means-different (rewrite) (implies (not (equal (fix s1) (fix s2))) (not (equal (nat-to-bv x s1) (nat-to-bv y s2)))) ((use (different-lengths-means-different-hack)) (disable-theory t) (enable-theory ground-zero))) (defn nat-to-bv-induct (x y s1 s2) (if (zerop s1) t (nat-to-bv-induct (if (lessp x (exp 2 (sub1 s1))) x (difference x (exp 2 (sub1 s1)))) (if (lessp y (exp 2 (sub1 s2))) y (difference y (exp 2 (sub1 s2)) )) (sub1 s1) (sub1 s2)))) (defn all-ones-vector (x) (if (zerop x) nil (cons 1 (all-ones-vector (sub1 x))))) (prove-lemma not-lessp-exp-means-all-ones (rewrite) (implies (not (lessp x (sub1 (exp 2 s)))) (equal (nat-to-bv x s) (all-ones-vector s)))) (prove-lemma lessp-sub1-plus-sub1-hack (rewrite) (implies (not (zerop y)) (equal (lessp (sub1 (plus x y)) (plus (sub1 y) z)) (lessp x z)))) (prove-lemma equal-cons-zero-bit-vector-nat-to-bv (rewrite) (equal (equal (cons 0 (zero-bit-vector x)) (nat-to-bv a b)) (and (equal (add1 x) (fix b)) (zerop a)))) (prove-lemma equal-all-ones-vector-all-ones-vector (rewrite) (equal (equal (all-ones-vector x) (all-ones-vector y)) (equal (fix x) (fix y))) ((induct (double-sub1-cdr x y l)))) (prove-lemma equal-all-ones-vector-cons (rewrite) (equal (equal (all-ones-vector x) (cons a b)) (and (not (zerop x)) (equal a 1) (equal (all-ones-vector (sub1 x)) b)))) (prove-lemma different-lengths-obvious nil (implies (equal x y) (equal (length x) (length y)))) (prove-lemma equal-all-ones-vector-nlistp (rewrite) (implies (nlistp x) (equal (equal (all-ones-vector y) x) (and (equal x nil) (zerop y))))) (prove-lemma length-all-ones-vector (rewrite) (equal (length (all-ones-vector x)) (fix x))) (prove-lemma different-lengths-hack (rewrite) (implies (not (equal (fix x) (fix y))) (not (equal (all-ones-vector x) (nat-to-bv a y)))) ((use (different-lengths-obvious (x (all-ones-vector x)) (y (nat-to-bv a y)))) (disable equal-all-ones-vector-nlistp))) (prove-lemma lessp-difference-arg1 (rewrite) (implies (not (lessp x y)) (equal (lessp (difference x y) z) (lessp x (plus y z))))) (prove-lemma equal-difference (rewrite) (implies (not (lessp x y)) (equal (equal (difference x y) z) (and (equal (fix x) (plus y z)) (numberp z))))) (prove-lemma equal-exp (rewrite) (implies (equal (fix a) (fix b)) (equal (equal (exp a c) (exp b d)) (or (equal a 1) (and (zerop a) (equal (zerop c) (zerop d))) (equal (fix c) (fix d))))) ((induct (double-sub1-cdr c d l)))) (prove-lemma equal-all-ones-nat-to-bv (rewrite) (equal (equal (all-ones-vector x) (nat-to-bv a b)) (and (equal (fix x) (fix b)) (not (lessp a (sub1 (exp 2 b)))))) ((induct (nat-to-bv-induct q a x b)))) (prove-lemma equal-nat-to-bv-nat-to-bv (rewrite) (equal (equal (nat-to-bv x s1) (nat-to-bv y s2)) (and (equal (fix s1) (fix s2)) (or (equal (fix x) (fix y)) (and (not (lessp x (sub1 (exp 2 s1)))) (not (lessp y (sub1 (exp 2 s1)))))))) ((induct (nat-to-bv-induct x y s1 s2)))) (prove-lemma listp-xor-bvs (rewrite) (equal (listp (xor-bvs x)) (listp (car x)))) (prove-lemma car-nat-to-bv-list (rewrite) (equal (car (nat-to-bv-list x s)) (if (listp x) (nat-to-bv (car x) s) 0))) ;; from later version of naturals that is used in this proof (PROVE-LEMMA QUOTIENT-DIFFERENCE (REWRITE) (EQUAL (QUOTIENT (DIFFERENCE X Y) Z) (IF (LESSP (REMAINDER X Z) (REMAINDER Y Z)) (SUB1 (DIFFERENCE (QUOTIENT X Z) (QUOTIENT Y Z))) (DIFFERENCE (QUOTIENT X Z) (QUOTIENT Y Z)))) ((DISABLE QUOTIENT-DIFFERENCE1 QUOTIENT-DIFFERENCE2 QUOTIENT-DIFFERENCE3) (INDUCT (QUOTIENT Y Z)))) (enable DIFFERENCE-X-SUB1-X) (prove-lemma all-but-last-nat-to-bv (rewrite) (equal (all-but-last (nat-to-bv x s)) (if (zerop s) nil (nat-to-bv (quotient x 2) (sub1 s))))) (prove-lemma equal-last-xor-bvs-1 (rewrite) (equal (equal (last (xor-bvs x)) 1) (not (equal (last (xor-bvs x)) 0)))) (prove-lemma not-green-state-means (rewrite) (implies (and (not (green-statep (append a (cons b c)) ws)) (lessp d (exp 2 ws)) (lessp b d)) (equal (green-statep (append a (cons d c)) ws) (or (not (zerop ws)) (zerop (number-with-at-least (append a (cons d c)) 2)))))) (prove-lemma green-in-list-all-valid-moves-helper nil (implies (and (nat-listp a ws) (nat-listp d ws) (numberp c) (lessp c (exp 2 ws)) (properp a) (non-green-in-list (all-valid-moves-helper a b c d) ws) (not (lessp c b)) (numberp b)) (green-statep (append a (cons c d)) ws)) ((disable green-statep))) (prove-lemma green-in-list-all-valid-moves-means (rewrite) (implies (and (nat-listp x ws) (non-green-in-list (all-valid-moves x) ws)) (green-statep x ws)) ((disable green-statep) (enable all-valid-moves) (use (green-in-list-all-valid-moves-helper (a nil) (b (car x)) (c (car x)) (d (cdr x)))))) (defn valid-movep (s1 s2) (if (and (listp s1) (listp s2)) (or (and (lessp (car s2) (car s1)) (numberp (car s2)) (equal (cdr s1) (cdr s2))) (and (equal (car s1) (car s2)) (valid-movep (cdr s1) (cdr s2)))) f)) (defn match-member (m list) (if (listp list) (if (not (all-zero-bitvp (and-bitv (car list) m))) (car list) (match-member m (cdr list))) f)) (prove-lemma xor-bvs-match-and-xor (rewrite) (implies (bit-vectorsp list (length value)) (equal (xor-bvs (match-and-xor list match value)) (if (match-member match list) (xor-bitv value (xor-bvs list)) (xor-bvs list))))) (defn remove-highest-bits (x) (if (listp x) (cons (cdar x) (remove-highest-bits (cdr x))) nil)) (prove-lemma car-remove-highest-bits (rewrite) (equal (car (remove-highest-bits x)) (cdr (car x)))) (prove-lemma equal-car-highest-bit-1 (rewrite) (equal (equal (car (highest-bit x)) 1) (equal (highest-bit x) (cons 1 (zero-bit-vector (sub1 (length x))))))) (prove-lemma car-xor-bitv (rewrite) (equal (car (xor-bitv x y)) (if (listp x) (xor-bit (car x) (car y)) 0))) (prove-lemma match-member-cons-0 (rewrite) (iff (match-member (cons 0 x) y) (match-member x (remove-highest-bits y)))) (prove-lemma match-member-cons (rewrite) (implies (and (bit-vectorsp v (length (cons a b))) (not (equal (car (xor-bvs v)) 0))) (iff (match-member (cons a b) v) (or (not (equal a 0)) (match-member b (remove-highest-bits v)))))) (prove-lemma equal-highest-bit-cons-1 (rewrite) (equal (equal (highest-bit x) (cons 1 y)) (and (not (equal (car x) 0)) (equal y (zero-bit-vector (sub1 (length x))))))) (prove-lemma length-cdr-xor-bitv (rewrite) (equal (length (cdr (xor-bitv x y))) (length (cdr x)))) (prove-lemma length-fix-bitv (rewrite) (equal (length (fix-bitv x)) (length x))) (prove-lemma length-cdr-xor-bvs (rewrite) (implies (bit-vectorsp x s) (equal (length (cdr (xor-bvs x))) (if (listp x) (sub1 s) 0)))) (defn highest-bits-induct (x s) (if (listp x) (if (listp (car x)) (if (equal (car (highest-bit (xor-bvs x))) 1) t (highest-bits-induct (remove-highest-bits x) (sub1 s))) t) t) ((lessp (length (car x))))) (prove-lemma bit-vectorsp-remove-highest-bits (rewrite) (implies (bit-vectorsp x (add1 s)) (bit-vectorsp (remove-highest-bits x) s))) (prove-lemma xor-bvs-remove-highest-bits (rewrite) (implies (bit-vectorsp x s) (equal (xor-bvs (remove-highest-bits x)) (if (and (listp x) (not (zerop s))) (cdr (xor-bvs x)) nil)))) (prove-lemma match-member-highest-bit-xor-bvs nil (implies (bit-vectorsp x s) (iff (match-member (highest-bit (xor-bvs x)) x) (not (all-zero-bitvp (xor-bvs x))))) ((induct (highest-bits-induct x s)))) (prove-lemma match-member-highest-bit-xor-bvs-rewrite (rewrite) (implies (bit-vectorsp x (length (xor-bvs x))) (iff (match-member (highest-bit (xor-bvs x)) x) (not (all-zero-bitvp (xor-bvs x))))) ((use (match-member-highest-bit-xor-bvs (s (length (xor-bvs x))))))) (prove-lemma bit-vectorsp-nat-to-bv-list-better (rewrite) (equal (bit-vectorsp (nat-to-bv-list x size) size2) (or (nlistp x) (equal (fix size) (fix size2))))) (prove-lemma match-member-at-least-min-means (rewrite) (implies (and (match-member y (nat-to-bv-list x ws)) (not (lessp (bv-to-nat (match-member y (nat-to-bv-list x ws))) min))) (not (equal (number-with-at-least x min) 0)))) (prove-lemma bit-vectorp-highest-bit-xor-bvs (rewrite) (equal (bit-vectorp (highest-bit (xor-bvs x)) ws) (bit-vectorp (xor-bvs x) ws))) (prove-lemma number-with-at-least-match-and-xor (rewrite) (implies (and (nat-listp x ws) (bit-vectorp y ws) (bit-vectorp z ws)) (equal (number-with-at-least (bv-to-nat-list (match-and-xor (nat-to-bv-list x ws) y z)) min) (if (match-member y (nat-to-bv-list x ws)) (difference (plus (number-with-at-least x min) (if (lessp (bv-to-nat (xor-bitv z (match-member y (nat-to-bv-list x ws)))) min) 0 1)) (if (lessp (bv-to-nat (match-member y (nat-to-bv-list x ws))) min) 0 1)) (number-with-at-least x min))))) (prove-lemma number-with-at-least-replace-value (rewrite) (equal (number-with-at-least (replace-value x e v) min) (if (member e x) (difference (plus (number-with-at-least x min) (if (lessp v min) 0 1)) (if (lessp e min) 0 1)) (number-with-at-least x min)))) (prove-lemma max-list-means-number-0 (rewrite) (implies (and (equal (max-list x) n) (lessp n m)) (equal (number-with-at-least x m) 0))) (prove-lemma member-max-list (rewrite) (implies (nat-listp-simple x) (equal (member (max-list x) x) (listp x)))) (prove-lemma listp-replace-value (rewrite) (equal (listp (replace-value x e v)) (listp x))) (prove-lemma member-means-lessp-sum (rewrite) (implies (member e x) (not (lessp (sum x) e)))) (prove-lemma sum-replace-value (rewrite) (equal (sum (replace-value x e v)) (if (member e x) (difference (plus (sum x) v) e) (sum x)))) (prove-lemma remainder-difference-2 (rewrite) (equal (remainder (difference x y) 2) (if (lessp x y) 0 (if (equal (remainder x 2) (remainder y 2)) 0 1)))) (prove-lemma lessp-max-list (rewrite) (not (lessp (sum x) (max-list x)))) (prove-lemma remainder-plus-remainder (rewrite) (and (equal (remainder (plus (remainder x y) z) y) (remainder (plus x z) y)) (equal (remainder (plus z (remainder x y)) y) (remainder (plus x z) y)))) (prove-lemma remainder-plus-remainder2 (rewrite) (and (equal (remainder (plus z (plus a (remainder x y))) y) (remainder (plus z (plus a x)) y)) (equal (remainder (plus z (plus (remainder x y) a)) y) (remainder (plus z (plus a x)) y))) ((use (remainder-plus-remainder (z (plus z a)))) (disable remainder-plus-remainder))) (prove-lemma lessp-max-list-from-number-with-at-least (rewrite) (implies (and (equal (number-with-at-least x m) 0) (not (zerop m))) (lessp (max-list x) m))) (prove-lemma number-with-at-least-as-sum (rewrite) (implies (zerop (number-with-at-least x 2)) (equal (number-with-at-least x 1) (sum x)))) (prove-lemma equal-remainder-add1-2 (rewrite) (equal (equal (remainder (add1 x) 2) (remainder (add1 y) 2)) (equal (remainder x 2) (remainder y 2)))) (prove-lemma remainder-plus-sum-number-hack (rewrite) (implies (equal (number-with-at-least x 2) 1) (equal (remainder (plus (sum x) (number-with-at-least x 1)) 2) (remainder (add1 (max-list x)) 2)))) (prove-lemma equal-remainder-add1 (rewrite) (equal (equal (remainder (add1 x) y) (remainder x y)) (equal y 1))) (prove-lemma max-0-means-sum-0 (rewrite) (equal (equal (sum x) 0) (equal (max-list x) 0))) (prove-lemma max-0-means-all-zero-bitvp (rewrite) (implies (and (equal (max-list x) 0) (nat-listp-simple x)) (all-zero-bitvp x))) (prove-lemma remainder-add1-2 (rewrite) (and (equal (equal (remainder (add1 x) 2) 0) (equal (remainder x 2) 1)) (equal (equal (remainder (add1 x) 2) 1) (equal (remainder x 2) 0)))) (prove-lemma remainder-sub1-2 (rewrite) (implies (not (zerop x)) (and (equal (equal (remainder (sub1 x) 2) 0) (equal (remainder x 2) 1)) (equal (equal (remainder (sub1 x) 2) 1) (equal (remainder x 2) 0))))) (prove-lemma equal-x-remainder-sub1-x (rewrite) (equal (equal (remainder (sub1 x) y) x) (equal x 0))) (prove-lemma computer-move-makes-non-green nil (implies (and (green-statep x ws) (nat-listp x ws) (listp x) (not (zerop ws)) (not (all-zero-bitvp x))) (not (green-statep (computer-move x ws) ws))) ((disable nat-to-bv bv-to-nat lessp-number-with-at-least))) (prove-lemma nat-listp-simplify (rewrite) (implies (zerop ws) (equal (nat-listp x ws) (and (properp x) (all-zero-bitvp x))))) (prove-lemma computer-move-makes-non-green-rewrite (rewrite) (implies (and (green-statep x ws) (nat-listp x ws) (not (all-zero-bitvp x))) (not (green-statep (computer-move x ws) ws))) ((use (computer-move-makes-non-green)) (disable-theory t) (enable nat-listp all-zero-bitvp nat-listp-simplify) (enable-theory ground-zero))) (defn make-properp (x) (if (listp x) (cons (car x) (make-properp (cdr x))) nil)) (prove-lemma properp-make-properp (rewrite) (implies (properp x) (equal (make-properp x) x))) (prove-lemma replace-value-simplify (rewrite) (implies (not (member x y)) (equal (replace-value y x z) (make-properp y)))) (prove-lemma member-make-properp (rewrite) (equal (member x (make-properp y)) (member x y))) (prove-lemma valid-movep-x-x (rewrite) (not (valid-movep x x))) (prove-lemma valid-movep-replace-value (rewrite) (implies (properp x) (equal (valid-movep x (replace-value x y z)) (and (member y x) (lessp z y) (numberp z))))) (prove-lemma number-with-at-least-max-list (rewrite) (implies (and (equal (number-with-at-least x m) v) (lessp 0 v)) (not (lessp (max-list x) m)))) (prove-lemma valid-movep-match-and-xor (rewrite) (implies (and (nat-listp x ws) (bit-vectorp y ws) (bit-vectorp z ws)) (equal (valid-movep x (bv-to-nat-list (match-and-xor (nat-to-bv-list x ws) y z))) (and (match-member y (nat-to-bv-list x ws)) (lessp (bv-to-nat (xor-bitv z (match-member y (nat-to-bv-list x ws)))) (bv-to-nat (match-member y (nat-to-bv-list x ws))))))) ((induct (length x)))) (defn lessp-bv (x y) (if (and (listp x) (listp y)) (if (equal (fix-bit (car x)) (fix-bit (car y))) (lessp-bv (cdr x) (cdr y)) (equal (car x) 0)) f)) (prove-lemma lessp-bv-to-nat (rewrite) (lessp (bv-to-nat x) (exp 2 (length x)))) (prove-lemma lessp-as-lessp-bv (rewrite) (implies (equal (length x) (length y)) (equal (lessp (bv-to-nat x) (bv-to-nat y)) (lessp-bv x y)))) (prove-lemma fix-bitv-highest-bit (rewrite) (equal (fix-bitv (highest-bit x)) (highest-bit x))) (prove-lemma properp-highest-bit (rewrite) (properp (highest-bit x))) (prove-lemma bit-vectorp-fix-bitv (rewrite) (equal (bit-vectorp (fix-bitv x) s) (equal (length x) (fix s)))) (prove-lemma lessp-bv-xor-bitv (rewrite) (implies (equal (length x) (length y)) (equal (lessp-bv (xor-bitv x y) y) (not (all-zero-bitvp (and-bitv y (highest-bit x))))))) (prove-lemma length-match-member-nat-to-bv-list (rewrite) (equal (length (match-member a (nat-to-bv-list x ws))) (if (match-member a (nat-to-bv-list x ws)) (fix ws) 0))) (prove-lemma bit-vectorsp-remove-highest-bits2 (rewrite) (implies (bit-vectorsp x s1) (equal (bit-vectorsp (remove-highest-bits x) s2) (or (equal (add1 s2) s1) (not (listp x)))))) (prove-lemma match-member-high-bit-xor-bvs-helper nil (implies (bit-vectorsp x ws) (iff (match-member (highest-bit (xor-bvs x)) x) (not (all-zero-bitvp (xor-bvs x))))) ((induct (highest-bits-induct x ws)))) (prove-lemma match-member-high-bit-xor-bvs (rewrite) (iff (match-member (highest-bit (xor-bvs (nat-to-bv-list y ws))) (nat-to-bv-list y ws)) (not (all-zero-bitvp (xor-bvs (nat-to-bv-list y ws))))) ((use (match-member-high-bit-xor-bvs-helper (x (nat-to-bv-list y ws)))) (disable-theory t) (enable-theory ground-zero) (enable bit-vectorsp-nat-to-bv-list-better))) (prove-lemma length-match-member (rewrite) (implies (match-member a (nat-to-bv-list x ws)) (equal (length (match-member a (nat-to-bv-list x ws))) (fix ws)))) (prove-lemma all-zero-bitvp-and-match-member (rewrite) (implies (bit-vectorsp b (length a)) (equal (all-zero-bitvp (and-bitv a (match-member a b))) (not (match-member a b)))) ((induct (match-member a b)))) (prove-lemma valid-movep-computer-move-helper nil (implies (and (nat-listp x ws) (not (all-zero-bitvp x)) (not (zerop ws)) (listp x)) (valid-movep x (computer-move x ws))) ((disable all-zero-bitvp nat-to-bv bv-to-nat-list match-and-xor))) ;;; PART OF SPECIFICATION (prove-lemma valid-movep-computer-move (rewrite) (implies (and (nat-listp x ws) (not (all-zero-bitvp x))) (valid-movep x (computer-move x ws))) ((use (valid-movep-computer-move-helper)) (disable-theory t) (enable-theory ground-zero) (enable nat-listp-simplify all-zero-bitvp))) (prove-lemma nthcdr-cdr (rewrite) (equal (nthcdr n (cdr x)) (cdr (nthcdr n x)))) (prove-lemma make-list-from-append (rewrite) (equal (make-list-from n (append a b)) (if (lessp (length a) n) (append a (make-list-from (difference n (length a)) b)) (make-list-from n a)))) (prove-lemma make-list-from-simplify-better (rewrite) (implies (equal n (length x)) (equal (make-list-from n x) (make-properp x)))) ;(prove-lemma length-cons (rewrite) ; (equal (length (cons a b)) (add1 (length b)))) (enable length-cons) (prove-lemma cdr-nthcdr-cons (rewrite) (equal (cdr (nthcdr n (cons a b))) (nthcdr n b))) (prove-lemma equal-append-2 (rewrite) (equal (equal x (append a b)) (and (not (lessp (length x) (length a))) (equal (make-list-from (length a) x) (make-properp a)) (equal (nthcdr (length a) x) b))) ((induct (double-cdr-induct x a)) (disable length))) (prove-lemma member-cons-all-valid-moves-helper1 (rewrite) (implies (listp a) (equal (member (cons x y) (all-valid-moves-helper a b c d)) (and (equal x (car a)) (member y (all-valid-moves-helper (cdr a) b c d)))))) (prove-lemma member-all-valid-moves-means-prefix (rewrite) (implies (properp a) (implies (member x (all-valid-moves-helper a b c d)) (equal (make-list-from (length a) x) a)))) (prove-lemma equal-nthcdr-cons (rewrite) (implies (not (lessp n (length x))) (not (equal (nthcdr n x) (cons a b))))) (prove-lemma lessp-length-simple-member-all-valid-moves (rewrite) (implies (not (lessp (length a) (length x))) (not (member x (all-valid-moves-helper a b c d))))) (prove-lemma nth-cons (rewrite) (equal (nth n (cons a b)) (if (zerop n) a (nth (sub1 n) b)))) (prove-lemma nth-1 (rewrite) (equal (nth 1 x) (cadr x))) (prove-lemma get-as-nth (rewrite) (equal (get n x) (nth n x))) (prove-lemma equal-cons-make-properp (rewrite) (equal (equal (cons a b) (make-properp x)) (and (listp x) (equal a (car x)) (equal b (make-properp (cdr x)))))) (prove-lemma nthcdr-cons-make-list-from-hack (rewrite) (equal (nthcdr n (cons a (make-list-from n z))) (if (zerop n) (list a) (list (nth (sub1 n) z))))) (prove-lemma lessp-sub1-as-equal (rewrite) (implies (lessp a b) (equal (lessp a (sub1 b)) (not (equal (add1 a) b))))) (prove-lemma equal-nthcdr-cons-better (rewrite) (equal (equal (nthcdr n x) (cons a b)) (and (lessp n (length x)) (equal (nth n x) a) (equal (nthcdr (add1 n) x) b)))) (prove-lemma member-all-valid-moves-helper (rewrite) (implies (and (nat-listp-simple a) (nat-listp-simple d) (numberp b) (numberp c)) (equal (member x (all-valid-moves-helper a b c d)) (and (equal (make-list-from (length a) x) (make-properp a)) (or (and (lessp (nth (length a) x) b) (numberp (nth (length a) x)) (equal (nthcdr (add1 (length a)) x) d)) (and (equal (nth (length a) x) c) (valid-movep d (cdr (nthcdr (length a) x))))))))) (prove-lemma member-all-valid-moves (rewrite) (implies (nat-listp-simple x) (equal (member y (all-valid-moves x)) (valid-movep x y))) ((enable all-valid-moves))) (prove-lemma valid-movep-and-makes-nongreen-means (rewrite) (implies (and (member x y) (not (green-statep x ws))) (non-green-in-list y ws)) ((disable green-statep))) (prove-lemma green-means-non-green-in-valid-moves (rewrite) (implies (and (nat-listp s ws) (not (all-zero-bitvp s)) (green-statep s ws)) (non-green-in-list (all-valid-moves s) ws)) ((use (valid-movep-and-makes-nongreen-means (x (computer-move s ws)) (y (all-valid-moves s)))) (disable green-statep computer-move))) (prove-lemma green-in-list-all-valid-moves (rewrite) (implies (and (nat-listp s ws) (not (all-zero-bitvp s))) (iff (non-green-in-list (all-valid-moves s) ws) (green-statep s ws))) ((disable green-statep))) (prove-lemma sum-when-all-zero (rewrite) (implies (all-zero-bitvp x) (equal (sum x) 0))) (prove-lemma green-statep-all-zero-bitvp (rewrite) (implies (all-zero-bitvp x) (green-statep x s))) (prove-lemma wsp-green-state-proof nil (implies (and (or (and flag (nat-listp s wordsize)) (and (not flag) (nat-listp-listp s wordsize))) (listp s)) (iff (wsp s flag) (if flag (green-statep s wordsize) (non-green-in-list s wordsize)))) ((disable green-statep))) (prove-lemma wsp-green-state (rewrite) (implies (nat-listp s wordsize) (iff (wsp s t) (green-statep s wordsize))) ((use (wsp-green-state-proof (flag t))) (disable green-statep))) (prove-lemma nat-listp-replace-value (rewrite) (implies (and (nat-listp s ws) (lessp new (exp 2 ws)) (numberp new)) (nat-listp (replace-value s y new) ws))) (prove-lemma nat-listp-bv-to-nat-list (rewrite) (implies (bit-vectorsp x s) (nat-listp (bv-to-nat-list x) s))) (prove-lemma nat-listp-smart-move nil (implies (and (nat-listp s ws) (not (zerop ws))) (nat-listp (smart-move s ws) ws)) ((disable-theory t) (enable-theory ground-zero naturals) (enable smart-move bit-vectorsp-nat-to-bv-list-better nat-listp-replace-value nat-listp-bv-to-nat-list lessp-exp-simple lessp-remainder-x-exp-x) (use (bit-vectorsp-match-and-xor (size ws) (x (nat-to-bv-list s ws)) (y (highest-bit (xor-bvs (nat-to-bv-list s ws)))) (z (xor-bvs (nat-to-bv-list s ws))))))) (prove-lemma all-zero-bitvp-max-list (rewrite) (implies (all-zero-bitvp s) (equal (max-list s) 0))) (prove-lemma replace-value-x-x (rewrite) (implies (properp x) (equal (replace-value x y y) x))) (prove-lemma smart-move-small-ws (rewrite) (implies (and (nat-listp s ws) (zerop ws)) (equal (smart-move s ws) s))) (prove-lemma lessp-max-list-from-nat-listp (rewrite) (implies (nat-listp s ws) (lessp (max-list s) (exp 2 ws)))) (prove-lemma nat-listp-computer-move (rewrite) (implies (nat-listp s ws) (nat-listp (computer-move s ws) ws)) ((use (nat-listp-smart-move)) (disable-theory t) (enable-theory ground-zero) (enable lessp-max-list-from-nat-listp smart-move-small-ws computer-move nat-listp-replace-value))) ;; PART OF SPECIFICATION (prove-lemma computer-move-works (rewrite) (implies (and (nat-listp state ws) (not (all-zero-bitvp state)) (wsp state t)) (not (wsp (computer-move state ws) t))) ((disable computer-move green-statep nat-listp-computer-move) (use (nat-listp-computer-move (s state))))) (defn nim-piton-ctrl-stk-requirement () 25) (defn nim-piton-temp-stk-requirement () 3) (defn computer-move-implemented-input-conditionp (p0) (and (listp (p-ctrl-stk p0)) (lessp 7 (p-word-size p0)) (lessp 1 (p-word-size p0)) ; useful to prover, but subsumed ;; there is some room on the stacks (at-least-morep (length (p-temp-stk p0)) (nim-piton-temp-stk-requirement) (p-max-temp-stk-size p0)) (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0)) (nim-piton-ctrl-stk-requirement) (p-max-ctrl-stk-size p0)) ;; the third thing on the stack is an address to the state array (equal (car (top (cddr (p-temp-stk p0)))) 'addr) (equal (cddr (top (cddr (p-temp-stk p0)))) nil) (listp (untag (top (cddr (p-temp-stk p0))))) (equal (cdr (untag (top (cddr (p-temp-stk p0))))) 0) (definedp (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0)) (nat-list-piton (array (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0)) (p-word-size p0)) ;; the second thing on the stack is the length of the state (equal (car (top (cdr (p-temp-stk p0)))) 'nat) (equal (cddr (top (cdr (p-temp-stk p0)))) nil) (equal (length (array (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0))) (untag (top (cdr (p-temp-stk p0))))) (lessp (untag (top (cdr (p-temp-stk p0)))) (exp 2 (p-word-size p0))) (not (zerop (untag (top (cdr (p-temp-stk p0)))))) ;; the top thing on the stack is a pointer to an array ;; that is the same size as the state array but distinct (equal (car (top (p-temp-stk p0))) 'addr) (equal (cddr (top (p-temp-stk p0))) nil) (listp (untag (top (p-temp-stk p0)))) (equal (cdr (untag (top (p-temp-stk p0)))) 0) (definedp (car (untag (top (p-temp-stk p0)))) (p-data-segment p0)) (array-pitonp (array (car (untag (top (p-temp-stk p0)))) (p-data-segment p0)) (untag (top (cdr (p-temp-stk p0))))) (not (equal (car (untag (top (p-temp-stk p0)))) (car (untag (top (cddr (p-temp-stk p0))))))) ;; at least one pile has one match (not (all-zero-bitvp (untag-array (array (car (untag (top (cddr (p-temp-stk p0))))) (p-data-segment p0))))))) ;; cm-prog is the Nim program. It may be disappointing to see that it is ;; a function of one argument rather than a constant, as programs ought to ;; be. This is because we wish to use bit vectors in our program, and ;; because of a weakness in the Piton design there is no way to push ;; a bit-vector on the stack without knowing the word-size. The only ;; subprogram that uses the word-size is push-1-vector, which is a ;; one-line program that pushes a one-vector onto the stack. (defn cm-prog (word-size) (list (xor-bvs-program) (push-1-vector-program word-size) (nat-to-bv-program) (bv-to-nat-program) (number-with-at-least-program) (highest-bit-program) (match-and-xor-program) (nat-to-bv-list-program) (bv-to-nat-list-program) (max-nat-program) (replace-value-program) (smart-move-program) (delay-program) (computer-move-program))) (disable computer-move-program) (disable *1*computer-move-program) (prove-lemma car-xor-bvs-program (rewrite) (equal (car (xor-bvs-program)) 'xor-bvs) ((enable xor-bvs-program))) (prove-lemma car-push-1-vector-program (rewrite) (equal (car (push-1-vector-program word-size)) 'push-1-vector) ((enable push-1-vector-program))) (prove-lemma car-nat-to-bv-program (rewrite) (equal (car (nat-to-bv-program)) 'nat-to-bv) ((enable nat-to-bv-program))) (prove-lemma car-bv-to-nat-program (rewrite) (equal (car (bv-to-nat-program)) 'bv-to-nat) ((enable bv-to-nat-program))) (prove-lemma car-number-with-at-least-program (rewrite) (equal (car (number-with-at-least-program)) 'number-with-at-least) ((enable number-with-at-least-program))) (prove-lemma car-highest-bit-program (rewrite) (equal (car (highest-bit-program)) 'highest-bit) ((enable highest-bit-program))) (prove-lemma car-match-and-xor-program (rewrite) (equal (car (match-and-xor-program)) 'match-and-xor) ((enable match-and-xor-program))) (prove-lemma car-nat-to-bv-list-program (rewrite) (equal (car (nat-to-bv-list-program)) 'nat-to-bv-list) ((enable nat-to-bv-list-program))) (prove-lemma car-bv-to-nat-list-program (rewrite) (equal (car (bv-to-nat-list-program)) 'bv-to-nat-list) ((enable bv-to-nat-list-program))) (prove-lemma car-max-nat-program (rewrite) (equal (car (max-nat-program)) 'max-nat) ((enable max-nat-program))) (prove-lemma car-replace-value-program (rewrite) (equal (car (replace-value-program)) 'replace-value) ((enable replace-value-program))) (prove-lemma car-smart-move-program (rewrite) (equal (car (smart-move-program)) 'smart-move) ((enable smart-move-program))) (prove-lemma car-delay-program (rewrite) (equal (car (delay-program)) 'delay)) (disable delay-program) (prove-lemma car-computer-move-program (rewrite) (equal (car (computer-move-program)) 'computer-move) ((enable computer-move-program))) (prove-lemma equal-untag-array-tag-array-x-x (rewrite) (equal (equal (untag-array (tag-array l x)) x) (properp x))) (prove-lemma properp-replace-value (rewrite) (implies (properp x) (properp (replace-value x y z)))) (prove-lemma properp-bv-to-nat-list (rewrite) (properp (bv-to-nat-list x))) (prove-lemma properp-nat-to-bv-list (rewrite) (properp (nat-to-bv-list x ws))) (prove-lemma properp-computer-move (rewrite) (implies (properp x) (properp (computer-move x s))) ((disable-theory t) (enable-theory ground-zero) (enable properp-replace-value properp-bv-to-nat-list smart-move computer-move))) (prove-lemma properp-untag-array (rewrite) (properp (untag-array x))) (prove-lemma properp-tag-array (rewrite) (properp (tag-array l x))) (prove-lemma computer-move-implemented (rewrite) (implies (and (equal p0 (p-state pc ctrl-stk (cons wa (cons np (cons s temp-stk))) (append (cm-prog word-size) prog-segment) data-segment max-ctrl-stk-size max-temp-stk-size word-size 'run)) (equal (p-current-instruction p0) '(call computer-move)) (computer-move-implemented-input-conditionp p0)) (let ((result (p p0 (computer-move-clock (untag-array (array (car (untag s)) data-segment)) word-size)))) (and (equal (p-pc result) (add1-addr pc)) (equal (p-psw result) 'run) (equal (untag-array (array (car (untag s)) (p-data-segment result))) (computer-move (untag-array (array (car (untag s)) data-segment)) word-size))))) ((disable computer-move computer-move-clock p-current-instruction lessp-max-list max-list all-zero-bitvp sum member-of-natlist-means lessp-sub1-x-y-crock all-zero-bitvp-max-list max-list-not-too-big))) #| A proof of some constant bounds on the computer-move-clock function was developed that makes slight use of the proof-checker enhancement of NQTHM. For completeness, here is the final theorem of that digression, with no proof included so that this script is executable in NQTHM without the enhancement (implies (and (nat-listp state ws) (lessp 0 ws) (not (lessp 32 ws)) (lessp 1 (length state)) (not (lessp 6 (length state)))) (and (lessp 10000 (computer-move-clock state ws)) (lessp (computer-move-clock state ws) 20000))) |# (prove-lemma nim-piton-space-reasonable (rewrite) (not (lessp 1000 (plus (nim-piton-ctrl-stk-requirement) (nim-piton-temp-stk-requirement))))) ;; bind up defns for presentation purposes (defn good-non-empty-nim-statep (state ws) (and (nat-listp state ws) (not (all-zero-bitvp state)))) (prove-lemma valid-movep-computer-move-better (rewrite) (implies (good-non-empty-nim-statep state ws) (valid-movep state (computer-move state ws))) ((use (valid-movep-computer-move (x state))) (disable-theory t) (enable good-non-empty-nim-statep) (enable-theory ground-zero))) (prove-lemma computer-move-works-better (rewrite) (implies (and (good-non-empty-nim-statep state ws) (wsp state t)) (not (wsp (computer-move state ws) t))) ((use (computer-move-works)) (disable-theory t) (enable good-non-empty-nim-statep) (enable-theory ground-zero))) ;;; An initial p-state to run the program on a particular NIM state, then ;;; enter an infinite loop. (defn example2-computer-move-p-state () (p-state '(pc (main . 0)) '((nil (pc (main . 0)))) nil (cons '(main nil nil (push-constant (addr (arr . 0))) (push-constant (nat 4)) (push-constant (addr (arr5 . 0))) (call computer-move) (push-constant (nat 1)) (push-constant (addr (flag . 0))) (deposit) (dl loop () (jump loop)) (ret)) (cm-prog 32)) '((arr (nat 15) (nat 4) (nat 7) (nat 1)) (arr5 (nat 3) (nat 4) (nat 2) (nat 1)) (flag (nat 0))) 30 10 32 'run)) ;;; Extra event that shows that the program is compilable and loadable ;;; onto FM9001, and that the correctness lemma for the Piton interpreter ;;; therefore holds. (ref: J's e-mail of 10 April 92.) (prove-lemma cm-prog-fm9001-loadable nil (let ((p0 (example2-computer-move-p-state))) (and (proper-p-statep p0) (p-loadablep p0 0) (equal (p-word-size p0) 32))) ((enable XOR-BVS-PROGRAM PUSH-1-VECTOR-PROGRAM NAT-TO-BV-PROGRAM BV-TO-NAT-PROGRAM NUMBER-WITH-AT-LEAST-PROGRAM HIGHEST-BIT-PROGRAM MATCH-AND-XOR-PROGRAM NAT-TO-BV-LIST-PROGRAM BV-TO-NAT-LIST-PROGRAM MAX-NAT-PROGRAM REPLACE-VALUE-PROGRAM SMART-MOVE-PROGRAM DELAY-PROGRAM COMPUTER-MOVE-PROGRAM))) ;;; Some events written by J Moore that produce an FM9001 image (defn pretty-load1 (p0 offset) (i->m (r->i (p->r p0)) nil offset)) (defn pretty-vector1 (lst) (cond ((nlistp lst) 0) ((car lst) (cons 49 (pretty-vector1 (cdr lst)))) (t (cons 48 (pretty-vector1 (cdr lst)))))) (defn pretty-vector (lst) (pack (cons 66 (pretty-vector1 lst)))) (defn pretty-vector-lst (lst) (cond ((nlistp lst) nil) (t (cons (pretty-vector (car lst)) (pretty-vector-lst (cdr lst)))))) (defn pretty-state (m) (list 'fm9001-state (pretty-vector-lst (m-regs m)) (m-c-flg m) (m-v-flg m) (m-n-flg m) (m-z-flg m) (pretty-vector-lst (m-mem m)))) (defn pretty-load (p offset) (pretty-state (pretty-load1 p offset))) ;; Using pretty-load in r-loop, we produce the following image: #| (LIST 'FM9001-STATE '(B00000000000000000000000000000000 B01001010001000000000000000000000 B01001010001000000000000000000000 B11111010001000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B11010000000000000000000000000000) F F F F '(B11110000000000000000000000000000 B00100000000000000000000000000000 B11100000000000000000000000000000 B10000000000000000000000000000000 B11000000000000000000000000000000 B00100000000000000000000000000000 B01000000000000000000000000000000 B10000000000000000000000000000000 B00000000000000000000000000000000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100001100010000011111110000 B00000000000000000000000000000000 B11111100001100010000011111110000 B00100000000000000000000000000000 B11111100001100010000011111110000 B00100000000000000000000000000000 B11111100000100010000011111110000 B10101000000000000000000000000000 B11111000001111000000011111110000 B10110101110000000000000000000000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11111100001100010000011111110000 B00010000000000000000000000000000 B11001100000010000000011111110000 B11001100000010100000011111110000 B11111000001111000000011111110000 B11011000000000000000000000000000 B11111000001111000000011111110000 B11111000000000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011110100000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100001010001000011111110000 B11111100000010000000011111110000 B00011010000000000000000000000000 B00100000001111000000111011110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011110100000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11001100000010000000011111110000 B00100000001100100000011111000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11001100000010000000011111110000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100100000011111010000 B11111000001111000000011111110000 B10101100000000000000000000000000 B11111000001111000000011111110000 B01011010000000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11111000001111000000011111110000 B11000110000000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11001100000100010000011111110000 B11111100000100010000011111110000 B10001110000000000000000000000000 B11111000001111000000011111110000 B10111010000000000000000000000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100000100010000011111110000 B10011110000000000000000000000000 B11111000001111000000011111110000 B10111010000000000000000000000000 B11001000001100100000011101010000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100001010001000011111110000 B11111100000010000000011111110000 B01110101000000000000000000000000 B00100000001111000000111011110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000001011111110000 B00100000000010000001011101010000 B00100000001100010000011111110000 B11111100001100010000011111110000 B00000000000000000000000000000000 B11111100001100100000100011110000 B10000000000000000000000000000000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100001010001000011111110000 B11111100000010000000011111110000 B11000101000000000000000000000000 B00100000001111000000111011110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100100000011111010000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011111000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111000001111000000011111110000 B01011110000000000000000000000000 B11111000001111000000011111110000 B00001101000000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11001100000100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100000100010000011111110000 B00100011000000000000000000000000 B11111000001111000000011111110000 B10111010000000000000000000000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100001100010000011111110000 B00000000000000000000000000000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100100000011110110000 B11001100001010001000011111110000 B11111100000010000000011111110000 B01111011000000000000000000000000 B00100000001111000000111011110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100100000011111000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011111000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11001100001010001000011111110000 B11111100000010000000011111110000 B01101111000000000000000000000000 B00100000001111000000111011110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011111000000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111000001111000000011111110000 B01010011000000000000000000000000 B11111000001111000000011111110000 B00011111000000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11111100001100010000011111110000 B00000000000000000000000000000000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00101000001100010000011111110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100100001011111100000 B11001000001100100000011111010000 B11111100001100100000100011110000 B10000000000000000000000000000000 B11001100001010001000011111110000 B11111100000010000000011111110000 B00111000100000000000000000000000 B00100000001111000000011011110000 B11001000001100100000011110000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011110000000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11001100000010000000011111110000 B00100000001100100000011111100000 B11001100001010001000011111110000 B11111100000010000000011111110000 B10111100100000000000000000000000 B00100000001111000000111011110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11001100000010000000011111110000 B00100000001100100000011111000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111000001111000000011111110000 B00010000100000000000000000000000 B11111000001111000000011111110000 B11111100100000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11001100000100010000011111110000 B11111100000100010000011111110000 B11010010100000000000000000000000 B11111000001111000000011111110000 B10111010000000000000000000000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11001000001100100000011101010000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100001010001000011111110000 B11111100000010000000011111110000 B01101110100000000000000000000000 B00100000001111000000111011110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100100000011110110000 B11001100001010001000011111110000 B11111100000010000000011111110000 B11010110100000000000000000000000 B00100000001111000000111011110000 B11001100000010000000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011111000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111000001111000000011111110000 B00001010100000000000000000000000 B11111000001111000000011111110000 B00011110100000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11111100001100010000011111110000 B00000000000000000000000000000000 B11111100000010000000011111110000 B00100000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00101000001100010000011111110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100100000011110110000 B11001100001010001000011111110000 B11111100000010000000011111110000 B10111101100000000000000000000000 B00100000001111000000011011110000 B11111100000010000000011111110000 B00100000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011110000000 B11111100000010000000011111110000 B00100000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100100001011111100000 B11001000001100100000011111010000 B11111100001100100000100011110000 B10000000000000000000000000000000 B11001100001010001000011111110000 B11111100000010000000011111110000 B11110011100000000000000000000000 B00100000001111000000111011110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11001100000010000000011111110000 B00100000001100100000011111000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111000001111000000011111110000 B10010001100000000000000000000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00101000001100010000011111110000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100100000011111010000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B11001100000010100000011111110000 B11111000001111000000011111110000 B10001011100000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00101000001100010000011111110000 B11111100000100010000011111110000 B10100111100000000000000000000000 B11111000001111000000011111110000 B01100110000000000000000000000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B11001100000010100000011111110000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011110000000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100101000011111010000 B11001000001100100000011111010000 B11111100001100100000111011110000 B10000000000000000000000000000000 B11001100001010001000011111110000 B11111100000010000000011111110000 B11011000010000000000000000000000 B00100000001111000000011011110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11001100000010000000011111110000 B00100000001100100000011111000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11001100000010000000011111110000 B00100000001100100000011111000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111000001111000000011111110000 B11011011100000000000000000000000 B11111000001111000000011111110000 B10111000010000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00101000001100010000011111110000 B11111100000100010000011111110000 B10001100010000000000000000000000 B11111000001111000000011111110000 B11001101000000000000000000000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B11001100000010100000011111110000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011110000000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100101000011111010000 B11001000001100100000011111010000 B11111100001100100000111011110000 B10000000000000000000000000000000 B11001100001010001000011111110000 B11111100000010000000011111110000 B11100110010000000000000000000000 B00100000001111000000011011110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11001100000010000000011111110000 B00100000001100100000011111000000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11001100000010000000011111110000 B00100000001100100000011111000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111000001111000000011111110000 B11100100010000000000000000000000 B11111000001111000000011111110000 B10010110010000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11111100001100010000011111110000 B00000000000000000000000000000000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00101000001100010000011111110000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11001100000010000000011111110000 B00100000001100100001011111100000 B11001000001100100000011111010000 B11111100001100100000100011110000 B10000000000000000000000000000000 B11001100001010001000011111110000 B11111100000010000000011111110000 B01101001010000000000000000000000 B00100000001111000000111011110000 B11001100000010000000011111110000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011110000000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100101000011111010000 B11001000001100100000011111010000 B11111100001100100000111011110000 B10000000000000000000000000000000 B11001100001010001000011111110000 B11111100000010000000011111110000 B01011101010000000000000000000000 B00100000001111000000011011110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11001100000010000000011111110000 B00100000001100100000011111000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111000001111000000011111110000 B01101110010000000000000000000000 B11111000001111000000011111110000 B00111101010000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B00100000001100101000011111010000 B11001000001100100000011111010000 B11111100001100100000111011110000 B10000000000000000000000000000000 B11001100001010001000011111110000 B11111100000010000000011111110000 B10100111010000000000000000000000 B00100000001111000000011011110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11001100000010000000011111110000 B00100000001100100000011111000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111000001111000000011111110000 B00100011010000000000000000000000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001100000010000000011111110000 B11001100000010100000011111110000 B11111000001111000000011111110000 B10001111010000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B01000000000000000000000000000000 B11111100000100010000011111110000 B10010000110000000000000000000000 B11111000001111000000011111110000 B11011111000000000000000000000000 B11111100001100010000011111110000 B01000000000000000000000000000000 B11001100000010000000011111110000 B00100000001100100001011111100000 B11001000001100100000011111010000 B11111100001100100000100011110000 B10000000000000000000000000000000 B11001100001010001000011111110000 B11111100000010000000011111110000 B01011010110000000000000000000000 B00100000001111000000011011110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000100010000011111110000 B00100100110000000000000000000000 B11111000001111000000011111110000 B00101011100000000000000000000000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000100010000011111110000 B00011100110000000000000000000000 B11111000001111000000011111110000 B01000100000000000000000000000000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B11111100000100010000011111110000 B00000010110000000000000000000000 B11111000001111000000011111110000 B01000010100000000000000000000000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000100010000011111110000 B00010010110000000000000000000000 B11111000001111000000011111110000 B11011110100000000000000000000000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000100010000011111110000 B00011010110000000000000000000000 B11111000001111000000011111110000 B00000100010000000000000000000000 B11111000001111000000011111110000 B01110001110000000000000000000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000100010000011111110000 B01010110110000000000000000000000 B11111000001111000000011111110000 B00110110010000000000000000000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B10000000000000000000000000000000 B11111100000100010000011111110000 B00011110110000000000000000000000 B11111000001111000000011111110000 B11011111000000000000000000000000 B11001100000010000001011111110000 B00100000000010000001011101010000 B00100000001100010000011111110000 B11111100001100010000011111110000 B00000000000000000000000000000000 B11111100001100100000100011110000 B10000000000000000000000000000000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11001100000010000000011111110000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000100010000011111110000 B00110001110000000000000000000000 B11111000001111000000011111110000 B11111101010000000000000000000000 B11111000001111000000011111110000 B01110001110000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11001100000100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011110100000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B11001000000010100000011111110000 B00100000000010000000011111110000 B00100000000010000000011111110000 B00100000000010000000011111110000 B00100000000010000000011111110000 B11001100001010001000011111110000 B11111100000010000000011111110000 B00010101110000000000000000000000 B00100000001111000000111011110000 B00100000000010000000011111110000 B11111000001111000000011111110000 B00101001110000000000000000000000 B11111000001111000000011111110000 B01010101110000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B10000000000100010000011111110000 B01000000001000000000011111110000 B11111100000100010000011111110000 B00000000000000000000000000000000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11001100000100010000011111110000 B11111100001100010000011111110000 B01011111000000000000000000000000 B11111100000100010000011111110000 B01011101110000000000000000000000 B11111000001111000000011111110000 B10001001110000000000000000000000 B11111100001100010000011111110000 B01011111000000000000000000000000 B11111100000100010000011111110000 B00000011110000000000000000000000 B11111000001111000000011111110000 B10001001110000000000000000000000 B11111100001100010000011111110000 B01011111000000000000000000000000 B11111100000100010000011111110000 B01100011110000000000000000000000 B11111000001111000000011111110000 B10001001110000000000000000000000 B11111100001100010000011111110000 B01011111000000000000000000000000 B11111100000100010000011111110000 B00110011110000000000000000000000 B11111000001111000000011111110000 B10001001110000000000000000000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100001100010000011111110000 B01000000000000000000000000000000 B11111100000100010000011111110000 B01011011110000000000000000000000 B11111000001111000000011111110000 B11011111000000000000000000000000 B11001100001010001000011111110000 B11111100000010000000011111110000 B00001000001000000000000000000000 B00100000001111000000111011110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000100010000011111110000 B01110111110000000000000000000000 B11111000001111000000011111110000 B00101011100000000000000000000000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000100010000011111110000 B01011111110000000000000000000000 B11111000001111000000011111110000 B01000100000000000000000000000000 B11001100001010001000011111110000 B11111100000010000000011111110000 B00001000001000000000000000000000 B00100000001111000000111011110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B01000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000100010000011111110000 B01110000001000000000000000000000 B11111000001111000000011111110000 B00101111010000000000000000000000 B11111000001111000000011111110000 B11001100001000000000000000000000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B00000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B10000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000100010000011111110000 B00000100001000000000000000000000 B11111000001111000000011111110000 B00110110010000000000000000000000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B11001100000010100000011111110000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11111100000010000000011111110000 B11000000000000000000000000000000 B01000000000010000000011111000000 B00101000001100010000011111110000 B11001000001100100000011110100000 B11111100000100010000011111110000 B10001100001000000000000000000000 B11111000001111000000011111110000 B11111101010000000000000000000000 B11111000001111000000011111110000 B11001100001000000000000000000000 B10000000000100000000011111110000 B01001100001000000000011111110000 B01001100001111000000011111110000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B01001010001000000000000000000000 B11010000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B00000000000000000000000000000000 B01101100001000000000000000000000 B10101010001000000000000000000000 B11111010001000000000000000000000)) |# ;; This image above executed on a fabricated FM9001 in a test jig at Indiana ;; University with the help of M. Esen Tuna, Bhaskar Bose, and Steve Johnson. ;; The resulting state that begins with the following: #| (2 4 7 1 2 4 7 1 1 266373121 266339330 266374207 0 266374207 4 266374207 4 266373183 21 266353695 941 266374207 1 266374207 8 266342451 266358835 266353695 27 266353695 31 266340353 266339378 266353714 266373121 266339330 266373171 266373171 266342463 0 65015810 266374164 266342451 266374164 266342463 1 65015810 266374164 98585619 266342463 1 65015810 266358835 266342463 1 65015810 266374164 266409011 266342463 88 259013636 266342463 1 65015810 266374164 98585619 266342463 1 65015810 266358835 266342463 0 .... Note that the Nim state beginning in location 0 of 15 4 7 1 has been transformed into 2 4 7 1, which by proof we know is an optimal move. |#