diff options
Diffstat (limited to 'src/hls/Value.v')
| -rw-r--r-- | src/hls/Value.v | 552 |
1 files changed, 0 insertions, 552 deletions
diff --git a/src/hls/Value.v b/src/hls/Value.v deleted file mode 100644 index 0d3ea66..0000000 --- a/src/hls/Value.v +++ /dev/null @@ -1,552 +0,0 @@ -(*(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * - * This program is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see <https://www.gnu.org/licenses/>. - *) - -(* begin hide *) -From bbv Require Import Word. -From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. -From compcert Require Import lib.Integers common.Values. -From vericert Require Import Vericertlib. -(* end hide *) - -(** * Value - -A [value] is a bitvector with a specific size. We are using the implementation -of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse. -However, we need to wrap it with an [Inductive] so that we can specify and match -on the size of the [value]. This is necessary so that we can easily store -[value]s of different sizes in a list or in a map. - -Using the default [word], this would not be possible, as the size is part of the type. *) - -Record value : Type := - mkvalue { - vsize: nat; - vword: word vsize - }. - -(** ** Value conversions - -Various conversions to different number types such as [N], [Z], [positive] and -[int], where the last one is a theory of integers of powers of 2 in CompCert. *) - -Definition wordToValue : forall sz : nat, word sz -> value := mkvalue. - -Definition valueToWord : forall v : value, word (vsize v) := vword. - -Definition valueToNat (v :value) : nat := - wordToNat (vword v). - -Definition natToValue sz (n : nat) : value := - mkvalue sz (natToWord sz n). - -Definition valueToN (v : value) : N := - wordToN (vword v). - -Definition NToValue sz (n : N) : value := - mkvalue sz (NToWord sz n). - -Definition ZToValue (s : nat) (z : Z) : value := - mkvalue s (ZToWord s z). - -Definition valueToZ (v : value) : Z := - wordToZ (vword v). - -Definition uvalueToZ (v : value) : Z := - uwordToZ (vword v). - -Definition posToValue sz (p : positive) : value := - ZToValue sz (Zpos p). - -Definition posToValueAuto (p : positive) : value := - let size := Pos.to_nat (Pos.size p) in - ZToValue size (Zpos p). - -Definition valueToPos (v : value) : positive := - Z.to_pos (uvalueToZ v). - -Definition intToValue (i : Integers.int) : value := - ZToValue Int.wordsize (Int.unsigned i). - -Definition valueToInt (i : value) : Integers.int := - Int.repr (uvalueToZ i). - -Definition ptrToValue (i : Integers.ptrofs) : value := - ZToValue Ptrofs.wordsize (Ptrofs.unsigned i). - -Definition valueToPtr (i : value) : Integers.ptrofs := - Ptrofs.repr (uvalueToZ i). - -Definition valToValue (v : Values.val) : option value := - match v with - | Values.Vint i => Some (intToValue i) - | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z - then Some (ptrToValue off) - else None - | Values.Vundef => Some (ZToValue 32 0%Z) - | _ => None - end. - -(** Convert a [value] to a [bool], so that choices can be made based on the -result. This is also because comparison operators will give back [value] instead -of [bool], so if they are in a condition, they will have to be converted before -they can be used. *) - -Definition valueToBool (v : value) : bool := - negb (weqb (@wzero (vsize v)) (vword v)). - -Definition boolToValue (sz : nat) (b : bool) : value := - natToValue sz (if b then 1 else 0). - -(** ** Arithmetic operations *) - -Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. -intros; subst; assumption. Defined. - -Lemma unify_word_unfold : - forall sz w, - unify_word sz sz w eq_refl = w. -Proof. auto. Qed. - -Definition value_eq_size: - forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. -Proof. - intros; destruct (Nat.eqb (vsize v1) (vsize v2)) eqn:?. - left; apply Nat.eqb_eq in Heqb; assumption. - right; trivial. -Defined. - -Definition map_any {A : Type} (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) - (EQ : vsize v1 = vsize v2) : A := - let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in - f (vword v1) w2. - -Definition map_any_opt {A : Type} (sz : nat) (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) - : option A := - match value_eq_size v1 v2 with - | left EQ => - Some (map_any v1 v2 f EQ) - | _ => None - end. - -Definition map_word (f : forall sz : nat, word sz -> word sz) (v : value) : value := - mkvalue (vsize v) (f (vsize v) (vword v)). - -Definition map_word2 (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value) - (EQ : (vsize v1 = vsize v2)) : value := - let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in - mkvalue (vsize v1) (f (vsize v1) (vword v1) w2). - -Definition map_word2_opt (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value) - : option value := - match value_eq_size v1 v2 with - | left EQ => Some (map_word2 f v1 v2 EQ) - | _ => None - end. - -Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value) - : option value := - match value_eq_size v1 v2 with - | left EQ => Some (f EQ) - | _ => None - end. - -Lemma eqvalue {sz : nat} (x y : word sz) : x = y <-> mkvalue sz x = mkvalue sz y. -Proof. - split; intros. - subst. reflexivity. inversion H. apply existT_wordToZ in H1. - apply wordToZ_inj. assumption. -Qed. - -Lemma eqvaluef {sz : nat} (x y : word sz) : x = y -> mkvalue sz x = mkvalue sz y. -Proof. apply eqvalue. Qed. - -Lemma nevalue {sz : nat} (x y : word sz) : x <> y <-> mkvalue sz x <> mkvalue sz y. -Proof. split; intros; intuition. apply H. apply eqvalue. assumption. - apply H. rewrite H0. trivial. -Qed. - -Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y. -Proof. apply nevalue. Qed. - -(*Definition rewrite_word_size (initsz finalsz : nat) (w : word initsz) - : option (word finalsz) := - match Nat.eqb initsz finalsz return option (word finalsz) with - | true => Some _ - | false => None - end.*) - -Definition valueeq (sz : nat) (x y : word sz) : - {mkvalue sz x = mkvalue sz y} + {mkvalue sz x <> mkvalue sz y} := - match weq x y with - | left eq => left (eqvaluef x y eq) - | right ne => right (nevaluef x y ne) - end. - -Definition valueeqb (x y : value) : bool := - match value_eq_size x y with - | left EQ => - weqb (vword x) (unify_word (vsize x) (vsize y) (vword y) EQ) - | right _ => false - end. - -Definition value_projZ_eqb (v1 v2 : value) : bool := Z.eqb (valueToZ v1) (valueToZ v2). - -Theorem value_projZ_eqb_true : - forall v1 v2, - v1 = v2 -> value_projZ_eqb v1 v2 = true. -Proof. intros. subst. unfold value_projZ_eqb. apply Z.eqb_eq. trivial. Qed. - -Theorem valueeqb_true_iff : - forall v1 v2, - valueeqb v1 v2 = true <-> v1 = v2. -Proof. - split; intros. - unfold valueeqb in H. destruct (value_eq_size v1 v2) eqn:?. - - destruct v1, v2. simpl in H. -Abort. - -Definition value_int_eqb (v : value) (i : int) : bool := - Z.eqb (valueToZ v) (Int.unsigned i). - -(** Arithmetic operations over [value], interpreting them as signed or unsigned -depending on the operation. - -The arithmetic operations over [word] are over [N] by default, however, can also -be called over [Z] explicitly, which is where the bits are interpreted in a -signed manner. *) - -Definition vplus v1 v2 := map_word2 wplus v1 v2. -Definition vplus_opt v1 v2 := map_word2_opt wplus v1 v2. -Definition vminus v1 v2 := map_word2 wminus v1 v2. -Definition vmul v1 v2 := map_word2 wmult v1 v2. -Definition vdiv v1 v2 := map_word2 wdiv v1 v2. -Definition vmod v1 v2 := map_word2 wmod v1 v2. - -Definition vmuls v1 v2 := map_word2 wmultZ v1 v2. -Definition vdivs v1 v2 := map_word2 wdivZ v1 v2. -Definition vmods v1 v2 := map_word2 wremZ v1 v2. - -(** ** Bitwise operations - -Bitwise operations over [value], which is independent of whether the number is -signed or unsigned. *) - -Definition vnot v := map_word wnot v. -Definition vneg v := map_word wneg v. -Definition vbitneg v := boolToValue (vsize v) (negb (valueToBool v)). -Definition vor v1 v2 := map_word2 wor v1 v2. -Definition vand v1 v2 := map_word2 wand v1 v2. -Definition vxor v1 v2 := map_word2 wxor v1 v2. - -(** ** Comparison operators - -Comparison operators that return a bool, there should probably be an equivalent -which returns another number, however I might just add that as an explicit -conversion. *) - -Definition veqb v1 v2 := map_any v1 v2 (@weqb (vsize v1)). -Definition vneb v1 v2 EQ := negb (veqb v1 v2 EQ). - -Definition veq v1 v2 EQ := boolToValue (vsize v1) (veqb v1 v2 EQ). -Definition vne v1 v2 EQ := boolToValue (vsize v1) (vneb v1 v2 EQ). - -Definition vltb v1 v2 := map_any v1 v2 wltb. -Definition vleb v1 v2 EQ := negb (map_any v2 v1 wltb (eq_sym EQ)). -Definition vgtb v1 v2 EQ := map_any v2 v1 wltb (eq_sym EQ). -Definition vgeb v1 v2 EQ := negb (map_any v1 v2 wltb EQ). - -Definition vltsb v1 v2 := map_any v1 v2 wsltb. -Definition vlesb v1 v2 EQ := negb (map_any v2 v1 wsltb (eq_sym EQ)). -Definition vgtsb v1 v2 EQ := map_any v2 v1 wsltb (eq_sym EQ). -Definition vgesb v1 v2 EQ := negb (map_any v1 v2 wsltb EQ). - -Definition vlt v1 v2 EQ := boolToValue (vsize v1) (vltb v1 v2 EQ). -Definition vle v1 v2 EQ := boolToValue (vsize v1) (vleb v1 v2 EQ). -Definition vgt v1 v2 EQ := boolToValue (vsize v1) (vgtb v1 v2 EQ). -Definition vge v1 v2 EQ := boolToValue (vsize v1) (vgeb v1 v2 EQ). - -Definition vlts v1 v2 EQ := boolToValue (vsize v1) (vltsb v1 v2 EQ). -Definition vles v1 v2 EQ := boolToValue (vsize v1) (vlesb v1 v2 EQ). -Definition vgts v1 v2 EQ := boolToValue (vsize v1) (vgtsb v1 v2 EQ). -Definition vges v1 v2 EQ := boolToValue (vsize v1) (vgesb v1 v2 EQ). - -(** ** Shift operators - -Shift operators on values. *) - -Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz) := - f w1 (wordToNat w2). - -Definition vshl v1 v2 := map_word2 (fun sz => shift_map sz (@wlshift sz)) v1 v2. -Definition vshr v1 v2 := map_word2 (fun sz => shift_map sz (@wrshift sz)) v1 v2. - -Module HexNotationValue. - Export HexNotation. - Import WordScope. - - Notation "sz ''h' a" := (NToValue sz (hex a)) (at level 50). - -End HexNotationValue. - -Inductive val_value_lessdef: val -> value -> Prop := -| val_value_lessdef_int: - forall i v', - i = valueToInt v' -> - val_value_lessdef (Vint i) v' -| val_value_lessdef_ptr: - forall b off v', - off = valueToPtr v' -> - (Z.modulo (uvalueToZ v') 4) = 0%Z -> - val_value_lessdef (Vptr b off) v' -| lessdef_undef: forall v, val_value_lessdef Vundef v. - -Inductive opt_val_value_lessdef: option val -> value -> Prop := -| opt_lessdef_some: - forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' -| opt_lessdef_none: forall v, opt_val_value_lessdef None v. - -Lemma valueToZ_ZToValue : - forall n z, - (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> - valueToZ (ZToValue (S n) z) = z. -Proof. - unfold valueToZ, ZToValue. simpl. - auto using wordToZ_ZToWord. -Qed. - -Lemma uvalueToZ_ZToValue : - forall n z, - (0 <= z < 2 ^ Z.of_nat n)%Z -> - uvalueToZ (ZToValue n z) = z. -Proof. - unfold uvalueToZ, ZToValue. simpl. - auto using uwordToZ_ZToWord. -Qed. - -Lemma uvalueToZ_ZToValue_full : - forall sz : nat, - (0 < sz)%nat -> - forall z : Z, uvalueToZ (ZToValue sz z) = (z mod 2 ^ Z.of_nat sz)%Z. -Proof. unfold uvalueToZ, ZToValue. simpl. auto using uwordToZ_ZToWord_full. Qed. - -Lemma ZToValue_uvalueToZ : - forall v, - ZToValue (vsize v) (uvalueToZ v) = v. -Proof. - intros. - unfold ZToValue, uvalueToZ. - rewrite ZToWord_uwordToZ. destruct v; auto. -Qed. - -Lemma valueToPos_posToValueAuto : - forall p, valueToPos (posToValueAuto p) = p. -Proof. - intros. unfold valueToPos, posToValueAuto. - rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. - split. apply Zle_0_pos. - - assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt. - inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. - simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. -Qed. - -Lemma valueToPos_posToValue : - forall p, valueToPos (posToValueAuto p) = p. -Proof. - intros. unfold valueToPos, posToValueAuto. - rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. - split. apply Zle_0_pos. - - assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt. - inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. - simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. -Qed. - -Lemma valueToInt_intToValue : - forall v, - valueToInt (intToValue v) = v. -Proof. - intros. - unfold valueToInt, intToValue. rewrite uvalueToZ_ZToValue. auto using Int.repr_unsigned. - split. apply Int.unsigned_range_2. - assert ((Int.unsigned v <= Int.max_unsigned)%Z) by apply Int.unsigned_range_2. - apply Z.lt_le_pred in H. apply H. -Qed. - -Lemma valueToPtr_ptrToValue : - forall v, - valueToPtr (ptrToValue v) = v. -Proof. - intros. - unfold valueToPtr, ptrToValue. rewrite uvalueToZ_ZToValue. auto using Ptrofs.repr_unsigned. - split. apply Ptrofs.unsigned_range_2. - assert ((Ptrofs.unsigned v <= Ptrofs.max_unsigned)%Z) by apply Ptrofs.unsigned_range_2. - apply Z.lt_le_pred in H. apply H. -Qed. - -Lemma intToValue_valueToInt : - forall v, - vsize v = 32%nat -> - intToValue (valueToInt v) = v. -Proof. - intros. unfold valueToInt, intToValue. rewrite Int.unsigned_repr_eq. - unfold ZToValue, uvalueToZ. unfold Int.modulus. unfold Int.wordsize. unfold Wordsize_32.wordsize. - pose proof (uwordToZ_bound (vword v)). - rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. - rewrite <- H. rewrite two_power_nat_equiv. apply H0. -Qed. - -Lemma ptrToValue_valueToPtr : - forall v, - vsize v = 32%nat -> - ptrToValue (valueToPtr v) = v. -Proof. - intros. unfold valueToPtr, ptrToValue. rewrite Ptrofs.unsigned_repr_eq. - unfold ZToValue, uvalueToZ. unfold Ptrofs.modulus. unfold Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize. - pose proof (uwordToZ_bound (vword v)). - rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. - rewrite <- H. rewrite two_power_nat_equiv. apply H0. -Qed. - -Lemma valToValue_lessdef : - forall v v', - valToValue v = Some v' -> - val_value_lessdef v v'. -Proof. - intros. - destruct v; try discriminate; constructor. - unfold valToValue in H. inversion H. - symmetry. apply valueToInt_intToValue. - inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate. - inv H1. symmetry. apply valueToPtr_ptrToValue. - inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. - inv H1. apply Z.eqb_eq. apply Heqb0. -Qed. - -Lemma boolToValue_ValueToBool : - forall b, - valueToBool (boolToValue 32 b) = b. -Proof. destruct b; auto. Qed. - -Local Open Scope Z. - -Ltac word_op_value H := - intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold; - rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega. - -Lemma zadd_vplus : - forall sz z1 z2, - (sz > 0)%nat -> - uvalueToZ (vplus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 + z2) mod 2 ^ Z.of_nat sz. -Proof. word_op_value ZToWord_plus. Qed. - -Lemma zadd_vplus2 : - forall z1 z2, - vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2). -Proof. - intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl. - rewrite ZToWord_plus; auto. -Qed. - -Lemma ZToValue_eq : - forall w1, - (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Abort. - -Lemma wordsize_32 : - Int.wordsize = 32%nat. -Proof. auto. Qed. - -Lemma intadd_vplus : - forall i1 i2, - valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2. -Proof. - intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus. - rewrite <- Int.unsigned_repr_eq. - rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. -Qed. - -(*Lemma intadd_vplus2 : - forall v1 v2 EQ, - vsize v1 = 32%nat -> - Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ). -Proof. - intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr). - rewrite (@vadd_vplus v1 v2 EQ). trivial. - unfold uvalueToZ. pose proof (@uwordToZ_bound (vsize v2) (vword v2)). - rewrite H in EQ. rewrite <- EQ in H0 at 3.*) - (*rewrite zadd_vplus3. trivia*) - -Lemma valadd_vplus : - forall v1 v2 v1' v2' v v' EQ, - val_value_lessdef v1 v1' -> - val_value_lessdef v2 v2' -> - Val.add v1 v2 = v -> - vplus v1' v2' EQ = v' -> - val_value_lessdef v v'. -Proof. - intros. inv H; inv H0; constructor; simplify. - Abort. - -Lemma zsub_vminus : - forall sz z1 z2, - (sz > 0)%nat -> - uvalueToZ (vminus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 - z2) mod 2 ^ Z.of_nat sz. -Proof. word_op_value ZToWord_minus. Qed. - -Lemma zmul_vmul : - forall sz z1 z2, - (sz > 0)%nat -> - uvalueToZ (vmul (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 * z2) mod 2 ^ Z.of_nat sz. -Proof. word_op_value ZToWord_mult. Qed. - -Local Open Scope N. -Lemma zdiv_vdiv : - forall n1 n2, - n1 < 2 ^ 32 -> - n2 < 2 ^ 32 -> - n1 / n2 < 2 ^ 32 -> - valueToN (vdiv (NToValue 32 n1) (NToValue 32 n2) eq_refl) = n1 / n2. -Proof. - intros; unfold valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv. - unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto. -Qed. - -Lemma ZToValue_valueToNat : - forall x sz, - (sz > 0)%nat -> - (0 <= x < 2^(Z.of_nat sz))%Z -> - valueToNat (ZToValue sz x) = Z.to_nat x. -Proof. - destruct x; intros; unfold ZToValue, valueToNat; crush. - - rewrite wzero'_def. apply wordToNat_wzero. - - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial. - clear H1. - lazymatch goal with - | [ H : context[(_ < ?x)%Z] |- _ ] => replace x with (Z.of_nat (Z.to_nat x)) in H - end. - 2: { apply Z2Nat.id; apply Z.pow_nonneg; lia. } - - rewrite Z2Nat.inj_pow in H2; crush. - replace (Pos.to_nat 2) with 2%nat in H2 by reflexivity. - rewrite Nat2Z.id in H2. - rewrite <- positive_nat_Z in H2. - apply Nat2Z.inj_lt in H2. - assumption. -Qed. -*) |