aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Jacobian coordinatesGravatar Andres Erbsen2018-01-09
|
* make src/Specific/solinas64_2e255m19_5limbs/*.cGravatar David Benjamin2018-01-08
| | | | | Also refresh things after PR#289. This too just updated the comments, as expected.
* Prove montladder correct in the zero case.Gravatar David Benjamin2018-01-08
|
* Add @@ infix notationGravatar Jason Gross2018-01-06
|
* make src/Specific/solinas32_2e255m19_10limbs/*.cGravatar David Benjamin2018-01-05
| | | | | Refresh things after PR#289, though that just updated the comments, as expected.
* Fix incorrect overridding of bool notationsGravatar Jason Gross2018-01-05
| | | | | | | This notation system is fragile and kludgy. This discovered from @davidben's https://github.com/mit-plv/fiat-crypto/pull/289/commits/ff0fb38346dde67abef982d6305595216d18519b#r159793723
* Handle the fact that we haven't forbidden TWord 3Gravatar Jason Gross2018-01-05
| | | | | We do this by adding notations for addcarryx and subborrow for all of the smaller-than-max-bitwidth sizes of arguments.
* Remove TWord 3 based addcarryx, subborrowGravatar Jason Gross2018-01-05
| | | | This handles bullet 3 of #288
* Print bool as uint8_tGravatar Jason Gross2018-01-05
| | | | This handles bullet point 1 of #288
* make selected-specific-display for permit `TWord 0`Gravatar Jason Gross2018-01-05
| | | | This handles bullet 2 of #288
* Permit `TWord 0`Gravatar Jason Gross2018-01-05
| | | | This handles bullet 2 of #288
* Add support for {addcarryx,subborrow}_u{25,26}Gravatar Jason Gross2018-01-02
| | | | | | | | | | | This closes #286 This is actually a +1,-1 diff in the python script generating the notations, plus running it and rebuilding: ```diff -ADD_CARRY_SUB_BORROW_SIZES = (32, 64, 128, 51) +ADD_CARRY_SUB_BORROW_SIZES = (32, 64, 128, 25, 26, 51) ```
* Update CNotationsGravatar Jason Gross2018-01-02
| | | | | | This makes it easier to add support for more kinds of addcarryx, etc, and also add `: expr_scope` to work around changes from https://github.com/coq/coq/pull/873
* Add some reserved notations for cps stuffGravatar Jason Gross2017-12-27
|
* restore fastpath logic in Curves.Montgomery.XZProofsGravatar Andres Erbsen2017-12-22
|
* prove montgomery ladder for non-zero inputsGravatar Andres Erbsen2017-12-22
|
* Montgomery.XZ, Loops: montladder proof scaffoldingGravatar Andres Erbsen2017-12-22
|
* specialized destruct_head'_* in src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
|
* expose missing proof in src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
|
* clean up src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
|
* Add pow_ceil_mul_nat_divide_nonzeroGravatar Jason Gross2017-12-15
|
* Add reserved notation for infix @ for applicationGravatar Jason Gross2017-12-15
|
* organize .gitignoreGravatar Andres Erbsen2017-12-15
|
* add non-cps version of chained_carries (resolves #283 again)Gravatar jadep2017-12-14
|
* add non-cps carry to experimental pipeline (this resolves #283)Gravatar jadep2017-12-14
|
* Also display timing on .log filesGravatar Jason Gross2017-12-14
|
* Also build non-specific on smithersGravatar Jason Gross2017-12-13
|
* Add missing file from previous commitGravatar Jason Gross2017-12-13
|
* [travis] remove autogenerated files from _CoqProjectGravatar Jason Gross2017-12-13
| | | | This will hopefully work better than kludging around coqdep
* Apparently ln -s is too slow on travis, so we fake it when we're not ↵Gravatar Jason Gross2017-12-13
| | | | building things
* Add fast-path versions of [destruct_head] for unit,bool,TrueGravatar Jason Gross2017-12-12
|
* Fix call to ln -sGravatar Jason Gross2017-12-12
|
* Fix fast-autogenerated-deps targetGravatar Jason Gross2017-12-12
| | | | | | | Also add a kludge to override the .v.d targets of the relevant files. It unfortunately spews a lot of makefile output, but it's better than the target not working at all. When the target is not passed, the behavior is unchanged.
* Loops (trying again) (#259)Gravatar Andres Erbsen2017-12-11
| | | | * clean up src/Experiments/Loops.v, add While and For
* Test more synthesis files on travis / liteGravatar Jason Gross2017-12-11
|
* Bump submoduleGravatar Jason Gross2017-12-08
|
* Bump submoduleGravatar Jason Gross2017-12-08
|
* Print out Coq version info on travisGravatar Jason Gross2017-12-05
|
* Curves.Montgomery.XZ: add+check boringssl ladderstep (#278)Gravatar Andres Erbsen2017-12-05
|
* pick best implementation, not firstGravatar jadep2017-12-01
|
* [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v (#275)Gravatar Jason Gross2017-11-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v It's rather verbose, unfortunately. The reification also doesn't have any of the nice debugging features of the version of reification in Compilers, because that's even more boilerplate. Not sure if I should add that back in, at the moment. Also, for some strange reason, places where `constr`s fail to typecheck seem to induce backtracking where I don't think they should, and I'm not sure what's going on... * [demo] Add more namespacing * Update llet notation, update is_known_const name As per code review suggestions * Namespace var_context, add some coqbug references * Rename is_type_arg to is_template_parameter As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153036059 * Simplify the logic around delayed arguments a bit We no longer pass around dummy markers in the tuple of arguments. * [demo] More informative reification error messages This time without exponential slowdown in failure cases and without needing to manually think up all of the possible errors and write them out. Possible thanks to Hugo's comment at https://github.com/coq/coq/issues/6252#issuecomment-347041995 * [demo] respond to code review, add comments * Update documentation with suggestions from Andres
* Rename run_tactic_as_bool to is_success_run_tacticGravatar Jason Gross2017-11-26
| | | | As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153084144
* Reserve a printing-only notation for function applicationGravatar Jason Gross2017-11-26
| | | | This sets the level and associativity in a common place, and will be useful for PHOAS application nodes
* Add Tactics.RunTacticAsConstrGravatar Jason Gross2017-11-26
|
* Add reserved expr_let notationGravatar Jason Gross2017-11-26
|
* Add src/Specific/.autgenerated-deps to clean targetGravatar Jason Gross2017-11-26
|
* Add a target to speed up coqdep with a kludge on travisGravatar Jason Gross2017-11-26
|
* [demo] Replace (max (length a) (length b)) with explicit nat argGravatar Jason Gross2017-11-24
|
* [Demo] Define [place] in terms of nat_rectGravatar Jason Gross2017-11-24
| | | | This will make it easier to reify
* [demo] Use [List.repeat] rather than [List.map]Gravatar Jason Gross2017-11-24
| | | | | As per https://github.com/mit-plv/fiat-crypto/pull/271/commits/76634efa66aa9085a1e410c04f930dd5645126df#r152719891
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 20:53:53 +0000