(* The pass of the spec iterated over a generation. The read tape, the idle bank read as a tape of
   N cells and the copy tape keep their cells in place, each head at an absolute cell. *)
From Stdlib Require Import List Bool Arith Lia.
Import ListNotations.
From TH Require Import TwoHead Abstract Spec PassCheck.

Record dst := mkD { dc : cfg; dR : tape; dA : tape; dK : tape }.

(* a tape holding the cells u and then z, its head on the first cell of z *)
Definition past (n : nat) (u z : list bool) : tape := mkT (u ++ z) (length u mod n).

Lemma upd_app_cons : forall u c z v, upd (u ++ c :: z) (length u) v = u ++ v :: z.
Proof. induction u as [|x u IH]; intros c z v; cbn; [reflexivity | rewrite IH; reflexivity]. Qed.

Lemma past_get : forall n u b z, length u < n -> tget (past n u (b :: z)) = b.
Proof.
  intros n u b z H. unfold tget, past. cbn [td th]. rewrite (Nat.mod_small _ _ H).
  rewrite app_nth2 by lia. rewrite Nat.sub_diag. reflexivity.
Qed.

Lemma past_adv : forall n u b z, 1 <= n ->
  mkT (td (past n u (b :: z))) (succ_mod n (th (past n u (b :: z)))) = past n (u ++ [b]) z.
Proof.
  intros n u b z H. unfold past. cbn [td th]. rewrite (succ_mod_mod n (length u) H).
  rewrite <- app_assoc, length_app. cbn [app length]. rewrite Nat.add_1_r. reflexivity.
Qed.

Lemma past_write : forall n u c z v, length u < n ->
  mkT (upd (td (past n u (c :: z))) (th (past n u (c :: z))) v) (succ_mod n (th (past n u (c :: z))))
  = past n (u ++ [v]) z.
Proof.
  intros n u c z v H. unfold past. cbn [td th]. rewrite (succ_mod_mod n (length u) ltac:(lia)).
  rewrite (Nat.mod_small _ _ H), upd_app_cons, <- app_assoc, length_app. cbn [app length].
  rewrite Nat.add_1_r. reflexivity.
Qed.

Lemma past_home : forall n u z, mkT (td (past n u z)) 0 = past n [] (u ++ z).
Proof. intros n u z. unfold past. cbn [td length app]. rewrite Nat.Div0.mod_0_l. reflexivity. Qed.

Lemma skipn_repeat_false : forall a n, skipn a (repeat false n) = repeat false (n - a).
Proof.
  induction a as [|a IH]; intros [|n]; cbn [skipn repeat]; try reflexivity. exact (IH n).
Qed.

(* ---- lists ---------------------------------------------------------------------------------- *)
Lemma some_inj : forall (A : Type) (a b : A), Some a = Some b -> a = b.
Proof. intros A a b H. injection H. auto. Qed.

Lemma split_at : forall (l : list bool) n, n <= length l -> exists a c, l = a ++ c /\ length a = n.
Proof.
  intros l n H. exists (firstn n l), (skipn n l). split; [symmetry; apply firstn_skipn|].
  apply firstn_length_le. exact H.
Qed.

Lemma skipn_app_exact : forall (a b : list bool) n, length a = n -> skipn n (a ++ b) = b.
Proof. intros a b n <-. induction a as [|x a IH]; [reflexivity|]. exact IH. Qed.

Lemma firstn_app_exact : forall (a b : list bool) n, length a = n -> firstn n (a ++ b) = a.
Proof.
  intros a b n <-. induction a as [|x a IH]; [reflexivity|]. cbn [length firstn app].
  rewrite IH. reflexivity.
Qed.

Lemma translate_aux_long : forall f l X, translate_aux f l = Some X -> 4 <= length l.
Proof.
  intros [|f] l X H; [discriminate|]. cbn [translate_aux] in H.
  destruct l as [|a [|b [|c [|d l]]]]; try discriminate. cbn [length]. lia.
Qed.

Lemma translate_aux_S : forall f c3 c2 s0 s1 rest,
  translate_aux (S f) (c3 :: c2 :: s0 :: s1 :: rest) =
  if c3 && c2 then
    if s0 && s1 then match rest with [] => Some [] | _ => None end
    else if Nat.eqb (length rest) 0 then None
    else option_map (fun t => firstn 26 rest ++ t) (translate_aux f (skipn 26 rest))
  else option_map (fun t => gate_bits (if c3 then 2 else if c2 then 1 else 0) s0 s1 ++ firstn 18 rest ++ t)
                  (translate_aux f (skipn 18 rest)).
Proof. reflexivity. Qed.

Fixpoint down (n : nat) : list nat := match n with O => [0] | S m => n :: down m end.

Definition kind_of (e3 e2 : bool) : nat := if e3 then 2 else if e2 then 1 else 0.

Lemma length_gate_bits : forall k s0 s1, length (gate_bits k s0 s1) = 8.
Proof. intros [|[|[|k]]] s0 s1; reflexivity. Qed.

Lemma table_gate : forall e3 e2 s0 s1, e3 && e2 = false ->
  map (table e3 e2 s0 s1) (down 7) = gate_bits (kind_of e3 e2) s0 s1.
Proof. intros [] [] [] [] H; try discriminate; reflexivity. Qed.

(* ---- the flags of a pass ---------------------------------------------------------------------- *)
Lemma dpass_flags : forall cf r,
  (fresh (dpass cf r) = true -> home (dpass cf r) = true)
  /\ (home (dpass cf r) = true -> emit (dpass cf r) = false)
  /\ (fresh (dpass cf r) = true -> cw (dpass cf r) = false).
Proof.
  intros [p n c3 c2 c1 c0 m] r. unfold dpass. cbn [ph Spec.z Spec.c3 Spec.c2 Spec.c1 Spec.c0 mo].
  destruct p; repeat match goal with |- context [if ?b then _ else _] => destruct b end;
    cbn [fresh home emit cw]; repeat split; intro H; first [discriminate | reflexivity].
Qed.

Lemma reach_step : forall cf r, reachable cf = true -> reachable (ncf (dpass cf r)) = true.
Proof.
  intros [p n e3 e2 e1 e0 m] r H. unfold reachable in H. cbn [ph Spec.z] in H.
  unfold dpass. cbn [ph Spec.z Spec.c3 Spec.c2 Spec.c1 Spec.c0 mo].
  destruct p; apply Nat.leb_le in H; destruct (Nat.eqb n 0) eqn:E;
    repeat match goal with |- context [if ?b then _ else _] => destruct b end;
    cbn [ncf reachable ph Spec.z]; apply Nat.leb_le; lia.
Qed.

Section Dec.
Variables N L : nat.
Hypotheses (HN : 1 <= N) (HL : 1 <= L).

Definition dout (t : dst) : out := dpass (dc t) (tget (dR t)).

(* one pass of the spec on the three tapes *)
Definition dstep (t : dst) : dst :=
  let r := tget (dR t) in
  let o := dpass (dc t) r in
  mkD (ncf o) (tape_eff L (expR o r) (dR t)) (tape_eff N (expA o (tget (dA t))) (dA t))
      (tape_eff L (expK o r (tget (dK t))) (dK t)).

Fixpoint dsteps (n : nat) (t : dst) : dst := match n with O => t | S m => dsteps m (dstep t) end.

Lemma dsteps_add : forall a b t, dsteps (a + b) t = dsteps b (dsteps a t).
Proof. induction a as [|a IH]; intros b t; cbn [dsteps Nat.add]; auto. Qed.

(* no pass among the first n hands over *)
Definition quiet (n : nat) (t : dst) : Prop := forall j, j < n -> ho (dout (dsteps j t)) = false.

Lemma quiet_S : forall n t, ho (dout t) = false -> quiet n (dstep t) -> quiet (S n) t.
Proof. intros n t H0 H [|j] Hj; [exact H0|]. cbn [dsteps]. apply H. lia. Qed.

Lemma quiet_add : forall a b t, quiet a t -> quiet b (dsteps a t) -> quiet (a + b) t.
Proof.
  intros a b t Ha Hb j Hj. destruct (Nat.lt_ge_cases j a) as [H|H]; [apply Ha; exact H|].
  replace j with (a + (j - a)) by lia. rewrite dsteps_add. apply Hb. lia.
Qed.

Lemma quiet_0 : forall t, quiet 0 t.
Proof. intros t j Hj. lia. Qed.

(* the effect of a pass on each tape, by its flags *)
Definition rmove (o : out) (t : tape) : tape :=
  if rr o then mkT (td t) 0 else if cons o then mkT (td t) (succ_mod L (th t)) else t.
Definition amove (o : out) (t : tape) : tape :=
  if fresh o then mkT (repeat false N) 0 else if home o then mkT (td t) 0
  else if emit o then mkT (upd (td t) (th t) (av o)) (succ_mod N (th t)) else t.
