/machines/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---/rocq/main.v · raw
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
Require Import ssim chain count right regroup step step2.
From BusyCoq Require Import Individual62.
Require Import Lia ZifyNat List Arith NArith ZArith.
Import ListNotations.
Open Scope nat_scope.

(* ===================================================================== *)
(* The invariant at the start of every record interval, and its closure. *)
(* ===================================================================== *)

Inductive cls := C5 | C0 | C1 | C2 | C3 | C4.

Definition Rs (r : cls) : list run :=
  match r with C5 => Rs_r5 | C0 => Rs_r0 | C1 => Rs_r1 | C2 => Rs_r2 | C3 => Rs_r3 | C4 => Rs_r4 end.

Definition ist : Type := (cls * nat * N * list (list N))%type.

Definition cfgI (s : ist) : Q * tape :=
  let '(r, e, t, nus) := s in Gc (repeat U0 (length nus), P0, 0) nus (evR [t] (Rs r)).

Definition win (r : cls) (e : nat) (t : N) (nus : list (list N)) : Prop :=
  match r with
  | C5 => exists f1 deep, nus = [W5t t; W5s t; W5a t; f1] :: deep /\ length deep = 1 + 2 * e
  | C0 => exists f1 f2 deep, nus = [W0t t; W0s t; f1; f2] :: deep /\ length deep = 1 + 2 * e
  | C1 => exists f1 f2 f3 deep, nus = [W1t t; W1s t; W1a t; W1I t] :: [W1u t; f1; f2; f3] :: deep /\
            length deep = 1 + 2 * e
  | C2 => exists q deep, nus = q :: deep /\ length deep = 1 + 2 * e
  | C3 => exists f1 f2 f3 deep, nus = [W3t t; f1; f2; f3] :: deep /\ length deep = 2 + 2 * e
  | C4 => exists q deep, nus = q :: deep /\ length deep = 2 + 2 * e
  end.

Definition Inv (s : ist) : Prop :=
  let '(r, e, t, nus) := s in 2 <= e /\ 1 + 8 * N.to_nat t = 9 ^ (e - 2) /\ win r e t nus.

