#|
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.
|#

Event: Start with the library "mc20-2" using the compiled version.

;         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 <mjrty>:         linkw a6,#0
0x2314 <mjrty+4>:       moveml d2-d5,sp@-
0x2318 <mjrty+8>:       moveal a6@(8),a0
0x231c <mjrty+12>:      movel a6@(12),d2
0x2320 <mjrty+16>:      clrl d1
0x2322 <mjrty+18>:      clrl d0

0x2324 <mjrty+20>:      cmpl d0,d2
0x2326 <mjrty+22>:      ble 0x2346 <mjrty+54>
0x2328 <mjrty+24>:      tstl d1
0x232a <mjrty+26>:      bne 0x2334 <mjrty+36>
0x232c <mjrty+28>:      movel 0(a0)[d0.l*4],d3
0x2330 <mjrty+32>:      movel #1,d1
0x2332 <mjrty+34>:      bra 0x2340 <mjrty+48>
0x2334 <mjrty+36>:      cmpl 0(a0)[d0.l*4],d3
0x2338 <mjrty+40>:      bne 0x233e <mjrty+46>
0x233a <mjrty+42>:      addql #1,d1
0x233c <mjrty+44>:      bra 0x2340 <mjrty+48>
0x233e <mjrty+46>:      subl #1,d1
0x2340 <mjrty+48>:      addql #1,d0
0x2342 <mjrty+50>:      cmpl d0,d2
0x2344 <mjrty+52>:      bgt 0x2328 <mjrty+24>
0x2346 <mjrty+54>:      movel d3,d4
0x2348 <mjrty+56>:      tstl d1
0x234a <mjrty+58>:      beq 0x2382 <mjrty+114>
0x234c <mjrty+60>:      movel d2,d0
0x234e <mjrty+62>:      bge 0x2352 <mjrty+66>
0x2350 <mjrty+64>:      addql #1,d0
0x2352 <mjrty+66>:      asrl #1,d0
0x2354 <mjrty+68>:      cmpl d1,d0
0x2356 <mjrty+70>:      bge 0x235c <mjrty+76>
0x2358 <mjrty+72>:      movel #1,d5
0x235a <mjrty+74>:      bra 0x2384 <mjrty+116>
0x235c <mjrty+76>:      clrl d1
0x235e <mjrty+78>:      clrl d0
0x2360 <mjrty+80>:      cmpl d0,d2
0x2362 <mjrty+82>:      ble 0x2372 <mjrty+98>
0x2364 <mjrty+84>:      cmpl 0(a0)[d0.l*4],d3
0x2368 <mjrty+88>:      bne 0x236c <mjrty+92>
0x236a <mjrty+90>:      addql #1,d1
0x236c <mjrty+92>:      addql #1,d0
0x236e <mjrty+94>:      cmpl d0,d2
0x2370 <mjrty+96>:      bgt 0x2364 <mjrty+84>
0x2372 <mjrty+98>:      movel d2,d0
0x2374 <mjrty+100>:     bge 0x2378 <mjrty+104>
0x2376 <mjrty+102>:     addql #1,d0
0x2378 <mjrty+104>:     asrl #1,d0
0x237a <mjrty+106>:     cmpl d1,d0
0x237c <mjrty+108>:     bge 0x2382 <mjrty+114>
0x237e <mjrty+110>:     movel #1,d5
0x2380 <mjrty+112>:     bra 0x2384 <mjrty+116>

0x2382 <mjrty+114>:     clrl d5
0x2384 <mjrty+116>:     movel d4,d0
0x2386 <mjrty+118>:     movel d5,d1
0x2388 <mjrty+120>:     moveml a6@(-16),d2-d5
0x238e <mjrty+126>:     unlk a6
0x2390 <mjrty+128>:     rts
The machine code of the above program is:

<mjrty>:      0x4e56  0x0000  0x48e7  0x3c00  0x206e  0x0008  0x242e  0x000c
<mjrty+16>:   0x4281  0x4280  0xb480  0x6f1e  0x4a81  0x6608  0x2630  0x0c00
<mjrty+32>:   0x7201  0x600c  0xb6b0  0x0c00  0x6604  0x5281  0x6002  0x5381
<mjrty+48>:   0x5280  0xb480  0x6ee2  0x2803  0x4a81  0x6736  0x2002  0x6c02
<mjrty+64>:   0x5280  0xe280  0xb081  0x6c04  0x7a01  0x6028  0x4281  0x4280
<mjrty+80>:   0xb480  0x6f0e  0xb6b0  0x0c00  0x6602  0x5281  0x5280  0xb480
<mjrty+96>:   0x6ef2  0x2002  0x6c02  0x5280  0xe280  0xb081  0x6c04  0x7a01
<mjrty+112>:  0x6002  0x4285  0x2004  0x2205  0x4cee  0x003c  0xfff0  0x4e5e
<mjrty+128>:  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).

Definition: 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.

Definition: mjrty-cand (n, lst, cand, i, k) = if i < n

