Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Switch to bounded Z | 2016-10-25 | |
* | Add pack, unpack, ge_modulus to axioms to be reified | 2016-10-24 | |
* | Unfold interp stuff in Assembly/GF25519BoundedInstantiation | 2016-10-22 | |
* | Instantiate some things with bounded things | 2016-10-21 | |
* | A bit of initial setup on correct_and_bounded proofs in GF25519BoundedInstant... | 2016-10-20 | |
* | Plug bounded into assembly stuff | 2016-10-20 | |
* | Adjust bounds in assembly | 2016-10-20 | |
* | Split up GF25519Bounded to avoid circular dependencies | 2016-10-20 | |
* | Use carry versions of operations | 2016-10-20 | |
* | rfreeze, not rinv; update to saner boundedness requirements | 2016-10-20 | |
* | Start instantiating boundedness things | 2016-10-19 |