(* Within one pass, each head is seen through the cell under it when the pass starts and what the pass
   does to it: the value it writes there, the cells it moves, whether it returns to its origin and
   whether its bank or tape is cleared; the active bank through the index of the record at its head.
   One step of the machine refines one step of this abstract machine. *)
From Stdlib Require Import List Bool Arith ZArith Lia.
Import ListNotations.
From TH Require Import TwoHead Net.

Record ahead := mkH { acur : bool; awr : option bool; amv : nat; arw : bool; acl : bool }.

(* the head is still on its first cell and its store is untouched but for its own write there *)
Definition hok (h : ahead) : bool := Nat.eqb (amv h) 0 && negb (arw h) && negb (acl h).
Definition hval (h : ahead) : bool := match awr h with Some v => v | None => acur h end.
Definition hwrite (h : ahead) (v : bool) : ahead := mkH (acur h) (Some v) (amv h) (arw h) (acl h).
Definition hadv (h : ahead) : ahead := mkH (acur h) (awr h) (S (amv h)) (arw h) (acl h).
Definition hrew (h : ahead) : ahead := mkH (acur h) (awr h) 0 true (acl h).
Definition hclr (h : ahead) : ahead := mkH (acur h) (awr h) (amv h) (arw h) true.

Record ast := mkAS { aw : list bool; aR : ahead; aA : ahead; aK : ahead; ai : nat; aho : bool; bad : bool }.

Definition acell (t : ast) (x : nat) : bool :=
  if Nat.eqb x SINK then false
  else if Nat.eqb x RD then hval (aR t)
  else if Nat.eqb x ARM then hval (aA t)
  else if Nat.eqb x CPY then hval (aK t)
  else wget (aw t) x.

(* an operand with a nonzero weight on a head cell must find the head on its first cell *)
Definition opok (t : ast) (x : nat) (w : Z) : bool :=
  if Z.eqb w 0 then true
  else if Nat.eqb x RD then hok (aR t)
  else if Nat.eqb x ARM then hok (aA t)
  else if Nat.eqb x CPY then hok (aK t)
  else true.

Definition astepres (rs : list rec) (t : ast) (a0 : nat) (w0 : Z) (a1 : nat) (w1 : Z) (ao : nat) (v : bool) : ast :=
  let wn := wnext (aw t) ao v in
  let A1 := if Nat.eqb ao ARM then hwrite (aA t) v else aA t in
  let K1 := if Nat.eqb ao CPY then hwrite (aK t) v else aK t in
  let okw := (if Nat.eqb ao ARM then hok (aA t) else true) && (if Nat.eqb ao CPY then hok (aK t) else true) in
  let R2 := if wget wn RR then hrew (aR t) else if wget wn AR then hadv (aR t) else aR t in
  let A1' := if wget wn CB then hclr A1 else A1 in
  let A2 := if wget wn RA then hrew A1' else if wget wn AA then hadv A1' else A1' in
  let K1' := if wget wn CT then hclr K1 else K1 in
  let K2 := if wget wn RC then hrew K1' else if wget wn AC then hadv K1' else K1' in
  let okho := negb (wget wn HO) || Nat.eqb (S (ai t)) (length rs) in
  mkAS (clearq wn) R2 A2 K2 (S (ai t)) (aho t || wget wn HO)
       (bad t || aho t || negb (opok t a0 w0 && opok t a1 w1 && okw && okho)).

Definition astep (rs : list rec) (t : ast) : ast :=
  match nth_error rs (ai t) with
  | None => mkAS (aw t) (aR t) (aA t) (aK t) (ai t) (aho t) true
  | Some (Rec a0 w0 a1 w1 beta ao) =>
      astepres rs t a0 w0 a1 w1 ao (Z.leb 0 (w0 * b2z (acell t a0) + w1 * b2z (acell t a1) + beta)%Z)
  end.

Fixpoint aiter (n : nat) (rs : list rec) (t : ast) : ast :=
  match n with O => t | S m => aiter m rs (astep rs t) end.

Definition enc (rs : list rec) : list bool := concat (map enc_rec rs).

(* ---- the effect of a pass on a tape and on a bank ---------------------------------------------- *)
Fixpoint iter {A : Type} (n : nat) (f : A -> A) (x : A) : A := match n with O => x | S m => f (iter m f x) end.