Definition kmove (o : out) (r : bool) (t : tape) : tape :=
  if fresh o then mkT (repeat false L) 0
  else if home o then mkT (if cw o then upd (td t) (th t) r else td t) 0
  else if cw o then mkT (upd (td t) (th t) r) (succ_mod L (th t)) else t.

Lemma dstep_eq : forall t, dstep t =
  mkD (ncf (dout t)) (rmove (dout t) (dR t)) (amove (dout t) (dA t)) (kmove (dout t) (tget (dR t)) (dK t)).
Proof.
  intros [c R A K]. unfold dstep, dout. cbn [dc dR dA dK].
  destruct (dpass_flags c (tget R)) as (F1 & F2 & F3).
  set (o := dpass c (tget R)) in *. f_equal.
  - unfold tape_eff, expR, rmove. cbn [acl awr amv arw].
    destruct (rr o), (cons o); cbn [iter]; try reflexivity. destruct R; reflexivity.
  - unfold tape_eff, expA, amove, tget. cbn [acl awr amv arw].
    destruct (fresh o) eqn:Ef; [rewrite (F1 eq_refl); reflexivity|].
    destruct (home o) eqn:Eh; [rewrite (F2 eq_refl), upd_same; reflexivity|].
    destruct (emit o); cbn [iter]; [reflexivity|]. rewrite upd_same. destruct A; reflexivity.
  - unfold tape_eff, expK, kmove, tget. cbn [acl awr amv arw].
    destruct (fresh o) eqn:Ef; [rewrite (F1 eq_refl); reflexivity|].
    destruct (home o), (cw o); cbn [iter]; rewrite ?upd_same; try reflexivity. destruct K; reflexivity.
Qed.

(* ---- one pass in each phase ---------------------------------------------------------------- *)
Lemma pass_PI : forall zc c3 c2 c1 c0 m R A K,
  ho (dout (mkD (mkC PI zc c3 c2 c1 c0 m) R A K)) = false
  /\ dstep (mkD (mkC PI zc c3 c2 c1 c0 m) R A K)
     = mkD (mkC PC 3 c3 c2 c1 c0 false) (mkT (td R) 0) (mkT (repeat false N) 0) (mkT (repeat false L) 0).
Proof. intros. split; [reflexivity|]. rewrite dstep_eq. reflexivity. Qed.

Lemma pass_PA : forall n e3 e2 e1 e0 m done b rest A K, length done < L ->
  ho (dout (mkD (mkC PA n e3 e2 e1 e0 m) (past L done (b :: rest)) A K)) = false
  /\ dstep (mkD (mkC PA n e3 e2 e1 e0 m) (past L done (b :: rest)) A K)
     = mkD (if Nat.eqb n 0 then mkC PC 3 e3 e2 e1 e0 m else mkC PA (n - 1) e3 e2 e1 e0 m)
           (past L (done ++ [b]) rest)
           (if m then A else mkT (upd (td A) (th A) b) (succ_mod N (th A)))
           (if m then mkT (upd (td K) (th K) b) (succ_mod L (th K)) else K).
Proof.
  intros n e3 e2 e1 e0 m done b rest A K Hd.
  assert (Ho : dout (mkD (mkC PA n e3 e2 e1 e0 m) (past L done (b :: rest)) A K)
               = mkO (if Nat.eqb n 0 then mkC PC 3 e3 e2 e1 e0 m else mkC PA (n - 1) e3 e2 e1 e0 m)
                     true (negb m) b m false false false false).
  { unfold dout. cbn [dc dR]. rewrite (past_get L done b rest Hd). reflexivity. }
  split; [rewrite Ho; reflexivity|].
  rewrite dstep_eq, Ho. cbn [dR dA dK]. rewrite (past_get L done b rest Hd).
  unfold rmove, amove, kmove. cbn [ncf rr cons fresh home emit cw av].
  rewrite (past_adv L done b rest HL). destruct m; reflexivity.
Qed.

Lemma pass_PG : forall n e3 e2 e1 e0 m R A K,
  ho (dout (mkD (mkC PG n e3 e2 e1 e0 m) R A K)) = false
  /\ dstep (mkD (mkC PG n e3 e2 e1 e0 m) R A K)
     = mkD (if Nat.eqb n 0 then mkC PA 17 e3 e2 e1 e0 m else mkC PG (n - 1) e3 e2 e1 e0 m)
           (if is_esc e3 e2 e1 e0 then mkT (td R) (succ_mod L (th R)) else R)
           (if m then A
            else mkT (upd (td A) (th A) (if is_esc e3 e2 e1 e0 then tget R else table e3 e2 e1 e0 n))
                     (succ_mod N (th A)))
           (if m && is_esc e3 e2 e1 e0 then mkT (upd (td K) (th K) (tget R)) (succ_mod L (th K)) else K).
Proof.
  intros n e3 e2 e1 e0 m R A K.
  assert (Ho : dout (mkD (mkC PG n e3 e2 e1 e0 m) R A K)
               = mkO (if Nat.eqb n 0 then mkC PA 17 e3 e2 e1 e0 m else mkC PG (n - 1) e3 e2 e1 e0 m)
                     (is_esc e3 e2 e1 e0) (negb m)
                     (if is_esc e3 e2 e1 e0 then tget R else table e3 e2 e1 e0 n)
                     (m && is_esc e3 e2 e1 e0) false false false false) by reflexivity.
  split; [rewrite Ho; reflexivity|].
  rewrite dstep_eq, Ho. cbn [dR dA dK]. unfold rmove, amove, kmove. cbn [ncf rr cons fresh home emit cw av].
  destruct (is_esc e3 e2 e1 e0), m; reflexivity.
Qed.

Lemma pass_PC : forall n e3 e2 e1 e0 m done b rest A K, length done < L ->
  ho (dout (mkD (mkC PC (S n) e3 e2 e1 e0 m) (past L done (b :: rest)) A K)) = false
  /\ dstep (mkD (mkC PC (S n) e3 e2 e1 e0 m) (past L done (b :: rest)) A K)
     = mkD (mkC PC n e2 e1 e0 b m) (past L (done ++ [b]) rest) A
           (if m then mkT (upd (td K) (th K) b) (succ_mod L (th K)) else K).
Proof.
  intros n e3 e2 e1 e0 m done b rest A K Hd.
  assert (Ho : dout (mkD (mkC PC (S n) e3 e2 e1 e0 m) (past L done (b :: rest)) A K)
               = mkO (mkC PC n e2 e1 e0 b m) true false false m false false false false).
  { unfold dout. cbn [dc dR]. rewrite (past_get L done b rest Hd). unfold dpass.
    cbn [ph Spec.z Spec.c3 Spec.c2 Spec.c1 Spec.c0 mo Nat.eqb]. replace (S n - 1) with n by lia. reflexivity. }
  split; [rewrite Ho; reflexivity|].
  rewrite dstep_eq, Ho. cbn [dR dA dK]. rewrite (past_get L done b rest Hd).
  unfold rmove, amove, kmove. cbn [ncf rr cons fresh home emit cw av].
  rewrite (past_adv L done b rest HL). destruct m; reflexivity.
Qed.

(* the pass that ends a codon: the codon register then holds c2 c1 c0 b *)
Lemma pass_PC0 : forall c3 c2 c1 c0 m done b rest A K, length done < L ->
  let o := dout (mkD (mkC PC 0 c3 c2 c1 c0 m) (past L done (b :: rest)) A K) in
  o = (if is_end c2 c1 c0 b then
         if m then mkO (mkC PI 1 c2 c1 c0 b false) true false false true false true false true
         else mkO (mkC PC 3 c2 c1 c0 b true) true false false false true false false false
       else if negb m || is_esc c2 c1 c0 b then mkO (mkC PG 7 c2 c1 c0 b m) true false false m false false false false
       else mkO (mkC PA 17 c2 c1 c0 b m) true false false m false false false false)
  /\ dstep (mkD (mkC PC 0 c3 c2 c1 c0 m) (past L done (b :: rest)) A K)
     = mkD (ncf o) (rmove o (past L done (b :: rest))) (amove o A) (kmove o b K).
Proof.
  intros c3 c2 c1 c0 m done b rest A K Hd o.
  split.
  - unfold o, dout. cbn [dc dR]. rewrite (past_get L done b rest Hd). reflexivity.
  - rewrite dstep_eq. cbn [dR dA dK]. fold o. rewrite (past_get L done b rest Hd). reflexivity.
Qed.

(* ---- the phases ------------------------------------------------------------------------------ *)
Lemma pa_construct : forall n e3 e2 e1 e0 done bs rest U W Z K,
  length bs = S n -> length W = S n -> length done + S n <= L -> length U + S n <= N ->
  quiet (S n) (mkD (mkC PA n e3 e2 e1 e0 false) (past L done (bs ++ rest)) (past N U (W ++ Z)) K)
  /\ dsteps (S n) (mkD (mkC PA n e3 e2 e1 e0 false) (past L done (bs ++ rest)) (past N U (W ++ Z)) K)
     = mkD (mkC PC 3 e3 e2 e1 e0 false) (past L (done ++ bs) rest) (past N (U ++ bs) Z) K.
