aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
Commit message (Collapse)AuthorAge
...
* Add ZUtil lemmasGravatar Jason Gross2017-02-06
|
* Move things from WordUtil to ZUtil, add word lemmaGravatar Jason Gross2017-02-06
|
* More zutilGravatar Jason Gross2017-02-03
|
* Add lemmas about bounds of Z.lor, and add Z.max_log2_upGravatar Jason Gross2017-02-03
|
* Add lemmas for Z ops ProperGravatar Jason Gross2017-02-03
|
* Add log2_up_le_fullGravatar Jason Gross2017-02-03
|
* Add Z.log2_up_nonneg to zarithGravatar Jason Gross2017-02-03
|
* Add ZUtil lemma from zetabaseGravatar Jason Gross2017-01-19
|
* Add Zmod_to_equiv_moduloGravatar Jason Gross2017-01-09
|
* Fix precedence issue with 8.4Gravatar Jason Gross2016-11-08
|
* Prove things in ModularBaseSystemListZOperationsProofsGravatar Jason Gross2016-11-08
|
* Add log2_lt_pow2_altGravatar Jason Gross2016-11-08
|
* Work around bug 5189 (broken [Hint Resolve ->])Gravatar Jason Gross2016-11-08
| | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5189, [Hint Resolve <- foo] does not survive the end of modules
* Add Z.lor_nonneg to zarithGravatar Jason Gross2016-11-08
|
* Z.ltb_to_lt now works in the goal, tooGravatar Jason Gross2016-11-05
|
* Add ZUtil.Z.log2_ones_lt_nonnegGravatar Jason Gross2016-11-02
|
* Add more ZUtilGravatar Jason Gross2016-11-02
|
* Add ZUtil lemmaGravatar Jason Gross2016-11-02
|
* Add ZUtil lemmaGravatar Jason Gross2016-11-02
|
* Add a ZUtil lemmaGravatar Jason Gross2016-11-02
|
* prove testbit_sub_pow2Gravatar Andres Erbsen2016-10-29
|
* Add some rewrites and admitted lemmasGravatar Jason Gross2016-10-27
|
* Add {push,pull}_Zof_N hint db to ZUtilGravatar Jason Gross2016-10-27
|
* prove admit about F.to_nat x mod mGravatar Andres Erbsen2016-10-27
|
* Add more simplify lemmas to ZUtilGravatar Jason Gross2016-10-17
|
* Add more simplify lemmas to ZUtilGravatar Jason Gross2016-10-17
|
* Add ZUtil lemmaGravatar Jason Gross2016-10-17
|
* Fix compatibility with sigT notationGravatar Jason Gross2016-10-10
|
* Make Ztestbit_fullGravatar Jason Gross2016-10-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It doesn't call autorewrite with Ztestbit After | File Name | Before || Change --------------------------------------------------------------------------------------------- 5m54.66s | Total | 6m23.36s || -0m28.69s --------------------------------------------------------------------------------------------- 0m35.89s | ModularArithmetic/Conversion | 0m40.00s || -0m04.10s 1m34.54s | Test/Curve25519SpecTestVectors | 1m38.00s || -0m03.46s 0m21.20s | ModularArithmetic/Pow2BaseProofs | 0m24.65s || -0m03.44s 0m19.47s | EdDSARepChange | 0m21.84s || -0m02.37s 0m10.19s | Testbit | 0m12.63s || -0m02.44s 0m08.34s | ModularArithmetic/Montgomery/ZProofs | 0m09.42s || -0m01.08s 0m07.96s | Encoding/PointEncoding | 0m09.16s || -0m01.20s 0m03.35s | ModularArithmetic/Tutorial | 0m04.54s || -0m01.18s 0m27.76s | ModularArithmetic/ModularBaseSystemProofs | 0m28.15s || -0m00.38s 0m14.36s | Specific/GF25519 | 0m14.43s || -0m00.07s 0m12.87s | Util/ZUtil | 0m13.72s || -0m00.85s 0m08.48s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.79s || -0m00.30s 0m08.09s | BoundedArithmetic/Double/Proofs/Multiply | 0m08.44s || -0m00.34s 0m07.75s | Specific/GF1305 | 0m07.64s || +0m00.11s 0m07.03s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m07.38s || -0m00.34s 0m05.34s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m05.46s || -0m00.12s 0m04.05s | BaseSystemProofs | 0m04.50s || -0m00.45s 0m03.76s | ModularArithmetic/BarrettReduction/ZHandbook | 0m04.04s || -0m00.28s 0m03.44s | ModularArithmetic/ModularBaseSystemListProofs | 0m03.53s || -0m00.08s 0m03.32s | BoundedArithmetic/InterfaceProofs | 0m03.58s || -0m00.26s 0m03.04s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.22s || -0m00.18s 0m02.86s | Encoding/PointEncodingPre | 0m02.92s || -0m00.06s 0m02.74s | BoundedArithmetic/Double/Proofs/Decode | 0m03.60s || -0m00.85s 0m02.66s | ModularArithmetic/ModularArithmeticTheorems | 0m03.44s || -0m00.77s 0m02.42s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.47s || -0m00.05s 0m02.34s | ModularArithmetic/ModularBaseSystemOpt | 0m02.39s || -0m00.05s 0m02.08s | Specific/FancyMachine256/Barrett | 0m02.24s || -0m00.16s 0m02.01s | Specific/FancyMachine256/Montgomery | 0m02.45s || -0m00.44s 0m01.78s | ModularArithmetic/Montgomery/ZBounded | 0m01.92s || -0m00.13s 0m01.78s | Specific/FancyMachine256/Core | 0m01.77s || +0m00.01s 0m01.54s | ModularArithmetic/BarrettReduction/Z | 0m01.52s || +0m00.02s 0m01.34s | ModularArithmetic/PrimeFieldTheorems | 0m01.59s || -0m00.25s 0m01.24s | BaseSystem | 0m01.20s || +0m00.04s 0m01.09s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.14s || -0m00.04s 0m01.08s | ModularArithmetic/ExtendedBaseVector | 0m01.25s || -0m00.16s 0m00.96s | Util/NumTheoryUtil | 0m00.99s || -0m00.03s 0m00.88s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m01.14s || -0m00.25s 0m00.86s | Experiments/EncodingLemmas | 0m00.93s || -0m00.07s 0m00.83s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m01.10s || -0m00.27s 0m00.66s | BoundedArithmetic/X86ToZLike | 0m00.73s || -0m00.06s 0m00.66s | Spec/EdDSA | 0m00.66s || +0m00.00s 0m00.66s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.80s || -0m00.14s 0m00.65s | ModularArithmetic/ModularBaseSystem | 0m00.59s || +0m00.06s 0m00.63s | Encoding/ModularWordEncodingTheorems | 0m00.77s || -0m00.14s 0m00.62s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.62s || +0m00.00s 0m00.60s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.98s || -0m00.38s 0m00.60s | ModularArithmetic/ModularBaseSystemList | 0m00.66s || -0m00.06s 0m00.60s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.58s || +0m00.02s 0m00.58s | Encoding/ModularWordEncodingPre | 0m00.71s || -0m00.13s 0m00.54s | Spec/Ed25519 | 0m00.63s || -0m00.08s 0m00.53s | BoundedArithmetic/Interface | 0m00.90s || -0m00.37s 0m00.53s | Spec/ModularWordEncoding | 0m00.65s || -0m00.12s 0m00.52s | ModularArithmetic/ZBounded | 0m00.67s || -0m00.15s 0m00.52s | BoundedArithmetic/ArchitectureToZLike | 0m00.64s || -0m00.12s 0m00.50s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.47s || +0m00.03s 0m00.50s | BoundedArithmetic/Double/Repeated/Core | 0m00.56s || -0m00.06s 0m00.49s | ModularArithmetic/Pre | 0m00.52s || -0m00.03s 0m00.48s | BoundedArithmetic/StripCF | 0m00.52s || -0m00.04s 0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.52s || -0m00.06s 0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.47s || -0m00.00s 0m00.46s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.46s || +0m00.00s 0m00.45s | BoundedArithmetic/Double/Core | 0m00.70s || -0m00.24s 0m00.43s | Spec/ModularArithmetic | 0m00.35s || +0m00.08s 0m00.42s | ModularArithmetic/Montgomery/Z | 0m00.42s || +0m00.00s 0m00.40s | ModularArithmetic/Pow2Base | 0m00.60s || -0m00.19s
* Fix Ztestbit_full databaseGravatar Jason Gross2016-10-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change --------------------------------------------------------------------------------------------- 5m59.20s | Total | 5m54.42s || +0m04.78s --------------------------------------------------------------------------------------------- 0m22.58s | ModularArithmetic/Pow2BaseProofs | 0m21.32s || +0m01.25s 1m35.12s | Test/Curve25519SpecTestVectors | 1m35.10s || +0m00.02s 0m35.67s | ModularArithmetic/Conversion | 0m35.54s || +0m00.13s 0m27.70s | ModularArithmetic/ModularBaseSystemProofs | 0m27.46s || +0m00.23s 0m20.14s | EdDSARepChange | 0m19.42s || +0m00.71s 0m14.57s | Specific/GF25519 | 0m14.69s || -0m00.11s 0m13.16s | Util/ZUtil | 0m12.89s || +0m00.26s 0m10.09s | Testbit | 0m09.77s || +0m00.32s 0m08.77s | ModularArithmetic/Montgomery/ZProofs | 0m08.57s || +0m00.19s 0m08.38s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.34s || +0m00.04s 0m08.04s | Encoding/PointEncoding | 0m08.09s || -0m00.05s 0m08.01s | BoundedArithmetic/Double/Proofs/Multiply | 0m08.00s || +0m00.00s 0m07.86s | Specific/GF1305 | 0m07.96s || -0m00.09s 0m07.14s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m06.73s || +0m00.40s 0m05.45s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m05.31s || +0m00.14s 0m03.85s | BaseSystemProofs | 0m03.83s || +0m00.02s 0m03.83s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.77s || +0m00.06s 0m03.46s | ModularArithmetic/ModularBaseSystemListProofs | 0m03.54s || -0m00.08s 0m03.36s | ModularArithmetic/Tutorial | 0m03.46s || -0m00.10s 0m03.36s | BoundedArithmetic/InterfaceProofs | 0m03.29s || +0m00.06s 0m02.98s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.05s || -0m00.06s 0m02.86s | Encoding/PointEncodingPre | 0m02.76s || +0m00.10s 0m02.85s | ModularArithmetic/ModularArithmeticTheorems | 0m02.61s || +0m00.24s 0m02.80s | BoundedArithmetic/Double/Proofs/Decode | 0m02.76s || +0m00.04s 0m02.46s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.23s || +0m00.23s 0m02.35s | ModularArithmetic/ModularBaseSystemOpt | 0m02.44s || -0m00.08s 0m02.13s | Specific/FancyMachine256/Barrett | 0m01.99s || +0m00.13s 0m02.08s | Specific/FancyMachine256/Montgomery | 0m02.10s || -0m00.02s 0m01.80s | ModularArithmetic/PrimeFieldTheorems | 0m01.33s || +0m00.47s 0m01.76s | ModularArithmetic/Montgomery/ZBounded | 0m01.84s || -0m00.08s 0m01.76s | Specific/FancyMachine256/Core | 0m01.70s || +0m00.06s 0m01.50s | ModularArithmetic/BarrettReduction/Z | 0m01.47s || +0m00.03s 0m01.23s | BaseSystem | 0m01.32s || -0m00.09s 0m01.22s | ModularArithmetic/ExtendedBaseVector | 0m01.23s || -0m00.01s 0m01.15s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.05s || +0m00.09s 0m00.97s | Util/NumTheoryUtil | 0m00.84s || +0m00.13s 0m00.92s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m00.95s || -0m00.02s 0m00.90s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m00.81s || +0m00.08s 0m00.89s | Experiments/EncodingLemmas | 0m00.89s || +0m00.00s 0m00.76s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.65s || +0m00.10s 0m00.65s | BoundedArithmetic/X86ToZLike | 0m00.62s || +0m00.03s 0m00.65s | ModularArithmetic/ModularBaseSystem | 0m00.56s || +0m00.08s 0m00.64s | BoundedArithmetic/Interface | 0m00.73s || -0m00.08s 0m00.62s | Spec/ModularWordEncoding | 0m00.64s || -0m00.02s 0m00.61s | Encoding/ModularWordEncodingTheorems | 0m00.65s || -0m00.04s 0m00.60s | Encoding/ModularWordEncodingPre | 0m00.62s || -0m00.02s 0m00.60s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.44s || +0m00.15s 0m00.60s | Spec/EdDSA | 0m00.63s || -0m00.03s 0m00.55s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.67s || -0m00.12s 0m00.55s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.45s || +0m00.10s 0m00.55s | ModularArithmetic/ModularBaseSystemList | 0m00.63s || -0m00.07s 0m00.55s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.61s || -0m00.05s 0m00.53s | BoundedArithmetic/Double/Repeated/Core | 0m00.51s || +0m00.02s 0m00.52s | ModularArithmetic/Pre | 0m00.51s || +0m00.01s 0m00.52s | BoundedArithmetic/StripCF | 0m00.54s || -0m00.02s 0m00.52s | Spec/Ed25519 | 0m00.48s || +0m00.04s 0m00.50s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.49s || +0m00.01s 0m00.49s | ModularArithmetic/ZBounded | 0m00.51s || -0m00.02s 0m00.49s | BoundedArithmetic/Double/Core | 0m00.50s || -0m00.01s 0m00.48s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.44s || +0m00.03s 0m00.46s | ModularArithmetic/Pow2Base | 0m00.50s || -0m00.03s 0m00.46s | BoundedArithmetic/ArchitectureToZLike | 0m00.46s || +0m00.00s 0m00.42s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.41s || +0m00.01s 0m00.37s | ModularArithmetic/Montgomery/Z | 0m00.41s || -0m00.03s 0m00.36s | Spec/ModularArithmetic | 0m00.31s || +0m00.04s
* Fix shiftr_spec_fullGravatar Jason Gross2016-10-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change --------------------------------------------------------------------------------------------- 5m54.81s | Total | 6m41.78s || -0m46.96s --------------------------------------------------------------------------------------------- 0m21.93s | ModularArithmetic/Pow2BaseProofs | 0m28.72s || -0m06.78s 0m35.50s | ModularArithmetic/Conversion | 0m40.00s || -0m04.50s 0m19.50s | EdDSARepChange | 0m23.84s || -0m04.33s 1m34.67s | Test/Curve25519SpecTestVectors | 1m38.63s || -0m03.95s 0m08.55s | ModularArithmetic/Montgomery/ZProofs | 0m11.52s || -0m02.96s 0m10.05s | Testbit | 0m11.42s || -0m01.36s 0m08.01s | BoundedArithmetic/Double/Proofs/Multiply | 0m09.97s || -0m01.96s 0m03.88s | BaseSystemProofs | 0m05.09s || -0m01.20s 0m03.74s | ModularArithmetic/BarrettReduction/ZHandbook | 0m05.44s || -0m01.70s 0m03.40s | BoundedArithmetic/InterfaceProofs | 0m05.01s || -0m01.60s 0m03.32s | ModularArithmetic/Tutorial | 0m04.34s || -0m01.02s 0m02.98s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m04.29s || -0m01.31s 0m02.59s | ModularArithmetic/ModularArithmeticTheorems | 0m03.70s || -0m01.11s 0m27.38s | ModularArithmetic/ModularBaseSystemProofs | 0m27.26s || +0m00.11s 0m14.42s | Specific/GF25519 | 0m14.47s || -0m00.05s 0m12.86s | Util/ZUtil | 0m13.54s || -0m00.67s 0m08.46s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.98s || -0m00.51s 0m08.02s | Encoding/PointEncoding | 0m08.90s || -0m00.88s 0m07.66s | Specific/GF1305 | 0m07.85s || -0m00.18s 0m06.74s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m07.62s || -0m00.87s 0m05.41s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m06.22s || -0m00.80s 0m03.49s | ModularArithmetic/ModularBaseSystemListProofs | 0m03.44s || +0m00.05s 0m02.96s | Encoding/PointEncodingPre | 0m03.80s || -0m00.83s 0m02.75s | BoundedArithmetic/Double/Proofs/Decode | 0m03.70s || -0m00.95s 0m02.34s | ModularArithmetic/ModularBaseSystemOpt | 0m02.36s || -0m00.02s 0m02.19s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.94s || -0m00.75s 0m02.08s | Specific/FancyMachine256/Montgomery | 0m02.08s || +0m00.00s 0m02.04s | Specific/FancyMachine256/Barrett | 0m02.05s || -0m00.00s 0m01.77s | ModularArithmetic/Montgomery/ZBounded | 0m02.06s || -0m00.29s 0m01.76s | ModularArithmetic/PrimeFieldTheorems | 0m01.78s || -0m00.02s 0m01.70s | Specific/FancyMachine256/Core | 0m01.70s || +0m00.00s 0m01.47s | ModularArithmetic/BarrettReduction/Z | 0m02.00s || -0m00.53s 0m01.30s | BaseSystem | 0m01.27s || +0m00.03s 0m01.13s | ModularArithmetic/ExtendedBaseVector | 0m01.40s || -0m00.27s 0m01.05s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.14s || -0m00.08s 0m00.92s | Util/NumTheoryUtil | 0m01.40s || -0m00.47s 0m00.86s | Experiments/EncodingLemmas | 0m01.38s || -0m00.51s 0m00.84s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m00.98s || -0m00.14s 0m00.82s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m00.90s || -0m00.08s 0m00.70s | BoundedArithmetic/Interface | 0m00.92s || -0m00.22s 0m00.70s | Spec/EdDSA | 0m00.97s || -0m00.27s 0m00.69s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.66s || +0m00.02s 0m00.69s | ModularArithmetic/ModularBaseSystem | 0m00.67s || +0m00.01s 0m00.66s | Encoding/ModularWordEncodingPre | 0m00.61s || +0m00.05s 0m00.66s | BoundedArithmetic/X86ToZLike | 0m01.01s || -0m00.35s 0m00.64s | ModularArithmetic/ModularBaseSystemList | 0m00.62s || +0m00.02s 0m00.64s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.79s || -0m00.15s 0m00.61s | Encoding/ModularWordEncodingTheorems | 0m01.02s || -0m00.41s 0m00.58s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.66s || -0m00.08s 0m00.56s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.84s || -0m00.27s 0m00.56s | Spec/ModularWordEncoding | 0m00.73s || -0m00.16s 0m00.55s | ModularArithmetic/ZBounded | 0m00.56s || -0m00.01s 0m00.55s | Spec/Ed25519 | 0m00.78s || -0m00.23s 0m00.52s | BoundedArithmetic/Double/Core | 0m00.57s || -0m00.04s 0m00.52s | BoundedArithmetic/ArchitectureToZLike | 0m00.64s || -0m00.12s 0m00.52s | BoundedArithmetic/Double/Repeated/Core | 0m00.71s || -0m00.18s 0m00.50s | BoundedArithmetic/StripCF | 0m00.70s || -0m00.19s 0m00.49s | ModularArithmetic/Pre | 0m00.74s || -0m00.25s 0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.74s || -0m00.27s 0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.72s || -0m00.25s 0m00.44s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.58s || -0m00.13s 0m00.44s | ModularArithmetic/Pow2Base | 0m00.63s || -0m00.19s 0m00.42s | ModularArithmetic/Montgomery/Z | 0m00.61s || -0m00.19s 0m00.36s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.60s || -0m00.24s 0m00.34s | Spec/ModularArithmetic | 0m00.52s || -0m00.18s
* Add more to Ztestbit_fullGravatar Jason Gross2016-10-09
|
* Add a Ztestbit_full databaseGravatar Jason Gross2016-10-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change --------------------------------------------------------------------------------------------- 6m00.58s | Total | 6m23.23s || -0m22.64s --------------------------------------------------------------------------------------------- 0m35.50s | ModularArithmetic/Conversion | 0m39.25s || -0m03.75s 1m35.19s | Test/Curve25519SpecTestVectors | 1m38.04s || -0m02.84s 0m06.69s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | 0m08.83s || -0m02.13s 0m27.51s | ModularArithmetic/ModularBaseSystemProofs | 0m28.99s || -0m01.47s 0m08.13s | Encoding/PointEncoding | 0m09.64s || -0m01.50s 0m05.25s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | 0m06.96s || -0m01.71s 0m22.82s | ModularArithmetic/Pow2BaseProofs | 0m23.37s || -0m00.55s 0m20.17s | EdDSARepChange | 0m20.89s || -0m00.71s 0m14.41s | Specific/GF25519 | 0m14.81s || -0m00.40s 0m13.08s | Util/ZUtil | 0m13.30s || -0m00.22s 0m10.31s | Testbit | 0m10.50s || -0m00.18s 0m09.57s | ModularArithmetic/Montgomery/ZProofs | 0m09.74s || -0m00.16s 0m08.46s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.68s || -0m00.21s 0m08.16s | BoundedArithmetic/Double/Proofs/Multiply | 0m09.02s || -0m00.85s 0m07.64s | Specific/GF1305 | 0m07.94s || -0m00.30s 0m04.01s | ModularArithmetic/Tutorial | 0m03.61s || +0m00.39s 0m03.91s | BaseSystemProofs | 0m04.01s || -0m00.09s 0m03.86s | ModularArithmetic/BarrettReduction/ZHandbook | 0m04.40s || -0m00.54s 0m03.46s | ModularArithmetic/ModularBaseSystemListProofs | 0m03.65s || -0m00.18s 0m03.37s | BoundedArithmetic/InterfaceProofs | 0m03.98s || -0m00.60s 0m03.28s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.78s || -0m00.50s 0m02.86s | Encoding/PointEncodingPre | 0m03.22s || -0m00.36s 0m02.78s | BoundedArithmetic/Double/Proofs/Decode | 0m03.25s || -0m00.47s 0m02.78s | ModularArithmetic/ModularArithmeticTheorems | 0m03.42s || -0m00.64s 0m02.31s | ModularArithmetic/ModularBaseSystemOpt | 0m02.38s || -0m00.06s 0m02.26s | Specific/FancyMachine256/Barrett | 0m02.80s || -0m00.54s 0m02.22s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.54s || -0m00.31s 0m02.07s | Specific/FancyMachine256/Montgomery | 0m02.31s || -0m00.24s 0m01.83s | ModularArithmetic/Montgomery/ZBounded | 0m02.12s || -0m00.29s 0m01.78s | Specific/FancyMachine256/Core | 0m01.78s || +0m00.00s 0m01.70s | ModularArithmetic/PrimeFieldTheorems | 0m01.38s || +0m00.32s 0m01.52s | ModularArithmetic/BarrettReduction/Z | 0m01.88s || -0m00.35s 0m01.38s | BaseSystem | 0m01.40s || -0m00.02s 0m01.24s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.16s || +0m00.08s 0m01.10s | ModularArithmetic/ExtendedBaseVector | 0m01.20s || -0m00.09s 0m01.05s | Util/NumTheoryUtil | 0m01.01s || +0m00.04s 0m00.88s | Experiments/EncodingLemmas | 0m00.93s || -0m00.05s 0m00.86s | BoundedArithmetic/Double/Proofs/LoadImmediate | 0m00.92s || -0m00.06s 0m00.84s | BoundedArithmetic/Double/Proofs/BitwiseOr | 0m01.19s || -0m00.35s 0m00.80s | Encoding/ModularWordEncodingPre | 0m00.61s || +0m00.19s 0m00.78s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.75s || +0m00.03s 0m00.71s | BoundedArithmetic/X86ToZLike | 0m00.89s || -0m00.18s 0m00.67s | Encoding/ModularWordEncodingTheorems | 0m00.72s || -0m00.04s 0m00.62s | BoundedArithmetic/Interface | 0m00.66s || -0m00.04s 0m00.62s | Spec/EdDSA | 0m00.59s || +0m00.03s 0m00.61s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.74s || -0m00.13s 0m00.61s | Spec/ModularWordEncoding | 0m00.69s || -0m00.07s 0m00.61s | ModularArithmetic/ModularBaseSystemList | 0m00.65s || -0m00.04s 0m00.60s | BoundedArithmetic/Double/Core | 0m00.49s || +0m00.10s 0m00.60s | Spec/Ed25519 | 0m00.50s || +0m00.09s 0m00.58s | ModularArithmetic/ModularBaseSystem | 0m00.62s || -0m00.04s 0m00.55s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.63s || -0m00.07s 0m00.53s | BoundedArithmetic/Double/Proofs/SelectConditional | 0m00.62s || -0m00.08s 0m00.51s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.55s || -0m00.04s 0m00.50s | BoundedArithmetic/StripCF | 0m00.51s || -0m00.01s 0m00.50s | BoundedArithmetic/ArchitectureToZLike | 0m00.48s || +0m00.02s 0m00.49s | ModularArithmetic/Pre | 0m00.47s || +0m00.02s 0m00.49s | BoundedArithmetic/Double/Repeated/Core | 0m00.48s || +0m00.01s 0m00.48s | ModularArithmetic/ZBounded | 0m00.50s || -0m00.02s 0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.54s || -0m00.08s 0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.54s || -0m00.08s 0m00.44s | ModularArithmetic/Pow2Base | 0m00.49s || -0m00.04s 0m00.40s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.44s || -0m00.03s 0m00.38s | ModularArithmetic/Montgomery/Z | 0m00.44s || -0m00.06s 0m00.35s | Spec/ModularArithmetic | 0m00.36s || -0m00.01s
* Stronger Ztestbit, convert_to_ztestbitGravatar Jason Gross2016-10-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 5m51.78s | Total | 5m58.93s || -0m07.15s ---------------------------------------------------------------------------------- 0m35.42s | ModularArithmetic/Conversion | 0m37.08s || -0m01.65s 0m22.17s | BoundedArithmetic/DoubleBoundedProofs | 0m23.61s || -0m01.43s 1m35.32s | Test/Curve25519SpecTestVectors | 1m36.20s || -0m00.88s 0m28.51s | ModularArithmetic/ModularBaseSystemProofs | 0m27.76s || +0m00.75s 0m22.26s | ModularArithmetic/Pow2BaseProofs | 0m22.74s || -0m00.47s 0m20.29s | EdDSARepChange | 0m19.76s || +0m00.52s 0m14.57s | Specific/GF25519 | 0m14.40s || +0m00.16s 0m13.05s | Util/ZUtil | 0m13.37s || -0m00.31s 0m09.95s | Testbit | 0m10.68s || -0m00.73s 0m08.56s | ModularArithmetic/Montgomery/ZProofs | 0m09.22s || -0m00.66s 0m08.34s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.38s || -0m00.04s 0m07.98s | Encoding/PointEncoding | 0m08.40s || -0m00.41s 0m07.75s | Specific/GF1305 | 0m08.07s || -0m00.32s 0m03.84s | ModularArithmetic/Tutorial | 0m03.43s || +0m00.40s 0m03.83s | BaseSystemProofs | 0m04.14s || -0m00.30s 0m03.79s | ModularArithmetic/BarrettReduction/ZHandbook | 0m04.31s || -0m00.51s 0m03.58s | ModularArithmetic/ModularBaseSystemListProofs | 0m03.57s || +0m00.01s 0m03.35s | BoundedArithmetic/InterfaceProofs | 0m03.53s || -0m00.17s 0m03.13s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m03.12s || +0m00.00s 0m02.84s | Encoding/PointEncodingPre | 0m02.83s || +0m00.00s 0m02.77s | ModularArithmetic/ModularArithmeticTheorems | 0m02.95s || -0m00.18s 0m02.42s | ModularArithmetic/ModularBaseSystemOpt | 0m02.20s || +0m00.21s 0m02.36s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.35s || +0m00.00s 0m02.22s | Specific/FancyMachine256/Montgomery | 0m02.10s || +0m00.12s 0m02.12s | Specific/FancyMachine256/Barrett | 0m02.39s || -0m00.27s 0m01.88s | ModularArithmetic/Montgomery/ZBounded | 0m01.97s || -0m00.09s 0m01.74s | Specific/FancyMachine256/Core | 0m01.76s || -0m00.02s 0m01.47s | ModularArithmetic/BarrettReduction/Z | 0m01.49s || -0m00.02s 0m01.35s | ModularArithmetic/PrimeFieldTheorems | 0m01.48s || -0m00.12s 0m01.31s | BaseSystem | 0m01.36s || -0m00.05s 0m01.28s | ModularArithmetic/ExtendedBaseVector | 0m01.50s || -0m00.21s 0m00.98s | Util/NumTheoryUtil | 0m01.12s || -0m00.14s 0m00.97s | Experiments/EncodingLemmas | 0m00.97s || +0m00.00s 0m00.69s | Encoding/ModularWordEncodingPre | 0m00.74s || -0m00.05s 0m00.67s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.80s || -0m00.13s 0m00.67s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.70s || -0m00.02s 0m00.66s | ModularArithmetic/ModularBaseSystem | 0m00.60s || +0m00.06s 0m00.66s | Encoding/ModularWordEncodingTheorems | 0m00.66s || +0m00.00s 0m00.64s | BoundedArithmetic/Interface | 0m00.58s || +0m00.06s 0m00.64s | ModularArithmetic/ModularBaseSystemList | 0m00.57s || +0m00.07s 0m00.61s | Spec/EdDSA | 0m00.66s || -0m00.05s 0m00.59s | Spec/Ed25519 | 0m00.57s || +0m00.02s 0m00.58s | Spec/ModularWordEncoding | 0m00.53s || +0m00.04s 0m00.53s | ModularArithmetic/Pre | 0m00.54s || -0m00.01s 0m00.51s | BoundedArithmetic/DoubleBounded | 0m00.50s || +0m00.01s 0m00.49s | BoundedArithmetic/ArchitectureToZLike | 0m00.43s || +0m00.06s 0m00.47s | ModularArithmetic/ZBounded | 0m00.47s || +0m00.00s 0m00.45s | BoundedArithmetic/StripCF | 0m00.46s || -0m00.01s 0m00.40s | ModularArithmetic/Pow2Base | 0m00.66s || -0m00.26s 0m00.40s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.42s || -0m00.01s 0m00.37s | ModularArithmetic/Montgomery/Z | 0m00.40s || -0m00.03s 0m00.35s | Spec/ModularArithmetic | 0m00.41s || -0m00.06s
* More zsimplify lemmas, stronger ZtestbitGravatar Jason Gross2016-10-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 5m47.85s | Total | 5m48.53s || -0m00.67s ---------------------------------------------------------------------------------- 1m34.28s | Test/Curve25519SpecTestVectors | 1m35.44s || -0m01.15s 0m35.79s | ModularArithmetic/Conversion | 0m36.48s || -0m00.68s 0m27.42s | ModularArithmetic/ModularBaseSystemProofs | 0m28.32s || -0m00.89s 0m22.15s | BoundedArithmetic/DoubleBoundedProofs | 0m21.67s || +0m00.47s 0m21.62s | ModularArithmetic/Pow2BaseProofs | 0m21.38s || +0m00.24s 0m19.60s | EdDSARepChange | 0m19.98s || -0m00.37s 0m14.52s | Specific/GF25519 | 0m14.89s || -0m00.37s 0m12.99s | Util/ZUtil | 0m12.60s || +0m00.39s 0m09.80s | Testbit | 0m09.45s || +0m00.35s 0m08.85s | ModularArithmetic/Montgomery/ZProofs | 0m08.11s || +0m00.74s 0m08.21s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.57s || -0m00.35s 0m07.85s | Encoding/PointEncoding | 0m08.24s || -0m00.39s 0m07.71s | Specific/GF1305 | 0m07.87s || -0m00.16s 0m03.94s | BaseSystemProofs | 0m03.85s || +0m00.08s 0m03.93s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.64s || +0m00.29s 0m03.52s | ModularArithmetic/Tutorial | 0m03.35s || +0m00.16s 0m03.48s | ModularArithmetic/ModularBaseSystemListProofs | 0m03.58s || -0m00.10s 0m03.36s | BoundedArithmetic/InterfaceProofs | 0m03.18s || +0m00.17s 0m03.16s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.89s || +0m00.27s 0m02.80s | Encoding/PointEncodingPre | 0m02.87s || -0m00.07s 0m02.65s | ModularArithmetic/ModularArithmeticTheorems | 0m02.59s || +0m00.06s 0m02.48s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.32s || +0m00.16s 0m02.36s | ModularArithmetic/ModularBaseSystemOpt | 0m02.35s || +0m00.00s 0m02.24s | Specific/FancyMachine256/Montgomery | 0m02.01s || +0m00.23s 0m02.14s | Specific/FancyMachine256/Barrett | 0m02.11s || +0m00.03s 0m01.89s | Specific/FancyMachine256/Core | 0m01.68s || +0m00.20s 0m01.86s | ModularArithmetic/Montgomery/ZBounded | 0m01.83s || +0m00.03s 0m01.55s | ModularArithmetic/BarrettReduction/Z | 0m01.50s || +0m00.05s 0m01.27s | ModularArithmetic/PrimeFieldTheorems | 0m01.36s || -0m00.09s 0m01.26s | BaseSystem | 0m01.35s || -0m00.09s 0m01.12s | ModularArithmetic/ExtendedBaseVector | 0m01.17s || -0m00.04s 0m00.92s | Util/NumTheoryUtil | 0m00.87s || +0m00.05s 0m00.89s | Experiments/EncodingLemmas | 0m00.84s || +0m00.05s 0m00.67s | Encoding/ModularWordEncodingTheorems | 0m00.64s || +0m00.03s 0m00.66s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.74s || -0m00.07s 0m00.64s | Spec/EdDSA | 0m00.58s || +0m00.06s 0m00.60s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.63s || -0m00.03s 0m00.60s | Encoding/ModularWordEncodingPre | 0m00.60s || +0m00.00s 0m00.60s | ModularArithmetic/ModularBaseSystem | 0m00.61s || -0m00.01s 0m00.59s | BoundedArithmetic/Interface | 0m00.62s || -0m00.03s 0m00.58s | ModularArithmetic/ModularBaseSystemList | 0m00.60s || -0m00.02s 0m00.56s | Spec/Ed25519 | 0m00.55s || +0m00.01s 0m00.55s | Spec/ModularWordEncoding | 0m00.59s || -0m00.03s 0m00.54s | BoundedArithmetic/StripCF | 0m00.44s || +0m00.10s 0m00.52s | ModularArithmetic/ZBounded | 0m00.44s || +0m00.08s 0m00.49s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.37s || +0m00.12s 0m00.48s | BoundedArithmetic/DoubleBounded | 0m00.53s || -0m00.05s 0m00.47s | ModularArithmetic/Pre | 0m00.47s || +0m00.00s 0m00.46s | BoundedArithmetic/ArchitectureToZLike | 0m00.50s || -0m00.03s 0m00.43s | ModularArithmetic/Pow2Base | 0m00.44s || -0m00.01s 0m00.42s | Spec/ModularArithmetic | 0m00.38s || +0m00.03s 0m00.38s | ModularArithmetic/Montgomery/Z | 0m00.46s || -0m00.08s
* Weaken hyps of lor_range, add it to zarithGravatar Jason Gross2016-10-07
|
* Moved lemma to ZUtil and added an extra lemma jgross neededGravatar jadep2016-10-06
|
* Add testbit_add_shiftl_fullGravatar Jason Gross2016-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 5m41.93s | Total | 5m42.43s || -0m00.50s ---------------------------------------------------------------------------------- 1m34.78s | Test/Curve25519SpecTestVectors | 1m34.04s || +0m00.74s 0m34.74s | ModularArithmetic/Conversion | 0m35.23s || -0m00.48s 0m27.39s | ModularArithmetic/ModularBaseSystemProofs | 0m27.12s || +0m00.26s 0m21.67s | ModularArithmetic/Pow2BaseProofs | 0m21.30s || +0m00.37s 0m20.51s | BoundedArithmetic/DoubleBoundedProofs | 0m20.75s || -0m00.23s 0m19.42s | EdDSARepChange | 0m19.76s || -0m00.33s 0m14.36s | Specific/GF25519 | 0m14.30s || +0m00.05s 0m12.32s | Util/ZUtil | 0m12.23s || +0m00.08s 0m09.36s | Testbit | 0m09.15s || +0m00.20s 0m08.41s | ModularArithmetic/Montgomery/ZProofs | 0m08.39s || +0m00.01s 0m08.35s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.48s || -0m00.13s 0m08.05s | Encoding/PointEncoding | 0m08.02s || +0m00.03s 0m07.51s | Specific/GF1305 | 0m07.54s || -0m00.03s 0m03.86s | BaseSystemProofs | 0m03.84s || +0m00.02s 0m03.57s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.69s || -0m00.12s 0m03.46s | ModularArithmetic/ModularBaseSystemListProofs | 0m03.47s || -0m00.01s 0m03.44s | ModularArithmetic/Tutorial | 0m03.59s || -0m00.14s 0m03.26s | BoundedArithmetic/InterfaceProofs | 0m03.16s || +0m00.09s 0m02.87s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.87s || +0m00.00s 0m02.80s | Encoding/PointEncodingPre | 0m02.94s || -0m00.14s 0m02.53s | ModularArithmetic/ModularArithmeticTheorems | 0m02.58s || -0m00.05s 0m02.25s | ModularArithmetic/ModularBaseSystemOpt | 0m02.28s || -0m00.02s 0m02.24s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.29s || -0m00.04s 0m02.07s | Specific/FancyMachine256/Montgomery | 0m02.22s || -0m00.15s 0m02.02s | Specific/FancyMachine256/Barrett | 0m02.16s || -0m00.14s 0m01.83s | ModularArithmetic/Montgomery/ZBounded | 0m01.74s || +0m00.09s 0m01.66s | Specific/FancyMachine256/Core | 0m01.73s || -0m00.07s 0m01.48s | ModularArithmetic/BarrettReduction/Z | 0m01.40s || +0m00.08s 0m01.28s | BaseSystem | 0m01.20s || +0m00.08s 0m01.27s | ModularArithmetic/PrimeFieldTheorems | 0m01.56s || -0m00.29s 0m01.16s | ModularArithmetic/ExtendedBaseVector | 0m01.19s || -0m00.03s 0m00.95s | Util/NumTheoryUtil | 0m00.91s || +0m00.03s 0m00.87s | Experiments/EncodingLemmas | 0m00.96s || -0m00.08s 0m00.70s | ModularArithmetic/ModularBaseSystem | 0m00.62s || +0m00.07s 0m00.67s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.66s || +0m00.01s 0m00.65s | BoundedArithmetic/Interface | 0m00.64s || +0m00.01s 0m00.64s | Encoding/ModularWordEncodingPre | 0m00.62s || +0m00.02s 0m00.64s | Spec/EdDSA | 0m00.70s || -0m00.05s 0m00.61s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.60s || +0m00.01s 0m00.61s | Encoding/ModularWordEncodingTheorems | 0m00.63s || -0m00.02s 0m00.56s | Spec/ModularWordEncoding | 0m00.56s || +0m00.00s 0m00.56s | ModularArithmetic/ModularBaseSystemList | 0m00.62s || -0m00.05s 0m00.52s | BoundedArithmetic/DoubleBounded | 0m00.43s || +0m00.09s 0m00.52s | ModularArithmetic/ZBounded | 0m00.58s || -0m00.05s 0m00.51s | BoundedArithmetic/ArchitectureToZLike | 0m00.45s || +0m00.06s 0m00.50s | Spec/Ed25519 | 0m00.56s || -0m00.06s 0m00.47s | BoundedArithmetic/StripCF | 0m00.46s || +0m00.00s 0m00.45s | ModularArithmetic/Pre | 0m00.67s || -0m00.22s 0m00.43s | ModularArithmetic/Pow2Base | 0m00.44s || -0m00.01s 0m00.42s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.36s || +0m00.06s 0m00.39s | ModularArithmetic/Montgomery/Z | 0m00.38s || +0m00.01s 0m00.34s | Spec/ModularArithmetic | 0m00.36s || -0m00.01s
* Use zutil_arith for side-conditions in testbitGravatar Jason Gross2016-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 5m41.34s | Total | 5m28.96s || +0m12.37s ---------------------------------------------------------------------------------- 0m34.92s | ModularArithmetic/Conversion | 0m27.15s || +0m07.77s 0m21.11s | ModularArithmetic/Pow2BaseProofs | 0m17.88s || +0m03.23s 1m34.77s | Test/Curve25519SpecTestVectors | 1m34.49s || +0m00.28s 0m27.17s | ModularArithmetic/ModularBaseSystemProofs | 0m27.52s || -0m00.34s 0m20.47s | BoundedArithmetic/DoubleBoundedProofs | 0m20.08s || +0m00.39s 0m19.56s | EdDSARepChange | 0m19.80s || -0m00.24s 0m14.35s | Specific/GF25519 | 0m14.58s || -0m00.23s 0m12.27s | Util/ZUtil | 0m12.18s || +0m00.08s 0m09.02s | Testbit | 0m08.96s || +0m00.05s 0m08.56s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.26s || +0m00.30s 0m08.18s | ModularArithmetic/Montgomery/ZProofs | 0m08.12s || +0m00.06s 0m07.96s | Encoding/PointEncoding | 0m08.14s || -0m00.18s 0m07.42s | Specific/GF1305 | 0m07.54s || -0m00.12s 0m03.83s | BaseSystemProofs | 0m03.83s || +0m00.00s 0m03.50s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.60s || -0m00.10s 0m03.46s | ModularArithmetic/ModularBaseSystemListProofs | 0m02.88s || +0m00.58s 0m03.44s | ModularArithmetic/Tutorial | 0m03.33s || +0m00.10s 0m03.23s | BoundedArithmetic/InterfaceProofs | 0m03.24s || -0m00.01s 0m02.90s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.86s || +0m00.04s 0m02.86s | Encoding/PointEncodingPre | 0m02.82s || +0m00.04s 0m02.58s | ModularArithmetic/ModularArithmeticTheorems | 0m02.55s || +0m00.03s 0m02.33s | ModularArithmetic/ModularBaseSystemOpt | 0m02.33s || +0m00.00s 0m02.31s | Specific/FancyMachine256/Montgomery | 0m02.08s || +0m00.23s 0m02.26s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.16s || +0m00.09s 0m02.10s | Specific/FancyMachine256/Barrett | 0m02.12s || -0m00.02s 0m01.82s | ModularArithmetic/Montgomery/ZBounded | 0m01.88s || -0m00.05s 0m01.69s | Specific/FancyMachine256/Core | 0m01.68s || +0m00.01s 0m01.47s | ModularArithmetic/BarrettReduction/Z | 0m01.44s || +0m00.03s 0m01.27s | ModularArithmetic/PrimeFieldTheorems | 0m01.31s || -0m00.04s 0m01.25s | BaseSystem | 0m01.31s || -0m00.06s 0m01.12s | ModularArithmetic/ExtendedBaseVector | 0m01.10s || +0m00.02s 0m00.98s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.67s || +0m00.30s 0m00.94s | Experiments/EncodingLemmas | 0m00.88s || +0m00.05s 0m00.91s | Util/NumTheoryUtil | 0m00.80s || +0m00.10s 0m00.67s | Spec/EdDSA | 0m00.65s || +0m00.02s 0m00.64s | Encoding/ModularWordEncodingTheorems | 0m00.61s || +0m00.03s 0m00.62s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.60s || +0m00.02s 0m00.62s | ModularArithmetic/ModularBaseSystem | 0m00.62s || +0m00.00s 0m00.59s | Encoding/ModularWordEncodingPre | 0m00.59s || +0m00.00s 0m00.59s | ModularArithmetic/ModularBaseSystemList | 0m00.67s || -0m00.08s 0m00.56s | BoundedArithmetic/Interface | 0m00.61s || -0m00.04s 0m00.56s | Spec/Ed25519 | 0m00.48s || +0m00.08s 0m00.55s | Spec/ModularWordEncoding | 0m00.60s || -0m00.04s 0m00.50s | BoundedArithmetic/DoubleBounded | 0m00.49s || +0m00.01s 0m00.50s | ModularArithmetic/ZBounded | 0m00.49s || +0m00.01s 0m00.48s | ModularArithmetic/Pow2Base | 0m00.50s || -0m00.02s 0m00.47s | ModularArithmetic/Pre | 0m00.45s || +0m00.01s 0m00.47s | BoundedArithmetic/StripCF | 0m00.42s || +0m00.04s 0m00.44s | BoundedArithmetic/ArchitectureToZLike | 0m00.42s || +0m00.02s 0m00.36s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.37s || -0m00.01s 0m00.36s | ModularArithmetic/Montgomery/Z | 0m00.46s || -0m00.10s 0m00.35s | Spec/ModularArithmetic | 0m00.36s || -0m00.01s
* Add Z.pow_le_mono_{r,l} to zarithGravatar Jason Gross2016-10-06
|
* Add a lemma to Ztestbit about large indicesGravatar Jason Gross2016-10-06
|
* More zsimplify lemmasGravatar Jason Gross2016-10-04
|
* Add Zplus_minus to zsimplifyGravatar Jason Gross2016-10-04
|
* Weaken hyps of zutil lemmaGravatar Jason Gross2016-10-04
|
* Add a variant of add_shift_modGravatar Jason Gross2016-10-04
|
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
|
* Add ZUtil lemmaGravatar Jason Gross2016-10-04
|
* Add Zmult_lt_compat_r to zarithGravatar Jason Gross2016-10-04
|
* Prevent infinite loops by not dealing with 0 mod _Gravatar Jason Gross2016-10-04
|
* Handle 0 mod _ in push_ZmodGravatar Jason Gross2016-10-04
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 04:25:15 +0000