aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-10-15 11:02:58 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2017-10-18 23:01:29 -0400
commitfd2935407d6dfd5075a49dc44d00b54af0ef70fa (patch)
treec6668102b8e689d06181996e0a48b1ebc054d362 /src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
parentfb9206fbe7355d5672413a3ffb8c1d6ca5c1f80e (diff)
Move coef, coef_mod to gallina
Also pose mul_code, square_code After | File Name | Before || Change ------------------------------------------------------------------------------------------- 4m28.75s | Total | 4m31.79s || -0m03.03s ------------------------------------------------------------------------------------------- 1m57.67s | Specific/NISTP256/AMD64/femul | 2m00.16s || -0m02.48s 0m23.68s | Specific/NISTP256/AMD64/fesub | 0m23.69s || -0m00.01s 0m21.58s | Specific/NISTP256/AMD64/feadd | 0m21.76s || -0m00.18s 0m20.13s | Specific/X25519/C64/freeze | 0m19.99s || +0m00.14s 0m17.60s | Specific/NISTP256/AMD64/feopp | 0m17.82s || -0m00.21s 0m15.23s | Specific/NISTP256/AMD64/fenz | 0m15.24s || -0m00.00s 0m11.79s | Specific/X25519/C64/Synthesis | 0m11.98s || -0m00.19s 0m09.47s | Specific/NISTP256/AMD64/Synthesis | 0m09.57s || -0m00.09s 0m04.95s | Specific/X25519/C64/ladderstep | 0m04.96s || -0m00.00s 0m02.59s | Specific/NISTP256/AMD64/femulDisplay | 0m02.61s || -0m00.02s 0m02.33s | Specific/X25519/C64/femul | 0m02.26s || +0m00.07s 0m01.87s | Specific/NISTP256/AMD64/feaddDisplay | 0m01.88s || -0m00.00s 0m01.81s | Specific/NISTP256/AMD64/fesubDisplay | 0m01.80s || +0m00.01s 0m01.78s | Specific/X25519/C64/fesquare | 0m01.81s || -0m00.03s 0m01.66s | Specific/NISTP256/AMD64/feoppDisplay | 0m01.66s || +0m00.00s 0m01.48s | Specific/NISTP256/AMD64/fenzDisplay | 0m01.46s || +0m00.02s 0m01.46s | Specific/X25519/C64/freezeDisplay | 0m01.45s || +0m00.01s 0m01.07s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m01.14s || -0m00.06s 0m01.03s | Specific/Framework/ArithmeticSynthesis/Base | 0m00.87s || +0m00.16s 0m00.99s | Specific/Framework/SynthesisFramework | 0m01.04s || -0m00.05s 0m00.80s | Specific/Framework/MontgomeryReificationTypesPackage | 0m00.75s || +0m00.05s 0m00.77s | Specific/Framework/ReificationTypesPackage | 0m00.76s || +0m00.01s 0m00.75s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m00.76s || -0m00.01s 0m00.74s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.75s || -0m00.01s 0m00.72s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.74s || -0m00.02s 0m00.72s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.77s || -0m00.05s 0m00.71s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.68s || +0m00.02s 0m00.71s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.71s || +0m00.00s 0m00.70s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.74s || -0m00.04s 0m00.69s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.67s || +0m00.01s 0m00.69s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.70s || -0m00.01s 0m00.32s | Specific/Framework/CurveParametersPackage | 0m00.32s || +0m00.00s 0m00.27s | Specific/Framework/CurveParameters | 0m00.30s || -0m00.02s
Diffstat (limited to 'src/Specific/Framework/ArithmeticSynthesis/BasePackage.v')
-rw-r--r--src/Specific/Framework/ArithmeticSynthesis/BasePackage.v15
1 files changed, 7 insertions, 8 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
index 791762975..ea53542a1 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
@@ -69,20 +69,17 @@ Ltac add_m_correct pkg :=
Ltac add_m_enc pkg :=
let sz := Tag.get pkg TAG.sz in
- let s := Tag.get pkg TAG.s in
- let c := Tag.get pkg TAG.c in
- let wt := Tag.get pkg TAG.wt in
+ let m := Tag.get pkg TAG.m in
let m_enc := fresh "m_enc" in
- let m_enc := pose_m_enc sz s c wt m_enc in
+ let m_enc := pose_m_enc sz m m_enc in
Tag.update pkg TAG.m_enc m_enc.
Ltac add_coef pkg :=
let sz := Tag.get pkg TAG.sz in
- let wt := Tag.get pkg TAG.wt in
- let m_enc := Tag.get pkg TAG.m_enc in
+ let m := Tag.get pkg TAG.m in
let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in
let coef := fresh "coef" in
- let coef := pose_coef sz wt m_enc coef_div_modulus coef in
+ let coef := pose_coef sz m coef_div_modulus coef in
Tag.update pkg TAG.coef coef.
Ltac add_coef_mod pkg :=
@@ -90,8 +87,10 @@ Ltac add_coef_mod pkg :=
let wt := Tag.get pkg TAG.wt in
let m := Tag.get pkg TAG.m in
let coef := Tag.get pkg TAG.coef in
+ let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in
+ let sz_le_log2_m := Tag.get pkg TAG.sz_le_log2_m in
let coef_mod := fresh "coef_mod" in
- let coef_mod := pose_coef_mod sz wt m coef coef_mod in
+ let coef_mod := pose_coef_mod sz wt m coef coef_div_modulus sz_le_log2_m coef_mod in
Tag.update pkg TAG.coef_mod coef_mod.
Ltac add_sz_nonzero pkg :=