proposition: Lemma body_summatrix: semax_body Vprog Gprog f_summatrix summatrix_spec.
proof: Proof. start_function. forward. forward. forward. forward_while (EX i: Z, PROP (0 <= i <= 2) LOCAL (temp _a a; temp _i (Vint (Int.repr i)); temp _n (Vint (Int.repr 2)); temp _s (Vint (Int.repr (sum_mat (sublist 0 i contents_mat))))) SEP (matrix_rep sh 2 contents_mat a)). - Exists 0; entailer!. - entailer!. - forward. forward_while ( EX j: Z, PROP (0 <= j <= 2) LOCAL (temp _a a; temp _i (Vint (Int.repr i)); temp _j (Vint (Int.repr j)); temp _n (Vint (Int.repr 2)); temp _s (Vint (Int.add (Int.repr (sum_list (sublist 0 j (Znth i contents_mat)))) (Int.repr (sum_mat (sublist 0 i contents_mat)))))) SEP (matrix_rep sh 2 contents_mat a)). + Exists 0; entailer!. + entailer!. + rewrite (matrix_unfold _ _ _ _ i) by lia. Intros. freeze F := (iter_sepcon (list_rep sh 2 a contents_mat) (sublist 0 i (Z_inc_list (Z.to_nat (Zlength contents_mat))))) (iter_sepcon (list_rep sh 2 a contents_mat) (sublist (i + 1) (Zlength contents_mat) (Z_inc_list (Z.to_nat (Zlength contents_mat))))). unfold list_rep. unfold list_address. simpl. Fail forward. assert_PROP (force_val (sem_add_ptr_int tuint Signed (force_val (sem_add_ptr_int (tarray tuint 2) Signed a (Vint (Int.repr i)))) (Vint (Int.repr j))) = field_address (tarray tuint 2) [ArraySubsc j] (list_address a i 2)). { entailer!. unfold list_address. simpl. rewrite field_address_offset. 1: rewrite offset_offset_val; simpl; f_equal; rep_lia. unfold field_compatible in H5. destruct H4 as [? [? [? [? ?]]]]. unfold field_compatible. split3; [| | split3]; auto. unfold legal_nested_field. split; [auto | simpl; lia]. } assert (Zlength (Znth i contents_mat) = 2). { rewrite Forall_forall in H0. apply H0. apply Znth_In. lia. } forward. forward. forward. Exists (j+1). entailer!. * f_equal. f_equal. rewrite sublist_last_1; [|lia..]. rewrite sum_list_app; simpl; lia. * thaw F. rewrite (matrix_unfold _ _ _ _ i). entailer!. lia. + forward. Exists (i+1). entailer!. assert (j = Zlength contents_mat) by lia. assert (j = 2) by lia. assert (Zlength (Znth i contents_mat) = 2). { rewrite Forall_forall in H0. apply H0. apply Znth_In. lia. } rewrite (sublist_same 0 j); trivial. 2: now rewrite H6. rewrite sublist_last_1; try rep_lia. rewrite sum_mat_app. do 2 f_equal. unfold sum_mat at 2. simpl. lia. - unfold POSTCONDITION, abbreviate. forward. entailer!. assert (i = Zlength contents_mat) by lia. rewrite sublist_same; trivial. Qed.
imports: VST.floyd.proofauto CertiGraph.summatrix.summatrix VST.msl.iter_sepcon