1
2open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_gc";
3
4open decompilerLib compilerLib prog_armLib;
5
6open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory;
7open combinTheory finite_mapTheory addressTheory;
8
9open tailrecLib tailrecTheory;
10open cheney_gcTheory cheney_allocTheory; (* an abstract implementation is imported *)
11
12
13infix \\ << >>
14val op \\ = op THEN;
15val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"];
16val RW = REWRITE_RULE;
17val RW1 = ONCE_REWRITE_RULE;
18
19val decompile_arm = decompile arm_tools;
20val basic_decompile_arm = basic_decompile arm_tools;
21
22val (th,def1) = decompile_arm "arm_move" `
23  E3150003 (* tst r5,#3 *)
24  1A000008 (* bne L1 *)
25  E5957000 (* ldr r7,[r5] *)
26  E2078003 (* and r8,r7,#3 *)
27  E3580001 (* cmp r8,#1 *)
28  15958004 (* ldrne r8,[r5,#4] *)
29  14847004 (* strne r7,[r4],#4 *)
30  14848004 (* strne r8,[r4],#4 *)
31  12447007 (* subne r7,r4,#7 *)
32  15857000 (* strne r7,[r5] *)
33  E2475001 (* sub r5,r7,#1 *)`;
34
35val (th,def2) = decompile_arm "arm_move2" `
36  E3160003 (* L1:tst r6,#3 *)
37  1A000008 (* bne L2 *)
38  E5967000 (* ldr r7,[r6] *)
39  E2078003 (* and r8,r7,#3 *)
40  E3580001 (* cmp r8,#1 *)
41  15968004 (* ldrne r8,[r6,#4] *)
42  14847004 (* strne r7,[r4],#4 *)
43  14848004 (* strne r8,[r4],#4 *)
44  12447007 (* subne r7,r4,#7 *)
45  15867000 (* strne r7,[r6] *)
46  E2476001 (* sub r6,r7,#1 *)`;
47
48val (th,def3) = decompile_arm "arm_cheney_step" `
49  E5935000 (* ldr r5,[r3] *)
50  E5936004 (* ldr r6,[r3,#4] *)
51  insert: arm_move
52  insert: arm_move2
53  E4835004 (* L2:str r5,[r3],#4 *)
54  E4836004 (* str r6,[r3],#4 *)`;
55
56val (th,def4) = basic_decompile_arm "arm_cheney_loop" NONE `
57  E1530004 (* CHENEY:cmp r3,r4 *)
58  0A00001A (* beq EXIT *)
59  insert: arm_cheney_step
60  EAFFFFE2 (* b CHENEY *)`;
61
62val (th,def5) = basic_decompile_arm "arm_move_roots" NONE `
63  E3560000 (* ROOTS:cmp r6,#0 *)
64  0A00000E (* beq CHENEY *)
65  E5995000 (* ldr r5,[r9] *)
66  insert: arm_move
67  E2466001 (* RL:sub r6,r6,#1 *)
68  E4895004 (* str r5,[r9],#4 *)
69  EAFFFFEE (* b ROOTS *)`;
70
71val (th,def6) = decompile_arm "arm_c_init" `
72  E2355001 (* eors r5,r5,#1 *)    (* calc u *)
73  E2893008 (* add r3,r9,#8 *)     (* set i *)
74  00833006 (* addeq r3,r3,r6 *)`;
75
76val (th,def7) = decompile_arm "arm_collect" `
77  E519501C (* ldr r5,[r9,#-28] *)
78  E5196020 (* ldr r6,[r9,#-32] *)
79  insert: arm_c_init
80  E509501C (* str r5,[r9,#-28] *)
81  E0835006 (* add r5,r3,r6 *)
82  E1A04003 (* mov r4,r3 *)
83  E5895004 (* str r5,[r9,#4] *)
84  E3A06006 (* mov r6,#6 *)
85  E2499018 (* sub r9,r9,#24 *)
86  insert: arm_move_roots
87  insert: arm_cheney_loop  (* main loop *)
88  E5994004 (* EXIT:ldr r4,[r9,#4] *)`;
89
90val (th,def8) = decompile_arm "arm_alloc_aux" `
91  E1530004 (* cmp r3,r4 *)
92  1A000039 (* bne NO_GC *)
93  insert: arm_collect`;
94
95val (th,def9) = decompile_arm "arm_alloc_aux2" `
96  E5197018 (* NO_GC:ldr r7,[r9,#-24] *)
97  E5198014 (* ldr r8,[r9,#-20] *)
98  E1530004 (* cmp r3,r4 *)
99  15093018 (* strne r3,[r9,#-24] *)
100  14837004 (* strne r7,[r3],#4 *)
101  14838004 (* strne r8,[r3],#4 *)
102  03A07002 (* moveq r7,#2 *)
103  05097018 (* streq r7,[r9,#-24] *)
104  E5893000 (* str r3,[r9] *)`;
105
106val (th,def10) = decompile_arm "arm_alloc_mem" `
107  E5993000 (* ldr r3,[r9] *)
108  E5994004 (* ldr r4,[r9,#4] *)
109  insert: arm_alloc_aux
110  insert: arm_alloc_aux2`;
111
112val (arm_alloc_thm,def11) = decompile_arm "arm_alloc" `
113  E5093018 (* str r3,[r9,#-24] *)
114  E5094014 (* str r4,[r9,#-20] *)
115  E5095010 (* str r5,[r9,#-16] *)
116  E509600C (* str r6,[r9,#-12] *)
117  E5097008 (* str r7,[r9,#-8] *)
118  E5098004 (* str r8,[r9,#-4] *)
119  insert: arm_alloc_mem
120  E5193018 (* ldr r3,[r9,#-24] *)
121  E5194014 (* ldr r4,[r9,#-20] *)
122  E5195010 (* ldr r5,[r9,#-16] *)
123  E519600C (* ldr r6,[r9,#-12] *)
124  E5197008 (* ldr r7,[r9,#-8] *)
125  E5198004 (* ldr r8,[r9,#-4] *)`;
126
127val _ = save_thm("arm_alloc_thm",arm_alloc_thm);
128
129
130(* proof *)
131
132val ref_addr_def = Define `
133  ref_addr a n = a + n2w (8 * n):word32`;
134
135val ref_field_def = Define `
136  ref_field a (n,x) = if n = 0 then
137    ADDR32 (FST x) + (if SND x then 3w else 2w) else ref_addr a n`;
138
139val ref_mem_def = Define `
140  (ref_mem i EMP (a,xs) = T) /\
141  (ref_mem i (REF j) (a,xs) =
142    (xs (ref_addr a i) = ref_addr a j + 1w)) /\
143  (ref_mem i (DATA (x,y,z,q)) (a,xs) =
144    (xs (ref_addr a i) = ref_field a (x,z)) /\
145    (xs (ref_addr a i + 4w) = ref_field a (y,q)))`;
146
147val valid_address_def = Define `
148  valid_address a i = w2n a + 8 * i + 8 < 2**32`;
149
150val ref_set_def = Define `
151  ref_set a f = { a + n2w (4 * i) | i < 2 * f + 4 } UNION { a - n2w (4 * i) | i <= 8 }`;
152
153val ref_cheney_def = Define `
154  ref_cheney (m,e) (a,d,xs,ys) =
155    ~(a = 0w) /\ (a && 3w = 0w) /\ (!i. i <= e ==> ref_mem i (m i) (a,xs)) /\
156    (m 0 = EMP) /\ valid_address a e /\ (!i. i <+ ref_addr a 1 ==> (xs i = ys i)) /\
157    (ref_set a e = d)`;
158
159val ref_addr_NOT_ZERO = prove(
160  ``!a. ref_cheney (m,e) (a,d,xs,ys) /\ x <= e /\ ~(x = 0) ==> ~(ref_addr a x = 0w)``,
161  Cases_word \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [ref_cheney_def,ref_addr_def,
162    word_add_n2w,n2w_11,valid_address_def,w2n_n2w] \\ REPEAT STRIP_TAC
163  \\ `(n + 8 * x) < 4294967296` by DECIDE_TAC
164  \\ `n + 8 * x = 0` by METIS_TAC [LESS_MOD] \\ DECIDE_TAC);
165
166val ref_field_NOT_ZERO = prove(
167  ``!a. ref_cheney (m,e) (a,d,xs,ys) /\ x <= e ==> ~(ref_field a (x,xx) = 0w)``,
168  REVERSE (Cases_on `x = 0`) THEN1 METIS_TAC [ref_addr_NOT_ZERO,ref_field_def]
169  \\ Cases_on `xx` \\ Cases_on `r`
170  \\ ASM_SIMP_TAC bool_ss [ref_field_def,FST,SND] \\ REPEAT STRIP_TAC
171  \\ Q.PAT_X_ASSUM `dfg = 0w` MP_TAC \\ REWRITE_TAC [ADDR32_ADD_EQ_ZERO]);
172
173val ref_addr_NEQ = prove(
174  ``!a i j. ~(i = j) /\ valid_address a i /\ valid_address a j ==> ~(ref_addr a i = ref_addr a j)``,
175  Cases_word \\ Cases \\ Cases
176  \\ SIMP_TAC std_ss [ref_addr_def,valid_address_def,word_add_n2w]
177  \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,LESS_MOD,n2w_11,DECIDE ``~(SUC n = 0)``]
178  \\ STRIP_TAC \\ IMP_RES_TAC (DECIDE ``m + n + 8 < l ==> m + n + 4 < l /\ m + n < l``)
179  \\ ASM_SIMP_TAC bool_ss [LESS_MOD] \\ DECIDE_TAC);
180
181val ref_addr_ADD_NEQ = prove(
182  ``!a i j. valid_address a i /\ valid_address a j ==> ~(ref_addr a i + 4w = ref_addr a j)``,
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 ``n + 8 < l ==> n + 4 < l /\ n < l``)
186  \\ ASM_SIMP_TAC bool_ss [LESS_MOD,MULT_CLAUSES]
187  \\ FULL_SIMP_TAC std_ss [EQ_ADD_LCANCEL,GSYM ADD_ASSOC] \\ REPEAT STRIP_TAC
188  \\ REPEAT DECIDE_TAC
189  \\ IMP_RES_TAC (METIS_PROVE [] ``(m = n) ==> (m MOD 8 = n MOD 8)``)
190  \\ FULL_SIMP_TAC std_ss [RW1 [MULT_COMM] (CONJ MOD_TIMES MOD_EQ_0)]);
191
192val ALIGNED_ref_addr = prove(
193  ``!n a. ALIGNED a ==> ALIGNED (ref_addr a n)``,
194  REWRITE_TAC [ref_addr_def,ALIGNED_def]
195  \\ REWRITE_TAC [GSYM ALIGNED_def,GSYM (EVAL ``4 * 2``),GSYM word_mul_n2w]
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 = prove(
203  ``ref_cheney (m,f) (a,d,xs,ys) /\ ~(x = 0) /\ x <= f ==> ref_addr a x IN d /\ ref_addr a x + 4w IN d``,
204  REWRITE_TAC [ref_cheney_def] \\ REPEAT STRIP_TAC
205  \\ Q.PAT_X_ASSUM `ref_set a f = d` (ASSUME_TAC o GSYM)
206  \\ ASM_SIMP_TAC bool_ss [ref_set_def,GSPECIFICATION,IN_UNION,ref_addr_def]
207  \\ DISJ1_TAC THENL [Q.EXISTS_TAC `2*x`,Q.EXISTS_TAC `2*x+1`]
208  \\ ASM_SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB,
209      GSYM word_add_n2w,WORD_ADD_ASSOC] \\ DECIDE_TAC);
210
211fun UPDATE_ref_addr_prove (c,tm) = prove(tm,
212  Cases_word \\ Cases_word \\ REPEAT STRIP_TAC
213  \\ sg c \\ ASM_SIMP_TAC bool_ss[APPLY_UPDATE_THM]
214  \\ Cases_on `x` \\ FULL_SIMP_TAC bool_ss []
215  \\ CCONTR_TAC \\ FULL_SIMP_TAC bool_ss [valid_address_def]
216  \\ Q.PAT_X_ASSUM `n' < dimword (:32)` ASSUME_TAC
217  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [LESS_MOD,w2n_n2w,ref_addr_def,WORD_LO,word_add_n2w]
218  \\ `(n' + 8 * SUC n'') < 4294967296 /\ (n' + 8) < 4294967296` by DECIDE_TAC
219  \\ `(n' + 8 * SUC n'' + 4) < 4294967296` by DECIDE_TAC
220  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [LESS_MOD,w2n_n2w,ref_addr_def,WORD_LO,word_add_n2w]
221  \\ DECIDE_TAC);
222
223val UPDATE_ref_addr = UPDATE_ref_addr_prove(`~(n2w n = ref_addr (n2w n') x)`,
224  ``!i a. valid_address a x /\ ~(x=0) /\ i <+ ref_addr a 1 /\ (xs i = ys i) ==>
225          ((ref_addr a x =+ y) xs i = ys i)``);
226
227val UPDATE_ref_addr4 = UPDATE_ref_addr_prove(`~(n2w n = ref_addr (n2w n') x + 4w)`,
228  ``!i a. valid_address a x /\ ~(x=0) /\ i <+ ref_addr a 1 /\ (xs i = ys i) ==>
229          ((ref_addr a x + 4w =+ y) xs i = ys i)``);
230
231val va_IMP = prove(
232  ``!a e i. valid_address a e /\ i <= e ==> valid_address a i``,
233  SIMP_TAC bool_ss [valid_address_def] \\ DECIDE_TAC);
234
235val ref_cheney_update_REF = prove(
236  ``ref_cheney (m,e) (a,d,xs,ys) /\ j <= e /\ x <= e /\ ~(x = 0) ==>
237    ref_cheney ((x =+ REF j) m,e) (a,d,(ref_addr a x =+ ref_addr a j + 1w) xs,ys)``,
238  SIMP_TAC bool_ss [ref_cheney_def] \\ REVERSE (REPEAT STRIP_TAC)
239  THEN1 (MATCH_MP_TAC UPDATE_ref_addr \\ METIS_TAC [va_IMP])
240  THEN1 ASM_SIMP_TAC bool_ss [UPDATE_def]
241  \\ Cases_on `i = x` \\ ASM_SIMP_TAC bool_ss [UPDATE_def,ref_mem_def]
242  \\ RES_TAC \\ Cases_on `m i` \\ FULL_SIMP_TAC bool_ss [ref_mem_def]
243  \\ `valid_address a i /\ valid_address a x` by METIS_TAC [va_IMP]
244  \\ `~(ref_addr a i = ref_addr a x)` by METIS_TAC [ref_addr_NEQ,va_IMP]
245  \\ ASM_SIMP_TAC bool_ss [] \\ Cases_on `p` \\ Cases_on `r` \\ Cases_on `r'`
246  \\ FULL_SIMP_TAC std_ss [ref_mem_def] \\ METIS_TAC [ref_addr_ADD_NEQ]);
247
248val ref_field_and_3 = prove(
249  ``!n a x m e d xs ys. ref_cheney (m,e) (a,d,xs,ys) ==> ((ref_field a (n,x) && 3w = 0w) = ~(n = 0))``,
250  STRIP_TAC \\ REVERSE (Cases_on `n = 0`) \\ ASM_SIMP_TAC bool_ss [ref_field_def]
251  THEN1 METIS_TAC [ref_field_def,ref_cheney_ALIGNED,GSYM ALIGNED_def]
252  \\ Cases_on `x` \\ Cases_on `r` \\ REWRITE_TAC [ref_field_def]
253  \\ SIMP_TAC std_ss [ALIGNED_add_3_and_3,ALIGNED_add_2_and_3,ALIGNED_ADDR32]
254  \\ EVAL_TAC \\ REWRITE_TAC []);
255
256val ref_field_and_3_EQ_1 = prove(
257  ``!x a y. ALIGNED a ==> ~(ref_field a (x,y) && 3w = 1w)``,
258  STRIP_TAC \\ Cases_on `x = 0` \\ ASM_SIMP_TAC bool_ss [ref_field_def] THENL [
259    Cases_on `y` \\ Cases_on `r` \\ REWRITE_TAC [FST,SND]
260    \\ METIS_TAC [ALIGNED_add_2_and_3,ALIGNED_add_3_and_3,
261         ALIGNED_ADDR32,EVAL ``~(2w = 1w:word32) /\ ~(3w = 1w:word32)``],
262    METIS_TAC [ALIGNED_ref_addr,ALIGNED_def,EVAL ``0w = 1w:word32``]]);
263
264val ref_cheney_move_lemma = prove(
265  ``ref_cheney (m,e) (a,d,xs,ys) /\ (~(x = 0) ==> ~(m x = EMP)) /\ (!x. ~(m x = REF 0)) /\
266    (move(x,j,m) = (x1,j1,m1)) /\ ~(j = 0) /\ j <= e /\ x <= e /\
267    (arm_move(ref_addr a j,ref_field a (x,xx),r7,r8,d,xs) = (j2,x2,r7_2,r8_2,d2,xs2)) ==>
268    ref_cheney (m1,e) (a,d,xs2,ys) /\ (x2 = ref_field a (x1,xx)) /\ (j2 = ref_addr a j1) /\ (d2 = d) /\
269    arm_move_pre(ref_addr a j,ref_field a (x,xx),r7,r8, d, xs)``,
270  SIMP_TAC std_ss [def1,GSYM AND_IMP_INTRO]
271  \\ STRIP_TAC \\ IMP_RES_TAC ref_field_and_3
272  \\ ASM_SIMP_TAC bool_ss []
273  \\ Q.PAT_X_ASSUM `!xnn.nnn` (K ALL_TAC)
274  \\ REWRITE_TAC [move_def] \\ Cases_on `x = 0`
275  THEN1 (Cases_on `xx` \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [])
276  \\ Cases_on `x <= e` \\ ASM_SIMP_TAC bool_ss []
277  \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ STRIP_TAC
278  \\ Cases_on `m x` \\ FULL_SIMP_TAC bool_ss [isREF_def,heap_type_11,getREF_def]
279  THEN1 (
280      ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss []
281      \\ SIMP_TAC std_ss [LET_DEF,GSYM AND_IMP_INTRO] \\ NTAC 2 STRIP_TAC
282      \\ IMP_RES_TAC ref_cheney_d \\ IMP_RES_TAC ref_cheney_ALIGNED
283      \\ FULL_SIMP_TAC bool_ss [ref_cheney_def,ref_mem_def]
284      \\ `ref_mem x (REF n) (a,xs)` by METIS_TAC []
285      \\ FULL_SIMP_TAC bool_ss [ref_cheney_def,ref_mem_def,ref_field_def]
286      \\ `ref_addr a n + 1w && 3w = 1w` by METIS_TAC [ALIGNED_add_1_and_3,ALIGNED_ref_addr,ALIGNED_def]
287      \\ ASM_SIMP_TAC bool_ss [PAIR_EQ,WORD_ADD_SUB]
288      \\ ASM_SIMP_TAC bool_ss [INSERT_SUBSET,EMPTY_SUBSET,ALIGNED_def]
289      \\ ONCE_REWRITE_TAC [WORD_AND_COMM]
290      \\ ASM_SIMP_TAC bool_ss [] \\ METIS_TAC [])
291  \\ SIMP_TAC std_ss [heap_type_distinct]
292  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss []
293  \\ SIMP_TAC std_ss [LET_DEF]
294  \\ `~(m x = EMP)` by METIS_TAC [heap_type_distinct]
295  \\ `valid_address a x` by METIS_TAC [ref_cheney_def,va_IMP]
296  \\ ASM_SIMP_TAC std_ss [word_arith_lemma1,WORD_ADD_SUB]
297  \\ IMP_RES_TAC (GEN_ALL ref_cheney_ALIGNED)
298  \\ ASM_SIMP_TAC std_ss [ref_field_def]
299  \\ `~(xs (ref_addr a x) && 3w = 1w)` by
300       (FULL_SIMP_TAC bool_ss [ref_cheney_def]
301        \\ Cases_on `p` \\ Cases_on `r` \\ Cases_on `r'`
302        \\ `ref_mem x (DATA (q,q',q'',r)) (a,xs)` by METIS_TAC []
303        \\ CCONTR_TAC \\ FULL_SIMP_TAC bool_ss [ref_mem_def]
304        \\ `ref_field a (q,q'') && 3w = 1w` by METIS_TAC []
305        \\ METIS_TAC [ALIGNED_def,ref_field_and_3_EQ_1])
306  \\ FULL_SIMP_TAC std_ss [PAIR_EQ,WORD_ADD_0,word_arith_lemma4]
307  \\ REVERSE (NTAC 6 STRIP_TAC) THEN1
308    (`~(j = 0)` by METIS_TAC []
309     \\ IMP_RES_TAC ref_cheney_d \\ IMP_RES_TAC ref_cheney_ALIGNED
310     \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,ALIGNED_def,LET_DEF,WORD_ADD_0,LENGTH]
311     \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
312     \\ ASM_REWRITE_TAC [RW [ALIGNED_def] ALIGNED_CLAUSES]
313     \\ SIMP_TAC std_ss [ref_addr_def,LEFT_ADD_DISTRIB,GSYM word_add_n2w,WORD_ADD_ASSOC])
314  \\ MATCH_MP_TAC ref_cheney_update_REF
315  \\ ASM_SIMP_TAC bool_ss []
316  \\ Cases_on `p` \\ Cases_on `r` \\ Cases_on `r'` \\ FULL_SIMP_TAC std_ss [ref_cheney_def]
317  \\ REVERSE (REPEAT STRIP_TAC) THENL [ALL_TAC,ASM_SIMP_TAC std_ss [UPDATE_def],ALL_TAC]
318  THEN1 (`valid_address a j` by METIS_TAC [va_IMP,UPDATE_ref_addr4,UPDATE_ref_addr]
319         \\ MATCH_MP_TAC UPDATE_ref_addr4 \\ ASM_SIMP_TAC bool_ss []
320         \\ MATCH_MP_TAC UPDATE_ref_addr \\ ASM_SIMP_TAC bool_ss [])
321  \\ `ref_mem x (DATA (q,q',q'',r)) (a,xs)` by METIS_TAC []
322  \\ Cases_on `i = j`
323  THEN1 (FULL_SIMP_TAC bool_ss [UPDATE_def,ref_mem_def,WORD_EQ_ADD_LCANCEL,
324           RW[WORD_ADD_0](Q.SPECL[`x`,`y`,`0w`]WORD_EQ_ADD_LCANCEL)]
325         \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11])
326  \\ `ref_mem i (m i) (a,xs)` by METIS_TAC []
327  \\ CONV_TAC (RATOR_CONV (SIMP_CONV std_ss [UPDATE_def]))
328  \\ ASM_SIMP_TAC bool_ss []
329  \\ Cases_on `m i` \\ 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  \\ `valid_address a i /\ valid_address a j` by METIS_TAC [va_IMP]
332  THEN1 ASM_SIMP_TAC bool_ss [ref_addr_ADD_NEQ]
333  \\ Cases_on `p` \\ Cases_on `r` \\ Cases_on `r'` \\ 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_field a (x,xx),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_field a (x2,xx) = xx2) /\ (ref_addr a j2 = xj2) /\ (d = d2) /\
345    arm_move_pre(ref_addr a j,ref_field a (x,xx), r7,r8, d, xs)``,
346  NTAC 28 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 d1a. getDATA (m i) = (x1,y1,d1,d1a)` 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 + 8w` 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 ad1. m i = DATA(ax,ay,ad,ad1)` by METIS_TAC [m_DATA,PAIR]
400  \\ `(x1,y1,d1',d1a) = (ax,ay,ad,ad1)` by METIS_TAC [getDATA_def]
401  \\ FULL_SIMP_TAC bool_ss [PAIR_EQ]
402  \\ Q.PAT_X_ASSUM `getDATA (DATA (ax,ay,ad,ad1)) = (ax,ay,ad,ad1)` (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,ad1)) (a,xs)` by METIS_TAC [ref_cheney_def]
415  \\ FULL_SIMP_TAC bool_ss [ref_mem_def]
416  \\ `(r51 = ref_field a (ax,ad)) /\ (r61 = ref_field a (ay,ad1))` 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,ad1)) (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 28 STRIP_TAC
464  \\ ONCE_REWRITE_TAC [def4]
465  \\ SIMP_TAC std_ss []
466  \\ Cases_on `i = j` THEN1
467    (Q.PAT_X_ASSUM `!m.bb` (K ALL_TAC)
468     \\ FULL_SIMP_TAC std_ss [ref_cheney_inv_def] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
469     \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [])
470  \\ Q.PAT_X_ASSUM `ref_cheney_inv (b,i,j,j,e,f,m,x,xx,r) (a,r3,r4,d,xs,ys)`
471      (fn th => STRIP_ASSUME_TAC (RW [ref_cheney_inv_def] th) \\ ASSUME_TAC th)
472  \\ `i <= j /\ j <= e` by METIS_TAC [cheney_inv_def]
473  \\ Cases_on `v = 0` THEN1 `F` by DECIDE_TAC
474  \\ `valid_address a i /\ valid_address a j /\ ~(e < i)` by
475    (FULL_SIMP_TAC bool_ss [valid_address_def] \\ DECIDE_TAC)
476  \\ ASM_REWRITE_TAC [] \\ SIMP_TAC (std_ss++pbeta_ss) [LET_DEF]
477  \\ `?i2 j2 e2 m2. cheney_step (i,j,e,m) = (i2,j2,e2,m2)` by METIS_TAC [PAIR]
478  \\ `?r31 r41 r51 r61 r71 r81 d1 xs1. arm_cheney_step (ref_addr a i,ref_addr a j,r7,r8,d,xs) =
479                      (r31,r41,r51,r61,r71,r81,d1,xs1)` by METIS_TAC [PAIR]
480  \\ `~(ref_addr a i = ref_addr a j)` by METIS_TAC [ref_addr_NEQ]
481  \\ ASM_REWRITE_TAC []
482  \\ STRIP_TAC
483  \\ `e - (i + 1) < v` by DECIDE_TAC
484  \\ Q.PAT_X_ASSUM `!m. m < v ==> !e i. bbb`
485    (ASSUME_TAC o RW [] o Q.SPECL [`e`,`i+1`] o UNDISCH o Q.SPEC `e - (i + 1)`)
486  \\ `ref_cheney_inv (b,i2,j2,j2,e2,f,m2,x,xx,r) (a,r31,r41,d,xs1,ys) /\ (d = d1) /\
487      arm_cheney_step_pre (r3,r4,r7,r8,d,xs)` by METIS_TAC [ref_cheney_step_thm]
488  \\ `(i2 = i+1) /\ (e2 = e)` by FULL_SIMP_TAC (std_ss++pbeta_ss) [cheney_step_def,LET_DEF]
489  \\ METIS_TAC []);
490
491val SING_IN_SUBSET0 = prove(
492  ``x IN t /\ t SUBSET0 s ==> {x} SUBSET0 s``,
493  SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY]);
494
495val roots_in_mem_def = Define `
496  (roots_in_mem [] (a,r12,m) = T) /\
497  (roots_in_mem (x::xs) (a,r12,m) =
498      (m r12 = ref_field a x) /\ r12 <+ ref_addr a 1 /\ r12 <+ r12 + 4w /\
499      roots_in_mem xs (a,r12+4w,m))`;
500
501val NOT_ref_addr = prove(
502  ``!x a. valid_address a i /\ x <+ ref_addr a 1 /\ ~(i = 0) ==>
503          ~(x = ref_addr a i) /\ ~(x = ref_addr a i + 4w)``,
504  Cases_word \\ Cases_word \\ ASM_SIMP_TAC (std_ss++SIZES_ss)
505       [ref_addr_def,word_add_n2w,n2w_11,WORD_LO,w2n_n2w,valid_address_def,LESS_MOD]
506  \\ REPEAT STRIP_TAC
507  \\ `n' + 8 * i < 4294967296 /\ n' + 8 < 4294967296` by DECIDE_TAC
508  \\ `n' + 8 * i + 4 < 4294967296` by DECIDE_TAC
509  \\ FULL_SIMP_TAC std_ss [LESS_MOD] \\ DECIDE_TAC);
510
511val lemma = prove(
512  ``ref_cheney (m1,f) (a,d,xs1,xs) /\ r12 <+ ref_addr a 1 ==>
513    ref_cheney (m1,f) (a,d,(r12 =+ r51) xs1,(r12 =+ r51) xs1)``,
514  SIMP_TAC bool_ss [ref_cheney_def] \\ REPEAT STRIP_TAC
515  \\ Cases_on `m1 i` \\ ASM_REWRITE_TAC [ref_mem_def] THENL [
516    `ref_addr a n + 1w = xs1 (ref_addr a i)` by METIS_TAC [ref_mem_def]
517    \\ ASM_SIMP_TAC bool_ss [APPLY_UPDATE_THM]
518    \\ METIS_TAC [NOT_ref_addr,va_IMP,heap_type_distinct],
519    Cases_on `p` \\ Cases_on `r` \\ Cases_on `r'` \\ ASM_REWRITE_TAC [ref_mem_def]
520    \\ ASM_SIMP_TAC bool_ss [APPLY_UPDATE_THM]
521    \\ METIS_TAC [NOT_ref_addr,va_IMP,heap_type_distinct,ref_mem_def]]);
522
523val roots_lemma = prove(
524  ``!rs b k.
525      roots_in_mem rs (a,b + k,xs) ==> b <+ b + k ==>
526      ref_cheney (m,f) (a,d,xs1,xs) ==>
527      roots_in_mem rs (a,b + k,(b =+ r51) xs1)``,
528  Induct \\ REWRITE_TAC [roots_in_mem_def]
529  \\ SIMP_TAC std_ss [APPLY_UPDATE_THM,WORD_LOWER_NOT_EQ,GSYM WORD_ADD_ASSOC]
530  \\ REPEAT STRIP_TAC \\ METIS_TAC [ref_cheney_def,WORD_LOWER_TRANS]);
531
532val root_address_ok_def = Define `
533  (root_address_ok a 0 x = T) /\
534  (root_address_ok a (SUC n) x = ALIGNED a /\ a IN x /\ root_address_ok (a+4w) n x)`;
535
536val ref_cheney_move_roots = prove(
537  ``!rs zs ds j m r4 r5 r7 r8 xs r12 ys jn mn.
538      LENGTH rs < 2**32 /\ (LENGTH ds = LENGTH rs + LENGTH zs) /\
539      root_address_ok r12 (LENGTH rs) x /\
540      roots_in_mem (ZIP (rs++zs,ds)) (a,r12,xs) /\
541      (!x. MEM x rs ==> {x} SUBSET0 DR0 (ICUT (b,e) m)) /\
542      ref_cheney_inv (b,i,j,j',e,f,m,(w:num->((bool[30] # bool) # bool[30] # bool) heap_type),ww,r) (a,r3,r4,x,xs,xs) ==>
543      (arm_move_roots(r4,r5,n2w (LENGTH rs),r7,r8,r12,x,xs) = (r4n,r5n,r6n,r7n,r8n,r12n,xn,xsn)) /\
544      (move_roots(rs,j,m) = (ys,jn,mn)) ==>
545      arm_move_roots_pre(r4,r5,n2w (LENGTH rs),r7,r8,r12,x,xs) /\
546      ref_cheney_inv (b,i,jn,j',e,f,mn,w,ww,r) (a,r3,r4n,x,xsn,xsn) /\
547      roots_in_mem (ZIP (ys++zs,ds)) (a,r12,xsn) /\
548      (LENGTH ys = LENGTH rs) /\ (r12n = r12 + n2w (4 * LENGTH rs)) /\
549      (!i. i <+ r12 ==> (xs i = xsn i)) /\ (xn = x)``,
550  STRIP_TAC \\ STRIP_TAC \\ Induct_on `rs` THEN1
551   (ONCE_REWRITE_TAC [def5] \\ SIMP_TAC std_ss [LET_DEF]
552    \\ Cases_on `ys` \\ REWRITE_TAC [move_roots_def,PAIR_EQ,LENGTH,MAP,NOT_NIL_CONS]
553    \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [LENGTH,WORD_MULT_CLAUSES,WORD_ADD_0])
554  \\ POP_ASSUM (ASSUME_TAC o RW1 [GSYM CONTAINER_def])
555  \\ ONCE_REWRITE_TAC [def5] \\ SIMP_TAC std_ss [LET_DEF]
556  \\ Cases_on `ds`
557  \\ SIMP_TAC std_ss [LENGTH,ADD1,DECIDE ``(k + 1 = m + 1 + n) = (k = m + n:num)``,ZIP,APPEND]
558  \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LESS_MOD,LENGTH,DECIDE ``~(SUC n = 0)``]
559  \\ SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB]
560  \\ NTAC 12 STRIP_TAC
561  \\ `?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]
562  \\ ASM_REWRITE_TAC [LET_DEF,PAIR_EQ,move_roots_def,APPEND,MAP]
563  \\ `?y1 j1 m1. move (h',j,m) = (y1,j1,m1)` by METIS_TAC [PAIR]
564  \\ `?ys j2 m2. move_roots (rs,j1,m1) = (ys,j2,m2)` by METIS_TAC [PAIR]
565  \\ FULL_SIMP_TAC std_ss [LET_DEF,PAIR_EQ,move_roots_def,GSYM AND_IMP_INTRO,MAP] \\ STRIP_TAC
566  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC bool_ss []
567  \\ FULL_SIMP_TAC bool_ss [MAP,CONS_11,NOT_NIL_CONS,NOT_CONS_NIL,ZIP,APPEND,ADD1,EQ_ADD_RCANCEL,LENGTH]
568  \\ REPEAT (MATCH_MP_TAC (METIS_PROVE [] ``P ==> (Q ==> P)``))
569  \\ `LENGTH rs < 4294967296` by DECIDE_TAC
570  \\ FULL_SIMP_TAC bool_ss [roots_in_mem_def,MEM,ref_cheney_inv_def,APPEND]
571  \\ `{h'} SUBSET0 DR0 (ICUT(b,e)m)` by METIS_TAC [SING_IN_SUBSET0,IN_INSERT]
572  \\ `arm_move (ref_addr a j,ref_field a (h',h),r7,r8,x,xs) = (r41,r51,r71,r81,x1,xs1)` by METIS_TAC [WORD_ADD_0]
573  \\ FULL_SIMP_TAC bool_ss [FST,SND]
574  \\ (STRIP_ASSUME_TAC o GSYM o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
575   Q.SPECL [`a`,`b`,`b`,`i`,`j`,`j1`,`j'`,`e`,`m`,`m1`,
576    `w`,`ww`,`r`,`h'`,`r41`,`r51`,`xs`,`xs1`,`x`,`y1`,`h`,`r7`,`r8`,`r71`,`r81`,`x1`] o Q.INST [`ys`|->`xs`]) (INST_TYPE [``:'a``|->``:((bool[30] # bool) # bool[30] # bool)``] ref_cheney_move)
577  \\ ASM_SIMP_TAC bool_ss [WORD_ADD_0]
578  \\ `!x. MEM x rs ==> {x} SUBSET0 DR0 (ICUT (b,e) m1)` by METIS_TAC []
579  \\ `ref_cheney (m1,f) (a,x,(r12 =+ r51) xs1,(r12 =+ r51) xs1)` by METIS_TAC [lemma]
580  \\ `roots_in_mem (ZIP (rs++zs,t)) (a,r12 + 4w,(r12 =+ r51) xs1)` by METIS_TAC [roots_lemma]
581  \\ Q.PAT_X_ASSUM `r51 = ref_field a (y1,h)` ASSUME_TAC \\ FULL_SIMP_TAC bool_ss []
582  \\ FULL_SIMP_TAC std_ss [root_address_ok_def,ALIGNED_def,GSYM ADD1,move_roots_def]
583  \\ Q.PAT_X_ASSUM `CONTAINER (!j m xs r12. bbb)`
584    (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
585     Q.SPECL [`t`,`j1`,`m1`,`ref_field a (y1,h)`,`r71`,`r81`,`(r12 =+ ref_field a (y1,h)) xs1`,`r12+4w`,`ys'`,`j2`,`m2`] o
586     RW [CONTAINER_def])
587  \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,word_add_n2w,word_mul_n2w,
588       GSYM WORD_ADD_ASSOC,LEFT_ADD_DISTRIB,AC ADD_ASSOC ADD_COMM,FST]
589  \\ METIS_TAC [APPLY_UPDATE_THM,WORD_LOWER_TRANS,WORD_LOWER_NOT_EQ,ref_cheney_def]);
590
591val ref_cheney_move_roots6 =
592  SIMP_RULE std_ss [LENGTH,ADD1,AND_IMP_INTRO,GSYM CONJ_ASSOC]
593  (Q.SPEC `[x1;x2;x3;x4;x5;x6]` ref_cheney_move_roots);
594
595val arm_c_init_lemma = prove(
596  ``(arm_c_init(if u then 0w else 1w,r6,r9) =
597     (r9 + 8w + if u then 0w else r6, if u then 1w else 0w,r6,r9))``,
598  Cases_on `u` \\ SIMP_TAC std_ss [SIMP_RULE std_ss [LET_DEF] def6,
599    WORD_ADD_0,PAIR_EQ,WORD_XOR_CLAUSES,EVAL ``0w = 1w:word32``]);
600
601val arm_coll_inv_def = Define `
602  arm_coll_inv (a,x,xs) (i,e,rs,rs',l,u,m) =
603    ?x1 x2 x3 x4 x5 x6 y1 y2 y3 y4 y5 y6.
604      roots_in_mem (ZIP (rs,rs') ++ [(i,(0w,F));(e,(0w,F))]) (a,a-24w,xs) /\
605      (rs = [x1;x2;x3;x4;x5;x6]) /\ (rs' = [y1;y2;y3;y4;y5;y6]) /\
606      valid_address a (l + l + 1) /\
607      ref_cheney (m,l+l+1) (a,x,xs,xs) /\
608      (xs (a-28w) = if u then 0w else 1w) /\ a - 28w <+ ref_addr a 1 /\ a - 28w <+ a - 24w /\
609      (xs (a-32w) = n2w (8 * l)) /\ a - 32w <+ ref_addr a 1 /\ a - 32w <+ a - 24w`;
610
611val roots_in_mem_carry_over = prove(
612  ``!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)``,
613  Induct \\ FULL_SIMP_TAC bool_ss [roots_in_mem_def,ref_cheney_def] \\ METIS_TAC []);
614
615val arm_coll_inv_pre_lemma = prove(
616  ``arm_coll_inv (a,x,xs) (q,e,rs,rs',l,u,m) ==>
617    {a+4w;a-32w;a-28w;a-24w;a-20w;a-16w;a-12w;a-8w;a-4w;a} SUBSET x /\
618    !i. i IN {a+4w;a-32w;a-28w;a-24w;a-20w;a-16w;a-12w;a-8w;a-4w;a} ==> ALIGNED i``,
619  REWRITE_TAC [arm_coll_inv_def,ref_cheney_def] \\ REPEAT STRIP_TAC THENL [
620    Q.PAT_X_ASSUM `ref_set a (l + l + 1) = x` (ASSUME_TAC o GSYM)
621    \\ ASM_SIMP_TAC bool_ss [INSERT_SUBSET,EMPTY_SUBSET,ref_set_def,IN_UNION]
622    \\ REPEAT STRIP_TAC
623    THEN1 (DISJ1_TAC \\ SIMP_TAC std_ss [GSPECIFICATION]
624           \\ Q.EXISTS_TAC `1` \\ SIMP_TAC std_ss [] \\ DECIDE_TAC)
625    \\ DISJ2_TAC \\ SIMP_TAC std_ss [GSPECIFICATION]
626    THEN1 (Q.EXISTS_TAC `8` \\ SIMP_TAC std_ss [])
627    THEN1 (Q.EXISTS_TAC `7` \\ SIMP_TAC std_ss [])
628    THEN1 (Q.EXISTS_TAC `6` \\ SIMP_TAC std_ss [])
629    THEN1 (Q.EXISTS_TAC `5` \\ SIMP_TAC std_ss [])
630    THEN1 (Q.EXISTS_TAC `4` \\ SIMP_TAC std_ss [])
631    THEN1 (Q.EXISTS_TAC `3` \\ SIMP_TAC std_ss [])
632    THEN1 (Q.EXISTS_TAC `2` \\ SIMP_TAC std_ss [])
633    THEN1 (Q.EXISTS_TAC `1` \\ SIMP_TAC std_ss [])
634    THEN1 (Q.EXISTS_TAC `0` \\ SIMP_TAC (std_ss++WORD_ss) []),
635    FULL_SIMP_TAC bool_ss [IN_INSERT,NOT_IN_EMPTY]
636    \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,word_arith_lemma1,word_arith_lemma2]
637    \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,GSYM ALIGNED_def]
638    \\ REWRITE_TAC [word_sub_def] \\ REPEAT STRIP_TAC
639    \\ MATCH_MP_TAC ALIGNED_ADD \\ ASM_SIMP_TAC bool_ss [] \\ EVAL_TAC]);
640
641val arm_collect_lemma = prove(
642  ``ok_state (i,e,rs,l,u,m) ==>
643    arm_coll_inv (a,x,xs) (i,e,rs,rs2,l,u,m) ==>
644    (cheney_collector (i,e,rs,l,u,m) = (i',e',rs',l',u',m')) ==>
645    (arm_collect (r7,r8,a,x,xs) = (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
646    arm_collect_pre (r7,r8,a,x,xs) /\
647    arm_coll_inv (a,x,xs') (i,e',rs',rs2,l',u',m') /\ (x = x') /\
648    (r3' = ref_addr a i') /\ (r4' = ref_addr a e') /\ (a = a') /\ (l = l')``,
649  STRIP_TAC \\ STRIP_TAC \\ IMP_RES_TAC arm_coll_inv_pre_lemma
650  \\ ONCE_REWRITE_TAC [def7]
651  \\ FULL_SIMP_TAC bool_ss [GSYM AND_IMP_INTRO,arm_coll_inv_def]
652  \\ POP_ASSUM (STRIP_ASSUME_TAC o RW [arm_coll_inv_def])
653  \\ ASM_SIMP_TAC bool_ss [LET_DEF]
654  \\ ASM_SIMP_TAC std_ss [arm_c_init_lemma]
655  \\ Q.ABBREV_TAC `xs1 = (a - 28w =+ (if u then 1w else 0w)) xs`
656  \\ Q.ABBREV_TAC `r4l = a + 8w + (if u then 0w else n2w (8 * l))`
657  \\ Q.ABBREV_TAC `xs2 = (a + 4w =+ r4l + n2w (8 * l)) xs1`
658  \\ `?r43 r53 r63 r73 r83 a3 x3 xs3.
659        arm_move_roots (r4l,r4l + n2w (8 * l),6w,r7,r8,a - 24w,x,xs2) =
660         (r43,r53,r63,r73,r83,a3,x3,xs3)` by METIS_TAC [PAIR]
661  \\ `?r34 r44 r54 r64 r74 r84 x4 xs4. arm_cheney_loop (r4l,r43,r53,r63,r73,r83,x3',xs3) =
662                    (r34,r44,r54,r64,r74,r84,x4,xs4)` by METIS_TAC [PAIR]
663  \\ ASM_SIMP_TAC std_ss [LET_DEF,cheney_collector_def]
664  \\ Q.ABBREV_TAC `b = if ~u then 1 + l else 1`
665  \\ `?ys j2 m2. move_roots ([x1; x2; x3; x4; x5; x6],b,m) = (ys,j2,m2)` by METIS_TAC [PAIR]
666  \\ `?i3 m3. cheney (b,j2,b + l,m2) = (i3,m3)` by METIS_TAC [PAIR]
667  \\ ASM_SIMP_TAC std_ss []
668  \\ ASM_SIMP_TAC std_ss [LET_DEF]
669  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO]
670  \\ REPEAT (MATCH_MP_TAC (METIS_PROVE [] ``P ==> (Q ==> P)``))
671  \\ `roots_in_mem (ZIP (rs,rs2) ++ [(i,0w,F); (e,0w,F)]) (a,a - 24w,xs1)` by
672   (Q.UNABBREV_TAC `xs1`
673    \\ FULL_SIMP_TAC bool_ss [APPEND,roots_in_mem_def,APPLY_UPDATE_THM,ZIP]
674    \\ SIMP_TAC (std_ss++WORD_ss) [WORD_EQ_ADD_LCANCEL,n2w_11,
675      RW [WORD_ADD_0] (Q.SPECL [`v`,`w`,`0w`] WORD_EQ_ADD_LCANCEL)])
676  \\ Q.PAT_X_ASSUM `roots_in_mem ppp (aaa,bbb,xs)` (K ALL_TAC)
677  \\ Q.PAT_X_ASSUM `rs = ppppp` ASSUME_TAC
678  \\ Q.PAT_X_ASSUM `rs2 = ppppp` ASSUME_TAC
679  \\ `roots_in_mem (ZIP (rs,rs2) ++ [(i,0w,F); (b+l,0w,F)]) (a,a - 24w,xs2) /\ a + 4w <+ ref_addr a 1` by
680   (Q.UNABBREV_TAC `xs2` \\ Q.UNABBREV_TAC `b`
681    \\ FULL_SIMP_TAC bool_ss [APPEND,roots_in_mem_def,APPLY_UPDATE_THM,ZIP]
682    \\ FULL_SIMP_TAC (std_ss++WORD_ss) [WORD_EQ_ADD_LCANCEL,n2w_11,
683      RW [WORD_ADD_0] (Q.SPECL [`v`,`w`,`0w`] WORD_EQ_ADD_LCANCEL)]
684    \\ Q.UNABBREV_TAC `r4l` \\ Cases_on `u`
685    \\ SIMP_TAC std_ss [ref_addr_def,DECIDE ``~(m+1 = 0)``,GSYM WORD_ADD_ASSOC,
686         word_add_n2w,LEFT_ADD_DISTRIB,AC ADD_COMM ADD_ASSOC,ref_field_def])
687  \\ IMP_RES_TAC (SIMP_RULE std_ss [LET_DEF] ok_state_IMP_cheney_inv)
688  \\ Q.UNABBREV_TAC `b`
689  \\ Q.ABBREV_TAC `b = if ~u then 1 + l else 1`
690  \\ Q.PAT_X_ASSUM `rs = [x1; x2; x3; x4; x5; x6]` ASSUME_TAC
691  \\ FULL_SIMP_TAC bool_ss []
692  \\ `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
693   (ASM_REWRITE_TAC [ref_cheney_inv_def,CONJ_ASSOC]
694    \\ Q.UNABBREV_TAC `r4l` \\ Q.UNABBREV_TAC `b`  \\ REVERSE STRIP_TAC
695    THEN1 (Cases_on `u` \\ SIMP_TAC std_ss [ref_addr_def,WORD_ADD_0,
696      LEFT_ADD_DISTRIB,GSYM word_add_n2w,WORD_ADD_ASSOC])
697    \\ REVERSE STRIP_TAC
698    THEN1 (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [valid_address_def] \\ DECIDE_TAC)
699    \\ Q.UNABBREV_TAC `xs2`
700    \\ Q.UNABBREV_TAC `xs1`
701    \\ MATCH_MP_TAC (Q.GEN `xs` lemma) \\ ASM_SIMP_TAC bool_ss []
702    \\ Q.EXISTS_TAC `(a - 28w =+ (if u then 1w else 0w)) xs`
703    \\ MATCH_MP_TAC lemma \\ ASM_SIMP_TAC bool_ss [])
704  \\ FULL_SIMP_TAC bool_ss [APPEND]
705  \\ `root_address_ok (a - 24w) 6 x /\ a - 28w IN x /\ a - 32w IN x /\ a + 4w IN x /\
706      ALIGNED (a-32w) /\ ALIGNED (a-28w) /\ ALIGNED (a+4w)` by
707   (REWRITE_TAC [GSYM (EVAL ``(SUC(SUC(SUC(SUC(SUC(SUC 0))))))``),root_address_ok_def]
708    \\ FULL_SIMP_TAC bool_ss [ref_cheney_def,IN_INSERT]
709    \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,word_arith_lemma1,word_arith_lemma2]
710    \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4] \\ METIS_TAC [])
711  \\ `!x1 x2 x3 x4 x5 x6 x7.
712        ZIP ([x1; x2; x3; x4; x5; x6],[y1; y2; y3; y4; y5; y6]) ++ [(i,0w,F); (b+l,0w,F)] =
713        ZIP ([x1; x2; x3; x4; x5; x6; i; b+l],[y1; y2; y3; y4; y5; y6; (0w,F); (0w,F)])` by
714         SIMP_TAC std_ss [ZIP,APPEND]
715  \\ Q.PAT_X_ASSUM `rs2 = ppppp` ASSUME_TAC
716  \\ FULL_SIMP_TAC bool_ss []
717  \\ STRIP_ASSUME_TAC
718    ((UNDISCH_ALL o Q.INST [`f`|->`l+l+1`])
719    (Q.INST [`r5n`|->`r53`,`r6n`|->`r63`,`r7n`|->`r73`,`r8n`|->`r83`,`xn`|->`x3'`]
720    (Q.SPECL [`b`,`m`,`r4l`,`r4l + n2w (8 * l)`,`r7`,`r8`,`xs2`,`a - 24w`,`ys`,`j2`,`m2`]
721    (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`]
722    (SIMP_RULE std_ss [APPEND,GSYM AND_IMP_INTRO,LENGTH,ADD1] (Q.SPECL [`[ii;e]`,`[y1;y2;y3;y4;y5;y6;(0w,F);(0w,F)]`] ref_cheney_move_roots6))))))
723  \\ `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
724   (REWRITE_TAC [ref_cheney_inv_def] \\ REPEAT STRIP_TAC THENL [
725      FULL_SIMP_TAC bool_ss [ref_cheney_inv_def] \\ IMP_RES_TAC cheney_inv_setup
726      \\ FULL_SIMP_TAC bool_ss [cheney_inv_def] \\ METIS_TAC [],
727      FULL_SIMP_TAC bool_ss [ref_cheney_inv_def],
728      MATCH_MP_TAC va_IMP \\ Q.EXISTS_TAC `l+l+1` \\ ASM_SIMP_TAC bool_ss []
729      \\ Q.UNABBREV_TAC `b` \\ Cases_on `u` \\ REWRITE_TAC [] \\ DECIDE_TAC,
730      FULL_SIMP_TAC bool_ss [ref_cheney_inv_def],
731      FULL_SIMP_TAC bool_ss [ref_cheney_inv_def]])
732  \\ `ref_cheney_inv (b,b,j2,j2,b + l,l + l + 1,m2,m2,m,RANGE (b,j2))
733        (a,r4l,r43,x3',xs3,xs3)` by METIS_TAC []
734  \\ (STRIP_ASSUME_TAC o
735      UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o
736      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
737      Q.INST [`xx`|->`m`,`ys`|->`xs3`,`f`|->`l+l+1`,`d`|->`x`])
738      (INST_TYPE [``:'a``|->``:((bool[30] # bool) # bool[30] # bool)``] ref_cheney_loop_th)
739  \\ Q.PAT_X_ASSUM `ref_cheney_inv ppppp (a,r34,r44,x3',xs4,xs3)` (STRIP_ASSUME_TAC o RW [ref_cheney_inv_def])
740  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
741  \\ ASM_SIMP_TAC bool_ss [WORD_SUB_ADD,GSYM ALIGNED_def]
742  \\ SIMP_TAC std_ss [def6,LET_DEF]
743  \\ `?x1' x2' x3' x4' x5' x6'. ys = [x1'; x2'; x3'; x4'; x5'; x6']` by
744   (Cases_on `ys`    \\ FULL_SIMP_TAC std_ss [LENGTH]
745    \\ Cases_on `t`  \\ FULL_SIMP_TAC std_ss [LENGTH]
746    \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH]
747    \\ Cases_on `t`  \\ FULL_SIMP_TAC std_ss [LENGTH]
748    \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH]
749    \\ Cases_on `t`  \\ FULL_SIMP_TAC std_ss [LENGTH]
750    \\ Cases_on `t'`  \\ FULL_SIMP_TAC std_ss [LENGTH,CONS_11,ADD1,GSYM ADD_ASSOC]
751    \\ FULL_SIMP_TAC bool_ss [DECIDE ``~(n + 7 = 6)``])
752  \\ FULL_SIMP_TAC bool_ss [CONS_11,APPEND]
753  \\ `xs4 (a-28w) = xs2 (a-28w)` by METIS_TAC [ref_cheney_def]
754  \\ `xs4 (a-32w) = xs2 (a-32w)` by METIS_TAC [ref_cheney_def]
755  \\ Q.PAT_X_ASSUM ` !i. i <+ a - 24w ==> (xs2 i = xs3 i)` (ASSUME_TAC o GSYM)
756  \\ `~(b = 0) /\ ~(b + l = 0)` by
757    (Q.UNABBREV_TAC `b` \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [LET_DEF,ok_state_def] \\ DECIDE_TAC)
758  \\ `(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,ZIP,ref_field_def]
759  \\ REWRITE_TAC [GSYM CONJ_ASSOC]
760  \\ STRIP_TAC THEN1 METIS_TAC [roots_in_mem_carry_over]
761  \\ REVERSE STRIP_TAC THENL [
762    `(xs4 (a - 32w) = xs3 (a - 32w)) /\ (xs4 (a + 4w) = xs3 (a + 4w)) /\
763     (xs4 (a - 28w) = xs3 (a - 28w))` by METIS_TAC [ref_cheney_def]
764    \\ ASM_SIMP_TAC bool_ss []
765    \\ Q.UNABBREV_TAC `xs2` \\ Q.UNABBREV_TAC `xs1` \\ Cases_on `u`
766    \\ FULL_SIMP_TAC (std_ss++WORD_ss) [APPLY_UPDATE_THM,WORD_EQ_ADD_LCANCEL,n2w_11,
767        RW [WORD_ADD_0] (Q.SPECL [`v`,`w`,`0w`] WORD_EQ_ADD_LCANCEL)],
768    FULL_SIMP_TAC bool_ss [ref_cheney_def,CUT_def]
769    \\ FULL_SIMP_TAC bool_ss [ref_cheney_def,GSYM CUT_def]
770    \\ METIS_TAC [ref_mem_def]]);
771
772val arm_alloc_aux_lemma = prove(
773  ``ok_state (i,e,rs,l,u,m) ==>
774    arm_coll_inv (a,x,xs) (i,e,rs,rs2,l,u,m) ==>
775    (cheney_alloc_gc (i,e,rs,l,u,m) = (i',e',rs',l',u',m')) ==>
776    (arm_alloc_aux (ref_addr a i,ref_addr a e,r5,r6,r7,r8,a,x,xs) =
777                   (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
778    arm_coll_inv (a,x,xs') (i,e',rs',rs2,l',u',m') /\ (a = a') /\ (l = l') /\
779    (r3' = ref_addr a i') /\ (r4' = ref_addr a e') /\ (x = x') /\
780    arm_alloc_aux_pre (ref_addr a i,ref_addr a e,r5,r6,r7,r8,a,x,xs)``,
781  REWRITE_TAC [def8,cheney_alloc_gc_def]
782  \\ STRIP_TAC \\ STRIP_TAC
783  \\ `valid_address a i /\ valid_address a e /\ i <= e` by (Cases_on `u` \\
784    FULL_SIMP_TAC bool_ss [ok_state_def,LET_DEF,arm_coll_inv_def,valid_address_def] \\ DECIDE_TAC)
785  \\ `(ref_addr a i = ref_addr a e) = (i = e)` by METIS_TAC [ref_addr_NEQ]
786  \\ `(i = e) = ~(i < e)` by DECIDE_TAC
787  \\ Cases_on `i < e` \\ ASM_SIMP_TAC bool_ss []
788  THEN1 (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ ASM_SIMP_TAC bool_ss [PAIR_EQ] \\ METIS_TAC [])
789  \\ `?r3i r4i r5i r6i r7i r8i r9i xi xsi. arm_collect (r7,r8,a,x,xs) =
790                         (r3i,r4i,r5i,r6i,r7i,r8i,r9i,xi,xsi)` by METIS_TAC [PAIR]
791  \\ ASM_SIMP_TAC std_ss [LET_DEF] \\ STRIP_TAC
792  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC bool_ss [GSYM AND_IMP_INTRO]
793  \\ REPEAT (MATCH_MP_TAC (METIS_PROVE [] ``P ==> (Q ==> P)``))
794  \\ IMP_RES_TAC arm_collect_lemma
795  \\ FULL_SIMP_TAC bool_ss []
796  \\ METIS_TAC []);
797
798val LO_IMP_ref_addr = prove(
799  ``!b a. b <+ ref_addr a 1 /\ valid_address a i /\ ~(i = 0) ==>
800          ~(ref_addr a i = b) /\ ~(ref_addr a i + 4w = b)``,
801  Cases_word \\ Cases_word
802  \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [ref_addr_def,WORD_LO,w2n_n2w,valid_address_def,word_add_n2w,n2w_11]
803  \\ REPEAT STRIP_TAC
804  \\ `n' + 8 * i + 4 < 4294967296 /\ n' + 8 * i < 4294967296` by DECIDE_TAC
805  \\ `n' + 8 < 4294967296` by DECIDE_TAC
806  \\ FULL_SIMP_TAC std_ss [LESS_MOD] \\ DECIDE_TAC);
807
808val roots_in_mem_UPDATE = prove(
809  ``!p b. valid_address a i /\ ~(i = 0) /\ roots_in_mem p (a,b,xs) ==>
810          roots_in_mem p (a,b,(ref_addr a i =+ y) xs)``,
811  Induct \\ ASM_SIMP_TAC std_ss [roots_in_mem_def,APPLY_UPDATE_THM]
812  \\ REPEAT STRIP_TAC \\ IMP_RES_TAC WORD_LOWER_NOT_EQ \\ IMP_RES_TAC LO_IMP_ref_addr
813  \\ ASM_SIMP_TAC bool_ss []);
814
815val roots_in_mem_UPDATE4 = prove(
816  ``!p b. valid_address a i /\ ~(i = 0) /\ roots_in_mem p (a,b,xs) ==>
817          roots_in_mem p (a,b,(ref_addr a i +4w  =+ y) xs)``,
818  Induct \\ ASM_SIMP_TAC std_ss [roots_in_mem_def,APPLY_UPDATE_THM]
819  \\ REPEAT STRIP_TAC \\ IMP_RES_TAC WORD_LOWER_NOT_EQ \\ IMP_RES_TAC LO_IMP_ref_addr
820  \\ ASM_SIMP_TAC bool_ss []);
821
822val arm_alloc_aux2_lemma = prove(
823  ``ok_state (i,e,rs,l,u,m) /\ ~(i = e) ==>
824    arm_coll_inv (a,x,xs) (q,e,rs,rs2,l,u,m) ==>
825    (cheney_alloc_aux (i,e,rs,l,u,m) (HD rs2,HD (TL rs2)) = (i',e',rs',l',u',m')) ==>
826    (arm_alloc_aux2 (ref_addr a i,ref_addr a e,a,x,xs) = (r3',r4',r8',r9',r10',x',xs')) ==>
827    arm_coll_inv (a,x,xs') (i',e',rs',rs2,l',u',m') /\ (l = l') /\ (x = x') /\ (a = r10') /\
828    arm_alloc_aux2_pre (ref_addr a i,ref_addr a e,a,x,xs)``,
829  STRIP_TAC \\ REWRITE_TAC [def9,cheney_alloc_aux_def]
830  \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss []
831  \\ IMP_RES_TAC arm_coll_inv_pre_lemma
832  \\ `valid_address a i /\ valid_address a e /\ ~(i = 0) /\ ~(e = 0)` by
833      (Cases_on `u` \\ FULL_SIMP_TAC std_ss [valid_address_def,
834         arm_coll_inv_def,ok_state_def,LET_DEF] \\ DECIDE_TAC)
835  \\ ASM_SIMP_TAC bool_ss [ref_addr_NEQ]
836  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
837  \\ SIMP_TAC std_ss [LET_DEF,WORD_ADD_0,GSYM AND_IMP_INTRO]
838  \\ REPEAT (MATCH_MP_TAC (METIS_PROVE [] ``P ==> (Q ==> P)``))
839  \\ FULL_SIMP_TAC bool_ss [CONS_11,arm_coll_inv_def,APPEND,HD,TL]
840  \\ Q.ABBREV_TAC `xs2 = (a - 24w =+ ref_addr a i) xs`
841  \\ Q.ABBREV_TAC `xs1 = (((ref_addr a i + 4w =+ xs (a - 20w))
842             ((ref_addr a i =+ xs (a - 24w)) xs2)))`
843  \\ SIMP_TAC std_ss [word_arith_lemma1]
844  \\ `ref_addr a i + 8w = ref_addr a (i+1)` by
845      FULL_SIMP_TAC std_ss [ref_addr_def,MULT_CLAUSES,GSYM ADD1,
846        GSYM WORD_ADD_ASSOC,word_add_n2w,AC ADD_ASSOC ADD_COMM]
847  \\ ASM_SIMP_TAC std_ss []
848  \\ `a <+ ref_addr a 1 /\ a - 24w <+ ref_addr a 1` by (FULL_SIMP_TAC std_ss [roots_in_mem_def,APPEND,word_arith_lemma1,word_arith_lemma2,ZIP]
849    \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,WORD_ADD_0])
850  \\ `ref_cheney (m,l+l+1) (a,x,xs2,xs2)` by METIS_TAC [lemma]
851  \\ `ref_cheney ((i =+ DATA (x1,x2,y1,y2)) m,l+l+1) (a,x,xs1,xs1)` by
852     (FULL_SIMP_TAC std_ss [ref_cheney_def,APPLY_UPDATE_THM] \\ REPEAT STRIP_TAC
853      \\ Cases_on `i' = i` \\ ASM_SIMP_TAC bool_ss [ref_mem_def,UPDATE_def] THENL [
854          Q.UNABBREV_TAC `xs1`
855          \\ FULL_SIMP_TAC std_ss [roots_in_mem_def,APPLY_UPDATE_THM,word_arith_lemma1,word_arith_lemma2,APPEND,ZIP]
856          \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,WORD_ADD_0]
857          \\ SIMP_TAC (std_ss++WORD_ss) [RW [WORD_ADD_0] (Q.SPECL [`v`,`x`,`0w`] WORD_EQ_ADD_LCANCEL),
858               RW [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL),n2w_11,WORD_EQ_ADD_LCANCEL],
859          Q.UNABBREV_TAC `xs1` \\ Cases_on `m i'` \\ ASM_SIMP_TAC bool_ss [ref_mem_def]
860          \\ `valid_address a i'` by METIS_TAC [va_IMP]
861          THENL [ALL_TAC,Cases_on `p` \\ Cases_on `r` \\ Cases_on `r'`]
862          \\ ASM_SIMP_TAC bool_ss [ref_addr_ADD_NEQ,ref_addr_NEQ,UPDATE_def,ref_mem_def,WORD_EQ_ADD_RCANCEL]
863          \\ METIS_TAC [ref_mem_def]])
864  \\ `ref_cheney ((i =+ DATA (x1,x2,y1,y2)) m,l+l+1)
865      (a,x,(a =+ ref_addr a (i + 1)) xs1,(a =+ ref_addr a (i + 1)) xs1)` by METIS_TAC [lemma]
866  \\ ASM_SIMP_TAC std_ss []
867  \\ Q.ABBREV_TAC `xxx = ZIP ([i; x2; x3; x4; x5; x6],[y1; y2; y3; y4; y5; y6]) ++
868       [(q,0w,F); (e,0w,F)]`
869  \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC]
870  \\ `roots_in_mem xxx (a,a - 24w,xs2)` by
871     (Q.UNABBREV_TAC `xxx` \\ Q.UNABBREV_TAC `xs2`
872      \\ FULL_SIMP_TAC std_ss [roots_in_mem_def,APPLY_UPDATE_THM,word_arith_lemma1,word_arith_lemma2,APPEND,ZIP]
873      \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,WORD_ADD_0]
874      \\ SIMP_TAC (std_ss++WORD_ss) [RW [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL),n2w_11]
875      \\ SIMP_TAC (std_ss++WORD_ss) [RW [WORD_ADD_0] (Q.SPECL [`v`,`x`,`0w`] WORD_EQ_ADD_LCANCEL),
876           RW [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL),n2w_11,WORD_EQ_ADD_LCANCEL]
877      \\ `~(i = 0)` by (FULL_SIMP_TAC std_ss [ok_state_def,LET_DEF] \\ Cases_on `u` \\ DECIDE_TAC)
878      \\ ASM_SIMP_TAC std_ss [ref_field_def])
879  \\ `roots_in_mem xxx (a,a - 24w,xs1)` by
880     (Q.UNABBREV_TAC `xxx` \\ Q.UNABBREV_TAC `xs1`
881      \\ FULL_SIMP_TAC std_ss [roots_in_mem_def,APPLY_UPDATE_THM,word_arith_lemma1,word_arith_lemma2,APPEND,ZIP]
882      \\ IMP_RES_TAC LO_IMP_ref_addr
883      \\ FULL_SIMP_TAC std_ss [roots_in_mem_def,APPLY_UPDATE_THM,word_arith_lemma1,word_arith_lemma2,APPEND,ZIP]
884      \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,WORD_ADD_0]
885      \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,WORD_ADD_0,WORD_EQ_SUB_LADD]
886      \\ FULL_SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL]
887      \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11])
888  \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC]
889  \\ STRIP_TAC THEN1
890    (Q.UNABBREV_TAC `xxx`
891     \\ FULL_SIMP_TAC std_ss [roots_in_mem_def,APPLY_UPDATE_THM,word_arith_lemma1,word_arith_lemma2,APPEND,ZIP]
892     \\ FULL_SIMP_TAC std_ss [WORD_EQ_SUB_RADD,WORD_EQ_SUB_LADD,word_arith_lemma3]
893     \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,WORD_EQ_ADD_CANCEL]
894     \\ ASM_SIMP_TAC std_ss [ref_field_def])
895  \\ NTAC 2 (STRIP_TAC THEN1
896   (ASM_SIMP_TAC std_ss [word_arith_lemma1]
897    \\ Q.UNABBREV_TAC `xs1` \\ Q.UNABBREV_TAC `xs2`
898    \\ IMP_RES_TAC LO_IMP_ref_addr
899    \\ SIMP_TAC bool_ss [UPDATE_def]
900    \\ ASM_SIMP_TAC std_ss [word_arith_lemma1]
901    \\ SIMP_TAC (std_ss++WORD_ss) [RW [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL),n2w_11]
902    \\ SIMP_TAC (std_ss++WORD_ss) [RW [WORD_ADD_0] (Q.SPECL [`v`,`x`,`0w`] WORD_EQ_ADD_LCANCEL),
903         RW [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL),n2w_11,WORD_EQ_ADD_LCANCEL]))
904  \\ `i <= l+l+1` by (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [ok_state_def,LET_DEF] \\ DECIDE_TAC)
905  \\ IMP_RES_TAC ref_cheney_d
906  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
907  \\ FULL_SIMP_TAC std_ss [ref_cheney_def,GSYM ALIGNED_def,INSERT_SUBSET,LENGTH,ALIGNED_ref_addr]
908  \\ REPEAT STRIP_TAC \\ REWRITE_TAC [word_sub_def]
909  \\ REPEAT (MATCH_MP_TAC ALIGNED_ADD) \\ ASM_SIMP_TAC bool_ss [] \\ REPEAT STRIP_TAC
910  \\ REPEAT (MATCH_MP_TAC ALIGNED_ref_addr) \\ ASM_SIMP_TAC bool_ss [] \\ EVAL_TAC);
911
912val not_full_heap_def = Define `
913  not_full_heap (i,e,root,l,u,m) =
914    ~(FST (cheney_alloc_gc (i,e,root,l,u,m)) =
915      FST (SND (cheney_alloc_gc (i,e,root,l,u,m))))`;
916
917val arm_alloc_lemma = prove(
918  ``ok_state (i,e,rs,l,u,m) ==>
919    not_full_heap (i,e,rs,l,u,m) ==>
920    arm_coll_inv (a,x,xs) (i,e,rs,rs3,l,u,m) ==>
921    (cheney_alloc (i,e,rs,l,u,m) (HD rs3,HD (TL rs3)) = (i',e',rs',l',u',m')) ==>
922    (arm_alloc_mem (r5,r6,r7,r8,a,x,xs) = (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
923    arm_coll_inv (a',x,xs') (i',e',rs',rs3,l',u',m') /\ (a' = a) /\ (l' = l) /\ (x = x') /\
924    arm_alloc_mem_pre (r5,r6,r7,r8,a,x,xs)``,
925  REWRITE_TAC [cheney_alloc_def,def10] \\ STRIP_TAC \\ STRIP_TAC \\ STRIP_TAC
926  \\ `~(i = 0) /\ ~(e = 0)` by
927         (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [ok_state_def,LET_DEF] \\ DECIDE_TAC)
928  \\ `(xs a = ref_addr a i) /\ (xs (a+4w) = ref_addr a e)` by
929   (FULL_SIMP_TAC std_ss [arm_coll_inv_def,APPEND,roots_in_mem_def,ZIP]
930    \\ FULL_SIMP_TAC std_ss [arm_coll_inv_def,APPEND,roots_in_mem_def,ZIP]
931    \\ FULL_SIMP_TAC std_ss [roots_in_mem_def,APPLY_UPDATE_THM,word_arith_lemma1,word_arith_lemma2,APPEND]
932    \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,WORD_ADD_0]
933    \\ SIMP_TAC (std_ss++WORD_ss) [RW [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL),n2w_11]
934    \\ ASM_SIMP_TAC std_ss [ref_field_def])
935  \\ `?r3i r4i r5i r6i r7i r8i r9i xi xsi.
936        arm_alloc_aux (ref_addr a i,ref_addr a e,r5,r6,r7,r8,a,x,xs) =
937                      (r3i,r4i,r5i,r6i,r7i,r8i,r9i,xi,xsi)` by METIS_TAC [PAIR]
938  \\ `?r3j r4j r7j r8j r9j xj xsj.
939        arm_alloc_aux2 (r3i,r4i,r9i,xi,xsi) = (r3j,r4j,r7j,r8j,r9j,xj,xsj)` by METIS_TAC [PAIR]
940  \\ `?i2 e2 rs2 l2 u2 m2. cheney_alloc_gc (i,e,rs,l,u,m) = (i2,e2,rs2,l2,u2,m2)` by METIS_TAC [PAIR]
941  \\ ASM_SIMP_TAC std_ss [LET_DEF] \\ STRIP_TAC
942  \\ FULL_SIMP_TAC std_ss [not_full_heap_def]
943  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ ASM_SIMP_TAC std_ss [GSYM CONJ_ASSOC]
944  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ ASM_SIMP_TAC std_ss [GSYM ALIGNED_def]
945  \\ IMP_RES_TAC arm_alloc_aux_lemma
946  \\ `ok_state (i2,e2,rs2,l2,u2,m2)` by METIS_TAC [cheney_collector_spec,cheney_alloc_gc_def]
947  \\ IMP_RES_TAC arm_coll_inv_pre_lemma
948  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ ASM_SIMP_TAC std_ss []
949  \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,NOT_IN_EMPTY,IN_INSERT,EMPTY_SUBSET]
950  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ STRIP_TAC \\ FULL_SIMP_TAC bool_ss []
951  \\ REPEAT (Q.PAT_X_ASSUM `~(i = 0)` ((K ALL_TAC)))
952  \\ IMP_RES_TAC arm_alloc_aux2_lemma \\ ASM_SIMP_TAC std_ss []
953  \\ REVERSE (REPEAT STRIP_TAC) \\ METIS_TAC []);
954
955val field_list_def = Define `
956  (field_list [] (a,r12,m) = T) /\
957  (field_list (x::xs) (a,r12,m) = (m r12 = ref_field a x) /\ field_list xs (a,r12 + 4w,m))`;
958
959val roots_in_mem_IMP_addr_list = prove(
960  ``!p a b xs. roots_in_mem p (a,b,xs) ==> field_list p (a,b,xs)``,
961  Induct \\ ASM_SIMP_TAC std_ss [field_list_def,roots_in_mem_def]);
962
963val ch_mem_def = Define `
964  ch_mem (i,e,rs,rs',l,u,m) (a,x,xs) =
965    ?x1 x2 x3 x4 x5 x6:num y1 y2 y3 y4 y5 y6:(word30 # bool).
966      32 <= w2n a /\ w2n a + 2 * 8 * l + 20 < 2**32 /\
967      ok_state(i,e,rs,l,u,m) /\
968      field_list (ZIP (rs,rs') ++ [(i,(0w,F));(e,(0w,F))]) (a,a-24w,xs) /\
969      (rs = [x1;x2;x3;x4;x5;x6]) /\ (rs' = [y1;y2;y3;y4;y5;y6]) /\
970      ref_cheney (m,l+l+1) (a,x,xs,xs) /\
971      (xs (a-28w) = if u then 0w else 1w) /\
972      (xs (a-32w) = n2w (8 * l)) /\ ~(l = 0)`;
973
974val ch_word_def = Define `
975  ch_word (i,e,rs,rs',l,u,m) (v1,v2,v3,v4,v5,v6,a,x,xs) =
976    ?x1 x2 x3 x4 x5 x6:num y1 y2 y3 y4 y5 y6:(word30 # bool).
977      32 <= w2n a /\ w2n a + 2 * 8 * l + 20 < 2**32 /\
978      ok_state(i,e,rs,l,u,m) /\ ref_cheney (m,l+l+1) (a,x,xs,xs) /\
979      (rs = [x1;x2;x3;x4;x5;x6]) /\ (rs' = [y1;y2;y3;y4;y5;y6]) /\
980      (v1 = ref_field a (x1,y1)) /\ (v2 = ref_field a (x2,y2)) /\ (v3 = ref_field a (x3,y3)) /\
981      (v4 = ref_field a (x4,y4)) /\ (v5 = ref_field a (x5,y5)) /\ (v6 = ref_field a (x6,y6)) /\
982      (xs a = ref_addr a i) /\ (xs (a+4w) = ref_addr a e) /\
983      (xs (a-28w) = if u then 0w else 1w) /\ (xs (a-32w) = n2w (8 * l)) /\ ~(l = 0)`;
984
985val ch_mem_lemma1 = prove(
986  ``!a. n < 2**32 /\ k < 2**32 /\ n <= w2n a /\
987        w2n a + k < 2**32 /\ ~(a = 0w) /\ ~(k = 0) ==> (a:word32 - n2w n <+ a + n2w k)``,
988  Cases_word
989  \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_arith_lemma2,WORD_LO,WORD_LS,w2n_n2w,
990      LESS_MOD,GSYM AND_IMP_INTRO,word_add_n2w,DECIDE ``n <= n' = ~(n' < n:num)``,n2w_11]
991  \\ REPEAT STRIP_TAC \\ `(n' - n) < 4294967296` by DECIDE_TAC
992  \\ ASM_SIMP_TAC bool_ss [LESS_MOD] \\ DECIDE_TAC);
993
994val ch_mem_lemma2 = prove(
995  ``!a. n < 2**32 /\ k < 2**32 /\ n <= w2n a /\ k < w2n a /\
996        ~(a = 0w) /\ (k < n) ==> (a:word32 - n2w n <+ a - n2w k)``,
997  Cases_word
998  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_arith_lemma2,WORD_LO,WORD_LS,w2n_n2w,
999      LESS_MOD,GSYM AND_IMP_INTRO,word_add_n2w,DECIDE ``n < n' ==> ~(n' < n:num)``,n2w_11,
1000      DECIDE ``n <= n' ==> ~(n' < n:num)``]
1001  \\ REPEAT STRIP_TAC
1002  \\ `(n' - n) < 4294967296` by DECIDE_TAC
1003  \\ `(n' - k) < 4294967296` by DECIDE_TAC
1004  \\ ASM_SIMP_TAC bool_ss [LESS_MOD] \\ DECIDE_TAC);
1005
1006val ch_mem_lemma3 = prove(
1007  ``!a. n < 2**32 /\ k < 2**32 /\ w2n a + n < 2**32 /\ w2n a + k < 2**32 /\
1008        ~(a = 0w) /\ ~(k = 0) /\ (n < k) ==> ((a:word32) + n2w n <+ a + n2w k)``,
1009  Cases_word
1010  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_arith_lemma2,WORD_LO,WORD_LS,w2n_n2w,
1011      LESS_MOD,GSYM AND_IMP_INTRO,word_add_n2w,DECIDE ``n < n' ==> ~(n' < n:num)``,n2w_11,
1012      DECIDE ``n <= n' ==> ~(n' < n:num)``]
1013  \\ REPEAT STRIP_TAC \\ DECIDE_TAC);
1014
1015val ch_mem_lemma4 = RW [WORD_ADD_0] (Q.INST [`n`|->`0`] ch_mem_lemma3)
1016
1017val ch_mem_lemma5 = prove(
1018  ``!a. n < 2**32 /\ n <= w2n a /\ ~(a = 0w) /\ ~(n = 0) ==> (a:word32 - n2w n <+ a)``,
1019  Cases_word
1020  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_arith_lemma2,WORD_LO,WORD_LS,w2n_n2w,
1021      LESS_MOD,GSYM AND_IMP_INTRO,word_add_n2w,DECIDE ``n <= n' = ~(n' < n:num)``,n2w_11]
1022  \\ REPEAT STRIP_TAC \\ `(n' - n) < 4294967296` by DECIDE_TAC
1023  \\ ASM_SIMP_TAC bool_ss [LESS_MOD] \\ DECIDE_TAC);
1024
1025val ch_mem_IMP_arm_coll_inv = prove(
1026  ``ch_mem (i,e,rs,rs',l,u,m) (a,x,xs) ==>
1027    ok_state (i,e,rs,l,u,m) /\ arm_coll_inv (a,x,xs) (i,e,rs,rs',l,u,m)``,
1028  REWRITE_TAC [ch_mem_def,arm_coll_inv_def] \\ REPEAT STRIP_TAC
1029  \\ FULL_SIMP_TAC std_ss [CONS_11,APPEND,roots_in_mem_def,field_list_def,valid_address_def,ZIP]
1030  \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,word_arith_lemma2,APPEND]
1031  \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,WORD_ADD_0]
1032  \\ FULL_SIMP_TAC bool_ss [GSYM TIMES2]
1033  \\ FULL_SIMP_TAC bool_ss [GSYM ADD_ASSOC,LEFT_ADD_DISTRIB,MULT_ASSOC]
1034  \\ FULL_SIMP_TAC std_ss [ref_addr_def]
1035  \\ `~(a = 0w)` by (STRIP_TAC \\ FULL_SIMP_TAC (std_ss++WORD_ss) [])
1036  \\ REPEAT STRIP_TAC
1037  \\ REPEAT (MATCH_MP_TAC ch_mem_lemma1 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1038  \\ REPEAT (MATCH_MP_TAC ch_mem_lemma2 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1039  \\ REPEAT (MATCH_MP_TAC ch_mem_lemma3 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1040  \\ REPEAT (MATCH_MP_TAC ch_mem_lemma4 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1041  \\ REPEAT (MATCH_MP_TAC ch_mem_lemma5 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1042  \\ DECIDE_TAC);
1043
1044val ch_mem_cheney_alloc_lemma = prove(
1045  ``ch_mem (i,e,rs,rs2,l,u,m) (a,x,xs) ==>
1046    not_full_heap (i,e,rs,l,u,m) ==>
1047    (cheney_alloc (i,e,rs,l,u,m) (HD rs2, HD (TL rs2)) = (i',e',rs',l',u',m')) ==>
1048    (arm_alloc_mem (r5,r6,r7,r8,a,x,xs) = (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
1049    ch_mem (i',e',rs',rs2,l',u',m') (a',x,xs') /\ (a = a') /\ (l = l') /\ (x = x') /\
1050    arm_alloc_mem_pre (r5,r6,r7,r8,a,x,xs) /\ arm_coll_inv (a,x,xs) (i,e,rs,rs2,l,u,m)``,
1051  NTAC 4 STRIP_TAC \\ IMP_RES_TAC ch_mem_IMP_arm_coll_inv
1052  \\ IMP_RES_TAC arm_alloc_lemma
1053  \\ FULL_SIMP_TAC bool_ss [ch_mem_def,APPEND,ZIP]
1054  \\ `ok_state (i',e',rs',l',u',m')` by METIS_TAC [cheney_alloc_ok]
1055  \\ FULL_SIMP_TAC std_ss [arm_coll_inv_def,CONS_11,ZIP,APPEND]
1056  \\ Q.PAT_X_ASSUM `rs' = xxxxx` (fn th => FULL_SIMP_TAC std_ss [th])
1057  \\ Q.PAT_X_ASSUM `rs2 = xxxxx` (fn th => FULL_SIMP_TAC std_ss [th])
1058  \\ FULL_SIMP_TAC bool_ss [APPEND,roots_in_mem_def,field_list_def,ZIP,CONS_11,HD]
1059  \\ Q.PAT_X_ASSUM `ok_state (i',e',[x1''; x2''; x3''; x4''; x5''; x6''],l',u',m')` MP_TAC
1060  \\ ASM_SIMP_TAC std_ss []);
1061
1062val ch_word_alloc = prove(
1063  ``ch_word (i,e,rs,rs2,l,u,m) (v1,v2,v3,v4,v5,v6,a,x,xs) ==>
1064    not_full_heap (i,e,rs,l,u,m) ==>
1065    (cheney_alloc (i,e,rs,l,u,m) (HD rs2, HD (TL rs2)) = (i',e',rs',l',u',m')) ==>
1066    (arm_alloc (v1,v2,v3,v4,v5,v6,a,x,xs) = (w1,w2,w3,w4,w5,w6,a',x',xs')) ==>
1067    ch_word (i',e',rs',rs2,l',u',m') (w1,w2,w3,w4,w5,w6,a',x',xs') /\ (a = a') /\ (l = l') /\ (x = x') /\
1068    arm_alloc_pre (v1,v2,v3,v4,v5,v6,a,x,xs)``,
1069  SIMP_TAC std_ss [def11,LET_DEF]
1070  \\ Q.ABBREV_TAC `xs1 = (a - 4w =+ v6)
1071      ((a - 8w =+ v5) ((a - 12w =+ v4) ((a - 16w =+ v3)
1072      ((a - 20w =+ v2) ((a - 24w =+ v1) (xs))))))`
1073  \\ `?r3i r4i r5i r6i r7i r8i r9i xi xsi.
1074        arm_alloc_mem (v3,v4,v5,v6,a,x,xs1) = (r3i,r4i,r5i,r6i,r7i,r8i,r9i,xi,xsi)` by METIS_TAC [PAIR]
1075  \\ ASM_SIMP_TAC std_ss [LET_DEF] \\ STRIP_TAC \\ STRIP_TAC \\ STRIP_TAC
1076  \\ REWRITE_TAC [GSYM ALIGNED_def]
1077  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ ASM_SIMP_TAC std_ss []
1078  \\ MATCH_MP_TAC (METIS_PROVE [] ``Q ==> (P ==> Q)``)
1079  \\ sg `ch_mem (i,e,rs,rs2,l,u,m) (a,x,xs1)` THENL [
1080    FULL_SIMP_TAC bool_ss [ch_mem_def,ch_word_def,CONS_11]
1081    \\ `ref_cheney (m,l+l+1) (a,x,xs1,xs1)` by (Q.UNABBREV_TAC `xs1`
1082        \\ Cases_on `a = 0w` THEN1 FULL_SIMP_TAC (std_ss++WORD_ss) [w2n_n2w]
1083        \\ REPEAT (MATCH_MP_TAC (Q.INST [`xs`|->`xs1`] lemma)
1084          \\ REVERSE STRIP_TAC THEN1
1085            (SIMP_TAC std_ss [ref_addr_def] \\ MATCH_MP_TAC ch_mem_lemma1
1086             \\ ASM_SIMP_TAC bool_ss [] \\ DECIDE_TAC))
1087        \\ METIS_TAC [])
1088    \\ ASM_SIMP_TAC bool_ss []
1089    \\ ASM_SIMP_TAC std_ss [field_list_def,ZIP,APPEND,word_arith_lemma1,word_arith_lemma2]
1090    \\ ASM_SIMP_TAC std_ss [field_list_def,ZIP,APPEND,word_arith_lemma3,word_arith_lemma4]
1091    \\ REPEAT STRIP_TAC \\ Q.UNABBREV_TAC `xs1`
1092    \\ ASM_SIMP_TAC (std_ss++WORD_ss) [APPLY_UPDATE_THM,WORD_EQ_ADD_LCANCEL,n2w_11,
1093         RW [WORD_ADD_0] (Q.SPECL [`v`,`x`,`0w`] WORD_EQ_ADD_LCANCEL),
1094         RW [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL)]
1095    \\ `~(i = 0) /\ ~(e = 0)` by
1096          (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [ok_state_def,LET_DEF] \\ DECIDE_TAC)
1097    \\ ASM_SIMP_TAC bool_ss [ref_field_def],
1098    IMP_RES_TAC ch_mem_cheney_alloc_lemma
1099    \\ Q.PAT_X_ASSUM `ch_mem (i,e,rs,rs2,l,u,m) (a,x,xs1)` (K ALL_TAC)
1100    \\ FULL_SIMP_TAC bool_ss [APPEND,ZIP,ch_word_def,ch_mem_def,field_list_def,CONS_11]
1101    \\ FULL_SIMP_TAC bool_ss [APPEND,ZIP,ch_word_def,ch_mem_def,field_list_def,CONS_11]
1102    \\ FULL_SIMP_TAC std_ss [field_list_def,ZIP,APPEND,word_arith_lemma1,word_arith_lemma2]
1103    \\ FULL_SIMP_TAC std_ss [field_list_def,ZIP,APPEND,word_arith_lemma3,word_arith_lemma4]
1104    \\ IMP_RES_TAC arm_coll_inv_pre_lemma
1105    \\ FULL_SIMP_TAC std_ss [WORD_ADD_0,LENGTH,IN_INSERT,NOT_IN_EMPTY,INSERT_SUBSET,ALIGNED_def]
1106    \\ `~(i' = 0) /\ ~(e' = 0)` by
1107          (Cases_on `u'` \\ FULL_SIMP_TAC bool_ss [ok_state_def,LET_DEF] \\ DECIDE_TAC)
1108    \\ ASM_SIMP_TAC bool_ss [ref_field_def]
1109    \\ METIS_TAC []]);
1110
1111val ch_arm_def = Define `
1112  ch_arm (r,h,l) c =
1113    ?i e rs l' u m. ch_inv (MAP FST r,h,l) (i,e,rs,l',u,m) /\ ch_word (i,e,rs,MAP SND r,l',u,m) c`;
1114
1115val ch_arm_alloc = store_thm("ch_arm_alloc",
1116  ``(arm_alloc (v1,v2,v3,v4,v5,v6,a,x,xs) = (w1,w2,w3,w4,w5,w6,a',x',xs')) ==>
1117    CARD (reachables (MAP FST (t1::t2::ts)) (ch_set h)) < l ==>
1118    ch_arm (t1::t2::ts,h,l) (v1,v2,v3,v4,v5,v6,a,x,xs) ==>
1119    ch_arm ((fresh h,SND t1)::t2::ts,h |+ (fresh h,FST t1,FST t2,SND t1, SND t2),l) (w1,w2,w3,w4,w5,w6,a',x,xs') /\
1120    (a' = a) /\ (x' = x) /\ arm_alloc_pre (v1,v2,v3,v4,v5,v6,a,x,xs)``,
1121  REWRITE_TAC [ch_arm_def] \\ STRIP_TAC \\ STRIP_TAC \\ STRIP_TAC
1122  \\ `?i' e' rs' l'' u' m'. cheney_alloc (i,e,rs,l,u,m) (SND t1, SND t2) = (i',e',rs',l'',u',m')` by METIS_TAC [PAIR]
1123  \\ `l' = l` by METIS_TAC [ch_inv_def] \\ FULL_SIMP_TAC bool_ss []
1124  \\ FULL_SIMP_TAC bool_ss [MAP,FST,SND]
1125  \\ `not_full_heap (i,e,rs,l,u,m)` by
1126   (`?i5 e5 c5 l5 u5 m5. cheney_alloc_gc (i,e,rs,l,u,m) = (i5,e5,c5,l5,u5,m5)` by METIS_TAC [PAIR]
1127    \\ IMP_RES_TAC cheney_alloc_gc_spec
1128    \\ FULL_SIMP_TAC std_ss [not_full_heap_def] \\ DECIDE_TAC)
1129  \\ IMP_RES_TAC (REWRITE_RULE [MAP,HD,TL]
1130       (Q.INST [`rs2`|->`MAP SND ((t1:(num#word30#bool))::t2::ts)`] ch_word_alloc))
1131  \\ RES_TAC \\ ASM_SIMP_TAC bool_ss []
1132  \\ Q.EXISTS_TAC `i'` \\ Q.EXISTS_TAC `e'` \\ Q.EXISTS_TAC `rs'` \\ Q.EXISTS_TAC `l''`
1133  \\ Q.EXISTS_TAC `u'` \\ Q.EXISTS_TAC `m'` \\ ASM_SIMP_TAC bool_ss [cheney_alloc_spec,FST]
1134  \\ MATCH_MP_TAC (GEN_ALL (RW [AND_IMP_INTRO] cheney_alloc_spec))
1135  \\ FULL_SIMP_TAC bool_ss [] \\ METIS_TAC []);
1136
1137
1138(* prove tree like representation *)
1139
1140val _ = Hol_datatype `XExp = XDot of XExp => XExp | XVal of word30 | XSym of word30`;
1141val XExp_11 = fetch "-" "XExp_11";
1142val XExp_distinct = fetch "-" "XExp_distinct";
1143
1144val word_tree_def = Define `
1145  (word_tree (XVal w) (a,m) d = (a = ADDR32 w + 2w)) /\
1146  (word_tree (XSym w) (a,m) d = (a = ADDR32 w + 3w)) /\
1147  (word_tree (XDot x y) (a,m) d = a IN d /\ ALIGNED a /\
1148     word_tree x (m a,m) d /\ word_tree y (m (a + 4w),m) d)`;
1149
1150val ch_active_set_def = Define `
1151  ch_active_set (a:word32,i,e) = { a + 8w * n2w j | i <= j /\ j < e }`;
1152
1153val ok_data_def = Define `
1154  ok_data w d = if ALIGNED w then w IN d else ~(ALIGNED (w - 1w))`;
1155
1156val ch_tree_def = Define `
1157  ch_tree (t1,t2,t3,t4,t5,t6,l) (w1,w2,w3,w4,w5,w6,a,dm,m,b,k) =
1158    ?i u.
1159      let v = (if u then 1 + l else 1) in
1160      let d = ch_active_set (a,v,i) in
1161        (b = a + n2w (8 * v)) /\ (k = i - v) /\
1162        32 <= w2n a /\ w2n a + 2 * 8 * l + 20 < 2 ** 32 /\ l <> 0 /\
1163        (m a = a + n2w (8 * i)) /\ ALIGNED a /\ v <= i /\ i <= v + l /\
1164        (m (a + 0x4w) = a + n2w (8 * (v + l))) /\
1165        (m (a - 0x1Cw) = (if u then 0x0w else 0x1w)) /\
1166        (m (a - 0x20w) = n2w (8 * l)) /\
1167        (dm = ref_set a (l + l + 1)) /\
1168        word_tree t1 (w1,m) d /\
1169        word_tree t2 (w2,m) d /\
1170        word_tree t3 (w3,m) d /\
1171        word_tree t4 (w4,m) d /\
1172        word_tree t5 (w5,m) d /\
1173        word_tree t6 (w6,m) d /\
1174        !w. w IN d ==> ok_data (m w) d /\ ok_data (m (w + 4w)) d`;
1175
1176val heap_el_def = Define `
1177  heap_el a w =
1178    if ALIGNED w then (w2n (w - a) DIV 8, (0w, F)) else
1179      (0, (ADDR30 w, ALIGNED (w - 3w)))`;
1180
1181val build_heap_def = Define `
1182  (build_heap (0,i,a,m) = FEMPTY) /\
1183  (build_heap (SUC n,i,a,m) =
1184     let (x1,x2) = heap_el a (m i) in
1185     let (y1,y2) = heap_el a (m (i + 4w)) in
1186       build_heap (n,i + 8w,a,m) |+ (w2n (i - a) DIV 8,x1,y1,x2,y2))`;
1187
1188val build_map_def = Define `
1189  (build_map (0,i,a,m) = \x. EMP) /\
1190  (build_map (SUC n,i,a,m) =
1191     let (x1,x2) = heap_el a (m i) in
1192     let (y1,y2) = heap_el a (m (i + 4w)) in
1193       ((w2n (i - a) DIV 8) =+ DATA (x1,y1,(x2,y2)))
1194       (build_map (n,i + 8w,a,m)))`;
1195
1196val abstract_build_heap = prove(
1197  ``!k a b m.
1198      abstract (I,build_map (k,b,a,m)) =
1199      ch_set (build_heap (k,b,a,m))``,
1200  Induct THENL [
1201     SIMP_TAC std_ss [abstract_def, ch_set_def, build_heap_def,
1202       build_map_def, heap_type_distinct, ch_set_def]
1203     \\ SIMP_TAC std_ss [EXTENSION,GSPECIFICATION, EXISTS_PROD]
1204     \\ SIMP_TAC std_ss [FORALL_PROD,IN_DEF,ch_set_def, FDOM_FEMPTY,
1205          EMPTY_DEF],
1206     FULL_SIMP_TAC std_ss [abstract_def, ch_set_def, build_heap_def,
1207       build_map_def, heap_type_distinct, ch_set_def]
1208     \\ REPEAT STRIP_TAC
1209     \\ Cases_on `heap_el a (m b)`
1210     \\ Cases_on `heap_el a (m (b + 0x4w))`
1211     \\ SIMP_TAC std_ss [LET_DEF]
1212     \\ FULL_SIMP_TAC std_ss [EXTENSION,GSPECIFICATION, EXISTS_PROD]
1213     \\ FULL_SIMP_TAC std_ss [FORALL_PROD,IN_DEF,FDOM_FEMPTY,EMPTY_DEF]
1214     \\ FULL_SIMP_TAC std_ss [ch_set_def,FDOM_FUPDATE,IN_INSERT,
1215          FAPPLY_FUPDATE_THM,APPLY_UPDATE_THM]
1216     \\ REPEAT STRIP_TAC
1217     \\ Cases_on `p_1 = w2n (b - a) DIV 8`
1218     \\ ASM_SIMP_TAC std_ss [heap_type_11]])
1219
1220val FDOM_build_heap = prove(
1221  ``!k a v m. 8 * (v + k) < 2 ** 32 ==>
1222              (FDOM (build_heap (k,a + n2w (8 * v),a,m)) = RANGE (v,v + k))``,
1223  Induct
1224  \\ REWRITE_TAC [build_heap_def,FDOM_FEMPTY,NOT_IN_EMPTY,EXTENSION]
1225  THEN1 (SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC)
1226  \\ REPEAT STRIP_TAC
1227  \\ Cases_on `heap_el a (m (a + n2w (8 * v)))`
1228  \\ Cases_on `heap_el a (m ((a + n2w (8 * v)) + 0x4w))`
1229  \\ SIMP_TAC std_ss [LET_DEF,FDOM_FUPDATE,IN_INSERT,WORD_ADD_SUB2]
1230  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w]
1231  \\ `8 * v < 4294967296` by DECIDE_TAC
1232  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w]
1233  \\ ONCE_REWRITE_TAC [MULT_COMM]
1234  \\ SIMP_TAC std_ss [MULT_DIV]
1235  \\ Cases_on `x = v` \\ ASM_SIMP_TAC std_ss []
1236  THEN1 SIMP_TAC std_ss [IN_DEF,RANGE_def]
1237  \\ REWRITE_TAC [GSYM WORD_ADD_ASSOC,word_add_n2w,GSYM MULT]
1238  \\ `8 * (SUC v + k) < 4294967296` by DECIDE_TAC
1239  \\ RES_TAC \\ FULL_SIMP_TAC std_ss [AC MULT_ASSOC MULT_COMM]
1240  \\ SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC);
1241
1242val IN_ch_active_set = prove(
1243  ``v1 IN ch_active_set (a,v,i) /\ 8 * i < 2 ** 32 ==>
1244    w2n (v1 - a) DIV 8 IN RANGE (v,i)``,
1245  SIMP_TAC std_ss [ch_active_set_def,GSPECIFICATION]
1246  \\ STRIP_TAC
1247  \\ ASM_SIMP_TAC std_ss [WORD_ADD_SUB2,word_mul_n2w]
1248  \\ `8 * j < 4294967296` by DECIDE_TAC
1249  \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w]
1250  \\ ONCE_REWRITE_TAC [MULT_COMM]
1251  \\ SIMP_TAC std_ss [MULT_DIV,IN_DEF,RANGE_def]
1252  \\ DECIDE_TAC);
1253
1254val FEVERY_FUPDATE_IMP = prove(
1255  ``!f P x y. P (x,y) /\ FEVERY P f ==> FEVERY P (f |+ (x,y))``,
1256  recInduct fmap_INDUCT
1257  \\ SIMP_TAC std_ss [FEVERY_DEF,FDOM_FUPDATE,IN_INSERT,
1258       FDOM_FEMPTY,NOT_IN_EMPTY, FAPPLY_FUPDATE_THM]
1259  \\ METIS_TAC []);
1260
1261val build_map_EMP = prove(
1262  ``!k v j. 8 * (v + k) < 2 ** 32 /\ j NOTIN RANGE (v,v + k) ==>
1263            (build_map (k,a + n2w (8 * v),a,m) j = EMP)``,
1264  Induct \\ REWRITE_TAC [build_map_def]
1265  \\ REPEAT STRIP_TAC
1266  \\ Cases_on `heap_el a (m (a + n2w (8 * v)))`
1267  \\ Cases_on `heap_el a (m ((a + n2w (8 * v)) + 0x4w))`
1268  \\ SIMP_TAC std_ss [LET_DEF,FDOM_FUPDATE,IN_INSERT,WORD_ADD_SUB2]
1269  \\ `8 * v < 2**32` by DECIDE_TAC
1270  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w]
1271  \\ ONCE_REWRITE_TAC [MULT_COMM]
1272  \\ SIMP_TAC std_ss [MULT_DIV,APPLY_UPDATE_THM]
1273  \\ Cases_on `v = j`
1274  THEN1 (FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC)
1275  \\ ASM_SIMP_TAC std_ss []
1276  \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w,GSYM MULT]
1277  \\ ONCE_REWRITE_TAC [MULT_COMM]
1278  \\ Q.PAT_X_ASSUM `!v. bbb` MATCH_MP_TAC
1279  \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def,MULT_CLAUSES]
1280  \\ DECIDE_TAC);
1281
1282val build_map_DATA = prove(
1283  ``!k i a m j v.
1284      8 * (v + k) < 2 ** 32 /\ j IN RANGE (v,v + k) ==>
1285      (build_map (k,a + n2w (8 * v),a,m) j =
1286        let (x1,x2) = heap_el a (m (a + n2w (8 * j))) in
1287        let (y1,y2) = heap_el a (m (a + n2w (8 * j) + 0x4w)) in
1288          DATA (x1,y1,x2,y2))``,
1289  Induct \\ REWRITE_TAC [build_map_def]
1290  \\ REPEAT STRIP_TAC
1291  THEN1 (FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ `F` by DECIDE_TAC)
1292  \\ Cases_on `heap_el a (m (a + n2w (8 * v)))`
1293  \\ Cases_on `heap_el a (m (a + n2w (8 * v) + 4w))`
1294  \\ FULL_SIMP_TAC std_ss [LET_DEF,heap_type_distinct]
1295  \\ `8 * v < 4294967296` by DECIDE_TAC
1296  \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,WORD_ADD_SUB2]
1297  \\ Cases_on `v = j`
1298  \\ FULL_SIMP_TAC std_ss [RW1 [MULT_COMM] MULT_DIV,APPLY_UPDATE_THM]
1299  \\ REWRITE_TAC [GSYM WORD_ADD_ASSOC,word_add_n2w, RW1 [MULT_COMM] (GSYM MULT)]
1300  \\ REWRITE_TAC [WORD_ADD_ASSOC,GSYM word_add_n2w]
1301  \\ Q.PAT_X_ASSUM `!bb. bbb` MATCH_MP_TAC
1302  \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC);
1303
1304val build_heap_DATA = prove(
1305  ``!k i a m j v.
1306      8 * (v + k) < 2 ** 32 /\ j IN RANGE (v,v + k) ==>
1307      j IN FDOM (build_heap (k,a + n2w (8 * v),a,m)) /\
1308      (build_heap (k,a + n2w (8 * v),a,m) ' j =
1309        let (x1,x2) = heap_el a (m (a + n2w (8 * j))) in
1310        let (y1,y2) = heap_el a (m (a + n2w (8 * j) + 0x4w)) in
1311          (x1,y1,x2,y2))``,
1312  Induct \\ REWRITE_TAC [build_heap_def]
1313  THEN1 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ `F` by DECIDE_TAC)
1314  \\ NTAC 5 STRIP_TAC
1315  \\ Cases_on `heap_el a (m (a + n2w (8 * v)))`
1316  \\ Cases_on `heap_el a (m (a + n2w (8 * v) + 4w))`
1317  \\ FULL_SIMP_TAC std_ss [LET_DEF,heap_type_distinct]
1318  \\ `8 * v < 4294967296` by DECIDE_TAC
1319  \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,WORD_ADD_SUB2]
1320  \\ Cases_on `v = j`
1321  \\ FULL_SIMP_TAC std_ss [RW1 [MULT_COMM] MULT_DIV,
1322       FAPPLY_FUPDATE_THM,FDOM_FUPDATE,IN_INSERT]
1323  \\ REWRITE_TAC [GSYM WORD_ADD_ASSOC,word_add_n2w, RW1 [MULT_COMM] (GSYM MULT)]
1324  \\ REWRITE_TAC [WORD_ADD_ASSOC,GSYM word_add_n2w]
1325  \\ Q.PAT_X_ASSUM `!bb. bbb` MATCH_MP_TAC
1326  \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC);
1327
1328val NOT_ALIGNED_LEMMA = prove(
1329  ``!c. ~ALIGNED (ADDR32 c + 0x1w) /\ ~ALIGNED (ADDR32 c + 0x2w) /\
1330        ~ALIGNED (ADDR32 c + 0x3w) /\ ~ALIGNED (ADDR32 c - 0x1w) /\
1331        ~ALIGNED (ADDR32 c - 0x2w) /\ ~ALIGNED (ADDR32 c - 0x3w)``,
1332  METIS_TAC [ALIGNED_ADDR32,NOT_ALIGNED,WORD_ADD_SUB,WORD_SUB_ADD]);
1333
1334val IN_ch_active_set2 = prove(
1335  ``!v a. v IN ch_active_set (a,b,j) /\ 8 * j < 2 ** 32 /\ b <> 0 ==>
1336          ?i. i <> 0 /\ 8 * i < 2 ** 32 /\ (8w * n2w i = v - a)``,
1337  Cases_word \\ Cases_word
1338  \\ SIMP_TAC std_ss [ch_active_set_def,GSPECIFICATION,
1339       WORD_EQ_SUB_LADD,word_mul_n2w,word_add_n2w]
1340  \\ REPEAT STRIP_TAC
1341  \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `j'`
1342  \\ SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC]
1343  \\ DECIDE_TAC);
1344
1345val ok_data_IMP_ref_field_heap_el = prove(
1346  ``!j b a. 8 * j < 2 ** 32 /\ b <> 0 /\
1347            ok_data v (ch_active_set (a,b,j)) ==>
1348            (ref_field a (heap_el a v) = v)``,
1349  Cases_on `ALIGNED v`
1350  \\ ASM_SIMP_TAC std_ss [ok_data_def,ref_field_def,heap_el_def]
1351  \\ REWRITE_TAC [GSYM (EVAL ``(2**32):num``)]
1352  \\ REPEAT STRIP_TAC
1353  \\ IMP_RES_TAC (IN_ch_active_set2)
1354  \\ REPEAT (Q.PAT_X_ASSUM `!v.bbb` (K ALL_TAC)) THENL [
1355    Q.PAT_X_ASSUM `0x8w * n2w i = v - a` (ASSUME_TAC o GSYM)
1356    \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,w2n_n2w]
1357    \\ ASM_SIMP_TAC std_ss [RW1 [MULT_COMM] MULT_DIV]
1358    \\ FULL_SIMP_TAC std_ss [WORD_EQ_SUB_RADD]
1359    \\ SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC,ref_addr_def],
1360    STRIP_ASSUME_TAC (Q.SPEC `v` EXISTS_ADDR32)
1361    \\ FULL_SIMP_TAC std_ss [WORD_ADD_0,ALIGNED_ADDR32,WORD_ADD_SUB,
1362          ADDR30_ADDR32,word_arith_lemma4,NOT_ALIGNED_LEMMA]]);
1363
1364val ref_field_heap_el = prove(
1365  ``!t j b a. 8 * j < 2 ** 32 /\ b <> 0 /\
1366              word_tree t (v,m) (ch_active_set (a,b,j)) ==>
1367              (ref_field a (heap_el a v) = v)``,
1368  REVERSE Cases
1369  \\ ASM_SIMP_TAC std_ss [word_tree_def,heap_el_def,NOT_ALIGNED_LEMMA,
1370       ref_field_def,ADDR30_ADDR32,word_arith_lemma4,WORD_ADD_0,
1371       ALIGNED_ADDR32,ref_addr_def]
1372  \\ REWRITE_TAC [GSYM (EVAL ``(2**32):num``)]
1373  \\ REPEAT STRIP_TAC
1374  \\ IMP_RES_TAC (IN_ch_active_set2)
1375  \\ REPEAT (Q.PAT_X_ASSUM `!v.bbb` (K ALL_TAC))
1376  \\ Q.PAT_X_ASSUM `0x8w * n2w i = v - a` (ASSUME_TAC o GSYM)
1377  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,w2n_n2w]
1378  \\ ASM_SIMP_TAC std_ss [RW1 [MULT_COMM] MULT_DIV]
1379  \\ FULL_SIMP_TAC std_ss [WORD_EQ_SUB_RADD]
1380  \\ SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC]);
1381
1382val IN_RANGE_IMP = prove(
1383  ``!i j v a. j IN RANGE (v,i) ==> a + 8w * n2w j IN ch_active_set (a,v,i)``,
1384  SIMP_TAC std_ss [ch_active_set_def,GSPECIFICATION]
1385  \\ SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ METIS_TAC []);
1386
1387val ZERO_OR_IN_RANGE = prove(
1388  ``!q r w a v i. 8 * i < 4294967296 /\
1389    ok_data w (ch_active_set (a,v,i)) /\
1390    (heap_el a w = (q,r)) ==>
1391    (q = 0) \/ q IN RANGE (v,i)``,
1392  STRIP_TAC
1393  \\ Cases_on `q = 0` \\ ASM_SIMP_TAC std_ss []
1394  \\ REPEAT STRIP_TAC
1395  \\ Cases_on `ALIGNED w`
1396  \\ FULL_SIMP_TAC std_ss [word_tree_def, heap_el_def, word_mul_n2w, ok_data_def]
1397  \\ Q.PAT_X_ASSUM `xxx = q` (ASSUME_TAC o GSYM)
1398  \\ FULL_SIMP_TAC std_ss []
1399  \\ MATCH_MP_TAC IN_ch_active_set
1400  \\ FULL_SIMP_TAC std_ss []);
1401
1402val ch_tree_IMP_ch_arm = prove(
1403  ``ch_tree (t1,t2,t3,t4,t5,t6,l) (v1,v2,v3,v4,v5,v6,a,dm,m,b,k) ==>
1404    ch_arm ([heap_el a v1; heap_el a v2; heap_el a v3;
1405             heap_el a v4; heap_el a v5; heap_el a v6],
1406            build_heap (k,b,a,m),l)
1407           (v1,v2,v3,v4,v5,v6,a,dm,m)``,
1408  REPEAT STRIP_TAC
1409  \\ FULL_SIMP_TAC std_ss [ch_arm_def,ch_tree_def,LET_DEF]
1410  \\ Q.ABBREV_TAC `v = if u then 1 + l else 1`
1411  \\ Q.EXISTS_TAC `i`
1412  \\ Q.EXISTS_TAC `v + l`
1413  \\ Q.EXISTS_TAC `(MAP FST [heap_el a v1; heap_el a v2; heap_el a v3;
1414             heap_el a v4; heap_el a v5; heap_el a v6])`
1415  \\ Q.EXISTS_TAC `l`
1416  \\ Q.EXISTS_TAC `u`
1417  \\ Q.EXISTS_TAC `build_map (k, b, a, m)`
1418  \\ REWRITE_TAC [ch_inv_def]
1419  \\ `ok_state (i,v + l,
1420       [FST (heap_el a v1); FST (heap_el a v2); FST (heap_el a v3);
1421        FST (heap_el a v4); FST (heap_el a v5); FST (heap_el a v6)],l,u,
1422          build_map (k,b,a,m))` by
1423   (SIMP_TAC std_ss [ok_state_def,LET_DEF]
1424    \\ Q.UNABBREV_TAC `v`
1425    \\ Q.ABBREV_TAC `v = if u then 1 + l else 1`
1426    \\ ASM_SIMP_TAC std_ss [MAP,MEM]
1427    \\ STRIP_TAC THEN1
1428     (`!c. ~ALIGNED (ADDR32 c + 0x3w) /\ ~ALIGNED (ADDR32 c + 0x2w)` by
1429            METIS_TAC [ALIGNED_ADDR32,NOT_ALIGNED]
1430      \\ `8 * i < 4294967296` by
1431        (Cases_on `u` \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def]
1432         \\ Q.UNABBREV_TAC `v` \\ DECIDE_TAC)
1433      \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC
1434      \\ FULL_SIMP_TAC std_ss []
1435      THENL [
1436        Cases_on `t1`,
1437        Cases_on `t2`,
1438        Cases_on `t3`,
1439        Cases_on `t4`,
1440        Cases_on `t5`,
1441        Cases_on `t6`]
1442      \\ FULL_SIMP_TAC std_ss [word_tree_def,heap_el_def]
1443      \\ REPEAT STRIP_TAC
1444      \\ MATCH_MP_TAC IN_ch_active_set
1445      \\ ASM_SIMP_TAC std_ss [])
1446    \\ STRIP_TAC THEN1
1447     (REPEAT STRIP_TAC
1448      \\ MATCH_MP_TAC build_map_EMP
1449      \\ `v + (i - v) = i` by DECIDE_TAC
1450      \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def]
1451      \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def]
1452      \\ Q.UNABBREV_TAC `v` \\ DECIDE_TAC)
1453    \\ REPEAT STRIP_TAC
1454    \\ IMP_RES_TAC IN_RANGE_IMP
1455    \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `a`)
1456    \\ `8 * (v + (i - v)) < 2 ** 32 /\ k' IN RANGE (v,v + (i - v))` by
1457     (`v + (i - v) = i` by DECIDE_TAC
1458      \\ Q.UNABBREV_TAC `v` \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss []
1459      \\ DECIDE_TAC)
1460    \\ IMP_RES_TAC build_map_DATA
1461    \\ ASM_SIMP_TAC std_ss [EXISTS_PROD]
1462    \\ POP_ASSUM (K ALL_TAC)
1463    \\ Cases_on `heap_el a (m (a + n2w (8 * k')))`
1464    \\ Cases_on `heap_el a (m (a + n2w (8 * k') + 4w))`
1465    \\ ASM_SIMP_TAC std_ss [LET_DEF,heap_type_11]
1466    \\ Q.EXISTS_TAC `FST r`
1467    \\ Q.EXISTS_TAC `SND r`
1468    \\ Q.EXISTS_TAC `FST r'`
1469    \\ Q.EXISTS_TAC `SND r'`
1470    \\ SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,SUBSET0_DEF,IN_INSERT]
1471    \\ RES_TAC
1472    \\ `v + (i - v) = i` by DECIDE_TAC
1473    \\ FULL_SIMP_TAC std_ss [word_tree_def,word_mul_n2w]
1474    \\ STRIP_TAC \\ MATCH_MP_TAC ZERO_OR_IN_RANGE \\ METIS_TAC [])
1475  \\ REPEAT STRIP_TAC THEN1 (POP_ASSUM MP_TAC  \\ ASM_REWRITE_TAC [MAP])
1476  THEN1
1477   (SIMP_TAC std_ss [ok_abs_def]
1478    \\ `v + (i - v) = i` by DECIDE_TAC
1479    \\ `FDOM (build_heap (i - v,a + n2w (8 * v),a,m)) = RANGE (v,v + (i - v))` by
1480     (MATCH_MP_TAC FDOM_build_heap
1481      \\ ASM_SIMP_TAC std_ss []
1482      \\ Cases_on `u` \\ Q.UNABBREV_TAC `v`
1483      \\ FULL_SIMP_TAC std_ss []
1484      \\ DECIDE_TAC)
1485    \\ ASM_SIMP_TAC std_ss []
1486    \\ STRIP_TAC THEN1
1487     (Cases_on `u` \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def]
1488      \\ Q.UNABBREV_TAC `v` \\ DECIDE_TAC)
1489    \\ REVERSE STRIP_TAC THEN1
1490     (SIMP_TAC std_ss [MAP,MEM]
1491      \\ `!c. ~ALIGNED (ADDR32 c + 0x3w) /\ ~ALIGNED (ADDR32 c + 0x2w)` by
1492            METIS_TAC [ALIGNED_ADDR32,NOT_ALIGNED]
1493      \\ `8 * i < 4294967296` by
1494        (Cases_on `u` \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def]
1495         \\ Q.UNABBREV_TAC `v` \\ DECIDE_TAC)
1496      \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC
1497      \\ FULL_SIMP_TAC std_ss []
1498      THENL [
1499        Cases_on `t1`,
1500        Cases_on `t2`,
1501        Cases_on `t3`,
1502        Cases_on `t4`,
1503        Cases_on `t5`,
1504        Cases_on `t6`]
1505      \\ FULL_SIMP_TAC std_ss [word_tree_def,heap_el_def]
1506      \\ REPEAT STRIP_TAC
1507      \\ MATCH_MP_TAC IN_ch_active_set
1508      \\ ASM_SIMP_TAC std_ss [])
1509    \\ ASM_SIMP_TAC std_ss [FEVERY_DEF]
1510    \\ REPEAT STRIP_TAC
1511    \\ IMP_RES_TAC IN_RANGE_IMP
1512    \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `a`)
1513    \\ `8 * (v + (i - v)) < 2 ** 32 /\ x IN RANGE (v,v + (i - v))` by
1514     (Q.UNABBREV_TAC `v` \\ Cases_on `u`
1515      \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1516    \\ IMP_RES_TAC build_heap_DATA
1517    \\ ASM_SIMP_TAC std_ss []
1518    \\ POP_ASSUM (K ALL_TAC)
1519    \\ Cases_on `heap_el a (m (a + n2w (8 * x)))`
1520    \\ Cases_on `heap_el a (m (a + n2w (8 * x) + 4w))`
1521    \\ ASM_SIMP_TAC std_ss [LET_DEF,heap_type_11]
1522    \\ SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,SUBSET0_DEF,IN_INSERT]
1523    \\ FULL_SIMP_TAC std_ss [word_tree_def,word_mul_n2w]
1524    \\ RES_TAC \\ STRIP_TAC \\ MATCH_MP_TAC ZERO_OR_IN_RANGE
1525    \\ Q.PAT_X_ASSUM `v + (i - v) = i` ASSUME_TAC
1526    \\ FULL_SIMP_TAC std_ss []
1527    \\ METIS_TAC [])
1528  THEN1
1529   (Q.EXISTS_TAC `I`
1530    \\ SIMP_TAC std_ss [MAP,bijection_def,ONE_ONE_DEF,ONTO_DEF]
1531    \\ ASM_SIMP_TAC std_ss [abstract_build_heap,SUBSET_REFL]
1532    \\ SIMP_TAC std_ss [SUBSET_DEF,IN_DEF,reachables_def,FORALL_PROD])
1533  THEN
1534   (ASM_SIMP_TAC std_ss [ch_word_def,MAP,CONS_11,ref_addr_def]
1535    \\ POP_ASSUM MP_TAC \\ ASM_SIMP_TAC std_ss [MAP]
1536    \\ STRIP_TAC \\ POP_ASSUM (K ALL_TAC)
1537    \\ REVERSE STRIP_TAC THEN1
1538     (`8 * i < 2 ** 32 /\ v <> 0` by
1539        (Cases_on `u` \\ Q.UNABBREV_TAC `v`
1540         \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1541      \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ REPEAT STRIP_TAC
1542      \\ MATCH_MP_TAC ref_field_heap_el
1543      THENL [Q.EXISTS_TAC `t1`,
1544             Q.EXISTS_TAC `t2`,
1545             Q.EXISTS_TAC `t3`,
1546             Q.EXISTS_TAC `t4`,
1547             Q.EXISTS_TAC `t5`,
1548             Q.EXISTS_TAC `t6`]
1549      \\ Q.EXISTS_TAC `i`
1550      \\ Q.EXISTS_TAC `v`
1551      \\ ASM_SIMP_TAC bool_ss [])
1552    \\ ASM_SIMP_TAC std_ss [ref_cheney_def,ALIGNED_INTRO]
1553    \\ STRIP_TAC THEN1
1554       (REPEAT (POP_ASSUM MP_TAC)
1555        \\ Q.SPEC_TAC (`a`,`a`)
1556        \\ Cases_word
1557        \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,n2w_11]
1558        \\ REPEAT STRIP_TAC
1559        \\ DECIDE_TAC)
1560    \\ REVERSE (REPEAT STRIP_TAC)
1561    THEN1 (FULL_SIMP_TAC std_ss [valid_address_def] \\ DECIDE_TAC)
1562    THEN1 (MATCH_MP_TAC build_map_EMP
1563           \\ Cases_on `u` \\ Q.UNABBREV_TAC `v`
1564           \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC)
1565    \\ `~(v = 0) /\ 8 * (v + (i - v)) < 2 ** 32 /\ 8 * i < 2 ** 32` by
1566     (Cases_on `u` \\ Q.UNABBREV_TAC `v`
1567      \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC)
1568    \\ REVERSE (Cases_on `i' IN RANGE (v,v + (i - v))`)
1569    THEN1 (IMP_RES_TAC build_map_EMP \\ ASM_SIMP_TAC std_ss [ref_mem_def])
1570    \\ IMP_RES_TAC build_map_DATA
1571    \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`m`,`a`])
1572    \\ Cases_on `heap_el a (m (a + n2w (8 * i')))`
1573    \\ Cases_on `heap_el a (m (a + n2w (8 * i') + 4w))`
1574    \\ FULL_SIMP_TAC std_ss [LET_DEF,ref_mem_def]
1575    \\ POP_ASSUM (fn th => REWRITE_TAC [GSYM th])
1576    \\ POP_ASSUM (fn th => REWRITE_TAC [GSYM th])
1577    \\ IMP_RES_TAC IN_RANGE_IMP
1578    \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `a`)
1579    \\ `v + (i - v) = i` by DECIDE_TAC
1580    \\ FULL_SIMP_TAC std_ss [ref_addr_def,word_mul_n2w]
1581    \\ RES_TAC \\ FULL_SIMP_TAC std_ss [word_tree_def]
1582    \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ STRIP_TAC
1583    \\ SIMP_TAC std_ss [ref_addr_def]
1584    \\ MATCH_MP_TAC ok_data_IMP_ref_field_heap_el
1585    \\ SIMP_TAC std_ss [] \\ METIS_TAC []));
1586
1587val XSIZE_def = Define `
1588  (XSIZE (XDot x y) = SUC (XSIZE x + XSIZE y)) /\
1589  (XSIZE (XVal w) = 0) /\
1590  (XSIZE (XSym s) = 0)`;
1591
1592val XDEPTH_def = Define `
1593  (XDEPTH (XDot x y) = SUC (MAX (XDEPTH x) (XDEPTH y))) /\
1594  (XDEPTH (XVal w) = 0) /\
1595  (XDEPTH (XSym s) = 0)`;
1596
1597val CARD_LESS_EQ_XSIZE = prove(
1598  ``!t1 v1 a m. ch_tree (t1,t2,t3,t4,t5,t6,l) (v1,v2,v3,v4,v5,v6,a,dm,m,b,k) ==>
1599                CARD (reachables [FST (heap_el a v1)] (ch_set (build_heap (k,b,a,m)))) <= XSIZE t1``,
1600  Induct THEN1
1601   (SIMP_TAC std_ss [word_tree_def,XSIZE_def,ADD1]
1602    \\ REPEAT STRIP_TAC \\ RES_TAC
1603    \\ Cases_on `heap_el a (m v1)`
1604    \\ Cases_on `heap_el a (m (v1+4w))`
1605    \\ `(build_heap (k,b,a,m)) ' (FST (heap_el a v1)) = (q,q',r,r')` by
1606     (REPEAT (Q.PAT_X_ASSUM `!xx.yy` (K ALL_TAC))
1607      \\ FULL_SIMP_TAC std_ss [ch_tree_def,LET_DEF]
1608      \\ Q.ABBREV_TAC `v = if u then 1 + l else 1`
1609      \\ `8 * (v + (i - v)) < 2 ** 32 /\ v <> 0` by
1610       (Cases_on `u` \\ Q.UNABBREV_TAC `v`
1611        \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1612      \\ `v + (i - v) = i` by DECIDE_TAC
1613      \\ FULL_SIMP_TAC bool_ss [word_tree_def]
1614      \\ ASM_SIMP_TAC std_ss [heap_el_def]
1615      \\ IMP_RES_TAC IN_ch_active_set
1616      \\ `8 * (v + (i - v)) < 2 ** 32 /\
1617          w2n (v1 - a) DIV 8 IN RANGE (v,v + (i - v))` by
1618            FULL_SIMP_TAC std_ss []
1619      \\ IMP_RES_TAC build_heap_DATA
1620      \\ ASM_SIMP_TAC std_ss []
1621      \\ POP_ASSUM (K ALL_TAC)
1622      \\ IMP_RES_TAC (RW [WORD_EQ_SUB_LADD] IN_ch_active_set2)
1623      \\ REPEAT (Q.PAT_X_ASSUM `!xx.yy` (K ALL_TAC))
1624      \\ Q.PAT_X_ASSUM `0x8w * n2w i' + a = v1` (ASSUME_TAC o GSYM)
1625      \\ FULL_SIMP_TAC std_ss [word_mul_n2w,WORD_ADD_SUB]
1626      \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w]
1627      \\ ASM_SIMP_TAC std_ss [RW1 [MULT_COMM] MULT_DIV]
1628      \\ FULL_SIMP_TAC std_ss [LET_DEF,AC WORD_ADD_ASSOC WORD_ADD_COMM])
1629    \\ `(FST (heap_el a v1)) IN FDOM (build_heap (k,b,a,m))` by
1630     (REPEAT (Q.PAT_X_ASSUM `!xx.yy` (K ALL_TAC))
1631      \\ FULL_SIMP_TAC std_ss [ch_tree_def,LET_DEF]
1632      \\ Q.ABBREV_TAC `v = if u then 1 + l else 1`
1633      \\ `8 * (v + (i - v)) < 2 ** 32 /\ v <> 0` by
1634       (Cases_on `u` \\ Q.UNABBREV_TAC `v`
1635        \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1636      \\ IMP_RES_TAC FDOM_build_heap
1637      \\ FULL_SIMP_TAC std_ss [word_tree_def,heap_el_def]
1638      \\ MATCH_MP_TAC IN_ch_active_set
1639      \\ `v + (i - v) = i` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss []
1640      \\ Cases_on `u` \\ Q.UNABBREV_TAC `v`
1641      \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1642    \\ IMP_RES_TAC reachables_NEXT \\ RES_TAC
1643    \\ ASM_SIMP_TAC std_ss []
1644    \\ `ch_tree (t1,t2,t3,t4,t5,t6,l) (m v1,v2,v3,v4,v5,v6,a,dm,m,b,k) /\
1645        ch_tree (t1',t2,t3,t4,t5,t6,l) (m (v1 + 4w),v2,v3,v4,v5,v6,a,dm,m,b,k)` by
1646     (REPEAT (Q.PAT_X_ASSUM `!xx.yy` (K ALL_TAC))
1647      \\ FULL_SIMP_TAC std_ss [LET_DEF,ch_tree_def,word_tree_def]
1648      \\ STRIP_TAC \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u`
1649      \\ Q.ABBREV_TAC `v = if u then 1 + l else 1`
1650      \\ ASM_SIMP_TAC std_ss [])
1651    \\ RES_TAC
1652    \\ REPEAT (Q.PAT_X_ASSUM `!xx.yy` (K ALL_TAC))
1653    \\ Q.PAT_X_ASSUM `ch_tree (t1,t2,t3,t4,t5,t6,l) (m v1,v2,v3,v4,v5,v6,a,dm,m,b,k)` (K ALL_TAC)
1654    \\ Q.PAT_X_ASSUM `ch_tree (t1',t2,t3,t4,t5,t6,l) (m (v1 + 4w),v2,v3,v4,v5,v6,a,dm,m,b,k)` (K ALL_TAC)
1655    \\ Q.PAT_X_ASSUM `heap_el a (m v1) = (q,r)` (fn th => FULL_SIMP_TAC std_ss [th])
1656    \\ Q.PAT_X_ASSUM `heap_el a (m (v1+4w)) = bbb` (fn th => FULL_SIMP_TAC std_ss [th])
1657    \\ MATCH_MP_TAC LESS_EQ_TRANS
1658    \\ Q.EXISTS_TAC `CARD (reachables [q] (ch_set (build_heap (k,b,a,m)))) +
1659                     CARD (reachables [q'] (ch_set (build_heap (k,b,a,m)))) + 1`
1660    \\ REVERSE STRIP_TAC THEN1 DECIDE_TAC
1661    \\ MATCH_MP_TAC LESS_EQ_TRANS
1662    \\ Q.EXISTS_TAC `CARD (reachables [q] (ch_set (build_heap (k,b,a,m))) UNION
1663                           reachables [q'] (ch_set (build_heap (k,b,a,m)))) + 1`
1664    \\ ASM_SIMP_TAC std_ss [GSYM CARD_UNION,FINITE_reachables]
1665    \\ `1 = CARD {(FST (heap_el a v1),q,q',r,r')}` by METIS_TAC [CARD_SING]
1666    \\ ASM_SIMP_TAC std_ss [GSYM CARD_UNION,FINITE_reachables,FINITE_INSERT,FINITE_UNION,FINITE_EMPTY]
1667    \\ SIMP_TAC std_ss [AC UNION_ASSOC UNION_COMM])
1668  \\ FULL_SIMP_TAC std_ss [ch_tree_def,LET_DEF]
1669  \\ SIMP_TAC bool_ss [XSIZE_def,DECIDE ``n <= 0 = (n = 0)``,CARD_EQ_0,FINITE_reachables]
1670  \\ SIMP_TAC std_ss [EXTENSION,IN_DEF,EMPTY_DEF]
1671  \\ REPEAT STRIP_TAC \\ Cases_on `x` \\ Cases_on `r` \\ Cases_on `r'`
1672  \\ FULL_SIMP_TAC std_ss [reachables_def,reachable_def,IN_DEF,ch_set_def,MEM]
1673  \\ REPEAT (Cases_on `p`)
1674  \\ POP_ASSUM MP_TAC
1675  \\ FULL_SIMP_TAC std_ss [APPEND,PATH_def,ch_set_def,IN_DEF,word_tree_def,
1676       heap_el_def,NOT_ALIGNED_LEMMA]
1677  \\ `~(FDOM (build_heap (k,b,a,m)) 0)` by
1678   (ASM_SIMP_TAC std_ss []
1679    \\ Q.ABBREV_TAC `v = if u then 1 + l else 1`
1680    \\ `8 * (v + (i - v)) < 2 ** 32 /\ v <> 0` by
1681     (Cases_on `u` \\ Q.UNABBREV_TAC `v`
1682      \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC)
1683    \\ IMP_RES_TAC FDOM_build_heap
1684    \\ ASM_SIMP_TAC std_ss [RANGE_def])
1685  \\ METIS_TAC []);
1686
1687val CARD_UNION_IMP = prove(
1688  ``!s t m n. FINITE s /\ FINITE t /\ CARD s <= m /\ CARD t <= n ==>
1689              CARD (s UNION t) <= m + n``,
1690  REPEAT STRIP_TAC \\ IMP_RES_TAC CARD_UNION \\ DECIDE_TAC);
1691
1692val ch_tree_swap = prove(
1693  ``ch_tree (t1,t2,t3,t4,t5,t6,l) (v1,v2,v3,v4,v5,v6,a,dm,m,b,k) ==>
1694    ch_tree (t2,t2,t3,t4,t5,t6,l) (v2,v2,v3,v4,v5,v6,a,dm,m,b,k) /\
1695    ch_tree (t3,t2,t3,t4,t5,t6,l) (v3,v2,v3,v4,v5,v6,a,dm,m,b,k) /\
1696    ch_tree (t4,t2,t3,t4,t5,t6,l) (v4,v2,v3,v4,v5,v6,a,dm,m,b,k) /\
1697    ch_tree (t5,t2,t3,t4,t5,t6,l) (v5,v2,v3,v4,v5,v6,a,dm,m,b,k) /\
1698    ch_tree (t6,t2,t3,t4,t5,t6,l) (v6,v2,v3,v4,v5,v6,a,dm,m,b,k)``,
1699  REPEAT STRIP_TAC
1700  \\ FULL_SIMP_TAC std_ss [ch_tree_def,LET_DEF]
1701  \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u`
1702  \\ FULL_SIMP_TAC std_ss [ch_tree_def,LET_DEF]);
1703
1704val CARD_LESS_EQ_SUM_XSIZE = prove(
1705  ``ch_tree (t1,t2,t3,t4,t5,t6,l) (v1,v2,v3,v4,v5,v6,a,dm,m,b,k) ==>
1706        CARD (reachables [FST (heap_el a v1) ;FST (heap_el a v2); FST (heap_el a v3);
1707                          FST (heap_el a v4) ;FST (heap_el a v5); FST (heap_el a v6)]
1708                (ch_set (build_heap (k,b,a,m))))
1709        <= XSIZE t1 + XSIZE t2 + XSIZE t3 + XSIZE t4 + XSIZE t5 + XSIZE t6``,
1710  NTAC 8 (ONCE_REWRITE_TAC [reachables_THM])
1711  \\ REWRITE_TAC [(hd o CONJUNCTS o SPEC_ALL) reachables_THM,UNION_EMPTY]
1712  \\ REPEAT STRIP_TAC
1713  \\ REWRITE_TAC [GSYM ADD_ASSOC]
1714  \\ STRIP_ASSUME_TAC (UNDISCH ch_tree_swap)
1715  \\ IMP_RES_TAC CARD_LESS_EQ_XSIZE
1716  \\ MATCH_MP_TAC CARD_UNION_IMP
1717  \\ ASM_REWRITE_TAC [FINITE_UNION,FINITE_reachables]
1718  \\ MATCH_MP_TAC CARD_UNION_IMP
1719  \\ ASM_REWRITE_TAC [FINITE_UNION,FINITE_reachables]
1720  \\ MATCH_MP_TAC CARD_UNION_IMP
1721  \\ ASM_REWRITE_TAC [FINITE_UNION,FINITE_reachables]
1722  \\ MATCH_MP_TAC CARD_UNION_IMP
1723  \\ ASM_REWRITE_TAC [FINITE_UNION,FINITE_reachables]
1724  \\ MATCH_MP_TAC CARD_UNION_IMP
1725  \\ ASM_REWRITE_TAC [FINITE_UNION,FINITE_reachables]);
1726
1727val LIMIT_LEMMA = prove(
1728  ``(p ==> m <= n) ==> (p ==> q ==> m < l ==> r) ==>
1729    (p ==> q ==> n < (l:num) ==> r)``,
1730  REPEAT STRIP_TAC \\ RES_TAC \\ `m < l` by DECIDE_TAC \\ METIS_TAC []);
1731
1732val ch_arm_setup = let
1733  val th = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] ch_arm_alloc))
1734  val th = DISCH_ALL (MATCH_MP th (UNDISCH ch_tree_IMP_ch_arm))
1735  val imp = MATCH_MP LIMIT_LEMMA CARD_LESS_EQ_SUM_XSIZE
1736  val th = MATCH_MP imp (RW [MAP] th)
1737  in th end
1738
1739val ch_arm2_def = Define `
1740  ch_arm2 (r,h,l,i,u) c =
1741    ?e rs m. ch_inv (MAP FST r,h,l) (i,e,rs,l,u,m) /\ ch_word (i,e,rs,MAP SND r,l,u,m) c`;
1742
1743val ch_arm_IMP_ch_arm2 = prove(
1744  ``ch_arm (r,h,l) c ==> ?i u. ch_arm2 (r,h,l,i,u) c``,
1745  SIMP_TAC std_ss [ch_arm_def,ch_arm2_def,ch_inv_def] \\ METIS_TAC []);
1746
1747(*
1748set_trace "Goalstack.print_goal_at_top" 0
1749*)
1750
1751
1752val ok_data_ref_field = prove(
1753  ``{x} SUBSET0 RANGE (v,i) /\ 8 * i < 2 ** 32 /\ ALIGNED a ==>
1754    ok_data (ref_field a (x,q)) (ch_active_set (a,v,i))``,
1755  SIMP_TAC std_ss [SUBSET0_DEF,INSERT_SUBSET,IN_INSERT,EMPTY_SUBSET]
1756  \\ Cases_on `x = 0` \\ ASM_SIMP_TAC std_ss []
1757  \\ REPEAT STRIP_TAC THEN1
1758   (FULL_SIMP_TAC std_ss [ref_field_def,ok_data_def]
1759    \\ Cases_on `SND q`
1760    \\ ASM_SIMP_TAC std_ss [NOT_ALIGNED_LEMMA,word_arith_lemma4])
1761  \\ ASM_SIMP_TAC std_ss [ref_field_def,ref_addr_def,ok_data_def]
1762  \\ ASM_SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_n2w]
1763  \\ REWRITE_TAC [GSYM (EVAL ``4*2``),GSYM MULT_ASSOC]
1764  \\ REWRITE_TAC [RW1 [MULT_COMM] (MATCH_MP MOD_EQ_0 (DECIDE ``0<4``))]
1765  \\ SIMP_TAC std_ss [MULT_ASSOC,ch_active_set_def,GSPECIFICATION]
1766  \\ Q.EXISTS_TAC `x` \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def,word_mul_n2w]);
1767
1768val REV_STRIP_TAC =
1769  REWRITE_TAC [CONJ_ASSOC] \\ REVERSE STRIP_TAC \\ REWRITE_TAC [GSYM CONJ_ASSOC]
1770
1771val ch_tree_CAR_CDR = prove(
1772  ``ch_tree (XDot t1 t7,t2,t3,t4,t5,t6,l) (v1,v2,v3,v4,v5,v6,a,dm,m,b,k) ==>
1773    ch_tree (t1,t2,t3,t4,t5,t6,l) (m v1,v2,v3,v4,v5,v6,a,dm,m,b,k) /\
1774    ch_tree (t7,t2,t3,t4,t5,t6,l) (m (v1 + 4w),v2,v3,v4,v5,v6,a,dm,m,b,k)``,
1775  SIMP_TAC std_ss [ch_tree_def,LET_DEF] \\ REPEAT STRIP_TAC
1776  \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u`
1777  \\ FULL_SIMP_TAC std_ss [word_tree_def]);
1778
1779val IN_ch_active_set3 = prove(
1780  ``!v a.
1781       v IN ch_active_set (a,b,j) /\ 8 * j < 2 ** 32 /\ b <> 0 /\ ALIGNED a ==>
1782       ?i. i <> 0 /\ 8 * i < 2 ** 32 /\ (v = n2w (8 * i) + a) /\
1783           (heap_el a v = (i,0w,F))``,
1784  REPEAT STRIP_TAC
1785  \\ IMP_RES_TAC IN_ch_active_set
1786  \\ IMP_RES_TAC IN_ch_active_set2
1787  \\ Q.EXISTS_TAC `i`
1788  \\ Q.PAT_X_ASSUM `0x8w * n2w i = v - a` (ASSUME_TAC o GSYM o RW [WORD_EQ_SUB_LADD])
1789  \\ ASM_SIMP_TAC std_ss [word_mul_n2w]
1790  \\ ASM_SIMP_TAC std_ss [heap_el_def,ALIGNED_ADD_EQ,WORD_ADD_SUB]
1791  \\ SIMP_TAC std_ss [ALIGNED_n2w]
1792  \\ REWRITE_TAC [GSYM (EVAL ``4 * 2``), GSYM MULT_ASSOC,
1793       RW1 [MULT_COMM] (MATCH_MP MOD_EQ_0 (DECIDE ``0<4``))]
1794  \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [MULT_ASSOC,w2n_n2w]
1795  \\ REWRITE_TAC [RW1 [MULT_COMM] (MATCH_MP MULT_DIV (DECIDE ``0<8``))]);
1796
1797val MEM_fix = prove(``set l x = MEM x l``, SIMP_TAC bool_ss [IN_DEF])
1798val IN_reachables =
1799    ``(a,b,c,d) IN reachables rs h``
1800        |> SIMP_CONV bool_ss [reachables_def, IN_DEF]
1801        |> REWRITE_RULE [MEM_fix]
1802
1803val ch_arm2_CAR = prove(
1804  ``(FST q1) IN FDOM h /\
1805    (h ' (FST q1) = (z1,y1,z2,y2)) /\
1806    ch_arm2 ([q1; q2; q3; q4; q5; q6],h,l,i,u) (w1,w2,w3,w4,w5,w6,a,dm,xs) ==>
1807    ch_arm2 ([(z1,z2); q2; q3; q4; q5; q6],h,l,i,u) (xs w1,w2,w3,w4,w5,w6,a,dm,xs)``,
1808  SIMP_TAC std_ss [ch_arm2_def,ch_inv_def] \\ REPEAT STRIP_TAC
1809  \\ `(FST q1,z1,y1,z2,y2) IN reachables (MAP FST [q1; q2; q3; q4; q5; q6]) (ch_set h)` by
1810   (FULL_SIMP_TAC std_ss [IN_reachables,ch_set_def]
1811    \\ Q.EXISTS_TAC `FST q1` \\ SIMP_TAC std_ss [MEM,MAP,reachable_def])
1812  \\ `(FST q1,z1,y1,z2,y2) IN abstract (b,m)` by METIS_TAC [SUBSET_DEF]
1813  \\ FULL_SIMP_TAC std_ss [abstract_def,GSPECIFICATION]
1814  \\ `?a1 a2 a3 a4 a5. x = (a1,a2,a3,a4,a5)` by METIS_TAC [PAIR]
1815  \\ FULL_SIMP_TAC std_ss [abstract_def,GSPECIFICATION]
1816  \\ Q.EXISTS_TAC `e`
1817  \\ Q.EXISTS_TAC `a2 :: TL rs` \\ Q.EXISTS_TAC `m`
1818  \\ `ok_state (i,e,a2::TL rs,l,u,m) /\ a1 IN RANGE (if u then 1 + l else 1,i)` by
1819   (FULL_SIMP_TAC std_ss [ok_state_def,LET_DEF,MEM]
1820    \\ Cases_on `rs`
1821    \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,NOT_NIL_CONS,MEM,ok_abs_def,TL]
1822    \\ `(h' = a1) /\ (b a1 <> 0)` by METIS_TAC [ONE_ONE_DEF,ONTO_DEF,bijection_def]
1823    \\ `(a1 <> 0)` by METIS_TAC [ONE_ONE_DEF,ONTO_DEF,bijection_def]
1824    \\ `a1 IN RANGE (if u then 1 + l else 1,i)` by METIS_TAC []
1825    \\ RES_TAC
1826    \\ FULL_SIMP_TAC std_ss [SUBSET0_DEF,INSERT_SUBSET,IN_INSERT,heap_type_11]
1827    \\ METIS_TAC [])
1828  \\ FULL_SIMP_TAC std_ss [GSYM abstract_def]
1829  \\ STRIP_TAC THEN1
1830   (FULL_SIMP_TAC std_ss [ok_abs_def,MEM,MAP,FEVERY_DEF]
1831    \\ RES_TAC \\ POP_ASSUM MP_TAC \\ ASM_REWRITE_TAC []
1832    \\ SIMP_TAC std_ss [] \\ STRIP_TAC \\ STRIP_TAC THEN1
1833      (FULL_SIMP_TAC std_ss [SUBSET0_DEF,INSERT_SUBSET,IN_INSERT]
1834      \\ METIS_TAC [])
1835    \\ Q.EXISTS_TAC `b` \\ Cases_on `rs`
1836    \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,NOT_NIL_CONS,MEM,ok_abs_def,TL]
1837    \\ MATCH_MP_TAC SUBSET_TRANS
1838    \\ Q.EXISTS_TAC `reachables [b a1; FST q2; FST q3; FST q4; FST q5; FST q6] (ch_set h)`
1839    \\ ASM_SIMP_TAC std_ss []
1840    \\ ASM_SIMP_TAC std_ss [SUBSET_DEF,IN_DEF,reachables_def,FORALL_PROD,MEM]
1841    \\ REPEAT STRIP_TAC THEN1
1842     (Q.EXISTS_TAC `b a1` \\ FULL_SIMP_TAC std_ss [reachable_def] THENL [
1843        DISJ2_TAC \\ Q.EXISTS_TAC `[]`
1844        \\ ASM_SIMP_TAC std_ss [APPEND,PATH_def,IN_DEF,ch_set_def]
1845        \\ METIS_TAC [],
1846        DISJ2_TAC \\ Q.EXISTS_TAC `b a2::p`
1847        \\ ASM_SIMP_TAC std_ss [APPEND,PATH_def,IN_DEF,ch_set_def]
1848        \\ METIS_TAC []])
1849    \\ METIS_TAC [])
1850  \\ FULL_SIMP_TAC std_ss [ch_word_def,MAP,CONS_11,TL]
1851  \\ FULL_SIMP_TAC std_ss [ref_cheney_def]
1852  \\ `a1 <= l+l+1` by (Cases_on `u`
1853    \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def,ok_state_def,LET_DEF]
1854    \\ DECIDE_TAC)
1855  \\ RES_TAC \\ POP_ASSUM MP_TAC
1856  \\ `a1 <> 0` by (CCONTR_TAC \\ FULL_SIMP_TAC std_ss [ok_abs_def])
1857  \\ `x1 <> 0` by (CCONTR_TAC \\ FULL_SIMP_TAC std_ss [ok_abs_def,MAP,CONS_11])
1858  \\ `ref_field a (x1,SND q1) = ref_addr a x1` by
1859       ASM_SIMP_TAC bool_ss [ref_mem_def,ref_field_def]
1860  \\ ASM_REWRITE_TAC []
1861  \\ ASM_SIMP_TAC std_ss [ref_mem_def]
1862  \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,bijection_def,ONE_ONE_DEF]
1863  \\ METIS_TAC []);
1864
1865val ch_arm2_swap2 = prove(
1866  ``ch_arm2 ([q1; q2; q3; q4; q5; q6],h,l,i,u) (w1,w2,w3,w4,w5,w6,a,dm,xs) ==>
1867    ch_arm2 ([q2; q1; q3; q4; q5; q6],h,l,i,u) (w2,w1,w3,w4,w5,w6,a,dm,xs)``,
1868  SIMP_TAC std_ss [ch_arm2_def,ch_word_def,ch_inv_def,ok_state_def,
1869    ok_abs_def,LET_DEF] \\ REPEAT STRIP_TAC
1870  \\ FULL_SIMP_TAC std_ss [MAP,MEM,CONS_11]
1871  \\ Q.EXISTS_TAC `[x2; x1; x3; x4; x5; x6]` \\ Q.EXISTS_TAC `m`
1872  \\ FULL_SIMP_TAC std_ss [MAP,MEM,CONS_11,SUBSET_DEF,IN_DEF,
1873       reachables_def,FORALL_PROD]
1874  \\ FULL_SIMP_TAC std_ss [AC DISJ_COMM DISJ_ASSOC]
1875  \\ REPEAT STRIP_TAC \\ REPEAT (Q.EXISTS_TAC `b`) \\ METIS_TAC []);
1876
1877val ch_arm2_swap3 = prove(
1878  ``ch_arm2 ([q1; q2; q3; q4; q5; q6],h,l,i,u) (w1,w2,w3,w4,w5,w6,a,dm,xs) ==>
1879    ch_arm2 ([q3; q2; q1; q4; q5; q6],h,l,i,u) (w3,w2,w1,w4,w5,w6,a,dm,xs)``,
1880  SIMP_TAC std_ss [ch_arm2_def,ch_word_def,ch_inv_def,ok_state_def,
1881    ok_abs_def,LET_DEF] \\ REPEAT STRIP_TAC
1882  \\ FULL_SIMP_TAC std_ss [MAP,MEM,CONS_11]
1883  \\ Q.EXISTS_TAC `[x3; x2; x1; x4; x5; x6]` \\ Q.EXISTS_TAC `m`
1884  \\ FULL_SIMP_TAC std_ss [MAP,MEM,CONS_11,SUBSET_DEF,IN_DEF,
1885       reachables_def,FORALL_PROD]
1886  \\ FULL_SIMP_TAC std_ss [AC DISJ_COMM DISJ_ASSOC]
1887  \\ REPEAT STRIP_TAC \\ REPEAT (Q.EXISTS_TAC `b`) \\ METIS_TAC []);
1888
1889val ch_arm2_swap4 = prove(
1890  ``ch_arm2 ([q1; q2; q3; q4; q5; q6],h,l,i,u) (w1,w2,w3,w4,w5,w6,a,dm,xs) ==>
1891    ch_arm2 ([q4; q2; q3; q1; q5; q6],h,l,i,u) (w4,w2,w3,w1,w5,w6,a,dm,xs)``,
1892  SIMP_TAC std_ss [ch_arm2_def,ch_word_def,ch_inv_def,ok_state_def,
1893    ok_abs_def,LET_DEF] \\ REPEAT STRIP_TAC
1894  \\ FULL_SIMP_TAC std_ss [MAP,MEM,CONS_11]
1895  \\ Q.EXISTS_TAC `[x4; x2; x3; x1; x5; x6]` \\ Q.EXISTS_TAC `m`
1896  \\ FULL_SIMP_TAC std_ss [MAP,MEM,CONS_11,SUBSET_DEF,IN_DEF,
1897       reachables_def,FORALL_PROD]
1898  \\ FULL_SIMP_TAC std_ss [AC DISJ_COMM DISJ_ASSOC]
1899  \\ REPEAT STRIP_TAC \\ REPEAT (Q.EXISTS_TAC `b`) \\ METIS_TAC []);
1900
1901val ch_arm2_swap5 = prove(
1902  ``ch_arm2 ([q1; q2; q3; q4; q5; q6],h,l,i,u) (w1,w2,w3,w4,w5,w6,a,dm,xs) ==>
1903    ch_arm2 ([q5; q2; q3; q4; q1; q6],h,l,i,u) (w5,w2,w3,w4,w1,w6,a,dm,xs)``,
1904  SIMP_TAC std_ss [ch_arm2_def,ch_word_def,ch_inv_def,ok_state_def,
1905    ok_abs_def,LET_DEF] \\ REPEAT STRIP_TAC
1906  \\ FULL_SIMP_TAC std_ss [MAP,MEM,CONS_11]
1907  \\ Q.EXISTS_TAC `[x5; x2; x3; x4; x1; x6]` \\ Q.EXISTS_TAC `m`
1908  \\ FULL_SIMP_TAC std_ss [MAP,MEM,CONS_11,SUBSET_DEF,IN_DEF,
1909       reachables_def,FORALL_PROD]
1910  \\ FULL_SIMP_TAC std_ss [AC DISJ_COMM DISJ_ASSOC]
1911  \\ REPEAT STRIP_TAC \\ REPEAT (Q.EXISTS_TAC `b`) \\ METIS_TAC []);
1912
1913val ch_arm2_swap6 = prove(
1914  ``ch_arm2 ([q1; q2; q3; q4; q5; q6],h,l,i,u) (w1,w2,w3,w4,w5,w6,a,dm,xs) ==>
1915    ch_arm2 ([q6; q2; q3; q4; q5; q1],h,l,i,u) (w6,w2,w3,w4,w5,w1,a,dm,xs)``,
1916  SIMP_TAC std_ss [ch_arm2_def,ch_word_def,ch_inv_def,ok_state_def,
1917    ok_abs_def,LET_DEF] \\ REPEAT STRIP_TAC
1918  \\ FULL_SIMP_TAC std_ss [MAP,MEM,CONS_11]
1919  \\ Q.EXISTS_TAC `[x6; x2; x3; x4; x5; x1]` \\ Q.EXISTS_TAC `m`
1920  \\ FULL_SIMP_TAC std_ss [MAP,MEM,CONS_11,SUBSET_DEF,IN_DEF,
1921       reachables_def,FORALL_PROD]
1922  \\ FULL_SIMP_TAC std_ss [AC DISJ_COMM DISJ_ASSOC]
1923  \\ REPEAT STRIP_TAC \\ REPEAT (Q.EXISTS_TAC `b`) \\ METIS_TAC []);
1924
1925val ch_arm2_CDR = prove(
1926  ``(FST q1) IN FDOM h /\
1927    (h ' (FST q1) = (z1,y1,z2,y2)) /\
1928    ch_arm2 ([q1; q2; q3; q4; q5; q6],h,l,i,u) (w1,w2,w3,w4,w5,w6,a,dm,xs) ==>
1929    ch_arm2 ([(y1,y2); q2; q3; q4; q5; q6],h,l,i,u) (xs (w1+4w),w2,w3,w4,w5,w6,a,dm,xs) /\
1930    w1 IN ch_active_set (a,if u then 1 + l else 1,i) /\ ALIGNED w1``,
1931  SIMP_TAC std_ss [ch_arm2_def,ch_inv_def] \\ STRIP_TAC
1932  \\ `(FST q1,z1,y1,z2,y2) IN reachables (MAP FST [q1; q2; q3; q4; q5; q6]) (ch_set h)` by
1933   (FULL_SIMP_TAC std_ss [IN_reachables,ch_set_def]
1934    \\ Q.EXISTS_TAC `FST q1` \\ SIMP_TAC std_ss [MEM,MAP,reachable_def])
1935  \\ `(FST q1,z1,y1,z2,y2) IN abstract (b,m)` by METIS_TAC [SUBSET_DEF]
1936  \\ FULL_SIMP_TAC std_ss [abstract_def,GSPECIFICATION]
1937  \\ `?a1 a2 a3 a4 a5. x = (a1,a3,a2,a5,a4)` by METIS_TAC [PAIR]
1938  \\ FULL_SIMP_TAC std_ss [abstract_def,GSPECIFICATION]
1939  \\ SIMP_TAC std_ss [METIS_PROVE [] ``(?x. P x) /\ Q = ?x. P x /\ Q``]
1940  \\ Q.EXISTS_TAC `e`
1941  \\ Q.EXISTS_TAC `a2 :: TL rs` \\ Q.EXISTS_TAC `m`
1942  \\ `ok_state (i,e,a2::TL rs,l,u,m) /\ a1 IN RANGE (if u then 1 + l else 1,i)` by
1943   (FULL_SIMP_TAC std_ss [ok_state_def,LET_DEF,MEM]
1944    \\ Cases_on `rs`
1945    \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,NOT_NIL_CONS,MEM,ok_abs_def,TL]
1946    \\ `(h' = a1) /\ (b a1 <> 0)` by METIS_TAC [ONE_ONE_DEF,ONTO_DEF,bijection_def]
1947    \\ `(a1 <> 0)` by METIS_TAC [ONE_ONE_DEF,ONTO_DEF,bijection_def]
1948    \\ `a1 IN RANGE (if u then 1 + l else 1,i)` by METIS_TAC []
1949    \\ RES_TAC
1950    \\ FULL_SIMP_TAC std_ss [SUBSET0_DEF,INSERT_SUBSET,IN_INSERT,heap_type_11]
1951    \\ METIS_TAC [])
1952  \\ FULL_SIMP_TAC std_ss [GSYM abstract_def]
1953  \\ REWRITE_TAC [GSYM CONJ_ASSOC]
1954  \\ ONCE_REWRITE_TAC [CONJ_ASSOC]
1955  \\ STRIP_TAC THEN1
1956   (FULL_SIMP_TAC std_ss [ok_abs_def,MEM,MAP,FEVERY_DEF]
1957    \\ RES_TAC \\ POP_ASSUM MP_TAC \\ ASM_REWRITE_TAC []
1958    \\ SIMP_TAC std_ss [] \\ STRIP_TAC \\ STRIP_TAC THEN1
1959      (FULL_SIMP_TAC std_ss [SUBSET0_DEF,INSERT_SUBSET,IN_INSERT]
1960      \\ METIS_TAC [])
1961    \\ Q.EXISTS_TAC `b` \\ Cases_on `rs`
1962    \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,NOT_NIL_CONS,MEM,ok_abs_def,TL]
1963    \\ MATCH_MP_TAC SUBSET_TRANS
1964    \\ Q.EXISTS_TAC `reachables [b a1; FST q2; FST q3; FST q4; FST q5; FST q6] (ch_set h)`
1965    \\ ASM_SIMP_TAC std_ss []
1966    \\ ASM_SIMP_TAC std_ss [SUBSET_DEF,IN_DEF,reachables_def,FORALL_PROD,MEM]
1967    \\ REPEAT STRIP_TAC THEN1
1968     (Q.EXISTS_TAC `b a1` \\ FULL_SIMP_TAC std_ss [reachable_def] THENL [
1969        DISJ2_TAC \\ Q.EXISTS_TAC `[]`
1970        \\ ASM_SIMP_TAC std_ss [APPEND,PATH_def,IN_DEF,ch_set_def]
1971        \\ METIS_TAC [],
1972        DISJ2_TAC \\ Q.EXISTS_TAC `b a2::p`
1973        \\ ASM_SIMP_TAC std_ss [APPEND,PATH_def,IN_DEF,ch_set_def]
1974        \\ METIS_TAC []])
1975    \\ METIS_TAC [])
1976  \\ FULL_SIMP_TAC std_ss [ch_word_def,MAP,CONS_11,TL]
1977  \\ FULL_SIMP_TAC std_ss [ref_cheney_def]
1978  \\ `a1 <= l+l+1` by (Cases_on `u`
1979    \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def,ok_state_def,LET_DEF]
1980    \\ DECIDE_TAC)
1981  \\ RES_TAC \\ POP_ASSUM MP_TAC
1982  \\ `a1 <> 0` by (CCONTR_TAC \\ FULL_SIMP_TAC std_ss [ok_abs_def])
1983  \\ `x1 <> 0` by (CCONTR_TAC \\ FULL_SIMP_TAC std_ss [ok_abs_def,MAP,CONS_11])
1984  \\ `ref_field a (x1,SND q1) = ref_addr a x1` by
1985       ASM_SIMP_TAC bool_ss [ref_mem_def,ref_field_def]
1986  \\ ASM_REWRITE_TAC []
1987  \\ ASM_SIMP_TAC std_ss [ref_mem_def]
1988  \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,bijection_def,ONE_ONE_DEF]
1989  \\ `a1 = x1` by METIS_TAC []
1990  \\ FULL_SIMP_TAC std_ss []
1991  \\ STRIP_TAC
1992  \\ FULL_SIMP_TAC std_ss [ref_addr_def,ch_active_set_def,
1993       GSPECIFICATION,word_mul_n2w,ALIGNED_ADD_EQ,ALIGNED_INTRO]
1994  \\ SIMP_TAC bool_ss [ALIGNED_n2w,GSYM (EVAL ``4*2``),GSYM MULT_ASSOC]
1995  \\ REWRITE_TAC [RW1 [MULT_COMM] (MATCH_MP MOD_EQ_0 (DECIDE ``0<4``))]
1996  \\ Q.EXISTS_TAC `x1` \\ REWRITE_TAC []
1997  \\ FULL_SIMP_TAC std_ss [LET_DEF,ok_state_def,MEM]
1998  \\ `x1 IN RANGE (if u then 1 + l else 1,i)` by METIS_TAC []
1999  \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def]
2000  \\ DECIDE_TAC);
2001
2002val ch_tree_XDot = prove(
2003  ``ch_tree (XDot tx ty,t2,t3,t4,t5,t6,l) (v1,v2,v3,v4,v5,v6,a,dm,m,b,k) ==>
2004    (FST (heap_el a v1)) IN FDOM (build_heap (k,b,a,m)) /\
2005    (build_heap (k,b,a,m) ' (FST (heap_el a v1)) =
2006      (FST (heap_el a (m v1)),
2007       FST (heap_el a (m (v1 + 4w))),
2008       SND (heap_el a (m v1)),
2009       SND (heap_el a (m (v1 + 4w)))))``,
2010  SIMP_TAC std_ss [ch_tree_def,LET_DEF,word_tree_def] \\ STRIP_TAC
2011  \\ Q.ABBREV_TAC `v = if u then 1 + l else 1`
2012  \\ `v <> 0 /\ 8 * i < 2 ** 32` by
2013   (Cases_on `u` \\ Q.UNABBREV_TAC `v`
2014    \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC)
2015  \\ `?j. j <> 0 /\ 8 * j < 2 ** 32 /\ (v1 = n2w (8 * j) + a) /\
2016          (heap_el a v1 = (j,0x0w,F))` by
2017              METIS_TAC [IN_ch_active_set3]
2018  \\ `j IN RANGE (v,i)` by
2019   (IMP_RES_TAC IN_ch_active_set
2020    \\ Q.PAT_X_ASSUM `w2n (v1 - a) DIV 8 IN RANGE (v,i)` MP_TAC
2021    \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_ADD_SUB,w2n_n2w]
2022    \\ SIMP_TAC std_ss [RW1 [MULT_COMM] (MULT_DIV)])
2023  \\ ASM_SIMP_TAC std_ss []
2024  \\ `i = v + (i - v)` by DECIDE_TAC
2025  \\ `j IN FDOM (build_heap (i - v,a + n2w (8 * v),a,m)) /\
2026      (build_heap (i - v,a + n2w (8 * v),a,m) ' j =
2027      (let (x1,x2) = heap_el a (m (n2w (8 * j) + a)) in
2028       let (y1,y2) = heap_el a (m (n2w (8 * j) + a + 0x4w)) in
2029         (x1,y1,x2,y2)))` by METIS_TAC [build_heap_DATA,WORD_ADD_COMM]
2030  \\ ASM_SIMP_TAC std_ss []
2031  \\ Cases_on `(heap_el a (m (n2w (8 * j) + a)))`
2032  \\ Cases_on `(heap_el a (m (n2w (8 * j) + a + 4w)))`
2033  \\ SIMP_TAC std_ss [LET_DEF]);
2034
2035val IMP_word_tree = prove(
2036  ``!t1 v1 w1.
2037      ch_tree (t1,t2,t3,t4,t5,t6,l) (v1,v2,v3,v4,v5,v6,a,dm,m,b,k) /\
2038      ch_arm2
2039        ([heap_el a v1; q2; q3; q4; q5; q6],
2040         build_heap (k,b,a,m) |+
2041         (fresh (build_heap (k,b,a,m)),qqq),l,i,u) (w1,w2,w3,w4,w5,w6,a,dm,xs) ==>
2042      word_tree t1 (w1,xs) (ch_active_set (a,if u then 1 + l else 1,i))``,
2043  REVERSE Induct THEN1
2044   (REPEAT STRIP_TAC
2045    \\ FULL_SIMP_TAC std_ss [ch_tree_def,LET_DEF,word_tree_def]
2046    \\ Q.PAT_X_ASSUM `v1 = ADDR32 c + 0x3w` (fn th => FULL_SIMP_TAC std_ss [th])
2047    \\ FULL_SIMP_TAC std_ss [heap_el_def,NOT_ALIGNED_LEMMA,WORD_ADD_SUB,
2048         ALIGNED_ADDR32,ADDR30_ADDR32,ch_arm2_def,ch_word_def,MAP,CONS_11]
2049    \\ FULL_SIMP_TAC std_ss [ch_inv_def,MAP,CONS_11,bijection_def]
2050    \\ `x1 = 0` by METIS_TAC [ONE_ONE_DEF]
2051    \\ ASM_SIMP_TAC std_ss [ref_field_def])
2052  THEN1
2053   (REPEAT STRIP_TAC
2054    \\ FULL_SIMP_TAC std_ss [ch_tree_def,LET_DEF,word_tree_def]
2055    \\ Q.PAT_X_ASSUM `v1 = ADDR32 c + 0x2w` (fn th => FULL_SIMP_TAC std_ss [th])
2056    \\ FULL_SIMP_TAC std_ss [heap_el_def,NOT_ALIGNED_LEMMA,WORD_ADD_SUB,
2057         ALIGNED_ADDR32,ADDR30_ADDR32,ch_arm2_def,ch_word_def,MAP,CONS_11,
2058         word_arith_lemma4]
2059    \\ FULL_SIMP_TAC std_ss [ch_inv_def,MAP,CONS_11,bijection_def]
2060    \\ `x1 = 0` by METIS_TAC [ONE_ONE_DEF]
2061    \\ ASM_SIMP_TAC std_ss [ref_field_def])
2062  \\ REPEAT STRIP_TAC
2063  \\ IMP_RES_TAC ch_tree_XDot
2064  \\ Q.ABBREV_TAC `hhh = build_heap (k,b,a,m) |+ (fresh (build_heap (k,b,a,m)),qqq)`
2065  \\ `FST (heap_el a v1) IN FDOM hhh /\
2066     (hhh ' (FST (heap_el a v1)) =
2067      (FST (heap_el a (m v1)),FST (heap_el a (m (v1 + 0x4w))),
2068       SND (heap_el a (m v1)),SND (heap_el a (m (v1 + 0x4w)))))` by
2069    (Q.UNABBREV_TAC `hhh`
2070    \\ ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM,FDOM_FUPDATE,IN_INSERT]
2071    \\ METIS_TAC [fresh_NOT_IN_FDOM])
2072  \\ IMP_RES_TAC ch_arm2_CAR
2073  \\ IMP_RES_TAC ch_arm2_CDR
2074  \\ REPEAT (Q.PAT_X_ASSUM `!xxx yyyy xzzz.bbb` (K ALL_TAC))
2075  \\ FULL_SIMP_TAC std_ss [word_tree_def]
2076  \\ IMP_RES_TAC ch_tree_CAR_CDR
2077  \\ RES_TAC \\ ASM_SIMP_TAC std_ss []
2078  \\ REPEAT (Q.PAT_X_ASSUM `xxx ==> yy` (K ALL_TAC))
2079  \\ REPEAT (Q.PAT_X_ASSUM `!xxx.bbb` (K ALL_TAC))
2080  \\ Q.UNABBREV_TAC `hhh`
2081  \\ NTAC 10 (POP_ASSUM (K ALL_TAC))
2082  \\ FULL_SIMP_TAC std_ss [ch_arm2_def]
2083  \\ `?j. j <> 0 /\ 8 * j < 2 ** 32 /\ (heap_el a v1 = (j,0x0w,F))` by
2084     (FULL_SIMP_TAC std_ss [ch_tree_def,LET_DEF,word_tree_def]
2085      \\ Q.ABBREV_TAC `vv = if u' then 1 + l else 1`
2086      \\ `8 * i' < 2**32 /\ vv <> 0` by
2087        (Cases_on `u'` \\ Q.UNABBREV_TAC `vv`
2088         \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC)
2089      \\ FULL_SIMP_TAC std_ss []
2090      \\ METIS_TAC [SIMP_RULE std_ss [] IN_ch_active_set3])
2091  \\ FULL_SIMP_TAC std_ss [FST,MAP]);
2092
2093val ch_tree_alloc_lemma = prove(
2094  ``ch_tree (t1,t2,t3,t4,t5,t6,l) (v1,v2,v3,v4,v5,v6,a,dm,m,b,k) ==>
2095    ch_arm2
2096     ([(fresh (build_heap (k,b,a,m)),SND (heap_el a v1)); heap_el a v2;
2097       heap_el a v3; heap_el a v4; heap_el a v5; heap_el a v6],
2098      build_heap (k,b,a,m) |+
2099      (fresh (build_heap (k,b,a,m)),FST (heap_el a v1),
2100       FST (heap_el a v2),SND (heap_el a v1),SND (heap_el a v2)),l,i,u)
2101     (w1,w2,w3,w4,w5,w6,a,dm,xs') ==>
2102    ?b k. ch_tree (XDot t1 t2,t2,t3,t4,t5,t6,l) (w1,w2,w3,w4,w5,w6,a,dm,xs',b,k)``,
2103  REPEAT STRIP_TAC
2104  \\ SIMP_TAC std_ss [ch_tree_def,LET_DEF]
2105  \\ Q.EXISTS_TAC `i` \\ Q.EXISTS_TAC `u`
2106  \\ REV_STRIP_TAC THEN1
2107   (FULL_SIMP_TAC std_ss [ch_arm2_def]
2108    \\ Q.PAT_X_ASSUM `ch_inv xxx yyy` (K ALL_TAC)
2109    \\ FULL_SIMP_TAC std_ss [ch_word_def]
2110    \\ REPEAT (Q.PAT_X_ASSUM `ww = ref_field a (xx,yy)` (K ALL_TAC))
2111    \\ POP_ASSUM MP_TAC
2112    \\ NTAC 6 (POP_ASSUM (K ALL_TAC))
2113    \\ NTAC 3 STRIP_TAC
2114    \\ FULL_SIMP_TAC std_ss [ok_state_def,LET_DEF]
2115    \\ Q.ABBREV_TAC `v = if u then 1 + l else 1`
2116    \\ `8 * i < 2 ** 32 /\ v <> 0` by
2117      (Cases_on `u` \\ Q.UNABBREV_TAC `v`
2118       \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC)
2119    \\ IMP_RES_TAC IN_ch_active_set
2120    \\ `?j. j <> 0 /\ 8 * j < 2 ** 32 /\ (w - a = 0x8w * n2w j)` by
2121         METIS_TAC [IN_ch_active_set2]
2122    \\ FULL_SIMP_TAC std_ss [WORD_EQ_SUB_LADD,word_mul_n2w]
2123    \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w, RW1 [MULT_COMM] MULT_DIV]
2124    \\ RES_TAC
2125    \\ FULL_SIMP_TAC std_ss [ref_cheney_def,ALIGNED_INTRO]
2126    \\ `j <= l + l + 1` by
2127      (Cases_on `u` \\ Q.UNABBREV_TAC `v`
2128       \\ FULL_SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ DECIDE_TAC)
2129    \\ RES_TAC
2130    \\ Q.PAT_X_ASSUM `ref_mem j xxx (a,yyy)` MP_TAC
2131    \\ Cases_on `d'`
2132    \\ ASM_REWRITE_TAC [ref_mem_def]
2133    \\ FULL_SIMP_TAC std_ss [ref_addr_def,WORD_EQ_SUB_RADD]
2134    \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM]
2135    \\ REPEAT STRIP_TAC
2136    \\ MATCH_MP_TAC ok_data_ref_field
2137    \\ FULL_SIMP_TAC std_ss [SUBSET0_DEF,INSERT_SUBSET,EMPTY_SUBSET])
2138  \\ REV_STRIP_TAC THEN1
2139   (MATCH_MP_TAC (GEN_ALL IMP_word_tree) \\ IMP_RES_TAC ch_arm2_swap6
2140    \\ IMP_RES_TAC ch_tree_swap \\ METIS_TAC [])
2141  \\ REV_STRIP_TAC THEN1
2142   (MATCH_MP_TAC (GEN_ALL IMP_word_tree) \\ IMP_RES_TAC ch_arm2_swap5
2143    \\ IMP_RES_TAC ch_tree_swap \\ METIS_TAC [])
2144  \\ REV_STRIP_TAC THEN1
2145   (MATCH_MP_TAC (GEN_ALL IMP_word_tree) \\ IMP_RES_TAC ch_arm2_swap4
2146    \\ IMP_RES_TAC ch_tree_swap \\ METIS_TAC [])
2147  \\ REV_STRIP_TAC THEN1
2148   (MATCH_MP_TAC (GEN_ALL IMP_word_tree) \\ IMP_RES_TAC ch_arm2_swap3
2149    \\ IMP_RES_TAC ch_tree_swap \\ METIS_TAC [])
2150  \\ REV_STRIP_TAC THEN1
2151   (MATCH_MP_TAC (GEN_ALL IMP_word_tree) \\ IMP_RES_TAC ch_arm2_swap2
2152    \\ IMP_RES_TAC ch_tree_swap \\ METIS_TAC [])
2153  \\ REVERSE REV_STRIP_TAC THEN1
2154   (FULL_SIMP_TAC std_ss [ch_arm2_def,ch_word_def,ref_addr_def,
2155      ALIGNED_INTRO,ch_tree_def,LET_DEF,ok_state_def]
2156    \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC)
2157  \\ SIMP_TAC std_ss [word_tree_def]
2158  \\ Q.ABBREV_TAC `f = fresh (build_heap (k,b,a,m))`
2159  \\ Q.ABBREV_TAC `xx = (FST (heap_el a v1),FST (heap_el a v2),SND (heap_el a v1),
2160          SND (heap_el a v2))`
2161  \\ Q.ABBREV_TAC `hh = build_heap (k,b,a,m) |+ (f,xx)`
2162  \\ `(FST (f,SND (heap_el a v1))) IN FDOM hh /\
2163      (hh ' (FST (f,SND (heap_el a v1))) = xx)` by
2164   (Q.UNABBREV_TAC `hh`
2165    \\ ASM_SIMP_TAC std_ss [FDOM_FUPDATE,IN_INSERT,FAPPLY_FUPDATE_THM,FST])
2166  \\ Q.UNABBREV_TAC `xx`
2167  \\ IMP_RES_TAC ch_arm2_CDR
2168  \\ IMP_RES_TAC ch_arm2_CAR
2169  \\ FULL_SIMP_TAC std_ss []
2170  \\ REV_STRIP_TAC THEN1
2171   (MATCH_MP_TAC (GEN_ALL IMP_word_tree) \\ IMP_RES_TAC ch_arm2_swap2
2172    \\ IMP_RES_TAC ch_tree_swap \\ METIS_TAC [])
2173  \\ MATCH_MP_TAC (GEN_ALL IMP_word_tree) \\ METIS_TAC []);
2174
2175val ch_tree_alloc = store_thm("ch_tree_alloc",
2176  ``ch_tree (t1,t2,t3,t4,t5,t6,l) (v1,v2,v3,v4,v5,v6,a,dm,m,b,k) ==>
2177    (arm_alloc (v1,v2,v3,v4,v5,v6,a,dm,m) = (w1,w2,w3,w4,w5,w6,a2,dm2,m2)) ==>
2178    XSIZE t1 + XSIZE t2 + XSIZE t3 + XSIZE t4 + XSIZE t5 + XSIZE t6 < l ==>
2179    (a2 = a) /\ (dm2 = dm) /\
2180    arm_alloc_pre (v1,v2,v3,v4,v5,v6,a,dm,m) /\
2181    ?b k. ch_tree (XDot t1 t2,t2,t3,t4,t5,t6,l) (w1,w2,w3,w4,w5,w6,a2,dm2,m2,b,k)``,
2182  REPEAT STRIP_TAC \\ IMP_RES_TAC ch_arm_setup
2183  \\ IMP_RES_TAC ch_arm_IMP_ch_arm2
2184  \\ Q.PAT_X_ASSUM `a2 = a` (fn th => FULL_SIMP_TAC std_ss [th])
2185  \\ Q.PAT_X_ASSUM `dm2 = dm` (fn th => FULL_SIMP_TAC std_ss [th])
2186  \\ IMP_RES_TAC ch_tree_alloc_lemma \\ METIS_TAC []);
2187
2188
2189(* --- PowerPC --- *)
2190
2191val (th,def,pre) = compile "ppc" ``
2192  ppc_move (r4:word32,r5:word32,r7:word32,r8:word32,df:word32 set,f:word32->word32) =
2193    (if r5 && 3w = 0x0w then
2194       (let r7 = f r5 in
2195        let r8 = r7 && 3w in
2196          (if r8 = 0x1w then
2197             (let r5 = r7 - 0x1w in (r4,r5,r7,r8,df,f))
2198           else
2199             (let r8 = f (r5 + 0x4w) in
2200              let f = (r4 =+ r7) f in
2201              let r4 = r4 + 0x4w in
2202              let f = (r4 =+ r8) f in
2203              let r4 = r4 + 0x4w in
2204              let r7 = r4 - 0x7w in
2205              let f = (r5 =+ r7) f in
2206              let r5 = r7 - 0x1w in
2207                (r4,r5,r7,r8,df,f))))
2208     else
2209       (r4,r5,r7,r8,df,f))``
2210
2211val (th,def,pre) = compile "ppc" ``
2212  ppc_move2 (r4:word32,r6:word32,r7:word32,r8:word32,df:word32 set,f:word32->word32) =
2213    (if r6 && 0x3w = 0x0w then
2214       (let r7 = f r6 in
2215        let r8 = 0x3w && r7 in
2216          (if r8 = 0x1w then
2217             (let r6 = r7 - 0x1w in (r4,r6,r7,r8,df,f))
2218           else
2219             (let r8 = f (r6 + 0x4w) in
2220              let f = (r4 =+ r7) f in
2221              let r4 = r4 + 0x4w in
2222              let f = (r4 =+ r8) f in
2223              let r4 = r4 + 0x4w in
2224              let r7 = r4 - 0x7w in
2225              let f = (r6 =+ r7) f in
2226              let r6 = r7 - 0x1w in
2227                (r4,r6,r7,r8,df,f))))
2228     else
2229       (r4,r6,r7,r8,df,f))``
2230
2231val (th,def,pre) = compile "ppc" ``
2232  ppc_cheney_step (r3:word32,r4:word32,r7:word32,r8:word32,df:word32 set,f:word32->word32) =
2233    (let r5 = f r3 in
2234     let r6 = f (r3 + 0x4w) in
2235     let (r4,r5,r7,r8,df,f) = ppc_move (r4,r5,r7,r8,df,f) in
2236     let (r4,r6,r7,r8,df,f) = ppc_move2 (r4,r6,r7,r8,df,f) in
2237     let f = (r3 =+ r5) f in
2238     let r3 = r3 + 0x4w in
2239     let f = (r3 =+ r6) f in
2240     let r3 = r3 + 0x4w in
2241       (r3,r4,r5,r6,r7,r8,df,f))``;
2242
2243val (th,def,pre) = compile "ppc" ``
2244  ppc_cheney_loop (r3,r4,r5,r6,r7,r8,df,f) =
2245    (if r3 = r4 then
2246       (r3,r4,r5,r6,r7,r8,df,f)
2247     else
2248       (let (r3,r4,r5,r6,r7,r8,df,f) = ppc_cheney_step (r3,r4,r7,r8,df,f) in
2249          ppc_cheney_loop (r3,r4,r5,r6,r7,r8,df,f)))``;
2250
2251val (th,def,pre) = compile "ppc" ``
2252  ppc_move_roots (r4,r5,r6:word32,r7,r8,r9,df,f) =
2253    (if r6 = 0x0w then
2254       (r4,r5,r6,r7,r8,r9,df,f)
2255     else
2256       (let r5 = f r9 in
2257        let (r4,r5,r7,r8,df,f) = ppc_move (r4,r5,r7,r8,df,f) in
2258        let r6 = r6 - 0x1w in
2259        let f = (r9 =+ r5) f in
2260        let r9 = r9 + 0x4w in
2261          ppc_move_roots (r4,r5,r6,r7,r8,r9,df,f)))``
2262
2263val (th,def,pre) = compile "ppc" ``
2264  ppc_c_init (r5:word32,r6:word32,r9:word32) =
2265    let r3 = r9 + 0x8w in
2266       if r5 = 0x1w then
2267          let r5 = r5 ?? 0x1w in
2268          let r3 = r3 + r6 in (r3,r5,r6,r9)
2269        else
2270          let r5 = r5 ?? 0x1w in (r3,r5,r6,r9)``
2271
2272val (th,def,pre) = compile "ppc" ``
2273  ppc_collect (r7,r8,r9,df,f) =
2274    (let r5 = f (r9 - 0x1Cw) in
2275     let r6 = f (r9 - 0x20w) in
2276     let (r3,r5,r6,r9) = ppc_c_init (r5,r6,r9) in
2277     let f = (r9 - 0x1Cw =+ r5) f in
2278     let r5 = r3 + r6 in
2279     let r4 = r3 in
2280     let f = (r9 + 0x4w =+ r5) f in
2281     let r6 = 0x6w in
2282     let r9 = r9 - 0x18w in
2283     let (r4,r5,r6,r7,r8,r9,df,f) = ppc_move_roots (r4,r5,r6,r7,r8,r9,df,f) in
2284     let (r3,r4,r5,r6,r7,r8,df,f) = ppc_cheney_loop (r3,r4,r5,r6,r7,r8,df,f) in
2285     let r4 = f (r9 + 0x4w) in
2286       (r3,r4,r5,r6,r7,r8,r9,df,f))``;
2287
2288val (th,def,pre) = compile "ppc" ``
2289  ppc_alloc_aux (r3,r4,r5,r6,r7,r8,r9,df,f) =
2290    (if r3 = r4 then
2291       (let (r3,r4,r5,r6,r7,r8,r9,df,f) = ppc_collect (r7,r8,r9,df,f) in
2292          (r3,r4,r5,r6,r7,r8,r9,df,f))
2293     else
2294       (r3,r4,r5,r6,r7,r8,r9,df,f))``;
2295
2296val (th,def,pre) = compile "ppc" ``
2297  ppc_alloc_aux2 (r3:word32,r4:word32,r9:word32,df:word32 set,f:word32->word32) =
2298    (let r7 = f (r9 - 0x18w) in
2299     let r8 = f (r9 - 0x14w) in
2300       (if r3 = r4 then
2301          (let r7 = 0x2w in
2302           let f = (r9 - 0x18w =+ r7) f in
2303           let f = (r9 =+ r3) f in (r3,r4,r7,r8,r9,df,f))
2304        else
2305          (let f = (r9 - 0x18w =+ r3) f in
2306           let f = (r3 =+ r7) f in
2307           let r3 = r3 + 0x4w in
2308           let f = (r3 =+ r8) f in
2309           let r3 = r3 + 0x4w in
2310           let f = (r9 =+ r3) f in
2311             (r3,r4,r7,r8,r9,df,f))))``;
2312
2313val (th,def,pre) = compile "ppc" ``
2314  ppc_alloc_mem (r5,r6,r7,r8,r9,df,f) =
2315    (let r3 = f r9 in
2316     let r4 = f (r9 + 0x4w) in
2317     let (r3,r4,r5,r6,r7,r8,r9,df,f) = ppc_alloc_aux (r3,r4,r5,r6,r7,r8,r9,df,f) in
2318     let (r3,r4,r7,r8,r9,df,f) = ppc_alloc_aux2 (r3,r4,r9,df,f) in
2319       (r3,r4,r5,r6,r7,r8,r9,df,f))``;
2320
2321val (th,def,pre) = compile "ppc" ``
2322  ppc_alloc (r3,r4,r5,r6,r7,r8,r9,df,f) =
2323     let f = (r9 - 0x18w =+ r3) f in
2324     let f = (r9 - 0x14w =+ r4) f in
2325     let f = (r9 - 0x10w =+ r5) f in
2326     let f = (r9 - 0xCw =+ r6) f in
2327     let f = (r9 - 0x8w =+ r7) f in
2328     let f = (r9 - 0x4w =+ r8) f in
2329     let (r3,r4,r5,r6,r7,r8,r9,df,f) = ppc_alloc_mem (r5,r6,r7,r8,r9,df,f) in
2330     let r3 = f (r9 - 0x18w) in
2331     let r4 = f (r9 - 0x14w) in
2332     let r5 = f (r9 - 0x10w) in
2333     let r6 = f (r9 - 0xCw) in
2334     let r7 = f (r9 - 0x8w) in
2335     let r8 = f (r9 - 0x4w) in
2336       (r3,r4,r5,r6,r7,r8,r9,df,f)``;
2337
2338val ppc_alloc_thm = save_thm("ppc_alloc_thm",th)
2339
2340
2341(* --- x86 --- *)
2342
2343val (th,def,pre) = compile "x86" ``
2344  x86_move (r1:word32,r2:word32,r4:word32,r5:word32,df:word32 set,f:word32->word32) =
2345    (if r2 && 3w = 0x0w then
2346       (let r4 = f r2 in
2347        let r5 = r4 && 3w in
2348          (if r5 = 0x1w then
2349             (let r2 = r4 - 0x1w in (r1,r2,r4,r5,df,f))
2350           else
2351             (let r5 = f (r2 + 0x4w) in
2352              let f = (r1 =+ r4) f in
2353              let r1 = r1 + 0x4w in
2354              let f = (r1 =+ r5) f in
2355              let r1 = r1 + 0x4w in
2356              let r4 = r1 - 0x7w in
2357              let f = (r2 =+ r4) f in
2358              let r2 = r4 - 0x1w in
2359                (r1,r2,r4,r5,df,f))))
2360     else
2361       (r1,r2,r4,r5,df,f))``
2362
2363val (th,def,pre) = compile "x86" ``
2364  x86_move2 (r1:word32,r3:word32,r4:word32,r5:word32,df:word32 set,f:word32->word32) =
2365    (if r3 && 0x3w = 0x0w then
2366       (let r4 = f r3 in
2367        let r5 = 0x3w && r4 in
2368          (if r5 = 0x1w then
2369             (let r3 = r4 - 0x1w in (r1,r3,r4,r5,df,f))
2370           else
2371             (let r5 = f (r3 + 0x4w) in
2372              let f = (r1 =+ r4) f in
2373              let r1 = r1 + 0x4w in
2374              let f = (r1 =+ r5) f in
2375              let r1 = r1 + 0x4w in
2376              let r4 = r1 - 0x7w in
2377              let f = (r3 =+ r4) f in
2378              let r3 = r4 - 0x1w in
2379                (r1,r3,r4,r5,df,f))))
2380     else
2381       (r1,r3,r4,r5,df,f))``
2382
2383val (th,def,pre) = compile "x86" ``
2384  x86_cheney_step (r0:word32,r1:word32,r4:word32,r5:word32,df:word32 set,f:word32->word32) =
2385    (let r2 = f r0 in
2386     let r3 = f (r0 + 0x4w) in
2387     let (r1,r2,r4,r5,df,f) = x86_move (r1,r2,r4,r5,df,f) in
2388     let (r1,r3,r4,r5,df,f) = x86_move2 (r1,r3,r4,r5,df,f) in
2389     let f = (r0 =+ r2) f in
2390     let r0 = r0 + 0x4w in
2391     let f = (r0 =+ r3) f in
2392     let r0 = r0 + 0x4w in
2393       (r0,r1,r2,r3,r4,r5,df,f))``;
2394
2395val (th,def,pre) = compile "x86" ``
2396  x86_cheney_loop (r0,r1,r2,r3,r4,r5,df,f) =
2397    (if r0 = r1 then
2398       (r0,r1,r2,r3,r4,r5,df,f)
2399     else
2400       (let (r0,r1,r2,r3,r4,r5,df,f) = x86_cheney_step (r0,r1,r4,r5,df,f) in
2401          x86_cheney_loop (r0,r1,r2,r3,r4,r5,df,f)))``;
2402
2403val (th,def,pre) = compile "x86" ``
2404  x86_move_roots (r1,r2,r3:word32,r4,r5,r6,df,f) =
2405    (if r3 = 0x0w then
2406       (r1,r2,r3,r4,r5,r6,df,f)
2407     else
2408       (let r2 = f r6 in
2409        let (r1,r2,r4,r5,df,f) = x86_move (r1,r2,r4,r5,df,f) in
2410        let r3 = r3 - 0x1w in
2411        let f = (r6 =+ r2) f in
2412        let r6 = r6 + 0x4w in
2413          x86_move_roots (r1,r2,r3,r4,r5,r6,df,f)))``
2414
2415val (th,def,pre) = compile "x86" ``
2416  x86_c_init (r2:word32,r3:word32,r6:word32) =
2417    let r0 = r6 + 0x8w in
2418       if r2 = 0x1w then
2419          let r2 = r2 ?? 0x1w in
2420          let r0 = r0 + r3 in (r0,r2,r3,r6)
2421        else
2422          let r2 = r2 ?? 0x1w in (r0,r2,r3,r6)``
2423
2424val (th,def,pre) = compile "x86" ``
2425  x86_collect (r4,r5,r6,df,f) =
2426    (let r2 = f (r6 - 0x1Cw) in
2427     let r3 = f (r6 - 0x20w) in
2428     let (r0,r2,r3,r6) = x86_c_init (r2,r3,r6) in
2429     let f = (r6 - 0x1Cw =+ r2) f in
2430     let r2 = r0 + r3 in
2431     let r1 = r0 in
2432     let f = (r6 + 0x4w =+ r2) f in
2433     let r3 = 0x6w in
2434     let r6 = r6 - 0x18w in
2435     let (r1,r2,r3,r4,r5,r6,df,f) = x86_move_roots (r1,r2,r3,r4,r5,r6,df,f) in
2436     let (r0,r1,r2,r3,r4,r5,df,f) = x86_cheney_loop (r0,r1,r2,r3,r4,r5,df,f) in
2437     let r1 = f (r6 + 0x4w) in
2438       (r0,r1,r2,r3,r4,r5,r6,df,f))``;
2439
2440val (th,def,pre) = compile "x86" ``
2441  x86_alloc_aux (r0,r1,r2,r3,r4,r5,r6,df,f) =
2442    (if r0 = r1 then
2443       (let (r0,r1,r2,r3,r4,r5,r6,df,f) = x86_collect (r4,r5,r6,df,f) in
2444          (r0,r1,r2,r3,r4,r5,r6,df,f))
2445     else
2446       (r0,r1,r2,r3,r4,r5,r6,df,f))``;
2447
2448val (th,def,pre) = compile "x86" ``
2449  x86_alloc_aux2 (r0:word32,r1:word32,r6:word32,df:word32 set,f:word32->word32) =
2450    (let r4 = f (r6 - 0x18w) in
2451     let r5 = f (r6 - 0x14w) in
2452       (if r0 = r1 then
2453          (let r4 = 0x2w in
2454           let f = (r6 - 0x18w =+ r4) f in
2455           let f = (r6 =+ r0) f in (r0,r1,r4,r5,r6,df,f))
2456        else
2457          (let f = (r6 - 0x18w =+ r0) f in
2458           let f = (r0 =+ r4) f in
2459           let r0 = r0 + 0x4w in
2460           let f = (r0 =+ r5) f in
2461           let r0 = r0 + 0x4w in
2462           let f = (r6 =+ r0) f in
2463             (r0,r1,r4,r5,r6,df,f))))``;
2464
2465val (th,def,pre) = compile "x86" ``
2466  x86_alloc_mem (r2,r3,r4,r5,r6,df,f) =
2467    (let r0 = f r6 in
2468     let r1 = f (r6 + 0x4w) in
2469     let (r0,r1,r2,r3,r4,r5,r6,df,f) = x86_alloc_aux (r0,r1,r2,r3,r4,r5,r6,df,f) in
2470     let (r0,r1,r4,r5,r6,df,f) = x86_alloc_aux2 (r0,r1,r6,df,f) in
2471       (r0,r1,r2,r3,r4,r5,r6,df,f))``;
2472
2473val (th,def,pre) = compile "x86" ``
2474  x86_alloc (r0,r1,r2,r3,r4,r5,r6,df,f) =
2475     let f = (r6 - 0x18w =+ r0) f in
2476     let f = (r6 - 0x14w =+ r1) f in
2477     let f = (r6 - 0x10w =+ r2) f in
2478     let f = (r6 - 0xCw =+ r3) f in
2479     let f = (r6 - 0x8w =+ r4) f in
2480     let f = (r6 - 0x4w =+ r5) f in
2481     let (r0,r1,r2,r3,r4,r5,r6,df,f) = x86_alloc_mem (r2,r3,r4,r5,r6,df,f) in
2482     let r0 = f (r6 - 0x18w) in
2483     let r1 = f (r6 - 0x14w) in
2484     let r2 = f (r6 - 0x10w) in
2485     let r3 = f (r6 - 0xCw) in
2486     let r4 = f (r6 - 0x8w) in
2487     let r5 = f (r6 - 0x4w) in
2488       (r0,r1,r2,r3,r4,r5,r6,df,f)``;
2489
2490val x86_alloc_thm = save_thm("x86_alloc_thm",th)
2491
2492fun prove_eq n1 n2 rw goal = prove(goal,
2493  STRIP_TAC \\ TAILREC_TAC \\ SIMP_TAC std_ss ([LET_DEF,word_arith_lemma1] @ rw)
2494  \\ SIMP_TAC std_ss [AC WORD_AND_ASSOC WORD_AND_COMM, AC WORD_ADD_ASSOC WORD_ADD_COMM]
2495  \\ COMPILER_TAC);
2496
2497val l1 = prove_eq "x86_move" "arm_move" []
2498  ``(x86_move = arm_move) /\ (x86_move_pre = arm_move_pre)``;
2499val l2 = prove_eq "x86_move2" "arm_move2" []
2500  ``(x86_move2 = arm_move2) /\ (x86_move2_pre = arm_move2_pre)``;
2501val l3 = prove_eq "x86_cheney_step" "arm_cheney_step" [l1,l2]
2502  ``(x86_cheney_step = arm_cheney_step) /\ (x86_cheney_step_pre = arm_cheney_step_pre)``;
2503val l4 = prove_eq "x86_cheney_loop" "arm_cheney_loop" [l3]
2504  ``(x86_cheney_loop = arm_cheney_loop) /\ (x86_cheney_loop_pre = arm_cheney_loop_pre)``;
2505val l5 = prove_eq "x86_move_roots" "arm_move_roots" [l4,l1,l2,l3]
2506  ``(x86_move_roots = arm_move_roots) /\ (x86_move_roots_pre = arm_move_roots_pre)``;
2507val l6 = prove_eq "x86_c_init" "arm_c_init" [l4,l1,l2,l3]
2508  ``(x86_c_init = arm_c_init) /\ (x86_c_init_pre = arm_c_init_pre)``;
2509val l7 = prove_eq "x86_collect" "arm_collect" [l1,l2,l3,l4,l5,l6]
2510  ``(x86_collect = arm_collect) /\ (x86_collect_pre = arm_collect_pre)``;
2511val l8 = prove_eq "x86_alloc_aux" "arm_alloc_aux" [l1,l2,l3,l4,l5,l6,l7]
2512  ``(x86_alloc_aux = arm_alloc_aux) /\ (x86_alloc_aux_pre = arm_alloc_aux_pre)``;
2513val l9 = prove_eq "x86_alloc_aux2" "arm_alloc_aux2" [l1,l2,l3,l4,l5,l6,l7,l8]
2514  ``(x86_alloc_aux2 = arm_alloc_aux2) /\ (x86_alloc_aux2_pre = arm_alloc_aux2_pre)``;
2515val lA = prove_eq "x86_alloc_mem" "arm_alloc_mem" [l1,l2,l3,l4,l5,l6,l7,l8,l9]
2516  ``(x86_alloc_mem = arm_alloc_mem) /\ (x86_alloc_mem_pre = arm_alloc_mem_pre)``;
2517val lB = prove_eq "x86_alloc" "arm_alloc" [l1,l2,l3,l4,l5,l6,l7,l8,l9,lA]
2518  ``(x86_alloc = arm_alloc) /\ (x86_alloc_pre = arm_alloc_pre)``;
2519
2520val x86_alloc_EQ = save_thm("x86_alloc_EQ",lB)
2521
2522val l1 = prove_eq "ppc_move" "arm_move" []
2523  ``(ppc_move = arm_move) /\ (ppc_move_pre = arm_move_pre)``;
2524val l2 = prove_eq "ppc_move2" "arm_move2" []
2525  ``(ppc_move2 = arm_move2) /\ (ppc_move2_pre = arm_move2_pre)``;
2526val l3 = prove_eq "ppc_cheney_step" "arm_cheney_step" [l1,l2]
2527  ``(ppc_cheney_step = arm_cheney_step) /\ (ppc_cheney_step_pre = arm_cheney_step_pre)``;
2528val l4 = prove_eq "ppc_cheney_loop" "arm_cheney_loop" [l3]
2529  ``(ppc_cheney_loop = arm_cheney_loop) /\ (ppc_cheney_loop_pre = arm_cheney_loop_pre)``;
2530val l5 = prove_eq "ppc_move_roots" "arm_move_roots" [l4,l1,l2,l3]
2531  ``(ppc_move_roots = arm_move_roots) /\ (ppc_move_roots_pre = arm_move_roots_pre)``;
2532val l6 = prove_eq "ppc_c_init" "arm_c_init" [l4,l1,l2,l3]
2533  ``(ppc_c_init = arm_c_init) /\ (ppc_c_init_pre = arm_c_init_pre)``;
2534val l7 = prove_eq "ppc_collect" "arm_collect" [l1,l2,l3,l4,l5,l6]
2535  ``(ppc_collect = arm_collect) /\ (ppc_collect_pre = arm_collect_pre)``;
2536val l8 = prove_eq "ppc_alloc_aux" "arm_alloc_aux" [l1,l2,l3,l4,l5,l6,l7]
2537  ``(ppc_alloc_aux = arm_alloc_aux) /\ (ppc_alloc_aux_pre = arm_alloc_aux_pre)``;
2538val l9 = prove_eq "ppc_alloc_aux2" "arm_alloc_aux2" [l1,l2,l3,l4,l5,l6,l7,l8]
2539  ``(ppc_alloc_aux2 = arm_alloc_aux2) /\ (ppc_alloc_aux2_pre = arm_alloc_aux2_pre)``;
2540val lA = prove_eq "ppc_alloc_mem" "arm_alloc_mem" [l1,l2,l3,l4,l5,l6,l7,l8,l9]
2541  ``(ppc_alloc_mem = arm_alloc_mem) /\ (ppc_alloc_mem_pre = arm_alloc_mem_pre)``;
2542val lB = prove_eq "ppc_alloc" "arm_alloc" [l1,l2,l3,l4,l5,l6,l7,l8,l9,lA]
2543  ``(ppc_alloc = arm_alloc) /\ (ppc_alloc_pre = arm_alloc_pre)``;
2544
2545val ppc_alloc_EQ = save_thm("ppc_alloc_EQ",lB)
2546
2547
2548val _ = export_theory();
2549