| Commit message (Collapse) | Author | Age |
|
|
|
| |
This way they won't become ambiguous if we add new files
|
|\ |
|
| | |
|
|/
|
|
| |
(BaseSystem.decode _ _)
|
|
|
|
| |
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.
|
|
|
|
| |
not perform reduction
|
|
|
|
| |
organization of reasoning.
|
|
|
|
|
|
| |
It leads to a slightly more transparent and clearer definition.
If I got everything right, nothing should depend on the judgmental
definition of [add_to_nth] anymore.
|
|
|
|
|
|
| |
Also make much of the remaining code outside of Pow2BaseProofs
independent of the precise definition of carry_simple. (We use [Local
Opaque] to enforce this modularity.
|
|
|
|
|
|
|
|
|
| |
* 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
|
|
|
|
|
|
|
|
| |
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.
|