Zero-cost meta-programmed stateful functors in F*

We present zero-cost, high-level F* functors and their compilation to low-level, efficient C code. Thanks to a combination of partial evaluation, fine-grained control of reduction, and tactic-driven C++ template-like metaprogramming, we provide the programmer with a toolkit that dramatically reduces the proof-to-code ratio, brings out the essence of algorithmic and implementation agility, and allows substantial code reuse while remaining at a very high-level of abstraction. None of our techniques require modifying the F* compiler. We describe a systematic process to develop functors, and illustrate it with the streaming functor, which wraps an error-prone, cryptographic block API by hiding internal buffering and state machine management to prevent C programmer mistakes. We apply this functor to 10 implementations from the HACLxN cryptographic library. We then write a tactic to automate the functor encoding, allowing the programmer to author multi-argument functors with a deeply nested call graph without any syntactic overhead. We apply this general tactic on 5 algorithms from HACL*, yielding over 30 specialized functor applications. We use as an example Curve25519, a complex algorithm whose final, specialized version we express as nested functor applications.