Coq: library updates, esp extending bitvector multiplies, Undefined

5 files changed, 15 insertions, 4 deletions

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 224ab18d..ebcc0925 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -245,8 +245,10 @@ val smult_vec : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'a -> mword
 Definition add_vec   {n} : mword n -> mword n -> mword n := word_binop Word.wplus.
 (*Definition sadd_vec  {n} : mword n -> mword n -> mword n := sadd_bv w.*)
 Definition sub_vec   {n} : mword n -> mword n -> mword n := word_binop Word.wminus.
-Definition mult_vec  {n} : mword n -> mword n -> mword n := word_binop Word.wmult.
-(*Definition smult_vec {n} : mword n -> mword n -> mword n := smult_bv w.*)
+Definition mult_vec  {n m} `{ArithFact (m >= n)} (l : mword n) (r : mword n) : mword m :=
+  word_binop Word.wmult (zero_extend l _) (zero_extend r _).
+Definition mults_vec  {n m} `{ArithFact (m >= n)} (l : mword n) (r : mword n) : mword m :=
+  word_binop Word.wmult (sign_extend l _) (sign_extend r _).
 
 (*val add_vec_int   : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val sadd_vec_int  : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 802fc302..336ca8de 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -48,7 +48,7 @@ match b with
   | BU => Fail "bool_of_bitU"
 end.
 
-(*val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e
+(*val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e*)
 Definition bool_of_bitU_oracle {rv E} (b : bitU) : monad rv bool E :=
 match b with
   | B0 => returnm false
@@ -57,7 +57,7 @@ match b with
 end.
 
 
-val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+(*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec whileM vars cond body =
   cond vars >>= fun cond_val ->
diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v
index 5bb9d477..2715b5e7 100644
--- a/lib/coq/Sail2_prompt_monad.v
+++ b/lib/coq/Sail2_prompt_monad.v
@@ -31,6 +31,7 @@ Inductive monad regval a e :=
   | Read_reg : register_name -> (regval -> monad regval a e) -> monad regval a e
   (* Request to write register *)
   | Write_reg : register_name -> regval -> monad regval a e -> monad regval a e
+  | Undefined : (bool -> monad regval a e) -> monad regval a e
   (*Result : a failed assert with possible error message to report*)
   | Fail : string -> monad regval a e
   | Error : string -> monad regval a e
@@ -49,6 +50,7 @@ Arguments Footprint [_ _ _].
 Arguments Barrier [_ _ _].
 Arguments Read_reg [_ _ _].
 Arguments Write_reg [_ _ _].
+Arguments Undefined [_ _ _].
 Arguments Fail [_ _ _].
 Arguments Error [_ _ _].
 Arguments Exception [_ _ _].
@@ -65,6 +67,7 @@ Fixpoint bind {rv A B E} (m : monad rv A E) (f : A -> monad rv B E) := match m w
   | Write_tag a t k =>    Write_tag a t    (fun v => bind (k v) f)
   | Read_reg descr k =>   Read_reg descr   (fun v => bind (k v) f)
   | Excl_res k =>         Excl_res         (fun v => bind (k v) f)
+  | Undefined k =>        Undefined        (fun v => bind (k v) f)
   | Write_ea wk a sz k => Write_ea wk a sz (bind k f)
   | Footprint k =>        Footprint        (bind k f)
   | Barrier bk k =>       Barrier bk       (bind k f)
@@ -83,6 +86,9 @@ Notation "m >> n" := (bind0 m n) (at level 50, left associativity).
 (*val exit : forall rv a e. unit -> monad rv a e*)
 Definition exit {rv A E} (_ : unit) : monad rv A E := Fail "exit".
 
+(*val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e*)
+Definition undefined_bool {rv e} (_:unit) : monad rv bool e := Undefined returnm.
+
 (*val assert_exp : forall rv e. bool -> string -> monad rv unit e*)
 Definition assert_exp {rv E} (exp :bool) msg : monad rv unit E :=
  if exp then Done tt else Fail msg.
@@ -105,6 +111,7 @@ Fixpoint try_catch {rv A E1 E2} (m : monad rv A E1) (h : E1 -> monad rv A E2) :=
   | Write_tag a t k =>    Write_tag a t     (fun v => try_catch (k v) h)
   | Read_reg descr k =>   Read_reg descr   (fun v => try_catch (k v) h)
   | Excl_res k =>         Excl_res         (fun v => try_catch (k v) h)
+  | Undefined k =>        Undefined        (fun v => try_catch (k v) h)
   | Write_ea wk a sz k => Write_ea wk a sz (try_catch k h)
   | Footprint k =>        Footprint        (try_catch k h)
   | Barrier bk k =>       Barrier bk       (try_catch k h)
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v
index 7e10aba3..1d5cb342 100644
--- a/lib/coq/Sail2_state.v
+++ b/lib/coq/Sail2_state.v
@@ -15,6 +15,7 @@ let rec liftState ra s = match s with
   | (Write_tagv t k)     -> bindS (write_tagS t)            (fun v -> liftState ra (k v))
   | (Read_reg r k)       -> bindS (read_regvalS ra r)       (fun v -> liftState ra (k v))
   | (Excl_res k)         -> bindS (excl_resultS ())         (fun v -> liftState ra (k v))
+  | (Undefined k)        -> bindS (undefined_boolS ())      (fun v -> liftState ra (k v))
   | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)    (liftState ra k)
   | (Write_reg r v k)    -> seqS (write_regvalS ra r v)     (liftState ra k)
   | (Footprint k)        -> liftState ra k
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 7c70f88b..55d85b3a 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1032,6 +1032,7 @@ Arguments write_to [_ _ _].
 Arguments of_regval [_ _ _].
 Arguments regval_of [_ _ _].
 
+(* Register accessors: pair of functions for reading and writing register values *)
 Definition register_accessors regstate regval : Type :=
   ((string -> regstate -> option regval) *
    (string -> regval -> regstate -> option regstate)).