1 2open HolKernel boolLib bossLib Parse; val _ = new_theory "arm_cheney_gc"; 3 4open decompilerLib prog_armLib; 5 6open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 7open combinTheory finite_mapTheory addressTheory; 8open tailrecLib tailrecTheory; 9open cheney_gcTheory; (* an abstract implementation is imported *) 10 11val decompile_arm = decompile arm_tools; 12val basic_decompile_arm = basic_decompile arm_tools; 13 14 15 16infix \\ << >> 17val op \\ = op THEN; 18val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"]; 19val RW = REWRITE_RULE; 20val RW1 = ONCE_REWRITE_RULE; 21 22 23val (th,def1) = decompile_arm "arm_move" ` 24 E3550000 (* cmp r5,#0 *) 25 0A000009 (* beq L1 *) 26 E5957000 (* ldr r7,[r5] *) 27 E3170001 (* tst r7,#1 *) 28 04847004 (* streq r7,[r4],#4 *) 29 05958004 (* ldreq r8,[r5,#4] *) 30 05957008 (* ldreq r7,[r5,#8] *) 31 04848004 (* streq r8,[r4],#4 *) 32 04847004 (* streq r7,[r4],#4 *) 33 0244700B (* subeq r7,r4,#11 *) 34 05857000 (* streq r7,[r5] *) 35 E2475001 (* sub r5,r7,#1 *)`; 36 37val (th,def2) = decompile_arm "arm_move2" ` 38 E3560000 (* cmp r6,#0 *) 39 0A000009 (* beq L2 *) 40 E5967000 (* ldr r7,[r6] *) 41 E3170001 (* tst r7,#1 *) 42 04847004 (* streq r7,[r4],#4 *) 43 05968004 (* ldreq r8,[r6,#4] *) 44 05967008 (* ldreq r7,[r6,#8] *) 45 04848004 (* streq r8,[r4],#4 *) 46 04847004 (* streq r7,[r4],#4 *) 47 0244700B (* subeq r7,r4,#11 *) 48 05867000 (* streq r7,[r6] *) 49 E2476001 (* sub r6,r7,#1 *)`; 50 51val (th,def3) = decompile_arm "arm_cheney_step" ` 52 E5935000 (* ldr r5,[r3] *) 53 E5936004 (* ldr r6,[r3,#4] *) 54 insert: arm_move 55 insert: arm_move2 56 E4835004 (* L2:str r5,[r3],#4 *) 57 E4836004 (* str r6,[r3],#4 *) 58 E2833004 (* add r3,r3,#4 *)`; 59 60val (th,def4) = basic_decompile_arm "arm_cheney_loop"NONE ` 61 E1530004 (* CHENEY:cmp r3,r4 *) 62 0A00001D (* beq EXIT *) 63 insert: arm_cheney_step 64 EAFFFFDF (* b CHENEY *)`; 65 66val (th,def5) = basic_decompile_arm "arm_move_roots" NONE ` 67 E3560000 (* ROOTS:cmp r6,#0 *) 68 0A00000F (* beq CHENEY *) 69 E5995000 (* ldr r5,[r9] *) 70 insert: arm_move 71 E2466001 (* RL:sub r6,r6,#1 *) 72 E4895004 (* str r5,[r9],#4 *) 73 EAFFFFED (* b ROOTS *)`; 74 75val (th,def6) = decompile_arm "arm_c_init" ` 76 E2355001 (* eors r5,r5,#1 *) (* calc u *) 77 E289300C (* add r3,r9,#12 *) (* set i *) 78 00833006 (* addeq r3,r3,r6 *)`; 79 80val (th,def7) = decompile_arm "arm_collect" ` 81 E519501C (* ldr r5,[r9,#-28] *) 82 E5196020 (* ldr r6,[r9,#-32] *) 83 insert: arm_c_init 84 E509501C (* str r5,[r9,#-28] *) 85 E0835006 (* add r5,r3,r6 *) 86 E1A04003 (* mov r4,r3 *) 87 E5895004 (* str r5,[r9,#4] *) 88 E3A06006 (* mov r6,#6 *) 89 E2499018 (* sub r9,r9,#24 *) 90 insert: arm_move_roots 91 insert: arm_cheney_loop (* main loop *) 92 E5994004 (* EXIT:ldr r4,[r9,#4] *)`; 93 94val (th,def8) = decompile_arm "arm_alloc_gc" ` 95 E1530004 (* cmp r3,r4 *) 96 1A00003D (* bne NO_GC *) 97 insert: arm_collect`; 98 99val (th,def9) = decompile_arm "arm_alloc_aux" ` 100 E5197018 (* NO_GC:ldr r7,[r9,#-24] *) 101 E5198014 (* ldr r8,[r9,#-20] *) 102 E3A06000 (* mov r6,#0 *) 103 E1530004 (* cmp r3,r4 *) 104 15093018 (* strne r3,[r9,#-24] *) 105 14837004 (* strne r7,[r3],#4 *) 106 14838004 (* strne r8,[r3],#4 *) 107 14836004 (* strne r6,[r3],#4 *) 108 03A07000 (* moveq r7,#0 *) 109 05097018 (* streq r7,[r9,#-24] *) 110 E5893000 (* str r3,[r9] *)`; 111 112val (th,def10) = decompile_arm "arm_alloc_mem" ` 113 E5993000 (* ldr r3,[r9] *) 114 E5994004 (* ldr r4,[r9,#4] *) 115 insert: arm_alloc_gc 116 insert: arm_alloc_aux`; 117 118val (arm_alloc_thm,def11) = decompile_arm "arm_alloc" ` 119 E5093018 (* str r3,[r9,#-24] *) 120 E5094014 (* str r4,[r9,#-20] *) 121 E5095010 (* str r5,[r9,#-16] *) 122 E509600C (* str r6,[r9,#-12] *) 123 E5097008 (* str r7,[r9,#-8] *) 124 E5098004 (* str r8,[r9,#-4] *) 125 insert: arm_alloc_mem 126 E5193018 (* ldr r3,[r9,#-24] *) 127 E5194014 (* ldr r4,[r9,#-20] *) 128 E5195010 (* ldr r5,[r9,#-16] *) 129 E519600C (* ldr r6,[r9,#-12] *) 130 E5197008 (* ldr r7,[r9,#-8] *) 131 E5198004 (* ldr r8,[r9,#-4] *)`; 132 133val _ = save_thm("arm_alloc_thm",arm_alloc_thm); 134 135 136(* proof *) 137 138val ref_addr_def = Define ` 139 (ref_addr a n = if n = 0 then 0w:word32 else a + n2w (12 * n))`; 140 141val ref_mem_def = Define ` 142 (ref_mem i EMP (a,xs) = T) /\ 143 (ref_mem i (REF j) (a,xs) = 144 (xs (ref_addr a i) = ref_addr a j + 1w)) /\ 145 (ref_mem i (DATA (x,y,z)) (a,xs) = 146 (xs (ref_addr a i) = ref_addr a x) /\ 147 (xs (ref_addr a i + 4w) = ref_addr a y) /\ 148 (xs (ref_addr a i + 8w) = z))`; 149 150val valid_address_def = Define ` 151 valid_address a i = w2n a + 12 * i + 8 < 2**32`; 152 153val ref_set_def = Define ` 154 ref_set a f = { a + n2w (4 * i) | i <= 3 * f + 2 } UNION { a - n2w (4 * i) | i <= 9 }`; 155 156val ref_cheney_def = Define ` 157 ref_cheney (m,e) (a,d,xs,ys) = 158 ~(a = 0w) /\ (a && 3w = 0w) /\ (!i. i <= e ==> ref_mem i (m i) (a,xs)) /\ 159 (m 0 = EMP) /\ valid_address a e /\ (!i. i <+ ref_addr a 1 ==> (xs i = ys i)) /\ 160 (ref_set a e = d)`; 161 162val ref_addr_NOT_ZERO = prove( 163 ``!a. ref_cheney (m,e) (a,d,xs,ys) /\ x <= e /\ ~(x = 0) ==> ~(ref_addr a x = 0w)``, 164 Cases_word \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [ref_cheney_def,ref_addr_def, 165 word_add_n2w,n2w_11,valid_address_def,w2n_n2w] \\ REPEAT STRIP_TAC 166 \\ `(n + 12 * x) < 4294967296` by DECIDE_TAC 167 \\ `n + 12 * x = 0` by METIS_TAC [LESS_MOD] \\ DECIDE_TAC); 168 169val ref_addr_NEQ = store_thm("ref_addr_NEQ", 170 ``!a i j. ~(i = j) /\ valid_address a i /\ valid_address a j ==> 171 ~(ref_addr a i = ref_addr a j)``, 172 Cases_word \\ Cases \\ Cases 173 \\ SIMP_TAC std_ss [ref_addr_def,valid_address_def,word_add_n2w] 174 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,LESS_MOD,n2w_11,DECIDE ``~(SUC n = 0)``] 175 \\ STRIP_TAC \\ IMP_RES_TAC (DECIDE ``m + n + 8 < l ==> m + n + 4 < l /\ m + n < l``) 176 \\ ASM_SIMP_TAC bool_ss [LESS_MOD] \\ DECIDE_TAC); 177 178val ref_addr_ADD_NEQ = store_thm("ref_addr_ADD_NEQ", 179 ``!a i j. valid_address a i /\ valid_address a j ==> 180 ~(ref_addr a i + 4w = ref_addr a j) /\ 181 ~(ref_addr a i + 8w = ref_addr a j) /\ 182 ~(ref_addr a i + 4w = ref_addr a j + 8w)``, 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 ``m + n + 8 < l ==> m + n + 4 < l /\ m + n < l``) 186 \\ ASM_SIMP_TAC bool_ss [LESS_MOD,MULT_CLAUSES] 187 THEN1 DECIDE_TAC THEN1 DECIDE_TAC 188 \\ FULL_SIMP_TAC std_ss [EQ_ADD_LCANCEL,GSYM ADD_ASSOC] \\ REPEAT STRIP_TAC 189 \\ IMP_RES_TAC (METIS_PROVE [] ``(m = n) ==> (m MOD 12 = n MOD 12)``) 190 \\ FULL_SIMP_TAC std_ss [RW1 [MULT_COMM] (CONJ MOD_TIMES MOD_EQ_0)]); 191 192val ALIGNED_ref_addr = store_thm("ALIGNED_ref_addr", 193 ``!n a. ALIGNED a ==> ALIGNED (ref_addr a n)``, 194 Cases \\ REWRITE_TAC [ref_addr_def,ALIGNED_def] THEN1 (STRIP_TAC \\ EVAL_TAC) 195 \\ REWRITE_TAC [GSYM ALIGNED_def,GSYM (EVAL ``4 * 3``),GSYM word_mul_n2w,DECIDE ``~(SUC n = 0)``] 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 = store_thm("ref_cheney_d", 203 ``ref_cheney (m,f) (a,d,xs,ys) /\ ~(x = 0) /\ x <= f ==> 204 ref_addr a x IN d /\ ref_addr a x + 4w IN d /\ ref_addr a x + 8w IN d``, 205 REWRITE_TAC [ref_cheney_def] \\ REPEAT STRIP_TAC 206 \\ Q.PAT_X_ASSUM `ref_set a f = d` (ASSUME_TAC o GSYM) 207 \\ ASM_SIMP_TAC bool_ss [ref_set_def,GSPECIFICATION,IN_UNION,ref_addr_def] 208 \\ DISJ1_TAC 209 THENL [Q.EXISTS_TAC `3*x`,Q.EXISTS_TAC `3*x+1`,Q.EXISTS_TAC `3*x+2`] 210 \\ ASM_SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB, 211 GSYM word_add_n2w,WORD_ADD_ASSOC] \\ DECIDE_TAC); 212 213fun UPDATE_ref_addr_prove (c,tm) = prove(tm, 214 Cases \\ Cases_word \\ REPEAT STRIP_TAC 215 \\ sg c \\ ASM_REWRITE_TAC [APPLY_UPDATE_THM] 216 \\ FULL_SIMP_TAC std_ss [ref_addr_def,EVAL ``1=0``,word_add_n2w,valid_address_def, 217 w2n_n2w,n2w_11,WORD_LO] 218 \\ Q.PAT_X_ASSUM `n < dimword (:32)` ASSUME_TAC 219 \\ Q.PAT_X_ASSUM `n' < dimword (:32)` ASSUME_TAC 220 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [LESS_MOD] 221 \\ `n' + 12 * x < 4294967296` by DECIDE_TAC 222 \\ `n' + 12 * x + 4 < 4294967296` by DECIDE_TAC 223 \\ `n' + 12 < 4294967296` by DECIDE_TAC 224 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [LESS_MOD] \\ DECIDE_TAC); 225 226val UPDATE_ref_addr = UPDATE_ref_addr_prove(`~(ref_addr (n2w n') x = (n2w n))`, 227 ``!i a. valid_address a x /\ 228 ~(x=0) /\ i <+ ref_addr a 1 /\ (xs i = ys i) ==> ((ref_addr a x =+ y) xs i = ys i)``); 229 230val UPDATE_ref_addr4 = UPDATE_ref_addr_prove(`~(ref_addr (n2w n') x + 4w = (n2w n))`, 231 ``!i a. valid_address a x /\ 232 ~(x=0) /\ i <+ ref_addr a 1 /\ (xs i = ys i) ==> ((ref_addr a x + 4w =+ y) xs i = ys i)``); 233 234val UPDATE_ref_addr8 = UPDATE_ref_addr_prove(`~(ref_addr (n2w n') x + 8w = (n2w n))`, 235 ``!i a. valid_address a x /\ 236 ~(x=0) /\ i <+ ref_addr a 1 /\ (xs i = ys i) ==> ((ref_addr a x + 8w =+ y) xs i = ys i)``); 237 238val va_IMP = store_thm("va_IMP", 239 ``!a e i. valid_address a e /\ i <= e ==> valid_address a i``, 240 SIMP_TAC bool_ss [valid_address_def] \\ DECIDE_TAC); 241 242val ref_cheney_update_REF = prove( 243 ``ref_cheney (m,e) (a,d,xs,ys) /\ j <= e /\ x <= e /\ ~(x = 0) ==> 244 ref_cheney ((x =+ REF j) m,e) (a,d,(ref_addr a x =+ ref_addr a j + 1w) xs,ys)``, 245 SIMP_TAC bool_ss [ref_cheney_def] \\ REVERSE (REPEAT STRIP_TAC) 246 THEN1 (MATCH_MP_TAC UPDATE_ref_addr \\ METIS_TAC [va_IMP]) 247 THEN1 ASM_SIMP_TAC bool_ss [UPDATE_def] 248 \\ Cases_on `i = x` \\ ASM_SIMP_TAC bool_ss [UPDATE_def,ref_mem_def] 249 \\ RES_TAC \\ Cases_on `m i` \\ FULL_SIMP_TAC bool_ss [ref_mem_def] 250 \\ `valid_address a i /\ valid_address a x` by METIS_TAC [va_IMP] 251 \\ `~(ref_addr a i = ref_addr a x)` by METIS_TAC [ref_addr_NEQ,va_IMP] 252 \\ ASM_SIMP_TAC bool_ss [] \\ Cases_on `p` \\ Cases_on `r` 253 \\ FULL_SIMP_TAC std_ss [ref_mem_def] \\ METIS_TAC [ref_addr_ADD_NEQ]); 254 255val ref_cheney_move_lemma = prove( 256 ``ref_cheney (m,e) (a,d,xs,ys) /\ (~(x = 0) ==> ~(m x = EMP)) /\ (!x. ~(m x = REF 0)) /\ 257 (move(x,j,m) = (x1,j1,m1)) /\ ~(j = 0) /\ j <= e /\ x <= e /\ 258 (arm_move(ref_addr a j,ref_addr a x,r7,r8,d,xs) = (j2,x2,r7_2,r8_2,d2,xs2)) ==> 259 ref_cheney (m1,e) (a,d,xs2,ys) /\ (x2 = ref_addr a x1) /\ (j2 = ref_addr a j1) /\ (d2 = d) /\ 260 arm_move_pre(ref_addr a j,ref_addr a x,r7,r8, d, xs)``, 261 REWRITE_TAC [move_def] \\ Cases_on `x = 0` THEN1 262 (ASM_SIMP_TAC std_ss [ref_addr_def] \\ REWRITE_TAC [def1] 263 \\ SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 264 \\ SIMP_TAC std_ss [ref_addr_def]) 265 \\ Cases_on `x <= e` \\ ASM_SIMP_TAC bool_ss [] 266 \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] \\ STRIP_TAC 267 \\ `~(ref_addr a x = 0w)` by METIS_TAC [ref_addr_NOT_ZERO] 268 \\ Cases_on `m x` \\ ASM_SIMP_TAC bool_ss [isREF_def,heap_type_11] THEN1 269 (REWRITE_TAC [getREF_def] 270 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [] 271 \\ REWRITE_TAC [def1] 272 \\ SIMP_TAC std_ss [LET_DEF,GSYM AND_IMP_INTRO] \\ NTAC 2 STRIP_TAC 273 \\ ASM_SIMP_TAC std_ss [] 274 \\ `~(xs (ref_addr a x) && 1w = 0w)` by ( 275 FULL_SIMP_TAC bool_ss [ref_cheney_def,ref_mem_def] 276 \\ `ref_mem x (REF n) (a,xs)` by METIS_TAC [] 277 \\ FULL_SIMP_TAC bool_ss [ref_cheney_def,ref_mem_def] 278 \\ MATCH_MP_TAC ALIGNED_add_1_and_1 279 \\ MATCH_MP_TAC ALIGNED_ref_addr 280 \\ ASM_REWRITE_TAC [ALIGNED_def]) 281 \\ ASM_SIMP_TAC std_ss [] 282 \\ `ref_mem x (REF n) (a,xs)` by METIS_TAC [ref_cheney_def] 283 \\ FULL_SIMP_TAC std_ss [ref_mem_def,WORD_ADD_SUB] 284 \\ IMP_RES_TAC ref_cheney_d \\ IMP_RES_TAC ref_cheney_ALIGNED 285 \\ ASM_SIMP_TAC bool_ss [INSERT_SUBSET,EMPTY_SUBSET,ALIGNED_def]) 286 \\ SIMP_TAC std_ss [heap_type_distinct] 287 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [] 288 \\ REWRITE_TAC [def1] 289 \\ SIMP_TAC std_ss [LET_DEF] 290 \\ `~(m x = EMP)` by METIS_TAC [heap_type_distinct] 291 \\ `valid_address a x` by METIS_TAC [ref_cheney_def,va_IMP] 292 \\ ASM_SIMP_TAC std_ss [word_arith_lemma1,WORD_ADD_SUB] 293 \\ `(xs (ref_addr a x) && 1w = 0w)` by 294 (FULL_SIMP_TAC bool_ss [ref_cheney_def] \\ Cases_on `p` \\ Cases_on `r` 295 \\ `ref_mem x (DATA (q,q',r')) (a,xs)` by METIS_TAC [] 296 \\ FULL_SIMP_TAC bool_ss [ref_mem_def] 297 \\ MATCH_MP_TAC ALIGNED_and_1 \\ MATCH_MP_TAC ALIGNED_ref_addr 298 \\ ASM_REWRITE_TAC [ALIGNED_def]) 299 \\ FULL_SIMP_TAC std_ss [PAIR_EQ,WORD_ADD_0,word_arith_lemma4] 300 \\ NTAC 4 STRIP_TAC 301 \\ `~(j = 0)` by METIS_TAC [] 302 \\ IMP_RES_TAC ref_cheney_d \\ IMP_RES_TAC ref_cheney_ALIGNED 303 \\ ASM_SIMP_TAC bool_ss [] 304 \\ REVERSE (STRIP_TAC \\ STRIP_TAC) THEN1 305 (FULL_SIMP_TAC std_ss [GSYM ALIGNED_def,ALIGNED_CLAUSES, 306 SIMP_RULE std_ss [word_mul_n2w] (Q.SPEC `2w` ALIGNED_CLAUSES)] 307 \\ ASM_SIMP_TAC std_ss [ref_addr_def,LEFT_ADD_DISTRIB,GSYM word_add_n2w,WORD_ADD_ASSOC]) 308 \\ MATCH_MP_TAC ref_cheney_update_REF \\ ASM_SIMP_TAC bool_ss [] 309 \\ Cases_on `p` \\ Cases_on `r` \\ FULL_SIMP_TAC std_ss [ref_cheney_def] 310 \\ REVERSE (REPEAT STRIP_TAC) 311 THEN1 312 (`valid_address a j` by METIS_TAC [va_IMP] 313 \\ MATCH_MP_TAC UPDATE_ref_addr8 \\ ASM_SIMP_TAC bool_ss [] 314 \\ MATCH_MP_TAC UPDATE_ref_addr4 \\ ASM_SIMP_TAC bool_ss [] 315 \\ MATCH_MP_TAC UPDATE_ref_addr \\ ASM_SIMP_TAC bool_ss []) 316 THEN1 ASM_SIMP_TAC std_ss [UPDATE_def] 317 \\ `ref_mem x (DATA (q,q',r')) (a,xs)` by METIS_TAC [] 318 \\ Cases_on `i = j` 319 THEN1 (FULL_SIMP_TAC bool_ss [UPDATE_def,ref_mem_def,WORD_EQ_ADD_LCANCEL, 320 RW[WORD_ADD_0](Q.SPECL[`x`,`y`,`0w`]WORD_EQ_ADD_LCANCEL)] 321 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 322 \\ IMP_RES_TAC va_IMP 323 \\ IMP_RES_TAC ref_addr_ADD_NEQ \\ ASM_SIMP_TAC std_ss [] 324 \\ METIS_TAC []) 325 \\ `ref_mem i (m i) (a,xs)` by METIS_TAC [] 326 \\ CONV_TAC (RATOR_CONV (SIMP_CONV std_ss [UPDATE_def])) 327 \\ ASM_SIMP_TAC bool_ss [] 328 \\ Cases_on `m i` 329 \\ 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 \\ RES_TAC \\ `valid_address a i /\ valid_address a j` by METIS_TAC [va_IMP] 332 \\ ASM_SIMP_TAC bool_ss [ref_addr_ADD_NEQ] 333 \\ Cases_on `p` \\ 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_addr a x,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_addr a x2 = xx2) /\ (ref_addr a j2 = xj2) /\ (d = d2) /\ 345 arm_move_pre(ref_addr a j,ref_addr a x, r7,r8, d, xs)``, 346 NTAC 27 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. getDATA (m i) = (x1,y1,d1)` 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 + 12w` 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. m i = DATA(ax,ay,ad)` by METIS_TAC [m_DATA,PAIR] 400 \\ `(x1,y1,d1') = (ax,ay,ad)` by METIS_TAC [getDATA_def] 401 \\ FULL_SIMP_TAC bool_ss [PAIR_EQ] 402 \\ Q.PAT_X_ASSUM `getDATA (DATA (ax,ay,ad)) = (ax,ay,ad)` (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)) (a,xs)` by METIS_TAC [ref_cheney_def] 415 \\ FULL_SIMP_TAC bool_ss [ref_mem_def] 416 \\ `(r51 = ref_addr a ax) /\ (r61 = ref_addr a ay)` 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)) (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 27 STRIP_TAC 464 \\ ONCE_REWRITE_TAC [def4] 465 \\ Cases_on `i = j` THEN1 466 (Q.PAT_X_ASSUM `!m.bb` (K ALL_TAC) 467 \\ FULL_SIMP_TAC std_ss [ref_cheney_inv_def] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 468 \\ METIS_TAC []) 469 \\ Q.PAT_X_ASSUM `ref_cheney_inv (b,i,j,j,e,f,m,x,xx,r) (a,r3,r4,d,xs,ys)` 470 (fn th => STRIP_ASSUME_TAC (RW [ref_cheney_inv_def] th) \\ ASSUME_TAC th) 471 \\ `i <= j /\ j <= e` by METIS_TAC [cheney_inv_def] 472 \\ Cases_on `v = 0` THEN1 `F` by DECIDE_TAC 473 \\ `valid_address a i /\ valid_address a j /\ ~(e < i)` by 474 (FULL_SIMP_TAC bool_ss [valid_address_def] \\ DECIDE_TAC) 475 \\ ASM_REWRITE_TAC [] \\ SIMP_TAC (std_ss++pbeta_ss) [LET_DEF] 476 \\ `?i2 j2 e2 m2. cheney_step (i,j,e,m) = (i2,j2,e2,m2)` by METIS_TAC [PAIR] 477 \\ `?r31 r41 r51 r61 r71 r81 d1 xs1. arm_cheney_step (ref_addr a i,ref_addr a j,r7,r8,d,xs) = 478 (r31,r41,r51,r61,r71,r81,d1,xs1)` by METIS_TAC [PAIR] 479 \\ `~(ref_addr a i = ref_addr a j)` by METIS_TAC [ref_addr_NEQ] 480 \\ ASM_REWRITE_TAC [] 481 \\ STRIP_TAC 482 \\ `e - (i + 1) < v` by DECIDE_TAC 483 \\ Q.PAT_X_ASSUM `!m. m < v ==> !e i. bbb` 484 (ASSUME_TAC o RW [] o Q.SPECL [`e`,`i+1`] o UNDISCH o Q.SPEC `e - (i + 1)`) 485 \\ `ref_cheney_inv (b,i2,j2,j2,e2,f,m2,x,xx,r) (a,r31,r41,d,xs1,ys) /\ (d = d1) /\ 486 arm_cheney_step_pre (r3,r4,r7,r8,d,xs)` by METIS_TAC [ref_cheney_step_thm] 487 \\ `(i2 = i+1) /\ (e2 = e)` by FULL_SIMP_TAC (std_ss++pbeta_ss) [cheney_step_def,LET_DEF] 488 \\ METIS_TAC []); 489 490val SING_IN_SUBSET0 = prove( 491 ``x IN t /\ t SUBSET0 s ==> {x} SUBSET0 s``, 492 SIMP_TAC bool_ss [SUBSET0_DEF,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY]); 493 494val roots_in_mem_def = Define ` 495 (roots_in_mem [] (a,r12,m) = T) /\ 496 (roots_in_mem (x::xs) (a,r12,m) = 497 (m r12 = ref_addr a x) /\ r12 <+ ref_addr a 1 /\ r12 <+ r12 + 4w /\ 498 roots_in_mem xs (a,r12+4w,m))`; 499 500val NOT_ref_addr = prove( 501 ``!x a. valid_address a i /\ x <+ ref_addr a 1 /\ ~(i = 0) ==> 502 ~(x = ref_addr a i) /\ ~(x = ref_addr a i + 4w) /\ ~(x = ref_addr a i + 8w)``, 503 NTAC 2 Cases_word \\ ASM_SIMP_TAC (std_ss++SIZES_ss) 504 [ref_addr_def,word_add_n2w,n2w_11,WORD_LO,w2n_n2w,valid_address_def,LESS_MOD] 505 \\ REPEAT STRIP_TAC 506 \\ `n' + 12 * i < 4294967296 /\ n' + 12 < 4294967296` by DECIDE_TAC 507 \\ `n' + 12 * i + 4 < 4294967296` by DECIDE_TAC 508 \\ FULL_SIMP_TAC std_ss [LESS_MOD] \\ DECIDE_TAC); 509 510val lemma = store_thm("lemma", 511 ``ref_cheney (m1,f) (a,d,xs1,xs) /\ r12 <+ ref_addr a 1 ==> 512 ref_cheney (m1,f) (a,d,(r12 =+ r51) xs1,(r12 =+ r51) xs1)``, 513 SIMP_TAC bool_ss [ref_cheney_def] \\ REPEAT STRIP_TAC 514 \\ Cases_on `m1 i` \\ ASM_REWRITE_TAC [ref_mem_def] THENL [ 515 `ref_addr a n + 1w = xs1 (ref_addr a i)` by METIS_TAC [ref_mem_def] 516 \\ ASM_SIMP_TAC bool_ss [APPLY_UPDATE_THM] 517 \\ METIS_TAC [NOT_ref_addr,va_IMP,heap_type_distinct], 518 Cases_on `p` \\ Cases_on `r` \\ ASM_REWRITE_TAC [ref_mem_def] 519 \\ ASM_SIMP_TAC bool_ss [APPLY_UPDATE_THM] 520 \\ METIS_TAC [NOT_ref_addr,va_IMP,heap_type_distinct,ref_mem_def]]); 521 522val roots_lemma = prove( 523 ``!rs b k. 524 roots_in_mem rs (a,b + k,xs) ==> b <+ b + k ==> 525 ref_cheney (m,f) (a,d,xs1,xs) ==> 526 roots_in_mem rs (a,b + k,(b =+ r51) xs1)``, 527 Induct \\ REWRITE_TAC [roots_in_mem_def] 528 \\ SIMP_TAC std_ss [APPLY_UPDATE_THM,WORD_LOWER_NOT_EQ,GSYM WORD_ADD_ASSOC] 529 \\ REPEAT STRIP_TAC \\ METIS_TAC [ref_cheney_def,WORD_LOWER_TRANS]); 530 531val root_address_ok_def = Define ` 532 (root_address_ok a 0 x = T) /\ 533 (root_address_ok a (SUC n) x = ALIGNED a /\ a IN x /\ root_address_ok (a+4w) n x)`; 534 535val ref_cheney_move_roots = prove( 536 ``!rs zs j m r4 r5 r7 r8 xs r12 ys jn mn. 537 LENGTH rs < 2**32 /\ 538 root_address_ok r12 (LENGTH rs) x /\ 539 roots_in_mem (rs++zs) (a,r12,xs) /\ 540 (!x. MEM x rs ==> {x} SUBSET0 DR0 (ICUT (b,e) m)) /\ 541 ref_cheney_inv (b,i,j,j',e,f,m,(w:num->word32 heap_type),ww,r) (a,r3,r4,x,xs,xs) ==> 542 (arm_move_roots(r4,r5,n2w (LENGTH rs),r7,r8,r12,x,xs) = (r4n,r5n,r6n,r7n,r8n,r12n,xn,xsn)) /\ 543 (move_roots(rs,j,m) = (ys,jn,mn)) ==> 544 arm_move_roots_pre(r4,r5,n2w (LENGTH rs),r7,r8,r12,x,xs) /\ 545 ref_cheney_inv (b,i,jn,j',e,f,mn,w,ww,r) (a,r3,r4n,x,xsn,xsn) /\ 546 roots_in_mem (ys++zs) (a,r12,xsn) /\ 547 (LENGTH ys = LENGTH rs) /\ (r12n = r12 + n2w (4 * LENGTH rs)) /\ 548 (!i. i <+ r12 ==> (xs i = xsn i)) /\ (xn = x)``, 549 STRIP_TAC \\ STRIP_TAC \\ Induct_on `rs` 550 \\ ONCE_REWRITE_TAC [def5] \\ SIMP_TAC std_ss [LET_DEF] 551 THEN1 (Cases_on `ys` \\ REWRITE_TAC [move_roots_def,PAIR_EQ,LENGTH,MAP,NOT_NIL_CONS] 552 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [LENGTH,WORD_MULT_CLAUSES,WORD_ADD_0]) 553 \\ POP_ASSUM (ASSUME_TAC o RW1 [GSYM CONTAINER_def]) 554 \\ SIMP_TAC std_ss [LENGTH,ADD1,DECIDE ``(k + 1 = m + 1 + n) = (k = m + n:num)``,ZIP,APPEND] 555 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LESS_MOD,LENGTH,DECIDE ``~(SUC n = 0)``] 556 \\ SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB] 557 \\ NTAC 12 STRIP_TAC 558 \\ `?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] 559 \\ ASM_REWRITE_TAC [LET_DEF,PAIR_EQ,move_roots_def,APPEND,MAP] 560 \\ `?y1 j1 m1. move (h,j,m) = (y1,j1,m1)` by METIS_TAC [PAIR] 561 \\ `?ys j2 m2. move_roots (rs,j1,m1) = (ys,j2,m2)` by METIS_TAC [PAIR] 562 \\ FULL_SIMP_TAC std_ss [LET_DEF,PAIR_EQ,move_roots_def,GSYM AND_IMP_INTRO,MAP] \\ STRIP_TAC 563 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC bool_ss [] 564 \\ FULL_SIMP_TAC bool_ss [MAP,CONS_11,NOT_NIL_CONS,NOT_CONS_NIL,ZIP,APPEND,ADD1,EQ_ADD_RCANCEL,LENGTH] 565 \\ REPEAT (MATCH_MP_TAC (METIS_PROVE [] ``P ==> (Q ==> P)``)) 566 \\ `LENGTH rs < 4294967296` by DECIDE_TAC 567 \\ FULL_SIMP_TAC bool_ss [roots_in_mem_def,MEM,ref_cheney_inv_def,APPEND] 568 \\ `{h} SUBSET0 DR0 (ICUT(b,e)m)` by METIS_TAC [SING_IN_SUBSET0,IN_INSERT] 569 \\ `arm_move (ref_addr a j,ref_addr a h,r7,r8,x,xs) = (r41,r51,r71,r81,x1,xs1)` by METIS_TAC [WORD_ADD_0] 570 \\ FULL_SIMP_TAC bool_ss [FST,SND] 571 \\ (STRIP_ASSUME_TAC o GSYM o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o 572 Q.SPECL [`a`,`b`,`b`,`i`,`j`,`j1`,`j'`,`e`,`m`,`m1`, 573 `w`,`ww`,`r`,`h`,`r41`,`r51`,`xs`,`xs1`,`x`,`y1`,`hx`,`r7`,`r8`,`r71`,`r81`,`x1`] o Q.INST [`ys`|->`xs`]) (INST_TYPE [``:'a``|->``:word32``] ref_cheney_move) 574 \\ ASM_SIMP_TAC bool_ss [WORD_ADD_0] 575 \\ `!x. MEM x rs ==> {x} SUBSET0 DR0 (ICUT (b,e) m1)` by METIS_TAC [] 576 \\ `ref_cheney (m1,f) (a,x,(r12 =+ r51) xs1,(r12 =+ r51) xs1)` by METIS_TAC [lemma] 577 \\ `roots_in_mem (rs++zs) (a,r12 + 4w,(r12 =+ r51) xs1)` by METIS_TAC [roots_lemma] 578 \\ Q.PAT_X_ASSUM `r51 = ref_addr a y1` ASSUME_TAC \\ FULL_SIMP_TAC bool_ss [] 579 \\ FULL_SIMP_TAC std_ss [root_address_ok_def,ALIGNED_def,GSYM ADD1,move_roots_def] 580 \\ Q.PAT_X_ASSUM `CONTAINER (!j m xs r12. bbb)` 581 (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o 582 Q.SPECL [`j1`,`m1`,`ref_addr a y1`,`r71`,`r81`,`(r12 =+ ref_addr a y1) xs1`,`r12+4w`,`ys'`,`j2`,`m2`] o 583 RW [CONTAINER_def]) 584 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,word_add_n2w,word_mul_n2w, 585 GSYM WORD_ADD_ASSOC,LEFT_ADD_DISTRIB,AC ADD_ASSOC ADD_COMM,FST] 586 \\ METIS_TAC [APPLY_UPDATE_THM,WORD_LOWER_TRANS,WORD_LOWER_NOT_EQ,ref_cheney_def]); 587 588val ref_cheney_move_roots6 = 589 SIMP_RULE std_ss [LENGTH,ADD1,AND_IMP_INTRO,GSYM CONJ_ASSOC] 590 (Q.SPEC `[x1;x2;x3;x4;x5;x6]` ref_cheney_move_roots); 591 592val arm_c_init_lemma = prove( 593 ``(arm_c_init(if u then 0w else 1w,r6,r10) = 594 (r10 + 12w + if u then 0w else r6, if u then 1w else 0w,r6,r10))``, 595 Cases_on `u` \\ SIMP_TAC std_ss [SIMP_RULE std_ss [LET_DEF] def6, 596 WORD_ADD_0,PAIR_EQ,WORD_XOR_CLAUSES,EVAL ``0w = 1w:word32``]); 597 598val arm_coll_inv_def = Define ` 599 arm_coll_inv (a,x,xs) (i,e,rs,l,u,m) = 600 ?x1 x2 x3 x4 x5 x6. 601 roots_in_mem (rs ++ [i;e]) (a,a-24w,xs) /\ 602 (rs = [x1;x2;x3;x4;x5;x6]) /\ 603 valid_address a (l + l + 1) /\ 604 ref_cheney (m,l+l+1) (a,x,xs,xs) /\ 605 (xs (a-28w) = if u then 0w else 1w) /\ a - 28w <+ ref_addr a 1 /\ a - 28w <+ a - 24w /\ 606 (xs (a-32w) = n2w (12 * l)) /\ a - 32w <+ ref_addr a 1 /\ a - 32w <+ a - 24w`; 607 608val roots_in_mem_carry_over = prove( 609 ``!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)``, 610 Induct \\ FULL_SIMP_TAC bool_ss [roots_in_mem_def,ref_cheney_def] \\ METIS_TAC []); 611 612val arm_coll_inv_pre_lemma = store_thm("arm_coll_inv_pre_lemma", 613 ``arm_coll_inv (a,x,xs) (q,e,rs,l,u,m) ==> 614 {a+4w;a-32w;a-28w;a-24w;a-20w;a-16w;a-12w;a-8w;a-4w;a} SUBSET x /\ 615 !i. i IN {a+4w;a-32w;a-28w;a-24w;a-20w;a-16w;a-12w;a-8w;a-4w;a} ==> ALIGNED i``, 616 REWRITE_TAC [arm_coll_inv_def,ref_cheney_def] \\ REPEAT STRIP_TAC THENL [ 617 Q.PAT_X_ASSUM `ref_set a (l + l + 1) = x` (ASSUME_TAC o GSYM) 618 \\ ASM_SIMP_TAC bool_ss [INSERT_SUBSET,EMPTY_SUBSET,ref_set_def,IN_UNION] 619 \\ REPEAT STRIP_TAC 620 THEN1 (DISJ1_TAC \\ SIMP_TAC std_ss [GSPECIFICATION] 621 \\ Q.EXISTS_TAC `1` \\ SIMP_TAC std_ss [] \\ DECIDE_TAC) 622 \\ DISJ2_TAC \\ SIMP_TAC std_ss [GSPECIFICATION] 623 THEN1 (Q.EXISTS_TAC `8` \\ SIMP_TAC std_ss []) 624 THEN1 (Q.EXISTS_TAC `7` \\ SIMP_TAC std_ss []) 625 THEN1 (Q.EXISTS_TAC `6` \\ SIMP_TAC std_ss []) 626 THEN1 (Q.EXISTS_TAC `5` \\ SIMP_TAC std_ss []) 627 THEN1 (Q.EXISTS_TAC `4` \\ SIMP_TAC std_ss []) 628 THEN1 (Q.EXISTS_TAC `3` \\ SIMP_TAC std_ss []) 629 THEN1 (Q.EXISTS_TAC `2` \\ SIMP_TAC std_ss []) 630 THEN1 (Q.EXISTS_TAC `1` \\ SIMP_TAC std_ss []) 631 THEN1 (Q.EXISTS_TAC `0` \\ SIMP_TAC (std_ss++WORD_ss) []), 632 FULL_SIMP_TAC bool_ss [IN_INSERT,NOT_IN_EMPTY] 633 \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,word_arith_lemma1,word_arith_lemma2] 634 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,GSYM ALIGNED_def] 635 \\ REWRITE_TAC [word_sub_def] \\ REPEAT STRIP_TAC 636 \\ MATCH_MP_TAC ALIGNED_ADD \\ ASM_SIMP_TAC bool_ss [] \\ EVAL_TAC]); 637 638val arm_collect_lemma = store_thm("arm_collect_lemma", 639 ``ok_state (i,e,rs,l,u,m) ==> 640 arm_coll_inv (a,x,xs) (i,e,rs,l,u,m) ==> 641 (cheney_collector (i,e,rs,l,u,m) = (i',e',rs',l',u',m')) ==> 642 (arm_collect (r7,r8,a,x,xs) = (r3',r4',r5',r6',r7',r8',a',x',xs')) ==> 643 arm_collect_pre (r7,r8,a,x,xs) /\ 644 arm_coll_inv (a,x,xs') (i,e',rs',l',u',m') /\ (x = x') /\ 645 (r3' = ref_addr a i') /\ (r4' = ref_addr a e') /\ (a = a') /\ (l = l')``, 646 STRIP_TAC \\ STRIP_TAC \\ IMP_RES_TAC arm_coll_inv_pre_lemma 647 \\ ONCE_REWRITE_TAC [def7] 648 \\ FULL_SIMP_TAC bool_ss [GSYM AND_IMP_INTRO,arm_coll_inv_def] 649 \\ POP_ASSUM (STRIP_ASSUME_TAC o RW [arm_coll_inv_def]) 650 \\ ASM_SIMP_TAC bool_ss [LET_DEF] 651 \\ ASM_SIMP_TAC std_ss [arm_c_init_lemma] 652 \\ Q.ABBREV_TAC `xs1 = (a - 28w =+ (if u then 1w else 0w)) xs` 653 \\ Q.ABBREV_TAC `r4l = a + 12w + (if u then 0w else n2w (12 * l))` 654 \\ Q.ABBREV_TAC `xs2 = (a + 4w =+ r4l + n2w (12 * l)) xs1` 655 \\ `?r43 r53 r63 r73 r83 a3 x3 xs3. 656 arm_move_roots (r4l,r4l + n2w (12 * l),6w,r7,r8,a - 24w,x,xs2) = 657 (r43,r53,r63,r73,r83,a3,x3,xs3)` by METIS_TAC [PAIR] 658 \\ `?r34 r44 r54 r64 r74 r84 x4 xs4. arm_cheney_loop (r4l,r43,r53,r63,r73,r83,x3',xs3) = 659 (r34,r44,r54,r64,r74,r84,x4,xs4)` by METIS_TAC [PAIR] 660 \\ ASM_SIMP_TAC std_ss [LET_DEF,cheney_collector_def] 661 \\ Q.ABBREV_TAC `b = if ~u then 1 + l else 1` 662 \\ `?ys j2 m2. move_roots ([x1; x2; x3; x4; x5; x6],b,m) = (ys,j2,m2)` by METIS_TAC [PAIR] 663 \\ `?i3 m3. cheney (b,j2,b + l,m2) = (i3,m3)` by METIS_TAC [PAIR] 664 \\ ASM_SIMP_TAC std_ss [] 665 \\ ASM_SIMP_TAC std_ss [LET_DEF] 666 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 667 \\ REPEAT (MATCH_MP_TAC (METIS_PROVE [] ``P ==> (Q ==> P)``)) 668 \\ `roots_in_mem (rs ++ [i;e]) (a,a - 24w,xs1)` by 669 (Q.UNABBREV_TAC `xs1` 670 \\ FULL_SIMP_TAC bool_ss [APPEND,roots_in_mem_def,APPLY_UPDATE_THM,ZIP] 671 \\ SIMP_TAC (std_ss++WORD_ss) [WORD_EQ_ADD_LCANCEL,n2w_11, 672 RW [WORD_ADD_0] (Q.SPECL [`v`,`w`,`0w`] WORD_EQ_ADD_LCANCEL)]) 673 \\ Q.PAT_X_ASSUM `roots_in_mem ppp (aaa,bbb,xs)` (K ALL_TAC) 674 \\ Q.PAT_X_ASSUM `rs = ppppp` ASSUME_TAC 675 \\ Q.PAT_X_ASSUM `rs2 = ppppp` ASSUME_TAC 676 \\ `roots_in_mem (rs ++ [i;b+l]) (a,a - 24w,xs2) /\ a + 4w <+ ref_addr a 1` by 677 (Q.UNABBREV_TAC `xs2` \\ Q.UNABBREV_TAC `b` 678 \\ FULL_SIMP_TAC bool_ss [APPEND,roots_in_mem_def,APPLY_UPDATE_THM,ZIP] 679 \\ FULL_SIMP_TAC (std_ss++WORD_ss) [WORD_EQ_ADD_LCANCEL,n2w_11, 680 RW [WORD_ADD_0] (Q.SPECL [`v`,`w`,`0w`] WORD_EQ_ADD_LCANCEL)] 681 \\ Q.UNABBREV_TAC `r4l` \\ Cases_on `u` 682 \\ SIMP_TAC std_ss [ref_addr_def,DECIDE ``~(m+1 = 0)``,GSYM WORD_ADD_ASSOC, 683 word_add_n2w,LEFT_ADD_DISTRIB,AC ADD_COMM ADD_ASSOC]) 684 \\ IMP_RES_TAC (SIMP_RULE std_ss [LET_DEF] ok_state_IMP_cheney_inv) 685 \\ Q.UNABBREV_TAC `b` 686 \\ Q.ABBREV_TAC `b = if ~u then 1 + l else 1` 687 \\ Q.PAT_X_ASSUM `rs = [x1; x2; x3; x4; x5; x6]` ASSUME_TAC 688 \\ FULL_SIMP_TAC bool_ss [] 689 \\ `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 690 (ASM_REWRITE_TAC [ref_cheney_inv_def,CONJ_ASSOC] 691 \\ Q.UNABBREV_TAC `r4l` \\ Q.UNABBREV_TAC `b` \\ REVERSE STRIP_TAC 692 THEN1 (Cases_on `u` \\ SIMP_TAC std_ss [ref_addr_def,WORD_ADD_0, 693 LEFT_ADD_DISTRIB,GSYM word_add_n2w,WORD_ADD_ASSOC]) 694 \\ REVERSE STRIP_TAC 695 THEN1 (Cases_on `u` \\ FULL_SIMP_TAC bool_ss [valid_address_def] \\ DECIDE_TAC) 696 \\ Q.UNABBREV_TAC `xs2` 697 \\ Q.UNABBREV_TAC `xs1` 698 \\ MATCH_MP_TAC (Q.GEN `xs` lemma) \\ ASM_SIMP_TAC bool_ss [] 699 \\ Q.EXISTS_TAC `(a - 28w =+ (if u then 1w else 0w)) xs` 700 \\ MATCH_MP_TAC lemma \\ ASM_SIMP_TAC bool_ss []) 701 \\ FULL_SIMP_TAC bool_ss [APPEND] 702 \\ `root_address_ok (a - 24w) 6 x /\ a - 28w IN x /\ a - 32w IN x /\ a + 4w IN x /\ 703 ALIGNED (a-32w) /\ ALIGNED (a-28w) /\ ALIGNED (a+4w)` by 704 (REWRITE_TAC [GSYM (EVAL ``(SUC(SUC(SUC(SUC(SUC(SUC 0))))))``),root_address_ok_def] 705 \\ FULL_SIMP_TAC bool_ss [ref_cheney_def,IN_INSERT] 706 \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,word_arith_lemma1,word_arith_lemma2] 707 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4] \\ METIS_TAC []) 708 \\ FULL_SIMP_TAC bool_ss [] 709 \\ STRIP_ASSUME_TAC 710 ((UNDISCH_ALL o Q.INST [`f`|->`l+l+1`]) 711 (Q.INST [`r5n`|->`r53`,`r6n`|->`r63`,`r7n`|->`r73`,`r8n`|->`r83`,`xn`|->`x3'`] 712 (Q.SPECL [`b`,`m`,`r4l`,`r4l + n2w (12 * l)`,`r7`,`r8`,`xs2`,`a - 24w`,`ys`,`j2`,`m2`] 713 (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`] 714 (SIMP_RULE std_ss [APPEND,GSYM AND_IMP_INTRO,LENGTH,ADD1] (Q.SPEC `[ii;e]` ref_cheney_move_roots6)))))) 715 \\ `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 716 (REWRITE_TAC [ref_cheney_inv_def] \\ REPEAT STRIP_TAC THENL [ 717 FULL_SIMP_TAC bool_ss [ref_cheney_inv_def] \\ IMP_RES_TAC cheney_inv_setup 718 \\ FULL_SIMP_TAC bool_ss [cheney_inv_def] \\ METIS_TAC [], 719 FULL_SIMP_TAC bool_ss [ref_cheney_inv_def], 720 MATCH_MP_TAC va_IMP \\ Q.EXISTS_TAC `l+l+1` \\ ASM_SIMP_TAC bool_ss [] 721 \\ Q.UNABBREV_TAC `b` \\ Cases_on `u` \\ REWRITE_TAC [] \\ DECIDE_TAC, 722 FULL_SIMP_TAC bool_ss [ref_cheney_inv_def], 723 FULL_SIMP_TAC bool_ss [ref_cheney_inv_def]]) 724 \\ `ref_cheney_inv (b,b,j2,j2,b + l,l + l + 1,m2,m2,m,RANGE (b,j2)) 725 (a,r4l,r43,x3',xs3,xs3)` by METIS_TAC [] 726 \\ (STRIP_ASSUME_TAC o 727 UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o 728 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 729 Q.INST [`xx`|->`m`,`ys`|->`xs3`,`f`|->`l+l+1`,`d`|->`x`]) 730 (INST_TYPE [``:'a``|->``:word32``] ref_cheney_loop_th) 731 \\ Q.PAT_X_ASSUM `ref_cheney_inv ppppp (a,r34,r44,x3',xs4,xs3)` (STRIP_ASSUME_TAC o RW [ref_cheney_inv_def]) 732 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 733 \\ ASM_SIMP_TAC bool_ss [WORD_SUB_ADD,GSYM ALIGNED_def] 734 \\ SIMP_TAC std_ss [def6,LET_DEF] 735 \\ `?x1' x2' x3' x4' x5' x6'. ys = [x1'; x2'; x3'; x4'; x5'; x6']` by 736 (Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH] 737 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH] 738 \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH] 739 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH] 740 \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH] 741 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH] 742 \\ Cases_on `t'` \\ FULL_SIMP_TAC std_ss [LENGTH,CONS_11,ADD1,GSYM ADD_ASSOC] 743 \\ FULL_SIMP_TAC bool_ss [DECIDE ``~(n + 7 = 6)``]) 744 \\ FULL_SIMP_TAC bool_ss [CONS_11,APPEND] 745 \\ `xs4 (a-28w) = xs2 (a-28w)` by METIS_TAC [ref_cheney_def] 746 \\ `xs4 (a-32w) = xs2 (a-32w)` by METIS_TAC [ref_cheney_def] 747 \\ Q.PAT_X_ASSUM ` !i. i <+ a - 24w ==> (xs2 i = xs3 i)` (ASSUME_TAC o GSYM) 748 \\ `~(b = 0) /\ ~(b + l = 0)` by 749 (Q.UNABBREV_TAC `b` \\ Cases_on `u` \\ FULL_SIMP_TAC std_ss [LET_DEF,ok_state_def] \\ DECIDE_TAC) 750 \\ `(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] 751 \\ REWRITE_TAC [GSYM CONJ_ASSOC] 752 \\ STRIP_TAC THEN1 METIS_TAC [roots_in_mem_carry_over] 753 \\ REVERSE STRIP_TAC THENL [ 754 `(xs4 (a - 32w) = xs3 (a - 32w)) /\ (xs4 (a + 4w) = xs3 (a + 4w)) /\ 755 (xs4 (a - 28w) = xs3 (a - 28w))` by METIS_TAC [ref_cheney_def] 756 \\ ASM_SIMP_TAC bool_ss [] 757 \\ Q.UNABBREV_TAC `xs2` \\ Q.UNABBREV_TAC `xs1` \\ Cases_on `u` 758 \\ FULL_SIMP_TAC (std_ss++WORD_ss) [APPLY_UPDATE_THM,WORD_EQ_ADD_LCANCEL,n2w_11, 759 RW [WORD_ADD_0] (Q.SPECL [`v`,`w`,`0w`] WORD_EQ_ADD_LCANCEL)], 760 FULL_SIMP_TAC bool_ss [ref_cheney_def,CUT_def] 761 \\ FULL_SIMP_TAC bool_ss [ref_cheney_def,GSYM CUT_def] 762 \\ METIS_TAC [ref_mem_def]]); 763 764 765val _ = export_theory(); 766