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