LAProof.C.spec_sparse: VST specifications of functions on sparse matrices.

Corresponds to C program sparse.h and sparse.c

The principal funspecs here are:

csr_matrix_vector_multiply_spec, specifying correctness of the C program for Compressed Sparse Row floating-point matrix-vector multiply w.r.t. a list-of-lists functional model of matrices;
csr_matrix_vector_multiply_spec', specifying correctness of the same program w.r.t. a MathComp floating-point functional model
along with the theorem csr_matrix_vector_multiply_spec_sub that the former implies the latter.

See also section IV of the paper, "LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs", https://www.cs.princeton.edu/~appel/papers/LAProof.pdf

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

From mathcomp Require ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require fintype finfun bigop finset fingroup perm order.
From mathcomp Require div ssralg countalg finalg zmodp matrix.
From mathcomp.zify Require Import ssrZ zify.

Require LAProof.accuracy_proofs.export.
Module F := LAProof.accuracy_proofs.mv_mathcomp.F.

Now we undo all the settings that mathcomp has modified

Unset Implicit Arguments.

#[export] Instance CompSpecs : compspecs.
Definition Vprog : varspecs.

Open Scope logic.

Definition t_csr := Tstruct _csr_matrix noattr.

Definition csr_rep (sh: share) (mval: matrix Tdouble) (p: val) : mpred :=
  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,
  !! 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.

Definition csr_matrix_rows_spec :=
DECLARE _csr_matrix_rows
WITH sh: share, m: val, mval: matrix Tdouble
PRE [ tptr t_csr ]
    PROP (readable_share sh; matrix_rows mval < Int.max_unsigned)
    PARAMS (m)
    SEP (csr_rep sh mval m)
POST [ tuint ]
    PROP ()
    RETURN (Vint (Int.repr (matrix_rows mval)))
    SEP (csr_rep sh mval m).

Definition csr_row_vector_multiply_spec {NAN : FPCore.Nans} :=
DECLARE _csr_row_vector_multiply
WITH sh1: share, sh2: share, sh3: share,
      m: val, mval: matrix Tdouble, v: val, vval: vector Tdouble, i: Z
PRE [ tptr t_csr, tptr tdouble, tuint ]
    PROP(readable_share sh1; readable_share sh2; writable_share sh3;
             matrix_cols mval (Zlength vval);
             matrix_rows mval < Int.max_unsigned;
             Zlength vval < Int.max_unsigned;
             0 ≤ i < matrix_rows mval;
             Forall finite vval;
             Forall (Forall finite) mval)
    PARAMS(m; v; Vint (Int.repr i))
    SEP (csr_rep sh1 mval m;
         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))
    RETURN(Vfloat s)
    SEP (csr_rep sh1 mval m;
          data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v).

Definition csr_matrix_vector_multiply_byrows_spec {NAN : FPCore.Nans} :=
DECLARE _csr_matrix_vector_multiply_byrows
WITH sh1: share, sh2: share, sh3: share,
      m: val, mval: matrix Tdouble, v: val, vval: vector Tdouble, p: val
PRE [ tptr t_csr, tptr tdouble, tptr tdouble ]
    PROP(readable_share sh1; readable_share sh2; writable_share sh3;
             matrix_cols mval (Zlength vval);
             matrix_rows mval < Int.max_unsigned;
             Zlength vval < Int.max_unsigned;
             Forall finite vval;
             Forall (Forall finite) mval)
    PARAMS(m; v; p)
    SEP (csr_rep sh1 mval m;
         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))
    RETURN()
    SEP (csr_rep sh1 mval m;
          data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v;
          data_at sh3 (tarray tdouble (matrix_rows mval))
             (map Vfloat result) p).

Definition csr_matrix_vector_multiply_spec {NAN : FPCore.Nans} :=
DECLARE _csr_matrix_vector_multiply
WITH sh1: share, sh2: share, sh3: share,
      m: val, mval: matrix Tdouble, v: val, vval: vector Tdouble, p: val
