diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 459c90a..2799da1 100644 --- a/.github/workflows/coq.yml +++ b/.github/workflows/coq.yml @@ -13,7 +13,7 @@ jobs: fail-fast: false matrix: include: - - env: { COQ_VERSION: "9.0", DOCKER_MATHCOMP_VERSION: "2.4.0" } + - env: { COQ_VERSION: "9.0", DOCKER_MATHCOMP_VERSION: "2.5.0" } runs-on: ubuntu-latest env: ${{ matrix.env }} diff --git a/C/VSU_densemat.v b/C/VSU_densemat.v index 8c31bd4..6cfea11 100644 --- a/C/VSU_densemat.v +++ b/C/VSU_densemat.v @@ -25,31 +25,6 @@ Set Bullet Behavior "Strict Subproofs". Open Scope logic. -(* BEGIN workaround for VST issue #814, until we can install VST 2.16 which fixes it. *) -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 (* id_in_list ... *) -| repeat apply Forall_cons; (* Forall complete_type fn_vars *) - try apply Forall_nil; reflexivity -| repeat constructor; simpl; rep_lia (* var_sizes_ok *) -| reflexivity (* fn_callconv ... *) -| split3; [reflexivity | reflexivity | intros; apply semax_vacuous] (* semax_body *) -| eexists; split; compute; reflexivity (* genv_find_func *) -]. -(* END workaround for VST issue #814 *) - Definition densematVSU: @VSU NullExtension.Espec densemat_E densemat_imported_specs ltac:(QPprog prog) densematASI (fun _ => TT). diff --git a/C/densemat_lemmas.v b/C/densemat_lemmas.v index 95ee2f8..a91a57e 100644 --- a/C/densemat_lemmas.v +++ b/C/densemat_lemmas.v @@ -110,6 +110,198 @@ transitivity (concat (repeat (repeat x m) n)). unfold const_mx; rewrite mxE; auto. Qed. + +Lemma nth_seq_nth: forall T al (d: T) i, nth i al d = seq.nth d al i. +Proof. +induction al; destruct i; simpl; intros; auto. +Qed. + +Lemma app_column_major: forall {t} m n1 n2 (A: 'M[t]_(m,n1)) (B: 'M[t]_(m,n2)), + column_major (row_mx A B) = column_major A ++ column_major B. +Proof. +intros. +unfold column_major. +rewrite <- concat_app. +f_equal. +replace (ord_enum (ssrnat.addn n1 n2)) + with (map (lshift n2) (ord_enum n1) ++ map (@rshift n1 n2) (ord_enum n2)). +- +rewrite map_app. +f_equal. ++ +rewrite map_map. +f_equal. +extensionality i. +f_equal. +extensionality j. +unfold row_mx. rewrite mxE. +unfold split. +destruct (ssrnat.ltnP _ _). f_equal. apply ord_inj; auto. +simpl in i0. +destruct i. simpl in *. lia. ++ +rewrite map_map. +f_equal. +extensionality i. +f_equal. +extensionality j. +unfold row_mx; rewrite mxE. +unfold split. +destruct (ssrnat.ltnP _ _); destruct i; simpl in *; try lia. +f_equal. +apply ord_inj; simpl. lia. +- +destruct n1. +simpl. change (ssrnat.addn 0 n2) with n2. +transitivity (map id (ord_enum n2)). +f_equal. extensionality x. apply ord_inj. simpl. reflexivity. apply map_id_eq. +change (ssrnat.addn (S n1) n2) with (S (ssrnat.addn n1 n2)). +apply (nth_ext _ _ ord0 ord0). +rewrite length_app, !length_map, !length_ord_enum. lia. +intros i Hi. +rewrite length_app, !length_map, !length_ord_enum in Hi. +destruct (lt_dec i (S n1)). ++ +rewrite app_nth1 by (rewrite length_map, length_ord_enum; auto). +rewrite nth_map_inrange with (d:=ord0) (d':=ord0) + by (rewrite length_ord_enum; lia). +symmetry; rewrite nth_seq_nth. +replace i with (nat_of_ord (@inord (ssrnat.addn n1 n2) i)) at 1 + by (rewrite inordK; lia). +rewrite !nth_ord_enum'. +rewrite densemat_lemmas.nth_seq_nth. +replace i with (nat_of_ord (@inord n1 i)) at 2 + by (rewrite inordK; lia). +rewrite nth_ord_enum'. +apply ord_inj; simpl. +rewrite !inordK by lia. +auto. ++ +destruct n2. +lia. +rewrite app_nth2 by (rewrite length_map, length_ord_enum; lia). +rewrite length_map, length_ord_enum. +rewrite nth_map_inrange with (d' := ord0) + by (rewrite length_ord_enum; lia). +rewrite !densemat_lemmas.nth_seq_nth. +replace (i - S n1)%nat with (nat_of_ord (@inord n2 (i - S n1))) + by (rewrite inordK; lia). +rewrite nth_ord_enum'. +replace i with (nat_of_ord (@inord (ssrnat.addn n1 (S n2)) i)) at 2 + by (rewrite inordK; lia). +rewrite nth_ord_enum'. +apply ord_inj. simpl. rewrite !inordK by lia. lia. +Qed. + + +Lemma Zlength_column_major: forall {T} m n (M: 'M[T]_(m,n)), + Zlength (column_major M) = (Z.of_nat m*Z.of_nat n)%Z. +Proof. +intros. +unfold column_major. +rewrite (@Zlength_concat' _ (Z.of_nat n) (Z.of_nat m)). +lia. +rewrite Zlength_map, Zlength_correct, length_ord_enum; auto. +apply Forall_map. +apply Forall_forall; intros. +simpl. +rewrite Zlength_map, Zlength_correct, length_ord_enum; auto. +Qed. + +Lemma sublist_column_major_left: + forall m n1 n2 (A: 'M[option (ftype the_type)]_(m,n1)) (B: 'M[option (ftype the_type)]_(m,n2)), + sublist 0 (Z.of_nat m * Z.of_nat n1) (column_major (row_mx A B)) = column_major A. +Proof. +intros. +rewrite app_column_major. +rewrite sublist_app1; [apply sublist_same | .. ]; +rewrite ?Zlength_column_major; lia. +Qed. + +Lemma sublist_column_major_right: + forall m n1 n2 (A: 'M[option (ftype the_type)]_(m,n1)) (B: 'M[option (ftype the_type)]_(m,n2)), + 0 < n1 -> 0 < n2 -> + sublist (Z.of_nat m * Z.of_nat n1) (Z.of_nat m * Z.of_nat (n1+n2)) (column_major (row_mx A B)) = column_major B. +Proof. +intros. +rewrite app_column_major. +rewrite sublist_app2; [apply sublist_same |]; +rewrite !Zlength_column_major; lia. +Qed. + +Lemma split_matrix_cols1: + forall sh m n1 n2 (A: 'M[option (ftype the_type)]_(m,n1)) (B: 'M[option (ftype the_type)]_(m,n2)) p, + 0 < n1 -> 0 < n2 -> + densematn sh (row_mx A B) p |-- + densematn sh A p * densematn sh B (field_address (tarray the_ctype (m*(n1+n2))) (SUB (m*n1)) p). +Proof. +intros. +unfold densematn. +change (ssrnat.addn n1 n2) with (n1+n2)%nat. +repeat change (reptype_ftype _ ?A) with A. +Intros. +entailer!. +rewrite <- (sublist_same 0 (Z.of_nat m * Z.of_nat (n1+n2)) (column_major (row_mx _ _))); + auto. +2: rewrite densemat_lemmas.Zlength_column_major; lia. +rewrite (sublist_split 0 (Z.of_nat m *Z.of_nat n1)) + by (rewrite ?densemat_lemmas.Zlength_column_major; lia). +rewrite map_app. +rewrite (split2_data_at_Tarray_app (Z.of_nat m * Z.of_nat n1)). +2,3: autorewrite with sublist; rewrite Zlength_sublist; + rewrite ?Zlength_column_major; list_solve. +rewrite sublist_column_major_left; auto. +rewrite sublist_column_major_right; auto. +cancel. +apply derives_refl'. +replace (Z.of_nat m * Z.of_nat (n1 + n2) - Z.of_nat m * Z.of_nat n1) + with (Z.of_nat m * Z.of_nat n2)%Z by lia. +f_equal. +rewrite field_address_offset by auto with field_compatible. +rewrite field_address0_offset by auto with field_compatible. +reflexivity. +Qed. + + +Lemma split_matrix_cols: + forall sh m n1 n2 (A: 'M[option (ftype the_type)]_(m,n1)) (B: 'M[option (ftype the_type)]_(m,n2)) p, + (0 < n1)%nat -> + (0 < n2)%nat -> + (0 < m)%nat -> + Z.of_nat (m * (n1+n2)) <= Int.max_signed -> + field_compatible (tarray the_ctype (Z.of_nat m * Z.of_nat (n1+n2))) [] p -> + densematn sh (row_mx A B) p = + densematn sh A p * densematn sh B (field_address (tarray the_ctype (m*(n1+n2))) (SUB (m*n1)) p). +Proof. +intros. +unfold densematn. +rewrite !prop_true_andp + by (try rep_lia; rewrite ssrnat.addnE; split3; try rep_lia; destruct m; try lia). +repeat change (reptype_ftype _ ?A) with A. +replace (column_major (row_mx A B)) with (column_major A ++ column_major B). +2:{ +rewrite <- (sublist_same 0 (Zlength (column_major (row_mx A B))) (column_major (row_mx A B))) by auto. +etransitivity ; [ | symmetry; apply sublist_split with (mid:=Zlength (column_major A))]. +2: rep_lia. 2: rewrite !densemat_lemmas.Zlength_column_major; lia. +rewrite !Zlength_column_major. +rewrite sublist_column_major_left by lia. +rewrite sublist_column_major_right by lia. +auto. +} +rewrite map_app, ssrnat.addnE, Nat2Z.inj_add, Z.mul_add_distr_l. +rewrite (split2_data_at_Tarray_app (m*n1)). +2: rewrite Zlength_map, Zlength_column_major; auto. +2: rewrite Zlength_map, Zlength_column_major; lia. +change (ctype_of_type the_type) with the_ctype. +set (mn1 := (Z.of_nat m * Z.of_nat n1)%Z). +set (mn2 := (Z.of_nat m * Z.of_nat n2)%Z). +replace (mn1+mn2-mn1) with mn2 by lia. +f_equal. +f_equal. +rewrite field_address0_offset, field_address_offset; auto with field_compatible. +Qed. + + Lemma densemat_field_compat0: forall m n p, 0 <= m -> 0 <= n -> m*n <= Int.max_unsigned -> @@ -154,11 +346,6 @@ intros. rewrite Zlength_correct, length_ord_enum; auto. Qed. -Lemma nth_seq_nth: forall T al (d: T) i, nth i al d = seq.nth d al i. -Proof. -induction al; destruct i; simpl; intros; auto. -Qed. - Lemma Znth_ord_enum: forall n `{IHn: Inhabitant 'I_n} (i: 'I_n), Znth i (ord_enum n) = i. Proof. @@ -224,21 +411,6 @@ rewrite !Znth_ord_enum. auto. Qed. -Lemma Zlength_column_major: forall {T} m n (M: 'M[T]_(m,n)), - Zlength (column_major M) = (Z.of_nat m*Z.of_nat n)%Z. -Proof. -intros. -unfold column_major. -rewrite (@Zlength_concat' _ (Z.of_nat n) (Z.of_nat m)). -lia. -rewrite Zlength_map, Zlength_correct, length_ord_enum; auto. -apply Forall_map. -apply Forall_forall; intros. -simpl. -rewrite Zlength_map, Zlength_correct, length_ord_enum; auto. -Qed. - - Lemma firstn_seq: forall k i m, (i<=m)%nat -> firstn i (seq k m) = seq k i. intros. revert k i H; induction m; simpl; intros. @@ -489,4 +661,148 @@ Ltac forward_densematn_set M i j p sh x:= : {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_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 + 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_get_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 +end. + +Ltac forward_densematn_set_special := + match goal with |- 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); + 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 +end; [entailer!! | ]. + +(** [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: + forall 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. +Proof. +intros. +unfold densematn. +entailer!!. +change (ctype_of_type _) with tdouble. +rewrite densemat_lemmas.column_major_const. +simpl. +rewrite data_at__eq. +apply derives_refl'. +set (ij := Z.mul (Z.of_nat _) (Z.of_nat _)). +unfold default_val. simpl. +unfold reptype_ftype; simpl. +unfold data_at. +unfold field_at, field_compatible. +f_equal. +f_equal. +f_equal. +f_equal. +f_equal. +f_equal. +unfold align_compatible. +destruct p; auto. +set (c1 := @cenv_cs _); clearbody c1. +set (c2 := @cenv_cs _); clearbody c2. +clearbody ij. +clear. +apply prop_ext. +split; intro H; inv H; try inv H0; constructor; intros; simpl; econstructor; try reflexivity; simpl; +apply H4 in H; inv H; inv H0; auto. +Qed. + + +(** [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: + forall 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. +Proof. +intros. +unfold densematn. +entailer!!. +change (ctype_of_type _) with tdouble. +rewrite data_at__eq. +unfold default_val. simpl. +unfold reptype_ftype; simpl. +apply derives_trans with (@data_at spec_densemat.CompSpecs sh (tarray tdouble (i * j)) (@Zrepeat val Vundef (i * j)) p +). +apply data_at_data_at_. +unfold data_at. +unfold field_at, field_compatible. +apply andp_derives. +apply prop_derives. intros [? [? [? [? ?]]]]. split3; auto. +split3; auto. +clear - H5. +hnf in H5|-*. destruct p; simpl in H5|-*; auto. +inv H5. inv H. constructor. intros. specialize (H3 _ H). simpl in H3. +inv H3. econstructor; try eassumption. +apply derives_refl. +Qed. + +(** [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. + It 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. diff --git a/C/verif_densemat_cholesky.v b/C/verif_densemat_cholesky.v index 764e1f1..f609ed5 100644 --- a/C/verif_densemat_cholesky.v +++ b/C/verif_densemat_cholesky.v @@ -323,7 +323,7 @@ forward_for_simple_bound (Z.of_nat n) (EX i:Z, set (al := seq.foldl _ _ _). subst bi. change (fstep i) with al. unfold forward_subst_step. - change ssralg.GRing.zero with (@ord0 O). + (* mathcomp 2.4: change ssralg.GRing.zero with (@ord0 O). *) change @seq.map with @map. rewrite take_sublist. set (uu := BDIV _ _). diff --git a/README.md b/README.md index 510c0d2..8c2664c 100644 --- a/README.md +++ b/README.md @@ -22,3 +22,13 @@ vector multiplication as an example of connecting LAProof to concrete programs. LAProof 2.0beta1 is based more directly on MathComp; that is, matrix and vector operations use definitions in mathcomp.algebra.matrix. ## DOCUMENTATION: click here + +## OPAM CONFIGURATION + +Developers of this software should probably confirm that their opam library installations are consistent with ./coq-laproof.opam +by running, + +opam switch create rocq9.0 4.14.2 # (the last argument is which version of ocaml) +opam install rocqide # optional, if you use rocqide +opam install --deps-only ./coq-laproof.opam + diff --git a/accuracy_proofs/gemv_acc.v b/accuracy_proofs/gemv_acc.v index 085fddc..ffcdf67 100644 --- a/accuracy_proofs/gemv_acc.v +++ b/accuracy_proofs/gemv_acc.v @@ -181,9 +181,7 @@ apply /RleP; auto with commonDB. apply /RleP; auto with commonDB. - rewrite /normv. -apply bigmax_le => [|i _]. -apply /RleP; auto with commonDB. -auto. +apply :bigmax_le; [apply /RleP | ]; auto with commonDB . Qed. End WithNAN. diff --git a/accuracy_proofs/libvalidsdp.v b/accuracy_proofs/libvalidsdp.v index 2d0a839..6c1aef2 100644 --- a/accuracy_proofs/libvalidsdp.v +++ b/accuracy_proofs/libvalidsdp.v @@ -634,9 +634,9 @@ pose proof @cholesky.lemma_2_1 fspec fspec_eta_nonzero k a' b' (mkFS c) (mkFS bk repeat change (float_spec.FS_val (mkFS ?x)) with (FT2R x) in H|-*. rewrite LVSDP_ytilded_eq in H; auto. replace (\sum_i (float_spec.FS_val _ * _)) with (\sum_i (FT2R (fun_of_fin a i) * (FT2R (b i)))) in H. -2: apply eq_big; auto; [ move => x // | move => i _; rewrite /a' /b' !ffunE //]. +2: by apply: eq_big => [// | i _]; rewrite /a' /b' !ffunE. replace (\sum_i Rabs (float_spec.FS_val _ * _)) with (\sum_i Rabs (FT2R (fun_of_fin a i) * (FT2R (b i)))) in H. -2: apply eq_big; auto; [ move => x // | move => i _; rewrite /a' /b' !ffunE //]. +2: by apply: eq_big => [// | i _]; rewrite /a' /b' !ffunE. rewrite default_abs_eq default_rel_eq. apply H. Qed. @@ -721,8 +721,8 @@ clear H. destruct H0. change i with (nat_of_ord (Ordinal H)). rewrite nth_take. rewrite nth_ord_enum'. -simpl. lia. -simpl; lia. +first [ (* mathcomp 2.4 *) simpl; lia | (* mathcomp 2.5 *) rewrite ltEord; auto]. +first [ (* mathcomp 2.4 *) simpl; lia | (* mathcomp 2.5 *) rewrite ltEord; auto]. Qed. Lemma stilde_subtract_loop: forall [n] (c: F) (R: 'M_n.+1) (i j: 'I_n.+1) (Hij: (i<=j)%N), diff --git a/coq-laproof.opam b/coq-laproof.opam index e1770d3..4f495de 100644 --- a/coq-laproof.opam +++ b/coq-laproof.opam @@ -36,12 +36,14 @@ install: [ [ make "-j%{jobs}%" "install" ] ] depends: [ - "coq" {>= "9.0"} + "rocq-runtime" {>= "9.0~"} # coq-compcert.3.16 requires <9.1 + "coq-menhirlib" {= "20250912"} # to work around https://gitlab.inria.fr/fpottier/menhir/-/issues/84 + "coq-compcert" {= "3.16"} "coq-flocq" "coq-interval" "coq-coquelicot" "coq-vcfloat" {>= "2.3~"} - "coq-mathcomp-ssreflect" {>= "2.4.0~"} + "coq-mathcomp-ssreflect" {>= "2.5.0~"} "coq-mathcomp-algebra" "coq-mathcomp-analysis" "coq-mathcomp-algebra-tactics" @@ -52,6 +54,6 @@ depends: [ "coq-libvalidsdp" {>= "1.1.1"} ] tags: [ - "date:2025-02-11" + "date:2026-02-11" "logpath:LAProof" ]