aboutsummaryrefslogtreecommitdiff
path: root/src/Util
Commit message (Collapse)AuthorAge
* Clean up notations after bbv removalHEADmasterGravatar Benjamin Barenblat2019-04-26
| | | | | | | Restore `Reserved Notation` directives for `$ x` and `# x`, which were commented out to avoid conflicts with bbv. Make both notations `at level 9, x at level 9`, which matches unary prefix operators throughout the rest of the development.
* Remove WordUtilGravatar Benjamin Barenblat2019-04-26
| | | | Remove Util/NUtil.v and Util/WordUtil.v. This code is no longer in use.
* Remove BoundedWordGravatar Benjamin Barenblat2019-04-26
| | | | | | Remove Util/BoundedWord.v and its reverse dependencies Util/FixedWordSizes.v and Util/FixedWordSizesEquality.v. This code is no longer in use.
* Add some move/transport eq lemmasGravatar Jason Gross2019-04-22
|
* Add push_rew_fun_depGravatar Jason Gross2019-04-22
|
* Add Primitive.reflect_eq_prodGravatar Jason Gross2019-04-18
|
* Add some bool eqb lemmasGravatar Jason Gross2019-04-05
|
* Don't eagerly unfold boolean functions, hopefully, in tc reflect searchGravatar Jason Gross2019-04-05
|
* Hint reflect on negbGravatar Jason Gross2019-04-05
| | | | | | This way we can pick it up based on the bool, and not just on the Prop. This allows us to `apply Reflect.reflect_bool in H` for `H : negb (_ =? _) = true` and have it work.
* Add Z.combine_at_bitwidthGravatar Jason Gross2019-04-02
|
* Add constr_fail and constr_fail_withGravatar Jason Gross2019-03-31
| | | | | | | | | | | | | Rather than taking the convention that failures during constr construction emit a type error from `I : I` with the actual error message `idtac`d above them (because Coq has no way to emit multiple things on stderr), we instead factor everything through a new `constr_fail` or `constr_fail_with msg_tac`, which emit more helpful messages instructing the user to look in `*coq*` or to use `Fail`/`try` to see the more informative error message. When we can make our own version that does both `idtac` and `fail` (c.f. https://github.com/coq/coq/issues/3913), then we can do something a bit more sane, hopefully.
* improve zero_bounds tacticGravatar jadep2019-03-26
|
* add some hints to the global databasesGravatar jadep2019-03-26
|
* Move some lemmas to appropriate placesGravatar jadep2019-03-25
|
* Add Forall2_Proper instancesGravatar Jason Gross2019-03-08
|
* Add Forall2_map_map_iffGravatar Jason Gross2019-03-08
|
* Fix issue with previous commitGravatar Jason Gross2019-03-08
|
* Add some eq list_rect lemmas to ListUtilGravatar Jason Gross2019-03-08
|
* Remove GlobalTacticalsGravatar Jason Gross2019-03-08
| | | | | | | | It turns out they don't actually work. See https://github.com/coq/coq/issues/9719, https://github.com/coq/coq/issues/9718, https://github.com/coq/coq/issues/9717, https://github.com/coq/coq/issues/9462#issuecomment-470822923
* Fix grepeat tacticGravatar Jason Gross2019-03-08
| | | | It previously required progress on all goals, rather than any goal
* Fix gprogress tacticalGravatar Jason Gross2019-03-08
|
* Add some gtacticsGravatar Jason Gross2019-03-08
|
* Add Forall2_forall_In_combine_iffGravatar Jason Gross2019-03-07
|
* Add some eq lemmas to ListUtilGravatar Jason Gross2019-03-07
|
* Add some Proper lemmas to ListUtilGravatar Jason Gross2019-03-07
|
* Add reserved notations for \inGravatar Jason Gross2019-03-05
|
* Add some minor reflect thingsGravatar Jason Gross2019-03-04
|
* Make [reflect] a typeclass and add a bunch of lemmasGravatar Jason Gross2019-03-04
|
* Add Option.{lift,map,combine}, List.Option.liftGravatar Jason Gross2019-02-11
| | | | These will be useful for extending the AST with `option` types.
* Add zrange_rect{,_Proper,_Proper_dep}Gravatar Jason Gross2019-02-02
|
* Add option_beq_heteroGravatar Jason Gross2019-02-02
|
* Add remove_duplicatesGravatar Jason Gross2019-01-24
|
* Define String.replaceGravatar Jason Gross2019-01-18
|
* Remove ? notationGravatar Jason Gross2019-01-17
| | | | It was colliding with the ?[a] notation for fresh evars
* Add some more basic ZRange lemmasGravatar Jason Gross2019-01-15
|
* Move StringMap into Strings/Gravatar Jason Gross2019-01-15
|
* Add StringMapGravatar Jason Gross2019-01-15
|
* Add String_as_OTGravatar Jason Gross2019-01-15
| | | | | Copied verbatim from https://github.com/mit-plv/fiat/blob/master/src/Common/String_as_OT.v
* Autocompute s and c in WBW MontgomeryGravatar Jason Gross2019-01-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows us to support primes which are not a power of 2. We also add p484 as an example. To support this, I added a small parser combinator library which can parse arithmetic expressions involving `()^*/+-` and decimal digits. Closes #486 Closes #342 After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 22m14.42s | Total | 12m14.76s || +9m59.65s | +81.61% -------------------------------------------------------------------------------------------- 9m41.91s | p484_32.c | N/A || +9m41.90s | ∞ 0m11.51s | p484_64.c | N/A || +0m11.50s | ∞ 3m16.22s | p384_32.c | 3m12.02s || +0m04.19s | +2.18% 4m12.18s | PushButtonSynthesis.vo | 4m10.16s || +0m02.02s | +0.80% 0m45.08s | ExtractionHaskell/word_by_word_montgomery | 0m45.24s || -0m00.16s | -0.35% 0m38.14s | p521_32.c | 0m38.12s || +0m00.02s | +0.05% 0m31.80s | p521_64.c | 0m31.78s || +0m00.01s | +0.06% 0m31.09s | ExtractionHaskell/unsaturated_solinas | 0m30.77s || +0m00.32s | +1.03% 0m24.18s | ExtractionHaskell/saturated_solinas | 0m24.21s || -0m00.03s | -0.12% 0m17.38s | ExtractionOCaml/word_by_word_montgomery | 0m17.35s || +0m00.02s | +0.17% 0m13.39s | secp256k1_32.c | 0m13.59s || -0m00.19s | -1.47% 0m13.14s | p256_32.c | 0m13.04s || +0m00.10s | +0.76% 0m10.58s | ExtractionOCaml/unsaturated_solinas | 0m10.73s || -0m00.15s | -1.39% 0m10.23s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.34s || -0m00.10s | -1.06% 0m07.88s | ExtractionOCaml/saturated_solinas | 0m07.94s || -0m00.06s | -0.75% 0m06.78s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.86s || -0m00.08s | -1.16% 0m06.28s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.42s || -0m00.13s | -2.18% 0m06.00s | p224_32.c | 0m05.97s || +0m00.03s | +0.50% 0m05.50s | p384_64.c | 0m05.35s || +0m00.15s | +2.80% 0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.08s || +0m00.20s | +3.93% 0m05.10s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.98s || +0m00.11s | +2.40% 0m04.12s | ExtractionHaskell/saturated_solinas.hs | 0m04.15s || -0m00.03s | -0.72% 0m02.14s | curve25519_32.c | 0m02.28s || -0m00.13s | -6.14% 0m01.44s | CLI.vo | 0m01.42s || +0m00.02s | +1.40% 0m01.44s | curve25519_64.c | 0m01.57s || -0m00.13s | -8.28% 0m01.14s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.02s | +2.70% 0m01.12s | p256_64.c | 0m00.98s || +0m00.14s | +14.28% 0m01.11s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.05s | -5.12% 0m01.03s | secp256k1_64.c | 0m01.15s || -0m00.11s | -10.43% 0m01.02s | p224_64.c | 0m00.99s || +0m00.03s | +3.03% 0m00.21s | Util/Strings/ParseArithmetic.vo | N/A || +0m00.21s | ∞
* Move le_{add,sub}_1_* to ZUtil.LeGravatar Jason Gross2018-12-25
|
* Add has_body tacticGravatar Jason Gross2018-12-21
|
* prove [eval_conditional_sub]Gravatar jadep2018-12-21
|
* Add ZRange.cc_m, ZRange.is_bounded_by_bool_cc_mGravatar Jason Gross2018-12-11
|
* Add ZRange.is_bounded_by_bool_normalize_constantGravatar Jason Gross2018-12-11
|
* Add ZRange.normalize_constantGravatar Jason Gross2018-12-11
|
* Add ZRange.is_bounded_by_bool_constantGravatar Jason Gross2018-12-11
|
* Add ZRange.OperationBoundsGravatar Jason Gross2018-12-11
|
* Add In_elements_mem_iffGravatar Jason Gross2018-12-11
|
* Add Forall2_update_nthGravatar Jason Gross2018-12-06
|
* Fix broken proofsGravatar Jason Gross2018-12-04
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-26 22:31:37 +0000