LAProof.C.verif_sparse

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


Open Scope logic.

Definition the_loop_body : statement.
Defined.

Lemma csr_multiply_loop_body:
 ∀ (Espec : OracleKind) (sh1 sh2 sh3 : share)
   (m : val) (mval : matrix Tdouble)
   (v : val) (vval : vector Tdouble)
   (p : val) (partial_result: list val)
  (SH : readable_share sh1)
  (SH0 : readable_share sh2)
  (SH1 : writable_share sh3)
  (H : matrix_cols mval (Zlength vval))
  (H0 : matrix_rows mval < Int.max_unsigned)
  (H1 : Zlength vval < Int.max_unsigned)
  (H2 : Forall (Forall finite) mval)
  (FINvval: Forall finite vval)
  (H3 : 0 ≤ matrix_rows mval)
  (vp ci rp : val)
  (csr : csr_matrix Tdouble)
  (H4 : csr_to_matrix csr mval)
  (FRAME: mpred)
  (H5 : 0 ≤ 0 < Zlength (csr_row_ptr csr))
  (i : Z)
  (H6 : 0 ≤ i < matrix_rows mval),
semax (func_tycontext f_csr_matrix_vector_multiply Vprog Gprog [])
  (PROP ( )
   LOCAL (temp _i (Vint (Int.repr i));
   temp _next (Vint (Int.repr (Znth i (csr_row_ptr csr))));
   temp _row_ptr rp; temp _col_ind ci; temp _val vp;
   temp _rows (Vint (Int.repr (matrix_rows mval)));
   temp _m m; temp _v v; temp _p p)
   SEP (FRAME;
   data_at sh1 (tarray tdouble (Zlength (csr_col_ind csr))) (map Vfloat (csr_vals csr)) vp;
   data_at sh1 (tarray tuint (Zlength (csr_col_ind csr)))
     (map Vint (map Int.repr (csr_col_ind csr))) ci;
   data_at sh1 (tarray tuint (matrix_rows mval + 1))
     (map Vint (map Int.repr (csr_row_ptr csr))) rp;
   data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v;
   data_at sh3 (tarray tdouble (matrix_rows mval)) partial_result p))
      the_loop_body
  (normal_ret_assert
    (EX r: ftype Tdouble,
     (PROP (feq r (dotprod (Znth i mval) vval))
      LOCAL (temp _i (Vint (Int.repr i));
      temp _next (Vint (Int.repr (Znth (i + 1) (csr_row_ptr csr))));
      temp _row_ptr rp; temp _col_ind ci; temp _val vp;
      temp _rows (Vint (Int.repr (matrix_rows mval)));
      temp _m m; temp _v v; temp _p p)
      SEP (FRAME;
      data_at sh1 (tarray tdouble (Zlength (csr_col_ind csr))) (map Vfloat (csr_vals csr)) vp;
      data_at sh1 (tarray tuint (Zlength (csr_col_ind csr)))
        (map Vint (map Int.repr (csr_col_ind csr))) ci;
      data_at sh1 (tarray tuint (matrix_rows mval + 1))
        (map Vint (map Int.repr (csr_row_ptr csr))) rp;
      data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v;
      data_at sh3 (tarray tdouble (matrix_rows mval))
                   (upd_Znth i partial_result (Vfloat r)) p)))).

Lemma body_csr_matrix_vector_multiply: semax_body Vprog Gprog f_csr_matrix_vector_multiply csr_matrix_vector_multiply_spec.