then if k ≃ 0 then mjrty-cand (n, lst, get-nth (i, lst), 1 + i, 1) elseif cand = get-nth (i, lst) then mjrty-cand (n, lst, cand, 1 + i, 1 + k) else mjrty-cand (n, lst, cand, 1 + i, k − 1) endif

else cand endif

Definition: mjrty-k (n, lst, cand, i, k) = if i < n

then if k ≃ 0 then mjrty-k (n, lst, get-nth (i, lst), 1 + i, 1)

elseif cand = get-nth (i, lst)

then mjrty-k (n, lst, cand, 1 + i, 1 + k) else mjrty-k (n, lst, cand, 1 + i, k − 1) endif

else k endif

; cand-cnt is a function in the logic to simulate the process of
; counting the number of votes for the given candidate.

Definition: cand-cnt (n, lst, cand, i, k) = if i < n

then if cand = get-nth (i, lst) then cand-cnt (n, lst, cand, 1 + i, 1 + k)

else cand-cnt (n, lst, cand, 1 + i, k) endif else k endif

; mjrty-p determines if the given candidate cand has received a majority
; voting.

Definition: mjrty-p (n, lst, cand, i, k) = if mjrty-k (n, lst, cand, i, k) ≃ 0 then f

elseif (n ÷ 2) < mjrty-k (n, lst, cand, i, k) then t else (n ÷ 2)

< cand-cnt (n, lst, mjrty-cand (n, lst, cand, i, k), i, k) endif

; the computation time.

Definition: mjrty-cand-t (a, n, lst, cand, i, k) = if i < n

then if k ≃ 0

then let cand1 be get-nth (i, lst)

in

splus (8, mjrty-cand-t (a, n, lst, cand1 , 1 + i, 1)) endlet elseif cand = get-nth (i, lst) then splus (9, mjrty-cand-t (a, n, lst, cand, 1 + i, 1 + k)) else splus (8, mjrty-cand-t (a, n, lst, cand, 1 + i, k − 1)) endif

elseif cand = get-nth (0, lst) then 18

else 17 endif

Definition: mjrty-sn-t (a, n, lst, cand, i, k) = if i < n

then if k ≃ 0

then let cand1 be get-nth (i, lst)

in

splus (8, mjrty-sn-t (a, n, lst, cand1 , 1 + i, 1)) endlet elseif cand = get-nth (i, lst) then splus (9, mjrty-sn-t (a, n, lst, cand, 1 + i, 1 + k)) else splus (8, mjrty-sn-t (a, n, lst, cand, 1 + i, k − 1)) endif

elseif k ≃ 0 then 11

else 17 endif

Definition: cand-cnt-t (a, n, lst, cand, i, k) = if i < n

then if cand = get-nth (i, lst)

then splus (6, cand-cnt-t (a, n, lst, cand, 1 + i, 1 + k)) else splus (5, cand-cnt-t (a, n, lst, cand, 1 + i, k)) endif

elseif (n ÷ 2) < k then 14

else 13 endif

Definition: mjrty-t (a, n, lst) = let cand be get-nth (0, lst)

in

splus (14,

if (mjrty-k (n, lst, cand, 1, 1) ≃ 0)

∨ ((n ÷ 2) < mjrty-k (n, lst, cand, 1, 1)) then mjrty-sn-t (a, n, lst, cand, 1, 1) else splus (mjrty-cand-t (a, n, lst, cand, 1, 1),

if cand = mjrty-cand (n, lst, cand, 1, 1) then cand-cnt-t (a,

n, lst, mjrty-cand (n,

lst, cand,

                                           1,

1),

                                 1,
                                 1)

else cand-cnt-t (a, n, lst, mjrty-cand (n,

lst, cand,

                                          1,

1),

                                1,

0) endif) endif) endlet

; induction hints.

Definition: mjrty-cand-induct (s, n, lst, cand, i, k) = if i < n

then if k ≃ 0

then let cand1 be get-nth (i, lst)

in

mjrty-cand-induct (stepn (s, 8), n, lst, cand1 , 1 + i, 1) endlet elseif cand = get-nth (i, lst) then mjrty-cand-induct (stepn (s, 9), n, lst, cand, 1 + i, 1 + k) else mjrty-cand-induct (stepn (s, 8), n, lst, cand, 1 + i, k − 1) endif

else t endif

Definition: cand-cnt-induct (s, n, lst, cand, i, k) = if i < n

then if cand = get-nth (i, lst) then cand-cnt-induct (stepn (s, 6), n, lst, cand, 1 + i, 1 + k) else cand-cnt-induct (stepn (s, 5), n, lst, cand, 1 + i, k) endif

else t endif

; the preconditions of the initial state.

Definition: mjrty-statep (s, a, n, lst) = ((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), 4 ∗ n) ∧ mem-ilst (4, a, mc-mem (s), n, lst) ∧ disjoint (a, 4 ∗ n, sub (32, 20, read-sp (s)), 32) ∧ (a = read-mem (add (32, read-sp (s), 4), mc-mem (s), 4)) ∧ (n = iread-mem (add (32, read-sp (s), 8), mc-mem (s), 4)) ∧ (n ≄ 0))

