1 2open HolKernel boolLib bossLib Parse; 3open pred_setTheory arithmeticTheory pairTheory listTheory wordsTheory; 4open addressTheory set_sepTheory progTheory prog_x86Theory; 5open wordsLib x86_encodeLib helperLib; 6open combinTheory; 7 8open jit_inputTheory; 9open jit_opsTheory; 10open jit_codegenTheory; 11 12open compilerLib; 13open export_codeLib; 14 15infix \\ 16val op \\ = op THEN; 17 18 19val _ = new_theory "jit_incremental"; 20 21(* compiler setup begins *) 22 23(* make function "f" have exec permissions *) 24val _ = decompilerLib.add_executable_data_name "f" 25 26(* assign meanings to r1, r2, r3, r4 etc *) 27val _ = codegen_x86Lib.set_x86_regs 28 [(1,"eax"),(6,"ebx"),(5,"ecx"),(2,"edx"),(3,"edi"),(4,"esi"),(7,"ebp")] 29 30(* informal codegen spec: 31 32 r1 eax - preserved (top of stack) 33 r2 edx - preserved (return address) 34 r3 edi - preserved (rest of stack) 35 r4 esi - input: code pointer, output ignored 36 r5 ecx - input: bytecode code pointer, output: 0 37 r6 ebx - preserved (poniter to code generator) 38 r7 ebp - pointer to j map and temp memory 39 40*) 41 42(* compiler setup ends *) 43 44(* calls to code generator execute "xor ecx, index; call ebx" *) 45 46val (xor_lemma,call_lemma) = let 47 val (spec,_,s,_) = prog_x86Lib.x86_tools 48 val _ = prog_x86Lib.set_x86_code_write_perm_flag true 49 val ((th1,_,_),_) = spec "83F1" 50 val ((th2,_,_),_) = spec "FFD3" 51 val _ = prog_x86Lib.set_x86_code_write_perm_flag false 52 val th1 = HIDE_STATUS_RULE true s th1 53 val th2 = Q.INST [`df`|->`{esp-4w}`,`f`|->`\x.w`] th2 54 val th2 = SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND,ALIGNED_INTRO] th2 55 val th2 = SIMP_RULE bool_ss [IN_INSERT,xM_THM] th2 56 val th2 = SIMP_RULE std_ss [GSYM SPEC_MOVE_COND] th2 57 val th2 = HIDE_PRE_RULE ``xM (esp - 4w)`` th2 58 val th1 = Q.INST [`ecx`|->`0w`,`imm8`|->`n2w t`] th1 59 fun foo th = RW [] (DISCH_ALL (SIMP_RULE std_ss [ALIGNED,WORD_XOR_CLAUSES] th)) 60 in (foo th1, foo th2) end; 61 62(* invariant definition *) 63 64val ENCODES_JUMP_def = Define ` 65 ENCODES_JUMP a (p:num) j (bs:word8 list) = 66 (bs = [0x83w; 0xF1w; n2w p; 0xFFw; 0xD3w:word8]) \/ 67 ?w. (j p = SOME w) /\ (bs = [0xE9w] ++ X86_IMMEDIATE (w - a - 5w))`; 68 69val X86_ENCODE_def = Define ` 70 (X86_ENCODE (iSUB) a p j bs = (bs = [0x2Bw; 0x07w])) /\ 71 (X86_ENCODE (iSWAP) a p j bs = (bs = [0x87w; 0x07w])) /\ 72 (X86_ENCODE (iSTOP) a p j bs = (bs = [0xFFw; 0xE2w])) /\ 73 (X86_ENCODE (iPOP) a p j bs = (bs = [0x8Bw; 0x07w; 0x83w; 0xC7w; 0x04w])) /\ 74 (X86_ENCODE (iPUSH i) a p j bs = (bs = [0x83w; 0xEFw; 0x04w; 0x89w; 0x07w; 0xB8w; w2w i; 0x00w; 0x00w; 0x00w])) /\ 75 (X86_ENCODE (iJUMP i) a p j bs = ENCODES_JUMP a (w2n i) j bs) /\ 76 (X86_ENCODE (iJEQ i) a p j bs = ?bs0 bs1 bs2. (bs = bs0 ++ bs1 ++ bs2) /\ 77 (bs0 = [0x3Bw;0x07w;0x0Fw;0x84w;0x5w;0w;0w;0w]) /\ 78 ENCODES_JUMP (a + 8w) (p+1) j bs1 /\ ENCODES_JUMP (a + 13w) (w2n i) j bs2) /\ 79 (X86_ENCODE (iJLT i) a p j bs = ?bs0 bs1 bs2. (bs = bs0 ++ bs1 ++ bs2) /\ 80 (bs0 = [0x3Bw;0x07w;0x0Fw;0x82w;0x5w;0w;0w;0w]) /\ 81 ENCODES_JUMP (a + 8w) (p+1) j bs1 /\ ENCODES_JUMP (a + 13w) (w2n i) j bs2)`; 82 83val INSTR_LENGTH_def = Define ` 84 (INSTR_LENGTH (iSUB) = 2) /\ 85 (INSTR_LENGTH (iSWAP) = 2) /\ 86 (INSTR_LENGTH (iSTOP) = 2) /\ 87 (INSTR_LENGTH (iPOP) = 5) /\ 88 (INSTR_LENGTH (iPUSH i) = 10) /\ 89 (INSTR_LENGTH (iJUMP i) = 5) /\ 90 (INSTR_LENGTH (iJEQ i) = 18) /\ 91 (INSTR_LENGTH (iJLT i) = 18)`; 92 93val INSTR_LENGTH_THM = prove( 94 ``!i a p j bs. X86_ENCODE i a p j bs ==> (INSTR_LENGTH i = LENGTH bs)``, 95 Cases THEN SIMP_TAC std_ss [X86_ENCODE_def,LENGTH, 96 INSTR_LENGTH_def,ENCODES_JUMP_def,X86_IMMEDIATE_def,APPEND] 97 THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [LENGTH,APPEND]); 98 99val SEP_BYTES_IN_MEM_def = Define ` 100 (SEP_BYTES_IN_MEM a [] = emp) /\ 101 (SEP_BYTES_IN_MEM a (x::xs) = one (a,x) * SEP_BYTES_IN_MEM (a+1w) xs)`; 102 103val INSTR_IN_MEM_def = Define ` 104 (INSTR_IN_MEM NONE c p j = emp) /\ 105 (INSTR_IN_MEM (SOME a) c p j = 106 SEP_EXISTS bs. cond (X86_ENCODE c a p j bs) * 107 SEP_BYTES_IN_MEM a bs)`; 108 109val CODE_LOOP_def = Define ` 110 (CODE_LOOP i j [] = emp) /\ 111 (CODE_LOOP i j (c::cs) = INSTR_IN_MEM (j i) c i j * CODE_LOOP (i + 1) j cs)`; 112 113val SPACE_LENGTH_def = Define ` 114 (SPACE_LENGTH i j [] = 0) /\ 115 (SPACE_LENGTH i (j:num->word32 option) (c::cs) = 116 if ~(j i = NONE) then SPACE_LENGTH (i + 1) j cs else 117 INSTR_LENGTH c + SPACE_LENGTH (i + 1) j cs)`; 118 119val CODE_SPACE_def = Define ` 120 (CODE_SPACE a 0 = emp) /\ 121 (CODE_SPACE a (SUC n) = SEP_EXISTS x. one (a,x) * CODE_SPACE (a+1w) n)`; 122 123val CODE_INV_def = Define ` 124 CODE_INV a cs j = CODE_LOOP 0 j cs * CODE_SPACE a (SPACE_LENGTH 0 j cs)`; 125 126val MAP_ROW_def = Define ` 127 (MAP_ROW a NONE = one (a,0w) * one ((a:word32)+4w,0w:word32)) /\ 128 (MAP_ROW a (SOME w) = one (a,1w) * one (a+4w,w))`; 129 130val MAP_INV_def = Define ` 131 (MAP_INV a i j [] = emp) /\ 132 (MAP_INV a i j (c::cs) = MAP_ROW a (j i) * MAP_INV (a + 8w) (i + 1) j cs)`; 133 134val TEMP_INV_def = Define ` 135 (TEMP_INV a 0 = emp) /\ 136 (TEMP_INV a (SUC n) = SEP_EXISTS w. one (a - 4w:word32,w:word32) * TEMP_INV (a-4w) n)`; 137 138val TEMP_INV_UNROLL = prove( 139 ``0 < n ==> (TEMP_INV a n = 140 SEP_EXISTS w. one (a - 4w:word32,w:word32) * TEMP_INV (a-4w) (n - 1))``, 141 Cases_on `n` \\ SIMP_TAC std_ss [TEMP_INV_def] \\ SIMP_TAC std_ss [ADD1]); 142 143val MAP_TEMP_INV_def = Define ` 144 MAP_TEMP_INV a x y j cs = 145 TEMP_INV (a - 8w) 7 * one (a-8w, x) * one (a-4w, y) * MAP_INV a 0 j cs * SEP_T`; 146 147val IS_JUMP_def = Define ` 148 (IS_JUMP (iJUMP i) = T) /\ 149 (IS_JUMP (iJEQ i) = T) /\ 150 (IS_JUMP (iJLT i) = T) /\ 151 (IS_JUMP (iSTOP) = T) /\ 152 (IS_JUMP x = F)`; 153 154val ON_OFF_def = Define ` 155 ON_OFF cs j p = 156 !i. 157 (iFETCH p cs = SOME i) /\ ~(iFETCH (p+1) cs = NONE) /\ ~(IS_JUMP i) ==> 158 ((j p = NONE) = (j (p + 1) = NONE)) /\ 159 !w. (j p = SOME w) ==> (j (p + 1) = SOME (w + n2w (INSTR_LENGTH i)))`; 160 161val state_inv_def = Define ` 162 state_inv cs dh h dg (g:word32->word8) df f jw j = 163 ?a b b1. 164 (one_string_0 b (iENCODE cs) b1) (fun2set (g,dg)) /\ 165 (MAP_TEMP_INV jw a b j cs) (fun2set (h,dh)) /\ 166 (CODE_INV a cs j) (fun2set (f,df)) /\ ALIGNED jw /\ 167 (!p. ON_OFF cs j p) /\ LENGTH cs < 128 /\ 168 !i. LENGTH cs <= i ==> (j i = NONE)`; 169 170(* code generator *) 171 172(* informal codegen spec: 173 174 r1 eax - preserved (top of stack) 175 r2 edx - preserved (return address) 176 r3 edi - preserved (rest of stack) 177 r4 esi - input: generated code pointer, output: where to continue execution 178 r5 ecx - input: bytecode program counter, output: 0 179 r6 ebx - preserved (poniter to code generator) 180 r7 ebp - unchanged (pointer to j map and temp memory) 181 182 during execution: 183 184 r3 - pointer to next code to be generated 185 r4 - pointer to current j table entry 186 r6 - pointer to bytecode 187 188fun teach_compiler func_name s = let 189 val (th1,th2) = decompilerLib.decompile_x86 "_auto_" 190 [QUOTE (x86_encodeLib.x86_encode s ^ "/" ^ func_name)] 191 val th3 = SIMP_RULE (std_ss++SIZES_ss) [th2,LET_DEF,w2n_n2w] th1 192 val _ = codegenLib.add_compiled [th3]; 193 in th3 end; 194val _ = teach_compiler "m" "lea esi, [8 * ecx + ebp]" 195 196*) 197 198fun ord_eval tm = let 199 val tms = find_terml (can (match_term ``n2w (ORD c):'a word``)) tm 200 in (snd o dest_eq o concl o REWRITE_CONV (map EVAL tms)) tm end; 201 202val _ = Parse.hide "x86_access_j"; 203val (th1,x86_access_j_def,x86_access_j_pre_def) = compile "x86" `` 204 x86_access_j (r5,r7:word32,dh:word32 set,h:word32->word32) = 205 let r2 = r5 << 3 in 206 let r2 = r2 + r7 in 207 let r1 = h (r2) in 208 let r2 = h (r2 + 4w) in 209 (r1,r2,r5,r7,dh,h)``; 210 211val _ = Parse.hide "x86_encodes_jump"; 212val (th1,x86_encodes_jump_def,x86_encodes_jump_pre_def) = compile "x86" `` 213 x86_encodes_jump (r3:word32,r6:word32,df:word32 set,f:word32->word8) = 214 let f = (r3 =+ 0x83w) f in 215 let f = (r3 + 1w =+ 0xF1w) f in 216 let f = (r3 + 2w =+ w2w r6) f in 217 let f = (r3 + 3w =+ 0xFFw) f in 218 let f = (r3 + 4w =+ 0xD3w) f in 219 let r3 = r3 + 5w in 220 (r3,r6,df,f)``; 221 222val _ = Parse.hide "x86_write_jcc"; 223val (th1,x86_write_jcc_def,x86_write_jcc_pre_def) = (compile "x86" o ord_eval) `` 224 x86_write_jcc (r1:word32,r3,r6,df,f) = 225 if r1 = n2w (ORD #"j") then (r1,r3,r6,df,f) else 226 let f = (r3 =+ 0x3Bw) f in 227 let f = (r3 + 1w =+ 0x07w) f in 228 let f = (r3 + 2w =+ 0x0Fw) f in 229 let f = (r3 + 3w =+ 0x84w) f in 230 let f = (r3 + 4w =+ 0x05w) f in 231 let f = (r3 + 5w =+ 0x00w) f in 232 let f = (r3 + 6w =+ 0x00w) f in 233 let f = (r3 + 7w =+ 0x00w) f in 234 let r3 = r3 + 8w in 235 let (r3,r6,df,f) = x86_encodes_jump (r3,r6,df,f) in 236 if r1 = n2w (ORD #"=") then (r1,r3,r6,df,f) else 237 let f = (r3 - 10w =+ 0x82w) f in (r1,r3,r6,df,f)``; 238 239val _ = Parse.hide "x86_writecode"; 240val (th1,x86_writecode_def,x86_writecode_pre_def) = (compile "x86" o ord_eval) `` 241 x86_writecode (r3:word32,r4:word32,r5:word32,r6:word32,df:word32 set,f:word32->word8,dg:word32 set,g:word32->word8,dh:word32 set,h:word32->word32) = 242 (* r6 = pointer to bytecode encoding *) 243 (* r5 = index of bytecode instruction *) 244 (* r4 = pointer to row in map j *) 245 (* r3 = pointer to place where new code is written *) 246 let r1 = (w2w (g r6)):word32 in 247 let r5 = r5 + 1w in 248 if r1 = 0w then (r3,df,f,dg,g,dh,h) else 249 let h = (r4 =+ 1w) h in 250 let h = (r4 + 4w =+ r3) h in 251 let r4 = r4 + 8w in 252 let r6 = r6 + 1w in 253 if r1 = n2w (ORD #"-") then 254 let f = (r3 =+ 0x2Bw) f in 255 let f = (r3 + 1w =+ 0x07w) f in 256 let r3 = r3 + 2w in 257 x86_writecode (r3,r4,r5,r6,df,f,dg,g,dh,h) 258 else if r1 = n2w (ORD #"s") then 259 let f = (r3 =+ 0x87w) f in 260 let f = (r3 + 1w =+ 0x07w) f in 261 let r3 = r3 + 2w in 262 x86_writecode (r3,r4,r5,r6,df,f,dg,g,dh,h) 263 else if r1 = n2w (ORD #"p") then 264 let f = (r3 =+ 0x8Bw) f in 265 let f = (r3 + 1w =+ 0x07w) f in 266 let f = (r3 + 2w =+ 0x83w) f in 267 let f = (r3 + 3w =+ 0xC7w) f in 268 let f = (r3 + 4w =+ 0x04w) f in 269 let r3 = r3 + 5w in 270 x86_writecode (r3,r4,r5,r6,df,f,dg,g,dh,h) 271 else if r1 = n2w (ORD #".") then 272 let f = (r3 =+ 0xFFw) f in 273 let f = (r3 + 1w =+ 0xE2w) f in 274 let r3 = r3 + 2w in 275 (r3,df,f,dg,g,dh,h) 276 else if r1 = n2w (ORD #"c") then 277 let r2 = (w2w (g r6)):word32 in 278 let r1 = r2 - 48w in 279 let r6 = r6 + 1w in 280 let r2 = r2 + 1w in 281 let f = (r3 =+ 0x83w) f in 282 let f = (r3 + 1w =+ 0xEFw) f in 283 let f = (r3 + 2w =+ 0x04w) f in 284 let f = (r3 + 3w =+ 0x89w) f in 285 let f = (r3 + 4w =+ 0x07w) f in 286 let f = (r3 + 5w =+ 0xB8w) f in 287 let f = (r3 + 6w =+ w2w r1) f in 288 let f = (r3 + 7w =+ 0w) f in 289 let f = (r3 + 8w =+ 0w) f in 290 let f = (r3 + 9w =+ 0w) f in 291 let r3 = r3 + 10w in 292 x86_writecode (r3,r4,r5,r6,df,f,dg,g,dh,h) 293 else 294 let r2 = (w2w (g r6)):word32 in 295 let r6 = r5 in 296 let (r1,r3,r6,df,f) = x86_write_jcc (r1,r3,r6,df,f) in 297 let r6 = r2 - 48w in 298 let (r3,r6,df,f) = x86_encodes_jump (r3,r6,df,f) in 299 (r3,df,f,dg,g,dh,h)``; 300 301val _ = Parse.hide "x86_findbyte"; 302val (th1,x86_findbyte_def,x86_findbyte_pre_def) = (compile "x86" o ord_eval) `` 303 x86_findbyte (r1:word32,r2:word32,r5:word32,r6:word32,dg:word32 set,g:word32->word8) = 304 if r5 = 0w then (r1,r2,r6,dg,g) else 305 let r5 = r5 - 1w in 306 if g r2 = n2w (ORD #"-") then let r2 = r2 + 1w in x86_findbyte (r1,r2,r5,r6,dg,g) else 307 if g r2 = n2w (ORD #"s") then let r2 = r2 + 1w in x86_findbyte (r1,r2,r5,r6,dg,g) else 308 if g r2 = n2w (ORD #"p") then let r2 = r2 + 1w in x86_findbyte (r1,r2,r5,r6,dg,g) else 309 if g r2 = n2w (ORD #"c") then let r2 = r2 + 2w in x86_findbyte (r1,r2,r5,r6,dg,g) else 310 if g r2 = n2w (ORD #".") then 311 let r2 = r2 + 1w in let r6 = r2 in let r1 = r5 in 312 x86_findbyte (r1,r2,r5,r6,dg,g) else 313 if g r2 = n2w (ORD #"j") then 314 let r2 = r2 + 1w in let r2 = r2 + 1w in 315 let r6 = r2 in let r1 = r5 in 316 x86_findbyte (r1,r2,r5,r6,dg,g) else 317 if g r2 = n2w (ORD #"=") then 318 let r2 = r2 + 1w in let r2 = r2 + 1w in 319 let r6 = r2 in let r1 = r5 in 320 x86_findbyte (r1,r2,r5,r6,dg,g) else 321 if g r2 = n2w (ORD #"<") then 322 let r2 = r2 + 1w in let r2 = r2 + 1w in 323 let r6 = r2 in let r1 = r5 in 324 x86_findbyte (r1,r2,r5,r6,dg,g) else 325 (r1,r2,r6,dg,g)``; 326 327val _ = Parse.hide "x86_newcode"; 328val (th1,x86_newcode_def,x86_newcode_pre_def) = compile "x86" `` 329 x86_newcode (r1:word32,r5:word32,r7:word32,df:word32 set,f:word32->word8,dg:word32 set,g:word32->word8,dh:word32 set,h:word32->word32) = 330 if ~(r1 = 0w) then (r7,df,f,dg,g,dh,h) else 331 (* find location r5 in bytecode, pointed to by r6 *) 332 let r6 = h (r7 - 4w) in (* pointer to start of bytecode *) 333 let r1 = r5 in 334 let r2 = r6 in 335 let (r1,r2,r6,dg,g) = x86_findbyte (r1,r2,r5,r6,dg,g) in 336 (* here r6 points to right byte code *) 337 let r5 = h (r7 - 32w) in 338 let r5 = r5 - r1 in (* r5 holds index that corresponds to pointer r6 *) 339 (* write the new code *) 340 let r3 = h (r7 - 8w) in 341 let r1 = r5 << 3 in 342 let r4 = r7 + r1 in 343 let (r3,df,f,dg,g,dh,h) = x86_writecode (r3,r4,r5,r6,df,f,dg,g,dh,h) in 344 let h = ((r7 - 8w) =+ r3) h in 345 (r7,df,f,dg,g,dh,h)`` 346 347val _ = Parse.hide "x86_write_jump"; 348val (th1,x86_write_jump_def,x86_write_jump_pre_def) = compile "x86" `` 349 x86_write_jump (r2:word32,r4:word32,df:word32 set,f:word32->word8) = 350 let f = (r4 - 5w =+ 0xE9w) f in 351 let r2 = r2 - r4 in 352 let f = (r4 - 4w =+ w2w r2) f in 353 let r2 = r2 >>> 8 in 354 let f = (r4 - 3w =+ w2w r2) f in 355 let r2 = r2 >>> 8 in 356 let f = (r4 - 2w =+ w2w r2) f in 357 let r2 = r2 >>> 8 in 358 let f = (r4 - 1w =+ w2w r2) f in 359 (df,f)``; 360 361val _ = Parse.hide "x86_write_jump_cond"; 362val (th1,x86_write_jump_cond_def,x86_write_jump_cond_pre_def) = compile "x86" `` 363 x86_write_jump_cond (r1:word32,r2:word32,r4:word32,df:word32 set,f:word32->word8) = 364 if r1 = 0w then 365 let (df,f) = x86_write_jump (r2,r4,df,f) in (df,f) 366 else (df,f)`` 367 368val _ = Parse.hide "x86_inc"; 369val (x86_inc_th,x86_inc_def,x86_inc_pre_def) = compile "x86" `` 370 x86_inc (r1,r2,r3,r4,r5,r6,r7,dh,h,df,f,dg,g) = 371 let h = (r7 - 12w =+ r1) h in 372 let h = (r7 - 16w =+ r2) h in 373 let h = (r7 - 20w =+ r3) h in 374 let h = (r7 - 24w =+ r4) h in (* address from which we got here *) 375 let h = (r7 - 28w =+ r6) h in 376 let h = (r7 - 32w =+ r5) h in 377 (* read state map j *) 378 let (r1,r2,r5,r7,dh,h) = x86_access_j (r5,r7,dh,h) in 379 let (r7,df,f,dg,g,dh,h) = x86_newcode (r1,r5,r7,df,f,dg,g,dh,h) in 380 let r5 = h (r7 - 32w) in 381 let (r1,r2,r5,r7,dh,h) = x86_access_j (r5,r7,dh,h) in 382 let r4 = h (r7 - 24w) in 383 let r1 = h (r7 - 0x24w) in 384 let r6 = r2 in 385 let r4 = r4 + 5w in 386 let (df,f) = x86_write_jump_cond (r1,r2,r4,df,f) in (* only do this if not first time *) 387 let r5 = 0w:word32 in 388 let r1 = h (r7 - 12w) in 389 let r2 = h (r7 - 16w) in 390 let r3 = h (r7 - 20w) in 391 let r4 = r6 in 392 let r6 = h (r7 - 28w) in 393 let h = (r7 - 0x24w =+ r5) h in 394 (r1,r2,r3,r4,r5,r6,r7,dh,h,df,f,dg,g)`` 395 396(* idea: 397 398 look up j map entry 399 if j i = none then 400 make j i some 401 - find right instruction in bytecode 402 - repeatedly update map j, write instruction, 403 stop after first jump instruction 404 write jump to point to generated code 405 406*) 407 408val UNFOLD_MAP_INV = (SIMP_RULE std_ss [] o Q.SPEC `0` o prove)( 409 ``!k a cs i. 410 i < LENGTH cs ==> 411 ?q. MAP_INV a k j cs = MAP_ROW (a + n2w (8 * i)) (j (i + k)) * q``, 412 Induct_on `cs` \\ SIMP_TAC std_ss [LENGTH] \\ Cases_on `i` 413 \\ SIMP_TAC std_ss [MAP_INV_def,WORD_ADD_0] \\ REPEAT STRIP_TAC 414 THEN1 METIS_TAC [] \\ RES_TAC 415 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`k+1`,`a+8w`]) 416 \\ ASM_SIMP_TAC std_ss [] 417 \\ FULL_SIMP_TAC std_ss [MULT_CLAUSES,word_arith_lemma1,ADD1] 418 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 419 \\ Q.EXISTS_TAC `q * MAP_ROW a (j k)` \\ SIMP_TAC (std_ss++star_ss) []); 420 421val x86_access_j_thm = prove( 422 ``i < LENGTH cs /\ LENGTH cs <= 128 /\ ALIGNED r7 /\ 423 (r * MAP_INV r7 0 j cs) (fun2set (h,dh)) ==> 424 x86_access_j_pre (n2w i,r7,dh,h) /\ 425 (x86_access_j (n2w i,r7,dh,h) = 426 (if j i = NONE then 0w else 1w, 427 if j i = NONE then 0w else THE (j i),n2w i,r7,dh,h))``, 428 STRIP_TAC \\ SIMP_TAC std_ss [x86_access_j_def,x86_access_j_pre_def,LET_DEF] 429 \\ SIMP_TAC (std_ss++SIZES_ss) [word_add_n2w,AC ADD_ASSOC ADD_COMM,w2n_n2w] 430 \\ SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED,WORD_MUL_LSL] 431 \\ IMP_RES_TAC UNFOLD_MAP_INV 432 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`j`,`r7`]) 433 \\ Cases_on `j i` 434 \\ FULL_SIMP_TAC std_ss [MAP_ROW_def] 435 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 436 \\ ASM_SIMP_TAC bool_ss [DECIDE ``8 = 4 * 2``,GSYM word_mul_n2w, 437 ALIGNED_CLAUSES,GSYM WORD_MULT_ASSOC] 438 \\ SIMP_TAC std_ss [word_mul_n2w,MULT_ASSOC] 439 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC,AC MULT_ASSOC MULT_COMM] 440 \\ SEP_READ_TAC); 441 442val CODE_LOOP_UNROLL = (SIMP_RULE std_ss [] o Q.SPEC `0` o prove) ( 443 ``!i cs p instr j r. 444 (iFETCH p cs = SOME c) ==> 445 ?q. CODE_LOOP i j cs = INSTR_IN_MEM (j (p + i)) c (p + i) j * q``, 446 Induct_on `cs` \\ SIMP_TAC std_ss [iFETCH_def] \\ REPEAT STRIP_TAC \\ Cases_on `p` 447 THEN1 (FULL_SIMP_TAC std_ss [CODE_LOOP_def,INSTR_IN_MEM_def,SEP_CLAUSES] \\ METIS_TAC []) 448 \\ FULL_SIMP_TAC std_ss [ADD1,CODE_LOOP_def] 449 \\ Q.PAT_X_ASSUM `!i.bbb` (ASSUME_TAC o Q.SPECL [`i+1`,`n`,`j`]) 450 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [] 451 \\ Q.EXISTS_TAC `INSTR_IN_MEM (j i) h i j * q` 452 \\ SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM,AC ADD_COMM ADD_ASSOC]); 453 454val CODE_LOOP_IMP_BYTES_IN_MEM = prove( 455 ``(CODE_LOOP 0 j cs * r) (fun2set (f,df)) ==> 456 !p c w. 457 (iFETCH p cs = SOME c) /\ (j p = SOME w) ==> 458 ?bs. BYTES_IN_MEM w df f bs /\ X86_ENCODE c w p j bs``, 459 REPEAT STRIP_TAC 460 \\ IMP_RES_TAC CODE_LOOP_UNROLL 461 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `j`) 462 \\ FULL_SIMP_TAC std_ss [INSTR_IN_MEM_def,SEP_CLAUSES] 463 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS_THM,cond_STAR,GSYM STAR_ASSOC] 464 \\ Q.EXISTS_TAC `bs` \\ ASM_SIMP_TAC std_ss [] 465 \\ Q.PAT_X_ASSUM `(SEP_BYTES_IN_MEM w bs * (q * r)) (fun2set (f,df))` MP_TAC 466 \\ Q.SPEC_TAC (`w`,`a`) \\ Q.SPEC_TAC (`q * r`,`rr`) \\ REPEAT (POP_ASSUM (K ALL_TAC)) 467 \\ Induct_on `bs` \\ SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,BYTES_IN_MEM_def] 468 \\ REPEAT STRIP_TAC THEN1 SEP_READ_TAC THEN1 SEP_READ_TAC 469 \\ Q.PAT_X_ASSUM `!rr. bb` MATCH_MP_TAC \\ Q.EXISTS_TAC `one (a,h) * rr` 470 \\ FULL_SIMP_TAC (std_ss++star_ss) []); 471 472val cont_jump_def = Define ` 473 cont_jump j p cs a (t:word7) = 474 (iFETCH p cs = SOME (iJUMP t)) /\ (j p = SOME a) \/ 475 (iFETCH p cs = SOME (iJLT t)) /\ (j p = SOME (a - 13w)) \/ 476 (iFETCH p cs = SOME (iJEQ t)) /\ (j p = SOME (a - 13w)) \/ 477 (?r. (iFETCH p cs = SOME (iJLT r)) /\ (j p = SOME (a - 8w)) /\ (p + 1 = w2n t)) \/ 478 (?r. (iFETCH p cs = SOME (iJEQ r)) /\ (j p = SOME (a - 8w)) /\ (p + 1 = w2n t))`; 479 480val x86_write_jump_thm = prove( 481 ``(CODE_LOOP 0 j cs * r) (fun2set (f,df)) /\ 482 cont_jump j p cs a t /\ (j (w2n t) = SOME w) ==> 483 ?f2. x86_write_jump_pre(w,a + 5w,df,f) /\ 484 (x86_write_jump(w,a + 5w,df,f) = (df,f2)) /\ 485 (CODE_LOOP 0 j cs * r) (fun2set (f2,df))``, 486 REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [cont_jump_def] 487 \\ IMP_RES_TAC CODE_LOOP_UNROLL 488 \\ POP_ASSUM (STRIP_ASSUME_TAC o SPEC_ALL) 489 \\ FULL_SIMP_TAC std_ss [INSTR_IN_MEM_def,SEP_CLAUSES] 490 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [SEP_EXISTS,cond_STAR] 491 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def] 492 THEN1 493 (`?x1 x2 x3 x4 x5. y = [x1;x2;x3;x4;x5]` by 494 FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,ENCODES_JUMP_def,CONS_11] 495 \\ FULL_SIMP_TAC std_ss [] 496 \\ FULL_SIMP_TAC std_ss [x86_write_jump_def,x86_write_jump_pre_def,LET_DEF] 497 \\ FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,SEP_BYTES_IN_MEM_def] 498 \\ FULL_SIMP_TAC std_ss [CONJ_ASSOC,word_arith_lemma4, 499 WORD_ADD_0,word_arith_lemma1,SEP_CLAUSES] 500 \\ STRIP_TAC THEN1 SEP_READ_TAC 501 \\ SIMP_TAC std_ss [WORD_SUB_PLUS] 502 \\ Q.EXISTS_TAC `[0xE9w] ++ X86_IMMEDIATE (w - a - 5w)` 503 \\ SIMP_TAC std_ss [X86_IMMEDIATE_def,LSR_ADD,APPEND,SEP_BYTES_IN_MEM_def] 504 \\ SIMP_TAC std_ss [word_arith_lemma1,ENCODES_JUMP_def,CONS_11] 505 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,X86_IMMEDIATE_def,APPEND] 506 \\ SIMP_TAC std_ss [SEP_CLAUSES] \\ SEP_WRITE_TAC) 507 THEN1 508 (`?x1 x2 x3 x4 x5. bs2 = [x1;x2;x3;x4;x5]` by 509 FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,ENCODES_JUMP_def,CONS_11] 510 \\ `?y1 y2 y3 y4 y5. bs1 = [y1;y2;y3;y4;y5]` by 511 FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,ENCODES_JUMP_def,CONS_11] 512 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,WORD_ADD_0] 513 \\ FULL_SIMP_TAC std_ss [x86_write_jump_def,x86_write_jump_pre_def,LET_DEF] 514 \\ Q.PAT_X_ASSUM `y = bbb` ASSUME_TAC 515 \\ FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,SEP_BYTES_IN_MEM_def] 516 \\ FULL_SIMP_TAC std_ss [CONJ_ASSOC,word_arith_lemma4, 517 WORD_ADD_0,word_arith_lemma1,SEP_CLAUSES,word_arith_lemma3] 518 \\ STRIP_TAC THEN1 SEP_READ_TAC 519 \\ SIMP_TAC std_ss [WORD_SUB_PLUS] 520 \\ Q.EXISTS_TAC `[0x3Bw; 0x7w; 0xFw; 0x82w; 0x5w; 0x0w; 0x0w; 0x0w; y1; y2; y3; y4; 521 y5; 0xE9w] ++ X86_IMMEDIATE (w - a - 5w)` 522 \\ REVERSE STRIP_TAC THEN1 523 (SIMP_TAC std_ss [X86_IMMEDIATE_def,LSR_ADD,APPEND,SEP_BYTES_IN_MEM_def] 524 \\ SIMP_TAC std_ss [word_arith_lemma1,ENCODES_JUMP_def,CONS_11] 525 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,X86_IMMEDIATE_def,APPEND] 526 \\ SIMP_TAC std_ss [SEP_CLAUSES,word_arith_lemma3,WORD_ADD_0] 527 \\ SEP_WRITE_TAC) 528 \\ Q.EXISTS_TAC `bs1` \\ Q.EXISTS_TAC `[0xE9w] ++ X86_IMMEDIATE (w - a - 5w)` 529 \\ ASM_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,CONS_11] 530 \\ ASM_SIMP_TAC std_ss [ENCODES_JUMP_def,X86_IMMEDIATE_def,APPEND]) 531 THEN1 532 (`?x1 x2 x3 x4 x5. bs2 = [x1;x2;x3;x4;x5]` by 533 FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,ENCODES_JUMP_def,CONS_11] 534 \\ `?y1 y2 y3 y4 y5. bs1 = [y1;y2;y3;y4;y5]` by 535 FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,ENCODES_JUMP_def,CONS_11] 536 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,WORD_ADD_0] 537 \\ FULL_SIMP_TAC std_ss [x86_write_jump_def,x86_write_jump_pre_def,LET_DEF] 538 \\ Q.PAT_X_ASSUM `y = bbb` ASSUME_TAC 539 \\ FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,SEP_BYTES_IN_MEM_def] 540 \\ FULL_SIMP_TAC std_ss [CONJ_ASSOC,word_arith_lemma4, 541 WORD_ADD_0,word_arith_lemma1,SEP_CLAUSES,word_arith_lemma3] 542 \\ STRIP_TAC THEN1 SEP_READ_TAC 543 \\ SIMP_TAC std_ss [WORD_SUB_PLUS] 544 \\ Q.EXISTS_TAC `[0x3Bw; 0x7w; 0xFw; 0x84w; 0x5w; 0x0w; 0x0w; 0x0w; y1; y2; y3; y4; 545 y5; 0xE9w] ++ X86_IMMEDIATE (w - a - 5w)` 546 \\ REVERSE STRIP_TAC THEN1 547 (SIMP_TAC std_ss [X86_IMMEDIATE_def,LSR_ADD,APPEND,SEP_BYTES_IN_MEM_def] 548 \\ SIMP_TAC std_ss [word_arith_lemma1,ENCODES_JUMP_def,CONS_11] 549 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,X86_IMMEDIATE_def,APPEND] 550 \\ SIMP_TAC std_ss [SEP_CLAUSES,word_arith_lemma3,WORD_ADD_0] 551 \\ SEP_WRITE_TAC) 552 \\ Q.EXISTS_TAC `bs1` \\ Q.EXISTS_TAC `[0xE9w] ++ X86_IMMEDIATE (w - a - 5w)` 553 \\ ASM_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,CONS_11] 554 \\ ASM_SIMP_TAC std_ss [ENCODES_JUMP_def,X86_IMMEDIATE_def,APPEND]) 555 THEN1 556 (`?x1 x2 x3 x4 x5. bs2 = [x1;x2;x3;x4;x5]` by 557 FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,ENCODES_JUMP_def,CONS_11] 558 \\ `?y1 y2 y3 y4 y5. bs1 = [y1;y2;y3;y4;y5]` by 559 FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,ENCODES_JUMP_def,CONS_11] 560 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,WORD_ADD_0] 561 \\ FULL_SIMP_TAC std_ss [x86_write_jump_def,x86_write_jump_pre_def,LET_DEF] 562 \\ Q.PAT_X_ASSUM `y = bbb` ASSUME_TAC 563 \\ FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,SEP_BYTES_IN_MEM_def] 564 \\ FULL_SIMP_TAC std_ss [CONJ_ASSOC,word_arith_lemma4, 565 WORD_ADD_0,word_arith_lemma1,SEP_CLAUSES,word_arith_lemma3] 566 \\ STRIP_TAC THEN1 SEP_READ_TAC 567 \\ SIMP_TAC std_ss [WORD_SUB_PLUS] 568 \\ Q.EXISTS_TAC `[0x3Bw; 0x7w; 0xFw; 0x82w; 0x5w; 0x0w; 0x0w; 0x0w] ++ 569 [0xE9w] ++ X86_IMMEDIATE (w - a - 5w) ++ [x1;x2;x3;x4;x5]` 570 \\ REVERSE STRIP_TAC THEN1 571 (SIMP_TAC std_ss [X86_IMMEDIATE_def,LSR_ADD,APPEND,SEP_BYTES_IN_MEM_def] 572 \\ SIMP_TAC std_ss [word_arith_lemma1,ENCODES_JUMP_def,CONS_11] 573 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,X86_IMMEDIATE_def,APPEND] 574 \\ SIMP_TAC std_ss [SEP_CLAUSES,word_arith_lemma3,WORD_ADD_0] 575 \\ SEP_WRITE_TAC) 576 \\ Q.EXISTS_TAC `[0xE9w] ++ X86_IMMEDIATE (w - a - 5w)` \\ Q.EXISTS_TAC `bs2` 577 \\ ASM_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,CONS_11] 578 \\ ASM_SIMP_TAC std_ss [ENCODES_JUMP_def,X86_IMMEDIATE_def,APPEND]) 579 THEN1 580 (`?x1 x2 x3 x4 x5. bs2 = [x1;x2;x3;x4;x5]` by 581 FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,ENCODES_JUMP_def,CONS_11] 582 \\ `?y1 y2 y3 y4 y5. bs1 = [y1;y2;y3;y4;y5]` by 583 FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,ENCODES_JUMP_def,CONS_11] 584 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,WORD_ADD_0] 585 \\ FULL_SIMP_TAC std_ss [x86_write_jump_def,x86_write_jump_pre_def,LET_DEF] 586 \\ Q.PAT_X_ASSUM `y = bbb` ASSUME_TAC 587 \\ FULL_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,SEP_BYTES_IN_MEM_def] 588 \\ FULL_SIMP_TAC std_ss [CONJ_ASSOC,word_arith_lemma4, 589 WORD_ADD_0,word_arith_lemma1,SEP_CLAUSES,word_arith_lemma3] 590 \\ STRIP_TAC THEN1 SEP_READ_TAC 591 \\ SIMP_TAC std_ss [WORD_SUB_PLUS] 592 \\ Q.EXISTS_TAC `[0x3Bw; 0x7w; 0xFw; 0x84w; 0x5w; 0x0w; 0x0w; 0x0w] ++ 593 [0xE9w] ++ X86_IMMEDIATE (w - a - 5w) ++ [x1;x2;x3;x4;x5]` 594 \\ REVERSE STRIP_TAC THEN1 595 (SIMP_TAC std_ss [X86_IMMEDIATE_def,LSR_ADD,APPEND,SEP_BYTES_IN_MEM_def] 596 \\ SIMP_TAC std_ss [word_arith_lemma1,ENCODES_JUMP_def,CONS_11] 597 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,X86_IMMEDIATE_def,APPEND] 598 \\ SIMP_TAC std_ss [SEP_CLAUSES,word_arith_lemma3,WORD_ADD_0] 599 \\ SEP_WRITE_TAC) 600 \\ Q.EXISTS_TAC `[0xE9w] ++ X86_IMMEDIATE (w - a - 5w)` \\ Q.EXISTS_TAC `bs2` 601 \\ ASM_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND,CONS_11] 602 \\ ASM_SIMP_TAC std_ss [ENCODES_JUMP_def,X86_IMMEDIATE_def,APPEND])); 603 604val x86_write_jump_cond_thm = prove( 605 ``(CODE_LOOP 0 j cs * r) (fun2set (f,df)) /\ 606 ((v = 0w) ==> cont_jump j p cs a t) /\ (j (w2n t) = SOME w) ==> 607 ?f2. x86_write_jump_cond_pre(v,w,a + 5w,df,f) /\ 608 (x86_write_jump_cond(v,w,a + 5w,df,f) = (df,f2)) /\ 609 (CODE_LOOP 0 j cs * r) (fun2set (f2,df))``, 610 Cases_on `v = 0w` 611 \\ ASM_SIMP_TAC std_ss [x86_write_jump_cond_def,x86_write_jump_cond_pre_def] 612 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC x86_write_jump_thm 613 \\ ASM_SIMP_TAC std_ss [LET_DEF]); 614 615fun TRY_TAC t goal = t goal handle e => ALL_TAC goal; 616 617(* r6 remembers last poniter *) 618(* r1 remembers how many to drop for r6 *) 619 620val DROP_EQ_CONS = prove( 621 ``!cs n. n < LENGTH cs ==> (DROP n cs = EL n cs :: DROP (n + 1) cs)``, 622 Induct \\ SIMP_TAC std_ss [LENGTH,DROP_def] 623 \\ REPEAT STRIP_TAC \\ Cases_on `n` 624 THEN1 (Cases_on `cs` \\ SIMP_TAC std_ss [EL,HD,DROP_def]) 625 \\ FULL_SIMP_TAC std_ss [EL,TL] \\ FULL_SIMP_TAC std_ss [ADD1]); 626 627val iFETCH_IMP = prove( 628 ``!cs p c. p < LENGTH cs /\ (EL p cs = c) ==> (iFETCH p cs = SOME c)``, 629 Induct \\ SIMP_TAC std_ss [LENGTH,iFETCH_def] \\ NTAC 2 STRIP_TAC 630 \\ Cases_on `p` \\ FULL_SIMP_TAC std_ss [EL,HD,TL] \\ SIMP_TAC std_ss [ADD1]); 631 632val prev_jump_def = Define ` 633 (prev_jump cs 0 = 0) /\ 634 (prev_jump cs (SUC i) = if IS_JUMP (EL i cs) then i + 1 else prev_jump cs i)`; 635 636val x86_findbyte_thm = (SIMP_RULE std_ss [prev_jump_def,DROP_0] o Q.SPECL [`p`,`0`,`p`,`r2`,`r2`,`q`,`q`] o prove)( 637 ``!k i j r2 r6 r q. 638 i + k < LENGTH cs /\ LENGTH cs <= 128 /\ 639 (r * one_string_0 r2 (iENCODE (DROP i cs)) b1) (fun2set (g,dg)) /\ 640 (q * one_string_0 r6 (iENCODE (DROP (prev_jump cs i) cs)) b1) (fun2set (g,dg)) /\ 641 (prev_jump cs i = i + k - j) /\ j <= i + k ==> 642 ?r2i r6i ji qi. 643 x86_findbyte_pre (n2w j,r2,n2w k,r6,dg,g) /\ 644 (x86_findbyte (n2w j,r2,n2w k,r6,dg,g) = (n2w ji,r2i,r6i,dg,g)) /\ 645 (qi * one_string_0 r6i (iENCODE (DROP (prev_jump cs (i + k)) cs)) b1) (fun2set (g,dg)) /\ 646 (prev_jump cs (i + k) = i + k - ji) /\ ji <= i + k``, 647 Induct THEN1 648 (REPEAT STRIP_TAC 649 \\ ONCE_REWRITE_TAC [x86_findbyte_def,x86_findbyte_pre_def] 650 \\ SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `j` 651 \\ FULL_SIMP_TAC std_ss [DROP_def,DECIDE ``i <= 0 = (i = 0)``] \\ METIS_TAC []) 652 \\ REPEAT STRIP_TAC 653 \\ `SUC k < 4294967296` by DECIDE_TAC 654 \\ `~(n2w (SUC k) = 0w:word32)` by (ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] \\ DECIDE_TAC) 655 \\ ONCE_REWRITE_TAC [x86_findbyte_def,x86_findbyte_pre_def] 656 \\ ASM_SIMP_TAC std_ss [LET_DEF] 657 \\ SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_ADD_SUB] 658 \\ SIMP_TAC std_ss [word_arith_lemma1] 659 \\ `i < LENGTH cs` by DECIDE_TAC 660 \\ IMP_RES_TAC DROP_EQ_CONS 661 \\ POP_ASSUM (K ALL_TAC) 662 \\ Cases_on `EL i cs` 663 \\ FULL_SIMP_TAC std_ss [iENCODE_def,iENCODE1_def,one_string_0_STRCAT,iIMM_def] 664 \\ FULL_SIMP_TAC std_ss [one_string_def,MAP,LENGTH,one_list_def,word_arith_lemma1, 665 stringTheory.ORD_CHR_RWT,SEP_CLAUSES,STAR_ASSOC,iIMM_def,APPEND] 666 \\ TRY_TAC (`g r2 = 0x2Dw` by SEP_READ_TAC) 667 \\ TRY_TAC (`g r2 = 0x20w` by SEP_READ_TAC) 668 \\ TRY_TAC (`g r2 = 0x73w` by SEP_READ_TAC) 669 \\ TRY_TAC (`g r2 = 0x2Ew` by SEP_READ_TAC) 670 \\ TRY_TAC (`g r2 = 0x6Aw` by SEP_READ_TAC) 671 \\ TRY_TAC (`g r2 = 0x3Dw` by SEP_READ_TAC) 672 \\ TRY_TAC (`g r2 = 0x3Cw` by SEP_READ_TAC) 673 \\ TRY_TAC (`g r2 = 0x70w` by SEP_READ_TAC) 674 \\ TRY_TAC (`g r2 = 0x63w` by SEP_READ_TAC) 675 \\ TRY_TAC (`r2 IN dg` by SEP_READ_TAC) 676 \\ TRY_TAC (`(r2 + 1w) IN dg` by SEP_READ_TAC) 677 \\ ASM_SIMP_TAC std_ss [] 678 \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 679 \\ FULL_SIMP_TAC std_ss [DECIDE ``i + (k + 1) = (i + 1) + k``,ADD1] 680 \\ Q.PAT_X_ASSUM `!i.bbb` MATCH_MP_TAC 681 \\ ASM_SIMP_TAC std_ss [RW[ADD1]prev_jump_def,IS_JUMP_def] 682 \\ METIS_TAC []); 683 684val x86_encodes_jump_thm = prove( 685 ``(SEP_BYTES_IN_MEM a [x1;x2;x3;x4;x5] * r) (fun2set (f,df)) /\ i < 256 ==> 686 ?f2 bs. x86_encodes_jump_pre (a,n2w i,df,f) /\ 687 (x86_encodes_jump (a,n2w i,df,f) = (a+5w,n2w i,df,f2)) /\ 688 (SEP_BYTES_IN_MEM a bs * r) (fun2set (f2,df)) /\ 689 ENCODES_JUMP a i j bs``, 690 SIMP_TAC std_ss [x86_encodes_jump_def,x86_encodes_jump_pre_def] 691 \\ SIMP_TAC std_ss [LET_DEF,SEP_BYTES_IN_MEM_def,word_arith_lemma1] 692 \\ SIMP_TAC std_ss [SEP_CLAUSES] 693 \\ REPEAT STRIP_TAC 694 \\ Q.EXISTS_TAC `[0x83w; 0xF1w; n2w i; 0xFFw; 0xD3w]` 695 \\ SIMP_TAC std_ss [ENCODES_JUMP_def,SEP_BYTES_IN_MEM_def,word_arith_lemma1] 696 \\ SIMP_TAC std_ss [SEP_CLAUSES] 697 \\ `i < 4294967296` by DECIDE_TAC 698 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 699 \\ REVERSE (REPEAT STRIP_TAC) THEN1 SEP_WRITE_TAC 700 \\ SEP_READ_TAC); 701 702val LENGTH_LE_DROP = prove( 703 ``!xs n. LENGTH xs <= n ==> (DROP n xs = [])``, 704 Induct \\ SIMP_TAC std_ss [DROP_def] \\ Cases_on `n` 705 \\ ASM_SIMP_TAC std_ss [DROP_def,LENGTH,ADD1]); 706 707val SPACE_LENGTH_UPDATE = prove( 708 ``!cs i k. 709 i < k ==> (SPACE_LENGTH k ((i =+ w) j) cs = SPACE_LENGTH k j cs)``, 710 Induct \\ SIMP_TAC std_ss [SPACE_LENGTH_def,APPLY_UPDATE_THM, 711 DECIDE ``n < m ==> ~(n = m:num)``] 712 \\ REPEAT STRIP_TAC 713 \\ `i < k + 1` by DECIDE_TAC \\ RES_TAC \\ ASM_SIMP_TAC std_ss []); 714 715val SPACE_LENGTH_UNROLL = (SIMP_RULE std_ss [] o Q.SPEC `0` o prove) ( 716 ``!i cs p c j r w. 717 (iFETCH p cs = SOME c) /\ (j (p + i) = NONE) ==> 718 (SPACE_LENGTH i j cs = 719 INSTR_LENGTH c + SPACE_LENGTH i ((p + i =+ SOME w) j) cs)``, 720 Induct_on `cs` \\ SIMP_TAC std_ss [iFETCH_def] \\ REPEAT STRIP_TAC \\ Cases_on `p` 721 THEN1 (FULL_SIMP_TAC std_ss [SPACE_LENGTH_def,APPLY_UPDATE_THM] 722 \\ `i < i + 1` by DECIDE_TAC 723 \\ ASM_SIMP_TAC std_ss [SPACE_LENGTH_UPDATE]) 724 \\ FULL_SIMP_TAC std_ss [ADD1,SPACE_LENGTH_def,APPLY_UPDATE_THM] 725 \\ Q.PAT_X_ASSUM `!i.bbb` (ASSUME_TAC o Q.SPECL [`i+1`,`n`,`c`,`j`,`w`]) 726 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [] 727 \\ FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM,AC ADD_COMM ADD_ASSOC] 728 \\ RES_TAC \\ Cases_on `j i <> NONE` 729 \\ FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM,AC ADD_COMM ADD_ASSOC]); 730 731val ENCODE_JUMP_UPDATE = prove( 732 ``(j k = NONE) /\ ENCODES_JUMP x i j y ==> 733 ENCODES_JUMP x i ((k =+ SOME w) j) y``, 734 SIMP_TAC std_ss [ENCODES_JUMP_def,APPLY_UPDATE_THM] 735 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 736 \\ Cases_on `k = i` \\ FULL_SIMP_TAC std_ss []); 737 738val SEP_IMP_INSTR_IN_MEM_UPDATE = prove( 739 ``~(i = k) /\ (j k = NONE) ==> 740 SEP_IMP (INSTR_IN_MEM (j i) h i j) 741 (INSTR_IN_MEM (j i) h i ((k =+ SOME w) j))``, 742 Cases_on `j i` \\ ASM_SIMP_TAC std_ss [INSTR_IN_MEM_def,SEP_IMP_REFL] 743 \\ FULL_SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS,cond_STAR] 744 \\ REPEAT STRIP_TAC 745 \\ Q.EXISTS_TAC `y` \\ ASM_SIMP_TAC std_ss [] 746 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def] 747 THEN1 METIS_TAC [ENCODE_JUMP_UPDATE] 748 \\ Q.EXISTS_TAC `bs1` \\ Q.EXISTS_TAC `bs2` 749 \\ SIMP_TAC std_ss [] 750 \\ METIS_TAC [ENCODE_JUMP_UPDATE]); 751 752val SEP_IMP_CODE_LOOP_UPDATE = prove( 753 ``!cs i j k. 754 k < i /\ (j k = NONE) ==> 755 SEP_IMP (CODE_LOOP i j cs) 756 (CODE_LOOP i ((k =+ SOME w) j) cs)``, 757 Induct \\ SIMP_TAC std_ss [CODE_LOOP_def,SEP_IMP_REFL,APPLY_UPDATE_THM] 758 \\ REPEAT STRIP_TAC 759 \\ `~(i = k) /\ k < i + 1` by DECIDE_TAC 760 \\ ASM_SIMP_TAC std_ss [] 761 \\ MATCH_MP_TAC SEP_IMP_STAR 762 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [] 763 \\ METIS_TAC [SEP_IMP_INSTR_IN_MEM_UPDATE]); 764 765val CODE_LOOP_PULL = (SIMP_RULE std_ss [] o Q.SPEC `0` o prove) ( 766 ``!i cs p c j r w. 767 (iFETCH p cs = SOME c) /\ (j (p + i) = NONE) ==> 768 SEP_IMP (INSTR_IN_MEM (SOME w) c (p + i) ((p + i =+ SOME w) j) * CODE_LOOP i j cs) 769 (CODE_LOOP i ((p + i =+ SOME w) j) cs)``, 770 Induct_on `cs` \\ SIMP_TAC std_ss [iFETCH_def] \\ REPEAT STRIP_TAC \\ Cases_on `p` 771 THEN1 (FULL_SIMP_TAC std_ss [CODE_LOOP_def,APPLY_UPDATE_THM] 772 \\ MATCH_MP_TAC SEP_IMP_STAR 773 \\ SIMP_TAC std_ss [SEP_IMP_REFL] 774 \\ SIMP_TAC std_ss [INSTR_IN_MEM_def,SEP_CLAUSES] 775 \\ MATCH_MP_TAC SEP_IMP_CODE_LOOP_UPDATE 776 \\ ASM_SIMP_TAC std_ss []) 777 \\ FULL_SIMP_TAC std_ss [ADD1,CODE_LOOP_def,APPLY_UPDATE_THM] 778 \\ FULL_SIMP_TAC std_ss [GSYM ADD_ASSOC] 779 \\ SIMP_TAC std_ss [STAR_ASSOC] 780 \\ ONCE_REWRITE_TAC [STAR_COMM] 781 \\ SIMP_TAC std_ss [STAR_ASSOC] 782 \\ MATCH_MP_TAC SEP_IMP_STAR 783 \\ ONCE_REWRITE_TAC [STAR_COMM] 784 \\ REPEAT STRIP_TAC THEN1 785 (REWRITE_TAC [DECIDE ``1 + i = i + 1``] 786 \\ Q.PAT_X_ASSUM `!i.bbb` MATCH_MP_TAC 787 \\ ASM_SIMP_TAC std_ss [] 788 \\ FULL_SIMP_TAC std_ss [DECIDE ``1 + i = i + 1``]) 789 \\ MATCH_MP_TAC SEP_IMP_INSTR_IN_MEM_UPDATE 790 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 791 792val CODE_SPACE_ADD = prove( 793 ``!n m a. 794 CODE_SPACE a (n + m) = CODE_SPACE a n * CODE_SPACE (a + n2w n) m``, 795 Induct \\ ASM_SIMP_TAC std_ss [CODE_SPACE_def,SEP_CLAUSES,WORD_ADD_0,ADD] 796 \\ SIMP_TAC std_ss [STAR_ASSOC,ADD1,word_arith_lemma1] 797 \\ SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC]); 798 799val CODE_INV_UPDATE = prove( 800 ``!p cs c j f f2 df. 801 (iFETCH p cs = SOME c) /\ (j p = NONE) /\ 802 (!r. (CODE_SPACE w (INSTR_LENGTH c) * r) (fun2set (f,df)) ==> 803 (INSTR_IN_MEM (SOME w) c p ((p =+ SOME w) j) * r) (fun2set (f2,df))) /\ 804 (CODE_INV w cs j) (fun2set (f,df)) ==> 805 (CODE_INV (w + n2w (INSTR_LENGTH c)) cs ((p =+ SOME w) j)) (fun2set (f2,df))``, 806 REPEAT STRIP_TAC 807 \\ FULL_SIMP_TAC std_ss [CODE_INV_def] 808 \\ IMP_RES_TAC SPACE_LENGTH_UNROLL 809 \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `w`) 810 \\ FULL_SIMP_TAC std_ss [CODE_SPACE_ADD,STAR_ASSOC] 811 \\ Q.PAT_X_ASSUM `!r. bbb` (ASSUME_TAC o Q.SPEC `CODE_LOOP 0 j cs * 812 CODE_SPACE (w + n2w (INSTR_LENGTH c)) (SPACE_LENGTH 0 ((p =+ SOME w) j) cs)`) 813 \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ RES_TAC 814 \\ POP_ASSUM MP_TAC 815 \\ Q.SPEC_TAC (`fun2set(f2,df)`,`r`) 816 \\ REWRITE_TAC [GSYM SEP_IMP_def,STAR_ASSOC] 817 \\ MATCH_MP_TAC SEP_IMP_STAR 818 \\ SIMP_TAC std_ss [SEP_IMP_REFL] 819 \\ ONCE_REWRITE_TAC [STAR_COMM] 820 \\ MATCH_MP_TAC CODE_LOOP_PULL 821 \\ ASM_SIMP_TAC std_ss []); 822 823val CODE_SPACE_UNWIND = prove( 824 ``!n a. 0 < n ==> 825 (CODE_SPACE a n = SEP_EXISTS w. one (a,w) * CODE_SPACE (a+1w) (n-1))``, 826 Cases \\ SIMP_TAC std_ss [CODE_SPACE_def]); 827 828val MAP_INV_IGNORE = prove( 829 ``!cs n k a j. 830 n < k ==> (MAP_INV a k ((n =+ w) j) cs = MAP_INV a k j cs)``, 831 Induct \\ SIMP_TAC std_ss [MAP_INV_def,APPLY_UPDATE_THM] 832 \\ REPEAT STRIP_TAC \\ `~(n = k) /\ n < k + 1` by DECIDE_TAC 833 \\ ASM_SIMP_TAC std_ss []); 834 835val iFETCH_NOT_NONE = prove( 836 ``!cs n. n < LENGTH cs = ~(iFETCH n cs = NONE)``, 837 Induct \\ SIMP_TAC std_ss [LENGTH] 838 \\ Cases_on `n` \\ ASM_SIMP_TAC std_ss [LENGTH,iFETCH_def] 839 \\ ASM_SIMP_TAC std_ss [ADD1]); 840 841val ENCODES_JUMP_IMP = prove( 842 ``!a i j bs. ENCODES_JUMP a i j bs ==> ?z1 z2 z3 z4 z5. bs = [z1;z2;z3;z4;z5]``, 843 SIMP_TAC std_ss [ENCODES_JUMP_def] 844 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [CONS_11,X86_IMMEDIATE_def,APPEND]); 845 846val ENCODE_JUMP_LENGTH = prove( 847 ``ENCODES_JUMP a i j bs ==> (LENGTH bs = 5)``, 848 REPEAT STRIP_TAC \\ IMP_RES_TAC ENCODES_JUMP_IMP \\ ASM_SIMP_TAC std_ss [LENGTH]); 849 850val x86_writecode_thm = prove( 851 ``!n cs q j g f r3 r4 r6 pp h. 852 LENGTH cs < 128 /\ ALIGNED r4 /\ (!p. n <= p ==> ON_OFF cs j p) /\ 853 (n < LENGTH cs ==> (j n = NONE)) /\ 854 (q * one_string_0 r6 (iENCODE (DROP n cs)) b1) (fun2set (g,dg)) /\ 855 (CODE_INV r3 cs j) (fun2set (f,df)) /\ 856 (pp * MAP_INV r4 n j (DROP n cs)) (fun2set (h,dh)) ==> 857 ?f2 r3i j2 h2. 858 x86_writecode_pre (r3,r4,n2w n,r6,df,f,dg,g,dh,h) /\ 859 (x86_writecode (r3,r4,n2w n,r6,df,f,dg,g,dh,h) = 860 (r3i,df,f2,dg,g,dh,h2)) /\ 861 (CODE_INV r3i cs j2) (fun2set (f2,df)) /\ 862 (pp * MAP_INV r4 n j2 (DROP n cs)) (fun2set (h2,dh)) /\ 863 (!p. n <= p ==> ON_OFF cs j2 p) /\ 864 (n < LENGTH cs ==> (j2 n = SOME r3)) /\ 865 (!p. p < n ==> (j p = j2 p)) /\ 866 (!i. ~(j i = NONE) \/ LENGTH cs <= i ==> (j2 i = j i))``, 867 STRIP_TAC \\ STRIP_TAC \\ Induct_on `LENGTH cs - n` 868 \\ REPEAT STRIP_TAC THEN1 869 (`LENGTH cs <= n /\ ~(n < LENGTH cs)` by DECIDE_TAC 870 \\ FULL_SIMP_TAC std_ss [LENGTH_LE_DROP,iENCODE_def,one_string_0_def] 871 \\ FULL_SIMP_TAC std_ss [APPEND,one_string_def,MAP,one_list_def] 872 \\ FULL_SIMP_TAC std_ss [stringTheory.ORD_CHR_RWT] 873 \\ `r6 IN dg /\ (g r6 = 0w)` by SEP_READ_TAC 874 \\ ONCE_REWRITE_TAC [x86_writecode_def,x86_writecode_pre_def] 875 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,n2w_11] 876 \\ FULL_SIMP_TAC std_ss [MAP_INV_def] 877 \\ METIS_TAC []) 878 \\ `v = LENGTH cs - (n + 1)` by DECIDE_TAC 879 \\ FULL_SIMP_TAC std_ss [] 880 \\ Q.PAT_X_ASSUM `!cs n. bbb` (ASSUME_TAC o RW [] o Q.SPECL [`cs`,`n + 1`]) 881 \\ `n < LENGTH cs` by DECIDE_TAC 882 \\ IMP_RES_TAC DROP_EQ_CONS 883 \\ FULL_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 884 \\ Q.PAT_X_ASSUM `j n = NONE` ASSUME_TAC 885 \\ FULL_SIMP_TAC std_ss [MAP_INV_def,MAP_ROW_def,STAR_ASSOC] 886 \\ `(pp * MAP_ROW r4 ((n =+ SOME r3) j n) * 887 MAP_INV (r4 + 0x8w) (n + 1) j (DROP (n + 1) cs)) 888 (fun2set ((r4 + 0x4w =+ r3) ((r4 =+ 0x1w) h),dh))` by 889 (SIMP_TAC std_ss [APPLY_UPDATE_THM,MAP_ROW_def] \\ SEP_WRITE_TAC) 890 \\ `(!p. n + 1 <= p ==> ON_OFF cs ((n =+ SOME r3) j) p)` by 891 (FULL_SIMP_TAC std_ss [ON_OFF_def] \\ REPEAT STRIP_TAC 892 \\ `~(n = p) /\ ~(n = p + 1) /\ n <= p` by DECIDE_TAC 893 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM] \\ METIS_TAC []) 894 \\ Cases_on `EL n cs` 895 \\ FULL_SIMP_TAC std_ss [iENCODE_def,one_string_0_STRCAT,one_string_def,STAR_ASSOC,MAP_APPEND, 896 iENCODE1_def,LENGTH,SEP_CLAUSES,iIMM_def] 897 \\ FULL_SIMP_TAC std_ss [APPEND,one_list_def,MAP,stringTheory.ORD_CHR_RWT, 898 LENGTH,word_arith_lemma1,SEP_CLAUSES] 899 \\ TRY_TAC (`g r6 = 0x2Dw` by SEP_READ_TAC) 900 \\ TRY_TAC (`g r6 = 0x20w` by SEP_READ_TAC) 901 \\ TRY_TAC (`g r6 = 0x73w` by SEP_READ_TAC) 902 \\ TRY_TAC (`g r6 = 0x2Ew` by SEP_READ_TAC) 903 \\ TRY_TAC (`g r6 = 0x6Aw` by SEP_READ_TAC) 904 \\ TRY_TAC (`g r6 = 0x3Dw` by SEP_READ_TAC) 905 \\ TRY_TAC (`g r6 = 0x3Cw` by SEP_READ_TAC) 906 \\ TRY_TAC (`g r6 = 0x70w` by SEP_READ_TAC) 907 \\ TRY_TAC (`g r6 = 0x63w` by SEP_READ_TAC) 908 \\ `r6 IN dg` by SEP_READ_TAC 909 \\ TRY_TAC (`(r6 + 1w) IN dg` by SEP_READ_TAC) 910 \\ Q.ABBREV_TAC `hi = (r4 + 0x4w =+ r3) ((r4 =+ 0x1w) h)` 911 \\ IMP_RES_TAC iFETCH_IMP 912 THEN1 913 (ONCE_REWRITE_TAC [x86_writecode_def,x86_writecode_pre_def] 914 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,n2w_11] 915 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED] 916 \\ `~(IS_JUMP iSUB)` by EVAL_TAC 917 \\ `(n + 1 < LENGTH cs) ==> (((n =+ SOME r3) j) (n + 1) = NONE)` by 918 (SIMP_TAC std_ss [APPLY_UPDATE_THM,DECIDE ``~(n = n + 1)``] 919 \\ `ON_OFF cs j n` by METIS_TAC [LESS_EQ_REFL] 920 \\ POP_ASSUM MP_TAC 921 \\ SIMP_TAC std_ss [ON_OFF_def] \\ METIS_TAC [iFETCH_NOT_NONE]) 922 \\ Q.ABBREV_TAC `c = iSUB` 923 \\ Q.ABBREV_TAC `fi = (r3 + 0x1w =+ 0x7w) ((r3 =+ 0x2Bw) f)` 924 \\ `CODE_INV (r3 + n2w (INSTR_LENGTH c)) cs ((n =+ SOME r3) j) 925 (fun2set (fi,df))` by 926 (MATCH_MP_TAC CODE_INV_UPDATE 927 \\ Q.EXISTS_TAC `f` \\ Q.UNABBREV_TAC `c` \\ Q.UNABBREV_TAC `fi` 928 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def,INSTR_IN_MEM_def] 929 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES,CODE_SPACE_UNWIND] 930 \\ SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,X86_ENCODE_def,SEP_BYTES_IN_MEM_def] 931 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,CODE_SPACE_def] 932 \\ REPEAT STRIP_TAC \\ SEP_WRITE_TAC) 933 \\ Q.PAT_X_ASSUM `!q j g. bbb` (MP_TAC o 934 Q.SPECL [`q * one_string r6 (iENCODE1 c) (r6 + 1w)`,`(n =+ SOME r3) j`, 935 `g`,`fi`,`r3 + n2w (INSTR_LENGTH c)`,`r4 + 8w`, `r6+1w`, 936 `pp * MAP_ROW r4 (((n:num) =+ SOME r3) j n)`,`hi`]) 937 \\ ASM_SIMP_TAC std_ss [ALIGNED] 938 \\ Q.UNABBREV_TAC `c` 939 \\ SIMP_TAC std_ss [iENCODE1_def,INSTR_LENGTH_def,one_string_def, 940 MAP,one_list_def,SEP_CLAUSES,stringTheory.ORD_CHR_RWT] 941 \\ SIMP_TAC std_ss [MATCH_MP MAP_INV_IGNORE (DECIDE ``n < n+1``)] 942 \\ STRIP_TAC 943 \\ POP_ASSUM (ASSUME_TAC o UNDISCH o RW [GSYM AND_IMP_INTRO]) 944 \\ POP_ASSUM (STRIP_ASSUME_TAC o UNDISCH o RW [GSYM AND_IMP_INTRO]) 945 \\ ASM_SIMP_TAC std_ss [word_add_n2w] 946 \\ Q.EXISTS_TAC `j2` 947 \\ ASM_SIMP_TAC std_ss [] 948 \\ `j2 n = SOME r3` by METIS_TAC [DECIDE ``n < n+1``,APPLY_UPDATE_THM] 949 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM] 950 \\ IMP_RES_TAC CODE_LOOP_UNROLL 951 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 952 \\ FULL_SIMP_TAC std_ss [CODE_INV_def,INSTR_IN_MEM_def,APPLY_UPDATE_THM] 953 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,APPLY_UPDATE_THM] 954 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,GSYM STAR_ASSOC] 955 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def] 956 \\ Q.PAT_X_ASSUM `y = bbbb` ASSUME_TAC 957 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES] 958 \\ REVERSE (REPEAT STRIP_TAC) 959 THEN1 (`i <> n` by DECIDE_TAC \\ METIS_TAC []) 960 THEN1 (METIS_TAC []) 961 THEN1 (`p < n + 1 /\ ~(n = p)` by DECIDE_TAC \\ METIS_TAC []) 962 THEN1 963 (`(n + 1 <= p) \/ (n = p)` by DECIDE_TAC THEN1 (METIS_TAC []) 964 \\ FULL_SIMP_TAC std_ss [] 965 \\ SIMP_TAC std_ss [ON_OFF_def] 966 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def] 967 \\ REPEAT STRIP_TAC 968 \\ FULL_SIMP_TAC std_ss [GSYM iFETCH_NOT_NONE]) 969 \\ SEP_READ_TAC) 970 THEN1 971 (ONCE_REWRITE_TAC [x86_writecode_def,x86_writecode_pre_def] 972 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,n2w_11] 973 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED] 974 \\ `~(IS_JUMP iSWAP)` by EVAL_TAC 975 \\ `(n + 1 < LENGTH cs) ==> (((n =+ SOME r3) j) (n + 1) = NONE)` by 976 (SIMP_TAC std_ss [APPLY_UPDATE_THM,DECIDE ``~(n = n + 1)``] 977 \\ `ON_OFF cs j n` by METIS_TAC [LESS_EQ_REFL] 978 \\ POP_ASSUM MP_TAC 979 \\ SIMP_TAC std_ss [ON_OFF_def] \\ METIS_TAC [iFETCH_NOT_NONE]) 980 \\ Q.ABBREV_TAC `c = iSWAP` 981 \\ Q.ABBREV_TAC `fi = (r3 + 0x1w =+ 0x7w) ((r3 =+ 0x87w) f)` 982 \\ `CODE_INV (r3 + n2w (INSTR_LENGTH c)) cs ((n =+ SOME r3) j) 983 (fun2set (fi,df))` by 984 (MATCH_MP_TAC CODE_INV_UPDATE 985 \\ Q.EXISTS_TAC `f` \\ Q.UNABBREV_TAC `c` \\ Q.UNABBREV_TAC `fi` 986 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def,INSTR_IN_MEM_def] 987 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES,CODE_SPACE_UNWIND] 988 \\ SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,X86_ENCODE_def,SEP_BYTES_IN_MEM_def] 989 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,CODE_SPACE_def] 990 \\ REPEAT STRIP_TAC \\ SEP_WRITE_TAC) 991 \\ Q.PAT_X_ASSUM `!q j g. bbb` (MP_TAC o 992 Q.SPECL [`q * one_string r6 (iENCODE1 c) (r6 + 1w)`,`(n =+ SOME r3) j`, 993 `g`,`fi`,`r3 + n2w (INSTR_LENGTH c)`,`r4 + 8w`, `r6+1w`, 994 `pp * MAP_ROW r4 (((n:num) =+ SOME r3) j n)`,`hi`]) 995 \\ ASM_SIMP_TAC std_ss [ALIGNED] 996 \\ Q.UNABBREV_TAC `c` 997 \\ SIMP_TAC std_ss [iENCODE1_def,INSTR_LENGTH_def,one_string_def, 998 MAP,one_list_def,SEP_CLAUSES,stringTheory.ORD_CHR_RWT] 999 \\ SIMP_TAC std_ss [MATCH_MP MAP_INV_IGNORE (DECIDE ``n < n+1``)] 1000 \\ STRIP_TAC 1001 \\ POP_ASSUM (ASSUME_TAC o UNDISCH o RW [GSYM AND_IMP_INTRO]) 1002 \\ POP_ASSUM (STRIP_ASSUME_TAC o UNDISCH o RW [GSYM AND_IMP_INTRO]) 1003 \\ ASM_SIMP_TAC std_ss [word_add_n2w] 1004 \\ Q.EXISTS_TAC `j2` 1005 \\ ASM_SIMP_TAC std_ss [] 1006 \\ `j2 n = SOME r3` by METIS_TAC [DECIDE ``n < n+1``,APPLY_UPDATE_THM] 1007 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM] 1008 \\ IMP_RES_TAC CODE_LOOP_UNROLL 1009 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1010 \\ FULL_SIMP_TAC std_ss [CODE_INV_def,INSTR_IN_MEM_def,APPLY_UPDATE_THM] 1011 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,APPLY_UPDATE_THM] 1012 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,GSYM STAR_ASSOC] 1013 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def] 1014 \\ Q.PAT_X_ASSUM `y = bbbb` ASSUME_TAC 1015 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES] 1016 \\ REVERSE (REPEAT STRIP_TAC) 1017 THEN1 (`i <> n` by DECIDE_TAC \\ METIS_TAC []) 1018 THEN1 (METIS_TAC []) 1019 THEN1 (`p < n + 1 /\ ~(n = p)` by DECIDE_TAC \\ METIS_TAC []) 1020 THEN1 1021 (`(n + 1 <= p) \/ (n = p)` by DECIDE_TAC THEN1 (METIS_TAC []) 1022 \\ FULL_SIMP_TAC std_ss [] 1023 \\ SIMP_TAC std_ss [ON_OFF_def] 1024 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def] 1025 \\ REPEAT STRIP_TAC 1026 \\ FULL_SIMP_TAC std_ss [GSYM iFETCH_NOT_NONE]) 1027 \\ SEP_READ_TAC) 1028 THEN1 1029 (ONCE_REWRITE_TAC [x86_writecode_def,x86_writecode_pre_def] 1030 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,n2w_11] 1031 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED] 1032 \\ `(IS_JUMP iSTOP)` by EVAL_TAC 1033 \\ Q.ABBREV_TAC `c = iSTOP` 1034 \\ Q.ABBREV_TAC `fi = (r3 + 0x1w =+ 0xE2w) ((r3 =+ 0xFFw) f)` 1035 \\ `CODE_INV (r3 + n2w (INSTR_LENGTH c)) cs ((n =+ SOME r3) j) 1036 (fun2set (fi,df))` by 1037 (MATCH_MP_TAC CODE_INV_UPDATE 1038 \\ Q.EXISTS_TAC `f` \\ Q.UNABBREV_TAC `c` \\ Q.UNABBREV_TAC `fi` 1039 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def,INSTR_IN_MEM_def] 1040 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES,CODE_SPACE_UNWIND] 1041 \\ SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,X86_ENCODE_def,SEP_BYTES_IN_MEM_def] 1042 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,CODE_SPACE_def] 1043 \\ REPEAT STRIP_TAC \\ SEP_WRITE_TAC) 1044 \\ Q.EXISTS_TAC `(n =+ SOME r3) j` 1045 \\ Q.UNABBREV_TAC `c` 1046 \\ FULL_SIMP_TAC std_ss [INSTR_LENGTH_def,APPLY_UPDATE_THM] 1047 \\ FULL_SIMP_TAC std_ss [MAP_ROW_def,STAR_ASSOC] 1048 \\ FULL_SIMP_TAC std_ss [MATCH_MP MAP_INV_IGNORE (DECIDE ``n < n+1``)] 1049 \\ SIMP_TAC std_ss [DECIDE ``n < m ==> ~(n = m:num)``] 1050 \\ REVERSE (REPEAT STRIP_TAC) 1051 THEN1 (`i <> n` by DECIDE_TAC \\ METIS_TAC []) 1052 THEN1 (METIS_TAC []) 1053 THEN1 1054 (`(n + 1 <= p) \/ (n = p)` by DECIDE_TAC THEN1 (METIS_TAC []) 1055 \\ FULL_SIMP_TAC std_ss [] 1056 \\ SIMP_TAC std_ss [ON_OFF_def] 1057 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def]) 1058 \\ IMP_RES_TAC CODE_LOOP_UNROLL 1059 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1060 \\ FULL_SIMP_TAC std_ss [CODE_INV_def,INSTR_IN_MEM_def,APPLY_UPDATE_THM] 1061 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,APPLY_UPDATE_THM] 1062 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,GSYM STAR_ASSOC] 1063 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def] 1064 \\ Q.PAT_X_ASSUM `y = bbbb` ASSUME_TAC 1065 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES] 1066 \\ SEP_READ_TAC) 1067 THEN1 1068 (ONCE_REWRITE_TAC [x86_writecode_def,x86_writecode_pre_def] 1069 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,n2w_11] 1070 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED] 1071 \\ `~(IS_JUMP iPOP)` by EVAL_TAC 1072 \\ `(n + 1 < LENGTH cs) ==> (((n =+ SOME r3) j) (n + 1) = NONE)` by 1073 (SIMP_TAC std_ss [APPLY_UPDATE_THM,DECIDE ``~(n = n + 1)``] 1074 \\ `ON_OFF cs j n` by METIS_TAC [LESS_EQ_REFL] 1075 \\ POP_ASSUM MP_TAC 1076 \\ SIMP_TAC std_ss [ON_OFF_def] \\ METIS_TAC [iFETCH_NOT_NONE]) 1077 \\ Q.ABBREV_TAC `c = iPOP` 1078 \\ Q.ABBREV_TAC `fi = (r3 + 0x4w =+ 0x4w) 1079 ((r3 + 0x3w =+ 0xC7w) 1080 ((r3 + 0x2w =+ 0x83w) 1081 ((r3 + 0x1w =+ 0x7w) ((r3 =+ 0x8Bw) f))))` 1082 \\ `CODE_INV (r3 + n2w (INSTR_LENGTH c)) cs ((n =+ SOME r3) j) 1083 (fun2set (fi,df))` by 1084 (MATCH_MP_TAC CODE_INV_UPDATE 1085 \\ Q.EXISTS_TAC `f` \\ Q.UNABBREV_TAC `c` \\ Q.UNABBREV_TAC `fi` 1086 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def,INSTR_IN_MEM_def] 1087 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES,CODE_SPACE_UNWIND] 1088 \\ SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,X86_ENCODE_def,SEP_BYTES_IN_MEM_def] 1089 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,CODE_SPACE_def,word_arith_lemma1] 1090 \\ REPEAT STRIP_TAC \\ SEP_WRITE_TAC) 1091 \\ Q.PAT_X_ASSUM `!q j g. bbb` (MP_TAC o 1092 Q.SPECL [`q * one_string r6 (iENCODE1 c) (r6 + 1w)`,`(n =+ SOME r3) j`, 1093 `g`,`fi`,`r3 + n2w (INSTR_LENGTH c)`,`r4 + 8w`, `r6+1w`, 1094 `pp * MAP_ROW r4 (((n:num) =+ SOME r3) j n)`,`hi`]) 1095 \\ ASM_SIMP_TAC std_ss [ALIGNED] 1096 \\ Q.UNABBREV_TAC `c` 1097 \\ SIMP_TAC std_ss [iENCODE1_def,INSTR_LENGTH_def,one_string_def, 1098 MAP,one_list_def,SEP_CLAUSES,stringTheory.ORD_CHR_RWT] 1099 \\ SIMP_TAC std_ss [MATCH_MP MAP_INV_IGNORE (DECIDE ``n < n+1``)] 1100 \\ STRIP_TAC 1101 \\ POP_ASSUM (ASSUME_TAC o UNDISCH o RW [GSYM AND_IMP_INTRO]) 1102 \\ POP_ASSUM (STRIP_ASSUME_TAC o UNDISCH o RW [GSYM AND_IMP_INTRO]) 1103 \\ ASM_SIMP_TAC std_ss [word_add_n2w] 1104 \\ Q.EXISTS_TAC `j2` 1105 \\ ASM_SIMP_TAC std_ss [] 1106 \\ `j2 n = SOME r3` by METIS_TAC [DECIDE ``n < n+1``,APPLY_UPDATE_THM] 1107 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM] 1108 \\ IMP_RES_TAC CODE_LOOP_UNROLL 1109 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1110 \\ FULL_SIMP_TAC std_ss [CODE_INV_def,INSTR_IN_MEM_def,APPLY_UPDATE_THM] 1111 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,APPLY_UPDATE_THM] 1112 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,GSYM STAR_ASSOC] 1113 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def] 1114 \\ Q.PAT_X_ASSUM `y = bbbb` ASSUME_TAC 1115 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES] 1116 \\ REVERSE (REPEAT STRIP_TAC) 1117 THEN1 (`i <> n` by DECIDE_TAC \\ METIS_TAC []) 1118 THEN1 (METIS_TAC []) 1119 THEN1 (`p < n + 1 /\ ~(n = p)` by DECIDE_TAC \\ METIS_TAC []) 1120 THEN1 1121 (`(n + 1 <= p) \/ (n = p)` by DECIDE_TAC THEN1 (METIS_TAC []) 1122 \\ FULL_SIMP_TAC std_ss [] 1123 \\ SIMP_TAC std_ss [ON_OFF_def] 1124 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def] 1125 \\ REPEAT STRIP_TAC 1126 \\ FULL_SIMP_TAC std_ss [GSYM iFETCH_NOT_NONE]) 1127 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 1128 \\ SEP_READ_TAC) 1129 \\ `n2w (w2n ((n2w (ORD (CHR (48 + w2n c)))):word8)) - 0x30w = n2w (w2n c):word32` by 1130 (ASSUME_TAC (Q.SPEC `c` (INST_TYPE [``:'a``|->``:7``] w2n_lt)) 1131 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [] 1132 \\ `48 + w2n c < 256 /\ 48 + w2n c < 4294967296` by DECIDE_TAC 1133 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [stringTheory.ORD_CHR_RWT,w2n_n2w] 1134 \\ ONCE_REWRITE_TAC [ADD_COMM] 1135 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_SUB]) 1136 \\ `(w2n c) < 256` by 1137 (ASSUME_TAC (Q.SPEC `c` (INST_TYPE [``:'a``|->``:7``] w2n_lt)) 1138 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [] \\ DECIDE_TAC) 1139 THEN1 1140 (ONCE_REWRITE_TAC [x86_writecode_def,x86_writecode_pre_def] 1141 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,n2w_11] 1142 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED] 1143 \\ `~(IS_JUMP (iPUSH c))` by EVAL_TAC 1144 \\ `(n + 1 < LENGTH cs) ==> (((n =+ SOME r3) j) (n + 1) = NONE)` by 1145 (SIMP_TAC std_ss [APPLY_UPDATE_THM,DECIDE ``~(n = n + 1)``] 1146 \\ `ON_OFF cs j n` by METIS_TAC [LESS_EQ_REFL] 1147 \\ POP_ASSUM MP_TAC 1148 \\ SIMP_TAC std_ss [ON_OFF_def] \\ METIS_TAC [iFETCH_NOT_NONE]) 1149 \\ `g (r6 + 1w) = n2w (ORD (CHR (48 + w2n c)))` by SEP_READ_TAC 1150 \\ ASM_SIMP_TAC std_ss [] 1151 \\ `w2n c < 4294967296` by DECIDE_TAC 1152 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w] 1153 \\ Q.ABBREV_TAC `d = iPUSH c` 1154 \\ Q.ABBREV_TAC `fi = (r3 + 0x9w =+ 0x0w) 1155 ((r3 + 0x8w =+ 0x0w) 1156 ((r3 + 0x7w =+ 0x0w) 1157 ((r3 + 0x6w =+ n2w (w2n c)) 1158 ((r3 + 0x5w =+ 0xB8w) 1159 ((r3 + 0x4w =+ 0x7w) 1160 ((r3 + 0x3w =+ 0x89w) 1161 ((r3 + 0x2w =+ 0x4w) 1162 ((r3 + 0x1w =+ 0xEFw) 1163 ((r3 =+ 0x83w) f)))))))))` 1164 \\ `CODE_INV (r3 + n2w (INSTR_LENGTH d)) cs ((n =+ SOME r3) j) 1165 (fun2set (fi,df))` by 1166 (MATCH_MP_TAC CODE_INV_UPDATE 1167 \\ Q.EXISTS_TAC `f` \\ Q.UNABBREV_TAC `d` \\ Q.UNABBREV_TAC `fi` 1168 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def,INSTR_IN_MEM_def] 1169 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES,CODE_SPACE_UNWIND] 1170 \\ SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,X86_ENCODE_def,SEP_BYTES_IN_MEM_def] 1171 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,CODE_SPACE_def,word_arith_lemma1,w2w_def] 1172 \\ REPEAT STRIP_TAC \\ SEP_WRITE_TAC) 1173 \\ Q.PAT_X_ASSUM `!q j g. bbb` (MP_TAC o 1174 Q.SPECL [`q * one_string r6 (iENCODE1 d) (r6 + 2w)`,`(n =+ SOME r3) j`, 1175 `g`,`fi`,`r3 + n2w (INSTR_LENGTH d)`,`r4 + 8w`, `r6+2w`, 1176 `pp * MAP_ROW r4 (((n:num) =+ SOME r3) j n)`,`hi`]) 1177 \\ Q.UNABBREV_TAC `d` 1178 \\ ASM_SIMP_TAC std_ss [ALIGNED] 1179 \\ SIMP_TAC std_ss [iENCODE1_def,INSTR_LENGTH_def,one_string_def, 1180 MAP,one_list_def,SEP_CLAUSES,stringTheory.ORD_CHR_RWT, 1181 one_list_def,iIMM_def,MAP,APPEND,word_arith_lemma1] 1182 \\ SIMP_TAC std_ss [MATCH_MP MAP_INV_IGNORE (DECIDE ``n < n+1``)] 1183 \\ STRIP_TAC 1184 \\ POP_ASSUM (ASSUME_TAC o UNDISCH o RW [GSYM AND_IMP_INTRO]) 1185 \\ POP_ASSUM (STRIP_ASSUME_TAC o UNDISCH o RW [GSYM AND_IMP_INTRO]) 1186 \\ ASM_SIMP_TAC std_ss [word_add_n2w] 1187 \\ Q.EXISTS_TAC `j2` 1188 \\ ASM_SIMP_TAC std_ss [] 1189 \\ `j2 n = SOME r3` by METIS_TAC [DECIDE ``n < n+1``,APPLY_UPDATE_THM] 1190 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM] 1191 \\ IMP_RES_TAC CODE_LOOP_UNROLL 1192 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1193 \\ FULL_SIMP_TAC std_ss [CODE_INV_def,INSTR_IN_MEM_def,APPLY_UPDATE_THM] 1194 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,APPLY_UPDATE_THM] 1195 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,GSYM STAR_ASSOC] 1196 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def] 1197 \\ Q.PAT_X_ASSUM `y = bbbb` ASSUME_TAC 1198 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES] 1199 \\ REVERSE (REPEAT STRIP_TAC) 1200 THEN1 (`i <> n` by DECIDE_TAC \\ METIS_TAC []) 1201 THEN1 (METIS_TAC []) 1202 THEN1 (`p < n + 1 /\ ~(n = p)` by DECIDE_TAC \\ METIS_TAC []) 1203 THEN1 1204 (`(n + 1 <= p) \/ (n = p)` by DECIDE_TAC THEN1 (METIS_TAC []) 1205 \\ FULL_SIMP_TAC std_ss [] 1206 \\ SIMP_TAC std_ss [ON_OFF_def] 1207 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def] 1208 \\ REPEAT STRIP_TAC 1209 \\ FULL_SIMP_TAC std_ss [GSYM iFETCH_NOT_NONE]) 1210 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 1211 \\ SEP_READ_TAC) 1212 \\ Q.PAT_X_ASSUM `!q j g. bbb` (K ALL_TAC) 1213 THEN1 1214 (ONCE_REWRITE_TAC [x86_writecode_def,x86_writecode_pre_def] 1215 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,n2w_11] 1216 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED] 1217 \\ `(IS_JUMP (iJUMP c))` by EVAL_TAC 1218 \\ Q.ABBREV_TAC `d = iJUMP c` 1219 \\ SIMP_TAC std_ss [x86_write_jcc_def,x86_write_jcc_pre_def] 1220 \\ `g (r6 + 1w) = n2w (ORD (CHR (48 + w2n c)))` by SEP_READ_TAC 1221 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 1222 \\ ASM_SIMP_TAC std_ss [] 1223 \\ Q.ABBREV_TAC `fi = SND (SND (SND (x86_encodes_jump (r3,n2w (w2n c),df,f))))` 1224 \\ `CODE_INV (r3 + n2w (INSTR_LENGTH d)) cs ((n =+ SOME r3) j) 1225 (fun2set (fi,df))` by 1226 (MATCH_MP_TAC CODE_INV_UPDATE 1227 \\ Q.EXISTS_TAC `f` \\ Q.UNABBREV_TAC `d` \\ Q.UNABBREV_TAC `fi` 1228 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def,INSTR_IN_MEM_def] 1229 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES,CODE_SPACE_UNWIND] 1230 \\ SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,X86_ENCODE_def,SEP_BYTES_IN_MEM_def] 1231 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,CODE_SPACE_def] 1232 \\ SIMP_TAC std_ss [word_arith_lemma1] 1233 \\ REPEAT STRIP_TAC 1234 \\ `(SEP_BYTES_IN_MEM r3 [y;y';y'';y''';y''''] * r) (fun2set (f,df))` 1235 by FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES, 1236 STAR_ASSOC,word_arith_lemma1] 1237 \\ IMP_RES_TAC x86_encodes_jump_thm 1238 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1239 \\ Q.EXISTS_TAC `bs` \\ ASM_SIMP_TAC std_ss []) 1240 \\ `x86_encodes_jump (r3,n2w (w2n c),df,f) = (r3 + 5w,n2w (w2n c),df,fi)` by (Q.UNABBREV_TAC `fi` \\ SIMP_TAC std_ss [x86_encodes_jump_def,LET_DEF]) 1241 \\ ASM_SIMP_TAC std_ss [x86_encodes_jump_pre_def,LET_DEF] 1242 \\ Q.EXISTS_TAC `(n =+ SOME r3) j` \\ ASM_SIMP_TAC std_ss [] 1243 \\ Q.UNABBREV_TAC `d` \\ FULL_SIMP_TAC std_ss [INSTR_LENGTH_def,APPLY_UPDATE_THM] 1244 \\ FULL_SIMP_TAC std_ss [MATCH_MP MAP_INV_IGNORE (DECIDE ``n < n+1``)] 1245 \\ SIMP_TAC std_ss [DECIDE ``n < m ==> ~(n = m:num)``] 1246 \\ REVERSE (REPEAT STRIP_TAC) 1247 THEN1 (`i <> n` by DECIDE_TAC \\ METIS_TAC []) 1248 THEN1 (METIS_TAC []) 1249 THEN1 1250 (`(n + 1 <= p) \/ (n = p)` by DECIDE_TAC THEN1 (METIS_TAC []) 1251 \\ FULL_SIMP_TAC std_ss [] 1252 \\ SIMP_TAC std_ss [ON_OFF_def] 1253 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def]) 1254 \\ IMP_RES_TAC CODE_LOOP_UNROLL 1255 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1256 \\ FULL_SIMP_TAC std_ss [CODE_INV_def,INSTR_IN_MEM_def,APPLY_UPDATE_THM] 1257 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,APPLY_UPDATE_THM] 1258 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,GSYM STAR_ASSOC] 1259 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def,ENCODES_JUMP_def] 1260 \\ Q.PAT_X_ASSUM `y = bbbb` ASSUME_TAC 1261 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES,X86_IMMEDIATE_def,APPEND] 1262 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 1263 \\ SEP_READ_TAC) 1264 THEN1 1265 (ONCE_REWRITE_TAC [x86_writecode_def,x86_writecode_pre_def] 1266 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,n2w_11] 1267 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED] 1268 \\ `(IS_JUMP (iJEQ c))` by EVAL_TAC 1269 \\ Q.ABBREV_TAC `d = iJEQ c` 1270 \\ SIMP_TAC std_ss [x86_write_jcc_def,x86_write_jcc_pre_def,LET_DEF] 1271 \\ `g (r6 + 1w) = n2w (ORD (CHR (48 + w2n c)))` by SEP_READ_TAC 1272 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 1273 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 1274 \\ Q.ABBREV_TAC `f3 = (r3 + 0x7w =+ 0x0w) 1275 ((r3 + 0x6w =+ 0x0w) 1276 ((r3 + 0x5w =+ 0x0w) 1277 ((r3 + 0x4w =+ 0x5w) 1278 ((r3 + 0x3w =+ 0x84w) 1279 ((r3 + 0x2w =+ 0xFw) 1280 ((r3 + 0x1w =+ 0x7w) 1281 ((r3 =+ 0x3Bw) f)))))))` 1282 \\ `?f4. x86_encodes_jump (r3 + 0x8w,n2w n + 0x1w,df,f3) = 1283 (r3 + 0xDw,n2w n + 0x1w,df,f4)` by 1284 SIMP_TAC std_ss [x86_encodes_jump_def,LET_DEF,word_arith_lemma1] 1285 \\ ASM_SIMP_TAC std_ss [] 1286 \\ `?f5. x86_encodes_jump (r3 + 0xDw,n2w (w2n c),df,f4) = 1287 (r3 + 0x12w,n2w (w2n c),df,f5)` by 1288 SIMP_TAC std_ss [x86_encodes_jump_def,LET_DEF,word_arith_lemma1] 1289 \\ ASM_SIMP_TAC std_ss [x86_encodes_jump_pre_def,LET_DEF,GSYM CONJ_ASSOC] 1290 \\ SIMP_TAC std_ss [word_arith_lemma1] 1291 \\ `CODE_INV (r3 + n2w (INSTR_LENGTH d)) cs ((n =+ SOME r3) j) (fun2set (f5,df))` by 1292 (MATCH_MP_TAC CODE_INV_UPDATE 1293 \\ Q.EXISTS_TAC `f` \\ Q.UNABBREV_TAC `d` 1294 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def,INSTR_IN_MEM_def] 1295 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES,CODE_SPACE_UNWIND] 1296 \\ SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,X86_ENCODE_def,SEP_BYTES_IN_MEM_def] 1297 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,CODE_SPACE_def,word_arith_lemma1] 1298 \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 1299 \\ Q.SPEC_TAC (`y`,`y0`) \\ STRIP_TAC 1300 \\ Q.SPEC_TAC (`y'`,`y1`) \\ STRIP_TAC 1301 \\ Q.SPEC_TAC (`y''`,`y2`) \\ STRIP_TAC 1302 \\ Q.SPEC_TAC (`y'''`,`y3`) \\ STRIP_TAC 1303 \\ Q.SPEC_TAC (`y''''`,`y4`) \\ STRIP_TAC 1304 \\ Q.SPEC_TAC (`y'''''`,`y5`) \\ STRIP_TAC 1305 \\ Q.SPEC_TAC (`y''''''`,`y6`) \\ STRIP_TAC 1306 \\ Q.SPEC_TAC (`y'''''''`,`y7`) \\ STRIP_TAC 1307 \\ Q.SPEC_TAC (`y''''''''`,`y8`) \\ STRIP_TAC 1308 \\ Q.SPEC_TAC (`y'''''''''`,`y9`) \\ STRIP_TAC 1309 \\ Q.SPEC_TAC (`y''''''''''`,`y10`) \\ STRIP_TAC 1310 \\ Q.SPEC_TAC (`y'''''''''''`,`y11`) \\ STRIP_TAC 1311 \\ Q.SPEC_TAC (`y''''''''''''`,`y12`) \\ STRIP_TAC 1312 \\ Q.SPEC_TAC (`y'''''''''''''`,`y13`) \\ STRIP_TAC 1313 \\ Q.SPEC_TAC (`y''''''''''''''`,`y14`) \\ STRIP_TAC 1314 \\ Q.SPEC_TAC (`y'''''''''''''''`,`y15`) \\ STRIP_TAC 1315 \\ Q.SPEC_TAC (`y''''''''''''''''`,`y16`) \\ STRIP_TAC 1316 \\ Q.SPEC_TAC (`y'''''''''''''''''`,`y17`) \\ STRIP_TAC 1317 \\ REPEAT STRIP_TAC 1318 \\ `(SEP_BYTES_IN_MEM (r3 + 8w) [y8;y9;y10;y11;y12] * 1319 (SEP_BYTES_IN_MEM r3 [0x3Bw; 0x7w; 0xFw; 0x84w; 0x5w; 0x0w; 0x0w; 0x0w] * 1320 SEP_BYTES_IN_MEM (r3 + 13w) [y13;y14;y15;y16;y17] * r)) (fun2set (f3,df))` by 1321 (Q.UNABBREV_TAC `f3` 1322 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES,word_arith_lemma1] 1323 \\ SEP_WRITE_TAC) 1324 \\ Q.PAT_X_ASSUM `Abbrev (f3 = fff)` (K ALL_TAC) 1325 \\ `n + 1 < 256` by DECIDE_TAC 1326 \\ IMP_RES_TAC (Q.INST [`i`|->`i+1`] x86_encodes_jump_thm) 1327 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1328 \\ FULL_SIMP_TAC std_ss [] 1329 \\ Q.PAT_X_ASSUM `f2 = f4` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 1330 \\ `(SEP_BYTES_IN_MEM (r3 + 0xDw) [y13; y14; y15; y16; y17] * 1331 (SEP_BYTES_IN_MEM r3 [0x3Bw; 0x7w; 0xFw; 0x84w; 0x5w; 0x0w; 0x0w; 0x0w] * 1332 SEP_BYTES_IN_MEM (r3 + 0x8w) bs * r)) 1333 (fun2set (f2,df))` by FULL_SIMP_TAC (std_ss++star_ss) [] 1334 \\ Q.PAT_X_ASSUM `(SEP_BYTES_IN_MEM (r3 + 0x8w) bs * rr) ggg` (K ALL_TAC) 1335 \\ IMP_RES_TAC (Q.INST [`i`|->`w2n (c:word7)`,`a`|->`a+0xDw`] x86_encodes_jump_thm) 1336 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1337 \\ FULL_SIMP_TAC std_ss [] 1338 \\ Q.PAT_X_ASSUM `f2' = f5` (fn th => FULL_SIMP_TAC std_ss [th]) 1339 \\ IMP_RES_TAC (Q.SPEC `a + 8w` ENCODES_JUMP_IMP) 1340 \\ IMP_RES_TAC (Q.SPEC `a + 0xDw` ENCODES_JUMP_IMP) 1341 \\ FULL_SIMP_TAC std_ss [] 1342 \\ Q.EXISTS_TAC `[0x3Bw; 0x7w; 0xFw; 0x84w; 0x5w; 0x0w; 0x0w; 0x0w] ++ 1343 [z1; z2; z3; z4; z5] ++ [z1'; z2'; z3'; z4'; z5']` 1344 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC THEN1 1345 (Q.EXISTS_TAC `[z1; z2; z3; z4; z5]` 1346 \\ Q.EXISTS_TAC `[z1'; z2'; z3'; z4'; z5']` 1347 \\ ASM_SIMP_TAC std_ss []) 1348 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,word_arith_lemma1,SEP_CLAUSES,APPEND] 1349 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 1350 \\ Q.PAT_X_ASSUM `Abbrev (f3 = fff)` (K ALL_TAC) 1351 \\ Q.EXISTS_TAC `(n =+ SOME r3) j` \\ ASM_SIMP_TAC std_ss [] 1352 \\ Q.UNABBREV_TAC `d` \\ FULL_SIMP_TAC std_ss [INSTR_LENGTH_def,APPLY_UPDATE_THM] 1353 \\ FULL_SIMP_TAC std_ss [MATCH_MP MAP_INV_IGNORE (DECIDE ``n < n+1``)] 1354 \\ SIMP_TAC std_ss [DECIDE ``n < m ==> ~(n = m:num)``] 1355 \\ REVERSE (REPEAT STRIP_TAC) 1356 THEN1 (`i <> n` by DECIDE_TAC \\ METIS_TAC []) 1357 THEN1 (METIS_TAC []) 1358 THEN1 1359 (`(n + 1 <= p) \/ (n = p)` by DECIDE_TAC THEN1 (METIS_TAC []) 1360 \\ FULL_SIMP_TAC std_ss [] 1361 \\ SIMP_TAC std_ss [ON_OFF_def] 1362 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def]) 1363 \\ IMP_RES_TAC CODE_LOOP_UNROLL 1364 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1365 \\ FULL_SIMP_TAC std_ss [CODE_INV_def,INSTR_IN_MEM_def,APPLY_UPDATE_THM] 1366 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,APPLY_UPDATE_THM] 1367 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,GSYM STAR_ASSOC] 1368 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def] 1369 \\ IMP_RES_TAC ENCODES_JUMP_IMP 1370 \\ FULL_SIMP_TAC std_ss [APPEND] 1371 \\ Q.PAT_X_ASSUM `y = bbbb` ASSUME_TAC 1372 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES,X86_IMMEDIATE_def,APPEND] 1373 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 1374 \\ SEP_READ_TAC) 1375 THEN1 1376 (ONCE_REWRITE_TAC [x86_writecode_def,x86_writecode_pre_def] 1377 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,n2w_11] 1378 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED] 1379 \\ `(IS_JUMP (iJLT c))` by EVAL_TAC 1380 \\ Q.ABBREV_TAC `d = iJLT c` 1381 \\ SIMP_TAC std_ss [x86_write_jcc_def,x86_write_jcc_pre_def,LET_DEF] 1382 \\ `g (r6 + 1w) = n2w (ORD (CHR (48 + w2n c)))` by SEP_READ_TAC 1383 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 1384 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 1385 \\ Q.ABBREV_TAC `f3 = (r3 + 0x7w =+ 0x0w) 1386 ((r3 + 0x6w =+ 0x0w) 1387 ((r3 + 0x5w =+ 0x0w) 1388 ((r3 + 0x4w =+ 0x5w) 1389 ((r3 + 0x3w =+ 0x84w) 1390 ((r3 + 0x2w =+ 0xFw) 1391 ((r3 + 0x1w =+ 0x7w) 1392 ((r3 =+ 0x3Bw) f)))))))` 1393 \\ `?f4. x86_encodes_jump (r3 + 0x8w,n2w n + 0x1w,df,f3) = 1394 (r3 + 0xDw,n2w n + 0x1w,df,f4)` by 1395 SIMP_TAC std_ss [x86_encodes_jump_def,LET_DEF,word_arith_lemma1] 1396 \\ ASM_SIMP_TAC std_ss [] 1397 \\ SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4] 1398 \\ `?f5. x86_encodes_jump (r3 + 0xDw,n2w (w2n c),df,(r3 + 0x3w =+ 0x82w) f4) = 1399 (r3 + 0x12w,n2w (w2n c),df,f5)` by 1400 SIMP_TAC std_ss [x86_encodes_jump_def,LET_DEF,word_arith_lemma1] 1401 \\ ASM_SIMP_TAC std_ss [x86_encodes_jump_pre_def,LET_DEF,GSYM CONJ_ASSOC] 1402 \\ SIMP_TAC std_ss [word_arith_lemma1] 1403 \\ Q.EXISTS_TAC `(n =+ SOME r3) j` \\ ASM_SIMP_TAC std_ss [] 1404 \\ FULL_SIMP_TAC std_ss [MATCH_MP MAP_INV_IGNORE (DECIDE ``n < n+1``)] 1405 \\ `CODE_INV (r3 + n2w (INSTR_LENGTH d)) cs ((n =+ SOME r3) j) (fun2set (f5,df))` by 1406 (MATCH_MP_TAC CODE_INV_UPDATE 1407 \\ Q.EXISTS_TAC `f` \\ Q.UNABBREV_TAC `d` 1408 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def,INSTR_IN_MEM_def] 1409 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES,CODE_SPACE_UNWIND] 1410 \\ SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,X86_ENCODE_def,SEP_BYTES_IN_MEM_def] 1411 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,CODE_SPACE_def,word_arith_lemma1] 1412 \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 1413 \\ Q.SPEC_TAC (`y`,`y0`) \\ STRIP_TAC 1414 \\ Q.SPEC_TAC (`y'`,`y1`) \\ STRIP_TAC 1415 \\ Q.SPEC_TAC (`y''`,`y2`) \\ STRIP_TAC 1416 \\ Q.SPEC_TAC (`y'''`,`y3`) \\ STRIP_TAC 1417 \\ Q.SPEC_TAC (`y''''`,`y4`) \\ STRIP_TAC 1418 \\ Q.SPEC_TAC (`y'''''`,`y5`) \\ STRIP_TAC 1419 \\ Q.SPEC_TAC (`y''''''`,`y6`) \\ STRIP_TAC 1420 \\ Q.SPEC_TAC (`y'''''''`,`y7`) \\ STRIP_TAC 1421 \\ Q.SPEC_TAC (`y''''''''`,`y8`) \\ STRIP_TAC 1422 \\ Q.SPEC_TAC (`y'''''''''`,`y9`) \\ STRIP_TAC 1423 \\ Q.SPEC_TAC (`y''''''''''`,`y10`) \\ STRIP_TAC 1424 \\ Q.SPEC_TAC (`y'''''''''''`,`y11`) \\ STRIP_TAC 1425 \\ Q.SPEC_TAC (`y''''''''''''`,`y12`) \\ STRIP_TAC 1426 \\ Q.SPEC_TAC (`y'''''''''''''`,`y13`) \\ STRIP_TAC 1427 \\ Q.SPEC_TAC (`y''''''''''''''`,`y14`) \\ STRIP_TAC 1428 \\ Q.SPEC_TAC (`y'''''''''''''''`,`y15`) \\ STRIP_TAC 1429 \\ Q.SPEC_TAC (`y''''''''''''''''`,`y16`) \\ STRIP_TAC 1430 \\ Q.SPEC_TAC (`y'''''''''''''''''`,`y17`) \\ STRIP_TAC 1431 \\ REPEAT STRIP_TAC 1432 \\ `(SEP_BYTES_IN_MEM (r3 + 8w) [y8;y9;y10;y11;y12] * 1433 (SEP_BYTES_IN_MEM r3 [0x3Bw; 0x7w; 0xFw; 0x84w; 0x5w; 0x0w; 0x0w; 0x0w] * 1434 SEP_BYTES_IN_MEM (r3 + 13w) [y13;y14;y15;y16;y17] * r)) (fun2set (f3,df))` by 1435 (Q.UNABBREV_TAC `f3` 1436 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES,word_arith_lemma1] 1437 \\ SEP_WRITE_TAC) 1438 \\ Q.PAT_X_ASSUM `Abbrev (f3 = fff)` (K ALL_TAC) 1439 \\ `n + 1 < 256` by DECIDE_TAC 1440 \\ IMP_RES_TAC (Q.INST [`i`|->`i+1`] x86_encodes_jump_thm) 1441 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1442 \\ FULL_SIMP_TAC std_ss [] 1443 \\ Q.PAT_X_ASSUM `f2 = f4` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 1444 \\ `(SEP_BYTES_IN_MEM (r3 + 0xDw) [y13; y14; y15; y16; y17] * 1445 (SEP_BYTES_IN_MEM r3 [0x3Bw; 0x7w; 0xFw; 0x82w; 0x5w; 0x0w; 0x0w; 0x0w] * 1446 SEP_BYTES_IN_MEM (r3 + 0x8w) bs * r)) 1447 (fun2set ((r3 + 0x3w =+ 0x82w) f2,df))` by 1448 (FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,word_arith_lemma1,SEP_CLAUSES] 1449 \\ SEP_WRITE_TAC) 1450 \\ Q.PAT_X_ASSUM `(SEP_BYTES_IN_MEM (r3 + 0x8w) bs * rr) ggg` (K ALL_TAC) 1451 \\ IMP_RES_TAC (Q.INST [`i`|->`w2n (c:word7)`,`a`|->`a+0xDw`] x86_encodes_jump_thm) 1452 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1453 \\ FULL_SIMP_TAC std_ss [] 1454 \\ Q.PAT_X_ASSUM `f2' = f5` (fn th => FULL_SIMP_TAC std_ss [th]) 1455 \\ IMP_RES_TAC (Q.SPEC `a + 8w` ENCODES_JUMP_IMP) 1456 \\ IMP_RES_TAC (Q.SPEC `a + 0xDw` ENCODES_JUMP_IMP) 1457 \\ FULL_SIMP_TAC std_ss [] 1458 \\ Q.EXISTS_TAC `[0x3Bw; 0x7w; 0xFw; 0x82w; 0x5w; 0x0w; 0x0w; 0x0w] ++ 1459 [z1; z2; z3; z4; z5] ++ [z1'; z2'; z3'; z4'; z5']` 1460 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC THEN1 1461 (Q.EXISTS_TAC `[z1; z2; z3; z4; z5]` 1462 \\ Q.EXISTS_TAC `[z1'; z2'; z3'; z4'; z5']` 1463 \\ ASM_SIMP_TAC std_ss []) 1464 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,word_arith_lemma1,SEP_CLAUSES,APPEND] 1465 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 1466 \\ Q.PAT_X_ASSUM `Abbrev (f3 = fff)` (K ALL_TAC) 1467 \\ Q.UNABBREV_TAC `d` \\ FULL_SIMP_TAC std_ss [INSTR_LENGTH_def,APPLY_UPDATE_THM] 1468 \\ FULL_SIMP_TAC std_ss [MATCH_MP MAP_INV_IGNORE (DECIDE ``n < n+1``)] 1469 \\ SIMP_TAC std_ss [DECIDE ``n < m ==> ~(n = m:num)``] 1470 \\ REVERSE (REPEAT STRIP_TAC) 1471 THEN1 (`i <> n` by DECIDE_TAC \\ METIS_TAC []) 1472 THEN1 (METIS_TAC []) 1473 THEN1 1474 (`(n + 1 <= p) \/ (n = p)` by DECIDE_TAC THEN1 (METIS_TAC []) 1475 \\ FULL_SIMP_TAC std_ss [] 1476 \\ SIMP_TAC std_ss [ON_OFF_def] 1477 \\ ASM_SIMP_TAC std_ss [INSTR_LENGTH_def]) 1478 \\ IMP_RES_TAC CODE_LOOP_UNROLL 1479 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `(n =+ SOME r3) j`) 1480 \\ FULL_SIMP_TAC std_ss [CODE_INV_def,INSTR_IN_MEM_def,APPLY_UPDATE_THM] 1481 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,APPLY_UPDATE_THM] 1482 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,cond_STAR,GSYM STAR_ASSOC] 1483 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def] 1484 \\ IMP_RES_TAC ENCODES_JUMP_IMP 1485 \\ FULL_SIMP_TAC std_ss [APPEND] 1486 \\ Q.PAT_X_ASSUM `y = bbbb` ASSUME_TAC 1487 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES,X86_IMMEDIATE_def,APPEND] 1488 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 1489 \\ SEP_READ_TAC)); 1490 1491val prev_jump_NONE = prove( 1492 ``!j cs n. n < LENGTH cs /\ (!p. ON_OFF cs j p) ==> 1493 ((j (prev_jump cs n) = NONE) = (j n = NONE))``, 1494 STRIP_TAC \\ STRIP_TAC \\ Induct 1495 \\ SIMP_TAC std_ss [prev_jump_def] \\ REPEAT STRIP_TAC 1496 \\ Cases_on `IS_JUMP (EL n cs)` \\ FULL_SIMP_TAC std_ss [ADD1] 1497 \\ `n < LENGTH cs` by DECIDE_TAC 1498 \\ FULL_SIMP_TAC std_ss [] 1499 \\ `?c. EL n cs = c` by METIS_TAC [] 1500 \\ `?c2. EL (n+1) cs = c2` by METIS_TAC [] 1501 \\ IMP_RES_TAC iFETCH_IMP 1502 \\ FULL_SIMP_TAC std_ss [ON_OFF_def]); 1503 1504val MAP_INV_DROP_THM = prove( 1505 ``!n i j a cs. MAP_INV a i j cs = MAP_INV a i j (TAKE n cs) * MAP_INV (a + n2w (8 * n)) (i + n) j (DROP n (cs:input_type list))``, 1506 Induct \\ REPEAT STRIP_TAC 1507 \\ SIMP_TAC std_ss [TAKE_0,DROP_0,SEP_CLAUSES,MAP_INV_def,WORD_ADD_0] 1508 \\ Cases_on `cs` \\ SIMP_TAC std_ss [MAP_INV_def,DROP_def,SEP_CLAUSES,TAKE_def] 1509 \\ SIMP_TAC std_ss [MULT_CLAUSES,GSYM word_add_n2w,WORD_ADD_ASSOC] 1510 \\ SIMP_TAC std_ss [RW1[ADD_COMM]ADD1,ADD_ASSOC] 1511 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`i+1`,`j`,`a + 8w`,`t`]) 1512 \\ ASM_SIMP_TAC std_ss [] \\ ASM_SIMP_TAC std_ss [STAR_ASSOC,MAP_INV_def]); 1513 1514val IS_JUMP_prev_jump = prove( 1515 ``!n cs. 0 < prev_jump cs n ==> IS_JUMP (EL (prev_jump cs n - 1) cs)``, 1516 Induct \\ SIMP_TAC std_ss [prev_jump_def] \\ REPEAT STRIP_TAC 1517 \\ Cases_on `IS_JUMP (EL n cs)` \\ ASM_SIMP_TAC std_ss [] 1518 \\ FULL_SIMP_TAC std_ss []); 1519 1520val iFETCH_IMP_EL = prove( 1521 ``!p cs i. (iFETCH p cs = SOME i) ==> (EL p cs = i)``, 1522 Induct \\ Cases \\ ASM_SIMP_TAC std_ss [iFETCH_def,EL,HD,ADD1,TL]); 1523 1524val IMP_ON_OFF = prove( 1525 ``(!p. (prev_jump cs n) <= p ==> ON_OFF cs j2 p) /\ 1526 (!p. ON_OFF cs j p) /\ 1527 (!p. p < prev_jump cs n ==> (j p = j2 p)) ==> 1528 (!p. ON_OFF cs j2 p)``, 1529 ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ REPEAT STRIP_TAC 1530 \\ Cases_on `prev_jump cs n <= p` THEN1 METIS_TAC [] 1531 \\ FULL_SIMP_TAC std_ss [DECIDE ``~(n <= m) = m < n:num``] 1532 \\ Cases_on `p + 1 < prev_jump cs n` THEN1 1533 (RES_TAC \\ `ON_OFF cs j p` by METIS_TAC [] 1534 \\ FULL_SIMP_TAC std_ss [ON_OFF_def]) 1535 \\ `(prev_jump cs n = p + 1) /\ 0 < prev_jump cs n` by DECIDE_TAC 1536 \\ IMP_RES_TAC IS_JUMP_prev_jump 1537 \\ POP_ASSUM MP_TAC 1538 \\ ASM_SIMP_TAC std_ss [ON_OFF_def] 1539 \\ REPEAT STRIP_TAC 1540 \\ IMP_RES_TAC iFETCH_IMP_EL 1541 \\ FULL_SIMP_TAC std_ss []); 1542 1543val MAP_INV_TAKE_EQ = prove( 1544 ``!k a cs i. 1545 (!p. p < i + k ==> (j p = j2 p)) ==> 1546 (MAP_INV a i j (TAKE k cs) = MAP_INV a i j2 (TAKE k (cs:input_type list)))``, 1547 Induct \\ SIMP_TAC std_ss [TAKE_0,MAP_INV_def] 1548 \\ Cases_on `cs` \\ SIMP_TAC std_ss [TAKE_def,MAP_INV_def] 1549 \\ SIMP_TAC std_ss [ADD1,MAP_INV_def] \\ REPEAT STRIP_TAC 1550 \\ `i < i + (k + 1)` by DECIDE_TAC 1551 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [] 1552 \\ MATCH_MP_TAC (METIS_PROVE [] ``(p = q) ==> (f m p = f m q)``) 1553 \\ Q.PAT_X_ASSUM `!a cs. bb` MATCH_MP_TAC 1554 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM]); 1555 1556val x86_newcode_thm = prove( 1557 `` LENGTH cs < 128 /\ ALIGNED r7 /\ n < LENGTH cs /\ 1558 (CODE_INV r3 cs j) (fun2set (f,df)) /\ 1559 (pp * one (r7 - 0x20w,n2w n) * one (r7 - 8w,r3) * one (r7 - 4w,r6) * MAP_INV r7 0 j cs) (fun2set (h,dh)) /\ 1560 (q * one_string_0 r6 (iENCODE cs) b1) (fun2set (g,dg)) ==> 1561 (!p. ON_OFF cs j p) /\ 1562 ((r1 = 0w) = (j n = NONE)) ==> 1563 ?f2 h2 j2 r3i. 1564 x86_newcode_pre (r1,n2w n,r7,df,f,dg,g,dh,h) /\ 1565 (x86_newcode (r1,n2w n,r7,df,f,dg,g,dh,h) = 1566 (r7,df,f2,dg,g,dh,h2)) /\ 1567 ~(j2 n = NONE) /\ 1568 (CODE_INV r3i cs j2) (fun2set (f2,df)) /\ 1569 (pp * one (r7 - 0x20w,n2w n) * one (r7 - 8w,r3i) * one (r7 - 4w,r6) * MAP_INV r7 0 j2 cs) (fun2set (h2,dh)) /\ 1570 (!p. ON_OFF cs j2 p) /\ !i. ~(j i = NONE) \/ LENGTH cs <= i ==> (j2 i = j i)``, 1571 SIMP_TAC std_ss [x86_newcode_def,x86_newcode_pre_def] 1572 \\ REVERSE (Cases_on `j n = NONE`) \\ ASM_SIMP_TAC std_ss [] 1573 THEN1 (REPEAT STRIP_TAC \\ Q.EXISTS_TAC `j` \\ Q.EXISTS_TAC `r3` 1574 \\ ASM_SIMP_TAC std_ss []) 1575 \\ ASM_SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 1576 \\ `(h (r7 - 4w) = r6) /\ (r7 - 4w) IN dh` by SEP_READ_TAC 1577 \\ `(h (r7 - 8w) = r3) /\ (r7 - 8w) IN dh` by SEP_READ_TAC 1578 \\ ASM_SIMP_TAC std_ss [] 1579 \\ `LENGTH cs <= 128` by DECIDE_TAC 1580 \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o 1581 Q.INST [`p`|->`n`,`r2`|->`r6`]) x86_findbyte_thm 1582 \\ `r7 - 0x20w IN dh /\ (h (r7 - 0x20w) = n2w n)` by SEP_READ_TAC 1583 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED,word_arith_lemma2, 1584 DECIDE ``n < j = ~(j <= n:num)``] 1585 \\ `j (n - ji) = NONE` by METIS_TAC [prev_jump_NONE] 1586 \\ `n - ji < LENGTH cs` by DECIDE_TAC 1587 \\ `ALIGNED (r7 + n2w (8 * (n - ji)))` by 1588 (ASM_SIMP_TAC bool_ss [DECIDE ``8 = 4 * 2``,GSYM WORD_MULT_ASSOC, 1589 ALIGNED_CLAUSES,GSYM word_mul_n2w]) 1590 \\ STRIP_ASSUME_TAC (Q.SPECL [`n - ji`,`0`,`j`,`r7`,`cs`] MAP_INV_DROP_THM) 1591 \\ FULL_SIMP_TAC std_ss [word_mul_n2w] 1592 \\ MP_TAC (Q.INST [`q`|->`qi`,`pp`|->`pp * one (r7 - 0x20w,n2w n) * one (r7 - 0x8w,r3) * one (r7 - 0x4w,r6) * MAP_INV r7 0 j (TAKE (n - ji) cs)`] 1593 (MATCH_INST (SPEC_ALL x86_writecode_thm) 1594 ``x86_writecode (r3,r7 + 0x8w * n2w (n - ji),n2w (n - ji),r6i,df,f,dg,g,dh,h)``)) 1595 \\ FULL_SIMP_TAC std_ss [word_mul_n2w,STAR_ASSOC] \\ REPEAT STRIP_TAC 1596 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,WORD_MUL_LSL,word_mul_n2w] 1597 \\ Q.EXISTS_TAC `j2` \\ Q.EXISTS_TAC `r3i` 1598 \\ `r7 - 0x8w IN dh` by SEP_READ_TAC 1599 \\ FULL_SIMP_TAC bool_ss [DECIDE ``m <= n + p = m - n <= p:num``] 1600 \\ `!p. ON_OFF cs j2 p` by METIS_TAC [IMP_ON_OFF] 1601 \\ ASM_SIMP_TAC std_ss [] 1602 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 1603 \\ ASM_SIMP_TAC std_ss [] 1604 \\ STRIP_ASSUME_TAC (Q.SPECL [`n - ji`,`0`,`j2`,`r7`,`cs`] MAP_INV_DROP_THM) 1605 \\ FULL_SIMP_TAC std_ss [] 1606 \\ IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPECL [`k`,`a`,`cs`,`0`] MAP_INV_TAKE_EQ)) 1607 \\ FULL_SIMP_TAC std_ss [] 1608 \\ IMP_RES_TAC (GSYM prev_jump_NONE) \\ ASM_SIMP_TAC std_ss [] 1609 \\ STRIP_TAC THEN1 SEP_WRITE_TAC 1610 \\ METIS_TAC []); 1611 1612val lemma1 = prove( 1613 ``!x. ((if x = NONE then 0x0w else 0x1w) = 0x0w) = (x = NONE)``, 1614 Cases \\ SIMP_TAC std_ss [n2w_11,ONE_LT_dimword,ZERO_LT_dimword]); 1615 1616val x86_inc_thm = prove( 1617 ``state_inv cs dh h dg g df f r7 j /\ n < LENGTH cs /\ 1618 ((h (r7 - 0x24w) = 0w) ==> cont_jump j p cs r4 (n2w n)) ==> 1619 ?h2 f2 j2 w. 1620 x86_inc_pre (r1,r2,r3,r4,n2w n,r6,r7,dh,h,df,f,dg,g) /\ 1621 (x86_inc (r1,r2,r3,r4,n2w n,r6,r7,dh,h,df,f,dg,g) = 1622 (r1,r2,r3,w,0w,r6,r7,dh,h2,df,f2,dg,g)) /\ 1623 state_inv cs dh h2 dg g df f2 r7 j2 /\ (j2 n = SOME w)``, 1624 SIMP_TAC std_ss [state_inv_def,SimpLHS,MAP_TEMP_INV_def] \\ REPEAT STRIP_TAC 1625 \\ SIMP_TAC std_ss [x86_inc_def,x86_inc_pre_def,LET_DEF] 1626 \\ Q.PAT_ABBREV_TAC `h3 = (r7 - 0x20w:word32 =+ (n2w n):word32) fff` 1627 \\ `?ww. (SEP_T * one (r7 - 0xCw,r1) * one (r7 - 0x10w,r2) * one (r7 - 0x14w,r3) * 1628 one (r7 - 0x18w,r4) * one (r7 - 0x1Cw,r6) * one (r7 - 0x24w,ww) * 1629 one (r7 - 0x20w,n2w n) * one (r7 - 0x8w,a) * one (r7 - 0x4w,b) * 1630 MAP_INV r7 0 j cs) (fun2set (h3,dh))` by 1631 (FULL_SIMP_TAC std_ss [TEMP_INV_UNROLL,word_arith_lemma1,TEMP_INV_def,SEP_CLAUSES] 1632 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,STAR_ASSOC] 1633 \\ Q.EXISTS_TAC `y''''''` \\ Q.UNABBREV_TAC `h3` \\ SEP_WRITE_TAC) 1634 \\ `h (r7 - 0x24w) = ww` by 1635 (`h (r7 - 0x24w) = h3 (r7 - 0x24w)` by (Q.UNABBREV_TAC `h3` 1636 \\ SIMP_TAC (std_ss++SIZES_ss) [APPLY_UPDATE_THM,WORD_EQ_ADD_LCANCEL, 1637 word_sub_def,word_2comp_n2w,n2w_11]) 1638 \\ ASM_SIMP_TAC std_ss [] \\ SEP_READ_TAC) 1639 \\ Q.PAT_X_ASSUM `Abbrev bbb` (K ALL_TAC) 1640 \\ `LENGTH cs <= 128` by DECIDE_TAC 1641 \\ IMP_RES_TAC x86_access_j_thm 1642 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED] 1643 \\ REPEAT (Q.PAT_X_ASSUM `x86_access_j bb = nnn` (K ALL_TAC)) 1644 \\ REPEAT (Q.PAT_X_ASSUM `x86_access_j_pre bb` (K ALL_TAC)) 1645 \\ ASM_SIMP_TAC std_ss [] 1646 \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [SEP_CLAUSES] o 1647 Q.INST [`r3`|->`a`,`r6`|->`b`,`pp`|->`SEP_T * one (r7 - 0xCw,r1) * one (r7 - 0x10w,r2) * 1648 one (r7 - 0x14w,r3) * one (r7 - 0x18w,r4) * one (r7 - 0x1Cw,r6) * one (r7 - 0x24w,ww)`,`q`|->`emp`] o 1649 RW [lemma1,GSYM AND_IMP_INTRO] o MATCH_INST x86_newcode_thm) 1650 ``x86_newcode (if (j:num->word32 option) n = NONE 1651 then 0x0w else 0x1w,n2w n,r7,df,f,dg,g,dh,h3)`` 1652 \\ ASM_SIMP_TAC std_ss [] 1653 \\ REPEAT (Q.PAT_X_ASSUM `x86_newcode bb = nnn` (K ALL_TAC)) 1654 \\ REPEAT (Q.PAT_X_ASSUM `x86_newcode_pre bb` (K ALL_TAC)) 1655 \\ `h2 (r7 - 0x20w) = n2w n` by SEP_READ_TAC 1656 \\ ASM_SIMP_TAC std_ss [] 1657 \\ IMP_RES_TAC x86_access_j_thm 1658 \\ ASM_SIMP_TAC std_ss [] 1659 \\ REPEAT (Q.PAT_X_ASSUM `x86_access_j bb = nnn` (K ALL_TAC)) 1660 \\ REPEAT (Q.PAT_X_ASSUM `x86_access_j_pre bb` (K ALL_TAC)) 1661 \\ Cases_on `j2 n` \\ FULL_SIMP_TAC std_ss [] 1662 \\ `h2 (r7 - 0x18w) = r4` by SEP_READ_TAC 1663 \\ ASM_SIMP_TAC std_ss [] 1664 \\ `n < 128` by DECIDE_TAC 1665 \\ `(ww = 0w) ==> cont_jump j2 p cs r4 (n2w n)` by 1666 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [cont_jump_def,input_type_11]) 1667 \\ (STRIP_ASSUME_TAC o UNDISCH o UNDISCH o UNDISCH o UNDISCH o 1668 REWRITE_RULE [GSYM CODE_INV_def] o 1669 Q.INST [`r`|->`CODE_SPACE r3i (SPACE_LENGTH 0 j2 cs)`] o 1670 SIMP_RULE (std_ss++SIZES_ss) [WORD_SUB_ADD,w2n_n2w,GSYM AND_IMP_INTRO] o 1671 DISCH ``n < 128`` o Q.INST [`t`|->`n2w n`,`j`|->`j2`] o 1672 MATCH_INST x86_write_jump_cond_thm) ``x86_write_jump_cond (ww,x,r4 + 0x5w,df,f2)`` 1673 \\ `h2 (r7 - 0x24w) = ww` by SEP_READ_TAC 1674 \\ ASM_SIMP_TAC std_ss [] 1675 \\ Q.EXISTS_TAC `j2` 1676 \\ ASM_SIMP_TAC std_ss [CONJ_ASSOC] 1677 \\ STRIP_TAC THEN1 SEP_READ_TAC 1678 \\ ASM_SIMP_TAC std_ss [] 1679 \\ Q.EXISTS_TAC `r3i` 1680 \\ Q.EXISTS_TAC `b` 1681 \\ Q.EXISTS_TAC `b1` 1682 \\ ASM_SIMP_TAC std_ss [TEMP_INV_UNROLL,word_arith_lemma1] 1683 \\ SIMP_TAC std_ss [SEP_CLAUSES,TEMP_INV_def,STAR_ASSOC] 1684 \\ SIMP_TAC std_ss [SEP_EXISTS] 1685 \\ Q.EXISTS_TAC `r1` 1686 \\ Q.EXISTS_TAC `r2` 1687 \\ Q.EXISTS_TAC `r3` 1688 \\ Q.EXISTS_TAC `r4` 1689 \\ Q.EXISTS_TAC `r6` 1690 \\ Q.EXISTS_TAC `n2w n` 1691 \\ Q.EXISTS_TAC `0w` 1692 \\ SEP_WRITE_TAC); 1693 1694val SPEC_PUSH_COND = prove( 1695 ``SPEC m (p * cond b) c q ==> SPEC m (p * cond b) c (q * cond b)``, 1696 SIMP_TAC std_ss [SPEC_MOVE_COND,SEP_CLAUSES]); 1697 1698val X86_STACK_def = Define ` 1699 X86_STACK (esp,xs,l) = xR ESP esp * xLIST esp xs * 1700 xSPACE esp l * cond (ALIGNED esp)`; 1701 1702val pop_esi = let 1703 val ((th,_,_),_) = prog_x86Lib.x86_spec (x86_encodeLib.x86_encode "pop esi") 1704 val th = Q.INST [`df`|->`{esp}`] (DISCH ``ALIGNED esp`` th) 1705 val th = INST [``f:word32->word32``|->``\x:word32.(w:word32)``] (DISCH_ALL th) 1706 val th = SIMP_RULE std_ss [IN_INSERT,NOT_IN_EMPTY,xM_THM,ALIGNED] th 1707 val th = SIMP_RULE bool_ss [GSYM SPEC_MOVE_COND] th 1708 val th = SPEC_FRAME_RULE th ``xLIST (esp+4w) xs * xSPACE esp n * cond (ALIGNED esp)`` 1709 val th = HIDE_POST_RULE ``xM esp`` th 1710 val th = HIDE_PRE_RULE ``xR ESI`` th 1711 val (th,goal) = SPEC_STRENGTHEN_RULE th ``xPC eip * X86_STACK (esp,w::xs,n) * ~xR ESI`` 1712 val lemma = prove(goal, 1713 SIMP_TAC (std_ss++sep_cond_ss) [X86_STACK_def,SEP_IMP_MOVE_COND, 1714 ALIGNED_INTRO,SEP_CLAUSES,xLIST_def] 1715 \\ SIMP_TAC (std_ss++star_ss) [SEP_IMP_REFL]) 1716 val th = MP th lemma 1717 val (th,goal) = SPEC_WEAKEN_RULE th ``xPC (eip+1w) * X86_STACK (esp+4w,xs,n+1) * xR ESI w`` 1718 val lemma = prove(goal, 1719 SIMP_TAC (bool_ss++sep_cond_ss) [X86_STACK_def,SEP_IMP_MOVE_COND, 1720 ALIGNED_INTRO,SEP_CLAUSES,xLIST_def,xSPACE_def,GSYM ADD1] 1721 \\ SIMP_TAC (std_ss++star_ss) [SEP_IMP_REFL,WORD_ADD_SUB,ALIGNED,SEP_CLAUSES]) 1722 val th = DISCH_ALL (MP th lemma) 1723 val th = Q.INST [`esp`|->`esp-4w`,`n`|->`0`,`xs`|->`[]`] th 1724 val th = SIMP_RULE std_ss [WORD_SUB_ADD] th 1725 in RW [] th end 1726 1727val (codege_code_def,x86_inc_lemma) = let 1728 val th = DISCH 1729 ``x86_inc (eax,edx,edi,esi,ecx,ebx,ebp,dh,h,df,f,dg,g) = 1730 (eax,edx,edi,w,0w,ebx,ebp,dh,h3,df,f3,dg,g)`` x86_inc_th 1731 val th = DISCH ``ALIGNED edi`` th 1732 val th = DISCH ``state_inv cs dh h dg g df f ebp j /\ n < LENGTH cs /\ 1733 ((h (ebp - 0x24w) = 0w) ==> cont_jump j pi cs esi (n2w n))`` th 1734 val th = SIMP_RULE std_ss [LET_DEF] th 1735 val th = RW [GSYM SPEC_MOVE_COND] th 1736 val ((sub_esi,_,_),_) = prog_x86Lib.x86_spec (x86_encodeLib.x86_encode "sub esi, 5") 1737 val (_,_,sts,_) = prog_x86Lib.x86_tools 1738 val sub_esi = HIDE_STATUS_RULE true sts sub_esi 1739 val th = SPEC_COMPOSE_RULE [Q.INST [`w`|->`esi`] pop_esi,sub_esi,th,xCODE_INTRO] 1740 val th = RW [STAR_ASSOC] th 1741 val th = SIMP_RULE (std_ss++sep_cond_ss) [] th 1742 val th = MATCH_MP SPEC_PUSH_COND th 1743 val th = Q.INST [`eip`|->`p`] th 1744 val (_,_,c,_) = dest_spec (concl th) 1745 val tm = ``(codegen_code (p:word32)):word32 # word8 list # bool -> bool`` 1746 val def = new_definition("codegen_code",mk_eq(tm,c)) 1747 val th = RW [GSYM def] th 1748 val th = RW [STAR_ASSOC] (RW1 [GSYM X86_SPEC_CODE] th) 1749 val th = Q.SPEC `xLIST edi xs * xSPACE edi l` (MATCH_MP SPEC_FRAME th) 1750 val th = RW [STAR_ASSOC] th 1751 val th = Q.INST [`eax`|->`x`,`p`|->`ebx`,`ecx`|->`n2w n`,`esi`|->`cp + 5w`] th 1752 val th = SIMP_RULE std_ss [WORD_SUB_ADD,WORD_ADD_SUB] th 1753 in (def,th) end 1754 1755(* main invariant definition: xINC_def *) 1756 1757val xINC_def = Define ` 1758 xINC (xs,l,p,cs:input_type list) (pw,r,esp) = 1759 SEP_EXISTS dh dg df jw g h f j eip. 1760 xR EBX pw * xCODE (codegen_code pw) * ~xR ESI * xR ECX 0w * 1761 xSTACK (xs,l,p,cs) * xMEMORY dh h * xBYTE_MEMORY dg g * xR EDX r * 1762 xR EBP jw * ~xS * xPC eip * xCODE (xCODE_SET df f) * X86_STACK (esp,[],1) * 1763 cond (state_inv cs dh h dg g df f jw j /\ (j p = SOME eip))`; 1764 1765val xINC_CODEGEN_def = Define ` 1766 xINC_CODEGEN (xs,l,p,cs:input_type list) (pw,r,esp) t = 1767 SEP_EXISTS dh h dg g df f jw j cp. 1768 xR EBX pw * xCODE (codegen_code pw) * ~xR ESI * xR ECX (n2w t) * 1769 xSTACK (xs,l,p,cs) * xMEMORY dh h * xBYTE_MEMORY dg g * xR EDX r * 1770 xR EBP jw * ~xS * xPC pw * xBYTE_MEMORY_X df f * X86_STACK (esp-4w,[cp+5w],0) * 1771 cond (state_inv cs dh h dg g df f jw j /\ p < LENGTH cs /\ t < LENGTH cs /\ 1772 ((h (jw - 0x24w) = 0x0w) ==> cont_jump j p cs cp (n2w t)))`; 1773 1774val xINC_JUMP_def = Define ` 1775 xINC_JUMP (xs,l,p,cs:input_type list) (pw,r,esp) t = 1776 SEP_EXISTS dh dg df jw g h f j eip bs. 1777 xR EBX pw * xCODE (codegen_code pw) * ~xR ESI * xR ECX 0w * 1778 xSTACK (xs,l,p,cs) * xMEMORY dh h * xBYTE_MEMORY dg g * xR EDX r * 1779 xR EBP jw * ~xS * xPC eip * xCODE (xCODE_SET df f) * X86_STACK (esp,[],1) * 1780 cond (state_inv cs dh h dg g df f jw j /\ t < LENGTH cs /\ 1781 ENCODES_JUMP eip t j bs /\ BYTES_IN_MEM eip df f bs /\ 1782 cont_jump j p cs eip (n2w t))`; 1783 1784val xINC_STOP_def = Define ` 1785 xINC_STOP (xs,l,p,cs:input_type list) (pw,r,esp) = 1786 SEP_EXISTS dh dg df jw g h f. 1787 xR EBX pw * xCODE (codegen_code pw) * ~xR ESI * xR ECX 0w * 1788 xSTACK (xs,l,p,cs) * xMEMORY dh h * xBYTE_MEMORY dg g * xR EDX r * 1789 xR EBP jw * ~xS * xPC r * xCODE (xCODE_SET df f) * X86_STACK (esp,[],1)`; 1790 1791fun QGENL [] th = th 1792 | QGENL (x::xs) th = Q.GEN x (QGENL xs th) 1793 1794fun QEXISTSL_TAC [] = ALL_TAC 1795 | QEXISTSL_TAC (x::xs) = Q.EXISTS_TAC x \\ (QEXISTSL_TAC xs) 1796 1797val xINC_CODEGEN_THM = let 1798 val th = x86_inc_lemma 1799 val (th,goal) = SPEC_WEAKEN_RULE th ``xINC (x::xs,l,n,cs) (ebx,edx,esp)`` 1800 val lemma = prove(goal, 1801 SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_MOVE_COND] 1802 \\ REPEAT STRIP_TAC 1803 \\ IMP_RES_TAC x86_inc_thm 1804 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`ebx`,`edi`,`edx`,`x`]) 1805 \\ FULL_SIMP_TAC std_ss [xINC_def,xSTACK_def,SEP_CLAUSES,STAR_ASSOC] 1806 \\ SIMP_TAC (std_ss++sep_cond_ss) [] 1807 \\ SIMP_TAC std_ss [SEP_IMP_def] 1808 \\ REPEAT STRIP_TAC 1809 \\ FULL_SIMP_TAC std_ss [Q.ISPEC `xR ESI` SEP_HIDE_def,SEP_CLAUSES] 1810 \\ SIMP_TAC std_ss [SEP_EXISTS_THM] 1811 \\ Q.EXISTS_TAC `dh` 1812 \\ Q.EXISTS_TAC `dg` 1813 \\ Q.EXISTS_TAC `df` 1814 \\ Q.EXISTS_TAC `ebp` 1815 \\ Q.EXISTS_TAC `g` 1816 \\ Q.EXISTS_TAC `h3` 1817 \\ Q.EXISTS_TAC `f3` 1818 \\ Q.EXISTS_TAC `j2` 1819 \\ Q.EXISTS_TAC `w` 1820 \\ Q.EXISTS_TAC `edi` 1821 \\ Q.EXISTS_TAC `w` 1822 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1823 \\ FULL_SIMP_TAC (std_ss++star_ss) [] 1824 \\ POP_ASSUM MP_TAC 1825 \\ SIMP_TAC std_ss [STAR_ASSOC] 1826 \\ METIS_TAC []) 1827 val th = MP th lemma 1828 val th = Q.INST [`n`|->`t`] th 1829 val th = QGENL [`w`,`pi`,`j`,`h3`,`h`,`g`,`f3`,`f`,`cp`,`edi`,`ebp`,`dh`,`dg`,`df`] th 1830 val th = SIMP_RULE std_ss [SPEC_PRE_EXISTS] th 1831 val (th,goal) = SPEC_STRENGTHEN_RULE th ``xINC_CODEGEN (x::xs,l,p,cs) (ebx,edx,esp) t`` 1832 val lemma = prove(goal, 1833 SIMP_TAC std_ss [SEP_IMP_def,xINC_CODEGEN_def,SEP_EXISTS_THM] 1834 \\ SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1835 \\ REPEAT STRIP_TAC 1836 \\ FULL_SIMP_TAC std_ss [GSYM iFETCH_NOT_NONE] 1837 \\ IMP_RES_TAC x86_inc_thm 1838 \\ FULL_SIMP_TAC std_ss [xINC_def,SEP_CLAUSES,STAR_ASSOC,xSTACK_def,SEP_EXISTS_THM] 1839 \\ Q.PAT_X_ASSUM `!r6' r3' r2' r1'. ?h2. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`ebx`,`edi`,`edx`,`x`]) 1840 \\ REPEAT (Q.PAT_X_ASSUM `!b. bb` (K ALL_TAC)) 1841 \\ QEXISTSL_TAC [`w`,`p`,`j`,`h2`,`h`,`g`,`f2`,`f`, 1842 `cp`,`edi`,`jw`,`dh`,`dg`,`df`] 1843 \\ ASM_SIMP_TAC std_ss [] 1844 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1845 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 1846 val th = MP th lemma 1847 val lemma = prove( 1848 ``SPEC X86_MODEL (xINC_CODEGEN (xs,l,p,cs) (ebx,edx,esp) t) {} 1849 (xINC (xs,l,t,cs) (ebx,edx,esp))``, 1850 Cases_on `xs` 1851 THEN1 SIMP_TAC std_ss [xINC_CODEGEN_def,xSTACK_def,SEP_CLAUSES,SPEC_FALSE_PRE] 1852 \\ SIMP_TAC std_ss [RW [] (DISCH_ALL th)]) 1853 in lemma end; 1854 1855 1856(* proving that the generated code + the code generator simulate the bytecode *) 1857 1858val fix_jump = let 1859 val lemma1 = EVAL ``(5w:word32) >>> 8`` 1860 val lemma2 = EVAL ``(5w:word32) >>> 16`` 1861 val lemma3 = EVAL ``(5w:word32) >>> 24`` 1862 val lemma4 = EVAL ``(w2w (5w:word32)):word8`` 1863 val lemma5 = EVAL ``(w2w (0w:word32)):word8`` 1864 in SIMP_RULE std_ss [word_arith_lemma1] o 1865 RW [lemma1,lemma2,lemma3,lemma4,lemma5] o Q.INST [`imm32`|->`5w`] end; 1866 1867val je_th = fix_jump je_lemma 1868val je_nop_th = fix_jump je_nop_lemma 1869val jb_th = fix_jump jb_lemma 1870val jb_nop_th = fix_jump jb_nop_lemma; 1871 1872val SPEC_EXISTS_EXISTS = prove( 1873 ``(!x. SPEC m (p x) c (q x)) ==> SPEC m (SEP_EXISTS x. p x) c (SEP_EXISTS x. q x)``, 1874 SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS] \\ REPEAT STRIP_TAC 1875 \\ (MATCH_MP_TAC o GEN_ALL o RW [AND_IMP_INTRO] o DISCH_ALL o 1876 SPEC_ALL o UNDISCH o SPEC_ALL) SPEC_WEAKEN 1877 \\ Q.EXISTS_TAC `q x` 1878 \\ ASM_SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS] 1879 \\ REPEAT STRIP_TAC \\ METIS_TAC []); 1880 1881val iEXEC_IMP = prove( 1882 ``!xs l p cs t. iEXEC (xs,l,p,cs) t ==> ~(iFETCH p cs = NONE)``, 1883 ONCE_REWRITE_TAC [iEXEC_cases] \\ REPEAT STRIP_TAC 1884 \\ FULL_SIMP_TAC std_ss [PAIR_EQ,iSTEP_cases] 1885 \\ NTAC 2 (POP_ASSUM MP_TAC) \\ FULL_SIMP_TAC std_ss []); 1886 1887val state_inv_IMP = prove( 1888 ``(iFETCH p cs = SOME c) /\ 1889 state_inv cs dh h dg g df f jw j /\ (j p = SOME eip) ==> 1890 (~(iFETCH (p + 1) cs = NONE) /\ ~IS_JUMP c ==> 1891 (j (p + 1) = SOME (eip + n2w (INSTR_LENGTH c)))) /\ 1892 ?bs. X86_ENCODE c eip p j bs /\ BYTES_IN_MEM eip df f bs``, 1893 REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [state_inv_def] 1894 THEN1 METIS_TAC [ON_OFF_def] 1895 \\ IMP_RES_TAC CODE_LOOP_UNROLL 1896 \\ POP_ASSUM (STRIP_ASSUME_TAC o SPEC_ALL) 1897 \\ FULL_SIMP_TAC std_ss [CODE_INV_def,INSTR_IN_MEM_def,SEP_CLAUSES] 1898 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 1899 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 1900 \\ Q.EXISTS_TAC `y` \\ ASM_SIMP_TAC std_ss [] 1901 \\ Q.PAT_X_ASSUM `ppp (fun2set (f,df))` MP_TAC 1902 \\ SIMP_TAC std_ss [GSYM STAR_ASSOC] 1903 \\ ONCE_REWRITE_TAC [STAR_COMM] 1904 \\ Q.SPEC_TAC (`q * CODE_SPACE a (SPACE_LENGTH 0 j cs)`,`x`) 1905 \\ Q.SPEC_TAC (`eip`,`a`) 1906 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1907 \\ Induct_on `y` 1908 \\ ASM_SIMP_TAC std_ss [BYTES_IN_MEM_def,SEP_BYTES_IN_MEM_def,STAR_ASSOC] 1909 \\ REPEAT STRIP_TAC \\ RES_TAC \\ ASM_SIMP_TAC std_ss [] 1910 \\ SEP_READ_TAC); 1911 1912val SEP_EXISTS_EQ = prove( 1913 ``(SEP_EXISTS z. p z * cond (x = z)) = p x``, 1914 FULL_SIMP_TAC std_ss [FUN_EQ_THM,SEP_EXISTS,cond_STAR]); 1915 1916val SPEC_POST_EXISTS = prove( 1917 ``!m p c q. (?x. SPEC m p c (q x)) ==> SPEC m p c (SEP_EXISTS x. q x)``, 1918 REPEAT STRIP_TAC 1919 \\ sg `SEP_IMP (q x) (SEP_EXISTS x. q x)` 1920 \\ IMP_RES_TAC SPEC_WEAKEN 1921 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS] \\ METIS_TAC []); 1922 1923val CASES_ON_xs1 = prove( 1924 ``(xs1 = []) \/ ?x xs. (xs1:word32 list) = x::xs``, 1925 Cases_on `xs1` \\ SIMP_TAC std_ss [CONS_11]); 1926 1927val SPEC_COMPOSE_LEMMA = prove( 1928 ``!x p m q. SPEC x p {} m /\ SPEC x m {} q ==> SPEC x p {} q``, 1929 REPEAT STRIP_TAC \\ IMP_RES_TAC SPEC_COMPOSE 1930 \\ FULL_SIMP_TAC std_ss [UNION_IDEMPOT]); 1931 1932val xBYTE_MEMORY_X_FLIP = prove( 1933 ``SPEC X86_MODEL p {(a,xs,T)} q /\ BYTES_IN_MEM a df f xs ==> 1934 SPEC X86_MODEL (p * xCODE (xCODE_SET df f)) {} 1935 (q * xBYTE_MEMORY_X df f)``, 1936 REPEAT STRIP_TAC 1937 \\ (MATCH_MP_TAC o GEN_ALL o RW [AND_IMP_INTRO] o DISCH_ALL o 1938 SPEC_ALL o UNDISCH_ALL o SPEC_ALL) SPEC_WEAKEN 1939 \\ Q.EXISTS_TAC `q * xCODE (xCODE_SET df f)` 1940 \\ SIMP_TAC std_ss [RW1[STAR_COMM] X86_SPEC_CODE] 1941 \\ STRIP_TAC THEN1 (METIS_TAC [SPEC_X86_MODEL_IN_BYTE_MEM]) 1942 \\ MATCH_MP_TAC SEP_IMP_STAR 1943 \\ SIMP_TAC std_ss [SEP_IMP_REFL,xCODE_IMP_BYTE_MEMORY]); 1944 1945val xINC_JUMP_THM = prove( 1946 ``SPEC X86_MODEL (xINC_JUMP (xs,l,p,cs) (v,r,e) t) {} 1947 (xINC (xs,l,t,cs) (v,r,e))``, 1948 SIMP_TAC std_ss [xINC_JUMP_def] 1949 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS] 1950 \\ SIMP_TAC std_ss [SPEC_MOVE_COND] \\ REPEAT STRIP_TAC 1951 \\ REVERSE (FULL_SIMP_TAC std_ss [ENCODES_JUMP_def]) THEN1 1952 (SIMP_TAC std_ss [xINC_def] 1953 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `dh` 1954 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `dg` 1955 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `df` 1956 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `jw` 1957 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `g` 1958 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `h` 1959 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `f` 1960 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `j` 1961 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `w` 1962 \\ Cases_on `xs` \\ SIMP_TAC std_ss [SEP_CLAUSES,SPEC_FALSE_PRE,xSTACK_def] 1963 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ STRIP_TAC 1964 \\ ASM_SIMP_TAC std_ss [STAR_ASSOC,SEP_CLAUSES] 1965 \\ ONCE_REWRITE_TAC [STAR_COMM] 1966 \\ SIMP_TAC std_ss [STAR_ASSOC] 1967 \\ SIMP_TAC std_ss [RW1 [STAR_COMM] X86_SPEC_CODE] 1968 \\ MATCH_MP_TAC (GEN_ALL (RW [AND_IMP_INTRO] SPEC_X86_MODEL_IN_BYTE_MEM)) 1969 \\ Q.EXISTS_TAC `bs` \\ Q.EXISTS_TAC `eip` 1970 \\ ASM_SIMP_TAC std_ss [X86_IMMEDIATE_def,APPEND] 1971 \\ `xPC w = xPC (eip + 5w + (w - eip - 0x5w))` by 1972 (SIMP_TAC std_ss [WORD_ADD_ASSOC] 1973 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 1974 \\ SIMP_TAC std_ss [GSYM WORD_SUB_PLUS,WORD_SUB_ADD]) 1975 \\ Cases_on `ALIGNED edi` 1976 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES,SPEC_FALSE_PRE] 1977 \\ Q.SPEC_TAC (`h'`,`hh`) \\ STRIP_TAC 1978 \\ Q.SPEC_TAC (`t'`,`tt`) \\ STRIP_TAC 1979 \\ SPEC_PROVE_TAC [Q.INST [`imm32`|->`w - eip - 5w`] jmp_lemma]) 1980 \\ MATCH_MP_TAC SPEC_COMPOSE_LEMMA 1981 \\ Q.EXISTS_TAC `xINC_CODEGEN (xs,l,p,cs) (v,r,e) t` 1982 \\ SIMP_TAC std_ss [xINC_CODEGEN_THM] 1983 \\ SIMP_TAC std_ss [xINC_CODEGEN_def] 1984 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `dh` 1985 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `h` 1986 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `dg` 1987 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `g` 1988 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `df` 1989 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `f` 1990 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `jw` 1991 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `j` 1992 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `eip` 1993 \\ `p < LENGTH cs` by 1994 (`~(j p = NONE)` by FULL_SIMP_TAC std_ss [cont_jump_def] 1995 \\ FULL_SIMP_TAC std_ss [state_inv_def] 1996 \\ `~(LENGTH cs <= p)` by METIS_TAC [] \\ DECIDE_TAC) 1997 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES] 1998 \\ ONCE_REWRITE_TAC [STAR_COMM] 1999 \\ SIMP_TAC std_ss [STAR_ASSOC] 2000 \\ MATCH_MP_TAC SPEC_COMPOSE_LEMMA 2001 \\ Q.EXISTS_TAC ` 2002 (X86_STACK (e,[],1) * xR EBX v * xCODE (codegen_code v) * ~xR ESI * 2003 xR ECX (n2w t) * xSTACK (xs,l,p,cs) * xMEMORY dh h * 2004 xBYTE_MEMORY dg g * xR EDX r * xR EBP jw * ~xS * xPC (eip+3w) * 2005 xCODE (xCODE_SET df f))` 2006 \\ REPEAT STRIP_TAC THEN1 2007 (SIMP_TAC std_ss [RW1[STAR_COMM]X86_SPEC_CODE] 2008 \\ MATCH_MP_TAC (GEN_ALL (RW [AND_IMP_INTRO] SPEC_X86_MODEL_IN_BYTE_MEM)) 2009 \\ Q.EXISTS_TAC `[0x83w; 0xF1w; n2w t]` \\ Q.EXISTS_TAC `eip` 2010 \\ Q.PAT_X_ASSUM `BYTES_IN_MEM eip df f bs` MP_TAC 2011 \\ FULL_SIMP_TAC std_ss [BYTES_IN_MEM_def,word_arith_lemma1] 2012 \\ REPEAT STRIP_TAC 2013 \\ `n2w t = (sw2sw ((n2w t):word8)):word32` by 2014 (SIMP_TAC (std_ss++SIZES_ss) [sw2sw_def,bitTheory.SIGN_EXTEND_def, 2015 LET_DEF,w2n_n2w,bitTheory.BIT_def,bitTheory.BITS_THM] 2016 \\ FULL_SIMP_TAC std_ss [state_inv_def] 2017 \\ `t < 128 /\ t < 256` by DECIDE_TAC 2018 \\ FULL_SIMP_TAC std_ss [LESS_DIV_EQ_ZERO]) 2019 \\ ASM_SIMP_TAC std_ss [] \\ SPEC_PROVE_TAC [xor_lemma]) 2020 \\ MATCH_MP_TAC (GEN_ALL xBYTE_MEMORY_X_FLIP) 2021 \\ Q.EXISTS_TAC `[0xFFw; 0xD3w]` \\ Q.EXISTS_TAC `eip+3w` 2022 \\ ASM_SIMP_TAC std_ss [] 2023 \\ Q.PAT_X_ASSUM `BYTES_IN_MEM eip df f bs` MP_TAC 2024 \\ FULL_SIMP_TAC std_ss [BYTES_IN_MEM_def,word_arith_lemma1] 2025 \\ REPEAT STRIP_TAC 2026 \\ SIMP_TAC (bool_ss++sep_cond_ss) [X86_STACK_def,xLIST_def, 2027 ALIGNED,xSPACE_def,SEP_CLAUSES, GSYM (EVAL ``SUC 0``),SPEC_MOVE_COND] 2028 \\ SIMP_TAC std_ss [GSYM SPEC_MOVE_COND] 2029 \\ SPEC_PROVE_TAC [SIMP_RULE std_ss [word_arith_lemma1] 2030 (Q.INST [`eip`|->`eip+3w`,`esp`|->`e`] call_lemma)]); 2031 2032val iSTEP_INIT_TAC = 2033 STRIP_ASSUME_TAC CASES_ON_xs1 2034 THEN1 FULL_SIMP_TAC std_ss [xINC_def,xSTACK_def,SEP_CLAUSES, 2035 SPEC_FALSE_PRE,NOT_NIL_CONS] 2036 \\ ASM_SIMP_TAC std_ss [] 2037 \\ SIMP_TAC std_ss [xINC_def] 2038 \\ NTAC 8 (HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ STRIP_TAC) 2039 \\ SIMP_TAC std_ss [xINC_def,GSYM SPEC_PRE_EXISTS] 2040 \\ SIMP_TAC std_ss [SPEC_MOVE_COND] \\ REPEAT STRIP_TAC 2041 \\ IMP_RES_TAC iEXEC_IMP 2042 \\ IMP_RES_TAC state_inv_IMP 2043 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def,IS_JUMP_def] 2044 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS_EQ,INSTR_LENGTH_def] 2045 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,SEP_CLAUSES] 2046 \\ ONCE_REWRITE_TAC [STAR_COMM] \\ SIMP_TAC std_ss [STAR_ASSOC] 2047 \\ SIMP_TAC std_ss [RW1 [STAR_COMM] X86_SPEC_CODE] 2048 \\ MATCH_MP_TAC (GEN_ALL (RW [AND_IMP_INTRO] SPEC_X86_MODEL_IN_BYTE_MEM)) 2049 \\ Q.EXISTS_TAC `bs` \\ Q.EXISTS_TAC `eip` 2050 \\ Q.PAT_X_ASSUM `bs = xxx` (fn th => FULL_SIMP_TAC std_ss [th]) 2051 \\ REPEAT (Q.PAT_X_ASSUM `yyy = xxx:word8 list` (K ALL_TAC)) 2052 \\ ASM_SIMP_TAC std_ss [] 2053 \\ REPEAT (Q.PAT_X_ASSUM `BYTES_IN_MEM eip df f bss` (K ALL_TAC)) 2054 \\ SIMP_TAC bool_ss [xSTACK_def,SEP_CLAUSES,xLIST_def,xSPACE_def,GSYM ADD1] 2055 \\ SIMP_TAC std_ss [STAR_ASSOC] 2056 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS] \\ STRIP_TAC 2057 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS 2058 \\ SIMP_TAC (std_ss++sep_cond_ss) [SPEC_MOVE_COND,SEP_CLAUSES] 2059 2060val BYTES_IN_MEM_APPEND = prove( 2061 ``!xs ys a. 2062 BYTES_IN_MEM a df f (xs ++ ys) = 2063 BYTES_IN_MEM a df f xs /\ BYTES_IN_MEM (a + n2w (LENGTH xs)) df f ys``, 2064 Induct \\ ASM_SIMP_TAC std_ss [BYTES_IN_MEM_def,LENGTH,APPEND,WORD_ADD_0] 2065 \\ SIMP_TAC std_ss [ADD1,word_arith_lemma1,AC ADD_COMM ADD_ASSOC] 2066 \\ METIS_TAC []); 2067 2068val iSTEP2_TAC = 2069 ASM_SIMP_TAC std_ss [xINC_JUMP_THM] 2070 \\ SIMP_TAC std_ss [xINC_def,xINC_JUMP_def] 2071 \\ NTAC 8 (HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ STRIP_TAC) 2072 \\ SIMP_TAC std_ss [xINC_def,GSYM SPEC_PRE_EXISTS] 2073 \\ SIMP_TAC std_ss [SPEC_MOVE_COND] \\ REPEAT STRIP_TAC 2074 \\ IMP_RES_TAC iEXEC_IMP 2075 \\ IMP_RES_TAC state_inv_IMP 2076 \\ Q.PAT_X_ASSUM `BYTES_IN_MEM eip df f bs` MP_TAC 2077 \\ Q.PAT_X_ASSUM `X86_ENCODE c eip p j bs` MP_TAC 2078 \\ SIMP_TAC std_ss [X86_ENCODE_def] \\ STRIP_TAC 2079 \\ IMP_RES_TAC ENCODE_JUMP_LENGTH 2080 \\ FULL_SIMP_TAC std_ss [BYTES_IN_MEM_APPEND,LENGTH_APPEND,LENGTH,GSYM iFETCH_NOT_NONE] 2081 \\ REPEAT STRIP_TAC 2082 2083val iSTEP3_TAC = 2084 FULL_SIMP_TAC std_ss [n2w_w2n,IS_JUMP_def] 2085 \\ FULL_SIMP_TAC std_ss [cont_jump_def,input_type_11,WORD_ADD_SUB,SEP_CLAUSES] 2086 \\ ONCE_REWRITE_TAC [STAR_COMM] \\ SIMP_TAC std_ss [STAR_ASSOC] 2087 \\ SIMP_TAC std_ss [RW1 [STAR_COMM] X86_SPEC_CODE] 2088 \\ MATCH_MP_TAC (GEN_ALL (RW [AND_IMP_INTRO] SPEC_X86_MODEL_IN_BYTE_MEM)) 2089 2090val iSTEP_xINC = prove( 2091 ``iSTEP (xs1,l,p,cs) (xs2,l2,p2,cs2) /\ iEXEC (xs2,l2,p2,cs2) tt ==> 2092 SPEC X86_MODEL (xINC (xs1,l,p,cs) (v,r,e)) {} (xINC (xs2,l2,p2,cs2) (v,r,e))``, 2093 SIMP_TAC std_ss [iSTEP_cases] \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 2094 \\ POP_ASSUM MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2095 THEN1 2096 (iSTEP_INIT_TAC \\ Q.EXISTS_TAC `edi` 2097 \\ SIMP_TAC std_ss [SEP_CLAUSES] 2098 \\ SIMP_TAC std_ss [GSYM SPEC_MOVE_COND] 2099 \\ SPEC_PROVE_TAC [sub_lemma]) 2100 THEN1 2101 (iSTEP_INIT_TAC \\ Q.EXISTS_TAC `edi` 2102 \\ SIMP_TAC std_ss [SEP_CLAUSES] 2103 \\ SIMP_TAC std_ss [GSYM SPEC_MOVE_COND] 2104 \\ SPEC_PROVE_TAC [swap_lemma]) 2105 THEN1 2106 (iSTEP_INIT_TAC \\ Q.EXISTS_TAC `edi + 4w` 2107 \\ SIMP_TAC std_ss [SEP_CLAUSES,ALIGNED] 2108 \\ SIMP_TAC std_ss [GSYM SPEC_MOVE_COND,WORD_ADD_SUB] 2109 \\ SPEC_PROVE_TAC [pop_lemma]) 2110 THEN1 2111 (iSTEP_INIT_TAC \\ Q.EXISTS_TAC `edi - 4w` 2112 \\ SIMP_TAC std_ss [SEP_CLAUSES,ALIGNED] 2113 \\ SIMP_TAC std_ss [GSYM SPEC_MOVE_COND,WORD_SUB_ADD] 2114 \\ SPEC_PROVE_TAC [push_lemma]) 2115 THEN1 2116 (MATCH_MP_TAC SPEC_COMPOSE_LEMMA 2117 \\ Q.EXISTS_TAC `xINC_JUMP (xs1,l,p,cs) (v,r,e) (w2n w)` 2118 \\ SIMP_TAC std_ss [xINC_JUMP_THM] 2119 \\ SIMP_TAC std_ss [xINC_def,xINC_JUMP_def] 2120 \\ NTAC 8 (HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ STRIP_TAC) 2121 \\ SIMP_TAC std_ss [xINC_def,GSYM SPEC_PRE_EXISTS] 2122 \\ SIMP_TAC std_ss [SPEC_MOVE_COND] \\ REPEAT STRIP_TAC 2123 \\ IMP_RES_TAC iEXEC_IMP 2124 \\ IMP_RES_TAC state_inv_IMP 2125 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `eip` 2126 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `bs` 2127 \\ `cont_jump j p cs eip w` by METIS_TAC [cont_jump_def] 2128 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def,n2w_w2n, 2129 GSYM iFETCH_NOT_NONE,SEP_CLAUSES,SPEC_REFL]) 2130 THEN1 2131 (MATCH_MP_TAC SPEC_COMPOSE_LEMMA 2132 \\ Q.EXISTS_TAC `xINC_JUMP (xs1,l,p,cs) (v,r,e) (w2n w)` 2133 \\ iSTEP2_TAC 2134 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `eip+13w` 2135 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `bs2` 2136 \\ iSTEP3_TAC 2137 \\ Q.EXISTS_TAC `[0x3Bw; 0x7w; 0xFw; 0x84w; 0x5w; 0x0w; 0x0w; 0x0w]` \\ Q.EXISTS_TAC `eip` 2138 \\ ASM_SIMP_TAC std_ss [xSTACK_def,SEP_CLAUSES,STAR_ASSOC,xLIST_def] 2139 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ STRIP_TAC 2140 \\ SIMP_TAC (std_ss++sep_cond_ss) [SPEC_MOVE_COND,SEP_CLAUSES] 2141 \\ SIMP_TAC std_ss [GSYM SPEC_MOVE_COND] 2142 \\ SPEC_PROVE_TAC [je_th]) 2143 THEN1 2144 (MATCH_MP_TAC SPEC_COMPOSE_LEMMA 2145 \\ Q.EXISTS_TAC `xINC_JUMP (xs1,l,p,cs) (v,r,e) (p + 1)` 2146 \\ iSTEP2_TAC 2147 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `eip+8w` 2148 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `bs1` 2149 \\ `w2n ((n2w (p + 1)):word7) = p + 1` by 2150 (FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,state_inv_def] \\ DECIDE_TAC) 2151 \\ iSTEP3_TAC 2152 \\ Q.EXISTS_TAC `[0x3Bw; 0x7w; 0xFw; 0x84w; 0x5w; 0x0w; 0x0w; 0x0w]` \\ Q.EXISTS_TAC `eip` 2153 \\ ASM_SIMP_TAC std_ss [xSTACK_def,SEP_CLAUSES,STAR_ASSOC,xLIST_def] 2154 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ STRIP_TAC 2155 \\ Q.PAT_X_ASSUM `x <> y` MP_TAC 2156 \\ SIMP_TAC (std_ss++sep_cond_ss) [SPEC_MOVE_COND,SEP_CLAUSES] 2157 \\ SIMP_TAC (std_ss++sep_cond_ss) [GSYM SPEC_MOVE_COND] 2158 \\ SPEC_PROVE_TAC [je_nop_th]) 2159 THEN1 2160 (MATCH_MP_TAC SPEC_COMPOSE_LEMMA 2161 \\ Q.EXISTS_TAC `xINC_JUMP (xs1,l,p,cs) (v,r,e) (w2n w)` 2162 \\ iSTEP2_TAC 2163 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `eip+13w` 2164 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `bs2` 2165 \\ iSTEP3_TAC 2166 \\ Q.EXISTS_TAC `[0x3Bw; 0x7w; 0xFw; 0x82w; 0x5w; 0x0w; 0x0w; 0x0w]` \\ Q.EXISTS_TAC `eip` 2167 \\ ASM_SIMP_TAC std_ss [xSTACK_def,SEP_CLAUSES,STAR_ASSOC,xLIST_def] 2168 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ STRIP_TAC 2169 \\ Q.PAT_X_ASSUM `x <+ y` MP_TAC 2170 \\ SIMP_TAC (std_ss++sep_cond_ss) [SPEC_MOVE_COND,SEP_CLAUSES] 2171 \\ SIMP_TAC std_ss [GSYM SPEC_MOVE_COND] 2172 \\ SPEC_PROVE_TAC [jb_th]) 2173 THEN1 2174 (MATCH_MP_TAC SPEC_COMPOSE_LEMMA 2175 \\ Q.EXISTS_TAC `xINC_JUMP (xs1,l,p,cs) (v,r,e) (p + 1)` 2176 \\ iSTEP2_TAC 2177 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `eip+8w` 2178 \\ HO_MATCH_MP_TAC SPEC_POST_EXISTS \\ Q.EXISTS_TAC `bs1` 2179 \\ `w2n ((n2w (p + 1)):word7) = p + 1` by 2180 (FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,state_inv_def] \\ DECIDE_TAC) 2181 \\ iSTEP3_TAC 2182 \\ Q.EXISTS_TAC `[0x3Bw; 0x7w; 0xFw; 0x82w; 0x5w; 0x0w; 0x0w; 0x0w]` \\ Q.EXISTS_TAC `eip` 2183 \\ ASM_SIMP_TAC std_ss [xSTACK_def,SEP_CLAUSES,STAR_ASSOC,xLIST_def] 2184 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ STRIP_TAC 2185 \\ Q.PAT_X_ASSUM `~(x <+ y)` MP_TAC 2186 \\ SIMP_TAC (std_ss++sep_cond_ss) [SPEC_MOVE_COND,SEP_CLAUSES] 2187 \\ SIMP_TAC std_ss [GSYM SPEC_MOVE_COND] 2188 \\ SPEC_PROVE_TAC [jb_nop_th])); 2189 2190val iEXEC_IMP = prove( 2191 ``!xs l p cs t. iEXEC (xs,l,p,cs) t ==> ?i2. iFETCH p cs = SOME i2``, 2192 ONCE_REWRITE_TAC [iEXEC_cases] \\ REPEAT STRIP_TAC 2193 \\ FULL_SIMP_TAC std_ss [PAIR_EQ,iSTEP_cases]); 2194 2195val sinduction = IndDefLib.derive_strong_induction(iEXEC_rules,iEXEC_ind); 2196 2197val iEXEC_xINC = prove( 2198 ``!s t. iEXEC s t ==> 2199 SPEC X86_MODEL (xINC s (v,r,e)) {} (xINC_STOP t (v,r,e))``, 2200 HO_MATCH_MP_TAC sinduction \\ REVERSE (REPEAT STRIP_TAC) THEN1 2201 (MATCH_MP_TAC SPEC_COMPOSE_LEMMA 2202 \\ Q.EXISTS_TAC `xINC s' (v,r,e)` 2203 \\ `?xs l p cs. s = (xs,l,p,cs)` by METIS_TAC [PAIR] 2204 \\ `?xs2 l2 p2 cs2. s' = (xs2,l2,p2,cs2)` by METIS_TAC [PAIR] 2205 \\ FULL_SIMP_TAC std_ss [] 2206 \\ IMP_RES_TAC iSTEP_xINC 2207 \\ FULL_SIMP_TAC std_ss []) 2208 \\ SIMP_TAC std_ss [xINC_STOP_def,xINC_def,SEP_CLAUSES] 2209 \\ NTAC 7 (HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ STRIP_TAC) 2210 \\ SIMP_TAC (std_ss++sep_cond_ss) [SPEC_MOVE_COND,GSYM SPEC_PRE_EXISTS] 2211 \\ REPEAT STRIP_TAC 2212 \\ IMP_RES_TAC state_inv_IMP 2213 \\ FULL_SIMP_TAC std_ss [IS_JUMP_def] 2214 \\ Q.PAT_X_ASSUM `BYTES_IN_MEM eip df f bs` MP_TAC 2215 \\ Q.PAT_X_ASSUM `X86_ENCODE iSTOP eip p j bs` MP_TAC 2216 \\ FULL_SIMP_TAC std_ss [X86_ENCODE_def] 2217 \\ REPEAT STRIP_TAC 2218 \\ ONCE_REWRITE_TAC [STAR_COMM] \\ SIMP_TAC std_ss [STAR_ASSOC] 2219 \\ SIMP_TAC std_ss [RW1[STAR_COMM]X86_SPEC_CODE] 2220 \\ MATCH_MP_TAC (GEN_ALL (RW [AND_IMP_INTRO] SPEC_X86_MODEL_IN_BYTE_MEM)) 2221 \\ Q.EXISTS_TAC `bs` \\ Q.EXISTS_TAC `eip` \\ ASM_SIMP_TAC std_ss [] 2222 \\ SPEC_PROVE_TAC [jmp_edx_lemma]); 2223 2224val xINC_CODEGEN_STOP_THM = prove( 2225 ``SPEC X86_MODEL 2226 (xINC_CODEGEN (xs,l,p,cs) (v,r,e) t * cond (iEXEC (xs,l,t,cs) s)) {} 2227 (xINC_STOP s (v,r,e))``, 2228 SIMP_TAC std_ss [SPEC_MOVE_COND] \\ REPEAT STRIP_TAC 2229 \\ MATCH_MP_TAC SPEC_COMPOSE_LEMMA 2230 \\ Q.EXISTS_TAC `xINC (xs,l,t,cs) (v,r,e)` 2231 \\ ASM_SIMP_TAC std_ss [iEXEC_xINC,xINC_CODEGEN_THM]); 2232 2233val SEP_IMP_PRE_EXISTS = prove( 2234 ``SEP_IMP (SEP_EXISTS x. p x) q = !x. SEP_IMP (p x) q``, 2235 SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] \\ METIS_TAC []); 2236 2237val SEP_IMP_xINC_STOP = prove( 2238 ``SEP_IMP (xINC_STOP s (v,r,e)) 2239 (xSTACK s * X86_STACK (e,[],1) * 2240 xPC r * SEP_T * xCODE (codegen_code v))``, 2241 NTAC 2 (ONCE_REWRITE_TAC [STAR_COMM] \\ SIMP_TAC std_ss [STAR_ASSOC]) 2242 \\ `?xs l p cs. s = (xs,l,p,cs)` by METIS_TAC [PAIR] 2243 \\ FULL_SIMP_TAC std_ss [] 2244 \\ `xINC_STOP (xs,l,p,cs) (v,r,e) = 2245 SEP_EXISTS dh dg df jw g h f. 2246 xR EBX v * ~xR ESI * xR ECX 0x0w * 2247 xMEMORY dh h * xBYTE_MEMORY dg g * 2248 xR EDX r * xR EBP jw * ~xS * xCODE (xCODE_SET df f) * 2249 xCODE (codegen_code v) * xSTACK (xs,l,p,cs) * X86_STACK (e,[],1) * xPC r` by (SIMP_TAC (std_ss++star_ss) [xINC_STOP_def]) 2250 \\ ASM_SIMP_TAC std_ss [SEP_IMP_PRE_EXISTS] 2251 \\ REPEAT STRIP_TAC 2252 \\ REPEAT (MATCH_MP_TAC SEP_IMP_STAR \\ SIMP_TAC std_ss [SEP_IMP_REFL]) 2253 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_T_def]); 2254 2255val xINC_SETUP_def = Define ` 2256 xINC_SETUP cs = 2257 SEP_EXISTS dh h dg g df f jw. 2258 xBYTE_MEMORY_X df f * xMEMORY dh h * xBYTE_MEMORY dg g * xR EBP jw * 2259 cond (state_inv cs dh h dg g df f jw (\x.NONE) /\ ~(h (jw - 0x24w) = 0x0w))`; 2260 2261val PRE_LEMMA = prove( 2262 ``SEP_IMP (SEP_EXISTS cp. 2263 xINC_SETUP cs * xR EBX pw * ~xR ESI * xR ECX 0w * 2264 xSTACK (xs,l,0,cs) * xR EDX r * xPC pw * ~xS * 2265 X86_STACK (esp - 0x4w,[cp],0) * cond (iEXEC (xs,l,0,cs) s) * 2266 xCODE (codegen_code pw)) 2267 (xINC_CODEGEN (xs,l,0,cs) (pw,r,esp) 0 * cond (iEXEC (xs,l,0,cs) s))``, 2268 SIMP_TAC std_ss [xINC_CODEGEN_def,xINC_SETUP_def,SEP_CLAUSES] 2269 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_def,SEP_EXISTS_THM,cond_STAR] 2270 \\ REPEAT STRIP_TAC 2271 \\ QEXISTSL_TAC [`dh`,`h`,`dg`,`g`,`df`,`f`,`jw`,`\x.NONE`,`cp-5w`] 2272 \\ FULL_SIMP_TAC (std_ss++star_ss) [WORD_SUB_ADD] 2273 \\ IMP_RES_TAC iEXEC_IMP 2274 \\ Cases_on `cs` \\ FULL_SIMP_TAC std_ss [iFETCH_def,LENGTH]) 2275 2276val code_generator_length = let 2277 val tms = list_dest pred_setSyntax.dest_insert ((cdr o concl o SPEC_ALL) codege_code_def) 2278 val (x,y) = (dest_pair o last o butlast) tms 2279 val x = Arbnum.toInt (numSyntax.dest_numeral (cdr (cdr x))) 2280 val i = (length o fst o listSyntax.dest_list o fst o dest_pair) y 2281 in x + i end 2282 2283val assign_eip_to_ebx = let 2284 val (spec,_,s,_) = prog_x86Lib.x86_tools 2285 val ((th1,_,_),_) = spec (x86_encode "call 0") 2286 val ((th2,_,_),_) = spec (x86_encode "mov ebx,[esp]") 2287 val ((th3,_,_),_) = spec (x86_encode "add ebx,12") 2288 val th = HIDE_STATUS_RULE true s (SPEC_COMPOSE_RULE [th1,th2,th3]) 2289 val th = RW [STAR_ASSOC,combinTheory.APPLY_UPDATE_THM,WORD_ADD_0] th 2290 val th = SIMP_RULE (bool_ss++sep_cond_ss) [SPEC_MOVE_COND,ALIGNED_INTRO] th 2291 val th = Q.INST [`df`|->`{esp-4w}`] (DISCH_ALL th) 2292 val th = INST [``f:word32->word32``|->``\x:word32.(w:word32)``] (DISCH_ALL th) 2293 val th = SIMP_RULE std_ss [IN_INSERT,NOT_IN_EMPTY,xM_THM,ALIGNED,WORD_ADD_0] th 2294 val th = SIMP_RULE bool_ss [GSYM SPEC_MOVE_COND,x86_astTheory.Xrm_distinct] th 2295 val th = SIMP_RULE std_ss [word_arith_lemma1] th 2296 val th = HIDE_PRE_RULE ``xM (esp - 4w)`` th 2297 val th = SPEC_BOOL_FRAME_RULE th ``ALIGNED esp`` 2298 val (th,goal) = SPEC_WEAKEN_RULE th ``xR EBX (eip + 0x11w) * 2299 xPC (eip + 0xBw) * ~xS * X86_STACK (esp-4w,[eip+5w],0)`` 2300 val lemma = prove(goal, 2301 SIMP_TAC (std_ss++star_ss) [X86_STACK_def,xSPACE_def,xLIST_def, 2302 SEP_CLAUSES,ALIGNED,SEP_IMP_REFL]) 2303 val th = MP th lemma 2304 val th = HIDE_PRE_RULE ``xR EBX`` th 2305 val (th,goal) = SPEC_STRENGTHEN_RULE th ``~xR EBX * 2306 xPC eip * ~xS * X86_STACK (esp,[],1)`` 2307 val lemma = prove(goal, 2308 SIMP_TAC (bool_ss++sep_cond_ss) [X86_STACK_def,xSPACE_def,xLIST_def, 2309 SEP_CLAUSES,ALIGNED,SEP_IMP_REFL,GSYM (EVAL ``SUC 0``)] 2310 \\ SIMP_TAC (std_ss++star_ss) [SEP_IMP_REFL]) 2311 val th = MP th lemma 2312 val s = int_to_string (code_generator_length) 2313 val ((th0,_,_),_) = spec (x86_encode "mov ecx,0") 2314 val ((th4,_,_),_) = spec (x86_encode ("lea edx,[ebx+"^s^"]")) 2315 val th = SPEC_COMPOSE_RULE [th0,th,th4] 2316 val th = SIMP_RULE std_ss [STAR_ASSOC] th 2317 val th = HIDE_PRE_RULE ``xR EDX`` th 2318 val th = HIDE_PRE_RULE ``xR ECX`` th 2319 val th = RW [] (DISCH_ALL th) 2320 in th end; 2321 2322val xINC_SETUP_THM = let 2323 val th = MATCH_MP (MATCH_MP SPEC_WEAKEN xINC_CODEGEN_STOP_THM) SEP_IMP_xINC_STOP 2324 val th = MATCH_MP (MATCH_MP SPEC_STRENGTHEN th) PRE_LEMMA 2325 val th = SPEC_ALL (SIMP_RULE std_ss [GSYM SPEC_PRE_EXISTS] th) 2326 val th = RW [RW1 [STAR_COMM] X86_SPEC_CODE] th 2327 val th = SPEC_COMPOSE_RULE [assign_eip_to_ebx,th] 2328 val th = SIMP_RULE std_ss [STAR_ASSOC,word_arith_lemma1] th 2329 in th end; 2330 2331val _ = Parse.hide "zero_loop"; 2332val (th1,zero_loop_def,zero_loop_pre_def) = compile "x86" `` 2333 zero_loop (r5:word32,r2:word32,r4:word32,dh:word32 set,h:word32->word32) = 2334 if r4 = 0w then (dh,h) else 2335 let h = (r2 =+ r5) h in 2336 let r2 = r2 + 4w in 2337 let r4 = r4 - 1w in 2338 zero_loop (r5,r2,r4,dh,h)``; 2339 2340val _ = Parse.hide "x86_inc_init"; 2341val (x86_inc_init_th,x86_inc_init_def,x86_inc_init_pre_def) = compile "x86" `` 2342 x86_inc_init (r2:word32,r4:word32,r7:word32,dh:word32 set,h:word32->word32) = 2343 let r5 = 1w:word32 in 2344 let h = (r7 =+ r5) h in 2345 let r7 = r7 + 36w in 2346 let h = (r7 - 4w =+ r2) h in 2347 let h = (r7 - 8w =+ r4) h in 2348 let r5 = 0w:word32 in 2349 let r2 = r7 in 2350 let r4 = 256w in 2351 let (dh,h) = zero_loop (r5,r2,r4,dh,h) in 2352 (r7,dh,h)`` 2353 2354val TEMP_SPACE_def = Define ` 2355 (TEMP_SPACE a 0 = emp) /\ 2356 (TEMP_SPACE a (SUC n) = SEP_EXISTS w. one (a:word32,w:word32) * TEMP_SPACE (a+4w) n)`; 2357 2358val zero_loop_thm = prove( 2359 ``!n h dh r2 p. 2360 n < 1000 /\ ALIGNED r2 ==> 2361 (p * TEMP_SPACE r2 (2 * n)) (fun2set (h,dh)) ==> 2362 ?h2. zero_loop_pre (0w,r2,n2w (2 * n),dh,h) /\ 2363 (zero_loop (0w,r2,n2w (2 * n),dh,h) = (dh,h2)) /\ 2364 !k xs. (LENGTH (xs:input_type list) = n) ==> (p * MAP_INV r2 k (\x.NONE) xs) (fun2set (h2,dh))``, 2365 Induct THEN1 2366 (SIMP_TAC std_ss [] 2367 \\ ONCE_REWRITE_TAC [zero_loop_def,zero_loop_pre_def] 2368 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ Cases_on `xs` 2369 \\ FULL_SIMP_TAC std_ss [LENGTH,MAP_INV_def,TEMP_SPACE_def] 2370 \\ `F` by DECIDE_TAC) 2371 THEN1 2372 (SIMP_TAC std_ss [TEMP_SPACE_def,STAR_ASSOC,TIMES2,ADD, 2373 ADD_CLAUSES,SEP_CLAUSES,SEP_EXISTS_THM,word_arith_lemma1] 2374 \\ REPEAT STRIP_TAC 2375 \\ ONCE_REWRITE_TAC [zero_loop_def,zero_loop_pre_def] 2376 \\ ONCE_REWRITE_TAC [zero_loop_def,zero_loop_pre_def] 2377 \\ SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,n2w_11,ADD1,GSYM word_add_n2w,WORD_ADD_SUB] 2378 \\ `(n + n + 1) < 4294967296 /\ (n + n + 1 + 1) < 4294967296` by DECIDE_TAC 2379 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,n2w_11,ADD1,word_add_n2w] 2380 \\ `n < 1000` by DECIDE_TAC 2381 \\ FULL_SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED,word_arith_lemma1] 2382 \\ `(p * one (r2,0w) * one (r2 + 0x4w,0w) * TEMP_SPACE (r2 + 0x8w) (n + n)) 2383 (fun2set ((r2 + 0x4w =+ 0x0w) ((r2 =+ 0x0w) h),dh))` by SEP_WRITE_TAC 2384 \\ POP_ASSUM MP_TAC 2385 \\ Q.PAT_X_ASSUM `bbb (fun2set (h,dh))` (K ALL_TAC) 2386 \\ REPEAT STRIP_TAC 2387 \\ `ALIGNED (r2 + 8w)` by FULL_SIMP_TAC std_ss [ALIGNED] 2388 \\ FULL_SIMP_TAC std_ss [TIMES2] 2389 \\ RES_TAC \\ Q.PAT_X_ASSUM `!p q x. bb` (K ALL_TAC) 2390 \\ ASM_SIMP_TAC std_ss [] 2391 \\ REPEAT STRIP_TAC THEN1 SEP_READ_TAC THEN1 SEP_READ_TAC 2392 \\ Cases_on `xs` 2393 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,MAP_INV_def,MAP_ROW_def,STAR_ASSOC])) 2394 2395val LENGTH_EXISTS = prove( 2396 ``!n. ?xs. LENGTH xs = n``, 2397 Induct THEN1 (Q.EXISTS_TAC `[]` \\ ASM_SIMP_TAC std_ss [LENGTH]) 2398 \\ FULL_SIMP_TAC std_ss [] 2399 \\ Q.EXISTS_TAC `ARB::xs` \\ ASM_SIMP_TAC std_ss [LENGTH]) 2400 2401val LENGTH_EXTEND = prove( 2402 ``!n xs. LENGTH xs < n ==> ?ys. LENGTH (xs ++ ys) = n``, 2403 REPEAT STRIP_TAC 2404 \\ `?m. n = LENGTH xs + m` by (Q.EXISTS_TAC `n - LENGTH xs` \\ DECIDE_TAC) 2405 \\ ASM_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH_EXISTS]); 2406 2407val CODE_LOOP_NONE = prove( 2408 ``!cs k. CODE_LOOP k (\x. NONE) cs = emp``, 2409 Induct \\ ASM_SIMP_TAC std_ss [CODE_LOOP_def,INSTR_IN_MEM_def,SEP_CLAUSES]); 2410 2411val SPACE_LENGTH_NONE = prove( 2412 ``!cs k. SPACE_LENGTH k (\x. NONE) cs = SUM (MAP INSTR_LENGTH cs)``, 2413 Induct \\ ASM_SIMP_TAC std_ss [SPACE_LENGTH_def,MAP,listTheory.SUM]); 2414 2415(* CLEAN *) 2416 2417fun RENAME_ALPHA_CONV tm = let 2418 val (v,t) = dest_abs tm 2419 val (name,ty) = dest_var v 2420 val cs = rev (explode name) 2421 fun primes ((#"'")::cs,n) = primes (cs,n+1) 2422 | primes (cs,n) = (cs,n) 2423 val (cs,n) = primes (cs,0) 2424 val _ = if n = 0 then fail() else n 2425 val vs = map (fst o dest_var) (all_vars tm) 2426 val v_name = implode cs 2427 fun find_name m = let 2428 val new_name = v_name ^ int_to_string m 2429 in if mem new_name vs then find_name (m+1) else new_name end 2430 val new_v = mk_var(find_name n,ty) 2431 in ALPHA_CONV new_v tm end handle HOL_ERR _ => NO_CONV tm 2432 2433val CLEAN_CONV = DEPTH_CONV RENAME_ALPHA_CONV 2434 2435fun SPEC_ALL_TAC (hs,goal) = 2436 (foldr (fn (v,t) => SPEC_TAC (v,v) THEN t) ALL_TAC (free_vars goal)) (hs,goal) 2437 2438val CLEAN_TAC = 2439 ONCE_REWRITE_TAC [GSYM markerTheory.Abbrev_def] 2440 THEN REPEAT (POP_ASSUM MP_TAC) 2441 THEN SPEC_ALL_TAC 2442 THEN CONV_TAC CLEAN_CONV 2443 THEN REPEAT STRIP_TAC 2444 THEN PURE_ONCE_REWRITE_TAC [markerTheory.Abbrev_def] 2445 2446(* / CLEAN *) 2447 2448val MAP_INV_APPEND = prove( 2449 ``!xs ys a k. 2450 MAP_INV a k (\x. NONE) (xs++ys) = 2451 MAP_INV a k (\x. NONE) xs * MAP_INV (a + n2w (8 * LENGTH xs)) (k + LENGTH xs) (\x. NONE) ys``, 2452 Induct 2453 \\ ASM_SIMP_TAC std_ss [MAP_INV_def,SEP_CLAUSES,APPEND,LENGTH, 2454 WORD_ADD_0,MAP_ROW_def,STAR_ASSOC,MULT_CLAUSES,word_arith_lemma1] 2455 \\ SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM,ADD1]) 2456 2457val SEP_IMP_INTRO = prove( 2458 ``!p q x. SEP_IMP p q ==> (p x ==> q x)``,METIS_TAC [SEP_IMP_def]); 2459 2460val xINC_SETUP_INTRO = prove( 2461 ``one_string_0 r3 (iENCODE cs) b1 (fun2set (g,dg)) /\ ALIGNED r5 /\ 2462 (TEMP_SPACE r5 265) (fun2set (h,dh)) /\ LENGTH cs < 128 /\ 2463 (CODE_SPACE r4 (SUM (MAP INSTR_LENGTH cs))) (fun2set (f,df)) ==> 2464 ?r4i h2. x86_inc_init_pre (r3,r4,r5,dh,h) /\ 2465 (x86_inc_init (r3,r4,r5,dh,h) = (r4i,dh,h2)) /\ 2466 state_inv cs dh h2 dg g df f r4i (\x.NONE) /\ 2467 h2 (r4i - 0x24w) <> 0x0w``, 2468 ONCE_REWRITE_TAC [x86_inc_init_def,x86_inc_init_pre_def] 2469 \\ SIMP_TAC std_ss [LET_DEF,ALIGNED_INTRO,ALIGNED,word_arith_lemma4] 2470 \\ REWRITE_TAC [GSYM (EVAL ``SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (256)))))))))``)] 2471 \\ REWRITE_TAC [TEMP_SPACE_def] 2472 \\ SIMP_TAC std_ss [SEP_CLAUSES,word_arith_lemma1,STAR_ASSOC,SEP_EXISTS_THM] 2473 \\ REPEAT STRIP_TAC 2474 \\ Q.ABBREV_TAC `hi = (r5 + 0x1Cw =+ r4) ((r5 + 0x20w =+ r3) ((r5 =+ 0x1w) h))` 2475 \\ `(one (r5,1w) * one (r5 + 0x4w,w') * one (r5 + 0x8w,w'') * 2476 one (r5 + 0xCw,w''') * one (r5 + 0x10w,w'''') * 2477 one (r5 + 0x14w,w''''') * one (r5 + 0x18w,w'''''') * 2478 one (r5 + 0x1Cw,r4) * one (r5 + 0x20w,r3) * 2479 TEMP_SPACE (r5 + 0x24w) 256) (fun2set (hi,dh))` by 2480 (Q.UNABBREV_TAC `hi` \\ SEP_WRITE_TAC) 2481 \\ Q.PAT_X_ASSUM `bbbb (fun2set (h,dh))` (K ALL_TAC) 2482 \\ `ALIGNED (r5 + 0x24w)` by ASM_SIMP_TAC std_ss [ALIGNED] 2483 \\ Q.PAT_X_ASSUM `ALIGNED r5` (K ALL_TAC) 2484 \\ IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPEC `128` zero_loop_thm)) 2485 \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `0`) 2486 \\ ASM_SIMP_TAC std_ss [word_arith_lemma4,WORD_ADD_0] 2487 \\ IMP_RES_TAC LENGTH_EXTEND 2488 \\ Q.PAT_X_ASSUM `!xs. bb` IMP_RES_TAC 2489 \\ `h2 r5 = 1w` by SEP_READ_TAC 2490 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 2491 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC THEN1 SEP_READ_TAC 2492 \\ FULL_SIMP_TAC std_ss [state_inv_def,ALIGNED,ON_OFF_def] 2493 \\ Q.EXISTS_TAC `r4` 2494 \\ Q.EXISTS_TAC `r3` 2495 \\ Q.EXISTS_TAC `b1` 2496 \\ ASM_SIMP_TAC std_ss [CODE_INV_def,CODE_LOOP_NONE, 2497 SPACE_LENGTH_NONE,SEP_CLAUSES] 2498 \\ ASM_SIMP_TAC std_ss [MAP_TEMP_INV_def,TEMP_INV_UNROLL,word_arith_lemma1, 2499 word_arith_lemma2,word_arith_lemma3,word_arith_lemma4,SEP_EXISTS_THM, 2500 SEP_CLAUSES,STAR_ASSOC,TEMP_INV_def] 2501 \\ CLEAN_TAC \\ QEXISTSL_TAC [`w6`,`w5`,`w4`,`w3`,`w2`,`w1`,`1w`] 2502 \\ FULL_SIMP_TAC std_ss [MAP_INV_APPEND,STAR_ASSOC] 2503 \\ POP_ASSUM (K ALL_TAC) 2504 \\ POP_ASSUM MP_TAC 2505 \\ MATCH_MP_TAC SEP_IMP_INTRO 2506 \\ MATCH_MP_TAC SEP_IMP_STAR 2507 \\ REVERSE STRIP_TAC THEN1 (SIMP_TAC std_ss [SEP_T_def,SEP_IMP_def]) 2508 \\ SIMP_TAC (std_ss++star_ss) [SEP_IMP_REFL,WORD_ADD_0]); 2509 2510val xINC_INIT_THM = let 2511 val imp = MATCH_INST xINC_SETUP_INTRO ``x86_inc_init (edx,esi,ebp,dh,h)`` 2512 val tm = (fst o dest_imp o concl) imp 2513 val th = x86_inc_init_th 2514 val th = SPEC_FRAME_RULE th ``xBYTE_MEMORY_X df f * xBYTE_MEMORY dg g`` 2515 val th = SPEC_BOOL_FRAME_RULE th tm 2516 val p = cdr (find_term (can (match_term ``xPC (p + n2w n)``)) (concl th)) 2517 val (th,goal) = SPEC_WEAKEN_RULE th (subst [``p:word32``|->p] ``xINC_SETUP cs * ~xR ECX * 2518 ~xR EDX * ~xR ESI * xPC p * ~xS``) 2519 val lemma = prove(goal, 2520 SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_MOVE_COND] \\ REPEAT STRIP_TAC 2521 \\ STRIP_ASSUME_TAC (UNDISCH_ALL (RW [GSYM AND_IMP_INTRO] imp)) 2522 \\ ASM_SIMP_TAC std_ss [LET_DEF,xINC_SETUP_def,SEP_CLAUSES] 2523 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] \\ REPEAT STRIP_TAC 2524 \\ QEXISTSL_TAC [`dh`,`h2`,`dg`,`g`,`df`,`f`,`r4i`] 2525 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES] 2526 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 2527 val th = MP th lemma 2528 val th = SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND,AND_IMP_INTRO] th 2529 val tm2 = (fst o dest_imp o concl) th 2530 val goal = mk_imp(tm,tm2) 2531 val lemma = prove(goal,ASM_SIMP_TAC std_ss [] \\ METIS_TAC [imp]) 2532 val th = RW [GSYM SPEC_MOVE_COND] (DISCH_ALL (MP th (UNDISCH lemma))) 2533 in th end; 2534 2535val x86_incremental_jit = let 2536 val th = SPEC_COMPOSE_RULE [xINC_INIT_THM,xINC_SETUP_THM] 2537 val th = SIMP_RULE (std_ss++sep_cond_ss) [SEP_CLAUSES,STAR_ASSOC] (DISCH_ALL th) 2538 val th = SIMP_RULE std_ss [codege_code_def,word_arith_lemma1] th 2539 in save_thm("x86_incremental_jit",th) end; 2540 2541val _ = write_code_to_file "incremental-jit.s" x86_incremental_jit; 2542 2543val _ = export_theory(); 2544