Definition tape_eff (L : nat) (h : ahead) (t : tape) : tape :=
  mkT (if acl h then repeat false L else match awr h with Some v => upd (td t) (th t) v | None => td t end)
      (iter (amv h) (succ_mod L) (if arw h then 0 else th t)).

Definition bank_eff (S0 b : nat) (h : ahead) (q : bank) : bank :=
  iter (amv h) (advb S0 b)
       (mkB (if acl h then repeat false (S0 * b) else
               match awr h with Some v => upd (bq q) (bs q * b + bj q) v | None => bq q end)
            (if arw h then 0 else bs q) (if arw h then 0 else bj q)).

(* ---- lists ------------------------------------------------------------------------------------- *)
Lemma upd_length : forall l i v, length (upd l i v) = length l.
Proof. induction l as [|x l IH]; intros [|i] v; cbn; auto. Qed.

Lemma nth_upd_same : forall l i v, i < length l -> nth i (upd l i v) false = v.
Proof. induction l as [|x l IH]; intros [|i] v Hi; cbn in *; try lia; auto. apply IH. lia. Qed.

Lemma nth_upd_other : forall l i j v, i <> j -> nth j (upd l i v) false = nth j l false.
Proof.
  induction l as [|x l IH]; intros i j v Hij; [reflexivity|].
  destruct i as [|i], j as [|j]; cbn; try reflexivity; [lia|]. apply IH. lia.
Qed.

Lemma upd_upd : forall l i v w, upd (upd l i v) i w = upd l i w.
Proof. induction l as [|x l IH]; intros [|i] v w; cbn; f_equal; auto. Qed.

Lemma upd_same : forall l i, upd l i (nth i l false) = l.
Proof. induction l as [|x l IH]; intros [|i]; cbn; f_equal; auto. Qed.

Lemma wget_upd : forall w i v x,
  wget (upd w i v) x = if Nat.eqb x i && Nat.ltb i (length w) then v else wget w x.
Proof.
  unfold wget. induction w as [|y w IH]; intros i v x.
  - simpl. rewrite andb_false_r. destruct x; reflexivity.
  - destruct i as [|i], x as [|x]; simpl; try reflexivity; rewrite IH; reflexivity.
Qed.

Lemma length_wnext : forall w ao v, length (wnext w ao v) = length w.
Proof. intros w ao v; unfold wnext. destruct (Nat.leb ao CPY); [reflexivity | apply upd_length]. Qed.

Lemma length_clearq : forall w, length (clearq w) = length w.
Proof. intro w; unfold clearq. rewrite !upd_length. reflexivity. Qed.

(* the cells from 4 on: two windows agree there *)
Definition agree (w w' : list bool) : Prop := forall x, 4 <= x -> wget w x = wget w' x.

Lemma agree_upd : forall w w' i v, agree w w' -> length w = length w' -> agree (upd w i v) (upd w' i v).
Proof.
  intros w w' i v H Hl x Hx. rewrite !wget_upd, Hl.
  destruct (Nat.eqb x i && Nat.ltb i (length w')); auto.
Qed.

Lemma agree_wnext : forall w w' ao v, agree w w' -> length w = length w' -> agree (wnext w ao v) (wnext w' ao v).
Proof. intros w w' ao v H Hl; unfold wnext. destruct (Nat.leb ao CPY); auto using agree_upd. Qed.

Lemma agree_clearq : forall w w', agree w w' -> length w = length w' -> agree (clearq w) (clearq w').
Proof.
  intros w w' H Hl; unfold clearq.
  repeat (apply agree_upd; [|rewrite ?upd_length; auto]). exact H.
Qed.

