LAProof.C.sparse_model

Require Import VST.floyd.proofauto.
Require Import vcfloat.VCFloat.
Require Import vcfloat.FPCompCert.
Require Import VSTlib.spec_math.
Require Import LAProof.C.floatlib.


Open Scope logic.

Inductive crs_row_rep {t: type} :
  ∀ (cols: Z) (vals: list (ftype t)) (col_ind: list Z)
  (v: list (ftype t)), Prop :=
 | crs_row_rep_nil: crs_row_rep 0%Z nil nil nil
 | crs_row_rep_zero: ∀ cols vals col_ind v,
          crs_row_rep (cols-1) vals (map Z.pred col_ind) v →
          crs_row_rep cols vals col_ind (Zconst t 0 :: v)
 | crs_row_rep_val: ∀ cols x vals col_ind v,
          crs_row_rep (cols-1) vals (map Z.pred col_ind) v →
          crs_row_rep cols (x::vals) (0::col_ind) (x::v).

Definition crs_rep_aux {t: type}
  (mval: matrix t) (cols: Z) (vals: list (ftype t)) (col_ind: list Z) (row_ptr: list Z) : Prop :=
  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]) ∧
  ∀ j, 0 ≤ j < Zlength mval →
        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:
 ∀ {A} {HA: Inhabitant A} (le: A → A → Prop) al bl,
  sorted le (al++bl) → sorted le al.

Lemma crs_rep_matrix_cols {t: type}:
   ∀ (mval: matrix t) cols vals col_ind row_ptr,
   crs_rep_aux mval cols vals col_ind row_ptr → matrix_cols mval cols.

Lemma crs_row_rep_cols_nonneg:
 ∀ {t} cols (vals: list (ftype t)) col_ind vval,
  crs_row_rep cols vals col_ind vval →
  0 ≤ cols.

Lemma crs_row_rep_col_range:
 ∀ {t} cols (vals: list (ftype t)) col_ind vval,
  crs_row_rep cols vals col_ind vval →
   ∀ j, 0 ≤ j < Zlength col_ind → 0 ≤ Znth j col_ind < cols.

Lemma crs_row_rep_property:
 ∀ {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.

Fixpoint rowmult {NAN: Nans} {t} (s: ftype t)
            (vals: list (ftype t)) (col_ind: list Z) (vval: list (ftype t)) :=
 match vals, col_ind with
  | v1::vals', c1::col_ind' ⇒ rowmult (BFMA v1 (Znth c1 vval) s) vals' col_ind' vval
  | _, _ ⇒ s
 end.

Add Parametric Morphism {NAN: Nans} {t: type} : rowmult
  with signature (@feq t) ==> Forall2 feq ==> @eq (list Z) ==> Forall2 feq ==> feq
  as rowmult_mor.

Add Parametric Morphism {NAN: Nans} {t: type} : rowmult
  with signature (@feq t) ==> Forall2 strict_feq ==> @eq (list Z) ==> Forall2 strict_feq ==> feq
  as rowmult_stricter_mor.

Definition partial_row {NAN: Nans} {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
   rowmult (Zconst t 0) vals' col_ind' vval.

Lemma partial_row_start {NAN: Nans}:
 ∀ {t} i (mval: matrix t) cols vals col_ind row_ptr vval,
  crs_rep_aux mval cols vals col_ind row_ptr →
  partial_row i (Znth i row_ptr) vals col_ind row_ptr vval = Zconst t 0.

Lemma strict_feq_i :
 ∀ {t} (x: ftype t), finite x → strict_feq x x.

Lemma strict_floatlist_eqv_i:
  ∀ {t} (vec: list (ftype t)), Forall finite vec → Forall2 strict_feq vec vec.
#[export] Hint Resolve strict_feq_i strict_floatlist_eqv_i : core.

Lemma partial_row_end {NAN: Nans}:
 ∀ {t} i (mval: matrix t) cols vals col_ind row_ptr vval
  (FINvval: Forall finite vval)
  (FINmval: Forall (Forall finite) mval)
  (LEN: Zlength vval = cols),
  0 ≤ i < matrix_rows mval →
  crs_rep_aux mval cols vals col_ind row_ptr →
  feq (partial_row i (Znth (i+1) row_ptr) vals col_ind row_ptr vval)
      (Znth i (matrix_vector_mult mval vval)).

Lemma rowmult_app {NAN : Nans }:
 ∀ {t} (s: ftype t) vals1 col_ind1 vals2 col_ind2 vvals,
   Zlength vals1 = Zlength col_ind1 →
   rowmult s (vals1++vals2) (col_ind1++col_ind2) vvals =
   rowmult (rowmult s vals1 col_ind1 vvals) vals2 col_ind2 vvals.

Lemma partial_row_next {NAN : Nans }:
 ∀ {t} i h (mval: matrix t) cols vals col_ind row_ptr vval,
  0 ≤ Znth i row_ptr →
  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 =
BFMA (Znth h vals) (Znth (Znth h col_ind) vval)
  (partial_row i h vals col_ind row_ptr vval).