1(* ------------------------------------------------------------------------ 2 Definitions and theorems used by CHERI/MIPS step evaluator (cheri_stepLib) 3 ------------------------------------------------------------------------ *) 4 5open HolKernel boolLib bossLib 6 7open utilsLib 8open wordsLib blastLib alignmentTheory 9open updateTheory cheriTheory 10 11val _ = new_theory "cheri_step" 12val _ = ParseExtras.temp_loose_equality() 13val _ = List.app (fn f => f ()) 14 [numLib.prefer_num, wordsLib.prefer_word, wordsLib.guess_lengths] 15 16(* ------------------------------------------------------------------------ *) 17 18(* Next state theorems *) 19 20val NextStateCHERI_def = Define` 21 NextStateCHERI s0 = 22 let s1 = Next s0 in if s1.exception = NoException then SOME s1 else NONE` 23 24val exceptionSignalled_id = Q.prove( 25 `!s. ~exceptionSignalled s ==> 26 (s with c_state := s.c_state with c_exceptionSignalled := F = s)`, 27 lrw [exceptionSignalled_def, cheri_state_component_equality, 28 procState_component_equality]) 29 30val tac = 31 lrw [NextStateCHERI_def, Next_def, AddressTranslation_def, 32 write'CP0_def, write'exceptionSignalled_def, 33 BranchTo_def, BranchDelay_def] 34 \\ Cases_on 35 `(Run (Decode w) (s' with currentInst := SOME w)).c_state.c_BranchTo` 36 \\ Cases_on 37 `(Run (Decode w) (s' with currentInst := SOME w)).c_state.c_BranchDelay` 38 \\ TRY (Cases_on `x`) 39 \\ lrw [write'PC_def, write'BranchTo_def, write'BranchDelay_def, CP0_def, 40 PC_def] 41 \\ fs [cheri_state_component_equality, procState_component_equality] 42 43val NextStateCHERI_nodelay = utilsLib.ustore_thm("NextStateCHERI_nodelay", 44 `(s.exception = NoException) /\ 45 (BranchDelay s = NONE) /\ 46 (s.BranchDelayPCC = NONE) /\ 47 ~exceptionSignalled s ==> 48 (Fetch (s with currentInst := NONE) = (SOME w, s')) /\ 49 (Decode w = i) /\ 50 (Run i (s' with currentInst := SOME w) = next_state) /\ 51 (next_state.exception = s.exception) /\ 52 (BranchDelay next_state = s.c_state.c_BranchDelay) /\ 53 (next_state.BranchDelayPCC = NONE) /\ 54 (next_state.BranchToPCC = NONE) /\ 55 (~next_state.CCallBranch) /\ 56 (~next_state.CCallBranchDelay) /\ 57 (BranchTo next_state = b) /\ 58 ~exceptionSignalled next_state ==> 59 (NextStateCHERI s = 60 SOME (next_state with 61 <| c_state := next_state.c_state with 62 <| c_PC := PC next_state + 4w; 63 c_BranchDelay := b; 64 c_BranchTo := NONE; 65 c_exceptionSignalled := F; 66 c_CP0 := CP0 next_state with 67 Count := (CP0 next_state).Count + 1w 68 |> 69 |>))`, 70 tac 71 ) 72 73val NextStateCHERI_delay = utilsLib.ustore_thm("NextStateCHERI_delay", 74 `(s.exception = NoException) /\ 75 (BranchDelay s = SOME a) /\ 76 (s.BranchDelayPCC = NONE) /\ 77 ~exceptionSignalled s ==> 78 (Fetch (s with currentInst := NONE) = (SOME w, s')) /\ 79 (Decode w = i) /\ 80 (Run i (s' with currentInst := SOME w) = next_state) /\ 81 (next_state.exception = s.exception) /\ 82 (BranchDelay next_state = s.c_state.c_BranchDelay) /\ 83 (next_state.BranchDelayPCC = NONE) /\ 84 (next_state.BranchToPCC = NONE) /\ 85 (~next_state.CCallBranch) /\ 86 (~next_state.CCallBranchDelay) /\ 87 (BranchTo next_state = NONE) /\ 88 ~exceptionSignalled next_state ==> 89 (NextStateCHERI s = 90 SOME (next_state with 91 <| c_state := next_state.c_state with 92 <| c_PC := a; 93 c_BranchDelay := NONE; 94 c_BranchTo := NONE; 95 c_exceptionSignalled := F; 96 c_CP0 := CP0 next_state with 97 Count := (CP0 next_state).Count + 1w 98 |> 99 |>))`, 100 tac 101 ) 102 103(* ------------------------------------------------------------------------ *) 104 105(* Lemmas and tools *) 106 107val not31 = Q.store_thm("not31", 108 `x0 /\ x1 /\ x2 /\ x3 /\ x4 = (v2w [x0; x1; x2; x3; x4] = (31w: word5))`, 109 blastLib.BBLAST_TAC 110 ) 111 112val v2w_0_rwts = Q.store_thm("v2w_0_rwts", 113 `((v2w [F; F; F; F; F] = 0w: word5)) /\ 114 ((v2w [T; b3; b2; b1; b0] = 0w: word5) = F) /\ 115 ((v2w [b3; T; b2; b1; b0] = 0w: word5) = F) /\ 116 ((v2w [b3; b2; T; b1; b0] = 0w: word5) = F) /\ 117 ((v2w [b3; b2; b1; T; b0] = 0w: word5) = F) /\ 118 ((v2w [b3; b2; b1; b0; T] = 0w: word5) = F)`, 119 blastLib.BBLAST_TAC 120 ) 121 122val NotWordValue0 = Q.store_thm("NotWordValue0", 123 `!b x. ~NotWordValue 0w`, 124 lrw [NotWordValue_def] 125 ) 126 127val NotWordValueCond = Q.store_thm("NotWordValueCond", 128 `!b x. NotWordValue (if b then 0w else x) = ~b /\ NotWordValue x`, 129 lrw [NotWordValue0] 130 ) 131 132val () = show_assums := true 133 134val isAligned = Q.store_thm("isAligned", 135 `(!a. isAligned (a, 0w)) /\ 136 (!a. isAligned (a, 1w) = aligned 1 a) /\ 137 (!a. isAligned (a, 3w) = aligned 2 a) /\ 138 (!a. isAligned (a, 7w) = aligned 3 a)`, 139 simp [isAligned_def, alignmentTheory.aligned_extract] 140 \\ blastLib.BBLAST_TAC 141 ) 142 143val aligned_pc = Q.prove( 144 `!pc : word64. ((1 >< 0) pc = 0w : word2) = aligned 2 pc`, 145 simp [alignmentTheory.aligned_extract] 146 \\ blastLib.BBLAST_TAC) 147 148val word1_lem = utilsLib.mk_cond_exhaustive_thm 1 149val word2_lem = utilsLib.mk_cond_exhaustive_thm 2 150val word3_lem = utilsLib.mk_cond_exhaustive_thm 3 151 152val write_data_lem0 = Q.prove( 153 `!d1 : word64 d2 : word64 d3 : word64 d4 : word64 mask : word64 data : word64. 154 (63 >< 0) d4 && (63 >< 0) (~mask) || 155 (63 >< 0) data && (63 >< 0) mask || (63 >< 0) d1 << 192 || 156 (63 >< 0) d2 << 128 || (63 >< 0) d3 << 64 = 157 (d1 @@ d2 @@ d3 @@ (d4 && ~mask || data && mask)) : 256 word`, 158 blastLib.BBLAST_TAC) 159 160val write_data_lem1 = Q.prove( 161 `!d1 : word64 d2 : word64 d3 : word64 d4 : word64 mask : word64 data : word64. 162 (63 >< 0) d3 << 64 && (63 >< 0) (~mask) << 64 || 163 (63 >< 0) data << 64 && (63 >< 0) mask << 64 || 164 (63 >< 0) d1 << 192 || (63 >< 0) d2 << 128 || (63 >< 0) d4 = 165 (d1 @@ d2 @@ (d3 && ~mask || data && mask) @@ d4) : 256 word`, 166 blastLib.BBLAST_TAC) 167 168val write_data_lem2 = Q.prove( 169 `!d1 : word64 d2 : word64 d3 : word64 d4 : word64 mask : word64 data : word64. 170 (63 >< 0) d2 << 128 && (63 >< 0) (~mask) << 128 || 171 (63 >< 0) data << 128 && (63 >< 0) mask << 128 || 172 (63 >< 0) d1 << 192 || (63 >< 0) d3 << 64 || (63 >< 0) d4 = 173 (d1 @@ (d2 && ~mask || data && mask) @@ d3 @@ d4) : 256 word`, 174 blastLib.BBLAST_TAC) 175 176val write_data_lem3 = Q.prove( 177 `!d1 : word64 d2 : word64 d3 : word64 d4 : word64 mask : word64 data : word64. 178 (63 >< 0) d1 << 192 && (63 >< 0) (~mask) << 192 || 179 (63 >< 0) data << 192 && (63 >< 0) mask << 192 || 180 (63 >< 0) d2 << 128 || (63 >< 0) d3 << 64 || (63 >< 0) d4 = 181 ((d1 && ~mask || data && mask) @@ d2 @@ d3 @@ d4) : 256 word`, 182 blastLib.BBLAST_TAC) 183 184val write_data_lem = 185 LIST_CONJ [write_data_lem0, write_data_lem1, write_data_lem2, write_data_lem3] 186 187val B_ZALL_lem = Q.prove( 188 `(if b then s with <| c_gpr := x; c_state := y |> else s) = 189 s with <| c_gpr := if b then x else s.c_gpr; 190 c_state := if b then y else s.c_state |>`, 191 rw [cheri_state_component_equality]) 192 193val for_end = 194 state_transformerTheory.FOR_def 195 |> Q.SPECL [`i`, `i`] 196 |> REWRITE_RULE [] 197 198val state_id = 199 LIST_CONJ [ 200 utilsLib.mk_state_id_thm cheri_state_component_equality 201 [["c_gpr"], 202 ["all_state", "c_state"], 203 ["BranchDelayPCC", "BranchToPCC", "c_capr", "c_pcc", "c_state"]], 204 utilsLib.mk_state_id_thm procState_component_equality 205 [["c_LLbit"], 206 ["c_CP0", "c_LLbit"]] 207 ] 208 209val st = ``s:cheri_state`` 210 211val extract_conv = simpLib.SIMP_CONV (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 212 213local 214 val datatype_thms = 215 utilsLib.datatype_rewrites true "cheri" 216 ["cheri_state", 217 "procState", "DataType", "CP0", "CapCause", "StatusRegister", 218 "ExceptionType"] 219 val datatype_conv = SIMP_CONV std_ss datatype_thms 220 val datatype_rule = CONV_RULE datatype_conv 221 val datatype_thms = 222 datatype_thms @ 223 List.map datatype_rule 224 (utilsLib.mk_cond_update_thms 225 [``:cheri_state``, 226 ``:procState``, ``:CP0``] @ 227 [state_id, updateTheory.APPLY_UPDATE_ID, CP0_def, 228 BETA_RULE (utilsLib.mk_cond_rand_thms [``\f. f (w2n a)``]), 229 utilsLib.mk_cond_rand_thms 230 [``cheri$CP0_Status``, 231 pairSyntax.fst_tm, pairSyntax.snd_tm, 232 optionSyntax.is_some_tm, 233 wordsSyntax.sw2sw_tm, wordsSyntax.w2w_tm, 234 wordsSyntax.word_add_tm, wordsSyntax.word_sub_tm, 235 wordsSyntax.word_mul_tm, 236 wordsSyntax.word_rem_tm, wordsSyntax.word_quot_tm, 237 wordsSyntax.word_mod_tm, wordsSyntax.word_div_tm, 238 wordsSyntax.word_lo_tm, wordsSyntax.word_lt_tm, 239 wordsSyntax.word_ls_tm, wordsSyntax.word_le_tm, 240 wordsSyntax.word_hi_tm, wordsSyntax.word_gt_tm, 241 wordsSyntax.word_hs_tm, wordsSyntax.word_ge_tm, 242 wordsSyntax.word_and_tm, wordsSyntax.word_or_tm, 243 wordsSyntax.word_xor_tm, wordsSyntax.word_lsl_tm, 244 wordsSyntax.word_lsr_tm, wordsSyntax.word_asr_tm, 245 wordsSyntax.word_1comp_tm, wordsSyntax.word_2comp_tm, 246 wordsSyntax.w2n_tm, 247 ``(h >< l) : 'a word -> 'b word``, 248 ``(=):'a word -> 'a word -> bool``, 249 ``word_bit n: 'a word -> bool``]]) 250 val thms = 251 List.map datatype_rule 252 [extract_conv ``(1 >< 0) ((39 >< 3) (vaddr: word64) : 37 word) : word2``, 253 extract_conv ``(36 >< 2) ((39 >< 3) (vaddr: word64) : 37 word) :35 word``, 254 extract_conv ``(39 >< 5) ((39 >< 0) (vaddr: word64) : 40 word) :35 word``, 255 bitstringLib.v2w_n2w_CONV ``v2w [F] :word1``, BranchDelay_def, 256 getTag_def, getSealed_def, getBase_def, 257 getLength_def, getPerms_def, getOffset_def, CAPR_def, write'CAPR_def, 258 setOffset_def, rec'Perms_def, Perms_accessors, 259 wordsTheory.WORD_XOR_CLAUSES, isAligned, BYTE_def, HALFWORD_def, 260 WORD_def, DOUBLEWORD_def, LLbit_def, write'LLbit_def, write'CP0_def, 261 KCC_def, PC_def, write'PC_def, PCC_def, write'PCC_def, write'EPCC_def, 262 NotWordValue0, NotWordValueCond, GPR_def, write'GPR_def, gpr_def, 263 write'gpr_def, CPR_def, write'CPR_def, boolTheory.COND_ID, 264 wordsLib.WORD_DECIDE ``~(a > a:'a word)``, 265 wordsLib.WORD_DECIDE ``a >= a:'a word``, 266 wordsTheory.WORD_EXTRACT_ZERO2, wordsTheory.WORD_ADD_0, 267 wordsTheory.WORD_AND_CLAUSES, wordsTheory.WORD_OR_CLAUSES, 268 wordsTheory.WORD_XOR_CLAUSES, wordsTheory.WORD_MULT_CLAUSES, 269 wordsTheory.WORD_SUB_RZERO, wordsTheory.WORD_SUB_LZERO, 270 wordsTheory.WORD_LESS_REFL, wordsTheory.WORD_LOWER_REFL, 271 wordsTheory.WORD_LESS_EQ_REFL, wordsTheory.WORD_LO_word_0, 272 wordsTheory.ZERO_SHIFT, wordsTheory.SHIFT_ZERO, 273 wordsTheory.WORD_XOR_ASSOC, wordsTheory.WORD_NEG_0, 274 wordsTheory.WORD_NOT_0, wordsTheory.sw2sw_0, wordsTheory.w2w_0, 275 wordsTheory.word_0_n2w, wordsTheory.word_bit_0 276 ] 277 val conv = SIMP_CONV std_ss (datatype_thms @ thms) 278in 279 val finish_off = List.map (utilsLib.FULL_CONV_RULE conv) 280 val datatype_rule = datatype_rule 281 val ev_conv = conv 282 val ev_rule = CONV_RULE conv 283 val step = utilsLib.STEP (Lib.curry (op @) datatype_thms, st) 284 fun ev ths ctxt cvr t = finish_off (step (ths @ thms) ctxt cvr t) 285end 286 287(* ------------------------------------------------------------------------ *) 288 289(* CHERI exceptions *) 290 291val () = utilsLib.resetStepConv () 292 293val cp0_conv = 294 RAND_CONV (SIMP_CONV (std_ss++boolSimps.LET_ss) 295 [PCC_def, CP0_def, write'CP0_def] 296 THENC ev_conv) 297 298val ev_assume = 299 Thm.ASSUME o utilsLib.rhsc o 300 (QCONV (REWRITE_CONV [CP0_def, BranchDelay_def]) 301 THENC ev_conv) 302 303val SignalException0_rwt = 304 SignalException_def 305 |> Drule.SPEC_ALL 306 |> (fn th => Thm.AP_THM th st) 307 |> Conv.RIGHT_CONV_RULE 308 (Thm.BETA_CONV 309 THENC REWRITE_CONV [BranchDelay_def] 310 THENC ev_conv 311 THENC REWRITE_CONV 312 (List.map ev_assume 313 [``~IS_SOME (BranchDelay ^st)``, 314 ``~IS_SOME (^st.BranchDelayPCC)``, 315 ``~(CP0 ^st).Status.EXL``, 316 ``ExceptionType <> XTLBRefillL``, 317 ``ExceptionType <> XTLBRefillS``, 318 ``ExceptionType <> C2E``]) 319 THENC cp0_conv 320 THENC PairedLambda.let_CONV 321 THENC RAND_CONV 322 (ev_conv 323 THENC REWRITE_CONV 324 [CP0_def, ev_assume ``IS_SOME ^st.currentInst``] 325 THENC PairedLambda.let_CONV 326 THENC ev_conv) 327 THENC PairedLambda.let_CONV 328 THENC cp0_conv 329 THENC PairedLambda.let_CONV 330 THENC cp0_conv 331 THENC PairedLambda.let_CONV 332 THENC RAND_CONV 333 (REWRITE_CONV 334 [write'BranchDelay_def, write'BranchTo_def, 335 write'exceptionSignalled_def, write'CAPR_def 336 ] 337 THENC ev_conv 338 THENC PairedLambda.let_CONV 339 THENC REWRITE_CONV [PCC_def] 340 THENC ev_conv) 341 THENC PairedLambda.let_CONV 342 THENC cp0_conv 343 THENC PairedLambda.let_CONV 344 THENC cp0_conv 345 THENC PairedLambda.let_CONV 346 THENC cp0_conv 347 THENC RAND_CONV 348 (ev_conv 349 THENC REWRITE_CONV [ev_assume ``(CP0 ^st).Status.BEV``] 350 ) 351 THENC PairedLambda.let_CONV 352 THENC PairedLambda.let_CONV 353 THENC cp0_conv 354 THENC SIMP_CONV (srw_ss()) [] 355 ) 356 357val SignalException_rwt = 358 ev [SignalException0_rwt] [[``(CP0 ^st).Status.BEV``]] [] 359 ``SignalException (ExceptionType)`` 360 |> hd 361 362local 363 val is_SignalException = #4 (HolKernel.syntax_fns2 "cheri" "SignalException") 364 fun negate b = 365 case Lib.total boolSyntax.dest_neg b of 366 SOME nb => nb 367 | NONE => boolSyntax.mk_neg b 368 fun get_exception_cond tm = 369 let 370 val (b, t, e) = boolSyntax.dest_cond tm 371 in 372 if is_SignalException t orelse is_SignalException e 373 then b 374 else raise mk_HOL_ERR "cheri_stepScript" "" "" 375 end 376in 377 fun split_exception th = 378 let 379 val t = HolKernel.find_term (Lib.can get_exception_cond) (Thm.concl th) 380 val b = #1 (boolSyntax.dest_cond t) 381 in 382 finish_off 383 (List.map (utilsLib.INST_REWRITE_RULE [SignalException_rwt] o ev_rule) 384 [REWRITE_RULE [ASSUME b] th, 385 REWRITE_RULE [ASSUME (negate b)] th]) 386 end 387 handle HOL_ERR _ => [th] 388end 389 390(* ------------------------------------------------------------------------ *) 391 392val () = ( utilsLib.reset_thms () 393 ; utilsLib.setStepConv utilsLib.WGROUND_CONV 394 ) 395 396fun get_def n = 397 let 398 val th = DB.fetch "cheri" ("dfn'" ^ n ^ "_def") 399 val tm = utilsLib.lhsc (Drule.SPEC_ALL th) 400 in 401 (th, tm) 402 end 403 404local 405 val thms = 406 [write'HI_def, write'LO_def, HI_def, LO_def, 407 write'hi_def, write'lo_def, hi_def, lo_def, 408 write'BranchTo_def, CheckBranch_def, 409 ev_rule B_ZALL_lem] 410 fun instr_ev d cvr name = 411 let 412 val (th, tm) = get_def name 413 in 414 ev (th :: thms) 415 [[``^d <> 0w : word5``, 416 ``~NotWordValue (^st.c_gpr (rs))``, 417 ``~NotWordValue (^st.c_gpr (rt))``, 418 ``^st.c_state.c_hi = SOME hival``, 419 ``^st.c_state.c_lo = SOME loval``, 420 ``~IS_SOME ^st.c_state.c_BranchDelay`` 421 ]] cvr tm 422 |> List.map split_exception 423 |> List.concat 424 |> utilsLib.save_thms name 425 end 426 val v0 = bitstringSyntax.padded_fixedwidth_of_num (Arbnum.fromInt 0, 5) 427in 428 val tev = instr_ev ``rt : word5`` [[`rt` |-> v0], []] 429 val dev = instr_ev ``rd : word5`` [[`rd` |-> v0], []] 430 val xev = instr_ev ``rx : word5`` [] 431end 432 433(* Arithmetic/Logic instructions *) 434 435val ADDI = tev "ADDI" 436val DADDI = tev "DADDI" 437 438val ADDIU = tev "ADDIU" 439val DADDIU = tev "DADDIU" 440val SLTI = tev "SLTI" 441val SLTIU = tev "SLTIU" 442val ANDI = tev "ANDI" 443val ORI = tev "ORI" 444val XORI = tev "XORI" 445 446val LUI = tev "LUI" 447 448val ADD = dev "ADD" 449val SUB = dev "SUB" 450val DADD = dev "DADD" 451val DSUB = dev "DSUB" 452val MOVN = dev "MOVN" 453val MOVZ = dev "MOVZ" 454 455val ADDU = dev "ADDU" 456val DADDU = dev "DADDU" 457val SUBU = dev "SUBU" 458val DSUBU = dev "DSUBU" 459val SLT = dev "SLT" 460val SLTU = dev "SLTU" 461val AND = dev "AND" 462val OR = dev "OR" 463val XOR = dev "XOR" 464val NOR = dev "NOR" 465val SLLV = dev "SLLV" 466val SRLV = dev "SRLV" 467val SRAV = dev "SRAV" 468val DSLLV = dev "DSLLV" 469val DSRLV = dev "DSRLV" 470val DSRAV = dev "DSRAV" 471 472val SLL = dev "SLL" 473val SRL = dev "SRL" 474val SRA = dev "SRA" 475val DSLL = dev "DSLL" 476val DSRL = dev "DSRL" 477val DSRA = dev "DSRA" 478val DSLL32 = dev "DSLL32" 479val DSRL32 = dev "DSRL32" 480val DSRA32 = dev "DSRA32" 481 482val MFHI = dev "MFHI" 483val MFLO = dev "MFLO" 484val MTHI = xev "MTHI" 485val MTLO = xev "MTLO" 486 487val MUL = dev "MUL" 488val MADD = xev "MADD" 489val MADDU = xev "MADDU" 490val MSUB = xev "MSUB" 491val MSUBU = xev "MSUBU" 492val MULT = xev "MULT" 493val MULTU = xev "MULTU" 494val DMULT = xev "DMULT" 495val DMULTU = xev "DMULTU" 496 497val DIV = tev "DIV" 498val DIVU = tev "DIVU" 499val DDIV = tev "DDIV" 500val DDIVU = tev "DDIVU" 501 502(* ------------------------------------------------------------------------- *) 503 504(* Jumps and Branches *) 505 506val J = xev "J" 507val JAL = xev "JAL" 508val JR = xev "JR" 509val JALR = dev "JALR" 510val BEQ = xev "BEQ" 511val BNE = xev "BNE" 512val BEQL = xev "BEQL" 513val BNEL = xev "BNEL" 514val BLEZ = xev "BLEZ" 515val BGTZ = xev "BGTZ" 516val BLTZ = xev "BLTZ" 517val BGEZ = xev "BGEZ" 518val BLTZAL = xev "BLTZAL" 519val BGEZAL = xev "BGEZAL" 520val BLEZL = xev "BLEZL" 521val BGTZL = xev "BGTZL" 522val BLTZL = xev "BLTZL" 523val BGEZL = xev "BGEZL" 524val BLTZALL = xev "BLTZALL" 525val BGEZALL = xev "BGEZALL" 526 527(* ------------------------------------------------------------------------ *) 528 529val cap_ok = 530 [``^st.totalCore = 1``, ``^st.procID = 0w``, 531 ``^st.c_capr 0w = capr0``, ``capr0.tag``, ``~capr0.sealed``, 532 ``^st.c_pcc.tag``, ``~^st.c_pcc.sealed``, 533 ``~(^st.c_pcc.base + ^st.c_state.c_PC <+ ^st.c_pcc.base)``, 534 ``~((63 >< 0) (^st.c_pcc.base + ^st.c_state.c_PC) + (4w : 65 word) >+ 535 (63 >< 0) ^st.c_pcc.base + (63 >< 0) ^st.c_pcc.length)``, 536 ``(1 >< 1) ^st.c_pcc.perms = 1w : word32``, 537 ``~(vaddr <+ capr0.base)``, 538 ``~((63 >< 0) (vaddr : word64) + (1w : 65 word) >+ 539 (63 >< 0) capr0.base + (63 >< 0) capr0.length)``, 540 ``~((63 >< 0) (vaddr : word64) + (4w : 65 word) >+ 541 (63 >< 0) capr0.base + (63 >< 0) capr0.length)``, 542 ``~((63 >< 0) (vaddr : word64) + (8w : 65 word) >+ 543 (63 >< 0) capr0.base + (63 >< 0) capr0.length)``, 544 ``~((63 >< 0) (vaddr : word64) + (2 >< 0) (accesslength : word3) + 545 (1w : 65 word) >+ (63 >< 0) capr0.base + (63 >< 0) capr0.length)``, 546 ``~(needalign /\ ~aligned 1 (vaddr : word64))``, 547 ``~(needalign /\ ~aligned 2 (vaddr : word64))``, 548 ``~(needalign /\ ~aligned 3 (vaddr : word64))``, 549 ``(2 >< 2) capr0.perms = 1w : word32``, 550 ``(3 >< 3) capr0.perms = 1w : word32``] 551 552val ReverseEndian_rwt = 553 ev [ReverseEndian_def] [[``~(CP0 ^st).Status.RE``]] [] 554 ``ReverseEndian`` |> hd 555 556(* CHERI is normally big-endian *) 557val BigEndianCPU_rwt = 558 ev [BigEndianCPU_def, BigEndianMem_def, ReverseEndian_rwt] 559 [[``(CP0 ^st).Config.BE``]] [] 560 ``BigEndianCPU`` |> hd 561 562val () = utilsLib.setStepConv (utilsLib.WGROUND_CONV THENC extract_conv) 563 564val WriteData_rwt = 565 ev [WriteData_def, updateDwordInRaw_def, CAPBYTEWIDTH_def, capToBits_def, 566 word2_lem] 567 [[``^st.mem ((36 >< 2) (addr : 37 word)) = 568 Raw ((d1 : word64) @@ (d2 : word64) @@ 569 (d3 : word64) @@ (d4 : word64))``]] [] 570 ``WriteData (addr, data, mask)`` 571 |> hd 572 |> REWRITE_RULE [write_data_lem] 573 574fun StoreMemory cnd = 575 ev [StoreMemory_def, StoreMemoryCap_def, AdjustEndian_def, ReverseEndian_rwt, 576 getBaseAndLength_def, for_end] 577 [``s.c_state.c_LLbit = SOME b`` :: 578 ``(CP0 ^st).LLAddr = (39 >< 0) (vaddr : word64)`` :: 579 cap_ok] 580 [[`memtype` |-> ``BYTE``, `accesslength` |-> ``BYTE``, `cnd` |-> cnd], 581 [`memtype` |-> ``WORD``, `accesslength` |-> ``WORD``, `cnd` |-> cnd], 582 [`memtype` |-> ``DOUBLEWORD``, `accesslength` |-> ``DOUBLEWORD``, 583 `cnd` |-> cnd]] 584 ``StoreMemory (memtype,accesslength,needalign,memelem,vaddr,cnd)`` 585 |> List.map (ev_rule o INST_REWRITE_RULE [WriteData_rwt]) 586 587val StoreMemory_cond_rwt = StoreMemory ``T`` 588val StoreMemory_notcond_rwt = StoreMemory ``F`` 589 590val ReadData_rwt = 591 step [ReadData_def, readDwordFromRaw_def, CAPBYTEWIDTH_def, word2_lem] 592 [[``^st.mem ((36 >< 2) (addr : 37 word)) = 593 Raw ((d1 : word64) @@ (d2 : word64) @@ 594 (d3 : word64) @@ (d4 : word64))``]] [] 595 ``ReadData addr`` |> hd 596 597val LoadMemory_rwt = 598 ev [LoadMemory_def, LoadMemoryCap_def, AdjustEndian_def, ReverseEndian_rwt, 599 ReadData_rwt, getBaseAndLength_def] 600 [cap_ok] 601 [[`memtype` |-> ``BYTE``], 602 [`memtype` |-> ``WORD``], 603 [`memtype` |-> ``DOUBLEWORD``] 604 ] 605 ``LoadMemory (memtype,accesslength,needalign,vaddr,link)``; 606 607val () = utilsLib.setStepConv utilsLib.WGROUND_CONV 608 609local 610 val thms = 611 LoadMemory_rwt @ StoreMemory_cond_rwt @ StoreMemory_notcond_rwt @ 612 [BigEndianCPU_rwt, getVirtualAddress_def, exceptionSignalled_def, 613 loadByte_def, loadHalf_def, loadWord_def, loadDoubleword_def, 614 storeWord_def, storeDoubleword_def, 615 word1_lem, word2_lem, word3_lem, 616 bitstringLib.v2w_n2w_CONV ``v2w [T] : word1``, 617 EVAL ``word_replicate 3 (1w : word1) : word3``, 618 SIMP_CONV (srw_ss()) [] ``x + y + (z - y) : 'a word``] 619 fun instr_ev rt name = 620 let 621 val (th, tm) = get_def name 622 in 623 ev (th :: thms) 624 [rt @ [``base <> 0w : word5``, ``~^st.c_state.c_exceptionSignalled``] @ 625 cap_ok] [] tm 626 |> utilsLib.save_thms name 627 end 628in 629 val lev = instr_ev [``rt <> 0w : word5``] 630 val sev = instr_ev [] 631end 632 633val LB = lev "LB" 634val LBU = lev "LBU" 635 636val LW = lev "LW" 637val LWU = lev "LWU" 638val LL = lev "LL" 639val LWL = lev "LWL" 640val LWR = lev "LWR" 641 642val LD = lev "LD" 643val LLD = lev "LLD" 644val LDL = lev "LDL" 645val LDR = lev "LDR" 646 647val SB = sev "SB" 648val SW = sev "SW" 649val SD = sev "SD" 650val SC = sev "SC" 651val SCD = sev "SCD" 652 653(* ------------------------------------------------------------------------ *) 654 655val () = utilsLib.setStepConv (utilsLib.WGROUND_CONV THENC extract_conv) 656 657val ReadWord_def = Define` 658 ReadWord m (addr : 40 word) = 659 case m ((39 >< 5) addr : 35 word) of 660 Raw w256 => 661 SOME 662 (let v = (4 >< 2) addr : word3 663 in 664 if v = 0w then (63 >< 32 ) w256 665 else if v = 1w then (31 >< 0 ) w256 666 else if v = 2w then (127 >< 96 ) w256 667 else if v = 3w then (95 >< 64 ) w256 668 else if v = 4w then (191 >< 160) w256 669 else if v = 5w then (159 >< 128) w256 670 else if v = 6w then (255 >< 224) w256 671 else (223 >< 192) w256 : word32) 672 | _ => NONE` 673 674val ReadInst = Q.prove( 675 `(ReadWord s.mem addr = SOME w) ==> (ReadInst addr s = w)`, 676 rw [ReadInst_def, readDwordFromRaw_def, CAPBYTEWIDTH_def, ReadWord_def, 677 alignmentTheory.aligned_extract, word2_lem] 678 \\ Cases_on `s.mem ((39 >< 5) addr)` 679 \\ full_simp_tac (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 680 \\ rw [] 681 \\ blastLib.FULL_BBLAST_TAC) |> Drule.UNDISCH_ALL 682 683val Fetch_rwt = 684 ev [Fetch_def, exceptionSignalled_def, aligned_pc] 685 [[``~(CP0 ^st).Status.IE``, 686 ``aligned 2 (^st.c_state.c_PC)``, 687 ``~^st.c_state.c_exceptionSignalled``] @ cap_ok] 688 [] ``Fetch`` 689 |> List.map (INST_REWRITE_RULE [ReadInst]) 690 |> finish_off 691 692val Fetch = Theory.save_thm("Fetch", hd Fetch_rwt) 693 694val lem = Q.prove( 695 `aligned 2 (a : word64) ==> 696 (~((63 >< 0) a + (4w : 65 word) >+ 0xFFFFFFFFFFFFFFFFw) = 697 a <> 0xFFFFFFFFFFFFFFFCw)`, 698 simp [alignmentTheory.aligned_extract] 699 \\ blastLib.BBLAST_TAC) |> Drule.UNDISCH_ALL 700 701val Fetch_default = Theory.save_thm("Fetch_default", 702 utilsLib.FULL_CONV_RULE 703 (utilsLib.SRW_CONV [] 704 THENC REWRITE_CONV [ev_assume ``^st.c_pcc = defaultCap``] 705 THENC utilsLib.SRW_CONV [wordsTheory.WORD_LO_word_0, defaultCap_def] 706 THENC utilsLib.INST_REWRITE_CONV [lem]) 707 (Thm.INST [st |-> ``^st with currentInst := NONE``] Fetch) 708 ) 709 710(* ------------------------------------------------------------------------ *) 711 712val () = (utilsLib.adjoin_thms (); export_theory ()) 713