fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	made BaseVector instance global	Jade Philipoom	2016-06-22
\|
*	refactor of Basesystem and ModularBaseSystem; includes general code ↵	Jade Philipoom	2016-06-22
\| \| \| \|	organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division
*	Refactored BaseSystem and ModularBaseSystem.	Jade Philipoom	2016-06-22
\|
*	IterAssocOp: now uses arbitrary representation of scalar that implements testbit	Jade Philipoom	2016-06-22
\|
*	IterAssocOp : now takes a bound argument instead of just using size of exponent	Jade Philipoom	2016-06-22
\|
*	Full pipeline working again	Robert Sloan	2016-06-22
\|
*	Huge Language / Conversion refactors	Robert Sloan	2016-06-22
\|
*	More refactors that will make this whole thing very unstable	Robert Sloan	2016-06-22
\|
*	Running PipelineExample	Robert Sloan	2016-06-22
\|
*	Parsing portion of StringConversion	Robert Sloan	2016-06-22
\| \| \| \| \| \| \| \|	Running PipelineExample Running PipelineExample Running PipelineExample
*	AlmostConversion and part of StringConversion	Robert Sloan	2016-06-22
\| \| \| \|	Parsing portion of StringConversion
*	PseudoMedialConversion done	Robert Sloan	2016-06-22
\|
*	Generalized and cleaned up state model	Robert Sloan	2016-06-22
\| \| \| \|	Pseudo conversions
*	Finished proofs in QhasmEvalCommon for formalizing mappings	Robert Sloan	2016-06-22
\| \| \| \| \| \|	Generalized and cleaned up state model Generalized and cleaned up state model
*	Major language refactoring to support Memory and AddWithCarry	Robert Sloan	2016-06-22
\| \| \| \|	Finished proofs in QhasmEvalCommon for formalizing mappings
*	MedialConversions done	Robert Sloan	2016-06-22
\| \| \| \|	Major language refactoring to support Memory and AddWithCarry
*	Tuple-ization tactics work	Robert Sloan	2016-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Most of Medial, less the conversions Most of Medial, less the conversions Most of Medial, less the conversions Most of Medial, less the conversions More of Medial MedialConversions done
*	Fixed MultiBoundedWords to use wand_mask	Robert Sloan	2016-06-22
\| \| \| \|	Tuple-ization tactics work
*	Full-pipeline example	Robert Sloan	2016-06-22
\|
*	multi works with enough time	Robert Sloan	2016-06-22
\| \| \| \| \| \|	Working on medial language Full-pipeline example
*	pushed mul through the pipeline	Robert Sloan	2016-06-22
\| \| \| \| \| \|	multi_bound weird but better multi_bound weird but better
*	Pushed through 2-ary multiplication except conversions	Robert Sloan	2016-06-22
\|
*	Finished first draft of PseudoConversions	Robert Sloan	2016-06-22
\|
*	actually-decent PseudoConversion semantics	Robert Sloan	2016-06-22
\|
*	A little progress on PseudoConversion	Robert Sloan	2016-06-22
\| \| \| \| \| \|	actually-decent PseudoConversion semantics actually-decent PseudoConversion semantics
*	removed float operations + improved pseudo somewhat	Robert Sloan	2016-06-22
\|
*	A little progress on PseudoConversion	Robert Sloan	2016-06-22
\|
*	Pseudo Evaluation Done	Robert Sloan	2016-06-22
\|
*	Part of Pseudo Evaluation	Robert Sloan	2016-06-22
\|
*	Finished string conversions	Robert Sloan	2016-06-22
\| \| \| \| \| \|	Part of Pseudo Evaluation Part of Pseudo Evaluation
*	Hypothesis-based Bounded Words	Robert Sloan	2016-06-22
\| \| \| \|	Most of string conversions
*	Assembly converted except String and Gallina conversions	Robert Sloan	2016-06-22
\| \| \| \| \| \|	Hypothesis-based Bounded Words Hypothesis-based Bounded Words
*	Simpler QhasmCommon grammar	Robert Sloan	2016-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	updating QhasmCommon Pushing through changes Pushing through changes Pushing through changes Pushing through changes Pushing through changes Pushing through changes
*	figured out all that crazy joinWords refinement	Robert Sloan	2016-06-22
\|
*	Fix Qhasm and AlmostQhasm with new State machinery	Robert Sloan	2016-06-22
\|
*	Breaking out State into its own file	Robert Sloan	2016-06-22
\|
*	add Assembly to CoqProject	Robert Sloan	2016-06-22
\| \| \| \| \| \|	very unstable, but interesting commit very unstable, but interesting commit
*	Module-based reorganization of Qhasm code	Robert Sloan	2016-06-22
\|
*	ed25519 derivation: pair programming with jgross... slow progress	Andres Erbsen	2016-06-22
\|
*	qhasm formal specification + evaluation finished	Robert Sloan	2016-06-22
\|
*	nicer verify() derivation starter	Andres Erbsen	2016-06-22
\| \| \| \| \| \|	Added base types for Qhasm emacs gitignore
*	state top-level derivation for Ed25519.verify	Andres Erbsen	2016-06-22
\|
*	instantiate ed25519 sign in spec	Andres Erbsen	2016-06-22
\|
*	Ed25519: d is nonsquare	Andres Erbsen	2016-06-22
\|
*	extended coordinates setoid boilerplate	Andres Erbsen	2016-06-22
\|
*	Finish absolutizing imports	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \| \| \| \| \|	The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" \| xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
*	Absolutize Coqprime imports	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \| \| \|	Used ```bash cd coqprime make -kj10 cd Coqprime git ls-files "*.v" \| xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Coqprime ```
*	Remove [Admitted]; [Qed] is now under a second	Jason Gross	2016-06-22
\|
*	Use [rewrite] rather than [change] to speed up Qed	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \|	[Opaque] tells kernel unification to defer unfolding a constant as long as possible. This is not a problem for [change], when the functions are small and directly convertible. It's disastrous for [Qed]/[Defined], which (if I understand correctly) try to unify [Opaquemul x' y'] with [mul x y] by fully unfolding [mul] and [x] and [y] before trying to unfold [Opaquemul]; when [x] and [y] are large, this takes a very long time. Rewrite avoids this by telling Coq how to unify [Opaquemul x' y'] with [mul x y] (namely, by unifying [Opaquemul] with [mul], and then [x] with [x'] and [y] with [y']).
*	IterAssocOp : proved iter_op with function exponential	Jade Philipoom	2016-06-22
\|