Verifying Quantitative Reliability for Programs that Execute on Unreliable Hardware