From 0e42c867fba498746405d2b878a12fd4d143c5d8 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 7 Oct 2019 16:00:56 +0100 Subject: Add {read,write}_ram for Coq --- handwritten_support/mem_metadata.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 handwritten_support/mem_metadata.v (limited to 'handwritten_support/mem_metadata.v') diff --git a/handwritten_support/mem_metadata.v b/handwritten_support/mem_metadata.v new file mode 100644 index 0000000..ddb26e4 --- /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} wk (addr : mword 64) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk 64 addr size v. + +Definition read_ram {rv e} rk (addr : mword 64) size (read_tag : bool) `{ArithFact (size >= 0)} : monad rv (mword (8 * size) * unit) e := + read_mem rk 64 addr size >>= fun data => + returnm (data, tt). \ No newline at end of file -- cgit v1.1 From 4809371012e7394853f01b179d088497212cf480 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 26 Nov 2019 17:32:16 +0000 Subject: Fix RV32 Coq build --- handwritten_support/mem_metadata.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'handwritten_support/mem_metadata.v') diff --git a/handwritten_support/mem_metadata.v b/handwritten_support/mem_metadata.v index ddb26e4..0e53888 100644 --- a/handwritten_support/mem_metadata.v +++ b/handwritten_support/mem_metadata.v @@ -4,8 +4,8 @@ Require Import Sail2_operators_mwords. Require Import Sail2_prompt_monad. Require Import Sail2_prompt. -Definition write_ram {rv e} wk (addr : mword 64) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk 64 addr size v. +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} rk (addr : mword 64) size (read_tag : bool) `{ArithFact (size >= 0)} : monad rv (mword (8 * size) * unit) e := - read_mem rk 64 addr size >>= fun data => - returnm (data, tt). \ No newline at end of file +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). -- cgit v1.1