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_csr_rep:
  ∀ sh (p v ci rp: val) mval cols (vals: list (ftype Tdouble)) col_ind row_ptr,
     csr_rep_aux mval cols vals col_ind row_ptr →
     data_at sh t_csr
          (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
     |-- csr_rep sh mval p.

Lemma body_csr_matrix_rows: semax_body Vprog Gprog f_csr_matrix_rows csr_matrix_rows_spec.

Lemma body_csr_row_vector_multiply: semax_body Vprog Gprog f_csr_row_vector_multiply csr_row_vector_multiply_spec.

Lemma body_csr_matrix_vector_multiply_byrows : semax_body Vprog Gprog f_csr_matrix_vector_multiply_byrows csr_matrix_vector_multiply_byrows_spec.