Adopt Grackle in gokv tutorial

[mjschwenne]

Hello everybody,

I'm Matt, one of Tej's students at UW Madison. I've been working on grackle to automate marshaling and unmarshaling in perennial, specifically for the gokv tutorial. This work introduces a new script update-grackle.sh which can regenerate all of the grackle files, similar to update-goose.py although written in bash instead of python and a CI workflow to check that the grackle files are up to date.

This PR should be merged immediately after the corresponding gokv PR.

By the way, I'm happy to remove the nixos setup (.envrc, flake.nix and flake.lock) if you don't want that stuff on the master branch.

[mjschwenne]

I don't think that the check-goose workflow will pass until the gokv PR is merged since the script now expects new grackle packages that aren't merged into gokv yet.

[upamanyus]

Looks like there's a merge conflict in the tutorial proofs with the master branch because of the migration to byte strings. I'm taking a look at it now. Let me know if someone else is also doing that so I don't duplicate the effort.

[tchajed]

@mjschwenne can you take a look? I thought you had already worked on these byte string changes, so you might have the context to fix these merge conflicts quickly.

[upamanyus]

I also just realized some of the broken files might be generated by grackle, not hand written. I'll definitely leave it to @mjschwenne. If they are grackle-generated, it might be good to put a comment at the top saying so (I originally thought src/program_proof/tutorial/kvservice/put_proof.v was hand written, but now I think it isn't).

[tchajed]

That put_proof.v file is definitely auto-generated and it already has an auto-generated notice. Looking at the grackle templates both the Go output and the Coq proofs have such a header.

[upamanyus]

My bad, I had an old commit of grackle checked out. Disregard my comments (there aren't even any merge conflicts).

[mjschwenne]

Ok good, I was a bit confused since I thought that I had already fixed all of the byte_string issues (which did create a bunch of merge conflicts) but that was resolved last week. I figured I'd merge again to see what popped up but everything seems to be up to date.

[tchajed]

Once you ignore all the auto-generated files, this PR removes 400 lines of marshaling proof from the kvservice proof, which is a great simplification.

Other than that the added infrastructure looks good to me; we now have another script update-grackle.sh to generate the marshaling proofs, and check that everything is up-to-date in CI, same as we already did with the goose output.

[tchajed]

We decided that the auto-generated Coq files should have _gk in them as well, to help indicate that they come from Grackle. Once that's implemented I'll merge the PR.