Skip to content

Latest commit

 

History

History
51 lines (50 loc) · 5.19 KB

GUIDE.md

File metadata and controls

51 lines (50 loc) · 5.19 KB

Claims

  1. The CC proof compiler
  2. The Tree proof compiler
  3. The "preserves stack" relation, exp_stack_pure_rel
  4. The relation between Imp environments and Stack's stacks
  5. The Tree plugin
  6. An example of the plugin being invoked
  7. The implication database translation proof obligation
  8. The compiler that changes < to <= (and its associated proof compiler)
  9. The multiplication wrapper helper lemma from Section <>
  10. The exponentiation wrapper helper lemma from Section <>
  11. The hoare triple for the infinite series example
  12. Soundness lemma for Tree
  13. The lemma that shows that stk_valid_tree, the certificate type, can be used to obtain hl_stk, the Stack Hoare proof type
  14. The left shift case study, compiled with the incomplete compiler
  15. The max case study, compiled with the incorrect optimization compiler
  16. The max case study, compiled with the unverified correct compiler
  17. The min case study, which has to be compiled with the unverified correct compiler
  18. The incomplete proof compiler (from our PotPie 3 Ways)
  19. The incorrect proof compiler (from the PotPie 3 Ways section)
  20. The unverified correct proof compiler
  21. The certificate generator in the Tree plugin
  22. stk_valid_tree, the certificate type
  23. How the plugin's boolean tree checker determines that all of the functions preserve the stack
  24. The plugin's boolean tree checker
  25. Uniqueness of Identity Proofs (UIP) for AbsEnv, the type of assertions for Imp: note that this also lets us get UIP for the implication database for Imp, since UIP for a type T implies UIP for T * T pairs, and UIP for a type A implies UIP for list A.
  26. UIP for Imp's function environments
  27. An example of setting opaques for the plugin's normalization algorithm: this led to 100x speedup for the certificate generator!
  28. Proof compiler automation, which helps with satisfying proof obligations for both Tree and CC
  29. Semantics proof automation, which also helps with proof obligations
  30. Sound translation of a Hoare triple's precondition, one of our proof obligations
  31. Sound translation of a Hoare triple's postcondition, another one of our proof obligations
  32. Utilizing unification with Coq's options to avoid unnecessary normalization calls