Merge Assembly Machinery into Master #7
Commits on May 10, 2016
Commits on May 16, 2016
Commits on May 18, 2016
Commits on May 19, 2016
Commits on May 26, 2016
Commits on May 27, 2016
Commits on May 29, 2016
Commits on May 30, 2016
Commits on Jun 1, 2016
Commits on Jun 3, 2016
Commits on Jun 4, 2016
Commits on Jun 5, 2016
Commits on Jun 6, 2016
Commits on Jun 20, 2016
Commits on Jun 22, 2016
-
-
-
-
-
-
-
GaloisTheory: added lemmas useful for proving Euler's Criterion with …
…GF. NumTheoryUtil: cleanup.
-
EdDSA25519 : wrote and proved optimized PointEncoding, which encodes …
…y and the sign bit of x, then solves the curve equation for x ^ 2. Required adding several lemmas to GaloisField (and moving others there from PointFormats). recursive-build coqprime
-
-
Update build process to use COQPATH & _CoqProject
Removed all of the files not built by default; they can be resurrected from git history. _CoqProject is the standard way to list the files in a project and to give information to coq_makefile. COQPATH is the standard way to make use of not-yet-installed libraries that are not part of your project (i.e., you don't want to remove them when you `make clean`, etc.).
-
Do some work pair-programming with Andres on opts
Partially pre-compile various optimizations in GF25519.
-
-
-
-
-
Define F m, a replacement for GF with several benefits.
- F has a human readable complete specification - F is a parametric type, not a parametric module - Different F instances can be disambiguated by type inference, which is more conventient that notation scopes. - F has significant support for non-prime moduli - It should be relatively easy to port existing GF code to F. Since the repository currently contains code referencing both F and GF, it makes sense to keep the names different for now. Later, F may or may not be renamed to GF. -
-
-
-
-
-
-
-
-
prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifi…
…edAdd Closed Under Global Context
-
-
-
-
-
-
-
-
moved two non-primality-dependent lemmas to ModularArithmeticTheorems…
… from PrimeFieldTheorems
-
-
instantiated FqEncoding and FlEncoding (also fixed indentation, which…
… is why the commit looks huge)
-
-
-
-
-
-
proved most of point encoding admits, fixed some build system issues …
…(dead imports of PointFormats and Galois things)
-
moved some theorems requiring q mod 8 = 5 precondition to PointEncodi…
…ng from CompleteEdwardsCurve, where the precondition is not in scope.
-
-
-
-
remove bedrock from COQ_ARGS because we all use COQPATH
BoundedWord2 Factor out a tactic and add more examples BoundedWord2: add test cases intermediate stage simple
-
-
-
Add etc/freshen-bedrock-files.sh
It is used on smithers to remove .vo files which are older than relevant Bedrock .vo files. This prevents version mismatches when updating Bedrock on smithers.
-
Ambiguous imports, oh joy! (Coqprime failed to build when Bedrock was in COQPATH.)
-
Factor out some bedrock dependencies into WordUtil
Also move a definition about words, with a TODO about location, into WordUtil.
-
Automate a UList proof a bit so it builds with 8.5
It still builds with 8.4
-
-
ModularArithmetic: [field] tactic that respects opacity, prettify Ext…
…endedCoordinates, outline Edwards curve associativity
-
-
-
-
Use [rewrite] rather than [change] to speed up Qed
[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']).
-
-
Used ```bash cd coqprime make -kj10 cd Coqprime git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Coqprime ```
-
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 ```
-
-
-
-
-
nicer verify() derivation starter
Added base types for Qhasm emacs gitignore
-
-
-
very unstable, but interesting commit very unstable, but interesting commit
-
-
-
-
updating QhasmCommon Pushing through changes Pushing through changes Pushing through changes Pushing through changes Pushing through changes Pushing through changes
-
Assembly converted except String and Gallina conversions
Hypothesis-based Bounded Words Hypothesis-based Bounded Words
-
Part of Pseudo Evaluation Part of Pseudo Evaluation
-
-
-
-
-
A little progress on PseudoConversion
actually-decent PseudoConversion semantics actually-decent PseudoConversion semantics
-
-
-
-
pushed mul through the pipeline
multi_bound weird but better multi_bound weird but better
-
Working on medial language Full-pipeline example
-
-
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
-
Major language refactoring to support Memory and AddWithCarry
-
Major language refactoring to support Memory and AddWithCarry
Finished proofs in QhasmEvalCommon for formalizing mappings
-
Finished proofs in QhasmEvalCommon for formalizing mappings
Generalized and cleaned up state model Generalized and cleaned up state model
-
-
AlmostConversion and part of StringConversion
Parsing portion of StringConversion
-
Parsing portion of StringConversion
Running PipelineExample Running PipelineExample Running PipelineExample
-
-
-
-
-
refactor of Basesystem and ModularBaseSystem; includes general code o…
…rganization 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
-
-
-
-
Reverting Util/IterAssocOp to an earlier version for compatibility wi…
…th CompleteEdwardsCurve/ExtendedCoordinates (we don't have testbit defined yet)
-
Finished refactor of GF25519 (partial evaluation); code builds but ne…
…eds to be reorganized, since many of the theorems in GF25519 are now generalized and do not need to be in Specific/.
-
-
Previously, it was not actually recording when it found things.
-
Retrieved updated version of Util/IterAssocOp and modified ExtendedCo…
…ordinates and Ed25519 to use it.
-
-
-
-
Defined a testbit variant for BaseSystem vectors and proved equivalen…
…ce to Z.testbit.
-
-
-
-
-
-
Add a tactic for field inequalities
Pair programming with Andres, a better proof of unifiedAddM1'_rep, some progress on twistedAddAssoc.
-
-
-
-
added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits…
… having weight 2^26)
-
-
-
-
-
-
-
-
Completed encoding reorganization; factored sign_bit out of PointEnco…
…dings and finished encoding admits.
-
Cleanup: mostly moving lemmas to Util files, some moving lemmas to mo…
…re general contexts.
-
Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to
comparing points).
-
-
-
Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) t…
…o avoid unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want.
-
-
First stage of canonicalization proofs complete; proved 3 carry loops…
… reduce input digits to their minimal widths. Remaining : name fixes and second stage -- proving that we subtract q iff the reduced input is over q (in the range [2^k-c, 2^k-1])
-
Fixed Encoding/PointEncodingTheorems; imports had been deleted, but f…
…or some reason I wasn't affected. Also updated the same file to use E module.
-
-
-
-
-
Fix some issues in Ed25519 tactics
- Use replace rather than refine to speed up [Defined] and make the tactics easier to read - Use [apply f_equal] in place of [reflexivity] for unknown presumably arcane reasons to satisfy Coq's unifier - Factor out some tactics into tactic scripts - Write a lemma to pull functions out of [Let_In] - Fix autoindentation in emacs by wrapping [Let_In_unRep] in parentheses (probably a ProofGeneral regexp gone wrong) - Write a kludgy tactic to unfold [proj1_sig] only when applied to [exist] (Pair programming with Andres)
-
Remove unfolding, rewrite -> setoid_rewrite
Moving the [scalar] argument to the beginning of [iter_op] makes inference of the [Proper] lemmas a bit easier. Making [Reflexive eq] come before [Reflexive Equivalence.equiv] allows [setoid_rewrite] to work; since [setoid_rewrite] does more unfolding than [rewrite], we no longer need to unfold things to make the [rewrite] work.
-
Factor some rewrites into a single [autorewrite]
Slightly less [apply f_equal] beforehand, more automation.
-
-
-
-
-
-
Proper word-based vectorization
Basic wordization lemmas Really complex derivation of wand correctness
-
-
-
first pseudo conversion lemma Decent machinery for automatic pseudo-conversion Decent machinery for automatic pseudo-conversion Decent machinery for automatic pseudo-conversion
-
-
-
-
-
-
-
