CFEM.verif_densemat: VST proofs of functions on dense matrices.

Corresponds to C program densemat.c

Prologue.

For explanation see the prologue of CFEM.spec_densemat
From VST.floyd Require Import proofauto VSU.
From CFEM 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.

Unset Implicit Arguments.

Open Scope logic.

VSU definitions

VSU, "Verified Software Units" is VST's system for modular proofs about modular programs. Here, we want to import a subset of the malloc/free interface (MallocASI), a subset of our own custom wrapper for malloc (AllocASI), and a subset of VSTlib's math library describing functions from C's standard math.h (MathASI). Finally, we construct Gprog which lists all the funspecs of the functions that might be called from a function in the densemat module.
Definition densemat_E : funspecs := [].
Definition densemat_imported_specs : funspecs :=
   [free_spec']
  ++ [surely_malloc_spec'; double_clear_spec]
  ++ [fma_spec; sqrt_spec]. Definition densemat_internal_specs : funspecs := densematASI.
Definition Gprog := densemat_imported_specs ++ densemat_internal_specs.

These change_composite_env definitions are a kind of standard boilerplate; this mechanism ought to be documented in the VST reference manual, but it isn't.
Instance change_composite_env_alloc :
  change_composite_env spec_alloc.CompSpecs CompSpecs.

Instance change_composite_env_alloc' :
  change_composite_env CompSpecs spec_alloc.CompSpecs.

Many useful supporting lemmas about column_major, ordinal, ord_enum, etc.

column_major : ∀ {T : Type} [rows cols : nat], 'M_(rows, cols) → list T is a function from a matrix to the list of all its elements in column-major order.

Lemma map_const_ord_enum: ∀ {T} n (x: T), map (fun _ ⇒ x) (ord_enum n) = repeat x n.

Lemma column_major_const:
 ∀ {t: type} m n (x: option (ftype t)),
  map val_of_optfloat (@column_major _ m n (const_mx x)) =
  Zrepeat (val_of_optfloat x) (Z.of_nat m × Z.of_nat n).

Lemma densemat_field_compat0:
 ∀ m n p,
  0 ≤ m → 0 ≤ n → m×n ≤ Int.max_unsigned →
  malloc_compatible
    (densemat_data_offset + sizeof (tarray tdouble (m × n))) p →
  field_compatible0 (tarray tdouble (m×n)) (SUB (n × m))
        (offset_val densemat_data_offset p).

Lemma Zlength_ord_enum: ∀ n, Zlength (ord_enum n) = Z.of_nat n.

Lemma nth_seq_nth: ∀ T al (d: T) i, nth i al d = seq.nth d al i.

Lemma Znth_ord_enum: ∀ n `{IHn: Inhabitant 'I_n} (i: 'I_n),
  Znth i (ord_enum n) = i.

Lemma Znth_column_major:
  ∀ {T} {INH: Inhabitant T} m n i j (M: 'M[T]_(m,n)),
  Znth (Z.of_nat (nat_of_ord i+nat_of_ord j × m))%nat (column_major M) = M i j.

Lemma Zlength_column_major: ∀ {T} m n (M: 'M[T]_(m,n)),
  Zlength (column_major M) = (Z.of_nat m×Z.of_nat n)%Z.

Lemma firstn_seq: ∀ k i m, (i≤m)%nat → firstn i (seq k m) = seq k i.

Lemma in_sublist_ord_enum: ∀ n (a: 'I_n) (lo hi: Z),
  0 ≤ lo ≤ hi → hi ≤ Z.of_nat n →
  In a (sublist lo hi (ord_enum n)) → (lo ≤ Z.of_nat a < hi)%Z.

Lemma upd_Znth_column_major: ∀ {T} [m n] (M:'M[T]_(m,n)) (i: 'I_m) (j: 'I_n) (x:T),
   upd_Znth (Z.of_nat (i + j × m)) (column_major M) x = column_major (update_mx M i j x).

Lemma val_of_optfloat_column_major:
  ∀ t m n (M: 'M[ftype t]_(m,n)),
  map val_of_optfloat (column_major (map_mx Some M))
  = map val_of_float (column_major M).

Lemma fold_left_preserves: ∀ [A C: Type] (g: A → C) [B: Type] (f: A → B → A) (bl: list B),
  (∀ x y, g (f x y) = g x) →
  (∀ x, g (fold_left f bl x) = g x).

Lemma take_sublist: ∀ {T} (al: list T) i,
  seq.take i al = sublist 0 (Z.of_nat i) al.

Lemma drop_sublist: ∀ {T} (al: list T) i,
   seq.drop i al = sublist (Z.of_nat i) (Zlength al) al.

Lemma seq_rev_rev: @seq.rev = @rev.

Tactics for ordinals

Given a variable i of type Z, replace it everywhere with a variable i of type 'I_n, appropriately coerced.
Ltac ordify n i :=
  let Hi := fresh "H" i in
  let Hj := fresh "H" i in
  let j := fresh "i" in
  assert (Hi: Datatypes.is_true (ssrnat.leq (S (Z.to_nat i)) n)) by lia;
  set (j := @Ordinal n (Z.to_nat i) Hi);
  assert (Hj : i = Z.of_nat (nat_of_ord j)) by (simpl; lia);
  clearbody j; clear Hi;
  subst i;
  rename j into i.

Given a variable (j: 'I_1), substitute ord0 everywhere
Ltac ord1_eliminate j :=
  let H := fresh in assert (H:= ord1 j); simpl in H; subst j.

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

Ltac destruct_it B :=
 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
     | @sigT _ (fun x ⇒ _) ⇒ destruct A as [x A]
     end
 end.

Ltac destruct_PRE_POST_lets :=
repeat lazymatch goal with
| |- semax _ (sepcon (close_precondition _ ?B) _) _ _ ⇒ destruct_it B
| |- semax _ _ _ (frame_ret_assert (function_body_ret_assert _ ?B) _) ⇒ destruct_it B
end;
repeat change (fst (?A,?B)) with A in *;
repeat change (snd (?A,?B)) with B in ×.

Ltac start_function ::= start_function1; destruct_PRE_POST_lets; start_function2; start_function3.

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.

Tactics for calling matrix subscripting functions

When doing forward_call to the function densematn_get and densematn_set, one must first build a dependently typed package as illustrated above in body_densemat_clear. The tactics in this section help automate that, so one can do
  • forward_densematn_get instead of forward_call when calling densemat_get
  • forward_densematn_set instead of forward_call when calling densemat_set


Parameters:
  • M: 'M[option (ftype the_type)]_(m,n), the matrix value to be subscripted
  • i: 'I_m j: 'I_n, the indices at which to subscript
  • p: val, the address in memory where the matrix is represented column-major
  • sh: share, the permission-share of the representation in memory
  • x: ftype the_type, the expected result of subscripting the matrix, or the value to store into the matrix

Ltac forward_densematn_get M i j p sh x:=
   typecheck_forward_densemat forward_densematn_get M i j p sh x;
   let X := fresh "X" in
   pose (X := existT _ (_,_) (M,(i, j))
          : {mn : nat × nat & 'M[option (ftype the_type)]_(fst mn, snd mn) × ('I_(fst mn) × 'I_(snd mn))}%type);
    forward_call (X, p, sh, x); clear X.

Ltac forward_densematn_set M i j p sh x:=
   typecheck_forward_densemat forward_densematn_set M i j p sh x;
   let X := fresh "X" in
   pose (X := existT _ (_,_) (M,(i, j))
          : {mn : nat × nat & 'M[option (ftype the_type)]_(fst mn, snd mn) × ('I_(fst mn) × 'I_(snd mn))}%type);
    forward_call (X, p, sh, x); clear X.

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.

densemat_cfactor verification: Cholesky factorization


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.

Packaging the densematVSU, the Verified Software Unit


Ltac new_simpl_fst_snd :=
  match goal with |- context[@fst ident funspec ?A] ⇒
     let j := eval hnf in A in
     match j with (?x,?y) ⇒
      try change (fst A) with x;
      try change (snd A) with y
     end
    end.

Ltac SF_vacuous ::=
 try new_simpl_fst_snd;
 match goal with |- SF _ _ _ (vacuous_funspec _) ⇒ idtac end;
 match goal with H: @eq compspecs _ _ |- _ ⇒ rewrite <- H end;
red; red; repeat simple apply conj;
[ reflexivity
| repeat apply Forall_cons;
  try apply Forall_nil; reflexivity
| repeat constructor; simpl; rep_lia
| reflexivity
| split3; [reflexivity | reflexivity | intros; apply semax_vacuous]
| eexists; split; compute; reflexivity
].

Definition densematVSU: @VSU NullExtension.Espec
         densemat_E densemat_imported_specs
         ltac:(QPprog prog) densematASI (fun _ ⇒ TT).