1open HolKernel boolLib bossLib
2open stateLib set_sepTheory progTheory riscv_stepTheory
3
4val () = new_theory "riscv_prog"
5
6(* ------------------------------------------------------------------------ *)
7
8val _ = stateLib.sep_definitions "riscv" []
9          (List.map Lib.list_of_singleton
10             ["c_update", "log", "totalCore", "done", "clock", "c_tlb",
11              "c_instret", "c_cycles", "c_UCSR", "c_SCSR", "c_ReserveLoad",
12              "c_HCSR", "c_ExitCode"])
13          riscv_stepTheory.NextRISCV_def
14
15val riscv_instr_def = Define`
16   riscv_instr (a, i: word32) =
17   { (riscv_c_MEM8 a, riscv_d_word8 ((7 >< 0) i));
18     (riscv_c_MEM8 (a + 1w), riscv_d_word8 ((15 >< 8) i));
19     (riscv_c_MEM8 (a + 2w), riscv_d_word8 ((23 >< 16) i));
20     (riscv_c_MEM8 (a + 3w), riscv_d_word8 ((31 >< 24) i)) }`;
21
22val riscv_proj_def = DB.definition "riscv_proj_def"
23
24val RISCV_MODEL_def = Define`
25  RISCV_MODEL =
26    (STATE riscv_proj, NEXT_REL (=) NextRISCV, riscv_instr,
27     ($= :riscv_state -> riscv_state -> bool), K F : riscv_state -> bool)`
28
29val RISCV_IMP_SPEC = Theory.save_thm ("RISCV_IMP_SPEC",
30  stateTheory.IMP_SPEC
31  |> Q.ISPECL [`riscv_proj`, `NextRISCV`, `riscv_instr`]
32  |> REWRITE_RULE [GSYM RISCV_MODEL_def]
33  )
34
35val RISCV_IMP_TEMPORAL = Theory.save_thm ("RISCV_IMP_TEMPORAL",
36  temporal_stateTheory.IMP_TEMPORAL
37  |> Q.ISPECL [`riscv_proj`, `NextRISCV`, `riscv_instr`,
38               `(=) : riscv_state -> riscv_state -> bool`,
39               `K F : riscv_state -> bool`]
40  |> REWRITE_RULE [GSYM RISCV_MODEL_def]
41  )
42
43(* ------------------------------------------------------------------------ *)
44
45val riscv_ID_def = Define`
46   riscv_ID id mcsr =
47   riscv_exception NoException * riscv_procID id * riscv_c_NextFetch id NONE *
48   riscv_c_MCSR id mcsr * cond (mcsr.mstatus.VM = 0w)`
49
50val riscv_ID_PC_def = Define`
51  riscv_ID_PC id pc = riscv_c_PC id pc * cond (aligned 2 pc)`
52
53(* ------------------------------------------------------------------------
54   Specialize to RV64I, core 0
55   ------------------------------------------------------------------------ *)
56
57val riscv_RV64I_def = Define`
58  riscv_RV64I mcsr = cond (mcsr.mcpuid.ArchBase = 2w) * riscv_ID 0w mcsr`
59
60val riscv_REG_def = Define`riscv_REG  = riscv_c_gpr 0w`
61val riscv_PC_def = Define`riscv_PC = riscv_ID_PC 0w`
62
63(* ------------------------------------------------------------------------ *)
64
65val RISCV_PC_INTRO = Q.store_thm("RISCV_PC_INTRO",
66   `SPEC m (p1 * riscv_ID_PC c pc) code (p2 * riscv_c_PC c pc') ==>
67    (aligned 2 pc ==> aligned 2 pc') ==>
68    SPEC m (p1 * riscv_ID_PC c pc) code (p2 * riscv_ID_PC c pc')`,
69   REPEAT STRIP_TAC
70   \\ FULL_SIMP_TAC std_ss
71        [riscv_ID_PC_def, SPEC_MOVE_COND, STAR_ASSOC, SEP_CLAUSES]
72   )
73
74val RISCV_TEMPORAL_PC_INTRO = Q.store_thm("RISCV_TEMPORAL_PC_INTRO",
75   `TEMPORAL_NEXT m (p1 * riscv_ID_PC c pc) code (p2 * riscv_c_PC c pc') ==>
76    (aligned 2 pc ==> aligned 2 pc') ==>
77    TEMPORAL_NEXT m (p1 * riscv_ID_PC c pc) code (p2 * riscv_ID_PC c pc')`,
78   REPEAT STRIP_TAC
79   \\ FULL_SIMP_TAC std_ss
80        [riscv_ID_PC_def, temporal_stateTheory.TEMPORAL_NEXT_MOVE_COND,
81         STAR_ASSOC, SEP_CLAUSES]
82   )
83
84val cond_branch_aligned = Q.store_thm("cond_branch_aligned",
85  `(aligned 2 (pc: word64) ==>
86    aligned 2
87      (if b then
88         pc +
89         sw2sw (v2w [x0; x21; x1; x2; x3; x4;
90                     x5; x6; x17; x18; x19; x20] : word12) << 1
91       else pc + 4w)) = (aligned 2 pc /\ b ==> ~x20)`,
92  rw [alignmentTheory.aligned_extract]
93  \\ blastLib.FULL_BBLAST_TAC
94  )
95
96val jal_aligned = Q.store_thm("jal_aligned",
97  `(aligned 2 (pc: word64) ==> aligned 2 (pc + sw2sw (a: word20) << 1)) =
98   aligned 2 pc ==> ~word_lsb a`,
99  rw [alignmentTheory.aligned_extract]
100  \\ blastLib.BBLAST_TAC
101  )
102
103val jalr_aligned = Q.store_thm("jalr_aligned",
104  `~(a: word12) ' 1 /\ (b \/ aligned 2 (v: word64)) /\
105   (c ==> aligned 2 (if b then sw2sw a && 0xFFFFFFFFFFFFFFFEw
106                     else v + sw2sw a && 0xFFFFFFFFFFFFFFFEw)) =
107   ~(a: word12) ' 1 /\ (b \/ aligned 2 (v: word64))`,
108  rw [alignmentTheory.aligned_extract]
109  \\ blastLib.FULL_BBLAST_TAC
110  )
111
112(* ------------------------------------------------------------------------ *)
113
114val c_gpr_frame = Q.store_thm("c_gpr_frame",
115  `!c_gpr a b w s x.
116     riscv_c_c_gpr a b IN x ==>
117     (FRAME_STATE riscv_proj x
118         (s with c_gpr := (a =+ (b =+ w) (c_gpr a)) c_gpr) =
119      FRAME_STATE riscv_proj x (s with c_gpr := c_gpr))`,
120  rw [stateTheory.FRAME_STATE_def, stateTheory.SELECT_STATE_def,
121      set_sepTheory.fun2set_def, pred_setTheory.EXTENSION]
122  \\ eq_tac
123  \\ rw []
124  \\ Cases_on `a'`
125  \\ rw [combinTheory.APPLY_UPDATE_THM, riscv_proj_def]
126  \\ Cases_on `b = c0`
127  \\ fs []
128  )
129
130(* ------------------------------------------------------------------------ *)
131
132val riscv_opcode_bytes = Theory.save_thm("riscv_opcode_bytes",
133   blastLib.BBLAST_PROVE
134    ``(d @@ ((c @@ ((b @@ a) : word16)) : word24) = r: word32) =
135      (a = ( 7 ><  0) r : word8) /\
136      (b = (15 ><  8) r : word8) /\
137      (c = (23 >< 16) r : word8) /\
138      (d = (31 >< 24) r : word8)``)
139
140val () = export_theory()
141