aboutsummaryrefslogtreecommitdiffstats
path: root/src/common/Monad.v
Commit message (Collapse)AuthorAgeFilesLines
* Prove a spec for the mapping of function paramsMichalis Pardalos2021-05-061-6/+5
| | | | | Extracted the traversal of call args into a function and gave it a spec, so that it can be used to prove the overall spec for the Icall instruction.
* Merge branch 'michalis' of https://github.com/mpardalos/vericert into ↵Yann Herklotz2021-02-161-4/+35
|\ | | | | | | michalis-merge
| * Add PTree traversal functions for vericert monadsMichalis Pardalos2021-02-151-1/+20
| |
| * Implement renumbering (wrong)Michalis Pardalos2021-01-251-3/+14
| |
* | Add correct copyright notices in filesYann Herklotz2021-01-101-0/+18
|/
* Continuing work on proving specificationYann Herklotz2020-05-251-0/+6
|
* Add statemonad declarationYann Herklotz2020-05-241-0/+42