Proof.
  induction n as [|n IH]; intros e3 e2 e1 e0 done bs rest U W Z K Hb HW Hd HU;
    (destruct bs as [|b bs]; [discriminate|]); (destruct W as [|w W]; [discriminate|]);
    cbn [app length] in *;
    match goal with |- context [mkC PA ?k _ _ _ _ _] =>
      destruct (pass_PA k e3 e2 e1 e0 false done b (bs ++ rest) (past N U (w :: W ++ Z)) K ltac:(lia)) as [Hq Hs] end;
    rewrite (past_write N U w (W ++ Z) b ltac:(lia)) in Hs.
  - destruct bs; [|discriminate]. destruct W; [|discriminate]. cbn [app Nat.eqb] in Hs, Hq |- *.
    split; [apply quiet_S; [exact Hq | apply quiet_0]|]. cbn [dsteps]. rewrite Hs. reflexivity.
  - cbn [Nat.eqb] in Hs. replace (S n - 1) with n in Hs by lia.
    destruct (IH e3 e2 e1 e0 (done ++ [b]) bs rest (U ++ [b]) W Z K ltac:(lia) ltac:(lia)
                ltac:(rewrite length_app; cbn [length]; lia) ltac:(rewrite length_app; cbn [length]; lia))
      as [Q E].
    rewrite <- Hs in Q, E. split; [apply quiet_S; [exact Hq | exact Q]|].
    change (dsteps (S (S n)) ?t) with (dsteps (S n) (dstep t)). rewrite E, <- !app_assoc. reflexivity.
Qed.

Lemma pa_copy : forall n e3 e2 e1 e0 done bs rest A V W C,
  length bs = S n -> length W = S n -> length done + S n <= L -> length V + S n <= L ->
  quiet (S n) (mkD (mkC PA n e3 e2 e1 e0 true) (past L done (bs ++ rest)) A (past L V (W ++ C)))
  /\ dsteps (S n) (mkD (mkC PA n e3 e2 e1 e0 true) (past L done (bs ++ rest)) A (past L V (W ++ C)))
     = mkD (mkC PC 3 e3 e2 e1 e0 true) (past L (done ++ bs) rest) A (past L (V ++ bs) C).
Proof.
  induction n as [|n IH]; intros e3 e2 e1 e0 done bs rest A V W C Hb HW Hd HV;
    (destruct bs as [|b bs]; [discriminate|]); (destruct W as [|w W]; [discriminate|]);
    cbn [app length] in *;
    match goal with |- context [mkC PA ?k _ _ _ _ _] =>
      destruct (pass_PA k e3 e2 e1 e0 true done b (bs ++ rest) A (past L V (w :: W ++ C)) ltac:(lia)) as [Hq Hs] end;
    rewrite (past_write L V w (W ++ C) b ltac:(lia)) in Hs.
  - destruct bs; [|discriminate]. destruct W; [|discriminate]. cbn [app Nat.eqb] in Hs, Hq |- *.
    split; [apply quiet_S; [exact Hq | apply quiet_0]|]. cbn [dsteps]. rewrite Hs. reflexivity.
  - cbn [Nat.eqb] in Hs. replace (S n - 1) with n in Hs by lia.
    destruct (IH e3 e2 e1 e0 (done ++ [b]) bs rest A (V ++ [b]) W C ltac:(lia) ltac:(lia)
                ltac:(rewrite length_app; cbn [length]; lia) ltac:(rewrite length_app; cbn [length]; lia))
      as [Q E].
    rewrite <- Hs in Q, E. split; [apply quiet_S; [exact Hq | exact Q]|].
    change (dsteps (S (S n)) ?t) with (dsteps (S n) (dstep t)). rewrite E, <- !app_assoc. reflexivity.
Qed.

Lemma pg_gate : forall n e3 e2 e1 e0 R U W Z K, is_esc e3 e2 e1 e0 = false ->
  length W = S n -> length U + S n <= N ->
  quiet (S n) (mkD (mkC PG n e3 e2 e1 e0 false) R (past N U (W ++ Z)) K)
  /\ dsteps (S n) (mkD (mkC PG n e3 e2 e1 e0 false) R (past N U (W ++ Z)) K)
     = mkD (mkC PA 17 e3 e2 e1 e0 false) R (past N (U ++ map (table e3 e2 e1 e0) (down n)) Z) K.
Proof.
  induction n as [|n IH]; intros e3 e2 e1 e0 R U W Z K He HW HU;
    (destruct W as [|w W]; [discriminate|]); cbn [app length] in *;
    match goal with |- context [mkC PG ?k _ _ _ _ _] =>
      destruct (pass_PG k e3 e2 e1 e0 false R (past N U (w :: W ++ Z)) K) as [Hq Hs] end;
    rewrite He in Hs; cbn [andb negb] in Hs;
    rewrite (past_write N U w (W ++ Z) _ ltac:(lia)) in Hs.
  - destruct W; [|discriminate]. cbn [app Nat.eqb] in Hs, Hq |- *.
    split; [apply quiet_S; [exact Hq | apply quiet_0]|]. cbn [dsteps]. rewrite Hs. reflexivity.
  - cbn [Nat.eqb] in Hs. replace (S n - 1) with n in Hs by lia.
    destruct (IH e3 e2 e1 e0 R (U ++ [table e3 e2 e1 e0 (S n)]) W Z K He ltac:(lia)
                ltac:(rewrite length_app; cbn [length]; lia)) as [Q E].
    rewrite <- Hs in Q, E. split; [apply quiet_S; [exact Hq | exact Q]|].
    change (dsteps (S (S n)) ?t) with (dsteps (S n) (dstep t)). rewrite E, <- !app_assoc. reflexivity.
Qed.

Lemma pg_esc_construct : forall n e3 e2 e1 e0 done bs rest U W Z K, is_esc e3 e2 e1 e0 = true ->
  length bs = S n -> length W = S n -> length done + S n <= L -> length U + S n <= N ->
  quiet (S n) (mkD (mkC PG n e3 e2 e1 e0 false) (past L done (bs ++ rest)) (past N U (W ++ Z)) K)
  /\ dsteps (S n) (mkD (mkC PG n e3 e2 e1 e0 false) (past L done (bs ++ rest)) (past N U (W ++ Z)) K)
     = mkD (mkC PA 17 e3 e2 e1 e0 false) (past L (done ++ bs) rest) (past N (U ++ bs) Z) K.
Proof.
  induction n as [|n IH]; intros e3 e2 e1 e0 done bs rest U W Z K He Hb HW Hd HU;
    (destruct bs as [|b bs]; [discriminate|]); (destruct W as [|w W]; [discriminate|]);
    cbn [app length] in *;
    match goal with |- context [mkC PG ?k _ _ _ _ _] =>
      destruct (pass_PG k e3 e2 e1 e0 false (past L done (b :: bs ++ rest)) (past N U (w :: W ++ Z)) K)
        as [Hq Hs] end;
    rewrite He in Hs; cbn [andb negb] in Hs;
    rewrite (past_get L done b (bs ++ rest) ltac:(lia)), (past_adv L done b (bs ++ rest) HL),
      (past_write N U w (W ++ Z) b ltac:(lia)) in Hs.
  - destruct bs; [|discriminate]. destruct W; [|discriminate]. cbn [app Nat.eqb] in Hs, Hq |- *.
    split; [apply quiet_S; [exact Hq | apply quiet_0]|]. cbn [dsteps]. rewrite Hs. reflexivity.
  - cbn [Nat.eqb] in Hs. replace (S n - 1) with n in Hs by lia.
    destruct (IH e3 e2 e1 e0 (done ++ [b]) bs rest (U ++ [b]) W Z K He ltac:(lia) ltac:(lia)
                ltac:(rewrite length_app; cbn [length]; lia) ltac:(rewrite length_app; cbn [length]; lia))
      as [Q E].
    rewrite <- Hs in Q, E. split; [apply quiet_S; [exact Hq | exact Q]|].
    change (dsteps (S (S n)) ?t) with (dsteps (S n) (dstep t)). rewrite E, <- !app_assoc. reflexivity.
Qed.

Lemma pg_esc_copy : forall n e3 e2 e1 e0 done bs rest A V W C, is_esc e3 e2 e1 e0 = true ->
  length bs = S n -> length W = S n -> length done + S n <= L -> length V + S n <= L ->
  quiet (S n) (mkD (mkC PG n e3 e2 e1 e0 true) (past L done (bs ++ rest)) A (past L V (W ++ C)))
  /\ dsteps (S n) (mkD (mkC PG n e3 e2 e1 e0 true) (past L done (bs ++ rest)) A (past L V (W ++ C)))
     = mkD (mkC PA 17 e3 e2 e1 e0 true) (past L (done ++ bs) rest) A (past L (V ++ bs) C).
