Poulet4 interpreter fixes

[hackedy]

Hi, I have some changes in the branch poulet4-interpreter over in the Petr4 repo that I would like to merge into poulet4. I took a look to see how much my changes break Verifiable P4 and in this PR I fix the issues, so far as I can tell.

Can someone take a look at what I've changed and let me know if it builds on your machine (after installing poulet4 from the poulet4-interpreter branch)? I am seeing some build problems that don't appear to be due to the poulet4-interpreter changes, e.g.,

File "./examples/sbf/FlowProperty.v", line 42, characters 63-65:
Error:
In environment
f : list packet
i : Z
The term "Tc" has type "Z -> Z -> Z" while it is expected to have type "Z".

And this, which I assume means I'm missing some VST-related opam package?

File "./examples/sbf/flow_proof.v", line 1, characters 0-35:
Error: Cannot find a physical path bound to logical path VST.floyd.proofauto.

[hackedy]

Build hangs in ./examples/bloomfilter/verif.v, so my changes might have accidentally made the genv terms really big.