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 (*Import*) ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require (*Import*) fintype finfun bigop finset fingroup perm order.
From mathcomp Require (*Import*) 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 ::= (* remove this if/when VST 2.17 incorporates it. *)
 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 ::= (* remove this when LAProof is updated for VST 2.16 *)
 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.

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).