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