; the conditions of the intermediate state s0.

Definition: mjrty-s0p (s, a, n, lst, cand, i, k) = ((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), 4 ∗ n) ∧ mem-ilst (4, a, mc-mem (s), n, lst) ∧ disjoint (a, 4 ∗ n, sub (32, 16, read-an (32, 6, s)), 32) ∧ (a = read-rn (32, 8, mc-rfile (s))) ∧ (n = nat-to-int (read-rn (32, 2, mc-rfile (s)), 32)) ∧ (cand = nat-to-int (read-rn (32, 3, mc-rfile (s)), 32)) ∧ (i = nat-to-int (read-rn (32, 0, mc-rfile (s)), 32)) ∧ (k = nat-to-int (read-rn (32, 1, mc-rfile (s)), 32)) ∧ (n ≄ 0) ∧ (i ∈ N) ∧ (k ∈ N) ∧ (k ≤ i))

; the conditions of the intermediate state s1.

Definition: mjrty-s1p (s, a, n, lst, cand, i, k) = ((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), 4 ∗ n) ∧ mem-ilst (4, a, mc-mem (s), n, lst) ∧ disjoint (a, 4 ∗ n, sub (32, 16, read-an (32, 6, s)), 32) ∧ (a = read-rn (32, 8, mc-rfile (s))) ∧ (n = nat-to-int (read-rn (32, 2, mc-rfile (s)), 32)) ∧ (cand = nat-to-int (read-rn (32, 4, mc-rfile (s)), 32)) ∧ (cand = nat-to-int (read-rn (32, 3, mc-rfile (s)), 32)) ∧ (i = nat-to-int (read-rn (32, 0, mc-rfile (s)), 32)) ∧ (k = nat-to-int (read-rn (32, 1, mc-rfile (s)), 32)) ∧ (n ≄ 0) ∧ (i ∈ N) ∧ (k ∈ N) ∧ (k ≤ i))

; the initial segment.  From the initial state to s0.

Theorem: mjrty-s-s0 let cand be get-nth (0, lst) in mjrty-statep (s, a, n, lst) → (mjrty-s0p (stepn (s, 14), a, n, lst, cand, 1, 1)

∧ (linked-rts-addr (stepn (s, 14)) = rts-addr (s)) ∧ (linked-a6 (stepn (s, 14)) = read-an (32, 6, s)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 14)))

= sub (32, 4, read-sp (s))) ∧ (movem-saved (stepn (s, 14), 4, 16, 4)

= readm-rn (32, '(2 3 4 5), mc-rfile (s)))) endlet

Theorem: mjrty-s-s0-rfile (mjrty-statep (s, a, n, lst) ∧ d6-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 14)))

= read-rn (oplen, rn, mc-rfile (s)))

Theorem: mjrty-s-s0-mem (mjrty-statep (s, a, n, lst) ∧ disjoint (sub (32, 20, read-sp (s)), 32, x, k)) → (read-mem (x, mc-mem (stepn (s, 14)), k) = read-mem (x, mc-mem (s), k))

; s0 --> exit.
; base case.

Theorem: mjrty-s0-sn-base-1 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ (k ≃ 0)) → ((mc-status (stepn (s, 11)) = 'running)

∧ (mc-pc (stepn (s, 11)) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, 11)) = cand) ∧ (iread-dn (32, 1, stepn (s, 11)) = 0) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 11))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 11)))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, 11)), l)

= read-mem (x, mc-mem (s), l)))

Theorem: mjrty-s0-sn-base-2 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ (k ≄ 0) ∧ ((n ÷ 2) < k)) → ((mc-status (stepn (s, 17)) = 'running)

∧ (mc-pc (stepn (s, 17)) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, 17)) = cand) ∧ (iread-dn (32, 1, stepn (s, 17)) = 1) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 17))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 17)))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, 17)), l)

= read-mem (x, mc-mem (s), l)))

Theorem: mjrty-s0-sn-rfile-base-1 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ (k ≃ 0) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 11)))

= if d6-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s))

else get-vlst (oplen,

               0,

rn,

               '(2 3 4 5),

movem-saved (s, 4, 16, 4)) endif)

Theorem: mjrty-s0-sn-rfile-base-2 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ (k ≄ 0) ∧ ((n ÷ 2) < k) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 17)))

= if d6-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s))

else get-vlst (oplen,

                    0,

rn,

                    '(2 3 4 5),

movem-saved (s, 4, 16, 4)) endif)

; induction case.

Theorem: add1-int-rangep (x < nat-to-int (y, n)) → int-rangep (1 + x, n)

Event: Enable iplus.

