aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
Commit message (Collapse)AuthorAge
* PrimeFieldTheorems: inv for isomorphic fieldsGravatar Andres Erbsen2017-03-02
|
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
|
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
|
* Handle more kinds of ops in fixed_size_op_to_wordGravatar Jason Gross2017-02-03
|
* Only unfold the non-zpecialized versions of wcmovl, wcmovne, wnegGravatar Jason Gross2017-02-03
| | | | The specialized versions don't match with the generic version; they'll need special behavior
* Also unfold wcmovl, wcmovne, wneg in fixed_size_constantsGravatar Jason Gross2017-02-03
|
* Better word operationsGravatar Jason Gross2017-01-03
|
* Add word versions of ModularBaseSystemListZOperationsGravatar Jason Gross2017-01-03
|
* Update bounds things with prefreezeGravatar Jason Gross2016-11-14
|
* Proper_sqrt_3mod4 Proper_sqrt_5mod8Gravatar Andres Erbsen2016-11-13
|
* Define word version of conditional subtractionGravatar jadep2016-11-11
|
* separate freeze into two partsGravatar jadep2016-11-11
|
* Remove special code for reified conditional subGravatar Jason Gross2016-11-11
|
* Silence a warning about name collisionGravatar Jason Gross2016-11-09
|
* Prove things in ModularBaseSystemListZOperationsProofsGravatar Jason Gross2016-11-08
|
* Factor related_Z_op (except conditional_sub)Gravatar Jason Gross2016-11-08
|
* Preliminary support: conditional sub as primitiveGravatar Jason Gross2016-11-06
| | | | | | | | | | | | | | | | | | | | | | | Things to be done: - Fill in Axiom conditional_subtract_modulus in src/ModularArithmetic/ModularBaseSystemListZOperations.v (jadep) - Refactor code to make GF25519.freeze use ModularBaseSystemListZOperations.conditional_subtract_modulus in a non-unfolded form (jadep) - Check that the bounds I defined in conditional_subtract' in src/Reflection/Z/Interpretations.v are correct (jadep) - Fill in bounds checking in conditional_subtract_o in src/Reflection/Z/Interpretations.v (jgross or jadep) - Integrate boundedness lemma about conditional_subtract_modulus into BoundedWord64.conditional_subtract in src/Reflection/Z/Interpretations.v (jadep and jgross?) - Prove BoundedWord64.invert_conditional_subtract (depends on some bits of the above bullet point, but could be done by jgross) - Fill in the three admits in src/Reflection/Z/Interpretations/Relations.v (jadep or jgross?) - Verify that everything works (cc @jadephilipoom @andres-erbsen)
* Fix 8.4 build partiallyGravatar Jason Gross2016-11-03
|
* Make [freeze] proofs consider machine integer width and hard input bounds ↵Gravatar jadep2016-11-03
| | | | separately
* Lift conversion correctness proofs to ModularBaseSystem by providing ↵Gravatar jadep2016-11-02
| | | | [pack_rep] and [unpack_rep] lemmas
* Changes to sqrt for easier bounds proofs; currently blocked on broken proof ↵Gravatar jadep2016-11-02
| | | | in GF25519Bounded
* Progress proving ERepDec_correct (included tweaking preconditions for ↵Gravatar jadep2016-11-02
| | | | ModularBaseSystem sqrt_5mod8 proofs)
* remove commented-out lemmaGravatar jadep2016-10-30
|
* revived accidentally deleted lemmaGravatar jadep2016-10-30
|
* proved feSign_correctGravatar jadep2016-10-29
|
* prove testbit_sub_pow2Gravatar Andres Erbsen2016-10-29
|
* prove admit about F.to_nat x mod mGravatar Andres Erbsen2016-10-27
|
* Fix a missing import in previous commitGravatar Jason Gross2016-10-27
|
* Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
| | | | This way we will have a faster build of reification things
* Slightly loosen freeze preconditions (in particular, I had failed to ↵Gravatar jadep2016-10-27
| | | | properly account for the case when which [n] and [pred n] are BOTH out of bounds in my statement of initial bounds)
* add extra convenience lemmas about boundedness of convertGravatar jadep2016-10-27
|
* Created separate definitions for cmovne and cmovl for reificationGravatar jadep2016-10-23
|
* final touches/fixes for freeze restructuringGravatar jadep2016-10-22
|
* Modified [freeze] to be more reifyableGravatar jadep2016-10-22
|
* Removed the lingering TODO and print statement that @JasonGross helpfully ↵Gravatar jadep2016-10-19
| | | | pointed out
* Fill in admits for field with carry_add, carry_opp, and carry_subGravatar jadep2016-10-19
|
* Define carry_opp in terms of carry_subGravatar Jason Gross2016-10-19
|
* Add opt versions of add, sub, oppGravatar Jason Gross2016-10-19
|
* Fix a proofGravatar Jason Gross2016-10-16
|
* Don't inline as much in ZBoundedZGravatar Jason Gross2016-10-16
|
* Add Z as ZBoundedGravatar Jason Gross2016-10-16
|
* Added top-level modulus comparison operation so field-element decoding can ↵Gravatar jadep2016-10-12
| | | | return None if input is greater than modulus
* Bundle arguments to Barrett ReductionGravatar Jason Gross2016-10-10
|
* Fix compatibility with sigT notationGravatar Jason Gross2016-10-10
|
* 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
* Moved lemma to ZUtil and added an extra lemma jgross neededGravatar jadep2016-10-06
|
* Moved conversion logic out of Pow2BaseProofs into its own fileGravatar jadep2016-10-06
|
* map -> List.map (not Tuple.map)Gravatar Jason Gross2016-09-29
|
* Merge pull request #69 from JasonGross/scalable-scalarsGravatar Jason Gross2016-09-26
|\ | | | | Scalable Scalars, Dead Code Removal, Register Assignment
* | Finished remaining admits in [freeze] proofsGravatar jadep2016-09-23
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 04:07:40 +0000