Factor out iterative program refinement checking algorithm

We want to be able to reuse this algorithm in an upcoming
extension of the partial string model of CKA.