proposition: Lemma svwl_reachable_or_marked: forall from to (roots: roots_t) l g1 g2, from <> to -> sound_gc_graph g1 -> graph_has_gen g1 to -> gen_unmarked g1 to -> roots_graph_compatible roots g1 -> no_dangling_dst g1 -> copied_vertex_prop g1 from to -> copy_compatible g1 -> backward_edge_prop g1 roots from to -> scan_vertex_while_loop from to l g1 g2 -> forall v, reachable_or_marked from g1 roots v <-> reachable_or_marked from g2 roots v.
proof: Proof. pose (H3:=True). do 4 intro. induction l; intros; inversion H9; subst; clear H9; try easy. 1: apply IHl; auto. pose proof H14. eapply svfl_reachable_or_marked with (v := v) in H9; eauto. 2: split; simpl; auto. 2: unfold no_scan in H13; lia. 2: intros; now rewrite nat_inc_list_In_iff in H10. rewrite H9. assert (graph_has_v g1 (to, a)) by (now split). assert (forall i : nat, In i (nat_inc_list (length (raw_fields (vlabel g1 (to, a))))) -> (i < length (raw_fields (vlabel g1 (to, a))))%nat). { intros. rewrite nat_inc_list_In_iff in H11; auto. } apply IHl; auto. - eapply svfl_P_holds; eauto. apply fr_O_sound. - rewrite <- svfl_graph_has_gen; eauto. - eapply svfl_gen_unmarked; eauto. - eapply svfl_roots_graph_compatible; eauto. unfold no_scan in H13; lia. - eapply (svfl_no_dangling_dst from to); eauto. unfold no_scan in H13; lia. - eapply svfl_copied_vertex_prop; eauto. unfold no_scan in H13; lia. - eapply svfl_copy_compatible; eauto. - eapply svfl_backward_edge_prop; eauto. unfold no_scan in H13; lia. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics compcert.lib.Integers compcert.common.Values VST.veric.base VST.veric.Clight_lemmas VST.veric.val_lemmas VST.veric.shares VST.msl.seplog VST.msl.shares VST.zlist.sublist VST.floyd.coqlib3 VST.floyd.functional_base VST.floyd.data_at_rec_lemmas CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.graph_isomorphism CertiGraph.graph.reachable_ind CertiGraph.CertiGC.GCGraph