The base case of the invariants still needs to be proven, but those should be easy. There's a lot of code churn, but it's mostly just formatting changes. Overall this porting went pretty smoothly, and should make the proofs considerably easier to use because sha256_inner actually depended on its own internal state for its output specification before (no longer necessary because now that we have postcondition-style reasoning, we can avoid having to construct the output for cases where we don't care about it).
The base case of the invariants still needs to be proven, but those should be easy. There's a lot of code churn, but it's mostly just formatting changes. Overall this porting went pretty smoothly, and should make the proofs considerably easier to use because
sha256_inneractually depended on its own internal state for its output specification before (no longer necessary because now that we have postcondition-style reasoning, we can avoid having to construct the output for cases where we don't care about it).