Our procrastination has been rewarded! :tada: Plenty thanks for proving these.
This is safe to merge now as it mostly fills in missing parts of opaque proofs, and the lemma whose statement is changed is intended to be private and indeed not used in bedrock2, riscv-coq, or fiat-crypto. The proof scripts look good at a glance as well -- explicit names, braces, nothing obviously redundant. (I still feel deeply unenthusiastic about digging into this code again, and now I can choose not to!)
Our procrastination has been rewarded! :tada: Plenty thanks for proving these.
This is safe to merge now as it mostly fills in missing parts of opaque proofs, and the lemma whose statement is changed is intended to be private and indeed not used in bedrock2, riscv-coq, or fiat-crypto. The proof scripts look good at a glance as well -- explicit names, braces, nothing obviously redundant. (I still feel deeply unenthusiastic about digging into this code again, and now I can choose not to!)