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

    From mathcomp Require Import ssralg ssrint.

    From mathcomp Require Import ssralg ssrint intdiv.

    Definition word_of_nat {n} (w : nat) : word n :=
        word_of_tuple [tuple odd (w %% (2^i)) | i < n].

    Definition word_of_int {n} (w : int) : word n :=
        word_of_tuple [tuple ~~(divz w (2^i)%:Z %| 2%:Z)%Z | i < n].
    Definition word_of_nat {n} (w : nat) : word n := word_of_int w.

        nat_of_word (pushLow (b, w)) = b + nat_of_word w * 2.

        nat_of_word (pushLow (b, w)) = b + double (nat_of_word w).

        - rewrite big_distrl.

        - rewrite -muln2 big_distrl.

    Lemma int_of_pushLow {n} b (w : word n) :
        (int_of_word (pushLow (b, w)) = b%:Z + int_of_word w * 2)%R.
    Proof. by rewrite /int_of_word nat_of_pushLow -muln2 PoszD PoszM. Qed.

    Lemma int_of_pushHigh {n} (w : word n) b :
        (int_of_word (pushHigh (w, b)) = int_of_word w + b%:Z * (2^n)%:Z)%R.
    Proof. by rewrite /int_of_word nat_of_pushHigh PoszD PoszM. Qed.

            rewrite -addnA -mulnDl -mulnDl addnA -IH.

            rewrite -muln2 -muln2 -addnA -mulnDl -mulnDl addnA -IH.

            rewrite nat_of_pushLow.

            rewrite nat_of_pushLow -muln2.

    Qed.

    Definition addw {n} (w w' : word n) : word n
        := (addition false w w').1.
    Definition increment {n} (i : int) (w : word n) : word n
        := addw w (word_of_int i).
Qed.

Definition word_eqMixin {n} := CanEqMixin (tuple_of_wordK (n := n)).
Canonical word_eqType {n} := EqType (word n) word_eqMixin.
Definition word_choiceMixin {n} := CanChoiceMixin (tuple_of_wordK (n := n)).
Canonical word_choiceType {n} := ChoiceType (word n) word_choiceMixin.
Definition word_countMixin {n} := CanCountMixin (tuple_of_wordK (n := n)).
Canonical word_countType {n} := CountType (word n) word_countMixin.
Definition word_finMixin {n} := CanFinMixin (tuple_of_wordK (n := n)).
Canonical word_finType {n} := FinType (word n) word_finMixin.
(* Section ZmodType.
    From mathcomp Require Import ssralg ssrint.
    Local Open Scope Z.
    Import GRing.Theory.
    Definition word_eqMixin {n} := CanEqMixin (tuple_of_wordK (n := n)).
    Canonical word_eqType {n} := EqType (word n) word_eqMixin.
    Definition word_choiceMixin {n} := CanChoiceMixin (tuple_of_wordK (n := n)).
    Canonical word_choiceType {n} := ChoiceType (word n) word_choiceMixin.
    Definition word_countMixin {n} := CanCountMixin (tuple_of_wordK (n := n)).
    Canonical word_countType {n} := CountType (word n) word_countMixin.
    Definition word_finMixin {n} := CanFinMixin (tuple_of_wordK (n := n)).
    Canonical word_finType {n} := FinType (word n) word_finMixin.
    Definition addw {n} (a b : word n) : word n := (addition false a b).1.
    Definition oppw {n} (a : word n) : word n := (subtraction true (op0 false) a).1.
    Lemma addwA {n} : associative (addw (n := n)). Admitted.
    Lemma addwC {n} : commutative (addw (n := n)). Admitted.
    Lemma add0w {n} : left_id (op0 false) (addw (n := n)). Admitted.
    Lemma addKw {n} : left_inverse (op0 false) oppw (addw (n := n)). Admitted.
    Definition word_zmodMixin {n} := ZmodMixin addwA addwC add0w (addKw (n := n)).
    Canonical word_zmodType {n} := ZmodType (word n) word_zmodMixin.
End ZmodType. *)

Require Import word memory.

Require Import word memory nondeterminism.

        I don't know what happens if you try to write to it, so I assume anything is possible.

        I don't know what happens if you try to write to it,
        so I assume anything can happen in that case.

        I don't understand what these do, so I'll assume they can do anything.

        I don't understand what these do, so I'll assume they can do anything they want.

Definition read {rom} (addr : word 16) (s : state rom) (w : word 8) : Prop.

(* 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).

        then w = get rom (split (n := 4) _).1

        then determined (get rom (split (n := 4) _).1)

        then True

        then unspecified

        then True

        then unspecified

        else w = get (RAM s) (split (n := 9) _).1

        else determined (get (RAM s) (split (n := 9) _).1)

Definition write {rom} (addr : word 16) (s : state rom) (w : word 8) (s' : state rom) : Prop.

(* 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).

        then True

        then unspecified

        then True

        then unspecified

        then True

        then unspecified

        else s' = fromRAM (update (RAM s) (fun=>w) (split (n := 9) _).1)

        else determined (fromRAM (update (RAM s) (fun=>w) (split (n := 9) _).1))

From mathcomp Require Import all_ssreflect.
Inductive nondet (T : Type) : Type := fromPossibilities of (T -> Prop).
Arguments fromPossibilities {T}.
Definition possible {T} : nondet T -> T -> Prop := fun '(fromPossibilities P) => P.
Lemma possibleK {T} : cancel possible (fromPossibilities (T := T)). by case. Qed.
Lemma fromPossibilitiesK {T} : cancel fromPossibilities (possible (T := T)). done. Qed.
(* A fully unspecified value. It can do anything. *)
Definition unspecified {T} : nondet T := fromPossibilities (fun=> True).
(* A fully determined value. *)
Definition determined {T} (x : T) : nondet T := fromPossibilities (eq x).
(* Apply a nondeterministic function to a nondeterministic value. *)
Definition bind {A B} (f : A -> nondet B) (n : nondet A) : nondet B :=
    fromPossibilities (fun b => exists a, possible n a /\ possible (f a) b).
Notation "x <- y ; z" := (bind (fun x => z) y)
    (at level 20, y at level 100, z at level 200).
Notation "' x <- y ; z" := (bind (fun x => z) y)
    (at level 20, x pattern, y at level 100, z at level 200).
(* Monad laws *)
Lemma nondet_unitl {A B} (f : A -> nondet B) a b
    : possible (x <- determined a; f x) b <-> possible (f a) b.
Proof.
    rewrite fromPossibilitiesK.
    split.
    - move=> [a' [<- pf]]; exact pf.
    - move=> pf; exists a; exact (conj Logic.eq_refl pf).
Qed.
Lemma nondet_unitr {A} (m : nondet A) (a : A)
    : possible (x <- m; determined x) a <-> possible m a.
Proof.
    rewrite fromPossibilitiesK.
    split.
    - move=> [a' [pf <-]]; exact pf.
    - move=> pf; exists a; exact (conj pf Logic.eq_refl).
Qed.
Lemma nondet_assoc {A B C} (f : A -> nondet B) (g : B -> nondet C) m c
    : possible (y <- (x <- m; f x); g y) c <-> possible (x <- m; y <- f x; g y) c.
Proof.
    rewrite fromPossibilitiesK fromPossibilitiesK fromPossibilitiesK.
    split.
    - move=> [b [[a [pm pf]] pg]].
        exists a.
        split; first exact pm.
        rewrite fromPossibilitiesK.
        exists b.
        split; [exact pf | exact pg].
    - move=> [a [pm x]].
        rewrite fromPossibilitiesK in x.
        move: x => [b [pf pg]].
        exists b.
        split; last exact pg.
        exists a.
        split; [exact pm | exact pf].
Qed.

From mathcomp Require Import all_ssreflect ssralg ssrint.
Import GRing.Theory.
Local Open Scope R.
Require Import nondeterminism word memory peripherals.
From RecordUpdate Require Import RecordSet.
(* In this file, I precisely describe the behavior of the Atari 2600.
    I then define what it means for a state of the Atari to be reachable.
    This is necessary to even *state* the theorem we want to prove;
    to prove anything about minimum speedrun times, we need to define what it means to run a program!
    Note that if there is a bug in this specification,
    the final theorem will instead prove a minimum speedrun time *when running Dragster on a buggy Atari*.
    This is an unavoidable limitation to the proof.
*)
(* Flags *)
Record flags := {
    FlagN : bool;
    FlagV : bool; (* WARNING: I assume the SO pin is unused. *)
    FlagD : bool;
    FlagI : bool;
    FlagZ : bool;
    FlagC : bool;
}.
Instance set_flags : Settable _ := settable! Build_flags
    <FlagN; FlagV; FlagD; FlagI; FlagZ; FlagC>.
Definition word_of_flags (break : bool) (f : flags) : word 8
    := word_of_tuple [tuple 
        (FlagC f);
        (FlagZ f);
        (FlagI f);
        (FlagD f);
        break;
        true;
        (FlagV f);
        (FlagN f)
    ].
Definition flags_of_word (w : word 8) : flags.
by refine {|
    FlagC := bit w (Ordinal (m := 0) _);
    FlagZ := bit w (Ordinal (m := 1) _);
    FlagI := bit w (Ordinal (m := 2) _);
    FlagD := bit w (Ordinal (m := 3) _);
    FlagV := bit w (Ordinal (m := 6) _);
    FlagN := bit w (Ordinal (m := 7) _);
|}.
Defined.
Lemma word_of_flagsK b : cancel (word_of_flags b) flags_of_word.
Proof.
    move=> [n v d i z c].
    rewrite /word_of_flags; simpl.
    by rewrite /flags_of_word /bit word_of_tupleK /tnth.
Qed.
(* State *)
Record state (rom : ROM) := {
    Peripherals : peripherals.state rom;
    Flags : flags;
    ProgramCounter : word 16;
    RegA : word 8;
    RegX : word 8;
    RegY : word 8;
    RegS : word 8; (* Stack Pointer *)
}.
Arguments Peripherals {rom}.
Arguments Flags {rom}.
Arguments ProgramCounter {rom}.
Arguments RegA {rom}.
Arguments RegX {rom}.
Arguments RegY {rom}.
Arguments RegS {rom}.
Instance set_state {rom} : Settable _ := settable! (Build_state rom)
    <Peripherals; Flags; ProgramCounter; RegA; RegX; RegY; RegS>.
Definition read {rom} (addr : word 16) (s : state rom) : nondet (word 8)
    := peripherals.read addr (Peripherals s).
Definition write {rom} (addr : word 16) (w : word 8) (s : state rom) : nondet (state rom)
    := p <- peripherals.write addr w (Peripherals s); determined (set Peripherals (fun=>p) s).
(* Flags *)
Definition setZN {rom} (w : word 8) : state rom -> state rom
    := set Flags
        (fun f => set FlagN (fun=> bit w ord_max)
            (set FlagZ (fun=> w == op0 false) f)).
(* Stack *)
Definition push8 {rom} (w : word 8) (s : state rom) : nondet (state rom). Admitted.
Definition push16 {rom} (w : word 16) (s : state rom) : nondet (state rom). Admitted.
Definition pull8 {rom} (s : state rom) : nondet (word 8 * state rom). Admitted.
Definition pull16 {rom} (s : state rom) : nondet (word 16 * state rom). Admitted.
(* Addressing Modes *)
Inductive addressing_mode :=
| Accumulator
| Immediate
| Implied
| Relative
| Absolute
| ZeroPage
| Indirect
| AbsoluteX
| AbsoluteY
| ZeroPageX
| ZeroPageY
| IndexedIndirect
| IndirectIndexed
.
Definition mode_width (mode : addressing_mode) : nat := match mode with
    | Accumulator => 0
    | Immediate => 1
    | Implied => 0
    | Relative => 1
    | Absolute => 2
    | ZeroPage => 1
    | Indirect => 2
    | AbsoluteX => 2
    | AbsoluteY => 2
    | ZeroPageX => 1
    | ZeroPageY => 1
    | IndexedIndirect => 1
    | IndirectIndexed => 1
end.
(* Many addressing modes pick out an address in memory. Return that address. *)
Definition mode_addr {rom} (mode : addressing_mode)
:= match mode return word (mode_width mode * 8) -> state rom -> nondet (word 16) with
    | Accumulator => fun _ _ => unspecified
    | Immediate => fun _ _ => unspecified
    | Implied => fun _ _ => unspecified
    | Relative => fun offset s =>
        determined (addw
            (ProgramCounter s)
            (concat (offset, op0 (bit offset ord_max))))
    | Absolute => fun addr s => determined addr
    | ZeroPage => fun addr s => determined (concat (addr, op0 false))
    | Indirect => fun addr s =>
        (* Annoying edge case. I could specify the behavior here too, but why bother? *)
        if (split addr).1 == op0 (n := 8) true then unspecified else
        lo <- read addr s;
        hi <- read (increment 1 addr) s;
        determined (concat (lo, hi))
    | AbsoluteX => fun addr s => determined (addw addr (concat (RegX s, op0 false)))
    | AbsoluteY => fun addr s => determined (addw addr (concat (RegY s, op0 false)))
    | ZeroPageX => fun addr s => determined (concat (addw addr (RegX s), op0 false))
    | ZeroPageY => fun addr s => determined (concat (addw addr (RegY s), op0 false))
    | IndexedIndirect => fun addr s => 
        let addr := addw addr (RegX s) in
        lo <- read (concat (addr, op0 false)) s;
        hi <- read (concat (increment 1 addr, op0 false)) s;
        determined (concat (lo, hi))
    | IndirectIndexed => fun addr s =>
        lo <- read (concat (addr, op0 false)) s;
        hi <- read (concat (increment 1 addr, op0 false)) s;
        determined (addw (concat (lo, hi)) (concat (RegY s, op0 false)))
end.
(* Read data, using this addressing mode. *)
Definition mode_read {rom} (mode : addressing_mode)
:= match mode return word (mode_width mode * 8) -> state rom -> nondet (word 8) with
    | Accumulator => fun _ s => determined (RegA s)
    | Immediate => fun w _ => determined w
    | Implied => fun _ _ => unspecified
    | mode => fun bytes s =>
        addr <- mode_addr mode bytes s;
        read addr s
end.
(* Write data, using this addressing mode. *)
Definition mode_write {rom} (mode : addressing_mode)
:= match mode return word (mode_width mode * 8) -> word 8 -> state rom -> nondet (state rom) with
    | Accumulator => fun _ w s => determined (set RegA (fun=>w) s)
    | Immediate => fun _ _ _ => unspecified
    | Implied => fun _ _ _ => unspecified
    | mode => fun bytes w s =>
        addr <- mode_addr mode bytes s;
        write addr w s
end.
(* Instructions *)
Inductive instruction :=
| ADC | AND | ASL | BCC | BCS | BEQ | BIT | BMI | BNE | BPL | BRK | BVC | BVS | CLC
| CLD | CLI | CLV | CMP | CPX | CPY | DEC | DEX | DEY | EOR | INC | INX | INY | JMP
| JSR | LDA | LDX | LDY | LSR | NOP | ORA | PHA | PHP | PLA | PLP | ROL | ROR | RTI
| RTS | SBC | SEC | SED | SEI | STA | STX | STY | TAX | TAY | TSX | TXA | TXS | TYA
.
Definition run_instruction {rom}
    (instr : instruction)
    (mode : addressing_mode)
    (bytes : word (mode_width mode * 8))
    (s : state rom)
    : nondet (state rom)
:= match instr with
    (* Organization based on https://masswerk.at/6502/6502_instruction_set.html *)
    (* Transfer Instructions *)
    | LDA => w <- mode_read mode bytes s; determined (set RegA (fun=> w) (setZN w s))
    | LDX => w <- mode_read mode bytes s; determined (set RegX (fun=> w) (setZN w s))
    | LDY => w <- mode_read mode bytes s; determined (set RegY (fun=> w) (setZN w s))
    | STA => mode_write mode bytes (RegA s) s
    | STX => mode_write mode bytes (RegX s) s
    | STY => mode_write mode bytes (RegY s) s
    | TAX => determined (let w := RegA s in set RegX (fun=> w) (setZN w s))
    | TAY => determined (let w := RegA s in set RegY (fun=> w) (setZN w s))
    | TSX => determined (let w := RegS s in set RegX (fun=> w) (setZN w s))
    | TXA => determined (let w := RegX s in set RegA (fun=> w) (setZN w s))
    | TXS => determined (let w := RegX s in set RegS (fun=> w) s)
    | TYA => determined (let w := RegY s in set RegA (fun=> w) (setZN w s))
    (* Stack Instructions *)
    | PHA => push8 (RegA s) s
    | PHP => push8 (word_of_flags true (Flags s)) s
    | PLA =>
        '(w, s) <- pull8 s;
        determined (set RegA (fun=> w) (setZN w s))
    | PLP =>
        '(w, s) <- pull8 s;
        determined (set Flags (fun=> set FlagI (fun=> false) (flags_of_word w)) s)
    (* Decrements and Increments *)
    | DEC =>
        w <- mode_read mode bytes s;
        let w := increment (-1) w in
        mode_write mode bytes w (setZN w s)
    | DEX =>
        let w := increment (-1) (RegX s) in
        determined (set RegX (fun=> w) (setZN w s))
    | DEY =>
        let w := increment (-1) (RegY s) in
        determined (set RegY (fun=> w) (setZN w s))
    | INC =>
        w <- mode_read mode bytes s;
        let w := increment 1 w in
        mode_write mode bytes w (setZN w s)
    | INX =>
        let w := increment 1 (RegX s) in
        determined (set RegX (fun=> w) (setZN w s))
    | INY =>
        let w := increment 1 (RegY s) in
        determined (set RegY (fun=> w) (setZN w s))
    (* Arithmetic Operations *)
    | ADC =>
        if FlagD (Flags s)
        then unspecified (* TODO. Note: Only C should be specified. *)
        else
            w <- mode_read mode bytes s;
            let '(w, carryout) := addition (FlagC (Flags s)) (RegA s) w in
            overflow <- unspecified;
            determined 
                (set RegA (fun=> w)
                    (set Flags
                        (fun f =>
                            set FlagC (fun=> carryout) 
                                (set FlagV (fun=> overflow) f))
                        (setZN w s)))
    | SBC =>
        if FlagD (Flags s)
        then unspecified (* TODO. Note: Only C should be specified. *)
        else
            w <- mode_read mode bytes s;
            let '(w, carryout) := subtraction (FlagC (Flags s)) (RegA s) w in
            overflow <- unspecified;
            determined 
                (set RegA (fun=> w)
                    (set Flags
                        (fun f =>
                            set FlagC (fun=> carryout) 
                                (set FlagV (fun=> overflow) f))
                        (setZN w s)))
    (* Logical Operations *)
    | AND =>
        w <- mode_read mode bytes s;
        let w := op2 andb (RegA s) w in
        determined (set RegA (fun=> w) (setZN w s))
    | ORA =>
        w <- mode_read mode bytes s;
        let w := op2 orb (RegA s) w in
        determined (set RegA (fun=> w) (setZN w s))
    | EOR =>
        w <- mode_read mode bytes s;
        let w := op2 addb (RegA s) w in
        determined (set RegA (fun=> w) (setZN w s))
    (* Shift & Rotate Instructions *)
    | ASL =>
        w <- mode_read mode bytes s;
        let '(w, b) := popHigh (pushLow (false, w)) in
        determined (set RegA (fun=> w) (set Flags (set FlagC (fun=>b)) (setZN w s)))
    | LSR =>
        w <- mode_read mode bytes s;
        let '(b, w) := popLow (pushHigh (w, false)) in
        determined (set RegA (fun=> w) (set Flags (set FlagC (fun=>b)) (setZN w s)))
    | ROL =>
        w <- mode_read mode bytes s;
        let '(w, b) := popHigh (pushLow (FlagC (Flags s), w)) in
        determined (set RegA (fun=> w) (set Flags (set FlagC (fun=>b)) (setZN w s)))
    | ROR =>
        w <- mode_read mode bytes s;
        let '(b, w) := popLow (pushHigh (w, FlagC (Flags s))) in
        determined (set RegA (fun=> w) (set Flags (set FlagC (fun=>b)) (setZN w s)))
    (* Flag Instructions *)
    | CLC => determined (set Flags (set FlagC (fun=> false)) s)
    | CLD => determined (set Flags (set FlagD (fun=> false)) s)
    | CLI => determined (set Flags (set FlagI (fun=> false)) s)
    | CLV => determined (set Flags (set FlagV (fun=> false)) s)
    | SEC => determined (set Flags (set FlagC (fun=> true)) s)
    | SED => determined (set Flags (set FlagD (fun=> true)) s)
    | SEI => determined (set Flags (set FlagI (fun=> true)) s)
    (* Comparisons *)
    | CMP =>
        w <- mode_read mode bytes s;
        let '(w, carryout) := subtraction true (RegA s) w in
        determined 
            (set Flags
                (set FlagC (fun=> carryout))
                (setZN w s))
    | CPX =>
        w <- mode_read mode bytes s;
        let '(w, carryout) := subtraction true (RegX s) w in
        determined 
            (set Flags
                (set FlagC (fun=> carryout))
                (setZN w s))
    | CPY =>
        w <- mode_read mode bytes s;
        let '(w, carryout) := subtraction true (RegY s) w in
        determined 
            (set Flags
                (set FlagC (fun=> carryout))
                (setZN w s))
                        
    (* Conditional Branch Instructions *)
    | BCS =>
        if   FlagC (Flags s) then
            addr <- mode_addr mode bytes s;
            determined (set ProgramCounter (fun=> addr) s)
        else determined s
    | BCC =>
        if ~~FlagC (Flags s) then
            addr <- mode_addr mode bytes s;
            determined (set ProgramCounter (fun=> addr) s)
        else determined s
    | BEQ =>
        if   FlagZ (Flags s) then
            addr <- mode_addr mode bytes s;
            determined (set ProgramCounter (fun=> addr) s)
        else determined s
    | BNE =>
        if ~~FlagZ (Flags s) then
            addr <- mode_addr mode bytes s;
            determined (set ProgramCounter (fun=> addr) s)
        else determined s
    | BVS =>
        if   FlagV (Flags s) then
            addr <- mode_addr mode bytes s;
            determined (set ProgramCounter (fun=> addr) s)
        else determined s
    | BVC =>
        if ~~FlagV (Flags s) then
            addr <- mode_addr mode bytes s;
            determined (set ProgramCounter (fun=> addr) s)
        else determined s
    | BMI =>
        if   FlagN (Flags s) then
            addr <- mode_addr mode bytes s;
            determined (set ProgramCounter (fun=> addr) s)
        else determined s
    | BPL =>
        if ~~FlagN (Flags s) then
            addr <- mode_addr mode bytes s;
            determined (set ProgramCounter (fun=> addr) s)
        else determined s
    (* Jumps & Subroutines *)
    | JMP =>
        addr <- mode_addr mode bytes s;
        determined (set ProgramCounter (fun=> addr) s)
    | JSR =>
        addr <- mode_addr mode bytes s;
        push16 (increment (-1) (ProgramCounter s))
            (set ProgramCounter (fun=> addr) s)
    | RTS =>
        '(addr, s) <- pull16 s;
        determined (set ProgramCounter (fun=> increment 1 addr) s)
    (* Interrupts *)
    | BRK => 
        s <- push16 (increment (-1) (ProgramCounter s)) s;
        s <- push8 (word_of_flags true (Flags s)) s;
        lo <- read (pushLow (false, op0 true)) s;
        hi <- read (pushLow (true, op0 true)) s;
        determined
            (set ProgramCounter (fun=> concat (lo : word 8, hi : word 8))
                (set Flags (set FlagI (fun=> true)) s))
    | RTI =>
        '(f, s) <- pull8 s;
        '(addr, s) <- pull16 s;
        determined
            (set ProgramCounter (fun=> addr)
                (set Flags (fun=> set FlagI (fun=> false) (flags_of_word f)) s))
    (* Other *)
    | BIT =>
        w <- mode_read mode bytes s;
        determined (set Flags 
            (fun f =>
                (set FlagZ (fun=> op2 andb (RegA s) w == op0 false)
                    (set FlagN (fun=> bit w (Ordinal (m := 7) (leqnn _)))
                        (set FlagV (fun=> bit w (Ordinal (m := 6) (leqnSn _)))
                            f))))
        s)
    | NOP => determined s
end.
(* Given an opcode, return the corresponding instruction and addressing mode.
    Return `None` if the opcode is invalid.
*)
Definition parse_opcode (w : word 8) : option (instruction * addressing_mode)
:= match nat_of_word w with
    | 0x00 => Some (BRK, Implied)
    | 0x01 => Some (ORA, IndexedIndirect)
    | 0x05 => Some (ORA, ZeroPage)
    | 0x06 => Some (ASL, ZeroPage)
    | 0x08 => Some (PHP, Implied)
    | 0x09 => Some (ORA, Immediate)
    | 0x0a => Some (ASL, Accumulator)
    | 0x0d => Some (ORA, Absolute)
    | 0x0e => Some (ASL, Absolute)
    | 0x10 => Some (BPL, Relative)
    | 0x11 => Some (ORA, IndirectIndexed)
    | 0x15 => Some (ORA, ZeroPageX)
    | 0x16 => Some (ASL, ZeroPageX)
    | 0x18 => Some (CLC, Implied)
    | 0x19 => Some (ORA, AbsoluteY)
    | 0x1d => Some (ORA, AbsoluteX)
    | 0x1e => Some (ASL, AbsoluteX)
    | 0x20 => Some (JSR, Absolute)
    | 0x21 => Some (AND, IndexedIndirect)
    | 0x24 => Some (BIT, ZeroPage)
    | 0x25 => Some (AND, ZeroPage)
    | 0x26 => Some (ROL, ZeroPage)
    | 0x28 => Some (PLP, Implied)
    | 0x29 => Some (AND, Immediate)
    | 0x2a => Some (ROL, Accumulator)
    | 0x2c => Some (BIT, Absolute)
    | 0x2d => Some (AND, Absolute)
    | 0x2e => Some (ROL, Absolute)
    | 0x30 => Some (BMI, Relative)
    | 0x31 => Some (AND, IndirectIndexed)
    | 0x35 => Some (AND, ZeroPageX)
    | 0x36 => Some (ROL, ZeroPageX)
    | 0x38 => Some (SEC, Implied)
    | 0x39 => Some (AND, AbsoluteY)
    | 0x3d => Some (AND, AbsoluteX)
    | 0x3e => Some (ROL, AbsoluteX)
    | 0x40 => Some (RTI, Implied)
    | 0x41 => Some (EOR, IndexedIndirect)
    | 0x45 => Some (EOR, ZeroPage)
    | 0x46 => Some (LSR, ZeroPage)
    | 0x48 => Some (PHA, Implied)
    | 0x49 => Some (EOR, Immediate)
    | 0x4a => Some (LSR, Accumulator)
    | 0x4c => Some (JMP, Absolute)
    | 0x4d => Some (EOR, Absolute)
    | 0x4e => Some (LSR, Absolute)
    | 0x50 => Some (BVC, Relative)
    | 0x51 => Some (EOR, IndirectIndexed)
    | 0x55 => Some (EOR, ZeroPageX)
    | 0x56 => Some (LSR, ZeroPageX)
    | 0x58 => Some (CLI, Implied)
    | 0x59 => Some (EOR, AbsoluteY)
    | 0x5d => Some (EOR, AbsoluteX)
    | 0x5e => Some (LSR, AbsoluteX)
    | 0x60 => Some (RTS, Implied)
    | 0x61 => Some (ADC, IndexedIndirect)
    | 0x65 => Some (ADC, ZeroPage)
    | 0x66 => Some (ROR, ZeroPage)
    | 0x68 => Some (PLA, Implied)
    | 0x69 => Some (ADC, Immediate)
    | 0x6a => Some (ROR, Accumulator)
    | 0x6c => Some (JMP, Indirect)
    | 0x6d => Some (ADC, Absolute)
    | 0x6e => Some (ROR, AbsoluteX)
    | 0x70 => Some (BVS, Relative)
    | 0x71 => Some (ADC, IndirectIndexed)
    | 0x75 => Some (ADC, ZeroPageX)
    | 0x76 => Some (ROR, ZeroPageX)
    | 0x78 => Some (SEI, Implied)
    | 0x79 => Some (ADC, AbsoluteY)
    | 0x7d => Some (ADC, AbsoluteX)
    | 0x7e => Some (ROR, Absolute)
    | 0x81 => Some (STA, IndexedIndirect)
    | 0x84 => Some (STY, ZeroPage)
    | 0x85 => Some (STA, ZeroPage)
    | 0x86 => Some (STX, ZeroPage)
    | 0x88 => Some (DEY, Implied)
    | 0x8a => Some (TXA, Implied)
    | 0x8c => Some (STY, Absolute)
    | 0x8d => Some (STA, Absolute)
    | 0x8e => Some (STX, Absolute)
    | 0x90 => Some (BCC, Relative)
    | 0x91 => Some (STA, IndirectIndexed)
    | 0x94 => Some (STY, ZeroPageX)
    | 0x95 => Some (STA, ZeroPageX)
    | 0x96 => Some (STX, ZeroPageY)
    | 0x98 => Some (TYA, Implied)
    | 0x99 => Some (STA, AbsoluteY)
    | 0x9a => Some (TXS, Implied)
    | 0x9d => Some (STA, AbsoluteX)
    | 0xa0 => Some (LDY, Immediate)
    | 0xa1 => Some (LDA, IndexedIndirect)
    | 0xa2 => Some (LDX, Immediate)
    | 0xa4 => Some (LDY, ZeroPage)
    | 0xa5 => Some (LDA, ZeroPage)
    | 0xa6 => Some (LDX, ZeroPage)
    | 0xa8 => Some (TAY, Implied)
    | 0xa9 => Some (LDA, Immediate)
    | 0xaa => Some (TAX, Implied)
    | 0xac => Some (LDY, Absolute)
    | 0xad => Some (LDA, Absolute)
    | 0xae => Some (LDX, Absolute)
    | 0xb0 => Some (BCS, Relative)
    | 0xb1 => Some (LDA, IndirectIndexed)
    | 0xb4 => Some (LDY, ZeroPageX)
    | 0xb5 => Some (LDA, ZeroPageX)
    | 0xb6 => Some (LDX, ZeroPageY)
    | 0xb8 => Some (CLV, Implied)
    | 0xb9 => Some (LDA, AbsoluteY)
    | 0xba => Some (TSX, Implied)
    | 0xbc => Some (LDY, AbsoluteX)
    | 0xbd => Some (LDA, AbsoluteX)
    | 0xbe => Some (LDX, AbsoluteY)
    | 0xc0 => Some (CPY, Immediate)
    | 0xc1 => Some (CMP, IndexedIndirect)
    | 0xc4 => Some (CPY, ZeroPage)
    | 0xc5 => Some (CMP, ZeroPage)
    | 0xc6 => Some (DEC, ZeroPage)
    | 0xc8 => Some (INY, Implied)
    | 0xc9 => Some (CMP, Immediate)
    | 0xca => Some (DEX, Implied)
    | 0xcc => Some (CPY, Absolute)
    | 0xcd => Some (CMP, Absolute)
    | 0xce => Some (DEC, Absolute)
    | 0xd0 => Some (BNE, Relative)
    | 0xd1 => Some (CMP, IndirectIndexed)
    | 0xd5 => Some (CMP, ZeroPageX)
    | 0xd6 => Some (DEC, ZeroPageX)
    | 0xd8 => Some (CLD, Implied)
    | 0xd9 => Some (CMP, AbsoluteY)
    | 0xdd => Some (CMP, AbsoluteX)
    | 0xde => Some (DEC, AbsoluteX)
    | 0xe0 => Some (CPX, Immediate)
    | 0xe1 => Some (SBC, IndexedIndirect)
    | 0xe4 => Some (CPX, ZeroPage)
    | 0xe5 => Some (SBC, ZeroPage)
    | 0xe6 => Some (INC, ZeroPage)
    | 0xe8 => Some (INX, Implied)
    | 0xe9 => Some (SBC, Immediate)
    | 0xea => Some (NOP, Implied)
    | 0xec => Some (CPX, Absolute)
    | 0xed => Some (SBC, Absolute)
    | 0xee => Some (INC, Absolute)
    | 0xf0 => Some (BEQ, Relative)
    | 0xf1 => Some (SBC, IndirectIndexed)
    | 0xf5 => Some (SBC, ZeroPageX)
    | 0xf6 => Some (INC, ZeroPageX)
    | 0xf8 => Some (SED, Implied)
    | 0xf9 => Some (SBC, AbsoluteY)
    | 0xfd => Some (SBC, AbsoluteX)
    | 0xfe => Some (INC, AbsoluteX)
    | _ => None
end.
(* Program Execution *)
Definition init {rom} : nondet (state rom) :=
    (* Begin in an arbitrary state. *)
    s <- unspecified;
    (* Jump to the address contained in the reset vector. *)
    run_instruction JMP Indirect (pushLow (false, pushLow (false, op0 true))) s.
Definition step {rom} (s : state rom) : nondet (state rom) :=
    (* Read the opcode. *)
    op <- read (ProgramCounter s) s;
    if parse_opcode op is Some (instr, mode)
    then 
        let s := set ProgramCounter (increment 1) s in
        (* Read the remaining bytes in the instruction *)
        '(s, bytes) <-
            nat_rect (* basically a for loop *)
                (fun n => nondet (state rom * word (n * 8)))%type
                (determined (s, trivial_word))
                (fun _ m =>
                    '(s, acc) <- m;
                    w <- read (ProgramCounter s) s;
                    (* I can make a `word (n * 8 + 8)`, but need a word ((n.+1) * 8).
                        `eq_rect` does the conversion.
                    *)
                    determined
                        ( set ProgramCounter (increment 1) s
                        , eq_rect _ _ (concat (acc, w)) _ (addnC _ _)
                        )
                )
                (mode_width mode);
        (* Run the instruction. *)
        run_instruction instr mode bytes s
    else unspecified.
Inductive reachable {rom : ROM} : state rom -> Type :=
| Init s : possible init s -> reachable s
| Step s1 s2 : reachable s1 -> possible (step s1) s2 -> reachable s2
.

theories/nondeterminism.v

theories/atari.v

# Dependencies
- coq 8.13.2
- coq-record-update 0.3.0
- coq-mathcomp-ssreflect 1.14.0
- coq-mathcomp-algebra 1.14.0