fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	add non-cps version of chained_carries (resolves #283 again)	jadep	2017-12-14
\|
*	add non-cps carry to experimental pipeline (this resolves #283)	jadep	2017-12-14
\|
*	Also display timing on .log files	Jason Gross	2017-12-14
\|
*	Also build non-specific on smithers	Jason Gross	2017-12-13
\|
*	Add missing file from previous commit	Jason Gross	2017-12-13
\|
*	[travis] remove autogenerated files from _CoqProject	Jason Gross	2017-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 ↵	Jason Gross	2017-12-13
\| \| \| \|	building things
*	Add fast-path versions of [destruct_head] for unit,bool,True	Jason Gross	2017-12-12
\|
*	Fix call to ln -s	Jason Gross	2017-12-12
\|
*	Fix fast-autogenerated-deps target	Jason Gross	2017-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)	Andres Erbsen	2017-12-11
\| \| \| \|	* clean up src/Experiments/Loops.v, add While and For
*	Test more synthesis files on travis / lite	Jason Gross	2017-12-11
\|
*	Bump submodule	Jason Gross	2017-12-08
\|
*	Bump submodule	Jason Gross	2017-12-08
\|
*	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
\|