LAProof.C.VSU_sparse

Require Import VST.floyd.proofauto VST.floyd.VSU.
Require Import vcfloat.VCFloat.
Require Import vcfloat.FPStdCompCert.
Require Import VSTlib.spec_math.
From LAProof.C Require Import sparse sparse_model spec_sparse
                            floatlib verif_sparse verif_sparse_byrows.


Open Scope logic.

#[local] Existing Instance NullExtension.Espec.
Definition sparseImports : funspecs := [fma_spec].
Definition SparseVSU {NAN : FPCore.Nans}: VSU nil sparseImports ltac:(QPprog prog) SparseASI emp.