diff options
| -rw-r--r-- | handwritten_support/mem_metadata.v | 8 | ||||
| -rw-r--r-- | model/riscv_termination_rv32.sail | 2 |
2 files changed, 5 insertions, 5 deletions
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). diff --git a/model/riscv_termination_rv32.sail b/model/riscv_termination_rv32.sail index 7cf8cb8..7318421 100644 --- a/model/riscv_termination_rv32.sail +++ b/model/riscv_termination_rv32.sail @@ -1 +1 @@ -termination_measure walk32(_,_,_,_,_,_,level,_) = level +termination_measure walk32(_,_,_,_,_,_,level,_,_) = level |