aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ModularBaseSystem.v
Commit message (Collapse)AuthorAge
* Put ModularBaseSystem carries in terms of [carry_gen], and pushed this ↵Gravatar jadep2016-07-25
| | | | change through the pipeline. Also began the process of redoing canonicalization proofs, attempting to put the messy case analysis in theorem statements rather than separate lemmas.
* restructured ModularBaseSystem pipeline to put tuple conversion before ↵Gravatar jadep2016-07-20
| | | | ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt
* Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.Gravatar jadep2016-07-19
|
* Move some definitions to Pow2Base (#24)Gravatar Jason Gross2016-07-18
| | | | | | | | | * Move some definitions to Pow2Base These definitions don't depend on PseudoMersenneBaseParams, only on limb_widths, and we'll want them for BarrettReduction / P256. * Fix for Coq 8.4
* pushing through a tweak to the arguments of [sub], and defining a field over ↵Gravatar jadep2016-07-12
| | | | ModularBaseSystemInterface using some placeholder operations.
* Make [base] and [log_cap] notationsGravatar Jason Gross2016-07-11
| | | | | | | | Also use [ZUtil.Z.pow2_mod]. This lets us remove the dependency of ModularBaseSystem on ModularArithmetic.PseudoMersenneBaseParamProofs. This is a small part of reorganizing and factoring ModularBaseSystem for use with Barrett reduction.
* Factored out some proofs that rely only on base being powers of two, and ↵Gravatar jadep2016-07-06
| | | | defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.
* encode operation in ModularBaseSystem now uses bitwise operators, taking ↵Gravatar jadep2016-06-29
| | | | advantage of the fact that base elements are required to be powers of 2
* BaseSystem encode function is no longer naive; it does a mod/div loop rather ↵Gravatar jadep2016-06-28
| | | | than sticking the value of the Z input in the first digit. The condition that c is positive has been added to PseudoMersenneBaseParams--it is necessary for this encode and for canonicalization, for which it was previously a section variable.
* Aggregate all level specifications not in Spec/*Gravatar Jason Gross2016-06-22
| | | | | This prevents notation conflicts (see comment in Notations.v for more explanation).
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
|
* PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵Gravatar jadep2016-06-15
| | | | base-length digit vectors)
* changed representation definition to require digits vector to be the exact ↵Gravatar jadep2016-06-15
| | | | length of the base vector
* Added canonicalization to ModularBaseSystemOpt.Gravatar jadep2016-06-15
|
* reversed modulus_digits and proved a few admitsGravatar jadep2016-06-13
|
* starting rewrite using different definition of mapGravatar jadep2016-06-11
|
* First stage of canonicalization proofs complete; proved 3 carry loops reduce ↵Gravatar jadep2016-05-20
| | | | input digits to their minimal widths. Remaining : name fixes and second stage -- proving that we subtract q iff the reduced input is over q (in the range [2^k-c, 2^k-1])
* Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ↵Gravatar jadep2016-05-09
| | | | unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want.
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-03-30
|\
* | made BaseVector instance globalGravatar Jade Philipoom2016-03-20
| |
* | refactor of Basesystem and ModularBaseSystem; includes general code ↵Gravatar Jade Philipoom2016-03-20
| | | | | | | | organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division
* | Refactored BaseSystem and ModularBaseSystem.Gravatar Jade Philipoom2016-03-11
| |
| * 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 ```
* Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 04:33:23 +0000