Advent of Code program verification?

Stream: general

[Jason Orendorff]

I'm solving Advent of Code in Lean this year. Is anyone else trying program verification for these, as an exercise? For a beginner like me, they are plenty complicated. I'd love to hang out in a chat where people are doing this... as things stand, I feel pretty alone :)

[suhr]

There's one difficulty: a proof is not very useful when the specification and the code are basically the same. This is a common problem with AoC.

But some problems can be fun to verify, like https://adventofcode.com/2025/day/5. In part 2 of this day the naive solution is not feasible, but a with a bit of thinking you can solve it quite elegantly.

[suhr]

And these bits of thinking demand a proof.

[suhr]

By the way, here's my solution in K: https://gist.github.com/suhr/4dde948d1d138d56fcc27da892bdb5b8. Which is basically an application of https://www.jsoftware.com/papers/50/50_05.htm.

[Jakub Nowak]

Even when specification and the code are basically the same, you can still prove well-formedness, e.g. that you doesn't lookup array outside it bounds.

[Jakub Nowak]

Also, you can do things like, write a program that can enumerate all possible (or some subset of) problems together with their solutions, and then you can prove that your program finds the solution for every problem.

[Jakub Nowak]

The specification of generating a problem from a solution, can be different, then that of finding a solution, so you get an extra check, that these two specification you wrote coincide.

[Jakub Nowak]

Though, in some cases, enumerating possible problems for a given solution can be much more difficult then finding a solution. .-.

[Jason Orendorff]

The problem, properly expressed, is not the same as my solution for any of the problems this year except day 1. Finding a reasonable way to express the spec is the first problem, for me...

(although the problem for day 12 is NP-complete, so... maybe set that aside for now)

[Jason Orendorff]

Jakub, i don't understand - all my solutions give the puzzle input a type, so the possibility space is clearly enumerable (?)

[Jason Orendorff]

The problem I've been thinking about today is day 3. It talks about "the largest possible" something. The use of the definite article in the question implies at least one such something exists, and that the set is finite...

Mapping that to Lean isn't super easy

[suhr]

largest (x: α) (p: α → Prop) := p x ∧ ∀y, p y → y ≤ x

[suhr]

If 987654321111111 is an a list of digits, then what needed is sublist of a certain length which then is turned into a number.

[suhr]

A useful way to think about sublist in this case is selection (as in https://mlochbaum.github.io/BQN/doc/select.html).

[suhr]

Then you basically take advantage of order relation on both indicies (more specifically, remaining choices) and digits.

[suhr]

Jason Orendorff said:

The problem, properly expressed, is not the same as my solution for any of the problems this year except day 1.

Funny enough, I wrote an informal proof for part 2 in order to debug my solution. It was not effective though, since the bug was in the code, not in how I solved the problem.

[suhr]

Here it is: https://gist.github.com/suhr/70f87b73e763b6238403f0abeaa2d675

[Jason Orendorff]

ok you would not believe what i was doing before, trying to write a spec for day 3, but now I have this

Spec for Day 3

import Day03.Basic

def isLargest (x : Nat) (p : Nat -> Prop) : Prop :=
  p x ∧ ∀ y, p y -> y ≤ x

def isSubsequence (xs : Array α) (ys : Array α) : Prop :=
  ∃ f : Fin xs.size -> Fin ys.size,
    (∀ i j, i < j -> f i < f j)
    ∧ ∀ i, xs[i] = ys[f i]

def decimalValue (digits : Array Nat) : Nat :=
  digits.reverse
    |>.zipWith (· * 10 ^ ·) (Array.range digits.size)
    |>.sum

def spec (size : Nat) (candidate : Input -> Nat) : Prop
:= ∀ input : Input, ∃ answers : Vector Nat input.size,
  (∀ i : Fin input.size, isLargest answers[i] (fun k =>
    ∃ subs, isSubsequence subs input[i] ∧ subs.size = size ∧ decimalValue subs = k))
  ∧ answers.sum = candidate input

theorem solve1_correct (input : Input) : spec 2 solve1 := by sorry
theorem solve2_correct (input : Input) : spec 12 solve2 := by sorry

[Jakub Nowak]

Jason Orendorff said:

Jakub, i don't understand - all my solutions give the puzzle input a type, so the possibility space is clearly enumerable (?)

Enumerating just inputs will only let you check that the program is well-formed.

Let's say, you have types Statement and Solution for the input and output of the solution program. So the solution code would be a function solution : Statement → Solution. Nothing interesting so far. Now, what you could do, is write a function statements : Solution → Set Statement. Function statements, given the solution, would generate some statements, for a particular given solution. With these two functions, you can prove ∀ sol : Solution, ∀ stmt ∈ statements sol, solution stmt = sol.

Creating Set Statement of all statements is usually easy. Creating Solution → Set Statement that enumerates all statements for a given solution, is often not easy.

Of course, you could define statements sol := { stmt : Statement | solution stmt = sol }, but then, the aforementioned proof is just tautology. The point is to write it independently.

[Jakub Nowak]

(deleted)