aboutsummaryrefslogtreecommitdiff
path: root/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
Commit message (Collapse)AuthorAge
* Split up DoubleBoundedProofs, add proofsGravatar Jason Gross2016-10-07
| | | | | | | | | | | | | | | | | | | | | | | | 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
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-10-03
|
* Drop CSE from Fancy MachineGravatar Jason Gross2016-09-22
| | | | | By being careful about building the expressions in the first place, we no longer need it, and can rely on dead code elimination.
* Use dlet, not lletGravatar Jason Gross2016-09-22
|
* Don't inline everything in Montgomery and BarrettGravatar Jason Gross2016-09-22
| | | | | | 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.
* Integrate suggestions from AndresGravatar Jason Gross2016-08-25
|
* Rework bounded proofsGravatar Jason Gross2016-08-24
| | | | | | | | | | Now the rewrite strategy no longer relies on projections of anything other than [decode], and the conversion to ZLike is simpler. Modulo some annoyingly delicate arithmetic around things like [2^n * 2^n = 2^(2*n)] and whether to factor [(decode (fst x) + decode (snd x) >> n) >> b] as [decode x >> n] or as [shrd (fst x) (snd x) n], the proofs bascially go by pulling/pushing decodes.
* Weaken the condition on smaller_boundGravatar Jason Gross2016-08-23
|
* Hook up the bounded interface, finish proofsGravatar Jason Gross2016-08-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 04:15:00 +0000