diff options
| -rw-r--r-- | lib/coq/Sail_operators_mwords.v | 77 | ||||
| -rw-r--r-- | lib/vector_dec.sail | 27 | ||||
| -rw-r--r-- | lib/vector_inc.sail | 25 |
3 files changed, 120 insertions, 9 deletions
diff --git a/lib/coq/Sail_operators_mwords.v b/lib/coq/Sail_operators_mwords.v index 326658d1..a962d554 100644 --- a/lib/coq/Sail_operators_mwords.v +++ b/lib/coq/Sail_operators_mwords.v @@ -11,6 +11,9 @@ rewrite <- eq. exact x. Defined. +Definition autocast {m n} (x : mword m) `{H:ArithFact (m = n)} : mword n := + cast_mword x (use_ArithFact H). + Definition cast_word {m n} (x : Word.word m) (eq : m = n) : Word.word n. rewrite <- eq. exact x. @@ -132,6 +135,75 @@ Definition cast_unit_vec := cast_unit_bv val vec_of_bit : forall 'a. Size 'a => integer -> bitU -> mword 'a Definition vec_of_bit := bv_of_bit*) +Require Import bbv.NatLib. + +Lemma Npow2_pow {n} : (2 ^ (N.of_nat n) = Npow2 n)%N. +induction n. +* reflexivity. +* rewrite Nnat.Nat2N.inj_succ. + rewrite N.pow_succ_r'. + rewrite IHn. + rewrite Npow2_S. + rewrite Word.Nmul_two. + reflexivity. +Qed. + +Program Definition uint {a} (x : mword a) : {z : Z & ArithFact (0 <= z /\ z <= 2 ^ a - 1)} := + existT _ (Z.of_N (Word.wordToN (get_word x))) _. +Next Obligation. +constructor. +constructor. +* apply N2Z.is_nonneg. +* assert (2 ^ a - 1 = Z.of_N (2 ^ (Z.to_N a) - 1)). { + rewrite N2Z.inj_sub. + * rewrite N2Z.inj_pow. + rewrite Z2N.id; auto. + destruct a; auto with zarith. destruct x. + * apply N.le_trans with (m := (2^0)%N); auto using N.le_refl. + apply N.pow_le_mono_r. + inversion 1. + apply N.le_0_l. + } + rewrite H. + apply N2Z.inj_le. + rewrite N.sub_1_r. + apply N.lt_le_pred. + rewrite <- Z_nat_N. + rewrite Npow2_pow. + apply Word.wordToN_bound. +Defined. + +Lemma Zpow_pow2 {n} : 2 ^ Z.of_nat n = Z.of_nat (pow2 n). +induction n. +* reflexivity. +* rewrite pow2_S_z. + rewrite Nat2Z.inj_succ. + rewrite Z.pow_succ_r; auto with zarith. +Qed. + +Program Definition sint {a} `{ArithFact (a > 0)} (x : mword a) : {z : Z & ArithFact (-(2^(a-1)) <= z /\ z <= 2 ^ (a-1) - 1)} := + existT _ (Word.wordToZ (get_word x)) _. +Next Obligation. +destruct H. +destruct a; try inversion fact. +constructor. +generalize (get_word x). +rewrite <- positive_nat_Z. +destruct (Pos2Nat.is_succ p) as [n eq]. +rewrite eq. +rewrite Nat2Z.id. +intro w. +destruct (Word.wordToZ_size' w) as [LO HI]. +replace 1 with (Z.of_nat 1); auto. +rewrite <- Nat2Z.inj_sub; auto with arith. +simpl. +rewrite <- minus_n_O. +rewrite Zpow_pow2. +rewrite Z.sub_1_r. +rewrite <- Z.lt_le_pred. +auto. +Defined. + Lemma length_list_pos : forall {A} {l:list A}, length_list l >= 0. unfold length_list. auto with zarith. @@ -258,12 +330,13 @@ match n with | S m => Word.combine w (replicate_bits_aux w m) end. Lemma replicate_ok {n a} `{ArithFact (n >= 0)} `{ArithFact (a >= 0)} : - Z.of_nat (Z.to_nat n * Z.to_nat a) = n * a. + Z.of_nat (Z.to_nat n * Z.to_nat a) = a * n. destruct H. destruct H0. rewrite <- Z2Nat.id; auto with zarith. rewrite Z2Nat.inj_mul; auto with zarith. +rewrite Nat.mul_comm. reflexivity. Qed. -Definition replicate_bits {a} (w : mword a) (n : Z) `{ArithFact (n >= 0)} : mword (n * a) := +Definition replicate_bits {a} (w : mword a) (n : Z) `{ArithFact (n >= 0)} : mword (a * n) := cast_to_mword (replicate_bits_aux (get_word w) (Z.to_nat n)) replicate_ok. (*val duplicate : forall 'a. Size 'a => bitU -> integer -> mword 'a diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index ad59f50e..075e8cb9 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -58,20 +58,38 @@ overload append = {bitvector_concat} /* Used for creating long bitvector literals in the C backend. */ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64) -val vector_access = { +val bitvector_access = { + ocaml: "access", + lem: "access_vec_dec", + coq: "access_vec_dec", + c: "vector_access" +} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit + +val plain_vector_access = { ocaml: "access", lem: "access_list_dec", coq: "access_list_dec", c: "vector_access" } : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a -val vector_update = { +overload vector_access = {bitvector_access, plain_vector_access} + +val bitvector_update = { + ocaml: "update", + lem: "update_vec_dec", + coq: "update_vec_dec", + c: "vector_update" +} : forall 'n, 'n >= 0. (bits('n), int, bit) -> bits('n) + +val plain_vector_update = { ocaml: "update", lem: "update_list_dec", coq: "update_list_dec", c: "vector_update" } : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) +overload vector_update = {bitvector_update, plain_vector_update} + val add_bits = { ocaml: "add_vec", lem: "add_vec", @@ -122,9 +140,10 @@ val unsigned = { lem: "uint", interpreter: "uint", c: "sail_uint", - coq: "unsigned" + coq: "uint" } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) -val signed = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) +/* We need a non-empty vector so that the range makes sense */ +val signed = "sint" : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) $endif diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail index b13e053c..5e73bafd 100644 --- a/lib/vector_inc.sail +++ b/lib/vector_inc.sail @@ -56,20 +56,38 @@ overload append = {bitvector_concat} /* Used for creating long bitvector literals in the C backend. */ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64) -val vector_access = { +val bitvector_access = { + ocaml: "access", + lem: "access_vec_inc", + coq: "access_vec_inc", + c: "vector_access" +} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit + +val plain_vector_access = { ocaml: "access", lem: "access_list_inc", coq: "access_list_inc", c: "vector_access" } : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, inc, 'a), atom('m)) -> 'a -val vector_update = { +overload vector_access = {bitvector_access, plain_vector_access} + +val bitvector_update = { + ocaml: "update", + lem: "update_vec_inc", + coq: "update_vec_inc", + c: "vector_update" +} : forall 'n, 'n >= 0. (bits('n), int, bit) -> bits('n) + +val plain_vector_update = { ocaml: "update", lem: "update_list_inc", coq: "update_list_inc", c: "vector_update" } : forall 'n ('a : Type). (vector('n, inc, 'a), int, 'a) -> vector('n, inc, 'a) +overload vector_update = {bitvector_update, plain_vector_update} + val add_bits = { ocaml: "add_vec", c: "add_bits" @@ -118,6 +136,7 @@ val unsigned = { coq: "uint" } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) -val signed = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) +/* We need a non-empty vector so that the range makes sense */ +val signed = "sint" : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) $endif |