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