  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.