Proof.
  induction n as [|n IH]; intros e3 e2 e1 e0 done bs rest A V W C He Hb HW Hd HV;
    (destruct bs as [|b bs]; [discriminate|]); (destruct W as [|w W]; [discriminate|]);
    cbn [app length] in *;
    match goal with |- context [mkC PG ?k _ _ _ _ _] =>
      destruct (pass_PG k e3 e2 e1 e0 true (past L done (b :: bs ++ rest)) A (past L V (w :: W ++ C)))
        as [Hq Hs] end;
    rewrite He in Hs; cbn [andb negb] in Hs;
    rewrite (past_get L done b (bs ++ rest) ltac:(lia)), (past_adv L done b (bs ++ rest) HL),
      (past_write L V w (W ++ C) b ltac:(lia)) in Hs.
  - destruct bs; [|discriminate]. destruct W; [|discriminate]. cbn [app Nat.eqb] in Hs, Hq |- *.
    split; [apply quiet_S; [exact Hq | apply quiet_0]|]. cbn [dsteps]. rewrite Hs. reflexivity.
  - cbn [Nat.eqb] in Hs. replace (S n - 1) with n in Hs by lia.
    destruct (IH e3 e2 e1 e0 (done ++ [b]) bs rest A (V ++ [b]) W C He ltac:(lia) ltac:(lia)
                ltac:(rewrite length_app; cbn [length]; lia) ltac:(rewrite length_app; cbn [length]; lia))
      as [Q E].
    rewrite <- Hs in Q, E. split; [apply quiet_S; [exact Hq | exact Q]|].
    change (dsteps (S (S n)) ?t) with (dsteps (S n) (dstep t)). rewrite E, <- !app_assoc. reflexivity.
Qed.

(* the first three passes of a codon *)
Lemma codon3_construct : forall b3 b2 b1 b0 e3 e2 e1 e0 done rest A K, length done + 3 < L ->
  quiet 3 (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done ([e3; e2; e1; e0] ++ rest)) A K)
  /\ dsteps 3 (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done ([e3; e2; e1; e0] ++ rest)) A K)
     = mkD (mkC PC 0 b0 e3 e2 e1 false) (past L (done ++ [e3; e2; e1]) (e0 :: rest)) A K.
Proof.
  intros b3 b2 b1 b0 e3 e2 e1 e0 done rest A K Hd. cbn [app].
  destruct (pass_PC 2 b3 b2 b1 b0 false done e3 (e2 :: e1 :: e0 :: rest) A K ltac:(lia)) as [Q1 E1].
  destruct (pass_PC 1 b2 b1 b0 e3 false (done ++ [e3]) e2 (e1 :: e0 :: rest) A K
              ltac:(rewrite length_app; cbn [length]; lia)) as [Q2 E2].
  destruct (pass_PC 0 b1 b0 e3 e2 false ((done ++ [e3]) ++ [e2]) e1 (e0 :: rest) A K
              ltac:(rewrite !length_app; cbn [length]; lia)) as [Q3 E3].
  split.
  - apply quiet_S; [exact Q1|]. rewrite E1. apply quiet_S; [exact Q2|]. rewrite E2.
    apply quiet_S; [exact Q3|]. apply quiet_0.
  - cbn [dsteps]. rewrite E1, E2, E3, <- !app_assoc. reflexivity.
Qed.

Lemma codon3_copy : forall b3 b2 b1 b0 e3 e2 e1 e0 done rest A V w1 w2 w3 C,
  length done + 3 < L -> length V + 3 < L ->
  quiet 3 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done ([e3; e2; e1; e0] ++ rest)) A
               (past L V (w1 :: w2 :: w3 :: C)))
  /\ dsteps 3 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done ([e3; e2; e1; e0] ++ rest)) A
                   (past L V (w1 :: w2 :: w3 :: C)))
     = mkD (mkC PC 0 b0 e3 e2 e1 true) (past L (done ++ [e3; e2; e1]) (e0 :: rest)) A
           (past L (V ++ [e3; e2; e1]) C).
Proof.
  intros b3 b2 b1 b0 e3 e2 e1 e0 done rest A V w1 w2 w3 C Hd HV. cbn [app].
  destruct (pass_PC 2 b3 b2 b1 b0 true done e3 (e2 :: e1 :: e0 :: rest) A (past L V (w1 :: w2 :: w3 :: C))
              ltac:(lia)) as [Q1 E1].
  rewrite (past_write L V w1 (w2 :: w3 :: C) e3 ltac:(lia)) in E1.
  destruct (pass_PC 1 b2 b1 b0 e3 true (done ++ [e3]) e2 (e1 :: e0 :: rest) A (past L (V ++ [e3]) (w2 :: w3 :: C))
              ltac:(rewrite length_app; cbn [length]; lia)) as [Q2 E2].
  rewrite (past_write L (V ++ [e3]) w2 (w3 :: C) e2 ltac:(rewrite length_app; cbn [length]; lia)) in E2.
  destruct (pass_PC 0 b1 b0 e3 e2 true ((done ++ [e3]) ++ [e2]) e1 (e0 :: rest) A
              (past L ((V ++ [e3]) ++ [e2]) (w3 :: C)) ltac:(rewrite !length_app; cbn [length]; lia)) as [Q3 E3].
  rewrite (past_write L ((V ++ [e3]) ++ [e2]) w3 C e1 ltac:(rewrite !length_app; cbn [length]; lia)) in E3.
  split.
  - apply quiet_S; [exact Q1|]. rewrite E1. apply quiet_S; [exact Q2|]. rewrite E2.
    apply quiet_S; [exact Q3|]. apply quiet_0.
  - cbn [dsteps]. rewrite E1, E2, E3, <- !app_assoc. reflexivity.
Qed.

(* ---- composing passes ------------------------------------------------------------------------ *)
Lemma one : forall t t', ho (dout t) = false -> dstep t = t' -> quiet 1 t /\ dsteps 1 t = t'.
Proof. intros t t' H E. split; [apply quiet_S; [exact H | apply quiet_0] | cbn [dsteps]; exact E]. Qed.

Lemma chain : forall a b t t' t'', quiet a t /\ dsteps a t = t' -> quiet b t' /\ dsteps b t' = t'' ->
  quiet (a + b) t /\ dsteps (a + b) t = t''.
Proof.
  intros a b t t' t'' [Qa Ea] [Qb Eb]. split.
  - apply quiet_add; [exact Qa|]. rewrite Ea. exact Qb.
  - rewrite dsteps_add, Ea. exact Eb.
Qed.

(* a run of passes whose last pass, and only that one, hands over *)
Lemma chain_last : forall a b t t' t'', quiet a t /\ dsteps a t = t' ->
  quiet (b - 1) t' /\ ho (dout (dsteps (b - 1) t')) = true /\ dsteps b t' = t'' -> 1 <= b ->
  quiet (a + b - 1) t /\ ho (dout (dsteps (a + b - 1) t)) = true /\ dsteps (a + b) t = t''.
Proof.
  intros a b t t' t'' [Qa Ea] (Qb & Hb & Eb) H1.
  replace (a + b - 1) with (a + (b - 1)) by lia.
  split; [apply quiet_add; [exact Qa | rewrite Ea; exact Qb]|].
  split; rewrite dsteps_add, Ea; assumption.
Qed.

Lemma skipn_app_plus : forall (a b : list bool) k, skipn (length a + k) (a ++ b) = skipn k b.
Proof. induction a as [|x a IH]; intros b k; [reflexivity|]. exact (IH b k). Qed.

(* lists of cells to the right-nested form with the known cells first *)
Ltac norm_in H := repeat (first [rewrite <- app_assoc in H | progress (cbn [app] in H)]).
Ltac norm_goal := repeat (first [rewrite <- app_assoc | progress (cbn [app])]).

(* ---- the pass that ends a codon ------------------------------------------------------------- *)
Lemma pc0_construct_go : forall c3 c2 c1 c0 done b rest A K, length done < L -> is_end c2 c1 c0 b = false ->
  quiet 1 (mkD (mkC PC 0 c3 c2 c1 c0 false) (past L done (b :: rest)) A K)
  /\ dsteps 1 (mkD (mkC PC 0 c3 c2 c1 c0 false) (past L done (b :: rest)) A K)
     = mkD (mkC PG 7 c2 c1 c0 b false) (past L (done ++ [b]) rest) A K.
Proof.
  intros c3 c2 c1 c0 done b rest A K Hd Hn.
  destruct (pass_PC0 c3 c2 c1 c0 false done b rest A K Hd) as [O E].
  rewrite Hn in O. cbn [negb orb] in O.
  apply one; [rewrite O; reflexivity|]. rewrite E, O. unfold rmove, amove, kmove.
  cbn [ncf rr cons fresh home emit cw]. rewrite (past_adv L done b rest HL). reflexivity.
