diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/SpecificGen/GF2213_32.v | 234 | ||||
| -rw-r--r-- | src/SpecificGen/GF2519_32.v | 234 | ||||
| -rw-r--r-- | src/SpecificGen/GF25519_32.v | 234 | ||||
| -rw-r--r-- | src/SpecificGen/GF25519_64.v | 234 | ||||
| -rw-r--r-- | src/SpecificGen/GF41417_32.v | 234 | ||||
| -rw-r--r-- | src/SpecificGen/GF5211_32.v | 234 | ||||
| -rw-r--r-- | src/SpecificGen/GFtemplate3mod4 | 234 | ||||
| -rw-r--r-- | src/SpecificGen/GFtemplate5mod8 | 234 |
8 files changed, 936 insertions, 936 deletions
diff --git a/src/SpecificGen/GF2213_32.v b/src/SpecificGen/GF2213_32.v index fe45e3423..4108ba2b0 100644 --- a/src/SpecificGen/GF2213_32.v +++ b/src/SpecificGen/GF2213_32.v @@ -25,15 +25,15 @@ Lemma prime_modulus : prime modulus. Admitted. Definition freeze_input_bound := 32%Z. Definition int_width := 32%Z. -Instance params : PseudoMersenneBaseParams modulus. +Instance params2213_32 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 8%nat 221. Defined. -Definition length_fe := Eval compute in length limb_widths. -Definition fe := Eval compute in (tuple Z length_fe). +Definition length_fe2213_32 := Eval compute in length limb_widths. +Definition fe2213_32 := Eval compute in (tuple Z length_fe2213_32). -Definition mul2modulus : fe := - Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params)). +Definition mul2modulus : fe2213_32 := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params2213_32)). Instance subCoeff : SubtractionCoefficient. apply Build_SubtractionCoefficient with (coeff := mul2modulus). @@ -150,24 +150,24 @@ Proof. reflexivity. Qed. -Definition app_n {T} (f : fe) (P : fe -> T) : T. +Definition app_n {T} (f : fe2213_32) (P : fe2213_32 -> T) : T. Proof. - cbv [fe] in *. + cbv [fe2213_32] in *. set (f0 := f). repeat (let g := fresh "g" in destruct f as [f g]). apply P. apply f0. Defined. -Definition app_n_correct {T} f (P : fe -> T) : app_n f P = P f. +Definition app_n_correct {T} f (P : fe2213_32 -> T) : app_n f P = P f. Proof. intros. - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. reflexivity. Qed. -Definition appify2 {T} (op : fe -> fe -> T) (f g : fe) := +Definition appify2 {T} (op : fe2213_32 -> fe2213_32 -> T) (f g : fe2213_32) := app_n f (fun f0 => (app_n g (fun g0 => op f0 g0))). Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g. @@ -176,102 +176,102 @@ Proof. etransitivity; apply app_n_correct. Qed. -Definition uncurry_unop_fe {T} (op : fe -> T) - := Eval compute in Tuple.uncurry (n:=length_fe) op. -Definition curry_unop_fe {T} op : fe -> T - := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe) op). -Definition uncurry_binop_fe {T} (op : fe -> fe -> T) - := Eval compute in uncurry_unop_fe (fun f => uncurry_unop_fe (op f)). -Definition curry_binop_fe {T} op : fe -> fe -> T - := Eval compute in appify2 (fun f => curry_unop_fe (curry_unop_fe op f)). +Definition uncurry_unop_fe2213_32 {T} (op : fe2213_32 -> T) + := Eval compute in Tuple.uncurry (n:=length_fe2213_32) op. +Definition curry_unop_fe2213_32 {T} op : fe2213_32 -> T + := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe2213_32) op). +Definition uncurry_binop_fe2213_32 {T} (op : fe2213_32 -> fe2213_32 -> T) + := Eval compute in uncurry_unop_fe2213_32 (fun f => uncurry_unop_fe2213_32 (op f)). +Definition curry_binop_fe2213_32 {T} op : fe2213_32 -> fe2213_32 -> T + := Eval compute in appify2 (fun f => curry_unop_fe2213_32 (curry_unop_fe2213_32 op f)). Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) := Eval compute in Tuple.uncurry (n:=length wire_widths) op. Definition curry_unop_wire_digits {T} op : wire_digits -> T := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op). -Definition add_sig (f g : fe) : - { fg : fe | fg = add_opt f g}. +Definition add_sig (f g : fe2213_32) : + { fg : fe2213_32 | fg = add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe2213_32). cbv. reflexivity. Defined. -Definition add (f g : fe) : fe := +Definition add (f g : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig add_sig] in proj1_sig (add_sig f g). -Definition add_correct (f g : fe) +Definition add_correct (f g : fe2213_32) : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (add_sig f g). -Definition carry_add_sig (f g : fe) : - { fg : fe | fg = carry_add_opt f g}. +Definition carry_add_sig (f g : fe2213_32) : + { fg : fe2213_32 | fg = carry_add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe2213_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_add (f g : fe) : fe := +Definition carry_add (f g : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj1_sig (carry_add_sig f g). -Definition carry_add_correct (f g : fe) +Definition carry_add_correct (f g : fe2213_32) : carry_add f g = carry_add_opt f g := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj2_sig (carry_add_sig f g). -Definition sub_sig (f g : fe) : - { fg : fe | fg = sub_opt f g}. +Definition sub_sig (f g : fe2213_32) : + { fg : fe2213_32 | fg = sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe2213_32). cbv. reflexivity. Defined. -Definition sub (f g : fe) : fe := +Definition sub (f g : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig sub_sig] in proj1_sig (sub_sig f g). -Definition sub_correct (f g : fe) +Definition sub_correct (f g : fe2213_32) : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). -Definition carry_sub_sig (f g : fe) : - { fg : fe | fg = carry_sub_opt f g}. +Definition carry_sub_sig (f g : fe2213_32) : + { fg : fe2213_32 | fg = carry_sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe2213_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_sub (f g : fe) : fe := +Definition carry_sub (f g : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj1_sig (carry_sub_sig f g). -Definition carry_sub_correct (f g : fe) +Definition carry_sub_correct (f g : fe2213_32) : carry_sub f g = carry_sub_opt f g := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj2_sig (carry_sub_sig f g). (* For multiplication, we add another layer of definition so that we can rewrite under the [let] binders. *) -Definition mul_simpl_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_simpl_sig (f g : fe2213_32) : + { fg : fe2213_32 | fg = carry_mul_opt k_ c_ f g}. Proof. - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. @@ -282,45 +282,45 @@ Proof. reflexivity. Defined. -Definition mul_simpl (f g : fe) : fe := +Definition mul_simpl (f g : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7) := g in proj1_sig (mul_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7) (g0, g1, g2, g3, g4, g5, g6, g7)). -Definition mul_simpl_correct (f g : fe) +Definition mul_simpl_correct (f g : fe2213_32) : mul_simpl f g = carry_mul_opt k_ c_ f g. Proof. pose proof (proj2_sig (mul_simpl_sig f g)). - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition mul_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_sig (f g : fe2213_32) : + { fg : fe2213_32 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe2213_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition mul (f g : fe) : fe := +Definition mul (f g : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). -Definition mul_correct (f g : fe) +Definition mul_correct (f g : fe2213_32) : mul f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (mul_sig f g). -Definition opp_sig (f : fe) : - { g : fe | g = opp_opt f }. +Definition opp_sig (f : fe2213_32) : + { g : fe2213_32 | g = opp_opt f }. Proof. eexists. cbv [opp_opt]. @@ -330,15 +330,15 @@ Proof. reflexivity. Defined. -Definition opp (f : fe) : fe +Definition opp (f : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). -Definition opp_correct (f : fe) +Definition opp_correct (f : fe2213_32) : opp f = opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). -Definition carry_opp_sig (f : fe) : - { g : fe | g = carry_opp_opt f }. +Definition carry_opp_sig (f : fe2213_32) : + { g : fe2213_32 | g = carry_opp_opt f }. Proof. eexists. cbv [carry_opp_opt]. @@ -348,16 +348,16 @@ Proof. reflexivity. Defined. -Definition carry_opp (f : fe) : fe +Definition carry_opp (f : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f). -Definition carry_opp_correct (f : fe) +Definition carry_opp_correct (f : fe2213_32) : carry_opp f = carry_opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f). -Definition pow (f : fe) chain := fold_chain_opt one_ mul chain [f]. +Definition pow (f : fe2213_32) chain := fold_chain_opt one_ mul chain [f]. -Lemma pow_correct (f : fe) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. +Lemma pow_correct (f : fe2213_32) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. Proof. cbv [pow pow_opt]; intros. rewrite !fold_chain_opt_correct. @@ -382,8 +382,8 @@ Qed. Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb. -Definition inv_sig (f : fe) : - { g : fe | g = inv_opt k_ c_ one_ f }. +Definition inv_sig (f : fe2213_32) : + { g : fe2213_32 | g = inv_opt k_ c_ one_ f }. Proof. eexists; cbv [inv_opt]. rewrite <-pow_correct. @@ -391,10 +391,10 @@ Proof. reflexivity. Defined. -Definition inv (f : fe) : fe +Definition inv (f : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). -Definition inv_correct (f : fe) +Definition inv_correct (f : fe2213_32) : inv f = inv_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f). @@ -405,12 +405,12 @@ Import Morphisms. Local Existing Instance prime_modulus. Lemma field_and_homomorphisms - : @field fe eq zero_ one_ opp add sub mul inv div + : @field fe2213_32 eq zero_ one_ opp add sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ add mul encode + fe2213_32 eq one_ add mul encode /\ @Ring.is_homomorphism - fe eq one_ add mul + fe2213_32 eq one_ add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -428,15 +428,15 @@ Proof. { intros; apply encode_rep. } Qed. -Definition field2213 : @field fe eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. +Definition field2213 : @field fe2213_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. Lemma carry_field_and_homomorphisms - : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div + : @field fe2213_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ carry_add mul encode + fe2213_32 eq one_ carry_add mul encode /\ @Ring.is_homomorphism - fe eq one_ carry_add mul + fe2213_32 eq one_ carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -454,29 +454,29 @@ Proof. { intros; apply encode_rep. } Qed. -Definition carry_field : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. +Definition carry_field : @field fe2213_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. Lemma homomorphism_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe2213_32 eq one add mul encode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_F_decode - : @Ring.is_homomorphism fe eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe2213_32 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one carry_add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe2213_32 eq one carry_add mul encode. Proof. apply carry_field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_decode - : @Ring.is_homomorphism fe eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe2213_32 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply carry_field_and_homomorphisms. Qed. -Definition ge_modulus_sig (f : fe) : +Definition ge_modulus_sig (f : fe2213_32) : { b : Z | b = ge_modulus_opt (to_list 8 f) }. Proof. - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [ge_modulus_opt]. rewrite !modulus_digits_subst. @@ -484,24 +484,24 @@ Proof. reflexivity. Defined. -Definition ge_modulus (f : fe) : Z := +Definition ge_modulus (f : fe2213_32) : Z := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in proj1_sig (ge_modulus_sig (f0, f1, f2, f3, f4, f5, f6, f7)). -Definition ge_modulus_correct (f : fe) : +Definition ge_modulus_correct (f : fe2213_32) : ge_modulus f = ge_modulus_opt (to_list 8 f). Proof. pose proof (proj2_sig (ge_modulus_sig f)). - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition freeze_sig (f : fe) : - { f' : fe | f' = from_list_default 0 8 (freeze_opt (int_width := int_width) c_ (to_list 8 f)) }. +Definition freeze_sig (f : fe2213_32) : + { f' : fe2213_32 | f' = from_list_default 0 8 (freeze_opt (int_width := int_width) c_ (to_list 8 f)) }. Proof. - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [freeze_opt int_width]. cbv [to_list to_list']. @@ -516,38 +516,38 @@ Proof. reflexivity. Defined. -Definition freeze (f : fe) : fe := +Definition freeze (f : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig freeze_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7)). -Definition freeze_correct (f : fe) +Definition freeze_correct (f : fe2213_32) : freeze f = from_list_default 0 8 (freeze_opt (int_width := int_width) c_ (to_list 8 f)). Proof. pose proof (proj2_sig (freeze_sig f)). - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition fieldwiseb_sig (f g : fe) : +Definition fieldwiseb_sig (f g : fe2213_32) : { b | b = @fieldwiseb Z Z 8 Z.eqb f g }. Proof. - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. reflexivity. Defined. -Definition fieldwiseb (f g : fe) : bool +Definition fieldwiseb (f g : fe2213_32) : bool := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7) := g in proj1_sig (fieldwiseb_sig (f0, f1, f2, f3, f4, f5, f6, f7) (g0, g1, g2, g3, g4, g5, g6, g7)). -Lemma fieldwiseb_correct (f g : fe) +Lemma fieldwiseb_correct (f g : fe2213_32) : fieldwiseb f g = @Tuple.fieldwiseb Z Z 8 Z.eqb f g. Proof. set (f' := f); set (g' := g). @@ -555,11 +555,11 @@ Proof. exact (proj2_sig (fieldwiseb_sig f' g')). Qed. -Definition eqb_sig (f g : fe) : +Definition eqb_sig (f g : fe2213_32) : { b | b = eqb int_width f g }. Proof. cbv [eqb]. - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [ModularBaseSystem.freeze int_width]. @@ -570,14 +570,14 @@ Proof. reflexivity. Defined. -Definition eqb (f g : fe) : bool +Definition eqb (f g : fe2213_32) : bool := Eval cbv beta iota delta [proj1_sig eqb_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7) := g in proj1_sig (eqb_sig (f0, f1, f2, f3, f4, f5, f6, f7) (g0, g1, g2, g3, g4, g5, g6, g7)). -Lemma eqb_correct (f g : fe) +Lemma eqb_correct (f g : fe2213_32) : eqb f g = ModularBaseSystem.eqb int_width f g. Proof. set (f' := f); set (g' := g). @@ -585,8 +585,8 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Definition sqrt_sig (powx powx_squared f : fe) : - { f' : fe | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powx powx_squared f}. +Definition sqrt_sig (powx powx_squared f : fe2213_32) : + { f' : fe2213_32 | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powx powx_squared f}. Proof. eexists. cbv [sqrt_5mod8_opt int_width]. @@ -595,17 +595,17 @@ Proof. reflexivity. Defined. -Definition sqrt (powx powx_squared f : fe) : fe +Definition sqrt (powx powx_squared f : fe2213_32) : fe2213_32 := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig powx powx_squared f). -Definition sqrt_correct (powx powx_squared f : fe) +Definition sqrt_correct (powx powx_squared f : fe2213_32) : sqrt powx powx_squared f = sqrt_5mod8_opt k_ c_ sqrt_m1 powx powx_squared f := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig powx powx_squared f). -Definition pack_simpl_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_simpl_sig (f : fe2213_32) : + { f' | f' = pack_opt params2213_32 wire_widths_nonneg bits_eq f }. Proof. - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [pack_opt]. @@ -616,22 +616,22 @@ Proof. reflexivity. Defined. -Definition pack_simpl (f : fe) := +Definition pack_simpl (f : fe2213_32) := Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in proj1_sig (pack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7)). -Definition pack_simpl_correct (f : fe) - : pack_simpl f = pack_opt params wire_widths_nonneg bits_eq f. +Definition pack_simpl_correct (f : fe2213_32) + : pack_simpl f = pack_opt params2213_32 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (pack_simpl_sig f)). - cbv [fe] in *. + cbv [fe2213_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition pack_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_sig (f : fe2213_32) : + { f' | f' = pack_opt params2213_32 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-pack_simpl_correct. @@ -640,15 +640,15 @@ Proof. reflexivity. Defined. -Definition pack (f : fe) : wire_digits := +Definition pack (f : fe2213_32) : wire_digits := Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f). -Definition pack_correct (f : fe) - : pack f = pack_opt params wire_widths_nonneg bits_eq f +Definition pack_correct (f : fe2213_32) + : pack f = pack_opt params2213_32 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f). Definition unpack_simpl_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params2213_32 wire_widths_nonneg bits_eq f }. Proof. cbv [wire_digits] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -662,13 +662,13 @@ Proof. reflexivity. Defined. -Definition unpack_simpl (f : wire_digits) : fe := +Definition unpack_simpl (f : wire_digits) : fe2213_32 := Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6) := f in proj1_sig (unpack_simpl_sig (f0, f1, f2, f3, f4, f5, f6)). Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params wire_widths_nonneg bits_eq f. + : unpack_simpl f = unpack_opt params2213_32 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (unpack_simpl_sig f)). cbv [wire_digits] in *. @@ -677,18 +677,18 @@ Proof. Qed. Definition unpack_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params2213_32 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-unpack_simpl_correct. - rewrite <-(@app_n2_correct fe). + rewrite <-(@app_n2_correct fe2213_32). cbv. reflexivity. Defined. -Definition unpack (f : wire_digits) : fe := +Definition unpack (f : wire_digits) : fe2213_32 := Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f). Definition unpack_correct (f : wire_digits) - : unpack f = unpack_opt params wire_widths_nonneg bits_eq f + : unpack f = unpack_opt params2213_32 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). diff --git a/src/SpecificGen/GF2519_32.v b/src/SpecificGen/GF2519_32.v index ebbf7a24d..9c350a04f 100644 --- a/src/SpecificGen/GF2519_32.v +++ b/src/SpecificGen/GF2519_32.v @@ -25,15 +25,15 @@ Lemma prime_modulus : prime modulus. Admitted. Definition freeze_input_bound := 32%Z. Definition int_width := 32%Z. -Instance params : PseudoMersenneBaseParams modulus. +Instance params2519_32 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 10%nat 251. Defined. -Definition length_fe := Eval compute in length limb_widths. -Definition fe := Eval compute in (tuple Z length_fe). +Definition length_fe2519_32 := Eval compute in length limb_widths. +Definition fe2519_32 := Eval compute in (tuple Z length_fe2519_32). -Definition mul2modulus : fe := - Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params)). +Definition mul2modulus : fe2519_32 := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params2519_32)). Instance subCoeff : SubtractionCoefficient. apply Build_SubtractionCoefficient with (coeff := mul2modulus). @@ -150,24 +150,24 @@ Proof. reflexivity. Qed. -Definition app_n {T} (f : fe) (P : fe -> T) : T. +Definition app_n {T} (f : fe2519_32) (P : fe2519_32 -> T) : T. Proof. - cbv [fe] in *. + cbv [fe2519_32] in *. set (f0 := f). repeat (let g := fresh "g" in destruct f as [f g]). apply P. apply f0. Defined. -Definition app_n_correct {T} f (P : fe -> T) : app_n f P = P f. +Definition app_n_correct {T} f (P : fe2519_32 -> T) : app_n f P = P f. Proof. intros. - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. reflexivity. Qed. -Definition appify2 {T} (op : fe -> fe -> T) (f g : fe) := +Definition appify2 {T} (op : fe2519_32 -> fe2519_32 -> T) (f g : fe2519_32) := app_n f (fun f0 => (app_n g (fun g0 => op f0 g0))). Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g. @@ -176,102 +176,102 @@ Proof. etransitivity; apply app_n_correct. Qed. -Definition uncurry_unop_fe {T} (op : fe -> T) - := Eval compute in Tuple.uncurry (n:=length_fe) op. -Definition curry_unop_fe {T} op : fe -> T - := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe) op). -Definition uncurry_binop_fe {T} (op : fe -> fe -> T) - := Eval compute in uncurry_unop_fe (fun f => uncurry_unop_fe (op f)). -Definition curry_binop_fe {T} op : fe -> fe -> T - := Eval compute in appify2 (fun f => curry_unop_fe (curry_unop_fe op f)). +Definition uncurry_unop_fe2519_32 {T} (op : fe2519_32 -> T) + := Eval compute in Tuple.uncurry (n:=length_fe2519_32) op. +Definition curry_unop_fe2519_32 {T} op : fe2519_32 -> T + := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe2519_32) op). +Definition uncurry_binop_fe2519_32 {T} (op : fe2519_32 -> fe2519_32 -> T) + := Eval compute in uncurry_unop_fe2519_32 (fun f => uncurry_unop_fe2519_32 (op f)). +Definition curry_binop_fe2519_32 {T} op : fe2519_32 -> fe2519_32 -> T + := Eval compute in appify2 (fun f => curry_unop_fe2519_32 (curry_unop_fe2519_32 op f)). Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) := Eval compute in Tuple.uncurry (n:=length wire_widths) op. Definition curry_unop_wire_digits {T} op : wire_digits -> T := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op). -Definition add_sig (f g : fe) : - { fg : fe | fg = add_opt f g}. +Definition add_sig (f g : fe2519_32) : + { fg : fe2519_32 | fg = add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe2519_32). cbv. reflexivity. Defined. -Definition add (f g : fe) : fe := +Definition add (f g : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig add_sig] in proj1_sig (add_sig f g). -Definition add_correct (f g : fe) +Definition add_correct (f g : fe2519_32) : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (add_sig f g). -Definition carry_add_sig (f g : fe) : - { fg : fe | fg = carry_add_opt f g}. +Definition carry_add_sig (f g : fe2519_32) : + { fg : fe2519_32 | fg = carry_add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe2519_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_add (f g : fe) : fe := +Definition carry_add (f g : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj1_sig (carry_add_sig f g). -Definition carry_add_correct (f g : fe) +Definition carry_add_correct (f g : fe2519_32) : carry_add f g = carry_add_opt f g := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj2_sig (carry_add_sig f g). -Definition sub_sig (f g : fe) : - { fg : fe | fg = sub_opt f g}. +Definition sub_sig (f g : fe2519_32) : + { fg : fe2519_32 | fg = sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe2519_32). cbv. reflexivity. Defined. -Definition sub (f g : fe) : fe := +Definition sub (f g : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig sub_sig] in proj1_sig (sub_sig f g). -Definition sub_correct (f g : fe) +Definition sub_correct (f g : fe2519_32) : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). -Definition carry_sub_sig (f g : fe) : - { fg : fe | fg = carry_sub_opt f g}. +Definition carry_sub_sig (f g : fe2519_32) : + { fg : fe2519_32 | fg = carry_sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe2519_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_sub (f g : fe) : fe := +Definition carry_sub (f g : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj1_sig (carry_sub_sig f g). -Definition carry_sub_correct (f g : fe) +Definition carry_sub_correct (f g : fe2519_32) : carry_sub f g = carry_sub_opt f g := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj2_sig (carry_sub_sig f g). (* For multiplication, we add another layer of definition so that we can rewrite under the [let] binders. *) -Definition mul_simpl_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_simpl_sig (f g : fe2519_32) : + { fg : fe2519_32 | fg = carry_mul_opt k_ c_ f g}. Proof. - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. @@ -282,45 +282,45 @@ Proof. reflexivity. Defined. -Definition mul_simpl (f g : fe) : fe := +Definition mul_simpl (f g : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in proj1_sig (mul_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). -Definition mul_simpl_correct (f g : fe) +Definition mul_simpl_correct (f g : fe2519_32) : mul_simpl f g = carry_mul_opt k_ c_ f g. Proof. pose proof (proj2_sig (mul_simpl_sig f g)). - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition mul_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_sig (f g : fe2519_32) : + { fg : fe2519_32 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe2519_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition mul (f g : fe) : fe := +Definition mul (f g : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). -Definition mul_correct (f g : fe) +Definition mul_correct (f g : fe2519_32) : mul f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (mul_sig f g). -Definition opp_sig (f : fe) : - { g : fe | g = opp_opt f }. +Definition opp_sig (f : fe2519_32) : + { g : fe2519_32 | g = opp_opt f }. Proof. eexists. cbv [opp_opt]. @@ -330,15 +330,15 @@ Proof. reflexivity. Defined. -Definition opp (f : fe) : fe +Definition opp (f : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). -Definition opp_correct (f : fe) +Definition opp_correct (f : fe2519_32) : opp f = opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). -Definition carry_opp_sig (f : fe) : - { g : fe | g = carry_opp_opt f }. +Definition carry_opp_sig (f : fe2519_32) : + { g : fe2519_32 | g = carry_opp_opt f }. Proof. eexists. cbv [carry_opp_opt]. @@ -348,16 +348,16 @@ Proof. reflexivity. Defined. -Definition carry_opp (f : fe) : fe +Definition carry_opp (f : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f). -Definition carry_opp_correct (f : fe) +Definition carry_opp_correct (f : fe2519_32) : carry_opp f = carry_opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f). -Definition pow (f : fe) chain := fold_chain_opt one_ mul chain [f]. +Definition pow (f : fe2519_32) chain := fold_chain_opt one_ mul chain [f]. -Lemma pow_correct (f : fe) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. +Lemma pow_correct (f : fe2519_32) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. Proof. cbv [pow pow_opt]; intros. rewrite !fold_chain_opt_correct. @@ -365,8 +365,8 @@ Proof. intros; subst; apply mul_correct. Qed. -Definition inv_sig (f : fe) : - { g : fe | g = inv_opt k_ c_ one_ f }. +Definition inv_sig (f : fe2519_32) : + { g : fe2519_32 | g = inv_opt k_ c_ one_ f }. Proof. eexists; cbv [inv_opt]. rewrite <-pow_correct. @@ -374,10 +374,10 @@ Proof. reflexivity. Defined. -Definition inv (f : fe) : fe +Definition inv (f : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). -Definition inv_correct (f : fe) +Definition inv_correct (f : fe2519_32) : inv f = inv_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f). @@ -388,12 +388,12 @@ Import Morphisms. Local Existing Instance prime_modulus. Lemma field_and_homomorphisms - : @field fe eq zero_ one_ opp add sub mul inv div + : @field fe2519_32 eq zero_ one_ opp add sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ add mul encode + fe2519_32 eq one_ add mul encode /\ @Ring.is_homomorphism - fe eq one_ add mul + fe2519_32 eq one_ add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -411,15 +411,15 @@ Proof. { intros; apply encode_rep. } Qed. -Definition field2519 : @field fe eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. +Definition field2519 : @field fe2519_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. Lemma carry_field_and_homomorphisms - : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div + : @field fe2519_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ carry_add mul encode + fe2519_32 eq one_ carry_add mul encode /\ @Ring.is_homomorphism - fe eq one_ carry_add mul + fe2519_32 eq one_ carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -437,29 +437,29 @@ Proof. { intros; apply encode_rep. } Qed. -Definition carry_field : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. +Definition carry_field : @field fe2519_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. Lemma homomorphism_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe2519_32 eq one add mul encode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_F_decode - : @Ring.is_homomorphism fe eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe2519_32 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one carry_add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe2519_32 eq one carry_add mul encode. Proof. apply carry_field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_decode - : @Ring.is_homomorphism fe eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe2519_32 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply carry_field_and_homomorphisms. Qed. -Definition ge_modulus_sig (f : fe) : +Definition ge_modulus_sig (f : fe2519_32) : { b : Z | b = ge_modulus_opt (to_list 10 f) }. Proof. - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [ge_modulus_opt]. rewrite !modulus_digits_subst. @@ -467,24 +467,24 @@ Proof. reflexivity. Defined. -Definition ge_modulus (f : fe) : Z := +Definition ge_modulus (f : fe2519_32) : Z := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in proj1_sig (ge_modulus_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). -Definition ge_modulus_correct (f : fe) : +Definition ge_modulus_correct (f : fe2519_32) : ge_modulus f = ge_modulus_opt (to_list 10 f). Proof. pose proof (proj2_sig (ge_modulus_sig f)). - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition freeze_sig (f : fe) : - { f' : fe | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }. +Definition freeze_sig (f : fe2519_32) : + { f' : fe2519_32 | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }. Proof. - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [freeze_opt int_width]. cbv [to_list to_list']. @@ -499,38 +499,38 @@ Proof. reflexivity. Defined. -Definition freeze (f : fe) : fe := +Definition freeze (f : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig freeze_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). -Definition freeze_correct (f : fe) +Definition freeze_correct (f : fe2519_32) : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)). Proof. pose proof (proj2_sig (freeze_sig f)). - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition fieldwiseb_sig (f g : fe) : +Definition fieldwiseb_sig (f g : fe2519_32) : { b | b = @fieldwiseb Z Z 10 Z.eqb f g }. Proof. - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. reflexivity. Defined. -Definition fieldwiseb (f g : fe) : bool +Definition fieldwiseb (f g : fe2519_32) : bool := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in proj1_sig (fieldwiseb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). -Lemma fieldwiseb_correct (f g : fe) +Lemma fieldwiseb_correct (f g : fe2519_32) : fieldwiseb f g = @Tuple.fieldwiseb Z Z 10 Z.eqb f g. Proof. set (f' := f); set (g' := g). @@ -538,11 +538,11 @@ Proof. exact (proj2_sig (fieldwiseb_sig f' g')). Qed. -Definition eqb_sig (f g : fe) : +Definition eqb_sig (f g : fe2519_32) : { b | b = eqb int_width f g }. Proof. cbv [eqb]. - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [ModularBaseSystem.freeze int_width]. @@ -553,14 +553,14 @@ Proof. reflexivity. Defined. -Definition eqb (f g : fe) : bool +Definition eqb (f g : fe2519_32) : bool := Eval cbv beta iota delta [proj1_sig eqb_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in proj1_sig (eqb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). -Lemma eqb_correct (f g : fe) +Lemma eqb_correct (f g : fe2519_32) : eqb f g = ModularBaseSystem.eqb int_width f g. Proof. set (f' := f); set (g' := g). @@ -568,8 +568,8 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Definition sqrt_sig (f : fe) : - { f' : fe | f' = sqrt_3mod4_opt k_ c_ one_ f}. +Definition sqrt_sig (f : fe2519_32) : + { f' : fe2519_32 | f' = sqrt_3mod4_opt k_ c_ one_ f}. Proof. eexists. cbv [sqrt_3mod4_opt int_width]. @@ -577,17 +577,17 @@ Proof. reflexivity. Defined. -Definition sqrt (f : fe) : fe +Definition sqrt (f : fe2519_32) : fe2519_32 := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig f). -Definition sqrt_correct (f : fe) +Definition sqrt_correct (f : fe2519_32) : sqrt f = sqrt_3mod4_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig f). -Definition pack_simpl_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_simpl_sig (f : fe2519_32) : + { f' | f' = pack_opt params2519_32 wire_widths_nonneg bits_eq f }. Proof. - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [pack_opt]. @@ -598,22 +598,22 @@ Proof. reflexivity. Defined. -Definition pack_simpl (f : fe) := +Definition pack_simpl (f : fe2519_32) := Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in proj1_sig (pack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). -Definition pack_simpl_correct (f : fe) - : pack_simpl f = pack_opt params wire_widths_nonneg bits_eq f. +Definition pack_simpl_correct (f : fe2519_32) + : pack_simpl f = pack_opt params2519_32 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (pack_simpl_sig f)). - cbv [fe] in *. + cbv [fe2519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition pack_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_sig (f : fe2519_32) : + { f' | f' = pack_opt params2519_32 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-pack_simpl_correct. @@ -622,15 +622,15 @@ Proof. reflexivity. Defined. -Definition pack (f : fe) : wire_digits := +Definition pack (f : fe2519_32) : wire_digits := Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f). -Definition pack_correct (f : fe) - : pack f = pack_opt params wire_widths_nonneg bits_eq f +Definition pack_correct (f : fe2519_32) + : pack f = pack_opt params2519_32 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f). Definition unpack_simpl_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params2519_32 wire_widths_nonneg bits_eq f }. Proof. cbv [wire_digits] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -644,13 +644,13 @@ Proof. reflexivity. Defined. -Definition unpack_simpl (f : wire_digits) : fe := +Definition unpack_simpl (f : wire_digits) : fe2519_32 := Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in proj1_sig (unpack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7)). Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params wire_widths_nonneg bits_eq f. + : unpack_simpl f = unpack_opt params2519_32 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (unpack_simpl_sig f)). cbv [wire_digits] in *. @@ -659,18 +659,18 @@ Proof. Qed. Definition unpack_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params2519_32 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-unpack_simpl_correct. - rewrite <-(@app_n2_correct fe). + rewrite <-(@app_n2_correct fe2519_32). cbv. reflexivity. Defined. -Definition unpack (f : wire_digits) : fe := +Definition unpack (f : wire_digits) : fe2519_32 := Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f). Definition unpack_correct (f : wire_digits) - : unpack f = unpack_opt params wire_widths_nonneg bits_eq f + : unpack f = unpack_opt params2519_32 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). diff --git a/src/SpecificGen/GF25519_32.v b/src/SpecificGen/GF25519_32.v index 80e51c2d7..ba2e76a0b 100644 --- a/src/SpecificGen/GF25519_32.v +++ b/src/SpecificGen/GF25519_32.v @@ -25,15 +25,15 @@ Lemma prime_modulus : prime modulus. Admitted. Definition freeze_input_bound := 32%Z. Definition int_width := 32%Z. -Instance params : PseudoMersenneBaseParams modulus. +Instance params25519_32 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 10%nat 255. Defined. -Definition length_fe := Eval compute in length limb_widths. -Definition fe := Eval compute in (tuple Z length_fe). +Definition length_fe25519_32 := Eval compute in length limb_widths. +Definition fe25519_32 := Eval compute in (tuple Z length_fe25519_32). -Definition mul2modulus : fe := - Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params)). +Definition mul2modulus : fe25519_32 := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params25519_32)). Instance subCoeff : SubtractionCoefficient. apply Build_SubtractionCoefficient with (coeff := mul2modulus). @@ -150,24 +150,24 @@ Proof. reflexivity. Qed. -Definition app_n {T} (f : fe) (P : fe -> T) : T. +Definition app_n {T} (f : fe25519_32) (P : fe25519_32 -> T) : T. Proof. - cbv [fe] in *. + cbv [fe25519_32] in *. set (f0 := f). repeat (let g := fresh "g" in destruct f as [f g]). apply P. apply f0. Defined. -Definition app_n_correct {T} f (P : fe -> T) : app_n f P = P f. +Definition app_n_correct {T} f (P : fe25519_32 -> T) : app_n f P = P f. Proof. intros. - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. reflexivity. Qed. -Definition appify2 {T} (op : fe -> fe -> T) (f g : fe) := +Definition appify2 {T} (op : fe25519_32 -> fe25519_32 -> T) (f g : fe25519_32) := app_n f (fun f0 => (app_n g (fun g0 => op f0 g0))). Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g. @@ -176,102 +176,102 @@ Proof. etransitivity; apply app_n_correct. Qed. -Definition uncurry_unop_fe {T} (op : fe -> T) - := Eval compute in Tuple.uncurry (n:=length_fe) op. -Definition curry_unop_fe {T} op : fe -> T - := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe) op). -Definition uncurry_binop_fe {T} (op : fe -> fe -> T) - := Eval compute in uncurry_unop_fe (fun f => uncurry_unop_fe (op f)). -Definition curry_binop_fe {T} op : fe -> fe -> T - := Eval compute in appify2 (fun f => curry_unop_fe (curry_unop_fe op f)). +Definition uncurry_unop_fe25519_32 {T} (op : fe25519_32 -> T) + := Eval compute in Tuple.uncurry (n:=length_fe25519_32) op. +Definition curry_unop_fe25519_32 {T} op : fe25519_32 -> T + := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe25519_32) op). +Definition uncurry_binop_fe25519_32 {T} (op : fe25519_32 -> fe25519_32 -> T) + := Eval compute in uncurry_unop_fe25519_32 (fun f => uncurry_unop_fe25519_32 (op f)). +Definition curry_binop_fe25519_32 {T} op : fe25519_32 -> fe25519_32 -> T + := Eval compute in appify2 (fun f => curry_unop_fe25519_32 (curry_unop_fe25519_32 op f)). Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) := Eval compute in Tuple.uncurry (n:=length wire_widths) op. Definition curry_unop_wire_digits {T} op : wire_digits -> T := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op). -Definition add_sig (f g : fe) : - { fg : fe | fg = add_opt f g}. +Definition add_sig (f g : fe25519_32) : + { fg : fe25519_32 | fg = add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe25519_32). cbv. reflexivity. Defined. -Definition add (f g : fe) : fe := +Definition add (f g : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig add_sig] in proj1_sig (add_sig f g). -Definition add_correct (f g : fe) +Definition add_correct (f g : fe25519_32) : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (add_sig f g). -Definition carry_add_sig (f g : fe) : - { fg : fe | fg = carry_add_opt f g}. +Definition carry_add_sig (f g : fe25519_32) : + { fg : fe25519_32 | fg = carry_add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe25519_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_add (f g : fe) : fe := +Definition carry_add (f g : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj1_sig (carry_add_sig f g). -Definition carry_add_correct (f g : fe) +Definition carry_add_correct (f g : fe25519_32) : carry_add f g = carry_add_opt f g := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj2_sig (carry_add_sig f g). -Definition sub_sig (f g : fe) : - { fg : fe | fg = sub_opt f g}. +Definition sub_sig (f g : fe25519_32) : + { fg : fe25519_32 | fg = sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe25519_32). cbv. reflexivity. Defined. -Definition sub (f g : fe) : fe := +Definition sub (f g : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig sub_sig] in proj1_sig (sub_sig f g). -Definition sub_correct (f g : fe) +Definition sub_correct (f g : fe25519_32) : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). -Definition carry_sub_sig (f g : fe) : - { fg : fe | fg = carry_sub_opt f g}. +Definition carry_sub_sig (f g : fe25519_32) : + { fg : fe25519_32 | fg = carry_sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe25519_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_sub (f g : fe) : fe := +Definition carry_sub (f g : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj1_sig (carry_sub_sig f g). -Definition carry_sub_correct (f g : fe) +Definition carry_sub_correct (f g : fe25519_32) : carry_sub f g = carry_sub_opt f g := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj2_sig (carry_sub_sig f g). (* For multiplication, we add another layer of definition so that we can rewrite under the [let] binders. *) -Definition mul_simpl_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_simpl_sig (f g : fe25519_32) : + { fg : fe25519_32 | fg = carry_mul_opt k_ c_ f g}. Proof. - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. @@ -282,45 +282,45 @@ Proof. reflexivity. Defined. -Definition mul_simpl (f g : fe) : fe := +Definition mul_simpl (f g : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in proj1_sig (mul_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). -Definition mul_simpl_correct (f g : fe) +Definition mul_simpl_correct (f g : fe25519_32) : mul_simpl f g = carry_mul_opt k_ c_ f g. Proof. pose proof (proj2_sig (mul_simpl_sig f g)). - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition mul_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_sig (f g : fe25519_32) : + { fg : fe25519_32 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe25519_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition mul (f g : fe) : fe := +Definition mul (f g : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). -Definition mul_correct (f g : fe) +Definition mul_correct (f g : fe25519_32) : mul f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (mul_sig f g). -Definition opp_sig (f : fe) : - { g : fe | g = opp_opt f }. +Definition opp_sig (f : fe25519_32) : + { g : fe25519_32 | g = opp_opt f }. Proof. eexists. cbv [opp_opt]. @@ -330,15 +330,15 @@ Proof. reflexivity. Defined. -Definition opp (f : fe) : fe +Definition opp (f : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). -Definition opp_correct (f : fe) +Definition opp_correct (f : fe25519_32) : opp f = opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). -Definition carry_opp_sig (f : fe) : - { g : fe | g = carry_opp_opt f }. +Definition carry_opp_sig (f : fe25519_32) : + { g : fe25519_32 | g = carry_opp_opt f }. Proof. eexists. cbv [carry_opp_opt]. @@ -348,16 +348,16 @@ Proof. reflexivity. Defined. -Definition carry_opp (f : fe) : fe +Definition carry_opp (f : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f). -Definition carry_opp_correct (f : fe) +Definition carry_opp_correct (f : fe25519_32) : carry_opp f = carry_opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f). -Definition pow (f : fe) chain := fold_chain_opt one_ mul chain [f]. +Definition pow (f : fe25519_32) chain := fold_chain_opt one_ mul chain [f]. -Lemma pow_correct (f : fe) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. +Lemma pow_correct (f : fe25519_32) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. Proof. cbv [pow pow_opt]; intros. rewrite !fold_chain_opt_correct. @@ -382,8 +382,8 @@ Qed. Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb. -Definition inv_sig (f : fe) : - { g : fe | g = inv_opt k_ c_ one_ f }. +Definition inv_sig (f : fe25519_32) : + { g : fe25519_32 | g = inv_opt k_ c_ one_ f }. Proof. eexists; cbv [inv_opt]. rewrite <-pow_correct. @@ -391,10 +391,10 @@ Proof. reflexivity. Defined. -Definition inv (f : fe) : fe +Definition inv (f : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). -Definition inv_correct (f : fe) +Definition inv_correct (f : fe25519_32) : inv f = inv_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f). @@ -405,12 +405,12 @@ Import Morphisms. Local Existing Instance prime_modulus. Lemma field_and_homomorphisms - : @field fe eq zero_ one_ opp add sub mul inv div + : @field fe25519_32 eq zero_ one_ opp add sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ add mul encode + fe25519_32 eq one_ add mul encode /\ @Ring.is_homomorphism - fe eq one_ add mul + fe25519_32 eq one_ add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -428,15 +428,15 @@ Proof. { intros; apply encode_rep. } Qed. -Definition field25519 : @field fe eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. +Definition field25519 : @field fe25519_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. Lemma carry_field_and_homomorphisms - : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div + : @field fe25519_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ carry_add mul encode + fe25519_32 eq one_ carry_add mul encode /\ @Ring.is_homomorphism - fe eq one_ carry_add mul + fe25519_32 eq one_ carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -454,29 +454,29 @@ Proof. { intros; apply encode_rep. } Qed. -Definition carry_field : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. +Definition carry_field : @field fe25519_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. Lemma homomorphism_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe25519_32 eq one add mul encode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_F_decode - : @Ring.is_homomorphism fe eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe25519_32 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one carry_add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe25519_32 eq one carry_add mul encode. Proof. apply carry_field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_decode - : @Ring.is_homomorphism fe eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe25519_32 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply carry_field_and_homomorphisms. Qed. -Definition ge_modulus_sig (f : fe) : +Definition ge_modulus_sig (f : fe25519_32) : { b : Z | b = ge_modulus_opt (to_list 10 f) }. Proof. - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [ge_modulus_opt]. rewrite !modulus_digits_subst. @@ -484,24 +484,24 @@ Proof. reflexivity. Defined. -Definition ge_modulus (f : fe) : Z := +Definition ge_modulus (f : fe25519_32) : Z := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in proj1_sig (ge_modulus_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). -Definition ge_modulus_correct (f : fe) : +Definition ge_modulus_correct (f : fe25519_32) : ge_modulus f = ge_modulus_opt (to_list 10 f). Proof. pose proof (proj2_sig (ge_modulus_sig f)). - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition freeze_sig (f : fe) : - { f' : fe | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }. +Definition freeze_sig (f : fe25519_32) : + { f' : fe25519_32 | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }. Proof. - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [freeze_opt int_width]. cbv [to_list to_list']. @@ -516,38 +516,38 @@ Proof. reflexivity. Defined. -Definition freeze (f : fe) : fe := +Definition freeze (f : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig freeze_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). -Definition freeze_correct (f : fe) +Definition freeze_correct (f : fe25519_32) : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)). Proof. pose proof (proj2_sig (freeze_sig f)). - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition fieldwiseb_sig (f g : fe) : +Definition fieldwiseb_sig (f g : fe25519_32) : { b | b = @fieldwiseb Z Z 10 Z.eqb f g }. Proof. - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. reflexivity. Defined. -Definition fieldwiseb (f g : fe) : bool +Definition fieldwiseb (f g : fe25519_32) : bool := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in proj1_sig (fieldwiseb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). -Lemma fieldwiseb_correct (f g : fe) +Lemma fieldwiseb_correct (f g : fe25519_32) : fieldwiseb f g = @Tuple.fieldwiseb Z Z 10 Z.eqb f g. Proof. set (f' := f); set (g' := g). @@ -555,11 +555,11 @@ Proof. exact (proj2_sig (fieldwiseb_sig f' g')). Qed. -Definition eqb_sig (f g : fe) : +Definition eqb_sig (f g : fe25519_32) : { b | b = eqb int_width f g }. Proof. cbv [eqb]. - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [ModularBaseSystem.freeze int_width]. @@ -570,14 +570,14 @@ Proof. reflexivity. Defined. -Definition eqb (f g : fe) : bool +Definition eqb (f g : fe25519_32) : bool := Eval cbv beta iota delta [proj1_sig eqb_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9) := g in proj1_sig (eqb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9)). -Lemma eqb_correct (f g : fe) +Lemma eqb_correct (f g : fe25519_32) : eqb f g = ModularBaseSystem.eqb int_width f g. Proof. set (f' := f); set (g' := g). @@ -585,8 +585,8 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Definition sqrt_sig (powx powx_squared f : fe) : - { f' : fe | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powx powx_squared f}. +Definition sqrt_sig (powx powx_squared f : fe25519_32) : + { f' : fe25519_32 | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powx powx_squared f}. Proof. eexists. cbv [sqrt_5mod8_opt int_width]. @@ -595,17 +595,17 @@ Proof. reflexivity. Defined. -Definition sqrt (powx powx_squared f : fe) : fe +Definition sqrt (powx powx_squared f : fe25519_32) : fe25519_32 := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig powx powx_squared f). -Definition sqrt_correct (powx powx_squared f : fe) +Definition sqrt_correct (powx powx_squared f : fe25519_32) : sqrt powx powx_squared f = sqrt_5mod8_opt k_ c_ sqrt_m1 powx powx_squared f := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig powx powx_squared f). -Definition pack_simpl_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_simpl_sig (f : fe25519_32) : + { f' | f' = pack_opt params25519_32 wire_widths_nonneg bits_eq f }. Proof. - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [pack_opt]. @@ -616,22 +616,22 @@ Proof. reflexivity. Defined. -Definition pack_simpl (f : fe) := +Definition pack_simpl (f : fe25519_32) := Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in proj1_sig (pack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). -Definition pack_simpl_correct (f : fe) - : pack_simpl f = pack_opt params wire_widths_nonneg bits_eq f. +Definition pack_simpl_correct (f : fe25519_32) + : pack_simpl f = pack_opt params25519_32 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (pack_simpl_sig f)). - cbv [fe] in *. + cbv [fe25519_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition pack_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_sig (f : fe25519_32) : + { f' | f' = pack_opt params25519_32 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-pack_simpl_correct. @@ -640,15 +640,15 @@ Proof. reflexivity. Defined. -Definition pack (f : fe) : wire_digits := +Definition pack (f : fe25519_32) : wire_digits := Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f). -Definition pack_correct (f : fe) - : pack f = pack_opt params wire_widths_nonneg bits_eq f +Definition pack_correct (f : fe25519_32) + : pack f = pack_opt params25519_32 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f). Definition unpack_simpl_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params25519_32 wire_widths_nonneg bits_eq f }. Proof. cbv [wire_digits] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -662,13 +662,13 @@ Proof. reflexivity. Defined. -Definition unpack_simpl (f : wire_digits) : fe := +Definition unpack_simpl (f : wire_digits) : fe25519_32 := Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in proj1_sig (unpack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7)). Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params wire_widths_nonneg bits_eq f. + : unpack_simpl f = unpack_opt params25519_32 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (unpack_simpl_sig f)). cbv [wire_digits] in *. @@ -677,18 +677,18 @@ Proof. Qed. Definition unpack_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params25519_32 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-unpack_simpl_correct. - rewrite <-(@app_n2_correct fe). + rewrite <-(@app_n2_correct fe25519_32). cbv. reflexivity. Defined. -Definition unpack (f : wire_digits) : fe := +Definition unpack (f : wire_digits) : fe25519_32 := Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f). Definition unpack_correct (f : wire_digits) - : unpack f = unpack_opt params wire_widths_nonneg bits_eq f + : unpack f = unpack_opt params25519_32 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). diff --git a/src/SpecificGen/GF25519_64.v b/src/SpecificGen/GF25519_64.v index 134090d0e..d5970edea 100644 --- a/src/SpecificGen/GF25519_64.v +++ b/src/SpecificGen/GF25519_64.v @@ -25,15 +25,15 @@ Lemma prime_modulus : prime modulus. Admitted. Definition freeze_input_bound := 64%Z. Definition int_width := 64%Z. -Instance params : PseudoMersenneBaseParams modulus. +Instance params25519_64 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 5%nat 255. Defined. -Definition length_fe := Eval compute in length limb_widths. -Definition fe := Eval compute in (tuple Z length_fe). +Definition length_fe25519_64 := Eval compute in length limb_widths. +Definition fe25519_64 := Eval compute in (tuple Z length_fe25519_64). -Definition mul2modulus : fe := - Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params)). +Definition mul2modulus : fe25519_64 := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params25519_64)). Instance subCoeff : SubtractionCoefficient. apply Build_SubtractionCoefficient with (coeff := mul2modulus). @@ -150,24 +150,24 @@ Proof. reflexivity. Qed. -Definition app_n {T} (f : fe) (P : fe -> T) : T. +Definition app_n {T} (f : fe25519_64) (P : fe25519_64 -> T) : T. Proof. - cbv [fe] in *. + cbv [fe25519_64] in *. set (f0 := f). repeat (let g := fresh "g" in destruct f as [f g]). apply P. apply f0. Defined. -Definition app_n_correct {T} f (P : fe -> T) : app_n f P = P f. +Definition app_n_correct {T} f (P : fe25519_64 -> T) : app_n f P = P f. Proof. intros. - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. reflexivity. Qed. -Definition appify2 {T} (op : fe -> fe -> T) (f g : fe) := +Definition appify2 {T} (op : fe25519_64 -> fe25519_64 -> T) (f g : fe25519_64) := app_n f (fun f0 => (app_n g (fun g0 => op f0 g0))). Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g. @@ -176,102 +176,102 @@ Proof. etransitivity; apply app_n_correct. Qed. -Definition uncurry_unop_fe {T} (op : fe -> T) - := Eval compute in Tuple.uncurry (n:=length_fe) op. -Definition curry_unop_fe {T} op : fe -> T - := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe) op). -Definition uncurry_binop_fe {T} (op : fe -> fe -> T) - := Eval compute in uncurry_unop_fe (fun f => uncurry_unop_fe (op f)). -Definition curry_binop_fe {T} op : fe -> fe -> T - := Eval compute in appify2 (fun f => curry_unop_fe (curry_unop_fe op f)). +Definition uncurry_unop_fe25519_64 {T} (op : fe25519_64 -> T) + := Eval compute in Tuple.uncurry (n:=length_fe25519_64) op. +Definition curry_unop_fe25519_64 {T} op : fe25519_64 -> T + := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe25519_64) op). +Definition uncurry_binop_fe25519_64 {T} (op : fe25519_64 -> fe25519_64 -> T) + := Eval compute in uncurry_unop_fe25519_64 (fun f => uncurry_unop_fe25519_64 (op f)). +Definition curry_binop_fe25519_64 {T} op : fe25519_64 -> fe25519_64 -> T + := Eval compute in appify2 (fun f => curry_unop_fe25519_64 (curry_unop_fe25519_64 op f)). Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) := Eval compute in Tuple.uncurry (n:=length wire_widths) op. Definition curry_unop_wire_digits {T} op : wire_digits -> T := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op). -Definition add_sig (f g : fe) : - { fg : fe | fg = add_opt f g}. +Definition add_sig (f g : fe25519_64) : + { fg : fe25519_64 | fg = add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe25519_64). cbv. reflexivity. Defined. -Definition add (f g : fe) : fe := +Definition add (f g : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig add_sig] in proj1_sig (add_sig f g). -Definition add_correct (f g : fe) +Definition add_correct (f g : fe25519_64) : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (add_sig f g). -Definition carry_add_sig (f g : fe) : - { fg : fe | fg = carry_add_opt f g}. +Definition carry_add_sig (f g : fe25519_64) : + { fg : fe25519_64 | fg = carry_add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe25519_64). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_add (f g : fe) : fe := +Definition carry_add (f g : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj1_sig (carry_add_sig f g). -Definition carry_add_correct (f g : fe) +Definition carry_add_correct (f g : fe25519_64) : carry_add f g = carry_add_opt f g := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj2_sig (carry_add_sig f g). -Definition sub_sig (f g : fe) : - { fg : fe | fg = sub_opt f g}. +Definition sub_sig (f g : fe25519_64) : + { fg : fe25519_64 | fg = sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe25519_64). cbv. reflexivity. Defined. -Definition sub (f g : fe) : fe := +Definition sub (f g : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig sub_sig] in proj1_sig (sub_sig f g). -Definition sub_correct (f g : fe) +Definition sub_correct (f g : fe25519_64) : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). -Definition carry_sub_sig (f g : fe) : - { fg : fe | fg = carry_sub_opt f g}. +Definition carry_sub_sig (f g : fe25519_64) : + { fg : fe25519_64 | fg = carry_sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe25519_64). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_sub (f g : fe) : fe := +Definition carry_sub (f g : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj1_sig (carry_sub_sig f g). -Definition carry_sub_correct (f g : fe) +Definition carry_sub_correct (f g : fe25519_64) : carry_sub f g = carry_sub_opt f g := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj2_sig (carry_sub_sig f g). (* For multiplication, we add another layer of definition so that we can rewrite under the [let] binders. *) -Definition mul_simpl_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_simpl_sig (f g : fe25519_64) : + { fg : fe25519_64 | fg = carry_mul_opt k_ c_ f g}. Proof. - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. @@ -282,45 +282,45 @@ Proof. reflexivity. Defined. -Definition mul_simpl (f g : fe) : fe := +Definition mul_simpl (f g : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in let '(f0, f1, f2, f3, f4) := f in let '(g0, g1, g2, g3, g4) := g in proj1_sig (mul_simpl_sig (f0, f1, f2, f3, f4) (g0, g1, g2, g3, g4)). -Definition mul_simpl_correct (f g : fe) +Definition mul_simpl_correct (f g : fe25519_64) : mul_simpl f g = carry_mul_opt k_ c_ f g. Proof. pose proof (proj2_sig (mul_simpl_sig f g)). - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition mul_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_sig (f g : fe25519_64) : + { fg : fe25519_64 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe25519_64). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition mul (f g : fe) : fe := +Definition mul (f g : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). -Definition mul_correct (f g : fe) +Definition mul_correct (f g : fe25519_64) : mul f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (mul_sig f g). -Definition opp_sig (f : fe) : - { g : fe | g = opp_opt f }. +Definition opp_sig (f : fe25519_64) : + { g : fe25519_64 | g = opp_opt f }. Proof. eexists. cbv [opp_opt]. @@ -330,15 +330,15 @@ Proof. reflexivity. Defined. -Definition opp (f : fe) : fe +Definition opp (f : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). -Definition opp_correct (f : fe) +Definition opp_correct (f : fe25519_64) : opp f = opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). -Definition carry_opp_sig (f : fe) : - { g : fe | g = carry_opp_opt f }. +Definition carry_opp_sig (f : fe25519_64) : + { g : fe25519_64 | g = carry_opp_opt f }. Proof. eexists. cbv [carry_opp_opt]. @@ -348,16 +348,16 @@ Proof. reflexivity. Defined. -Definition carry_opp (f : fe) : fe +Definition carry_opp (f : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f). -Definition carry_opp_correct (f : fe) +Definition carry_opp_correct (f : fe25519_64) : carry_opp f = carry_opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f). -Definition pow (f : fe) chain := fold_chain_opt one_ mul chain [f]. +Definition pow (f : fe25519_64) chain := fold_chain_opt one_ mul chain [f]. -Lemma pow_correct (f : fe) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. +Lemma pow_correct (f : fe25519_64) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. Proof. cbv [pow pow_opt]; intros. rewrite !fold_chain_opt_correct. @@ -382,8 +382,8 @@ Qed. Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb. -Definition inv_sig (f : fe) : - { g : fe | g = inv_opt k_ c_ one_ f }. +Definition inv_sig (f : fe25519_64) : + { g : fe25519_64 | g = inv_opt k_ c_ one_ f }. Proof. eexists; cbv [inv_opt]. rewrite <-pow_correct. @@ -391,10 +391,10 @@ Proof. reflexivity. Defined. -Definition inv (f : fe) : fe +Definition inv (f : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). -Definition inv_correct (f : fe) +Definition inv_correct (f : fe25519_64) : inv f = inv_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f). @@ -405,12 +405,12 @@ Import Morphisms. Local Existing Instance prime_modulus. Lemma field_and_homomorphisms - : @field fe eq zero_ one_ opp add sub mul inv div + : @field fe25519_64 eq zero_ one_ opp add sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ add mul encode + fe25519_64 eq one_ add mul encode /\ @Ring.is_homomorphism - fe eq one_ add mul + fe25519_64 eq one_ add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -428,15 +428,15 @@ Proof. { intros; apply encode_rep. } Qed. -Definition field25519 : @field fe eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. +Definition field25519 : @field fe25519_64 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. Lemma carry_field_and_homomorphisms - : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div + : @field fe25519_64 eq zero_ one_ carry_opp carry_add carry_sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ carry_add mul encode + fe25519_64 eq one_ carry_add mul encode /\ @Ring.is_homomorphism - fe eq one_ carry_add mul + fe25519_64 eq one_ carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -454,29 +454,29 @@ Proof. { intros; apply encode_rep. } Qed. -Definition carry_field : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. +Definition carry_field : @field fe25519_64 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. Lemma homomorphism_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe25519_64 eq one add mul encode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_F_decode - : @Ring.is_homomorphism fe eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe25519_64 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one carry_add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe25519_64 eq one carry_add mul encode. Proof. apply carry_field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_decode - : @Ring.is_homomorphism fe eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe25519_64 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply carry_field_and_homomorphisms. Qed. -Definition ge_modulus_sig (f : fe) : +Definition ge_modulus_sig (f : fe25519_64) : { b : Z | b = ge_modulus_opt (to_list 5 f) }. Proof. - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [ge_modulus_opt]. rewrite !modulus_digits_subst. @@ -484,24 +484,24 @@ Proof. reflexivity. Defined. -Definition ge_modulus (f : fe) : Z := +Definition ge_modulus (f : fe25519_64) : Z := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in let '(f0, f1, f2, f3, f4) := f in proj1_sig (ge_modulus_sig (f0, f1, f2, f3, f4)). -Definition ge_modulus_correct (f : fe) : +Definition ge_modulus_correct (f : fe25519_64) : ge_modulus f = ge_modulus_opt (to_list 5 f). Proof. pose proof (proj2_sig (ge_modulus_sig f)). - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition freeze_sig (f : fe) : - { f' : fe | f' = from_list_default 0 5 (freeze_opt (int_width := int_width) c_ (to_list 5 f)) }. +Definition freeze_sig (f : fe25519_64) : + { f' : fe25519_64 | f' = from_list_default 0 5 (freeze_opt (int_width := int_width) c_ (to_list 5 f)) }. Proof. - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [freeze_opt int_width]. cbv [to_list to_list']. @@ -516,38 +516,38 @@ Proof. reflexivity. Defined. -Definition freeze (f : fe) : fe := +Definition freeze (f : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig freeze_sig] in let '(f0, f1, f2, f3, f4) := f in proj1_sig (freeze_sig (f0, f1, f2, f3, f4)). -Definition freeze_correct (f : fe) +Definition freeze_correct (f : fe25519_64) : freeze f = from_list_default 0 5 (freeze_opt (int_width := int_width) c_ (to_list 5 f)). Proof. pose proof (proj2_sig (freeze_sig f)). - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition fieldwiseb_sig (f g : fe) : +Definition fieldwiseb_sig (f g : fe25519_64) : { b | b = @fieldwiseb Z Z 5 Z.eqb f g }. Proof. - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. reflexivity. Defined. -Definition fieldwiseb (f g : fe) : bool +Definition fieldwiseb (f g : fe25519_64) : bool := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in let '(f0, f1, f2, f3, f4) := f in let '(g0, g1, g2, g3, g4) := g in proj1_sig (fieldwiseb_sig (f0, f1, f2, f3, f4) (g0, g1, g2, g3, g4)). -Lemma fieldwiseb_correct (f g : fe) +Lemma fieldwiseb_correct (f g : fe25519_64) : fieldwiseb f g = @Tuple.fieldwiseb Z Z 5 Z.eqb f g. Proof. set (f' := f); set (g' := g). @@ -555,11 +555,11 @@ Proof. exact (proj2_sig (fieldwiseb_sig f' g')). Qed. -Definition eqb_sig (f g : fe) : +Definition eqb_sig (f g : fe25519_64) : { b | b = eqb int_width f g }. Proof. cbv [eqb]. - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [ModularBaseSystem.freeze int_width]. @@ -570,14 +570,14 @@ Proof. reflexivity. Defined. -Definition eqb (f g : fe) : bool +Definition eqb (f g : fe25519_64) : bool := Eval cbv beta iota delta [proj1_sig eqb_sig] in let '(f0, f1, f2, f3, f4) := f in let '(g0, g1, g2, g3, g4) := g in proj1_sig (eqb_sig (f0, f1, f2, f3, f4) (g0, g1, g2, g3, g4)). -Lemma eqb_correct (f g : fe) +Lemma eqb_correct (f g : fe25519_64) : eqb f g = ModularBaseSystem.eqb int_width f g. Proof. set (f' := f); set (g' := g). @@ -585,8 +585,8 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Definition sqrt_sig (powx powx_squared f : fe) : - { f' : fe | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powx powx_squared f}. +Definition sqrt_sig (powx powx_squared f : fe25519_64) : + { f' : fe25519_64 | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powx powx_squared f}. Proof. eexists. cbv [sqrt_5mod8_opt int_width]. @@ -595,17 +595,17 @@ Proof. reflexivity. Defined. -Definition sqrt (powx powx_squared f : fe) : fe +Definition sqrt (powx powx_squared f : fe25519_64) : fe25519_64 := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig powx powx_squared f). -Definition sqrt_correct (powx powx_squared f : fe) +Definition sqrt_correct (powx powx_squared f : fe25519_64) : sqrt powx powx_squared f = sqrt_5mod8_opt k_ c_ sqrt_m1 powx powx_squared f := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig powx powx_squared f). -Definition pack_simpl_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_simpl_sig (f : fe25519_64) : + { f' | f' = pack_opt params25519_64 wire_widths_nonneg bits_eq f }. Proof. - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [pack_opt]. @@ -616,22 +616,22 @@ Proof. reflexivity. Defined. -Definition pack_simpl (f : fe) := +Definition pack_simpl (f : fe25519_64) := Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in let '(f0, f1, f2, f3, f4) := f in proj1_sig (pack_simpl_sig (f0, f1, f2, f3, f4)). -Definition pack_simpl_correct (f : fe) - : pack_simpl f = pack_opt params wire_widths_nonneg bits_eq f. +Definition pack_simpl_correct (f : fe25519_64) + : pack_simpl f = pack_opt params25519_64 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (pack_simpl_sig f)). - cbv [fe] in *. + cbv [fe25519_64] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition pack_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_sig (f : fe25519_64) : + { f' | f' = pack_opt params25519_64 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-pack_simpl_correct. @@ -640,15 +640,15 @@ Proof. reflexivity. Defined. -Definition pack (f : fe) : wire_digits := +Definition pack (f : fe25519_64) : wire_digits := Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f). -Definition pack_correct (f : fe) - : pack f = pack_opt params wire_widths_nonneg bits_eq f +Definition pack_correct (f : fe25519_64) + : pack f = pack_opt params25519_64 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f). Definition unpack_simpl_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params25519_64 wire_widths_nonneg bits_eq f }. Proof. cbv [wire_digits] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -662,13 +662,13 @@ Proof. reflexivity. Defined. -Definition unpack_simpl (f : wire_digits) : fe := +Definition unpack_simpl (f : wire_digits) : fe25519_64 := Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in let '(f0, f1, f2, f3) := f in proj1_sig (unpack_simpl_sig (f0, f1, f2, f3)). Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params wire_widths_nonneg bits_eq f. + : unpack_simpl f = unpack_opt params25519_64 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (unpack_simpl_sig f)). cbv [wire_digits] in *. @@ -677,18 +677,18 @@ Proof. Qed. Definition unpack_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params25519_64 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-unpack_simpl_correct. - rewrite <-(@app_n2_correct fe). + rewrite <-(@app_n2_correct fe25519_64). cbv. reflexivity. Defined. -Definition unpack (f : wire_digits) : fe := +Definition unpack (f : wire_digits) : fe25519_64 := Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f). Definition unpack_correct (f : wire_digits) - : unpack f = unpack_opt params wire_widths_nonneg bits_eq f + : unpack f = unpack_opt params25519_64 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). diff --git a/src/SpecificGen/GF41417_32.v b/src/SpecificGen/GF41417_32.v index 7e7f5ace8..345f4b7b0 100644 --- a/src/SpecificGen/GF41417_32.v +++ b/src/SpecificGen/GF41417_32.v @@ -25,15 +25,15 @@ Lemma prime_modulus : prime modulus. Admitted. Definition freeze_input_bound := 32%Z. Definition int_width := 32%Z. -Instance params : PseudoMersenneBaseParams modulus. +Instance params41417_32 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 18%nat 414. Defined. -Definition length_fe := Eval compute in length limb_widths. -Definition fe := Eval compute in (tuple Z length_fe). +Definition length_fe41417_32 := Eval compute in length limb_widths. +Definition fe41417_32 := Eval compute in (tuple Z length_fe41417_32). -Definition mul2modulus : fe := - Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params)). +Definition mul2modulus : fe41417_32 := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params41417_32)). Instance subCoeff : SubtractionCoefficient. apply Build_SubtractionCoefficient with (coeff := mul2modulus). @@ -150,24 +150,24 @@ Proof. reflexivity. Qed. -Definition app_n {T} (f : fe) (P : fe -> T) : T. +Definition app_n {T} (f : fe41417_32) (P : fe41417_32 -> T) : T. Proof. - cbv [fe] in *. + cbv [fe41417_32] in *. set (f0 := f). repeat (let g := fresh "g" in destruct f as [f g]). apply P. apply f0. Defined. -Definition app_n_correct {T} f (P : fe -> T) : app_n f P = P f. +Definition app_n_correct {T} f (P : fe41417_32 -> T) : app_n f P = P f. Proof. intros. - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. reflexivity. Qed. -Definition appify2 {T} (op : fe -> fe -> T) (f g : fe) := +Definition appify2 {T} (op : fe41417_32 -> fe41417_32 -> T) (f g : fe41417_32) := app_n f (fun f0 => (app_n g (fun g0 => op f0 g0))). Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g. @@ -176,102 +176,102 @@ Proof. etransitivity; apply app_n_correct. Qed. -Definition uncurry_unop_fe {T} (op : fe -> T) - := Eval compute in Tuple.uncurry (n:=length_fe) op. -Definition curry_unop_fe {T} op : fe -> T - := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe) op). -Definition uncurry_binop_fe {T} (op : fe -> fe -> T) - := Eval compute in uncurry_unop_fe (fun f => uncurry_unop_fe (op f)). -Definition curry_binop_fe {T} op : fe -> fe -> T - := Eval compute in appify2 (fun f => curry_unop_fe (curry_unop_fe op f)). +Definition uncurry_unop_fe41417_32 {T} (op : fe41417_32 -> T) + := Eval compute in Tuple.uncurry (n:=length_fe41417_32) op. +Definition curry_unop_fe41417_32 {T} op : fe41417_32 -> T + := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe41417_32) op). +Definition uncurry_binop_fe41417_32 {T} (op : fe41417_32 -> fe41417_32 -> T) + := Eval compute in uncurry_unop_fe41417_32 (fun f => uncurry_unop_fe41417_32 (op f)). +Definition curry_binop_fe41417_32 {T} op : fe41417_32 -> fe41417_32 -> T + := Eval compute in appify2 (fun f => curry_unop_fe41417_32 (curry_unop_fe41417_32 op f)). Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) := Eval compute in Tuple.uncurry (n:=length wire_widths) op. Definition curry_unop_wire_digits {T} op : wire_digits -> T := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op). -Definition add_sig (f g : fe) : - { fg : fe | fg = add_opt f g}. +Definition add_sig (f g : fe41417_32) : + { fg : fe41417_32 | fg = add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe41417_32). cbv. reflexivity. Defined. -Definition add (f g : fe) : fe := +Definition add (f g : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig add_sig] in proj1_sig (add_sig f g). -Definition add_correct (f g : fe) +Definition add_correct (f g : fe41417_32) : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (add_sig f g). -Definition carry_add_sig (f g : fe) : - { fg : fe | fg = carry_add_opt f g}. +Definition carry_add_sig (f g : fe41417_32) : + { fg : fe41417_32 | fg = carry_add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe41417_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_add (f g : fe) : fe := +Definition carry_add (f g : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj1_sig (carry_add_sig f g). -Definition carry_add_correct (f g : fe) +Definition carry_add_correct (f g : fe41417_32) : carry_add f g = carry_add_opt f g := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj2_sig (carry_add_sig f g). -Definition sub_sig (f g : fe) : - { fg : fe | fg = sub_opt f g}. +Definition sub_sig (f g : fe41417_32) : + { fg : fe41417_32 | fg = sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe41417_32). cbv. reflexivity. Defined. -Definition sub (f g : fe) : fe := +Definition sub (f g : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig sub_sig] in proj1_sig (sub_sig f g). -Definition sub_correct (f g : fe) +Definition sub_correct (f g : fe41417_32) : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). -Definition carry_sub_sig (f g : fe) : - { fg : fe | fg = carry_sub_opt f g}. +Definition carry_sub_sig (f g : fe41417_32) : + { fg : fe41417_32 | fg = carry_sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe41417_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_sub (f g : fe) : fe := +Definition carry_sub (f g : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj1_sig (carry_sub_sig f g). -Definition carry_sub_correct (f g : fe) +Definition carry_sub_correct (f g : fe41417_32) : carry_sub f g = carry_sub_opt f g := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj2_sig (carry_sub_sig f g). (* For multiplication, we add another layer of definition so that we can rewrite under the [let] binders. *) -Definition mul_simpl_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_simpl_sig (f g : fe41417_32) : + { fg : fe41417_32 | fg = carry_mul_opt k_ c_ f g}. Proof. - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. @@ -282,45 +282,45 @@ Proof. reflexivity. Defined. -Definition mul_simpl (f g : fe) : fe := +Definition mul_simpl (f g : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17) := g in proj1_sig (mul_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17)). -Definition mul_simpl_correct (f g : fe) +Definition mul_simpl_correct (f g : fe41417_32) : mul_simpl f g = carry_mul_opt k_ c_ f g. Proof. pose proof (proj2_sig (mul_simpl_sig f g)). - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition mul_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_sig (f g : fe41417_32) : + { fg : fe41417_32 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe41417_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition mul (f g : fe) : fe := +Definition mul (f g : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). -Definition mul_correct (f g : fe) +Definition mul_correct (f g : fe41417_32) : mul f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (mul_sig f g). -Definition opp_sig (f : fe) : - { g : fe | g = opp_opt f }. +Definition opp_sig (f : fe41417_32) : + { g : fe41417_32 | g = opp_opt f }. Proof. eexists. cbv [opp_opt]. @@ -330,15 +330,15 @@ Proof. reflexivity. Defined. -Definition opp (f : fe) : fe +Definition opp (f : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). -Definition opp_correct (f : fe) +Definition opp_correct (f : fe41417_32) : opp f = opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). -Definition carry_opp_sig (f : fe) : - { g : fe | g = carry_opp_opt f }. +Definition carry_opp_sig (f : fe41417_32) : + { g : fe41417_32 | g = carry_opp_opt f }. Proof. eexists. cbv [carry_opp_opt]. @@ -348,16 +348,16 @@ Proof. reflexivity. Defined. -Definition carry_opp (f : fe) : fe +Definition carry_opp (f : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f). -Definition carry_opp_correct (f : fe) +Definition carry_opp_correct (f : fe41417_32) : carry_opp f = carry_opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f). -Definition pow (f : fe) chain := fold_chain_opt one_ mul chain [f]. +Definition pow (f : fe41417_32) chain := fold_chain_opt one_ mul chain [f]. -Lemma pow_correct (f : fe) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. +Lemma pow_correct (f : fe41417_32) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. Proof. cbv [pow pow_opt]; intros. rewrite !fold_chain_opt_correct. @@ -365,8 +365,8 @@ Proof. intros; subst; apply mul_correct. Qed. -Definition inv_sig (f : fe) : - { g : fe | g = inv_opt k_ c_ one_ f }. +Definition inv_sig (f : fe41417_32) : + { g : fe41417_32 | g = inv_opt k_ c_ one_ f }. Proof. eexists; cbv [inv_opt]. rewrite <-pow_correct. @@ -374,10 +374,10 @@ Proof. reflexivity. Defined. -Definition inv (f : fe) : fe +Definition inv (f : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). -Definition inv_correct (f : fe) +Definition inv_correct (f : fe41417_32) : inv f = inv_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f). @@ -388,12 +388,12 @@ Import Morphisms. Local Existing Instance prime_modulus. Lemma field_and_homomorphisms - : @field fe eq zero_ one_ opp add sub mul inv div + : @field fe41417_32 eq zero_ one_ opp add sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ add mul encode + fe41417_32 eq one_ add mul encode /\ @Ring.is_homomorphism - fe eq one_ add mul + fe41417_32 eq one_ add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -411,15 +411,15 @@ Proof. { intros; apply encode_rep. } Qed. -Definition field41417 : @field fe eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. +Definition field41417 : @field fe41417_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. Lemma carry_field_and_homomorphisms - : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div + : @field fe41417_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ carry_add mul encode + fe41417_32 eq one_ carry_add mul encode /\ @Ring.is_homomorphism - fe eq one_ carry_add mul + fe41417_32 eq one_ carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -437,29 +437,29 @@ Proof. { intros; apply encode_rep. } Qed. -Definition carry_field : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. +Definition carry_field : @field fe41417_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. Lemma homomorphism_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe41417_32 eq one add mul encode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_F_decode - : @Ring.is_homomorphism fe eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe41417_32 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one carry_add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe41417_32 eq one carry_add mul encode. Proof. apply carry_field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_decode - : @Ring.is_homomorphism fe eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe41417_32 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply carry_field_and_homomorphisms. Qed. -Definition ge_modulus_sig (f : fe) : +Definition ge_modulus_sig (f : fe41417_32) : { b : Z | b = ge_modulus_opt (to_list 18 f) }. Proof. - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [ge_modulus_opt]. rewrite !modulus_digits_subst. @@ -467,24 +467,24 @@ Proof. reflexivity. Defined. -Definition ge_modulus (f : fe) : Z := +Definition ge_modulus (f : fe41417_32) : Z := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) := f in proj1_sig (ge_modulus_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17)). -Definition ge_modulus_correct (f : fe) : +Definition ge_modulus_correct (f : fe41417_32) : ge_modulus f = ge_modulus_opt (to_list 18 f). Proof. pose proof (proj2_sig (ge_modulus_sig f)). - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition freeze_sig (f : fe) : - { f' : fe | f' = from_list_default 0 18 (freeze_opt (int_width := int_width) c_ (to_list 18 f)) }. +Definition freeze_sig (f : fe41417_32) : + { f' : fe41417_32 | f' = from_list_default 0 18 (freeze_opt (int_width := int_width) c_ (to_list 18 f)) }. Proof. - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [freeze_opt int_width]. cbv [to_list to_list']. @@ -499,38 +499,38 @@ Proof. reflexivity. Defined. -Definition freeze (f : fe) : fe := +Definition freeze (f : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig freeze_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) := f in proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17)). -Definition freeze_correct (f : fe) +Definition freeze_correct (f : fe41417_32) : freeze f = from_list_default 0 18 (freeze_opt (int_width := int_width) c_ (to_list 18 f)). Proof. pose proof (proj2_sig (freeze_sig f)). - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition fieldwiseb_sig (f g : fe) : +Definition fieldwiseb_sig (f g : fe41417_32) : { b | b = @fieldwiseb Z Z 18 Z.eqb f g }. Proof. - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. reflexivity. Defined. -Definition fieldwiseb (f g : fe) : bool +Definition fieldwiseb (f g : fe41417_32) : bool := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17) := g in proj1_sig (fieldwiseb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17)). -Lemma fieldwiseb_correct (f g : fe) +Lemma fieldwiseb_correct (f g : fe41417_32) : fieldwiseb f g = @Tuple.fieldwiseb Z Z 18 Z.eqb f g. Proof. set (f' := f); set (g' := g). @@ -538,11 +538,11 @@ Proof. exact (proj2_sig (fieldwiseb_sig f' g')). Qed. -Definition eqb_sig (f g : fe) : +Definition eqb_sig (f g : fe41417_32) : { b | b = eqb int_width f g }. Proof. cbv [eqb]. - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [ModularBaseSystem.freeze int_width]. @@ -553,14 +553,14 @@ Proof. reflexivity. Defined. -Definition eqb (f g : fe) : bool +Definition eqb (f g : fe41417_32) : bool := Eval cbv beta iota delta [proj1_sig eqb_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17) := g in proj1_sig (eqb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17)). -Lemma eqb_correct (f g : fe) +Lemma eqb_correct (f g : fe41417_32) : eqb f g = ModularBaseSystem.eqb int_width f g. Proof. set (f' := f); set (g' := g). @@ -568,8 +568,8 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Definition sqrt_sig (f : fe) : - { f' : fe | f' = sqrt_3mod4_opt k_ c_ one_ f}. +Definition sqrt_sig (f : fe41417_32) : + { f' : fe41417_32 | f' = sqrt_3mod4_opt k_ c_ one_ f}. Proof. eexists. cbv [sqrt_3mod4_opt int_width]. @@ -577,17 +577,17 @@ Proof. reflexivity. Defined. -Definition sqrt (f : fe) : fe +Definition sqrt (f : fe41417_32) : fe41417_32 := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig f). -Definition sqrt_correct (f : fe) +Definition sqrt_correct (f : fe41417_32) : sqrt f = sqrt_3mod4_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig f). -Definition pack_simpl_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_simpl_sig (f : fe41417_32) : + { f' | f' = pack_opt params41417_32 wire_widths_nonneg bits_eq f }. Proof. - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [pack_opt]. @@ -598,22 +598,22 @@ Proof. reflexivity. Defined. -Definition pack_simpl (f : fe) := +Definition pack_simpl (f : fe41417_32) := Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) := f in proj1_sig (pack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17)). -Definition pack_simpl_correct (f : fe) - : pack_simpl f = pack_opt params wire_widths_nonneg bits_eq f. +Definition pack_simpl_correct (f : fe41417_32) + : pack_simpl f = pack_opt params41417_32 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (pack_simpl_sig f)). - cbv [fe] in *. + cbv [fe41417_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition pack_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_sig (f : fe41417_32) : + { f' | f' = pack_opt params41417_32 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-pack_simpl_correct. @@ -622,15 +622,15 @@ Proof. reflexivity. Defined. -Definition pack (f : fe) : wire_digits := +Definition pack (f : fe41417_32) : wire_digits := Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f). -Definition pack_correct (f : fe) - : pack f = pack_opt params wire_widths_nonneg bits_eq f +Definition pack_correct (f : fe41417_32) + : pack f = pack_opt params41417_32 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f). Definition unpack_simpl_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params41417_32 wire_widths_nonneg bits_eq f }. Proof. cbv [wire_digits] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -644,13 +644,13 @@ Proof. reflexivity. Defined. -Definition unpack_simpl (f : wire_digits) : fe := +Definition unpack_simpl (f : wire_digits) : fe41417_32 := Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12) := f in proj1_sig (unpack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12)). Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params wire_widths_nonneg bits_eq f. + : unpack_simpl f = unpack_opt params41417_32 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (unpack_simpl_sig f)). cbv [wire_digits] in *. @@ -659,18 +659,18 @@ Proof. Qed. Definition unpack_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params41417_32 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-unpack_simpl_correct. - rewrite <-(@app_n2_correct fe). + rewrite <-(@app_n2_correct fe41417_32). cbv. reflexivity. Defined. -Definition unpack (f : wire_digits) : fe := +Definition unpack (f : wire_digits) : fe41417_32 := Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f). Definition unpack_correct (f : wire_digits) - : unpack f = unpack_opt params wire_widths_nonneg bits_eq f + : unpack f = unpack_opt params41417_32 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v index f04fe80f2..c2272aa1a 100644 --- a/src/SpecificGen/GF5211_32.v +++ b/src/SpecificGen/GF5211_32.v @@ -25,15 +25,15 @@ Lemma prime_modulus : prime modulus. Admitted. Definition freeze_input_bound := 32%Z. Definition int_width := 32%Z. -Instance params : PseudoMersenneBaseParams modulus. +Instance params5211_32 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 20%nat 521. Defined. -Definition length_fe := Eval compute in length limb_widths. -Definition fe := Eval compute in (tuple Z length_fe). +Definition length_fe5211_32 := Eval compute in length limb_widths. +Definition fe5211_32 := Eval compute in (tuple Z length_fe5211_32). -Definition mul2modulus : fe := - Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params)). +Definition mul2modulus : fe5211_32 := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params5211_32)). Instance subCoeff : SubtractionCoefficient. apply Build_SubtractionCoefficient with (coeff := mul2modulus). @@ -150,24 +150,24 @@ Proof. reflexivity. Qed. -Definition app_n {T} (f : fe) (P : fe -> T) : T. +Definition app_n {T} (f : fe5211_32) (P : fe5211_32 -> T) : T. Proof. - cbv [fe] in *. + cbv [fe5211_32] in *. set (f0 := f). repeat (let g := fresh "g" in destruct f as [f g]). apply P. apply f0. Defined. -Definition app_n_correct {T} f (P : fe -> T) : app_n f P = P f. +Definition app_n_correct {T} f (P : fe5211_32 -> T) : app_n f P = P f. Proof. intros. - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. reflexivity. Qed. -Definition appify2 {T} (op : fe -> fe -> T) (f g : fe) := +Definition appify2 {T} (op : fe5211_32 -> fe5211_32 -> T) (f g : fe5211_32) := app_n f (fun f0 => (app_n g (fun g0 => op f0 g0))). Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g. @@ -176,102 +176,102 @@ Proof. etransitivity; apply app_n_correct. Qed. -Definition uncurry_unop_fe {T} (op : fe -> T) - := Eval compute in Tuple.uncurry (n:=length_fe) op. -Definition curry_unop_fe {T} op : fe -> T - := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe) op). -Definition uncurry_binop_fe {T} (op : fe -> fe -> T) - := Eval compute in uncurry_unop_fe (fun f => uncurry_unop_fe (op f)). -Definition curry_binop_fe {T} op : fe -> fe -> T - := Eval compute in appify2 (fun f => curry_unop_fe (curry_unop_fe op f)). +Definition uncurry_unop_fe5211_32 {T} (op : fe5211_32 -> T) + := Eval compute in Tuple.uncurry (n:=length_fe5211_32) op. +Definition curry_unop_fe5211_32 {T} op : fe5211_32 -> T + := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe5211_32) op). +Definition uncurry_binop_fe5211_32 {T} (op : fe5211_32 -> fe5211_32 -> T) + := Eval compute in uncurry_unop_fe5211_32 (fun f => uncurry_unop_fe5211_32 (op f)). +Definition curry_binop_fe5211_32 {T} op : fe5211_32 -> fe5211_32 -> T + := Eval compute in appify2 (fun f => curry_unop_fe5211_32 (curry_unop_fe5211_32 op f)). Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) := Eval compute in Tuple.uncurry (n:=length wire_widths) op. Definition curry_unop_wire_digits {T} op : wire_digits -> T := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op). -Definition add_sig (f g : fe) : - { fg : fe | fg = add_opt f g}. +Definition add_sig (f g : fe5211_32) : + { fg : fe5211_32 | fg = add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe5211_32). cbv. reflexivity. Defined. -Definition add (f g : fe) : fe := +Definition add (f g : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig add_sig] in proj1_sig (add_sig f g). -Definition add_correct (f g : fe) +Definition add_correct (f g : fe5211_32) : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (add_sig f g). -Definition carry_add_sig (f g : fe) : - { fg : fe | fg = carry_add_opt f g}. +Definition carry_add_sig (f g : fe5211_32) : + { fg : fe5211_32 | fg = carry_add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe5211_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_add (f g : fe) : fe := +Definition carry_add (f g : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj1_sig (carry_add_sig f g). -Definition carry_add_correct (f g : fe) +Definition carry_add_correct (f g : fe5211_32) : carry_add f g = carry_add_opt f g := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj2_sig (carry_add_sig f g). -Definition sub_sig (f g : fe) : - { fg : fe | fg = sub_opt f g}. +Definition sub_sig (f g : fe5211_32) : + { fg : fe5211_32 | fg = sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe5211_32). cbv. reflexivity. Defined. -Definition sub (f g : fe) : fe := +Definition sub (f g : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig sub_sig] in proj1_sig (sub_sig f g). -Definition sub_correct (f g : fe) +Definition sub_correct (f g : fe5211_32) : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). -Definition carry_sub_sig (f g : fe) : - { fg : fe | fg = carry_sub_opt f g}. +Definition carry_sub_sig (f g : fe5211_32) : + { fg : fe5211_32 | fg = carry_sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe5211_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_sub (f g : fe) : fe := +Definition carry_sub (f g : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj1_sig (carry_sub_sig f g). -Definition carry_sub_correct (f g : fe) +Definition carry_sub_correct (f g : fe5211_32) : carry_sub f g = carry_sub_opt f g := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj2_sig (carry_sub_sig f g). (* For multiplication, we add another layer of definition so that we can rewrite under the [let] binders. *) -Definition mul_simpl_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_simpl_sig (f g : fe5211_32) : + { fg : fe5211_32 | fg = carry_mul_opt k_ c_ f g}. Proof. - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. @@ -282,45 +282,45 @@ Proof. reflexivity. Defined. -Definition mul_simpl (f g : fe) : fe := +Definition mul_simpl (f g : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17, g18, g19) := g in proj1_sig (mul_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17, g18, g19)). -Definition mul_simpl_correct (f g : fe) +Definition mul_simpl_correct (f g : fe5211_32) : mul_simpl f g = carry_mul_opt k_ c_ f g. Proof. pose proof (proj2_sig (mul_simpl_sig f g)). - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition mul_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_sig (f g : fe5211_32) : + { fg : fe5211_32 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe5211_32). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition mul (f g : fe) : fe := +Definition mul (f g : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). -Definition mul_correct (f g : fe) +Definition mul_correct (f g : fe5211_32) : mul f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (mul_sig f g). -Definition opp_sig (f : fe) : - { g : fe | g = opp_opt f }. +Definition opp_sig (f : fe5211_32) : + { g : fe5211_32 | g = opp_opt f }. Proof. eexists. cbv [opp_opt]. @@ -330,15 +330,15 @@ Proof. reflexivity. Defined. -Definition opp (f : fe) : fe +Definition opp (f : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). -Definition opp_correct (f : fe) +Definition opp_correct (f : fe5211_32) : opp f = opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). -Definition carry_opp_sig (f : fe) : - { g : fe | g = carry_opp_opt f }. +Definition carry_opp_sig (f : fe5211_32) : + { g : fe5211_32 | g = carry_opp_opt f }. Proof. eexists. cbv [carry_opp_opt]. @@ -348,16 +348,16 @@ Proof. reflexivity. Defined. -Definition carry_opp (f : fe) : fe +Definition carry_opp (f : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f). -Definition carry_opp_correct (f : fe) +Definition carry_opp_correct (f : fe5211_32) : carry_opp f = carry_opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f). -Definition pow (f : fe) chain := fold_chain_opt one_ mul chain [f]. +Definition pow (f : fe5211_32) chain := fold_chain_opt one_ mul chain [f]. -Lemma pow_correct (f : fe) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. +Lemma pow_correct (f : fe5211_32) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. Proof. cbv [pow pow_opt]; intros. rewrite !fold_chain_opt_correct. @@ -365,8 +365,8 @@ Proof. intros; subst; apply mul_correct. Qed. -Definition inv_sig (f : fe) : - { g : fe | g = inv_opt k_ c_ one_ f }. +Definition inv_sig (f : fe5211_32) : + { g : fe5211_32 | g = inv_opt k_ c_ one_ f }. Proof. eexists; cbv [inv_opt]. rewrite <-pow_correct. @@ -374,10 +374,10 @@ Proof. reflexivity. Defined. -Definition inv (f : fe) : fe +Definition inv (f : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). -Definition inv_correct (f : fe) +Definition inv_correct (f : fe5211_32) : inv f = inv_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f). @@ -388,12 +388,12 @@ Import Morphisms. Local Existing Instance prime_modulus. Lemma field_and_homomorphisms - : @field fe eq zero_ one_ opp add sub mul inv div + : @field fe5211_32 eq zero_ one_ opp add sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ add mul encode + fe5211_32 eq one_ add mul encode /\ @Ring.is_homomorphism - fe eq one_ add mul + fe5211_32 eq one_ add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -411,15 +411,15 @@ Proof. { intros; apply encode_rep. } Qed. -Definition field5211 : @field fe eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. +Definition field5211 : @field fe5211_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. Lemma carry_field_and_homomorphisms - : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div + : @field fe5211_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ carry_add mul encode + fe5211_32 eq one_ carry_add mul encode /\ @Ring.is_homomorphism - fe eq one_ carry_add mul + fe5211_32 eq one_ carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -437,29 +437,29 @@ Proof. { intros; apply encode_rep. } Qed. -Definition carry_field : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. +Definition carry_field : @field fe5211_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. Lemma homomorphism_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe5211_32 eq one add mul encode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_F_decode - : @Ring.is_homomorphism fe eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe5211_32 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one carry_add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe5211_32 eq one carry_add mul encode. Proof. apply carry_field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_decode - : @Ring.is_homomorphism fe eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe5211_32 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply carry_field_and_homomorphisms. Qed. -Definition ge_modulus_sig (f : fe) : +Definition ge_modulus_sig (f : fe5211_32) : { b : Z | b = ge_modulus_opt (to_list 20 f) }. Proof. - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [ge_modulus_opt]. rewrite !modulus_digits_subst. @@ -467,24 +467,24 @@ Proof. reflexivity. Defined. -Definition ge_modulus (f : fe) : Z := +Definition ge_modulus (f : fe5211_32) : Z := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) := f in proj1_sig (ge_modulus_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19)). -Definition ge_modulus_correct (f : fe) : +Definition ge_modulus_correct (f : fe5211_32) : ge_modulus f = ge_modulus_opt (to_list 20 f). Proof. pose proof (proj2_sig (ge_modulus_sig f)). - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition freeze_sig (f : fe) : - { f' : fe | f' = from_list_default 0 20 (freeze_opt (int_width := int_width) c_ (to_list 20 f)) }. +Definition freeze_sig (f : fe5211_32) : + { f' : fe5211_32 | f' = from_list_default 0 20 (freeze_opt (int_width := int_width) c_ (to_list 20 f)) }. Proof. - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [freeze_opt int_width]. cbv [to_list to_list']. @@ -499,38 +499,38 @@ Proof. reflexivity. Defined. -Definition freeze (f : fe) : fe := +Definition freeze (f : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig freeze_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) := f in proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19)). -Definition freeze_correct (f : fe) +Definition freeze_correct (f : fe5211_32) : freeze f = from_list_default 0 20 (freeze_opt (int_width := int_width) c_ (to_list 20 f)). Proof. pose proof (proj2_sig (freeze_sig f)). - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition fieldwiseb_sig (f g : fe) : +Definition fieldwiseb_sig (f g : fe5211_32) : { b | b = @fieldwiseb Z Z 20 Z.eqb f g }. Proof. - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. reflexivity. Defined. -Definition fieldwiseb (f g : fe) : bool +Definition fieldwiseb (f g : fe5211_32) : bool := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17, g18, g19) := g in proj1_sig (fieldwiseb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17, g18, g19)). -Lemma fieldwiseb_correct (f g : fe) +Lemma fieldwiseb_correct (f g : fe5211_32) : fieldwiseb f g = @Tuple.fieldwiseb Z Z 20 Z.eqb f g. Proof. set (f' := f); set (g' := g). @@ -538,11 +538,11 @@ Proof. exact (proj2_sig (fieldwiseb_sig f' g')). Qed. -Definition eqb_sig (f g : fe) : +Definition eqb_sig (f g : fe5211_32) : { b | b = eqb int_width f g }. Proof. cbv [eqb]. - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [ModularBaseSystem.freeze int_width]. @@ -553,14 +553,14 @@ Proof. reflexivity. Defined. -Definition eqb (f g : fe) : bool +Definition eqb (f g : fe5211_32) : bool := Eval cbv beta iota delta [proj1_sig eqb_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) := f in let '(g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17, g18, g19) := g in proj1_sig (eqb_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) (g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, g17, g18, g19)). -Lemma eqb_correct (f g : fe) +Lemma eqb_correct (f g : fe5211_32) : eqb f g = ModularBaseSystem.eqb int_width f g. Proof. set (f' := f); set (g' := g). @@ -568,8 +568,8 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Definition sqrt_sig (f : fe) : - { f' : fe | f' = sqrt_3mod4_opt k_ c_ one_ f}. +Definition sqrt_sig (f : fe5211_32) : + { f' : fe5211_32 | f' = sqrt_3mod4_opt k_ c_ one_ f}. Proof. eexists. cbv [sqrt_3mod4_opt int_width]. @@ -577,17 +577,17 @@ Proof. reflexivity. Defined. -Definition sqrt (f : fe) : fe +Definition sqrt (f : fe5211_32) : fe5211_32 := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig f). -Definition sqrt_correct (f : fe) +Definition sqrt_correct (f : fe5211_32) : sqrt f = sqrt_3mod4_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig f). -Definition pack_simpl_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_simpl_sig (f : fe5211_32) : + { f' | f' = pack_opt params5211_32 wire_widths_nonneg bits_eq f }. Proof. - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [pack_opt]. @@ -598,22 +598,22 @@ Proof. reflexivity. Defined. -Definition pack_simpl (f : fe) := +Definition pack_simpl (f : fe5211_32) := Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) := f in proj1_sig (pack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19)). -Definition pack_simpl_correct (f : fe) - : pack_simpl f = pack_opt params wire_widths_nonneg bits_eq f. +Definition pack_simpl_correct (f : fe5211_32) + : pack_simpl f = pack_opt params5211_32 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (pack_simpl_sig f)). - cbv [fe] in *. + cbv [fe5211_32] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition pack_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_sig (f : fe5211_32) : + { f' | f' = pack_opt params5211_32 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-pack_simpl_correct. @@ -622,15 +622,15 @@ Proof. reflexivity. Defined. -Definition pack (f : fe) : wire_digits := +Definition pack (f : fe5211_32) : wire_digits := Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f). -Definition pack_correct (f : fe) - : pack f = pack_opt params wire_widths_nonneg bits_eq f +Definition pack_correct (f : fe5211_32) + : pack f = pack_opt params5211_32 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f). Definition unpack_simpl_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params5211_32 wire_widths_nonneg bits_eq f }. Proof. cbv [wire_digits] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -644,13 +644,13 @@ Proof. reflexivity. Defined. -Definition unpack_simpl (f : wire_digits) : fe := +Definition unpack_simpl (f : wire_digits) : fe5211_32 := Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16) := f in proj1_sig (unpack_simpl_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16)). Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params wire_widths_nonneg bits_eq f. + : unpack_simpl f = unpack_opt params5211_32 wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (unpack_simpl_sig f)). cbv [wire_digits] in *. @@ -659,18 +659,18 @@ Proof. Qed. Definition unpack_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params5211_32 wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-unpack_simpl_correct. - rewrite <-(@app_n2_correct fe). + rewrite <-(@app_n2_correct fe5211_32). cbv. reflexivity. Defined. -Definition unpack (f : wire_digits) : fe := +Definition unpack (f : wire_digits) : fe5211_32 := Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f). Definition unpack_correct (f : wire_digits) - : unpack f = unpack_opt params wire_widths_nonneg bits_eq f + : unpack f = unpack_opt params5211_32 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4 index 6c25c91ca..0ad1a423a 100644 --- a/src/SpecificGen/GFtemplate3mod4 +++ b/src/SpecificGen/GFtemplate3mod4 @@ -25,15 +25,15 @@ Lemma prime_modulus : prime modulus. Admitted. Definition freeze_input_bound := {{{w}}}%Z. Definition int_width := {{{w}}}%Z. -Instance params : PseudoMersenneBaseParams modulus. +Instance params{{{k}}}{{{c}}}_{{{w}}} : PseudoMersenneBaseParams modulus. construct_params prime_modulus {{{n}}}%nat {{{k}}}. Defined. -Definition length_fe := Eval compute in length limb_widths. -Definition fe := Eval compute in (tuple Z length_fe). +Definition length_fe{{{k}}}{{{c}}}_{{{w}}} := Eval compute in length limb_widths. +Definition fe{{{k}}}{{{c}}}_{{{w}}} := Eval compute in (tuple Z length_fe{{{k}}}{{{c}}}_{{{w}}}). -Definition mul2modulus : fe := - Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params)). +Definition mul2modulus : fe{{{k}}}{{{c}}}_{{{w}}} := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params{{{k}}}{{{c}}}_{{{w}}})). Instance subCoeff : SubtractionCoefficient. apply Build_SubtractionCoefficient with (coeff := mul2modulus). @@ -150,24 +150,24 @@ Proof. reflexivity. Qed. -Definition app_n {T} (f : fe) (P : fe -> T) : T. +Definition app_n {T} (f : fe{{{k}}}{{{c}}}_{{{w}}}) (P : fe{{{k}}}{{{c}}}_{{{w}}} -> T) : T. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. set (f0 := f). repeat (let g := fresh "g" in destruct f as [f g]). apply P. apply f0. Defined. -Definition app_n_correct {T} f (P : fe -> T) : app_n f P = P f. +Definition app_n_correct {T} f (P : fe{{{k}}}{{{c}}}_{{{w}}} -> T) : app_n f P = P f. Proof. intros. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. reflexivity. Qed. -Definition appify2 {T} (op : fe -> fe -> T) (f g : fe) := +Definition appify2 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (f g : fe{{{k}}}{{{c}}}_{{{w}}}) := app_n f (fun f0 => (app_n g (fun g0 => op f0 g0))). Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g. @@ -176,102 +176,102 @@ Proof. etransitivity; apply app_n_correct. Qed. -Definition uncurry_unop_fe {T} (op : fe -> T) - := Eval compute in Tuple.uncurry (n:=length_fe) op. -Definition curry_unop_fe {T} op : fe -> T - := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe) op). -Definition uncurry_binop_fe {T} (op : fe -> fe -> T) - := Eval compute in uncurry_unop_fe (fun f => uncurry_unop_fe (op f)). -Definition curry_binop_fe {T} op : fe -> fe -> T - := Eval compute in appify2 (fun f => curry_unop_fe (curry_unop_fe op f)). +Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T) + := Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op. +Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T + := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op). +Definition uncurry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) + := Eval compute in uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun f => uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (op f)). +Definition curry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T + := Eval compute in appify2 (fun f => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op f)). Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) := Eval compute in Tuple.uncurry (n:=length wire_widths) op. Definition curry_unop_wire_digits {T} op : wire_digits -> T := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op). -Definition add_sig (f g : fe) : - { fg : fe | fg = add_opt f g}. +Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. reflexivity. Defined. -Definition add (f g : fe) : fe := +Definition add (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig add_sig] in proj1_sig (add_sig f g). -Definition add_correct (f g : fe) +Definition add_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (add_sig f g). -Definition carry_add_sig (f g : fe) : - { fg : fe | fg = carry_add_opt f g}. +Definition carry_add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_add (f g : fe) : fe := +Definition carry_add (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj1_sig (carry_add_sig f g). -Definition carry_add_correct (f g : fe) +Definition carry_add_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : carry_add f g = carry_add_opt f g := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj2_sig (carry_add_sig f g). -Definition sub_sig (f g : fe) : - { fg : fe | fg = sub_opt f g}. +Definition sub_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. reflexivity. Defined. -Definition sub (f g : fe) : fe := +Definition sub (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig sub_sig] in proj1_sig (sub_sig f g). -Definition sub_correct (f g : fe) +Definition sub_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). -Definition carry_sub_sig (f g : fe) : - { fg : fe | fg = carry_sub_opt f g}. +Definition carry_sub_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_sub (f g : fe) : fe := +Definition carry_sub (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj1_sig (carry_sub_sig f g). -Definition carry_sub_correct (f g : fe) +Definition carry_sub_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : carry_sub f g = carry_sub_opt f g := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj2_sig (carry_sub_sig f g). (* For multiplication, we add another layer of definition so that we can rewrite under the [let] binders. *) -Definition mul_simpl_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_simpl_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_mul_opt k_ c_ f g}. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. @@ -282,45 +282,45 @@ Proof. reflexivity. Defined. -Definition mul_simpl (f g : fe) : fe := +Definition mul_simpl (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in let '{{{enum f}}} := f in let '{{{enum g}}} := g in proj1_sig (mul_simpl_sig {{{enum f}}} {{{enum g}}}). -Definition mul_simpl_correct (f g : fe) +Definition mul_simpl_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : mul_simpl f g = carry_mul_opt k_ c_ f g. Proof. pose proof (proj2_sig (mul_simpl_sig f g)). - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition mul_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition mul (f g : fe) : fe := +Definition mul (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). -Definition mul_correct (f g : fe) +Definition mul_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : mul f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (mul_sig f g). -Definition opp_sig (f : fe) : - { g : fe | g = opp_opt f }. +Definition opp_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = opp_opt f }. Proof. eexists. cbv [opp_opt]. @@ -330,15 +330,15 @@ Proof. reflexivity. Defined. -Definition opp (f : fe) : fe +Definition opp (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). -Definition opp_correct (f : fe) +Definition opp_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : opp f = opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). -Definition carry_opp_sig (f : fe) : - { g : fe | g = carry_opp_opt f }. +Definition carry_opp_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = carry_opp_opt f }. Proof. eexists. cbv [carry_opp_opt]. @@ -348,16 +348,16 @@ Proof. reflexivity. Defined. -Definition carry_opp (f : fe) : fe +Definition carry_opp (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f). -Definition carry_opp_correct (f : fe) +Definition carry_opp_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : carry_opp f = carry_opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f). -Definition pow (f : fe) chain := fold_chain_opt one_ mul chain [f]. +Definition pow (f : fe{{{k}}}{{{c}}}_{{{w}}}) chain := fold_chain_opt one_ mul chain [f]. -Lemma pow_correct (f : fe) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. +Lemma pow_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. Proof. cbv [pow pow_opt]; intros. rewrite !fold_chain_opt_correct. @@ -365,8 +365,8 @@ Proof. intros; subst; apply mul_correct. Qed. -Definition inv_sig (f : fe) : - { g : fe | g = inv_opt k_ c_ one_ f }. +Definition inv_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = inv_opt k_ c_ one_ f }. Proof. eexists; cbv [inv_opt]. rewrite <-pow_correct. @@ -374,10 +374,10 @@ Proof. reflexivity. Defined. -Definition inv (f : fe) : fe +Definition inv (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). -Definition inv_correct (f : fe) +Definition inv_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : inv f = inv_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f). @@ -388,12 +388,12 @@ Import Morphisms. Local Existing Instance prime_modulus. Lemma field_and_homomorphisms - : @field fe eq zero_ one_ opp add sub mul inv div + : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ add mul encode + fe{{{k}}}{{{c}}}_{{{w}}} eq one_ add mul encode /\ @Ring.is_homomorphism - fe eq one_ add mul + fe{{{k}}}{{{c}}}_{{{w}}} eq one_ add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -411,15 +411,15 @@ Proof. { intros; apply encode_rep. } Qed. -Definition field{{{k}}}{{{c}}} : @field fe eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. +Definition field{{{k}}}{{{c}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. Lemma carry_field_and_homomorphisms - : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div + : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ carry_add mul encode + fe{{{k}}}{{{c}}}_{{{w}}} eq one_ carry_add mul encode /\ @Ring.is_homomorphism - fe eq one_ carry_add mul + fe{{{k}}}{{{c}}}_{{{w}}} eq one_ carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -437,29 +437,29 @@ Proof. { intros; apply encode_rep. } Qed. -Definition carry_field : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. +Definition carry_field : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. Lemma homomorphism_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul encode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_F_decode - : @Ring.is_homomorphism fe eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one carry_add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul encode. Proof. apply carry_field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_decode - : @Ring.is_homomorphism fe eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply carry_field_and_homomorphisms. Qed. -Definition ge_modulus_sig (f : fe) : +Definition ge_modulus_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : { b : Z | b = ge_modulus_opt (to_list {{{n}}} f) }. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [ge_modulus_opt]. rewrite !modulus_digits_subst. @@ -467,24 +467,24 @@ Proof. reflexivity. Defined. -Definition ge_modulus (f : fe) : Z := +Definition ge_modulus (f : fe{{{k}}}{{{c}}}_{{{w}}}) : Z := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in let '{{{enum f}}} := f in proj1_sig (ge_modulus_sig {{{enum f}}}). -Definition ge_modulus_correct (f : fe) : +Definition ge_modulus_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : ge_modulus f = ge_modulus_opt (to_list {{{n}}} f). Proof. pose proof (proj2_sig (ge_modulus_sig f)). - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition freeze_sig (f : fe) : - { f' : fe | f' = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)) }. +Definition freeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)) }. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [freeze_opt int_width]. cbv [to_list to_list']. @@ -499,38 +499,38 @@ Proof. reflexivity. Defined. -Definition freeze (f : fe) : fe := +Definition freeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig freeze_sig] in let '{{{enum f}}} := f in proj1_sig (freeze_sig {{{enum f}}}). -Definition freeze_correct (f : fe) +Definition freeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : freeze f = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)). Proof. pose proof (proj2_sig (freeze_sig f)). - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition fieldwiseb_sig (f g : fe) : +Definition fieldwiseb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : { b | b = @fieldwiseb Z Z {{{n}}} Z.eqb f g }. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. reflexivity. Defined. -Definition fieldwiseb (f g : fe) : bool +Definition fieldwiseb (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : bool := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in let '{{{enum f}}} := f in let '{{{enum g}}} := g in proj1_sig (fieldwiseb_sig {{{enum f}}} {{{enum g}}}). -Lemma fieldwiseb_correct (f g : fe) +Lemma fieldwiseb_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fieldwiseb f g = @Tuple.fieldwiseb Z Z {{{n}}} Z.eqb f g. Proof. set (f' := f); set (g' := g). @@ -538,11 +538,11 @@ Proof. exact (proj2_sig (fieldwiseb_sig f' g')). Qed. -Definition eqb_sig (f g : fe) : +Definition eqb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : { b | b = eqb int_width f g }. Proof. cbv [eqb]. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [ModularBaseSystem.freeze int_width]. @@ -553,14 +553,14 @@ Proof. reflexivity. Defined. -Definition eqb (f g : fe) : bool +Definition eqb (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : bool := Eval cbv beta iota delta [proj1_sig eqb_sig] in let '{{{enum f}}} := f in let '{{{enum g}}} := g in proj1_sig (eqb_sig {{{enum f}}} {{{enum g}}}). -Lemma eqb_correct (f g : fe) +Lemma eqb_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : eqb f g = ModularBaseSystem.eqb int_width f g. Proof. set (f' := f); set (g' := g). @@ -568,8 +568,8 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Definition sqrt_sig (f : fe) : - { f' : fe | f' = sqrt_3mod4_opt k_ c_ one_ f}. +Definition sqrt_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = sqrt_3mod4_opt k_ c_ one_ f}. Proof. eexists. cbv [sqrt_3mod4_opt int_width]. @@ -577,17 +577,17 @@ Proof. reflexivity. Defined. -Definition sqrt (f : fe) : fe +Definition sqrt (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig f). -Definition sqrt_correct (f : fe) +Definition sqrt_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : sqrt f = sqrt_3mod4_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig f). -Definition pack_simpl_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_simpl_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { f' | f' = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [pack_opt]. @@ -598,22 +598,22 @@ Proof. reflexivity. Defined. -Definition pack_simpl (f : fe) := +Definition pack_simpl (f : fe{{{k}}}{{{c}}}_{{{w}}}) := Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in let '{{{enum f}}} := f in proj1_sig (pack_simpl_sig {{{enum f}}}). -Definition pack_simpl_correct (f : fe) - : pack_simpl f = pack_opt params wire_widths_nonneg bits_eq f. +Definition pack_simpl_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) + : pack_simpl f = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (pack_simpl_sig f)). - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition pack_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { f' | f' = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-pack_simpl_correct. @@ -622,15 +622,15 @@ Proof. reflexivity. Defined. -Definition pack (f : fe) : wire_digits := +Definition pack (f : fe{{{k}}}{{{c}}}_{{{w}}}) : wire_digits := Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f). -Definition pack_correct (f : fe) - : pack f = pack_opt params wire_widths_nonneg bits_eq f +Definition pack_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) + : pack f = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f). Definition unpack_simpl_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. Proof. cbv [wire_digits] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -644,13 +644,13 @@ Proof. reflexivity. Defined. -Definition unpack_simpl (f : wire_digits) : fe := +Definition unpack_simpl (f : wire_digits) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in let '{{{enumw f}}} := f in proj1_sig (unpack_simpl_sig {{{enumw f}}}). Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params wire_widths_nonneg bits_eq f. + : unpack_simpl f = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (unpack_simpl_sig f)). cbv [wire_digits] in *. @@ -659,18 +659,18 @@ Proof. Qed. Definition unpack_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-unpack_simpl_correct. - rewrite <-(@app_n2_correct fe). + rewrite <-(@app_n2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. reflexivity. Defined. -Definition unpack (f : wire_digits) : fe := +Definition unpack (f : wire_digits) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f). Definition unpack_correct (f : wire_digits) - : unpack f = unpack_opt params wire_widths_nonneg bits_eq f + : unpack f = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). diff --git a/src/SpecificGen/GFtemplate5mod8 b/src/SpecificGen/GFtemplate5mod8 index 4b8d4a9e4..92e25cd18 100644 --- a/src/SpecificGen/GFtemplate5mod8 +++ b/src/SpecificGen/GFtemplate5mod8 @@ -25,15 +25,15 @@ Lemma prime_modulus : prime modulus. Admitted. Definition freeze_input_bound := {{{w}}}%Z. Definition int_width := {{{w}}}%Z. -Instance params : PseudoMersenneBaseParams modulus. +Instance params{{{k}}}{{{c}}}_{{{w}}} : PseudoMersenneBaseParams modulus. construct_params prime_modulus {{{n}}}%nat {{{k}}}. Defined. -Definition length_fe := Eval compute in length limb_widths. -Definition fe := Eval compute in (tuple Z length_fe). +Definition length_fe{{{k}}}{{{c}}}_{{{w}}} := Eval compute in length limb_widths. +Definition fe{{{k}}}{{{c}}}_{{{w}}} := Eval compute in (tuple Z length_fe{{{k}}}{{{c}}}_{{{w}}}). -Definition mul2modulus : fe := - Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params)). +Definition mul2modulus : fe{{{k}}}{{{c}}}_{{{w}}} := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params{{{k}}}{{{c}}}_{{{w}}})). Instance subCoeff : SubtractionCoefficient. apply Build_SubtractionCoefficient with (coeff := mul2modulus). @@ -150,24 +150,24 @@ Proof. reflexivity. Qed. -Definition app_n {T} (f : fe) (P : fe -> T) : T. +Definition app_n {T} (f : fe{{{k}}}{{{c}}}_{{{w}}}) (P : fe{{{k}}}{{{c}}}_{{{w}}} -> T) : T. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. set (f0 := f). repeat (let g := fresh "g" in destruct f as [f g]). apply P. apply f0. Defined. -Definition app_n_correct {T} f (P : fe -> T) : app_n f P = P f. +Definition app_n_correct {T} f (P : fe{{{k}}}{{{c}}}_{{{w}}} -> T) : app_n f P = P f. Proof. intros. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. reflexivity. Qed. -Definition appify2 {T} (op : fe -> fe -> T) (f g : fe) := +Definition appify2 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (f g : fe{{{k}}}{{{c}}}_{{{w}}}) := app_n f (fun f0 => (app_n g (fun g0 => op f0 g0))). Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g. @@ -176,102 +176,102 @@ Proof. etransitivity; apply app_n_correct. Qed. -Definition uncurry_unop_fe {T} (op : fe -> T) - := Eval compute in Tuple.uncurry (n:=length_fe) op. -Definition curry_unop_fe {T} op : fe -> T - := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe) op). -Definition uncurry_binop_fe {T} (op : fe -> fe -> T) - := Eval compute in uncurry_unop_fe (fun f => uncurry_unop_fe (op f)). -Definition curry_binop_fe {T} op : fe -> fe -> T - := Eval compute in appify2 (fun f => curry_unop_fe (curry_unop_fe op f)). +Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T) + := Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op. +Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T + := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op). +Definition uncurry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) + := Eval compute in uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun f => uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (op f)). +Definition curry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T + := Eval compute in appify2 (fun f => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op f)). Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T) := Eval compute in Tuple.uncurry (n:=length wire_widths) op. Definition curry_unop_wire_digits {T} op : wire_digits -> T := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op). -Definition add_sig (f g : fe) : - { fg : fe | fg = add_opt f g}. +Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. reflexivity. Defined. -Definition add (f g : fe) : fe := +Definition add (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig add_sig] in proj1_sig (add_sig f g). -Definition add_correct (f g : fe) +Definition add_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (add_sig f g). -Definition carry_add_sig (f g : fe) : - { fg : fe | fg = carry_add_opt f g}. +Definition carry_add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_add_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_add (f g : fe) : fe := +Definition carry_add (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj1_sig (carry_add_sig f g). -Definition carry_add_correct (f g : fe) +Definition carry_add_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : carry_add f g = carry_add_opt f g := Eval cbv beta iota delta [proj1_sig carry_add_sig] in proj2_sig (carry_add_sig f g). -Definition sub_sig (f g : fe) : - { fg : fe | fg = sub_opt f g}. +Definition sub_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. reflexivity. Defined. -Definition sub (f g : fe) : fe := +Definition sub (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig sub_sig] in proj1_sig (sub_sig f g). -Definition sub_correct (f g : fe) +Definition sub_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). -Definition carry_sub_sig (f g : fe) : - { fg : fe | fg = carry_sub_opt f g}. +Definition carry_sub_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_sub_opt f g}. Proof. eexists. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition carry_sub (f g : fe) : fe := +Definition carry_sub (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj1_sig (carry_sub_sig f g). -Definition carry_sub_correct (f g : fe) +Definition carry_sub_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : carry_sub f g = carry_sub_opt f g := Eval cbv beta iota delta [proj1_sig carry_sub_sig] in proj2_sig (carry_sub_sig f g). (* For multiplication, we add another layer of definition so that we can rewrite under the [let] binders. *) -Definition mul_simpl_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_simpl_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_mul_opt k_ c_ f g}. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. (* N.B. The slow part of this is computing with [Z_div_opt]. @@ -282,45 +282,45 @@ Proof. reflexivity. Defined. -Definition mul_simpl (f g : fe) : fe := +Definition mul_simpl (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in let '{{{enum f}}} := f in let '{{{enum g}}} := g in proj1_sig (mul_simpl_sig {{{enum f}}} {{{enum g}}}). -Definition mul_simpl_correct (f g : fe) +Definition mul_simpl_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : mul_simpl f g = carry_mul_opt k_ c_ f g. Proof. pose proof (proj2_sig (mul_simpl_sig f g)). - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition mul_sig (f g : fe) : - { fg : fe | fg = carry_mul_opt k_ c_ f g}. +Definition mul_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : + { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. - rewrite <-(@appify2_correct fe). + rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv. autorewrite with zsimplify_Z_to_pos; cbv. reflexivity. Defined. -Definition mul (f g : fe) : fe := +Definition mul (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). -Definition mul_correct (f g : fe) +Definition mul_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : mul f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (mul_sig f g). -Definition opp_sig (f : fe) : - { g : fe | g = opp_opt f }. +Definition opp_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = opp_opt f }. Proof. eexists. cbv [opp_opt]. @@ -330,15 +330,15 @@ Proof. reflexivity. Defined. -Definition opp (f : fe) : fe +Definition opp (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). -Definition opp_correct (f : fe) +Definition opp_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : opp f = opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). -Definition carry_opp_sig (f : fe) : - { g : fe | g = carry_opp_opt f }. +Definition carry_opp_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = carry_opp_opt f }. Proof. eexists. cbv [carry_opp_opt]. @@ -348,16 +348,16 @@ Proof. reflexivity. Defined. -Definition carry_opp (f : fe) : fe +Definition carry_opp (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f). -Definition carry_opp_correct (f : fe) +Definition carry_opp_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : carry_opp f = carry_opp_opt f := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f). -Definition pow (f : fe) chain := fold_chain_opt one_ mul chain [f]. +Definition pow (f : fe{{{k}}}{{{c}}}_{{{w}}}) chain := fold_chain_opt one_ mul chain [f]. -Lemma pow_correct (f : fe) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. +Lemma pow_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain. Proof. cbv [pow pow_opt]; intros. rewrite !fold_chain_opt_correct. @@ -382,8 +382,8 @@ Qed. Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb. -Definition inv_sig (f : fe) : - { g : fe | g = inv_opt k_ c_ one_ f }. +Definition inv_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = inv_opt k_ c_ one_ f }. Proof. eexists; cbv [inv_opt]. rewrite <-pow_correct. @@ -391,10 +391,10 @@ Proof. reflexivity. Defined. -Definition inv (f : fe) : fe +Definition inv (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). -Definition inv_correct (f : fe) +Definition inv_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : inv f = inv_opt k_ c_ one_ f := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f). @@ -405,12 +405,12 @@ Import Morphisms. Local Existing Instance prime_modulus. Lemma field_and_homomorphisms - : @field fe eq zero_ one_ opp add sub mul inv div + : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ add mul encode + fe{{{k}}}{{{c}}}_{{{w}}} eq one_ add mul encode /\ @Ring.is_homomorphism - fe eq one_ add mul + fe{{{k}}}{{{c}}}_{{{w}}} eq one_ add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -428,15 +428,15 @@ Proof. { intros; apply encode_rep. } Qed. -Definition field{{{k}}}{{{c}}} : @field fe eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. +Definition field{{{k}}}{{{c}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms. Lemma carry_field_and_homomorphisms - : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div + : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div /\ @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul - fe eq one_ carry_add mul encode + fe{{{k}}}{{{c}}}_{{{w}}} eq one_ carry_add mul encode /\ @Ring.is_homomorphism - fe eq one_ carry_add mul + fe{{{k}}}{{{c}}}_{{{w}}} eq one_ carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. @@ -454,29 +454,29 @@ Proof. { intros; apply encode_rep. } Qed. -Definition carry_field : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. +Definition carry_field : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms. Lemma homomorphism_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul encode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_F_decode - : @Ring.is_homomorphism fe eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_encode - : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one carry_add mul encode. + : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul encode. Proof. apply carry_field_and_homomorphisms. Qed. Lemma homomorphism_carry_F_decode - : @Ring.is_homomorphism fe eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. + : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode. Proof. apply carry_field_and_homomorphisms. Qed. -Definition ge_modulus_sig (f : fe) : +Definition ge_modulus_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : { b : Z | b = ge_modulus_opt (to_list {{{n}}} f) }. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [ge_modulus_opt]. rewrite !modulus_digits_subst. @@ -484,24 +484,24 @@ Proof. reflexivity. Defined. -Definition ge_modulus (f : fe) : Z := +Definition ge_modulus (f : fe{{{k}}}{{{c}}}_{{{w}}}) : Z := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in let '{{{enum f}}} := f in proj1_sig (ge_modulus_sig {{{enum f}}}). -Definition ge_modulus_correct (f : fe) : +Definition ge_modulus_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : ge_modulus f = ge_modulus_opt (to_list {{{n}}} f). Proof. pose proof (proj2_sig (ge_modulus_sig f)). - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition freeze_sig (f : fe) : - { f' : fe | f' = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)) }. +Definition freeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)) }. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists; cbv [freeze_opt int_width]. cbv [to_list to_list']. @@ -516,38 +516,38 @@ Proof. reflexivity. Defined. -Definition freeze (f : fe) : fe := +Definition freeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig freeze_sig] in let '{{{enum f}}} := f in proj1_sig (freeze_sig {{{enum f}}}). -Definition freeze_correct (f : fe) +Definition freeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : freeze f = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)). Proof. pose proof (proj2_sig (freeze_sig f)). - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -Definition fieldwiseb_sig (f g : fe) : +Definition fieldwiseb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : { b | b = @fieldwiseb Z Z {{{n}}} Z.eqb f g }. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. reflexivity. Defined. -Definition fieldwiseb (f g : fe) : bool +Definition fieldwiseb (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : bool := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in let '{{{enum f}}} := f in let '{{{enum g}}} := g in proj1_sig (fieldwiseb_sig {{{enum f}}} {{{enum g}}}). -Lemma fieldwiseb_correct (f g : fe) +Lemma fieldwiseb_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fieldwiseb f g = @Tuple.fieldwiseb Z Z {{{n}}} Z.eqb f g. Proof. set (f' := f); set (g' := g). @@ -555,11 +555,11 @@ Proof. exact (proj2_sig (fieldwiseb_sig f' g')). Qed. -Definition eqb_sig (f g : fe) : +Definition eqb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : { b | b = eqb int_width f g }. Proof. cbv [eqb]. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [ModularBaseSystem.freeze int_width]. @@ -570,14 +570,14 @@ Proof. reflexivity. Defined. -Definition eqb (f g : fe) : bool +Definition eqb (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : bool := Eval cbv beta iota delta [proj1_sig eqb_sig] in let '{{{enum f}}} := f in let '{{{enum g}}} := g in proj1_sig (eqb_sig {{{enum f}}} {{{enum g}}}). -Lemma eqb_correct (f g : fe) +Lemma eqb_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : eqb f g = ModularBaseSystem.eqb int_width f g. Proof. set (f' := f); set (g' := g). @@ -585,8 +585,8 @@ Proof. exact (proj2_sig (eqb_sig f' g')). Qed. -Definition sqrt_sig (powx powx_squared f : fe) : - { f' : fe | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powx powx_squared f}. +Definition sqrt_sig (powx powx_squared f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = sqrt_5mod8_opt (int_width := int_width) k_ c_ sqrt_m1 powx powx_squared f}. Proof. eexists. cbv [sqrt_5mod8_opt int_width]. @@ -595,17 +595,17 @@ Proof. reflexivity. Defined. -Definition sqrt (powx powx_squared f : fe) : fe +Definition sqrt (powx powx_squared f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig powx powx_squared f). -Definition sqrt_correct (powx powx_squared f : fe) +Definition sqrt_correct (powx powx_squared f : fe{{{k}}}{{{c}}}_{{{w}}}) : sqrt powx powx_squared f = sqrt_5mod8_opt k_ c_ sqrt_m1 powx powx_squared f := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig powx powx_squared f). -Definition pack_simpl_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_simpl_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { f' | f' = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. Proof. - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv [pack_opt]. @@ -616,22 +616,22 @@ Proof. reflexivity. Defined. -Definition pack_simpl (f : fe) := +Definition pack_simpl (f : fe{{{k}}}{{{c}}}_{{{w}}}) := Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in let '{{{enum f}}} := f in proj1_sig (pack_simpl_sig {{{enum f}}}). -Definition pack_simpl_correct (f : fe) - : pack_simpl f = pack_opt params wire_widths_nonneg bits_eq f. +Definition pack_simpl_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) + : pack_simpl f = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (pack_simpl_sig f)). - cbv [fe] in *. + cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Qed. -Definition pack_sig (f : fe) : - { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }. +Definition pack_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) : + { f' | f' = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-pack_simpl_correct. @@ -640,15 +640,15 @@ Proof. reflexivity. Defined. -Definition pack (f : fe) : wire_digits := +Definition pack (f : fe{{{k}}}{{{c}}}_{{{w}}}) : wire_digits := Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f). -Definition pack_correct (f : fe) - : pack f = pack_opt params wire_widths_nonneg bits_eq f +Definition pack_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) + : pack f = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f). Definition unpack_simpl_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. Proof. cbv [wire_digits] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -662,13 +662,13 @@ Proof. reflexivity. Defined. -Definition unpack_simpl (f : wire_digits) : fe := +Definition unpack_simpl (f : wire_digits) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in let '{{{enumw f}}} := f in proj1_sig (unpack_simpl_sig {{{enumw f}}}). Definition unpack_simpl_correct (f : wire_digits) - : unpack_simpl f = unpack_opt params wire_widths_nonneg bits_eq f. + : unpack_simpl f = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f. Proof. pose proof (proj2_sig (unpack_simpl_sig f)). cbv [wire_digits] in *. @@ -677,18 +677,18 @@ Proof. Qed. Definition unpack_sig (f : wire_digits) : - { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }. + { f' | f' = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }. Proof. eexists. rewrite <-unpack_simpl_correct. - rewrite <-(@app_n2_correct fe). + rewrite <-(@app_n2_correct fe{{{k}}}{{{c}}}_{{{w}}}). cbv. reflexivity. Defined. -Definition unpack (f : wire_digits) : fe := +Definition unpack (f : wire_digits) : fe{{{k}}}{{{c}}}_{{{w}}} := Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f). Definition unpack_correct (f : wire_digits) - : unpack f = unpack_opt params wire_widths_nonneg bits_eq f + : unpack f = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). |