Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper
a9ea017 | (* What one pass of the organism is meant to do, written without reference to its records. *) | |
| From Stdlib Require Import List Bool Arith ZArith Lia. | |
| Import ListNotations. | |
| From TH Require Import TwoHead. | |
| (* I starts a generation; C reads a codon, G the gate bits, A the address bits *) | |
| Inductive phase := PI | PC | PG | PA. | |
| (* the codon register holds c3 c2 c1 c0, c3 the first bit read; z counts down; mo is the copy mode *) | |
| Record cfg := mkC { ph : phase; z : nat; c3 : bool; c2 : bool; c1 : bool; c0 : bool; mo : bool }. | |
| (* the gate bit at position 7 - z of a gate codon *) | |
| Definition table (a3 a2 s0 s1 : bool) (k : nat) : bool := | |
| let cpy := a3 && negb a2 in | |
| let sign := if a3 then s0 else if a2 then s0 && s1 else s0 || s1 in | |
| let odd := if a3 then s0 else xorb a2 (xorb s0 s1) in | |
| match k with | |
| | 7 => negb s0 | |
| | 6 => s0 | |
| | 5 => negb cpy && negb s1 | |
| | 4 => negb cpy && s1 | |
| | 3 | 2 | 1 => sign | |
| | 0 => odd | |
| | _ => false | |
| end. | |
| Definition is_esc (a3 a2 a1 a0 : bool) : bool := a3 && a2 && negb (a1 && a0). | |
| Definition is_end (a3 a2 a1 a0 : bool) : bool := a3 && a2 && a1 && a0. | |
| (* one pass, from the bit r under the read head: the next configuration; whether the read head moves, | |
| whether the arm writes av and moves, whether the copy head writes r and moves; whether the read head | |
| returns to its origin, whether the arm and the copy head do, whether the idle bank and the copy tape | |
| are cleared, and whether the pass hands over *) | |
| Record out := mkO { ncf : cfg; cons : bool; emit : bool; av : bool; cw : bool; | |
| rr : bool; home : bool; fresh : bool; ho : bool }. | |
| Definition dpass (cf : cfg) (r : bool) : out := | |
| let m := mo cf in | |
| let zero := Nat.eqb (z cf) 0 in | |
| match ph cf with | |
| | PI => mkO (mkC PC 3 (c3 cf) (c2 cf) (c1 cf) (c0 cf) false) false false false false true true true false | |
| | PC => | |
| let n3 := c2 cf in let n2 := c1 cf in let n1 := c0 cf in let n0 := r in | |
| if zero then | |
| if is_end n3 n2 n1 n0 then | |
| if m then mkO (mkC PI 1 n3 n2 n1 n0 false) true false false true false true false true | |
| else mkO (mkC PC 3 n3 n2 n1 n0 true) true false false false true false false false | |
| else if negb m || is_esc n3 n2 n1 n0 then mkO (mkC PG 7 n3 n2 n1 n0 m) true false false m false false false false | |
| else mkO (mkC PA 17 n3 n2 n1 n0 m) true false false m false false false false | |
| else mkO (mkC PC (z cf - 1) n3 n2 n1 n0 m) true false false m false false false false | |
| | PG => | |
| let e := is_esc (c3 cf) (c2 cf) (c1 cf) (c0 cf) in | |
| let a := if e then r else table (c3 cf) (c2 cf) (c1 cf) (c0 cf) (z cf) in | |
| let nx := if zero then mkC PA 17 (c3 cf) (c2 cf) (c1 cf) (c0 cf) m | |
| else mkC PG (z cf - 1) (c3 cf) (c2 cf) (c1 cf) (c0 cf) m in | |
| mkO nx e (negb m) a (m && e) false false false false | |
| | PA => | |
| let nx := if zero then mkC PC 3 (c3 cf) (c2 cf) (c1 cf) (c0 cf) m | |
| else mkC PA (z cf - 1) (c3 cf) (c2 cf) (c1 cf) (c0 cf) m in | |
| mkO nx true (negb m) r m false false false false | |
| end. | |
| (* the configurations a run visits *) | |
| Definition reachable (cf : cfg) : bool := | |
| match ph cf with PI => Nat.leb (z cf) 31 | PC => Nat.leb (z cf) 3 | PG => Nat.leb (z cf) 7 | PA => Nat.leb (z cf) 17 end. | |
| (* the window cells that hold the configuration: m 13, I 14, C 15, G 16, Ad 17, c0..c3 18..21, z 22..26 *) | |
| Definition cell_of_cfg (cf : cfg) (i : nat) : bool := | |
| match i with | |
| | 13 => mo cf | |
| | 14 => match ph cf with PI => true | _ => false end | |
| | 15 => match ph cf with PC => true | _ => false end | |
| | 16 => match ph cf with PG => true | _ => false end | |
| | 17 => match ph cf with PA => true | _ => false end | |
| | 18 => c0 cf | 19 => c1 cf | 20 => c2 cf | 21 => c3 cf | |
| | 22 => Nat.testbit (z cf) 0 | 23 => Nat.testbit (z cf) 1 | 24 => Nat.testbit (z cf) 2 | |
| | 25 => Nat.testbit (z cf) 3 | 26 => Nat.testbit (z cf) 4 | |
| | _ => false | |
| end. | |
| Definition wcfg (cf : cfg) : list bool := map (cell_of_cfg cf) (seq 0 64). | |
| (* the cells a pass carries over: the requests and the configuration; cells 0 to 3 are not held *) | |
| Definition relevant (i : nat) : bool := Nat.leb 4 i && Nat.leb i 26. | |
| Definition istmp (i : nat) : bool := Nat.leb 27 i. | |