aboutsummaryrefslogtreecommitdiffstats
path: root/src/common/IntegerExtra.v
Commit message (Expand)AuthorAgeFilesLines
* Define ofbytesYann Herklotz2020-07-041-1/+72
* Switch to uvalueToZ in lessdef.James Pollard2020-07-021-23/+34
* Improve (?) automation.James Pollard2020-07-011-8/+25
* Eliminate memory bounds assumption!James Pollard2020-06-291-2/+2
* Finish first IStore proof (modulo some admissions).James Pollard2020-06-281-12/+12
* Fix unsigned/signed issues.James Pollard2020-06-281-13/+15
* Work on proof.James Pollard2020-06-281-0/+50
* Finish ILoad proof with some assumptions:James Pollard2020-06-241-184/+163
* Normalise entire expression to avoid overflow issues.James Pollard2020-06-231-0/+235