1 2open HolKernel Parse boolLib bossLib; 3 4val _ = new_theory "prog_x64_extra"; 5 6open prog_x64Theory prog_x64Lib x64_encodeLib; 7open helperLib progTheory set_sepTheory addressTheory temporalTheory; 8 9open wordsTheory wordsLib listTheory arithmeticTheory; 10open whileTheory pairTheory relationTheory combinTheory optionTheory; 11 12infix \\ val op \\ = op THEN; 13 14(* generic code gen infrastructure *) 15 16val zCODE_HEAP_RAX_def = Define ` 17 zCODE_HEAP_RAX b a n code = 18 zCODE_HEAP b a code n * zR 0w (a + n2w (LENGTH code))`; 19 20val SNOC_R1 = let 21 val (_,_,sts,_) = x64_tools 22 val ((th1,_,_),_) = x64_spec (x64_encode "mov [r0],r1b") 23 val ((th2,_,_),_) = x64_spec (x64_encode "inc r0") 24 val th1 = th1 |> REWRITE_RULE [SIGN_EXTEND_IGNORE,n2w_w2n, 25 GSYM zBYTE_MEMORY_Z_def,zBYTE_MEMORY_def] 26 |> Q.GEN `g` |> Q.GEN `dg` 27 |> Q.INST [`r0`|->`a+n2w (LENGTH (code:word8 list))`] 28 |> MATCH_MP zCODE_HEAP_SNOC |> Q.INST [`xs`|->`code`] 29 val th = SPEC_COMPOSE_RULE [th1,th2] |> HIDE_STATUS_RULE true sts 30 val (th,goal) = SPEC_WEAKEN_RULE th 31 ``zCODE_HEAP_RAX F a n (SNOC (w2w r1) code) * zR 0x1w r1 * 32 zPC (rip + 0x5w) * ~zS`` 33 val lemma = prove(goal, 34 FULL_SIMP_TAC (std_ss++star_ss) [zCODE_HEAP_RAX_def,LENGTH_SNOC,ADD1,SEP_IMP_REFL]); 35 val th = MP th lemma 36 val (th,goal) = SPEC_STRENGTHEN_RULE th 37 ``zCODE_HEAP_RAX F a n code * zR 0x1w r1 * 38 zPC rip * ~zS * cond (LENGTH code < n)`` 39 val lemma = prove(goal, 40 FULL_SIMP_TAC (std_ss++star_ss) [zCODE_HEAP_RAX_def,LENGTH_SNOC,ADD1,SEP_IMP_REFL]); 41 val th = MP th lemma 42 in th |> REWRITE_RULE [SNOC_APPEND] end; 43 44val SNOC_IMM = let 45 val (_,_,sts,_) = x64_tools 46 val ((th1,_,_),_) = x64_spec "C600" 47 val ((th2,_,_),_) = x64_spec (x64_encode "inc r0") 48 val th1 = th1 |> REWRITE_RULE [SIGN_EXTEND_IGNORE,n2w_w2n, 49 GSYM zBYTE_MEMORY_Z_def,zBYTE_MEMORY_def] 50 |> Q.GEN `g` |> Q.GEN `dg` 51 |> Q.INST [`r0`|->`a+n2w (LENGTH (code:word8 list))`,`imm8`|->`n2w k`] 52 |> MATCH_MP zCODE_HEAP_SNOC |> Q.INST [`xs`|->`code`] 53 val th = SPEC_COMPOSE_RULE [th1,th2] |> HIDE_STATUS_RULE true sts 54 val (th,goal) = SPEC_WEAKEN_RULE th 55 ``zCODE_HEAP_RAX F a n (SNOC (n2w k) code) * 56 zPC (rip + 0x6w) * ~zS`` 57 val lemma = prove(goal, 58 FULL_SIMP_TAC (std_ss++star_ss) [zCODE_HEAP_RAX_def,LENGTH_SNOC,ADD1,SEP_IMP_REFL]); 59 val th = MP th lemma 60 val (th,goal) = SPEC_STRENGTHEN_RULE th 61 ``zCODE_HEAP_RAX F a n code * 62 zPC rip * ~zS * cond (LENGTH code < n)`` 63 val lemma = prove(goal, 64 FULL_SIMP_TAC (std_ss++star_ss) [zCODE_HEAP_RAX_def,LENGTH_SNOC,ADD1,SEP_IMP_REFL]); 65 val th = MP th lemma 66 in th |> REWRITE_RULE [SNOC_APPEND] end; 67 68val LUPDATE_R1 = let 69 val ((th1,_,_),_) = x64_spec (x64_encode "mov BYTE [r2],r1b") 70 val th1 = th1 |> REWRITE_RULE [SIGN_EXTEND_IGNORE,n2w_w2n, 71 GSYM zBYTE_MEMORY_Z_def,zBYTE_MEMORY_def] 72 |> Q.GEN `g` |> Q.GEN `dg` 73 |> Q.INST [`r2`|->`a+n2w k`,`imm8`|->`n2w k1`] 74 |> MATCH_MP zCODE_HEAP_UPDATE |> Q.INST [`xs`|->`code`] 75 val th1 = SPEC_FRAME_RULE th1 ``zR 0w (a + n2w (LENGTH (code:word8 list)))`` 76 val (th,goal) = SPEC_WEAKEN_RULE th1 77 ``zCODE_HEAP_RAX F a n (LUPDATE (w2w r1) k code) * zR 0x2w (a + n2w k) * 78 zR 1w r1 * zPC (rip + 0x2w)`` 79 val lemma = prove(goal, 80 FULL_SIMP_TAC (std_ss++star_ss) [zCODE_HEAP_RAX_def,LENGTH_SNOC,ADD1, 81 SEP_IMP_REFL,LENGTH_LUPDATE]); 82 val th = MP th lemma 83 val (th,goal) = SPEC_STRENGTHEN_RULE th 84 ``zCODE_HEAP_RAX F a n code * zR 0x2w (a + n2w k) * 85 zR 1w r1 * zPC rip * cond (k < LENGTH code)`` 86 val lemma = prove(goal, 87 FULL_SIMP_TAC (std_ss++star_ss) [zCODE_HEAP_RAX_def,LENGTH_SNOC,ADD1,SEP_IMP_REFL]); 88 val th = MP th lemma 89 in th end; 90 91val LUPDATE_IMM = let 92 val ((th1,_,_),_) = x64_spec "C602" 93 val th1 = th1 |> REWRITE_RULE [SIGN_EXTEND_IGNORE,n2w_w2n, 94 GSYM zBYTE_MEMORY_Z_def,zBYTE_MEMORY_def] 95 |> Q.GEN `g` |> Q.GEN `dg` 96 |> Q.INST [`r2`|->`a+n2w k`,`imm8`|->`n2w k1`] 97 |> MATCH_MP zCODE_HEAP_UPDATE |> Q.INST [`xs`|->`code`] 98 val th1 = SPEC_FRAME_RULE th1 ``zR 0w (a + n2w (LENGTH (code:word8 list)))`` 99 val (th,goal) = SPEC_WEAKEN_RULE th1 100 ``zCODE_HEAP_RAX F a n (LUPDATE (n2w k1) k code) * zR 0x2w (a + n2w k) * 101 zPC (rip + 0x3w)`` 102 val lemma = prove(goal, 103 FULL_SIMP_TAC (std_ss++star_ss) [zCODE_HEAP_RAX_def,LENGTH_SNOC,ADD1, 104 SEP_IMP_REFL,LENGTH_LUPDATE]); 105 val th = MP th lemma 106 val (th,goal) = SPEC_STRENGTHEN_RULE th 107 ``zCODE_HEAP_RAX F a n code * zR 0x2w (a + n2w k) * 108 zPC rip * cond (k < LENGTH code)`` 109 val lemma = prove(goal, 110 FULL_SIMP_TAC (std_ss++star_ss) [zCODE_HEAP_RAX_def,LENGTH_SNOC,ADD1,SEP_IMP_REFL]); 111 val th = MP th lemma 112 in th end; 113 114val IMM32_def = Define ` 115 IMM32 (w:word32) = 116 [w2w w; w2w (w >>> 8); w2w (w >>> 16); w2w (w >>> 24)]:word8 list`; 117 118val IMM32_INTRO = prove( 119 ``[w2w r1; w2w (r1 >>> 8); w2w (r1 >>> 16); w2w (r1 >>> 24)] = 120 IMM32 (w2w (r1:word64))``, 121 FULL_SIMP_TAC (srw_ss()) [IMM32_def] \\ blastLib.BBLAST_TAC); 122 123val SNOC_IMM32 = let 124 val th0 = SNOC_R1 125 val (_,_,sts,_) = x64_tools 126 val ((th2,_,_),_) = x64_spec (x64_encode "mov r1,r2") 127 val ((th1,_,_),_) = x64_spec (x64_encode "shr r1,8") 128 val th1 = HIDE_STATUS_RULE true sts th1 129 val th = SPEC_COMPOSE_RULE [th2,th0,th1,th0,th1,th0,th1,th0] 130 val th = th |> SIMP_RULE (std_ss++sep_cond_ss) 131 [LENGTH,LENGTH_APPEND,GSYM APPEND_ASSOC,APPEND,LSR_ADD,ADD_CLAUSES, 132 DECIDE ``k < n /\ k+1 < n /\ k+1+1 < n /\ k+1+1+1 < n 133 = k + 4 <= n``,IMM32_INTRO] 134 in th end; 135 136 137(* a stack assertion: 138 - RSP points at the top element in the stack, 139 - the stack grows towards 0, 140 - there is a Ghost_stack_top of the stack 141 - SPEC is setup to say nothing if RSP hits Ghost_stack_top 142 *) 143 144val stack_list_def = Define ` 145 (stack_list a [] = emp) /\ 146 (stack_list a (x::xs) = one (a,x:word64) * stack_list (a+8w) xs)`; 147 148val stack_list_rev_def = Define ` 149 (stack_list_rev a [] = emp) /\ 150 (stack_list_rev a (x::xs) = one (a-8w,x:word64) * stack_list_rev (a-8w) xs)`; 151 152val stack_ok_def = Define ` 153 stack_ok (rsp:word64) top base stack dm m = 154 (rsp && 7w = 0w) /\ (top && 7w = 0w) /\ (base && 7w = 0w) /\ 155 (rsp + n2w (8 * LENGTH stack) = base) /\ 156 ?rest. (stack_list top (rest ++ stack)) (fun2set (m,dm)) /\ 157 (top + n2w (8 * LENGTH (rest ++ stack)) = base) /\ 158 8 * LENGTH (rest ++ stack) < 2 ** 64 /\ rest <> []`; 159 160val zSTACK_def = Define ` 161 zSTACK (base,stack) = 162 SEP_EXISTS rsp top dm m. 163 zR1 RSP rsp * zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 164 zMEMORY64 dm m * cond (stack_ok rsp top base stack dm m)`; 165 166val x0 = ("r0",``0w:word4``,``r0:word64``) 167val x1 = ("r1",``1w:word4``,``r1:word64``) 168val x2 = ("r2",``2w:word4``,``r2:word64``) 169val x3 = ("r3",``3w:word4``,``r3:word64``) 170val x6 = ("r6",``6w:word4``,``r6:word64``) 171val x7 = ("r7",``7w:word4``,``r7:word64``) 172val x8 = ("r8",``8w:word4``,``r8:word64``) 173val x9 = ("r9",``9w:word4``,``r9:word64``) 174val x10 = ("r10",``10w:word4``,``r10:word64``) 175val x11 = ("r11",``11w:word4``,``r11:word64``) 176val x12 = ("r12",``12w:word4``,``r12:word64``) 177val x13 = ("r13",``13w:word4``,``r13:word64``) 178val x14 = ("r14",``14w:word4``,``r14:word64``) 179val x15 = ("r15",``15w:word4``,``r15:word64``) 180 181val stack_ss = Q.INST [`stack`|->`ss`] 182 183(* lemmas *) 184 185val stack_list_APPEND = prove( 186 ``!xs ys a. stack_list a (xs ++ ys) = 187 stack_list a xs * stack_list (a + n2w (8 * LENGTH xs)) ys``, 188 Induct \\ ASM_SIMP_TAC std_ss [APPEND,stack_list_def,SEP_CLAUSES,LENGTH, 189 WORD_ADD_0,STAR_ASSOC,addressTheory.word_arith_lemma1,MULT_CLAUSES]); 190 191val stack_list_REVERSE = prove( 192 ``!rest. stack_list top (REVERSE rest) = 193 stack_list_rev (top + n2w (8 * LENGTH rest)) rest``, 194 Induct THEN1 EVAL_TAC 195 \\ SRW_TAC [] [MULT_CLAUSES] 196 \\ SIMP_TAC std_ss [stack_list_rev_def] 197 \\ ONCE_REWRITE_TAC [ADD_COMM] 198 \\ SIMP_TAC std_ss [GSYM addressTheory.word_arith_lemma1,WORD_ADD_SUB] 199 \\ ASM_SIMP_TAC (std_ss++star_ss) [stack_list_APPEND,LENGTH_REVERSE, 200 stack_list_def,SEP_CLAUSES]) 201 |> Q.SPEC `REVERSE xs` 202 |> SIMP_RULE std_ss [LENGTH_REVERSE,REVERSE_REVERSE] |> GSYM; 203 204val stack_list_rev_REVERSE = 205 stack_list_REVERSE |> Q.GEN `xs` 206 |> Q.SPEC `REVERSE xs` |> SIMP_RULE std_ss [LENGTH_REVERSE,REVERSE_REVERSE] 207 208val stack_ok_thm = prove( 209 ``stack_ok rsp top base stack dm m = 210 (rsp && 7w = 0w) /\ (top && 7w = 0w) /\ (base && 7w = 0w) /\ 211 (rsp + n2w (8 * LENGTH stack) = base) /\ 212 ?rest. (stack_list_rev rsp rest * stack_list rsp stack) (fun2set (m,dm)) /\ 213 (top + n2w (8 * LENGTH (rest ++ stack)) = base) /\ 214 8 * LENGTH (rest ++ stack) < 2 ** 64 /\ rest <> []``, 215 SIMP_TAC std_ss [stack_ok_def] 216 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ STRIP_TAC 217 \\ FULL_SIMP_TAC std_ss [] 218 \\ Q.EXISTS_TAC `REVERSE rest` 219 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH_REVERSE,REVERSE_EQ_NIL] 220 \\ `rsp = top + n2w (8 * LENGTH rest)` by 221 (FULL_SIMP_TAC std_ss [LEFT_ADD_DISTRIB,GSYM addressTheory.word_arith_lemma1] 222 \\ Q.PAT_X_ASSUM `xx + yy = base` (ASSUME_TAC o GSYM) 223 \\ FULL_SIMP_TAC std_ss [wordsTheory.WORD_EQ_ADD_RCANCEL,WORD_ADD_ASSOC]) 224 \\ FULL_SIMP_TAC std_ss [stack_list_REVERSE,stack_list_APPEND] 225 \\ FULL_SIMP_TAC std_ss [stack_list_rev_REVERSE,LENGTH_REVERSE]); 226 227(* pop *) 228 229val stack_ok_POP = prove( 230 ``stack_ok rsp top base stack dm m /\ stack <> [] ==> 231 rsp IN dm /\ (m rsp = HD stack) /\ (rsp && 0x7w = 0x0w) /\ 232 stack_ok (rsp + 8w) top base (TL stack) dm m``, 233 SIMP_TAC std_ss [stack_ok_thm] \\ STRIP_TAC 234 \\ Cases_on `stack` \\ FULL_SIMP_TAC std_ss [HD,TL] 235 \\ FULL_SIMP_TAC std_ss [PULL_EXISTS] \\ Q.EXISTS_TAC `h::rest` 236 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND,ADD1,AC ADD_COMM ADD_ASSOC, 237 LEFT_ADD_DISTRIB,addressTheory.word_arith_lemma1] 238 \\ FULL_SIMP_TAC std_ss [APPEND,GSYM APPEND_ASSOC] 239 \\ FULL_SIMP_TAC std_ss [stack_list_rev_def,stack_list_def,NOT_CONS_NIL] 240 \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [WORD_ADD_SUB] 241 \\ FULL_SIMP_TAC (std_ss++star_ss) [] 242 \\ Q.PAT_X_ASSUM `rsp && 0x7w = 0x0w` MP_TAC 243 \\ blastLib.BBLAST_TAC); 244 245fun x64_pop (s,r,v) = save_thm("x64_pop_" ^ s,let 246 val ((th,_,_),_) = x64_spec_memory64 (x64_encode ("pop " ^ s)) 247 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 248 val th = SPEC_FRAME_RULE th `` 249 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 250 cond (stack_ok rsp top base stack dm m /\ stack <> [])`` 251 val (th,goal) = SPEC_WEAKEN_RULE th 252 ``zPC (p + 2w) * zR ^r (HD stack) * zSTACK (base,TL stack)`` 253 val lemma = prove(goal, 254 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 255 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp+8w`,`top`,`dm`,`m`] 256 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 257 \\ IMP_RES_TAC stack_ok_POP 258 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 259 val th = MP th lemma 260 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 261 |> SIMP_RULE std_ss [SPEC_PRE_EXISTS] 262 val (th,goal) = SPEC_STRENGTHEN_RULE th 263 ``zPC p * zR ^r ^v * zSTACK (base,stack) * cond (stack <> [])`` 264 val lemma = prove(goal, 265 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 266 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 267 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 268 \\ IMP_RES_TAC stack_ok_POP 269 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 270 val th = MP th lemma 271 in th |> stack_ss end); 272 273val all_pops = map x64_pop [x0,x1,x2,x3,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15]; 274 275(* push *) 276 277val stack_ok_PUSH = prove( 278 ``stack_ok rsp top base stack dm m ==> 279 rsp - 0x8w IN dm /\ (rsp - 0x8w && 0x7w = 0x0w) /\ 280 (stack_ok (rsp - 8w) top base (v::stack) dm ((rsp - 8w =+ v) m) \/ 281 (top = rsp - 8w))``, 282 SIMP_TAC std_ss [stack_ok_thm] \\ STRIP_TAC 283 \\ Cases_on `top = rsp - 8w` \\ FULL_SIMP_TAC std_ss [] 284 \\ Cases_on `rest` \\ FULL_SIMP_TAC std_ss [stack_list_rev_def] \\ SEP_R_TAC 285 \\ SIMP_TAC std_ss [LENGTH,MULT_CLAUSES,GSYM addressTheory.word_arith_lemma1] 286 \\ ASM_SIMP_TAC std_ss [WORD_SUB_ADD] 287 \\ SIMP_TAC std_ss [PULL_EXISTS] 288 \\ Q.EXISTS_TAC `t` \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND] 289 \\ FULL_SIMP_TAC std_ss [LEFT_ADD_DISTRIB,MULT_CLAUSES] 290 \\ FULL_SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC,stack_list_def,WORD_SUB_ADD] 291 \\ Cases_on `t = []` \\ FULL_SIMP_TAC std_ss [] THEN1 292 (FULL_SIMP_TAC std_ss [LENGTH,GSYM word_add_n2w] 293 \\ Q.ABBREV_TAC `s = 8 * LENGTH stack` 294 \\ NTAC 2 (Q.PAT_X_ASSUM `x = y:word64` MP_TAC) 295 \\ REPEAT (Q.PAT_X_ASSUM `x <> y:word64` MP_TAC) 296 \\ blastLib.BBLAST_TAC) 297 \\ FULL_SIMP_TAC (std_ss++star_ss) [WORD_ADD_ASSOC,WORD_SUB_ADD] 298 \\ SIMP_TAC std_ss [CONJ_ASSOC] \\ STRIP_TAC 299 THEN1 (Q.PAT_X_ASSUM `rsp && 0x7w = 0x0w` MP_TAC \\ blastLib.BBLAST_TAC) 300 \\ SEP_W_TAC \\ FULL_SIMP_TAC (std_ss++star_ss) []); 301 302val X64_SPEC_WEAKEN = prove( 303 ``!p c q. SPEC X64_MODEL p EMPTY q ==> 304 !r. SEP_IMP q (r \/ SEP_EXISTS x frame. 305 zR1 RSP x * zR1 zGhost_stack_top x * frame) ==> 306 SPEC X64_MODEL p EMPTY r``, 307 SIMP_TAC std_ss [X64_SPEC_SEMANTICS] \\ REPEAT STRIP_TAC 308 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`y`,`s`,`t1`,`seq`]) 309 \\ FULL_SIMP_TAC std_ss [] \\ REVERSE STRIP_TAC THEN1 (METIS_TAC []) 310 \\ Q.LIST_EXISTS_TAC [`k`,`t2`] \\ FULL_SIMP_TAC std_ss [] 311 \\ FULL_SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def,SEP_EXISTS_THM] 312 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 313 \\ `?rs st ei ms. y = (rs,st,ei,ms)` by METIS_TAC [PAIR] 314 \\ `?r e s m i. t2 = (r,e,s,m,i)` by METIS_TAC [PAIR] 315 \\ `?r e s m i. seq k = (r,e,s,m,i)` by METIS_TAC [PAIR] 316 \\ FULL_SIMP_TAC std_ss [STAR_x64_2set,GSYM STAR_ASSOC] 317 \\ FULL_SIMP_TAC std_ss [X64_STACK_FULL_def,x64_icacheTheory.X64_ICACHE_def] 318 \\ SRW_TAC [] []) |> SIMP_RULE std_ss [PULL_FORALL,AND_IMP_INTRO]; 319 320val X64_SPEC_WEAKEN = prove( 321 ``!p c q. SPEC X64_MODEL p c q ==> 322 !r. SEP_IMP q (r \/ SEP_EXISTS x frame. 323 zR1 RSP x * zR1 zGhost_stack_top x * frame) ==> 324 SPEC X64_MODEL p c r``, 325 ONCE_REWRITE_TAC [GSYM X64_SPEC_CODE] \\ REPEAT STRIP_TAC 326 \\ MATCH_MP_TAC X64_SPEC_WEAKEN 327 \\ Q.EXISTS_TAC `zCODE c * q` \\ FULL_SIMP_TAC std_ss [] 328 \\ IMP_RES_TAC SEP_IMP_FRAME 329 \\ POP_ASSUM (MP_TAC o Q.SPEC `zCODE c`) 330 \\ SIMP_TAC (std_ss++star_ss) [SEP_CLAUSES] 331 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def,SEP_EXISTS_THM] 332 \\ REPEAT STRIP_TAC \\ RES_TAC THEN1 (METIS_TAC []) 333 \\ METIS_TAC [STAR_ASSOC,STAR_COMM]); 334 335val X64_SPEC_1_WEAKEN = prove( 336 ``!p c q. SPEC_1 X64_MODEL p EMPTY q SEP_F ==> 337 !r. SEP_IMP q (r \/ SEP_EXISTS x frame. 338 zR1 RSP x * zR1 zGhost_stack_top x * frame) ==> 339 SPEC_1 X64_MODEL p EMPTY r SEP_F``, 340 SIMP_TAC std_ss [X64_SPEC_1_SEMANTICS] \\ REPEAT STRIP_TAC 341 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`y`,`s`,`t1`,`seq`]) 342 \\ FULL_SIMP_TAC std_ss [] \\ REVERSE STRIP_TAC THEN1 (METIS_TAC []) 343 \\ Cases_on `X64_STACK_FULL (seq (k+1))` THEN1 METIS_TAC [] 344 \\ Cases_on `X64_STACK_FULL (seq k)` THEN1 METIS_TAC [] 345 \\ Q.LIST_EXISTS_TAC [`k`,`t2`] \\ FULL_SIMP_TAC std_ss [] 346 \\ FULL_SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def,SEP_EXISTS_THM] 347 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 348 \\ `?rs st ei ms. y = (rs,st,ei,ms)` by METIS_TAC [PAIR] 349 \\ `?r e s m i. t2 = (r,e,s,m,i)` by METIS_TAC [PAIR] 350 \\ `?r e s m i. seq (k+1) = (r,e,s,m,i)` by METIS_TAC [PAIR] 351 \\ FULL_SIMP_TAC std_ss [STAR_x64_2set,GSYM STAR_ASSOC] 352 \\ FULL_SIMP_TAC std_ss [X64_STACK_FULL_def,x64_icacheTheory.X64_ICACHE_def] 353 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss []) 354 |> SIMP_RULE std_ss [PULL_FORALL,AND_IMP_INTRO]; 355 356val X64_SPEC_1_WEAKEN = prove( 357 ``!p c q. SPEC_1 X64_MODEL p c q SEP_F ==> 358 !r. SEP_IMP q (r \/ SEP_EXISTS x frame. 359 zR1 RSP x * zR1 zGhost_stack_top x * frame) ==> 360 SPEC_1 X64_MODEL p c r SEP_F``, 361 ONCE_REWRITE_TAC [GSYM X64_SPEC_1_CODE] \\ REPEAT STRIP_TAC 362 \\ MATCH_MP_TAC X64_SPEC_1_WEAKEN 363 \\ Q.EXISTS_TAC `zCODE c * q` \\ FULL_SIMP_TAC std_ss [] 364 \\ IMP_RES_TAC SEP_IMP_FRAME 365 \\ POP_ASSUM (MP_TAC o Q.SPEC `zCODE c`) 366 \\ SIMP_TAC (std_ss++star_ss) [SEP_CLAUSES] 367 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def,SEP_EXISTS_THM] 368 \\ REPEAT STRIP_TAC \\ RES_TAC THEN1 (METIS_TAC []) 369 \\ METIS_TAC [STAR_ASSOC,STAR_COMM]); 370 371fun x64_push (s,r,v) = save_thm("x64_push_" ^ s,let 372 val ((th,_,_),_) = x64_spec_memory64 (x64_encode ("push " ^ s)) 373 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 374 val th = SPEC_FRAME_RULE th `` 375 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 376 cond (stack_ok rsp top base stack dm m)`` 377 val th = MATCH_MP X64_SPEC_WEAKEN th 378 |> Q.SPEC `zPC (p + 2w) * zR ^r ^v * zSTACK (base,^v::stack)` 379 val goal = th |> concl |> dest_imp |> fst 380 val lemma = prove(goal, 381 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 382 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp-8w`, 383 `zPC (p + 0x2w) * zR ^r ^v * 384 zR1 zGhost_stack_bottom base * zMEMORY64 dm ((rsp - 0x8w =+ ^v) m)`, 385 `rsp-8w`,`top`,`dm`, 386 `((rsp - 0x8w =+ ^v) m)`] 387 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR,SEP_DISJ_def] 388 \\ IMP_RES_TAC stack_ok_PUSH 389 \\ POP_ASSUM (STRIP_ASSUME_TAC o SPEC v) 390 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 391 val th = MP th lemma 392 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 393 |> SIMP_RULE std_ss [SPEC_PRE_EXISTS] 394 val (th,goal) = SPEC_STRENGTHEN_RULE th 395 ``zPC p * zR ^r ^v * zSTACK (base,stack)`` 396 val lemma = prove(goal, 397 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 398 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 399 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 400 \\ IMP_RES_TAC stack_ok_PUSH 401 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 402 val th = MP th lemma 403 in th |> stack_ss end); 404 405val all_pushes = map x64_push [x0,x1,x2,x3,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15]; 406 407(* call *) 408 409val sw2sw_64_32 = 410 sw2sw_def |> INST_TYPE [``:'b``|->``:64``,``:'a``|->``:32``] 411 |> SIMP_RULE std_ss [EVAL ``dimindex (:64)``,EVAL ``dimindex (:32)``] 412 |> GSYM 413 414fun SPEC_1_FRAME_RULE th tm = 415 SPEC tm (MATCH_MP temporalTheory.SPEC_1_FRAME th) |> RW [SEP_CLAUSES] 416 417val x64_call_imm_raw_spec_1 = let 418 val th = x64_Lib.x64_step "48E8" 419 val c = calc_code th 420 val th = pre_process_thm th 421 val th = RW [w2n_MOD] th 422 val th = x64_prove_one_spec_1 th c 423 val th = introduce_zMEMORY64 th 424 in th end 425 426val x64_call_imm_spec_1 = save_thm("x64_call_imm_spec_1",let 427 val th = x64_call_imm_raw_spec_1 428 val th = th |> RW [sw2sw_64_32,GSYM word_add_n2w,WORD_ADD_ASSOC] 429 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 430 val th = SPEC_1_FRAME_RULE th `` 431 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 432 cond (stack_ok rsp top base stack dm m)`` 433 val new_p = ``(p + 6w + sw2sw (imm32:word32)):word64`` 434 val th = MATCH_MP X64_SPEC_1_WEAKEN th 435 |> Q.SPEC `zPC ^new_p * zSTACK (base,p+6w::stack)` 436 val goal = th |> concl |> dest_imp |> fst 437 val lemma = prove(goal, 438 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 439 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`top`, 440 `zPC ^new_p * 441 zR1 zGhost_stack_bottom base * zMEMORY64 dm ((rsp - 0x8w =+ p+6w) m)`, 442 `rsp-8w`,`top`,`dm`, 443 `((rsp - 0x8w =+ p+6w) m)`] 444 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR,SEP_DISJ_def] 445 \\ IMP_RES_TAC stack_ok_PUSH 446 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `p+6w`) 447 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 448 val th = MP th lemma 449 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 450 |> SIMP_RULE std_ss [SPEC_1_PRE_EXISTS] 451 val (th,goal) = SPEC_STRENGTHEN_RULE th 452 ``zPC p * zSTACK (base,stack)`` 453 val lemma = prove(goal, 454 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 455 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 456 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 457 \\ IMP_RES_TAC stack_ok_PUSH 458 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 459 val th = MP th lemma 460 val th = RW [GSYM IMM32_def,GSYM word_add_n2w,WORD_ADD_ASSOC] th 461 in th |> stack_ss end); 462 463val x64_call_imm = save_thm("x64_call_imm",let 464 val ((th,_,_),_) = x64_spec_memory64 "48E8" 465 val th = th |> RW [sw2sw_64_32,GSYM word_add_n2w,WORD_ADD_ASSOC] 466 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 467 val th = SPEC_FRAME_RULE th `` 468 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 469 cond (stack_ok rsp top base stack dm m)`` 470 val new_p = ``(p + 6w + sw2sw (imm32:word32)):word64`` 471 val th = MATCH_MP X64_SPEC_WEAKEN th 472 |> Q.SPEC `zPC ^new_p * zSTACK (base,p+6w::stack)` 473 val goal = th |> concl |> dest_imp |> fst 474 val lemma = prove(goal, 475 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 476 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`top`, 477 `zPC ^new_p * 478 zR1 zGhost_stack_bottom base * zMEMORY64 dm ((rsp - 0x8w =+ p+6w) m)`, 479 `rsp-8w`,`top`,`dm`, 480 `((rsp - 0x8w =+ p+6w) m)`] 481 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR,SEP_DISJ_def] 482 \\ IMP_RES_TAC stack_ok_PUSH 483 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `p+6w`) 484 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 485 val th = MP th lemma 486 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 487 |> SIMP_RULE std_ss [SPEC_PRE_EXISTS] 488 val (th,goal) = SPEC_STRENGTHEN_RULE th 489 ``zPC p * zSTACK (base,stack)`` 490 val lemma = prove(goal, 491 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 492 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 493 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 494 \\ IMP_RES_TAC stack_ok_PUSH 495 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 496 val th = MP th lemma 497 val th = RW [GSYM IMM32_def,GSYM word_add_n2w,WORD_ADD_ASSOC] th 498 in th |> stack_ss end); 499 500fun x64_call (s,r,v) = save_thm("x64_call_" ^ s,let 501 val ((th,_,_),_) = x64_spec_memory64 (x64_encode ("call " ^ s)) 502 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 503 val th = SPEC_FRAME_RULE th `` 504 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 505 cond (stack_ok rsp top base stack dm m)`` 506 val new_p = v 507 val th = MATCH_MP X64_SPEC_WEAKEN th 508 |> Q.SPEC `zPC ^new_p * zR ^r ^v * zSTACK (base,p+3w::stack)` 509 val goal = th |> concl |> dest_imp |> fst 510 val lemma = prove(goal, 511 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 512 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`top`, 513 `zPC ^new_p * zR ^r ^v * 514 zR1 zGhost_stack_bottom base * zMEMORY64 dm ((rsp - 0x8w =+ p+3w) m)`, 515 `rsp-8w`,`top`,`dm`, 516 `((rsp - 0x8w =+ p+3w) m)`] 517 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR,SEP_DISJ_def] 518 \\ IMP_RES_TAC stack_ok_PUSH 519 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `p+3w`) 520 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 521 val th = MP th lemma 522 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 523 |> SIMP_RULE std_ss [SPEC_PRE_EXISTS] 524 val (th,goal) = SPEC_STRENGTHEN_RULE th 525 ``zPC p * zR ^r ^v * zSTACK (base,stack)`` 526 val lemma = prove(goal, 527 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 528 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 529 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 530 \\ IMP_RES_TAC stack_ok_PUSH 531 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 532 val th = MP th lemma 533 val th = RW [GSYM IMM32_def,GSYM word_add_n2w,WORD_ADD_ASSOC] th 534 in th |> stack_ss end); 535 536val res = map x64_call [x0,x1,x2,x3,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15]; 537 538(* pops *) 539 540val LENGTH_LESS_EQ = prove( 541 ``!xs m. m <= LENGTH xs ==> ?ys zs. (xs = ys ++ zs) /\ (LENGTH ys = m)``, 542 Induct \\ SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC 543 \\ Cases_on `m` \\ FULL_SIMP_TAC std_ss [LENGTH_NIL,APPEND] 544 \\ RES_TAC \\ Q.LIST_EXISTS_TAC [`h::ys`,`zs`] 545 \\ FULL_SIMP_TAC std_ss [APPEND,LENGTH]); 546 547val stack_list_rev_APPEND = prove( 548 ``!rest ys a. 549 stack_list_rev a (rest ++ ys) = 550 stack_list_rev a rest * 551 stack_list_rev (a - n2w (8 * LENGTH rest)) ys``, 552 Induct THEN1 (FULL_SIMP_TAC (srw_ss()) [stack_list_rev_def,SEP_CLAUSES]) 553 \\ FULL_SIMP_TAC std_ss [stack_list_rev_def,SEP_CLAUSES,APPEND] 554 \\ FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM,LENGTH, 555 GSYM WORD_SUB_PLUS,word_add_n2w,MULT_CLAUSES]); 556 557val stack_ok_POPS = store_thm("stack_ok_POPS", 558 ``stack_ok rsp top base stack dm m /\ k <= LENGTH stack ==> 559 stack_ok (rsp + n2w (8 * k)) top base (DROP k stack) dm m``, 560 SIMP_TAC std_ss [stack_ok_thm] \\ STRIP_TAC 561 \\ IMP_RES_TAC LENGTH_LESS_EQ \\ FULL_SIMP_TAC std_ss [] 562 \\ POP_ASSUM (ASSUME_TAC o GSYM) 563 \\ FULL_SIMP_TAC std_ss [addressTheory.word_arith_lemma1, 564 rich_listTheory.DROP_LENGTH_APPEND,GSYM LEFT_ADD_DISTRIB,LENGTH_APPEND] 565 \\ FULL_SIMP_TAC std_ss [GSYM word_mul_n2w] \\ STRIP_TAC 566 THEN1 (Q.PAT_X_ASSUM `rsp && 0x7w = 0x0w` MP_TAC \\ blastLib.BBLAST_TAC) 567 \\ Q.EXISTS_TAC `REVERSE ys ++ rest` 568 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND,ADD_ASSOC,APPEND_eq_NIL,LENGTH_REVERSE] 569 \\ FULL_SIMP_TAC std_ss [stack_list_APPEND,STAR_ASSOC] 570 \\ SIMP_TAC std_ss [stack_list_rev_APPEND,word_mul_n2w,LENGTH_REVERSE] 571 \\ FULL_SIMP_TAC std_ss [WORD_ADD_SUB] 572 \\ FULL_SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC,word_mul_n2w] 573 \\ ONCE_REWRITE_TAC [GSYM LENGTH_REVERSE] 574 \\ ASM_SIMP_TAC std_ss [stack_list_rev_REVERSE] 575 \\ FULL_SIMP_TAC std_ss [REVERSE_REVERSE,AC STAR_COMM STAR_ASSOC,LENGTH_REVERSE]); 576 577val imm32_lemma = prove( 578 ``(k:num) < 2 ** 28 ==> 579 (SIGN_EXTEND 32 64 (w2n ((n2w:num->word32) (8 * k))) = 8 * k)``, 580 FULL_SIMP_TAC (srw_ss()) [w2n_n2w,bitTheory.SIGN_EXTEND_def,LET_DEF] 581 \\ REPEAT STRIP_TAC \\ `(8 * k) < 4294967296` by DECIDE_TAC 582 \\ FULL_SIMP_TAC std_ss [bitTheory.BIT_def,bitTheory.BITS_THM] 583 \\ `8 * k < 2147483648` by DECIDE_TAC 584 \\ FULL_SIMP_TAC std_ss [LESS_DIV_EQ_ZERO]); 585 586val x64_pops = save_thm("x64_pops",let 587 val ((pops,_,_),_) = x64_spec "4881C4" 588 val pops = RW [GSYM IMM32_def] pops 589 val th = Q.INST [`imm32`|->`n2w (8*k)`,`rip`|->`p`] pops 590 val th = DISCH ``(k:num) < 2 ** 28`` th 591 val lemma2 = prove( 592 ``k < 2 ** 28 ==> (8 * k) < 18446744073709551616n``, 593 FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC); 594 val th = SIMP_RULE bool_ss [lemma2,RW1 [MULT_COMM] MULT_DIV, 595 RW1 [MULT_COMM] MOD_EQ_0,imm32_lemma] th 596 val th = Q.INST [`x1`|->`ss`] (RW [GSYM SPEC_MOVE_COND] th) 597 val th = SIMP_RULE bool_ss [imm32_lemma] th 598 val (_,_,sts,_) = x64_tools 599 val th = th |> HIDE_STATUS_RULE true sts 600 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 601 val th = SPEC_FRAME_RULE th `` 602 zMEMORY64 dm m * 603 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 604 cond (stack_ok rsp top base stack dm m /\ k <= LENGTH stack)`` 605 val (th,goal) = SPEC_WEAKEN_RULE th 606 ``zPC (p + 7w) * zSTACK (base,DROP k stack) * ~zS`` 607 val lemma = prove(goal, 608 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 609 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp+n2w (8*k)`,`top`,`dm`,`m`] 610 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 611 \\ IMP_RES_TAC stack_ok_POPS 612 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 613 val th = MP th lemma 614 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 615 |> SIMP_RULE std_ss [SPEC_PRE_EXISTS] 616 val (th,goal) = SPEC_STRENGTHEN_RULE th 617 ``zPC p * zSTACK (base,stack) * ~zS * cond (k <= LENGTH stack /\ k < 2 ** 28)`` 618 val lemma = prove(goal, 619 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 620 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 621 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 622 \\ IMP_RES_TAC stack_ok_POPS 623 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 624 val th = MP th lemma 625 in th |> stack_ss end); 626 627(* ret *) 628 629val x64_ret_raw_spec_1 = let 630 val th = x64_Lib.x64_step (x64_encode "ret") 631 val c = calc_code th 632 val th = pre_process_thm th 633 val th = RW [w2n_MOD] th 634 val th = x64_prove_one_spec_1 th c 635 val th = introduce_zMEMORY64 th 636 in th end 637 638val x64_ret_spec_1 = save_thm("x64_ret_spec_1",let 639 val th = x64_ret_raw_spec_1 640 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 641 val th = SPEC_1_FRAME_RULE th `` 642 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 643 cond (stack_ok rsp top base stack dm m /\ stack <> [])`` 644 val (th,goal) = SPEC_WEAKEN_RULE th 645 ``zPC (HD stack) * zSTACK (base,TL stack)`` 646 val lemma = prove(goal, 647 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 648 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp+8w`,`top`,`dm`,`m`] 649 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 650 \\ IMP_RES_TAC stack_ok_POP 651 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 652 val th = MP th lemma 653 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 654 |> SIMP_RULE std_ss [SPEC_1_PRE_EXISTS] 655 val (th,goal) = SPEC_STRENGTHEN_RULE th 656 ``zPC p * zSTACK (base,stack) * cond (stack <> [])`` 657 val lemma = prove(goal, 658 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 659 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 660 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 661 \\ IMP_RES_TAC stack_ok_POP 662 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 663 val th = MP th lemma 664 in th |> stack_ss end); 665 666val x64_ret = save_thm("x64_ret",let 667 val ((th,_,_),_) = x64_spec_memory64 (x64_encode "ret") 668 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 669 val th = SPEC_FRAME_RULE th `` 670 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 671 cond (stack_ok rsp top base stack dm m /\ stack <> [])`` 672 val (th,goal) = SPEC_WEAKEN_RULE th 673 ``zPC (HD stack) * zSTACK (base,TL stack)`` 674 val lemma = prove(goal, 675 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 676 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp+8w`,`top`,`dm`,`m`] 677 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 678 \\ IMP_RES_TAC stack_ok_POP 679 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 680 val th = MP th lemma 681 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 682 |> SIMP_RULE std_ss [SPEC_PRE_EXISTS] 683 val (th,goal) = SPEC_STRENGTHEN_RULE th 684 ``zPC p * zSTACK (base,stack) * cond (stack <> [])`` 685 val lemma = prove(goal, 686 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 687 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 688 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 689 \\ IMP_RES_TAC stack_ok_POP 690 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 691 val th = MP th lemma 692 in th |> stack_ss end); 693 694(* SPEC_1 jmp imm *) 695 696val x64_ret_raw_spec_1 = save_thm("x64_ret_raw_spec_1",let 697 val th = x64_Lib.x64_step "48E9" 698 val c = calc_code th 699 val th = pre_process_thm th 700 val th = RW [w2n_MOD] th 701 val th = x64_prove_one_spec_1 th c 702 in th end); 703 704(* read/write stack *) 705 706val LENGTH_LESS = prove( 707 ``!xs m. m < LENGTH xs ==> ?ys z zs. (xs = ys ++ z::zs) /\ (LENGTH ys = m)``, 708 Induct \\ SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC 709 \\ Cases_on `m` \\ FULL_SIMP_TAC std_ss [LENGTH_NIL,APPEND,CONS_11] 710 \\ RES_TAC \\ Q.LIST_EXISTS_TAC [`h::ys`,`z`,`zs`] 711 \\ FULL_SIMP_TAC std_ss [APPEND,LENGTH,GSYM APPEND_ASSOC]); 712 713val EL_LENGTH = prove( 714 ``!xs y ys. EL (LENGTH xs) (xs ++ y::ys) = y``, 715 Induct \\ FULL_SIMP_TAC std_ss [LENGTH,EL,APPEND,HD,TL]); 716 717val stack_ok_EL = store_thm("stack_ok_EL", 718 ``stack_ok rsp top base stack dm m /\ 719 w2n r8 DIV 8 < LENGTH stack /\ (w2n r8 MOD 8 = 0) ==> 720 (r8 + rsp IN dm /\ (r8 + rsp && 0x7w = 0x0w)) /\ 721 stack_ok rsp top base (LUPDATE r0 (w2n r8 DIV 8) stack) dm 722 ((r8 + rsp =+ r0) m) /\ 723 (m (r8 + rsp) = EL (w2n r8 DIV 8) stack)``, 724 SIMP_TAC std_ss [stack_ok_thm] \\ STRIP_TAC 725 \\ Cases_on `r8` \\ FULL_SIMP_TAC (srw_ss()) [] 726 \\ MP_TAC (DIVISION |> SIMP_RULE std_ss [PULL_FORALL] 727 |> Q.SPECL [`8`,`n`] |> RW1 [MULT_COMM]) 728 \\ ASM_SIMP_TAC std_ss [] \\ Q.ABBREV_TAC `k = n DIV 8` 729 \\ POP_ASSUM (K ALL_TAC) \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 730 \\ POP_ASSUM (K ALL_TAC) 731 \\ IMP_RES_TAC LENGTH_LESS 732 \\ POP_ASSUM (ASSUME_TAC o GSYM) 733 \\ FULL_SIMP_TAC std_ss [LUPDATE_LENGTH,EL_LENGTH] 734 \\ FULL_SIMP_TAC std_ss [PULL_EXISTS] 735 \\ Q.EXISTS_TAC `rest` 736 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND] 737 \\ FULL_SIMP_TAC std_ss [stack_list_APPEND,stack_list_def] 738 \\ SEP_R_TAC \\ STRIP_TAC 739 THEN1 (SIMP_TAC std_ss [GSYM word_mul_n2w] 740 \\ Q.PAT_X_ASSUM `0x7w && rsp = 0x0w` MP_TAC \\ blastLib.BBLAST_TAC) 741 \\ SEP_W_TAC \\ FULL_SIMP_TAC (std_ss++star_ss) []); 742 743val LENGTH_LESS_REV = prove( 744 ``!xs m. m < LENGTH xs ==> ?ys z zs. (xs = ys ++ z::zs) /\ (LENGTH zs = m)``, 745 recInduct SNOC_INDUCT \\ SIMP_TAC std_ss [LENGTH,LENGTH_SNOC] 746 \\ SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC 747 \\ Cases_on `m` \\ FULL_SIMP_TAC std_ss [LENGTH_NIL,APPEND,CONS_11,APPEND_NIL] 748 THEN1 (METIS_TAC []) \\ RES_TAC \\ Q.LIST_EXISTS_TAC [`ys`,`z`,`zs ++ [x]`] 749 \\ FULL_SIMP_TAC std_ss [APPEND,LENGTH,GSYM APPEND_ASSOC,LENGTH_APPEND,ADD1]); 750 751val stack_ok_REV_EL = store_thm("stack_ok_REV_EL", 752 ``stack_ok rsp top base stack dm m /\ 753 w2n r8 DIV 8 < LENGTH stack /\ (w2n r8 MOD 8 = 0) ==> 754 (base - 8w - r8 IN dm /\ (base - 8w - r8 && 0x7w = 0x0w)) /\ 755 (m (base - 8w - r8) = EL (w2n r8 DIV 8) (REVERSE stack))``, 756 SIMP_TAC std_ss [stack_ok_thm] \\ STRIP_TAC 757 \\ Cases_on `r8` \\ FULL_SIMP_TAC std_ss [w2n_n2w] 758 \\ MP_TAC (DIVISION |> SIMP_RULE std_ss [PULL_FORALL] 759 |> Q.SPECL [`8`,`n`] |> RW1 [MULT_COMM]) 760 \\ ASM_SIMP_TAC std_ss [] \\ Q.ABBREV_TAC `k = n DIV 8` 761 \\ POP_ASSUM (K ALL_TAC) \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 762 \\ POP_ASSUM (K ALL_TAC) 763 \\ IMP_RES_TAC LENGTH_LESS_REV 764 \\ FULL_SIMP_TAC std_ss [REVERSE_APPEND,REVERSE_DEF] 765 \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 766 \\ POP_ASSUM (ASSUME_TAC o GSYM) 767 \\ FULL_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 768 \\ ONCE_REWRITE_TAC [GSYM LENGTH_REVERSE] 769 \\ SIMP_TAC std_ss [rich_listTheory.EL_LENGTH_APPEND 770 |> Q.SPEC `x::xs` |> SIMP_RULE (srw_ss()) []] 771 \\ SIMP_TAC std_ss [LENGTH_REVERSE] 772 \\ FULL_SIMP_TAC std_ss [stack_list_APPEND,stack_list_def] 773 \\ Q.PAT_X_ASSUM `xx = base` (ASSUME_TAC o GSYM) \\ POP_ASSUM (K ALL_TAC) 774 \\ Q.PAT_X_ASSUM `xx = base` (ASSUME_TAC o GSYM) 775 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH,LEFT_ADD_DISTRIB] 776 \\ SIMP_TAC std_ss [MULT_CLAUSES,GSYM word_arith_lemma1] 777 \\ SIMP_TAC std_ss [WORD_ADD_SUB,WORD_ADD_ASSOC] 778 \\ ONCE_REWRITE_TAC [word_arith_lemma1] 779 \\ ONCE_REWRITE_TAC [word_arith_lemma1] 780 \\ SIMP_TAC std_ss [WORD_ADD_SUB,WORD_ADD_ASSOC] 781 \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [] 782 \\ SIMP_TAC std_ss [GSYM word_mul_n2w] 783 \\ Q.PAT_X_ASSUM `rsp && 0x7w = 0x0w` MP_TAC 784 \\ blastLib.BBLAST_TAC); 785 786val x64_el_r0_r8 = save_thm("x64_el_r0_r8",let 787 val ((th,_,_),_) = x64_spec_memory64 (x64_encode "mov [rsp+r8], r0") 788 val th = th |> RW [WORD_ADD_SUB] 789 val th = Q.INST [`rip`|->`p`] th 790 val pre = ``w2n r8 DIV 8 < LENGTH (stack:word64 list) /\ 791 (w2n (r8:word64) MOD 8 = 0)`` 792 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 793 val th = SPEC_FRAME_RULE th `` 794 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 795 cond (stack_ok rsp top base stack dm m /\ ^pre)`` 796 val (th,goal) = SPEC_WEAKEN_RULE th ``(zPC (p + 0x4w) * zR 0x8w r8 * 797 zR 0x0w r0 * zSTACK (base,LUPDATE r0 (w2n r8 DIV 8) stack))`` 798 val lemma = prove(goal, 799 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 800 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`, 801 `(r8 + rsp =+ r0) m`] 802 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 803 \\ IMP_RES_TAC stack_ok_EL 804 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 805 val th = MP th lemma 806 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 807 |> SIMP_RULE std_ss [SPEC_PRE_EXISTS] 808 val (th,goal) = SPEC_STRENGTHEN_RULE th 809 ``zPC p * zR 0x8w r8 * zR 0x0w r0 * zSTACK (base,stack) * cond (^pre)`` 810 val lemma = prove(goal, 811 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 812 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 813 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 814 \\ IMP_RES_TAC stack_ok_EL 815 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 816 val th = MP th lemma 817 in th |> stack_ss end); 818 819val x64_lupdate_r0_r8 = save_thm("x64_lupdate_r0_r8",let 820 val ((th,_,_),_) = x64_spec_memory64 (x64_encode "mov r0, [rsp+r8]") 821 val th = th |> RW [WORD_ADD_SUB] 822 val th = Q.INST [`rip`|->`p`] th 823 val pre = ``w2n r8 DIV 8 < LENGTH (stack:word64 list) /\ 824 (w2n (r8:word64) MOD 8 = 0)`` 825 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 826 val th = SPEC_FRAME_RULE th `` 827 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 828 cond (stack_ok rsp top base stack dm m /\ ^pre)`` 829 val (th,goal) = SPEC_WEAKEN_RULE th ``(zPC (p + 0x4w) * zR 0x8w r8 * 830 zR 0x0w (EL (w2n r8 DIV 8) stack) * zSTACK (base,stack))`` 831 val lemma = prove(goal, 832 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 833 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 834 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 835 \\ IMP_RES_TAC stack_ok_EL 836 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 837 val th = MP th lemma 838 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 839 |> SIMP_RULE std_ss [SPEC_PRE_EXISTS] 840 val (th,goal) = SPEC_STRENGTHEN_RULE th 841 ``zPC p * zR 0x8w r8 * zR 0x0w r0 * zSTACK (base,stack) * cond (^pre)`` 842 val lemma = prove(goal, 843 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 844 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 845 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 846 \\ IMP_RES_TAC stack_ok_EL 847 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 848 val th = MP th lemma 849 in th |> stack_ss end); 850 851val imm32_lemma = prove( 852 ``(k:num) < 2 ** 28 ==> 853 (SIGN_EXTEND 32 64 (w2n ((n2w:num->word32) (8 * k))) = 8 * k)``, 854 FULL_SIMP_TAC (srw_ss()) [w2n_n2w,bitTheory.SIGN_EXTEND_def,LET_DEF] 855 \\ REPEAT STRIP_TAC \\ `(8 * k) < 4294967296` by DECIDE_TAC 856 \\ FULL_SIMP_TAC std_ss [bitTheory.BIT_def,bitTheory.BITS_THM] 857 \\ `8 * k < 2147483648` by DECIDE_TAC 858 \\ FULL_SIMP_TAC std_ss [LESS_DIV_EQ_ZERO]); 859 860val stack_ok_EL_VAR = prove( 861 ``stack_ok rsp top base stack dm m /\ k < LENGTH stack ==> 862 (rsp + n2w (8 * k) IN dm /\ (rsp + n2w (8 * k) && 0x7w = 0x0w)) /\ 863 stack_ok rsp top base (LUPDATE r0 k stack) dm ((rsp + n2w (8 * k) =+ r0) m) /\ 864 (m (rsp + n2w (8 * k)) = EL k stack)``, 865 SIMP_TAC std_ss [stack_ok_thm] \\ STRIP_TAC 866 \\ FULL_SIMP_TAC std_ss [] 867 \\ IMP_RES_TAC LENGTH_LESS 868 \\ POP_ASSUM (ASSUME_TAC o GSYM) 869 \\ FULL_SIMP_TAC std_ss [LUPDATE_LENGTH,EL_LENGTH] 870 \\ FULL_SIMP_TAC std_ss [PULL_EXISTS] 871 \\ Q.EXISTS_TAC `rest` 872 \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND] 873 \\ FULL_SIMP_TAC std_ss [stack_list_APPEND,stack_list_def] 874 \\ SEP_R_TAC \\ STRIP_TAC 875 THEN1 (SIMP_TAC std_ss [GSYM word_mul_n2w] 876 \\ Q.PAT_X_ASSUM `rsp && 0x7w = 0x0w` MP_TAC \\ blastLib.BBLAST_TAC) 877 \\ SEP_W_TAC \\ FULL_SIMP_TAC (std_ss++star_ss) []); 878 879val x64_el_r0_imm = save_thm("x64_el_r0_imm",let 880 val ((th,_,_),_) = x64_spec_memory64 "488B8424" 881 val th = RW [GSYM IMM32_def] th 882 val th = Q.INST [`imm32`|->`n2w (8*k)`,`rip`|->`p`] th 883 val th = DISCH ``(k:num) < 2 ** 28`` th 884 val th = SIMP_RULE bool_ss [imm32_lemma] th 885 val lemma2 = prove( 886 ``k < 2 ** 28 ==> (8 * k) < 18446744073709551616n``, 887 FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC); 888 val th = RW1 [WORD_ADD_COMM] th |> RW [WORD_ADD_SUB] 889 val th = SIMP_RULE std_ss [lemma2,RW1 [MULT_COMM] MULT_DIV,w2n_n2w, 890 RW1 [MULT_COMM] MOD_EQ_0,EVAL ``dimword (:64)``] th 891 val th = SIMP_RULE std_ss [GSYM SPEC_MOVE_COND] th 892 val pre = ``k < LENGTH (stack:word64 list) /\ k < 268435456`` 893 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 894 val th = SPEC_FRAME_RULE th `` 895 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 896 cond (stack_ok rsp top base stack dm m /\ ^pre)`` 897 val th = RW1 [WORD_ADD_COMM] th 898 val (th,goal) = SPEC_WEAKEN_RULE th ``(zPC (p + 0x8w) * 899 zR 0x0w (EL k stack) * zSTACK (base,stack))`` 900 val lemma = prove(goal, 901 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 902 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 903 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 904 \\ IMP_RES_TAC stack_ok_EL_VAR 905 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 906 val th = MP th lemma 907 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 908 |> SIMP_RULE std_ss [SPEC_PRE_EXISTS] 909 val (th,goal) = SPEC_STRENGTHEN_RULE th 910 ``zPC p * zR 0x0w r0 * zSTACK (base,stack) * cond (^pre)`` 911 val lemma = prove(goal, 912 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 913 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 914 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 915 \\ IMP_RES_TAC stack_ok_EL_VAR 916 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 917 val th = MP th lemma 918 in th |> stack_ss end); 919 920val x64_lupdate_r0_imm = save_thm("x64_lupdate_r0_imm",let 921 val ((th,_,_),_) = x64_spec_memory64 "48898424" 922 val th = RW [GSYM IMM32_def] th 923 val th = Q.INST [`imm32`|->`n2w (8*k)`,`rip`|->`p`] th 924 val th = DISCH ``(k:num) < 2 ** 28`` th 925 val th = SIMP_RULE bool_ss [imm32_lemma] th 926 val lemma2 = prove( 927 ``k < 2 ** 28 ==> (8 * k) < 18446744073709551616n``, 928 FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC); 929 val th = RW1 [WORD_ADD_COMM] th |> RW [WORD_ADD_SUB] 930 val th = SIMP_RULE std_ss [lemma2,RW1 [MULT_COMM] MULT_DIV,w2n_n2w, 931 RW1 [MULT_COMM] MOD_EQ_0,EVAL ``dimword (:64)``] th 932 val th = SIMP_RULE std_ss [GSYM SPEC_MOVE_COND] th 933 val pre = ``k < LENGTH (stack:word64 list) /\ k < 268435456`` 934 val th = th |> Q.INST [`r4`|->`rsp`,`df`|->`dm`,`f`|->`m`,`rip`|->`p`] 935 val th = SPEC_FRAME_RULE th `` 936 zR1 zGhost_stack_top top * zR1 zGhost_stack_bottom base * 937 cond (stack_ok rsp top base stack dm m /\ ^pre)`` 938 val th = RW1 [WORD_ADD_COMM] th 939 val (th,goal) = SPEC_WEAKEN_RULE th ``(zPC (p + 0x8w) * 940 zR 0x0w r0 * zSTACK (base,LUPDATE r0 k stack))`` 941 val lemma = prove(goal, 942 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 943 \\ REPEAT STRIP_TAC 944 \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`(rsp + n2w (8 * k) =+ r0) m`] 945 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 946 \\ IMP_RES_TAC stack_ok_EL_VAR 947 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 948 val th = MP th lemma 949 val th = th |> Q.GENL [`rsp`,`top`,`dm`,`m`] 950 |> SIMP_RULE std_ss [SPEC_PRE_EXISTS] 951 val (th,goal) = SPEC_STRENGTHEN_RULE th 952 ``zPC p * zR 0x0w r0 * zSTACK (base,stack) * cond (^pre)`` 953 val lemma = prove(goal, 954 SIMP_TAC std_ss [SEP_IMP_def,zSTACK_def,SEP_CLAUSES,SEP_EXISTS_THM] 955 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`rsp`,`top`,`dm`,`m`] 956 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 957 \\ IMP_RES_TAC stack_ok_EL_VAR 958 \\ FULL_SIMP_TAC (std_ss++star_ss) [zR_def]) 959 val th = MP th lemma 960 in th |> stack_ss end); 961 962 963(* I/O interface to C: getchar, putchar *) 964 965val IO = 966 mk_var("IO",``:word64 # word8 list # word64 # word8 list -> x64_set -> bool``); 967 968(* 969 safe approximation of calling convention: 970 RBP, R12 -- R15 are callee saved 971 RAX -- R11 are caller saved 972*) 973 974val caller_saver_tm = 975 ``~zR1 RBX * ~zR1 RCX * ~zR1 RDX * ~zR1 RSI * 976 ~zR1 zR8 * ~zR1 zR9 * ~zR1 zR10 * ~zR1 zR11`` 977 978val callee_saved_tm = 979 ``zR1 zR12 r12 * zR1 zR13 r13 * zR1 zR14 r14 * zR1 zR15 r15`` 980 981val io_getchar_tm = 982 ``SPEC X64_MODEL 983 (zPC pi * ~zR1 RAX * ~zR1 RDI * ^caller_saver_tm * ^callee_saved_tm * 984 ^IO (pi,input,po,output) * ~zS * zSTACK (base,x::stack)) {} 985 (zPC x * zR1 RAX (HD (SNOC (~0w) (MAP w2w input))) * ~zR1 RDI * 986 ^caller_saver_tm * ^callee_saved_tm * 987 ^IO (pi,DROP 1 input,po,output) * ~zS * zSTACK (base,stack))``; 988 989val io_putchar_tm = 990 ``SPEC X64_MODEL 991 (zPC po * ~zR1 RAX * zR1 RDI (w2w c) * ^caller_saver_tm * ^callee_saved_tm * 992 ^IO (pi,input,po,output) * ~zS * zSTACK (base,x::stack)) {} 993 (zPC x * ~zR1 RAX * ~zR1 RDI * ^caller_saver_tm * ^callee_saved_tm * 994 ^IO (pi,input,po,output ++ [c]) * ~zS * zSTACK (base,stack))``; 995 996fun genall tm v = foldr mk_forall tm (filter (fn x => not (x = v)) (free_vars tm)); 997 998val IO_ASSUMS_def = Define ` 999 IO_ASSUMS ^IO = ^(genall io_getchar_tm IO) /\ ^(genall io_putchar_tm IO)` 1000 |> RW [STAR_ASSOC]; 1001 1002val zIO_def = Define ` 1003 zIO x = SEP_EXISTS IO. ^IO x * cond (IO_ASSUMS ^IO)`; 1004 1005val x64_putchar_thm = prove( 1006 io_putchar_tm |> subst [IO|->``zIO``], 1007 SIMP_TAC std_ss [zIO_def,SEP_CLAUSES] 1008 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ REPEAT STRIP_TAC 1009 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [SPEC_MOVE_COND,SEP_CLAUSES] 1010 \\ FULL_SIMP_TAC std_ss [IO_ASSUMS_def]) |> RW [STAR_ASSOC,GSYM zR_def]; 1011 1012val x64_getchar_thm = prove( 1013 io_getchar_tm |> subst [IO|->``zIO``], 1014 SIMP_TAC std_ss [zIO_def,SEP_CLAUSES] 1015 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ REPEAT STRIP_TAC 1016 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [SPEC_MOVE_COND,SEP_CLAUSES] 1017 \\ FULL_SIMP_TAC std_ss [IO_ASSUMS_def]) |> RW [STAR_ASSOC,GSYM zR_def]; 1018 1019val _ = save_thm("x64_getchar_thm",x64_getchar_thm); 1020val _ = save_thm("x64_putchar_thm",x64_putchar_thm); 1021 1022val _ = save_thm("x64_getchar_r1_thm", 1023 SPEC_COMPOSE_RULE [fetch "-" "x64_call_r1",x64_getchar_thm] |> RW [STAR_ASSOC]); 1024val _ = save_thm("x64_putchar_r1_thm", 1025 SPEC_COMPOSE_RULE [fetch "-" "x64_call_r1",x64_putchar_thm] |> RW [STAR_ASSOC]); 1026 1027val _ = export_theory(); 1028