(** W6-1 exit lemmas (formal-planning stage).

    Everything is stated in SOBCv10's frame and on SOBCv10's table
    ([1LB0RD_1LC0RC_1RA1LC_1LE0RB_1LF---_0LA0LE]); our machine is that table
    mirrored and renamed, started in SOBCv10's state D.  This file reuses an
    unmodified copy of SOBCv10.v as a library (logical name W61.SOBCv10).

    Contents
    - T2   : the raw pass with a tail [U^(2k+1) B t], k = 0..5
             ([raw_tail_base], [raw_tail_column], [raw_tail_columns]).
    - O    : the raw pass with k = 6 overflows into the cycler window
             ([overflow_base], [overflow_column], [overflow_columns]).
    - C    : the 919-step, 3-cell translated cycler ([cycler_step],
             [cycler_nonhalt]); with O: [exit_nonhalt].
    - E'/E'': the nested exception launched by a trigger hash inside an
             ordinary exception's call phase ([nested_pre_left],
             [launch_far], [relaunches_far], [nested_launch]), its counter
             run to the all-B word ([nested_counter]), and the whole exit
             from exception 9's decode trigger ([nested_exit]). *)

From BusyCoq Require Import Individual62 Longitudinal.
From W61 Require Import SOBCv10.
Require Import ZifyNat Lia Arith List.
Import ListNotations.
Local Open Scope list.
Local Open Scope nat_scope.
Local Open Scope sym.

Ltac run_c steps :=
  unfold tm; eapply multistep_progress with (n := steps);
  apply multistep_c_spec; vm_compute; reflexivity.

(** * 1. Law T2: the raw pass with a tail *)

(** The tail digit after a raw pass with tail index [k]: level [k - 1]. *)
Definition y_after (k : nat) : list Sym :=
  match k with
  | 0%nat => A8
  | 1%nat => B8
  | 2%nat => E8 ++ [1;1]
  | 3%nat => D8 ++ [1;1]
  | 4%nat => A8 ++ [1;1]
  | _ => B8 ++ [1;1]
  end.

(** The tail at level 4 ([B t]) behind [2k+1] separators. *)
Definition tail_word (k : nat) : list Sym := U^^(2*k+1) ++ B8 ++ [1;1].

Lemma raw_tail_base k l : k <= 5 ->
  l {{{((B, []), R)}}} ((B8 ++ U^^(2*k+1) ++ B8 ++ [1;1]) *> 0inf)
    -[tm]->+
  ([1;0;1] *> l) {{{((F, []), L)}}} ((U^^(2*k+3) ++ y_after k) *> 0inf).
Proof.
  intro Hk.
  destruct k as [|[|[|[|[|[|k]]]]]];
    [run_c 97|run_c 199|run_c 343|run_c 501|run_c 695|run_c 909|lia].
Qed.

Lemma raw_tail_column k e l : k <= 5 ->
  l {{{((B, []), R)}}} ((B8^^S e ++ tail_word k) *> 0inf)
    -[tm]->+
  ([1;0;1] *> l) {{{((F, []), L)}}}
    ((E8^^e ++ U^^(2*k+3) ++ y_after k) *> 0inf).
Proof.
  intro Hk.
  induction e as [|e IH] in l |- *.
  - exact (raw_tail_base k l Hk).
  - eapply evstep_progress_trans.
    + applys_eq (raw_B_forward l ((B8^^(S e) ++ tail_word k) *> 0inf)).
    + eapply progress_trans.
      * applys_eq (IH (Q8 *> l)).
      * applys_eq (raw_B_return l
          ((E8^^e ++ U^^(2*k+3) ++ y_after k) *> 0inf)).
Qed.

(** Column layouts: columns [es] (column [i] is [B^(S e_i)]), then a last
    column [B^(S e)], then the tail. *)
Definition full_tail (es : list nat) (e k : nat) : list Sym :=
  spaced_words (map (fun e => B8^^S e) es ++ [B8^^S e]) ++ tail_word k.

(** After the raw pass: every column but the last is [E^e A]; the last
    column has lost its top digit ([E^e]); the U run has grown by a pair. *)
Definition mixed_tail (es : list nat) (e k : nat) : list Sym :=
  spaced_words (map (fun e => E8^^e ++ A8) es ++ [E8^^e]) ++
    U^^(2*k+3) ++ y_after k.

Lemma spaced_snoc_cons (w : list Sym) ws x :
  spaced_words ((w :: ws) ++ [x]) = w ++ U^^2 ++ spaced_words (ws ++ [x]).
Proof.
  destruct ws; reflexivity.