Lemma iter_advb_bq : forall S1 b' n q, bq (iter n (advb S1 b') q) = bq q.
Proof.
  intros S1 b' n. induction n as [|n IH]; intro q; [reflexivity|].
  change (bq (advb S1 b' (iter n (advb S1 b') q)) = bq q).
  transitivity (bq (iter n (advb S1 b') q)); [|apply IH].
  set (X := iter n (advb S1 b') q). unfold advb. destruct (Nat.eqb (S (bj X)) b'); reflexivity.
Qed.

(* the arm's moves do not depend on the bits of the bank *)
Lemma iter_advb_mkB : forall S1 b' n X Y s j,
  iter n (advb S1 b') (mkB X s j) = mkB X (bs (iter n (advb S1 b') (mkB Y s j))) (bj (iter n (advb S1 b') (mkB Y s j))).
Proof.
  intros S1 b' n. induction n as [|n IH]; intros X Y s j; [reflexivity|]. cbn [iter].
  rewrite (IH X Y s j). set (Z := iter n (advb S1 b') (mkB Y s j)). unfold advb. cbn [bq bs bj].
  destruct (Nat.eqb (S (bj Z)) b'); reflexivity.
Qed.

Lemma succ_mod_mod : forall n x, 1 <= n -> succ_mod n (x mod n) = S x mod n.
Proof.
  intros n x Hn. pose proof (Nat.mod_upper_bound x n ltac:(lia)) as H.
  rewrite <- Nat.add_1_r, <- Nat.Div0.add_mod_idemp_l. unfold succ_mod.
  destruct (Nat.eqb_spec (S (x mod n)) n) as [E|E].
  - rewrite Nat.add_1_r, E. symmetry. apply Nat.Div0.mod_same.
  - rewrite Nat.add_1_r. symmetry. apply Nat.mod_small. lia.
Qed.

(* ---- one step of the machine, against one step of the abstract machine ------------------------ *)
Section Refine.
Variables (al K S0 L : nat) (rs : list rec) (s0 : st).
Hypotheses (HK : 2 <= K) (HS : 1 <= S0) (HL : 1 <= L) (Hfit : fits al K S0 L s0).

Let k0 := kap s0.
Let i0 := succ_mod K k0.
Let b := recw al.

(* the concrete state s and the abstract state t agree, from the state s0 that started the pass *)
Definition rel (s : st) (t : ast) : Prop :=
  agree (win s) (aw t) /\ length (win s) = 2 ^ al /\ length (aw t) = 2 ^ al
  /\ kap s = (if aho t then i0 else k0)
  /\ length (banks s) = K /\ length (tapes s) = K
  /\ nth k0 (banks s) bank0 = mkB (bq (nth k0 (banks s0) bank0)) (ai t) (bj (nth k0 (banks s0) bank0))
  /\ nth i0 (banks s) bank0 = bank_eff S0 b (aA t) (nth i0 (banks s0) bank0)
  /\ nth k0 (tapes s) tape0 = tape_eff L (aR t) (nth k0 (tapes s0) tape0)
  /\ nth i0 (tapes s) tape0 = tape_eff L (aK t) (nth i0 (tapes s0) tape0)
  /\ (forall x, x < K -> x <> k0 -> x <> i0 -> nth x (banks s) bank0 = nth x (banks s0) bank0)
  /\ (forall x, x < K -> x <> k0 -> x <> i0 -> nth x (tapes s) tape0 = nth x (tapes s0) tape0)
  /\ acur (aR t) = tget (nth k0 (tapes s0) tape0)
  /\ acur (aA t) = bget al (nth i0 (banks s0) bank0)
  /\ acur (aK t) = tget (nth i0 (tapes s0) tape0)
  /\ awr (aR t) = None.

Lemma k0_lt : k0 < K.
Proof. destruct Hfit as (_ & H & _). exact H. Qed.

Lemma i0_lt : i0 < K.
Proof. unfold i0, succ_mod. pose proof k0_lt. destruct (Nat.eqb_spec (S k0) K); lia. Qed.

Lemma i0_k0 : i0 <> k0.
Proof. unfold i0, succ_mod. pose proof k0_lt. destruct (Nat.eqb_spec (S k0) K); lia. Qed.

Lemma bank0_ok : forall x, x < K -> length (bq (nth x (banks s0) bank0)) = S0 * b
  /\ bs (nth x (banks s0) bank0) < S0 /\ bj (nth x (banks s0) bank0) < b.
Proof. intros x Hx. destruct Hfit as (_ & _ & _ & _ & H & _). apply H. exact Hx. Qed.

Lemma tape0_ok : forall x, x < K -> length (td (nth x (tapes s0) tape0)) = L /\ th (nth x (tapes s0) tape0) < L.
Proof. intros x Hx. destruct Hfit as (_ & _ & _ & _ & _ & H). apply H. exact Hx. Qed.

(* reading a head cell of a related state, the head being on its first cell *)
Lemma tget_eff : forall h t0, hok h = true -> th t0 < length (td t0) ->
  tget (tape_eff L h t0) = match awr h with Some v => v | None => tget t0 end.
Proof.
  intros h t0 Hok Ht. unfold hok in Hok. destruct h as [c w m r cl]. cbn [amv arw acl] in Hok.
  destruct m; [|discriminate]. destruct r, cl; try discriminate.
  unfold tape_eff, tget. cbn [acl awr amv arw iter td th]. destruct w; [apply nth_upd_same; exact Ht | reflexivity].
Qed.

Lemma bget_eff : forall h q, hok h = true -> bs q * b + bj q < length (bq q) ->
  bget al (bank_eff S0 b h q) = match awr h with Some v => v | None => bget al q end.
Proof.
  intros h q Hok Hq. unfold hok in Hok. destruct h as [c w m r cl]. cbn [amv arw acl] in Hok.
  destruct m; [|discriminate]. destruct r, cl; try discriminate.
  unfold bank_eff, bget, apos. cbn [acl awr amv arw iter bq bs bj]. fold b.
  destruct w; [apply nth_upd_same; exact Hq | reflexivity].
Qed.

(* the concrete operations on the effect of a head *)
Lemma tape_eff_write : forall h t0 v, hok h = true ->
  mkT (upd (td (tape_eff L h t0)) (th (tape_eff L h t0)) v) (th (tape_eff L h t0)) = tape_eff L (hwrite h v) t0.
Proof.
  intros h t0 v Hok. unfold hok in Hok. destruct h as [c w m r cl]. cbn [amv arw acl] in Hok.
  destruct m; [|discriminate]. destruct r, cl; try discriminate.
  unfold tape_eff, hwrite. cbn [acl awr amv arw iter td th acur]. f_equal. destruct w; [apply upd_upd | reflexivity].
Qed.

Lemma tape_eff_adv : forall h t0, mkT (td (tape_eff L h t0)) (succ_mod L (th (tape_eff L h t0))) = tape_eff L (hadv h) t0.
Proof. intros. reflexivity. Qed.

Lemma tape_eff_rew : forall h t0, mkT (td (tape_eff L h t0)) 0 = tape_eff L (hrew h) t0.
Proof. intros. reflexivity. Qed.

Lemma tape_eff_clr : forall h t0, mkT (repeat false L) (th (tape_eff L h t0)) = tape_eff L (hclr h) t0.
Proof. intros. reflexivity. Qed.

Lemma bank_eff_write : forall h q v, hok h = true ->
  mkB (upd (bq (bank_eff S0 b h q)) (apos al (bank_eff S0 b h q)) v) (bs (bank_eff S0 b h q)) (bj (bank_eff S0 b h q))
  = bank_eff S0 b (hwrite h v) q.
Proof.
  intros h q v Hok. unfold hok in Hok. destruct h as [c w m r cl]. cbn [amv arw acl] in Hok.
  destruct m; [|discriminate]. destruct r, cl; try discriminate.
  unfold bank_eff, hwrite, apos. cbn [acl awr amv arw iter bq bs bj acur]. fold b. f_equal.
  destruct w; [apply upd_upd | reflexivity].
Qed.

Lemma bank_eff_adv : forall h q, advb S0 b (bank_eff S0 b h q) = bank_eff S0 b (hadv h) q.
Proof. intros. reflexivity. Qed.

Lemma bank_eff_rew : forall h q, mkB (bq (bank_eff S0 b h q)) 0 0 = bank_eff S0 b (hrew h) q.
Proof.
  intros [c w m r cl] q. unfold bank_eff, hrew. cbn [acl awr amv arw iter bq bs bj acur].
  rewrite iter_advb_bq. reflexivity.
Qed.

Lemma bank_eff_clr : forall h q,
  mkB (repeat false (S0 * b)) (bs (bank_eff S0 b h q)) (bj (bank_eff S0 b h q)) = bank_eff S0 b (hclr h) q.
Proof.
  intros [c w m r cl] q. unfold bank_eff, hclr. cbn [acl awr amv arw acur].
  symmetry. apply (iter_advb_mkB S0 b m (repeat false (S0 * b))).
Qed.

Lemma eta_bank : forall q, mkB (bq q) (bs q) (bj q) = q.
Proof. intros [x y z]. reflexivity. Qed.

Lemma eta_tape : forall t, mkT (td t) (th t) = t.
Proof. intros [x y]. reflexivity. Qed.

(* the active bank holds the records rs from its first slot *)
Hypothesis Hdec : forall r, In r rs -> decodeA al (enc_recA al r) = r.
Hypothesis Hact : forall a r, nth_error rs a = Some r ->
  firstn b (skipn (a * b) (bq (nth k0 (banks s0) bank0))) = enc_recA al r.
Hypothesis Hrs : length rs <= S0.

Definition relA (s : st) (t : ast) : Prop :=
  agree (win s) (aw t) /\ length (win s) = 2 ^ al /\ length (aw t) = 2 ^ al
  /\ kap s = (if aho t then i0 else k0)
  /\ length (banks s) = K /\ length (tapes s) = K
  /\ nth k0 (banks s) bank0 = mkB (bq (nth k0 (banks s0) bank0)) (ai t mod S0) (bj (nth k0 (banks s0) bank0))
  /\ nth i0 (banks s) bank0 = bank_eff S0 b (aA t) (nth i0 (banks s0) bank0)
  /\ nth k0 (tapes s) tape0 = tape_eff L (aR t) (nth k0 (tapes s0) tape0)
  /\ nth i0 (tapes s) tape0 = tape_eff L (aK t) (nth i0 (tapes s0) tape0)
  /\ (forall x, x < K -> x <> k0 -> x <> i0 -> nth x (banks s) bank0 = nth x (banks s0) bank0)
  /\ (forall x, x < K -> x <> k0 -> x <> i0 -> nth x (tapes s) tape0 = nth x (tapes s0) tape0)
  /\ acur (aR t) = tget (nth k0 (tapes s0) tape0)
  /\ acur (aA t) = bget al (nth i0 (banks s0) bank0)
  /\ acur (aK t) = tget (nth i0 (tapes s0) tape0)
  /\ awr (aR t) = None.

Lemma head_ops_acur : forall h v,
  acur (hwrite h v) = acur h /\ acur (hadv h) = acur h /\ acur (hrew h) = acur h /\ acur (hclr h) = acur h.
Proof. intros. repeat split. Qed.

Lemma step_refines : forall s t,
  relA s t -> ai t < length rs -> aho t = false -> bad (astep rs t) = false ->
  relA (step al K S0 L s) (astep rs t).
Proof.
  intros s t Hrel Hi Hho Hbad. pose proof k0_lt as Hk0. pose proof i0_lt as Hi0. pose proof i0_k0 as Hik.
  destruct Hrel as (Hw & Hlw & Hla & Hkap & HlB & HlT & HA & HI & HR & HC & HoB & HoT & cR & cA & cK & wR).
  rewrite Hho in Hkap.
  destruct (nth_error rs (ai t)) as [r|] eqn:Er; [|apply nth_error_None in Er; lia].
  assert (Hdr : decodeA al (enc_recA al r) = r) by (apply Hdec; eapply nth_error_In; exact Er).
  destruct r as [a0 w0 a1 w1 beta ao].
  (* the abstract step and its checks *)
  unfold astep in Hbad |- *. rewrite Er in Hbad |- *.
  set (va := Z.leb 0 (w0 * b2z (acell t a0) + w1 * b2z (acell t a1) + beta)%Z) in *.
  unfold astepres in Hbad. cbv zeta in Hbad. cbn [bad] in Hbad.
  rewrite Hho in Hbad. apply orb_false_iff in Hbad as [Hb0 Hb]. apply orb_false_iff in Hb0 as [Hb0 _].
  apply negb_false_iff in Hb.
  apply andb_prop in Hb as [Hb Hokho]. apply andb_prop in Hb as [Hb Hokw]. apply andb_prop in Hb as [Hop0 Hop1].
  assert (OkA : Nat.eqb ao ARM = true -> hok (aA t) = true)
    by (intro E; rewrite E in Hokw; apply andb_prop in Hokw as [H _]; exact H).
  assert (OkK : Nat.eqb ao CPY = true -> hok (aK t) = true)
    by (intro E; rewrite E in Hokw; apply andb_prop in Hokw as [_ H]; exact H).
  (* the concrete step reads the record at slot ai t of the active bank *)
  destruct (bank0_ok k0 Hk0) as (Hq0 & _ & _). destruct (bank0_ok i0 Hi0) as (Hqi & Hsi & Hji).
  destruct (tape0_ok k0 Hk0) as (Hd0 & Ht0). destruct (tape0_ok i0 Hi0) as (Hdi & Hti).
  assert (Hslot : slot al (nth (kap s) (banks s) bank0) = enc_recA al (Rec a0 w0 a1 w1 beta ao)).
  { rewrite Hkap, HA. unfold slot. cbn [bq bs]. rewrite Nat.mod_small by lia. apply Hact. exact Er. }
  (* the cells the record reads are those of the abstract state *)
  assert (Hcell : forall a w, opok t a w = true -> (w * b2z (cellof al K s a) = w * b2z (acell t a))%Z).
  { intros a w Ho. unfold opok in Ho. unfold cellof, acell. rewrite Hkap. fold i0.
    destruct (Z.eqb_spec w 0) as [Ew|Ew]; [rewrite Ew; reflexivity|].
    destruct (Nat.eqb_spec a SINK); [reflexivity|].
    destruct (Nat.eqb_spec a RD).
    { rewrite HR, (tget_eff (aR t) _ Ho) by lia. rewrite wR. unfold hval. rewrite wR, cR. reflexivity. }
    destruct (Nat.eqb_spec a ARM).
    { rewrite HI, (bget_eff (aA t) _ Ho) by (rewrite Hqi; unfold b; nia).
      unfold hval. destruct (awr (aA t)); [reflexivity|]. rewrite cA. reflexivity. }
    destruct (Nat.eqb_spec a CPY).
    { rewrite HC, (tget_eff (aK t) _ Ho) by lia.
      unfold hval. destruct (awr (aK t)); [reflexivity|]. rewrite cK. reflexivity. }
    rewrite Hw by (unfold SINK, RD, ARM, CPY in *; lia). reflexivity. }
  assert (Hv : Z.leb 0 (w0 * b2z (cellof al K s a0) + w1 * b2z (cellof al K s a1) + beta)%Z = va).
  { unfold va. rewrite (Hcell a0 w0 Hop0), (Hcell a1 w1 Hop1). reflexivity. }
  unfold step. rewrite Hslot, Hdr. rewrite Hv.
  (* the state after the step *)
  assert (Hag : agree (wnext (win s) ao va) (wnext (aw t) ao va)) by (apply agree_wnext; [exact Hw | congruence]).
  assert (Hq : forall c, 4 <= c -> wget (wnext (win s) ao va) c = wget (wnext (aw t) ao va) c) by (intros; apply Hag; lia).
  unfold stepres, astepres. cbv zeta. rewrite Hkap. fold i0.
  rewrite !Hq by (unfold AR, AA, AC, RR, RA, RC, CB, CT, HO; lia).
  refine (conj _ (conj _ (conj _ (conj _ (conj _ (conj _ (conj _ (conj _ (conj _ (conj _ (conj _ (conj _ _)))))))))))).
  - cbn [win aw]. apply agree_clearq; [exact Hag | rewrite !length_wnext; congruence].
  - cbn [win]. rewrite length_clearq, length_wnext. exact Hlw.
  - cbn [aw]. rewrite length_clearq, length_wnext. exact Hla.
  - cbn [kap aho]. rewrite Hho. cbn [orb]. reflexivity.
  - cbn [banks]. rewrite length_map, length_seq. reflexivity.
  - cbn [tapes]. rewrite length_map, length_seq. reflexivity.
  - (* the active bank *)
    cbn [banks ai]. rewrite (nth_map_seq _ _ K k0 bank0 Hk0), Nat.eqb_refl. rewrite HA. cbn [bq bs bj].
    rewrite succ_mod_mod by lia. reflexivity.
  - (* the idle bank *)
    cbn [banks aA]. rewrite (nth_map_seq _ _ K i0 bank0 Hi0), (proj2 (Nat.eqb_neq i0 k0) Hik), Nat.eqb_refl. rewrite HI.
    assert (HI1 : (if Nat.eqb ao ARM
                   then mkB (upd (bq (bank_eff S0 b (aA t) (nth i0 (banks s0) bank0)))
                              (apos al (bank_eff S0 b (aA t) (nth i0 (banks s0) bank0))) va)
                            (bs (bank_eff S0 b (aA t) (nth i0 (banks s0) bank0)))
                            (bj (bank_eff S0 b (aA t) (nth i0 (banks s0) bank0)))
                   else bank_eff S0 b (aA t) (nth i0 (banks s0) bank0))
                  = bank_eff S0 b (if Nat.eqb ao ARM then hwrite (aA t) va else aA t) (nth i0 (banks s0) bank0)).
    { destruct (Nat.eqb ao ARM) eqn:E; [|reflexivity]. apply bank_eff_write. apply OkA. reflexivity. }
    rewrite HI1. set (A1 := if Nat.eqb ao ARM then hwrite (aA t) va else aA t).
    assert (HI1' : mkB (if wget (wnext (aw t) ao va) CB then repeat false (S0 * recw al) else bq (bank_eff S0 b A1 (nth i0 (banks s0) bank0)))
                       (bs (bank_eff S0 b A1 (nth i0 (banks s0) bank0))) (bj (bank_eff S0 b A1 (nth i0 (banks s0) bank0)))
                   = bank_eff S0 b (if wget (wnext (aw t) ao va) CB then hclr A1 else A1) (nth i0 (banks s0) bank0)).
    { destruct (wget (wnext (aw t) ao va) CB); [apply bank_eff_clr | apply eta_bank]. }
    rewrite HI1'. set (A1' := if wget (wnext (aw t) ao va) CB then hclr A1 else A1).
    destruct (wget (wnext (aw t) ao va) RA); [apply bank_eff_rew|].
    destruct (wget (wnext (aw t) ao va) AA); [apply bank_eff_adv | reflexivity].
  - (* the read tape *)
    cbn [tapes aR]. rewrite (nth_map_seq _ _ K k0 tape0 Hk0), Nat.eqb_refl. rewrite HR.
    destruct (wget (wnext (aw t) ao va) RR); [apply tape_eff_rew|].
    destruct (wget (wnext (aw t) ao va) AR); [apply tape_eff_adv | apply eta_tape].
  - (* the copy tape *)
    cbn [tapes aK]. rewrite (nth_map_seq _ _ K i0 tape0 Hi0), (proj2 (Nat.eqb_neq i0 k0) Hik), Nat.eqb_refl. rewrite HC.
    assert (HC1 : (if Nat.eqb ao CPY
                   then mkT (upd (td (tape_eff L (aK t) (nth i0 (tapes s0) tape0))) (th (tape_eff L (aK t) (nth i0 (tapes s0) tape0))) va)
                            (th (tape_eff L (aK t) (nth i0 (tapes s0) tape0)))
                   else tape_eff L (aK t) (nth i0 (tapes s0) tape0))
                  = tape_eff L (if Nat.eqb ao CPY then hwrite (aK t) va else aK t) (nth i0 (tapes s0) tape0)).
    { destruct (Nat.eqb ao CPY) eqn:E; [|reflexivity]. apply tape_eff_write. apply OkK. reflexivity. }
    rewrite HC1. set (K1 := if Nat.eqb ao CPY then hwrite (aK t) va else aK t).
    assert (HC1' : mkT (if wget (wnext (aw t) ao va) CT then repeat false L else td (tape_eff L K1 (nth i0 (tapes s0) tape0)))
                       (th (tape_eff L K1 (nth i0 (tapes s0) tape0)))
                   = tape_eff L (if wget (wnext (aw t) ao va) CT then hclr K1 else K1) (nth i0 (tapes s0) tape0)).
    { destruct (wget (wnext (aw t) ao va) CT); [apply tape_eff_clr | apply eta_tape]. }
    transitivity (let C1' := tape_eff L (if wget (wnext (aw t) ao va) CT then hclr K1 else K1) (nth i0 (tapes s0) tape0) in
                  mkT (td C1') (if wget (wnext (aw t) ao va) RC then 0
                                else if wget (wnext (aw t) ao va) AC then succ_mod L (th C1') else th C1')).
    { cbv zeta. rewrite <- HC1'. cbn [td th]. reflexivity. }
    cbv zeta. set (K1' := if wget (wnext (aw t) ao va) CT then hclr K1 else K1).
    destruct (wget (wnext (aw t) ao va) RC); [apply tape_eff_rew|].
    destruct (wget (wnext (aw t) ao va) AC); [apply tape_eff_adv | apply eta_tape].
  - (* the other banks *)
    intros x Hx E1 E2. cbn [banks]. rewrite (nth_map_seq _ _ K x bank0 Hx).
    rewrite (proj2 (Nat.eqb_neq x k0) E1), (proj2 (Nat.eqb_neq x i0) E2). apply HoB; assumption.
  - (* the other tapes *)
    intros x Hx E1 E2. cbn [tapes]. rewrite (nth_map_seq _ _ K x tape0 Hx).
    rewrite (proj2 (Nat.eqb_neq x k0) E1), (proj2 (Nat.eqb_neq x i0) E2). apply HoT; assumption.
  - (* the cells under the heads when the pass started, and the read tape never written *)
    cbn [aR aA aK]. refine (conj _ (conj _ (conj _ _))).
    + destruct (wget (wnext (aw t) ao va) RR); [|destruct (wget (wnext (aw t) ao va) AR)]; exact cR.
    + destruct (wget (wnext (aw t) ao va) RA), (wget (wnext (aw t) ao va) AA), (wget (wnext (aw t) ao va) CB),
        (Nat.eqb ao ARM); exact cA.
    + destruct (wget (wnext (aw t) ao va) RC), (wget (wnext (aw t) ao va) AC), (wget (wnext (aw t) ao va) CT),
        (Nat.eqb ao CPY); exact cK.
    + destruct (wget (wnext (aw t) ao va) RR); [|destruct (wget (wnext (aw t) ao va) AR)]; exact wR.
Qed.

Lemma bad_mono : forall n t, bad t = true -> bad (aiter n rs t) = true.
Proof.
  induction n as [|n IH]; intros t H; cbn [aiter]; [exact H|].
  apply IH. unfold astep. destruct (nth_error rs (ai t)) as [[a0 w0 a1 w1 beta ao]|]; [|reflexivity].
  unfold astepres. cbv zeta. cbn [bad]. rewrite H. reflexivity.
Qed.

Lemma astep_clean : forall t, bad (astep rs t) = false -> bad t = false /\ aho t = false.
Proof.
  intros t H. unfold astep in H. destruct (nth_error rs (ai t)) as [[a0 w0 a1 w1 beta ao]|]; [|discriminate].
  unfold astepres in H. cbv zeta in H. cbn [bad] in H.
  apply orb_false_iff in H as [H _]. apply orb_false_iff in H as [H1 H2]. split; assumption.
Qed.

Lemma astep_ai : forall t, ai t < length rs -> ai (astep rs t) = S (ai t).
Proof.
  intros t H. unfold astep. destruct (nth_error rs (ai t)) as [[a0 w0 a1 w1 beta ao]|] eqn:E; [reflexivity|].
  apply nth_error_None in E. lia.
Qed.

Lemma aiter_ai : forall n t, ai t + n <= length rs -> ai (aiter n rs t) = ai t + n.
Proof.
  induction n as [|n IH]; intros t H; cbn [aiter]; [lia|]. rewrite IH; rewrite ?astep_ai; lia.
Qed.

(* a pass of the machine refines the abstract pass, as long as the abstract pass is not bad *)
Lemma pass_refines : forall n s t, relA s t -> ai t + n <= length rs -> bad (aiter n rs t) = false ->
  relA (itern al K S0 L n s) (aiter n rs t).
Proof.
  induction n as [|n IH]; intros s t Hrel Hn Hbad; [exact Hrel|].
  cbn [itern aiter] in *.
  assert (Hb1 : bad (astep rs t) = false).
  { destruct (bad (astep rs t)) eqn:E; [|reflexivity]. rewrite (bad_mono n _ E) in Hbad. discriminate. }
  destruct (astep_clean t Hb1) as [_ Hho].
  apply IH; [apply step_refines; auto; lia | rewrite astep_ai; lia | exact Hbad].
Qed.

End Refine.