Coq: add more to library

3 files changed, 104 insertions, 9 deletions

diff --git a/lib/coq/Sail_operators.v b/lib/coq/Sail_operators.v
index 8183daea..f94276e9 100644
--- a/lib/coq/Sail_operators.v
+++ b/lib/coq/Sail_operators.v
@@ -242,4 +242,16 @@ Definition ugteq_bv := ucmp_bv (>=)
 Definition sgteq_bv := scmp_bv (>=)
 *)
 
+(*val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a*)
+Definition get_slice_int_bv {a} `{Bitvector a} len n lo : a :=
+  let hi := lo + len - 1 in
+  let bs := bools_of_int (hi + 1) n in
+  of_bools (subrange_list false bs hi lo).
+
+(*val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer
+Definition set_slice_int_bv {a} `{Bitvector a} len n lo (v : a) :=
+  let hi := lo + len - 1 in
+  let bs := bits_of_int (hi + 1) n in
+  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v))).*)
+
 End Bitvectors.
diff --git a/lib/coq/Sail_operators_mwords.v b/lib/coq/Sail_operators_mwords.v
index d32a7dbf..a701ddc1 100644
--- a/lib/coq/Sail_operators_mwords.v
+++ b/lib/coq/Sail_operators_mwords.v
@@ -199,10 +199,12 @@ val shiftl       : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val shiftr       : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val rotl         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-val rotr         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
-Definition shiftl       := shiftl_bv
-Definition shiftr       := shiftr_bv
-Definition arith_shiftr := arith_shiftr_bv
+val rotr         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
+(* TODO: check/redefine behaviour on out-of-range n *)
+Definition shiftl       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wlshift w (Z.to_nat n)) v.
+Definition shiftr       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshift w (Z.to_nat n)) v.
+Definition arith_shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshifta w (Z.to_nat n)) v.
+(*
 Definition rotl         := rotl_bv
 Definition rotr         := rotr_bv
 
@@ -246,3 +248,5 @@ Definition ugteq_vec := ugteq_bv.
 Definition sgteq_vec := sgteq_bv.
 
 *)
