(** W6-1 PLANNING FILE.  Statements only: every [Admitted] below is open work.
    Nothing in this file counts as proved except the plumbing that composes the
    statements ([sobc_D_nonhalt], [nonhalt]); [Print Assumptions nonhalt] at
    the end lists exactly the open statements.

    Frame: SOBCv10's table and frame (W61.SOBCv10, an unmodified copy of the
    upstream file).  Our machine is that table mirrored and renamed and started
    in SOBCv10's state D ([perm], [nonhalt] at the end).

    Open statements:
    - [opening]          blank tape (state D) to the entry post-C/A state:
                         exceptions 1-5 and families (a)-(d) at m = 30, p = n4;
    - [entry_pre]        the round precondition at the entry (concrete numbers);
    - [tail_round]       THE tail-aware round lemma (one round, no trigger),
                         used three times (exceptions 6, 7, 8);
    - [tail_round_trigger] the same round when the decode triggers
                         (exception 9), ending where [nested_exit] starts. *)

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

(** * 1. The tail-aware post-C/A state *)

(** Digits of the last column: SOBCv10's [A]/[B] plus the deficit (pre-state)
    digits [D] (-1) and [E] (-2) that a short decode leaves behind (law T3). *)
Inductive SDigit := SE | SD | SA | SB.
Definition sdigit_word (d : SDigit) : list Sym :=
  match d with SE => E8 | SD => D8 | SA => A8 | SB => B8 end.
Definition sdigit_value (d : SDigit) : Z :=
  match d with SE => (-2)%Z | SD => (-1)%Z | SA => 0%Z | SB => 1%Z end.
Fixpoint sdigits_word (ds : list SDigit) : list Sym :=
  match ds with [] => [] | d :: ds' => sdigit_word d ++ sdigits_word ds' end.
Fixpoint sdigits_value (ds : list SDigit) : Z :=
  match ds with
  | [] => 0%Z
  | d :: ds' => (sdigit_value d + 2 * sdigits_value ds')%Z
  end.
Definition sdigit_of (d : BDigit) : SDigit := match d with BA => SA | BB => SB end.

(** The counter after C/A: primary [A^primary], the z-columns [zs] (SOBCv10
    binary columns), the last column [last], then the tail [U^(2k+1) y] with
    [y = y_after lv]: tail value [lv] (= level + 1), i.e.
    [A], [B], [E t], [D t], [A t], [B t] for [lv] = 0..5. *)
Definition tail_layout (primary : nat) (zs : list BinaryColumn)
    (last : list SDigit) (k lv : nat) : list Sym :=
  A8^^primary ++ U^^2 ++
  spaced_words (map binary_column_word zs ++ [sdigits_word last]) ++
  U^^(2*k+1) ++ y_after lv.

Definition post_ca_tail (unary primary : nat) (zs : list BinaryColumn)
    (last : list SDigit) (k lv : nat) : Q * tape :=
  ordinary_left unary {{{((B, []), R)}}} (tail_layout primary zs last k lv *> 0inf).

(** * 2. The round parameters with a tail (laws T1 and T3) *)

Fixpoint zs_value (o : nat) (zs : list BinaryColumn) : Z :=
  match zs with
  | [] => 0%Z
  | c :: zs' => (2^Z.of_nat o * Z.of_nat (column_value c) +
                 zs_value (o + column_width c) zs')%Z
  end.

(** W: digits before the tail.  V: the counter value, tail level at 2^W. *)
Definition tail_W (primary : nat) zs (last : list SDigit) : nat :=
  primary + columns_width_sum zs + length last.
Definition tail_V (primary : nat) zs last (lv : nat) : Z :=
  (zs_value primary zs +
   2^Z.of_nat (primary + columns_width_sum zs) * sdigits_value last +
   2^Z.of_nat (tail_W primary zs last) * (Z.of_nat lv - 1))%Z.

(** T1: the hash that finds every digit [B] and the tail at [B t]. *)
Definition trigger_hash primary zs last lv : Z :=
  (5 * 2^Z.of_nat (tail_W primary zs last) - tail_V primary zs last lv)%Z.

