| Commit message (Collapse) | Author | Age |
|
|
|
| |
cleaning up freeze-related organization and definitions along the way
|
| |
|
| |
|
|
|
|
| |
actually is a multiple of the modulus. This allows for proving the Proper properties of [sub] based on its correctness proof alone, which has the modulus multiple correctness as a precondition.
|
|
|
|
| |
implementation, and pushed that up through Specific.
|
|
|
|
| |
placeholders, and proved their correctness. In the process, reorganized early parts of ModularBaseSystemProofs.v by moving some lemmas to PseudoMersenneBaseParamProofs.v and introducing lemmas about the algebraic properties of ModularBaseSystem operations.
|
|
|
|
| |
widths in ModularBaseSystem
|
|
|
|
| |
Specific.
|
|
|
|
|
|
| |
[ZToField] -> [F.of_Z]
[FieldToZ] -> [F.to_Z]
[Zmod.lem] -> [F.lem]
|
|
|
|
|
|
|
|
|
|
|
|
| |
ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.
Backwards-incompatible changes:
F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1
|
|
|
|
| |
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.
|
|
|
|
| |
ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt
|
| |
|
|
|
|
|
|
|
|
|
| |
* 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
|
|
|
|
| |
ModularBaseSystemInterface using some placeholder operations.
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
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.
|
|
|
|
| |
advantage of the fact that base elements are required to be powers of 2
|
|
|
|
| |
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.
|
|
|
|
|
| |
This prevents notation conflicts (see comment in Notations.v for more
explanation).
|
| |
|
|
|
|
| |
base-length digit vectors)
|
|
|
|
| |
length of the base vector
|
| |
|
| |
|
| |
|
|
|
|
| |
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])
|
|
|
|
| |
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.
|
|\ |
|
| | |
|
| |
| |
| |
| | |
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
|
| | |
|
|/
|
|
|
|
|
|
|
|
|
|
| |
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
```
|
|
|