General data type for recursive permissions

[m-yac]

Instead of having to write a SAW core data type and fold/unfold functions for each recursive permission one wants to define, we should have a single data type (IRT for iso-recursive type) which encapsulates everything we need. Then, to define a recursive permission we would just need to provide the Heapster types. Eventually, this would be the only way to define such a permission.

• Define RPTs in Coq
  • Finish defining RPTDesc with variables, then define interpretation, substitution, and RPTElem
  • Write unfoldRPT, foldRPT and a proof (with Admitteds) that they form an isomorphism
  • (Eventually) Figure out a nice way to write recursors / induction principles
• Define IRTs in SAWCore
• In Coq, prove unfoldIRT and foldIRT are inverses
• Integrate with Heapster
  • Add a command to saw-script which defines recursive permissions using IRTs
  • Add IRTs to the proof automation
  • Add some simple examples of using this command (and writing proofs about the output) to heapster-saw
  • Add a command to saw-script which defines reachability permissions using IRTs
  • Add some examples of using the above
• Convert old examples to use IRTs
  • Remove the concept of recursive permissions from the implication checker in favor of IRTs
  • Remove the manual datatypes and fold/unfold functions from old examples and replace the old recursive/reachbility permission commands with the new ones
  • Remove the proof automation for the old datatypes