Module CACorrectness

From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.
From Coq Require Import Setoid Morphisms.

From Velus Require Import Common.
From Velus Require Import Operators Environment.
From Velus Require Import FunctionalEnvironment.
From Velus Require Import Clocks.
From Velus Require Import CoindStreams IndexedStreams.
From Velus Require Import CoindIndexed.
From Velus Require Import StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LOrdered Lustre.LTyping Lustre.LClocking Lustre.LSemantics Lustre.LClockedSemantics.
From Velus Require Import Lustre.CompAuto.CompAuto Lustre.CompAuto.CAClocking.
From Velus Require Import Lustre.SubClock.SCCorrectness.

Module Type CACORRECTNESS
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import CStr : COINDSTREAMS Ids Op OpAux Cks)
       (Import Senv : STATICENV Ids Op OpAux Cks)
       (Import Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Import Ty : LTYPING Ids Op OpAux Cks Senv Syn)
       (Import Cl : LCLOCKING Ids Op OpAux Cks Senv Syn)
       (Import Ord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Import Sem : LSEMANTICS Ids Op OpAux Cks Senv Syn Ord CStr)
       (Import LCS : LCLOCKEDSEMANTICS Ids Op OpAux Cks Senv Syn Cl Ord CStr Sem)
       (Import CA : COMPAUTO Ids Op OpAux Cks Senv Syn).

  Module Import SCC := SCCorrectnessFun Ids Op OpAux Cks CStr Senv Syn Cl Ord Sem LCS SC. Import SC.

  Import Fresh Notations Facts Tactics.
  Local Open Scope fresh_monad_scope.

  Definition stres_proj1 := stres_st.
  Definition stres_proj2 (stres : Stream (synchronous (enumtag * bool))) :=
    Streams.map (fun x => match x with
                       | absent => absent
                       | present (_, b) => present (Venum (if (b : bool) then OpAux.true_tag else OpAux.false_tag)) end) stres.

  Add Parametric Morphism : stres_proj2
      with signature @EqSt _ ==> @EqSt _
        as stres_proj2_EqSt.
  Proof.

  Fact ac_stres_proj1 : forall xs,
      abstract_clock (stres_proj1 xs) ≡ abstract_clock xs.
  Proof.

  Fact ac_stres_proj2 : forall xs,
      abstract_clock (stres_proj2 xs) ≡ abstract_clock xs.
  Proof.

  Fact stres_proj1_const : forall bs x r,
      stres_proj1 (const_stres bs (x, r)) ≡ enum bs x.
  Proof.

  Fact stres_proj2_const : forall bs x r,
      stres_proj2 (const_stres bs (x, r)) ≡ enum bs (if r then true_tag else false_tag).
  Proof.

  Fact stres_proj1_fselect : forall e k stres xs,
      stres_proj1 (fselect absent e k stres xs) ≡ fselectv e k stres (stres_proj1 xs).
  Proof.

  Fact stres_proj2_fselect : forall e k stres xs,
      stres_proj2 (fselect absent e k stres xs) ≡ fselectv e k stres (stres_proj2 xs).
  Proof.

  Import Permutation.

  Section sem_node.
    Variable G1 : @global nolast last_prefs.
    Variable G2 : @global noauto auto_prefs.

    Hypothesis HwcG : wc_global G1.
    Hypothesis Href : global_sem_refines G1 G2.

    Ltac auto_block_simpl_Forall :=
      repeat
        simpl_Forall;
        (match goal with
         | Hmap: mmap2 _ _ _ = (?blks', _, _), Hin:In _ ?blks' |- _ =>
           eapply mmap2_values, Forall3_ignore13 in Hmap;
           eauto; simpl_Forall
         | _ => idtac
         end; repeat inv_bind);
        eauto.

    Fact case_choose_first1 : forall e r bs vs bs' stres,
        bools_of vs bs' ->
        abstract_clock vs ≡ bs ->
        abstract_clock stres ≡ bs ->
        case vs [(true_tag, enum bs e); (false_tag, stres_proj1 stres)] None (stres_proj1 (choose_first (const_stres bs' (e, r)) stres)).
    Proof.

    Fact case_choose_first2 : forall e r bs vs bs' stres,
        bools_of vs bs' ->
        abstract_clock vs ≡ bs ->
        abstract_clock stres ≡ bs ->
        case vs [(true_tag, enum bs (if (r : bool) then true_tag else false_tag));
                (false_tag, stres_proj2 stres)] None (stres_proj2 (choose_first (const_stres bs' (e, r)) stres)).
    Proof.

    Lemma init_state_exp_sem Γ : forall Hi bs tx ck bs' trans oth stres0,
        Forall (fun '(e, _) => wc_exp G1 Γ e /\ clockof e = [Cbase]) trans ->
        sem_clock (var_history Hi) bs ck bs' ->
        sc_vars Γ Hi bs' ->
        sem_transitions_ck G1 Hi bs' (List.map (fun '(e, t) => (e, (t, false))) trans) (oth, false) stres0 ->
        sem_exp_ck G2 Hi bs (init_state_exp tx ck trans oth) [stres_proj1 stres0].
    Proof.

    Lemma trans_exp_sem Γ : forall Hi bs tx trans oth stres,
        Forall (fun '(e, _) => wc_exp G1 Γ e /\ clockof e = [Cbase]) trans ->
        sc_vars Γ Hi bs ->
        sem_transitions_ck G1 Hi bs trans (oth, false) stres ->
        exists vss, Forall2 (sem_exp_ck G2 Hi bs) (trans_exp tx trans oth) vss
               /\ concat vss = [stres_proj1 stres; stres_proj2 stres].
    Proof.

    Lemma sem_transitions_init_noreset Γ : forall ck ini oth Hi bs bs' stres,
        Forall (fun '(e, _) => wc_exp G1 Γ e /\ clockof e = [Cbase]) ini ->
        sem_clock (var_history Hi) bs ck bs' ->
        sc_vars Γ Hi bs' ->
        sem_transitions_ck G1 Hi bs' (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres ->
        stres_proj2 stres ≡ enum bs' false_tag.
    Proof.

    Fact fby1_stres_proj1 : forall b e xs ys zs,
        fby1 (e, b) xs ys zs ->
        fby1 (Venum e) (stres_proj1 xs) (stres_proj1 ys) (stres_proj1 zs).
    Proof.

    Fact fby_stres_proj1 : forall xs ys zs,
        fby xs ys zs ->
        fby (stres_proj1 xs) (stres_proj1 ys) (stres_proj1 zs).
    Proof.

    Fact fby1_stres_proj2 : forall b e xs ys zs,
        fby1 (e, b) xs ys zs ->
        fby1 (Venum (if (b : bool) then true_tag else false_tag)) (stres_proj2 xs) (stres_proj2 ys) (stres_proj2 zs).
    Proof.

    Fact fby_stres_proj2 : forall xs ys zs,
        fby xs ys zs ->
        fby (stres_proj2 xs) (stres_proj2 ys) (stres_proj2 zs).
    Proof.

    Opaque FEnv.restrict.

    Fact bools_of_stres_proj2 : forall xs,
        bools_of (stres_proj2 xs) (stres_res xs).
    Proof.

    Fact bools_of_fwhen e : forall sc xs bs,
        bools_of xs bs ->
        bools_of (fwhenv e xs sc) (fwhenb e bs sc).
    Proof.

    Lemma fselect_mask_fwhen_hist : forall (Hi: history) e k stres,
        FEnv.Equiv (EqSt (A:=svalue))
                  (fselect_hist e k stres Hi)
                  (CStr.mask_hist k (fwhenb e (stres_res stres) (stres_st stres))
                                  (fwhen_hist e Hi (stres_st stres))).
    Proof.

    Definition default_ann : annotation :=
      Build_annotation OpAux.bool_velus_type Cbase xH None.

    Ltac inv_branch := (Syn.inv_branch || Ty.inv_branch || Cl.inv_branch || Sem.inv_branch || LCS.inv_branch).
    Ltac inv_scope := (Syn.inv_scope || Ty.inv_scope || Cl.inv_scope || Sem.inv_scope || LCS.inv_scope).

    Local Ltac sem_new_vars :=
      subst; eapply sem_var_union3', sem_var_of_list; eauto with datatypes;
      try rewrite fst_NoDupMembers; auto.

    Lemma sc_vars_fselect ck e k sc : forall Γ Γ' Hi bs,
        sem_clock (var_history Hi) bs ck (abstract_clock sc) ->
        (forall x ck', HasClock Γ' x ck' -> HasClock Γ x ck /\ ck' = Cbase) ->
        (forall x, IsLast Γ' x -> IsLast Γ x) ->
        sc_vars Γ Hi bs ->
        sc_vars Γ' (fselect_hist e k sc Hi) (fselectb e k sc bs).
    Proof.

    Lemma sem_transitions_wt_state {PSyn prefs A} (G : @global PSyn prefs) (states : list ((enumtag * ident) * A)) :
      forall Hi bs trans default stres,
        Permutation.Permutation (List.map fst (List.map fst states)) (seq 0 (Datatypes.length states)) ->
        Forall (fun '(_, (t, _)) => InMembers t (List.map fst states)) trans ->
        In (fst default) (seq 0 (Datatypes.length states)) ->
        sem_transitions_ck G Hi bs trans default stres ->
        SForall (fun v => match v with present (e, _) => e < length states | _ => True end) stres.
    Proof.

    Corollary sem_automaton_wt_state1 {PSyn prefs A} (G : @global PSyn prefs) (states : list ((enumtag * ident) * branch (list transition * scope (A * list transition)))) :
      forall Hi bs bs' ini oth stres0 stres1 stres,
        Permutation.Permutation (List.map fst (List.map fst states)) (seq 0 (Datatypes.length states)) ->
        Forall (fun '(_, t) => InMembers t (List.map fst states)) ini ->
        In oth (seq 0 (Datatypes.length states)) ->
        Forall (fun '(_, Branch _ (_, Scope _ (_, trans))) =>
                  Forall (fun '(e, (t, _)) => InMembers t (List.map fst states)) trans) states ->
        sem_transitions_ck G Hi bs' (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres0 ->
        fby stres0 stres1 stres ->
        Forall (fun '((sel, _), Branch _ (_, Scope _ (_, trans))) =>
                  forall k, exists Hik,
                    (let bik := fselectb sel k stres bs in
                     sem_transitions_ck G Hik bik trans
                       (sel, false) (fselect absent sel k stres stres1))) states ->
        SForall (fun v => match v with present (e, _) => e < length states | _ => True end) stres.
    Proof.

    Corollary sem_automaton_wt_state2 {PSyn prefs A} (G : @global PSyn prefs) (states : list ((enumtag * ident) * branch (list transition * scope (A * list transition)))) :
      forall bs bs' ini stres1 stres,
        Permutation.Permutation (List.map fst (List.map fst states)) (seq 0 (Datatypes.length states)) ->
        In ini (seq 0 (Datatypes.length states)) ->
        Forall (fun '(_, Branch _ (trans, _)) =>
                  Forall (fun '(e, (t, _)) => InMembers t (List.map fst states)) trans) states ->
        fby (const_stres bs' (ini, false)) stres1 stres ->
        Forall (fun '((sel, _), Branch _ (trans, _)) =>
                  forall k, exists Hik,
                    (let bik := fselectb sel k stres bs in
                     sem_transitions_ck G Hik bik trans
                       (sel, false) (fselect absent sel k stres stres1))) states ->
        SForall (fun v => match v with present (e, _) => e < length states | _ => True end) stres.
    Proof.

    Corollary sem_automaton_wt_state3 {PSyn prefs A} (G : @global PSyn prefs) (states : list ((enumtag * ident) * branch (list transition * scope (A * list transition)))) :
      forall bs bs' ini stres1 stres,
        Permutation.Permutation (List.map fst (List.map fst states)) (seq 0 (Datatypes.length states)) ->
        In ini (seq 0 (Datatypes.length states)) ->
        Forall (fun '(_, Branch _ (trans, _)) =>
                  Forall (fun '(e, (t, _)) => InMembers t (List.map fst states)) trans) states ->
        fby (const_stres bs' (ini, false)) stres1 stres ->
        Forall (fun '((sel, _), Branch _ (trans, _)) =>
                  forall k, exists Hik,
                    (let bik := fselectb sel k stres bs in
                     sem_transitions_ck G Hik bik trans
                       (sel, false) (fselect absent sel k stres stres1))) states ->
        SForall (fun v => match v with present (e, _) => e < length states | _ => True end) stres1.
    Proof.

    Lemma auto_block_sem : forall blk Γty Γck Hi bs blk' tys st st',
        (forall x, IsVar Γty x -> AtomOrGensym last_prefs x) ->
        (forall x, ~IsLast Γty x) ->
        (forall x, ~IsLast Γck x) ->
        (forall x, IsVar Γck x -> IsVar Γty x) ->
        NoDupLocals (List.map fst Γty) blk ->
        GoodLocals last_prefs blk ->
        nolast_block blk ->
        wt_block G1 Γty blk ->
        wc_block G1 Γck blk ->
        dom_ub Hi Γty ->
        sc_vars Γck Hi bs ->
        sem_block_ck G1 Hi bs blk ->
        auto_block blk st = (blk', tys, st') ->
        sem_block_ck G2 Hi bs blk'.
    Proof.

    Lemma auto_node_sem : forall f n ins outs,
        wt_global (Global G1.(types) G1.(externs) (n::G1.(nodes))) ->
        wc_global (Global G1.(types) G1.(externs) (n::G1.(nodes))) ->
        Ordered_nodes (Global G1.(types) G1.(externs) (n::G1.(nodes))) ->
        Ordered_nodes (Global G2.(types) G2.(externs) ((fst (auto_node n))::G2.(nodes))) ->
        sem_node_ck (Global G1.(types) G1.(externs) (n::G1.(nodes))) f ins outs ->
        sem_node_ck (Global G2.(types) G2.(externs) ((fst (auto_node n))::G2.(nodes))) f ins outs.
    Proof with

  End sem_node.

  Module Clocking := CAClockingFun Ids Op OpAux Cks Senv Syn Cl CA.

  Lemma auto_global_refines : forall G,
      wt_global G ->
      wc_global G ->
      global_sem_refines G (auto_global G).
  Proof with

  Theorem auto_global_sem : forall G f ins outs,
      wt_global G ->
      wc_global G ->
      sem_node_ck G f ins outs ->
      sem_node_ck (auto_global G) f ins outs.
  Proof.

End CACORRECTNESS.

Module CACorrectnessFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (CStr : COINDSTREAMS Ids Op OpAux Cks)
       (Senv : STATICENV Ids Op OpAux Cks)
       (Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Ty : LTYPING Ids Op OpAux Cks Senv Syn)
       (Clo : LCLOCKING Ids Op OpAux Cks Senv Syn)
       (Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Sem : LSEMANTICS Ids Op OpAux Cks Senv Syn Lord CStr)
       (LClockSem : LCLOCKEDSEMANTICS Ids Op OpAux Cks Senv Syn Clo Lord CStr Sem)
       (CA : COMPAUTO Ids Op OpAux Cks Senv Syn)
       <: CACORRECTNESS Ids Op OpAux Cks CStr Senv Syn Ty Clo Lord Sem LClockSem CA.
  Include CACORRECTNESS Ids Op OpAux Cks CStr Senv Syn Ty Clo Lord Sem LClockSem CA.
End CACorrectnessFun.
Generated by coq2html