CFEM.C.verif_matrix

Require Import VST.floyd.proofauto.
From vcfloat Require Import FPStdCompCert FPStdLib.
From VSTlib Require Import spec_math spec_malloc.
From LAProof.accuracy_proofs Require Import solve_model.
From LAProof.C Require Import VSU_densemat spec_alloc floatlib matrix_model.
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 CFEM.C Require Import matrix spec_matrix.

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

Unset Implicit Arguments.
Open Scope logic.

Section import_densemat.
Import spec_densemat.
Definition matrix_imported_specs :=
  [densemat_addto_spec; densemat_clear_spec; densemat_norm2_spec; densemat_print_spec;
   sqrt_spec ].
End import_densemat.

Definition matrix_E : funspecs := [].
Definition matrix_internal_specs : funspecs := matrix_ASI.

Definition Gprog := matrix_imported_specs ++ matrix_internal_specs.

Ltac destruct_it B ::=
 match B with
 | ?C _ ⇒ destruct_it C
 | let '(x,y) := ?A in _ ⇒ destruct A as [x y]
 | match ?A with _ ⇒ _ end ⇒
    match type of A with ?tA ⇒ let uA := eval hnf in tA in
     match uA with
     | @sigT _ (fun x ⇒ _) ⇒ destruct A as [x A]
     end end
 end.

Ltac densemat_lemmas.destruct_it B ::=
 match B with
 | ?C _ ⇒ destruct_it C
 | let '(x,y) := ?A in _ ⇒ destruct A as [x y]
 | match ?A with _ ⇒ _ end ⇒
    match type of A with ?tA ⇒ let uA := eval hnf in tA in
     match uA with
     | @sigT _ (fun x ⇒ _) ⇒ destruct A as [x A]
     end end
 end.

Lemma body_matrix_add: semax_body Vprog Gprog f_matrix_add matrix_add_spec.

Lemma body_casted_densemat_add: semax_body Vprog Gprog f_casted_densemat_add casted_densemat_add_spec.

Lemma body_matrix_clear: semax_body Vprog Gprog f_matrix_clear matrix_clear_spec.

Lemma body_casted_densemat_clear: semax_body Vprog Gprog f_casted_densemat_clear casted_densemat_clear_spec.

Lemma body_matrix_norm2: semax_body Vprog Gprog f_matrix_norm2 matrix_norm2_spec.

Lemma body_matrix_norm: semax_body Vprog Gprog f_matrix_norm matrix_norm_spec.
Locate sqrt_ff.
Qed.

Lemma body_casted_densemat_norm2: semax_body Vprog Gprog f_casted_densemat_norm2 casted_densemat_norm2_spec.

Lemma body_matrix_print: semax_body Vprog Gprog f_matrix_print matrix_print_spec.

Lemma body_casted_densemat_print: semax_body Vprog Gprog f_casted_densemat_print casted_densemat_print_spec.

Lemma body_init_matrix_dense: semax_body Vprog Gprog f_init_matrix_dense init_matrix_dense_spec.

Require Import VST.floyd.VSU.

Definition matrixVSU: @VSU NullExtension.Espec
         matrix_E matrix_imported_specs
         ltac:(QPprog prog) matrix_ASI (fun _ ⇒ TT).