HyPre.prop.NonInterference

(* CLN B *)
From Coq Require Export
  Classes.EquivDec
  RelationClasses.
From Coq Require Import
  Program.Basics.
Open Scope program_scope.

From HyPre Require Export
  ApplyLf
  PreSuffix
  Safety
  Tac
  VectorList
  VectorPred.
Export Safety.Veclist.

Import ListNotations.
Import VectorListNotations.
Import ListSafety.

Section with_st.
  Context {Input State LL : Type}.
  Context (low_eq : Input -> Input -> Prop).
  Context {low_eqEquiv : Equivalence low_eq}.
  (* a leakage function, mapping from some internal state (used for the simulation)
     to the observable leakage *)
  Context (leakS : State -> list LL).
  Context `{Heq : EqDec LL eq}.

  Definition ll_eq sl1 sl2
    := apply_lf' leakS sl1 = apply_lf' leakS sl2.

  Definition ni_eq i1 i2 sl1 sl2
    := low_eq i1 i2 -> ll_eq sl1 sl2.

  (* ll_eq and correspondingly ni_eq, are too strict when considering arbitrary prefixes of different length *)
  Definition ll_pre sl1 sl2
    := let sl1' := apply_lf' leakS sl1 in
       let sl2' := apply_lf' leakS sl2 in
       prefix sl1' sl2' \/ prefix sl2' sl1'.

  Definition ni_pre i1 i2 sl1 sl2
    := low_eq i1 i2 -> ll_pre sl1 sl2.

  Ltac unfold_llni := unfold ll_eq,ll_pre,ni_pre,ni_eq in *.

  Lemma ll_eq_ll_pre sl1 sl2
    : ll_eq sl1 sl2 -> ll_pre sl1 sl2.
  Proof.
    intros.
    unfold_llni.
    setoid_rewrite H.
    left.
    econstructor.
  Qed.

  Lemma ll_pre_nil1 l
    : ll_pre [] l.
  Proof.
    unfold ll_pre.
    cbn.
    left.
    eapply prefix_nil.
  Qed.

  Lemma ll_pre_nil2 l
    : ll_pre l [].
  Proof.
    unfold ll_pre.
    cbn.
    right.
    eapply prefix_nil.
  Qed.

  Lemma apply_lf'_prefix {X Y : Type} (lf : X -> list Y) l1 l2
        (Hpre : prefix l1 l2)
    : prefix (apply_lf' lf l1) (apply_lf' lf l2).
  Proof.
    induction Hpre.
    - econstructor.
    - rewrite apply_lf'_S.
      eapply prefix_app_r;eauto.
  Qed.

  (* TODO Prove vl_ll lemmas *)
  Lemma vl_ll_pre_safety
    : veclist_safety (v2 ll_pre).
  Proof.
    unfold veclist_safety.
    unfold Safety.safety_property.
    intros.
    unfold veclist_prefix in H.
    unfold ll_pre in *.
    unfold v2 in *.
    destruct H0.
    - specialize (vec_forall2_nth _ _ _ _ H) with (i:=Fin.F1) as H1.
      specialize (vec_forall2_nth _ _ _ _ H) with (i:=Fin.FS Fin.F1) as H2.
      cbn in H1,H2.
      eapply apply_lf'_prefix with (lf:=leakS) in H1.
      eapply apply_lf'_prefix with (lf:=leakS) in H2.
      eapply prefix_trans in H0.
      2: eapply H1.
      eapply prefix_order_destruct in H0.
      2: eapply H2.
      destruct H0;[right|left];assumption.
    - specialize (vec_forall2_nth _ _ _ _ H) with (i:=Fin.F1) as H1.
      specialize (vec_forall2_nth _ _ _ _ H) with (i:=Fin.FS Fin.F1) as H2.
      cbn in H1,H2.
      eapply apply_lf'_prefix with (lf:=leakS) in H1.
      eapply apply_lf'_prefix with (lf:=leakS) in H2.
      eapply prefix_trans in H0.
      2: eapply H2.
      eapply prefix_order_destruct in H0.
      2: eapply H1.
      destruct H0;[left|right];assumption.
  Qed.

  Lemma vl_ll_eq_zero
    : v2 ll_eq vl_zero.
  Proof.
    unfold v2, ll_eq.
    setoid_rewrite Vector.const_nth.
    reflexivity.
  Qed.

  Lemma vl_ll_eq_ll_pre a
    : v2 ll_eq a -> v2 ll_pre a.
  Proof.
    eapply ll_eq_ll_pre.
  Qed.

  Lemma vl_ll_pre_len_ll_eq a
    : v2 ll_pre a -> v2 (fun sl1 sl2 => | apply_lf' leakS sl1 | = | apply_lf' leakS sl2 |) a -> v2 ll_eq a.
  Proof.
    intros.
    unfold v2 in *.
    unfold ll_pre in H.
    unfold ll_eq.
    destruct H. 2: symmetry.
    all:eapply prefix_length;eauto.
  Qed.

End with_st.

Lemma v2_leak_map_map {L1 L2 L3 : Type} (a : Vector.t (list L1) 2) (l1 : L1 -> L2) (l2 : L2 -> list L3)
  : v2 (ll_eq (l2 ∘ l1)) a <-> v2 (ll_eq l2) (Vector.map (map l1) a).
Proof.
  unfold v2,ll_eq in *.
  setoid_rewrite Vector.nth_map. 2,3:reflexivity.
  setoid_rewrite apply_lf'_compose at 1 2.
  reflexivity.
Qed.

Definition rem_None {L : Type} (l : option L) : list L
  := match l with
     | Some l => [l]
     | None => []
     end.