State the theorem!
Created by finegeometer on March 22, 2022
NJNJOBP4TDPPOBAQ52CAXIY3HC6CIEDBYT3HZG4KU36HW3KWZDVAC Dependencies
In channels
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)) inlet '(digit3, digit4) := split (m := 4) (n := 4)(get (RAM (Peripherals s)) (word_of_nat 0x35)) innat_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_nat0x78 0xd8 0xa2 0x00 0xa9 0x00 0x95 0x00 0x9a 0xe8 0xd0 0xfa 0xa5 0x82 0xd0 0x030x4c 0xfd 0xf2 0x20 0xd3 0xf6 0xa2 0x06 0xbd 0xca 0xf6 0x45 0x84 0x25 0x85 0x950x86 0xca 0x10 0xf4 0xea 0xea 0xea 0xea 0xea 0xa6 0x8f 0x38 0xa0 0x00 0xb5 0xba0xc8 0xe9 0x03 0x10 0xfb 0x88 0x38 0x98 0xa0 0x00 0xc8 0xe9 0x05 0x10 0xfb 0x880x94 0xbc 0x69 0x05 0x95 0xbe 0xad 0x84 0x02 0xd0 0xfb 0x85 0x02 0x85 0x01 0x850xaa 0xa6 0xaa 0xb5 0xba 0x20 0xe5 0xf4 0xa6 0xaa 0xa9 0x03 0x85 0x04 0x85 0x050xb4 0xc4 0xb9 0xc0 0xf6 0x85 0x02 0x85 0x0d 0x85 0x0f 0xb9 0xc4 0xf6 0x85 0x0e0x20 0xd0 0xf7 0xa0 0x05 0x85 0x02 0x88 0x10 0xfb 0xa6 0xaa 0xb4 0xbc 0x88 0x100xfd 0xb4 0xbe 0xc0 0x04 0xf0 0x0e 0xc0 0x03 0xf0 0x0d 0xc0 0x02 0xf0 0x0c 0xc00x01 0xf0 0x0b 0xd0 0x0b 0xea 0xa5 0xd8 0xea 0xa5 0xd8 0xea 0xa5 0xd8 0xa5 0xd80xea 0xea 0xa9 0x16 0x85 0x8e 0x18 0xa4 0x8e 0xb1 0x90 0x85 0x1b 0xb1 0x92 0x850x1c 0xb1 0x94 0x85 0x1b 0xb1 0x9a 0x85 0xd8 0xb1 0x98 0xaa 0xb1 0x96 0xa4 0xd80x85 0x1c 0x86 0x1b 0x84 0x1c 0x85 0x1b 0xa5 0xd8 0xea 0xa5 0x8e 0x4a 0x4a 0x4a0xa8 0xb9 0xd0 0xf6 0x85 0x0d 0x85 0x0e 0x85 0x0f 0xa4 0x8e 0xb1 0x90 0x85 0x1b0xb1 0x92 0x85 0x1c 0xb1 0x94 0x85 0x1b 0xb1 0x96 0xa4 0xd8 0x85 0x1c 0x86 0x1b0x84 0x1c 0x85 0x1b 0xea 0xea 0xea 0xc6 0x8e 0x10 0xac 0xa2 0x01 0xa0 0x00 0x840x1b 0x84 0x1c 0xca 0x10 0xf7 0x86 0x02 0xa5 0x88 0x85 0x09 0xa2 0x09 0x85 0x020xa9 0xf7 0x95 0x90 0xca 0xca 0x10 0xf6 0xa5 0x89 0x85 0x09 0xa9 0x02 0x85 0x0a0xa5 0x8a 0x85 0x06 0xa5 0x8b 0x85 0x07 0xa6 0xaa 0xa0 0x07 0x85 0x02 0xb5 0x9c0x85 0x0d 0xb5 0x9e 0x85 0x0e 0xb5 0xa0 0x85 0x0f 0xa5 0xd8 0xb5 0xa2 0x85 0x0d0xa5 0xd8 0xb5 0xa4 0x85 0x0e 0xa5 0xd8 0xb5 0xa6 0x85 0x0f 0x88 0x10 0xdd 0x850x02 0xc8 0x84 0x0d 0x84 0x0e 0x84 0x0f 0xa9 0x10 0x85 0x0a 0xa5 0x86 0x85 0x060x85 0x07 0xa9 0x0f 0x20 0xe5 0xf4 0xa9 0x06 0x85 0x04 0xa9 0x01 0x85 0x05 0xa60xaa 0xb4 0xd4 0x85 0x02 0xf0 0x0a 0x20 0x3b 0xf5 0x85 0x02 0x85 0x02 0x4c 0x090xf2 0xa5 0x8c 0x85 0x08 0xa6 0xaa 0xa0 0x68 0xb5 0xb3 0xf0 0x08 0xa0 0x50 0x290xf0 0xf0 0x02 0x4a 0xa8 0x85 0x02 0x98 0x85 0x90 0xb5 0xb3 0x29 0x0f 0x0a 0x0a0x0a 0x85 0x92 0xb5 0xb5 0x29 0xf0 0x4a 0x85 0x96 0xa5 0x8d 0xf0 0x08 0x29 0xf00x4a 0x69 0x08 0x4c 0xbd 0xf1 0xb5 0xb5 0x29 0x0f 0x0a 0x0a 0x0a 0x85 0x94 0xa90x0c 0xb4 0xcc 0x30 0x05 0x98 0xd0 0x02 0xa9 0x0b 0x0a 0x0a 0x0a 0x85 0x98 0xa90x07 0xb4 0xb5 0xc0 0xaa 0xd0 0x02 0xa9 0x0a 0xaa 0xa0 0x07 0x85 0x02 0xea 0xb10x92 0x85 0x1c 0xb1 0x90 0x85 0x1b 0xb1 0x96 0x85 0x1c 0xb1 0x94 0x85 0x1b 0x850x1c 0xb1 0x98 0x85 0x1b 0x85 0x1c 0xbd 0x6a 0xf5 0x85 0x1f 0xca 0x88 0x10 0xdc0xc8 0x84 0x1b 0x84 0x1c 0x84 0x1b 0x84 0x1f 0xa5 0x88 0x85 0x08 0xe6 0xaa 0xa50xaa 0x4a 0x90 0x03 0x4c 0x51 0xf0 0xa9 0x0f 0x20 0xe5 0xf4 0xa0 0x39 0x20 0x3b0xf5 0xa9 0x21 0x8d 0x96 0x02 0xa5 0x81 0x29 0x01 0xaa 0x86 0x8f 0xa0 0x00 0xa50xb9 0x30 0x4c 0xb5 0xd2 0xd0 0x48 0xb5 0xd0 0xf0 0x07 0xa0 0x08 0xd6 0xd0 0x4c0x4e 0xf2 0xa5 0x8d 0xf0 0x11 0x29 0x0f 0xd0 0x0d 0xa0 0x0c 0xa9 0x18 0x95 0x190x94 0x17 0x94 0x15 0x4c 0x85 0xf2 0xb5 0xce 0xd0 0x24 0xa5 0x81 0x29 0x02 0xf00x10 0xa0 0x09 0xa9 0x01 0x95 0x17 0xb5 0xc0 0xf0 0x06 0xb5 0xc8 0x15 0xca 0xd00x0e 0xb5 0xa8 0xc9 0x20 0x90 0x02 0xa9 0x1f 0x49 0x1f 0x95 0x17 0xa0 0x03 0x940x15 0xb5 0xb1 0x95 0x19 0xad 0x84 0x02 0xd0 0xfb 0xa0 0x82 0x84 0x02 0x84 0x010x84 0x00 0x84 0x02 0x84 0x02 0x84 0x02 0x85 0x00 0xe6 0x81 0xd0 0x07 0xe6 0xb90xd0 0x03 0x38 0x66 0xb9 0xa0 0xff 0xad 0x82 0x02 0x29 0x08 0xd0 0x02 0xa0 0x0f0xa9 0x00 0x24 0xb9 0x10 0x07 0x98 0x29 0xf7 0xa8 0xa5 0xb9 0x0a 0x85 0x84 0x840x85 0xa9 0x19 0x85 0x02 0x8d 0x96 0x02 0xad 0x80 0x02 0xa8 0x29 0x0f 0x85 0xae0x98 0x4a 0x4a 0x4a 0x4a 0x85 0xad 0xa5 0xa8 0x05 0xa9 0xd0 0x06 0xb5 0xad 0xc90x07 0xf0 0x06 0xad 0x82 0x02 0x4a 0xb0 0x05 0xa2 0xb9 0x4c 0x04 0xf0 0xa0 0x000x4a 0xb0 0x29 0xa5 0xb0 0xf0 0x04 0xc6 0xb0 0x10 0x23 0xe6 0x80 0xa5 0x80 0x290x01 0x85 0x80 0x85 0xb9 0xa8 0xc8 0x84 0xcc 0x20 0xd3 0xf6 0xa9 0x0a 0x85 0xcd0xa9 0x00 0x85 0x8d 0x85 0xd4 0xa0 0x1e 0x84 0xd2 0x84 0xd3 0x84 0xb0 0xa5 0x8d0xf0 0x0c 0xc6 0x8d 0xd0 0x08 0xa2 0x05 0x4a 0x95 0xb3 0xca 0x10 0xfb 0xa6 0x8f0xa5 0xb9 0x30 0x0d 0xb5 0xd2 0xf0 0x0c 0xa0 0x01 0x94 0xd2 0x88 0x94 0xa8 0x940xc8 0x4c 0xa4 0xf4 0xa5 0x8d 0xd0 0x1f 0xf8 0x18 0xb5 0xb7 0x69 0x34 0x95 0xb70xb5 0xb5 0x69 0x03 0x95 0xb5 0xb5 0xb3 0x69 0x00 0x95 0xb3 0xd8 0x90 0x08 0xa90x99 0x95 0xb3 0x95 0xb5 0xd0 0xd1 0xb5 0xc0 0xf0 0x35 0x18 0x75 0xc2 0x95 0xc20x90 0x02 0xf6 0xba 0xb5 0xc0 0x2a 0x2a 0x2a 0x29 0x03 0xa8 0xb9 0xc8 0xf6 0x250x81 0xd0 0x0f 0xf6 0xc4 0x18 0xb5 0xc6 0x69 0x17 0xc9 0x2f 0x90 0x02 0xa9 0x000x95 0xc6 0xb5 0xc4 0x29 0x03 0x95 0xc4 0xb5 0xba 0xc9 0x60 0x90 0x02 0xd0 0xc50xb5 0xce 0xd0 0x2b 0xa5 0x81 0xb4 0xcc 0x10 0x02 0xa0 0x00 0x39 0xf6 0xf6 0xd00x50 0xb5 0x0c 0x30 0x1c 0xb5 0xca 0xf0 0x06 0xa5 0x81 0x29 0x02 0xf0 0x12 0x180xb5 0xa8 0x79 0xfb 0xf6 0x95 0xa8 0xa9 0x0c 0x95 0xb1 0x85 0xb9 0xd0 0x14 0xd00x6a 0x38 0xb5 0xa8 0xf9 0xfb 0xf6 0x95 0xa8 0xd6 0xb1 0xa9 0x04 0xd5 0xb1 0x900x02 0x95 0xb1 0xb5 0xa8 0x10 0x02 0xa9 0x00 0xc9 0x20 0x90 0x12 0xa9 0x0f 0x950xd0 0xa9 0x01 0x95 0xd4 0xa9 0x04 0x95 0xab 0xa9 0x1a 0x95 0xce 0xa9 0x00 0x950xa8 0xa9 0x00 0x95 0xc8 0x98 0xf0 0x33 0xb5 0xa8 0xc9 0x14 0x88 0xf0 0x04 0x2a0x4c 0x0c 0xf4 0x85 0xd8 0xd5 0xc0 0xf0 0x22 0xb0 0x09 0xb5 0xc0 0xf0 0x1c 0xd60xc0 0x4c 0x3b 0xf4 0xa5 0xd8 0x38 0xf5 0xc0 0xf6 0xc0 0xf6 0xc0 0xc9 0x10 0x900x0a 0xb5 0xce 0xd0 0x06 0xa9 0x17 0x95 0xc8 0xd6 0xa8 0xb5 0xad 0x29 0x04 0xd50xd6 0x95 0xd6 0xf0 0x21 0xc9 0x00 0xd0 0x07 0x16 0xcc 0x38 0x76 0xcc 0x30 0x160xa5 0x8d 0xf0 0x04 0xa9 0x1d 0x95 0xd4 0xf6 0xcc 0xb5 0xcc 0x29 0x7f 0xc9 0x040x90 0x02 0xa9 0x04 0x95 0xcc 0xa5 0x80 0x4a 0x90 0x39 0xb5 0xce 0xd0 0x35 0xb50xc0 0xf0 0x31 0xa5 0x81 0x29 0x06 0xd0 0x2b 0xb5 0xad 0x4a 0xb0 0x02 0xd6 0xab0x4a 0xb0 0x02 0xf6 0xab 0xa5 0x82 0x10 0x04 0xf6 0xab 0xf6 0xab 0xd6 0xab 0xa90x00 0x95 0xca 0xb4 0xab 0x10 0x03 0xa8 0xf6 0xca 0xc0 0x08 0x90 0x04 0xa0 0x080xf6 0xca 0x94 0xab 0xa5 0x82 0x0a 0x0a 0x0a 0x45 0x82 0x0a 0x26 0x82 0x8a 0x090x0a 0xa8 0xa9 0x00 0x99 0x9c 0x00 0x88 0x88 0x10 0xf9 0xb4 0xa8 0xc0 0x13 0x900x10 0x98 0xe9 0x13 0xa8 0xa9 0xff 0x95 0x9c 0x95 0x9e 0x95 0xa0 0x8a 0x09 0x060xaa 0x88 0x30 0x0e 0xb5 0x9c 0x09 0x08 0x0a 0x95 0x9c 0x76 0x9e 0x36 0xa0 0x4c0xd1 0xf4 0x4c 0x16 0xf0 0x85 0xd9 0xa2 0x00 0x85 0x2b 0xa4 0x8c 0x84 0x02 0x840x09 0x18 0x69 0x2e 0xa8 0x29 0x0f 0x85 0xd8 0x98 0x4a 0x4a 0x4a 0x4a 0xa8 0x180x65 0xd8 0xc9 0x0f 0x90 0x03 0xe9 0x0f 0xc8 0x49 0x07 0x0a 0x0a 0x0a 0x0a 0x950x20 0x85 0x02 0x88 0x10 0xfd 0x95 0x10 0xa5 0xd9 0x18 0x69 0x08 0xe8 0xe0 0x020x90 0xc9 0x85 0x02 0x85 0x2a 0xa5 0x89 0x85 0x02 0x85 0x09 0x60 0xb9 0xc5 0xf70x99 0x91 0x00 0x88 0x88 0x30 0x03 0x4c 0xd2 0xf7 0x60 0xa9 0x01 0x85 0x04 0x850x02 0xa2 0x06 0x85 0x02 0xc8 0xb9 0x6e 0xf7 0x85 0x1b 0xb9 0x75 0xf7 0x85 0x1c0xb9 0x7c 0xf7 0x85 0x1b 0xb9 0x83 0xf7 0xea 0x85 0x1c 0x85 0x1b 0xca 0x10 0xe30xe8 0x86 0x1b 0x86 0x1c 0x86 0x1b 0x85 0x02 0x60 0x02 0x02 0x02 0x02 0x00 0x000x00 0x00 0x00 0x00 0x00 0x00 0x07 0x1f 0x3f 0x7e 0x7d 0xfd 0xef 0xf7 0xfe 0x7e0x7d 0x3f 0x1f 0x07 0x01 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x07 0x1f 0x3f0x77 0x77 0xfb 0xff 0xff 0xfb 0x77 0x7f 0x3f 0x1f 0x07 0x01 0x00 0x00 0x00 0x000x00 0x00 0x00 0x00 0x07 0x1f 0x3f 0x7f 0x6f 0xf6 0xfb 0xff 0xfd 0x7b 0x77 0x3f0x1f 0x07 0x01 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x80 0xe0 0xf7 0xfb 0xfb0xff 0xbf 0xdf 0xfd 0xfa 0xfa 0xf6 0xec 0xb8 0xe0 0x00 0x00 0x00 0x00 0x00 0x000x00 0x00 0x80 0xe0 0xf7 0xfb 0xbb 0x7f 0xff 0xff 0x7d 0xba 0xba 0xf6 0xec 0xb80xe0 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x80 0xe0 0xf7 0xbb 0x7b 0xff 0xff0x7f 0xbd 0xda 0xfa 0xf6 0xec 0xb8 0xe0 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x000x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x44 0x22 0xee 0xf7 0xfb 0xfd 0xff 0xef0xe8 0xf8 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x000x00 0x20 0x92 0xe1 0xf6 0xfb 0xfb 0xff 0xef 0xe0 0x00 0x00 0x00 0x00 0x00 0x000x00 0x00 0x00 0x00 0x00 0x00 0x40 0x20 0xef 0x74 0xba 0xdd 0xff 0xff 0x00 0x000x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x000x00 0x20 0x10 0x60 0xb6 0xbb 0xfa 0xff 0x0f 0x00 0x00 0x00 0x00 0x00 0x00 0x000x00 0x00 0x00 0x00 0x00 0x00 0xff 0x00 0xff 0x80 0x80 0x80 0x00 0x00 0x00 0x000x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x000x00 0x00 0x00 0xf0 0x0e 0xe1 0x1f 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x000x00 0x00 0x30 0x78 0xfc 0xfe 0xfa 0x34 0x18 0x00 0x00 0x00 0x00 0x00 0x00 0x000x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x000x00 0x60 0xf0 0xf8 0xfc 0xf4 0x68 0x30 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x000x77 0xbb 0xdd 0xee 0xee 0xdd 0xbb 0x77 0x06 0x02 0x00 0x00 0x88 0xcc 0xd8 0x460x00 0x00 0xff 0xa9 0x9f 0x85 0x8d 0xa2 0x01 0xa9 0x01 0x95 0x25 0x85 0x82 0xa90xaa 0x95 0xb3 0x95 0xb5 0xa9 0x04 0x95 0xab 0x95 0xd6 0x95 0xb1 0xca 0x10 0xe90xaa 0xa9 0x23 0x4c 0xe9 0xf4 0x00 0x00 0x02 0x06 0x0e 0x03 0x01 0x01 0x01 0x010x3c 0x66 0x66 0x66 0x66 0x66 0x66 0x3c 0x7e 0x18 0x18 0x18 0x18 0x78 0x38 0x180x7e 0x60 0x60 0x3c 0x06 0x06 0x46 0x3c 0x3c 0x46 0x06 0x0c 0x0c 0x06 0x46 0x3c0x0c 0x0c 0x0c 0x7e 0x4c 0x2c 0x1c 0x0c 0x7c 0x46 0x06 0x06 0x7c 0x60 0x60 0x7e0x3c 0x66 0x66 0x66 0x7c 0x60 0x62 0x3c 0x18 0x18 0x18 0x18 0x0c 0x06 0x42 0x7e0x3c 0x66 0x66 0x3c 0x3c 0x66 0x66 0x3c 0x3c 0x46 0x06 0x3e 0x66 0x66 0x66 0x3c0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0xc3 0xc7 0xcf 0xdf 0xfb 0xf3 0xe3 0xc30x7e 0xc3 0xc0 0xc0 0xc0 0xc0 0xc3 0x7e 0x7e 0xc3 0xc3 0xcf 0xc0 0xc0 0xc3 0x7e0xf2 0x4a 0x4a 0x72 0x4a 0x4a 0xf3 0x0e 0x11 0x11 0x11 0x11 0x11 0xce 0x45 0x450x45 0x45 0x55 0x6d 0x45 0x10 0x90 0x50 0x30 0x10 0x10 0x10 0xf8 0x81 0x82 0xe20x83 0x82 0xfa 0x8f 0x48 0x28 0x2f 0xea 0x29 0x28 0x21 0xa1 0xa0 0x20 0x20 0x200xbe 0x10 0x10 0xa0 0x40 0x40 0x40 0x40 0x0f 0x41 0xed 0xa9 0xe9 0xa9 0xad 0xf00x11 0x53 0x56 0x5c 0x58 0x50 0xfe 0x80 0x3a 0xa2 0xba 0x8a 0xba 0x00 0x00 0xe90xad 0xaf 0xab 0xe9 0x6e 0xf5 0xb3 0xf5 0x00 0xf6 0x2e 0xf6 0x5c 0xf6 0x8a 0xf60xa0 0x0a 0xb9 0xc4 0xf7 0x18 0x75 0xab 0xc0 0x04 0x90 0x15 0x18 0x75 0xc8 0xc00x08 0xb0 0x11 0x85 0xd8 0xb5 0xce 0xf0 0x03 0x79 0xf2 0xf6 0x65 0xd8 0x4c 0xf40xf7 0x18 0x75 0xc6 0x99 0x90 0x00 0x4c 0x2d 0xf5 0x00 0x00 0x00 0xf0 0x00 0x00.Insertion in _CoqProject at line 8 [4.58]
Replacement in README.md at line 5 [5.34]
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.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.