(** The exception's n: the tally after the trigger hash is [2n+1]. *)
Definition tail_next_half current previous zs last lv : Z :=
  ((Z.of_nat (round_post_unary current previous) +
    trigger_hash (round_primary_width current previous) zs last lv - 1) / 2)%Z.
Definition tail_next_index current previous zs last lv : nat :=
  Z.to_nat ((tail_next_half current previous zs last lv - 6) / 2).

(** Effective tail level: the level minus the deficit left in the last column. *)
Definition eff_level (last : list SDigit) (lv : nat) : Z :=
  ((sdigits_value last + 2^Z.of_nat (length last) * (Z.of_nat lv - 1)) /
     2^Z.of_nat (length last))%Z.

(** The decode of the next exception reaches [B t] with a carry left over. *)
Definition tail_triggers (k : nat) (last : list SDigit) (lv : nat) : Prop :=
  (Z.of_nat k - 1 + (2 - eff_level last lv) >= 5)%Z.

(** DRAFT precondition (to be fixed in the first proving stage).  It holds
    SOBCv10's column conditions for the z-columns, SOBCv10's width dominance
    for the whole layout, and the window that keeps the last column's decode
    below its top digit (T3).  Each field is a condition SOBCv10's own round
    proof uses or the tail laws need. *)
Record tail_round_pre (current previous : nat) (zs : list BinaryColumn)
    (last : list SDigit) (k lv : nat) : Prop := {
  tp_zs_safe : Forall column_safe zs;
  tp_head_odd : match zs with
                | c :: _ => Nat.odd (column_value c) = true
                | [] => Z.odd (sdigits_value last) = true
                end;
  tp_width :
    2 * (columns_width_sum zs + length last) + 4 <= half_parameter previous + 1 /\
    2 * (half_parameter previous + 1 + columns_width_sum zs + length last) + 4 <=
      half_parameter current + 1;
  tp_last_len : 2 <= length last;
  tp_last_window :
    (3 <= sdigits_value last + 2^Z.of_nat (length last) * 2)%Z /\
    (sdigits_value last <= 2^Z.of_nat (length last) - 6)%Z;
  tp_k : k <= 4;
  tp_lv : lv <= 5
}.

(** * 3. The tail-aware round lemma (open) *)

(** One SOBCv10 round with the tail carried along.  Compared with
    [sobc1_round_invariant_progress]:
    - the exception's n is [tail_next_half] (T1 + T3), not [round_next_half];
    - its raw pass is [raw_tail_columns] (T2): the last column loses its top
      digit and the U run grows by one pair ([k -> S k]);
    - the decode leaves the tail at effective level [k + 1 - L] (T3);
    - the z-columns are SOBCv10's ([columns_step]), with the new
      [z_column previous] in front, as in SOBCv10. *)
Theorem tail_round current previous zs last k lv :
  tail_round_pre current previous zs last k lv ->
  ~ tail_triggers k last lv ->
  exists zs' last' lv',
    post_ca_tail (round_post_unary current previous)
      (round_primary_width current previous) zs last k lv
    -[tm]->+
    post_ca_tail
      (round_post_unary (tail_next_index current previous zs last lv) current)
      (round_primary_width (tail_next_index current previous zs last lv) current)
      (z_column previous :: zs') last' (S k) lv' /\
    tail_round_pre (tail_next_index current previous zs last lv) current
      (z_column previous :: zs') last' (S k) lv' /\
    length last' = pred (length last) /\
    eff_level last' lv' = (Z.of_nat k + 1 - eff_level last lv)%Z.
Admitted.

(** The round in which the decode triggers (exception 9: k = 4): the run
    reaches the configuration of [nested_exit] (W61Exit), with E''s call
    count below E''s budget (h'' - 1 <= h_t - 1). *)
Theorem tail_round_trigger current previous zs last lv :
  tail_round_pre current previous zs last 4 lv ->
  tail_triggers 4 last lv ->
  exists c f es e,
    post_ca_tail (round_post_unary current previous)
      (round_primary_width current previous) zs last 4 lv
    -[tm]->+
    exception_call_left c f {{{((B, []), R)}}} (full_tail es (S e) 5 *> 0inf) /\
    nested_required es e <= f.
Admitted.

(** * 4. The entry and the opening (open) *)

Definition n4 : nat := 3 * 2^29 - 2.
Definition n5 : nat := 2^n4 - 2 + 2^(n4-2) * ((1292 * 2^30 + 4) / 3).
Definition entry_current : nat := (n5 - 6) / 2.
Definition entry_previous : nat := n4 / 2 - 3.
(** The entry column, least significant digit first: 29 digits, value
    391,468,375. *)
Definition entry_digits : list BDigit :=
  [BB;BB;BB;BA;BB;BA;BB;BA;BB;BA;BB;BA;BB;BA;BB;BA;BB;BA;BB;BA;
   BB;BA;BB;BA;BB;BB;BB;BA;BB].
Definition entry_last : list SDigit := map sdigit_of entry_digits.
Definition entry_state : Q * tape :=
  post_ca_tail (round_post_unary entry_current entry_previous)
    (round_primary_width entry_current entry_previous) [] entry_last 1 4.

Lemma entry_last_value : sdigits_value entry_last = 391468375%Z.
Proof. vm_compute. reflexivity. Qed.

Lemma entry_level : eff_level entry_last 4 = 3%Z.
Proof. vm_compute. reflexivity. Qed.

(** Exceptions 1-5 from the blank tape in SOBCv10's state D (families (a)-(d)
    of proof.md section 2), ending in [exception_done_ca]. *)
Lemma opening : (D;; tape0) -[tm]->* entry_state.
Admitted.

Lemma entry_pre : tail_round_pre entry_current entry_previous [] entry_last 1 4.
Admitted.

(** * 5. Composition (proved from the open statements) *)

Lemma halts_back c c' : c -[tm]->+ c' -> halts tm c -> halts tm c'.
Proof.
  intros Hrun Hh. exact (proj1 (halts_evstep_iff tm _ _ (progress_evstep _ _ _ Hrun)) Hh).
Qed.

Theorem sobc_D_nonhalt : ~ halts tm (D;; tape0).
Proof.
  intro H.
  apply (proj1 (halts_evstep_iff tm _ _ opening)) in H.
  unfold entry_state in H.
  (* exception 6: k = 1, L = 3 *)
  assert (T1 : ~ tail_triggers 1 entry_last 4)
    by (unfold tail_triggers; rewrite entry_level; lia).
  destruct (tail_round _ _ _ _ _ _ entry_pre T1) as
    [zs1 [last1 [lv1 [R1 [P1 [_ L1]]]]]].
  apply (halts_back _ _ R1) in H.
  (* exception 7: k = 2, L = -1 *)
  assert (T2 : ~ tail_triggers 2 last1 lv1)
    by (unfold tail_triggers; rewrite L1, entry_level; lia).
  destruct (tail_round _ _ _ _ _ _ P1 T2) as
    [zs2 [last2 [lv2 [R2 [P2 [_ L2]]]]]].
  apply (halts_back _ _ R2) in H.
  (* exception 8: k = 3, L = 4 *)
  assert (T3 : ~ tail_triggers 3 last2 lv2)
    by (unfold tail_triggers; rewrite L2, L1, entry_level; lia).
  destruct (tail_round _ _ _ _ _ _ P2 T3) as
    [zs3 [last3 [lv3 [R3 [P3 [_ L3]]]]]].
  apply (halts_back _ _ R3) in H.
  (* exception 9: k = 4, L = 0: the decode triggers *)
  assert (T4 : tail_triggers 4 last3 lv3)
    by (unfold tail_triggers; rewrite L3, L2, L1, entry_level; lia).
  destruct (tail_round_trigger _ _ _ _ _ P3 T4) as [c [f [es [e [R4 Hle]]]]].
  apply (halts_back _ _ R4) in H.
  exact (nested_exit c f es e Hle H).
Qed.

(** * 6. Our machine *)

Definition tm61 := Eval compute in
  (TM_from_str "1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF").

(** phi maps our states to SOBCv10's; with the mirror, our blank-tape run is
    SOBCv10's run from state D. *)
Definition phi (q : Q) : Q :=
  match q with
  | A => D | B => E | C => F | D => A | E => B | F => C
  end.

Lemma perm : Perm (flip tm61) tm phi.
Proof.
  split.
  - intros [] [] H; cbn in *; try discriminate; reflexivity.
  - intros [] [] s' d q' H; cbn in *; inversion H; subst; reflexivity.
Qed.

Lemma nonhalt : ~ halts tm61 c0.
Proof.
  intros H.
  apply flip_halts in H.
  change (halts (flip tm61) (A;; tape0)) in H.
  exact (sobc_D_nonhalt (perm_halts _ _ _ _ _ perm H)).
Qed.

Print Assumptions nonhalt.