hacspec
[ProVerif] Insert markers for including handwritten model instead of stub definitions
As one part of addressing #563, this PR replaces the stub definitions for designated-as-handwritten translations by commented-out inclusion markers of the form (* {{ proofs/proverif/handwritten/<path_to_item_module>.pvl }} *) that indicate where the handwritten model can be found.
The idea is to connect this to further tooling (e.g. in the hax driver?) which would replace these markers with the contents of the handwritten model, most probably replacing the first occurrence of a given handwritten model marker with it's file contents and removing the remaining ones, if any. This would ensure that handwritten models are inserted as early as possible and should avoid ProVerif missing a definition because it's defined later in the file.
As a caveat to this simple approach, removing the handwritten stubs entirely means the extracted model will not typecheck anymore if there are handwritten portions still missing. To address this, we could generate the stub and the inclusion marker and make the marker replacement tooling a bit smarter so it's able to also remove the stub definitions.
