IIRC this book unfortunately only proves correctness directly and not runtime. Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code.

Does anybody know of any languages that let you prove properties about the runtime of a function directly implemented in the language?