Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Print out Coq version info on travis | Jason Gross | 2017-12-05 |
| | |||
* | Curves.Montgomery.XZ: add+check boringssl ladderstep (#278) | Andres Erbsen | 2017-12-05 |
| | |||
* | pick best implementation, not first | jadep | 2017-12-01 |
| | |||
* | [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v (#275) | Jason Gross | 2017-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_tactic | Jason Gross | 2017-11-26 |
| | | | | As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153084144 | ||
* | Reserve a printing-only notation for function application | Jason Gross | 2017-11-26 |
| | | | | This sets the level and associativity in a common place, and will be useful for PHOAS application nodes | ||
* | Add Tactics.RunTacticAsConstr | Jason Gross | 2017-11-26 |
| | |||
* | Add reserved expr_let notation | Jason Gross | 2017-11-26 |
| | |||
* | Add src/Specific/.autgenerated-deps to clean target | Jason Gross | 2017-11-26 |
| | |||
* | Add a target to speed up coqdep with a kludge on travis | Jason Gross | 2017-11-26 |
| | |||
* | [demo] Replace (max (length a) (length b)) with explicit nat arg | Jason Gross | 2017-11-24 |
| | |||
* | [Demo] Define [place] in terms of nat_rect | Jason Gross | 2017-11-24 |
| | | | | This will make it easier to reify | ||
* | [demo] Use [List.repeat] rather than [List.map] | Jason Gross | 2017-11-24 |
| | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/271/commits/76634efa66aa9085a1e410c04f930dd5645126df#r152719891 | ||
* | [demo] Pass in a [nat] for list length | Jason Gross | 2017-11-24 |
| | | | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/271/commits/76634efa66aa9085a1e410c04f930dd5645126df#r152720364 and https://github.com/mit-plv/fiat-crypto/pull/271/commits/76634efa66aa9085a1e410c04f930dd5645126df#r152720444 | ||
* | Remove tuple from src/DemoWithReification.v | Jason Gross | 2017-11-24 |
| | |||
* | Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.v | Jason Gross | 2017-11-24 |
| | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/271#discussion_r152720545 | ||
* | Make a copy of Demo.v | Jason Gross | 2017-11-24 |
| | |||
* | Remove obsolete syntax for locality. (#270) | Maxime Dénès | 2017-11-20 |
| | | | | | | | This is preparing the landing of https://github.com/coq/coq/pull/1049. For now, I'm duplicating this patch which was already done upstream in CoqPrime, but please consider removing this ad-hoc copy (see discussion on PR #269). | ||
* | Add support for custom intro tactic in ring pkg, for speed | Jason Gross | 2017-11-17 |
| | |||
* | Fix an argument order issue | Jason Gross | 2017-11-17 |
| | |||
* | Add interpf_SmartVarf | Jason Gross | 2017-11-17 |
| | |||
* | Add fast path for vm_decide (_ = false) | Jason Gross | 2017-11-17 |
| | |||
* | Update display logs and c files | Jason Gross | 2017-11-17 |
| | |||
* | Add fast path for vm_decide (_ = true) package | Jason Gross | 2017-11-17 |
| | |||
* | Add a regenerate-curves target | Jason Gross | 2017-11-17 |
| | | | | | | It's currently a bit ad-hoc, and relies on the presence of git to add things to _CoqProject, but it's a bit better than manually invoking the commands. More refinements to come, hopefully. | ||
* | Make arguments of InterpLinearize more implicit | Jason Gross | 2017-11-17 |
| | |||
* | Add Interp{ExprEta,Linearize}_ind | Jason Gross | 2017-11-17 |
| | |||
* | Update display logs and c files | Jason Gross | 2017-11-17 |
| | |||
* | Add native_compute evar packages | Jason Gross | 2017-11-16 |
| | |||
* | Add vm_compute_cbv_evar_package | Jason Gross | 2017-11-16 |
| | |||
* | Add ModInv autosolver | Jason Gross | 2017-11-16 |
| | |||
* | change how input data is gathered and tweak tables | jadep | 2017-11-16 |
| | |||
* | table formatting tweaks | jadep | 2017-11-16 |
| | |||
* | remove old aggregate file | jadep | 2017-11-16 |
| | |||
* | krail -> krait | Andres Erbsen | 2017-11-16 |
| | |||
* | excplicit, sorted list of failures on haswell | Andres Erbsen | 2017-11-16 |
| | |||
* | clean benchmarks on android | Andres Erbsen | 2017-11-16 |
| | |||
* | android benchmarking script in new format | Andres Erbsen | 2017-11-16 |
| | |||
* | actual measurements on Haswell | Andres Erbsen | 2017-11-16 |
| | |||
* | Update display logs and c files | Jason Gross | 2017-11-16 |
| | |||
* | clean Haswell benchmarks | Andres Erbsen | 2017-11-16 |
| | |||
* | build src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femul.c | Andres Erbsen | 2017-11-16 |
| | |||
* | Update display logs and c files | Jason Gross | 2017-11-16 |
| | |||
* | make latex tables | jadep | 2017-11-15 |
| | |||
* | rename a couple files | jadep | 2017-11-15 |
| | |||
* | change error format on parameter generation script | jadep | 2017-11-15 |
| | |||
* | remove bad curve25519 representation from benchmark results | jadep | 2017-11-15 |
| | |||
* | Update crypto-defects.md | Andres Erbsen | 2017-11-15 |
| | |||
* | Update README.md | Jason Gross | 2017-11-15 |
| | | | Formatting | ||
* | Update README.md | Jason Gross | 2017-11-15 |
| |