diff options
-rw-r--r-- | Makefile | 21 | ||||
-rw-r--r-- | _CoqProject | 5 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 4 | ||||
-rw-r--r-- | src/Specific/IntegrationTestDisplayCommon.v | 42 | ||||
-rw-r--r-- | src/Specific/IntegrationTestLadderstep.v | 44 | ||||
-rw-r--r-- | src/Specific/IntegrationTestLadderstepDisplay.v | 4 | ||||
-rw-r--r-- | src/Specific/IntegrationTestMul.v | 19 | ||||
-rw-r--r-- | src/Specific/IntegrationTestMulDisplay.v | 4 | ||||
-rw-r--r-- | src/Specific/IntegrationTestSub.v | 19 | ||||
-rw-r--r-- | src/Specific/IntegrationTestSubDisplay.v | 4 | ||||
-rw-r--r-- | src/Specific/IntegrationTestTemporaryMiscCommon.v | 43 |
11 files changed, 124 insertions, 85 deletions
@@ -12,6 +12,7 @@ HIDE := $(if $(VERBOSE),,@) .PHONY: coq clean update-_CoqProject cleanall install \ install-coqprime clean-coqprime coqprime \ + specific-display display \ specific non-specific SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' | uniq @@ -50,11 +51,17 @@ COQ_VOFILES := $(filter-out $(UNMADE_VOFILES),$(VOFILES)) LITE_VOFILES := $(filter-out $(HEAVY_VOFILES),$(COQ_VOFILES)) SPECIFIC_VO := $(filter src/Specific/%,$(VOFILES)) NON_SPECIFIC_VO := $(filter-out $(SPECIFIC_VO),$(VO_FILES)) +SPECIFIC_DISPLAY_VO := $(filter src/Specific/%Display.vo,$(VOFILES)) +DISPLAY_VO := $(SPECIFIC_DISPLAY_VO) +DISPLAY_JAVA_VO := $(filter %JavaDisplay.vo,$(DISPLAY_VO)) +DISPLAY_NON_JAVA_VO := $(filter-out $(DISPLAY_JAVA_VO),$(DISPLAY_VO)) specific: $(SPECIFIC_VO) coqprime non-specific: $(NON_SPECIFIC_VO) coqprime coq: $(COQ_VOFILES) coqprime lite: $(LITE_VOFILES) coqprime +specific-display: $(SPECIFIC_DISPLAY_VO:.vo=.log) coqprime +display: $(DISPLAY_VO:.vo=.log) coqprime COQPRIME_FOLDER := coqprime ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5 @@ -82,13 +89,13 @@ Makefile.coq: Makefile _CoqProject $(SHOW)'COQ_MAKEFILE -f _CoqProject > $@' $(HIDE)$(COQBIN)coq_makefile -f _CoqProject | sed s'/^clean:$$/clean::/g' | sed s'/^Makefile: /Makefile-old: /g' | sed s'/^printenv:$$/printenv::/g' > $@ -#$(DISPLAY_NON_JAVA_VO:.vo=.log) : %Display.log : %.vo %Display.v src/Reflection/Z/CNotations.vo -# $(SHOW)"COQC $*Display > $@" -# $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*Display.v > $@.tmp && mv -f $@.tmp $@ -# -#$(DISPLAY_JAVA_VO:.vo=.log) : %JavaDisplay.log : %.vo %JavaDisplay.v src/Reflection/Z/JavaNotations.vo -# $(SHOW)"COQC $*JavaDisplay > $@" -# $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*JavaDisplay.v > $@.tmp && mv -f $@.tmp $@ +$(DISPLAY_NON_JAVA_VO:.vo=.log) : %Display.log : %.vo %Display.v src/Compilers/Z/CNotations.vo + $(SHOW)"COQC $*Display > $@" + $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*Display.v > $@.tmp && mv -f $@.tmp $@ + +$(DISPLAY_JAVA_VO:.vo=.log) : %JavaDisplay.log : %.vo %JavaDisplay.v src/Compilers/Z/JavaNotations.vo + $(SHOW)"COQC $*JavaDisplay > $@" + $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*JavaDisplay.v > $@.tmp && mv -f $@.tmp $@ clean:: rm -f Makefile.coq diff --git a/_CoqProject b/_CoqProject index 8d25c02b3..0ecbfc92f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -191,9 +191,14 @@ src/Spec/MxDH.v src/Spec/WeierstrassCurve.v src/Spec/Test/X25519.v src/Specific/ArithmeticSynthesisTest.v +src/Specific/IntegrationTestDisplayCommon.v src/Specific/IntegrationTestLadderstep.v +src/Specific/IntegrationTestLadderstepDisplay.v src/Specific/IntegrationTestMul.v +src/Specific/IntegrationTestMulDisplay.v src/Specific/IntegrationTestSub.v +src/Specific/IntegrationTestSubDisplay.v +src/Specific/IntegrationTestTemporaryMiscCommon.v src/Specific/FancyMachine256/Barrett.v src/Specific/FancyMachine256/Core.v src/Specific/FancyMachine256/Montgomery.v diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v index a04f3505c..15150eab1 100644 --- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v +++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v @@ -181,7 +181,7 @@ Definition PipelineCorrect : e_final_newtype = eq_rect _ (fun t => Expr base_type op (Arrow (pick_type input_bounds) t)) e' _ (eq_sym Hbounds_sane)) (** ** instantiation of original evar *) - (Hevar : final_e_evar = Interp (t:=Arrow _ _) Syntax.interp_op e_final_newtype v') + (Hevar : final_e_evar = InterpEta (t:=Arrow _ _) Syntax.interp_op e_final_newtype v') (** ** side condition *) (Hv : Bounds.is_bounded_by input_bounds (cast_back_flat_const v')) : Bounds.is_bounded_by given_output_bounds (fZ (cast_back_flat_const v')) @@ -196,7 +196,7 @@ Proof. clear Hwf He_unnatize_for_wf. symmetry in Hpost_correct. subst; cbv [proj1_sig] in *. - rewrite <- Hrexpr. + rewrite eq_InterpEta, <- Hrexpr. eapply PostWfPipelineCorrect in Hpost_correct; [ | solve [ eauto ].. ]. rewrite !@InterpPreWfPipeline in Hpost_correct. unshelve eapply relax_output_bounds; try eassumption; []. diff --git a/src/Specific/IntegrationTestDisplayCommon.v b/src/Specific/IntegrationTestDisplayCommon.v new file mode 100644 index 000000000..a9955ad5b --- /dev/null +++ b/src/Specific/IntegrationTestDisplayCommon.v @@ -0,0 +1,42 @@ +Require Import Crypto.Util.Sigma.Lift. +Require Import Crypto.Util.Sigma.Associativity. +Require Import Crypto.Util.Sigma.MapProjections. +Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Compilers.Z.Bounds.Interpretation. +Require Export Coq.ZArith.ZArith. +Require Export Crypto.Util.LetIn. +Require Export Crypto.Util.FixedWordSizes. +Require Export Crypto.Compilers.Z.CNotations. + +Global Arguments Pos.to_nat !_ / . + +Ltac display_helper f := + lazymatch type of f with + | forall _ : ?A, ?B + => let x := fresh "x" in + lazymatch (eval hnf in A) with + | @sig ?A ?P + => refine (fun x : A => _); + let f' := open_constr:(f (exist P x _)) in + display_helper f' + | prod ?A ?B + => let f' := open_constr:(fun (a : A) (b : B) => f (a, b)%core) in + display_helper f' + end + | _ => first [ refine (proj1_sig f) + | refine f ] + end. +Tactic Notation "display" open_constr(f) := + let do_red F := (eval cbv [proj1_sig f Lift.lift2_sig sig_eq_trans_exist1 MapProjections.proj2_sig_map Associativity.sig_sig_assoc Tuple.tuple Tuple.tuple' FixedWordSizes.wordT PeanoNat.Nat.log2 FixedWordSizes.word_case PeanoNat.Nat.log2_iter PeanoNat.Nat.pred FixedWordSizes.ZToWord FixedWordSizes.word_case_dep Bounds.bounds_to_base_type + Z.leb Z.compare Pos.compare Pos.compare_cont ZRange.lower ZRange.upper + ] in F) in + let ret := open_constr:(ltac:(display_helper (proj1_sig f))) in + let ret := do_red ret in + let ret := lazymatch ret with + | context[match ?sz with O => _ | _ => _ end] => (eval cbv [sz] in ret) + | _ => ret + end in + let ret := (eval simpl @Z.to_nat in ret) in + let ret := (eval cbv beta iota zeta in ret) in + refine ret. +Notation display f := (ltac:(let v := f in display v)) (only parsing). diff --git a/src/Specific/IntegrationTestLadderstep.v b/src/Specific/IntegrationTestLadderstep.v index f7b6665c4..34eb10c46 100644 --- a/src/Specific/IntegrationTestLadderstep.v +++ b/src/Specific/IntegrationTestLadderstep.v @@ -16,6 +16,8 @@ Require Import Crypto.Util.Tactics.SubstEvars. Require Import Crypto.Curves.Montgomery.XZ. Import ListNotations. +Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. + Require Import Crypto.Compilers.Z.Bounds.Pipeline. Section BoundedField25p5. @@ -60,48 +62,6 @@ Section BoundedField25p5. reflexivity. Defined. - Definition adjust_tuple2_tuple2_sig {A P Q} - (v : { a : { a : tuple (tuple A 2) 2 | (P (fst (fst a)) /\ P (snd (fst a))) /\ (P (fst (snd a)) /\ P (snd (snd a))) } - | Q (exist _ _ (proj1 (proj1 (proj2_sig a))), - exist _ _ (proj2 (proj1 (proj2_sig a))), - (exist _ _ (proj1 (proj2 (proj2_sig a))), - exist _ _ (proj2 (proj2 (proj2_sig a))))) }) - : { a : tuple (tuple (@sig A P) 2) 2 | Q a }. - Proof. - eexists. - exact (proj2_sig v). - Defined. - - (** TODO MOVE ME *) - (** The [eexists_sig_etransitivity] tactic takes a goal of the form - [{ a | f a = b }], and splits it into two goals, [?b' = b] and - [{ a | f a = ?b' }], where [?b'] is a fresh evar. *) - Definition sig_eq_trans_exist1 {A B} (f : A -> B) - (b b' : B) - (pf : b' = b) - (y : { a : A | f a = b' }) - : { a : A | f a = b } - := let 'exist a p := y in exist _ a (eq_trans p pf). - Ltac eexists_sig_etransitivity := - lazymatch goal with - | [ |- { a : ?A | @?f a = ?b } ] - => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in - simple refine (lem _ _) - end. - Definition sig_eq_trans_rewrite_fun_exist1 {A B} (f f' : A -> B) - (b : B) - (pf : forall a, f' a = f a) - (y : { a : A | f' a = b }) - : { a : A | f a = b } - := let 'exist a p := y in exist _ a (eq_trans (eq_sym (pf a)) p). - Ltac eexists_sig_etransitivity_for_rewrite_fun := - lazymatch goal with - | [ |- { a : ?A | @?f a = ?b } ] - => let lem := open_constr:(@sig_eq_trans_rewrite_fun_exist1 A _ f _ b) in - simple refine (lem _ _); cbv beta - end. - - (** TODO MOVE ME *) (* TODO : change this to field once field isomorphism happens *) Definition xzladderstep : { xzladderstep : feBW -> feBW -> feBW * feBW -> feBW * feBW -> feBW * feBW * (feBW * feBW) diff --git a/src/Specific/IntegrationTestLadderstepDisplay.v b/src/Specific/IntegrationTestLadderstepDisplay.v new file mode 100644 index 000000000..ce551f580 --- /dev/null +++ b/src/Specific/IntegrationTestLadderstepDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.IntegrationTestLadderstep. +Require Import Crypto.Specific.IntegrationTestDisplayCommon. + +(*Check display xzladderstep.*) diff --git a/src/Specific/IntegrationTestMul.v b/src/Specific/IntegrationTestMul.v index ec9120246..0cbc3966e 100644 --- a/src/Specific/IntegrationTestMul.v +++ b/src/Specific/IntegrationTestMul.v @@ -11,6 +11,8 @@ Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.MoveLetIn. Import ListNotations. +Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. + Require Import Crypto.Compilers.Z.Bounds.Pipeline. Section BoundedField25p5. @@ -39,23 +41,6 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x). - (** TODO MOVE ME *) - (** The [eexists_sig_etransitivity] tactic takes a goal of the form - [{ a | f a = b }], and splits it into two goals, [?b' = b] and - [{ a | f a = ?b' }], where [?b'] is a fresh evar. *) - Definition sig_eq_trans_exist1 {A B} (f : A -> B) - (b b' : B) - (pf : b' = b) - (y : { a : A | f a = b' }) - : { a : A | f a = b } - := let 'exist a p := y in exist _ a (eq_trans p pf). - Ltac eexists_sig_etransitivity := - lazymatch goal with - | [ |- { a : ?A | @?f a = ?b } ] - => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in - simple refine (lem _ _) - end. - (* TODO : change this to field once field isomorphism happens *) Definition mul : { mul : feBW -> feBW -> feBW diff --git a/src/Specific/IntegrationTestMulDisplay.v b/src/Specific/IntegrationTestMulDisplay.v new file mode 100644 index 000000000..bf6a3e1c4 --- /dev/null +++ b/src/Specific/IntegrationTestMulDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.IntegrationTestMul. +Require Import Crypto.Specific.IntegrationTestDisplayCommon. + +Check display mul. diff --git a/src/Specific/IntegrationTestSub.v b/src/Specific/IntegrationTestSub.v index a3a1e8613..3eadc371d 100644 --- a/src/Specific/IntegrationTestSub.v +++ b/src/Specific/IntegrationTestSub.v @@ -11,6 +11,8 @@ Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.MoveLetIn. Import ListNotations. +Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. + Require Import Crypto.Compilers.Z.Bounds.Pipeline. Section BoundedField25p5. @@ -39,23 +41,6 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x). - (** TODO MOVE ME *) - (** The [eexists_sig_etransitivity] tactic takes a goal of the form - [{ a | f a = b }], and splits it into two goals, [?b' = b] and - [{ a | f a = ?b' }], where [?b'] is a fresh evar. *) - Definition sig_eq_trans_exist1 {A B} (f : A -> B) - (b b' : B) - (pf : b' = b) - (y : { a : A | f a = b' }) - : { a : A | f a = b } - := let 'exist a p := y in exist _ a (eq_trans p pf). - Ltac eexists_sig_etransitivity := - lazymatch goal with - | [ |- { a : ?A | @?f a = ?b } ] - => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in - simple refine (lem _ _) - end. - (* TODO : change this to field once field isomorphism happens *) Definition sub : { sub : feBW -> feBW -> feBW diff --git a/src/Specific/IntegrationTestSubDisplay.v b/src/Specific/IntegrationTestSubDisplay.v new file mode 100644 index 000000000..9f8e5eadc --- /dev/null +++ b/src/Specific/IntegrationTestSubDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.IntegrationTestSub. +Require Import Crypto.Specific.IntegrationTestDisplayCommon. + +Check display sub. diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v new file mode 100644 index 000000000..3bf18d4e7 --- /dev/null +++ b/src/Specific/IntegrationTestTemporaryMiscCommon.v @@ -0,0 +1,43 @@ +(*** XXX TODO MOVE ALL THINGS IN THIS FILE TO BETTER PLACES *) +Require Import Crypto.Util.Tuple. + +Definition adjust_tuple2_tuple2_sig {A P Q} + (v : { a : { a : tuple (tuple A 2) 2 | (P (fst (fst a)) /\ P (snd (fst a))) /\ (P (fst (snd a)) /\ P (snd (snd a))) } + | Q (exist _ _ (proj1 (proj1 (proj2_sig a))), + exist _ _ (proj2 (proj1 (proj2_sig a))), + (exist _ _ (proj1 (proj2 (proj2_sig a))), + exist _ _ (proj2 (proj2 (proj2_sig a))))) }) + : { a : tuple (tuple (@sig A P) 2) 2 | Q a }. +Proof. + eexists. + exact (proj2_sig v). +Defined. + +(** TODO MOVE ME *) +(** The [eexists_sig_etransitivity] tactic takes a goal of the form + [{ a | f a = b }], and splits it into two goals, [?b' = b] and + [{ a | f a = ?b' }], where [?b'] is a fresh evar. *) +Definition sig_eq_trans_exist1 {A B} (f : A -> B) + (b b' : B) + (pf : b' = b) + (y : { a : A | f a = b' }) + : { a : A | f a = b } + := let 'exist a p := y in exist _ a (eq_trans p pf). +Ltac eexists_sig_etransitivity := + lazymatch goal with + | [ |- { a : ?A | @?f a = ?b } ] + => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in + simple refine (lem _ _) + end. +Definition sig_eq_trans_rewrite_fun_exist1 {A B} (f f' : A -> B) + (b : B) + (pf : forall a, f' a = f a) + (y : { a : A | f' a = b }) + : { a : A | f a = b } + := let 'exist a p := y in exist _ a (eq_trans (eq_sym (pf a)) p). +Ltac eexists_sig_etransitivity_for_rewrite_fun := + lazymatch goal with + | [ |- { a : ?A | @?f a = ?b } ] + => let lem := open_constr:(@sig_eq_trans_rewrite_fun_exist1 A _ f _ b) in + simple refine (lem _ _); cbv beta + end. |