From VST.floyd Require Import proofauto VSU.
From LAProof.C Require Import densemat spec_alloc spec_densemat floatlib matrix_model.
From vcfloat Require Import FPStdCompCert FPStdLib.
Require Import VSTlib.spec_math VSTlib.spec_malloc.
Require Import Coq.Classes.RelationClasses.

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.
Import fintype matrix.

From LAProof.C Require Import densemat_lemmas verif_densemat verif_densemat_mult verif_densemat_cholesky.

Unset Implicit Arguments.

Open Scope logic.

Ltac new_simpl_fst_snd :=
  match goal with |- context[@fst ident funspec ?A] ⇒
     let j := eval hnf in A in
     match j with (?x,?y) ⇒
      try change (fst A) with x;
      try change (snd A) with y
     end
    end.

Ltac SF_vacuous ::=
 try new_simpl_fst_snd;
 match goal with |- SF _ _ _ (vacuous_funspec _) ⇒ idtac end;
 match goal with H: @eq compspecs _ _ |- _ ⇒ rewrite <- H end;
red; red; repeat simple apply conj;
[ reflexivity
| repeat apply Forall_cons;
  try apply Forall_nil; reflexivity
| repeat constructor; simpl; rep_lia
| reflexivity
| split3; [reflexivity | reflexivity | intros; apply semax_vacuous]
| eexists; split; compute; reflexivity
].

Definition densematVSU: @VSU NullExtension.Espec
         densemat_E densemat_imported_specs
         ltac:(QPprog prog) densematASI (fun _ ⇒ TT).