proposition: Lemma svfl_reachable_or_marked: forall from to (roots: roots_t) r l g1 g2, from <> to -> sound_gc_graph g1 -> graph_has_gen g1 to -> graph_has_v g1 r -> raw_mark (vlabel g1 r) = false -> raw_tag (vlabel g1 r) < NO_SCAN_TAG -> vgeneration r = to -> gen_unmarked g1 to -> roots_graph_compatible roots g1 -> no_dangling_dst g1 -> copied_vertex_prop g1 from to -> copy_compatible g1 -> (forall i : nat, In i l -> (i < length (raw_fields (vlabel g1 r)))%nat) -> backward_edge_prop g1 roots from to -> scan_vertex_for_loop from to r l g1 g2 -> forall v, reachable_or_marked from g1 roots v <-> reachable_or_marked from g2 roots v.
proof: Proof. pose (H6:=True). intros until l. induction l; intros ? ? ? ? ? ? ? NOSCAN; intros; inversion H13; subst; clear H13; try easy. change (forward_p2forward_t (inr (r, Z.of_nat a)) [] g1) with (forward_p2forward_t (inr (r, Z.of_nat a)) roots g1) in H16. pose proof H16. assert (forward_p_compatible (inr (r, Z.of_nat a)) roots g1 from). { simpl. split3; [ | | split3]; auto. split; auto. lia. rewrite Zlength_correct. apply inj_lt, H11. now left. } eapply fr_O_reachable_or_marked with (v := v) in H4; eauto. 2: simpl; split; auto. remember (vgeneration r) as to. simpl in H4. rewrite H4. apply IHl; auto. - eapply fr_O_sound; eauto. - rewrite <- fr_graph_has_gen; eauto. - eapply fr_graph_has_v; eauto. - erewrite <- fr_raw_mark; eauto. subst to; auto. - erewrite <- fr_raw_tag; eauto. subst to; auto. - eapply fr_gen_unmarked; eauto. - eapply fr_right_roots_graph_compatible; eauto. - eapply fr_O_no_dangling_dst; eauto. - eapply fr_O_copied_vertex_prop; eauto. - eapply fr_copy_compatible; eauto. - erewrite <- fr_raw_fields; eauto. intros. apply H11. now right. - eapply fr_O_backward_edge_prop in H16; eauto. now simpl. 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