4 ms·
I'm not entirely sure what you had in mind, but you can express certain inequalities. For example, https://github.com/google/puffs/blob/master/std/gif/decode_lz
by nigeltao 9y ago
I'm not entirely sure what you had in mind, but you can express certain inequalities. For example, https://github.com/google/puffs/blob/master/std/gif/decode_lzw.puffs https://github.com/google/puffs/blob/master/std/gif/decode_l... has this line:
assert n_bits < (width + 8) via etc
The 'via' syntax is discussed at https://github.com/google/puffs/blob/master/doc/puffs-the-language.md https://github.com/google/puffs/blob/master/doc/puffs-the-la...
- tom_mellior 9y agoThanks 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!