Verifiable C exercise

Here's a C program that implements a hash table with external chaining to implement an efficient mapping from strings to integers. Your task is to prove it correct, using the Verified Software Toolchain.

You may work on this homework with a partner. If you do, then each partner is responsible for doing his or her own proof of each lemma, but you may exchange ideas and advice, look at each others' code, and so on.
This exercise has several different parts. Each part can be worked on independently of the others. They are in approximately increasing order of difficulty. You don't have to do all the parts; just do what you have time for.
If you don't want to work on C programs and Separation Logic, you can complete the Simply Typed Lambda Calculus homework instead.

How to get started

Make sure you can run make and coqc from the command line on your computer. This should be straightforward on a Mac or Linux machine; on Windows I use cygwin.
Download and unpack the VC volume of Software Foundations.
In the vc directory, make should build all your .vo files.
- You should be using a "Coq Platform" installation that has access to VST as a library. If you are not using the "Coq platform install", you may get an error message at "Require Import VST.floyd.proofauto" that it can't find VST.
Now, using CoqIDE (or VSCode, etc.), you can complete the exercises.