aboutsummaryrefslogtreecommitdiff
path: root/src/Util/NatUtil.v
Commit message (Collapse)AuthorAge
* Add some natutil and listutil lemmasGravatar Jason Gross2018-10-10
|
* Fix some issues in previous commitGravatar Jason Gross2018-07-30
|
* Add nat_rect_Proper_nondep_genGravatar Jason Gross2018-07-30
|
* Add more proper instancesGravatar Jason Gross2018-07-26
|
* Add minor lemmas to utilGravatar Jason Gross2018-07-17
|
* [Require NatUtil] should not change [tauto]Gravatar Jason Gross2017-06-19
| | | | | | | | | Work around [bug #5444](https://coq.inria.fr/bugs/show_bug.cgi?id=5444), [Require Nsatz] should not change the behavior of [tauto]. Because [tauto] is stupid and checks to see whether or not [Classical_Prop] has been *required* to decide whether or not to use classical axioms. Aren't side-effects of [Require] wonderful? Since we're not actually using nsatz or psatz in NatUtil, we now simply [Require Import Lia].
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
| | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
* Add transparent equality proofs for fixed wordTGravatar Jason Gross2017-01-21
| | | | Such a pain to make proofs compute
* Add nat_beq_to_eqGravatar Jason Gross2017-01-19
|
* Fix 8.4 build issueGravatar Jason Gross2016-10-23
|
* Prove an admitted NatUtil lemmaGravatar Jason Gross2016-10-23
|
* integrate bitwise operationsGravatar Andres Erbsen2016-10-12
|
* Equality for nat in natutilGravatar Jason Gross2016-09-16
|
* Add natutilGravatar Jason Gross2016-08-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------------------ 4m05.87s | Total | 3m55.03s || +0m10.84s ------------------------------------------------------------------------------------ 0m29.03s | ModularArithmetic/Pow2BaseProofs | 0m22.86s || +0m06.17s 0m42.14s | CompleteEdwardsCurve/ExtendedCoordinates | 0m37.78s || +0m04.35s 0m33.70s | Specific/GF25519 | 0m36.48s || -0m02.77s 0m18.10s | ModularArithmetic/ModularBaseSystemProofs | 0m16.95s || +0m01.15s 0m09.83s | ModularArithmetic/Montgomery/ZProofs | 0m08.72s || +0m01.10s 0m08.38s | Specific/GF1305 | 0m06.89s || +0m01.49s 0m04.00s | ModularArithmetic/ModularArithmeticTheorems | 0m02.62s || +0m01.37s 0m03.61s | ModularArithmetic/Tutorial | 0m05.40s || -0m01.79s 0m16.27s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.14s || +0m00.12s 0m13.68s | Experiments/SpecEd25519 | 0m13.66s || +0m00.01s 0m10.18s | Util/ZUtil | 0m09.70s || +0m00.48s 0m08.91s | Testbit | 0m09.14s || -0m00.23s 0m03.99s | BaseSystemProofs | 0m03.85s || +0m00.14s 0m03.96s | Util/ListUtil | 0m04.19s || -0m00.23s 0m03.60s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.59s || +0m00.01s 0m03.37s | Experiments/SpecificCurve25519 | 0m03.36s || +0m00.01s 0m02.90s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.90s || +0m00.00s 0m02.51s | Experiments/EdDSARefinement | 0m01.78s || +0m00.72s 0m02.28s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.35s || -0m00.07s 0m02.25s | ModularArithmetic/ModularBaseSystemOpt | 0m02.27s || -0m00.02s 0m01.58s | Util/Tuple | 0m01.63s || -0m00.04s 0m01.53s | Encoding/PointEncodingPre | 0m02.33s || -0m00.80s 0m01.47s | ModularArithmetic/BarrettReduction/Z | 0m01.54s || -0m00.07s 0m01.27s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.93s || +0m00.34s 0m01.19s | Util/NatUtil | 0m01.10s || +0m00.08s 0m01.19s | ModularArithmetic/ExtendedBaseVector | 0m01.18s || +0m00.01s 0m01.18s | BaseSystem | 0m01.20s || -0m00.02s 0m01.17s | ModularArithmetic/PrimeFieldTheorems | 0m01.04s || +0m00.12s 0m00.97s | Util/NumTheoryUtil | 0m00.86s || +0m00.10s 0m00.88s | Experiments/DerivationsOptionRectLetInEncoding | 0m00.94s || -0m00.05s 0m00.87s | ModularArithmetic/ModularBaseSystemField | 0m00.92s || -0m00.05s 0m00.84s | ModularArithmetic/Montgomery/ZBounded | 0m00.88s || -0m00.04s 0m00.78s | Spec/ModularWordEncoding | 0m00.68s || +0m00.09s 0m00.68s | Encoding/ModularWordEncodingTheorems | 0m00.75s || -0m00.06s 0m00.66s | Encoding/ModularWordEncodingPre | 0m00.79s || -0m00.13s 0m00.65s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.78s || -0m00.13s 0m00.65s | Util/AdditionChainExponentiation | 0m00.67s || -0m00.02s 0m00.65s | Spec/EdDSA | 0m00.92s || -0m00.27s 0m00.63s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.64s || -0m00.01s 0m00.62s | ModularArithmetic/ModularBaseSystemList | 0m00.64s || -0m00.02s 0m00.61s | ModularArithmetic/ModularBaseSystem | 0m00.60s || +0m00.01s 0m00.52s | ModularArithmetic/Pre | 0m00.49s || +0m00.03s 0m00.50s | Util/WordUtil | 0m00.62s || -0m00.12s 0m00.45s | ModularArithmetic/Pow2Base | 0m00.47s || -0m00.01s 0m00.44s | ModularArithmetic/ZBounded | 0m00.44s || +0m00.00s 0m00.42s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.39s || +0m00.02s 0m00.40s | ModularArithmetic/Montgomery/Z | 0m00.41s || -0m00.00s 0m00.38s | Spec/ModularArithmetic | 0m00.56s || -0m00.18s
* Convert defined and mostly proven, modulo several admitted lemmas about Z ↵Gravatar jadep2016-08-09
| | | | operations and a couple subroutines.
* Fix 8.4 build.Gravatar jadep2016-07-25
|
* A couple new util lemmasGravatar jadep2016-07-25
|
* Add another lemma about +, <= to arithGravatar Jason Gross2016-07-20
|
* Fix for Coq 8.4 (omega used to be weaker)Gravatar Jason Gross2016-07-18
|
* Add more natsimplify le_dec lemmasGravatar Jason Gross2016-07-18
|
* Add more NatUtil lemmasGravatar Jason Gross2016-07-18
|
* Add natsimplify lemmas about eq_nat_decGravatar Jason Gross2016-07-18
|
* Added lemmas to ZUtil and NatUtil (for Testbit)Gravatar jadep2016-07-18
|
* Fix NatUtil for 8.4Gravatar Jason Gross2016-07-08
|
* Add useful tactics and util lemmasGravatar Jason Gross2016-07-08
|
* Add a NatUtil lemma and dbGravatar Jason Gross2016-07-08
|
* Fix ListUtil for Coq 8.4Gravatar Jason Gross2016-07-07
|
* Add [update_nth] to ListUtil, change [set_nth]Gravatar Jason Gross2016-07-06
| | | | Define [set_nth] in terms of [update_nth]
* Prove that a ^ k <> 0Gravatar Jason Gross2016-06-30
|
* MergeGravatar jadep2016-06-14
|\
* | progress on second stage (conditional constant-time subtraction) of ↵Gravatar jadep2016-06-13
| | | | | | | | canonicalization proofs
| * 8.5 fixesGravatar Jason Gross2016-06-10
|/
* moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-04-20
|
* Finish absolutizing importsGravatar Jason Gross2016-03-10
| | | | | | | | | | | | The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
* Factor out some bedrock dependencies into WordUtilGravatar Jason Gross2016-02-25
| | | | Also move a definition about words, with a TODO about location, into WordUtil.
* a few lemmas in util about powers of 2 in Bedrock's various rewritten formsGravatar Jade Philipoom2016-02-15
|
* Util: added util lemmas needed to instantiate EdDSA25519.Gravatar Jade Philipoom2016-01-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 05:42:32 +0000