From 673534439ac5002e995ebcf49ea640692c83f2d8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 24 Aug 2018 21:40:48 -0400 Subject: Do almost all ZRange proofs We haven't done most of the fancy machine operations (and, in fact, most of that bounds analysis is wrong in theory even if it's correct on the inputs that we see), but the rest is done. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 17m45.36s | Total | 17m48.00s || -0m02.63s | -0.24% -------------------------------------------------------------------------------------------------------------------- 4m34.24s | Experiments/NewPipeline/Toplevel1 | 4m36.34s || -0m02.10s | -0.75% 0m21.01s | Experiments/NewPipeline/AbstractInterpretationZRangeProofs | 0m23.78s || -0m02.76s | -11.64% 6m03.20s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 6m01.29s || +0m01.90s | +0.52% 1m44.40s | Experiments/NewPipeline/Toplevel2 | 1m43.68s || +0m00.71s | +0.69% 0m38.53s | p521_32.c | 0m38.56s || -0m00.03s | -0.07% 0m37.22s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m37.36s || -0m00.14s | -0.37% 0m35.10s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m34.95s || +0m00.14s | +0.42% 0m32.10s | p521_64.c | 0m32.20s || -0m00.10s | -0.31% 0m23.75s | p384_32.c | 0m23.76s || -0m00.01s | -0.04% 0m20.06s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m20.38s || -0m00.32s | -1.57% 0m18.77s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m18.77s || +0m00.00s | +0.00% 0m13.63s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m13.52s || +0m00.11s | +0.81% 0m11.74s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m11.72s || +0m00.01s | +0.17% 0m10.38s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m10.40s || -0m00.01s | -0.19% 0m08.66s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.61s || +0m00.05s | +0.58% 0m08.50s | p384_64.c | 0m08.48s || +0m00.01s | +0.23% 0m05.46s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.52s || -0m00.05s | -1.08% 0m05.35s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.40s || -0m00.05s | -0.92% 0m03.98s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.04s || -0m00.06s | -1.48% 0m03.91s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m03.93s || -0m00.02s | -0.50% 0m03.90s | p256_32.c | 0m03.87s || +0m00.02s | +0.77% 0m03.76s | secp256k1_32.c | 0m03.73s || +0m00.02s | +0.80% 0m03.16s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.25s || -0m00.08s | -2.76% 0m02.21s | p224_32.c | 0m02.10s || +0m00.10s | +5.23% 0m02.15s | curve25519_32.c | 0m02.07s || +0m00.08s | +3.86% 0m01.67s | p224_64.c | 0m01.68s || -0m00.01s | -0.59% 0m01.65s | secp256k1_64.c | 0m01.66s || -0m00.01s | -0.60% 0m01.51s | p256_64.c | 0m01.66s || -0m00.14s | -9.03% 0m01.43s | Experiments/NewPipeline/CLI | 0m01.46s || -0m00.03s | -2.05% 0m01.38s | curve25519_64.c | 0m01.39s || -0m00.01s | -0.71% 0m01.28s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.26s || +0m00.02s | +1.58% 0m01.28s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.18s || +0m00.10s | +8.47% --- .../AbstractInterpretationZRangeProofs.v | 82 ++++++++++++++-------- 1 file changed, 52 insertions(+), 30 deletions(-) (limited to 'src') diff --git a/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v index cd918f263..a4b6098b7 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v +++ b/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v @@ -4,10 +4,11 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.Classes.RelationPairs. Require Import Coq.Relations.Relations. Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZRange.BasicLemmas. Require Import Crypto.Util.ZRange.SplitBounds. -Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZRange.CornersMonotoneBounds. +Require Import Crypto.Util.ZRange.LandLorBounds. Require Import Crypto.Util.Sum. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Prod. @@ -15,7 +16,6 @@ Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Option. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.ZUtil.Morphisms. Require Import Crypto.Util.ZUtil.AddGetCarry. Require Import Crypto.Util.ZUtil.AddModulo. Require Import Crypto.Util.ZUtil.CC. @@ -25,6 +25,7 @@ Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax. Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Import Crypto.Util.ZUtil.Morphisms. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. @@ -404,33 +405,7 @@ Module Compilers. | [ |- is_bounded_by_bool (_ mod _) r[_ ~> _] = true ] => cbv [is_bounded_by_bool]; rewrite Bool.andb_true_iff end | progress Z.ltb_to_lt - | progress rewrite ?Z.mul_split_div, ?Z.mul_split_mod, ?Z.add_get_carry_full_div, ?Z.add_get_carry_full_mod, ?Z.add_with_get_carry_full_div, ?Z.add_with_get_carry_full_mod, ?Z.sub_get_borrow_full_div, ?Z.sub_get_borrow_full_mod, ?Z.sub_with_get_borrow_full_div, ?Z.sub_with_get_borrow_full_mod, ?Z.zselect_correct, ?Z.add_modulo_correct - | rewrite Bool.andb_true_iff - | match goal with - | [ Hx : is_bounded_by_bool ?x ?x_bs = true - |- is_bounded_by_bool _ (ZRange.two_corners ?f ?x_bs) = true ] - => unshelve eapply (@ZRange.monotoneb_two_corners_gen f _ _ _ Hx) - | [ Hx : is_bounded_by_bool ?x ?x_bs = true, Hy : is_bounded_by_bool ?y ?y_bs = true - |- is_bounded_by_bool _ (ZRange.four_corners ?f ?x_bs ?y_bs) = true ] - => unshelve eapply (@ZRange.monotoneb_four_corners_gen f _ _ _ _ _ _ Hx Hy) - | [ Hx : is_bounded_by_bool ?x ?x_bs = true, Hy : is_bounded_by_bool ?y ?y_bs = true - |- is_bounded_by_bool _ (ZRange.four_corners_and_zero ?f ?x_bs ?y_bs) = true ] - => unshelve eapply (@ZRange.monotoneb_four_corners_and_zero_gen f _ _ _ _ _ _ _ _ Hx Hy) - | [ Hx : is_bounded_by_bool ?x ?x_bs = true, Hy : is_bounded_by_bool ?y ?y_bs = true, Hz : is_bounded_by_bool ?z ?z_bs = true - |- is_bounded_by_bool _ (ZRange.eight_corners ?f ?x_bs ?y_bs ?z_bs) = true ] - => unshelve eapply (@ZRange.monotoneb_eight_corners_gen f _ _ _ _ _ _ _ _ _ Hx Hy Hz) - | [ |- is_bounded_by_bool _ _ = true /\ is_bounded_by_bool _ _ = true ] => split - end ]. - all: try solve [ - repeat - first [ solve [ auto using ZRange.is_bounded_by_bool_Proper_if_sumbool_union, Z.mod_pos_bound, Z.mod_neg_bound with zarith ] - | match goal with - | [ |- forall x : Z, Proper _ _ \/ Proper _ _ ] => intros [|?|?] - | [ |- forall x y : Z, Proper _ _ \/ Proper _ _ ] => do 2 intros [|?|?] - | [ |- Proper _ _ \/ Proper _ _ ] - => cbv [Proper respectful Basics.flip]; - solve [ constructor; intros; autorewrite with Zshift_to_pow zsimplify_const; lia ] - end ] ]. + | progress rewrite ?Z.mul_split_div, ?Z.mul_split_mod, ?Z.add_get_carry_full_div, ?Z.add_get_carry_full_mod, ?Z.add_with_get_carry_full_div, ?Z.add_with_get_carry_full_mod, ?Z.sub_get_borrow_full_div, ?Z.sub_get_borrow_full_mod, ?Z.sub_with_get_borrow_full_div, ?Z.sub_with_get_borrow_full_mod, ?Z.zselect_correct, ?Z.add_modulo_correct ]. all: clear cast_outside_of_range. all: repeat match goal with | [ H : ?T |- _ ] @@ -442,7 +417,54 @@ Module Compilers. | _ => fail 10 T end end. - all: exact admit. + all: intros. + all: repeat lazymatch goal with + | [ |- is_bounded_by_bool (Z.land _ _) (ZRange.land_bounds _ _) = true ] + => apply ZRange.is_bounded_by_bool_land_bounds; auto + | [ |- is_bounded_by_bool (Z.lor _ _) (ZRange.lor_bounds _ _) = true ] + => apply ZRange.is_bounded_by_bool_lor_bounds; auto + | [ |- is_bounded_by_bool (if _ then (_ + _ - _)%Z else (_ + _)%Z) (ZRange.union (ZRange.four_corners Z.add _ _) (ZRange.eight_corners _ _ _ _)) = true ] + => rewrite ZRange.union_comm; apply ZRange.is_bounded_by_bool_Proper_if_bool_union_dep; intros; Z.ltb_to_lt + | [ |- is_bounded_by_bool (?a + ?b - ?c) (ZRange.eight_corners (fun x y z => Z.max 0 (x + y - z)) _ _ _) = true ] + => replace (a + b - c)%Z with (Z.max 0 (a + b - c)) by lia + | [ Hx : is_bounded_by_bool _ ?x = true, Hy : is_bounded_by_bool _ ?y = true, Hz : is_bounded_by_bool _ ?z = true + |- is_bounded_by_bool _ (ZRange.eight_corners ?f ?x ?y ?z) = true ] + => apply (fun pf1 pf2 pf3 => @ZRange.monotoneb_eight_corners_gen f pf1 pf2 pf3 _ _ _ _ _ _ Hx Hy Hz); intros; auto with zarith + | [ Hx : is_bounded_by_bool _ ?x = true, Hy : is_bounded_by_bool _ ?y = true + |- is_bounded_by_bool _ (ZRange.four_corners_and_zero ?f ?x ?y) = true ] + => apply (fun pf1 pf2 pf3 pf4 => @ZRange.monotoneb_four_corners_and_zero_gen f pf1 pf2 pf3 pf4 _ _ _ _ Hx Hy); intros; auto with zarith + | [ Hx : is_bounded_by_bool _ ?x = true, Hy : is_bounded_by_bool _ ?y = true + |- is_bounded_by_bool _ (ZRange.four_corners ?f ?x ?y) = true ] + => apply (fun pf1 pf2 => @ZRange.monotoneb_four_corners_gen f pf1 pf2 _ _ _ _ Hx Hy); intros; auto with zarith + | [ Hx : is_bounded_by_bool _ ?x = true + |- is_bounded_by_bool _ (ZRange.two_corners ?f ?x) = true ] + => apply (fun pf => @ZRange.monotoneb_two_corners_gen f pf x _ Hx); intros; auto with zarith + | [ H : ?x <> ?x |- _ ] => destruct (H eq_refl) + | [ |- context[Proper _ (Z.mul ?v)] ] => is_var v; destruct v; auto with zarith + | [ |- context[Proper _ (Z.div ?v)] ] => is_var v; destruct v; auto with zarith + | [ |- context[Proper _ (fun y => Z.mul _ ?v)] ] => is_var v; destruct v; auto with zarith + | [ |- context[Proper _ (fun y => Z.mul ?v _)] ] => is_var v; destruct v; auto with zarith + | [ |- context[Proper _ (fun y => Z.div _ ?v)] ] => is_var v; destruct v; auto with zarith + | [ |- context[Proper _ (fun y => Z.div ?v _)] ] => is_var v; destruct v; auto with zarith + | [ |- context[Proper _ (fun y => Z.shiftr _ ?v)] ] => is_var v; destruct v; auto with zarith + | [ |- context[Proper _ (fun y => Z.shiftr ?v _)] ] => is_var v; destruct v; auto with zarith + | [ |- context[Proper _ (fun y => Z.shiftl _ ?v)] ] => is_var v; destruct v; auto with zarith + | [ |- context[Proper _ (fun y => Z.shiftl ?v _)] ] => is_var v; destruct v; auto with zarith + | _ => idtac + end. + all: try solve [ cbv [Proper respectful Basics.flip]; constructor; intros; lia ]. + all: try solve [ cbv [Proper respectful Basics.flip]; constructor; intros; autorewrite with zsimplify_const; lia ]. + all: repeat match goal with + | [ H : ?T |- _ ] + => lazymatch T with + | Z => clear H + | zrange => clear H + | _ = true => revert H + | _ = false => revert H + | _ => fail 10 T + end + end. + 1-12: exact admit. Qed. End interp_related. End option. -- cgit v1.2.3