diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-09 23:50:20 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-09 23:53:31 -0400 |
| commit | 02b75805f7f4355ce32b5322377b83852e5f0b05 (patch) | |
| tree | 6aecd0ca068026e66a55597da08848bff2a1a23b /_CoqProject | |
| parent | 9daf921fe206fa0fb0f7d88e406096fa00c6051e (diff) | |
Add shl,shr,shrd to repeated doubling
After | File Name | Before || Change
---------------------------------------------------------------------------------------------------------
0m03.99s | Total | 0m03.08s || +0m00.90s
---------------------------------------------------------------------------------------------------------
0m01.14s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.02s || +0m00.11s
0m00.52s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.53s || -0m00.01s
0m00.51s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.51s || +0m00.00s
0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | N/A || +0m00.47s
0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.54s || -0m00.08s
0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight | N/A || +0m00.46s
0m00.44s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.49s || -0m00.04s
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 27d5a040b..ab6c0fb42 100644 --- a/_CoqProject +++ b/_CoqProject @@ -47,6 +47,8 @@ src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v +src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v +src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v |