The Design and Implementation of a Verified File System with End-to-End Data Integrity