proposition: Lemma concrete_valid_pointer_valid_pointer: forall p, concrete_valid_pointer p |-- valid_pointer (pointer_val_val p).
proof: Proof. intros. unfold concrete_valid_pointer. apply orp_left. + normalize. auto with valid_pointer. + apply data_at_valid_ptr. - intro. apply identity_share_bot in H. apply comp_Ews_not_bot. auto. - change (sizeof node_type) with (if Archi.ptr64 then 32 else 16). cbv [Archi.ptr64]. lia. Qed.
imports: CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin VST.veric.SeparationLogic CertiGraph.copy.env_copy_bin