aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly/GF25519BoundedInstantiation.v
Commit message (Expand)AuthorAge
* Switch to bounded ZGravatar Jason Gross2016-10-25
* Add pack, unpack, ge_modulus to axioms to be reifiedGravatar Jason Gross2016-10-24
* Unfold interp stuff in Assembly/GF25519BoundedInstantiationGravatar Jason Gross2016-10-22
* Instantiate some things with bounded thingsGravatar Jason Gross2016-10-21
* A bit of initial setup on correct_and_bounded proofs in GF25519BoundedInstant...Gravatar Jason Gross2016-10-20
* Plug bounded into assembly stuffGravatar Jason Gross2016-10-20
* Adjust bounds in assemblyGravatar Jason Gross2016-10-20
* Split up GF25519Bounded to avoid circular dependenciesGravatar Jason Gross2016-10-20
* Use carry versions of operationsGravatar Jason Gross2016-10-20
* rfreeze, not rinv; update to saner boundedness requirementsGravatar Jason Gross2016-10-20
* Start instantiating boundedness thingsGravatar Jason Gross2016-10-19