proposition: Lemma frame_root_address_eq: forall frames i, 0 <= i < Zlength (frames2rootpairs frames) -> frame_root_address frames i = rp_adr (Znth i (frames2rootpairs frames)).
proof: Proof. unfold frames2rootpairs. induction frames as [ | [ a r s] fr']; simpl; intros. - list_solve. - pose proof (Zlength_frame2rootpairs' r 0 s). unfold frame2rootpairs at 1. unfold frame2rootpairs at 1 in H. simpl in H|-*. if_tac. rewrite Znth_app1 by list_solve. assert (0 <= i < Zlength s) by lia. clear - H2. change i with (0+i) at 1. set (j:=0). clearbody j. revert i j H2; induction s; simpl; intros. list_solve. destruct (zeq i 0). subst. list_simplify. rewrite Znth_pos_cons by list_solve. rewrite <- IHs by list_solve. f_equal. lia. rewrite Znth_app2 by list_solve. rewrite IHfr' by list_solve. f_equal. f_equal. list_solve. Qed.
imports: Coq.ZArith.ZArith Coq.Program.Basics Coq.micromega.Lia 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 VST.zlist.list_solver CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen