On verifying functional properties of filesystems in the presence of failures, using proof assistants