LAProof.C.verif_sparse_byrows

Require Import VST.floyd.proofauto.
From LAProof.C Require Import sparse sparse_model spec_sparse.
Require Import vcfloat.FPStdLib.
Require Import vcfloat.FPStdCompCert.
Require Import VSTlib.spec_math.
Require Import LAProof.C.floatlib.


Open Scope logic.

Lemma fold_crs_rep:
  ∀ sh (p v ci rp: val) mval cols (vals: list (ftype Tdouble)) col_ind row_ptr,
     crs_rep_aux mval cols vals col_ind row_ptr →
     data_at sh t_crs
          (v, (ci, (rp, (Vint (Int.repr (matrix_rows mval)),
                      Vint (Int.repr cols))))) p ×
     data_at sh (tarray tdouble (Zlength col_ind)) (map Vfloat vals) v ×
     data_at sh (tarray tuint (Zlength col_ind))
                     (map Vint (map Int.repr col_ind)) ci ×
     data_at sh (tarray tuint (matrix_rows mval + 1))
            (map Vint (map Int.repr row_ptr)) rp
     |-- crs_rep sh mval p.

Lemma body_crs_matrix_rows: semax_body Vprog Gprog f_crs_matrix_rows crs_matrix_rows_spec.

Lemma body_crs_row_vector_multiply: semax_body Vprog Gprog f_crs_row_vector_multiply crs_row_vector_multiply_spec.

Lemma body_crs_matrix_vector_multiply_byrows : semax_body Vprog Gprog f_crs_matrix_vector_multiply_byrows crs_matrix_vector_multiply_byrows_spec.