Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add fast-path versions of [destruct_head] for unit,bool,True | 2017-12-12 | |
| | |||
* | Loops (trying again) (#259) | 2017-12-11 | |
| | | | | * clean up src/Experiments/Loops.v, add While and For | ||
* | Curves.Montgomery.XZ: add+check boringssl ladderstep (#278) | 2017-12-05 | |
| | |||
* | [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v (#275) | 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 | 2017-11-26 | |
| | | | | As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153084144 | ||
* | Reserve a printing-only notation for function application | 2017-11-26 | |
| | | | | This sets the level and associativity in a common place, and will be useful for PHOAS application nodes | ||
* | Add Tactics.RunTacticAsConstr | 2017-11-26 | |
| | |||
* | Add reserved expr_let notation | 2017-11-26 | |
| | |||
* | [demo] Replace (max (length a) (length b)) with explicit nat arg | 2017-11-24 | |
| | |||
* | [Demo] Define [place] in terms of nat_rect | 2017-11-24 | |
| | | | | This will make it easier to reify | ||
* | [demo] Use [List.repeat] rather than [List.map] | 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 | 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 | 2017-11-24 | |
| | |||
* | Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.v | 2017-11-24 | |
| | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/271#discussion_r152720545 | ||
* | Make a copy of Demo.v | 2017-11-24 | |
| | |||
* | Add support for custom intro tactic in ring pkg, for speed | 2017-11-17 | |
| | |||
* | Fix an argument order issue | 2017-11-17 | |
| | |||
* | Add interpf_SmartVarf | 2017-11-17 | |
| | |||
* | Add fast path for vm_decide (_ = false) | 2017-11-17 | |
| | |||
* | Update display logs and c files | 2017-11-17 | |
| | |||
* | Add fast path for vm_decide (_ = true) package | 2017-11-17 | |
| | |||
* | Make arguments of InterpLinearize more implicit | 2017-11-17 | |
| | |||
* | Add Interp{ExprEta,Linearize}_ind | 2017-11-17 | |
| | |||
* | Update display logs and c files | 2017-11-17 | |
| | |||
* | Add native_compute evar packages | 2017-11-16 | |
| | |||
* | Add vm_compute_cbv_evar_package | 2017-11-16 | |
| | |||
* | Add ModInv autosolver | 2017-11-16 | |
| | |||
* | Update display logs and c files | 2017-11-16 | |
| | |||
* | build src/Specific/montgomery64_2e510m290x2e496m1_8limbs/femul.c | 2017-11-16 | |
| | |||
* | Update display logs and c files | 2017-11-16 | |
| | |||
* | Delete .gitignore | 2017-11-15 | |
| | |||
* | Update display logs and c files | 2017-11-15 | |
| | |||
* | Add a bunch of missing fesquare files | 2017-11-15 | |
| | | | | | I (or someone else?) forgot to `git add` them when invoking remake_curves. | ||
* | build two montgomery files, including 32-bit p256 | 2017-11-15 | |
| | |||
* | Add MontgomeryAPI.encode and two lemmas about it | 2017-11-14 | |
| | | | | One of them is Admitted. | ||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Add more constant notations | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| | |||
* | Update display logs and c files | 2017-11-14 | |
| |