Update Coq memory interfaces

(requires recent changes to the Coq library)

1 files changed, 12 insertions, 12 deletions

diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index 8e483f8..b6fa0bc 100644
--- a/model/prelude_mem.sail
+++ b/model/prelude_mem.sail
@@ -2,22 +2,22 @@
  * They depend on the XLEN of the architecture.
  */
 
-val __WriteRAM = {lem: "MEMw", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM = {lem: "MEMw", coq: "MEMw", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __WriteRAM_release = {lem: "MEMw_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_release = {lem: "MEMw_release", coq: "MEMw_release", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __WriteRAM_strong_release = {lem: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_strong_release = {lem: "MEMw_strong_release", coq: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __WriteRAM_conditional = {lem: "MEMw_conditional", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_conditional = {lem: "MEMw_conditional", coq: "MEMw_conditional", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", coq: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm.
+val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", coq: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
 val __RISCV_write : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv}
@@ -36,22 +36,22 @@ function __RISCV_write (addr, width, data, aq, rl, con) =
 val __TraceMemoryWrite : forall 'n 'm.
   (atom('n), bits('m), bits(8 * 'n)) -> unit
 
-val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM = { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_acquire = { lem: "MEMr_acquire", coq: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", coq: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_reserved = { lem: "MEMr_reserved", coq: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", coq: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", coq: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
 val __RISCV_read : forall 'n, 'n >= 0. (xlenbits, atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}