1open HolKernel Parse boolLib bossLib; val _ = new_theory "lisp_symbols"; 2open lisp_sexpTheory lisp_consTheory lisp_invTheory; 3 4(* --- *) 5 6open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 7open combinTheory finite_mapTheory addressTheory helperLib; 8open set_sepTheory bitTheory fcpTheory stringTheory; 9 10val wstd_ss = std_ss ++ SIZES_ss ++ rewrites [DECIDE ``n<256 ==> (n:num)<18446744073709551616``,ORD_BOUND]; 11 12open stop_and_copyTheory; 13open codegenLib decompilerLib prog_x64Lib prog_x64Theory progTheory; 14open lisp_parseTheory; 15 16infix \\ 17val op \\ = op THEN; 18val RW = REWRITE_RULE; 19val RW1 = ONCE_REWRITE_RULE; 20fun SUBGOAL q = REVERSE (sg q) 21 22 23val align_blast = blastLib.BBLAST_PROVE 24 ``(a && 3w = 0w) ==> ((a - w && 3w = 0w) = (w && 3w = 0w:word64))`` 25 26val align_add_blast = blastLib.BBLAST_PROVE 27 ``(a && 3w = 0w) ==> ((a + w && 3w = 0w) = (w && 3w = 0w:word64))`` 28 29 30(* lookup 31 32 r11 - pointer to symbol table 33 r0 - used as temp 34 r10 - symbol index 35 36 (assemble "x64" ` 37L1: test r10,r10 38 je L2 39 movzx r0,BYTE [r11] 40 add r11,r0 41 dec r10 42 jmp L1 43L2: `) 44 45*) 46 47val (thm,mc_lookup_def) = decompile_io x64_tools "mc_lookup" 48 (SOME (``(r10:word64,r11:word64,dg:word64 set,g:word64->word8)``, 49 ``(r11:word64,dg:word64 set,g:word64->word8)``)) ` 50 4D85D2 (* L1: test r10,r10 *) 51 48740D (* je L2 *) 52 490FB603/g (* movzx r0,BYTE [r11] *) 53 4901C3 (* add r11,r0 *) 54 49FFCA (* dec r10 *) 55 48EBED (* jmp L1 *) 56 (* L2: *)`; 57 58val mc_lookup_thm = prove( 59 ``!xs a k i p. 60 (LIST_FIND k s xs = SOME (k+i)) /\ i < 2**32 /\ 61 EVERY (\x. LENGTH x < 255) xs /\ 62 (one_byte_list a (symbol_list xs) * p) (fun2set (g,dg)) ==> 63 ?a2 q. mc_lookup_pre (n2w i,a,dg,g) /\ 64 (mc_lookup (n2w i,a,dg,g) = (a2,dg,g)) /\ 65 (one_byte_list a2 (string_data s) * q) (fun2set (g,dg))``, 66 Induct \\ SIMP_TAC std_ss [LIST_FIND_def] \\ REPEAT STRIP_TAC 67 \\ Cases_on `s = h` \\ FULL_SIMP_TAC std_ss [] THEN1 68 (`i = 0` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 69 \\ ONCE_REWRITE_TAC [mc_lookup_def] \\ FULL_SIMP_TAC std_ss [] 70 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [one_symbol_list_def,SEP_CLAUSES, 71 SEP_EXISTS_THM,cond_STAR,symbol_list_def,one_byte_list_APPEND] 72 \\ FULL_SIMP_TAC std_ss [GSYM STAR_ASSOC] \\ METIS_TAC []) 73 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [one_symbol_list_def,SEP_CLAUSES, 74 SEP_EXISTS_THM,cond_STAR,symbol_list_def,RW1[STAR_COMM]one_byte_list_APPEND] 75 \\ ONCE_REWRITE_TAC [mc_lookup_def] \\ FULL_SIMP_TAC std_ss [] 76 \\ `i < 18446744073709551616` by DECIDE_TAC 77 \\ IMP_RES_TAC LIST_FIND_LESS_EQ 78 \\ `~(i = 0)` by DECIDE_TAC 79 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LET_DEF] 80 \\ Cases_on `i` \\ FULL_SIMP_TAC std_ss [] 81 \\ ASM_SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB] 82 \\ FULL_SIMP_TAC std_ss [string_data_def,one_byte_list_def,STAR_ASSOC] 83 \\ SEP_R_TAC 84 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,EVERY_DEF] 85 \\ `(STRLEN h + 1) < 256` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 86 \\ `n < 4294967296` by DECIDE_TAC 87 \\ SEP_I_TAC "mc_lookup" \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `k+1`) 88 \\ FULL_SIMP_TAC std_ss [DECIDE ``k + SUC n = k + 1 + n``] 89 \\ POP_ASSUM MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 90 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_MAP,ADD1] \\ SEP_F_TAC 91 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []); 92 93 94(* string less-than 95 96 r10 - length of str10 97 r11 - length of str11 98 r8 - pointer to str10 99 r9 - pointer to str11 100 r0 - temp and result 101 102 (assemble "x64" ` 103START: cmp r11,0 104 je FALSE 105 cmp r10,0 106 je TRUE 107 movzx r0,BYTE [r8] 108 cmp r0b,BYTE [r9] 109 jb TRUE 110 ja FALSE 111 inc r8 112 inc r9 113 dec r10 114 dec r11 115 jmp START 116FALSE: mov r0d,3 117 jmp EXIT 118TRUE: mov r0d,11 119EXIT:`) 120 121*) 122 123val (thm,mc_string_lt_def) = basic_decompile x64_tools "mc_string_lt" 124 (SOME (``(r10:word64,r11:word64,r8:word64,r9:word64,dg:word64 set,g:word64->word8)``, 125 ``(r0:word64,dg:word64 set,g:word64->word8)``)) ` 126 4983FB00 (* START: cmp r11,0 *) 127 487423 (* je FALSE *) 128 4983FA00 (* cmp r10,0 *) 129 487424 (* je TRUE *) 130 490FB600/g (* movzx r0,BYTE [r8] *) 131 413A01/g (* cmp r0b,BYTE [r9] *) 132 48721A (* jb TRUE *) 133 48770F (* ja FALSE *) 134 49FFC0 (* inc r8 *) 135 49FFC1 (* inc r9 *) 136 49FFCA (* dec r10 *) 137 49FFCB (* dec r11 *) 138 48EBD6 (* jmp START *) 139 B803000000 (* FALSE: mov r0d,3 *) 140 48EB05 (* jmp EXIT *) 141 B80B000000 (* TRUE: mov r0d,11 *) 142 (* EXIT: *)`; 143 144val one_string_def = Define ` 145 one_string a s = one_byte_list a (MAP (n2w o ORD) s)`; 146 147val one_string_CONS = ``one_string a (x::xs)`` 148 |> (SIMP_CONV std_ss [one_string_def,MAP,one_byte_list_def] THENC 149 SIMP_CONV std_ss [GSYM one_string_def]) |> RW1 [STAR_COMM] 150 151val mc_string_lt_lemma = prove( 152 ``!w. (7 -- 0) (w2w (w:word8)):word64 = w2w (w:word8)``, 153 blastLib.BBLAST_TAC); 154 155val mc_string_lt_thm = prove( 156 ``!s2 s1 a1 a2 q1 q2. 157 LENGTH s1 < 255 /\ LENGTH s2 < 255 /\ 158 (one_string a1 s1 * q1) (fun2set (g,dg)) /\ 159 (one_string a2 s2 * q2) (fun2set (g,dg)) ==> 160 mc_string_lt_pre (n2w (LENGTH s1),n2w (LENGTH s2),a1,a2,dg,g) /\ 161 (mc_string_lt (n2w (LENGTH s1),n2w (LENGTH s2),a1,a2,dg,g) = 162 (if s1 < s2 then 11w else 3w,dg,g))``, 163 Induct THEN1 164 (Cases \\ SIMP_TAC std_ss [string_lt_def,LENGTH] 165 \\ ONCE_REWRITE_TAC [mc_string_lt_def] \\ ASM_SIMP_TAC std_ss [LET_DEF]) 166 \\ Cases_on `s1` THEN1 167 (SIMP_TAC std_ss [string_lt_def,LENGTH,ADD1] 168 \\ ONCE_REWRITE_TAC [mc_string_lt_def] \\ ASM_SIMP_TAC std_ss [LET_DEF] 169 \\ REPEAT STRIP_TAC 170 \\ `(STRLEN s2 + 1) < 18446744073709551616` by DECIDE_TAC 171 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11]) 172 \\ SIMP_TAC std_ss [string_lt_def] \\ NTAC 6 STRIP_TAC 173 \\ FULL_SIMP_TAC std_ss [one_string_CONS,GSYM STAR_ASSOC,LENGTH] 174 \\ IMP_RES_TAC (DECIDE ``SUC n < 255 ==> n < 255 /\ n+1 < 18446744073709551616``) 175 \\ ONCE_REWRITE_TAC [mc_string_lt_def] 176 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [ADD1,n2w_11,LET_DEF] 177 \\ SEP_R_TAC 178 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_SUB] 179 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [mc_string_lt_lemma] 180 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,n2w_11,word_lo_n2w] 181 \\ `ORD h < 256 /\ ORD h' < 256` by ASM_SIMP_TAC std_ss [ORD_BOUND] 182 \\ IMP_RES_TAC (DECIDE ``n < 256 ==> n < 18446744073709551616``) 183 \\ ASM_SIMP_TAC std_ss [char_lt_def,GSYM ORD_11] \\ METIS_TAC []); 184 185(* symbol-< 186 187 (assemble "x64" ` 188 mov r11,[r7-224] 189 shr r8,3 190 mov r10,r8 191 insert mc_lookup 192 mov r8,r11 193 shr r9,3 194 mov r10,r9 195 mov r11,[r7-224] 196 insert mc_lookup 197 mov r9,r11 198 movzx r10,BYTE [r8] 199 movzx r11,BYTE [r9] 200 dec r10 201 dec r11 202 inc r8 203 inc r9 204 insert mc_string_lt 205 mov r8,r0 206 mov r0d,3 207 mov r9,r0 208 mov r10,r0 209 mov r11,r0 210 `) 211 212*) 213 214val (mc_symbol_less_spec,mc_symbol_less_def) = basic_decompile x64_tools "mc_symbol_less" 215 (SOME (``(r8:word64,r9:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 216 ``(r0:word64,r8:word64,r9:word64,r10:word64,r11:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) ` 217 4C8B9F20FFFFFF (* mov r11,[r7-224] *) 218 49C1E803 (* shr r8,3 *) 219 4D8BD0 (* mov r10,r8 *) 220 insert:mc_lookup 221 4D8BC3 (* mov r8,r11 *) 222 49C1E903 (* shr r9,3 *) 223 4D8BD1 (* mov r10,r9 *) 224 4C8B9F20FFFFFF (* mov r11,[r7-224] *) 225 insert:mc_lookup 226 4D8BCB (* mov r9,r11 *) 227 4D0FB610/g (* movzx r10,BYTE [r8] *) 228 4D0FB619/g (* movzx r11,BYTE [r9] *) 229 49FFCA (* dec r10 *) 230 49FFCB (* dec r11 *) 231 49FFC0 (* inc r8 *) 232 49FFC1 (* inc r9 *) 233 insert:mc_string_lt 234 4C8BC0 (* mov r8,r0 *) 235 B803000000 (* mov r0d,3 *) 236 4C8BC8 (* mov r9,r0 *) 237 4C8BD0 (* mov r10,r0 *) 238 4C8BD8 (* mov r11,r0 *)` 239 240val _ = save_thm("mc_symbol_less_spec",mc_symbol_less_spec); 241 242val mc_symbol_less_blast = prove( 243 ``!w. ((w2w (w2w (w:29 word) << 3 !! 0x3w:word32) >>> 3):word64 = w2w w) /\ 244 (((sp - 0xE0w && 0x3w) = 0x0w) = (sp && 0x3w = 0x0w:word64)) /\ 245 (((sp - 0xDCw && 0x3w) = 0x0w) = (sp && 0x3w = 0x0w:word64))``, 246 blastLib.BBLAST_TAC); 247 248val FORALL_EXISTS = METIS_PROVE [] ``(!x. P x ==> Q) = ((?x. P x) ==> Q)`` 249val IMP_IMP = METIS_PROVE [] ``b /\ (c ==> d) ==> ((b ==> c) ==> d)`` 250 251val LIST_FIND_MEM = prove( 252 ``!s a k l. (LIST_FIND k a s = SOME l) ==> MEM a s``, 253 Induct \\ SIMP_TAC std_ss [LIST_FIND_def] \\ REPEAT STRIP_TAC 254 \\ Cases_on `a = h` \\ FULL_SIMP_TAC std_ss [MEM] \\ METIS_TAC []); 255 256val LISP = lisp_inv_def |> SPEC_ALL |> concl |> dest_eq |> fst; 257val REST = LISP |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr; 258val STAT = LISP |> car |> car |> cdr; 259val VAR_REST = LISP |> car |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr; 260 261val lisp_inv_NIL = lisp_inv_Sym 262 |> CONJUNCTS |> hd |> UNDISCH |> CONJUNCTS |> hd |> DISCH_ALL |> GEN_ALL; 263 264val lisp_inv_T = save_thm("lisp_inv_T",lisp_inv_Sym 265 |> CONJUNCTS |> tl |> hd |> UNDISCH |> CONJUNCTS |> hd |> DISCH_ALL |> GEN_ALL); 266 267val mc_symbol_less_thm = store_thm("mc_symbol_less_thm", 268 ``lisp_inv ^STAT (x0,x1,x2,x3,x4,x5,^VAR_REST) 269 (w0,w1,w2,w3,w4,w5,df,f,^REST) ==> isSym x0 /\ isSym x1 ==> 270 ?fi w0i w1i w2i w3i. 271 mc_symbol_less_pre (w2w w0,w2w w1,sp,df,f,dg,g) /\ 272 (mc_symbol_less (w2w w0,w2w w1,sp,df,f,dg,g) = (tw0,w2w w0i,w2w w1i,w2w w2i,w2w w3i,sp,df,fi,dg,g)) /\ 273 lisp_inv ^STAT (LISP_SYMBOL_LESS x0 x1,Sym "NIL",Sym "NIL",Sym "NIL",x4,x5,^VAR_REST) 274 (w0i,w1i,w2i,w3i,w4,w5,df,fi,^REST)``, 275 SIMP_TAC std_ss [AND_IMP_INTRO] 276 \\ MATCH_MP_TAC (METIS_PROVE [] ``(b1 ==> b1 /\ b2 /\ b3 ==> b4) ==> (b1 /\ b2 /\ b3 ==> b4)``) 277 \\ STRIP_TAC \\ SIMP_TAC std_ss [Once lisp_inv_def] 278 \\ SIMP_TAC std_ss [isSym_thm,mc_symbol_less_def] \\ STRIP_TAC 279 \\ ASM_SIMP_TAC std_ss [LISP_SYMBOL_LESS_def,getSym_def] 280 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,MAP,CONS_11,lisp_x_def] 281 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (MP_TAC o GSYM) 282 \\ Q.PAT_X_ASSUM `ref_heap_addr s1 = w1` (MP_TAC o GSYM) 283 \\ ASM_SIMP_TAC std_ss [ref_heap_addr_def,INSERT_SUBSET,EMPTY_SUBSET] 284 \\ `(w2w (f (sp - 0xDCw)) << 32 !! w2w (f (sp - 0xE0w)) = sa1) /\ 285 sp - 0xDCw IN df /\ sp - 0xE0w IN df` by 286 (FULL_SIMP_TAC std_ss [lisp_inv_def,ref_full_stack_def,ref_static_def,APPEND] 287 \\ FULL_SIMP_TAC std_ss [LET_DEF,word64_3232_def,word_arith_lemma3,STAR_ASSOC,SEP_CLAUSES] 288 \\ SEP_R_TAC \\ blastLib.BBLAST_TAC) 289 \\ ASM_SIMP_TAC std_ss [mc_symbol_less_blast] 290 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,LET_DEF] 291 (* lookup1 *) 292 \\ ASSUME_TAC ((GEN_ALL o RW [ADD_CLAUSES] o Q.INST [`k`|->`0`] o SPEC_ALL) mc_lookup_thm) 293 \\ SEP_I_TAC "mc_lookup" 294 \\ POP_ASSUM (MP_TAC o Q.SPECL [`INIT_SYMBOLS ++ sym`,`a`]) 295 \\ ASM_SIMP_TAC std_ss [FORALL_EXISTS] 296 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 297 (FULL_SIMP_TAC std_ss [symtable_inv_def,one_symbol_list_def, 298 one_byte_list_APPEND,SEP_EXISTS_THM,cond_STAR] 299 \\ Q.EXISTS_TAC `one_byte_list 300 (sa1 + n2w (LENGTH (symbol_list (INIT_SYMBOLS ++ sym)))) ys` 301 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC) 302 \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 303 (* lookup2 *) 304 \\ ASSUME_TAC ((GEN_ALL o RW [ADD_CLAUSES] o Q.INST [`k`|->`0`] o SPEC_ALL) mc_lookup_thm) 305 \\ SEP_I_TAC "mc_lookup" 306 \\ POP_ASSUM (MP_TAC o Q.SPECL [`INIT_SYMBOLS ++ sym`,`a'`]) 307 \\ ASM_SIMP_TAC std_ss [FORALL_EXISTS] 308 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 309 (FULL_SIMP_TAC std_ss [symtable_inv_def,one_symbol_list_def, 310 one_byte_list_APPEND,SEP_EXISTS_THM,cond_STAR] 311 \\ Q.EXISTS_TAC `one_byte_list 312 (sa1 + n2w (LENGTH (symbol_list (INIT_SYMBOLS ++ sym)))) ys` 313 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC) 314 \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 315 (* string_lt *) 316 \\ FULL_SIMP_TAC std_ss [string_data_def,one_byte_list_def] 317 \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [GSYM one_string_def] 318 \\ `STRLEN a < 255 /\ STRLEN a' < 255` by 319 (FULL_SIMP_TAC std_ss [symtable_inv_def,one_symbol_list_def, 320 one_byte_list_APPEND,SEP_EXISTS_THM,cond_STAR] 321 \\ IMP_RES_TAC LIST_FIND_MEM \\ FULL_SIMP_TAC std_ss [EVERY_MEM]) 322 \\ IMP_RES_TAC (DECIDE ``n<255 ==> n+1<256``) 323 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w] 324 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_SUB] 325 \\ ASSUME_TAC (GEN_ALL mc_string_lt_thm) 326 \\ SEP_I_TAC "mc_string_lt" \\ POP_ASSUM MP_TAC 327 \\ ASM_SIMP_TAC std_ss [FORALL_EXISTS] 328 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 329 (Q.EXISTS_TAC `one (a2',n2w (STRLEN a) + 0x1w) * q` 330 \\ Q.EXISTS_TAC `one (a2'',n2w (STRLEN a') + 0x1w) * q'` 331 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 332 \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 333 \\ Q.LIST_EXISTS_TAC [`if a < a' then 0xBw else 0x3w`,`3w`,`3w`,`3w`] 334 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC 335 THEN1 (Cases_on `a < a'` \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 336 \\ MATCH_MP_TAC lisp_inv_swap1 337 \\ MATCH_MP_TAC lisp_inv_NIL \\ Q.LIST_EXISTS_TAC [`x1`,`w1`] 338 \\ MATCH_MP_TAC lisp_inv_swap1 339 \\ MATCH_MP_TAC lisp_inv_swap2 340 \\ MATCH_MP_TAC lisp_inv_NIL \\ Q.LIST_EXISTS_TAC [`x2`,`w2`] 341 \\ MATCH_MP_TAC lisp_inv_swap2 342 \\ MATCH_MP_TAC lisp_inv_swap3 343 \\ MATCH_MP_TAC lisp_inv_NIL \\ Q.LIST_EXISTS_TAC [`x3`,`w3`] 344 \\ MATCH_MP_TAC lisp_inv_swap3 345 \\ Cases_on `a < a'` \\ FULL_SIMP_TAC std_ss [LISP_TEST_def] 346 THEN1 (MATCH_MP_TAC lisp_inv_T \\ Q.LIST_EXISTS_TAC [`x0`,`w0`] 347 \\ FULL_SIMP_TAC std_ss []) 348 THEN1 (MATCH_MP_TAC lisp_inv_NIL \\ Q.LIST_EXISTS_TAC [`x0`,`w0`] 349 \\ FULL_SIMP_TAC std_ss [])); 350 351 352(* helper function *) 353 354fun make_code_set code = let 355 fun take 0 xs = [] | take n xs = hd xs :: take (n-1) xs 356 fun drop 0 xs = xs | drop n xs = drop (n-1) xs 357 fun split s = if s = "" then [] else 358 substring(s,0,2) :: split (substring(s,2,size(s)-2)); 359 val ns = map (map (Arbnum.toInt o Arbnum.fromHexString)) (map split code) 360 fun mk_byte n = wordsSyntax.mk_n2w(numSyntax.term_of_int n,``:8``) 361 fun listw x = listSyntax.mk_list(map mk_byte x,``:word8``) 362 fun foo n w = subst [mk_var("n",``:num``)|->numSyntax.term_of_int n, 363 mk_var("xs",``:word8 list``)|->w] 364 ``(p + (n2w n):word64,xs:word8 list)`` 365 fun foos n [] = pred_setSyntax.mk_empty(type_of (foo 0 (listw (hd ns)))) 366 | foos n (w::ws) = pred_setSyntax.mk_insert(foo n (listw w),foos (n+length w) ws) 367 fun post_pc n [] = (fst (dest_pair (foo n (listw (hd ns)))),n) 368 | post_pc n (w::ws) = post_pc (n+length w) ws 369 in (foos 0 ns, post_pc 0 ns) end; 370 371 372(* reading and writing io *) 373 374val IO_READ_def = Define ` 375 (IO_READ (IO_STREAMS [] ys) = ~0w:word64) /\ 376 (IO_READ (IO_STREAMS (x::xs) ys) = n2w (ORD x))`; 377 378val IO_NEXT_def = Define ` 379 (IO_NEXT (IO_STREAMS [] ys) = IO_STREAMS [] ys) /\ 380 (IO_NEXT (IO_STREAMS (x::xs) ys) = IO_STREAMS xs ys)`; 381 382val IO_WRITE_def = Define ` 383 IO_WRITE (IO_STREAMS xs ys) zs = IO_STREAMS xs (ys ++ zs)`; 384 385val IO_STATS_def = Define ` 386 IO_STATS (n:num) (IO_STREAMS xs ys) = (IO_STREAMS xs ys)`; 387 388val REPLACE_INPUT_IO_def = Define ` 389 REPLACE_INPUT_IO x (IO_STREAMS xs ys) = IO_STREAMS x ys`; 390 391val getINPUT_def = Define ` 392 getINPUT (IO_STREAMS xs ys) = xs`; 393 394val IO_INPUT_APPLY_def = Define ` 395 IO_INPUT_APPLY f io = REPLACE_INPUT_IO (f (getINPUT io)) io`; 396 397val IO_INPUT_LEMMA = store_thm("IO_INPUT_LEMMA", 398 ``(IO_READ (REPLACE_INPUT_IO (w::ws) io) = n2w (ORD w)) /\ 399 (IO_NEXT (REPLACE_INPUT_IO (w::ws) io) = REPLACE_INPUT_IO ws io) /\ 400 (IO_READ (REPLACE_INPUT_IO [] io) = ~0w) /\ 401 (REPLACE_INPUT_IO (getINPUT io) io = io)``, 402 Cases_on `io` \\ SIMP_TAC std_ss [REPLACE_INPUT_IO_def,IO_READ_def,IO_NEXT_def,getINPUT_def]); 403 404val IO_WRITE_APPEND = store_thm("IO_WRITE_APPEND", 405 ``!io x1 x2. IO_WRITE (IO_WRITE io x1) x2 = IO_WRITE io (x1 ++ x2)``, 406 Cases \\ ASM_SIMP_TAC std_ss [IO_WRITE_def,APPEND_ASSOC,MAP_APPEND]); 407 408val zIO_def = Define ` 409 zIO (iow:word64,ior:word64,iod:word64,ioi:word64) (io:io_streams) = zR 2w 3w`; 410 411val zIO_R_def = Define ` 412 zIO_R (iow,ior,iod) io = SEP_EXISTS ioi. zR 1w ioi * zIO (iow,ior,iod,ioi) io`; 413 414val null_term_str_def = Define ` 415 null_term_str a df f str = 416 ?p. (one_string a (str ++ [CHR 0]) * p) (fun2set (f,df)) /\ 417 EVERY (\x. ~(x = CHR 0)) str`; 418 419val exists_null_term_str_def = Define ` 420 exists_null_term_str a df f = ?str. null_term_str a df f str`; 421 422val mem2string_def = Define ` 423 mem2string a df f = @str. null_term_str a df f str`; 424 425 426(* IO assumpiptions *) 427 428val IO = mk_var("IO",``:bool[64] # bool[64] # bool[64] # bool[64] -> 429 io_streams -> x64_set -> bool``); 430 431val IOR = ``\(iow,ior,iod) io. SEP_EXISTS ioi. zR 1w ioi * ^IO (iow,ior,iod,ioi) io`` 432 433val (read_code,(read_post_pc,read_code_len)) = make_code_set 434 (assemble "x64" ` 435 movzx r0, BYTE [r1] 436 test r0,r0 437 jne SKIP 438 call r2 439 movzx r0, BYTE [r1] 440 test r0,r0 441 jne SKIP 442 xor r0,r0 443 not r0 444SKIP:`) 445 446val io_read_tm = 447 ``SPEC X64_MODEL 448 (zPC p * zR 0x0w r0 * zR 0x2w r2 * ^IOR (x,r2,y) io * ~zS) 449 ^read_code 450 (let r0 = IO_READ io in 451 (zPC ^read_post_pc * zR 0x0w r0 * zR 0x2w r2 * ^IOR (x,r2,y) io * ~zS))``; 452 453(* IO_NEXT *) 454 455val (next_code,(next_post_pc,next_code_len)) = make_code_set 456 (assemble "x64" ` 457 inc r1 458 `) 459 460val io_next_tm = 461 ``SPEC X64_MODEL 462 (zPC p * zR 0x2w r2 * ^IOR (x,r2,y) io * ~zS) 463 ^next_code 464 (let io = IO_NEXT io in (zPC ^next_post_pc * zR 0x2w r2 * ^IOR (x,r2,y) io * ~zS))``; 465 466(* IO_WRITE *) 467 468val (write_code,(write_post_pc,write_code_len)) = make_code_set 469 (assemble "x64" ` 470 call r1 471 `) 472 473val io_write_tm = 474 ``SPEC X64_MODEL 475 (zPC p * zR 0w r0 * zR 0x1w r1 * ^IO (ior,x,y,z) io * zBYTE_MEMORY dg g * ~zS * 476 cond (exists_null_term_str r0 dg g /\ (ior = r1))) 477 ^write_code 478 (let io = IO_WRITE io (mem2string r0 dg g) in 479 (zPC ^write_post_pc * zR 0w r0 * zR 0x1w r1 * ^IO (ior,x,y,z) io * ~zS * zBYTE_MEMORY dg g))``; 480 481(* IO_STATS *) 482 483val (stats_code,(stats_post_pc,stats_code_len)) = make_code_set 484 (assemble "x64" ` 485 call r1 486 `) 487 488val io_stats_tm = 489 ``SPEC X64_MODEL 490 (zPC p * zR 0x1w r1 * zR 0x7w r7 * ^IO (ior,iow,iod,ioi) io * ~zS * cond (iod = r1)) 491 ^stats_code 492 (let io = IO_STATS (w2n r7) io in 493 (zPC ^stats_post_pc * zR 0x1w r1 * zR 0x7w r7 * ^IO (ior,iow,iod,ioi) io * ~zS))``; 494 495(* definition of IO assertions *) 496 497fun genall tm v = foldr mk_forall tm (filter (fn x => not (x = v)) (free_vars tm)); 498 499val io_assums_def = Define ` 500 io_assums ^IO = ^(genall io_stats_tm IO) /\ 501 ^(genall io_write_tm IO) /\ 502 ^(genall io_read_tm IO) /\ 503 ^(genall io_next_tm IO)`; 504 505val zIO_def = Define ` 506 zIO (iow,ior,iod,ioi) io = 507 SEP_EXISTS IO. ^IO (iow,ior,iod,ioi) io * cond (io_assums ^IO)`; 508 509val zIO_R_def = Define ` 510 zIO_R (iow,ior,iod) io = 511 SEP_EXISTS ioi. zR 0x1w ioi * zIO (iow,ior,iod,ioi) io`; 512 513val SPEC_EXISTS_EXISTS = store_thm("SPEC_EXISTS_EXISTS", 514 ``(!x. SPEC m (P x) c (Q x)) ==> SPEC m (SEP_EXISTS x. P x) c (SEP_EXISTS x. Q x)``, 515 SIMP_TAC std_ss [GSYM progTheory.SPEC_PRE_EXISTS] 516 \\ REPEAT STRIP_TAC \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `x`) 517 \\ IMP_RES_TAC progTheory.SPEC_WEAKEN 518 \\ POP_ASSUM MATCH_MP_TAC 519 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] \\ METIS_TAC []); 520 521val ff = subst [IO |-> ``zIO``, 522 IOR |-> ``zIO_R``] 523 524val zIO_R_THM = prove( 525 ``zIO_R (iow,ior,iod) io = 526 SEP_EXISTS IO. ^IOR (iow,ior,iod) io * cond (io_assums IO)``, 527 SIMP_TAC std_ss [zIO_def,zIO_R_def,SEP_CLAUSES,STAR_ASSOC] 528 \\ SIMP_TAC std_ss [FUN_EQ_THM,SEP_EXISTS_THM] 529 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ METIS_TAC []); 530 531val zIO_STATS = prove(ff io_stats_tm, 532 SIMP_TAC std_ss [zIO_def,SEP_CLAUSES,LET_DEF] 533 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS 534 \\ REPEAT STRIP_TAC \\ Cases_on `io_assums IO` 535 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,progTheory.SPEC_FALSE_PRE] 536 \\ FULL_SIMP_TAC std_ss [io_assums_def,LET_DEF]); 537 538val zIO_WRITE = prove(ff io_write_tm, 539 SIMP_TAC std_ss [zIO_def,SEP_CLAUSES,LET_DEF] 540 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS 541 \\ REPEAT STRIP_TAC \\ Cases_on `io_assums IO` 542 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,progTheory.SPEC_FALSE_PRE] 543 \\ FULL_SIMP_TAC std_ss [io_assums_def,LET_DEF]); 544 545val zIO_READ = prove(ff io_read_tm, 546 SIMP_TAC std_ss [zIO_R_THM,SEP_CLAUSES,LET_DEF] 547 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS 548 \\ REPEAT STRIP_TAC \\ Cases_on `io_assums IO` 549 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,progTheory.SPEC_FALSE_PRE] 550 \\ FULL_SIMP_TAC std_ss [io_assums_def,LET_DEF,SEP_CLAUSES]); 551 552val zIO_NEXT = prove(ff io_next_tm, 553 SIMP_TAC std_ss [zIO_R_THM,SEP_CLAUSES,LET_DEF] 554 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS 555 \\ REPEAT STRIP_TAC \\ Cases_on `io_assums IO` 556 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,progTheory.SPEC_FALSE_PRE] 557 \\ FULL_SIMP_TAC std_ss [io_assums_def,LET_DEF,SEP_CLAUSES]); 558 559val _ = add_decompiled("io_next",zIO_NEXT,next_code_len,SOME next_code_len); 560val _ = add_decompiled("io_read",zIO_READ,read_code_len,SOME read_code_len); 561val _ = add_decompiled("io_write",zIO_WRITE,write_code_len,SOME write_code_len); 562val _ = add_decompiled("io_stats",zIO_STATS,stats_code_len,SOME stats_code_len); 563 564 565(* read until newline character *) 566 567val (thm,mc_read_until_newline_def) = basic_decompile_strings x64_tools "mc_read_until_newline" 568 (SOME (``(io:io_streams)``, 569 ``(io:io_streams)``)) 570 (assemble "x64" ` 571START: 572 insert io_read 573 cmp r0,255 574 ja EXIT 575 cmp r0,10 576 je EXIT 577 insert io_next 578 jmp START 579EXIT:`) 580 581val SND_read_while = prove( 582 ``!zs s P. SND (read_while P zs s) = SND (read_while P zs "")``, 583 Induct \\ SIMP_TAC std_ss [read_while_def] \\ REPEAT STRIP_TAC 584 \\ Cases_on `P h` \\ ASM_SIMP_TAC std_ss []); 585 586val mc_read_until_newline_thm = prove( 587 ``!zs io. 588 mc_read_until_newline_pre (REPLACE_INPUT_IO zs io) /\ 589 (mc_read_until_newline (REPLACE_INPUT_IO zs io) = 590 REPLACE_INPUT_IO (SND (read_while (\x. x <> #"\n") zs "")) io)``, 591 Induct \\ ONCE_REWRITE_TAC [mc_read_until_newline_def] 592 \\ SIMP_TAC std_ss [MAP,LET_DEF,IO_INPUT_LEMMA,APPEND,EVAL ``~0w:word64``] 593 \\ ASM_SIMP_TAC wstd_ss [word_lo_n2w,read_while_def] \\ REPEAT STRIP_TAC 594 \\ `ORD h < 256` by FULL_SIMP_TAC std_ss [ORD_BOUND] 595 \\ `~(255 < ORD h)` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 596 \\ Cases_on `h = #"\n"` \\ ASM_SIMP_TAC std_ss [EVAL ``ORD #"\n"``] 597 \\ `~(ORD h = 10)` by 598 (ONCE_REWRITE_TAC [GSYM (EVAL ``ORD #"\n"``)] \\ FULL_SIMP_TAC std_ss [ORD_11]) 599 \\ FULL_SIMP_TAC wstd_ss [n2w_11] 600 \\ ONCE_REWRITE_TAC [SND_read_while] \\ FULL_SIMP_TAC std_ss []); 601 602 603(* read space chars -- test for end of file *) 604 605val (mc_test_eof_spec,mc_test_eof_def) = basic_decompile_strings x64_tools "mc_test_eof" 606 (SOME (``io:io_streams``, 607 ``(r0:word64,r8:word64,io:io_streams)``)) 608 (assemble "x64" ` 609START: 610 insert io_read 611 cmp r0,32 612 ja NOT_SPACE 613 insert io_next 614 jmp START 615NOT_SPACE: 616 cmp r0,255 617 ja TRUE 618 cmp r0,59 619 je COMMENT 620 mov r8d,3 621 jmp EXIT 622COMMENT: 623 mov r0d,0 624 insert io_next 625 insert mc_read_until_newline 626 mov r0d,0 627 jmp START 628TRUE: 629 mov r8d,11 630EXIT: 631 mov r0d,3 632 `); 633 634val _ = save_thm("mc_test_eof_spec",mc_test_eof_spec); 635 636val mc_test_eof_lemma = prove( 637 ``!cs. 638 mc_test_eof_pre (REPLACE_INPUT_IO (cs) io) /\ 639 (mc_test_eof (REPLACE_INPUT_IO (cs) io) = 640 (3w,if FST (is_eof cs) then 11w else 3w, 641 REPLACE_INPUT_IO (SND (is_eof cs)) io))``, 642 HO_MATCH_MP_TAC is_eof_ind \\ STRIP_TAC THEN1 643 (ONCE_REWRITE_TAC [mc_test_eof_def] 644 \\ SIMP_TAC std_ss [MAP,MAP,IO_INPUT_LEMMA,LET_DEF] \\ EVAL_TAC) 645 \\ NTAC 3 STRIP_TAC \\ Cases_on `space_char c` \\ FULL_SIMP_TAC std_ss [] 646 \\ ONCE_REWRITE_TAC [mc_test_eof_def] 647 \\ ONCE_REWRITE_TAC [is_eof_def] 648 \\ SIMP_TAC std_ss [MAP,IO_INPUT_LEMMA,LET_DEF] 649 \\ SIMP_TAC wstd_ss [w2w_def,w2n_n2w,word_lo_n2w,space_char_def,GSYM NOT_LESS] 650 \\ FULL_SIMP_TAC std_ss [space_char_def,DECIDE ``32 < n = ~(n <= 32)``] 651 \\ `ORD c < 256` by FULL_SIMP_TAC std_ss [ORD_BOUND] 652 \\ `~(255 < ORD c)` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 653 \\ Cases_on `c = #";"` 654 \\ FULL_SIMP_TAC std_ss [mc_read_until_newline_thm, EVAL ``ORD #";"``] 655 \\ Cases_on `c` 656 \\ FULL_SIMP_TAC wstd_ss [ORD_CHR_RWT,n2w_11,CHR_11]); 657 658val MAP_MAP_LEMMA = prove( 659 ``!xs. MAP (n2w o ORD) (MAP (CHR o w2n) xs) = xs:word8 list``, 660 Induct \\ ASM_SIMP_TAC std_ss [MAP,CONS_11] 661 \\ Cases \\ FULL_SIMP_TAC wstd_ss [w2n_n2w,ORD_CHR_RWT]); 662 663val getINPUT_EQ_NIL = prove( 664 ``!io. (f (getINPUT io) = "") = 665 (getINPUT (IO_INPUT_APPLY f io) = [])``, 666 Cases \\ SIMP_TAC std_ss [getINPUT_def,IO_INPUT_APPLY_def, 667 REPLACE_INPUT_IO_def,MAP_EQ_NIL]); 668 669val mc_test_eof_thm = prove( 670 ``^LISP ==> 671 ?v0 io2. 672 mc_test_eof_pre io /\ 673 (mc_test_eof io = (tw0,w2w v0,io2)) /\ 674 (io2 = IO_INPUT_APPLY (SND o is_eof) io) /\ 675 let (io,w0,x0) = (io2,v0,LISP_TEST (FST (is_eof (getINPUT io)))) in ^LISP``, 676 SIMP_TAC std_ss [RW [IO_INPUT_LEMMA,GSYM IO_INPUT_APPLY_def,MAP_MAP_LEMMA] (Q.SPEC `((getINPUT io))` mc_test_eof_lemma)] 677 \\ SIMP_TAC std_ss [IO_INPUT_APPLY_def,LET_DEF] \\ STRIP_TAC 678 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 679 \\ Cases_on `FST (is_eof (getINPUT io))` \\ FULL_SIMP_TAC std_ss [] 680 THEN1 681 (Q.EXISTS_TAC `0xBw` \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,LISP_TEST_def] 682 \\ METIS_TAC [el 2 (CONJUNCTS lisp_inv_Sym),lisp_inv_ignore_io]) 683 THEN1 684 (Q.EXISTS_TAC `0x3w` \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,LISP_TEST_def] 685 \\ METIS_TAC [el 1 (CONJUNCTS lisp_inv_Sym),lisp_inv_ignore_io])); 686 687val _ = save_thm("mc_test_eof_thm",mc_test_eof_thm); 688 689 690(* read number *) 691 692val (thm,mc_read_num_def) = basic_decompile_strings x64_tools "mc_read_num" 693 (SOME (``(r8:word64,io:io_streams)``, 694 ``(r8:word64,io:io_streams)``)) 695 (assemble "x64" ` 696START: 697 insert io_read 698 cmp r0,57 699 ja EXIT 700 cmp r0,48 701 jb EXIT 702 insert io_next 703 sub r0,48 704 xchg r8,r0 705 lea r0,[4*r0+r0] 706 add r0,r0 707 xchg r8,r0 708 add r8,r0 709 cmp r8,1073741824 710 jb START 711 xor r8,r8 712 not r8 713 jmp START 714EXIT: 715 `) 716 717val PUSH_IF = METIS_PROVE [] 718 ``((if b then mc_read_num (x1,y) else mc_read_num (x2,y)) = 719 mc_read_num (if b then x1 else x2,y)) /\ 720 ((if b then mc_read_num_pre (x1,y) else mc_read_num_pre (x2,y)) = 721 mc_read_num_pre (if b then x1 else x2,y))`` 722 723val mc_read_num_lemma = prove( 724 ``!cs cs2 n. 725 EVERY number_char cs /\ (~(cs2 = []) ==> (~number_char (HD cs2))) ==> 726 mc_read_num_pre (if n < 2**30 then (n2w n) else ~0w, 727 REPLACE_INPUT_IO ((cs ++ cs2)) io) /\ 728 (mc_read_num (if n < 2**30 then (n2w n) else ~0w, 729 REPLACE_INPUT_IO ((cs ++ cs2)) io) = 730 (if 10**(LENGTH cs) * n + str2num cs < 2**30 then 731 n2w (10**(LENGTH cs) * n + str2num cs) else ~0w, 732 REPLACE_INPUT_IO (cs2) io))``, 733 Induct THEN1 734 (SIMP_TAC std_ss [LENGTH,str2num_def,APPEND] \\ Cases 735 \\ ONCE_REWRITE_TAC [mc_read_num_def] THEN1 736 (SIMP_TAC std_ss [MAP,LET_DEF,IO_INPUT_LEMMA] 737 \\ SIMP_TAC std_ss [IO_INPUT_LEMMA,LET_DEF,EVAL ``~0w:word64``] 738 \\ SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w]) 739 \\ SIMP_TAC std_ss [MAP,LET_DEF,IO_INPUT_LEMMA] 740 \\ `ORD h < 256` by METIS_TAC [ORD_BOUND] 741 \\ `ORD h < 18446744073709551616` by DECIDE_TAC 742 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,word_lo_n2w,number_char_def] 743 \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL,HD] 744 \\ SIMP_TAC std_ss [LESS_EQ,ADD1] 745 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 746 \\ Cases_on `58 <= ORD h` \\ ASM_SIMP_TAC std_ss [] 747 \\ Cases_on `ORD h + 1 <= 48` \\ ASM_SIMP_TAC std_ss [] 748 \\ `F` by DECIDE_TAC) 749 \\ SIMP_TAC std_ss [read_while_def,LET_DEF,LENGTH,str2num_def,MAP] 750 \\ ONCE_REWRITE_TAC [mc_read_num_def] 751 \\ SIMP_TAC std_ss [IO_INPUT_LEMMA,LET_DEF] 752 \\ ASM_SIMP_TAC std_ss [MAP,IO_INPUT_LEMMA,APPEND] 753 \\ STRIP_TAC 754 \\ `ORD h < 256` by METIS_TAC [ORD_BOUND] 755 \\ `ORD h < 18446744073709551616` by DECIDE_TAC 756 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,word_lo_n2w,number_char_def,EVERY_DEF] 757 \\ NTAC 3 STRIP_TAC 758 \\ `~(57 < ORD h)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 759 \\ `~(ORD h < 48)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 760 \\ ASM_SIMP_TAC std_ss [word_mul_n2w,word_add_n2w,DECIDE ``4*n+n+(4*n+n)=10*n``] 761 \\ ASM_SIMP_TAC std_ss [word_arith_lemma2,word_add_n2w] 762 \\ REVERSE (Cases_on `n < 1073741824`) THEN1 763 (ASM_SIMP_TAC std_ss [EVAL ``~0w:word64``,word_mul_n2w,word_add_n2w] 764 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,word_lo_n2w] 765 \\ ONCE_REWRITE_TAC [MATCH_MP (GSYM MOD_PLUS) (DECIDE ``0 < 18446744073709551616:num``)] 766 \\ SIMP_TAC std_ss [] 767 \\ `(ORD h - 48) < 18446744073709551616` by DECIDE_TAC 768 \\ `(18446744073709551606 + (ORD h - 48)) < 18446744073709551616` by DECIDE_TAC 769 \\ `~(18446744073709551606 + (ORD h - 48) < 1073741824)` by DECIDE_TAC 770 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [number_char_def] 771 \\ FULL_SIMP_TAC std_ss [EVAL ``~0w:word64``] 772 \\ RES_TAC \\ REPEAT (POP_ASSUM (MP_TAC o Q.SPEC`n`)) 773 \\ Q.PAT_X_ASSUM `!csss. bbb` (K ALL_TAC) 774 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 775 \\ SIMP_TAC std_ss [EXP] 776 \\ Cases_on `(10:num) ** (LENGTH cs)` \\ ASM_SIMP_TAC std_ss [] 777 \\ FULL_SIMP_TAC std_ss [MULT_CLAUSES] 778 \\ `~(n' * n + n + str2num cs < 1073741824)` by DECIDE_TAC 779 \\ FULL_SIMP_TAC std_ss [RIGHT_ADD_DISTRIB] 780 \\ SRW_TAC [] [] 781 \\ FULL_SIMP_TAC std_ss [DECIDE ``10*n=n+9*n``,GSYM ADD_ASSOC] 782 \\ IMP_RES_TAC (DECIDE ``n+m<k==>n<k:num``)) 783 \\ ASM_SIMP_TAC std_ss [] 784 \\ SIMP_TAC std_ss [word_mul_n2w,word_add_n2w,DECIDE ``4*n+n+(4*n+n)=10*n``] 785 \\ `(10 * n + (ORD h - 48)) < 18446744073709551616` by DECIDE_TAC 786 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,PUSH_IF] 787 \\ FULL_SIMP_TAC std_ss [number_char_def] 788 \\ SIMP_TAC std_ss [EXP,LEFT_ADD_DISTRIB] 789 \\ SIMP_TAC std_ss [AC MULT_ASSOC MULT_COMM,AC ADD_ASSOC ADD_COMM]); 790 791val ORD_BOUND_LEMMA = prove( 792 ``ORD h < 1073741872``, 793 METIS_TAC [DECIDE ``256 < 1073741872:num``,ORD_BOUND,LESS_TRANS]); 794 795val mc_read_num_thm = mc_read_num_lemma 796 |> Q.SPECL [`cs1`,`cs2`,`ORD h - 48`] 797 |> SIMP_RULE std_ss [RW1[MULT_COMM](GSYM str2num_def)] 798 |> SIMP_RULE std_ss [ORD_BOUND_LEMMA] |> GEN_ALL 799 800val mc_read_num_thm0 = mc_read_num_lemma 801 |> Q.SPECL [`cs1`,`cs2`,`0`] |> SIMP_RULE std_ss [] 802 803val read_while_SPLIT_lemma = prove( 804 ``!xs ys P. 805 EVERY P ys ==> 806 ?xs1 xs2. (read_while P xs ys = (xs1,xs2)) /\ (ys ++ xs = xs1 ++ xs2) /\ 807 EVERY P xs1 /\ (xs2 <> "" ==> ~P (HD xs2))``, 808 Induct \\ SIMP_TAC std_ss [read_while_def,APPEND,EVERY_DEF] \\ REPEAT STRIP_TAC 809 \\ Cases_on `P h` \\ ASM_SIMP_TAC std_ss [] THEN1 810 (`EVERY P (ys ++ [h])` by ASM_SIMP_TAC std_ss [EVERY_APPEND,EVERY_DEF] 811 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND]) 812 \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL,HD]); 813 814val read_while_SPLIT = read_while_SPLIT_lemma 815 |> Q.SPECL [`xs`,`[]`] |> RW [EVERY_DEF] |> Q.GEN `xs`; 816 817 818(* read symbol *) 819 820val (thm,mc_read_barsym_0_def) = basic_decompile_strings x64_tools "mc_read_barsym_0" 821 (SOME (``(r0:word64)``, 822 ``(r0:word64)``)) 823 (assemble "x64" ` 824 cmp r0,48 825 jne EXIT 826 xor r0d,r0d 827EXIT: 828 `) 829 830val (thm,mc_read_barsym_def) = basic_decompile_strings x64_tools "mc_read_barsym" 831 (SOME (``(r9:word64,r10:word64,r15:word64,io:io_streams,dg:word64 set,g:word64->word8)``, 832 ``(r9:word64,r15:word64,io:io_streams,dg:word64 set,g:word64->word8)``)) 833 (assemble "x64" ` 834START: 835 insert io_read 836 cmp r0,255 837 ja EXIT 838 insert io_next 839 test r10,r10 840 jne SKIP 841 cmp r0,124 842 je EXIT 843 not r10 844 cmp r0,92 845 je START 846 mov [r9+r15],r0b 847 inc r15 848 not r10 849 cmp r15,254 850 jna START 851 jmp EXIT 852SKIP: 853 insert mc_read_barsym_0 854 mov [r9+r15],r0b 855 inc r15 856 not r10 857 cmp r15,254 858 jna START 859EXIT: 860 `) 861 862val mc_read_barsym_thm = prove( 863 ``!cs b cs1 cs2 r15 r15i g p xs. 864 (str2sym_aux cs b = (cs1,cs2)) /\ 865 LENGTH cs1 + w2n r15 < 255 /\ (LENGTH xs = LENGTH cs1) ==> 866 (one_string (r9+r15) xs * p) (fun2set (g,dg)) ==> 867 ?g2 cs3 r15i. 868 mc_read_barsym_pre (r9,if b then ~0w else 0w,r15,REPLACE_INPUT_IO (cs) io,dg,g) /\ 869 (mc_read_barsym (r9,if b then ~0w else 0w,r15,REPLACE_INPUT_IO (cs) io,dg,g) = 870 (r9,r15 + n2w (LENGTH cs1),REPLACE_INPUT_IO (cs2) io,dg,g2)) /\ 871 (one_string (r9+r15) cs1 * p) (fun2set (g2,dg))``, 872 Induct \\ SIMP_TAC std_ss [MAP] THEN1 873 (ONCE_REWRITE_TAC [mc_read_barsym_def] 874 \\ SIMP_TAC std_ss [IO_INPUT_LEMMA,LET_DEF,EVAL ``0xFFw <+ ~0x0w:word64``] 875 \\ SIMP_TAC std_ss [str2sym_aux_def,LENGTH,MAP,WORD_ADD_0,LENGTH_NIL]) 876 \\ ONCE_REWRITE_TAC [mc_read_barsym_def] 877 \\ SIMP_TAC wstd_ss [IO_INPUT_LEMMA,LET_DEF,w2w_def,w2n_n2w,word_lo_n2w] 878 \\ STRIP_TAC \\ `ORD h < 256` by FULL_SIMP_TAC wstd_ss [] 879 \\ `~(255 < ORD h)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 880 \\ Cases \\ ASM_SIMP_TAC wstd_ss [n2w_11,EVAL ``~0w = 0w:word64``] THEN1 881 (SIMP_TAC std_ss [str2sym_aux_def] 882 \\ `?x1 x2. str2sym_aux cs F = (x1,x2)` by METIS_TAC [PAIR] 883 \\ ASM_SIMP_TAC std_ss [LET_DEF,LENGTH,WORD_NOT_NOT] 884 \\ NTAC 5 STRIP_TAC 885 \\ `~(0xFEw <+ r15 + 0x1w) /\ STRLEN x1 + w2n (r15 + 0x1w) < 255` by 886 (NTAC 4 (POP_ASSUM MP_TAC) \\ Q.SPEC_TAC (`r15`,`w`) \\ Cases 887 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w,word_add_n2w,word_lo_n2w,LENGTH] 888 \\ REPEAT STRIP_TAC \\ `n + 1 < 256` by DECIDE_TAC 889 \\ FULL_SIMP_TAC wstd_ss [] \\ DECIDE_TAC) 890 \\ ASM_SIMP_TAC std_ss [] 891 \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 892 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] 893 \\ Q.PAT_X_ASSUM `!b.bbb` (MP_TAC o Q.SPEC `F`) 894 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 895 \\ FULL_SIMP_TAC std_ss [one_string_def,one_byte_list_def,MAP] 896 \\ Q.ABBREV_TAC `g6 = (r15 + r9 =+ n2w (w2n (mc_read_barsym_0 (n2w (ORD h))))) g` 897 \\ `(one (r9 + r15,n2w (w2n (mc_read_barsym_0 (n2w (ORD h))))) * 898 one_byte_list (r9 + r15 + 0x1w) (MAP (n2w o ORD) t) * p) 899 (fun2set (g6,dg)) /\ r15 + r9 IN dg` by 900 (Q.UNABBREV_TAC `g6` \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 901 \\ SEP_I_TAC "mc_read_barsym" 902 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * one (r9 + r15,n2w (w2n (mc_read_barsym_0 (n2w (ORD h)))))`,`t`]) 903 \\ `w2n (mc_read_barsym_0 (n2w (ORD h))) = ORD (if h = #"0" then #"\^@" else h)` by 904 (SIMP_TAC wstd_ss [mc_read_barsym_0_def,LET_DEF,n2w_11] 905 \\ Cases_on `h` \\ ASM_SIMP_TAC std_ss [ORD_CHR_RWT,CHR_11] 906 \\ Cases_on `n = 48` \\ ASM_SIMP_TAC wstd_ss [ORD_CHR_RWT,w2n_n2w]) 907 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_ADD_COMM WORD_ADD_ASSOC,GSYM word_add_n2w]) 908 \\ SIMP_TAC std_ss [str2sym_aux_def] 909 \\ Cases_on `h` \\ ASM_SIMP_TAC std_ss [CHR_11,ORD_CHR_RWT,WORD_NOT_NOT] 910 \\ Cases_on `n = 92` \\ ASM_SIMP_TAC std_ss [] THEN1 911 (Q.PAT_X_ASSUM `!b.bbb` (MP_TAC o Q.SPEC `T`) 912 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC) 913 \\ Cases_on `n = 124` \\ ASM_SIMP_TAC std_ss [] 914 THEN1 SIMP_TAC std_ss [LENGTH,LENGTH_NIL,WORD_ADD_0] 915 \\ `?x1 x2. str2sym_aux cs F = (x1,x2)` by METIS_TAC [PAIR] 916 \\ ASM_SIMP_TAC std_ss [LET_DEF,LENGTH,WORD_NOT_NOT] 917 \\ NTAC 5 STRIP_TAC 918 \\ `~(0xFEw <+ r15 + 0x1w) /\ STRLEN x1 + w2n (r15 + 0x1w) < 255` by 919 (NTAC 4 (POP_ASSUM MP_TAC) \\ Q.SPEC_TAC (`r15`,`w`) \\ Cases 920 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w,word_add_n2w,word_lo_n2w,LENGTH] 921 \\ REPEAT STRIP_TAC \\ `n' + 1 < 255` by DECIDE_TAC 922 \\ `(n' + 1) < 18446744073709551616` by DECIDE_TAC 923 \\ FULL_SIMP_TAC wstd_ss [] \\ DECIDE_TAC) 924 \\ ASM_SIMP_TAC std_ss [] 925 \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 926 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] 927 \\ Q.PAT_X_ASSUM `!b.bbb` (MP_TAC o Q.SPEC `F`) 928 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 929 \\ FULL_SIMP_TAC std_ss [one_string_def,one_byte_list_def,MAP] 930 \\ Q.ABBREV_TAC `g6 = (r15 + r9 =+ n2w n) g` 931 \\ `(one (r9 + r15,n2w n) * 932 one_byte_list (r9 + r15 + 0x1w) (MAP (n2w o ORD) t) * p) 933 (fun2set (g6,dg)) /\ r15 + r9 IN dg` by 934 (Q.UNABBREV_TAC `g6` \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 935 \\ ASM_SIMP_TAC std_ss [ORD_CHR_RWT] 936 \\ SEP_I_TAC "mc_read_barsym" 937 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * one (r9 + r15,n2w n)`,`t`]) 938 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_ADD_COMM WORD_ADD_ASSOC,GSYM word_add_n2w]); 939 940val mc_read_barsym_overflow_thm = prove( 941 ``!cs b cs1 cs2 r15 g p xs. 942 (str2sym_aux cs b = (cs1,cs2)) /\ 943 (254 <= LENGTH cs1 + w2n r15) /\ 944 (LENGTH xs <= LENGTH cs1) /\ (LENGTH xs = 255 - w2n r15) /\ w2n r15 < 255 ==> 945 (one_string (r9+r15) xs * p) (fun2set (g,dg)) ==> 946 ?g2 io2 xs2. 947 mc_read_barsym_pre (r9,if b then ~0w else 0w,r15,REPLACE_INPUT_IO cs io,dg,g) /\ 948 (mc_read_barsym (r9,if b then ~0w else 0w,r15,REPLACE_INPUT_IO cs io,dg,g) = 949 (r9,255w,io2,dg,g2)) /\ 950 (one_string (r9+r15) xs2 * p) (fun2set (g2,dg)) /\ 951 (LENGTH xs2 = LENGTH xs)``, 952 Induct \\ SIMP_TAC std_ss [MAP] THEN1 953 (SIMP_TAC std_ss [str2sym_aux_def,LENGTH] \\ REPEAT STRIP_TAC 954 \\ `F` by DECIDE_TAC) 955 \\ ONCE_REWRITE_TAC [mc_read_barsym_def] 956 \\ SIMP_TAC wstd_ss [IO_INPUT_LEMMA,LET_DEF,w2w_def,w2n_n2w,word_lo_n2w] 957 \\ STRIP_TAC \\ `ORD h < 256` by FULL_SIMP_TAC wstd_ss [] 958 \\ `~(255 < ORD h)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 959 \\ Cases \\ ASM_SIMP_TAC wstd_ss [n2w_11,EVAL ``~0w = 0w:word64``] THEN1 960 (SIMP_TAC std_ss [str2sym_aux_def] 961 \\ `?x1 x2. str2sym_aux cs F = (x1,x2)` by METIS_TAC [PAIR] 962 \\ ASM_SIMP_TAC std_ss [LET_DEF,LENGTH,WORD_NOT_NOT] 963 \\ NTAC 5 STRIP_TAC 964 \\ ASM_SIMP_TAC std_ss [] 965 \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 966 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] THEN1 (`F` by DECIDE_TAC) 967 \\ FULL_SIMP_TAC std_ss [IO_INPUT_LEMMA,APPEND] 968 \\ ASM_SIMP_TAC wstd_ss [IO_INPUT_LEMMA,LET_DEF,w2w_def,w2n_n2w,word_lo_n2w] 969 \\ Q.PAT_X_ASSUM `!b.bbb` (MP_TAC o Q.SPEC `F`) 970 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 971 \\ FULL_SIMP_TAC std_ss [one_string_def,one_byte_list_def,MAP] 972 \\ Q.ABBREV_TAC `g6 = (r15 + r9 =+ n2w (w2n (mc_read_barsym_0 (n2w (ORD h))))) g` 973 \\ `(one (r9 + r15,n2w (w2n (mc_read_barsym_0 (n2w (ORD h))))) * 974 one_byte_list (r9 + r15 + 0x1w) (MAP (n2w o ORD) t) * p) 975 (fun2set (g6,dg)) /\ r15 + r9 IN dg` by 976 (Q.UNABBREV_TAC `g6` \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 977 \\ `w2n (mc_read_barsym_0 (n2w (ORD h))) = ORD (if h = #"0" then #"\^@" else h)` by 978 (SIMP_TAC wstd_ss [mc_read_barsym_0_def,LET_DEF,n2w_11] 979 \\ Cases_on `h` \\ ASM_SIMP_TAC std_ss [ORD_CHR_RWT,CHR_11] 980 \\ Cases_on `n = 48` \\ ASM_SIMP_TAC wstd_ss [ORD_CHR_RWT,w2n_n2w]) 981 \\ SEP_R_TAC 982 \\ Cases_on `0xFEw <+ r15 + 0x1w` \\ FULL_SIMP_TAC std_ss [] THEN1 983 (Cases_on `r15` \\ FULL_SIMP_TAC wstd_ss [w2n_n2w,word_lo_n2w,word_add_n2w] 984 \\ `n+1 < 18446744073709551616` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 985 \\ `n = 254` by DECIDE_TAC \\ FULL_SIMP_TAC wstd_ss [n2w_11] 986 \\ Q.EXISTS_TAC `(if h = #"0" then #"\^@" else h)::t` 987 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,LENGTH,MAP,word_arith_lemma1]) 988 \\ SEP_I_TAC "mc_read_barsym" 989 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * one (r9 + r15,n2w (w2n (mc_read_barsym_0 (n2w (ORD h)))))`,`t`]) 990 \\ Cases_on `r15` 991 \\ FULL_SIMP_TAC wstd_ss [word_add_n2w,w2n_n2w,word_lo_n2w] 992 \\ `(n + 1) < 18446744073709551616` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 993 \\ FULL_SIMP_TAC wstd_ss [word_add_n2w,w2n_n2w,word_lo_n2w] 994 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 DECIDE_TAC 995 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_ADD_COMM WORD_ADD_ASSOC,GSYM word_add_n2w] 996 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 997 \\ Q.EXISTS_TAC `(if h = #"0" then #"\^@" else h) :: xs2` 998 \\ FULL_SIMP_TAC (std_ss++star_ss) [LENGTH,MAP,one_byte_list_def,WORD_ADD_ASSOC] 999 \\ DECIDE_TAC) 1000 \\ ASM_SIMP_TAC wstd_ss [IO_INPUT_LEMMA,LET_DEF,w2w_def,w2n_n2w,word_lo_n2w,APPEND] 1001 \\ SIMP_TAC std_ss [str2sym_aux_def] 1002 \\ Cases_on `h` \\ ASM_SIMP_TAC std_ss [CHR_11,ORD_CHR_RWT,WORD_NOT_NOT] 1003 \\ Cases_on `n = 92` \\ ASM_SIMP_TAC std_ss [] THEN1 1004 (FULL_SIMP_TAC wstd_ss [n2w_11] 1005 \\ Q.PAT_X_ASSUM `!b.bbb` (MP_TAC o Q.SPEC `T`) 1006 \\ ASM_SIMP_TAC std_ss [LENGTH] \\ REPEAT STRIP_TAC 1007 \\ FULL_SIMP_TAC std_ss [] 1008 \\ Q.PAT_X_ASSUM `!xx.bbb` (MATCH_MP_TAC o RW [AND_IMP_INTRO]) 1009 \\ Q.EXISTS_TAC `xs` \\ FULL_SIMP_TAC std_ss []) 1010 \\ Cases_on `n = 124` \\ ASM_SIMP_TAC std_ss [] THEN1 1011 (SIMP_TAC std_ss [LENGTH,LENGTH_NIL,WORD_ADD_0] 1012 \\ REPEAT STRIP_TAC \\ `F` by DECIDE_TAC) 1013 \\ FULL_SIMP_TAC wstd_ss [n2w_11] 1014 \\ `?x1 x2. str2sym_aux cs F = (x1,x2)` by METIS_TAC [PAIR] 1015 \\ ASM_SIMP_TAC std_ss [LET_DEF,LENGTH,WORD_NOT_NOT] 1016 \\ NTAC 5 STRIP_TAC 1017 \\ ASM_SIMP_TAC std_ss [] 1018 \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] THEN1 (`F` by DECIDE_TAC) 1019 \\ REPEAT STRIP_TAC 1020 \\ FULL_SIMP_TAC std_ss [one_string_def,one_byte_list_def,MAP] 1021 \\ Q.ABBREV_TAC `g6 = (r15 + r9 =+ n2w n) g` 1022 \\ `(one (r9 + r15,n2w n) * 1023 one_byte_list (r9 + r15 + 0x1w) (MAP (n2w o ORD) t) * p) 1024 (fun2set (g6,dg)) /\ r15 + r9 IN dg` by 1025 (Q.UNABBREV_TAC `g6` \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 1026 \\ SEP_R_TAC 1027 \\ Cases_on `0xFEw <+ r15 + 0x1w` \\ FULL_SIMP_TAC std_ss [] THEN1 1028 (Cases_on `r15` \\ FULL_SIMP_TAC wstd_ss [w2n_n2w,word_lo_n2w,word_add_n2w] 1029 \\ `n'+1 < 18446744073709551616` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 1030 \\ `n' = 254` by DECIDE_TAC \\ FULL_SIMP_TAC wstd_ss [n2w_11] 1031 \\ Q.EXISTS_TAC `CHR n::t` 1032 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,LENGTH,MAP,word_arith_lemma1,ORD_CHR_RWT]) 1033 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] 1034 \\ Q.PAT_X_ASSUM `!b.bbb` (MP_TAC o Q.SPEC `F`) 1035 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1036 \\ ASM_SIMP_TAC std_ss [ORD_CHR_RWT] 1037 \\ SEP_I_TAC "mc_read_barsym" 1038 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * one (r9 + r15,n2w n)`,`t`]) 1039 \\ Cases_on `r15` 1040 \\ FULL_SIMP_TAC wstd_ss [word_add_n2w,w2n_n2w,word_lo_n2w] 1041 \\ `(n' + 1) < 18446744073709551616` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 1042 \\ FULL_SIMP_TAC wstd_ss [word_add_n2w,w2n_n2w,word_lo_n2w] 1043 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 DECIDE_TAC 1044 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_ADD_COMM WORD_ADD_ASSOC,GSYM word_add_n2w] 1045 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1046 \\ Q.EXISTS_TAC `CHR n :: xs2` 1047 \\ FULL_SIMP_TAC (std_ss++star_ss) [LENGTH,MAP,one_byte_list_def,WORD_ADD_ASSOC,ORD_CHR_RWT] 1048 \\ DECIDE_TAC); 1049 1050val (thm,mc_read_stdsym_0_def) = basic_decompile_strings x64_tools "mc_read_stdsym_0" 1051 (SOME (``(r0:word64)``, 1052 ``(r0:word64)``)) 1053 (assemble "x64" ` 1054 cmp r0,96 1055 jna EXIT 1056 cmp r0,122 1057 ja EXIT 1058 sub r0,32 1059EXIT: 1060 `) 1061 1062val mc_read_stdsym_0_thm = prove( 1063 ``!c. mc_read_stdsym_0 (n2w (ORD c)) = n2w (ORD (upper_case c))``, 1064 Cases \\ ASM_SIMP_TAC wstd_ss [mc_read_stdsym_0_def,word_lo_n2w, 1065 upper_case_def,LET_DEF,is_lower_case_def,CHR_11,char_le_def,ORD_CHR_RWT] 1066 \\ SIMP_TAC std_ss [LESS_EQ,ADD1] 1067 \\ Cases_on `97 <= n` \\ ASM_SIMP_TAC std_ss [ORD_CHR_RWT] 1068 \\ ASM_SIMP_TAC std_ss [DECIDE ``n <= 122 = ~(123 <= n:num)``] 1069 \\ Cases_on `123 <= n` \\ ASM_SIMP_TAC std_ss [ORD_CHR_RWT] 1070 \\ `~(n < 32) /\ n - 32 < 256` by DECIDE_TAC 1071 \\ ASM_SIMP_TAC std_ss [word_arith_lemma2,ORD_CHR_RWT]); 1072 1073val (thm,mc_read_stdsym_def) = basic_decompile_strings x64_tools "mc_read_stdsym" 1074 (SOME (``(r9:word64,r15:word64,io:io_streams,dg:word64 set,g:word64->word8)``, 1075 ``(r9:word64,r15:word64,io:io_streams,dg:word64 set,g:word64->word8)``)) 1076 (assemble "x64" ` 1077START: 1078 insert io_read 1079 cmp r0,255 1080 ja EXIT 1081 cmp r0,41 1082 jna EXIT 1083 cmp r0,46 1084 je EXIT 1085 cmp r0,59 1086 je EXIT 1087 cmp r0,124 1088 je EXIT 1089 insert io_next 1090 insert mc_read_stdsym_0 1091 mov [r9+r15],r0b 1092 inc r15 1093 cmp r15,254 1094 jna START 1095EXIT: 1096 `) 1097 1098val mc_read_stdsym_thm = prove( 1099 ``!cs cs2 r15 g p xs. 1100 EVERY identifier_char cs /\ (~(cs2 = []) ==> (~identifier_char (HD cs2))) ==> 1101 LENGTH cs + w2n r15 < 255 /\ (LENGTH xs = LENGTH cs) ==> 1102 (one_string (r9+r15) xs * p) (fun2set (g,dg)) ==> 1103 ?g2. 1104 mc_read_stdsym_pre (r9,r15,REPLACE_INPUT_IO ((cs ++ cs2)) io,dg,g) /\ 1105 (mc_read_stdsym (r9,r15,REPLACE_INPUT_IO ((cs ++ cs2)) io,dg,g) = 1106 (r9,r15 + n2w (LENGTH cs),REPLACE_INPUT_IO ((cs2)) io,dg,g2)) /\ 1107 (one_string (r9+r15) (MAP upper_case cs) * p) (fun2set (g2,dg))``, 1108 Induct THEN1 1109 (SIMP_TAC std_ss [LENGTH,LENGTH_NIL,EVERY_DEF] \\ Cases 1110 \\ ASM_SIMP_TAC std_ss [HD,APPEND,MAP] THEN1 1111 (ONCE_REWRITE_TAC [mc_read_stdsym_def] 1112 \\ SIMP_TAC std_ss [IO_INPUT_LEMMA,LET_DEF,EVAL ``0xFFw <+ ~0x0w:word64``] 1113 \\ SIMP_TAC std_ss [WORD_ADD_0] \\ METIS_TAC []) 1114 \\ SIMP_TAC std_ss [NOT_CONS_NIL] 1115 \\ ONCE_REWRITE_TAC [mc_read_stdsym_def] 1116 \\ SIMP_TAC wstd_ss [IO_INPUT_LEMMA,LET_DEF,w2w_def,w2n_n2w,word_lo_n2w,n2w_11] 1117 \\ `ORD h < 256` by FULL_SIMP_TAC wstd_ss [] 1118 \\ `~(255 < ORD h)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 1119 \\ SIMP_TAC std_ss [DECIDE ``41<n=42<=n:num``] 1120 \\ SIMP_TAC std_ss [identifier_char_def] 1121 \\ NTAC 5 STRIP_TAC 1122 \\ ASM_SIMP_TAC std_ss [WORD_ADD_0] \\ METIS_TAC []) 1123 \\ STRIP_TAC 1124 \\ ONCE_REWRITE_TAC [mc_read_stdsym_def] 1125 \\ SIMP_TAC wstd_ss [IO_INPUT_LEMMA,LET_DEF,w2w_def,w2n_n2w,word_lo_n2w,n2w_11,MAP,APPEND] 1126 \\ `ORD h < 256` by FULL_SIMP_TAC wstd_ss [] 1127 \\ `~(255 < ORD h)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 1128 \\ SIMP_TAC std_ss [EVERY_DEF,identifier_char_def] 1129 \\ SIMP_TAC std_ss [DECIDE ``41<n=42<=n:num``] 1130 \\ NTAC 7 STRIP_TAC 1131 \\ `~(0xFEw <+ r15 + 0x1w) /\ STRLEN cs + w2n (r15 + 0x1w) < 255` by 1132 (NTAC 4 (POP_ASSUM MP_TAC) \\ Q.SPEC_TAC (`r15`,`w`) \\ Cases 1133 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w,word_add_n2w,word_lo_n2w,LENGTH] 1134 \\ REPEAT STRIP_TAC \\ `n + 1 < 255 /\ n + 1 < 256` by DECIDE_TAC 1135 \\ FULL_SIMP_TAC wstd_ss [] \\ DECIDE_TAC) 1136 \\ ASM_SIMP_TAC std_ss [] 1137 \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,mc_read_stdsym_0_thm] 1138 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] 1139 \\ Q.ABBREV_TAC `g4 = (r15 + r9 =+ n2w (ORD (upper_case h))) g` 1140 \\ FULL_SIMP_TAC std_ss [one_string_def,MAP,one_byte_list_def] 1141 \\ STRIP_TAC 1142 \\ `(one_byte_list (r9 + r15 + 0x1w) (MAP (n2w o ORD) t) * (p * one (r9 + r15,n2w (ORD (upper_case h))))) 1143 (fun2set (g4,dg)) /\ r15 + r9 IN dg` by 1144 (Q.UNABBREV_TAC `g4` \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 1145 \\ SEP_I_TAC "mc_read_stdsym" 1146 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * one (r9 + r15,n2w (ORD (upper_case h)))`,`t`]) 1147 \\ FULL_SIMP_TAC (std_ss++star_ss) [identifier_char_def,AC WORD_ADD_COMM WORD_ADD_ASSOC,GSYM word_add_n2w]); 1148 1149val mc_read_stdsym_overflow_thm = prove( 1150 ``!cs cs2 r15 g p xs. 1151 EVERY identifier_char cs ==> 1152 (255 <= LENGTH cs + w2n r15) /\ 1153 (LENGTH xs <= LENGTH cs) /\ (LENGTH xs = 255 - w2n r15) /\ w2n r15 < 255 ==> 1154 (one_string (r9+r15) xs * p) (fun2set (g,dg)) ==> 1155 ?g2 io2 xs2. 1156 mc_read_stdsym_pre (r9,r15,REPLACE_INPUT_IO ((cs ++ cs2)) io,dg,g) /\ 1157 (mc_read_stdsym (r9,r15,REPLACE_INPUT_IO ((cs ++ cs2)) io,dg,g) = 1158 (r9,255w,io2,dg,g2)) /\ 1159 (one_string (r9+r15) xs2 * p) (fun2set (g2,dg)) /\ 1160 (LENGTH xs2 = LENGTH xs)``, 1161 Induct THEN1 1162 (SIMP_TAC std_ss [LENGTH,LENGTH_NIL,EVERY_DEF] \\ Cases 1163 \\ FULL_SIMP_TAC std_ss [w2n_n2w,APPEND] 1164 \\ REPEAT STRIP_TAC \\ `F` by DECIDE_TAC) 1165 \\ STRIP_TAC 1166 \\ ONCE_REWRITE_TAC [mc_read_stdsym_def] 1167 \\ SIMP_TAC wstd_ss [IO_INPUT_LEMMA,LET_DEF,w2w_def,w2n_n2w,word_lo_n2w,n2w_11,MAP,APPEND] 1168 \\ `ORD h < 256` by FULL_SIMP_TAC wstd_ss [] 1169 \\ `~(255 < ORD h)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 1170 \\ SIMP_TAC std_ss [EVERY_DEF,identifier_char_def] 1171 \\ SIMP_TAC std_ss [DECIDE ``41<n=42<=n:num``] 1172 \\ NTAC 7 STRIP_TAC 1173 \\ ASM_SIMP_TAC std_ss [] 1174 \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,mc_read_stdsym_0_thm] 1175 THEN1 (`F` by DECIDE_TAC) 1176 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] 1177 \\ Q.ABBREV_TAC `g4 = (r15 + r9 =+ n2w (ORD (upper_case h))) g` 1178 \\ FULL_SIMP_TAC std_ss [one_string_def,MAP,one_byte_list_def] 1179 \\ STRIP_TAC 1180 \\ `(one_byte_list (r9 + r15 + 0x1w) (MAP (n2w o ORD) t) * (p * one (r9 + r15,n2w (ORD (upper_case h))))) 1181 (fun2set (g4,dg)) /\ r15 + r9 IN dg` by 1182 (Q.UNABBREV_TAC `g4` \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 1183 \\ Cases_on `0xFEw <+ r15 + 0x1w` \\ FULL_SIMP_TAC std_ss [] THEN1 1184 (NTAC 10 (POP_ASSUM MP_TAC) \\ Q.SPEC_TAC (`r15`,`w`) \\ Cases 1185 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w,word_add_n2w,word_lo_n2w,LENGTH] 1186 \\ REPEAT STRIP_TAC \\ `n + 1 < 18446744073709551616` by DECIDE_TAC 1187 \\ FULL_SIMP_TAC wstd_ss [] 1188 \\ `n = 254` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 1189 \\ Cases_on `t` \\ Q.EXISTS_TAC `[upper_case h]` 1190 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,one_byte_list_def,SEP_CLAUSES,MAP] 1191 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 1192 \\ SEP_I_TAC "mc_read_stdsym" 1193 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * one (r9 + r15,n2w (ORD (upper_case h)))`,`t`]) 1194 \\ FULL_SIMP_TAC (std_ss++star_ss) [identifier_char_def,AC WORD_ADD_COMM WORD_ADD_ASSOC,GSYM word_add_n2w] 1195 \\ NTAC 10 (POP_ASSUM MP_TAC) \\ Q.SPEC_TAC (`r15`,`w`) \\ Cases 1196 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w,word_add_n2w,word_lo_n2w,LENGTH] 1197 \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 1198 \\ `n + 1 < 18446744073709551616` by DECIDE_TAC 1199 \\ FULL_SIMP_TAC wstd_ss [] 1200 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 DECIDE_TAC 1201 \\ REPEAT STRIP_TAC 1202 \\ FULL_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `upper_case h :: xs2` 1203 \\ FULL_SIMP_TAC (std_ss++star_ss) [LENGTH,MAP,one_byte_list_def,WORD_ADD_ASSOC] 1204 \\ DECIDE_TAC); 1205 1206val (thm,mc_read_sym_def) = basic_decompile_strings x64_tools "mc_read_sym" 1207 (SOME (``(r9:word64,io:io_streams,dg:word64 set,g:word64->word8)``, 1208 ``(r9:word64,r15:word64,io:io_streams,dg:word64 set,g:word64->word8)``)) 1209 (assemble "x64" ` 1210START: 1211 insert io_read 1212 xor r15,r15 1213 cmp r0,124 1214 je BAR 1215 cmp r0,255 1216 ja EXIT 1217 insert mc_read_stdsym_0 1218 mov [r9+r15],r0b 1219 inc r15 1220 insert io_next 1221 insert mc_read_stdsym 1222 jmp EXIT 1223BAR: 1224 insert io_next 1225 xor r10,r10 1226 insert mc_read_barsym 1227EXIT: 1228 `) 1229 1230val mc_read_sym_thm = prove( 1231 ``!cs cs1 cs2 g p xs. 1232 (str2sym cs = (cs1,cs2)) /\ 1233 LENGTH cs1 < 255 /\ (LENGTH xs = LENGTH cs1) ==> 1234 (one_string r9 xs * p) (fun2set (g,dg)) ==> 1235 ?g2 cs3 r15i. 1236 mc_read_sym_pre (r9,REPLACE_INPUT_IO (cs) io,dg,g) /\ 1237 (mc_read_sym (r9,REPLACE_INPUT_IO (cs) io,dg,g) = 1238 (r9,n2w (LENGTH cs1),REPLACE_INPUT_IO (cs2) io,dg,g2)) /\ 1239 (one_string r9 cs1 * p) (fun2set (g2,dg))``, 1240 SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [mc_read_sym_def] 1241 \\ SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 1242 \\ Cases_on `IO_READ (REPLACE_INPUT_IO cs io) = 0x7Cw` 1243 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC THEN1 1244 (Cases_on `cs` \\ FULL_SIMP_TAC wstd_ss [MAP,IO_INPUT_LEMMA,word_1comp_n2w, 1245 n2w_11,str2sym_def,HD,w2w_def,w2n_n2w] 1246 \\ Cases_on `h` \\ FULL_SIMP_TAC wstd_ss [CHR_11,NOT_CONS_NIL,ORD_CHR_RWT,TL] 1247 \\ `?x1 x2. str2sym_aux t F = (x1,x2)` by METIS_TAC [PAIR] 1248 \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ EXPAND_TAC 1249 \\ ASSUME_TAC (GEN_ALL (Q.SPECL [`cs`,`F`,`cs1`,`cs2`,`0w`] mc_read_barsym_thm)) 1250 \\ FULL_SIMP_TAC std_ss [WORD_ADD_0] 1251 \\ SEP_I_TAC "mc_read_barsym" \\ POP_ASSUM MP_TAC 1252 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 1253 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p`,`xs`]) 1254 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w] \\ REPEAT STRIP_TAC 1255 \\ ASM_SIMP_TAC std_ss []) 1256 \\ Cases_on `cs` THEN1 1257 (FULL_SIMP_TAC std_ss [MAP,IO_INPUT_LEMMA,EVAL ``0xFFw <+ ~0x0w:word64``,EVAL ``str2sym ""``] 1258 \\ EXPAND_TAC \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_NIL,MAP] \\ METIS_TAC []) 1259 \\ STRIP_ASSUME_TAC (Q.SPEC `identifier_char` (Q.ISPEC `t:string` read_while_SPLIT)) 1260 \\ `~(0xFFw <+ IO_READ (REPLACE_INPUT_IO ((STRING h t)) io))` by 1261 (FULL_SIMP_TAC wstd_ss [MAP,IO_INPUT_LEMMA,w2w_def,w2n_n2w,word_lo_n2w] 1262 \\ FULL_SIMP_TAC wstd_ss [DECIDE ``~(255<n) = (n<256)``]) 1263 \\ ASM_SIMP_TAC std_ss [] 1264 \\ FULL_SIMP_TAC wstd_ss [MAP,IO_INPUT_LEMMA,w2w_def,w2n_n2w,word_lo_n2w,WORD_ADD_0] 1265 \\ `str2sym (h::t) = (MAP upper_case (h::xs1),xs2)` by 1266 (Cases_on `h` 1267 \\ Q.PAT_X_ASSUM `bbb = (cs1,cs2)` MP_TAC 1268 \\ FULL_SIMP_TAC wstd_ss [str2sym_def,HD,NOT_CONS_NIL,LET_DEF,MAP,IO_INPUT_LEMMA, 1269 w2w_def,w2n_n2w,n2w_11,CHR_11,ORD_CHR_RWT]) 1270 \\ FULL_SIMP_TAC std_ss [APPEND] \\ EXPAND_TAC 1271 \\ FULL_SIMP_TAC std_ss [LENGTH_MAP,MAP,LENGTH] 1272 \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 1273 \\ ASSUME_TAC (GEN_ALL (Q.SPECL [`cs1`,`cs2`,`1w`] mc_read_stdsym_thm)) 1274 \\ FULL_SIMP_TAC std_ss [WORD_ADD_0,LENGTH_MAP] 1275 \\ SEP_I_TAC "mc_read_stdsym" \\ POP_ASSUM MP_TAC 1276 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 1277 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * one_string r9 [upper_case h]`,`t'`]) 1278 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w] 1279 \\ MATCH_MP_TAC (METIS_PROVE [] ``b /\ (c ==> d) ==> ((b ==> c) ==> d)``) 1280 \\ STRIP_TAC THEN1 1281 (FULL_SIMP_TAC wstd_ss [one_string_def,one_byte_list_def,MAP,SEP_CLAUSES, 1282 mc_read_stdsym_0_thm,w2n_n2w] \\ SEP_WRITE_TAC) 1283 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def,one_byte_list_def,SEP_CLAUSES,MAP] 1284 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w] \\ REPEAT STRIP_TAC 1285 \\ ASM_SIMP_TAC std_ss [] 1286 \\ FULL_SIMP_TAC std_ss [word_add_n2w,AC ADD_ASSOC ADD_COMM] 1287 \\ SEP_R_TAC); 1288 1289val mc_read_sym_overflow_thm = prove( 1290 ``!cs cs1 cs2 g p xs. 1291 (str2sym cs = (cs1,cs2)) /\ 1292 255 <= LENGTH cs1 /\ (LENGTH xs = 255) ==> 1293 (one_string r9 xs * p) (fun2set (g,dg)) ==> 1294 ?g2 io2 xs2. 1295 mc_read_sym_pre (r9,REPLACE_INPUT_IO (cs) io,dg,g) /\ 1296 (mc_read_sym (r9,REPLACE_INPUT_IO (cs) io,dg,g) = 1297 (r9,255w,io2,dg,g2)) /\ 1298 (one_string r9 xs2 * p) (fun2set (g2,dg)) /\ 1299 (LENGTH xs = LENGTH xs2)``, 1300 SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [mc_read_sym_def] 1301 \\ SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 1302 \\ Cases_on `IO_READ (REPLACE_INPUT_IO cs io) = 0x7Cw` 1303 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC THEN1 1304 (CONV_TAC (DEPTH_CONV PairRules.PBETA_CONV) 1305 \\ Cases_on `cs` \\ FULL_SIMP_TAC wstd_ss [MAP,IO_INPUT_LEMMA,word_1comp_n2w, 1306 n2w_11,str2sym_def,HD,w2w_def,w2n_n2w] 1307 \\ Cases_on `h` \\ FULL_SIMP_TAC wstd_ss [CHR_11,NOT_CONS_NIL,ORD_CHR_RWT,TL] 1308 \\ `?x1 x2. str2sym_aux t F = (x1,x2)` by METIS_TAC [PAIR] 1309 \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ EXPAND_TAC 1310 \\ ASSUME_TAC (GEN_ALL (Q.SPECL [`cs`,`F`,`cs1`,`cs2`,`0w`] mc_read_barsym_overflow_thm)) 1311 \\ FULL_SIMP_TAC std_ss [WORD_ADD_0] 1312 \\ SEP_I_TAC "mc_read_barsym" \\ POP_ASSUM MP_TAC 1313 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 1314 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p`,`xs`]) 1315 \\ `255 <= STRLEN x1` by DECIDE_TAC 1316 \\ `254 <= STRLEN x1` by DECIDE_TAC 1317 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w] \\ REPEAT STRIP_TAC 1318 \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `xs2` \\ FULL_SIMP_TAC std_ss []) 1319 \\ Cases_on `cs` THEN1 1320 (FULL_SIMP_TAC std_ss [MAP,IO_INPUT_LEMMA,EVAL ``0xFFw <+ ~0x0w:word64``,EVAL ``str2sym ""``] 1321 \\ EXPAND_TAC \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_NIL,MAP] \\ METIS_TAC []) 1322 \\ STRIP_ASSUME_TAC (Q.SPEC `identifier_char` (Q.ISPEC `t:string` read_while_SPLIT)) 1323 \\ `~(0xFFw <+ IO_READ (REPLACE_INPUT_IO ((STRING h t)) io))` by 1324 (FULL_SIMP_TAC wstd_ss [MAP,IO_INPUT_LEMMA,w2w_def,w2n_n2w,word_lo_n2w] 1325 \\ FULL_SIMP_TAC wstd_ss [DECIDE ``~(255<n) = (n<256)``]) 1326 \\ ASM_SIMP_TAC std_ss [] 1327 \\ FULL_SIMP_TAC wstd_ss [MAP,IO_INPUT_LEMMA,w2w_def,w2n_n2w,word_lo_n2w,WORD_ADD_0] 1328 \\ `str2sym (h::t) = (MAP upper_case (h::xs1),xs2)` by 1329 (Cases_on `h` 1330 \\ Q.PAT_X_ASSUM `bbb = (cs1,cs2)` MP_TAC 1331 \\ FULL_SIMP_TAC wstd_ss [str2sym_def,HD,NOT_CONS_NIL,LET_DEF,MAP,IO_INPUT_LEMMA, 1332 w2w_def,w2n_n2w,n2w_11,CHR_11,ORD_CHR_RWT]) 1333 \\ FULL_SIMP_TAC std_ss [APPEND] \\ EXPAND_TAC 1334 \\ FULL_SIMP_TAC std_ss [LENGTH_MAP,MAP,LENGTH] 1335 \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 1336 \\ ASSUME_TAC (GEN_ALL (Q.SPECL [`cs1`,`cs2`,`1w`] mc_read_stdsym_overflow_thm)) 1337 \\ FULL_SIMP_TAC std_ss [WORD_ADD_0,LENGTH_MAP] 1338 \\ SEP_I_TAC "mc_read_stdsym" \\ POP_ASSUM MP_TAC 1339 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 1340 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * one_string r9 [upper_case h]`,`t'`]) 1341 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w] 1342 \\ MATCH_MP_TAC (METIS_PROVE [] ``b /\ (c ==> d) ==> ((b ==> c) ==> d)``) 1343 \\ STRIP_TAC THEN1 DECIDE_TAC 1344 \\ MATCH_MP_TAC (METIS_PROVE [] ``b /\ (c ==> d) ==> ((b ==> c) ==> d)``) 1345 \\ STRIP_TAC THEN1 1346 (FULL_SIMP_TAC wstd_ss [one_string_def,one_byte_list_def,MAP,SEP_CLAUSES, 1347 mc_read_stdsym_0_thm,w2n_n2w] \\ SEP_WRITE_TAC) 1348 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def,one_byte_list_def,SEP_CLAUSES,MAP] 1349 \\ ASM_SIMP_TAC wstd_ss [w2n_n2w] \\ REPEAT STRIP_TAC 1350 \\ ASM_SIMP_TAC std_ss [] 1351 \\ FULL_SIMP_TAC std_ss [word_add_n2w,AC ADD_ASSOC ADD_COMM] 1352 \\ SEP_R_TAC \\ Q.EXISTS_TAC `upper_case h::xs2'` \\ FULL_SIMP_TAC std_ss [] 1353 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def,one_byte_list_def,SEP_CLAUSES,MAP,LENGTH]); 1354 1355 1356(* string eq for insert symbol (below) *) 1357 1358val (thm,mc_string_eq_def) = basic_decompile_strings x64_tools "mc_string_eq" 1359 (SOME (``(r8:word64,r9:word64,r11:word64,dg:word64 set,g:word64->word8)``, 1360 ``(r0:word64,r8:word64,r9:word64,dg:word64 set,g:word64->word8)``)) 1361 (assemble "x64" ` 1362START: 1363 test r11,r11 1364 je TRUE 1365 movzx r0,BYTE [r8+r11] 1366 cmp r0b,BYTE [r9+r11] 1367 jne FALSE 1368 dec r11 1369 jmp START 1370TRUE: 1371 xor r0,r0 1372 jmp EXIT 1373FALSE: 1374 mov r0d,1 1375EXIT: `) 1376 1377val mc_string_eq_blast = blastLib.BBLAST_PROVE 1378 ``!w. w2w ((w2w (w:word8)):word64) = w`` 1379 1380val APPEND_11_LEMMA = prove( 1381 ``!s1 t1 s2 t2. 1382 (LENGTH s1 = LENGTH t1) ==> ((s1 ++ s2 = t1 ++ t2) = (s1 = t1) /\ (s2 = t2))``, 1383 Induct \\ Cases_on `t1` \\ FULL_SIMP_TAC std_ss [APPEND,LENGTH,ADD1,CONS_11] 1384 \\ METIS_TAC []); 1385 1386val mc_string_eq_thm = prove( 1387 ``!s t p. 1388 (LENGTH s = LENGTH t) /\ LENGTH t < 256 /\ 1389 (one_string (a+1w) s * one_string (b+1w) t * p) (fun2set (g,dg)) ==> 1390 mc_string_eq_pre (a,b,n2w (LENGTH t),dg,g) /\ 1391 (mc_string_eq (a,b,n2w (LENGTH t),dg,g) = 1392 ((if s = t then 0w else 1w),a,b,dg,g))``, 1393 HO_MATCH_MP_TAC rich_listTheory.SNOC_INDUCT \\ NTAC 3 STRIP_TAC 1394 THEN1 (Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,LENGTH_SNOC] 1395 \\ ONCE_REWRITE_TAC [mc_string_eq_def] \\ SIMP_TAC std_ss [LET_DEF]) 1396 \\ NTAC 3 STRIP_TAC 1397 \\ `(t = []) \/ ?h2 tt. t = SNOC h2 tt` by METIS_TAC [rich_listTheory.SNOC_CASES] 1398 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,LENGTH_SNOC] 1399 \\ FULL_SIMP_TAC std_ss [SNOC_APPEND] 1400 \\ FULL_SIMP_TAC std_ss [one_string_def,one_byte_list_def,MAP,MAP_APPEND, 1401 APPEND,one_byte_list_APPEND,SEP_CLAUSES,STAR_ASSOC] 1402 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def,LENGTH_MAP,word_arith_lemma1] 1403 \\ STRIP_TAC 1404 \\ ONCE_REWRITE_TAC [mc_string_eq_def] \\ SIMP_TAC std_ss [LET_DEF] 1405 \\ `(LENGTH tt + 1) < 18446744073709551616` by DECIDE_TAC 1406 \\ ASM_SIMP_TAC wstd_ss [n2w_11,CONS_11] 1407 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_SUB,mc_string_eq_blast] 1408 \\ SIMP_TAC std_ss [word_add_n2w] 1409 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,AC ADD_ASSOC ADD_COMM] 1410 \\ Q.PAT_X_ASSUM `LENGTH s = LENGTH tt` ASSUME_TAC \\ FULL_SIMP_TAC std_ss [] 1411 \\ SEP_R_TAC \\ ASM_SIMP_TAC wstd_ss [n2w_11,ORD_11] 1412 \\ FULL_SIMP_TAC std_ss [APPEND_11_LEMMA,CONS_11] 1413 \\ Cases_on `x = h2` \\ FULL_SIMP_TAC std_ss [] 1414 \\ Q.PAT_X_ASSUM `!t.bbb` MATCH_MP_TAC 1415 \\ Q.EXISTS_TAC `one (a + n2w (STRLEN tt + 1),n2w (ORD h2)) * 1416 one (b + n2w (STRLEN tt + 1),n2w (ORD h2)) * p` 1417 \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ DECIDE_TAC); 1418 1419 1420(* insert symbol *) 1421 1422val (thm,mc_insert_sym_def) = basic_decompile_strings x64_tools "mc_insert_sym" 1423 (SOME (``(r7:word64,r8:word64,r9:word64,r10:word64,r15:word64,dg:word64 set,g:word64->word8,df:word64 set,f:word64->word32)``, 1424 ``(r7:word64,r8:word64,r9:word64,dg:word64 set,g:word64->word8,df:word64 set,f:word64->word32)``)) 1425 (assemble "x64" ` 1426START: 1427 movzx r11, BYTE [r8] 1428 test r11,r11 1429 je INSERT 1430 cmp r15,r11 1431 je EQ 1432 add r8,r11 1433 inc r10 1434 jmp START 1435EQ: 1436 dec r11 1437 insert mc_string_eq 1438 test r0,r0 1439 je FOUND 1440 add r8,r15 1441 inc r10 1442 jmp START 1443INSERT: 1444 cmp r15,254 1445 ja ERROR 1446 mov r0,[r7-208] 1447 sub r0,[r7-216] 1448 sub r0,r15 1449 cmp r0,520 1450 jna ERROR2 1451 cmp r10,536870910 1452 ja ERROR2 1453 mov BYTE [r8],r15b 1454 mov BYTE [r8+r15],0 1455 mov r0,[r7-216] 1456 add r0,r15 1457 mov [r7-216],r0 1458FOUND: 1459 mov r8,r10 1460 shl r8,3 1461 or r8,3 1462 mov r9d,1 1463 jmp EXIT 1464ERROR2: 1465 mov r8d,29 1466 mov r9d,3 1467 jmp EXIT 1468ERROR: 1469 mov r8d,25 1470 mov r9d,3 1471EXIT: `) 1472 1473val mc_insert_sym_lemma1 = prove( 1474 ``!xs n k p a. 1475 (LIST_FIND n s xs = SOME k) /\ EVERY (\x. STRLEN x < 255) xs /\ LENGTH s < 256 /\ 1476 (one_byte_list a (symbol_list xs) * one_string (r9+1w) s * p) (fun2set (g,dg)) ==> 1477 mc_insert_sym_pre (r7,a,r9,n2w n,n2w (LENGTH s + 1),dg,g,df,f) /\ 1478 (mc_insert_sym (r7,a,r9,n2w n,n2w (LENGTH s + 1),dg,g,df,f) = (r7,n2w k << 3 !! 3w,1w,dg,g,df,f))``, 1479 Induct \\ SIMP_TAC std_ss [LIST_FIND_def] 1480 \\ SIMP_TAC std_ss [symbol_list_def,string_data_def,one_byte_list_def, 1481 one_byte_list_APPEND,LENGTH,LENGTH_MAP,ADD1] 1482 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def,EVERY_DEF] 1483 \\ NTAC 6 STRIP_TAC 1484 \\ ONCE_REWRITE_TAC [mc_insert_sym_def] 1485 \\ SIMP_TAC std_ss [LET_DEF] 1486 \\ SEP_R_TAC 1487 \\ `LENGTH h + 1 < 256` by DECIDE_TAC 1488 \\ `LENGTH s + 1 < 18446744073709551616` by DECIDE_TAC 1489 \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,n2w_11] 1490 \\ ASM_SIMP_TAC wstd_ss [GSYM word_add_n2w,WORD_ADD_SUB] 1491 \\ SIMP_TAC std_ss [word_add_n2w] 1492 \\ REVERSE (Cases_on `LENGTH s = LENGTH h`) \\ FULL_SIMP_TAC std_ss [] THEN1 1493 (Q.PAT_X_ASSUM `!x.bb` MATCH_MP_TAC 1494 \\ Cases_on `s = h` \\ FULL_SIMP_TAC std_ss [] 1495 \\ Q.EXISTS_TAC `one (a,n2w (STRLEN h + 1)) * one_string (a + 0x1w) h * p` 1496 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 1497 \\ ASSUME_TAC (GEN_ALL (Q.SPECL [`s1`,`s2`] mc_string_eq_thm)) 1498 \\ Q.PAT_X_ASSUM `STRLEN s = STRLEN h` (ASSUME_TAC o GSYM) 1499 \\ FULL_SIMP_TAC std_ss [] \\ SEP_I_TAC "mc_string_eq" 1500 \\ POP_ASSUM (MP_TAC o Q.SPECL [`h`,`one (a,n2w (STRLEN h + 1)) * 1501 one_byte_list (a + n2w (STRLEN h + 1)) (symbol_list xs) * p`]) 1502 \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ STRIP_TAC 1503 \\ REVERSE (Cases_on `h = s`) \\ FULL_SIMP_TAC wstd_ss [n2w_11] THEN1 1504 (Q.PAT_X_ASSUM `!x.bb` MATCH_MP_TAC 1505 \\ Q.EXISTS_TAC `one (a,n2w (STRLEN h + 1)) * one_string (a + 0x1w) h * p` 1506 \\ FULL_SIMP_TAC (std_ss++star_ss) [])); 1507 1508val mc_insert_sym_lemma2_blast = blastLib.BBLAST_PROVE 1509 ``(w2w ((w2w (w >>> 32)):word32) << 32 !! w2w ((w2w (w:word64)):word32) = w) /\ 1510 ((63 >< 32) w = (w2w (w >>> 32)):word32) /\ ((31 >< 0) w = (w2w w):word32)``; 1511 1512val mc_insert_sym_lemma2 = prove( 1513 ``!xs n k p a x r9. 1514 Abbrev (r9 = a + n2w (LENGTH (symbol_list xs)) - 1w) /\ (r7 && 3w = 0w) /\ 1515 (LIST_FIND n s xs = NONE) /\ EVERY (\x. STRLEN x < 255) xs /\ LENGTH s < 256 /\ 1516 (ref_static (r7 - 0xD8w) [sa2;sa3] * q) (fun2set (f,df)) /\ 1517 (one_byte_list a (symbol_list xs) * one_string (r9+1w) s * one (r9+1w+n2w(LENGTH s),x) * p) (fun2set (g,dg)) ==> 1518 ?fail g2 f2 toosmall. 1519 mc_insert_sym_pre (r7,a,r9,n2w n,n2w (LENGTH s + 1),dg,g,df,f) /\ 1520 (mc_insert_sym (r7,a,r9,n2w n,n2w (LENGTH s + 1),dg,g,df,f) = 1521 if fail then (r7,if toosmall then 25w else 29w,3w,dg,g,df,f) else 1522 (r7,n2w (n+LENGTH xs) << 3 !! 3w,1w,dg,g2,df,f2)) /\ 1523 (~fail ==> 0x208w <+ sa3 - sa2 - n2w (STRLEN s + 1) /\ 1524 ~(536870910w <+ (n2w (n + LENGTH xs):word64)) /\ 1525 (ref_static (r7 - 0xD8w) [sa2+n2w (LENGTH s + 1);sa3] * q) (fun2set (f2,df)) /\ 1526 (one_byte_list a (symbol_list (xs ++ [s])) * p) (fun2set (g2,dg)))``, 1527 REVERSE Induct \\ SIMP_TAC std_ss [LIST_FIND_def] THEN1 1528 (STRIP_TAC \\ Cases_on `h = s` \\ FULL_SIMP_TAC std_ss [EVERY_DEF] 1529 \\ SIMP_TAC std_ss [symbol_list_def,string_data_def,one_byte_list_def, 1530 one_byte_list_APPEND,LENGTH,LENGTH_MAP,ADD1] 1531 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def,EVERY_DEF] 1532 \\ ONCE_REWRITE_TAC [mc_insert_sym_def] 1533 \\ SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ SEP_R_TAC 1534 \\ `LENGTH h + 1 < 256` by DECIDE_TAC 1535 \\ `(STRLEN s + 1) < 18446744073709551616` by DECIDE_TAC 1536 \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,n2w_11] 1537 \\ REVERSE (Cases_on `LENGTH h = LENGTH s`) \\ ASM_SIMP_TAC std_ss [] THEN1 1538 (FULL_SIMP_TAC std_ss [word_add_n2w,APPEND,symbol_list_def] 1539 \\ FULL_SIMP_TAC std_ss [string_data_def,one_byte_list_def, 1540 one_byte_list_APPEND,LENGTH,LENGTH_APPEND,LENGTH_MAP] 1541 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def] 1542 \\ `n + (LENGTH xs + 1) = (n+1) + LENGTH xs` by DECIDE_TAC 1543 \\ ASM_SIMP_TAC std_ss [ADD1] 1544 \\ SEP_I_TAC "mc_insert_sym" 1545 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * (one (a,n2w (STRLEN h + 1)) * one_string (a + 0x1w) h)`,`x`]) 1546 \\ FULL_SIMP_TAC (std_ss++star_ss) [] 1547 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,AC ADD_COMM ADD_ASSOC,ADD1] 1548 \\ FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def]) 1549 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_SUB] 1550 \\ ASSUME_TAC (GEN_ALL (Q.SPECL [`s1`,`s2`] mc_string_eq_thm)) 1551 \\ SEP_I_TAC "mc_string_eq" 1552 \\ POP_ASSUM (MP_TAC o Q.SPECL [`h`,`one (a,n2w (STRLEN h + 1)) * 1553 one (r9 + 0x1w + n2w (STRLEN h),x) * 1554 one_byte_list (a + n2w (STRLEN h + 1)) (symbol_list xs) * p`]) 1555 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,word_add_n2w,AC ADD_ASSOC ADD_COMM] 1556 \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ STRIP_TAC 1557 \\ FULL_SIMP_TAC wstd_ss [n2w_11] THEN1 1558 (FULL_SIMP_TAC std_ss [word_add_n2w,APPEND,symbol_list_def] 1559 \\ FULL_SIMP_TAC std_ss [string_data_def,one_byte_list_def, 1560 one_byte_list_APPEND,LENGTH,LENGTH_APPEND,LENGTH_MAP] 1561 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def] 1562 \\ `n + (LENGTH xs + 1) = (n+1) + LENGTH xs` by DECIDE_TAC 1563 \\ ASM_SIMP_TAC std_ss [ADD1] 1564 \\ SEP_I_TAC "mc_insert_sym" 1565 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * (one (a,n2w (STRLEN h + 1)) * one_string (a + 0x1w) h)`,`x`]) 1566 \\ FULL_SIMP_TAC (std_ss++star_ss) [] 1567 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,AC ADD_COMM ADD_ASSOC,ADD1] 1568 \\ FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def])) 1569 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,symbol_list_def,one_byte_list_def,SEP_CLAUSES, 1570 word_arith_lemma1,AC ADD_ASSOC ADD_COMM,LENGTH,WORD_ADD_0,APPEND,string_data_def, 1571 one_byte_list_APPEND,LENGTH_MAP] 1572 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def] 1573 \\ ONCE_REWRITE_TAC [mc_insert_sym_def] 1574 \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ SEP_R_TAC 1575 \\ `(STRLEN s + 1) < 18446744073709551616` by DECIDE_TAC 1576 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,word_lo_n2w] 1577 \\ Cases_on `254 < STRLEN s + 1` \\ ASM_SIMP_TAC std_ss [] 1578 THEN1 (Q.EXISTS_TAC `T` \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 1579 \\ SIMP_TAC std_ss [GSYM w2w_def] 1580 \\ FULL_SIMP_TAC std_ss [ref_static_def,LET_DEF,word64_3232_def,word_arith_lemma1, 1581 word_arith_lemma2,word_arith_lemma3,word_arith_lemma4,SEP_CLAUSES,STAR_ASSOC, 1582 INSERT_SUBSET,EMPTY_SUBSET] 1583 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [mc_insert_sym_lemma2_blast] 1584 \\ FULL_SIMP_TAC std_ss [align_add_blast,align_blast,n2w_and_3] 1585 \\ REVERSE (Cases_on `0x208w <+ sa3 - sa2 - n2w (STRLEN s + 1)`) 1586 THEN1 (ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) \\ ASM_SIMP_TAC std_ss [] 1587 \\ Cases_on `536870910 < n MOD 18446744073709551616` 1588 THEN1 (ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) \\ ASM_SIMP_TAC std_ss [] 1589 \\ Q.EXISTS_TAC `F` \\ FULL_SIMP_TAC std_ss [word_add_n2w] 1590 \\ Q.UNABBREV_TAC `r9` 1591 \\ FULL_SIMP_TAC std_ss [WORD_ADD_SUB] 1592 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,word_arith_lemma1] 1593 \\ FULL_SIMP_TAC std_ss [mc_insert_sym_lemma2_blast] 1594 \\ REPEAT STRIP_TAC \\ SEP_R_TAC \\ SEP_WRITE_TAC); 1595 1596val mc_insert_sym_lemma3 = prove( 1597 ``!xs n p a r9. 1598 (r7 && 3w = 0w) /\ EVERY (\x. STRLEN x < 255) xs /\ 1599 (one_byte_list a (symbol_list xs) * p) (fun2set (g,dg)) ==> 1600 ?toosmall. 1601 mc_insert_sym_pre (r7,a,r9,n2w n,256w,dg,g,df,f) /\ 1602 (mc_insert_sym (r7,a,r9,n2w n,256w,dg,g,df,f) = 1603 (r7,if toosmall then 25w else 29w,3w,dg,g,df,f))``, 1604 REVERSE Induct \\ SIMP_TAC std_ss [LIST_FIND_def] THEN1 1605 (STRIP_TAC \\ FULL_SIMP_TAC std_ss [EVERY_DEF] 1606 \\ SIMP_TAC std_ss [symbol_list_def,string_data_def,one_byte_list_def, 1607 one_byte_list_APPEND,LENGTH,LENGTH_MAP,ADD1] 1608 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def,EVERY_DEF] 1609 \\ ONCE_REWRITE_TAC [mc_insert_sym_def] 1610 \\ SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ SEP_R_TAC 1611 \\ `LENGTH h + 1 < 256` by DECIDE_TAC 1612 \\ `~(256 = STRLEN h + 1)` by DECIDE_TAC 1613 \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,n2w_11] 1614 \\ ASM_SIMP_TAC std_ss [ADD1,word_add_n2w] 1615 \\ SEP_I_TAC "mc_insert_sym" 1616 \\ POP_ASSUM (MP_TAC o Q.SPECL [`p * (one (a,n2w (STRLEN h + 1)) * one_string (a + 0x1w) h)`]) 1617 \\ FULL_SIMP_TAC (std_ss++star_ss) [] 1618 \\ FULL_SIMP_TAC std_ss [string_data_def,one_byte_list_def, 1619 one_byte_list_APPEND,LENGTH,LENGTH_APPEND,LENGTH_MAP] 1620 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,ADD1,WORD_ADD_ASSOC] 1621 \\ METIS_TAC []) 1622 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,symbol_list_def,one_byte_list_def,SEP_CLAUSES, 1623 word_arith_lemma1,AC ADD_ASSOC ADD_COMM,LENGTH,WORD_ADD_0,APPEND,string_data_def, 1624 one_byte_list_APPEND,LENGTH_MAP] 1625 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def] 1626 \\ ONCE_REWRITE_TAC [mc_insert_sym_def] 1627 \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ SEP_R_TAC 1628 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,word_lo_n2w] 1629 \\ METIS_TAC []); 1630 1631 1632(* read next token *) 1633 1634val (mc_next_token_spec,mc_next_token_def) = basic_decompile_strings x64_tools "mc_next_token" 1635 (SOME (``(r7:word64,r15:word64,io:io_streams,dg:word64 set,g:word64->word8,df:word64 set,f:word64->word32)``, 1636 ``(r0:word64,r7:word64,r8:word64,r9:word64,r10:word64,r11:word64,r15:word64,io:io_streams,dg:word64 set,g:word64->word8,df:word64 set,f:word64->word32)``)) 1637 (assemble "x64" ` 1638START: 1639 insert io_read 1640 cmp r0,32 1641 ja NOT_SPACE 1642 insert io_next 1643 jmp START 1644NOT_SPACE: 1645 cmp r0,40 1646 je OPEN 1647 cmp r0,41 1648 je CLOSE 1649 cmp r0,39 1650 je QUOTE 1651 cmp r0,46 1652 je DOT 1653 cmp r0,35 1654 je HASH 1655 cmp r0,59 1656 je COMMENT 1657 cmp r0,57 1658 ja SYMBOL 1659 cmp r0,48 1660 jb SYMBOL 1661NUMBER: 1662 sub r0,48 1663 mov r8,r0 1664 insert io_next 1665 insert mc_read_num 1666 mov r9d,1 1667 cmp r8,1073741823 1668 ja TOOLARGENUM 1669 shl r8,2 1670 inc r8 1671 jmp EXIT 1672COMMENT: 1673 mov r0d,0 1674 insert io_next 1675 insert mc_read_until_newline 1676 mov r0d,0 1677 jmp START 1678TOOLARGENUM: 1679 mov r8d,37 1680 mov r9d,3 1681 jmp EXIT 1682SYMBOL: 1683 cmp r0,255 1684 ja END 1685 mov r9,[r7-216] 1686 insert mc_read_sym 1687 mov r8,[r7-224] 1688 dec r9 1689 inc r15 1690 xor r10,r10 1691 insert mc_insert_sym 1692 mov r15,[r7-240] 1693 add r15,r15 1694 jmp EXIT 1695END: 1696 mov r8d,41 1697 mov r9d,3 1698 jmp EXIT 1699HASH: 1700 insert io_next 1701 xor r8,r8 1702 insert mc_read_num 1703 insert io_read 1704 cmp r0,255 1705 ja HASH_ERR 1706 insert io_next 1707 cmp r0,35 1708 jne HASH1 1709 cmp r8,1073741823 1710 ja TOOLARGENUM 1711 shl r8,2 1712 inc r8 1713 mov r9d,13 1714 jmp EXIT 1715HASH1: 1716 cmp r0,61 1717 jne HASH_ERR 1718 cmp r8,1073741823 1719 ja TOOLARGENUM 1720 shl r8,2 1721 inc r8 1722 mov r9d,9 1723 jmp EXIT 1724HASH_ERR: 1725 mov r8d,33 1726 mov r9d,3 1727 jmp EXIT 1728OPEN: 1729 mov r0d,1 1730 jmp BASIC 1731CLOSE: 1732 mov r0d,9 1733 jmp BASIC 1734DOT: 1735 mov r0d,5 1736 jmp BASIC 1737QUOTE: 1738 mov r0d,13 1739BASIC: 1740 mov r8,r0 1741 mov r0d,5 1742 mov r9,r0 1743 insert io_next 1744EXIT: 1745 mov r0d,3 1746 mov r10,r0 1747 mov r11,r0 1748 `); 1749 1750val _ = save_thm("mc_next_token_spec",mc_next_token_spec); 1751 1752val lisp_inv_Val0 = Q.SPEC `0` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1753val lisp_inv_Val1 = Q.SPEC `1` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1754val lisp_inv_Val2 = Q.SPEC `2` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1755val lisp_inv_Val3 = Q.SPEC `3` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1756val lisp_inv_Val4 = Q.SPEC `4` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1757val lisp_inv_Val5 = Q.SPEC `5` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1758val lisp_inv_Val6 = Q.SPEC `6` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1759val lisp_inv_Val7 = Q.SPEC `7` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1760val lisp_inv_Val8 = Q.SPEC `8` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1761val lisp_inv_Val9 = Q.SPEC `9` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1762val lisp_inv_Val10 = Q.SPEC `10` lisp_inv_Val_n2w |> SIMP_RULE std_ss []; 1763 1764val lisp_inv_Val_lemma = LIST_CONJ [lisp_inv_Val0,lisp_inv_Val1,lisp_inv_Val2,lisp_inv_Val3,lisp_inv_Val4,lisp_inv_Val5,lisp_inv_Val10]; 1765 1766val IF_OR = METIS_PROVE [] ``(if b then x else if c then x else y) = 1767 (if b \/ c then x else y)`` 1768 1769val next_token_blast = blastLib.BBLAST_PROVE 1770 ``(w << 3 !! 3w = (w << 3) + 3w:word64) /\ 1771 (v << 3 !! 3w = (v << 3) + 3w:word32)`` 1772 1773val LIST_FIND_NONE_SOME = prove( 1774 ``!xs n s x. 1775 (LIST_FIND n s xs = NONE) ==> (LIST_FIND n s (xs ++ [s]) = SOME (n + LENGTH xs))``, 1776 Induct \\ ASM_SIMP_TAC std_ss [LIST_FIND_def,APPEND,LENGTH] 1777 \\ REPEAT STRIP_TAC \\ Cases_on `s = h` \\ FULL_SIMP_TAC std_ss [] 1778 \\ FULL_SIMP_TAC std_ss [ADD1] \\ DECIDE_TAC); 1779 1780val LIST_FIND_NONE_IMP = prove( 1781 ``!xs n s x. (LIST_FIND n s xs = NONE) ==> ~MEM s xs``, 1782 Induct \\ ASM_SIMP_TAC std_ss [LIST_FIND_def,APPEND,LENGTH,MEM] 1783 \\ REPEAT STRIP_TAC \\ Cases_on `s = h` \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []); 1784 1785val LIST_FIND_SOME_LESS_LENGTH = prove( 1786 ``!xs n s k. (LIST_FIND n s xs = SOME k) ==> k < n + LENGTH xs``, 1787 Induct \\ SIMP_TAC std_ss [LIST_FIND_def,LENGTH] \\ SRW_TAC [] [] 1788 \\ RES_TAC \\ DECIDE_TAC); 1789 1790val LENGTH_symbol_list_SNOC = prove( 1791 ``!xs x. LENGTH (symbol_list (xs ++ [x])) = LENGTH (symbol_list xs) + LENGTH x + 1``, 1792 Induct \\ ASM_SIMP_TAC std_ss [symbol_list_def,APPEND,LENGTH, 1793 string_data_def,ADD1,LENGTH_APPEND,LENGTH_MAP,AC ADD_ASSOC ADD_COMM]); 1794 1795val one_byte_list_IMP = prove( 1796 ``!f df p a xs. 1797 (one_byte_list a xs * p) (fun2set (f,df)) ==> 1798 LENGTH xs <= 18446744073709551616``, 1799 REPEAT STRIP_TAC \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss [GSYM NOT_LESS] 1800 \\ IMP_RES_TAC SPLIT_LIST 1801 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND] 1802 \\ Cases_on `xs1` \\ FULL_SIMP_TAC std_ss [LENGTH] 1803 \\ FULL_SIMP_TAC std_ss [one_byte_list_def] 1804 \\ `~(a = a + 0x10000000000000000w)` by SEP_NEQ_TAC 1805 \\ POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [] \\ Cases_on `a` 1806 \\ FULL_SIMP_TAC wstd_ss [word_add_n2w,n2w_11,ADD_MODULUS_LEFT]); 1807 1808val tw0_lemma = prove( 1809 ``^LISP ==> (tw0 = 3w)``, 1810 SIMP_TAC std_ss [lisp_inv_def] \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss []); 1811 1812val gc_w2w_lemma = prove( 1813 ``!w. ((w2w:word64->word32) ((w2w:word32->word64) w) = w) /\ 1814 ((31 -- 0) ((w2w:word32->word64) w) = w2w w) /\ 1815 ((31 >< 0) bp = (w2w bp):word32) /\ 1816 ((63 >< 32) bp = (w2w (bp >>> 32)):word32) /\ 1817 (w2w ((w2w (bp >>> 32)):word32) << 32 !! w2w ((w2w bp):word32) = bp:word64)``, 1818 blastLib.BBLAST_TAC); 1819 1820val lisp_inv_3NIL = prove( 1821 ``^LISP ==> let (x1,x2,x3,w1,w2,w3) = (Sym "NIL",Sym "NIL",Sym "NIL",3w,3w,3w) in ^LISP``, 1822 SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 1823 \\ MATCH_MP_TAC lisp_inv_swap1 1824 \\ MATCH_MP_TAC lisp_inv_NIL 1825 \\ Q.LIST_EXISTS_TAC [`x1`,`w1`] 1826 \\ MATCH_MP_TAC lisp_inv_swap1 1827 \\ MATCH_MP_TAC lisp_inv_swap2 1828 \\ MATCH_MP_TAC lisp_inv_NIL 1829 \\ Q.LIST_EXISTS_TAC [`x2`,`w2`] 1830 \\ MATCH_MP_TAC lisp_inv_swap2 1831 \\ MATCH_MP_TAC lisp_inv_swap3 1832 \\ MATCH_MP_TAC lisp_inv_NIL 1833 \\ Q.LIST_EXISTS_TAC [`x3`,`w3`] 1834 \\ MATCH_MP_TAC lisp_inv_swap3 1835 \\ ASM_SIMP_TAC std_ss []) |> SIMP_RULE std_ss [LET_DEF]; 1836 1837val lisp_inv_2NIL = prove( 1838 ``^LISP ==> let (x2,x3,w2,w3) = (Sym "NIL",Sym "NIL",3w,3w) in ^LISP``, 1839 SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 1840 \\ MATCH_MP_TAC lisp_inv_swap2 1841 \\ MATCH_MP_TAC lisp_inv_NIL 1842 \\ Q.LIST_EXISTS_TAC [`x2`,`w2`] 1843 \\ MATCH_MP_TAC lisp_inv_swap2 1844 \\ MATCH_MP_TAC lisp_inv_swap3 1845 \\ MATCH_MP_TAC lisp_inv_NIL 1846 \\ Q.LIST_EXISTS_TAC [`x3`,`w3`] 1847 \\ MATCH_MP_TAC lisp_inv_swap3 1848 \\ ASM_SIMP_TAC std_ss []) |> SIMP_RULE std_ss [LET_DEF]; 1849 1850val my_next_token_ind = prove( 1851 ``!P. P "" /\ 1852 (!h zs. 1853 ((h = #";") ==> P (SND (read_while (\x. x <> #"\n") zs ""))) /\ 1854 (space_char h ==> P zs) ==> 1855 P (STRING h zs)) ==> 1856 !zs. P zs``, 1857 NTAC 2 STRIP_TAC \\ HO_MATCH_MP_TAC (SIMP_RULE std_ss [] next_token_ind) 1858 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1859 \\ Q.PAT_X_ASSUM `!h zs. bbb` (MP_TAC o Q.SPECL [`c`,`cs`]) 1860 \\ Cases_on `c = #";"` \\ FULL_SIMP_TAC wstd_ss [CHR_11] 1861 \\ FULL_SIMP_TAC std_ss [EVAL ``~space_char #";" /\ ~number_char #";"``]); 1862 1863(* allow for failure, e.g. too large number, too long symbol, not enough symtable space *) 1864val mc_next_token_lemma = prove( 1865 ``!zs z zs2. 1866 (next_token zs = (z,zs2)) ==> 1867 (lisp_inv ^STAT (x0,x1,x2,x3,x4,x5,^VAR_REST) 1868 (w0,w1,w2,w3,w4,w5,df,f,^REST)) ==> 1869 ?ok1 zX z0 z1 w0i w1i w2i w3i io2 gi fi sa2. 1870 mc_next_token_pre (sp,we,REPLACE_INPUT_IO zs io,dg,g,df,f) /\ 1871 (mc_next_token (sp,we,REPLACE_INPUT_IO zs io,dg,g,df,f) = 1872 (tw0,sp,w2w w0i,w2w w1i,w2w w2i,w2w w3i,we,io2,dg,gi,df,fi)) /\ 1873 (lisp_inv ^STAT 1874 (if ok1 then z0 else zX,if ok1 then z1 else Sym "NIL",Sym "NIL",Sym "NIL",x4,x5,^VAR_REST) 1875 (w0i,w1i,w2i,w3i,w4,w5,df,fi,let g = gi in ^REST)) /\ 1876 (ok1 ==> (REPLACE_INPUT_IO zs2 io = io2)) /\ 1877 (if ok1 then (z = (z0,z1)) else isVal zX)``, 1878 1879 SIMP_TAC std_ss [LET_DEF] 1880 \\ HO_MATCH_MP_TAC my_next_token_ind \\ REPEAT STRIP_TAC 1881 \\ Q.PAT_X_ASSUM `next_token xxx = yyy` (MP_TAC o GSYM) 1882 \\ SIMP_TAC std_ss [next_token_def] \\ STRIP_TAC 1883 \\ SIMP_TAC std_ss [MAP] \\ ONCE_REWRITE_TAC [mc_next_token_def] 1884 \\ `ORD h < 256` by METIS_TAC [ORD_BOUND] 1885 \\ `ORD h < 18446744073709551616` by DECIDE_TAC 1886 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,IO_INPUT_LEMMA,w2w_def,w2n_n2w, 1887 n2w_11,word_lo_n2w,space_char_def,DECIDE ``n < 33 = n <= 32:num``] 1888 \\ ONCE_REWRITE_TAC [GSYM (EVAL ``ORD #"("``)] 1889 \\ ONCE_REWRITE_TAC [GSYM (EVAL ``ORD #")"``)] 1890 \\ ONCE_REWRITE_TAC [GSYM (EVAL ``ORD #"."``)] 1891 \\ ONCE_REWRITE_TAC [GSYM (EVAL ``ORD #"'"``)] 1892 \\ FULL_SIMP_TAC std_ss [] 1893 \\ SIMP_TAC std_ss [ORD_11,CHR_ORD] THEN1 1894 (SIMP_TAC (std_ss++SIZES_ss) ([word_1comp_n2w,word_lo_n2w,n2w_11,w2n_n2w] 1895 @ map EVAL [``ORD #"("``,``ORD #")"``,``ORD #"."``,``ORD #"'"``]) 1896 \\ `tw0 = 3w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1897 \\ FULL_SIMP_TAC std_ss [] 1898 \\ Q.EXISTS_TAC `F` 1899 \\ Q.EXISTS_TAC `Val 10` \\ ASM_SIMP_TAC std_ss [isVal_def] 1900 \\ Q.LIST_EXISTS_TAC [`41w`,`3w`,`3w`,`3w`] 1901 \\ SIMP_TAC wstd_ss [w2n_n2w] 1902 \\ Q.EXISTS_TAC `sa2` 1903 \\ MATCH_MP_TAC lisp_inv_3NIL 1904 \\ IMP_RES_TAC lisp_inv_Val_lemma) 1905 \\ Q.PAT_X_ASSUM `(z,zs2) = xxx` MP_TAC 1906 \\ Cases_on `ORD h <= 32` \\ ASM_SIMP_TAC std_ss [] THEN1 1907 (ASM_SIMP_TAC std_ss [DECIDE ``32 < ORD h = ~(ORD h <= 32)``,GSYM w2w_def,space_char_def] 1908 \\ FULL_SIMP_TAC std_ss [LET_DEF,space_char_def] \\ METIS_TAC [tw0_lemma]) 1909 \\ Q.PAT_X_ASSUM `space_char h ==> bbb` (K ALL_TAC) 1910 \\ `32 < ORD h` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 1911 \\ Cases_on `h = #";"` \\ ASM_SIMP_TAC std_ss [] THEN1 1912 (ASM_SIMP_TAC (srw_ss()) [EVAL ``ORD #";"``,EVAL ``number_char #";"``] 1913 \\ ASM_SIMP_TAC std_ss [LET_DEF,EVAL ``space_char #";"``, 1914 mc_read_until_newline_thm] \\ METIS_TAC [w2w_def]) 1915 \\ Q.PAT_X_ASSUM `(h = #";") ==> bbb` (K ALL_TAC) 1916 \\ ASM_SIMP_TAC std_ss [space_char_def] 1917 \\ Cases_on `h = #"("` \\ ASM_SIMP_TAC std_ss [] THEN1 1918 (REPEAT STRIP_TAC \\ IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 1919 \\ Q.EXISTS_TAC `T` \\ FULL_SIMP_TAC std_ss [] 1920 \\ Q.LIST_EXISTS_TAC [`1w`,`5w`,`3w`,`3w`] 1921 \\ SIMP_TAC wstd_ss [w2n_n2w] \\ Q.EXISTS_TAC `sa2` 1922 \\ MATCH_MP_TAC lisp_inv_2NIL 1923 \\ METIS_TAC [lisp_inv_Val_lemma,lisp_inv_swap1,tw0_lemma]) 1924 \\ Cases_on `h = #")"` \\ ASM_SIMP_TAC std_ss [] THEN1 1925 (ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,CHR_11] 1926 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 1927 \\ Q.EXISTS_TAC `T` \\ FULL_SIMP_TAC std_ss [] 1928 \\ Q.LIST_EXISTS_TAC [`9w`,`5w`,`3w`,`3w`] 1929 \\ SIMP_TAC wstd_ss [w2n_n2w] \\ Q.EXISTS_TAC `sa2` 1930 \\ MATCH_MP_TAC lisp_inv_2NIL 1931 \\ METIS_TAC [lisp_inv_Val_lemma,lisp_inv_swap1,tw0_lemma]) 1932 \\ Cases_on `h = #"'"` \\ ASM_SIMP_TAC std_ss [] THEN1 1933 (ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,CHR_11] 1934 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 1935 \\ Q.EXISTS_TAC `T` \\ FULL_SIMP_TAC std_ss [] 1936 \\ Q.LIST_EXISTS_TAC [`0xDw`,`5w`,`3w`,`3w`] 1937 \\ SIMP_TAC wstd_ss [w2n_n2w] \\ Q.EXISTS_TAC `sa2` 1938 \\ MATCH_MP_TAC lisp_inv_2NIL 1939 \\ METIS_TAC [lisp_inv_Val_lemma,lisp_inv_swap1,tw0_lemma]) 1940 \\ Cases_on `h = #"."` \\ ASM_SIMP_TAC std_ss [] THEN1 1941 (ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,CHR_11] 1942 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 1943 \\ Q.EXISTS_TAC `T` \\ FULL_SIMP_TAC std_ss [] 1944 \\ Q.LIST_EXISTS_TAC [`0x5w`,`5w`,`3w`,`3w`] 1945 \\ SIMP_TAC wstd_ss [w2n_n2w] \\ Q.EXISTS_TAC `sa2` 1946 \\ MATCH_MP_TAC lisp_inv_2NIL 1947 \\ METIS_TAC [lisp_inv_Val_lemma,lisp_inv_swap1,tw0_lemma]) 1948 \\ `~(255 < ORD h)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 1949 \\ FULL_SIMP_TAC std_ss [LET_DEF] 1950 \\ Cases_on `number_char h` THEN1 1951 (`~(h = #"#") /\ ~(ORD h = 35) /\ ~(ORD h = 59) /\ ~(57 < ORD h) /\ ~(ORD h < 48)`by 1952 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [EVAL ``number_char #"#"``] 1953 \\ FULL_SIMP_TAC std_ss [number_char_def] \\ DECIDE_TAC) 1954 \\ ASM_SIMP_TAC std_ss [] 1955 \\ STRIP_ASSUME_TAC (Q.SPECL [`zs`,`number_char`] read_while_SPLIT) 1956 \\ FULL_SIMP_TAC std_ss [APPEND,word_arith_lemma2,mc_read_num_thm] 1957 \\ Cases_on `str2num (STRING h xs1') < 1073741824` \\ ASM_SIMP_TAC std_ss [] THEN1 1958 (SIMP_TAC (std_ss++SIZES_ss) [WORD_MUL_LSL,word_mul_n2w,word_add_n2w,word_lo_n2w,w2n_n2w] 1959 \\ `~(1073741823 < str2num (STRING h xs1'))` by DECIDE_TAC 1960 \\ `(str2num (STRING h xs1')) < 18446744073709551616` by DECIDE_TAC 1961 \\ `(4 * str2num (STRING h xs1') + 1) < 18446744073709551616` by DECIDE_TAC 1962 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `T` 1963 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_add_n2w,word_lo_n2w,w2n_n2w] 1964 \\ Q.LIST_EXISTS_TAC [`n2w (4 * str2num (STRING h xs1') + 1)`,`1w`,`3w`,`3w`] 1965 \\ Q.EXISTS_TAC `sa2` \\ IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 1966 \\ SIMP_TAC wstd_ss [w2n_n2w] 1967 \\ `(4 * str2num (STRING h xs1') + 1) < 4294967296` by DECIDE_TAC 1968 \\ ASM_SIMP_TAC std_ss [] 1969 \\ MATCH_MP_TAC lisp_inv_2NIL 1970 \\ MATCH_MP_TAC lisp_inv_Val_n2w \\ ASM_SIMP_TAC std_ss [] 1971 \\ METIS_TAC [lisp_inv_Val_lemma,lisp_inv_swap1]) 1972 \\ ASM_SIMP_TAC std_ss [EVAL ``0x3FFFFFFFw <+ ~n2w (str2num ""):word64``] 1973 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `F` \\ ASM_SIMP_TAC std_ss [] 1974 \\ IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 1975 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_add_n2w,word_lo_n2w,w2n_n2w] 1976 \\ Q.EXISTS_TAC `Val 9` \\ ASM_SIMP_TAC std_ss [isVal_def] 1977 \\ Q.LIST_EXISTS_TAC [`0x25w`,`3w`,`3w`,`3w`,`sa2`] 1978 \\ SIMP_TAC wstd_ss [w2n_n2w] 1979 \\ ASM_SIMP_TAC std_ss [] 1980 \\ MATCH_MP_TAC lisp_inv_3NIL 1981 \\ IMP_RES_TAC lisp_inv_Val9) 1982 \\ ASM_SIMP_TAC std_ss [] 1983 \\ Cases_on `h = #"#"` \\ ASM_SIMP_TAC std_ss [] THEN1 1984 (ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,EVAL ``ORD #"#"``] 1985 \\ STRIP_ASSUME_TAC (Q.SPECL [`zs`,`number_char`] read_while_SPLIT) 1986 \\ FULL_SIMP_TAC std_ss [APPEND,word_arith_lemma2,mc_read_num_thm0] 1987 \\ Cases_on `xs2` \\ ASM_SIMP_TAC std_ss [IO_INPUT_LEMMA,MAP] THEN1 1988 (ASM_SIMP_TAC (std_ss++SIZES_ss) [EVAL ``0xFFw <+ ~0x0w:word64``] 1989 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`F`,`Val 8`] 1990 \\ IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 1991 \\ Q.LIST_EXISTS_TAC [`0x21w`,`3w`,`3w`,`3w`,`sa2`] 1992 \\ SIMP_TAC wstd_ss [w2n_n2w,isVal_def] 1993 \\ ASM_SIMP_TAC std_ss [] 1994 \\ MATCH_MP_TAC lisp_inv_3NIL 1995 \\ IMP_RES_TAC lisp_inv_Val8) 1996 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,ORD_BOUND] 1997 \\ `~(0xFFw <+ n2w (ORD h'):word64)` by 1998 (`ORD h' < 256` by ASM_SIMP_TAC std_ss [ORD_BOUND] 1999 \\ `ORD h' < 18446744073709551616` by DECIDE_TAC 2000 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,ORD_BOUND,word_lo_n2w] 2001 \\ DECIDE_TAC) \\ ASM_SIMP_TAC std_ss [] 2002 \\ `ORD h' < 256` by ASM_SIMP_TAC std_ss [ORD_BOUND] 2003 \\ `ORD h' < 18446744073709551616` by DECIDE_TAC 2004 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [NOT_CONS_NIL,n2w_11,HD] 2005 \\ Cases_on `h' = #"#"` \\ ASM_SIMP_TAC std_ss [EVAL ``ORD #"#"``] THEN1 2006 (REVERSE (Cases_on `str2num xs1' < 1073741824`) \\ ASM_SIMP_TAC std_ss [] 2007 \\ ASM_SIMP_TAC std_ss [EVAL ``0x3FFFFFFFw <+ ~0x0w:word64``,NOT_CONS_NIL,TL] 2008 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [HD,w2w_def,w2n_n2w,ORD_BOUND] 2009 \\ REPEAT STRIP_TAC THEN1 2010 (IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 2011 \\ Q.EXISTS_TAC `F` \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `Val 9` 2012 \\ Q.LIST_EXISTS_TAC [`0x25w`,`3w`,`3w`,`3w`,`sa2`] 2013 \\ SIMP_TAC wstd_ss [w2n_n2w,isVal_def] 2014 \\ ASM_SIMP_TAC std_ss [] 2015 \\ MATCH_MP_TAC lisp_inv_3NIL 2016 \\ IMP_RES_TAC lisp_inv_Val9) 2017 \\ IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 2018 \\ `str2num xs1' < 18446744073709551616` by DECIDE_TAC 2019 \\ `~(1073741823 < str2num xs1')` by DECIDE_TAC 2020 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,TL,w2n_n2w] 2021 \\ Q.EXISTS_TAC `T` 2022 \\ ASM_SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 2023 \\ Q.LIST_EXISTS_TAC [`n2w (4 * str2num xs1' + 1)`,`0xDw`,`3w`,`3w`,`sa2`] 2024 \\ SIMP_TAC wstd_ss [w2n_n2w,isVal_def] 2025 \\ ASM_SIMP_TAC std_ss [] 2026 \\ `(4 * str2num xs1' + 1) < 4294967296` by DECIDE_TAC 2027 \\ ASM_SIMP_TAC std_ss [] 2028 \\ MATCH_MP_TAC lisp_inv_2NIL 2029 \\ MATCH_MP_TAC lisp_inv_Val_n2w \\ ASM_SIMP_TAC std_ss [] 2030 \\ METIS_TAC [lisp_inv_Val_lemma,lisp_inv_swap1]) 2031 \\ ASM_SIMP_TAC std_ss [] 2032 \\ `~(ORD h' = 35)` by FULL_SIMP_TAC std_ss [GSYM ORD_11,EVAL ``ORD #"#"``] 2033 \\ ASM_SIMP_TAC std_ss [] 2034 \\ Cases_on `h' = #"="` \\ ASM_SIMP_TAC std_ss [EVAL ``ORD #"="``] THEN1 2035 (REVERSE (Cases_on `str2num xs1' < 1073741824`) \\ ASM_SIMP_TAC std_ss [] 2036 \\ ASM_SIMP_TAC std_ss [EVAL ``0x3FFFFFFFw <+ ~0x0w:word64``,NOT_CONS_NIL,TL] 2037 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [HD,w2w_def,w2n_n2w,ORD_BOUND] 2038 \\ REPEAT STRIP_TAC THEN1 2039 (IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 2040 \\ Q.EXISTS_TAC `F` \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `Val 9` 2041 \\ Q.LIST_EXISTS_TAC [`0x25w`,`3w`,`3w`,`3w`,`sa2`] 2042 \\ SIMP_TAC wstd_ss [w2n_n2w,isVal_def] 2043 \\ ASM_SIMP_TAC std_ss [] 2044 \\ MATCH_MP_TAC lisp_inv_3NIL 2045 \\ IMP_RES_TAC lisp_inv_Val9) 2046 \\ IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 2047 \\ `str2num xs1' < 18446744073709551616` by DECIDE_TAC 2048 \\ `~(1073741823 < str2num xs1')` by DECIDE_TAC 2049 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,TL,w2n_n2w] 2050 \\ Q.EXISTS_TAC `T` 2051 \\ ASM_SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 2052 \\ Q.LIST_EXISTS_TAC [`n2w (4 * str2num xs1' + 1)`,`0x9w`,`3w`,`3w`,`sa2`] 2053 \\ SIMP_TAC wstd_ss [w2n_n2w,isVal_def] 2054 \\ ASM_SIMP_TAC std_ss [] 2055 \\ `(4 * str2num xs1' + 1) < 4294967296` by DECIDE_TAC 2056 \\ ASM_SIMP_TAC std_ss [] 2057 \\ MATCH_MP_TAC lisp_inv_2NIL 2058 \\ MATCH_MP_TAC lisp_inv_Val_n2w \\ ASM_SIMP_TAC std_ss [] 2059 \\ METIS_TAC [lisp_inv_Val_lemma,lisp_inv_swap1]) 2060 \\ `~(ORD h' = 61)` by FULL_SIMP_TAC std_ss [GSYM ORD_11,EVAL ``ORD #"="``] 2061 \\ ASM_SIMP_TAC std_ss [TL] 2062 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,TL,w2n_n2w] 2063 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`F`,`Val 8`] 2064 \\ IMP_RES_TAC tw0_lemma \\ FULL_SIMP_TAC std_ss [] 2065 \\ ASM_SIMP_TAC std_ss [isVal_def] 2066 \\ Q.LIST_EXISTS_TAC [`0x21w`,`3w`,`3w`,`3w`,`sa2`] 2067 \\ SIMP_TAC wstd_ss [w2n_n2w,isVal_def] 2068 \\ ASM_SIMP_TAC std_ss [] 2069 \\ MATCH_MP_TAC lisp_inv_3NIL 2070 \\ IMP_RES_TAC lisp_inv_Val8) 2071 \\ `~(ORD h = 35)` by FULL_SIMP_TAC std_ss [GSYM ORD_11,EVAL ``ORD #"#"``] 2072 \\ `~(ORD h = 59)` by FULL_SIMP_TAC std_ss [GSYM ORD_11,EVAL ``ORD #";"``] 2073 \\ ASM_SIMP_TAC std_ss [IF_OR] 2074 \\ `57 < ORD h \/ ORD h < 48 = ~number_char h` by 2075 (FULL_SIMP_TAC std_ss [number_char_def] \\ DECIDE_TAC) 2076 \\ ASM_SIMP_TAC std_ss [GSYM w2w_def] 2077 \\ `?cs1 cs2. str2sym (STRING h zs) = (cs1,cs2)` by METIS_TAC [PAIR] 2078 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 2079 \\ `w2w (f (sp - 0xDCw)) << 32 !! w2w (f (sp - 0xE0w)) = sa1` by 2080 (IMP_RES_TAC lisp_inv_cs_read \\ ASM_SIMP_TAC std_ss []) 2081 \\ `w2w (f (sp - 0xD4w)) << 32 !! w2w (f (sp - 0xD8w)) = sa2` by 2082 (IMP_RES_TAC lisp_inv_cs_read \\ ASM_SIMP_TAC std_ss []) 2083 \\ `w2w (f (sp - 236w)) << 32 !! w2w (f (sp - 240w)) = (n2w e):word64` by 2084 (FULL_SIMP_TAC std_ss [lisp_inv_def] 2085 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` MP_TAC 2086 \\ FULL_SIMP_TAC std_ss [APPEND,ref_full_stack_def] 2087 \\ NTAC 4 (ONCE_REWRITE_TAC [ref_static_def]) 2088 \\ FULL_SIMP_TAC std_ss [word64_3232_def,LET_DEF,STAR_ASSOC] 2089 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3] \\ STRIP_TAC \\ SEP_R_TAC 2090 \\ FULL_SIMP_TAC std_ss [gc_w2w_lemma]) 2091 \\ ASM_SIMP_TAC std_ss [word_add_n2w,DECIDE ``n+n=2*n``] 2092 \\ REVERSE (Cases_on `LENGTH cs1 < 255`) THEN1 2093 (Q.PAT_X_ASSUM `lisp_inv xxx yyy zzz` (STRIP_ASSUME_TAC o RW [lisp_inv_def]) 2094 \\ FULL_SIMP_TAC std_ss [symtable_inv_def,one_symbol_list_def,SEP_EXISTS_THM,cond_STAR] 2095 \\ Q.ABBREV_TAC `sll = LENGTH (symbol_list (INIT_SYMBOLS ++ sym))` 2096 \\ `255 < LENGTH ys` by DECIDE_TAC 2097 \\ IMP_RES_TAC SPLIT_LIST 2098 \\ MP_TAC (Q.SPECL [`h::zs`,`cs1`,`cs2`,`g`,`one_byte_list sa1 (symbol_list (INIT_SYMBOLS ++ sym)) * 2099 one (sa1 + n2w (sll + 255),x) * 2100 one_byte_list (sa1 + n2w (sll + 256)) xs2`,`MAP (CHR o w2n) (xs1':word8 list)`] (Q.INST [`r9`|->`sa1 + n2w sll`] mc_read_sym_overflow_thm)) 2101 \\ ASM_SIMP_TAC std_ss [LENGTH_MAP] 2102 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,one_byte_list_APPEND,STAR_ASSOC] 2103 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 2104 \\ ASM_SIMP_TAC std_ss [LENGTH_MAP,one_string_def,MAP_MAP_LEMMA] 2105 \\ `255 <= STRLEN cs1` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 2106 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 FULL_SIMP_TAC (std_ss++star_ss) [] 2107 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [word_add_n2w] 2108 \\ POP_ASSUM (ASSUME_TAC o GSYM) \\ FULL_SIMP_TAC std_ss [] 2109 \\ ASSUME_TAC (Q.GEN `r7` (Q.GEN `g` (Q.SPEC `INIT_SYMBOLS ++ sym` mc_insert_sym_lemma3))) 2110 \\ SEP_I_TAC "mc_insert_sym" \\ POP_ASSUM MP_TAC 2111 \\ FULL_SIMP_TAC std_ss [] \\ STRIP_TAC \\ SEP_F_TAC 2112 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 2113 \\ Q.EXISTS_TAC `F` \\ ASM_SIMP_TAC std_ss [] 2114 \\ Q.LIST_EXISTS_TAC [`Val (if toosmall then 6 else 7)`, 2115 `if toosmall then 0x19w else 0x1Dw`,`3w`,`3w`,`3w`,`sa2`] 2116 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,isVal_def,word_add_n2w, 2117 DECIDE ``n+n=2*n:num``] 2118 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC THEN1 2119 (REVERSE STRIP_TAC THEN1 (Cases_on `toosmall` \\ EVAL_TAC) 2120 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3,ref_full_stack_def,STAR_ASSOC, 2121 ref_static_def,LET_DEF,APPEND,word64_3232_def,word_arith_lemma3, 2122 INSERT_SUBSET,EMPTY_SUBSET] 2123 \\ SEP_R_TAC \\ SIMP_TAC std_ss []) 2124 \\ Cases_on `toosmall` \\ ASM_SIMP_TAC wstd_ss [w2n_n2w] THEN1 2125 (MATCH_MP_TAC lisp_inv_Val6 2126 \\ MATCH_MP_TAC lisp_inv_3NIL 2127 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 2128 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 2129 \\ FULL_SIMP_TAC std_ss [] 2130 \\ ASM_SIMP_TAC std_ss [symtable_inv_def,SEP_EXISTS_THM,one_symbol_list_def,cond_STAR] 2131 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_PLUS] 2132 \\ Q.EXISTS_TAC `MAP (n2w o ORD) xs2' ++ x::xs2` 2133 \\ `255 <= LENGTH cs1` by DECIDE_TAC 2134 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_MAP,LENGTH_APPEND,LENGTH_TAKE] 2135 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,one_byte_list_APPEND,LENGTH_MAP,LENGTH_TAKE] 2136 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def,word_arith_lemma1]) 2137 THEN1 2138 (MATCH_MP_TAC lisp_inv_Val7 2139 \\ MATCH_MP_TAC lisp_inv_3NIL 2140 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 2141 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 2142 \\ FULL_SIMP_TAC std_ss [] 2143 \\ ASM_SIMP_TAC std_ss [symtable_inv_def,SEP_EXISTS_THM,one_symbol_list_def,cond_STAR] 2144 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_PLUS] 2145 \\ Q.EXISTS_TAC `MAP (n2w o ORD) xs2' ++ x::xs2` 2146 \\ `255 <= LENGTH cs1` by DECIDE_TAC 2147 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_MAP,LENGTH_APPEND,LENGTH_TAKE] 2148 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,one_byte_list_APPEND,LENGTH_MAP,LENGTH_TAKE] 2149 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def,word_arith_lemma1])) 2150 \\ Q.PAT_X_ASSUM `lisp_inv xxx yyy zzz` (STRIP_ASSUME_TAC o RW [lisp_inv_def]) 2151 \\ FULL_SIMP_TAC std_ss [symtable_inv_def,one_symbol_list_def,SEP_EXISTS_THM,cond_STAR] 2152 \\ `LENGTH cs1 < LENGTH ys` by DECIDE_TAC 2153 \\ IMP_RES_TAC SPLIT_LIST 2154 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,one_byte_list_APPEND,STAR_ASSOC] 2155 \\ Q.ABBREV_TAC `sll = LENGTH (symbol_list (INIT_SYMBOLS ++ sym))` 2156 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 2157 \\ MP_TAC (Q.SPECL [`h::zs`,`cs1`,`cs2`,`g`,`one_byte_list sa1 (symbol_list (INIT_SYMBOLS ++ sym)) * 2158 one (sa1 + n2w (sll + STRLEN cs1),x) * 2159 one_byte_list (sa1 + n2w (sll + (STRLEN cs1 + 1))) xs2`,`MAP (CHR o w2n) (xs1':word8 list)`] (Q.INST [`r9`|->`sa1 + n2w sll`] mc_read_sym_thm)) 2160 \\ `LENGTH cs1 < 256` by DECIDE_TAC 2161 \\ ASM_SIMP_TAC std_ss [LENGTH_MAP,one_string_def,MAP_MAP_LEMMA] 2162 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 FULL_SIMP_TAC (std_ss++star_ss) [] 2163 \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [word_arith_lemma1] 2164 \\ REVERSE (Cases_on `LIST_FIND 0 cs1 (INIT_SYMBOLS ++ sym)`) THEN1 2165 (MP_TAC (Q.SPECL [`INIT_SYMBOLS ++ sym`,`0`,`x'`,` 2166 one (sa1 + n2w (sll + STRLEN cs1),x) * 2167 one_byte_list (sa1 + n2w (sll + (STRLEN cs1 + 1))) xs2`,`sa1`] (Q.INST [`s`|->`cs1`,`g`|->`g2`,`r9`|->`sa1 + n2w sll - 1w`,`r7`|->`sp`] mc_insert_sym_lemma1)) 2168 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 2169 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 2170 (FULL_SIMP_TAC std_ss [WORD_SUB_ADD] 2171 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def,word_arith_lemma1]) 2172 \\ STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 2173 \\ Q.EXISTS_TAC `T` 2174 \\ SIMP_TAC std_ss [next_token_blast,WORD_MUL_LSL,word_add_n2w,word_mul_n2w] 2175 \\ Q.LIST_EXISTS_TAC [`n2w (8 * x' + 3)`,`1w`,`3w`,`3w`,`sa2`] 2176 \\ SIMP_TAC wstd_ss [w2w_def,w2n_n2w] \\ SIMP_TAC std_ss [GSYM w2w_def] 2177 \\ IMP_RES_TAC LIST_FIND_SOME_LESS_LENGTH 2178 \\ `x' < 536870912` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 2179 \\ `(8 * x' + 3) < 4294967296` by DECIDE_TAC 2180 \\ ASM_SIMP_TAC std_ss [word_add_n2w,DECIDE ``n+n=2*n``] 2181 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC THEN1 2182 (FULL_SIMP_TAC std_ss [align_blast,n2w_and_3,ref_full_stack_def,STAR_ASSOC, 2183 ref_static_def,LET_DEF,APPEND,word64_3232_def,word_arith_lemma3] 2184 \\ SEP_R_TAC \\ SIMP_TAC std_ss []) 2185 \\ MATCH_MP_TAC lisp_inv_2NIL 2186 \\ MATCH_MP_TAC lisp_inv_swap1 2187 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_Val0) 2188 \\ Q.LIST_EXISTS_TAC [`x1`,`w1`] 2189 \\ MATCH_MP_TAC lisp_inv_swap1 2190 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 2191 \\ Q.LIST_EXISTS_TAC [`H_DATA (INR (n2w x'))`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 2192 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,lisp_x_def,MAP,CONS_11,ref_heap_addr_def] 2193 \\ REPEAT STRIP_TAC THEN1 2194 (FULL_SIMP_TAC std_ss [APPEND,ok_split_heap_def,ADDR_SET_THM,UNION_SUBSET] 2195 \\ MATCH_MP_TAC SUBSET_TRANS 2196 \\ Q.EXISTS_TAC `ADDR_SET (s0::s1::s2::s3::s4::s5::(ss++ss1))` 2197 \\ ASM_SIMP_TAC std_ss [] 2198 \\ Cases_on `s0` 2199 \\ FULL_SIMP_TAC std_ss [ADDR_SET_THM,SUBSET_DEF,IN_INSERT]) 2200 THEN1 2201 (`(8 * x' + 3) < 18446744073709551616` by DECIDE_TAC 2202 \\ ASM_SIMP_TAC wstd_ss [next_token_blast,WORD_MUL_LSL,word_add_n2w,w2w_def, 2203 w2n_n2w,word_mul_n2w]) 2204 THEN1 (FULL_SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_PLUS]) 2205 \\ FULL_SIMP_TAC std_ss [symtable_inv_def,one_symbol_list_def,SEP_EXISTS_THM,cond_STAR] 2206 \\ Q.EXISTS_TAC `MAP (n2w o ORD) cs1 ++ x::xs2` 2207 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH,LENGTH_MAP] 2208 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND,LENGTH_MAP,one_byte_list_def] 2209 \\ FULL_SIMP_TAC (std_ss++star_ss) [word_arith_lemma1]) 2210 \\ MP_TAC (Q.SPECL [`INIT_SYMBOLS ++ sym`,`0`,`x'`,` 2211 one_byte_list (sa1 + n2w (sll + (STRLEN cs1 + 1))) xs2`,`sa1`,`x`,`sa1 + n2w sll - 1w`] 2212 (Q.INST [`s`|->`cs1`,`g`|->`g2`,`r7`|->`sp`,`q`|->` 2213 ref_mem bp m 0 e * ref_mem bp2 (\x. H_EMP) 0 e * 2214 ref_stack (sp + 0x4w * wsp) (ss ++ ss1) * 2215 ref_stack_space (sp + 0x4w * wsp) (w2n wsp + 6) * 2216 ref_static (sp - 256w) ([a1; a2; n2w e; bp2; sa1]) * 2217 ref_stack_space_above 2218 (sp + 0x4w * wsp + n2w (4 * (LENGTH ss + LENGTH ss1))) 2219 (sl1 - LENGTH ss1) * 2220 ref_static (sp - 0xC8w) ([ex] ++ cs ++ ds)`] mc_insert_sym_lemma2)) 2221 \\ ASM_SIMP_TAC std_ss [markerTheory.Abbrev_def] 2222 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 2223 (FULL_SIMP_TAC std_ss [WORD_SUB_ADD,STAR_ASSOC] 2224 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def,word_arith_lemma1] 2225 \\ `[a1; a2; n2w e; bp2; sa1; sa1 + n2w sll; sa3; ex] ++ cs ++ ds = 2226 [a1; a2; n2w e; bp2; sa1] ++ [sa1 + n2w sll; sa3] ++ ([ex] ++ cs ++ ds)` by SIMP_TAC std_ss [APPEND] 2227 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` MP_TAC 2228 \\ ASM_SIMP_TAC std_ss [] 2229 \\ Q.SPEC_TAC (`[ex]++cs++ds`,`xxs`) \\ STRIP_TAC 2230 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,ref_static_APPEND] 2231 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND,word_arith_lemma3] 2232 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def,word_arith_lemma1]) 2233 \\ STRIP_TAC \\ Cases_on `fail` THEN1 2234 (FULL_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `F` \\ ASM_SIMP_TAC std_ss [] 2235 \\ Q.LIST_EXISTS_TAC [`Val (if toosmall then 6 else 7)`,`(if toosmall then 0x19w else 0x1Dw)`,`3w`,`3w`,`3w`,`sa2`] 2236 \\ ASM_SIMP_TAC wstd_ss [isVal_def,w2w_def,w2n_n2w,word_add_n2w,DECIDE ``n+n=2*n``] 2237 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC THEN1 2238 (REVERSE STRIP_TAC THEN1 (Cases_on `toosmall` \\ EVAL_TAC) 2239 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3,ref_full_stack_def,STAR_ASSOC, 2240 ref_static_def,LET_DEF,APPEND,word64_3232_def,word_arith_lemma3, 2241 INSERT_SUBSET,EMPTY_SUBSET] 2242 \\ SEP_R_TAC \\ SIMP_TAC std_ss []) 2243 \\ MATCH_MP_TAC lisp_inv_3NIL 2244 \\ Cases_on `toosmall` \\ ASM_SIMP_TAC wstd_ss [w2n_n2w] THEN1 2245 (MATCH_MP_TAC lisp_inv_Val6 2246 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 2247 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 2248 \\ ASM_SIMP_TAC std_ss [symtable_inv_def,SEP_EXISTS_THM,one_symbol_list_def,cond_STAR] 2249 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_PLUS] 2250 \\ Q.EXISTS_TAC `MAP (n2w o ORD) cs1 ++ x::xs2` 2251 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_MAP,LENGTH_APPEND] 2252 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,one_byte_list_APPEND,LENGTH_MAP] 2253 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def,word_arith_lemma1]) 2254 THEN1 2255 (MATCH_MP_TAC lisp_inv_Val7 2256 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 2257 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 2258 \\ ASM_SIMP_TAC std_ss [symtable_inv_def,SEP_EXISTS_THM,one_symbol_list_def,cond_STAR] 2259 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_PLUS] 2260 \\ Q.EXISTS_TAC `MAP (n2w o ORD) cs1 ++ x::xs2` 2261 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_MAP,LENGTH_APPEND] 2262 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,one_byte_list_APPEND,LENGTH_MAP] 2263 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def,word_arith_lemma1])) 2264 \\ FULL_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `T` \\ ASM_SIMP_TAC std_ss [] 2265 \\ `w2w (f2 (sp - 236w)) << 32 !! w2w (f2 (sp - 240w)) = (n2w e):word64` by 2266 (FULL_SIMP_TAC std_ss [lisp_inv_def] 2267 \\ Q.PAT_X_ASSUM `xxx (fun2set (f2,df))` MP_TAC 2268 \\ FULL_SIMP_TAC std_ss [APPEND,ref_full_stack_def] 2269 \\ NTAC 4 (ONCE_REWRITE_TAC [ref_static_def]) 2270 \\ FULL_SIMP_TAC std_ss [word64_3232_def,LET_DEF,STAR_ASSOC] 2271 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3] \\ STRIP_TAC \\ SEP_R_TAC 2272 \\ FULL_SIMP_TAC std_ss [gc_w2w_lemma]) 2273 \\ ASM_SIMP_TAC std_ss [GSYM w2w_def,word_add_n2w,DECIDE ``n+n=2*n``] 2274 \\ ASM_SIMP_TAC std_ss [next_token_blast,WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 2275 \\ Q.LIST_EXISTS_TAC [`n2w (8 * LENGTH (INIT_SYMBOLS ++ sym) + 3)`,`1w`,`3w`,`3w`] 2276 \\ Q.EXISTS_TAC `sa1 + n2w (sll + (STRLEN cs1 + 1))` 2277 \\ `(8 * LENGTH (INIT_SYMBOLS ++ sym) + 3) < 4294967296` by DECIDE_TAC 2278 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w] 2279 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC THEN1 2280 (FULL_SIMP_TAC std_ss [align_blast,n2w_and_3,ref_full_stack_def,STAR_ASSOC, 2281 ref_static_def,LET_DEF,APPEND,word64_3232_def,word_arith_lemma3, 2282 INSERT_SUBSET,EMPTY_SUBSET] \\ SEP_R_TAC \\ SIMP_TAC std_ss []) 2283 \\ MATCH_MP_TAC lisp_inv_2NIL 2284 \\ MATCH_MP_TAC lisp_inv_swap1 2285 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_Val0) \\ Q.LIST_EXISTS_TAC [`x1`,`w1`] 2286 \\ MATCH_MP_TAC lisp_inv_swap1 2287 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 2288 \\ Q.LIST_EXISTS_TAC [`H_DATA (INR (n2w (LENGTH (INIT_SYMBOLS ++ sym))))`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym ++ [cs1]`,`b`] 2289 \\ `code_heap code (INIT_SYMBOLS ++ (sym ++ [cs1]),EL 4 cs,EL 2 ds,EL 3 ds,dd,d)` by 2290 METIS_TAC [code_heap_add_symbol,APPEND_ASSOC] 2291 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,ref_heap_addr_def,GSYM w2w_def] 2292 \\ REPEAT STRIP_TAC THEN1 2293 (FULL_SIMP_TAC std_ss [APPEND,ok_split_heap_def,ADDR_SET_THM,UNION_SUBSET] 2294 \\ MATCH_MP_TAC SUBSET_TRANS 2295 \\ Q.EXISTS_TAC `ADDR_SET (s0::s1::s2::s3::s4::s5::(ss++ss1))` 2296 \\ ASM_SIMP_TAC std_ss [] 2297 \\ Cases_on `s0` 2298 \\ FULL_SIMP_TAC std_ss [ADDR_SET_THM,SUBSET_DEF,IN_INSERT]) 2299 THEN1 2300 (ONCE_REWRITE_TAC [EVERY_DEF] \\ REPEAT STRIP_TAC THEN1 2301 (SIMP_TAC std_ss [lisp_x_def] 2302 \\ Q.EXISTS_TAC `LENGTH (INIT_SYMBOLS ++ sym)` 2303 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC] 2304 \\ METIS_TAC [LIST_FIND_NONE_SOME,ADD_CLAUSES]) 2305 \\ MATCH_MP_TAC (GEN_ALL (RW [AND_IMP_INTRO] MONO_EVERY)) 2306 \\ Q.EXISTS_TAC `lisp_x (m,INIT_SYMBOLS ++ (sym))` 2307 \\ REVERSE STRIP_TAC THEN1 FULL_SIMP_TAC std_ss [EVERY_DEF] 2308 \\ Cases \\ Q.SPEC_TAC (`q`,`q`) \\ Induct_on `r` 2309 \\ FULL_SIMP_TAC std_ss [lisp_x_def] THEN1 (REPEAT STRIP_TAC \\ METIS_TAC []) 2310 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `k` 2311 \\ ASM_SIMP_TAC std_ss [APPEND_ASSOC] 2312 \\ Q.PAT_X_ASSUM `xxx = SOME k` MP_TAC 2313 \\ Q.SPEC_TAC (`INIT_SYMBOLS ++ sym`,`syms`) 2314 \\ Q.SPEC_TAC (`0`,`n`) 2315 \\ Induct_on `syms` \\ ASM_SIMP_TAC std_ss [LIST_FIND_def,APPEND] \\ METIS_TAC []) 2316 THEN1 2317 (`((8 * LENGTH (INIT_SYMBOLS ++ sym) + 3) < 18446744073709551616)` by DECIDE_TAC 2318 \\ ASM_SIMP_TAC wstd_ss [next_token_blast,w2w_def,w2n_n2w,WORD_MUL_LSL, 2319 word_mul_n2w,word_add_n2w]) 2320 THEN1 2321 (FULL_SIMP_TAC std_ss [word_arith_lemma1]) 2322 THEN1 2323 (FULL_SIMP_TAC std_ss [ref_full_stack_def] 2324 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 2325 \\ `[a1; a2; n2w e; bp2; sa1; sa1 + n2w (sll + (STRLEN cs1 + 1)); sa3; ex] ++ cs ++ ds = 2326 [a1; a2; n2w e; bp2; sa1] ++ [sa1 + n2w (sll + (STRLEN cs1 + 1)); sa3] ++ ([ex] ++ cs ++ ds)` by SIMP_TAC std_ss [APPEND] 2327 \\ Q.PAT_X_ASSUM `xxx (fun2set (f2,df))` MP_TAC 2328 \\ ASM_SIMP_TAC std_ss [] 2329 \\ Q.SPEC_TAC (`[ex]++cs++ds`,`xxs`) \\ STRIP_TAC 2330 \\ FULL_SIMP_TAC std_ss [ref_static_APPEND,LENGTH,LENGTH_APPEND,word_arith_lemma3] 2331 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 2332 \\ Q.UNABBREV_TAC `sll` 2333 \\ SIMP_TAC std_ss [symtable_inv_def,LENGTH_APPEND,APPEND_ASSOC] 2334 \\ SIMP_TAC std_ss [LENGTH_symbol_list_SNOC,ADD_ASSOC] 2335 \\ SIMP_TAC std_ss [one_symbol_list_def,SEP_EXISTS_THM,cond_STAR,one_byte_list_APPEND] 2336 \\ Q.EXISTS_TAC `xs2` 2337 \\ Q.PAT_X_ASSUM `xxx = w2n sa3 - w2n sa1` (ASSUME_TAC o GSYM) 2338 \\ ASM_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH_symbol_list_SNOC,LENGTH,ADD1] 2339 \\ FULL_SIMP_TAC std_ss [EVERY_APPEND,EVERY_DEF,AC ADD_ASSOC ADD_COMM] 2340 \\ ASM_SIMP_TAC std_ss [RW [SNOC_APPEND] rich_listTheory.ALL_DISTINCT_SNOC] 2341 \\ IMP_RES_TAC LIST_FIND_NONE_IMP \\ ASM_SIMP_TAC std_ss [] 2342 \\ STRIP_TAC THEN1 2343 (Q.PAT_X_ASSUM `xx <+ yyy` MP_TAC \\ Q.PAT_X_ASSUM `w2n _ - w2n _ = _` MP_TAC 2344 \\ Q.SPEC_TAC (`sa1`,`sa1`) \\ Q.SPEC_TAC (`sa3`,`sa3`) \\ Cases \\ Cases 2345 \\ FULL_SIMP_TAC std_ss [w2n_n2w,LENGTH_APPEND,LENGTH,ADD1,word_add_n2w] 2346 \\ SIMP_TAC std_ss [GSYM WORD_SUB_PLUS,word_add_n2w] 2347 \\ SIMP_TAC std_ss [SUB_RIGHT_EQ] 2348 \\ SIMP_TAC std_ss [word_arith_lemma2,ADD_ASSOC,DECIDE ``~(m + n < m:num)``] 2349 \\ SIMP_TAC std_ss [DECIDE ``n + m + 1 - (n + 1):num = m``] 2350 \\ SIMP_TAC wstd_ss [word_lo_n2w] 2351 \\ `LENGTH (x::xs2) <= 18446744073709551616` by 2352 (MATCH_MP_TAC one_byte_list_IMP 2353 \\ Q.LIST_EXISTS_TAC [`g`,`dg`, 2354 `one_byte_list sa1 (symbol_list (INIT_SYMBOLS ++ sym)) * 2355 one_byte_list (sa1 + n2w (LENGTH (symbol_list (INIT_SYMBOLS ++ sym)))) xs1'`, 2356 `sa1 + n2w (STRLEN cs1 + LENGTH (symbol_list (INIT_SYMBOLS ++ sym)))`] 2357 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_byte_list_def,word_arith_lemma1, 2358 AC ADD_ASSOC ADD_COMM]) 2359 \\ FULL_SIMP_TAC std_ss [LENGTH,GSYM LESS_EQ] \\ DECIDE_TAC) 2360 \\ Q.PAT_X_ASSUM `~(xxx <+ yy)` MP_TAC 2361 \\ FULL_SIMP_TAC wstd_ss [word_lo_n2w] 2362 \\ `LENGTH (INIT_SYMBOLS ++ sym) < 18446744073709551616` by DECIDE_TAC 2363 \\ ASM_SIMP_TAC std_ss [NOT_LESS,LENGTH_APPEND] 2364 \\ DECIDE_TAC) |> SIMP_RULE std_ss [LET_DEF]; 2365 2366val mc_next_token_thm = mc_next_token_lemma 2367 |> Q.SPECL [`getINPUT io`,`FST (next_token (getINPUT io))`,`(SND o next_token) (getINPUT io)`] 2368 |> RW [IO_INPUT_LEMMA,GSYM IO_INPUT_APPLY_def] 2369 |> SIMP_RULE std_ss [] 2370 |> (fn th => save_thm("mc_next_token_thm",th)); 2371 2372 2373(* num2str *) 2374 2375val (thm,mc_num2strlen_def) = basic_decompile_strings x64_tools "mc_num2strlen" 2376 (SOME (``(r0:word64,r8:word64,r9:word64)``, 2377 ``(r8:word64,r9:word64)``)) 2378 (assemble "x64" ` 2379START: 2380 inc r9 2381 cmp r8,r0 2382 jb EXIT 2383 lea r0,[4*r0+r0] 2384 add r0,r0 2385 jmp START 2386EXIT: `) 2387 2388val mc_num2strlen_blast = prove( 2389 ``!w. 4w * w + w + (4w * w + w) = 10w * w:word64``, 2390 blastLib.BBLAST_TAC); 2391 2392val mc_num2strlen_lemma = mc_num2strlen_def 2393 |> SIMP_RULE std_ss [LET_DEF,mc_num2strlen_blast] 2394 2395val mc_num2strlen_thm = prove( 2396 ``n < 2**30 ==> 2397 (mc_num2strlen (10w,n2w n,n2w i) = (n2w n, n2w (i + LENGTH (num2str n)))) /\ 2398 mc_num2strlen_pre (10w,n2w n,n2w i) /\ 2399 LENGTH (num2str n) <= 10``, 2400 SIMP_TAC std_ss [] \\ STRIP_TAC 2401 \\ `n < 18446744073709551616` by DECIDE_TAC 2402 \\ ONCE_REWRITE_TAC [mc_num2strlen_lemma,num2str_def] 2403 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,DIV_EQ_X, 2404 LENGTH_APPEND,dec2str_def,LENGTH,word_add_n2w,word_mul_n2w] 2405 \\ Cases_on `n < 10` \\ ASM_SIMP_TAC std_ss [LENGTH] 2406 \\ ONCE_REWRITE_TAC [mc_num2strlen_lemma,num2str_def] 2407 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,DIV_EQ_X,GSYM ADD_ASSOC, 2408 LENGTH_APPEND,dec2str_def,LENGTH,word_add_n2w,word_mul_n2w,DIV_LT_X] 2409 \\ Cases_on `n < 100` \\ ASM_SIMP_TAC std_ss [LENGTH] 2410 \\ ONCE_REWRITE_TAC [mc_num2strlen_lemma,num2str_def] 2411 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,DIV_EQ_X,GSYM ADD_ASSOC, 2412 LENGTH_APPEND,dec2str_def,LENGTH,word_add_n2w,word_mul_n2w,DIV_LT_X] 2413 \\ Cases_on `n < 1000` \\ ASM_SIMP_TAC std_ss [LENGTH] 2414 \\ ONCE_REWRITE_TAC [mc_num2strlen_lemma,num2str_def] 2415 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,DIV_EQ_X,GSYM ADD_ASSOC, 2416 LENGTH_APPEND,dec2str_def,LENGTH,word_add_n2w,word_mul_n2w,DIV_LT_X] 2417 \\ Cases_on `n < 10000` \\ ASM_SIMP_TAC std_ss [LENGTH] 2418 \\ ONCE_REWRITE_TAC [mc_num2strlen_lemma,num2str_def] 2419 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,DIV_EQ_X,GSYM ADD_ASSOC, 2420 LENGTH_APPEND,dec2str_def,LENGTH,word_add_n2w,word_mul_n2w,DIV_LT_X] 2421 \\ Cases_on `n < 100000` \\ ASM_SIMP_TAC std_ss [LENGTH] 2422 \\ ONCE_REWRITE_TAC [mc_num2strlen_lemma,num2str_def] 2423 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,DIV_EQ_X,GSYM ADD_ASSOC, 2424 LENGTH_APPEND,dec2str_def,LENGTH,word_add_n2w,word_mul_n2w,DIV_LT_X] 2425 \\ Cases_on `n < 1000000` \\ ASM_SIMP_TAC std_ss [LENGTH] 2426 \\ ONCE_REWRITE_TAC [mc_num2strlen_lemma,num2str_def] 2427 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,DIV_EQ_X,GSYM ADD_ASSOC, 2428 LENGTH_APPEND,dec2str_def,LENGTH,word_add_n2w,word_mul_n2w,DIV_LT_X] 2429 \\ Cases_on `n < 10000000` \\ ASM_SIMP_TAC std_ss [LENGTH] 2430 \\ ONCE_REWRITE_TAC [mc_num2strlen_lemma,num2str_def] 2431 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,DIV_EQ_X,GSYM ADD_ASSOC, 2432 LENGTH_APPEND,dec2str_def,LENGTH,word_add_n2w,word_mul_n2w,DIV_LT_X] 2433 \\ Cases_on `n < 100000000` \\ ASM_SIMP_TAC std_ss [LENGTH] 2434 \\ ONCE_REWRITE_TAC [mc_num2strlen_lemma,num2str_def] 2435 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,DIV_EQ_X,GSYM ADD_ASSOC, 2436 LENGTH_APPEND,dec2str_def,LENGTH,word_add_n2w,word_mul_n2w,DIV_LT_X] 2437 \\ Cases_on `n < 1000000000` \\ ASM_SIMP_TAC std_ss [LENGTH] 2438 \\ ONCE_REWRITE_TAC [mc_num2strlen_lemma,num2str_def] 2439 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w,DIV_EQ_X,GSYM ADD_ASSOC, 2440 LENGTH_APPEND,dec2str_def,LENGTH,word_add_n2w,word_mul_n2w,DIV_LT_X] 2441 \\ Cases_on `n < 10000000000` \\ ASM_SIMP_TAC std_ss [LENGTH] 2442 \\ `F` by DECIDE_TAC); 2443 2444val (thm,mc_num2str_loop_def) = basic_decompile_strings x64_tools "mc_num2str_loop" 2445 (SOME (``(r8:word64,r9:word64,r10:word64,dg:word64 set,g:word64->word8)``, 2446 ``(dg:word64 set,g:word64->word8)``)) 2447 (assemble "x64" ` 2448START: 2449 dec r9 2450 cmp r8,10 2451 jb EXIT 2452 mov eax,r10d 2453 mul r8d (* r2 has r8 div 10 *) 2454 lea r0,[4*r2+r2] 2455 add r0,r0 (* r0 has r8 div 10 * 10 *) 2456 sub r8,r0 (* r8 has r8 div 10 *) 2457 add r8,48 2458 mov BYTE [r9],r8b 2459 mov r8,r2 2460 jmp START 2461EXIT: add r8,48 2462 mov BYTE [r9],r8b`) 2463 2464val FAST_DIV_10 = prove( 2465 ``!x. x < 2**30 ==> (0x1999999A * x DIV 2**32 = x DIV 10)``, 2466 REPEAT STRIP_TAC 2467 \\ `?z. x DIV 10 = z` by METIS_TAC [] \\ ASM_SIMP_TAC std_ss [] 2468 \\ FULL_SIMP_TAC std_ss [DIV_EQ_X] \\ DECIDE_TAC); 2469 2470val SPLIT = METIS_PROVE [] ``b /\ (b1 ==> b2) ==> ((b ==> b1) ==> b2)``; 2471 2472val mc_num2str_loop_thm = prove( 2473 ``!n a xs p g. 2474 ((one_byte_list a xs * p) (fun2set (g,dg))) /\ n < 2**30 ==> 2475 (LENGTH (num2str n) = LENGTH xs) ==> 2476 ?g1. mc_num2str_loop_pre(n2w n,a + n2w (LENGTH (num2str n)),0x1999999Aw,dg,g) /\ 2477 (mc_num2str_loop(n2w n,a + n2w (LENGTH (num2str n)),0x1999999Aw,dg,g) = (dg,g1)) /\ 2478 (one_string a (num2str n) * p) (fun2set (g1,dg))``, 2479 completeInduct_on `n` \\ NTAC 5 STRIP_TAC 2480 \\ ONCE_REWRITE_TAC [mc_num2str_loop_def] 2481 \\ `n < 18446744073709551616` by (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 2482 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,word_lo_n2w] 2483 \\ Cases_on `n < 10` THEN1 2484 (ONCE_REWRITE_TAC [num2str_def] \\ ASM_SIMP_TAC std_ss [DIV_EQ_X] 2485 \\ SIMP_TAC std_ss [dec2str_def,one_string_def,LENGTH,MAP] 2486 \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_NIL] 2487 \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2488 \\ `n + 48 < 256 /\ (n + 48) < 18446744073709551616` by DECIDE_TAC 2489 \\ FULL_SIMP_TAC std_ss [ORD_CHR] 2490 \\ FULL_SIMP_TAC std_ss [word_add_n2w,one_byte_list_def,SEP_CLAUSES] 2491 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [WORD_ADD_SUB,w2w_def,w2n_n2w] 2492 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 2493 \\ `n < 4294967296` by (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 2494 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_bits_n2w,bitTheory.BITS_THM,w2n_n2w] 2495 \\ FULL_SIMP_TAC std_ss [] 2496 \\ ASM_SIMP_TAC std_ss [SIMP_RULE std_ss [] FAST_DIV_10, 2497 mc_num2strlen_blast,word_mul_n2w] 2498 \\ SIMP_TAC std_ss [word_arith_lemma2] 2499 \\ `~(n < 10 * (n DIV 10)) /\ (n - 10 * (n DIV 10) = n MOD 10)` by 2500 (ASSUME_TAC (Q.SPEC `n` (SIMP_RULE std_ss [] (Q.SPEC `10` DIVISION))) 2501 \\ DECIDE_TAC) \\ ASM_SIMP_TAC std_ss [word_add_n2w] 2502 \\ ONCE_REWRITE_TAC [num2str_def] 2503 \\ ASM_SIMP_TAC std_ss [DIV_EQ_X,LENGTH_APPEND,LENGTH,dec2str_def] 2504 \\ `(xs = []) \/ ?x l. xs = SNOC x l` by METIS_TAC [rich_listTheory.SNOC_CASES] 2505 \\ ASM_SIMP_TAC std_ss [LENGTH,LENGTH_SNOC,ADD1] 2506 \\ ASM_SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_SUB,WORD_ADD_ASSOC] 2507 \\ FULL_SIMP_TAC std_ss [one_string_def,MAP_APPEND,MAP,one_byte_list_APPEND, 2508 LENGTH_MAP,one_byte_list_def,SEP_CLAUSES,SNOC_APPEND] 2509 \\ `n MOD 10 < 10` by METIS_TAC [MOD_LESS,DECIDE ``0<10``] 2510 \\ `n MOD 10 + 48 < 256` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [ORD_CHR] 2511 \\ `n MOD 10 + 48 < 18446744073709551616` by DECIDE_TAC 2512 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [word_add_n2w,w2w_def,w2n_n2w] \\ STRIP_TAC 2513 \\ Q.ABBREV_TAC `g6 = (a + n2w (LENGTH l) =+ n2w (n MOD 10 + 48)) g` 2514 \\ Q.PAT_X_ASSUM `!m.bb` (MP_TAC o Q.SPEC `n DIV 10`) 2515 \\ MATCH_MP_TAC SPLIT \\ STRIP_TAC 2516 THEN1 (ASM_SIMP_TAC std_ss [DIV_LT_X] \\ DECIDE_TAC) 2517 \\ STRIP_TAC \\ POP_ASSUM (MP_TAC o Q.SPECL [`a`,`l`,`one (a + n2w (LENGTH (l:word8 list)),n2w (n MOD 10 + 48)) * p`,`g6`]) 2518 \\ MATCH_MP_TAC SPLIT \\ STRIP_TAC THEN1 2519 (REVERSE STRIP_TAC THEN1 (SIMP_TAC std_ss [DIV_LT_X] \\ DECIDE_TAC) 2520 \\ Q.UNABBREV_TAC `g6` \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] \\ SEP_W_TAC) 2521 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2522 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] 2523 \\ SEP_R_TAC \\ EVAL_TAC); 2524 2525val (mc_num2str_spec,mc_num2str_def) = basic_decompile_strings x64_tools "mc_num2str" 2526 (SOME (``(r8:word64,r11:word64,dg:word64 set,g:word64->word8)``, 2527 ``(r11:word64,dg:word64 set,g:word64->word8)``)) 2528 (assemble "x64" ` 2529 shr r8,2 2530 mov r0d,10 2531 mov r9,r11 2532 insert mc_num2strlen 2533 mov r10d,429496730 2534 mov r11,r9 2535 insert mc_num2str_loop 2536 `) 2537 2538val mc_num2str_blast2 = blastLib.BBLAST_PROVE 2539 ``(w2w w << 2 !! 0x1w) >>> 2 = (w2w (w:word30)):word64``; 2540 2541val mc_num2str_thm = prove( 2542 ``!a. 2543 (one_byte_list a xs * p) (fun2set (g,dg)) /\ n < 2**30 /\ 2544 (LENGTH (num2str n) = LENGTH xs) ==> 2545 ?g1. mc_num2str_pre(n2w n << 2 !! 1w,a,dg,g) /\ 2546 (mc_num2str(n2w n << 2 !! 1w,a,dg,g) = (a + n2w (LENGTH (num2str n)),dg,g1)) /\ 2547 (one_string a (num2str n) * p) (fun2set (g1,dg))``, 2548 Cases \\ SIMP_TAC std_ss [mc_num2str_def,LET_DEF] \\ REPEAT STRIP_TAC 2549 \\ `(n2w n) = (w2w ((n2w n):word30)):word64` by 2550 ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 2551 \\ ASM_SIMP_TAC std_ss [mc_num2str_blast2] \\ POP_ASSUM (K ALL_TAC) 2552 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 2553 \\ ASM_SIMP_TAC std_ss [SIMP_RULE std_ss [] mc_num2strlen_thm] 2554 \\ IMP_RES_TAC (SIMP_RULE std_ss [] mc_num2str_loop_thm) 2555 \\ FULL_SIMP_TAC std_ss [word_add_n2w]); 2556 2557 2558(* sym2str 2559 - find symbol string 2560 - check if sym2str_aux is needed 2561 - run wither copy or sym2str_aux 2562*) 2563 2564val (thm,mc_sym2str_aux_def) = basic_decompile_strings x64_tools "mc_sym2str_aux" 2565 (SOME (``(r8:word64,r9:word64,r10:word64,r11:word64,dg:word64 set,g:word64->word8)``, 2566 ``(r8:word64,r9:word64,r10:word64,r11:word64,dg:word64 set,g:word64->word8)``)) 2567 (assemble "x64" ` 2568START: 2569 cmp r8,r10 2570 je EXIT 2571 movzx r0,BYTE [r9+r8] 2572 inc r8 2573 cmp r0,0 2574 je ZERO 2575 cmp r0,92 2576 je SLASH 2577 cmp r0,124 2578 je BAR 2579 mov BYTE [r11],r0b 2580 inc r11 2581 jmp START 2582BAR: 2583 mov BYTE [r11+1],124 2584 jmp FINISH 2585SLASH: 2586 mov BYTE [r11+1],92 2587 jmp FINISH 2588ZERO: 2589 mov BYTE [r11+1],48 2590FINISH: 2591 mov BYTE [r11],92 2592 add r11,2 2593 jmp START 2594EXIT: 2595 `) 2596 2597val (thm,mc_sym2str_ok_loop_def) = basic_decompile_strings x64_tools "mc_sym2str_ok_loop" 2598 (SOME (``(r0:word64,r8:word64,r9:word64,r10:word64,dg:word64 set,g:word64->word8)``, 2599 ``(r0:word64,r8:word64,r9:word64,r10:word64,dg:word64 set,g:word64->word8)``)) 2600 (assemble "x64" ` 2601START: 2602 cmp r8,r10 2603 je TRUE 2604 movzx r0,BYTE [r9+r8] 2605 inc r8 2606 cmp r0,42 2607 jb FALSE 2608 cmp r0,46 2609 je FALSE 2610 cmp r0,59 2611 je FALSE 2612 cmp r0,124 2613 je FALSE 2614 cmp r0,97 2615 jb START 2616 cmp r0,122 2617 ja START 2618FALSE: 2619 xor r0,r0 2620TRUE: 2621 `) 2622 2623val (thm,mc_sym2str_ok_def) = basic_decompile_strings x64_tools "mc_sym2str_ok" 2624 (SOME (``(r8:word64,r9:word64,r10:word64,dg:word64 set,g:word64->word8)``, 2625 ``(r0:word64,r8:word64,r9:word64,r10:word64,dg:word64 set,g:word64->word8)``)) 2626 (assemble "x64" ` 2627START: 2628 cmp r10,0 2629 je FALSE 2630 movzx r0,BYTE [r9] 2631 cmp r0,57 2632 ja CONTINUE 2633 cmp r0,47 2634 ja FALSE 2635CONTINUE: 2636 mov r0d,1 2637 xor r8,r8 2638 insert mc_sym2str_ok_loop 2639 jmp EXIT 2640FALSE: 2641 xor r0,r0 2642EXIT: 2643 `) 2644 2645val (thm,mc_sym2str_copy_def) = basic_decompile_strings x64_tools "mc_sym2str_copy" 2646 (SOME (``(r8:word64,r9:word64,r10:word64,r11:word64,dg:word64 set,g:word64->word8)``, 2647 ``(r8:word64,r9:word64,r10:word64,r11:word64,dg:word64 set,g:word64->word8)``)) 2648 (assemble "x64" ` 2649START: 2650 movzx r0,BYTE [r9+r8] 2651 inc r8 2652 mov BYTE [r11],r0b 2653 inc r11 2654 cmp r8,r10 2655 jne START 2656 `) 2657 2658val (thm,mc_lookup_sym_def) = basic_decompile_strings x64_tools "mc_lookup_sym" 2659 (SOME (``(r8:word64,r9:word64,dg:word64 set,g:word64->word8)``, 2660 ``(r8:word64,r9:word64,dg:word64 set,g:word64->word8)``)) 2661 (assemble "x64" ` 2662L1: test r8,r8 2663 je L2 2664 movzx r0,BYTE [r9] 2665 add r9,r0 2666 dec r8 2667 jmp L1 2668L2: `) 2669 2670val (thm,mc_sym2str_main_def) = basic_decompile_strings x64_tools "mc_sym2str_main" 2671 (SOME (``(r8:word64,r9:word64,r10:word64,r11:word64,dg:word64 set,g:word64->word8)``, 2672 ``(r8:word64,r9:word64,r10:word64,r11:word64,dg:word64 set,g:word64->word8)``)) 2673 (assemble "x64" ` 2674 insert mc_sym2str_ok 2675 xor r8,r8 2676 test r0,r0 2677 je AUX 2678 insert mc_sym2str_copy 2679 jmp EXIT 2680AUX: 2681 mov BYTE [r11],124 2682 inc r11 2683 insert mc_sym2str_aux 2684 mov BYTE [r11],124 2685 inc r11 2686EXIT: 2687 `) 2688 2689val (thm,mc_sym2str_def) = basic_decompile_strings x64_tools "mc_sym2str" 2690 (SOME (``(r8:word64,r9:word64,r11:word64,dg:word64 set,g:word64->word8)``, 2691 ``(r8:word64,r9:word64,r11:word64,dg:word64 set,g:word64->word8)``)) 2692 (assemble "x64" ` 2693 shr r8,3 2694 insert mc_lookup_sym 2695 movzx r10,BYTE [r9] 2696 inc r9 2697 dec r10 2698 insert mc_sym2str_main 2699 `) 2700 2701val upper_identifier_char_def = Define ` 2702 upper_identifier_char c = identifier_char c /\ ~(is_lower_case c)`; 2703 2704val mc_sym2str_ok_loop_thm = prove( 2705 ``!s n p a. 2706 (one_string (n2w n + r9) s * p) (fun2set (f,df)) /\ 2707 n + LENGTH s < 256 /\ ~(a = 0w) ==> 2708 ?ax r8i. 2709 mc_sym2str_ok_loop_pre (a,n2w n,r9,n2w (n + LENGTH s),df,f) /\ 2710 (mc_sym2str_ok_loop (a,n2w n,r9,n2w (n + LENGTH s),df,f) = 2711 (ax,r8i,r9,n2w (n + LENGTH s),df,f)) /\ 2712 (~(ax = 0w) = EVERY upper_identifier_char s)``, 2713 Induct \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL,LENGTH] 2714 \\ SIMP_TAC std_ss [one_string_def,MAP,one_byte_list_def] 2715 \\ SIMP_TAC std_ss [GSYM one_string_def] 2716 \\ ONCE_REWRITE_TAC [mc_sym2str_ok_loop_def] 2717 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [EVERY_DEF,LET_DEF] 2718 \\ `(n + SUC (STRLEN s)) < 18446744073709551616` by DECIDE_TAC 2719 \\ `n < 18446744073709551616` by DECIDE_TAC 2720 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,DECIDE ``~(n=n+SUC m)``] 2721 \\ SEP_R_TAC 2722 \\ `ORD h < 256` by ASM_SIMP_TAC std_ss [ORD_BOUND] 2723 \\ `ORD h < 18446744073709551616` by DECIDE_TAC 2724 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,ORD_BOUND,word_lo_n2w,n2w_11] 2725 \\ REVERSE (Cases_on `upper_identifier_char h` \\ ASM_SIMP_TAC std_ss []) 2726 THEN1 (FULL_SIMP_TAC std_ss [upper_identifier_char_def,char_le_def, 2727 identifier_char_def,GSYM NOT_LESS,is_lower_case_def, 2728 EVAL ``ORD #"a"``,EVAL ``ORD #"z"``]) 2729 \\ FULL_SIMP_TAC std_ss [upper_identifier_char_def,char_le_def, 2730 identifier_char_def,GSYM NOT_LESS,is_lower_case_def, 2731 EVAL ``ORD #"a"``,EVAL ``ORD #"z"``] 2732 \\ FULL_SIMP_TAC std_ss [word_add_n2w,DECIDE ``n+SUC m = (n+1)+m``] 2733 \\ SEP_I_TAC "mc_sym2str_ok_loop" 2734 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,AC WORD_ADD_ASSOC WORD_ADD_COMM] 2735 \\ SEP_F_TAC \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 2736 \\ `~(ORD h = 0)` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss []) 2737 |> Q.SPECL [`s`,`0`,`p`,`1w`] |> SIMP_RULE wstd_ss [WORD_ADD_0,ADD_CLAUSES,n2w_11] 2738 |> GEN_ALL; 2739 2740val upper_identifier_char_thm = prove( 2741 ``!s. EVERY upper_identifier_char s = 2742 EVERY identifier_char s /\ EVERY (\c. ~is_lower_case c) s``, 2743 Induct \\ ASM_SIMP_TAC std_ss [EVERY_DEF,upper_identifier_char_def] 2744 \\ SIMP_TAC std_ss [AC CONJ_ASSOC CONJ_COMM]); 2745 2746val mc_sym2str_ok_thm = prove( 2747 ``(one_string r9 s * p) (fun2set (f,df)) /\ LENGTH s < 256 ==> 2748 ?ax r8i. 2749 mc_sym2str_ok_pre (r8,r9,n2w (LENGTH s),df,f) /\ 2750 (mc_sym2str_ok (r8,r9,n2w (LENGTH s),df,f) = 2751 (ax,r8i,r9,n2w (LENGTH s),df,f)) /\ 2752 (~(ax = 0w) = identifier_string s /\ EVERY (\c. ~is_lower_case c) s)``, 2753 SIMP_TAC wstd_ss [mc_sym2str_ok_def,n2w_11,LENGTH_NIL] 2754 \\ Cases_on `s = ""` \\ ASM_SIMP_TAC std_ss [LET_DEF] THEN1 EVAL_TAC 2755 \\ ASM_SIMP_TAC std_ss [identifier_string_def] \\ REPEAT STRIP_TAC 2756 \\ `r9 IN df /\ (f r9 = n2w (ORD (HD s)))` by 2757 (Cases_on `s` \\ FULL_SIMP_TAC std_ss [one_string_def,one_byte_list_def,MAP,HD] 2758 \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss []) 2759 \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,word_lo_n2w] 2760 \\ Cases_on `number_char (HD s)` \\ ASM_SIMP_TAC std_ss [] THEN1 2761 (FULL_SIMP_TAC std_ss [number_char_def] \\ ASM_SIMP_TAC std_ss [LESS_EQ] 2762 \\ `~(58 <= ORD (HD s))` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss []) 2763 \\ FULL_SIMP_TAC std_ss [number_char_def] 2764 \\ IMP_RES_TAC mc_sym2str_ok_loop_thm \\ ASM_SIMP_TAC std_ss [] 2765 \\ FULL_SIMP_TAC std_ss [LESS_EQ,upper_identifier_char_thm]); 2766 2767val mc_sym2str_copy_thm = prove( 2768 ``!s t n p r11 f. 2769 (one_string (n2w n + r9) s * one_string r11 t * p) (fun2set (f,df)) /\ 2770 n + LENGTH s < 256 /\ (LENGTH t = LENGTH s) /\ ~(s = "") ==> 2771 ?fi. 2772 mc_sym2str_copy_pre (n2w n,r9,n2w (n + LENGTH s),r11,df,f) /\ 2773 (mc_sym2str_copy (n2w n,r9,n2w (n + LENGTH s),r11,df,f) = 2774 (n2w (n + LENGTH s),r9,n2w (n + LENGTH s),r11 + n2w (LENGTH s),df,fi)) /\ 2775 (one_string (n2w n + r9) s * one_string r11 s * p) (fun2set (fi,df))``, 2776 Induct \\ SIMP_TAC std_ss [] \\ Cases_on `t` \\ SIMP_TAC std_ss [ADD1,LENGTH] 2777 \\ ONCE_REWRITE_TAC [DECIDE ``n+1=1+n:num``] \\ SIMP_TAC std_ss [NOT_CONS_NIL] 2778 \\ SIMP_TAC std_ss [one_string_def,MAP,one_byte_list_def] 2779 \\ SIMP_TAC std_ss [GSYM one_string_def,STAR_ASSOC,ADD_ASSOC] 2780 \\ ONCE_REWRITE_TAC [mc_sym2str_copy_def] \\ REPEAT STRIP_TAC 2781 \\ `n+1 < 256` by DECIDE_TAC 2782 \\ SEP_R_TAC \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,LET_DEF,word_add_n2w,n2w_11] 2783 \\ SEP_W_TAC \\ ASM_SIMP_TAC std_ss [DECIDE ``(n=n+k)=(k=0:num)``,LENGTH_NIL] 2784 \\ Cases_on `s = ""` \\ ASM_SIMP_TAC std_ss [] 2785 THEN1 (Cases_on `t' = ""` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,LENGTH_NIL]) 2786 \\ SEP_I_TAC "mc_sym2str_copy" 2787 \\ POP_ASSUM (MP_TAC o Q.SPECL [`t'`,`one (n2w n + r9,n2w (ORD h')) * 2788 one (r11,n2w (ORD h')) * p`]) 2789 \\ FULL_SIMP_TAC (std_ss++star_ss) [GSYM word_add_n2w,AC WORD_ADD_COMM WORD_ADD_ASSOC]) 2790 |> Q.SPECL [`s`,`t`,`0`,`p`] |> SIMP_RULE wstd_ss [WORD_ADD_0,ADD_CLAUSES,n2w_11] 2791 |> GEN_ALL; 2792 2793val ORD_CHR_IMP = prove(``n<256 ==> (ORD (CHR n) = n)``,METIS_TAC [ORD_CHR]); 2794 2795val mc_sym2str_aux_thm = prove( 2796 ``!s t n p r11 f. 2797 (one_string (n2w n + r9) s * one_string r11 t * p) (fun2set (f,df)) /\ 2798 n + LENGTH s < 256 /\ (LENGTH t = LENGTH (sym2str_aux s)) ==> 2799 ?fi. 2800 mc_sym2str_aux_pre (n2w n,r9,n2w (n + LENGTH s),r11,df,f) /\ 2801 (mc_sym2str_aux (n2w n,r9,n2w (n + LENGTH s),r11,df,f) = 2802 (n2w (n + LENGTH s),r9,n2w (n + LENGTH s),r11 + n2w (LENGTH (sym2str_aux s)),df,fi)) /\ 2803 (one_string (n2w n + r9) s * one_string r11 (sym2str_aux s) * p) (fun2set (fi,df))``, 2804 Induct \\ SIMP_TAC std_ss [sym2str_aux_def,LENGTH,LENGTH_NIL] 2805 THEN1 (ONCE_REWRITE_TAC [mc_sym2str_aux_def] \\ SIMP_TAC std_ss [WORD_ADD_0]) 2806 \\ STRIP_TAC \\ Cases_on `ORD h = 0` THEN1 2807 (Cases_on `t` \\ ASM_SIMP_TAC std_ss [ADD1,LENGTH] 2808 \\ Cases_on `t'` \\ ASM_SIMP_TAC std_ss [ADD1,LENGTH] 2809 \\ ONCE_REWRITE_TAC [DECIDE ``n+1=1+n:num``] 2810 \\ SIMP_TAC std_ss [one_string_def,MAP,one_byte_list_def] 2811 \\ SIMP_TAC std_ss [GSYM one_string_def,STAR_ASSOC,ADD_ASSOC,word_arith_lemma1] 2812 \\ ONCE_REWRITE_TAC [mc_sym2str_aux_def] \\ REPEAT STRIP_TAC 2813 \\ `n < 256` by DECIDE_TAC 2814 \\ SEP_R_TAC \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,LET_DEF,word_add_n2w,n2w_11] 2815 \\ ASM_SIMP_TAC std_ss [DECIDE ``~(n=n+1+k)``,LENGTH_NIL] 2816 \\ ASM_SIMP_TAC std_ss [ORD_CHR_IMP] 2817 \\ SEP_W_TAC 2818 \\ SEP_I_TAC "mc_sym2str_aux" 2819 \\ POP_ASSUM (MP_TAC o Q.SPECL [`t`,`one (n2w n + r9,0x0w) * 2820 one (r11,0x5Cw) * one (r11 + 0x1w,0x30w) * p`]) 2821 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 2822 (Q.PAT_X_ASSUM `ORD h = 0` ASSUME_TAC 2823 \\ FULL_SIMP_TAC (std_ss++star_ss) [GSYM word_add_n2w,AC WORD_ADD_COMM WORD_ADD_ASSOC] 2824 \\ SEP_WRITE_TAC) 2825 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [word_add_n2w] 2826 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,AC WORD_ADD_COMM WORD_ADD_ASSOC] 2827 \\ FULL_SIMP_TAC std_ss [word_add_n2w] 2828 \\ FULL_SIMP_TAC (std_ss++star_ss) [GSYM word_add_n2w,AC WORD_ADD_COMM WORD_ADD_ASSOC]) 2829 \\ ASM_SIMP_TAC std_ss [MEM] 2830 \\ Cases_on `h = #"|"` THEN1 2831 (Cases_on `t` \\ ASM_SIMP_TAC std_ss [ADD1,LENGTH] 2832 \\ Cases_on `t'` \\ ASM_SIMP_TAC std_ss [ADD1,LENGTH] 2833 \\ ONCE_REWRITE_TAC [DECIDE ``n+1=1+n:num``] 2834 \\ SIMP_TAC std_ss [one_string_def,MAP,one_byte_list_def] 2835 \\ SIMP_TAC std_ss [GSYM one_string_def,STAR_ASSOC,ADD_ASSOC,word_arith_lemma1] 2836 \\ ONCE_REWRITE_TAC [mc_sym2str_aux_def] \\ REPEAT STRIP_TAC 2837 \\ `n < 256` by DECIDE_TAC 2838 \\ SEP_R_TAC \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,LET_DEF,word_add_n2w,n2w_11] 2839 \\ ASM_SIMP_TAC std_ss [DECIDE ``~(n=n+1+k)``,LENGTH_NIL] 2840 \\ FULL_SIMP_TAC std_ss [ORD_CHR_IMP] 2841 \\ SEP_W_TAC 2842 \\ SEP_I_TAC "mc_sym2str_aux" 2843 \\ POP_ASSUM (MP_TAC o Q.SPECL [`t`,`one (n2w n + r9,0x7Cw) * 2844 one (r11,0x5Cw) * one (r11 + 0x1w,0x7Cw) * p`]) 2845 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [] 2846 \\ FULL_SIMP_TAC (std_ss++star_ss) [GSYM word_add_n2w,AC WORD_ADD_COMM WORD_ADD_ASSOC] 2847 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [word_add_n2w]) 2848 \\ Cases_on `h = #"\\"` THEN1 2849 (Cases_on `t` \\ ASM_SIMP_TAC std_ss [ADD1,LENGTH] 2850 \\ Cases_on `t'` \\ ASM_SIMP_TAC std_ss [ADD1,LENGTH] 2851 \\ ONCE_REWRITE_TAC [DECIDE ``n+1=1+n:num``] 2852 \\ SIMP_TAC std_ss [one_string_def,MAP,one_byte_list_def] 2853 \\ SIMP_TAC std_ss [GSYM one_string_def,STAR_ASSOC,ADD_ASSOC,word_arith_lemma1] 2854 \\ ONCE_REWRITE_TAC [mc_sym2str_aux_def] \\ REPEAT STRIP_TAC 2855 \\ `n < 256` by DECIDE_TAC 2856 \\ SEP_R_TAC \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,LET_DEF,word_add_n2w,n2w_11] 2857 \\ ASM_SIMP_TAC std_ss [DECIDE ``~(n=n+1+k)``,LENGTH_NIL] 2858 \\ FULL_SIMP_TAC std_ss [ORD_CHR_IMP] 2859 \\ SEP_W_TAC 2860 \\ SEP_I_TAC "mc_sym2str_aux" 2861 \\ POP_ASSUM (MP_TAC o Q.SPECL [`t`,`one (n2w n + r9,0x5Cw) * 2862 one (r11,0x5Cw) * one (r11 + 0x1w,0x5Cw) * p`]) 2863 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [] 2864 \\ FULL_SIMP_TAC (std_ss++star_ss) [GSYM word_add_n2w,AC WORD_ADD_COMM WORD_ADD_ASSOC] 2865 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [word_add_n2w]) 2866 \\ ASM_SIMP_TAC std_ss [] 2867 \\ Cases_on `t` \\ SIMP_TAC std_ss [ADD1,LENGTH] 2868 \\ ONCE_REWRITE_TAC [DECIDE ``n+1=1+n:num``] \\ SIMP_TAC std_ss [NOT_CONS_NIL] 2869 \\ SIMP_TAC std_ss [one_string_def,MAP,one_byte_list_def] 2870 \\ SIMP_TAC std_ss [GSYM one_string_def,STAR_ASSOC,ADD_ASSOC] 2871 \\ ONCE_REWRITE_TAC [mc_sym2str_aux_def] \\ REPEAT STRIP_TAC 2872 \\ `n < 256` by DECIDE_TAC 2873 \\ ASM_SIMP_TAC wstd_ss [DECIDE ``~(n=n+1+k)``,LENGTH_NIL,n2w_11,LET_DEF] 2874 \\ SEP_R_TAC \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,LET_DEF,word_add_n2w,n2w_11] 2875 \\ FULL_SIMP_TAC std_ss [GSYM ORD_11,ORD_CHR_IMP] 2876 \\ SEP_W_TAC \\ ASM_SIMP_TAC std_ss [LENGTH_NIL] 2877 \\ SEP_I_TAC "mc_sym2str_aux" 2878 \\ POP_ASSUM (MP_TAC o Q.SPECL [`t'`,`one (n2w n + r9,n2w (ORD h)) * 2879 one (r11,n2w (ORD h)) * p`]) 2880 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [] 2881 \\ FULL_SIMP_TAC (std_ss++star_ss) [GSYM word_add_n2w,AC WORD_ADD_COMM WORD_ADD_ASSOC]); 2882 2883val mc_sym2str_thm = prove( 2884 ``(one_string r9 s * one_string r11 t * p) (fun2set (f,df)) /\ 2885 LENGTH s < 256 /\ (LENGTH t = LENGTH (sym2str s)) ==> 2886 ?fi r8i r9i. 2887 mc_sym2str_main_pre (r8,r9,n2w (LENGTH s),r11,df,f) /\ 2888 (mc_sym2str_main (r8,r9,n2w (LENGTH s),r11,df,f) = 2889 (r8i,r9i,n2w (LENGTH s),r11 + n2w (LENGTH (sym2str s)),df,fi)) /\ 2890 (one_string r9 s * one_string r11 (sym2str s) * p) (fun2set (fi,df))``, 2891 SIMP_TAC std_ss [mc_sym2str_main_def] \\ REPEAT STRIP_TAC 2892 \\ FULL_SIMP_TAC std_ss [GSYM STAR_ASSOC] 2893 \\ IMP_RES_TAC mc_sym2str_ok_thm \\ POP_ASSUM (MP_TAC o Q.SPEC `r8`) 2894 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [LET_DEF] 2895 \\ `sym2str s = if ax = 0w then "|" ++ sym2str_aux s ++ "|" else s` by 2896 (SIMP_TAC std_ss [sym2str_def] \\ METIS_TAC []) 2897 \\ `~(ax = 0w) ==> ~(s = "")` by 2898 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [identifier_string_def]) 2899 \\ Q.PAT_X_ASSUM `ax <> 0x0w <=> bbb` (K ALL_TAC) 2900 \\ REVERSE (Cases_on `ax = 0w`) \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] 2901 THEN1 (IMP_RES_TAC mc_sym2str_copy_thm \\ ASM_SIMP_TAC std_ss []) 2902 \\ FULL_SIMP_TAC std_ss [APPEND,APPEND_ASSOC,LENGTH] 2903 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 2904 \\ Cases_on `t' = []` THEN1 (FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND,ADD1]) 2905 \\ `?h2 ts. t' = SNOC h2 ts` by METIS_TAC [rich_listTheory.SNOC_CASES] 2906 \\ FULL_SIMP_TAC std_ss [SNOC_APPEND,LENGTH_APPEND,LENGTH] 2907 \\ FULL_SIMP_TAC std_ss [one_string_def,one_byte_list_APPEND,MAP,MAP_APPEND,one_byte_list_def] 2908 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,GSYM one_string_def,SEP_CLAUSES,LENGTH_MAP] 2909 \\ SIMP_TAC std_ss [ORD_CHR_RWT] 2910 \\ `(one_string r9 s * one_string (r11 + 0x1w) ts * (one (r11,0x7Cw) * 2911 one (r11 + 0x1w + n2w (STRLEN (sym2str_aux s)),n2w (ORD h2)) * p)) 2912 (fun2set ((r11 =+ 0x7Cw) f,df))` by SEP_WRITE_TAC 2913 \\ IMP_RES_TAC (SIMP_RULE std_ss [WORD_ADD_0] (Q.SPECL [`s`,`t`,`0`] mc_sym2str_aux_thm)) 2914 \\ ASM_SIMP_TAC std_ss [] 2915 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,AC ADD_ASSOC ADD_COMM] 2916 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC); 2917 2918 2919(* printing lemmas *) 2920 2921val LENGTH_EXPAND = prove( 2922 ``((LENGTH xs = 1) ==> (?x0. xs = [x0])) /\ 2923 ((LENGTH xs = 2) ==> (?x0 x1. xs = [x0;x1])) /\ 2924 ((LENGTH xs = 3) ==> (?x0 x1 x2. xs = [x0;x1;x2])) /\ 2925 ((LENGTH xs = 4) ==> (?x0 x1 x2 x3. xs = [x0;x1;x2;x3]))``, 2926 Cases_on `xs` \\ ASM_SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 2927 \\ Cases_on `t` \\ ASM_SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 2928 \\ Cases_on `t'` \\ ASM_SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 2929 \\ Cases_on `t` \\ ASM_SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 2930 \\ Cases_on `t'` \\ ASM_SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 2931 \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL] \\ DECIDE_TAC); 2932 2933val null_term_str_CONS_NOT_NIL = prove( 2934 ``!a s t. null_term_str a dg g (x::xs) /\ null_term_str a dg g "" ==> (HD [2] = 5)``, 2935 SIMP_TAC std_ss [null_term_str_def,APPEND] 2936 \\ SIMP_TAC std_ss [one_string_def,MAP,EVERY_DEF,one_byte_list_def, 2937 ORD_CHR_RWT,SEP_CLAUSES] 2938 \\ REPEAT STRIP_TAC 2939 \\ `g a = 0w` by SEP_READ_TAC 2940 \\ `g a = n2w (ORD x)` by SEP_READ_TAC 2941 \\ FULL_SIMP_TAC wstd_ss [n2w_11] 2942 \\ Cases_on `x` \\ FULL_SIMP_TAC std_ss [ORD_CHR_RWT]) 2943 |> SIMP_RULE std_ss [HD]; 2944 2945val null_term_str_CONS = prove( 2946 ``null_term_str a dg g (x::xs) ==> null_term_str (a+1w) dg g xs /\ (g a = n2w (ORD x))``, 2947 SIMP_TAC std_ss [null_term_str_def,APPEND,one_string_def, 2948 one_byte_list_def,MAP,EVERY_DEF] \\ REPEAT STRIP_TAC 2949 THEN1 (Q.EXISTS_TAC `p * one (a,n2w (ORD x))` \\ FULL_SIMP_TAC (std_ss++star_ss) []) 2950 \\ SEP_R_TAC); 2951 2952val null_term_str_unique = prove( 2953 ``!a s t. null_term_str a dg g s /\ null_term_str a dg g t ==> (s = t)``, 2954 Induct_on `s` THEN1 2955 (Cases_on `t` \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL] 2956 \\ METIS_TAC [null_term_str_CONS_NOT_NIL]) 2957 \\ Cases_on `t` THEN1 2958 (ASM_SIMP_TAC std_ss [NOT_CONS_NIL] 2959 \\ METIS_TAC [null_term_str_CONS_NOT_NIL]) 2960 \\ REPEAT STRIP_TAC \\ SIMP_TAC std_ss [CONS_11] 2961 \\ IMP_RES_TAC null_term_str_CONS \\ RES_TAC 2962 \\ FULL_SIMP_TAC wstd_ss [n2w_11,ORD_11]); 2963 2964val null_term_str_IMP = prove( 2965 ``null_term_str a dg g s ==> (mem2string a dg g = s) /\ exists_null_term_str a dg g``, 2966 SIMP_TAC std_ss [mem2string_def,exists_null_term_str_def] 2967 \\ METIS_TAC [null_term_str_unique]); 2968 2969 2970(* print a newline character *) 2971 2972val (mc_print_nl_spec,mc_print_nl_def) = basic_decompile_strings x64_tools "mc_print_nl" 2973 (SOME (``(ior:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``, 2974 ``(ior:word64,r0:word64,r1:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``)) 2975 (assemble "x64" ` 2976 mov r1,[r7-192] 2977 mov r0,[r7-216] 2978 mov BYTE [r0], 10 2979 mov BYTE [r0+1], 0 2980 insert io_write 2981 mov r0d,3 2982 mov r1d,1 2983 `); 2984 2985val _ = save_thm("mc_print_nl_spec",mc_print_nl_spec); 2986 2987val mc_print_nl_thm = store_thm("mc_print_nl_thm", 2988 ``^LISP ==> 2989 ?g2. mc_print_nl_pre (EL 0 cs,sp,df,f,dg,g,io) /\ 2990 (mc_print_nl (EL 0 cs,sp,df,f,dg,g,io) = 2991 (EL 0 cs,tw0,tw1,sp,df,f,dg,g2,IO_WRITE io "\n")) /\ 2992 let (g,io) = (g2,IO_WRITE io "\n") in ^LISP``, 2993 SIMP_TAC std_ss [LET_DEF,mc_print_nl_def] \\ STRIP_TAC 2994 \\ IMP_RES_TAC lisp_inv_cs_read 2995 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 2996 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 2997 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 2998 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 2999 \\ IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPECL [`2`,`[10w;0w]`] lisp_inv_temp_string)) 3000 \\ FULL_SIMP_TAC std_ss [LENGTH] 3001 \\ Q.ABBREV_TAC `g3 = (sa2 + 0x1w =+ 0x0w) ((sa2 =+ 0xAw) g)` 3002 \\ IMP_RES_TAC LENGTH_EXPAND 3003 \\ `(one_byte_list sa2 [0xAw; 0x0w] * p) (fun2set (g3,dg)) /\ 3004 sa2 IN dg /\ sa2+1w IN dg` by 3005 (Q.UNABBREV_TAC `g3` 3006 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,SEP_CLAUSES,STAR_ASSOC] 3007 \\ SEP_R_TAC \\ SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 3008 \\ `null_term_str sa2 dg g3 "\n"` by 3009 (FULL_SIMP_TAC std_ss [null_term_str_def,one_string_def,MAP,APPEND, 3010 ORD_CHR_RWT,EVERY_DEF,CHR_11] \\ METIS_TAC []) 3011 \\ IMP_RES_TAC null_term_str_IMP 3012 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [lisp_inv_ignore_io]); 3013 3014 3015(* print num *) 3016 3017val (thm,mc_print_num_def) = basic_decompile_strings x64_tools "mc_print_num" 3018 (SOME (``(ior:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``, 3019 ``(ior:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``)) 3020 (assemble "x64" ` 3021 mov r11,[r7-216] 3022 insert mc_num2str 3023 mov BYTE [r11], 0 3024 mov r1,[r7-192] 3025 mov r0,[r7-216] 3026 insert io_write 3027 `); 3028 3029val mc_print_num_thm = prove( 3030 ``^LISP ==> 3031 n < 2**30 ==> 3032 ?g2. mc_print_num_pre (EL 0 cs,sp,n2w n << 2 !! 1w,df,f,dg,g,io)/\ 3033 (mc_print_num (EL 0 cs,sp,n2w n << 2 !! 1w,df,f,dg,g,io) = 3034 (EL 0 cs,sp,df,f,dg,g2,IO_WRITE io (num2str n))) /\ 3035 let (g,io) = (g2,IO_WRITE io (num2str n)) in ^LISP``, 3036 SIMP_TAC std_ss [LET_DEF,mc_print_num_def] \\ STRIP_TAC 3037 \\ IMP_RES_TAC lisp_inv_cs_read 3038 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 3039 \\ Q.PAT_X_ASSUM `lisp_inv xx yyy zzz` MP_TAC 3040 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 3041 \\ REPEAT STRIP_TAC 3042 \\ IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPECL [`LENGTH (num2str n) + 1`,`MAP (n2w o ORD) (num2str n) ++ [0w]`] lisp_inv_temp_string)) 3043 \\ POP_ASSUM (MP_TAC o Q.SPEC `n`) 3044 \\ `LENGTH (num2str n) <= 10` by METIS_TAC [EVAL ``(2**30):num``,mc_num2strlen_thm] 3045 \\ `STRLEN (num2str n) + 1 <= 520` by DECIDE_TAC 3046 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 3047 \\ `(str = []) \/ ?x l. str = SNOC x l` by METIS_TAC [rich_listTheory.SNOC_CASES] 3048 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,SNOC_APPEND,LENGTH_APPEND,one_byte_list_APPEND] 3049 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,SEP_CLAUSES,LENGTH_MAP,GSYM STAR_ASSOC] 3050 \\ ASSUME_TAC (GEN_ALL mc_num2str_thm) 3051 \\ SEP_I_TAC "mc_num2str" 3052 \\ POP_ASSUM (MP_TAC o Q.SPECL [`l`,`one (sa2 + n2w (STRLEN (num2str n)),x) * p`]) 3053 \\ ASM_SIMP_TAC std_ss [] 3054 \\ Q.PAT_X_ASSUM `LENGTH l = sss` ASSUME_TAC 3055 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 3056 \\ ASM_SIMP_TAC std_ss [] 3057 \\ Q.ABBREV_TAC `g3 = (sa2 + n2w (STRLEN (num2str n)) =+ 0x0w) g1` 3058 \\ `(one_string sa2 (num2str n) * 3059 (one (sa2 + n2w (STRLEN (num2str n)),0w) * p)) (fun2set (g3,dg))` by 3060 (Q.UNABBREV_TAC `g3` \\ SEP_WRITE_TAC) 3061 \\ `null_term_str sa2 dg g3 (num2str n)` by 3062 (FULL_SIMP_TAC std_ss [null_term_str_def,one_string_def,one_byte_list_APPEND, 3063 MAP_APPEND,MAP,SEP_CLAUSES,LENGTH_MAP,one_byte_list_def,ORD_CHR_RWT] 3064 \\ Q.EXISTS_TAC `p` \\ FULL_SIMP_TAC (std_ss++star_ss) [] 3065 \\ STRIP_ASSUME_TAC (Q.SPEC `n` str2num_num2str) 3066 \\ POP_ASSUM MP_TAC \\ MATCH_MP_TAC MONO_EVERY \\ Cases 3067 \\ FULL_SIMP_TAC std_ss [number_char_def,CHR_11,ORD_CHR_RWT] \\ DECIDE_TAC) 3068 \\ IMP_RES_TAC null_term_str_IMP \\ ASM_SIMP_TAC std_ss [] 3069 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] \\ SEP_R_TAC 3070 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3] 3071 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_io) \\ Q.EXISTS_TAC `io` 3072 \\ Q.PAT_X_ASSUM `!g2. bbb` MATCH_MP_TAC 3073 \\ FULL_SIMP_TAC (std_ss++star_ss) [one_string_def]) 3074 |> SIMP_RULE std_ss [LET_DEF]; 3075 3076val (mc_print_num_full_spec,mc_print_num_full_def) = basic_decompile_strings x64_tools "mc_print_num_full" 3077 (SOME (``(ior:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``, 3078 ``(ior:word64,r0:word64,r1:word64,r2:word64,r7:word64,r8:word64,r9:word64,r10:word64,r11:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``)) 3079 (assemble "x64" ` 3080 insert mc_print_num 3081 mov r0d,3 3082 mov r1d,1 3083 mov r2d,r0d 3084 mov r8d,r0d 3085 mov r9d,r0d 3086 mov r10d,r0d 3087 mov r11d,r0d 3088 `); 3089 3090val _ = save_thm("mc_print_num_full_spec",mc_print_num_full_spec); 3091 3092val mc_print_num_full_blast = blastLib.BBLAST_PROVE 3093 ``w2w (w !! 0x1w) = w2w (w:word32) !! 1w:word64`` 3094 3095val lisp_inv_nil_lemma = el 1 (CONJUNCTS lisp_inv_Sym) 3096 |> UNDISCH |> CONJUNCTS |> hd |> DISCH_ALL |> GEN_ALL 3097 3098val mc_print_num_full_thm = prove( 3099 ``^LISP ==> 3100 isVal x0 ==> 3101 ?g2 v0 v1 v2 v3 v4. 3102 mc_print_num_full_pre (EL 0 cs,sp,w2w w0,df,f,dg,g,io)/\ 3103 (mc_print_num_full (EL 0 cs,sp,w2w w0,df,f,dg,g,io) = 3104 (EL 0 cs,tw0,tw1,tw0,sp,w2w v0,w2w v1,w2w v2,w2w v3,df,f,dg,g2,IO_WRITE io (num2str (getVal x0)))) /\ 3105 let (g,io,w0,w1,w2,w3,x0,x1,x2,x3,tw2) = 3106 (g2,IO_WRITE io (num2str (getVal x0)),v0,v1,v2,v3,Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL",tw0) 3107 in ^LISP``, 3108 REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [isVal_thm] \\ FULL_SIMP_TAC std_ss [] 3109 \\ SIMP_TAC std_ss [mc_print_num_full_def,LET_DEF,EVAL ``(31 -- 0) 3w:word64``] 3110 \\ `(w0 = n2w a << 2 !! 1w) /\ a < 2**30` by 3111 (FULL_SIMP_TAC std_ss [lisp_inv_def,MAP,EVERY_DEF,CONS_11,lisp_x_def] 3112 \\ Q.PAT_X_ASSUM `ref_heap_addr s0 = w0` (ASSUME_TAC o GSYM) 3113 \\ FULL_SIMP_TAC wstd_ss [ref_heap_addr_def,w2w_def,w2n_n2w]) 3114 \\ FULL_SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w,mc_print_num_full_blast] 3115 \\ `(4 * a) < 4294967296` by DECIDE_TAC 3116 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w] 3117 \\ IMP_RES_TAC (SIMP_RULE std_ss [WORD_MUL_LSL,word_mul_n2w] mc_print_num_thm) 3118 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3119 \\ ASM_SIMP_TAC std_ss [getVal_def] 3120 \\ Q.LIST_EXISTS_TAC [`3w`,`3w`,`3w`,`3w`] \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w] 3121 \\ MATCH_MP_TAC lisp_inv_nil_lemma \\ Q.LIST_EXISTS_TAC [`x3`,`w3`] 3122 \\ MATCH_MP_TAC lisp_inv_swap3 3123 \\ MATCH_MP_TAC lisp_inv_nil_lemma \\ Q.LIST_EXISTS_TAC [`x2`,`w2`] 3124 \\ MATCH_MP_TAC lisp_inv_swap2 3125 \\ MATCH_MP_TAC lisp_inv_nil_lemma \\ Q.LIST_EXISTS_TAC [`x1`,`w1`] 3126 \\ MATCH_MP_TAC lisp_inv_swap1 3127 \\ MATCH_MP_TAC lisp_inv_nil_lemma 3128 \\ Q.LIST_EXISTS_TAC [`Val a`,`n2w (4 * a) !! 1w`] 3129 \\ MATCH_MP_TAC lisp_inv_ignore_tw2 \\ ASM_SIMP_TAC std_ss []) 3130 |> SIMP_RULE std_ss [LET_DEF]; 3131 3132val _ = save_thm("mc_print_num_full_thm",mc_print_num_full_thm); 3133 3134 3135(* print symbol *) 3136 3137val (thm,mc_print_sym_def) = basic_decompile_strings x64_tools "mc_print_sym" 3138 (SOME (``(ior:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``, 3139 ``(ior:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``)) 3140 (assemble "x64" ` 3141 shr r8,3 3142 mov r9,[r7-224] 3143 insert mc_lookup_sym 3144 movzx r10,BYTE [r9] 3145 inc r9 3146 dec r10 3147 mov r11,[r7-216] 3148 insert mc_sym2str_main 3149 mov BYTE [r11], 0 3150 mov r1,[r7-192] 3151 mov r0,[r7-216] 3152 insert io_write 3153 `); 3154 3155val mc_lookup_sym_thm = prove( 3156 ``!xs a k i p. 3157 (LIST_FIND k s xs = SOME (k+i)) /\ i < 2**32 /\ 3158 EVERY (\x. LENGTH x < 255) xs /\ 3159 (one_byte_list a (symbol_list xs) * p) (fun2set (g,dg)) ==> 3160 ?a2 q. mc_lookup_sym_pre (n2w i,a,dg,g) /\ 3161 (mc_lookup_sym (n2w i,a,dg,g) = (0w,a2,dg,g)) /\ 3162 (one_byte_list a2 (string_data s) * q * p) (fun2set (g,dg)) /\ 3163 (one_byte_list a2 (string_data s) * q = one_byte_list a (symbol_list xs))``, 3164 Induct \\ SIMP_TAC std_ss [LIST_FIND_def] \\ REPEAT STRIP_TAC 3165 \\ Cases_on `s = h` \\ FULL_SIMP_TAC std_ss [] THEN1 3166 (`i = 0` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 3167 \\ ONCE_REWRITE_TAC [mc_lookup_sym_def] \\ FULL_SIMP_TAC std_ss [] 3168 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [one_symbol_list_def,SEP_CLAUSES, 3169 SEP_EXISTS_THM,cond_STAR,symbol_list_def,one_byte_list_APPEND] 3170 \\ Q.EXISTS_TAC `one_byte_list (a + n2w (LENGTH (string_data h))) 3171 (symbol_list xs)` 3172 \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ METIS_TAC []) 3173 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [one_symbol_list_def,SEP_CLAUSES, 3174 SEP_EXISTS_THM,cond_STAR,symbol_list_def,RW1[STAR_COMM]one_byte_list_APPEND] 3175 \\ ONCE_REWRITE_TAC [mc_lookup_sym_def] \\ FULL_SIMP_TAC std_ss [] 3176 \\ `i < 18446744073709551616` by DECIDE_TAC 3177 \\ IMP_RES_TAC LIST_FIND_LESS_EQ 3178 \\ `~(i = 0)` by DECIDE_TAC 3179 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LET_DEF] 3180 \\ Cases_on `i` \\ FULL_SIMP_TAC std_ss [] 3181 \\ ASM_SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB] 3182 \\ FULL_SIMP_TAC std_ss [string_data_def,one_byte_list_def,STAR_ASSOC] 3183 \\ SEP_R_TAC 3184 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,EVERY_DEF] 3185 \\ `(STRLEN h + 1) < 256` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 3186 \\ `n < 4294967296` by DECIDE_TAC 3187 \\ SEP_I_TAC "mc_lookup_sym" \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `k+1`) 3188 \\ FULL_SIMP_TAC std_ss [DECIDE ``k + SUC n = k + 1 + n``] 3189 \\ POP_ASSUM MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 3190 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_MAP,ADD1] \\ SEP_F_TAC 3191 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 3192 \\ POP_ASSUM (MP_TAC o GSYM) \\ FULL_SIMP_TAC std_ss [] 3193 \\ REPEAT STRIP_TAC 3194 \\ Q.EXISTS_TAC `q * one (a,n2w (STRLEN h + 1)) * one_byte_list (a + 0x1w) (MAP (n2w o ORD) h)` 3195 \\ FULL_SIMP_TAC (std_ss++star_ss) []); 3196 3197val mc_print_sym_blast = blastLib.BBLAST_PROVE 3198 ``w2w (w2w (w:29 word) << 3 !! 0x3w:word32) >>> 3 = (w2w w):word64`` 3199 3200val LENGTH_sym2str = prove( 3201 ``!s. LENGTH (sym2str s) <= 2 * LENGTH s + 2``, 3202 SIMP_TAC std_ss [sym2str_def] \\ SRW_TAC [] [] THEN1 DECIDE_TAC 3203 \\ ASM_SIMP_TAC std_ss [ADD1,GSYM ADD_ASSOC] \\ POP_ASSUM (K ALL_TAC) 3204 \\ Induct_on `s` \\ ASM_SIMP_TAC std_ss [LENGTH,sym2str_aux_def] 3205 \\ SRW_TAC [] [LENGTH] \\ DECIDE_TAC); 3206 3207val one_string_MAP = prove( 3208 ``!xs a. one_string a (MAP (CHR o w2n) xs) = one_byte_list a xs``, 3209 Induct \\ FULL_SIMP_TAC std_ss [one_string_def,MAP,one_byte_list_def] 3210 \\ REPEAT STRIP_TAC \\ sg `n2w (ORD (CHR (w2n h))) = h` 3211 \\ FULL_SIMP_TAC std_ss [] \\ Cases_on `h` 3212 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w,ORD_CHR_RWT]); 3213 3214val EVERY_NOT_NULL_sym2str = prove( 3215 ``!s. EVERY (\x. x <> CHR 0) (sym2str s)``, 3216 SIMP_TAC std_ss [sym2str_def] \\ SRW_TAC [] [] THEN1 3217 (FULL_SIMP_TAC std_ss [identifier_string_def] 3218 \\ Q.PAT_X_ASSUM `EVERY identifier_char s` MP_TAC \\ MATCH_MP_TAC MONO_EVERY 3219 \\ FULL_SIMP_TAC std_ss [identifier_char_def,ORD_CHR_RWT]) 3220 \\ POP_ASSUM (K ALL_TAC) \\ Induct_on `s` 3221 \\ SRW_TAC [] [sym2str_aux_def,EVERY_DEF,CHR_11] 3222 \\ SRW_TAC [] [sym2str_aux_def,EVERY_DEF,CHR_11] 3223 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [ORD_CHR_RWT,CHR_11]); 3224 3225val mc_print_sym_thm = prove( 3226 ``(let x0 = Sym s in ^LISP) ==> 3227 ?g2. mc_print_sym_pre (EL 0 cs,sp,w2w w0,df,f,dg,g,io) /\ 3228 (mc_print_sym (EL 0 cs,sp,w2w w0,df,f,dg,g,io) = 3229 (EL 0 cs,sp,df,f,dg,g2,IO_WRITE io (sym2str s))) /\ 3230 (let (x0,g,io) = (Sym s,g2,IO_WRITE io (sym2str s)) in ^LISP)``, 3231 SIMP_TAC std_ss [LET_DEF,mc_print_sym_def] \\ STRIP_TAC 3232 \\ IMP_RES_TAC lisp_inv_cs_read 3233 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 3234 \\ Q.PAT_X_ASSUM `lisp_inv xx yyy zzz` MP_TAC 3235 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 3236 \\ REPEAT STRIP_TAC 3237 \\ Q.PAT_X_ASSUM `lisp_inv xx yyy zzz` MP_TAC 3238 \\ SIMP_TAC std_ss [Once lisp_inv_def] 3239 \\ FULL_SIMP_TAC std_ss [symtable_inv_def] \\ REPEAT STRIP_TAC 3240 \\ FULL_SIMP_TAC std_ss [one_symbol_list_def,SEP_EXISTS_THM,cond_STAR] 3241 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,lisp_x_def] 3242 \\ Q.PAT_X_ASSUM `MAP ref_heap_addr xx = yy` (MP_TAC o GSYM) 3243 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11] \\ REPEAT STRIP_TAC 3244 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,mc_print_sym_blast] 3245 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,one_byte_list_APPEND] 3246 \\ ASSUME_TAC (GEN_ALL (SIMP_RULE std_ss [ADD_CLAUSES] (Q.SPECL [`xs`,`a`,`0`] mc_lookup_sym_thm))) 3247 \\ SEP_I_TAC "mc_lookup_sym" 3248 \\ POP_ASSUM (MP_TAC o Q.SPECL [`INIT_SYMBOLS ++ sym`,`s`,`one_byte_list 3249 (sa1 + n2w (LENGTH (symbol_list (INIT_SYMBOLS ++ sym)))) ys`]) 3250 \\ `k < 4294967296` by DECIDE_TAC 3251 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 3252 \\ ASM_SIMP_TAC std_ss [] 3253 \\ POP_ASSUM (ASSUME_TAC o GSYM) 3254 \\ FULL_SIMP_TAC std_ss [string_data_def,one_byte_list_def,STAR_ASSOC] 3255 \\ `(n2w (w2n (g a2')) - 0x1w = (n2w (LENGTH s)):word64) /\ 3256 LENGTH s < 256` by 3257 (SEP_R_TAC \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] \\ IMP_RES_TAC LIST_FIND_MEM 3258 \\ FULL_SIMP_TAC std_ss [EVERY_MEM] \\ RES_TAC 3259 \\ `LENGTH s + 1 < 256 /\ LENGTH s < 256` by DECIDE_TAC 3260 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w,GSYM word_add_n2w,WORD_ADD_SUB]) 3261 \\ FULL_SIMP_TAC std_ss [GSYM one_string_def] 3262 \\ Q.ABBREV_TAC `syml = LENGTH (symbol_list (INIT_SYMBOLS ++ sym))` 3263 \\ `LENGTH (sym2str s) < LENGTH ys` by 3264 (MATCH_MP_TAC LESS_EQ_LESS_TRANS \\ Q.EXISTS_TAC `2 * LENGTH s + 2` 3265 \\ ASM_SIMP_TAC std_ss [LENGTH_sym2str] \\ DECIDE_TAC) 3266 \\ IMP_RES_TAC SPLIT_LIST 3267 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND,one_byte_list_def,STAR_ASSOC] 3268 \\ ASSUME_TAC (GEN_ALL mc_sym2str_thm) 3269 \\ SEP_I_TAC "mc_sym2str_main" 3270 \\ POP_ASSUM (MP_TAC o Q.SPECL [`MAP (CHR o w2n) (xs1':word8 list)`,`one (a2',n2w (STRLEN s + 1)) * q * 3271 one (sa1 + n2w syml + n2w (STRLEN (sym2str s)),x) * 3272 one_byte_list (sa1 + n2w syml + n2w (STRLEN (sym2str s)) + 0x1w) 3273 xs2`]) 3274 \\ FULL_SIMP_TAC (std_ss++star_ss) [LENGTH_MAP,one_string_MAP] 3275 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] \\ REPEAT STRIP_TAC 3276 \\ ASM_SIMP_TAC std_ss [] 3277 \\ Q.ABBREV_TAC `gi = ((sa1 + n2w syml + n2w (STRLEN (sym2str s)) =+ 0x0w) fi)` 3278 \\ `(q * one_string (sa1 + n2w syml) (sym2str s) * 3279 one_string (a2' + 0x1w) s * one (a2',n2w (STRLEN s + 1)) * 3280 one (sa1 + n2w syml + n2w (STRLEN (sym2str s)),0w) * 3281 one_byte_list (sa1 + n2w syml + n2w (STRLEN (sym2str s)) + 0x1w) 3282 xs2) (fun2set (gi,dg))` 3283 by (Q.UNABBREV_TAC `gi` \\ SEP_WRITE_TAC) 3284 \\ SEP_R_TAC 3285 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3286 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3] 3287 \\ `null_term_str (sa1 + n2w syml) dg gi (sym2str s)` by 3288 (FULL_SIMP_TAC std_ss [null_term_str_def] 3289 \\ Q.EXISTS_TAC `q * 3290 one_string (a2' + 0x1w) s * one (a2',n2w (STRLEN s + 1)) * 3291 one_byte_list (sa1 + n2w syml + n2w (STRLEN (sym2str s)) + 0x1w) 3292 xs2` 3293 \\ FULL_SIMP_TAC std_ss [one_string_def,one_byte_list_APPEND,LENGTH_MAP, 3294 one_byte_list_def,SEP_CLAUSES,MAP,ORD_CHR_RWT,MAP_APPEND] 3295 \\ FULL_SIMP_TAC (std_ss++star_ss) [LENGTH_MAP,one_string_MAP, 3296 EVERY_NOT_NULL_sym2str]) 3297 \\ IMP_RES_TAC null_term_str_IMP \\ ASM_SIMP_TAC std_ss [] 3298 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_io) \\ Q.EXISTS_TAC `io` 3299 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 3300 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 3301 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,MAP,CONS_11,ref_heap_addr_def] 3302 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,lisp_x_def] 3303 \\ FULL_SIMP_TAC std_ss [symtable_inv_def,one_symbol_list_def,SEP_EXISTS_THM, 3304 cond_STAR,one_byte_list_APPEND] 3305 \\ Q.EXISTS_TAC `MAP (n2w o ORD) (sym2str s) ++ 0w::xs2` 3306 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH_MAP,MAP,LENGTH, 3307 one_byte_list_APPEND,one_byte_list_def] 3308 \\ Q.UNABBREV_TAC `syml` 3309 \\ FULL_SIMP_TAC (std_ss++star_ss) [GSYM one_string_def]) 3310 |> SIMP_RULE std_ss [LET_DEF]; 3311 3312val (mc_print_sym_full_spec,mc_print_sym_full_def) = basic_decompile_strings x64_tools "mc_print_sym_full" 3313 (SOME (``(ior:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``, 3314 ``(ior:word64,r0:word64,r1:word64,r7:word64,r8:word64,r9:word64,r10:word64,r11:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``)) 3315 (assemble "x64" ` 3316 insert mc_print_sym 3317 mov r0d,3 3318 mov r1d,1 3319 mov r8d,r0d 3320 mov r9d,r0d 3321 mov r10d,r0d 3322 mov r11d,r0d 3323 `); 3324 3325val _ = save_thm("mc_print_sym_full_spec",mc_print_sym_full_spec); 3326 3327val mc_print_sym_full_blast = blastLib.BBLAST_PROVE 3328 ``w2w (w !! 0x1w) = w2w (w:word32) !! 1w:word64`` 3329 3330val lisp_inv_nil_lemma = el 1 (CONJUNCTS lisp_inv_Sym) 3331 |> UNDISCH |> CONJUNCTS |> hd |> DISCH_ALL |> GEN_ALL 3332 3333val mc_print_sym_full_thm = prove( 3334 ``^LISP ==> 3335 isSym x0 ==> 3336 ?g2 v0 v1 v2 v3 v4. 3337 mc_print_sym_full_pre (EL 0 cs,sp,w2w w0,df,f,dg,g,io)/\ 3338 (mc_print_sym_full (EL 0 cs,sp,w2w w0,df,f,dg,g,io) = 3339 (EL 0 cs,tw0,tw1,sp,w2w v0,w2w v1,w2w v2,w2w v3,df,f,dg,g2,IO_WRITE io (sym2str (getSym x0)))) /\ 3340 let (g,io,w0,w1,w2,w3,x0,x1,x2,x3) = 3341 (g2,IO_WRITE io (sym2str (getSym x0)),v0,v1,v2,v3,Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL") 3342 in ^LISP``, 3343 REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [isSym_thm] \\ FULL_SIMP_TAC std_ss [] 3344 \\ SIMP_TAC std_ss [mc_print_sym_full_def,LET_DEF,EVAL ``(31 -- 0) 3w:word64``] 3345 \\ IMP_RES_TAC (SIMP_RULE std_ss [WORD_MUL_LSL,word_mul_n2w] mc_print_sym_thm) 3346 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3347 \\ ASM_SIMP_TAC std_ss [getSym_def] 3348 \\ Q.LIST_EXISTS_TAC [`3w`,`3w`,`3w`,`3w`] \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w] 3349 \\ MATCH_MP_TAC lisp_inv_nil_lemma \\ Q.LIST_EXISTS_TAC [`x3`,`w3`] 3350 \\ MATCH_MP_TAC lisp_inv_swap3 3351 \\ MATCH_MP_TAC lisp_inv_nil_lemma \\ Q.LIST_EXISTS_TAC [`x2`,`w2`] 3352 \\ MATCH_MP_TAC lisp_inv_swap2 3353 \\ MATCH_MP_TAC lisp_inv_nil_lemma \\ Q.LIST_EXISTS_TAC [`x1`,`w1`] 3354 \\ MATCH_MP_TAC lisp_inv_swap1 3355 \\ MATCH_MP_TAC lisp_inv_nil_lemma \\ Q.LIST_EXISTS_TAC [`Sym a`,`w0`] 3356 \\ ASM_SIMP_TAC std_ss []) 3357 |> SIMP_RULE std_ss [LET_DEF]; 3358 3359val _ = save_thm("mc_print_sym_full_thm",mc_print_sym_full_thm); 3360 3361 3362(* print " " *) 3363 3364val (mc_print_sp_spec,mc_print_sp_def) = basic_decompile_strings x64_tools "mc_print_sp" 3365 (SOME (``(ior:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``, 3366 ``(ior:word64,r0:word64,r1:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``)) 3367 (assemble "x64" ` 3368 mov r1,[r7-192] 3369 mov r0,[r7-216] 3370 mov BYTE [r0], 32 3371 mov BYTE [r0+1], 0 3372 insert io_write 3373 mov r0d,3 3374 mov r1d,1 `); 3375 3376val _ = save_thm("mc_print_sp_spec",mc_print_sp_spec); 3377 3378val mc_print_sp_thm = store_thm("mc_print_sp_thm", 3379 ``^LISP ==> 3380 ?g2. mc_print_sp_pre (EL 0 cs,sp,df,f,dg,g,io) /\ 3381 (mc_print_sp (EL 0 cs,sp,df,f,dg,g,io) = 3382 (EL 0 cs,tw0,tw1,sp,df,f,dg,g2,IO_WRITE io " ")) /\ 3383 let (g,io) = (g2,IO_WRITE io " ") in ^LISP``, 3384 SIMP_TAC std_ss [LET_DEF,mc_print_sp_def] \\ STRIP_TAC 3385 \\ IMP_RES_TAC lisp_inv_cs_read 3386 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 3387 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3388 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3389 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 3390 \\ IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPECL [`2`,`[32w;0w]`] lisp_inv_temp_string)) 3391 \\ FULL_SIMP_TAC std_ss [LENGTH] 3392 \\ Q.ABBREV_TAC `g3 = (sa2 + 0x1w =+ 0x0w) ((sa2 =+ 32w) g)` 3393 \\ IMP_RES_TAC LENGTH_EXPAND 3394 \\ `(one_byte_list sa2 [32w; 0x0w] * p) (fun2set (g3,dg)) /\ 3395 sa2 IN dg /\ sa2+1w IN dg` by 3396 (Q.UNABBREV_TAC `g3` 3397 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,SEP_CLAUSES,STAR_ASSOC] 3398 \\ SEP_R_TAC \\ SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 3399 \\ `null_term_str sa2 dg g3 " "` by 3400 (FULL_SIMP_TAC std_ss [null_term_str_def,one_string_def,MAP,APPEND, 3401 ORD_CHR_RWT,EVERY_DEF,CHR_11] \\ METIS_TAC []) 3402 \\ IMP_RES_TAC null_term_str_IMP 3403 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [lisp_inv_ignore_io]); 3404 3405 3406(* print "'" *) 3407 3408val (mc_print_qt_spec,mc_print_qt_def) = basic_decompile_strings x64_tools "mc_print_qt" 3409 (SOME (``(ior:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``, 3410 ``(ior:word64,r0:word64,r1:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``)) 3411 (assemble "x64" ` 3412 mov r1,[r7-192] 3413 mov r0,[r7-216] 3414 mov BYTE [r0], 39 3415 mov BYTE [r0+1], 0 3416 insert io_write 3417 mov r0d,3 3418 mov r1d,1 `); 3419 3420val _ = save_thm("mc_print_qt_spec",mc_print_qt_spec); 3421 3422val mc_print_qt_thm = store_thm("mc_print_qt_thm", 3423 ``^LISP ==> 3424 ?g2. mc_print_qt_pre (EL 0 cs,sp,df,f,dg,g,io) /\ 3425 (mc_print_qt (EL 0 cs,sp,df,f,dg,g,io) = 3426 (EL 0 cs,tw0,tw1,sp,df,f,dg,g2,IO_WRITE io "'")) /\ 3427 let (g,io) = (g2,IO_WRITE io "'") in ^LISP``, 3428 SIMP_TAC std_ss [LET_DEF,mc_print_qt_def] \\ STRIP_TAC 3429 \\ IMP_RES_TAC lisp_inv_cs_read 3430 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 3431 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3432 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3433 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 3434 \\ IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPECL [`2`,`[39w;0w]`] lisp_inv_temp_string)) 3435 \\ FULL_SIMP_TAC std_ss [LENGTH] 3436 \\ Q.ABBREV_TAC `g3 = (sa2 + 0x1w =+ 0x0w) ((sa2 =+ 39w) g)` 3437 \\ IMP_RES_TAC LENGTH_EXPAND 3438 \\ `(one_byte_list sa2 [39w; 0x0w] * p) (fun2set (g3,dg)) /\ 3439 sa2 IN dg /\ sa2+1w IN dg` by 3440 (Q.UNABBREV_TAC `g3` 3441 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,SEP_CLAUSES,STAR_ASSOC] 3442 \\ SEP_R_TAC \\ SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 3443 \\ `null_term_str sa2 dg g3 "'"` by 3444 (FULL_SIMP_TAC std_ss [null_term_str_def,one_string_def,MAP,APPEND, 3445 ORD_CHR_RWT,EVERY_DEF,CHR_11] \\ METIS_TAC []) 3446 \\ IMP_RES_TAC null_term_str_IMP 3447 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [lisp_inv_ignore_io]); 3448 3449 3450(* print "(" *) 3451 3452val (mc_print_open_spec,mc_print_open_def) = basic_decompile_strings x64_tools "mc_print_open" 3453 (SOME (``(ior:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``, 3454 ``(ior:word64,r0:word64,r1:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``)) 3455 (assemble "x64" ` 3456 mov r1,[r7-192] 3457 mov r0,[r7-216] 3458 mov BYTE [r0], 40 3459 mov BYTE [r0+1], 0 3460 insert io_write 3461 mov r0d,3 3462 mov r1d,1 `); 3463 3464val _ = save_thm("mc_print_open_spec",mc_print_open_spec); 3465 3466val mc_print_open_thm = store_thm("mc_print_open_thm", 3467 ``^LISP ==> 3468 ?g2. mc_print_open_pre (EL 0 cs,sp,df,f,dg,g,io) /\ 3469 (mc_print_open (EL 0 cs,sp,df,f,dg,g,io) = 3470 (EL 0 cs,tw0,tw1,sp,df,f,dg,g2,IO_WRITE io "(")) /\ 3471 let (g,io) = (g2,IO_WRITE io "(") in ^LISP``, 3472 SIMP_TAC std_ss [LET_DEF,mc_print_open_def] \\ STRIP_TAC 3473 \\ IMP_RES_TAC lisp_inv_cs_read 3474 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 3475 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3476 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3477 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 3478 \\ IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPECL [`2`,`[40w;0w]`] lisp_inv_temp_string)) 3479 \\ FULL_SIMP_TAC std_ss [LENGTH] 3480 \\ Q.ABBREV_TAC `g3 = (sa2 + 0x1w =+ 0x0w) ((sa2 =+ 40w) g)` 3481 \\ IMP_RES_TAC LENGTH_EXPAND 3482 \\ `(one_byte_list sa2 [40w; 0x0w] * p) (fun2set (g3,dg)) /\ 3483 sa2 IN dg /\ sa2+1w IN dg` by 3484 (Q.UNABBREV_TAC `g3` 3485 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,SEP_CLAUSES,STAR_ASSOC] 3486 \\ SEP_R_TAC \\ SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 3487 \\ `null_term_str sa2 dg g3 "("` by 3488 (FULL_SIMP_TAC std_ss [null_term_str_def,one_string_def,MAP,APPEND, 3489 ORD_CHR_RWT,EVERY_DEF,CHR_11] \\ METIS_TAC []) 3490 \\ IMP_RES_TAC null_term_str_IMP 3491 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [lisp_inv_ignore_io]); 3492 3493 3494(* print ")" *) 3495 3496val (mc_print_close_spec,mc_print_close_def) = basic_decompile_strings x64_tools "mc_print_close" 3497 (SOME (``(ior:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``, 3498 ``(ior:word64,r0:word64,r1:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``)) 3499 (assemble "x64" ` 3500 mov r1,[r7-192] 3501 mov r0,[r7-216] 3502 mov BYTE [r0], 41 3503 mov BYTE [r0+1], 0 3504 insert io_write 3505 mov r0d,3 3506 mov r1d,1 `); 3507 3508val _ = save_thm("mc_print_close_spec",mc_print_close_spec); 3509 3510val mc_print_close_thm = store_thm("mc_print_close_thm", 3511 ``^LISP ==> 3512 ?g2. mc_print_close_pre (EL 0 cs,sp,df,f,dg,g,io) /\ 3513 (mc_print_close (EL 0 cs,sp,df,f,dg,g,io) = 3514 (EL 0 cs,tw0,tw1,sp,df,f,dg,g2,IO_WRITE io ")")) /\ 3515 let (g,io) = (g2,IO_WRITE io ")") in ^LISP``, 3516 SIMP_TAC std_ss [LET_DEF,mc_print_close_def] \\ STRIP_TAC 3517 \\ IMP_RES_TAC lisp_inv_cs_read 3518 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 3519 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3520 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3521 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 3522 \\ IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPECL [`2`,`[41w;0w]`] lisp_inv_temp_string)) 3523 \\ FULL_SIMP_TAC std_ss [LENGTH] 3524 \\ Q.ABBREV_TAC `g3 = (sa2 + 0x1w =+ 0x0w) ((sa2 =+ 41w) g)` 3525 \\ IMP_RES_TAC LENGTH_EXPAND 3526 \\ `(one_byte_list sa2 [41w; 0x0w] * p) (fun2set (g3,dg)) /\ 3527 sa2 IN dg /\ sa2+1w IN dg` by 3528 (Q.UNABBREV_TAC `g3` 3529 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,SEP_CLAUSES,STAR_ASSOC] 3530 \\ SEP_R_TAC \\ SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 3531 \\ `null_term_str sa2 dg g3 ")"` by 3532 (FULL_SIMP_TAC std_ss [null_term_str_def,one_string_def,MAP,APPEND, 3533 ORD_CHR_RWT,EVERY_DEF,CHR_11] \\ METIS_TAC []) 3534 \\ IMP_RES_TAC null_term_str_IMP 3535 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [lisp_inv_ignore_io]); 3536 3537 3538(* print " . " *) 3539 3540val (mc_print_dot_spec,mc_print_dot_def) = basic_decompile_strings x64_tools "mc_print_dot" 3541 (SOME (``(ior:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``, 3542 ``(ior:word64,r0:word64,r1:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8,io:io_streams)``)) 3543 (assemble "x64" ` 3544 mov r1,[r7-192] 3545 mov r0,[r7-216] 3546 mov BYTE [r0], 32 3547 mov BYTE [r0+1], 46 3548 mov BYTE [r0+2], 32 3549 mov BYTE [r0+3], 0 3550 insert io_write 3551 mov r0d,3 3552 mov r1d,1 `); 3553 3554val _ = save_thm("mc_print_dot_spec",mc_print_dot_spec); 3555 3556val mc_print_dot_thm = store_thm("mc_print_dot_thm", 3557 ``^LISP ==> 3558 ?g2. mc_print_dot_pre (EL 0 cs,sp,df,f,dg,g,io) /\ 3559 (mc_print_dot (EL 0 cs,sp,df,f,dg,g,io) = 3560 (EL 0 cs,tw0,tw1,sp,df,f,dg,g2,IO_WRITE io " . ")) /\ 3561 let (g,io) = (g2,IO_WRITE io " . ") in ^LISP``, 3562 SIMP_TAC std_ss [LET_DEF,mc_print_dot_def] \\ STRIP_TAC 3563 \\ IMP_RES_TAC lisp_inv_cs_read 3564 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 3565 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3566 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3567 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 3568 \\ IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPECL [`4`,`[32w;46w;32w;0w]`] lisp_inv_temp_string)) 3569 \\ FULL_SIMP_TAC std_ss [LENGTH] 3570 \\ Q.ABBREV_TAC `g3 = (sa2+3w =+ 0x0w) ((sa2+2w =+ 32w) ((sa2+1w =+ 46w) ((sa2 =+ 32w) g)))` 3571 \\ IMP_RES_TAC LENGTH_EXPAND 3572 \\ `(one_byte_list sa2 [32w; 46w; 32w; 0x0w] * p) (fun2set (g3,dg)) /\ 3573 sa2 IN dg /\ sa2+1w IN dg /\ sa2+2w IN dg /\ sa2+3w IN dg` by 3574 (Q.UNABBREV_TAC `g3` 3575 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,SEP_CLAUSES,STAR_ASSOC] 3576 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 3577 \\ SEP_R_TAC \\ SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 3578 \\ `null_term_str sa2 dg g3 " . "` by 3579 (FULL_SIMP_TAC std_ss [null_term_str_def,one_string_def,MAP,APPEND, 3580 ORD_CHR_RWT,EVERY_DEF,CHR_11] \\ METIS_TAC []) 3581 \\ IMP_RES_TAC null_term_str_IMP 3582 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [lisp_inv_ignore_io]); 3583 3584 3585(* call stats function 1 *) 3586 3587val (mc_print_stats1_spec,mc_print_stats1_def) = basic_decompile_strings x64_tools "mc_print_stats1" 3588 (SOME (``(iod:word64,r0:word64,r6:word64,r7:word64,r8:word64,r14:word64,r15:word64,df:word64 set,f:word64->word32,io:io_streams)``, 3589 ``(iod:word64,r0:word64,r1:word64,r2:word64,r6:word64,r7:word64,r8:word64,r14:word64,r15:word64,df:word64 set,f:word64->word32,io:io_streams)``)) 3590 (assemble "x64" ` 3591 mov r1,[r7-176] 3592 xchg rdi,r0 3593 xchg rsi,r14 3594 mov rdx,r15 3595 shr rdx,1 3596 shr rsi,1 3597 mov edi, 1 3598 insert io_stats 3599 shl rsi,1 3600 xchg rsi,r14 3601 mov rdi,r0 3602 mov r1d,1 3603 mov r0d,3 `); 3604 3605val _ = save_thm("mc_print_stats1_spec",mc_print_stats1_spec); 3606 3607val mc_print_stats1_thm = store_thm("mc_print_stats1_thm", 3608 ``^LISP ==> 3609 ?g2. mc_print_stats1_pre (EL 2 cs,tw0,bp,sp,w2w w0,wi,we,df,f,io) /\ 3610 (mc_print_stats1 (EL 2 cs,tw0,bp,sp,w2w w0,wi,we,df,f,io) = 3611 (EL 2 cs,tw0,tw1,we >>> 1,bp,sp,w2w w0,wi,we,df,f,IO_STATS 1 io)) /\ 3612 let (io,tw2) = (IO_STATS 1 io,we >>> 1) in ^LISP``, 3613 SIMP_TAC std_ss [LET_DEF,mc_print_stats1_def] \\ STRIP_TAC 3614 \\ IMP_RES_TAC lisp_inv_cs_read 3615 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 3616 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3617 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3618 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] \\ REVERSE (REPEAT STRIP_TAC) 3619 THEN1 (METIS_TAC [lisp_inv_ignore_io,lisp_inv_ignore_tw2]) 3620 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] 3621 \\ FULL_SIMP_TAC std_ss [lisp_inv_def,GSYM word_mul_n2w] 3622 \\ Q.SPEC_TAC (`(n2w i):word64`,`w`) \\ blastLib.BBLAST_TAC); 3623 3624 3625(* call stats function 2 *) 3626 3627val (mc_print_stats2_spec,mc_print_stats2_def) = basic_decompile_strings x64_tools "mc_print_stats2" 3628 (SOME (``(iod:word64,r0:word64,r6:word64,r7:word64,r8:word64,r14:word64,r15:word64,df:word64 set,f:word64->word32,io:io_streams)``, 3629 ``(iod:word64,r0:word64,r1:word64,r2:word64,r6:word64,r7:word64,r8:word64,r14:word64,r15:word64,df:word64 set,f:word64->word32,io:io_streams)``)) 3630 (assemble "x64" ` 3631 mov r1,[r7-176] 3632 xchg rdi,r0 3633 xchg rsi,r14 3634 mov rdx,r15 3635 shr rdx,1 3636 shr rsi,1 3637 mov edi, 2 3638 insert io_stats 3639 shl rsi,1 3640 xchg rsi,r14 3641 mov rdi,r0 3642 mov r1d,1 3643 mov r0d,3 `); 3644 3645val _ = save_thm("mc_print_stats2_spec",mc_print_stats2_spec); 3646 3647val mc_print_stats2_thm = store_thm("mc_print_stats2_thm", 3648 ``^LISP ==> 3649 ?g2. mc_print_stats2_pre (EL 2 cs,tw0,bp,sp,w2w w0,wi,we,df,f,io) /\ 3650 (mc_print_stats2 (EL 2 cs,tw0,bp,sp,w2w w0,wi,we,df,f,io) = 3651 (EL 2 cs,tw0,tw1,we >>> 1,bp,sp,w2w w0,wi,we,df,f,IO_STATS 2 io)) /\ 3652 let (io,tw2) = (IO_STATS 2 io,we >>> 1) in ^LISP``, 3653 SIMP_TAC std_ss [LET_DEF,mc_print_stats2_def] \\ STRIP_TAC 3654 \\ IMP_RES_TAC lisp_inv_cs_read 3655 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 3656 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3657 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 3658 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] \\ REVERSE (REPEAT STRIP_TAC) 3659 THEN1 (METIS_TAC [lisp_inv_ignore_io,lisp_inv_ignore_tw2]) 3660 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] 3661 \\ FULL_SIMP_TAC std_ss [lisp_inv_def,GSYM word_mul_n2w] 3662 \\ Q.SPEC_TAC (`(n2w i):word64`,`w`) \\ blastLib.BBLAST_TAC); 3663 3664val _ = export_theory(); 3665