# How fast *can't* games be completed?
*Dragster*, for the Atari 2600, is an interesting case in speedrunning history.
A famous speedrunner, Todd Rogers, claims to have beaten the game in 5.51 seconds. (It's a short game.)
But this is disputed. Other people in the speedrunning community claim that this is not just incorrect, but impossible. 
They claim that there *does not exist* a sequence of joystick movements and button presses
that will lead to the game being completed in less than 5.57 seconds.
Now, there are methods for formally proving properties of software.
They're not common, but see examples like the [CompCert C compiler](https://compcert.org/),
or the [seL4 operating system](https://sel4.systems/).
So my question is: can we *formally prove* a lower bound on how fast Dragster can be completed?
There are three possible outcomes.
- We prove a lower bound of 5.54 or 5.57. 
In this case, Todd Rogers must have been wrong about achieving a 5.51.
- We prove a lower bound of 5.51 or lower. 
If we're lucky, this could lead to the discovery a way to beat Dragster in 5.51 seconds, vindicating Todd Rogers.
- Formally proving useful things about games may just turn out to be infeasible. 
This would be disappointing, but is very possible.
If this project is successful, a more ambitious target might be the original *Super Mario Bros.*,
for which the fastest possible time is believed to be 4:54.265.
## A formal model
In mathematics, you need to define your terms. If you want to talk about real numbers, you first need to define them.
(They're a ordered collection of things with addition, negation, multiplication, and reciprocation, saisfying thirteen axioms.)
If you want to talk about symmetry, you need to define the concept of symmetry group. And if you want to prove a lower bound on Dragster times, you need to precisely define how an Atari 2600 works.
This basically amounts to writing an emulator. 
We define the state of the processor, and how each instruction affects it.
We define the memory map; the behavior of reading and writing to different areas of memory.
The behavior does not need to be completely defined. We don't need to describe how illegal opcodes behave; we just need to prove they won't be executed. We probably don't need to precisely define the behavior of the peripherals; I don't think we care what value is read from them.
It's worth noting that proof will assume the Atari 2600 definition is correct. If it isn't, the proof won't quite prove what we think it does.
## Making the model usable
Once we have our model of the Atari 2600, we can prove things about it. Right?
Not so fast. In theory, we can. But it won't be practical.
It'll take dozens of lines even to prove the behavior of `LABEL: JMP LABEL`, let alone any real program.
So we need to simplify. We need most of the low-level detail to be handled automatically.
I'm not entirely sure how to do this. But I have a few ideas.
---
Here's my thinking:
We want to specify, for each possible value of the program counter, a property of the Atari's state. 
We want to prove that the property holds on startup, and that it will continue to hold as the program runs.
Finally, we want the property at the victory-handling code to ensure that the timer's value is greater than our lower bound. 
And we need all this to not take an unreasonable amount of work. So we simplify.
1. For program counter values outside of ROM, we choose the property `False`.
    This will require us to prove that the program counter never leaves ROM.
    But in return, we get that each possible program counter value corresponds to a unique instruction,
    irrespective of the state of the processor or memory.
2. For most possible values of the program counter, the property can be automatically generated.
    For example, consider this code:
    ```
    LABEL1: LDA #$00
    LABEL2: ...
    ```
    If the property at `LABEL2` is `P`, the property at `LABEL1` should default to
    `state => P(state[accumulator = 0x00, sign_flag = False, zero_flag = True])`.
    Property-preservation is automatic.
Suddenly, instead of having to define thousands of properties, and thousands of property-preservation theorems,
we only need a few. But I worry about two things:
- We still need to specify a property somewhere in each loop, to keep the automatic property generation from endlessly looping.
Even in the rendering code, which we really don't care about.
- The property-preservation theorems might be too complicated.
"If this property holds, and then we apply these ten instructions, then that property will hold."
## Using the model
Once using the model is practical, we get to the main part of the project: proving a lower bound on the time.
This is where we analyze the actual mechanics of the game.
If all goes well, we can formalize players' reasoning about why one can't beat 5.57. Alternatively, we might find a subtle error in that reasoning, and discover that 5.57 can be beaten! Either result would be interesting.

- [How fast *can't* games be completed?](./speedrunning_lower_bound.md)