Module SliceObs

Lemmas related to the observable nodes validator.

Require Import Bool.
Require Import BinPos.
Require Import BinNat.
Require Import List.
Require Import TheoryList.
Require Import Arith.

Require Import Coqlib.
Require Import RTL.
Require Import Maps.
Require Import Errors.
Require Import Op.
Require Import Registers.

Require Import UtilTacs.
Require Import UtilLemmas.
Require Import UtilBase.
Require Import RTLWfFunction.
Require Import RTLPaths.
Require Import SliceRegVint.

Require Import Utils.
Require Import Scope.
Require Import SliceObs.
Require Import SliceGen.

Local Open Scope positive_scope.

Section DOBS.

  Variable f : function.
  Variable nc : t_criterion.
  Variable slice_nodes : list node.
  Variable s_dobs : dobsT.
  Variable dexit : PTree.t N.

  Definition nobsT := PTree.t (nat * nat * node).
  Definition nobs : nobsT := PTree.map (fun n d_dc_o => let '(d, dc, o) := d_dc_o in
                                                        (Nnat.nat_of_N d, Nnat.nat_of_N dc, o)) s_dobs.
  Definition nexit : PTree.t nat := PTree.map (fun n dx => Nnat.nat_of_N dx) dexit.

Properties to be checked.

  Record checked_nobs (f : function) (nc : t_criterion) (exit_n : node) (slice_nodes : list node) (nobs : nobsT) (nexit : PTree.t nat) : Prop := {
    checked_nobs_refl: forall n, In n slice_nodes <-> exists dc, nobs ! n = Some (0%nat, dc, n);
    checked_nobs_f_In: forall n, In n slice_nodes -> f_In n f;
    checked_nobs_none_not_in_slice: forall n, nobs ! n = None -> ~ In n slice_nodes;
    checked_nobs_ex_succ: forall n d dc o, nobs ! n = Some (S d, dc, o) -> exists s, succ_node f n s /\ exists dc', nobs ! s = Some (d, dc', o);
    checked_nobs_minus_one: forall n d dc o, nobs ! n = Some (S d, dc, o) -> forall s d' dc' o', succ_node f n s -> nobs ! s = Some (d', dc', o') -> (d' >= d)%nat;
    checked_nobs_none_succ_none: forall n i, nobs ! n = None -> (fn_code f) ! n = Some i -> forall s, In s (successors_instr i) -> nobs ! s = None;
    checked_nobs_some_succ_same: forall n d dc i o, nobs ! n = Some (S d, dc, o) -> (fn_code f) ! n = Some i -> forall s, In s (successors_instr i) -> exists d', exists dc', nobs ! s = Some (d', dc', o);
    checked_nobs_zero_refl: forall n dc o, nobs ! n = Some (0%nat, dc, o) -> n = o;
    checked_nobs_control: forall n i, (fn_code f) ! n = Some i -> forall s1 s2 d dc o, In s1 (successors_instr i) -> In s2 (successors_instr i) -> nobs ! s1 = Some (d, dc, o) -> nobs ! s2 = None -> In n slice_nodes;
    checked_nobs_jumptable: forall n arg tbl, (fn_code f) ! n = Some (Ijumptable arg tbl) -> In n slice_nodes;

    checked_nexit_exit: nexit ! exit_n = Some 0%nat;
    checked_has_nexit: forall n, f_In n f -> exists dx, nexit ! n = Some dx;
    checked_nexit_ex_succ: forall n dx, f_In n f -> nexit ! n = Some (S dx) -> exists s, succ_node f n s /\ nexit ! s = Some dx;
    checked_nexit_zero_refl: forall n, f_In n f -> nexit ! n = Some (0%nat) -> n = exit_n;
    checked_nexit_minus_one: forall n dx, nexit ! n = Some (S dx) -> forall s dx', succ_node f n s -> nexit ! s = Some (dx') -> (dx' >= dx)%nat

  }.

  Variable exit_n : node.
  Hypothesis exit_no_succ:
    forall s, ~ succ_node f exit_n s.

  Hypothesis CHECK: s_dobs_checker f nc exit_n slice_nodes s_dobs dexit = true.

  Lemma checked_nobs_reaches_nc:
    forall
      dc n d o
      (DOBS: nobs ! n = Some (d, dc, o)),
      reaches f n nc.

