#| Copyright (C) 1994 by Yuan Yu. All Rights Reserved. This script is hereby placed in the public domain, and therefore unlimited editing and redistribution is permitted. NO WARRANTY Yuan Yu 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 Yuan Yu 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 "mc20-2" t) ; Proof of the Corectness of a Majority Voting Program ; #| The following C function MJRTY determines if there is a candidate who has received a majority of votes cast in an election. /* a majority voting algorithm invented by Boyer and Moore */ #define YES 1 #define NO 0 struct winner { int x; int y; }; struct winner mjrty (int a[], int n) { int cand, i, k; struct winner temp; k = 0; for (i = 0; i < n; i++) if (k == 0) { cand = a[i]; k = 1; } else { if (cand == a[i]) k++; else k--; }; temp.x = cand; if (k == 0) { temp.y = NO; return temp; }; if (k > n/2) { temp.y = YES; return temp; }; k = 0; for (i = 0; i < n; i++) if (a[i] == cand) k++; if (k > n/2) temp.y = YES; else temp.y = NO; return temp; } Here is the MC68020 assembly code of the above C program. The code is generated by "gcc -O". 0x2310 : linkw a6,#0 0x2314 : moveml d2-d5,sp@- 0x2318 : moveal a6@(8),a0 0x231c : movel a6@(12),d2 0x2320 : clrl d1 0x2322 : clrl d0 0x2324 : cmpl d0,d2 0x2326 : ble 0x2346 0x2328 : tstl d1 0x232a : bne 0x2334 0x232c : movel 0(a0)[d0.l*4],d3 0x2330 : movel #1,d1 0x2332 : bra 0x2340 0x2334 : cmpl 0(a0)[d0.l*4],d3 0x2338 : bne 0x233e 0x233a : addql #1,d1 0x233c : bra 0x2340 0x233e : subl #1,d1 0x2340 : addql #1,d0 0x2342 : cmpl d0,d2 0x2344 : bgt 0x2328 0x2346 : movel d3,d4 0x2348 : tstl d1 0x234a : beq 0x2382 0x234c : movel d2,d0 0x234e : bge 0x2352 0x2350 : addql #1,d0 0x2352 : asrl #1,d0 0x2354 : cmpl d1,d0 0x2356 : bge 0x235c 0x2358 : movel #1,d5 0x235a : bra 0x2384 0x235c : clrl d1 0x235e : clrl d0 0x2360 : cmpl d0,d2 0x2362 : ble 0x2372 0x2364 : cmpl 0(a0)[d0.l*4],d3 0x2368 : bne 0x236c 0x236a : addql #1,d1 0x236c : addql #1,d0 0x236e : cmpl d0,d2 0x2370 : bgt 0x2364 0x2372 : movel d2,d0 0x2374 : bge 0x2378 0x2376 : addql #1,d0 0x2378 : asrl #1,d0 0x237a : cmpl d1,d0 0x237c : bge 0x2382 0x237e : movel #1,d5 0x2380 : bra 0x2384 0x2382 : clrl d5 0x2384 : movel d4,d0 0x2386 : movel d5,d1 0x2388 : moveml a6@(-16),d2-d5 0x238e : unlk a6 0x2390 : rts The machine code of the above program is: : 0x4e56 0x0000 0x48e7 0x3c00 0x206e 0x0008 0x242e 0x000c : 0x4281 0x4280 0xb480 0x6f1e 0x4a81 0x6608 0x2630 0x0c00 : 0x7201 0x600c 0xb6b0 0x0c00 0x6604 0x5281 0x6002 0x5381 : 0x5280 0xb480 0x6ee2 0x2803 0x4a81 0x6736 0x2002 0x6c02 : 0x5280 0xe280 0xb081 0x6c04 0x7a01 0x6028 0x4281 0x4280 : 0xb480 0x6f0e 0xb6b0 0x0c00 0x6602 0x5281 0x5280 0xb480 : 0x6ef2 0x2002 0x6c02 0x5280 0xe280 0xb081 0x6c04 0x7a01 : 0x6002 0x4285 0x2004 0x2205 0x4cee 0x003c 0xfff0 0x4e5e : 0x4e75 In the Nqthm logic, it is like: '(78 86 0 0 72 231 60 0 32 110 0 8 36 46 0 12 66 129 66 128 180 128 111 30 74 129 102 8 38 48 12 0 114 1 96 12 182 176 12 0 102 4 82 129 96 2 83 129 82 128 180 128 110 226 40 3 74 129 103 54 32 2 108 2 82 128 226 128 176 129 108 4 122 1 96 40 66 129 66 128 180 128 111 14 182 176 12 0 102 2 82 129 82 128 180 128 110 242 32 2 108 2 82 128 226 128 176 129 108 4 122 1 96 2 66 133 32 4 34 5 76 238 0 60 255 240 78 94 78 117) |# ; in the logic, the above program is defined by (mjrty-code). (defn mjrty-code () '(78 86 0 0 72 231 60 0 32 110 0 8 36 46 0 12 66 129 66 128 180 128 111 30 74 129 102 8 38 48 12 0 114 1 96 12 182 176 12 0 102 4 82 129 96 2 83 129 82 128 180 128 110 226 40 3 74 129 103 54 32 2 108 2 82 128 226 128 176 129 108 4 122 1 96 40 66 129 66 128 180 128 111 14 182 176 12 0 102 2 82 129 82 128 180 128 110 242 32 2 108 2 82 128 226 128 176 129 108 4 122 1 96 2 66 133 32 4 34 5 76 238 0 60 255 240 78 94 78 117)) ; mjrty-cand is a function in the logic to simulate the candidate ; findhe above code. (defn mjrty-cand (n lst cand i k) (if (lessp i n) (if (zerop k) (mjrty-cand n lst (get-nth i lst) (add1 i) 1) (if (equal cand (get-nth i lst)) (mjrty-cand n lst cand (add1 i) (add1 k)) (mjrty-cand n lst cand (add1 i) (sub1 k)))) cand) ((lessp (difference n i)))) (defn mjrty-k (n lst cand i k) (if (lessp i n) (if (zerop k) (mjrty-k n lst (get-nth i lst) (add1 i) 1) (if (equal cand (get-nth i lst)) (mjrty-k n lst cand (add1 i) (add1 k)) (mjrty-k n lst cand (add1 i) (sub1 k)))) k) ((lessp (difference n i)))) ; cand-cnt is a function in the logic to simulate the process of ; counting the number of votes for the given candidate. (defn cand-cnt (n lst cand i k) (if (lessp i n) (if (equal cand (get-nth i lst)) (cand-cnt n lst cand (add1 i) (add1 k)) (cand-cnt n lst cand (add1 i) k)) k) ((lessp (difference n i)))) ; mjrty-p determines if the given candidate cand has received a majority ; voting. (defn mjrty-p (n lst cand i k) (if (zerop (mjrty-k n lst cand i k)) f (if (lessp (quotient n 2) (mjrty-k n lst cand i k)) t (lessp (quotient n 2) (cand-cnt n lst (mjrty-cand n lst cand i k) i k))))) ; the computation time. (defn mjrty-cand-t (a n lst cand i k) (if (lessp i n) (if (zerop k) (let ((cand1 (get-nth i lst))) (splus 8 (mjrty-cand-t a n lst cand1 (add1 i) 1))) (if (equal cand (get-nth i lst)) (splus 9 (mjrty-cand-t a n lst cand (add1 i) (add1 k))) (splus 8 (mjrty-cand-t a n lst cand (add1 i) (sub1 k))))) (if (equal cand (get-nth 0 lst)) 18 17)) ((lessp (difference n i)))) (defn mjrty-sn-t (a n lst cand i k) (if (lessp i n) (if (zerop k) (let ((cand1 (get-nth i lst))) (splus 8 (mjrty-sn-t a n lst cand1 (add1 i) 1))) (if (equal cand (get-nth i lst)) (splus 9 (mjrty-sn-t a n lst cand (add1 i) (add1 k))) (splus 8 (mjrty-sn-t a n lst cand (add1 i) (sub1 k))))) (if (zerop k) 11 17)) ((lessp (difference n i)))) (defn cand-cnt-t (a n lst cand i k) (if (lessp i n) (if (equal cand (get-nth i lst)) (splus 6 (cand-cnt-t a n lst cand (add1 i) (add1 k))) (splus 5 (cand-cnt-t a n lst cand (add1 i) k))) (if (lessp (quotient n 2) k) 14 13)) ((lessp (difference n i)))) (defn mjrty-t (a n lst) (let ((cand (get-nth 0 lst))) (splus 14 (if (or (zerop (mjrty-k n lst cand 1 1)) (lessp (quotient n 2) (mjrty-k n lst cand 1 1))) (mjrty-sn-t a n lst cand 1 1) (splus (mjrty-cand-t a n lst cand 1 1) (if (equal cand (mjrty-cand n lst cand 1 1)) (cand-cnt-t a n lst (mjrty-cand n lst cand 1 1) 1 1) (cand-cnt-t a n lst (mjrty-cand n lst cand 1 1) 1 0))))))) ; induction hints. (defn mjrty-cand-induct (s n lst cand i k) (if (lessp i n) (if (zerop k) (let ((cand1 (get-nth i lst))) (mjrty-cand-induct (stepn s 8) n lst cand1 (add1 i) 1)) (if (equal cand (get-nth i lst)) (mjrty-cand-induct (stepn s 9) n lst cand (add1 i) (add1 k)) (mjrty-cand-induct (stepn s 8) n lst cand (add1 i) (sub1 k)))) t) ((lessp (difference n i)))) (defn cand-cnt-induct (s n lst cand i k) (if (lessp i n) (if (equal cand (get-nth i lst)) (cand-cnt-induct (stepn s 6) n lst cand (add1 i) (add1 k)) (cand-cnt-induct (stepn s 5) n lst cand (add1 i) k)) t) ((lessp (difference n i)))) ; the preconditions of the initial state. (defn mjrty-statep (s a n lst) (and (equal (mc-status s) 'running) (evenp (mc-pc s)) (rom-addrp (mc-pc s) (mc-mem s) 130) (mcode-addrp (mc-pc s) (mc-mem s) (mjrty-code)) (ram-addrp (sub 32 20 (read-sp s)) (mc-mem s) 32) (ram-addrp a (mc-mem s) (times 4 n)) (mem-ilst 4 a (mc-mem s) n lst) (disjoint a (times 4 n) (sub 32 20 (read-sp s)) 32) (equal a (read-mem (add 32 (read-sp s) 4) (mc-mem s) 4)) (equal n (iread-mem (add 32 (read-sp s) 8) (mc-mem s) 4)) (not (zerop n)))) ; the conditions of the intermediate state s0. (defn mjrty-s0p (s a n lst cand i k) (and (equal (mc-status s) 'running) (evenp (mc-pc s)) (rom-addrp (sub 32 50 (mc-pc s)) (mc-mem s) 130) (mcode-addrp (sub 32 50 (mc-pc s)) (mc-mem s) (mjrty-code)) (ram-addrp (sub 32 16 (read-an 32 6 s)) (mc-mem s) 32) (ram-addrp a (mc-mem s) (times 4 n)) (mem-ilst 4 a (mc-mem s) n lst) (disjoint a (times 4 n) (sub 32 16 (read-an 32 6 s)) 32) (equal a (read-rn 32 8 (mc-rfile s))) (equal n (nat-to-int (read-rn 32 2 (mc-rfile s)) 32)) (equal cand (nat-to-int (read-rn 32 3 (mc-rfile s)) 32)) (equal i (nat-to-int (read-rn 32 0 (mc-rfile s)) 32)) (equal k (nat-to-int (read-rn 32 1 (mc-rfile s)) 32)) (not (zerop n)) (numberp i) (numberp k) (leq k i))) ; the conditions of the intermediate state s1. (defn mjrty-s1p (s a n lst cand i k) (and (equal (mc-status s) 'running) (evenp (mc-pc s)) (rom-addrp (sub 32 94 (mc-pc s)) (mc-mem s) 130) (mcode-addrp (sub 32 94 (mc-pc s)) (mc-mem s) (mjrty-code)) (ram-addrp (sub 32 16 (read-an 32 6 s)) (mc-mem s) 32) (ram-addrp a (mc-mem s) (times 4 n)) (mem-ilst 4 a (mc-mem s) n lst) (disjoint a (times 4 n) (sub 32 16 (read-an 32 6 s)) 32) (equal a (read-rn 32 8 (mc-rfile s))) (equal n (nat-to-int (read-rn 32 2 (mc-rfile s)) 32)) (equal cand (nat-to-int (read-rn 32 4 (mc-rfile s)) 32)) (equal cand (nat-to-int (read-rn 32 3 (mc-rfile s)) 32)) (equal i (nat-to-int (read-rn 32 0 (mc-rfile s)) 32)) (equal k (nat-to-int (read-rn 32 1 (mc-rfile s)) 32)) (not (zerop n)) (numberp i) (numberp k) (leq k i))) ; the initial segment. From the initial state to s0. (prove-lemma mjrty-s-s0 (rewrite) (let ((cand (get-nth 0 lst))) (implies (mjrty-statep s a n lst) (and (mjrty-s0p (stepn s 14) a n lst cand 1 1) (equal (linked-rts-addr (stepn s 14)) (rts-addr s)) (equal (linked-a6 (stepn s 14)) (read-an 32 6 s)) (equal (read-rn 32 14 (mc-rfile (stepn s 14))) (sub 32 4 (read-sp s))) (equal (movem-saved (stepn s 14) 4 16 4) (readm-rn 32 '(2 3 4 5) (mc-rfile s)))))) ((disable times))) (prove-lemma mjrty-s-s0-rfile (rewrite) (implies (and (mjrty-statep s a n lst) (d6-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 14))) (read-rn oplen rn (mc-rfile s)))) ((disable times))) (prove-lemma mjrty-s-s0-mem (rewrite) (implies (and (mjrty-statep s a n lst) (disjoint (sub 32 20 (read-sp s)) 32 x k)) (equal (read-mem x (mc-mem (stepn s 14)) k) (read-mem x (mc-mem s) k))) ((disable times))) ; s0 --> exit. ; base case. (prove-lemma mjrty-s0-sn-base-1 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (not (lessp i n)) (zerop k)) (and (equal (mc-status (stepn s 11)) 'running) (equal (mc-pc (stepn s 11)) (linked-rts-addr s)) (equal (iread-dn 32 0 (stepn s 11)) cand) (equal (iread-dn 32 1 (stepn s 11)) 0) (equal (read-rn 32 14 (mc-rfile (stepn s 11))) (linked-a6 s)) (equal (read-rn 32 15 (mc-rfile (stepn s 11))) (add 32 (read-an 32 6 s) 8)) (equal (read-mem x (mc-mem (stepn s 11)) l) (read-mem x (mc-mem s) l))))) (prove-lemma mjrty-s0-sn-base-2 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (not (lessp i n)) (not (zerop k)) (lessp (quotient n 2) k)) (and (equal (mc-status (stepn s 17)) 'running) (equal (mc-pc (stepn s 17)) (linked-rts-addr s)) (equal (iread-dn 32 0 (stepn s 17)) cand) (equal (iread-dn 32 1 (stepn s 17)) 1) (equal (read-rn 32 14 (mc-rfile (stepn s 17))) (linked-a6 s)) (equal (read-rn 32 15 (mc-rfile (stepn s 17))) (add 32 (read-an 32 6 s) 8)) (equal (read-mem x (mc-mem (stepn s 17)) l) (read-mem x (mc-mem s) l)))) ((enable iquotient))) (prove-lemma mjrty-s0-sn-rfile-base-1 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (not (lessp i n)) (zerop k) (d2-7a2-5p rn) (leq oplen 32)) (equal (read-rn oplen rn (mc-rfile (stepn s 11))) (if (d6-7a2-5p rn) (read-rn oplen rn (mc-rfile s)) (get-vlst oplen 0 rn '(2 3 4 5) (movem-saved s 4 16 4)))))) (prove-lemma mjrty-s0-sn-rfile-base-2 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (not (lessp i n)) (not (zerop k)) (lessp (quotient n 2) k) (d2-7a2-5p rn) (leq oplen 32)) (equal (read-rn oplen rn (mc-rfile (stepn s 17))) (if (d6-7a2-5p rn) (read-rn oplen rn (mc-rfile s)) (get-vlst oplen 0 rn '(2 3 4 5) (movem-saved s 4 16 4))))) ((enable iquotient))) ; induction case. (prove-lemma add1-int-rangep (rewrite) (implies (lessp x (nat-to-int y n)) (int-rangep (add1 x) n)) ((enable int-rangep nat-to-int))) (enable iplus) (prove-lemma mjrty-s0-s0-1 (rewrite) (let ((cand1 (get-nth i lst))) (implies (and (mjrty-s0p s a n lst cand i k) (lessp i n) (zerop k)) (and (mjrty-s0p (stepn s 8) a n lst cand1 (add1 i) 1) (equal (linked-rts-addr (stepn s 8)) (linked-rts-addr s)) (equal (linked-a6 (stepn s 8)) (linked-a6 s)) (equal (read-rn 32 14 (mc-rfile (stepn s 8))) (read-rn 32 14 (mc-rfile s))) (equal (movem-saved (stepn s 8) 4 16 4) (movem-saved s 4 16 4)) (equal (read-mem x (mc-mem (stepn s 8)) l) (read-mem x (mc-mem s) l))))) ((disable times lessp))) (prove-lemma add1-int-rangepxx (rewrite) (implies (and (leq i r) (lessp r n) (int-rangep n 32)) (int-rangep (add1 i) 32)) ((enable int-rangep nat-to-int))) (prove-lemma mjrty-s0-s0-2 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (lessp i n) (not (zerop k)) (equal cand (get-nth i lst))) (and (mjrty-s0p (stepn s 9) a n lst cand (add1 i) (add1 k)) (equal (linked-rts-addr (stepn s 9)) (linked-rts-addr s)) (equal (linked-a6 (stepn s 9)) (linked-a6 s)) (equal (read-rn 32 14 (mc-rfile (stepn s 9))) (read-rn 32 14 (mc-rfile s))) (equal (movem-saved (stepn s 9) 4 16 4) (movem-saved s 4 16 4)) (equal (read-mem x (mc-mem (stepn s 9)) l) (read-mem x (mc-mem s) l)))) ((disable times lessp))) (prove-lemma mjrty-s0-s0-3 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (lessp i n) (not (zerop k)) (not (equal cand (get-nth i lst)))) (and (mjrty-s0p (stepn s 8) a n lst cand (add1 i) (sub1 k)) (equal (linked-rts-addr (stepn s 8)) (linked-rts-addr s)) (equal (linked-a6 (stepn s 8)) (linked-a6 s)) (equal (read-rn 32 14 (mc-rfile (stepn s 8))) (read-rn 32 14 (mc-rfile s))) (equal (movem-saved (stepn s 8) 4 16 4) (movem-saved s 4 16 4)) (equal (read-mem x (mc-mem (stepn s 8)) l) (read-mem x (mc-mem s) l)))) ((disable times lessp))) (prove-lemma mjrty-s0-s0-rfile-1 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (lessp i n) (zerop k) (d6-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 8))) (read-rn oplen rn (mc-rfile s)))) ((disable times lessp))) (prove-lemma mjrty-s0-s0-rfile-2 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (lessp i n) (not (zerop k)) (equal cand (get-nth i lst)) (d6-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 9))) (read-rn oplen rn (mc-rfile s)))) ((disable times lessp))) (prove-lemma mjrty-s0-s0-rfile-3 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (lessp i n) (not (zerop k)) (not (equal cand (get-nth i lst))) (d6-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 8))) (read-rn oplen rn (mc-rfile s)))) ((disable times lessp))) ; the proof of s0 --> exit. (prove-lemma mjrty-s0-sn (rewrite) (let ((sn (stepn s (mjrty-sn-t a n lst cand i k)))) (implies (and (mjrty-s0p s a n lst cand i k) (or (zerop (mjrty-k n lst cand i k)) (lessp (quotient n 2) (mjrty-k n lst cand i k)))) (and (equal (mc-status sn) 'running) (equal (mc-pc sn) (linked-rts-addr s)) (equal (iread-dn 32 0 sn) (mjrty-cand n lst cand i k)) (equal (iread-dn 32 1 sn) (if (lessp (quotient n 2) (mjrty-k n lst cand i k)) 1 0)) (equal (read-rn 32 14 (mc-rfile sn)) (linked-a6 s)) (equal (read-rn 32 15 (mc-rfile sn)) (add 32 (read-an 32 6 s) 8)) (equal (read-mem x (mc-mem sn) l) (read-mem x (mc-mem s) l))))) ((induct (mjrty-cand-induct s n lst cand i k)) (disable mjrty-s0p linked-rts-addr rts-addr linked-a6 iread-dn))) (prove-lemma mjrty-s0-sn-rfile (rewrite) (let ((sn (stepn s (mjrty-sn-t a n lst cand i k)))) (implies (and (mjrty-s0p s a n lst cand i k) (or (zerop (mjrty-k n lst cand i k)) (lessp (quotient n 2) (mjrty-k n lst cand i k))) (d2-7a2-5p rn) (leq oplen 32)) (equal (read-rn oplen rn (mc-rfile sn)) (if (d6-7a2-5p rn) (read-rn oplen rn (mc-rfile s)) (get-vlst oplen 0 rn '(2 3 4 5) (movem-saved s 4 16 4)))))) ((induct (mjrty-cand-induct s n lst cand i k)) (disable mjrty-s0p))) ; s0 --> s1. ; base case: (prove-lemma mjrty-s0-s1-base1 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (not (lessp i n)) (not (zerop k)) (not (lessp (quotient n 2) k)) (equal cand (get-nth 0 lst))) (and (mjrty-s1p (stepn s 18) a n lst cand 1 1) (equal (linked-rts-addr (stepn s 18)) (linked-rts-addr s)) (equal (linked-a6 (stepn s 18)) (linked-a6 s)) (equal (read-rn 32 14 (mc-rfile (stepn s 18))) (read-rn 32 14 (mc-rfile s))) (equal (movem-saved (stepn s 18) 4 16 4) (movem-saved s 4 16 4)) (equal (read-mem x (mc-mem (stepn s 18)) l) (read-mem x (mc-mem s) l)))) ((disable times) (enable iquotient))) (prove-lemma mjrty-s0-s1-base2 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (not (lessp i n)) (not (zerop k)) (not (lessp (quotient n 2) k)) (not (equal cand (get-nth 0 lst)))) (and (mjrty-s1p (stepn s 17) a n lst cand 1 0) (equal (linked-rts-addr (stepn s 17)) (linked-rts-addr s)) (equal (linked-a6 (stepn s 17)) (linked-a6 s)) (equal (read-rn 32 14 (mc-rfile (stepn s 17))) (read-rn 32 14 (mc-rfile s))) (equal (movem-saved (stepn s 17) 4 16 4) (movem-saved s 4 16 4)) (equal (read-mem x (mc-mem (stepn s 17)) l) (read-mem x (mc-mem s) l)))) ((disable times) (enable iquotient))) (prove-lemma mjrty-s0-s1-rfile-base1 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (not (lessp i n)) (not (zerop k)) (not (lessp (quotient n 2) k)) (equal cand (get-nth 0 lst)) (d6-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 18))) (read-rn oplen rn (mc-rfile s)))) ((disable times) (enable iquotient))) (prove-lemma mjrty-s0-s1-rfile-base2 (rewrite) (implies (and (mjrty-s0p s a n lst cand i k) (not (lessp i n)) (not (zerop k)) (not (lessp (quotient n 2) k)) (not (equal cand (get-nth 0 lst))) (d6-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 17))) (read-rn oplen rn (mc-rfile s)))) ((enable iquotient))) ; the proof of s0 --> s1. (prove-lemma mjrty-s0-s1 (rewrite) (let ((s1 (stepn s (mjrty-cand-t a n lst cand i k)))) (implies (and (mjrty-s0p s a n lst cand i k) (not (zerop (mjrty-k n lst cand i k))) (not (lessp (quotient n 2) (mjrty-k n lst cand i k))) (equal cand0 (mjrty-cand n lst cand i k)) (equal k0 (if (equal (mjrty-cand n lst cand i k) (get-nth 0 lst)) 1 0))) (and (mjrty-s1p s1 a n lst cand0 1 k0) (equal (linked-rts-addr s1) (linked-rts-addr s)) (equal (linked-a6 s1) (linked-a6 s)) (equal (read-rn 32 14 (mc-rfile s1)) (read-rn 32 14 (mc-rfile s))) (equal (movem-saved s1 4 16 4) (movem-saved s 4 16 4)) (equal (read-mem x (mc-mem s1) l) (read-mem x (mc-mem s) l))))) ((induct (mjrty-cand-induct s n lst cand i k)) (disable mjrty-s0p mjrty-s1p movem-saved linked-rts-addr linked-a6))) (prove-lemma mjrty-s0-s1-rfile (rewrite) (let ((s1 (stepn s (mjrty-cand-t a n lst cand i k)))) (implies (and (mjrty-s0p s a n lst cand i k) (not (zerop (mjrty-k n lst cand i k))) (not (lessp (quotient n 2) (mjrty-k n lst cand i k))) (d6-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile s1)) (read-rn oplen rn (mc-rfile s))))) ((induct (mjrty-cand-induct s n lst cand i k)) (disable mjrty-s0p))) ; s1 --> exit. ; base case. (prove-lemma mjrty-s1-sn-1 (rewrite) (implies (and (mjrty-s1p s a n lst cand i k) (not (lessp i n)) (lessp (quotient n 2) k)) (and (equal (mc-status (stepn s 14)) 'running) (equal (mc-pc (stepn s 14)) (linked-rts-addr s)) (equal (iread-dn 32 0 (stepn s 14)) cand) (equal (iread-dn 32 1 (stepn s 14)) 1) (equal (read-rn 32 14 (mc-rfile (stepn s 14))) (linked-a6 s)) (equal (read-rn 32 15 (mc-rfile (stepn s 14))) (add 32 (read-an 32 6 s) 8)) (equal (read-mem x (mc-mem (stepn s 14)) l) (read-mem x (mc-mem s) l)))) ((enable iquotient))) (prove-lemma mjrty-s1-sn-rfile-1 (rewrite) (implies (and (mjrty-s1p s a n lst cand i k) (not (lessp i n)) (lessp (quotient n 2) k) (d2-7a2-5p rn) (leq oplen 32)) (equal (read-rn oplen rn (mc-rfile (stepn s 14))) (if (d6-7a2-5p rn) (read-rn oplen rn (mc-rfile s)) (get-vlst oplen 0 rn '(2 3 4 5) (movem-saved s 4 16 4))))) ((enable iquotient))) (prove-lemma mjrty-s1-sn-2 (rewrite) (implies (and (mjrty-s1p s a n lst cand i k) (not (lessp i n)) (not (lessp (quotient n 2) k))) (and (equal (mc-status (stepn s 13)) 'running) (equal (mc-pc (stepn s 13)) (linked-rts-addr s)) (equal (iread-dn 32 0 (stepn s 13)) cand) (equal (iread-dn 32 1 (stepn s 13)) 0) (equal (read-rn 32 14 (mc-rfile (stepn s 13))) (linked-a6 s)) (equal (read-rn 32 15 (mc-rfile (stepn s 13))) (add 32 (read-an 32 6 s) 8)) (equal (read-mem x (mc-mem (stepn s 13)) l) (read-mem x (mc-mem s) l)))) ((enable iquotient))) (prove-lemma mjrty-s1-sn-rfile-2 (rewrite) (implies (and (mjrty-s1p s a n lst cand i k) (not (lessp i n)) (not (lessp (quotient n 2) k)) (d2-7a2-5p rn) (leq oplen 32)) (equal (read-rn oplen rn (mc-rfile (stepn s 13))) (if (d6-7a2-5p rn) (read-rn oplen rn (mc-rfile s)) (get-vlst oplen 0 rn '(2 3 4 5) (movem-saved s 4 16 4))))) ((enable iquotient))) ; induction case. (prove-lemma mjrty-s1-s1-1 (rewrite) (implies (and (mjrty-s1p s a n lst cand i k) (lessp i n) (equal cand (get-nth i lst))) (and (mjrty-s1p (stepn s 6) a n lst cand (add1 i) (add1 k)) (equal (linked-rts-addr (stepn s 6)) (linked-rts-addr s)) (equal (linked-a6 (stepn s 6)) (linked-a6 s)) (equal (read-rn 32 14 (mc-rfile (stepn s 6))) (read-rn 32 14 (mc-rfile s))) (equal (movem-saved (stepn s 6) 4 16 4) (movem-saved s 4 16 4)) (equal (read-mem x (mc-mem (stepn s 6)) l) (read-mem x (mc-mem s) l)))) ((disable times lessp))) (prove-lemma mjrty-s1-s1-2 (rewrite) (implies (and (mjrty-s1p s a n lst cand i k) (lessp i n) (not (equal cand (get-nth i lst)))) (and (mjrty-s1p (stepn s 5) a n lst cand (add1 i) k) (equal (linked-rts-addr (stepn s 5)) (linked-rts-addr s)) (equal (linked-a6 (stepn s 5)) (linked-a6 s)) (equal (read-rn 32 14 (mc-rfile (stepn s 5))) (read-rn 32 14 (mc-rfile s))) (equal (movem-saved (stepn s 5) 4 16 4) (movem-saved s 4 16 4)) (equal (read-mem x (mc-mem (stepn s 5)) l) (read-mem x (mc-mem s) l)))) ((disable times lessp))) (prove-lemma mjrty-s1-s1-rfile-1 (rewrite) (implies (and (mjrty-s1p s a n lst cand i k) (lessp i n) (equal cand (get-nth i lst)) (d6-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 6))) (read-rn oplen rn (mc-rfile s)))) ((disable times lessp))) (prove-lemma mjrty-s1-s1-rfile-2 (rewrite) (implies (and (mjrty-s1p s a n lst cand i k) (lessp i n) (not (equal cand (get-nth i lst))) (d6-7a2-5p rn)) (equal (read-rn oplen rn (mc-rfile (stepn s 5))) (read-rn oplen rn (mc-rfile s)))) ((disable times lessp))) (prove-lemma mjrty-s1-sn (rewrite) (let ((sn (stepn s (cand-cnt-t a n lst cand i k)))) (implies (mjrty-s1p s a n lst cand i k) (and (equal (mc-status sn) 'running) (equal (mc-pc sn) (linked-rts-addr s)) (equal (iread-dn 32 0 sn) cand) (equal (iread-dn 32 1 sn) (if (lessp (quotient n 2) (cand-cnt n lst cand i k)) 1 0)) (equal (read-rn 32 14 (mc-rfile sn)) (linked-a6 s)) (equal (read-rn 32 15 (mc-rfile sn)) (add 32 (read-an 32 6 s) 8)) (equal (read-mem x (mc-mem sn) l) (read-mem x (mc-mem s) l))))) ((induct (cand-cnt-induct s n lst cand i k)) (disable mjrty-s1p linked-rts-addr rts-addr linked-a6 iread-dn))) (prove-lemma mjrty-s1-sn-rfile (rewrite) (let ((sn (stepn s (cand-cnt-t a n lst cand i k)))) (implies (and (mjrty-s1p s a n lst cand i k) (d2-7a2-5p rn) (leq oplen 32)) (equal (read-rn oplen rn (mc-rfile sn)) (if (d6-7a2-5p rn) (read-rn oplen rn (mc-rfile s)) (get-vlst oplen 0 rn '(2 3 4 5) (movem-saved s 4 16 4)))))) ((induct (cand-cnt-induct s n lst cand i k)) (disable mjrty-s1p))) ; the correctness of MJRTY. (prove-lemma mjrty-statep-info () (implies (mjrty-statep s a n lst) (not (zerop n)))) (prove-lemma mjrty-correctness (rewrite) (let ((sn (stepn s (mjrty-t a n lst)))) (implies (mjrty-statep s a n lst) (and (equal (mc-status sn) 'running) (equal (mc-pc sn) (rts-addr s)) (equal (read-rn 32 14 (mc-rfile sn)) (read-rn 32 14 (mc-rfile s))) (equal (read-rn 32 15 (mc-rfile sn)) (add 32 (read-sp s) 4)) (implies (and (d2-7a2-5p rn) (leq oplen 32)) (equal (read-rn oplen rn (mc-rfile sn)) (read-rn oplen rn (mc-rfile s)))) (implies (disjoint (sub 32 20 (read-sp s)) 32 x k) (equal (read-mem x (mc-mem sn) k) (read-mem x (mc-mem s) k))) (equal (iread-dn 32 0 sn) (mjrty-cand n lst 0 0 0)) (equal (iread-dn 32 1 sn) (if (mjrty-p n lst 0 0 0) 1 0))))) ((use (mjrty-statep-info)) (disable iread-dn linked-a6 linked-rts-addr mjrty-statep mjrty-s0p mjrty-s1p))) (disable mjrty-t) ; in the logic, mjrty is expected to have these properties: ; 1. mjrty-thm-1: if mjrty-p returns 1, cand wins the majority. ; 2. mjrty-thm-2: if mjrty-p returns 0, no one wins the majority. (prove-lemma mjrty-cand-0 (rewrite) (equal (mjrty-cand n lst x n k) x) ((expand (mjrty-cand n lst x n k)))) (prove-lemma mjrty-cand-1 (rewrite) (equal (mjrty-cand (add1 n) lst x n k) (if (zerop k) (get-nth n lst) x)) ((expand (mjrty-cand (add1 n) lst x n k)))) (prove-lemma mjrty-k-0 (rewrite) (equal (mjrty-k n lst x n k) k) ((expand (mjrty-k n lst x n k)))) (prove-lemma mjrty-k-1 (rewrite) (equal (mjrty-k (add1 n) lst x n k) (if (zerop k) 1 (if (equal x (get-nth n lst)) (add1 k) (sub1 k)))) ((expand (mjrty-k (add1 n) lst x n k)))) (prove-lemma cand-cnt-0 (rewrite) (equal (cand-cnt n lst x n k) k) ((expand (cand-cnt n lst x n k)))) (prove-lemma cand-cnt-1 (rewrite) (equal (cand-cnt (add1 n) lst x n k) (if (equal x (get-nth n lst)) (add1 k) k)) ((expand (cand-cnt (add1 n) lst x n k)))) (prove-lemma mjrty-k-lemma (rewrite) (implies (and (leq i n) (leq j i) (numberp i)) (equal (mjrty-k n lst (mjrty-cand i lst x j k) i (mjrty-k i lst x j k)) (mjrty-k n lst x j k))) ((enable get-nth))) (prove-lemma mjrty-cand-lemma (rewrite) (implies (and (leq i n) (leq j i) (numberp i)) (equal (mjrty-cand n lst (mjrty-cand i lst x j k) i (mjrty-k i lst x j k)) (mjrty-cand n lst x j k))) ((enable get-nth))) (prove-lemma cand-cnt-lemma (rewrite) (implies (and (leq i n) (leq j i) (numberp i)) (equal (cand-cnt n lst x i (cand-cnt i lst x j k)) (cand-cnt n lst x j k))) ((enable get-nth))) (prove-lemma mjrty-cand-rec (rewrite) (implies (numberp n) (equal (mjrty-cand (add1 n) lst x 0 0) (mjrty-cand (add1 n) lst (mjrty-cand n lst x 0 0) n (mjrty-k n lst x 0 0))))) (prove-lemma mjrty-k-rec (rewrite) (implies (numberp n) (equal (mjrty-k (add1 n) lst x 0 0) (mjrty-k (add1 n) lst (mjrty-cand n lst x 0 0) n (mjrty-k n lst x 0 0))))) (prove-lemma cand-cnt-rec (rewrite) (implies (numberp n) (equal (cand-cnt (add1 n) lst x 0 0) (cand-cnt (add1 n) lst x n (cand-cnt n lst x 0 0))))) (disable mjrty-cand-lemma) (disable mjrty-k-lemma) (disable cand-cnt-lemma) (prove-lemma mjrty-lemma1 (rewrite) (not (lessp (cand-cnt n lst (mjrty-cand n lst 0 0 0) 0 0) (mjrty-k n lst 0 0 0))) ((induct (plus n y)))) (defn mjrty-lemma2-induct (n lst x) (if (zerop n) t (and (mjrty-lemma2-induct (sub1 n) lst x) (mjrty-lemma2-induct (sub1 n) lst (get-nth (sub1 n) lst))))) (prove-lemma mjrty-lemma2 (rewrite) (and (not (lessp (plus n (mjrty-k n lst 0 0 0)) (times 2 (cand-cnt n lst (mjrty-cand n lst 0 0 0) 0 0)))) (implies (not (equal x (mjrty-cand n lst 0 0 0))) (not (lessp n (plus (mjrty-k n lst 0 0 0) (times 2 (cand-cnt n lst x 0 0))))))) ((induct (mjrty-lemma2-induct n lst x)))) (disable mjrty-cand-rec) (disable mjrty-k-rec) (disable cand-cnt-rec) (prove-lemma mjrty-thm1 (rewrite) (implies (mjrty-p n lst 0 0 0) (lessp (quotient n 2) (cand-cnt n lst (mjrty-cand n lst 0 0 0) 0 0)))) (prove-lemma mjrty-thm2 (rewrite) (implies (not (mjrty-p n lst 0 0 0)) (not (lessp (quotient n 2) (cand-cnt n lst x 0 0)))) ((use (mjrty-lemma2)))) ; a simple time analysis. (prove-lemma mjrty-t-crock (rewrite) (equal (times z (difference (sub1 x) y)) (difference (times z (difference x y)) z))) (prove-lemma mjrty-cand-t-0 (rewrite) (and (equal (mjrty-cand-t a 0 lst cand i k) (if (equal cand (get-nth 0 lst)) 18 17)) (equal (mjrty-cand-t a 1 lst cand 1 k) (if (equal cand (get-nth 0 lst)) 18 17)))) (prove-lemma mjrty-cand-t-1 (rewrite) (equal (mjrty-cand-t a 1 lst cand i k) (if (zerop i) (if (zerop k) 26 (if (equal cand (get-nth i lst)) (if (equal cand (get-nth 0 lst)) 27 26) (if (equal cand (get-nth 0 lst)) 26 25))) (if (equal cand (get-nth 0 lst)) 18 17))) ((expand (mjrty-cand-t a 1 lst cand i k)) (enable get-nth-0))) (prove-lemma mjrty-cand-t-ubound (rewrite) (not (lessp (plus 18 (times 9 (difference n i))) (mjrty-cand-t a n lst cand i k))) ((enable splus times) (expand (mjrty-cand-t a 1 lst cand i k)))) (prove-lemma mjrty-sn-t-ubound (rewrite) (not (lessp (plus 17 (times 9 (difference n i))) (mjrty-sn-t a n lst cand i k))) ((enable splus times))) (prove-lemma cand-cnt-t-0 (rewrite) (and (equal (cand-cnt-t a 0 lst cand i k) (if (lessp 0 k) 14 13)) (equal (cand-cnt-t a n lst cand n k) (if (lessp (quotient n 2) k) 14 13))) ((expand (cand-cnt-t a n lst cand n k)))) (prove-lemma cand-cnt-t-1 (rewrite) (equal (cand-cnt-t a 1 lst cand i k) (if (zerop i) (if (equal cand (get-nth i lst)) 20 (if (lessp 0 k) 19 18)) (if (lessp 0 k) 14 13))) ((expand (cand-cnt-t a 1 lst cand i k)))) (prove-lemma cand-cnt-t-ubound (rewrite) (not (lessp (plus 14 (times 6 (difference n i))) (cand-cnt-t a n lst cand i k))) ((enable splus times))) (prove-lemma mjrty-t-ubound () (leq (mjrty-t a n lst) (plus 46 (times 15 (sub1 n)))) ((enable splus mjrty-t)))