From 4225439aa82294a6d2a56fc4f622dc318e69529f Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Fri, 21 Oct 2016 11:04:03 -0700 Subject: committing unstable refactors to patch master --- src/Assembly/Bounded.v | 732 ------------------------------------------- src/Assembly/Compile.v | 79 +++-- src/Assembly/Conversions.v | 758 +++++++++++++++++++++++---------------------- src/Assembly/Evaluables.v | 206 ++++++++---- src/Assembly/GF25519.v | 173 +++-------- src/Assembly/HL.v | 26 +- src/Assembly/LL.v | 45 ++- src/Assembly/Pipeline.v | 63 ++-- src/Assembly/QhasmUtil.v | 6 + 9 files changed, 730 insertions(+), 1358 deletions(-) delete mode 100644 src/Assembly/Bounded.v (limited to 'src/Assembly') diff --git a/src/Assembly/Bounded.v b/src/Assembly/Bounded.v deleted file mode 100644 index 964f6f810..000000000 --- a/src/Assembly/Bounded.v +++ /dev/null @@ -1,732 +0,0 @@ -Require Import Bedrock.Word Bedrock.Nomega. -Require Import NPeano NArith PArith Ndigits ZArith Znat ZArith_dec Ndec. -Require Import List Basics Bool Nsatz. - -Require Import Crypto.Assembly.QhasmUtil. -Require Import Crypto.Assembly.WordizeUtil. -Require Import Crypto.Assembly.Bounds. - -Import ListNotations. - -Section BoundedZ. - - Section Trans4. - Definition min4 (a b c d: Z) := - Z.min 0 (Z.min (Z.min a b) (Z.min c d)). - - Definition max4 (a b c d: Z) := - Z.max 0 (Z.max (Z.max a b) (Z.max c d)). - - Ltac trans4min_tac := intros; unfold min4; - repeat match goal with - | [|- context[(Z.min ?x0 ?x1)%Z]] => is_var x1; - let A := fresh in let B := fresh in - destruct (Zmin_spec x0 x1)%Z as [A|A]; - destruct A as [A B]; - rewrite B; clear B - end; nomega. - - Lemma trans4min_0: forall (x a b c d: Z), - (0 <= x)%Z -> (min4 a b c d <= x)%Z. - Proof. trans4min_tac. Qed. - - Lemma trans4min_a: forall (x a b c d: Z), - (a <= x)%Z -> (min4 a b c d <= x)%Z. - Proof. trans4min_tac. Qed. - - Lemma trans4min_b: forall (x a b c d: Z), - (b <= x)%Z -> (min4 a b c d <= x)%Z. - Proof. trans4min_tac. Qed. - - Lemma trans4min_c: forall (x a b c d: Z), - (c <= x)%Z -> (min4 a b c d <= x)%Z. - Proof. trans4min_tac. Qed. - - Lemma trans4min_d: forall (x a b c d: Z), - (d <= x)%Z -> (min4 a b c d <= x)%Z. - Proof. trans4min_tac. Qed. - - Ltac trans4max_tac := intros; unfold max4; - repeat match goal with - | [|- context[(Z.max ?x0 ?x1)%Z]] => is_var x1; - let A := fresh in let B := fresh in - destruct (Zmax_spec x0 x1)%Z as [A|A]; - destruct A as [A B]; - rewrite B; clear B - end; try nomega. - - Lemma trans4max_0: forall (x a b c d: Z), - (x <= 0)%Z -> (x <= max4 a b c d)%Z. - Proof. trans4max_tac. Qed. - - Lemma trans4max_a: forall (x a b c d: Z), - (x <= a)%Z -> (x <= max4 a b c d)%Z. - Proof. trans4max_tac. Qed. - - Lemma trans4max_b: forall (x a b c d: Z), - (x <= b)%Z -> (x <= max4 a b c d)%Z. - Proof. trans4max_tac. Qed. - - Lemma trans4max_c: forall (x a b c d: Z), - (x <= c)%Z -> (x <= max4 a b c d)%Z. - Proof. trans4max_tac. Qed. - - Lemma trans4max_d: forall (x a b c d: Z), - (x <= d)%Z -> (x <= max4 a b c d)%Z. - Proof. trans4max_tac. Qed. - End Trans4. - - Section BoundedMul. - Lemma bZMul_min: forall (x0 low0 high0 x1 low1 high1: Z), - (low0 <= x0)%Z -> (x0 <= high0)%Z -> - (low1 <= x1)%Z -> (x1 <= high1)%Z -> - (min4 (low0 * low1) (low0 * high1) - (high0 * low1) (high0 * high1) <= x0 * x1)%Z. - Proof. - intros x0 low0 high0 x1 low1 high1 - Hlow0 Hhigh0 Hlow1 Hhigh1. - destruct (Z_le_dec 0 x0), (Z_le_dec 0 x1). - - - apply trans4min_0. - replace 0%Z with (0*0)%Z by nomega. - apply Z.mul_le_mono_nonneg; nomega. - - - apply trans4min_c. - transitivity (x0 * low1)%Z. - - + apply Z.mul_le_mono_nonpos_r; try nomega. - + apply Z.mul_le_mono_nonneg_l; try nomega. - - - apply trans4min_b. - transitivity (x0 * high1)%Z. - - + apply Z.mul_le_mono_nonneg_r; try nomega. - + apply Z.mul_le_mono_nonpos_l; try nomega. - - - apply trans4min_0. - replace 0%Z with (0*0)%Z by nomega. - apply Z.mul_le_mono_nonpos; try nomega. - Qed. - - Lemma bZMul_max: forall (x0 low0 high0 x1 low1 high1: Z), - (low0 <= x0)%Z -> (x0 <= high0)%Z -> - (low1 <= x1)%Z -> (x1 <= high1)%Z -> - (x0 * x1 <= - max4 (low0 * low1) (low0 * high1) - (high0 * low1) (high0 * high1))%Z. - Proof. - intros x0 low0 high0 x1 low1 high1 - Hlow0 Hhigh0 Hlow1 Hhigh1. - destruct (Z_le_dec 0 x0), (Z_le_dec 0 x1). - - - apply trans4max_d. - apply Z.mul_le_mono_nonneg; nomega. - - - apply trans4max_0. - replace 0%Z with (0*0)%Z by nomega. - transitivity (x0 * 0)%Z. - - + apply Z.mul_le_mono_nonneg_l; try nomega. - + apply Z.mul_le_mono_nonpos_r; try nomega. - - - apply trans4max_0. - replace 0%Z with (0*0)%Z by nomega. - transitivity (x0 * 0)%Z. - - + apply Z.mul_le_mono_nonpos_l; try nomega. - + apply Z.mul_le_mono_nonneg_r; try nomega. - - - apply trans4max_a. - apply Z.mul_le_mono_nonpos; try nomega. - Qed. - End BoundedMul. - - Inductive BoundedZ := - | boundedZ: forall (x low high: Z), - (low <= x)%Z -> (x <= high)%Z -> BoundedZ. - - Definition bprojZ (x: BoundedZ) := - match x with - | boundedZ x0 low0 high0 plow0 phigh0 => x0 - end. - - Definition bZAdd (a b: BoundedZ): BoundedZ. - refine match a with - | boundedZ x0 low0 high0 plow0 phigh0 => - match b with - | boundedZ x1 low1 high1 plow1 phigh1 => - boundedZ (x0 + x1) (low0 + low1) (high0 + high1) _ _ - end - end; abstract nomega. - Defined. - - Definition bZSub (a b: BoundedZ): BoundedZ. - refine match a with - | boundedZ x0 low0 high0 plow0 phigh0 => - match b with - | boundedZ x1 low1 high1 plow1 phigh1 => - boundedZ (x0 - x1) (low0 - high1) (high0 - low1) _ _ - end - end; abstract nomega. - Defined. - - Definition bZMul (a b: BoundedZ): BoundedZ. - refine match a with - | boundedZ x0 low0 high0 plow0 phigh0 => - match b with - | boundedZ x1 low1 high1 plow1 phigh1 => - boundedZ (x0 * x1) - (min4 (low0 * low1) (low0 * high1) - (high0 * low1) (high0 * high1)) - (max4 (low0 * low1) (low0 * high1) - (high0 * low1) (high0 * high1)) - _ _ - end - end; try apply bZMul_min; try apply bZMul_max; try assumption. - Defined. - - Definition bZShiftr (a: BoundedZ) (k: nat): BoundedZ. - assert (forall k, 2 ^ (Z.of_nat k) > 0)%Z as H by abstract ( - intro m; - rewrite <- two_p_equiv; - apply two_p_gt_ZERO; - induction m; try reflexivity; - rewrite Nat2Z.inj_succ; - nomega). - - refine match a with - | boundedZ x low high plow phigh => - boundedZ (Z.shiftr x (Z.of_nat k)) - (Z.shiftr low (Z.of_nat k)) - (Z.succ (Z.shiftr high (Z.of_nat k))) _ _ - end. - - - abstract ( - repeat rewrite Z.shiftr_div_pow2; - try apply Nat2Z.is_nonneg; - apply Z_div_le; try assumption; - try apply H). - - - abstract ( - apply Z.lt_succ_r; - repeat rewrite Z.shiftr_div_pow2; - try apply Nat2Z.is_nonneg; - apply Z.lt_lt_succ_r; - apply Z.lt_succ_r; - apply Z_div_le; - try apply H; - try assumption). - Qed. - - Definition bZMask (a: BoundedZ) (k: nat): BoundedZ. - assert (0 < 2 ^ Z.of_nat k)%Z as Hk by ( - induction k; - try abstract (vm_compute; reflexivity); - rewrite Nat2Z.inj_succ; - rewrite <- two_p_equiv; - apply Z.gt_lt; - apply two_p_gt_ZERO; - apply Z.le_le_succ_r; - apply Nat2Z.is_nonneg). - - refine match a with - | boundedZ x low high plow phigh => - boundedZ (Z.land x (Z.ones (Z.of_nat k))) - (Z.of_N 0%N) - (Z.of_N (Npow2 k)) _ _ - end. - - - repeat rewrite Z.land_ones; - try apply Nat2Z.is_nonneg. - - abstract ( - apply (Z.mod_pos_bound x) in Hk; destruct Hk; - induction k; simpl in *; assumption). - - - repeat rewrite Z.land_ones; - try apply Nat2Z.is_nonneg. - - abstract ( - rewrite Npow2_N; - rewrite N2Z.inj_pow; simpl; - apply (Z.mod_pos_bound x) in Hk; destruct Hk; - apply Z.lt_le_incl; - induction k; simpl in *; assumption). - Qed. -End BoundedZ. - -Section BoundedN. - - Inductive BoundedN := - | boundedN: forall (x low high: N), - (low <= x)%N -> (x < high)%N -> BoundedN. - - Definition bprojN (x: BoundedN) := - match x with - | boundedN x0 low0 high0 plow0 phigh0 => x0 - end. - - Definition bNAdd (a b: BoundedN): BoundedN. - refine match a with - | boundedN x0 low0 high0 plow0 phigh0 => - match b with - | boundedN x1 low1 high1 plow1 phigh1 => - boundedN (x0 + x1) (low0 + low1) (high0 + high1) _ _ - end - end. - - - abstract (apply N.add_le_mono; assumption). - - abstract nomega. - Defined. - - Definition bNSub (a b: BoundedN): BoundedN. - refine match a with - | boundedN x0 low0 high0 plow0 phigh0 => - match b with - | boundedN x1 low1 high1 plow1 phigh1 => - boundedN (x0 - x1) (low0 - high1) (N.succ (high0 - low1)) _ _ - end - end. - - - transitivity (x0 - high1)%N. - - + apply N.sub_le_mono_r; assumption. - + apply N.sub_le_mono_l; apply N.lt_le_incl; assumption. - - - apply N.lt_succ_r; transitivity (high0 - x1)%N. - - + apply N.sub_le_mono_r; apply N.lt_le_incl; assumption. - + apply N.sub_le_mono_l; assumption. - - Defined. - - Definition bNMul (a b: BoundedN): BoundedN. - refine match a with - | boundedN x0 low0 high0 plow0 phigh0 => - match b with - | boundedN x1 low1 high1 plow1 phigh1 => - boundedN (x0 * x1)%N (low0 * low1)%N (high0 * high1)%N _ _ - end - end; abstract ( - try apply N.mul_le_mono_nonneg; - try apply N.mul_lt_mono_nonneg; - try assumption; - try apply N_ge_0). - Qed. - - Definition bNShiftr (a: BoundedN) (k: nat): BoundedN. - assert (forall k, 2 ^ (N.of_nat k) > 0)%N as H by abstract ( - intros; - rewrite <- Npow2_N; - apply N.lt_gt; - apply Npow2_gt0). - - refine match a with - | boundedN x low high plow phigh => - boundedN (N.shiftr x (N.of_nat k)) - (N.shiftr low (N.of_nat k)) - (N.succ (N.shiftr high (N.of_nat k))) _ _ - end. - - - repeat rewrite N.shiftr_div_pow2. - apply N.div_le_mono; try assumption. - pose proof (H k) as H0. - induction ((2 ^ N.of_nat k)%N); - [inversion H0; intuition |]. - apply N.neq_0_lt_0; apply N.gt_lt; assumption. - - - apply N.lt_succ_r. - repeat rewrite N.shiftr_div_pow2. - apply N.div_le_mono; [|apply N.lt_le_incl; assumption]. - pose proof (H k) as H0. - induction ((2 ^ N.of_nat k)%N); - [inversion H0; intuition |]. - apply N.neq_0_lt_0; apply N.gt_lt; assumption. - Defined. - - Definition bNMask (a: BoundedN) (k: nat): BoundedN. - assert (forall k, 0 < 2 ^ (N.of_nat k))%N as H by abstract ( - intros; - rewrite <- Npow2_N; - apply Npow2_gt0). - - refine match a with - | boundedN x low high plow phigh => - boundedN (N.land x (N.ones (N.of_nat k))) - 0%N - (Npow2 k) _ _ - end. - - - repeat rewrite N.land_ones; - apply N_ge_0. - - - repeat rewrite N.land_ones. - - abstract ( - rewrite Npow2_N; - pose proof (N.mod_bound_pos x (2 ^ N.of_nat k)%N (N_ge_0 _) (H k)) - as H0; destruct H0; - assumption). - Defined. - -End BoundedN. - -Section BoundedWord. - Context {n: nat}. - - Section BoundedSub. - Lemma NToWord_Npow2: wzero n = NToWord n (Npow2 n). - Proof. - induction n as [|n0]. - - + repeat rewrite shatter_word_0; reflexivity. - - + unfold wzero in *; simpl in *. - rewrite IHn0; simpl. - induction (Npow2 n0); simpl; reflexivity. - Qed. - - Lemma bWSub_lem0: forall (x0 x1: word n) (low0 high1: N), - (low0 <= wordToN x0)%N -> (wordToN x1 < high1)%N -> - (low0 - high1 <= & (x0 ^- x1))%N. - Proof. - intros. - - destruct (Nge_dec (wordToN x1) 1)%N as [e|e]. - destruct (Nge_dec (wordToN x1) (wordToN x0)). - - - unfold wminus, wneg. - assert (low0 < high1)%N. { - apply (N.le_lt_trans _ (wordToN x0) _); [assumption|]. - apply (N.le_lt_trans _ (wordToN x1) _); [apply N.ge_le|]; assumption. - } - - replace (low0 - high1)%N with 0%N; [apply N_ge_0|]. - symmetry. - apply N.sub_0_le. - apply N.lt_le_incl. - assumption. - - - transitivity (wordToN x0 - wordToN x1)%N. - - + transitivity (wordToN x0 - high1)%N. - - * apply N.sub_le_mono_r; assumption. - - * apply N.sub_le_mono_l; apply N.lt_le_incl; assumption. - - + assert (& x0 - & x1 < Npow2 n)%N. { - transitivity (wordToN x0); - try apply word_size_bound; - apply N.sub_lt. - - + apply N.lt_le_incl; assumption. - - + nomega. - } - - assert (& x0 - & x1 + & x1 < Npow2 n)%N. { - replace (wordToN x0 - wordToN x1 + wordToN x1)%N - with (wordToN x0) by nomega. - apply word_size_bound. - } - - assert (x0 = NToWord n (wordToN x0 - wordToN x1) ^+ x1) as Hv. { - apply NToWord_equal. - rewrite <- wordize_plus; rewrite wordToN_NToWord; - try assumption. - nomega. - } - - apply N.eq_le_incl. - rewrite Hv. - unfold wminus. - rewrite <- wplus_assoc. - rewrite wminus_inv. - rewrite (wplus_comm (NToWord n (wordToN x0 - wordToN x1)) (wzero n)). - rewrite wplus_unit. - rewrite <- wordize_plus; [nomega|]. - rewrite wordToN_NToWord; assumption. - - - unfold wminus, wneg. - assert (wordToN x1 = 0)%N as e' by nomega. - rewrite e'. - replace (Npow2 n - 0)%N with (Npow2 n) by nomega. - rewrite <- NToWord_Npow2. - - erewrite <- wordize_plus; - try rewrite wordToN_zero; - replace (wordToN x0 + 0)%N with (wordToN x0)%N by nomega; - try apply word_size_bound. - - transitivity low0; try assumption. - apply N.le_sub_le_add_r. - apply N.le_add_r. - Qed. - - Lemma bWSub_lem1: forall (x0 x1: word n) (low1 high0: N), - (low1 <= wordToN x1)%N -> (wordToN x0 < high0)%N -> - (& (x0 ^- x1) < N.succ (high0 + Npow2 n - low1))%N. - Proof. - intros; unfold wminus. - destruct (Nge_dec (wordToN x1) 1)%N as [e|e]. - destruct (Nge_dec (wordToN x0) (wordToN x1)). - - - apply N.lt_succ_r. - assert (& x0 - & x1 < Npow2 n)%N. { - transitivity (wordToN x0); - try apply word_size_bound; - apply N.sub_lt. - - + apply N.ge_le; assumption. - - + nomega. - } - - assert (& x0 - & x1 + & x1 < Npow2 n)%N. { - replace (wordToN x0 - wordToN x1 + wordToN x1)%N - with (wordToN x0) by nomega. - apply word_size_bound. - } - - assert (x0 = NToWord n (wordToN x0 - wordToN x1) ^+ x1) as Hv. { - apply NToWord_equal. - rewrite <- wordize_plus; rewrite wordToN_NToWord; - try assumption. - nomega. - } - - rewrite Hv. - rewrite <- wplus_assoc. - rewrite wminus_inv. - rewrite wplus_comm. - rewrite wplus_unit. - rewrite wordToN_NToWord. - - + transitivity (wordToN x0 - low1)%N. - - * apply N.sub_le_mono_l; assumption. - - * apply N.sub_le_mono_r. - transitivity high0; [apply N.lt_le_incl; assumption|]. - replace' high0 with (high0 + 0)%N at 1 by nomega. - apply N.add_le_mono_l. - apply N_ge_0. - - + transitivity (wordToN x0); try apply word_size_bound. - nomega. - - - rewrite <- wordize_plus; [apply N.lt_succ_r|]. - - + transitivity (high0 + (wordToN (wneg x1)))%N. - - * apply N.add_le_mono_r; apply N.lt_le_incl; assumption. - - * unfold wneg. - rewrite wordToN_NToWord; [|abstract ( - apply N.sub_lt; - try apply N.lt_le_incl; - try apply word_size_bound; - nomega )]. - - rewrite N.add_sub_assoc; [|abstract ( - try apply N.lt_le_incl; - try apply word_size_bound)]. - - apply N.sub_le_mono_l. - assumption. - - + unfold wneg. - - rewrite wordToN_NToWord; [|abstract ( - apply N.sub_lt; - try apply N.lt_le_incl; - try apply word_size_bound; - nomega )]. - - replace (wordToN x0 + (Npow2 n - wordToN x1))%N - with (Npow2 n - (wordToN x1 - wordToN x0))%N. - - * apply N.sub_lt; try nomega. - transitivity (wordToN x1); [apply N.le_sub_l|]. - apply N.lt_le_incl. - apply word_size_bound. - - * apply N.add_sub_eq_l. - rewrite <- N.add_sub_swap; - [|apply N.lt_le_incl; assumption]. - rewrite (N.add_comm (wordToN x0)). - rewrite N.add_assoc. - rewrite N.add_sub_assoc; - [|apply N.lt_le_incl; apply word_size_bound]. - rewrite N.add_sub. - rewrite N.add_comm. - rewrite N.add_sub. - reflexivity. - - - apply N.lt_succ_r. - assert (wordToN x1 = 0)%N as e' by nomega. - assert (NToWord n (wordToN x1) = NToWord n 0%N) as E by - (rewrite e'; reflexivity). - rewrite NToWord_wordToN in E. - simpl in E; rewrite wzero'_def in E. - rewrite E. - unfold wneg. - rewrite wordToN_zero. - rewrite N.sub_0_r. - rewrite <- NToWord_Npow2. - rewrite wplus_comm. - rewrite wplus_unit. - transitivity high0. - - + apply N.lt_le_incl. - assumption. - - + rewrite <- N.add_sub_assoc. - - * replace high0 with (high0 + 0)%N by nomega. - apply N.add_le_mono; [|apply N_ge_0]. - apply N.eq_le_incl. - rewrite N.add_0_r. - reflexivity. - - * transitivity (wordToN x1); - [ assumption - | apply N.lt_le_incl; - apply word_size_bound]. - - Qed. - End BoundedSub. - - Inductive BoundedWord := - | boundedWord: forall (x: word n) (low high: N) (overflowed: bool), - (low <= wordToN x)%N -> (wordToN x < high)%N -> BoundedWord. - - Definition bprojW (x: BoundedWord) := - match x with - | boundedWord x0 _ _ _ _ _ => x0 - end. - - Definition bWAdd (a b: BoundedWord): BoundedWord. - refine match a with - | boundedWord x0 low0 high0 o0 plow0 phigh0 => - match b with - | boundedWord x1 low1 high1 o1 plow1 phigh1 => - if (overflows n (high0 + high1)) - then boundedWord (x0 ^+ x1) 0%N (high0 + high1) (orb o0 o1) _ _ - else boundedWord (x0 ^+ x1) (low0 + low1) (high0 + high1) true _ _ - end - end; try abstract ( - apply (N.le_lt_trans _ (wordToN x0 + wordToN x1)%N _); - try apply plus_le; - abstract nomega). - - - apply N_ge_0. - - - erewrite <- wordize_plus'; - try eassumption; - try abstract nomega. - - + apply N.add_le_mono; assumption. - - + abstract (apply N.lt_le_incl; nomega). - Qed. - - Definition bWSub (a b: BoundedWord): BoundedWord. - refine match a with - | boundedWord x0 low0 high0 o0 plow0 phigh0 => - match b with - | boundedWord x1 low1 high1 o1 plow1 phigh1 => - let upper_bound := - if (Nge_dec high0 (Npow2 n)) - then Npow2 n - else if (Nge_dec high1 (Npow2 n)) - then Npow2 n - else (N.succ (high0 + Npow2 n - low1)) in - - if (Nge_dec low0 high1) - then boundedWord (x0 ^- x1) (low0 - high1)%N upper_bound (orb o0 o1) _ _ - else boundedWord (x0 ^- x1) 0%N upper_bound (orb o0 o1) _ _ - end - end; abstract (unfold upper_bound; try apply N_ge_0; - destruct (Nge_dec high0 (Npow2 n)), (Nge_dec high1 (Npow2 n)); - repeat match goal with - | [|- (_ - ?x <= wordToN _)%N] => apply bWSub_lem0 - | [|- (wordToN _ < N.succ (?x + _ - _))%N] => apply bWSub_lem1 - | [|- (wordToN _ < Npow2 _)%N] => apply word_size_bound - | [|- (0 <= _)%N] => apply N_ge_0 - end; assumption). - Qed. - - Definition bWMul (a b: BoundedWord): BoundedWord. - refine match a with - | boundedWord x0 low0 high0 o0 plow0 phigh0 => - match b with - | boundedWord x1 low1 high1 o1 plow1 phigh1 => - if (overflows n (high0 * high1)) - then boundedWord (x0 ^* x1)%N 0%N (high0 * high1)%N true _ _ - else boundedWord (x0 ^* x1)%N (low0 * low1)%N (high0 * high1)%N (orb o0 o1) _ _ - end - end. - - - apply N_ge_0. - - - apply (N.le_lt_trans _ (wordToN x0 * wordToN x1)%N _); [apply mult_le|]. - apply N.mul_lt_mono; assumption. - - - rewrite <- wordize_mult. - - + apply N.mul_le_mono; assumption. - - + transitivity (high0 * high1)%N; [|assumption]. - apply N.mul_lt_mono; assumption. - - - apply (N.le_lt_trans _ (wordToN x0 * wordToN x1)%N _); [apply mult_le|]. - apply N.mul_lt_mono; assumption. - Qed. - - Definition bWShiftr (a: BoundedWord) (k: nat): BoundedWord. - assert (forall k, 2 ^ (N.of_nat k) > 0)%N as H by abstract ( - intros; - rewrite <- Npow2_N; - apply N.lt_gt; - apply Npow2_gt0). - - refine match a with - | boundedWord x low high o plow phigh => - boundedWord (extend _ (shiftr x k)) - (N.shiftr low (N.of_nat k)) - (N.succ (N.shiftr high (N.of_nat k))) o _ _ - end. - - - unfold extend; rewrite wordToN_convS. - - rewrite wordToN_zext. - rewrite <- wordize_shiftr. - rewrite <- Nshiftr_equiv_nat. - repeat rewrite N.shiftr_div_pow2. - apply N.div_le_mono; try assumption. - pose proof (H k) as H0. - induction ((2 ^ N.of_nat k)%N); - [inversion H0; intuition |]. - apply N.neq_0_lt_0; apply N.gt_lt; assumption. - - - unfold extend; rewrite wordToN_convS. - rewrite wordToN_zext. - rewrite Nshiftr_equiv_nat. - eapply N.lt_le_trans; [apply shiftr_bound; eassumption|]. - try apply N.eq_le_incl. - try eassumption; reflexivity. - - (* TODO(rsloan): how do we fix this? *) - Unshelve. - reflexivity. - Qed. - - Definition bWMask (a: BoundedWord) (k: nat): BoundedWord. - refine match a with - | boundedWord x low high o plow phigh => - boundedWord (mask k x) 0%N (Npow2 k) o _ _ - end; [apply N_ge_0 | apply mask_bound]. - Qed. -End BoundedWord. \ No newline at end of file diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v index 53612cfbb..2ff50e0e1 100644 --- a/src/Assembly/Compile.v +++ b/src/Assembly/Compile.v @@ -10,31 +10,46 @@ Require Import Crypto.Assembly.QhasmCommon. Require Import Crypto.Assembly.Qhasm. Module CompileHL. - Context {ivar : type -> Type}. - Context {ovar : Type}. - - Fixpoint compile {t} (e:@HL.expr Z (@LL.arg Z Z) t) : @LL.expr Z Z t := - match e with - | HL.Const n => LL.Return (LL.Const n) - | HL.Var _ arg => LL.Return arg - | HL.Binop t1 t2 t3 op e1 e2 => - LL.under_lets (@compile _ e1) (fun arg1 => - LL.under_lets (@compile _ e2) (fun arg2 => - LL.LetBinop op arg1 arg2 (fun v => - LL.Return v))) - | HL.Let _ ex _ eC => - LL.under_lets (@compile _ ex) (fun arg => @compile _ (eC arg)) - | HL.Pair t1 e1 t2 e2 => - LL.under_lets (@compile _ e1) (fun arg1 => - LL.under_lets (@compile _ e2) (fun arg2 => - LL.Return (LL.Pair arg1 arg2))) - | HL.MatchPair _ _ ep _ eC => - LL.under_lets (@compile _ ep) (fun arg => - let (a1, a2) := LL.match_arg_Prod arg in @compile _ (eC a1 a2)) - end. + Section Compilation. + Context {T: Type}. + + Fixpoint compile {V t} (e:@HL.expr T (@LL.arg T V) t) : @LL.expr T V t := + match e with + | HL.Const n => LL.Return (LL.Const n) + + | HL.Var _ arg => LL.Return arg + + | HL.Binop t1 t2 t3 op e1 e2 => + LL.under_lets (compile e1) (fun arg1 => + LL.under_lets (compile e2) (fun arg2 => + LL.LetBinop op arg1 arg2 (fun v => + LL.Return v))) + + | HL.Let _ ex _ eC => + LL.under_lets (compile ex) (fun arg => + compile (eC arg)) + + | HL.Pair t1 e1 t2 e2 => + LL.under_lets (compile e1) (fun arg1 => + LL.under_lets (compile e2) (fun arg2 => + LL.Return (LL.Pair arg1 arg2))) + + | HL.MatchPair _ _ ep _ eC => + LL.under_lets (compile ep) (fun arg => + let (a1, a2) := LL.match_arg_Prod arg in + compile (eC a1 a2)) + end. + + Definition Expr' t : Type := forall var, @HL.expr T (@LL.arg T var) t. + + Definition Compile {t} (e:@Expr' t) : @LL.Expr T t := + fun var => compile (e var). + End Compilation. Section Correctness. - Lemma compile_correct {_: Evaluable Z} {t} e1 e2 G (wf:HL.wf G e1 e2) : + Context {T: Type}. + + Lemma compile_correct {_: Evaluable T} {t} e1 e2 G (wf:HL.wf G e1 e2) : List.Forall (fun v => let 'existT _ (x, a) := v in LL.interp_arg a = x) G -> LL.interp (compile e2) = HL.interp e1 :> interp_type t. Proof. @@ -69,8 +84,8 @@ Module CompileLL. Section Compile. Context {n: nat} {w: Width n}. - Definition WArg t': Type := @LL.arg (word n) (word n) t'. - Definition WExpr t': Type := @LL.expr (word n) (word n) t'. + Definition WArg t': Type := @LL.arg (word n) Z t'. + Definition WExpr t': Type := @LL.expr (word n) Z t'. Section Mappings. Definition indexize (x: nat) : Index n. @@ -85,7 +100,7 @@ Module CompileLL. Definition getMapping (x: WArg TT) := match x with | Const v => constM n (@constant n w v) - | Var v => regM n (@reg n w (wordToNat v)) + | Var v => regM n (@reg n w (Z.to_nat v)) end. Definition getReg (x: Mapping n): option (Reg n) := @@ -188,7 +203,7 @@ Module CompileLL. match t as t' return WArg t' -> list nat with | TT => fun a' => match a' with - | Var v' => [wordToNat v'] + | Var v' => [Z.to_nat v'] | _ => @nil nat end | Prod t0 t1 => fun a' => @@ -239,7 +254,7 @@ Module CompileLL. omap (getOutputSlot nextRegName op' x' y') (fun r => let var := match t3 as t3' return WArg t3' with - | TT => Var (natToWord n r) + | TT => Var (Z.of_nat r) | _ => zeros _ end in @@ -266,13 +281,13 @@ Module CompileLL. (fun rt var op x y out => Some out) (fun t' a => Some (vars a)). - Fixpoint fillInputs {t inputs} (prog: NAry inputs (WArg TT) (WExpr t)) {struct inputs}: WExpr t := - match inputs as inputs' return NAry inputs' (WArg TT) (WExpr t) -> NAry O (WArg TT) (WExpr t) with + Fixpoint fillInputs {t inputs} (prog: NAry inputs Z (WExpr t)) {struct inputs}: WExpr t := + match inputs as inputs' return NAry inputs' Z (WExpr t) -> NAry O Z (WExpr t) with | O => fun p => p - | S inputs'' => fun p => fillInputs (p (Var (natToWord _ inputs))) + | S inputs'' => fun p => fillInputs (p (Z.of_nat inputs)) end prog. - Definition compile {t inputs} (p: NAry inputs (WArg TT) (WExpr t)): option (Program * list nat) := + Definition compile {t inputs} (p: NAry inputs Z (WExpr t)): option (Program * list nat) := let p' := fillInputs p in omap (getOuts _ (S inputs) p') (fun outs => diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v index 593aa06a4..436a6639b 100644 --- a/src/Assembly/Conversions.v +++ b/src/Assembly/Conversions.v @@ -61,25 +61,12 @@ Module HLConversions. convertExpr (f x y)) end. - Fixpoint convertExpr' {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t} (a: expr (T := A) (var := @interp_type A) t): expr (T := B) (var := @interp_type B) t := - match a with - | Const x => Const (@toT B EB (@fromT A EA x)) - | Var t x => @Var B _ t (convertVar x) - | Binop t1 t2 t3 o e1 e2 => - @Binop B _ t1 t2 t3 o (convertExpr' e1) (convertExpr' e2) - | Let tx e tC f => - Let (convertExpr' e) (fun x => convertExpr' (f (convertVar x))) - | Pair t1 e1 t2 e2 => Pair (convertExpr' e1) (convertExpr' e2) - | MatchPair t1 t2 e tC f => MatchPair (convertExpr' e) (fun x y => - convertExpr' (f (convertVar x) (convertVar y))) - end. - Definition convertZToWord {t} n v a := - @convertExpr Z (word n) ZEvaluable (@WordEvaluable n) t v a. + @convertExpr Z (word n) (@ZEvaluable n) (@WordEvaluable n) t v a. Definition convertZToBounded {t} n v a := @convertExpr Z (option (@BoundedWord n)) - ZEvaluable (@BoundedEvaluable n) t v a. + (@ZEvaluable n) (@BoundedEvaluable n) t v a. Definition ZToWord {t} n (a: @Expr Z t): @Expr (word n) t := fun v => convertZToWord n v (a v). @@ -97,316 +84,130 @@ Module HLConversions. Binop OPadd (Var x) (Var y)))))%Z. Example interp_example_range : - option_map high (BInterp (ZToRange 32 example_Expr)) = Some 28%N. + option_map bw_high (BInterp (ZToRange 32 example_Expr)) = Some 28%N. Proof. cbv; reflexivity. Qed. End HLConversions. Module LLConversions. Import LL. - Definition convertVar {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t} (a: interp_type (T := A) t): interp_type (T := B) t. - Proof. - induction t as [| t3 IHt1 t4 IHt2]. + Section VarConv. + Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}. - - refine (@toT B EB (@fromT A EA _)); assumption. - - - destruct a as [a1 a2]; constructor; - [exact (IHt1 a1) | exact (IHt2 a2)]. - Defined. - - Fixpoint convertArg {A B: Type} {EA: Evaluable A} {EB: Evaluable B} t {struct t}: @arg A A t -> @arg B B t := - match t as t' return @arg A A t' -> @arg B B t' with - | TT => fun x => - match x with - | Const c => Const (convertVar (t := TT) c) - | Var v => Var (convertVar (t := TT) v) - end - | Prod t0 t1 => fun x => - match (match_arg_Prod x) with - | (a, b) => Pair ((convertArg t0) a) ((convertArg t1) b) - end - end. - - Arguments convertArg [_ _ _ _ _ _]. - - Fixpoint convertExpr {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t} (a: expr (T := A) t): expr (T := B) t := - match a with - | LetBinop _ _ out op a b _ eC => - LetBinop (T := B) op (convertArg a) (convertArg b) (fun x: (arg out) => convertExpr (eC (convertArg x))) - | Return _ a => Return (convertArg a) - end. - - Definition convertZToWord {t} n a := - @convertExpr Z (word n) ZEvaluable (@WordEvaluable n) t a. - - Definition convertZToBounded {t} n a := - @convertExpr Z (option (@BoundedWord n)) ZEvaluable (@BoundedEvaluable n) t a. - - Definition zinterp {t} E := @interp Z ZEvaluable t E. - - Definition wordInterp {n t} E := @interp (word n) (@WordEvaluable n) t E. - - Definition boundedInterp {n t} E: @interp_type (option (@BoundedWord n)) t := - @interp (option (@BoundedWord n)) (@BoundedEvaluable n) t E. - - Section Correctness. - (* Aliases to make the proofs easier to read. *) - - Definition varZToBounded {n t} (v: @interp_type Z t): @interp_type (option (@BoundedWord n)) t := - @convertVar Z (option (@BoundedWord n)) ZEvaluable BoundedEvaluable t v. - - Definition varBoundedToZ {n t} (v: @interp_type _ t): @interp_type Z t := - @convertVar (option (@BoundedWord n)) Z BoundedEvaluable ZEvaluable t v. - - Definition varZToWord {n t} (v: @interp_type Z t): @interp_type (@word n) t := - @convertVar Z (@word n) ZEvaluable (@WordEvaluable n) t v. - - Definition varWordToZ {n t} (v: @interp_type (@word n) t): @interp_type Z t := - @convertVar (word n) Z (@WordEvaluable n) ZEvaluable t v. - - Definition zOp {tx ty tz: type} (op: binop tx ty tz) - (x: @interp_type Z tx) (y: @interp_type Z ty): @interp_type Z tz := - @interp_binop Z ZEvaluable _ _ _ op x y. - - Definition wOp {n} {tx ty tz: type} (op: binop tx ty tz) - (x: @interp_type _ tx) (y: @interp_type _ ty): @interp_type _ tz := - @interp_binop (word n) (@WordEvaluable n) _ _ _ op x y. - - Definition bOp {n} {tx ty tz: type} (op: binop tx ty tz) - (x: @interp_type _ tx) (y: @interp_type _ ty): @interp_type _ tz := - @interp_binop (option (@BoundedWord n)) BoundedEvaluable _ _ _ op x y. - - Definition boundedArg {n t} (x: @arg (option (@BoundedWord n)) (option (@BoundedWord n)) t) := - @interp_arg _ _ x. + Definition convertVar {t} (a: interp_type (T := A) t): interp_type (T := B) t. + Proof. + induction t as [| t3 IHt1 t4 IHt2]. - Definition wordArg {n t} (x: @arg (word n) (word n) t) := @interp_arg _ _ x. + - refine (@toT B EB (@fromT A EA _)); assumption. - (* BoundedWord-based Bounds-checking fixpoint *) + - destruct a as [a1 a2]; constructor; + [exact (IHt1 a1) | exact (IHt2 a2)]. + Defined. + End VarConv. - Definition getBounds {n t} T (E: Evaluable T) (e : @expr T T t): @interp_type (option (@BoundedWord n)) t := - interp (E := BoundedEvaluable) (@convertExpr T (option (@BoundedWord n)) E BoundedEvaluable t e). + Section ArgConv. + Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}. - Fixpoint bcheck' {n t} (x: @interp_type (option (@BoundedWord n)) t) := - match t as t' return (interp_type t') -> bool with - | TT => fun x' => - match x' with - | Some _ => true - | None => false + Fixpoint convertArg {V} t {struct t}: @arg A V t -> @arg B V t := + match t as t' return @arg A V t' -> @arg B V t' with + | TT => fun x => + match x with + | Const c => Const (convertVar (t := TT) c) + | Var v => Var v end - | Prod t0 t1 => fun x' => - match x' with - | (x0, x1) => andb (bcheck' x0) (bcheck' x1) + | Prod t0 t1 => fun x => + match (match_arg_Prod x) with + | (a, b) => Pair ((convertArg t0) a) ((convertArg t1) b) end - end x. - - Definition bcheck {n t} T (E: Evaluable T) (e : @expr T T t): bool := bcheck' (n := n) (getBounds T E e). - - (* Utility Lemmas *) - - Lemma convertArg_interp: forall {A B t} {EA: Evaluable A} {EB: Evaluable B} (x: @arg A A t), - (interp_arg (@convertArg A B EA EB t x)) = @convertVar A B EA EB t (interp_arg x). - Proof. - induction x as [| |t0 t1 i0 i1]; [reflexivity|reflexivity|]. - induction EA, EB; simpl; f_equal; assumption. - Qed. - - Lemma convertArg_var: forall {A B EA EB t} (x: @interp_type A t), - @convertArg A B EA EB t (uninterp_arg x) = uninterp_arg (@convertVar A B EA EB t x). - Proof. - induction t as [|t0 IHt_0 t1 IHt_1]; simpl; intros; [reflexivity|]. - induction x as [a b]; simpl; f_equal; - induction t0 as [|t0a IHt0_0 t0b IHt0_1], - t1 as [|t1a IHt1_0]; simpl in *; - try rewrite IHt_0; - try rewrite IHt_1; - reflexivity. - Qed. - - Ltac kill_just n := - match goal with - | [|- context[just ?x] ] => - let Hvalue := fresh in let Hvalue' := fresh in - let Hlow := fresh in let Hlow' := fresh in - let Hhigh := fresh in let Hhigh' := fresh in - let Hnone := fresh in let Hnone' := fresh in - - let B := fresh in - - pose proof (just_value_spec (n := n) x) as Hvalue; - pose proof (just_low_spec (n := n) x) as Hlow; - pose proof (just_high_spec (n := n) x) as Hhigh; - pose proof (just_None_spec (n := n) x) as Hnone; - - destruct (just x); - - try pose proof (Hlow _ eq_refl) as Hlow'; - try pose proof (Hvalue _ eq_refl) as Hvalue'; - try pose proof (Hhigh _ eq_refl) as Hhigh'; - try pose proof (Hnone eq_refl) as Hnone'; - - clear Hlow Hhigh Hvalue Hnone end. + End ArgConv. - Ltac kill_dec := - repeat match goal with - | [|- context[Nge_dec ?a ?b] ] => destruct (Nge_dec a b) - | [H : context[Nge_dec ?a ?b] |- _ ] => destruct (Nge_dec a b) - end. + Section ExprConv. + Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}. - Lemma ZToBounded_binop_correct : forall {n tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e, - bcheck (n := n) (t := tz) Z ZEvaluable (LetBinop op x y e) = true - -> zOp op (interp_arg x) (interp_arg y) = - varBoundedToZ (bOp (n := n) op (varZToBounded (interp_arg x)) (varZToBounded (interp_arg y))). - Proof. - Admitted. + Fixpoint convertExpr {t V} (a: @expr A V t): @expr B V t := + match a with + | LetBinop _ _ out op a b _ eC => + LetBinop (T := B) op (convertArg _ a) (convertArg _ b) (fun x: (arg out) => + convertExpr (eC (convertArg _ x))) - Lemma ZToWord_binop_correct : forall {n tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e, - bcheck (n := n) (t := tz) Z ZEvaluable (LetBinop op x y e) = true - -> zOp op (interp_arg x) (interp_arg y) = - varWordToZ (wOp (n := n) op (varZToWord (interp_arg x)) (varZToWord (interp_arg y))). - Proof. - Admitted. + | Return _ a => Return (convertArg _ a) + end. + End ExprConv. - Lemma just_zero: forall n, exists x, just (n := n) 0 = Some x. - Proof. - Admitted. + Section Defaults. + Context {t: type} {n: nat}. - (* Main correctness guarantee *) + Definition Word := word n. + Definition Bounded := option (@BoundedWord n). + Definition RWV := option (RangeWithValue). - Lemma RangeInterp_bounded_spec: forall {n t} (E: expr t), - bcheck (n := n) Z ZEvaluable E = true - -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E) = wordInterp (convertZToWord n E). - Proof. - intros n t E S. - unfold convertZToBounded, zinterp, convertZToWord, wordInterp. + Transparent Word Bounded RWV. - induction E as [tx ty tz op x y z|]; simpl; try reflexivity. + Instance RWVEvaluable' : Evaluable RWV := @RWVEvaluable n. + Instance ZEvaluable' : Evaluable Z := @ZEvaluable n. - - repeat rewrite convertArg_var in *. - repeat rewrite convertArg_interp in *. + Existing Instance ZEvaluable'. + Existing Instance WordEvaluable. + Existing Instance BoundedEvaluable. + Existing Instance RWVEvaluable'. - rewrite H; clear H; repeat f_equal. + Definition ZToWord a := @convertExpr Z Word _ _ t a. + Definition ZToBounded a := @convertExpr Z Bounded _ _ t a. + Definition ZToRWV a := @convertExpr Z RWV _ _ t a. - + pose proof (ZToWord_binop_correct (n := n) op x y) as C; - unfold zOp, wOp, varWordToZ, varZToWord in C; - simpl in C. + Definition varZToWord a := @convertVar Z Word _ _ t a. + Definition varZToBounded a := @convertVar Z Bounded _ _ t a. + Definition varZToRWV a := @convertVar Z RWV _ _ t a. - induction op; apply (C (fun _ => Return (Const 0%Z))); clear C; - unfold bcheck, getBounds; simpl; - destruct (@just_zero n) as [j p]; rewrite p; reflexivity. + Definition varWordToZ a := @convertVar Word Z _ _ t a. + Definition varBoundedToZ a := @convertVar Bounded Z _ _ t a. + Definition varRWVToZ a := @convertVar RWV Z _ _ t a. - + unfold bcheck, getBounds in *; simpl in *. - replace (interp_binop op _ _) - with (varBoundedToZ (n := n) (bOp (n := n) op - (boundedArg (@convertArg _ _ ZEvaluable (@BoundedEvaluable n) _ x)) - (boundedArg (@convertArg _ _ ZEvaluable (@BoundedEvaluable n) _ y)))); - [unfold varBoundedToZ, boundedArg; rewrite <- convertArg_var; assumption |]. + Definition zinterp E := @interp Z _ t E. + Definition wordInterp E := @interp' Word _ _ t (fun x => NToWord n (Z.to_N x)) E. + Definition boundedInterp E := @interp Bounded _ t E. + Definition rwvInterp E := @interp RWV _ t E. - pose proof (ZToBounded_binop_correct (n := n) op x y) as C; - unfold boundedArg, zOp, wOp, varZToBounded, - varBoundedToZ, convertZToBounded in *; - simpl in C. + Section Operations. + Context {tx ty tz: type}. - repeat rewrite convertArg_interp; symmetry. + Definition opZ (op: binop tx ty tz) + (x: @interp_type Z tx) (y: @interp_type Z ty): @interp_type Z tz := + @interp_binop Z _ _ _ _ op x y. - induction op; apply (C (fun _ => Return (Const 0%Z))); clear C; - unfold bcheck, getBounds; simpl; - destruct (@just_zero n) as [j p]; rewrite p; reflexivity. + Definition opBounded (op: binop tx ty tz) + (x: @interp_type Bounded tx) (y: @interp_type Bounded ty): @interp_type Bounded tz := + @interp_binop Bounded _ _ _ _ op x y. - - simpl in S. - induction a as [| |t0 t1 a0 IHa0 a1 IHa1]; simpl in *; try reflexivity. - apply andb_true_iff in S; destruct S; rewrite IHa0, IHa1; try reflexivity; assumption. - Qed. - End Correctness. - - Section FastCorrect. - Context {n: nat}. - - Record RangeWithValue := rwv { - low: N; - value: N; - high: N; - }. - - Definition rwv_app {rangeF wordF} - (op: @validBinaryWordOp n rangeF wordF) - (X Y: RangeWithValue): option (RangeWithValue) := - omap (rangeF (range N (low X) (high X)) (range N (low Y) (high Y))) (fun r' => - match r' with - | range l h => Some ( - rwv l (wordToN (wordF (NToWord n (value X)) (NToWord n (value Y)))) h) - end). - - Definition proj (x: RangeWithValue): Range N := range N (low x) (high x). - - Definition from_range (x: Range N): RangeWithValue := - match x with - | range l h => rwv l h h - end. + Definition opWord (op: binop tx ty tz) + (x: @interp_type Word tx) (y: @interp_type Word ty): @interp_type Word tz := + @interp_binop Word _ _ _ _ op x y. - Instance RWVEval : Evaluable (option RangeWithValue) := { - ezero := None; + Definition opRWV (op: binop tx ty tz) + (x: @interp_type RWV tx) (y: @interp_type RWV ty): @interp_type RWV tz := + @interp_binop RWV _ _ _ _ op x y. + End Operations. + End Defaults. - toT := fun x => - if (Nge_dec (N.pred (Npow2 n)) (Z.to_N x)) - then Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x)) - else None; - - fromT := fun x => orElse 0%Z (option_map Z.of_N (option_map value x)); - - eadd := fun x y => omap x (fun X => omap y (fun Y => - rwv_app range_add_valid X Y)); - - esub := fun x y => omap x (fun X => omap y (fun Y => - rwv_app range_sub_valid X Y)); - - emul := fun x y => omap x (fun X => omap y (fun Y => - rwv_app range_mul_valid X Y)); - - eshiftr := fun x y => omap x (fun X => omap y (fun Y => - rwv_app range_shiftr_valid X Y)); - - eand := fun x y => omap x (fun X => omap y (fun Y => - rwv_app range_and_valid X Y)); - - eltb := fun x y => - match (x, y) with - | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) => - N.ltb xv yv - - | _ => false - end; - - eeqb := fun x y => - match (x, y) with - | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) => - andb (andb (N.eqb xlow ylow) (N.eqb xhigh yhigh)) (N.eqb xv yv) - - | _ => false - end; - }. + Section Correctness. + Context {n: nat}. - Definition getRWV {t} T (E: Evaluable T) (e : @expr T T t): @interp_type (option RangeWithValue) t := - interp (@convertExpr T (option RangeWithValue) E RWVEval t e). + Definition W := (word n). + Definition B := (@Bounded n). + Definition R := (option RangeWithValue). - Definition getRanges {t} T (E: Evaluable T) (e : @expr T T t): @interp_type (option (Range N)) t := - typeMap (option_map proj) (getRWV T E e). + Instance RE : Evaluable R := @RWVEvaluable n. + Instance ZE : Evaluable Z := @ZEvaluable n. + Instance WE : Evaluable W := @WordEvaluable n. + Instance BE : Evaluable B := @BoundedEvaluable n. - Fixpoint check' {t} (x: @interp_type (option RangeWithValue) t) := - match t as t' return (interp_type t') -> bool with - | TT => fun x' => - match x' with - | Some _ => true - | None => false - end - | Prod t0 t1 => fun x' => - match x' with - | (x0, x1) => andb (check' x0) (check' x1) - end - end x. + Transparent ZE RE WE BE W B R. - Definition check {t} T (E: Evaluable T) (e : @expr T T t): bool := - check' (getRWV T E e). + Existing Instance ZE. + Existing Instance RE. + Existing Instance WE. + Existing Instance BE. Ltac kill_dec := repeat match goal with @@ -414,68 +215,297 @@ Module LLConversions. | [H : context[Nge_dec ?a ?b] |- _ ] => destruct (Nge_dec a b) end. - Lemma check_spec: forall {t} (E: expr t), - check Z ZEvaluable E = true - -> bcheck (n := n) Z ZEvaluable E = true. - Proof. - intros t E H. - induction E as [tx ty tz op x y z eC IH| t a]. - - - unfold bcheck, getBounds, check, getRWV in *. - apply IH; simpl in *; revert H; clear IH. - repeat rewrite convertArg_interp. - generalize (interp_arg x) as X; intro X; clear x. - generalize (interp_arg y) as Y; intro Y; clear y. - intro H; rewrite <- H; clear H; repeat f_equal. - - induction op; unfold ZEvaluable, BoundedEvaluable, RWVEval, just in *; - simpl in *; kill_dec; simpl in *; try reflexivity; - try rewrite (bapp_value_spec _ _ _ (fun x => Z.of_N (@wordToN n x))); - unfold vapp, rapp, rwv_app, overflows in *; kill_dec; simpl in *; - try reflexivity; try nomega. - - - induction a as [c|v|t0 t1 a0 IHa0 a1 IHa1]; - unfold bcheck, getBounds, check, getRWV in *; simpl in *; unfold just. - - + induction (Nge_dec (N.pred (Npow2 n)) (Z.to_N c)); - simpl in *; [reflexivity|inversion H]. - - + induction (Nge_dec (N.pred (Npow2 n)) (Z.to_N v)); - simpl in *; [reflexivity|inversion H]. - - + apply andb_true_iff; apply andb_true_iff in H; - destruct H as [H0 H1]; split; - [apply IHa0|apply IHa1]; assumption. - Qed. - - Lemma RangeInterp_spec: forall {t} (E: expr t), - check Z ZEvaluable E = true - -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E) = wordInterp (convertZToWord n E). - Proof. - intros. - apply RangeInterp_bounded_spec. - apply check_spec. - assumption. - Qed. - - Lemma getRanges_spec: forall {t} T E (e: @expr T T t), - getRanges T E e = typeMap (t := t) (option_map (toRange (n := n))) (getBounds T E e). - Proof. - intros; induction e as [tx ty tz op x y z eC IH| t a]; - unfold getRanges, getRWV, option_map, toRange, getBounds in *; - simpl in *. - - - rewrite <- IH; clear IH; simpl. - repeat f_equal. - repeat rewrite (convertArg_interp x); generalize (interp_arg x) as X; intro; clear x. - repeat rewrite (convertArg_interp y); generalize (interp_arg y) as Y; intro; clear y. - - (* induction op; - unfold RWVEval, BoundedEvaluable, bapp, rwv_app, - overflows, omap, option_map, just; simpl; - kill_dec; simpl in *. *) - Admitted. - End FastCorrect. + Section BoundsChecking. + Context {T: Type} {E: Evaluable T}. + + Definition boundVarInterp := fun x => bwFromRWV (n := n) (rwv 0%N (Z.to_N x) (Z.to_N x)). + + Definition getBounds {t} (e : @expr T Z t): @interp_type B t := + interp' boundVarInterp (@convertExpr T B _ _ t _ e). + + Fixpoint bcheck' {t} (x: @interp_type B t) := + match t as t' return (interp_type t') -> bool with + | TT => fun x' => + match x' with + | Some _ => true + | None => false + end + | Prod t0 t1 => fun x' => + match x' with + | (x0, x1) => andb (bcheck' x0) (bcheck' x1) + end + end x. + + Definition bcheck {t} (e : expr t): bool := bcheck' (getBounds e). + End BoundsChecking. + + Section UtilityLemmas. + Context {A B} {EA: Evaluable A} {EB: Evaluable B}. + + Lemma convertArg_interp' : forall {t V} f (x: @arg A V t), + (interp_arg' (fun z => toT (fromT (f z))) (@convertArg A B EA EB _ t x)) + = @convertVar A B EA EB t (interp_arg' f x). + Proof. + intros. + induction x as [| |t0 t1 i0 i1]; simpl; [reflexivity|reflexivity|]. + induction EA, EB; simpl; f_equal; assumption. + Qed. + + Lemma convertArg_var: forall {A B EA EB t} V (x: @interp_type A t), + @convertArg A B EA EB V t (uninterp_arg x) = uninterp_arg (var := V) (@convertVar A B EA EB t x). + Proof. + induction t as [|t0 IHt_0 t1 IHt_1]; simpl; intros; [reflexivity|]. + induction x as [a b]; simpl; f_equal; + induction t0 as [|t0a IHt0_0 t0b IHt0_1], + t1 as [|t1a IHt1_0]; simpl in *; + try rewrite IHt_0; + try rewrite IHt_1; + reflexivity. + Qed. + + Lemma ZToBounded_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: @arg Z Z tx) (y: @arg Z Z ty) e, + bcheck (t := tz) (LetBinop op x y e) = true + -> opZ (n := n) op (interp_arg x) (interp_arg y) = + varBoundedToZ (n := n) (opBounded op + (interp_arg' boundVarInterp (convertArg _ x)) + (interp_arg' boundVarInterp (convertArg _ y))). + Proof. + Admitted. + + Lemma ZToWord_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e, + bcheck (t := tz) (LetBinop op x y e) = true + -> opZ (n := n) op (interp_arg x) (interp_arg y) = + varWordToZ (opWord (n := n) op (varZToWord (interp_arg x)) (varZToWord (interp_arg y))). + Proof. + Admitted. + + Lemma roundTrip_0 : @toT Correctness.B BE (@fromT Z ZE 0%Z) <> None. + Proof. + intros; unfold toT, fromT, BE, ZE, BoundedEvaluable, ZEvaluable, bwFromRWV; + kill_dec; simpl; kill_dec; simpl; try abstract (intro Z; inversion Z); + pose proof (Npow2_gt0 n); simpl in *; nomega. + Qed. + + Lemma double_conv_var: forall t x, + @convertVar R Z _ _ t (@convertVar B R _ _ t x) = + @convertVar B Z _ _ t x. + Proof. + intros. + Admitted. + + Lemma double_conv_arg: forall V t a, + @convertArg R B _ _ V t (@convertArg Z R _ _ V t a) = + @convertArg Z B _ _ V t a. + Proof. + intros. + Admitted. + End UtilityLemmas. + + + Section Spec. + Ltac kill_just n := + match goal with + | [|- context[just ?x] ] => + let Hvalue := fresh in let Hvalue' := fresh in + let Hlow := fresh in let Hlow' := fresh in + let Hhigh := fresh in let Hhigh' := fresh in + let Hnone := fresh in let Hnone' := fresh in + + let B := fresh in + + pose proof (just_value_spec (n := n) x) as Hvalue; + pose proof (just_low_spec (n := n) x) as Hlow; + pose proof (just_high_spec (n := n) x) as Hhigh; + pose proof (just_None_spec (n := n) x) as Hnone; + + destruct (just x); + + try pose proof (Hlow _ eq_refl) as Hlow'; + try pose proof (Hvalue _ eq_refl) as Hvalue'; + try pose proof (Hhigh _ eq_refl) as Hhigh'; + try pose proof (Hnone eq_refl) as Hnone'; + + clear Hlow Hhigh Hvalue Hnone + end. + + Lemma RangeInterp_bounded_spec: forall {t} (E: expr t), + bcheck (@convertExpr Z R _ _ _ _ E) = true + -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp (n := n) E) = wordInterp (ZToWord _ E). + Proof. + intros t E S. + unfold zinterp, ZToWord, wordInterp. + + induction E as [tx ty tz op x y z|]; simpl; try reflexivity. + + - repeat rewrite convertArg_var in *. + repeat rewrite convertArg_interp in *. + + rewrite H; clear H; repeat f_equal. + + + pose proof (ZToWord_binop_correct op x y) as C; + unfold opZ, opWord, varWordToZ, varZToWord in C; + simpl in C. + + assert (N.pred (Npow2 n) >= 0)%N. { + apply N.le_ge. + rewrite <- (N.pred_succ 0). + apply N.le_pred_le_succ. + rewrite N.succ_pred; [| apply N.neq_0_lt_0; apply Npow2_gt0]. + apply N.le_succ_l. + apply Npow2_gt0. + } + + admit. (* + induction op; rewrite (C (fun _ => Return (Const 0%Z))); clear C; + unfold bcheck, getBounds, boundedInterp, bwFromRWV in *; simpl in *; + kill_dec; simpl in *; kill_dec; first [reflexivity|nomega]. *) + + + unfold bcheck, getBounds in *. + replace (interp_binop op _ _) + with (varBoundedToZ (n := n) (opBounded op + (interp_arg' boundVarInterp (convertArg _ x)) + (interp_arg' boundVarInterp (convertArg _ y)))). + + * rewrite <- S; f_equal; clear S. + simpl; repeat f_equal. + unfold varBoundedToZ, opBounded. + repeat rewrite convertArg_var. + Arguments convertArg _ _ _ _ _ _ _ : clear implicits. + rewrite double_conv_var. + repeat rewrite double_conv_arg. + reflexivity. + + * pose proof (ZToBounded_binop_correct op x y) as C; + unfold opZ, opWord, varZToBounded, + varBoundedToZ in *; + simpl in C. + + Local Opaque boundVarInterp toT fromT. + + induction op; rewrite (C (fun _ => Return (Const 0%Z))); clear C; try reflexivity; + unfold bcheck, getBounds; simpl; + pose proof roundTrip_0 as H; + induction (toT (fromT _)); first [reflexivity|contradict H; reflexivity]. + + Local Transparent boundVarInterp toT fromT. + + - simpl in S. + induction a as [| |t0 t1 a0 IHa0 a1 IHa1]; simpl in *; try reflexivity. + admit. + + (* + + f_equal. + unfold bcheck, getBounds, boundedInterp in S; simpl in S. + kill_dec; simpl; [reflexivity|simpl in S; inversion S]. + + + f_equal. + unfold bcheck, getBounds, boundedInterp, boundVarInterp in S; simpl in S; + kill_dec; simpl; try reflexivity; try nomega. + inversion S. + admit. + admit. + + + unfold bcheck in S; simpl in S; + apply andb_true_iff in S; destruct S as [S0 S1]; + rewrite IHa0, IHa1; [reflexivity| |]; + unfold bcheck, getBounds; simpl; assumption. *) + Admitted. + End Spec. + + Section RWVSpec. + Definition rangeOf := fun x => + Some (rwv 0%N (Z.to_N x) (Z.to_N x)). + + Definition getRWV {t} (e : @expr R Z t): @interp_type R t := + interp' rangeOf e. + + Definition getRanges {t} (e : @expr R Z t): @interp_type (option (Range N)) t := + typeMap (option_map rwvToRange) (getRWV e). + + Fixpoint check' {t} (x: @interp_type (option RangeWithValue) t) := + match t as t' return (interp_type t') -> bool with + | TT => fun x' => + match omap x' (bwFromRWV (n := n)) with + | Some _ => true + | None => false + end + | Prod t0 t1 => fun x' => + match x' with + | (x0, x1) => andb (check' x0) (check' x1) + end + end x. + + Definition check {t} (e : @expr R Z t): bool := check' (getRWV e). + + Ltac kill_dec := + repeat match goal with + | [|- context[Nge_dec ?a ?b] ] => destruct (Nge_dec a b) + | [H : context[Nge_dec ?a ?b] |- _ ] => destruct (Nge_dec a b) + end. + + Lemma check_spec' : forall {rangeF wordF} (op: @validBinaryWordOp n rangeF wordF) x y, + @convertVar B R _ _ TT ( + omap (interp_arg' boundVarInterp (convertArg TT x)) (fun X => + omap (interp_arg' boundVarInterp (convertArg TT y)) (fun Y => + bapp op X Y))) = + omap (interp_arg' rangeOf x) (fun X => + omap (interp_arg' rangeOf y) (fun Y => + rwv_app (n := n) op X Y)). + Proof. + Admitted. + + Lemma check_spec: forall {t} (E: @expr R Z t), check E = true -> bcheck E = true. + Proof. + intros t E H. + induction E as [tx ty tz op x y z eC IH| t a]. + + - unfold bcheck, getBounds, check, getRWV in *. + + simpl; apply IH; clear IH; rewrite <- H; clear H. + simpl; rewrite convertArg_var; repeat f_equal. + + unfold interp_binop, RE, WE, BE, ZE, + BoundedEvaluable, RWVEvaluable, ZEvaluable, + eadd, emul, esub, eshiftr, eand. + + induction op; rewrite check_spec'; reflexivity. + + - unfold bcheck, getBounds, check, getRWV in *. + + induction a as [a|a|t0 t1 a0 IHa0 a1 IHa1]. + + + induction a as [a|]; [| inversion H]; simpl in *. + + assert (Z : (exists a', bwFromRWV (n := n) a = Some a') + \/ bwFromRWV (n := n) a = None) by ( + destruct (bwFromRWV a); + [left; eexists; reflexivity | right; reflexivity]). + + destruct Z as [aSome|aNone]; [destruct aSome as [a' aSome] |]. + + * rewrite aSome; simpl; rewrite aSome; reflexivity. + * rewrite aNone in H; inversion H. + + + unfold boundVarInterp, rangeOf in *. + simpl in *; kill_dec; try reflexivity; try inversion H. + + + simpl in *; rewrite IHa0, IHa1; simpl; [reflexivity | | ]; + apply andb_true_iff in H; destruct H as [H1 H2]; + assumption. + Qed. + + Lemma RangeInterp_spec: forall {t} (E: expr t), + check (convertExpr E) = true + -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp (n := n) E) + = wordInterp (ZToWord _ E). + Proof. + intros. + apply RangeInterp_bounded_spec. + apply check_spec. + assumption. + Qed. + End RWVSpec. + End Correctness. End LLConversions. Section ConversionTest. @@ -492,22 +522,22 @@ Section ConversionTest. Definition testCase := Eval vm_compute in KeepAddingOne 4000. - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 0 testCase))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 1 testCase))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 10 testCase))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 32 testCase))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 64 testCase))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 128 testCase))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 0 testCase))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 1 testCase))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 10 testCase))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 32 testCase))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 64 testCase))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 128 testCase))). Definition nefarious : Expr (T := Z) TT := fun var => Let (Binop OPadd (Const 10%Z) (Const 20%Z)) (fun y => Binop OPmul (Var y) (Const 0%Z)). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 0 nefarious))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 1 nefarious))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 4 nefarious))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 5 nefarious))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 32 nefarious))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 64 nefarious))). - Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 128 nefarious))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 0 nefarious))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 1 nefarious))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 4 nefarious))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 5 nefarious))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 32 nefarious))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 64 nefarious))). + Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 128 nefarious))). End ConversionTest. diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v index c22709331..0b19b5237 100644 --- a/src/Assembly/Evaluables.v +++ b/src/Assembly/Evaluables.v @@ -7,13 +7,33 @@ Require Import ProofIrrelevance. Import ListNotations. +Section BaseTypes. + Inductive Range T := | range: forall (low high: T), Range T. + + Record RangeWithValue := rwv { + rwv_low: N; + rwv_value: N; + rwv_high: N; + }. + + Record BoundedWord {n} := bounded { + bw_low: N; + bw_value: word n; + bw_high: N; + + ge_low: (bw_low <= wordToN bw_value)%N; + le_high: (wordToN bw_value <= bw_high)%N; + high_bound: (bw_high < Npow2 n)%N; + }. +End BaseTypes. + Section Evaluability. Class Evaluable T := evaluator { ezero: T; (* Conversions *) - toT: Z -> T; - fromT: T -> Z; + toT: option RangeWithValue -> T; + fromT: T -> option RangeWithValue; (* Operations *) eadd: T -> T -> T; @@ -29,12 +49,16 @@ Section Evaluability. End Evaluability. Section Z. + Context {n: nat}. Instance ZEvaluable : Evaluable Z := { ezero := 0%Z; (* Conversions *) - toT := fun x => x; - fromT := fun x => x; + toT := fun x => Z.of_N (orElse 0%N (option_map rwv_value x)); + fromT := fun x => + if (Nge_dec (N.pred (Npow2 n)) (Z.to_N x)) + then Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x)) + else None; (* Operations *) eadd := Z.add; @@ -47,7 +71,6 @@ Section Z. eltb := Z.ltb; eeqb := Z.eqb; }. - End Z. Section Word. @@ -57,8 +80,8 @@ Section Word. ezero := wzero n; (* Conversions *) - toT := fun x => @NToWord n (Z.to_N x); - fromT := fun x => Z.of_N (@wordToN n x); + toT := fun x => @NToWord n (orElse 0%N (option_map rwv_value x)); + fromT := fun x => let v := @wordToN n x in (Some (rwv v v v)); (* Operations *) eadd := @wplus n; @@ -76,8 +99,6 @@ End Word. Section RangeUpdate. Context {n: nat}. - Inductive Range T := | range: forall (low high: T), Range T. - Definition validBinaryWordOp (rangeF: Range N -> Range N -> option (Range N)) (wordF: word n -> word n -> word n): Prop := @@ -464,19 +485,12 @@ End RangeUpdate. Section BoundedWord. Context {n: nat}. - Record BoundedWord := bounded { - low: N; - value: word n; - high: N; - - ge_low: (low <= wordToN value)%N; - le_high: (wordToN value <= high)%N; - high_bound: (high < Npow2 n)%N; - }. + Definition BW := @BoundedWord n. + Transparent BW. Definition bapp {rangeF wordF} (op: @validBinaryWordOp n rangeF wordF) - (X Y: BoundedWord): option BoundedWord. + (X Y: BW): option BW. refine ( let op' := op _ _ _ _ _ _ @@ -484,12 +498,12 @@ Section BoundedWord. (ge_low Y) (le_high Y) (high_bound Y) in let result := rangeF - (range N (low X) (high X)) - (range N (low Y) (high Y)) in + (range N (bw_low X) (bw_high X)) + (range N (bw_low Y) (bw_high Y)) in match result as r' return result = r' -> _ with | Some (range low high) => fun e => - Some (bounded low (wordF (value X) (value Y)) high _ _ _) + Some (@bounded n low (wordF (bw_value X) (bw_value Y)) high _ _ _) | None => fun _ => None end eq_refl); abstract ( @@ -510,26 +524,42 @@ Section BoundedWord. (X Y: word n): option (word n) := Some (wordF X Y). - Lemma bapp_value_spec: forall {T rangeF wordF} - (op: @validBinaryWordOp n rangeF wordF) - (b0 b1: BoundedWord) (f: word n -> T), - option_map (fun x => f (value x)) (bapp op b0 b1) - = option_map (fun x => f x) ( - omap (rapp op (range N (low b0) (high b0)) - (range N (low b1) (high b1))) (fun _ => - vapp op (value b0) (value b1))). - Proof. - Admitted. + Definition bwToRWV (w: BW): RangeWithValue := + rwv (bw_low w) (wordToN (bw_value w)) (bw_high w). + + Definition bwFromRWV (r: RangeWithValue): option BW. + refine + match r with + | rwv l v h => + match (Nge_dec h v, Nge_dec v l, Nge_dec (N.pred (Npow2 n)) h) with + | (left p0, left p1, left p2) => Some (@bounded n l (NToWord n l) h _ _ _) + | _ => None + end + end; try rewrite wordToN_NToWord; - Definition toRange (w: BoundedWord): Range N := - range N (low w) (high w). + assert (N.succ h <= Npow2 n)%N by abstract ( + apply N.ge_le in p2; + rewrite <- (N.pred_succ h) in p2; + apply -> N.le_pred_le_succ in p2; + rewrite N.succ_pred in p2; [assumption |]; + apply N.neq_0_lt_0; + apply Npow2_gt0); + + try abstract (apply (N.lt_le_trans _ (N.succ h) _); + [nomega|assumption]); + + [reflexivity| etransitivity; apply N.ge_le; eassumption]. + Defined. - Definition fromRange (r: Range N): option (BoundedWord). + Definition bwToRange (w: BW): Range N := + range N (bw_low w) (bw_high w). + + Definition bwFromRange (r: Range N): option BW. refine match r with | range l h => match (Nge_dec h l, Nge_dec (N.pred (Npow2 n)) h) with - | (left p0, left p1) => Some (bounded l (NToWord n l) h _ _ _) + | (left p0, left p1) => Some (@bounded n l (NToWord n l) h _ _ _) | _ => None end end; try rewrite wordToN_NToWord; @@ -546,13 +576,12 @@ Section BoundedWord. [nomega|assumption]); [reflexivity|apply N.ge_le; assumption]. - Defined. - Definition just (x: N): option (BoundedWord). + Definition just (x: N): option BW. refine match Nge_dec (N.pred (Npow2 n)) x with - | left p => Some (bounded x (NToWord n x) x _ _ _) + | left p => Some (@bounded n x (NToWord n x) x _ _ _) | right _ => None end; try rewrite wordToN_NToWord; try reflexivity; @@ -580,29 +609,29 @@ Section BoundedWord. apply N.le_ge; apply N.succ_le_mono; assumption. Qed. - Lemma just_value_spec: forall x b, just x = Some b -> value b = NToWord n x. + Lemma just_value_spec: forall x b, just x = Some b -> bw_value b = NToWord n x. Proof. intros x b H; destruct b; unfold just in *; destruct (Nge_dec (N.pred (Npow2 n)) x); simpl in *; inversion H; subst; reflexivity. Qed. - Lemma just_low_spec: forall x b, just x = Some b -> low b = x. + Lemma just_low_spec: forall x b, just x = Some b -> bw_low b = x. Proof. intros x b H; destruct b; unfold just in *; destruct (Nge_dec (N.pred (Npow2 n)) x); simpl in *; inversion H; subst; reflexivity. Qed. - Lemma just_high_spec: forall x b, just x = Some b -> high b = x. + Lemma just_high_spec: forall x b, just x = Some b -> bw_high b = x. Proof. intros x b H; destruct b; unfold just in *; destruct (Nge_dec (N.pred (Npow2 n)) x); simpl in *; inversion H; subst; reflexivity. Qed. - Definition any: BoundedWord. - refine (bounded 0%N (wzero n) (N.pred (Npow2 n)) _ _ _); + Definition any: BW. + refine (@bounded n 0%N (wzero n) (N.pred (Npow2 n)) _ _ _); try rewrite wordToN_zero; try reflexivity; try abstract (apply N.lt_le_pred; apply Npow2_gt0). @@ -610,17 +639,11 @@ Section BoundedWord. apply N.lt_pred_l; apply N.neq_0_lt_0; apply Npow2_gt0. Defined. - Definition orElse {T} (d: T) (o: option T): T := - match o with - | Some v => v - | None => d - end. - - Instance BoundedEvaluable : Evaluable (option BoundedWord) := { + Instance BoundedEvaluable : Evaluable (option BW) := { ezero := Some any; - toT := fun x => just (Z.to_N x); - fromT := fun x => orElse 0%Z (option_map (fun x' => Z.of_N (wordToN (value x'))) x); + toT := fun x => omap x bwFromRWV; + fromT := option_map bwToRWV; eadd := fun x y => omap x (fun X => omap y (fun Y => bapp range_add_valid X Y)); esub := fun x y => omap x (fun X => omap y (fun Y => bapp range_sub_valid X Y)); @@ -630,11 +653,82 @@ Section BoundedWord. eltb := fun x y => orElse false (omap x (fun X => omap y (fun Y => - Some (N.ltb (high X) (high Y))))); + Some (N.ltb (wordToN (bw_value X)) (wordToN (bw_value Y)))))); eeqb := fun x y => orElse false (omap x (fun X => omap y (fun Y => - Some (andb (N.eqb (low X) (low Y)) (N.eqb (high X) (high Y)))))) + Some (N.eqb (wordToN (bw_value X)) (wordToN (bw_value Y)))))) }. +End BoundedWord. -End BoundedWord. \ No newline at end of file +Section RangeWithValue. + Context {n: nat}. + + Definition rwv_app {rangeF wordF} + (op: @validBinaryWordOp n rangeF wordF) + (X Y: RangeWithValue): option (RangeWithValue) := + omap (rangeF (range N (rwv_low X) (rwv_high X)) + (range N (rwv_low Y) (rwv_high Y))) (fun r' => + match r' with + | range l h => Some ( + rwv l (wordToN (wordF (NToWord n (rwv_value X)) + (NToWord n (rwv_value Y)))) h) + end). + + Lemma rwv_None_spec : forall {rangeF wordF} + (op: @validBinaryWordOp n rangeF wordF) + (X Y: RangeWithValue), + omap (rwv_app op X Y) (bwFromRWV (n := n)) <> None. + Proof. + Admitted. + + Definition rwvToRange (x: RangeWithValue): Range N := + range N (rwv_low x) (rwv_high x). + + Definition rwvFromRange (x: Range N): RangeWithValue := + match x with + | range l h => rwv l h h + end. + + Lemma bwToFromRWV: forall x, option_map (@bwToRWV n) (omap x bwFromRWV) = x. + Proof. + Admitted. + + Instance RWVEvaluable : Evaluable (option RangeWithValue) := { + ezero := None; + + toT := fun x => x; + fromT := fun x => omap (omap x (bwFromRWV (n := n))) (fun _ => x); + + eadd := fun x y => omap x (fun X => omap y (fun Y => + rwv_app range_add_valid X Y)); + + esub := fun x y => omap x (fun X => omap y (fun Y => + rwv_app range_sub_valid X Y)); + + emul := fun x y => omap x (fun X => omap y (fun Y => + rwv_app range_mul_valid X Y)); + + eshiftr := fun x y => omap x (fun X => omap y (fun Y => + rwv_app range_shiftr_valid X Y)); + + eand := fun x y => omap x (fun X => omap y (fun Y => + rwv_app range_and_valid X Y)); + + eltb := fun x y => + match (x, y) with + | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) => + N.ltb xv yv + + | _ => false + end; + + eeqb := fun x y => + match (x, y) with + | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) => + andb (andb (N.eqb xlow ylow) (N.eqb xhigh yhigh)) (N.eqb xv yv) + + | _ => false + end; + }. +End RangeWithValue. \ No newline at end of file diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 80d9044c4..a21b54cf0 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -9,6 +9,9 @@ Module GF25519. Definition bits: nat := 64. Definition width: Width bits := W64. + Instance ZE : Evaluable Z := @ZEvaluable bits. + Existing Instance ZE. + Fixpoint makeBoundList {n} k (b: @BoundedWord n) := match k with | O => nil @@ -17,9 +20,9 @@ Module GF25519. Section DefaultBounds. Import ListNotations. - Local Notation rr exp := (range N 0%N (2^exp + 2^exp/10)%N). + Local Notation rr exp := (2^exp + 2^exp/10)%Z. - Definition feBound: list (Range N) := + Definition feBound: list Z := [rr 26; rr 27; rr 26; rr 27; rr 26; rr 27; rr 26; rr 27; rr 26; rr 27]. End DefaultBounds. @@ -45,8 +48,7 @@ Module GF25519. Eval cbv beta delta [fe25519 add mul sub Let_In] in add. Definition ge25519_add' (P Q: @interp_type Z FE) : - { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_add_expr P Q }. + { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_add_expr P Q }. Proof. vm_compute in P, Q; repeat match goal with @@ -63,8 +65,7 @@ Module GF25519. let R := HL.rhs_of_goal in let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); - [reflexivity|]. + transitivity (HL.interp (t := ResultType) X); [reflexivity|]. cbv iota beta delta [ interp_type interp_binop HL.interp @@ -75,124 +76,10 @@ Module GF25519. Definition ge25519_add (P Q: @interp_type Z ResultType) := proj1_sig (ge25519_add' P Q). - Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := + Definition hlProg: NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := liftFE (fun p => (liftFE (fun q => ge25519_add p q))). - - Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t; - [ refine LL.uninterp_arg | refine LL.interp_arg ]. - Defined. - - Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - Eval vm_compute in hlProg'. End AddExpr. - Module SubExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. - - Definition ge25519_sub_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in sub. - - Definition ge25519_sub' (P Q: @interp_type Z FE) : - { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_sub_expr P Q }. - Proof. - vm_compute in P, Q; repeat - match goal with - | [x:?T |- _] => - lazymatch T with - | Z => fail - | prod _ _ => destruct x - | _ => clear x - end - end. - - eexists. - cbv beta delta [ge25519_sub_expr]. - - let R := HL.rhs_of_goal in - let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); - [reflexivity|]. - - cbv iota beta delta [ - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - reflexivity. - Defined. - - Definition ge25519_sub (P Q: @interp_type Z ResultType) := - proj1_sig (ge25519_sub' P Q). - - Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := - liftFE (fun p => (liftFE (fun q => ge25519_sub p q))). - - Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t; - [ refine LL.uninterp_arg | refine LL.interp_arg ]. - Defined. - - Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - Eval vm_compute in hlProg'. - End SubExpr. - - Module MulExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. - - Definition ge25519_mul_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in mul. - - Definition ge25519_mul' (P Q: @interp_type Z FE) : - { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_mul_expr P Q }. - Proof. - vm_compute in P, Q; repeat - match goal with - | [x:?T |- _] => - lazymatch T with - | Z => fail - | prod _ _ => destruct x - | _ => clear x - end - end. - - eexists. - cbv beta delta [ge25519_mul_expr]. - - let R := HL.rhs_of_goal in - let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); - [reflexivity|]. - - cbv iota beta delta [ - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - reflexivity. - Defined. - - Definition ge25519_mul (P Q: @interp_type Z ResultType) := - proj1_sig (ge25519_mul' P Q). - - Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := - liftFE (fun p => (liftFE (fun q => ge25519_mul p q))). - - Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t; - [ refine LL.uninterp_arg | refine LL.interp_arg ]. - Defined. - - Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - Eval vm_compute in hlProg'. - End MulExpr. - Module OppExpr <: Expression. Definition bits: nat := bits. Definition inputs: nat := 10. @@ -205,7 +92,7 @@ Module GF25519. Definition ge25519_opp' (P: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_opp_expr P }. + | HL.interp (E := @ZEvaluable bits) (t := FE) r = ge25519_opp_expr P }. Proof. vm_compute in P; repeat match goal with @@ -222,7 +109,7 @@ Module GF25519. let R := HL.rhs_of_goal in let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); + transitivity (HL.interp (E := @ZEvaluable bits) (t := ResultType) X); [reflexivity|]. cbv iota beta delta [ @@ -234,25 +121,41 @@ Module GF25519. Definition ge25519_opp (P: @interp_type Z ResultType) := proj1_sig (ge25519_opp' P). - Definition hlProg'': NAry 10 Z (@HL.expr Z (@interp_type Z) ResultType) := + Definition hlProg: NAry 10 Z (@HL.expr Z (@interp_type Z) ResultType) := liftFE (fun p => ge25519_opp p). - - Definition hlProg': NAry 10 Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t; - [ refine LL.uninterp_arg | refine LL.interp_arg ]. - Defined. - - Definition hlProg: NAry 10 Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - Eval vm_compute in hlProg'. End OppExpr. Module Add := Pipeline AddExpr. - Module Sub := Pipeline SubExpr. - Module Mul := Pipeline MulExpr. Module Opp := Pipeline OppExpr. + + Section Operations. + Definition wfe: Type := @interp_type (word bits) FE. + + Definition ExprBinOp : Type := NAry 20 Z (@CompileLL.WExpr bits FE). + Definition ExprUnOp : Type := NAry 10 Z (@CompileLL.WExpr bits FE). + + Existing Instance WordEvaluable. + + Definition interp_bexpr (op: ExprBinOp) (x y: tuple (word bits) 10): tuple (word bits) 10 := + let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in + let '(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9) := y in + let op' := NArgMap (fun v => Z.of_N (@wordToN bits v)) op in + let z := LL.interp (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in + z. + + Definition interp_uexpr (op: ExprUnOp) (x: tuple (word bits) 10): tuple (word bits) 10 := + let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in + let op' := NArgMap (fun v => Z.of_N (@wordToN bits v)) op in + let z := LL.interp (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) in + z. + + Definition radd : ExprBinOp := Add.wordProg. + Definition ropp : ExprUnOp := Opp.wordProg. + End Operations. End GF25519. Extraction "GF25519Add" GF25519.Add. Extraction "GF25519Sub" GF25519.Sub. Extraction "GF25519Mul" GF25519.Mul. -Extraction "GF25519Opp" GF25519.Opp. \ No newline at end of file +Extraction "GF25519Opp" GF25519.Opp. + diff --git a/src/Assembly/HL.v b/src/Assembly/HL.v index 264cd0351..14ca2edca 100644 --- a/src/Assembly/HL.v +++ b/src/Assembly/HL.v @@ -1,4 +1,5 @@ Require Import Crypto.Assembly.PhoasCommon. +Require Import Coq.setoid_ring.InitialRing. Module HL. Section Language. @@ -41,9 +42,9 @@ Module HL. refine (IHt1 x1, IHt2 x2). Defined. - Definition zinterp {t} E := @interp Z ZEvaluable t E. + Definition zinterp {n t} E := @interp Z (@ZEvaluable n) t E. - Definition ZInterp {t} E := @Interp Z ZEvaluable t E. + Definition ZInterp {n t} E := @Interp Z (@ZEvaluable n) t E. Definition wordInterp {n t} E := @interp (word n) (@WordEvaluable n) t E. @@ -55,7 +56,7 @@ Module HL. MatchPair (Var p) (fun x y => Binop OPadd (Var x) (Var y)))))%Z. - Example interp_example_Expr : ZInterp example_Expr = 28%Z. + Example interp_example_Expr : ZInterp (n := 16) example_Expr = 28%Z. Proof. reflexivity. Qed. (* Reification assumes the argument type is Z *) @@ -114,10 +115,15 @@ Module HL. | ?x => lazymatch goal with | _:reify_var_for_in_is x ?t ?v |- _ => constr:(@Var Z var t v) - | _ => (* let t := match type of x with ?t => reify_type t end in *) - constr:(@Const Z var x) + | _ => + let x' := eval cbv in x in + match isZcst x' with + | true => constr:(@Const Z var x) + | false => constr:(@Var Z var TT x) + end end end. + Hint Extern 0 (reify ?var ?e) => (let e := reify var e in eexact e) : typeclass_instances. Ltac Reify e := @@ -130,7 +136,7 @@ Module HL. Goal forall (x : Z) (v : zinterp_type TT) (_:reify_var_for_in_is x TT v), reify(T:=Z) zinterp_type ((fun x => x+x) x)%Z. intros. - let A := (reify zinterp_type (x + x)%Z) in pose A. + let A := (reify zinterp_type (x + x + 1)%Z) in pose A. Abort. Goal False. @@ -140,18 +146,18 @@ Module HL. Ltac lhs_of_goal := match goal with |- ?R ?LHS ?RHS => constr:(LHS) end. Ltac rhs_of_goal := match goal with |- ?R ?LHS ?RHS => constr:(RHS) end. - Ltac Reify_rhs := + Ltac Reify_rhs n := let rhs := rhs_of_goal in let RHS := Reify rhs in - transitivity (ZInterp RHS); + transitivity (ZInterp (n := n) RHS); [|cbv iota beta delta [ZInterp Interp interp_type interp_binop interp]; reflexivity]. Goal (0 = let x := 1+2 in x*3)%Z. - Reify_rhs. + Reify_rhs 32. Abort. Goal (0 = let x := 1 in let y := 2 in x * y)%Z. - Reify_rhs. + Reify_rhs 32. Abort. Section wf. diff --git a/src/Assembly/LL.v b/src/Assembly/LL.v index 92f07832f..e08b752fe 100644 --- a/src/Assembly/LL.v +++ b/src/Assembly/LL.v @@ -24,6 +24,15 @@ Module LL. | Return : forall {t}, arg t -> expr t. End expr. + Definition Expr t := forall var, @expr var t. + + Fixpoint interp_arg' {V t} (f: V -> T) (e: arg t) : interp_type t := + match e with + | Pair _ _ x y => (interp_arg' f x, interp_arg' f y) + | Const x => x + | Var x => f x + end. + Fixpoint interp_arg {t} (e: arg t) : interp_type t := match e with | Pair _ _ x y => (interp_arg x, interp_arg y) @@ -31,6 +40,12 @@ Module LL. | Var x => x end. + Lemma interp_arg_spec: forall {t} (x: arg t), interp_arg x = interp_arg' id x. + Proof. + intros; induction x; unfold id in *; simpl; repeat f_equal; + first [reflexivity| assumption]. + Qed. + Fixpoint uninterp_arg {var t} (x: interp_type t) : @arg var t := match t as t' return interp_type t' -> arg t' with | Prod t0 t1 => fun x' => @@ -40,16 +55,41 @@ Module LL. | TT => Const end x. + Fixpoint uninterp_arg_as_var {var t} (x: @interp_type var t) : @arg var t := + match t as t' return @interp_type var t' -> @arg var t' with + | Prod t0 t1 => fun x' => + match x' with + | (x0, x1) => Pair (uninterp_arg_as_var x0) (uninterp_arg_as_var x1) + end + | TT => Var + end x. + + Fixpoint interp' {V t} (f: V -> T) (e:expr t) : interp_type t := + match e with + | LetBinop _ _ _ op a b _ eC => + let x := interp_binop op (interp_arg' f a) (interp_arg' f b) in interp' f (eC (uninterp_arg x)) + | Return _ a => interp_arg' f a + end. + Fixpoint interp {t} (e:expr t) : interp_type t := match e with | LetBinop _ _ _ op a b _ eC => let x := interp_binop op (interp_arg a) (interp_arg b) in interp (eC (uninterp_arg x)) | Return _ a => interp_arg a end. + + Lemma interp_spec: forall {t} (e: expr t), interp e = interp' id e. + Proof. + intros; induction e; unfold id in *; simpl; repeat f_equal; + try rewrite H; simpl; repeat f_equal; + rewrite interp_arg_spec; repeat f_equal. + Qed. End Language. + Transparent interp interp_arg. + Example example_expr : - (@interp Z ZEvaluable _ + (@interp Z (ZEvaluable (n := 32)) _ (LetBinop OPadd (Const 7%Z) (Const 8%Z) (fun v => Return v)) = 15)%Z. Proof. reflexivity. Qed. @@ -112,7 +152,8 @@ Module LL. Proof. induction t as [|i0 v0 i1 v1]; simpl; intros; try reflexivity. break_match; subst; simpl. - rewrite v0, v1; reflexivity. + unfold interp_arg in *. + cbn; rewrite v0, v1; reflexivity. Qed. Lemma interp_under_lets {T} {_: Evaluable T} {t: type} {tC: type} diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index e7fc23e0a..31988ab10 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -21,19 +21,34 @@ Module Type Expression. Parameter width: Width bits. Parameter inputs: nat. Parameter ResultType: type. - Parameter hlProg: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType). - Parameter inputBounds: list (Range N). + Parameter hlProg: NAry inputs Z (@HL.expr Z (@interp_type Z) ResultType). + Parameter inputBounds: list Z. End Expression. Module Pipeline (Input: Expression). Export Input. + Module Util. + Fixpoint applyProgOn {A B k} ins (f: NAry k (option A) B): B := + match k as k' return NAry k' (option A) B -> B with + | O => id + | S m => fun f' => + match ins with + | cons x xs => @applyProgOn A B m xs (f' x) + | nil => @applyProgOn A B m nil (f' None) + end + end f. + End Util. + + Definition hlProg': NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType) := + liftN (HLConversions.mapVar (fun t => @LL.uninterp_arg_as_var _ _ t) + (fun t => @LL.interp_arg _ t)) hlProg. + Definition llProg: NAry inputs Z (@LL.expr Z Z ResultType) := - liftN CompileHL.compile hlProg. + liftN CompileHL.compile hlProg'. - Definition wordProg: NAry inputs (@CompileLL.WArg bits TT) (@LL.expr _ _ ResultType) := - NArgMap (fun x => Z.of_N (wordToN (LL.interp_arg (t := TT) x))) ( - liftN (LLConversions.convertZToWord bits) llProg). + Definition wordProg: NAry inputs Z (@CompileLL.WExpr bits ResultType) := + liftN (LLConversions.ZToWord (n := bits) Z) llProg. Definition qhasmProg := CompileLL.compile (w := width) wordProg. @@ -47,28 +62,22 @@ Module Pipeline (Input: Expression). Definition RWV: Type := option RangeWithValue. - Definition rwvProg: NAry inputs RWV (@LL.expr RWV RWV ResultType) := - NArgMap (fun x => orElse 0%Z (option_map (fun v => Z.of_N (value v)) x) ) ( - liftN (@convertExpr Z RWV ZEvaluable (RWVEval (n := bits)) _) llProg). + Instance RWVEvaluable : Evaluable RWV := @RWVEvaluable bits. + + Existing Instance RWVEvaluable. - Fixpoint applyProgOn {A B k} ins (f: NAry k (option A) B): B := - match k as k' return NAry k' (option A) B -> B with - | O => id - | S m => fun f' => - match ins with - | cons x xs => @applyProgOn A B m xs (f' x) - | nil => @applyProgOn A B m nil (f' None) - end - end f. + Definition rwvProg: @LL.expr RWV Z ResultType := + Util.applyProgOn (map (@Some _) inputBounds) ( + NArgMap (orElse 0%Z) ( + liftN (@convertExpr Z RWV (@ZEvaluable bits) _ _ _) + llProg)). Definition outputBounds := - applyProgOn (map (@Some _) (map from_range inputBounds)) ( - liftN (fun e => typeMap (option_map proj) (@LL.interp RWV (@RWVEval bits) _ e)) - rwvProg). + typeMap (option_map rwvToRange) ( + LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x))) ( + rwvProg)). - Definition valid := - applyProgOn (map (@Some _) (map from_range inputBounds)) ( - liftN (@check bits _ RWV (@RWVEval bits)) rwvProg). + Definition valid := check (n := bits) rwvProg. End Pipeline. Module SimpleExample. @@ -80,10 +89,10 @@ Module SimpleExample. Definition inputs: nat := 1. Definition ResultType := TT. - Definition hlProg: NAry 1 Z (@HL.expr Z (@LL.arg Z Z) TT) := - Eval vm_compute in (fun x => HL.Binop OPadd (HL.Const x) (HL.Const 5%Z)). + Definition hlProg: NAry 1 Z (@HL.expr Z (@interp_type Z) TT) := + Eval vm_compute in (fun x => HL.Binop OPadd (HL.Var x) (HL.Const 5%Z)). - Definition inputBounds: list (Range N) := [ range N 0%N (Npow2 31) ]. + Definition inputBounds: list Z := [ (2^30)%Z ]. End SimpleExpression. Module SimplePipeline := Pipeline SimpleExpression. diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v index 79591d40d..b7dd90da6 100644 --- a/src/Assembly/QhasmUtil.v +++ b/src/Assembly/QhasmUtil.v @@ -80,6 +80,12 @@ Section Util. end. Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity). + + Definition orElse {T} (d: T) (o: option T): T := + match o with + | Some v => v + | None => d + end. End Util. Close Scope nword_scope. \ No newline at end of file -- cgit v1.2.3