Long-lived invariant violation issue has been fixed so it may be possible to avoid stubbing out these functions aws_cryptosdk_*_(init|clean|clear_up) functions.
Many proofs in this repository include stubs for these functions so the next step would be to study how not including them would affect their performance. If the performance is good, we can avoid using these stubs altogether.
Long-lived invariant violation issue has been fixed so it may be possible to avoid stubbing out these functions
aws_cryptosdk_*_(init|clean|clear_up)functions.Many proofs in this repository include stubs for these functions so the next step would be to study how not including them would affect their performance. If the performance is good, we can avoid using these stubs altogether.