LAProof.C.verif_densemat_cholesky: VST proofs of Cholesky 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.accuracy_proofs Require Import solve_model.
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_cfactor verification: Cholesky factorization


Definition cholesky_return' [n] (j: 'I_(S n)) (R: 'M[ftype the_type]_n) : ftype the_type :=
   seq.foldl BMULT (Zconst the_type 1) (map (fun k ⇒ fst (BFREXP (R k k))) (seq.take j (ord_enum n))).

Lemma cholesky_return'_e: ∀ n (R: 'M_n) (n': 'I_(S n)),
     n = nat_of_ord n' → cholesky_return' n' R = cholesky_return R.

Lemma body_densematn_cfactor: semax_body Vprog Gprog f_densematn_cfactor densematn_cfactor_spec.

Lemma body_densemat_cfactor: semax_body Vprog Gprog f_densemat_cfactor densemat_cfactor_spec.

densemat_csolve verification: Cholesky solve by forward substitution and back substitution


Lemma body_densematn_csolve: semax_body Vprog Gprog f_densematn_csolve densematn_csolve_spec.

Lemma body_densemat_csolve: semax_body Vprog Gprog f_densemat_csolve densemat_csolve_spec.

Lemma body_densematn_cfactor_and_solve: semax_body Vprog Gprog
        f_densematn_cfactor_and_solve densematn_cfactor_and_solve_spec.