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 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.