blob: d6ca4d7db862435d35107c7674c881a4c36a5cba (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
theory Riscv_duopod_lemmas
imports
Sail.Sail_values_lemmas
Sail.State_lemmas
Riscv_duopod
begin
abbreviation "liftS \<equiv> liftState (get_regval, set_regval)"
lemmas register_defs = get_regval_def set_regval_def Xs_ref_def nextPC_ref_def PC_ref_def
lemma regval_vector_64_dec_bit[simp]:
"vector_64_dec_bit_of_regval (regval_of_vector_64_dec_bit v) = Some v"
by (auto simp: regval_of_vector_64_dec_bit_def)
lemma vector_of_rv_rv_of_vector[simp]:
assumes "\<And>v. of_rv (rv_of v) = Some v"
shows "vector_of_regval of_rv (regval_of_vector rv_of len is_inc v) = Some v"
proof -
from assms have "of_rv \<circ> rv_of = Some" by auto
then show ?thesis by (auto simp: vector_of_regval_def regval_of_vector_def)
qed
lemma liftS_read_reg_Xs[simp]:
"liftS (read_reg Xs_ref) = readS (Xs \<circ> regstate)"
by (auto simp: liftState_read_reg_readS register_defs)
lemma liftS_write_reg_Xs[simp]:
"liftS (write_reg Xs_ref v) = updateS (regstate_update (Xs_update (\<lambda>_. v)))"
by (auto simp: liftState_write_reg_updateS register_defs)
lemma liftS_read_reg_nextPC[simp]:
"liftS (read_reg nextPC_ref) = readS (nextPC \<circ> regstate)"
by (auto simp: liftState_read_reg_readS register_defs)
lemma liftS_write_reg_nextPC[simp]:
"liftS (write_reg nextPC_ref v) = updateS (regstate_update (nextPC_update (\<lambda>_. v)))"
by (auto simp: liftState_write_reg_updateS register_defs)
lemma liftS_read_reg_PC[simp]:
"liftS (read_reg PC_ref) = readS (PC \<circ> regstate)"
by (auto simp: liftState_read_reg_readS register_defs)
lemma liftS_write_reg_PC[simp]:
"liftS (write_reg PC_ref v) = updateS (regstate_update (PC_update (\<lambda>_. v)))"
by (auto simp: liftState_write_reg_updateS register_defs)
end
|
