| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
return None if input is greater than modulus
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Some help from jadep on BitwiseOr.
After | File Name | Before || Change
--------------------------------------------------------------------------------------
0m39.26s | Total | 0m36.03s || +0m03.23s
--------------------------------------------------------------------------------------
N/A | BoundedArithmetic/DoubleBoundedProofs | 0m21.20s || -0m21.19s
0m07.47s | BoundedArithmetic/Double/Proofs/Multiply | N/A || +0m07.46s
0m06.70s | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate | N/A || +0m06.70s
0m05.14s | BoundedArithmetic/Double/Proofs/RippleCarryAddSub | N/A || +0m05.13s
0m02.75s | BoundedArithmetic/Double/Proofs/Decode | N/A || +0m02.75s
0m08.06s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.05s || +0m00.00s
0m02.01s | Specific/FancyMachine256/Barrett | 0m02.13s || -0m00.12s
0m02.00s | Specific/FancyMachine256/Montgomery | 0m02.06s || -0m00.06s
0m01.75s | Specific/FancyMachine256/Core | 0m01.66s || +0m00.09s
0m00.90s | BoundedArithmetic/Double/Proofs/LoadImmediate | N/A || +0m00.90s
0m00.88s | BoundedArithmetic/Double/Proofs/BitwiseOr | N/A || +0m00.88s
0m00.58s | BoundedArithmetic/Double/Proofs/SelectConditional | N/A || +0m00.57s
0m00.53s | BoundedArithmetic/ArchitectureToZLike | 0m00.47s || +0m00.06s
0m00.49s | BoundedArithmetic/Double/Core | N/A || +0m00.49s
N/A | BoundedArithmetic/DoubleBounded | 0m00.46s || -0m00.46s
|
| |
|
| |
|
| |
|
|
|
|
|
| |
By being careful about building the expressions in the first place, we
no longer need it, and can rely on dead code elimination.
|
| |
|
|
|
|
|
|
| |
We still use CSE in fancy machine, because we want to lift the ldi's
above the rest of the code. However, on a quick inspection, the
algorithm no longer needs CSE to be duplicate-free.
|
| |
|
|
|
|
|
| |
We reserve [a # b] in Notations.v, and make it's level compatible with
the notation declared in the std lib for Q.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Quoting Andres:
> I am leaning towards putting this in Specifc instead of Experiments -- it
> seems like complete result on its own, these files are unlikely to be reused
> for something else, and I don't think we are expecting to need to remove it
> any time soon. Currently, `Specific` code does not quantify over anything (no
> context variables), but this seems secondary. We could make versions of this
> with the curve constants plugged in, though.
|
| |
|
| |
|
|
|
|
| |
cleaning up freeze-related organization and definitions along the way
|
| |
|
|
|
|
| |
for instantiating it in GF25519 (needed for equality comparison in sqrt_5mod8)
|
|
|
|
| |
implementation, and pushed that up through Specific.
|
|
|
|
| |
ModularBaseSystemField.v
|
|
|
|
| |
field proof through GF1305.v as a proof of concept; working towards deleting that ModularBaseSystemField.v
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change
-----------------------------------------------------------------
0m13.37s | Total | 0m40.29s || -0m26.91s
-----------------------------------------------------------------
0m10.09s | Specific/GF25519 | 0m37.00s || -0m26.91s
0m03.29s | Experiments/SpecificCurve25519 | 0m03.30s || -0m00.00s
|
| |
|
| |
|
|\ |
|
|/ |
|
|
|
|
| |
Specific.
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
| |
organization of reasoning.
|
|
|
|
| |
ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt
|
|
|
|
| |
the zsimplify step; after inserting clauses, we can't rewrite under the binders, but we can do the rewrite and insertions in different definitions.
|
| |
|
| |
|
|
|
|
| |
proved that GF1305 is a field
|
|
|
|
| |
ModularBaseSystemInterface using some placeholder operations.
|
| |
|
|
|
|
| |
terms of isomorphism to ModularArithmetic.F), proved lemma about tuple-based [mul] based on the goals generated by the group constructor
|
| |
|
|
|
|
|
| |
This prevents notation conflicts (see comment in Notations.v for more
explanation).
|
| |
|
| |
|
|\
| |
| |
| | |
includes broken files to be removed in next commit
|
| | |
|
| | |
|
| |
| |
| |
| | |
base-length digit vectors)
|
| | |
|
| |
| |
| |
| |
| | |
This is https://coq.inria.fr/bugs/show_bug.cgi?id=4811, [f_equal]
loops(?) in 8.5pl1 (fixed already in 8.5.dev)
|
| | |
|