aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Remove eval_small_bounded_numlimbsGravatar Jason Gross2017-06-12
| | | | | As per https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-307772410
* Initial stab at id_with_altGravatar Jason Gross2017-06-11
| | | | | What remains (beyond the equality-semidecider) is to propogate the side conditions through the boundedness finder.
* Add dummy version of IdWithAlt to compilersGravatar Jason Gross2017-06-11
| | | | Currently, it doesn't do anything special
* Factor karatsuba through IdfunWithAlt, add testGravatar Jason Gross2017-06-11
| | | | | | | | | | | Currently the refinement is commented out. Also, we drop the proof of equality early (and probably won't use it in the first place); there's no way we can carry around such a proof in reflective-land, so we'll need to add an arithmetical-equality semi-decider to reflective-land that can prove the relevant equalities (or we'll need to leave them over as side-conditions). I expeect this may make things significantly easier on @jadephilipoom.
* Add unfold lemmas for id_with_altGravatar Jason Gross2017-06-11
|
* Add IdfunWithAltGravatar Jason Gross2017-06-11
|
* Don't print directory when entering coqprime folderGravatar Jason Gross2017-06-11
|
* Be more forceful about clearing before abstract in glue codeGravatar Jason Gross2017-06-11
| | | | This is needed to make the typechecker not loop in some cases
* Add script to remake Tactics.v fileGravatar Jason Gross2017-06-11
|
* Add clearbody_allGravatar Jason Gross2017-06-11
|
* Fix loop notations, add for loopsGravatar Jason Gross2017-06-11
|
* Reserve some more notationsGravatar Jason Gross2017-06-11
|
* cps notations WIP...Gravatar Andres Erbsen2017-06-11
|
* cps and loop notations WIPGravatar Andres Erbsen2017-06-11
|
* Finish admits in WordByWord/Proofs.vGravatar Jason Gross2017-06-10
| | | | | Some of the proofs are a bit monsterous. It'd be nice to go back and automate them more sometime.
* Add mod_pull_div{,_full}Gravatar Jason Gross2017-06-10
|
* More powerful replace_neg_with_posGravatar Jason Gross2017-06-10
|
* Fix a typoGravatar Jason Gross2017-06-10
|
* Rename power_mod_full to mod_pow_full for similarity with std libGravatar Jason Gross2017-06-10
|
* Add Z.pow_mod_ProperGravatar Jason Gross2017-06-10
|
* Minor changes to a proof in progressGravatar Jason Gross2017-06-10
|
* Remove useless small_from_bound; drop R_bigGravatar Jason Gross2017-06-10
|
* Add proofs about numlimbsGravatar Jason Gross2017-06-10
|
* Add constraint on scmul scalarGravatar Jason Gross2017-06-10
|
* Update context to not need eval_nonnegGravatar Jason Gross2017-06-10
| | | | | Also add [small], as per https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-307568416
* Add redc_boundGravatar Jason Gross2017-06-10
|
* Create crypto-defects.mdGravatar Andres Erbsen2017-06-10
|
* Remove temporary fileGravatar Jason Gross2017-06-10
| | | | It's been migrated to Definitions.v and Proofs.v in the same directory
* More work in progress on montgomery proofsGravatar Jason Gross2017-06-10
|
* More work on redc correctness proofsGravatar Jason Gross2017-06-10
|
* Add initial proofs for word-by-wordGravatar Jason Gross2017-06-10
|
* Switch from t to T to match #157Gravatar Jason Gross2017-06-10
|
* Update redc algorithmGravatar Jason Gross2017-06-10
| | | | | | | Transcribe https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-301334813 Not sure if it's right, but now I'll try proofs.
* Update word-by-word montgomery with ctx varsGravatar Jason Gross2017-06-10
| | | | | As per https://github.com/mit-plv/fiat-crypto/issues/157#issuecomment-307212425
* Finish proving loop invariant for wbw redcGravatar Jason Gross2017-06-09
|
* Make it clear that the combined definition/proof file is a work in progressGravatar Jason Gross2017-06-09
|
* Admit-free proof of cS3_mod_NGravatar Jason Gross2017-06-09
| | | | | | Fix the algorithm to not talk about join, based on http://colinandmargaret.co.uk/Research/CDW_ELL_99.pdf (p2) and discussions over Signal with @andres-erbsen.
* Fix open sections errorGravatar Jason Gross2017-06-09
|
* More WIP on bounds for redcGravatar Jason Gross2017-06-09
|
* Minor progress on boundsGravatar Jason Gross2017-06-09
|
* Add pair-programmed wbw montgomeryGravatar Jason Gross2017-06-09
| | | | Partial progress with @andres-erbsen
* Remove Karatsuba from the lite targetGravatar Jason Gross2017-06-09
| | | | It was pretty slow.
* Fix broken implicitsGravatar Jason Gross2017-06-08
| | | | Closes #190
* add zero (as per #157)Gravatar jadep2017-06-08
|
* start saturated-arithmetic API for use in Montgomery (see discussion in #157)Gravatar jadep2017-06-08
|
* add Specific/Karatsuba to CoqProjectGravatar jadep2017-06-07
|
* first stage of synthesis for karatsuba with alt-bounds hack, contains ↵Gravatar jadep2017-06-07
| | | | several admitted lemmas
* Bump coq-scriptsGravatar Jason Gross2017-06-06
|
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
| | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
* Allow loop notation to printGravatar Jason Gross2017-06-05
| | | | | | With help from Hugo at https://coq.inria.fr/bugs/show_bug.cgi?id=5581#c1 cc @andres-erbsen
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 03:58:34 +0000