From cdd5ffb086eb647eabe640c81de9d8af7cd0a1dd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 17 Jan 2019 15:07:47 -0500 Subject: Split up PushButtonSynthesis.v Closes #497 --- src/PushButtonSynthesis/BarrettReduction.v | 133 ++++ .../BarrettReductionReificationCache.v | 30 + src/PushButtonSynthesis/InvertHighLow.v | 39 ++ src/PushButtonSynthesis/LegacySynthesisTactics.v | 112 +++ src/PushButtonSynthesis/MontgomeryReduction.v | 124 ++++ .../MontgomeryReductionReificationCache.v | 23 + src/PushButtonSynthesis/Primitives.v | 383 +++++++++++ src/PushButtonSynthesis/ReificationCache.v | 11 +- src/PushButtonSynthesis/SaturatedSolinas.v | 184 +++++ .../SaturatedSolinasReificationCache.v | 28 + src/PushButtonSynthesis/SmallExamples.v | 95 +++ src/PushButtonSynthesis/UnsaturatedSolinas.v | 602 ++++++++++++++++ .../UnsaturatedSolinasReificationCache.v | 168 +++++ src/PushButtonSynthesis/WordByWordMontgomery.v | 762 +++++++++++++++++++++ .../WordByWordMontgomeryReificationCache.v | 247 +++++++ 15 files changed, 2937 insertions(+), 4 deletions(-) create mode 100644 src/PushButtonSynthesis/BarrettReduction.v create mode 100644 src/PushButtonSynthesis/BarrettReductionReificationCache.v create mode 100644 src/PushButtonSynthesis/InvertHighLow.v create mode 100644 src/PushButtonSynthesis/LegacySynthesisTactics.v create mode 100644 src/PushButtonSynthesis/MontgomeryReduction.v create mode 100644 src/PushButtonSynthesis/MontgomeryReductionReificationCache.v create mode 100644 src/PushButtonSynthesis/Primitives.v create mode 100644 src/PushButtonSynthesis/SaturatedSolinas.v create mode 100644 src/PushButtonSynthesis/SaturatedSolinasReificationCache.v create mode 100644 src/PushButtonSynthesis/SmallExamples.v create mode 100644 src/PushButtonSynthesis/UnsaturatedSolinas.v create mode 100644 src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v create mode 100644 src/PushButtonSynthesis/WordByWordMontgomery.v create mode 100644 src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v (limited to 'src/PushButtonSynthesis') diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v new file mode 100644 index 000000000..3e3e4e105 --- /dev/null +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -0,0 +1,133 @@ +(** * Push-Button Synthesis of Barrett Reduction *) +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Language. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.PushButtonSynthesis.Primitives. +Require Import Crypto.PushButtonSynthesis.BarrettReductionReificationCache. +Require Import Crypto.PushButtonSynthesis.InvertHighLow. +Require Import Crypto.PushButtonSynthesis.LegacySynthesisTactics. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + Language.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. + +Import Associational Positional Arithmetic.BarrettReduction. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Local Opaque reified_barrett_red_gen. (* needed for making [autorewrite] not take a very long time *) + +Section rbarrett_red. + Context (M : Z) + (machine_wordsize : Z). + + Let value_range := r[0 ~> (2^machine_wordsize - 1)%Z]%zrange. + Let flag_range := r[0 ~> 1]%zrange. + Let bound := Some value_range. + Let mu := (2 ^ (2 * machine_wordsize)) / M. + Let muLow := mu mod (2 ^ machine_wordsize). + Let consts_list := [M; muLow]. + + Definition possible_values_of_machine_wordsize + := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z. + Let possible_values := possible_values_of_machine_wordsize. + + Definition check_args {T} (res : Pipeline.ErrorT T) + : Pipeline.ErrorT T + := fold_right + (fun '(b, e) k => if b:bool then Error e else k) + res + [((mu / (2 ^ machine_wordsize) =? 0), Pipeline.Values_not_provably_distinctZ "mu / 2 ^ k ≠ 0" (mu / 2 ^ machine_wordsize) 0); + ((machine_wordsize (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2)) + | None => True + end. + Proof. + cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right]; + split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence. + Qed. + + Definition barrett_red + := Pipeline.BoundsPipeline + false (* subst01 *) + fancy_args (* fancy *) + possible_values + (reified_barrett_red_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify M @ GallinaReify.Reify muLow @ GallinaReify.Reify 2%nat @ GallinaReify.Reify 2%nat) + (bound, (bound, tt)) + bound. + + Definition sbarrett_red (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "barrett_red" barrett_red. + + (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like +<< +Lemma barrett_red_correct res + (Hres : barrett_red = Success res) + : barrett_red_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. +>> *) + + Notation BoundsPipeline_correct in_bounds out_bounds op + := (fun rv (rop : Expr (reify_type_of op)) Hrop + => @Pipeline.BoundsPipeline_correct_trans + false (* subst01 *) + fancy_args + fancy_args_good + possible_values + _ + rop + in_bounds + out_bounds + _ + op + Hrop rv) + (only parsing). + + Definition rbarrett_red_correct + := BoundsPipeline_correct + (bound, (bound, tt)) + bound + (barrett_reduce machine_wordsize M muLow 2 2). + + Notation type_of_strip_3arrow := ((fun (d : Prop) (_ : forall A B C, d) => d) _). + Definition rbarrett_red_correctT rv : Prop + := type_of_strip_3arrow (@rbarrett_red_correct rv). +End rbarrett_red. + +(* TODO: After moving to new-glue-style, remove these tactics *) +Ltac solve_rbarrett_red := solve_rop rbarrett_red_correct. +Ltac solve_rbarrett_red_nocache := solve_rop_nocache rbarrett_red_correct. diff --git a/src/PushButtonSynthesis/BarrettReductionReificationCache.v b/src/PushButtonSynthesis/BarrettReductionReificationCache.v new file mode 100644 index 000000000..4c538087e --- /dev/null +++ b/src/PushButtonSynthesis/BarrettReductionReificationCache.v @@ -0,0 +1,30 @@ +(** * Push-Button Synthesis of Barrett Reduction: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Arithmetic. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import Associational Positional Arithmetic.BarrettReduction. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Module Export BarrettReduction. + (* all the list operations from for_reification.ident *) + Strategy 100 [length seq repeat combine map flat_map partition app rev fold_right update_nth nth_default ]. + Strategy -10 [barrett_reduce reduce]. + + Derive reified_barrett_red_gen + SuchThat (is_reification_of reified_barrett_red_gen barrett_reduce) + As reified_barrett_red_gen_correct. + Proof. Time cache_reify (). Time Qed. + + Module Export ReifyHints. + Hint Extern 1 (_ = _) => apply_cached_reification barrett_reduce (proj1 reified_barrett_red_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_barrett_red_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_barrett_red_gen_correct) : interp_gen_cache. + End ReifyHints. + Local Opaque reified_barrett_red_gen. (* needed for making [autorewrite] not take a very long time *) +End BarrettReduction. diff --git a/src/PushButtonSynthesis/InvertHighLow.v b/src/PushButtonSynthesis/InvertHighLow.v new file mode 100644 index 000000000..f7deb4145 --- /dev/null +++ b/src/PushButtonSynthesis/InvertHighLow.v @@ -0,0 +1,39 @@ +(** * Push-Button Synthesis fancy argument definitions *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Local Open Scope Z_scope. + +Section with_wordmax. + Context (log2wordmax : Z) (consts : list Z). + Let wordmax := 2 ^ log2wordmax. + Let half_bits := log2wordmax / 2. + Let wordmax_half_bits := 2 ^ half_bits. + + Inductive kind_of_constant := upper_half (c : BinInt.Z) | lower_half (c : BinInt.Z). + + Definition constant_to_scalar_single (const x : BinInt.Z) : option kind_of_constant := + if x =? (BinInt.Z.shiftr const half_bits) + then Some (upper_half const) + else if x =? (BinInt.Z.land const (wordmax_half_bits - 1)) + then Some (lower_half const) + else None. + + Definition constant_to_scalar (x : BinInt.Z) + : option kind_of_constant := + fold_right (fun c res => match res with + | Some s => Some s + | None => constant_to_scalar_single c x + end) None consts. + + Definition invert_low (v : BinInt.Z) : option BinInt.Z + := match constant_to_scalar v with + | Some (lower_half v) => Some v + | _ => None + end. + + Definition invert_high (v : BinInt.Z) : option BinInt.Z + := match constant_to_scalar v with + | Some (upper_half v) => Some v + | _ => None + end. +End with_wordmax. diff --git a/src/PushButtonSynthesis/LegacySynthesisTactics.v b/src/PushButtonSynthesis/LegacySynthesisTactics.v new file mode 100644 index 000000000..c2ae24f7c --- /dev/null +++ b/src/PushButtonSynthesis/LegacySynthesisTactics.v @@ -0,0 +1,112 @@ +(** * Push-Button Synthesis: Legacy Synthesis Tactics *) +Require Import Coq.Classes.Morphisms. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.Util.Equality. (* fg_equal_rel *) +Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Crypto.Util.Tactics.GetGoal. + +Import + LanguageWf.Compilers + Language.Compilers. +Import Compilers.defaults. + +(** TODO: Port Barrett and Montgomery to the new glue style, and remove these tactics. These tactics are only needed for the old-glue-style derivations. *) +Ltac peel_interp_app _ := + lazymatch goal with + | [ |- ?R' (?InterpE ?arg) (?f ?arg) ] + => apply fg_equal_rel; [ | reflexivity ]; + try peel_interp_app () + | [ |- ?R' (Interp ?ev) (?f ?x) ] + => let sv := type of x in + let fx := constr:(f x) in + let dv := type of fx in + let rs := reify_type sv in + let rd := reify_type dv in + etransitivity; + [ apply @expr.Interp_APP_rel_reflexive with (s:=rs) (d:=rd) (R:=R'); + typeclasses eauto + | apply fg_equal_rel; + [ try peel_interp_app () + | try lazymatch goal with + | [ |- ?R (Interp ?ev) (Interp _) ] + => reflexivity + | [ |- ?R (Interp ?ev) ?c ] + => let rc := constr:(GallinaReify.Reify c) in + unify ev rc; vm_compute; reflexivity + end ] ] + end. +Ltac pre_cache_reify _ := + let H' := fresh in + lazymatch goal with + | [ |- ?P /\ Wf ?e ] + => let P' := fresh in + evar (P' : Prop); + assert (H' : P' /\ Wf e); subst P' + end; + [ + | split; [ destruct H' as [H' _] | destruct H' as [_ H']; exact H' ]; + cbv [type.app_curried]; + let arg := fresh "arg" in + let arg2 := fresh in + intros arg arg2; + cbn [type.and_for_each_lhs_of_arrow type.eqv]; + let H := fresh in + intro H; + repeat match type of H with + | and _ _ => let H' := fresh in + destruct H as [H' H]; + rewrite <- H' + end; + clear dependent arg2; clear H; + intros _; + peel_interp_app (); + [ lazymatch goal with + | [ |- ?R (Interp ?ev) _ ] + => (tryif is_evar ev + then let ev' := fresh "ev" in set (ev' := ev) + else idtac) + end; + cbv [pointwise_relation]; + repeat lazymatch goal with + | [ H : _ |- _ ] => first [ constr_eq H H'; fail 1 + | revert H ] + end; + eexact H' + | .. ] ]; + [ intros; clear | .. ]. +Ltac do_inline_cache_reify do_if_not_cached := + pre_cache_reify (); + [ try solve [ + cbv beta zeta; + repeat match goal with H := ?e |- _ => is_evar e; subst H end; + try solve [ split; [ solve [ eauto with nocore reify_gen_cache ] | solve [ eauto with wf_gen_cache; prove_Wf () ] ] ]; + do_if_not_cached () + ]; + cache_reify () + | .. ]. + +(* TODO: MOVE ME *) +Ltac vm_compute_lhs_reflexivity := + lazymatch goal with + | [ |- ?LHS = ?RHS ] + => let x := (eval vm_compute in LHS) in + (* we cannot use the unify tactic, which just gives "not + unifiable" as the error message, because we want to see the + terms that were not unifable. See also + COQBUG(https://github.com/coq/coq/issues/7291) *) + let _unify := constr:(ltac:(reflexivity) : RHS = x) in + vm_cast_no_check (eq_refl x) + end. + +Ltac solve_rop' rop_correct do_if_not_cached machine_wordsizev := + eapply rop_correct with (machine_wordsize:=machine_wordsizev); + [ do_inline_cache_reify do_if_not_cached + | subst_evars; vm_compute_lhs_reflexivity (* lazy; reflexivity *) ]. +Ltac solve_rop_nocache rop_correct := + solve_rop' rop_correct ltac:(fun _ => idtac). +Ltac solve_rop rop_correct := + solve_rop' + rop_correct + ltac:(fun _ => let G := get_goal in fail 2 "Could not find a solution in reify_gen_cache for" G). diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v new file mode 100644 index 000000000..2b7841ac0 --- /dev/null +++ b/src/PushButtonSynthesis/MontgomeryReduction.v @@ -0,0 +1,124 @@ +(** * Push-Button Synthesis of Montgomery Reduction *) +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Language. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.PushButtonSynthesis.Primitives. +Require Import Crypto.PushButtonSynthesis.MontgomeryReductionReificationCache. +Require Import Crypto.PushButtonSynthesis.InvertHighLow. +Require Import Crypto.PushButtonSynthesis.LegacySynthesisTactics. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + Language.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. + +Import Associational Positional Arithmetic.MontgomeryReduction. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *) + +Section rmontred. + Context (N R N' : Z) + (machine_wordsize : Z). + + Let value_range := r[0 ~> (2^machine_wordsize - 1)%Z]%zrange. + Let flag_range := r[0 ~> 1]%zrange. + Let bound := Some value_range. + Let consts_list := [N; N']. + + Definition possible_values_of_machine_wordsize + := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z. + Local Arguments possible_values_of_machine_wordsize / . + + Let possible_values := possible_values_of_machine_wordsize. + + Definition check_args {T} (res : Pipeline.ErrorT T) + : Pipeline.ErrorT T + := res. (* TODO: this should actually check stuff that corresponds with preconditions of montred'_correct *) + + Let fancy_args + := (Some {| Pipeline.invert_low log2wordsize := invert_low log2wordsize consts_list; + Pipeline.invert_high log2wordsize := invert_high log2wordsize consts_list; + Pipeline.value_range := value_range; + Pipeline.flag_range := flag_range |}). + + Lemma fancy_args_good + : match fancy_args with + | Some {| Pipeline.invert_low := il ; Pipeline.invert_high := ih |} + => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2)) + | None => True + end. + Proof. + cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right]; + split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence. + Qed. + + Definition montred + := Pipeline.BoundsPipeline + false (* subst01 *) + fancy_args (* fancy *) + possible_values + (reified_montred_gen + @ GallinaReify.Reify N @ GallinaReify.Reify R @ GallinaReify.Reify N' @ GallinaReify.Reify (Z.log2 R) @ GallinaReify.Reify 2%nat @ GallinaReify.Reify 2%nat) + (bound, (bound, tt)) + bound. + + Definition smontred (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "montred" montred. + + (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like +<< +Lemma montred_correct res + (Hres : montred = Success res) + : montred_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. +>> *) + + Notation BoundsPipeline_correct in_bounds out_bounds op + := (fun rv (rop : Expr (reify_type_of op)) Hrop + => @Pipeline.BoundsPipeline_correct_trans + false (* subst01 *) + fancy_args + fancy_args_good + possible_values + _ + rop + in_bounds + out_bounds + _ + op + Hrop rv) + (only parsing). + + Definition rmontred_correct + := BoundsPipeline_correct + (bound, (bound, tt)) + bound + (montred' N R N' (Z.log2 R) 2 2). + + Notation type_of_strip_3arrow := ((fun (d : Prop) (_ : forall A B C, d) => d) _). + Definition rmontred_correctT rv : Prop + := type_of_strip_3arrow (@rmontred_correct rv). +End rmontred. + +(* TODO: After moving to new-glue-style, remove these tactics *) +Ltac solve_rmontred := solve_rop rmontred_correct. +Ltac solve_rmontred_nocache := solve_rop_nocache rmontred_correct. diff --git a/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v b/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v new file mode 100644 index 000000000..f787063a4 --- /dev/null +++ b/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v @@ -0,0 +1,23 @@ +(** * Push-Button Synthesis of Saturated Solinas: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Crypto.Arithmetic. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import Associational Positional Arithmetic.MontgomeryReduction. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Module Export MontgomeryReduction. + Derive reified_montred_gen + SuchThat (is_reification_of reified_montred_gen montred') + As reified_montred_gen_correct. + Proof. Time cache_reify (). Time Qed. + Module Export ReifyHints. + Hint Extern 1 (_ = _) => apply_cached_reification montred' (proj1 reified_montred_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_montred_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_montred_gen_correct) : interp_gen_cache. + End ReifyHints. + Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *) +End MontgomeryReduction. diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v new file mode 100644 index 000000000..4afa64433 --- /dev/null +++ b/src/PushButtonSynthesis/Primitives.v @@ -0,0 +1,383 @@ +(** * Push-Button Synthesis of Primitives *) +Require Import Coq.Strings.String. +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.Lists.List. +Require Import Coq.QArith.QArith_base Coq.QArith.Qround. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.Strings.Decimal. +Require Import Crypto.Util.Strings.Equality. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.Tactics.HasBody. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + LanguageWf.Compilers + Language.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. +Import COperationSpecifications.Solinas. (* for selectznz *) + +Import Associational Positional. + +Local Coercion Z.of_nat : nat >-> Z. +Local Coercion QArith_base.inject_Z : Z >-> Q. +Local Coercion Z.pos : positive >-> Z. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +(** +<< +#!/usr/bin/env python + +indent = '' + +print((indent + '(' + r'''** +<< +%s +>> +*''' + ')\n') % open(__file__, 'r').read()) + +for (op, opmod) in (('id', '(@id (list Z))'), ('selectznz', 'Positional.select'), ('mulx', 'mulx'), ('addcarryx', 'addcarryx'), ('subborrowx', 'subborrowx'), ('cmovznz', 'cmovznz')): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %s) + As reified_%s_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %s (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, op, op, opmod, op, opmod, op, op, op, op)).replace('\n', '\n%s' % indent) + '\n') + +>> +*) + +Derive reified_id_gen + SuchThat (is_reification_of reified_id_gen (@id (list Z))) + As reified_id_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification (@id (list Z)) (proj1 reified_id_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_id_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_id_gen_correct) : interp_gen_cache. +Local Opaque reified_id_gen. (* needed for making [autorewrite] not take a very long time *) + +Derive reified_selectznz_gen + SuchThat (is_reification_of reified_selectznz_gen Positional.select) + As reified_selectznz_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification Positional.select (proj1 reified_selectznz_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_selectznz_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_selectznz_gen_correct) : interp_gen_cache. +Local Opaque reified_selectznz_gen. (* needed for making [autorewrite] not take a very long time *) + +Derive reified_mulx_gen + SuchThat (is_reification_of reified_mulx_gen mulx) + As reified_mulx_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification mulx (proj1 reified_mulx_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_mulx_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_mulx_gen_correct) : interp_gen_cache. +Local Opaque reified_mulx_gen. (* needed for making [autorewrite] not take a very long time *) + +Derive reified_addcarryx_gen + SuchThat (is_reification_of reified_addcarryx_gen addcarryx) + As reified_addcarryx_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification addcarryx (proj1 reified_addcarryx_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_addcarryx_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_addcarryx_gen_correct) : interp_gen_cache. +Local Opaque reified_addcarryx_gen. (* needed for making [autorewrite] not take a very long time *) + +Derive reified_subborrowx_gen + SuchThat (is_reification_of reified_subborrowx_gen subborrowx) + As reified_subborrowx_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification subborrowx (proj1 reified_subborrowx_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_subborrowx_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_subborrowx_gen_correct) : interp_gen_cache. +Local Opaque reified_subborrowx_gen. (* needed for making [autorewrite] not take a very long time *) + +Derive reified_cmovznz_gen + SuchThat (is_reification_of reified_cmovznz_gen cmovznz) + As reified_cmovznz_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification cmovznz (proj1 reified_cmovznz_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_cmovznz_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_cmovznz_gen_correct) : interp_gen_cache. +Local Opaque reified_cmovznz_gen. (* needed for making [autorewrite] not take a very long time *) + +(* needed for making [autorewrite] with [Set Keyed Unification] fast *) +Local Opaque expr.Interp. + +Local Notation arg_bounds_of_pipeline result + := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => arg_bounds) _ _ _ _ _ _ _ result eq_refl) + (only parsing). +Local Notation out_bounds_of_pipeline result + := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => out_bounds) _ _ _ _ _ _ _ result eq_refl) + (only parsing). + +Notation FromPipelineToString prefix name result + := (((prefix ++ name)%string, + match result with + | Success E' + => let E := ToString.C.ToFunctionLines + true true (* static *) prefix (prefix ++ name)%string [] E' None + (arg_bounds_of_pipeline result) + (out_bounds_of_pipeline result) in + match E with + | inl E => Success E + | inr err => Error (Pipeline.Stringification_failed E' err) + end + | Error err => Error err + end)). + +Ltac prove_correctness use_curve_good := + let Hres := match goal with H : _ = Success _ |- _ => H end in + let H := fresh in + pose proof use_curve_good as H; + (* I want to just use [clear -H Hres], but then I can't use any lemmas in the section because of COQBUG(https://github.com/coq/coq/issues/8153) *) + repeat match goal with + | [ H' : _ |- _ ] + => tryif first [ has_body H' | constr_eq H' H | constr_eq H' Hres ] + then fail + else clear H' + end; + cbv zeta in *; + destruct_head'_and; + let f := match type of Hres with ?f = _ => head f end in + try cbv [f] in *; + hnf; + PipelineTactics.do_unfolding; + try (let m := match goal with m := _ - Associational.eval _ |- _ => m end in + cbv [m] in * ); + intros; + try split; PipelineTactics.use_compilers_correctness Hres; + [ pose_proof_length_list_Z_bounded_by; + repeat first [ reflexivity + | progress autorewrite with interp interp_gen_cache push_eval + | progress autounfold with push_eval + | progress autorewrite with distr_length in * ] + | .. ]. + +Section __. + Context (n : nat) + (machine_wordsize : Z). + + Definition saturated_bounds_list : list (option zrange) + := List.repeat (Some r[0 ~> 2^machine_wordsize-1]%zrange) n. + Definition saturated_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some saturated_bounds_list. + + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) + Definition possible_values_of_machine_wordsize + := [0; machine_wordsize; 2 * machine_wordsize]%Z. + + Definition possible_values_of_machine_wordsize_with_bytes + := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. + + Let possible_values := possible_values_of_machine_wordsize. + Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. + + Lemma length_saturated_bounds_list : List.length saturated_bounds_list = n. + Proof using Type. cbv [saturated_bounds_list]; now autorewrite with distr_length. Qed. + Hint Rewrite length_saturated_bounds_list : distr_length. + + Definition selectznz + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + reified_selectznz_gen + (Some r[0~>1], (saturated_bounds, (saturated_bounds, tt)))%zrange + saturated_bounds. + + Definition sselectznz (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "selectznz" selectznz. + + Definition mulx (s : Z) + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_mulx_gen + @ GallinaReify.Reify s) + (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt))%zrange + (Some r[0~>2^s-1], Some r[0~>2^s-1])%zrange. + + Definition smulx (prefix : string) (s : Z) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix ("mulx_u" ++ decimal_string_of_Z s) (mulx s). + + Definition addcarryx (s : Z) + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_addcarryx_gen + @ GallinaReify.Reify s) + (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange + (Some r[0~>2^s-1], Some r[0~>1])%zrange. + + Definition saddcarryx (prefix : string) (s : Z) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s). + + Definition subborrowx (s : Z) + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_subborrowx_gen + @ GallinaReify.Reify s) + (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange + (Some r[0~>2^s-1], Some r[0~>1])%zrange. + + Definition ssubborrowx (prefix : string) (s : Z) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s). + + Definition cmovznz (s : Z) + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_cmovznz_gen + @ GallinaReify.Reify s) + (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange + (Some r[0~>2^s-1])%zrange. + + Definition scmovznz (prefix : string) (s : Z) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix ("cmovznz_u" ++ decimal_string_of_Z s) (cmovznz s). + + Local Ltac solve_extra_bounds_side_conditions := + cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. + + Hint Rewrite + eval_select + Arithmetic.mulx_correct + Arithmetic.addcarryx_correct + Arithmetic.subborrowx_correct + Arithmetic.cmovznz_correct + Z.zselect_correct + using solve [ auto | congruence | solve_extra_bounds_side_conditions ] : push_eval. + + Strategy -1000 [mulx]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma mulx_correct s' res + (Hres : mulx s' = Success res) + : mulx_correct s' (Interp res). + Proof using Type. prove_correctness I. Qed. + + Strategy -1000 [addcarryx]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma addcarryx_correct s' res + (Hres : addcarryx s' = Success res) + : addcarryx_correct s' (Interp res). + Proof using Type. prove_correctness I. Qed. + + Strategy -1000 [subborrowx]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma subborrowx_correct s' res + (Hres : subborrowx s' = Success res) + : subborrowx_correct s' (Interp res). + Proof using Type. prove_correctness I. Qed. + + Strategy -1000 [cmovznz]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma cmovznz_correct s' res + (Hres : cmovznz s' = Success res) + : cmovznz_correct s' (Interp res). + Proof using Type. prove_correctness I. Qed. + + Lemma selectznz_correct limbwidth res + (Hres : selectznz = Success res) + : selectznz_correct (weight (Qnum limbwidth) (QDen limbwidth)) n saturated_bounds_list (Interp res). + Proof using Type. prove_correctness I. Qed. + + Section for_stringification. + Context (valid_names : string) + (known_functions : list (string + * (string + -> string * + Pipeline.ErrorT (list string * ToString.C.ident_infos)))) + (extra_special_synthesis : string -> + list + (option + (string * + Pipeline.ErrorT + (list string * ToString.C.ident_infos)))). + + Definition aggregate_infos {A B C} (ls : list (A * ErrorT B (C * ToString.C.ident_infos))) : ToString.C.ident_infos + := fold_right + ToString.C.ident_info_union + ToString.C.ident_info_empty + (List.map + (fun '(_, res) => match res with + | Success (_, infos) => infos + | Error _ => ToString.C.ident_info_empty + end) + ls). + + Definition extra_synthesis (function_name_prefix : string) (infos : ToString.C.ident_infos) + : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t + := let ls_addcarryx := List.flat_map + (fun lg_split:positive => [saddcarryx function_name_prefix lg_split; ssubborrowx function_name_prefix lg_split]) + (PositiveSet.elements (ToString.C.addcarryx_lg_splits infos)) in + let ls_mulx := List.map + (fun lg_split:positive => smulx function_name_prefix lg_split) + (PositiveSet.elements (ToString.C.mulx_lg_splits infos)) in + let ls_cmov := List.map + (fun bitwidth:positive => scmovznz function_name_prefix bitwidth) + (PositiveSet.elements (ToString.C.cmovznz_bitwidths infos)) in + let ls := ls_addcarryx ++ ls_mulx ++ ls_cmov in + let infos := aggregate_infos ls in + (List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls, + ToString.C.bitwidths_used infos). + + + Definition synthesize_of_name (function_name_prefix : string) (name : string) + : string * ErrorT Pipeline.ErrorMessage (list string * ToString.C.ident_infos) + := fold_right + (fun v default + => match v with + | Some res => res + | None => default + end) + ((name, + Error + (Pipeline.Invalid_argument + ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ valid_names ++ ".")))) + ((map + (fun '(expected_name, resf) => if string_beq name expected_name then Some (resf function_name_prefix) else None) + known_functions) + ++ extra_special_synthesis name). + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition Synthesize (function_name_prefix : string) (requests : list string) + : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + := let ls := match requests with + | nil => List.map (fun '(_, sr) => sr function_name_prefix) known_functions + | requests => List.map (synthesize_of_name function_name_prefix) requests + end in + let infos := aggregate_infos ls in + let '(extra_ls, extra_bit_widths) := extra_synthesis function_name_prefix infos in + (extra_ls ++ List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls, + PositiveSet.union extra_bit_widths (ToString.C.bitwidths_used infos)). + End for_stringification. +End __. diff --git a/src/PushButtonSynthesis/ReificationCache.v b/src/PushButtonSynthesis/ReificationCache.v index ba8488820..148cac049 100644 --- a/src/PushButtonSynthesis/ReificationCache.v +++ b/src/PushButtonSynthesis/ReificationCache.v @@ -26,10 +26,13 @@ Definition is_reification_of' {t} (e : Expr t) (v : type.interp base.interp t) : := pointwise_equal (Interp e) v /\ Wf e. Notation is_reification_of rop op - := (ltac:(let T := constr:(@is_reification_of' (reify_type_of op) rop op) in - let T := (eval cbv [pointwise_equal is_reification_of'] in T) in - let T := (eval cbn [type.interp base.interp base.base_interp] in T) in - exact T)) + := (match @is_reification_of' (reify_type_of op) rop op with + | T + => ltac:( + let T := (eval cbv [pointwise_equal is_reification_of' T] in T) in + let T := (eval cbn [type.interp base.interp base.base_interp] in T) in + exact T) + end) (only parsing). Ltac cache_reify _ := diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v new file mode 100644 index 000000000..bcb93c4a1 --- /dev/null +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -0,0 +1,184 @@ +(** * Push-Button Synthesis of Saturated Solinas *) +Require Import Coq.Strings.String. +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.Lists.List. +Require Import Coq.QArith.QArith_base Coq.QArith.Qround. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.FoldBool. +Require Import Crypto.Util.Strings.Decimal. +Require Import Crypto.Util.Strings.Equality. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.Tactics.HasBody. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.AbstractInterpretation. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.PushButtonSynthesis.Primitives. +Require Import Crypto.PushButtonSynthesis.SaturatedSolinasReificationCache. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + LanguageWf.Compilers + Language.Compilers + AbstractInterpretation.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. +Import COperationSpecifications.Solinas. +Import COperationSpecifications.SaturatedSolinas. + +Import Associational Positional. + +Local Coercion Z.of_nat : nat >-> Z. +Local Coercion QArith_base.inject_Z : Z >-> Q. +Local Coercion Z.pos : positive >-> Z. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Local Opaque reified_mul_gen. (* needed for making [autorewrite] not take a very long time *) +(* needed for making [autorewrite] with [Set Keyed Unification] fast *) +Local Opaque expr.Interp. + +Section __. + Context (s : Z) + (c : list (Z * Z)) + (machine_wordsize : Z). + + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) + Definition possible_values_of_machine_wordsize + := [0; 1; machine_wordsize]%Z. + + Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)). + Let m := s - Associational.eval c. + (* Number of reductions is calculated as follows : + Let i be the highest limb index of c. Then, each reduction + decreases the number of extra limbs by (n-i). So, to go from + the n extra limbs we have post-multiplication down to 0, we + need ceil (n / (n - i)) reductions. *) + Let nreductions : nat := + let i := fold_right Z.max 0 (map (fun t => Z.log2 (fst t) / machine_wordsize) c) in + Z.to_nat (Qceiling (Z.of_nat n / (Z.of_nat n - i))). + Let possible_values := possible_values_of_machine_wordsize. + Let bound := Some r[0 ~> (2^machine_wordsize - 1)]%zrange. + Let boundsn : list (ZRange.type.option.interp base.type.Z) + := repeat bound n. + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition check_args {T} (res : Pipeline.ErrorT T) + : Pipeline.ErrorT T + := fold_right + (fun '(b, e) k => if b:bool then Error e else k) + res + [((negb (0 0 + /\ s <> 0 + /\ 0 < machine_wordsize + /\ n <> 0%nat. + Proof using curve_good. + clear -curve_good. + cbv [check_args fold_right] in curve_good. + break_innermost_match_hyps; try discriminate. + rewrite negb_false_iff in *. + Z.ltb_to_lt. + rewrite NPeano.Nat.eqb_neq in *. + intros. + rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *. + specialize_by lia. + repeat match goal with H := _ |- _ => subst H end. + repeat match goal with + | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ] + end. + repeat apply conj. + { destruct (s - Associational.eval c) eqn:?; cbn; lia. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + Qed. + + Definition mul + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_mul_gen + @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify nreductions) + (Some boundsn, (Some boundsn, tt)) + (Some boundsn, None (* Should be: Some r[0~>0]%zrange, but bounds analysis is not good enough *) ). + + Definition smul (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "mul" mul. + + Local Ltac solve_extra_bounds_side_conditions := + cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. + + Hint Rewrite + (fun pf => @Rows.eval_mulmod (weight machine_wordsize 1) (@wprops _ _ pf)) + using solve [ auto with zarith | congruence | solve_extra_bounds_side_conditions ] : push_eval. + Hint Unfold mulmod : push_eval. + + Local Ltac prove_correctness _ := Primitives.prove_correctness use_curve_good. + + Lemma mul_correct res + (Hres : mul = Success res) + : mul_correct (weight machine_wordsize 1) n m boundsn (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Section for_stringification. + Local Open Scope string_scope. + Local Open Scope list_scope. + + Definition known_functions + := [("mul", smul)]. + + Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions). + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition Synthesize (function_name_prefix : string) (requests : list string) + : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + := Primitives.Synthesize + machine_wordsize valid_names known_functions (fun _ => nil) + function_name_prefix requests. + End for_stringification. +End __. diff --git a/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v b/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v new file mode 100644 index 000000000..ccc48e2cd --- /dev/null +++ b/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v @@ -0,0 +1,28 @@ +(** * Push-Button Synthesis of Saturated Solinas: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Crypto.Arithmetic. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import Associational Positional. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Module Export SaturatedSolinas. + Definition mulmod + (s : Z) + (c : list (Z * Z)) + (log2base : Z) + (n nreductions : nat) + := @Rows.mulmod (weight log2base 1) (2^log2base) s c n nreductions. + + Derive reified_mul_gen + SuchThat (is_reification_of reified_mul_gen mulmod) + As reified_mul_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification mulmod (proj1 reified_mul_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_mul_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_mul_gen_correct) : interp_gen_cache. + Local Opaque reified_mul_gen. (* needed for making [autorewrite] not take a very long time *) +End SaturatedSolinas. diff --git a/src/PushButtonSynthesis/SmallExamples.v b/src/PushButtonSynthesis/SmallExamples.v new file mode 100644 index 000000000..09f361356 --- /dev/null +++ b/src/PushButtonSynthesis/SmallExamples.v @@ -0,0 +1,95 @@ +(** * Push-Button Synthesis Examples *) +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Language. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. + +Import + Language.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import Associational Positional. + +Time Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (to_associational (weight 51 1) 5) in + exact r) + (Some (repeat (@None _) 5), tt) + ZRange.type.base.option.None). + +Time Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (scmul (weight 51 1) 5) in + exact r) + (None, (Some (repeat (@None _) 5), tt)) + ZRange.type.base.option.None). + +Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun f => carry_mulmod 51 1 (2^255) [(1,19)] 5 (seq 0 5 ++ [0; 1])%list%nat f f) in + exact r) + (Some (repeat (@None _) 5), tt) + ZRange.type.base.option.None). + +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_mulx_u64" [] + true None [64; 128] + ltac:(let r := Reify (Arithmetic.mulx 64) in + exact r) + (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt))%zrange + (Some r[0~>2^64-1], Some r[0~>2^64-1])%zrange). + +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_addcarryx_u64" [] + true None [1; 64; 128] + ltac:(let r := Reify (Arithmetic.addcarryx 64) in + exact r) + (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange + (Some r[0~>2^64-1], Some r[0~>1])%zrange). + +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_addcarryx_u51" [] + true None [1; 64; 128] + ltac:(let r := Reify (Arithmetic.addcarryx 51) in + exact r) + (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange + (Some r[0~>2^51-1], Some r[0~>1])%zrange). + +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_subborrowx_u64" [] + true None [1; 64; 128] + ltac:(let r := Reify (Arithmetic.subborrowx 64) in + exact r) + (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange + (Some r[0~>2^64-1], Some r[0~>1])%zrange). +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_subborrowx_u51" [] + true None [1; 64; 128] + ltac:(let r := Reify (Arithmetic.subborrowx 51) in + exact r) + (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange + (Some r[0~>2^51-1], Some r[0~>1])%zrange). + +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_cmovznz64" [] + true None [1; 64; 128] + ltac:(let r := Reify (Arithmetic.cmovznz 64) in + exact r) + (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange + (Some r[0~>2^64-1])%zrange). diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v new file mode 100644 index 000000000..4f22070c5 --- /dev/null +++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v @@ -0,0 +1,602 @@ +(** * Push-Button Synthesis of Unsaturated Solinas *) +Require Import Coq.Strings.String. +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.Lists.List. +Require Import Coq.QArith.QArith_base Coq.QArith.Qround. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.FoldBool. +Require Import Crypto.Util.Strings.Decimal. +Require Import Crypto.Util.Strings.Equality. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.Tactics.HasBody. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.AbstractInterpretation. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.PushButtonSynthesis.Primitives. +Require Import Crypto.PushButtonSynthesis.UnsaturatedSolinasReificationCache. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + LanguageWf.Compilers + Language.Compilers + AbstractInterpretation.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. +Import COperationSpecifications.Solinas. + +Import Associational Positional. + +Local Coercion Z.of_nat : nat >-> Z. +Local Coercion QArith_base.inject_Z : Z >-> Q. +Local Coercion Z.pos : positive >-> Z. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +(* needed for making [autorewrite] not take a very long time *) +Local Opaque + reified_carry_square_gen + reified_carry_scmul_gen + reified_carry_gen + reified_encode_gen + reified_add_gen + reified_sub_gen + reified_opp_gen + reified_zero_gen + reified_one_gen + reified_prime_gen + reified_to_bytes_gen + reified_from_bytes_gen + expr.Interp. + +Section __. + Context (n : nat) + (s : Z) + (c : list (Z * Z)) + (machine_wordsize : Z). + + Let limbwidth := (Z.log2_up (s - Associational.eval c) / Z.of_nat n)%Q. + Let idxs := (List.seq 0 n ++ [0; 1])%list%nat. + Let coef := 2. + Let n_bytes := bytes_n (Qnum limbwidth) (Qden limbwidth) n. + Let prime_upperbound_list : list Z + := encode_no_reduce (weight (Qnum limbwidth) (Qden limbwidth)) n (s-1). + Let prime_bytes_upperbound_list : list Z + := encode_no_reduce (weight 8 1) n_bytes (s-1). + Let tight_upperbounds : list Z + := List.map + (fun v : Z => Qceiling (11/10 * v)) + prime_upperbound_list. + Definition prime_bound : ZRange.type.option.interp (base.type.Z) + := Some r[0~>(s - Associational.eval c - 1)]%zrange. + Definition prime_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_upperbound_list). + Definition prime_bytes_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_bytes_upperbound_list). + Local Notation saturated_bounds_list := (saturated_bounds_list n machine_wordsize). + Local Notation saturated_bounds := (saturated_bounds n machine_wordsize). + + Let m : Z := s - Associational.eval c. + Definition m_enc : list Z + := encode (weight (Qnum limbwidth) (Qden limbwidth)) n s c m. + + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) + Definition possible_values_of_machine_wordsize + := [0; machine_wordsize; 2 * machine_wordsize]%Z. + + Definition possible_values_of_machine_wordsize_with_bytes + := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. + + Let possible_values := possible_values_of_machine_wordsize. + Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. + Definition tight_bounds : list (ZRange.type.option.interp base.type.Z) + := List.map (fun u => Some r[0~>u]%zrange) tight_upperbounds. + Definition loose_bounds : list (ZRange.type.option.interp base.type.Z) + := List.map (fun u => Some r[0 ~> 3*u]%zrange) tight_upperbounds. + + Lemma length_prime_upperbound_list : List.length prime_upperbound_list = n. + Proof using Type. cbv [prime_upperbound_list]; now autorewrite with distr_length. Qed. + Hint Rewrite length_prime_upperbound_list : distr_length. + Lemma length_tight_upperbounds : List.length tight_upperbounds = n. + Proof using Type. cbv [tight_upperbounds]; now autorewrite with distr_length. Qed. + Hint Rewrite length_tight_upperbounds : distr_length. + Lemma length_tight_bounds : List.length tight_bounds = n. + Proof using Type. cbv [tight_bounds]; now autorewrite with distr_length. Qed. + Hint Rewrite length_tight_bounds : distr_length. + Lemma length_loose_bounds : List.length loose_bounds = n. + Proof using Type. cbv [loose_bounds]; now autorewrite with distr_length. Qed. + Hint Rewrite length_loose_bounds : distr_length. + Lemma length_prime_bytes_upperbound_list : List.length prime_bytes_upperbound_list = bytes_n (Qnum limbwidth) (Qden limbwidth) n. + Proof using Type. cbv [prime_bytes_upperbound_list]; now autorewrite with distr_length. Qed. + Hint Rewrite length_prime_bytes_upperbound_list : distr_length. + Lemma length_saturated_bounds_list : List.length saturated_bounds_list = n. + Proof using Type. cbv [saturated_bounds_list]; now autorewrite with distr_length. Qed. + Hint Rewrite length_saturated_bounds_list : distr_length. + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition check_args {T} (res : Pipeline.ErrorT T) + : Pipeline.ErrorT T + := fold_right + (fun '(b, e) k => if b:bool then Error e else k) + res + [(negb (Qle_bool 1 limbwidth)%Q, Pipeline.Value_not_leQ "limbwidth < 1" 1%Q limbwidth); + ((negb (0 0 + /\ s <> 0 + /\ 0 < machine_wordsize + /\ n <> 0%nat + /\ List.length tight_bounds = n + /\ List.length loose_bounds = n + /\ List.length prime_bytes_upperbound_list = n_bytes + /\ List.length saturated_bounds_list = n + /\ 0 < Qden limbwidth <= Qnum limbwidth + /\ s = weight (Qnum limbwidth) (QDen limbwidth) n + /\ map (Z.land (Z.ones machine_wordsize)) m_enc = m_enc + /\ eval m_enc = s - Associational.eval c + /\ Datatypes.length m_enc = n + /\ 0 < Associational.eval c < s + /\ eval tight_upperbounds < 2 * eval m_enc + /\ 0 < m. + Proof using curve_good. + clear -curve_good. + cbv [check_args fold_right] in curve_good. + cbv [tight_bounds loose_bounds prime_bound m_enc] in *. + break_innermost_match_hyps; try discriminate. + rewrite negb_false_iff in *. + Z.ltb_to_lt. + rewrite Qle_bool_iff in *. + rewrite NPeano.Nat.eqb_neq in *. + intros. + cbv [Qnum Qden limbwidth Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *. + rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *. + specialize_by lia. + repeat match goal with H := _ |- _ => subst H end. + repeat match goal with + | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ] + end. + repeat apply conj. + { destruct (s - Associational.eval c) eqn:?; cbn; lia. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + Qed. + + Definition carry_mul + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_carry_mul_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) + (Some loose_bounds, (Some loose_bounds, tt)) + (Some tight_bounds). + + Definition scarry_mul (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "carry_mul" carry_mul. + + Definition carry_square + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_carry_square_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) + (Some loose_bounds, tt) + (Some tight_bounds). + + Definition scarry_square (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "carry_square" carry_square. + + Definition carry_scmul_const (x : Z) + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_carry_scmul_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs @ GallinaReify.Reify x) + (Some loose_bounds, tt) + (Some tight_bounds). + + Definition scarry_scmul_const (prefix : string) (x : Z) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x). + + Definition carry + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_carry_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) + (Some loose_bounds, tt) + (Some tight_bounds). + + Definition scarry (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "carry" carry. + + Definition add + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_add_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify n) + (Some tight_bounds, (Some tight_bounds, tt)) + (Some loose_bounds). + + Definition sadd (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "add" add. + + Definition sub + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_sub_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify coef) + (Some tight_bounds, (Some tight_bounds, tt)) + (Some loose_bounds). + + Definition ssub (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "sub" sub. + + Definition opp + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_opp_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify coef) + (Some tight_bounds, tt) + (Some loose_bounds). + + Definition sopp (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "opp" opp. + + Definition to_bytes + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_to_bytes_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify n @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify m_enc) + (Some tight_bounds, tt) + prime_bytes_bounds. + + Definition sto_bytes (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "to_bytes" to_bytes. + + Definition from_bytes + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_from_bytes_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify n) + (prime_bytes_bounds, tt) + (Some tight_bounds). + + Definition sfrom_bytes (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "from_bytes" from_bytes. + + Definition encode + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_encode_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n) + (prime_bound, tt) + (Some tight_bounds). + + Definition sencode (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "encode" encode. + + Definition zero + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_zero_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n) + tt + (Some tight_bounds). + + Definition szero (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "zero" zero. + + Definition one + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_one_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n) + tt + (Some tight_bounds). + + Definition sone (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "one" one. + + Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. + Definition sselectznz (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Primitives.sselectznz n machine_wordsize prefix. + + Local Ltac solve_extra_bounds_side_conditions := + cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. + + Hint Rewrite + eval_carry_mulmod + eval_carry_squaremod + eval_carry_scmulmod + eval_addmod + eval_submod + eval_oppmod + eval_carrymod + freeze_to_bytesmod_partitions + eval_to_bytesmod + eval_from_bytesmod + eval_encodemod + using solve [ auto | congruence | solve_extra_bounds_side_conditions ] : push_eval. + Hint Unfold zeromod onemod : push_eval. + + Local Ltac prove_correctness _ := + Primitives.prove_correctness use_curve_good; + try solve [ auto | congruence | solve_extra_bounds_side_conditions ]. + + Lemma carry_mul_correct res + (Hres : carry_mul = Success res) + : carry_mul_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma carry_square_correct res + (Hres : carry_square = Success res) + : carry_square_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma carry_scmul_const_correct a res + (Hres : carry_scmul_const a = Success res) + : carry_scmul_const_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds a (Interp res). + Proof using curve_good. + prove_correctness (). + erewrite eval_carry_scmulmod by (auto || congruence); reflexivity. + Qed. + + Lemma carry_correct res + (Hres : carry = Success res) + : carry_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma add_correct res + (Hres : add = Success res) + : add_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma sub_correct res + (Hres : sub = Success res) + : sub_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma opp_correct res + (Hres : opp = Success res) + : opp_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma from_bytes_correct res + (Hres : from_bytes = Success res) + : from_bytes_correct (weight (Qnum limbwidth) (QDen limbwidth)) n n_bytes m s tight_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma relax_correct + : forall x, list_Z_bounded_by tight_bounds x -> list_Z_bounded_by loose_bounds x. + Proof using Type. + cbv [tight_bounds loose_bounds list_Z_bounded_by]. + intro. + rewrite !fold_andb_map_map1, !fold_andb_map_iff; cbn [upper lower]. + setoid_rewrite Bool.andb_true_iff. + intro H. + repeat first [ let H' := fresh in destruct H as [H' H]; split; [ assumption | ] + | let x := fresh in intro x; specialize (H x) ]. + Z.ltb_to_lt; lia. + Qed. + + Lemma to_bytes_correct res + (Hres : to_bytes = Success res) + : to_bytes_correct (weight (Qnum limbwidth) (QDen limbwidth)) n n_bytes m tight_bounds (Interp res). + Proof using curve_good. + prove_correctness (); []. + erewrite freeze_to_bytesmod_partitions; [ reflexivity | .. ]. + all: repeat apply conj; autorewrite with distr_length; (congruence || auto). + all: cbv [tight_bounds] in *. + all: lazymatch goal with + | [ H1 : list_Z_bounded_by (List.map (fun x => Some (@?f x)) ?b) ?x, H2 : eval ?wt ?n ?b < _ + |- context[eval ?wt ?n ?x] ] + => unshelve epose proof (eval_list_Z_bounded_by wt n (List.map (fun x => Some (f x)) b) (List.map f b) x H1 _ _ (fun A B => Z.lt_le_incl _ _ (weight_positive _ _))); clear H1 + end. + all: congruence || auto. + all: repeat first [ reflexivity + | apply wprops + | progress rewrite ?map_map in * + | progress rewrite ?map_id in * + | progress cbn [upper lower] in * + | lia + | match goal with + | [ H : context[List.map (fun _ => 0) _] |- _ ] => erewrite <- zeros_ext_map, ?eval_zeros in H by reflexivity + end + | progress autorewrite with distr_length push_eval in * + | progress cbv [tight_upperbounds] in * ]. + Qed. + + Strategy -1000 [encode]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma encode_correct res + (Hres : encode = Success res) + : encode_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Strategy -1000 [zero]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma zero_correct res + (Hres : zero = Success res) + : zero_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Strategy -1000 [one]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma one_correct res + (Hres : one = Success res) + : one_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Section ring. + Context carry_mul_res (Hcarry_mul : carry_mul = Success carry_mul_res) + add_res (Hadd : add = Success add_res) + sub_res (Hsub : sub = Success sub_res) + opp_res (Hopp : opp = Success opp_res) + carry_res (Hcarry : carry = Success carry_res) + encode_res (Hencode : encode = Success encode_res) + zero_res (Hzero : zero = Success zero_res) + one_res (Hone : one = Success one_res). + + Definition GoodT : Prop + := GoodT + (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds + (Interp carry_mul_res) + (Interp add_res) + (Interp sub_res) + (Interp opp_res) + (Interp carry_res) + (Interp encode_res) + (Interp zero_res) + (Interp one_res). + + Theorem Good : GoodT. + Proof using curve_good Hcarry_mul Hadd Hsub Hopp Hcarry Hencode Hzero Hone. + pose proof use_curve_good; cbv zeta in *; destruct_head'_and. + eapply Good. + all: repeat first [ assumption + | apply carry_mul_correct + | apply add_correct + | apply sub_correct + | apply opp_correct + | apply carry_correct + | apply encode_correct + | apply zero_correct + | apply one_correct + | apply relax_correct ]. + Qed. + End ring. + + Section for_stringification. + Local Open Scope string_scope. + Local Open Scope list_scope. + + Definition known_functions + := [("carry_mul", scarry_mul); + ("carry_square", scarry_square); + ("carry", scarry); + ("add", sadd); + ("sub", ssub); + ("opp", sopp); + ("selectznz", sselectznz); + ("to_bytes", sto_bytes); + ("from_bytes", sfrom_bytes)]. + + Definition valid_names : string + := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions) ++ ", or 'carry_scmul' followed by a decimal literal". + + Definition extra_special_synthesis (function_name_prefix : string) (name : string) + : list (option (string * Pipeline.ErrorT (list string * ToString.C.ident_infos))) + := [if prefix "carry_scmul" name + then let sc := substring (String.length "carry_scmul") (String.length name) name in + let scZ := Z_of_decimal_string sc in + if string_beq sc (decimal_string_of_Z scZ) + then Some (scarry_scmul_const function_name_prefix scZ) + else None + else None]. + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition Synthesize (function_name_prefix : string) (requests : list string) + : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + := Primitives.Synthesize + machine_wordsize valid_names known_functions (extra_special_synthesis function_name_prefix) + function_name_prefix requests. + End for_stringification. +End __. diff --git a/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v b/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v new file mode 100644 index 000000000..3cee63c4e --- /dev/null +++ b/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v @@ -0,0 +1,168 @@ +(** * Push-Button Synthesis of Unsaturated Solinas: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Crypto.Arithmetic. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import Associational Positional. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Module Export UnsaturatedSolinas. + Definition zeromod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 0. + Definition onemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 1. + Definition primemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n (s - Associational.eval c). + + (** +<< +#!/usr/bin/env python + +indent = ' ' + +print((indent + '(' + r'''** +<< +%s +>> +*''' + ')\n') % open(__file__, 'r').read()) + +for i in ('carry_mul', 'carry_square', 'carry_scmul', 'carry', 'encode', 'add', 'sub', 'opp', 'zero', 'one', 'prime'): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %smod) + As reified_%s_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') + +for (op, opmod) in (('to_bytes', 'freeze_to_bytesmod'), ('from_bytes', 'from_bytesmod')): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %s) + As reified_%s_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %s (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, op, op, opmod, op, opmod, op, op, op, op)).replace('\n', '\n%s' % indent) + '\n') + +>> +*) + + Derive reified_carry_mul_gen + SuchThat (is_reification_of reified_carry_mul_gen carry_mulmod) + As reified_carry_mul_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification carry_mulmod (proj1 reified_carry_mul_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_carry_mul_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_carry_mul_gen_correct) : interp_gen_cache. + Local Opaque reified_carry_mul_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_carry_square_gen + SuchThat (is_reification_of reified_carry_square_gen carry_squaremod) + As reified_carry_square_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification carry_squaremod (proj1 reified_carry_square_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_carry_square_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_carry_square_gen_correct) : interp_gen_cache. + Local Opaque reified_carry_square_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_carry_scmul_gen + SuchThat (is_reification_of reified_carry_scmul_gen carry_scmulmod) + As reified_carry_scmul_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification carry_scmulmod (proj1 reified_carry_scmul_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_carry_scmul_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_carry_scmul_gen_correct) : interp_gen_cache. + Local Opaque reified_carry_scmul_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_carry_gen + SuchThat (is_reification_of reified_carry_gen carrymod) + As reified_carry_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification carrymod (proj1 reified_carry_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_carry_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_carry_gen_correct) : interp_gen_cache. + Local Opaque reified_carry_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_encode_gen + SuchThat (is_reification_of reified_encode_gen encodemod) + As reified_encode_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification encodemod (proj1 reified_encode_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_encode_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_encode_gen_correct) : interp_gen_cache. + Local Opaque reified_encode_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_add_gen + SuchThat (is_reification_of reified_add_gen addmod) + As reified_add_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification addmod (proj1 reified_add_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_add_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_add_gen_correct) : interp_gen_cache. + Local Opaque reified_add_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_sub_gen + SuchThat (is_reification_of reified_sub_gen submod) + As reified_sub_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification submod (proj1 reified_sub_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_sub_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_sub_gen_correct) : interp_gen_cache. + Local Opaque reified_sub_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_opp_gen + SuchThat (is_reification_of reified_opp_gen oppmod) + As reified_opp_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification oppmod (proj1 reified_opp_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_opp_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_opp_gen_correct) : interp_gen_cache. + Local Opaque reified_opp_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_zero_gen + SuchThat (is_reification_of reified_zero_gen zeromod) + As reified_zero_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification zeromod (proj1 reified_zero_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_zero_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_zero_gen_correct) : interp_gen_cache. + Local Opaque reified_zero_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_one_gen + SuchThat (is_reification_of reified_one_gen onemod) + As reified_one_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification onemod (proj1 reified_one_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_one_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_one_gen_correct) : interp_gen_cache. + Local Opaque reified_one_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_prime_gen + SuchThat (is_reification_of reified_prime_gen primemod) + As reified_prime_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification primemod (proj1 reified_prime_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_prime_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_prime_gen_correct) : interp_gen_cache. + Local Opaque reified_prime_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_to_bytes_gen + SuchThat (is_reification_of reified_to_bytes_gen freeze_to_bytesmod) + As reified_to_bytes_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification freeze_to_bytesmod (proj1 reified_to_bytes_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_to_bytes_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_to_bytes_gen_correct) : interp_gen_cache. + Local Opaque reified_to_bytes_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_from_bytes_gen + SuchThat (is_reification_of reified_from_bytes_gen from_bytesmod) + As reified_from_bytes_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification from_bytesmod (proj1 reified_from_bytes_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_from_bytes_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_from_bytes_gen_correct) : interp_gen_cache. + Local Opaque reified_from_bytes_gen. (* needed for making [autorewrite] not take a very long time *) +End UnsaturatedSolinas. diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v new file mode 100644 index 000000000..3b28329c5 --- /dev/null +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -0,0 +1,762 @@ +(** * Push-Button Synthesis of Word-By-Word Montgomery *) +Require Import Coq.Strings.String. +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.Lists.List. +Require Import Coq.QArith.QArith_base Coq.QArith.Qround. +Require Import Coq.Program.Tactics. (* For WBW Montgomery proofs *) +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.FoldBool. +Require Import Crypto.Util.Strings.Decimal. +Require Import Crypto.Util.Strings.Equality. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.ModInv. (* Only needed for WBW Montgomery *) +Require Import Crypto.Util.ZUtil.Modulo. (* Only needed for WBW Montgomery proofs *) +Require Import Crypto.Util.ZUtil.Le. (* Only needed for WBW Montgomery proofs *) +Require Import Crypto.Util.Prod. (* For WBW Montgomery proofs *) +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. (* For WBW montgomery proofs *) +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. (* For WBW montgomery proofs *) +Require Import Crypto.Util.ZUtil.Div. (* For WBW Montgomery proofs *) +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. (* For WBW Montgomery proofs *) +Require Import Crypto.Util.ZUtil.Ones. (* For WBW montgomery proofs *) +Require Import Crypto.Util.ZUtil.Shift. (* For WBW montgomery proofs *) +Require Import Crypto.Util.Tactics.HasBody. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.AbstractInterpretation. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.PushButtonSynthesis.Primitives. +Require Import Crypto.PushButtonSynthesis.WordByWordMontgomeryReificationCache. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + LanguageWf.Compilers + Language.Compilers + AbstractInterpretation.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. +Import COperationSpecifications.Solinas. +Import COperationSpecifications.WordByWordMontgomery. + +Import Associational Positional. +Import Arithmetic.WordByWordMontgomery. + +Import WordByWordMontgomeryReificationCache.WordByWordMontgomery. + +Local Coercion Z.of_nat : nat >-> Z. +Local Coercion QArith_base.inject_Z : Z >-> Q. +Local Coercion Z.pos : positive >-> Z. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +(* needed for making [autorewrite] not take a very long time *) +Local Opaque + reified_mul_gen + reified_add_gen + reified_sub_gen + reified_opp_gen + reified_to_bytes_gen + reified_from_bytes_gen + reified_nonzero_gen + reified_square_gen + reified_encode_gen + reified_from_montgomery_gen + reified_zero_gen + reified_one_gen + expr.Interp. + +Section __. + Context (m : Z) + (machine_wordsize : Z). + + Let s := 2^Z.log2_up m. + Let c := s - m. + Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)). + Let r := 2^machine_wordsize. + Let r' := match Z.modinv r m with + | Some r' => r' + | None => 0 + end. + Let m' := match Z.modinv (-m) r with + | Some m' => m' + | None => 0 + end. + Let n_bytes := bytes_n machine_wordsize 1 n. + Let prime_upperbound_list : list Z + := Partition.partition (UniformWeight.uweight machine_wordsize) n (s-1). + Let prime_bytes_upperbound_list : list Z + := Partition.partition (weight 8 1) n_bytes (s-1). + Let upperbounds : list Z := prime_upperbound_list. + Definition prime_bound : ZRange.type.option.interp (base.type.Z) + := Some r[0~>m-1]%zrange. + Definition prime_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_upperbound_list). + Definition prime_bytes_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_bytes_upperbound_list). + Local Notation saturated_bounds_list := (saturated_bounds_list n machine_wordsize). + Local Notation saturated_bounds := (saturated_bounds n machine_wordsize). + + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) + Definition possible_values_of_machine_wordsize + := [0; 1; machine_wordsize; 2 * machine_wordsize]%Z. + + Definition possible_values_of_machine_wordsize_with_bytes + := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. + + Let possible_values := possible_values_of_machine_wordsize. + Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. + Definition bounds : list (ZRange.type.option.interp base.type.Z) + := Option.invert_Some saturated_bounds (*List.map (fun u => Some r[0~>u]%zrange) upperbounds*). + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition check_args {T} (res : Pipeline.ErrorT T) + : Pipeline.ErrorT T + := fold_right + (fun '(b, e) k => if b:bool then Error e else k) + res + [(negb (1 0 + /\ s - c <> 0 + /\ 0 < s + /\ s <> 0 + /\ 0 < machine_wordsize + /\ n <> 0%nat + /\ List.length bounds = n + /\ 0 < 1 <= machine_wordsize + /\ 0 < c < s + /\ (r * r') mod m = 1 + /\ (m * m') mod r = (-1) mod r + /\ 0 < machine_wordsize + /\ 1 < m + /\ m < r^n + /\ s = 2^Z.log2 s + /\ s <= UniformWeight.uweight machine_wordsize n + /\ s <= UniformWeight.uweight 8 n_bytes + /\ UniformWeight.uweight machine_wordsize n = UniformWeight.uweight 8 n_bytes. + Proof. + clear -curve_good. + cbv [check_args fold_right] in curve_good. + cbv [bounds prime_bound prime_bounds saturated_bounds] in *. + break_innermost_match_hyps; try discriminate. + rewrite negb_false_iff in *. + Z.ltb_to_lt. + rewrite NPeano.Nat.eqb_neq in *. + intros. + cbv [Qnum Qden Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *. + rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *. + specialize_by lia. + repeat match goal with H := _ |- _ => subst H end. + repeat match goal with + | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ] + end. + repeat apply conj. + { destruct m eqn:?; cbn; lia. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + Qed. + + + Definition mul + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_mul_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + (Some bounds, (Some bounds, tt)) + (Some bounds). + + Definition smul (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "mul" mul. + + Definition square + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_square_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + (Some bounds, tt) + (Some bounds). + + Definition ssquare (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "square" square. + + Definition add + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_add_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m) + (Some bounds, (Some bounds, tt)) + (Some bounds). + + Definition sadd (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "add" add. + + Definition sub + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_sub_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m) + (Some bounds, (Some bounds, tt)) + (Some bounds). + + Definition ssub (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "sub" sub. + + Definition opp + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_opp_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m) + (Some bounds, tt) + (Some bounds). + + Definition sopp (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "opp" opp. + + Definition from_montgomery + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_from_montgomery_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + (Some bounds, tt) + (Some bounds). + + Definition sfrom_montgomery (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "from_montgomery" from_montgomery. + + Definition nonzero + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + reified_nonzero_gen + (Some bounds, tt) + (Some r[0~>r-1]%zrange). + + Definition snonzero (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "nonzero" nonzero. + + Definition to_bytes + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_to_bytes_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n) + (prime_bounds, tt) + prime_bytes_bounds. + + Definition sto_bytes (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "to_bytes" to_bytes. + + Definition from_bytes + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_from_bytes_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify 1 @ GallinaReify.Reify n) + (prime_bytes_bounds, tt) + prime_bounds. + + Definition sfrom_bytes (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "from_bytes" from_bytes. + + Definition encode + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_encode_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + (prime_bound, tt) + (Some bounds). + + Definition sencode (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "encode" encode. + + Definition zero + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_zero_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + tt + (Some bounds). + + Definition szero (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "zero" zero. + + Definition one + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_one_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + tt + (Some bounds). + + Definition sone (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "one" one. + + Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. + Definition sselectznz (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Primitives.sselectznz n machine_wordsize prefix. + + Local Notation valid := (Arithmetic.WordByWordMontgomery.valid machine_wordsize n m). + Local Notation bytes_valid := (Arithmetic.WordByWordMontgomery.valid 8 n_bytes m). + + Lemma bounded_by_of_valid x + (H : valid x) + : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some bounds) x = true. + Proof using curve_good. + pose proof use_curve_good as use_curve_good. + clear -H use_curve_good curve_good. + destruct H as [H _]; destruct_head'_and. + cbv [small] in H. + cbv [ZRange.type.base.option.is_bounded_by bounds saturated_bounds saturated_bounds_list Option.invert_Some]. + replace n with (List.length x) by now rewrite H, Partition.length_partition. + rewrite <- map_const, fold_andb_map_map1, fold_andb_map_iff. + cbv [ZRange.type.base.is_bounded_by is_bounded_by_bool lower upper]. + split; [ reflexivity | ]. + intros *; rewrite combine_same, in_map_iff, Bool.andb_true_iff, !Z.leb_le. + intros; destruct_head'_ex; destruct_head'_and; subst *; cbn [fst snd]. + match goal with + | [ H : In ?v x |- _ ] => revert v H + end. + rewrite H. + generalize (eval (n:=n) machine_wordsize x). + cbn [base.interp base.base_interp]. + generalize n. + intro n'. + induction n' as [|n' IHn']. + { cbv [Partition.partition seq map In]; tauto. } + { intros *; rewrite Partition.partition_step, in_app_iff; cbn [List.In]. + intros; destruct_head'_or; subst *; eauto; try tauto; []. + rewrite UniformWeight.uweight_S by lia. + assert (0 < UniformWeight.uweight machine_wordsize n') by now apply UniformWeight.uwprops. + assert (0 < 2 ^ machine_wordsize) by auto with zarith. + assert (0 < 2 ^ machine_wordsize * UniformWeight.uweight machine_wordsize n') by nia. + rewrite <- Z.mod_pull_div by lia. + rewrite Z.le_sub_1_iff. + auto with zarith. } + Qed. + + (* XXX FIXME *) + Lemma bounded_by_prime_bounds_of_valid_gen lgr n' x + (Hlgr : 0 < lgr) + (Hs : s = 2^Z.log2 s) + (Hs' : s <= UniformWeight.uweight lgr n') + (H : WordByWordMontgomery.valid lgr n' m x) + : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some (List.map (fun v => Some r[0~>v]%zrange) (Partition.partition (UniformWeight.uweight lgr) n' (s-1)))) x = true. + Proof using curve_good. + pose proof use_curve_good as use_curve_good. + clear -H use_curve_good curve_good Hlgr Hs Hs'. + destruct H as [H ?]; destruct_head'_and. + cbv [small] in H. + cbv [ZRange.type.base.option.is_bounded_by]. + replace n' with (List.length x) by now rewrite H, Partition.length_partition. + rewrite fold_andb_map_map1, fold_andb_map_iff. + split; [ now autorewrite with distr_length | ]. + cbv [ZRange.type.base.is_bounded_by is_bounded_by_bool lower upper]. + rewrite H; autorewrite with distr_length. + intros [v1 v0]; cbn [fst snd]. + rename x into x'. + generalize dependent (eval (n:=n') lgr x'). + replace m with (s - c) in * by easy. + intro x; intros ??? H; subst x'. + eapply In_nth_error in H; destruct H as [i H]. + rewrite nth_error_combine in H. + break_match_hyps; try discriminate; []; Option.inversion_option; Prod.inversion_prod; subst. + cbv [Partition.partition] in *. + apply nth_error_map in Heqo; apply nth_error_map in Heqo0; destruct Heqo as (?&?&?), Heqo0 as (?&?&?). + rewrite nth_error_seq in *. + break_match_hyps; try discriminate; Option.inversion_option; Prod.inversion_prod; subst. + rewrite ?Nat.add_0_l. + assert (0 <= x < s) by lia. + replace s with (2^Z.log2 s) by easy. + assert (1 < s) by lia. + assert (0 < Z.log2 s) by now apply Z.log2_pos. + assert (1 < 2^Z.log2 s) by auto with zarith. + generalize dependent (Z.log2 s); intro lgs; intros. + + edestruct (UniformWeight.uwprops lgr); try lia. + assert (forall i : nat, 0 <= UniformWeight.uweight lgr i) by (intro z; specialize (weight_positive z); lia). + apply Bool.andb_true_intro; split; apply OrdersEx.Z_as_OT.leb_le; + [apply Z.div_nonneg | apply Z.div_le_mono_nonneg]; trivial. + apply Z.mod_pos_bound; trivial. + + cbv [UniformWeight.uweight]. + cbv [weight]. + rewrite Z.div_1_r. + rewrite Z.opp_involutive. + rewrite <-2Z.land_ones by nia. + rewrite Z.sub_1_r, <-Z.ones_equiv. + rewrite Z.land_ones_ones. + destruct ((lgs H end in + let H := fresh in + pose proof use_curve_good as H; + (* I want to just use [clear -H Hres], but then I can't use any lemmas in the section because of COQBUG(https://github.com/coq/coq/issues/8153) *) + repeat match goal with + | [ H' : _ |- _ ] + => tryif first [ has_body H' | constr_eq H' H | constr_eq H' Hres | dont_clear H' ] + then fail + else clear H' + end; + cbv zeta in *; + destruct_head'_and; + let f := match type of Hres with ?f = _ => head f end in + try cbv [f] in *; + hnf; + PipelineTactics.do_unfolding; + try (let m := match goal with m := _ - Associational.eval _ |- _ => m end in + cbv [m] in * ); + intros; + lazymatch goal with + | [ |- _ <-> _ ] => idtac + | [ |- _ = _ ] => idtac + | _ => split; [ | try split ]; + cbv [small] + end; + PipelineTactics.use_compilers_correctness Hres; + repeat first [ reflexivity + | now apply bounded_by_of_valid + | now apply bounded_by_prime_bounds_of_valid + | now apply bounded_by_prime_bytes_bounds_of_bytes_valid + | now apply weight_bounded_of_bytes_valid + | solve [ eapply op_correct; try eassumption; solve_extra_bounds_side_conditions ] + | progress autorewrite with interp interp_gen_cache push_eval + | progress autounfold with push_eval + | progress autorewrite with distr_length in * + | solve [ cbv [valid small eval UniformWeight.uweight n_bytes] in *; destruct_head'_and; auto ] ]. + + (** TODO: DESIGN DECISION: + + The correctness lemmas for most of the montgomery things are + parameterized over a `from_montgomery`. When filling this in + for, e.g., mul-correctness, should I use `from_montgomery` + from arithmetic, or should I use `Interp + reified_from_montgomery` (the post-pipeline version), and take + in success of the pipeline on `from_montgomery` as well? *) + + Local Notation from_montgomery_res := (from_montgomerymod machine_wordsize n m m'). + + Lemma mul_correct res + (Hres : mul = Success res) + : mul_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness mulmod_correct. Qed. + + Lemma square_correct res + (Hres : square = Success res) + : square_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness squaremod_correct. Qed. + + Lemma add_correct res + (Hres : add = Success res) + : add_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness addmod_correct. Qed. + + Lemma sub_correct res + (Hres : sub = Success res) + : sub_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness submod_correct. Qed. + + Lemma opp_correct res + (Hres : opp = Success res) + : opp_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness oppmod_correct. Qed. + + Lemma from_montgomery_correct res + (Hres : from_montgomery = Success res) + : from_montgomery_correct machine_wordsize n m r' valid (Interp res). + Proof using curve_good. prove_correctness from_montgomerymod_correct. Qed. + + Lemma nonzero_correct res + (Hres : nonzero = Success res) + : nonzero_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness nonzeromod_correct. Qed. + + Lemma to_bytes_correct res + (Hres : to_bytes = Success res) + : to_bytes_correct machine_wordsize n n_bytes m valid (Interp res). + Proof using curve_good. prove_correctness to_bytesmod_correct. Qed. + + Lemma from_bytes_correct res + (Hres : from_bytes = Success res) + : from_bytes_correct machine_wordsize n n_bytes m valid bytes_valid (Interp res). + Proof using curve_good. prove_correctness eval_from_bytesmod_and_partitions. Qed. + + Strategy -1000 [encode]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma encode_correct res + (Hres : encode = Success res) + : encode_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness encodemod_correct. Qed. + + Strategy -1000 [zero]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma zero_correct res + (Hres : zero = Success res) + : zero_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness encodemod_correct. Qed. + + Strategy -1000 [one]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma one_correct res + (Hres : one = Success res) + : one_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness encodemod_correct. Qed. + + Local Opaque Pipeline.BoundsPipeline. (* need this or else [eapply Pipeline.BoundsPipeline_correct in Hres] takes forever *) + Lemma selectznz_correct res + (Hres : selectznz = Success res) + : selectznz_correct machine_wordsize n saturated_bounds_list (Interp res). + Proof using curve_good. Primitives.prove_correctness use_curve_good. Qed. + + Section ring. + Context from_montgomery_res (Hfrom_montgomery : from_montgomery = Success from_montgomery_res) + mul_res (Hmul : mul = Success mul_res) + add_res (Hadd : add = Success add_res) + sub_res (Hsub : sub = Success sub_res) + opp_res (Hopp : opp = Success opp_res) + encode_res (Hencode : encode = Success encode_res) + zero_res (Hzero : zero = Success zero_res) + one_res (Hone : one = Success one_res). + + Definition GoodT : Prop + := GoodT + machine_wordsize n m valid + (Interp from_montgomery_res) + (Interp mul_res) + (Interp add_res) + (Interp sub_res) + (Interp opp_res) + (Interp encode_res) + (Interp zero_res) + (Interp one_res). + + Theorem Good : GoodT. + Proof using curve_good Hfrom_montgomery Hmul Hadd Hsub Hopp Hencode Hzero Hone. + pose proof use_curve_good; cbv zeta in *; destruct_head'_and. + eapply Good. + all: repeat first [ assumption + | apply from_montgomery_correct + | lia ]. + all: hnf; intros. + all: push_Zmod; erewrite !(fun v Hv => proj1 (from_montgomery_correct _ Hfrom_montgomery v Hv)), <- !eval_from_montgomerymod; try eassumption; pull_Zmod. + all: repeat first [ assumption + | lazymatch goal with + | [ |- context[mul_res] ] => apply mul_correct + | [ |- context[add_res] ] => apply add_correct + | [ |- context[sub_res] ] => apply sub_correct + | [ |- context[opp_res] ] => apply opp_correct + | [ |- context[encode_res] ] => apply encode_correct + | [ |- context[zero_res] ] => apply zero_correct + | [ |- context[one_res] ] => apply one_correct + end ]. + Qed. + End ring. + + Section for_stringification. + Local Open Scope string_scope. + Local Open Scope list_scope. + + Definition known_functions + := [("mul", smul); + ("square", ssquare); + ("add", sadd); + ("sub", ssub); + ("opp", sopp); + ("from_montgomery", sfrom_montgomery); + ("nonzero", snonzero); + ("selectznz", sselectznz); + ("to_bytes", sto_bytes); + ("from_bytes", sfrom_bytes)]. + + Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions). + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition Synthesize (function_name_prefix : string) (requests : list string) + : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + := Primitives.Synthesize + machine_wordsize valid_names known_functions (fun _ => nil) + function_name_prefix requests. + End for_stringification. +End __. diff --git a/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v b/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v new file mode 100644 index 000000000..ac429cdb5 --- /dev/null +++ b/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v @@ -0,0 +1,247 @@ +(** * Push-Button Synthesis of Word-By-Word Montgomery: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Arithmetic. +Require Import Crypto.Language. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import + LanguageWf.Compilers + Language.Compilers. +Import Compilers.defaults. + +Import Associational Positional. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Module Export WordByWordMontgomery. + Import Arithmetic.WordByWordMontgomery. + + Definition zeromod bitwidth n m m' := encodemod bitwidth n m m' 0. + Definition onemod bitwidth n m m' := encodemod bitwidth n m m' 1. + + (* we would do something faster, but it generally breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) + Local Ltac precache_reify_faster _ := + split; + [ let marker := fresh "marker" in + pose I as marker; + intros; + let LHS := lazymatch goal with |- ?LHS = _ => LHS end in + let reified_op_gen := lazymatch LHS with context[expr.Interp _ ?reified_op_gen] => reified_op_gen end in + subst reified_op_gen; + etransitivity; + [ + | let opmod := match goal with |- _ = ?RHS => head RHS end in + cbv [opmod]; solve [ eauto with reify_cache_gen nocore ] ]; + repeat lazymatch goal with + | [ H : _ |- _ ] => tryif constr_eq H marker then fail else revert H + end; + clear marker + | ]. + Local Ltac cache_reify_faster_2arg _ := + precache_reify_faster (); + [ lazymatch goal with + | [ |- forall bw n m m' v, ?interp ?ev bw n m m' v = ?interp' ?reified_mul_gen bw n m m' (@?A bw n m m' v) (@?B bw n m m' v) ] + => let rv := constr:(fun F bw n m m' v => (F bw n m m' (A bw n m m' v) (B bw n m m' v)):list Z) in + intros; + instantiate (1:=ltac:(let r := Reify rv in + refine (r @ reified_mul_gen)%Expr)) + end; + reflexivity + | prove_Wf () ]. + Local Ltac cache_reify_faster_1arg _ := + precache_reify_faster (); + [ lazymatch goal with + | [ |- forall bw n m m', ?interp ?ev bw n m m' = ?interp' ?reified_op_gen bw n m m' (@?A bw n m m') ] + => let rv := constr:(fun F bw n m m' => (F bw n m m' (A bw n m m')):list Z) in + intros; + instantiate (1:=ltac:(let r := Reify rv in + refine (r @ reified_op_gen)%Expr)) + end; + reflexivity + | prove_Wf () ]. + + (** +<< +#!/usr/bin/env python + +indent = ' ' + +print((indent + '(' + r'''** +<< +%s +>> +*''' + ')\n') % open(__file__, 'r').read()) + +for i in ('mul', 'add', 'sub', 'opp', 'to_bytes', 'from_bytes', 'nonzero'): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %smod) + As reified_%s_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') + +for i in ('square', 'encode', 'from_montgomery'): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %smod) + As reified_%s_gen_correct. +Proof. + Time cache_reify (). + (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) + (* Time cache_reify_faster_2arg (). *) +Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') + + +for i in ('zero', 'one'): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %smod) + As reified_%s_gen_correct. +Proof. + (* Time cache_reify (). *) + (* we do something faster *) + Time cache_reify_faster_1arg (). +Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') + +>> +*) + + Derive reified_mul_gen + SuchThat (is_reification_of reified_mul_gen mulmod) + As reified_mul_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification mulmod (proj1 reified_mul_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_mul_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_mul_gen_correct) : interp_gen_cache. + Local Opaque reified_mul_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_add_gen + SuchThat (is_reification_of reified_add_gen addmod) + As reified_add_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification addmod (proj1 reified_add_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_add_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_add_gen_correct) : interp_gen_cache. + Local Opaque reified_add_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_sub_gen + SuchThat (is_reification_of reified_sub_gen submod) + As reified_sub_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification submod (proj1 reified_sub_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_sub_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_sub_gen_correct) : interp_gen_cache. + Local Opaque reified_sub_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_opp_gen + SuchThat (is_reification_of reified_opp_gen oppmod) + As reified_opp_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification oppmod (proj1 reified_opp_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_opp_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_opp_gen_correct) : interp_gen_cache. + Local Opaque reified_opp_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_to_bytes_gen + SuchThat (is_reification_of reified_to_bytes_gen to_bytesmod) + As reified_to_bytes_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification to_bytesmod (proj1 reified_to_bytes_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_to_bytes_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_to_bytes_gen_correct) : interp_gen_cache. + Local Opaque reified_to_bytes_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_from_bytes_gen + SuchThat (is_reification_of reified_from_bytes_gen from_bytesmod) + As reified_from_bytes_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification from_bytesmod (proj1 reified_from_bytes_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_from_bytes_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_from_bytes_gen_correct) : interp_gen_cache. + Local Opaque reified_from_bytes_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_nonzero_gen + SuchThat (is_reification_of reified_nonzero_gen nonzeromod) + As reified_nonzero_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification nonzeromod (proj1 reified_nonzero_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_nonzero_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_nonzero_gen_correct) : interp_gen_cache. + Local Opaque reified_nonzero_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_square_gen + SuchThat (is_reification_of reified_square_gen squaremod) + As reified_square_gen_correct. + Proof. + Time cache_reify (). + (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) + (* Time cache_reify_faster_2arg (). *) + Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification squaremod (proj1 reified_square_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_square_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_square_gen_correct) : interp_gen_cache. + Local Opaque reified_square_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_encode_gen + SuchThat (is_reification_of reified_encode_gen encodemod) + As reified_encode_gen_correct. + Proof. + Time cache_reify (). + (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) + (* Time cache_reify_faster_2arg (). *) + Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification encodemod (proj1 reified_encode_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_encode_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_encode_gen_correct) : interp_gen_cache. + Local Opaque reified_encode_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_from_montgomery_gen + SuchThat (is_reification_of reified_from_montgomery_gen from_montgomerymod) + As reified_from_montgomery_gen_correct. + Proof. + Time cache_reify (). + (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) + (* Time cache_reify_faster_2arg (). *) + Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification from_montgomerymod (proj1 reified_from_montgomery_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_from_montgomery_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_from_montgomery_gen_correct) : interp_gen_cache. + Local Opaque reified_from_montgomery_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_zero_gen + SuchThat (is_reification_of reified_zero_gen zeromod) + As reified_zero_gen_correct. + Proof. + (* Time cache_reify (). *) + (* we do something faster *) + Time cache_reify_faster_1arg (). + Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification zeromod (proj1 reified_zero_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_zero_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_zero_gen_correct) : interp_gen_cache. + Local Opaque reified_zero_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_one_gen + SuchThat (is_reification_of reified_one_gen onemod) + As reified_one_gen_correct. + Proof. + (* Time cache_reify (). *) + (* we do something faster *) + Time cache_reify_faster_1arg (). + Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification onemod (proj1 reified_one_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_one_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_one_gen_correct) : interp_gen_cache. + Local Opaque reified_one_gen. (* needed for making [autorewrite] not take a very long time *) +End WordByWordMontgomery. -- cgit v1.2.3