Qed.

Theorem raw_tail_columns es e k l : k <= 5 ->
  l {{{((B, []), R)}}} (full_tail es e k *> 0inf)
    -[tm]->+
  ([1;0;1] *> l) {{{((F, []), L)}}} (mixed_tail es e k *> 0inf).
Proof.
  intro Hk.
  induction es as [|e0 es IH] in l |- *.
  - exact (raw_tail_column k e l Hk).
  - unfold full_tail, mixed_tail. cbn [map].
    rewrite !spaced_snoc_cons.
    eapply evstep_progress_trans.
    + applys_eq (raw_Bs_to_Qs (S e0) l
        ((U^^2 ++ full_tail es e k) *> 0inf));
        unfold full_tail; repeat rewrite Str_app_assoc; reflexivity.
    + eapply evstep_progress_trans.
      * applys_eq (raw_Us_to_Xs 2 (Q8^^(S e0) *> l)
          (full_tail es e k *> 0inf)).
      * eapply progress_trans.
        -- exact (IH (X4^^2 *> Q8^^(S e0) *> l)).
        -- eapply progress_evstep_trans.
           ++ applys_eq (raw_separator_return (Q8^^e0 *> l)
                (mixed_tail es e k *> 0inf)).
           ++ applys_eq (raw_B_returns e0 l
                ((A8 ++ U^^2 ++ mixed_tail es e k) *> 0inf));
                unfold mixed_tail; repeat rewrite Str_app_assoc;
                reflexivity.
Qed.

(** * 2. Lemma O (overflow) and Lemma C (translated cycler) *)

(** The cycler window, in tape order (left to right). *)
Definition Yw : list Sym :=
  [1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;
   1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;0;1;0;0;1;0;1;0;0;1;0;0].

(** C: every 919 steps the head moves 3 cells right; [L] is never read. *)
Lemma cycler_step L :
  (rev Yw *> L) {{B}}> 0inf -[tm]->+ (rev Yw *> [0;0;1] *> L) {{B}}> 0inf.
Proof.
  run_c 918.
Qed.

Theorem cycler_nonhalt L : ~ halts tm ((rev Yw *> L) {{B}}> 0inf).
Proof.
  apply progress_nonhalt_simple with
    (C := fun L => (rev Yw *> L) {{B}}> 0inf) (i0 := L).
  intro L'. exists ([0;0;1] *> L'). apply cycler_step.
Qed.

(** O, base: from the last remaining [B] of the last column, the k = 6 raw
    pass never comes back; 1208 steps, the left side is never read. *)
Lemma overflow_base l :
  l {{{((B, []), R)}}} ((B8 ++ tail_word 6) *> 0inf)
    -[tm]->+
  (rev Yw *> [0;1;0;1] *> l) {{B}}> 0inf.
Proof.
  run_c 1207.
Qed.

