Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL