aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Add .c and .log filesGravatar Jason Gross2018-01-15
|
* Add x25519 donna versions with the new way of generating C codeGravatar Jason Gross2018-01-15
|
* Combine the zero and non-zero cases together.Gravatar David Benjamin2018-01-15
| | | | | | This required tending to montladder not being proved Feq-preserving (sidestepped by proving for all P = 0), and then some wrestling with scalarmult to show the right-hand side was indeed zero when x is (0, 0).
* Add a comment for why Z.peano_rect_strong exists.Gravatar David Benjamin2018-01-14
|
* Add some fecarry .log filesGravatar Jason Gross2018-01-10
|
* Add some fecarry .log and .c filesGravatar Jason Gross2018-01-10
|
* Generate fecarry for solinasGravatar Jason Gross2018-01-10
| | | | | | | This is a one-line change in generate_parameters.py (plus some whitespace trimming), and running `make regenerate-curves` This handles part of #294
* Factor out fsatz lemmasGravatar Jason Gross2018-01-09
| | | | | | | | | After | File Name | Before || Change | % Change ------------------------------------------------------------------------- 1m11.42s | Total | 1m53.75s || -0m42.33s | -37.21% ------------------------------------------------------------------------- 1m06.02s | Curves/Weierstrass/Jacobian | 1m53.76s || -0m47.73s | -41.96% 0m05.40s | Util/FsatzAutoLemmas | N/A || +0m05.40s | ∞
* Replace char_ge_12 with char_ge_3Gravatar Jason Gross2018-01-09
| | | | We no longer seem to need the stronger hypothesis.
* Massively speed up JacobianGravatar Jason Gross2018-01-09
| | | | | | | | After | File Name | Before || Change | % Change --------------------------------------------------------------------------- 1m52.31s | Total | 13m36.75s || -11m44.44s | -86.24% --------------------------------------------------------------------------- 1m52.31s | Curves/Weierstrass/Jacobian | 13m36.75s || -11m44.44s | -86.24%
* Revert "Replace char_ge_12 with char_ge_3"Gravatar Jason Gross2018-01-09
| | | | | | This reverts commit d33d8be154dbce048ac10d82bc0b39468abd5fdb. Hmm, apparently there's an error on Qed... maybe a bug in fsatz?
* Replace char_ge_12 with char_ge_3Gravatar Jason Gross2018-01-09
| | | | We no longer seem to need the stronger hypothesis.
* Jabobian.v: par -> allGravatar Andres Erbsen2018-01-09
|
* src/Curves/Weierstrass/Jacobian.v: specialized destruct_head_*Gravatar Andres Erbsen2018-01-09
|
* @davidben merged Jacobian+affine into Jacobian+JacobianGravatar Andres Erbsen2018-01-09
|
* 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
|
* 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
|
* Add fast-path versions of [destruct_head] for unit,bool,TrueGravatar Jason Gross2017-12-12
|
* Loops (trying again) (#259)Gravatar Andres Erbsen2017-12-11
| | | | * clean up src/Experiments/Loops.v, add While and For
* Curves.Montgomery.XZ: add+check boringssl ladderstep (#278)Gravatar Andres Erbsen2017-12-05
|
* [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
|
* [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-14 03:17:30 +0000