In this paper, we develop semantics foundations for precise cost analyses for architectures with multi-scalar pipelines and in-order execution with branch prediction. This model is then used to prove correct an automatic cost analysis. The analysis is implemented and evaluated in an extant framework for high-assurance cryptography. In this field, developers aggressively hand-optimize their code to take maximal advantage of micro-architectural features while looking for provable semantic guarantees.