From 13c5d20a62f276ef51f0d766d4e3a60ad5c5c410 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 22 Nov 2016 23:30:30 -0500 Subject: Copy bounds, fix a typo --- src/SpecificGen/GF2213_32BoundedAddCoordinates.v | 77 ++++++++++++++++++++++ .../GF2213_32BoundedExtendedAddCoordinates.v | 67 +++++++++++++++++++ src/SpecificGen/GF2213_32Reflective/Common.v | 77 ++++++++++++++-------- .../GF2213_32ReflectiveAddCoordinates.v | 76 +++++++++++++++++++++ src/SpecificGen/GF2519_32BoundedAddCoordinates.v | 77 ++++++++++++++++++++++ .../GF2519_32BoundedExtendedAddCoordinates.v | 67 +++++++++++++++++++ src/SpecificGen/GF2519_32Reflective/Common.v | 77 ++++++++++++++-------- .../GF2519_32ReflectiveAddCoordinates.v | 76 +++++++++++++++++++++ src/SpecificGen/GF25519_32BoundedAddCoordinates.v | 77 ++++++++++++++++++++++ .../GF25519_32BoundedExtendedAddCoordinates.v | 67 +++++++++++++++++++ src/SpecificGen/GF25519_32Reflective/Common.v | 77 ++++++++++++++-------- .../GF25519_32ReflectiveAddCoordinates.v | 76 +++++++++++++++++++++ src/SpecificGen/GF25519_64BoundedAddCoordinates.v | 77 ++++++++++++++++++++++ .../GF25519_64BoundedExtendedAddCoordinates.v | 67 +++++++++++++++++++ src/SpecificGen/GF25519_64Reflective/Common.v | 77 ++++++++++++++-------- .../GF25519_64ReflectiveAddCoordinates.v | 76 +++++++++++++++++++++ src/SpecificGen/GF41417_32BoundedAddCoordinates.v | 77 ++++++++++++++++++++++ .../GF41417_32BoundedExtendedAddCoordinates.v | 67 +++++++++++++++++++ src/SpecificGen/GF41417_32Reflective/Common.v | 77 ++++++++++++++-------- .../GF41417_32ReflectiveAddCoordinates.v | 76 +++++++++++++++++++++ src/SpecificGen/GF5211_32BoundedAddCoordinates.v | 77 ++++++++++++++++++++++ .../GF5211_32BoundedExtendedAddCoordinates.v | 67 +++++++++++++++++++ src/SpecificGen/GF5211_32Reflective/Common.v | 77 ++++++++++++++-------- .../GF5211_32ReflectiveAddCoordinates.v | 76 +++++++++++++++++++++ 24 files changed, 1620 insertions(+), 162 deletions(-) create mode 100644 src/SpecificGen/GF2213_32BoundedAddCoordinates.v create mode 100644 src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v create mode 100644 src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v create mode 100644 src/SpecificGen/GF2519_32BoundedAddCoordinates.v create mode 100644 src/SpecificGen/GF2519_32BoundedExtendedAddCoordinates.v create mode 100644 src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v create mode 100644 src/SpecificGen/GF25519_32BoundedAddCoordinates.v create mode 100644 src/SpecificGen/GF25519_32BoundedExtendedAddCoordinates.v create mode 100644 src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v create mode 100644 src/SpecificGen/GF25519_64BoundedAddCoordinates.v create mode 100644 src/SpecificGen/GF25519_64BoundedExtendedAddCoordinates.v create mode 100644 src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v create mode 100644 src/SpecificGen/GF41417_32BoundedAddCoordinates.v create mode 100644 src/SpecificGen/GF41417_32BoundedExtendedAddCoordinates.v create mode 100644 src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v create mode 100644 src/SpecificGen/GF5211_32BoundedAddCoordinates.v create mode 100644 src/SpecificGen/GF5211_32BoundedExtendedAddCoordinates.v create mode 100644 src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v (limited to 'src/SpecificGen') diff --git a/src/SpecificGen/GF2213_32BoundedAddCoordinates.v b/src/SpecificGen/GF2213_32BoundedAddCoordinates.v new file mode 100644 index 000000000..6079aadc9 --- /dev/null +++ b/src/SpecificGen/GF2213_32BoundedAddCoordinates.v @@ -0,0 +1,77 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.SpecificGen.GF2213_32. +Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. +Require Import Crypto.SpecificGen.GF2213_32ReflectiveAddCoordinates. +Require Import Crypto.Util.LetIn. +Local Open Scope Z. + +Local Ltac bounded_t opW blem := + apply blem; apply is_bounded_proj1_fe2213_32. + +Local Ltac define_binop f g opW blem := + refine (exist_fe2213_32W (opW (proj1_fe2213_32W f) (proj1_fe2213_32W g)) _); + abstract bounded_t opW blem. + +Local Opaque Let_In. +Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64. +Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _. +Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2213_32W) : Tuple.tuple fe2213_32W 4 + := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8. + +Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb := + change opW with (interp_rop); + rewrite pre_rewrite; + intros; apply rop_cb; assumption. + +Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates. +Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed. + +Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem := + refine (let ts := opW (proj1_fe2213_32W x0) + (proj1_fe2213_32W x1) + (proj1_fe2213_32W x2) + (proj1_fe2213_32W x3) + (proj1_fe2213_32W x4) + (proj1_fe2213_32W x5) + (proj1_fe2213_32W x6) + (proj1_fe2213_32W x7) + (proj1_fe2213_32W x8) in + HList.mapt exist_fe2213_32W (ts:=ts) _); + abstract ( + rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe2213_32WToZ)); + apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe2213_32 + ). +Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2213_32) : Tuple.tuple fe2213_32 4. +Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined. + +Local Ltac op_correct_t op opW_correct_and_bounded := + cbv [op]; + rewrite ?HList.map_mapt; + lazymatch goal with + | [ |- context[proj1_fe2213_32 (exist_fe2213_32W _ _)] ] + => rewrite proj1_fe2213_32_exist_fe2213_32W || setoid_rewrite proj1_fe2213_32_exist_fe2213_32W + | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ] + => rewrite proj1_wire_digits_exist_wire_digitsW + | _ => idtac + end; + rewrite <- ?HList.map_is_mapt; + apply opW_correct_and_bounded; + lazymatch goal with + | [ |- is_bounded _ = true ] + => apply is_bounded_proj1_fe2213_32 + | [ |- wire_digits_is_bounded _ = true ] + => apply is_bounded_proj1_wire_digits + end. + +Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2213_32) + : Tuple.map (n:=4) proj1_fe2213_32 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8) + = Reified.AddCoordinates.add_coordinates (proj1_fe2213_32 x0) + (proj1_fe2213_32 x1) + (proj1_fe2213_32 x2) + (proj1_fe2213_32 x3) + (proj1_fe2213_32 x4) + (proj1_fe2213_32 x5) + (proj1_fe2213_32 x6) + (proj1_fe2213_32 x7) + (proj1_fe2213_32 x8). +Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed. diff --git a/src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v new file mode 100644 index 000000000..58c297578 --- /dev/null +++ b/src/SpecificGen/GF2213_32BoundedExtendedAddCoordinates.v @@ -0,0 +1,67 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.SpecificGen.GF2213_32Bounded. +Require Import Crypto.SpecificGen.GF2213_32ExtendedAddCoordinates. +Require Import Crypto.SpecificGen.GF2213_32BoundedAddCoordinates. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. + +Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23 + : Tuple.fieldwise + (n:=4) GF2213_32BoundedCommon.eq + (@GF2213_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23) + (@ExtendedCoordinates.Extended.add_coordinates + GF2213_32BoundedCommon.fe2213_32 + GF2213_32Bounded.add GF2213_32Bounded.sub GF2213_32Bounded.mul twice_d + (P10, P11, P12, P13) (P20, P21, P22, P23)). +Proof. + unfold GF2213_32BoundedCommon.eq. + apply -> (fieldwise_map_iff (n:=4) eq GF2213_32BoundedCommon.proj1_fe2213_32 GF2213_32BoundedCommon.proj1_fe2213_32). + rewrite add_coordinates_correct. + cbv [AddCoordinates.add_coordinates]. + setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry. + unfold edwards_extended_carry_add_coordinates. + match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end. + apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF2213_32BoundedCommon.proj1_fe2213_32). + apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero; + intros; + repeat match goal with + | [ |- context[add _ _] ] + => rewrite add_correct + | [ |- context[sub _ _] ] + => rewrite sub_correct + | [ |- context[mul _ _] ] + => rewrite mul_correct + | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in * + | [ |- and _ _ ] => split + | [ |- ?x = ?x ] => reflexivity + | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct + | _ => congruence + end. +Qed. + +Definition add_coordinates' twice_d P1 P2 + := let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF2213_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Definition add_coordinates twice_d P1 P2 + := Eval cbv beta iota delta [GF2213_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in + let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF2213_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Lemma add_coordinates_correct_full twice_d P1 P2 + : Tuple.fieldwise + GF2213_32BoundedCommon.eq + (add_coordinates twice_d P1 P2) + (@ExtendedCoordinates.Extended.add_coordinates + GF2213_32BoundedCommon.fe2213_32 + GF2213_32Bounded.add GF2213_32Bounded.sub GF2213_32Bounded.mul twice_d P1 P2). +Proof. + destruct_head' prod. + rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity. +Qed. diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v index ea4539963..52f488f2e 100644 --- a/src/SpecificGen/GF2213_32Reflective/Common.v +++ b/src/SpecificGen/GF2213_32Reflective/Common.v @@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op := let T := (type of uncurried_op) in make_type_from' T. -Definition ExprBinOpT : type base_type. -Proof. make_type_from (uncurry_binop_fe2213_32 carry_add). Defined. -Definition ExprUnOpT : type base_type. -Proof. make_type_from (uncurry_unop_fe2213_32 carry_opp). Defined. +Definition fe2213_32T : flat_type base_type. +Proof. + let T := (eval compute in GF2213_32.fe2213_32) in + let T := reify_flat_type T in + exact T. +Defined. +Definition Expr_n_OpT (count_out : nat) : flat_type base_type + := Eval cbv [Syntax.tuple Syntax.tuple' fe2213_32T] in + Syntax.tuple fe2213_32T count_out. +Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type + := match count_in with + | 0 => Expr_n_OpT count_out + | S n => SmartArrow base_type fe2213_32T (Expr_nm_OpT n count_out) + end. +Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1. +Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1. Definition ExprUnOpFEToZT : type base_type. Proof. make_type_from (uncurry_unop_fe2213_32 ge_modulus). Defined. Definition ExprUnOpWireToFET : type base_type. Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined. Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe2213_32 pack). Defined. -Definition Expr4OpT : type base_type. -Proof. - let T := lazymatch type of (apply4_nd - (B:=GF2213_32.fe2213_32) - (@uncurry_unop_fe2213_32)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. -Definition Expr9_4OpT : type base_type. -Proof. - let T := lazymatch type of (apply9_nd - (B:=Tuple.tuple GF2213_32.fe2213_32 4) - (@uncurry_unop_fe2213_32)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. +Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. +Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type Definition ExprArgWireRevT : flat_type base_type := Eval compute in all_binders_for ExprUnOpWireToFET. Definition ExprZ : Type := Expr (Tbase TZ). -Definition ExprBinOp : Type := Expr ExprBinOpT. -Definition ExprUnOp : Type := Expr ExprUnOpT. Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT. Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET. Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT. +Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out). +Definition ExprBinOp : Type := Expr ExprBinOpT. +Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). +Definition expr_nm_Op count_in count_out interp_base_type var : Type + := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. +Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. +Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. +Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Local Ltac bounds_from_list_cps ls := + lazymatch (eval hnf in ls) with + | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra)) + | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in + constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra)) + end. + +Local Ltac make_bounds_cps ls := + let v := bounds_from_list_cps (List.rev ls) in + let v := (eval compute in v) in + pose v. + Local Ltac bounds_from_list ls := lazymatch (eval hnf in ls) with | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}) @@ -105,6 +116,18 @@ Local Ltac make_bounds ls := let v := (eval compute in v) in exact v. +(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type. +Proof. + refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with + | 0 => tt + | S n => let v := Expr_nm_Op_bounds n count_out in + _ + end; simpl. + make_bounds_cps (Tuple.to_list _ bounds). + pose (p _ v). + repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]). + exact p0. +*) Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined. Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type. diff --git a/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v new file mode 100644 index 000000000..3b95ae5c4 --- /dev/null +++ b/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v @@ -0,0 +1,76 @@ +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Export Crypto.SpecificGen.GF2213_32. +Require Import Crypto.SpecificGen.GF2213_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Reflection.Z.Interpretations64. +Require Crypto.Reflection.Z.Interpretations64.Relations. +Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. +Require Import Crypto.Reflection.Z.Reify. +Require Import Crypto.Reflection.Z.Syntax. +Require Import Crypto.SpecificGen.GF2213_32Reflective.Common. +Require Import Crypto.SpecificGen.GF2213_32Reflective.Reified.AddCoordinates. +Require Import Bedrock.Word Crypto.Util.WordUtil. +Require Import Coq.Lists.List Crypto.Util.ListUtil. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Algebra. +Import ListNotations. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Local Open Scope Z. + +Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW. + +Declare Reduction asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW curry_9op_fe2213_32W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. +Ltac asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe2213_32W curry_unop_fe2213_32W curry_unop_wire_digitsW curry_9op_fe2213_32W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + Interp interp interp_flat_type interpf interp_flat_type fst snd]. + + +Time Definition interp_radd_coordinates : SpecificGen.GF2213_32BoundedCommon.fe2213_32W + -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W + -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W + -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W + -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W + -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W + -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W + -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W + -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W + -> Tuple.tuple SpecificGen.GF2213_32BoundedCommon.fe2213_32W 4 + := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). +(*Print interp_radd_coordinates.*) +Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. + +Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates. +Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed. diff --git a/src/SpecificGen/GF2519_32BoundedAddCoordinates.v b/src/SpecificGen/GF2519_32BoundedAddCoordinates.v new file mode 100644 index 000000000..68b97f000 --- /dev/null +++ b/src/SpecificGen/GF2519_32BoundedAddCoordinates.v @@ -0,0 +1,77 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.SpecificGen.GF2519_32. +Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. +Require Import Crypto.SpecificGen.GF2519_32ReflectiveAddCoordinates. +Require Import Crypto.Util.LetIn. +Local Open Scope Z. + +Local Ltac bounded_t opW blem := + apply blem; apply is_bounded_proj1_fe2519_32. + +Local Ltac define_binop f g opW blem := + refine (exist_fe2519_32W (opW (proj1_fe2519_32W f) (proj1_fe2519_32W g)) _); + abstract bounded_t opW blem. + +Local Opaque Let_In. +Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64. +Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _. +Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2519_32W) : Tuple.tuple fe2519_32W 4 + := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8. + +Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb := + change opW with (interp_rop); + rewrite pre_rewrite; + intros; apply rop_cb; assumption. + +Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates. +Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed. + +Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem := + refine (let ts := opW (proj1_fe2519_32W x0) + (proj1_fe2519_32W x1) + (proj1_fe2519_32W x2) + (proj1_fe2519_32W x3) + (proj1_fe2519_32W x4) + (proj1_fe2519_32W x5) + (proj1_fe2519_32W x6) + (proj1_fe2519_32W x7) + (proj1_fe2519_32W x8) in + HList.mapt exist_fe2519_32W (ts:=ts) _); + abstract ( + rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe2519_32WToZ)); + apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe2519_32 + ). +Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2519_32) : Tuple.tuple fe2519_32 4. +Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined. + +Local Ltac op_correct_t op opW_correct_and_bounded := + cbv [op]; + rewrite ?HList.map_mapt; + lazymatch goal with + | [ |- context[proj1_fe2519_32 (exist_fe2519_32W _ _)] ] + => rewrite proj1_fe2519_32_exist_fe2519_32W || setoid_rewrite proj1_fe2519_32_exist_fe2519_32W + | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ] + => rewrite proj1_wire_digits_exist_wire_digitsW + | _ => idtac + end; + rewrite <- ?HList.map_is_mapt; + apply opW_correct_and_bounded; + lazymatch goal with + | [ |- is_bounded _ = true ] + => apply is_bounded_proj1_fe2519_32 + | [ |- wire_digits_is_bounded _ = true ] + => apply is_bounded_proj1_wire_digits + end. + +Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe2519_32) + : Tuple.map (n:=4) proj1_fe2519_32 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8) + = Reified.AddCoordinates.add_coordinates (proj1_fe2519_32 x0) + (proj1_fe2519_32 x1) + (proj1_fe2519_32 x2) + (proj1_fe2519_32 x3) + (proj1_fe2519_32 x4) + (proj1_fe2519_32 x5) + (proj1_fe2519_32 x6) + (proj1_fe2519_32 x7) + (proj1_fe2519_32 x8). +Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed. diff --git a/src/SpecificGen/GF2519_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF2519_32BoundedExtendedAddCoordinates.v new file mode 100644 index 000000000..309a62324 --- /dev/null +++ b/src/SpecificGen/GF2519_32BoundedExtendedAddCoordinates.v @@ -0,0 +1,67 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.SpecificGen.GF2519_32Bounded. +Require Import Crypto.SpecificGen.GF2519_32ExtendedAddCoordinates. +Require Import Crypto.SpecificGen.GF2519_32BoundedAddCoordinates. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. + +Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23 + : Tuple.fieldwise + (n:=4) GF2519_32BoundedCommon.eq + (@GF2519_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23) + (@ExtendedCoordinates.Extended.add_coordinates + GF2519_32BoundedCommon.fe2519_32 + GF2519_32Bounded.add GF2519_32Bounded.sub GF2519_32Bounded.mul twice_d + (P10, P11, P12, P13) (P20, P21, P22, P23)). +Proof. + unfold GF2519_32BoundedCommon.eq. + apply -> (fieldwise_map_iff (n:=4) eq GF2519_32BoundedCommon.proj1_fe2519_32 GF2519_32BoundedCommon.proj1_fe2519_32). + rewrite add_coordinates_correct. + cbv [AddCoordinates.add_coordinates]. + setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry. + unfold edwards_extended_carry_add_coordinates. + match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end. + apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF2519_32BoundedCommon.proj1_fe2519_32). + apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero; + intros; + repeat match goal with + | [ |- context[add _ _] ] + => rewrite add_correct + | [ |- context[sub _ _] ] + => rewrite sub_correct + | [ |- context[mul _ _] ] + => rewrite mul_correct + | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in * + | [ |- and _ _ ] => split + | [ |- ?x = ?x ] => reflexivity + | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct + | _ => congruence + end. +Qed. + +Definition add_coordinates' twice_d P1 P2 + := let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF2519_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Definition add_coordinates twice_d P1 P2 + := Eval cbv beta iota delta [GF2519_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in + let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF2519_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Lemma add_coordinates_correct_full twice_d P1 P2 + : Tuple.fieldwise + GF2519_32BoundedCommon.eq + (add_coordinates twice_d P1 P2) + (@ExtendedCoordinates.Extended.add_coordinates + GF2519_32BoundedCommon.fe2519_32 + GF2519_32Bounded.add GF2519_32Bounded.sub GF2519_32Bounded.mul twice_d P1 P2). +Proof. + destruct_head' prod. + rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity. +Qed. diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v index d23856c4b..4be893f8f 100644 --- a/src/SpecificGen/GF2519_32Reflective/Common.v +++ b/src/SpecificGen/GF2519_32Reflective/Common.v @@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op := let T := (type of uncurried_op) in make_type_from' T. -Definition ExprBinOpT : type base_type. -Proof. make_type_from (uncurry_binop_fe2519_32 carry_add). Defined. -Definition ExprUnOpT : type base_type. -Proof. make_type_from (uncurry_unop_fe2519_32 carry_opp). Defined. +Definition fe2519_32T : flat_type base_type. +Proof. + let T := (eval compute in GF2519_32.fe2519_32) in + let T := reify_flat_type T in + exact T. +Defined. +Definition Expr_n_OpT (count_out : nat) : flat_type base_type + := Eval cbv [Syntax.tuple Syntax.tuple' fe2519_32T] in + Syntax.tuple fe2519_32T count_out. +Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type + := match count_in with + | 0 => Expr_n_OpT count_out + | S n => SmartArrow base_type fe2519_32T (Expr_nm_OpT n count_out) + end. +Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1. +Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1. Definition ExprUnOpFEToZT : type base_type. Proof. make_type_from (uncurry_unop_fe2519_32 ge_modulus). Defined. Definition ExprUnOpWireToFET : type base_type. Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined. Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe2519_32 pack). Defined. -Definition Expr4OpT : type base_type. -Proof. - let T := lazymatch type of (apply4_nd - (B:=GF2519_32.fe2519_32) - (@uncurry_unop_fe2519_32)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. -Definition Expr9_4OpT : type base_type. -Proof. - let T := lazymatch type of (apply9_nd - (B:=Tuple.tuple GF2519_32.fe2519_32 4) - (@uncurry_unop_fe2519_32)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. +Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. +Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type Definition ExprArgWireRevT : flat_type base_type := Eval compute in all_binders_for ExprUnOpWireToFET. Definition ExprZ : Type := Expr (Tbase TZ). -Definition ExprBinOp : Type := Expr ExprBinOpT. -Definition ExprUnOp : Type := Expr ExprUnOpT. Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT. Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET. Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT. +Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out). +Definition ExprBinOp : Type := Expr ExprBinOpT. +Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). +Definition expr_nm_Op count_in count_out interp_base_type var : Type + := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. +Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. +Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. +Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Local Ltac bounds_from_list_cps ls := + lazymatch (eval hnf in ls) with + | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra)) + | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in + constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra)) + end. + +Local Ltac make_bounds_cps ls := + let v := bounds_from_list_cps (List.rev ls) in + let v := (eval compute in v) in + pose v. + Local Ltac bounds_from_list ls := lazymatch (eval hnf in ls) with | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}) @@ -105,6 +116,18 @@ Local Ltac make_bounds ls := let v := (eval compute in v) in exact v. +(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type. +Proof. + refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with + | 0 => tt + | S n => let v := Expr_nm_Op_bounds n count_out in + _ + end; simpl. + make_bounds_cps (Tuple.to_list _ bounds). + pose (p _ v). + repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]). + exact p0. +*) Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined. Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type. diff --git a/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v new file mode 100644 index 000000000..a400a893a --- /dev/null +++ b/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v @@ -0,0 +1,76 @@ +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Export Crypto.SpecificGen.GF2519_32. +Require Import Crypto.SpecificGen.GF2519_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Reflection.Z.Interpretations64. +Require Crypto.Reflection.Z.Interpretations64.Relations. +Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. +Require Import Crypto.Reflection.Z.Reify. +Require Import Crypto.Reflection.Z.Syntax. +Require Import Crypto.SpecificGen.GF2519_32Reflective.Common. +Require Import Crypto.SpecificGen.GF2519_32Reflective.Reified.AddCoordinates. +Require Import Bedrock.Word Crypto.Util.WordUtil. +Require Import Coq.Lists.List Crypto.Util.ListUtil. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Algebra. +Import ListNotations. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Local Open Scope Z. + +Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW. + +Declare Reduction asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe2519_32W curry_unop_fe2519_32W curry_unop_wire_digitsW curry_9op_fe2519_32W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. +Ltac asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe2519_32W curry_unop_fe2519_32W curry_unop_wire_digitsW curry_9op_fe2519_32W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + Interp interp interp_flat_type interpf interp_flat_type fst snd]. + + +Time Definition interp_radd_coordinates : SpecificGen.GF2519_32BoundedCommon.fe2519_32W + -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W + -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W + -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W + -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W + -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W + -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W + -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W + -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W + -> Tuple.tuple SpecificGen.GF2519_32BoundedCommon.fe2519_32W 4 + := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). +(*Print interp_radd_coordinates.*) +Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. + +Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates. +Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed. diff --git a/src/SpecificGen/GF25519_32BoundedAddCoordinates.v b/src/SpecificGen/GF25519_32BoundedAddCoordinates.v new file mode 100644 index 000000000..5a1fd12b3 --- /dev/null +++ b/src/SpecificGen/GF25519_32BoundedAddCoordinates.v @@ -0,0 +1,77 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.SpecificGen.GF25519_32. +Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. +Require Import Crypto.SpecificGen.GF25519_32ReflectiveAddCoordinates. +Require Import Crypto.Util.LetIn. +Local Open Scope Z. + +Local Ltac bounded_t opW blem := + apply blem; apply is_bounded_proj1_fe25519_32. + +Local Ltac define_binop f g opW blem := + refine (exist_fe25519_32W (opW (proj1_fe25519_32W f) (proj1_fe25519_32W g)) _); + abstract bounded_t opW blem. + +Local Opaque Let_In. +Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64. +Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _. +Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_32W) : Tuple.tuple fe25519_32W 4 + := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8. + +Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb := + change opW with (interp_rop); + rewrite pre_rewrite; + intros; apply rop_cb; assumption. + +Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates. +Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed. + +Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem := + refine (let ts := opW (proj1_fe25519_32W x0) + (proj1_fe25519_32W x1) + (proj1_fe25519_32W x2) + (proj1_fe25519_32W x3) + (proj1_fe25519_32W x4) + (proj1_fe25519_32W x5) + (proj1_fe25519_32W x6) + (proj1_fe25519_32W x7) + (proj1_fe25519_32W x8) in + HList.mapt exist_fe25519_32W (ts:=ts) _); + abstract ( + rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe25519_32WToZ)); + apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe25519_32 + ). +Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_32) : Tuple.tuple fe25519_32 4. +Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined. + +Local Ltac op_correct_t op opW_correct_and_bounded := + cbv [op]; + rewrite ?HList.map_mapt; + lazymatch goal with + | [ |- context[proj1_fe25519_32 (exist_fe25519_32W _ _)] ] + => rewrite proj1_fe25519_32_exist_fe25519_32W || setoid_rewrite proj1_fe25519_32_exist_fe25519_32W + | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ] + => rewrite proj1_wire_digits_exist_wire_digitsW + | _ => idtac + end; + rewrite <- ?HList.map_is_mapt; + apply opW_correct_and_bounded; + lazymatch goal with + | [ |- is_bounded _ = true ] + => apply is_bounded_proj1_fe25519_32 + | [ |- wire_digits_is_bounded _ = true ] + => apply is_bounded_proj1_wire_digits + end. + +Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_32) + : Tuple.map (n:=4) proj1_fe25519_32 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8) + = Reified.AddCoordinates.add_coordinates (proj1_fe25519_32 x0) + (proj1_fe25519_32 x1) + (proj1_fe25519_32 x2) + (proj1_fe25519_32 x3) + (proj1_fe25519_32 x4) + (proj1_fe25519_32 x5) + (proj1_fe25519_32 x6) + (proj1_fe25519_32 x7) + (proj1_fe25519_32 x8). +Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed. diff --git a/src/SpecificGen/GF25519_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF25519_32BoundedExtendedAddCoordinates.v new file mode 100644 index 000000000..c23bcea4a --- /dev/null +++ b/src/SpecificGen/GF25519_32BoundedExtendedAddCoordinates.v @@ -0,0 +1,67 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.SpecificGen.GF25519_32Bounded. +Require Import Crypto.SpecificGen.GF25519_32ExtendedAddCoordinates. +Require Import Crypto.SpecificGen.GF25519_32BoundedAddCoordinates. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. + +Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23 + : Tuple.fieldwise + (n:=4) GF25519_32BoundedCommon.eq + (@GF25519_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23) + (@ExtendedCoordinates.Extended.add_coordinates + GF25519_32BoundedCommon.fe25519_32 + GF25519_32Bounded.add GF25519_32Bounded.sub GF25519_32Bounded.mul twice_d + (P10, P11, P12, P13) (P20, P21, P22, P23)). +Proof. + unfold GF25519_32BoundedCommon.eq. + apply -> (fieldwise_map_iff (n:=4) eq GF25519_32BoundedCommon.proj1_fe25519_32 GF25519_32BoundedCommon.proj1_fe25519_32). + rewrite add_coordinates_correct. + cbv [AddCoordinates.add_coordinates]. + setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry. + unfold edwards_extended_carry_add_coordinates. + match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end. + apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF25519_32BoundedCommon.proj1_fe25519_32). + apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero; + intros; + repeat match goal with + | [ |- context[add _ _] ] + => rewrite add_correct + | [ |- context[sub _ _] ] + => rewrite sub_correct + | [ |- context[mul _ _] ] + => rewrite mul_correct + | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in * + | [ |- and _ _ ] => split + | [ |- ?x = ?x ] => reflexivity + | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct + | _ => congruence + end. +Qed. + +Definition add_coordinates' twice_d P1 P2 + := let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF25519_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Definition add_coordinates twice_d P1 P2 + := Eval cbv beta iota delta [GF25519_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in + let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF25519_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Lemma add_coordinates_correct_full twice_d P1 P2 + : Tuple.fieldwise + GF25519_32BoundedCommon.eq + (add_coordinates twice_d P1 P2) + (@ExtendedCoordinates.Extended.add_coordinates + GF25519_32BoundedCommon.fe25519_32 + GF25519_32Bounded.add GF25519_32Bounded.sub GF25519_32Bounded.mul twice_d P1 P2). +Proof. + destruct_head' prod. + rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity. +Qed. diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v index 4801c64fd..3389f908a 100644 --- a/src/SpecificGen/GF25519_32Reflective/Common.v +++ b/src/SpecificGen/GF25519_32Reflective/Common.v @@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op := let T := (type of uncurried_op) in make_type_from' T. -Definition ExprBinOpT : type base_type. -Proof. make_type_from (uncurry_binop_fe25519_32 carry_add). Defined. -Definition ExprUnOpT : type base_type. -Proof. make_type_from (uncurry_unop_fe25519_32 carry_opp). Defined. +Definition fe25519_32T : flat_type base_type. +Proof. + let T := (eval compute in GF25519_32.fe25519_32) in + let T := reify_flat_type T in + exact T. +Defined. +Definition Expr_n_OpT (count_out : nat) : flat_type base_type + := Eval cbv [Syntax.tuple Syntax.tuple' fe25519_32T] in + Syntax.tuple fe25519_32T count_out. +Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type + := match count_in with + | 0 => Expr_n_OpT count_out + | S n => SmartArrow base_type fe25519_32T (Expr_nm_OpT n count_out) + end. +Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1. +Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1. Definition ExprUnOpFEToZT : type base_type. Proof. make_type_from (uncurry_unop_fe25519_32 ge_modulus). Defined. Definition ExprUnOpWireToFET : type base_type. Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined. Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe25519_32 pack). Defined. -Definition Expr4OpT : type base_type. -Proof. - let T := lazymatch type of (apply4_nd - (B:=GF25519_32.fe25519_32) - (@uncurry_unop_fe25519_32)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. -Definition Expr9_4OpT : type base_type. -Proof. - let T := lazymatch type of (apply9_nd - (B:=Tuple.tuple GF25519_32.fe25519_32 4) - (@uncurry_unop_fe25519_32)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. +Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. +Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type Definition ExprArgWireRevT : flat_type base_type := Eval compute in all_binders_for ExprUnOpWireToFET. Definition ExprZ : Type := Expr (Tbase TZ). -Definition ExprBinOp : Type := Expr ExprBinOpT. -Definition ExprUnOp : Type := Expr ExprUnOpT. Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT. Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET. Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT. +Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out). +Definition ExprBinOp : Type := Expr ExprBinOpT. +Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). +Definition expr_nm_Op count_in count_out interp_base_type var : Type + := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. +Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. +Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. +Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Local Ltac bounds_from_list_cps ls := + lazymatch (eval hnf in ls) with + | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra)) + | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in + constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra)) + end. + +Local Ltac make_bounds_cps ls := + let v := bounds_from_list_cps (List.rev ls) in + let v := (eval compute in v) in + pose v. + Local Ltac bounds_from_list ls := lazymatch (eval hnf in ls) with | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}) @@ -105,6 +116,18 @@ Local Ltac make_bounds ls := let v := (eval compute in v) in exact v. +(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type. +Proof. + refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with + | 0 => tt + | S n => let v := Expr_nm_Op_bounds n count_out in + _ + end; simpl. + make_bounds_cps (Tuple.to_list _ bounds). + pose (p _ v). + repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]). + exact p0. +*) Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined. Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type. diff --git a/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v new file mode 100644 index 000000000..b13c07f44 --- /dev/null +++ b/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v @@ -0,0 +1,76 @@ +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Export Crypto.SpecificGen.GF25519_32. +Require Import Crypto.SpecificGen.GF25519_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Reflection.Z.Interpretations64. +Require Crypto.Reflection.Z.Interpretations64.Relations. +Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. +Require Import Crypto.Reflection.Z.Reify. +Require Import Crypto.Reflection.Z.Syntax. +Require Import Crypto.SpecificGen.GF25519_32Reflective.Common. +Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.AddCoordinates. +Require Import Bedrock.Word Crypto.Util.WordUtil. +Require Import Coq.Lists.List Crypto.Util.ListUtil. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Algebra. +Import ListNotations. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Local Open Scope Z. + +Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW. + +Declare Reduction asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe25519_32W curry_unop_fe25519_32W curry_unop_wire_digitsW curry_9op_fe25519_32W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. +Ltac asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe25519_32W curry_unop_fe25519_32W curry_unop_wire_digitsW curry_9op_fe25519_32W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + Interp interp interp_flat_type interpf interp_flat_type fst snd]. + + +Time Definition interp_radd_coordinates : SpecificGen.GF25519_32BoundedCommon.fe25519_32W + -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W + -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W + -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W + -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W + -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W + -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W + -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W + -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W + -> Tuple.tuple SpecificGen.GF25519_32BoundedCommon.fe25519_32W 4 + := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). +(*Print interp_radd_coordinates.*) +Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. + +Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates. +Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed. diff --git a/src/SpecificGen/GF25519_64BoundedAddCoordinates.v b/src/SpecificGen/GF25519_64BoundedAddCoordinates.v new file mode 100644 index 000000000..a1ba335c8 --- /dev/null +++ b/src/SpecificGen/GF25519_64BoundedAddCoordinates.v @@ -0,0 +1,77 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.SpecificGen.GF25519_64. +Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. +Require Import Crypto.SpecificGen.GF25519_64ReflectiveAddCoordinates. +Require Import Crypto.Util.LetIn. +Local Open Scope Z. + +Local Ltac bounded_t opW blem := + apply blem; apply is_bounded_proj1_fe25519_64. + +Local Ltac define_binop f g opW blem := + refine (exist_fe25519_64W (opW (proj1_fe25519_64W f) (proj1_fe25519_64W g)) _); + abstract bounded_t opW blem. + +Local Opaque Let_In. +Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord128. +Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _. +Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_64W) : Tuple.tuple fe25519_64W 4 + := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8. + +Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb := + change opW with (interp_rop); + rewrite pre_rewrite; + intros; apply rop_cb; assumption. + +Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates. +Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed. + +Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem := + refine (let ts := opW (proj1_fe25519_64W x0) + (proj1_fe25519_64W x1) + (proj1_fe25519_64W x2) + (proj1_fe25519_64W x3) + (proj1_fe25519_64W x4) + (proj1_fe25519_64W x5) + (proj1_fe25519_64W x6) + (proj1_fe25519_64W x7) + (proj1_fe25519_64W x8) in + HList.mapt exist_fe25519_64W (ts:=ts) _); + abstract ( + rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe25519_64WToZ)); + apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe25519_64 + ). +Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_64) : Tuple.tuple fe25519_64 4. +Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined. + +Local Ltac op_correct_t op opW_correct_and_bounded := + cbv [op]; + rewrite ?HList.map_mapt; + lazymatch goal with + | [ |- context[proj1_fe25519_64 (exist_fe25519_64W _ _)] ] + => rewrite proj1_fe25519_64_exist_fe25519_64W || setoid_rewrite proj1_fe25519_64_exist_fe25519_64W + | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ] + => rewrite proj1_wire_digits_exist_wire_digitsW + | _ => idtac + end; + rewrite <- ?HList.map_is_mapt; + apply opW_correct_and_bounded; + lazymatch goal with + | [ |- is_bounded _ = true ] + => apply is_bounded_proj1_fe25519_64 + | [ |- wire_digits_is_bounded _ = true ] + => apply is_bounded_proj1_wire_digits + end. + +Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_64) + : Tuple.map (n:=4) proj1_fe25519_64 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8) + = Reified.AddCoordinates.add_coordinates (proj1_fe25519_64 x0) + (proj1_fe25519_64 x1) + (proj1_fe25519_64 x2) + (proj1_fe25519_64 x3) + (proj1_fe25519_64 x4) + (proj1_fe25519_64 x5) + (proj1_fe25519_64 x6) + (proj1_fe25519_64 x7) + (proj1_fe25519_64 x8). +Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed. diff --git a/src/SpecificGen/GF25519_64BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF25519_64BoundedExtendedAddCoordinates.v new file mode 100644 index 000000000..d5e92dfac --- /dev/null +++ b/src/SpecificGen/GF25519_64BoundedExtendedAddCoordinates.v @@ -0,0 +1,67 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.SpecificGen.GF25519_64Bounded. +Require Import Crypto.SpecificGen.GF25519_64ExtendedAddCoordinates. +Require Import Crypto.SpecificGen.GF25519_64BoundedAddCoordinates. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. + +Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23 + : Tuple.fieldwise + (n:=4) GF25519_64BoundedCommon.eq + (@GF25519_64BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23) + (@ExtendedCoordinates.Extended.add_coordinates + GF25519_64BoundedCommon.fe25519_64 + GF25519_64Bounded.add GF25519_64Bounded.sub GF25519_64Bounded.mul twice_d + (P10, P11, P12, P13) (P20, P21, P22, P23)). +Proof. + unfold GF25519_64BoundedCommon.eq. + apply -> (fieldwise_map_iff (n:=4) eq GF25519_64BoundedCommon.proj1_fe25519_64 GF25519_64BoundedCommon.proj1_fe25519_64). + rewrite add_coordinates_correct. + cbv [AddCoordinates.add_coordinates]. + setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry. + unfold edwards_extended_carry_add_coordinates. + match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end. + apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF25519_64BoundedCommon.proj1_fe25519_64). + apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero; + intros; + repeat match goal with + | [ |- context[add _ _] ] + => rewrite add_correct + | [ |- context[sub _ _] ] + => rewrite sub_correct + | [ |- context[mul _ _] ] + => rewrite mul_correct + | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in * + | [ |- and _ _ ] => split + | [ |- ?x = ?x ] => reflexivity + | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct + | _ => congruence + end. +Qed. + +Definition add_coordinates' twice_d P1 P2 + := let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF25519_64BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Definition add_coordinates twice_d P1 P2 + := Eval cbv beta iota delta [GF25519_64BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in + let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF25519_64BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Lemma add_coordinates_correct_full twice_d P1 P2 + : Tuple.fieldwise + GF25519_64BoundedCommon.eq + (add_coordinates twice_d P1 P2) + (@ExtendedCoordinates.Extended.add_coordinates + GF25519_64BoundedCommon.fe25519_64 + GF25519_64Bounded.add GF25519_64Bounded.sub GF25519_64Bounded.mul twice_d P1 P2). +Proof. + destruct_head' prod. + rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity. +Qed. diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v index 58764461e..bbdccaf26 100644 --- a/src/SpecificGen/GF25519_64Reflective/Common.v +++ b/src/SpecificGen/GF25519_64Reflective/Common.v @@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op := let T := (type of uncurried_op) in make_type_from' T. -Definition ExprBinOpT : type base_type. -Proof. make_type_from (uncurry_binop_fe25519_64 carry_add). Defined. -Definition ExprUnOpT : type base_type. -Proof. make_type_from (uncurry_unop_fe25519_64 carry_opp). Defined. +Definition fe25519_64T : flat_type base_type. +Proof. + let T := (eval compute in GF25519_64.fe25519_64) in + let T := reify_flat_type T in + exact T. +Defined. +Definition Expr_n_OpT (count_out : nat) : flat_type base_type + := Eval cbv [Syntax.tuple Syntax.tuple' fe25519_64T] in + Syntax.tuple fe25519_64T count_out. +Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type + := match count_in with + | 0 => Expr_n_OpT count_out + | S n => SmartArrow base_type fe25519_64T (Expr_nm_OpT n count_out) + end. +Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1. +Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1. Definition ExprUnOpFEToZT : type base_type. Proof. make_type_from (uncurry_unop_fe25519_64 ge_modulus). Defined. Definition ExprUnOpWireToFET : type base_type. Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined. Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe25519_64 pack). Defined. -Definition Expr4OpT : type base_type. -Proof. - let T := lazymatch type of (apply4_nd - (B:=GF25519_64.fe25519_64) - (@uncurry_unop_fe25519_64)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. -Definition Expr9_4OpT : type base_type. -Proof. - let T := lazymatch type of (apply9_nd - (B:=Tuple.tuple GF25519_64.fe25519_64 4) - (@uncurry_unop_fe25519_64)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. +Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. +Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type Definition ExprArgWireRevT : flat_type base_type := Eval compute in all_binders_for ExprUnOpWireToFET. Definition ExprZ : Type := Expr (Tbase TZ). -Definition ExprBinOp : Type := Expr ExprBinOpT. -Definition ExprUnOp : Type := Expr ExprUnOpT. Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT. Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET. Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT. +Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out). +Definition ExprBinOp : Type := Expr ExprBinOpT. +Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). +Definition expr_nm_Op count_in count_out interp_base_type var : Type + := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. +Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. +Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. +Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Local Ltac bounds_from_list_cps ls := + lazymatch (eval hnf in ls) with + | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra)) + | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in + constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra)) + end. + +Local Ltac make_bounds_cps ls := + let v := bounds_from_list_cps (List.rev ls) in + let v := (eval compute in v) in + pose v. + Local Ltac bounds_from_list ls := lazymatch (eval hnf in ls) with | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}) @@ -105,6 +116,18 @@ Local Ltac make_bounds ls := let v := (eval compute in v) in exact v. +(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type. +Proof. + refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with + | 0 => tt + | S n => let v := Expr_nm_Op_bounds n count_out in + _ + end; simpl. + make_bounds_cps (Tuple.to_list _ bounds). + pose (p _ v). + repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]). + exact p0. +*) Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined. Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type. diff --git a/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v new file mode 100644 index 000000000..e9067cee8 --- /dev/null +++ b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v @@ -0,0 +1,76 @@ +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Export Crypto.SpecificGen.GF25519_64. +Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Reflection.Z.Interpretations128. +Require Crypto.Reflection.Z.Interpretations128.Relations. +Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations. +Require Import Crypto.Reflection.Z.Reify. +Require Import Crypto.Reflection.Z.Syntax. +Require Import Crypto.SpecificGen.GF25519_64Reflective.Common. +Require Import Crypto.SpecificGen.GF25519_64Reflective.Reified.AddCoordinates. +Require Import Bedrock.Word Crypto.Util.WordUtil. +Require Import Coq.Lists.List Crypto.Util.ListUtil. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Algebra. +Import ListNotations. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Local Open Scope Z. + +Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW. + +Declare Reduction asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW curry_9op_fe25519_64W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. +Ltac asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW curry_9op_fe25519_64W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word128ize rword128ize + Interp interp interp_flat_type interpf interp_flat_type fst snd]. + + +Time Definition interp_radd_coordinates : SpecificGen.GF25519_64BoundedCommon.fe25519_64W + -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W + -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W + -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W + -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W + -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W + -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W + -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W + -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W + -> Tuple.tuple SpecificGen.GF25519_64BoundedCommon.fe25519_64W 4 + := Eval asm_interp_add_coordinates in interp_9_4expr (rword128ize radd_coordinates). +(*Print interp_radd_coordinates.*) +Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. + +Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates. +Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed. diff --git a/src/SpecificGen/GF41417_32BoundedAddCoordinates.v b/src/SpecificGen/GF41417_32BoundedAddCoordinates.v new file mode 100644 index 000000000..e7d5842ce --- /dev/null +++ b/src/SpecificGen/GF41417_32BoundedAddCoordinates.v @@ -0,0 +1,77 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.SpecificGen.GF41417_32. +Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. +Require Import Crypto.SpecificGen.GF41417_32ReflectiveAddCoordinates. +Require Import Crypto.Util.LetIn. +Local Open Scope Z. + +Local Ltac bounded_t opW blem := + apply blem; apply is_bounded_proj1_fe41417_32. + +Local Ltac define_binop f g opW blem := + refine (exist_fe41417_32W (opW (proj1_fe41417_32W f) (proj1_fe41417_32W g)) _); + abstract bounded_t opW blem. + +Local Opaque Let_In. +Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64. +Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _. +Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe41417_32W) : Tuple.tuple fe41417_32W 4 + := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8. + +Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb := + change opW with (interp_rop); + rewrite pre_rewrite; + intros; apply rop_cb; assumption. + +Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates. +Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed. + +Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem := + refine (let ts := opW (proj1_fe41417_32W x0) + (proj1_fe41417_32W x1) + (proj1_fe41417_32W x2) + (proj1_fe41417_32W x3) + (proj1_fe41417_32W x4) + (proj1_fe41417_32W x5) + (proj1_fe41417_32W x6) + (proj1_fe41417_32W x7) + (proj1_fe41417_32W x8) in + HList.mapt exist_fe41417_32W (ts:=ts) _); + abstract ( + rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe41417_32WToZ)); + apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe41417_32 + ). +Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe41417_32) : Tuple.tuple fe41417_32 4. +Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined. + +Local Ltac op_correct_t op opW_correct_and_bounded := + cbv [op]; + rewrite ?HList.map_mapt; + lazymatch goal with + | [ |- context[proj1_fe41417_32 (exist_fe41417_32W _ _)] ] + => rewrite proj1_fe41417_32_exist_fe41417_32W || setoid_rewrite proj1_fe41417_32_exist_fe41417_32W + | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ] + => rewrite proj1_wire_digits_exist_wire_digitsW + | _ => idtac + end; + rewrite <- ?HList.map_is_mapt; + apply opW_correct_and_bounded; + lazymatch goal with + | [ |- is_bounded _ = true ] + => apply is_bounded_proj1_fe41417_32 + | [ |- wire_digits_is_bounded _ = true ] + => apply is_bounded_proj1_wire_digits + end. + +Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe41417_32) + : Tuple.map (n:=4) proj1_fe41417_32 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8) + = Reified.AddCoordinates.add_coordinates (proj1_fe41417_32 x0) + (proj1_fe41417_32 x1) + (proj1_fe41417_32 x2) + (proj1_fe41417_32 x3) + (proj1_fe41417_32 x4) + (proj1_fe41417_32 x5) + (proj1_fe41417_32 x6) + (proj1_fe41417_32 x7) + (proj1_fe41417_32 x8). +Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed. diff --git a/src/SpecificGen/GF41417_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF41417_32BoundedExtendedAddCoordinates.v new file mode 100644 index 000000000..dc99e0b11 --- /dev/null +++ b/src/SpecificGen/GF41417_32BoundedExtendedAddCoordinates.v @@ -0,0 +1,67 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.SpecificGen.GF41417_32Bounded. +Require Import Crypto.SpecificGen.GF41417_32ExtendedAddCoordinates. +Require Import Crypto.SpecificGen.GF41417_32BoundedAddCoordinates. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. + +Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23 + : Tuple.fieldwise + (n:=4) GF41417_32BoundedCommon.eq + (@GF41417_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23) + (@ExtendedCoordinates.Extended.add_coordinates + GF41417_32BoundedCommon.fe41417_32 + GF41417_32Bounded.add GF41417_32Bounded.sub GF41417_32Bounded.mul twice_d + (P10, P11, P12, P13) (P20, P21, P22, P23)). +Proof. + unfold GF41417_32BoundedCommon.eq. + apply -> (fieldwise_map_iff (n:=4) eq GF41417_32BoundedCommon.proj1_fe41417_32 GF41417_32BoundedCommon.proj1_fe41417_32). + rewrite add_coordinates_correct. + cbv [AddCoordinates.add_coordinates]. + setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry. + unfold edwards_extended_carry_add_coordinates. + match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end. + apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF41417_32BoundedCommon.proj1_fe41417_32). + apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero; + intros; + repeat match goal with + | [ |- context[add _ _] ] + => rewrite add_correct + | [ |- context[sub _ _] ] + => rewrite sub_correct + | [ |- context[mul _ _] ] + => rewrite mul_correct + | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in * + | [ |- and _ _ ] => split + | [ |- ?x = ?x ] => reflexivity + | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct + | _ => congruence + end. +Qed. + +Definition add_coordinates' twice_d P1 P2 + := let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF41417_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Definition add_coordinates twice_d P1 P2 + := Eval cbv beta iota delta [GF41417_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in + let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF41417_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Lemma add_coordinates_correct_full twice_d P1 P2 + : Tuple.fieldwise + GF41417_32BoundedCommon.eq + (add_coordinates twice_d P1 P2) + (@ExtendedCoordinates.Extended.add_coordinates + GF41417_32BoundedCommon.fe41417_32 + GF41417_32Bounded.add GF41417_32Bounded.sub GF41417_32Bounded.mul twice_d P1 P2). +Proof. + destruct_head' prod. + rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity. +Qed. diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v index e40dd0c53..40089d503 100644 --- a/src/SpecificGen/GF41417_32Reflective/Common.v +++ b/src/SpecificGen/GF41417_32Reflective/Common.v @@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op := let T := (type of uncurried_op) in make_type_from' T. -Definition ExprBinOpT : type base_type. -Proof. make_type_from (uncurry_binop_fe41417_32 carry_add). Defined. -Definition ExprUnOpT : type base_type. -Proof. make_type_from (uncurry_unop_fe41417_32 carry_opp). Defined. +Definition fe41417_32T : flat_type base_type. +Proof. + let T := (eval compute in GF41417_32.fe41417_32) in + let T := reify_flat_type T in + exact T. +Defined. +Definition Expr_n_OpT (count_out : nat) : flat_type base_type + := Eval cbv [Syntax.tuple Syntax.tuple' fe41417_32T] in + Syntax.tuple fe41417_32T count_out. +Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type + := match count_in with + | 0 => Expr_n_OpT count_out + | S n => SmartArrow base_type fe41417_32T (Expr_nm_OpT n count_out) + end. +Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1. +Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1. Definition ExprUnOpFEToZT : type base_type. Proof. make_type_from (uncurry_unop_fe41417_32 ge_modulus). Defined. Definition ExprUnOpWireToFET : type base_type. Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined. Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe41417_32 pack). Defined. -Definition Expr4OpT : type base_type. -Proof. - let T := lazymatch type of (apply4_nd - (B:=GF41417_32.fe41417_32) - (@uncurry_unop_fe41417_32)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. -Definition Expr9_4OpT : type base_type. -Proof. - let T := lazymatch type of (apply9_nd - (B:=Tuple.tuple GF41417_32.fe41417_32 4) - (@uncurry_unop_fe41417_32)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. +Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. +Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type Definition ExprArgWireRevT : flat_type base_type := Eval compute in all_binders_for ExprUnOpWireToFET. Definition ExprZ : Type := Expr (Tbase TZ). -Definition ExprBinOp : Type := Expr ExprBinOpT. -Definition ExprUnOp : Type := Expr ExprUnOpT. Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT. Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET. Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT. +Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out). +Definition ExprBinOp : Type := Expr ExprBinOpT. +Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). +Definition expr_nm_Op count_in count_out interp_base_type var : Type + := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. +Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. +Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. +Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Local Ltac bounds_from_list_cps ls := + lazymatch (eval hnf in ls) with + | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra)) + | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in + constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra)) + end. + +Local Ltac make_bounds_cps ls := + let v := bounds_from_list_cps (List.rev ls) in + let v := (eval compute in v) in + pose v. + Local Ltac bounds_from_list ls := lazymatch (eval hnf in ls) with | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}) @@ -105,6 +116,18 @@ Local Ltac make_bounds ls := let v := (eval compute in v) in exact v. +(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type. +Proof. + refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with + | 0 => tt + | S n => let v := Expr_nm_Op_bounds n count_out in + _ + end; simpl. + make_bounds_cps (Tuple.to_list _ bounds). + pose (p _ v). + repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]). + exact p0. +*) Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined. Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type. diff --git a/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v new file mode 100644 index 000000000..6d4dd60bb --- /dev/null +++ b/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v @@ -0,0 +1,76 @@ +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Export Crypto.SpecificGen.GF41417_32. +Require Import Crypto.SpecificGen.GF41417_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Reflection.Z.Interpretations64. +Require Crypto.Reflection.Z.Interpretations64.Relations. +Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. +Require Import Crypto.Reflection.Z.Reify. +Require Import Crypto.Reflection.Z.Syntax. +Require Import Crypto.SpecificGen.GF41417_32Reflective.Common. +Require Import Crypto.SpecificGen.GF41417_32Reflective.Reified.AddCoordinates. +Require Import Bedrock.Word Crypto.Util.WordUtil. +Require Import Coq.Lists.List Crypto.Util.ListUtil. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Algebra. +Import ListNotations. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Local Open Scope Z. + +Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW. + +Declare Reduction asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe41417_32W curry_unop_fe41417_32W curry_unop_wire_digitsW curry_9op_fe41417_32W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. +Ltac asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe41417_32W curry_unop_fe41417_32W curry_unop_wire_digitsW curry_9op_fe41417_32W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + Interp interp interp_flat_type interpf interp_flat_type fst snd]. + + +Time Definition interp_radd_coordinates : SpecificGen.GF41417_32BoundedCommon.fe41417_32W + -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W + -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W + -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W + -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W + -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W + -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W + -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W + -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W + -> Tuple.tuple SpecificGen.GF41417_32BoundedCommon.fe41417_32W 4 + := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). +(*Print interp_radd_coordinates.*) +Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. + +Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates. +Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed. diff --git a/src/SpecificGen/GF5211_32BoundedAddCoordinates.v b/src/SpecificGen/GF5211_32BoundedAddCoordinates.v new file mode 100644 index 000000000..17189f4d0 --- /dev/null +++ b/src/SpecificGen/GF5211_32BoundedAddCoordinates.v @@ -0,0 +1,77 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.SpecificGen.GF5211_32. +Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. +Require Import Crypto.SpecificGen.GF5211_32ReflectiveAddCoordinates. +Require Import Crypto.Util.LetIn. +Local Open Scope Z. + +Local Ltac bounded_t opW blem := + apply blem; apply is_bounded_proj1_fe5211_32. + +Local Ltac define_binop f g opW blem := + refine (exist_fe5211_32W (opW (proj1_fe5211_32W f) (proj1_fe5211_32W g)) _); + abstract bounded_t opW blem. + +Local Opaque Let_In. +Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64. +Local Arguments interp_radd_coordinates / _ _ _ _ _ _ _ _ _. +Definition add_coordinatesW (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe5211_32W) : Tuple.tuple fe5211_32W 4 + := Eval simpl in interp_radd_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8. + +Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb := + change opW with (interp_rop); + rewrite pre_rewrite; + intros; apply rop_cb; assumption. + +Lemma add_coordinatesW_correct_and_bounded : i9top_correct_and_bounded 4 add_coordinatesW Reified.AddCoordinates.add_coordinates. +Proof. port_correct_and_bounded interp_radd_coordinates_correct add_coordinatesW interp_radd_coordinates radd_coordinates_correct_and_bounded. Qed. + +Local Ltac define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 opW blem := + refine (let ts := opW (proj1_fe5211_32W x0) + (proj1_fe5211_32W x1) + (proj1_fe5211_32W x2) + (proj1_fe5211_32W x3) + (proj1_fe5211_32W x4) + (proj1_fe5211_32W x5) + (proj1_fe5211_32W x6) + (proj1_fe5211_32W x7) + (proj1_fe5211_32W x8) in + HList.mapt exist_fe5211_32W (ts:=ts) _); + abstract ( + rewrite <- (HList.hlist_map (F:=fun x => is_bounded x = true) (f:=fe5211_32WToZ)); + apply add_coordinatesW_correct_and_bounded; apply is_bounded_proj1_fe5211_32 + ). +Definition add_coordinates (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe5211_32) : Tuple.tuple fe5211_32 4. +Proof. define_9_4op x0 x1 x2 x3 x4 x5 x6 x7 x8 add_coordinatesW add_coordinatesW_correct_and_bounded. Defined. + +Local Ltac op_correct_t op opW_correct_and_bounded := + cbv [op]; + rewrite ?HList.map_mapt; + lazymatch goal with + | [ |- context[proj1_fe5211_32 (exist_fe5211_32W _ _)] ] + => rewrite proj1_fe5211_32_exist_fe5211_32W || setoid_rewrite proj1_fe5211_32_exist_fe5211_32W + | [ |- context[proj1_wire_digits (exist_wire_digitsW _ _)] ] + => rewrite proj1_wire_digits_exist_wire_digitsW + | _ => idtac + end; + rewrite <- ?HList.map_is_mapt; + apply opW_correct_and_bounded; + lazymatch goal with + | [ |- is_bounded _ = true ] + => apply is_bounded_proj1_fe5211_32 + | [ |- wire_digits_is_bounded _ = true ] + => apply is_bounded_proj1_wire_digits + end. + +Lemma add_coordinates_correct (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe5211_32) + : Tuple.map (n:=4) proj1_fe5211_32 (add_coordinates x0 x1 x2 x3 x4 x5 x6 x7 x8) + = Reified.AddCoordinates.add_coordinates (proj1_fe5211_32 x0) + (proj1_fe5211_32 x1) + (proj1_fe5211_32 x2) + (proj1_fe5211_32 x3) + (proj1_fe5211_32 x4) + (proj1_fe5211_32 x5) + (proj1_fe5211_32 x6) + (proj1_fe5211_32 x7) + (proj1_fe5211_32 x8). +Proof. op_correct_t add_coordinates add_coordinatesW_correct_and_bounded. Qed. diff --git a/src/SpecificGen/GF5211_32BoundedExtendedAddCoordinates.v b/src/SpecificGen/GF5211_32BoundedExtendedAddCoordinates.v new file mode 100644 index 000000000..f6ba06ec6 --- /dev/null +++ b/src/SpecificGen/GF5211_32BoundedExtendedAddCoordinates.v @@ -0,0 +1,67 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.SpecificGen.GF5211_32Bounded. +Require Import Crypto.SpecificGen.GF5211_32ExtendedAddCoordinates. +Require Import Crypto.SpecificGen.GF5211_32BoundedAddCoordinates. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. + +Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23 + : Tuple.fieldwise + (n:=4) GF5211_32BoundedCommon.eq + (@GF5211_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23) + (@ExtendedCoordinates.Extended.add_coordinates + GF5211_32BoundedCommon.fe5211_32 + GF5211_32Bounded.add GF5211_32Bounded.sub GF5211_32Bounded.mul twice_d + (P10, P11, P12, P13) (P20, P21, P22, P23)). +Proof. + unfold GF5211_32BoundedCommon.eq. + apply -> (fieldwise_map_iff (n:=4) eq GF5211_32BoundedCommon.proj1_fe5211_32 GF5211_32BoundedCommon.proj1_fe5211_32). + rewrite add_coordinates_correct. + cbv [AddCoordinates.add_coordinates]. + setoid_rewrite <- fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry. + unfold edwards_extended_carry_add_coordinates. + match goal with |- ?R ?x ?y => rewrite <- (Tuple.map_id (n:=4) x) end. + apply <- (fieldwise_map_iff (n:=4) eq (fun x => x) GF5211_32BoundedCommon.proj1_fe5211_32). + apply ExtendedCoordinates.Extended.add_coordinates_respectful_hetero; + intros; + repeat match goal with + | [ |- context[add _ _] ] + => rewrite add_correct + | [ |- context[sub _ _] ] + => rewrite sub_correct + | [ |- context[mul _ _] ] + => rewrite mul_correct + | _ => progress unfold Tuple.fieldwise, Tuple.fieldwise', fst, snd, eq in * + | [ |- and _ _ ] => split + | [ |- ?x = ?x ] => reflexivity + | _ => progress rewrite_strat topdown hints edwards_extended_add_coordinates_correct + | _ => congruence + end. +Qed. + +Definition add_coordinates' twice_d P1 P2 + := let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF5211_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Definition add_coordinates twice_d P1 P2 + := Eval cbv beta iota delta [GF5211_32BoundedAddCoordinates.add_coordinates HList.mapt HList.mapt'] in + let '(P10, P11, P12, P13) := P1 in + let '(P20, P21, P22, P23) := P2 in + @GF5211_32BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23. + +Lemma add_coordinates_correct_full twice_d P1 P2 + : Tuple.fieldwise + GF5211_32BoundedCommon.eq + (add_coordinates twice_d P1 P2) + (@ExtendedCoordinates.Extended.add_coordinates + GF5211_32BoundedCommon.fe5211_32 + GF5211_32Bounded.add GF5211_32Bounded.sub GF5211_32Bounded.mul twice_d P1 P2). +Proof. + destruct_head' prod. + rewrite <- fieldwise_eq_extended_add_coordinates_full'; reflexivity. +Qed. diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v index 1db5efcd0..2ad555057 100644 --- a/src/SpecificGen/GF5211_32Reflective/Common.v +++ b/src/SpecificGen/GF5211_32Reflective/Common.v @@ -31,34 +31,30 @@ Local Ltac make_type_from uncurried_op := let T := (type of uncurried_op) in make_type_from' T. -Definition ExprBinOpT : type base_type. -Proof. make_type_from (uncurry_binop_fe5211_32 carry_add). Defined. -Definition ExprUnOpT : type base_type. -Proof. make_type_from (uncurry_unop_fe5211_32 carry_opp). Defined. +Definition fe5211_32T : flat_type base_type. +Proof. + let T := (eval compute in GF5211_32.fe5211_32) in + let T := reify_flat_type T in + exact T. +Defined. +Definition Expr_n_OpT (count_out : nat) : flat_type base_type + := Eval cbv [Syntax.tuple Syntax.tuple' fe5211_32T] in + Syntax.tuple fe5211_32T count_out. +Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type + := match count_in with + | 0 => Expr_n_OpT count_out + | S n => SmartArrow base_type fe5211_32T (Expr_nm_OpT n count_out) + end. +Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1. +Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1. Definition ExprUnOpFEToZT : type base_type. Proof. make_type_from (uncurry_unop_fe5211_32 ge_modulus). Defined. Definition ExprUnOpWireToFET : type base_type. Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined. Definition ExprUnOpFEToWireT : type base_type. Proof. make_type_from (uncurry_unop_fe5211_32 pack). Defined. -Definition Expr4OpT : type base_type. -Proof. - let T := lazymatch type of (apply4_nd - (B:=GF5211_32.fe5211_32) - (@uncurry_unop_fe5211_32)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. -Definition Expr9_4OpT : type base_type. -Proof. - let T := lazymatch type of (apply9_nd - (B:=Tuple.tuple GF5211_32.fe5211_32 4) - (@uncurry_unop_fe5211_32)) with - | _ -> ?T => T - end in - make_type_from' T. -Defined. +Definition Expr4OpT : type base_type := Eval compute in Expr_nm_OpT 4 1. +Definition Expr9_4OpT : type base_type := Eval compute in Expr_nm_OpT 9 4. Definition ExprArgT : flat_type base_type := Eval compute in remove_all_binders ExprUnOpT. Definition ExprArgWireT : flat_type base_type @@ -68,30 +64,45 @@ Definition ExprArgRevT : flat_type base_type Definition ExprArgWireRevT : flat_type base_type := Eval compute in all_binders_for ExprUnOpWireToFET. Definition ExprZ : Type := Expr (Tbase TZ). -Definition ExprBinOp : Type := Expr ExprBinOpT. -Definition ExprUnOp : Type := Expr ExprUnOpT. Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT. Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET. Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT. +Definition Expr_nm_Op count_in count_out : Type := Expr (Expr_nm_OpT count_in count_out). +Definition ExprBinOp : Type := Expr ExprBinOpT. +Definition ExprUnOp : Type := Expr ExprUnOpT. Definition Expr4Op : Type := Expr Expr4OpT. Definition Expr9_4Op : Type := Expr Expr9_4OpT. Definition ExprArg : Type := Expr ExprArgT. Definition ExprArgWire : Type := Expr ExprArgWireT. Definition ExprArgRev : Type := Expr ExprArgRevT. Definition ExprArgWireRev : Type := Expr ExprArgWireRevT. -Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). +Definition expr_nm_Op count_in count_out interp_base_type var : Type + := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out). Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT. Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT. +Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. +Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. +Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ). Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT. Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET. Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT. -Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT. -Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT. Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT. Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT. Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT. Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT. +Local Ltac bounds_from_list_cps ls := + lazymatch (eval hnf in ls) with + | (?x :: nil)%list => constr:(fun T (extra : T) => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, extra)) + | (?x :: ?xs)%list => let bs := bounds_from_list_cps xs in + constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra)) + end. + +Local Ltac make_bounds_cps ls := + let v := bounds_from_list_cps (List.rev ls) in + let v := (eval compute in v) in + pose v. + Local Ltac bounds_from_list ls := lazymatch (eval hnf in ls) with | (?x :: nil)%list => constr:(Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}) @@ -105,6 +116,18 @@ Local Ltac make_bounds ls := let v := (eval compute in v) in exact v. +(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type. +Proof. + refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with + | 0 => tt + | S n => let v := Expr_nm_Op_bounds n count_out in + _ + end; simpl. + make_bounds_cps (Tuple.to_list _ bounds). + pose (p _ v). + repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]). + exact p0. +*) Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined. Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type. diff --git a/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v new file mode 100644 index 000000000..ddba2a199 --- /dev/null +++ b/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v @@ -0,0 +1,76 @@ +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Export Crypto.SpecificGen.GF5211_32. +Require Import Crypto.SpecificGen.GF5211_32BoundedCommon. +Require Import Crypto.Reflection.Reify. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.MapInterp. +Require Import Crypto.Reflection.Z.Interpretations64. +Require Crypto.Reflection.Z.Interpretations64.Relations. +Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations. +Require Import Crypto.Reflection.Z.Reify. +Require Import Crypto.Reflection.Z.Syntax. +Require Import Crypto.SpecificGen.GF5211_32Reflective.Common. +Require Import Crypto.SpecificGen.GF5211_32Reflective.Reified.AddCoordinates. +Require Import Bedrock.Word Crypto.Util.WordUtil. +Require Import Coq.Lists.List Crypto.Util.ListUtil. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Algebra. +Import ListNotations. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Local Open Scope Z. + +Time Definition radd_coordinates : Expr9_4Op := Eval vm_compute in radd_coordinatesW. + +Declare Reduction asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW curry_9op_fe5211_32W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd]. +Ltac asm_interp_add_coordinates + := cbv beta iota delta + [id + interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr + radd_coordinates + curry_binop_fe5211_32W curry_unop_fe5211_32W curry_unop_wire_digitsW curry_9op_fe5211_32W + WordW.interp_op WordW.interp_base_type + Z.interp_op Z.interp_base_type + Z.Syntax.interp_op Z.Syntax.interp_base_type + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize + Interp interp interp_flat_type interpf interp_flat_type fst snd]. + + +Time Definition interp_radd_coordinates : SpecificGen.GF5211_32BoundedCommon.fe5211_32W + -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W + -> Tuple.tuple SpecificGen.GF5211_32BoundedCommon.fe5211_32W 4 + := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates). +(*Print interp_radd_coordinates.*) +Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl. + +Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates. +Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed. -- cgit v1.2.3