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