Coq: fill in a few more RISC-V axioms

4 files changed, 52 insertions, 80 deletions

diff --git a/riscv/coq.patch b/riscv/coq.patch
index 54a8a662..9ee0fc71 100644
--- a/riscv/coq.patch
+++ b/riscv/coq.patch
@@ -1,6 +1,6 @@
---- riscv.v.plain	2018-09-05 16:42:05.798948328 +0100
-+++ riscv.v	2018-09-05 16:43:04.035671001 +0100
-@@ -8379,14 +8379,16 @@
+--- riscv.v.plain	2018-09-06 11:57:47.900156894 +0100
++++ riscv.v	2018-09-06 11:57:50.244172679 +0100
+@@ -8383,14 +8383,16 @@
     returnm ((EXTZ 56 (shiftl (_get_Satp64_PPN satp64) PAGESIZE_BITS))
      : mword 56).
  
@@ -20,7 +20,7 @@
               (projT1 (sub_range (build_ex SV39_LEVEL_BITS) (build_ex 1))) 0)) PTE39_LOG_SIZE in
     let pte_addr := add_vec ptb pt_ofs in
     phys_mem_read Data (EXTZ 64 pte_addr) 8 false false false >>= fun w__0 : MemoryOpResult (mword (8 * 8)) =>
-@@ -8399,27 +8401,27 @@
+@@ -8403,27 +8405,27 @@
         let is_global := orb global (eq_vec (_get_PTE_Bits_G pattr) ((bool_to_bits true)  : mword 1)) in
         (if ((isInvalidPTE pbits)) then returnm ((PTW_Failure (PTW_Invalid_PTE))  : PTW_Result )
          else if ((isPTEPtr pbits)) then
@@ -54,7 +54,7 @@
                        if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask)
                               (EXTZ 44 (vec_of_bits [B0]  : mword 1)))) then
                          PTW_Failure
-@@ -8429,12 +8431,12 @@
+@@ -8433,12 +8435,12 @@
                            or_vec (_get_SV39_PTE_PPNi pte)
                              (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in
                          PTW_Success
@@ -69,7 +69,7 @@
             : PTW_Result))
          : M (PTW_Result)
      end)
-@@ -8560,7 +8562,7 @@
+@@ -8564,7 +8566,7 @@
          : M (TR39_Result)
      | None =>
         curPTB39 tt >>= fun w__6 : mword 56 =>
@@ -78,7 +78,7 @@
         (match w__7 with
          | PTW_Failure (f) => returnm ((TR39_Failure (f))  : TR39_Result )
          | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) =>
-@@ -12335,138 +12337,144 @@
+@@ -12339,138 +12341,144 @@
     returnm (true
      : bool).
  
@@ -282,7 +282,7 @@
     | UTYPE (imm,rd,op) => (execute_UTYPE imm rd op)  : M (bool)
     | RISCV_JAL (imm,rd) => (execute_RISCV_JAL imm rd)  : M (bool)
     | RISCV_JALR (imm,rs1,rd) => (execute_RISCV_JALR imm rs1 rd)  : M (bool)
-@@ -12506,6 +12514,7 @@
+@@ -12510,6 +12518,7 @@
     | THREAD_START (arg0) => returnm ((execute_THREAD_START arg0)  : bool)
     | ILLEGAL (s) => (execute_ILLEGAL s)  : M (bool)
     | C_ILLEGAL (arg0) => (execute_C_ILLEGAL arg0)  : M (bool)
@@ -290,7 +290,7 @@
     end.
  
  Definition assembly_forwards (arg_ : ast) 
-@@ -12768,7 +12777,7 @@
+@@ -12772,7 +12781,7 @@
      | _ => exit tt  : M (string)
      end)
      : M (string).
@@ -299,7 +299,7 @@
  Definition assembly_backwards (arg_ : string) 
  : M (ast) :=
     let _stringappend_756_ := arg_ in
-@@ -27034,7 +27043,7 @@
+@@ -27038,7 +27047,7 @@
            : M (option ((ast * {n : Z & ArithFact (n >= 0)}))))
         : M (option ((ast * {n : Z & ArithFact (n >= 0)}))))
      : M (option ((ast * {n : Z & ArithFact (n >= 0)}))).
@@ -308,7 +308,7 @@
  Definition encdec_forwards (arg_ : ast) 
  : M (mword 32) :=
     (match arg_ with
-@@ -29122,7 +29131,7 @@
+@@ -29126,7 +29135,7 @@
          : M ((bool * bool))
      end)
      : M ((bool * bool)).
@@ -317,7 +317,7 @@
  Definition loop '(tt : unit) 
  : M (unit) :=
     let insns_per_tick := plat_insns_per_tick tt in