Theorem: mjrty-s0-s0-1 let cand1 be get-nth (i, lst) in (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i < n) ∧ (k ≃ 0)) → (mjrty-s0p (stepn (s, 8), a, n, lst, cand1 , 1 + i, 1)

∧ (linked-rts-addr (stepn (s, 8)) = linked-rts-addr (s)) ∧ (linked-a6 (stepn (s, 8)) = linked-a6 (s)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 8))) = read-rn (32, 14, mc-rfile (s))) ∧ (movem-saved (stepn (s, 8), 4, 16, 4) = movem-saved (s, 4, 16, 4)) ∧ (read-mem (x, mc-mem (stepn (s, 8)), l)

= read-mem (x, mc-mem (s), l))) endlet

Theorem: add1-int-rangepxx ((i ≤ r) ∧ (r < n) ∧ int-rangep (n, 32)) → int-rangep (1 + i, 32)

Theorem: mjrty-s0-s0-2 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i < n) ∧ (k ≄ 0) ∧ (cand = get-nth (i, lst))) → (mjrty-s0p (stepn (s, 9), a, n, lst, cand, 1 + i, 1 + k)

∧ (linked-rts-addr (stepn (s, 9)) = linked-rts-addr (s)) ∧ (linked-a6 (stepn (s, 9)) = linked-a6 (s)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 9)))

= read-rn (32, 14, mc-rfile (s))) ∧ (movem-saved (stepn (s, 9), 4, 16, 4) = movem-saved (s, 4, 16, 4)) ∧ (read-mem (x, mc-mem (stepn (s, 9)), l)

= read-mem (x, mc-mem (s), l)))

Theorem: mjrty-s0-s0-3 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i < n) ∧ (k ≄ 0) ∧ (cand ≠ get-nth (i, lst))) → (mjrty-s0p (stepn (s, 8), a, n, lst, cand, 1 + i, k − 1)

∧ (linked-rts-addr (stepn (s, 8)) = linked-rts-addr (s)) ∧ (linked-a6 (stepn (s, 8)) = linked-a6 (s)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 8)))

= read-rn (32, 14, mc-rfile (s))) ∧ (movem-saved (stepn (s, 8), 4, 16, 4) = movem-saved (s, 4, 16, 4)) ∧ (read-mem (x, mc-mem (stepn (s, 8)), l)

= read-mem (x, mc-mem (s), l)))

Theorem: mjrty-s0-s0-rfile-1 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i < n) ∧ (k ≃ 0) ∧ d6-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 8)))

= read-rn (oplen, rn, mc-rfile (s)))

Theorem: mjrty-s0-s0-rfile-2 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i < n) ∧ (k ≄ 0) ∧ (cand = get-nth (i, lst)) ∧ d6-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 9)))

= read-rn (oplen, rn, mc-rfile (s)))

Theorem: mjrty-s0-s0-rfile-3 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i < n) ∧ (k ≄ 0) ∧ (cand ≠ get-nth (i, lst)) ∧ d6-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 8)))

= read-rn (oplen, rn, mc-rfile (s)))

; the proof of s0 --> exit.

Theorem: mjrty-s0-sn let sn be stepn (s, mjrty-sn-t (a, n, lst, cand, i, k)) in (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ ((mjrty-k (n, lst, cand, i, k) ≃ 0)

∨ ((n ÷ 2) < mjrty-k (n, lst, cand, i, k)))) → ((mc-status (sn) = 'running)

∧ (mc-pc (sn) = linked-rts-addr (s))

∧ (iread-dn (32, 0, sn) = mjrty-cand (n, lst, cand, i, k))

∧ (iread-dn (32, 1, sn)

= if (n ÷ 2) < mjrty-k (n, lst, cand, i, k) then 1 else 0 endif)

∧ (read-rn (32, 14, mc-rfile (sn)) = linked-a6 (s))

∧ (read-rn (32, 15, mc-rfile (sn))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (sn), l) = read-mem (x, mc-mem (s), l))) endlet

Theorem: mjrty-s0-sn-rfile let sn be stepn (s, mjrty-sn-t (a, n, lst, cand, i, k)) in (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ ((mjrty-k (n, lst, cand, i, k) ≃ 0)

∨ ((n ÷ 2) < mjrty-k (n, lst, cand, i, k))) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (sn))

= if d6-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s))

else get-vlst (oplen,

                    0,

rn,

                    '(2 3 4 5),

movem-saved (s, 4, 16, 4)) endif) endlet

; s0 --> s1.
; base case:

Theorem: mjrty-s0-s1-base1 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ (k ≄ 0) ∧ ((n ÷ 2) ≮ k) ∧ (cand = get-nth (0, lst)))

→ (mjrty-s1p (stepn (s, 18), a, n, lst, cand, 1, 1) ∧ (linked-rts-addr (stepn (s, 18)) = linked-rts-addr (s)) ∧ (linked-a6 (stepn (s, 18)) = linked-a6 (s)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 18))) = read-rn (32, 14, mc-rfile (s)))

