diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-06 18:52:20 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-09 22:49:36 -0400 |
| commit | 9daf921fe206fa0fb0f7d88e406096fa00c6051e (patch) | |
| tree | 8aa0f0faa2c5bb5319245603d4dfc1f1c7b246a0 /_CoqProject | |
| parent | 3e7ef06ef6d9beb00b22a66c1bc3368dbe455c06 (diff) | |
Add proofs for doubling shl,shr,shrd
After | File Name | Before || Change
------------------------------------------------------------------------------------------------
0m14.81s | Total | 0m00.00s || +0m14.81s
------------------------------------------------------------------------------------------------
0m08.87s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | N/A || +0m08.86s
0m02.82s | BoundedArithmetic/Double/Proofs/ShiftLeft | N/A || +0m02.81s
0m02.72s | BoundedArithmetic/Double/Proofs/ShiftRight | N/A || +0m02.72s
0m00.40s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic | N/A || +0m00.40s
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 5f348b3ee..27d5a040b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -36,6 +36,10 @@ src/BoundedArithmetic/Double/Proofs/LoadImmediate.v src/BoundedArithmetic/Double/Proofs/Multiply.v src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v src/BoundedArithmetic/Double/Proofs/SelectConditional.v +src/BoundedArithmetic/Double/Proofs/ShiftLeft.v +src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v +src/BoundedArithmetic/Double/Proofs/ShiftRight.v +src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v src/BoundedArithmetic/Double/Repeated/Core.v src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v |