Thanks for your answer. Yes, this kind of symbolic inequalities was what I had in mind. The solution via "via" is quite clever. In the beginning I had thought

Thanks for your answer. Yes, this kind of symbolic inequalities was what I had in mind. The solution via "via" is quite clever. In the beginning I had thought that maybe you were using something like Pentagons: https://www.microsoft.com/en-us/research/publication/pentagons-a-weakly-relational-abstract-domain-for-the-efficient-validation-of-array-accesses/ https://www.microsoft.com/en-us/research/publication/pentago... which were developed explicitly in the context of proving array bounds checks. You might want to give them a look. They would cost you in implementation effort, of course, but they might make Puffs (almost as) fast and pretty smart!