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" 12 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", "cheri_state_brss__0", "cheri_state_brss__1", 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``, ``:cheri_state_brss__0``, ``:cheri_state_brss__1``, 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$cheri_state_brss__sf0``, 231 ``cheri$cheri_state_brss__sf1``, 232 ``cheri$CP0_Status``, 233 pairSyntax.fst_tm, pairSyntax.snd_tm, 234 optionSyntax.is_some_tm, 235 wordsSyntax.sw2sw_tm, wordsSyntax.w2w_tm, 236 wordsSyntax.word_add_tm, wordsSyntax.word_sub_tm, 237 wordsSyntax.word_mul_tm, 238 wordsSyntax.word_rem_tm, wordsSyntax.word_quot_tm, 239 wordsSyntax.word_mod_tm, wordsSyntax.word_div_tm, 240 wordsSyntax.word_lo_tm, wordsSyntax.word_lt_tm, 241 wordsSyntax.word_ls_tm, wordsSyntax.word_le_tm, 242 wordsSyntax.word_hi_tm, wordsSyntax.word_gt_tm, 243 wordsSyntax.word_hs_tm, wordsSyntax.word_ge_tm, 244 wordsSyntax.word_and_tm, wordsSyntax.word_or_tm, 245 wordsSyntax.word_xor_tm, wordsSyntax.word_lsl_tm, 246 wordsSyntax.word_lsr_tm, wordsSyntax.word_asr_tm, 247 wordsSyntax.word_1comp_tm, wordsSyntax.word_2comp_tm, 248 wordsSyntax.w2n_tm, 249 ``(h >< l) : 'a word -> 'b word``, 250 ``(=):'a word -> 'a word -> bool``, 251 ``word_bit n: 'a word -> bool``]]) 252 val thms = 253 List.map datatype_rule 254 [extract_conv ``(1 >< 0) ((39 >< 3) (vaddr: word64) : 37 word) : word2``, 255 extract_conv ``(36 >< 2) ((39 >< 3) (vaddr: word64) : 37 word) :35 word``, 256 extract_conv ``(39 >< 5) ((39 >< 0) (vaddr: word64) : 40 word) :35 word``, 257 bitstringLib.v2w_n2w_CONV ``v2w [F] :word1``, BranchDelay_def, 258 getTag_def, getSealed_def, getBase_def, 259 getLength_def, getPerms_def, getOffset_def, CAPR_def, write'CAPR_def, 260 setOffset_def, rec'Perms_def, Perms_accessors, 261 wordsTheory.WORD_XOR_CLAUSES, isAligned, BYTE_def, HALFWORD_def, 262 WORD_def, DOUBLEWORD_def, LLbit_def, write'LLbit_def, write'CP0_def, 263 KCC_def, PC_def, write'PC_def, PCC_def, write'PCC_def, write'EPCC_def, 264 NotWordValue0, NotWordValueCond, GPR_def, write'GPR_def, gpr_def, 265 write'gpr_def, CPR_def, write'CPR_def, boolTheory.COND_ID, 266 wordsLib.WORD_DECIDE ``~(a > a:'a word)``, 267 wordsLib.WORD_DECIDE ``a >= a:'a word``, 268 wordsTheory.WORD_EXTRACT_ZERO2, wordsTheory.WORD_ADD_0, 269 wordsTheory.WORD_AND_CLAUSES, wordsTheory.WORD_OR_CLAUSES, 270 wordsTheory.WORD_XOR_CLAUSES, wordsTheory.WORD_MULT_CLAUSES, 271 wordsTheory.WORD_SUB_RZERO, wordsTheory.WORD_SUB_LZERO, 272 wordsTheory.WORD_LESS_REFL, wordsTheory.WORD_LOWER_REFL, 273 wordsTheory.WORD_LESS_EQ_REFL, wordsTheory.WORD_LO_word_0, 274 wordsTheory.ZERO_SHIFT, wordsTheory.SHIFT_ZERO, 275 wordsTheory.WORD_XOR_ASSOC, wordsTheory.WORD_NEG_0, 276 wordsTheory.WORD_NOT_0, wordsTheory.sw2sw_0, wordsTheory.w2w_0, 277 wordsTheory.word_0_n2w, wordsTheory.word_bit_0 278 ] 279 val conv = SIMP_CONV std_ss (datatype_thms @ thms) 280in 281 val finish_off = List.map (utilsLib.FULL_CONV_RULE conv) 282 val datatype_rule = datatype_rule 283 val ev_conv = conv 284 val ev_rule = CONV_RULE conv 285 val step = utilsLib.STEP (Lib.curry (op @) datatype_thms, st) 286 fun ev ths ctxt cvr t = finish_off (step (ths @ thms) ctxt cvr t) 287end 288 289(* ------------------------------------------------------------------------ *) 290 291(* CHERI exceptions *) 292 293val () = utilsLib.resetStepConv () 294 295val cp0_conv = 296 RAND_CONV (SIMP_CONV (std_ss++boolSimps.LET_ss) 297 [PCC_def, CP0_def, write'CP0_def] 298 THENC ev_conv) 299 300val ev_assume = 301 Thm.ASSUME o utilsLib.rhsc o 302 (QCONV (REWRITE_CONV [CP0_def, BranchDelay_def]) 303 THENC ev_conv) 304 305val SignalException0_rwt = 306 SignalException_def 307 |> Drule.SPEC_ALL 308 |> (fn th => Thm.AP_THM th st) 309 |> Conv.RIGHT_CONV_RULE 310 (Thm.BETA_CONV 311 THENC REWRITE_CONV [BranchDelay_def] 312 THENC ev_conv 313 THENC REWRITE_CONV 314 (List.map ev_assume 315 [``~IS_SOME (BranchDelay ^st)``, 316 ``~IS_SOME (^st.BranchDelayPCC)``, 317 ``~(CP0 ^st).Status.EXL``, 318 ``ExceptionType <> XTLBRefillL``, 319 ``ExceptionType <> XTLBRefillS``, 320 ``ExceptionType <> C2E``]) 321 THENC cp0_conv 322 THENC PairedLambda.let_CONV 323 THENC RAND_CONV 324 (ev_conv 325 THENC REWRITE_CONV 326 [CP0_def, ev_assume ``IS_SOME ^st.currentInst``] 327 THENC PairedLambda.let_CONV 328 THENC ev_conv) 329 THENC PairedLambda.let_CONV 330 THENC cp0_conv 331 THENC PairedLambda.let_CONV 332 THENC cp0_conv 333 THENC PairedLambda.let_CONV 334 THENC RAND_CONV 335 (REWRITE_CONV 336 [write'BranchDelay_def, write'BranchTo_def, 337 write'exceptionSignalled_def, write'CAPR_def 338 ] 339 THENC ev_conv 340 THENC PairedLambda.let_CONV 341 THENC REWRITE_CONV [PCC_def] 342 THENC ev_conv) 343 THENC PairedLambda.let_CONV 344 THENC cp0_conv 345 THENC PairedLambda.let_CONV 346 THENC cp0_conv 347 THENC PairedLambda.let_CONV 348 THENC cp0_conv 349 THENC RAND_CONV 350 (ev_conv 351 THENC REWRITE_CONV [ev_assume ``(CP0 ^st).Status.BEV``] 352 ) 353 THENC PairedLambda.let_CONV 354 THENC PairedLambda.let_CONV 355 THENC cp0_conv 356 THENC SIMP_CONV (srw_ss()) [] 357 ) 358 359val SignalException_rwt = 360 ev [SignalException0_rwt] [[``(CP0 ^st).Status.BEV``]] [] 361 ``SignalException (ExceptionType)`` 362 |> hd 363 364local 365 val is_SignalException = #4 (HolKernel.syntax_fns2 "cheri" "SignalException") 366 fun negate b = 367 case Lib.total boolSyntax.dest_neg b of 368 SOME nb => nb 369 | NONE => boolSyntax.mk_neg b 370 fun get_exception_cond tm = 371 let 372 val (b, t, e) = boolSyntax.dest_cond tm 373 in 374 if is_SignalException t orelse is_SignalException e 375 then b 376 else raise ERR "" "" 377 end 378in 379 fun split_exception th = 380 let 381 val t = HolKernel.find_term (Lib.can get_exception_cond) (Thm.concl th) 382 val b = #1 (boolSyntax.dest_cond t) 383 in 384 finish_off 385 (List.map (utilsLib.INST_REWRITE_RULE [SignalException_rwt] o ev_rule) 386 [REWRITE_RULE [ASSUME b] th, 387 REWRITE_RULE [ASSUME (negate b)] th]) 388 end 389 handle HOL_ERR _ => [th] 390end 391 392(* ------------------------------------------------------------------------ *) 393 394val () = ( utilsLib.reset_thms () 395 ; utilsLib.setStepConv utilsLib.WGROUND_CONV 396 ) 397 398fun get_def n = 399 let 400 val th = DB.fetch "cheri" ("dfn'" ^ n ^ "_def") 401 val tm = utilsLib.lhsc (Drule.SPEC_ALL th) 402 in 403 (th, tm) 404 end 405 406local 407 val thms = 408 [write'HI_def, write'LO_def, HI_def, LO_def, 409 write'hi_def, write'lo_def, hi_def, lo_def, 410 write'BranchTo_def, CheckBranch_def, 411 ev_rule B_ZALL_lem] 412 fun instr_ev d cvr name = 413 let 414 val (th, tm) = get_def name 415 in 416 ev (th :: thms) 417 [[``^d <> 0w : word5``, 418 ``~NotWordValue (^st.c_gpr (rs))``, 419 ``~NotWordValue (^st.c_gpr (rt))``, 420 ``^st.c_state.c_hi = SOME hival``, 421 ``^st.c_state.c_lo = SOME loval``, 422 ``~IS_SOME ^st.c_state.c_BranchDelay`` 423 ]] cvr tm 424 |> List.map split_exception 425 |> List.concat 426 |> utilsLib.save_thms name 427 end 428 val v0 = bitstringSyntax.padded_fixedwidth_of_num (Arbnum.fromInt 0, 5) 429in 430 val tev = instr_ev ``rt : word5`` [[`rt` |-> v0], []] 431 val dev = instr_ev ``rd : word5`` [[`rd` |-> v0], []] 432 val xev = instr_ev ``rx : word5`` [] 433end 434 435(* Arithmetic/Logic instructions *) 436 437val ADDI = tev "ADDI" 438val DADDI = tev "DADDI" 439 440val ADDIU = tev "ADDIU" 441val DADDIU = tev "DADDIU" 442val SLTI = tev "SLTI" 443val SLTIU = tev "SLTIU" 444val ANDI = tev "ANDI" 445val ORI = tev "ORI" 446val XORI = tev "XORI" 447 448val LUI = tev "LUI" 449 450val ADD = dev "ADD" 451val SUB = dev "SUB" 452val DADD = dev "DADD" 453val DSUB = dev "DSUB" 454val MOVN = dev "MOVN" 455val MOVZ = dev "MOVZ" 456 457val ADDU = dev "ADDU" 458val DADDU = dev "DADDU" 459val SUBU = dev "SUBU" 460val DSUBU = dev "DSUBU" 461val SLT = dev "SLT" 462val SLTU = dev "SLTU" 463val AND = dev "AND" 464val OR = dev "OR" 465val XOR = dev "XOR" 466val NOR = dev "NOR" 467val SLLV = dev "SLLV" 468val SRLV = dev "SRLV" 469val SRAV = dev "SRAV" 470val DSLLV = dev "DSLLV" 471val DSRLV = dev "DSRLV" 472val DSRAV = dev "DSRAV" 473 474val SLL = dev "SLL" 475val SRL = dev "SRL" 476val SRA = dev "SRA" 477val DSLL = dev "DSLL" 478val DSRL = dev "DSRL" 479val DSRA = dev "DSRA" 480val DSLL32 = dev "DSLL32" 481val DSRL32 = dev "DSRL32" 482val DSRA32 = dev "DSRA32" 483 484val MFHI = dev "MFHI" 485val MFLO = dev "MFLO" 486val MTHI = xev "MTHI" 487val MTLO = xev "MTLO" 488 489val MUL = dev "MUL" 490val MADD = xev "MADD" 491val MADDU = xev "MADDU" 492val MSUB = xev "MSUB" 493val MSUBU = xev "MSUBU" 494val MULT = xev "MULT" 495val MULTU = xev "MULTU" 496val DMULT = xev "DMULT" 497val DMULTU = xev "DMULTU" 498 499val DIV = tev "DIV" 500val DIVU = tev "DIVU" 501val DDIV = tev "DDIV" 502val DDIVU = tev "DDIVU" 503 504(* ------------------------------------------------------------------------- *) 505 506(* Jumps and Branches *) 507 508val J = xev "J" 509val JAL = xev "JAL" 510val JR = xev "JR" 511val JALR = dev "JALR" 512val BEQ = xev "BEQ" 513val BNE = xev "BNE" 514val BEQL = xev "BEQL" 515val BNEL = xev "BNEL" 516val BLEZ = xev "BLEZ" 517val BGTZ = xev "BGTZ" 518val BLTZ = xev "BLTZ" 519val BGEZ = xev "BGEZ" 520val BLTZAL = xev "BLTZAL" 521val BGEZAL = xev "BGEZAL" 522val BLEZL = xev "BLEZL" 523val BGTZL = xev "BGTZL" 524val BLTZL = xev "BLTZL" 525val BGEZL = xev "BGEZL" 526val BLTZALL = xev "BLTZALL" 527val BGEZALL = xev "BGEZALL" 528 529(* ------------------------------------------------------------------------ *) 530 531val cap_ok = 532 [``^st.totalCore = 1``, ``^st.procID = 0w``, 533 ``^st.c_capr 0w = capr0``, ``capr0.tag``, ``~capr0.sealed``, 534 ``^st.c_pcc.tag``, ``~^st.c_pcc.sealed``, 535 ``~(^st.c_pcc.base + ^st.c_state.c_PC <+ ^st.c_pcc.base)``, 536 ``~((63 >< 0) (^st.c_pcc.base + ^st.c_state.c_PC) + (4w : 65 word) >+ 537 (63 >< 0) ^st.c_pcc.base + (63 >< 0) ^st.c_pcc.length)``, 538 ``(1 >< 1) ^st.c_pcc.perms = 1w : word32``, 539 ``~(vaddr <+ capr0.base)``, 540 ``~((63 >< 0) (vaddr : word64) + (1w : 65 word) >+ 541 (63 >< 0) capr0.base + (63 >< 0) capr0.length)``, 542 ``~((63 >< 0) (vaddr : word64) + (4w : 65 word) >+ 543 (63 >< 0) capr0.base + (63 >< 0) capr0.length)``, 544 ``~((63 >< 0) (vaddr : word64) + (8w : 65 word) >+ 545 (63 >< 0) capr0.base + (63 >< 0) capr0.length)``, 546 ``~((63 >< 0) (vaddr : word64) + (2 >< 0) (accesslength : word3) + 547 (1w : 65 word) >+ (63 >< 0) capr0.base + (63 >< 0) capr0.length)``, 548 ``~(needalign /\ ~aligned 1 (vaddr : word64))``, 549 ``~(needalign /\ ~aligned 2 (vaddr : word64))``, 550 ``~(needalign /\ ~aligned 3 (vaddr : word64))``, 551 ``(2 >< 2) capr0.perms = 1w : word32``, 552 ``(3 >< 3) capr0.perms = 1w : word32``] 553 554val ReverseEndian_rwt = 555 ev [ReverseEndian_def] [[``~(CP0 ^st).Status.RE``]] [] 556 ``ReverseEndian`` |> hd 557 558(* CHERI is normally big-endian *) 559val BigEndianCPU_rwt = 560 ev [BigEndianCPU_def, BigEndianMem_def, ReverseEndian_rwt] 561 [[``(CP0 ^st).Config.BE``]] [] 562 ``BigEndianCPU`` |> hd 563 564val () = utilsLib.setStepConv (utilsLib.WGROUND_CONV THENC extract_conv) 565 566val WriteData_rwt = 567 ev [WriteData_def, updateDwordInRaw_def, CAPBYTEWIDTH_def, capToBits_def, 568 word2_lem] 569 [[``^st.mem ((36 >< 2) (addr : 37 word)) = 570 Raw ((d1 : word64) @@ (d2 : word64) @@ 571 (d3 : word64) @@ (d4 : word64))``]] [] 572 ``WriteData (addr, data, mask)`` 573 |> hd 574 |> REWRITE_RULE [write_data_lem] 575 576fun StoreMemory cnd = 577 ev [StoreMemory_def, StoreMemoryCap_def, AdjustEndian_def, ReverseEndian_rwt, 578 getBaseAndLength_def, for_end] 579 [``s.c_state.c_LLbit = SOME b`` :: 580 ``(CP0 ^st).LLAddr = (39 >< 0) (vaddr : word64)`` :: 581 cap_ok] 582 [[`memtype` |-> ``BYTE``, `accesslength` |-> ``BYTE``, `cnd` |-> cnd], 583 [`memtype` |-> ``WORD``, `accesslength` |-> ``WORD``, `cnd` |-> cnd], 584 [`memtype` |-> ``DOUBLEWORD``, `accesslength` |-> ``DOUBLEWORD``, 585 `cnd` |-> cnd]] 586 ``StoreMemory (memtype,accesslength,needalign,memelem,vaddr,cnd)`` 587 |> List.map (ev_rule o INST_REWRITE_RULE [WriteData_rwt]) 588 589val StoreMemory_cond_rwt = StoreMemory ``T`` 590val StoreMemory_notcond_rwt = StoreMemory ``F`` 591 592val ReadData_rwt = 593 step [ReadData_def, readDwordFromRaw_def, CAPBYTEWIDTH_def, word2_lem] 594 [[``^st.mem ((36 >< 2) (addr : 37 word)) = 595 Raw ((d1 : word64) @@ (d2 : word64) @@ 596 (d3 : word64) @@ (d4 : word64))``]] [] 597 ``ReadData addr`` |> hd 598 599val LoadMemory_rwt = 600 ev [LoadMemory_def, LoadMemoryCap_def, AdjustEndian_def, ReverseEndian_rwt, 601 ReadData_rwt, getBaseAndLength_def] 602 [cap_ok] 603 [[`memtype` |-> ``BYTE``], 604 [`memtype` |-> ``WORD``], 605 [`memtype` |-> ``DOUBLEWORD``] 606 ] 607 ``LoadMemory (memtype,accesslength,needalign,vaddr,link)``; 608 609val () = utilsLib.setStepConv utilsLib.WGROUND_CONV 610 611local 612 val thms = 613 LoadMemory_rwt @ StoreMemory_cond_rwt @ StoreMemory_notcond_rwt @ 614 [BigEndianCPU_rwt, getVirtualAddress_def, exceptionSignalled_def, 615 loadByte_def, loadHalf_def, loadWord_def, loadDoubleword_def, 616 storeWord_def, storeDoubleword_def, 617 word1_lem, word2_lem, word3_lem, 618 bitstringLib.v2w_n2w_CONV ``v2w [T] : word1``, 619 EVAL ``word_replicate 3 (1w : word1) : word3``, 620 SIMP_CONV (srw_ss()) [] ``x + y + (z - y) : 'a word``] 621 fun instr_ev rt name = 622 let 623 val (th, tm) = get_def name 624 in 625 ev (th :: thms) 626 [rt @ [``base <> 0w : word5``, ``~^st.c_state.c_exceptionSignalled``] @ 627 cap_ok] [] tm 628 |> utilsLib.save_thms name 629 end 630in 631 val lev = instr_ev [``rt <> 0w : word5``] 632 val sev = instr_ev [] 633end 634 635val LB = lev "LB" 636val LBU = lev "LBU" 637 638val LW = lev "LW" 639val LWU = lev "LWU" 640val LL = lev "LL" 641val LWL = lev "LWL" 642val LWR = lev "LWR" 643 644val LD = lev "LD" 645val LLD = lev "LLD" 646val LDL = lev "LDL" 647val LDR = lev "LDR" 648 649val SB = sev "SB" 650val SW = sev "SW" 651val SD = sev "SD" 652val SC = sev "SC" 653val SCD = sev "SCD" 654 655(* ------------------------------------------------------------------------ *) 656 657val () = utilsLib.setStepConv (utilsLib.WGROUND_CONV THENC extract_conv) 658 659val ReadWord_def = Define` 660 ReadWord m (addr : 40 word) = 661 case m ((39 >< 5) addr : 35 word) of 662 Raw w256 => 663 SOME 664 (let v = (4 >< 2) addr : word3 665 in 666 if v = 0w then (63 >< 32 ) w256 667 else if v = 1w then (31 >< 0 ) w256 668 else if v = 2w then (127 >< 96 ) w256 669 else if v = 3w then (95 >< 64 ) w256 670 else if v = 4w then (191 >< 160) w256 671 else if v = 5w then (159 >< 128) w256 672 else if v = 6w then (255 >< 224) w256 673 else (223 >< 192) w256 : word32) 674 | _ => NONE` 675 676val ReadInst = Q.prove( 677 `(ReadWord s.mem addr = SOME w) ==> (ReadInst addr s = w)`, 678 rw [ReadInst_def, readDwordFromRaw_def, CAPBYTEWIDTH_def, ReadWord_def, 679 alignmentTheory.aligned_extract, word2_lem] 680 \\ Cases_on `s.mem ((39 >< 5) addr)` 681 \\ full_simp_tac (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 682 \\ rw [] 683 \\ blastLib.FULL_BBLAST_TAC) |> Drule.UNDISCH_ALL 684 685val Fetch_rwt = 686 ev [Fetch_def, exceptionSignalled_def, aligned_pc] 687 [[``~(CP0 ^st).Status.IE``, 688 ``aligned 2 (^st.c_state.c_PC)``, 689 ``~^st.c_state.c_exceptionSignalled``] @ cap_ok] 690 [] ``Fetch`` 691 |> List.map (INST_REWRITE_RULE [ReadInst]) 692 |> finish_off 693 694val Fetch = Theory.save_thm("Fetch", hd Fetch_rwt) 695 696val lem = Q.prove( 697 `aligned 2 (a : word64) ==> 698 (~((63 >< 0) a + (4w : 65 word) >+ 0xFFFFFFFFFFFFFFFFw) = 699 a <> 0xFFFFFFFFFFFFFFFCw)`, 700 simp [alignmentTheory.aligned_extract] 701 \\ blastLib.BBLAST_TAC) |> Drule.UNDISCH_ALL 702 703val Fetch_default = Theory.save_thm("Fetch_default", 704 utilsLib.FULL_CONV_RULE 705 (utilsLib.SRW_CONV [] 706 THENC REWRITE_CONV [ev_assume ``^st.c_pcc = defaultCap``] 707 THENC utilsLib.SRW_CONV [wordsTheory.WORD_LO_word_0, defaultCap_def] 708 THENC utilsLib.INST_REWRITE_CONV [lem]) 709 (Thm.INST [st |-> ``^st with currentInst := NONE``] Fetch) 710 ) 711 712(* ------------------------------------------------------------------------ *) 713 714val () = (utilsLib.adjoin_thms (); export_theory ()) 715