Merge branch 'master' into rsnikhil.

3 files changed, 43 insertions, 0 deletions

diff --git a/handwritten_support/0.11/mem_metadata.lem b/handwritten_support/0.11/mem_metadata.lem
new file mode 100644
index 0000000..8a8c070
--- /dev/null
+++ b/handwritten_support/0.11/mem_metadata.lem
@@ -0,0 +1,16 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators_mwords
+open import Sail2_prompt_monad
+open import Sail2_prompt
+
+val write_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => write_kind -> mword 'a -> integer -> mword 'n -> unit -> monad 'rv bool 'e
+let write_ram wk addr width data meta =
+  write_mem wk () addr width data
+
+val read_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => read_kind -> mword 'a -> integer -> bool -> monad 'rv (mword 'n * unit) 'e
+let read_ram rk addr width read_tag =
+  read_mem rk () addr width >>= (fun (data : mword 'n) ->
+  return (data, ()))
diff --git a/handwritten_support/mem_metadata.lem b/handwritten_support/mem_metadata.lem
new file mode 100644
index 0000000..8a8c070
--- /dev/null
+++ b/handwritten_support/mem_metadata.lem
@@ -0,0 +1,16 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators_mwords
+open import Sail2_prompt_monad
+open import Sail2_prompt
+
+val write_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => write_kind -> mword 'a -> integer -> mword 'n -> unit -> monad 'rv bool 'e
+let write_ram wk addr width data meta =
+  write_mem wk () addr width data
+
+val read_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => read_kind -> mword 'a -> integer -> bool -> monad 'rv (mword 'n * unit) 'e
+let read_ram rk addr width read_tag =
+  read_mem rk () addr width >>= (fun (data : mword 'n) ->
+  return (data, ()))
diff --git a/handwritten_support/mem_metadata.v b/handwritten_support/mem_metadata.v
new file mode 100644
index 0000000..0e53888
--- /dev/null
+++ b/handwritten_support/mem_metadata.v
@@ -0,0 +1,11 @@
+Require Import Sail2_instr_kinds.
+Require Import Sail2_values.
+Require Import Sail2_operators_mwords.
+Require Import Sail2_prompt_monad.
+Require Import Sail2_prompt.
+
+Definition write_ram {rv e a} wk (addr : mword a) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk a addr size v.
+
+Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >= 0)} : monad rv (mword (8 * size) * unit) e :=
+  read_mem rk a addr size >>= fun data =>
+  returnm (data, tt).