LAProof.C.cblas.stride_model
Require Import VST.floyd.proofauto.
strided_from start inc N X is the logical length-N vector whose
element i is stored at array index start + i×inc.
Definition strided_from {A} `{Inhabitant A}
(start inc N : Z) (X : list A) : list A :=
map (fun i ⇒ Znth (start + i×inc) X) (upto (Z.to_nat N)).
(start inc N : Z) (X : list A) : list A :=
map (fun i ⇒ Znth (start + i×inc) X) (upto (Z.to_nat N)).
The starting index computed by GSL's OFFSET(N,inc) macro.
Definition blas_offset (N inc : Z) : Z :=
if 0 <? inc then 0 else (N-1) × (-inc).
Definition blas_strided {A} `{Inhabitant A}
(inc N : Z) (X : list A) : list A :=
strided_from (blas_offset N inc) inc N X.
Lemma Zlength_strided_from: ∀ {A} `{Inhabitant A} start inc N (X: list A),
0 ≤ N → Zlength (strided_from start inc N X) = N.
Lemma strided_from_snoc: ∀ {A} `{Inhabitant A} start inc k (X: list A),
0 ≤ k →
strided_from start inc (k+1) X =
strided_from start inc k X ++ [Znth (start + k×inc) X].
if 0 <? inc then 0 else (N-1) × (-inc).
Definition blas_strided {A} `{Inhabitant A}
(inc N : Z) (X : list A) : list A :=
strided_from (blas_offset N inc) inc N X.
Lemma Zlength_strided_from: ∀ {A} `{Inhabitant A} start inc N (X: list A),
0 ≤ N → Zlength (strided_from start inc N X) = N.
Lemma strided_from_snoc: ∀ {A} `{Inhabitant A} start inc k (X: list A),
0 ≤ k →
strided_from start inc (k+1) X =
strided_from start inc k X ++ [Znth (start + k×inc) X].