aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
| * | | consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-06-22
| * | | refactor field lemmas out of ed25519Gravatar Andres Erbsen2016-06-22
| * | | reduce admits related to point negationGravatar Andres Erbsen2016-06-22
| * | | Reorganization and revision of Encoding code and redefinition of sign_bit fun...Gravatar jadep2016-06-22
| * | | Update to_gallina.mdGravatar jadep2016-06-22
| * | | point_eq_decGravatar Andres Erbsen2016-06-22
| * | | finished last cases of nonzero proofs for associativityGravatar jadep2016-06-22
| * | | wrote up remaining tasks needed for Gallina code (from board at 04/19 meeting)Gravatar jadep2016-06-22
| * | | added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ...Gravatar jadep2016-06-22
| * | | automated most of the code in GF25519Gravatar jadep2016-06-22
| * | | Cleanup of GF25519Gravatar jadep2016-06-22
| * | | Pulled generalized code out of GF25519 so that it can be used for other moduliGravatar jadep2016-06-22
| * | | moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-06-22
| * | | GF25519 additionGravatar jadep2016-06-22
| * | | GF25519: boring stuff -- fixed indentation and removed commented-out codeGravatar jadep2016-06-22
| * | | Add a tactic for field inequalitiesGravatar Jason Gross2016-06-22
| * | | ed25519 derivation: down to final encodingGravatar Andres Erbsen2016-06-22
| * | | ed25519 derivation: use representation of FGravatar Andres Erbsen2016-06-22
| * | | ed25519 derivation: wrangle non-unique representationsGravatar Andres Erbsen2016-06-22
| * | | ed25519 derivation: stuck at main loopGravatar Andres Erbsen2016-06-22
| * | | ed25519 derivation down to word until main equationGravatar Andres Erbsen2016-06-22
| * | | Defined a testbit variant for BaseSystem vectors and proved equivalence to Z....Gravatar jadep2016-06-22
| * | | Added lemmas to Util/ that are needed for testbit.Gravatar jadep2016-06-22
| * | | Cleaned up and revised DoubleAndAdd.Gravatar jadep2016-06-22
| * | | Removed old iter_op version and its last dependency.Gravatar jadep2016-06-22
| * | | Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinate...Gravatar jadep2016-06-22
| * | | Fixed syntax error (missing bracket) in Ed25519 to make merge buildGravatar jadep2016-06-22
| * | | Fix freshen-bedrock-files.shGravatar Jason Gross2016-06-22
| * | | ed25519: continue derivationGravatar Andres Erbsen2016-06-22
| * | | Finished refactor of GF25519 (partial evaluation); code builds but needs to b...Gravatar jadep2016-06-22
| * | | Reverting Util/IterAssocOp to an earlier version for compatibility with Compl...Gravatar jadep2016-06-22
| * | | Merge and refactor of GF25519Gravatar jadep2016-06-22
| * | | Drop second projections in Ed25519Gravatar Jason Gross2016-06-22
| * | | fix of GF25519 in progress; created instantiation of PseudoMersenneBaseParamsGravatar Jade Philipoom2016-06-22
| * | | made BaseVector instance globalGravatar Jade Philipoom2016-06-22
| * | | refactor of Basesystem and ModularBaseSystem; includes general code organizat...Gravatar Jade Philipoom2016-06-22
| * | | Refactored BaseSystem and ModularBaseSystem.Gravatar Jade Philipoom2016-06-22
| * | | IterAssocOp: now uses arbitrary representation of scalar that implements testbitGravatar Jade Philipoom2016-06-22
| * | | IterAssocOp : now takes a bound argument instead of just using size of exponentGravatar Jade Philipoom2016-06-22
| * | | Full pipeline working againGravatar Robert Sloan2016-06-22
| * | | Huge Language / Conversion refactorsGravatar Robert Sloan2016-06-22
| * | | More refactors that will make this whole thing very unstableGravatar Robert Sloan2016-06-22
| * | | Running PipelineExampleGravatar Robert Sloan2016-06-22
| * | | Parsing portion of StringConversionGravatar Robert Sloan2016-06-22
| * | | AlmostConversion and part of StringConversionGravatar Robert Sloan2016-06-22
| * | | PseudoMedialConversion doneGravatar Robert Sloan2016-06-22
| * | | Generalized and cleaned up state modelGravatar Robert Sloan2016-06-22
| * | | Finished proofs in QhasmEvalCommon for formalizing mappingsGravatar Robert Sloan2016-06-22
| * | | Major language refactoring to support Memory and AddWithCarryGravatar Robert Sloan2016-06-22
| * | | MedialConversions doneGravatar Robert Sloan2016-06-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 06:26:09 +0000