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.