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