string case study

[cassiatorczon]

A case study with null-terminated strings. Includes a CN datatype for string buffers (cn_types.h), logical CN specification functions (spec_funs.h), a few trusted lemmas (trusted.h), a few lemmas proven in CN (lemmas.c), a utility function (util.c), and a toy example (example.c).

I also included more_lemmas.broken.c, which contains in-progress CN versions of the trusted lemmas (these got stuck on the issue of having no equivalent of Rocq's intro x), and unused.c, which has a few lemmas I did not end up using for this example but that may be useful for future work with strings. I'm happy to remove these two files if that's cleaner. For the broken lemmas, it's not clear to me whether it's preferable to prove them in CN; as is, the fact that the lemmas in lemmas.c are proven in CN means that CN re-verifies all of the lemmas in lemmas.c every time it verifies example.c, which gets slow. (@dc-mak is there any way to prevent CN from re-verifying code that has not changed?)

[dc-mak]

You can use the --skip flag (which takes a comma separated list of names IIRC) to skip the lemmas, and you can also mark them as trusted: in the spec (but obviously with such great power comes great responsibility).

[dc-mak]

Also for the "we need intros tactic": you might be able to use a loop (or recursive function) to prove this? The "intro" tactic would then just be a C variable declaration int i; (C as a proof language is strange, I admire this effort), and inside the loop you do instantiate i;.