LAProof.C.verif_sparse

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.

Definition the_loop_body : statement.
Defined.

Lemma crs_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)
  (cols : Z)
  (vals : list (ftype Tdouble))
  (col_ind row_ptr : list Z)
  (H4 : crs_rep_aux mval cols vals col_ind row_ptr)
  (FRAME: mpred)
  (H5 : 0 ≤ 0 < Zlength row_ptr)
  (i : Z)
  (H6 : 0 ≤ i < matrix_rows mval),
semax (func_tycontext f_crs_matrix_vector_multiply Vprog Gprog [])
  (PROP ( )
   LOCAL (temp _i (Vint (Int.repr i));
   temp _next (Vint (Int.repr (Znth i row_ptr)));
   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 col_ind)) (map Vfloat vals) vp;
   data_at sh1 (tarray tuint (Zlength col_ind))
     (map Vint (map Int.repr col_ind)) ci;
   data_at sh1 (tarray tuint (matrix_rows mval + 1))
     (map Vint (map Int.repr row_ptr)) 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) row_ptr)));
      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 col_ind)) (map Vfloat vals) vp;
      data_at sh1 (tarray tuint (Zlength col_ind))
        (map Vint (map Int.repr col_ind)) ci;
      data_at sh1 (tarray tuint (matrix_rows mval + 1))
        (map Vint (map Int.repr row_ptr)) 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_crs_matrix_vector_multiply :
  semax_body Vprog Gprog f_crs_matrix_vector_multiply crs_matrix_vector_multiply_spec.