-@@ -29169,7 +29178,7 @@
+@@ -29173,7 +29182,7 @@
         returnm (i, step_no))) >>= fun '(i, step_no) =>
     returnm (tt
      : unit).
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 5d418aad..abdb3da0 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -257,7 +257,7 @@ val putchar = "putchar" : forall ('a : Type). 'a -> unit
 
 val concat_str = {c: "concat_str", ocaml: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string
 
-val string_of_int = {c: "string_of_int", ocaml: "string_of_int", lem: "stringFromInteger"} : int -> string
+val string_of_int = {c: "string_of_int", ocaml: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
 
 val DecStr : int -> string
 
diff --git a/riscv/riscv_extras.v b/riscv/riscv_extras.v
index 3f1fe7e0..820e3f3a 100644
--- a/riscv/riscv_extras.v
+++ b/riscv/riscv_extras.v
@@ -9,60 +9,32 @@ Import List.ListNotations.
 
 Axiom real : Type.
 
+Definition MEM_fence_rw_rw {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_rw_rw.
+Definition MEM_fence_r_rw  {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_r_rw.
+Definition MEM_fence_r_r   {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_r_r.
+Definition MEM_fence_rw_w  {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_rw_w.
+Definition MEM_fence_w_w   {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_w_w.
+Definition MEM_fence_w_rw  {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_w_rw.
+Definition MEM_fence_rw_r  {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_rw_r.
+Definition MEM_fence_r_w   {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_r_w.
+Definition MEM_fence_w_r   {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_w_r.
+Definition MEM_fence_i     {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_i.
 (*
-val MEMr             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e
-val MEMr_reserve     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e
-val MEMr_tag         : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e
-val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e
+val MEMea                            : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+val MEMea_release                    : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+val MEMea_strong_release             : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+val MEMea_conditional                : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+val MEMea_conditional_release        : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
 *)
-Definition MEMr {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size            : monad regval (mword b) e := read_mem Read_plain addr size.
-Definition MEMr_reserve {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size    : monad regval (mword b) e := read_mem Read_reserve addr size.
+Definition MEMea {rv a e} (addr : mword a) size                     : monad rv unit e := write_mem_ea Write_plain addr size.
+Definition MEMea_release {rv a e} (addr : mword a) size             : monad rv unit e := write_mem_ea Write_RISCV_release addr size.
+Definition MEMea_strong_release {rv a e} (addr : mword a) size      : monad rv unit e := write_mem_ea Write_RISCV_strong_release addr size.
+Definition MEMea_conditional {rv a e} (addr : mword a) size         : monad rv unit e := write_mem_ea Write_RISCV_conditional addr size.
+Definition MEMea_conditional_release {rv a e} (addr : mword a) size : monad rv unit e := write_mem_ea Write_RISCV_conditional_release addr size.
+Definition MEMea_conditional_strong_release {rv a e} (addr : mword a) size : monad rv unit e
+                                          := write_mem_ea Write_RISCV_conditional_strong_release addr size.
 
-(*val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e*)
-Definition read_tag_bool {regval a e} (addr : mword a) : monad regval bool e :=
-  read_tag addr >>= fun t =>
-  maybe_fail "read_tag_bool" (bool_of_bitU t).
-
-(*val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e*)
-Definition write_tag_bool {regval a e} (addr : mword a) t : monad regval unit e :=
- write_tag addr (bitU_of_bool t) >>= fun _ => returnm tt.
-
-Definition MEMr_tag {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (bool * mword b) e :=
-  read_mem Read_plain addr size >>= fun v =>
-  read_tag_bool addr >>= fun t =>
-  returnm (t, v).
-
-Definition MEMr_tag_reserve {regval a b e} `{ArithFact (b >= 0)} (addr : mword a) size : monad regval (bool * mword b) e :=
-  read_mem Read_plain addr size >>= fun v =>
-  read_tag_bool addr >>= fun t =>
-  returnm (t, v).
-
-(*
-val MEMea                 : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
-val MEMea_conditional     : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
-val MEMea_tag             : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
-val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e
-*)
-Definition MEMea {regval a e} (addr : mword a) size                : monad regval unit e := write_mem_ea Write_plain addr size.
-Definition MEMea_conditional {regval a e} (addr : mword a) size    : monad regval unit e := write_mem_ea Write_conditional addr size.
-
-Definition MEMea_tag {regval a e} (addr : mword a) size            : monad regval unit e := write_mem_ea Write_plain addr size.
-Definition MEMea_tag_conditional {regval a e} (addr : mword a) size : monad regval unit e := write_mem_ea Write_conditional addr size.
-
-(*
-val MEMval                 : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval unit 'e
-val MEMval_conditional     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval bool 'e
-val MEMval_tag             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e
-val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e
-*)
-Definition MEMval {regval a b e} (_ : mword a) (size : Z) (v : mword b)                      : monad regval unit e := write_mem_val v >>= fun _ => returnm tt.
-Definition MEMval_conditional {regval a b e} (_ : mword a) (size : Z) (v : mword b)          : monad regval bool e := write_mem_val v >>= fun b => returnm (if b then true else false).
-Definition MEMval_tag {regval a b e} (addr : mword a) (size : Z) t (v : mword b)             : monad regval unit e := write_mem_val v >>= fun _ => write_tag_bool addr t >>= fun _ => returnm tt.
-Definition MEMval_tag_conditional {regval a b e} (addr : mword a) (size : Z) t (v : mword b) : monad regval bool e := write_mem_val v >>= fun b => write_tag_bool addr t >>= fun _ => returnm (if b then true else false).
-
-(*val MEM_sync  : forall 'regval 'e. unit -> monad 'regval unit 'e*)
-
-Definition MEM_sync {regval e} (_:unit) : monad regval unit e := barrier Barrier_MIPS_SYNC.
 
 (* Some wrappers copied from aarch64_extras *)
 (* TODO: Harmonise into a common library *)
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 6c341341..2d59a891 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -58,17 +58,17 @@ function mem_read (addr, width, aq, rl, res) = {
   }
 }
 
-val MEMea = {lem: "MEMea", _: "memea"} : forall 'n.
+val MEMea = {lem: "MEMea", coq: "MEMea", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_release = {lem: "MEMea_release", _: "memea"} : forall 'n.
+val MEMea_release = {lem: "MEMea_release", coq: "MEMea_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_strong_release = {lem: "MEMea_strong_release", _: "memea"} : forall 'n.
+val MEMea_strong_release = {lem: "MEMea_strong_release", coq: "MEMea_strong_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional = {lem: "MEMea_conditional", _: "memea"} : forall 'n.
+val MEMea_conditional = {lem: "MEMea_conditional", coq: "MEMea_conditional", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional_release = {lem: "MEMea_conditional_release", _: "memea"} : forall 'n.
+val MEMea_conditional_release = {lem: "MEMea_conditional_release", coq: "MEMea_conditional_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
-val MEMea_conditional_strong_release = {lem: "MEMea_conditional_strong_release", _: "memea"} : forall 'n.
+val MEMea_conditional_strong_release = {lem: "MEMea_conditional_strong_release", coq: "MEMea_conditional_strong_release", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
 
 val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
@@ -136,13 +136,13 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
   }
 }
 
-val MEM_fence_rw_rw = {lem: "MEM_fence_rw_rw", _: "skip"} : unit -> unit effect {barr}
-val MEM_fence_r_rw  = {lem: "MEM_fence_r_rw", _: "skip"}  : unit -> unit effect {barr}
-val MEM_fence_r_r   = {lem: "MEM_fence_r_r", _: "skip"}   : unit -> unit effect {barr}
-val MEM_fence_rw_w  = {lem: "MEM_fence_rw_w", _: "skip"}  : unit -> unit effect {barr}
-val MEM_fence_w_w   = {lem: "MEM_fence_w_w", _: "skip"}   : unit -> unit effect {barr}
-val MEM_fence_w_rw  = {lem: "MEM_fence_w_rw", _: "skip"}  : unit -> unit effect {barr}
-val MEM_fence_rw_r  = {lem: "MEM_fence_rw_r", _: "skip"}  : unit -> unit effect {barr}
-val MEM_fence_r_w   = {lem: "MEM_fence_r_w", _: "skip"}   : unit -> unit effect {barr}
-val MEM_fence_w_r   = {lem: "MEM_fence_w_r", _: "skip"}   : unit -> unit effect {barr}
-val MEM_fence_i     = {lem: "MEM_fence_i", _: "skip"}     : unit -> unit effect {barr}
+val MEM_fence_rw_rw = {lem: "MEM_fence_rw_rw", coq: "MEM_fence_rw_rw", _: "skip"} : unit -> unit effect {barr}
+val MEM_fence_r_rw  = {lem: "MEM_fence_r_rw", coq: "MEM_fence_r_rw", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_r_r   = {lem: "MEM_fence_r_r", coq: "MEM_fence_r_r", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_rw_w  = {lem: "MEM_fence_rw_w", coq: "MEM_fence_rw_w", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_w_w   = {lem: "MEM_fence_w_w", coq: "MEM_fence_w_w", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_w_rw  = {lem: "MEM_fence_w_rw", coq: "MEM_fence_w_rw", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_rw_r  = {lem: "MEM_fence_rw_r", coq: "MEM_fence_rw_r", _: "skip"}  : unit -> unit effect {barr}
+val MEM_fence_r_w   = {lem: "MEM_fence_r_w", coq: "MEM_fence_r_w", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_w_r   = {lem: "MEM_fence_w_r", coq: "MEM_fence_w_r", _: "skip"}   : unit -> unit effect {barr}
+val MEM_fence_i     = {lem: "MEM_fence_i", coq: "MEM_fence_i", _: "skip"}     : unit -> unit effect {barr}