machine-code/garbage-collectors/arm_improved_gcScript.sml

188   ``~(RANGE (b2,e2) j) ==>
189     (ref_mem ((j =+ x) m) b2 e2 = ref_mem m b2 e2)``,
190   completeInduct_on `e2-b2` \\ REPEAT STRIP_TAC
192   \\ Cases_on `e2<=b2` \\ ASM_SIMP_TAC std_ss []
193   \\ `~(b2 = j)` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC)
195   \\ Q.ABBREV_TAC `y = MAX 1 (getLENGTH (m b2))`
197   \\ `e2 - (b2 + y) < e2 - b2` by DECIDE_TAC
198   \\ `~RANGE (b2+y,e2) j` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC)
348   ``gc_inv (h1,roots1,h,ff) (b,i,j,e,b2,e2,m,z UNION ADDR_SET [x]) /\ j2 <= je /\ je <= e /\
349     (ADDR_SET [x]) SUBSET (DR0(CUT(b2,e2)m)) /\ ALIGNED r1 /\ b <= ij /\ ij <= j /\
350     (one (r1,ref_heap_addr x) * ref_mem m ij je * ref_mem m b2 e2 * p) (fun2set (f,df)) /\
354          (one (r1,ref_heap_addr x2) * ref_mem m2 ij je * ref_mem m2 b2 e2 * p) (fun2set (f2,df)) /\
376     \\ `RANGE (b2,e2) n` by FULL_SIMP_TAC std_ss [IN_DEF,R0_def,D0_def,DR0_def,CUT_EQ]
381   \\ `~RANGE (b2,e2) j /\ ~RANGE (ij,je) n /\ n < e2` by RANGE_TAC
392   \\ `?len. part_heap b2 e2 m len` by METIS_TAC [gc_inv_def]
393   \\ `?len2. part_heap b2 e2 ((n =+ H_REF j) m) len2` by
395   \\ `RANGE (b2,e2) n` by FULL_SIMP_TAC std_ss [IN_DEF,R0_def,D0_def,DR0_def,CUT_EQ]
398   \\ `~(RANGE(b2,n)n) /\ ~(RANGE(n+1,e2)n) /\ ~(RANGE(j+MAX 1 (x + 1),je)j) /\
427        ref_mem m (j + 1) je * ref_mem m b2 n *
447         ref_mem m b2 n * one (ref_addr n,ref_addr j) *
499       ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m) /\ ALIGNED r1 /\
501       gc_inv (h1,roots1,h,f8) (b,i,j,e,b2,e2,m,z UNION ADDR_SET xs) /\ e < 2**30 /\ LENGTH xs < 2**32 /\
502       (ref_mem m ij je * ref_mem m b2 e2 * one_list r1 (MAP ref_heap_addr xs) * p) (fun2set (f,df)) /\
507         (ref_mem m2 ij je * ref_mem m2 b2 e2 * one_list r1 (MAP ref_heap_addr ys) * p) (fun2set (f2,df)) /\
509                            (b,i,j2,e,b2,e2,m2,z UNION D1 (CUT (j,j2) m2)) /\
521   \\ `ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m3)` by METIS_TAC [SUBSET_TRANS]
552       ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m) /\ ALIGNED r1 /\
554       gc_inv (h1,roots1,h,f8) (b,i,j,e,b2,e2,m,z UNION ADDR_SET xs) /\ e < 2**30 /\
555       (ref_mem m ij je * ref_mem m b2 e2 * one_list_roots r1 xs * p) (fun2set (f,df)) /\
560            (ref_mem m2 ij je * ref_mem m2 b2 e2 * one_list_roots r1 ys * p) (fun2set (f2,df)) /\
562                            (b,i,j2,e,b2,e2,m2,z UNION D1 (CUT (j,j2) m2))``,
574   \\ `ADDR_SET xs SUBSET DR0 (CUT (b2,e2) m3)` by METIS_TAC [SUBSET_TRANS]
612   ``!f m j h8 f8. gc_inv (h1,roots1,h8,f8) (b,i,j,e,b2,e2,m,D1 (CUT (i,j) m)) /\
614     (ref_mem m b i2 * ref_mem m b2 e2 * p) (fun2set (f,df)) /\
618          (ref_mem m2 b i2 * ref_mem m2 b2 e2 * p) (fun2set (f2,df)) /\ ok_memory m2``,
685        (ref_mem m3 (i + LENGTH xs + 1) i2 * ref_mem m3 b2 e2 *
690          (b,i,j8,e,b2,e2,m3,D1 (CUT (i+LENGTH xs+1,j) m) UNION D1 (CUT (j,j8) m3)) /\
708   \\ SUBGOAL `(ref_mem m8 b i2 * ref_mem m8 b2 e2 * p) (fun2set (f2,df)) /\
726   \\ `~(RANGE (b,i) i) /\ ~(RANGE (i8,i2) i) /\ ~(RANGE (b2,e2) i)`
740   one_scratch a (b,e,b2,e2) =
742     one (a + 48w,ref_addr b2) * one (a + 52w,ref_addr e2)`;
823   arm_heap_ok (h,xs) (b,i,j,e,b2,e2,m) (r1,r6,df,f,p,l) =
824     ok_full_heap (h,xs) (b,i,e,b2,e2,m) /\
826     (ref_mem m b e * ref_mem m b2 l * one_list_roots r1 xs *
827      one_scratch r6 (b,e,b2,e2) * p) (fun2set (f,df))`;
830   ``arm_heap_ok (h,xs) (b,i,j11,e,b2,e2,m) (r1,r6,df,f,p,i2) ==>
831     (gc(b,e,b2,e2,xs,m) = (b2,i2,e2,b,e,xs2,m2)) ==>
834          (ref_mem m2 b e * ref_mem m2 b2 i2 * one_list_roots r1 xs2 *
835           one_scratch r6 (b2,e2,b,e) * p) (fun2set (f2,df)) /\ ok_memory m2``,
841   \\ `(ref_mem m b2 i2 * ref_mem m b e * one_list_roots r1 xs *
842          (one_scratch r6 (b2,e2,b,e) * p)) (fun2set (f5,df)) /\
843       (f (r6 + 0x30w) = ref_addr b2) /\
848   \\ `?j m3 xs3. move_list (xs,b2,m) = (xs3,j,m3)` by METIS_TAC [PAIR]
849   \\ `?i4 m4. gc_loop (b2,j,m3) = (i4,m4)` by METIS_TAC [PAIR]
864   \\ `f2 (r6 + 0x28w) = ref_addr b2` by (FULL_SIMP_TAC std_ss [one_scratch_def] \\ SEP_READ_TAC)
871   \\ `EQ_RANGE (b2,i2) m4 (CUT (b2,i2) m4)` by METIS_TAC [EQ_RANGE_CUT]
874   \\ `EQ_RANGE (b,e) (CUT (b2,i2) m4) (\a.H_EMP)` by
875     (Q.PAT_X_ASSUM `gc_inv xxx (b2,i2,i2,e2,b,e,m4,{})` MP_TAC
878      \\ Cases_on `RANGE (b2,i2) a` \\ ASM_SIMP_TAC std_ss [CUT_def]