HyPre.sstep.MultiStep

From Coq Require Export
  Program.Equality
  Relations.Relations.

From HyPre Require Export
  ListExtra
  NatExtra
  MapExtra
  Tac.

From HyPre Require Export
  ApplyLf.

Import ListNotations.

Fixpoint multi_step {St : Type} (step : St -> St) (s : St) (n : nat) : list St
  := match n with
     | 0 => [s]
     | S n => multi_step step (step s) n ++ [s]
     end.

Fixpoint multi_until {St : Type} (b : St -> bool) (step : St -> St) (s : St) (n : nat) : St
  := match n with
     | 0 => s
     | S n => if b s then s else multi_until b step (step s) n
     end.

Fixpoint multi_step_until_opt {St : Type} (b : St -> bool) (step : St -> St) (s : St) (n : nat) : option (list St)
  := match n with
     | 0 => None
     | S n => if b s then Some [s] else match multi_step_until_opt b step (step s) n with
                                       | Some x => Some (x ++ [s])
                                       | None => None
                                       end
     end.

Definition multi_step_hd {St : Type} (step : St -> St) (s : St) (n : nat) : St
  := hd s (multi_step step s n).

Fixpoint multi_eval {L : Type}
  (e : L -> list L -> nat -> list L) (b : L -> nat) acc (n : nat)
  : list L
  := match n with
     | 0 => acc
     | S n => match acc with
             | [] => []
             | s :: acc' => multi_eval e b (e s acc' (b s)) n
             end
     end.

Lemma multi_step_len {St : Type} (step : St -> St) (s : St) (n : nat)
  : length (multi_step step s n) = S n.
Proof.
  revert s.
  induction n;intros;cbn.
  - reflexivity.
  - rewrite app_length.
    rewrite IHn.
    cbn.
    lia.
Qed.

Lemma multi_step_app {St : Type} (step : St -> St) (s : St) (n m : nat)
  : multi_step step s (S n + m) = multi_step step (step (multi_step_hd step s m)) n ++ multi_step step s m.
Proof.
  revert s n.
  induction m;intros;cbn.
  - setoid_rewrite <-plus_n_O.
    reflexivity.
  - replace (n + S m) with (S n + m) by lia.
    rewrite IHm.
    unfold multi_step_hd.
    cbn.
    rewrite app_assoc.
    f_equal.
    f_equal.
    f_equal.
    f_equal.
    destruct (multi_step step (step s) m) eqn:E;cbn.
    + exfalso.
      eapply f_equal with (f:=@length _) in E.
      rewrite multi_step_len in E.
      cbn in E.
      congruence.
    + reflexivity.
Qed.

