LAProof.C.verif_densemat: VST proofs of functions on dense matrices.

Corresponds to C program densemat.c

Prologue.

For explanation see the prologue of LAProof.C.spec_densemat
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.

Require Import LAProof.C.densemat_lemmas.

Unset Implicit Arguments.

Open Scope logic.

densemat_malloc verification

Lemma body_densemat_malloc: semax_body Vprog Gprog f_densemat_malloc densemat_malloc_spec.

densemat_free verification

Lemma body_densemat_free: semax_body Vprog Gprog f_densemat_free densemat_free_spec.

Unpacking dependently typed WITH components

When a funspec has a dependently typed package such as WITH X: {mn & 'M[option (ftype the_type)]_(fst mn, snd mn)}, the funspec may destruct it by a let-definition immediately after PRE or POST, such as let '(existT _ (m,n) M) := X in. Standard VST 2.15's start_function tactic cannot process such funspects. Here we add a new feature to start_function. See also: https://github.com/PrincetonUniversity/VST/issues/839

densemat_clear verification


Lemma body_densematn_clear: semax_body Vprog Gprog f_densematn_clear densematn_clear_spec.

This proof demonstrates a good way to prove a function call to a function whose funspec contains a dependently typed package. Before doing the forward_call, build the package using existT. There will be no use for X after the forward_call, so it can be cleared immediately.

Lemma body_densemat_clear: semax_body Vprog Gprog f_densemat_clear densemat_clear_spec.
Proof.
start_function.
rename X into M.
unfold densemat in POSTCONDITION|-*.
Intros.
forward.
forward.
pose (X := existT _ (m,n) M : {mn & 'M[option (ftype the_type)]_(fst mn, snd mn)}).
forward_call (X, offset_val densemat_data_offset p, sh); clear X.
entailer!.
Qed.

densemat_get verification


Lemma body_densematn_get: semax_body Vprog Gprog f_densematn_get densematn_get_spec.

Lemma body_densemat_get: semax_body Vprog Gprog f_densemat_get densemat_get_spec.

densemat_set verification


Lemma body_densematn_set: semax_body Vprog Gprog f_densematn_set densematn_set_spec.

Lemma body_densemat_set: semax_body Vprog Gprog f_densemat_set densemat_set_spec.

densemat_addto verification


Lemma body_densematn_addto: semax_body Vprog Gprog f_densematn_addto densematn_addto_spec.

Lemma body_densemat_addto: semax_body Vprog Gprog f_densemat_addto densemat_addto_spec.

data_norm and densemat_norm verification


Lemma body_data_norm2: semax_body Vprog Gprog f_data_norm2 data_norm2_spec.

Lemma body_data_norm: semax_body Vprog Gprog f_data_norm data_norm_spec.

Lemma body_densemat_norm2: semax_body Vprog Gprog f_densemat_norm2 densemat_norm2_spec.

Lemma body_densemat_norm: semax_body Vprog Gprog f_densemat_norm densemat_norm_spec.