1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_parse"; 2 3open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 4open combinTheory finite_mapTheory addressTheory stringTheory helperLib; 5 6open compilerLib; 7open lisp_gcTheory lisp_typeTheory lisp_invTheory; 8 9 10infix \\ 11val op \\ = op THEN; 12val RW = REWRITE_RULE; 13val RW1 = ONCE_REWRITE_RULE; 14 15 16(* setting up the compiler *) 17val _ = codegen_x86Lib.set_x86_regs 18 [(3,"eax"),(4,"ecx"),(5,"edx"),(6,"ebx"),(7,"edi"),(8,"esi"),(9,"ebp")] 19 20(* --- READ NUMBER --- *) 21 22val (th1,arm_read_loop_def,arm_read_loop_pre_def) = compile_all `` 23 arm_read_loop (r3:word32,r4:word32,r5:word32,df:word32 set,f:word32->word8) = 24 (let r6 = r3 << 2 in 25 let r3 = r3 + r6 in 26 let r3 = r3 + r3 in 27 let r3 = r3 + r4 in 28 let r6 = w2w (f (r5 + 0x1w)) in 29 let r5 = r5 + 0x1w in 30 let r4 = r6 - 0x30w in 31 if ~(r6 <+ 0x30w) then 32 if ~(r4 <+ 0xAw) then 33 (let r4 = r4 + 0x30w in (r3,r4,r5,r6,df,f)) 34 else 35 arm_read_loop (r3,r4,r5,df,f) 36 else 37 (let r4 = r4 + 0x30w in (r3,r4,r5,r6,df,f)))`` 38 39val (th1,arm_readnum_def,arm_readnum_pre_def) = compile_all `` 40 arm_readnum (r4:word32,r5:word32,df:word32 set,f:word32->word8) = 41 let r3 = 0x0w:word32 in 42 let r4 = r4 - 0x30w in 43 let (r3,r4,r5,r6,df,f) = arm_read_loop (r3,r4,r5,df,f) in 44 (r3,r4,r5,r6,df,f)``; 45 46val number_char_def = Define ` 47 number_char c = 48 <= ORD c /\ ORD c < 58`; 48 49val is_number_string_def = Define ` 50 is_number_string s = EVERY number_char (EXPLODE s)`; 51 52val dec2str_def = Define `dec2str n = STRING (CHR (n + 48)) ""`; 53 54val num2str_def = tDefine "num2str" ` 55 num2str n = 56 if n DIV 10 = 0 then dec2str (n MOD 10) else 57 STRCAT (num2str (n DIV 10)) (dec2str (n MOD 10))` 58 (Q.EXISTS_TAC `measure I` 59 \\ SIMP_TAC std_ss [prim_recTheory.WF_measure] 60 \\ SIMP_TAC std_ss [prim_recTheory.measure_thm] 61 \\ STRIP_TAC 62 \\ STRIP_ASSUME_TAC (Q.SPEC `n` (MATCH_MP DA (DECIDE ``0 < 10:num``))) 63 \\ ASM_SIMP_TAC std_ss [DIV_MULT] 64 \\ DECIDE_TAC); 65 66val str2dec_def = Define ` 67 str2dec c = ORD c - 48`; 68 69val str2num_def = Define ` 70 (str2num "" = 0) /\ 71 (str2num (STRING c s) = (ORD c - 48) * 10 ** (LENGTH s) + str2num s)`; 72 73val str2num_dec2str = prove( 74 ``!n. n < 10 ==> (str2num (dec2str n) = n) /\ ~(dec2str n = "") /\ 75 EVERY (\c. 48 <= ORD c /\ ORD c < 58) (EXPLODE (dec2str n))``, 76 SRW_TAC [] [dec2str_def,str2num_def,LENGTH,ORD_CHR] 77 \\ `n + 48 < 256` by DECIDE_TAC 78 \\ IMP_RES_TAC ORD_CHR 79 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 80 81val EXPLODE_STRCAT = store_thm("EXPLODE_STRCAT", 82 ``!s t. EXPLODE (STRCAT s t) = EXPLODE s ++ EXPLODE t``, 83 Induct THEN ASM_SIMP_TAC std_ss [STRCAT_def,EXPLODE_def,APPEND]) 84 85val LENGTH_STRCAT = store_thm("LENGTH_STRCAT", 86 ``!x y. LENGTH (STRCAT x y) = LENGTH x + LENGTH y``, 87 Induct THEN ASM_SIMP_TAC std_ss [LENGTH,STRCAT_def,ADD_ASSOC, 88 DECIDE ``SUC n = 1 + n``]); 89 90val str2num_STRCAT = prove( 91 ``!s c. str2num (STRCAT s (STRING c "")) = str2num s * 10 + str2num (STRING c "")``, 92 Induct \\ ASM_SIMP_TAC std_ss [str2num_def,STRCAT_def,LENGTH_STRCAT, 93 LENGTH,EXP_ADD,RIGHT_ADD_DISTRIB,AC MULT_ASSOC MULT_COMM, AC ADD_ASSOC ADD_COMM]); 94 95val dec2str_lemma = prove( 96 ``?c. dec2str r = STRING c ""``, 97 SRW_TAC [] [dec2str_def,str2num_def,LENGTH]); 98 99val str2num_num2str = prove( 100 ``!n. (str2num (num2str n) = n) /\ ~((num2str n) = "") /\ 101 EVERY (\c. 48 <= ORD c /\ ORD c < 58) (EXPLODE (num2str n))``, 102 completeInduct_on `n` \\ Cases_on `n < 10` THENL [ 103 IMP_RES_TAC LESS_DIV_EQ_ZERO \\ ONCE_REWRITE_TAC [num2str_def] 104 \\ ASM_SIMP_TAC std_ss [str2num_dec2str], 105 STRIP_ASSUME_TAC (Q.SPEC `n` (MATCH_MP DA (DECIDE ``0 < 10:num``))) 106 \\ ONCE_REWRITE_TAC [num2str_def] 107 \\ ASM_SIMP_TAC std_ss [DIV_MULT] 108 \\ Cases_on `q = 0` THEN1 (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 109 \\ ASM_SIMP_TAC std_ss [MOD_TIMES,STRCAT_EQ_EMPTY,EXPLODE_STRCAT,EVERY_APPEND] 110 \\ ASM_SIMP_TAC std_ss [str2num_dec2str,str2num_STRCAT] 111 \\ `q < n` by DECIDE_TAC \\ RES_TAC 112 \\ STRIP_ASSUME_TAC dec2str_lemma 113 \\ ASM_SIMP_TAC std_ss [str2num_STRCAT] 114 \\ METIS_TAC [str2num_dec2str]]); 115 116val arm_read_loop_lemma = (RW [markerTheory.Abbrev_def] o prove)( 117 ``!s a k. 118 EVERY number_char (EXPLODE s) /\ ~(s = "") /\ 119 string_mem (STRCAT s (STRING c1 s1)) (a,f,df) /\ 120 Abbrev ~(number_char c1) ==> 121 arm_read_loop_pre (n2w k,w2w (f a) - 48w,a,df,f) /\ 122 ?x. arm_read_loop (n2w k,w2w (f a) - 48w,a,df,f) = 123 (n2w (k * 10 ** LENGTH s + str2num s), 124 w2w (f (a + n2w (LENGTH s))),a + n2w (LENGTH s),x,df,f)``, 125 Induct \\ FULL_SIMP_TAC bool_ss [NOT_CONS_NIL] 126 \\ SIMP_TAC std_ss [EXPLODE_def,EVERY_DEF,STRCAT_def,string_mem_def] 127 \\ NTAC 4 STRIP_TAC 128 \\ `ORD h < 256 /\ ORD c1 < 256` by REWRITE_TAC [ORD_BOUND] 129 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,w2w_def,ORD_BOUND] 130 \\ ONCE_REWRITE_TAC [arm_read_loop_pre_def,arm_read_loop_def] 131 \\ FULL_SIMP_TAC std_ss [LET_DEF,WORD_SUB_ADD,number_char_def] 132 \\ SIMP_TAC std_ss [WORD_MUL_LSL,word_add_n2w,word_mul_n2w, 133 DECIDE ``(k + 4 * k + (k + 4 * k) = 10 * k:num)``] 134 \\ `~(ORD h < 48)` by DECIDE_TAC 135 \\ ASM_SIMP_TAC std_ss [word_arith_lemma2,word_add_n2w] 136 \\ Cases_on `s` 137 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [STRCAT_def,string_mem_def,w2w_def,w2n_n2w] 138 THEN1 139 (`ORD c1 < 4294967296 /\ ORD c1 - 48 < 4294967296` by DECIDE_TAC 140 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_LO,w2n_n2w] 141 \\ REWRITE_TAC [METIS_PROVE [] ``b \/ c = ~b ==> c:bool``] 142 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [markerTheory.Abbrev_def,LENGTH, 143 str2num_def,w2n_n2w, AC MULT_ASSOC MULT_COMM,word_arith_lemma2,GSYM NOT_LESS]) 144 \\ `ORD h' < 256` by REWRITE_TAC [ORD_BOUND] 145 \\ `ORD h' < 4294967296 /\ ORD h' - 48 < 4294967296` by DECIDE_TAC 146 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_LO,w2n_n2w,GSYM NOT_LESS,EXPLODE_def,EVERY_DEF,number_char_def] 147 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_arith_lemma2,w2n_n2w,NOT_CONS_NIL,GSYM AND_IMP_INTRO] 148 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `bb ==> cc` (K ALL_TAC)) 149 \\ Q.PAT_X_ASSUM `!k. ?b. bbb` (STRIP_ASSUME_TAC o Q.SPEC `10 * k + (ORD h - 48)`) 150 \\ ASM_SIMP_TAC std_ss [LENGTH,word_add_n2w,GSYM WORD_ADD_ASSOC] 151 \\ SIMP_TAC std_ss [str2num_def,LENGTH,EXP_ADD,EXP] 152 \\ SIMP_TAC std_ss [RIGHT_ADD_DISTRIB] 153 \\ SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC, AC MULT_COMM MULT_ASSOC,ADD1]); 154 155val arm_readnum_lemma = prove( 156 ``!s a df f c1 s1. 157 EVERY number_char (EXPLODE s) /\ ~(s = "") /\ 158 string_mem (STRCAT s (STRING c1 s1)) (a,f,df) /\ 159 ~(number_char c1) ==> 160 arm_readnum_pre (w2w (f a),a,df,f) /\ 161 ?x y. arm_readnum (w2w (f a),a,df,f) = 162 (n2w (str2num s),y,a + n2w (LENGTH s),x,df,f)``, 163 REPEAT STRIP_TAC \\ IMP_RES_TAC arm_read_loop_lemma 164 \\ Q.PAT_X_ASSUM `!k. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`0`]) 165 \\ ASM_SIMP_TAC std_ss [arm_readnum_pre_def,arm_readnum_def,LET_DEF]); 166 167 168(* --- READ NUMBER TOKEN --- *) 169 170val (th1,arm_read_number_def,arm_read_number_pre_def) = compile_all `` 171 arm_read_number (r4,r5,df,f) = 172 let (r3,r4,r5,r6,df,f) = arm_readnum (r4,r5,df,f) in 173 let r3 = r3 << 2 in 174 let r3 = r3 + 0x2w in 175 (r3,r4,r5,r6,df,f)``; 176 177val string_mem_STRCAT = prove( 178 ``!s t a df f. string_mem (STRCAT s t) (a,f,df) = 179 string_mem s (a,f,df) /\ string_mem t (a + n2w (LENGTH s),f,df)``, 180 Induct \\ ASM_SIMP_TAC std_ss [ADD1,LENGTH,WORD_ADD_0,string_mem_def,STRCAT_def] 181 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w,CONJ_ASSOC, 182 AC ADD_ASSOC ADD_COMM]); 183 184val arm_read_number_lemma = prove( 185 ``!s a df f c1 s1. 186 EVERY number_char (EXPLODE s) /\ 187 string_mem (STRCAT s (STRING c1 s1)) (a,f,df) /\ ~(s = "") /\ ~(number_char c1) ==> 188 arm_read_number_pre (w2w (f a),a,df,f) /\ 189 ?x y z. 190 (arm_read_number (w2w (f a),a,df,f) = (ADDR32 (n2w (str2num s)) + 2w,z,x,y,df,f)) /\ 191 string_mem (STRING c1 s1) (x,f,df)``, 192 NTAC 7 STRIP_TAC \\ IMP_RES_TAC arm_readnum_lemma 193 \\ ONCE_REWRITE_TAC [arm_read_number_pre_def,arm_read_number_def] 194 \\ FULL_SIMP_TAC std_ss [LET_DEF,string_mem_STRCAT] 195 \\ FULL_SIMP_TAC std_ss [string_mem_def,ADDR32_n2w,WORD_MUL_LSL,word_mul_n2w]); 196 197 198(* --- READ STRING LENGTH --- *) 199 200val space_char_def = Define ` 201 space_char c = ORD c <= 32`; 202 203val identifier_char_def = Define ` 204 identifier_char c = ~(space_char c) /\ ~(MEM (STRING c "") ["(";")";"."])`; 205 206val (th1,arm_strlen_def,arm_strlen_pre_def) = compile_all `` 207 arm_strlen (r4:word32,r5:word32,df:word32 set,f:word32->word8) = 208 if r4 <+ 0x21w then (r4,r5,df,f) else 209 if r4 = 0x28w then (r4,r5,df,f) else 210 if r4 = 0x29w then (r4,r5,df,f) else 211 if r4 = 0x2Ew then (r4,r5,df,f) else 212 let r5 = r5 + 0x1w in 213 let r4 = w2w (f r5) in 214 arm_strlen (r4,r5,df,f)``; 215 216val (th1,arm_string_length_def,arm_string_length_pre_def) = compile_all `` 217 arm_string_length (r4:word32,r5:word32,df:word32 set,f:word32->word8) = 218 let r7 = r5:word32 in 219 let (r4,r5,df,f) = arm_strlen (r4,r5,df,f) in 220 let r8 = r5 - r7 in 221 (r4,r5,r7,r8,df,f)`` 222 223val identifier_lemma = prove( 224 ``identifier_char c = 225 let w = (w2w ((n2w (ORD c)):word8)):word32 in 226 ~(w <+ 0x21w) /\ ~(w = 0x28w) /\ ~(w = 0x29w) /\ ~(w = 0x2Ew)``, 227 SIMP_TAC std_ss [identifier_char_def,MEM,CONS_11,LET_DEF] 228 \\ SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,ORD_BOUND] 229 \\ Cases_on `c` 230 \\ IMP_RES_TAC ORD_CHR 231 \\ ASM_SIMP_TAC std_ss [CHR_11,space_char_def] 232 \\ `n < 4294967296` by DECIDE_TAC 233 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,WORD_LO,w2n_n2w] 234 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ DECIDE_TAC); 235 236val arm_strlen_lemma = prove( 237 ``!s a. 238 EVERY identifier_char (EXPLODE s) /\ ~(identifier_char c1) /\ 239 string_mem (STRCAT s (STRING c1 s1)) (a,f,df) ==> 240 arm_strlen_pre (w2w (f a),a,df,f) /\ 241 ?x. arm_strlen (w2w (f a),a,df,f) = (x,a + n2w (LENGTH s),df,f)``, 242 Induct \\ SIMP_TAC std_ss [EXPLODE_def,EVERY_DEF,STRCAT_def,string_mem_def] 243 THENL [ 244 ONCE_REWRITE_TAC [arm_strlen_pre_def,arm_strlen_def] 245 \\ SIMP_TAC bool_ss [WORD_EQ_SUB_ZERO,LENGTH,WORD_ADD_0] 246 \\ STRIP_TAC \\ STRIP_TAC 247 \\ FULL_SIMP_TAC std_ss [SIMP_RULE std_ss [LET_DEF] identifier_lemma] 248 \\ SRW_TAC [] [], 249 STRIP_TAC \\ STRIP_TAC \\ STRIP_TAC 250 \\ ONCE_REWRITE_TAC [arm_strlen_def,arm_strlen_pre_def] 251 \\ SIMP_TAC bool_ss [WORD_EQ_SUB_ZERO,LENGTH,WORD_ADD_0,LET_DEF] 252 \\ RES_TAC \\ Q.PAT_X_ASSUM `~identifier_char c1` (K ALL_TAC) 253 \\ FULL_SIMP_TAC std_ss [SIMP_RULE std_ss [LET_DEF] identifier_lemma] 254 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_ASSOC,ADD1] 255 \\ Cases_on `s` \\ FULL_SIMP_TAC std_ss [STRCAT_def,string_mem_def] 256 \\ SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC]]); 257 258val arm_string_length_thm = prove( 259 ``!s a. 260 EVERY identifier_char (EXPLODE s) /\ ~(identifier_char c1) /\ 261 string_mem (STRCAT s (STRING c1 s1)) (a,f,df) ==> 262 arm_string_length_pre (w2w (f a),a,df,f) /\ 263 ?x1 x2. arm_string_length (w2w (f a),a,df,f) = (x1,x2,a,n2w (LENGTH s),df,f)``, 264 SIMP_TAC bool_ss [arm_string_length_pre_def,arm_string_length_def,LET_DEF] 265 \\ REPEAT STRIP_TAC 266 \\ IMP_RES_TAC arm_strlen_lemma 267 \\ ASM_SIMP_TAC std_ss [] 268 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 269 \\ REWRITE_TAC [WORD_ADD_SUB]); 270 271 272(* --- TEST STRING EQUALITY --- *) 273 274val (th1,arm_streq_def,arm_streq_pre_def) = compile_all `` 275 arm_streq (r4:word32,r5:word32,r6:word32,r7:word32,df:word32 set,dg:word32 set,f:word32->word8,g:word32->word8) = 276 if r7 = 0x0w then 277 (let r5 = r7 + r5 in (r4,r5,r6,r7,df,dg,f,g)) 278 else 279 (let r4 = w2w (g r6) in 280 let r6 = r6 + 0x1w in 281 if r4 = w2w (f r5):word32 then 282 (let r7 = r7 - 0x1w in 283 let r5 = r5 + 0x1w in 284 arm_streq (r4,r5,r6,r7,df,dg,f,g)) 285 else 286 (let r5 = r7 + r5 in (r4,r5,r6,r7,df,dg,f,g)))`` 287 288val arm_streq_lemma = prove( 289 ``!s t a b r4. 290 LENGTH s < 2**32 /\ 291 string_mem s (a,f,df) /\ string_mem t (b,g,dg) /\ (LENGTH t = LENGTH s) ==> 292 arm_streq_pre (r4,a,b,n2w (LENGTH s),df,dg,f,g) /\ 293 ?x4 x5 x6 x7. (arm_streq (r4,a,b,n2w (LENGTH s),df,dg,f,g) = 294 (x4,a + n2w (LENGTH s),x6,x7,df,dg,f,g)) /\ 295 ((x7 = 0w) = (s = t))``, 296 Induct 297 THEN1 (ONCE_REWRITE_TAC [arm_streq_pre_def,arm_streq_def] 298 \\ Cases \\ SIMP_TAC std_ss [LENGTH,WORD_ADD_0,LET_DEF,ADD1] 299 \\ ONCE_REWRITE_TAC [arm_streq_def] 300 \\ SIMP_TAC std_ss [LENGTH,WORD_ADD_0,LET_DEF]) 301 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 302 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,DECIDE ``~(1 + n = 0:num)``] 303 \\ SIMP_TAC std_ss [LET_DEF] 304 \\ NTAC 5 STRIP_TAC 305 \\ ONCE_REWRITE_TAC [arm_streq_pre_def,arm_streq_def] 306 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LET_DEF] 307 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [string_mem_def,w2w_def,w2n_n2w,ORD_BOUND] 308 \\ `ORD h' < 256 /\ ORD h < 256` by REWRITE_TAC [ORD_BOUND] 309 \\ `ORD h' < 4294967296 /\ ORD h < 4294967296` by DECIDE_TAC 310 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,ORD_11] 311 THEN1 (`F` by DECIDE_TAC) 312 \\ `~(SUC (LENGTH s) = 0)` by DECIDE_TAC 313 \\ REVERSE (Cases_on `h' = h`) \\ ASM_SIMP_TAC std_ss [CONS_11] THENL [ 314 ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 315 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM], 316 ONCE_REWRITE_TAC [ADD_COMM] 317 \\ REWRITE_TAC [GSYM word_add_n2w,WORD_ADD_SUB] 318 \\ `LENGTH s < 4294967296` by DECIDE_TAC 319 \\ RES_TAC \\ Q.PAT_X_ASSUM `!t a b. bbb` (K ALL_TAC) 320 \\ REPEAT (Q.PAT_X_ASSUM `!r4. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`n2w (ORD h)`])) 321 \\ ASM_SIMP_TAC std_ss [] 322 \\ ASM_SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB] 323 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM]]); 324 325 326(* --- COPY STRING --- *) 327 328val (th1,arm_strcopy_def,arm_strcopy_pre_def) = compile_all `` 329 arm_strcopy (r4:word32,r5:word32,r8:word32,df:word32 set,dg:word32 set,f:word32->word8,g:word32->word8) = 330 (let r6 = (w2w (f r5)):word32 in 331 let r5 = r5 + 0x1w in 332 let g = (r4 =+ w2w r6) g in 333 let r4 = r4 + 0x1w in 334 let r8 = r8 - 0x1w in 335 if r8 = 0w then 336 (r4,r5,r6,r8,df,dg,f,g) 337 else 338 arm_strcopy (r4,r5,r8,df,dg,f,g))`` 339 340val arm_strcopy_lemma = prove( 341 ``!s a b g. 342 w2n b + LENGTH s < 2**32 /\ string_mem s (a,f,df) /\ 343 string_mem_dom s b SUBSET dg /\ ~(s = "") ==> 344 arm_strcopy_pre (b,a,n2w (LENGTH s),df,dg,f,g) /\ 345 ?x3 x4 x5 g'. (arm_strcopy (b,a,n2w (LENGTH s),df,dg,f,g) = 346 (x3,a + n2w (LENGTH s), x4, x5, df,dg,f,g')) /\ 347 string_mem s (b,g',dg) /\ !i. i <+ b ==> (g i = g' i)``, 348 Induct \\ SIMP_TAC std_ss [NOT_CONS_NIL] 349 \\ ONCE_REWRITE_TAC [arm_strcopy_pre_def,arm_strcopy_def] 350 \\ SIMP_TAC std_ss [LET_DEF] 351 \\ NTAC 5 STRIP_TAC 352 \\ FULL_SIMP_TAC std_ss [string_mem_def,string_mem_dom_def,INSERT_SUBSET] 353 \\ Cases_on `s` THENL [ 354 SIMP_TAC std_ss [LENGTH,string_mem_def,APPLY_UPDATE_THM] 355 \\ SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 356 \\ `ORD h < 256` by REWRITE_TAC [ORD_BOUND] 357 \\ `ORD h < 4294967296` by DECIDE_TAC 358 \\ ASM_SIMP_TAC std_ss [GSYM WORD_NOT_LOWER_EQUAL] 359 \\ SIMP_TAC std_ss [WORD_LOWER_OR_EQ,WORD_SUB_REFL,APPLY_UPDATE_THM], 360 ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 361 \\ `LENGTH (STRING h (STRING h' t)) < 4294967296` by 362 (FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC) 363 \\ ASM_SIMP_TAC std_ss [] 364 \\ `~(LENGTH (STRING h (STRING h' t)) = 1)` by 365 (SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC) 366 \\ ASM_SIMP_TAC std_ss [] 367 \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL] 368 \\ `(w2n b + 1) < 4294967296` by 369 (FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC) 370 \\ `w2n (b + 1w) + LENGTH (STRING h' t) < 4294967296` by 371 (ASM_SIMP_TAC (std_ss++SIZES_ss) [word_add_def,w2n_n2w] 372 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC) 373 \\ `ORD h < 256` by REWRITE_TAC [ORD_BOUND] 374 \\ `ORD h < 4294967296` by DECIDE_TAC 375 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 376 \\ ONCE_REWRITE_TAC [LENGTH] 377 \\ ONCE_REWRITE_TAC [ADD_COMM] 378 \\ REWRITE_TAC [ADD1,GSYM word_add_n2w,WORD_ADD_SUB] 379 \\ Q.PAT_X_ASSUM `!a. bbb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o 380 Q.SPECL [`a+1w`,`b+1w`,`(b =+ n2w (ORD h)) g`]) 381 \\ ASM_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 382 \\ `b <+ b + 1w` by ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_LO,word_add_def,w2n_n2w] 383 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM] 384 \\ `~(n2w (STRLEN (STRING h' t)) = 0x0w:word32)` by 385 (FULL_SIMP_TAC (std_ss++SIZES_ss) [LENGTH,ADD1,n2w_11] 386 \\ `STRLEN t + 1 < 4294967296` by DECIDE_TAC 387 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [LENGTH,ADD1,n2w_11]) 388 \\ ASM_SIMP_TAC std_ss [] 389 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC WORD_LOWER_TRANS 390 \\ IMP_RES_TAC WORD_LOWER_NOT_EQ \\ RES_TAC 391 \\ FULL_SIMP_TAC std_ss [LENGTH] 392 \\ REPEAT STRIP_TAC 393 \\ RES_TAC 394 \\ IMP_RES_TAC WORD_LOWER_NOT_EQ \\ RES_TAC 395 \\ FULL_SIMP_TAC std_ss [] 396 \\ METIS_TAC []]); 397 398 399(* --- INSERT SYMBOL NAME --- *) 400 401val (th1,arm_symbol_insert_def,arm_symbol_insert_pre_def) = compile_all `` 402 arm_symbol_insert (r3,r5,r8,df:word32 set,dg:word32 set,dm:word32 set,f,g,m) = 403 (let m = (r3 =+ r8) m in 404 let r7 = r8 + 0x3w in 405 let r7 = r7 >>> 2 in 406 let r7 = r7 << 2 in 407 let r7 = r7 + r3 in 408 let r7 = r7 + 0x8w in 409 let m = (r3 + 0x4w =+ r7) m in 410 let r6 = 0x0w:word32 in 411 let m = (r7 =+ r6) m in 412 let r4 = r3 + 0x8w in 413 let (r4,r5,r6,r8,df,dg,f,g) = arm_strcopy (r4,r5,r8,df,dg,f,g) in 414 (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m))`` 415 416val word_shift_right_n2w = store_thm("word_shift_right_n2w", 417 ``!n k. n < dimword (:'a) ==> (n2w n >>> k = n2w (n DIV 2 ** k) :'a word)``, 418 SIMP_TAC std_ss [GSYM w2n_11,w2n_lsr,w2n_n2w] \\ REPEAT STRIP_TAC 419 \\ `n DIV 2 ** k <= n` by (MATCH_MP_TAC DIV_LESS_EQ \\ SIMP_TAC std_ss [ZERO_LT_EXP]) 420 \\ IMP_RES_TAC LESS_EQ_LESS_TRANS 421 \\ ASM_SIMP_TAC std_ss []); 422 423val symbol_table_dom_ALIGNED = prove( 424 ``!xs a dm dg. symbol_table_dom xs (a,dm,dg) ==> ALIGNED a``, 425 Induct \\ SIMP_TAC std_ss [symbol_table_dom_def] \\ REPEAT STRIP_TAC \\ RES_TAC 426 \\ Q.PAT_X_ASSUM `ALIGNED b` MP_TAC 427 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] \\ SIMP_TAC std_ss [WORD_ADD_0] 428 \\ ONCE_REWRITE_TAC [GSYM (MATCH_MP MOD_PLUS (DECIDE ``0<4:num``))] 429 \\ REWRITE_TAC [EVAL ``8 MOD 4``] 430 \\ SIMP_TAC std_ss [SIMP_RULE std_ss [] (Q.SPECL [`4`,`0`] MOD_MULT),WORD_ADD_0]); 431 432val arm_symbol_insert_lemma = prove( 433 ``string_mem s (k,f,df) /\ symbol_table [] {} (a,dm,m,dg,g) /\ 434 symbol_table_dom [s] (a,dm,dg) ==> 435 arm_symbol_insert_pre (a,k,n2w (LENGTH s),df,dg,dm,f,g,m) /\ 436 ?r4i r5i r6i r7i r8i gi mi. 437 (arm_symbol_insert (a,k,n2w (LENGTH s),df,dg,dm,f,g,m) = 438 (a,r4i,k + n2w (LENGTH s),r6i,r7i,r8i,df,dg,dm,f,gi,mi)) /\ 439 symbol_table [s] {(a,s)} (a,dm,mi,dg,gi) /\ 440 !i. i <+ a ==> (gi i = g i) /\ (mi i = m i)``, 441 STRIP_TAC \\ IMP_RES_TAC symbol_table_dom_ALIGNED 442 \\ FULL_SIMP_TAC std_ss [arm_symbol_insert_pre_def, 443 arm_symbol_insert_def,LET_DEF,symbol_table_dom_def] 444 \\ `(w2n (a + 8w) = w2n a + 8) /\ (w2n (a + 4w) = w2n a + 4)` by 445 (SIMP_TAC (std_ss++SIZES_ss) [word_add_def,w2n_n2w] \\ DECIDE_TAC) 446 \\ `w2n (a + 0x8w) + LENGTH s < 2 ** 32` by 447 (ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC) 448 \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o 449 Q.SPECL [`s`,`k`,`a+8w`,`g`]) arm_strcopy_lemma 450 \\ ASM_SIMP_TAC std_ss [symbol_table_def,LET_DEF,APPLY_UPDATE_THM] 451 \\ `a + (n2w (LENGTH s) + 0x3w) >>> 2 << 2 + 8w = 452 a + n2w (8 + (LENGTH s + 3) DIV 4 * 4)` by 453 (`LENGTH s + 3 < dimword (:32)` by 454 (FULL_SIMP_TAC (std_ss++SIZES_ss) [] \\ DECIDE_TAC) 455 \\ IMP_RES_TAC word_shift_right_n2w 456 \\ ASM_SIMP_TAC std_ss [word_add_n2w,WORD_MUL_LSL,word_mul_n2w,GSYM WORD_ADD_ASSOC] 457 \\ SIMP_TAC bool_ss [AC ADD_ASSOC ADD_COMM, AC MULT_COMM MULT_ASSOC]) 458 \\ `(n2w (LENGTH s) + 0x3w) >>> 2 << 2 + a + 8w = 459 a + n2w (8 + (LENGTH s + 3) DIV 4 * 4)` by 460 (FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] \\ METIS_TAC []) 461 \\ ASM_REWRITE_TAC [SING_DELETE,IN_INSERT] 462 \\ ASM_SIMP_TAC std_ss [RW [WORD_ADD_0] (Q.SPECL [`v`,`w`,`0w`] WORD_EQ_ADD_LCANCEL), 463 WORD_EQ_ADD_LCANCEL] 464 \\ `(STRLEN s + 3) DIV 4 * 4 <= STRLEN s + 3` by 465 (ASSUME_TAC (Q.SPEC `STRLEN s + 3` (SIMP_RULE std_ss [] (Q.SPEC `4` DIVISION))) 466 \\ POP_ASSUM (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [th]))) 467 \\ DECIDE_TAC) 468 \\ `8 + (LENGTH s + 3) DIV 4 * 4 < 4294967296` by DECIDE_TAC 469 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,DECIDE ``~(8 + k = 4:num)``] 470 \\ FULL_SIMP_TAC std_ss [ALIGNED_INTRO,INSERT_SUBSET] 471 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] \\ ASM_SIMP_TAC std_ss [WORD_ADD_0] 472 \\ STRIP_TAC \\ STRIP_TAC 473 \\ ASM_SIMP_TAC std_ss [] 474 \\ `(w2n (a + n2w (8 + (LENGTH s + 3) DIV 4 * 4)) = 475 w2n a + (8 + (LENGTH s + 3) DIV 4 * 4))` by 476 (ASM_SIMP_TAC (std_ss++SIZES_ss) [word_add_def,w2n_n2w] \\ DECIDE_TAC) 477 \\ `a <+ a + 8w /\ a <+ a + 4w /\ a <+ a + n2w (8 + (LENGTH s + 3) DIV 4 * 4)` by 478 (ASM_SIMP_TAC std_ss [WORD_LO] \\ DECIDE_TAC) 479 \\ IMP_RES_TAC WORD_LOWER_TRANS 480 \\ IMP_RES_TAC WORD_LOWER_NOT_EQ 481 \\ RES_TAC \\ ASM_SIMP_TAC std_ss []); 482 483 484 485 486(* --- ADD SYMBOL NAME --- *) 487 488val (th1,arm_symbol_add_def,arm_symbol_add_pre_def) = compile_all `` 489 arm_symbol_add (r3,r5,r8,df,dg,dm,f,g,m) = 490 (let r4 = m r3 in 491 if r4 = 0x0w then 492 (let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) = 493 arm_symbol_insert (r3,r5,r8,df,dg,dm,f,g,m) 494 in 495 (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m)) 496 else 497 if r4 = r8 then 498 (let r7 = r8 in 499 let r6 = r3 + 0x8w in 500 let (r4,r5,r6,r7,df,dg,f,g) = 501 arm_streq (r4,r5,r6,r7,df,dg,f,g) 502 in 503 if r7 = 0x0w then 504 (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) 505 else 506 (let r5 = r5 - r8 in 507 let r3 = m (r3 + 0x4w) in 508 arm_symbol_add (r3,r5,r8,df,dg,dm,f,g,m))) 509 else 510 (let r3 = m (r3 + 0x4w) in 511 arm_symbol_add (r3,r5,r8,df,dg,dm,f,g,m)))``; 512 513val add_symbol_def = Define ` 514 (add_symbol y [] = [y]) /\ 515 (add_symbol y (x::xs) = if y = x then x :: xs else x :: add_symbol y xs)`; 516 517val add_symbol_thm = prove( 518 ``!xs y. add_symbol y xs = if MEM y xs then xs else xs ++ [y]``, 519 Induct \\ SIMP_TAC std_ss [MEM,add_symbol_def,APPEND] \\ METIS_TAC []); 520 521val symbol_table_dom_add_symbol = prove( 522 ``!xs s a. symbol_table_dom (add_symbol s xs) (a,dm,dg) ==> 523 w2n a + 8 + LENGTH s + 3 < 2**32``, 524 Induct \\ REPEAT STRIP_TAC THENL [ALL_TAC, Cases_on `s = h`] 525 \\ FULL_SIMP_TAC std_ss [add_symbol_def,symbol_table_dom_def] 526 \\ `w2n a <= w2n (a + n2w (8 + (LENGTH h + 3) DIV 4 * 4))` suffices_by 527 (STRIP_TAC THEN RES_TAC \\ DECIDE_TAC) 528 \\ `(LENGTH h + 3) DIV 4 * 4 <= LENGTH h + 3` by 529 (ASSUME_TAC (Q.SPEC `STRLEN h + 3` (SIMP_RULE std_ss [] (Q.SPEC `4` DIVISION))) 530 \\ `(LENGTH h + 3) MOD 4 < 4` by SIMP_TAC std_ss [MOD_LESS] \\ DECIDE_TAC) 531 \\ `8 + (LENGTH h + 3) DIV 4 * 4 < 4294967296 /\ 532 w2n a + (8 + (LENGTH h + 3) DIV 4 * 4) < 4294967296` by DECIDE_TAC 533 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_add_def,w2n_n2w]); 534 535val arm_symbol_add_string_mem = prove( 536 ``!s a g gi dg. 537 w2n a + LENGTH s < 4294967296 /\ string_mem s (a,g,dg) /\ 538 (!i. i <+ a + n2w (LENGTH s) ==> (gi i = g i)) ==> 539 string_mem s (a,gi,dg)``, 540 Induct \\ SIMP_TAC std_ss [string_mem_def,LENGTH] 541 \\ REPEAT STRIP_TAC THENL [ 542 `a <+ a + n2w (SUC (STRLEN s))` suffices_by METIS_TAC [] 543 \\ `SUC (LENGTH s) < 4294967296` by DECIDE_TAC 544 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_LO,word_add_def,w2n_n2w] \\ DECIDE_TAC, 545 Q.PAT_X_ASSUM `!x y. bb` MATCH_MP_TAC \\ Q.EXISTS_TAC `g` 546 \\ ASM_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w] 547 \\ `w2n a + 1 < 4294967296` by DECIDE_TAC 548 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_add_def,w2n_n2w,GSYM ADD_ASSOC, 549 DECIDE ``1 + (n:num) = SUC n``]]); 550 551val LESS_EQ_DIV_MULT = prove( 552 ``!n. n <= (n + 3) DIV 4 * 4``, 553 STRIP_TAC \\ STRIP_ASSUME_TAC (Q.SPEC `n + 3` (MATCH_MP (GSYM DIVISION) (DECIDE ``0 < 4:num``))) 554 \\ `(n + 3) DIV 4 * 4 = (n + 3) - (n + 3) MOD 4` by DECIDE_TAC 555 \\ ASM_REWRITE_TAC [] \\ DECIDE_TAC); 556 557val arm_symbol_add_lemma = prove( 558 ``!xs x s a f g. 559 string_mem s (k,f,df) /\ symbol_table xs x (a,dm,m,dg,g) /\ 560 symbol_table_dom (add_symbol s xs) (a,dm,dg) ==> 561 arm_symbol_add_pre (a,k,n2w (LENGTH s),df,dg,dm,f,g,m) /\ 562 ?r3i r4i r6i r7i r8i gi mi. 563 (arm_symbol_add (a,k,n2w (LENGTH s),df,dg,dm,f,g,m) = 564 (r3i,r4i,k + n2w (LENGTH s),r6i,r7i,r8i,df,dg,dm,f,gi,mi)) /\ 565 symbol_table (add_symbol s xs) ((r3i,s) INSERT x) (a,dm,mi,dg,gi) /\ 566 !i. i <+ a ==> (gi i = g i) /\ (mi i = m i)``, 567 Induct THEN1 568 (ONCE_REWRITE_TAC [arm_symbol_add_pre_def,arm_symbol_add_def] 569 \\ SIMP_TAC std_ss [LET_DEF,add_symbol_def,APPEND,MEM] 570 \\ REPEAT STRIP_TAC 571 \\ `x = {}` by FULL_SIMP_TAC std_ss [symbol_table_def] 572 \\ FULL_SIMP_TAC std_ss [] 573 \\ IMP_RES_TAC arm_symbol_insert_lemma 574 \\ IMP_RES_TAC symbol_table_dom_ALIGNED 575 \\ ASM_SIMP_TAC std_ss [] 576 \\ FULL_SIMP_TAC std_ss [symbol_table_def,ALIGNED_INTRO]) 577 \\ ONCE_REWRITE_TAC [arm_symbol_add_pre_def,arm_symbol_add_def] \\ REWRITE_TAC [add_symbol_def] 578 \\ NTAC 7 STRIP_TAC \\ Cases_on `s = h` 579 \\ FULL_SIMP_TAC std_ss [symbol_table_def,symbol_table_dom_def,LET_DEF] 580 \\ `LENGTH h < 4294967296` by DECIDE_TAC 581 \\ `~(LENGTH h = 0)` by 582 (Cases_on `h` \\ FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC) 583 \\ `ALIGNED a` by 584 (IMP_RES_TAC symbol_table_dom_ALIGNED 585 \\ Q.PAT_X_ASSUM `ALIGNED xxx` MP_TAC 586 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] \\ ASM_SIMP_TAC std_ss [WORD_ADD_0] 587 \\ ONCE_REWRITE_TAC [MATCH_MP(GSYM MOD_PLUS) (DECIDE ``0<4:num``)] 588 \\ REWRITE_TAC [ADD,EVAL ``8 MOD 4``] 589 \\ SIMP_TAC std_ss [MOD_EQ_0,WORD_ADD_0]) 590 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 591 THEN1 592 (STRIP_ASSUME_TAC (UNDISCH_ALL (SIMP_RULE std_ss [GSYM AND_IMP_INTRO] 593 (Q.SPECL [`h`,`h`,`k`,`a + 8w`,`n2w (STRLEN h)`] arm_streq_lemma))) 594 \\ `((a,h) INSERT x) DELETE (a,h) = x DELETE (a,h)` by (SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE] \\ METIS_TAC []) 595 \\ FULL_SIMP_TAC std_ss [ALIGNED_INTRO,INSERT_SUBSET,IN_INSERT]) 596 \\ REVERSE (Cases_on `STRLEN h = STRLEN s`) 597 \\ IMP_RES_TAC symbol_table_dom_add_symbol 598 \\ FULL_SIMP_TAC std_ss [] 599 \\ `STRLEN s < 4294967296` by DECIDE_TAC 600 \\ `w2n (a + 8w) = w2n a + 8` by 601 (SIMP_TAC (std_ss++SIZES_ss) [word_add_def,w2n_n2w] \\ DECIDE_TAC) 602 \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,ALIGNED_INTRO,ALIGNED_CLAUSES] 603 \\ `(STRLEN h + 3) DIV 4 * 4 <= STRLEN h + 3` by 604 (ASSUME_TAC (Q.SPEC `STRLEN h + 3` (SIMP_RULE std_ss [] (Q.SPEC `4` DIVISION))) 605 \\ `(STRLEN h + 3) MOD 4 < 4` by SIMP_TAC std_ss [MOD_LESS] \\ DECIDE_TAC) 606 \\ `(STRLEN s + 3) DIV 4 * 4 <= STRLEN s + 3` by 607 (ASSUME_TAC (Q.SPEC `STRLEN s + 3` (SIMP_RULE std_ss [] (Q.SPEC `4` DIVISION))) 608 \\ `(STRLEN s + 3) MOD 4 < 4` by SIMP_TAC std_ss [MOD_LESS] \\ DECIDE_TAC) 609 THEN1 610 (Q.ABBREV_TAC `a2 = a + n2w (8 + (LENGTH h + 3) DIV 4 * 4)` 611 \\ `w2n a + 4 < 4294967296 /\ 612 (w2n a + (8 + (STRLEN h + 3) DIV 4 * 4)) < 4294967296 /\ 613 8 + (STRLEN h + 3) DIV 4 * 4 < 4294967296` by 614 (ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC) 615 \\ `a <+ a2 /\ a + 4w <+ a2` by 616 (Q.UNABBREV_TAC `a2` \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_LO,word_add_def,w2n_n2w] \\ DECIDE_TAC) 617 \\ Q.PAT_X_ASSUM `!s a f g. bb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o 618 Q.SPECL [`x DELETE (a,h)`,`s`,`a2`,`f`,`g`]) 619 \\ `(((r3i,s) INSERT x) DELETE (a,h)) = (r3i,s) INSERT (x DELETE (a,h))` by (ASM_SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE] \\ METIS_TAC [PAIR_EQ,PAIR]) 620 \\ ASM_SIMP_TAC std_ss [WORD_LOWER_TRANS,IN_INSERT] 621 \\ REVERSE STRIP_TAC THEN1 METIS_TAC [WORD_LOWER_TRANS] 622 \\ MATCH_MP_TAC arm_symbol_add_string_mem \\ Q.EXISTS_TAC `g` 623 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC THEN1 DECIDE_TAC 624 \\ REWRITE_TAC [GSYM WORD_ADD_ASSOC,word_add_n2w] 625 \\ REPEAT STRIP_TAC 626 \\ `a + n2w (8 + STRLEN h) <=+ a2` suffices_by METIS_TAC [WORD_LOWER_LOWER_EQ_TRANS] 627 \\ Q.UNABBREV_TAC `a2` 628 \\ `8 + STRLEN h < 4294967296 /\ 629 w2n a + (8 + STRLEN h) < 4294967296` by DECIDE_TAC 630 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_LS,word_add_def,w2n_n2w,LESS_EQ_DIV_MULT]) 631 THEN1 632 (STRIP_ASSUME_TAC (UNDISCH_ALL (REWRITE_RULE [GSYM AND_IMP_INTRO, EVAL ``(2:num)**32``] 633 (Q.SPECL [`s`,`h`,`k`,`a + 8w`,`n2w (STRLEN s)`] arm_streq_lemma))) 634 \\ ASM_SIMP_TAC std_ss [WORD_ADD_SUB] 635 \\ Q.ABBREV_TAC `a2 = a + n2w (8 + (STRLEN s + 3) DIV 4 * 4)` 636 \\ Q.PAT_X_ASSUM `!s a f g. bb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o 637 Q.SPECL [`x DELETE (a,h)`,`s`,`a2`,`f`,`g`]) 638 \\ ASM_SIMP_TAC std_ss [] 639 \\ `w2n a + 4 < 4294967296 /\ 640 (w2n a + (8 + (STRLEN s + 3) DIV 4 * 4)) < 4294967296 /\ 641 8 + (STRLEN s + 3) DIV 4 * 4 < 4294967296` by DECIDE_TAC 642 \\ `a <+ a2 /\ a + 4w <+ a2` by 643 (Q.UNABBREV_TAC `a2` \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_LO,word_add_def,w2n_n2w] \\ DECIDE_TAC) 644 \\ `(((r3i,s) INSERT x) DELETE (a,h)) = (r3i,s) INSERT (x DELETE (a,h))` by (ASM_SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE] \\ METIS_TAC [PAIR_EQ,PAIR]) 645 \\ ASM_SIMP_TAC std_ss [WORD_LOWER_TRANS,IN_INSERT] 646 \\ REVERSE STRIP_TAC THEN1 METIS_TAC [WORD_LOWER_TRANS] 647 \\ MATCH_MP_TAC arm_symbol_add_string_mem \\ Q.EXISTS_TAC `g` 648 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC THEN1 DECIDE_TAC 649 \\ REWRITE_TAC [GSYM WORD_ADD_ASSOC,word_add_n2w] 650 \\ REPEAT STRIP_TAC 651 \\ `a + n2w (8 + STRLEN s) <=+ a2` suffices_by METIS_TAC [WORD_LOWER_LOWER_EQ_TRANS] 652 \\ Q.UNABBREV_TAC `a2` 653 \\ `8 + STRLEN s < 4294967296 /\ 654 w2n a + (8 + STRLEN s) < 4294967296` by DECIDE_TAC 655 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_LS,word_add_def,w2n_n2w,LESS_EQ_DIV_MULT])); 656 657 658(* --- UPDATE SYMBOL TABLE --- *) 659 660val (th1,arm_symbol_def,arm_symbol_pre_def) = compile_all `` 661 arm_symbol (r3,r4,r5,df,dg,dm,f,g,m) = 662 (let r7 = r5 in 663 let (r4,r5,df,f) = arm_strlen (r4,r5,df,f) in 664 let r8 = r5 - r7 in 665 let r5 = r5 - r8 in 666 let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) = 667 arm_symbol_add (r3,r5,r8,df,dg,dm,f,g,m) 668 in 669 let r3 = r3 + 0x3w in 670 (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m))``; 671 672val arm_symbol_lemma = prove( 673 ``!xs s a f g. 674 EVERY identifier_char (EXPLODE s) /\ ~identifier_char c1 /\ 675 string_mem (STRCAT s (STRING c1 s1)) (k,f,df) /\ 676 symbol_table xs x (a,dm,m,dg,g) /\ 677 symbol_table_dom (add_symbol s xs) (a,dm,dg) ==> 678 arm_symbol_pre (a,w2w (f k),k,df,dg,dm,f,g,m) /\ 679 ?r3i r4i r5i r6i r7i r8i gi mi. 680 (arm_symbol (a,w2w (f k),k,df,dg,dm,f,g,m) = 681 (r3i,r4i,r5i,r6i,r7i,r8i,df,dg,dm,f,gi,mi)) /\ 682 symbol_table (add_symbol s xs) ((r3i - 3w,s) INSERT x) (a,dm,mi,dg,gi) /\ 683 string_mem (STRING c1 s1) (r5i,f,df)``, 684 REPEAT STRIP_TAC \\ SIMP_TAC std_ss[arm_symbol_def,arm_symbol_pre_def,LET_DEF] 685 \\ SIMP_TAC std_ss [GSYM WORD_NEG_MUL,GSYM (RW1 [WORD_ADD_COMM] word_sub_def)] 686 \\ IMP_RES_TAC arm_strlen_lemma 687 \\ ASM_SIMP_TAC std_ss [] 688 \\ REWRITE_TAC [WORD_SUB_SUB2] 689 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 690 \\ REWRITE_TAC [WORD_ADD_SUB] 691 \\ FULL_SIMP_TAC std_ss [string_mem_STRCAT] 692 \\ IMP_RES_TAC arm_symbol_add_lemma 693 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 694 \\ ASM_SIMP_TAC std_ss [WORD_SUB_ADD,WORD_ADD_SUB]); 695 696 697(* --- LEX SYMBOL AND NUMBER --- *) 698 699val (th1,arm_number_symbol_def,arm_number_symbol_pre_def) = compile_all `` 700 arm_number_symbol (r9,r3,r4,r5,r7,r8,df,dg,dh:word32 set,dm,f,g,h:word32->word32,m) = 701 if ~(r4 <+ 0x30w) then 702 if ~(r4 <+ 0x3Aw) then 703 (let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) = 704 arm_symbol (r3,r4,r5,df,dg,dm,f,g,m) 705 in 706 let r4 = h (r9 + 4w) in 707 let r3 = r3 - r4 in 708 let r4 = (w2w (f r5)):word32 in 709 let h = (r9 =+ r3) h in 710 let r9 = r9 + 0x8w in 711 (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m)) 712 else 713 (let (r3,r4,r5,r6,df,f) = arm_read_number (r4,r5,df,f) in 714 let r4 = w2w (f r5) in 715 let h = (r9 =+ r3) h in 716 let r9 = r9 + 0x8w in 717 (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m)) 718 else 719 (let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) = 720 arm_symbol (r3,r4,r5,df,dg,dm,f,g,m) 721 in 722 let r4 = h (r9 + 4w) in 723 let r3 = r3 - r4 in 724 let r4 = w2w (f r5) in 725 let h = (r9 =+ r3) h in 726 let r9 = r9 + 0x8w in 727 (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))``; 728 729 730(* --- LEXER AUX --- *) 731 732val (th1,arm_lexer_aux_def,arm_lexer_aux_pre_def) = compile_all `` 733 arm_lexer_aux (r4:word32,r6:word32) = 734 if r4 = 0x27w then let r6 = 0x10w in (r4,r6) else 735 if r4 = 0x2Ew then let r6 = 0xCw in (r4,r6) else 736 if r4 = 0x29w then let r6 = 0x8w in (r4,r6) else 737 if r4 = 0x28w then let r6 = 0x4w in (r4,r6) else 738 (r4,r6)``; 739 740 741(* --- LEXER --- *) 742 743val (th1,arm_lexer_def,arm_lexer_pre_def) = compile_all `` 744 arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) = 745 if r4 = 0x0w then 746 (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) 747 else 748 if ~(r4 <+ 0x21w) then 749 (let r6 = 0x0w in 750 let (r4,r6) = arm_lexer_aux (r4,r6) in 751 if r6 = 0x0w then 752 (let h = (r9 + 4w =+ r3) h in 753 let (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) = 754 arm_number_symbol 755 (r9,r3,r4,r5,r7,r8,df,dg,dh,dm,f,g,h,m) 756 in 757 let r3 = h (r9 - 4w) in 758 arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m)) 759 else 760 (let h = (r9 =+ r6) h in 761 let r9 = r9 + 0x8w in 762 let r5 = r5 + 0x1w in 763 let r4 = w2w (f r5) in 764 arm_lexer 765 (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))) 766 else 767 (let r5 = r5 + 0x1w in 768 let r4 = w2w (f r5) in 769 arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))``; 770 771val read_while_def = Define ` 772 (read_while P "" s = (s,"")) /\ 773 (read_while P (STRING c cs) s = 774 if P c then read_while P cs (STRCAT s (STRING c "")) 775 else (s,STRING c cs))`; 776 777val read_while_thm = prove( 778 ``!cs s cs' s'. 779 (read_while P cs s = (s',cs')) ==> LENGTH cs' <= LENGTH cs + LENGTH s``, 780 Induct \\ SIMP_TAC std_ss [read_while_def] 781 \\ REPEAT STRIP_TAC 782 \\ Cases_on `P h` \\ FULL_SIMP_TAC std_ss [LENGTH] 783 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_STRCAT] 784 \\ REPEAT (Q.PAT_X_ASSUM `STRING c cs = cs'` (ASSUME_TAC o GSYM)) 785 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_STRCAT] \\ DECIDE_TAC); 786 787val sexp_lex_def = tDefine "sexp_lex" ` 788 (sexp_lex "" = []) /\ 789 (sexp_lex (STRING c cs) = 790 if space_char c then sexp_lex cs else 791 if MEM c [#"(";#")";#".";#"'"] then (STRING c "") :: sexp_lex cs else 792 if number_char c then 793 (let (x,cs) = read_while number_char cs "" in (STRING c x) :: sexp_lex cs) else 794 (let (x,cs) = read_while identifier_char cs "" in (STRING c x) :: sexp_lex cs))` 795 (WF_REL_TAC `measure (LENGTH)` \\ REPEAT STRIP_TAC 796 \\ IMP_RES_TAC (GSYM read_while_thm) 797 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ DECIDE_TAC) 798 799val null_string_def = Define `null_string = STRING (CHR 0) ""`; 800 801val identifier_string_def = Define ` 802 identifier_string s = 803 EVERY identifier_char (EXPLODE s) /\ ~(number_char (HD (EXPLODE s))) /\ 804 ~(HD (EXPLODE s) = #"'")`; 805 806val all_symbols_def = Define ` 807 (all_symbols [] xs = xs) /\ 808 (all_symbols (c::cs) xs = 809 if identifier_string c 810 then all_symbols cs (add_symbol c xs) else all_symbols cs xs)`; 811 812val read_while_thm2_lemma = prove( 813 ``!cs s P. ?t1 t2. (read_while P cs s = (t1,t2)) /\ (STRCAT s cs = STRCAT t1 t2) /\ 814 (EVERY P (EXPLODE s) ==> EVERY P (EXPLODE t1)) /\ 815 (~(t2 = "") ==> ~ P (HD (EXPLODE t2)))``, 816 Induct \\ SIMP_TAC std_ss [read_while_def,EXPLODE_def,EVERY_DEF] 817 \\ REPEAT STRIP_TAC \\ Cases_on `P h` \\ ASM_SIMP_TAC std_ss [EXPLODE_def,HD] 818 \\ Q.PAT_X_ASSUM `!s. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`STRCAT s (STRING h "")`,`P`]) 819 \\ FULL_SIMP_TAC std_ss [EXPLODE_STRCAT,EVERY_APPEND,EXPLODE_def,EVERY_DEF] 820 \\ FULL_SIMP_TAC std_ss [GSYM STRCAT_ASSOC,STRCAT_def]); 821 822val read_while_thm2 = 823 GEN_ALL (RW [STRCAT_def,EXPLODE_def,EVERY_DEF] (Q.SPECL [`cs`,`""`] read_while_thm2_lemma)); 824 825val symbol_table_dom_IMPLIES = prove( 826 ``!xs ys a dm dg. 827 symbol_table_dom (all_symbols xs ys) (a,dm,dg) ==> 828 symbol_table_dom ys (a,dm,dg)``, 829 Induct \\ REWRITE_TAC [all_symbols_def] \\ NTAC 5 STRIP_TAC 830 \\ Cases_on `identifier_string h` \\ ASM_SIMP_TAC std_ss [] 831 \\ STRIP_TAC \\ RES_TAC \\ POP_ASSUM MP_TAC 832 \\ REWRITE_TAC [add_symbol_thm] 833 \\ Cases_on `MEM h ys` THEN1 METIS_TAC [] 834 \\ ASM_REWRITE_TAC [] 835 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 836 \\ Q.SPEC_TAC (`a`,`a`) 837 \\ Induct_on `ys` THENL [ 838 SIMP_TAC std_ss [symbol_table_dom_def,INSERT_SUBSET] 839 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC symbol_table_dom_ALIGNED 840 \\ FULL_SIMP_TAC std_ss [symbol_table_dom_def,INSERT_SUBSET,APPEND], 841 REWRITE_TAC [APPEND] 842 \\ ONCE_REWRITE_TAC [symbol_table_dom_def] 843 \\ REPEAT STRIP_TAC \\ RES_TAC 844 \\ ASM_SIMP_TAC std_ss []]); 845 846open set_sepTheory; 847 848val arm_token_def = Define ` 849 arm_token w str b x = 850 if str = "(" then (w = 4w) else 851 if str = ")" then (w = 8w) else 852 if str = "." then (w = 12w) else 853 if str = "'" then (w = 16w) else 854 if EVERY number_char (EXPLODE str) 855 then (w = ADDR32 (n2w (str2num str)) + 2w) 856 else (b + w - 3w, str) IN x /\ ALIGNED (w - 3w)`; 857 858val arm_tokens_def = Define ` 859 (arm_tokens a [] b x y = cond (a = y)) /\ 860 (arm_tokens a (str::xs) b x y = 861 SEP_EXISTS w1:word32 w2:word32. one (a,w1) * one (a+4w,w2) * 862 cond (arm_token w1 str b x) * 863 arm_tokens (a + 8w:word32) xs b x y)`; 864 865val token_slots_def = Define ` 866 (token_slots a 0 = emp) /\ 867 (token_slots a (SUC n) = 868 SEP_EXISTS w1:word32 w2:word32. one (a,w1) * one (a+4w,w2) * 869 token_slots (a + 8w:word32) n)`; 870 871val symbol_table_IMP_ALIGNED = prove( 872 ``!xs x r3 a y. (a,y) IN x /\ ALIGNED r3 /\ 873 symbol_table xs x (r3,dm,mi,dg,gi) ==> 874 ALIGNED a``, 875 Induct 876 \\ REWRITE_TAC [symbol_table_def] THEN1 METIS_TAC [NOT_IN_EMPTY] 877 \\ SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 878 \\ Cases_on `(a,y) = (r3,h)` THEN1 METIS_TAC [PAIR_EQ] 879 \\ `(a,y) IN (x DELETE (r3,h))` by ASM_SIMP_TAC std_ss [IN_DELETE] 880 \\ `ALIGNED (r3 + n2w (8 + (STRLEN h + 3) DIV 4 * 4))` suffices_by METIS_TAC [] 881 \\ REWRITE_TAC [GSYM word_add_n2w] 882 \\ MATCH_MP_TAC ALIGNED_ADD \\ ASM_SIMP_TAC std_ss [] 883 \\ MATCH_MP_TAC ALIGNED_ADD \\ ASM_SIMP_TAC std_ss [ALIGNED_n2w] 884 \\ SIMP_TAC std_ss [MOD_EQ_0]); 885 886val string_mem_IMP_IN = prove( 887 ``!t x f df. string_mem (STRCAT t null_string) (x,f,df) ==> x IN df``, 888 Cases \\ FULL_SIMP_TAC std_ss [APPEND,null_string_def,string_mem_def]); 889 890val arm_lexer_lemma = prove( 891 ``!s r1 r3 k r6 r7 r8 p x xs df dg dh dm f g h m. 892 string_mem (STRCAT s null_string) (k,f,df) /\ 893 (EVERY (\c. ~(ORD c = 0)) (EXPLODE s)) /\ 894 symbol_table xs x (r3,dm,m,dg,g) /\ ALIGNED r1 /\ 895 (p * token_slots r1 (LENGTH (sexp_lex s))) (fun2set (h,dh)) /\ 896 symbol_table_dom (all_symbols (sexp_lex s) xs) (r3,dm,dg) ==> 897 ?r1i r4i r5i r6i r7i r8i gi hi mi xi. 898 arm_lexer_pre (r1,r3,w2w (f k),k,r6,r7,r8,df,dg,dh,dm,f,g,h,m) /\ 899 (arm_lexer (r1,r3,w2w (f k),k,r6,r7,r8,df,dg,dh,dm,f,g,h,m) = 900 (r1i,r3,r4i,r5i,r6i,r7i,r8i,df,dg,dh,dm,f,gi,hi,mi)) /\ 901 (p * arm_tokens r1 (sexp_lex s) r3 xi r1i) (fun2set (hi,dh)) /\ 902 (r1 + n2w (8 * LENGTH (sexp_lex s)) = r1i) /\ 903 symbol_table (all_symbols (sexp_lex s) xs) xi (r3,dm,mi,dg,gi) /\ 904 x SUBSET xi``, 905 completeInduct_on `STRLEN s` \\ Cases THEN1 906 (SIMP_TAC std_ss [STRCAT_def,null_string_def,string_mem_def] 907 \\ ONCE_REWRITE_TAC [arm_lexer_def,arm_lexer_pre_def] 908 \\ SIMP_TAC std_ss [sexp_lex_def,all_symbols_def,arm_tokens_def,LENGTH,WORD_ADD_0] 909 \\ SIMP_TAC std_ss [EVAL ``(w2w (n2w (ORD #"\^@") :word8)):word32``] 910 \\ SIMP_TAC std_ss [token_slots_def,SEP_CLAUSES] 911 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `x` \\ ASM_REWRITE_TAC [SUBSET_REFL]) 912 \\ SIMP_TAC std_ss [EVERY_DEF,EXPLODE_def,STRCAT_def,string_mem_def] 913 \\ SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,ORD_BOUND] 914 \\ ONCE_REWRITE_TAC [arm_lexer_def,arm_lexer_pre_def] 915 \\ REPEAT STRIP_TAC 916 \\ `ORD h < 256` by REWRITE_TAC [ORD_BOUND] 917 \\ `ORD h < 4294967296` by DECIDE_TAC 918 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 919 \\ `k + 0x1w IN df` by (IMP_RES_TAC string_mem_IMP_IN) 920 \\ Cases_on `space_char h` THEN1 921 (FULL_SIMP_TAC std_ss [sexp_lex_def] 922 \\ FULL_SIMP_TAC std_ss [space_char_def] 923 \\ `ORD h < 33` by DECIDE_TAC 924 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,WORD_LO,w2n_n2w] 925 \\ Q.PAT_X_ASSUM `!xyz. myz` (ASSUME_TAC o Q.SPEC `STRLEN t`) 926 \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``m < m + 1:num``] 927 \\ Q.PAT_X_ASSUM `!xys. msd` (ASSUME_TAC o RW [] o Q.SPEC `t`) 928 \\ RES_TAC \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`r8`,`r7`,`r6`]) 929 \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `xi` 930 \\ ASM_SIMP_TAC std_ss []) 931 \\ `~(n2w (ORD h) <+ 0x21w:word32)` by 932 (FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_LO,w2n_n2w,space_char_def] \\ DECIDE_TAC) 933 \\ ASM_SIMP_TAC std_ss [] 934 \\ Cases_on `MEM (ORD h) [40;41;39;46]` THEN1 935 (`?x2 y2. (arm_lexer_aux (n2w (ORD h),0w) = (x2,y2)) /\ ~(y2 = 0w)` by FULL_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,MEM,arm_lexer_aux_def,n2w_11] 936 \\ FULL_SIMP_TAC std_ss [LET_DEF] 937 \\ Q.PAT_X_ASSUM `!x. mq` (ASSUME_TAC o Q.SPEC `STRLEN t`) 938 \\ FULL_SIMP_TAC std_ss [LENGTH,DECIDE ``m < m + 1:num``] 939 \\ Q.PAT_X_ASSUM `!x. mq` (ASSUME_TAC o RW [] o Q.SPEC `t`) 940 \\ `sexp_lex (STRING h t) = STRING h ""::sexp_lex t` by 941 FULL_SIMP_TAC std_ss [sexp_lex_def,MEM,GSYM ORD_11, 942 EVAL ``ORD #"("``,EVAL ``ORD #")"``,EVAL ``ORD #"."``,EVAL ``ORD #"'"``] 943 \\ FULL_SIMP_TAC std_ss [] 944 \\ `~identifier_string (STRING h "")` by 945 FULL_SIMP_TAC std_ss [all_symbols_def,EXPLODE_def,EVERY_DEF, 946 identifier_char_def,MEM,CONS_11,GSYM ORD_11,identifier_string_def,HD, 947 EVAL ``ORD #"("``,EVAL ``ORD #")"``,EVAL ``ORD #"."``,EVAL ``ORD #"'"``] 948 \\ FULL_SIMP_TAC std_ss [all_symbols_def,arm_tokens_def,LENGTH,RW1[MULT_COMM]MULT] 949 \\ FULL_SIMP_TAC std_ss [token_slots_def,SEP_CLAUSES] 950 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 951 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] 952 \\ `(p * one (r1,y2) * one (r1 + 0x4w,y') * 953 token_slots (r1 + 0x8w) (LENGTH (sexp_lex t))) 954 (fun2set ((r1 =+ y2) h',dh))` by SEP_WRITE_TAC 955 \\ `ALIGNED (r1+8w)` by ALIGNED_TAC 956 \\ Q.PAT_X_ASSUM `!r1 r2. bbb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o Q.SPECL 957 [`r1+8w`,`r3`,`k+1w`,`y2`,`r7`,`r8`,`p * one (r1,y2) * one (r1 + 0x4w,y')`,`x`,`xs`,`df`,`dg`,`dh`,`dm`,`f`,`g`,`(r1 =+ y2) h'`,`m`]) 958 \\ ASM_SIMP_TAC std_ss [] 959 \\ Q.EXISTS_TAC `xi` \\ ASM_SIMP_TAC std_ss [SUBSET_REFL] 960 \\ `(h' r1 = y) /\ r1 IN dh` by SEP_READ_TAC 961 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO] 962 \\ STRIP_TAC THEN1 963 (REWRITE_TAC [GSYM word_add_n2w] 964 \\ SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC]) 965 \\ Q.ABBREV_TAC `i = r1 + n2w (8 * LENGTH (sexp_lex t) + 8)` 966 \\ Q.EXISTS_TAC `y2` \\ Q.EXISTS_TAC `y'` 967 \\ SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 968 \\ STRIP_TAC THEN1 969 (Q.PAT_X_ASSUM `arm_lexer_aux (n2w (ORD h),0x0w) = (x2,y2)` (ASSUME_TAC o GSYM) 970 \\ Q.PAT_X_ASSUM `MEM (ORD h) [40; 41; 39; 46]` 971 (STRIP_ASSUME_TAC o RW [MEM]) 972 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [arm_lexer_aux_def,LET_DEF,n2w_11,arm_token_def,CONS_11] 973 \\ ASM_REWRITE_TAC [GSYM ORD_11] \\ EVAL_TAC) 974 \\ `r1 + 0x8w + n2w (8 * LENGTH (sexp_lex t)) = i` by 975 (Q.UNABBREV_TAC `i` 976 \\ SIMP_TAC std_ss [GSYM word_add_n2w, 977 AC WORD_ADD_ASSOC WORD_ADD_COMM]) 978 \\ FULL_SIMP_TAC std_ss []) 979 \\ `arm_lexer_aux (n2w (ORD h),0w) = (n2w (ORD h),0w)` by FULL_SIMP_TAC (std_ss++SIZES_ss) [arm_lexer_aux_def,MEM,n2w_11,LET_DEF] 980 \\ ASM_SIMP_TAC std_ss [LET_DEF,arm_number_symbol_def,arm_number_symbol_pre_def] 981 \\ Cases_on `number_char h` THEN1 982 (FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_LO,w2n_n2w,number_char_def, 983 DECIDE ``48 <= n = ~(n < 48:num)``] 984 \\ STRIP_ASSUME_TAC (Q.SPECL [`t`,`number_char`] read_while_thm2) 985 \\ `sexp_lex (STRING h t) = STRING h t1 :: sexp_lex t2` by 986 (ONCE_REWRITE_TAC [sexp_lex_def] 987 \\ ASM_SIMP_TAC std_ss [space_char_def,MEM,GSYM ORD_11, 988 EVAL ``ORD #"("``,EVAL ``ORD #")"``,EVAL ``ORD #"."``,EVAL ``ORD #"'"``] 989 \\ FULL_SIMP_TAC std_ss [number_char_def,MEM,DECIDE ``48 <= m = ~(m < 48:num)``,LET_DEF]) 990 \\ FULL_SIMP_TAC std_ss [GSYM STRCAT_ASSOC] 991 \\ `EVERY number_char (EXPLODE (STRING h t1))` by 992 (ASM_SIMP_TAC std_ss [number_char_def,EXPLODE_def,EVERY_DEF] \\ DECIDE_TAC) 993 \\ `?c2 t3. (STRCAT t2 null_string = STRING c2 t3) /\ ~(number_char c2)` by 994 (Cases_on `t2` \\ SIMP_TAC std_ss [STRCAT_def,null_string_def,CONS_11] 995 THEN1 EVAL_TAC \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL,EXPLODE_def,HD]) 996 \\ FULL_SIMP_TAC std_ss [] 997 \\ `string_mem (STRCAT (STRING h t1) (STRING c2 t3)) (k,f,df)` by 998 ASM_SIMP_TAC std_ss [STRCAT_def,string_mem_def] 999 \\ STRIP_ASSUME_TAC ((UNDISCH_ALL o SIMP_RULE std_ss [GSYM NOT_CONS_NIL,GSYM AND_IMP_INTRO]) 1000 (Q.SPECL [`STRING h t1`,`k`,`df`,`f`,`c2`,`t3`] arm_read_number_lemma)) 1001 \\ `w2w (f k) = n2w (ORD h):word32` by 1002 ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,ORD_BOUND] 1003 \\ FULL_SIMP_TAC std_ss [] 1004 \\ Q.PAT_X_ASSUM `STRCAT t2 null_string = STRING c2 t3` (ASSUME_TAC o GSYM) 1005 \\ FULL_SIMP_TAC std_ss [] 1006 \\ `LENGTH t2 < LENGTH (STRING h (STRCAT t1 t2))` by 1007 (SIMP_TAC std_ss [LENGTH,LENGTH_STRCAT] \\ DECIDE_TAC) 1008 \\ Q.PAT_X_ASSUM `!m. bb ==> ccc` (ASSUME_TAC o 1009 RW [] o Q.SPEC `t2` o UNDISCH o Q.SPEC `STRLEN t2`) 1010 \\ FULL_SIMP_TAC std_ss [LENGTH,token_slots_def,SEP_CLAUSES] 1011 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,STAR_ASSOC] 1012 \\ Q.ABBREV_TAC [ANTIQUOTE ``n = ADDR32 (n2w (str2num (STRING h t1))) + 2w``] 1013 \\ FULL_SIMP_TAC std_ss [EXPLODE_STRCAT,EVERY_APPEND,LENGTH,RW1[MULT_COMM]MULT] 1014 \\ `~identifier_string (STRING h t1)` by 1015 (FULL_SIMP_TAC std_ss [identifier_string_def,EXPLODE_def,HD,number_char_def] 1016 \\ ASM_SIMP_TAC std_ss [DECIDE ``48 <= m = ~(m < 48:num)``]) 1017 \\ FULL_SIMP_TAC std_ss [all_symbols_def] 1018 \\ SIMP_TAC std_ss [APPLY_UPDATE_THM,word_arith_lemma4] 1019 \\ SIMP_TAC (std_ss++SIZES_ss) [WORD_EQ_ADD_CANCEL,n2w_11] 1020 \\ `(p * one (r1,n) * one (r1 + 0x4w,r3) * 1021 token_slots (r1 + 0x8w) (LENGTH (sexp_lex t2))) 1022 (fun2set ((r1 =+ n) ((r1 + 0x4w =+ r3) h'),dh))` by SEP_WRITE_TAC 1023 \\ `ALIGNED (r1+8w)` by ALIGNED_TAC 1024 \\ Q.PAT_X_ASSUM `!r1 r2. bbb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o Q.SPECL 1025 [`r1+8w`,`r3`,`x'`,`y`,`r7`,`r8`,`p * one (r1,n) * one (r1 + 0x4w,r3)`,`x`,`xs`,`df`,`dg`,`dh`,`dm`,`f`,`g`,`(r1 =+ n) ((r1 + 4w =+ r3) h')`,`m`]) 1026 \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `xi` \\ ASM_SIMP_TAC std_ss [SUBSET_REFL] 1027 \\ `(h' r1 = y') /\ r1 IN dh` by SEP_READ_TAC 1028 \\ `(h' (r1 + 4w) = y'') /\ r1 + 4w IN dh` by SEP_READ_TAC 1029 \\ IMP_RES_TAC string_mem_IMP_IN 1030 \\ `ALIGNED (r1 + 0x4w)` by ALIGNED_TAC 1031 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO] 1032 \\ STRIP_TAC THEN1 1033 (REWRITE_TAC [GSYM word_add_n2w] 1034 \\ SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC]) 1035 \\ Q.ABBREV_TAC `i = r1 + n2w (8 * LENGTH (sexp_lex t) + 8)` 1036 \\ REWRITE_TAC [arm_tokens_def] 1037 \\ SIMP_TAC std_ss [SEP_CLAUSES] 1038 \\ SIMP_TAC std_ss [SEP_EXISTS] 1039 \\ Q.EXISTS_TAC `n` \\ Q.EXISTS_TAC `r3` 1040 \\ SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1041 \\ STRIP_TAC THEN1 1042 (POP_ASSUM (K ALL_TAC) 1043 \\ Q.UNABBREV_TAC `n` 1044 \\ ASM_REWRITE_TAC [arm_token_def,CONS_11,GSYM ORD_11] 1045 \\ REWRITE_TAC [EVAL ``ORD #"'"``] 1046 \\ REWRITE_TAC [EVAL ``ORD #"."``] 1047 \\ REWRITE_TAC [EVAL ``ORD #"("``] 1048 \\ REWRITE_TAC [EVAL ``ORD #")"``] 1049 \\ FULL_SIMP_TAC std_ss [MEM]) 1050 \\ FULL_SIMP_TAC (std_ss++star_ss) [ 1051 AC ADD_COMM ADD_ASSOC, 1052 GSYM WORD_ADD_ASSOC,word_add_n2w]) 1053 \\ `~(n2w (ORD h) <+ 0x30w:word32) ==> ~(n2w (ORD h) <+ 0x3Aw:word32)` by 1054 (FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_LO,w2n_n2w,number_char_def] \\ DECIDE_TAC) 1055 \\ ASM_SIMP_TAC std_ss [] 1056 \\ STRIP_ASSUME_TAC (Q.SPECL [`t`,`identifier_char`] read_while_thm2) 1057 \\ `sexp_lex (STRING h t) = STRING h t1 :: sexp_lex t2` by 1058 (ONCE_REWRITE_TAC [sexp_lex_def] 1059 \\ ASM_SIMP_TAC std_ss [space_char_def,MEM,GSYM ORD_11, 1060 EVAL ``ORD #"("``,EVAL ``ORD #")"``,EVAL ``ORD #"."``,EVAL ``ORD #"'"``] 1061 \\ FULL_SIMP_TAC std_ss [number_char_def,MEM,DECIDE ``48 <= m = ~(m < 48:num)``,LET_DEF]) 1062 \\ FULL_SIMP_TAC std_ss [GSYM STRCAT_ASSOC] 1063 \\ `EVERY identifier_char (EXPLODE (STRING h t1))` by 1064 (FULL_SIMP_TAC std_ss [identifier_char_def,EXPLODE_def,EVERY_DEF,MEM,CONS_11,GSYM ORD_11, 1065 EVAL ``ORD #"("``,EVAL ``ORD #")"``,EVAL ``ORD #"."``,EVAL ``ORD #"'"``]) 1066 \\ `?c2 t3. (STRCAT t2 null_string = STRING c2 t3) /\ ~(identifier_char c2)` by 1067 (Cases_on `t2` \\ SIMP_TAC std_ss [STRCAT_def,null_string_def,CONS_11] 1068 THEN1 EVAL_TAC \\ FULL_SIMP_TAC std_ss [NOT_CONS_NIL,EXPLODE_def,HD]) 1069 \\ FULL_SIMP_TAC std_ss [] 1070 \\ `string_mem (STRCAT (STRING h t1) (STRING c2 t3)) (k,f,df)` by 1071 ASM_SIMP_TAC std_ss [STRCAT_def,string_mem_def] 1072 \\ `identifier_string (STRING h t1)` by 1073 FULL_SIMP_TAC std_ss [identifier_string_def,EXPLODE_def,HD,GSYM ORD_11, EVAL ``ORD #"'"``,MEM] 1074 \\ FULL_SIMP_TAC std_ss [all_symbols_def] 1075 \\ IMP_RES_TAC symbol_table_dom_IMPLIES 1076 \\ STRIP_ASSUME_TAC (UNDISCH_ALL (SIMP_RULE std_ss [GSYM NOT_CONS_NIL,GSYM AND_IMP_INTRO] 1077 (Q.INST [`c1`|->`c2`,`s1`|->`t3`] 1078 (Q.SPECL [`xs`,`STRING h t1`,`r3`,`f`,`g`] arm_symbol_lemma)))) 1079 \\ ASM_SIMP_TAC std_ss [] 1080 \\ `w2w (f k) = n2w (ORD h):word32` by 1081 ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,ORD_BOUND] 1082 \\ FULL_SIMP_TAC std_ss [] 1083 \\ Q.PAT_X_ASSUM `!xx. bb ==> bbb` (ASSUME_TAC o Q.SPEC `STRLEN t2`) 1084 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_STRCAT,DECIDE ``n < SUC (m + n:num)``] 1085 \\ Q.PAT_X_ASSUM `!xx. bb` (ASSUME_TAC o RW [] o Q.SPEC `t2`) 1086 \\ `string_mem (STRCAT t2 null_string) (r5i,f,df)` by ASM_SIMP_TAC std_ss [] 1087 \\ FULL_SIMP_TAC std_ss [EXPLODE_STRCAT,EVERY_APPEND,LENGTH,RW1[MULT_COMM]MULT] 1088 \\ SIMP_TAC std_ss [APPLY_UPDATE_THM,word_arith_lemma4] 1089 \\ SIMP_TAC (std_ss++SIZES_ss) [WORD_EQ_ADD_CANCEL,n2w_11] 1090 \\ FULL_SIMP_TAC std_ss [LENGTH,token_slots_def,SEP_CLAUSES] 1091 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,STAR_ASSOC] 1092 \\ `(p * one (r1,r3i - r3) * one (r1 + 0x4w,r3) * 1093 token_slots (r1 + 0x8w) (LENGTH (sexp_lex t2))) 1094 (fun2set ((r1 =+ r3i - r3) ((r1 + 0x4w =+ r3) h'),dh))` by SEP_WRITE_TAC 1095 \\ `ALIGNED (r1+8w)` by ALIGNED_TAC 1096 \\ Q.PAT_X_ASSUM `!r1 r2. bbb` (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o Q.SPECL 1097 [`r1+8w`,`r3`,`r5i`,`r6i`,`r7i`,`r8i`,`p * one (r1,r3i - r3) * one (r1 + 4w,r3)`,`(r3i - 3w, STRING h t1) INSERT x`,`add_symbol (STRING h t1) xs`,`df`,`dg`,`dh`,`dm`,`f`,`gi`,`(r1 =+ r3i - r3) ((r1 + 4w =+ r3) h')`,`mi`]) 1098 \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `xi` \\ ASM_SIMP_TAC std_ss [SUBSET_REFL] 1099 \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET] 1100 \\ `ALIGNED (r1+4w)` by ALIGNED_TAC 1101 \\ IMP_RES_TAC string_mem_IMP_IN 1102 \\ `(hi (r1 + 4w) = r3) /\ r1 + 0x4w IN dh` by SEP_READ_TAC 1103 \\ `(hi r1 = r3i-r3) /\ r1 IN dh` by SEP_READ_TAC 1104 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO] 1105 \\ STRIP_TAC THEN1 1106 (REWRITE_TAC [GSYM word_add_n2w] 1107 \\ SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC]) 1108 \\ REWRITE_TAC [arm_tokens_def] 1109 \\ SIMP_TAC std_ss [SEP_CLAUSES] 1110 \\ SIMP_TAC std_ss [SEP_EXISTS] 1111 \\ Q.EXISTS_TAC `r3i - r3` 1112 \\ Q.EXISTS_TAC `r3` 1113 \\ SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1114 \\ FULL_SIMP_TAC (std_ss++star_ss) [ 1115 AC ADD_COMM ADD_ASSOC, 1116 GSYM WORD_ADD_ASSOC,word_add_n2w] 1117 \\ ASM_SIMP_TAC std_ss [arm_token_def,WORD_SUB_ADD2] 1118 \\ ASM_REWRITE_TAC [arm_token_def,CONS_11,GSYM ORD_11] 1119 \\ REWRITE_TAC [EVAL ``ORD #"'"``] 1120 \\ REWRITE_TAC [EVAL ``ORD #"."``] 1121 \\ REWRITE_TAC [EVAL ``ORD #"("``] 1122 \\ REWRITE_TAC [EVAL ``ORD #")"``] 1123 \\ FULL_SIMP_TAC std_ss [MEM] 1124 \\ ASM_SIMP_TAC std_ss [EVERY_DEF,EXPLODE_def] 1125 \\ `(r3i - 0x3w,STRING h t1) IN ((r3i - 0x3w,STRING h t1) INSERT x)` 1126 by SIMP_TAC std_ss [IN_INSERT] 1127 \\ IMP_RES_TAC symbol_table_dom_ALIGNED 1128 \\ IMP_RES_TAC symbol_table_IMP_ALIGNED 1129 \\ REPEAT (Q.PAT_X_ASSUM `ALIGNED xxx` MP_TAC) 1130 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1131 \\ ONCE_REWRITE_TAC [word_sub_def] 1132 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 1133 \\ ONCE_REWRITE_TAC [word_sub_def] 1134 \\ REWRITE_TAC [WORD_ADD_ASSOC] 1135 \\ REPEAT STRIP_TAC 1136 \\ MATCH_MP_TAC ALIGNED_ADD 1137 \\ ASM_SIMP_TAC std_ss [ALIGNED_NEG]); 1138 1139 1140(* --- PARSER --- *) 1141 1142val LIST_STRCAT_def = Define ` 1143 (LIST_STRCAT [] = "") /\ 1144 (LIST_STRCAT (x::xs) = STRCAT x (LIST_STRCAT xs))`; 1145 1146val sexp2string_aux_def = tDefine "sexp2string_aux" ` 1147 (sexp2string_aux (Val n, b) = num2str n) /\ 1148 (sexp2string_aux (Sym s, b) = s) /\ 1149 (sexp2string_aux (Dot x y, b) = 1150 if isQuote (Dot x y) /\ b then LIST_STRCAT ["'"; sexp2string_aux (CAR y,T)] else 1151 let (a,e) = if b then ("(",")") else ("","") in 1152 if y = Sym "nil" then LIST_STRCAT [a; sexp2string_aux (x,T); e] else 1153 if isDot y 1154 then LIST_STRCAT [a; sexp2string_aux (x,T); " "; sexp2string_aux (y,F); e] 1155 else LIST_STRCAT [a; sexp2string_aux (x,T); " . "; sexp2string_aux (y,F); e])` 1156 (WF_REL_TAC `measure (LSIZE o FST)` \\ REWRITE_TAC [LSIZE_def,ADD1] 1157 \\ REPEAT STRIP_TAC 1158 \\ FULL_SIMP_TAC std_ss [isQuote_thm,SExp_11,CAR_def,LSIZE_def] 1159 \\ DECIDE_TAC); 1160 1161val sexp2string_def = Define `sexp2string x = sexp2string_aux (x, T)`; 1162 1163val sexp2tokens_def = tDefine "sexp2tokens" ` 1164 (sexp2tokens (Val n) b = [num2str n]) /\ 1165 (sexp2tokens (Sym s) b = [s]) /\ 1166 (sexp2tokens (Dot x y) b = 1167 if isQuote (Dot x y) /\ b then 1168 ["'"] ++ sexp2tokens (CAR y) T 1169 else if b then 1170 if y = Sym "nil" then ["("] ++ sexp2tokens x T ++ [")"] else 1171 if isDot y 1172 then ["("] ++ sexp2tokens x T ++ sexp2tokens y F ++ [")"] 1173 else ["("] ++ sexp2tokens x T ++ ["."] ++ sexp2tokens y F ++ [")"] 1174 else 1175 if y = Sym "nil" then sexp2tokens x T else 1176 if isDot y 1177 then sexp2tokens x T ++ sexp2tokens y F 1178 else sexp2tokens x T ++ ["."] ++ sexp2tokens y F)` 1179 (WF_REL_TAC `measure (LSIZE o FST)` \\ REWRITE_TAC [LSIZE_def,ADD1] \\ STRIP_TAC 1180 THEN1 (SIMP_TAC std_ss [isQuote_def,isDot_thm] \\ REPEAT STRIP_TAC 1181 \\ FULL_SIMP_TAC std_ss [CAR_def,CDR_def,LSIZE_def,ADD1] \\ DECIDE_TAC) 1182 \\ REPEAT STRIP_TAC \\ DECIDE_TAC); 1183 1184val sexp_parse_def = Define ` 1185 (sexp_parse [] exp stack = exp) /\ 1186 (sexp_parse (t::ts) exp stack = 1187 if t = ")" then sexp_parse ts (Sym "nil") (exp::stack) else 1188 if t = "." then sexp_parse ts (CAR exp) stack else 1189 if t = "(" then (if stack = [] then sexp_parse ts exp stack 1190 else sexp_parse ts (Dot exp (HD stack)) (TL stack)) else 1191 if t = "'" then (if isDot exp then sexp_parse ts (Dot (Dot (Sym "quote") (Dot (CAR exp) (Sym "nil"))) (CDR exp)) stack 1192 else sexp_parse ts exp stack) else 1193 if is_number_string t then sexp_parse ts (Dot (Val (str2num t)) exp) stack else 1194 sexp_parse ts (Dot (Sym t) exp) stack)`; 1195 1196val sexp_inject_def = Define ` 1197 (sexp_inject (Val m) x = Dot (Val m) x) /\ 1198 (sexp_inject (Sym s) x = Dot (Sym s) x) /\ 1199 (sexp_inject (Dot t1 t2) x = 1200 if x = Sym "nil" then Dot t1 t2 else 1201 if t2 = Sym "nil" then Dot t1 x else Dot t1 (sexp_inject t2 x))`; 1202 1203val parse_tac = 1204 REPEAT STRIP_TAC 1205 \\ SIMP_TAC std_ss [sexp2tokens_def,rich_listTheory.REVERSE,rich_listTheory.SNOC_APPEND,APPEND,REVERSE_APPEND,GSYM APPEND_ASSOC] 1206 \\ ASM_SIMP_TAC std_ss [sexp_parse_def] \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 1207 \\ SIMP_TAC std_ss [NOT_CONS_NIL,HD,TL,CAR_def] 1208 1209val sexp_ok_def = Define ` 1210 (sexp_ok (Val m) = m < 2**30) /\ 1211 (sexp_ok (Sym s) = identifier_string s /\ ~(s = "")) /\ 1212 (sexp_ok (Dot t1 t2) = sexp_ok t1 /\ sexp_ok t2)`; 1213 1214val sexp_ok_Sym = prove( 1215 ``sexp_ok (Sym s) ==> ~(s = "(") /\ ~(s = ".") /\ ~(s = ")") /\ 1216 ~(s = "'") /\ ~(is_number_string s)``, 1217 FULL_SIMP_TAC std_ss [sexp_ok_def,identifier_string_def] \\ REPEAT STRIP_TAC 1218 \\ FULL_SIMP_TAC std_ss [EXPLODE_def,EVERY_DEF,identifier_char_def,MEM,HD] \\ Cases_on `s` 1219 \\ FULL_SIMP_TAC std_ss [EXPLODE_def,EVERY_DEF,identifier_char_def,MEM,HD,is_number_string_def]); 1220 1221val sexp_ok_Val = prove( 1222 ``sexp_ok (Val n) ==> is_number_string (num2str n)``, 1223 `number_char = \c. 48 <= ORD c /\ ORD c < 58` by SIMP_TAC std_ss [FUN_EQ_THM,number_char_def] 1224 \\ ASM_REWRITE_TAC [is_number_string_def,number_char_def,str2num_num2str]); 1225 1226val is_number_string_IMP = prove( 1227 ``!s. is_number_string s ==> ~(s = ")") /\ ~(s = ".") /\ ~(s = "(") /\ ~(s = "'")``, 1228 Cases \\ SIMP_TAC std_ss [NOT_CONS_NIL,CONS_11,is_number_string_def,EVERY_DEF, 1229 EVAL ``ORD #"("``,EVAL ``ORD #")"``,EVAL ``ORD #"."``,EVAL ``ORD #"'"``, 1230 EXPLODE_def,number_char_def,GSYM ORD_11] 1231 \\ REPEAT STRIP_TAC \\ DISJ1_TAC \\ DECIDE_TAC); 1232 1233val sexp_parse_lemma = prove( 1234 ``!exp b ys x stack. 1235 sexp_ok exp /\ (~b ==> (x = Sym "nil")) ==> 1236 (sexp_parse (REVERSE (sexp2tokens exp b) ++ ys) x stack = 1237 sexp_parse ys (if b then Dot exp x else sexp_inject exp x) stack)``, 1238 completeInduct_on `LSIZE exp` \\ REVERSE Cases 1239 THEN1 1240 (REPEAT STRIP_TAC \\ IMP_RES_TAC sexp_ok_Sym 1241 \\ SIMP_TAC std_ss [sexp2tokens_def,rich_listTheory.REVERSE,rich_listTheory.SNOC_APPEND,APPEND] 1242 \\ Cases_on `b` \\ ASM_SIMP_TAC std_ss [sexp_parse_def] \\ SIMP_TAC std_ss [sexp_inject_def]) 1243 THEN1 1244 (REPEAT STRIP_TAC \\ IMP_RES_TAC sexp_ok_Val \\ IMP_RES_TAC is_number_string_IMP 1245 \\ SIMP_TAC std_ss [sexp2tokens_def,rich_listTheory.REVERSE,rich_listTheory.SNOC_APPEND,APPEND] 1246 \\ Cases_on `b` \\ ASM_SIMP_TAC std_ss [sexp_parse_def,str2num_num2str,sexp_inject_def]) 1247 \\ Q.ABBREV_TAC `exp = S'` \\ Q.ABBREV_TAC `exp' = S0` 1248 \\ REPEAT (Q.PAT_X_ASSUM `Abbrev bbb` (K ALL_TAC)) 1249 \\ NTAC 2 STRIP_TAC 1250 \\ REWRITE_TAC [sexp2tokens_def] 1251 \\ Cases_on `isQuote (Dot exp exp') /\ b` \\ ASM_SIMP_TAC std_ss [] THEN1 1252 (REWRITE_TAC [REVERSE_APPEND,rich_listTheory.REVERSE,rich_listTheory.SNOC_APPEND,APPEND,GSYM APPEND_ASSOC] 1253 \\ FULL_SIMP_TAC std_ss [isQuote_thm,SExp_11,CAR_def,sexp_ok_def] 1254 \\ REPEAT STRIP_TAC 1255 \\ `LSIZE y < LSIZE (Dot (Sym "quote") (Dot y (Sym "nil")))` by 1256 (FULL_SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC) 1257 \\ FULL_SIMP_TAC std_ss [] 1258 \\ Q.PAT_X_ASSUM `!m.bbb` (ASSUME_TAC o UNDISCH o Q.SPEC `LSIZE y`) 1259 \\ Q.PAT_X_ASSUM `!exp.bbb` (ASSUME_TAC o UNDISCH o RW [] o Q.SPECL [`T`,`"'"::ys`,`x`,`stack`] o RW [] o Q.SPEC `y`) 1260 \\ ASM_REWRITE_TAC [] 1261 \\ ONCE_REWRITE_TAC [sexp_parse_def] 1262 \\ REWRITE_TAC [EVAL ``"'" = ")"``,EVAL ``"'" = "("``,EVAL ``"'" = "."``,isDot_def] 1263 \\ SIMP_TAC std_ss [CAR_def,CDR_def]) 1264 \\ Q.PAT_X_ASSUM `~bb` (K ALL_TAC) 1265 \\ REWRITE_TAC [sexp_ok_def] 1266 \\ REPEAT STRIP_TAC 1267 \\ `LSIZE exp < v /\ LSIZE exp' < v` by (FULL_SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC) 1268 \\ Q.PAT_X_ASSUM `!m.bbb` (fn th => ASSUME_TAC (Q.SPEC `exp` (UNDISCH (Q.SPEC `LSIZE exp` th))) THEN 1269 ASSUME_TAC (Q.SPEC `exp'` (UNDISCH (Q.SPEC `LSIZE exp'` th)))) 1270 \\ FULL_SIMP_TAC std_ss [] 1271 \\ REPEAT (Q.PAT_X_ASSUM `sexp_ok _` (fn th => FULL_SIMP_TAC std_ss [th])) 1272 \\ Cases_on `b` THENL [ 1273 Cases_on `exp' = Sym "nil"` \\ ASM_SIMP_TAC std_ss [] 1274 THEN1 (`~isDot exp'` by ASM_SIMP_TAC std_ss [isDot_def] 1275 \\ REPEAT (Q.PAT_X_ASSUM `!x:bool. bbb` (ASSUME_TAC o RW[] o Q.SPEC `T`)) \\ parse_tac) 1276 \\ REVERSE (Cases_on `isDot exp'` \\ ASM_SIMP_TAC std_ss []) 1277 THEN1 (`sexp2tokens exp' F = sexp2tokens exp' T` by 1278 (Cases_on `exp'` \\ FULL_SIMP_TAC std_ss [isDot_def,sexp2tokens_def]) 1279 \\ ASM_REWRITE_TAC [] 1280 \\ REPEAT (Q.PAT_X_ASSUM `!x:bool. bbb` (ASSUME_TAC o RW[] o Q.SPEC `T`)) \\ parse_tac) 1281 \\ `~F ==> (Sym "nil" = Sym "nil")` by REWRITE_TAC [] 1282 \\ RES_TAC \\ ASM_REWRITE_TAC [] 1283 \\ REPEAT (Q.PAT_X_ASSUM `!x:bool. bbb` (ASSUME_TAC o RW[] o Q.SPEC `T`)) 1284 \\ Cases_on `isQuote exp'` \\ parse_tac \\ parse_tac 1285 \\ Cases_on `exp'` \\ FULL_SIMP_TAC std_ss [isDot_def,sexp_inject_def,CAR_def], 1286 Cases_on `exp' = Sym "nil"` \\ ASM_SIMP_TAC std_ss [] 1287 THEN1 (SIMP_TAC std_ss [sexp_inject_def] \\ METIS_TAC []) 1288 \\ REVERSE (Cases_on `isDot exp'`) \\ ASM_SIMP_TAC std_ss [isDot_def,CDR_def] 1289 THEN1 (REPEAT (Q.PAT_X_ASSUM `!x:bool. bbb` (ASSUME_TAC o RW[] o Q.SPEC `T`)) 1290 \\ `sexp2tokens exp' F = sexp2tokens exp' T` by 1291 (Cases_on `exp'` \\ FULL_SIMP_TAC std_ss [isDot_def,sexp2tokens_def]) 1292 \\ parse_tac \\ Cases_on `exp'` 1293 \\ FULL_SIMP_TAC std_ss [isDot_def,sexp_inject_def,CAR_def]) 1294 \\ REPEAT STRIP_TAC 1295 \\ `~F ==> (x = Sym "nil")` by FULL_SIMP_TAC std_ss [isDot_def] 1296 \\ ASM_SIMP_TAC std_ss [] \\ RES_TAC 1297 \\ REPEAT (Q.PAT_X_ASSUM `!x:bool. bbb` (ASSUME_TAC o RW[] o Q.SPEC `T`)) 1298 \\ FULL_SIMP_TAC std_ss [] 1299 \\ Q.PAT_X_ASSUM `x = Sym "nil"` (fn th => FULL_SIMP_TAC std_ss [th]) 1300 \\ parse_tac \\ ASM_SIMP_TAC std_ss [sexp_inject_def] 1301 \\ Q.PAT_X_ASSUM `isDot exp'` ASSUME_TAC \\ NTAC 2 (FULL_SIMP_TAC std_ss [isDot_thm]) 1302 \\ ASM_SIMP_TAC bool_ss [sexp_inject_def,CAR_def]]); 1303 1304val string2sexp_def = Define ` 1305 string2sexp s = CAR (sexp_parse (REVERSE (sexp_lex s)) (Sym "nil") [])`; 1306 1307val EVERY_read_while = prove( 1308 ``!s t. EVERY P (EXPLODE s) ==> (read_while P s t = (STRCAT t s,""))``, 1309 Induct 1310 \\ ASM_SIMP_TAC std_ss [read_while_def,STRCAT_def,STRCAT_EQNS,EVERY_DEF,EXPLODE_def] 1311 \\ REWRITE_TAC [GSYM STRCAT_ASSOC] \\ REWRITE_TAC [STRCAT_def]); 1312 1313val string_nil_or_not_def = Define ` 1314 string_nil_or_not P s = ~(s = "") ==> ~P (HD (EXPLODE s))`; 1315 1316val read_while_step = prove( 1317 ``!s t q. EVERY P (EXPLODE s) /\ string_nil_or_not P q ==> 1318 (read_while P (STRCAT s q) t = (STRCAT t s,q))``, 1319 Induct THENL [ 1320 Cases_on `q` \\ SIMP_TAC std_ss [STRCAT_EQNS,read_while_def, 1321 string_nil_or_not_def,NOT_CONS_NIL,EXPLODE_def,HD], 1322 ASM_SIMP_TAC std_ss [EXPLODE_def,EVERY_DEF,STRCAT_EQNS,read_while_def] 1323 \\ REWRITE_TAC [GSYM STRCAT_ASSOC,STRCAT_EQNS]]); 1324 1325val sexp2tokens_lemma = prove( 1326 ``!exp b t. sexp_ok exp /\ string_nil_or_not (\c. ~MEM c [#".";#"(";#")"] /\ ~space_char c) t ==> 1327 (sexp_lex (STRCAT (sexp2string_aux (exp,b)) t) = sexp2tokens exp b ++ sexp_lex t)``, 1328 completeInduct_on `LSIZE exp` \\ REVERSE Cases 1329 THEN1 1330 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def,sexp2tokens_def,sexp_lex_def] 1331 \\ Cases_on `s` \\ FULL_SIMP_TAC std_ss [sexp_lex_def,CONS_11,sexp_ok_def,STRCAT_EQNS] 1332 \\ FULL_SIMP_TAC std_ss [identifier_string_def,EVERY_DEF,EXPLODE_def, 1333 identifier_char_def,MEM,CONS_11,HD] 1334 \\ `string_nil_or_not identifier_char t` by 1335 (Cases_on `t` \\ FULL_SIMP_TAC std_ss [string_nil_or_not_def,NOT_CONS_NIL, 1336 EXPLODE_def,HD,identifier_char_def,MEM,CONS_11]) 1337 \\ IMP_RES_TAC read_while_step 1338 \\ ASM_SIMP_TAC std_ss [LET_DEF,STRCAT_EQNS,APPEND]) 1339 THEN1 1340 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [sexp2string_aux_def,sexp2tokens_def,sexp_lex_def] 1341 \\ IMP_RES_TAC sexp_ok_Val 1342 \\ Cases_on `num2str n` \\ FULL_SIMP_TAC std_ss [str2num_num2str,is_number_string_def] 1343 \\ FULL_SIMP_TAC std_ss [sexp_lex_def,EVERY_DEF,EXPLODE_def,STRCAT_EQNS] 1344 \\ `~space_char h /\ ~MEM h [#"("; #")"; #"."; #"'"]` by 1345 (FULL_SIMP_TAC std_ss [space_char_def,MEM,GSYM ORD_11,number_char_def, 1346 EVAL ``ORD #"("``,EVAL ``ORD #")"``,EVAL ``ORD #"."``,EVAL ``ORD #"'"``] 1347 \\ DECIDE_TAC) 1348 \\ ASM_SIMP_TAC std_ss [] 1349 \\ `string_nil_or_not number_char t` by 1350 (Cases_on `t` \\ FULL_SIMP_TAC std_ss [string_nil_or_not_def,NOT_CONS_NIL, 1351 EXPLODE_def,HD,identifier_char_def,MEM,CONS_11] 1352 \\ FULL_SIMP_TAC std_ss [space_char_def,number_char_def, 1353 EVAL ``ORD #"("``,EVAL ``ORD #")"``,EVAL ``ORD #"."``,EVAL ``ORD #"'"``] 1354 \\ DECIDE_TAC) 1355 \\ IMP_RES_TAC read_while_step 1356 \\ ASM_SIMP_TAC std_ss [LET_DEF,STRCAT_EQNS,APPEND]) 1357 \\ REWRITE_TAC [ADD1,LSIZE_def,sexp_ok_def] \\ REPEAT STRIP_TAC 1358 \\ Q.ABBREV_TAC `exp = S'` \\ Q.ABBREV_TAC `exp' = S0` 1359 \\ REPEAT (Q.PAT_X_ASSUM `Abbrev bbb` (K ALL_TAC)) 1360 \\ SIMP_TAC std_ss [sexp2string_aux_def,sexp2tokens_def] 1361 \\ Cases_on `isQuote (Dot exp exp') /\ b` \\ ASM_REWRITE_TAC [] THEN1 1362 (SIMP_TAC std_ss [LIST_STRCAT_def,STRCAT_EQNS,APPEND,sexp_lex_def,MEM] 1363 \\ `~space_char #"'"` by EVAL_TAC \\ ASM_SIMP_TAC std_ss [] 1364 \\ FULL_SIMP_TAC std_ss [isQuote_def,isDot_def,CAR_def,CDR_def] 1365 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def,LSIZE_def,ADD1] 1366 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def,LSIZE_def,ADD1] 1367 \\ `LSIZE a < LSIZE a + LSIZE b' + 1 + 1` by DECIDE_TAC 1368 \\ RES_TAC \\ METIS_TAC [sexp_ok_def]) 1369 \\ Q.PAT_X_ASSUM `~bbb` (K ALL_TAC) 1370 \\ `LSIZE exp < v /\ LSIZE exp' < v` by DECIDE_TAC 1371 \\ `!t. string_nil_or_not (\c. ~MEM c [#"."; #"("; #")"] /\ ~space_char c) t ==> 1372 (sexp_lex (STRCAT (sexp2string_aux (exp,T)) t) = sexp2tokens exp T ++ sexp_lex t)` 1373 by METIS_TAC [] 1374 \\ `!t. string_nil_or_not (\c. ~MEM c [#"."; #"("; #")"] /\ ~space_char c) t ==> 1375 (sexp_lex (STRCAT (sexp2string_aux (exp',F)) t) = sexp2tokens exp' F ++ sexp_lex t)` 1376 by METIS_TAC [] 1377 \\ Q.PAT_X_ASSUM `!m. m < v ==> fgh` (K ALL_TAC) 1378 \\ `~(space_char #".") /\ ~(space_char #"(") /\ ~(space_char #")") /\ space_char #" "` by EVAL_TAC 1379 \\ Q.ABBREV_TAC `g = (\c. ~MEM c [#"."; #"("; #")"] /\ ~space_char c)` 1380 \\ Cases_on `b` \\ ASM_SIMP_TAC std_ss [LIST_STRCAT_def,STRCAT_EQNS,LET_DEF] THENL [ 1381 Cases_on `exp' = Sym "nil"` \\ ASM_SIMP_TAC std_ss [] THENL [ 1382 ASM_SIMP_TAC std_ss [STRCAT_EQNS,sexp_lex_def,MEM,APPEND,CONS_11] 1383 \\ REWRITE_TAC [GSYM STRCAT_ASSOC] 1384 \\ `string_nil_or_not g (STRCAT ")" t)` by 1385 (Q.UNABBREV_TAC `g` \\ SIMP_TAC std_ss [STRCAT_EQNS,string_nil_or_not_def,EXPLODE_def,HD,MEM]) 1386 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [STRCAT_EQNS,sexp_lex_def,MEM,GSYM APPEND_ASSOC,APPEND], 1387 Cases_on `isDot exp'` \\ ASM_SIMP_TAC std_ss [STRCAT_EQNS] THENL [ 1388 ASM_SIMP_TAC std_ss [sexp_lex_def,MEM,APPEND,CONS_11] 1389 \\ REWRITE_TAC [GSYM STRCAT_ASSOC] 1390 \\ `string_nil_or_not g (STRCAT (STRING #" " (STRCAT (sexp2string_aux (exp',F)) ")")) t)` by 1391 (Q.UNABBREV_TAC `g` \\ SIMP_TAC std_ss [STRCAT_EQNS,string_nil_or_not_def, 1392 EXPLODE_def,HD,MEM,EVAL ``space_char #" "``]) 1393 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [STRCAT_EQNS,sexp_lex_def] 1394 \\ REWRITE_TAC [GSYM STRCAT_ASSOC] 1395 \\ `string_nil_or_not g (STRCAT ")" t)` by 1396 (Q.UNABBREV_TAC `g` \\ SIMP_TAC std_ss [STRCAT_EQNS,string_nil_or_not_def,EXPLODE_def,HD,MEM]) 1397 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [STRCAT_EQNS,sexp_lex_def,MEM,GSYM APPEND_ASSOC,APPEND], 1398 ASM_SIMP_TAC std_ss [sexp_lex_def,MEM,APPEND,CONS_11] 1399 \\ REWRITE_TAC [GSYM STRCAT_ASSOC] 1400 \\ `string_nil_or_not g (STRCAT (STRING #" " 1401 (STRING #"." (STRING #" " (STRCAT (sexp2string_aux (exp',F)) ")")))) t)` by 1402 (Q.UNABBREV_TAC `g` \\ SIMP_TAC std_ss [STRCAT_EQNS,string_nil_or_not_def, 1403 EXPLODE_def,HD,MEM,EVAL ``space_char #" "``]) 1404 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [sexp_lex_def] 1405 \\ ASM_SIMP_TAC std_ss [STRCAT_EQNS,sexp_lex_def,MEM] 1406 \\ REWRITE_TAC [GSYM STRCAT_ASSOC] 1407 \\ `string_nil_or_not g (STRCAT ")" t)` by 1408 (Q.UNABBREV_TAC `g` \\ SIMP_TAC std_ss [STRCAT_EQNS,string_nil_or_not_def,EXPLODE_def,HD,MEM]) 1409 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [STRCAT_EQNS,sexp_lex_def,MEM,GSYM APPEND_ASSOC,APPEND]]], 1410 Cases_on `exp' = Sym "nil"` \\ ASM_SIMP_TAC std_ss [] 1411 \\ Cases_on `isDot exp'` \\ ASM_SIMP_TAC std_ss [STRCAT_EQNS] THENL [ 1412 ASM_SIMP_TAC std_ss [sexp_lex_def,MEM,APPEND,CONS_11] 1413 \\ REWRITE_TAC [GSYM STRCAT_ASSOC] 1414 \\ `string_nil_or_not g (STRCAT (STRING #" " (sexp2string_aux (exp',F))) t)` by 1415 (Q.UNABBREV_TAC `g` \\ SIMP_TAC std_ss [STRCAT_EQNS,string_nil_or_not_def, 1416 EXPLODE_def,HD,MEM,EVAL ``space_char #" "``]) 1417 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [STRCAT_EQNS,sexp_lex_def] 1418 \\ REWRITE_TAC [GSYM STRCAT_ASSOC,APPEND_ASSOC], 1419 ASM_SIMP_TAC std_ss [sexp_lex_def,MEM,APPEND,CONS_11] 1420 \\ REWRITE_TAC [GSYM STRCAT_ASSOC] 1421 \\ `string_nil_or_not g (STRCAT (STRING #" " 1422 (STRING #"." (STRING #" " ((sexp2string_aux (exp',F)))))) t)` by 1423 (Q.UNABBREV_TAC `g` \\ SIMP_TAC std_ss [STRCAT_EQNS,string_nil_or_not_def, 1424 EXPLODE_def,HD,MEM,EVAL ``space_char #" "``]) 1425 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [sexp_lex_def] 1426 \\ ASM_SIMP_TAC std_ss [STRCAT_EQNS,sexp_lex_def,MEM] 1427 \\ REWRITE_TAC [GSYM STRCAT_ASSOC,GSYM APPEND_ASSOC,APPEND]]]); 1428 1429val sexp_lex_sexp2str = 1430 (RW [string_nil_or_not_def,sexp_lex_def,APPEND_NIL,STRCAT_EQNS] o 1431 Q.SPECL [`exp`,`T`,`""`]) sexp2tokens_lemma; 1432 1433val string2sexp_sexp2string = store_thm("string2sexp_sexp2string", 1434 ``!x. sexp_ok x ==> (string2sexp (sexp2string x) = x)``, 1435 REWRITE_TAC [string2sexp_def,sexp2string_def] 1436 \\ SIMP_TAC std_ss [sexp_lex_sexp2str, 1437 RW [APPEND_NIL] (Q.SPECL [`x`,`T`,`[]`] sexp_parse_lemma)] 1438 \\ SIMP_TAC std_ss [sexp_parse_def,CAR_def]); 1439 1440 1441(* PARSER IMPLEMENTATION *) 1442 1443val (th,arm_parse1_def,arm_parse1_pre_def) = compile_all `` 1444 arm_parse1 (r4:word32,r7:word32,r8:word32,dh:word32 set,h:word32->word32) = 1445 let h = (r4 =+ r7) h in 1446 let h = (r4 + 0x4w =+ r8) h in 1447 let r7 = 0x3w in 1448 let r8 = r4 in 1449 (r4:word32,r7:word32,r8:word32,dh,h)`` 1450 1451val (th,arm_parse2_def,arm_parse2_pre_def) = compile_all `` 1452 arm_parse2 (r4:word32,r6:word32,r7:word32,r8,dh:word32 set,h:word32->word32) = 1453 if r8 && 0x3w = 0x0w then 1454 (let r6 = h r8 in 1455 let h = (r4 =+ r7) h in 1456 let r7 = r8 in 1457 let h = (r4 + 4w =+ r6) h in 1458 let r8 = h (r8 + 0x4w) in 1459 let r6 = 3w in 1460 let h = (r7 =+ r6) h in 1461 let h = (r7 + 0x4w =+ r6) h in 1462 let r7 = r4 in 1463 (r4,r6,r7,r8,dh,h)) 1464 else 1465 (let r6 = 3w in 1466 let h = (r4 =+ r6) h in 1467 let h = (r4 + 0x4w =+ r6) h in 1468 (r4,r6,r7,r8,dh,h))`` 1469 1470val (th,arm_parse3_def,arm_parse3_pre_def) = compile_all `` 1471 arm_parse3 (r4:word32,r7:word32,dh:word32 set,h:word32->word32) = 1472 (if r7 && 3w = 0x0w then 1473 (let r6 = r7 in 1474 let r7 = h r7 in 1475 let r3 = 3w in 1476 let h = (r6 =+ r3) h in 1477 let r6 = 0x3w in 1478 let h = (r4 =+ r6) h in 1479 let h = (r4 + 0x4w =+ r6) h in 1480 (r4,r6,r7,dh,h)) 1481 else 1482 (let r6 = 0x3w in 1483 let h = (r4 =+ r6) h in 1484 let h = (r4 + 0x4w =+ r6) h in 1485 (r4,r6,r7,dh,h)))`` 1486 1487val (th,arm_parse4_def,arm_parse4_pre_def) = compile_all `` 1488 arm_parse4 (r4:word32,r5:word32,r7:word32,dh:word32 set,h:word32->word32) = 1489 if r7 && 3w = 0x0w then 1490 (let r6 = h r7 in 1491 let h = (r5 + 0x8w =+ r6) h in 1492 let r5 = r5 + 0x8w in 1493 let r6 = 0x3w in 1494 let h = (r5 + 0x4w =+ r6) h in 1495 let r6 = 0x1Bw in 1496 let h = (r4 + 0x4w =+ r5) h in 1497 let h = (r4 =+ r6) h in 1498 let h = (r7 =+ r4) h in 1499 (r4,r5,r6,r7,dh,h)) 1500 else 1501 (let r6 = 0x3w:word32 in 1502 let h = (r5 + 0x8w =+ r6) h in 1503 let r5 = r5 + 0x8w in 1504 let h = (r5 + 0x4w =+ r6) h in 1505 let h = (r4 =+ r6) h in 1506 let h = (r4 + 0x4w =+ r6) h in 1507 (r4,r5,r6,r7,dh,h))``; 1508 1509val (th,arm_parse_next_def,arm_parse_next_pre_def) = compile_all `` 1510 arm_parse_next (r4,r5,r6,r7,r8,dh,h) = 1511 if r6 && 3w = 0x0w then 1512 if r6 = 0x8w then 1513 (let (r4,r7,r8,dh,h) = arm_parse1 (r4,r7,r8,dh,h) 1514 in (r4,r5,r6,r7,r8,dh,h)) 1515 else 1516 if r6 = 0x4w then 1517 (let (r4,r6,r7,r8,dh,h) = arm_parse2 (r4,r6,r7,r8,dh,h) 1518 in (r4,r5,r6,r7,r8,dh,h)) 1519 else 1520 if r6 = 0xCw then 1521 (let (r4,r6,r7,dh,h) = arm_parse3 (r4,r7,dh,h) 1522 in (r4,r5,r6,r7,r8,dh,h)) 1523 else 1524 (let (r4,r5,r6,r7,dh,h) = arm_parse4 (r4,r5,r7,dh,h) 1525 in (r4,r5,r6,r7,r8,dh,h)) 1526 else 1527 (let h = (r4 + 0x4w =+ r7) h in 1528 let r7 = r4 in 1529 (r4,r5,r6,r7,r8,dh,h))`` 1530 1531val (th,arm_parse_loop_def,arm_parse_loop_pre_def) = compile_all `` 1532 arm_parse_loop1 (r4,r5,r6,r7,r8,dh:word32 set,h:word32->word32) = 1533 if r6 = 40w then 1534 if r7 && 3w = 0w then 1535 let r6 = 3w in 1536 let r8 = r7 in 1537 let r7 = h r7 in 1538 let h = (r8 =+ r6) h in 1539 (r4,r5,r6,r7,r8,dh,h) 1540 else 1541 (r4,r5,r6,r7,r8,dh,h) 1542 else 1543 let (r4,r5,r6,r7,r8,dh,h) = arm_parse_next (r4,r5,r6,r7,r8,dh,h) in 1544 let r6 = h (r4 - 0x8w) in 1545 let r4 = r4 - 0x8w in 1546 arm_parse_loop1 (r4,r5,r6,r7,r8,dh,h)``; 1547 1548val sexp_list_def = Define ` 1549 (sexp_list [] = Sym "nil") /\ 1550 (sexp_list (x::xs) = Dot x (sexp_list xs))`; 1551 1552val add_set_def = Define `add_set x s (i,j) = (x + i,j) IN s`; 1553 1554val SPLIT_thm = prove( 1555 ``!x y z. SPLIT x (y,z) = (y = x DIFF z) /\ z SUBSET x``, 1556 FULL_SIMP_TAC std_ss [set_sepTheory.SPLIT_def,EXTENSION,IN_DELETE, 1557 IN_DIFF,IN_UNION,DISJOINT_DEF,IN_INTER,NOT_IN_EMPTY,SUBSET_DEF] 1558 \\ METIS_TAC []); 1559 1560val SPLIT_DISJOINT_DISJOINT = prove( 1561 ``SPLIT (x DELETE t1 DELETE t2) (y,z) /\ DISJOINT i x ==> DISJOINT i y``, 1562 FULL_SIMP_TAC std_ss [DISJOINT_DEF,EXTENSION,NOT_IN_EMPTY,IN_INTER,IN_UNION,SPLIT_thm,IN_DELETE,SUBSET_DEF,IN_DELETE,IN_DIFF] \\ METIS_TAC []); 1563 1564val SET_TAC = 1565 FULL_SIMP_TAC std_ss [DISJOINT_DEF,EXTENSION,NOT_IN_EMPTY,IN_INTER, 1566 IN_UNION,IN_INSERT,IN_DELETE,IN_DIFF,SUBSET_DEF,set_sepTheory.SPLIT_def] \\ METIS_TAC [] 1567 1568val arm_tokens2_def = Define ` 1569 (arm_tokens2 a [] b x y = cond (a = y)) /\ 1570 (arm_tokens2 a (str::xs) b x y = 1571 SEP_EXISTS w1:word32 w2:word32. one (a,w1) * one (a+4w,w2) * 1572 cond (arm_token w1 str b x) * 1573 arm_tokens2 (a - 8w:word32) xs b x y)`; 1574 1575val arm_tokens2_SNOC = prove( 1576 ``!xs a b x w. arm_tokens2 a (xs ++ [h]) b x w = 1577 arm_tokens2 a xs b x (w + 8w) * arm_tokens2 (w + 8w) [h] b x w``, 1578 Induct THENL [ 1579 REPEAT STRIP_TAC 1580 \\ SIMP_TAC std_ss [arm_tokens2_def,APPEND] 1581 \\ REWRITE_TAC [WORD_EQ_SUB_RADD] 1582 \\ Cases_on `a = w + 8w` \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES], 1583 ASM_REWRITE_TAC [APPEND,arm_tokens2_def,WORD_ADD_SUB] 1584 \\ SIMP_TAC std_ss [SEP_CLAUSES] 1585 \\ SIMP_TAC (std_ss++star_ss) []]); 1586 1587val arm_tokens_EQ_arm_tokens2 = prove( 1588 ``!xs a b x y. arm_tokens a xs b x y = arm_tokens2 (y - 8w) (REVERSE xs) b x (a - 8w)``, 1589 Induct 1590 \\ REWRITE_TAC [arm_tokens2_def,arm_tokens_def,REVERSE_DEF] 1591 \\ REPEAT STRIP_TAC \\ REWRITE_TAC [WORD_LCANCEL_SUB] 1592 THEN1 (Cases_on `a = y` \\ ASM_SIMP_TAC std_ss []) 1593 \\ ASM_REWRITE_TAC [arm_tokens2_SNOC,WORD_SUB_ADD,WORD_ADD_SUB] 1594 \\ SIMP_TAC std_ss [SEP_CLAUSES,arm_tokens2_def] 1595 \\ SIMP_TAC (std_ss++star_ss) []); 1596 1597val arm_tokens4_def = Define ` 1598 arm_tokens4 a xs b x y = 1599 arm_tokens2 a xs b x y * one (y,40w) * SEP_EXISTS w. one (y+4w,w)`; 1600 1601val arm_tokens4_thm = prove( 1602 ``arm_tokens4 a (str::xs) b x y = 1603 arm_tokens2 a [str] b x (a - 8w) * arm_tokens4 (a - 8w) xs b x y``, 1604 REWRITE_TAC [arm_tokens4_def,arm_tokens2_def] 1605 \\ REWRITE_TAC [STAR_ASSOC] 1606 \\ SIMP_TAC std_ss [SEP_CLAUSES]); 1607 1608val arm_tokens3_def = Define ` 1609 (arm_tokens3 a [] q = cond (a = q)) /\ 1610 (arm_tokens3 a (str::xs) q = 1611 if str = "'" then SEP_EXISTS w3:word32 w4. 1612 one (a,w3) * one (a+4w,w4) * arm_tokens3 (a + 8w) xs q 1613 else arm_tokens3 a xs q)`; 1614 1615val lisp_exp_def = Define ` 1616 (lisp_exp (Sym s) a (b,d) = cond (ALIGNED (a - 3w) /\ (b + a - 3w:word32,s) IN d)) /\ 1617 (lisp_exp (Val n) a (b,d) = cond (a = ADDR32 (n2w n) + 2w)) /\ 1618 (lisp_exp (Dot x y) a (b,d) = cond (ALIGNED a /\ (w2n (b - a) MOD 8 = 0)) * 1619 SEP_EXISTS a1 a2. one (a,a1) * one (a+4w,a2) * lisp_exp x a1 (b,d) * lisp_exp y a2 (b,d))`; 1620 1621val SEP_EXPS_def = Define ` 1622 (SEP_EXPS [] (b,d) = emp) /\ 1623 (SEP_EXPS ((a,x)::xs) (b,d) = lisp_exp x a (b,d) * SEP_EXPS xs (b,d))`; 1624 1625val SEP_FILL_def = Define `SEP_FILL (b,d) = SEP_EXISTS xs. SEP_EXPS xs (b,d)`; 1626 1627val lisp_exp_FILL = prove( 1628 ``!exp exp2 a a2 b d a. 1629 (lisp_exp exp a (b,d) * lisp_exp exp2 a2 (b,d) * SEP_FILL (b,d)) s ==> 1630 (lisp_exp exp a (b,d) * SEP_FILL (b,d)) s``, 1631 SIMP_TAC std_ss [SEP_FILL_def,SEP_CLAUSES] 1632 \\ SIMP_TAC std_ss [SEP_EXISTS] 1633 \\ REPEAT STRIP_TAC 1634 \\ Q.EXISTS_TAC `(a2,exp2)::y` 1635 \\ ASM_REWRITE_TAC [SEP_EXPS_def,STAR_ASSOC]); 1636 1637val LENGTH_LEMMA1 = prove( 1638 ``(0x8w + r4 - n2w (8 * LENGTH (x::xs)) = r4 - n2w (8 * LENGTH xs)) /\ 1639 (r4 + 0x8w - n2w (8 * LENGTH (x::xs)) = r4 - n2w (8 * LENGTH xs))``, 1640 REWRITE_TAC [LENGTH,MULT_CLAUSES,GSYM word_add_n2w] 1641 \\ REWRITE_TAC [WORD_SUB_PLUS,WORD_ADD_SUB] 1642 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 1643 \\ REWRITE_TAC [WORD_SUB_PLUS,WORD_ADD_SUB]); 1644 1645val WORD_EQ_SUB_CANCEL = prove( 1646 ``!x:'a word y. (x - y = x) = (y = 0w)``, 1647 METIS_TAC [WORD_RCANCEL_SUB,WORD_SUB_RZERO]) 1648 1649val LENGTH_LEMMA2 = prove( 1650 ``LENGTH (x::xs) <= 536870912 ==> 1651 ((n2w (8 * LENGTH xs) = 0w:word32) = (xs = [])) /\ 1652 LENGTH xs <= 536870912``, 1653 SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LENGTH] 1654 \\ REPEAT STRIP_TAC 1655 \\ `8 * LENGTH xs < 4294967296` by DECIDE_TAC 1656 \\ ASM_SIMP_TAC std_ss [LENGTH_NIL] \\ DECIDE_TAC); 1657 1658val ALIGNED8_def = Define ` 1659 ALIGNED8 x = (w2n x MOD 8 = 0)`; 1660 1661val ALIGNED8_LEMMA = prove( 1662 ``!x:word32. ALIGNED8 (x + 0x8w) = ALIGNED8 x``, 1663 REWRITE_TAC [ALIGNED8_def] 1664 \\ Cases \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_add_n2w,w2n_n2w] 1665 \\ REWRITE_TAC [GSYM (EVAL ``8 * 536870912``)] 1666 \\ SIMP_TAC bool_ss [MOD_MULT_MOD,DECIDE ``0<8:num /\ 0<536870912:num``] 1667 \\ SIMP_TAC std_ss [ADD_MODULUS]); 1668 1669val ALIGNED8_STEP = prove( 1670 ``!a:word32 b. 1671 (ALIGNED8 (b - (a - 0x8w)) = ALIGNED8 (b - a)) /\ 1672 (ALIGNED8 (b - (a + 0x8w)) = ALIGNED8 (b - a))``, 1673 NTAC 2 STRIP_TAC 1674 \\ SIMP_TAC std_ss [WORD_SUB_PLUS,WORD_SUB_SUB,WORD_ADD_SUB_SYM] 1675 \\ SIMP_TAC std_ss [ALIGNED8_LEMMA] 1676 \\ SIMP_TAC std_ss [GSYM (RW [WORD_SUB_ADD] (Q.SPEC `x - 8w` ALIGNED8_LEMMA))]); 1677 1678val arm_parse_lemma = prove( 1679 ``!xs r4 r5 r7 r8 df f d1 d2 d3 exp stack p. 1680 ALIGNED8 (b - r4) /\ ALIGNED8 (b - r5) /\ ALIGNED b /\ 1681 (ALIGNED r8 ==> ALIGNED8 (b - r8)) /\ 1682 (ALIGNED r7 ==> ALIGNED8 (b - r7)) /\ 1683 (arm_tokens4 r4 xs b d y * arm_tokens3 (r5 + 8w) xs q * lisp_exp exp r7 (b,d) * 1684 lisp_exp (sexp_list stack) r8 (b,d) * SEP_FILL (b,d) * p) (fun2set (f,df)) /\ 1685 (b + 0x18w,"quote") IN d /\ (b,"nil") IN d /\ 1686 ALIGNED r4 /\ ALIGNED r5 ==> 1687 ?r4i r5i r6i r7i r8i fi. 1688 arm_parse_loop1_pre (r4,r5,f r4,r7,r8,df,f) /\ 1689 (arm_parse_loop1(r4,r5,f r4,r7,r8,df,f) = (y,q - 8w,r6i,r7i,r8i,df,fi)) /\ 1690 (arm_tokens4 y [] b d y * lisp_exp (CAR (sexp_parse xs exp stack)) r7i (b,d) * SEP_FILL (b,d) * p) (fun2set (fi,df)) /\ 1691 r4 IN df``, 1692 Induct THEN1 1693 (REWRITE_TAC [sexp_parse_def,arm_tokens4_def,arm_tokens2_def] 1694 \\ ONCE_REWRITE_TAC [arm_parse_loop_pre_def,arm_parse_loop_def] 1695 \\ SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1696 \\ REPEAT STRIP_TAC 1697 \\ `(f y = 0x28w) /\ y IN df` by SEP_READ_TAC 1698 \\ ASM_SIMP_TAC std_ss [] 1699 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,SEP_FILL_def] 1700 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 1701 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 1702 \\ REWRITE_TAC [ALIGNED_INTRO] 1703 \\ `ALIGNED r7 = isDot exp` by 1704 (Cases_on `exp` 1705 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [lisp_exp_def,SEP_CLAUSES] 1706 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,isDot_def] 1707 \\ METIS_TAC [NOT_ALIGNED,ALIGNED_ADDR32,WORD_SUB_ADD]) 1708 \\ ASM_SIMP_TAC std_ss [LET_DEF] 1709 \\ REVERSE (Cases_on `isDot exp`) 1710 THEN1 1711 (`CAR exp = exp` by (Cases_on `exp` \\ FULL_SIMP_TAC std_ss [CAR_def,isDot_def]) 1712 \\ ASM_SIMP_TAC std_ss [] 1713 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_EXPS_def,arm_tokens3_def,SEP_CLAUSES] 1714 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1715 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_EXPS_def,arm_tokens3_def,SEP_CLAUSES] 1716 \\ ASM_SIMP_TAC std_ss [WORD_EQ_SUB_LADD] 1717 \\ Q.EXISTS_TAC `(r8,sexp_list stack)::y'` 1718 \\ Q.EXISTS_TAC `y''` 1719 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_EXPS_def,arm_tokens3_def,SEP_CLAUSES] 1720 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1721 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_EXPS_def,arm_tokens3_def,SEP_CLAUSES]) 1722 \\ ASM_SIMP_TAC std_ss [] 1723 \\ FULL_SIMP_TAC std_ss [isDot_thm,lisp_exp_def,SEP_CLAUSES] 1724 \\ FULL_SIMP_TAC std_ss [isDot_thm,lisp_exp_def,SEP_CLAUSES] 1725 \\ FULL_SIMP_TAC std_ss [CAR_def,STAR_ASSOC,SEP_EXISTS] 1726 \\ `(f r7 = y''') /\ r7 IN df` by SEP_READ_TAC 1727 \\ ASM_SIMP_TAC std_ss [] 1728 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_EXPS_def,arm_tokens3_def,SEP_CLAUSES] 1729 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1730 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_EXPS_def,arm_tokens3_def,SEP_CLAUSES] 1731 \\ ASM_SIMP_TAC std_ss [WORD_EQ_SUB_LADD] 1732 \\ Q.EXISTS_TAC `(r7,Dot (Sym "nil") b')::(r8,sexp_list stack)::y'` 1733 \\ Q.EXISTS_TAC `y''` 1734 \\ SIMP_TAC std_ss [SEP_EXPS_def,lisp_exp_def,SEP_CLAUSES] 1735 \\ SIMP_TAC std_ss [SEP_EXISTS] 1736 \\ Q.EXISTS_TAC `3w` 1737 \\ Q.EXISTS_TAC `y''''` 1738 \\ ASM_SIMP_TAC std_ss [WORD_SUB_REFL,ALIGNED_n2w,WORD_ADD_SUB,SEP_CLAUSES] 1739 \\ FULL_SIMP_TAC std_ss [arm_tokens3_def,SEP_CLAUSES] 1740 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1741 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_EXPS_def,arm_tokens3_def,SEP_CLAUSES] 1742 \\ SEP_WRITE_TAC) 1743 \\ SIMP_TAC std_ss [arm_tokens4_thm,arm_tokens2_def,SEP_CLAUSES] 1744 \\ REWRITE_TAC [STAR_ASSOC] 1745 \\ SIMP_TAC std_ss [SEP_EXISTS] 1746 \\ SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1747 \\ REPEAT STRIP_TAC 1748 \\ `ALIGNED (r4 - 8w) /\ ALIGNED (r5 + 8w)` by ALIGNED_TAC 1749 \\ `(f r4 = y') /\ r4 IN df` by SEP_READ_TAC 1750 \\ Cases_on `h = "'"` THEN1 1751 (FULL_SIMP_TAC std_ss [arm_tokens3_def,sexp_parse_def,SEP_CLAUSES] 1752 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 1753 \\ SIMP_TAC std_ss [] 1754 \\ Q.PAT_X_ASSUM `arm_token y' ccc b x` MP_TAC 1755 \\ FULL_SIMP_TAC std_ss [arm_token_def] 1756 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 1757 \\ SIMP_TAC std_ss [] 1758 \\ ONCE_REWRITE_TAC [arm_parse_loop_def,arm_parse_loop_pre_def] 1759 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LET_DEF,arm_parse_next_def,arm_parse_next_pre_def] 1760 \\ SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_n2w] 1761 \\ SIMP_TAC std_ss [LET_DEF,arm_parse4_pre_def,arm_parse4_def,ALIGNED_INTRO] 1762 \\ `ALIGNED r7 = isDot exp` by 1763 (Cases_on `exp` 1764 \\ FULL_SIMP_TAC std_ss [lisp_exp_def,SEP_CLAUSES] 1765 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [SEP_EXISTS,cond_STAR,isDot_def] 1766 \\ METIS_TAC [NOT_ALIGNED,ALIGNED_ADDR32,WORD_SUB_ADD]) 1767 \\ SIMP_TAC std_ss [word_arith_lemma1] 1768 \\ REVERSE (Cases_on `isDot exp` \\ ASM_SIMP_TAC std_ss []) 1769 THEN1 1770 (Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ 0x3w) 1771 ((r4 =+ 0x3w) ((r5 + 0xCw =+ 0x3w) ((r5 + 0x8w =+ 0x3w) f)))` 1772 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,word_arith_lemma1,STAR_ASSOC] 1773 \\ `(arm_tokens4 (r4 - 8w) xs b d y * arm_tokens3 ((r5 + 8w) + 0x8w) xs q * 1774 lisp_exp exp r7 (b,d) * lisp_exp (sexp_list stack) r8 (b,d) * 1775 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by 1776 (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5 + 8w`,`r7`,`r8`]) 1777 \\ ASM_SIMP_TAC std_ss [ALIGNED8_STEP] \\ STRIP_TAC 1778 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 1779 \\ REPEAT (Q.PAT_X_ASSUM `!df. bbb` (STRIP_ASSUME_TAC o SPEC_ALL)) 1780 \\ ASM_SIMP_TAC std_ss [] \\ ALIGNED_TAC \\ SEP_READ_TAC) 1781 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC) 1782 \\ Q.UNABBREV_TAC `f2` 1783 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,SEP_FILL_def,SEP_CLAUSES] 1784 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 1785 \\ Q.EXISTS_TAC `(r4,Dot (Sym "nil") (Sym "nil"))::(r5+8w,Dot (Sym "nil") (Sym "nil"))::y'''''` 1786 \\ SIMP_TAC std_ss [SEP_EXPS_def,lisp_exp_def] 1787 \\ SIMP_TAC std_ss [SEP_CLAUSES] 1788 \\ SIMP_TAC std_ss [SEP_EXISTS] 1789 \\ REPEAT (Q.EXISTS_TAC `3w`) 1790 \\ ASM_SIMP_TAC std_ss [WORD_SUB_REFL,ALIGNED_n2w,WORD_ADD_SUB,SEP_CLAUSES] 1791 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] 1792 \\ ASM_SIMP_TAC std_ss [GSYM ALIGNED8_def,ALIGNED8_STEP] 1793 \\ ASM_SIMP_TAC std_ss [WORD_ADD_0,SEP_CLAUSES,STAR_ASSOC,word_arith_lemma1] 1794 \\ SEP_WRITE_TAC) 1795 THEN 1796 (Q.ABBREV_TAC `f2 = (r7 =+ r4) ((r4 =+ 0x1Bw) ((r4 + 0x4w =+ r5 + 0x8w) 1797 ((r5 + 0xCw =+ 0x3w) ((r5 + 0x8w =+ f r7) f))))` 1798 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,word_arith_lemma1,STAR_ASSOC] 1799 \\ `(arm_tokens4 (r4 - 8w) xs b d y * arm_tokens3 ((r5 + 8w) + 0x8w) xs q * 1800 lisp_exp (Dot (Dot (Sym "quote") (Dot (CAR exp) (Sym "nil"))) (CDR exp)) 1801 r7 (b,d) * lisp_exp (sexp_list stack) r8 (b,d) * 1802 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5 + 8w`,`r7`,`r8`]) 1803 \\ ASM_SIMP_TAC std_ss [ALIGNED8_STEP] \\ STRIP_TAC 1804 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 1805 \\ REPEAT (Q.PAT_X_ASSUM `!df. bbb` (STRIP_ASSUME_TAC o SPEC_ALL)) 1806 \\ ALIGNED_TAC \\ ASM_SIMP_TAC std_ss [] 1807 \\ Q.PAT_X_ASSUM `isDot xxxxx` MP_TAC \\ STRIP_TAC 1808 \\ FULL_SIMP_TAC std_ss [isDot_thm,lisp_exp_def] 1809 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 1810 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 1811 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1812 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 1813 \\ ASM_SIMP_TAC std_ss [] \\ SEP_READ_TAC) 1814 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC) 1815 \\ Q.UNABBREV_TAC `f2` 1816 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,SEP_FILL_def,SEP_CLAUSES] 1817 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 1818 \\ Q.EXISTS_TAC `y'''''` 1819 \\ SIMP_TAC std_ss [lisp_exp_def] 1820 \\ SIMP_TAC std_ss [SEP_CLAUSES] 1821 \\ SIMP_TAC std_ss [SEP_EXISTS] 1822 \\ FULL_SIMP_TAC std_ss [isDot_thm,lisp_exp_def,SEP_CLAUSES] 1823 \\ FULL_SIMP_TAC std_ss [isDot_thm,lisp_exp_def,SEP_CLAUSES] 1824 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 1825 \\ Q.ABBREV_TAC `y2 = y''` 1826 \\ Q.ABBREV_TAC `y3 = y'''` 1827 \\ Q.ABBREV_TAC `y4 = y''''` 1828 \\ Q.ABBREV_TAC `y5 = y'''''` 1829 \\ Q.ABBREV_TAC `y6 = y''''''` 1830 \\ Q.ABBREV_TAC `y7 = y'''''''` 1831 \\ NTAC 6 (POP_ASSUM (K ALL_TAC)) 1832 \\ Q.EXISTS_TAC `r4` 1833 \\ Q.EXISTS_TAC `y7` 1834 \\ Q.EXISTS_TAC `0x1Bw` 1835 \\ Q.EXISTS_TAC `r5 + 8w` 1836 \\ Q.EXISTS_TAC `y6` 1837 \\ Q.EXISTS_TAC `3w` 1838 \\ ASM_SIMP_TAC std_ss [word_arith_lemma1,word_arith_lemma2,ALIGNED_n2w] 1839 \\ ASM_SIMP_TAC std_ss [word_arith_lemma4,word_arith_lemma3,WORD_ADD_0] 1840 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] 1841 \\ Q.PAT_X_ASSUM `bbb (fun2set (f,df))` MP_TAC 1842 \\ FULL_SIMP_TAC std_ss [GSYM ALIGNED8_def,ALIGNED8_STEP,SEP_CLAUSES] 1843 \\ STRIP_TAC 1844 \\ ASM_SIMP_TAC std_ss [WORD_ADD_0,SEP_CLAUSES,STAR_ASSOC,CAR_def,CDR_def] 1845 \\ `f r7 = y6` by SEP_READ_TAC 1846 \\ ASM_SIMP_TAC std_ss [] 1847 \\ SEP_WRITE_TAC)) 1848 \\ Cases_on `h = ")"` THEN1 1849 (FULL_SIMP_TAC std_ss [arm_tokens3_def,sexp_parse_def,SEP_CLAUSES] 1850 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 1851 \\ SIMP_TAC std_ss [] 1852 \\ Q.PAT_X_ASSUM `arm_token y' ccc b x` MP_TAC 1853 \\ FULL_SIMP_TAC std_ss [arm_token_def] 1854 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 1855 \\ SIMP_TAC std_ss [] 1856 \\ ONCE_REWRITE_TAC [arm_parse_loop_def,arm_parse_loop_pre_def] 1857 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LET_DEF,arm_parse_next_def,arm_parse_next_pre_def] 1858 \\ SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_n2w] 1859 \\ SIMP_TAC std_ss [LET_DEF,arm_parse1_def,arm_parse1_pre_def,ALIGNED_INTRO] 1860 \\ Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ r8) ((r4 =+ r7) f)` 1861 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,word_arith_lemma1,STAR_ASSOC] 1862 \\ `(arm_tokens4 (r4 - 8w) xs b d y * arm_tokens3 (r5 + 0x8w) xs q * 1863 lisp_exp (Sym "nil") 3w (b,d) * 1864 lisp_exp (sexp_list (exp::stack)) r4 (b,d) * 1865 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`3w`,`r4`]) 1866 \\ ASM_SIMP_TAC std_ss [ALIGNED8_STEP,ALIGNED_n2w] \\ STRIP_TAC 1867 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 1868 \\ REPEAT (Q.PAT_X_ASSUM `!df. bbb` (STRIP_ASSUME_TAC o SPEC_ALL)) 1869 \\ ASM_SIMP_TAC std_ss [] \\ ALIGNED_TAC \\ SEP_READ_TAC) 1870 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC) 1871 \\ Q.UNABBREV_TAC `f2` 1872 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,SEP_CLAUSES] 1873 \\ ASM_SIMP_TAC std_ss [sexp_list_def,lisp_exp_def,SEP_CLAUSES,WORD_SUB_REFL, 1874 ALIGNED_n2w,WORD_ADD_SUB] 1875 \\ FULL_SIMP_TAC std_ss [GSYM ALIGNED8_def,ALIGNED8_STEP,SEP_CLAUSES] 1876 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 1877 \\ Q.EXISTS_TAC `r7` 1878 \\ Q.EXISTS_TAC `r8` 1879 \\ SEP_WRITE_TAC) 1880 \\ Cases_on `h = "("` THEN1 1881 (FULL_SIMP_TAC std_ss [arm_tokens3_def,sexp_parse_def,SEP_CLAUSES] 1882 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 1883 \\ SIMP_TAC std_ss [] 1884 \\ Q.PAT_X_ASSUM `arm_token y' ccc b x` MP_TAC 1885 \\ FULL_SIMP_TAC std_ss [arm_token_def] 1886 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 1887 \\ SIMP_TAC std_ss [] 1888 \\ ONCE_REWRITE_TAC [arm_parse_loop_def,arm_parse_loop_pre_def] 1889 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LET_DEF,arm_parse_next_def,arm_parse_next_pre_def] 1890 \\ SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_n2w] 1891 \\ SIMP_TAC std_ss [LET_DEF,arm_parse2_def,arm_parse2_pre_def,ALIGNED_INTRO] 1892 \\ `ALIGNED r8 = (stack <> [])` by 1893 (Cases_on `stack` 1894 \\ FULL_SIMP_TAC std_ss [lisp_exp_def,SEP_CLAUSES,sexp_list_def] 1895 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [SEP_EXISTS,cond_STAR,isDot_def,NOT_CONS_NIL] 1896 \\ METIS_TAC [NOT_ALIGNED,ALIGNED_ADDR32,WORD_SUB_ADD]) 1897 \\ ASM_SIMP_TAC std_ss [word_arith_lemma1,NOT_IF] 1898 \\ REVERSE (Cases_on `stack` \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL]) 1899 THEN1 1900 (Q.ABBREV_TAC `f2 = (r8 + 0x4w =+ 0x3w) 1901 ((r8 =+ 0x3w) ((r4 + 0x4w =+ f r8) ((r4 =+ r7) f)))` 1902 \\ FULL_SIMP_TAC std_ss [sexp_list_def,lisp_exp_def,NOT_CONS_NIL,SEP_CLAUSES] 1903 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 1904 \\ Q.PAT_X_ASSUM `ALIGNED8 (b - r8)` ASSUME_TAC 1905 \\ `(r4 + 0x4w =+ f r8) ((r4 =+ r7) f) (r8 + 0x4w) = y''''` by 1906 (`r4 + 0x4w <> r8 + 0x4w` by SEP_NEQ_TAC 1907 \\ `r8 + 0x4w <> r4` by SEP_NEQ_TAC 1908 \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM] 1909 \\ SEP_READ_TAC) 1910 \\ ASM_SIMP_TAC std_ss [HD,TL] 1911 \\ POP_ASSUM (K ALL_TAC) 1912 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,word_arith_lemma1,STAR_ASSOC] 1913 \\ `(ALIGNED y'''' ==> ALIGNED8 (b - y''''))` by 1914 (STRIP_TAC \\ REVERSE (Cases_on `t`) 1915 \\ FULL_SIMP_TAC std_ss [lisp_exp_def,SEP_CLAUSES,sexp_list_def] 1916 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [GSYM ALIGNED8_def, 1917 cond_STAR,SEP_EXISTS] 1918 \\ IMP_RES_TAC NOT_ALIGNED \\ METIS_TAC [WORD_SUB_ADD]) 1919 \\ `(arm_tokens4 (r4 - 8w) xs b d y * arm_tokens3 (r5 + 0x8w) xs q * 1920 lisp_exp (Dot exp h') r4 (b,d) * lisp_exp (sexp_list t) y'''' (b,d) * 1921 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`r4`,`y''''`]) 1922 \\ ASM_SIMP_TAC std_ss [ALIGNED8_STEP,ALIGNED_n2w] \\ STRIP_TAC 1923 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 1924 \\ REPEAT (Q.PAT_X_ASSUM `!df. bbb` (STRIP_ASSUME_TAC o SPEC_ALL)) 1925 \\ ASM_SIMP_TAC std_ss [] \\ ALIGNED_TAC \\ SEP_READ_TAC) 1926 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC) 1927 \\ Q.UNABBREV_TAC `f2` 1928 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,SEP_CLAUSES,SEP_FILL_def] 1929 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 1930 \\ Q.EXISTS_TAC `(r8,Dot (Sym "nil") (Sym "nil"))::y'''''` 1931 \\ SIMP_TAC std_ss [SEP_EXPS_def,lisp_exp_def] 1932 \\ SIMP_TAC std_ss [SEP_CLAUSES] 1933 \\ SIMP_TAC std_ss [SEP_EXISTS] 1934 \\ Q.EXISTS_TAC `r7` 1935 \\ Q.EXISTS_TAC `y'''` 1936 \\ Q.EXISTS_TAC `3w` 1937 \\ Q.EXISTS_TAC `3w` 1938 \\ ASM_SIMP_TAC std_ss [WORD_SUB_REFL,ALIGNED_n2w,WORD_ADD_SUB,SEP_CLAUSES] 1939 \\ `f r8 = y'''` by SEP_READ_TAC 1940 \\ FULL_SIMP_TAC std_ss [GSYM ALIGNED8_def,ALIGNED8_STEP,SEP_CLAUSES] 1941 \\ ASM_SIMP_TAC std_ss [STAR_ASSOC] 1942 \\ SEP_WRITE_TAC) 1943 THEN 1944 (Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ 0x3w) ((r4 =+ 0x3w) f)` 1945 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,word_arith_lemma1,STAR_ASSOC] 1946 \\ `(arm_tokens4 (r4 - 8w) xs b d y * arm_tokens3 (r5 + 0x8w) xs q * 1947 lisp_exp exp r7 (b,d) * lisp_exp (sexp_list []) r8 (b,d) * 1948 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`r7`,`r8`]) 1949 \\ ASM_SIMP_TAC std_ss [ALIGNED8_STEP,ALIGNED_n2w] \\ STRIP_TAC 1950 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 1951 \\ REPEAT (Q.PAT_X_ASSUM `!df. bbb` (STRIP_ASSUME_TAC o SPEC_ALL)) 1952 \\ ASM_SIMP_TAC std_ss [] \\ ALIGNED_TAC \\ SEP_READ_TAC) 1953 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC) 1954 \\ Q.UNABBREV_TAC `f2` 1955 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,SEP_CLAUSES,SEP_FILL_def] 1956 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 1957 \\ Q.EXISTS_TAC `(r4,Dot (Sym "nil") (Sym "nil"))::y'''` 1958 \\ SIMP_TAC std_ss [SEP_EXPS_def,lisp_exp_def] 1959 \\ SIMP_TAC std_ss [SEP_CLAUSES] 1960 \\ SIMP_TAC std_ss [SEP_EXISTS] 1961 \\ Q.EXISTS_TAC `3w` 1962 \\ Q.EXISTS_TAC `3w` 1963 \\ ASM_SIMP_TAC std_ss [WORD_SUB_REFL,ALIGNED_n2w,WORD_ADD_SUB,SEP_CLAUSES] 1964 \\ FULL_SIMP_TAC std_ss [GSYM ALIGNED8_def,ALIGNED8_STEP,SEP_CLAUSES] 1965 \\ SEP_WRITE_TAC)) 1966 \\ Cases_on `h = "."` THEN1 1967 (FULL_SIMP_TAC std_ss [arm_tokens3_def,sexp_parse_def,SEP_CLAUSES] 1968 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 1969 \\ SIMP_TAC std_ss [] 1970 \\ Q.PAT_X_ASSUM `arm_token y' ccc b x` MP_TAC 1971 \\ FULL_SIMP_TAC std_ss [arm_token_def] 1972 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 1973 \\ SIMP_TAC std_ss [] 1974 \\ ONCE_REWRITE_TAC [arm_parse_loop_def,arm_parse_loop_pre_def] 1975 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LET_DEF,arm_parse_next_def,arm_parse_next_pre_def] 1976 \\ SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_n2w] 1977 \\ SIMP_TAC std_ss [LET_DEF,arm_parse3_def,arm_parse3_pre_def,ALIGNED_INTRO] 1978 \\ `ALIGNED r7 = isDot exp` by 1979 (Cases_on `exp` 1980 \\ FULL_SIMP_TAC std_ss [lisp_exp_def,SEP_CLAUSES] 1981 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [SEP_EXISTS,cond_STAR,isDot_def] 1982 \\ METIS_TAC [NOT_ALIGNED,ALIGNED_ADDR32,WORD_SUB_ADD]) 1983 \\ SIMP_TAC std_ss [word_arith_lemma1] 1984 \\ REVERSE (Cases_on `isDot exp` \\ ASM_SIMP_TAC std_ss []) 1985 THEN1 1986 (Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ 0x3w) ((r4 =+ 0x3w) f)` 1987 \\ `CAR exp = exp` by 1988 (Cases_on `exp` \\ FULL_SIMP_TAC std_ss [isDot_def,CAR_def]) 1989 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,word_arith_lemma1,STAR_ASSOC] 1990 \\ `(arm_tokens4 (r4 - 8w) xs b d y * arm_tokens3 (r5 + 0x8w) xs q * 1991 lisp_exp exp r7 (b,d) * lisp_exp (sexp_list stack) r8 (b,d) * 1992 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`r7`,`r8`]) 1993 \\ ASM_SIMP_TAC std_ss [ALIGNED8_STEP,ALIGNED_n2w] \\ STRIP_TAC 1994 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 1995 \\ REPEAT (Q.PAT_X_ASSUM `!df. bbb` (STRIP_ASSUME_TAC o SPEC_ALL)) 1996 \\ ASM_SIMP_TAC std_ss [] \\ ALIGNED_TAC \\ SEP_READ_TAC) 1997 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC) 1998 \\ Q.UNABBREV_TAC `f2` 1999 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,SEP_FILL_def,SEP_CLAUSES] 2000 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 2001 \\ Q.EXISTS_TAC `(r4,Dot (Sym "nil") (Sym "nil"))::y'''` 2002 \\ SIMP_TAC std_ss [SEP_EXPS_def,lisp_exp_def] 2003 \\ SIMP_TAC std_ss [SEP_CLAUSES] 2004 \\ SIMP_TAC std_ss [SEP_EXISTS] 2005 \\ REPEAT (Q.EXISTS_TAC `3w`) 2006 \\ ASM_SIMP_TAC std_ss [WORD_SUB_REFL,ALIGNED_n2w,WORD_ADD_SUB,SEP_CLAUSES] 2007 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] 2008 \\ ASM_SIMP_TAC std_ss [WORD_ADD_0,SEP_CLAUSES,STAR_ASSOC,word_arith_lemma1] 2009 \\ FULL_SIMP_TAC std_ss [GSYM ALIGNED8_def,ALIGNED8_STEP,SEP_CLAUSES] 2010 \\ SEP_WRITE_TAC) 2011 THEN 2012 (FULL_SIMP_TAC std_ss [isDot_thm,CAR_def] 2013 \\ Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ 0x3w) ((r4 =+ 0x3w) ((r7 =+ 3w) f))` 2014 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,word_arith_lemma1,STAR_ASSOC] 2015 \\ FULL_SIMP_TAC std_ss [lisp_exp_def,SEP_CLAUSES] 2016 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 2017 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] 2018 \\ `f r7 = y'''` by SEP_READ_TAC 2019 \\ FULL_SIMP_TAC std_ss [] 2020 \\ `(ALIGNED y''' ==> ALIGNED8 (b - y'''))` by 2021 (STRIP_TAC \\ REVERSE (Cases_on `a`) 2022 \\ FULL_SIMP_TAC std_ss [lisp_exp_def,SEP_CLAUSES,sexp_list_def] 2023 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [GSYM ALIGNED8_def, 2024 cond_STAR,SEP_EXISTS] 2025 THEN1 (IMP_RES_TAC NOT_ALIGNED \\ METIS_TAC [WORD_SUB_ADD]) 2026 \\ POP_ASSUM MP_TAC 2027 \\ ASM_SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_ADDR32,ALIGNED_n2w]) 2028 \\ `(arm_tokens4 (r4 - 8w) xs b d y * arm_tokens3 (r5 + 0x8w) xs q * 2029 lisp_exp a y''' (b,d) * lisp_exp (sexp_list stack) r8 (b,d) * 2030 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`y'''`,`r8`]) 2031 \\ ASM_SIMP_TAC std_ss [ALIGNED8_STEP,ALIGNED_n2w] \\ STRIP_TAC 2032 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 2033 \\ REPEAT (Q.PAT_X_ASSUM `!df. bbb` (STRIP_ASSUME_TAC o SPEC_ALL)) 2034 \\ ASM_SIMP_TAC std_ss [] \\ ALIGNED_TAC \\ SEP_READ_TAC) 2035 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC) 2036 \\ Q.UNABBREV_TAC `f2` 2037 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,SEP_CLAUSES,SEP_FILL_def] 2038 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 2039 \\ Q.EXISTS_TAC `(r4,Dot (Sym "nil") (Sym "nil"))::(r7,Dot (Sym "nil") b')::y'''''` 2040 \\ SIMP_TAC std_ss [SEP_EXPS_def,lisp_exp_def] 2041 \\ SIMP_TAC std_ss [SEP_CLAUSES] 2042 \\ SIMP_TAC std_ss [SEP_EXISTS] 2043 \\ Q.EXISTS_TAC `3w` 2044 \\ Q.EXISTS_TAC `3w` 2045 \\ Q.EXISTS_TAC `3w` 2046 \\ Q.EXISTS_TAC `y''''` 2047 \\ ASM_SIMP_TAC std_ss [WORD_SUB_REFL,ALIGNED_n2w,WORD_ADD_SUB,SEP_CLAUSES] 2048 \\ ASM_SIMP_TAC std_ss [STAR_ASSOC] 2049 \\ Q.PAT_X_ASSUM `ALIGNED8 (b - r7)` ASSUME_TAC 2050 \\ FULL_SIMP_TAC std_ss [GSYM ALIGNED8_def,ALIGNED8_STEP,SEP_CLAUSES] 2051 \\ SEP_WRITE_TAC)) 2052 \\ Cases_on `is_number_string h` THEN1 2053 (FULL_SIMP_TAC std_ss [arm_tokens3_def,sexp_parse_def,SEP_CLAUSES] 2054 \\ Q.PAT_X_ASSUM `arm_token y' ccc b x` MP_TAC 2055 \\ FULL_SIMP_TAC std_ss [arm_token_def,GSYM is_number_string_def] 2056 \\ ONCE_REWRITE_TAC [arm_parse_loop_def,arm_parse_loop_pre_def] 2057 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LET_DEF,arm_parse_next_def,arm_parse_next_pre_def] 2058 \\ SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_n2w] 2059 \\ `~ALIGNED (ADDR32 (n2w (str2num h)) + 0x2w)` by 2060 METIS_TAC [NOT_ALIGNED,ALIGNED_ADDR32] 2061 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 2062 \\ `ADDR32 (n2w (str2num h)) + 0x2w <> 0x28w` by 2063 METIS_TAC [EVAL ``ALIGNED 0x28w``] 2064 \\ ASM_SIMP_TAC std_ss [] 2065 \\ Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ r7) f` 2066 \\ STRIP_TAC 2067 \\ `(arm_tokens4 (r4 - 8w) xs b d y * arm_tokens3 (r5 + 0x8w) xs q * 2068 lisp_exp (Dot (Val (str2num h)) exp) r4 (b,d) * 2069 lisp_exp (sexp_list stack) r8 (b,d) * 2070 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`r4`,`r8`]) 2071 \\ ASM_SIMP_TAC std_ss [ALIGNED8_STEP,ALIGNED_n2w] \\ STRIP_TAC 2072 \\ RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `!xx yy. zz` (K ALL_TAC)) 2073 \\ REPEAT (Q.PAT_X_ASSUM `!df. bbb` (STRIP_ASSUME_TAC o SPEC_ALL)) 2074 \\ ASM_SIMP_TAC std_ss [] \\ ALIGNED_TAC \\ SEP_READ_TAC) 2075 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC) 2076 \\ Q.UNABBREV_TAC `f2` 2077 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,SEP_CLAUSES,lisp_exp_def] 2078 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 2079 \\ Q.EXISTS_TAC `y'` 2080 \\ Q.EXISTS_TAC `r7` 2081 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES,STAR_ASSOC] 2082 \\ FULL_SIMP_TAC std_ss [GSYM ALIGNED8_def,ALIGNED8_STEP,SEP_CLAUSES] 2083 \\ SEP_WRITE_TAC) 2084 THEN 2085 (FULL_SIMP_TAC std_ss [arm_tokens3_def,sexp_parse_def,SEP_CLAUSES] 2086 \\ Q.PAT_X_ASSUM `arm_token y' ccc b x` MP_TAC 2087 \\ FULL_SIMP_TAC std_ss [arm_token_def,GSYM is_number_string_def] 2088 \\ ONCE_REWRITE_TAC [arm_parse_loop_pre_def,arm_parse_loop_def] 2089 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LET_DEF,arm_parse_next_def,arm_parse_next_pre_def] 2090 \\ SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_n2w] 2091 \\ STRIP_TAC 2092 \\ `~ALIGNED y'` by METIS_TAC [WORD_SUB_ADD,NOT_ALIGNED] 2093 \\ `y' <> 0x28w` by METIS_TAC [EVAL ``ALIGNED 0x28w``] 2094 \\ ASM_SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO] 2095 \\ Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ r7) f` 2096 \\ `(arm_tokens4 (r4 - 8w) xs b d y * arm_tokens3 (r5 + 0x8w) xs q * 2097 lisp_exp (Dot (Sym h) exp) r4 (b,d) * 2098 lisp_exp (sexp_list stack) r8 (b,d) * 2099 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`r4`,`r8`]) 2100 \\ ASM_SIMP_TAC std_ss [ALIGNED8_STEP,ALIGNED_n2w] \\ STRIP_TAC 2101 \\ RES_TAC 2102 \\ REPEAT (Q.PAT_X_ASSUM `!df. bbb` (STRIP_ASSUME_TAC o SPEC_ALL)) 2103 \\ ASM_SIMP_TAC std_ss [] 2104 \\ ONCE_REWRITE_TAC [ALIGNED_MOD_4] 2105 \\ ASM_SIMP_TAC std_ss [WORD_ADD_0] 2106 \\ SEP_READ_TAC) 2107 \\ Q.PAT_X_ASSUM `!r4 r5. bb` (K ALL_TAC) 2108 \\ Q.UNABBREV_TAC `f2` 2109 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,SEP_CLAUSES,lisp_exp_def] 2110 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 2111 \\ Q.EXISTS_TAC `y'` 2112 \\ Q.EXISTS_TAC `r7` 2113 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES,STAR_ASSOC] 2114 \\ FULL_SIMP_TAC std_ss [GSYM ALIGNED8_def,ALIGNED8_STEP,SEP_CLAUSES] 2115 \\ SEP_WRITE_TAC)); 2116 2117val arm_parse_string2sexp_lemma = let 2118 val th = Q.SPECL [`REVERSE (sexp_lex s)`,`r4`,`r5`,`3w`,`3w`,`df`,`f`,`d1`,`d2`,`d3`,`Sym "nil"`,`[]`] arm_parse_lemma 2119 val th = RW [lisp_exp_def,GSYM AND_IMP_INTRO,WORD_SUB_REFL,WORD_ADD_SUB,sexp_list_def] th 2120 val th = SIMP_RULE (std_ss++sep_cond_ss) [cond_STAR,ALIGNED_n2w] th 2121 val th = RW1 [CONJ_COMM] th 2122 val th = RW [AND_IMP_INTRO,GSYM CONJ_ASSOC,GSYM string2sexp_def] th 2123 in th end 2124 2125val SUB_n2w_LO = prove( 2126 ``!w:'a word k. 0 < k /\ k <= w2n w ==> w - n2w k <+ w``, 2127 Cases \\ ASM_SIMP_TAC std_ss [w2n_n2w,word_arith_lemma2] 2128 \\ REPEAT STRIP_TAC 2129 \\ `~(n < k) /\ n - k < dimword (:'a)` by DECIDE_TAC 2130 \\ ASM_SIMP_TAC std_ss [WORD_LO,w2n_n2w] \\ DECIDE_TAC); 2131 2132val (th,arm_parse8_def,arm_parse8_pre_def) = compilerLib.compile_all `` 2133 arm_parse8 (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) = 2134 let r4 = w2w (f r5) in 2135 let (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) = 2136 arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) in 2137 let r4 = r9 - 8w in 2138 let r6 = h r4 in 2139 let r5 = r4 in 2140 let r7 = 3w:word32 in 2141 let r8 = 3w:word32 in 2142 let (r4,r5,r6,r7,r8,dh,h) = arm_parse_loop1 (r4,r5,r6,r7,r8,dh,h) in 2143 (r9,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m)``; 2144 2145val all_symbols_exists = prove( 2146 ``!ys xs. ?zs. all_symbols ys xs = xs ++ zs``, 2147 Induct THEN1 (REWRITE_TAC [all_symbols_def] \\ METIS_TAC [APPEND_NIL]) 2148 \\ REPEAT STRIP_TAC 2149 \\ ASM_SIMP_TAC std_ss [all_symbols_def] 2150 \\ Cases_on `identifier_string h` \\ ASM_SIMP_TAC std_ss [] 2151 \\ POP_ASSUM (K ALL_TAC) 2152 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `add_symbol h xs`) 2153 \\ ASM_REWRITE_TAC [] 2154 \\ POP_ASSUM (K ALL_TAC) 2155 \\ Induct_on `xs` 2156 \\ SIMP_TAC std_ss [add_symbol_def,APPEND] 2157 \\ REPEAT STRIP_TAC 2158 \\ Cases_on `h = h'` \\ FULL_SIMP_TAC std_ss [APPEND] 2159 \\ METIS_TAC []); 2160 2161val sexp_lex_space_def = Define ` 2162 sexp_lex_space s = LENGTH (sexp_lex s ++ FILTER (\x. x = "'") (sexp_lex s))`; 2163 2164val token_slots_FILTER = prove( 2165 ``!xs a n. 2166 token_slots a (LENGTH (FILTER (\x. x = "'") xs) + n) = 2167 arm_tokens3 (a + n2w (8 * n)) xs 2168 (a + n2w (8 * (LENGTH (FILTER (\x. x = "'") xs) + n))) * 2169 token_slots a n``, 2170 Induct_on `n` THEN1 2171 (SIMP_TAC std_ss [ADD_CLAUSES,WORD_ADD_0,token_slots_def,SEP_CLAUSES] 2172 \\ Induct \\ SIMP_TAC std_ss [arm_tokens3_def,LENGTH,FILTER,token_slots_def, 2173 WORD_ADD_0,SEP_CLAUSES] 2174 \\ REPEAT STRIP_TAC \\ Cases_on `h = "'"` \\ASM_SIMP_TAC std_ss [] 2175 \\ ASM_SIMP_TAC std_ss [token_slots_def,LENGTH,ADD] 2176 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w,MULT_CLAUSES]) 2177 \\ ASM_SIMP_TAC std_ss [ADD_CLAUSES,token_slots_def,SEP_CLAUSES] 2178 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w,MULT_CLAUSES] 2179 \\ SIMP_TAC std_ss [SEP_EXISTS,STAR_ASSOC,FUN_EQ_THM] 2180 \\ SIMP_TAC (std_ss++star_ss) []); 2181 2182val token_slots_sexp_lex_space = prove( 2183 ``token_slots r9 (sexp_lex_space s) = 2184 arm_tokens3 (r9 + n2w (8 * LENGTH (sexp_lex s))) (REVERSE (sexp_lex s)) 2185 (r9 + n2w (8 * sexp_lex_space s)) * 2186 token_slots r9 (LENGTH (sexp_lex s))``, 2187 REWRITE_TAC [sexp_lex_space_def,LENGTH_APPEND] 2188 \\ ONCE_REWRITE_TAC [ADD_COMM] 2189 \\ REWRITE_TAC [RW [rich_listTheory.FILTER_REVERSE,rich_listTheory.LENGTH_REVERSE] 2190 (Q.SPEC `REVERSE xs` token_slots_FILTER)]); 2191 2192val ALIGNED8_IMP = prove( 2193 ``!a. ALIGNED8 a ==> ALIGNED a``, 2194 REWRITE_TAC [ALIGNED_THM,ALIGNED8_def] 2195 \\ Cases \\ ASM_SIMP_TAC std_ss [w2n_n2w] 2196 \\ STRIP_TAC 2197 \\ Q.EXISTS_TAC `n2w (n DIV 8 * 2)` 2198 \\ SIMP_TAC std_ss [word_mul_n2w,GSYM MULT_ASSOC] 2199 \\ METIS_TAC [DIVISION,EVAL ``0<8``,ADD_0]); 2200 2201val ALIGNED8_ADD = prove( 2202 ``!a:word32 n. ALIGNED8 (a + n2w (8 * n)) = ALIGNED8 a``, 2203 Cases \\ REWRITE_TAC [ALIGNED8_def,word_add_n2w] 2204 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w] 2205 \\ REWRITE_TAC [GSYM (EVAL ``8 * 536870912``)] 2206 \\ SIMP_TAC bool_ss [MOD_MULT_MOD,DECIDE ``0<8:num /\ 0<536870912:num``] 2207 \\ ONCE_REWRITE_TAC [ADD_COMM] 2208 \\ ONCE_REWRITE_TAC [MULT_COMM] 2209 \\ SIMP_TAC std_ss [MOD_TIMES,DECIDE ``0<8:num``]); 2210 2211val ALIGNED8_SUB = 2212 (GSYM o RW [WORD_SUB_ADD] o Q.SPECL [`a - n2w (8 * n)`,`n`]) ALIGNED8_ADD; 2213 2214val arm_parse6_lemma = (GEN_ALL o SIMP_RULE std_ss [WORD_ADD_SUB,ALIGNED8_STEP] o Q.SPEC `r9+8w` o prove)( 2215 ``!r9 r8 r7 r6 r5 r3 y x s p m h g f dm dh dg df d b. 2216 string_mem (STRCAT s null_string) (r5,f,df) /\ 2217 EVERY (\c. ORD c <> 0) (EXPLODE s) /\ 2218 ALIGNED r9 /\ ALIGNED8 (r3 - r9) /\ 2219 symbol_table builtin_symbols x (r3,dm,m,dg,g) /\ 2220 (p * arm_tokens4 (r9 - 8w) [] b d y * 2221 token_slots r9 (sexp_lex_space s)) (fun2set (h,dh)) /\ 2222 symbol_table_dom (all_symbols (sexp_lex s) builtin_symbols) (r3,dm,dg) ==> 2223 ?r9i r4i r5i r6i r7i r8i gi hi mi xi. 2224 arm_parse8_pre (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) /\ 2225 (arm_parse8 (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) = 2226 (r4i,r9 - 8w,r5i,r6i,r7i,r8i,df,dg,dh,dm,f,gi,hi,mi)) /\ 2227 (arm_tokens4 (r9 - 8w) [] r3 xi (r9 - 8w) * 2228 lisp_exp (string2sexp s) r7i (r3,xi) * 2229 SEP_FILL (r3,xi) * p) (fun2set (hi,dh)) /\ 2230 (r5i = (r9 - 8w) + n2w (8 * sexp_lex_space s)) /\ 2231 symbol_table (all_symbols (sexp_lex s) builtin_symbols) xi 2232 (r3,dm,mi,dg,gi)``, 2233 REWRITE_TAC [token_slots_sexp_lex_space,STAR_ASSOC] 2234 \\ REPEAT STRIP_TAC 2235 \\ IMP_RES_TAC (REWRITE_RULE [arm_tokens_EQ_arm_tokens2] arm_lexer_lemma) 2236 \\ SIMP_TAC std_ss [LET_DEF,arm_parse8_def,arm_parse8_pre_def] 2237 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`r8`,`r7`,`r6`]) 2238 \\ ASM_SIMP_TAC std_ss [] 2239 \\ `ALIGNED r1i /\ ALIGNED r3 /\ ALIGNED8 (r3 - r1i)` by 2240 (Q.PAT_X_ASSUM `r9 + bbb = r1i` (MP_TAC o GSYM) 2241 \\ SIMP_TAC std_ss [] \\ STRIP_TAC 2242 \\ REPEAT STRIP_TAC THENL [ 2243 MATCH_MP_TAC ALIGNED_ADD 2244 \\ ASM_SIMP_TAC bool_ss [ALIGNED_n2w,GSYM (EVAL ``4*2``)] 2245 \\ REWRITE_TAC [GSYM MULT_ASSOC] 2246 \\ SIMP_TAC std_ss [RW1 [MULT_COMM] MOD_EQ_0], 2247 IMP_RES_TAC ALIGNED8_IMP 2248 \\ POP_ASSUM MP_TAC 2249 \\ SIMP_TAC std_ss [word_sub_def] 2250 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 2251 \\ ASM_SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_NEG], 2252 ASM_SIMP_TAC std_ss [WORD_SUB_PLUS,ALIGNED8_SUB]]) 2253 \\ `ALIGNED (r1i - 8w)` by ALIGNED_TAC 2254 \\ FULL_SIMP_TAC std_ss [] 2255 \\ `(arm_tokens4 (r1i - 0x8w) (REVERSE (sexp_lex s)) r3 xi (r9 - 8w) * 2256 arm_tokens3 r1i (REVERSE (sexp_lex s)) (r9 + n2w (8 * sexp_lex_space s)) * SEP_FILL (r3,xi) * p) 2257 (fun2set (hi,dh))` by 2258 (FULL_SIMP_TAC std_ss [SEP_FILL_def,SEP_CLAUSES] 2259 \\ SIMP_TAC std_ss [SEP_EXISTS] 2260 \\ Q.EXISTS_TAC `[]` 2261 \\ SIMP_TAC std_ss [SEP_EXPS_def,SEP_CLAUSES] 2262 \\ FULL_SIMP_TAC std_ss [arm_tokens4_def,SEP_CLAUSES] 2263 \\ FULL_SIMP_TAC std_ss [arm_tokens2_def,SEP_EXISTS] 2264 \\ Q.EXISTS_TAC `y''` 2265 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 2266 \\ Q.PAT_X_ASSUM `r9 - 8w = y` (ASSUME_TAC o GSYM) 2267 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 2268 \\ `(r3, "nil") IN xi /\ (r3 + 0x18w, "quote") IN xi` by 2269 (STRIP_ASSUME_TAC (Q.SPECL [`sexp_lex s`,`builtin_symbols`] all_symbols_exists) 2270 \\ FULL_SIMP_TAC std_ss [] 2271 \\ Q.PAT_X_ASSUM `symbol_table (builtin_symbols ++ zs) xi (r3,dm,mi,dg,gi)` MP_TAC 2272 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 2273 \\ REWRITE_TAC [builtin_symbols_def,APPEND] 2274 \\ NTAC 3 (ONCE_REWRITE_TAC [symbol_table_def]) 2275 \\ ASM_SIMP_TAC std_ss [LET_DEF,LENGTH,IN_DELETE,word_arith_lemma1]) 2276 \\ `ALIGNED8 (r3 - (r1i - 8w))` by ASM_SIMP_TAC std_ss [ALIGNED8_STEP] 2277 \\ (IMP_RES_TAC o RW [WORD_SUB_ADD,GSYM AND_IMP_INTRO] o Q.SPEC `p`) 2278 (MATCH_INST (MATCH_INST arm_parse_string2sexp_lemma ``arm_parse_loop1 2279 (r1i - 0x8w,r1i - 0x8w,hi (r1i - 0x8w),0x3w,0x3w,dh,hi)``) 2280 ``SEP_FILL (r3,xi)``) 2281 \\ ASM_SIMP_TAC std_ss [] 2282 \\ Q.EXISTS_TAC `xi` 2283 \\ IMP_RES_TAC string_mem_IMP_IN 2284 \\ ASM_SIMP_TAC std_ss [] 2285 \\ ALIGNED_TAC 2286 \\ SIMP_TAC std_ss [word_sub_def,AC WORD_ADD_ASSOC WORD_ADD_COMM]); 2287 2288 2289 2290 2291(* SETTING UP THE INITIAL SYMBOL TABLE *) 2292 2293fun append_lists [] = [] 2294 | append_lists (x::xs) = x @ append_lists xs 2295 2296fun N_CONV 0 c = ALL_CONV 2297 | N_CONV n c = N_CONV (n-1) c THENC c 2298 2299val symbol_table_th = 2300 (ONCE_REWRITE_CONV [builtin_symbols_def] THENC 2301 N_CONV 20 (ONCE_REWRITE_CONV [symbol_table_def]) THENC 2302 SIMP_CONV std_ss [LET_DEF,string_mem_def,LENGTH] THENC 2303 EVAL_ANY_MATCH_CONV [``n2w (ORD c):word8``] THENC 2304 SIMP_CONV std_ss [word_arith_lemma1,NOT_CONS_NIL,IN_DELETE] THENC 2305 SIMP_CONV (std_ss++SIZES_ss) [WORD_EQ_ADD_CANCEL,n2w_11] THENC 2306 REWRITE_CONV [GSYM CONJ_ASSOC]) 2307 ``symbol_table builtin_symbols x (r3,dm,m,dg,g)`` 2308 2309val symbol_table_dom_th = 2310 (ONCE_REWRITE_CONV [builtin_symbols_def] THENC 2311 N_CONV 20 (ONCE_REWRITE_CONV [symbol_table_dom_def]) THENC 2312 SIMP_CONV std_ss [LET_DEF,string_mem_def,LENGTH] THENC 2313 EVAL_ANY_MATCH_CONV [``n2w (ORD c):word8``] THENC 2314 SIMP_CONV std_ss [word_arith_lemma1,NOT_CONS_NIL,IN_DELETE] THENC 2315 SIMP_CONV (std_ss++SIZES_ss) [WORD_EQ_ADD_CANCEL,n2w_11] THENC 2316 REWRITE_CONV [GSYM CONJ_ASSOC] THENC 2317 REWRITE_CONV [string_mem_dom_def] THENC 2318 SIMP_CONV std_ss [word_arith_lemma1,INSERT_SUBSET,EMPTY_SUBSET] THENC 2319 REWRITE_CONV [GSYM CONJ_ASSOC] THENC 2320 SIMP_CONV std_ss [GSYM ADD_ASSOC]) 2321 ``symbol_table_dom builtin_symbols (r3,dm,dg)`` 2322 2323val symbol_table_tm = let 2324 fun all_distinct [] = [] 2325 | all_distinct (x::xs) = x :: all_distinct (filter (fn y => not (x = y)) xs) 2326 val tms = find_terms (can (match_term ``(g:word32->word8) (r3 + n2w m) = n2w n``)) (concl symbol_table_th) 2327 val mooch = Arbnum.toInt o numSyntax.dest_numeral o cdr o cdr 2328 val ys = sort (fn x => fn y => x <= y) (all_distinct (map mooch tms)) 2329 val zs = map (fn x => (x, filter (fn tm => mooch tm = x) tms)) ys 2330 val tt = (car o car) ``(x:word32 =+ y:word8)`` 2331 val ww = mk_comb(``w2w:word32->word8``,mk_var("r6",``:word32``)) 2332 fun cuscus (x,ws) = let 2333 val v = mk_comb(``n2w:num->word32``,numSyntax.mk_numeral(Arbnum.fromInt x)) 2334 val v = (mk_var("r6",``:word32``),v) 2335 fun hipochus tm = let 2336 val (x,y) = dest_eq tm 2337 in (car x, mk_comb(mk_comb(mk_comb(tt,cdr x),ww),car x)) end 2338 in v :: map hipochus ws end 2339 val ts = append_lists (map cuscus zs) 2340 val tms = find_terms (can (match_term ``(m:word32->word32) (r3) = w``)) (concl symbol_table_th) 2341 val tt = (car o car) ``(x:word32 =+ y:word32)`` 2342 val ww = mk_var("r6",``:word32``) 2343 fun cuscus tm = let 2344 val (x,y) = dest_eq tm 2345 in [(ww, y), 2346 (car x, mk_comb(mk_comb(mk_comb(tt,cdr x),ww),car x))] end 2347 val ts2 = append_lists (map cuscus tms) 2348 val ll = pairSyntax.list_mk_pair[mk_var("r3",``:word32``), 2349 mk_var("r6",``:word32``), 2350 mk_var("dg",``:word32 set``), 2351 mk_var("g",``:word32->word8``)] 2352 fun take_drop n [] = ([],[]) 2353 | take_drop n (x::xs) = if n = 0 then ([],x::xs) else let 2354 val (ys,zs) = take_drop (n-1) xs 2355 in (x::ys,zs) end 2356 fun split [] = [] 2357 | split (x::xs) = let 2358 val (ys,zs) = take_drop 8 (x::xs) 2359 in ys :: split zs end 2360 val tts = split ts 2361 val i = ref 0 2362 val ss = hd tts 2363 val ty = type_of (mk_abs(mk_var("fgh",type_of ll),ll)) 2364 fun mk_func ss = let 2365 val tm3 = foldr (fn ((x,y),tm) => pairSyntax.mk_anylet([(x,y)],tm)) ll ss 2366 val _ = (i := !i + 1) 2367 val def = mk_eq(mk_comb(mk_var("arm_setup" ^ int_to_string (!i),ty),ll),tm3) 2368 in def end 2369 val defs = map mk_func tts 2370 val gh = map (fn tm => (ll, cdr (car tm))) defs 2371 val ls = (defs @ [mk_func gh]) 2372 val ll2 = pairSyntax.list_mk_pair[mk_var("r3",``:word32``), 2373 mk_var("r6",``:word32``), 2374 mk_var("dm",``:word32 set``), 2375 mk_var("m",``:word32->word32``)] 2376 val tts = split ts2 2377 val ss = hd tts 2378 val ty = type_of (mk_abs(mk_var("fgh",type_of ll2),ll2)) 2379 fun mk_func2 ss = let 2380 val tm3 = foldr (fn ((x,y),tm) => pairSyntax.mk_anylet([(x,y)],tm)) ll2 ss 2381 val _ = (i := !i + 1) 2382 val def = mk_eq(mk_comb(mk_var("arm_setup" ^ int_to_string (!i),ty),ll2),tm3) 2383 in def end 2384 val defs = map mk_func2 tts 2385 val gh = map (fn tm => (ll2, cdr (car tm))) defs 2386 val ls2 = (defs @ [mk_func2 gh]) 2387 val ll3 = pairSyntax.list_mk_pair[mk_var("r3",``:word32``), 2388 mk_var("r6",``:word32``), 2389 mk_var("dm",``:word32 set``), 2390 mk_var("dg",``:word32 set``), 2391 mk_var("m",``:word32->word32``), 2392 mk_var("g",``:word32->word8``)] 2393 val ty = type_of (mk_abs(mk_var("fgh",type_of ll3),ll3)) 2394 fun mk_func3 ss = let 2395 val tm3 = foldr (fn ((x,y),tm) => pairSyntax.mk_anylet([(x,y)],tm)) ll3 ss 2396 val _ = (i := !i + 1) 2397 val def = mk_eq(mk_comb(mk_var("arm_setup",ty),ll3),tm3) 2398 in def end 2399 val def = mk_func3 [(ll,(fst o dest_eq o last) ls), (ll2,(fst o dest_eq o last) ls2)] 2400 val tm = list_mk_conj (ls @ ls2 @ [def]) 2401 in tm end; 2402 2403val (_,arm_setup_def,arm_setup_pre_def) = compilerLib.compile_all symbol_table_tm; 2404 2405val arm_setup_lemma = prove( 2406 ``!r3 dg dm g m. 2407 symbol_table_dom builtin_symbols (r3,dm,dg) ==> 2408 arm_setup_pre (r3,r6,dm,dg,m,g) /\ 2409 ?gi mi r6i. 2410 (arm_setup (r3,r6,dm,dg,m,g) = (r3,r6i,dm,dg,mi,gi)) /\ 2411 symbol_table builtin_symbols (builtin_symbols_set r3) (r3,dm,mi,dg,gi)``, 2412 SIMP_TAC std_ss [arm_setup_def,LET_DEF] 2413 THEN CONV_TAC (EVAL_ANY_MATCH_CONV [``w2w (n2w n)``]) 2414 THEN REWRITE_TAC [symbol_table_th] 2415 THEN SIMP_TAC (std_ss++SIZES_ss) [WORD_EQ_ADD_CANCEL,n2w_11,APPLY_UPDATE_THM] 2416 THEN SIMP_TAC std_ss [builtin_symbols_set_def,EXTENSION,IN_INSERT,IN_DELETE,NOT_IN_EMPTY] 2417 THEN REWRITE_TAC [CONJ_ASSOC] 2418 THEN REVERSE (STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC) 2419 THEN1 METIS_TAC [] THEN REWRITE_TAC [GSYM CONJ_ASSOC] 2420 THEN POP_ASSUM MP_TAC 2421 THEN SIMP_TAC std_ss [symbol_table_dom_th,INSERT_SUBSET,EMPTY_SUBSET] 2422 THEN SIMP_TAC std_ss [arm_setup_def,arm_setup_pre_def,LET_DEF] 2423 THEN SIMP_TAC std_ss [ALIGNED_INTRO,GSYM CONJ_ASSOC] 2424 THEN ONCE_REWRITE_TAC [ALIGNED_MOD_4] 2425 THEN SIMP_TAC std_ss [] THEN SIMP_TAC std_ss [WORD_ADD_0]) 2426 2427 2428(* SETTING UP lisp_inv *) 2429 2430val (arm_string2sexp_thms,arm_string2sexp_def,arm_string2sexp_pre_def) = compile_all `` 2431 arm_string2sexp' (r3,r4,r5,df,dg,dh,dm,f,g,h,m) = 2432 let r9 = r5 in 2433 let r8 = r4 << 3 in 2434 let r7 = r8 + r8 in 2435 let h = (r9 - 0x20w =+ r8) h in 2436 let r5 = r3 in 2437 let r3 = r9 + r7 in 2438 let r9 = r9 + 8w in 2439 let r3 = r3 + 24w in 2440 let r6 = 40w in 2441 let (r3,r6,dm,dg,m,g) = arm_setup (r3,r6,dm,dg,m,g) in 2442 let r6 = 40w in 2443 let h = (r9 - 8w =+ r6) h in 2444 let (r9,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) = 2445 arm_parse8 (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) in 2446 let r9 = r4 in 2447 let r8 = 1w in 2448 let r6 = h (r9 - 0x20w) in 2449 let h = (r9 - 0x1Cw =+ r8) h in 2450 let r8 = r9 + r6 in 2451 let r8 = r8 + 8w in 2452 let h = (r9 + 4w =+ r8) h in 2453 let r5 = r5 + 8w in 2454 let r3 = r7 in 2455 let h = (r9 =+ r5) h in 2456 let r4 = 3w:word32 in 2457 let r5 = 3w:word32 in 2458 let r6 = 3w:word32 in 2459 let r7 = 3w:word32 in 2460 let r8 = 3w:word32 in 2461 (r3,r4,r5,r6,r7,r8,r9,df,dg,dh,dm,f,g,h,m)``; 2462 2463val symbol_table_dom_APPEND = prove( 2464 ``!xs ys a dm dg. 2465 symbol_table_dom (xs++ys) (a,dm,dg) ==> 2466 symbol_table_dom xs (a,dm,dg)``, 2467 REVERSE Induct 2468 THEN1 (SIMP_TAC std_ss [symbol_table_dom_def,APPEND] \\ METIS_TAC []) 2469 \\ REWRITE_TAC [symbol_table_dom_def,APPEND] 2470 \\ Cases THEN1 REWRITE_TAC [symbol_table_dom_def,APPEND] 2471 \\ REPEAT STRIP_TAC THEN1 METIS_TAC [symbol_table_dom_ALIGNED] 2472 \\ FULL_SIMP_TAC std_ss [symbol_table_dom_def,INSERT_SUBSET]) ; 2473 2474val sexp2string_NOT_NULL = prove( 2475 ``!s. sexp_ok s ==> EVERY (\c. ORD c <> 0) (EXPLODE (sexp2string s))``, 2476 REWRITE_TAC [sexp2string_def] \\ Q.SPEC_TAC (`T`,`b`) 2477 \\ completeInduct_on `LSIZE s` 2478 \\ REVERSE (STRIP_TAC \\ STRIP_ASSUME_TAC (Q.SPEC `s` SExp_expand)) 2479 \\ ASM_SIMP_TAC std_ss [] 2480 THEN1 2481 (FULL_SIMP_TAC std_ss [sexp_ok_def,sexp2string_aux_def,identifier_string_def] 2482 \\ FULL_SIMP_TAC std_ss [EVERY_MEM] \\ REPEAT STRIP_TAC \\ RES_TAC 2483 \\ FULL_SIMP_TAC std_ss [identifier_char_def,space_char_def] 2484 \\ DECIDE_TAC) 2485 THEN1 2486 (SIMP_TAC std_ss [sexp_ok_def,sexp2string_aux_def,identifier_string_def] 2487 \\ REPEAT STRIP_TAC \\ MP_TAC (Q.SPEC `n` str2num_num2str) 2488 \\ SIMP_TAC std_ss [EVERY_MEM] \\ REPEAT STRIP_TAC \\ RES_TAC 2489 \\ DECIDE_TAC) 2490 \\ SIMP_TAC std_ss [sexp_ok_def,sexp2string_aux_def] 2491 \\ REPEAT STRIP_TAC 2492 \\ Q.ABBREV_TAC `a1 = exp1` 2493 \\ Q.ABBREV_TAC `a2 = exp2` 2494 \\ `ORD #"(" <> 0 /\ ORD #")" <> 0 /\ ORD #"." <> 0 /\ ORD #" " <> 0 /\ ORD #"'" <> 0` by EVAL_TAC 2495 \\ Cases_on `isQuote (Dot a1 a2) /\ b` \\ ASM_SIMP_TAC std_ss [] THEN1 2496 (FULL_SIMP_TAC std_ss [isQuote_thm,SExp_11,CAR_def,LSIZE_def,sexp_ok_def] 2497 \\ REWRITE_TAC [LIST_STRCAT_def,EXPLODE_STRCAT,EVERY_APPEND] 2498 \\ ASM_SIMP_TAC std_ss [EXPLODE_def,EVERY_DEF] 2499 \\ FULL_SIMP_TAC std_ss [isQuote_thm,SExp_11,CAR_def,LSIZE_def,sexp_ok_def] 2500 \\ `LSIZE y < SUC (SUC (LSIZE y))` by DECIDE_TAC \\ METIS_TAC []) 2501 \\ POP_ASSUM (K ALL_TAC) 2502 \\ FULL_SIMP_TAC std_ss [LSIZE_def] 2503 \\ `LSIZE a1 < v` by DECIDE_TAC 2504 \\ `LSIZE a2 < v` by DECIDE_TAC 2505 \\ Cases_on `b` THEN 2506 (SIMP_TAC std_ss [LET_DEF] 2507 \\ REWRITE_TAC [LIST_STRCAT_def,EXPLODE_STRCAT,EVERY_APPEND] 2508 \\ ASM_SIMP_TAC std_ss [EXPLODE_def,EVERY_DEF] 2509 \\ FULL_SIMP_TAC std_ss [isQuote_thm,SExp_11,CAR_def,LSIZE_def,sexp_ok_def] 2510 \\ Cases_on `a2 = Sym "nil"` \\ ASM_SIMP_TAC std_ss [] THEN1 2511 (REWRITE_TAC [LIST_STRCAT_def,EXPLODE_STRCAT,EVERY_APPEND] 2512 \\ ASM_SIMP_TAC std_ss [EXPLODE_def,EVERY_DEF] 2513 \\ FULL_SIMP_TAC std_ss [isQuote_thm,SExp_11,CAR_def,LSIZE_def,sexp_ok_def]) 2514 \\ Cases_on `isDot a2` 2515 \\ ASM_SIMP_TAC std_ss [] 2516 \\ REWRITE_TAC [LIST_STRCAT_def,EXPLODE_STRCAT,EVERY_APPEND] 2517 \\ ASM_SIMP_TAC std_ss [EXPLODE_def,EVERY_DEF] \\ METIS_TAC [])); 2518 2519val token_slots_IMP = prove( 2520 ``!n a h dh. 2521 token_slots a n (fun2set (h,dh)) ==> 2522 (dh = ch_active_set (a,0,n) UNION ch_active_set (a + 4w,0,n))``, 2523 Induct THEN1 2524 (SIMP_TAC std_ss [token_slots_def,fun2set_def, 2525 ch_active_set_def,emp_def, DECIDE ``i <= j /\ j < i + 0:num = F``] 2526 \\ SIMP_TAC std_ss [GSPECIFICATION,EXTENSION,NOT_IN_EMPTY,IN_UNION]) 2527 \\ ASM_SIMP_TAC std_ss [token_slots_def,SEP_EXISTS,one_STAR,GSYM STAR_ASSOC] 2528 \\ SIMP_TAC std_ss [IN_fun2set,IN_DELETE] 2529 \\ `!a. ch_active_set (a:word32,0,SUC n) = 2530 a INSERT ch_active_set (a + 8w:word32,0,n)` by 2531 (SIMP_TAC std_ss [GSPECIFICATION,EXTENSION,IN_INSERT, 2532 ch_active_set_def,GSYM WORD_ADD_ASSOC, 2533 word_add_n2w,word_mul_n2w,GSYM MULT_CLAUSES] 2534 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THENL [ 2535 Cases_on `j = 0` \\ FULL_SIMP_TAC std_ss [WORD_ADD_0] 2536 \\ DISJ2_TAC \\ Q.EXISTS_TAC `j - 1` 2537 \\ `SUC (j - 1) = j` by DECIDE_TAC 2538 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC, 2539 Q.EXISTS_TAC `0` \\ ASM_SIMP_TAC std_ss [WORD_ADD_0], 2540 Q.EXISTS_TAC `SUC j` \\ ASM_SIMP_TAC std_ss [WORD_ADD_0]]) 2541 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2542 \\ REVERSE (Cases_on `a IN dh /\ a + 4w IN dh`) 2543 THEN1 (FULL_SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_UNION] \\ METIS_TAC []) 2544 \\ FULL_SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL] 2545 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,WORD_EQ_ADD_CANCEL] 2546 \\ FULL_SIMP_TAC std_ss [fun2set_DELETE] \\ RES_TAC 2547 \\ FULL_SIMP_TAC std_ss [EXTENSION,IN_DELETE,IN_UNION,word_arith_lemma1,IN_INSERT] 2548 \\ METIS_TAC []); 2549 2550val token_slots_ADD = prove( 2551 ``!n m a. 2552 token_slots a (n + m) = 2553 token_slots a n * token_slots (a + n2w (8 * n)) m``, 2554 Induct \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES,token_slots_def,WORD_ADD_0, 2555 ADD,MULT_CLAUSES,word_add_n2w,GSYM WORD_ADD_ASSOC,STAR_ASSOC]); 2556 2557val ch_active_set_ADD = prove( 2558 ``!a m n. ch_active_set (a,0,n + m) = 2559 ch_active_set (a,0,n) UNION ch_active_set (a + n2w (8 * n),0,m)``, 2560 SIMP_TAC std_ss [ch_active_set_def,EXTENSION,GSPECIFICATION,IN_UNION] 2561 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_mul_n2w,word_add_n2w] 2562 \\ SIMP_TAC std_ss [GSYM LEFT_ADD_DISTRIB] 2563 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 2564 \\ ASM_SIMP_TAC std_ss [] THENL [ 2565 Cases_on `j < n` THEN1 METIS_TAC [] 2566 \\ `j - n < m /\ (n + (j - n) = j)` by DECIDE_TAC \\ METIS_TAC [], 2567 `j < n + m` by DECIDE_TAC \\ METIS_TAC [], 2568 `n + j < n + m` by DECIDE_TAC \\ METIS_TAC []]); 2569 2570val ch_active_set_4 = prove( 2571 ``!a n. ch_active_set (a,0,n) UNION ch_active_set (a + 0x4w,0,n) = 2572 { a + n2w (4 * i) | i < 2 * n }``, 2573 SIMP_TAC std_ss [ch_active_set_def,EXTENSION,GSPECIFICATION,IN_UNION] 2574 \\ REWRITE_TAC [GSYM WORD_ADD_ASSOC,word_add_n2w,word_mul_n2w] 2575 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 2576 \\ ASM_SIMP_TAC std_ss [] 2577 THEN1 (Q.EXISTS_TAC `2 * j` \\ SIMP_TAC std_ss [MULT_ASSOC] \\ DECIDE_TAC) 2578 THEN1 (Q.EXISTS_TAC `2 * j + 1` 2579 \\ SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB] 2580 \\ SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC] \\ DECIDE_TAC) 2581 \\ STRIP_ASSUME_TAC (RW1 [MULT_COMM] (MATCH_MP (Q.SPEC `i` DA) (DECIDE ``0 < 2:num``))) 2582 \\ ASM_SIMP_TAC std_ss [MULT_ASSOC,LEFT_ADD_DISTRIB] 2583 \\ `(r = 0) \/ (r = 1)` by DECIDE_TAC THENL [ 2584 DISJ1_TAC \\ Q.EXISTS_TAC `q` 2585 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC, 2586 DISJ2_TAC \\ Q.EXISTS_TAC `q` 2587 \\ ASM_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] \\ DECIDE_TAC]); 2588 2589val ALL_DISTINCT_all_symbols = prove( 2590 ``!xs ys. ALL_DISTINCT (all_symbols xs ys) = ALL_DISTINCT ys``, 2591 Induct \\ REPEAT STRIP_TAC 2592 \\ ASM_SIMP_TAC std_ss [all_symbols_def] 2593 \\ Cases_on `identifier_string h` 2594 \\ ASM_SIMP_TAC std_ss [all_symbols_def] 2595 \\ Q.SPEC_TAC (`h`,`h`) \\ REPEAT (POP_ASSUM (K ALL_TAC)) 2596 \\ Induct_on `ys` 2597 \\ SIMP_TAC std_ss [add_symbol_def,ALL_DISTINCT,MEM] 2598 \\ REPEAT STRIP_TAC 2599 \\ Cases_on `h = h'` \\ FULL_SIMP_TAC std_ss [ALL_DISTINCT] 2600 \\ `h <> h' ==> (MEM h (add_symbol h' ys) = MEM h ys)` suffices_by METIS_TAC [] 2601 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 2602 \\ Induct_on `ys` 2603 \\ SIMP_TAC std_ss [MEM,add_symbol_def] \\ METIS_TAC [MEM]); 2604 2605val set_lemma = prove( 2606 ``(v UNION u = s) /\ DISJOINT v u ==> (u = s DIFF v) /\ (v SUBSET s)``, 2607 SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_DIFF,SUBSET_DEF, 2608 DISJOINT_DEF,NOT_IN_EMPTY,IN_INTER] \\ METIS_TAC []); 2609 2610val fun2set_DIFF_IMP = store_thm("fun2set_DIFF_IMP", 2611 ``!p x. (!y. p (fun2set (f,y)) ==> (x = y)) /\ (p * q) (fun2set (f,df)) ==> 2612 q (fun2set (f,df DIFF x))``, 2613 SIMP_TAC std_ss [STAR_def,GSYM fun2set_DIFF] \\ REPEAT STRIP_TAC 2614 \\ FULL_SIMP_TAC std_ss [SPLIT_def] 2615 \\ IMP_RES_TAC set_lemma 2616 \\ IMP_RES_TAC SUBSET_fun2set 2617 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC 2618 \\ FULL_SIMP_TAC std_ss []); 2619 2620val ch_active_set2_def = Define ` 2621 ch_active_set2 (a,i,n) = 2622 ch_active_set (a,i,n) UNION ch_active_set (a + 0x4w,i,n)`; 2623 2624val ALIGNED8_EXISTS = prove( 2625 ``!w:word32. ALIGNED8 w ==> ?k. w = n2w (8 * k)``, 2626 Cases \\ ASM_SIMP_TAC std_ss [ALIGNED8_def,w2n_n2w] 2627 \\ METIS_TAC [DIVISION,EVAL ``0<8``,ADD_0,MULT_COMM]) 2628 2629val ALIGNED8_ADD_EQ = prove( 2630 ``!w:word32 v. ALIGNED8 w ==> (ALIGNED8 (w + v) = ALIGNED8 v) /\ 2631 (ALIGNED8 (w - v) = ALIGNED8 (-v))``, 2632 SIMP_TAC std_ss [word_sub_def] 2633 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 2634 \\ REPEAT STRIP_TAC 2635 \\ IMP_RES_TAC ALIGNED8_EXISTS 2636 \\ ASM_SIMP_TAC std_ss [ALIGNED8_ADD]); 2637 2638val IMP_lisp_x = prove( 2639 ``!s a p. 2640 sexp_ok s /\ ALIGNED8 (sa - r5) /\ 2641 (lisp_exp s a (sa,xi) * p) (fun2set (h,ch_active_set2 (r5 + 8w,0,ll))) ==> 2642 lisp_x s (a,ch_active_set (r5,1,1 + ll),h) (set_add (0x0w - sa) xi)``, 2643 REVERSE Induct THENL [ 2644 SIMP_TAC std_ss [lisp_exp_def,cond_STAR,lisp_x_def,ALIGNED_INTRO] 2645 \\ SIMP_TAC std_ss [IN_DEF,set_add_def,WORD_SUB_SUB,WORD_SUB_RZERO] 2646 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,word_sub_def], 2647 SIMP_TAC std_ss [lisp_exp_def,cond_STAR,lisp_x_def,ALIGNED_INTRO,sexp_ok_def] 2648 \\ SIMP_TAC std_ss [ADDR32_n2w,word_add_n2w,AC MULT_COMM MULT_ASSOC], 2649 SIMP_TAC std_ss [lisp_exp_def,cond_STAR,lisp_x_def,ALIGNED_INTRO,sexp_ok_def] 2650 \\ SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR,SEP_CLAUSES] 2651 \\ SIMP_TAC std_ss [SEP_EXISTS] \\ REPEAT STRIP_TAC THENL [ 2652 `a IN ch_active_set2 (r5 + 0x8w,0,ll)` by SEP_READ_TAC 2653 \\ FULL_SIMP_TAC std_ss [ch_active_set2_def,ch_active_set_def, 2654 GSPECIFICATION,IN_UNION] THENL [ 2655 Q.EXISTS_TAC `1 + j` 2656 \\ SIMP_TAC std_ss [word_mul_n2w,LEFT_ADD_DISTRIB] 2657 \\ ASM_SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_ASSOC], 2658 FULL_SIMP_TAC (std_ss++sep_cond_ss) [GSYM ALIGNED8_def,cond_STAR] 2659 \\ FULL_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w,word_mul_n2w] 2660 \\ FULL_SIMP_TAC bool_ss [DECIDE ``8 + (4 + 8 * j) = 4 + 8 * (1 + j:num)``] 2661 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_PLUS] 2662 \\ FULL_SIMP_TAC std_ss [ALIGNED8_SUB] 2663 \\ FULL_SIMP_TAC std_ss [word_sub_def] 2664 \\ `ALIGNED8 (-4w:word32)` by METIS_TAC [ALIGNED8_ADD_EQ] 2665 \\ POP_ASSUM MP_TAC \\ EVAL_TAC], 2666 FULL_SIMP_TAC (std_ss++sep_cond_ss) [GSYM ALIGNED8_def,cond_STAR], 2667 FULL_SIMP_TAC (std_ss++sep_cond_ss) [GSYM ALIGNED8_def,cond_STAR] 2668 \\ Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC) 2669 \\ Q.PAT_X_ASSUM `!xx.bbb` MATCH_MP_TAC 2670 \\ Q.EXISTS_TAC `one (a,y) * one (a + 0x4w,y') * p * lisp_exp s' y' (sa,xi)` 2671 \\ `h a = y` by SEP_READ_TAC 2672 \\ FULL_SIMP_TAC (std_ss++star_ss) [], 2673 FULL_SIMP_TAC (std_ss++sep_cond_ss) [GSYM ALIGNED8_def,cond_STAR] 2674 \\ Q.PAT_X_ASSUM `!xx.bbb` MATCH_MP_TAC 2675 \\ Q.EXISTS_TAC `one (a,y) * one (a + 0x4w,y') * p * lisp_exp s y (sa,xi)` 2676 \\ `h (a + 4w) = y'` by SEP_READ_TAC 2677 \\ FULL_SIMP_TAC (std_ss++star_ss) []]]); 2678 2679val lisp_exp_ok_data = prove( 2680 ``!x w a s p f df. 2681 (lisp_exp x w (a,s) * p) (fun2set (f,df)) ==> 2682 ok_data w { y | y IN df /\ ALIGNED8 (a - y) }``, 2683 REVERSE Induct THENL [ 2684 SIMP_TAC std_ss [lisp_exp_def,cond_STAR,ok_data_def] 2685 \\ REPEAT STRIP_TAC 2686 \\ IMP_RES_TAC NOT_ALIGNED 2687 \\ FULL_SIMP_TAC std_ss [WORD_SUB_ADD,word_arith_lemma3,WORD_ADD_0], 2688 SIMP_TAC std_ss [lisp_exp_def,cond_STAR,ok_data_def] 2689 \\ SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_ADDR32,ALIGNED_n2w] 2690 \\ FULL_SIMP_TAC std_ss [WORD_ADD_0,word_arith_lemma4] 2691 \\ SIMP_TAC std_ss [ALIGNED_ADD_EQ,ALIGNED_ADDR32,ALIGNED_n2w], 2692 SIMP_TAC (std_ss++sep_cond_ss) [lisp_exp_def,cond_STAR,ok_data_def] 2693 \\ SIMP_TAC std_ss [SEP_CLAUSES] \\ SIMP_TAC std_ss [SEP_EXISTS] 2694 \\ SIMP_TAC std_ss [GSYM STAR_ASSOC,one_STAR,IN_fun2set] 2695 \\ REPEAT STRIP_TAC 2696 \\ ASM_SIMP_TAC std_ss [GSPECIFICATION,ALIGNED8_def]]); 2697 2698val SUBSET_ok_data = prove( 2699 ``!a s t. ok_data a t /\ t SUBSET s ==> ok_data a s``, 2700 METIS_TAC [ok_data_def,SUBSET_DEF]); 2701 2702val SEP_EXPS_ok_data = prove( 2703 ``!xs sa xi hh s x g. 2704 SEP_EXPS xs (a,xi) (fun2set (hh,g)) /\ x IN g /\ g SUBSET s ==> 2705 ok_data (hh x) { y | y IN s /\ ALIGNED8 (a - y) }``, 2706 STRIP_TAC \\ completeInduct_on `LENGTH xs + 2 * SUM_LSIZE (MAP SND xs)` 2707 \\ Cases \\ SIMP_TAC std_ss [SEP_EXPS_def,emp_def,fun2set_EMPTY,SUBSET_EMPTY] 2708 THEN1 METIS_TAC [NOT_IN_EMPTY] 2709 \\ Cases_on `h` 2710 \\ SIMP_TAC std_ss [SEP_EXPS_def,LENGTH,MAP,SUM_LSIZE_def,MULT_CLAUSES] 2711 \\ REVERSE (STRIP_ASSUME_TAC (Q.SPEC `r` SExp_expand)) 2712 \\ ASM_SIMP_TAC (std_ss++sep_cond_ss) [lisp_exp_def,cond_STAR,LSIZE_def] 2713 THEN1 (FULL_SIMP_TAC std_ss [ADD] \\ METIS_TAC [DECIDE ``m < SUC m:num``]) 2714 THEN1 (FULL_SIMP_TAC std_ss [ADD] \\ METIS_TAC [DECIDE ``m < SUC m:num``]) 2715 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES] 2716 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 2717 \\ FULL_SIMP_TAC std_ss [GSYM STAR_ASSOC,one_STAR,IN_fun2set,fun2set_DELETE] 2718 \\ NTAC 7 STRIP_TAC 2719 \\ `(g DELETE q DELETE (q + 0x4w)) SUBSET g` by METIS_TAC [SUBSET_DEF,IN_DELETE] 2720 \\ Cases_on `x = q` THEN1 2721 (REPEAT STRIP_TAC \\ IMP_RES_TAC lisp_exp_ok_data 2722 \\ MATCH_MP_TAC SUBSET_ok_data 2723 \\ Q.EXISTS_TAC `{y | y IN g DELETE q DELETE (q + 0x4w) /\ ALIGNED8 (a - y)}` 2724 \\ ASM_SIMP_TAC std_ss [] 2725 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,GSPECIFICATION,IN_DELETE]) 2726 \\ Cases_on `x = q + 4w` THEN1 2727 (Q.PAT_X_ASSUM `bbb (fun2set (hh,g DELETE q DELETE (q + 0x4w)))` MP_TAC 2728 \\ ONCE_REWRITE_TAC [STAR_COMM] 2729 \\ SIMP_TAC std_ss [GSYM STAR_ASSOC] 2730 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC lisp_exp_ok_data 2731 \\ MATCH_MP_TAC SUBSET_ok_data 2732 \\ Q.EXISTS_TAC `{y | y IN g DELETE q DELETE (q + 0x4w) /\ ALIGNED8 (a - y)}` 2733 \\ ASM_SIMP_TAC std_ss [] 2734 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,GSPECIFICATION,IN_DELETE]) 2735 \\ SIMP_TAC std_ss [GSYM STAR_ASSOC,GSYM SEP_EXPS_def,IN_DELETE] 2736 \\ SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL] 2737 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 2738 \\ Q.ABBREV_TAC `a1 = exp1` \\ Q.ABBREV_TAC `a2 = exp2` 2739 \\ NTAC 2 (POP_ASSUM (K ALL_TAC)) 2740 \\ REPEAT STRIP_TAC 2741 \\ `x IN (g DELETE q DELETE (q + 0x4w))` by ASM_SIMP_TAC std_ss [IN_DELETE] 2742 \\ IMP_RES_TAC SUBSET_TRANS 2743 \\ FULL_SIMP_TAC std_ss [] 2744 \\ Q.ABBREV_TAC `ys = (hh q,a1)::(hh (q + 0x4w),a2)::t` 2745 \\ Q.ABBREV_TAC `i = SUC (LENGTH t) + 2746 2 * (SUC (LSIZE a1 + LSIZE a2) + SUM_LSIZE (MAP SND t))` 2747 \\ `LENGTH ys + 2 * SUM_LSIZE (MAP SND ys) < i` by 2748 (Q.UNABBREV_TAC `ys` \\ Q.UNABBREV_TAC `i` 2749 \\ FULL_SIMP_TAC std_ss [LENGTH,MAP,SUM_LSIZE_def,MULT_CLAUSES,ADD1] 2750 \\ DECIDE_TAC) 2751 \\ FULL_SIMP_TAC std_ss [] 2752 \\ Q.PAT_X_ASSUM `!m. m < i ==> bbb` (ASSUME_TAC o UNDISCH o Q.SPEC `LENGTH (ys:(word32 # SExp) list) + 2 * SUM_LSIZE (MAP SND ys)`) 2753 \\ POP_ASSUM (ASSUME_TAC o RW [] o Q.SPEC `ys`) 2754 \\ `x IN (g DELETE q DELETE (q + 0x4w))` by METIS_TAC [IN_DELETE] 2755 \\ FULL_SIMP_TAC std_ss [GSYM SEP_EXPS_def] 2756 \\ METIS_TAC [SUBSET_TRANS]); 2757 2758val arm_string2sexp_lemma = store_thm("arm_string2sexp_lemma", 2759 ``32 <= w2n r5 /\ w2n r5 + 16 * l + 20 < 2 ** 32 /\ l <> 0 /\ 2760 sexp_lex_space (sexp2string s) <= l /\ sexp_ok s /\ 2761 string_mem (STRCAT (sexp2string s) null_string) (r3,f,df) /\ ALIGNED r5 /\ 2762 (token_slots (r5 - 32w) (l + l + 7)) (fun2set (h,dh)) /\ 2763 symbol_table_dom (all_symbols (sexp2tokens s T) builtin_symbols) 2764 (r5 + n2w (l * 16) + 0x18w,dm,dg) ==> 2765 ?r3i gi hi mi. 2766 arm_string2sexp'_pre (r3,n2w l,r5,df,dg,dh,dm,f,g,h,m) /\ 2767 (arm_string2sexp' (r3,n2w l,r5,df,dg,dh,dm,f,g,h,m) = 2768 (r3i,3w,3w,3w,3w,3w,r5,df,dg,dh,dm,f,gi,hi,mi)) /\ 2769 ?sym. lisp_inv (s,Sym "nil",Sym "nil",Sym "nil",Sym "nil",Sym "nil",l) 2770 (r3i,3w,3w,3w,3w,3w,r5,dh,hi,sym,dm,mi,dg,gi)``, 2771 REWRITE_TAC [GSYM AND_IMP_INTRO] 2772 \\ SIMP_TAC std_ss [GSYM sexp_lex_sexp2str] 2773 \\ REWRITE_TAC [AND_IMP_INTRO,GSYM CONJ_ASSOC,GSYM sexp2string_def] 2774 \\ REPEAT STRIP_TAC 2775 \\ SIMP_TAC std_ss [arm_string2sexp_def,arm_string2sexp_pre_def,LET_DEF] 2776 \\ SIMP_TAC std_ss [word_LSL_n2w,word_add_n2w,GSYM LEFT_ADD_DISTRIB] 2777 \\ `symbol_table_dom builtin_symbols (r5 + n2w (l * 16) + 0x18w,dm,dg)` by 2778 (MATCH_MP_TAC symbol_table_dom_APPEND \\ METIS_TAC [all_symbols_exists]) 2779 \\ (STRIP_ASSUME_TAC o UNDISCH o SPEC_ALL o 2780 Q.SPECL [`40w`,`r5 + n2w (l * 16) + 0x18w`] o GEN_ALL) arm_setup_lemma 2781 \\ ASM_SIMP_TAC std_ss [WORD_ADD_SUB,ALIGNED_INTRO] 2782 \\ `n2w (l * 16) + r5 + 0x18w = r5 + n2w (l * 16) + 0x18w` by 2783 SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 2784 \\ ASM_SIMP_TAC std_ss [WORD_ADD_SUB,ALIGNED_INTRO] 2785 \\ POP_ASSUM (K ALL_TAC) 2786 \\ Q.ABBREV_TAC `h2 = (r5 =+ 0x28w) ((r5 - 0x20w =+ n2w (l * 8)) h)` 2787 \\ `ALIGNED (r5 + 8w)` by ALIGNED_TAC 2788 \\ IMP_RES_TAC sexp2string_NOT_NULL 2789 \\ `(token_slots (r5 - 0x18w) 3 * one (r5 - 0x20w,n2w (l * 8)) * 2790 token_slots (r5 + 0x8w + n2w (8 * sexp_lex_space (sexp2string s))) 2791 (l + l + 2 - sexp_lex_space (sexp2string s)) * 2792 (SEP_EXISTS w. one (r5 - 0x1Cw,w)) * arm_tokens4 r5 [] b d r5 * 2793 token_slots (r5 + 0x8w) (sexp_lex_space (sexp2string s))) 2794 (fun2set (h2,dh))` by 2795 (Q.PAT_X_ASSUM `32 <= w2n r5` (K ALL_TAC) 2796 \\ Q.PAT_X_ASSUM `w2n r5 + 16 * l + 20 < 4294967296` (K ALL_TAC) 2797 \\ Q.PAT_X_ASSUM `l <> 0` (K ALL_TAC) 2798 \\ FULL_SIMP_TAC std_ss [LESS_EQ_EXISTS] 2799 \\ Q.ABBREV_TAC `k = sexp_lex_space (sexp2string s)` 2800 \\ Q.UNABBREV_TAC `h2` 2801 \\ `k + p + (k + p) + 2 - k = k + p + p + 2` by DECIDE_TAC 2802 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES] 2803 \\ ASM_SIMP_TAC std_ss [arm_tokens2_def,arm_tokens4_def,SEP_CLAUSES,STAR_ASSOC] 2804 \\ `l + l + 7 = 1 + 3 + 1 + k + k + p + p + 2` by DECIDE_TAC 2805 \\ FULL_SIMP_TAC bool_ss [] 2806 \\ FULL_SIMP_TAC std_ss [token_slots_ADD] 2807 \\ FULL_SIMP_TAC std_ss [LEFT_ADD_DISTRIB,GSYM word_add_n2w] 2808 \\ FULL_SIMP_TAC std_ss [WORD_ADD_ASSOC,WORD_SUB_ADD,STAR_ASSOC] 2809 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3] 2810 \\ FULL_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w,ADD_ASSOC] 2811 \\ FULL_SIMP_TAC bool_ss [GSYM (EVAL ``SUC 0``)] 2812 \\ FULL_SIMP_TAC bool_ss [token_slots_def,SEP_CLAUSES] 2813 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,STAR_ASSOC] 2814 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 2815 \\ Q.EXISTS_TAC `y'` 2816 \\ Q.EXISTS_TAC `y'''` 2817 \\ SEP_WRITE_TAC) 2818 \\ `ALIGNED8 (r5 + n2w (l * 16) + 0x18w - r5)` by 2819 (SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_ADD_SUB2] 2820 \\ SIMP_TAC bool_ss [word_add_n2w,DECIDE ``l * 16 + 24 = 0 + 8 * (2 * l + 3:num)``] 2821 \\ SIMP_TAC bool_ss [GSYM word_add_n2w,ALIGNED8_ADD] \\ EVAL_TAC) 2822 \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o SPEC_ALL o 2823 Q.SPECL [`r5`,`builtin_symbols_set (r5 + n2w (l * 16) + 0x18w)`, 2824 `sexp2string s`,`token_slots (r5 - 24w) 3 * one (r5 - 32w,n2w (l * 8)) * 2825 token_slots (r5 + 0x8w + n2w (8 * sexp_lex_space (sexp2string s))) 2826 (l + l + 2 - sexp_lex_space (sexp2string s)) * 2827 SEP_EXISTS w. one (r5 - 28w,w)`] o 2828 MATCH_INST arm_parse6_lemma) 2829 ``arm_parse8 2830 (r5 + 0x8w,r5 + n2w (l * 16) + 0x18w,r3,0x28w,n2w (l * 16),n2w (l * 8), 2831 df,dg,dh,dm,f,gi,h2,mi)`` 2832 \\ ASM_SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC THEN1 2833 (ALIGNED_TAC 2834 \\ FULL_SIMP_TAC bool_ss [DECIDE ``3:num = SUC (SUC (SUC 0))``,token_slots_def,arm_tokens4_def,arm_tokens2_def] 2835 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,SEP_CLAUSES] 2836 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,STAR_ASSOC] \\ SEP_READ_TAC) 2837 \\ Q.EXISTS_TAC `set_add (0w - (r5 + n2w (l * 16) + 0x18w)) xi` 2838 \\ `hi (r5 - 0x20w) = n2w (l * 8)` by SEP_READ_TAC 2839 \\ ASM_SIMP_TAC std_ss [] 2840 \\ Q.ABBREV_TAC `h3 = (r5 =+ r5 + n2w (8 * sexp_lex_space (sexp2string s)) + 0x8w) 2841 ((r5 + 0x4w =+ r5 + n2w (l * 8) + 0x8w) ((r5 - 0x1Cw =+ 0x1w) hi))` 2842 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 2843 \\ Q.EXISTS_TAC `1 + sexp_lex_space (sexp2string s)` 2844 \\ Q.EXISTS_TAC `F` 2845 \\ ASM_SIMP_TAC std_ss [LET_DEF,lisp_x_def,word_arith_lemma2, 2846 ALIGNED_INTRO,ALIGNED_n2w] 2847 \\ Q.ABBREV_TAC `ll = sexp_lex_space (sexp2string s)` 2848 \\ SIMP_TAC std_ss [lisp_symbol_table_def] 2849 \\ STRIP_TAC THEN1 2850 (Q.UNABBREV_TAC `h3` 2851 \\ SIMP_TAC std_ss [LEFT_ADD_DISTRIB,GSYM word_add_n2w] 2852 \\ SIMP_TAC std_ss [APPLY_UPDATE_THM] 2853 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM]) 2854 \\ STRIP_TAC THEN1 2855 (Q.UNABBREV_TAC `h3` 2856 \\ SIMP_TAC std_ss [LEFT_ADD_DISTRIB,GSYM word_add_n2w] 2857 \\ SIMP_TAC std_ss [APPLY_UPDATE_THM,WORD_EQ_ADD_CANCEL] 2858 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 2859 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM, 2860 AC MULT_COMM MULT_ASSOC]) 2861 \\ STRIP_TAC THEN1 2862 (Q.UNABBREV_TAC `h3` 2863 \\ SIMP_TAC std_ss [APPLY_UPDATE_THM,WORD_EQ_SUB_LADD,word_arith_lemma1] 2864 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,WORD_EQ_ADD_CANCEL,WORD_SUB_ADD]) 2865 \\ STRIP_TAC THEN1 2866 (Q.UNABBREV_TAC `h3` 2867 \\ SIMP_TAC std_ss [APPLY_UPDATE_THM,WORD_EQ_SUB_LADD,word_arith_lemma3,word_arith_lemma1] 2868 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11,WORD_EQ_ADD_CANCEL] 2869 \\ ONCE_REWRITE_TAC [MULT_COMM] \\ SEP_READ_TAC) 2870 \\ STRIP_TAC THEN1 2871 (IMP_RES_TAC token_slots_IMP \\ ASM_SIMP_TAC std_ss [] 2872 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 2873 \\ REWRITE_TAC [ch_active_set_4,ref_set_def] 2874 \\ SIMP_TAC std_ss [LEFT_ADD_DISTRIB,MULT_ASSOC] 2875 \\ SIMP_TAC std_ss [EXTENSION,IN_UNION,GSPECIFICATION] 2876 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 2877 \\ ASM_SIMP_TAC std_ss [] THENL [ 2878 Cases_on `i <= 8` THENL [ 2879 DISJ2_TAC \\ Q.EXISTS_TAC `8 - i` 2880 \\ SIMP_TAC std_ss [LEFT_SUB_DISTRIB,MULT_ASSOC] 2881 \\ Cases_on `i = 8` 2882 \\ ASM_SIMP_TAC std_ss [word_arith_lemma3,WORD_ADD_0,WORD_SUB_RZERO] 2883 \\ `4 * i < 32` by DECIDE_TAC 2884 \\ ASM_SIMP_TAC std_ss [], 2885 DISJ1_TAC \\ Q.EXISTS_TAC `i - 8` 2886 \\ `~(4 * i < 32)` by DECIDE_TAC 2887 \\ ASM_SIMP_TAC std_ss [word_arith_lemma3,WORD_ADD_0,WORD_SUB_RZERO] 2888 \\ SIMP_TAC std_ss [LEFT_SUB_DISTRIB,MULT_ASSOC] \\ DECIDE_TAC], 2889 Q.EXISTS_TAC `8 + i` 2890 \\ SIMP_TAC std_ss [LEFT_ADD_DISTRIB,MULT_ASSOC,GSYM word_add_n2w] 2891 \\ SIMP_TAC std_ss [WORD_ADD_ASSOC,WORD_SUB_ADD] \\ DECIDE_TAC, 2892 Q.EXISTS_TAC `8 - i` 2893 \\ SIMP_TAC std_ss [LEFT_SUB_DISTRIB,MULT_ASSOC] 2894 \\ Cases_on `i = 0` 2895 \\ ASM_SIMP_TAC std_ss [word_arith_lemma3,WORD_ADD_0,WORD_SUB_RZERO] 2896 THEN1 DECIDE_TAC 2897 \\ `0 < 4 * i /\ (32 - (32 - 4 * i) = 4*i)` by DECIDE_TAC 2898 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC]) 2899 \\ STRIP_TAC THEN1 2900 (FULL_SIMP_TAC std_ss [word_mul_n2w,Q.SPEC `16` MULT_COMM] 2901 \\ Q.ABBREV_TAC `a = r5 + n2w (l * 16) + 0x18w` 2902 \\ `?zs. all_symbols (sexp_lex (sexp2string s)) builtin_symbols = 2903 builtin_symbols ++ zs` by 2904 METIS_TAC [all_symbols_exists] 2905 \\ Q.EXISTS_TAC `zs` 2906 \\ FULL_SIMP_TAC std_ss [] 2907 \\ `set_add a (set_add (0x0w - a) xi) = xi` by 2908 (REPEAT (POP_ASSUM (K ALL_TAC)) 2909 \\ SIMP_TAC std_ss [set_add_def,FUN_EQ_THM,FORALL_PROD,IN_DEF] 2910 \\ SIMP_TAC std_ss [WORD_SUB_SUB,WORD_SUB_ADD,WORD_SUB_RZERO]) 2911 \\ ASM_SIMP_TAC std_ss [] 2912 \\ POP_ASSUM (K ALL_TAC) 2913 \\ POP_ASSUM (fn th => REWRITE_TAC [GSYM th]) 2914 \\ REWRITE_TAC [ALL_DISTINCT_all_symbols] \\ EVAL_TAC) 2915 \\ Q.ABBREV_TAC `sa = (r5 + n2w (l * 16) + 0x18w)` 2916 \\ `(0x0w,"nil") IN set_add (0x0w - sa) xi` by 2917 (Q.PAT_X_ASSUM `symbol_table 2918 (all_symbols (sexp_lex (sexp2string s)) builtin_symbols) xi 2919 (sa,dm,mi',dg,gi')` MP_TAC 2920 \\ Q.UNABBREV_TAC `sa` \\ REPEAT (POP_ASSUM (K ALL_TAC)) 2921 \\ `?zs. all_symbols (sexp_lex (sexp2string s)) builtin_symbols = 2922 builtin_symbols ++ zs` by METIS_TAC [all_symbols_exists] 2923 \\ Q.ABBREV_TAC `sa = (r5 + n2w (l * 16) + 0x18w)` 2924 \\ ASM_SIMP_TAC std_ss [builtin_symbols_def,APPEND] 2925 \\ ONCE_REWRITE_TAC [symbol_table_def] 2926 \\ SIMP_TAC std_ss [IN_DEF,set_add_def,WORD_SUB_SUB, 2927 WORD_ADD_0,WORD_SUB_RZERO]) 2928 \\ ASM_SIMP_TAC std_ss [] 2929 \\ `(token_slots (r5 - 0x20w) 5 * 2930 token_slots (r5 + 0x8w + n2w (8 * ll)) (l + l + 2 - ll) * 2931 lisp_exp (string2sexp (sexp2string s)) r7i (sa,xi) * 2932 SEP_FILL (sa,xi)) (fun2set (h3,dh))` by 2933 (Q.PAT_X_ASSUM `ppp (fun2set (hi,dh))` MP_TAC \\ Q.UNABBREV_TAC `h3` 2934 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 2935 \\ SIMP_TAC std_ss [arm_tokens4_def,arm_tokens2_def,SEP_CLAUSES] 2936 \\ REWRITE_TAC [DECIDE ``5 = SUC 0 + 3 + SUC 0:num``] 2937 \\ REWRITE_TAC [token_slots_ADD,token_slots_def] 2938 \\ SIMP_TAC std_ss [WORD_SUB_ADD,SEP_CLAUSES] 2939 \\ SIMP_TAC std_ss [STAR_ASSOC,word_arith_lemma3,SEP_EXISTS] 2940 \\ REPEAT STRIP_TAC 2941 \\ Q.EXISTS_TAC `r5 + n2w (8 * ll) + 0x8w` 2942 \\ Q.EXISTS_TAC `r5 + n2w (l * 8) + 0x8w` 2943 \\ Q.EXISTS_TAC `n2w (l * 8)` 2944 \\ Q.EXISTS_TAC `1w` 2945 \\ SEP_WRITE_TAC) 2946 \\ `(lisp_exp (string2sexp (sexp2string s)) r7i (sa,xi) * 2947 SEP_FILL (sa,xi)) (fun2set (h3,dh 2948 DIFF ch_active_set2 (r5 - 0x20w,0,5) 2949 DIFF ch_active_set2 (r5 + 0x8w + n2w (8 * ll),0,l + l + 2 - ll)))` by 2950 (MATCH_MP_TAC fun2set_DIFF_IMP 2951 \\ Q.EXISTS_TAC `token_slots (r5 + 0x8w + n2w (8 * ll)) (l + l + 2 - ll)` 2952 \\ STRIP_TAC THEN1 2953 (REPEAT STRIP_TAC 2954 \\ IMP_RES_TAC token_slots_IMP 2955 \\ FULL_SIMP_TAC std_ss [ch_active_set2_def]) 2956 \\ MATCH_MP_TAC fun2set_DIFF_IMP 2957 \\ Q.EXISTS_TAC `token_slots (r5 - 0x20w) 5` 2958 \\ ASM_SIMP_TAC std_ss [STAR_ASSOC] 2959 \\ REPEAT STRIP_TAC 2960 \\ IMP_RES_TAC token_slots_IMP 2961 \\ FULL_SIMP_TAC std_ss [ch_active_set2_def]) 2962 \\ `dh DIFF ch_active_set2 (r5 - 0x20w,0,5) DIFF 2963 ch_active_set2 (r5 + 0x8w + n2w (8 * ll),0,l + l + 2 - ll) = 2964 ch_active_set2 (r5 + 0x8w,0,ll)` by 2965 (IMP_RES_TAC token_slots_IMP 2966 \\ ASM_SIMP_TAC std_ss [] 2967 \\ NTAC 24 (POP_ASSUM (K ALL_TAC)) 2968 \\ ASM_SIMP_TAC std_ss [ch_active_set2_def] 2969 \\ SIMP_TAC std_ss [ch_active_set_4] 2970 \\ `{r5 - 0x20w + n2w (4 * i) | i < 2 * (l + l + 7)} DIFF 2971 {r5 - 0x20w + n2w (4 * i) | i < 10} = 2972 {r5 + 0x8w + n2w (4 * i) | i < 2 * (l + l + 2)}` by 2973 (SIMP_TAC std_ss [EXTENSION,IN_DIFF,GSPECIFICATION] 2974 \\ REVERSE (REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC) 2975 \\ ASM_SIMP_TAC std_ss [] THENL [ 2976 SIMP_TAC std_ss [GSYM WORD_ADD_SUB_SYM,WORD_EQ_SUB_LADD] 2977 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 2978 \\ SIMP_TAC std_ss [word_add_n2w,ADD_ASSOC] 2979 \\ `8 + 4 * i + 32 < 4294967296` by DECIDE_TAC 2980 \\ Cases_on `i' < 10` \\ ASM_SIMP_TAC std_ss [] 2981 \\ `4 * i' < 4294967296` by DECIDE_TAC 2982 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] \\ DECIDE_TAC, 2983 SIMP_TAC std_ss [GSYM WORD_ADD_SUB_SYM,WORD_EQ_SUB_LADD] 2984 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 2985 \\ SIMP_TAC std_ss [word_add_n2w,ADD_ASSOC] 2986 \\ Q.EXISTS_TAC `2 + i + 8` 2987 \\ ASM_SIMP_TAC std_ss [LEFT_ADD_DISTRIB] \\ DECIDE_TAC, 2988 REPEAT (Q.PAT_X_ASSUM `!x.bbb` MP_TAC) 2989 \\ ASM_SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL] 2990 \\ SIMP_TAC std_ss [GSYM WORD_ADD_SUB_SYM,WORD_EQ_SUB_RADD] 2991 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 2992 \\ REWRITE_TAC [METIS_PROVE [] ``b \/ ~c = c ==> b``] 2993 \\ REPEAT STRIP_TAC 2994 \\ Cases_on `i < 10` THEN1 (RES_TAC \\ FULL_SIMP_TAC std_ss []) 2995 \\ Q.EXISTS_TAC `i - 10` 2996 \\ ASM_SIMP_TAC std_ss [LEFT_SUB_DISTRIB] 2997 \\ `8 + (4 * i - 40) + 32 = 4 * i` by DECIDE_TAC 2998 \\ ASM_SIMP_TAC std_ss [word_add_n2w,ADD_ASSOC] \\ DECIDE_TAC]) 2999 \\ ASM_SIMP_TAC std_ss [] 3000 \\ SIMP_TAC std_ss [EXTENSION,IN_DIFF,GSPECIFICATION] 3001 \\ REVERSE (REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC) 3002 \\ ASM_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC, WORD_EQ_ADD_CANCEL] 3003 THENL [ 3004 SIMP_TAC std_ss [word_add_n2w] 3005 \\ REWRITE_TAC [METIS_PROVE [] ``b \/ ~c = c ==> b``] 3006 \\ STRIP_TAC 3007 \\ `8 * ll + 4 * i' < 4294967296 /\ 4 * i < 4294967296` by DECIDE_TAC 3008 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] \\ DECIDE_TAC, 3009 Q.EXISTS_TAC `i` \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC, 3010 Q.EXISTS_TAC `i` \\ ASM_SIMP_TAC std_ss [] 3011 \\ POP_ASSUM MP_TAC 3012 \\ ASM_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC, WORD_EQ_ADD_CANCEL] 3013 \\ REWRITE_TAC [METIS_PROVE [] ``b \/ ~c = c ==> b``] 3014 \\ SIMP_TAC std_ss [word_add_n2w] \\ STRIP_TAC 3015 \\ CCONTR_TAC 3016 \\ `i - 2 * ll < 2 * (l + l + 2 - ll)` by DECIDE_TAC 3017 \\ RES_TAC 3018 \\ `8 * ll + 4 * (i - 2 * ll) = 4 * i` by DECIDE_TAC 3019 \\ FULL_SIMP_TAC std_ss []]) 3020 \\ FULL_SIMP_TAC std_ss [] 3021 \\ POP_ASSUM (K ALL_TAC) 3022 \\ `SEP_FILL (sa,xi) (fun2set (h3,ch_active_set2 (r5 + 0x8w,0,ll)))` by 3023 (POP_ASSUM MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 3024 \\ ASM_SIMP_TAC std_ss [SEP_FILL_def,SEP_CLAUSES] 3025 \\ SIMP_TAC std_ss [SEP_EXISTS] \\ STRIP_TAC 3026 \\ METIS_TAC [SEP_EXPS_def]) 3027 \\ IMP_RES_TAC string2sexp_sexp2string 3028 \\ FULL_SIMP_TAC std_ss [] 3029 \\ STRIP_TAC THEN1 METIS_TAC [IMP_lisp_x] 3030 \\ POP_ASSUM (K ALL_TAC) 3031 \\ POP_ASSUM MP_TAC 3032 \\ Q.PAT_X_ASSUM `ALIGNED8 (sa - r5)` MP_TAC 3033 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 3034 \\ STRIP_TAC 3035 \\ `ch_active_set (r5,1,1 + ll) = 3036 { y | y IN ch_active_set2 (r5 + 0x8w,0,ll) /\ ALIGNED8 (sa - y) }` by 3037 (SIMP_TAC std_ss [ch_active_set2_def] 3038 \\ SIMP_TAC std_ss [IN_UNION,METIS_PROVE [] 3039 ``(b1 \/ b2) /\ b = b /\ b1 \/ b /\ b2``] 3040 \\ `!y. ALIGNED8 (sa - y) /\ y IN ch_active_set (r5 + 0x8w + 0x4w,0,ll) = F` by 3041 (STRIP_TAC \\ Cases_on `y IN ch_active_set (r5 + 0x8w + 0x4w,0,ll)` 3042 \\ ASM_SIMP_TAC std_ss [] 3043 \\ FULL_SIMP_TAC std_ss [ch_active_set_def,GSPECIFICATION] 3044 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w,word_mul_n2w] 3045 \\ REWRITE_TAC [DECIDE ``8 + (4 + 8 * j) = 4 + 8 * (j + 1:num)``] 3046 \\ SIMP_TAC std_ss [WORD_SUB_PLUS,GSYM word_add_n2w,ALIGNED8_SUB] 3047 \\ FULL_SIMP_TAC std_ss [ALIGNED8_ADD_EQ,word_sub_def] \\ EVAL_TAC) 3048 \\ ASM_SIMP_TAC std_ss [] 3049 \\ SIMP_TAC std_ss [EXTENSION,GSPECIFICATION,ch_active_set_def] 3050 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 3051 \\ ASM_SIMP_TAC std_ss [] 3052 THEN1 ASM_SIMP_TAC std_ss [WORD_SUB_PLUS,word_mul_n2w,ALIGNED8_SUB] 3053 THENL [ 3054 Q.EXISTS_TAC `j - 1` 3055 \\ `8 + 8 * (j - 1) = 8 * j` by DECIDE_TAC 3056 \\ ASM_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_mul_n2w,word_add_n2w] 3057 \\ DECIDE_TAC, 3058 Q.EXISTS_TAC `SUC j` 3059 \\ ASM_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_mul_n2w,word_add_n2w, 3060 MULT_CLAUSES] \\ DECIDE_TAC]) 3061 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 3062 \\ MATCH_MP_TAC SEP_EXPS_ok_data 3063 \\ FULL_SIMP_TAC std_ss [SEP_FILL_def,SEP_EXISTS] 3064 THENL [ 3065 Q.EXISTS_TAC `y` \\ Q.EXISTS_TAC `xi` 3066 \\ Q.EXISTS_TAC `ch_active_set2 (r5 + 0x8w,0,ll)` 3067 \\ ASM_SIMP_TAC std_ss [SUBSET_REFL] 3068 \\ POP_ASSUM MP_TAC 3069 \\ ASM_SIMP_TAC std_ss [GSPECIFICATION], 3070 Q.EXISTS_TAC `y` \\ Q.EXISTS_TAC `xi` 3071 \\ Q.EXISTS_TAC `ch_active_set2 (r5 + 0x8w,0,ll)` 3072 \\ ASM_SIMP_TAC std_ss [SUBSET_REFL] 3073 \\ POP_ASSUM MP_TAC 3074 \\ SIMP_TAC std_ss [GSPECIFICATION,ch_active_set2_def, 3075 ch_active_set_def,IN_UNION] 3076 \\ REPEAT STRIP_TAC \\ DISJ2_TAC 3077 \\ Q.EXISTS_TAC `j - 1` 3078 \\ ASM_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_CANCEL] 3079 \\ `8 + (4 + 8 * (j - 1)) = 8 * j + 4`by DECIDE_TAC 3080 \\ ASM_SIMP_TAC std_ss [word_add_n2w,word_mul_n2w] 3081 \\ DECIDE_TAC]); 3082 3083 3084(* formulating the final theorem *) 3085 3086open lisp_opsTheory; 3087 3088val aSTRING_def = Define ` 3089 aSTRING a str = SEP_EXISTS df f. aBYTE_MEMORY df f * 3090 cond (string_mem (STRCAT str null_string) (a,f,df))`; 3091 3092val pSTRING_def = Define ` 3093 pSTRING a str = SEP_EXISTS df f. pBYTE_MEMORY df f * 3094 cond (string_mem (STRCAT str null_string) (a,f,df))`; 3095 3096val xSTRING_def = Define ` 3097 xSTRING a str = SEP_EXISTS df f. xBYTE_MEMORY df f * 3098 cond (string_mem (STRCAT str null_string) (a,f,df))`; 3099 3100fun AUTO_EXISTS_TAC (asm,tm) = let 3101 fun ex tm = let 3102 val (v,tm) = dest_exists tm 3103 in v :: ex tm end handle e => [] 3104 val xs = ex tm 3105 val x = hd (list_dest dest_conj (repeat (snd o dest_exists) tm)) 3106 val assum = [``lisp_inv (Dot x1 x2,x2,x3,x4,x5,x6,limit) 3107 (w1,w2,w3,w4,w5,w6,a',x',xs',s,dm,m,dg,g)``, 3108 ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) 3109 (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g)``] 3110 val tm2 = hd (filter (can (match_term x)) asm) 3111 val (s,_) = match_term x tm2 3112 val ys = map (subst s) xs 3113 fun exx [] = ALL_TAC | exx (x::xs) = EXISTS_TAC x THEN exx xs 3114 in exx ys (asm,tm) end 3115 3116fun store_string2sexp_thm target extra post = let 3117 fun get_thm s [] = fail() 3118 | get_thm s ((t,th)::xs) = if s = t then th else get_thm s xs 3119 val th = get_thm target arm_string2sexp_thms 3120 val p = find_term (can (match_term ``aPC p``)) (cdr (concl th)) handle e => 3121 find_term (can (match_term ``pPC p``)) (cdr (concl th)) handle e => 3122 find_term (can (match_term ``xPC p``)) (cdr (concl th)) 3123 val p = cdr p 3124 val post = subst [mk_var("p",``:word32``) |-> p] post 3125 val imp = arm_string2sexp_lemma 3126 val tm = (cdr o car o concl) imp 3127 val s = INST (map (fn (x,y) => mk_var(y,``:word32``) |-> mk_var("r"^x,``:word32``)) 3128 [("3","eax"),("4","ecx"),("5","edx"),("6","ebx"), 3129 ("7","edi"),("8","esi"),("9","ebp")]) 3130 val s = Q.INST [`r4`|->`n2w l`] o s 3131 val s = MATCH_MP progTheory.SPEC_FRAME o s 3132 val s = SPEC tm o Q.GEN `c` o Q.SPEC `cond c` o s 3133 val s = MATCH_MP progTheory.SPEC_FRAME o s 3134 val s = Q.SPEC extra o s 3135 val s = MATCH_MP progTheory.SPEC_WEAKEN o s 3136 val th = s th 3137 val th = SPEC post th 3138 val tm = (cdr o car o concl) th 3139 val tac = 3140 SIMP_TAC std_ss [SEP_IMP_MOVE_COND] 3141 THEN REPEAT STRIP_TAC 3142 THEN (STRIP_ASSUME_TAC o UNDISCH_ALL o 3143 REWRITE_RULE [GSYM AND_IMP_INTRO] o 3144 SIMP_RULE std_ss []) imp 3145 THEN ASM_SIMP_TAC std_ss [LET_DEF,aSTRING_def,pSTRING_def,xSTRING_def,SEP_CLAUSES] 3146 THEN REWRITE_TAC [aLISP_def,pLISP_def,xLISP_def] 3147 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_IMP_def,STAR_ASSOC] 3148 THEN SIMP_TAC (std_ss++sep_cond_ss) [] 3149 THEN SIMP_TAC (std_ss) [cond_STAR,SEP_EXISTS] 3150 THEN REPEAT STRIP_TAC 3151 THEN Q.EXISTS_TAC `df` 3152 THEN Q.EXISTS_TAC `f` 3153 THEN AUTO_EXISTS_TAC 3154 THEN FULL_SIMP_TAC std_ss [AC STAR_COMM STAR_ASSOC] 3155 val thi = TAC_PROOF(([], tm),tac) 3156 val th = MP th thi 3157 val th = DISCH_ALL th 3158 val th = SIMP_RULE (std_ss++sep_cond_ss) [progTheory.SPEC_MOVE_COND,AND_IMP_INTRO,SEP_CLAUSES] th 3159 val tm = (cdr o car o concl) th 3160 val tm2 = (cdr o car o concl) imp 3161 val tm3 = mk_imp(tm2,tm) 3162 val tac = 3163 SIMP_TAC std_ss [] 3164 THEN REPEAT STRIP_TAC 3165 THEN (STRIP_ASSUME_TAC o UNDISCH_ALL o 3166 REWRITE_RULE [GSYM AND_IMP_INTRO] o 3167 SIMP_RULE std_ss []) imp 3168 THEN ASM_SIMP_TAC std_ss [] 3169 val thi = prove(tm3,tac) 3170 val th = DISCH_ALL (MP th (UNDISCH thi)) 3171 val th = REWRITE_RULE [GSYM progTheory.SPEC_MOVE_COND] th 3172 val _ = save_thm("arm_string2sexp_" ^ target ^ "_thm",th) 3173 in th end; 3174 3175val th = store_string2sexp_thm "arm" `emp` 3176 ``aLISP (s,Sym "nil",Sym "nil",Sym "nil",Sym "nil",Sym "nil",l) * 3177 ~aR 0x0w * aSTRING r3 (sexp2string s) * aPC p * ~aS`` 3178 3179val th = store_string2sexp_thm "ppc" `~pR 0x2w` 3180 ``pLISP (s,Sym "nil",Sym "nil",Sym "nil",Sym "nil",Sym "nil",l) * 3181 pSTRING r3 (sexp2string s) * pPC p * ~pS`` 3182 3183val th = store_string2sexp_thm "x86" `emp` 3184 ``xLISP (s,Sym "nil",Sym "nil",Sym "nil",Sym "nil",Sym "nil",l) * 3185 xSTRING r3 (sexp2string s) * xPC p * ~xS`` 3186 3187 3188val _ = export_theory(); 3189