feat: stricter word ram model

[Shreyas4991]

The goal of this PR was initially to experiment with a stricter version of the WordRAM model previously introduced in #88. The problem there is one can extract Bitvecs, perform computations in pure and put them back in memory. This is always an issue with monadic models, but here we had a chance to do something stronger. We could force the syntax to specify registers and return Unit.unit. The contents of the registers should remain inaccessible, so there is no get operation. Thus it's basically impossible to work on bitvectors in pure computations, because in the Prog syntax, once can never access them in the first place. OTOH, this suggested some design changes.

Note:

1. Once the set of accessed memory addresses is hidden in the model's state monad, costing it for space complexity separately became tedious. So we merged evalM and costM in ModelM into a single run which returns an AddWriterT value. This also changes how the mvcgen setup works. Note we could just use the old setup and treat cost as a dummy field, but that's pretty suggestive that we really ought to just return a single AddWriterT computation instead of two separate functions for running and costing.

2. On the other hand, keeping evaluation and costs separate has its benefits. It keeps the correctness and complexity proofs separate and simpler, without relying on monadic verification machinery. I have not touched Model itself for now because it is incredibly convenient to not rely on mvcgen for algorithmic proofs where we can avoid it. It is also unclear how the random quick sort PRs Add randomized quicksort and prove correctness #82 and explore: random quicksort variant 2 #87 are affected by this change. It might turn out that there we benefit from the simplicity of not getting into monad transformers.

For now this is an experiment. So I'll leave this a draft PR.