LAProof.C.verif_build_csr
Require Import VST.floyd.proofauto.
Require Import LAProof.C.floatlib.
From LAProof.C Require Import build_csr sparse_model spec_sparse distinct partial_csr.
Require Import VSTlib.spec_math.
Require Import vcfloat.FPStdCompCert.
Require Import vcfloat.FPStdLib.
Require Import Coq.Classes.RelationClasses.
Open Scope logic.
Lemma body_coo_count: semax_body Vprog Gprog f_coo_count coo_count_spec.
Lemma fold_coo_rep:
∀ sh (coo: coo_matrix Tdouble) p (maxn: Z) (rp cp vp : val),
!! (0 ≤ Zlength (coo_entries coo) ≤ maxn ∧ maxn ≤ Int.max_signed
∧ 0 ≤ coo_rows coo < Int.max_signed
∧ 0 ≤ coo_cols coo < Int.max_signed ∧ coo_matrix_wellformed coo) &&
data_at sh t_coo (rp, (cp, (vp, (Vint (Int.repr (Zlength (coo_entries coo))), (Vint (Int.repr maxn),
(Vint (Int.repr (coo_rows coo)),
(Vint (Int.repr (coo_cols coo))))))))) p ×
data_at sh (tarray tuint maxn)
(map (fun e ⇒ Vint (Int.repr (fst (fst e)))) (coo_entries coo)
++ Zrepeat Vundef (maxn-(Zlength (coo_entries coo)))) rp ×
data_at sh (tarray tuint maxn)
(map (fun e ⇒ Vint (Int.repr (snd (fst e)))) (coo_entries coo)
++ Zrepeat Vundef (maxn-(Zlength (coo_entries coo)))) cp ×
data_at sh (tarray tdouble maxn)
(map (fun e ⇒ Vfloat (snd e)) (coo_entries coo)
++ Zrepeat Vundef (maxn-(Zlength (coo_entries coo)))) vp
|-- coo_rep sh coo p.
Lemma fold_csr_rep': ∀ sh (csr: csr_matrix Tdouble) (v: val) (ci: val) (rp: val) (p: val),
data_at sh t_csr (v,(ci,(rp,(Vint (Int.repr (csr_rows csr)), Vint (Int.repr (csr_cols csr)))))) p ×
data_at sh (tarray tdouble (Zlength (csr_col_ind csr))) (map Vfloat (csr_vals csr)) v ×
data_at sh (tarray tuint (Zlength (csr_col_ind csr))) (map Vint (map Int.repr (csr_col_ind csr))) ci ×
data_at sh (tarray tuint (csr_rows csr + 1)) (map Vint (map Int.repr (csr_row_ptr csr))) rp
|-- csr_rep' sh csr v ci rp p.
Lemma body_coo_to_csr_matrix: semax_body Vprog Gprog f_coo_to_csr_matrix coo_to_csr_matrix_spec.
Ltac entailer_for_return ::= idtac.
Require Import LAProof.C.floatlib.
From LAProof.C Require Import build_csr sparse_model spec_sparse distinct partial_csr.
Require Import VSTlib.spec_math.
Require Import vcfloat.FPStdCompCert.
Require Import vcfloat.FPStdLib.
Require Import Coq.Classes.RelationClasses.
Open Scope logic.
Lemma body_coo_count: semax_body Vprog Gprog f_coo_count coo_count_spec.
Lemma fold_coo_rep:
∀ sh (coo: coo_matrix Tdouble) p (maxn: Z) (rp cp vp : val),
!! (0 ≤ Zlength (coo_entries coo) ≤ maxn ∧ maxn ≤ Int.max_signed
∧ 0 ≤ coo_rows coo < Int.max_signed
∧ 0 ≤ coo_cols coo < Int.max_signed ∧ coo_matrix_wellformed coo) &&
data_at sh t_coo (rp, (cp, (vp, (Vint (Int.repr (Zlength (coo_entries coo))), (Vint (Int.repr maxn),
(Vint (Int.repr (coo_rows coo)),
(Vint (Int.repr (coo_cols coo))))))))) p ×
data_at sh (tarray tuint maxn)
(map (fun e ⇒ Vint (Int.repr (fst (fst e)))) (coo_entries coo)
++ Zrepeat Vundef (maxn-(Zlength (coo_entries coo)))) rp ×
data_at sh (tarray tuint maxn)
(map (fun e ⇒ Vint (Int.repr (snd (fst e)))) (coo_entries coo)
++ Zrepeat Vundef (maxn-(Zlength (coo_entries coo)))) cp ×
data_at sh (tarray tdouble maxn)
(map (fun e ⇒ Vfloat (snd e)) (coo_entries coo)
++ Zrepeat Vundef (maxn-(Zlength (coo_entries coo)))) vp
|-- coo_rep sh coo p.
Lemma fold_csr_rep': ∀ sh (csr: csr_matrix Tdouble) (v: val) (ci: val) (rp: val) (p: val),
data_at sh t_csr (v,(ci,(rp,(Vint (Int.repr (csr_rows csr)), Vint (Int.repr (csr_cols csr)))))) p ×
data_at sh (tarray tdouble (Zlength (csr_col_ind csr))) (map Vfloat (csr_vals csr)) v ×
data_at sh (tarray tuint (Zlength (csr_col_ind csr))) (map Vint (map Int.repr (csr_col_ind csr))) ci ×
data_at sh (tarray tuint (csr_rows csr + 1)) (map Vint (map Int.repr (csr_row_ptr csr))) rp
|-- csr_rep' sh csr v ci rp p.
Lemma body_coo_to_csr_matrix: semax_body Vprog Gprog f_coo_to_csr_matrix coo_to_csr_matrix_spec.
Ltac entailer_for_return ::= idtac.