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