aboutsummaryrefslogtreecommitdiff
path: root/src/BoundedArithmetic
Commit message (Collapse)AuthorAge
* Actually fix the exponential blowup (hopefully)Gravatar Jason Gross2016-10-14
| | | | | This is a case where a variable was used in two places, and thus duplicated. Not sure if the other cases actually trigger.
* Fix a typo in the previous commitGravatar Jason Gross2016-10-14
|
* Fix exponential blowup in some doubling opsGravatar Jason Gross2016-10-14
| | | | Thanks @andres-erbsen !
* Work around bug 5401 (bad let '(x, y))Gravatar Jason Gross2016-10-13
| | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5140, destructuring let under binders of a class with an argument gives "Anomaly: index to an anonymous variable. Please report at http://coq.inria.fr/bugs/."
* Revert "Eta-expand pairs in Eta.v"Gravatar Jason Gross2016-10-13
| | | | | | | | | This reverts commit 778c1906711f68bed5760710712bb16eeb9c2365. It's not particularly useful, I think, and might be counterproductive; most of the unfolded pair projections in x86 are applied to variables, not instructions, and some instructions don't have pair projections directly applied to them.
* Eta-expand pairs in Eta.vGravatar Jason Gross2016-10-13
|
* Unfold more things in etaGravatar Jason Gross2016-10-13
|
* Add src/BoundedArithmetic/Eta.vGravatar Jason Gross2016-10-13
|
* Fix for missing Nat.log2 in 8.4Gravatar Jason Gross2016-10-11
|
* Fix for missing Nat.log2 in 8.4Gravatar Jason Gross2016-10-11
|
* Add some admitted x86->ZLike proofsGravatar Jason Gross2016-10-10
|
* Work around bug 5003 (broken omega on projections)Gravatar Jason Gross2016-10-10
| | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5003, [xlia] ([lia], [nia]) constructs ill typed terms when projections from records are involved.
* Add definitions for x86Gravatar Jason Gross2016-10-10
| | | | | | | | After | File Name | Before || Change --------------------------------------------------------------- 0m00.48s | Total | 0m00.62s || -0m00.14s --------------------------------------------------------------- 0m00.48s | BoundedArithmetic/X86ToZLike | 0m00.62s || -0m00.14s
* Add repeated multipleGravatar Jason Gross2016-10-10
| | | | | | | | | | | | | | After | File Name | Before || Change --------------------------------------------------------------------------------------------------------- 0m04.24s | Total | 0m04.12s || +0m00.12s --------------------------------------------------------------------------------------------------------- 0m01.01s | BoundedArithmetic/Double/Repeated/Proofs/Decode | 0m01.03s || -0m00.02s 0m00.58s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub | 0m00.56s || +0m00.01s 0m00.56s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr | 0m00.54s || +0m00.02s 0m00.56s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate | 0m00.50s || +0m00.06s 0m00.55s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional | 0m00.56s || -0m00.01s 0m00.50s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.46s || +0m00.03s 0m00.48s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight | 0m00.47s || +0m00.01s
* Add shl,shr,shrd to repeated doublingGravatar Jason Gross2016-10-09
| | | | | | | | | | | | | | 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
* Add proofs for doubling shl,shr,shrdGravatar Jason Gross2016-10-09
| | | | | | | | | | | 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
* Some work on x86 and bounded repeated thingsGravatar Jason Gross2016-10-09
|
* Add some bounded decode/and thingsGravatar Jason Gross2016-10-09
|
* 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
* Add testbit_add_shiftl_fullGravatar Jason Gross2016-10-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ---------------------------------------------------------------------------------- 5m41.93s | Total | 5m42.43s || -0m00.50s ---------------------------------------------------------------------------------- 1m34.78s | Test/Curve25519SpecTestVectors | 1m34.04s || +0m00.74s 0m34.74s | ModularArithmetic/Conversion | 0m35.23s || -0m00.48s 0m27.39s | ModularArithmetic/ModularBaseSystemProofs | 0m27.12s || +0m00.26s 0m21.67s | ModularArithmetic/Pow2BaseProofs | 0m21.30s || +0m00.37s 0m20.51s | BoundedArithmetic/DoubleBoundedProofs | 0m20.75s || -0m00.23s 0m19.42s | EdDSARepChange | 0m19.76s || -0m00.33s 0m14.36s | Specific/GF25519 | 0m14.30s || +0m00.05s 0m12.32s | Util/ZUtil | 0m12.23s || +0m00.08s 0m09.36s | Testbit | 0m09.15s || +0m00.20s 0m08.41s | ModularArithmetic/Montgomery/ZProofs | 0m08.39s || +0m00.01s 0m08.35s | BoundedArithmetic/ArchitectureToZLikeProofs | 0m08.48s || -0m00.13s 0m08.05s | Encoding/PointEncoding | 0m08.02s || +0m00.03s 0m07.51s | Specific/GF1305 | 0m07.54s || -0m00.03s 0m03.86s | BaseSystemProofs | 0m03.84s || +0m00.02s 0m03.57s | ModularArithmetic/BarrettReduction/ZHandbook | 0m03.69s || -0m00.12s 0m03.46s | ModularArithmetic/ModularBaseSystemListProofs | 0m03.47s || -0m00.01s 0m03.44s | ModularArithmetic/Tutorial | 0m03.59s || -0m00.14s 0m03.26s | BoundedArithmetic/InterfaceProofs | 0m03.16s || +0m00.09s 0m02.87s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.87s || +0m00.00s 0m02.80s | Encoding/PointEncodingPre | 0m02.94s || -0m00.14s 0m02.53s | ModularArithmetic/ModularArithmeticTheorems | 0m02.58s || -0m00.05s 0m02.25s | ModularArithmetic/ModularBaseSystemOpt | 0m02.28s || -0m00.02s 0m02.24s | ModularArithmetic/BarrettReduction/ZBounded | 0m02.29s || -0m00.04s 0m02.07s | Specific/FancyMachine256/Montgomery | 0m02.22s || -0m00.15s 0m02.02s | Specific/FancyMachine256/Barrett | 0m02.16s || -0m00.14s 0m01.83s | ModularArithmetic/Montgomery/ZBounded | 0m01.74s || +0m00.09s 0m01.66s | Specific/FancyMachine256/Core | 0m01.73s || -0m00.07s 0m01.48s | ModularArithmetic/BarrettReduction/Z | 0m01.40s || +0m00.08s 0m01.28s | BaseSystem | 0m01.20s || +0m00.08s 0m01.27s | ModularArithmetic/PrimeFieldTheorems | 0m01.56s || -0m00.29s 0m01.16s | ModularArithmetic/ExtendedBaseVector | 0m01.19s || -0m00.03s 0m00.95s | Util/NumTheoryUtil | 0m00.91s || +0m00.03s 0m00.87s | Experiments/EncodingLemmas | 0m00.96s || -0m00.08s 0m00.70s | ModularArithmetic/ModularBaseSystem | 0m00.62s || +0m00.07s 0m00.67s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.66s || +0m00.01s 0m00.65s | BoundedArithmetic/Interface | 0m00.64s || +0m00.01s 0m00.64s | Encoding/ModularWordEncodingPre | 0m00.62s || +0m00.02s 0m00.64s | Spec/EdDSA | 0m00.70s || -0m00.05s 0m00.61s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.60s || +0m00.01s 0m00.61s | Encoding/ModularWordEncodingTheorems | 0m00.63s || -0m00.02s 0m00.56s | Spec/ModularWordEncoding | 0m00.56s || +0m00.00s 0m00.56s | ModularArithmetic/ModularBaseSystemList | 0m00.62s || -0m00.05s 0m00.52s | BoundedArithmetic/DoubleBounded | 0m00.43s || +0m00.09s 0m00.52s | ModularArithmetic/ZBounded | 0m00.58s || -0m00.05s 0m00.51s | BoundedArithmetic/ArchitectureToZLike | 0m00.45s || +0m00.06s 0m00.50s | Spec/Ed25519 | 0m00.56s || -0m00.06s 0m00.47s | BoundedArithmetic/StripCF | 0m00.46s || +0m00.00s 0m00.45s | ModularArithmetic/Pre | 0m00.67s || -0m00.22s 0m00.43s | ModularArithmetic/Pow2Base | 0m00.44s || -0m00.01s 0m00.42s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.36s || +0m00.06s 0m00.39s | ModularArithmetic/Montgomery/Z | 0m00.38s || +0m00.01s 0m00.34s | Spec/ModularArithmetic | 0m00.36s || -0m00.01s
* Do shl, shr doubling in terms of orGravatar Jason Gross2016-10-06
|
* Add more bounded assembly lemmasGravatar Jason Gross2016-10-06
|
* Add some doubling constructions to bounded arithGravatar Jason Gross2016-10-04
|
* Add some more instructionsGravatar Jason Gross2016-10-04
|
* Add instructions with carry flagsGravatar Jason Gross2016-10-04
|
* Add spec for x86 (#72)Gravatar Jason Gross2016-10-04
|
* Add bitwise and, remove mkl from fancyGravatar Jason Gross2016-10-03
|
* Work around bug 5107 (broken return inference)Gravatar Jason Gross2016-10-03
| | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5107, Unification got weaker in the past week or so. We work around this by making [dlet] non-dependent.
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-10-03
|
* Work around bug #5112 ([Arguments id /] broken)Gravatar Jason Gross2016-09-30
|
* More map -> List.mapGravatar Jason Gross2016-09-29
|
* Add a comment with an exampleGravatar Jason Gross2016-09-26
|
* 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.
* More slight cleanupsGravatar Jason Gross2016-08-24
|
* Clean up DoubleBoundedGravatar Jason Gross2016-08-24
|
* Coq 8.4 fixesGravatar Jason Gross2016-08-24
|
* Weaken the condition on smaller_boundGravatar Jason Gross2016-08-23
|
* Hook up the bounded interface, finish proofsGravatar Jason Gross2016-08-23
|
* Revert "Add _valid properties"Gravatar Jason Gross2016-08-23
| | | | This reverts commit 4e77295a689361876b3e45262f8908d1d98c0073.
* Add _valid propertiesGravatar Jason Gross2016-08-23
|
* Fix some thingsGravatar Jason Gross2016-08-23
|
* Add TODOGravatar Jason Gross2016-08-23
|
* Rework interface to support rewriting databaseGravatar Jason Gross2016-08-23
|
* alternative machine interface specification proposalGravatar Andres Erbsen2016-08-23
|
* Initial work on an architecture interface for ℤ/nℤGravatar Jason Gross2016-08-23
This provides a cleaner interface for the bottom level implementation, as well as an implementation of multiplying 128x128 -> 256.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 19:16:07 +0000