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.

Author: btj

.gitignore

@@ -0,0 +1,6 @@
+*.aux
+*.log
+tutorial.pdf
+*.synctex.*
+*.toc
+*.out