Qed.

Lemma pc0_construct_end : forall c3 c2 c1 c0 done b rest A K, length done < L -> is_end c2 c1 c0 b = true ->
  quiet 1 (mkD (mkC PC 0 c3 c2 c1 c0 false) (past L done (b :: rest)) A K)
  /\ dsteps 1 (mkD (mkC PC 0 c3 c2 c1 c0 false) (past L done (b :: rest)) A K)
     = mkD (mkC PC 3 c2 c1 c0 b true) (past L [] (done ++ b :: rest)) A K.
Proof.
  intros c3 c2 c1 c0 done b rest A K Hd Hn.
  destruct (pass_PC0 c3 c2 c1 c0 false done b rest A K Hd) as [O E].
  rewrite Hn in O.
  apply one; [rewrite O; reflexivity|]. rewrite E, O. unfold rmove, amove, kmove.
  cbn [ncf rr cons fresh home emit cw]. rewrite past_home. reflexivity.
Qed.

Lemma pc0_copy_go : forall c3 c2 c1 c0 done b rest A V w C, length done < L -> length V < L ->
  is_end c2 c1 c0 b = false ->
  quiet 1 (mkD (mkC PC 0 c3 c2 c1 c0 true) (past L done (b :: rest)) A (past L V (w :: C)))
  /\ dsteps 1 (mkD (mkC PC 0 c3 c2 c1 c0 true) (past L done (b :: rest)) A (past L V (w :: C)))
     = mkD (if is_esc c2 c1 c0 b then mkC PG 7 c2 c1 c0 b true else mkC PA 17 c2 c1 c0 b true)
           (past L (done ++ [b]) rest) A (past L (V ++ [b]) C).
Proof.
  intros c3 c2 c1 c0 done b rest A V w C Hd HV Hn.
  destruct (pass_PC0 c3 c2 c1 c0 true done b rest A (past L V (w :: C)) Hd) as [O E].
  rewrite Hn in O. cbn [negb orb] in O.
  apply one; [rewrite O; destruct (is_esc c2 c1 c0 b); reflexivity|].
  rewrite E, O. destruct (is_esc c2 c1 c0 b); unfold rmove, amove, kmove;
    cbn [ncf rr cons fresh home emit cw];
    rewrite (past_adv L done b rest HL), (past_write L V w C b HV); reflexivity.
Qed.

Lemma pc0_copy_end : forall c3 c2 c1 c0 done b rest A V w C, length done < L -> length V < L ->
  is_end c2 c1 c0 b = true ->
  ho (dout (mkD (mkC PC 0 c3 c2 c1 c0 true) (past L done (b :: rest)) A (past L V (w :: C)))) = true
  /\ dstep (mkD (mkC PC 0 c3 c2 c1 c0 true) (past L done (b :: rest)) A (past L V (w :: C)))
     = mkD (mkC PI 1 c2 c1 c0 b false) (past L (done ++ [b]) rest) (mkT (td A) 0) (mkT (V ++ b :: C) 0).
Proof.
  intros c3 c2 c1 c0 done b rest A V w C Hd HV Hn.
  destruct (pass_PC0 c3 c2 c1 c0 true done b rest A (past L V (w :: C)) Hd) as [O E].
  rewrite Hn in O.
  split; [rewrite O; reflexivity|].
  assert (Hk : upd (td (past L V (w :: C))) (th (past L V (w :: C))) b = V ++ b :: C)
    by (unfold past; cbn [td th]; rewrite (Nat.mod_small _ _ HV); apply upd_app_cons).
  rewrite E, O. unfold rmove, amove, kmove. cbn [ncf rr cons fresh home emit cw].
  rewrite (past_adv L done b rest HL), Hk. reflexivity.
Qed.

(* ---- a whole codon ------------------------------------------------------------------------------ *)
Lemma codon_construct_go : forall b3 b2 b1 b0 e3 e2 e1 e0 done rest A K, length done + 4 <= L ->
  is_end e3 e2 e1 e0 = false ->
  quiet 4 (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done (e3 :: e2 :: e1 :: e0 :: rest)) A K)
  /\ dsteps 4 (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done (e3 :: e2 :: e1 :: e0 :: rest)) A K)
     = mkD (mkC PG 7 e3 e2 e1 e0 false) (past L (done ++ [e3; e2; e1; e0]) rest) A K.
Proof.
  intros b3 b2 b1 b0 e3 e2 e1 e0 done rest A K Hd Hn.
  destruct (pc0_construct_go b0 e3 e2 e1 (done ++ [e3; e2; e1]) e0 rest A K
              ltac:(rewrite length_app; cbn [length]; lia) Hn) as [Q E].
  rewrite <- app_assoc in E. cbn [app] in E.
  exact (chain 3 1 _ _ _ (codon3_construct b3 b2 b1 b0 e3 e2 e1 e0 done rest A K ltac:(lia)) (conj Q E)).
Qed.

Lemma codon_construct_end : forall b3 b2 b1 b0 done rest A K, length done + 4 <= L ->
  quiet 4 (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done (true :: true :: true :: true :: rest)) A K)
  /\ dsteps 4 (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done (true :: true :: true :: true :: rest)) A K)
     = mkD (mkC PC 3 true true true true true) (past L [] (done ++ true :: true :: true :: true :: rest)) A K.
Proof.
  intros b3 b2 b1 b0 done rest A K Hd.
  destruct (pc0_construct_end b0 true true true (done ++ [true; true; true]) true rest A K
              ltac:(rewrite length_app; cbn [length]; lia) eq_refl) as [Q E].
  rewrite <- app_assoc in E. cbn [app] in E.
  exact (chain 3 1 _ _ _ (codon3_construct b3 b2 b1 b0 true true true true done rest A K ltac:(lia)) (conj Q E)).
Qed.

Lemma codon_copy_go : forall b3 b2 b1 b0 e3 e2 e1 e0 done rest A V w1 w2 w3 w4 C,
  length done + 4 <= L -> length V + 4 <= L -> is_end e3 e2 e1 e0 = false ->
  quiet 4 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (e3 :: e2 :: e1 :: e0 :: rest)) A
               (past L V (w1 :: w2 :: w3 :: w4 :: C)))
  /\ dsteps 4 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (e3 :: e2 :: e1 :: e0 :: rest)) A
                   (past L V (w1 :: w2 :: w3 :: w4 :: C)))
     = mkD (if is_esc e3 e2 e1 e0 then mkC PG 7 e3 e2 e1 e0 true else mkC PA 17 e3 e2 e1 e0 true)
           (past L (done ++ [e3; e2; e1; e0]) rest) A (past L (V ++ [e3; e2; e1; e0]) C).
Proof.
  intros b3 b2 b1 b0 e3 e2 e1 e0 done rest A V w1 w2 w3 w4 C Hd HV Hn.
  destruct (pc0_copy_go b0 e3 e2 e1 (done ++ [e3; e2; e1]) e0 rest A (V ++ [e3; e2; e1]) w4 C
              ltac:(rewrite length_app; cbn [length]; lia) ltac:(rewrite length_app; cbn [length]; lia) Hn)
    as [Q E].
  rewrite <- !app_assoc in E. cbn [app] in E.
  exact (chain 3 1 _ _ _ (codon3_copy b3 b2 b1 b0 e3 e2 e1 e0 done rest A V w1 w2 w3 (w4 :: C)
                            ltac:(lia) ltac:(lia)) (conj Q E)).
Qed.

Lemma codon_copy_end : forall b3 b2 b1 b0 done rest A V w1 w2 w3 w4 C,
  length done + 4 <= L -> length V + 4 <= L ->
  quiet 3 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (true :: true :: true :: true :: rest)) A
               (past L V (w1 :: w2 :: w3 :: w4 :: C)))
  /\ ho (dout (dsteps 3 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (true :: true :: true :: true :: rest)) A
                             (past L V (w1 :: w2 :: w3 :: w4 :: C))))) = true
  /\ dsteps 4 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (true :: true :: true :: true :: rest)) A
                   (past L V (w1 :: w2 :: w3 :: w4 :: C)))
     = mkD (mkC PI 1 true true true true false) (past L (done ++ [true; true; true; true]) rest)
           (mkT (td A) 0) (mkT (V ++ true :: true :: true :: true :: C) 0).
Proof.
  intros b3 b2 b1 b0 done rest A V w1 w2 w3 w4 C Hd HV.
  destruct (codon3_copy b3 b2 b1 b0 true true true true done rest A V w1 w2 w3 (w4 :: C) ltac:(lia) ltac:(lia))
    as [Q E].
  cbn [app] in Q, E.
  destruct (pc0_copy_end b0 true true true (done ++ [true; true; true]) true rest A (V ++ [true; true; true]) w4 C
              ltac:(rewrite length_app; cbn [length]; lia) ltac:(rewrite length_app; cbn [length]; lia) eq_refl)
    as [H4 E4].
  rewrite <- !app_assoc in E4. cbn [app] in E4.
  split; [exact Q|]. split; [rewrite E; exact H4|].
  change 4 with (3 + 1). rewrite dsteps_add, E. cbn [dsteps]. exact E4.
