LAProof.C.densemat_lemmas: Supporting lemmas for VST proofs of functions on dense matrices.


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.
From VSTlib Require Import spec_math spec_malloc.
From Stdlib Require Import 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']
  ++ [exit_spec; surely_malloc_spec'; double_clear_spec]
  ++ [fma_spec; sqrt_spec; frexp_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.

Instance change_composite_env_empty: change_composite_env emptyCS CompSpecs.

Instance change_composite_env_empty': change_composite_env CompSpecs emptyCS.

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.

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.

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.

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 to these tactics:
  • 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.

In the special case when a densemat or densematn is indexed by constant indexes (i,j) of type Z, the tactic forward_densematn_special can be used without any arguments, which automatically calculate all of the arguments to forward_densemat[|n]_[get|set].

Ltac forward_densematn_get_special_aux pvar p stride i j :=
    match goal with |- semax _ ?Pre _ _ ⇒ match Pre with context [densematn ?sh ?M p] ⇒
     match type of M with @matrix _ ?m ?n ⇒
      let i' := constr:(@Ordinal m (Z.to_nat i) (eq_refl _)) in
      let j' := constr:(@Ordinal n (Z.to_nat j) (eq_refl _)) in
        densemat_lemmas.forward_densematn_get M i' j' p sh (optfloat_to_float (M i' j'))
    end end end;
    [ try (unfold map_mx; rewrite !mxE; reflexivity) | ].

Ltac forward_densematn_special :=
 match goal with
 | |- context [Scall (Some _) (Evar ?f _)
                      [Etempvar ?pvar _; Econst_int (Int.repr ?stride) _;
                       Econst_int (Int.repr ?i) _; Econst_int (Int.repr ?j) _]] ⇒
     unify f _densematn_get;
     match goal with
     | |- context [temp pvar ?p] ⇒ forward_densematn_get_special_aux pvar p stride i j
     end
 | |- context [Scall (Some _) (Evar ?f _)
                      [Evar ?pvar _; Econst_int (Int.repr ?stride) _;
                       Econst_int (Int.repr ?i) _; Econst_int (Int.repr ?j) _]] ⇒
     unify f _densematn_get;
     match goal with
     | |- context [lvar pvar _ ?p] ⇒ forward_densematn_get_special_aux pvar p stride i j
     end
 | |- context [Scall None (Evar ?f _)
                     [Etempvar ?pvar _; Econst_int (Int.repr ?stride) _;
                      Econst_int (Int.repr ?i) _; Econst_int (Int.repr ?j) _; _]] ⇒
    unify f _densematn_set;
    match goal with |- context [temp pvar ?p] ⇒
    match goal with |- semax _ ?Pre _ _ ⇒ match Pre with context [densematn ?sh ?M p] ⇒
     match type of M with @matrix _ ?m ?n ⇒
     let y := fresh "y" in
      evar (y: ftype Tdouble);
        densemat_lemmas.forward_densematn_set M
        (@Ordinal m (Z.to_nat i) (eq_refl _)) (@Ordinal n (Z.to_nat j) (eq_refl _)) p sh y; subst y
    end end end
   end; [entailer!! | ]
end.

begin_densematn_in_frame is used when you already have an array of floats/doubles that you want to treat as a dense matrix. That is, you don't want to call densemat_alloc. Typical example is a stack-allocated (local-variable) array. There is a tactic begin_densemat_in_frame for automatically applying this lemma.
Lemma begin_densematn_in_frame:
  ∀ compspecs sh ij i j p,
   ij = Z.mul (Z.of_nat i) (Z.of_nat j) →
   0 < Z.of_nat i ≤ Int.max_signed →
    0 < Z.of_nat j ≤ Int.max_signed →
    Z.of_nat i × Z.of_nat j ≤ Int.max_signed →
   @data_at_ compspecs sh (tarray tdouble ij) p |--
   densematn sh (@const_mx (option (ftype Tdouble)) i j None) p.

end_densematn_in_frame is used at the end of a scope, where you want to turn the dense matrix (created by begin_densemat_in_frame) back into an array, so it can be deallocated.
Lemma end_densematn_in_frame:
  ∀ compspecs sh i j M p,
   @densematn Tdouble sh i j M p |--
   @data_at_ compspecs sh (tarray tdouble (Z.mul (Z.of_nat i) (Z.of_nat j))) p.

begin_densematn_in_frame is used when you already have an array of floats/doubles that you want to treat as a dense matrix. That is, you don't want to call densemat_alloc. Typical example is a stack-allocated (local-variable) array. This tactic looks for an entailment with an uninitialized array of doubles at address p in the precondition, and a matching uninitialized dense matrix at address p in the postcondition, and automatically applies the lemma.
Ltac begin_densematn_in_frame :=
lazymatch goal with |- ?A |-- ?B ⇒
 match A with context [@data_at_ ?compspecs ?sh (tarray tdouble ?n) ?p] ⇒
  match B with context [densematn sh (@const_mx _ ?i ?j None) p ] ⇒
    tryif unify (Z.of_nat (i×j)) n
    then sep_apply (begin_densematn_in_frame compspecs sh n i j p); try rep_lia
    else fail 2 "begin_densematn_in_frame requires n in [data_at _ (tarray tdouble n)" p "] to match product of matrix dimensions of [densematn _" p
                 "] but you have " n " and "i"*"j
end end end.

end_densemat_in_frame automatically converts a dense matrix back into an uninitialized array. (You would want to do this at the end of a block or the end of a function, so that when going forward through a return statement, VST-Floyd can pop the stack frame properly.) This tactic looks for an entailment with a densematn at address p in the precondition, and a matching uninitialized array at address p in the postcondition.
Ltac end_densematn_in_frame :=
lazymatch goal with |- ?A |-- ?B ⇒
 match B with context [@data_at_ ?compspecs ?sh (tarray tdouble ?n) ?p] ⇒
  match A with context [@densematn _ sh ?i ?j ?m p] ⇒
    tryif unify (Z.of_nat (i×j)) n
    then sep_apply (end_densematn_in_frame compspecs sh i j m p)
    else fail 2 "begin_densematn_in_frame requires n in [data_at _ (tarray tdouble n)" p "] to match product of matrix dimensions of [densematn _" p
                 "] but you have " n " and "i"*"j
end end end.