From Coq Require Import Streams.
From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.

From Coq Require Import Sorting.Permutation.
From Coq Require Import Setoid.
From Coq Require Import Morphisms.

From Coq Require Import FSets.FMapPositive.
From Velus Require Import Common.
From Velus Require Import CommonList.
From Velus Require Import FunctionalEnvironment.
From Velus Require Import Operators.
From Velus Require Import CoindStreams IndexedStreams.
From Velus Require Import CoindIndexed.
From Velus Require Import Clocks.
From Velus Require Import Lustre.StaticEnv.
From Velus Require Import Lustre.LSyntax Lustre.LTyping Lustre.LClocking Lustre.LCausality Lustre.LOrdered.
From Velus Require Import Lustre.LSemantics Lustre.LClockedSemantics.

Clock Correctness Proof

Module Type LCLOCKCORRECTNESS
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import Senv : STATICENV Ids Op OpAux Cks)
       (Import Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Import Typ : LTYPING Ids Op OpAux Cks Senv Syn)
       (Import Clo : LCLOCKING Ids Op OpAux Cks Senv Syn)
       (Import LCA : LCAUSALITY Ids Op OpAux Cks Senv Syn)
       (Import Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (Import CStr : COINDSTREAMS Ids Op OpAux Cks)
       (Import Sem : LSEMANTICS Ids Op OpAux Cks Senv Syn Lord CStr)
       (Import CkSem : LCLOCKEDSEMANTICS Ids Op OpAux Cks Senv Syn Clo Lord CStr Sem).

  Import CStr.
  Module IStr := IndexedStreamsFun Ids Op OpAux Cks.
  Module Import CIStr := CoindIndexedFun Ids Op OpAux Cks CStr IStr.

  Import List.

  Definition sem_clock_inputs {PSyn prefs} (G : @global PSyn prefs) (f : ident) (xs : list (Stream svalue)): Prop :=
    exists H n,
      find_node f G = Some n /\
      Forall2 (fun x => sem_var H (Var x)) (idents (n_in n)) xs /\
      Forall2 (fun xc => sem_clock (var_history H) (clocks_of xs) (snd xc))
              (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) (map abstract_clock xs).

  Lemma sem_clock_inputs_cons {PSyn prefs} :
    forall types externs (nodes : list (@node PSyn prefs)) f n ins,
      n_name n <> f ->
      sem_clock_inputs (Global types externs nodes) f ins <-> sem_clock_inputs (Global types externs (n :: nodes)) f ins.

  Fact sem_var_env_eq :
    forall H H' xs ss,
      Forall2 (fun x => sem_var H (Var x)) xs ss ->
      Forall2 (fun x => sem_var H' (Var x)) xs ss ->
      Forall (fun x => orel (EqSt (A:=svalue)) (H (Var x)) (H' (Var x))) xs.

  Lemma inputs_clocked_vars {PSyn prefs} :
    forall types externs (nodes : list (@node PSyn prefs)) n H f ins,
      sem_clock_inputs (Global types externs (n :: nodes)) f ins ->
      n_name n = f ->
      wc_env (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) ->
      Forall2 (fun x => sem_var H (Var x)) (idents (n_in n)) ins ->
      Forall2 (fun xc => sem_clock (var_history H) (clocks_of ins) (snd xc)) (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) (map abstract_clock ins).

  Lemma sem_clocks_corres_in : forall H H' b (ins : list (ident * (type * clock * ident))) vins ss,
      wc_env (map (fun '(x, (_, ck, _)) => (x, ck)) ins) ->
      Forall2 (fun x => sem_var H (Var x)) (map fst ins) vins ->
      Forall2 (fun x => sem_var H' (Var x)) (map fst ins) vins ->
      Forall2 (fun xc => sem_clock (var_history H) b (snd xc)) (map (fun '(x, (_, ck, _)) => (x, ck)) ins) ss ->
      Forall2 (fun xs => sem_clock (var_history H') b (snd xs)) (map (fun '(x, (_, ck, _)) => (x, ck)) ins) ss.

  Lemma sem_clocks_corres_out : forall H H' b (ins : list (ident * (type * clock * ident))) (outs: list decl) vins vouts ss,
      wc_env (map (fun '(x, (_, ck, _)) => (x, ck)) ins ++ map (fun '(x, (_, ck, _, _)) => (x, ck)) outs) ->
      Forall2 (fun x => sem_var H (Var x)) (map fst ins) vins ->
      Forall2 (fun x => sem_var H (Var x)) (map fst outs) vouts ->
      Forall2 (fun x => sem_var H' (Var x)) (map fst ins) vins ->
      Forall2 (fun x => sem_var H' (Var x)) (map fst outs) vouts ->
      Forall2 (fun xc => sem_clock (var_history H) b (snd xc)) (map (fun '(x, (_, ck, _, _)) => (x, ck)) outs) ss ->
      Forall2 (fun xs => sem_clock (var_history H') b (snd xs)) (map (fun '(x, (_, ck, _, _)) => (x, ck)) outs) ss.

  Section sc_inv.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.
    Variable (G : @global complete prefs).

    Hypothesis Hnode : forall f ins outs,
        sem_node G f ins outs ->
        sem_clock_inputs G f ins ->
        sem_node_ck G f ins outs.

    Lemma Hscnodes :
      forall G1 H f n xs os,
        wc_node G1 n ->
        Sem.sem_node G f xs os ->
        find_node f G = Some n ->
        Forall2 (fun x => sem_var H (Var x)) (map fst (n_in n)) xs ->
        Forall2 (fun x => sem_var H (Var x)) (map fst (n_out n)) os ->
        Forall2 (fun xc => sem_clock (var_history H) (clocks_of xs) (snd xc))
                (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) (map abstract_clock xs) ->
        Forall2 (fun xc => sem_clock (var_history H) (clocks_of xs) (snd xc))
                (map (fun '(x, (_, ck, _, _)) => (x, ck)) (n_out n)) (map abstract_clock os).

    Definition sc_var_inv Γ (H : Sem.history) (b : Stream bool) : ident -> Prop :=
      fun cx =>
        (forall x ck xs,
            HasCaus Γ x cx ->
            HasClock Γ x ck ->
            sem_var H (Var x) xs ->
            sem_clock (var_history H) b ck (abstract_clock xs))
        /\ (forall x ck xs,
              HasLastCaus Γ x cx ->
              HasClock Γ x ck ->
              sem_var H (Last x) xs ->
              sem_clock (var_history H) b ck (abstract_clock xs)).

    Lemma sc_vars_sc_var_inv : forall Γ H b,
        sc_vars Γ H b ->
        Forall (sc_var_inv Γ H b) (map snd (idcaus_of_senv Γ)).

    Lemma sc_var_inv_sc_vars : forall Γ H b,
        NoDupMembers Γ ->
        Forall (sc_var_inv Γ H b) (map snd (idcaus_of_senv Γ)) ->
        sc_vars Γ H b.

    Definition sc_exp_inv Γ Γty H b : exp -> nat -> Prop :=
      fun e k => forall ss,
          wt_exp G Γty e ->
          wc_exp G Γ e ->
          Sem.sem_exp G H b e ss ->
          sem_clock (var_history H) b (nth k (clockof e) Cbase) (abstract_clock (nth k ss (def_stream b))).

    Fact P_exps_sc_exp_inv : forall Γ Γty H b es ss k,
        Forall (wt_exp G Γty) es ->
        Forall (wc_exp G Γ) es ->
        Forall2 (Sem.sem_exp G H b) es ss ->
        P_exps (sc_exp_inv Γ Γty H b) es k ->
        sem_clock (var_history H) b (nth k (clocksof es) Cbase) (abstract_clock (nth k (concat ss) (def_stream b))).

    Fact Forall2Brs_sc_exp_inv1 : forall Γ Γty H b ck x tx es k ss,
        k < length ss ->
        Forall (fun es => Forall (wt_exp G Γty) (snd es)) es ->
        Forall (fun es => Forall (wc_exp G Γ) (snd es)) es ->
        Forall (fun '(i, es0) => Forall (eq (Con ck x (tx, i))) (clocksof es0)) es ->
        Forall (fun es0 => length ss = length (clocksof (snd es0))) es ->
        Forall2Brs (Sem.sem_exp G H b) es ss ->
        Forall (fun es => P_exps (sc_exp_inv Γ Γty H b) (snd es) k) es ->
        Forall (fun '(i, v) => sem_clock (var_history H) b (Con ck x (tx, i)) (abstract_clock v)) (nth k ss []).

    Fact P_exps_sc_exp_inv_all : forall Γ Γty H b es ss,
        Forall (wt_exp G Γty) es ->
        Forall (wc_exp G Γ) es ->
        Forall2 (Sem.sem_exp G H b) es ss ->
        (forall k, k < length (annots es) -> P_exps (sc_exp_inv Γ Γty H b) es k) ->
        Forall2 (sem_clock (var_history H) b) (clocksof es) (map abstract_clock (concat ss)).

    Lemma sc_exp_const : forall Γ Γty H b c,
        sc_exp_inv Γ Γty H b (Econst c) 0.

    Lemma sc_exp_enum : forall Γ Γty H b k ty,
        sc_exp_inv Γ Γty H b (Eenum k ty) 0.

    Lemma sc_exp_var : forall Γ Γty H b x cx ann,
        HasCaus Γ x cx ->
        sc_var_inv Γ H b cx ->
        sc_exp_inv Γ Γty H b (Evar x ann) 0.

    Lemma sc_exp_last : forall Γ Γty H b x cx ann,
        HasLastCaus Γ x cx ->
        sc_var_inv Γ H b cx ->
        sc_exp_inv Γ Γty H b (Elast x ann) 0.

    Lemma sc_exp_unop : forall Γ Γty H b op e1 ann,
        sc_exp_inv Γ Γty H b e1 0 ->
        sc_exp_inv Γ Γty H b (Eunop op e1 ann) 0.

    Lemma sc_exp_binop : forall Γ Γty H b op e1 e2 ann,
        sc_exp_inv Γ Γty H b e1 0 ->
        sc_exp_inv Γ Γty H b e2 0 ->
        sc_exp_inv Γ Γty H b (Ebinop op e1 e2 ann) 0.

    Lemma sc_exp_extcall : forall Γ Γty H b f es ann,
       (forall k, k < length (annots es) -> P_exps (sc_exp_inv Γ Γty H b) es k) ->
       sc_exp_inv Γ Γty H b (Eextcall f es ann) 0.

    Lemma sc_exp_fby : forall Γ Γty H b e0s es ann k,
        k < length ann ->
        P_exps (sc_exp_inv Γ Γty H b) e0s k ->
        sc_exp_inv Γ Γty H b (Efby e0s es ann) k.

    Lemma sc_exp_arrow : forall Γ Γty H b e0s es ann k,
        k < length ann ->
        P_exps (sc_exp_inv Γ Γty H b) e0s k ->
        P_exps (sc_exp_inv Γ Γty H b) es k ->
        sc_exp_inv Γ Γty H b (Earrow e0s es ann) k.

    Lemma sc_exp_when : forall Γ Γty H b es x tx cx b' ann k,
        NoDupMembers Γ ->
        k < length (fst ann) ->
        P_exps (sc_exp_inv Γ Γty H b) es k ->
        HasCaus Γ x cx ->
        sc_var_inv Γ H b cx ->
        sc_exp_inv Γ Γty H b (Ewhen es (x, tx) b' ann) k.

    Lemma sc_exp_merge : forall Γ Γty H b x cx tx es ann k,
        NoDupMembers Γ ->
        k < length (fst ann) ->
        HasCaus Γ x cx ->
        sc_var_inv Γ H b cx ->
        Forall (fun es => P_exps (sc_exp_inv Γ Γty H b) (snd es) k) es ->
        sc_exp_inv Γ Γty H b (Emerge (x, tx) es ann) k.

    Lemma sc_exp_case : forall Γ Γty H b e es d ann k,
        k < length (fst ann) ->
        sc_exp_inv Γ Γty H b e 0 ->
        Forall (fun es => P_exps (sc_exp_inv Γ Γty H b) (snd es) k) es ->
        LiftO True (fun d => P_exps (sc_exp_inv Γ Γty H b) d k) d ->
        sc_exp_inv Γ Γty H b (Ecase e es d ann) k.

    Lemma sc_exp_app : forall Γ Γty H b f es er ann k,
        wc_global G ->
        k < length ann ->
        (forall k0 : nat, k0 < length (annots es) -> P_exps (sc_exp_inv Γ Γty H b) es k0) ->
        sc_exp_inv Γ Γty H b (Eapp f es er ann) k.

    Lemma sc_exp' : forall Γ Γty H b e k,
        NoDupMembers Γ ->
        wc_global G ->
        wt_exp G Γty e ->
        wc_exp G Γ e ->
        k < numstreams e ->
        (forall cx, Is_free_left Γ cx k e -> sc_var_inv Γ H b cx) ->
        sc_exp_inv Γ Γty H b e k.

    Lemma sc_exp_equation : forall Γ Γty H b xs es k cx,
        wc_global G ->
        NoDup (map snd (idcaus_of_senv Γ)) ->
        NoDupMembers Γ ->
        k < length xs ->
        wt_equation G Γty (xs, es) ->
        wc_equation G Γ (xs, es) ->
        Sem.sem_equation G H b (xs, es) ->
        (forall cx, Is_free_left_list Γ cx k es -> sc_var_inv Γ H b cx) ->
        HasCaus Γ (nth k xs xH) cx ->
        sc_var_inv Γ H b cx.

more `mask` properties

    Lemma sc_var_inv_mask : forall Γ H b x r k,
        sc_var_inv Γ H b x ->
        sc_var_inv Γ (mask_hist k r H) (maskb k r b) x.

    Lemma sc_var_inv_unmask : forall Γ H b x r,
      (forall k : nat, sc_var_inv Γ (mask_hist k r H) (maskb k r b) x) ->
      sc_var_inv Γ H b x.

    Section sem_block_ck'.

      Section sem_scope.

        Context {A : Type}.

        Variable sem_block : static_env -> Sem.history -> A -> Prop.

        Inductive sem_scope_ck' (envS : list ident) : static_env -> Sem.history -> Stream bool -> (scope A) -> Prop :=
        | Sckscope : forall Γ Hi Hi' bs locs blks,
            dom Hi' (senv_of_decls locs) ->

            Forall (sem_last_decl (sem_exp G) Hi Hi' bs) locs ->

            sem_block (Γ ++ senv_of_decls locs) (Hi + Hi') blks ->

            Forall (fun x => sc_var_inv (senv_of_decls locs) (Hi + Hi') bs x) envS ->
            sem_scope_ck' envS Γ Hi bs (Scope locs blks).
      End sem_scope.

      Section sem_scope.

        Context {A : Type}.

        Variable sem_block : static_env -> A -> Prop.

        Variable must_def : ident -> Prop.
        Variable is_def : ident -> A -> Prop.

        Inductive sem_branch_ck' (envS : list ident) : static_env -> Sem.history -> Stream bool -> (branch A) -> Prop :=
        | Sckbranch : forall Γ Hi bs caus blks,
            sem_block (replace_idcaus caus Γ) blks ->
            (forall x, must_def x -> ~is_def x blks -> exists vs, sem_var Hi (Last x) vs /\ sem_var Hi (Var x) vs) ->

            Forall (fun cx => forall x ck vs, In (x, cx) caus -> HasClock Γ x ck -> sem_var Hi (Var x) vs -> sem_clock (var_history Hi) bs ck (abstract_clock vs)) envS ->
            sem_branch_ck' envS Γ Hi bs (Branch caus blks).
      End sem_scope.

      Inductive sem_block_ck' (envP : list ident) : static_env -> Sem.history -> Stream bool -> block -> Prop :=
      | Sckbeq : forall Γ Hi bs eq,
          sem_equation G Hi bs eq ->
          sem_block_ck' envP Γ Hi bs (Beq eq)
      | Sckreset : forall Γ Hi bs blocks er sr r,
          sem_exp G Hi bs er [sr] ->
          bools_of sr r ->
          (forall k, Forall (sem_block_ck' envP Γ (mask_hist k r Hi) (maskb k r bs)) blocks) ->
          sem_block_ck' envP Γ Hi bs (Breset blocks er)
      | Sckswitch:
        forall Γ Hi b ec branches sc,
          sem_exp G Hi b ec [sc] ->
          wt_streams [sc] (typeof ec) ->
          Forall (fun blks =>
                    exists Hi', when_hist (fst blks) Hi sc Hi'
                           /\ let bi := fwhenb (fst blks) b sc in
                             sem_branch_ck'
                               (fun Γ => Forall (sem_block_ck' envP Γ Hi' bi))
                               (fun x => Syn.Is_defined_in x (Bswitch ec branches))
                               (fun x => List.Exists (Syn.Is_defined_in x))
                               envP (map (fun '(x, a) => (x, ann_with_clock a Cbase)) Γ) Hi' bi (snd blks)) branches ->
          sem_block_ck' envP Γ Hi b (Bswitch ec branches)
      | SckautoWeak:
        forall Γ H bs ini oth states ck bs' stres0 stres1 stres,
          sem_clock (var_history H) bs ck bs' ->
          sem_transitions G H bs' (List.map (fun '(e, t) => (e, (t, false))) ini) (oth, false) stres0 ->
          fby stres0 stres1 stres ->
          Forall (fun state =>
                    let tag := fst (fst state) in
                    forall k, exists Hik, select_hist tag k stres H Hik
                                /\ let bik := fselectb tag k stres bs in
                                  sem_branch_ck'
                                    (fun Γ scope =>
                                       sem_scope_ck' (fun Γ Hi' blks =>
                                                        Forall (sem_block_ck' envP Γ Hi' bik) (fst blks)
                                                        /\ sem_transitions G Hi' bik (snd blks) (tag, false) (fselect absent (tag) k stres stres1)
                                         ) envP Γ Hik bik (snd scope))
                                    (fun x => Syn.Is_defined_in x (Bauto Weak ck (ini, oth) states))
                                    (fun x '(_, s) => Syn.Is_defined_in_scope (fun '(blks, _) => List.Exists (Syn.Is_defined_in x) blks) x s)
                                    envP (map (fun '(x, a) => (x, ann_with_clock a Cbase)) Γ) Hik bik (snd state)) states ->
          sem_block_ck' envP Γ H bs (Bauto Weak ck (ini, oth) states)
      | SckautoStrong:
        forall Γ H bs ini states ck bs' stres stres1,
          sem_clock (var_history H) bs ck bs' ->
          fby (const_stres bs' (ini, false)) stres1 stres ->
          Forall (fun state =>
                    let tag := fst (fst state) in
                    forall k, exists Hik, select_hist tag k stres H Hik
                                /\ let bik := fselectb tag k stres bs in
                                  sem_branch
                                    (fun scope => sem_transitions G Hik bik (fst scope) (tag, false) (fselect absent (tag) k stres stres1))
                                    (fun x => Syn.Is_defined_in x (Bauto Strong ck ([], ini) states))
                                    (fun x '(_, s) => Syn.Is_defined_in_scope (fun '(blks, _) => List.Exists (Syn.Is_defined_in x) blks) x s)
                                    Hik (snd state)
                 ) states ->
          Forall (fun state =>
                    let tag := fst (fst state) in
                    forall k, exists Hik, select_hist tag k stres1 H Hik
                                /\ let bik := fselectb tag k stres1 bs in
                                  sem_branch_ck'
                                    (fun Γ scope =>
                                       sem_scope_ck' (fun Γ Hi' blks => Forall (sem_block_ck' envP Γ Hi' bik) (fst blks)
                                         ) envP Γ Hik bik (snd scope))
                                    (fun x => Syn.Is_defined_in x (Bauto Strong ck ([], ini) states))
                                    (fun x '(_, s) => Syn.Is_defined_in_scope (fun '(blks, _) => List.Exists (Syn.Is_defined_in x) blks) x s)
                                    envP (map (fun '(x, a) => (x, ann_with_clock a Cbase)) Γ) Hik bik (snd state)
                 ) states ->
          sem_block_ck' envP Γ H bs (Bauto Strong ck ([], ini) states)
      | Scklocal:
        forall Γ Hi bs scope,
          sem_scope_ck' (fun Γ Hi' => Forall (sem_block_ck' envP Γ Hi' bs)) envP Γ Hi bs scope ->
          sem_block_ck' envP Γ Hi bs (Blocal scope).

    End sem_block_ck'.

    Ltac inv_branch :=
      match goal with
      | H:sem_branch_ck' _ _ _ _ _ _ _ _ |- _ => inv H; destruct_conjs; subst
      | _ => (Syn.inv_branch || Typ.inv_branch || Clo.inv_branch || Sem.inv_branch || CkSem.inv_branch)
      end.

    Ltac inv_scope :=
      match goal with
      | H:sem_scope_ck' _ _ _ _ _ _ |- _ => inv H; destruct_conjs; subst
      | _ => (Syn.inv_scope || Typ.inv_scope || Clo.inv_scope || Sem.inv_scope || CkSem.inv_scope)
      end.

    Ltac inv_block :=
      match goal with
      | H:sem_block_ck' _ _ _ _ _ |- _ => inv H
      | _ => (Syn.inv_block || Typ.inv_block || Clo.inv_block || Sem.inv_block || CkSem.inv_block)
      end.

    Lemma sem_block_sem_block_ck' : forall blk Γ Hi bs,
        sem_block G Hi bs blk ->
        sem_block_ck' [] Γ Hi bs blk.

    Lemma sem_block_ck'_sem_block : forall envP blk Γ Hi bs,
        sem_block_ck' envP Γ Hi bs blk ->
        sem_block G Hi bs blk.

    Lemma sem_block_ck'_Perm : forall xs ys blk Γ Hi bs,
        Permutation xs ys ->
        sem_block_ck' xs Γ Hi bs blk ->
        sem_block_ck' ys Γ Hi bs blk.

    Lemma sc_var_inv_unwhen : forall Γ Γ' tx tn sc Hi bs x,
        0 < length tn ->
        wt_stream sc (Tenum tx tn) ->
        (forall y ck, HasCaus Γ y x -> HasClock Γ y ck -> HasCaus Γ' y x /\ HasClock Γ' y Cbase) ->
        (forall y ck, HasCaus Γ y x -> HasClock Γ y ck -> sem_clock (var_history Hi) bs ck (abstract_clock sc)) ->
        (forall c, In c (seq 0 (length tn)) ->
              exists Hi',
                (forall y, HasCaus Γ y x -> FEnv.In (Var y) Hi')
                /\ when_hist c Hi sc Hi'
                /\ sc_var_inv Γ' Hi' (fwhenb c bs sc) x) ->
        (forall y, ~HasLastCaus Γ y x) ->
        sc_var_inv Γ Hi bs x.

    Lemma sc_var_inv_unselect : forall Γ Γ' tn sc Hi bs x,
        0 < tn ->
        SForall (fun v => match v with present (e, _) => e < tn | _ => True end) sc ->
        (forall y ck, HasCaus Γ y x -> HasClock Γ y ck -> HasCaus Γ' y x /\ HasClock Γ' y Cbase) ->
        (forall y ck, HasCaus Γ y x -> HasClock Γ y ck -> sem_clock (var_history Hi) bs ck (abstract_clock sc)) ->
        (forall c k, In c (seq 0 tn) ->
                exists Hi',
                  (forall y, HasCaus Γ y x -> FEnv.In (Var y) Hi')
                  /\ select_hist c k sc Hi Hi'
                  /\ sc_var_inv Γ' Hi' (fselectb c k sc bs) x) ->
        (forall y, ~HasLastCaus Γ y x) ->
        sc_var_inv Γ Hi bs x.

    Lemma sc_var_inv_local :
      forall Γ (locs : list (ident * (type * clock * ident * option (exp * ident)))) Hi Hi' bs cx,
        (forall x, InMembers x locs -> ~IsVar Γ x) ->
        dom_ub Hi Γ ->
        dom Hi' (senv_of_decls locs) ->
        (forall x, HasCaus Γ x cx \/ HasLastCaus Γ x cx -> sc_var_inv Γ Hi bs cx) ->
        (forall x, HasCaus (senv_of_decls locs) x cx \/ HasLastCaus (senv_of_decls locs) x cx ->
              sc_var_inv (senv_of_decls locs) (Hi + Hi') bs cx) ->
        sc_var_inv (Γ ++ senv_of_decls locs) (Hi + Hi') bs cx.

    Lemma sc_var_inv_branch :
      forall Γ caus Hi bs cx,
        (forall x, HasCaus Γ x cx \/ HasLastCaus Γ x cx -> sc_var_inv Γ Hi bs cx) ->
        (forall x ck vs, In (x, cx) caus -> HasClock Γ x ck -> sem_var Hi (Var x) vs ->
                    sem_clock (var_history Hi) bs ck (abstract_clock vs)) ->
        sc_var_inv (replace_idcaus caus Γ) Hi bs cx.

    Lemma sc_transitions' Γty Γ : forall Hi bs' trans def stres,
        wc_global G ->
        NoDupMembers Γ ->
        Forall (fun '(e, _) => wt_exp G Γty e) trans ->
        Forall (fun '(e, _) => wc_exp G Γ e /\ clockof e = [Cbase]) trans ->
        (forall cx, Exists (fun '(e, _) => Is_free_left Γ cx 0 e) trans -> sc_var_inv Γ Hi bs' cx) ->
        sem_transitions G Hi bs' trans def stres ->
        abstract_clock stres ≡ bs'.

    Lemma sc_var_inv_subclock Γ Γ' : forall Hi bs bs' cx ck,
        sem_clock (var_history Hi) bs ck bs' ->
        (forall x ck', HasClock Γ' x ck' -> HasClock Γ x ck /\ ck' = Cbase) ->
        (forall x, HasCaus Γ' x cx -> HasCaus Γ x cx) ->
        (forall x, HasLastCaus Γ' x cx -> HasLastCaus Γ x cx) ->
        sc_var_inv Γ Hi bs cx ->
        sc_var_inv Γ' Hi bs' cx.

    Lemma sc_scope {A} f_idcaus P_nd P_vd P_wt P_wc (P_blk1 P_blk2 : _ -> _ -> _ -> Prop) P_dep :
      forall envS locs (blks: A) Γ Γty xs Hi bs cy,
        wc_global G ->
        NoDup (map snd (idcaus_of_senv Γ ++ idcaus_of_scope f_idcaus (Scope locs blks))) ->
        NoDupMembers Γ ->
        NoDupScope P_nd (map fst Γ) (Scope locs blks) ->
        VarsDefinedCompScope P_vd (Scope locs blks) xs ->
        incl xs (map fst Γ) ->
        wt_scope P_wt G Γty (Scope locs blks) ->
        wc_env (idck Γ) ->
        wc_scope P_wc G Γ (Scope locs blks) ->
        sem_scope_ck' P_blk1 envS Γ Hi bs (Scope locs blks) ->
        dom_ub Hi Γ ->
        (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx ->
                 depends_on_scope P_dep Γ cy cx (Scope locs blks) -> sc_var_inv Γ Hi bs cx) ->
        (forall cx, In cx (map snd (idcaus_of_scope f_idcaus (Scope locs blks))) ->
               depends_on_scope P_dep Γ cy cx (Scope locs blks) -> In cx envS) ->
        (forall Γ Γty xs Hi,
            NoDup (map snd (idcaus_of_senv Γ ++ f_idcaus blks)) ->
            NoDupMembers Γ ->
            P_nd (map fst Γ) blks ->
            P_vd blks xs ->
            incl xs (map fst Γ) ->
            P_wt Γty blks ->
            wc_env (idck Γ) ->
            P_wc Γ blks ->
            P_blk1 Γ Hi blks ->
            dom_ub Hi Γ ->
            (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx ->
                     P_dep Γ cy cx blks -> sc_var_inv Γ Hi bs cx) ->
            (forall cx, In cx (map snd (f_idcaus blks)) ->
                   P_dep Γ cy cx blks -> In cx envS) ->
            (forall y, In y xs -> HasCaus Γ y cy -> sc_var_inv Γ Hi bs cy)
            /\ P_blk2 Γ Hi blks) ->
        (forall y, In y xs -> HasCaus Γ y cy -> sc_var_inv Γ Hi bs cy)
        /\ sem_scope_ck' P_blk2 (cy::envS) Γ Hi bs (Scope locs blks).

    Lemma sc_branch {A} f_idcaus P_nd P_vd P_wt P_wc (P_blk1 P_blk2 : _ -> _ -> Prop) P_dep must_def is_def :
      forall envS caus (blks: A) Γ xs Hi bs cy,
        wc_global G ->
        NoDup (map snd (idcaus_of_senv Γ ++ idcaus_of_branch f_idcaus (Branch caus blks))) ->
        NoDupMembers Γ ->
        NoDupBranch P_nd (Branch caus blks) ->
        VarsDefinedCompBranch P_vd (Branch caus blks) xs ->
        incl xs (map fst Γ) ->
        wt_branch P_wt (Branch caus blks) ->
        wc_env (idck Γ) ->
        wc_branch P_wc (Branch caus blks) ->
        sem_branch_ck' P_blk1 must_def is_def envS Γ Hi bs (Branch caus blks) ->
        dom_ub Hi Γ ->
        (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx ->
                 depends_on_branch P_dep Γ cy cx (Branch caus blks) -> sc_var_inv Γ Hi bs cx) ->
        (forall cx, In cx (map snd (idcaus_of_branch f_idcaus (Branch caus blks))) ->
               depends_on_branch P_dep Γ cy cx (Branch caus blks) -> In cx envS) ->
        (let Γ := replace_idcaus caus Γ in
         NoDup (map snd (idcaus_of_senv Γ ++ f_idcaus blks)) ->
         NoDupMembers Γ ->
         P_nd blks ->
         P_vd blks xs ->
         incl xs (map fst Γ) ->
         P_wt blks ->
         wc_env (idck Γ) ->
         P_wc blks ->
         P_blk1 Γ blks ->
         dom_ub Hi Γ ->
         (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx ->
                  P_dep Γ cy cx blks -> sc_var_inv Γ Hi bs cx) ->
         (forall cx, In cx (map snd (f_idcaus blks)) ->
                P_dep Γ cy cx blks -> In cx envS) ->
         (forall y, In y xs -> HasCaus Γ y cy -> sc_var_inv Γ Hi bs cy)
         /\ P_blk2 Γ blks) ->
        (forall y, In y xs -> HasCaus Γ y cy -> sc_var_inv Γ Hi bs cy)
        /\ sem_branch_ck' P_blk2 must_def is_def (cy::envS) Γ Hi bs (Branch caus blks).

    Lemma sc_block : forall envP blk xs Γ Γty Hi bs cy,
        wc_global G ->
        NoDup (map snd (idcaus_of_senv Γ ++ idcaus_of_locals blk)) ->
        NoDupMembers Γ ->
        NoDupLocals (map fst Γ) blk ->
        VarsDefinedComp blk xs ->
        incl xs (map fst Γ) ->
        wt_block G Γty blk ->
        wc_env (idck Γ) ->
        wc_block G Γ blk ->
        sem_block_ck' envP Γ Hi bs blk ->
        dom_ub Hi Γ ->
        (forall x cx, HasCaus Γ x cx \/ HasLastCaus Γ x cx -> depends_on Γ cy cx blk -> sc_var_inv Γ Hi bs cx) ->
        (forall cx, In cx (map snd (idcaus_of_locals blk)) -> depends_on Γ cy cx blk -> In cx envP) ->
        (forall y, In y xs -> HasCaus Γ y cy -> sc_var_inv Γ Hi bs cy)
        /\ sem_block_ck' (cy::envP) Γ Hi bs blk.

    Lemma sem_node_sc_vars :
      forall n H b,
        wc_global G ->
        wt_node G n ->
        wc_node G n ->
        node_causal n ->
        dom H (senv_of_ins (n_in n) ++ senv_of_decls (n_out n)) ->
        Forall (sc_var_inv (senv_of_ins (n_in n) ++ senv_of_decls (n_out n)) H b) (map snd (idcaus (n_in n))) ->
        Forall (sem_last_decl (sem_exp G) (FEnv.empty _) H b) (n_out n) ->
        Sem.sem_block G H b (n_block n) ->
        sc_vars (senv_of_ins (n_in n) ++ senv_of_decls (n_out n)) H b /\
        sem_block_ck' (map snd (idcaus (n_in n) ++ idcaus_of_decls (n_out n) ++ idcaus_of_locals (n_block n)))
                      (senv_of_ins (n_in n) ++ senv_of_decls (n_out n))
                      H b (n_block n).

    Lemma sem_node_restrict {prefs2} : forall (n : @node complete prefs2) H b xs ys,
        let Γ := senv_of_ins (n_in n) ++ senv_of_decls (n_out n) in
        Forall (fun '(_, (_, ck, _, o)) => LiftO True (fun '(e, _) => wc_exp G Γ e /\ clockof e = [ck]) o) (n_out n) ->
        wc_block G Γ (n_block n) ->
        Forall2 (fun x => sem_var H (Var x)) (map fst (n_in n)) xs ->
        Forall2 (fun x => sem_var H (Var x)) (map fst (n_out n)) ys ->
        Forall (sem_last_decl (sem_exp G) (FEnv.empty (Stream svalue)) H b) (n_out n) ->
        Sem.sem_block G H b (n_block n) ->
        let H' := restrict H Γ in
        dom H' Γ /\
        Forall2 (fun x => sem_var H' (Var x)) (map fst (n_in n)) xs /\
        Forall2 (fun x => sem_var H' (Var x)) (map fst (n_out n)) ys /\
        Forall (sem_last_decl (sem_exp G) (FEnv.empty (Stream svalue)) H' b) (n_out n) /\
        Sem.sem_block G H' b (n_block n).

    Lemma sc_var_inv_intro {prefs2} : forall (n : @node PSyn prefs2) H xs,
        node_causal n ->
        Forall2 (fun x => sem_var H (Var x)) (idents (n_in n)) xs ->
        Forall2 (fun xc => sem_clock (var_history H) (clocks_of xs) (snd xc)) (map (fun '(x, (_, ck, _)) => (x, ck)) (n_in n)) (map abstract_clock xs) ->
        Forall (sc_var_inv (senv_of_ins (n_in n) ++ senv_of_decls (n_out n)) H (clocks_of xs)) (map snd (idcaus (n_in n))).

    Fact wc_exp_Is_free_left : forall Γ e x k,
        wc_exp G Γ e ->
        Is_free_left Γ x k e ->
        In x (map snd (idcaus_of_senv Γ)).

    Lemma sc_exp'' : forall Γ Γty H b e vs,
        wc_global G ->
        NoDupMembers Γ ->
        sc_vars Γ H b ->

        wt_exp G Γty e ->
        wc_exp G Γ e ->
        Sem.sem_exp G H b e vs ->
        Forall2 (sem_clock (var_history H) b) (clockof e) (map abstract_clock vs).

    Corollary sc_exps'' : forall Γ Γty H b es vss,
        wc_global G ->
        NoDupMembers Γ ->
        sc_vars Γ H b ->

        Forall (wt_exp G Γty) es ->
        Forall (wc_exp G Γ) es ->
        Forall2 (Sem.sem_exp G H b) es vss ->
        Forall2 (sem_clock (var_history H) b) (clocksof es) (map abstract_clock (concat vss)).

    Lemma sc_transitions'' Γty Γ : forall Hi bs' trans def stres,
        wc_global G ->
        NoDupMembers Γ ->
        Forall (fun '(e, _) => wt_exp G Γty e) trans ->
        Forall (fun '(e, _) => wc_exp G Γ e /\ clockof e = [Cbase]) trans ->
        sc_vars Γ Hi bs' ->
        sem_transitions G Hi bs' trans def stres ->
        abstract_clock stres ≡ bs'.

  End sc_inv.

  Section sem_ck.
    Context {PSyn : list decl -> block -> Prop}.
    Context {prefs : PS.t}.
    Variable (G : @global complete prefs).

    Hypothesis HwcG : wc_global G.

    Hypothesis Hnode : forall f ins outs,
        sem_node G f ins outs ->
        sem_clock_inputs G f ins ->
        sem_node_ck G f ins outs.

    Lemma sem_exp_sem_exp_ck : forall Γ Γty H bs e vs,
        NoDupMembers Γ ->
        NoDup (map snd (idcaus_of_senv Γ)) ->
        sc_vars Γ H bs ->
        wt_exp G Γty e ->
        wc_exp G Γ e ->
        Sem.sem_exp G H bs e vs ->
        sem_exp_ck G H bs e vs.

    Corollary sem_equation_sem_equation_ck : forall Γ Γty H bs equ,
        NoDupMembers Γ ->
        NoDup (map snd (idcaus_of_senv Γ)) ->
        sc_vars Γ H bs ->
        wt_equation G Γty equ ->
        wc_equation G Γ equ ->
        Sem.sem_equation G H bs equ ->
        sem_equation_ck G H bs equ.

    Corollary sem_transitions_sem_transitions_ck : forall Γ Γty H bs trans def stres,
        NoDupMembers Γ ->
        NoDup (map snd (idcaus_of_senv Γ)) ->
        sc_vars Γ H bs ->
        Forall (fun '(e, _) => wt_exp G Γty e) trans ->
        Forall (fun '(e, _) => wc_exp G Γ e) trans ->
        Sem.sem_transitions G H bs trans def stres ->
        sem_transitions_ck G H bs trans def stres.

    Hint Resolve EqStrel EqStrel_Reflexive : core.

    Fact idcaus_of_senv_when_NoDup : forall ck Γ,
        NoDup (map snd (idcaus_of_senv Γ)) ->
        NoDup (map snd (idcaus_of_senv (map_filter (fun '(x, e0) => if clo e0 ==b ck then Some (x, ann_with_clock e0 Cbase) else None) Γ))).

    Lemma sem_scope_sem_scope_ck {A} f_idcaus P_nd P_wt P_wc P_blk1 (P_blk2: _ -> _ -> Prop) :
      forall envP locs (blk: A) Γty Γck Γ' Hi bs,
        NoDupMembers Γty ->
        NoDupMembers Γck ->
        NoDup (map snd (idcaus_of_senv Γck ++ idcaus_of_scope f_idcaus (Scope locs blk))) ->
        NoDupScope P_nd (map fst Γty) (Scope locs blk) ->
        (forall x ty, HasType Γck x ty -> HasType Γty x ty) ->
        incl (map snd (idcaus_of_senv Γck ++ idcaus_of_scope f_idcaus (Scope locs blk))) envP ->
        dom_ub Hi Γty ->
        sc_vars Γck Hi bs ->
        wt_scope P_wt G Γty (Scope locs blk) ->
        wc_env (idck Γck) ->
        Forall (fun '(_, a) => wc_clock (idck Γck) (clo a)) Γ' ->
        wc_scope P_wc G Γck (Scope locs blk) ->
        sem_scope_ck' G P_blk1 envP Γ' Hi bs (Scope locs blk) ->
        (forall Γty Γck Γ' Hi,
            NoDupMembers Γty ->
            NoDupMembers Γck ->
            NoDup (map snd (idcaus_of_senv Γck ++ f_idcaus blk)) ->
            P_nd (map fst Γty) blk ->
            (forall x ty, HasType Γck x ty -> HasType Γty x ty) ->
            incl (map snd (idcaus_of_senv Γck ++ f_idcaus blk)) envP ->
            dom_ub Hi Γty ->
            sc_vars Γck Hi bs ->
            P_wt Γty blk ->
            wc_env (idck Γck) ->
            Forall (fun '(_, a) => wc_clock (idck Γck) (clo a)) Γ' ->
            P_wc Γck blk ->
            P_blk1 Γ' Hi blk ->
            P_blk2 Hi blk) ->
        sem_scope_ck (sem_exp_ck G) P_blk2 Hi bs (Scope locs blk).

    Lemma sem_branch_sem_branch_ck {A} f_idcaus P_nd P_wt P_wc P_blk1 (P_blk2: _ -> Prop) must_def is_def :
      forall envP caus (blk: A) Γty Γck Γ' Hi bs,
        NoDupMembers Γty ->
        NoDupMembers Γck ->
        NoDup (map snd (idcaus_of_senv Γck ++ idcaus_of_branch f_idcaus (Branch caus blk))) ->
        NoDupBranch P_nd (Branch caus blk) ->
        (forall x ty, HasType Γck x ty -> HasType Γty x ty) ->
        incl (map snd (idcaus_of_senv Γck ++ idcaus_of_branch f_idcaus (Branch caus blk))) envP ->
        dom_ub Hi Γty ->
        sc_vars Γck Hi bs ->
        wt_branch P_wt (Branch caus blk) ->
        wc_env (idck Γck) ->
        Forall (fun '(_, a) => wc_clock (idck Γck) (clo a)) Γ' ->
        wc_branch P_wc (Branch caus blk) ->
        sem_branch_ck' P_blk1 must_def is_def envP Γ' Hi bs (Branch caus blk) ->
        (forall Γ',
            NoDup (map snd (idcaus_of_senv Γck ++ f_idcaus blk)) ->
            P_nd blk ->
            (forall x ty, HasType Γck x ty -> HasType Γty x ty) ->
            incl (map snd (idcaus_of_senv Γck ++ f_idcaus blk)) envP ->
            sc_vars Γck Hi bs ->
            P_wt blk ->
            wc_env (idck Γck) ->
            Forall (fun '(_, a) => wc_clock (idck Γck) (clo a)) Γ' ->
            P_wc blk ->
            P_blk1 Γ' blk ->
            P_blk2 blk) ->
        sem_branch_ck P_blk2 (Branch caus blk).

    Local Ltac simpl_ndup Hnd :=
      simpl in *;
      try rewrite app_nil_r in Hnd; repeat rewrite map_app.

    Lemma sem_block_sem_block_ck : forall envP blk Γty Γck Γ' Hi bs,
        NoDupMembers Γty ->
        NoDupMembers Γck ->
        NoDup (map snd (idcaus_of_senv Γck ++ idcaus_of_locals blk)) ->
        NoDupLocals (map fst Γty) blk ->
        (forall x ty, HasType Γck x ty -> HasType Γty x ty) ->
        incl (map snd (idcaus_of_senv Γck ++ idcaus_of_locals blk)) envP ->
        dom_ub Hi Γty ->
        sc_vars Γck Hi bs ->
        wt_block G Γty blk ->
        wc_env (idck Γck) ->
        Forall (fun '(_, a) => wc_clock (idck Γck) (clo a)) Γ' ->
        wc_block G Γck blk ->
        sem_block_ck' G envP Γ' Hi bs blk ->
        sem_block_ck G Hi bs blk.

  End sem_ck.

  Theorem sem_node_sem_node_ck {prefs} :
    forall (G : @global complete prefs),
      wt_global G ->
      wc_global G ->
      Forall node_causal (nodes G) ->
      forall f ins outs,
        Sem.sem_node G f ins outs ->
        sem_clock_inputs G f ins ->
        sem_node_ck G f ins outs.

End LCLOCKCORRECTNESS.

Module LClockCorrectnessFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (Senv : STATICENV Ids Op OpAux Cks)
       (Syn : LSYNTAX Ids Op OpAux Cks Senv)
       (Typ : LTYPING Ids Op OpAux Cks Senv Syn)
       (Clo : LCLOCKING Ids Op OpAux Cks Senv Syn)
       (LCA : LCAUSALITY Ids Op OpAux Cks Senv Syn)
       (Lord : LORDERED Ids Op OpAux Cks Senv Syn)
       (CStr : COINDSTREAMS Ids Op OpAux Cks)
       (Sem : LSEMANTICS Ids Op OpAux Cks Senv Syn Lord CStr)
       (CkSem : LCLOCKEDSEMANTICS Ids Op OpAux Cks Senv Syn Clo Lord CStr Sem)
<: LCLOCKCORRECTNESS Ids Op OpAux Cks Senv Syn Typ Clo LCA Lord CStr Sem CkSem.
  Include LCLOCKCORRECTNESS Ids Op OpAux Cks Senv Syn Typ Clo LCA Lord CStr Sem CkSem.
End LClockCorrectnessFun.