From mathcomp Require Import all_ssreflect.
Require Import word memory nondeterminism.

(* The peripherals attached to the processor in the Atari 2600.
    These present themselves to the processor via memory addresses.
*)

(* There are four kinds of peripheral inside the Atari 2600.
    - ROM
        The Atari has 4096 bytes of read-only memory, used to store the game code.
        These present themselves on addresses `...1 xxxx xxxx xxxx`.
        (A dot means the bit is ignored.)
        I don't know what happens if you try to write to it,
        so I assume anything can happen in that case.
    - RAM
        The Atari has 128 bytes of writable memory, used to store the game state.
        These present themselves on addresses `...0 ..0. 1xxx xxxx`.
    - TIA and PIA
        The Atari has two other peripherals, for stuff like graphics, player input, et cetera.
        I don't understand what these do, so I'll assume they can do anything they want.
        The TIA is on adresses `...0 .... 0.xx xxxx`.
        The PIA is on addresses `...0 ..1. 1..x xxxx`.
*)

Definition ROM := memory 12 (word 8).

Inductive state (rom : ROM) := fromRAM of (memory 7 (word 8)).
Arguments fromRAM {rom}.
Definition RAM {rom} : state rom -> memory 7 (word 8) := fun '(fromRAM ram) => ram.

Lemma RAMK {rom} : cancel RAM (fromRAM (rom := rom)). by case. Qed.
Lemma fromRAMK {rom} : cancel fromRAM (RAM (rom := rom)). done. Qed.

(* If the processor reads from `addr`,
    while the peripherals are in state `s`,
    what answers could it get?
*)
Definition read {rom} (addr : word 16) (s : state rom) : nondet (word 8).
Proof.
    by refine (
        (* ROM *)
        if bit addr (Ordinal (m := 12) _)
        then determined (get rom (split (n := 4) _).1)
        (* TIA *)
        else if ~~ bit addr (Ordinal (m := 7) _)
        then unspecified
        (* PIA *)
        else if bit addr (Ordinal (m := 9) _)
        then unspecified
        (* RAM *)
        else determined (get (RAM s) (split (n := 9) _).1)
    ).
Defined.

(* If the processor writes `w` to `addr`,
    while the peripherals are in state `s`,
    what states could the peripherals end up in?
    (If I don't know, assume they could.)
*)
Definition write {rom} (addr : word 16) (w : word 8) (s : state rom) : nondet (state rom).
Proof.
    by refine (
        (* ROM *)
        if bit addr (Ordinal (m := 12) _)
        then unspecified
        (* TIA *)
        else if ~~ bit addr (Ordinal (m := 7) _)
        then unspecified
        (* PIA *)
        else if bit addr (Ordinal (m := 9) _)
        then unspecified
        (* RAM *)
        else determined (fromRAM (update (RAM s) (fun=>w) (split (n := 9) _).1))
    ).
Defined.