diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-06 18:52:20 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-07 18:56:03 -0400 |
| commit | c87d67809851682bbc404546c1cc7d9f3c457840 (patch) | |
| tree | 29b75c5c614e474ae633a42794f9b48379a8b752 /src/BoundedArithmetic/ArchitectureToZLikeProofs.v | |
| parent | 9e67aab9d86311a2faa21781b3e208b169e184f2 (diff) | |
Split up DoubleBoundedProofs, add proofs
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
Diffstat (limited to 'src/BoundedArithmetic/ArchitectureToZLikeProofs.v')
| -rw-r--r-- | src/BoundedArithmetic/ArchitectureToZLikeProofs.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v b/src/BoundedArithmetic/ArchitectureToZLikeProofs.v index 00ab82ea2..a816d8ebd 100644 --- a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v +++ b/src/BoundedArithmetic/ArchitectureToZLikeProofs.v @@ -2,8 +2,9 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.BoundedArithmetic.Interface. Require Import Crypto.BoundedArithmetic.InterfaceProofs. -Require Import Crypto.BoundedArithmetic.DoubleBounded. -Require Import Crypto.BoundedArithmetic.DoubleBoundedProofs. +Require Import Crypto.BoundedArithmetic.Double.Core. +Require Import Crypto.BoundedArithmetic.Double.Proofs.RippleCarryAddSub. +Require Import Crypto.BoundedArithmetic.Double.Proofs.Multiply. Require Import Crypto.BoundedArithmetic.ArchitectureToZLike. Require Import Crypto.ModularArithmetic.ZBounded. Require Import Crypto.Util.Tuple. |