diff options
Diffstat (limited to 'build/riscv_types.v')
| -rw-r--r-- | build/riscv_types.v | 599 |
1 files changed, 599 insertions, 0 deletions
diff --git a/build/riscv_types.v b/build/riscv_types.v new file mode 100644 index 0000000..2b32fd2 --- /dev/null +++ b/build/riscv_types.v @@ -0,0 +1,599 @@ +(*Generated by Sail from riscv.*) +Require Import Sail.Base. +Require Import Sail.Real. +Import ListNotations. +Open Scope string. +Open Scope bool. +Open Scope Z. + +Definition bits (n : Z) : Type := mword n. + +Definition xlen : Z := 64. +Hint Unfold xlen : sail. + +Definition xlen_bytes : Z := 8. +Hint Unfold xlen_bytes : sail. + +Definition xlenbits : Type := bits 64. + +Definition regtype : Type := xlenbits. + +Definition regno (n : Z)`{ArithFact ((0 <=? n) && (n <? 32))} : Type := Z. + +Definition regidx : Type := bits 5. + +Definition cregidx : Type := bits 3. + +Definition csreg : Type := bits 12. + +Inductive register_value := + | Regval_vector : list register_value -> register_value + | Regval_list : list register_value -> register_value + | Regval_option : option register_value -> register_value + | Regval_bit : bitU -> register_value + | Regval_bitvector_64_dec : mword 64 -> register_value. + +Arguments register_value : clear implicits. + +Record regstate := + { x31 : mword 64; + x30 : mword 64; + x29 : mword 64; + x28 : mword 64; + x27 : mword 64; + x26 : mword 64; + x25 : mword 64; + x24 : mword 64; + x23 : mword 64; + x22 : mword 64; + x21 : mword 64; + x20 : mword 64; + x19 : mword 64; + x18 : mword 64; + x17 : mword 64; + x16 : mword 64; + x15 : mword 64; + x14 : mword 64; + x13 : mword 64; + x12 : mword 64; + x11 : mword 64; + x10 : mword 64; + x9 : mword 64; + x8 : mword 64; + x7 : mword 64; + x6 : mword 64; + x5 : mword 64; + x4 : mword 64; + x3 : mword 64; + x2 : mword 64; + x1 : mword 64; + instbits : mword 64; + nextPC : mword 64; + PC : mword 64; }. + +Arguments regstate : clear implicits. + +Notation "{[ r 'with' 'x31' := e ]}" := + match r with Build_regstate _ f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate e f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x30' := e ]}" := + match r with Build_regstate f0 _ f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 e f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x29' := e ]}" := + match r with Build_regstate f0 f1 _ f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 e f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x28' := e ]}" := + match r with Build_regstate f0 f1 f2 _ f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 e f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x27' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 _ f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 e f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x26' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 _ f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 e f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x25' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 _ f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 e f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x24' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 _ f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 e f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x23' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 _ f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 e f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x22' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 _ f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 e f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x21' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 _ f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 e f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x20' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 _ f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 e f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x19' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 _ f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 e f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x18' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 _ f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 e f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x17' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 _ f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 e f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x16' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 _ f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 e f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x15' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 _ f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 e f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x14' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 _ f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 e f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x13' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 _ f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 e f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x12' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 _ f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 e f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x11' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 _ f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 e f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x10' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 _ f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 e f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x9' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 _ f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 e f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x8' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 _ f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 e f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x7' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 _ f25 f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 e f25 f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x6' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 _ f26 f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 e f26 f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x5' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 _ f27 f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 e f27 f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x4' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 _ f28 f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 e f28 f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x3' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 _ f29 f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 e f29 f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x2' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 _ f30 f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 e f30 f31 f32 f33 + end. +Notation "{[ r 'with' 'x1' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 _ f31 f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 e f31 f32 f33 + end. +Notation "{[ r 'with' 'instbits' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 _ f32 f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 e f32 f33 + end. +Notation "{[ r 'with' 'nextPC' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 _ f33 => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 e f33 + end. +Notation "{[ r 'with' 'PC' := e ]}" := + match r with Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 _ => + Build_regstate f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 e + end. + + + +Definition bit_of_regval (merge_var : register_value) : option bitU := + match merge_var with | Regval_bit v => Some v | _ => None end. + +Definition regval_of_bit (v : bitU) : register_value := Regval_bit v. + +Definition bitvector_64_dec_of_regval (merge_var : register_value) : + option (mword 64) := + match merge_var with | Regval_bitvector_64_dec v => Some v | _ => None end. + + +Definition regval_of_bitvector_64_dec (v : mword 64) : register_value := + Regval_bitvector_64_dec v. + + +Definition vector_of_regval {a} n (of_regval : register_value -> option a) + (rv : register_value) : option (vec a n) := + match rv with + | Regval_vector v => + if n =? length_list v then + map_bind (vec_of_list n) (just_list (List.map of_regval v)) + else None + | _ => None +end. + +Definition regval_of_vector {a size} (regval_of : a -> register_value) (xs : vec a size) : register_value := Regval_vector (List.map regval_of (list_of_vec xs)). + +Definition list_of_regval {a} (of_regval : register_value -> option a) + (rv : register_value) : option (list a) := + match rv with + | Regval_list v => just_list (List.map of_regval v) + | _ => None +end. + +Definition regval_of_list {a} (regval_of : a -> register_value) + (xs : list a) : register_value := + Regval_list (List.map regval_of xs). + +Definition option_of_regval {a} (of_regval : register_value -> option a) + (rv : register_value) : option (option a) := + match rv with + | Regval_option v => option_map of_regval v + | _ => None +end. + +Definition regval_of_option {a} (regval_of : a -> register_value) + (v : option a) := Regval_option (option_map regval_of v). + + +Definition x31_ref := {| + name := "x31"; + read_from := (fun s => s.(x31)); + write_to := (fun v s => ({[ s with x31 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x30_ref := {| + name := "x30"; + read_from := (fun s => s.(x30)); + write_to := (fun v s => ({[ s with x30 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x29_ref := {| + name := "x29"; + read_from := (fun s => s.(x29)); + write_to := (fun v s => ({[ s with x29 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x28_ref := {| + name := "x28"; + read_from := (fun s => s.(x28)); + write_to := (fun v s => ({[ s with x28 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x27_ref := {| + name := "x27"; + read_from := (fun s => s.(x27)); + write_to := (fun v s => ({[ s with x27 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x26_ref := {| + name := "x26"; + read_from := (fun s => s.(x26)); + write_to := (fun v s => ({[ s with x26 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x25_ref := {| + name := "x25"; + read_from := (fun s => s.(x25)); + write_to := (fun v s => ({[ s with x25 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x24_ref := {| + name := "x24"; + read_from := (fun s => s.(x24)); + write_to := (fun v s => ({[ s with x24 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x23_ref := {| + name := "x23"; + read_from := (fun s => s.(x23)); + write_to := (fun v s => ({[ s with x23 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x22_ref := {| + name := "x22"; + read_from := (fun s => s.(x22)); + write_to := (fun v s => ({[ s with x22 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x21_ref := {| + name := "x21"; + read_from := (fun s => s.(x21)); + write_to := (fun v s => ({[ s with x21 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x20_ref := {| + name := "x20"; + read_from := (fun s => s.(x20)); + write_to := (fun v s => ({[ s with x20 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x19_ref := {| + name := "x19"; + read_from := (fun s => s.(x19)); + write_to := (fun v s => ({[ s with x19 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x18_ref := {| + name := "x18"; + read_from := (fun s => s.(x18)); + write_to := (fun v s => ({[ s with x18 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x17_ref := {| + name := "x17"; + read_from := (fun s => s.(x17)); + write_to := (fun v s => ({[ s with x17 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x16_ref := {| + name := "x16"; + read_from := (fun s => s.(x16)); + write_to := (fun v s => ({[ s with x16 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x15_ref := {| + name := "x15"; + read_from := (fun s => s.(x15)); + write_to := (fun v s => ({[ s with x15 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x14_ref := {| + name := "x14"; + read_from := (fun s => s.(x14)); + write_to := (fun v s => ({[ s with x14 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x13_ref := {| + name := "x13"; + read_from := (fun s => s.(x13)); + write_to := (fun v s => ({[ s with x13 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x12_ref := {| + name := "x12"; + read_from := (fun s => s.(x12)); + write_to := (fun v s => ({[ s with x12 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x11_ref := {| + name := "x11"; + read_from := (fun s => s.(x11)); + write_to := (fun v s => ({[ s with x11 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x10_ref := {| + name := "x10"; + read_from := (fun s => s.(x10)); + write_to := (fun v s => ({[ s with x10 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x9_ref := {| + name := "x9"; + read_from := (fun s => s.(x9)); + write_to := (fun v s => ({[ s with x9 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x8_ref := {| + name := "x8"; + read_from := (fun s => s.(x8)); + write_to := (fun v s => ({[ s with x8 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x7_ref := {| + name := "x7"; + read_from := (fun s => s.(x7)); + write_to := (fun v s => ({[ s with x7 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x6_ref := {| + name := "x6"; + read_from := (fun s => s.(x6)); + write_to := (fun v s => ({[ s with x6 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x5_ref := {| + name := "x5"; + read_from := (fun s => s.(x5)); + write_to := (fun v s => ({[ s with x5 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x4_ref := {| + name := "x4"; + read_from := (fun s => s.(x4)); + write_to := (fun v s => ({[ s with x4 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x3_ref := {| + name := "x3"; + read_from := (fun s => s.(x3)); + write_to := (fun v s => ({[ s with x3 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x2_ref := {| + name := "x2"; + read_from := (fun s => s.(x2)); + write_to := (fun v s => ({[ s with x2 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition x1_ref := {| + name := "x1"; + read_from := (fun s => s.(x1)); + write_to := (fun v s => ({[ s with x1 := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition instbits_ref := {| + name := "instbits"; + read_from := (fun s => s.(instbits)); + write_to := (fun v s => ({[ s with instbits := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +(* These should get generated from anno.json... *) +Definition Xtype (X: Type) := + match X with + | x1_ref => true + | x2_ref => true + | x3_ref => true + | x4_ref => true + (* ... *) + end. +Inductive typing_result (A : Type) := +| Checked (a : A) +| TypeError (t : type_error). + +Check Xtype(x1_ref). +Check Xtype(x2_ref). +Check Xtype(x3_ref). +Check Xtype(x4_ref). + +Definition nextPC_ref := {| + name := "nextPC"; + read_from := (fun s => s.(nextPC)); + write_to := (fun v s => ({[ s with nextPC := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + +Definition PC_ref := {| + name := "PC"; + read_from := (fun s => s.(PC)); + write_to := (fun v s => ({[ s with PC := v ]})); + of_regval := (fun v => bitvector_64_dec_of_regval v); + regval_of := (fun v => regval_of_bitvector_64_dec v) |}. + + +Local Open Scope string. +Definition get_regval (reg_name : string) (s : regstate) : option register_value := + if string_dec reg_name "x31" then Some (x31_ref.(regval_of) (x31_ref.(read_from) s)) else + if string_dec reg_name "x30" then Some (x30_ref.(regval_of) (x30_ref.(read_from) s)) else + if string_dec reg_name "x29" then Some (x29_ref.(regval_of) (x29_ref.(read_from) s)) else + if string_dec reg_name "x28" then Some (x28_ref.(regval_of) (x28_ref.(read_from) s)) else + if string_dec reg_name "x27" then Some (x27_ref.(regval_of) (x27_ref.(read_from) s)) else + if string_dec reg_name "x26" then Some (x26_ref.(regval_of) (x26_ref.(read_from) s)) else + if string_dec reg_name "x25" then Some (x25_ref.(regval_of) (x25_ref.(read_from) s)) else + if string_dec reg_name "x24" then Some (x24_ref.(regval_of) (x24_ref.(read_from) s)) else + if string_dec reg_name "x23" then Some (x23_ref.(regval_of) (x23_ref.(read_from) s)) else + if string_dec reg_name "x22" then Some (x22_ref.(regval_of) (x22_ref.(read_from) s)) else + if string_dec reg_name "x21" then Some (x21_ref.(regval_of) (x21_ref.(read_from) s)) else + if string_dec reg_name "x20" then Some (x20_ref.(regval_of) (x20_ref.(read_from) s)) else + if string_dec reg_name "x19" then Some (x19_ref.(regval_of) (x19_ref.(read_from) s)) else + if string_dec reg_name "x18" then Some (x18_ref.(regval_of) (x18_ref.(read_from) s)) else + if string_dec reg_name "x17" then Some (x17_ref.(regval_of) (x17_ref.(read_from) s)) else + if string_dec reg_name "x16" then Some (x16_ref.(regval_of) (x16_ref.(read_from) s)) else + if string_dec reg_name "x15" then Some (x15_ref.(regval_of) (x15_ref.(read_from) s)) else + if string_dec reg_name "x14" then Some (x14_ref.(regval_of) (x14_ref.(read_from) s)) else + if string_dec reg_name "x13" then Some (x13_ref.(regval_of) (x13_ref.(read_from) s)) else + if string_dec reg_name "x12" then Some (x12_ref.(regval_of) (x12_ref.(read_from) s)) else + if string_dec reg_name "x11" then Some (x11_ref.(regval_of) (x11_ref.(read_from) s)) else + if string_dec reg_name "x10" then Some (x10_ref.(regval_of) (x10_ref.(read_from) s)) else + if string_dec reg_name "x9" then Some (x9_ref.(regval_of) (x9_ref.(read_from) s)) else + if string_dec reg_name "x8" then Some (x8_ref.(regval_of) (x8_ref.(read_from) s)) else + if string_dec reg_name "x7" then Some (x7_ref.(regval_of) (x7_ref.(read_from) s)) else + if string_dec reg_name "x6" then Some (x6_ref.(regval_of) (x6_ref.(read_from) s)) else + if string_dec reg_name "x5" then Some (x5_ref.(regval_of) (x5_ref.(read_from) s)) else + if string_dec reg_name "x4" then Some (x4_ref.(regval_of) (x4_ref.(read_from) s)) else + if string_dec reg_name "x3" then Some (x3_ref.(regval_of) (x3_ref.(read_from) s)) else + if string_dec reg_name "x2" then Some (x2_ref.(regval_of) (x2_ref.(read_from) s)) else + if string_dec reg_name "x1" then Some (x1_ref.(regval_of) (x1_ref.(read_from) s)) else + if string_dec reg_name "instbits" then Some (instbits_ref.(regval_of) (instbits_ref.(read_from) s)) else + if string_dec reg_name "nextPC" then Some (nextPC_ref.(regval_of) (nextPC_ref.(read_from) s)) else + if string_dec reg_name "PC" then Some (PC_ref.(regval_of) (PC_ref.(read_from) s)) else + None. + +Definition set_regval (reg_name : string) (v : register_value) (s : regstate) : option regstate := + if string_dec reg_name "x31" then option_map (fun v => x31_ref.(write_to) v s) (x31_ref.(of_regval) v) else + if string_dec reg_name "x30" then option_map (fun v => x30_ref.(write_to) v s) (x30_ref.(of_regval) v) else + if string_dec reg_name "x29" then option_map (fun v => x29_ref.(write_to) v s) (x29_ref.(of_regval) v) else + if string_dec reg_name "x28" then option_map (fun v => x28_ref.(write_to) v s) (x28_ref.(of_regval) v) else + if string_dec reg_name "x27" then option_map (fun v => x27_ref.(write_to) v s) (x27_ref.(of_regval) v) else + if string_dec reg_name "x26" then option_map (fun v => x26_ref.(write_to) v s) (x26_ref.(of_regval) v) else + if string_dec reg_name "x25" then option_map (fun v => x25_ref.(write_to) v s) (x25_ref.(of_regval) v) else + if string_dec reg_name "x24" then option_map (fun v => x24_ref.(write_to) v s) (x24_ref.(of_regval) v) else + if string_dec reg_name "x23" then option_map (fun v => x23_ref.(write_to) v s) (x23_ref.(of_regval) v) else + if string_dec reg_name "x22" then option_map (fun v => x22_ref.(write_to) v s) (x22_ref.(of_regval) v) else + if string_dec reg_name "x21" then option_map (fun v => x21_ref.(write_to) v s) (x21_ref.(of_regval) v) else + if string_dec reg_name "x20" then option_map (fun v => x20_ref.(write_to) v s) (x20_ref.(of_regval) v) else + if string_dec reg_name "x19" then option_map (fun v => x19_ref.(write_to) v s) (x19_ref.(of_regval) v) else + if string_dec reg_name "x18" then option_map (fun v => x18_ref.(write_to) v s) (x18_ref.(of_regval) v) else + if string_dec reg_name "x17" then option_map (fun v => x17_ref.(write_to) v s) (x17_ref.(of_regval) v) else + if string_dec reg_name "x16" then option_map (fun v => x16_ref.(write_to) v s) (x16_ref.(of_regval) v) else + if string_dec reg_name "x15" then option_map (fun v => x15_ref.(write_to) v s) (x15_ref.(of_regval) v) else + if string_dec reg_name "x14" then option_map (fun v => x14_ref.(write_to) v s) (x14_ref.(of_regval) v) else + if string_dec reg_name "x13" then option_map (fun v => x13_ref.(write_to) v s) (x13_ref.(of_regval) v) else + if string_dec reg_name "x12" then option_map (fun v => x12_ref.(write_to) v s) (x12_ref.(of_regval) v) else + if string_dec reg_name "x11" then option_map (fun v => x11_ref.(write_to) v s) (x11_ref.(of_regval) v) else + if string_dec reg_name "x10" then option_map (fun v => x10_ref.(write_to) v s) (x10_ref.(of_regval) v) else + if string_dec reg_name "x9" then option_map (fun v => x9_ref.(write_to) v s) (x9_ref.(of_regval) v) else + if string_dec reg_name "x8" then option_map (fun v => x8_ref.(write_to) v s) (x8_ref.(of_regval) v) else + if string_dec reg_name "x7" then option_map (fun v => x7_ref.(write_to) v s) (x7_ref.(of_regval) v) else + if string_dec reg_name "x6" then option_map (fun v => x6_ref.(write_to) v s) (x6_ref.(of_regval) v) else + if string_dec reg_name "x5" then option_map (fun v => x5_ref.(write_to) v s) (x5_ref.(of_regval) v) else + if string_dec reg_name "x4" then option_map (fun v => x4_ref.(write_to) v s) (x4_ref.(of_regval) v) else + if string_dec reg_name "x3" then option_map (fun v => x3_ref.(write_to) v s) (x3_ref.(of_regval) v) else + if string_dec reg_name "x2" then option_map (fun v => x2_ref.(write_to) v s) (x2_ref.(of_regval) v) else + if string_dec reg_name "x1" then option_map (fun v => x1_ref.(write_to) v s) (x1_ref.(of_regval) v) else + if string_dec reg_name "instbits" then option_map (fun v => instbits_ref.(write_to) v s) (instbits_ref.(of_regval) v) else + if string_dec reg_name "nextPC" then option_map (fun v => nextPC_ref.(write_to) v s) (nextPC_ref.(of_regval) v) else + if string_dec reg_name "PC" then option_map (fun v => PC_ref.(write_to) v s) (PC_ref.(of_regval) v) else + None. + +Definition register_accessors := (get_regval, set_regval). + + +Definition MR a r := monadR register_value a r unit. +Definition M a := monad register_value a unit. |