{"header":{"message":"Implement specification of Atari 2600 console.","description":null,"timestamp":"2022-03-23T00:53:41.523930172Z","authors":[{}]},"hash":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC","authors":[{"login":"finegeometer","key":"64ARLu9ao3fdRKWR644xoCX9eBBEMzfkyWsK7kYdkcxn"}],"deps":{"hashes":[["3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC","Implement specification of Atari 2600 console."],["AA",null],["DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC","Implement processor peripherals. Fix the missing proof in word."],["GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC","Define the underlying word type."],["GVKFJJTTO257PW7OYH7NMFNUY4QMUIXATMXVWTN7PDIFBSNZ3IYQC","Set up Coq project."],["PPEVHPV3NUKUGSD2IQWYM6O42TKH3X55SCWED3C6FHNFJZ6GGBPQC","Explain the basic idea."]],"deps":["DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC"],"known":["GVKFJJTTO257PW7OYH7NMFNUY4QMUIXATMXVWTN7PDIFBSNZ3IYQC","GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC"]},"hunks":[{"Edit":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":18,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1},"to":{"change":2,"start":1,"end":137},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":2,"pos":137},"to":{"change":3,"start":669,"end":670},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":669},"to":{"change":3,"start":669,"end":670},"introduced_by":3}],"inode":{"change":3,"pos":31}}},"contents":[{"Del":{"text":" Definition word_eqMixin {n} := CanEqMixin (tuple_of_wordK (n := n)).","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:73"}},{"Del":{"text":" Canonical word_eqType {n} := EqType (word n) word_eqMixin.","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:136"}},{"Del":{"text":"","pos":"GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC:669"}}]}},{"Replacement":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":273,"ins":{"up_context":[{"change":3,"pos":6750}],"down_context":[{"change":3,"pos":6798}],"flag":"BLOCK","start":0,"end":55,"inode":{"change":3,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":6750},"to":{"change":3,"start":6750,"end":6798},"introduced_by":3}],"inode":{"change":3,"pos":31}},"ins_contents":[{"Add":{"text":" From mathcomp Require Import ssralg ssrint intdiv.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:54"}}],"del_contents":[{"Del":{"text":" From mathcomp Require Import ssralg ssrint.","pos":"GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC:6797"}}]}},{"Replacement":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":280,"ins":{"up_context":[{"change":3,"pos":6992}],"down_context":[{"change":3,"pos":7101}],"flag":"BLOCK","start":56,"end":246,"inode":{"change":3,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":6992},"to":{"change":3,"start":6992,"end":7101},"introduced_by":3}],"inode":{"change":3,"pos":31}},"ins_contents":[{"Add":{"text":" Definition word_of_int {n} (w : int) : word n :=","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:108"}},{"Add":{"text":" word_of_tuple [tuple ~~(divz w (2^i)%:Z %| 2%:Z)%Z | i < n].","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:177"}},{"Add":{"text":" Definition word_of_nat {n} (w : nat) : word n := word_of_int w.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:245"}}],"del_contents":[{"Del":{"text":" Definition word_of_nat {n} (w : nat) : word n :=","pos":"GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC:7044"}},{"Del":{"text":" word_of_tuple [tuple odd (w %% (2^i)) | i < n].","pos":"GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC:7100"}}]}},{"Replacement":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":311,"ins":{"up_context":[{"change":3,"pos":7885}],"down_context":[{"change":3,"pos":7947}],"flag":"BLOCK","start":247,"end":314,"inode":{"change":3,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7885},"to":{"change":3,"start":7885,"end":7947},"introduced_by":3}],"inode":{"change":3,"pos":31}},"ins_contents":[{"Add":{"text":" nat_of_word (pushLow (b, w)) = b + double (nat_of_word w).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:313"}}],"del_contents":[{"Del":{"text":" nat_of_word (pushLow (b, w)) = b + nat_of_word w * 2.","pos":"GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC:7946"}}]}},{"Replacement":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":315,"ins":{"up_context":[{"change":3,"pos":8065}],"down_context":[{"change":3,"pos":8095}],"flag":"BLOCK","start":315,"end":352,"inode":{"change":3,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":8065},"to":{"change":3,"start":8065,"end":8095},"introduced_by":3}],"inode":{"change":3,"pos":31}},"ins_contents":[{"Add":{"text":" - rewrite -muln2 big_distrl.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:351"}}],"del_contents":[{"Del":{"text":" - rewrite big_distrl.","pos":"GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC:8094"}}]}},{"Edit":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":320,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":8243}],"down_context":[{"change":3,"pos":8243}],"flag":"BLOCK","start":353,"end":544,"inode":{"change":3,"pos":31}}},"contents":[{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:353"}},{"Add":{"text":" Lemma int_of_pushLow {n} b (w : word n) :","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:399"}},{"Add":{"text":" (int_of_word (pushLow (b, w)) = b%:Z + int_of_word w * 2)%R.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:468"}},{"Add":{"text":" Proof. by rewrite /int_of_word nat_of_pushLow -muln2 PoszD PoszM. Qed.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:543"}}]}},{"Edit":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":333,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":8543}],"down_context":[{"change":3,"pos":8543}],"flag":"BLOCK","start":545,"end":739,"inode":{"change":3,"pos":31}}},"contents":[{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:545"}},{"Add":{"text":" Lemma int_of_pushHigh {n} (w : word n) b :","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:592"}},{"Add":{"text":" (int_of_word (pushHigh (w, b)) = int_of_word w + b%:Z * (2^n)%:Z)%R.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:669"}},{"Add":{"text":" Proof. by rewrite /int_of_word nat_of_pushHigh PoszD PoszM. Qed.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:738"}}]}},{"Edit":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":338,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":8544}],"down_context":[{"change":3,"pos":8544}],"flag":"BLOCK","start":740,"end":741,"inode":{"change":3,"pos":31}}},"contents":[{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:740"}}]}},{"Replacement":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":387,"ins":{"up_context":[{"change":3,"pos":10265}],"down_context":[{"change":3,"pos":10319}],"flag":"BLOCK","start":742,"end":810,"inode":{"change":3,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":10265},"to":{"change":3,"start":10265,"end":10319},"introduced_by":3}],"inode":{"change":3,"pos":31}},"ins_contents":[{"Add":{"text":" rewrite -muln2 -muln2 -addnA -mulnDl -mulnDl addnA -IH.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:809"}}],"del_contents":[{"Del":{"text":" rewrite -addnA -mulnDl -mulnDl addnA -IH.","pos":"GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC:10318"}}]}},{"Replacement":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":389,"ins":{"up_context":[{"change":3,"pos":10385}],"down_context":[{"change":3,"pos":10421}],"flag":"BLOCK","start":811,"end":854,"inode":{"change":3,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":10385},"to":{"change":3,"start":10385,"end":10421},"introduced_by":3}],"inode":{"change":3,"pos":31}},"ins_contents":[{"Add":{"text":" rewrite nat_of_pushLow -muln2.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:853"}}],"del_contents":[{"Del":{"text":" rewrite nat_of_pushLow.","pos":"GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC:10420"}}]}},{"Replacement":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":422,"ins":{"up_context":[{"change":3,"pos":11877}],"down_context":[{"change":3,"pos":11886}],"flag":"BLOCK","start":855,"end":1044,"inode":{"change":3,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":11877},"to":{"change":3,"start":11877,"end":11886},"introduced_by":3}],"inode":{"change":3,"pos":31}},"ins_contents":[{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:855"}},{"Add":{"text":" Definition addw {n} (w w' : word n) : word n","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:904"}},{"Add":{"text":" := (addition false w w').1.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:940"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:941"}},{"Add":{"text":" Definition increment {n} (i : int) (w : word n) : word n","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1002"}},{"Add":{"text":" := addw w (word_of_int i).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1037"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1038"}},{"Add":{"text":"Qed.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1043"}}],"del_contents":[{"Del":{"text":" Qed.","pos":"GA6XQIN5BJLEGXXMPHSBQJETK7AHPV5AH5KYWWUPO7B4A3KZYN4AC:11885"}}]}},{"Edit":{"inode":{"change":3,"pos":31},"path":"theories/word.v","line":433,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":11902}],"down_context":[],"flag":"BLOCK","start":1045,"end":2912,"inode":{"change":3,"pos":31}}},"contents":[{"Add":{"text":"Definition word_eqMixin {n} := CanEqMixin (tuple_of_wordK (n := n)).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1113"}},{"Add":{"text":"Canonical word_eqType {n} := EqType (word n) word_eqMixin.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1172"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1173"}},{"Add":{"text":"Definition word_choiceMixin {n} := CanChoiceMixin (tuple_of_wordK (n := n)).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1250"}},{"Add":{"text":"Canonical word_choiceType {n} := ChoiceType (word n) word_choiceMixin.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1321"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1322"}},{"Add":{"text":"Definition word_countMixin {n} := CanCountMixin (tuple_of_wordK (n := n)).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1397"}},{"Add":{"text":"Canonical word_countType {n} := CountType (word n) word_countMixin.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1465"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1466"}},{"Add":{"text":"Definition word_finMixin {n} := CanFinMixin (tuple_of_wordK (n := n)).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1537"}},{"Add":{"text":"Canonical word_finType {n} := FinType (word n) word_finMixin.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1599"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1600"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1601"}},{"Add":{"text":"(* Section ZmodType.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1622"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1623"}},{"Add":{"text":" From mathcomp Require Import ssralg ssrint.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1671"}},{"Add":{"text":" Local Open Scope Z.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1695"}},{"Add":{"text":" Import GRing.Theory.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1720"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1721"}},{"Add":{"text":" Definition word_eqMixin {n} := CanEqMixin (tuple_of_wordK (n := n)).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1794"}},{"Add":{"text":" Canonical word_eqType {n} := EqType (word n) word_eqMixin.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1857"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1858"}},{"Add":{"text":" Definition word_choiceMixin {n} := CanChoiceMixin (tuple_of_wordK (n := n)).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:1939"}},{"Add":{"text":" Canonical word_choiceType {n} := ChoiceType (word n) word_choiceMixin.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2014"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2015"}},{"Add":{"text":" Definition word_countMixin {n} := CanCountMixin (tuple_of_wordK (n := n)).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2094"}},{"Add":{"text":" Canonical word_countType {n} := CountType (word n) word_countMixin.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2166"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2167"}},{"Add":{"text":" Definition word_finMixin {n} := CanFinMixin (tuple_of_wordK (n := n)).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2242"}},{"Add":{"text":" Canonical word_finType {n} := FinType (word n) word_finMixin.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2308"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2309"}},{"Add":{"text":" Definition addw {n} (a b : word n) : word n := (addition false a b).1.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2384"}},{"Add":{"text":" Definition oppw {n} (a : word n) : word n := (subtraction true (op0 false) a).1.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2469"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2470"}},{"Add":{"text":" Lemma addwA {n} : associative (addw (n := n)). Admitted.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2531"}},{"Add":{"text":" Lemma addwC {n} : commutative (addw (n := n)). Admitted.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2592"}},{"Add":{"text":" Lemma add0w {n} : left_id (op0 false) (addw (n := n)). Admitted.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2661"}},{"Add":{"text":" Lemma addKw {n} : left_inverse (op0 false) oppw (addw (n := n)). Admitted.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2740"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2741"}},{"Add":{"text":" Definition word_zmodMixin {n} := ZmodMixin addwA addwC add0w (addKw (n := n)).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2824"}},{"Add":{"text":" Canonical word_zmodType {n} := ZmodType (word n) word_zmodMixin.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2893"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2894"}},{"Add":{"text":"End ZmodType. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2911"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":2,"ins":{"up_context":[{"change":2,"pos":3699}],"down_context":[{"change":2,"pos":3727}],"flag":"BLOCK","start":2913,"end":2956,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":3699},"to":{"change":2,"start":3699,"end":3727},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":"Require Import word memory nondeterminism.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:2955"}}],"del_contents":[{"Del":{"text":"Require Import word memory.","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:3726"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":13,"ins":{"up_context":[{"change":2,"pos":4129}],"down_context":[{"change":2,"pos":4224}],"flag":"BLOCK","start":2957,"end":3072,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":4129},"to":{"change":2,"start":4129,"end":4224},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":" I don't know what happens if you try to write to it,","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3017"}},{"Add":{"text":" so I assume anything can happen in that case.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3071"}}],"del_contents":[{"Del":{"text":" I don't know what happens if you try to write to it, so I assume anything is possible.","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:4223"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":20,"ins":{"up_context":[{"change":2,"pos":4498}],"down_context":[{"change":2,"pos":4577}],"flag":"BLOCK","start":3073,"end":3162,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":4498},"to":{"change":2,"start":4498,"end":4577},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":" I don't understand what these do, so I'll assume they can do anything they want.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3161"}}],"del_contents":[{"Del":{"text":" I don't understand what these do, so I'll assume they can do anything.","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:4576"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":34,"ins":{"up_context":[{"change":2,"pos":5040}],"down_context":[{"change":2,"pos":5116}],"flag":"BLOCK","start":3163,"end":3354,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":5040},"to":{"change":2,"start":5040,"end":5116},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":"(* If the processor reads from `addr`,","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3201"}},{"Add":{"text":" while the peripherals are in state `s`,","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3245"}},{"Add":{"text":" what answers could it get?","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3276"}},{"Add":{"text":"*)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3279"}},{"Add":{"text":"Definition read {rom} (addr : word 16) (s : state rom) : nondet (word 8).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3353"}}],"del_contents":[{"Del":{"text":"Definition read {rom} (addr : word 16) (s : state rom) (w : word 8) : Prop.","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:5115"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":43,"ins":{"up_context":[{"change":2,"pos":5199}],"down_context":[{"change":2,"pos":5245}],"flag":"BLOCK","start":3355,"end":3410,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":5199},"to":{"change":2,"start":5199,"end":5245},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":" then determined (get rom (split (n := 4) _).1)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3409"}}],"del_contents":[{"Del":{"text":" then w = get rom (split (n := 4) _).1","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:5244"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":46,"ins":{"up_context":[{"change":2,"pos":5312}],"down_context":[{"change":2,"pos":5330}],"flag":"BLOCK","start":3411,"end":3436,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":5312},"to":{"change":2,"start":5312,"end":5330},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":" then unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3435"}}],"del_contents":[{"Del":{"text":" then True","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:5329"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":49,"ins":{"up_context":[{"change":2,"pos":5394}],"down_context":[{"change":2,"pos":5412}],"flag":"BLOCK","start":3437,"end":3462,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":5394},"to":{"change":2,"start":5394,"end":5412},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":" then unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3461"}}],"del_contents":[{"Del":{"text":" then True","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:5411"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":51,"ins":{"up_context":[{"change":2,"pos":5430}],"down_context":[{"change":2,"pos":5480}],"flag":"BLOCK","start":3463,"end":3522,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":5430},"to":{"change":2,"start":5430,"end":5480},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":" else determined (get (RAM s) (split (n := 9) _).1)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3521"}}],"del_contents":[{"Del":{"text":" else w = get (RAM s) (split (n := 9) _).1","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:5479"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":55,"ins":{"up_context":[{"change":2,"pos":5497}],"down_context":[{"change":2,"pos":5591}],"flag":"BLOCK","start":3523,"end":3794,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":5497},"to":{"change":2,"start":5497,"end":5591},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":"(* If the processor writes `w` to `addr`,","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3564"}},{"Add":{"text":" while the peripherals are in state `s`,","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3608"}},{"Add":{"text":" what states could the peripherals end up in?","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3657"}},{"Add":{"text":" (If I don't know, assume they could.)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3699"}},{"Add":{"text":"*)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3702"}},{"Add":{"text":"Definition write {rom} (addr : word 16) (w : word 8) (s : state rom) : nondet (state rom).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3793"}}],"del_contents":[{"Del":{"text":"Definition write {rom} (addr : word 16) (s : state rom) (w : word 8) (s' : state rom) : Prop.","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:5590"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":65,"ins":{"up_context":[{"change":2,"pos":5674}],"down_context":[{"change":2,"pos":5692}],"flag":"BLOCK","start":3795,"end":3820,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":5674},"to":{"change":2,"start":5674,"end":5692},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":" then unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3819"}}],"del_contents":[{"Del":{"text":" then True","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:5691"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":68,"ins":{"up_context":[{"change":2,"pos":5759}],"down_context":[{"change":2,"pos":5777}],"flag":"BLOCK","start":3821,"end":3846,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":5759},"to":{"change":2,"start":5759,"end":5777},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":" then unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3845"}}],"del_contents":[{"Del":{"text":" then True","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:5776"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":71,"ins":{"up_context":[{"change":2,"pos":5841}],"down_context":[{"change":2,"pos":5859}],"flag":"BLOCK","start":3847,"end":3872,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":5841},"to":{"change":2,"start":5841,"end":5859},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":" then unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3871"}}],"del_contents":[{"Del":{"text":" then True","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:5858"}}]}},{"Replacement":{"inode":{"change":2,"pos":3654},"path":"theories/peripherals.v","line":73,"ins":{"up_context":[{"change":2,"pos":5877}],"down_context":[{"change":2,"pos":5950}],"flag":"BLOCK","start":3873,"end":3954,"inode":{"change":2,"pos":3654}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":5877},"to":{"change":2,"start":5877,"end":5950},"introduced_by":2}],"inode":{"change":2,"pos":3654}},"ins_contents":[{"Add":{"text":" else determined (fromRAM (update (RAM s) (fun=>w) (split (n := 9) _).1))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:3953"}}],"del_contents":[{"Del":{"text":" else s' = fromRAM (update (RAM s) (fun=>w) (split (n := 9) _).1)","pos":"DGOX3ISBTC7HQKYLNHUFUOJMCIOICC2F4IHHPK6OR3LZOKQIWIXAC:5949"}}]}},{"FileAdd":{"meta":{"basename":"nondeterminism.v","metadata":0},"context":[{"change":3,"pos":20}],"contents":[{"Add":{"text":"From mathcomp Require Import all_ssreflect.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4040"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4041"}},{"Add":{"text":"Inductive nondet (T : Type) : Type := fromPossibilities of (T -> Prop).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4113"}},{"Add":{"text":"Arguments fromPossibilities {T}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4146"}},{"Add":{"text":"Definition possible {T} : nondet T -> T -> Prop := fun '(fromPossibilities P) => P.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4230"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4231"}},{"Add":{"text":"Lemma possibleK {T} : cancel possible (fromPossibilities (T := T)). by case. Qed.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4313"}},{"Add":{"text":"Lemma fromPossibilitiesK {T} : cancel fromPossibilities (possible (T := T)). done. Qed.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4401"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4402"}},{"Add":{"text":"(* A fully unspecified value. It can do anything. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4455"}},{"Add":{"text":"Definition unspecified {T} : nondet T := fromPossibilities (fun=> True).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4528"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4529"}},{"Add":{"text":"(* A fully determined value. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4561"}},{"Add":{"text":"Definition determined {T} (x : T) : nondet T := fromPossibilities (eq x).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4635"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4636"}},{"Add":{"text":"(* Apply a nondeterministic function to a nondeterministic value. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4705"}},{"Add":{"text":"Definition bind {A B} (f : A -> nondet B) (n : nondet A) : nondet B :=","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4776"}},{"Add":{"text":" fromPossibilities (fun b => exists a, possible n a /\\ possible (f a) b).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4853"}},{"Add":{"text":"Notation \"x <- y ; z\" := (bind (fun x => z) y)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4900"}},{"Add":{"text":" (at level 20, y at level 100, z at level 200).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:4951"}},{"Add":{"text":"Notation \"' x <- y ; z\" := (bind (fun x => z) y)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5000"}},{"Add":{"text":" (at level 20, x pattern, y at level 100, z at level 200).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5062"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5063"}},{"Add":{"text":"(* Monad laws *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5080"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5081"}},{"Add":{"text":"Lemma nondet_unitl {A B} (f : A -> nondet B) a b","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5130"}},{"Add":{"text":" : possible (x <- determined a; f x) b <-> possible (f a) b.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5194"}},{"Add":{"text":"Proof.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5201"}},{"Add":{"text":" rewrite fromPossibilitiesK.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5233"}},{"Add":{"text":" split.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5244"}},{"Add":{"text":" - move=> [a' [<- pf]]; exact pf.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5281"}},{"Add":{"text":" - move=> pf; exists a; exact (conj Logic.eq_refl pf).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5339"}},{"Add":{"text":"Qed.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5344"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5345"}},{"Add":{"text":"Lemma nondet_unitr {A} (m : nondet A) (a : A)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5391"}},{"Add":{"text":" : possible (x <- m; determined x) a <-> possible m a.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5449"}},{"Add":{"text":"Proof.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5456"}},{"Add":{"text":" rewrite fromPossibilitiesK.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5488"}},{"Add":{"text":" split.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5499"}},{"Add":{"text":" - move=> [a' [pf <-]]; exact pf.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5536"}},{"Add":{"text":" - move=> pf; exists a; exact (conj pf Logic.eq_refl).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5594"}},{"Add":{"text":"Qed.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5599"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5600"}},{"Add":{"text":"Lemma nondet_assoc {A B C} (f : A -> nondet B) (g : B -> nondet C) m c","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5671"}},{"Add":{"text":" : possible (y <- (x <- m; f x); g y) c <-> possible (x <- m; y <- f x; g y) c.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5754"}},{"Add":{"text":"Proof.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5761"}},{"Add":{"text":" rewrite fromPossibilitiesK fromPossibilitiesK fromPossibilitiesK.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5831"}},{"Add":{"text":" split.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5842"}},{"Add":{"text":" - move=> [b [[a [pm pf]] pg]].","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5877"}},{"Add":{"text":" exists a.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5895"}},{"Add":{"text":" split; first exact pm.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5926"}},{"Add":{"text":" rewrite fromPossibilitiesK.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5962"}},{"Add":{"text":" exists b.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:5980"}},{"Add":{"text":" split; [exact pf | exact pg].","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6018"}},{"Add":{"text":" - move=> [a [pm x]].","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6043"}},{"Add":{"text":" rewrite fromPossibilitiesK in x.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6084"}},{"Add":{"text":" move: x => [b [pf pg]].","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6116"}},{"Add":{"text":" exists b.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6134"}},{"Add":{"text":" split; last exact pg.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6164"}},{"Add":{"text":" exists a.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6182"}},{"Add":{"text":" split; [exact pm | exact pf].","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6220"}},{"Add":{"text":"Qed.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6225"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6226"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6227"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6228"}}]}},{"FileAdd":{"meta":{"basename":"atari.v","metadata":0},"context":[{"change":3,"pos":20}],"contents":[{"Add":{"text":"From mathcomp Require Import all_ssreflect ssralg ssrint.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6320"}},{"Add":{"text":"Import GRing.Theory.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6341"}},{"Add":{"text":"Local Open Scope R.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6361"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6362"}},{"Add":{"text":"Require Import nondeterminism word memory peripherals.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6417"}},{"Add":{"text":"From RecordUpdate Require Import RecordSet.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6461"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6462"}},{"Add":{"text":"(* In this file, I precisely describe the behavior of the Atari 2600.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6532"}},{"Add":{"text":" I then define what it means for a state of the Atari to be reachable.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6606"}},{"Add":{"text":" This is necessary to even *state* the theorem we want to prove;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6674"}},{"Add":{"text":" to prove anything about minimum speedrun times, we need to define what it means to run a program!","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6776"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6777"}},{"Add":{"text":" Note that if there is a bug in this specification,","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6832"}},{"Add":{"text":" the final theorem will instead prove a minimum speedrun time *when running Dragster on a buggy Atari*.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6939"}},{"Add":{"text":" This is an unavoidable limitation to the proof.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6991"}},{"Add":{"text":"*)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6994"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6995"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:6996"}},{"Add":{"text":"(* Flags *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7008"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7009"}},{"Add":{"text":"Record flags := {","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7027"}},{"Add":{"text":" FlagN : bool;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7045"}},{"Add":{"text":" FlagV : bool; (* WARNING: I assume the SO pin is unused. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7109"}},{"Add":{"text":" FlagD : bool;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7127"}},{"Add":{"text":" FlagI : bool;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7145"}},{"Add":{"text":" FlagZ : bool;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7163"}},{"Add":{"text":" FlagC : bool;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7181"}},{"Add":{"text":"}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7184"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7185"}},{"Add":{"text":"Instance set_flags : Settable _ := settable! Build_flags","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7242"}},{"Add":{"text":" .","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7290"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7291"}},{"Add":{"text":"Definition word_of_flags (break : bool) (f : flags) : word 8","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7352"}},{"Add":{"text":" := word_of_tuple [tuple ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7381"}},{"Add":{"text":" (FlagC f);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7400"}},{"Add":{"text":" (FlagZ f);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7419"}},{"Add":{"text":" (FlagI f);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7438"}},{"Add":{"text":" (FlagD f);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7457"}},{"Add":{"text":" break;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7472"}},{"Add":{"text":" true;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7486"}},{"Add":{"text":" (FlagV f);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7505"}},{"Add":{"text":" (FlagN f)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7523"}},{"Add":{"text":" ].","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7530"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7531"}},{"Add":{"text":"Definition flags_of_word (w : word 8) : flags.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7578"}},{"Add":{"text":"by refine {|","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7591"}},{"Add":{"text":" FlagC := bit w (Ordinal (m := 0) _);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7632"}},{"Add":{"text":" FlagZ := bit w (Ordinal (m := 1) _);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7673"}},{"Add":{"text":" FlagI := bit w (Ordinal (m := 2) _);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7714"}},{"Add":{"text":" FlagD := bit w (Ordinal (m := 3) _);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7755"}},{"Add":{"text":" FlagV := bit w (Ordinal (m := 6) _);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7796"}},{"Add":{"text":" FlagN := bit w (Ordinal (m := 7) _);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7837"}},{"Add":{"text":"|}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7841"}},{"Add":{"text":"Defined.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7850"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7851"}},{"Add":{"text":"Lemma word_of_flagsK b : cancel (word_of_flags b) flags_of_word.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7916"}},{"Add":{"text":"Proof.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7923"}},{"Add":{"text":" move=> [n v d i z c].","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7949"}},{"Add":{"text":" rewrite /word_of_flags; simpl.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:7984"}},{"Add":{"text":" by rewrite /flags_of_word /bit word_of_tupleK /tnth.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8041"}},{"Add":{"text":"Qed.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8046"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8047"}},{"Add":{"text":"(* State *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8059"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8060"}},{"Add":{"text":"Record state (rom : ROM) := {","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8090"}},{"Add":{"text":" Peripherals : peripherals.state rom;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8131"}},{"Add":{"text":" Flags : flags;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8150"}},{"Add":{"text":" ProgramCounter : word 16;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8180"}},{"Add":{"text":" RegA : word 8;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8199"}},{"Add":{"text":" RegX : word 8;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8218"}},{"Add":{"text":" RegY : word 8;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8237"}},{"Add":{"text":" RegS : word 8; (* Stack Pointer *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8276"}},{"Add":{"text":"}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8279"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8280"}},{"Add":{"text":"Arguments Peripherals {rom}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8309"}},{"Add":{"text":"Arguments Flags {rom}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8332"}},{"Add":{"text":"Arguments ProgramCounter {rom}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8364"}},{"Add":{"text":"Arguments RegA {rom}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8386"}},{"Add":{"text":"Arguments RegX {rom}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8408"}},{"Add":{"text":"Arguments RegY {rom}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8430"}},{"Add":{"text":"Arguments RegS {rom}.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8452"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8453"}},{"Add":{"text":"Instance set_state {rom} : Settable _ := settable! (Build_state rom)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8522"}},{"Add":{"text":" .","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8588"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8589"}},{"Add":{"text":"Definition read {rom} (addr : word 16) (s : state rom) : nondet (word 8)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8662"}},{"Add":{"text":" := peripherals.read addr (Peripherals s).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8708"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8709"}},{"Add":{"text":"Definition write {rom} (addr : word 16) (w : word 8) (s : state rom) : nondet (state rom)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8799"}},{"Add":{"text":" := p <- peripherals.write addr w (Peripherals s); determined (set Peripherals (fun=>p) s).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8894"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8895"}},{"Add":{"text":"(* Flags *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8907"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8908"}},{"Add":{"text":"Definition setZN {rom} (w : word 8) : state rom -> state rom","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8969"}},{"Add":{"text":" := set Flags","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:8986"}},{"Add":{"text":" (fun f => set FlagN (fun=> bit w ord_max)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9036"}},{"Add":{"text":" (set FlagZ (fun=> w == op0 false) f)).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9087"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9088"}},{"Add":{"text":"(* Stack *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9100"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9101"}},{"Add":{"text":"Definition push8 {rom} (w : word 8) (s : state rom) : nondet (state rom). Admitted.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9185"}},{"Add":{"text":"Definition push16 {rom} (w : word 16) (s : state rom) : nondet (state rom). Admitted.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9271"}},{"Add":{"text":"Definition pull8 {rom} (s : state rom) : nondet (word 8 * state rom). Admitted.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9351"}},{"Add":{"text":"Definition pull16 {rom} (s : state rom) : nondet (word 16 * state rom). Admitted.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9433"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9434"}},{"Add":{"text":"(* Addressing Modes *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9457"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9458"}},{"Add":{"text":"Inductive addressing_mode :=","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9487"}},{"Add":{"text":"| Accumulator","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9501"}},{"Add":{"text":"| Immediate","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9513"}},{"Add":{"text":"| Implied","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9523"}},{"Add":{"text":"| Relative","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9534"}},{"Add":{"text":"| Absolute","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9545"}},{"Add":{"text":"| ZeroPage","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9556"}},{"Add":{"text":"| Indirect","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9567"}},{"Add":{"text":"| AbsoluteX","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9579"}},{"Add":{"text":"| AbsoluteY","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9591"}},{"Add":{"text":"| ZeroPageX","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9603"}},{"Add":{"text":"| ZeroPageY","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9615"}},{"Add":{"text":"| IndexedIndirect","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9633"}},{"Add":{"text":"| IndirectIndexed","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9651"}},{"Add":{"text":".","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9653"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9654"}},{"Add":{"text":"Definition mode_width (mode : addressing_mode) : nat := match mode with","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9726"}},{"Add":{"text":" | Accumulator => 0","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9749"}},{"Add":{"text":" | Immediate => 1","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9770"}},{"Add":{"text":" | Implied => 0","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9789"}},{"Add":{"text":" | Relative => 1","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9809"}},{"Add":{"text":" | Absolute => 2","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9829"}},{"Add":{"text":" | ZeroPage => 1","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9849"}},{"Add":{"text":" | Indirect => 2","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9869"}},{"Add":{"text":" | AbsoluteX => 2","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9890"}},{"Add":{"text":" | AbsoluteY => 2","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9911"}},{"Add":{"text":" | ZeroPageX => 1","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9932"}},{"Add":{"text":" | ZeroPageY => 1","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9953"}},{"Add":{"text":" | IndexedIndirect => 1","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:9980"}},{"Add":{"text":" | IndirectIndexed => 1","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10007"}},{"Add":{"text":"end.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10012"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10013"}},{"Add":{"text":"(* Many addressing modes pick out an address in memory. Return that address. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10093"}},{"Add":{"text":"Definition mode_addr {rom} (mode : addressing_mode)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10145"}},{"Add":{"text":":= match mode return word (mode_width mode * 8) -> state rom -> nondet (word 16) with","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10231"}},{"Add":{"text":" | Accumulator => fun _ _ => unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10275"}},{"Add":{"text":" | Immediate => fun _ _ => unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10317"}},{"Add":{"text":" | Implied => fun _ _ => unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10357"}},{"Add":{"text":" | Relative => fun offset s =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10391"}},{"Add":{"text":" determined (addw","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10416"}},{"Add":{"text":" (ProgramCounter s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10447"}},{"Add":{"text":" (concat (offset, op0 (bit offset ord_max))))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10504"}},{"Add":{"text":" | Absolute => fun addr s => determined addr","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10552"}},{"Add":{"text":" | ZeroPage => fun addr s => determined (concat (addr, op0 false))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10622"}},{"Add":{"text":" | Indirect => fun addr s =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10654"}},{"Add":{"text":" (* Annoying edge case. I could specify the behavior here too, but why bother? *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10743"}},{"Add":{"text":" if (split addr).1 == op0 (n := 8) true then unspecified else","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10812"}},{"Add":{"text":" lo <- read addr s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10839"}},{"Add":{"text":" hi <- read (increment 1 addr) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10880"}},{"Add":{"text":" determined (concat (lo, hi))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:10917"}},{"Add":{"text":" | AbsoluteX => fun addr s => determined (addw addr (concat (RegX s, op0 false)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11002"}},{"Add":{"text":" | AbsoluteY => fun addr s => determined (addw addr (concat (RegY s, op0 false)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11087"}},{"Add":{"text":" | ZeroPageX => fun addr s => determined (concat (addw addr (RegX s), op0 false))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11172"}},{"Add":{"text":" | ZeroPageY => fun addr s => determined (concat (addw addr (RegY s), op0 false))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11257"}},{"Add":{"text":" | IndexedIndirect => fun addr s => ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11297"}},{"Add":{"text":" let addr := addw addr (RegX s) in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11339"}},{"Add":{"text":" lo <- read (concat (addr, op0 false)) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11388"}},{"Add":{"text":" hi <- read (concat (increment 1 addr, op0 false)) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11449"}},{"Add":{"text":" determined (concat (lo, hi))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11486"}},{"Add":{"text":" | IndirectIndexed => fun addr s =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11525"}},{"Add":{"text":" lo <- read (concat (addr, op0 false)) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11574"}},{"Add":{"text":" hi <- read (concat (increment 1 addr, op0 false)) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11635"}},{"Add":{"text":" determined (addw (concat (lo, hi)) (concat (RegY s, op0 false)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11708"}},{"Add":{"text":"end.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11713"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11714"}},{"Add":{"text":"(* Read data, using this addressing mode. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11759"}},{"Add":{"text":"Definition mode_read {rom} (mode : addressing_mode)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11811"}},{"Add":{"text":":= match mode return word (mode_width mode * 8) -> state rom -> nondet (word 8) with","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11896"}},{"Add":{"text":" | Accumulator => fun _ s => determined (RegA s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11948"}},{"Add":{"text":" | Immediate => fun w _ => determined w","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:11991"}},{"Add":{"text":" | Implied => fun _ _ => unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12031"}},{"Add":{"text":" | mode => fun bytes s =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12060"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12100"}},{"Add":{"text":" read addr s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12120"}},{"Add":{"text":"end.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12125"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12126"}},{"Add":{"text":"(* Write data, using this addressing mode. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12172"}},{"Add":{"text":"Definition mode_write {rom} (mode : addressing_mode)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12225"}},{"Add":{"text":":= match mode return word (mode_width mode * 8) -> word 8 -> state rom -> nondet (state rom) with","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12323"}},{"Add":{"text":" | Accumulator => fun _ w s => determined (set RegA (fun=>w) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12390"}},{"Add":{"text":" | Immediate => fun _ _ _ => unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12434"}},{"Add":{"text":" | Implied => fun _ _ _ => unspecified","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12476"}},{"Add":{"text":" | mode => fun bytes w s =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12507"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12547"}},{"Add":{"text":" write addr w s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12570"}},{"Add":{"text":"end.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12575"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12576"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12577"}},{"Add":{"text":"(* Instructions *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12596"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12597"}},{"Add":{"text":"Inductive instruction :=","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12622"}},{"Add":{"text":"| ADC | AND | ASL | BCC | BCS | BEQ | BIT | BMI | BNE | BPL | BRK | BVC | BVS | CLC","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12706"}},{"Add":{"text":"| CLD | CLI | CLV | CMP | CPX | CPY | DEC | DEX | DEY | EOR | INC | INX | INY | JMP","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12790"}},{"Add":{"text":"| JSR | LDA | LDX | LDY | LSR | NOP | ORA | PHA | PHP | PLA | PLP | ROL | ROR | RTI","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12874"}},{"Add":{"text":"| RTS | SBC | SEC | SED | SEI | STA | STX | STY | TAX | TAY | TSX | TXA | TXS | TYA","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12958"}},{"Add":{"text":".","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12960"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12961"}},{"Add":{"text":"Definition run_instruction {rom}","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:12994"}},{"Add":{"text":" (instr : instruction)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13020"}},{"Add":{"text":" (mode : addressing_mode)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13049"}},{"Add":{"text":" (bytes : word (mode_width mode * 8))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13090"}},{"Add":{"text":" (s : state rom)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13110"}},{"Add":{"text":" : nondet (state rom)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13135"}},{"Add":{"text":":= match instr with","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13155"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13156"}},{"Add":{"text":" (* Organization based on https://masswerk.at/6502/6502_instruction_set.html *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13239"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13240"}},{"Add":{"text":" (* Transfer Instructions *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13272"}},{"Add":{"text":" | LDA => w <- mode_read mode bytes s; determined (set RegA (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13358"}},{"Add":{"text":" | LDX => w <- mode_read mode bytes s; determined (set RegX (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13444"}},{"Add":{"text":" | LDY => w <- mode_read mode bytes s; determined (set RegY (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13530"}},{"Add":{"text":" | STA => mode_write mode bytes (RegA s) s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13576"}},{"Add":{"text":" | STX => mode_write mode bytes (RegX s) s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13622"}},{"Add":{"text":" | STY => mode_write mode bytes (RegY s) s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13668"}},{"Add":{"text":" | TAX => determined (let w := RegA s in set RegX (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13744"}},{"Add":{"text":" | TAY => determined (let w := RegA s in set RegY (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13820"}},{"Add":{"text":" | TSX => determined (let w := RegS s in set RegX (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13896"}},{"Add":{"text":" | TXA => determined (let w := RegX s in set RegA (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:13972"}},{"Add":{"text":" | TXS => determined (let w := RegX s in set RegS (fun=> w) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14038"}},{"Add":{"text":" | TYA => determined (let w := RegY s in set RegA (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14114"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14115"}},{"Add":{"text":" (* Stack Instructions *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14144"}},{"Add":{"text":" | PHA => push8 (RegA s) s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14174"}},{"Add":{"text":" | PHP => push8 (word_of_flags true (Flags s)) s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14226"}},{"Add":{"text":" | PLA =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14239"}},{"Add":{"text":" '(w, s) <- pull8 s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14267"}},{"Add":{"text":" determined (set RegA (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14319"}},{"Add":{"text":" | PLP =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14332"}},{"Add":{"text":" '(w, s) <- pull8 s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14360"}},{"Add":{"text":" determined (set Flags (fun=> set FlagI (fun=> false) (flags_of_word w)) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14443"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14444"}},{"Add":{"text":" (* Decrements and Increments *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14480"}},{"Add":{"text":" | DEC =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14493"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14530"}},{"Add":{"text":" let w := increment (-1) w in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14567"}},{"Add":{"text":" mode_write mode bytes w (setZN w s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14611"}},{"Add":{"text":" | DEX =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14624"}},{"Add":{"text":" let w := increment (-1) (RegX s) in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14668"}},{"Add":{"text":" determined (set RegX (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14720"}},{"Add":{"text":" | DEY =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14733"}},{"Add":{"text":" let w := increment (-1) (RegY s) in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14777"}},{"Add":{"text":" determined (set RegY (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14829"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14830"}},{"Add":{"text":" | INC =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14843"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14880"}},{"Add":{"text":" let w := increment 1 w in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14914"}},{"Add":{"text":" mode_write mode bytes w (setZN w s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14958"}},{"Add":{"text":" | INX =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:14971"}},{"Add":{"text":" let w := increment 1 (RegX s) in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15012"}},{"Add":{"text":" determined (set RegX (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15064"}},{"Add":{"text":" | INY =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15077"}},{"Add":{"text":" let w := increment 1 (RegY s) in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15118"}},{"Add":{"text":" determined (set RegY (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15170"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15171"}},{"Add":{"text":" (* Arithmetic Operations *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15203"}},{"Add":{"text":" | ADC =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15216"}},{"Add":{"text":" if FlagD (Flags s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15243"}},{"Add":{"text":" then unspecified (* TODO. Note: Only C should be specified. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15314"}},{"Add":{"text":" else","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15327"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15368"}},{"Add":{"text":" let '(w, carryout) := addition (FlagC (Flags s)) (RegA s) w in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15443"}},{"Add":{"text":" overflow <- unspecified;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15480"}},{"Add":{"text":" determined ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15504"}},{"Add":{"text":" (set RegA (fun=> w)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15540"}},{"Add":{"text":" (set Flags","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15571"}},{"Add":{"text":" (fun f =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15605"}},{"Add":{"text":" set FlagC (fun=> carryout) ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15661"}},{"Add":{"text":" (set FlagV (fun=> overflow) f))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15725"}},{"Add":{"text":" (setZN w s)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15763"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15764"}},{"Add":{"text":" | SBC =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15777"}},{"Add":{"text":" if FlagD (Flags s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15804"}},{"Add":{"text":" then unspecified (* TODO. Note: Only C should be specified. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15875"}},{"Add":{"text":" else","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15888"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:15929"}},{"Add":{"text":" let '(w, carryout) := subtraction (FlagC (Flags s)) (RegA s) w in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16007"}},{"Add":{"text":" overflow <- unspecified;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16044"}},{"Add":{"text":" determined ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16068"}},{"Add":{"text":" (set RegA (fun=> w)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16104"}},{"Add":{"text":" (set Flags","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16135"}},{"Add":{"text":" (fun f =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16169"}},{"Add":{"text":" set FlagC (fun=> carryout) ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16225"}},{"Add":{"text":" (set FlagV (fun=> overflow) f))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16289"}},{"Add":{"text":" (setZN w s)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16327"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16328"}},{"Add":{"text":" (* Logical Operations *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16357"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16358"}},{"Add":{"text":" | AND =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16371"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16408"}},{"Add":{"text":" let w := op2 andb (RegA s) w in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16448"}},{"Add":{"text":" determined (set RegA (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16500"}},{"Add":{"text":" | ORA =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16513"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16550"}},{"Add":{"text":" let w := op2 orb (RegA s) w in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16589"}},{"Add":{"text":" determined (set RegA (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16641"}},{"Add":{"text":" | EOR =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16654"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16691"}},{"Add":{"text":" let w := op2 addb (RegA s) w in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16731"}},{"Add":{"text":" determined (set RegA (fun=> w) (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16783"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16784"}},{"Add":{"text":" (* Shift & Rotate Instructions *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16822"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16823"}},{"Add":{"text":" | ASL =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16836"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16873"}},{"Add":{"text":" let '(w, b) := popHigh (pushLow (false, w)) in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:16928"}},{"Add":{"text":" determined (set RegA (fun=> w) (set Flags (set FlagC (fun=>b)) (setZN w s)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17013"}},{"Add":{"text":" | LSR =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17026"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17063"}},{"Add":{"text":" let '(b, w) := popLow (pushHigh (w, false)) in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17118"}},{"Add":{"text":" determined (set RegA (fun=> w) (set Flags (set FlagC (fun=>b)) (setZN w s)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17203"}},{"Add":{"text":" | ROL =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17216"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17253"}},{"Add":{"text":" let '(w, b) := popHigh (pushLow (FlagC (Flags s), w)) in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17318"}},{"Add":{"text":" determined (set RegA (fun=> w) (set Flags (set FlagC (fun=>b)) (setZN w s)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17403"}},{"Add":{"text":" | ROR =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17416"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17453"}},{"Add":{"text":" let '(b, w) := popLow (pushHigh (w, FlagC (Flags s))) in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17518"}},{"Add":{"text":" determined (set RegA (fun=> w) (set Flags (set FlagC (fun=>b)) (setZN w s)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17603"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17604"}},{"Add":{"text":" (* Flag Instructions *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17632"}},{"Add":{"text":" | CLC => determined (set Flags (set FlagC (fun=> false)) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17696"}},{"Add":{"text":" | CLD => determined (set Flags (set FlagD (fun=> false)) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17760"}},{"Add":{"text":" | CLI => determined (set Flags (set FlagI (fun=> false)) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17824"}},{"Add":{"text":" | CLV => determined (set Flags (set FlagV (fun=> false)) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17888"}},{"Add":{"text":" | SEC => determined (set Flags (set FlagC (fun=> true)) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:17951"}},{"Add":{"text":" | SED => determined (set Flags (set FlagD (fun=> true)) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18014"}},{"Add":{"text":" | SEI => determined (set Flags (set FlagI (fun=> true)) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18077"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18078"}},{"Add":{"text":" (* Comparisons *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18100"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18101"}},{"Add":{"text":" | CMP =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18114"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18151"}},{"Add":{"text":" let '(w, carryout) := subtraction true (RegA s) w in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18212"}},{"Add":{"text":" determined ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18232"}},{"Add":{"text":" (set Flags","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18255"}},{"Add":{"text":" (set FlagC (fun=> carryout))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18300"}},{"Add":{"text":" (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18329"}},{"Add":{"text":" | CPX =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18342"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18379"}},{"Add":{"text":" let '(w, carryout) := subtraction true (RegX s) w in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18440"}},{"Add":{"text":" determined ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18460"}},{"Add":{"text":" (set Flags","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18483"}},{"Add":{"text":" (set FlagC (fun=> carryout))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18528"}},{"Add":{"text":" (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18557"}},{"Add":{"text":" | CPY =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18570"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18607"}},{"Add":{"text":" let '(w, carryout) := subtraction true (RegY s) w in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18668"}},{"Add":{"text":" determined ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18688"}},{"Add":{"text":" (set Flags","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18711"}},{"Add":{"text":" (set FlagC (fun=> carryout))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18756"}},{"Add":{"text":" (setZN w s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18785"}},{"Add":{"text":" ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18810"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18811"}},{"Add":{"text":" (* Conditional Branch Instructions *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18853"}},{"Add":{"text":" | BCS =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18866"}},{"Add":{"text":" if FlagC (Flags s) then","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18900"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:18944"}},{"Add":{"text":" determined (set ProgramCounter (fun=> addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19003"}},{"Add":{"text":" else determined s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19029"}},{"Add":{"text":" | BCC =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19042"}},{"Add":{"text":" if ~~FlagC (Flags s) then","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19076"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19120"}},{"Add":{"text":" determined (set ProgramCounter (fun=> addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19179"}},{"Add":{"text":" else determined s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19205"}},{"Add":{"text":" | BEQ =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19218"}},{"Add":{"text":" if FlagZ (Flags s) then","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19252"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19296"}},{"Add":{"text":" determined (set ProgramCounter (fun=> addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19355"}},{"Add":{"text":" else determined s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19381"}},{"Add":{"text":" | BNE =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19394"}},{"Add":{"text":" if ~~FlagZ (Flags s) then","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19428"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19472"}},{"Add":{"text":" determined (set ProgramCounter (fun=> addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19531"}},{"Add":{"text":" else determined s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19557"}},{"Add":{"text":" | BVS =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19570"}},{"Add":{"text":" if FlagV (Flags s) then","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19604"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19648"}},{"Add":{"text":" determined (set ProgramCounter (fun=> addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19707"}},{"Add":{"text":" else determined s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19733"}},{"Add":{"text":" | BVC =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19746"}},{"Add":{"text":" if ~~FlagV (Flags s) then","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19780"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19824"}},{"Add":{"text":" determined (set ProgramCounter (fun=> addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19883"}},{"Add":{"text":" else determined s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19909"}},{"Add":{"text":" | BMI =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19922"}},{"Add":{"text":" if FlagN (Flags s) then","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:19956"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20000"}},{"Add":{"text":" determined (set ProgramCounter (fun=> addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20059"}},{"Add":{"text":" else determined s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20085"}},{"Add":{"text":" | BPL =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20098"}},{"Add":{"text":" if ~~FlagN (Flags s) then","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20132"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20176"}},{"Add":{"text":" determined (set ProgramCounter (fun=> addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20235"}},{"Add":{"text":" else determined s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20261"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20262"}},{"Add":{"text":" (* Jumps & Subroutines *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20292"}},{"Add":{"text":" | JMP =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20305"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20345"}},{"Add":{"text":" determined (set ProgramCounter (fun=> addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20400"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20401"}},{"Add":{"text":" | JSR =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20414"}},{"Add":{"text":" addr <- mode_addr mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20454"}},{"Add":{"text":" push16 (increment (-1) (ProgramCounter s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20505"}},{"Add":{"text":" (set ProgramCounter (fun=> addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20553"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20554"}},{"Add":{"text":" | RTS =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20567"}},{"Add":{"text":" '(addr, s) <- pull16 s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20599"}},{"Add":{"text":" determined (set ProgramCounter (fun=> increment 1 addr) s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20666"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20667"}},{"Add":{"text":" (* Interrupts *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20688"}},{"Add":{"text":" | BRK => ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20702"}},{"Add":{"text":" s <- push16 (increment (-1) (ProgramCounter s)) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20761"}},{"Add":{"text":" s <- push8 (word_of_flags true (Flags s)) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20814"}},{"Add":{"text":" lo <- read (pushLow (false, op0 true)) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20864"}},{"Add":{"text":" hi <- read (pushLow (true, op0 true)) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20913"}},{"Add":{"text":" determined","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:20932"}},{"Add":{"text":" (set ProgramCounter (fun=> concat (lo : word 8, hi : word 8))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21006"}},{"Add":{"text":" (set Flags (set FlagI (fun=> true)) s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21062"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21063"}},{"Add":{"text":" | RTI =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21076"}},{"Add":{"text":" '(f, s) <- pull8 s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21104"}},{"Add":{"text":" '(addr, s) <- pull16 s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21136"}},{"Add":{"text":" determined","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21155"}},{"Add":{"text":" (set ProgramCounter (fun=> addr)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21200"}},{"Add":{"text":" (set Flags (fun=> set FlagI (fun=> false) (flags_of_word f)) s))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21281"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21282"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21283"}},{"Add":{"text":" (* Other *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21299"}},{"Add":{"text":" | BIT =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21312"}},{"Add":{"text":" w <- mode_read mode bytes s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21349"}},{"Add":{"text":" determined (set Flags ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21380"}},{"Add":{"text":" (fun f =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21402"}},{"Add":{"text":" (set FlagZ (fun=> op2 andb (RegA s) w == op0 false)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21470"}},{"Add":{"text":" (set FlagN (fun=> bit w (Ordinal (m := 7) (leqnn _)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21544"}},{"Add":{"text":" (set FlagV (fun=> bit w (Ordinal (m := 6) (leqnSn _)))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21623"}},{"Add":{"text":" f))))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21657"}},{"Add":{"text":" s)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21668"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21669"}},{"Add":{"text":" | NOP => determined s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21695"}},{"Add":{"text":"end.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21700"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21701"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21702"}},{"Add":{"text":"(* Given an opcode, return the corresponding instruction and addressing mode.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21780"}},{"Add":{"text":" Return `None` if the opcode is invalid.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21824"}},{"Add":{"text":"*)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21827"}},{"Add":{"text":"Definition parse_opcode (w : word 8) : option (instruction * addressing_mode)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21905"}},{"Add":{"text":":= match nat_of_word w with","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21933"}},{"Add":{"text":" | 0x00 => Some (BRK, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:21967"}},{"Add":{"text":" | 0x01 => Some (ORA, IndexedIndirect)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22009"}},{"Add":{"text":" | 0x05 => Some (ORA, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22044"}},{"Add":{"text":" | 0x06 => Some (ASL, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22079"}},{"Add":{"text":" | 0x08 => Some (PHP, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22113"}},{"Add":{"text":" | 0x09 => Some (ORA, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22149"}},{"Add":{"text":" | 0x0a => Some (ASL, Accumulator)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22187"}},{"Add":{"text":" | 0x0d => Some (ORA, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22222"}},{"Add":{"text":" | 0x0e => Some (ASL, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22257"}},{"Add":{"text":" | 0x10 => Some (BPL, Relative)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22292"}},{"Add":{"text":" | 0x11 => Some (ORA, IndirectIndexed)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22334"}},{"Add":{"text":" | 0x15 => Some (ORA, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22370"}},{"Add":{"text":" | 0x16 => Some (ASL, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22406"}},{"Add":{"text":" | 0x18 => Some (CLC, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22440"}},{"Add":{"text":" | 0x19 => Some (ORA, AbsoluteY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22476"}},{"Add":{"text":" | 0x1d => Some (ORA, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22512"}},{"Add":{"text":" | 0x1e => Some (ASL, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22548"}},{"Add":{"text":" | 0x20 => Some (JSR, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22583"}},{"Add":{"text":" | 0x21 => Some (AND, IndexedIndirect)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22625"}},{"Add":{"text":" | 0x24 => Some (BIT, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22660"}},{"Add":{"text":" | 0x25 => Some (AND, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22695"}},{"Add":{"text":" | 0x26 => Some (ROL, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22730"}},{"Add":{"text":" | 0x28 => Some (PLP, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22764"}},{"Add":{"text":" | 0x29 => Some (AND, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22800"}},{"Add":{"text":" | 0x2a => Some (ROL, Accumulator)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22838"}},{"Add":{"text":" | 0x2c => Some (BIT, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22873"}},{"Add":{"text":" | 0x2d => Some (AND, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22908"}},{"Add":{"text":" | 0x2e => Some (ROL, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22943"}},{"Add":{"text":" | 0x30 => Some (BMI, Relative)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:22978"}},{"Add":{"text":" | 0x31 => Some (AND, IndirectIndexed)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23020"}},{"Add":{"text":" | 0x35 => Some (AND, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23056"}},{"Add":{"text":" | 0x36 => Some (ROL, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23092"}},{"Add":{"text":" | 0x38 => Some (SEC, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23126"}},{"Add":{"text":" | 0x39 => Some (AND, AbsoluteY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23162"}},{"Add":{"text":" | 0x3d => Some (AND, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23198"}},{"Add":{"text":" | 0x3e => Some (ROL, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23234"}},{"Add":{"text":" | 0x40 => Some (RTI, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23268"}},{"Add":{"text":" | 0x41 => Some (EOR, IndexedIndirect)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23310"}},{"Add":{"text":" | 0x45 => Some (EOR, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23345"}},{"Add":{"text":" | 0x46 => Some (LSR, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23380"}},{"Add":{"text":" | 0x48 => Some (PHA, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23414"}},{"Add":{"text":" | 0x49 => Some (EOR, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23450"}},{"Add":{"text":" | 0x4a => Some (LSR, Accumulator)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23488"}},{"Add":{"text":" | 0x4c => Some (JMP, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23523"}},{"Add":{"text":" | 0x4d => Some (EOR, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23558"}},{"Add":{"text":" | 0x4e => Some (LSR, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23593"}},{"Add":{"text":" | 0x50 => Some (BVC, Relative)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23628"}},{"Add":{"text":" | 0x51 => Some (EOR, IndirectIndexed)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23670"}},{"Add":{"text":" | 0x55 => Some (EOR, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23706"}},{"Add":{"text":" | 0x56 => Some (LSR, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23742"}},{"Add":{"text":" | 0x58 => Some (CLI, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23776"}},{"Add":{"text":" | 0x59 => Some (EOR, AbsoluteY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23812"}},{"Add":{"text":" | 0x5d => Some (EOR, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23848"}},{"Add":{"text":" | 0x5e => Some (LSR, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23884"}},{"Add":{"text":" | 0x60 => Some (RTS, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23918"}},{"Add":{"text":" | 0x61 => Some (ADC, IndexedIndirect)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23960"}},{"Add":{"text":" | 0x65 => Some (ADC, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:23995"}},{"Add":{"text":" | 0x66 => Some (ROR, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24030"}},{"Add":{"text":" | 0x68 => Some (PLA, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24064"}},{"Add":{"text":" | 0x69 => Some (ADC, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24100"}},{"Add":{"text":" | 0x6a => Some (ROR, Accumulator)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24138"}},{"Add":{"text":" | 0x6c => Some (JMP, Indirect)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24173"}},{"Add":{"text":" | 0x6d => Some (ADC, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24208"}},{"Add":{"text":" | 0x6e => Some (ROR, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24244"}},{"Add":{"text":" | 0x70 => Some (BVS, Relative)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24279"}},{"Add":{"text":" | 0x71 => Some (ADC, IndirectIndexed)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24321"}},{"Add":{"text":" | 0x75 => Some (ADC, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24357"}},{"Add":{"text":" | 0x76 => Some (ROR, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24393"}},{"Add":{"text":" | 0x78 => Some (SEI, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24427"}},{"Add":{"text":" | 0x79 => Some (ADC, AbsoluteY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24463"}},{"Add":{"text":" | 0x7d => Some (ADC, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24499"}},{"Add":{"text":" | 0x7e => Some (ROR, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24534"}},{"Add":{"text":" | 0x81 => Some (STA, IndexedIndirect)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24576"}},{"Add":{"text":" | 0x84 => Some (STY, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24611"}},{"Add":{"text":" | 0x85 => Some (STA, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24646"}},{"Add":{"text":" | 0x86 => Some (STX, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24681"}},{"Add":{"text":" | 0x88 => Some (DEY, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24715"}},{"Add":{"text":" | 0x8a => Some (TXA, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24749"}},{"Add":{"text":" | 0x8c => Some (STY, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24784"}},{"Add":{"text":" | 0x8d => Some (STA, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24819"}},{"Add":{"text":" | 0x8e => Some (STX, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24854"}},{"Add":{"text":" | 0x90 => Some (BCC, Relative)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24889"}},{"Add":{"text":" | 0x91 => Some (STA, IndirectIndexed)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24931"}},{"Add":{"text":" | 0x94 => Some (STY, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:24967"}},{"Add":{"text":" | 0x95 => Some (STA, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25003"}},{"Add":{"text":" | 0x96 => Some (STX, ZeroPageY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25039"}},{"Add":{"text":" | 0x98 => Some (TYA, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25073"}},{"Add":{"text":" | 0x99 => Some (STA, AbsoluteY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25109"}},{"Add":{"text":" | 0x9a => Some (TXS, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25143"}},{"Add":{"text":" | 0x9d => Some (STA, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25179"}},{"Add":{"text":" | 0xa0 => Some (LDY, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25215"}},{"Add":{"text":" | 0xa1 => Some (LDA, IndexedIndirect)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25257"}},{"Add":{"text":" | 0xa2 => Some (LDX, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25293"}},{"Add":{"text":" | 0xa4 => Some (LDY, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25328"}},{"Add":{"text":" | 0xa5 => Some (LDA, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25363"}},{"Add":{"text":" | 0xa6 => Some (LDX, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25398"}},{"Add":{"text":" | 0xa8 => Some (TAY, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25432"}},{"Add":{"text":" | 0xa9 => Some (LDA, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25468"}},{"Add":{"text":" | 0xaa => Some (TAX, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25502"}},{"Add":{"text":" | 0xac => Some (LDY, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25537"}},{"Add":{"text":" | 0xad => Some (LDA, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25572"}},{"Add":{"text":" | 0xae => Some (LDX, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25607"}},{"Add":{"text":" | 0xb0 => Some (BCS, Relative)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25642"}},{"Add":{"text":" | 0xb1 => Some (LDA, IndirectIndexed)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25684"}},{"Add":{"text":" | 0xb4 => Some (LDY, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25720"}},{"Add":{"text":" | 0xb5 => Some (LDA, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25756"}},{"Add":{"text":" | 0xb6 => Some (LDX, ZeroPageY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25792"}},{"Add":{"text":" | 0xb8 => Some (CLV, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25826"}},{"Add":{"text":" | 0xb9 => Some (LDA, AbsoluteY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25862"}},{"Add":{"text":" | 0xba => Some (TSX, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25896"}},{"Add":{"text":" | 0xbc => Some (LDY, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25932"}},{"Add":{"text":" | 0xbd => Some (LDA, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:25968"}},{"Add":{"text":" | 0xbe => Some (LDX, AbsoluteY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26004"}},{"Add":{"text":" | 0xc0 => Some (CPY, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26040"}},{"Add":{"text":" | 0xc1 => Some (CMP, IndexedIndirect)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26082"}},{"Add":{"text":" | 0xc4 => Some (CPY, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26117"}},{"Add":{"text":" | 0xc5 => Some (CMP, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26152"}},{"Add":{"text":" | 0xc6 => Some (DEC, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26187"}},{"Add":{"text":" | 0xc8 => Some (INY, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26221"}},{"Add":{"text":" | 0xc9 => Some (CMP, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26257"}},{"Add":{"text":" | 0xca => Some (DEX, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26291"}},{"Add":{"text":" | 0xcc => Some (CPY, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26326"}},{"Add":{"text":" | 0xcd => Some (CMP, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26361"}},{"Add":{"text":" | 0xce => Some (DEC, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26396"}},{"Add":{"text":" | 0xd0 => Some (BNE, Relative)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26431"}},{"Add":{"text":" | 0xd1 => Some (CMP, IndirectIndexed)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26473"}},{"Add":{"text":" | 0xd5 => Some (CMP, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26509"}},{"Add":{"text":" | 0xd6 => Some (DEC, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26545"}},{"Add":{"text":" | 0xd8 => Some (CLD, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26579"}},{"Add":{"text":" | 0xd9 => Some (CMP, AbsoluteY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26615"}},{"Add":{"text":" | 0xdd => Some (CMP, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26651"}},{"Add":{"text":" | 0xde => Some (DEC, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26687"}},{"Add":{"text":" | 0xe0 => Some (CPX, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26723"}},{"Add":{"text":" | 0xe1 => Some (SBC, IndexedIndirect)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26765"}},{"Add":{"text":" | 0xe4 => Some (CPX, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26800"}},{"Add":{"text":" | 0xe5 => Some (SBC, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26835"}},{"Add":{"text":" | 0xe6 => Some (INC, ZeroPage)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26870"}},{"Add":{"text":" | 0xe8 => Some (INX, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26904"}},{"Add":{"text":" | 0xe9 => Some (SBC, Immediate)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26940"}},{"Add":{"text":" | 0xea => Some (NOP, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:26974"}},{"Add":{"text":" | 0xec => Some (CPX, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27009"}},{"Add":{"text":" | 0xed => Some (SBC, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27044"}},{"Add":{"text":" | 0xee => Some (INC, Absolute)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27079"}},{"Add":{"text":" | 0xf0 => Some (BEQ, Relative)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27114"}},{"Add":{"text":" | 0xf1 => Some (SBC, IndirectIndexed)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27156"}},{"Add":{"text":" | 0xf5 => Some (SBC, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27192"}},{"Add":{"text":" | 0xf6 => Some (INC, ZeroPageX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27228"}},{"Add":{"text":" | 0xf8 => Some (SED, Implied)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27262"}},{"Add":{"text":" | 0xf9 => Some (SBC, AbsoluteY)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27298"}},{"Add":{"text":" | 0xfd => Some (SBC, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27334"}},{"Add":{"text":" | 0xfe => Some (INC, AbsoluteX)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27370"}},{"Add":{"text":" | _ => None","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27386"}},{"Add":{"text":"end.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27391"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27392"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27393"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27394"}},{"Add":{"text":"(* Program Execution *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27418"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27419"}},{"Add":{"text":"Definition init {rom} : nondet (state rom) :=","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27465"}},{"Add":{"text":" (* Begin in an arbitrary state. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27504"}},{"Add":{"text":" s <- unspecified;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27526"}},{"Add":{"text":" (* Jump to the address contained in the reset vector. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27587"}},{"Add":{"text":" run_instruction JMP Indirect (pushLow (false, pushLow (false, op0 true))) s.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27668"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27669"}},{"Add":{"text":"Definition step {rom} (s : state rom) : nondet (state rom) :=","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27731"}},{"Add":{"text":" (* Read the opcode. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27758"}},{"Add":{"text":" op <- read (ProgramCounter s) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27795"}},{"Add":{"text":" if parse_opcode op is Some (instr, mode)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27840"}},{"Add":{"text":" then ","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27850"}},{"Add":{"text":" let s := set ProgramCounter (increment 1) s in","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27905"}},{"Add":{"text":" (* Read the remaining bytes in the instruction *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27963"}},{"Add":{"text":" '(s, bytes) <-","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:27986"}},{"Add":{"text":" nat_rect (* basically a for loop *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28034"}},{"Add":{"text":" (fun n => nondet (state rom * word (n * 8)))%type","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28100"}},{"Add":{"text":" (determined (s, trivial_word))","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28147"}},{"Add":{"text":" (fun _ m =>","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28175"}},{"Add":{"text":" '(s, acc) <- m;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28211"}},{"Add":{"text":" w <- read (ProgramCounter s) s;","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28263"}},{"Add":{"text":" (* I can make a `word (n * 8 + 8)`, but need a word ((n.+1) * 8).","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28349"}},{"Add":{"text":" `eq_rect` does the conversion.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28404"}},{"Add":{"text":" *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28427"}},{"Add":{"text":" determined","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28458"}},{"Add":{"text":" ( set ProgramCounter (increment 1) s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28519"}},{"Add":{"text":" , eq_rect _ _ (concat (acc, w)) _ (addnC _ _)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28589"}},{"Add":{"text":" )","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28615"}},{"Add":{"text":" )","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28633"}},{"Add":{"text":" (mode_width mode);","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28668"}},{"Add":{"text":" (* Run the instruction. *)","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28703"}},{"Add":{"text":" run_instruction instr mode bytes s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28746"}},{"Add":{"text":" else unspecified.","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28768"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28769"}},{"Add":{"text":"Inductive reachable {rom : ROM} : state rom -> Type :=","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28824"}},{"Add":{"text":"| Init s : possible init s -> reachable s","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28866"}},{"Add":{"text":"| Step s1 s2 : reachable s1 -> possible (step s1) s2 -> reachable s2","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28935"}},{"Add":{"text":".","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28937"}}]}},{"Edit":{"inode":{"change":3,"pos":58},"path":"_CoqProject","line":1,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":58}],"down_context":[{"change":3,"pos":11903}],"flag":"BLOCK","start":28938,"end":28965,"inode":{"change":3,"pos":58}}},"contents":[{"Add":{"text":"theories/nondeterminism.v","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28963"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28964"}}]}},{"Replacement":{"inode":{"change":3,"pos":58},"path":"_CoqProject","line":6,"ins":{"up_context":[{"change":2,"pos":8633}],"down_context":[{"change":2,"pos":8634}],"flag":"BLOCK","start":28966,"end":28983,"inode":{"change":3,"pos":58}},"del":{"edges":[{"previous":"","flag":"DELETED","from":{"change":2,"pos":8633},"to":{"change":3,"start":80,"end":81},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":3,"pos":11919},"to":{"change":3,"start":80,"end":81},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":80},"to":{"change":3,"start":80,"end":81},"introduced_by":3}],"inode":{"change":3,"pos":58}},"ins_contents":[{"Add":{"text":"theories/atari.v","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28982"}}],"del_contents":[{"Del":{"text":"","pos":"GVKFJJTTO257PW7OYH7NMFNUY4QMUIXATMXVWTN7PDIFBSNZ3IYQC:80"}}]}},{"Edit":{"inode":{"change":6,"pos":34},"path":"README.md","line":16,"atom":{"NewVertex":{"up_context":[{"change":6,"pos":1238}],"down_context":[],"flag":"BLOCK","start":28984,"end":29101,"inode":{"change":6,"pos":34}}},"contents":[{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28984"}},{"Add":{"text":"# Dependencies","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:28999"}},{"Add":{"text":"","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:29000"}},{"Add":{"text":"- coq 8.13.2","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:29013"}},{"Add":{"text":"- coq-record-update 0.3.0","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:29039"}},{"Add":{"text":"- coq-mathcomp-ssreflect 1.14.0","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:29071"}},{"Add":{"text":"- coq-mathcomp-algebra 1.14.0","pos":"3XT4NIINMDSDTALK46WDXSRSDZS7XTRJ7UP43JNFQB64XI6U3W2QC:29101"}}]}}],"owner":"finegeometer","repo":"atari-proofs","token":"ytaPY8z7bxuAP8+c6HU4bCz9mqgjarijY78mRkCwDT8=","login":null}

…

Dependencies

Change contents

Review