∧ (movem-saved (stepn (s, 18), 4, 16, 4) = movem-saved (s, 4, 16, 4)) ∧ (read-mem (x, mc-mem (stepn (s, 18)), l) = read-mem (x, mc-mem (s), l)))

Theorem: mjrty-s0-s1-base2 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ (k ≄ 0) ∧ ((n ÷ 2) ≮ k) ∧ (cand ≠ get-nth (0, lst))) → (mjrty-s1p (stepn (s, 17), a, n, lst, cand, 1, 0)

∧ (linked-rts-addr (stepn (s, 17)) = linked-rts-addr (s))

∧ (linked-a6 (stepn (s, 17)) = linked-a6 (s)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 17))) = read-rn (32, 14, mc-rfile (s)))

∧ (movem-saved (stepn (s, 17), 4, 16, 4) = movem-saved (s, 4, 16, 4)) ∧ (read-mem (x, mc-mem (stepn (s, 17)), l) = read-mem (x, mc-mem (s), l)))

Theorem: mjrty-s0-s1-rfile-base1 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ (k ≄ 0) ∧ ((n ÷ 2) ≮ k) ∧ (cand = get-nth (0, lst)) ∧ d6-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 18)))

= read-rn (oplen, rn, mc-rfile (s)))

Theorem: mjrty-s0-s1-rfile-base2 (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ (k ≄ 0) ∧ ((n ÷ 2) ≮ k) ∧ (cand ≠ get-nth (0, lst)) ∧ d6-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 17)))

= read-rn (oplen, rn, mc-rfile (s)))

; the proof of s0 --> s1.

Theorem: mjrty-s0-s1 let s1 be stepn (s, mjrty-cand-t (a, n, lst, cand, i, k)) in (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (mjrty-k (n, lst, cand, i, k) ≄ 0) ∧ ((n ÷ 2) ≮ mjrty-k (n, lst, cand, i, k)) ∧ (cand0 = mjrty-cand (n, lst, cand, i, k)) ∧ (k0 = if mjrty-cand (n, lst, cand, i, k) = get-nth (0, lst)

then 1

else 0 endif))

→ (mjrty-s1p (s1 , a, n, lst, cand0 , 1, k0 )

∧ (linked-rts-addr (s1 ) = linked-rts-addr (s)) ∧ (linked-a6 (s1 ) = linked-a6 (s)) ∧ (read-rn (32, 14, mc-rfile (s1 ))

= read-rn (32, 14, mc-rfile (s))) ∧ (movem-saved (s1 , 4, 16, 4) = movem-saved (s, 4, 16, 4)) ∧ (read-mem (x, mc-mem (s1 ), l) = read-mem (x, mc-mem (s), l))) endlet

Theorem: mjrty-s0-s1-rfile let s1 be stepn (s, mjrty-cand-t (a, n, lst, cand, i, k)) in (mjrty-s0p (s, a, n, lst, cand, i, k) ∧ (mjrty-k (n, lst, cand, i, k) ≄ 0) ∧ ((n ÷ 2) ≮ mjrty-k (n, lst, cand, i, k)) ∧ d6-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (s1 ))

= read-rn (oplen, rn, mc-rfile (s))) endlet

; s1 --> exit.
; base case.

Theorem: mjrty-s1-sn-1 (mjrty-s1p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ ((n ÷ 2) < k)) → ((mc-status (stepn (s, 14)) = 'running)

∧ (mc-pc (stepn (s, 14)) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, 14)) = cand) ∧ (iread-dn (32, 1, stepn (s, 14)) = 1) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 14))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 14)))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, 14)), l)

= read-mem (x, mc-mem (s), l)))

Theorem: mjrty-s1-sn-rfile-1 (mjrty-s1p (s, a, n, lst, cand, i, k)

∧ (i ≮ n) ∧ ((n ÷ 2) < k) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 14)))

= if d6-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s))

else get-vlst (oplen,

               0,

rn,

               '(2 3 4 5),

movem-saved (s, 4, 16, 4)) endif)

Theorem: mjrty-s1-sn-2 (mjrty-s1p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ ((n ÷ 2) ≮ k)) → ((mc-status (stepn (s, 13)) = 'running)

∧ (mc-pc (stepn (s, 13)) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, stepn (s, 13)) = cand) ∧ (iread-dn (32, 1, stepn (s, 13)) = 0) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 13))) = linked-a6 (s)) ∧ (read-rn (32, 15, mc-rfile (stepn (s, 13)))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (stepn (s, 13)), l)

= read-mem (x, mc-mem (s), l)))

Theorem: mjrty-s1-sn-rfile-2 (mjrty-s1p (s, a, n, lst, cand, i, k) ∧ (i ≮ n) ∧ ((n ÷ 2) ≮ k) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 13)))

= if d6-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s))

else get-vlst (oplen,

               0,

rn,

               '(2 3 4 5),

movem-saved (s, 4, 16, 4)) endif)

; induction case.