Lemma inv_step s : Inv s -> exists s', cfgI s -->+ cfgI s' /\ Inv s'.
Proof.
  destruct s as [[[r e] t] nus]. intros [He [Ht Hw]].
  destruct r; cbn [win] in Hw.
  - destruct Hw as [f1 [deep [-> Hl]]].
    exists (C0, e, t, [W5s t; W5a t; f1; rtop deep 0%N] :: rshift deep 0%N). split.
    + cbn [cfgI length Rs]. rewrite shift_len. apply (S_r5 e); assumption.
    + cbn [Inv win]. split; [exact He|]. split; [exact Ht|].
      exists f1, (rtop deep 0%N), (rshift deep 0%N). split; [reflexivity|]. rewrite shift_len. exact Hl.
  - destruct Hw as [f1 [f2 [deep [-> Hl]]]].
    exists (C1, e, t, [W1t t; W1s t; W1a t; W1I t] :: [W0s t; f1; f2; rtop deep 0%N] :: rshift deep 0%N). split.
    + cbn [cfgI length Rs]. rewrite shift_len. apply (S_r0 e); assumption.
    + cbn [Inv win]. split; [exact He|]. split; [exact Ht|].
      exists f1, f2, (rtop deep 0%N), (rshift deep 0%N). split; [reflexivity|]. rewrite shift_len. exact Hl.
  - destruct Hw as [f1 [f2 [f3 [deep [-> Hl]]]]].
    exists (C2, e, t, [f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N). split.
    + cbn [cfgI length Rs]. rewrite shift_len. apply (S_r1 e); assumption.
    + cbn [Inv win]. split; [exact He|]. split; [exact Ht|].
      exists [f1; f2; f3; rtop deep 0%N], (rshift deep 0%N). split; [reflexivity|]. rewrite shift_len. exact Hl.
  - destruct Hw as [q [deep [-> Hl]]].
    exists (C3, e, t, [W3t t; wv 6227 49896 t; wv 2069 16632 t; nth 0 q 0%N] :: rshift (q :: deep) 0%N). split.
    + cbn [cfgI length Rs]. rewrite shift_len. cbn [length]. apply (S_r2 e); assumption.
    + cbn [Inv win]. split; [exact He|]. split; [exact Ht|].
      exists (wv 6227 49896 t), (wv 2069 16632 t), (nth 0 q 0%N), (rshift (q :: deep) 0%N). split; [reflexivity|].
      rewrite shift_len. cbn [length]. lia.
  - destruct Hw as [f1 [f2 [f3 [deep [-> Hl]]]]].
    exists (C4, e, t, [f1; f2; f3; rtop deep 0%N] :: rshift deep 0%N). split.
    + cbn [cfgI length Rs]. rewrite shift_len. apply (S_r3 e); assumption.
    + cbn [Inv win]. split; [exact He|]. split; [exact Ht|].
      exists [f1; f2; f3; rtop deep 0%N], (rshift deep 0%N). split; [reflexivity|]. rewrite shift_len. exact Hl.
  - destruct Hw as [q [deep [-> Hl]]].
    exists (C5, S e, (1 + 9 * t)%N, [W5t (1 + 9 * t); W5s (1 + 9 * t); W5a (1 + 9 * t); nth 0 q 0%N] :: rshift (q :: deep) 0%N).
    split.
    + cbn [cfgI length Rs]. rewrite shift_len. cbn [length]. apply (S_r4 e); assumption.
    + cbn [Inv win]. split; [lia|]. split.
      * replace (S e - 2) with (S (e - 2)) by lia. cbn [Nat.pow]. rewrite <-Ht. lia.
      * exists (nth 0 q 0%N), (rshift (q :: deep) 0%N). split; [reflexivity|]. rewrite shift_len. cbn [length]. lia.
Qed.

(* ===================================================================== *)
(* From record exit 28 to the invariant (class r5, e = 2, u = 1).        *)
(* ===================================================================== *)

Definition L28 : list run :=
  [(S0, cn 74808); (S1, cn 24912); (S0, cn 8277); (S0, cn 2737); (S0, cn 972); (S1, cn 36);
   (S0, cn 37); (S0, cn 37); (S0, cn 44); (S1, cn 24); (S0, cn 13); (S0, cn 9);
   (S0, cn 4); (S1, cn 4); (S0, cn 1); (S0, cn 5); (S0, cn 4); (S1, cn 4); (S0, cn 1); (S0, cn 5);
   (S0, cn 4); (S1, cn 4); (S0, cn 1); (S0, cn 5); (S0, cn 1); (S0, cn 6); (S1, cn 4); (S0, cn 1);
   (S0, cn 5); (S0, cn 1); (S0, cn 5); (S0, cn 1); (S0, cn 5); (S0, cn 1); (S0, cn 5); (S0, cn 2)]%N.
Definition R28 : list run := [(S0, cn 224492); (S1, cn 673559); (S1, cn 7); (S1, cn 9841); (S1, cn 1942040); (S0, cn 2)]%N.

Definition nus28 : list (list N) :=
  [[18701; 6227; 2069; 683]; [242; 8; 9; 8]; [10; 5; 3; 1]; [0; 0; 0; 0]; [0; 0; 0; 0]; [0; 0; 0; 0]]%N.

Lemma inv28 : Inv (C5, 2, 0%N, nus28).
Proof.
  cbn [Inv win]. split; [lia|]. split; [reflexivity|].
  exists 683%N, (tl nus28). split; reflexivity.
Qed.

Lemma split1 nu b c v rest X :
  ev_runs nu ((b, LF (3 + c) v) :: rest) X = ev_runs nu [(b, cn 3)] (ev_runs nu ((sneg b, LF c v) :: rest) X).
Proof.
  cbn [ev_runs]. unfold ev. cbn [lc lv].
  replace (N.to_nat (3 + c + dot v nu)) with (3 + N.to_nat (c + dot v nu)) by lia.
  rewrite alt_add, Str_app_assoc. reflexivity.
Qed.

Lemma b28a : reach 1000 (Rc B (L28, T0) ([(S1, cn 3)], TV 1)) (Rc A ((S0, cn 3) :: L28, T0) ([], TV 1)) = true.
Proof. vm_compute. reflexivity. Qed.

Lemma b28b : ep_run true R28 = Some (map (fun r => (fst r, cn (evN [0%N] (snd r)))) Rs_r5).
Proof. vm_compute. reflexivity. Qed.

Lemma b28_chain : ev_runs [] ((S0, cn 3) :: L28) (const S0) = chs (repeat U0 6) nus28 (b1s P0 (LWs 0)).
Proof. reflexivity. Qed.

Lemma b28_right : evR [] (map (fun r => (fst r, cn (evN [0%N] (snd r)))) Rs_r5) = evR [0%N] Rs_r5.
Proof. reflexivity. Qed.

Lemma base28 (sg : nat -> side) :
  ev_runs [] L28 (const S0) {{B}}> ev_runs [] ((S1, cn 224495) :: tl R28) (const S0) -->*
  cfgI (C5, 2, 0%N, nus28).
Proof.
  change (cn 224495) with (LF (3 + 224492) []).
  rewrite split1.
  eapply evstep_trans.
  - apply progress_evstep. exact (reach_spec _ _ _ b28a [] (sg2 (const S0) (evR [] R28))).
  - change (ev_runs [] ((S0, cn 3) :: L28) (const S0) {{A}}> evR [] R28 -->* cfgI (C5, 2, 0%N, nus28)).
    replace (cfgI (C5, 2, 0%N, nus28))
      with (ev_runs [] ((S0, cn 3) :: L28) (const S0) <{{D}} evR [] (map (fun r => (fst r, cn (evN [0%N] (snd r)))) Rs_r5)).
    + apply (ep_run_spec _ _ _ b28b []).
    + unfold cfgI, Gc. rewrite b28_chain, b28_right. reflexivity.
Qed.