aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers
Commit message (Collapse)AuthorAge
* Better simplification of mulsplitGravatar Jason Gross2017-06-18
|
* Fix typo in formatGravatar Jason Gross2017-06-18
|
* Add fake notation for addcarryx_u128 and similarGravatar Jason Gross2017-06-18
|
* Add some notations for mulxGravatar Jason Gross2017-06-18
|
* Better test for simplifierGravatar Jason Gross2017-06-18
| | | | This one catches more things
* Stronger simplification of adc too add when we can prove the carry is 0Gravatar Jason Gross2017-06-18
|
* Add cnotations for addcarryx with uint8_tGravatar Jason Gross2017-06-18
|
* Add convenience for supporting uint8Gravatar Jason Gross2017-06-18
|
* Add notationsGravatar Jason Gross2017-06-18
|
* Adding more (possibly unneeded) simplificationGravatar Jason Gross2017-06-18
|
* Try more simplificationGravatar Jason Gross2017-06-17
|
* Drop the 0-carry bit before bounds analysisGravatar Jason Gross2017-06-17
|
* Be a bit more forceful in eliminating zeros in arith simplGravatar Jason Gross2017-06-17
|
* More arithmetic simplification for adc, mulGravatar Jason Gross2017-06-17
|
* Add more simplification to pipelineGravatar Jason Gross2017-06-17
| | | | This seemes to be making it slower though....
* Add linearization to inline pairs in post-bounds pipelineGravatar Jason Gross2017-06-17
|
* Add extra simplification to simplifier for adcGravatar Jason Gross2017-06-17
|
* Add more constantsGravatar Jason Gross2017-06-17
|
* Unfold Z.mul_split_at_bitwidth for reificationGravatar Jason Gross2017-06-17
| | | | Also reimplement it with a shift and a mask
* Add some more display constantsGravatar Jason Gross2017-06-17
|
* Add bool into P256Gravatar Jason Gross2017-06-17
|
* Remove fails; if we fail too strongly, we miss debugging informationGravatar Jason Gross2017-06-17
|
* Try to fail a bit faster in bad reificationGravatar Jason Gross2017-06-17
|
* Add back failure at level 100Gravatar Jason Gross2017-06-17
| | | | We still need to idtac, because tc resolution eats messages from fail at any level
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 03:43:15 +0000