feat: prove specification of Max program that manipulates memory

[bollu]

After trying to get this to work via the current VCG framework with @alexkeizer , we concluded that the right course of action is to do what's currently done in https://github.com/leanprover/LNSym/blob/main/Proofs/Experiments/AbsVCG.lean