sync-2025-10-09: VeriFast proofs update (#506)

This merges the upstream changes into the VeriFast proofs.

VeriFast now fails on a newly introduced construct. I'm leaving that for
a future commit.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: btj