Qed.

(* ---- one record of the description, and its end -------------------------------------------- *)
Lemma seg_gate : forall b3 b2 b1 b0 e3 e2 s0 s1 addr rest done U W Z K,
  e3 && e2 = false -> length addr = 18 -> length W = 26 -> length done + 22 <= L -> length U + 26 <= N ->
  quiet 30 (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done (e3 :: e2 :: s0 :: s1 :: addr ++ rest))
                (past N U (W ++ Z)) K)
  /\ dsteps 30 (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done (e3 :: e2 :: s0 :: s1 :: addr ++ rest))
                    (past N U (W ++ Z)) K)
     = mkD (mkC PC 3 e3 e2 s0 s1 false) (past L (done ++ e3 :: e2 :: s0 :: s1 :: addr) rest)
           (past N (U ++ gate_bits (kind_of e3 e2) s0 s1 ++ addr) Z) K.
Proof.
  intros b3 b2 b1 b0 e3 e2 s0 s1 addr rest done U W Z K H32 Ha HW Hd HU.
  assert (He : is_esc e3 e2 s0 s1 = false) by (unfold is_esc; rewrite H32; reflexivity).
  assert (Hn : is_end e3 e2 s0 s1 = false) by (unfold is_end; rewrite H32; reflexivity).
  destruct (split_at W 8 ltac:(lia)) as (W1 & W2 & -> & HW1). rewrite length_app in HW.
  rewrite <- (app_assoc W1 W2 Z).
  destruct (codon_construct_go b3 b2 b1 b0 e3 e2 s0 s1 done (addr ++ rest) (past N U (W1 ++ W2 ++ Z)) K
              ltac:(lia) Hn) as [Q1 E1].
  destruct (pg_gate 7 e3 e2 s0 s1 (past L (done ++ [e3; e2; s0; s1]) (addr ++ rest)) U W1 (W2 ++ Z) K He
              HW1 ltac:(lia)) as [Q2 E2].
  rewrite table_gate in E2 by exact H32.
  destruct (pa_construct 17 e3 e2 s0 s1 (done ++ [e3; e2; s0; s1]) addr rest
              (U ++ gate_bits (kind_of e3 e2) s0 s1) W2 Z K Ha ltac:(lia)
              ltac:(rewrite length_app; cbn [length]; lia)
              ltac:(rewrite length_app, length_gate_bits; lia)) as [Q3 E3].
  norm_in E2. norm_in Q3. norm_in E3. norm_goal.
  replace 30 with (4 + (8 + 18)) by reflexivity.
  exact (chain 4 (8 + 18) _ _ _ (conj Q1 E1) (chain 8 18 _ _ _ (conj Q2 E2) (conj Q3 E3))).
Qed.

Lemma seg_esc : forall b3 b2 b1 b0 s0 s1 lit addr rest done U W Z K,
  s0 && s1 = false -> length lit = 8 -> length addr = 18 -> length W = 26 -> length done + 30 <= L ->
  length U + 26 <= N ->
  quiet 30 (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done (true :: true :: s0 :: s1 :: lit ++ addr ++ rest))
                (past N U (W ++ Z)) K)
  /\ dsteps 30 (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done (true :: true :: s0 :: s1 :: lit ++ addr ++ rest))
                    (past N U (W ++ Z)) K)
     = mkD (mkC PC 3 true true s0 s1 false) (past L (done ++ true :: true :: s0 :: s1 :: lit ++ addr) rest)
           (past N (U ++ lit ++ addr) Z) K.
Proof.
  intros b3 b2 b1 b0 s0 s1 lit addr rest done U W Z K Hs Hl Ha HW Hd HU.
  assert (He : is_esc true true s0 s1 = true) by (unfold is_esc; cbn [andb]; rewrite Hs; reflexivity).
  assert (Hn : is_end true true s0 s1 = false) by (unfold is_end; cbn [andb]; exact Hs).
  destruct (split_at W 8 ltac:(lia)) as (W1 & W2 & -> & HW1). rewrite length_app in HW.
  rewrite <- (app_assoc W1 W2 Z).
  destruct (codon_construct_go b3 b2 b1 b0 true true s0 s1 done (lit ++ addr ++ rest) (past N U (W1 ++ W2 ++ Z)) K
              ltac:(lia) Hn) as [Q1 E1].
  destruct (pg_esc_construct 7 true true s0 s1 (done ++ [true; true; s0; s1]) lit (addr ++ rest) U W1 (W2 ++ Z) K
              He Hl HW1 ltac:(rewrite length_app; cbn [length]; lia) ltac:(lia)) as [Q2 E2].
  destruct (pa_construct 17 true true s0 s1 ((done ++ [true; true; s0; s1]) ++ lit) addr rest (U ++ lit) W2 Z K
              Ha ltac:(lia) ltac:(rewrite !length_app; cbn [length]; lia) ltac:(rewrite length_app; lia)) as [Q3 E3].
  norm_in E2. norm_in Q3. norm_in E3. norm_goal.
  replace 30 with (4 + (8 + 18)) by reflexivity.
  exact (chain 4 (8 + 18) _ _ _ (conj Q1 E1) (chain 8 18 _ _ _ (conj Q2 E2) (conj Q3 E3))).
Qed.

Lemma seg_copy_gate : forall b3 b2 b1 b0 e3 e2 s0 s1 addr rest done A V W C,
  e3 && e2 = false -> length addr = 18 -> length W = 22 -> length done + 22 <= L -> length V + 22 <= L ->
  quiet 22 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (e3 :: e2 :: s0 :: s1 :: addr ++ rest)) A
                (past L V (W ++ C)))
  /\ dsteps 22 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (e3 :: e2 :: s0 :: s1 :: addr ++ rest)) A
                    (past L V (W ++ C)))
     = mkD (mkC PC 3 e3 e2 s0 s1 true) (past L (done ++ e3 :: e2 :: s0 :: s1 :: addr) rest) A
           (past L (V ++ e3 :: e2 :: s0 :: s1 :: addr) C).
Proof.
  intros b3 b2 b1 b0 e3 e2 s0 s1 addr rest done A V W C H32 Ha HW Hd HV.
  assert (He : is_esc e3 e2 s0 s1 = false) by (unfold is_esc; rewrite H32; reflexivity).
  assert (Hn : is_end e3 e2 s0 s1 = false) by (unfold is_end; rewrite H32; reflexivity).
  destruct W as [|w1 [|w2 [|w3 [|w4 W]]]]; cbn [length] in HW; try lia.
  destruct (codon_copy_go b3 b2 b1 b0 e3 e2 s0 s1 done (addr ++ rest) A V w1 w2 w3 w4 (W ++ C)
              ltac:(lia) ltac:(lia) Hn) as [Q1 E1].
  rewrite He in E1.
  destruct (pa_copy 17 e3 e2 s0 s1 (done ++ [e3; e2; s0; s1]) addr rest A (V ++ [e3; e2; s0; s1]) W C Ha
              ltac:(lia) ltac:(rewrite length_app; cbn [length]; lia) ltac:(rewrite length_app; cbn [length]; lia))
    as [Q2 E2].
  norm_in E2.
  replace 22 with (4 + 18) by reflexivity.
  exact (chain 4 18 _ _ _ (conj Q1 E1) (conj Q2 E2)).
Qed.

Lemma seg_copy_esc : forall b3 b2 b1 b0 s0 s1 lit addr rest done A V W C,
  s0 && s1 = false -> length lit = 8 -> length addr = 18 -> length W = 30 -> length done + 30 <= L ->
  length V + 30 <= L ->
  quiet 30 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (true :: true :: s0 :: s1 :: lit ++ addr ++ rest)) A
                (past L V (W ++ C)))
  /\ dsteps 30 (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (true :: true :: s0 :: s1 :: lit ++ addr ++ rest)) A
                    (past L V (W ++ C)))
     = mkD (mkC PC 3 true true s0 s1 true) (past L (done ++ true :: true :: s0 :: s1 :: lit ++ addr) rest) A
           (past L (V ++ true :: true :: s0 :: s1 :: lit ++ addr) C).
