Actually, my loop invariant was unnecessarily confusing (I was sleep deprived), here's a better version: https://clbin.com/OhyJ3

Your question is very interesting and I think the answer is 'yes'. I will try to implement it and report back.