+
+Definition get_slice_int {a} `{ArithFact (a >= 0)} : Z -> Z -> Z -> mword a := get_slice_int_bv.
diff --git a/lib/coq/Sail_values.v b/lib/coq/Sail_values.v
index ee3a90bb..6c5a098b 100644
--- a/lib/coq/Sail_values.v
+++ b/lib/coq/Sail_values.v
@@ -26,12 +26,11 @@ Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFac
 Definition ii := Z.
 Definition nn := nat.
 
-(*
-val pow : Z -> Z -> Z
-Definition pow m n := m ** (Z.to_nat n)
-
-Definition pow2 n := pow 2 n
+(*val pow : Z -> Z -> Z*)
+Definition pow m n := m ^ n.
 
+Definition pow2 n := pow 2 n.
+(*
 Definition inline lt := (<)
 Definition inline gt := (>)
 Definition inline lteq := (<=)
@@ -229,6 +228,83 @@ val (+.) : bitU -> bitU -> bitU
 Definition inline (+.) x y := xor_bit x y
 *)
 
+(*** Bool lists ***)
+
+(*val bools_of_nat_aux : integer -> natural -> list bool -> list bool*)
+Fixpoint bools_of_nat_aux len (x : nat) (acc : list bool) : list bool :=
+  match len with
+  | O => acc
+  | S len' => bools_of_nat_aux len' (x / 2) ((if x mod 2 =? 1 then true else false) :: acc)
+  end %nat.
+  (*else (if x mod 2 = 1 then true else false) :: bools_of_nat_aux (x / 2)*)
+(*declare {isabelle} termination_argument bools_of_nat_aux = automatic*)
+Definition bools_of_nat len n := bools_of_nat_aux (Z.to_nat len) n [] (*List.reverse (bools_of_nat_aux n)*).
+
+(*val nat_of_bools_aux : natural -> list bool -> natural*)
+Fixpoint nat_of_bools_aux (acc : nat) (bs : list bool) : nat :=
+  match bs with
+  | [] => acc
+  | true :: bs => nat_of_bools_aux ((2 * acc) + 1) bs
+  | false :: bs => nat_of_bools_aux (2 * acc) bs
+end.
+(*declare {isabelle; hol} termination_argument nat_of_bools_aux = automatic*)
+Definition nat_of_bools bs := nat_of_bools_aux 0 bs.
+
+(*val unsigned_of_bools : list bool -> integer*)
+Definition unsigned_of_bools bs := Z.of_nat (nat_of_bools bs).
+
+(*val signed_of_bools : list bool -> integer*)
+Definition signed_of_bools bs :=
+  match bs with
+    | true :: _  => 0 - (1 + (unsigned_of_bools (List.map negb bs)))
+    | false :: _ => unsigned_of_bools bs
+    | [] => 0 (* Treat empty list as all zeros *)
+  end.
+
+(*val int_of_bools : bool -> list bool -> integer*)
+Definition int_of_bools (sign : bool) bs := if sign then signed_of_bools bs else unsigned_of_bools bs.
+
+(*val pad_list : forall 'a. 'a -> list 'a -> integer -> list 'a*)
+Fixpoint pad_list_nat {a} (x : a) (xs : list a) n :=
+  match n with
+  | O => xs
+  | S n' => pad_list_nat x (x :: xs) n'
+  end.
+(*declare {isabelle} termination_argument pad_list = automatic*)
+Definition pad_list {a} x xs n := @pad_list_nat a x xs (Z.to_nat n).
+
+Definition ext_list {a} pad len (xs : list a) :=
+  let longer := len - (Z.of_nat (List.length xs)) in
+  if longer <? 0 then skipn (Z.abs_nat (longer)) xs
+  else pad_list pad xs longer.
+
+(*let extz_bools len bs = ext_list false len bs*)
+Definition exts_bools len bs :=
+  match bs with
+    | true :: _ => ext_list true len bs
+    | _ => ext_list false len bs
+  end.
+
+Fixpoint add_one_bool_ignore_overflow_aux bits := match bits with
+  | [] => []
+  | false :: bits => true :: bits
+  | true :: bits => false :: add_one_bool_ignore_overflow_aux bits
+end.
+(*declare {isabelle; hol} termination_argument add_one_bool_ignore_overflow_aux = automatic*)
+
+Definition add_one_bool_ignore_overflow bits :=
+  List.rev (add_one_bool_ignore_overflow_aux (List.rev bits)).
+
+(*let bool_list_of_int n =
+  let bs_abs = false :: bools_of_nat (naturalFromInteger (abs n)) in
+  if n >= (0 : integer) then bs_abs
+  else add_one_bool_ignore_overflow (List.map not bs_abs)
+let bools_of_int len n = exts_bools len (bool_list_of_int n)*)
+Definition bools_of_int len n :=
+  let bs_abs := bools_of_nat len (Z.abs_nat n) in
+  if n >=? 0 then bs_abs
+  else add_one_bool_ignore_overflow (List.map negb bs_abs).
+
 (*** Bit lists ***)
 
 (*val bits_of_nat_aux : natural -> list bitU*)
@@ -663,6 +739,7 @@ Local Close Scope nat.
 Class Bitvector (a:Type) : Type := {
   bits_of : a -> list bitU;
   of_bits : list bitU -> a;
+  of_bools : list bool -> a;
   (* The first parameter specifies the desired length of the bitvector *)
   of_int : Z -> Z -> a;
   length : a -> Z;
@@ -685,6 +762,7 @@ end.
 Instance bitlist_Bitvector {a : Type} `{BitU a} : (Bitvector (list a)) := {
   bits_of v := List.map to_bitU v;
   of_bits v := List.map of_bitU v;
+  of_bools v := List.map of_bitU (List.map bitU_of_bool v);
   of_int len n := List.map of_bitU (bits_of_int len n);
   length := length_list;
   unsigned v := unsigned_of_bits (List.map to_bitU v);
@@ -767,6 +845,7 @@ Hint Extern 0 (ReasonableSize ?A) => (unwrap_ArithFacts; solve [apply Reasonable
 Instance mword_Bitvector {a : Z} `{ReasonableSize a} : (Bitvector (mword a)) := {
   bits_of v := List.map to_bitU (bitlistFromWord (get_word v));
   of_bits v := to_word isPositive (fit_bbv_word (wordFromBitlist (List.map of_bitU v)));
+  of_bools v := to_word isPositive (fit_bbv_word (wordFromBitlist v));
   of_int len z := @mword_of_int a isPositive z; (* cheat a little *)
   length v := a;
   unsigned v := Z.of_N (wordToN (get_word v));