LMS-verify: Abstraction without regret for verified systems programming