In preparation for proving sha256, I realized it would be helpful to change the phrasing of sha256_inner's specification. In particular:
The abstract state should reference the message seen so far, not the whole message, because sha256 won't know the whole message if it's only gotten part of the data
The postcondition should be in terms of sha256_step, not sha256_compress, just to make the logic a little smoother
Change (2) was pretty straightforward, but change (1) was more complicated. Basically, the sha256_inner circuit really should only reason about the padded message, which is its input, not whatever original message the padded message came from. But this was problematic because the specs require the original message; I couldn't describe what sha256_step should return without passing it the original bytes of the message, which were complicated to derive from the circuit input.
To resolve this problem, I created some shadow definitions for some of the spec functions (M, W, sha256_step, and sha256) that take the padded message as their argument instead of the original message, and proved they're equivalent to the originals. Then I could prove that sha256_inner matches this alternate representation with respect to the padded-message input it gets, without actually requiring that it's a valid padded message. In sha256, when I have the context to know that what I'm passing sha256_inner is indeed a valid padded message, I can use the equivalence lemma to rewrite back to the original spec.
In preparation for proving
sha256, I realized it would be helpful to change the phrasing ofsha256_inner's specification. In particular:sha256won't know the whole message if it's only gotten part of the datasha256_step, notsha256_compress, just to make the logic a little smootherChange (2) was pretty straightforward, but change (1) was more complicated. Basically, the
sha256_innercircuit really should only reason about the padded message, which is its input, not whatever original message the padded message came from. But this was problematic because the specs require the original message; I couldn't describe whatsha256_stepshould return without passing it the original bytes of the message, which were complicated to derive from the circuit input.To resolve this problem, I created some shadow definitions for some of the spec functions (
M,W,sha256_step, andsha256) that take the padded message as their argument instead of the original message, and proved they're equivalent to the originals. Then I could prove thatsha256_innermatches this alternate representation with respect to the padded-message input it gets, without actually requiring that it's a valid padded message. Insha256, when I have the context to know that what I'm passingsha256_inneris indeed a valid padded message, I can use the equivalence lemma to rewrite back to the original spec.