PRE [ tptr t_csr, tptr tdouble, tptr tdouble ]
    PROP(readable_share sh1; readable_share sh2; writable_share sh3;
             matrix_cols mval (Zlength vval);
             matrix_rows mval < Int.max_unsigned;
             Zlength vval < Int.max_unsigned;
             Forall finite vval;
             Forall (Forall finite) mval)
    PARAMS(m; v; p)
    SEP (csr_rep sh1 mval m;
         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))
    RETURN()
    SEP (csr_rep sh1 mval m;
          data_at sh2 (tarray tdouble (Zlength vval)) (map Vfloat vval) v;
          data_at sh3 (tarray tdouble (matrix_rows mval))
             (map Vfloat result) p).

Section MathComp.

Among all the mathcomp stuff, these are the files that we *do* want to Import:

Local Import fintype matrix mv_mathcomp.

Definition csr_matrix_vector_multiply_spec' {NAN : FPCore.Nans} :=
DECLARE _csr_matrix_vector_multiply
WITH sh1: share, sh2: share, sh3: share,
      mp: val, X: { mn & 'M[ftype Tdouble]_(fst mn, snd mn) × 'cV[ftype Tdouble]_(snd mn)}%type, v: val, p: val
PRE [ tptr t_csr, tptr tdouble, tptr tdouble ] let '(existT _ (rows,cols) (A,x)) := X in
    PROP(readable_share sh1; readable_share sh2; writable_share sh3;
             Z.of_nat rows < Int.max_unsigned; Z.of_nat cols < Int.max_unsigned;
             (∀ (i: 'I_cols), finite (x i ord0));
             (∀ (i: 'I_rows) (j:'I_cols), finite (A i j)))
    PARAMS(mp; v; p)
    SEP (csr_rep sh1 (listlist_of_mx A) mp;
         data_at sh2 (tarray tdouble (Z.of_nat cols)) (map Vfloat (list_of_cV x)) v;
         data_at_ sh3 (tarray tdouble (Z.of_nat rows)) p)
POST [ tvoid ] let '(existT _ (rows,cols) (A,x)) := X in
   EX result: 'cV[ftype Tdouble]_rows,
    PROP(∀ i, feq (result i ord0) (F.FMA_mulmx A x i ord0))
    RETURN()
    SEP (csr_rep sh1 (listlist_of_mx A) mp;
          data_at sh2 (tarray tdouble (Z.of_nat cols)) (map Vfloat (list_of_cV x)) v;
          data_at sh3 (tarray tdouble (Z.of_nat rows))
             (map Vfloat (list_of_cV result)) p).

Lemma zip_combine: @seq.zip = @combine.

Lemma foldl_fold_left: ∀ A B (f: B → A → B) (b: B) (al: list A),
   seq.foldl f b al = fold_left f al b.

Lemma mc_matrix_vector_mult: @floatlib.matrix_vector_mult = @matrix_vector_mult.

Lemma matrix_cols_nat':
    ∀ t (al: list (list (ftype t))) n, matrix_cols al (Z.of_nat n) ↔ matrix_cols_nat al n.

Lemma Forall2_nth: ∀ {A B} `{d1: Inhabitant A} `{d2: Inhabitant B} (P: A → B → Prop)
       (l1: list A) (l2: list B),
  Forall2 P l1 l2 → ∀ i: nat, (i < length l1)%nat → P (seq.nth d1 l1 i) (seq.nth d2 l2 i).

Lemma csr_matrix_vector_multiply_spec_sub:
   funspec_sub (snd csr_matrix_vector_multiply_spec) (snd (csr_matrix_vector_multiply_spec')).
End MathComp.

Definition SparseASI : funspecs := [
   csr_matrix_rows_spec ;
   csr_row_vector_multiply_spec ;
   csr_matrix_vector_multiply_byrows_spec ;
   csr_matrix_vector_multiply_spec ].

Definition SubsetMathASI := [fma_spec].
Definition Gprog : funspecs := SubsetMathASI ++ SparseASI.

Lemma BFMA_eq:
   ∀ H H' H0 (x y z : Binary.binary_float (fprec Tdouble) (femax Tdouble)),
  Binary.Bfma (fprec Tdouble) (femax Tdouble) H H0
    (FPCore.fma_nan (fprec Tdouble) (femax Tdouble) H') BinarySingleNaN.mode_NE x y z =
  BFMA x y z.