This post is part of a series in the context of my PhD work, showcasing the future Rox* (Rust-Oxide-F*) toolchain that will bring deductive verification to Rust. For the full context, see the initial post. The code for this case study is available here.
Our first example concerns how Servo handles the movement of the cursor in HTML’s multiline
<textinput> area. All the logic for this feature is contained within a single file of code. In order to avoid dealing with Servo-specific structs (such as
DOMString) that may not be part of the subset of Rust translatable to F*, I wrote another version of the file keeping only the core logic of the feature. The main structure that describes the state of a selection of text inside the
<textinput> is this one:
There are two tricky things here: first, all the
lines of the text do not have the same length. So navigating inside the text is not as simple as navigating in a perfect rectangle. Second, we keep track of the origin and the direction of the selection, which can be updated as we move the cursor. Given all these elements, figuring out all the cases of what could happen when you press the up arrow key is not trivial. This is precisely the kind of situations where verification can help us make sure we’re not forgetting something.
To help debug the code, the Servo developer had included a very interesting function:
assert_ok_selection function is called at the end of every other function that updates
TextInput; however since it only features
debug_assert, it gets eliminated in release mode. This pattern is precisely equivalent to a postcondition, and this is how I translated it into F* code.
Once I had translated all the code into F*, I proceeded to prove that each function updating
TextInput preserved the invariant
assert_ok_selection: if it is true before the function (in the precondition), it should be true after (in the postcondition). Thanks to the automatic prover Z3, this proof was almost completely automated (I only had to guide the prover with one assertion in one function). However, I could not prove this for the function
adjust_vertical; indeed, it was buggy! Furthermore, it turns out that this newly found bug was causing real problems in the Rust build of Servo, as described in the issue I filed immediately.
Using the error messages from F*, I was able to find a fix in F* that allowed me to prove the postcondition of the function. I backtranslated this fix into the Rust code and opened a pull request including the fix and a few more test cases that triggered the bug.
Note that this work does not guarantee that the code is completely “correct”. Indeed, we just proved that an invariant was preserved, whatever the user input. Thanks to this method, we found a situation not covered by any test case, but which was triggering failures in the build of Servo. With an automated translation tool from Rust to F* and an automatic proof search, I believe that using verification techniques is actually more efficient time-wise than coming up with all the test cases that would trigger all the situations. Moreover, using verification lets you know when you’re done: when it’s proven, it’s proven. With testing, you never know if the test cases you’ve written are enough.