search

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
124 stars 20 forks source link

Prove and reorganize all padder helper lemmas #937

Closed jadephilipoom closed 3 years ago

jadephilipoom commented 3 years ago

I needed some of the same helper lemmas to adjust some of the other proofs and start with the outer sha256 circuit, so it made sense to just prove them and move them to the appropriate files. Padder proofs are now closed under the global context :tada: