Formally verifying Advent of Code using Dijkstra's program construction

Summary

It’s a very different style of thinking about programming than most people are used to, but I’ll try my best to explain the notation and the logic I’m using. We start out by writing our post-condition. This is what we want to be true once our program has finished running — in other words, it’s what we want to calculate. We’re going to use this funky-looking syntax called Quantified Notation.As an intro, here’s a basic quantified expression:<+ i:0≤i<N:f.i><+\;i : 0 \leq i < N: f.i><+i:0≤i<N:f.i>f.if.if.i is the syntax we’ll use for accessing the ithi^{th}ith element of some array fff. This is simply shorthand for this longer expression:f.0+f.1+f.2+f.3+⋯+f.(N−1)f.0 + f.1 + f.2 + f.3 + \dotsb + f.(N - 1)f.0+f.1+f.2+f.3+⋯+f.(N−1)For those of you more familiar with functional programming, you’ll find that this is just a reduction over a list. fff is the list in question and +++ is the operation we want to use to combine each element with the accumulator. However, program construction is designed around an imperative language, and so we need an index variable iii to keep track of our position in the array. We also have to specify the range of iii, which is from 000 to the length of the array.With that exposition out of the way, here’s the postcondition for our AoC problem (for a single bank of batteries). You should go read the problem statement over on the AoC website for this to make sense :)<↑i,j:0≤i<j<N:10⋅f.i+f.j><\uparrow i, j : 0 \leq i < j < N : 10 \cdot f.i + f.j><↑i,j:0≤i<j<N:10⋅f.i+f.j>This is a quantification over two variables: iii and jjj. It’s essentially the same as before, but when we reduce using the max operator (↑\uparrow↑), we have to reduce over 10⋅f.i+f.j10 \cdot f.i + f.j10⋅f.i+f.j for every possible combination of iii and jjj, such that jjj is greater than iii. And yeah, that’s exactly what we want: we want the two batteries to turn on such that the concatenation of their joltages is the maximum possible. Note that we’re assuming here that we’ve a...