Revision 855bc8b8f798a6734b8e90f2b2190327f7769105 authored by Jay Bosamiya on 11 June 2019, 21:33:57 UTC, committed by Jay Bosamiya on 11 June 2019, 21:33:57 UTC
Previously, we had an assumption in proof of [lemma_locations_complete] that was unprovable since it was false. By refining the statement that the lemma proves, we no longer need this false assumption, and are able to prove things. This does come with the additional cost of a few "observe" assertions in the [InstrReordering] proofs, but all is well and good :)
1 parent f3ec0c6
| File | Mode | Size |
|---|---|---|
| .docker | ||
| code | ||
| dist | ||
| doc | ||
| hints | ||
| lib | ||
| obj | ||
| providers | ||
| secure_api | ||
| specs | ||
| tests | ||
| tools | ||
| vale | ||
| .gitattributes | -rw-r--r-- | 118 bytes |
| .gitignore | -rw-r--r-- | 219 bytes |
| LICENSE | -rw-r--r-- | 11.1 KB |
| Makefile | -rw-r--r-- | 32.2 KB |
| Makefile.common | -rw-r--r-- | 1.2 KB |
| Makefile.include | -rw-r--r-- | 2.7 KB |
| README.EverCrypt.md | -rw-r--r-- | 14.9 KB |
| README.HACL.md | -rw-r--r-- | 3.4 KB |
| README.Vale.md | -rw-r--r-- | 2.2 KB |
| README.md | -rw-r--r-- | 1.8 KB |
| build_local.sh | -rwxr-xr-x | 1.8 KB |
Computing file changes ...
