rocq/Run.v

(* The decoder's passes carried out by the ring machine. A pass is the organism's G steps followed by
   the empty slots of the active bank; the pass that hands over ends with the organism's steps. *)
From Stdlib Require Import List Bool Arith ZArith Lia.
Import ListNotations.
From TH Require Import TwoHead Net Abstract Indep Spec Organism PassCheck PassLemma Decoder PhysMain.

(* the idle bank read as a tape: its bits, the arm on bit bs * 26 + bj *)
Definition btape (q : bank) : tape := mkT (bq q) (bs q * 26 + bj q).

Lemma advb_tape : forall S0 q, bs q < S0 -> bj q < 26 ->
  bq (advb S0 26 q) = bq q
  /\ bs (advb S0 26 q) * 26 + bj (advb S0 26 q) = succ_mod (S0 * 26) (bs q * 26 + bj q)
  /\ bs (advb S0 26 q) < S0 /\ bj (advb S0 26 q) < 26.
Proof.
  intros S0 [X s j] Hs Hj. cbn [bs bj] in *. unfold advb, succ_mod. cbn [bq bs bj].
  destruct (Nat.eqb_spec (S j) 26) as [E|E]; cbn [bq bs bj].
  - destruct (Nat.eqb_spec (S s) S0) as [E2|E2];
      destruct (Nat.eqb_spec (S (s * 26 + j)) (S0 * 26)) as [E3|E3]; repeat split; first [reflexivity | lia].
  - destruct (Nat.eqb_spec (S (s * 26 + j)) (S0 * 26)) as [E3|E3]; repeat split; first [reflexivity | lia].
Qed.

Lemma iter_advb_tape : forall S0 n q, bs q < S0 -> bj q < 26 ->
  bq (iter n (advb S0 26) q) = bq q
  /\ bs (iter n (advb S0 26) q) * 26 + bj (iter n (advb S0 26) q) = iter n (succ_mod (S0 * 26)) (bs q * 26 + bj q)
  /\ bs (iter n (advb S0 26) q) < S0 /\ bj (iter n (advb S0 26) q) < 26.
Proof.
  intros S0 n q Hs Hj. induction n as [|n IH]; [cbn [iter]; repeat split; assumption|].
  destruct IH as (Hq & Hp & Hs' & Hj'). cbn [iter].
  destruct (advb_tape S0 (iter n (advb S0 26) q) Hs' Hj') as (Aq & Ap & As & Aj).
  rewrite Aq, Ap, Hp, Hq. repeat split; assumption.
Qed.

(* the arm's effect on the bank, read on the bank as a tape *)
Lemma btape_eff : forall S0 h q, bs q < S0 -> bj q < 26 ->
  btape (bank_eff S0 26 h q) = tape_eff (S0 * 26) h (btape q)
  /\ bs (bank_eff S0 26 h q) < S0 /\ bj (bank_eff S0 26 h q) < 26.
Proof.
  intros S0 [c w mv rw cl] q Hs Hj. unfold bank_eff, tape_eff, btape. cbn [acl awr amv arw td th].
  set (C := if cl then repeat false (S0 * 26)
            else match w with Some v => upd (bq q) (bs q * 26 + bj q) v | None => bq q end).
  destruct (iter_advb_tape S0 mv (mkB C (if rw then 0 else bs q) (if rw then 0 else bj q))
              ltac:(cbn [bs]; destruct rw; lia) ltac:(cbn [bj]; destruct rw; lia)) as (Hq & Hp & Hs' & Hj').
  cbn [bq bs bj] in Hq, Hp. rewrite Hq, Hp. split; [|split; assumption].
  destruct rw; reflexivity.
Qed.

Lemma btape_zero : forall q C, btape q = mkT C 0 -> q = mkB C 0 0.
Proof.
  intros [X s j] C H. unfold btape in H. cbn [bq bs bj] in H. injection H as -> Hp.
  assert (s = 0) by lia. assert (j = 0) by lia. subst. reflexivity.
Qed.

Lemma decode_zero : decodeA 6 (repeat false 26) = Rec 0 0 0 0 0 0.
Proof. reflexivity. Qed.

Lemma upd_false : forall w c, wget w c = false -> upd w c false = w.
Proof. intros w c H. unfold wget in H. rewrite <- H. apply upd_same. Qed.

(* the request cells of a window are clear *)
Definition reqclear (w : list bool) : Prop := forall c, AR <= c <= HO -> wget w c = false.

Lemma clearq_id : forall w, reqclear w -> clearq w = w.
Proof.
  intros w H. unfold clearq.
  rewrite (upd_false w AR), (upd_false w AA), (upd_false w AC), (upd_false w RR), (upd_false w RA),
    (upd_false w RC), (upd_false w CB), (upd_false w CT), (upd_false w HO); try reflexivity;
    apply H; unfold AR, AA, AC, RR, RA, RC, CB, CT, HO; lia.
Qed.

Lemma wcfg_req : forall cf, reqclear (wcfg cf).
Proof.
  intros cf c Hc. unfold wget, wcfg. rewrite nth_map_seq by (unfold AR, HO in Hc; lia).
  unfold AR, HO in Hc.
  destruct c as [|[|[|[|[|[|[|[|[|[|[|[|[|c]]]]]]]]]]]]]; try lia; reflexivity.
Qed.

Lemma map_nth_self : forall (A : Type) (l : list A) d, map (fun x => nth x l d) (seq 0 (length l)) = l.
Proof.
  intros A l d. induction l as [|a l IH]; [reflexivity|].
  cbn [length seq map nth]. f_equal. rewrite <- seq_shift, map_map. exact IH.
Qed.

(* the cells no step writes: those below the requests, and the temporaries no record of the organism
   writes *)
Definition fixedcell (i : nat) : Prop := i < AR \/ (27 <= i /\ ~ In i (map ao_of organism)).

Lemma step_low : forall al K S0 L s i, i < AR -> wget (win (step al K S0 L s)) i = wget (win s) i.
Proof.
  intros al K S0 L s i Hi. unfold step.
  destruct (decodeA al (slot al (nth (kap s) (banks s) bank0))) as [a0 w0 a1 w1 beta ao].
  unfold stepres. cbv zeta. cbn [win].
  rewrite wget_clearq_out by (left; exact Hi).
  unfold wnext. destruct (Nat.leb_spec ao CPY) as [E|E]; [reflexivity|].
  rewrite wget_upd. replace (Nat.eqb i ao) with false by (symmetry; apply Nat.eqb_neq; unfold AR, CPY in *; lia).
  reflexivity.
Qed.

Lemma itern_low : forall al K S0 L n s i, i < AR -> wget (win (itern al K S0 L n s)) i = wget (win s) i.
Proof.
  intros al K S0 L n. induction n as [|n IH]; intros s i Hi; [reflexivity|].
  cbn [itern]. rewrite IH by exact Hi. apply step_low. exact Hi.
Qed.

Section Run.
Variables (K S0 L : nat).
Hypotheses (HK : 2 <= K) (HS : G <= S0) (HL : 1 <= L).

Lemma HS1 : 1 <= S0.
Proof. pose proof length_organism. lia. Qed.

(* ---- an empty slot changes nothing but the slot of the active bank ----------------------------- *)
Lemma empty_step : forall s, fits 6 K S0 L s -> reqclear (win s) ->
  slot 6 (nth (kap s) (banks s) bank0) = repeat false 26 ->
  win (step 6 K S0 L s) = win s /\ kap (step 6 K S0 L s) = kap s /\ tapes (step 6 K S0 L s) = tapes s
  /\ (forall x, x < K -> nth x (banks (step 6 K S0 L s)) bank0 =
        if Nat.eqb x (kap s)
        then mkB (bq (nth x (banks s) bank0)) (succ_mod S0 (bs (nth x (banks s) bank0))) (bj (nth x (banks s) bank0))
        else nth x (banks s) bank0).
Proof.
  intros s Hf Hq Hslot. destruct Hf as (Hlw & Hk & HlB & HlT & HB & HT).
  assert (Hst : step 6 K S0 L s = stepres 6 K S0 L s 0 true) by (unfold step; rewrite Hslot, decode_zero; reflexivity).
  assert (Hreq : forall c, AR <= c <= HO -> wget (wnext (win s) 0 true) c = false) by exact Hq.
  rewrite Hst. unfold stepres. cbv zeta.
  change (wnext (win s) 0 true) with (win s).
  rewrite (Hq RR), (Hq AR), (Hq AA), (Hq AC), (Hq RA), (Hq RC), (Hq CB), (Hq CT), (Hq HO)
    by (unfold AR, AA, AC, RR, RA, RC, CB, CT, HO; lia).
  change (Nat.eqb 0 ARM) with false. change (Nat.eqb 0 CPY) with false. cbv iota beta.
  cbn [win kap banks tapes]. rewrite (clearq_id _ Hq).
  refine (conj eq_refl (conj eq_refl (conj _ _))).
  - transitivity (map (fun x => nth x (tapes s) tape0) (seq 0 K)); [|rewrite <- HlT; apply map_nth_self].
    apply map_ext_in. intros x _. destruct (Nat.eqb_spec x (kap s)) as [->|]; [apply eta_tape|].
    destruct (Nat.eqb_spec x (succ_mod K (kap s))) as [->|]; [apply eta_tape | reflexivity].
  - intros x Hx. rewrite nth_map_seq by exact Hx. cbn [bq bs bj].
    destruct (Nat.eqb_spec x (kap s)) as [->|]; [reflexivity|].
    destruct (Nat.eqb_spec x (succ_mod K (kap s))) as [->|]; [apply eta_bank | reflexivity].
Qed.

(* the empty slots from the slot after the organism to the last bring the active bank back to slot 0 *)
Lemma empty_steps : forall n s, fits 6 K S0 L s -> reqclear (win s) ->
  bq (nth (kap s) (banks s) bank0) = enc organism ++ repeat false ((S0 - G) * 26) ->
  G <= bs (nth (kap s) (banks s) bank0) -> bs (nth (kap s) (banks s) bank0) + S n = S0 ->
  win (itern 6 K S0 L (S n) s) = win s /\ kap (itern 6 K S0 L (S n) s) = kap s
  /\ tapes (itern 6 K S0 L (S n) s) = tapes s
  /\ (forall x, x < K -> nth x (banks (itern 6 K S0 L (S n) s)) bank0 =
        if Nat.eqb x (kap s) then mkB (bq (nth x (banks s) bank0)) 0 (bj (nth x (banks s) bank0))
        else nth x (banks s) bank0).
Proof.
  induction n as [|n IH]; intros s Hf Hq Hact HG Hn.
  - assert (Hslot : slot 6 (nth (kap s) (banks s) bank0) = repeat false 26).
    { unfold slot. rewrite Hact. apply slot_empty; unfold G in *; lia. }
    destruct (empty_step s Hf Hq Hslot) as (Hw & Hk & Ht & Hb).
    cbn [itern]. refine (conj Hw (conj Hk (conj Ht _))).
    intros x Hx. rewrite (Hb x Hx). destruct (Nat.eqb_spec x (kap s)) as [->|]; [|reflexivity].
    unfold succ_mod. replace (Nat.eqb (S (bs (nth (kap s) (banks s) bank0))) S0) with true
      by (symmetry; apply Nat.eqb_eq; lia). reflexivity.
  - assert (Hslot : slot 6 (nth (kap s) (banks s) bank0) = repeat false 26).
    { unfold slot. rewrite Hact. apply slot_empty; unfold G in *; lia. }
    destruct (empty_step s Hf Hq Hslot) as (Hw & Hk & Ht & Hb).
    assert (Hf1 : fits 6 K S0 L (step 6 K S0 L s)) by exact (itern_fits 6 K S0 L 1 s ltac:(lia) HK HS1 HL Hf).
    pose proof (Hb (kap s) ltac:(destruct Hf as (_ & H & _); exact H)) as Ha.
    rewrite Nat.eqb_refl in Ha.
    assert (Hsucc : succ_mod S0 (bs (nth (kap s) (banks s) bank0)) = S (bs (nth (kap s) (banks s) bank0))).
    { unfold succ_mod. replace (Nat.eqb (S (bs (nth (kap s) (banks s) bank0))) S0) with false
        by (symmetry; apply Nat.eqb_neq; lia). reflexivity. }
    destruct (IH (step 6 K S0 L s) Hf1 ltac:(rewrite Hw; exact Hq)
                ltac:(rewrite Hk, Ha; exact Hact) ltac:(rewrite Hk, Ha; cbn [bs]; lia)
                ltac:(rewrite Hk, Ha; cbn [bs]; lia)) as (Hw' & Hk' & Ht' & Hb').
    change (itern 6 K S0 L (S (S n)) s) with (itern 6 K S0 L (S n) (step 6 K S0 L s)).
    refine (conj _ (conj _ (conj _ _))); [congruence | congruence | congruence |].
    intros x Hx. rewrite (Hb' x Hx), Hk.
    destruct (Nat.eqb_spec x (kap s)) as [->|E]; [rewrite Ha; reflexivity|].
    rewrite (Hb x Hx). apply Nat.eqb_neq in E. rewrite E. reflexivity.
Qed.

(* ---- the machine carries the decoder ------------------------------------------------------------ *)
(* the state s carries the decoder state t: the organism in the active bank from slot 0, the decoder's
   configuration in the window, its read tape, arm and copy tape in the roles of the bank kap s *)
Definition mrel (t : dst) (s : st) : Prop :=
  fits 6 K S0 L s
  /\ bq (nth (kap s) (banks s) bank0) = enc organism ++ repeat false ((S0 - G) * 26)
  /\ bs (nth (kap s) (banks s) bank0) = 0
  /\ (forall i, relevant i = true -> wget (win s) i = wget (wcfg (dc t)) i)
  /\ reachable (dc t) = true
  /\ nth (kap s) (tapes s) tape0 = dR t
  /\ btape (nth (succ_mod K (kap s)) (banks s) bank0) = dA t
  /\ nth (succ_mod K (kap s)) (tapes s) tape0 = dK t.

Lemma k_lt : forall s, fits 6 K S0 L s -> kap s < K.
Proof. intros s (_ & H & _). exact H. Qed.

Lemma i_lt : forall s, fits 6 K S0 L s -> succ_mod K (kap s) < K.
Proof. intros s Hf. pose proof (k_lt s Hf). unfold succ_mod. destruct (Nat.eqb_spec (S (kap s)) K); lia. Qed.

Lemma i_k : forall s, fits 6 K S0 L s -> succ_mod K (kap s) <> kap s.
Proof. intros s Hf. pose proof (k_lt s Hf). unfold succ_mod. destruct (Nat.eqb_spec (S (kap s)) K); lia. Qed.

Lemma bank_ok : forall s x, fits 6 K S0 L s -> x < K ->
  length (bq (nth x (banks s) bank0)) = S0 * 26 /\ bs (nth x (banks s) bank0) < S0 /\ bj (nth x (banks s) bank0) < 26.
Proof. intros s x (_ & _ & _ & _ & H & _) Hx. exact (H x Hx). Qed.

(* the organism's pass in the machine, with the machine's view of the three heads *)
Lemma organism_pass : forall t s, mrel t s ->
  let s1 := itern 6 K S0 L G s in
  fits 6 K S0 L s1
  /\ kap s1 = (if ho (dout t) then succ_mod K (kap s) else kap s)
  /\ (forall i, relevant i = true -> wget (win s1) i = wget (wcfg (dc (dstep (S0 * 26) L t))) i)
  /\ nth (kap s) (banks s1) bank0 = mkB (bq (nth (kap s) (banks s) bank0)) (G mod S0) (bj (nth (kap s) (banks s) bank0))
  /\ btape (nth (succ_mod K (kap s)) (banks s1) bank0) = dA (dstep (S0 * 26) L t)
  /\ nth (kap s) (tapes s1) tape0 = dR (dstep (S0 * 26) L t)
  /\ nth (succ_mod K (kap s)) (tapes s1) tape0 = dK (dstep (S0 * 26) L t)
  /\ (forall x, x < K -> x <> kap s -> x <> succ_mod K (kap s) ->
        nth x (banks s1) bank0 = nth x (banks s) bank0 /\ nth x (tapes s1) tape0 = nth x (tapes s) tape0)
  /\ (forall i, 4 <= i -> wget (win s1) i
                         = wget (aw (aiter G organism (start_ast (win s) (tget (dR t)) (tget (dA t)) (tget (dK t))))) i).
Proof.
  intros t s (Hf & Hact & Hslot & Hw & Hreach & HRt & HAt & HKt) s1.
  pose proof (i_lt s Hf) as Hi.
  destruct (bank_ok s (succ_mod K (kap s)) Hf Hi) as (_ & HIs & HIj).
  destruct (machine_pass K S0 L s HK HS HL Hf Hact Hslot (dc t) (tget (dR t)) (tget (dA t)) (tget (dK t)) (dout t)
              Hreach Hw ltac:(rewrite HRt; reflexivity) ltac:(rewrite <- HAt; reflexivity)
              ltac:(rewrite HKt; reflexivity) eq_refl)
    as (Hw1 & _ & Hk1 & _ & _ & HA1 & HI1 & HR1 & HC1 & HoB & HoT & _ & Hwin).
  fold s1 in Hw1, Hk1, HA1, HI1, HR1, HC1, HoB, HoT, Hwin.
  destruct (btape_eff S0 (expA (dout t) (tget (dA t))) (nth (succ_mod K (kap s)) (banks s) bank0) HIs HIj)
    as (Hbt & _ & _).
  refine (conj (itern_fits 6 K S0 L G s ltac:(lia) HK HS1 HL Hf) (conj Hk1 (conj Hw1 (conj HA1 (conj _
            (conj _ (conj _ (conj _ Hwin)))))))).
  - rewrite HI1, Hbt, HAt. reflexivity.
  - rewrite HR1, HRt. reflexivity.
  - rewrite HC1, HKt. reflexivity.
  - intros x Hx H1 H2. split; [apply HoB | apply HoT]; assumption.
Qed.

(* a pass that does not hand over: the organism's steps and the empty slots *)
Lemma quiet_pass : forall t s, mrel t s -> ho (dout t) = false ->
  let s2 := itern 6 K S0 L S0 s in
  mrel (dstep (S0 * 26) L t) s2 /\ kap s2 = kap s
  /\ nth (kap s) (banks s2) bank0 = nth (kap s) (banks s) bank0
  /\ (forall x, x < K -> x <> kap s -> x <> succ_mod K (kap s) ->
        nth x (banks s2) bank0 = nth x (banks s) bank0 /\ nth x (tapes s2) tape0 = nth x (tapes s) tape0)
  /\ win s2 = win (itern 6 K S0 L G s).
Proof.
  intros t s Hm Hho s2.
  destruct (organism_pass t s Hm) as (Hf1 & Hk1 & Hw1 & HA1 & HI1 & HR1 & HC1 & Ho1 & _).
  rewrite Hho in Hk1.
  destruct Hm as (Hf & Hact & Hslot & _ & Hreach & _ & _ & _).
  pose proof (k_lt s Hf) as Hk. pose proof (i_lt s Hf) as Hi. pose proof (i_k s Hf) as Hik.
  set (s1 := itern 6 K S0 L G s) in *.
  assert (Hq1 : reqclear (win s1)).
  { intros c Hc. rewrite Hw1 by (unfold relevant; apply andb_true_iff; split; apply Nat.leb_le;
                                 unfold AR, HO in Hc; lia). apply wcfg_req. exact Hc. }
  (* after the organism's steps the active bank is at slot G mod S0 *)
  assert (Hrest : exists s2', s2 = s2' /\ fits 6 K S0 L s2' /\ win s2' = win s1 /\ kap s2' = kap s1
                  /\ tapes s2' = tapes s1
                  /\ (forall x, x < K -> nth x (banks s2') bank0 =
                        if Nat.eqb x (kap s) then nth (kap s) (banks s) bank0 else nth x (banks s1) bank0)).
  { destruct (Nat.eq_dec G S0) as [E|E].
    - exists s1. split; [unfold s2, s1; rewrite E; reflexivity|].
      refine (conj Hf1 (conj eq_refl (conj eq_refl (conj eq_refl _)))).
      intros x Hx. destruct (Nat.eqb_spec x (kap s)) as [->|]; [|reflexivity].
      rewrite HA1, E, Nat.Div0.mod_same, <- Hslot. apply eta_bank.
    - assert (En : exists n, S0 - G = S n) by (exists (S0 - G - 1); lia). destruct En as [n En].
      assert (Hs2 : s2 = itern 6 K S0 L (S n) s1) by (unfold s2, s1; rewrite <- itern_add; f_equal; lia).
      rewrite Nat.mod_small in HA1 by lia.
      destruct (empty_steps n s1 Hf1 Hq1 ltac:(rewrite Hk1, HA1; exact Hact) ltac:(rewrite Hk1, HA1; cbn [bs]; lia)
                  ltac:(rewrite Hk1, HA1; cbn [bs]; lia)) as (Hw2 & Hk2 & Ht2 & Hb2).
      exists (itern 6 K S0 L (S n) s1). refine (conj Hs2 (conj _ (conj Hw2 (conj Hk2 (conj Ht2 _))))).
      + exact (itern_fits 6 K S0 L (S n) s1 ltac:(lia) HK HS1 HL Hf1).
      + intros x Hx. rewrite (Hb2 x Hx), Hk1. destruct (Nat.eqb_spec x (kap s)) as [->|]; [|reflexivity].
        rewrite HA1. cbn [bq bj]. rewrite <- Hslot. apply eta_bank. }
  destruct Hrest as (s2' & -> & Hf2 & Hw2 & Hk2 & Ht2 & Hb2).
  assert (Hk2' : kap s2' = kap s) by congruence.
  pose proof (Hb2 (kap s) Hk) as HA2. rewrite Nat.eqb_refl in HA2.
  pose proof (Hb2 (succ_mod K (kap s)) Hi) as HI2. replace (Nat.eqb (succ_mod K (kap s)) (kap s)) with false in HI2
    by (symmetry; apply Nat.eqb_neq; exact Hik).
  refine (conj _ (conj Hk2' (conj HA2 (conj _ Hw2)))).
  - unfold mrel. rewrite Hk2', HA2, HI2, Ht2.
    refine (conj Hf2 (conj Hact (conj Hslot (conj _ (conj _ (conj HR1 (conj HI1 HC1))))))).
    + intros i Hr. rewrite Hw2. exact (Hw1 i Hr).
    + unfold dstep. cbn [dc]. apply reach_step. exact Hreach.
  - intros x Hx H1 H2. rewrite (Hb2 x Hx), Ht2. apply Nat.eqb_neq in H1. rewrite H1. exact (Ho1 x Hx (proj1 (Nat.eqb_neq _ _) H1) H2).
Qed.

(* the passes before the hand-over *)
Lemma run_quiet : forall n t s, mrel t s -> quiet (S0 * 26) L n t ->
  mrel (dsteps (S0 * 26) L n t) (itern 6 K S0 L (n * S0) s)
  /\ kap (itern 6 K S0 L (n * S0) s) = kap s
  /\ nth (kap s) (banks (itern 6 K S0 L (n * S0) s)) bank0 = nth (kap s) (banks s) bank0
  /\ (forall x, x < K -> x <> kap s -> x <> succ_mod K (kap s) ->
        nth x (banks (itern 6 K S0 L (n * S0) s)) bank0 = nth x (banks s) bank0
        /\ nth x (tapes (itern 6 K S0 L (n * S0) s)) tape0 = nth x (tapes s) tape0).
Proof.
  induction n as [|n IH]; intros t s Hm Hq.
  - cbn [itern Nat.mul dsteps]. refine (conj Hm (conj eq_refl (conj eq_refl _))). intros; split; reflexivity.
  - destruct (quiet_pass t s Hm (Hq 0 ltac:(lia))) as (Hm1 & Hk1 & HA1 & Ho1 & _).
    assert (Hq' : quiet (S0 * 26) L n (dstep (S0 * 26) L t)) by (intros j Hj; exact (Hq (S j) ltac:(lia))).
    destruct (IH _ _ Hm1 Hq') as (Hm2 & Hk2 & HA2 & Ho2).
    change (S n * S0) with (S0 + n * S0). rewrite itern_add. cbn [dsteps].
    rewrite Hk1 in Hk2, HA2, Ho2.
    refine (conj Hm2 (conj Hk2 (conj _ _))); [congruence|].
    intros x Hx H1 H2. destruct (Ho2 x Hx H1 H2) as [B T]. destruct (Ho1 x Hx H1 H2) as [B' T'].
    split; congruence.
Qed.

Lemma dsteps_last : forall N n t, dsteps N L (S n) t = dstep N L (dsteps N L n t).
Proof. intros N n t. rewrite <- Nat.add_1_r, dsteps_add. reflexivity. Qed.

(* ---- universal construction ------------------------------------------------------------------ *)
(* Let the active bank hold the organism from slot 0, the window a configuration of phase I, and the
   read tape a description d of an image X of records that fits the bank, followed by any cells;
   whatever the idle bank, the copy tape and the other cells hold. After one pass per bit of d,
   30 per record of X and 5 more, each of S0 steps but the last, of G, the idle bank holds X from
   slot 0, the copy tape d from cell 0, and the next bank is active: from the next step on the
   machine evaluates the records of X. *)
Theorem universal_construction : forall d X tail s zc c3 c2 c1 c0 m,
  translate d = Some X -> length X <= S0 * 26 -> length d <= L -> zc <= 31 -> fits 6 K S0 L s ->
  bq (nth (kap s) (banks s) bank0) = enc organism ++ repeat false ((S0 - G) * 26) ->
  bs (nth (kap s) (banks s) bank0) = 0 ->
  (forall i, relevant i = true -> wget (win s) i = wget (wcfg (mkC PI zc c3 c2 c1 c0 m)) i) ->
  td (nth (kap s) (tapes s) tape0) = d ++ tail ->
  exists nrec, length X = 26 * nrec /\
  let s' := itern 6 K S0 L ((30 * nrec + 4 + length d) * S0 + G) s in
  fits 6 K S0 L s' /\ kap s' = succ_mod K (kap s)
  /\ nth (succ_mod K (kap s)) (banks s') bank0 = mkB (X ++ repeat false (S0 * 26 - length X)) 0 0
  /\ nth (succ_mod K (kap s)) (tapes s') tape0 = mkT (d ++ repeat false (L - length d)) 0
  /\ nth (kap s) (banks s') bank0
     = mkB (bq (nth (kap s) (banks s) bank0)) (G mod S0) (bj (nth (kap s) (banks s) bank0))
  /\ nth (kap s) (tapes s') tape0 = mkT (d ++ tail) (length d mod L)
  /\ (forall i, relevant i = true -> wget (win s') i = wget (wcfg (mkC PI 1 true true true true false)) i)
  /\ (forall x, x < K -> x <> kap s -> x <> succ_mod K (kap s) ->
        nth x (banks s') bank0 = nth x (banks s) bank0 /\ nth x (tapes s') tape0 = nth x (tapes s) tape0).
Proof.
  intros d X tail s zc c3 c2 c1 c0 m Ht HX Hd Hz Hf Hact Hslot Hw HR.
  set (t0 := mkD (mkC PI zc c3 c2 c1 c0 m) (nth (kap s) (tapes s) tape0)
                 (btape (nth (succ_mod K (kap s)) (banks s) bank0)) (nth (succ_mod K (kap s)) (tapes s) tape0)).
  assert (Hm : mrel t0 s).
  { refine (conj Hf (conj Hact (conj Hslot (conj Hw (conj _ (conj eq_refl (conj eq_refl eq_refl))))))).
    unfold reachable. cbn [dc ph Spec.z t0]. apply Nat.leb_le. exact Hz. }
  destruct (generation (S0 * 26) L ltac:(pose proof HS1; lia) HL d X tail (nth (kap s) (tapes s) tape0)
              (btape (nth (succ_mod K (kap s)) (banks s) bank0)) (nth (succ_mod K (kap s)) (tapes s) tape0)
              zc c3 c2 c1 c0 m Ht HR Hd HX) as (nrec & Hn & Q & H & E).
  fold t0 in Q, H, E.
  exists nrec. split; [exact Hn|]. cbv zeta.
  set (P := 30 * nrec + 4 + length d) in *.
  destruct (run_quiet P t0 s Hm Q) as (Hm1 & Hk1 & HA1 & Ho1).
  set (s1 := itern 6 K S0 L (P * S0) s) in *.
  destruct (organism_pass (dsteps (S0 * 26) L P t0) s1 Hm1) as (Hf2 & Hk2 & Hw2 & HA2 & HI2 & HR2 & HC2 & Ho2 & _).
  rewrite H, Hk1 in Hk2. rewrite Hk1 in HA2, HI2, HR2, HC2, Ho2.
  rewrite <- dsteps_last, E in Hw2, HI2, HR2, HC2. cbn [dc dR dA dK] in Hw2, HI2, HR2, HC2.
  assert (Hs' : itern 6 K S0 L (P * S0 + G) s = itern 6 K S0 L G s1) by (unfold s1; apply itern_add).
  rewrite Hs'.
  pose proof (k_lt s Hf) as Hk. pose proof (i_lt s Hf) as Hi. pose proof (i_k s Hf) as Hik.
  refine (conj Hf2 (conj Hk2 (conj _ (conj HC2 (conj _ (conj _ (conj Hw2 _))))))).
  - apply btape_zero. exact HI2.
  - rewrite HA2, HA1. reflexivity.
  - rewrite HR2. reflexivity.
  - intros x Hx H1 H2. destruct (Ho2 x Hx H1 H2) as [B T]. destruct (Ho1 x Hx H1 H2) as [B' T']. split; congruence.
Qed.

(* ---- the window over a generation ------------------------------------------------------------- *)
(* An organism pass keeps the fixed cells and leaves every other cell from 4 on as a function of the
   decoder's state alone. *)
Lemma organism_pass_window : forall t s, mrel t s ->
  (forall i, fixedcell i -> wget (win (itern 6 K S0 L G s)) i = wget (win s) i)
  /\ (forall i, 4 <= i -> istmp i = false \/ In i (map ao_of organism) ->
        wget (win (itern 6 K S0 L G s)) i
        = wget (aw (aiter G organism (start_ast (wcfg (dc t)) (tget (dR t)) (tget (dA t)) (tget (dK t))))) i).
Proof.
  intros t s (Hf & Hact & Hslot & Hw & Hreach & HRt & HAt & HKt).
  destruct (machine_pass K S0 L s HK HS HL Hf Hact Hslot (dc t) (tget (dR t)) (tget (dA t)) (tget (dK t)) (dout t)
              Hreach Hw ltac:(rewrite HRt; reflexivity) ltac:(rewrite <- HAt; reflexivity)
              ltac:(rewrite HKt; reflexivity) eq_refl)
    as (_ & _ & _ & _ & _ & _ & _ & _ & _ & _ & _ & Hdet & Hfull).
  split; [|exact Hdet].
  intros i [Hi|(Hi & Hn)]; [apply itern_low; exact Hi|].
  rewrite (Hfull i ltac:(lia)). apply aiter_unwritten; [unfold HO; lia | exact Hn].
Qed.

Lemma quiet_pass_fixed : forall t s, mrel t s -> ho (dout t) = false ->
  forall i, fixedcell i -> wget (win (itern 6 K S0 L S0 s)) i = wget (win s) i.
Proof.
  intros t s Hm Hho i Hi. destruct (quiet_pass t s Hm Hho) as (_ & _ & _ & _ & Hw2).
  rewrite Hw2. exact (proj1 (organism_pass_window t s Hm) i Hi).
Qed.

Lemma run_quiet_fixed : forall n t s, mrel t s -> quiet (S0 * 26) L n t ->
  forall i, fixedcell i -> wget (win (itern 6 K S0 L (n * S0) s)) i = wget (win s) i.
Proof.
  induction n as [|n IH]; intros t s Hm Hq i Hi; [reflexivity|].
  destruct (quiet_pass t s Hm (Hq 0 ltac:(lia))) as (Hm1 & _).
  change (S n * S0) with (S0 + n * S0). rewrite itern_add.
  rewrite (IH _ _ Hm1 (fun j Hj => Hq (S j) ltac:(lia)) i Hi).
  exact (quiet_pass_fixed t s Hm (Hq 0 ltac:(lia)) i Hi).
Qed.

(* Over a generation the fixed cells keep their values, and every other cell from 4 on ends as a
   function of the hand-over pass's decoder state, which depends only on d, the cells after it on the
   read tape and the codon register of phase I. *)
Theorem uc_window : forall d X tail s zc c3 c2 c1 c0 m,
  translate d = Some X -> length X <= S0 * 26 -> length d <= L -> zc <= 31 -> fits 6 K S0 L s ->
  bq (nth (kap s) (banks s) bank0) = enc organism ++ repeat false ((S0 - G) * 26) ->
  bs (nth (kap s) (banks s) bank0) = 0 ->
  (forall i, relevant i = true -> wget (win s) i = wget (wcfg (mkC PI zc c3 c2 c1 c0 m)) i) ->
  td (nth (kap s) (tapes s) tape0) = d ++ tail ->
  exists nrec, length X = 26 * nrec /\
  let s' := itern 6 K S0 L ((30 * nrec + 4 + length d) * S0 + G) s in
  let tH := dsteps (S0 * 26) L (30 * nrec + 4 + length d - 1)
              (mkD (mkC PC 3 c3 c2 c1 c0 false) (mkT (d ++ tail) 0) (mkT (repeat false (S0 * 26)) 0)
                   (mkT (repeat false L) 0)) in
  (forall i, fixedcell i -> wget (win s') i = wget (win s) i)
  /\ (forall i, 4 <= i -> istmp i = false \/ In i (map ao_of organism) ->
        wget (win s') i
        = wget (aw (aiter G organism (start_ast (wcfg (dc tH)) (tget (dR tH)) (tget (dA tH)) (tget (dK tH))))) i).
Proof.
  intros d X tail s zc c3 c2 c1 c0 m Ht HX Hd Hz Hf Hact Hslot Hw HR.
  set (t0 := mkD (mkC PI zc c3 c2 c1 c0 m) (nth (kap s) (tapes s) tape0)
                 (btape (nth (succ_mod K (kap s)) (banks s) bank0)) (nth (succ_mod K (kap s)) (tapes s) tape0)).
  assert (Hm : mrel t0 s).
  { refine (conj Hf (conj Hact (conj Hslot (conj Hw (conj _ (conj eq_refl (conj eq_refl eq_refl))))))).
    unfold reachable. cbn [dc ph Spec.z t0]. apply Nat.leb_le. exact Hz. }
  destruct (generation (S0 * 26) L ltac:(pose proof HS1; lia) HL d X tail (nth (kap s) (tapes s) tape0)
              (btape (nth (succ_mod K (kap s)) (banks s) bank0)) (nth (succ_mod K (kap s)) (tapes s) tape0)
              zc c3 c2 c1 c0 m Ht HR Hd HX) as (nrec & Hn & Q & _ & _).
  fold t0 in Q.
  exists nrec. split; [exact Hn|]. cbv zeta.
  pose proof (translate_aux_long _ _ _ Ht) as Hd4.
  set (P := 30 * nrec + 4 + length d) in *.
  destruct (run_quiet P t0 s Hm Q) as (Hm1 & _).
  pose proof (run_quiet_fixed P t0 s Hm Q) as Hfx.
  set (s1 := itern 6 K S0 L (P * S0) s) in *.
  destruct (organism_pass_window (dsteps (S0 * 26) L P t0) s1 Hm1) as [Hfx2 Hdet].
  assert (Hs' : itern 6 K S0 L (P * S0 + G) s = itern 6 K S0 L G s1) by (unfold s1; apply itern_add).
  assert (HP : dsteps (S0 * 26) L P t0
               = dsteps (S0 * 26) L (P - 1) (mkD (mkC PC 3 c3 c2 c1 c0 false) (mkT (d ++ tail) 0)
                                                 (mkT (repeat false (S0 * 26)) 0) (mkT (repeat false L) 0))).
  { replace P with (S (P - 1)) at 1 by lia. cbn [dsteps]. f_equal. unfold t0.
    destruct (pass_PI (S0 * 26) L zc c3 c2 c1 c0 m (nth (kap s) (tapes s) tape0)
                (btape (nth (succ_mod K (kap s)) (banks s) bank0)) (nth (succ_mod K (kap s)) (tapes s) tape0))
      as [_ E0].
    rewrite E0, HR. reflexivity. }
  rewrite Hs'. split.
  - intros i Hi. rewrite (Hfx2 i Hi). exact (Hfx i Hi).
  - intros i H4 Hi. rewrite (Hdet i H4 Hi), HP. reflexivity.
Qed.

End Run.