aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers
Commit message (Collapse)AuthorAge
...
* Better error messages in reificationGravatar Jason Gross2017-06-17
|
* Better reification tactic debuggingGravatar Jason Gross2017-06-17
|
* Revert PR #203Gravatar Jason Gross2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309060964 and https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309101747 Revert "update ocq2C sed script" This reverts commit 4a39f39e195b9b7273810a83de78dfd1d150783e. Revert "make display" This reverts commit cbf6d013c533d5165d749d0f9405a15d1ff0b43e. Revert "Make use of CArrayNotations" This reverts commit cae0e80ae76b76091e7fb86fcd794358a4fe55bb. Revert "Fix CArrayNotations" This reverts commit d0d0fbd4499296a2164e209466227892671556f0. Revert "Revert "Revert "Add CArrayNotations""" This reverts commit b2b8403ca76f6fd461d9a71ac2e9add4359bba8c.
* Fix CArrayNotationsGravatar Jason Gross2017-06-16
| | | | | | Work around [bug #5608](https://coq.inria.fr/bugs/show_bug.cgi?id=5608), Anomaly: No printing rule found for _ _ [1] = { _ } ; return ( _ , _ , .. , _ ). Please report at http://coq.inria.fr/bugs/.
* Revert "Revert "Add CArrayNotations""Gravatar Jason Gross2017-06-16
| | | | This reverts commit 29ad742d76dca90ec9c8d03ab6f4359ccf053a90.
* Revert "Add CArrayNotations"Gravatar Jason Gross2017-06-15
| | | | | | | This reverts commit 44359b29d99ab52154dcfdf2b2b16bca7dbaf339. It triggers [bug #5469](https://coq.inria.fr/bugs/show_bug.cgi?id=5469), which is present in 8.6, but not v8.6 (nor 8.6.1, once it comes out).
* Add CArrayNotationsGravatar Jason Gross2017-06-15
|
* Display Z operations with ℤ attachedGravatar Jason Gross2017-06-15
| | | | This is the lighter-weight solution to #197.
* Eliminate well-bounded IdWithAlt from final outputGravatar Jason Gross2017-06-15
| | | | This closes #195
* Fix debugging codeGravatar Jason Gross2017-06-15
| | | | It was previously trying to run constrs and erroring when we turned on debugging
* Don't force [Require Import String] for debug msgsGravatar Jason Gross2017-06-15
|
* Add constant-pushing IdWithAlt optimizationGravatar Jason Gross2017-06-14
|
* Rework and speed up arithmetic simplifier proofsGravatar Jason Gross2017-06-14
| | | | | | | | | | | | | | | | | | | | | Induction is so much faster than brute force. After | File Name | Before || Change -------------------------------------------------------------------------------- 6m15.02s | Total | 7m14.18s || -0m59.15s -------------------------------------------------------------------------------- 0m11.62s | Compilers/Z/ArithmeticSimplifierWf | 0m42.97s || -0m31.35s 0m06.52s | Compilers/Z/ArithmeticSimplifierInterp | 0m34.28s || -0m27.76s 2m47.55s | Specific/IntegrationTestLadderstep | 2m48.14s || -0m00.58s 1m09.50s | Specific/IntegrationTestKaratsubaMul | 1m08.86s || +0m00.64s 1m03.53s | Specific/IntegrationTestLadderstep130 | 1m04.05s || -0m00.51s 0m16.39s | Specific/IntegrationTestFreeze | 0m16.29s || +0m00.10s 0m13.60s | Specific/IntegrationTestMul | 0m13.60s || +0m00.00s 0m11.58s | Specific/IntegrationTestSub | 0m11.36s || +0m00.22s 0m09.79s | Specific/IntegrationTestSquare | 0m09.71s || +0m00.07s 0m03.64s | Compilers/Z/Bounds/Pipeline/Definition | 0m03.54s || +0m00.10s 0m00.75s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || -0m00.05s 0m00.55s | Compilers/Z/Bounds/Pipeline | 0m00.58s || -0m00.02s
* Make rewrite_eta_match_base_type_impl a bit fasterGravatar Jason Gross2017-06-13
|
* Fix a typoGravatar Jason Gross2017-06-13
|
* Add rewrite_eta_match_base_type_implGravatar Jason Gross2017-06-13
|
* Add eta_match_base_type_implGravatar Jason Gross2017-06-13
|
* Stronger invert_op tacticGravatar Jason Gross2017-06-13
| | | | Now it can handle ops that return (Tbase TZ)
* Fix a major bug in C-notation printingGravatar Jason Gross2017-06-13
| | | | | | | Binary operations with casts were wrongly parenthesized. Luckily, this impacted nothing in A-normal form, and it impacted nothing that is currently displayed. It does, however, impact the display of karatsuba mul.
* Reify Z.mul_with_split_at_bitwidthGravatar Jason Gross2017-06-13
|
* Handle IdWithAlt in the simplifierGravatar Jason Gross2017-06-12
| | | | | It now knows how to deal with _ + 0 involving words, and also eliminates IdWithAlt when both the first argument and the output are the same size word.
* Add some more constant notationsGravatar Jason Gross2017-06-12
|
* Push bounds side conditions through the pipelineGravatar Jason Gross2017-06-12
| | | | This will (hopefully) be useful for karatsuba.
* Add CompileInterpSideConditions.vGravatar Jason Gross2017-06-12
|
* Add snd_interpf_side_conditions_gen_SomeGravatar Jason Gross2017-06-12
|
* Add Named.InterpSideConditionsGravatar Jason Gross2017-06-12
|
* Add Z.InterpSideConditionsGravatar Jason Gross2017-06-12
|
* Add InterpSideConditionsGravatar Jason Gross2017-06-12
|
* Have interped_op_side_conditions return a pointed_PropGravatar Jason Gross2017-06-12
| | | | This will make it easier for [ring] to run on the result, without having spurious [True]s
* Initial stab at id_with_altGravatar Jason Gross2017-06-11
| | | | | What remains (beyond the equality-semidecider) is to propogate the side conditions through the boundedness finder.
* Add dummy version of IdWithAlt to compilersGravatar Jason Gross2017-06-11
| | | | Currently, it doesn't do anything special
* Be more forceful about clearing before abstract in glue codeGravatar Jason Gross2017-06-11
| | | | This is needed to make the typechecker not loop in some cases
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
| | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
* Only use bool in freezeGravatar Jason Gross2017-05-21
| | | | This closes #186
* Fix extra opp in freezeGravatar Jason Gross2017-05-20
| | | | No idea why it's valid both ways, but apparently it is.
* Add compiler optimization for [Zselect (-x) _ _]Gravatar Jason Gross2017-05-20
| | | | | | | | | | | | | | | | | | | | | | | Since x = 0 <-> -x = 0, we can eliminate the negative on the borrow-bit in freeze. After | File Name | Before || Change -------------------------------------------------------------------------------- 5m01.81s | Total | 4m55.75s || +0m06.05s -------------------------------------------------------------------------------- 0m29.05s | Compilers/Z/ArithmeticSimplifierInterp | 0m24.85s || +0m04.19s 0m28.68s | Compilers/Z/ArithmeticSimplifierWf | 0m25.88s || +0m02.80s 2m18.19s | Specific/IntegrationTestLadderstep | 2m19.51s || -0m01.31s 0m53.86s | Specific/IntegrationTestLadderstep130 | 0m53.64s || +0m00.21s 0m15.40s | Specific/IntegrationTestFreeze | 0m15.30s || +0m00.09s 0m11.85s | Specific/IntegrationTestMul | 0m11.72s || +0m00.12s 0m10.72s | Specific/IntegrationTestSub | 0m10.47s || +0m00.25s 0m08.97s | Specific/IntegrationTestSquare | 0m09.15s || -0m00.17s 0m02.78s | Compilers/Z/Bounds/Pipeline/Definition | 0m02.81s || -0m00.03s 0m00.75s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.75s || +0m00.00s 0m00.60s | Compilers/Z/Bounds/Pipeline | 0m00.62s || -0m00.02s 0m00.60s | Compilers/Z/ArithmeticSimplifier | 0m00.65s || -0m00.05s 0m00.36s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.41s || -0m00.04s
* Get sbb conversion working in the pipelineGravatar Jason Gross2017-05-20
| | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change -------------------------------------------------------------------------------- 4m56.46s | Total | 4m54.81s || +0m01.64s -------------------------------------------------------------------------------- 2m19.22s | Specific/IntegrationTestLadderstep | 2m18.29s || +0m00.93s 0m53.92s | Specific/IntegrationTestLadderstep130 | 0m53.83s || +0m00.09s 0m26.24s | Compilers/Z/ArithmeticSimplifierWf | 0m25.65s || +0m00.58s 0m24.93s | Compilers/Z/ArithmeticSimplifierInterp | 0m24.87s || +0m00.05s 0m15.38s | Specific/IntegrationTestFreeze | 0m15.97s || -0m00.58s 0m11.83s | Specific/IntegrationTestMul | 0m11.82s || +0m00.00s 0m10.57s | Specific/IntegrationTestSub | 0m10.50s || +0m00.07s 0m09.18s | Specific/IntegrationTestSquare | 0m09.07s || +0m00.10s 0m02.80s | Compilers/Z/Bounds/Pipeline/Definition | 0m02.57s || +0m00.23s 0m00.78s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.64s || +0m00.14s 0m00.64s | Compilers/Z/ArithmeticSimplifier | 0m00.66s || -0m00.02s 0m00.62s | Compilers/Z/Bounds/Pipeline | 0m00.59s || +0m00.03s 0m00.35s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.36s || -0m00.01s
* Add adc -> sbb to arithmetic simpliferGravatar Jason Gross2017-05-20
| | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change --------------------------------------------------------------------------------------- 6m14.04s | Total | 6m23.68s || -0m09.63s --------------------------------------------------------------------------------------- 0m26.28s | Compilers/Z/ArithmeticSimplifierWf | 0m48.67s || -0m22.39s 0m25.64s | Compilers/Z/ArithmeticSimplifierInterp | 0m14.14s || +0m11.50s 2m17.60s | Specific/IntegrationTestLadderstep | 2m17.90s || -0m00.30s 0m56.48s | Compilers/Z/Named/RewriteAddToAdcInterp | 0m55.76s || +0m00.71s 0m54.26s | Specific/IntegrationTestLadderstep130 | 0m54.53s || -0m00.27s 0m15.89s | Specific/IntegrationTestFreeze | 0m15.07s || +0m00.82s 0m11.69s | Specific/IntegrationTestMul | 0m11.78s || -0m00.08s 0m10.62s | Specific/ArithmeticSynthesisTest | 0m10.59s || +0m00.02s 0m10.54s | Specific/IntegrationTestSub | 0m10.55s || -0m00.01s 0m08.98s | Specific/IntegrationTestSquare | 0m09.04s || -0m00.05s 0m06.05s | Arithmetic/Saturated | 0m06.02s || +0m00.03s 0m03.04s | Compilers/Z/RewriteAddToAdcInterp | 0m03.00s || +0m00.04s 0m02.60s | Compilers/Z/Bounds/Pipeline/Definition | 0m02.25s || +0m00.35s 0m01.52s | Util/ZUtil/AddGetCarry | 0m01.50s || +0m00.02s 0m00.74s | Arithmetic/MontgomeryReduction/WordByWord/Definition | 0m00.71s || +0m00.03s 0m00.62s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.78s || -0m00.16s 0m00.59s | Compilers/Z/ArithmeticSimplifier | 0m00.42s || +0m00.17s 0m00.57s | Compilers/Z/Bounds/Pipeline | 0m00.60s || -0m00.03s 0m00.34s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.37s || -0m00.02s
* Add sbb notations to CNotationsGravatar Jason Gross2017-05-20
| | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------ 0m01.14s | Total | 0m01.29s || -0m00.14s ------------------------------------------------------------------------ 0m00.79s | Compilers/Z/CNotations | 0m00.87s || -0m00.07s 0m00.36s | Specific/IntegrationTestDisplayCommon | 0m00.42s || -0m00.06s
* Also reify Z.sub_with_get_borrowGravatar Jason Gross2017-05-20
| | | | | | | | | | | | | | | | | After | File Name | Before || Change -------------------------------------------------------------------------------- 4m01.69s | Total | 4m00.89s || +0m00.80s -------------------------------------------------------------------------------- 2m18.60s | Specific/IntegrationTestLadderstep | 2m18.52s || +0m00.07s 0m54.16s | Specific/IntegrationTestLadderstep130 | 0m53.85s || +0m00.30s 0m15.24s | Specific/IntegrationTestFreeze | 0m15.10s || +0m00.14s 0m11.70s | Specific/IntegrationTestMul | 0m11.76s || -0m00.06s 0m10.55s | Specific/IntegrationTestSub | 0m10.40s || +0m00.15s 0m09.10s | Specific/IntegrationTestSquare | 0m09.02s || +0m00.08s 0m00.79s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.68s || +0m00.10s 0m00.54s | Compilers/Z/Bounds/Pipeline | 0m00.58s || -0m00.03s 0m00.52s | Compilers/Z/Reify | 0m00.54s || -0m00.02s 0m00.50s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.44s || +0m00.06s
* Add SubWithGetBorrow to reflective machineryGravatar Jason Gross2017-05-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------------------------------- 12m37.09s | Total | 12m23.52s || +0m13.56s ------------------------------------------------------------------------------------------------- 0m12.09s | Compilers/Z/Syntax/Equality | 0m06.70s || +0m05.38s 0m56.82s | Compilers/Z/Named/RewriteAddToAdcInterp | 0m54.12s || +0m02.70s 2m20.25s | Specific/IntegrationTestLadderstep | 2m18.79s || +0m01.46s 0m13.83s | Compilers/Z/ArithmeticSimplifierInterp | 0m12.56s || +0m01.26s 1m38.90s | Spec/Test/X25519 | 1m38.46s || +0m00.43s 0m53.83s | Specific/IntegrationTestLadderstep130 | 0m53.93s || -0m00.10s 0m48.70s | Compilers/Z/ArithmeticSimplifierWf | 0m49.10s || -0m00.39s 0m39.72s | Spec/Ed25519 | 0m39.65s || +0m00.07s 0m22.19s | Primitives/EdDSARepChange | 0m22.08s || +0m00.11s 0m19.69s | Compilers/Named/MapCastWf | 0m19.63s || +0m00.06s 0m15.09s | Specific/IntegrationTestFreeze | 0m15.28s || -0m00.18s 0m11.78s | Specific/IntegrationTestMul | 0m11.61s || +0m00.16s 0m10.54s | Specific/IntegrationTestSub | 0m10.48s || +0m00.05s 0m10.46s | Specific/ArithmeticSynthesisTest | 0m10.47s || -0m00.00s 0m09.30s | Util/ZUtil | 0m09.21s || +0m00.08s 0m09.15s | Compilers/Named/MapCastInterp | 0m09.19s || -0m00.03s 0m09.14s | Specific/IntegrationTestSquare | 0m09.28s || -0m00.13s 0m08.82s | Arithmetic/MontgomeryReduction/Proofs | 0m08.78s || +0m00.04s 0m08.46s | LegacyArithmetic/ArchitectureToZLikeProofs | 0m08.38s || +0m00.08s 0m08.23s | LegacyArithmetic/Double/Proofs/Multiply | 0m08.16s || +0m00.07s 0m07.80s | Arithmetic/Core | 0m07.71s || +0m00.08s 0m07.70s | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m07.78s || -0m00.08s 0m06.72s | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate | 0m06.79s || -0m00.07s 0m06.37s | Util/FixedWordSizesEquality | 0m06.33s || +0m00.04s 0m06.06s | Arithmetic/Saturated | 0m05.84s || +0m00.21s 0m05.43s | LegacyArithmetic/Double/Proofs/RippleCarryAddSub | 0m05.38s || +0m00.04s 0m05.41s | LegacyArithmetic/Pow2BaseProofs | 0m05.31s || +0m00.10s 0m05.05s | Specific/ArithmeticSynthesisTest130 | 0m05.09s || -0m00.04s 0m04.98s | Compilers/Z/Bounds/InterpretationLemmas/PullCast | 0m04.80s || +0m00.18s 0m03.94s | Arithmetic/BarrettReduction/HAC | 0m03.84s || +0m00.10s 0m03.79s | Util/ForLoop/Unrolling | 0m03.80s || -0m00.00s 0m03.45s | LegacyArithmetic/InterfaceProofs | 0m03.40s || +0m00.05s 0m03.23s | Arithmetic/BarrettReduction/Generalized | 0m03.07s || +0m00.16s 0m03.02s | Specific/FancyMachine256/Montgomery | 0m03.20s || -0m00.18s 0m03.00s | Compilers/Z/RewriteAddToAdcInterp | 0m02.94s || +0m00.06s 0m02.98s | Arithmetic/ModularArithmeticTheorems | 0m03.02s || -0m00.04s 0m02.94s | LegacyArithmetic/ZBoundedZ | 0m02.88s || +0m00.06s 0m02.82s | Specific/FancyMachine256/Barrett | 0m02.82s || +0m00.00s 0m02.64s | LegacyArithmetic/Double/Proofs/ShiftLeft | 0m02.54s || +0m00.10s 0m02.63s | LegacyArithmetic/Double/Proofs/Decode | 0m02.53s || +0m00.10s 0m02.62s | LegacyArithmetic/Double/Proofs/ShiftRight | 0m02.72s || -0m00.10s 0m02.56s | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy | 0m02.25s || +0m00.31s 0m02.34s | Compilers/Z/Bounds/Relax | 0m02.40s || -0m00.06s 0m02.26s | LegacyArithmetic/BarretReduction | 0m02.25s || +0m00.00s 0m02.21s | Compilers/Z/Bounds/Pipeline/Definition | 0m02.13s || +0m00.08s 0m02.10s | Util/WordUtil | 0m02.07s || +0m00.03s 0m02.00s | Util/ForLoop/InvariantFramework | 0m01.98s || +0m00.02s 0m01.86s | Specific/FancyMachine256/Core | 0m01.82s || +0m00.04s 0m01.82s | Util/ZUtil/AddGetCarry | 0m01.61s || +0m00.20s 0m01.60s | Arithmetic/PrimeFieldTheorems | 0m01.45s || +0m00.15s 0m01.56s | Arithmetic/BarrettReduction/Wikipedia | 0m01.50s || +0m00.06s 0m01.55s | LegacyArithmetic/MontgomeryReduction | 0m01.53s || +0m00.02s 0m01.25s | Util/NumTheoryUtil | 0m00.96s || +0m00.29s 0m01.03s | Compilers/Z/RewriteAddToAdcWf | 0m01.02s || +0m00.01s 0m00.99s | Arithmetic/Karatsuba | 0m00.81s || +0m00.17s 0m00.98s | LegacyArithmetic/Double/Proofs/BitwiseOr | 0m00.99s || -0m00.01s 0m00.98s | Util/ZUtil/Pow2Mod | 0m00.97s || +0m00.01s 0m00.90s | LegacyArithmetic/Double/Proofs/LoadImmediate | 0m00.95s || -0m00.04s 0m00.80s | LegacyArithmetic/BaseSystemProofs | 0m00.88s || -0m00.07s 0m00.80s | Util/ZUtil/Testbit | 0m00.74s || +0m00.06s 0m00.79s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.65s || +0m00.14s 0m00.76s | Compilers/Z/CNotations | 0m00.78s || -0m00.02s 0m00.76s | Util/ZUtil/Stabilization | 0m00.64s || +0m00.12s 0m00.68s | Util/IterAssocOp | 0m00.69s || -0m00.00s 0m00.66s | Compilers/Z/Syntax/Util | 0m00.66s || +0m00.00s 0m00.66s | Compilers/MapCastByDeBruijnInterp | 0m00.78s || -0m00.12s 0m00.64s | Compilers/Z/CommonSubexpressionElimination | 0m00.58s || +0m00.06s 0m00.63s | LegacyArithmetic/Interface | 0m00.56s || +0m00.06s 0m00.62s | Compilers/Z/Bounds/Pipeline | 0m00.53s || +0m00.08s 0m00.62s | Arithmetic/MontgomeryReduction/WordByWord/Definition | 0m00.67s || -0m00.05s 0m00.62s | LegacyArithmetic/Double/Proofs/SelectConditional | 0m00.58s || +0m00.04s 0m00.55s | Compilers/MapCastByDeBruijnWf | 0m00.62s || -0m00.06s 0m00.52s | Compilers/Z/Reify | 0m00.56s || -0m00.04s 0m00.52s | Compilers/Z/JavaNotations | 0m00.50s || +0m00.02s 0m00.52s | LegacyArithmetic/ZBounded | 0m00.54s || -0m00.02s 0m00.51s | Compilers/Z/Bounds/RoundUpLemmas | 0m00.44s || +0m00.07s 0m00.51s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.47s || +0m00.04s 0m00.50s | Compilers/Z/Syntax | 0m00.44s || +0m00.06s 0m00.50s | Compilers/Z/ArithmeticSimplifier | 0m00.47s || +0m00.03s 0m00.50s | LegacyArithmetic/Double/Core | 0m00.53s || -0m00.03s 0m00.49s | Compilers/Z/Bounds/MapCastByDeBruijnInterp | 0m00.48s || +0m00.01s 0m00.48s | Arithmetic/ModularArithmeticPre | 0m00.47s || +0m00.01s 0m00.47s | Util/NUtil | 0m00.51s || -0m00.04s 0m00.47s | Compilers/Z/Bounds/MapCastByDeBruijnWf | 0m00.40s || +0m00.06s 0m00.47s | Spec/EdDSA | 0m00.51s || -0m00.04s 0m00.46s | Compilers/Z/Bounds/InterpretationLemmas/Tactics | 0m00.48s || -0m00.01s 0m00.46s | Compilers/Z/Named/RewriteAddToAdc | 0m00.49s || -0m00.02s 0m00.45s | Spec/ModularArithmetic | 0m00.45s || +0m00.00s 0m00.45s | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.54s || -0m00.09s 0m00.44s | Arithmetic/MontgomeryReduction/Definition | 0m00.45s || -0m00.01s 0m00.44s | Util/ForLoop/Tests | 0m00.43s || +0m00.01s 0m00.44s | Compilers/Z/MapCastByDeBruijn | 0m00.49s || -0m00.04s 0m00.44s | LegacyArithmetic/ArchitectureToZLike | 0m00.44s || +0m00.00s 0m00.43s | LegacyArithmetic/BaseSystem | 0m00.41s || +0m00.02s 0m00.43s | Compilers/Z/InlineInterp | 0m00.36s || +0m00.07s 0m00.43s | Compilers/Z/MapCastByDeBruijnWf | 0m00.40s || +0m00.02s 0m00.42s | LegacyArithmetic/Pow2Base | 0m00.48s || -0m00.06s 0m00.42s | Compilers/Z/CommonSubexpressionEliminationWf | 0m00.40s || +0m00.01s 0m00.42s | Compilers/Z/Bounds/Interpretation | 0m00.46s || -0m00.04s 0m00.42s | Specific/IntegrationTestDisplayCommon | 0m00.36s || +0m00.06s 0m00.42s | Compilers/Z/RewriteAddToAdc | 0m00.41s || +0m00.01s 0m00.42s | Util/ZUtil/Morphisms | 0m00.38s || +0m00.03s 0m00.42s | Compilers/Z/InlineWf | 0m00.44s || -0m00.02s 0m00.41s | Compilers/Z/CommonSubexpressionEliminationInterp | 0m00.39s || +0m00.01s 0m00.41s | Compilers/Z/HexNotationConstants | 0m00.38s || +0m00.02s 0m00.40s | Compilers/Z/Bounds/MapCastByDeBruijn | 0m00.36s || +0m00.04s 0m00.39s | Compilers/Z/Named/DeadCodeElimination | 0m00.36s || +0m00.03s 0m00.38s | Compilers/Z/Named/DeadCodeEliminationInterp | 0m00.40s || -0m00.02s 0m00.37s | Compilers/Z/MapCastByDeBruijnInterp | 0m00.40s || -0m00.03s 0m00.36s | Compilers/Z/OpInversion | 0m00.36s || +0m00.00s 0m00.36s | Compilers/Z/FoldTypes | 0m00.36s || +0m00.00s 0m00.35s | Compilers/Z/Bounds/Pipeline/OutputType | 0m00.33s || +0m00.01s 0m00.34s | Compilers/Z/BinaryNotationConstants | 0m00.36s || -0m00.01s 0m00.34s | Compilers/Z/Inline | 0m00.41s || -0m00.06s 0m00.34s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.35s || -0m00.00s 0m00.31s | Util/ZUtil/Tactics/Ztestbit | 0m00.30s || +0m00.01s 0m00.31s | Util/ZUtil/Tactics | 0m00.30s || +0m00.01s 0m00.30s | Util/ZUtil/Definitions | 0m00.27s || +0m00.02s 0m00.30s | Util/ZUtil/Zselect | 0m00.30s || +0m00.00s
* Add InlineConstAndOppGravatar Jason Gross2017-05-19
|
* Add compiler optimization for add-with-carryGravatar Jason Gross2017-05-17
| | | | | | | | | | | This closes #171. It's unfortunately a bit fragile, and takes a really long time (about 60s) to prove correct, because Coq is bad at deep dependent pattern matching. We enable a-normal form for the freeze test, because the rewriter only works when the arguments to adc are var or const.
* Allow 'bool' in outputGravatar Jason Gross2017-05-17
|
* Add notations for adcGravatar Jason Gross2017-05-17
| | | | This closes #173
* Zselect notationGravatar Jason Gross2017-05-17
|
* Add reflective machinery for adc, zselectGravatar Jason Gross2017-05-17
|
* Ltac scope interprets some notations as errors, so we make anf a definitionGravatar Jason Gross2017-05-17
|
* Fix a typo in prev commit, add convenience notationGravatar Jason Gross2017-05-17
|
* Allow specifying pipeline options at call-timeGravatar Jason Gross2017-05-17
| | | | | For now, the only option is anormal-form. This will be needed for freeze, because the adc optimization doesn't work when not in anf.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 01:28:59 +0000