Machine-checked proof of functional equivalence for Simplicity cryptographic Jets

This thesis focuses on the mathematical verification of “jets”—optimized C-language implementations of specific functions within the Simplicity language. The candidate will select a non-trivial cryptographic function, such as jet::bip_0340_verify (Schnorr signatures), and develop a machine-checked proof using a theorem prover like Coq or Lean. The objective is to demonstrate that the optimized jet is functionally equivalent to the verbose Simplicity program specification, ensuring both performance and high-assurance security.

Expected Deliverables:

● A complete, machine-checked proof script in Coq or Lean

● Technical documentation outlining the proof strategy and equivalence results