Definition word_eqMixin {n} := CanEqMixin (tuple_of_wordK (n := n)).
    Canonical word_eqType {n} := EqType (word n) word_eqMixin.

    Lemma rew_bit n w m eq i :
        bit (eq_rect n word w m eq) i = bit w (eq_rect m ordinal i n (Logic.eq_sym eq)).
    Proof. by move: i; case eq => i. Qed.
    Lemma rew_ord n i m eq:
        eq_rect n ordinal i m eq =
        let '(Ordinal i l) := i in Ordinal (eq_rect n (fun m => i < m) l m eq).
    Proof. by move: i; case eq; case=> m' ltn. Qed.

    (* Somehow, I can't figure out the nice way to implement `popHigh`. *)

    Definition popLow {n} (w : word n.+1) : bool * word n. Admitted.
    Lemma pushLowK {n} : cancel pushLow (popLow (n := n)). Admitted.
    Lemma popLowK {n} : cancel popLow (pushLow (n := n)). Admitted.

    Proof.

    Definition popLow {n} (w : word n.+1) : bool * word n.
        apply locked.
        refine (let '(b,w) := split _ in (bool_of_word1 b, w)).
        by rewrite add1n.
    Defined.

    Lemma pushLowK {n} : cancel pushLow (popLow (n := n)).
    Proof.
        move=> [b w].
        rewrite /popLow; unlock.
        apply pair_equal_spec; split.
        - rewrite -{2}[b](pushLow_spec1 b w).
            rewrite /bool_of_word1 fromBitsK rew_bit; f_equal.
            by apply /eqP; rewrite rew_ord /eq_op; simpl.
        - apply wordP => i.
            rewrite -(pushLow_spec2 b w).
            rewrite fromBitsK rew_bit; f_equal.
            by apply /eqP; rewrite rew_ord /eq_op; simpl.
    Qed.
    Lemma popLowK {n} : cancel popLow (pushLow (n := n)).
    Proof.
        move=> w.
        rewrite /popLow; unlock.
        apply wordP; case /ordLowP.
        - rewrite pushLow_spec1 /bool_of_word1 fromBitsK rew_bit; f_equal.
            by apply /eqP; rewrite rew_ord /eq_op; simpl.
        - move=> i.
            rewrite pushLow_spec2 fromBitsK rew_bit; f_equal.
            by apply /eqP; rewrite rew_ord /eq_op; simpl.
    Qed.
    

    Definition popHigh {n} (w : word n.+1) : word n * bool. Admitted.
    Lemma pushHighK {n} : cancel pushHigh (popHigh (n := n)). Admitted.
    Lemma popHighK {n} : cancel popHigh (pushHigh (n := n)). Admitted.

    Inductive ordHigh {n} : 'I_n.+1 -> Type :=
    | ordHigh1 (i : 'I_n) : ordHigh (widen_ord (leqnSn _) i)
    | ordHigh2 : ordHigh ord_max
    .

    Lemma ordHighP {n} (i : 'I_n.+1) : ordHigh i.
    Proof.
        case i => m pf.
        have: (m == n) = (m == n) by []; case: {-1}(m == n) => [eq | neq].
        - have->: Ordinal pf = ord_max by apply /eqP; rewrite /eq_op; simpl.
            apply ordHigh2.
        - move: (pf) => pf'.
            rewrite leq_eqVlt eqSS neq -[m.+1]add1n -[n.+1]add1n ltn_add2l in pf.
            simpl in pf.
            have->: Ordinal pf' = widen_ord (leqnSn _) (Ordinal pf)
                by apply /eqP; rewrite /eq_op; simpl.
            apply ordHigh1.
    Qed.
    Definition popHigh {n} (w : word n.+1) : word n * bool.
        apply locked.
        refine (let '(w,b) := split _ in (w, bool_of_word1 b)).
        by rewrite addn1.
    Defined.
    Lemma pushHighK {n} : cancel pushHigh (popHigh (n := n)).
    Proof.
        move=> [w b].
        rewrite /popHigh; unlock.
        apply pair_equal_spec; split.
        - apply wordP => i.
            rewrite -(pushHigh_spec1 w b).
            rewrite fromBitsK rew_bit; f_equal.
            by apply /eqP; rewrite rew_ord /eq_op; simpl.
        - rewrite -{2}[b](pushHigh_spec2 w b).
            rewrite /bool_of_word1 fromBitsK rew_bit; f_equal.
            by apply /eqP; rewrite rew_ord /eq_op; simpl; rewrite addn0.
    Qed.
    Lemma popHighK {n} : cancel popHigh (pushHigh (n := n)).
    Proof.
        move=> w.
        rewrite /popHigh; unlock.
        apply wordP; case /ordHighP.
        - move=> i.
            rewrite pushHigh_spec1 fromBitsK rew_bit; f_equal.
            by apply /eqP; rewrite rew_ord /eq_op; simpl.
        - rewrite pushHigh_spec2 /bool_of_word1 fromBitsK rew_bit; f_equal.
            by apply /eqP; rewrite rew_ord /eq_op; simpl; rewrite addn0.
    Qed.

        - move=> n IH cin a b. simpl.

        - move=> n IH cin a b.
            simpl.

From mathcomp Require Import all_ssreflect.
Require Import word memory.
(* 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 is possible.
    - 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.
        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.
Definition read {rom} (addr : word 16) (s : state rom) (w : word 8) : Prop.
Proof.
    by refine (
        (* ROM *)
        if bit addr (Ordinal (m := 12) _)
        then w = get rom (split (n := 4) _).1
        (* TIA *)
        else if ~~ bit addr (Ordinal (m := 7) _)
        then True
        (* PIA *)
        else if bit addr (Ordinal (m := 9) _)
        then True
        (* RAM *)
        else w = get (RAM s) (split (n := 9) _).1
    ).
Defined.
Definition write {rom} (addr : word 16) (s : state rom) (w : word 8) (s' : state rom) : Prop.
Proof.
    by refine (
        (* ROM *)
        if bit addr (Ordinal (m := 12) _)
        then True
        (* TIA *)
        else if ~~ bit addr (Ordinal (m := 7) _)
        then True
        (* PIA *)
        else if bit addr (Ordinal (m := 9) _)
        then True
        (* RAM *)
        else s' = fromRAM (update (RAM s) (fun=>w) (split (n := 9) _).1)
    ).
Defined.

From mathcomp Require Import all_ssreflect.
Require Import word.
(* An efficient implementation of `word n -> V`. *)
Fixpoint memory n (V : Type) : Type := match n with
    | 0 => V
    | n.+1 => memory n (V * V)
end.
Definition get {n V} : memory n V -> (word n -> V).
Proof.
    move: V; elim: n.
    - move=> V v _. exact v.
    - move=> n recurse V m /popLow [b w].
        move: (recurse (V*V)%type m w) => [x y].
        exact (if b then y else x).
Defined.
Definition fromFun {n V} : (word n -> V) -> memory n V.
Proof.
    move: V; elim: n.
    - move=> V f. exact (f trivial_word).
    - move=> n recurse V f.
        apply recurse.
        move=> w.
        split; apply f.
        + exact (pushLow (false, w)).
        + exact (pushLow (true, w)).
Defined.
Lemma fromFun_respect_eq1 {n V f g} : f =1 g -> fromFun f = fromFun (n := n) (V := V) g.
Proof.
    move: V f g; elim: n.
    - simpl. done.
    - move=> n IH V f g eq. apply IH => w. by rewrite eq eq.
Qed.
Lemma getK {n V} : cancel get (fromFun (n := n) (V := V)).
Proof.
    move: V; elim: n.
    - done.
    - move=> n IH V m.
        rewrite -{2}(IH _ m).
        simpl.
        apply: fromFun_respect_eq1 => w.
        rewrite pushLowK pushLowK.
        by apply: injective_projections.
Qed.
Lemma fromFunK {n V} : forall f, get (fromFun (n := n) (V := V) f) =1 f.
Proof.
    move: V; elim: n.
    - move=> V f w. by rewrite word0.
    - move=> n IH V f w.
        simpl.
        have: popLow w = popLow w by []; move: {-1}(popLow w) => [b w'] eq.
        rewrite IH.
        have: b = b by []; case: {-1}b => <-; move: eq => <-; by rewrite popLowK.
Qed.
Definition update {n V} : memory n V -> (V -> V) -> word n -> memory n V.
Proof.
    move: V; elim: n.
    - move=> V m f _. exact (f m).
    - move=> n recurse V m f /popLow [b w].
        move: (fun '(x,y) => if b then (x, f y) else (f x, y)) => f'.
        exact (recurse (V*V)%type m f' w).
Defined.
Lemma update_spec {n V} (f : V -> V) (w w' : word n) m
    : get (update m f w') w = if w == w' then f (get m w) else get m w.
Proof.
    move: V f w w' m; elim: n.
    - move=> V f w w' m. by rewrite word0 word0.
    - move=> n IH V f w w' m.
        rewrite -{2}[w]popLowK -{2}[w']popLowK.
        simpl.
        move: (popLow w) (popLow w'); clear w w'; move=> [b w] [b' w'].
        rewrite IH.
        have->: (pushLow (b, w) == pushLow (b', w')) = andb (b == b') (w == w')
            by rewrite /pushLow; do 3 (rewrite /eq_op; simpl).
        
        move: (get (n := n) m w) => [x y].
        by case: (w == w'); case: b; case: b'.
Qed.

theories/memory.v
theories/peripherals.v