From 6ea13f7ad4cddb5886b4602b299da164ac140f89 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 3 Aug 2016 10:02:12 -0700 Subject: Add {push,pull}_Zdiv databases After | File Name | Before || Change ---------------------------------------------------------------------------------- 1m43.16s | Total | 1m44.38s || -0m01.21s ---------------------------------------------------------------------------------- 0m15.14s | ModularArithmetic/ModularBaseSystemProofs | 0m16.70s || -0m01.55s 0m32.63s | Specific/GF25519 | 0m32.58s || +0m00.05s 0m11.49s | Experiments/SpecEd25519 | 0m11.35s || +0m00.14s 0m07.46s | Specific/GF1305 | 0m07.13s || +0m00.33s 0m04.06s | ModularArithmetic/Pow2BaseProofs | 0m04.02s || +0m00.04s 0m03.72s | ModularArithmetic/Tutorial | 0m03.70s || +0m00.02s 0m03.71s | BaseSystemProofs | 0m03.68s || +0m00.02s 0m03.21s | ModularArithmetic/ModularBaseSystemOpt | 0m03.24s || -0m00.03s 0m02.70s | Util/ZUtil | 0m02.75s || -0m00.04s 0m01.59s | ModularArithmetic/PrimeFieldTheorems | 0m01.53s || +0m00.06s 0m01.57s | ModularArithmetic/ModularArithmeticTheorems | 0m01.54s || +0m00.03s 0m01.51s | Encoding/PointEncodingPre | 0m01.48s || +0m00.03s 0m01.18s | BaseSystem | 0m01.18s || +0m00.00s 0m01.14s | ModularArithmetic/ExtendedBaseVector | 0m01.09s || +0m00.04s 0m00.98s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.96s || +0m00.02s 0m00.96s | ModularArithmetic/BarrettReduction/Z | 0m00.95s || +0m00.01s 0m00.86s | ModularArithmetic/ModularBaseSystemField | 0m00.92s || -0m00.06s 0m00.85s | Util/NumTheoryUtil | 0m00.86s || -0m00.01s 0m00.84s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.83s || +0m00.01s 0m00.83s | ModularArithmetic/ModularBaseSystemList | 0m00.88s || -0m00.05s 0m00.71s | Experiments/SpecificCurve25519 | 0m00.70s || +0m00.01s 0m00.68s | Encoding/ModularWordEncodingTheorems | 0m00.66s || +0m00.02s 0m00.65s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.94s || -0m00.28s 0m00.65s | Testbit | 0m00.65s || +0m00.00s 0m00.63s | Spec/ModularWordEncoding | 0m00.60s || +0m00.03s 0m00.63s | Encoding/ModularWordEncodingPre | 0m00.65s || -0m00.02s 0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.60s || +0m00.00s 0m00.57s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.00s 0m00.47s | ModularArithmetic/Pre | 0m00.46s || +0m00.00s 0m00.39s | ModularArithmetic/Pow2Base | 0m00.42s || -0m00.02s 0m00.38s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.40s || -0m00.02s 0m00.38s | Spec/ModularArithmetic | 0m00.36s || +0m00.02s --- src/Util/ZUtil.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 1e0ed36e4..773a4818d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -35,6 +35,8 @@ Create HintDb push_Zpow discriminated. Create HintDb pull_Zpow discriminated. Create HintDb push_Zmul discriminated. Create HintDb pull_Zmul discriminated. +Create HintDb push_Zdiv discriminated. +Create HintDb pull_Zdiv discriminated. Create HintDb pull_Zmod discriminated. Create HintDb push_Zmod discriminated. Hint Extern 1 => autorewrite with push_Zopp in * : push_Zopp. @@ -43,6 +45,8 @@ Hint Extern 1 => autorewrite with push_Zpow in * : push_Zpow. Hint Extern 1 => autorewrite with pull_Zpow in * : pull_Zpow. Hint Extern 1 => autorewrite with push_Zmul in * : push_Zmul. Hint Extern 1 => autorewrite with pull_Zmul in * : pull_Zmul. +Hint Extern 1 => autorewrite with push_Zdiv in * : push_Zmul. +Hint Extern 1 => autorewrite with pull_Zdiv in * : pull_Zmul. Hint Extern 1 => autorewrite with pull_Zmod in * : pull_Zmod. Hint Extern 1 => autorewrite with push_Zmod in * : push_Zmod. Hint Rewrite Z.div_opp_l_nz Z.div_opp_l_z using lia : pull_Zopp. @@ -55,6 +59,8 @@ Hint Rewrite Z.pow_sub_r Z.pow_div_l Z.pow_twice_r Z.pow_mul_l Z.pow_add_r using Hint Rewrite <- Z.pow_sub_r Z.pow_div_l Z.pow_mul_l Z.pow_add_r Z.pow_twice_r using lia : pull_Zpow. Hint Rewrite Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : push_Zmul. Hint Rewrite <- Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : pull_Zmul. +Hint Rewrite Z.div_div using lia : pull_Zdiv. +Hint Rewrite <- Z.div_div using lia : push_Zdiv. Hint Rewrite <- Z.mul_mod Z.add_mod Zminus_mod using lia : pull_Zmod. Hint Rewrite Zminus_mod_idemp_l Zminus_mod_idemp_r : pull_Zmod. -- cgit v1.2.3