Require Import ssim chain count.
From BusyCoq Require Import Individual62.
Require Import Lia ZifyNat List Arith NArith ZArith.
Import ListNotations.

Open Scope nat_scope.

(* ===================================================================== *)
(* The right region: a verified symbolic executor for interval programs. *)
(* ===================================================================== *)

(* run the simulator until it is stuck (or out of fuel) *)
Fixpoint urun (p : positive) (c : cfg) : cfg * bool :=
  match p with
  | xH => match sstep c with Some (c', _) => (c', false) | None => (c, true) end
  | xO p' => let '(c1, s1) := urun p' c in if s1 then (c1, true) else urun p' c1
  | xI p' =>
    match sstep c with
    | Some (c0, _) => let '(c1, s1) := urun p' c0 in if s1 then (c1, true) else urun p' c1
    | None => (c, true)
    end
  end.

Lemma sstep_ev nu sg c c' b : sstep c = Some (c', b) -> ev_cfg nu sg c -->* ev_cfg nu sg c'.
Proof.
  intros E. pose proof (sstep_spec nu sg _ _ _ E) as H. destruct b; cbn in H; [apply progress_evstep|]; exact H.
Qed.

Lemma urun_spec p : forall c nu sg, ev_cfg nu sg c -->* ev_cfg nu sg (fst (urun p c)).
Proof.
  induction p as [p IH|p IH|]; intros c nu sg; cbn [urun].
  - destruct (sstep c) as [[c0 b]|] eqn:E; [|apply evstep_refl].
    pose proof (sstep_ev nu sg _ _ _ E) as H0.
    pose proof (IH c0 nu sg) as H1. destruct (urun p c0) as [c1 s1]. cbn [fst] in H1.
    destruct s1; cbn [fst].
    + eapply evstep_trans; eassumption.
    + eapply evstep_trans; [eassumption|]. eapply evstep_trans; [exact H1|]. apply IH.
  - pose proof (IH c nu sg) as H1. destruct (urun p c) as [c1 s1]. cbn [fst] in H1.
    destruct s1; cbn [fst]; [exact H1|]. eapply evstep_trans; [exact H1|]. apply IH.
  - destruct (sstep c) as [[c0 b]|] eqn:E; cbn [fst]; [|apply evstep_refl].
    exact (sstep_ev nu sg _ _ _ E).
Qed.

Definition tgtD (c : cfg) : option (list run) :=
  match c with
  | Lc D ([], TV O) (rr, T0) => Some rr
  | _ => None
  end.

