1 2open HolKernel boolLib bossLib Parse; 3open wordsTheory bit_listTheory listTheory opmonTheory; 4 5open ppc_coretypesTheory; 6 7val _ = new_theory "ppc_seq_monad"; 8 9 10(* state *) 11 12val _ = type_abbrev("ppc_state", 13 ``:(ppc_reg -> word32) # (ppc_bit -> bool option) # (word32 -> word8 option)``); 14 (* tuple consists of registers, status bits and byte-addressed memory *) 15 16(* functions for reading/writing state *) 17 18val PREAD_R_def = Define `PREAD_R rd ((r,s,m):ppc_state) = r rd`; 19val PREAD_S_def = Define `PREAD_S rd ((r,s,m):ppc_state) = s rd`; 20val PREAD_M_def = Define `PREAD_M rd ((r,s,m):ppc_state) = m rd`; 21 22val PWRITE_R_def = Define `PWRITE_R rd x (r,s,m) = ((rd =+ x) r,s,m):ppc_state`; 23val PWRITE_S_def = Define `PWRITE_S rd x (r,s,m) = (r,(rd =+ x) s,m):ppc_state`; 24val PWRITE_M_def = Define `PWRITE_M rd x (r,s,m) = (r,s,(rd =+ x) m):ppc_state`; 25 26 27 28(* ---------------------------------------------------------------------------------- *> 29 30 We define a state and monads for constructing a sequential version of the semantics. 31 32<* ---------------------------------------------------------------------------------- *) 33 34val _ = type_abbrev("ppc_M",``:ppc_state -> ('a # ppc_state) option``); 35 36 37(* sequential monads for an option state *) 38 39val constT_seq_def = Define ` 40 (constT_seq: 'a -> 'a ppc_M) x = \y. SOME (x,y)`; 41 42val addT_seq_def = Define ` 43 (addT_seq: 'a -> 'b ppc_M -> ('a # 'b) ppc_M) x s = 44 \y. case s y of NONE => NONE | SOME (z,t) => SOME ((x,z),t)`; 45 46val lockT_seq_def = Define ` 47 (lockT_seq: 'a ppc_M -> 'a ppc_M) s = s`; 48 49val failureT_seq_def = Define ` 50 (failureT_seq: 'a ppc_M) = \y. NONE`; 51 52val seqT_seq_def = Define ` 53 (seqT_seq: 'a ppc_M -> ('a -> 'b ppc_M) -> 'b ppc_M) s f = 54 \y. case s y of NONE => NONE | SOME (z,t) => f z t`; 55 56val parT_seq_def = Define ` 57 (parT_seq: 'a ppc_M -> 'b ppc_M -> ('a # 'b) ppc_M) s t = 58 \y. case s y of NONE => NONE | SOME (a,z) => 59 case t z of NONE => NONE | SOME (b,x) => SOME ((a,b),x)`; 60 61val parT_unit_seq_def = Define ` 62 (parT_unit_seq: unit ppc_M -> unit ppc_M -> unit ppc_M) s t = 63 \y. case s y of NONE => NONE | SOME (a,z) => 64 case t z of NONE => NONE | SOME (b,x) => SOME ((),x)`; 65 66(* register reads/writes always succeed. *) 67 68val write_reg_seq_def = Define `(write_reg_seq ii r x):unit ppc_M = 69 \s. SOME ((),PWRITE_R r x s)`; 70 71val read_reg_seq_def = Define `(read_reg_seq ii r):word32 ppc_M = 72 \s. SOME (PREAD_R r s,s)`; 73 74(* eflags can always be written, but reading a NONE status bit causes a failure *) 75 76val write_status_seq_def = Define `(write_status_seq ii f x):unit ppc_M = 77 (\s. SOME ((),PWRITE_S f x s))`; 78 79val read_status_seq_def = Define `(read_status_seq ii f):bool ppc_M = 80 (\s. case PREAD_S f s of NONE => NONE | SOME b => SOME (b,s))`; 81 82(* memory writes are only allowed to modelled memory, i.e. locations containing SOME ... *) 83 84val write_mem_seq_def = Define `(write_mem_seq ii a x):unit ppc_M = 85 (\s. case PREAD_M a s of NONE => NONE | SOME y => SOME ((),PWRITE_M a (SOME x) s))`; 86 87(* a memory read to an unmodelled memory location causes a failure *) 88 89val read_mem_seq_def = Define `(read_mem_seq ii a):word8 ppc_M = 90 (\s. case PREAD_M a s of NONE => NONE | SOME x => SOME (x,s))`; 91 92 93(* export *) 94 95val _ = Define `(constT: 'a -> 'a ppc_M) = constT_seq`; 96val _ = Define `(addT: 'a -> 'b ppc_M -> ('a # 'b) ppc_M) = addT_seq`; 97val _ = Define `(lockT: unit ppc_M -> unit ppc_M) = lockT_seq`; 98val _ = Define `(failureT: unit ppc_M) = failureT_seq`; 99val _ = Define `(seqT: 'a ppc_M -> (('a -> 'b ppc_M) -> 'b ppc_M)) = seqT_seq`; 100val _ = Define `(parT: 'a ppc_M -> 'b ppc_M -> ('a # 'b) ppc_M) = parT_seq`; 101val _ = Define `(parT_unit: unit ppc_M -> unit ppc_M -> unit ppc_M) = parT_unit_seq`; 102val _ = Define `(write_reg: iiid -> ppc_reg -> word32 -> unit ppc_M) = write_reg_seq`; 103val _ = Define `(read_reg: iiid -> ppc_reg -> word32 ppc_M) = read_reg_seq`; 104val _ = Define `(write_status: iiid -> ppc_bit -> bool option -> unit ppc_M) = write_status_seq`; 105val _ = Define `(read_status: iiid -> ppc_bit -> bool ppc_M) = read_status_seq`; 106val _ = Define `(write_mem: iiid -> word32 -> word8 -> unit ppc_M) = write_mem_seq`; 107val _ = Define `(read_mem: iiid -> word32 -> word8 ppc_M) = read_mem_seq`; 108 109 110 111(* some rewriter-friendly theorems *) 112 113val mem_seq_lemma = prove( 114 ``(read_mem_seq ii a s = option_apply (PREAD_M a s) (\x. SOME (x,s))) /\ 115 (write_mem_seq ii a y s = option_apply (PREAD_M a s) (\x. SOME ((),PWRITE_M a (SOME y) s)))``, 116 SRW_TAC [] [option_apply_def,read_mem_seq_def,write_mem_seq_def] 117 THEN Cases_on `PREAD_M a s` THEN FULL_SIMP_TAC std_ss []); 118 119val read_status_seq_lemma = prove( 120 ``read_status_seq ii f s = option_apply (PREAD_S f s) (\x. SOME (x,s))``, 121 SRW_TAC [] [option_apply_def,read_status_seq_def] 122 THEN Cases_on `PREAD_S f s` THEN FULL_SIMP_TAC std_ss []); 123 124val parT_unit_seq_lemma = prove( 125 ``(parT_unit_seq s t = \y. option_apply (s y) (\z. 126 option_apply (t (SND z)) (\x. SOME ((),SND x))))``, 127 SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `s y` 128 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `x` 129 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] 130 THEN FULL_SIMP_TAC std_ss [] THEN Cases_on `t r` 131 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `x` 132 THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def]); 133 134val monad_simp_lemma = prove( 135 ``(constT_seq x = \y. SOME (x,y)) /\ (failureT_seq = \y. NONE) /\ (lockT_seq d = d) /\ 136 (addT_seq q s = \y. option_apply (s y) (\t. SOME ((q,FST t),SND t))) /\ 137 (seqT_seq s f = \y. option_apply (s y) (\t. f (FST t) (SND t))) /\ 138 (parT_seq s t = \y. option_apply (s y) (\z. 139 option_apply (t (SND z)) (\x. SOME ((FST z,FST x),SND x))))``, 140 SRW_TAC [] [parT_seq_def,seqT_seq_def,failureT_seq_def,lockT_seq_def, 141 addT_seq_def,constT_seq_def,FUN_EQ_THM] 142 THEN Cases_on `s y` THEN POP_ASSUM MP_TAC THEN SRW_TAC [] [option_apply_def] 143 THEN Cases_on `x` THEN POP_ASSUM MP_TAC THEN SRW_TAC [] [option_apply_def] 144 THEN Cases_on `t r` THEN SRW_TAC [] [option_apply_def] THEN FULL_SIMP_TAC std_ss [] 145 THEN Cases_on `x` THEN SRW_TAC [] [option_apply_def]); 146 147val seq_monad_thm = save_thm("seq_monad_thm",let 148 val xs = option_apply_SOME :: mem_seq_lemma :: read_status_seq_lemma :: 149 parT_unit_seq_lemma :: (CONJUNCTS monad_simp_lemma) 150 in LIST_CONJ (map GEN_ALL xs) end); 151 152val PREAD_CLAUSES = store_thm("PREAD_CLAUSES", 153 ``!s. (PREAD_R r (PWRITE_M a x s) = PREAD_R r s) /\ 154 (PREAD_R r (PWRITE_S f b s) = PREAD_R r s) /\ 155 (PREAD_M a (PWRITE_R r w s) = PREAD_M a s) /\ 156 (PREAD_M a (PWRITE_S f b s) = PREAD_M a s) /\ 157 (PREAD_S f (PWRITE_R r w s) = PREAD_S f s) /\ 158 (PREAD_S f (PWRITE_M a x s) = PREAD_S f s) /\ 159 (PREAD_R r (PWRITE_R r2 w s) = if r = r2 then w else PREAD_R r s) /\ 160 (PREAD_M a (PWRITE_M a2 x s) = if a = a2 then x else PREAD_M a s) /\ 161 (PREAD_S f (PWRITE_S f2 b s) = if f = f2 then b else PREAD_S f s)``, 162 Cases THEN Cases_on `r'` THEN SRW_TAC [] [PREAD_R_def,PREAD_M_def,PREAD_S_def, 163 PWRITE_M_def,PWRITE_R_def,PWRITE_S_def, combinTheory.APPLY_UPDATE_THM]); 164 165val ppc_else_none_mem_lemma = store_thm("ppc_else_none_mem_lemma", 166 ``!m a f. ~(m a = NONE) ==> 167 (option_apply ((m:ppc_state->word8 option) a) (f:word8->'a option) = f (THE (m a)))``, 168 SIMP_TAC std_ss [option_apply_def]); 169 170val ppc_else_none_status_lemma = store_thm("ppc_else_none_status_lemma", 171 ``!m a f. ~(m a = NONE) ==> 172 (option_apply ((m:ppc_state->bool option) a) (f:bool->'a option) = f (THE (m a)))``, 173 SIMP_TAC std_ss [option_apply_def]); 174 175val _ = export_theory (); 176