CFEM.C.spec_matrix
Require Import VST.floyd.proofauto.
From CFEM.C Require Import matrix.
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.
Require LAProof.accuracy_proofs.export.
Module F := LAProof.accuracy_proofs.mv_mathcomp.F.
From CFEM.C Require Import matrix.
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.
Require LAProof.accuracy_proofs.export.
Module F := LAProof.accuracy_proofs.mv_mathcomp.F.
Now we undo all the settings that mathcomp has modified
Unset Implicit Arguments.
#[export] Instance CompSpecs : compspecs.
Definition Vprog : varspecs.
Require Import CFEM.C.nonexpansive.
Open Scope logic.
Notation the_type := spec_densemat.the_type.
Notation the_ctype := spec_densemat.the_ctype.
Notation val_of_float := spec_densemat.val_of_float.
Notation frobenius_norm2 := spec_densemat.frobenius_norm2.
Coercion Z.of_nat : nat >-> Z.
Definition matrix_rep (t: type): Type := ∀ (sh: share) (X: { mn & 'M[option (ftype t)]_(fst mn, snd mn)}) (p: val), mpred.
Definition matrix_data_t := Tstruct _matrix_data_t noattr.
Definition matrix_t := Tstruct _matrix_t noattr.
Definition matrix_add_spec' (instance: matrix_rep the_type) :=
WITH p: val, sh: share, X: {mn: nat×nat & 'M[option (ftype the_type)]_(fst mn, snd mn) × ('I_(fst mn) × 'I_(snd mn))}%type,
y: ftype the_type, x: ftype the_type
PRE[ tptr matrix_data_t, tint, tint, the_ctype ] let '(existT _ (m,n) (A,(i,j))) := X in
PROP(writable_share sh; A i j = Some y)
PARAMS( p; Vint (Int.repr i); Vint (Int.repr j); Vfloat x)
SEP(instance sh (existT _ (m,n) A) p)
POST [ tvoid ] let '(existT _ (m,n) (A,(i,j))) := X in
PROP()
RETURN()
SEP(instance sh (existT _ (m,n) (update_mx A i j (Some (BPLUS y x)))) p).
Definition matrix_clear_spec' (instance: matrix_rep the_type) :=
WITH p: val, sh: share, X: {mn: nat×nat & 'M[option (ftype the_type)]_(fst mn, snd mn)}%type
PRE[ tptr matrix_data_t ] let '(existT _ (m,n) A) := X in
PROP(writable_share sh)
PARAMS( p )
SEP(instance sh (existT _ (m,n) A) p)
POST [ tvoid ] let '(existT _ (m,n) A) := X in
PROP()
RETURN()
SEP(instance sh (existT _ (m,n) (@const_mx _ m n (Some (Zconst the_type 0)))) p).
Definition matrix_norm2_spec' (instance: matrix_rep the_type) :=
WITH p: val, sh: share, X: {mn: nat×nat & 'M[ftype the_type]_(fst mn, snd mn)}%type
PRE[ tptr matrix_data_t ] let '(existT _ (m,n) A) := X in
PROP(readable_share sh)
PARAMS( p )
SEP(instance sh (existT _ (m,n) (map_mx Some A)) p)
POST [ the_ctype ] let '(existT _ (m,n) A) := X in
PROP()
RETURN(val_of_float (frobenius_norm2 A))
SEP(instance sh (existT _ (m,n) (map_mx Some A)) p).
Definition matrix_print_spec' (instance: matrix_rep the_type) :=
WITH p: val, sh: share, X: {mn: nat×nat & 'M[ftype the_type]_(fst mn, snd mn)}%type
PRE[ tptr matrix_data_t ] let '(existT _ (m,n) A) := X in
PROP(readable_share sh)
PARAMS( p )
SEP(instance sh (existT _ (m,n) (map_mx Some A)) p)
POST [ tvoid ] let '(existT _ (m,n) A) := X in
PROP()
RETURN()
SEP(instance sh (existT _ (m,n) (map_mx Some A)) p).
Definition matrix_obj (sho sh: share) (instance: matrix_rep the_type)
(m n: nat) (A: 'M[option (ftype the_type)]_(m,n)) (obj: val) :=
EX p: val, EX add: val, EX clear: val, EX norm2: val, EX print: val,
!! (readable_share sho ∧ isptr p) &&
func_ptr' (matrix_add_spec' instance) add ×
func_ptr' (matrix_clear_spec' instance) clear ×
func_ptr' (matrix_norm2_spec' instance) norm2 ×
func_ptr' (matrix_print_spec' instance) print ×
data_at sho matrix_t (p,(add,(clear,(norm2,print)))) obj × instance sh (existT _ (m,n) A) p.
Lemma matrix_obj_local_facts: ∀ sho sh instance m n A obj,
matrix_obj sho sh instance m n A obj |-- !!(isptr obj).
#[export] Hint Resolve matrix_obj_local_facts : saturate_local.
Lemma matrix_obj_valid_pointer: ∀ sho sh instance m n A obj,
sepalg.nonidentity sho →
matrix_obj sho sh instance m n A obj |-- valid_pointer obj.
#[export] Hint Resolve matrix_obj_valid_pointer : valid_pointer.
Definition matrix_package : Type :=
{mn: nat×nat & matrix (option (ftype the_type)) (fst mn) (snd mn)}%type.
Definition matrix_and_indices : Type :=
{mn: nat×nat & matrix (option (ftype the_type)) (fst mn) (snd mn) × ('I_(fst mn) × 'I_(snd mn))}%type.
Import rmaps.
Definition matrix_package_typetree : TypeTree :=
SigType (nat×nat) (fun mn ⇒ ConstType ('M[option (ftype the_type)]_(fst mn, snd mn))).
Definition test_typetree (tree: TypeTree) (type: Type) :=
∀ t, (functors.MixVariantFunctor._functor (rmaps.dependent_type_functor_rec nil (AssertTT tree)) t) = (type → environ → t).
Goal test_typetree matrix_package_typetree matrix_package.
Definition matrix_and_indices_typetree: TypeTree :=
SigType (nat×nat) (fun mn ⇒ ConstType ('M[option (ftype the_type)]_(fst mn, snd mn) × ('I_(fst mn) × 'I_(snd mn)))).
Goal test_typetree matrix_and_indices_typetree matrix_and_indices.
Definition matrix_rep_type : TypeTree :=
ProdType (ConstType share)
(ArrowType (ConstType {mn : nat × nat & 'M[option (ftype the_type)]_(fst mn, snd mn)}) (ArrowType (ConstType val) Mpred)).
Lemma matrix_obj_nonexpansive : ∀ n' sho sh inst m n A obj,
compcert_rmaps.RML.R.approx n' (matrix_obj sho sh inst m n A obj) =
compcert_rmaps.RML.R.approx n'
(matrix_obj sho sh
(fun (a : share) (a0 : matrix_package) (a1 : val) ⇒ compcert_rmaps.R.approx n' (inst a a0 a1)) m n A obj).
Hint Resolve matrix_obj_nonexpansive : nonexpansive.
Definition matrix_add_type :=
ProdType (ConstType (val × share × share × matrix_and_indices × ftype the_type × ftype the_type))
(ArrowType (ConstType share) (ArrowType (ConstType matrix_package) (ArrowType (ConstType val) Mpred))).
Program Definition matrix_add_spec :=
DECLARE _matrix_add
TYPE matrix_add_type
WITH obj: val, sho: share, sh: share,
X: matrix_and_indices,
y: ftype the_type, x: ftype the_type,
inst: matrix_rep the_type
PRE[ tptr matrix_t, tint, tint, the_ctype ] let '(existT _ (m,n) (A,(i,j))) := X in
PROP(writable_share sh; A i j = Some y)
PARAMS( obj; Vint (Int.repr i); Vint (Int.repr j); Vfloat x) GLOBALS()
SEP (matrix_obj sho sh inst m n A obj)
POST [ tvoid ] let '(existT _ (m,n) (A,(i,j))) := X in
PROP()
RETURN()
SEP (matrix_obj sho sh inst m n (update_mx A i j (Some (BPLUS y x))) obj).
Definition matrix_clear_type :=
ProdType (ConstType (val × share × share × matrix_package))
(ArrowType (ConstType share) (ArrowType (ConstType matrix_package) (ArrowType (ConstType val) Mpred))).
Program Definition matrix_clear_spec :=
DECLARE _matrix_clear
TYPE matrix_clear_type
WITH obj: val, sho: share, sh: share,
X: matrix_package,
inst: matrix_rep the_type
PRE[ tptr matrix_t ] let '(existT _ (m,n) A) := X in
PROP(writable_share sh)
PARAMS( obj ) GLOBALS()
SEP (matrix_obj sho sh inst m n A obj)
POST [ tvoid ] let '(existT _ (m,n) A) := X in
PROP()
RETURN()
SEP (matrix_obj sho sh inst m n (@const_mx _ m n (Some (Zconst the_type 0))) obj).
Definition matrix_norm2_type :=
ProdType (ConstType (val × share × share × {mn: nat×nat & matrix (ftype the_type) (fst mn) (snd mn)}))
(ArrowType (ConstType share) (ArrowType (ConstType matrix_package) (ArrowType (ConstType val) Mpred))).
Program Definition matrix_norm2_spec :=
DECLARE _matrix_norm2
TYPE matrix_norm2_type
WITH obj: val, sho: share, sh: share,
X: {mn: nat×nat & matrix (ftype the_type) (fst mn) (snd mn)}%type,
inst: matrix_rep the_type
PRE[ tptr matrix_t ] let '(existT _ (m,n) A) := X in
PROP(writable_share sh)
PARAMS( obj ) GLOBALS()
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj)
POST [ the_ctype ] let '(existT _ (m,n) A) := X in
PROP()
RETURN(val_of_float (frobenius_norm2 A))
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj).
Program Definition matrix_norm_spec :=
DECLARE _matrix_norm
TYPE matrix_norm2_type
WITH obj: val, sho: share, sh: share,
X: {mn: nat×nat & matrix (ftype the_type) (fst mn) (snd mn)}%type,
inst: matrix_rep the_type
PRE[ tptr matrix_t ] let '(existT _ (m,n) A) := X in
PROP(writable_share sh)
PARAMS( obj ) GLOBALS()
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj)
POST [ the_ctype ] let '(existT _ (m,n) A) := X in
PROP()
RETURN(val_of_float (BSQRT (frobenius_norm2 A)))
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj).
Definition matrix_print_type :=
ProdType (ConstType (val × share × share × {mn: nat×nat & 'M[ftype the_type]_(fst mn, snd mn)}))
(ArrowType (ConstType share) (ArrowType (ConstType matrix_package) (ArrowType (ConstType val) Mpred))).
Program Definition matrix_print_spec :=
DECLARE _matrix_print
TYPE matrix_print_type
WITH obj: val, sho: share, sh: share,
X: {mn: nat×nat & 'M[ftype the_type]_(fst mn, snd mn)},
inst: matrix_rep the_type
PRE[ tptr matrix_t ] let '(existT _ (m,n) A) := X in
PROP(writable_share sh)
PARAMS( obj ) GLOBALS()
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj)
POST [ tvoid ] let '(existT _ (m,n) A) := X in
PROP()
RETURN()
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj).
Definition dense_matrix_rep : matrix_rep the_type :=
fun (sh: share) (X: { mn & 'M[option (ftype the_type)]_(fst mn, snd mn)}) (p: val) ⇒
spec_densemat.densemat sh (projT2 X) p.
Definition casted_densemat_add_spec :=
DECLARE _casted_densemat_add (matrix_add_spec' dense_matrix_rep).
Definition casted_densemat_clear_spec :=
DECLARE _casted_densemat_clear (matrix_clear_spec' dense_matrix_rep).
Definition casted_densemat_norm2_spec :=
DECLARE _casted_densemat_norm2 (matrix_norm2_spec' dense_matrix_rep).
Definition casted_densemat_print_spec :=
DECLARE _casted_densemat_print (matrix_print_spec' dense_matrix_rep).
Definition init_matrix_dense_spec :=
DECLARE _init_matrix_dense
WITH obj: val, sho: share, p: val, shp: share, X: { mn & 'M[option (ftype the_type)]_(fst mn, snd mn)}%type, gv: globals
PRE [ tptr matrix_t , tptr spec_densemat.densemat_t ]
PROP(writable_share sho)
PARAMS (obj; p) GLOBALS(gv)
SEP(data_at_ sho matrix_t obj; spec_densemat.densemat shp (projT2 X) p)
POST [ tvoid ]
PROP()
RETURN()
SEP(matrix_obj sho shp dense_matrix_rep _ _ (projT2 X) obj).
Definition casted_bandmat_add_spec : ident×funspec :=
(_casted_bandmat_add, vacuous_funspec (Internal f_casted_bandmat_add)).
Definition casted_bandmat_clear_spec : ident×funspec :=
(_casted_bandmat_clear, vacuous_funspec (Internal f_casted_bandmat_clear)).
Definition casted_bandmat_norm2_spec : ident×funspec :=
(_casted_bandmat_norm2, vacuous_funspec (Internal f_casted_bandmat_norm2)).
Definition casted_bandmat_print_spec : ident×funspec :=
(_casted_bandmat_print, vacuous_funspec (Internal f_casted_bandmat_print)).
Definition init_matrix_band_spec : ident×funspec :=
(_init_matrix_band, vacuous_funspec (Internal f_init_matrix_band)).
Definition matrix_ASI: funspecs :=
[ matrix_add_spec; casted_densemat_add_spec;
matrix_clear_spec; casted_densemat_clear_spec;
matrix_norm2_spec; casted_densemat_norm2_spec; matrix_norm_spec;
matrix_print_spec; casted_densemat_print_spec;
init_matrix_dense_spec;
casted_bandmat_add_spec; casted_bandmat_clear_spec;
casted_bandmat_norm2_spec; casted_bandmat_print_spec;
init_matrix_band_spec ].
#[export] Instance CompSpecs : compspecs.
Definition Vprog : varspecs.
Require Import CFEM.C.nonexpansive.
Open Scope logic.
Notation the_type := spec_densemat.the_type.
Notation the_ctype := spec_densemat.the_ctype.
Notation val_of_float := spec_densemat.val_of_float.
Notation frobenius_norm2 := spec_densemat.frobenius_norm2.
Coercion Z.of_nat : nat >-> Z.
Definition matrix_rep (t: type): Type := ∀ (sh: share) (X: { mn & 'M[option (ftype t)]_(fst mn, snd mn)}) (p: val), mpred.
Definition matrix_data_t := Tstruct _matrix_data_t noattr.
Definition matrix_t := Tstruct _matrix_t noattr.
Definition matrix_add_spec' (instance: matrix_rep the_type) :=
WITH p: val, sh: share, X: {mn: nat×nat & 'M[option (ftype the_type)]_(fst mn, snd mn) × ('I_(fst mn) × 'I_(snd mn))}%type,
y: ftype the_type, x: ftype the_type
PRE[ tptr matrix_data_t, tint, tint, the_ctype ] let '(existT _ (m,n) (A,(i,j))) := X in
PROP(writable_share sh; A i j = Some y)
PARAMS( p; Vint (Int.repr i); Vint (Int.repr j); Vfloat x)
SEP(instance sh (existT _ (m,n) A) p)
POST [ tvoid ] let '(existT _ (m,n) (A,(i,j))) := X in
PROP()
RETURN()
SEP(instance sh (existT _ (m,n) (update_mx A i j (Some (BPLUS y x)))) p).
Definition matrix_clear_spec' (instance: matrix_rep the_type) :=
WITH p: val, sh: share, X: {mn: nat×nat & 'M[option (ftype the_type)]_(fst mn, snd mn)}%type
PRE[ tptr matrix_data_t ] let '(existT _ (m,n) A) := X in
PROP(writable_share sh)
PARAMS( p )
SEP(instance sh (existT _ (m,n) A) p)
POST [ tvoid ] let '(existT _ (m,n) A) := X in
PROP()
RETURN()
SEP(instance sh (existT _ (m,n) (@const_mx _ m n (Some (Zconst the_type 0)))) p).
Definition matrix_norm2_spec' (instance: matrix_rep the_type) :=
WITH p: val, sh: share, X: {mn: nat×nat & 'M[ftype the_type]_(fst mn, snd mn)}%type
PRE[ tptr matrix_data_t ] let '(existT _ (m,n) A) := X in
PROP(readable_share sh)
PARAMS( p )
SEP(instance sh (existT _ (m,n) (map_mx Some A)) p)
POST [ the_ctype ] let '(existT _ (m,n) A) := X in
PROP()
RETURN(val_of_float (frobenius_norm2 A))
SEP(instance sh (existT _ (m,n) (map_mx Some A)) p).
Definition matrix_print_spec' (instance: matrix_rep the_type) :=
WITH p: val, sh: share, X: {mn: nat×nat & 'M[ftype the_type]_(fst mn, snd mn)}%type
PRE[ tptr matrix_data_t ] let '(existT _ (m,n) A) := X in
PROP(readable_share sh)
PARAMS( p )
SEP(instance sh (existT _ (m,n) (map_mx Some A)) p)
POST [ tvoid ] let '(existT _ (m,n) A) := X in
PROP()
RETURN()
SEP(instance sh (existT _ (m,n) (map_mx Some A)) p).
Definition matrix_obj (sho sh: share) (instance: matrix_rep the_type)
(m n: nat) (A: 'M[option (ftype the_type)]_(m,n)) (obj: val) :=
EX p: val, EX add: val, EX clear: val, EX norm2: val, EX print: val,
!! (readable_share sho ∧ isptr p) &&
func_ptr' (matrix_add_spec' instance) add ×
func_ptr' (matrix_clear_spec' instance) clear ×
func_ptr' (matrix_norm2_spec' instance) norm2 ×
func_ptr' (matrix_print_spec' instance) print ×
data_at sho matrix_t (p,(add,(clear,(norm2,print)))) obj × instance sh (existT _ (m,n) A) p.
Lemma matrix_obj_local_facts: ∀ sho sh instance m n A obj,
matrix_obj sho sh instance m n A obj |-- !!(isptr obj).
#[export] Hint Resolve matrix_obj_local_facts : saturate_local.
Lemma matrix_obj_valid_pointer: ∀ sho sh instance m n A obj,
sepalg.nonidentity sho →
matrix_obj sho sh instance m n A obj |-- valid_pointer obj.
#[export] Hint Resolve matrix_obj_valid_pointer : valid_pointer.
Definition matrix_package : Type :=
{mn: nat×nat & matrix (option (ftype the_type)) (fst mn) (snd mn)}%type.
Definition matrix_and_indices : Type :=
{mn: nat×nat & matrix (option (ftype the_type)) (fst mn) (snd mn) × ('I_(fst mn) × 'I_(snd mn))}%type.
Import rmaps.
Definition matrix_package_typetree : TypeTree :=
SigType (nat×nat) (fun mn ⇒ ConstType ('M[option (ftype the_type)]_(fst mn, snd mn))).
Definition test_typetree (tree: TypeTree) (type: Type) :=
∀ t, (functors.MixVariantFunctor._functor (rmaps.dependent_type_functor_rec nil (AssertTT tree)) t) = (type → environ → t).
Goal test_typetree matrix_package_typetree matrix_package.
Definition matrix_and_indices_typetree: TypeTree :=
SigType (nat×nat) (fun mn ⇒ ConstType ('M[option (ftype the_type)]_(fst mn, snd mn) × ('I_(fst mn) × 'I_(snd mn)))).
Goal test_typetree matrix_and_indices_typetree matrix_and_indices.
Definition matrix_rep_type : TypeTree :=
ProdType (ConstType share)
(ArrowType (ConstType {mn : nat × nat & 'M[option (ftype the_type)]_(fst mn, snd mn)}) (ArrowType (ConstType val) Mpred)).
Lemma matrix_obj_nonexpansive : ∀ n' sho sh inst m n A obj,
compcert_rmaps.RML.R.approx n' (matrix_obj sho sh inst m n A obj) =
compcert_rmaps.RML.R.approx n'
(matrix_obj sho sh
(fun (a : share) (a0 : matrix_package) (a1 : val) ⇒ compcert_rmaps.R.approx n' (inst a a0 a1)) m n A obj).
Hint Resolve matrix_obj_nonexpansive : nonexpansive.
Definition matrix_add_type :=
ProdType (ConstType (val × share × share × matrix_and_indices × ftype the_type × ftype the_type))
(ArrowType (ConstType share) (ArrowType (ConstType matrix_package) (ArrowType (ConstType val) Mpred))).
Program Definition matrix_add_spec :=
DECLARE _matrix_add
TYPE matrix_add_type
WITH obj: val, sho: share, sh: share,
X: matrix_and_indices,
y: ftype the_type, x: ftype the_type,
inst: matrix_rep the_type
PRE[ tptr matrix_t, tint, tint, the_ctype ] let '(existT _ (m,n) (A,(i,j))) := X in
PROP(writable_share sh; A i j = Some y)
PARAMS( obj; Vint (Int.repr i); Vint (Int.repr j); Vfloat x) GLOBALS()
SEP (matrix_obj sho sh inst m n A obj)
POST [ tvoid ] let '(existT _ (m,n) (A,(i,j))) := X in
PROP()
RETURN()
SEP (matrix_obj sho sh inst m n (update_mx A i j (Some (BPLUS y x))) obj).
Definition matrix_clear_type :=
ProdType (ConstType (val × share × share × matrix_package))
(ArrowType (ConstType share) (ArrowType (ConstType matrix_package) (ArrowType (ConstType val) Mpred))).
Program Definition matrix_clear_spec :=
DECLARE _matrix_clear
TYPE matrix_clear_type
WITH obj: val, sho: share, sh: share,
X: matrix_package,
inst: matrix_rep the_type
PRE[ tptr matrix_t ] let '(existT _ (m,n) A) := X in
PROP(writable_share sh)
PARAMS( obj ) GLOBALS()
SEP (matrix_obj sho sh inst m n A obj)
POST [ tvoid ] let '(existT _ (m,n) A) := X in
PROP()
RETURN()
SEP (matrix_obj sho sh inst m n (@const_mx _ m n (Some (Zconst the_type 0))) obj).
Definition matrix_norm2_type :=
ProdType (ConstType (val × share × share × {mn: nat×nat & matrix (ftype the_type) (fst mn) (snd mn)}))
(ArrowType (ConstType share) (ArrowType (ConstType matrix_package) (ArrowType (ConstType val) Mpred))).
Program Definition matrix_norm2_spec :=
DECLARE _matrix_norm2
TYPE matrix_norm2_type
WITH obj: val, sho: share, sh: share,
X: {mn: nat×nat & matrix (ftype the_type) (fst mn) (snd mn)}%type,
inst: matrix_rep the_type
PRE[ tptr matrix_t ] let '(existT _ (m,n) A) := X in
PROP(writable_share sh)
PARAMS( obj ) GLOBALS()
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj)
POST [ the_ctype ] let '(existT _ (m,n) A) := X in
PROP()
RETURN(val_of_float (frobenius_norm2 A))
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj).
Program Definition matrix_norm_spec :=
DECLARE _matrix_norm
TYPE matrix_norm2_type
WITH obj: val, sho: share, sh: share,
X: {mn: nat×nat & matrix (ftype the_type) (fst mn) (snd mn)}%type,
inst: matrix_rep the_type
PRE[ tptr matrix_t ] let '(existT _ (m,n) A) := X in
PROP(writable_share sh)
PARAMS( obj ) GLOBALS()
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj)
POST [ the_ctype ] let '(existT _ (m,n) A) := X in
PROP()
RETURN(val_of_float (BSQRT (frobenius_norm2 A)))
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj).
Definition matrix_print_type :=
ProdType (ConstType (val × share × share × {mn: nat×nat & 'M[ftype the_type]_(fst mn, snd mn)}))
(ArrowType (ConstType share) (ArrowType (ConstType matrix_package) (ArrowType (ConstType val) Mpred))).
Program Definition matrix_print_spec :=
DECLARE _matrix_print
TYPE matrix_print_type
WITH obj: val, sho: share, sh: share,
X: {mn: nat×nat & 'M[ftype the_type]_(fst mn, snd mn)},
inst: matrix_rep the_type
PRE[ tptr matrix_t ] let '(existT _ (m,n) A) := X in
PROP(writable_share sh)
PARAMS( obj ) GLOBALS()
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj)
POST [ tvoid ] let '(existT _ (m,n) A) := X in
PROP()
RETURN()
SEP (matrix_obj sho sh inst m n (map_mx Some A) obj).
Definition dense_matrix_rep : matrix_rep the_type :=
fun (sh: share) (X: { mn & 'M[option (ftype the_type)]_(fst mn, snd mn)}) (p: val) ⇒
spec_densemat.densemat sh (projT2 X) p.
Definition casted_densemat_add_spec :=
DECLARE _casted_densemat_add (matrix_add_spec' dense_matrix_rep).
Definition casted_densemat_clear_spec :=
DECLARE _casted_densemat_clear (matrix_clear_spec' dense_matrix_rep).
Definition casted_densemat_norm2_spec :=
DECLARE _casted_densemat_norm2 (matrix_norm2_spec' dense_matrix_rep).
Definition casted_densemat_print_spec :=
DECLARE _casted_densemat_print (matrix_print_spec' dense_matrix_rep).
Definition init_matrix_dense_spec :=
DECLARE _init_matrix_dense
WITH obj: val, sho: share, p: val, shp: share, X: { mn & 'M[option (ftype the_type)]_(fst mn, snd mn)}%type, gv: globals
PRE [ tptr matrix_t , tptr spec_densemat.densemat_t ]
PROP(writable_share sho)
PARAMS (obj; p) GLOBALS(gv)
SEP(data_at_ sho matrix_t obj; spec_densemat.densemat shp (projT2 X) p)
POST [ tvoid ]
PROP()
RETURN()
SEP(matrix_obj sho shp dense_matrix_rep _ _ (projT2 X) obj).
Definition casted_bandmat_add_spec : ident×funspec :=
(_casted_bandmat_add, vacuous_funspec (Internal f_casted_bandmat_add)).
Definition casted_bandmat_clear_spec : ident×funspec :=
(_casted_bandmat_clear, vacuous_funspec (Internal f_casted_bandmat_clear)).
Definition casted_bandmat_norm2_spec : ident×funspec :=
(_casted_bandmat_norm2, vacuous_funspec (Internal f_casted_bandmat_norm2)).
Definition casted_bandmat_print_spec : ident×funspec :=
(_casted_bandmat_print, vacuous_funspec (Internal f_casted_bandmat_print)).
Definition init_matrix_band_spec : ident×funspec :=
(_init_matrix_band, vacuous_funspec (Internal f_init_matrix_band)).
Definition matrix_ASI: funspecs :=
[ matrix_add_spec; casted_densemat_add_spec;
matrix_clear_spec; casted_densemat_clear_spec;
matrix_norm2_spec; casted_densemat_norm2_spec; matrix_norm_spec;
matrix_print_spec; casted_densemat_print_spec;
init_matrix_dense_spec;
casted_bandmat_add_spec; casted_bandmat_clear_spec;
casted_bandmat_norm2_spec; casted_bandmat_print_spec;
init_matrix_band_spec ].