Verify typestate transition functions #10
Description
SquirrelFS's correctness relies heavily on the correctness of its typestate transitions; if they don't do what the typestate says they do, the system may have subtle crash consistency bugs. One way we could improve this is to verify only the typestate transition functions (which would hopefully be a relatively self-contained verification project and not require modeling the entire system) with a tool like Verus https://github.com/verus-lang/verus