4 ms·
> how could this ever be proven to never go out of bounds? I've done this in Ada/SPARK. My simple_regex implementation of Rob Pike's algorithm [1] based on th
by pyjarrett 4y ago
> how could this ever be proven to never go out of bounds?
I've done this in Ada/SPARK.
My simple_regex implementation of Rob Pike's algorithm [1] based on this blog post [2], is proved not to crash on overflow or bounds checks.
[1]: https://github.com/pyjarrett/simple_regex https://github.com/pyjarrett/simple_regex
[2]: https://benhoyt.com/writings/rob-pike-regex/ https://benhoyt.com/writings/rob-pike-regex/
- gamegoblin 4y agoIMO, a program failing due to a parse error on the input, and a program failing due to a bounds check are functionally the same thing (provided you are using a language with bounds-checked arrays so you don't segfault). You're just moving the bounds checking from the array access path to the input collecting path. I could be misunderstanding you, though.
- pyjarrett 4y agoMy referenced program is just proven for input sizes. If I wanted to do something to validate an entire program subset similarly, I'd make a type with the bounds I needed that gets fed into that algorithm which is proved for those ranges. This isolates the proved code from user input, but the newtype with range ensures those checks are done prior to being fed into the algorithm. You can't "prove" user input, there has to be validation, but you can force that validation prior to entering the proofed code.