Proof.
  intros b3 b2 b1 b0 s0 s1 lit addr rest done A V W C Hs Hl Ha HW Hd HV.
  assert (He : is_esc true true s0 s1 = true) by (unfold is_esc; cbn [andb]; rewrite Hs; reflexivity).
  assert (Hn : is_end true true s0 s1 = false) by (unfold is_end; cbn [andb]; exact Hs).
  destruct W as [|w1 [|w2 [|w3 [|w4 W]]]]; cbn [length] in HW; try lia.
  destruct (split_at W 8 ltac:(lia)) as (W1 & W2 & -> & HW1). rewrite length_app in HW.
  destruct (codon_copy_go b3 b2 b1 b0 true true s0 s1 done (lit ++ addr ++ rest) A V w1 w2 w3 w4 ((W1 ++ W2) ++ C)
              ltac:(lia) ltac:(lia) Hn) as [Q1 E1].
  rewrite He in E1. norm_in Q1. norm_in E1.
  destruct (pg_esc_copy 7 true true s0 s1 (done ++ [true; true; s0; s1]) lit (addr ++ rest) A
              (V ++ [true; true; s0; s1]) W1 (W2 ++ C) He Hl HW1 ltac:(rewrite length_app; cbn [length]; lia)
              ltac:(rewrite length_app; cbn [length]; lia)) as [Q2 E2].
  destruct (pa_copy 17 true true s0 s1 ((done ++ [true; true; s0; s1]) ++ lit) addr rest A
              ((V ++ [true; true; s0; s1]) ++ lit) W2 C Ha ltac:(lia) ltac:(rewrite !length_app; cbn [length]; lia)
              ltac:(rewrite !length_app; cbn [length]; lia)) as [Q3 E3].
  norm_in E2. norm_in Q3. norm_in E3. norm_goal.
  replace 30 with (4 + (8 + 18)) by reflexivity.
  exact (chain 4 (8 + 18) _ _ _ (conj Q1 E1) (chain 8 18 _ _ _ (conj Q2 E2) (conj Q3 E3))).
Qed.

(* ---- the description read in construct mode ------------------------------------------------- *)
Lemma construct_phase : forall f rest Xr done tail U Z K b3 b2 b1 b0,
  translate_aux f rest = Some Xr -> length done + length rest <= L ->
  length U + length Xr <= N -> length Xr <= length Z ->
  exists nrec, length Xr = 26 * nrec
    /\ quiet (30 * nrec + 4) (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done (rest ++ tail)) (past N U Z) K)
    /\ dsteps (30 * nrec + 4) (mkD (mkC PC 3 b3 b2 b1 b0 false) (past L done (rest ++ tail)) (past N U Z) K)
       = mkD (mkC PC 3 true true true true true) (past L [] (done ++ rest ++ tail))
             (past N (U ++ Xr) (skipn (length Xr) Z)) K.
