aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Add seq_add, seq_len_0Gravatar Jason Gross2018-06-19
|
* Add a comment about subGravatar Jason Gross2018-06-18
|
* More compact printing of ASTs in errorsGravatar Jason Gross2018-06-18
|
* Add another prime exampleGravatar Jason Gross2018-06-18
|
* Fix a typo in to-C shiftsGravatar Jason Gross2018-06-18
|
* Don't duplicate error message printing in OCamlGravatar Jason Gross2018-06-18
|
* Pass around lists of strings for error messagesGravatar Jason Gross2018-06-17
| | | | | | | | | | This allows us to get back an error message in Saturated Solinas in OCaml on P256 x32 in reasonable time without blowing the stack. There's the slight oddity that the list of string in the success case is joined by the empty string, but the list of string in the error case is joined by newline. Probably meanas that I chose the wrong abstraction barrier somewhere.
* Add ShowLinesGravatar Jason Gross2018-06-17
|
* New pipeline, split among filesGravatar Jason Gross2018-06-17
|
* Reserve a notatoin for ;;Gravatar Jason Gross2018-06-16
|
* Add zrange equalityGravatar Jason Gross2018-06-15
|
* Add ErrorT monad, and Show classGravatar Jason Gross2018-06-15
|
* Add decimal_string_of_ZGravatar Jason Gross2018-06-15
|
* Add some lemmas and defs to ListUtil.FoldBoolGravatar Jason Gross2018-06-14
|
* Set universe polymorphism in CPSNotationsGravatar Jason Gross2018-06-14
| | | | | | This bypasses universe inconsistencies that arise when trying to return continuations from other continuations, which is a scenario that comes up frequently with cpsbind.
* Add notations for cpsbind, cps_option_bindGravatar Jason Gross2018-06-14
|
* Actually use primitive projections in PrimitiveHListGravatar Jason Gross2018-06-13
|
* Minor refactoringGravatar Jason Gross2018-06-13
| | | | Note that List.repeat (ListUtil.List.repeat) rather than repeat (Coq.Lists.List.repeat) was interfering with extraction
* Add PrimitiveHList, PrimitiveProdGravatar Jason Gross2018-06-13
|
* Move Option.List.map to OptionList.map to fix name clashes in TupleGravatar Jason Gross2018-06-04
|
* Add Option.List.mapGravatar Jason Gross2018-06-04
|
* Move cps notations into a scopeGravatar Jason Gross2018-06-01
|
* Add more bind reserved notationsGravatar Jason Gross2018-05-31
|
* fix over-indented lineGravatar Jade Philipoom2018-05-31
|
* prove prefancy->fancy for barrett special caseGravatar Jade Philipoom2018-05-31
|
* move around some Lets so that 8.8 doesn't errorGravatar Jade Philipoom2018-05-31
|
* relocate ok_expr tactics and fix an admit with a silly bounds relaxation hackGravatar Jade Philipoom2018-05-31
|
* Proved pre-fancy barrett reduction correct (except 1 admit for boundsGravatar Jade Philipoom2018-05-31
| | | | | that are correct but for which bounds relaxation loses necessary information) and add explanatory comments.
* temporary workaround for #352Gravatar Jade Philipoom2018-05-31
|
* Define machine model, write prefancy->fancy pass, and prove Montgomery code ↵Gravatar Jade Philipoom2018-05-31
| | | | correct
* [WIP] shifting addsGravatar Jade Philipoom2018-05-31
|
* change order of additions so that they a) make more sense and b) are more ↵Gravatar Jade Philipoom2018-05-31
| | | | suited to shifting adds
* tweak binders so that shifts from base conversion get inlinedGravatar Jade Philipoom2018-05-31
|
* remove unneeded comment and extra whitespaceGravatar Jade Philipoom2018-05-31
|
* end-to-end proof for montgomeryGravatar Jade Philipoom2018-05-31
|
* Proofs for pre-fancy pass (could use cleanup)Gravatar Jade Philipoom2018-05-31
|
* proofs for straightline pass (with admits for some depth stuff that should ↵Gravatar Jade Philipoom2018-05-31
| | | | be unneeded soon)
* Move function argument out of fixpoint of List.map2Gravatar Jason Gross2018-05-21
| | | | | This allows us to make use of nested fixpoints involving map2, because the function argument can be inlined for guard checking now.
* Compatibility after Coq PR#262.Gravatar Hugo Herbelin2018-05-14
| | | | | | | | | Coq PR#262 makes the inference of return clauses more uniform and general but unification is sometimes not strong enough to deal with this generality. See #5107 for details. One reduces the search space for a return clause by forbidding it to be obtained by small inversion.
* finish pushing through changes to dummy and factor out identifier matchGravatar Jade Philipoom2018-05-07
|
* replace dummy_var with dummy_arrow and change style of straightline tests to ↵Gravatar Jade Philipoom2018-05-07
| | | | be more robust
* clean up shared notations and constant-rewriting logic for prefancyGravatar Jade Philipoom2018-05-07
|
* prefancy now works on barrett (modulo add-opp=>sub)Gravatar Jade Philipoom2018-05-07
|
* Move straightline and prefancy stuff above barrett reductionGravatar Jade Philipoom2018-05-07
|
* Translating to 'pre-fancy' form now works on MontgomeryGravatar Jade Philipoom2018-05-07
|
* move depth to a more sensible locationGravatar Jade Philipoom2018-05-07
|
* Translation to straightline code now works correctly on montgomery256Gravatar Jade Philipoom2018-05-07
|
* Translation to straightline code (first attempts, mostly working)Gravatar Jade Philipoom2018-05-07
|
* fix the placement of a dlet to make more senseGravatar Jade Philipoom2018-05-07
|
* Backtrack on moving a notation to Notations.v, to fix conflictGravatar Jason Gross2018-05-06
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 05:47:33 +0000