Theorem: mjrty-s1-s1-1 (mjrty-s1p (s, a, n, lst, cand, i, k) ∧ (i < n) ∧ (cand = get-nth (i, lst))) → (mjrty-s1p (stepn (s, 6), a, n, lst, cand, 1 + i, 1 + k)

∧ (linked-rts-addr (stepn (s, 6)) = linked-rts-addr (s)) ∧ (linked-a6 (stepn (s, 6)) = linked-a6 (s))

∧ (read-rn (32, 14, mc-rfile (stepn (s, 6)))

= read-rn (32, 14, mc-rfile (s))) ∧ (movem-saved (stepn (s, 6), 4, 16, 4) = movem-saved (s, 4, 16, 4)) ∧ (read-mem (x, mc-mem (stepn (s, 6)), l)

= read-mem (x, mc-mem (s), l)))

Theorem: mjrty-s1-s1-2 (mjrty-s1p (s, a, n, lst, cand, i, k) ∧ (i < n) ∧ (cand ≠ get-nth (i, lst))) → (mjrty-s1p (stepn (s, 5), a, n, lst, cand, 1 + i, k)

∧ (linked-rts-addr (stepn (s, 5)) = linked-rts-addr (s)) ∧ (linked-a6 (stepn (s, 5)) = linked-a6 (s)) ∧ (read-rn (32, 14, mc-rfile (stepn (s, 5)))

= read-rn (32, 14, mc-rfile (s))) ∧ (movem-saved (stepn (s, 5), 4, 16, 4) = movem-saved (s, 4, 16, 4)) ∧ (read-mem (x, mc-mem (stepn (s, 5)), l)

= read-mem (x, mc-mem (s), l)))

Theorem: mjrty-s1-s1-rfile-1 (mjrty-s1p (s, a, n, lst, cand, i, k) ∧ (i < n) ∧ (cand = get-nth (i, lst)) ∧ d6-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 6)))

= read-rn (oplen, rn, mc-rfile (s)))

Theorem: mjrty-s1-s1-rfile-2 (mjrty-s1p (s, a, n, lst, cand, i, k) ∧ (i < n) ∧ (cand ≠ get-nth (i, lst)) ∧ d6-7a2-5p (rn)) → (read-rn (oplen, rn, mc-rfile (stepn (s, 5)))

= read-rn (oplen, rn, mc-rfile (s)))

Theorem: mjrty-s1-sn let sn be stepn (s, cand-cnt-t (a, n, lst, cand, i, k)) in mjrty-s1p (s, a, n, lst, cand, i, k) → ((mc-status (sn) = 'running)

∧ (mc-pc (sn) = linked-rts-addr (s)) ∧ (iread-dn (32, 0, sn) = cand) ∧ (iread-dn (32, 1, sn)

= if (n ÷ 2) < cand-cnt (n, lst, cand, i, k) then 1 else 0 endif)

∧ (read-rn (32, 14, mc-rfile (sn)) = linked-a6 (s))

∧ (read-rn (32, 15, mc-rfile (sn))

= add (32, read-an (32, 6, s), 8)) ∧ (read-mem (x, mc-mem (sn), l) = read-mem (x, mc-mem (s), l))) endlet

Theorem: mjrty-s1-sn-rfile let sn be stepn (s, cand-cnt-t (a, n, lst, cand, i, k)) in (mjrty-s1p (s, a, n, lst, cand, i, k) ∧ d2-7a2-5p (rn) ∧ (oplen ≤ 32)) → (read-rn (oplen, rn, mc-rfile (sn))

= if d6-7a2-5p (rn) then read-rn (oplen, rn, mc-rfile (s))

else get-vlst (oplen,

               0,

rn,

               '(2 3 4 5),

movem-saved (s, 4, 16, 4)) endif) endlet

; the correctness of MJRTY.

Theorem: mjrty-statep-info mjrty-statep (s, a, n, lst) → (n ≄ 0)

Theorem: mjrty-correctness let sn be stepn (s, mjrty-t (a, n, lst)) in mjrty-statep (s, a, n, lst) → ((mc-status (sn) = 'running)

∧ (mc-pc (sn) = rts-addr (s)) ∧ (read-rn (32, 14, mc-rfile (sn))

= read-rn (32, 14, mc-rfile (s))) ∧ (read-rn (32, 15, mc-rfile (sn))

= add (32, read-sp (s), 4)) ∧ ((d2-7a2-5p (rn) ∧ (oplen ≤ 32))

→ (read-rn (oplen, rn, mc-rfile (sn))

= read-rn (oplen, rn, mc-rfile (s))))

∧ (disjoint (sub (32, 20, read-sp (s)), 32, x, k)

→ (read-mem (x, mc-mem (sn), k)

= read-mem (x, mc-mem (s), k)))

∧ (iread-dn (32, 0, sn) = mjrty-cand (n, lst, 0, 0, 0)) ∧ (iread-dn (32, 1, sn)

= if mjrty-p (n, lst, 0, 0, 0) then 1 else 0 endif)) endlet

Event: 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.

Theorem: mjrty-cand-0 mjrty-cand (n, lst, x, n, k) = x

Theorem: mjrty-cand-1 mjrty-cand (1 + n, lst, x, n, k) = if k ≃ 0 then get-nth (n, lst)

else x endif

Theorem: mjrty-k-0 mjrty-k (n, lst, x, n, k) = k

Theorem: mjrty-k-1 mjrty-k (1 + n, lst, x, n, k) = if k ≃ 0 then 1

elseif x = get-nth (n, lst) then 1 + k else k − 1 endif

Theorem: cand-cnt-0 cand-cnt (n, lst, x, n, k) = k

Theorem: cand-cnt-1 cand-cnt (1 + n, lst, x, n, k) = if x = get-nth (n, lst) then 1 + k

else k endif

Theorem: mjrty-k-lemma ((i ≤ n) ∧ (j ≤ i) ∧ (i ∈ N)) → (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))

Theorem: mjrty-cand-lemma ((i ≤ n) ∧ (j ≤ i) ∧ (i ∈ N)) → (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))

