Created by finegeometer on January 26, 2022

`PPEVHPV3NUKUGSD2IQWYM6O42TKH3X55SCWED3C6FHNFJZ6GGBPQC`

main

###### File addition: README.md

[2.1]`# atari-proofs`

`The goal of this project is to formally prove a lower bound on the time it takes to beat the game [*Dragster*](https://en.wikipedia.org/wiki/Dragster_(video_game)).`

`Here is the plan:`

`- Implement a partial Atari 2600 emulator in [Coq](https://coq.inria.fr/).`

`- Connect it to the [Iris](https://iris-project.org/) separation logic framework.`

`- Documentation is sparse, but an explanation of how to define a language can be found [here](https://github.com/tchajed/iris-simp-lang).`

`- Iris can be used for assembly code — see [this project](https://github.com/logsem/cerise-stack).`

`- Along the way, do some toy proofs. For example, prove that `LABEL: JMP LABEL` does not affect memory.`

`- Attempt to prove a useful lower bound for Dragster.`

`- The final theorem should not mention the Iris logic. It should look something like this:`

`- In any reachable state, if RAM location 0b0000000 is nonzero, some function of RAM locations 0b0110011, 0b0110101, and 0b0110111 is greater than some number.`

`- Yes, there's only 128 bytes of RAM!`

`- Due to *Dragster*'s history, it will be interesting to see whether I can prove a bound greater than 5.51 seconds, or not.`

###### File addition: .ignore

[2.1]`.git`

`.DS_Store`