Strip some trailing whitespace

C/VSU_sparse.v

@@ -12,11 +12,11 @@ Open Scope logic.
 
 #[local] Existing Instance NullExtension.Espec.  (* FIXME *)
 
-Definition sparseImports : funspecs := [fma_spec]. (* Ideally , 
+Definition sparseImports : funspecs := [fma_spec]. (* Ideally ,
    the VSU system would let us say MathASI instead of [fma_spec] *)
 
 Definition SparseVSU: VSU nil sparseImports ltac:(QPprog prog) SparseASI emp.
-  Proof. 
+  Proof.
     mkVSU prog SparseASI.
 - solve_SF_internal body_crs_matrix_rows.
 - solve_SF_internal body_crs_row_vector_multiply.

C/sparse_model.v

@@ -21,14 +21,14 @@ Definition crs_rep_aux {t} (mval: matrix t) (cols: Z) (vals: list (ftype t)) (co
   Zlength row_ptr = 1 + Zlength mval /\
   Zlength vals = Znth (Zlength mval) row_ptr /\
   Zlength col_ind = Znth (Zlength mval) row_ptr /\
-  sorted Z.le (0::row_ptr ++ [Int.max_unsigned]) /\ 
+  sorted Z.le (0::row_ptr ++ [Int.max_unsigned]) /\
   forall j, 0 <= j < Zlength mval ->
-        crs_row_rep cols 
+        crs_row_rep cols
              (sublist (Znth j row_ptr) (Znth (j+1) row_ptr) vals)
              (sublist (Znth j row_ptr) (Znth (j+1) row_ptr) col_ind)
              (Znth j mval).
 
-Lemma sorted_app_e1: 
+Lemma sorted_app_e1:
  forall {A} {HA: Inhabitant A} (le: A -> A -> Prop) al bl,
   sorted le (al++bl) -> sorted le al.
 Proof.
@@ -89,7 +89,7 @@ split3; [ | | split3].
        rewrite !Znth_pos_cons in H by lia.
        rewrite !Z.add_simpl_r in H.
        rewrite !Znth_map by lia.
-       assert (0 <= Znth j row_ptr - r <= Znth (j + 1) row_ptr - r) 
+       assert (0 <= Znth j row_ptr - r <= Znth (j + 1) row_ptr - r)
                     by (clear - H0 H1 SORT L; abstract list_solve).
        assert (Znth (j + 1) row_ptr - r <= Zlength col_ind - r)
                     by (clear - H0 H1 SORT L L1; abstract list_solve).
@@ -120,11 +120,11 @@ induction 1; intros.
   + subst. rewrite Znth_0_cons. apply crs_row_rep_cols_nonneg in H. lia.
   + rewrite Znth_pos_cons by lia.
      specialize (IHcrs_row_rep (j-1) ltac:(list_solve)).
-     rewrite Znth_map in IHcrs_row_rep by list_solve. 
+     rewrite Znth_map in IHcrs_row_rep by list_solve.
      lia.
 Qed.
 
-Lemma crs_row_rep_property: 
+Lemma crs_row_rep_property:
  forall {t} (P: ftype t -> Prop) cols (vals: list (ftype t)) col_ind vval,
   crs_row_rep cols vals col_ind vval ->
   Forall P vval -> Forall P vals.
@@ -188,7 +188,7 @@ apply Forall2_Znth with (i:=z) in Hvval; auto.
 lia.
 Qed.
 
-Definition partial_row {t} (i: Z) (h: Z) (vals: list (ftype t)) (col_ind: list Z) (row_ptr: list Z) 
+Definition partial_row {t} (i: Z) (h: Z) (vals: list (ftype t)) (col_ind: list Z) (row_ptr: list Z)
                 (vval: vector t) : ftype t :=
  let vals' := sublist (Znth i row_ptr) h vals in
  let col_ind' := sublist (Znth i row_ptr) h col_ind in
@@ -234,7 +234,7 @@ assert (COL := crs_rep_matrix_cols _ _ _ _ _ H0).
 red in COL.
 destruct H0 as [? [? [? [? ?]]]].
 specialize (H4 _ H).
-set (vals' := sublist _ _ vals) in *. clearbody vals'. 
+set (vals' := sublist _ _ vals) in *. clearbody vals'.
 set (col_ind' := sublist _ _ col_ind)  in *. clearbody col_ind'.
 unfold matrix_rows in *.
 rewrite Znth_map by list_solve.
@@ -283,7 +283,7 @@ destruct vval as [ | v0 vval'].
    inv FINvals'.
    rewrite IHvals; auto. f_equal. f_equal.
    inv H0.
-   list_solve. 
+   list_solve.
    inv H0; auto. clear; list_solve.
  * clear - FINvval FINrow.
     inv FINvval.
@@ -293,7 +293,7 @@ destruct vval as [ | v0 vval'].
     destruct vval'; simpl; auto.
     inv H2. inv FINrow.
     apply IHv; auto.
-    apply BFMA_mor; auto. 
+    apply BFMA_mor; auto.
 -
   inv FINrow. rename H1 into FINx. rename H2 into FINrow.
   inv FINvals'. clear H1. rename H2 into FINvals.
@@ -346,7 +346,7 @@ Lemma partial_row_next:
   Znth i row_ptr <= h < Zlength vals ->
   Zlength vals = Zlength col_ind ->
   crs_rep_aux mval cols vals col_ind row_ptr ->
-partial_row i (h + 1) vals col_ind row_ptr vval = 
+partial_row i (h + 1) vals col_ind row_ptr vval =
 BFMA (Znth h vals) (Znth (Znth h col_ind) vval)
   (partial_row i h vals col_ind row_ptr vval).
 Proof.

C/spec_sparse.v

@@ -15,11 +15,11 @@ Open Scope logic.
 Definition t_crs := Tstruct _crs_matrix noattr.
 
 Definition crs_rep (sh: share) (mval: matrix Tdouble) (p: val) : mpred :=
-  EX v: val, EX ci: val, EX rp: val, 
+  EX v: val, EX ci: val, EX rp: val,
   EX cols, EX vals: list (ftype Tdouble), EX col_ind: list Z, EX row_ptr: list Z,
   !! 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 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.
 
@@ -52,7 +52,7 @@ Definition crs_row_vector_multiply_spec :=
          data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v)
  POST [ tdouble ]
    EX s: ftype Tdouble,
-    PROP(feq s (dotprod (Znth i mval) vval)) 
+    PROP(feq s (dotprod (Znth i mval) vval))
     RETURN(Vfloat s)
     SEP (crs_rep sh1 mval m;
           data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v).
@@ -70,15 +70,15 @@ Definition crs_matrix_vector_multiply_byrows_spec :=
              Forall (Forall finite) mval)
     PARAMS(m; v; p)
     SEP (crs_rep sh1 mval m;
-         data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v; 
+         data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v;
          data_at_ sh3 (tarray tdouble (matrix_rows mval)) p)
  POST [ tvoid ]
    EX result: vector Tdouble,
-    PROP(Forall2 feq result (matrix_vector_mult mval vval)) 
+    PROP(Forall2 feq result (matrix_vector_mult mval vval))
     RETURN()
     SEP (crs_rep sh1 mval m;
-          data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v; 
-          data_at sh3 (tarray tdouble (matrix_rows mval)) 
+          data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v;
+          data_at sh3 (tarray tdouble (matrix_rows mval))
              (map Vfloat result) p).
 
 Definition crs_matrix_vector_multiply_spec :=
@@ -94,18 +94,18 @@ Definition crs_matrix_vector_multiply_spec :=
              Forall (Forall finite) mval)
     PARAMS(m; v; p)
     SEP (crs_rep sh1 mval m;
-         data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v; 
+         data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v;
          data_at_ sh3 (tarray tdouble (matrix_rows mval)) p)
  POST [ tvoid ]
    EX result: vector Tdouble,
-    PROP(Forall2 feq result (matrix_vector_mult mval vval)) 
+    PROP(Forall2 feq result (matrix_vector_mult mval vval))
     RETURN()
     SEP (crs_rep sh1 mval m;
-          data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v; 
-          data_at sh3 (tarray tdouble (matrix_rows mval)) 
+          data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v;
+          data_at sh3 (tarray tdouble (matrix_rows mval))
              (map Vfloat result) p).
 
-Definition SparseASI : funspecs := [ 
+Definition SparseASI : funspecs := [
    crs_matrix_rows_spec;
    crs_row_vector_multiply_spec;
    crs_matrix_vector_multiply_byrows_spec;

C/verif_sparse.v

@@ -11,13 +11,13 @@ Open Scope logic.
 
 Definition the_loop_body : statement.
 let c := constr:(f_crs_matrix_vector_multiply) in
-let c := eval red in c in 
+let c := eval red in c in
 match c with context [Sloop (Ssequence _ ?body)] =>
  exact body
 end.
 Defined.
 
-Lemma crs_multiply_loop_body: 
+Lemma crs_multiply_loop_body:
  forall (Espec : OracleKind)  (sh1 sh2 sh3 : share)
    (m : val) (mval : matrix Tdouble)
    (v : val) (vval : vector Tdouble)
@@ -43,9 +43,9 @@ Lemma crs_multiply_loop_body:
 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 _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 _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;
@@ -62,7 +62,7 @@ semax (func_tycontext f_crs_matrix_vector_multiply Vprog Gprog [])
       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 _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;
@@ -86,15 +86,15 @@ assert(0 <= i + 1 < Zlength row_ptr)
   by (rewrite H4; unfold matrix_rows in H6; lia).
 forward.
 
-forward_loop 
+forward_loop
   (EX h:Z, (PROP (Znth i row_ptr <= h <= Znth (i+1) row_ptr )
    LOCAL (
    temp _s (Vfloat (partial_row i h vals col_ind row_ptr vval));
    temp _i (Vint (Int.repr i));
    temp _h (Vint  (Int.repr h));
-   temp _next (Vint (Int.repr (Znth (i+1) row_ptr))); 
+   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 _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;
@@ -110,9 +110,9 @@ forward_loop
    LOCAL (
    temp _s (Vfloat r);
    temp _i (Vint (Int.repr i));
-   temp _next (Vint (Int.repr (Znth (i+1) row_ptr))); 
+   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 _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;
@@ -134,7 +134,7 @@ forward_if.
  +
   assert (0 <= Znth i row_ptr) by list_solve.
   rewrite Int.unsigned_repr in H14 by list_solve.
-  rewrite Int.unsigned_repr in H14 
+  rewrite Int.unsigned_repr in H14
      by (clear - H4 H6 H9; unfold matrix_rows in H6; list_solve).
   forward.
   apply prop_right. rewrite H8. unfold matrix_rows in *; list_solve.
@@ -151,13 +151,13 @@ forward_if.
      assert (Znth (i+1) row_ptr <= Zlength col_ind) by list_solve.
      clear - COLS H H17 H14 H6 H10 H15 H18.
       specialize (H10 _ H6).
-      replace (Znth h col_ind) with 
+      replace (Znth h col_ind) with
               (Znth (h-Znth i row_ptr) (sublist (Znth i row_ptr) (Znth (i+1) row_ptr) col_ind))
          by list_solve.
 
   pose proof (crs_row_rep_col_range _ _ _ _ H10).
   specialize (H0 (h - Znth i row_ptr)).
-  autorewrite with sublist in H0. autorewrite with sublist. 
+  autorewrite with sublist in H0. autorewrite with sublist.
   rewrite <- (sublist.Forall_Znth _ _ _ H6 H), (sublist.Forall_Znth _ _ _ H6 COLS).
   apply H0. list_solve.
   }
@@ -170,15 +170,15 @@ forward_if.
   Exists (h+1).
   entailer!.
   f_equal.
-  change (Binary.Bfma _ _ _ _ _ _ _ _ _) with 
+  change (Binary.Bfma _ _ _ _ _ _ _ _ _) with
    (@BFMA _ Tdouble (Znth h vals) (Znth (Znth h col_ind) vval)
      (partial_row i h vals col_ind row_ptr vval)
   ).
   eapply partial_row_next; try eassumption; lia.
 +
- forward. 
+ forward.
  Exists (partial_row i h vals col_ind row_ptr vval).
- entailer!. 
+ entailer!.
  replace h with (Znth (i+1) row_ptr).
  erewrite partial_row_end; try eassumption.
  unfold matrix_vector_mult.
@@ -188,7 +188,7 @@ forward_if.
  specialize (H10 i H6).
  unfold matrix_rows in *.
   rewrite Int.unsigned_repr in H14 by list_solve.
-  rewrite Int.unsigned_repr in H14 
+  rewrite Int.unsigned_repr in H14
      by (clear - H4 H6 H9; unfold matrix_rows in H6; list_solve).
  lia.
 -
@@ -210,15 +210,15 @@ forward.
 freeze FR1 := (data_at sh1 _ _ _).
 rename v0 into vp.
 assert_PROP (0 <= 0 < Zlength row_ptr)
-  by (entailer!; rewrite !Zlength_map in H12; rewrite H12; clear -H3; lia). 
+  by (entailer!; rewrite !Zlength_map in H12; rewrite H12; clear -H3; lia).
 forward.
 forward_for_simple_bound (matrix_rows mval)
   (EX i:Z, EX result: list (ftype Tdouble),
-   PROP(Forall2 feq result (sublist 0 i (matrix_vector_mult mval vval))) 
-   LOCAL (temp _next (Vint (Int.repr (Znth i row_ptr))); 
+   PROP(Forall2 feq result (sublist 0 i (matrix_vector_mult mval vval)))
+   LOCAL (temp _next (Vint (Int.repr (Znth i row_ptr)));
    temp _row_ptr rp; temp _col_ind ci; temp _val vp;
 (*   temp _cols (Vint (Int.repr cols));*)
-   temp _rows (Vint (Int.repr (matrix_rows mval))); 
+   temp _rows (Vint (Int.repr (matrix_rows mval)));
    temp _m m; temp _v v; temp _p p)
    SEP (FRZL FR1;
    data_at sh1 (tarray tdouble (Zlength col_ind)) (map Vfloat vals) vp;
@@ -227,7 +227,7 @@ forward_for_simple_bound (matrix_rows mval)
    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)) 
+   data_at sh3 (tarray tdouble (matrix_rows mval))
       (map Vfloat result ++ Zrepeat Vundef (matrix_rows mval - i)) p))%assert.
 -
 Exists (@nil (ftype Tdouble)). simpl app.
@@ -252,7 +252,7 @@ unfold matrix_rows in H6.
 unfold matrix_vector_mult. rewrite Znth_map by auto. auto.
 apply derives_refl'. f_equal.
 assert (Zlength result = i).
- apply Forall2_Zlength in H7. 
+ apply Forall2_Zlength in H7.
  clear - H7 H6. unfold matrix_rows, matrix_vector_mult in *. list_solve.
 clear - H24 H6.
 unfold matrix_rows in *.

C/verif_sparse_byrows.v

@@ -60,7 +60,7 @@ assert (COLS: cols = Zlength vval). {
 }
 destruct H5 as [H2' [H7 [H8 [H9 H10]]]].
 unfold matrix_rows in *.
-assert (H9': 0 <= Znth i row_ptr <= Znth (i+1) row_ptr 
+assert (H9': 0 <= Znth i row_ptr <= Znth (i+1) row_ptr
             /\ Znth (i+1) row_ptr <= Znth (Zlength mval) row_ptr <= Int.max_unsigned)
    by (clear - H9 H2' H2; list_solve).
 clear H9. destruct H9' as [H9 H9'].
@@ -69,7 +69,7 @@ forward_for_simple_bound (Znth (i + 1) row_ptr)
    LOCAL (
    temp _s (Vfloat (partial_row i h vals col_ind row_ptr vval));
    temp _i (Vint (Int.repr i));
-   temp _hi (Vint (Int.repr (Znth (i+1) row_ptr))); 
+   temp _hi (Vint (Int.repr (Znth (i+1) row_ptr)));
    temp _row_ptr rp; temp _col_ind ci; temp _val vp;
    temp _m m; temp _v v)
    SEP (FRZL FR1;
@@ -81,13 +81,13 @@ forward_for_simple_bound (Znth (i + 1) row_ptr)
    data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v))%assert.
 -
  forward.
- change float with (ftype Tdouble) in *. 
+ change float with (ftype Tdouble) in *.
  EExists. entailer!.
  f_equal. erewrite partial_row_start. reflexivity. eassumption.
 -
 rename i0 into h.
 forward.
-change float with (ftype Tdouble) in *. 
+change float with (ftype Tdouble) in *.
 forward.
 assert (0 <= Znth h col_ind < Zlength vval). {
     specialize (H10 _ H2).
@@ -103,7 +103,7 @@ forward_call (Znth h vals, Znth (Znth h col_ind) vval, partial_row i h vals col_
 forward.
 entailer!.
 f_equal.
-change (Binary.Bfma _ _ _ _ _ _ _ _ _) with 
+change (Binary.Bfma _ _ _ _ _ _ _ _ _) with
    (@BFMA _ Tdouble (Znth h vals) (Znth (Znth h col_ind) vval)
      (partial_row i h vals col_ind row_ptr vval)
   ).
@@ -127,12 +127,12 @@ start_function.
 forward_call.
 forward_for_simple_bound (Zlength mval)
   (EX i:Z, EX result: list (ftype Tdouble),
-   PROP(Forall2 feq result (sublist 0 i (matrix_vector_mult mval vval))) 
-   LOCAL (temp _rows (Vint (Int.repr (matrix_rows mval))); 
+   PROP(Forall2 feq result (sublist 0 i (matrix_vector_mult mval vval)))
+   LOCAL (temp _rows (Vint (Int.repr (matrix_rows mval)));
    temp _m m; temp _v v; temp _p p)
    SEP (crs_rep sh1 mval m;
    data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v;
-   data_at sh3 (tarray tdouble (matrix_rows mval)) 
+   data_at sh3 (tarray tdouble (matrix_rows mval))
       (map Vfloat result ++ Zrepeat Vundef (matrix_rows mval - i)) p))%assert.
 - unfold matrix_rows in H0; lia.
 - Exists (@nil (ftype Tdouble)). simpl app. entailer!.
@@ -141,11 +141,11 @@ forward_for_simple_bound (Zlength mval)
    Intros s.
    unfold matrix_rows in H0.
    forward.
-   progress change float with (ftype Tdouble) in *. 
+   progress change float with (ftype Tdouble) in *.
    Exists (result ++ [s]).
-   entailer!. 
+   entailer!.
    clear H11 H12 H10 H9 H8 H7 PNp PNv PNm.
-   assert (Zlength (matrix_vector_mult mval vval) = Zlength mval). 
+   assert (Zlength (matrix_vector_mult mval vval) = Zlength mval).
       unfold matrix_vector_mult. list_solve.
    rewrite (sublist_split 0 i (i+1)) by list_solve.
    apply Forall2_app.