1
2open HolKernel Parse boolLib bossLib; val _ = new_theory "lisp_cons";
3val _ = ParseExtras.temp_loose_equality()
4
5open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory;
6open combinTheory finite_mapTheory addressTheory helperLib;
7open set_sepTheory bitTheory fcpTheory;
8
9open stop_and_copyTheory;
10open codegenLib decompilerLib prog_x64Lib prog_x64Theory;
11
12infix \\
13val op \\ = op THEN;
14val RW = REWRITE_RULE;
15val RW1 = ONCE_REWRITE_RULE;
16fun SUBGOAL q = REVERSE (sg q)
17
18(*
19  r9 = temp
20  r11 = i
21  r12 = j
22  r15 = to heap base
23  r6 = from heap base
24*)
25
26val (thm,mc_move_def) = decompile_io_strings x64_tools "mc_move"
27  (SOME (``(r6:word64,r8:word64,r10:word64,r12:word64,r15:word64,df:word64 set,f:word64->word32)``,
28         ``(r6:word64,r8:word64,r10:word64,r12:word64,r15:word64,df:word64 set,f:word64->word32)``))
29  (assemble "x64" `
30     test r8d,1
31     jne L2
32     mov r9,[4*r8+r6]
33     cmp r9d,r10d
34     je L1
35     mov [4*r12+r15],r9
36     mov [4*r8+r6],r10d
37     mov [4*r8+r6+4],r12d
38     mov r8,r12
39     add r12,2
40     jmp L2
41L1:  shr r9,32
42     mov r8,r9
43L2:  `)
44
45val (thm,mc_move2_def) = decompile_io_strings x64_tools "mc_move2"
46  (SOME (``(r6:word64,r13:word64,r10:word64,r12:word64,r15:word64,df:word64 set,f:word64->word32)``,
47         ``(r6:word64,r13:word64,r10:word64,r12:word64,r15:word64,df:word64 set,f:word64->word32)``))
48  (assemble "x64" `
49     test r13d,1
50     jne L2
51     mov r9,[4*r13+r6]
52     cmp r9d,r10d
53     je L1
54     mov [4*r12+r15],r9
55     mov [4*r13+r6],r10d
56     mov [4*r13+r6+4],r12d
57     mov r13,r12
58     add r12,2
59     jmp L2
60L1:  shr r9,32
61     mov r13,r9
62L2:  `)
63
64val (thm,mc_gc_step_def) = decompile_io_strings x64_tools "mc_gc_step"
65  (SOME (``(r6:word64,r10:word64,r11:word64,r12:word64,r15:word64,df:word64 set,f:word64->word32)``,
66         ``(r6:word64,r10:word64,r11:word64,r12:word64,r15:word64,df:word64 set,f:word64->word32)``))
67  (assemble "x64" `
68     mov r8d,[4*r11+r15]
69     mov r13d,[4*r11+r15+4]
70     insert mc_move
71     insert mc_move2
72     mov [4*r11+r15],r8d
73     mov [4*r11+r15+4],r13d
74     add r11,2
75     `);
76
77val (thm,mc_gc_loop_def) = decompile_io_strings x64_tools "mc_gc_loop"
78  (SOME (``(r6:word64,r10:word64,r11:word64,r12:word64,r15:word64,df:word64 set,f:word64->word32)``,
79         ``(r6:word64,r10:word64,r11:word64,r12:word64,r15:word64,df:word64 set,f:word64->word32)``))
80  (assemble "x64" `
81     jmp L2
82L1:  insert mc_gc_step
83L2:  cmp r11,r12
84     jne L1`);
85
86val (thm,mc_move_list_def) = decompile_io_strings x64_tools "mc_move_list"
87  (SOME (``(r6:word64,r10:word64,r12:word64,r14:word64,r15:word64,df:word64 set,f:word64->word32)``,
88         ``(r6:word64,r8:word64,r10:word64,r12:word64,r14:word64,r15:word64,df:word64 set,f:word64->word32)``))
89  (assemble "x64" `
90     jmp L2
91L1:  insert mc_move
92     mov [r14],r8d
93     lea r14,[r14+4]
94L2:  mov r8d,[r14]
95     cmp r8d,r10d
96     jne L1`);
97
98val (thm,mc_gc_def) = decompile_io_strings x64_tools "mc_gc"
99  (SOME (``(r6:word64,r14:word64,r15:word64,df:word64 set,f:word64->word32)``,
100         ``(r6:word64,r11:word64,r15:word64,df:word64 set,f:word64->word32)``))
101  (assemble "x64" `
102     xor r10,r10
103     xor r11,r11
104     xor r12,r12
105     not r10d
106     insert mc_move_list
107     insert mc_gc_loop
108     xchg r6,r15
109     `);
110
111val (thm,mc_full_gc_def) = decompile_io_strings x64_tools "mc_full_gc"
112  (SOME (``(r3:word64,r6:word64,r7:word64,r8:word64,r9:word64,r10:word64,r11:word64,r12:word64,r13:word64,r14:word64,df:word64 set,f:word64->word32)``,
113         ``(r3:word64,r6:word64,r7:word64,r8:word64,r9:word64,r10:word64,r11:word64,r12:word64,r13:word64,r14:word64,r15:word64,df:word64 set,f:word64->word32)``))
114  (assemble "x64" `
115     lea r14,[r7+4*r3-24]
116     mov r15,[r7-232]
117     mov [r14],r8d
118     mov [r14+4],r9d
119     mov [r14+8],r10d
120     mov [r14+12],r11d
121     mov [r14+16],r12d
122     mov [r14+20],r13d
123     insert mc_gc
124     mov [r7-232],r15
125     mov r14,r11
126     lea r15,[r7+4*r3-24]
127     mov r8d,[r15]
128     mov r9d,[r15+4]
129     mov r10d,[r15+8]
130     mov r11d,[r15+12]
131     mov r12d,[r15+16]
132     mov r13d,[r15+20]
133     mov r15,[r7-240]
134     add r15,r15
135     `);
136
137val _ = save_thm("mc_full_thm",thm);
138
139
140val SET_TAC =
141  FULL_SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_UNION,IN_DELETE,SUBSET_DEF,
142    DISJOINT_DEF,NOT_IN_EMPTY,EXTENSION,IN_INSERT,IN_INTER,IN_DIFF,IN_UNIV]
143  \\ METIS_TAC [PAIR_EQ];
144
145val RANGE_TAC = FULL_SIMP_TAC std_ss [RANGE_def,IN_DEF,gc_inv_def] \\ DECIDE_TAC
146
147val ref_addr_def = Define `ref_addr k n = n2w (8 * n + k):word64`;
148
149val ref_heap_addr_def = Define `
150  (ref_heap_addr (H_ADDR a) = (n2w a << 1):word32) /\
151  (ref_heap_addr (H_DATA (INL (w:word30))) = w2w w << 2 !! 1w) /\
152  (ref_heap_addr (H_DATA (INR (v:29 word))) = w2w v << 3 !! 3w)`;
153
154val ONE32 = ``0xFFFFFFFFw:word32``;
155val ONE64 = ``0xFFFFFFFFw:word64``;
156
157val word_LSL_n2w = prove(
158  ``!m k. ((n2w m):'a word) << k = n2w (m * 2 ** k)``,
159  SIMP_TAC std_ss [AC MULT_ASSOC MULT_COMM,WORD_MUL_LSL,word_mul_n2w]);
160
161val ref_heap_addr_NOT_ONE32 = prove(
162  ``!x. ~(ref_heap_addr x = ^ONE32)``,
163  Cases \\ REPEAT (Cases_on `a`)
164  \\ ASM_SIMP_TAC std_ss [ref_heap_addr_def,w2n_n2w,w2w_def]
165  \\ Q.SPEC_TAC (`(n2w n):word32`,`w`)
166  \\ blastLib.BBLAST_TAC);
167
168val ref_heap_addr_and_1 = prove(
169  ``(w2w (w2w (ref_heap_addr (H_ADDR a)) && 1w:word64) = 0w:word32) /\
170    ~(w2w (w2w (ref_heap_addr (H_DATA b)) && 1w:word64) = 0w:word32)``,
171  Cases_on `b` \\ ASM_SIMP_TAC std_ss [ref_heap_addr_def]
172  \\ blastLib.BBLAST_TAC);
173
174val ADDR_SIMP_LEMMA = prove(
175  ``!a b. (w2w (0x4w * a + b && 0x3w:word64) = 0x0w:word32) = (b && 3w = 0w)``,
176  blastLib.BBLAST_TAC);
177
178val ADDR_SIMP_LEMMA2 = prove(
179  ``!b. ((b + 4w) && 3w = 0w) = (b && 3w = 0w:word64)``,
180  blastLib.BBLAST_TAC);
181
182val ADDR_w2w_ALIGNED = prove(
183  ``!b. ((w2w (3w && b:word64) = 0w:word32) = (b && 3w = 0w:word64)) /\
184        ((w2w (b && 3w:word64) = 0w:word32) = (b && 3w = 0w:word64)) /\
185        (((b+4w) && 3w = 0w) = (b && 3w = 0w:word64))``,
186  REPEAT STRIP_TAC \\ blastLib.BBLAST_TAC);
187
188val ADDR_SIMP = store_thm("ADDR_SIMP",
189  ``!a b.
190      ((w2w (0x4w * a + b && 0x3w:word64) = 0x0w:word32) = (b && 3w = 0w)) /\
191      ((w2w (0x4w * a + b + 4w && 0x3w:word64) = 0x0w:word32) = (b && 3w = 0w))``,
192  METIS_TAC [ADDR_SIMP_LEMMA,ADDR_SIMP_LEMMA2,WORD_ADD_ASSOC]);
193
194val ref_aux_def = Define `
195  (ref_aux a H_EMP = SEP_EXISTS x y. one (a:word64,x) * one (a+4w,y)) /\
196  (ref_aux a (H_REF n) = one (a,^ONE32) * one (a+4w,n2w n << 1)) /\
197  (ref_aux a (H_BLOCK (xs,l,())) =
198     one (a,ref_heap_addr(HD xs)) * one (a+4w,ref_heap_addr(HD (TL xs))))`;
199
200val ref_mem_def = Define `
201  (ref_mem a m b 0 = emp) /\
202  (ref_mem a m b (SUC e) =
203     if e < b then emp else ref_aux (a + n2w (8 * e)) (m e) * ref_mem a m b e)`;
204
205val ref_mem_EQ_EMP = prove(
206  ``!e a m. ref_mem a m e e = emp``,
207  Cases \\ SIMP_TAC std_ss [ref_mem_def]);
208
209val ref_mem_SPLIT = prove(
210  ``!b e i m.
211      RANGE(b,e)i ==>
212      (ref_mem a m b e = ref_mem a m b i * ref_mem a m i e)``,
213  Induct_on `e` THEN1 (SIMP_TAC std_ss [RANGE_def])
214  \\ REPEAT STRIP_TAC \\ Cases_on `i = e` \\ `~(e<b)` by RANGE_TAC
215  \\ ASM_SIMP_TAC std_ss [ref_mem_EQ_EMP,AC STAR_ASSOC STAR_COMM,SEP_CLAUSES,ref_mem_def]
216  \\ `RANGE (b,e) i /\ ~(e < i)` by RANGE_TAC \\ RES_TAC
217  \\ ASM_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM]);
218
219val ref_mem_RANGE = store_thm("ref_mem_RANGE",
220  ``!m b e i.
221      RANGE(b,e)i ==>
222      (ref_mem a m b e = ref_mem a m b i * ref_aux (a + n2w (8 * i)) (m i) *
223                         ref_mem a m (SUC i) e)``,
224  REPEAT STRIP_TAC \\ IMP_RES_TAC ref_mem_SPLIT
225  \\ ASM_SIMP_TAC std_ss [GSYM STAR_ASSOC] \\ AP_TERM_TAC
226  \\ POP_ASSUM (K ALL_TAC) \\ POP_ASSUM MP_TAC
227  \\ Induct_on `e` THEN1 (SIMP_TAC std_ss [RANGE_def])
228  \\ REPEAT STRIP_TAC \\ Cases_on `e = i` THEN1
229   (ASM_SIMP_TAC std_ss [ref_mem_EQ_EMP]
230    \\ ASM_SIMP_TAC std_ss [ref_mem_def,ref_mem_EQ_EMP])
231  \\ ASM_SIMP_TAC std_ss [ref_mem_def,ref_mem_EQ_EMP]
232  \\ `~(e < i) /\ ~(e < SUC i) /\ RANGE (b,e) i` by RANGE_TAC
233  \\ ASM_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM]);
234
235val ref_mem_IGNORE = prove(
236  ``!e i b m a. ~RANGE(b,e)i ==> (ref_mem a ((i =+ x) m) b e = ref_mem a m b e)``,
237  Induct \\ SIMP_TAC std_ss [ref_mem_def]
238  \\ REPEAT STRIP_TAC \\ Cases_on `e < b` \\ ASM_SIMP_TAC std_ss []
239  \\ `~(i = e) /\ ~RANGE (b,e) i` by RANGE_TAC \\ RES_TAC
240  \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM]);
241
242val ref_mem_UPDATE = store_thm("ref_mem_UPDATE",
243  ``!m b e i.
244      RANGE(b,e)i ==>
245      (ref_mem a ((i =+ x) m) b e =
246       ref_mem a m b i *
247       ref_aux (a + n2w (8 * i)) x *
248       ref_mem a m (SUC i) e)``,
249  REPEAT STRIP_TAC \\ IMP_RES_TAC ref_mem_RANGE
250  \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM]
251  \\ `~RANGE(b,i)i /\ ~RANGE(SUC i,e)i` by RANGE_TAC
252  \\ ASM_SIMP_TAC std_ss [ref_mem_IGNORE]);
253
254val memory_ok_def = Define `
255  memory_ok m =
256    !i xs n d. (m i = H_BLOCK (xs,n,d)) ==> (n = 0) /\ (LENGTH xs = 2)`;
257
258val w2w_SUB_EQ = prove(
259  ``!x y. (w2w (x - y:word64) = 0w:word32) = (w2w x = (w2w y):word32)``,
260  blastLib.BBLAST_TAC);
261
262val ref_heap_addr_H_ADDR = prove(
263  ``n < 2147483648 ==>
264    (0x4w * w2w (ref_heap_addr (H_ADDR n)) = n2w (8 * n))``,
265  REPEAT STRIP_TAC \\ `2 * n < 4294967296` by DECIDE_TAC
266  \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [ref_heap_addr_def,WORD_MUL_LSL,
267       word_mul_n2w,w2w_def,w2n_n2w,MULT_ASSOC]);
268
269val word_32_32_def = Define `
270  word_32_32 (x:word32) (y:word32) = w2w y << 32 !! (w2w x):word64`;
271
272val w2w_word_32_32 = prove(
273  ``!x y. (w2w (word_32_32 x y) = x) /\
274          (word_32_32 x y >>> 32 = w2w y) /\
275          ((31 >< 0) (word_32_32 x y) = x) /\
276          ((63 >< 32) (word_32_32 x y) = y)``,
277  SIMP_TAC std_ss [word_32_32_def] \\ blastLib.BBLAST_TAC);
278
279val memory_ok_REF = prove(
280  ``!m k n. memory_ok m ==> memory_ok ((n =+ H_REF k) m)``,
281  SIMP_TAC std_ss [memory_ok_def,APPLY_UPDATE_THM] \\ REPEAT STRIP_TAC
282  \\ Cases_on `n = i` \\ FULL_SIMP_TAC (srw_ss()) [] \\ METIS_TAC []);
283
284val memory_ok_BLOCK = prove(
285  ``memory_ok m /\ (LENGTH xs = 2) /\ (n = 0) ==>
286    memory_ok ((i =+ H_BLOCK (xs,n,d)) m)``,
287  SIMP_TAC std_ss [memory_ok_def,APPLY_UPDATE_THM] \\ REPEAT STRIP_TAC
288  \\ Cases_on `i = i'` \\ FULL_SIMP_TAC (srw_ss()) [] \\ METIS_TAC []);
289
290val mc_move_thm = prove(
291  ``(split_move (x,j,mF,mT,e) = (T,x2,j2,mF2,mT2)) /\
292    memory_ok mF /\ memory_ok mT /\ e < 2**31 /\ (r6 && 3w = 0w) /\ (r15 && 3w = 0w) ==>
293    (ref_mem r6 mF 0 e * ref_mem r15 mT 0 e * p) (fun2set (f,df)) ==>
294    ?fi.
295      memory_ok mF2 /\ memory_ok mT2 /\
296      mc_move_pre (r6,w2w (ref_heap_addr x),^ONE64,n2w (2 * j),r15,df,f) /\
297      (mc_move (r6,w2w (ref_heap_addr x),^ONE64,n2w (2 * j),r15,df,f) =
298         (r6,w2w (ref_heap_addr x2),^ONE64,n2w (2 * j2),r15,df,fi)) /\
299      (ref_mem r6 mF2 0 e * ref_mem r15 mT2 0 e * p) (fun2set (fi,df))``,
300  REVERSE (Cases_on `x`) \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN1
301   (SIMP_TAC std_ss [split_move_def] \\ ONCE_REWRITE_TAC [mc_move_def]
302    \\ SIMP_TAC std_ss [ref_heap_addr_and_1])
303  \\ SIMP_TAC std_ss [ALIGNED64]
304  \\ SIMP_TAC std_ss [split_move_def] \\ ONCE_REWRITE_TAC [RW [ADDR_SIMP] mc_move_def]
305  \\ SIMP_TAC std_ss [GSYM word_32_32_def]
306  \\ SIMP_TAC std_ss [ref_heap_addr_and_1,w2w_SUB_EQ]
307  \\ Cases_on `mF n` \\ ASM_SIMP_TAC (srw_ss()) [] THEN1
308   (STRIP_TAC
309    \\ `RANGE(0,e)n` by RANGE_TAC
310    \\ IMP_RES_TAC ref_mem_RANGE
311    \\ ASM_SIMP_TAC std_ss [STAR_ASSOC,ref_aux_def,SEP_CLAUSES]
312    \\ `n < 2147483648` by IMP_RES_TAC LESS_TRANS
313    \\ ASM_SIMP_TAC std_ss [ref_heap_addr_H_ADDR]
314    \\ REPEAT STRIP_TAC \\ SEP_R_TAC
315    \\ SIMP_TAC std_ss [LET_DEF,w2w_word_32_32]
316    \\ SIMP_TAC (srw_ss()) []
317    \\ FULL_SIMP_TAC (std_ss++star_ss) [w2w_word_32_32,ref_heap_addr_def]
318    \\ FULL_SIMP_TAC std_ss [ALIGNED64])
319  \\ `?xs nn d. p' = (xs,nn,d)` by METIS_TAC [PAIR]
320  \\ ASM_SIMP_TAC (srw_ss()) [LET_DEF]
321  \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [w2w_word_32_32]
322  \\ `(nn = 0) /\ (LENGTH xs = 2)` by METIS_TAC [memory_ok_def]
323  \\ `n < 2147483648` by IMP_RES_TAC LESS_TRANS
324  \\ ASM_SIMP_TAC std_ss [ref_heap_addr_H_ADDR]
325  \\ SIMP_TAC std_ss [word_mul_n2w,MULT_ASSOC]
326  \\ `RANGE(0,e)n` by RANGE_TAC
327  \\ IMP_RES_TAC ref_mem_RANGE
328  \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`mF`,`r6`])
329  \\ Q.PAT_X_ASSUM `RANGE (0,e) n` (K ALL_TAC)
330  \\ `RANGE(0,e)j` by RANGE_TAC
331  \\ IMP_RES_TAC ref_mem_RANGE
332  \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`mT`,`r15`])
333  \\ ASM_SIMP_TAC std_ss [ref_aux_def,oneTheory.one,SEP_CLAUSES,STAR_ASSOC]
334  \\ SIMP_TAC std_ss [SEP_EXISTS_THM] \\ STRIP_TAC
335  \\ SEP_R_TAC \\ SIMP_TAC std_ss [EVAL ``-1w:word32``,ref_heap_addr_NOT_ONE32]
336  \\ SIMP_TAC std_ss [ref_heap_addr_def,WORD_MUL_LSL,word_mul_n2w]
337  \\ FULL_SIMP_TAC std_ss [ALIGNED64]
338  \\ `w2w (n2w (2 * j):word32) = n2w (2 * j):word64` by
339   (`(2 * j) < 4294967296` by DECIDE_TAC
340    \\ ASM_SIMP_TAC (srw_ss()) [ref_heap_addr_def,WORD_MUL_LSL,word_mul_n2w,
341       w2w_def,w2n_n2w])
342  \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC
343  THEN1 METIS_TAC [memory_ok_REF]
344  THEN1 METIS_TAC [memory_ok_BLOCK]
345  THEN1 (ASM_SIMP_TAC (srw_ss()) [word_add_n2w]
346         \\ AP_THM_TAC \\ AP_TERM_TAC \\ DECIDE_TAC)
347  \\ `RANGE(0,e)j /\ RANGE(0,e)n` by RANGE_TAC
348  \\ IMP_RES_TAC ref_mem_UPDATE
349  \\ ASM_SIMP_TAC std_ss [ref_aux_def,STAR_ASSOC]
350  \\ SIMP_TAC (std_ss++SIZES_ss) [w2w_n2w,WORD_MUL_LSL,word_mul_n2w]
351  \\ SEP_W_TAC);
352
353val mc_move2_thm = prove(
354  ``(mc_move2 = mc_move) /\ (mc_move2_pre = mc_move_pre)``,
355  SIMP_TAC std_ss [mc_move2_def,mc_move_def,FUN_EQ_THM,FORALL_PROD]);
356
357val SELECT_32_LEMMA = prove(
358  ``!w. (31 -- 0) (w2w (w:word32)):word64 = w2w w``,
359  blastLib.BBLAST_TAC);
360
361val w2w_w2w_LEMMA = prove(
362  ``!w. w2w ((w2w w):word64) = w:word32``,
363  blastLib.BBLAST_TAC);
364
365val mc_gc_step_thm = prove(
366  ``(split_gc_step (i,j,mF,mT,e) = (T,i2,j2,mF2,mT2)) /\
367    memory_ok mF /\ memory_ok mT /\ e < 2**31 /\ (r6 && 3w = 0w) /\ (r15 && 3w = 0w) ==>
368    (ref_mem r6 mF 0 e * ref_mem r15 mT 0 e * p) (fun2set (f,df)) ==>
369    ?r9i fi.
370      memory_ok mF2 /\ memory_ok mT2 /\
371      mc_gc_step_pre (r6,^ONE64,n2w (2 * i),n2w (2 * j),r15,df,f) /\
372      (mc_gc_step (r6,^ONE64,n2w (2 * i),n2w (2 * j),r15,df,f) =
373                  (r6,^ONE64,n2w (2 * i2),n2w (2 * j2),r15,df,fi)) /\
374      (ref_mem r6 mF2 0 e * ref_mem r15 mT2 0 e * p) (fun2set (fi,df))``,
375  ONCE_REWRITE_TAC [EQ_SYM_EQ]
376  \\ SIMP_TAC std_ss [split_gc_step_def]
377  \\ `?xs n d. getBLOCK (mT i) = (xs,n,d)` by METIS_TAC [PAIR]
378  \\ ASM_SIMP_TAC std_ss [LET_DEF]
379  \\ `?c3 ys3 j3 mF3 mT3. split_move_list (xs,j,mF,mT,e) = (c3,ys3,j3,mF3,mT3)` by
380       METIS_TAC [PAIR]
381  \\ ASM_SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [Q.ISPEC `0w` EQ_SYM_EQ]
382  \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [oneTheory.one]
383  \\ `mT i = H_BLOCK (xs,n,())` by
384    (Cases_on `mT i` \\ FULL_SIMP_TAC (srw_ss()) [isBLOCK_def,getBLOCK_def])
385  \\ `(n = 0) /\ (LENGTH xs = 2)` by METIS_TAC [memory_ok_def]
386  \\ `?x1 x2. xs = [x1;x2]` by
387   (Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH]
388    \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH]
389    \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH,CONS_11,ADD1])
390  \\ Q.PAT_X_ASSUM `xxx = (T,ys3,j3,mF3,mT3)` (MP_TAC o GSYM)
391  \\ ASM_SIMP_TAC std_ss [split_move_list_def]
392  \\ `?c5 x5 j5 mF5 mT5. split_move (x1,j,mF,mT,e) = (c5,x5,j5,mF5,mT5)` by METIS_TAC [PAIR]
393  \\ `?c6 x6 j6 mF6 mT6. split_move (x2,j5,mF5,mT5,e) = (c6,x6,j6,mF6,mT6)` by METIS_TAC [PAIR]
394  \\ ASM_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC
395  \\ SIMP_TAC std_ss [RW [ADDR_SIMP] mc_gc_step_def,word_mul_n2w,MULT_ASSOC]
396  \\ `(n2w (8 * i) + r15) IN df /\ (n2w (8 * i) + r15 + 4w) IN df /\
397      (f (n2w (8 * i) + r15) = ref_heap_addr x1) /\
398      (f (n2w (8 * i) + r15 + 4w) = ref_heap_addr x2)` by
399   (POP_ASSUM MP_TAC
400    \\ `RANGE(0,e)i` by RANGE_TAC
401    \\ IMP_RES_TAC ref_mem_RANGE
402    \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`mT`,`r15`])
403    \\ FULL_SIMP_TAC std_ss [ref_mem_UPDATE] \\ POP_ASSUM (K ALL_TAC)
404    \\ FULL_SIMP_TAC std_ss [ref_aux_def,HD,TL,AC WORD_ADD_ASSOC WORD_ADD_COMM]
405    \\ REPEAT STRIP_TAC \\ SEP_R_TAC)
406  \\ FULL_SIMP_TAC std_ss [SELECT_32_LEMMA]
407  \\ SIMP_TAC std_ss [LET_DEF]
408  \\ ASSUME_TAC (GEN_ALL mc_move_thm)
409  \\ SEP_I_TAC "mc_move"
410  \\ Q.PAT_X_ASSUM `split_move (x1,j,mF,mT,e) = (T,x5,j5,mF5,mT5)` MP_TAC
411  \\ SEP_I_TAC "split_move"
412  \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
413  \\ Q.PAT_X_ASSUM `!p.bbb` (MP_TAC o Q.SPEC `p`)
414  \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC
415  \\ ASM_SIMP_TAC std_ss [LET_DEF,mc_move2_thm]
416  \\ ASSUME_TAC (GEN_ALL (Q.INST [`x2`|->`x99`] mc_move_thm))
417  \\ SEP_I_TAC "mc_move"
418  \\ Q.PAT_X_ASSUM `split_move (x2,j5,mF5,mT5,e) = (T,x6,j6,mF6,mT6)` MP_TAC
419  \\ SEP_I_TAC "split_move"
420  \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
421  \\ Q.PAT_X_ASSUM `!p.bbb` (MP_TAC o Q.SPEC `p`)
422  \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC
423  \\ ASM_SIMP_TAC std_ss [memory_ok_BLOCK,LENGTH]
424  \\ FULL_SIMP_TAC std_ss [ALIGNED64]
425  \\ STRIP_TAC THEN1 SIMP_TAC std_ss [word_add_n2w,LEFT_ADD_DISTRIB]
426  \\ `RANGE(0,e)i` by RANGE_TAC
427  \\ ASM_SIMP_TAC std_ss [ref_mem_UPDATE,ref_aux_def,HD,TL,STAR_ASSOC]
428  \\ ASM_SIMP_TAC std_ss [w2w_w2w_LEMMA]
429  \\ IMP_RES_TAC ref_mem_RANGE
430  \\ POP_ASSUM (ASSUME_TAC o Q.SPECL [`mT6`,`r15`])
431  \\ Q.PAT_X_ASSUM `mT6 i = nnnn` ASSUME_TAC
432  \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,ref_aux_def,HD,TL]
433  \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM]
434  \\ SEP_W_TAC);
435
436val mc_gc_loop_thm = prove(
437  ``!j mF mT f i2 mF2 mT2.
438      memory_ok mF /\ memory_ok mT /\ e < 2**31 /\ (r6 && 3w = 0w) /\ (r15 && 3w = 0w) ==>
439      (split_gc_loop (i,j,mF,mT,e) = (T,i2,mF2,mT2)) ==>
440      (ref_mem r6 mF 0 e * ref_mem r15 mT 0 e * p) (fun2set (f,df)) ==>
441      ?r9i fi.
442        memory_ok mF2 /\ memory_ok mT2 /\
443        mc_gc_loop1_pre (r6,^ONE64,n2w (2 * i),n2w (2 * j),r15,df,f) /\
444        (mc_gc_loop1 (r6,^ONE64,n2w (2 * i),n2w (2 * j),r15,df,f) =
445                     (r6,^ONE64,n2w (2 * i2),n2w (2 * i2),r15,df,fi)) /\
446        (ref_mem r6 mF2 0 e * ref_mem r15 mT2 0 e * p) (fun2set (fi,df))``,
447  Induct_on `e-i` \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN1
448   (ONCE_REWRITE_TAC [split_gc_loop_def] \\ NTAC 10 STRIP_TAC
449    \\ Cases_on `i = j` \\ ASM_SIMP_TAC std_ss []
450    THEN1 (ONCE_REWRITE_TAC [mc_gc_loop_def] \\ ASM_SIMP_TAC std_ss [])
451    \\ Cases_on `i < j` \\ ASM_SIMP_TAC std_ss []
452    \\ Cases_on `j <= e` \\ ASM_SIMP_TAC std_ss []
453    \\ `F` by DECIDE_TAC)
454  \\ ONCE_REWRITE_TAC [split_gc_loop_def] \\ NTAC 10 STRIP_TAC
455  \\ Cases_on `i = j` \\ ASM_SIMP_TAC std_ss []
456  THEN1 (ONCE_REWRITE_TAC [mc_gc_loop_def] \\ ASM_SIMP_TAC std_ss [])
457  \\ Cases_on `i < j` \\ ASM_SIMP_TAC std_ss []
458  \\ Cases_on `j <= e` \\ ASM_SIMP_TAC std_ss []
459  \\ ONCE_REWRITE_TAC [Q.ISPEC `0w` EQ_SYM_EQ]
460  \\ ONCE_REWRITE_TAC [mc_gc_loop_def] \\ STRIP_TAC
461  \\ `?c4 i4 j4 mF4 mT4. split_gc_step (i,j,mF,mT,e) = (c4,i4,j4,mF4,mT4)`
462        by METIS_TAC [PAIR]
463  \\ ASSUME_TAC (GEN_ALL mc_gc_step_thm)
464  \\ SEP_I_TAC "split_gc_step"
465  \\ SEP_I_TAC "mc_gc_step"
466  \\ POP_ASSUM MP_TAC
467  \\ ASM_SIMP_TAC std_ss [LET_DEF]
468  \\ `?c5 i5 mF5 mT5. split_gc_loop (i4,j4,mF4,mT4,e) = (c5,i5,mF5,mT5)` by METIS_TAC [PAIR]
469  \\ Cases_on `c4` \\ Cases_on `c5` \\ ASM_SIMP_TAC std_ss []
470  \\ STRIP_TAC \\ POP_ASSUM (MP_TAC o Q.SPEC `p`)
471  \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC
472  \\ FULL_SIMP_TAC std_ss []
473  \\ `e - i4 = v` by
474   (SUBGOAL `i4 = i+1` THEN1 DECIDE_TAC
475    \\ Q.PAT_X_ASSUM `split_gc_step xxx = yyyy` (MP_TAC o GSYM)
476    \\ FULL_SIMP_TAC std_ss [split_gc_step_def,LET_DEF]
477    \\ CONV_TAC (DEPTH_CONV (helperLib.FORCE_PBETA_CONV))
478    \\ ASM_SIMP_TAC std_ss []
479    \\ Cases_on `mT i` \\ ASM_SIMP_TAC (srw_ss()) [isBLOCK_def]
480    \\ Cases_on `p'` \\ Cases_on `r`
481    \\ FULL_SIMP_TAC std_ss [getBLOCK_def] \\ METIS_TAC [memory_ok_def])
482  \\ Q.PAT_X_ASSUM `!ee ii. bbb` (MP_TAC o Q.SPECL [`e`,`i4`])
483  \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC
484  \\ Q.PAT_X_ASSUM `split_gc_loop xxx = yyy` MP_TAC
485  \\ SEP_I_TAC "split_gc_loop"
486  \\ SEP_I_TAC "mc_gc_loop1"
487  \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
488  \\ Q.PAT_X_ASSUM `bbb ==> ccc` MP_TAC \\ ASM_SIMP_TAC std_ss []
489  \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss []
490  \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11]
491  \\ `2 * i < 18446744073709551616` by DECIDE_TAC
492  \\ `2 * j < 18446744073709551616` by DECIDE_TAC
493  \\ `~(2 * i = 2 * j)` by DECIDE_TAC
494  \\ ASM_SIMP_TAC std_ss []);
495
496val mc_gc_loop1_THM = prove(
497  ``(mc_gc_loop1 = mc_gc_loop) /\ (mc_gc_loop1_pre = mc_gc_loop_pre)``,
498  REPEAT STRIP_TAC \\ SIMP_TAC std_ss [FUN_EQ_THM,FORALL_PROD]
499  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
500  \\ SIMP_TAC std_ss [Once mc_gc_loop_def,LET_DEF]
501  \\ CONV_TAC (DEPTH_CONV (helperLib.FORCE_PBETA_CONV))
502  \\ SIMP_TAC std_ss []);
503
504val ref_stack_def = Define `
505  (ref_stack a [] = one (a:word64,^ONE32)) /\
506  (ref_stack a (x::xs) = one (a,ref_heap_addr x) * ref_stack (a+4w) xs)`;
507
508val mc_move_list1_THM = prove(
509  ``(mc_move_list1 = mc_move_list) /\ (mc_move_list1_pre = mc_move_list_pre)``,
510  REPEAT STRIP_TAC \\ SIMP_TAC std_ss [FUN_EQ_THM,FORALL_PROD]
511  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
512  \\ SIMP_TAC std_ss [Once mc_move_list_def,LET_DEF]
513  \\ CONV_TAC (DEPTH_CONV (helperLib.FORCE_PBETA_CONV))
514  \\ SIMP_TAC std_ss []);
515
516val mc_move_list_thm = prove(
517  ``!xs r14 j mF mT f i2 mF2 mT2 xs2 p.
518      memory_ok mF /\ memory_ok mT /\ e < 2**31 /\ (r6 && 3w = 0w) /\ (r15 && 3w = 0w) /\ (r14 && 3w = 0w) ==>
519      (split_move_list (xs,j,mF,mT,e) = (T,xs2,i2,mF2,mT2)) ==>
520      (ref_mem r6 mF 0 e * ref_mem r15 mT 0 e * ref_stack r14 xs * p) (fun2set (f,df)) ==>
521      ?fi r8i r14i.
522        memory_ok mF2 /\ memory_ok mT2 /\
523        mc_move_list_pre (r6,^ONE64,n2w (2 * j),r14,r15,df,f) /\
524        (mc_move_list (r6,^ONE64,n2w (2 * j),r14,r15,df,f) =
525                      (r6,r8i,^ONE64,n2w (2 * i2),r14i,r15,df,fi)) /\
526        (ref_mem r6 mF2 0 e * ref_mem r15 mT2 0 e * ref_stack r14 xs2 * p) (fun2set (fi,df))``,
527  SIMP_TAC std_ss [GSYM mc_move_list1_THM] \\ Induct THEN1
528   (ONCE_REWRITE_TAC [EQ_SYM_EQ]
529    \\ ONCE_REWRITE_TAC [Q.ISPEC `0w` EQ_SYM_EQ]
530    \\ SIMP_TAC std_ss [split_move_list_def,ref_stack_def]
531    \\ ONCE_REWRITE_TAC [mc_move_list_def]
532    \\ SIMP_TAC std_ss [w2w_SUB_EQ,SELECT_32_LEMMA,LET_DEF,w2w_w2w_LEMMA]
533    \\ REPEAT STRIP_TAC \\ SEP_R_TAC
534    \\ ASM_SIMP_TAC (srw_ss()) [w2w_n2w,ADDR_w2w_ALIGNED])
535  \\ ONCE_REWRITE_TAC [EQ_SYM_EQ]
536  \\ ONCE_REWRITE_TAC [Q.ISPEC `0w` EQ_SYM_EQ]
537  \\ NTAC 12 STRIP_TAC
538  \\ SIMP_TAC std_ss [split_move_list_def]
539  \\ `?c5 h5 j5 mF5 mT5. split_move (h,j,mF,mT,e) = (c5,h5,j5,mF5,mT5)` by METIS_TAC [PAIR]
540  \\ `?c6 xs6 j6 mF6 mT6. split_move_list (xs,j5,mF5,mT5,e) = (c6,xs6,j6,mF6,mT6)` by METIS_TAC [PAIR]
541  \\ ASM_SIMP_TAC std_ss [LET_DEF] \\ STRIP_TAC
542  \\ FULL_SIMP_TAC std_ss [ref_stack_def,STAR_ASSOC] \\ REPEAT STRIP_TAC
543  \\ ONCE_REWRITE_TAC [mc_move_list_def]
544  \\ SIMP_TAC std_ss [w2w_SUB_EQ,SELECT_32_LEMMA,LET_DEF,w2w_w2w_LEMMA]
545  \\ SEP_R_TAC \\ SIMP_TAC std_ss [EVAL ``(w2w ^ONE64):word32``]
546  \\ SIMP_TAC std_ss [ref_heap_addr_NOT_ONE32]
547  \\ ASSUME_TAC (GEN_ALL mc_move_thm)
548  \\ SEP_I_TAC "mc_move"
549  \\ Q.PAT_X_ASSUM `split_move xxx = yyy` MP_TAC
550  \\ SEP_I_TAC "split_move"
551  \\ REPEAT STRIP_TAC
552  \\ FULL_SIMP_TAC std_ss [w2w_0]
553  \\ Q.PAT_X_ASSUM `!p. bbb ==> ccc`
554       (MP_TAC o Q.SPEC `one (r14,ref_heap_addr h) * ref_stack (r14 + 0x4w) xs * p`)
555  \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ REPEAT STRIP_TAC
556  \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,w2w_w2w_LEMMA] \\ SEP_W_TAC
557  \\ SEP_I_TAC "mc_move_list1"
558  \\ Q.PAT_X_ASSUM `split_move_list xxx = yyy` MP_TAC
559  \\ SEP_I_TAC "split_move_list"
560  \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
561  \\ Q.PAT_X_ASSUM `!p. bbb ==> ccc`
562       (MP_TAC o Q.SPEC `one (r14,ref_heap_addr h5) * p`)
563  \\ FULL_SIMP_TAC (std_ss++star_ss) [ADDR_w2w_ALIGNED] \\ REPEAT STRIP_TAC
564  \\ ASM_SIMP_TAC std_ss [] \\ SEP_R_TAC);
565
566val ref_mem_CUT = prove(
567  ``!e b a m s p. (p * ref_mem a m b e) s ==> (p * ref_mem a (CUT(x,y)m) b e) s``,
568  Induct \\ SIMP_TAC std_ss [ref_mem_def] \\ REPEAT STRIP_TAC
569  \\ Cases_on `e<b` \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] \\ RES_TAC
570  \\ FULL_SIMP_TAC std_ss [CUT_def]
571  \\ Cases_on `RANGE(x,y)e` \\ FULL_SIMP_TAC std_ss []
572  \\ Cases_on `m e`
573  \\ FULL_SIMP_TAC std_ss [ref_aux_def,SEP_CLAUSES,SEP_EXISTS_THM]
574  THEN1 METIS_TAC [] THEN1 METIS_TAC []
575  \\ Cases_on `p'` \\ Cases_on `r`
576  \\ FULL_SIMP_TAC std_ss [ref_aux_def,SEP_CLAUSES,SEP_EXISTS_THM,oneTheory.one]
577  \\ METIS_TAC []);
578
579val mc_gc_thm = store_thm("mc_gc_thm",
580  ``memory_ok mF /\ memory_ok mT /\ e < 2**31 /\ (r6 && 3w = 0w) /\ (r15 && 3w = 0w) /\ (r14 && 3w = 0w) ==>
581    (split_gc (xs,mF,mT,e) = (T,i2,xs2,mT2,e)) ==>
582    (ref_mem r6 mF 0 e * ref_mem r15 mT 0 e * ref_stack r14 xs * p) (fun2set (f,df)) ==>
583    ?fi.
584      memory_ok mT2 /\ mc_gc_pre (r6,r14,r15,df,f) /\
585      (mc_gc (r6,r14,r15,df,f) = (r15,n2w (2 * i2),r6,df,fi)) /\
586      (ref_mem r6 (\x.H_EMP) 0 e * ref_mem r15 mT2 0 e * ref_stack r14 xs2 * p) (fun2set (fi,df))``,
587  STRIP_TAC \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [split_gc_def]
588  \\ `?c6 xs6 j6 mF6 mT6. split_move_list (xs,0,mF,mT,e) = (c6,xs6,j6,mF6,mT6)` by METIS_TAC [PAIR]
589  \\ `?c7 i7 mF7 mT7. split_gc_loop (0,j6,mF6,mT6,e) = (c7,i7,mF7,mT7)` by METIS_TAC [PAIR]
590  \\ ASM_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
591  \\ SIMP_TAC std_ss [mc_gc_def,LET_DEF,EVAL ``(31 -- 0) (~0x0w):word64``]
592  \\ ASSUME_TAC (RW [MULT_CLAUSES] (SUBST_INST [``j:num``|->``0:num``] (GEN_ALL mc_move_list_thm)))
593  \\ SEP_I_TAC "mc_move_list"
594  \\ Q.PAT_X_ASSUM `split_move_list xxx=yyy` MP_TAC
595  \\ SEP_I_TAC "split_move_list"
596  \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
597  \\ Q.PAT_X_ASSUM `!p.bb` (MP_TAC o Q.SPEC `p`)
598  \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC
599  \\ ASM_SIMP_TAC std_ss []
600  \\ ASSUME_TAC (RW [MULT_CLAUSES] (SUBST_INST [``i:num``|->``0:num``] (GEN_ALL mc_gc_loop_thm)))
601  \\ FULL_SIMP_TAC std_ss [mc_gc_loop1_THM]
602  \\ SEP_I_TAC "mc_gc_loop"
603  \\ Q.PAT_X_ASSUM `split_gc_loop xxx=yyy` MP_TAC
604  \\ SEP_I_TAC "split_gc_loop"
605  \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
606  \\ Q.PAT_X_ASSUM `!r6.bb` (MP_TAC o Q.SPECL [`ref_stack r14 xs6 * p`])
607  \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ REPEAT STRIP_TAC
608  \\ ASM_SIMP_TAC std_ss []
609  \\ REPEAT STRIP_TAC
610  THEN1 (SIMP_TAC std_ss [memory_ok_def,CUT_EQ] \\ METIS_TAC [memory_ok_def])
611  \\ `(\x. H_EMP) = CUT (0,0) mF7` by
612    (SIMP_TAC std_ss [CUT_def,FUN_EQ_THM,IN_DEF,RANGE_def])
613  \\ FULL_SIMP_TAC std_ss [STAR_ASSOC]
614  \\ `((p * ref_stack r14 xs6 * ref_mem r15 mT7 0 e) *
615       ref_mem r6 mF7 0 e) (fun2set (fi',df))` by FULL_SIMP_TAC (std_ss++star_ss) []
616  \\ `((p * ref_stack r14 xs6 * ref_mem r15 mT7 0 e) *
617       ref_mem r6 (CUT (0,0) mF7) 0 e) (fun2set (fi',df))` by
618         (MATCH_MP_TAC ref_mem_CUT \\ FULL_SIMP_TAC (std_ss++star_ss) [])
619  \\ `((p * ref_stack r14 xs6 * ref_mem r6 (CUT (0,0) mF7) 0 e) *
620       ref_mem r15 (CUT (0,i7) mT7) 0 e) (fun2set (fi',df))` by
621         (MATCH_MP_TAC ref_mem_CUT \\ FULL_SIMP_TAC (std_ss++star_ss) [])
622  \\ FULL_SIMP_TAC (std_ss++star_ss) []);
623
624val word64_3232_def = Define `
625  word64_3232 (w:word64) = (w2w w, w2w (w >>> 32)):word32 # word32`;
626
627val word3232_64_def = Define `
628  word3232_64 ((w0,w1):word32 # word32) = w2w w1 << 32 !! w2w w0`;
629
630val ref_static_def = Define `
631  (ref_static a [] = emp) /\
632  (ref_static a (x::xs) =
633     let (w0,w1) = word64_3232 x in
634       one (a,w0) * one (a+4w,w1) * ref_static (a+8w) xs)`;
635
636val ref_stack_space_def = Define `
637  (ref_stack_space sp 0 = emp) /\
638  (ref_stack_space sp (SUC n) =
639     ref_stack_space (sp-4w) n * SEP_EXISTS w. one (sp:word64-4w,w:word32))`;
640
641val ok_split_heap_def = Define `
642  ok_split_heap (roots,m,i,e) =
643    i <= e /\ ADDR_SET roots UNION D1 m SUBSET D0 m /\ memory_ok m /\ (R0 m = {}) /\
644    !k. i <= k ==> (m k = H_EMP)`;
645
646val RANGE_LEMMA = prove(
647  ``(RANGE (0,0) = {}) /\
648    (RANGE (0,SUC i) = i INSERT RANGE (0,i))``,
649  SIMP_TAC std_ss [EXTENSION,IN_INSERT,NOT_IN_EMPTY]
650  \\ SIMP_TAC std_ss [RANGE_def,IN_DEF] \\ DECIDE_TAC);
651
652val IMP_part_heap = prove(
653  ``memory_ok m /\ b <= e ==> ?t. part_heap b e m t``,
654  Induct_on `e-b` \\ REPEAT STRIP_TAC
655  THEN1 (`e = b` by DECIDE_TAC \\ METIS_TAC [part_heap_cases])
656  \\ ONCE_REWRITE_TAC [part_heap_cases]
657  \\ `(v = e - (b+1)) /\ b+1<=e /\ ~(b = e)` by DECIDE_TAC \\ RES_TAC
658  \\ Cases_on `m b` \\ FULL_SIMP_TAC (srw_ss()) [isBLOCK_def]
659  \\ Cases_on `p` \\ Cases_on `r` \\ FULL_SIMP_TAC std_ss [memory_ok_def]
660  \\ Q.EXISTS_TAC `t` \\ RES_TAC \\ FULL_SIMP_TAC std_ss []
661  \\ SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF,RANGE_def] \\ REPEAT STRIP_TAC
662  \\ `F` by DECIDE_TAC);
663
664val IN_D0 = SIMP_CONV bool_ss [IN_DEF, D0_def] ``x IN D0 m``
665val IN_D1 = (REWRITE_CONV [IN_DEF] THENC SIMP_CONV bool_ss [D1_def])
666                ``x IN D1 m``
667
668val ok_split_heap = store_thm("ok_split_heap",
669  ``!roots m i e.
670      ok_split_heap (roots,m,i,e) =
671      memory_ok m /\ ?h. ok_full_heap (h,roots) (0,i,e,e,e + e,m)``,
672  REPEAT STRIP_TAC \\ SIMP_TAC std_ss [ok_split_heap_def,ok_full_heap_def]
673  \\ REVERSE EQ_TAC \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] THEN1
674   (FULL_SIMP_TAC std_ss [RANGE_def,NOT_LESS,UNION_SUBSET,ok_heap_def]
675    \\ REPEAT STRIP_TAC THEN1
676     (FULL_SIMP_TAC std_ss [SUBSET_DEF] \\ REPEAT STRIP_TAC \\ RES_TAC
677      \\ FULL_SIMP_TAC std_ss [ref_heap_mem_def]
678      \\ FULL_SIMP_TAC std_ss [IN_DEF,D0_def,R0_def,EXTENSION,NOT_IN_EMPTY]
679      \\ SRW_TAC [] [] \\ METIS_TAC [PAIR])
680    THEN1
681     (ASM_SIMP_TAC std_ss [SUBSET_DEF,IN_DEF,D0_def]
682      \\ FULL_SIMP_TAC std_ss [D1_def,ref_heap_mem_def,SUBSET_DEF]
683      \\ REPEAT STRIP_TAC
684      \\ Cases_on `k IN FDOM h` \\ FULL_SIMP_TAC (srw_ss()) []
685      \\ FULL_SIMP_TAC std_ss [POINTERS_def,IN_UNIV,GSPECIFICATION]
686      \\ `x IN FDOM h` by METIS_TAC []
687      \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [PAIR])
688    \\ FULL_SIMP_TAC std_ss [SUBSET_DEF] \\ REPEAT STRIP_TAC \\ RES_TAC
689    \\ FULL_SIMP_TAC std_ss [ref_heap_mem_def]
690    \\ FULL_SIMP_TAC std_ss [IN_DEF,D0_def,R0_def,EXTENSION,NOT_IN_EMPTY]
691    \\ SRW_TAC [] [])
692  \\ FULL_SIMP_TAC std_ss [RANGE_def,NOT_LESS]
693  \\ Q.EXISTS_TAC `FUN_FMAP (\a. getBLOCK (m a)) (D0 m)`
694  \\ `FINITE (D0 m)` by
695   (`D0 m = D0 m INTER RANGE(0,i)` by
696      (SIMP_TAC std_ss [EXTENSION,IN_INTER]
697       \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC
698       \\ ASM_SIMP_TAC std_ss []
699       \\ SIMP_TAC std_ss [IN_DEF,RANGE_def] \\ CCONTR_TAC
700       \\ FULL_SIMP_TAC std_ss [NOT_LESS] \\ RES_TAC
701       \\ FULL_SIMP_TAC (srw_ss()) [IN_DEF,D0_def])
702    \\ POP_ASSUM (fn th => ONCE_REWRITE_TAC [th])
703    \\ MATCH_MP_TAC FINITE_INTER \\ DISJ2_TAC
704    \\ REPEAT (POP_ASSUM (K ALL_TAC))
705    \\ Induct_on `i`
706    \\ ASM_SIMP_TAC std_ss [RANGE_LEMMA,FINITE_EMPTY,FINITE_INSERT])
707  \\ REPEAT STRIP_TAC
708  THEN1 (METIS_TAC [IMP_part_heap,DECIDE ``0<=m:num``])
709  THEN1
710   (ASM_SIMP_TAC std_ss [ref_heap_mem_def,FUN_FMAP_DEF]
711    \\ STRIP_TAC \\ Cases_on `a IN D0 m` \\ ASM_SIMP_TAC std_ss []
712    \\ FULL_SIMP_TAC std_ss [EXTENSION,NOT_IN_EMPTY]
713    \\ FULL_SIMP_TAC std_ss [D0_def,IN_DEF,getBLOCK_def,R0_def]
714    \\ Cases_on `m a` \\ FULL_SIMP_TAC (srw_ss()) [] \\ POP_ASSUM MP_TAC
715    \\ FULL_SIMP_TAC (srw_ss()) [] \\ METIS_TAC [PAIR])
716  THEN1
717   (ASM_SIMP_TAC std_ss [ref_heap_mem_def,
718      FUN_FMAP_DEF,ok_heap_def,UNION_SUBSET,POINTERS_def]
719    \\ ASM_SIMP_TAC std_ss [SUBSET_DEF,GSPECIFICATION,IN_UNIV]
720    \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC
721    \\ ASM_SIMP_TAC std_ss [FUN_FMAP_DEF,ADDR_SET_def,GSPECIFICATION]
722    \\ FULL_SIMP_TAC std_ss [UNION_SUBSET]
723    \\ FULL_SIMP_TAC std_ss [IN_D0,getBLOCK_def,SUBSET_DEF,IN_D1]
724    \\ FULL_SIMP_TAC std_ss [ADDR_SET_def,GSPECIFICATION]
725    \\ FULL_SIMP_TAC std_ss [IN_D0,getBLOCK_def,SUBSET_DEF]
726    \\ FULL_SIMP_TAC std_ss [IN_D1,ADDR_SET_def,GSPECIFICATION]
727    \\ METIS_TAC []));
728
729val _ = export_theory();
730