CHERI
Proofs for CHERI Concentrate
For the paper CHERI Concentrate: Practical Compressed Capabilities we constructed proofs for:
With the appropriate packages installed, these proofs can be run using Holmake:
Holmake boundsTheory.uo
Holmake compressTheory.uo