Proof.

    induction dc; intros.
    unfold nobs in DOBS.
    rewrite PTree.gmap in DOBS; unfold option_map in DOBS.
    optDecN DOBS NOBS; trim.
    destruct p as [[d' dc'] o'].
    unfolds in CHECK.
    boolrw.
    destruct CHECK as [[[[[[IN_NODES DOBS_IN] NC_ZERO] IN_ENTRY] IN_NC] IN_EXIT] FOLD].
    unfold checker_cond_in_slice in FOLD.
    rewrite forallb_forall in IN_NODES.
    apply option_N_N_node_beq_eq in NC_ZERO.
    eapply forall_ptree_true with (i := n) in DOBS_IN; eauto.
    unfold Pmem in DOBS_IN.
    optDecN DOBS_IN INST; trim.
    apply ptree_forall with (i := n) (x := i) in FOLD; auto.
    rewrite NOBS in FOLD.
    optDecN FOLD IN_SL.
    optDec FOLD.
    subst n. apply r_refl.
    intro; trim.
    boolrw.
    decs FOLD.
    inv_clear DOBS.
    projInv H4. lia2.
    boolrw.
    destruct FOLD as (DEXIT & (JUMP & CONTROL) & CONDS).
    destruct CONDS as [[[[A B] C] D] E].
    projInv A; projInv B.
    inv_clear DOBS.
    lia2.

    unfolds in CHECK.
    boolrw.
    destruct CHECK as [[[[[[IN_NODES DOBS_IN] NC_ZERO] IN_ENTRY] IN_NC] IN_EXIT] FOLD].
    unfold checker_cond_in_slice in FOLD.
    rewrite forallb_forall in IN_NODES.
    apply option_N_N_node_beq_eq in NC_ZERO.
    unfold nobs in DOBS.
    rewrite PTree.gmap in DOBS; unfold option_map in DOBS.
    optDecN DOBS DOBS'; trim.
    destruct p as [[d' dc'] o'].
    inv_clear DOBS.
    subst d o'.
    eapply forall_ptree_true with (i := n) in DOBS_IN; eauto.
    unfold Pmem in DOBS_IN.
    optDecN DOBS_IN INST; trim.
    apply ptree_forall with (i := n) (x := i) in FOLD; auto.
    rewrite DOBS' in FOLD.
    optDecN FOLD IN_SL.
    optDec FOLD.
    subst n.
    apply r_refl; trim.
    boolrw.
    destruct FOLD as (DEXIT & ((A & B) & C) & D).
    unfolds in D.
    rewrite existsb_exists in D.
    destruct D as [s [SUCC DOBSS]].
    optDecN DOBSS DOBSS'; trim.
    destruct p as [[d dc''] o'].
    apply Neqb_eq in DOBSS. subst dc''.
    projInv A; subst d'.
    projInv B.
    apply r_succ with (n' := s).
    gen (IHdc s (Nnat.nat_of_N d) o') as IHs.
    apply IHs.
    unfold nobs.
    rewrite PTree.gmap; unfold option_map.
    rewrite DOBSS'.
    repeat f_equal.
    lia2.
    eexists; eauto.

    boolrw.
    destruct FOLD as (DEXIT & (JUMP & CONTROL) & (((A & B) & C) & D) & E).
    unfolds in E.
    apply existsb_exists in E.
    destruct E as [s [SUCC DOBSS]].
    optDecN DOBSS DOBSS'; trim.
    destruct p as [[d dc''] o'].
    boolrw.
    destruct DOBSS as [EQD EQDC].
    apply Neqb_eq in EQD.
    apply Neqb_eq in EQDC.
    subst d dc''.
    apply r_succ with (n' := s).
    apply IHdc with (d := ((Nnat.nat_of_N d') - 1)%nat) (o := o).
    unfold nobs.
    rewrite PTree.gmap; unfold option_map.
    rewrite DOBSS'.
    unfolds in D.
    rewrite forallb_forall in D.
    apply D in SUCC.
    rewrite DOBSS' in SUCC.
    boolrw.
    decs SUCC.
    apply Peqb_eq in H2; subst o'.
    repeat f_equal; lia2.
    eexists; eauto.
  Qed.

  Lemma dobs_some_f_In:
    forall
      n p
      (DOBS: s_dobs ! n = Some p),
      f_In n f.

Proof.

    intros.
    unfolds in CHECK.
    boolrw.
    destruct CHECK as [[[[[[IN_NODES DOBS_IN] NC_ZERO] IN_ENTRY] IN_NC] IN_EXIT] FOLD].
    unfold checker_cond_in_slice in FOLD.
    rewrite forallb_forall in IN_NODES.
    apply option_N_N_node_beq_eq in NC_ZERO.
    eapply forall_ptree_true with (i := n) in DOBS_IN; eauto.
    unfold Pmem in DOBS_IN.
    optDecN DOBS_IN INST; trim.
  Qed.

Proof that the checker ensures the required properties.

Lemma checked_nobs_wf:
checked_nobs f nc exit_n slice_nodes nobs nexit.

Proof.

    dup CHECK CHECK'.
    unfolds in CHECK.
    boolrw.
    destruct CHECK as [[[[[[IN_NODES DOBS_IN] NC_ZERO] IN_ENTRY] IN_NC] IN_EXIT] FOLD].
    unfold checker_cond_in_slice in FOLD.
    rewrite forallb_forall in IN_NODES.
    apply option_N_N_node_beq_eq in NC_ZERO.
    constructor; unfold nobs in *; try rewrite PTree.gmap in *; unfold option_map in *.
    Case "checked_nobs_refl".
      intros; split.
      SCase "->".
        introsv IN_SL.
        rewrite PTree.gmap; unfold option_map.
        dup IN_SL PMEM.
        apply IN_NODES in PMEM.
        unfold Pmem in PMEM.
        optDecN PMEM GET; trim.
        eapply forall_ptree_true with (i := n) (x := i) in FOLD; auto.
        rewrite <- mem_iff_In in IN_SL.
        rewrite IN_SL in FOLD.
        optDec FOLD.
        boolrw.
        destruct FOLD as (DEXIT & FOLD).
        subst n.
        apply option_N_N_node_beq_eq in FOLD; auto.
        rewrite FOLD; auto.
        eexists; eauto.
        optDecN FOLD DOBS_ENTRY; trim.
        destruct p. destruct p.
        boolrw.
        destruct FOLD as [DEXIT [[[A B] C] D]].
        projInv C. subst n1.
        projInv A. subst n2.
        eexists; eauto.
        boolrw. destruct FOLD; trim.
      SCase "<-".
        introsv GET.
        rewrite PTree.gmap in GET; unfold option_map in GET.
        destruct GET as [dc GET].
        optDecN GET GET'; trim.
        inversion GET; clear GET.
        destruct p as [[d dc'] p].
        inversion H0; clear H0.
        apply nat_of_N_eq_0 in H1. subst d n dc.
        eapply forall_ptree_true with (i := p) in DOBS_IN; eauto.
        unfold Pmem in DOBS_IN. optDecN DOBS_IN INST; trim.
        eapply forall_ptree_true with (i := p) (x := i) in FOLD; eauto.
        optDecN FOLD MEM.
        rewrite mem_iff_In in MEM.
        simpl; auto.
        rewrite GET' in FOLD.
        boolrw.
        destruct FOLD as [DEXIT [JUMP [[CONTROL C1] C2]]].
        destruct CONTROL as [[LTDC LEDC] EQ].
        rewrite negb_true_iff in EQ.
        projInv EQ.
    Case "checked_nobs_f_In".
      introsv IN_SL.
      apply Pmem_f_In.
      apply IN_NODES; auto.
    Case "checked_nobs_none_not_in_slice".
      intros.
      rewrite PTree.gmap in H; unfold option_map in H.
      optDecN H DOBS; trim.
      intro IN_SLICE.
      dup IN_SLICE IN_SL.
      apply IN_NODES in IN_SLICE.
      unfold Pmem in IN_SLICE.
      optDecN IN_SLICE INST; trim.
      eapply forall_ptree_true with (i := n) in FOLD; eauto.
      apply <- mem_iff_In in IN_SL.
      rewrite IN_SL in FOLD.
      optDec FOLD; trim.
      rewrite DOBS in FOLD.
      boolrw. destruct FOLD; trim.
    Case "checked_nobs_ex_succ".
      intros.
      rewrite PTree.gmap in H; unfold option_map in H.
      optDecN H DOBS; trim.
      inversion H; clear H.
      destruct p as [[d' dc'] o'].
      inversion H1; clear H1. subst o' dc.
      dup DOBS FIN.
      apply dobs_some_f_In in FIN.
      apply f_In_ex in FIN.
      destruct FIN as [i INST].
      eapply forall_ptree_true with (i := n) (x := i) in FOLD; eauto.
      optDecN FOLD IN_SL.
      optDec FOLD.
      boolrw.
      destruct FOLD as [DEXIT FOLD].
      subst n.
      apply option_N_N_node_beq_eq in FOLD.
      rewrite FOLD in DOBS.
      inv DOBS; trim.
      rewrite DOBS in FOLD.
      boolrw.
      destruct FOLD as [DEXIT [[[DEQ DCLT] OEQ] COND]].
      projInv DEQ. subst d'.
      lia2.
      rewrite DOBS in FOLD.
      boolrw.
      destruct FOLD as [DEXIT [JUMP [[CONTROL C1] C2]]].
      unfolds in C2.
      rewrite existsb_exists in C2.
      destruct C2 as [s [SUCC DOBSS]].
      optDecN DOBSS DOBSS'; trim.
      destruct p as [[d'' dc''] o'].
      exists s.
      split.
      eexists; eauto.
      rewrite PTree.gmap; unfold option_map.
      rewrite DOBSS'.
      boolrw.
      destruct DOBSS.
      apply Neqb_eq in H. apply Neqb_eq in H1.
      subst d'' dc''.
      unfolds in C1.
      rewrite forallb_forall in C1.
      apply C1 in SUCC.
      rewrite DOBSS' in SUCC.
      boolrw.
      decs SUCC.
      apply Peqb_eq in H2. subst o'.
      eexists.
      repeat f_equal.
      lia2.
    Case "checked_nobs_minus_one".
      introsv DOBSN SUCC DOBSS.
      rewrite PTree.gmap in *; unfold option_map in *.
      optDecN DOBSN DOBS; trim.
      optDecN DOBSS DOBS'; trim.
      destruct p as [[d'' dc''] o''].
      destruct p0 as [[d''' dc'''] o'''].
      inversion DOBSN. inversion DOBSS.
      clear DOBSN DOBSS.
      subst o'' o''' d' dc'.
      dup SUCC S.
      apply succ_f_In in S. apply f_In_ex in S. destruct S as [i INST].
      apply forall_ptree_true with (i := n) (x := i) in FOLD; eauto.
      rewrite DOBS in FOLD.
      optDecN FOLD IN_SL.
      optDec FOLD.
      boolrw.
      destruct FOLD as [DEXIT FOLD].
      subst n.
      apply option_N_N_node_beq_eq in FOLD.
      inv FOLD; trim.
      boolrw.
      destruct FOLD as [DEXIT [[[DEQ DCLT] OEQ] COND2]].
      projInv DEQ; subst d''.
      lia2.
      boolrw.
      destruct FOLD as [DEXIT [[JUMP CONTROL] [[[[P1 P2] P3] C1] C2]]].
      unfolds in C1.
      rewrite forallb_forall in C1.
      unfolds in SUCC. destruct SUCC as [i' [INST' SUCCS]].
      rewrite INST in INST'. inversion INST'; clear INST'; subst i'.
      apply C1 in SUCCS.
      rewrite DOBS' in SUCCS.
      boolrw.
      decs SUCCS.
      projInv H4. lia2.
    Case " checked_nobs_none_succ_none".
      introsv DOBS INST SUCC.
      rewrite PTree.gmap in *; unfold option_map in *.
      optDecGN DOBSS; trim.
      exfalso.
      destruct p as [[d' dc'] o'].
      optDecN DOBS DOBSN; trim.
      apply forall_ptree_true with (i := n) (x := i) in FOLD; eauto.
      rewrite DOBSN in FOLD.
      optDecN FOLD IN_SL.
      optDec FOLD; trim.
      boolrw. destruct FOLD; trim.
      boolrw.
      destruct FOLD as [DEXIT [JUMP CNONE]].
      unfolds in CNONE.
      rewrite forallb_forall in CNONE.
      apply CNONE in SUCC.
      rewrite DOBSS in SUCC.
      apply option_N_N_node_beq_eq in SUCC; trim.
    Case "checked_nobs_some_succ_same".
      introsv DOBS INST SUCC.
      rewrite PTree.gmap in DOBS; unfold option_map in DOBS.
      rewrite PTree.gmap; unfold option_map.
      optDecN DOBS DOBSN; trim.
      destruct p as [[d' dc'] o'].
      apply forall_ptree_true with (i := n) (x := i) in FOLD; eauto.
      rewrite DOBSN in FOLD.
      inv_clear DOBS. subst dc o'.
      optDecN FOLD IN_SL.
      optDec FOLD.
      boolrw. destruct FOLD as [DEXIT FOLD].
      subst nc.
      rewrite DOBSN in NC_ZERO. inv_clear NC_ZERO.
      subst d' dc'; trim.
      boolrw.
      decs FOLD. projInv H2. lia2.
      boolrw.
      destruct FOLD as [DEXIT [[JUMP CONTROL] CONDS]].
      destruct CONDS as [[A C1] C2].
      unfolds in C2.
      rewrite existsb_exists in C2.
      destruct C2 as [s' [SUCC' DOBSS]].
      unfolds in C1.
      rewrite forallb_forall in C1.
      gen (C1 _ SUCC) as DOBSS'.
      optDecN DOBSS DOBS'; trim.
      destruct p as [[d'' dc''] o'].
      case_eq (successors_instr i); introsv SUCCS; trim.
      rewrite SUCCS in SUCC'; trim.
      destruct l.
      rewrite SUCCS in SUCC, SUCC'.
      inv_clear SUCC; trim. inv_clear SUCC'; trim.
      subst s' n0.
      rewrite DOBS' in DOBSS'.
      boolrw.
      decs DOBSS'. apply Peqb_eq in H2. subst o'.
      eexists; eexists; rewrite DOBS'; eauto.
      rewrite SUCCS in CONTROL; simpl in CONTROL.
      unfolds in CONTROL.
      boolrw.
      repeat rewrite forallb_forall in CONTROL.
      destruct CONTROL as [NONE | SOME].
      exfalso.
      gen (NONE s') as OBSNONE.
      unfold option_none_beq in OBSNONE.
      rewrite DOBS' in OBSNONE.
      rewrite <- SUCCS in OBSNONE.
      apply OBSNONE in SUCC'; trim.
      optDecN DOBSS' DOBS.
      destruct p as [[d''' dc] o''].
      boolrw. decs DOBSS'. apply Peqb_eq in H2. subst o''.
      eexists; eexists; eauto.
      exfalso.
      gen (SOME s) as S1.
      rewrite DOBS in S1.
      rewrite <- SUCCS in S1.
      apply S1 in SUCC.
      rewrite negb_true_iff in SUCC; trim.
    Case "checked_nobs_zero_refl".
      introsv DOBS.
      rewrite PTree.gmap in DOBS; unfold option_map in DOBS.
      optDecN DOBS DOBSN; trim.
      dup DOBSN FIN.
      apply dobs_some_f_In in FIN.
      apply f_In_ex in FIN.
      destruct FIN as [i INST].
      eapply forall_ptree_true with (i := n) (x := i) in FOLD; eauto.
      rewrite DOBSN in FOLD.
      optDecN FOLD IN_SL.
      optDec FOLD.
      subst n.
      rewrite NC_ZERO in DOBSN.
      inversion DOBS. inversion DOBSN.
      subst p.
      inversion H0; auto.
      destruct p. destruct p.
      boolrw.
      decs FOLD.
      projInv H3; trim.
      boolrw.
      inversion DOBS; clear DOBS.
      destruct p as [[d' dc'] o'].
      inversion H0; clear H0.
      subst dc o'.
      boolrw.
      destruct FOLD as [DEXIT [JUMP [[[[A B] C] C1] C2]]].
      projInv A.
      projInv B.
      lia2.
    Case "checked_nobs_control".
      introsv INST S1 S2 GETS1 GETS2.
      rewrite PTree.gmap in *; unfold option_map in *.
      optDecN GETS1 GET1; trim.
      optDecN GETS2 GET2; trim.
      clear GETS1 GETS2.
      apply ptree_forall with (i := n) (x := i) in FOLD; auto.
      optDecN FOLD MEM.
      rewrite mem_iff_In in MEM; auto.
      boolrw.
      destruct FOLD as [DEXIT [[JUMP CONTROL] DOBS]].
      assert (LGT: (length (successors_instr i) > 1)%nat).
        case_eq (successors_instr i); intros.
        rewrite H in S1; trim.
        destruct l.
        rewrite H in S1; rewrite H in S2.
        simpls. destruct S1, S2; trim.
        simpl. lia2.
      optDec CONTROL; trim.
      unfolds in CONTROL.
      boolrw.
      destruct CONTROL as [CONTROL | CONTROL]; rewrite forallb_forall in CONTROL.
      apply CONTROL in S1.
      unfolds in S1; rewrite GET1 in S1; trim.
      apply CONTROL in S2.
      unfolds in S2; rewrite GET2 in S2; trim.
    Case "checked_nobs_jumptable".
      intros.
      apply ptree_forall with (i := n) (x := (Ijumptable arg tbl)) in FOLD; auto.
      optDecN FOLD MEM.
      rewrite mem_iff_In in MEM; auto.
      boolrw.
      destruct FOLD as [DEXIT [[JUMP C] C']]; trim.
    Case "checked_nexit_exit".
      destruct IN_EXIT as [IN_EXIT EEQ].
      unfold nexit.
      rewrite PTree.gmap; unfold option_map.
      optDecG; trim.
      projInv EEQ. subst n; auto.
    Case "checked_has_exit".
      introsv FIN.
      unfold nexit.
      rewrite PTree.gmap in *; unfold option_map in *.
      apply f_In_ex in FIN.
      destruct FIN as [i INST].
      eapply forall_ptree_true with (i := n) (x := i) in FOLD; eauto.
      boolrw. destruct FOLD as [DEXIT FOLD]; trim.
      unfolds in DEXIT.
      case_match (dexit ! n) as DEXIT' in DEXIT; trim.
      eexists; eauto.
    Case "checked_nexit_ex_succ".
      introsv FIN NEXIT.
      unfold nexit in NEXIT.
      rewrite PTree.gmap in *; unfold option_map in *.
      optDecN NEXIT DEXIT; trim.
      inversion NEXIT; clear NEXIT.
      apply f_In_ex in FIN.
      destruct FIN as [i INST].
      eapply forall_ptree_true with (i := n) (x := i) in FOLD; eauto.
      boolrw. destruct FOLD as [CDEXIT FOLD]; trim.
      unfolds in CDEXIT.
      rewrite DEXIT in CDEXIT.
      optDec CDEXIT.
      subst n.
      apply Neqb_eq in CDEXIT.
      lia2.
      boolrw.
      rewrite forallb_forall, existsb_exists in CDEXIT.
      destruct CDEXIT as [FASUCCS EXSUCCS].
      destruct EXSUCCS as [s [INS DEXITS]].
      optDecN DEXITS DS; trim.
      exists s. split.
      exists i; auto.
      unfold nexit.
      rewrite PTree.gmap; unfold option_map.
      rewrite DS.
      f_equal.
      apply Neqb_eq in DEXITS.
      lia2.
    Case "checked_nexit_zero_refl".
      introsv FIN NEXIT.
      unfold nexit in NEXIT.
      rewrite PTree.gmap in *; unfold option_map in *.
      optDecN NEXIT DEXIT; trim.
      inversion NEXIT; clear NEXIT.
      apply f_In_ex in FIN.
      destruct FIN as [i INST].
      eapply forall_ptree_true with (i := n) (x := i) in FOLD; eauto.
      boolrw. destruct FOLD as [CDEXIT FOLD]; trim.
      unfolds in CDEXIT.
      rewrite DEXIT in CDEXIT.
      optDec CDEXIT; trim.
      boolrw.
      rewrite forallb_forall, existsb_exists in CDEXIT.
      destruct CDEXIT as [FASUCCS EXSUCCS].
      destruct EXSUCCS as [s [INS DEXITS]].
      apply FASUCCS in INS.
      optDecN DEXITS DEXITS'; trim.
      apply Neqb_eq in DEXITS.
      lia2.
    Case "checked_nexit_minus_one".
      introsv NEXITN SUCC NEXITS.
      unfold nobs, nexit in *.
      rewrite PTree.gmap in *; unfold option_map in *.
      optDecN NEXITN DEXITN; trim.
      optDecN NEXITS DEXITS; trim.
      inv NEXITN. inv NEXITS.
      dup SUCC S.
      apply succ_f_In in S. apply f_In_ex in S. destruct S as [i INST].
      apply forall_ptree_true with (i := n) (x := i) in FOLD; eauto.
      boolrw. destruct FOLD as [CDEXIT FOLD].
      unfolds in CDEXIT.
      rewrite DEXITN in CDEXIT.
      optDec CDEXIT; trim.
      subst n.
      gen (exit_no_succ s); trim.
      boolrw.
      rewrite forallb_forall in CDEXIT.
      rewrite existsb_exists in CDEXIT.
      destruct CDEXIT as [FA EX].
      destruct SUCC as [i' [INST' SUCC']].
      rewrite INST in INST'.
      inv INST'.
      apply FA in SUCC'.
      rewrite DEXITS in SUCC'.
      projInv SUCC'.
      lia2.
  Qed.

  Lemma checked_crit_nobs_refl:
    forall n d o,
      nobs ! n = Some (d, 0%nat, o) ->
      d = 0%nat /\ n = o /\ o = nc.

Proof.

End DOBS.

Section SLICE.

  Variable f : function.
  Variable fsc : Scope.family f.
  Variable nc : t_criterion.
  Variable exit_n : node.
  Variable reg_vint : reg.
  Variable sliced_f : function.
  Variable of : obs_function.
  Hypothesis FOK: slice_function f nc fsc exit_n reg_vint = OK (sliced_f, of).

  Notation nobs' := (nobs (_s_dobs of)).
  Notation nexit' := (nexit (_dexit of)).
  Notation exit_n' := (_exit of).

  Hypothesis exit_no_succ:
    forall s, ~ succ_node f exit_n' s.

  Ltac prepareConds EQ EQ1 DOBS RVS SCEX :=
    unfold slice_function, compute_slice in FOK; monadInv FOK; monadInv EQ; optDecN EQ1 DOBS; trim; optDecN EQ1 RVS; trim; optDecN EQ1 SCEX; trim; inv EQ1; simpls; unfolds in DOBS; boolrw; destruct DOBS as [[[[[[ALLIN DOBS_IN] NCZ] ENTRY] NC] EXIT] FOLD]; rewrite forallb_forall in ALLIN.

  Lemma entry_in_slice:
    In (fn_entrypoint f) (_slice_nodes of).

Proof.

    intros.
    prepareConds EQ EQ1 DOBS RVS SCEX.
    rewrite <- mem_iff_In.
    apply ENTRY.
  Qed.

Lemma crit_in_slice:
In nc (_slice_nodes of).

Proof.

    intros.
    prepareConds EQ EQ1 DOBS RVS SCEX.
    apply mem_iff_In in NC; auto.
  Qed.

Lemma slice_ok_dobs_checker_true:
s_dobs_checker f nc of.(_exit) of.(_slice_nodes) of.(_s_dobs) of.(_dexit) = true.

Proof.

    prepareConds EQ EQ1 DOBS RVS SCEX.
    unfold s_dobs_checker.
    boolrw; auto.
    repeat (split; trim).
    rewrite forallb_forall.
    intros n IN.
    apply ALLIN in IN; auto.
  Qed.

Lemma slice_ok_checked_nobs:
checked_nobs f nc of.(_exit) of.(_slice_nodes) nobs' nexit'.

Proof.

    apply checked_nobs_wf; auto.
    apply slice_ok_dobs_checker_true.
  Qed.

  Lemma exit_no_entry:
    forall
      (WFF: check_wf f = OK (exit_n, reg_vint)),
      f.(fn_entrypoint) <> exit_n'.

Proof.

    intros WFF CONTRA.
    exploit entry_inst; eauto.
    intros EINST.
    destruct EINST as (s & EINST).
    rewrite CONTRA in EINST.
    exploit exit_no_succ; eauto.
    eexists; eauto.
  Qed.

  Lemma nobs_not_zero_not_in_slice:
    forall n d dc o,
      nobs' ! n = Some (S d, dc, o) ->
      ~ In n (_slice_nodes of).

Proof.

    intros.
    prepareConds EQ EQ1 DOBS RVS SCEX.
    intro IN.
    dup IN IN'.
    apply ALLIN in IN'.
    unfold Pmem in IN'. optDecN IN' GET; trim.
    apply ptree_forall with (i := n) (x := i) in FOLD; auto.
    rewrite <- mem_iff_In in IN.
    rewrite IN in FOLD.
    optDec FOLD.
    boolrw.
    destruct FOLD as [DEXIT FOLD].
    apply option_N_N_node_beq_eq in FOLD.
    unfold nobs in H. rewrite PTree.gmap in H. unfold option_map in H.
    rewrite FOLD in H.
    inv H.
    boolrw.
    destruct FOLD as [DEXIT FOLD].
    unfolds in FOLD.
    unfold nobs in H. rewrite PTree.gmap in H. unfold option_map in H.
    optDecN H DOBS; trim.
    rewrite DOBS in FOLD.
    destruct p as [[d' dc'] o'].
    boolrw.
    decs FOLD.
    projInv H0.
    subst d'; trim.
  Qed.

  Lemma nobs_zero_in_slice:
    forall n dc o,
      nobs' ! n = Some (0%nat, dc, o) ->
      In n (_slice_nodes of).

Proof.

    intros.
    unfold slice_function, compute_slice in FOK.
    monadInv FOK.
    monadInv EQ.
    optDecN EQ1 DOBS; trim.
    optDecN EQ1 RVS; trim.
    optDecN EQ1 SCEX; trim.
    inversion EQ1 as [EQOF]; clear EQ1; simpls.
    subst of; simpls.
    dup DOBS WF.
    apply checked_nobs_wf in WF; auto.
    dup WF DREFL.
    apply checked_nobs_refl with (n := n) in DREFL; auto.
    dup WF D0REFL.
    eapply checked_nobs_zero_refl in D0REFL; eauto.
    subst o.
    apply DREFL; auto.
    eexists; eauto.
  Qed.

  Lemma nobs_in_slice_zero:
    forall n d dc o,
      nobs' ! n = Some (d, dc, o) ->
      In n (_slice_nodes of) ->
      d = 0%nat.

Proof.

    intros.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    exploit checked_nobs_refl; eauto; intros.
    apply H1 in H0.
    decs H0.
    rewrite H in H2.
    inv H2; auto.
  Qed.

  Lemma nobs_none_not_in_slice:
    forall n,
      nobs' ! n = None ->
      ~ In n (_slice_nodes of).

Proof.

    intros.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    intro.
    exploit checked_nobs_none_not_in_slice; eauto.
  Qed.

  Lemma nobs_non_zero_ex_succ:
    forall n d dc o,
      nobs' ! n = Some (S d, dc, o) ->
      exists s, exists dc', succ_node f n s /\ nobs' ! s = Some (d, dc', o).

Proof.

    intros.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    exploit checked_nobs_ex_succ; eauto; intros.
    decs H0.
    eexists; eauto.
  Qed.

  Lemma nobs_non_zero_ex_succ':
    forall n d dc o,
      nobs' ! n = Some (S d, dc, o) ->
      exists s, exists n', exists dc', succ_node f n s /\ nobs' ! s = Some (n', dc', o).

Proof.

    intros.
    apply nobs_non_zero_ex_succ in H.
    decs H; eexists; eexists; eauto.
  Qed.

  Lemma nobs_succ_minus_one:
    forall n d dc o,
      nobs' ! n = Some (S d, dc, o) ->
      forall s,
        succ_node f n s ->
        forall d' dc' o',
          nobs' ! s = Some (d', dc', o') ->
          (d' >= d)%nat.

Proof.

    intros.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    exploit checked_nobs_minus_one; eauto; intros.
  Qed.

  Lemma nobs_none_succ_none:
    forall n,
      nobs' ! n = None ->
      forall s,
        succ_node f n s -> nobs' ! s = None.

Proof.

    intros.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    unfolds in H0. decs H0.
    exploit checked_nobs_none_succ_none; eauto; intros.
  Qed.

  Lemma nobs_none_reaches_none:
    forall n,
      nobs' ! n = None ->
      forall s,
        reaches f n s -> nobs' ! s = None.

Proof.

    induction 2; intros; auto.
    apply IHreaches.
    eapply nobs_none_succ_none; eauto.
  Qed.

  Lemma nobs_some_succ_same:
    forall n d dc o,
      nobs' ! n = Some (S d, dc, o) ->
      forall s,
        succ_node f n s -> exists d', exists dc', nobs' ! s = Some (d', dc', o).

Proof.

    intros.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    unfolds in H0. decs H0.
    exploit checked_nobs_some_succ_same; eauto; intros.
  Qed.

  Lemma nobs_zero_refl:
    forall n dc o,
      nobs' ! n = Some (0%nat, dc, o) ->
      o = n.

Proof.

    intros.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    exploit checked_nobs_zero_refl; eauto; intros.
  Qed.

A node that has different observables for its successors is always a control node and therefore must belong in the slice. checked_nobs_control

  Lemma nobs_control_in_slice:
    forall n s1 s2 d dc o,
      succ_node f n s1 ->
      succ_node f n s2 ->
      nobs' ! s1 = Some (d, dc, o) ->
      nobs' ! s2 = None ->
      In n (_slice_nodes of).

Proof.

    intros.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    unfold succ_node in H, H0.
    decs H. decs H0.
    rewrite H3 in H4.
    inv_clear H4; subst x0.
    exploit checked_nobs_control; intros; auto.
    apply CHECK.
    eauto. apply H5.
    eauto.
    eauto.
    eauto.
    eauto.
  Qed.

checked_nobs_jumptable

  Lemma slice_includes_Ijumptable:
    forall pc arg tbl,
      (fn_code f) ! pc = Some (Ijumptable arg tbl) ->
      In pc of.(_slice_nodes).

Proof.

    intros.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    exploit checked_nobs_jumptable; eauto.
  Qed.

  Lemma in_slice_nobs_refl:
    forall n,
      In n (_slice_nodes of) ->
      exists dc, nobs' ! n = Some (0%nat, dc, n).

Proof.

    intros.
    case_eq (nobs' ! n); intros.
    destruct p as [[d dc] o].
    dup H0 NOBS.
    apply nobs_in_slice_zero in H0; auto.
    subst d.
    exists dc.
    apply (nobs_zero_refl) in NOBS. subst o; auto.
    apply nobs_none_not_in_slice in H0.
    contra.
  Qed.

  Lemma nexit_succ_minus_one:
    forall n dx,
      nexit' ! n = Some (S dx) ->
      forall s,
        succ_node f n s ->
        forall dx',
          nexit' ! s = Some (dx') ->
          (dx' >= dx)%nat.

Proof.

    intros.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    exploit checked_nexit_minus_one; eauto; intros.
  Qed.

  Lemma nexit_eq:
    forall
      (WFF: check_wf f = OK (exit_n, reg_vint)),
      exit_n' = exit_n.

Proof.

    intros WFF.
    unfolds in WFF.
    optDecN WFF CONDS; trim.
    monadInv WFF.
    unfolds in FOK.
    monadInv FOK.
    unfolds in EQ0.
    monadInv EQ0.
    optDec EQ3; trim.
    optDec EQ3; trim.
    optDec EQ3; trim.
    inv EQ3; auto.
  Qed.

  Lemma exit_in':
    forall
      (WFF: check_wf f = OK (exit_n, reg_vint))
      dx n s
      (SUCC: succ_node f n s)
      (DX: nexit' ! s = Some dx),
      f_In exit_n f.

Proof.

    intro WFF.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    induction dx; intros n s SUCC DX.
    eapply checked_nexit_zero_refl in DX; eauto.
    subst s. rewrite <- nexit_eq; auto.
    eapply succ_f_In'; eauto.
    eapply succ_f_In'; eauto.
    eapply checked_nexit_ex_succ in DX; eauto.
    destruct DX as (s' & SUCC' & DX).
    apply IHdx with (n := s) (s := s'); eauto.
    eapply succ_f_In'; eauto.
  Qed.

  Lemma exit_in:
    forall
      (WFF: check_wf f = OK (exit_n, reg_vint)),
      f_In exit_n f.

Proof.

    intros WFF.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    dup CHECK HASNEXIT.
    apply checked_has_nexit with (n := f.(fn_entrypoint)) in HASNEXIT.
    destruct HASNEXIT as (dx & DX).
    destruct dx.
    Case "dx = 0 -> contradiction".
      eapply checked_nexit_zero_refl in DX; eauto.
      apply exit_no_entry in DX; cong.
      eapply wf_entry_in; eauto.
    Case "dx > 0".
      eapply checked_nexit_ex_succ in DX; eauto.
      destruct DX as (s & SUCC & DX).
      eapply exit_in'; eauto.
      eapply entry_in; eauto.
      eapply entry_in; eauto.
  Qed.

  Lemma reaches_exit:
    forall
      (WFF: check_wf f = OK (exit_n, reg_vint))
      dx n s
      (SUCC: succ_node f n s)
      (DX: nexit' ! s = Some dx),
      reaches f n exit_n.

Proof.

    intro WFF.
    gen slice_ok_dobs_checker_true as CHECK.
    apply checked_nobs_wf in CHECK; auto.
    induction dx; intros n s SUCC DX.
    eapply checked_nexit_zero_refl in DX; eauto.
    subst s. eapply r_succ; eauto.
    rewrite nexit_eq; auto.
    apply r_refl.
    apply exit_in; auto.
    eapply succ_f_In'; eauto.
    eapply checked_nexit_ex_succ in DX; eauto.
    destruct DX as (s' & SUCC' & DX).
    apply r_succ with (n' := s); auto.
    apply IHdx with (n := s) (s := s'); eauto.
    eapply succ_f_In'; eauto.
  Qed.

End SLICE.

Module SliceObs_proof