aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments
Commit message (Expand)AuthorAge
* Montgomery.XZ, Loops: montladder proof scaffoldingGravatar Andres Erbsen2017-12-22
* add non-cps version of chained_carries (resolves #283 again)Gravatar jadep2017-12-14
* add non-cps carry to experimental pipeline (this resolves #283)Gravatar jadep2017-12-14
* Loops (trying again) (#259)Gravatar Andres Erbsen2017-12-11
* [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v (#275)Gravatar Jason Gross2017-11-26
* [demo] Replace (max (length a) (length b)) with explicit nat argGravatar Jason Gross2017-11-24
* [Demo] Define [place] in terms of nat_rectGravatar Jason Gross2017-11-24
* [demo] Use [List.repeat] rather than [List.map]Gravatar Jason Gross2017-11-24
* [demo] Pass in a [nat] for list lengthGravatar Jason Gross2017-11-24
* Remove tuple from src/DemoWithReification.vGravatar Jason Gross2017-11-24
* Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.vGravatar Jason Gross2017-11-24
* automate some proofs; also remove trace-based reasoning in favor of induction...Gravatar jadep2017-10-26
* invariants don't need to know the fuelGravatar jadep2017-10-26
* WIP: loopsGravatar jadep2017-10-26
* remove unused filesGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Remove everything after the individual reified opsGravatar Jason Gross2017-04-03
* remove undeclared lines from Ed25519Extraction.vGravatar Andres Erbsen2017-03-02
* move large non-building chunks of Ed25519.vGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Removed code that will be completely replaced in the future; replaced some po...Gravatar jadep2017-02-22
* move lemmas from Ed25519 to WordUtilGravatar jadep2017-02-22
* move some lemmas from Ed25519 to ZUtilGravatar jadep2017-02-22
* moved more stuff to NUtilGravatar jadep2017-02-22
* Moved N lemmas from Ed25519 and IterAssocOp into new NUtil fileGravatar jadep2017-02-22
* categorize the rest of the stuff in Ed25519Gravatar jadep2017-02-22
* categorize some of the stuff in Ed25519Gravatar jadep2017-02-22
* Fix changed namesGravatar Jason Gross2017-02-03
* Generalize add_coordinatesGravatar Jason Gross2016-11-17
* Support for 128-bit wordsGravatar Jason Gross2016-11-14
* extraction: inline field operations into group operationsGravatar Andres Erbsen2016-11-14
* Add mulW_noinlineGravatar Jason Gross2016-11-14
* Proper_sqrtGravatar Andres Erbsen2016-11-13
* Remove extra admitted lemmas in 8.4Gravatar Jason Gross2016-11-12
* GF25519: add ErepAddGravatar Andres Erbsen2016-11-11
* [cbn] is 8.5 onlyGravatar Jason Gross2016-11-11
* Fix proofs broken by stronger preconditionsGravatar Jason Gross2016-11-11
* Most of the admits in Ed25519.vGravatar Rob Sloan2016-11-11
* extraction less slowGravatar Andres Erbsen2016-11-11
* Work around looping in 8.4Gravatar Jason Gross2016-11-10
* Rewrite cast_word so that it's extracted betterGravatar Jason Gross2016-11-09
* implement X25519Gravatar Andres Erbsen2016-11-06
* move B_order_l and prime_qGravatar Andres Erbsen2016-11-06
* Connect [is_bounded] to [bounded_by]Gravatar Jason Gross2016-11-06
* Work around a bug in 8.4 vm_computeGravatar Jason Gross2016-11-05
* put EdDSA encoding sign bit at the MSBGravatar Andres Erbsen2016-11-04
* fix extraction directives -- tested enc((l+1)B)=enc(B)Gravatar Andres Erbsen2016-11-03
* separate Ed25519Extraction.v, add extraction to MakefileGravatar Andres Erbsen2016-11-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 18:18:39 +0000