Proof.
  induction f as [|f IH]; intros rest Xr done tail U Z K b3 b2 b1 b0 Ht Hd HU HZ; [discriminate|].
  destruct rest as [|e3 [|e2 [|s0 [|s1 rest1]]]]; try discriminate.
  rewrite translate_aux_S in Ht.
  destruct (e3 && e2) eqn:E32.
  - apply andb_prop in E32 as [-> ->].
    destruct (s0 && s1) eqn:Es.
    + (* the end codon *)
      destruct rest1; [|discriminate]. apply some_inj in Ht. subst Xr.
      apply andb_prop in Es as [-> ->].
      exists 0. split; [reflexivity|]. rewrite app_nil_r.
      cbn [length] in Hd. exact (codon_construct_end b3 b2 b1 b0 done tail (past N U Z) K ltac:(lia)).
    + (* an escaped record *)
      destruct (Nat.eqb (length rest1) 0) eqn:El; [discriminate|].
      destruct (translate_aux f (skipn 26 rest1)) as [X'|] eqn:Ht'; [|discriminate].
      cbn [option_map] in Ht. apply some_inj in Ht. subst Xr.
      pose proof (translate_aux_long _ _ _ Ht') as Hlong. rewrite length_skipn in Hlong.
      destruct (split_at rest1 8 ltac:(lia)) as (lit & r1 & -> & Hl).
      destruct (split_at r1 18 ltac:(rewrite length_app in Hlong; lia)) as (addr & rest2 & -> & Ha).
      assert (Hs26 : skipn 26 (lit ++ addr ++ rest2) = rest2)
        by (rewrite app_assoc; apply skipn_app_exact; rewrite length_app; lia).
      assert (Hf26 : firstn 26 (lit ++ addr ++ rest2) = lit ++ addr)
        by (rewrite app_assoc; apply firstn_app_exact; rewrite length_app; lia).
      rewrite Hs26 in Ht'. rewrite Hf26 in HU, HZ |- *.
      rewrite !length_app in HU, HZ. cbn [length] in Hd. rewrite !length_app in Hd.
      destruct (split_at Z 26 ltac:(lia)) as (W & Z' & -> & HW).
      destruct (seg_esc b3 b2 b1 b0 s0 s1 lit addr (rest2 ++ tail) done U W Z' K Es Hl Ha HW ltac:(lia) ltac:(lia))
        as [Q1 E1].
      destruct (IH rest2 X' (done ++ true :: true :: s0 :: s1 :: lit ++ addr) tail (U ++ lit ++ addr) Z' K
                  true true s0 s1 Ht' ltac:(rewrite length_app; cbn [length]; rewrite !length_app; lia)
                  ltac:(rewrite !length_app; lia) ltac:(rewrite length_app in HZ; lia)) as (nrec & Hn & Q2 & E2).
      norm_in E2.
      exists (S nrec). split; [rewrite !length_app; lia|].
      assert (Hsk : skipn (length ((lit ++ addr) ++ X')) (W ++ Z') = skipn (length X') Z').
      { replace (length ((lit ++ addr) ++ X')) with (length W + length X') by (rewrite !length_app; lia).
        apply skipn_app_plus. }
      rewrite Hsk. norm_goal.
      replace (30 * S nrec + 4) with (30 + (30 * nrec + 4)) by lia.
      exact (chain 30 (30 * nrec + 4) _ _ _ (conj Q1 E1) (conj Q2 E2)).
  - (* a record named by its gate codon *)
    destruct (translate_aux f (skipn 18 rest1)) as [X'|] eqn:Ht'; [|discriminate].
    cbn [option_map] in Ht. apply some_inj in Ht. subst Xr.
    pose proof (translate_aux_long _ _ _ Ht') as Hlong. rewrite length_skipn in Hlong.
    destruct (split_at rest1 18 ltac:(lia)) as (addr & rest2 & -> & Ha).
    rewrite (skipn_app_exact addr rest2 18 Ha) in Ht'.
    rewrite (firstn_app_exact addr rest2 18 Ha) in HU, HZ |- *.
    change (if e3 then 2 else if e2 then 1 else 0) with (kind_of e3 e2) in HU, HZ |- *.
    rewrite !length_app, length_gate_bits in HU, HZ. cbn [length] in Hd. rewrite length_app in Hd.
    destruct (split_at Z 26 ltac:(lia)) as (W & Z' & -> & HW).
    destruct (seg_gate b3 b2 b1 b0 e3 e2 s0 s1 addr (rest2 ++ tail) done U W Z' K E32 Ha HW ltac:(lia) ltac:(lia))
      as [Q1 E1].
    destruct (IH rest2 X' (done ++ e3 :: e2 :: s0 :: s1 :: addr) tail (U ++ gate_bits (kind_of e3 e2) s0 s1 ++ addr)
                Z' K e3 e2 s0 s1 Ht' ltac:(rewrite length_app; cbn [length]; rewrite ?length_app; lia)
                ltac:(rewrite !length_app, length_gate_bits; lia) ltac:(rewrite length_app in HZ; lia))
      as (nrec & Hn & Q2 & E2).
    norm_in E2.
    exists (S nrec). split; [rewrite !length_app, length_gate_bits; lia|].
    assert (Hsk : skipn (length (gate_bits (kind_of e3 e2) s0 s1 ++ addr ++ X')) (W ++ Z') = skipn (length X') Z').
    { replace (length (gate_bits (kind_of e3 e2) s0 s1 ++ addr ++ X')) with (length W + length X')
        by (rewrite !length_app, length_gate_bits; lia).
      apply skipn_app_plus. }
    rewrite Hsk. norm_goal.
    replace (30 * S nrec + 4) with (30 + (30 * nrec + 4)) by lia.
    exact (chain 30 (30 * nrec + 4) _ _ _ (conj Q1 E1) (conj Q2 E2)).
Qed.

(* ---- the description read again in copy mode ------------------------------------------------- *)
Lemma copy_phase : forall f rest Xr done tail A V Z b3 b2 b1 b0,
  translate_aux f rest = Some Xr -> length done + length rest <= L -> length V + length rest <= L ->
  length rest <= length Z ->
  quiet (length rest - 1) (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (rest ++ tail)) A (past L V Z))
  /\ ho (dout (dsteps (length rest - 1) (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (rest ++ tail)) A
                                            (past L V Z)))) = true
  /\ dsteps (length rest) (mkD (mkC PC 3 b3 b2 b1 b0 true) (past L done (rest ++ tail)) A (past L V Z))
     = mkD (mkC PI 1 true true true true false) (past L (done ++ rest) tail) (mkT (td A) 0)
           (mkT (V ++ rest ++ skipn (length rest) Z) 0).
Proof.
  induction f as [|f IH]; intros rest Xr done tail A V Z b3 b2 b1 b0 Ht Hd HV HZ; [discriminate|].
  destruct rest as [|e3 [|e2 [|s0 [|s1 rest1]]]]; try discriminate.
  rewrite translate_aux_S in Ht.
  destruct (e3 && e2) eqn:E32.
  - apply andb_prop in E32 as [-> ->].
    destruct (s0 && s1) eqn:Es.
    + (* the end codon *)
      destruct rest1; [|discriminate]. apply andb_prop in Es as [-> ->].
      cbn [length] in Hd, HV, HZ.
      destruct Z as [|w1 [|w2 [|w3 [|w4 Z]]]]; cbn [length] in HZ; try lia.
      exact (codon_copy_end b3 b2 b1 b0 done tail A V w1 w2 w3 w4 Z ltac:(lia) ltac:(lia)).
    + (* an escaped record *)
      destruct (Nat.eqb (length rest1) 0) eqn:El; [discriminate|].
      destruct (translate_aux f (skipn 26 rest1)) as [X'|] eqn:Ht'; [|discriminate].
      pose proof (translate_aux_long _ _ _ Ht') as Hlong. rewrite length_skipn in Hlong.
      destruct (split_at rest1 8 ltac:(lia)) as (lit & r1 & -> & Hl).
      destruct (split_at r1 18 ltac:(rewrite length_app in Hlong; lia)) as (addr & rest2 & -> & Ha).
      assert (Hs26 : skipn 26 (lit ++ addr ++ rest2) = rest2)
        by (rewrite app_assoc; apply skipn_app_exact; rewrite length_app; lia).
      rewrite Hs26 in Ht'. pose proof (translate_aux_long _ _ _ Ht') as H4.
      assert (Hlen : length (true :: true :: s0 :: s1 :: lit ++ addr ++ rest2) = 30 + length rest2)
        by (cbn [length]; rewrite !length_app; lia).
      rewrite Hlen in Hd, HV, HZ |- *.
      destruct (split_at Z 30 ltac:(lia)) as (W & Z' & -> & HW).
      destruct (seg_copy_esc b3 b2 b1 b0 s0 s1 lit addr (rest2 ++ tail) done A V W Z' Es Hl Ha HW
                  ltac:(lia) ltac:(lia)) as [Q1 E1].
      destruct (IH rest2 X' (done ++ true :: true :: s0 :: s1 :: lit ++ addr) tail A
                  (V ++ true :: true :: s0 :: s1 :: lit ++ addr) Z' true true s0 s1 Ht'
                  ltac:(rewrite length_app; cbn [length]; rewrite !length_app; lia)
                  ltac:(rewrite length_app; cbn [length]; rewrite !length_app; lia)
                  ltac:(rewrite length_app in HZ; lia)) as (Q2 & H2 & E2).
      norm_in E2.
      assert (Hsk : skipn (30 + length rest2) (W ++ Z') = skipn (length rest2) Z') by (rewrite <- HW; apply skipn_app_plus).
      rewrite Hsk. norm_goal.
      exact (chain_last 30 (length rest2) _ _ _ (conj Q1 E1) (conj Q2 (conj H2 E2)) ltac:(lia)).
  - (* a record named by its gate codon *)
    destruct (translate_aux f (skipn 18 rest1)) as [X'|] eqn:Ht'; [|discriminate].
    pose proof (translate_aux_long _ _ _ Ht') as Hlong. rewrite length_skipn in Hlong.
    destruct (split_at rest1 18 ltac:(lia)) as (addr & rest2 & -> & Ha).
    rewrite (skipn_app_exact addr rest2 18 Ha) in Ht'. pose proof (translate_aux_long _ _ _ Ht') as H4.
    assert (Hlen : length (e3 :: e2 :: s0 :: s1 :: addr ++ rest2) = 22 + length rest2)
      by (cbn [length]; rewrite length_app; lia).
    rewrite Hlen in Hd, HV, HZ |- *.
    destruct (split_at Z 22 ltac:(lia)) as (W & Z' & -> & HW).
    destruct (seg_copy_gate b3 b2 b1 b0 e3 e2 s0 s1 addr (rest2 ++ tail) done A V W Z' E32 Ha HW
                ltac:(lia) ltac:(lia)) as [Q1 E1].
    destruct (IH rest2 X' (done ++ e3 :: e2 :: s0 :: s1 :: addr) tail A (V ++ e3 :: e2 :: s0 :: s1 :: addr) Z'
                e3 e2 s0 s1 Ht' ltac:(rewrite length_app; cbn [length]; rewrite ?length_app; lia)
                ltac:(rewrite length_app; cbn [length]; rewrite ?length_app; lia)
                ltac:(rewrite length_app in HZ; lia)) as (Q2 & H2 & E2).
    norm_in E2.
    assert (Hsk : skipn (22 + length rest2) (W ++ Z') = skipn (length rest2) Z') by (rewrite <- HW; apply skipn_app_plus).
    rewrite Hsk. norm_goal.
    exact (chain_last 22 (length rest2) _ _ _ (conj Q1 E1) (conj Q2 (conj H2 E2)) ltac:(lia)).
Qed.

(* ---- one generation -------------------------------------------------------------------------- *)
(* From phase I, with a description d of the image X at the start of the read tape and whatever the
   arm and the copy tape hold, a generation is one pass of phase I, 30 passes per record of X and 4
   on the end codon in construct mode, and one pass per bit of d in copy mode. Only its last pass
   hands over. The arm then holds X from its first cell and the copy tape d, both heads at cell 0. *)
Theorem generation : forall d X tail R A K zc c3 c2 c1 c0 m,
  translate d = Some X -> td R = d ++ tail -> length d <= L -> length X <= N ->
  exists nrec, length X = 26 * nrec
    /\ quiet (30 * nrec + 4 + length d) (mkD (mkC PI zc c3 c2 c1 c0 m) R A K)
    /\ ho (dout (dsteps (30 * nrec + 4 + length d) (mkD (mkC PI zc c3 c2 c1 c0 m) R A K))) = true
    /\ dsteps (S (30 * nrec + 4 + length d)) (mkD (mkC PI zc c3 c2 c1 c0 m) R A K)
       = mkD (mkC PI 1 true true true true false) (past L d tail)
             (mkT (X ++ repeat false (N - length X)) 0) (mkT (d ++ repeat false (L - length d)) 0).
Proof.
  intros d X tail R A K zc c3 c2 c1 c0 m Ht HR HdL HXN. unfold translate in Ht.
  pose proof (translate_aux_long _ _ _ Ht) as Hd4.
  destruct (pass_PI zc c3 c2 c1 c0 m R A K) as [Q0 E0].
  assert (E0' : dstep (mkD (mkC PI zc c3 c2 c1 c0 m) R A K)
                = mkD (mkC PC 3 c3 c2 c1 c0 false) (past L [] (d ++ tail)) (past N [] (repeat false N))
                      (past L [] (repeat false L))).
  { rewrite E0, HR. unfold past. cbn [length app]. rewrite !Nat.Div0.mod_0_l. reflexivity. }
  destruct (construct_phase (length d) d X [] tail [] (repeat false N) (past L [] (repeat false L)) c3 c2 c1 c0 Ht
              ltac:(cbn [length]; lia) ltac:(cbn [length]; lia) ltac:(rewrite repeat_length; lia))
    as (nrec & Hn & Q1 & E1).
  cbn [app] in E1.
  destruct (copy_phase (length d) d X [] tail (past N X (skipn (length X) (repeat false N))) [] (repeat false L)
              true true true true Ht ltac:(cbn [length]; lia) ltac:(cbn [length]; lia)
              ltac:(rewrite repeat_length; lia)) as (Q2 & H2 & E2).
  cbn [app] in E2.
  assert (Htd : td (past N X (skipn (length X) (repeat false N))) = X ++ repeat false (N - length X))
    by (unfold past; cbn [td]; rewrite skipn_repeat_false; reflexivity).
  rewrite Htd, (skipn_repeat_false (length d) L) in E2.
  destruct (chain_last (1 + (30 * nrec + 4)) (length d) _ _ _
              (chain 1 (30 * nrec + 4) _ _ _ (one _ _ Q0 E0') (conj Q1 E1)) (conj Q2 (conj H2 E2)) ltac:(lia))
    as (Q & H & E).
  exists nrec. split; [exact Hn|].
  replace (1 + (30 * nrec + 4) + length d - 1) with (30 * nrec + 4 + length d) in Q, H by lia.
  replace (1 + (30 * nrec + 4) + length d) with (S (30 * nrec + 4 + length d)) in E by lia.
  exact (conj Q (conj H E)).
Qed.

End Dec.