diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_instr_kinds.v | 6 | ||||
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v index c93e9e93..eadc567a 100644 --- a/lib/coq/Sail2_instr_kinds.v +++ b/lib/coq/Sail2_instr_kinds.v @@ -144,7 +144,7 @@ Inductive barrier_kind := (* AArch64 barriers *) | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB - | Barrier_TM_COMMIT + (* | Barrier_TM_COMMIT*) (* MIPS barriers *) | Barrier_MIPS_SYNC (* RISC-V barriers *) @@ -204,11 +204,11 @@ Inductive instruction_kind := | IK_mem_read : read_kind -> instruction_kind | IK_mem_write : write_kind -> instruction_kind | IK_mem_rmw : (read_kind * write_kind) -> instruction_kind - | IK_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address), + | IK_branch : unit -> instruction_kind (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address), indirect/computed-branch (single nia of kind NIA_indirect_address) and branch/jump (single nia of kind NIA_concrete_address) *) | IK_trans : trans_kind -> instruction_kind - | IK_simple : instruction_kind. + | IK_simple : unit -> instruction_kind. (* instance (Show instruction_kind) diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 0f2c0955..12c1a9d9 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -128,3 +128,5 @@ Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad r Definition derive_m {rv e} {P Q:Z -> Prop} (x : monad rv {x : Z & P x} e) `{forall x, ArithFact (P x) -> ArithFact (Q x)} : monad rv {x : Z & (ArithFact (Q x))} e := x >>= fun y => returnm (build_ex (projT1 y)). +Definition memea {rv e} {T:Type} (_:T) (_:Z) : monad rv unit e := returnm tt. +Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt. |