TODO

TODO

DONE Native while loops
DONE Integrated prep-oce-eqs to preprocessor
DONE verified bin-search

DONE: Heap and Heapmap

Instantiate higher-order (template) parameters in preprocessor
  (could also help for locale instantiations, e.g., in the sorting examples)


Elaborate memory model: No confusion for better verifiability!

Refinement framework: more flexible matching, 
  e.g., only on combinator structure/loop structure.
  Use pw inside. 
  
  Splitting on refinement goals: Split conc side, then simplify, 
  and only split abs side when necessary.



more verified algos
  Ideas: 
    * Heaps, Dijkstra [we have some performance data there]
    * gratchk: Exception compilation, memmap of certificate. Actually fast enough.
    * drat-checker: Quite complex, but would be cool ... own paper?
    * Push-Relabel: Performance data available, compare with ProgComp C++ algo!
  

Motivation for paper:
  Efficient verified code, still small TCB
    How big is TCB of Isabelle's standard codegen? How big is ours?

  Approach: 
    * Code generation from shallowly embedded IR, which is easy to compile to LLVM.
    * Outside TCB: Preprocessing, VCG, integration of Sepref-Tool