Backport F* proofs to Rust and remove patches

[karthikbhargavan]

• Remove patches:
  • Macro for adding inlined F*/Coq/PV/... hax#588, remove patches and inline the F* code.
  • F*: add type annotations on list literals hax#590
  • fix(engine/backend): F*: rec qual. when interface mode hax#589
• Backport F* proofs to Rust

[franziskuskiefer]

Everything in here is done. What are the next steps?

[W95Psp]

I updated the issue, only the "remove patch" part of that issue is done.

[jschneider-bensch]

@karthikbhargavan I believe this is done, latest in #148 (which incorporated all changes from #133). Can you confirm?

[karthikbhargavan]

Looks like yes.

[jschneider-bensch]

Thanks for checking!