aboutsummaryrefslogtreecommitdiff
path: root/src/Galois/ModularBaseSystem.v
Commit message (Expand)AuthorAge
* Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-02-15
* port ModularBaseSystem.v and GF25519.v to F mGravatar Andres Erbsen2016-02-14
* ModualrBaseSystem: proved lingering admit in subtraction proof.Gravatar Jade Philipoom2016-01-25
* assumption lemmas in PointFormatsGravatar Rob Sloan2016-01-11
* simple refactor of makefile; commentsGravatar varomodt2016-01-09
* Specific/GF25519: explicit formula for multiplicationGravatar Andres Erbsen2015-12-05
* reorganized lemmas; moved several to ListUtil and ZUtil.Gravatar Jade Philipoom2015-11-24
* ModularBaseSystem: added definition to perform a specific sequence of carries...Gravatar Jade Philipoom2015-11-24
* ModularBaseSystem: relocated base_succ to PsuedoMersenneBaseParams, proved ca...Gravatar Jade Philipoom2015-11-20
* Added base_succ precondition to BaseSystem to help prove carrying.Gravatar Jade Philipoom2015-11-19
* ModularBaseSystem: proving reduce case of carry_rep.Gravatar Jade Philipoom2015-11-18
* ModularBaseSystem: carry_rep has boring modular arithmetic proofsGravatar Andres Erbsen2015-11-17
* ModularBaseSystem: introduced lemmas about breaking lists; working on carry_r...Gravatar Jade Philipoom2015-11-17
* ModularBaseSystem.carry: implement, state lemmas, some progress on proofsGravatar Andres Erbsen2015-11-17
* ModularBaseSystem: Implemented and proved subtraction, completing implementat...Gravatar Jade Philipoom2015-11-10
* ModularBaseSystem: implemented fromGF and proved correct, moved inline admits...Gravatar Jade Philipoom2015-11-10
* BaseSystem: added encode definition, included b0_1 precondition in BaseCoefs ...Gravatar Jade Philipoom2015-11-10
* ModularBaseSystem: finished most admits for addition and multiplication, move...Gravatar Jade Philipoom2015-11-09
* ModularBaseSystem: proved addition and multiplication.Gravatar Jade Philipoom2015-11-07
* ModularBaseSystem: finish base_goodGravatar Andres Erbsen2015-11-07
* ModularBaseSystem: prove some admits in mase system extensionGravatar Andres Erbsen2015-11-07
* ModularBaseSystem: continuing to prove base_good.Gravatar Jade Philipoom2015-11-07
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2015-11-06
|\
* | Starting to prove base_good in ModularBaseSystemGravatar Jade Philipoom2015-11-06
| * Specific: PseudoMersenneBaseParams for GF25519Base25Point5.Gravatar Andres Erbsen2015-11-06
| * Merge remote-tracking branch 'jadep/master'Gravatar Andres Erbsen2015-11-06
|/
* ModularBaseSystem: finished proving all admits for reduce_rep; proved base_po...Gravatar Jade Philipoom2015-11-05
* ModularBaseSystem: Implemented reduce and proved reduce_rep, currently workin...Gravatar Jade Philipoom2015-11-05
* ModularBaseSystem: defined an extended base system to represent unreduced pro...Gravatar Jade Philipoom2015-11-04
* ModularBaseSystem skeletonGravatar Andres Erbsen2015-10-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 21:05:18 +0000