diff --git a/.gitignore b/.gitignore index 77882f9..5cd85bc 100644 --- a/.gitignore +++ b/.gitignore @@ -1,11 +1,13 @@ -**/Makefile -**/Makefile.conf -**/.CoqMakefile.d -**/.Makefile.d +**/Makefile.rocq +**/Makefile.rocq.conf +**/.Makefile.rocq.d **/*.glob **/*.vo **/*.vok **/*.vos **/.*.aux _opam -_build \ No newline at end of file +_build +freer_playground/.Makefile.d +freer_playground/Makefile +freer_playground/Makefile.conf \ No newline at end of file diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..d80bd56 --- /dev/null +++ b/Makefile @@ -0,0 +1,15 @@ +all: Makefile.rocq + $(MAKE) -f Makefile.rocq all + +clean: Makefile.rocq + $(MAKE) -f Makefile.rocq cleanall + +Makefile.rocq: _CoqProject + rocq makefile -f _CoqProject -o Makefile.rocq + +_CoqProject Makefile: ; + +%: Makefile.rocq + $(MAKE) -f Makefile.rocq $@ + +.PHONY: all clean diff --git a/README.md b/README.md index 21867fe..4f16bcf 100644 --- a/README.md +++ b/README.md @@ -4,14 +4,14 @@ FreerDPS stands for : **Freer** *E*quational *R*easoning for **D**istributed and # Code structure -As of now, the code base is mainly a rewrite of [FreeSpec](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect. +As of now, the code base is mainly a rewrite/extension of [FreeSpec Core](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect. # Install ## Libraries You need to install the following libraries for the project to work : -- coq 9.0 (it will use rocq as soon as monae makes the move) +- Rocq 9.0 - monae - infotheo - mathcomp @@ -28,14 +28,15 @@ opam pin add coq 9.0.0 eval $(opam env) opam repo add coq-released https://coq.inria.fr/opam/released -opam install coq-hierarchy-builder coq-mathcomp-ssreflect coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable coq-mathcomp-classical +opam install coq-hierarchy-builder coq-mathcomp-ssreflect coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable coq-mathcomp-classical +opam install coq-monae coq-infotheo ``` In case monae / infotheo can not be installed through opam, you can clone them from github and fix their versions. Versions known to work : -- monae : dev -- infotheo : 0.9.6 => [I have a local fork for now](https://github.com/forrazh/infotheo/tree/fix/0.9.6) +- monae : 0.9.2 +- infotheo : 0.9.7 You just need to clone the repositories and run : @@ -49,11 +50,10 @@ inside the repository. Once everything is installed, you can run the following commands : ```sh -coq_makefile -f _CoqProject -o Makefile make ``` # Publications -This work has been submitted to COMPAS and is under reviewing. \ No newline at end of file +This work has been submitted and accepted to [COMPAS26](https://2026.compas-conference.fr/) (no paper available online). diff --git a/_CoqProject b/_CoqProject index 5035822..315e68f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -4,6 +4,7 @@ ./theories/Component.v ./theories/Contract.v ./theories/Core.v +./theories/mathcomp_extra.v ./theories/Hoare.v ./theories/HoareFacts.v ./theories/Impure.v diff --git a/dune-project b/dune-project index bda8af8..2cf5074 100644 --- a/dune-project +++ b/dune-project @@ -26,10 +26,10 @@ (coq-mathcomp-classical (= "latest")) (coq (= "9.0")) (coq-stdlib (= "9.0.0")) - (coq-infotheo (= "dev")) + (coq-infotheo (= "0.9.7")) )) -; monae and infotheo are in dev for now because we want +; monae is in dev and infotheo is in 0.9.7 for now because we want ; to use the latest coq version available, which is not ; possible using the current opam versions. diff --git a/freer_playground/theories/FlipMonad.v b/freer_playground/theories/FlipMonad.v index 586d42d..04ac84a 100644 --- a/freer_playground/theories/FlipMonad.v +++ b/freer_playground/theories/FlipMonad.v @@ -1,7 +1,7 @@ Ltac typeof X := type of X. -From Stdlib Require Import ssrmatching Reals. -From mathcomp Require Import ssreflect ssrbool ssralg reals. +From Stdlib Require Import ssrmatching . +From mathcomp Require Import ssreflect ssrnum ssrbool ssralg reals interval_inference. From infotheo Require Import realType_ext. From HB Require Import structures. @@ -14,16 +14,16 @@ Local Open Scope proba_scope. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - +Local Open Scope ring_scope. Local Open Scope reals_ext_scope. - +Local Open Scope convex_scope. (* 1st step : FlipMonad *) HB.mixin Record isMonadFlip {R : realType} (M : UU0 -> UU0) of Monad M := { flip : forall (p : {prob R}), M bool ; (* identity axiom *) - flip1 : flip 1%:pr = Ret true ; + flip1 : flip 1%:i01 = Ret true ; (* skewed commutativity *) - flipNeg : forall (p: {prob R}), flip p = flip (Prob.p p).~%:pr >>= (fun x => Ret (~~x)) ; + flipNeg : forall (p: {prob R}), flip p = flip p%:num.~%:i01 >>= (fun x => Ret (~~x)) ; (* idempotence *) flipmm : forall (A:UU0) p (a:M A), flip p >> a = a ; (* quasi associativity *) @@ -34,7 +34,7 @@ HB.mixin Record isMonadFlip {R : realType} (M : UU0 -> UU0) of Monad M := { (* Prob.p p = (Prob.p r * Prob.p s)%R :> R -> ((Prob.p s).~ = (Prob.p p).~ * (Prob.p q).~)%R -> *) flip p >>= (fun x => if x then a else flip q >>= (fun x0 => if x0 then b else c)) = flip [s_of p, q] >>= - (fun x => if x then flip [r_of p, q] >>= (fun x0 => if x0 then a else b) else c) ; + (fun x => if x then flip [r_of p, q] >>= (fun x0 => if x0 then a else b) else c) ; }. #[short(type=flipMonad)] @@ -52,11 +52,11 @@ Module FlipLib. (*** identity laws ***) -Let flip1 : flip_c 1%:pr = Ret true. +Let flip1 : flip_c 1%:i01 = Ret true. Proof. exact: choice1. Qed. (*** negation law ***) -Let flipNeg : forall p, flip_c p = (flip_c ((Prob.p p).~ %:pr)) >>= (fun x => Ret (~~ x)). +Let flipNeg : forall p, flip_c p = (flip_c (p%:num.~ %:i01)) >>= (fun x => Ret (~~ x)). Proof. by move=>p; rewrite /flip_c/bcoin-choiceC choice_bindDl!bindretf. Qed. @@ -93,13 +93,13 @@ Let choicef (p : {prob R}) (A:UU0) (a b : M A) : M A := flip p >>= (fun x => if (*** identity laws ***) -Let choice1 : forall (A:UU0) (a b : M A), choicef 1%:pr a b = a. +Let choice1 : forall (A:UU0) (a b : M A), choicef 1%:i01 a b = a. Proof. move=>A a b/=. by rewrite /choicef flip1 bindretf. Qed. (*** negation law ***) -Let choiceC : forall (A : UU0) (p:{prob R}) (a b : M A), choicef p a b = choicef ((Prob.p p).~ %:pr) b a. +Let choiceC : forall (A : UU0) (p:{prob R}) (a b : M A), choicef p a b = choicef (p%:num.~ %:i01) b a. Proof. move=> A p a b. rewrite /choicef flipNeg bindA. @@ -164,13 +164,13 @@ Notation pr := (probMonad R). Definition cflip (p : {prob R}) := @bcoin R flipacto p. (*** identity laws ***) -Let flip1 : @cflip 1%:pr = ret R bool true. +Let flip1 : @cflip 1%:i01 = ret R bool true. Proof. exact: choice1. Qed. Ltac rw_choicebind_dl:=rewrite /cflip choice_bindDl!bindretf/=. (*** negation law ***) -Let flipNeg : forall p, cflip p = (cflip ((Prob.p p).~ %:pr) >>= (fun x => ret R bool (~~ x))). +Let flipNeg : forall p, cflip p = (cflip (p%:num.~ %:i01) >>= (fun x => ret R bool (~~ x))). Proof. move=>p. rw_choicebind_dl; diff --git a/freer_playground/theories/lib/FreerFlip.v b/freer_playground/theories/lib/FreerFlip.v index e6a8927..31dad9a 100644 --- a/freer_playground/theories/lib/FreerFlip.v +++ b/freer_playground/theories/lib/FreerFlip.v @@ -1,5 +1,5 @@ From Stdlib Require Import ssrmatching Reals JMeq Relations Morphisms Eqdep. -From mathcomp Require Import ssreflect ssrbool ssrnum ssralg reals. +From mathcomp Require Import ssreflect ssrbool ssrnum ssralg reals interval_inference. From infotheo Require Import realType_ext. From HB Require Import structures. From monae Require Import preamble hierarchy monad_lib. @@ -11,6 +11,8 @@ Local Open Scope monae_scope. Local Open Scope proba_scope. Local Open Scope reals_ext_scope. Local Open Scope freer_flip_scope. +Local Open Scope ring_scope. +Local Open Scope convex_scope. Reserved Notation "x <|| p ||> y" (at level 40, left associativity, y at next level). Reserved Notation "a === b" (at level 90). @@ -51,8 +53,8 @@ Notation "x <|| p ||> y" := (* 5th step : Flip equiv laws *) Inductive flip_rel :forall `[X : UU0] (m1 m2 : M X), Prop := -| rflip1 : flip_rel (flipf 1%:pr) (Ret true) -| rflipNeg : forall p, flip_rel (flipf p) ((flipf (Prob.p p).~%:pr) >>= (fun x => Ret (~~ x))) +| rflip1 : flip_rel (flipf 1%:i01) (Ret true) +| rflipNeg : forall p, flip_rel (flipf p) ((flipf p%:num.~%:i01) >>= (fun x => Ret (~~ x))) | rflipmm : forall (A:UU0) p (a: (M A)), flip_rel (flipf p >> a) a (* quasi associativity *) | rflipA : forall (T:UU0) (p q r s : {prob R}) (a b c : M T), flip_rel @@ -96,7 +98,7 @@ Proof. all: rewrite !denote_trigger/denote_flip_effect. - exact/fA0. - exact/flipmm. - - under eq_bind do rewrite denote_ret; exact/flipNeg. + - under eq_bind do rewrite denote_ret. exact/flipNeg. - rewrite denote_ret; exact/flip1. Qed. diff --git a/theories/Hoare.v b/theories/Hoare.v index cd49a4d..0127ec1 100644 --- a/theories/Hoare.v +++ b/theories/Hoare.v @@ -5,14 +5,13 @@ (* Copyright (C) 2018–2020 ANSSI *) (* From ExtLib Require Import Functor Applicative Monad. *) -From FreerDPS Require Import Interface Impure Contract. -From monae Require Import preamble hierarchy. -From mathcomp Require Import ssreflect. From HB Require Import structures. +From FreerDPS Require Import Interface Impure Contract mathcomp_extra. +From mathcomp Require Import all_boot boolp classical_sets. +From monae Require Import preamble hierarchy. Generalizable All Variables. - Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -30,17 +29,16 @@ Unset Printing Implicit Defensive. (** * Definition *) -Record hoare (Σ : Type) (α : Type) : Type := - mk_hoare { pre : Σ -> Prop - ; post : Σ -> α -> Σ -> Prop - }. +Record hoare (Σ : Type) (α : Type) : Type := mk_hoare { + pre : set Σ ; + post : Σ -> α -> set Σ }. Arguments mk_hoare {Σ α} (pre post). Arguments pre {Σ α} (_ _). Arguments post {Σ α} (_ _ _). Definition hoare_pure {Σ α} (x : α) : hoare Σ α := - mk_hoare (fun _ => True) (fun s y s' => x = y /\ s = s'). + mk_hoare [set: Σ] (fun s y s' => x = y /\ s = s'). Definition hoare_bind {Σ α β} (h : hoare Σ α) (k : α -> hoare Σ β) : hoare Σ β := mk_hoare (fun s => pre h s /\ (forall x s', post h s x s' -> pre (k x) s')) @@ -61,90 +59,78 @@ Definition hoare_apply {Σ α β} (hf : hoare Σ (α -> β)) (h : hoare Σ α) (** ** Monad *) Module hoare_mon. - Section hm. - Variable Σ: UU0. - Let ret := @hoare_pure Σ. - Let bind := @hoare_bind Σ. - - Let right_neutral : BindLaws.right_neutral bind ret. - Proof. - move=>A. rewrite/bind/ret/hoare_bind/hoare_pure/=. - case=>pr po. - congr mk_hoare; apply/boolp.funext=>s. - - apply/boolp.propext; tauto. - apply/boolp.funext=>a; - apply/boolp.funext=>s'. - rewrite boolp.propeqE. - split. case=>a'; case=>s''. - all: move=>/=H. - - firstorder congruence. - by exists a; exists s'. - (* Prop exten *) - Qed. +Section hm. +Variable Σ : UU0. +Let ret := @hoare_pure Σ. +Let bind := @hoare_bind Σ. + +Let right_neutral : BindLaws.right_neutral bind ret. +Proof. +move=> A [pr po]. +rewrite /bind /ret /hoare_bind /hoare_pure/=; congr mk_hoare. +- by apply/funext => s/=; apply/propext; split; tauto. +- apply/eq3_fun => s a s''. + under eq2_exists do rewrite andA. + by rewrite ex2C ex2_eqr ex_eqr. +Qed. (* Local Open Scope ssripat_scope. *) - Let left_neutral : BindLaws.left_neutral bind ret. - Proof. - move=>A B a f. rewrite/bind/ret/hoare_bind/hoare_pure/=. - case eFA: (f a). - congr mk_hoare; apply/boolp.funext=>s. - - apply/boolp.propext=>/=; firstorder. - (* How to specialize ? *) - + by move: H0 eFA => /(_ a s) /[swap] -> /=; exact. - + by subst; rewrite eFA. - - apply/boolp.funext=>b; apply/boolp.funext=>s'. - rewrite boolp.propeqE. - split. - - case=>a'; case=>s''. - all: move=>/=H. - - firstorder. by rewrite -H-H1 eFA in H0. - - exists a; exists s. - rewrite eFA/=; - firstorder. - Qed. - - Let assoc : BindLaws.associative bind. - Proof. - move=>A B C m f g. rewrite/bind/ret/hoare_bind/hoare_pure/=. - case: m=>prA poA. - congr mk_hoare; apply/boolp.funext=>s. - - apply/boolp.propext=>/=; firstorder. - move:x s' x0 s'0 H0 H H1 H2 H3=>a s' b s'' Hcomb _ _ Hpostm Hpostf. - case eGB : (g b). - (* => /=[prC poC]. *) - move: Hcomb eGB=>/(_ b s'')/[swap]->; apply. - exists a; exists s'. - by split. - apply/boolp.funext=>c; - apply/boolp.funext=>s'''. - apply/boolp.propext=>/=. - firstorder; - move:x x0 x1 x2 H H0 H1=>x s'' y s' HpostA Hpostf Hpostg; - exists y; - exists s'; - firstorder. - Qed. - - HB.instance Definition _ := isMonad_ret_bind.Build (hoare Σ) left_neutral right_neutral assoc. - - End hm. +Let left_neutral : BindLaws.left_neutral bind ret. +Proof. +move=> A B a f; rewrite /bind /ret /hoare_bind /hoare_pure/=. +move fa : (f a) => [pr po]; congr mk_hoare. +- apply/funext=> s; rewrite andTP; apply/propext; split. + + by move=> /(_ a s); rewrite fa/=; exact. + + by move=> prs _ _ [<- <-]; rewrite fa. +- apply/eq3_fun => s b s'. + under eq2_exists do rewrite andC andA. + rewrite ex2C. + under eq_exists do rewrite ex_andl. + by rewrite ex_eqr_sym ex_eqr_sym fa. +Qed. + +Let assoc : BindLaws.associative bind. +Proof. +move=> A B C m f g; rewrite /bind /ret /hoare_bind /hoare_pure/=. +case: m => prA poA/=; congr mk_hoare. +- apply/funext => s; apply/propext; split. + + move=> [[prAs poApre postpre]]. + split => // a s1 sas1; split=> [|b s2 s'bs2]. + exact: poApre. + by apply: postpre; exists a, s1. + + move=> [prAs poApre]; split. + by split=> // a s1 /poApre[]. + move=> b s1 [x [s2]] [] /poApre [fxs2] /[swap] s2bs1. + exact. +- apply: eq3_fun => s c s1. + under eq2_exists do rewrite -ex_andl. + rewrite ex3C; apply: eq_exists => a. + under eq2_exists do rewrite -ex_andl. + rewrite ex3C; apply: eq_exists => s2. + rewrite -ex_andr. + under [in RHS]eq_exists do rewrite -ex_andr. + by under [in RHS]eq2_exists do rewrite andA. +Qed. + +HB.instance Definition _ := isMonad_ret_bind.Build (hoare Σ) + left_neutral right_neutral assoc. + +End hm. End hoare_mon. HB.export hoare_mon. (** * Reasoning about Programs *) -Definition interface_to_hoare `{MayProvide ix i} `(c : contract i Ω) : ix ~~> hoare Ω := - fun a e => - {| pre := fun ω => gen_caller_obligation c ω e - ; post := fun ω x ω' => gen_callee_obligation c ω e x - /\ ω' = gen_witness_update c ω e x - |}. +Definition interface_to_hoare `{MayProvide ix i} `(c : contract i Ω) + : ix ~~> hoare Ω := + fun a e => mk_hoare + (fun ω => gen_caller_obligation c ω e) + (fun ω x ω' => gen_callee_obligation c ω e x /\ + ω' = gen_witness_update c ω e x). Definition to_hoare `{MayProvide ix i} {im : impureMonad ix} `(c : contract i Ω) - : im ~~> hoare Ω := + : im ~~> hoare Ω := impure_lift _ (interface_to_hoare c). - Arguments to_hoare {ix i _ im Ω} c {α} : rename. diff --git a/theories/mathcomp_extra.v b/theories/mathcomp_extra.v new file mode 100644 index 0000000..4cf1d41 --- /dev/null +++ b/theories/mathcomp_extra.v @@ -0,0 +1,86 @@ +(* This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at https://mozilla.org/MPL/2.0/. *) + +(**md**************************************************************************) +(* # Temporary logical lemmas awaiting inclusion in MathComp *) +(* *) +(* TODO: Move to MCA *) +(* *) +(* ``` *) +(* eq4_exists == congruence under four existential quantifiers *) +(* andTP == remove `True` from the left of a conjunction *) +(* ex2C == exchange two existential quantifiers *) +(* ex3C == exchange the first and third quantifiers *) +(* ex3AC == exchange the second and third quantifiers *) +(* ex_andl == distribute an existential over a right conjunction *) +(* ex_andr == distribute an existential over a left conjunction *) +(* ex_eqr == eliminate a right equality witness *) +(* ex_eqr_sym == eliminate a symmetric right equality witness *) +(* ex2_eqr == eliminate an equality under two existentials *) +(* ex2_eqr_sym == symmetric version of `ex2_eqr` *) +(* ``` *) +(* *) +(******************************************************************************) + +From mathcomp Require Import all_boot boolp. + +Lemma eq4_exists T S R N + (U V : forall (x : T) (y : S x) (z : R x y), N x y z -> Prop) : + (forall x y z n, U x y z n = V x y z n) -> + (exists x y z n, U x y z n) = (exists x y z n, V x y z n). +Proof. by move=> UV; apply/eq3_exists => x y z; exact/eq_exists. Qed. + +Lemma andTP (P : Prop) : (True /\ P) = P. +Proof. by apply/propext; split => // -[]. Qed. + +Lemma ex2C A B (P : A -> B -> Prop) : + (exists a b, P a b) = (exists b a, P a b). +Proof. by apply/propeqP; split=> -[x [y xy]]; [exists y, x | exists y, x]. Qed. + +Lemma ex3C A B C (P : A -> B -> C -> Prop) : + (exists a b c, P a b c) = (exists c b a, P a b c). +Proof. +apply/propeqP; split=> -[x [y [z xyz]]]. + by exists z, y, x. +by exists z, y, x. +Qed. + +Lemma ex3AC A B C (P : A -> B -> C -> Prop) : + (exists a b c, P a b c) = (exists a c b, P a b c). +Proof. +apply/propeqP; split=> [[a [b [c abc]]] | [a [c [b abc]]]]. + by exists a, c, b. +by exists a, b, c. +Qed. + +Lemma ex_andl A (P : A -> Prop) (Q : Prop) : + (exists a, P a /\ Q) = ((exists a, P a) /\ Q). +Proof. +apply/propeqP; split=> [[a [Pa q]] | [[a Pa] q]]. + by split=> //; exists a. +by exists a. +Qed. + +Lemma ex_andr A (P : Prop) (Q : A -> Prop) : + (exists a, P /\ Q a) = (P /\ (exists a, Q a)). +Proof. +under eq_exists do rewrite andC. +by rewrite ex_andl andC. +Qed. + +Lemma ex_eqr A (a' : A) (P : A -> Prop) : + (exists a, P a /\ a = a') = P a'. +Proof. by apply/propeqP; split=> [[a [Pa <-//]] | Pa']; exists a'. Qed. + +Lemma ex_eqr_sym A (a' : A) (P : A -> Prop) : + (exists a, P a /\ a' = a) = P a'. +Proof. by apply/propeqP; split=> [[a [Pa ->//]] | Pa']; exists a'. Qed. + +Lemma ex2_eqr A B (a' : A) (P : A -> B -> Prop) : + (exists a b, P a b /\ a = a') = (exists b, P a' b). +Proof. by rewrite ex2C; apply: eq_exists => b; rewrite ex_eqr. Qed. + +Lemma ex2_eqr_sym A B (a' : A) (P : A -> B -> Prop) : + (exists a b, P a b /\ a' = a) = (exists b, P a' b). +Proof. by rewrite ex2C; apply: eq_exists => b; rewrite ex_eqr_sym. Qed.