diff options
Diffstat (limited to 'src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v')
| -rw-r--r-- | src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v | 458 |
1 files changed, 458 insertions, 0 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v new file mode 100644 index 000000000..4980f09b9 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v @@ -0,0 +1,458 @@ +(* This file is autogenerated from Montgomery.v by remake_packages.py *) +Require Import Crypto.Specific.Framework.CurveParametersPackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.FreezePackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.LadderstepPackage. +Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Montgomery. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. + +Module TAG. + Inductive tags := m' | r' | m'_correct | r'_correct | m_enc_correct_montgomery | r'_pow_correct | montgomery_to_F | r_big | m_big | m_enc_small | map_m_enc | mul_ext | add_ext | sub_ext | opp_ext | nonzero_ext | mul_bounded | add_bounded | sub_bounded | opp_bounded | nonzero_sig. +End TAG. + +Ltac add_m' pkg := + if_montgomery + pkg + ltac:(fun _ => let modinv_fuel := Tag.get pkg TAG.modinv_fuel in + let m := Tag.get pkg TAG.m in + let r := Tag.get pkg TAG.r in + let m' := fresh "m'" in + let m' := pose_m' modinv_fuel m r m' in + Tag.update pkg TAG.m' m') + ltac:(fun _ => pkg) + (). +Ltac add_r' pkg := + if_montgomery + pkg + ltac:(fun _ => let modinv_fuel := Tag.get pkg TAG.modinv_fuel in + let m := Tag.get pkg TAG.m in + let r := Tag.get pkg TAG.r in + let r' := fresh "r'" in + let r' := pose_r' modinv_fuel m r r' in + Tag.update pkg TAG.r' r') + ltac:(fun _ => pkg) + (). +Ltac add_m'_correct pkg := + if_montgomery + pkg + ltac:(fun _ => let m := Tag.get pkg TAG.m in + let m' := Tag.get pkg TAG.m' in + let r := Tag.get pkg TAG.r in + let m'_correct := fresh "m'_correct" in + let m'_correct := pose_m'_correct m m' r m'_correct in + Tag.update pkg TAG.m'_correct m'_correct) + ltac:(fun _ => pkg) + (). +Ltac add_r'_correct pkg := + if_montgomery + pkg + ltac:(fun _ => let m := Tag.get pkg TAG.m in + let r := Tag.get pkg TAG.r in + let r' := Tag.get pkg TAG.r' in + let r'_correct := fresh "r'_correct" in + let r'_correct := pose_r'_correct m r r' r'_correct in + Tag.update pkg TAG.r'_correct r'_correct) + ltac:(fun _ => pkg) + (). +Ltac add_m_enc_correct_montgomery pkg := + if_montgomery + pkg + ltac:(fun _ => let m := Tag.get pkg TAG.m in + let sz := Tag.get pkg TAG.sz in + let r := Tag.get pkg TAG.r in + let m_enc := Tag.get pkg TAG.m_enc in + let m_enc_correct_montgomery := fresh "m_enc_correct_montgomery" in + let m_enc_correct_montgomery := pose_m_enc_correct_montgomery m sz r m_enc m_enc_correct_montgomery in + Tag.update pkg TAG.m_enc_correct_montgomery m_enc_correct_montgomery) + ltac:(fun _ => pkg) + (). +Ltac add_r'_pow_correct pkg := + if_montgomery + pkg + ltac:(fun _ => let r' := Tag.get pkg TAG.r' in + let sz := Tag.get pkg TAG.sz in + let r := Tag.get pkg TAG.r in + let m_enc := Tag.get pkg TAG.m_enc in + let r'_pow_correct := fresh "r'_pow_correct" in + let r'_pow_correct := pose_r'_pow_correct r' sz r m_enc r'_pow_correct in + Tag.update pkg TAG.r'_pow_correct r'_pow_correct) + ltac:(fun _ => pkg) + (). +Ltac add_montgomery_to_F pkg := + if_montgomery + pkg + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let r' := Tag.get pkg TAG.r' in + let montgomery_to_F := fresh "montgomery_to_F" in + let montgomery_to_F := pose_montgomery_to_F sz m r' montgomery_to_F in + Tag.update pkg TAG.montgomery_to_F montgomery_to_F) + ltac:(fun _ => pkg) + (). +Ltac add_r_big pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let r_big := fresh "r_big" in + let r_big := pose_r_big r r_big in + Tag.update pkg TAG.r_big r_big) + ltac:(fun _ => pkg) + (). +Ltac add_m_big pkg := + if_montgomery + pkg + ltac:(fun _ => let m := Tag.get pkg TAG.m in + let m_big := fresh "m_big" in + let m_big := pose_m_big m m_big in + Tag.update pkg TAG.m_big m_big) + ltac:(fun _ => pkg) + (). +Ltac add_m_enc_small pkg := + if_montgomery + pkg + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let r := Tag.get pkg TAG.r in + let m_enc := Tag.get pkg TAG.m_enc in + let m_enc_small := fresh "m_enc_small" in + let m_enc_small := pose_m_enc_small sz r m_enc m_enc_small in + Tag.update pkg TAG.m_enc_small m_enc_small) + ltac:(fun _ => pkg) + (). +Ltac add_map_m_enc pkg := + if_montgomery + pkg + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let r := Tag.get pkg TAG.r in + let m_enc := Tag.get pkg TAG.m_enc in + let map_m_enc := fresh "map_m_enc" in + let map_m_enc := pose_map_m_enc sz r m_enc map_m_enc in + Tag.update pkg TAG.map_m_enc map_m_enc) + ltac:(fun _ => pkg) + (). +Ltac add_mul_ext pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let r' := Tag.get pkg TAG.r' in + let r'_correct := Tag.get pkg TAG.r'_correct in + let m' := Tag.get pkg TAG.m' in + let m'_correct := Tag.get pkg TAG.m'_correct in + let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in + let r_big := Tag.get pkg TAG.r_big in + let m_big := Tag.get pkg TAG.m_big in + let m_enc_small := Tag.get pkg TAG.m_enc_small in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let mul_ext := fresh "mul_ext" in + let mul_ext := pose_mul_ext r sz m m_enc r' r'_correct m' m'_correct m_enc_correct_montgomery r_big m_big m_enc_small montgomery_to_F mul_ext in + Tag.update pkg TAG.mul_ext mul_ext) + ltac:(fun _ => pkg) + (). +Ltac add_add_ext pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let r' := Tag.get pkg TAG.r' in + let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in + let r_big := Tag.get pkg TAG.r_big in + let m_big := Tag.get pkg TAG.m_big in + let m_enc_small := Tag.get pkg TAG.m_enc_small in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let add_ext := fresh "add_ext" in + let add_ext := pose_add_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_big m_enc_small montgomery_to_F add_ext in + Tag.update pkg TAG.add_ext add_ext) + ltac:(fun _ => pkg) + (). +Ltac add_sub_ext pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let r' := Tag.get pkg TAG.r' in + let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in + let r_big := Tag.get pkg TAG.r_big in + let m_enc_small := Tag.get pkg TAG.m_enc_small in + let map_m_enc := Tag.get pkg TAG.map_m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let sub_ext := fresh "sub_ext" in + let sub_ext := pose_sub_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc montgomery_to_F sub_ext in + Tag.update pkg TAG.sub_ext sub_ext) + ltac:(fun _ => pkg) + (). +Ltac add_opp_ext pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let r' := Tag.get pkg TAG.r' in + let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in + let r_big := Tag.get pkg TAG.r_big in + let m_enc_small := Tag.get pkg TAG.m_enc_small in + let map_m_enc := Tag.get pkg TAG.map_m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let opp_ext := fresh "opp_ext" in + let opp_ext := pose_opp_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc montgomery_to_F opp_ext in + Tag.update pkg TAG.opp_ext opp_ext) + ltac:(fun _ => pkg) + (). +Ltac add_nonzero_ext pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let r' := Tag.get pkg TAG.r' in + let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in + let r'_pow_correct := Tag.get pkg TAG.r'_pow_correct in + let r_big := Tag.get pkg TAG.r_big in + let m_big := Tag.get pkg TAG.m_big in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let nonzero_ext := fresh "nonzero_ext" in + let nonzero_ext := pose_nonzero_ext r sz m m_enc r' m_enc_correct_montgomery r'_pow_correct r_big m_big montgomery_to_F nonzero_ext in + Tag.update pkg TAG.nonzero_ext nonzero_ext) + ltac:(fun _ => pkg) + (). +Ltac add_mul_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let mul_ext := Tag.get pkg TAG.mul_ext in + let mul_sig := fresh "mul_sig" in + let mul_sig := pose_mul_sig r sz montgomery_to_F mul_ext mul_sig in + Tag.update pkg TAG.mul_sig mul_sig) + ltac:(fun _ => pkg) + (). +Ltac add_mul_bounded pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let mul_ext := Tag.get pkg TAG.mul_ext in + let mul_sig := Tag.get pkg TAG.mul_sig in + let mul_bounded := fresh "mul_bounded" in + let mul_bounded := pose_mul_bounded r sz m_enc montgomery_to_F mul_ext mul_sig mul_bounded in + Tag.update pkg TAG.mul_bounded mul_bounded) + ltac:(fun _ => pkg) + (). +Ltac add_add_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let add_ext := Tag.get pkg TAG.add_ext in + let add_sig := fresh "add_sig" in + let add_sig := pose_add_sig r sz m_enc montgomery_to_F add_ext add_sig in + Tag.update pkg TAG.add_sig add_sig) + ltac:(fun _ => pkg) + (). +Ltac add_add_bounded pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let add_ext := Tag.get pkg TAG.add_ext in + let add_sig := Tag.get pkg TAG.add_sig in + let add_bounded := fresh "add_bounded" in + let add_bounded := pose_add_bounded r sz m_enc montgomery_to_F add_ext add_sig add_bounded in + Tag.update pkg TAG.add_bounded add_bounded) + ltac:(fun _ => pkg) + (). +Ltac add_sub_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let sub_ext := Tag.get pkg TAG.sub_ext in + let sub_sig := fresh "sub_sig" in + let sub_sig := pose_sub_sig r sz m_enc montgomery_to_F sub_ext sub_sig in + Tag.update pkg TAG.sub_sig sub_sig) + ltac:(fun _ => pkg) + (). +Ltac add_sub_bounded pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let sub_ext := Tag.get pkg TAG.sub_ext in + let sub_sig := Tag.get pkg TAG.sub_sig in + let sub_bounded := fresh "sub_bounded" in + let sub_bounded := pose_sub_bounded r sz m_enc montgomery_to_F sub_ext sub_sig sub_bounded in + Tag.update pkg TAG.sub_bounded sub_bounded) + ltac:(fun _ => pkg) + (). +Ltac add_opp_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let opp_ext := Tag.get pkg TAG.opp_ext in + let opp_sig := fresh "opp_sig" in + let opp_sig := pose_opp_sig r sz m_enc montgomery_to_F opp_ext opp_sig in + Tag.update pkg TAG.opp_sig opp_sig) + ltac:(fun _ => pkg) + (). +Ltac add_opp_bounded pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let opp_ext := Tag.get pkg TAG.opp_ext in + let opp_sig := Tag.get pkg TAG.opp_sig in + let opp_bounded := fresh "opp_bounded" in + let opp_bounded := pose_opp_bounded r sz m_enc montgomery_to_F opp_ext opp_sig opp_bounded in + Tag.update pkg TAG.opp_bounded opp_bounded) + ltac:(fun _ => pkg) + (). +Ltac add_nonzero_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let nonzero_ext := Tag.get pkg TAG.nonzero_ext in + let nonzero_sig := fresh "nonzero_sig" in + let nonzero_sig := pose_nonzero_sig r sz m m_enc montgomery_to_F nonzero_ext nonzero_sig in + Tag.update pkg TAG.nonzero_sig nonzero_sig) + ltac:(fun _ => pkg) + (). +Ltac add_ring pkg := + if_montgomery + pkg + ltac:(fun _ => let ring := fresh "ring" in + let ring := pose_ring ring in + Tag.update pkg TAG.ring ring) + ltac:(fun _ => pkg) + (). +Ltac add_carry_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let carry_sig := fresh "carry_sig" in + let carry_sig := pose_carry_sig carry_sig in + Tag.update pkg TAG.carry_sig carry_sig) + ltac:(fun _ => pkg) + (). +Ltac add_freeze_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let freeze_sig := fresh "freeze_sig" in + let freeze_sig := pose_freeze_sig freeze_sig in + Tag.update pkg TAG.freeze_sig freeze_sig) + ltac:(fun _ => pkg) + (). +Ltac add_Mxzladderstep_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in + let Mxzladderstep_sig := pose_Mxzladderstep_sig Mxzladderstep_sig in + Tag.update pkg TAG.Mxzladderstep_sig Mxzladderstep_sig) + ltac:(fun _ => pkg) + (). +Ltac add_Montgomery_package pkg := + let pkg := add_m' pkg in + let pkg := add_r' pkg in + let pkg := add_m'_correct pkg in + let pkg := add_r'_correct pkg in + let pkg := add_m_enc_correct_montgomery pkg in + let pkg := add_r'_pow_correct pkg in + let pkg := add_montgomery_to_F pkg in + let pkg := add_r_big pkg in + let pkg := add_m_big pkg in + let pkg := add_m_enc_small pkg in + let pkg := add_map_m_enc pkg in + let pkg := add_mul_ext pkg in + let pkg := add_add_ext pkg in + let pkg := add_sub_ext pkg in + let pkg := add_opp_ext pkg in + let pkg := add_nonzero_ext pkg in + let pkg := add_mul_sig pkg in + let pkg := add_mul_bounded pkg in + let pkg := add_add_sig pkg in + let pkg := add_add_bounded pkg in + let pkg := add_sub_sig pkg in + let pkg := add_sub_bounded pkg in + let pkg := add_opp_sig pkg in + let pkg := add_opp_bounded pkg in + let pkg := add_nonzero_sig pkg in + let pkg := add_ring pkg in + let pkg := add_carry_sig pkg in + let pkg := add_freeze_sig pkg in + let pkg := add_Mxzladderstep_sig pkg in + Tag.strip_local pkg. + + +Module MakeMontgomeryPackage (PKG : PrePackage). + Module Import MakeMontgomeryPackageInternal := MakePackageBase PKG. + + Ltac get_m' _ := get TAG.m'. + Notation m' := (ltac:(let v := get_m' () in exact v)) (only parsing). + Ltac get_r' _ := get TAG.r'. + Notation r' := (ltac:(let v := get_r' () in exact v)) (only parsing). + Ltac get_m'_correct _ := get TAG.m'_correct. + Notation m'_correct := (ltac:(let v := get_m'_correct () in exact v)) (only parsing). + Ltac get_r'_correct _ := get TAG.r'_correct. + Notation r'_correct := (ltac:(let v := get_r'_correct () in exact v)) (only parsing). + Ltac get_m_enc_correct_montgomery _ := get TAG.m_enc_correct_montgomery. + Notation m_enc_correct_montgomery := (ltac:(let v := get_m_enc_correct_montgomery () in exact v)) (only parsing). + Ltac get_r'_pow_correct _ := get TAG.r'_pow_correct. + Notation r'_pow_correct := (ltac:(let v := get_r'_pow_correct () in exact v)) (only parsing). + Ltac get_montgomery_to_F _ := get TAG.montgomery_to_F. + Notation montgomery_to_F := (ltac:(let v := get_montgomery_to_F () in exact v)) (only parsing). + Ltac get_r_big _ := get TAG.r_big. + Notation r_big := (ltac:(let v := get_r_big () in exact v)) (only parsing). + Ltac get_m_big _ := get TAG.m_big. + Notation m_big := (ltac:(let v := get_m_big () in exact v)) (only parsing). + Ltac get_m_enc_small _ := get TAG.m_enc_small. + Notation m_enc_small := (ltac:(let v := get_m_enc_small () in exact v)) (only parsing). + Ltac get_map_m_enc _ := get TAG.map_m_enc. + Notation map_m_enc := (ltac:(let v := get_map_m_enc () in exact v)) (only parsing). + Ltac get_mul_ext _ := get TAG.mul_ext. + Notation mul_ext := (ltac:(let v := get_mul_ext () in exact v)) (only parsing). + Ltac get_add_ext _ := get TAG.add_ext. + Notation add_ext := (ltac:(let v := get_add_ext () in exact v)) (only parsing). + Ltac get_sub_ext _ := get TAG.sub_ext. + Notation sub_ext := (ltac:(let v := get_sub_ext () in exact v)) (only parsing). + Ltac get_opp_ext _ := get TAG.opp_ext. + Notation opp_ext := (ltac:(let v := get_opp_ext () in exact v)) (only parsing). + Ltac get_nonzero_ext _ := get TAG.nonzero_ext. + Notation nonzero_ext := (ltac:(let v := get_nonzero_ext () in exact v)) (only parsing). + Ltac get_mul_bounded _ := get TAG.mul_bounded. + Notation mul_bounded := (ltac:(let v := get_mul_bounded () in exact v)) (only parsing). + Ltac get_add_bounded _ := get TAG.add_bounded. + Notation add_bounded := (ltac:(let v := get_add_bounded () in exact v)) (only parsing). + Ltac get_sub_bounded _ := get TAG.sub_bounded. + Notation sub_bounded := (ltac:(let v := get_sub_bounded () in exact v)) (only parsing). + Ltac get_opp_bounded _ := get TAG.opp_bounded. + Notation opp_bounded := (ltac:(let v := get_opp_bounded () in exact v)) (only parsing). + Ltac get_nonzero_sig _ := get TAG.nonzero_sig. + Notation nonzero_sig := (ltac:(let v := get_nonzero_sig () in exact v)) (only parsing). +End MakeMontgomeryPackage. |