proposition: Lemma data_at_mfs_eq: forall g v i sh nv, field_compatible int_or_ptr_type [] (offset_val (WORD_SIZE * i) nv) -> 0 <= i < Zlength (raw_fields (vlabel g v)) -> data_at sh (tarray int_or_ptr_type i) (sublist 0 i (make_fields_vals g v)) nv * field_at sh int_or_ptr_type [] (Znth i (make_fields_vals g v)) (offset_val (WORD_SIZE * i) nv) = data_at sh (tarray int_or_ptr_type (i + 1)) (sublist 0 (i + 1) (make_fields_vals g v)) nv.
proof: Proof. intros. rewrite field_at_data_at. unfold field_address. rewrite if_true by assumption. simpl nested_field_type. simpl nested_field_offset. rewrite offset_offset_val. replace (WORD_SIZE * i + 0) with (WORD_SIZE * i)%Z by lia. rewrite <- (data_at_singleton_array_eq sh int_or_ptr_type _ [Znth i (make_fields_vals g v)]) by reflexivity. rewrite <- fields_eq_length in H0. rewrite (data_at_tarray_value sh (i + 1) i nv (sublist 0 (i + 1) (make_fields_vals g v)) (make_fields_vals g v) (sublist 0 i (make_fields_vals g v)) [Znth i (make_fields_vals g v)]). - replace (i + 1 - i) with 1 by lia. reflexivity. - lia. - lia. - autorewrite with sublist. reflexivity. - reflexivity. - rewrite sublist_one; [reflexivity | lia..]. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec) CertiGraph.msl_ext.ramification_lemmas VST.concurrency.conclib