Lemma multi_step_hd_app {St : Type} (step : St -> St) (s s' s'' : St) (n : nat) x
  : hd s' (multi_step step s n ++ x) = hd s'' (multi_step step s n).
Proof.
  revert s s' s'' x.
  induction n;cbn;eauto;intros.
  setoid_rewrite IHn.
  rewrite <-app_assoc.
  setoid_rewrite IHn.
  reflexivity.
  Unshelve.
  exact s.
Qed.

Lemma multi_step_hd_step {St : Type} (step : St -> St) (s : St) (n : nat)
  : multi_step_hd step s (S n) = step (multi_step_hd step s n).
Proof.
  unfold multi_step_hd.
  cbn.
  setoid_rewrite multi_step_hd_app with (s'':=s).
  revert s.
  induction n;cbn;intros.
  - reflexivity.
  - setoid_rewrite multi_step_hd_app.
    rewrite <-IHn.
    reflexivity.
Qed.

(* TODO clean-up & instantiate this lemma with b = length of imp program *)
Lemma multi_step_apply_lf_progress {L L' Y: Type}
  (step : L -> L) (lf : L -> Y -> list L' * Y) (b : nat)
  (s : L) (i : Y) (n : nat)
  (Hb : forall s' i n, multi_step_hd step s n = s' -> 0 < length (apply_lf lf i (multi_step step s' b))) (* b depends on s *)
  : length (apply_lf lf i (multi_step step s (n * S b))) >= n.
Proof.
  revert i.
  induction n;intros.
  - cbn.
    lia.
  - replace (S n * S b) with (S b + n * S b) by lia.
    rewrite multi_step_app.
    rewrite apply_lf_app.
    rewrite app_length.
    specialize (IHn i).
    match goal with |- length (apply_lf _ ?y (_ _ ?s2 _)) + _ >= _
                    => specialize (Hb s2 y (S (n * S b)))
    end.
    cbn in Hb.
    exploit Hb.
    eapply multi_step_hd_step.
    lia.
Qed.

Lemma multi_step_S {X : Type} (step : X -> X) (x : X) n
  : multi_step step x (S n) = (multi_step step (step x) n) ++ [x].
Proof.
  cbn.
  reflexivity.
Qed.

Lemma multi_step_hd_S {X : Type} (step : X -> X) (x y y' : X) n
  : hd y (multi_step step (step x) n) = hd y' (multi_step step x (S n)).
Proof.
  revert x y y'.
  induction n;intros;cbn.
  - reflexivity.
  - setoid_rewrite multi_step_hd_app.
    rewrite <-multi_step_S.
    setoid_rewrite multi_step_hd_app.
    eapply IHn.
    Unshelve.
    all: exact x.
Qed.

Lemma multi_step_S2 {X : Type} (step : X -> X) (x : X) n
  : multi_step step x (S n) = step (multi_step_hd step x n) :: multi_step step x n.
Proof.
  revert x.
  induction n;intros.
  - cbn;reflexivity.
  - cbn.
    rewrite app_comm_cons.
    f_equal.
    rewrite <-multi_step_S.
    rewrite IHn.
    f_equal.
    f_equal.
    eapply multi_step_hd_S.
Qed.

Lemma multi_step_apply_lf_progress_step {L L' Y: Type}
  (step : L -> L) (lf : L -> Y -> list L' * Y)
  (s : L) (i : Y) (n : nat)
  (Hb : forall i s, 0 < length (apply_lf lf i ([step s])))
  : length (apply_lf lf i (multi_step step s n)) >= n.
Proof.
  revert i.
  induction n;intros.
  - cbn.
    lia.
  - setoid_rewrite multi_step_S2.
    rewrite cons_app.
    rewrite cons_app.
    rewrite apply_lf_app.
    rewrite app_length.
    cbn.
    specialize (IHn i).
    match goal with
      |- | _ _ ?i' ([step ?s']) | + _ >= _ => specialize (Hb i' s')
    end.
    lia.
Qed.

Fail Lemma multi_step_apply_lf_progress_dep {L L' Y: Type}
  (step : L -> L) (lf : L -> Y -> list L' * Y) (b : L -> nat)
  (s : L) (i : Y) (n : nat)
  (Hb : forall s, length (apply_lf lf i (multi_step step s n)) < length (apply_lf lf i (multi_step step s (b s))))
  : length (apply_lf lf i (multi_step step s (fold_right 0 n))) >= n.
(*TODO remove:
 I might want to revisit the multi_eval approach:
     If have a progress lemma with a budget dependent on the current state,
     I could just use stmt_len as budget. IS that REALLY easier?
     maybe just scrap all of it and write inductive loop semantics *)

Lemma multi_step_apply_lf_progress' {L L' Y: Type}
  (step : L -> L) (lf : L -> list L') (b : nat)
  (s : L) (n : nat)
  (Hb : forall s' n, multi_step_hd step s n = s' -> 0 < length (apply_lf' lf (multi_step step s' b))) (* b depends on s *)
  : length (apply_lf' lf (multi_step step s (n * S b))) >= n.
Proof.
  unfold apply_lf' in *.
  eapply multi_step_apply_lf_progress.
  intros;eauto.
  destruct i.
  eapply Hb;eauto.
Qed.

(* this ensures that we can construct arbitrarily long traces on the leakage.
     afterwards the idea is, that we can make sure it is not too long by using lastn *)
(* so stst_sem would use a combination of multi_eval_len, lastn & length
     similar to imp_trace *)
(* in our example b would be the distance to the next loop header
      ^-- NO, much simpler: just the length of the program
     (since we're allowed to overshoot, we may ignore other possible leaks in between *)
(* come to think of it, it is probably easier to write one evaluator that does a loop iteration
     in one step *)

Inductive multi {X : Type} (R : relation X) : relation X :=
| multi_refl x : multi R x x
| multi_trans : forall (x y z : X),
    R y z ->
    multi R x y ->
    multi R x z.

(* TODO would it be simpler to use multi_trace ? *)
Inductive multi_trace {X : Type} (R : relation X) : list X -> Prop :=
| multi_nil : multi_trace R []
| multiT_refl : forall (x : X), multi_trace R [x]
| multiT_step : forall (x y : X) (yt : list X),
    R y x
    -> multi_trace R (y :: yt)
    -> multi_trace R (x :: y :: yt).

Inductive multi_trace_from {X : Type} (R : relation X) (z : X) : list X -> Prop :=
| multifT_refl : multi_trace_from R z [z]
| multifT_step : forall (x y : X) (yt : list X),
    R y x
    -> multi_trace_from R z (y :: yt)
    -> multi_trace_from R z (x :: y :: yt).

Lemma multi_trace_multi_step {X : Type} (step : X -> X) (x : X) (xt : list X)
  : multi_trace_from (fun a b => step a = b) x xt -> multi_step step x (length xt - 1) = xt.
Proof.
  intros H.
  dependent induction H.
  - cbn.
    reflexivity.
  - rename IHmulti_trace_from into Q.
    cbn in *.
    rewrite Nat.sub_0_r in Q.
    rewrite <-multi_step_S.
    rewrite multi_step_S2.
    f_equal.
    2: eapply Q.
    rewrite <-H.
    unfold multi_step_hd.
    rewrite Q.
    cbn.
    reflexivity.
Qed.

Lemma multi_step_multi_trace {X : Type} (step : X -> X) (x : X) (xt : list X)
  : multi_step step x (length xt - 1) = xt -> multi_trace_from (fun a b => step a = b) x xt.
Proof.
  dependent induction xt;cbn;intros.
  - congruence.
  - rewrite PeanoNat.Nat.sub_0_r in H.
    destruct xt;cbn in H.
    + inversion H.
      econstructor.
    + cbn in IHxt.
      rewrite <-multi_step_S in H.
      rewrite multi_step_S2 in H.
      econstructor.
      * inversion H.
        unfold multi_step_hd.
        rewrite H2.
        cbn.
        reflexivity.
      * eapply IHxt.
        rewrite PeanoNat.Nat.sub_0_r.
        inversion H.
        reflexivity.
Qed.

Lemma multi_step_multi_trace' {X : Type} (step : X -> X) (x y : X) (xt : list X)
  : multi_step step x (length xt) = y :: xt -> multi_trace_from (fun a b => step a = b) x (y :: xt).
Proof.
  intros.
  eapply multi_step_multi_trace.
  cbn.
  replace (|xt| - 0) with (|xt|) by lia.
  assumption.
Qed.

From Coq Require Import
  Classes.RelationClasses
  Classes.Morphisms.

Global Instance multi_step_Proper {X : Type}
  : Proper ((fun st1 st2 => forall (x : X), st1 x = st2 x) ==> eq ==> eq ==> eq) multi_step.
Proof.
  unfold Proper, respectful.
  intros.
  subst y0 y1.
  revert x0.
  induction x1;intros;cbn.
  - reflexivity.
  - setoid_rewrite IHx1.
    rewrite H.
    reflexivity.
Qed.

From Coq Require Import Program.Basics.

Global Instance multi_trace_from_Proper {X : Type}
  : Proper ((fun (R1 R2 : relation X) => forall x y, R1 x y -> R2 x y) ==> eq ==> eq ==> impl) multi_trace_from.
Proof.
  unfold Proper, respectful.
  intros.
  subst y0 y1.
  unfold impl.
  intros.
  dependent induction H0.
  - econstructor.
  - econstructor.
    + eapply H;eauto.
    + eauto.
Qed.

Lemma multi_until_S {X : Type} (step : X -> X) b (x : X) n
  : b (multi_until b step x n) = true
    -> b (multi_until b step x (S n)) = true.
Proof.
  revert x.
  induction n;intros.
  - cbn in H.
    cbn.
    destruct (b x) eqn:E;[ | congruence].
    eauto.
  - cbn.
    cbn in H.
    destruct (b x) eqn:E;eauto.
Qed.

Lemma multi_until_le {X : Type} (step : X -> X) b (x : X) n m
  : n <= m -> b (multi_until b step x n) = true -> b (multi_until b step x m) = true.
Proof.
  intros.
  induction H.
  - assumption.
  - eapply multi_until_S;eauto.
Qed.

Definition multi_step' {X : Type} (step : X -> X) (x : X) (n : nat)
  := match n with
     | 0 => []
     | S n => multi_step step x n
     end.