1
2open HolKernel boolLib bossLib Parse; val _ = new_theory "arm_cheney_gc";
3
4open decompilerLib prog_armLib;
5
6open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory;
7open combinTheory finite_mapTheory addressTheory;
8open tailrecLib tailrecTheory;
9open cheney_gcTheory; (* an abstract implementation is imported *)
10
11val decompile_arm = decompile arm_tools;
12val basic_decompile_arm = basic_decompile arm_tools;
13
14
15
16infix \\ << >>
17val op \\ = op THEN;
18val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"];
19val RW = REWRITE_RULE;
20val RW1 = ONCE_REWRITE_RULE;
21
22
23val (th,def1) = decompile_arm "arm_move" `
24  E3550000 (* cmp r5,#0 *)
25  0A000009 (* beq L1 *)
26  E5957000 (* ldr r7,[r5] *)
27  E3170001 (* tst r7,#1 *)
28  04847004 (* streq r7,[r4],#4 *)
29  05958004 (* ldreq r8,[r5,#4] *)
30  05957008 (* ldreq r7,[r5,#8] *)
31  04848004 (* streq r8,[r4],#4 *)
32  04847004 (* streq r7,[r4],#4 *)
33  0244700B (* subeq r7,r4,#11 *)
34  05857000 (* streq r7,[r5] *)
35  E2475001 (* sub r5,r7,#1 *)`;
36
37val (th,def2) = decompile_arm "arm_move2" `
38  E3560000 (* cmp r6,#0 *)
39  0A000009 (* beq L2 *)
40  E5967000 (* ldr r7,[r6] *)
41  E3170001 (* tst r7,#1 *)
42  04847004 (* streq r7,[r4],#4 *)
43  05968004 (* ldreq r8,[r6,#4] *)
44  05967008 (* ldreq r7,[r6,#8] *)
45  04848004 (* streq r8,[r4],#4 *)
46  04847004 (* streq r7,[r4],#4 *)
47  0244700B (* subeq r7,r4,#11 *)
48  05867000 (* streq r7,[r6] *)
49  E2476001 (* sub r6,r7,#1 *)`;
50
51val (th,def3) = decompile_arm "arm_cheney_step" `
52  E5935000 (* ldr r5,[r3] *)
53  E5936004 (* ldr r6,[r3,#4] *)
54  insert: arm_move
55  insert: arm_move2
56  E4835004 (* L2:str r5,[r3],#4 *)
57  E4836004 (* str r6,[r3],#4 *)
58  E2833004 (* add r3,r3,#4 *)`;
59
60val (th,def4) = basic_decompile_arm "arm_cheney_loop"NONE `
61  E1530004 (* CHENEY:cmp r3,r4 *)
62  0A00001D (* beq EXIT *)
63  insert: arm_cheney_step
64  EAFFFFDF (* b CHENEY *)`;
65
66val (th,def5) = basic_decompile_arm "arm_move_roots" NONE `
67  E3560000 (* ROOTS:cmp r6,#0 *)
68  0A00000F (* beq CHENEY *)
69  E5995000 (* ldr r5,[r9] *)
70  insert: arm_move
71  E2466001 (* RL:sub r6,r6,#1 *)
72  E4895004 (* str r5,[r9],#4 *)
73  EAFFFFED (* b ROOTS *)`;
74
75val (th,def6) = decompile_arm "arm_c_init" `
76  E2355001 (* eors r5,r5,#1 *)    (* calc u *)
77  E289300C (* add r3,r9,#12 *)    (* set i *)
78  00833006 (* addeq r3,r3,r6 *)`;
79
80val (th,def7) = decompile_arm "arm_collect" `
81  E519501C (* ldr r5,[r9,#-28] *)
82  E5196020 (* ldr r6,[r9,#-32] *)
83  insert: arm_c_init
84  E509501C (* str r5,[r9,#-28] *)
85  E0835006 (* add r5,r3,r6 *)
86  E1A04003 (* mov r4,r3 *)
87  E5895004 (* str r5,[r9,#4] *)
88  E3A06006 (* mov r6,#6 *)
89  E2499018 (* sub r9,r9,#24 *)
90  insert: arm_move_roots
91  insert: arm_cheney_loop  (* main loop *)
92  E5994004 (* EXIT:ldr r4,[r9,#4] *)`;
93
94val (th,def8) = decompile_arm "arm_alloc_gc" `
95  E1530004 (* cmp r3,r4 *)
96  1A00003D (* bne NO_GC *)
97  insert: arm_collect`;
98
99val (th,def9) = decompile_arm "arm_alloc_aux" `
100  E5197018 (* NO_GC:ldr r7,[r9,#-24] *)
101  E5198014 (* ldr r8,[r9,#-20] *)
102  E3A06000 (* mov r6,#0 *)
103  E1530004 (* cmp r3,r4 *)
104  15093018 (* strne r3,[r9,#-24] *)
105  14837004 (* strne r7,[r3],#4 *)
106  14838004 (* strne r8,[r3],#4 *)
107  14836004 (* strne r6,[r3],#4 *)
108  03A07000 (* moveq r7,#0 *)
109  05097018 (* streq r7,[r9,#-24] *)
110  E5893000 (* str r3,[r9] *)`;
111
112val (th,def10) = decompile_arm "arm_alloc_mem" `
113  E5993000 (* ldr r3,[r9] *)
114  E5994004 (* ldr r4,[r9,#4] *)
115  insert: arm_alloc_gc
116  insert: arm_alloc_aux`;
117
118val (arm_alloc_thm,def11) = decompile_arm "arm_alloc" `
119  E5093018 (* str r3,[r9,#-24] *)
120  E5094014 (* str r4,[r9,#-20] *)
121  E5095010 (* str r5,[r9,#-16] *)
122  E509600C (* str r6,[r9,#-12] *)
123  E5097008 (* str r7,[r9,#-8] *)
124  E5098004 (* str r8,[r9,#-4] *)
125  insert: arm_alloc_mem
126  E5193018 (* ldr r3,[r9,#-24] *)
127  E5194014 (* ldr r4,[r9,#-20] *)
128  E5195010 (* ldr r5,[r9,#-16] *)
129  E519600C (* ldr r6,[r9,#-12] *)
130  E5197008 (* ldr r7,[r9,#-8] *)
131  E5198004 (* ldr r8,[r9,#-4] *)`;
132
133val _ = save_thm("arm_alloc_thm",arm_alloc_thm);
134
135
136(* proof *)
137
138val ref_addr_def = Define `
139  (ref_addr a n = if n = 0 then 0w:word32 else a + n2w (12 * n))`;
140
141val ref_mem_def = Define `
142  (ref_mem i EMP (a,xs) = T) /\
143  (ref_mem i (REF j) (a,xs) =
144    (xs (ref_addr a i) = ref_addr a j + 1w)) /\
145  (ref_mem i (DATA (x,y,z)) (a,xs) =
146    (xs (ref_addr a i) = ref_addr a x) /\
147    (xs (ref_addr a i + 4w) = ref_addr a y) /\
148    (xs (ref_addr a i + 8w) = z))`;
149
150val valid_address_def = Define `
151  valid_address a i = w2n a + 12 * i + 8 < 2**32`;
152
153val ref_set_def = Define `
154  ref_set a f = { a + n2w (4 * i) | i <= 3 * f + 2 } UNION { a - n2w (4 * i) | i <= 9 }`;
155
156val ref_cheney_def = Define `
157  ref_cheney (m,e) (a,d,xs,ys) =
158    ~(a = 0w) /\ (a && 3w = 0w) /\ (!i. i <= e ==> ref_mem i (m i) (a,xs)) /\
159    (m 0 = EMP) /\ valid_address a e /\ (!i. i <+ ref_addr a 1 ==> (xs i = ys i)) /\
160    (ref_set a e = d)`;
161
162val ref_addr_NOT_ZERO = prove(
163  ``!a. ref_cheney (m,e) (a,d,xs,ys) /\ x <= e /\ ~(x = 0) ==> ~(ref_addr a x = 0w)``,
164  Cases_word \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [ref_cheney_def,ref_addr_def,
165    word_add_n2w,n2w_11,valid_address_def,w2n_n2w] \\ REPEAT STRIP_TAC
166  \\ `(n + 12 * x) < 4294967296` by DECIDE_TAC
167  \\ `n + 12 * x = 0` by METIS_TAC [LESS_MOD] \\ DECIDE_TAC);
168
169val ref_addr_NEQ = store_thm("ref_addr_NEQ",
170  ``!a i j. ~(i = j) /\ valid_address a i /\ valid_address a j ==>
171            ~(ref_addr a i = ref_addr a j)``,
172  Cases_word \\ Cases \\ Cases
173  \\ SIMP_TAC std_ss [ref_addr_def,valid_address_def,word_add_n2w]
174  \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,LESS_MOD,n2w_11,DECIDE ``~(SUC n = 0)``]
175  \\ STRIP_TAC \\ IMP_RES_TAC (DECIDE ``m + n + 8 < l ==> m + n + 4 < l /\ m + n < l``)
176  \\ ASM_SIMP_TAC bool_ss [LESS_MOD] \\ DECIDE_TAC);
177
178val ref_addr_ADD_NEQ = store_thm("ref_addr_ADD_NEQ",
179  ``!a i j. valid_address a i /\ valid_address a j ==>
180            ~(ref_addr a i + 4w = ref_addr a j) /\
181            ~(ref_addr a i + 8w = ref_addr a j) /\
182            ~(ref_addr a i + 4w = ref_addr a j + 8w)``,
183  Cases_word \\ Cases \\ Cases
184  \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [ref_addr_def,word_add_n2w,n2w_11,LESS_MOD,valid_address_def,w2n_n2w,DECIDE ``~(SUC n = 0)``]
185  \\ STRIP_TAC \\ IMP_RES_TAC (DECIDE ``m + n + 8 < l ==> m + n + 4 < l /\ m + n < l``)
186  \\ ASM_SIMP_TAC bool_ss [LESS_MOD,MULT_CLAUSES]
187  THEN1 DECIDE_TAC THEN1 DECIDE_TAC
188  \\ FULL_SIMP_TAC std_ss [EQ_ADD_LCANCEL,GSYM ADD_ASSOC] \\ REPEAT STRIP_TAC
189  \\ IMP_RES_TAC (METIS_PROVE [] ``(m = n) ==> (m MOD 12 = n MOD 12)``)
190  \\ FULL_SIMP_TAC std_ss [RW1 [MULT_COMM] (CONJ MOD_TIMES MOD_EQ_0)]);
191
192val ALIGNED_ref_addr = store_thm("ALIGNED_ref_addr",
193  ``!n a. ALIGNED a ==> ALIGNED (ref_addr a n)``,
194  Cases \\ REWRITE_TAC [ref_addr_def,ALIGNED_def] THEN1 (STRIP_TAC \\ EVAL_TAC)
195  \\ REWRITE_TAC [GSYM ALIGNED_def,GSYM (EVAL ``4 * 3``),GSYM word_mul_n2w,DECIDE ``~(SUC n = 0)``]
196  \\ SIMP_TAC bool_ss [ALIGNED_MULT,GSYM WORD_MULT_ASSOC]);
197
198val ref_cheney_ALIGNED = prove(
199  ``ref_cheney (m,f) (a,d,xs,ys) ==> (ref_addr a x && 3w = 0w)``,
200  METIS_TAC [ALIGNED_def,ALIGNED_ref_addr,ref_cheney_def]);
201
202val ref_cheney_d = store_thm("ref_cheney_d",
203  ``ref_cheney (m,f) (a,d,xs,ys) /\ ~(x = 0) /\ x <= f ==>
204    ref_addr a x IN d /\ ref_addr a x + 4w IN d /\ ref_addr a x + 8w IN d``,
205  REWRITE_TAC [ref_cheney_def] \\ REPEAT STRIP_TAC
206  \\ Q.PAT_X_ASSUM `ref_set a f = d` (ASSUME_TAC o GSYM)
207  \\ ASM_SIMP_TAC bool_ss [ref_set_def,GSPECIFICATION,IN_UNION,ref_addr_def]
208  \\ DISJ1_TAC
209  THENL [Q.EXISTS_TAC `3*x`,Q.EXISTS_TAC `3*x+1`,Q.EXISTS_TAC `3*x+2`]
210  \\ ASM_SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB,
211      GSYM word_add_n2w,WORD_ADD_ASSOC] \\ DECIDE_TAC);
212
213fun UPDATE_ref_addr_prove (c,tm) = prove(tm,
214  Cases \\ Cases_word \\ REPEAT STRIP_TAC
215  \\ sg c \\ ASM_REWRITE_TAC [APPLY_UPDATE_THM]
216  \\ FULL_SIMP_TAC std_ss [ref_addr_def,EVAL ``1=0``,word_add_n2w,valid_address_def,
217      w2n_n2w,n2w_11,WORD_LO]
218  \\ Q.PAT_X_ASSUM `n < dimword (:32)` ASSUME_TAC
219  \\ Q.PAT_X_ASSUM `n' < dimword (:32)` ASSUME_TAC
220  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [LESS_MOD]
221  \\ `n' + 12 * x < 4294967296` by DECIDE_TAC
222  \\ `n' + 12 * x + 4 < 4294967296` by DECIDE_TAC
223  \\ `n' + 12 < 4294967296` by DECIDE_TAC
224  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [LESS_MOD] \\ DECIDE_TAC);
225
226val UPDATE_ref_addr = UPDATE_ref_addr_prove(`~(ref_addr (n2w n') x = (n2w n))`,
227  ``!i a. valid_address a x /\
228          ~(x=0) /\ i <+ ref_addr a 1 /\ (xs i = ys i) ==> ((ref_addr a x =+ y) xs i = ys i)``);
229
230val UPDATE_ref_addr4 = UPDATE_ref_addr_prove(`~(ref_addr (n2w n') x + 4w = (n2w n))`,
231  ``!i a. valid_address a x /\
232          ~(x=0) /\ i <+ ref_addr a 1 /\ (xs i = ys i) ==> ((ref_addr a x + 4w =+ y) xs i = ys i)``);
233
234val UPDATE_ref_addr8 = UPDATE_ref_addr_prove(`~(ref_addr (n2w n') x + 8w = (n2w n))`,
235  ``!i a. valid_address a x /\
236          ~(x=0) /\ i <+ ref_addr a 1 /\ (xs i = ys i) ==> ((ref_addr a x + 8w =+ y) xs i = ys i)``);
237
238val va_IMP = store_thm("va_IMP",
239  ``!a e i. valid_address a e /\ i <= e ==> valid_address a i``,
240  SIMP_TAC bool_ss [valid_address_def] \\ DECIDE_TAC);
241
242val ref_cheney_update_REF = prove(
243  ``ref_cheney (m,e) (a,d,xs,ys) /\ j <= e /\ x <= e /\ ~(x = 0) ==>
244    ref_cheney ((x =+ REF j) m,e) (a,d,(ref_addr a x =+ ref_addr a j + 1w) xs,ys)``,
245  SIMP_TAC bool_ss [ref_cheney_def] \\ REVERSE (REPEAT STRIP_TAC)
246  THEN1 (MATCH_MP_TAC UPDATE_ref_addr \\ METIS_TAC [va_IMP])
247  THEN1 ASM_SIMP_TAC bool_ss [UPDATE_def]
248  \\ Cases_on `i = x` \\ ASM_SIMP_TAC bool_ss [UPDATE_def,ref_mem_def]
249  \\ RES_TAC \\ Cases_on `m i` \\ FULL_SIMP_TAC bool_ss [ref_mem_def]
250  \\ `valid_address a i /\ valid_address a x` by METIS_TAC [va_IMP]
251  \\ `~(ref_addr a i = ref_addr a x)` by METIS_TAC [ref_addr_NEQ,va_IMP]
252  \\ ASM_SIMP_TAC bool_ss [] \\ Cases_on `p` \\ Cases_on `r`
253  \\ FULL_SIMP_TAC std_ss [ref_mem_def] \\ METIS_TAC [ref_addr_ADD_NEQ]);
254
255val ref_cheney_move_lemma = prove(
256  ``ref_cheney (m,e) (a,d,xs,ys) /\ (~(x = 0) ==> ~(m x = EMP)) /\ (!x. ~(m x = REF 0)) /\
257    (move(x,j,m) = (x1,j1,m1)) /\ ~(j = 0) /\ j <= e /\ x <= e /\
258    (arm_move(ref_addr a j,ref_addr a x,r7,r8,d,xs) = (j2,x2,r7_2,r8_2,d2,xs2)) ==>
259    ref_cheney (m1,e) (a,d,xs2,ys) /\ (x2 = ref_addr a x1) /\ (j2 = ref_addr a j1) /\ (d2 = d) /\
260    arm_move_pre(ref_addr a j,ref_addr a x,r7,r8, d, xs)``,
261  REWRITE_TAC [move_def] \\ Cases_on `x = 0` THEN1
262   (ASM_SIMP_TAC std_ss [ref_addr_def] \\ REWRITE_TAC [def1]
263    \\ SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
264    \\ SIMP_TAC std_ss [ref_addr_def])
265  \\ Cases_on `x <= e` \\ ASM_SIMP_TAC bool_ss []
266  \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ STRIP_TAC
267  \\ `~(ref_addr a x = 0w)` by METIS_TAC [ref_addr_NOT_ZERO]
268  \\ Cases_on `m x` \\ ASM_SIMP_TAC bool_ss [isREF_def,heap_type_11] THEN1
269     (REWRITE_TAC [getREF_def]
270      \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss []
271      \\ REWRITE_TAC [def1]
272      \\ SIMP_TAC std_ss [LET_DEF,GSYM AND_IMP_INTRO] \\ NTAC 2 STRIP_TAC
273      \\ ASM_SIMP_TAC std_ss []
274      \\ `~(xs (ref_addr a x) && 1w = 0w)` by (
275        FULL_SIMP_TAC bool_ss [ref_cheney_def,ref_mem_def]
276        \\ `ref_mem x (REF n) (a,xs)` by METIS_TAC []
277        \\ FULL_SIMP_TAC bool_ss [ref_cheney_def,ref_mem_def]
278        \\ MATCH_MP_TAC ALIGNED_add_1_and_1
279        \\ MATCH_MP_TAC ALIGNED_ref_addr
280        \\ ASM_REWRITE_TAC [ALIGNED_def])
281      \\ ASM_SIMP_TAC std_ss []
282      \\ `ref_mem x (REF n) (a,xs)` by METIS_TAC [ref_cheney_def]
283      \\ FULL_SIMP_TAC std_ss [ref_mem_def,WORD_ADD_SUB]
284      \\ IMP_RES_TAC ref_cheney_d \\ IMP_RES_TAC ref_cheney_ALIGNED
285      \\ ASM_SIMP_TAC bool_ss [INSERT_SUBSET,EMPTY_SUBSET,ALIGNED_def])
286  \\ SIMP_TAC std_ss [heap_type_distinct]
287  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss []
288  \\ REWRITE_TAC [def1]
289  \\ SIMP_TAC std_ss [LET_DEF]
290  \\ `~(m x = EMP)` by METIS_TAC [heap_type_distinct]
291  \\ `valid_address a x` by METIS_TAC [ref_cheney_def,va_IMP]
292  \\ ASM_SIMP_TAC std_ss [word_arith_lemma1,WORD_ADD_SUB]
293  \\ `(xs (ref_addr a x) && 1w = 0w)` by
294       (FULL_SIMP_TAC bool_ss [ref_cheney_def] \\ Cases_on `p` \\ Cases_on `r`
295        \\ `ref_mem x (DATA (q,q',r')) (a,xs)` by METIS_TAC []
296        \\ FULL_SIMP_TAC bool_ss [ref_mem_def]
297        \\ MATCH_MP_TAC ALIGNED_and_1 \\ MATCH_MP_TAC ALIGNED_ref_addr
298        \\ ASM_REWRITE_TAC [ALIGNED_def])
299  \\ FULL_SIMP_TAC std_ss [PAIR_EQ,WORD_ADD_0,word_arith_lemma4]
300  \\ NTAC 4 STRIP_TAC
301  \\ `~(j = 0)` by METIS_TAC []
302  \\ IMP_RES_TAC ref_cheney_d \\ IMP_RES_TAC ref_cheney_ALIGNED
303  \\ ASM_SIMP_TAC bool_ss []
304  \\ REVERSE (STRIP_TAC \\ STRIP_TAC) THEN1
305   (FULL_SIMP_TAC std_ss [GSYM ALIGNED_def,ALIGNED_CLAUSES,
306      SIMP_RULE std_ss [word_mul_n2w] (Q.SPEC `2w` ALIGNED_CLAUSES)]
307    \\ ASM_SIMP_TAC std_ss [ref_addr_def,LEFT_ADD_DISTRIB,GSYM word_add_n2w,WORD_ADD_ASSOC])
308  \\ MATCH_MP_TAC ref_cheney_update_REF \\ ASM_SIMP_TAC bool_ss []
309  \\ Cases_on `p` \\ Cases_on `r` \\ FULL_SIMP_TAC std_ss [ref_cheney_def]
310  \\ REVERSE (REPEAT STRIP_TAC)
311  THEN1
312    (`valid_address a j` by METIS_TAC [va_IMP]
313     \\ MATCH_MP_TAC UPDATE_ref_addr8 \\ ASM_SIMP_TAC bool_ss []
314     \\ MATCH_MP_TAC UPDATE_ref_addr4 \\ ASM_SIMP_TAC bool_ss []
315     \\ MATCH_MP_TAC UPDATE_ref_addr \\ ASM_SIMP_TAC bool_ss [])
316  THEN1 ASM_SIMP_TAC std_ss [UPDATE_def]
317  \\ `ref_mem x (DATA (q,q',r')) (a,xs)` by METIS_TAC []
318  \\ Cases_on `i = j`
319  THEN1 (FULL_SIMP_TAC bool_ss [UPDATE_def,ref_mem_def,WORD_EQ_ADD_LCANCEL,
320         RW[WORD_ADD_0](Q.SPECL[`x`,`y`,`0w`]WORD_EQ_ADD_LCANCEL)]
321       \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11]
322       \\ IMP_RES_TAC va_IMP
323       \\ IMP_RES_TAC ref_addr_ADD_NEQ \\ ASM_SIMP_TAC std_ss []
324       \\ METIS_TAC [])
325  \\ `ref_mem i (m i) (a,xs)` by METIS_TAC []
326  \\ CONV_TAC (RATOR_CONV (SIMP_CONV std_ss [UPDATE_def]))
327  \\ ASM_SIMP_TAC bool_ss []
328  \\ Cases_on `m i`
329  \\ FULL_SIMP_TAC bool_ss [ref_mem_def,UPDATE_def]
330  \\ `~(ref_addr a j = ref_addr a i)` by METIS_TAC [va_IMP,ref_addr_NEQ]
331  \\ RES_TAC \\ `valid_address a i /\ valid_address a j` by METIS_TAC [va_IMP]
332  \\ ASM_SIMP_TAC bool_ss [ref_addr_ADD_NEQ]
333  \\ Cases_on `p` \\ Cases_on `r`
334  \\ FULL_SIMP_TAC bool_ss [ref_mem_def,UPDATE_def,ref_addr_ADD_NEQ,WORD_EQ_ADD_RCANCEL]);
335
336val ref_cheney_move = prove(
337  ``!a b b' i j j2 j3 e m m2 w ww r x xj2 xx2 xs xs2 d x2 xx  r7 r8 r7_2 r8_2 d2.
338    cheney_inv (b,b',i,j,j3,e,f,m,w,ww,r) /\ {x} SUBSET0 DR0(ICUT(b,e)m) /\
339    ref_cheney (m,f) (a,d,xs,ys) /\ (move(x,j,m) = (x2,j2,m2)) /\
340    (arm_move(ref_addr a j,ref_addr a x,r7,r8, d, xs) = (xj2,xx2,r7_2,r8_2,d2,xs2)) ==>
341    cheney_inv(b,b',i,j2,j3,e,f,m2,w,ww,r) /\ {x2} SUBSET0 RANGE(b,j2) /\ j <= j2 /\
342    (CUT(b,j)m = CUT(b,j)m2) /\ (DR0 (ICUT(b,e)m) = DR0 (ICUT(b,e)m2)) /\
343    ref_cheney (m2,f) (a,d,xs2,ys) /\
344    (ref_addr a x2 = xx2) /\ (ref_addr a j2 = xj2) /\ (d = d2) /\
345    arm_move_pre(ref_addr a j,ref_addr a x, r7,r8, d, xs)``,
346  NTAC 27 STRIP_TAC \\ `~(x = 0) ==> ~(m x = EMP)` by (STRIP_TAC
347    \\ FULL_SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY]
348    \\ FULL_SIMP_TAC bool_ss [IN_DEF,DR0_def,D0_def,R0_def,ICUT_def]
349    \\ METIS_TAC [heap_type_distinct])
350  \\ `~(j = 0) /\ j <= f` by (FULL_SIMP_TAC bool_ss [cheney_inv_def] \\ DECIDE_TAC)
351  \\ IMP_RES_TAC move_lemma
352  \\ ASM_SIMP_TAC bool_ss [] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
353  \\ `!x. ~(m x = REF 0)` by
354   (CCONTR_TAC \\ FULL_SIMP_TAC bool_ss [cheney_inv_def,cheney_gcTheory.R1_def]
355    \\ `RANGE(b,j) 0` by METIS_TAC [cheney_gcTheory.R1_def]
356    \\ FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC)
357  \\ MATCH_MP_TAC ref_cheney_move_lemma
358  \\ ASM_SIMP_TAC bool_ss [PAIR_EQ] \\ METIS_TAC []);
359
360val arm_move2_thm = prove(
361  ``(arm_move2 = arm_move) /\ (arm_move2_pre = arm_move_pre)``,
362  TAILREC_TAC \\ SIMP_TAC std_ss [LET_DEF]);
363
364val ref_cheney_inv_def = Define `
365  ref_cheney_inv (b,i,j,k,e,f,m,w,ww,r) (a,r3,r4,d,xs,ys) =
366    cheney_inv (b,b,i,j,k,e,f,m,w,ww,r) /\ ref_cheney (m,f) (a,d,xs,ys) /\
367    valid_address a e /\ (r4 = ref_addr a j) /\ (r3 = ref_addr a i)`;
368
369val ref_cheney_step_thm = prove(
370  ``ref_cheney_inv (b,i,j,j,e,f,m,x,xx,r) (a,r3,r4,d,xs,ys) /\ ~(i = j) /\
371    (cheney_step (i,j,e,m) = (i',j',e',m')) /\
372    (arm_cheney_step (r3,r4,r7,r8,d,xs) = (r3',r4',r5',r6',r7',r8',d',xs')) ==>
373    ref_cheney_inv (b,i',j',j',e',f,m',x,xx,r) (a,r3',r4',d,xs',ys) /\ (d = d') /\
374    arm_cheney_step_pre (r3,r4,r7,r8,d,xs)``,
375  REWRITE_TAC [ref_cheney_inv_def] \\ STRIP_TAC
376  \\ `cheney_inv (b,b,i',j',j',e',f,m',x,xx,r)` by METIS_TAC [cheney_inv_step]
377  \\ ASM_SIMP_TAC bool_ss []
378  \\ Q.UNDISCH_TAC `cheney_step (i,j,e,m) = (i',j',e',m')`
379  \\ Q.UNDISCH_TAC `arm_cheney_step (r3,r4,r7,r8,d,xs) = (r3',r4',r5',r6',r7',r8',d',xs')`
380  \\ REWRITE_TAC [cheney_step_def]
381  \\ SIMP_TAC bool_ss [def3]
382  \\ `?r51. xs r3 = r51` by METIS_TAC []
383  \\ `?r61. xs (r3+4w) = r61` by METIS_TAC []
384  \\ `?r41 r52 r71 r81 d1 xs1. arm_move (ref_addr a j,r51,r7,r8,d,xs) = (r41,r52,r71,r81,d1,xs1)` by METIS_TAC [PAIR]
385  \\ `?r42 r62 r72 r82 d2 xs2. arm_move (r41,r61,r71,r81,d1,xs1) = (r42,r62,r72,r82,d2,xs2)` by METIS_TAC [PAIR]
386  \\ `?x1 y1 d1. getDATA (m i) = (x1,y1,d1)` by METIS_TAC [PAIR]
387  \\ `?x2 j2 m2. move(x1,j,m) = (x2,j2,m2)` by METIS_TAC [PAIR]
388  \\ `?y3 j3 m3. move(y1,j2,m2) = (y3,j3,m3)` by METIS_TAC [PAIR]
389  \\ `(xs (ref_addr a i) = r51) /\ (xs (ref_addr a i + 4w) = r61)` by METIS_TAC []
390  \\ ASM_SIMP_TAC std_ss [LET_DEF,arm_move2_thm,GSYM AND_IMP_INTRO]
391  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC bool_ss []
392  \\ REPEAT (MATCH_MP_TAC (METIS_PROVE [] ``P ==> (Q ==> P)``))
393  \\ `~(i = 0) /\ ~(j = 0) /\ (j <= e)` by
394       (FULL_SIMP_TAC bool_ss [cheney_inv_def] \\ DECIDE_TAC)
395  \\ `ref_addr a (i + 1) = ref_addr a i + 12w` by
396   (ASM_SIMP_TAC std_ss [ref_addr_def,GSYM ADD1,MULT_CLAUSES,GSYM word_add_n2w]
397    \\ SIMP_TAC bool_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM])
398  \\ ASM_SIMP_TAC bool_ss []
399  \\ `?ax ay ad. m i = DATA(ax,ay,ad)` by METIS_TAC [m_DATA,PAIR]
400  \\ `(x1,y1,d1') = (ax,ay,ad)` by METIS_TAC [getDATA_def]
401  \\ FULL_SIMP_TAC bool_ss [PAIR_EQ]
402  \\ Q.PAT_X_ASSUM `getDATA (DATA (ax,ay,ad)) = (ax,ay,ad)` (K ALL_TAC)
403  \\ `{ax} SUBSET0 DR0 (ICUT (b,e) m) /\ {ay} SUBSET0 DR0 (ICUT (b,e) m)` by
404   (sg `{ax;ay} SUBSET0 D1(CUT(i,j)m)` THENL [
405      FULL_SIMP_TAC bool_ss [SUBSET0_DEF,IN_INSERT,SUBSET_DEF,NOT_IN_EMPTY]
406      \\ FULL_SIMP_TAC bool_ss [IN_DEF,D1_def,CUT_def,cheney_inv_def]
407      \\ `RANGE(i,j)i` by (REWRITE_TAC [RANGE_def] \\ DECIDE_TAC)
408      \\ METIS_TAC [],
409      `{ax;ay} SUBSET0 DR0 (ICUT (b,e) m)` by
410        METIS_TAC [cheney_inv_def,SUBSET0_TRANS]
411      \\ FULL_SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY]])
412  \\ `i <= e /\ i <= f /\ j <= f /\ RANGE(b,j)i` by
413        (FULL_SIMP_TAC bool_ss [cheney_inv_def,RANGE_def] \\ DECIDE_TAC)
414  \\ `ref_mem i (DATA (ax,ay,ad)) (a,xs)` by METIS_TAC [ref_cheney_def]
415  \\ FULL_SIMP_TAC bool_ss [ref_mem_def]
416  \\ `(r51 = ref_addr a ax) /\ (r61 = ref_addr a ay)` by METIS_TAC []
417  \\ FULL_SIMP_TAC bool_ss []
418  \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
419       Q.SPECL [`a`,`b`,`b`,`i`,`j`,`j2`,`j`,`e`,`m`,`m2`,`x`,`xx`,`r`,`ax`,`r41`,`r52`,`xs`,`xs1`,`d`,`x2`,`ad`,`r7`,`r8`,`r71`,`r81`,`d1`]) ref_cheney_move
420  \\ Q.PAT_X_ASSUM `ref_addr a j2 = r41` (ASSUME_TAC o GSYM)
421  \\ FULL_SIMP_TAC bool_ss []
422  \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
423       Q.SPECL [`a`,`b`,`b`,`i`,`j2`,`j3`,`j`,`e`,`m2`,`m3`,`x`,`xx`,`r`,`ay`,`r42`,`r62`,`xs1`,`xs2`,`d1`,`y3`,`ad1`,`r71`,`r81`,`r72`,`r82`,`d2`]) ref_cheney_move
424  \\ IMP_RES_TAC ref_cheney_d
425  \\ REPEAT (Q.PAT_X_ASSUM `!xx.bb` (K ALL_TAC))
426  \\ REPEAT (Q.PAT_X_ASSUM `ccc ==> !xx.bb` (K ALL_TAC))
427  \\ IMP_RES_TAC ref_cheney_ALIGNED
428  \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,ALIGNED_def,LET_DEF,WORD_ADD_0,LENGTH]
429  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
430  \\ ASM_SIMP_TAC std_ss [RW [ALIGNED_def] ALIGNED_CLAUSES,word_arith_lemma1]
431  \\ Q.PAT_X_ASSUM `ref_cheney (m3,f) (a,d1,xs2,ys)` (STRIP_ASSUME_TAC o RW [ref_cheney_def])
432  \\ REVERSE STRIP_TAC THEN1 METIS_TAC []
433  \\ ASM_SIMP_TAC bool_ss [ref_cheney_def,APPLY_UPDATE_THM]
434  \\ ASM_SIMP_TAC bool_ss [ref_addr_ADD_NEQ]
435  \\ `m3 i = m i` by
436       (`RANGE(b,j2)i` by (FULL_SIMP_TAC bool_ss [RANGE_def] \\ DECIDE_TAC)
437        \\ FULL_SIMP_TAC bool_ss [CUT_def,FUN_EQ_THM]
438        \\ METIS_TAC [heap_type_distinct])
439  \\ REVERSE (REPEAT STRIP_TAC) \\ `~(j3 = 0)` by DECIDE_TAC
440  THEN1 (REWRITE_TAC [GSYM APPLY_UPDATE_THM]
441    \\ `valid_address a i` by METIS_TAC [va_IMP]
442    \\ MATCH_MP_TAC UPDATE_ref_addr4 \\ ASM_SIMP_TAC bool_ss []
443    \\ MATCH_MP_TAC UPDATE_ref_addr \\ ASM_SIMP_TAC bool_ss [] \\ METIS_TAC [])
444  \\ Cases_on `i'' = i` \\ ASM_SIMP_TAC bool_ss [ref_mem_def,UPDATE_def] THENL [
445    `valid_address a i` by METIS_TAC [va_IMP]
446    \\ `ref_mem i (DATA (ax,ay,ad)) (a,xs2)` by METIS_TAC []
447    \\ FULL_SIMP_TAC bool_ss [ref_mem_def,ref_addr_ADD_NEQ],
448    Cases_on `m3 i''` \\ ASM_SIMP_TAC bool_ss [ref_mem_def]
449    THENL [ALL_TAC,Cases_on`p` \\ Cases_on`r'` \\ Cases_on`r''`]
450    \\ `valid_address a i /\ valid_address a i'' /\ ref_mem i'' (m3 i'') (a,xs2)` by
451      METIS_TAC [ref_cheney_def,heap_type_distinct,va_IMP]
452    \\ Q.PAT_X_ASSUM `m3 i'' = xxxxx` (ASSUME_TAC)
453    \\ FULL_SIMP_TAC bool_ss [ref_mem_def,ref_addr_NEQ,ref_addr_ADD_NEQ,WORD_EQ_ADD_RCANCEL]]);
454
455val ref_cheney_loop_th = prove(
456  ``!b i j e m x y r r3 r4 r5 r6 r7 r8 d xs i' m' r3' r4' r5' r6' r7' r8' d2 xs'.
457      ref_cheney_inv (b,i,j,j,e,f,m,x,xx,r) (a,r3,r4,d,xs,ys) /\
458      (cheney (i,j,e,m) = (i',m')) /\
459      (arm_cheney_loop (r3,r4,r5,r6,r7,r8,d,xs) = (r3',r4',r5',r6',r7',r8',d2,xs')) ==>
460      ref_cheney_inv (b,i',i',i',e,f,m',x,xx,r) (a,r3',r4',d,xs',ys) /\ (d2 = d) /\
461      arm_cheney_loop_pre (r3,r4,r5,r6,r7,r8,d,xs)``,
462  completeInduct_on `e - i:num` \\ NTAC 2 (ONCE_REWRITE_TAC [cheney_def])
463  \\ ASM_REWRITE_TAC [GSYM AND_IMP_INTRO] \\ NTAC 27 STRIP_TAC
464  \\ ONCE_REWRITE_TAC [def4]
465  \\ Cases_on `i = j` THEN1
466    (Q.PAT_X_ASSUM `!m.bb` (K ALL_TAC)
467     \\ FULL_SIMP_TAC std_ss [ref_cheney_inv_def] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
468     \\ METIS_TAC [])
469  \\ Q.PAT_X_ASSUM `ref_cheney_inv (b,i,j,j,e,f,m,x,xx,r) (a,r3,r4,d,xs,ys)`
470      (fn th => STRIP_ASSUME_TAC (RW [ref_cheney_inv_def] th) \\ ASSUME_TAC th)
471  \\ `i <= j /\ j <= e` by METIS_TAC [cheney_inv_def]
472  \\ Cases_on `v = 0` THEN1 `F` by DECIDE_TAC
473  \\ `valid_address a i /\ valid_address a j /\ ~(e < i)` by
474    (FULL_SIMP_TAC bool_ss [valid_address_def] \\ DECIDE_TAC)
475  \\ ASM_REWRITE_TAC [] \\ SIMP_TAC (std_ss++pbeta_ss) [LET_DEF]
476  \\ `?i2 j2 e2 m2. cheney_step (i,j,e,m) = (i2,j2,e2,m2)` by METIS_TAC [PAIR]
477  \\ `?r31 r41 r51 r61 r71 r81 d1 xs1. arm_cheney_step (ref_addr a i,ref_addr a j,r7,r8,d,xs) =
478                      (r31,r41,r51,r61,r71,r81,d1,xs1)` by METIS_TAC [PAIR]
479  \\ `~(ref_addr a i = ref_addr a j)` by METIS_TAC [ref_addr_NEQ]
480  \\ ASM_REWRITE_TAC []
481  \\ STRIP_TAC
482  \\ `e - (i + 1) < v` by DECIDE_TAC
483  \\ Q.PAT_X_ASSUM `!m. m < v ==> !e i. bbb`
484    (ASSUME_TAC o RW [] o Q.SPECL [`e`,`i+1`] o UNDISCH o Q.SPEC `e - (i + 1)`)
485  \\ `ref_cheney_inv (b,i2,j2,j2,e2,f,m2,x,xx,r) (a,r31,r41,d,xs1,ys) /\ (d = d1) /\
486      arm_cheney_step_pre (r3,r4,r7,r8,d,xs)` by METIS_TAC [ref_cheney_step_thm]
487  \\ `(i2 = i+1) /\ (e2 = e)` by FULL_SIMP_TAC (std_ss++pbeta_ss) [cheney_step_def,LET_DEF]
488  \\ METIS_TAC []);
489
490val SING_IN_SUBSET0 = prove(
491  ``x IN t /\ t SUBSET0 s ==> {x} SUBSET0 s``,
492  SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY]);
493
494val roots_in_mem_def = Define `
495  (roots_in_mem [] (a,r12,m) = T) /\
496  (roots_in_mem (x::xs) (a,r12,m) =
497      (m r12 = ref_addr a x) /\ r12 <+ ref_addr a 1 /\ r12 <+ r12 + 4w /\
498      roots_in_mem xs (a,r12+4w,m))`;
499
500val NOT_ref_addr = prove(
501  ``!x a. valid_address a i /\ x <+ ref_addr a 1 /\ ~(i = 0) ==>
502          ~(x = ref_addr a i) /\ ~(x = ref_addr a i + 4w) /\ ~(x = ref_addr a i + 8w)``,
503  NTAC 2 Cases_word \\ ASM_SIMP_TAC (std_ss++SIZES_ss)
504       [ref_addr_def,word_add_n2w,n2w_11,WORD_LO,w2n_n2w,valid_address_def,LESS_MOD]
505  \\ REPEAT STRIP_TAC
506  \\ `n' + 12 * i < 4294967296 /\ n' + 12 < 4294967296` by DECIDE_TAC
507  \\ `n' + 12 * i + 4 < 4294967296` by DECIDE_TAC
508  \\ FULL_SIMP_TAC std_ss [LESS_MOD] \\ DECIDE_TAC);
509
510val lemma = store_thm("lemma",
511  ``ref_cheney (m1,f) (a,d,xs1,xs) /\ r12 <+ ref_addr a 1 ==>
512    ref_cheney (m1,f) (a,d,(r12 =+ r51) xs1,(r12 =+ r51) xs1)``,
513  SIMP_TAC bool_ss [ref_cheney_def] \\ REPEAT STRIP_TAC
514  \\ Cases_on `m1 i` \\ ASM_REWRITE_TAC [ref_mem_def] THENL [
515    `ref_addr a n + 1w = xs1 (ref_addr a i)` by METIS_TAC [ref_mem_def]
516    \\ ASM_SIMP_TAC bool_ss [APPLY_UPDATE_THM]
517    \\ METIS_TAC [NOT_ref_addr,va_IMP,heap_type_distinct],
518    Cases_on `p` \\ Cases_on `r` \\ ASM_REWRITE_TAC [ref_mem_def]
519    \\ ASM_SIMP_TAC bool_ss [APPLY_UPDATE_THM]
520    \\ METIS_TAC [NOT_ref_addr,va_IMP,heap_type_distinct,ref_mem_def]]);
521
522val roots_lemma = prove(
523  ``!rs b k.
524      roots_in_mem rs (a,b + k,xs) ==> b <+ b + k ==>
525      ref_cheney (m,f) (a,d,xs1,xs) ==>
526      roots_in_mem rs (a,b + k,(b =+ r51) xs1)``,
527  Induct \\ REWRITE_TAC [roots_in_mem_def]
528  \\ SIMP_TAC std_ss [APPLY_UPDATE_THM,WORD_LOWER_NOT_EQ,GSYM WORD_ADD_ASSOC]
529  \\ REPEAT STRIP_TAC \\ METIS_TAC [ref_cheney_def,WORD_LOWER_TRANS]);
530
531val root_address_ok_def = Define `
532  (root_address_ok a 0 x = T) /\
533  (root_address_ok a (SUC n) x = ALIGNED a /\ a IN x /\ root_address_ok (a+4w) n x)`;
534
535val ref_cheney_move_roots = prove(
536  ``!rs zs j m r4 r5 r7 r8 xs r12 ys jn mn.
537      LENGTH rs < 2**32 /\
538      root_address_ok r12 (LENGTH rs) x /\
539      roots_in_mem (rs++zs) (a,r12,xs) /\
540      (!x. MEM x rs ==> {x} SUBSET0 DR0 (ICUT (b,e) m)) /\
541      ref_cheney_inv (b,i,j,j',e,f,m,(w:num->word32 heap_type),ww,r) (a,r3,r4,x,xs,xs) ==>
542      (arm_move_roots(r4,r5,n2w (LENGTH rs),r7,r8,r12,x,xs) = (r4n,r5n,r6n,r7n,r8n,r12n,xn,xsn)) /\
543      (move_roots(rs,j,m) = (ys,jn,mn)) ==>
544      arm_move_roots_pre(r4,r5,n2w (LENGTH rs),r7,r8,r12,x,xs) /\
545      ref_cheney_inv (b,i,jn,j',e,f,mn,w,ww,r) (a,r3,r4n,x,xsn,xsn) /\
546      roots_in_mem (ys++zs) (a,r12,xsn) /\
547      (LENGTH ys = LENGTH rs) /\ (r12n = r12 + n2w (4 * LENGTH rs)) /\
548      (!i. i <+ r12 ==> (xs i = xsn i)) /\ (xn = x)``,
549  STRIP_TAC \\ STRIP_TAC \\ Induct_on `rs`
550  \\ ONCE_REWRITE_TAC [def5] \\ SIMP_TAC std_ss [LET_DEF]
551  THEN1 (Cases_on `ys` \\ REWRITE_TAC [move_roots_def,PAIR_EQ,LENGTH,MAP,NOT_NIL_CONS]
552         \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [LENGTH,WORD_MULT_CLAUSES,WORD_ADD_0])
553  \\ POP_ASSUM (ASSUME_TAC o RW1 [GSYM CONTAINER_def])
554  \\ SIMP_TAC std_ss [LENGTH,ADD1,DECIDE ``(k + 1 = m + 1 + n) = (k = m + n:num)``,ZIP,APPEND]
555  \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LESS_MOD,LENGTH,DECIDE ``~(SUC n = 0)``]
556  \\ SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB]
557  \\ NTAC 12 STRIP_TAC
558  \\ `?r41 r51 r71 r81 x1 xs1. arm_move (r4,xs r12,r7,r8,x,xs) = (r41,r51,r71,r81,x1,xs1)` by METIS_TAC [PAIR]
559  \\ ASM_REWRITE_TAC [LET_DEF,PAIR_EQ,move_roots_def,APPEND,MAP]
560  \\ `?y1 j1 m1. move (h,j,m) = (y1,j1,m1)` by METIS_TAC [PAIR]
561  \\ `?ys j2 m2. move_roots (rs,j1,m1) = (ys,j2,m2)` by METIS_TAC [PAIR]
562  \\ FULL_SIMP_TAC std_ss [LET_DEF,PAIR_EQ,move_roots_def,GSYM AND_IMP_INTRO,MAP] \\ STRIP_TAC
563  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC bool_ss []
564  \\ FULL_SIMP_TAC bool_ss [MAP,CONS_11,NOT_NIL_CONS,NOT_CONS_NIL,ZIP,APPEND,ADD1,EQ_ADD_RCANCEL,LENGTH]
565  \\ REPEAT (MATCH_MP_TAC (METIS_PROVE [] ``P ==> (Q ==> P)``))
566  \\ `LENGTH rs < 4294967296` by DECIDE_TAC
567  \\ FULL_SIMP_TAC bool_ss [roots_in_mem_def,MEM,ref_cheney_inv_def,APPEND]
568  \\ `{h} SUBSET0 DR0 (ICUT(b,e)m)` by METIS_TAC [SING_IN_SUBSET0,IN_INSERT]
569  \\ `arm_move (ref_addr a j,ref_addr a h,r7,r8,x,xs) = (r41,r51,r71,r81,x1,xs1)` by METIS_TAC [WORD_ADD_0]
570  \\ FULL_SIMP_TAC bool_ss [FST,SND]
571  \\ (STRIP_ASSUME_TAC o GSYM o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
572   Q.SPECL [`a`,`b`,`b`,`i`,`j`,`j1`,`j'`,`e`,`m`,`m1`,
573    `w`,`ww`,`r`,`h`,`r41`,`r51`,`xs`,`xs1`,`x`,`y1`,`hx`,`r7`,`r8`,`r71`,`r81`,`x1`] o Q.INST [`ys`|->`xs`]) (INST_TYPE [``:'a``|->``:word32``] ref_cheney_move)
574  \\ ASM_SIMP_TAC bool_ss [WORD_ADD_0]
575  \\ `!x. MEM x rs ==> {x} SUBSET0 DR0 (ICUT (b,e) m1)` by METIS_TAC []
576  \\ `ref_cheney (m1,f) (a,x,(r12 =+ r51) xs1,(r12 =+ r51) xs1)` by METIS_TAC [lemma]
577  \\ `roots_in_mem (rs++zs) (a,r12 + 4w,(r12 =+ r51) xs1)` by METIS_TAC [roots_lemma]
578  \\ Q.PAT_X_ASSUM `r51 = ref_addr a y1` ASSUME_TAC \\ FULL_SIMP_TAC bool_ss []
579  \\ FULL_SIMP_TAC std_ss [root_address_ok_def,ALIGNED_def,GSYM ADD1,move_roots_def]
580  \\ Q.PAT_X_ASSUM `CONTAINER (!j m xs r12. bbb)`
581    (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
582     Q.SPECL [`j1`,`m1`,`ref_addr a y1`,`r71`,`r81`,`(r12 =+ ref_addr a y1) xs1`,`r12+4w`,`ys'`,`j2`,`m2`] o
583     RW [CONTAINER_def])
584  \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,word_add_n2w,word_mul_n2w,
585       GSYM WORD_ADD_ASSOC,LEFT_ADD_DISTRIB,AC ADD_ASSOC ADD_COMM,FST]
586  \\ METIS_TAC [APPLY_UPDATE_THM,WORD_LOWER_TRANS,WORD_LOWER_NOT_EQ,ref_cheney_def]);
587
588val ref_cheney_move_roots6 =
589  SIMP_RULE std_ss [LENGTH,ADD1,AND_IMP_INTRO,GSYM CONJ_ASSOC]
590  (Q.SPEC `[x1;x2;x3;x4;x5;x6]` ref_cheney_move_roots);
591
592val arm_c_init_lemma = prove(
593  ``(arm_c_init(if u then 0w else 1w,r6,r10) =
594     (r10 + 12w + if u then 0w else r6, if u then 1w else 0w,r6,r10))``,
595  Cases_on `u` \\ SIMP_TAC std_ss [SIMP_RULE std_ss [LET_DEF] def6,
596    WORD_ADD_0,PAIR_EQ,WORD_XOR_CLAUSES,EVAL ``0w = 1w:word32``]);
597
598val arm_coll_inv_def = Define `
599  arm_coll_inv (a,x,xs) (i,e,rs,l,u,m) =
600    ?x1 x2 x3 x4 x5 x6.
601      roots_in_mem (rs ++ [i;e]) (a,a-24w,xs) /\
602      (rs = [x1;x2;x3;x4;x5;x6]) /\
603      valid_address a (l + l + 1) /\
604      ref_cheney (m,l+l+1) (a,x,xs,xs) /\
605      (xs (a-28w) = if u then 0w else 1w) /\ a - 28w <+ ref_addr a 1 /\ a - 28w <+ a - 24w /\
606      (xs (a-32w) = n2w (12 * l)) /\ a - 32w <+ ref_addr a 1 /\ a - 32w <+ a - 24w`;
607
608val roots_in_mem_carry_over = prove(
609  ``!p r xs ys. ref_cheney (m,f) (a,x,xs,ys) /\ roots_in_mem p (a,r,ys) ==> roots_in_mem p (a,r,xs)``,
610  Induct \\ FULL_SIMP_TAC bool_ss [roots_in_mem_def,ref_cheney_def] \\ METIS_TAC []);
611
612val arm_coll_inv_pre_lemma = store_thm("arm_coll_inv_pre_lemma",
613  ``arm_coll_inv (a,x,xs) (q,e,rs,l,u,m) ==>
614    {a+4w;a-32w;a-28w;a-24w;a-20w;a-16w;a-12w;a-8w;a-4w;a} SUBSET x /\
615    !i. i IN {a+4w;a-32w;a-28w;a-24w;a-20w;a-16w;a-12w;a-8w;a-4w;a} ==> ALIGNED i``,
616  REWRITE_TAC [arm_coll_inv_def,ref_cheney_def] \\ REPEAT STRIP_TAC THENL [
617    Q.PAT_X_ASSUM `ref_set a (l + l + 1) = x` (ASSUME_TAC o GSYM)
618    \\ ASM_SIMP_TAC bool_ss [INSERT_SUBSET,EMPTY_SUBSET,ref_set_def,IN_UNION]
619    \\ REPEAT STRIP_TAC
620    THEN1 (DISJ1_TAC \\ SIMP_TAC std_ss [GSPECIFICATION]
621           \\ Q.EXISTS_TAC `1` \\ SIMP_TAC std_ss [] \\ DECIDE_TAC)
622    \\ DISJ2_TAC \\ SIMP_TAC std_ss [GSPECIFICATION]
623    THEN1 (Q.EXISTS_TAC `8` \\ SIMP_TAC std_ss [])
624    THEN1 (Q.EXISTS_TAC `7` \\ SIMP_TAC std_ss [])
625    THEN1 (Q.EXISTS_TAC `6` \\ SIMP_TAC std_ss [])
626    THEN1 (Q.EXISTS_TAC `5` \\ SIMP_TAC std_ss [])
627    THEN1 (Q.EXISTS_TAC `4` \\ SIMP_TAC std_ss [])
628    THEN1 (Q.EXISTS_TAC `3` \\ SIMP_TAC std_ss [])
629    THEN1 (Q.EXISTS_TAC `2` \\ SIMP_TAC std_ss [])
630    THEN1 (Q.EXISTS_TAC `1` \\ SIMP_TAC std_ss [])
631    THEN1 (Q.EXISTS_TAC `0` \\ SIMP_TAC (std_ss++WORD_ss) []),
632    FULL_SIMP_TAC bool_ss [IN_INSERT,NOT_IN_EMPTY]
633    \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,word_arith_lemma1,word_arith_lemma2]
634    \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,GSYM ALIGNED_def]
635    \\ REWRITE_TAC [word_sub_def] \\ REPEAT STRIP_TAC
636    \\ MATCH_MP_TAC ALIGNED_ADD \\ ASM_SIMP_TAC bool_ss [] \\ EVAL_TAC]);
637
638val arm_collect_lemma = store_thm("arm_collect_lemma",
639  ``ok_state (i,e,rs,l,u,m) ==>
640    arm_coll_inv (a,x,xs) (i,e,rs,l,u,m) ==>
641    (cheney_collector (i,e,rs,l,u,m) = (i',e',rs',l',u',m')) ==>
642    (arm_collect (r7,r8,a,x,xs) = (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
643    arm_collect_pre (r7,r8,a,x,xs) /\
644    arm_coll_inv (a,x,xs') (i,e',rs',l',u',m') /\ (x = x') /\
645    (r3' = ref_addr a i') /\ (r4' = ref_addr a e') /\ (a = a') /\ (l = l')``,
646  STRIP_TAC \\ STRIP_TAC \\ IMP_RES_TAC arm_coll_inv_pre_lemma
647  \\ ONCE_REWRITE_TAC [def7]
648  \\ FULL_SIMP_TAC bool_ss [GSYM AND_IMP_INTRO,arm_coll_inv_def]
649  \\ POP_ASSUM (STRIP_ASSUME_TAC o RW [arm_coll_inv_def])
650  \\ ASM_SIMP_TAC bool_ss [LET_DEF]
651  \\ ASM_SIMP_TAC std_ss [arm_c_init_lemma]
652  \\ Q.ABBREV_TAC `xs1 = (a - 28w =+ (if u then 1w else 0w)) xs`
653  \\ Q.ABBREV_TAC `r4l = a + 12w + (if u then 0w else n2w (12 * l))`
654  \\ Q.ABBREV_TAC `xs2 = (a + 4w =+ r4l + n2w (12 * l)) xs1`
655  \\ `?r43 r53 r63 r73 r83 a3 x3 xs3.
656        arm_move_roots (r4l,r4l + n2w (12 * l),6w,r7,r8,a - 24w,x,xs2) =
657         (r43,r53,r63,r73,r83,a3,x3,xs3)` by METIS_TAC [PAIR]
658  \\ `?r34 r44 r54 r64 r74 r84 x4 xs4. arm_cheney_loop (r4l,r43,r53,r63,r73,r83,x3',xs3) =
659                    (r34,r44,r54,r64,r74,r84,x4,xs4)` by METIS_TAC [PAIR]
660  \\ ASM_SIMP_TAC std_ss [LET_DEF,cheney_collector_def]
661  \\ Q.ABBREV_TAC `b = if ~u then 1 + l else 1`
662  \\ `?ys j2 m2. move_roots ([x1; x2; x3; x4; x5; x6],b,m) = (ys,j2,m2)` by METIS_TAC [PAIR]
663  \\ `?i3 m3. cheney (b,j2,b + l,m2) = (i3,m3)` by METIS_TAC [PAIR]
664  \\ ASM_SIMP_TAC std_ss []
665  \\ ASM_SIMP_TAC std_ss [LET_DEF]
666  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO]
667  \\ REPEAT (MATCH_MP_TAC (METIS_PROVE [] ``P ==> (Q ==> P)``))
668  \\ `roots_in_mem (rs ++ [i;e]) (a,a - 24w,xs1)` by
669   (Q.UNABBREV_TAC `xs1`
670    \\ FULL_SIMP_TAC bool_ss [APPEND,roots_in_mem_def,APPLY_UPDATE_THM,ZIP]
671    \\ SIMP_TAC (std_ss++WORD_ss) [WORD_EQ_ADD_LCANCEL,n2w_11,
672      RW [WORD_ADD_0] (Q.SPECL [`v`,`w`,`0w`] WORD_EQ_ADD_LCANCEL)])
673  \\ Q.PAT_X_ASSUM `roots_in_mem ppp (aaa,bbb,xs)` (K ALL_TAC)
674  \\ Q.PAT_X_ASSUM `rs = ppppp` ASSUME_TAC
675  \\ Q.PAT_X_ASSUM `rs2 = ppppp` ASSUME_TAC
676  \\ `roots_in_mem (rs ++ [i;b+l]) (a,a - 24w,xs2) /\ a + 4w <+ ref_addr a 1` by
677   (Q.UNABBREV_TAC `xs2` \\ Q.UNABBREV_TAC `b`
678    \\ FULL_SIMP_TAC bool_ss [APPEND,roots_in_mem_def,APPLY_UPDATE_THM,ZIP]
679    \\ FULL_SIMP_TAC (std_ss++WORD_ss) [WORD_EQ_ADD_LCANCEL,n2w_11,
680      RW [WORD_ADD_0] (Q.SPECL [`v`,`w`,`0w`] WORD_EQ_ADD_LCANCEL)]
681    \\ Q.UNABBREV_TAC `r4l` \\ Cases_on `u`
682    \\ SIMP_TAC std_ss [ref_addr_def,DECIDE ``~(m+1 = 0)``,GSYM WORD_ADD_ASSOC,
683         word_add_n2w,LEFT_ADD_DISTRIB,AC ADD_COMM ADD_ASSOC])
684  \\ IMP_RES_TAC (SIMP_RULE std_ss [LET_DEF] ok_state_IMP_cheney_inv)
685  \\ Q.UNABBREV_TAC `b`
686  \\ Q.ABBREV_TAC `b = if ~u then 1 + l else 1`
687  \\ Q.PAT_X_ASSUM `rs = [x1; x2; x3; x4; x5; x6]` ASSUME_TAC
688  \\ FULL_SIMP_TAC bool_ss []
689  \\ `ref_cheney_inv (b,b,b,b,b+l,l+l+1,m,m,m,{}) (a,ref_addr a b,r4l,x,xs2,xs2)` by
690   (ASM_REWRITE_TAC [ref_cheney_inv_def,CONJ_ASSOC]
691    \\ Q.UNABBREV_TAC `r4l` \\ Q.UNABBREV_TAC `b`  \\ REVERSE STRIP_TAC
692    THEN1 (Cases_on `u` \\ SIMP_TAC std_ss [ref_addr_def,WORD_ADD_0,
693      LEFT_ADD_DISTRIB,GSYM word_add_n2w,WORD_ADD_ASSOC])
694    \\ REVERSE STRIP_TAC
695    THEN1 (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [valid_address_def] \\ DECIDE_TAC)
696    \\ Q.UNABBREV_TAC `xs2`
697    \\ Q.UNABBREV_TAC `xs1`
698    \\ MATCH_MP_TAC (Q.GEN `xs` lemma) \\ ASM_SIMP_TAC bool_ss []
699    \\ Q.EXISTS_TAC `(a - 28w =+ (if u then 1w else 0w)) xs`
700    \\ MATCH_MP_TAC lemma \\ ASM_SIMP_TAC bool_ss [])
701  \\ FULL_SIMP_TAC bool_ss [APPEND]
702  \\ `root_address_ok (a - 24w) 6 x /\ a - 28w IN x /\ a - 32w IN x /\ a + 4w IN x /\
703      ALIGNED (a-32w) /\ ALIGNED (a-28w) /\ ALIGNED (a+4w)` by
704   (REWRITE_TAC [GSYM (EVAL ``(SUC(SUC(SUC(SUC(SUC(SUC 0))))))``),root_address_ok_def]
705    \\ FULL_SIMP_TAC bool_ss [ref_cheney_def,IN_INSERT]
706    \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,word_arith_lemma1,word_arith_lemma2]
707    \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4] \\ METIS_TAC [])
708  \\ FULL_SIMP_TAC bool_ss []
709  \\ STRIP_ASSUME_TAC
710    ((UNDISCH_ALL o Q.INST [`f`|->`l+l+1`])
711    (Q.INST [`r5n`|->`r53`,`r6n`|->`r63`,`r7n`|->`r73`,`r8n`|->`r83`,`xn`|->`x3'`]
712    (Q.SPECL [`b`,`m`,`r4l`,`r4l + n2w (12 * l)`,`r7`,`r8`,`xs2`,`a - 24w`,`ys`,`j2`,`m2`]
713    (Q.INST [`e`|->`b+l`,`j'`|->`b`,`w`|->`m`,`ww`|->`m`,`r`|->`{}`,`i`|->`b`,`r3`|->`ref_addr a b`,`r4n`|->`r43`,`r12n`|->`a3`,`xsn`|->`xs3`,`ii`|->`i`]
714    (SIMP_RULE std_ss [APPEND,GSYM AND_IMP_INTRO,LENGTH,ADD1] (Q.SPEC `[ii;e]` ref_cheney_move_roots6))))))
715  \\ `ref_cheney_inv (b,b,j2,j2,b + l,l+l+1,m2,m2,m,RANGE (b,j2)) (a,r4l,r43,x,xs3,xs3)` by
716   (REWRITE_TAC [ref_cheney_inv_def] \\ REPEAT STRIP_TAC THENL [
717      FULL_SIMP_TAC bool_ss [ref_cheney_inv_def] \\ IMP_RES_TAC cheney_inv_setup
718      \\ FULL_SIMP_TAC bool_ss [cheney_inv_def] \\ METIS_TAC [],
719      FULL_SIMP_TAC bool_ss [ref_cheney_inv_def],
720      MATCH_MP_TAC va_IMP \\ Q.EXISTS_TAC `l+l+1` \\ ASM_SIMP_TAC bool_ss []
721      \\ Q.UNABBREV_TAC `b` \\ Cases_on `u` \\ REWRITE_TAC [] \\ DECIDE_TAC,
722      FULL_SIMP_TAC bool_ss [ref_cheney_inv_def],
723      FULL_SIMP_TAC bool_ss [ref_cheney_inv_def]])
724  \\ `ref_cheney_inv (b,b,j2,j2,b + l,l + l + 1,m2,m2,m,RANGE (b,j2))
725        (a,r4l,r43,x3',xs3,xs3)` by METIS_TAC []
726  \\ (STRIP_ASSUME_TAC o
727      UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
728      Q.SPECL [`b`,`b`,`j2`,`b+l`,`m2`,`m2`,`x`,`RANGE(b,j2)`,`r4l`,`r43`,`r53`,`r63`,`r73`,`r83`,`x3'`,`xs3`,`i3`,`m3`,`r34`,`r44`,`r54`,`r64`,`r74`,`r84`,`x4'`,`xs4`] o
729      Q.INST [`xx`|->`m`,`ys`|->`xs3`,`f`|->`l+l+1`,`d`|->`x`])
730      (INST_TYPE [``:'a``|->``:word32``] ref_cheney_loop_th)
731  \\ Q.PAT_X_ASSUM `ref_cheney_inv ppppp (a,r34,r44,x3',xs4,xs3)` (STRIP_ASSUME_TAC o RW [ref_cheney_inv_def])
732  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
733  \\ ASM_SIMP_TAC bool_ss [WORD_SUB_ADD,GSYM ALIGNED_def]
734  \\ SIMP_TAC std_ss [def6,LET_DEF]
735  \\ `?x1' x2' x3' x4' x5' x6'. ys = [x1'; x2'; x3'; x4'; x5'; x6']` by
736   (Cases_on `ys`    \\ FULL_SIMP_TAC std_ss [LENGTH]
737    \\ Cases_on `t`  \\ FULL_SIMP_TAC std_ss [LENGTH]
738    \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH]
739    \\ Cases_on `t`  \\ FULL_SIMP_TAC std_ss [LENGTH]
740    \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH]
741    \\ Cases_on `t`  \\ FULL_SIMP_TAC std_ss [LENGTH]
742    \\ Cases_on `t'`  \\ FULL_SIMP_TAC std_ss [LENGTH,CONS_11,ADD1,GSYM ADD_ASSOC]
743    \\ FULL_SIMP_TAC bool_ss [DECIDE ``~(n + 7 = 6)``])
744  \\ FULL_SIMP_TAC bool_ss [CONS_11,APPEND]
745  \\ `xs4 (a-28w) = xs2 (a-28w)` by METIS_TAC [ref_cheney_def]
746  \\ `xs4 (a-32w) = xs2 (a-32w)` by METIS_TAC [ref_cheney_def]
747  \\ Q.PAT_X_ASSUM ` !i. i <+ a - 24w ==> (xs2 i = xs3 i)` (ASSUME_TAC o GSYM)
748  \\ `~(b = 0) /\ ~(b + l = 0)` by
749    (Q.UNABBREV_TAC `b` \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [LET_DEF,ok_state_def] \\ DECIDE_TAC)
750  \\ `(a + 4w <+ ref_addr a 1) /\ (xs3 (a+4w) = ref_addr a (b + l))` by FULL_SIMP_TAC (std_ss++WORD_ss) [roots_in_mem_def]
751  \\ REWRITE_TAC [GSYM CONJ_ASSOC]
752  \\ STRIP_TAC THEN1 METIS_TAC [roots_in_mem_carry_over]
753  \\ REVERSE STRIP_TAC THENL [
754    `(xs4 (a - 32w) = xs3 (a - 32w)) /\ (xs4 (a + 4w) = xs3 (a + 4w)) /\
755     (xs4 (a - 28w) = xs3 (a - 28w))` by METIS_TAC [ref_cheney_def]
756    \\ ASM_SIMP_TAC bool_ss []
757    \\ Q.UNABBREV_TAC `xs2` \\ Q.UNABBREV_TAC `xs1` \\ Cases_on `u`
758    \\ FULL_SIMP_TAC (std_ss++WORD_ss) [APPLY_UPDATE_THM,WORD_EQ_ADD_LCANCEL,n2w_11,
759        RW [WORD_ADD_0] (Q.SPECL [`v`,`w`,`0w`] WORD_EQ_ADD_LCANCEL)],
760    FULL_SIMP_TAC bool_ss [ref_cheney_def,CUT_def]
761    \\ FULL_SIMP_TAC bool_ss [ref_cheney_def,GSYM CUT_def]
762    \\ METIS_TAC [ref_mem_def]]);
763
764
765val _ = export_theory();
766