[FStar] Prove panic freedom without hand-edits

[karthikbhargavan]

The F* verification currently requires hand-edits to the generated F* code.
We would like to eliminate these hand-edits and prove panic-freedom.
We would also like to prove panic freedom for all the core code.

[karthikbhargavan]

Termination checking (without hand-edits) for some recursive functions is blocked by cryspen/hax#1233