### State the theorem!

Created by  finegeometer  on March 22, 2022
`NJNJOBP4TDPPOBAQ52CAXIY3HC6CIEDBYT3HZG4KU36HW3KWZDVAC`
main
##### Change contents
• ###### Insertion in theories/memory.v at line 88 [3.6002]
[3.8591]
``Lemma shift_pair {n V} : (memory n (V * V) = memory n V * memory n V)%type.``Proof.``    move: V.``    elim n; first done.``    move=> n' IH V.``    apply IH.``Defined.``Definition from_bytes (n : nat) {A V} (convert : A -> V) :``    nat_rect``        (fun _ => Type -> Type)``        (fun T => A -> T)``        (fun _ f T => f (f T))``        n``        (memory n V).``Proof.``    set X := memory n V.``    have: memory n V -> X by [].``    move: X.``    elim n; simpl.``    - by move=> X f /convert /f.``    - move=> n0 recurse X pair.``        apply: (recurse) => mem1.``        apply: recurse => mem2.``        rewrite shift_pair in pair.``        exact: pair (mem1, mem2).``Defined.``(* How do we know that `from_bytes` puts the bytes in the right order?``    I don't know how to phrase the theorem. But here's an example:``*)``Goal from_bytes 3 (fun x => x) 0 1 2 3 4 5 6 7 = (((0,1),(2,3)),((4,5),(6,7))).``Proof. compute. reflexivity. Qed.``Goal get (from_bytes 3 (fun x => x) 0 1 2 3 4 5 6 7) (word_of_nat 6) = 6.``Proof.``    have -> : from_bytes 3 (fun x => x) 0 1 2 3 4 5 6 7 = (((0,1),(2,3)),((4,5),(6,7))) by compute.``    simpl.``    (* Actually, I don't know how to evaluate this cleanly. *)``Abort.``
• ###### File addition: goal.v (----------)
[4.20]
``Require Import word memory peripherals atari dragster.``Definition this_is_a_dragster_rom (rom : ROM) : Prop``    (* The first half of the cartridge contains the code for Dragster. ``        (Dragster is a 2K game, but there is 4K of memory available.)``    *)``    := fst rom = dragster_rom``    (* The reset vector points to 0xF000. *)``    /\ get rom (pushLow (false, pushLow (false, op0 true))) = op0 false``    /\ get rom (pushLow (true, pushLow (false, op0 true))) = ``        concat (op0 (n := 4) false, op0 (n := 4) true).``(* The theorem we want to prove.``    "Dragster cannot be beaten in fewer than 5.57 seconds."``*)``Definition speedrun_lower_bound : Prop :=``    (* On any Dragster rom, *)``    forall rom, this_is_a_dragster_rom rom ->``    (* for any reachable state of the game, *)``    forall s : state rom, reachable s ->``        (* if the player has crossed the finish line, *)``        nat_of_word (get (RAM (Peripherals s)) (word_of_nat 0x3a)) > 0x60 ->``        (* then the timer shows at least 5.57 seconds. *)``        let '(digit1, digit2) := split (m := 4) (n := 4) ``            (get (RAM (Peripherals s)) (word_of_nat 0x33)) in``        let '(digit3, digit4) := split (m := 4) (n := 4) ``            (get (RAM (Peripherals s)) (word_of_nat 0x35)) in``        nat_of_word digit1 * 1000 +``        nat_of_word digit2 * 100 +``        nat_of_word digit3 * 10 +``        nat_of_word digit4 * 1 >= 557.``
• ###### File addition: dragster.v (----------)
[4.20]
``Require Import word memory.``Definition dragster_rom : memory 11 (word 8) := from_bytes 11 word_of_nat``    0x78 0xd8 0xa2 0x00 0xa9 0x00 0x95 0x00  0x9a 0xe8 0xd0 0xfa 0xa5 0x82 0xd0 0x03``    0x4c 0xfd 0xf2 0x20 0xd3 0xf6 0xa2 0x06  0xbd 0xca 0xf6 0x45 0x84 0x25 0x85 0x95``    0x86 0xca 0x10 0xf4 0xea 0xea 0xea 0xea  0xea 0xa6 0x8f 0x38 0xa0 0x00 0xb5 0xba``    0xc8 0xe9 0x03 0x10 0xfb 0x88 0x38 0x98  0xa0 0x00 0xc8 0xe9 0x05 0x10 0xfb 0x88``    0x94 0xbc 0x69 0x05 0x95 0xbe 0xad 0x84  0x02 0xd0 0xfb 0x85 0x02 0x85 0x01 0x85``    0xaa 0xa6 0xaa 0xb5 0xba 0x20 0xe5 0xf4  0xa6 0xaa 0xa9 0x03 0x85 0x04 0x85 0x05``    0xb4 0xc4 0xb9 0xc0 0xf6 0x85 0x02 0x85  0x0d 0x85 0x0f 0xb9 0xc4 0xf6 0x85 0x0e``    0x20 0xd0 0xf7 0xa0 0x05 0x85 0x02 0x88  0x10 0xfb 0xa6 0xaa 0xb4 0xbc 0x88 0x10``    0xfd 0xb4 0xbe 0xc0 0x04 0xf0 0x0e 0xc0  0x03 0xf0 0x0d 0xc0 0x02 0xf0 0x0c 0xc0``    0x01 0xf0 0x0b 0xd0 0x0b 0xea 0xa5 0xd8  0xea 0xa5 0xd8 0xea 0xa5 0xd8 0xa5 0xd8``    0xea 0xea 0xa9 0x16 0x85 0x8e 0x18 0xa4  0x8e 0xb1 0x90 0x85 0x1b 0xb1 0x92 0x85``    0x1c 0xb1 0x94 0x85 0x1b 0xb1 0x9a 0x85  0xd8 0xb1 0x98 0xaa 0xb1 0x96 0xa4 0xd8``    0x85 0x1c 0x86 0x1b 0x84 0x1c 0x85 0x1b  0xa5 0xd8 0xea 0xa5 0x8e 0x4a 0x4a 0x4a``    0xa8 0xb9 0xd0 0xf6 0x85 0x0d 0x85 0x0e  0x85 0x0f 0xa4 0x8e 0xb1 0x90 0x85 0x1b``    0xb1 0x92 0x85 0x1c 0xb1 0x94 0x85 0x1b  0xb1 0x96 0xa4 0xd8 0x85 0x1c 0x86 0x1b``    0x84 0x1c 0x85 0x1b 0xea 0xea 0xea 0xc6  0x8e 0x10 0xac 0xa2 0x01 0xa0 0x00 0x84``    0x1b 0x84 0x1c 0xca 0x10 0xf7 0x86 0x02  0xa5 0x88 0x85 0x09 0xa2 0x09 0x85 0x02``    0xa9 0xf7 0x95 0x90 0xca 0xca 0x10 0xf6  0xa5 0x89 0x85 0x09 0xa9 0x02 0x85 0x0a``    0xa5 0x8a 0x85 0x06 0xa5 0x8b 0x85 0x07  0xa6 0xaa 0xa0 0x07 0x85 0x02 0xb5 0x9c``    0x85 0x0d 0xb5 0x9e 0x85 0x0e 0xb5 0xa0  0x85 0x0f 0xa5 0xd8 0xb5 0xa2 0x85 0x0d``    0xa5 0xd8 0xb5 0xa4 0x85 0x0e 0xa5 0xd8  0xb5 0xa6 0x85 0x0f 0x88 0x10 0xdd 0x85``    0x02 0xc8 0x84 0x0d 0x84 0x0e 0x84 0x0f  0xa9 0x10 0x85 0x0a 0xa5 0x86 0x85 0x06``    0x85 0x07 0xa9 0x0f 0x20 0xe5 0xf4 0xa9  0x06 0x85 0x04 0xa9 0x01 0x85 0x05 0xa6``    0xaa 0xb4 0xd4 0x85 0x02 0xf0 0x0a 0x20  0x3b 0xf5 0x85 0x02 0x85 0x02 0x4c 0x09``    0xf2 0xa5 0x8c 0x85 0x08 0xa6 0xaa 0xa0  0x68 0xb5 0xb3 0xf0 0x08 0xa0 0x50 0x29``    0xf0 0xf0 0x02 0x4a 0xa8 0x85 0x02 0x98  0x85 0x90 0xb5 0xb3 0x29 0x0f 0x0a 0x0a``    0x0a 0x85 0x92 0xb5 0xb5 0x29 0xf0 0x4a  0x85 0x96 0xa5 0x8d 0xf0 0x08 0x29 0xf0``    0x4a 0x69 0x08 0x4c 0xbd 0xf1 0xb5 0xb5  0x29 0x0f 0x0a 0x0a 0x0a 0x85 0x94 0xa9``    0x0c 0xb4 0xcc 0x30 0x05 0x98 0xd0 0x02  0xa9 0x0b 0x0a 0x0a 0x0a 0x85 0x98 0xa9``    0x07 0xb4 0xb5 0xc0 0xaa 0xd0 0x02 0xa9  0x0a 0xaa 0xa0 0x07 0x85 0x02 0xea 0xb1``    0x92 0x85 0x1c 0xb1 0x90 0x85 0x1b 0xb1  0x96 0x85 0x1c 0xb1 0x94 0x85 0x1b 0x85``    0x1c 0xb1 0x98 0x85 0x1b 0x85 0x1c 0xbd  0x6a 0xf5 0x85 0x1f 0xca 0x88 0x10 0xdc``    0xc8 0x84 0x1b 0x84 0x1c 0x84 0x1b 0x84  0x1f 0xa5 0x88 0x85 0x08 0xe6 0xaa 0xa5``    0xaa 0x4a 0x90 0x03 0x4c 0x51 0xf0 0xa9  0x0f 0x20 0xe5 0xf4 0xa0 0x39 0x20 0x3b``    0xf5 0xa9 0x21 0x8d 0x96 0x02 0xa5 0x81  0x29 0x01 0xaa 0x86 0x8f 0xa0 0x00 0xa5``    0xb9 0x30 0x4c 0xb5 0xd2 0xd0 0x48 0xb5  0xd0 0xf0 0x07 0xa0 0x08 0xd6 0xd0 0x4c``    0x4e 0xf2 0xa5 0x8d 0xf0 0x11 0x29 0x0f  0xd0 0x0d 0xa0 0x0c 0xa9 0x18 0x95 0x19``    0x94 0x17 0x94 0x15 0x4c 0x85 0xf2 0xb5  0xce 0xd0 0x24 0xa5 0x81 0x29 0x02 0xf0``    0x10 0xa0 0x09 0xa9 0x01 0x95 0x17 0xb5  0xc0 0xf0 0x06 0xb5 0xc8 0x15 0xca 0xd0``    0x0e 0xb5 0xa8 0xc9 0x20 0x90 0x02 0xa9  0x1f 0x49 0x1f 0x95 0x17 0xa0 0x03 0x94``    0x15 0xb5 0xb1 0x95 0x19 0xad 0x84 0x02  0xd0 0xfb 0xa0 0x82 0x84 0x02 0x84 0x01``    0x84 0x00 0x84 0x02 0x84 0x02 0x84 0x02  0x85 0x00 0xe6 0x81 0xd0 0x07 0xe6 0xb9``    0xd0 0x03 0x38 0x66 0xb9 0xa0 0xff 0xad  0x82 0x02 0x29 0x08 0xd0 0x02 0xa0 0x0f``    0xa9 0x00 0x24 0xb9 0x10 0x07 0x98 0x29  0xf7 0xa8 0xa5 0xb9 0x0a 0x85 0x84 0x84``    0x85 0xa9 0x19 0x85 0x02 0x8d 0x96 0x02  0xad 0x80 0x02 0xa8 0x29 0x0f 0x85 0xae``    0x98 0x4a 0x4a 0x4a 0x4a 0x85 0xad 0xa5  0xa8 0x05 0xa9 0xd0 0x06 0xb5 0xad 0xc9``    0x07 0xf0 0x06 0xad 0x82 0x02 0x4a 0xb0  0x05 0xa2 0xb9 0x4c 0x04 0xf0 0xa0 0x00``    0x4a 0xb0 0x29 0xa5 0xb0 0xf0 0x04 0xc6  0xb0 0x10 0x23 0xe6 0x80 0xa5 0x80 0x29``    0x01 0x85 0x80 0x85 0xb9 0xa8 0xc8 0x84  0xcc 0x20 0xd3 0xf6 0xa9 0x0a 0x85 0xcd``    0xa9 0x00 0x85 0x8d 0x85 0xd4 0xa0 0x1e  0x84 0xd2 0x84 0xd3 0x84 0xb0 0xa5 0x8d``    0xf0 0x0c 0xc6 0x8d 0xd0 0x08 0xa2 0x05  0x4a 0x95 0xb3 0xca 0x10 0xfb 0xa6 0x8f``    0xa5 0xb9 0x30 0x0d 0xb5 0xd2 0xf0 0x0c  0xa0 0x01 0x94 0xd2 0x88 0x94 0xa8 0x94``    0xc8 0x4c 0xa4 0xf4 0xa5 0x8d 0xd0 0x1f  0xf8 0x18 0xb5 0xb7 0x69 0x34 0x95 0xb7``    0xb5 0xb5 0x69 0x03 0x95 0xb5 0xb5 0xb3  0x69 0x00 0x95 0xb3 0xd8 0x90 0x08 0xa9``    0x99 0x95 0xb3 0x95 0xb5 0xd0 0xd1 0xb5  0xc0 0xf0 0x35 0x18 0x75 0xc2 0x95 0xc2``    0x90 0x02 0xf6 0xba 0xb5 0xc0 0x2a 0x2a  0x2a 0x29 0x03 0xa8 0xb9 0xc8 0xf6 0x25``    0x81 0xd0 0x0f 0xf6 0xc4 0x18 0xb5 0xc6  0x69 0x17 0xc9 0x2f 0x90 0x02 0xa9 0x00``    0x95 0xc6 0xb5 0xc4 0x29 0x03 0x95 0xc4  0xb5 0xba 0xc9 0x60 0x90 0x02 0xd0 0xc5``    0xb5 0xce 0xd0 0x2b 0xa5 0x81 0xb4 0xcc  0x10 0x02 0xa0 0x00 0x39 0xf6 0xf6 0xd0``    0x50 0xb5 0x0c 0x30 0x1c 0xb5 0xca 0xf0  0x06 0xa5 0x81 0x29 0x02 0xf0 0x12 0x18``    0xb5 0xa8 0x79 0xfb 0xf6 0x95 0xa8 0xa9  0x0c 0x95 0xb1 0x85 0xb9 0xd0 0x14 0xd0``    0x6a 0x38 0xb5 0xa8 0xf9 0xfb 0xf6 0x95  0xa8 0xd6 0xb1 0xa9 0x04 0xd5 0xb1 0x90``    0x02 0x95 0xb1 0xb5 0xa8 0x10 0x02 0xa9  0x00 0xc9 0x20 0x90 0x12 0xa9 0x0f 0x95``    0xd0 0xa9 0x01 0x95 0xd4 0xa9 0x04 0x95  0xab 0xa9 0x1a 0x95 0xce 0xa9 0x00 0x95``    0xa8 0xa9 0x00 0x95 0xc8 0x98 0xf0 0x33  0xb5 0xa8 0xc9 0x14 0x88 0xf0 0x04 0x2a``    0x4c 0x0c 0xf4 0x85 0xd8 0xd5 0xc0 0xf0  0x22 0xb0 0x09 0xb5 0xc0 0xf0 0x1c 0xd6``    0xc0 0x4c 0x3b 0xf4 0xa5 0xd8 0x38 0xf5  0xc0 0xf6 0xc0 0xf6 0xc0 0xc9 0x10 0x90``    0x0a 0xb5 0xce 0xd0 0x06 0xa9 0x17 0x95  0xc8 0xd6 0xa8 0xb5 0xad 0x29 0x04 0xd5``    0xd6 0x95 0xd6 0xf0 0x21 0xc9 0x00 0xd0  0x07 0x16 0xcc 0x38 0x76 0xcc 0x30 0x16``    0xa5 0x8d 0xf0 0x04 0xa9 0x1d 0x95 0xd4  0xf6 0xcc 0xb5 0xcc 0x29 0x7f 0xc9 0x04``    0x90 0x02 0xa9 0x04 0x95 0xcc 0xa5 0x80  0x4a 0x90 0x39 0xb5 0xce 0xd0 0x35 0xb5``    0xc0 0xf0 0x31 0xa5 0x81 0x29 0x06 0xd0  0x2b 0xb5 0xad 0x4a 0xb0 0x02 0xd6 0xab``    0x4a 0xb0 0x02 0xf6 0xab 0xa5 0x82 0x10  0x04 0xf6 0xab 0xf6 0xab 0xd6 0xab 0xa9``    0x00 0x95 0xca 0xb4 0xab 0x10 0x03 0xa8  0xf6 0xca 0xc0 0x08 0x90 0x04 0xa0 0x08``    0xf6 0xca 0x94 0xab 0xa5 0x82 0x0a 0x0a  0x0a 0x45 0x82 0x0a 0x26 0x82 0x8a 0x09``    0x0a 0xa8 0xa9 0x00 0x99 0x9c 0x00 0x88  0x88 0x10 0xf9 0xb4 0xa8 0xc0 0x13 0x90``    0x10 0x98 0xe9 0x13 0xa8 0xa9 0xff 0x95  0x9c 0x95 0x9e 0x95 0xa0 0x8a 0x09 0x06``    0xaa 0x88 0x30 0x0e 0xb5 0x9c 0x09 0x08  0x0a 0x95 0x9c 0x76 0x9e 0x36 0xa0 0x4c``    0xd1 0xf4 0x4c 0x16 0xf0 0x85 0xd9 0xa2  0x00 0x85 0x2b 0xa4 0x8c 0x84 0x02 0x84``    0x09 0x18 0x69 0x2e 0xa8 0x29 0x0f 0x85  0xd8 0x98 0x4a 0x4a 0x4a 0x4a 0xa8 0x18``    0x65 0xd8 0xc9 0x0f 0x90 0x03 0xe9 0x0f  0xc8 0x49 0x07 0x0a 0x0a 0x0a 0x0a 0x95``    0x20 0x85 0x02 0x88 0x10 0xfd 0x95 0x10  0xa5 0xd9 0x18 0x69 0x08 0xe8 0xe0 0x02``    0x90 0xc9 0x85 0x02 0x85 0x2a 0xa5 0x89  0x85 0x02 0x85 0x09 0x60 0xb9 0xc5 0xf7``    0x99 0x91 0x00 0x88 0x88 0x30 0x03 0x4c  0xd2 0xf7 0x60 0xa9 0x01 0x85 0x04 0x85``    0x02 0xa2 0x06 0x85 0x02 0xc8 0xb9 0x6e  0xf7 0x85 0x1b 0xb9 0x75 0xf7 0x85 0x1c``    0xb9 0x7c 0xf7 0x85 0x1b 0xb9 0x83 0xf7  0xea 0x85 0x1c 0x85 0x1b 0xca 0x10 0xe3``    0xe8 0x86 0x1b 0x86 0x1c 0x86 0x1b 0x85  0x02 0x60 0x02 0x02 0x02 0x02 0x00 0x00``    0x00 0x00 0x00 0x00 0x00 0x00 0x07 0x1f  0x3f 0x7e 0x7d 0xfd 0xef 0xf7 0xfe 0x7e``    0x7d 0x3f 0x1f 0x07 0x01 0x00 0x00 0x00  0x00 0x00 0x00 0x00 0x00 0x07 0x1f 0x3f``    0x77 0x77 0xfb 0xff 0xff 0xfb 0x77 0x7f  0x3f 0x1f 0x07 0x01 0x00 0x00 0x00 0x00``    0x00 0x00 0x00 0x00 0x07 0x1f 0x3f 0x7f  0x6f 0xf6 0xfb 0xff 0xfd 0x7b 0x77 0x3f``    0x1f 0x07 0x01 0x00 0x00 0x00 0x00 0x00  0x00 0x00 0x00 0x80 0xe0 0xf7 0xfb 0xfb``    0xff 0xbf 0xdf 0xfd 0xfa 0xfa 0xf6 0xec  0xb8 0xe0 0x00 0x00 0x00 0x00 0x00 0x00``    0x00 0x00 0x80 0xe0 0xf7 0xfb 0xbb 0x7f  0xff 0xff 0x7d 0xba 0xba 0xf6 0xec 0xb8``    0xe0 0x00 0x00 0x00 0x00 0x00 0x00 0x00  0x00 0x80 0xe0 0xf7 0xbb 0x7b 0xff 0xff``    0x7f 0xbd 0xda 0xfa 0xf6 0xec 0xb8 0xe0  0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00``    0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00  0x44 0x22 0xee 0xf7 0xfb 0xfd 0xff 0xef``    0xe8 0xf8 0x00 0x00 0x00 0x00 0x00 0x00  0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00``    0x00 0x20 0x92 0xe1 0xf6 0xfb 0xfb 0xff  0xef 0xe0 0x00 0x00 0x00 0x00 0x00 0x00``    0x00 0x00 0x00 0x00 0x00 0x00 0x40 0x20  0xef 0x74 0xba 0xdd 0xff 0xff 0x00 0x00``    0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00  0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00``    0x00 0x20 0x10 0x60 0xb6 0xbb 0xfa 0xff  0x0f 0x00 0x00 0x00 0x00 0x00 0x00 0x00``    0x00 0x00 0x00 0x00 0x00 0x00 0xff 0x00  0xff 0x80 0x80 0x80 0x00 0x00 0x00 0x00``    0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00  0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00``    0x00 0x00 0x00 0xf0 0x0e 0xe1 0x1f 0x00  0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00``    0x00 0x00 0x30 0x78 0xfc 0xfe 0xfa 0x34  0x18 0x00 0x00 0x00 0x00 0x00 0x00 0x00``    0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00  0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00``    0x00 0x60 0xf0 0xf8 0xfc 0xf4 0x68 0x30  0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00``    0x77 0xbb 0xdd 0xee 0xee 0xdd 0xbb 0x77  0x06 0x02 0x00 0x00 0x88 0xcc 0xd8 0x46``    0x00 0x00 0xff 0xa9 0x9f 0x85 0x8d 0xa2  0x01 0xa9 0x01 0x95 0x25 0x85 0x82 0xa9``    0xaa 0x95 0xb3 0x95 0xb5 0xa9 0x04 0x95  0xab 0x95 0xd6 0x95 0xb1 0xca 0x10 0xe9``    0xaa 0xa9 0x23 0x4c 0xe9 0xf4 0x00 0x00  0x02 0x06 0x0e 0x03 0x01 0x01 0x01 0x01``    0x3c 0x66 0x66 0x66 0x66 0x66 0x66 0x3c  0x7e 0x18 0x18 0x18 0x18 0x78 0x38 0x18``    0x7e 0x60 0x60 0x3c 0x06 0x06 0x46 0x3c  0x3c 0x46 0x06 0x0c 0x0c 0x06 0x46 0x3c``    0x0c 0x0c 0x0c 0x7e 0x4c 0x2c 0x1c 0x0c  0x7c 0x46 0x06 0x06 0x7c 0x60 0x60 0x7e``    0x3c 0x66 0x66 0x66 0x7c 0x60 0x62 0x3c  0x18 0x18 0x18 0x18 0x0c 0x06 0x42 0x7e``    0x3c 0x66 0x66 0x3c 0x3c 0x66 0x66 0x3c  0x3c 0x46 0x06 0x3e 0x66 0x66 0x66 0x3c``    0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00  0xc3 0xc7 0xcf 0xdf 0xfb 0xf3 0xe3 0xc3``    0x7e 0xc3 0xc0 0xc0 0xc0 0xc0 0xc3 0x7e  0x7e 0xc3 0xc3 0xcf 0xc0 0xc0 0xc3 0x7e``    0xf2 0x4a 0x4a 0x72 0x4a 0x4a 0xf3 0x0e  0x11 0x11 0x11 0x11 0x11 0xce 0x45 0x45``    0x45 0x45 0x55 0x6d 0x45 0x10 0x90 0x50  0x30 0x10 0x10 0x10 0xf8 0x81 0x82 0xe2``    0x83 0x82 0xfa 0x8f 0x48 0x28 0x2f 0xea  0x29 0x28 0x21 0xa1 0xa0 0x20 0x20 0x20``    0xbe 0x10 0x10 0xa0 0x40 0x40 0x40 0x40  0x0f 0x41 0xed 0xa9 0xe9 0xa9 0xad 0xf0``    0x11 0x53 0x56 0x5c 0x58 0x50 0xfe 0x80  0x3a 0xa2 0xba 0x8a 0xba 0x00 0x00 0xe9``    0xad 0xaf 0xab 0xe9 0x6e 0xf5 0xb3 0xf5  0x00 0xf6 0x2e 0xf6 0x5c 0xf6 0x8a 0xf6``    0xa0 0x0a 0xb9 0xc4 0xf7 0x18 0x75 0xab  0xc0 0x04 0x90 0x15 0x18 0x75 0xc8 0xc0``    0x08 0xb0 0x11 0x85 0xd8 0xb5 0xce 0xf0  0x03 0x79 0xf2 0xf6 0x65 0xd8 0x4c 0xf4``    0xf7 0x18 0x75 0xc6 0x99 0x90 0x00 0x4c  0x2d 0xf5 0x00 0x00 0x00 0xf0 0x00 0x00``.``
• ###### Insertion in _CoqProject at line 8 [4.58]
[3.8635]
[4.81]
``theories/dragster.v``theories/goal.v``
• ###### Replacement in README.md at line 5 [5.34]
B:BD[5.217] → [5.217:1238]
``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.``
[5.217]
[2.28984]
``So far, I have implemented a specification of the Atari 2600 console, and used it to state the theorem. Now I just have to prove it!``Of course, that's easier said than done.``