Add a deep embedding of Hacspec

[cmester0]

We could add a deep embedding of Hacspec, this would enable us to reason cross backend, and allow us to make the semantics of Hacspec precise. An attempt at defining this is was done in #284.