Theorem: cand-cnt-lemma ((i ≤ n) ∧ (j ≤ i) ∧ (i ∈ N)) → (cand-cnt (n, lst, x, i, cand-cnt (i, lst, x, j , k)) = cand-cnt (n, lst, x, j , k))

Theorem: mjrty-cand-rec (n ∈ N) → (mjrty-cand (1 + n, lst, x, 0, 0)

= mjrty-cand (1 + n, lst, mjrty-cand (n, lst, x, 0, 0), n, mjrty-k (n, lst, x, 0, 0)))

Theorem: mjrty-k-rec (n ∈ N) → (mjrty-k (1 + n, lst, x, 0, 0)

= mjrty-k (1 + n, lst, mjrty-cand (n, lst, x, 0, 0), n, mjrty-k (n, lst, x, 0, 0)))

Theorem: cand-cnt-rec (n ∈ N) → (cand-cnt (1 + n, lst, x, 0, 0)

= cand-cnt (1 + n, lst, x, n, cand-cnt (n, lst, x, 0, 0)))

Event: Disable mjrty-cand-lemma.

Event: Disable mjrty-k-lemma.

Event: Disable cand-cnt-lemma.

Theorem: mjrty-lemma1 cand-cnt (n, lst, mjrty-cand (n, lst, 0, 0, 0), 0, 0) ≮ mjrty-k (n, lst, 0, 0, 0)

Definition: mjrty-lemma2-induct (n, lst, x) = if n ≃ 0 then t

else mjrty-lemma2-induct (n − 1, lst, x) ∧ mjrty-lemma2-induct (n − 1, lst, get-nth (n − 1, lst)) endif

Theorem: mjrty-lemma2 ((n + mjrty-k (n, lst, 0, 0, 0)) ≮ (2 ∗ cand-cnt (n, lst, mjrty-cand (n, lst, 0, 0, 0), 0, 0))) ∧ ((x ≠ mjrty-cand (n, lst, 0, 0, 0))

→ (n ≮ (mjrty-k (n, lst, 0, 0, 0) + (2 ∗ cand-cnt (n, lst, x, 0, 0)))))

Event: Disable mjrty-cand-rec.

Event: Disable mjrty-k-rec.

Event: Disable cand-cnt-rec.

Theorem: mjrty-thm1 mjrty-p (n, lst, 0, 0, 0) → ((n ÷ 2) < cand-cnt (n, lst, mjrty-cand (n, lst, 0, 0, 0), 0, 0))

Theorem: mjrty-thm2 (¬ mjrty-p (n, lst, 0, 0, 0)) → ((n ÷ 2) ≮ cand-cnt (n, lst, x, 0, 0))

; a simple time analysis.

Theorem: mjrty-t-crock (z ∗ ((x − 1) − y)) = ((z ∗ (x − y)) − z)

Theorem: mjrty-cand-t-0 (mjrty-cand-t (a, 0, lst, cand, i, k) = if cand = get-nth (0, lst) then 18

else 17 endif) ∧ (mjrty-cand-t (a, 1, lst, cand, 1, k)

= if cand = get-nth (0, lst) then 18 else 17 endif)

Theorem: mjrty-cand-t-1 mjrty-cand-t (a, 1, lst, cand, i, k) = if i ≃ 0

then if k ≃ 0 then 26 elseif cand = get-nth (i, lst) then if cand = get-nth (0, lst) then 27

else 26 endif elseif cand = get-nth (0, lst) then 26 else 25 endif

elseif cand = get-nth (0, lst) then 18 else 17 endif

Theorem: mjrty-cand-t-ubound (18 + (9 ∗ (n − i))) ≮ mjrty-cand-t (a, n, lst, cand, i, k)

Theorem: mjrty-sn-t-ubound (17 + (9 ∗ (n − i))) ≮ mjrty-sn-t (a, n, lst, cand, i, k)

