1(* ------------------------------------------------------------------------ 2 Definitions and theorems used by RISC-V step evaluator (riscv_stepLib) 3 ------------------------------------------------------------------------ *) 4 5open HolKernel boolLib bossLib 6 7open utilsLib 8open wordsLib blastLib alignmentTheory 9open riscvTheory 10 11val () = Theory.new_theory "riscv_step" 12 13val ERR = mk_HOL_ERR "riscv_stepTheory"; 14 15val () = 16 ( List.app (fn f => f ()) 17 [numLib.prefer_num, wordsLib.prefer_word, wordsLib.guess_lengths] 18 ; show_assums := true 19 ; General.ignore (Parse.hide "imm") 20 ) 21 22fun uprove a b = utilsLib.STRIP_UNDISCH (Q.prove (a, b)) 23 24(* ------------------------------------------------------------------------ 25 Simplified Fetch and Next functions 26 ------------------------------------------------------------------------ *) 27 28val Fetch_def = Define` 29 Fetch s = 30 let (w, s) = translateAddr (PC s, Instruction, Read) s in 31 (rawReadInst (THE w) s, s)` 32 33val update_pc_def = Define `update_pc v s = SOME (write'PC v s)` 34 35val NextRISCV_def = Define` 36 NextRISCV s = 37 let (w, s) = Fetch s in 38 let s = Run (Decode w) s in 39 if s.exception <> NoException then 40 NONE 41 else 42 let pc = PC s in 43 case NextFetch s of 44 NONE => update_pc (pc + 4w) s 45 | SOME (BranchTo a) => update_pc a (write'NextFetch NONE s) 46 | _ => NONE` 47 48(* ------------------------------------------------------------------------ 49 Evaluation theorem 50 ------------------------------------------------------------------------ *) 51 52val NextRISCV = Q.store_thm("NextRISCV", 53 `(Fetch s = (w, s')) /\ 54 (Decode w = i) /\ 55 (Run i s' = nxt) /\ 56 (nxt.exception = NoException) /\ 57 (nxt.c_NextFetch nxt.procID = NONE) ==> 58 (NextRISCV s = update_pc (nxt.c_PC nxt.procID + 4w) nxt)`, 59 lrw [NextRISCV_def, PC_def, NextFetch_def, write'NextFetch_def] 60 \\ Cases_on `Run (Decode w) s'` 61 \\ fs [] 62 ) 63 64val NextRISCV_branch = Q.store_thm("NextRISCV_branch", 65 `(Fetch s = (w, s')) /\ 66 (Decode w = i) /\ 67 (Run i s' = nxt) /\ 68 (nxt.exception = NoException) /\ 69 (nxt.c_NextFetch nxt.procID = SOME (BranchTo a)) ==> 70 (NextRISCV s = 71 update_pc a 72 (nxt with c_NextFetch := (nxt.procID =+ NONE) nxt.c_NextFetch))`, 73 lrw [NextRISCV_def, PC_def, NextFetch_def, write'NextFetch_def] 74 \\ Cases_on `Run (Decode w) s'` 75 \\ fs [] 76 ) 77 78val NextRISCV_cond_branch = Q.store_thm("NextRISCV_cond_branch", 79 `(Fetch s = (w, s')) /\ 80 (Decode w = i) /\ 81 (Run i s' = nxt) /\ 82 (nxt.exception = NoException) /\ 83 (nxt.c_NextFetch nxt.procID = if b then SOME (BranchTo a) else NONE) ==> 84 (NextRISCV s = 85 update_pc (if b then a else nxt.c_PC nxt.procID + 4w) 86 (nxt with c_NextFetch := (nxt.procID =+ NONE) nxt.c_NextFetch))`, 87 lrw [NextRISCV_def, PC_def, NextFetch_def, write'NextFetch_def] 88 \\ Cases_on `Run (Decode w) s'` 89 \\ fs [update_pc_def, write'PC_def, riscv_state_component_equality, 90 combinTheory.UPDATE_APPLY_IMP_ID] 91 ) 92 93(* ------------------------------------------------------------------------ 94 Sub-word select operation (temporary) 95 ------------------------------------------------------------------------ *) 96 97val select_def = zDefine` 98 select (p:'a word) (w: word64) = 99 let sz = 64 DIV (2 ** dimindex(:'a)) in 100 let l = w2n p * sz in 101 (l + sz - 1 >< l) w : 'b word` 102 103(* ------------------------------------------------------------------------ 104 Word extend abbreviations 105 ------------------------------------------------------------------------ *) 106 107val () = List.app Parse.temp_overload_on 108 [ 109 ("s_extend32", ``\w: word64. sw2sw ((31 >< 0) w : word32) : word64``), 110 ("z_extend32", ``\w: word64. w2w ((31 >< 0) w : word32) : word64``), 111 ("s_extend16", ``\w: word64. sw2sw ((15 >< 0) w : word16) : word64``), 112 ("z_extend16", ``\w: word64. w2w ((15 >< 0) w : word16) : word64``), 113 ("s_extend8", ``\w: word64. sw2sw ((7 >< 0) w : word8) : word64``), 114 ("z_extend8", ``\w: word64. w2w ((7 >< 0) w : word8) : word64``) 115 ] 116 117(* ------------------------------------------------------------------------ 118 Simplifying Rewrites 119 ------------------------------------------------------------------------ *) 120 121val cond_lem1 = Q.prove( 122 `(if b1 then (if b2 then x else y1) else (if b2 then x else y2)) = 123 (if b2 then x else if b1 then y1 else y2)`, 124 rw [] 125 ) 126 127val cond_rand_shift = Q.prove( 128 `((if b then x else y) << n = if b then x << n else y << n) /\ 129 ((if b then x else y) >>> n = if b then x >>> n else y >>> n)`, 130 rw [] 131 ) 132 133val cond_rand_thms = 134 utilsLib.mk_cond_rand_thms 135 [pairSyntax.fst_tm, 136 pairSyntax.snd_tm, 137 wordsSyntax.sw2sw_tm, 138 wordsSyntax.w2w_tm, 139 wordsSyntax.word_add_tm, 140 wordsSyntax.word_and_tm, 141 wordsSyntax.word_or_tm, 142 wordsSyntax.word_xor_tm, 143 ``(=):Architecture -> Architecture -> bool``, 144 ``(=):'a word -> 'a word -> bool``, 145 ``(h >< l) : 'a word -> 'b word`` 146 ] 147 148val ifTF = Q.prove(`(if b then T else F) = b`, rw []) 149 150val v2w_0_rwts = Q.store_thm("v2w_0_rwts", 151 `((v2w [F; F; F; F; F] = 0w: word5)) /\ 152 ((v2w [T; b3; b2; b1; b0] = 0w: word5) = F) /\ 153 ((v2w [b3; T; b2; b1; b0] = 0w: word5) = F) /\ 154 ((v2w [b3; b2; T; b1; b0] = 0w: word5) = F) /\ 155 ((v2w [b3; b2; b1; T; b0] = 0w: word5) = F) /\ 156 ((v2w [b3; b2; b1; b0; T] = 0w: word5) = F)`, 157 blastLib.BBLAST_TAC 158 ) 159 160val aligned2 = Q.prove( 161 `(!w: word64. ((1 >< 0) w = 0w: word2) = aligned 2 w)`, 162 simp [alignmentTheory.aligned_extract] 163 \\ blastLib.BBLAST_TAC 164 ) 165 166val aligned3 = Q.prove( 167 `(!w: word64. (w2n ((2 >< 0) w: word3) = 0) = aligned 3 w)`, 168 simp [alignmentTheory.aligned_extract] 169 \\ blastLib.BBLAST_TAC 170 ) 171 172val address_align = blastLib.BBLAST_PROVE 173 ``w2w ((63 >< 3) a : 61 word) << 3 = (63 '' 3) (a: word64)`` 174 175val address_align2 = blastLib.BBLAST_PROVE 176 ``w2w ((63 >< 3) a + 1w: 61 word) << 3 = (63 '' 3) (a: word64) + 8w`` 177 178val address_aligned3 = uprove 179 `aligned 3 (a: word64) ==> ((63 '' 3) a = a)` 180 ( 181 simp [alignmentTheory.aligned_extract] 182 \\ blastLib.BBLAST_TAC 183 ) 184 185val words_of_dword = Q.prove( 186 `!b7:word8 b6:word8 b5:word8 b4:word8 b3:word8 b2:word8 b1:word8 b0:word8. 187 ((63 >< 32) ( b7 @@ b6 @@ b5 @@ b4 @@ b3 @@ b2 @@ b1 @@ b0 ) = 188 b7 @@ b6 @@ b5 @@ b4) /\ 189 ((31 >< 0 ) ( b7 @@ b6 @@ b5 @@ b4 @@ b3 @@ b2 @@ b1 @@ b0 ) = 190 b3 @@ b2 @@ b1 @@ b0)`, 191 simp_tac (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 192 ) 193 194val read_word = uprove 195 `aligned 2 (a: word64) ==> 196 ((if word_bit 2 a then 197 (63 >< 32) 198 (mem ((63 '' 3) a + 7w) @@ 199 mem ((63 '' 3) a + 6w) @@ 200 mem ((63 '' 3) a + 5w) @@ 201 mem ((63 '' 3) a + 4w) @@ 202 mem ((63 '' 3) a + 3w) @@ 203 mem ((63 '' 3) a + 2w) @@ 204 mem ((63 '' 3) a + 1w) @@ 205 mem ((63 '' 3) a)) : word32 206 else 207 (31 >< 0) 208 (mem ((63 '' 3) a + 7w) @@ 209 mem ((63 '' 3) a + 6w) @@ 210 mem ((63 '' 3) a + 5w) @@ 211 mem ((63 '' 3) a + 4w) @@ 212 mem ((63 '' 3) a + 3w) @@ 213 mem ((63 '' 3) a + 2w) @@ 214 mem ((63 '' 3) a + 1w) @@ 215 mem ((63 '' 3) a))) = 216 mem (a + 3w) @@ mem (a + 2w) @@ mem (a + 1w) @@ (mem a : word8))` 217 ( 218 rewrite_tac [GSYM aligned2, words_of_dword] 219 \\ strip_tac 220 \\ CASE_TAC 221 >| [ 222 `(63 '' 3) a = a - 4w` by blastLib.FULL_BBLAST_TAC, 223 `(63 '' 3) a = a` by blastLib.FULL_BBLAST_TAC 224 ] 225 \\ simp [] 226 ) 227 228val tac = 229 lrw [select_def, alignmentTheory.aligned_extract] 230 >| [ 231 `(2 >< 2) x = 0w: word1` by blastLib.FULL_BBLAST_TAC, 232 `((2 >< 2) x = 1w: word1) /\ 233 ((2 >< 0) x = 4w: word3)` by blastLib.FULL_BBLAST_TAC, 234 `(2 >< 2) y = 0w: word1` by blastLib.FULL_BBLAST_TAC, 235 `((2 >< 2) y = 1w: word1) /\ 236 ((2 >< 0) y = 4w: word3)` by blastLib.FULL_BBLAST_TAC 237 ] 238 \\ simp [] 239 \\ blastLib.FULL_BBLAST_TAC 240 241val aligned_select_word_s = uprove 242 `aligned 2 (if b then (x: word64) else y) ==> 243 ((if aligned 3 (if b then x else y) then 244 s_extend32 w0 245 else 246 s_extend32 247 ((63 >< 0) 248 (((w1: word64) @@ w0) >> 249 (w2n (if b then (2 >< 0) x else (2 >< 0) y : word3) * 8)))) = 250 s_extend32 (select (if b then (2 >< 2) x else (2 >< 2) y : word1) w0))` 251 tac 252 253val aligned_select_word_z = uprove 254 `aligned 2 (if b then (x: word64) else y) ==> 255 ((if aligned 3 (if b then x else y) then 256 z_extend32 w0 257 else 258 z_extend32 259 ((63 >< 0) 260 (((w1: word64) @@ w0) >> 261 (w2n (if b then (2 >< 0) x else (2 >< 0) y : word3) * 8)))) = 262 z_extend32 (select (if b then (2 >< 2) x else (2 >< 2) y : word1) w0))` 263 tac 264 265val select_word = Q.prove( 266 `aligned 2 (a: word64) ==> 267 ((31 >< 0) 268 (select ((2 >< 2) a : word1) 269 (mem ((63 '' 3) a + 7w) @@ 270 mem ((63 '' 3) a + 6w) @@ 271 mem ((63 '' 3) a + 5w) @@ 272 mem ((63 '' 3) a + 4w) @@ 273 mem ((63 '' 3) a + 3w) @@ 274 mem ((63 '' 3) a + 2w) @@ 275 mem ((63 '' 3) a + 1w) @@ 276 mem ((63 '' 3) a )) : word64) = 277 mem (a + 3w) @@ mem (a + 2w) @@ mem (a + 1w) @@ (mem a : word8))`, 278 lrw [alignmentTheory.aligned_extract, select_def] 279 \\ wordsLib.Cases_on_word_value `(2 >< 2) a : word1` 280 >| [ 281 `(63 '' 3) a = a - 4w` by blastLib.FULL_BBLAST_TAC, 282 `(63 '' 3) a = a` by blastLib.FULL_BBLAST_TAC 283 ] 284 \\ simp [] 285 \\ simp_tac (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 286 ) 287 |> Q.INST [`a` |-> `if b then x else y`, `mem` |-> `s.MEM8`] 288 |> REWRITE_RULE [cond_rand_thms] 289 |> utilsLib.STRIP_UNDISCH 290 291val tac = 292 lrw [select_def, alignmentTheory.aligned_extract] 293 >| [ 294 `(2 >< 1) x = 0w: word2` by blastLib.FULL_BBLAST_TAC, 295 `(2 >< 1) x IN {1w; 2w; 3w: word2}` 296 by (wordsLib.Cases_on_word_value `(2 >< 1) x : word2` 297 \\ fs [] 298 \\ blastLib.FULL_BBLAST_TAC 299 ) 300 \\ fs [] 301 >| [ 302 `(2 >< 0) x = 2w: word3` by blastLib.FULL_BBLAST_TAC, 303 `(2 >< 0) x = 4w: word3` by blastLib.FULL_BBLAST_TAC, 304 `(2 >< 0) x = 6w: word3` by blastLib.FULL_BBLAST_TAC 305 ], 306 `(2 >< 1) y = 0w: word2` by blastLib.FULL_BBLAST_TAC, 307 `(2 >< 1) y IN {1w; 2w; 3w: word2}` 308 by (wordsLib.Cases_on_word_value `(2 >< 1) y : word2` 309 \\ fs [] 310 \\ blastLib.FULL_BBLAST_TAC 311 ) 312 \\ fs [] 313 >| [ 314 `(2 >< 0) y = 2w: word3` by blastLib.FULL_BBLAST_TAC, 315 `(2 >< 0) y = 4w: word3` by blastLib.FULL_BBLAST_TAC, 316 `(2 >< 0) y = 6w: word3` by blastLib.FULL_BBLAST_TAC 317 ] 318 ] 319 \\ simp [] 320 \\ blastLib.FULL_BBLAST_TAC 321 322val aligned_select_half_s = uprove 323 `aligned 1 (if b then (x: word64) else y) ==> 324 ((if aligned 3 (if b then x else y) then 325 s_extend16 w0 326 else 327 s_extend16 328 ((63 >< 0) 329 (((w1: word64) @@ w0) >> 330 (w2n (if b then (2 >< 0) x else (2 >< 0) y : word3) * 8)))) = 331 s_extend16 (select (if b then (2 >< 1) x else (2 >< 1) y : word2) w0))` 332 tac 333 334val aligned_select_half_z = uprove 335 `aligned 1 (if b then (x: word64) else y) ==> 336 ((if aligned 3 (if b then x else y) then 337 z_extend16 w0 338 else 339 z_extend16 340 ((63 >< 0) 341 (((w1: word64) @@ w0) >> 342 (w2n (if b then (2 >< 0) x else (2 >< 0) y : word3) * 8)))) = 343 z_extend16 (select (if b then (2 >< 1) x else (2 >< 1) y : word2) w0))` 344 tac 345 346val select_half = Q.prove( 347 `aligned 1 (a: word64) ==> 348 ((15 >< 0) 349 (select ((2 >< 1) a : word2) 350 (mem ((63 '' 3) a + 7w) @@ 351 mem ((63 '' 3) a + 6w) @@ 352 mem ((63 '' 3) a + 5w) @@ 353 mem ((63 '' 3) a + 4w) @@ 354 mem ((63 '' 3) a + 3w) @@ 355 mem ((63 '' 3) a + 2w) @@ 356 mem ((63 '' 3) a + 1w) @@ 357 mem ((63 '' 3) a )) : word64) = 358 mem (a + 1w) @@ (mem a : word8))`, 359 lrw [alignmentTheory.aligned_extract, select_def] 360 \\ wordsLib.Cases_on_word_value `(2 >< 1) a : word2` 361 >| [ 362 `(63 '' 3) a = a - 6w` by blastLib.FULL_BBLAST_TAC, 363 `(63 '' 3) a = a - 4w` by blastLib.FULL_BBLAST_TAC, 364 `(63 '' 3) a = a - 2w` by blastLib.FULL_BBLAST_TAC, 365 `(63 '' 3) a = a` by blastLib.FULL_BBLAST_TAC 366 ] 367 \\ simp [] 368 \\ simp_tac (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 369 ) 370 |> Q.INST [`a` |-> `if b then x else y`, `mem` |-> `s.MEM8`] 371 |> REWRITE_RULE [cond_rand_thms] 372 |> utilsLib.STRIP_UNDISCH 373 374val tac = 375 lrw [select_def, alignmentTheory.aligned_extract] 376 \\ fs [] 377 >| [ 378 `(2 >< 0) x : word3 = 0w` by blastLib.FULL_BBLAST_TAC, 379 `(2 >< 0) y : word3 = 0w` by blastLib.FULL_BBLAST_TAC, 380 wordsLib.Cases_on_word_value `(2 >< 0) x : word3`, 381 wordsLib.Cases_on_word_value `(2 >< 0) y : word3` 382 ] 383 \\ simp [] 384 \\ blastLib.BBLAST_TAC 385 386val aligned_select_byte_s = Q.prove( 387 `(if aligned 3 (if b then (x: word64) else y) then 388 s_extend8 w0 389 else 390 s_extend8 391 ((63 >< 0) 392 (((w1: word64) @@ w0) >> 393 (w2n (if b then (2 >< 0) x else (2 >< 0) y : word3) * 8)))) = 394 s_extend8 (select (if b then (2 >< 0) x else (2 >< 0) y : word3) w0)`, 395 tac 396 ) 397 398val aligned_select_byte_z = Q.prove( 399 `(if aligned 3 (if b then (x: word64) else y) then 400 z_extend8 w0 401 else 402 z_extend8 403 ((63 >< 0) 404 (((w1: word64) @@ w0) >> 405 (w2n (if b then (2 >< 0) x else (2 >< 0) y : word3) * 8)))) = 406 z_extend8 (select (if b then (2 >< 0) x else (2 >< 0) y : word3) w0)`, 407 tac 408 ) 409 410val select_byte = Q.prove( 411 `((7 >< 0) 412 (select ((2 >< 0) a : word3) 413 (mem ((63 '' 3) a + 7w) @@ 414 mem ((63 '' 3) a + 6w) @@ 415 mem ((63 '' 3) a + 5w) @@ 416 mem ((63 '' 3) a + 4w) @@ 417 mem ((63 '' 3) a + 3w) @@ 418 mem ((63 '' 3) a + 2w) @@ 419 mem ((63 '' 3) a + 1w) @@ 420 mem ((63 '' 3) a )) : word64) = 421 ((mem: word64 -> word8) a))`, 422 lrw [alignmentTheory.aligned_extract, select_def] 423 \\ wordsLib.Cases_on_word_value `(2 >< 0) a : word3` 424 >| [ 425 `(63 '' 3) a = a - 7w` by blastLib.FULL_BBLAST_TAC, 426 `(63 '' 3) a = a - 6w` by blastLib.FULL_BBLAST_TAC, 427 `(63 '' 3) a = a - 5w` by blastLib.FULL_BBLAST_TAC, 428 `(63 '' 3) a = a - 4w` by blastLib.FULL_BBLAST_TAC, 429 `(63 '' 3) a = a - 3w` by blastLib.FULL_BBLAST_TAC, 430 `(63 '' 3) a = a - 2w` by blastLib.FULL_BBLAST_TAC, 431 `(63 '' 3) a = a - 1w` by blastLib.FULL_BBLAST_TAC, 432 `(63 '' 3) a = a` by blastLib.FULL_BBLAST_TAC 433 ] 434 \\ simp [] 435 \\ simp_tac (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 436 ) 437 |> Q.INST [`a` |-> `if b then x else y`, `mem` |-> `s.MEM8`] 438 |> REWRITE_RULE [cond_rand_thms] 439 440val byte_access = Q.prove( 441 `w2n ((2 >< 0) a : word3) + 1 <= 8`, 442 wordsLib.n2w_INTRO_TAC 4 443 \\ blastLib.FULL_BBLAST_TAC 444 ) 445 446val aligned1_aligned3 = uprove 447 `aligned 1 (a: word64) ==> (aligned 3 a = ((2 >< 1) a = 0w: word2))` 448 (simp [alignmentTheory.aligned_extract] \\ blastLib.BBLAST_TAC) 449 450val aligned1_aligned3b = uprove 451 `aligned 1 (a: word64) ==> w2n ((2 >< 0) a : word3) + 2 <= 8` 452 ( 453 rw [alignmentTheory.aligned_extract] 454 \\ wordsLib.n2w_INTRO_TAC 4 455 \\ blastLib.FULL_BBLAST_TAC 456 ) 457 458val aligned2_aligned3 = uprove 459 `aligned 2 (a: word64) ==> (aligned 3 a = ((2 >< 2) a = 0w: word1))` 460 (simp [alignmentTheory.aligned_extract] \\ blastLib.BBLAST_TAC) 461 462val aligned2_aligned3b = uprove 463 `aligned 2 (a: word64) ==> w2n ((2 >< 0) a : word3) + 4 <= 8` 464 ( 465 rw [alignmentTheory.aligned_extract] 466 \\ wordsLib.n2w_INTRO_TAC 4 467 \\ blastLib.FULL_BBLAST_TAC 468 ) 469 470val w = 471 List.tabulate (8, fn i => Term.mk_var ("b" ^ Int.toString i, ``:word8``)) 472val w = List.foldl wordsSyntax.mk_word_concat (hd w) (tl w) 473 474val extract_thms = Q.prove( 475 `((7 >< 0 ) ^w = b0) /\ ((15 >< 8 ) ^w = b1) /\ ((23 >< 16) ^w = b2) /\ 476 ((31 >< 24) ^w = b3) /\ ((39 >< 32) ^w = b4) /\ ((47 >< 40) ^w = b5) /\ 477 ((55 >< 48) ^w = b6) /\ ((63 >< 56) ^w = b7)`, 478 simp_tac (std_ss++wordsLib.SIZES_ss++wordsLib.WORD_EXTRACT_ss) 479 [wordsTheory.SHIFT_ZERO, wordsTheory.WORD_OR_CLAUSES] 480 ) 481 482val not1 = uprove 483 `a <> 1w: word2 ==> 484 ((if a = 0w then x1 485 else if a = 2w then x2 486 else if a = 3w then x3 487 else x4) = 488 (if a = 0w then x1 489 else if a = 2w then x2 490 else x3))` 491 (rw [] \\ blastLib.FULL_BBLAST_TAC) 492 493val extract_over_add = 494 wordsTheory.WORD_EXTRACT_OVER_ADD 495 |> Q.ISPECL [`a: word64`, `b: word64`, `31n`] 496 |> INST_TYPE [Type.beta |-> ``:32``] 497 |> SIMP_RULE (srw_ss()) [] 498 |> GSYM 499 500val jal = uprove 501 `aligned 2 (pc: word64) /\ ~word_lsb (imm: word20) ==> 502 aligned 2 (pc + sw2sw imm << 1)` 503 ( 504 simp [alignmentTheory.aligned_extract] \\ blastLib.BBLAST_TAC 505 ) 506 507val jalr = uprove 508 `(b \/ aligned 2 x) /\ ~(imm: word12 ' 1) ==> 509 aligned 2 (if b then sw2sw imm && 0xFFFFFFFFFFFFFFFEw : word64 510 else x + sw2sw imm && 0xFFFFFFFFFFFFFFFEw)` 511 ( 512 rw [alignmentTheory.aligned_extract] 513 \\ blastLib.FULL_BBLAST_TAC 514 ) 515 516(* ------------------------------------------------------------------------ 517 Evaluation setup 518 ------------------------------------------------------------------------ *) 519 520val s = ``s:riscv_state`` 521val rd0 = ``rd = 0w: word5`` 522val bare = ``(^s.c_MCSR ^s.procID).mstatus.VM = 0w`` 523val archbase = ``(^s.c_MCSR ^s.procID).mcpuid.ArchBase`` 524val shift = ``~((^archbase = 0w) /\ word_bit 5n (imm: word6))`` 525val aligned = ``aligned 2 (^s.c_PC ^s.procID)`` 526val aligned_d = 527 ``aligned 3 (if rs1 = 0w then sw2sw offs 528 else ^s.c_gpr ^s.procID rs1 + sw2sw (offs:word12))`` 529 530local 531 val cond_updates = utilsLib.mk_cond_update_thms [``:riscv_state``] 532 val datatype_rwts = 533 utilsLib.datatype_rewrites true "riscv" 534 ["riscv_state", "VM_Mode", "Architecture"] 535 fun riscv_thms thms = 536 thms @ cond_updates @ datatype_rwts @ 537 [wordsTheory.WORD_EXTRACT_ZERO2, wordsTheory.ZERO_SHIFT, 538 wordsTheory.WORD_ADD_0, wordsTheory.WORD_MULT_CLAUSES, 539 wordsTheory.WORD_AND_CLAUSES, wordsTheory.WORD_OR_CLAUSES, 540 wordsTheory.WORD_XOR_CLAUSES, wordsTheory.w2w_0, wordsTheory.sw2sw_0, 541 ifTF, cond_lem1, extract_over_add, cond_rand_shift, cond_rand_thms 542 ] 543in 544 fun step_conv b = 545 utilsLib.setStepConv 546 (if b then 547 Conv.DEPTH_CONV wordsLib.SIZES_CONV 548 THENC utilsLib.WGROUND_CONV 549 else 550 ALL_CONV) 551 val ev = utilsLib.STEP (riscv_thms, s) 552 fun EV a b c d = hd (ev a b c d) 553end 554 555local 556 val word_eq_ss = 557 simpLib.std_conv_ss 558 {name = "word_eq_ss", conv = wordsLib.word_EQ_CONV, 559 pats = [``n2w a = n2w b: word64``]} 560in 561 val store_tac = 562 asm_simp_tac (std_ss++wordsLib.WORD_ss) 563 [GSYM wordsTheory.WORD_EXTRACT_OVER_BITWISE, extract_thms] 564 \\ simp_tac (std_ss++wordsLib.SIZES_ss++wordsLib.WORD_EXTRACT_ss) 565 [wordsTheory.SHIFT_ZERO, wordsTheory.WORD_OR_CLAUSES] 566 \\ simp_tac 567 (std_ss++wordsLib.WORD_ARITH_ss++wordsLib.WORD_CANCEL_ss++word_eq_ss) 568 [updateTheory.UPDATE_APPLY_IMP_ID, combinTheory.UPDATE_APPLY] 569end 570 571(* ------------------------------------------------------------------------ 572 Architecture Rewrites 573 ------------------------------------------------------------------------ *) 574 575val () = step_conv false 576 577val translateAddr = EV 578 [translateAddr_def, MCSR_def, vmType_def, pairTheory.pair_case_thm] 579 [[bare]] [] 580 ``translateAddr (vPC, ft, ac)`` 581 582val in32BitMode = EV 583 [in32BitMode_def, curArch_def, MCSR_def, architecture_def, not1] [] [] 584 ``in32BitMode()`` 585 586val PC = EV [PC_def] [] [] ``PC`` 587 588val rawReadInst = EV 589 [rawReadInst_def, MEM_def, address_align, read_word] [] [] 590 ``rawReadInst a`` 591 592val rawReadData = EV 593 [rawReadData_def, aligned3, MEM_def, address_align, address_align2] 594 [] [] 595 ``rawReadData a`` 596 597val branchTo = EV 598 [branchTo_def, write'NextFetch_def] [] [] 599 ``branchTo newPC`` 600 601val GPR = EV [GPR_def, gpr_def] [] [] ``GPR n`` 602 603val write'GPR0 = 604 ev [write'GPR_def] [[``d = 0w:word5``]] [] 605 ``write'GPR (n, d)`` |> hd 606 607val write'GPR = 608 ev [write'GPR_def, write'gpr_def] [[``d <> 0w:word5``]] [] 609 ``write'GPR (n, d)`` |> hd 610 611val Fetch = Theory.save_thm("Fetch", 612 EV [Fetch_def, PC, translateAddr, rawReadInst] [[aligned]] [] 613 ``Fetch`` 614 ) 615 616val update_pc = Theory.save_thm("update_pc", 617 EV [update_pc_def, write'PC_def] [] [] ``update_pc v``) 618 619(* ------------------------------------------------------------------------ 620 Memory Store Rewrites 621 ------------------------------------------------------------------------ *) 622 623val () = step_conv true 624 625val write'MEM = EV [write'MEM_def] [] [] ``write'MEM (d, a)`` 626 627fun write_data_ev l1 l2 = 628 EV ([rawWriteData_def, aligned3, MEM_def, write'MEM, address_align] @ l1) l2 629 [] 630 631val rawWriteData8 = 632 write_data_ev [address_aligned3] [[``aligned 3 (a: word64)``]] 633 ``rawWriteData (a, d, 8)`` 634 635fun get_mem8 thm = 636 thm |> utilsLib.rhsc 637 |> boolSyntax.rator 638 |> boolSyntax.rand 639 |> boolSyntax.rand 640 641val rawWriteData4 = write_data_ev [aligned2_aligned3, aligned2_aligned3b] [] 642 ``rawWriteData (a, d, 4)`` 643 644val tm = get_mem8 rawWriteData4 645 646val thm = uprove 647 `aligned 2 a ==> 648 (^tm = (a =+ (7 >< 0) d) ((a + 1w =+ (15 >< 8) d) 649 ((a + 2w =+ (23 >< 16) d) ((a + 3w =+ (31 >< 24) d) s.MEM8))))` 650 ( 651 rw [alignmentTheory.aligned_extract] 652 \\ qabbrev_tac `mem = s.MEM8` 653 >- (`(63 '' 3) a = a` by blastLib.FULL_BBLAST_TAC \\ store_tac) 654 \\ `(2 >< 0) a : word3 = 4w: word3` by blastLib.FULL_BBLAST_TAC 655 \\ `(63 '' 3) a = a - 4w` by blastLib.FULL_BBLAST_TAC 656 \\ store_tac 657 ) 658 659val rawWriteData4 = utilsLib.INST_REWRITE_RULE [thm] rawWriteData4 660 661val rawWriteData2 = write_data_ev [aligned1_aligned3, aligned1_aligned3b] [] 662 ``rawWriteData (a, d, 2)`` 663 664val tm = get_mem8 rawWriteData2 665 666val thm = uprove 667 `aligned 1 a ==> (^tm = (a =+ (7 >< 0) d) ((a + 1w =+ (15 >< 8) d) s.MEM8))` 668 ( 669 rw [alignmentTheory.aligned_extract] 670 \\ qabbrev_tac `mem = s.MEM8` 671 >- (`(63 '' 3) a = a` by blastLib.FULL_BBLAST_TAC \\ store_tac) 672 \\ `(2 >< 0) a : word3 IN {2w; 4w; 6w: word3}` 673 by (simp [] \\ blastLib.FULL_BBLAST_TAC) 674 \\ fs [] 675 >| [ 676 `(63 '' 3) a = a - 2w` by blastLib.FULL_BBLAST_TAC, 677 `(63 '' 3) a = a - 4w` by blastLib.FULL_BBLAST_TAC, 678 `(63 '' 3) a = a - 6w` by blastLib.FULL_BBLAST_TAC 679 ] 680 \\ store_tac 681 ) 682 683val rawWriteData2 = utilsLib.INST_REWRITE_RULE [thm] rawWriteData2 684 685val rawWriteData1 = write_data_ev [byte_access] [] ``rawWriteData (a, d, 1)`` 686 687val tm = get_mem8 rawWriteData1 688 689val thm = Q.prove( 690 `^tm = (a =+ (7 >< 0) d) s.MEM8`, 691 rw [alignmentTheory.aligned_extract] 692 \\ qabbrev_tac `mem = s.MEM8` 693 >- (`(63 '' 3) a = a` by blastLib.FULL_BBLAST_TAC \\ store_tac) 694 \\ wordsLib.Cases_on_word_value `(2 >< 0) a: word3` 695 \\ fs [] 696 >| [ 697 `(63 '' 3) a = a - 7w` by blastLib.FULL_BBLAST_TAC, 698 `(63 '' 3) a = a - 6w` by blastLib.FULL_BBLAST_TAC, 699 `(63 '' 3) a = a - 5w` by blastLib.FULL_BBLAST_TAC, 700 `(63 '' 3) a = a - 4w` by blastLib.FULL_BBLAST_TAC, 701 `(63 '' 3) a = a - 3w` by blastLib.FULL_BBLAST_TAC, 702 `(63 '' 3) a = a - 2w` by blastLib.FULL_BBLAST_TAC, 703 `(63 '' 3) a = a - 1w` by blastLib.FULL_BBLAST_TAC, 704 blastLib.FULL_BBLAST_TAC 705 ] 706 \\ store_tac 707 ) 708 709val rawWriteData1 = REWRITE_RULE [thm] rawWriteData1 710 711(* ------------------------------------------------------------------------ 712 Instruction Rewrites 713 ------------------------------------------------------------------------ *) 714 715local 716 val l = 717 [GPR, in32BitMode, PC, wordsTheory.word_len_def, 718 branchTo, translateAddr, jal, jalr, aligned2, 719 aligned_select_word_s, aligned_select_word_z, select_word, 720 aligned_select_half_s, aligned_select_half_z, select_half, 721 aligned_select_byte_s, aligned_select_byte_z, select_byte, 722 rawReadData, rawWriteData8, rawWriteData4, rawWriteData2, rawWriteData1] 723 val hyp_eq_rule = 724 utilsLib.ALL_HYP_CONV_RULE (Conv.DEPTH_CONV wordsLib.word_EQ_CONV) 725in 726 val () = utilsLib.reset_thms() 727 fun class args avoid n = 728 let 729 val name = "dfn'" ^ n 730 val read = if Lib.mem n ["LD"] then [address_aligned3] else [] 731 val (write, n) = 732 if List.exists (Lib.mem rd0) avoid then 733 ([write'GPR0], n ^ "_NOP") 734 else 735 ([write'GPR], n) 736 val thms = DB.fetch "riscv" (name ^ "_def") :: write @ read 737 in 738 case ev (thms @ l) avoid [] (Parse.Term ([QUOTE name] @ args)) of 739 [th] => utilsLib.save_thms n [hyp_eq_rule th] 740 | _ => raise ERR "class" ("more than one theorem" ^ n) 741 end 742end 743 744fun class_rd0 args avoid n = 745 let 746 val f = class args 747 in 748 (f avoid n, 749 f (case avoid of 750 [] => [[rd0]] 751 | [l] => [rd0 :: l] 752 | _ => raise ERR "" "") n) 753 end 754 755val arithi = class_rd0 `(rd, rs1, imm)` 756 757val ADDI = arithi [] "ADDI" 758val ADDIW = arithi [[``^archbase <> 0w``]] "ADDIW" 759val SLTI = arithi [] "SLTI" 760val SLTIU = arithi [] "SLTIU" 761val ANDI = arithi [] "ANDI" 762val ORI = arithi [] "ORI" 763val XORI = arithi [] "XORI" 764val SLLI = arithi [[shift]] "SLLI" 765val SRLI = arithi [[shift]] "SRLI" 766val SRAI = arithi [[shift]] "SRAI" 767val SLLIW = arithi [[``^archbase <> 0w``]] "SLLIW" 768val SRLIW = arithi [[``^archbase <> 0w``]] "SRLIW" 769val SRAIW = arithi [[``^archbase <> 0w``]] "SRAIW" 770 771val arithi = class_rd0 `(rd, imm)` [] 772 773val LUI = arithi "LUI" 774val AUIPC = arithi "AUIPC" 775 776val arithr = class_rd0 `(rd, rs1, rs2)` 777 778val ADD = arithr [] "ADD" 779val ADDW = arithr [[``^archbase <> 0w``]] "ADDW" 780val SUB = arithr [] "SUB" 781val SUBW = arithr [[``^archbase <> 0w``]] "SUBW" 782val SLT = arithr [] "SLT" 783val SLTU = arithr [] "SLTU" 784val AND = arithr [] "AND" 785val OR = arithr [] "OR" 786val XOR = arithr [] "XOR" 787val SLL = arithr [] "SLL" 788val SRL = arithr [] "SRL" 789val SRA = arithr [] "SRA" 790val SLLW = arithr [[``^archbase <> 0w``]] "SLLW" 791val SRLW = arithr [[``^archbase <> 0w``]] "SRLW" 792val SRAW = arithr [[``^archbase <> 0w``]] "SRAW" 793 794val MUL = arithr [] "MUL" 795val MULH = arithr [] "MULH" 796val MULHU = arithr [] "MULHU" 797val MULHSU = arithr [] "MULHSU" 798val MULW = arithr [[``^archbase <> 0w``]] "MULW" 799val DIV = arithr [] "DIV" 800val REM = arithr [] "REM" 801val DIVU = arithr [] "DIVU" 802val REMU = arithr [] "REMU" 803val DIVW = arithr [[``^archbase <> 0w``]] "DIVW" 804val REMW = arithr [[``^archbase <> 0w``]] "REMW" 805val DIVUW = arithr [[``^archbase <> 0w``]] "DIVUW" 806val REMUW = arithr [[``^archbase <> 0w``]] "REMUW" 807 808val JAL = class_rd0 `(rd, imm)` [] "JAL" 809val JALR = class_rd0 `(rd, rs1, imm)` [] "JALR" 810 811val cbranch = class `(rs1, rs2, offs)` [] 812 813val BEQ = cbranch "BEQ" 814val BNE = cbranch "BNE" 815val BLT = cbranch "BLT" 816val BLTU = cbranch "BLTU" 817val BGE = cbranch "BGE" 818val BGEU = cbranch "BGEU" 819 820val load = class_rd0 `(rd, rs1, offs)` 821 822val LD = load [[``^archbase <> 0w``, aligned_d]] "LD" 823val LW = load [] "LW" 824val LH = load [] "LH" 825val LB = load [] "LB" 826val LWU = load [[``^archbase <> 0w``]] "LWU" 827val LHU = load [[``^archbase <> 0w``]] "LHU" 828val LBU = load [[``^archbase <> 0w``]] "LBU" 829 830val store = class `(rs1, rs2, offs)` 831 832val SD = store [[``^archbase <> 0w``, aligned_d]] "SD" 833val SW = store [] "SW" 834val SH = store [] "SH" 835val SB = store [] "SB" 836 837(* ------------------------------------------------------------------------ *) 838 839val () = ( Theory.delete_const "select" 840 ; utilsLib.adjoin_thms () 841 ; export_theory () 842 ) 843