| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix definition of BoundedWord |  Jason Gross | 2017-04-01 |
| | | | | | | | | We need to take log2, because wordT takes lg(wordsize). We need to pass None rather than Some, because None means "the original output type of the function we're reifying is a tuple of Z" (as opposed to a tuple of words), which is the situation we're in. | ||
| * | Split off BoundedWord.v from IntegrationTest.v | Jason Gross | 2017-04-01 |
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |