24.05

Update tutorial after VeriFast breaking changes

In particular, the recent changes to VeriFast that introduce the
distinction between predicates representing initialized memory
(e.g. account_balance) and predicates representing
possibly-uninitialized memory (e.g. account_balance_)
necessitate a number of small changes to the tutorial.