Lemma overflow_column e l : exists l',
  l {{{((B, []), R)}}} ((B8^^S e ++ tail_word 6) *> 0inf)
    -[tm]->+ (rev Yw *> l') {{B}}> 0inf.
Proof.
  induction e as [|e IH] in l |- *.
  - exists ([0;1;0;1] *> l). exact (overflow_base l).
  - destruct (IH (Q8 *> l)) as [l' H]. exists l'.
    eapply evstep_progress_trans; [|exact H].
    applys_eq (raw_B_forward l ((B8^^(S e) ++ tail_word 6) *> 0inf)).
Qed.

Theorem overflow_columns es e l : exists l',
  l {{{((B, []), R)}}} (full_tail es e 6 *> 0inf)
    -[tm]->+ (rev Yw *> l') {{B}}> 0inf.
Proof.
  induction es as [|e0 es IH] in l |- *.
  - exact (overflow_column e l).
  - destruct (IH (X4^^2 *> Q8^^(S e0) *> l)) as [l' H]. exists l'.
    unfold full_tail in *. cbn [map]. rewrite spaced_snoc_cons.
    eapply evstep_progress_trans.
    + applys_eq (raw_Bs_to_Qs (S e0) l
        ((U^^2 ++ full_tail es e 6) *> 0inf));
        unfold full_tail; repeat rewrite Str_app_assoc; reflexivity.
    + eapply evstep_progress_trans; [|exact H].
      applys_eq (raw_Us_to_Xs 2 (Q8^^(S e0) *> l)
        (full_tail es e 6 *> 0inf)).
Qed.

(** O + C: a hash that walks right into an all-B layout whose tail is
    [U^13 B t] (k = 6) starts the cycler, whatever lies to its left. *)
Theorem exit_nonhalt es e l :
  ~ halts tm (l {{{((B, []), R)}}} (full_tail es e 6 *> 0inf)).
Proof.
  destruct (overflow_columns es e l) as [l' H].
  intro Hh. apply (cycler_nonhalt l').
  exact (proj1 (halts_evstep_iff tm _ _ (progress_evstep _ _ _ H)) Hh).
Qed.

(** * 3. The nested exceptions E' and E'' *)

(** SOBCv10's exception left sides with an arbitrary far end. *)
Definition pre_left_far (n : nat) (far : side) : side :=
  ([1;0;1;0] ++ V4^^(2*n+2)) *> far.
Definition call_left_far (remaining finished : nat) (far : side) : side :=
  (X4^^(2*finished+5) ++ V4^^(2*remaining)) *> far.

Lemma pre_rotate_list m :
  [1;0;1] ++ X4^^(S m) = [1;0;1;0] ++ V4^^m ++ [0;1;0].
Proof.
  induction m as [|m IH].
  - reflexivity.
  - replace (X4^^(S (S m))) with (X4^^(S m) ++ X4)
      by (rewrite lpow_shift; reflexivity).
    rewrite app_assoc, IH.
    replace (V4^^(S m)) with (V4^^m ++ V4)
      by (rewrite lpow_shift; reflexivity).
    repeat rewrite <- app_assoc. reflexivity.
Qed.

(** The raw return of a trigger hash puts [101] in front of the finished
    calls; that is an exception pre-state whose far end holds the outer
    exception's pending calls. *)
Lemma nested_pre_left c f :
  [1;0;1] *> exception_call_left c f =
  pre_left_far (S f) ([0;1;0] *> V4^^(2*c) *> [1;0;1] *> 0inf).
Proof.
  unfold exception_call_left, pre_left_far.
  rewrite <- !Str_app_assoc. f_equal.
  repeat rewrite <- app_assoc.
  replace (2*f+5) with (S (2*f+4)) by lia.
  replace (2 * S f + 2) with (2*f+4) by lia.
  rewrite app_assoc, pre_rotate_list.
  repeat rewrite <- app_assoc. reflexivity.
Qed.

Lemma launch_far k far :
  sideRLs (flip tm) [left_hash] (pre_left_far (S k) far) (call_left_far k 0 far).
Proof.
  unfold pre_left_far, call_left_far.
  replace (2*S k+2) with (4+2*k) by lia; rewrite lpow_add.
  cbn [Nat.mul Nat.add].
  applys_eq (segRLs_sideRLs_concat left_launch_segment
    (sideRLseq_O (flip tm) (V4^^(2*k) *> far)));
    repeat rewrite Str_app_assoc; reflexivity.
Qed.

Lemma relaunch_far remaining finished far :
  sideRLs (flip tm) [left_hash]
    (call_left_far (S remaining) finished far)
    (call_left_far remaining (S finished) far).
Proof.
  pose proof (segRLs_concat
    (left_hash_X_pairs finished) left_relaunch_base) as Hseg.
  unfold call_left_far.
  replace (2*S remaining) with (2+2*remaining) by lia.
  replace (2*S finished+5) with (2*finished+7) by lia.
  repeat rewrite Str_app_assoc.
  rewrite <- (lpow_add' X4 (2*finished) 5).
  rewrite <- (lpow_add' X4 (2*finished) 7).
  rewrite <- (lpow_add' V4 2 (2*remaining)).
  applys_eq (segRLs_sideRLs_concat Hseg
    (sideRLseq_O (flip tm) (V4^^(2*remaining) *> far)));
    repeat rewrite Str_app_assoc; reflexivity.
Qed.

Lemma relaunches_far k r finished far :
  sideRLs (flip tm) ([left_hash]^^k)
    (call_left_far (k + r) finished far)
    (call_left_far r (finished + k) far).
Proof.
  induction k as [|k IH] in finished |- *.
  - cbn [lpow Nat.add]. replace (finished + 0) with finished by lia.
    constructor.
  - cbn [lpow]; eapply sideRLs_trans.
    + apply relaunch_far.
    + applys_eq (IH (S finished)); flia.
Qed.

(** The nested launch: from the nested pre-state, [h] calls run through the
    counter; the next call leaves with [r] calls still pending. *)
Theorem nested_launch h r far inp out :
  segRLs tm (hashes^^h) [] inp out ->
  pre_left_far (S (h + r)) far {{{((F, []), L)}}} (inp *> 0inf)
    -[tm]->+
  call_left_far r h far {{{((B, []), R)}}} (out *> 0inf).
Proof.
  intro Hseg.
  eapply progress_evstep_trans.
  - exact (sideRLs_1L _ _ _ _ _ (launch_far (h + r) far) (inp *> 0inf)).
  - pose proof (segRLs_0inf Hseg) as Hright.
    pose proof (relaunches_far h r 0 far) as Hleft.
    cbn [Nat.add] in Hleft.
    exact (sideRLs_concat_1 Hright Hleft).
Qed.

(** E''s counter, from the raw-pass word to the all-B word. *)
Lemma E_to_B m : segRLs tm (hashes^^(3*(2^m-1))) [] (E8^^m) (B8^^m).
Proof.
  induction m as [|m IH].
  - rewrite Nat.pow_0_r. cbn [Nat.sub Nat.mul Nat.add lpow]. constructor.
  - applys_eq (segRLs_concat (hash_E_odd (3*(2^m-1))) IH).
    f_equal. rewrite Nat.pow_succ_r'.
    generalize (Nat.pow_nonzero 2 m ltac:(lia)). lia.
Qed.

Lemma digits_word_repeat_BB n : digits_word (repeat BB n) = B8^^n.
Proof.
  induction n as [|n IH]; [reflexivity|].
  cbn [repeat digits_word digit_word lpow]. rewrite IH. reflexivity.
Qed.

Lemma digits_value_repeat_BB n : digits_value (repeat BB n) = 2^n - 1.
Proof.
  induction n as [|n IH]; [reflexivity|].
  cbn [repeat digits_value]. rewrite IH, Nat.pow_succ_r'.
  generalize (Nat.pow_nonzero 2 n ltac:(lia)); lia.
Qed.

(** Calls that take [mixed] columns [es] and a last column [E^(S e)] to the
    all-B layout, with no carry into the tail. *)
Fixpoint nested_required (es : list nat) (e : nat) : nat :=
  match es with
  | [] => 3*(2^(S e)-1)
  | e0 :: es' =>
      (nested_required es' e + 1) * 2^(S e0) - 2 + (2^(S e0) - 1)
  end.

Lemma nested_counter es e :
  segRLs tm (hashes^^nested_required es e) []
    (spaced_words (map (fun e => E8^^e ++ A8) es ++ [E8^^S e]))
    (spaced_words (map (fun e => B8^^S e) es ++ [B8^^S e])).
Proof.
  induction es as [|e0 es IH].
  - exact (E_to_B (S e)).
  - cbn [map nested_required]. rewrite !spaced_snoc_cons.
    pose proof (standard_mixed_to_binary_out_spec e0 (repeat BB (S e0))
      (nested_required es e) (repeat_length _ _)) as H0.
    rewrite digits_word_repeat_BB, digits_value_repeat_BB in H0.
    exact (segRLs_concat H0
      (segRLs_concat (hashes_U_run (nested_required es e) 2) IH)).
Qed.

(** The exit, from the configuration in which exception 9's trigger hash
    leaves its call region: [c] calls pending, [f] finished, the counter all
    B with layout [es ++ [S (S e)]] and the tail [U^11 B t] (k = 5).
    The trigger's raw pass (T2, k = 5) starts E' with [S f] calls; E'' fires
    after [nested_required es e] of them, and its raw pass overflows (O)
    into the cycler (C). *)
Theorem nested_exit c f es e :
  nested_required es e <= f ->
  ~ halts tm (exception_call_left c f {{{((B, []), R)}}}
    (full_tail es (S e) 5 *> 0inf)).
Proof.
  intros Hle Hh.
  set (h := nested_required es e) in *.
  set (far := [0;1;0] *> V4^^(2*c) *> [1;0;1] *> 0inf).
  pose proof (raw_tail_columns es (S e) 5 (exception_call_left c f)
    ltac:(lia)) as Hraw.
  rewrite nested_pre_left in Hraw. fold far in Hraw.
  pose proof (segRLs_concat (nested_counter es e) (segRLs_O tm (tail_word 6)))
    as Hseg.
  pose proof (nested_launch h (f - h) far _ _ Hseg) as Hlaunch.
  replace (S (h + (f - h))) with (S f) in Hlaunch by lia.
  destruct (overflow_columns es e (call_left_far (f - h) h far))
    as [l' Hover].
  apply (cycler_nonhalt l').
  refine (proj1 (halts_evstep_iff tm _ _ _) Hh).
  apply progress_evstep.
  eapply progress_trans; [exact Hraw|].
  eapply progress_trans; [exact Hlaunch|].
  exact Hover.
Qed.

Print Assumptions nested_exit.
Print Assumptions exit_nonhalt.