Proposal: verify Raft handlers down to machine code level

[palmskog]

This is a more ambitious version of uwplse/verdi#123, where one uses VST to refine the Raft handlers to C code, which CompCert can compile to verified machine code. As a first step, the verified code could interact with the existing Verdi shim that Verdi Raft uses via OCaml's C interface. One could also implement a standalone shim in C by taking inspiration from the OCaml shim.