Theorem: cand-cnt-t-0 (cand-cnt-t (a, 0, lst, cand, i, k) = if 0 < k then 14

else 13 endif) ∧ (cand-cnt-t (a, n, lst, cand, n, k)

= if (n ÷ 2) < k then 14 else 13 endif)

Theorem: cand-cnt-t-1 cand-cnt-t (a, 1, lst, cand, i, k) = if i ≃ 0

then if cand = get-nth (i, lst) then 20 elseif 0 < k then 19 else 18 endif elseif 0 < k then 14 else 13 endif

Theorem: cand-cnt-t-ubound (14 + (6 ∗ (n − i))) ≮ cand-cnt-t (a, n, lst, cand, i, k)

Theorem: mjrty-t-ubound mjrty-t (a, n, lst) ≤ (46 + (15 ∗ (n − 1)))

Index

add, 8, 10, 13, 15, 16, 18 add1-int-rangep, 11 add1-int-rangepxx, 11

cand-cnt, 5, 6, 17, 19–21 cand-cnt-0, 19 cand-cnt-1, 19 cand-cnt-induct, 7, 8 cand-cnt-lemma, 19 cand-cnt-rec, 20 cand-cnt-t, 6, 7, 17, 18, 21, 22 cand-cnt-t-0, 21 cand-cnt-t-1, 22 cand-cnt-t-ubound, 22

d2-7a2-5p, 10, 11, 13, 16, 18 d6-7a2-5p, 9–18 disjoint, 8, 9, 18

evenp, 8, 9

get-nth, 5–9, 11–17, 19–22 get-vlst, 10, 11, 13, 16, 18

int-rangep, 11 iread-dn, 10, 13, 15–18 iread-mem, 8

linked-a6, 9–17 linked-rts-addr, 9–17

mc-mem, 8–18 mc-pc, 8–10, 13, 15–18 mc-rfile, 8–18 mc-status, 8–10, 13, 15–18 mcode-addrp, 8, 9 mem-ilst, 8, 9 mjrty-cand, 5–7, 13, 15, 18–21 mjrty-cand-0, 19 mjrty-cand-1, 19 mjrty-cand-induct, 7 mjrty-cand-lemma, 19 mjrty-cand-rec, 19 mjrty-cand-t, 6, 7, 15, 21 mjrty-cand-t-0, 21 mjrty-cand-t-1, 21 mjrty-cand-t-ubound, 21 mjrty-code, 4, 5, 8, 9 mjrty-correctness, 18 mjrty-k, 5–7, 13, 15, 19, 20 mjrty-k-0, 19 mjrty-k-1, 19 mjrty-k-lemma, 19 mjrty-k-rec, 20 mjrty-lemma1, 20 mjrty-lemma2, 20 mjrty-lemma2-induct, 20 mjrty-p, 6, 18, 21 mjrty-s-s0, 9 mjrty-s-s0-mem, 9 mjrty-s-s0-rfile, 9 mjrty-s0-s0-1, 11 mjrty-s0-s0-2, 11 mjrty-s0-s0-3, 12 mjrty-s0-s0-rfile-1, 12 mjrty-s0-s0-rfile-2, 12 mjrty-s0-s0-rfile-3, 12 mjrty-s0-s1, 15 mjrty-s0-s1-base1, 13 mjrty-s0-s1-base2, 14 mjrty-s0-s1-rfile, 15 mjrty-s0-s1-rfile-base1, 14 mjrty-s0-s1-rfile-base2, 14 mjrty-s0-sn, 13 mjrty-s0-sn-base-1, 10 mjrty-s0-sn-base-2, 10 mjrty-s0-sn-rfile, 13 mjrty-s0-sn-rfile-base-1, 10 mjrty-s0-sn-rfile-base-2, 11 mjrty-s0p, 8–15 mjrty-s1-s1-1, 16 mjrty-s1-s1-2, 17 mjrty-s1-s1-rfile-1, 17 mjrty-s1-s1-rfile-2, 17 mjrty-s1-sn, 17 mjrty-s1-sn-1, 15 mjrty-s1-sn-2, 16 mjrty-s1-sn-rfile, 18 mjrty-s1-sn-rfile-1, 15 mjrty-s1-sn-rfile-2, 16 mjrty-s1p, 9, 14–18 mjrty-sn-t, 6, 7, 13, 21 mjrty-sn-t-ubound, 21 mjrty-statep, 8, 9, 18 mjrty-statep-info, 18 mjrty-t, 6, 7, 18, 22 mjrty-t-crock, 21 mjrty-t-ubound, 22 mjrty-thm1, 21 mjrty-thm2, 21 movem-saved, 9–18

nat-to-int, 8, 9, 11

ram-addrp, 8, 9 read-an, 8–10, 13, 15, 16, 18 read-mem, 8–18 read-rn, 8–18 read-sp, 8, 9, 18 readm-rn, 9 rom-addrp, 8, 9 rts-addr, 9, 18

splus, 6, 7 stepn, 7–18 sub, 8, 9, 18