Lemma tgtD_spec c rr : tgtD c = Some rr -> c = Lc D ([], TV 0) (rr, T0).
Proof.
  unfold tgtD. destruct c as [q l r|q [l t] [r t']]; [discriminate|].
  destruct q; try discriminate. destruct l; try discriminate.
  destruct t as [|[|k]]; try discriminate. destruct t'; try discriminate.
  intros H; inversion H; subst; reflexivity.
Qed.

Definition evR (nu : list N) (rr : list run) : side := ev_runs nu rr (const S0).

(* one episode of the right region, entered at phase p, the chain side abstract *)
Definition ep_run (p : bool) (rr : list run) : option (list run) :=
  tgtD (fst (urun 50000 (Rc (stp p) ([], TV 0) (rr, T0)))).

Lemma ep_run_spec p rr rr' : ep_run p rr = Some rr' -> forall nu, Ep p (evR nu rr) (evR nu rr').
Proof.
  unfold ep_run. intros H nu l.
  pose proof (urun_spec 50000 (Rc (stp p) ([], TV 0) (rr, T0)) nu (fun _ => l)) as U.
  destruct (urun 50000 (Rc (stp p) ([], TV 0) (rr, T0))) as [c s]. cbn [fst] in H, U.
  apply tgtD_spec in H. subst c. exact U.
Qed.

Fixpoint eps (ps : list bool) (rr : list run) : option (list run) :=
  match ps with
  | [] => Some rr
  | p :: ps' => match ep_run p rr with Some rr' => eps ps' rr' | None => None end
  end.

Lemma eps_spec ps : forall rr rr', eps ps rr = Some rr' -> forall nu, EpSeq ps (evR nu rr) (evR nu rr').
Proof.
  induction ps as [|p ps IH]; intros rr rr' H nu; cbn in H.
  - inversion H; reflexivity.
  - destruct (ep_run p rr) as [r1|] eqn:E; [|discriminate].
    exists (evR nu r1). split; [apply (ep_run_spec _ _ _ E) | apply (IH _ _ H)].
Qed.

Lemma EpSeq_app a : forall b R R1 R2, EpSeq a R R1 -> EpSeq b R1 R2 -> EpSeq (a ++ b) R R2.
Proof.
  induction a as [|p a IH]; intros b R R1 R2 H1 H2; cbn in *.
  - subst. exact H2.
  - destruct H1 as [R3 [H3 H4]]. exists R3. split; [exact H3 | apply (IH _ _ _ _ H4 H2)].
Qed.

(* ---- linear-form algebra ---- *)

Definition evN (nu : list N) (a : lf) : N := (lc a + dot (lv a) nu)%N.

Lemma dot_zadd2 v : forall a b, dot v (zadd a b) = (dot v a + dot v b)%N.
Proof.
  induction v as [|x v IH]; intros [|y a] [|z b]; cbn; try lia.
  rewrite IH. lia.
Qed.

Definition vscale (k : N) (w : list N) : list N := map (N.mul k) w.

Lemma dot_vscale v : forall k w, dot v (vscale k w) = (k * dot v w)%N.
Proof. unfold vscale. induction v as [|x v IH]; intros k [|y w]; cbn; try lia. rewrite IH. lia. Qed.

Lemma ev_runs_dot nu nu' T X : (forall v, dot v nu = dot v nu') -> ev_runs nu T X = ev_runs nu' T X.
Proof.
  intros H. induction T as [|[b a] T IH]; cbn; [reflexivity|]. unfold ev. rewrite H, IH. reflexivity.
Qed.

Definition subst_lf (w : list N) (a : lf) : lf := LF (lc a + dot (lv a) w) (lv a).
Definition subst_runs (w : list N) (T : list run) : list run := map (fun r => (fst r, subst_lf w (snd r))) T.

Lemma ev_runs_subst nu w T X : ev_runs nu (subst_runs w T) X = ev_runs (zadd nu w) T X.
Proof.
  unfold subst_runs. induction T as [|[b a] T IH]; cbn; [reflexivity|]. rewrite IH. unfold ev, subst_lf. cbn.
  rewrite dot_zadd2. f_equal. f_equal. lia.
Qed.

Definition lf_scale (k : N) (a : lf) : lf := LF (k * lc a) (map (N.mul k) (lv a)).

Lemma dot_scale_l vs : forall k nu, dot (map (N.mul k) vs) nu = (k * dot vs nu)%N.
Proof. induction vs as [|x vs IH]; intros k [|y nu]; cbn; try lia. rewrite IH. lia. Qed.

Lemma evN_add nu a b : evN nu (lf_add a b) = (evN nu a + evN nu b)%N.
Proof. unfold evN, lf_add. cbn. rewrite dot_zadd. lia. Qed.

Lemma evN_scale nu k a : evN nu (lf_scale k a) = (k * evN nu a)%N.
Proof. unfold evN, lf_scale. cbn. rewrite dot_scale_l. lia. Qed.

Fixpoint comp_aux (vs : list N) (sg : list lf) : lf :=
  match vs, sg with
  | v :: vs', s :: sg' => lf_add (lf_scale v s) (comp_aux vs' sg')
  | _, _ => LF 0 []
  end.
Definition compose_lf (sg : list lf) (a : lf) : lf := lf_add (LF (lc a) []) (comp_aux (lv a) sg).
Definition comp_runs (sg : list lf) (T : list run) : list run := map (fun r => (fst r, compose_lf sg (snd r))) T.

Lemma evN_comp_aux nu vs : forall sg, evN nu (comp_aux vs sg) = dot vs (map (evN nu) sg).
Proof.
  induction vs as [|v vs IH]; intros [|s sg]; cbn [comp_aux map dot]; try reflexivity.
  rewrite evN_add, evN_scale, IH. lia.
Qed.

Lemma evN_compose nu sg a : evN nu (compose_lf sg a) = evN (map (evN nu) sg) a.
Proof. unfold compose_lf. rewrite evN_add, evN_comp_aux. unfold evN at 1 3. cbn. lia. Qed.

Lemma ev_runs_comp nu sg T X : ev_runs nu (comp_runs sg T) X = ev_runs (map (evN nu) sg) T X.
Proof.
  unfold comp_runs. induction T as [|[b a] T IH]; cbn; [reflexivity|]. rewrite IH. unfold ev.
  change (lc (compose_lf sg a) + dot (lv (compose_lf sg a)) nu)%N with (evN nu (compose_lf sg a)).
  rewrite evN_compose. reflexivity.
Qed.

(* ---- the 4-cycle jump (Lemma J) ---- *)

Lemma jump_lemma T p dec inc :
  (forall nu, EpSeq [p; p; p; p] (evR nu (subst_runs dec T)) (evR nu (subst_runs inc T))) ->
  forall k nu, EpSeq (repeat p (4 * k)) (evR (zadd nu (vscale (N.of_nat k) dec)) T)
                                        (evR (zadd nu (vscale (N.of_nat k) inc)) T).
Proof.
  intros Hc k. induction k as [|k IH]; intros nu.
  - cbn [repeat Nat.mul EpSeq]. unfold evR. apply ev_runs_dot. intros v.
    rewrite !dot_zadd2, !dot_vscale. lia.
  - replace (4 * S k) with (4 + 4 * k) by lia. rewrite repeat_add.
    apply (EpSeq_app _ _ _ (evR (zadd (zadd nu inc) (vscale (N.of_nat k) dec)) T)).
    + specialize (Hc (zadd nu (vscale (N.of_nat k) dec))). unfold evR in *.
      rewrite !ev_runs_subst in Hc.
      replace (ev_runs (zadd nu (vscale (N.of_nat (S k)) dec)) T (const S0))
        with (ev_runs (zadd (zadd nu (vscale (N.of_nat k) dec)) dec) T (const S0))
        by (apply ev_runs_dot; intros v; rewrite !dot_zadd2, !dot_vscale; lia).
      replace (ev_runs (zadd (zadd nu inc) (vscale (N.of_nat k) dec)) T (const S0))
        with (ev_runs (zadd (zadd nu (vscale (N.of_nat k) dec)) inc) T (const S0))
        by (apply ev_runs_dot; intros v; rewrite !dot_zadd2; lia).
      exact Hc.
    + specialize (IH (zadd nu inc)). unfold evR in *.
      replace (ev_runs (zadd nu (vscale (N.of_nat (S k)) inc)) T (const S0))
        with (ev_runs (zadd (zadd nu inc) (vscale (N.of_nat k) inc)) T (const S0))
        by (apply ev_runs_dot; intros v; rewrite !dot_zadd2, !dot_vscale; lia).
      replace (ev_runs (zadd (zadd nu inc) (vscale (N.of_nat k) dec)) T (const S0))
        with (ev_runs (zadd (zadd nu inc) (vscale (N.of_nat k) dec)) T (const S0)) by reflexivity.
      exact IH.
Qed.

(* ---- building a jump from the actual configuration ---- *)

Definition uvar (i : nat) (c : N) : lf := LF c (repeat 0%N i ++ [4%N]).

Fixpoint zsub (a b : list N) : list N :=
  match a, b with
  | x :: a', y :: b' => (x - y)%N :: zsub a' b'
  | _, [] => a
  | [], _ => []
  end.

Fixpoint mk_jump (i : nat) (rr rr4 : list run) (c : lf) : option (list run * list N * list N * list lf) :=
  match rr, rr4 with
  | [], [] => Some ([], [], [], [])
  | (b, a) :: rr', (b4, a4) :: rr4' =>
    if negb (seqb b b4) then None else
    if negb (listN_eqb (strip0 (lv a)) (strip0 (lv a4))) then None else
    match mk_jump (S i) rr' rr4' c with
    | None => None
    | Some (T, dec, inc, sg) =>
      let d := (Z.of_N (lc a4) - Z.of_N (lc a))%Z in
      if negb (Z.eqb (Z.modulo d 4) 0) then None else
      let q := Z.div d 4 in
      if andb (allz (lv a)) (Z.eqb q 0) then
        Some ((b, a) :: T, 0%N :: dec, 0%N :: inc, LF 0 [] :: sg)
      else if Z.ltb q 0 then
        let dn := Z.to_N (- q) in
        let M := (lc a - 4 * dn * lc c)%N in
        let s := LF 0 (map (fun x => x / 4)%N (zsub (lv a) (map (N.mul (4 * dn)) (lv c)))) in
        Some ((b, uvar i M) :: T, dn :: dec, 0%N :: inc, s :: sg)
      else
        let s := LF 0 (map (fun x => x / 4)%N (lv a)) in
        Some ((b, uvar i (lc a)) :: T, 0%N :: dec, Z.to_N q :: inc, s :: sg)
    end
  | _, _ => None
  end.

Fixpoint mapadd (c : lf) (sg : list lf) (w : list N) : list lf :=
  match sg, w with
  | s :: sg', x :: w' => lf_add s (lf_scale x c) :: mapadd c sg' w'
  | _, _ => []
  end.

Lemma mapadd_ev nu c sg : forall w, length sg = length w ->
  map (evN nu) (mapadd c sg w) = zadd (map (evN nu) sg) (vscale (evN nu c) w).
Proof.
  induction sg as [|s sg IH]; intros [|x w] Hl; cbn in Hl; try discriminate; [reflexivity|].
  cbn [mapadd map vscale zadd]. injection Hl as Hl. rewrite (IH w Hl). unfold vscale.
  f_equal. rewrite evN_add, evN_scale. lia.
Qed.

Definition cyc4 (p : bool) : list bool := [p; p; p; p].

Definition jump_run (p : bool) (c : lf) (rr : list run) : option (list run) :=
  match eps (cyc4 p) rr with
  | None => None
  | Some rr4 =>
    match mk_jump 0 rr rr4 c with
    | None => None
    | Some (T, dec, inc, sg) =>
      if andb (Nat.eqb (length sg) (length dec)) (Nat.eqb (length sg) (length inc)) then
        match eps (cyc4 p) (subst_runs dec T) with
        | None => None
        | Some X =>
          if andb (runs_eqb X (subst_runs inc T)) (runs_eqb rr (comp_runs (mapadd c sg dec) T))
          then Some (comp_runs (mapadd c sg inc) T) else None
        end
      else None
    end
  end.

Lemma jump_run_spec p c rr rr' : jump_run p c rr = Some rr' ->
  forall nu, EpSeq (repeat p (4 * ev nu c)) (evR nu rr) (evR nu rr').
Proof.
  unfold jump_run. intros H nu.
  destruct (eps (cyc4 p) rr) as [rr4|]; [|discriminate].
  destruct (mk_jump 0 rr rr4 c) as [[[[T dec] inc] sg]|]; [|discriminate].
  destruct (andb (Nat.eqb (length sg) (length dec)) (Nat.eqb (length sg) (length inc))) eqn:El; [|discriminate].
  apply andb_prop in El as [El1 El2]. apply Nat.eqb_eq in El1, El2.
  destruct (eps (cyc4 p) (subst_runs dec T)) as [X|] eqn:EX; [|discriminate].
  destruct (andb (runs_eqb X (subst_runs inc T)) (runs_eqb rr (comp_runs (mapadd c sg dec) T))) eqn:Ec;
    [|discriminate].
  apply andb_prop in Ec as [Ec1 Ec2]. inversion H; subst rr'; clear H.
  assert (Hc : forall nu', EpSeq [p; p; p; p] (evR nu' (subst_runs dec T)) (evR nu' (subst_runs inc T))).
  { intros nu'. pose proof (eps_spec _ _ _ EX nu') as HX. unfold evR in *.
    rewrite <-(runs_eqb_ev nu' _ _ (const S0) Ec1). exact HX. }
  pose proof (jump_lemma T p dec inc Hc (ev nu c) (map (evN nu) sg)) as J.
  unfold ev in J at 2 3. rewrite N2Nat.id in J.
  unfold evR in *. rewrite (runs_eqb_ev nu _ _ (const S0) Ec2), !ev_runs_comp, !mapadd_ev by assumption.
  exact J.
Qed.

(* ---- programs: single episodes and jumps ---- *)

Inductive instr := ISingle (p : bool) | IJump (p : bool) (c : lf).

Definition seg : Type := (bool * lf)%type.

Fixpoint segs_ev (nu : list N) (ss : list seg) : list bool :=
  match ss with [] => [] | (p, n) :: ss' => repeat p (ev nu n) ++ segs_ev nu ss' end.

Fixpoint exec (prog : list instr) (rr : list run) : option (list run * list seg) :=
  match prog with
  | [] => Some (rr, [])
  | ISingle p :: prog' =>
    match ep_run p rr with
    | Some rr1 => match exec prog' rr1 with Some (rr2, ss) => Some (rr2, (p, cn 1) :: ss) | None => None end
    | None => None
    end
  | IJump p c :: prog' =>
    match jump_run p c rr with
    | Some rr1 => match exec prog' rr1 with Some (rr2, ss) => Some (rr2, (p, lf_scale 4 c) :: ss) | None => None end
    | None => None
    end
  end.

Lemma ev_scale4 nu c : ev nu (lf_scale 4 c) = 4 * ev nu c.
Proof. unfold ev. change (lc (lf_scale 4 c) + dot (lv (lf_scale 4 c)) nu)%N with (evN nu (lf_scale 4 c)).
  rewrite evN_scale. unfold evN. lia. Qed.

Lemma exec_spec prog : forall rr rr' ss, exec prog rr = Some (rr', ss) ->
  forall nu, EpSeq (segs_ev nu ss) (evR nu rr) (evR nu rr').
Proof.
  induction prog as [|[p|p c] prog IH]; intros rr rr' ss H nu; cbn [exec] in H.
  - inversion H; subst. reflexivity.
  - destruct (ep_run p rr) as [rr1|] eqn:E1; [|discriminate].
    destruct (exec prog rr1) as [[rr2 ss2]|] eqn:E2; [|discriminate].
    inversion H; subst; clear H. cbn [segs_ev].
    replace (ev nu (cn 1)) with 1 by reflexivity. cbn [repeat app].
    exists (evR nu rr1). split; [apply (ep_run_spec _ _ _ E1) | apply (IH _ _ _ E2)].
  - destruct (jump_run p c rr) as [rr1|] eqn:E1; [|discriminate].
    destruct (exec prog rr1) as [[rr2 ss2]|] eqn:E2; [|discriminate].
    inversion H; subst; clear H. cbn [segs_ev]. rewrite ev_scale4.
    apply (EpSeq_app _ _ _ (evR nu rr1)); [apply (jump_run_spec _ _ _ _ E1) | apply (IH _ _ _ E2)].
Qed.

(* the phase sequence of a program: all c_K + 2 episodes first, then all c_K episodes *)
Fixpoint sum_ph (p : bool) (ss : list seg) : lf :=
  match ss with
  | [] => LF 0 []
  | (q, n) :: ss' => if Bool.eqb p q then lf_add n (sum_ph p ss') else sum_ph p ss'
  end.
Fixpoint split_ok (seen_false : bool) (ss : list seg) : bool :=
  match ss with
  | [] => true
  | (true, _) :: ss' => andb (negb seen_false) (split_ok false ss')
  | (false, _) :: ss' => split_ok true ss'
  end.

Lemma ev_lf_add nu a b : ev nu (lf_add a b) = ev nu a + ev nu b.
Proof. apply ev_add. Qed.

Lemma split_false ss nu : split_ok true ss = true -> segs_ev nu ss = repeat false (ev nu (sum_ph false ss)).
Proof.
  induction ss as [|[q n] ss IH]; intros H; [reflexivity|].
  destruct q; cbn in H; [discriminate|]. cbn [segs_ev sum_ph Bool.eqb]. rewrite ev_lf_add, repeat_add, IH by exact H.
  reflexivity.
Qed.

Lemma sum_false_true ss : split_ok true ss = true -> sum_ph true ss = LF 0 [] \/ True.
Proof. auto. Qed.

Lemma split_spec ss nu : split_ok false ss = true ->
  segs_ev nu ss = repeat true (ev nu (sum_ph true ss)) ++ repeat false (ev nu (sum_ph false ss)).
Proof.
  induction ss as [|[q n] ss IH]; intros H; [reflexivity|].
  destruct q.
  - cbn in H. cbn [segs_ev sum_ph Bool.eqb]. rewrite ev_lf_add, repeat_add, IH by exact H. rewrite app_assoc. reflexivity.
  - cbn in H. cbn [segs_ev sum_ph Bool.eqb]. rewrite split_false by exact H.
    assert (Et : ev nu (sum_ph true ((false, n) :: ss)) = 0).
    { clear IH. cbn [sum_ph Bool.eqb]. revert H. induction ss as [|[q m] ss IH2]; intros H; [reflexivity|].
      destruct q; cbn in H; [discriminate|]. cbn [sum_ph Bool.eqb]. apply IH2, H. }
    cbn [sum_ph Bool.eqb] in Et. rewrite Et. cbn [repeat app]. rewrite ev_lf_add, repeat_add. reflexivity.
Qed.

Definition prog_check (prog : list instr) (rs re : list run) (T F : lf) : bool :=
  match exec prog rs with
  | Some (re', ss) =>
    andb (andb (runs_eqb re' re) (split_ok false ss)) (andb (lf_eqb (sum_ph true ss) T) (lf_eqb (sum_ph false ss) F))
  | None => false
  end.

Lemma prog_check_spec prog rs re T F : prog_check prog rs re T F = true ->
  forall nu, EpSeq (repeat true (ev nu T) ++ repeat false (ev nu F)) (evR nu rs) (evR nu re).
Proof.
  unfold prog_check. intros H nu.
  destruct (exec prog rs) as [[re' ss]|] eqn:E; [|discriminate].
  apply andb_prop in H as [H1 H2]. apply andb_prop in H1 as [H1 H3]. apply andb_prop in H2 as [H2 H4].
  pose proof (exec_spec _ _ _ _ E nu) as HE. rewrite (split_spec _ _ H3) in HE.
  rewrite (lf_eqb_ev nu _ _ H2), (lf_eqb_ev nu _ _ H4) in HE.
  unfold evR in *. rewrite <-(runs_eqb_ev nu _ _ (const S0) H1). exact HE.
Qed.

(* ===================================================================== *)
(* The six interval programs (Appendix B of the write-up), u = 1 + 8 t.   *)
(* ===================================================================== *)

Definition tl1 (c a : N) : lf := LF c [a].
Definition Rs_r5 : list run := mkruns S0 [tl1 224492 1796256; tl1 673559 5388768; cn 8; tl1 9836 78732; tl1 1942069 15536448]%N.
Definition prog_r5 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 817 6561)] ++ repeat (ISingle true) 6 ++ repeat (ISingle false) 13 ++ [IJump false (tl1 43462 347733)] ++ repeat (ISingle false) 7.
Definition Rs_r0 : list run := mkruns S0 [tl1 74804 598752; tl1 224495 1796256; tl1 673560 5388768; tl1 2020752 16166304; cn 4; tl1 521610 4172796; cn 1]%N.
Definition prog_r0 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 817 6561)] ++ repeat (ISingle true) 6 ++ repeat (ISingle false) 9 ++ [IJump false (tl1 43463 347733)] ++ repeat (ISingle false) 7.
Definition Rs_r1 : list run := mkruns S0 [tl1 2020748 16166304; cn 7; tl1 551120 4408992; tl1 1564809 12518388; cn 2]%N.
Definition prog_r1 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 2457 19683)] ++ repeat (ISingle true) 7 ++ repeat (ISingle false) 5 ++ [IJump false (tl1 130398 1043199)] ++ repeat (ISingle false) 4.
Definition Rs_r2 : list run := mkruns S0 [tl1 8276 66528; tl1 24911 199584; tl1 74808 598752; tl1 224496 1796256; tl1 673559 5388768; tl1 2020751 16166304; cn 8; tl1 29514 236196; tl1 5826224 46609344; cn 2]%N.
Definition prog_r2 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 817 6561)] ++ repeat (ISingle true) 6 ++ repeat (ISingle false) 8 ++ [IJump false (tl1 43464 347733)] ++ repeat (ISingle false) 4.
Definition Rs_r3 : list run := mkruns S0 [tl1 224492 1796256; tl1 673559 5388768; tl1 2020752 16166304; tl1 6062328 48498912; cn 4; tl1 1564810 12518388]%N.
Definition prog_r3 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 2457 19683)] ++ repeat (ISingle true) 7 ++ repeat (ISingle false) 9 ++ [IJump false (tl1 130397 1043199)] ++ repeat (ISingle false) 4.
Definition Rs_r4 : list run := mkruns S0 [tl1 74804 598752; tl1 224495 1796256; tl1 673560 5388768; tl1 2020752 16166304; tl1 6062327 48498912; cn 7; tl1 1653368 13226976; tl1 4694422 37555164; cn 1]%N.
Definition prog_r4 : list instr := repeat (ISingle true) 4 ++ [IJump true (tl1 2457 19683)] ++ repeat (ISingle true) 7 ++ repeat (ISingle false) 6 ++ [IJump false (tl1 130397 1043199)] ++ repeat (ISingle false) 7.
Definition Re_r5 : list run := [(S0, tl1 224492 1796256); (S1, tl1 673560 5388768); (S0, tl1 2020752 16166304); (S1, cn 4); (S0, tl1 521602 4172796)]%N.
Lemma int_r5 : prog_check prog_r5 Rs_r5 Re_r5 (tl1 3278 26244) (tl1 173868 1390932) = true.
Proof. vm_compute. reflexivity. Qed.
Definition Re_r0 : list run := [(S0, tl1 74804 598752); (S1, tl1 224496 1796256); (S0, tl1 673560 5388768); (S1, tl1 2020751 16166304); (S1, cn 7); (S1, tl1 551120 4408992); (S0, tl1 1564798 12518388); (S1, cn 1)]%N.
Lemma int_r0 : prog_check prog_r0 Rs_r0 Re_r0 (tl1 3278 26244) (tl1 173868 1390932) = true.
Proof. vm_compute. reflexivity. Qed.
Definition Re_r1 : list run := [(S0, tl1 2020748 16166304); (S1, cn 8); (S0, tl1 29521 236196); (S0, tl1 5826161 46609344); (S0, cn 2)]%N.
Lemma int_r1 : prog_check prog_r1 Rs_r1 Re_r1 (tl1 9839 78732) (tl1 521601 4172796) = true.
Proof. vm_compute. reflexivity. Qed.
Definition Re_r2 : list run := [(S0, tl1 8276 66528); (S1, tl1 24912 199584); (S0, tl1 74808 598752); (S1, tl1 224495 1796256); (S1, tl1 673559 5388768); (S1, tl1 2020752 16166304); (S0, tl1 6062328 48498912); (S1, cn 3); (S1, tl1 1564801 12518388); (S1, cn 1)]%N.
Lemma int_r2 : prog_check prog_r2 Rs_r2 Re_r2 (tl1 3278 26244) (tl1 173868 1390932) = true.
Proof. vm_compute. reflexivity. Qed.
Definition Re_r3 : list run := [(S0, tl1 224492 1796256); (S1, tl1 673560 5388768); (S0, tl1 2020752 16166304); (S1, tl1 6062327 48498912); (S1, cn 7); (S1, tl1 1653368 13226976); (S0, tl1 4694397 37555164); (S0, cn 2)]%N.
Lemma int_r3 : prog_check prog_r3 Rs_r3 Re_r3 (tl1 9839 78732) (tl1 521601 4172796) = true.
Proof. vm_compute. reflexivity. Qed.
Definition Re_r4 : list run := [(S0, tl1 74804 598752); (S1, tl1 224496 1796256); (S0, tl1 673560 5388768); (S1, tl1 2020751 16166304); (S1, tl1 6062327 48498912); (S1, cn 7); (S1, tl1 88573 708588); (S1, tl1 17478488 139828032); (S0, cn 2)]%N.
Lemma int_r4 : prog_check prog_r4 Rs_r4 Re_r4 (tl1 9839 78732) (tl1 521601 4172796) = true.
Proof. vm_compute. reflexivity. Qed.