From ad5c28e00ca3fb89508138354ddaf2f5ba79bd0b Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Fri, 14 Oct 2016 15:51:04 -0700 Subject: Making sub bounds actually tight --- src/Assembly/Compile.v | 2 +- src/Assembly/Conversions.v | 1 - src/Assembly/Evaluables.v | 175 +++++++-------------------------------------- src/Assembly/GF25519.v | 62 ++++++++-------- src/Assembly/WordizeUtil.v | 51 +++++++++++++ 5 files changed, 111 insertions(+), 180 deletions(-) (limited to 'src/Assembly') diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v index d73ed8a07..53612cfbb 100644 --- a/src/Assembly/Compile.v +++ b/src/Assembly/Compile.v @@ -245,7 +245,7 @@ Module CompileLL. omap (exprF (S (S nextRegName)) (eC var)) (fun out => omap (argToTT var) (fun var' => - update (reg w (S nextRegName)) var' op' x' y' out)))))) + update (reg w nextRegName) var' op' x' y' out)))))) | Return _ a => get _ a end. End ExprF. diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v index bb2f1e6fa..705a49a5b 100644 --- a/src/Assembly/Conversions.v +++ b/src/Assembly/Conversions.v @@ -340,7 +340,6 @@ Module LLConversions. admit. - admit. - simpl; unfold getUpperBoundOpt. repeat rewrite convertArg_interp in H. diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v index 7b6e4a264..30d1029a3 100644 --- a/src/Assembly/Evaluables.v +++ b/src/Assembly/Evaluables.v @@ -104,7 +104,7 @@ Section RangeUpdate. induction (Npow2 n0); simpl; reflexivity. Qed. - Lemma bWSub_lem0: forall (x0 x1: word n) (low0 high1: N), + Lemma bWSub_lem: forall (x0 x1: word n) (low0 high1: N), (low0 <= wordToN x0)%N -> (wordToN x1 <= high1)%N -> (low0 - high1 <= & (x0 ^- x1))%N. Proof. @@ -177,138 +177,7 @@ Section RangeUpdate. 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) <= 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)). - - - 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; [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. - - + transitivity (high0 + (wordToN (wneg x1)))%N. - - * apply N.add_le_mono_r; 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. - - - 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. - - + 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. + Qed. End BoundedSub. Section LandOnes. @@ -391,20 +260,14 @@ Section RangeUpdate. then Some (range N (low0 - high1)%N (if (Nge_dec high0 (Npow2 n)) then N.pred (Npow2 n) else if (Nge_dec high1 (Npow2 n)) then N.pred (Npow2 n) else - if (Nge_dec (high0 + Npow2 n - low1) (Npow2 n)) - then N.pred (Npow2 n) - else high0 + Npow2 n - low1)%N) + high0 - low1)%N) else None end) (@wminus n). Proof. unfold validBinaryWordOp; intros. - destruct (Nge_dec high0 (Npow2 n)), - (Nge_dec high1 (Npow2 n)), - (Nge_dec low0 high1), - (Nge_dec (high0 + Npow2 n - low1) (Npow2 n)); - repeat split; + Ltac kill_preds := repeat match goal with | [|- (N.pred _ < _)%N] => rewrite <- (N.pred_succ (Npow2 n)); @@ -412,13 +275,31 @@ Section RangeUpdate. rewrite N.pred_succ; [ apply N.lt_succ_diag_r | apply N.neq_0_lt_0; apply Npow2_gt0] - | [|- (wordToN _ <= N.pred _)%N] => apply N.lt_le_pred + end. + + destruct (Nge_dec high0 (Npow2 n)), + (Nge_dec high1 (Npow2 n)), + (Nge_dec low0 high1); + repeat split; kill_preds; + repeat match goal with | [|- (wordToN _ < Npow2 _)%N] => apply word_size_bound - | [|- (_ - ?x <= wordToN _)%N] => apply bWSub_lem0 - | [|- (wordToN _ <= ?x + _ - _)%N] => apply bWSub_lem1 + | [|- (?x - _ < Npow2)%N] => transitivity x; [nomega|] + | [|- (_ - ?x <= wordToN _)%N] => apply bWSub_lem + | [|- (wordToN _ <= _ - _)%N] => eapply wordize_sub | [|- (0 <= _)%N] => apply N_ge_0 - end; try assumption. + end; try eassumption. + + - apply N.le_ge. + transitivity high1; [assumption|]. + transitivity low0; [|assumption]. + apply N.ge_le; assumption. + + - apply (N.le_lt_trans _ high0 _); [|assumption]. + replace high0 with (high0 - 0)%N by nomega. + replace' (high0 - 0)%N with high0 at 1 by nomega. + apply N.sub_le_mono_l. + apply N.ge_le; nomega. Qed. Lemma range_mul_valid : @@ -534,9 +415,7 @@ Section RangeUpdate. match (range0, range1) with | (range low0 high0, range low1 high1) => let upper := (N.pred (Npow2 (min (N.to_nat (getBits high0)) (N.to_nat (getBits high1)))))%N in - Some (range N 0%N ( - if (Nge_dec upper (Npow2 n)) - then (N.pred (Npow2 n)) else upper)) + Some (range N 0%N (if (Nge_dec upper (Npow2 n)) then (N.pred (Npow2 n)) else upper)) end) (@wand n). Proof. diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 0ec5f508c..081ddc008 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -6,11 +6,23 @@ Require Import Crypto.Specific.GF25519. Require Import Crypto.Util.Tuple. Module GF25519. - Definition q : Z := (2 ^ 255 - 19)%Z. - Definition d : F q := (F.opp (F.of_Z q 121665%Z) / (F.of_Z q 121666%Z))%F. + Definition bits: nat := 32. + Definition width: Width bits := W32. - Definition twice_d' := Eval cbv [length params25519 ModularBaseSystemOpt.limb_widths_from_len ModularBaseSystem.encode ModularBaseSystemList.encode PseudoMersenneBaseParams.limb_widths] in ModularBaseSystem.encode(modulus:=q) (d + d)%F. - Definition twice_d : fe25519 := Eval vm_compute in twice_d'. + Fixpoint makeBoundList {n} k (b: @WordRangeOpt n) := + match k with + | O => nil + | S k' => cons b (makeBoundList k' b) + end. + + Section DefaultBounds. + Import ListNotations. + Local Notation rr exp := (makeRange 0 (2^exp + 2^exp/10)%Z). + + Definition feBound: list (@WordRangeOpt bits) := + [rr 26; rr 27; rr 26; rr 27; rr 26; + rr 27; rr 26; rr 27; rr 26; rr 27]. + End DefaultBounds. Definition FE: type. Proof. @@ -22,22 +34,15 @@ Module GF25519. Definition liftFE {T} (F: @interp_type Z FE -> T) := fun (a b c d e f g h i j: Z) => F (a, b, c, d, e, f, g, h, i, j). - Fixpoint makeBoundList {n} k (b: @WordRangeOpt n) := - match k with - | O => nil - | S k' => cons b (makeBoundList k' b) - end. - Module AddExpr <: Expression. - Definition bits: nat := 64. + Definition bits: nat := bits. Definition inputs: nat := 20. - Definition width: Width bits := W64. + Definition width: Width bits := width. Definition ResultType := FE. - Definition inputUpperBounds: list (@WordRangeOpt bits) := - makeBoundList 20 (makeRange 0 (Z.of_N (Npow2 28))). + Definition inputUpperBounds: list (@WordRangeOpt bits) := feBound ++ feBound. Definition ge25519_add_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In twice_d] in add. + 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 @@ -83,15 +88,14 @@ Module GF25519. End AddExpr. Module SubExpr <: Expression. - Definition bits: nat := 64. + Definition bits: nat := bits. Definition inputs: nat := 20. - Definition width: Width bits := W64. + Definition width: Width bits := width. Definition ResultType := FE. - Definition inputUpperBounds: list (@WordRangeOpt bits) := - makeBoundList 20 (makeRange 0 (Z.of_N (Npow2 28))). + Definition inputUpperBounds: list (@WordRangeOpt bits) := feBound ++ feBound. Definition ge25519_sub_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In twice_d] in sub. + 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 @@ -137,15 +141,14 @@ Module GF25519. End SubExpr. Module MulExpr <: Expression. - Definition bits: nat := 64. + Definition bits: nat := bits. Definition inputs: nat := 20. - Definition width: Width bits := W64. + Definition width: Width bits := width. Definition ResultType := FE. - Definition inputUpperBounds: list (@WordRangeOpt bits) := - makeBoundList 20 (makeRange 0 (Z.of_N (Npow2 28))). + Definition inputUpperBounds: list (@WordRangeOpt bits) := feBound ++ feBound. Definition ge25519_mul_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In twice_d] in mul. + 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 @@ -191,15 +194,14 @@ Module GF25519. End MulExpr. Module OppExpr <: Expression. - Definition bits: nat := 64. + Definition bits: nat := bits. Definition inputs: nat := 10. - Definition width: Width bits := W64. + Definition width: Width bits := width. Definition ResultType := FE. - Definition inputUpperBounds: list (@WordRangeOpt bits) := - makeBoundList 10 (makeRange 0 (Z.of_N (Npow2 28))). + Definition inputUpperBounds: list (@WordRangeOpt bits) := feBound. Definition ge25519_opp_expr := - Eval cbv beta delta [fe25519 add mul sub opp Let_In twice_d] in opp. + Eval cbv beta delta [fe25519 add mul sub opp Let_In] in opp. Definition ge25519_opp' (P: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE diff --git a/src/Assembly/WordizeUtil.v b/src/Assembly/WordizeUtil.v index d0b563368..d4a9409e2 100644 --- a/src/Assembly/WordizeUtil.v +++ b/src/Assembly/WordizeUtil.v @@ -806,6 +806,57 @@ Section TopLevel. apply wordize_plus; assumption. Qed. + Lemma wordize_sub: forall {n} (x y: word n) low0 high0 low1 high1, + (low0 <= wordToN x)%N -> (wordToN x <= high0)%N + -> (low1 <= wordToN y)%N -> (wordToN y <= high1)%N + -> (&x >= &y)%N -> (& (x ^- y) <= high0 - low1)%N. + Proof. + intros. + + destruct (Nge_dec 0%N (&y)). { + unfold wminus, wneg. + replace (& y) with 0%N in * by nomega. + replace low1 with 0%N by (symmetry; apply N.le_0_r; assumption). + replace (Npow2 n - 0)%N with (& (wzero n) + Npow2 n)%N + by (rewrite wordToN_zero; nomega). + rewrite <- Npow2_ignore. + rewrite wplus_comm. + rewrite wplus_unit. + replace (high0 - 0)%N with high0 by nomega; assumption. + } + + assert (& x - & y < Npow2 n)%N. { + transitivity (wordToN x); + try apply word_size_bound; + apply N.sub_lt; + [apply N.ge_le|]; assumption. + } + + assert (& x - & y + & y < Npow2 n)%N. { + replace (& x - & y + & y)%N + with (wordToN x) by nomega; + apply word_size_bound. + } + + assert (x = NToWord n (wordToN x - wordToN y) ^+ y) as Hv. { + apply NToWord_equal. + rewrite <- wordize_plus; rewrite wordToN_NToWord; try assumption. + nomega. + } + + rewrite Hv. + unfold wminus. + rewrite <- wplus_assoc. + rewrite wminus_inv. + rewrite wplus_comm. + rewrite wplus_unit. + rewrite wordToN_NToWord; try assumption. + + transitivity (high0 - & y)%N; + [apply N.sub_le_mono_r | apply N.sub_le_mono_l]; + assumption. + Qed. + Lemma wordize_mult: forall {n} (x y: word n), (&x * &y < Npow2 n)%N -> (&x * &y)%N = &(x ^* y). -- cgit v1.2.3