1 2open HolKernel boolLib bossLib Parse; val _ = new_theory "arm_improved_gc"; 3 4open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 5open combinTheory finite_mapTheory addressTheory helperLib; 6open set_sepTheory bitTheory; 7 8open improved_gcTheory; 9open compilerLib; 10 11infix \\ 12val op \\ = op THEN; 13val RW = REWRITE_RULE; 14val RW1 = ONCE_REWRITE_RULE; 15fun SUBGOAL q = REVERSE (sg q) 16 17 18val _ = codegen_x86Lib.set_x86_regs 19 [(1,"eax"),(2,"ecx"),(3,"edx"),(4,"ebx"),(5,"edi"),(6,"esi"),(7,"ebp")] 20 21val (th,arm_move_loop_def,arm_move_loop_pre_def) = compile "arm" `` 22 arm_move_loop (r2:word32,r3:word32,r4:word32,df:word32 set,f:word32->word32) = 23 if r4 = 0w then (r2,r3,r4,df,f) else 24 let r5 = f r2 in 25 let r4 = r4 - 1w in 26 let r2 = r2 + 4w in 27 let f = (r3 =+ r5) f in 28 let r3 = r3 + 4w in 29 arm_move_loop (r2,r3,r4,df,f)``; 30 31val (th,arm_move_def,arm_move_pre_def) = compile "arm" `` 32 arm_move (r1:word32,r2:word32,r3:word32,df:word32 set,f:word32->word32) = 33 if ~(r2 && 3w = 0w) then (r1,r3,df,f) else 34 let r4 = f r2 in 35 if r4 && 3w = 0w then 36 let f = (r1 =+ r4) f in 37 (r1,r3,df,f) 38 else 39 let f = (r1 =+ r3) f in 40 let f = (r3 =+ r4) f in 41 let f = (r2 =+ r3) f in 42 let r4 = r4 >>> 10 in 43 let r3 = r3 + 4w in 44 let r2 = r2 + 4w in 45 let (r2,r3,r4,df,f) = arm_move_loop (r2,r3,r4,df,f) in 46 (r1,r3,df,f)`` 47 48val (th,arm_move_list_def,arm_move_list_pre_def) = compile "arm" `` 49 arm_move_list (r1:word32,r3:word32,r6:word32,df:word32 set,f:word32->word32) = 50 if r6 = 0w then (r1,r3,df,f) else 51 let r2 = f r1 in 52 let r6 = r6 - 1w in 53 let (r1,r3,df,f) = arm_move (r1,r2,r3,df,f) in 54 let r1 = r1 + 4w in 55 arm_move_list (r1,r3,r6,df,f)`` 56 57val (th,arm_loop_def,arm_loop_pre_def) = compile "arm" `` 58 arm_loop (r1:word32,r3:word32,df:word32 set,f:word32->word32) = 59 if r1 = r3 then (r1,df,f) else 60 let r2 = f r1 in 61 let r6 = r2 >>> 10 in 62 let r1 = r1 + 4w in 63 if r2 && 1w = 0w then 64 let r6 = r6 << 2 in 65 let r1 = r1 + r6 in 66 arm_loop (r1,r3,df,f) 67 else 68 let (r1,r3,df,f) = arm_move_list (r1,r3,r6,df,f) in 69 arm_loop (r1,r3,df,f)`` 70 71val (th,arm_move_roots_def,arm_move_roots_pre_def) = compile "arm" `` 72 arm_move_roots (r1:word32,r3:word32,df:word32 set,f:word32->word32) = 73 let r2 = f r1 in 74 if r2 = 2w then (r3,df,f) else 75 let (r1,r3,df,f) = arm_move (r1,r2,r3,df,f) in 76 let r1 = r1 - 4w in 77 arm_move_roots (r1,r3,df,f)`` 78 79val (th,arm_gc_def,arm_gc_pre_def) = compile "arm" `` 80 arm_gc (r1:word32,r7:word32,df:word32 set,f:word32->word32) = 81 let r3 = f (r7 + 48w) in 82 let r5 = f (r7 + 52w) in 83 let r2 = f (r7 + 44w) in 84 let r4 = f (r7 + 40w) in 85 let f = (r7 + 40w =+ r3) f in 86 let f = (r7 + 44w =+ r5) f in 87 let f = (r7 + 48w =+ r4) f in 88 let f = (r7 + 52w =+ r2) f in 89 let (r3,df,f) = arm_move_roots (r1,r3,df,f) in 90 let r1 = f (r7 + 40w) in 91 let (r1,df,f) = arm_loop (r1,r3,df,f) in 92 (r1,r7,df,f)`` 93 94 95val SET_TAC = 96 FULL_SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_UNION,IN_DELETE,SUBSET_DEF, 97 DISJOINT_DEF,NOT_IN_EMPTY,EXTENSION,IN_INSERT,IN_INTER,IN_DIFF,IN_UNIV] 98 \\ METIS_TAC [PAIR_EQ]; 99 100val RANGE_TAC = FULL_SIMP_TAC std_ss [RANGE_def,IN_DEF,gc_inv_def] \\ DECIDE_TAC 101 102val ref_addr_def = Define `ref_addr n = n2w (4 * n):word32`; 103 104val ref_heap_addr_def = Define ` 105 (ref_heap_addr (H_DATA w) = n2w (w2n (w:31 word) * 2 + 1)) /\ 106 (ref_heap_addr (H_ADDR a) = ref_addr a)`; 107 108val one_list_def = Define ` 109 (one_list a [] = emp) /\ 110 (one_list a (x::xs) = one (a,x) * one_list (a + 4w) xs)`; 111 112val one_list_roots_def = Define ` 113 (one_list_roots a [] = one (a,2w)) /\ 114 (one_list_roots a (x::xs) = one_list_roots (a - 4w) xs * one (a,ref_heap_addr x))`; 115 116val ref_tag_def = Define ` 117 ref_tag (n,b,t:word8) = n2w (n * 1024 + w2n t * 4 + 2 + (if b then 1 else 0)) :word32`; 118 119val ref_aux_def = Define ` 120 (ref_aux a H_EMP = SEP_EXISTS x. one (a:word32,x)) /\ 121 (ref_aux a (H_REF n) = one (a,ref_addr n)) /\ 122 (ref_aux a (H_BLOCK (xs,l,(b,d,ys))) = 123 let zs = (if d then MAP ref_heap_addr xs else ys) in 124 one (a,ref_tag (LENGTH zs,d,b)) * one_list (a+4w) zs)`; 125 126val ref_mem_def = tDefine "ref_mem" ` 127 (ref_mem m a e = 128 if e <= a then cond (a = e) else 129 ref_aux (ref_addr a) (m a) * ref_mem m (a + MAX 1 (getLENGTH (m a))) e)` 130 (WF_REL_TAC `measure (\(m,a,e). e - a)` 131 \\ SIMP_TAC std_ss [MAX_DEF] \\ DECIDE_TAC) 132 133val ALIGNED_ref_addr = prove( 134 ``!n. ALIGNED (ref_addr n)``, 135 SIMP_TAC std_ss [ALIGNED_n2w,ref_addr_def,RW1[MULT_COMM]MOD_EQ_0]); 136 137val ref_addr_and_3 = prove( 138 ``!n m. ref_addr m + n2w n && 3w = n2w (n MOD 4)``, 139 SIMP_TAC std_ss [ref_addr_def,word_add_n2w,n2w_and_3, 140 MATCH_MP (RW1[MULT_COMM]MOD_TIMES) (DECIDE``0<4:num``)]); 141 142val ref_addr_NEQ = prove( 143 ``!i j. ~(ref_addr i = ref_addr j + 1w) /\ 144 ~(ref_addr i = ref_addr j + 2w) /\ 145 ~(ref_addr i = ref_addr j + 3w)``, 146 REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [] 147 \\ MATCH_MP_TAC (METIS_PROVE [] ``~(x && 3w = y && 3w) ==> ~(x = y)``) 148 \\ SIMP_TAC (std_ss++SIZES_ss) [ref_addr_and_3,n2w_11, 149 SIMP_RULE std_ss [WORD_ADD_0] (Q.SPEC `0` ref_addr_and_3)]); 150 151val ref_tag_lsr = prove( 152 ``n < 2 ** 22 ==> (ref_tag (n,b,t) >>> 10 = n2w n)``, 153 SIMP_TAC (std_ss++SIZES_ss) [ref_tag_def,LEFT_ADD_DISTRIB, 154 GSYM ADD_ASSOC,word_add_n2w,DECIDE ``8 * (n * 2) = 16 * n:num``, 155 SIMP_CONV std_ss [word_lsr_n2w,word_bits_n2w,BITS_THM] ``n2w n >>> k``] 156 \\ ASSUME_TAC (Q.ISPEC `t:word8` w2n_lt) \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [] 157 \\ `w2n t * 4 + (2 + if b then 1 else 0) < 1024` by (Cases_on `b` \\ DECIDE_TAC) 158 \\ IMP_RES_TAC DIV_MULT \\ ASM_SIMP_TAC std_ss []); 159 160val MAX_LEMMA = prove( 161 ``MAX 1 (n + 1) = n + 1``, 162 FULL_SIMP_TAC std_ss [MAX_DEF] \\ DECIDE_TAC); 163 164val ref_heap_addr_NEQ_2 = prove( 165 ``!x. ~(ref_heap_addr x = 2w)``, 166 Cases \\ MATCH_MP_TAC (METIS_PROVE [] ``~(v && 3w = w && 3w) ==> ~(v = w:word32)``) 167 \\ SIMP_TAC (std_ss++SIZES_ss) [ref_heap_addr_def,n2w_11,ref_addr_def] 168 \\ SIMP_TAC std_ss [n2w_and_3,DECIDE ``4*n = n*4``,MOD_EQ_0] THEN1 EVAL_TAC 169 \\ MATCH_MP_TAC (METIS_PROVE [] ``~(w && 1w = v && 1w) ==> ~(w = v)``) 170 \\ SIMP_TAC std_ss [n2w_and_1] \\ SIMP_TAC bool_ss [DECIDE ``4=2*2``] 171 \\ SIMP_TAC bool_ss [MATCH_MP MOD_MULT_MOD (DECIDE ``0<2 /\ 0<2``)] 172 \\ SIMP_TAC std_ss [MATCH_MP MOD_MULT (DECIDE ``1 < 2``)] \\ EVAL_TAC); 173 174val ok_memory_def = Define ` 175 ok_memory m = 176 !(a:num) l (xs:(31 word) heap_address list) b:word8 t:bool ys:word32 list. 177 (m a = H_BLOCK (xs,l,(b,t,ys))) ==> 178 LENGTH xs < 2 ** 22 /\ LENGTH ys < 2 ** 22 /\ 179 if t then l = LENGTH xs else (l = LENGTH ys) /\ (xs = [])`; 180 181val ref_addr_ADD1 = prove( 182 ``!i j. (ref_addr (i + 1) = ref_addr i + 4w) /\ 183 (ref_addr (i + j) = ref_addr i + ref_addr j)``, 184 SIMP_TAC std_ss [ref_addr_def,LEFT_ADD_DISTRIB,word_add_n2w]); 185 186val ref_mem_IGNORE = prove( 187 ``~(RANGE (b2,e2) j) ==> 188 (ref_mem ((j =+ x) m) b2 e2 = ref_mem m b2 e2)``, 189 completeInduct_on `e2-b2` \\ REPEAT STRIP_TAC 190 \\ ONCE_REWRITE_TAC [ref_mem_def] 191 \\ Cases_on `e2<=b2` \\ ASM_SIMP_TAC std_ss [] 192 \\ `~(b2 = j)` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 193 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM] 194 \\ Q.ABBREV_TAC `y = MAX 1 (getLENGTH (m b2))` 195 \\ `0 < y` by (Q.UNABBREV_TAC `y` \\ SIMP_TAC std_ss [MAX_DEF]) 196 \\ `e2 - (b2 + y) < e2 - b2` by DECIDE_TAC 197 \\ `~RANGE (b2+y,e2) j` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 198 \\ RES_TAC \\ METIS_TAC []); 199 200val ref_mem_LESS = prove( 201 ``!j e. j < e ==> !m. ref_mem m j e = 202 ref_aux (ref_addr j) (m j) * 203 ref_mem m (j + MAX 1 (getLENGTH (m j))) e``, 204 METIS_TAC [DECIDE ``j<e = ~(e<=j:num)``,ref_mem_def]); 205 206val arm_move_loop_thm = store_thm("arm_move_loop_thm", 207 ``!xs ys r2 r3 r5:word32 f p. 208 (one_list r2 xs * one_list r3 ys * p) (fun2set (f,df)) /\ 209 (LENGTH ys = LENGTH xs) /\ LENGTH xs < 2 ** 23 /\ ALIGNED r2 /\ ALIGNED r3 ==> 210 ?r2i r3i fi. 211 arm_move_loop_pre (r2,r3,n2w (LENGTH xs),df,f) /\ 212 (arm_move_loop (r2,r3,n2w (LENGTH xs),df,f) = 213 (r2i,r3 + n2w (4 * LENGTH xs),0w,df,fi)) /\ 214 (one_list r2 xs * one_list r3 xs * p) (fun2set (fi,df))``, 215 Induct \\ REPEAT STRIP_TAC 216 \\ PURE_ONCE_REWRITE_TAC [arm_move_loop_def,arm_move_loop_pre_def] 217 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 218 THEN1 (Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,WORD_ADD_0] \\ `F` by DECIDE_TAC) 219 \\ `?z zs. ys = z::zs` by 220 (Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,CONS_11]) 221 \\ FULL_SIMP_TAC std_ss [] \\ `LENGTH (h::xs) < 4294967296` by DECIDE_TAC 222 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LENGTH,DECIDE ``~(SUC n = 0)``,MULT_CLAUSES] 223 \\ ASM_SIMP_TAC std_ss [LET_DEF,GSYM word_add_n2w,WORD_ADD_SUB,ADD1] 224 \\ FULL_SIMP_TAC std_ss [one_list_def,LET_DEF,ALIGNED_INTRO] 225 \\ `(f r2 = h) /\ r2 IN df /\ r3 IN df` by SEP_READ_TAC 226 \\ FULL_SIMP_TAC std_ss [WORD_ADD_ASSOC] 227 \\ SIMP_TAC std_ss [prove(``one(r2,h)*y*(x2*y2)*p = y*y2*(p*x2*one(r2,h))``, 228 SIMP_TAC (std_ss++star_ss) [])] 229 \\ Q.PAT_X_ASSUM `!ys.bbb` MATCH_MP_TAC \\ Q.EXISTS_TAC `zs` 230 \\ FULL_SIMP_TAC std_ss [ALIGNED] \\ REPEAT STRIP_TAC 231 THEN1 SEP_WRITE_TAC \\ DECIDE_TAC); 232 233val ref_mem_one_list = prove( 234 ``!k a. k <= e - a /\ (!i. i < k ==> (m (a + i) = H_EMP)) ==> 235 (ref_mem m a e = SEP_EXISTS ts. cond (LENGTH ts = k) * 236 one_list (ref_addr a) ts * ref_mem m (a + k) e)``, 237 Induct \\ REPEAT STRIP_TAC THEN1 238 SIMP_TAC std_ss [FUN_EQ_THM,SEP_CLAUSES,SEP_EXISTS_THM, 239 cond_STAR,GSYM STAR_ASSOC,LENGTH_NIL,one_list_def] 240 \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [ref_mem_def])) 241 \\ `~(e <= a)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 242 \\ `0 < SUC k` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 243 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [getLENGTH_def,ref_aux_def,SEP_CLAUSES] 244 \\ POP_ASSUM (K ALL_TAC) 245 \\ Q.PAT_X_ASSUM `!a.bb /\ bbbb ==> bbb` (ASSUME_TAC o Q.SPEC `a+1`) 246 \\ `k <= e - (a + 1)` by DECIDE_TAC 247 \\ `(!i. i < k ==> (m ((a + 1) + i) = H_EMP))` by 248 (REPEAT STRIP_TAC \\ `1 + i < SUC k` by DECIDE_TAC \\ METIS_TAC [ADD_ASSOC]) 249 \\ Q.PAT_X_ASSUM `bb ==> bbb` MP_TAC \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES] 250 \\ REPEAT STRIP_TAC 251 \\ SIMP_TAC (std_ss++sep_cond_ss) [FUN_EQ_THM,SEP_CLAUSES,SEP_EXISTS_THM,cond_STAR] 252 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 253 (Q.EXISTS_TAC `x'::ts` 254 \\ ASM_SIMP_TAC std_ss [LENGTH,one_list_def,ADD1,LEFT_ADD_DISTRIB] 255 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC ADD_ASSOC ADD_COMM, 256 word_arith_lemma1,ref_addr_ADD1] \\ DECIDE_TAC) 257 \\ Cases_on `ts` \\ FULL_SIMP_TAC bool_ss [LENGTH] THEN1 `F` by DECIDE_TAC 258 \\ Q.LIST_EXISTS_TAC [`h`,`t`] 259 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC ADD_ASSOC ADD_COMM, 260 word_arith_lemma1,ref_addr_ADD1,one_list_def,ADD1] \\ DECIDE_TAC); 261 262val part_heap_ref_mem_SPLIT = prove( 263 ``!b j m k. part_heap b j m k ==> j <= e ==> (ref_mem m b j * ref_mem m j e = ref_mem m b e)``, 264 HO_MATCH_MP_TAC part_heap_ind \\ REPEAT STRIP_TAC 265 THEN1 (ONCE_REWRITE_TAC [ref_mem_def] \\ SIMP_TAC std_ss [SEP_CLAUSES]) THEN1 266 (REPEAT STRIP_TAC \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [ref_mem_def])) 267 \\ CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [ref_mem_def])) 268 \\ IMP_RES_TAC part_heap_LESS_EQ 269 \\ `~(j <= b) /\ ~(e <= b)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 270 \\ FULL_SIMP_TAC std_ss [GSYM ref_mem_def] 271 \\ `getLENGTH (m b) = 0` by (Cases_on `m b` \\ FULL_SIMP_TAC std_ss [getLENGTH_def, 272 heap_element_distinct,isBLOCK_def,heap_element_11]) 273 \\ ASM_SIMP_TAC std_ss [GSYM STAR_ASSOC]) 274 \\ `!i. b < i ==> (ref_mem m b i = ref_aux (ref_addr b) (m b) * ref_mem m (b + n + 1) i)` by 275 (REPEAT STRIP_TAC \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [ref_mem_def])) 276 \\ `MAX 1 (n + 1) = n + 1` by (SIMP_TAC std_ss [MAX_DEF] \\ DECIDE_TAC) 277 \\ ASM_SIMP_TAC std_ss [getLENGTH_def,DECIDE ``i<=b=~(b<i:num)``,ADD_ASSOC]) 278 \\ IMP_RES_TAC part_heap_LESS_EQ \\ `b < j /\ b < e` by DECIDE_TAC 279 \\ METIS_TAC [STAR_ASSOC]); 280 281val part_heap_ref_mem_SPLIT_LESS = prove( 282 ``!b j m k. part_heap b j m k /\ j < e ==> 283 (ref_mem m b e = ref_mem m b j * ref_aux (ref_addr j) (m j) * 284 ref_mem m (j + MAX 1 (getLENGTH (m j))) e)``, 285 REPEAT STRIP_TAC \\ `j <= e /\ ~(e <= j)` by DECIDE_TAC 286 \\ IMP_RES_TAC (GSYM part_heap_ref_mem_SPLIT) 287 \\ ASM_SIMP_TAC std_ss [GSYM STAR_ASSOC] \\ METIS_TAC [ref_mem_def]); 288 289val full_heap_ref_mem_SPLIT = prove( 290 ``!b j m. full_heap b j m ==> j <= e ==> (ref_mem m b j * ref_mem m j e = ref_mem m b e)``, 291 METIS_TAC [full_heap_IMP_part_heap,part_heap_ref_mem_SPLIT]); 292 293val part_heap_SPLIT = prove( 294 ``!b e m k. part_heap b e m k /\ RANGE(b,e)i /\ ~(m i = H_EMP) ==> 295 ?k1 k2. part_heap b i m k1 /\ part_heap i e m k2``, 296 SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 297 \\ HO_MATCH_MP_TAC part_heap_ind \\ REPEAT STRIP_TAC THEN1 `F` by RANGE_TAC THEN1 298 (Cases_on `i = b` \\ FULL_SIMP_TAC std_ss [] THEN1 METIS_TAC [part_heap_cases] 299 \\ `RANGE (b + 1,e) i` by RANGE_TAC \\ RES_TAC 300 \\ Q.LIST_EXISTS_TAC [`k1`,`k2`] \\ ASM_SIMP_TAC std_ss [] 301 \\ METIS_TAC [part_heap_cases]) 302 \\ Cases_on `i = b` \\ FULL_SIMP_TAC std_ss [] THEN1 METIS_TAC [part_heap_cases] 303 \\ Cases_on `RANGE (b + n + 1,e) i` THEN1 304 (RES_TAC \\ Q.LIST_EXISTS_TAC [`k1 + (n + 1)`,`k2`] \\ ASM_SIMP_TAC std_ss [] 305 \\ ONCE_REWRITE_TAC [part_heap_cases] \\ DISJ2_TAC \\ DISJ2_TAC 306 \\ Q.LIST_EXISTS_TAC [`n`,`xs`,`d`,`k1`] \\ ASM_SIMP_TAC std_ss [ADD_ASSOC]) 307 \\ `RANGE (b + 1,b + n + 1) i` by RANGE_TAC 308 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def,IN_DEF] \\ RES_TAC); 309 310val part_heap_ref_mem_SPLIT3 = prove( 311 ``!b e m k a. 312 part_heap b e m k /\ RANGE(b,e)a /\ ~(m a = H_EMP) ==> 313 (ref_mem m b e = ref_mem m b a * ref_aux (ref_addr a) (m a) * 314 ref_mem m (a + MAX 1 (getLENGTH (m a))) e)``, 315 REPEAT STRIP_TAC 316 \\ `?k1 k2. part_heap b a m k1 /\ part_heap a e m k2` by METIS_TAC [part_heap_SPLIT] 317 \\ `a <= e` by IMP_RES_TAC part_heap_LESS_EQ 318 \\ `ref_mem m b e = ref_mem m b a * ref_mem m a e` by METIS_TAC [part_heap_ref_mem_SPLIT] 319 \\ ASM_SIMP_TAC std_ss [] \\ `~(e <= a)` by RANGE_TAC 320 \\ ONCE_REWRITE_TAC [ref_mem_def] \\ ASM_SIMP_TAC std_ss [] 321 \\ ASM_SIMP_TAC std_ss [GSYM ref_mem_def] \\ ASM_SIMP_TAC std_ss [STAR_ASSOC]); 322 323val ALIGNED_ref_tag = prove( 324 ``~ALIGNED (ref_tag (n,d,t))``, 325 SIMP_TAC std_ss [ref_tag_def,ALIGNED_n2w] 326 \\ `(n * 1024 + w2n t * 4 + 2 + (if d then 1 else 0) = 327 (n * 256 + w2n t) * 4 + (2 + if d then 1 else 0)) /\ 328 2 + (if d then 1 else 0) < 4` 329 by (Cases_on `d` \\ DECIDE_TAC) 330 \\ ASM_SIMP_TAC std_ss [MOD_MULT]); 331 332val part_heap_IMP_EMP_RANGE = prove( 333 ``!b e m k. 334 part_heap b e m k /\ RANGE(b,e)i /\ (m i = H_BLOCK (xs,n,d)) ==> 335 EMP_RANGE (i + 1,i + n + 1) m /\ n <= e - (i + 1)``, 336 NTAC 5 STRIP_TAC \\ `~(m i = H_EMP)` by FULL_SIMP_TAC std_ss [heap_element_distinct] 337 \\ `?k2. part_heap i e m k2` by METIS_TAC [part_heap_SPLIT] 338 \\ IMP_RES_TAC part_heap_LENGTH_LESS_EQ 339 \\ `RANGE (i,e) i` by RANGE_TAC 340 \\ `n + 1 <= k2` by METIS_TAC [part_heap_REF] 341 \\ Q.PAT_X_ASSUM `part_heap i e m k2` (MP_TAC o RW1[part_heap_cases]) 342 \\ `~(e = i)` by RANGE_TAC \\ ASM_SIMP_TAC std_ss [isBLOCK_def,heap_element_11] 343 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC part_heap_LENGTH_LESS_EQ \\ ASM_SIMP_TAC std_ss [] 344 \\ RANGE_TAC); 345 346val arm_move_thm = prove( 347 ``gc_inv (h1,roots1,h,ff) (b,i,j,e,b2,e2,m,z UNION ADDR_SET [x]) /\ j2 <= je /\ je <= e /\ 348 (ADDR_SET [x]) SUBSET (DR0(CUT(b2,e2)m)) /\ ALIGNED r1 /\ b <= ij /\ ij <= j /\ 349 (one (r1,ref_heap_addr x) * ref_mem m ij je * ref_mem m b2 e2 * p) (fun2set (f,df)) /\ 350 ok_memory m /\ full_heap ij j m /\ (move(x,j,m) = (x2,j2,m2)) ==> 351 ?f2. arm_move_pre (r1,ref_heap_addr x,ref_addr j,df,f) /\ 352 (arm_move (r1,ref_heap_addr x,ref_addr j,df,f) = (r1,ref_addr j2,df,f2)) /\ 353 (one (r1,ref_heap_addr x2) * ref_mem m2 ij je * ref_mem m2 b2 e2 * p) (fun2set (f2,df)) /\ 354 ok_memory m2``, 355 REVERSE (Cases_on `x`) THEN1 356 (SIMP_TAC std_ss [ref_heap_addr_def] 357 \\ ONCE_REWRITE_TAC [arm_move_def,arm_move_pre_def,move_def] 358 \\ `(n2w (w2n a * 2 + 1) && 0x3w) <> 0x0w:word32` suffices_by 359 (STRIP_TAC THEN ASM_SIMP_TAC std_ss [] \\ METIS_TAC [ref_heap_addr_def]) 360 \\ MATCH_MP_TAC (METIS_PROVE [] ``~(w && 1w = v && 1w) ==> ~(w = v)``) 361 \\ SIMP_TAC std_ss [n2w_and_1,n2w_and_3] \\ SIMP_TAC bool_ss [DECIDE ``4=2*2``] 362 \\ SIMP_TAC bool_ss [MATCH_MP MOD_MULT_MOD (DECIDE ``0<2 /\ 0<2``)] 363 \\ SIMP_TAC std_ss [MATCH_MP MOD_MULT (DECIDE ``1 < 2``)] \\ EVAL_TAC) 364 \\ SIMP_TAC std_ss [ADDR_SET_THM,INSERT_SUBSET,EMPTY_SUBSET] 365 \\ STRIP_TAC \\ IMP_RES_TAC move_lemma 366 \\ ONCE_REWRITE_TAC [arm_move_def,arm_move_pre_def,move_def] 367 \\ SIMP_TAC std_ss [ref_heap_addr_def,ALIGNED_INTRO,LET_DEF,ALIGNED_ref_addr] 368 \\ `~(m n = H_EMP)` by ASM_SIMP_TAC std_ss [heap_element_distinct] 369 \\ FULL_SIMP_TAC (srw_ss()) [move_def] THEN1 370 (SUBGOAL `(f (ref_addr n) = ref_addr (ff n)) /\ (ref_addr n) IN df` THEN1 371 (ASM_SIMP_TAC std_ss [ALIGNED_and_1,NOT_ALIGNED,ALIGNED_ref_addr] 372 \\ EXPAND_TAC \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def] \\ SEP_R_TAC 373 \\ SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 374 \\ FULL_SIMP_TAC std_ss [gc_inv_def] \\ EXPAND_TAC 375 \\ `RANGE (b2,e2) n` by FULL_SIMP_TAC std_ss [IN_DEF,R0_def,D0_def,DR0_def,CUT_EQ] 376 \\ IMP_RES_TAC part_heap_ref_mem_SPLIT3 \\ FULL_SIMP_TAC std_ss [] 377 \\ FULL_SIMP_TAC std_ss [ref_aux_def] \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss []) 378 \\ `?xs y d. h ' n = (xs,y,d)` by METIS_TAC [PAIR] 379 \\ FULL_SIMP_TAC (srw_ss()) [LET_DEF,getLENGTH_def,ADD_ASSOC] \\ EXPAND_TAC 380 \\ `~RANGE (b2,e2) j /\ ~RANGE (ij,je) n /\ n < e2` by RANGE_TAC 381 \\ ASM_SIMP_TAC std_ss [ref_mem_IGNORE] 382 \\ Q.PAT_X_ASSUM `~(n = j)` (fn th => REWRITE_TAC [MATCH_MP UPDATE_COMMUTES (GSYM th)] 383 \\ ASSUME_TAC th) 384 \\ ASM_SIMP_TAC std_ss [ref_mem_IGNORE] 385 \\ `j < e` by RANGE_TAC 386 \\ `m j = H_EMP` by 387 (FULL_SIMP_TAC std_ss [gc_inv_def] 388 \\ Q.PAT_X_ASSUM `!k. bb ==> (m k = H_EMP)` MATCH_MP_TAC \\ RANGE_TAC) 389 \\ `((n =+ H_REF j) m) n <> H_EMP` by 390 FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,heap_element_distinct] 391 \\ `?len. part_heap b2 e2 m len` by METIS_TAC [gc_inv_def] 392 \\ `?len2. part_heap b2 e2 ((n =+ H_REF j) m) len2` by 393 (FULL_SIMP_TAC std_ss [IN_DEF,gc_inv_def] \\ METIS_TAC [part_heap_REF]) 394 \\ `RANGE (b2,e2) n` by FULL_SIMP_TAC std_ss [IN_DEF,R0_def,D0_def,DR0_def,CUT_EQ] 395 \\ IMP_RES_TAC part_heap_ref_mem_SPLIT3 396 \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM,getLENGTH_def,ref_heap_addr_def] 397 \\ `~(RANGE(b2,n)n) /\ ~(RANGE(n+1,e2)n) /\ ~(RANGE(j+MAX 1 (x + 1),je)j) /\ 398 ~(RANGE(ij,j)j) /\ ~(RANGE(ij,je)n) /\ j < je` by 399 (FULL_SIMP_TAC std_ss [RANGE_def,MAX_DEF] \\ DECIDE_TAC) 400 \\ FULL_SIMP_TAC std_ss [ref_mem_IGNORE,STAR_ASSOC,getLENGTH_def] 401 \\ `j <= je` by DECIDE_TAC 402 \\ `full_heap ij j ((j =+ H_BLOCK (xs,y,d)) m)` by 403 (MATCH_MP_TAC full_heap_RANGE \\ ASM_SIMP_TAC std_ss [RANGE_def]) 404 \\ IMP_RES_TAC (GSYM full_heap_ref_mem_SPLIT) 405 \\ ASSUME_TAC (UNDISCH (Q.SPECL [`j`,`je`] ref_mem_LESS)) 406 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,getLENGTH_def,ref_mem_IGNORE] 407 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] 408 \\ Cases_on `d` 409 \\ `ok_memory ((n =+ H_REF j) ((j =+ H_BLOCK (xs,y,q,r)) m))` by 410 (FULL_SIMP_TAC std_ss [ok_memory_def,APPLY_UPDATE_THM] 411 \\ METIS_TAC [heap_element_distinct,heap_element_11]) 412 \\ `?z1 z2. r = (z1,z2)` by METIS_TAC [PAIR] 413 \\ FULL_SIMP_TAC std_ss [MAX_LEMMA] \\ POP_ASSUM (K ALL_TAC) 414 \\ FULL_SIMP_TAC std_ss [ref_aux_def,SEP_CLAUSES,SEP_EXISTS_THM,LET_DEF] 415 \\ Q.ABBREV_TAC `qs = if z1 then MAP ref_heap_addr xs else z2` 416 \\ `ref_addr n IN df /\ r1 IN df /\ ref_addr j IN df` by SEP_READ_TAC 417 \\ `f (ref_addr n) = ref_tag (LENGTH qs,z1,q)` by SEP_READ_TAC 418 \\ ASM_SIMP_TAC std_ss [ALIGNED_ref_tag] 419 \\ `LENGTH qs < 2 ** 22` by 420 (Q.UNABBREV_TAC `qs` \\ Cases_on `z1` \\ FULL_SIMP_TAC std_ss [ok_memory_def] 421 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [LENGTH_MAP]) 422 \\ ASM_SIMP_TAC std_ss [ref_tag_lsr] 423 \\ Q.PAT_ABBREV_TAC `fff = (ref_addr n =+ ref_addr j) ffff` 424 \\ `(one (r1,ref_addr j) * ref_mem m ij j * 425 one (ref_addr j,ref_tag (LENGTH qs,z1,q)) * 426 ref_mem m (j + 1) je * ref_mem m b2 n * 427 (one (ref_addr n,ref_addr j) * 428 one_list (ref_addr n + 0x4w) qs) * ref_mem m (n + (y + 1)) e2 * 429 p) (fun2set (fff,df))` by (Q.UNABBREV_TAC `fff` \\ SEP_WRITE_TAC) 430 \\ `y <= je - (j + 1)` by RANGE_TAC 431 \\ `!i. i < y ==> (m ((j + 1) + i) = H_EMP)` by 432 (FULL_SIMP_TAC std_ss [gc_inv_def] \\ REPEAT STRIP_TAC 433 \\ REPEAT (Q.PAT_X_ASSUM `~RANGE(bb,ee)ii` (K ALL_TAC)) 434 \\ Q.PAT_X_ASSUM `!k. bbb ==> (m k = H_EMP)` MATCH_MP_TAC 435 \\ FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC) 436 \\ IMP_RES_TAC ref_mem_one_list 437 \\ FULL_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 438 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES,cond_STAR] 439 \\ Q.PAT_X_ASSUM `bbbb (fun2set (f,df))` (K ALL_TAC) 440 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS_THM,ref_addr_ADD1,word_arith_lemma1] 441 \\ FULL_SIMP_TAC std_ss [cond_STAR] 442 \\ `(one_list (ref_addr n + 0x4w) qs * one_list (ref_addr j + 0x4w) ts * 443 (one (r1,ref_addr j) * ref_mem m ij j * 444 one (ref_addr j,ref_tag (LENGTH qs,z1,q)) * 445 ref_mem m (j + 1 + y) je * 446 ref_mem m b2 n * one (ref_addr n,ref_addr j) * 447 ref_mem m (n + (y + 1)) e2 * p)) (fun2set (fff,df))` by 448 FULL_SIMP_TAC (std_ss++star_ss) [] 449 \\ `ALIGNED (ref_addr n + 0x4w) /\ ALIGNED (ref_addr j + 0x4w)` 450 by ASM_SIMP_TAC std_ss [ALIGNED,ALIGNED_ref_addr] 451 \\ `LENGTH ts < 2 ** 23 /\ (LENGTH qs = LENGTH ts) /\ y < 8388608` by 452 (FULL_SIMP_TAC std_ss [ok_memory_def] \\ RES_TAC 453 \\ Cases_on `z1` \\ Q.UNABBREV_TAC `qs` 454 \\ FULL_SIMP_TAC std_ss [LENGTH_MAP] \\ DECIDE_TAC) 455 \\ IMP_RES_TAC arm_move_loop_thm 456 \\ REPEAT (Q.PAT_X_ASSUM `!xx yy zz. bb` (K ALL_TAC)) 457 \\ FULL_SIMP_TAC std_ss [] 458 \\ POP_ASSUM MP_TAC \\ ASM_SIMP_TAC bool_ss [] \\ REPEAT STRIP_TAC 459 \\ FULL_SIMP_TAC (std_ss++star_ss) [GSYM ref_addr_ADD1, GSYM ref_addr_def] 460 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 461 \\ `y <= e2 - (n + 1) /\ (!i. i < y ==> (m ((n + 1) + i) = H_EMP))` by 462 (IMP_RES_TAC part_heap_IMP_EMP_RANGE \\ ASM_SIMP_TAC std_ss [] 463 \\ FULL_SIMP_TAC std_ss [EMP_RANGE_def] \\ REPEAT STRIP_TAC 464 \\ Q.PAT_X_ASSUM `!k. k IN RANGE (n + 1,n + y + 1) ==> (m k = H_EMP)` MATCH_MP_TAC 465 \\ RANGE_TAC) 466 \\ IMP_RES_TAC ref_mem_one_list 467 \\ `~RANGE(j + (y + 1),je)j` by RANGE_TAC \\ FULL_SIMP_TAC std_ss [ref_mem_IGNORE] 468 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,SEP_EXISTS_THM] \\ Q.EXISTS_TAC `qs` 469 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_CLAUSES, AC ADD_ASSOC ADD_COMM]); 470 471val EQ_RANGE_ref_mem = prove( 472 ``!i j m m2. EQ_RANGE (i,j) m m2 ==> (ref_mem m i j = ref_mem m2 i j)``, 473 NTAC 2 STRIP_TAC \\ completeInduct_on `j-i` \\ ONCE_REWRITE_TAC [ref_mem_def] 474 \\ REPEAT STRIP_TAC \\ Cases_on `j<=i` \\ ASM_SIMP_TAC std_ss [] 475 \\ `m i = m2 i` by 476 (FULL_SIMP_TAC std_ss [EQ_RANGE_def,RANGE_def,IN_DEF] 477 \\ `i <= i /\ i < j` by DECIDE_TAC \\ METIS_TAC []) 478 \\ ASM_SIMP_TAC std_ss [] 479 \\ Q.ABBREV_TAC `y = MAX 1 (getLENGTH (m2 i))` 480 \\ `0 < y` by (Q.UNABBREV_TAC `y` \\ SIMP_TAC std_ss [MAX_DEF] \\ DECIDE_TAC) 481 \\ `j - (i + y) < j - i` by DECIDE_TAC 482 \\ `EQ_RANGE (i+y,j) m m2` suffices_by METIS_TAC [] 483 \\ MATCH_MP_TAC EQ_RANGE_IMP_EQ_RANGE \\ Q.LIST_EXISTS_TAC [`i`,`j`] 484 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 485 486val EQ_RANGE_TRANS = prove( 487 ``!m1 m2 m3. EQ_RANGE (b,e) m1 m2 /\ EQ_RANGE (b,e) m2 m3 ==> EQ_RANGE (b,e) m1 m3``, 488 METIS_TAC [EQ_RANGE_def]); 489 490val full_heap_NEXT = prove( 491 ``(m i = H_BLOCK (x,n,y)) /\ ~(i = j) /\ full_heap i j m ==> 492 full_heap (i + n + 1) j m``, 493 CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [full_heap_cases])) 494 \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO,heap_element_11]); 495 496val arm_move_list_thm = prove( 497 ``!f m j ys p r1 z h f8. 498 ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m) /\ ALIGNED r1 /\ 499 full_heap ij j m /\ b <= ij /\ ij <= j /\ j2 <= je /\ je <= e /\ 500 gc_inv (h1,roots1,h,f8) (b,i,j,e,b2,e2,m,z UNION ADDR_SET xs) /\ e < 2**30 /\ LENGTH xs < 2**32 /\ 501 (ref_mem m ij je * ref_mem m b2 e2 * one_list r1 (MAP ref_heap_addr xs) * p) (fun2set (f,df)) /\ 502 ok_memory m ==> (move_list(xs,j,m) = (ys,j2,m2)) ==> 503 ?f2 h3 f3. 504 arm_move_list_pre (r1,ref_addr j,n2w (LENGTH xs),df,f)/\ 505 (arm_move_list (r1,ref_addr j,n2w (LENGTH xs),df,f) = (r1 + n2w (4 * LENGTH xs),ref_addr j2,df,f2)) /\ 506 (ref_mem m2 ij je * ref_mem m2 b2 e2 * one_list r1 (MAP ref_heap_addr ys) * p) (fun2set (f2,df)) /\ 507 ok_memory m2 /\ gc_inv (h1,roots1,h3,f3) 508 (b,i,j2,e,b2,e2,m2,z UNION D1 (CUT (j,j2) m2)) /\ 509 (LENGTH ys = LENGTH xs)``, 510 Induct_on `xs` THEN1 511 (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [move_list_def,one_list_def] 512 \\ ONCE_REWRITE_TAC [arm_move_list_def,arm_move_list_pre_def] 513 \\ SIMP_TAC std_ss [LENGTH,WORD_ADD_0,CUT_EMPTY,ADDR_SET_THM] \\ METIS_TAC []) 514 \\ ONCE_REWRITE_TAC [ADDR_SET_CONS] \\ SIMP_TAC std_ss [UNION_SUBSET] 515 \\ NTAC 6 STRIP_TAC \\ `?y j3 m3. move(h,j,m) = (y,j3,m3)` by METIS_TAC [PAIR] 516 \\ `?zs j4 m4. move_list (xs,j3,m3) = (zs,j4,m4)` by METIS_TAC [PAIR] 517 \\ ASM_SIMP_TAC std_ss [move_list_def,one_list_def,MAP,LET_DEF,STAR_ASSOC] 518 \\ REPEAT STRIP_TAC \\ NTAC 2 (POP_ASSUM (fn th => FULL_SIMP_TAC std_ss [GSYM th])) 519 \\ FULL_SIMP_TAC std_ss [UNION_ASSOC] \\ IMP_RES_TAC move_thm 520 \\ `ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m3)` by METIS_TAC [SUBSET_TRANS] 521 \\ `z UNION ADDR_SET xs UNION D1 (CUT (j,j3) m3) = 522 (z UNION D1 (CUT (j,j3) m3)) UNION ADDR_SET xs` by SET_TAC 523 \\ `j3 <= j4` by METIS_TAC [move_list_thm] 524 \\ ONCE_REWRITE_TAC [arm_move_list_def,arm_move_list_pre_def] \\ SEP_R_TAC 525 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,LENGTH,n2w_11,DECIDE ``~(SUC n = 0)``] 526 \\ SIMP_TAC std_ss [MULT_CLAUSES,GSYM word_add_n2w,WORD_ADD_ASSOC] 527 \\ ASM_SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB,ALIGNED_INTRO] 528 \\ `j3 <= je` by DECIDE_TAC 529 \\ SEP_S_TAC ["arm_move","move","gc_inv"] (GEN_ALL arm_move_thm) 530 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 531 \\ Q.PAT_X_ASSUM `!xx yy. bbb` (SEP_S_TAC ["arm_move_list","move_list","gc_inv"]) 532 \\ IMP_RES_TAC full_heap_LESS_EQ 533 \\ `ij <= j3 /\ LENGTH xs < 4294967296` by DECIDE_TAC 534 \\ ASM_SIMP_TAC std_ss [ALIGNED] 535 \\ `EQ_RANGE (ij,j) m m3` by 536 (MATCH_MP_TAC EQ_RANGE_IMP_EQ_RANGE \\ METIS_TAC [EQ_RANGE_THM,LESS_EQ_REFL]) 537 \\ IMP_RES_TAC EQ_RANGE_full_heap 538 \\ IMP_RES_TAC full_heap_TRANS \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 539 \\ ASM_SIMP_TAC std_ss [] \\ EXPAND_TAC 540 \\ FULL_SIMP_TAC (std_ss++star_ss) [LENGTH,one_list_def,MAP,ADD1] 541 \\ `D1 (CUT (j,j4) m4) = D1 (CUT (j,j3) m4) UNION D1 (CUT (j3,j4) m4)` by 542 METIS_TAC [D1_UNION] 543 \\ SUBGOAL `CUT (j,j3) m3 = CUT (j,j3) m4` THEN1 METIS_TAC [UNION_ASSOC] 544 \\ `(CUT(b,j3)m3 = CUT(b,j3)m4)` by METIS_TAC [move_list_thm] 545 \\ FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM,IN_DEF] \\ REPEAT STRIP_TAC 546 \\ Cases_on `RANGE (j,j3) x` \\ ASM_SIMP_TAC std_ss [] 547 \\ `RANGE (b,j3) x` by RANGE_TAC \\ SET_TAC); 548 549val arm_move_roots_thm = prove( 550 ``!f m j ys p r1 z h f8. 551 ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m) /\ ALIGNED r1 /\ 552 full_heap ij j m /\ b <= ij /\ ij <= j /\ j2 <= je /\ je <= e /\ 553 gc_inv (h1,roots1,h,f8) (b,i,j,e,b2,e2,m,z UNION ADDR_SET xs) /\ e < 2**30 /\ 554 (ref_mem m ij je * ref_mem m b2 e2 * one_list_roots r1 xs * p) (fun2set (f,df)) /\ 555 ok_memory m ==> (move_list(xs,j,m) = (ys,j2,m2)) ==> 556 ?f2 h3 f3. 557 arm_move_roots_pre (r1,ref_addr j,df,f)/\ 558 (arm_move_roots (r1,ref_addr j,df,f) = (ref_addr j2,df,f2)) /\ 559 (ref_mem m2 ij je * ref_mem m2 b2 e2 * one_list_roots r1 ys * p) (fun2set (f2,df)) /\ 560 ok_memory m2 /\ gc_inv (h1,roots1,h3,f3) 561 (b,i,j2,e,b2,e2,m2,z UNION D1 (CUT (j,j2) m2))``, 562 Induct_on `xs` THEN1 563 (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [move_list_def,one_list_roots_def] 564 \\ ONCE_REWRITE_TAC [arm_move_roots_def,arm_move_roots_pre_def] 565 \\ REPEAT STRIP_TAC \\ `(f r1 = 2w) /\ r1 IN df` by SEP_READ_TAC 566 \\ FULL_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO,ADDR_SET_THM,CUT_EMPTY] \\ SET_TAC) 567 \\ ONCE_REWRITE_TAC [ADDR_SET_CONS] \\ SIMP_TAC std_ss [UNION_SUBSET] 568 \\ NTAC 6 STRIP_TAC \\ `?y j3 m3. move(h,j,m) = (y,j3,m3)` by METIS_TAC [PAIR] 569 \\ `?zs j4 m4. move_list (xs,j3,m3) = (zs,j4,m4)` by METIS_TAC [PAIR] 570 \\ ASM_SIMP_TAC std_ss [move_list_def,one_list_roots_def,MAP,LET_DEF,STAR_ASSOC] 571 \\ REPEAT STRIP_TAC \\ NTAC 2 (POP_ASSUM (fn th => FULL_SIMP_TAC std_ss [GSYM th])) 572 \\ FULL_SIMP_TAC std_ss [UNION_ASSOC] \\ IMP_RES_TAC move_thm 573 \\ `ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m3)` by METIS_TAC [SUBSET_TRANS] 574 \\ `z UNION ADDR_SET xs UNION D1 (CUT (j,j3) m3) = 575 (z UNION D1 (CUT (j,j3) m3)) UNION ADDR_SET xs` by SET_TAC 576 \\ `j3 <= j4` by METIS_TAC [move_list_thm] 577 \\ ONCE_REWRITE_TAC [arm_move_roots_def,arm_move_roots_pre_def] \\ SEP_R_TAC 578 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,LENGTH,ref_heap_addr_NEQ_2] 579 \\ SIMP_TAC std_ss [MULT_CLAUSES,GSYM word_add_n2w,WORD_ADD_ASSOC] 580 \\ ASM_SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB,ALIGNED_INTRO] 581 \\ `j3 <= je` by DECIDE_TAC 582 \\ SEP_S_TAC ["arm_move","move","gc_inv"] (GEN_ALL arm_move_thm) 583 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 584 \\ Q.PAT_X_ASSUM `!xx yy. bbb` (SEP_S_TAC ["arm_move_roots","move_list","gc_inv"]) 585 \\ IMP_RES_TAC full_heap_LESS_EQ 586 \\ `ij <= j3` by DECIDE_TAC 587 \\ ASM_SIMP_TAC std_ss [ALIGNED] 588 \\ `EQ_RANGE (ij,j) m m3` by 589 (MATCH_MP_TAC EQ_RANGE_IMP_EQ_RANGE \\ METIS_TAC [EQ_RANGE_THM,LESS_EQ_REFL]) 590 \\ IMP_RES_TAC EQ_RANGE_full_heap 591 \\ IMP_RES_TAC full_heap_TRANS \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 592 \\ ASM_SIMP_TAC std_ss [] \\ EXPAND_TAC 593 \\ FULL_SIMP_TAC (std_ss++star_ss) [LENGTH,one_list_roots_def,MAP,ADD1] 594 \\ `D1 (CUT (j,j4) m4) = D1 (CUT (j,j3) m4) UNION D1 (CUT (j3,j4) m4)` by 595 METIS_TAC [D1_UNION] 596 \\ SUBGOAL `CUT (j,j3) m3 = CUT (j,j3) m4` THEN1 METIS_TAC [UNION_ASSOC] 597 \\ `(CUT(b,j3)m3 = CUT(b,j3)m4)` by METIS_TAC [move_list_thm] 598 \\ FULL_SIMP_TAC std_ss [CUT_def,FUN_EQ_THM,IN_DEF] \\ REPEAT STRIP_TAC 599 \\ Cases_on `RANGE (j,j3) x` \\ ASM_SIMP_TAC std_ss [] 600 \\ `RANGE (b,j3) x` by RANGE_TAC \\ SET_TAC); 601 602val ref_tag_and_1 = prove( 603 ``(ref_tag (n,x,y) && 1w = 0w) = ~x``, 604 SIMP_TAC std_ss [ref_tag_def,n2w_and_1] 605 \\ `n * 1024 + w2n y * 4 + 2 = (n * 512 + w2n y * 2 + 1) * 2` by DECIDE_TAC 606 \\ `(if x then 1 else 0) < 2` by (Cases_on `x` \\ DECIDE_TAC) 607 \\ ASM_SIMP_TAC std_ss [MOD_MULT] \\ Cases_on `x` 608 \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC); 609 610val arm_loop_thm = prove( 611 ``!f m j h8 f8. gc_inv (h1,roots1,h8,f8) (b,i,j,e,b2,e2,m,D1 (CUT (i,j) m)) /\ 612 e < 2 ** 30 /\ 613 (ref_mem m b i2 * ref_mem m b2 e2 * p) (fun2set (f,df)) /\ 614 ok_memory m ==> (gc_loop(i,j,m) = (i2,m2)) ==> 615 ?f2. arm_loop_pre (ref_addr i,ref_addr j,df,f) /\ 616 (arm_loop (ref_addr i,ref_addr j,df,f) = (ref_addr i2,df,f2)) /\ 617 (ref_mem m2 b i2 * ref_mem m2 b2 e2 * p) (fun2set (f2,df)) /\ ok_memory m2``, 618 completeInduct_on `e-i` \\ NTAC 9 STRIP_TAC \\ Cases_on `j <= i` THEN1 619 (`i = j` by (FULL_SIMP_TAC std_ss [gc_inv_def] \\ DECIDE_TAC) 620 \\ PURE_ONCE_REWRITE_TAC [gc_loop_def,arm_loop_def,arm_loop_pre_def] 621 \\ ASM_SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 622 \\ FULL_SIMP_TAC std_ss [CUT_EMPTY] \\ METIS_TAC []) 623 \\ `~(i = j)` by (FULL_SIMP_TAC std_ss [gc_inv_def] \\ DECIDE_TAC) 624 \\ IMP_RES_TAC gc_step_lemma 625 \\ PURE_ONCE_REWRITE_TAC [gc_loop_def,arm_loop_def,arm_loop_pre_def] 626 \\ ASM_SIMP_TAC std_ss [] 627 \\ `~(ref_addr i = ref_addr j)` by 628 (FULL_SIMP_TAC (std_ss++SIZES_ss) [ref_addr_def,n2w_11] 629 \\ `i <= e /\ j <= e` by (FULL_SIMP_TAC std_ss [gc_inv_def] \\ DECIDE_TAC) 630 \\ `4 * i < 4 * 1073741824 /\ 4 * j < 4 * 1073741824` by DECIDE_TAC 631 \\ FULL_SIMP_TAC bool_ss [EVAL ``4 * 1073741824``,LESS_MOD] \\ DECIDE_TAC) 632 \\ `?i8 j8 m8. gc_step (i,j,m) = (i8,j8,m8)` by METIS_TAC [PAIR] 633 \\ ASM_SIMP_TAC std_ss [LET_DEF] 634 \\ `i < j` by DECIDE_TAC \\ IMP_RES_TAC gc_step_thm 635 \\ REPEAT (Q.PAT_X_ASSUM `!xx yy zz dd. bb` (K ALL_TAC)) 636 \\ Q.PAT_X_ASSUM `m i = H_BLOCK (xs,n,d)` ASSUME_TAC 637 \\ FULL_SIMP_TAC std_ss [getBLOCK_def,gc_step_def,LET_DEF] 638 \\ STRIP_TAC \\ `i8 <= i2 /\ j8 <= i2 /\ i2 <= e` by 639 (IMP_RES_TAC gc_loop_thm \\ ASM_SIMP_TAC std_ss [] 640 \\ FULL_SIMP_TAC std_ss [gc_inv_def] \\ DECIDE_TAC) 641 \\ Q.PAT_X_ASSUM `xx = (i2,m2)` MP_TAC 642 \\ `?z1 z2 z3. d = (z1,z2,z3)` by METIS_TAC [PAIR] 643 \\ FULL_SIMP_TAC std_ss [] 644 \\ Q.ABBREV_TAC `qs = if z2 then MAP ref_heap_addr xs else z3` 645 \\ `(f (ref_addr i) = ref_tag (LENGTH qs,z2,z1)) /\ 646 (ref_addr i) IN df` by 647 (FULL_SIMP_TAC std_ss [gc_inv_def] 648 \\ `i < i2` by (FULL_SIMP_TAC std_ss [gc_inv_def,RANGE_def] \\ DECIDE_TAC) 649 \\ IMP_RES_TAC full_heap_IMP_part_heap 650 \\ IMP_RES_TAC part_heap_ref_mem_SPLIT_LESS 651 \\ FULL_SIMP_TAC std_ss [ref_aux_def,LET_DEF] \\ SEP_READ_TAC) 652 \\ ASM_SIMP_TAC std_ss [ref_tag_and_1] 653 \\ REVERSE (Cases_on `z2`) THEN1 654 (FULL_SIMP_TAC std_ss [] \\ Q.UNABBREV_TAC `qs` 655 \\ `(xs = []) /\ LENGTH z3 < 2 ** 22 /\ (LENGTH z3 = n)` 656 by METIS_TAC [heap_element_11,ok_memory_def] 657 \\ ASM_SIMP_TAC bool_ss [ref_tag_lsr] 658 \\ FULL_SIMP_TAC std_ss [move_list_def,UPDATE_APPLY_IMP_ID,GSYM ref_addr_ADD1] 659 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_ref_addr,WORD_MUL_LSL, 660 word_mul_n2w,GSYM ref_addr_def,GSYM ref_addr_ADD1] 661 \\ `e - (i + n + 1) < e - i` by (FULL_SIMP_TAC std_ss [gc_inv_def] \\ DECIDE_TAC) 662 \\ Q.PAT_X_ASSUM `!m. m < e - i ==> bbb` ASSUME_TAC 663 \\ POP_ASSUM (ASSUME_TAC o UNDISCH o Q.SPEC `e - (i + n + 1)`) 664 \\ POP_ASSUM (MP_TAC o RW[] o Q.SPECL [`e`,`i + n + 1`]) 665 \\ `i + 1 + n = i + n + 1` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 666 \\ STRIP_TAC \\ POP_ASSUM MATCH_MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ SET_TAC) 667 \\ `i < i2` by RANGE_TAC 668 \\ `?k. part_heap b i m k` by (FULL_SIMP_TAC std_ss [gc_inv_def] 669 \\ IMP_RES_TAC full_heap_IMP_part_heap \\ SET_TAC) 670 \\ `ref_mem m b i2 = 671 ref_mem m b i * ref_aux (ref_addr i) (m i) * 672 ref_mem m (i + MAX 1 (getLENGTH (m i))) i2` by METIS_TAC [part_heap_ref_mem_SPLIT_LESS] 673 \\ FULL_SIMP_TAC std_ss [ref_aux_def,STAR_ASSOC,ALIGNED_INTRO,ALIGNED_ref_addr] 674 \\ Q.UNABBREV_TAC `qs` 675 \\ `LENGTH xs < 2 ** 22 /\ (LENGTH xs = n)` by METIS_TAC [heap_element_11,ok_memory_def] 676 \\ FULL_SIMP_TAC bool_ss [LENGTH_MAP,ref_tag_lsr,LET_DEF] 677 \\ `?xs3 j3 m3. move_list (xs,j,m) = (xs3,j3,m3)` by METIS_TAC [PAIR] 678 \\ FULL_SIMP_TAC std_ss [LET_DEF,LENGTH_MAP,STAR_ASSOC,getLENGTH_def,MAX_LEMMA] 679 \\ Q.PAT_X_ASSUM `LENGTH xs = n` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 680 \\ `?f2 h3 f3. 681 arm_move_list_pre (ref_addr i + 0x4w,ref_addr j,n2w (LENGTH xs),df,f) /\ 682 (arm_move_list (ref_addr i + 0x4w,ref_addr j,n2w (LENGTH xs),df,f) = 683 (ref_addr i + 0x4w + n2w (4 * LENGTH xs),ref_addr j8,df,f2)) /\ 684 (ref_mem m3 (i + LENGTH xs + 1) i2 * ref_mem m3 b2 e2 * 685 one_list (ref_addr i + 0x4w) (MAP ref_heap_addr xs3) * 686 (ref_mem m b i * one (ref_addr i,ref_tag (LENGTH xs,T,z1)) * p)) 687 (fun2set (f2,df)) /\ ok_memory m3 /\ 688 gc_inv (h1,roots1,h3,f3) 689 (b,i,j8,e,b2,e2,m3,D1 (CUT (i+LENGTH xs+1,j) m) UNION D1 (CUT (j,j8) m3)) /\ 690 (LENGTH xs3 = LENGTH xs)` by 691 (MATCH_MP_TAC (RW [AND_IMP_INTRO] (GEN_ALL arm_move_list_thm)) 692 \\ Q.LIST_EXISTS_TAC [`m`,`h8`,`f8`] 693 \\ `LENGTH xs < 4294967296` by DECIDE_TAC 694 \\ ASM_SIMP_TAC std_ss [ALIGNED,ALIGNED_ref_addr] 695 \\ `full_heap i8 j m` by METIS_TAC [full_heap_NEXT,gc_inv_def] 696 \\ EXPAND_TAC \\ FULL_SIMP_TAC (std_ss++star_ss) [AC ADD_ASSOC ADD_COMM] 697 \\ IMP_RES_TAC full_heap_LESS_EQ \\ FULL_SIMP_TAC std_ss [gc_inv_def]) 698 \\ FULL_SIMP_TAC std_ss [move_list_def,UPDATE_APPLY_IMP_ID,GSYM ref_addr_ADD1] 699 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_ref_addr,WORD_MUL_LSL, 700 word_mul_n2w,GSYM ref_addr_def,GSYM ref_addr_ADD1] 701 \\ `e - i8 < e - i /\ (i + 1 + LENGTH xs = i8)` by DECIDE_TAC 702 \\ ASM_SIMP_TAC std_ss [] 703 \\ Q.PAT_X_ASSUM `!m. m < e - i ==> bbb` (ASSUME_TAC o UNDISCH o Q.SPEC `e - i8`) 704 \\ POP_ASSUM (MATCH_MP_TAC o RW[] o Q.SPECL [`e`,`i8`]) 705 \\ Q.PAT_X_ASSUM `(i + LENGTH xs + 1 = i8)` ASSUME_TAC \\ FULL_SIMP_TAC std_ss [] 706 \\ `i8 <= j` by IMP_RES_TAC full_heap_LESS_EQ 707 \\ SUBGOAL `(ref_mem m8 b i2 * ref_mem m8 b2 e2 * p) (fun2set (f2,df)) /\ 708 ok_memory m8` THEN1 METIS_TAC [D1_UNION] 709 \\ Q.PAT_X_ASSUM `mmm = m8` (ASSUME_TAC o GSYM) \\ FULL_SIMP_TAC std_ss [] 710 \\ REVERSE STRIP_TAC THEN1 711 (FULL_SIMP_TAC std_ss [ok_memory_def,APPLY_UPDATE_THM] \\ RES_TAC 712 \\ STRIP_TAC \\ Cases_on `i = a` \\ FULL_SIMP_TAC std_ss [heap_element_11] 713 \\ METIS_TAC []) 714 \\ `full_heap b i ((i =+ H_BLOCK (xs3,LENGTH xs,z1,T,z3)) m3)` by 715 (`~(RANGE(b,i)i)` by RANGE_TAC \\ FULL_SIMP_TAC std_ss [gc_inv_def] 716 \\ METIS_TAC [full_heap_RANGE]) 717 \\ `(ref_mem ((i =+ H_BLOCK (xs3,LENGTH xs,z1,T,z3)) m3) b i2 = 718 ref_mem ((i =+ H_BLOCK (xs3,LENGTH xs,z1,T,z3)) m3) b i * 719 ref_aux (ref_addr i) (((i =+ H_BLOCK (xs3,LENGTH xs,z1,T,z3)) m3) i) * 720 ref_mem ((i =+ H_BLOCK (xs3,LENGTH xs,z1,T,z3)) m3) 721 (i + MAX 1 (getLENGTH (((i =+ H_BLOCK (xs3,LENGTH xs,z1,T,z3)) m3) i))) i2)` by 722 (MATCH_MP_TAC part_heap_ref_mem_SPLIT_LESS 723 \\ FULL_SIMP_TAC std_ss [gc_inv_def] 724 \\ METIS_TAC [full_heap_IMP_part_heap]) 725 \\ `~(RANGE (b,i) i) /\ ~(RANGE (i8,i2) i) /\ ~(RANGE (b2,e2) i)` 726 by (FULL_SIMP_TAC std_ss [gc_inv_def,RANGE_def] \\ DECIDE_TAC) 727 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM,getLENGTH_def,STAR_ASSOC, 728 ref_aux_def,HD,ref_mem_IGNORE,LET_DEF,LENGTH_MAP,MAX_LEMMA,ADD_ASSOC] 729 \\ `ref_mem m b i = ref_mem m3 b i` 730 suffices_by (STRIP_TAC \\ 731 FULL_SIMP_TAC (std_ss++star_ss) 732 [AC ADD_ASSOC ADD_COMM,ref_addr_ADD1]) 733 \\ MATCH_MP_TAC EQ_RANGE_ref_mem 734 \\ MATCH_MP_TAC EQ_RANGE_IMP_EQ_RANGE 735 \\ Q.LIST_EXISTS_TAC [`b`,`j`] \\ `i <= j` by RANGE_TAC \\ ASM_SIMP_TAC std_ss [] 736 \\ MATCH_MP_TAC EQ_RANGE_THM \\ IMP_RES_TAC move_list_thm); 737 738val one_scratch_def = Define ` 739 one_scratch a (b,e,b2,e2) = 740 one (a + 40w,ref_addr b) * one (a + 44w,ref_addr e) * 741 one (a + 48w,ref_addr b2) * one (a + 52w,ref_addr e2)`; 742 743val ref_mem_LESS_EQ = prove( 744 ``!p x. (ref_mem m b e * p) x ==> b <= e``, 745 completeInduct_on `e - b` \\ NTAC 3 STRIP_TAC \\ Cases_on `e <= b` 746 \\ ONCE_REWRITE_TAC [ref_mem_def] \\ ASM_SIMP_TAC std_ss [cond_STAR] 747 \\ SIMP_TAC std_ss [GSYM STAR_ASSOC] 748 \\ ONCE_REWRITE_TAC [STAR_COMM] \\ SIMP_TAC std_ss [GSYM STAR_ASSOC] 749 \\ Q.ABBREV_TAC `y = MAX 1 (getLENGTH (m b))` 750 \\ `0 < y` by (Q.UNABBREV_TAC `y` \\ FULL_SIMP_TAC std_ss [MAX_DEF] \\ DECIDE_TAC) 751 \\ `e - (b+y)<v /\ (e - (b+y) = e - (b+y))` by DECIDE_TAC 752 \\ REPEAT STRIP_TAC \\ `b+y <= e` by METIS_TAC [] \\ DECIDE_TAC); 753 754val ref_mem_H_EMP = store_thm("ref_mem_H_EMP", 755 ``ref_mem (\a.H_EMP) b e = 756 SEP_EXISTS xs. one_list (ref_addr b) xs * cond (LENGTH xs = (e-b)) * cond (b <= e)``, 757 Induct_on `e-b` THEN1 758 (ONCE_REWRITE_TAC [ref_mem_def] \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 759 \\ REVERSE (Cases_on `b <= e`) 760 THEN1 (`~(b = e)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES]) 761 \\ `(b = e)` by DECIDE_TAC 762 \\ ASM_SIMP_TAC std_ss [FUN_EQ_THM,cond_STAR,SEP_EXISTS_THM,LENGTH_NIL,one_list_def,SEP_CLAUSES]) 763 \\ REPEAT STRIP_TAC 764 \\ ONCE_REWRITE_TAC [ref_mem_def] \\ `~(e <= b)` by DECIDE_TAC 765 \\ ASM_SIMP_TAC std_ss [getLENGTH_def,ref_aux_def,STAR_ASSOC,SEP_CLAUSES] 766 \\ `v = e - (b + 1)` by DECIDE_TAC 767 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES,STAR_ASSOC] 768 \\ SIMP_TAC std_ss [FUN_EQ_THM,SEP_EXISTS_THM] 769 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 770 (Q.EXISTS_TAC `x'::xs` \\ FULL_SIMP_TAC std_ss [one_list_def,STAR_ASSOC, 771 LENGTH,cond_STAR,word_arith_lemma1,GSYM ref_addr_ADD1] \\ DECIDE_TAC) 772 \\ FULL_SIMP_TAC std_ss [cond_STAR] 773 \\ Cases_on `xs` THEN1 (FULL_SIMP_TAC std_ss [LENGTH] \\ `F` by DECIDE_TAC) 774 \\ FULL_SIMP_TAC std_ss [one_list_def,word_arith_lemma1,GSYM ref_addr_ADD1,LENGTH] 775 \\ Q.LIST_EXISTS_TAC [`h`,`t`] \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] \\ DECIDE_TAC); 776 777val ref_aux_IMP = prove( 778 ``!p x. (ref_aux (ref_addr b) (m b) * p) x /\ ok_memory m ==> 779 (ref_mem (\a.H_EMP) b (b + MAX 1 (getLENGTH (m b))) * p) x``, 780 REVERSE (Cases_on `m b`) THEN1 781 (`?x1 x2 x3 x4 x5. p = (x1,x2,x3,x4,x5)` by METIS_TAC [PAIR] 782 \\ FULL_SIMP_TAC std_ss [ref_aux_def,LET_DEF,LENGTH_MAP,getLENGTH_def,MAX_LEMMA] 783 \\ REPEAT STRIP_TAC \\ SIMP_TAC std_ss [ref_mem_H_EMP,SEP_CLAUSES] 784 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_EXISTS_THM,cond_STAR] 785 \\ Q.ABBREV_TAC `y = if x4 then MAP ref_heap_addr x1 else x5` 786 \\ Q.EXISTS_TAC `ref_tag (LENGTH y,x4,x3) :: y` 787 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,one_list_def,STAR_ASSOC] 788 \\ FULL_SIMP_TAC std_ss [ok_memory_def] \\ RES_TAC 789 \\ Q.UNABBREV_TAC `y` \\ METIS_TAC [LENGTH_MAP]) 790 \\ NTAC 2 (ONCE_REWRITE_TAC [ref_mem_def]) 791 \\ SIMP_TAC std_ss [getLENGTH_def,ref_aux_def,DECIDE ``~(b+1<=b)``, 792 SEP_CLAUSES,SEP_EXISTS_THM] \\ METIS_TAC []); 793 794val ref_mem_H_EMP_SPLIT = prove( 795 ``b <= i /\ i <= e ==> 796 (ref_mem (\a. H_EMP) b e = ref_mem (\a. H_EMP) b i * ref_mem (\a. H_EMP) i e)``, 797 Induct_on `i-b` \\ REPEAT STRIP_TAC \\ ONCE_REWRITE_TAC [ref_mem_def] 798 THEN1 (`i = b` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES]) 799 \\ `~(e <= b) /\ ~(i <= b)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 800 \\ SIMP_TAC std_ss [GSYM ref_mem_def,getLENGTH_def] 801 \\ `b + 1 <= i /\ (v = i - (b + 1))` by DECIDE_TAC 802 \\ RES_TAC \\ ASM_SIMP_TAC (std_ss++star_ss) []); 803 804val ref_mem_IMP_H_EMP = prove( 805 ``!m p x. (ref_mem m b e * p) x /\ ok_memory m ==> (ref_mem (\a.H_EMP) b e * p) x``, 806 STRIP_TAC \\ completeInduct_on `e - b` \\ REPEAT STRIP_TAC \\ Cases_on `e <= b` 807 THEN1 (METIS_TAC [ref_mem_def]) 808 \\ Q.PAT_X_ASSUM `(ref_mem m b e * p) x` MP_TAC 809 \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [ref_mem_def])) 810 \\ FULL_SIMP_TAC std_ss [GSYM STAR_ASSOC] \\ REPEAT STRIP_TAC 811 \\ IMP_RES_TAC ref_aux_IMP \\ POP_ASSUM MP_TAC \\ POP_ASSUM (K ALL_TAC) 812 \\ ONCE_REWRITE_TAC [STAR_COMM] \\ SIMP_TAC std_ss [GSYM STAR_ASSOC] 813 \\ Q.ABBREV_TAC `y = MAX 1 (getLENGTH (m b))` 814 \\ `0 < y` by (Q.UNABBREV_TAC `y` \\ FULL_SIMP_TAC std_ss [MAX_DEF] \\ DECIDE_TAC) 815 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC ref_mem_LESS_EQ 816 \\ `e - (b + y) < e - b /\ (e - (b + y) = e - (b + y))` by DECIDE_TAC 817 \\ RES_TAC \\ POP_ASSUM MP_TAC \\ `b <= b + y` by DECIDE_TAC 818 \\ IMP_RES_TAC ref_mem_H_EMP_SPLIT \\ ONCE_ASM_REWRITE_TAC [] 819 \\ SIMP_TAC (std_ss++star_ss) []); 820 821val arm_heap_ok_def = Define ` 822 arm_heap_ok (h,xs) (b,i,j,e,b2,e2,m) (r1,r6,df,f,p,l) = 823 ok_full_heap (h,xs) (b,i,e,b2,e2,m) /\ 824 ALIGNED r1 /\ ALIGNED r6 /\ e2 < 2 ** 30 /\ e < 2 ** 30 /\ ok_memory m /\ 825 (ref_mem m b e * ref_mem m b2 l * one_list_roots r1 xs * 826 one_scratch r6 (b,e,b2,e2) * p) (fun2set (f,df))`; 827 828val arm_gc_lemma = store_thm("arm_gc_lemma", 829 ``arm_heap_ok (h,xs) (b,i,j11,e,b2,e2,m) (r1,r6,df,f,p,i2) ==> 830 (gc(b,e,b2,e2,xs,m) = (b2,i2,e2,b,e,xs2,m2)) ==> 831 ?f2. arm_gc_pre (r1,r6,df,f) /\ 832 (arm_gc (r1,r6,df,f) = (ref_addr i2,r6,df,f2)) /\ 833 (ref_mem m2 b e * ref_mem m2 b2 i2 * one_list_roots r1 xs2 * 834 one_scratch r6 (b2,e2,b,e) * p) (fun2set (f2,df)) /\ ok_memory m2``, 835 STRIP_TAC \\ SIMP_TAC std_ss [LET_DEF,gc_def,arm_gc_def,arm_gc_pre_def] 836 \\ FULL_SIMP_TAC std_ss [arm_heap_ok_def] 837 \\ IMP_RES_TAC ok_full_heap_IMP 838 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED] 839 \\ Q.PAT_ABBREV_TAC `f5 = (r6 + 0x34w =+ f (r6 + 0x2Cw)) xxx` 840 \\ `(ref_mem m b2 i2 * ref_mem m b e * one_list_roots r1 xs * 841 (one_scratch r6 (b2,e2,b,e) * p)) (fun2set (f5,df)) /\ 842 (f (r6 + 0x30w) = ref_addr b2) /\ 843 (f (r6 + 0x28w) = ref_addr b)` by 844 (Q.UNABBREV_TAC `f5` \\ FULL_SIMP_TAC std_ss [one_scratch_def] 845 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 846 \\ Q.PAT_X_ASSUM `Abbrev (f5 = fghfgh)` (K ALL_TAC) 847 \\ `?j m3 xs3. move_list (xs,b2,m) = (xs3,j,m3)` by METIS_TAC [PAIR] 848 \\ `?i4 m4. gc_loop (b2,j,m3) = (i4,m4)` by METIS_TAC [PAIR] 849 \\ ASM_SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [] 850 \\ STRIP_TAC \\ EXPAND_TAC 851 \\ SEP_S_TAC ["gc_inv"] (RW [UNION_EMPTY] 852 (SUBST_INST [``z:num set``|->``{}:num set``] (GEN_ALL arm_move_roots_thm))) 853 \\ ASM_SIMP_TAC std_ss [full_heap_REFL] 854 \\ FULL_SIMP_TAC std_ss [] 855 \\ REPEAT STRIP_TAC 856 \\ IMP_RES_TAC (RW [UNION_EMPTY] (helperLib.SUBST_INST [``z:num set``|->``{}:num set``] move_list_thm)) 857 \\ Q.PAT_X_ASSUM `gc_inv (h,roots,h3,f3) ttt` MP_TAC 858 \\ REPEAT (Q.PAT_X_ASSUM `gc_inv xxx yyy` (K ALL_TAC)) \\ STRIP_TAC 859 \\ IMP_RES_TAC gc_loop_thm 860 \\ Q.PAT_X_ASSUM `r3 = ADDR_MAP f3 roots` MP_TAC 861 \\ REPEAT (Q.PAT_X_ASSUM `r3 = ADDR_MAP xx roots` (K ALL_TAC)) \\ STRIP_TAC 862 \\ `i2 <= e2` by RANGE_TAC \\ FULL_SIMP_TAC std_ss [] \\ CLEAN_TAC 863 \\ `f2 (r6 + 0x28w) = ref_addr b2` by (FULL_SIMP_TAC std_ss [one_scratch_def] \\ SEP_READ_TAC) 864 \\ FULL_SIMP_TAC std_ss [] 865 \\ SEP_S_TAC ["arm_loop","gc_inv"] (GEN_ALL arm_loop_thm) 866 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 867 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ REVERSE STRIP_TAC 868 THEN1 (FULL_SIMP_TAC std_ss [ok_memory_def,CUT_EQ] \\ METIS_TAC []) 869 \\ STRIP_TAC THEN1 (FULL_SIMP_TAC std_ss [one_scratch_def] \\ SEP_READ_TAC) 870 \\ `EQ_RANGE (b2,i2) m4 (CUT (b2,i2) m4)` by METIS_TAC [EQ_RANGE_CUT] 871 \\ IMP_RES_TAC (GSYM EQ_RANGE_ref_mem) \\ ASM_SIMP_TAC std_ss [] 872 \\ NTAC 2 (POP_ASSUM (K ALL_TAC)) 873 \\ `EQ_RANGE (b,e) (CUT (b2,i2) m4) (\a.H_EMP)` by 874 (Q.PAT_X_ASSUM `gc_inv xxx (b2,i2,i2,e2,b,e,m4,{})` MP_TAC 875 \\ SIMP_TAC std_ss [gc_inv_def] 876 \\ SIMP_TAC std_ss [EQ_RANGE_def,IN_DEF] \\ REPEAT STRIP_TAC 877 \\ Cases_on `RANGE (b2,i2) a` \\ ASM_SIMP_TAC std_ss [CUT_def] 878 \\ Q.PAT_X_ASSUM `!k. bbb ==> (m4 k = H_EMP)` MATCH_MP_TAC 879 \\ IMP_RES_TAC full_heap_LESS_EQ \\ RANGE_TAC) 880 \\ IMP_RES_TAC EQ_RANGE_ref_mem \\ ASM_SIMP_TAC std_ss [] 881 \\ SIMP_TAC std_ss [GSYM STAR_ASSOC] \\ MATCH_MP_TAC ref_mem_IMP_H_EMP 882 \\ Q.EXISTS_TAC `m4` \\ FULL_SIMP_TAC (std_ss++star_ss) []); 883 884val _ = export_theory(); 885