1 2open HolKernel boolLib bossLib Parse; 3open wordsTheory bit_listTheory listTheory opmonTheory combinTheory; 4 5open x64_coretypesTheory; 6 7val _ = new_theory "x64_seq_monad"; 8 9val _ = type_abbrev("Zimm",``:word64``); 10 11val _ = Hol_datatype `x64_permission = Zread | Zwrite | Zexecute`; 12 13val _ = type_abbrev("x64_memory",``: word64 -> ((word8 # x64_permission set) option)``); 14 15val _ = type_abbrev("x64_state", (* state = tuple consisting of: *) 16 ``: (Zreg -> word64) # (* - general-purpose 32-bit registers *) 17 (word64) # (* - rip *) 18 (Zeflags -> bool option) # (* - eflags *) 19 x64_memory # (* - unsegmented memory *) 20 x64_memory (* - instruction cache *) ``); 21 22(* functions for reading/writing state *) 23 24val ZREAD_REG_def = Define `ZREAD_REG x ((r,p,s,m,i):x64_state) = r x `; 25val ZREAD_RIP_def = Define `ZREAD_RIP ((r,p,s,m,i):x64_state) = p `; 26val ZREAD_EFLAG_def = Define `ZREAD_EFLAG x ((r,p,s,m,i):x64_state) = s x `; 27 28val ZREAD_MEM_def = Define ` 29 ZREAD_MEM x ((r,p,s,m,i):x64_state) = 30 case m x of 31 NONE => NONE 32 | SOME (w,perms) => if Zread IN perms then SOME w else NONE`; 33 34val ZREAD_INSTR_def = Define ` 35 ZREAD_INSTR x ((r,p,s,m,i):x64_state) = 36 case (i x, m x) of 37 (NONE, NONE) => NONE 38 | (NONE, SOME (w,perms)) => if {Zread;Zexecute} SUBSET perms then SOME w else NONE 39 | (SOME (w,perms), _) => if {Zread;Zexecute} SUBSET perms then SOME w else NONE`; 40 41val X64_ICACHE_EMPTY_def = Define `X64_ICACHE_EMPTY = (\addr. NONE):x64_memory`; 42 43val ZCLEAR_ICACHE_def = Define ` 44 ZCLEAR_ICACHE ((r,p,s,m,i):x64_state) = (r,p,s,m,X64_ICACHE_EMPTY):x64_state`; 45 46val ZWRITE_REG_def = Define `ZWRITE_REG x y ((r,p,s,m,i):x64_state) = ((x =+ y) r,p,s,m,i):x64_state `; 47val ZWRITE_RIP_def = Define `ZWRITE_RIP y ((r,p,s,m,i):x64_state) = (r,y,s,m,i):x64_state `; 48val ZWRITE_EFLAG_def = Define `ZWRITE_EFLAG x y ((r,p,s,m,i):x64_state) = (r,p,(x =+ y) s,m,i):x64_state `; 49 50val ZWRITE_MEM_def = Define ` 51 ZWRITE_MEM x y ((r,p,s,m,i):x64_state) = 52 case m x of 53 NONE => NONE 54 | SOME (w,perms) => if Zwrite IN perms then SOME ((r,p,s,(x =+ SOME (y,perms)) m,i):x64_state) else NONE`; 55 56val ZREAD_MEM_BYTES_def = Define ` 57 ZREAD_MEM_BYTES n a s = 58 if n = 0 then [] else ZREAD_MEM a s :: ZREAD_MEM_BYTES (n-1) (a+1w) s`; 59 60val ZREAD_INSTR_BYTES_def = Define ` 61 ZREAD_INSTR_BYTES n a s = 62 if n = 0 then [] else ZREAD_INSTR a s :: ZREAD_INSTR_BYTES (n-1) (a+1w) s`; 63 64val w2bits_EL = store_thm("w2bits_EL", 65 ``(w2bits (w:word8) ++ ys = x1::x2::x3::x4::x5::x6::x7::x8::xs) = 66 (EL 0 (w2bits (w:word8)) = x1) /\ 67 (EL 1 (w2bits (w:word8)) = x2) /\ 68 (EL 2 (w2bits (w:word8)) = x3) /\ 69 (EL 3 (w2bits (w:word8)) = x4) /\ 70 (EL 4 (w2bits (w:word8)) = x5) /\ 71 (EL 5 (w2bits (w:word8)) = x6) /\ 72 (EL 6 (w2bits (w:word8)) = x7) /\ 73 (EL 7 (w2bits (w:word8)) = x8) /\ (ys = xs)``, 74 SIMP_TAC (std_ss++wordsLib.SIZES_ss) [w2bits_def] 75 THEN NTAC 9 (ONCE_REWRITE_TAC [n2bits_def] THEN SIMP_TAC std_ss [CONS_11]) 76 THEN SIMP_TAC std_ss [APPEND,CONS_11,EL,rich_listTheory.EL_CONS,HD]); 77 78val expand_mem_read_bytes = 79 (ONCE_REWRITE_CONV [ZREAD_MEM_BYTES_def,word2bytes_def] THENC 80 ONCE_REWRITE_CONV [ZREAD_MEM_BYTES_def,word2bytes_def] THENC 81 ONCE_REWRITE_CONV [ZREAD_MEM_BYTES_def,word2bytes_def] THENC 82 ONCE_REWRITE_CONV [ZREAD_MEM_BYTES_def,word2bytes_def] THENC 83 ONCE_REWRITE_CONV [ZREAD_MEM_BYTES_def,word2bytes_def] THENC 84 SIMP_CONV std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w,ASR_ADD]) 85 86val ZREAD_MEM_BYTES_thm = save_thm("ZREAD_MEM_BYTES_thm", 87 CONJ (expand_mem_read_bytes ``ZREAD_MEM_BYTES 1 a s``) 88 (CONJ (expand_mem_read_bytes ``ZREAD_MEM_BYTES 2 a s``) 89 (CONJ (expand_mem_read_bytes ``ZREAD_MEM_BYTES 4 a s``) 90 (expand_mem_read_bytes ``ZREAD_MEM_BYTES 8 a s``)))); 91 92val word2bytes_thm = save_thm("word2bytes_thm", 93 CONJ (expand_mem_read_bytes ``word2bytes 1 w``) 94 (CONJ (expand_mem_read_bytes ``word2bytes 2 w``) 95 (CONJ (expand_mem_read_bytes ``word2bytes 4 w``) 96 (expand_mem_read_bytes ``word2bytes 8 w``)))); 97 98val EL_thm = save_thm("EL_thm", 99 CONJ (EVAL ``EL 0 ((x0:'a)::xs)``) 100 (CONJ (EVAL ``EL 1 ((x0:'a)::x2::xs)``) 101 (CONJ (EVAL ``EL 2 ((x0:'a)::x2::x3::xs)``) 102 (CONJ (EVAL ``EL 3 ((x0:'a)::x2::x3::x4::xs)``) 103 (CONJ (EVAL ``EL 4 ((x0:'a)::x2::x3::x4::x5::xs)``) 104 (CONJ (EVAL ``EL 5 ((x0:'a)::x2::x3::x4::x5::x6::xs)``) 105 (CONJ (EVAL ``EL 6 ((x0:'a)::x2::x3::x4::x5::x6::x7::xs)``) 106 (EVAL ``EL 7 ((x0:'a)::x2::x3::x4::x5::x6::x7::x8::xs)``)))))))) 107 108 109(* ---------------------------------------------------------------------------------- *> 110 111 We define a state and monads for constructing a sequential version of the semantics. 112 113<* ---------------------------------------------------------------------------------- *) 114 115(* val _ = type_abbrev("Zstate",``:x64_state -> ('a # x64_state) option``); *) 116 117val _ = type_abbrev("x64_M",``:x64_state -> ('a # x64_state) option``); 118 119 120(* sequential monads for an option state *) 121 122val constT_seq_def = Define ` 123 (constT_seq: 'a -> 'a x64_M) x = \y. SOME (x,y)`; 124 125val addT_seq_def = Define ` 126 (addT_seq: 'a -> 'b x64_M -> ('a # 'b) x64_M) x s = 127 \y. case s y of NONE => NONE | SOME (z,t) => SOME ((x,z),t)`; 128 129val lockT_seq_def = Define ` 130 (lockT_seq: 'a x64_M -> 'a x64_M) s = s`; 131 132val failureT_seq_def = Define ` 133 (failureT_seq: 'a x64_M) = \y. NONE`; 134 135val seqT_seq_def = Define ` 136 (seqT_seq: 'a x64_M -> ('a -> 'b x64_M) -> 'b x64_M) s f = 137 \y. case s y of NONE => NONE | SOME (z,t) => f z t`; 138 139val parT_seq_def = Define ` 140 (parT_seq: 'a x64_M -> 'b x64_M -> ('a # 'b) x64_M) s t = 141 \y. case s y of NONE => NONE | SOME (a,z) => 142 case t z of NONE => NONE | SOME (b,x) => SOME ((a,b),x)`; 143 144val parT_unit_seq_def = Define ` 145 (parT_unit_seq: unit x64_M -> unit x64_M -> unit x64_M) s t = 146 \y. case s y of NONE => NONE | SOME (a,z) => 147 case t z of NONE => NONE | SOME (b,x) => SOME ((),x)`; 148 149(* register reads/writes always succeed. *) 150 151val write_reg_seq_def = Define `(write_reg_seq ii r x):unit x64_M = 152 \s. SOME ((),ZWRITE_REG r x s)`; 153 154val read_reg_seq_def = Define `(read_reg_seq ii r):word64 x64_M = 155 \s. SOME (ZREAD_REG r s,s)`; 156 157(* eflags can always be written, but reading a NONE eflag causes a failure *) 158 159val write_eflag_seq_def = Define `(write_eflag_seq ii f x):unit x64_M = 160 (\s. SOME ((),ZWRITE_EFLAG f x s))`; 161 162val read_eflag_seq_def = Define `(read_eflag_seq ii f):bool x64_M = 163 (\s. case ZREAD_EFLAG f s of NONE => NONE | SOME b => SOME (b,s))`; 164 165(* rip reads/writes always succeed. *) 166 167val write_rip_seq_def = Define `(write_rip_seq ii x):unit x64_M = 168 \s. SOME ((),ZWRITE_RIP x s)`; 169 170val read_rip_seq_def = Define `(read_rip_seq ii):Zimm x64_M = 171 \s. SOME (ZREAD_RIP s,s)`; 172 173(* memory writes are only allowed to modelled memory, i.e. locations containing SOME ... *) 174 175val write_mem_seq_def = Define `(write_mem_seq ii a x):unit x64_M = 176 (\s. case ZWRITE_MEM a x s of NONE => NONE | SOME s2 => SOME ((),s2))`; 177 178(* a memory read to an unmodelled memory location causes a failure *) 179 180val read_mem_seq_def = Define `(read_mem_seq ii a):word8 x64_M = 181 (\s. case ZREAD_MEM a s of NONE => NONE | SOME x => SOME (x,s))`; 182 183(* reading and writing from/to memory *) 184 185val read_m8_seq_def = Define `(read_m8_seq ii a):word8 x64_M = 186 read_mem_seq ii a`; 187 188val read_m16_seq_def = Define `(read_m16_seq ii a):word16 x64_M = 189 seqT_seq (parT_seq (read_mem_seq ii (a+0w)) (read_mem_seq ii (a+1w))) 190 (\(x0,x1). constT_seq (bytes2word [x0;x1]))`; 191 192val read_m32_seq_def = Define `(read_m32_seq ii a):word32 x64_M = 193 seqT_seq (parT_seq (read_mem_seq ii (a+0w)) 194 (parT_seq (read_mem_seq ii (a+1w)) 195 (parT_seq (read_mem_seq ii (a+2w)) 196 (read_mem_seq ii (a+3w))))) 197 (\(x0,x1,x2,x3). constT_seq (bytes2word [x0;x1;x2;x3]))`; 198 199val read_m64_seq_def = Define `(read_m64_seq ii a):word64 x64_M = 200 seqT_seq (parT_seq (read_mem_seq ii (a+0w)) 201 (parT_seq (read_mem_seq ii (a+1w)) 202 (parT_seq (read_mem_seq ii (a+2w)) 203 (parT_seq (read_mem_seq ii (a+3w)) 204 (parT_seq (read_mem_seq ii (a+4w)) 205 (parT_seq (read_mem_seq ii (a+5w)) 206 (parT_seq (read_mem_seq ii (a+6w)) 207 (read_mem_seq ii (a+7w))))))))) 208 (\(x0,x1,x2,x3,x4,x5,x6,x7). constT_seq (bytes2word [x0;x1;x2;x3;x4;x5;x6;x7]))`; 209 210 211val write_m8_seq_def = Define `(write_m8_seq ii a w):unit x64_M = 212 write_mem_seq ii a (w:word8)`; 213 214val write_m16_seq_def = Define `(write_m16_seq ii a w):unit x64_M = 215 (let bs = word2bytes 2 (w:word16) in 216 parT_unit_seq (write_mem_seq ii (a+0w) (EL 0 bs)) 217 (write_mem_seq ii (a+1w) (EL 1 bs)))`; 218 219val write_m32_seq_def = Define `(write_m32_seq ii a w):unit x64_M = 220 (let bs = word2bytes 4 (w:word32) in 221 parT_unit_seq (write_mem_seq ii (a+0w) (EL 0 bs)) 222 (parT_unit_seq (write_mem_seq ii (a+1w) (EL 1 bs)) 223 (parT_unit_seq (write_mem_seq ii (a+2w) (EL 2 bs)) 224 (write_mem_seq ii (a+3w) (EL 3 bs)))))`; 225 226val write_m64_seq_def = Define `(write_m64_seq ii a w):unit x64_M = 227 (let bs = word2bytes 8 (w:word64) in 228 parT_unit_seq (write_mem_seq ii (a+0w) (EL 0 bs)) 229 (parT_unit_seq (write_mem_seq ii (a+1w) (EL 1 bs)) 230 (parT_unit_seq (write_mem_seq ii (a+2w) (EL 2 bs)) 231 (parT_unit_seq (write_mem_seq ii (a+3w) (EL 3 bs)) 232 (parT_unit_seq (write_mem_seq ii (a+4w) (EL 4 bs)) 233 (parT_unit_seq (write_mem_seq ii (a+5w) (EL 5 bs)) 234 (parT_unit_seq (write_mem_seq ii (a+6w) (EL 6 bs)) 235 (write_mem_seq ii (a+7w) (EL 7 bs)))))))))`; 236 237(* clear the icache *) 238 239val clear_icache_seq_def = Define `(clear_icache_seq ii):unit x64_M = 240 \s. SOME ((),ZCLEAR_ICACHE s)`; 241 242 243(* export *) 244 245val _ = Define `(constT: 'a -> 'a x64_M) = constT_seq`; 246val _ = Define `(addT: 'a -> 'b x64_M -> ('a # 'b) x64_M) = addT_seq`; 247val _ = Define `(lockT: unit x64_M -> unit x64_M) = lockT_seq`; 248val _ = Define `(failureT: unit x64_M) = failureT_seq`; 249val _ = Define `(seqT: 'a x64_M -> (('a -> 'b x64_M) -> 'b x64_M)) = seqT_seq`; 250val _ = Define `(parT: 'a x64_M -> 'b x64_M -> ('a # 'b) x64_M) = parT_seq`; 251val _ = Define `(parT_unit: unit x64_M -> unit x64_M -> unit x64_M) = parT_unit_seq`; 252val _ = Define `(write_reg: iiid -> Zreg -> Zimm -> unit x64_M) = write_reg_seq`; 253val _ = Define `(read_reg: iiid -> Zreg -> Zimm x64_M) = read_reg_seq`; 254val _ = Define `(write_rip: iiid -> Zimm -> unit x64_M) = write_rip_seq`; 255val _ = Define `(read_rip: iiid -> Zimm x64_M) = read_rip_seq`; 256val _ = Define `(write_eflag: iiid -> Zeflags -> bool option -> unit x64_M) = write_eflag_seq`; 257val _ = Define `(read_eflag: iiid -> Zeflags -> bool x64_M) = read_eflag_seq`; 258val _ = Define `(write_m8: iiid -> word64 -> word8 -> unit x64_M) = write_m8_seq`; 259val _ = Define `(read_m8: iiid -> word64 -> word8 x64_M) = read_m8_seq`; 260val _ = Define `(write_m16: iiid -> word64 -> word16 -> unit x64_M) = write_m16_seq`; 261val _ = Define `(read_m16: iiid -> word64 -> word16 x64_M) = read_m16_seq`; 262val _ = Define `(write_m32: iiid -> word64 -> word32 -> unit x64_M) = write_m32_seq`; 263val _ = Define `(read_m32: iiid -> word64 -> word32 x64_M) = read_m32_seq`; 264val _ = Define `(write_m64: iiid -> word64 -> word64 -> unit x64_M) = write_m64_seq`; 265val _ = Define `(read_m64: iiid -> word64 -> word64 x64_M) = read_m64_seq`; 266val _ = Define `(clear_icache: iiid -> unit x64_M) = clear_icache_seq`; 267 268 269 270(* some rewriter-friendly theorems *) 271 272val option_apply_def = Define ` 273 option_apply x f = if x = NONE then NONE else f (THE x)`; 274 275val option_apply_SOME = prove( 276 ``!x f. option_apply (SOME x) f = f x``,SRW_TAC [] [option_apply_def]); 277 278val ZWRITE_MEM2_def = Define ` 279 ZWRITE_MEM2 a w ((r,e,s,m,i):x64_state) = (r,e,s,(a =+ SOME (w, SND (THE (m a)))) m,i)`; 280 281val ZREAD_MEM2_def = Define ` 282 ZREAD_MEM2 a ((r,e,s,m,i):x64_state) = FST (THE (m a))`; 283 284val ZREAD_MEM2_WORD16_def = Define ` 285 ZREAD_MEM2_WORD16 a (s:x64_state) = (bytes2word 286 [ZREAD_MEM2 (a + 0x0w) s; ZREAD_MEM2 (a + 0x1w) s]) :word16`; 287 288val ZREAD_MEM2_WORD32_def = Define ` 289 ZREAD_MEM2_WORD32 a (s:x64_state) = (bytes2word 290 [ZREAD_MEM2 (a + 0x0w) s; ZREAD_MEM2 (a + 0x1w) s; 291 ZREAD_MEM2 (a + 0x2w) s; ZREAD_MEM2 (a + 0x3w) s]) :word32`; 292 293val ZREAD_MEM2_WORD64_def = Define ` 294 ZREAD_MEM2_WORD64 a (s:x64_state) = (bytes2word 295 [ZREAD_MEM2 (a + 0x0w) s; ZREAD_MEM2 (a + 0x1w) s; 296 ZREAD_MEM2 (a + 0x2w) s; ZREAD_MEM2 (a + 0x3w) s; 297 ZREAD_MEM2 (a + 0x4w) s; ZREAD_MEM2 (a + 0x5w) s; 298 ZREAD_MEM2 (a + 0x6w) s; ZREAD_MEM2 (a + 0x7w) s]) :word64`; 299 300val ZWRITE_MEM2_WORD16_def = Define ` 301 ZWRITE_MEM2_WORD16 a (w:word16) (s:x64_state) = 302 ZWRITE_MEM2 (a + 1w) (EL 1 (word2bytes 2 w)) 303 (ZWRITE_MEM2 (a + 0w) (EL 0 (word2bytes 2 w)) s)`; 304 305val ZWRITE_MEM2_WORD32_def = Define ` 306 ZWRITE_MEM2_WORD32 a (w:word32) (s:x64_state) = 307 ZWRITE_MEM2 (a + 3w) (EL 3 (word2bytes 4 w)) 308 (ZWRITE_MEM2 (a + 2w) (EL 2 (word2bytes 4 w)) 309 (ZWRITE_MEM2 (a + 1w) (EL 1 (word2bytes 4 w)) 310 (ZWRITE_MEM2 (a + 0w) (EL 0 (word2bytes 4 w)) s)))`; 311 312val ZWRITE_MEM2_WORD64_def = Define ` 313 ZWRITE_MEM2_WORD64 a (w:word64) (s:x64_state) = 314 ZWRITE_MEM2 (a + 7w) (EL 7 (word2bytes 8 w)) 315 (ZWRITE_MEM2 (a + 6w) (EL 6 (word2bytes 8 w)) 316 (ZWRITE_MEM2 (a + 5w) (EL 5 (word2bytes 8 w)) 317 (ZWRITE_MEM2 (a + 4w) (EL 4 (word2bytes 8 w)) 318 (ZWRITE_MEM2 (a + 3w) (EL 3 (word2bytes 8 w)) 319 (ZWRITE_MEM2 (a + 2w) (EL 2 (word2bytes 8 w)) 320 (ZWRITE_MEM2 (a + 1w) (EL 1 (word2bytes 8 w)) 321 (ZWRITE_MEM2 (a + 0w) (EL 0 (word2bytes 8 w)) s)))))))`; 322 323val ZREAD_MEM2_WORD64_THM = store_thm("ZREAD_MEM2_WORD64_THM", 324 ``ZREAD_MEM2_WORD64 a (s:x64_state) = 325 (w2w (ZREAD_MEM2_WORD32 (a + 4w) s) << 32) !! w2w (ZREAD_MEM2_WORD32 a s)``, 326 SIMP_TAC std_ss [ZREAD_MEM2_WORD32_def,ZREAD_MEM2_WORD64_def,bytes2word_def] 327 THEN ASM_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w] 328 THEN SIMP_TAC (std_ss++wordsLib.WORD_SHIFT_ss) [GSYM LSL_BITWISE] 329 THEN SIMP_TAC (std_ss++wordsLib.WORD_EXTRACT_ss++wordsLib.SIZES_ss) [WORD_OR_CLAUSES] 330 THEN SIMP_TAC (std_ss++wordsLib.WORD_SHIFT_ss) [GSYM LSL_BITWISE] 331 THEN SIMP_TAC std_ss [AC WORD_OR_ASSOC WORD_OR_COMM]); 332 333val ZWRITE_MEM2_WORD64_THM = store_thm("ZWRITE_MEM2_WORD64_THM", 334 ``ZWRITE_MEM2_WORD64 a (w:word64) (s:x64_state) = 335 ZWRITE_MEM2_WORD32 (a + 4w) ((63 >< 32) w) 336 (ZWRITE_MEM2_WORD32 (a + 0w) ((31 >< 0) w) s)``, 337 SIMP_TAC std_ss [ZWRITE_MEM2_WORD32_def,ZWRITE_MEM2_WORD64_def] 338 THEN NTAC 8 (ONCE_REWRITE_TAC [word2bytes_def] THEN SIMP_TAC std_ss [EL_thm]) 339 THEN ASM_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w] 340 THEN SIMP_TAC (std_ss++wordsLib.WORD_SHIFT_ss) [] 341 THEN SIMP_TAC (std_ss++wordsLib.WORD_EXTRACT_ss++wordsLib.SIZES_ss) [WORD_OR_CLAUSES]); 342 343val CAN_ZWRITE_MEM_def = Define ` 344 CAN_ZWRITE_MEM a s = !w. ~(ZWRITE_MEM a w s = NONE)`; 345 346val CAN_ZREAD_MEM_def = Define ` 347 CAN_ZREAD_MEM a s = ~(ZREAD_MEM a s = NONE)`; 348 349val mem_seq_lemma = prove( 350 ``(read_mem_seq ii a s = option_apply (ZREAD_MEM a s) (\x. SOME (x,s))) /\ 351 (write_mem_seq ii a y s = option_apply (ZWRITE_MEM a y s) (\s. SOME ((),s)))``, 352 SRW_TAC [] [option_apply_def,read_mem_seq_def,write_mem_seq_def] 353 THEN Cases_on `ZREAD_MEM a s` THEN FULL_SIMP_TAC std_ss [] 354 THEN Cases_on `ZWRITE_MEM a y s` THEN FULL_SIMP_TAC std_ss []); 355 356val read_eflag_seq_lemma = prove( 357 ``read_eflag_seq ii f s = option_apply (ZREAD_EFLAG f s) (\x. SOME (x,s))``, 358 SRW_TAC [] [option_apply_def,read_eflag_seq_def] 359 THEN Cases_on `ZREAD_EFLAG f s` THEN FULL_SIMP_TAC std_ss []); 360 361val parT_unit_seq_lemma = prove( 362 ``(parT_unit_seq s t = \y. option_apply (s y) (\z. 363 option_apply (t (SND z)) (\x. SOME ((),SND x))))``, 364 SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `s y` 365 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `x` 366 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] 367 THEN FULL_SIMP_TAC std_ss [] THEN Cases_on `t r` 368 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `x` 369 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def]); 370 371val monad_simp_lemma = prove( 372 ``(constT_seq x = \y. SOME (x,y)) /\ (failureT_seq = \y. NONE) /\ (lockT_seq d = d) /\ 373 (addT_seq q s = \y. option_apply (s y) (\t. SOME ((q,FST t),SND t))) /\ 374 (seqT_seq s f = \y. option_apply (s y) (\t. f (FST t) (SND t))) /\ 375 (parT_seq s t = \y. option_apply (s y) (\z. 376 option_apply (t (SND z)) (\x. SOME ((FST z,FST x),SND x))))``, 377 SRW_TAC [] [parT_seq_def,seqT_seq_def,failureT_seq_def,lockT_seq_def, 378 addT_seq_def,constT_seq_def,FUN_EQ_THM] 379 THEN Cases_on `s y` THEN POP_ASSUM MP_TAC THEN SRW_TAC [] [option_apply_def] 380 THEN Cases_on `x` THEN POP_ASSUM MP_TAC THEN SRW_TAC [] [option_apply_def] 381 THEN Cases_on `t r` THEN SRW_TAC [] [option_apply_def] THEN FULL_SIMP_TAC std_ss [] 382 THEN Cases_on `x` THEN SRW_TAC [] [option_apply_def]); 383 384val seq_monad_thm = save_thm("seq_monad_thm",let 385 val xs = option_apply_SOME :: mem_seq_lemma :: read_eflag_seq_lemma :: 386 parT_unit_seq_lemma :: (CONJUNCTS monad_simp_lemma) 387 in LIST_CONJ (map GEN_ALL xs) end); 388 389val CAN_ZWRITE_MEM = store_thm("CAN_ZWRITE_MEM", 390 ``CAN_ZWRITE_MEM a (r,e,s,m,i) = 391 ~(m a = NONE) /\ Zwrite IN SND (THE (m a))``, 392 SIMP_TAC std_ss [ZWRITE_MEM_def,CAN_ZWRITE_MEM_def] 393 THEN Cases_on `m a` THEN ASM_SIMP_TAC std_ss [] THEN SRW_TAC [] [] 394 THEN Cases_on `x` THEN Cases_on `Zwrite IN r'` THEN SRW_TAC [] []); 395 396val CAN_ZREAD_MEM = store_thm("CAN_ZREAD_MEM", 397 ``CAN_ZREAD_MEM a (r,e,s,m,i) = 398 ~(m a = NONE) /\ Zread IN SND (THE (m a))``, 399 SIMP_TAC std_ss [ZREAD_MEM_def,CAN_ZREAD_MEM_def] 400 THEN Cases_on `m a` THEN ASM_SIMP_TAC std_ss [] THEN SRW_TAC [] [] 401 THEN Cases_on `x` THEN SRW_TAC [] []); 402 403val CAN_ZREAD_ZWRITE_THM = store_thm("CAN_ZREAD_ZWRITE_THM", 404 ``!s. (CAN_ZWRITE_MEM a s ==> CAN_ZWRITE_MEM a (ZWRITE_REG r2 w s)) /\ 405 (CAN_ZWRITE_MEM a s ==> CAN_ZWRITE_MEM a (ZWRITE_RIP e s)) /\ 406 (CAN_ZWRITE_MEM a s ==> CAN_ZWRITE_MEM a (ZWRITE_EFLAG f b s)) /\ 407 (CAN_ZWRITE_MEM a s ==> CAN_ZWRITE_MEM a (ZCLEAR_ICACHE s)) /\ 408 (CAN_ZWRITE_MEM a s ==> CAN_ZWRITE_MEM a (ZWRITE_MEM2 c x s)) /\ 409 (CAN_ZREAD_MEM a s ==> CAN_ZREAD_MEM a (ZWRITE_REG r2 w s)) /\ 410 (CAN_ZREAD_MEM a s ==> CAN_ZREAD_MEM a (ZWRITE_RIP e s)) /\ 411 (CAN_ZREAD_MEM a s ==> CAN_ZREAD_MEM a (ZWRITE_EFLAG f b s)) /\ 412 (CAN_ZREAD_MEM a s ==> CAN_ZREAD_MEM a (ZCLEAR_ICACHE s)) /\ 413 (CAN_ZREAD_MEM a s /\ CAN_ZWRITE_MEM c s ==> CAN_ZREAD_MEM a (ZWRITE_MEM2 c x s))``, 414 STRIP_TAC THEN `?r2 e2 s2 m2 i2. s = (r2,e2,s2,m2,i2)` by METIS_TAC [pairTheory.PAIR] 415 THEN ASM_SIMP_TAC std_ss [ZREAD_REG_def,ZREAD_RIP_def, 416 ZREAD_EFLAG_def, ZWRITE_REG_def, ZWRITE_MEM2_def, ZREAD_MEM2_def, 417 combinTheory.APPLY_UPDATE_THM, ZWRITE_RIP_def,CAN_ZREAD_MEM, 418 ZWRITE_EFLAG_def,ZCLEAR_ICACHE_def,CAN_ZWRITE_MEM] 419 THEN Cases_on `c = a` THEN ASM_SIMP_TAC std_ss []); 420 421val x64_else_none_write_mem_lemma = store_thm("x64_else_none_write_mem_lemma", 422 ``!a x t f. CAN_ZWRITE_MEM a t ==> 423 (option_apply (ZWRITE_MEM a x t) f = f (ZWRITE_MEM2 a x t))``, 424 REPEAT STRIP_TAC 425 THEN `?r e s m i. t = (r,e,s,m,i)` by METIS_TAC [pairTheory.PAIR] 426 THEN FULL_SIMP_TAC std_ss [CAN_ZWRITE_MEM,ZWRITE_MEM_def,ZWRITE_MEM2_def] 427 THEN Cases_on `m a` THEN FULL_SIMP_TAC std_ss [] 428 THEN Cases_on `x'` THEN FULL_SIMP_TAC (srw_ss()) [] 429 THEN SRW_TAC [] [option_apply_def]); 430 431val x64_else_none_read_mem_lemma = store_thm("x64_else_none_read_mem_lemma", 432 ``!a x t f. CAN_ZREAD_MEM a t ==> 433 (option_apply (ZREAD_MEM a t) f = f (ZREAD_MEM2 a t))``, 434 REPEAT STRIP_TAC 435 THEN `?r e s m i. t = (r,e,s,m,i)` by METIS_TAC [pairTheory.PAIR] 436 THEN FULL_SIMP_TAC std_ss [CAN_ZREAD_MEM,ZREAD_MEM2_def,ZREAD_MEM_def] 437 THEN Cases_on `m a` THEN FULL_SIMP_TAC std_ss [] 438 THEN Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] 439 THEN SRW_TAC [] [option_apply_def]); 440 441val x64_else_none_eflag_lemma = store_thm("x64_else_none_eflag_lemma", 442 ``!m a f. ~(m a = NONE) ==> 443 (option_apply ((m:x64_state->bool option) a) (f:bool->'a option) = f (THE (m a)))``, 444 SIMP_TAC std_ss [option_apply_def]); 445 446val x64_state_EXPAND = store_thm("x64_state_EXPAND", 447 ``?r p f t m i. s:x64_state = (r,p,f,m,i)``, 448 Q.SPEC_TAC (`s`,`s`) THEN SIMP_TAC std_ss [pairTheory.FORALL_PROD]); 449 450val ZREAD_RIP_ADD_0 = store_thm("ZREAD_RIP_ADD_0", 451 ``ZREAD_MEM (ZREAD_RIP s) s = ZREAD_MEM (ZREAD_RIP s + 0w) s``, 452 REWRITE_TAC [WORD_ADD_0]); 453 454val x64_address_lemma = save_thm("x64_address_lemma", 455 SIMP_RULE std_ss [listTheory.ALL_DISTINCT,MEM,GSYM CONJ_ASSOC] 456 (EVAL ``ALL_DISTINCT [0w;1w;2w;3w;4w;5w;6w;7w:word64]``)); 457 458val _ = export_theory (); 459