From 12b50ecb1989a4fece58211e429a9a83e4e3b643 Mon Sep 17 00:00:00 2001 From: forrazh <56563878+forrazh@users.noreply.github.com> Date: Thu, 26 Mar 2026 15:51:54 +0100 Subject: [PATCH 1/8] Merge pull request #1 from forrazh/initialise First version of FreerDPS. For now it features : - a rework of most FreeSpec (not everything has been rewritten yet) using + Coq 9.0.0 + monae + mathcomp - a first draft of probabilities usage inside FreeSpec --- .gitignore | 9 +- README.md | 29 +- _CoqProject | 15 + dune-project | 36 ++ examples/airlock.v | 377 ++++++++++++++++++ examples/prob_airlock.v | 188 +++++++++ freer_playground/_CoqProject | 7 + freer_playground/theories/FlipMonad.v | 201 ++++++++++ freer_playground/theories/FreerMonad.v | 173 ++++++++ .../theories/lib/AbstractFreerCoproduct.v | 53 +++ .../theories/lib/ActoFreerCoproduct.v | 166 ++++++++ freer_playground/theories/lib/FreerFlip.v | 119 ++++++ freerdps.opam | 38 ++ theories/Component.v | 100 +++++ theories/Contract.v | 340 ++++++++++++++++ theories/Core.v | 16 + theories/Hoare.v | 150 +++++++ theories/HoareFacts.v | 159 ++++++++ theories/Impure.v | 253 ++++++++++++ theories/Init.v | 39 ++ theories/Instrument.v | 37 ++ theories/Interface.v | 268 +++++++++++++ theories/Semantics.v | 170 ++++++++ theories/Tactics.v | 266 ++++++++++++ theories/Typeclasses.v | 117 ++++++ theories/dune | 8 + 26 files changed, 3328 insertions(+), 6 deletions(-) create mode 100644 _CoqProject create mode 100644 dune-project create mode 100644 examples/airlock.v create mode 100644 examples/prob_airlock.v create mode 100644 freer_playground/_CoqProject create mode 100644 freer_playground/theories/FlipMonad.v create mode 100644 freer_playground/theories/FreerMonad.v create mode 100644 freer_playground/theories/lib/AbstractFreerCoproduct.v create mode 100644 freer_playground/theories/lib/ActoFreerCoproduct.v create mode 100644 freer_playground/theories/lib/FreerFlip.v create mode 100644 freerdps.opam create mode 100644 theories/Component.v create mode 100644 theories/Contract.v create mode 100644 theories/Core.v create mode 100644 theories/Hoare.v create mode 100644 theories/HoareFacts.v create mode 100644 theories/Impure.v create mode 100644 theories/Init.v create mode 100644 theories/Instrument.v create mode 100644 theories/Interface.v create mode 100644 theories/Semantics.v create mode 100644 theories/Tactics.v create mode 100644 theories/Typeclasses.v create mode 100644 theories/dune diff --git a/.gitignore b/.gitignore index 5ce878f..77882f9 100644 --- a/.gitignore +++ b/.gitignore @@ -1,10 +1,11 @@ -.CoqMakefile.d -.Makefile.d -Makefile -Makefile.conf +**/Makefile +**/Makefile.conf +**/.CoqMakefile.d +**/.Makefile.d **/*.glob **/*.vo **/*.vok **/*.vos **/.*.aux _opam +_build \ No newline at end of file diff --git a/README.md b/README.md index e7c5a36..21867fe 100644 --- a/README.md +++ b/README.md @@ -2,6 +2,10 @@ This repo is the home of **FreerDPS**. FreerDPS stands for : **Freer** *E*quational *R*easoning for **D**istributed and **P**robabilistic **S**ystems. +# 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. + # Install ## Libraries @@ -11,6 +15,7 @@ You need to install the following libraries for the project to work : - monae - infotheo - mathcomp +- hierarchy builder ## Commands @@ -20,15 +25,35 @@ Mainly for interns installing it first time : opam switch create . ocaml-base-compiler.4.14.2 eval $(opam env) 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 ``` 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 +- infotheo : 0.9.6 => [I have a local fork for now](https://github.com/forrazh/infotheo/tree/fix/0.9.6) + +You just need to clone the repositories and run : + +```sh +eval $(opam env) # it should be the same switch as the one created above +oam pin add . +``` + +inside the repository. + +Once everything is installed, you can run the following commands : + +```sh +coq_makefile -f _CoqProject -o Makefile +make +``` + # Publications -As of now, no work have been peer-reviewed. \ No newline at end of file +This work has been submitted to COMPAS and is under reviewing. \ No newline at end of file diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..5035822 --- /dev/null +++ b/_CoqProject @@ -0,0 +1,15 @@ +-Q theories FreerDPS +-arg -w -arg -projection-no-head-constant + +./theories/Component.v +./theories/Contract.v +./theories/Core.v +./theories/Hoare.v +./theories/HoareFacts.v +./theories/Impure.v +./theories/Init.v +./theories/Instrument.v +./theories/Interface.v +./theories/Semantics.v +./theories/Tactics.v +./theories/Typeclasses.v diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..bda8af8 --- /dev/null +++ b/dune-project @@ -0,0 +1,36 @@ +(lang dune 3.21) +(warnings (deprecated_coq_lang disabled)) +(using coq 0.9) + +(name freerdps) + +(generate_opam_files true) + +(authors "Hugo Forraz ") + + +(package + (name freerdps) + (synopsis "A FreeSpec rewrite to bring the power of equational reasoning and probabilities.") + (description "A longer description") + (depends + (coq-monae (= "dev")) + (coq-equations (="latest")) + (coq-hierarchy-builder (= "latest")) + (coq-mathcomp-ssreflect (= "latest")) + (coq-mathcomp-algebra (= "latest")) + (coq-mathcomp-character (= "latest")) + (coq-mathcomp-field (= "latest")) + (coq-mathcomp-fingroup (= "latest")) + (coq-mathcomp-solvable (= "latest")) + (coq-mathcomp-classical (= "latest")) + (coq (= "9.0")) + (coq-stdlib (= "9.0.0")) + (coq-infotheo (= "dev")) + )) + +; monae and infotheo are in dev for now because we want +; to use the latest coq version available, which is not +; possible using the current opam versions. + +; (tags (rocq "distributed systems" probabilities)) \ No newline at end of file diff --git a/examples/airlock.v b/examples/airlock.v new file mode 100644 index 0000000..9f125d2 --- /dev/null +++ b/examples/airlock.v @@ -0,0 +1,377 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +From Coq Require Import Arith. +From FreerDPS Require Import Core Impure Hoare. +From monae Require Import preamble hierarchy. + +#[local] Open Scope nat_scope. +#[local] Open Scope monae_scope. + +Create HintDb airlock. + +(** * Specifying *) + +(** ** Doors *) + +Inductive door : Type := left | right. + +Definition door_eq_dec (d d' : door) : { d = d' } + { ~ d = d' } := + ltac:(decide equality). + +Inductive DOORS : interface := +| IsOpen : door -> DOORS bool +| Toggle : door -> DOORS unit. + +Generalizable All Variables. + +Arguments request {_ } _ _ _. + +Check request. + +Section a. + +Definition is_open `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im bool := trigger (inj_p $ IsOpen d). + +Definition toggle `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im unit := trigger (inj_p $ Toggle d). + +Definition open_door `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im unit := + is_open d >>= fun open => + when (negb open) (toggle d). + +Definition close_door `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im unit := + is_open d >>= fun open => + when open (toggle d). + +(** ** Controller *) + +Inductive CONTROLLER : interface := +| Tick : CONTROLLER unit +| RequestOpen (d : door) : CONTROLLER unit. + +Definition tick `{Provide ix CONTROLLER} {im : impureMonad ix} : im unit := + trigger (inj_p Tick). + +Definition request_open `{Provide ix CONTROLLER} {im : impureMonad ix} (d : door) : im unit := + trigger (inj_p $ RequestOpen d). + +Definition co (d : door) : door := + match d with + | left => right + | right => left + end. + +Definition controller `{Provide ix DOORS, Provide ix (STORE nat)} {im : impureMonad ix} + : component (im:=im) CONTROLLER ix + (* . + move=>X; case=>[|d]. + - apply/bind=>[|cpt]. + + apply/iget. + + apply/when. + * apply: (15 [|_]. + -- apply/close_door/left. + -- apply/bind=>[|_]. + ++ apply/close_door/right. + ++ apply/iput/0. + - apply/bind=>[|_]. + + apply/close_door/co/d. + + apply/bind=>[|_]. + * apply/open_door/d. + * apply/iput/0. + Show Proof. *) + := + fun _ op => + match op with + | Tick => + iget >>= fun cpt => + when (15 > + close_door right >> + iput 0 + | RequestOpen d => + close_door (co d) >> + open_door d >> + iput 0 + end. + +(** * Verifying the Airlock Controller *) + +(** ** Doors Specification *) + +(** *** Witness States *) + +Definition Ω : Type := bool * bool. + +Definition sel (d : door) : Ω -> bool := + match d with + | left => fst + | right => snd + end. + +Definition tog (d : door) (ω : Ω) : Ω := + match d with + | left => (negb (fst ω), snd ω) + | right => (fst ω, negb (snd ω)) + end. + +Lemma tog_equ_1 (d : door) (ω : Ω) + : sel d (tog d ω) = negb (sel d ω). + +Proof. + by case:d. +Qed. + +Lemma tog_equ_2 (d : door) (ω : Ω) + : sel (co d) (tog d ω) = sel (co d) ω. + +Proof. + destruct d; reflexivity. +Qed. + +(** From now on, we will reason about [tog] using [tog_equ_1] and [tog_equ_2]. + FreeSpec tactics rely heavily on [cbn] to simplify certain terms, so we use + the <> options of the [Arguments] vernacular command to prevent + [cbn] from unfolding [tog]. + + This pattern is common in FreeSpec. Later in this example, we will use this + trick to prevent [cbn] to unfold impure computations covered by intermediary + theorems. *) + +#[local] Opaque tog. + +Definition step (ω : Ω) (a : Type) (e : DOORS a) (x : a) := + match e with + | Toggle d => tog d ω + | _ => ω + end. + +(** *** Requirements *) + +Inductive doors_o_caller : Ω -> forall (a : Type), DOORS a -> Prop := + +(** - Given the door [d] of o system [ω], it is always possible to ask for the + state of [d]. *) + +| req_is_open (d : door) (ω : Ω) + : doors_o_caller ω bool (IsOpen d) + +(** - Given the door [d] of o system [ω], if [d] is closed, then the second door + [co d] has to be closed too for a request to toggle [d] to be valid. *) + +| req_toggle (d : door) (ω : Ω) (H : sel d ω = false -> sel (co d) ω = false) + : doors_o_caller ω unit (Toggle d). + +Hint Constructors doors_o_caller : airlock. + +(** *** Promises *) + +Inductive doors_o_callee : Ω -> forall (a : Type), DOORS a -> a -> Prop := + +(** - When a system in a state [ω] reports the state of the door [d], it shall + reflect the true state of [d]. *) + +| doors_o_callee_is_open (d : door) (ω : Ω) (x : bool) (equ : sel d ω = x) + : doors_o_callee ω bool (IsOpen d) x + +(** - There is no particular doors_o_calleeises on the result [x] of a request for [ω] to + close the door [d]. *) + +| doors_o_callee_toggle (d : door) (ω : Ω) (x : unit) + : doors_o_callee ω unit (Toggle d) x. + + Hint Constructors doors_o_callee : airlock. + +Definition doors_contract : contract DOORS Ω := + make_contract step doors_o_caller doors_o_callee. + +(** ** Intermediary Lemmas *) + +(** Closing a door [d] in any system [ω] is always a respectful operation. *) + +Lemma close_door_respectful `{Provide ix DOORS} {im : impureMonad ix} (ω : Ω) (d : door) + : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) (doors_contract) (close_door d))( ω). + +Proof. + prove impure with airlock; subst ; constructor. + + (* This leaves us with one goal to prove: + + [sel d ω = false -> sel (co d) ω = false] + + Yet, thanks to our call to [IsOpen d], we can predict that + + [sel d ω = true] *) + + inversion o_caller0; ssubst. + now rewrite H3. +Qed. + + Hint Resolve close_door_respectful : airlock. + +Lemma open_door_respectful `{Provide ix DOORS} (ω : Ω) + (d : door) (safe : sel (co d) ω = false) + : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) doors_contract (open_door (ix := ix) d)) ω. + +Proof. + prove impure; repeat constructor; subst. + by inversion o_caller0; ssubst. +Qed. + + Hint Resolve open_door_respectful : airlock. + +Lemma close_door_run `{Provide ix DOORS} (ω : Ω) (d : door) (ω' : Ω) (x : unit) + (run : post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) doors_contract (close_door d)) ω x ω') + : sel d ω' = false. +Proof. + run_simpl run; + cleanvert H1. + cleanvert run. + cleanvert H1. + run_simpl H2. + + cleanvert H2. + (* cleanvert H4. *) + + - cleanvert H1. + by rewrite tog_equ_1 H5. + by cleanvert run. +Qed. + + Hint Resolve close_door_run : airlock. + +#[local] Opaque close_door. +#[local] Opaque open_door. +#[local] Opaque Nat.ltb. + +Remark one_door_safe_all_doors_safe (ω : Ω) (d : door) + (safe : sel d ω = false \/ sel (co d) ω = false) + : forall (d' : door), sel d' ω = false \/ sel (co d') ω = false. + +Proof. + intros d'. + destruct d; destruct d'; auto. + + cbn -[sel]. + now rewrite or_comm. + + cbn -[sel]. + fold (co right). + now rewrite or_comm. +Qed. + +(** The objective of this lemma is to prove that, if either the right door or + the left door is closed, then after any respectful run of a computation + [p] that interacts with doors, this fact remains true. *) + +#[local] Opaque sel. + +Lemma respectful_run_inv `{Provide ix DOORS} {A} (p : impure ix A) + (ω : Ω) (safe : sel left ω = false \/ sel right ω = false) + (a : A) (ω' : Ω) + (hpre : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) doors_contract p) ω) + (hpost: post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) doors_contract p) ω a ω') + : sel left ω' = false \/ sel right ω' = false. + +(** We reason by induction on the impure computation [p]: + + - Either [p] is a local, pure computation; in such a case, the doors state + does not change, hence the proof is trivial. + + - Or [p] consists in a request to the doors interface, and a continuation + whose domain satisfies the theorem, i.e. it preserves the invariant that + either the left or the right door is closed. Due to this hypothesis, we + only have to prove that the first request made by [p] does not break the + invariant. We consider two cases. + + - Either the computation asks for the state of a given door ([IsOpen]), + then again the doors state does not change and the proof is trivial. + - Or the computation wants to toggle a door [d]. We know by hypothesis + that either [d] is closed or [d] is open (thanks to the + [one_door_safe_all_doors_safe] result and the [safe] hypothesis). + Again, we consider both cases. + + - If [d] is closed —and therefore will be opened—, then because we + consider a respectful run, [co d] is necessarily closed too (it is a + requirements of [door_contract]). Once [d] is opened, [co d] is still + closed. + - Otherwise, [co d] is closed, which means once [d] is toggled (no + matter its initial state), then [co d] is still closed. + + That is, we prove that, when [p] toggles [d], [co d] is necessarily + closed after the request has been handled. Because there is at least + one door closed ([co d]), we can conclude that either the right or the + left door is closed thanks to [one_door_safe_all_doors_safe]. *) + +Proof. + fold (co left) in *. + revert ω hpre hpost safe. + (* elim p=>[a'|B e f IH] ω pre run safe. *) + induction p; intros ω hpre run safe. + + by unroll_post run. + + run_simpl run. + have hpost : post (interface_to_hoare doors_contract (A:=β) e) ω x ω0 + by split; [apply H2| by rewrite H3]. + (* move: H1 => /(_ x ω0) => H1. *) + apply/(H1 x ω0) => //; [by apply hpre|]. + cbn in *. + inversion hpre; rewrite /=/gen_caller_obligation in H4. + (* simplify_gens *) + unfold gen_caller_obligation, gen_callee_obligation, gen_witness_update in *. + cbn in *. + destruct (proj_p e) as [e'|]. + ++ destruct hpost as [o_callee equω]. + destruct e' as [d|d]. + +++ rewrite H3. + apply safe. + +++ apply one_door_safe_all_doors_safe with (d := d); + apply one_door_safe_all_doors_safe with (d' := d) in safe; + subst. + inversion H4. + cbn. + by destruct safe as [safe|safe]; + right; rewrite tog_equ_2//. + ++ rewrite H3; + exact: safe. +Qed. + +(** ** Main Theorem *) +Definition correct_component `{MayProvide jx j} + `(c : component i jx) `(ci : contract i Ωi) `(cj : contract j Ωj) + (pred : Ωi -> Ωj -> Prop) + : Prop := + forall (ωi : Ωi) (ωj : Ωj) (init : pred ωi ωj) + `(e : i α) (o_caller : caller_obligation ci ωi e), + pre (to_hoare cj $ c α e) ωj /\ + forall (x : α) (ωj' : Ωj) (run : post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure jx) cj $ c α e) ωj x ωj'), + callee_obligation ci ωi e x /\ pred (witness_update ci ωi e x) ωj'. + + + +Lemma controller_correct `{StrictProvide2 ix DOORS (STORE nat)} + : correct_component controller + (no_contract CONTROLLER) + doors_contract + (fun _ ω => sel left ω = false \/ sel right ω = false). +Proof. + move=>ωc ωd pred A eff req. + have hpre : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) doors_contract (controller A eff)) ωd. + { + case eff; do ! [prove impure with airlock; ssubst; constructor => //]. + + + (* case eff=> [|d]//; prove impure with airlock; ssubst; constructor=>//. *) + (* do ! [prove impure with airlock; ssubst; constructor=>//=]. *) + - by inversion o_caller; ssubst; rewrite H6. + - by inversion o_caller1; ssubst; rewrite H6. + - by inversion o_caller0; ssubst; rewrite H6. + - by inversion o_caller; ssubst; rewrite H6. + - by inversion o_caller1; ssubst;inversion o_caller; ssubst; rewrite H6 tog_equ_1/=H7. + - by inversion o_caller; ssubst. + } + + split=>[|a ωj' run]//=; + split=>//=. + by apply/(respectful_run_inv _ _ _ _ _ _ run). +Qed. diff --git a/examples/prob_airlock.v b/examples/prob_airlock.v new file mode 100644 index 0000000..6a72df2 --- /dev/null +++ b/examples/prob_airlock.v @@ -0,0 +1,188 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +From Stdlib Require Import Arith. +From FreerDPS Require Import Core Impure Hoare. +From monae Require Import preamble hierarchy. + +From mathcomp Require Import unstable mathcomp_extra ring lra reals Rstruct. +From infotheo Require Import realType_ext ssr_ext fsdist convex. +#[local] Open Scope nat_scope. +#[local] Open Scope monae_scope. +#[local] Open Scope proba_scope. +Local Open Scope reals_ext_scope. + + + +Create HintDb airlock. + +(** * Specifying *) + +(** ** Doors *) + +Locate not_locked_false_eq_true. + +Ltac done := + trivial; hnf; intros; solve + [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial] + | discriminate | contradiction | split] + | match goal with H : ~ _ |- _ => solve [case H; trivial] end + | auto with freespec + ]. +Generalizable All Variables. +Arguments request {_ } _ _ _. + +Module ProbIfaceMod. + Section prob_sec. + Context {R : realType}. +Inductive prob_interface : interface := +| CanWork (p : {prob R}) : prob_interface bool +. + +Definition can_work `{Provide ix prob_interface} {im : impureMonad ix} (p:{prob R}) : im bool := ( trigger (inj_p $ CanWork p)). + + End prob_sec. +End ProbIfaceMod. + +Import ProbIfaceMod. + +Inductive door : Type := left | right. + +Definition door_eq_dec (d d' : door) : { d = d' } + { ~ d = d' } := + ltac:(decide equality). + +Inductive DOORS : interface := +| IsOpen : door -> DOORS bool +| Toggle : door -> DOORS unit. + + + +Check request. + +Section a. + + Context (R : realType). + +Definition is_open `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im bool := trigger (inj_p $ IsOpen d). + +Definition toggle `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im unit := trigger (inj_p $ Toggle d). + +Definition open_door `{Provide2 ix DOORS prob_interface} {im : impureMonad ix} (d : door) (p : {prob R}) : im unit := + can_work p >>= fun ok => when ok $ + is_open d >>= fun open => + when (negb open) (toggle d). + +Definition close_door `{Provide2 ix DOORS prob_interface} {im : impureMonad ix} (d : door) (p: {prob R}): im unit := + can_work p >>= fun ok => when ok $ + is_open d >>= fun open => + when open (toggle d). + +(** ** Controller *) + +Inductive CONTROLLER : interface := +| Tick : CONTROLLER unit +| RequestOpen (d : door) : CONTROLLER unit. + +Definition tick `{Provide ix CONTROLLER} {im : impureMonad ix} : im unit := + trigger (inj_p Tick). + +Definition request_open `{Provide ix CONTROLLER} {im : impureMonad ix} (d : door) : im unit := + trigger (inj_p $ RequestOpen d). + +Definition co (d : door) : door := + match d with + | left => right + | right => left + end. + +Check (forall i, component CONTROLLER i). + +Search iget. + +Definition controller `{Provide ix DOORS, Provide ix (STORE nat), Provide ix prob_interface} {im : impureMonad ix} + : {prob R} -> component (im:=im) CONTROLLER ix + (* . + move=>X; case=>[|d]. + - apply/bind=>[|cpt]. + + apply/iget. + + apply/when. + * apply: (15 [|_]. + -- apply/close_door/left. + -- apply/bind=>[|_]. + ++ apply/close_door/right. + ++ apply/iput/0. + - apply/bind=>[|_]. + + apply/close_door/co/d. + + apply/bind=>[|_]. + * apply/open_door/d. + * apply/iput/0. + Show Proof. *) + := + fun p _ op => + match op with + | Tick => + iget >>= fun cpt => + when (15 > + close_door right p >> + iput 0 + | RequestOpen d => + close_door (co d) p >> + open_door d p >> + iput 0 + end. + +(** * Verifying the Airlock Controller *) + +(** ** Doors Specification *) + +(** *** Witness States *) + +Definition Ω : Type := bool * bool. + +Definition sel (d : door) : Ω -> bool := + match d with + | left => fst + | right => snd + end. + +Definition tog (d : door) (ω : Ω) : Ω := + match d with + | left => (negb (fst ω), snd ω) + | right => (fst ω, negb (snd ω)) + end. + +Lemma tog_equ_1 (d : door) (ω : Ω) + : sel d (tog d ω) = negb (sel d ω). + +Proof. + by case:d. +Qed. + +Lemma tog_equ_2 (d : door) (ω : Ω) + : sel (co d) (tog d ω) = sel (co d) ω. + +Proof. + destruct d; reflexivity. +Qed. + +(** From now on, we will reason about [tog] using [tog_equ_1] and [tog_equ_2]. + FreeSpec tactics rely heavily on [cbn] to simplify certain terms, so we use + the <> options of the [Arguments] vernacular command to prevent + [cbn] from unfolding [tog]. + + This pattern is common in FreeSpec. Later in this example, we will use this + trick to prevent [cbn] to unfold impure computations covered by intermediary + theorems. *) + +#[local] Opaque tog. + +Definition step (ω : Ω) (a : Type) (e : DOORS a) (x : a) := + match e with + | Toggle d => tog d ω + | _ => ω + end. diff --git a/freer_playground/_CoqProject b/freer_playground/_CoqProject new file mode 100644 index 0000000..fa9ab22 --- /dev/null +++ b/freer_playground/_CoqProject @@ -0,0 +1,7 @@ +-Q theories FreerTheories +-arg -w -arg -projection-no-head-constant + +./theories/FreerMonad.v +./theories/FlipMonad.v +./theories/lib/ActoFreerCoproduct.v +./theories/lib/FreerFlip.v diff --git a/freer_playground/theories/FlipMonad.v b/freer_playground/theories/FlipMonad.v new file mode 100644 index 0000000..586d42d --- /dev/null +++ b/freer_playground/theories/FlipMonad.v @@ -0,0 +1,201 @@ +Ltac typeof X := type of X. + +From Stdlib Require Import ssrmatching Reals. +From mathcomp Require Import ssreflect ssrbool ssralg reals. +From infotheo Require Import realType_ext. + +From HB Require Import structures. +From monae Require Import preamble hierarchy monad_lib proba_lib proba_model. + + +Local Open Scope monae_scope. +Local Open Scope proba_scope. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope reals_ext_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 ; + (* skewed commutativity *) + flipNeg : forall (p: {prob R}), flip p = flip (Prob.p p).~%:pr >>= (fun x => Ret (~~x)) ; + (* idempotence *) + flipmm : forall (A:UU0) p (a:M A), flip p >> a = a ; + (* quasi associativity *) + (* flipA : forall (p q r s : {prob R}), + flip p >>= (fun a => flip q >>= (fun b => Ret ))) + = flip [r_of p, q] >>= (fun a => flip [s_of p, q] >>= (fun b => Ret (a && b))) *) + fA0:forall (T:UU0) (p q r s : {prob R}) (a b c : M T), + (* 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) ; +}. + +#[short(type=flipMonad)] +HB.structure Definition MonadFlip {R : realType} := {M of isMonadFlip R M & }. + +Local Open Scope reals_ext_scope. + +Module FlipLib. + (* =========== correct =========== *) + Section proba2flipM. + Variable R : realType. + Variable M : probMonad R. + + Let flip_c (p : {prob R}) : M bool := bcoin p. + + +(*** identity laws ***) +Let flip1 : flip_c 1%:pr = 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)). +Proof. + by move=>p; rewrite /flip_c/bcoin-choiceC choice_bindDl!bindretf. +Qed. + +(*** skewed commutativity law ***) +Let flipmm : forall (A:UU0) (p:{prob R}) (a : M A), flip_c p >> a = a. +Proof. + move=>A p a; rewrite/flip_c/bcoin choice_bindDl 2!bindretf. + exact: choicemm. +Qed. + +(*** quasi assoc law ***) +Let flipA : forall (T:UU0) (p q r s : {prob R}) (a b c : M T), + flip_c p >>= (fun x : bool => if x then a else flip_c q >>= (fun x0 : bool => if x0 then b else c)) + = flip_c [s_of p, q] >>= (fun x : bool => if x then flip_c [r_of p, q] >>= (fun x0 : bool => if x0 then a else b) else c). +Proof. + move=>T p q r s a b c. + rewrite /flip_c/bcoin!choice_bindDl!bindretf. + exact:choiceA. +Qed. + + #[non_forgetful_inheritance] + HB.instance Definition t_ := isMonadFlip.Build R M flip1 flipNeg flipmm flipA. + + End proba2flipM. + + (* =========== complete =========== *) + Section flip2probaM. + Variable R : realType. + Variable M : flipMonad R. + +Let choicef (p : {prob R}) (A:UU0) (a b : M A) : M A := flip p >>= (fun x => if x then a else b). + + + +(*** identity laws ***) +Let choice1 : forall (A:UU0) (a b : M A), choicef 1%:pr 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. +Proof. + move=> A p a b. + rewrite /choicef flipNeg bindA. + congr (flip _ >>= _). + by apply/boolp.funext=>x; + rewrite bindretf if_neg. +Qed. + + +(*** skewed commutativity law ***) +Let choicemm : forall (A : UU0) (p : {prob R}) (a : M A), choicef p a a = a. +Proof. + move=>A p a. + rewrite /choicef -{3}(flipmm A p a). + congr (flip p >> _). + apply/boolp.funext=>x; + exact/if_same. +Qed. + +(*** quasi assoc law ***) +Let choiceA : + forall (T : UU0) (p q : {prob R}), + forall a b c : M T, + choicef p a (choicef q b c) = + choicef [s_of p, q] (choicef [r_of p, q] a b) c. +Proof. + by rewrite/choicef=>A p q a b c; apply: fA0. +Qed. + +Set Warnings "-redundant-canonical-projection". + + #[non_forgetful_inheritance] + HB.instance Definition _ := isMonadConvex.Build R M choicef choice1 choiceC choicemm choiceA. + +Let prob_bindDl p : + BindLaws.left_distributive ( @hierarchy.bind M) (fun A => @choicef p A). +Proof. +move=> A B m1 m2 k. +rewrite !/choicef bindA. +congr (flip p >>= _). +by apply/boolp.funext; case. +Qed. + + #[non_forgetful_inheritance] +HB.instance Definition _ := isMonadProb.Build R M prob_bindDl. + + End flip2probaM. +End FlipLib. + +HB.export FlipLib. + +Module FlipModel. + (* === test with ret/bind === *) +Section ConcreteFlip. + Variable R : realType. + + Definition flipacto := MonadProbModel.acto R. + + +Notation pr := (probMonad R). + +Definition cflip (p : {prob R}) := @bcoin R flipacto p. + +(*** identity laws ***) +Let flip1 : @cflip 1%:pr = 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))). +Proof. + move=>p. + rw_choicebind_dl; + exact: choiceC. +Qed. + + +(*** skewed commutativity law ***) +Let flipmm : forall (A:UU0) (p:{prob R}) (a : flipacto A), (cflip p >>= (fun _ => a)) = a. +Proof. + move=>A p a. + rw_choicebind_dl; exact:choicemm. +Qed. + +(*** quasi assoc law ***) +Let flipA : forall (T:UU0) (p q r s : {prob R}) (a b c : flipacto T), + (cflip p >>= (fun x : bool => if x then a else (cflip q >>= (fun x0 : bool => if x0 then b else c)))) + = (cflip [s_of p, q] >>= (fun x : bool => if x then cflip [r_of p, q] >>= (fun x0 : bool => if x0 then a else b) else c )). +Proof. + move=>T p q r s a b c. + repeat rw_choicebind_dl. exact: choiceA. +Qed. + + HB.instance Definition _ := Monad.on flipacto. + HB.instance Definition _ := isMonadFlip.Build R flipacto flip1 flipNeg flipmm flipA. + +End ConcreteFlip. +End FlipModel. \ No newline at end of file diff --git a/freer_playground/theories/FreerMonad.v b/freer_playground/theories/FreerMonad.v new file mode 100644 index 0000000..bb42e03 --- /dev/null +++ b/freer_playground/theories/FreerMonad.v @@ -0,0 +1,173 @@ +(* TODO: maybe push this to monae instead of using it here ?? *) + +From mathcomp Require Import ssreflect ssrfun. +From monae Require Import monad_lib monad_model monad_transformer hierarchy. +From HB Require Import structures. + +Local Open Scope monae_scope. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Definition Eff : UU0 := UU0 -> UU0. + +HB.mixin Record isFreerMonad (F : Eff) (M : UU0 -> UU0) of Monad M := { + (* F : UU0 -> UU0 ; *) + trigger : F ~~> M ; + denote {cm : monad} (denote_effect : F ~~> cm) : M ~~> cm; + denote_ret : forall (cm : monad) (denote_effect : F ~~> cm) X (x : X), + denote denote_effect X (ret X x) = @ret cm X x; + denote_bind : forall (cm : monad) (denote_effect : F ~~> cm) X Y m (f : X -> M Y), + denote denote_effect Y (m >>= f) = (denote denote_effect X m) >>= (fun x => denote denote_effect Y (f x)) ; + denote_trigger : forall (cm : monad) (denote_effect : F ~~> cm) X (fx : F X), + denote denote_effect X (trigger X fx) = denote_effect X fx; + denote_unique : forall (cm : monad) (denote_effect : F ~~> cm) (denote' : M ~~> cm), + (forall X (x : X), denote' X (ret X x) = @ret cm X x) -> + (forall X Y (m : M X) (f : X -> M Y), denote' Y (m >>= f) = (denote' X m) >>= (fun x => denote' Y (f x))) -> + (forall X (fx : F X), (denote' X (trigger X fx)) = denote_effect X fx) -> + forall X (m : M X), denote' X m = denote denote_effect X m +}. + +#[short(type=freerMonad)] +HB.structure Definition FreerMonad (F : Eff) := {M of isFreerMonad F M & }. + +Module FreerMonadMod. + Section freer. + + Variable F : Eff. + + Inductive Freer (X : UU0) := + | Pure : X -> Freer X + | Impure : forall Y, F Y -> (Y -> Freer X) -> Freer X + . + + Definition acto := fun X : UU0 => Freer X. + + Local Notation M := acto. + + Let ret : idfun ~~> M := fun _ x => Pure x. + + Local Fixpoint bind [A B : UU0] (m : M A) (f : A -> M B) := + match m with + | Pure x => f x + | Impure Y fy k => Impure fy (fun y => bind (k y) f) + end. + + Let left_neutral: BindLaws.left_neutral bind ret . + Proof. + rewrite /BindLaws.left_neutral. + by []. + Qed. + + Let right_neutral : BindLaws.right_neutral bind ret. + Proof. + move=>/=A. + elim=>[x|Y fy k IHm]//=. + congr Impure; + exact/boolp.funext. + Qed. + +Let assoc : BindLaws.associative bind. +Proof. + move=>/=A B C m f g. + elim:m=>//=Y fy k IHm. + congr Impure; + exact/boolp.funext. +Qed. + +HB.instance Definition _ := + isMonad_ret_bind.Build M left_neutral right_neutral assoc. + + End freer. + +End FreerMonadMod. + +HB.export FreerMonadMod. + +Module FreerMod. +Section freer. + +Variable F : Eff. + +Local Notation M := (acto F). + +Let trigger : F ~~> M := fun X fx => Impure fx (fun x => Pure F x). + +Local Fixpoint denote {cm : monad} (denote_effect : F ~~> cm) (X : UU0) (m : M X):cm X:= +match m with +| Pure x => Ret x +| Impure Y fy k => denote_effect Y fy >>= fun y => denote denote_effect (k y) +end. + +Let denote_ret : forall (cm : monad) (denote_effect : F ~~> cm) X (x : X), + denote denote_effect (Ret x) = Ret x. +Proof. + rewrite/=/denote. + by []. +Qed. + + +Let denote_bind (cm : monad) (denote_effect : F ~~> cm) X Y m (f : X -> M Y) : + denote denote_effect (m >>= f) = ( denote denote_effect m) >>= (fun x => denote denote_effect (f x)) . +Proof. + elim:m=>[x | Z fz k]/=. + - by rewrite !bindretf. + rewrite bindA=>H. + congr bind. + exact/boolp.funext/H. +Qed. + +Let denote_trigger : forall (cm : monad) (denote_effect : F ~~> cm) X (fx : F X), + denote denote_effect (trigger fx) = denote_effect X fx. +Proof. + move=>cm denote_effect X fx. + by rewrite/denote/trigger/=bindmret. +Qed. + +Let denote_unique : forall (cm : monad) (denote_effect : F ~~> cm) (denote' : M ~~> cm), + (forall X (x : X), denote' X (ret X x) = @hierarchy.ret cm X x) -> + (forall X Y (m : M X) (f : X -> M Y), denote' Y (m >>= f) = (denote' X m) >>= (fun x => denote' Y (f x))) -> + (forall X (fx : F X), (denote' X (trigger fx)) = denote_effect X fx) -> + forall X (m : M X), denote' X m = denote denote_effect m. +Proof. + move=>cm denote_effect denote' dret' dbind' dtrigger' X m. + rewrite/denote. + elim:m=>[x| Y fy k Hy]/=. + - exact/dret'. + under [in RHS]eq_bind do rewrite -Hy. + by rewrite -dtrigger'-dbind'/trigger. +Qed. + +HB.instance Definition _ := isFreerMonad.Build F M + denote_ret + denote_bind + denote_trigger + denote_unique. + + End freer. +End FreerMod. + +Lemma denote_if : forall (F : Eff) (M : freerMonad F) (cm : monad) (denote_effect : F ~~> cm) X (m m' : M X) b, + denote cm denote_effect X (if b then m else m') = if b then ( denote cm denote_effect X m) else ( denote cm denote_effect X m'). +Proof. + by move=>? ? ? ? ? ? ?; case. +Qed. + +HB.export FreerMod. + +(** This mixin is a first attepmt at equational reasoning, if we ever use it... *) +HB.mixin Record isFreerEquiv (F : Eff) := { + M : freerMonad F ; + cm : monad ; + denote_effect : F ~~> cm ; + equiv_rel : forall X, M X -> M X -> Prop ; + is_equiv_correct : forall (X : UU0) (m1 m2 : M X), + equiv_rel X m1 m2 -> + denote cm denote_effect X m1 = denote cm denote_effect X m2 ; +}. + + +#[short(type=freerMonadEq)] +HB.structure Definition FreerMonadEq := {F of isFreerEquiv F & }. + diff --git a/freer_playground/theories/lib/AbstractFreerCoproduct.v b/freer_playground/theories/lib/AbstractFreerCoproduct.v new file mode 100644 index 0000000..8150515 --- /dev/null +++ b/freer_playground/theories/lib/AbstractFreerCoproduct.v @@ -0,0 +1,53 @@ + +(* ======== Freeeeeee ======== *) + +(* Check monadM. + +HB.mixin Record isFreerMonadCoproduct (F G : Eff) (mf : freerMonad F) (mg : freerMonad G) (cm : monad) (M : UU0 -> UU0) of freerMonad (F<+>G) M := { + cp_left : monadM (mf) M ; + cp_right : monadM mg M ; + from_coproduct : (mf ~~> cm) -> (mg ~~> cm) -> (M ~~> cm) ; + cp_left_law : forall (f : monadM mf cm) (g : monadM mg cm) X (m : mf X), from_coproduct f g X (cp_left X m) = f X m ; + cp_right_law : forall (f : monadM mf cm) (g : monadM mg cm) X (m : mg X), from_coproduct f g X (cp_right X m) = g X m ; + from_coproduct_unique : forall (f : monadM mf cm) (g : monadM mg cm) (c : monadM M cm), (forall X m, c X (cp_left X m) = from_coproduct f g X (cp_left X m)) -> (forall X m, c X (cp_right X m) = from_coproduct f g X (cp_right X m)) -> forall X m, from_coproduct f g X m = c X m +}. + +#[short(type=coprodMF)] +HB.structure Definition CoproductOfMonads (freerMonad F freerMonad G cm : monad) := {M of isMonadCoproduct freerMonad F freerMonad G cm M &}. + + +Module FLeftCoprod. + Section leftc. + Variable F G : UU0 -> UU0. + Variable Mf : freerMonad F. + Variable Mfg : freerMonad (F <+> G). +Definition mmor_left [X] (mf : Mf X) : Mfg X. +case: mf. + +:= match mf with +| Pure x => Pure (F <+> G) x +| Impure Y fy k => Impure (inl fy) (fun y => mmor_left (k y)) +end. + +Let ret : MonadMLaws.ret mmor_left. +Proof. + by []. +Qed. + +Let bind : MonadMLaws.bind mmor_left. +Proof. + move=>a b m f. + elim: m=>[x|Y fy k H]//=. + congr (Impure); + apply/boolp.funext=>y. + by rewrite H. +Qed. + +(* HB.about isMonadM_ret_bind.Build. *) +HB.instance Definition _ := isMonadM_ret_bind.Build (acto F) (acto (F<+>G)) mmor_left ret bind. + End leftc. +End LeftCoprod. + + + + *) diff --git a/freer_playground/theories/lib/ActoFreerCoproduct.v b/freer_playground/theories/lib/ActoFreerCoproduct.v new file mode 100644 index 0000000..9fe0e8c --- /dev/null +++ b/freer_playground/theories/lib/ActoFreerCoproduct.v @@ -0,0 +1,166 @@ + +From Stdlib Require Import ssrmatching Reals JMeq. +From mathcomp Require Import ssreflect. +From HB Require Import structures. +From monae Require Import preamble hierarchy monad_transformer. +From FreerTheories Require Import FreerMonad. + +Local Open Scope monae_scope. +Local Close Scope nat_scope. +Declare Scope fm_scope. +Local Open Scope fm_scope. + +(* Step 3 *) +Notation "F <+> G" := (fun X:Type => F X + G X)%type (at level 50) : fm_scope. + +HB.mixin Record isMonadCoproduct (N N': monad) (M : UU0 -> UU0) of Monad M := { + cp_left : monadM N M ; + cp_right : monadM N' M ; + from_coproduct : forall (cm : monad), + (N ~~> cm) -> (N' ~~> cm) -> (M ~~> cm) ; + cp_left_law : + forall cm + (f : monadM N cm) + (g : monadM N' cm) + X + (m : N X), + from_coproduct cm f g X (cp_left X m) = f X m ; + cp_right_law : forall (cm : monad) (f : monadM N cm) (g : monadM N' cm) X (m : N' X), + from_coproduct cm f g X (cp_right X m) = g X m ; + from_coproduct_unique : forall (cm : monad) (f : monadM N cm) (g : monadM N' cm) (c : monadM M cm), + (forall X m, c X (cp_left X m) = from_coproduct cm f g X (cp_left X m)) + -> (forall X m, c X (cp_right X m) = from_coproduct cm f g X (cp_right X m)) + -> forall X m, from_coproduct cm f g X m = c X m +}. + +#[short(type=coprodM)] +HB.structure Definition CoproductOfMonads (N N' : monad) := {M of isMonadCoproduct N N' M &}. + + +Module LeftCoprod. + Section leftc. + Variable F G : UU0 -> UU0. + +Fixpoint mmor_left [X] (mf : acto F X) : acto (F <+> G) X := match mf with +| Pure x => Pure (F <+> G) x +| Impure Y fy k => Impure (inl fy) (fun y => mmor_left (k y)) +end. + +Let ret : MonadMLaws.ret mmor_left. +Proof. + by []. +Qed. + +Let bind : MonadMLaws.bind mmor_left. +Proof. + move=>a b m f. + elim: m=>[x|Y fy k H]//=. + congr (Impure); + apply/boolp.funext=>y. + by rewrite H. +Qed. + +HB.instance Definition _ := isMonadM_ret_bind.Build (acto F) (acto (F<+>G)) mmor_left ret bind. + + End leftc. +End LeftCoprod. +HB.export LeftCoprod. + +Module RightCoprod. + Section righc. + Variable F G : UU0 -> UU0. + +Fixpoint mmor_right [X] (mf : acto G X) : acto (F <+> G) X := match mf with +| Pure x => Pure (F <+> G) x +| Impure Y fy k => Impure (inr fy) (fun y => mmor_right (k y)) +end. + +Let ret : MonadMLaws.ret mmor_right. +Proof. + move=>a. + by []. +Qed. + +Let bind : MonadMLaws.bind mmor_right. +Proof. + move=>a b m f. + elim: m=>[x|Y fy k H]//=. + congr (Impure); + apply/boolp.funext=>y. + by rewrite H. +Qed. + +HB.instance Definition _ := isMonadM_ret_bind.Build (acto G) (acto (F<+>G)) mmor_right ret bind. + + End righc. +End RightCoprod. +HB.export RightCoprod. + +Module FullCoprod. + Section cop. + Variable F G : UU0 -> UU0. + Notation Nacto := (acto F). + Notation Nacto':= (acto G). + Notation Macto := (acto (F<+>G)). + +Variable ammor_left : forall {X} (MF:freerMonad F) (MFG:freerMonad (F <+> G)) (mf : MF X), MFG X. +Variable ammor_right : forall {X} (MG:freerMonad G) (MFG:freerMonad (F <+> G)) (mg : MG X), MFG X. + +Definition ctrigger `{X:UU0} (MF:freerMonad F) (MG:freerMonad G) {MFG : freerMonad (F<+>G)} (fg : (F<+>G) X) + : MFG X. +Proof. + case: fg=>[fx|gx]. + apply/(ammor_left MF)/trigger/fx. + apply/(ammor_right MG)/trigger/gx. +Defined. + +Local Fixpoint from_coproduct (cm : monad) (l : Nacto ~~> cm) (r : Nacto' ~~> cm) `[X:UU0] (m : Macto X) : cm X +:= match m with +| Pure x => ret X x +| Impure Y fgy k => match fgy with + | inl f => l Y (Impure f (fun y:Y => Pure F y)) + | inr g => r Y (Impure g (fun y:Y => Pure G y)) + end >>= fun y => from_coproduct cm l r (k y) +end +. + +Notation mmor_l := (mmor_left F G). +Notation mmor_r := (mmor_right F G). + + +Let cp_left_law : forall (cm : monad) (f : monadM Nacto cm) (g : monadM Nacto' cm) X (m : Nacto X), from_coproduct cm f g (mmor_l m) = f X m. +Proof. + move=>cm f g X. + elim=>[x|Y fy k H]/=. + by rewrite -(monadMret (s:=f)). + under eq_bind do rewrite H. + by rewrite -monadMbind. +Qed. +Let cp_right_law : forall (cm : monad) (f : monadM Nacto cm) (g : monadM Nacto' cm) X (m : Nacto' X), from_coproduct cm f g (mmor_r m) = g X m. +Proof. + move=>cm f g X. + elim=>[x|Y fy k H]/=. + by rewrite -(monadMret (s:=g)). + under eq_bind do rewrite H. + by rewrite -monadMbind. +Qed. + +Let from_coproduct_unique : forall (cm : monad) (f : monadM Nacto cm) (g : monadM Nacto' cm) (c : monadM Macto cm), (forall X m, c X (mmor_l m) = from_coproduct cm f g (mmor_l m)) -> (forall X m, c X (mmor_r m) = from_coproduct cm f g (mmor_r m)) -> forall X m, from_coproduct cm f g m = c X m. +Proof. + move=>cm f g c Hl Hr X. + elim=>[x|Y fgy ky H]/=. + by rewrite/=-(monadMret (s:=c)). + under eq_bind do rewrite H. + by case: fgy=>[fy|gy]; + rewrite -?(cp_left_law cm f g) -?Hl + -?(cp_right_law cm f g) -?Hr + /=-(monadMbind (s:=c)). + +Qed. + +HB.instance Definition _ := isMonadCoproduct.Build (Nacto) (Nacto') (Macto) mmor_l mmor_r from_coproduct cp_left_law cp_right_law from_coproduct_unique. + + End cop. +End FullCoprod. + +HB.export FullCoprod. diff --git a/freer_playground/theories/lib/FreerFlip.v b/freer_playground/theories/lib/FreerFlip.v new file mode 100644 index 0000000..e6a8927 --- /dev/null +++ b/freer_playground/theories/lib/FreerFlip.v @@ -0,0 +1,119 @@ +From Stdlib Require Import ssrmatching Reals JMeq Relations Morphisms Eqdep. +From mathcomp Require Import ssreflect ssrbool ssrnum ssralg reals. +From infotheo Require Import realType_ext. +From HB Require Import structures. +From monae Require Import preamble hierarchy monad_lib. +From FreerTheories Require Import FlipMonad FreerMonad. + +Declare Scope freer_flip_scope. + +Local Open Scope monae_scope. +Local Open Scope proba_scope. +Local Open Scope reals_ext_scope. +Local Open Scope freer_flip_scope. + +Reserved Notation "x <|| p ||> y" (at level 40, left associativity, y at next level). +Reserved Notation "a === b" (at level 90). + +Module FreerFlipModel. + + Section freer_flip. +Variable R:realType. + +Inductive FlipEff : UU0 -> UU0 := +| flip_e (p : {prob R}) : FlipEff bool +. + + +Arguments trigger {_ _ _}. +Variable M : (freerMonad FlipEff). + + +Definition flipf (p:{prob R}) := ( @trigger FlipEff M bool (flip_e p)). + + +(* Let fa := flipacto R. *) +Variable fl : flipMonad R. + +Definition denote_flip_effect : FlipEff ~~> fl := +fun X fx => match fx with +| flip_e p => flip p +end. + +Notation choice_of_Type := monad_model.choice_of_Type. + +Definition choicef {X} (p : {prob R}) (a b : M X) := flipf p >>= (fun b0 => if b0 then a else b). + +Notation "x <|| p ||> y" := + (choicef p x y) +(at level 40, left associativity, y at next level) : freer_flip_scope. + + +(* 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))) +| 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 + (a <|| p ||> (b <|| q ||> c)) + ((a <|| [r_of p, q] ||> b) <|| [s_of p, q] ||> c) + (* (flipf p >>= (fun x : bool => if x then a else flipf q >>= (fun x0 : bool => if x0 then b else c))) *) + (* (flipf [s_of p, q] >>= (fun x : bool => if x then flipf [r_of p, q] >>= (fun x0 : bool => if x0 then a else b) else c)) *) +| equiv_bind_congr : forall (A B :UU0) (a b : M A) (f g : A -> M B), + (* a === b -> (forall x, (f x) === (g x)) -> (a >>= f) === (b >>= g) *) + flip_rel a b -> (forall x, flip_rel (f x) (g x)) -> flip_rel (a >>= f) (b >>= g) +| equiv_refl : forall (A:UU0) (m : M A), flip_rel m m +| equiv_sym : forall (A:UU0) (m n : M A), flip_rel m n -> flip_rel n m +| equiv_trans : forall (A:UU0) (m n o : M A), flip_rel m n -> flip_rel n o -> flip_rel m o +. + +(* 6th step : Equiv correct *) +Lemma equiv_correct : forall (X : UU0) (m1 m2 : M X), + @flip_rel X m1 m2 -> + denote fl denote_flip_effect X m1 = denote fl denote_flip_effect X m2. +Proof. + move=>X m1 m2 H. + (* rewrite/denote/=. *) + elim: H=>[| p | A p a | T p q r s a b c + | A B a b f g Hab H Hfg H' + | A m | A m n Hmn H | A m n o Hmn H Hno H' + ]/= + ; last first. + - by rewrite H H'. + - by rewrite H. + - by []. + - rewrite !denote_bind ; congr bind. + + exact/H. + + apply/boolp.funext/H'. + (* all: rewrite/=. *) + all: rewrite ?denote_bind. + (* flip_a *) + under eq_bind do rewrite denote_if denote_bind; + under [in RHS]eq_bind do rewrite denote_if denote_bind; + under eq_bind do under eq_bind do rewrite denote_if; + under [in RHS]eq_bind do under eq_bind do rewrite denote_if. + all: rewrite !denote_trigger/denote_flip_effect. + - exact/fA0. + - exact/flipmm. + - under eq_bind do rewrite denote_ret; exact/flipNeg. + - rewrite denote_ret; exact/flip1. +Qed. + +HB.instance Definition _ := isFreerEquiv.Build FlipEff equiv_correct. + +Notation "a === b" := +(flip_rel a b) + (at level 90) : freer_flip_scope. + +End freer_flip. +End FreerFlipModel. + +HB.export FreerFlipModel. + +Arguments flip_rel {_ _ _}. +Arguments flipf {_ _}. +Arguments choicef {_ _ _}. + + + diff --git a/freerdps.opam b/freerdps.opam new file mode 100644 index 0000000..8abe52a --- /dev/null +++ b/freerdps.opam @@ -0,0 +1,38 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: + "A FreeSpec rewrite to bring the power of equational reasoning and probabilities." +description: "A longer description" +authors: ["Hugo Forraz "] +depends: [ + "dune" {>= "3.21"} + "coq-monae" {= "dev"} + "coq-equations" {= "latest"} + "coq-hierarchy-builder" {= "latest"} + "coq-mathcomp-ssreflect" {= "latest"} + "coq-mathcomp-algebra" {= "latest"} + "coq-mathcomp-character" {= "latest"} + "coq-mathcomp-field" {= "latest"} + "coq-mathcomp-fingroup" {= "latest"} + "coq-mathcomp-solvable" {= "latest"} + "coq-mathcomp-classical" {= "latest"} + "coq" {= "9.0"} + "coq-stdlib" {= "9.0.0"} + "coq-infotheo" {= "dev"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +x-maintenance-intent: ["(latest)"] diff --git a/theories/Component.v b/theories/Component.v new file mode 100644 index 0000000..4714b8e --- /dev/null +++ b/theories/Component.v @@ -0,0 +1,100 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +(* From ExtLib Require Import StateMonad. *) +From mathcomp Require Import ssreflect. +From FreerDPS Require Export Interface Semantics Impure. +From monae Require Import preamble hierarchy monad_lib. +From HB Require Import structures. +(** * Definition *) + +(** In FreeSpec, a _component_ is an entity which exposes an interface [i], + and uses primitives of an interface [j] to compute the results of primitives + of [i]. Besides, a component is likely to carry its own internal state (of + type [s]). + +<< + i +-------------------+ j + | | | | + +------>| | c : component i j |----->| + | | | | + +-------------------+ +>> + + Thus, a component [c : component i j] is a polymorphic function which + maps primitives of [i] to impure computations using [j]. *) + +Definition component (i j : interface) `{im : impureMonad j} : Type := + forall (α : Type), i α -> im α. + +(** The similarity between FreeSpec components and operational semantics may be + confusing at first. The main difference between the two concepts is simple: + operational semantics are self-contained terms which can, alone, be used to + interpret impure computations of a given interface. Components, on the + other hand, are not self-contained. Without an operational semantics for + [j], we cannot use a component [c : component i j] to interpret an impure + computation using [i]. + + Given an initial semantics for [j], we can however derive an operational + semantics for [i] from a component [c]. *) + +(** * Semantics Derivation *) + + +CoFixpoint derive_semantics {i j} {im : impureMonad j} (c : component i j) (sem : semantics j) + : semantics i := + mk_semantics (fun a p => + let (res, next) := (to_state (α:=im) _ $ c a p) sem in + (res, derive_semantics c next)). + +(** So, [semprod] on the one hand allows for composing operational semantics + horizontally, and [derive_semantics] allows for composing components + vertically. Using these two operators, we can model a complete system in a + hierarchical and modular manner, by defining each of its components + independently, then composing them together with [semprod] and + [derive_semantics]. *) + +Definition bootstrap {i} {im : impureMonad iempty} (c : component i iempty) : semantics i := + derive_semantics (im:=im) c iempty_semantics. + +(** * In-place Primitives Handling *) + +(** The function [with_component] allows for locally providing an additional + interface [j] within an impure computation of type [impure ix a]. The + primitives of [j] will be handled by impure computations, i.e., a component. + of type [c : compoment j ix s]. *) +Local Open Scope monae_scope. + + +#[local] +Fixpoint with_component_aux {ix j α} + (* {im : impureMonad ix} *) + (* {jm : impureMonad (ix + j)} *) +(c : component (im:=Impure.ImpureModule_acto__canonical__Impure_MonadImpure ix) j ix) (p : impure (ix + j) α) + : impure ix α := + match p with + | local x => local x + | request_then T (in_right e) f => + c T e >>= fun res => with_component_aux c (f res) + | request_then _ (in_left e) f => + request_then e (fun x => with_component_aux c (f x)) + end. + +Notation "m >>= f" := (impure_bind m f). +Notation "m >> f" := (impure_bind m (fun _ =>f)). + +Definition with_component {ix j α} + (* `{im : impureMonad ix} + `{ixjm : impureMonad (ix+j)} *) + (initializer : impure ix unit) + (c : component (im:=Impure.ImpureModule_acto__canonical__Impure_MonadImpure ix) j ix) + (finalizer : impure ix unit) + (p : impure (ix+j) α) + : impure ix α := + initializer >> + with_component_aux c p >>= fun res => + finalizer >> + local res. diff --git a/theories/Contract.v b/theories/Contract.v new file mode 100644 index 0000000..c975c77 --- /dev/null +++ b/theories/Contract.v @@ -0,0 +1,340 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +(** In this library, we provide the necessary material to reason about FreeSpec + components both in isolation, and in composition. To do that, we focus our + reasoning principles on interfaces, by defining how their primitives shall + be used, and what to expect the result computed by “correct” operational + semantics (according to a certain definition of “correct”). *) + +From Stdlib Require Import Setoid Morphisms. +(* From ExtLib Require Import StateMonad MonadState MonadTrans. *) +From FreerDPS Require Import Interface Impure Semantics Component. +From mathcomp Require Import ssreflect. +From monae Require Import preamble hierarchy. +#[local] +Open Scope signature_scope. +Open Scope monae_scope. + +Generalizable All Variables. + +(** * Definition *) + +(** A contract dedicated to [i : interface] primarily provides two + predicates. + + - [caller_obligation] distinguishes between primitives that can be used (by + an impure computation), and primitives that cannot be used. + - [callee_obligation] specifies which guarantees can be expected from + primitives results, as computed by a “good” operational semantics. + + Both [caller_obligation] and [callee_obligation] model properties that may + vary in time, e.g., a primitive may be forbidden at a given time, but + authorized later. To take this possibility into account, contracts are + parameterized by what we have called a “witness.” A witness is a term which + describes the necessary information of the past, and allows for taking + decision for the present. It can be seen as an abstraction of the concrete + state of the interface implementor. + + To keep this state up-to-date after each primitive interpretation, + contracts also define a dedicated function [witness_update]. *) + +Record contract (i : interface) (Ω : Type) : Type := make_contract + { witness_update (ω : Ω) : forall (α : Type), i α -> α -> Ω + ; caller_obligation (ω : Ω) : forall (α : Type), i α -> Prop + ; callee_obligation (ω : Ω) : forall (α : Type), i α -> α -> Prop + }. + +Declare Scope contract_scope. +Bind Scope contract_scope with contract. + +Arguments make_contract [i Ω] (_ _ _). +Arguments witness_update [i Ω] (c ω) [α] (_ _). +Arguments caller_obligation [i Ω] (c ω) [α] (_). +Arguments callee_obligation [i Ω] (c ω) [α] (_ _). + +(** The most simple contract we can define is the one that requires + anything both for the impure computations which uses the primitives of a + given interface, and for the operational semantics which compute results for + these primitives. *) + +Definition const_witness {i} := + fun (u : unit) (α : Type) (e : i α) (x : α) => u. + +Inductive no_caller_obligation {i Ω} (ω : Ω) (α : Type) (e : i α) : Prop := +| mk_no_caller_obligation : no_caller_obligation ω α e. + +#[global] Hint Constructors no_caller_obligation : freespec. + +Inductive no_callee_obligation {i Ω} (ω : Ω) (α : Type) (e : i α) (x : α) : Prop := +| mk_no_callee_obligation : no_callee_obligation ω α e x. + +#[global] Hint Constructors no_callee_obligation : freespec. + +Definition no_contract (i : interface) : contract i unit := + {| witness_update := const_witness + ; caller_obligation := no_caller_obligation + ; callee_obligation := no_callee_obligation + |}. + +(** A similar —and as simple— contract is the one that forbids the use of a + given interface. *) + +Definition do_no_use {i Ω} (ω : Ω) (α : Type) (e : i α) : Prop := False. + +Definition forbid_specs (i : interface) : contract i unit := + {| witness_update := const_witness + ; caller_obligation := do_no_use + ; callee_obligation := no_callee_obligation + |}. + +(** * Contract Equivalence *) + +Definition contract_caller_equ `(c1 : contract i Ω1) `(c2 : contract i Ω2) + (f : Ω1 -> Ω2) + : Prop := + forall ω1 a (p : i a), + caller_obligation c1 ω1 p <-> caller_obligation c2 (f ω1) p. + +Definition contract_callee_equ `(c1 : contract i Ω1) `(c2 : contract i Ω2) + (f : Ω1 -> Ω2) + : Prop := + forall ω1 a (p : i a) x, + callee_obligation c1 ω1 p x <-> callee_obligation c2 (f ω1) p x. + +Definition contract_witness_equ `(c1 : contract i Ω1) `(c2 : contract i Ω2) + (f : Ω1 -> Ω2) + : Prop := + forall ω1 a (p : i a) x, + f (witness_update c1 ω1 p x) = witness_update c2 (f ω1) p x. + +Inductive contract_equ `(c1 : contract i Ω1) `(c2 : contract i Ω2) + : Type := +| mk_contract_equ (f : Ω1 -> Ω2) (g : Ω2 -> Ω1) + (iso1 : forall x, f (g x) = x) (iso2 : forall x, g (f x) = x) + (caller_equ : contract_caller_equ c1 c2 f) + (callee_equ : contract_callee_equ c1 c2 f) + (witness_equ : contract_witness_equ c1 c2 f) + : contract_equ c1 c2. + +Definition contract_iso_lr `(c1 : contract i Ω1) `(c2 : contract i Ω2) + (equ : contract_equ c1 c2) (ω1 : Ω1) + : Ω2 := + match equ with + | @mk_contract_equ _ _ _ _ _ f _ _ _ _ _ _ => f ω1 + end. + +Definition contract_iso_rl `(c1 : contract i Ω1) `(c2 : contract i Ω2) + (equ : contract_equ c1 c2) (ω2 : Ω2) + : Ω1 := + match equ with + | @mk_contract_equ _ _ _ _ _ _ g _ _ _ _ _ => g ω2 + end. + +Arguments contract_iso_lr {i Ω1 c1 Ω2 c2} (equ ω1). +Arguments contract_iso_rl {i Ω1 c1 Ω2 c2} (equ ω2). + +Lemma contract_equ_refl `(c : contract i Ω) + : contract_equ c c. + +Proof. + apply mk_contract_equ with (f:=fun x => x) (g:=fun x => x); auto. + + now intros ω α p. + + now intros ω α p x. + + now intros ω α p x. +Defined. + +Lemma contract_equ_sym `(c1 : contract i Ω1) `(c2 : contract i Ω2) + (equ : contract_equ c1 c2) + : contract_equ c2 c1. + +Proof. + induction equ. + apply mk_contract_equ with (f:=g) (g:=f). + + apply iso2. + + apply iso1. + + intros ω α p. + transitivity (caller_obligation c2 (f (g ω)) p). + ++ now rewrite iso1. + ++ now symmetry. + + intros ω α p x. + transitivity (callee_obligation c2 (f (g ω)) p x). + ++ now rewrite iso1. + ++ now symmetry. + + intros ω α p x. + rewrite <- (iso2 (witness_update c1 (g ω) p x)). + assert (equ : witness_update c2 ω p x = f (witness_update c1 (g ω) p x)). { + transitivity (witness_update c2 (f (g ω)) p x). + + now rewrite iso1. + + now rewrite witness_equ. + } + now rewrite equ. +Defined. + +Lemma contract_equ_trans `(c1 : contract i Ω1) `(c2 : contract i Ω2) + `(c3 : contract i Ω3) + `(is_equ12 : contract_equ c1 c2) + `(is_equ23 : contract_equ c2 c3) + : contract_equ c1 c3. + +Proof. + destruct is_equ12 as [f12 g21 isofg12 isogf12 caller_equ12 callee_equ12 witness_equ12]. + destruct is_equ23 as [f23 g32 isofg23 isogf23 caller_equ23 callee_equ23 witness_equ23]. + apply mk_contract_equ + with (f:=fun x => f23 (f12 x)) (g:=fun x => g21 (g32 x)). + + setoid_rewrite isofg12. + now setoid_rewrite isofg23. + + setoid_rewrite isogf23. + now setoid_rewrite isogf12. + + intros ω1 α p. + transitivity (caller_obligation c2 (f12 ω1) p); + [ now apply caller_equ12 + | now apply caller_equ23 ]. + + intros ω1 α p x. + transitivity (callee_obligation c2 (f12 ω1) p x); [ now apply callee_equ12 + | now apply callee_equ23 ]. + + intros ω1 α p x. + rewrite <- witness_equ23. + assert (equ : f12 (witness_update c1 ω1 p x) = witness_update c2 (f12 ω1) p x) + by now rewrite <- witness_equ12. + now rewrite equ. +Defined. + +(** * Composing Contracts *) + +(** As we compose interfaces and operational semantics, we can easily compose + contracts together, by means of the [contractprod] operator. Given [i] and [j] + two interfaces, if we can reason about [i] and [j] independently (e.g., the + caller obligations of [j] do not vary when we use [i]), then we can compose + [ci : contract i Ωi] and [cj : contract j Ωj], such that [contractprod ci cj] in a + contract for [i + j]. *) + +Definition gen_witness_update `{MayProvide ix i} {Ω α} (c : contract i Ω) + (ω : Ω) (e : ix α) (x : α) + : Ω := + match proj_p e with + | Some e => witness_update c ω e x + | None => ω + end. + +Definition gen_caller_obligation `{MayProvide ix i} {Ω α} (c : contract i Ω) + (ω : Ω) (e : ix α) + : Prop := + match proj_p e with + | Some e => caller_obligation c ω e + | None => True + end. + +Definition gen_callee_obligation `{MayProvide ix i} {Ω α} (c : contract i Ω) + (ω : Ω) (e : ix α) (x : α) + : Prop := + match proj_p e with + | Some e => callee_obligation c ω e x + | None => True + end. + +Definition contractprod `{Provide ix i, Provide ix j} {Ωi Ωj} + (ci : contract i Ωi) (cj : contract j Ωj) + : contract ix (Ωi * Ωj) := + {| witness_update := fun (ω : Ωi * Ωj) (α : Type) (e : ix α) (x : α) => + (gen_witness_update ci (fst ω) e x, gen_witness_update cj (snd ω) e x) + ; caller_obligation := fun (ω : Ωi * Ωj) (α : Type) (e : ix α) => + gen_caller_obligation ci (fst ω) e /\ gen_caller_obligation cj (snd ω) e + ; callee_obligation := fun (ω : Ωi * Ωj) (α : Type) (e : ix α) (x : α) => + gen_callee_obligation ci (fst ω) e x /\ gen_callee_obligation cj (snd ω) e x + |}. + +Infix "*" := contractprod : contract_scope. + +(** We also introduce a second composition operator which shares the + witness state among its two operands. *) + +(* FIXME: Should be [StrictProvide2 ix i j] *) + +Definition sharedcontractprod `{Provide ix i, Provide ix j} + `(ci : contract i Ω) (cj : contract j Ω) + : contract ix Ω := + {| + witness_update := + fun (ω : Ω) (α : Type) (e : ix α) (x : α) => + (* we need to check [i] before [j] because [sharedcontractprod] + will be right associative *) + match proj_p (i:=i) e with + | Some e => witness_update ci ω e x + | _ => match proj_p (i:=j) e with + | Some e => witness_update cj ω e x + | _ => ω + end + end; + caller_obligation := + fun (ω : Ω) (α : Type) (e : ix α) => + gen_caller_obligation ci ω e /\ gen_caller_obligation cj ω e; + callee_obligation := + fun (ω : Ω) (α : Type) (e : ix α) (x : α) => + gen_callee_obligation ci ω e x /\ gen_callee_obligation cj ω e x + |}. + +Infix "^" := sharedcontractprod : contract_scope. + +(** * Contract By Example *) + +(** Finally, and as an example, we define a contract for the interface + [STORE s] we discuss in [FreeSpec.Core.Impure]. As a reminder, the + interface is defined as follows: + +<< +Inductive STORE (s : Type) : interface := +| Get : STORE s s +| Put (x : s) : STORE s unit. +>> + + For [STORE s], the best witness is the actual value of the mutable + variable. Therefore, the contract for [STORE s] may be [specs (STORE + s) s], and the witness will be updated after each [Put] call. *) + +Definition store_update (s : Type) := + fun (x : s) (α : Type) (e : STORE s α) (_ : α) => + match e with + | Get => x + | Put x' => x' + end. + +(** Assuming the mutable variable is being initialized prior to any impure + computation interpretation, we do not have any obligations over the use of + [STORE s] primitives. We will get back to this assertion once we have + defined our contract, but in the meantime, we define its callee obligation. + + The logic of these callee obligations is as follows: [Get] is expected to + produce a result strictly equivalent to the witness, and we do not have any + obligations about the result of [Put] (which belongs to [unit] anyway, so + there is not much to tell). *) + +Inductive o_callee_store (s : Type) (x : s) : forall (α : Type), STORE s α -> α -> Prop := +| get_o_callee (x' : s) (equ : x = x') : o_callee_store s x s Get x' +| put_o_callee (x' : s) (u : unit) : o_callee_store s x unit (Put x') u. + +(** The actual contract can therefore be defined as follows: *) + +Definition store_specs (s : Type) : contract (STORE s) s := + {| witness_update := store_update s + ; caller_obligation := no_caller_obligation + ; callee_obligation := o_callee_store s + |}. + +(** Now, as we briefly mentionned, this contract allows for reasoning about an + impure computation which uses the [STORE s] interface, assuming the mutable, + global variable has been initialized. We can define another contract that + does not rely on such assumption, and on the contrary, requires an impure + computation to initialize the variable prior to using it. + + In this context, the witness can solely be a boolean which tells if the + variable has been initialized, and the [callee_obligation] will require the + witness to be [true] to authorize a call of [Get]. + + This is one of the key benefits of the FreeSpec approach: because the + contracts are defined independently from impure computations and + interfaces, we can actually define several contracts to consider + different set of hypotheses. *) diff --git a/theories/Core.v b/theories/Core.v new file mode 100644 index 0000000..90c26c9 --- /dev/null +++ b/theories/Core.v @@ -0,0 +1,16 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +From FreerDPS Require Export + Interface + Typeclasses + Impure + Semantics + Component + Contract + Hoare + Tactics + . \ No newline at end of file diff --git a/theories/Hoare.v b/theories/Hoare.v new file mode 100644 index 0000000..cd49a4d --- /dev/null +++ b/theories/Hoare.v @@ -0,0 +1,150 @@ +(* 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/. *) + +(* 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. + +Generalizable All Variables. + + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** To reason about impure computations, we introduce the “Hoare + monad,” also called the “specification monad.” An instance of the + specification monad is a couple of [pre] and [post] conditions, + such that [pre p σ] means the program specified by [p] can be + executed safely from a state [σ], and [post p σ x σ'] means the + execution of [p] from [σ] may compute a result [x] and bring the + system to a state [σ']. + + We equip this couple of predicate with a [bind] function to + sequentially compose specifications. *) + +(** * Definition *) + +Record hoare (Σ : Type) (α : Type) : Type := + mk_hoare { pre : Σ -> Prop + ; post : Σ -> α -> Σ -> Prop + }. + +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'). + +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')) + (fun s x s'' => exists y s', post h s y s' /\ post (k y) s' x s''). + +(** * Instances *) + +(** ** Functor *) + +Definition hoare_map {Σ α β} (f : α -> β) (h : hoare Σ α) : hoare Σ β := + hoare_bind h (fun x => hoare_pure (f x)). + +(** ** Applicative *) + +Definition hoare_apply {Σ α β} (hf : hoare Σ (α -> β)) (h : hoare Σ α) + : hoare Σ β := + hoare_bind hf (fun f => hoare_map f h). + +(** ** 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. + +(* 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. +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 to_hoare `{MayProvide ix i} {im : impureMonad ix} `(c : contract i Ω) + : im ~~> hoare Ω := + impure_lift _ (interface_to_hoare c). + +Arguments to_hoare {ix i _ im Ω} c {α} : rename. diff --git a/theories/HoareFacts.v b/theories/HoareFacts.v new file mode 100644 index 0000000..13b1be2 --- /dev/null +++ b/theories/HoareFacts.v @@ -0,0 +1,159 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +From mathcomp Require Import ssreflect. +From FreerDPS Require Import Interface Impure Contract Hoare. +From monae Require Import preamble hierarchy. +Generalizable All Variables. + +(** * General Lemmas *) + +Lemma to_hoare_step `{MayProvide ix i} `(c : contract i Ω) + `(e : ix a) `(f : a -> impure ix a) + `(hpre : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (request_then e f)) ω) + (x : a) (step : gen_callee_obligation c ω e x) + : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (f x)) (gen_witness_update c ω e x). + +Proof. + destruct hpre as [hbefore hafter]. + apply hafter. + cbn. + unfold gen_callee_obligation, gen_witness_update in *. + now destruct proj_p. +Qed. + +#[global] Hint Resolve to_hoare_step : freespec. + +Lemma to_hoare_pre_bind_assoc `{MayProvide ix i} `(c : contract i Ω) + `(p : impure ix a) `(Hp : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c p) ω) + `(f : a -> impure ix b) + (run : forall (x : a) (ω' : Ω), + post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c p) ω x ω' -> pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (f x)) ω') + : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (impure_bind p f)) ω. + +Proof. + revert ω Hp run. + induction p; intros ω Hp run. + + now apply run. + + cbn in Hp. + destruct Hp as [He Hn]. + change (impure_bind (request_then e f0) f) + with (impure_bind (request_then e (fun x => f0 x)) f). + split. + ++ exact He. + ++ intros x ω' Hpost. + specialize Hn with x ω'. + destruct Hpost. + rewrite -> H2 in *. + assert (Hpre : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (f0 x)) (gen_witness_update c ω e x)) + by now apply Hn. + apply H0; [ apply Hpre |]. + intros y ω'' Hpost. + apply run. + cbn. + exists x. + exists ω'. + split; [split |]. + +++ exact H1. + +++ exact H2. + +++ rewrite H2. + exact Hpost. +Qed. + +Lemma to_hoare_post_bind_assoc `{MayProvide ix i} `(c : contract i Ω) + `(p : impure ix a) `(f : a -> impure ix b) + `(Hp : post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (impure_bind p f)) ω x ω') + : exists y ω'', + post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c p) ω y ω'' /\ post (to_hoare c (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) $ f y) ω'' x ω'. + +Proof. +move: ω Hp; elim p=>[in_a|Y j k IH] ω. +- by exists in_a, ω. +case=>y [ω'' [Hp1 ]]. +move:IH=>/[apply]. +move=> [z [ω''' [Hp2 Hp3]]]. +exists z, ω'''. +split=>//. +exists y, ω''. +by split. +Qed. + +Lemma to_hoare_contractprod `{Provide ix i, Provide ix j} + `(ci : contract i Ωi) `(cj : contract j Ωj) + `(p : impure ix a) + `(prei : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) ci p) ωi) `(prej : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) cj p) ωj) + : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) (ci * cj) p) (ωi, ωj). + +Proof. + revert ωi prei ωj prej. + induction p; intros ωi prei ωj prej. + + auto. + + destruct prei as [calleri Hcalleei]. + destruct prej as [callerj Hcalleej]. + split. + ++ now split. + ++ intros x [ωi' ωj'] [[calleei calleej] equωs]. + cbn in equωs. + inversion equωs; subst. + apply H3. + +++ apply Hcalleei. + now split. + +++ apply Hcalleej. + now split. +Qed. + +#[global] Hint Resolve to_hoare_contractprod : freespec. + +Lemma contract_equ_pre `(c1 : contract i Ω1) `(c2 : contract i Ω2) + `(equ : contract_equ c1 c2) (ω1 : Ω1) + `(p : impure i A) + : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure i) c1 p) ω1 <-> pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure i) c2 p) (contract_iso_lr equ ω1). + +Proof. + elim: equ => f g iso1 iso2 caller_equ callee_equ witness_equ. + move: ω1. + elim: p=> [a | B e k IH] ω1. + - by split. + rewrite /=/gen_caller_obligation/gen_callee_obligation/gen_witness_update/=. + rewrite (caller_equ ω1 B e). + setoid_rewrite (callee_equ ω1 B e). + split => [[ocaller onext] | [ocaller onext]]; + split => // x ω1' [ocallee owitness]. + - by rewrite owitness -witness_equ -IH; eauto. + rewrite IH; eauto. + rewrite owitness /= witness_equ; eauto. +Qed. + +#[global] Hint Resolve contract_equ_pre : freespec. + +Lemma contract_equ_post `(c1 : contract i Ω1) `(c2 : contract i Ω2) + `(equ : contract_equ c1 c2) (ω1 ω1' : Ω1) + `(p : impure i a) (x : a) + (post1 : post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure i) c1 p) ω1 x ω1') + : post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure i) c2 p) (contract_iso_lr equ ω1) x (contract_iso_lr equ ω1'). + +Proof. + induction equ. + cbn in *. + revert x ω1 ω1' post1. + induction p; intros y ω1 ω1' post1. + + destruct post1 as [xequ ω1equ]. + cbn. + now subst. + + cbn in post1. + destruct post1 as [x [ω1'' [[ocallee owitness] post1]]]. + eapply H in post1. + exists x. + exists (f ω1''). + split; auto. + cbn. + repeat split. + ++ eapply callee_equ; eauto. + ++ rewrite owitness. + apply witness_equ. +Qed. + +#[global] Hint Resolve contract_equ_post : freespec. diff --git a/theories/Impure.v b/theories/Impure.v new file mode 100644 index 0000000..e92a80c --- /dev/null +++ b/theories/Impure.v @@ -0,0 +1,253 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +(** In [FreeSpec.Core.Interface], we have introduced the [interface] type, to + model the set of primitives an impure computation can use. We also introduce + [MayProvide], [Provide] and [Distinguish]. They are three type classes which + allow for manipulating _polymorphic interface composite_. + + + In this library, we provide the [impure] monad, defined after the + <> monad introduced by the <> package (see + <>). *) + +From mathcomp Require Import ssreflect ssrfun. +From Stdlib Require Import Program Setoid Morphisms. +From HB Require Import structures. +From monae Require Import preamble hierarchy. +From FreerDPS Require Export Interface. + +Local Open Scope monae_scope. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Generalizable All Variables. + +(** We introduce the [impure] monad to describe impure computations, that is + computations which uses primitives from certain interfaces. *) + +(** * Definition *) + +(** The [impure] monad is an inductive datatype with two parameters: the + interface [i] to be used, and the type [α] of the result of the computation. + The fact that [impure] is inductive rather than co-inductive means it is not + possible to describe infinite computations. This also means it is possible + to interpret impure computations within Coq, providing an operational + semantics for [i]. *) + +Inductive impure (i : interface) (α : Type) : Type := +| local (x : α) : impure i α +| request_then {β} (e : i β) (f : β -> impure i α) : impure i α. + +Arguments local [i α] (x). +Arguments request_then [i α β] (e f). + +Register impure as freespec.core.impure.type. +Register local as freespec.core.impure.local. +Register request_then as freespec.core.impure.request_then. + +Declare Scope impure_scope. +Bind Scope impure_scope with impure. +Delimit Scope impure_scope with impure. + +HB.mixin Record isMonadImpure (i : interface) (M : UU0 -> UU0) of Monad M := { + request : i ~~> M ; + impure_lift (N : monad) (l : i ~~> N) : M ~~> N ; + impure_lift_ret : forall (N : monad) (l : i ~~> N) X (x : X), + impure_lift N l X (ret X x) = @ret N X x; + impure_lift_bind : forall (N : monad) (l : i ~~> N) X Y m (f : X -> M Y), + impure_lift N l Y (m >>= f) = (impure_lift N l X m) >>= (fun x => impure_lift N l Y (f x)) ; + impure_lift_request : forall (N : monad) (l : i ~~> N) X (fx : i X), + impure_lift N l X (request X fx) = l X fx; + impure_lift_unique : forall (N : monad) (l : i ~~> N) (impure_lift' : M ~~> N), + (forall X (x : X), impure_lift' X (ret X x) = @ret N X x) -> + (forall X Y (m : M X) (f : X -> M Y), impure_lift' Y (m >>= f) = (impure_lift' X m) >>= (fun x => impure_lift' Y (f x))) -> + (forall X (fx : i X), (impure_lift' X (request X fx)) = l X fx) -> + forall X (m : M X), impure_lift' X m = impure_lift N l X m +}. + + +#[short(type=impureMonad)] +HB.structure Definition MonadImpure (i : interface) := {M of isMonadImpure i M & isMonad M & isFunctor M}. + +(** * Monad Instances *) + +(** We then provide the necessary instances of the <> Monad + typeclasses hierarchy. *) +Module ImpureModule. +Section freer. + +Variable i : UU0 -> UU0. +Definition acto := fun X => @impure i X. +Notation FM := acto. + +Definition impure_pure {α} (x : α) : impure i α := local x. + +Let ret : idfun ~~> FM := fun _ => impure_pure. + +Fixpoint impure_bind {α β} (p : impure i α) (f : α -> impure i β) : impure i β := + match p with + | local x => f x + | request_then Y e g => request_then e (fun x => impure_bind (g x) f) + end. + +Let bind := fun A B m f => @impure_bind A B m f. + +Let left_neutral : BindLaws.left_neutral bind ret. +Proof. + by []. +Qed. + +Let right_neutral : BindLaws.right_neutral bind ret. +Proof. + move=>/=A. + elim=>[x|Y fy k IHm]//=. + congr request_then. + exact/boolp.funext=>y. +Qed. + +Let assoc : BindLaws.associative bind. +Proof. + move=>/=A B C m f g. + elim:m=>//=Y fy k IHm. + congr request_then. + exact/boolp.funext=>y. +Qed. + +HB.instance Definition _ := @isMonad_ret_bind.Build acto ret bind left_neutral right_neutral assoc. + +(** * Defining Impure Computations *) + +(** FreeSpec users shall not use the [impure] monad constructors directly. The + [pure] function from the [Applicative] typeclass allows for defining pure + computations which do not depend on any impure primitive. The [bind] + function from the [Monad] typeclass allows for seamlessly combine impure + computations together. + + To complete these two monadic operations, we introduce the [request] + function, whose purpose is to define an impure computation that uses a given + primitive [e] from an interface [i], and returns its result. [request] does + not parameterize the [impure] monad with [i] directly, but rather with a + generic interface [ix]. [ix] is constrained with the [Provide] notation, so + that it has to provide at least [i]'s primitives. *) + +End freer. +End ImpureModule. + +HB.export ImpureModule. + +Module Impure. +Section freer. + +Variable i : interface. + +Local Notation M := (acto i). + +Definition requesti : i ~~> acto i := fun α e => + request_then (inj_p e) (fun x => local x). + +Definition lifter (M : monad) `(l : i ~~> M) : acto i ~~> M := + fix aux a (p : acto i a) := + match p with + | local x => Ret x + | request_then Y e f => l _ e >>= fun x => aux a (f x) + end. + +Let lifter_ret : forall (cm : monad) (lifter_effect : i ~~> cm) X (x : X), + lifter lifter_effect (ret X x) = @hierarchy.ret cm X x. +Proof. + rewrite/=/lifter. + by []. +Qed. + + +Let lifter_bind : forall (cm : monad) (lifter_effect : i ~~> cm) X Y m (f : X -> M Y), + lifter lifter_effect (m >>= f) = ( lifter lifter_effect m) >>= (fun x => lifter lifter_effect (f x)) . +Proof. + move=>cm lifter_effect X Y m f. + elim:m=>[x | Z fz k]/=. + - by rewrite !bindretf. + rewrite bindA=>H. + congr bind. + exact/boolp.funext/H. +Qed. + +Let lifter_trigger : forall (cm : monad) (lifter_effect : i ~~> cm) X (fx : i X), + lifter lifter_effect (requesti fx) = lifter_effect X fx. +Proof. + move=>cm lifter_effect X fx. + by rewrite/lifter/requesti/=bindmret. +Qed. + +Let lifter_unique : forall (cm : monad) (lifter_effect : i ~~> cm) (lifter' : M ~~> cm), + (forall X (x : X), lifter' X (ret X x) = @hierarchy.ret cm X x) -> + (forall X Y (m : M X) (f : X -> M Y), lifter' Y (m >>= f) = (lifter' X m) >>= (fun x => lifter' Y (f x))) -> + (forall X (fx : i X), (lifter' X (requesti fx)) = lifter_effect X fx) -> + forall X (m : M X), lifter' X m = lifter lifter_effect m. +Proof. + move=>cm lifter_effect lifter' dret' dbind' dtrigger' X m. + rewrite/lifter. + elim:m=>[x| Y fy k Hy]/=. + - exact/dret'. + under [in RHS]eq_bind do rewrite -Hy. + by rewrite -dtrigger'-dbind'/requesti. +Qed. + +HB.instance Definition _ := isMonadImpure.Build i M + lifter_ret + lifter_bind + lifter_trigger + lifter_unique. + +End freer. +End Impure. +HB.export Impure. + +Lemma impure_lift_if : forall (i : interface) (M : impureMonad i) (cm : monad) (lifter_effect : i ~~> cm) X (m m' : M X) b, + impure_lift cm lifter_effect X (if b then m else m') = if b then ( impure_lift cm lifter_effect X m) else ( impure_lift cm lifter_effect X m'). +Proof. + by move=>? ? ? ? ? ? ?; case. +Qed. +HB.export impure_lift_if. + +Module ImpSt. + Section impstate. + Variable i : interface. + Variable S : UU0. +Definition requestis `{Provide ix i} {A} (e : i A): acto ix A := + request_then (inj_p e) (fun x => local x). + + Let iget `{Provide i (STORE S)} : acto i S:=requestis (inj_p Get). + Let iput `{Provide i (STORE S)} (s : S) : acto i ():=requestis (inj_p (Put s)). + +(** Note: there have been attempts to turn [request] into a typeclass + function (to seamlessly use [request] with a [MonadTrans] instance such as + [state_t]). The reason why it has not been kept into the codebase is that + the flexibility it gives for writing code has a real impact on the + verification process. It is simpler to reason about “pure” impure + computations (that is, not within a monad stack), then wrapping these + computations thanks to [lift]. + + The <> provides notations (inspired by the do notation of + Haskell) to write monadic functions more easily. These notations live + inside the [monad_scope]. *) + +(** * Lift *) + + End impstate. +End ImpSt. + +(* HB.export ImpSt. *) + +Module ImpureFuns. +Definition trigger `{Provide ix i} {im : impureMonad ix} : ix ~~> im := fun a e => request a (inj_p e). +Definition iget {S} `{Provide i (STORE S)} {im : impureMonad i} : im S:= trigger (inj_p Get). +Definition iput {S} `{Provide i (STORE S)} {im : impureMonad i} (s : S) : im unit:= trigger (inj_p (Put s)). +End ImpureFuns. + +HB.export ImpureFuns. \ No newline at end of file diff --git a/theories/Init.v b/theories/Init.v new file mode 100644 index 0000000..1c1b509 --- /dev/null +++ b/theories/Init.v @@ -0,0 +1,39 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +(** * Utils Functions *) +(* From HB Require Export structures. *) +From monae Require Export preamble hierarchy. +From mathcomp Require Export ssreflect. +Ltac done := + trivial; hnf; intros; solve + [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial] + | discriminate | contradiction | split] + | match goal with H : ~ _ |- _ => solve [case H; trivial] end + | auto with freespec + ]. +Local Open Scope monae_scope. + +Definition when {X} {M : monad} (b : bool) (m : M X) : M unit := if b then m >> skip else skip. +Notation "f $ x" := (f x) (at level 60, right associativity, only parsing). + +(** * Tactics *) + +From Stdlib Require Export Eqdep. + +Ltac ssubst := + lazymatch goal with +| [ H : existT _ _ _ = existT _ _ _ |- _ ] + => apply Eqdep.EqdepTheory.inj_pair2 in H; ssubst +| [ |- _] => subst +end. + +Reserved Infix "===" (at level 70, no associativity). + +Generalizable All Variables. + +Definition function_eq {a b} (r : b -> b -> Prop) (f g : a -> b) : Prop := + forall (x : a), r (f x) (g x). diff --git a/theories/Instrument.v b/theories/Instrument.v new file mode 100644 index 0000000..d16c1c2 --- /dev/null +++ b/theories/Instrument.v @@ -0,0 +1,37 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +From FreerDPS Require Import Interface Semantics Contract. +From monae Require Import preamble hierarchy monad_transformer monad_model. +From HB Require Import structures. + +From mathcomp Require Import ssreflect. +Generalizable All Variables. + +Notation instrument Ω i := (stateT Ω (StateMonad.acto (semantics i))). + + +Definition modify {S} {M : stateMonad S} (f : S -> S) : M S := get >>= + fun s => put (f s) >>= + fun _ => Ret s. + +Arguments liftS {_ _ _}. +Arguments interface_to_state {_ _}. + + +Program Definition interface_to_instrument `{MayProvide ix i} `(c : contract i Ω) + : ix ~~> instrument Ω ix := + fun a e => + (liftS (A:=a) $ interface_to_state e) + >>= fun x => modify (fun ω => gen_witness_update c ω e x) + >>= fun _ => Ret x. + +Definition to_instrument `{MayProvide ix i} `(c : contract i Ω) {im : impureMonad ix} + : im ~~> instrument Ω ix := + impure_lift _ $ interface_to_instrument c. + +Arguments to_instrument {ix i _ Ω} (c) {α} : rename. + diff --git a/theories/Interface.v b/theories/Interface.v new file mode 100644 index 0000000..5961d61 --- /dev/null +++ b/theories/Interface.v @@ -0,0 +1,268 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +From FreerDPS Require Export Init. +From Stdlib Require Import Program. + +(** * Definition *) + +(** Following the definition of the <> package, interfaces in + FreeSpec are parameterized inductive types whose terms purposely describe + the primitives the interface provides. *) + +Definition interface := Type -> Type. + +Declare Scope interface_scope. +Bind Scope interface_scope with interface. + +(** Given [i : interface], a term of type [i α] identifies a primitive of [i] + expected to produce a result of type [α]. + + The simpler interface is the empty interface, which provides no primitives + whatsoever. *) + +Inductive iempty : interface := . + +(** Another example of general-purpose interface we can define is the [STORE s] + interface, where [s] is a type for a state, and [STORE s] allows for + manipulating a global, mutable variable of type [s] within an impure + computation. *) + +Inductive STORE (s : Type) : interface := +| Get : STORE s s +| Put (x : s) : STORE s unit. + +Arguments Get {s}. +Arguments Put [s] (x). + +(** According to the definition of [STORE s], an impure computation can use two + primitives. The term [Get : STORE s s] describes a primitive expected to + produce a result of type [s], that is the current value of the mutable + variable. Terms of the form [Put x : STORE s unit] describe a primitive + which does not produce any meaningful result, but is expected to update the + current value of the mutable variable. + + The use of the word “expected” to describe the primitive of [STORE s] is + voluntary. The definition of an interface does not attach any particular + semantics to the primitives it describes. This will come later, and in + fact, one interface may have many legitimate semantics. + + Impure computations are likely to use more than one interface, but the + [impure] monad takes only one argument. We introduce [iplus] (denoted by + [<+>] or [⊕]) to compose interfaces together. An impure computation + parameterized by [i ⊕ j] can therefore leverage the primitives of both [i] + and [j]. *) + +(** * Polymorphic Interface Composites *) + +(** When defining general-purpose impure computations that we expect to reuse in + different context, we want to leave the interface as a parameter, and rather + express the constraints in terms of interface availability. We tackle this + challenge by means of _interface composites_. + + - We say an interface composite [ix] _provides_ a concrete interface [i] + when there exists a function [inj_p : forall α, i α -> ix α]. + - Conversely, we can determine if a primitive of an interface composite [ix] + is forwarded to a concrete interface [i] when there exists a function + [proj_p : forall α, ix α -> option (i a)]. + + We encode this mechanics using two type classes: [MayProvide], and + [Provide]. *) + +Class MayProvide (ix i : interface) : Type := + { proj_p {α} (e : ix α) : option (i α) + }. + +Class Provide (ix i : interface) `{MayProvide ix i} : Type := + { inj_p {α} (e : i α) : ix α + ; proj_inj_p_equ {α} (e : i α) : proj_p (inj_p e) = Some e + }. + +(** We provide a default instance for [MayProvide] in the form of a function + [proj_p] which always return [None]. We give to this default instance a + ridiculously high priority number to ensure it is selected only if no other + instances are found. *) + +Instance default_MayProvide (i j : interface) : MayProvide i j|1000 := + { proj_p := fun _ _ => None + }. + +(** It is expected that, for an interface composite [ix] which provides [i] and + may provide [j], [inj_p] and [proj_p] do not mix up [i] and [j] + primitives. That is, injecting a primitive [e] of [i] inside [ix], then + projecting the resulting primitive into [j] returns [None] as long as [i] + and [j] are two different interfaces. *) + +Class Distinguish (ix i j : interface) `{Provide ix i, MayProvide ix j} : Prop := + { distinguish : forall {α} (e : i α), proj_p (i := j) (inj_p (ix := ix) e) = None + }. + +(** * Composing Interfaces *) + +(** We provide the [iplus] operator to compose interface together. That is, + [iplus] can be used to build _concrete_ (as opposed to polymorphic) + interface composite. *) + +Inductive iplus (i j : interface) (α : Type) := +| in_left (e : i α) : iplus i j α +| in_right (e : j α) : iplus i j α. + +Arguments in_left [i j α] (e). +Arguments in_right [i j α] (e). + +Register iplus as freespec.core.iplus.type. +Register in_left as freespec.core.iplus.in_left. +Register in_right as freespec.core.iplus.in_right. + +Infix "+" := iplus : interface_scope. + +(** For [iplus] to be used seamlessly as a concrete interface composite, we + provide the necessary instances for the [MayProvide], [Provide] and + [Distinguish] type classes. Note that these instances always prefer the + left operand of [iplus]. For instance, considering a situation where + there is an instance for [Provide ix i] and an instance for [Provide jx i], + the instance of [Provide (ix + jx) i] will rely on [ix]. + + The main use case for [iplus] is to locally provide an additional + interface. For instance, we can consider a [with_state] function which would + locally give access to the [STORE] interface, that is [with_state : forall + ix s α, s -> impure (ix + STORE s) α -> impure ix α]. In such a case, the + interface made locally available shall be the right operand of [iplus]. This + way, functions such as [with_state] are reentrant. If we take an example, + the following impure computation: + +<< +with_state true (with_state false get) +>> + + will return false (that is, the variable in the inner store). *) + +Instance refl_MayProvide (i : interface) : MayProvide i i := + { proj_p := fun _ e => Some e + }. + +#[program] +Instance refl_Provide (i : interface) : @Provide i i (refl_MayProvide i) := + { inj_p := fun (a : Type) (e : i a) => e + }. + +Instance iplus_left_MayProvide (ix i j : interface) `{MayProvide ix i} + : MayProvide (ix + j) i := + { proj_p := fun _ e => + match e with + | in_left e => proj_p e + | _ => None + end + }. + +#[program] +Instance iplus_left_Provide (ix i j : interface) `{Provide ix i} + : @Provide (ix + j) i (iplus_left_MayProvide ix i j) := + { inj_p := fun (a : Type) (e : i a) => in_left (inj_p e) + }. + +Next Obligation. + now rewrite proj_inj_p_equ. +Qed. + +Instance iplus_right_MayProvide (i jx j : interface) `{MayProvide jx j} + : MayProvide (i + jx) j := + { proj_p := fun _ e => + match e with + | in_right e => proj_p e + | _ => None + end + }. + +#[program] +Instance iplus_right_Provide (i jx j : interface) `{Provide jx j} + : @Provide (i + jx) j (iplus_right_MayProvide i jx j) := + { inj_p := fun _ e => in_right (inj_p e) + }. + +Next Obligation. + now rewrite proj_inj_p_equ. +Qed. + +(** By default, Coq's inference algorithm for type classe instances inference is + a depth-first search. This is not without consequence in our case. For + instance, if we consider the search of an instance for [MayProvide (i + j) + j], Coq will first try [iplus_right_MayProvide] (as explained previously), + meaning he now search for [MayProvide i j]. It turns out such an instance + exists: [default_MayProvide]. + + To circumvent this issue, we write a dedicated tactic [find_may_provide] + which attempts to find an instance for [MayProvide (?ix + ?jx) ?i] with + [refl_MayProvide], [iplus_left_MayProvide] and [iplus_right_MayProvide]. *) + +Ltac find_may_provide := + eapply refl_MayProvide + + (eapply iplus_left_MayProvide; find_may_provide) + + (eapply iplus_right_MayProvide; find_may_provide). + +#[global] Hint Extern 1 (MayProvide (iplus _ _) _) => find_may_provide : typeclass_instances. + +#[program] +Instance refl_Distinguish (i j : interface) + : @Distinguish i i j ( @refl_MayProvide i) ( @refl_Provide i) ( @default_MayProvide i j). + +#[program] +Instance iplus_left_default_Distinguish (ix jx i j : interface) + `{M1 : MayProvide ix i} `{P1 : @Provide ix i M1} + : @Distinguish (ix + jx) i j + ( @iplus_left_MayProvide ix i jx M1) + ( @iplus_left_Provide ix i jx M1 P1) + ( @default_MayProvide _ j). + +#[program] +Instance iplus_right_default_Distinguish (ix jx i j : interface) + `{M1 : MayProvide jx i} `{P1 : @Provide jx i M1} + : @Distinguish (ix + jx) i j + ( @iplus_right_MayProvide ix jx i M1) + ( @iplus_right_Provide ix jx i M1 P1) + ( @default_MayProvide _ j). + +#[program] +Instance iplus_left_may_right_Distinguish (ix jx i j : interface) + `{M1 : MayProvide ix i} `{P1 : @Provide ix i M1} `{M2 : MayProvide jx j} + : @Distinguish (ix + jx) i j + ( @iplus_left_MayProvide ix i jx M1) + ( @iplus_left_Provide ix i jx M1 P1) + ( @iplus_right_MayProvide ix jx j M2). + +#[program] +Instance iplus_right_may_left_Distinguish (ix jx i j : interface) + `{M1 : MayProvide jx i} `{P1 : @Provide jx i M1} `{M2 : MayProvide ix j} + : @Distinguish (ix + jx) i j + ( @iplus_right_MayProvide ix jx i M1) + ( @iplus_right_Provide ix jx i M1 P1) + ( @iplus_left_MayProvide ix j jx M2). + +#[program] +Instance iplus_left_distinguish_left_Distinguish (ix jx i j : interface) + `{M1 : MayProvide ix i} `{P1 : @Provide ix i M1} `{M2 : MayProvide ix j} + `{@Distinguish ix i j M1 P1 M2} + : @Distinguish (ix + jx) i j + ( @iplus_left_MayProvide ix i jx M1) + ( @iplus_left_Provide ix i jx M1 P1) + ( @iplus_left_MayProvide ix j jx M2). + +Next Obligation. + apply distinguish. +Defined. + +#[program] +Instance iplus_right_distinguish_right_Distinguish (ix jx i j : interface) + `{M1 : MayProvide jx i} `{P1 : @Provide jx i M1} `{M2 : MayProvide jx j} + `{@Distinguish jx i j M1 P1 M2} + : @Distinguish (ix + jx) i j + ( @iplus_right_MayProvide ix jx i M1) + ( @iplus_right_Provide ix jx i M1 P1) + ( @iplus_right_MayProvide ix jx j M2). + +Next Obligation. + apply distinguish. +Defined. diff --git a/theories/Semantics.v b/theories/Semantics.v new file mode 100644 index 0000000..4145bfa --- /dev/null +++ b/theories/Semantics.v @@ -0,0 +1,170 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +(** In FreeSpec, there is no particular semantics attach to interface's + primitives. Once an interface has been defined, we can provide one (or + more) operational semantics to interpret its primitives. *) + +(** * Definition *) + +(** An operational [semantics] for the interface [i] is coinductively defined as + a function which can be used to interpret any primitive of [i]; it produces + an [interp_out] term. *) + +From mathcomp Require Import ssreflect. + +From Stdlib Require Import Program Setoid Morphisms. +(* From ExtLib Require Import Monad StateMonad. *) +From FreerDPS Require Export Interface Impure. +From monae Require Import preamble hierarchy monad_model. + +From HB Require Import structures. + +#[local] Open Scope signature_scope. +#[local] Open Scope monae_scope. + + +CoInductive semantics (i : interface) : Type := +| mk_semantics (f : forall (α : Type), i α -> α * semantics i) : semantics i. + +Arguments mk_semantics [i] (f). + +(** Thus, a [semantics] does not only compute a result for a primitive, but also + provides a new semantics. This is necessary to model impurity: the same + primitive may or may not return the same result when called several + times. + + As for interfaces, the simpler [semantics] is the operational semantics for + [iempty], the empty interface. *) + +Definition iempty_semantics : semantics iempty := + mk_semantics (fun α (e : iempty α) => match e with end). + +(** We also provide a semantics for the [STORE s] interface: *) + +CoFixpoint store {s} (init : s) : semantics (STORE s) := + mk_semantics (fun α (e : STORE s α) => + match e with + | Get => (init, store init) + | Put next => (tt, store next) + end). + +(** We provide several helper functions to interpret primitives with + semantics. *) + +Definition run_effect {i α} (sem : semantics i) (e : i α) : α * semantics i := + match sem with mk_semantics f => f α e end. + +Definition eval_effect {i α} (sem : semantics i) (e : i α) : α := + fst (run_effect sem e). + +Definition exec_effect {i α} (sem : semantics i) (e : i α) : semantics i := + snd (run_effect sem e). + +Lemma run_effect_equation {i α} (sem : semantics i) (e : i α) + : run_effect sem e = (eval_effect sem e, exec_effect sem e). + +Proof. + unfold eval_effect, exec_effect. + destruct run_effect; reflexivity. +Qed. + +(** Besides, and similarly to interfaces, operational semantics can and should + be composed together. To that end, we provide the [semprod] operator. *) + +CoFixpoint semprod {i j} (sem_i : semantics i) (sem_j : semantics j) + : semantics (i + j) := + mk_semantics (fun _ e => + match e with + | in_left e => + let (x, out) := run_effect sem_i e in + (x, semprod out sem_j) + | in_right e => + let (x, out) := run_effect sem_j e in + (x, semprod sem_i out) + end). + +Declare Scope semantics_scope. +Bind Scope semantics_scope with semantics. +Delimit Scope semantics_scope with semantics. + +Infix "*" := semprod : semantics_scope. + +(** * Interpreting Impure Computations *) + +(** A term of type [impure a] describes an impure computation expected to return + a term of type [a]. Interpreting this term means actually realizing the + computation and producing the result. This requires to provide an + operational semantics for the interfaces used by the computation. + + Some operational semantics may be defined in Gallina by means of the + [semantics] type. In such a case, we provide helper functions to use them in + conjunction with [impure] terms. The terminology follows a logic similar to + the Haskell state monad: + + - [run_impure] interprets an impure computation [p] with an operational + semantics [sem], and returns both the result of [p] and the new + operational semantics to use afterwards. + - [eval_impure] only returns the result of [p]. + - [exec_impure] only returns the new operational semantics. *) + +Notation interp i := (StateMonad.acto (semantics i)). + +Definition interface_to_state {i:interface} : i ~~> interp i := + fun a e => (fun sem => run_effect sem e). + + +Definition to_state {i} {im : impureMonad i}: im ~~> interp i := impure_lift _ interface_to_state. + +Arguments to_state {i α} _ : rename. + +Definition run_impure {i a} {im : impureMonad i} (sem : semantics i) (p : im a) : a * semantics i := + (to_state _ p) sem. + +Definition eval_impure {i a} {im : impureMonad i} (sem : semantics i) (p : im a) : a := + fst (run_impure sem p). + +Definition exec_impure {i a} {im : impureMonad i} (sem : semantics i) (p : im a) : semantics i := + snd (run_impure sem p). + +(** * In-place Primitives Handling *) + + +Fixpoint with_semantics {ix j α} (sem : semantics j) (p : impure (ix + j) α) + : impure ix α := + match p with + | Impure.local x => Impure.local x + | request_then _ (in_right e) f => + let (res, next) := run_effect sem e in + with_semantics next (f res) + | request_then _ (in_left e) f => + request_then e (fun x => with_semantics sem (f x)) + end. + +(** We provide [with_store], a helper function to locally provide a mutable + variable. *) + +Definition with_store {ix s a} (x : s) (p : impure (ix + STORE s) a) + : impure ix a := + with_semantics (store x) p. + +(** Nesting [with_semantics] calls works to some extends. If each + [with_semantics] provides a different interface from the rest of the stack, + then everything behaves as expected. If, for some reason, you end up in a + situation where you provide the exact same interface twice (typically if you + use [with_store]), then the typeclass inferences will favor the deepest one + in the stack. For instance, + +<< +Compute (with_store 0 (with_store 1 get)). +>> + + returns + +<< + = local 1 + : impure ?ix nat +>> *) diff --git a/theories/Tactics.v b/theories/Tactics.v new file mode 100644 index 0000000..f38fd1b --- /dev/null +++ b/theories/Tactics.v @@ -0,0 +1,266 @@ +(* 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/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +(* From ExtLib Require Import Monad. *) +From monae Require Import preamble hierarchy. +From FreerDPS Require Import Init Interface Contract Impure Hoare HoareFacts. + +Ltac destruct_if_when := + let equ_cond := fresh "equ_cond" in + match goal with + | |- context[when (negb ?B) _] => case_eq B; intros equ_cond; cbn + | |- context[when ?B _] => case_eq B; intros equ_cond; cbn + | |- context[if (negb ?B) then _ else _] => case_eq B; intros equ_cond; cbn + | |- context[if ?B then _ else _] => case_eq B; intros equ_cond; cbn + | _ => idtac + end. + +Ltac destruct_if_when_in hyp := + let equ_cond := fresh "equ" in + match type of hyp with + | context[when (negb ?B) _] => case_eq B; + intro equ_cond; + rewrite equ_cond in hyp + | context[when ?B _] => case_eq B; + intro equ_cond; + rewrite equ_cond in hyp + | context[if (negb ?B) then _ else _] => case_eq B; + intro equ_cond; + rewrite equ_cond in hyp + | context[if ?B then _ else _] => case_eq B; + intro equ_cond; + rewrite equ_cond in hyp + | _ => idtac + end. + +Ltac simplify_gens := + repeat match goal with + | H : True |- _ => + clear H + + | H: _ /\ _ |- _ => + destruct H + + | |- context[@proj_p ?ix ?ix (refl_MayProvide ?ix) _ ?e] => + change (@proj_p ix ix (refl_MayProvide ix) _ e) with (Some e); + cbn match; + cbn beta + + | H: context[@proj_p ?ix ?ix (refl_MayProvide ?ix) _ ?e] |- _ => + change (@proj_p ix ix (refl_MayProvide ix) _ e) with (Some e) in H; + cbn match in H; + cbn beta in H + + | |- context[gen_witness_update _ _ _ _] => + unfold gen_witness_update; + repeat (rewrite proj_inj_p_equ || rewrite distinguish) + + | H : context[gen_witness_update _ _ _ _] |- _ => + unfold gen_witness_update in H; + repeat (rewrite proj_inj_p_equ in H || rewrite distinguish in H) + + | |- context[gen_caller_obligation ?c ?ω ?e] => + unfold gen_caller_obligation; + repeat (rewrite proj_inj_p_equ || rewrite distinguish) + + | H : context[gen_caller_obligation ?c ?ω ?e] |- _ => + unfold gen_caller_obligation in H; + repeat (rewrite proj_inj_p_equ in H || rewrite distinguish in H) + + | |- context[gen_callee_obligation ?c ?ω ?e ?x] => + unfold gen_callee_obligation; + repeat (rewrite proj_inj_p_equ || rewrite distinguish) + + | H : context[gen_callee_obligation ?c ?ω ?e ?x] |- _ => + unfold gen_callee_obligation in H; + repeat (rewrite proj_inj_p_equ in H || rewrite distinguish in H) + end. + +#[local] +Ltac prove_impure := + repeat (cbn -[ + to_hoare + gen_caller_obligation + gen_callee_obligation + gen_witness_update + lifter + ] in *; + simplify_gens; + destruct_if_when); + lazymatch goal with + + | |- _ /\ _ => + split; + prove_impure + + | |- forall _ _, _ /\ _ = _ -> _ => + let x := fresh "x" in + let ω' := fresh "ω" in + let o_caller := fresh "o_caller" in + let equ := fresh "equ" in + intros x ω' [o_caller equ]; + repeat rewrite -> equ in *; clear equ; clear ω'; + prove_impure + + | |- pre ?pcond ?ω => + + lazymatch pcond with + | lifter (i:=?ifce) (M:=?m) (interface_to_hoare ?c) (A:=_) ?p => let p := (eval hnf in p) in + lazymatch p with + | request_then ?e ?f => + let o_caller := fresh "o_caller" in + assert (o_caller : gen_caller_obligation c ω e) ; + [ prove_impure | constructor; prove_impure] + | local _ => constructor + | impure_bind (impure_bind ?p ?f) ?g => + rewrite (bindA p f g); + prove_impure + | bind ?p ?f => + apply to_hoare_pre_bind_assoc; [ eauto with freespec + | let x := fresh "x" in + let ω' := fresh "ω" in + let hpost := fresh "hpost" in + intros x ω' hpost; + prove_impure + ] + | _ => eauto with freespec + end + + | to_hoare ?c ?p => let p := (eval hnf in p) in + lazymatch p with + | request_then ?e ?f => + let o_caller := fresh "o_caller" in + assert (o_caller : gen_caller_obligation c ω e) ; + [ prove_impure | constructor; prove_impure] + | local _ => constructor + | impure_bind (impure_bind ?p ?f) ?g => + rewrite (bindA p f g); + prove_impure + | bind ?p ?f => + apply to_hoare_pre_bind_assoc; [ eauto with freespec + | let x := fresh "x" in + let ω' := fresh "ω" in + let hpost := fresh "hpost" in + intros x ω' hpost; + prove_impure + ] + | _ => eauto with freespec + end + | _ => idtac "==>not handled" + end + | |- ?a => + eauto with freespec + + end. + +Tactic Notation "prove" "impure" := prove_impure. +Tactic Notation "prove" "impure" "with" ident(db) := prove_impure; eauto with db. + +Ltac unroll_post run := + repeat (cbn -[ + to_hoare + gen_caller_obligation + gen_callee_obligation + gen_witness_update + ] in *; + simplify_gens; + destruct_if_when_in run); + lazymatch type of run with + + | post (to_hoare ?c ?p) ?ω ?x ?ω' => + let p := (eval hnf in p) in + lazymatch p with + | request_then ?e ?f => + inversion run; ssubst; + clear run; + lazymatch goal with + | next : exists _, post (interface_to_hoare c _ e) _ _ _ /\ _ |- _ => + let ω'' := fresh "ω" in + let o_callee := fresh "o_callee" in + let run := fresh "run" in + destruct next as [ω'' [o_callee run]]; + unroll_post run + | _ => idtac + end + + | local ?x => + inversion run; ssubst; + clear run + + | bind ?p ?f => + apply (bindA c p f) in run; + let run1 := fresh "run" in + let run2 := fresh "run" in + let x := fresh "x" in + let ω := fresh "ω" in + destruct run as [x [ω [run1 run2]]]; + unroll_post run1; unroll_post run2 + + | ?a => idtac + end + + | ?a => idtac + end. + + Ltac cleanvert hyp := inversion hyp; ssubst; move:hyp=>_. + +Ltac easy_simpl hyp := idtac "--simpl"; do ? [cbn -[ + to_hoare + gen_caller_obligation + gen_callee_obligation + gen_witness_update +] in *; simplify_gens; do ? destruct_if_when_in hyp]. + +Ltac run_simpl run := + idtac "run_simpl: " run; + easy_simpl run ; + match type of run with +| post (to_hoare ?c ?p) ?ω ?x ?ω' => + idtac "=> to_hoare" "c: " c " ; p: " p; + let p := (eval hnf in p) in + idtac "=> hnf of p: " p; + match p with + | request_then ?e ?f => + idtac "=> => impure!"; + cleanvert run; + idtac "=> => inverted"; + match goal with + | next : exists _, post (interface_to_hoare c (A:=_) e) _ _ _ /\ _ |- _ => + idtac "=> => => found next: " next; + let ω'' := fresh "ω" in + let o_callee := fresh "o_callee" in + let run := fresh "run" in + case: next =>ω'' [o_callee run]; + idtac "=> => => destructed as : [" ω'' "[" o_callee ", " run"]]"; + run_simpl run; + idtac "<== <== after run" + | _ => idtac "<== branched out exists match" + end + | local ?x => idtac "=> => PURE!"; cleanvert run + | _ => idtac "<== freer out" + end +| post (lifter (i:=?ifce) (M:=?m) (interface_to_hoare ?c) (A:=_) (bind ?f ?g)) _ _ _ => + idtac "=> lifter bind"; + let run1 := fresh "lrun" in + let run2 := fresh "rrun" in + let ω := fresh "ω" in + let x := fresh "x" in + idtac "=> var names : " run1 run2 ω x; + move: run => /(to_hoare_post_bind_assoc c f g); + idtac "=> thpba applied"; + move => [x [ω [run1 run2]]]; + idtac "=> destructed run"; + idtac "=>> run first:"; + run_simpl run1; + idtac "<<= finished first"; + idtac "=>> run second:"; + run_simpl run2; + idtac "<<= finished second" + (* idtac *) + (* destruct run as [x [ω [run1 run2]]]; *) + (* run_simpl run1; run_simpl run2 *) +| ?a => idtac "not post" +end. \ No newline at end of file diff --git a/theories/Typeclasses.v b/theories/Typeclasses.v new file mode 100644 index 0000000..a541bfa --- /dev/null +++ b/theories/Typeclasses.v @@ -0,0 +1,117 @@ +From FreerDPS Require Import Interface. + +Class Provide1 ix i1 `{Provide ix i1}. + +#[global] Hint Resolve Build_Provide1 : typeclass_instances. + +Class Provide2 ix i1 i2 `{Provide ix i1, Provide ix i2}. + +#[global] Hint Resolve Build_Provide2 : typeclass_instances. + +Class Provide3 ix i1 i2 i3 `{Provide ix i1, Provide ix i2, Provide ix i3}. + +#[global] Hint Resolve Build_Provide3 : typeclass_instances. + +Class Provide4 ix i1 i2 i3 i4 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4}. + +#[global] Hint Resolve Build_Provide4 : typeclass_instances. + +Class Provide5 ix i1 i2 i3 i4 i5 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5}. + +#[global] Hint Resolve Build_Provide5 : typeclass_instances. + +Class Provide6 ix i1 i2 i3 i4 i5 i6 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6}. + +#[global] Hint Resolve Build_Provide6 : typeclass_instances. + +Class Provide7 ix i1 i2 i3 i4 i5 i6 i7 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7}. + +#[global] Hint Resolve Build_Provide7 : typeclass_instances. + +Class Provide8 ix i1 i2 i3 i4 i5 i6 i7 i8 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8}. + +#[global] Hint Resolve Build_Provide8 : typeclass_instances. + +Class Provide9 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9}. + +#[global] Hint Resolve Build_Provide9 : typeclass_instances. + +Class Provide10 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10}. + +#[global] Hint Resolve Build_Provide10 : typeclass_instances. + +Class Provide11 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11}. + +#[global] Hint Resolve Build_Provide11 : typeclass_instances. + +Class Provide12 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12}. + +#[global] Hint Resolve Build_Provide12 : typeclass_instances. + +Class Provide13 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13}. + +#[global] Hint Resolve Build_Provide13 : typeclass_instances. + +Class Provide14 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13, Provide ix i14}. + +#[global] Hint Resolve Build_Provide14 : typeclass_instances. + +Class Provide15 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 i15 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13, Provide ix i14, Provide ix i15}. + +#[global] Hint Resolve Build_Provide15 : typeclass_instances. + +Class StrictProvide2 ix i1 i2 `{Provide ix i1, Provide ix i2, ! Distinguish ix i1 i2, ! Distinguish ix i2 i1}. + +#[global] Hint Resolve Build_StrictProvide2 : typeclass_instances. + +Class StrictProvide3 ix i1 i2 i3 `{Provide ix i1, Provide ix i2, Provide ix i3, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2}. + +#[global] Hint Resolve Build_StrictProvide3 : typeclass_instances. + +Class StrictProvide4 ix i1 i2 i3 i4 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3}. + +#[global] Hint Resolve Build_StrictProvide4 : typeclass_instances. + +Class StrictProvide5 ix i1 i2 i3 i4 i5 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4}. + +#[global] Hint Resolve Build_StrictProvide5 : typeclass_instances. + +Class StrictProvide6 ix i1 i2 i3 i4 i5 i6 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5}. + +#[global] Hint Resolve Build_StrictProvide6 : typeclass_instances. + +Class StrictProvide7 ix i1 i2 i3 i4 i5 i6 i7 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6}. + +#[global] Hint Resolve Build_StrictProvide7 : typeclass_instances. + +Class StrictProvide8 ix i1 i2 i3 i4 i5 i6 i7 i8 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7}. + +#[global] Hint Resolve Build_StrictProvide8 : typeclass_instances. + +Class StrictProvide9 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8}. + +#[global] Hint Resolve Build_StrictProvide9 : typeclass_instances. + +Class StrictProvide10 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9}. + +#[global] Hint Resolve Build_StrictProvide10 : typeclass_instances. + +Class StrictProvide11 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i1 i11, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i2 i11, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i3 i11, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i4 i11, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i5 i11, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i6 i11, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i7 i11, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i8 i11, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i9 i11, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9, ! Distinguish ix i10 i11, ! Distinguish ix i11 i1, ! Distinguish ix i11 i2, ! Distinguish ix i11 i3, ! Distinguish ix i11 i4, ! Distinguish ix i11 i5, ! Distinguish ix i11 i6, ! Distinguish ix i11 i7, ! Distinguish ix i11 i8, ! Distinguish ix i11 i9, ! Distinguish ix i11 i10}. + +#[global] Hint Resolve Build_StrictProvide11 : typeclass_instances. + +Class StrictProvide12 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i1 i11, ! Distinguish ix i1 i12, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i2 i11, ! Distinguish ix i2 i12, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i3 i11, ! Distinguish ix i3 i12, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i4 i11, ! Distinguish ix i4 i12, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i5 i11, ! Distinguish ix i5 i12, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i6 i11, ! Distinguish ix i6 i12, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i7 i11, ! Distinguish ix i7 i12, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i8 i11, ! Distinguish ix i8 i12, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i9 i11, ! Distinguish ix i9 i12, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9, ! Distinguish ix i10 i11, ! Distinguish ix i10 i12, ! Distinguish ix i11 i1, ! Distinguish ix i11 i2, ! Distinguish ix i11 i3, ! Distinguish ix i11 i4, ! Distinguish ix i11 i5, ! Distinguish ix i11 i6, ! Distinguish ix i11 i7, ! Distinguish ix i11 i8, ! Distinguish ix i11 i9, ! Distinguish ix i11 i10, ! Distinguish ix i11 i12, ! Distinguish ix i12 i1, ! Distinguish ix i12 i2, ! Distinguish ix i12 i3, ! Distinguish ix i12 i4, ! Distinguish ix i12 i5, ! Distinguish ix i12 i6, ! Distinguish ix i12 i7, ! Distinguish ix i12 i8, ! Distinguish ix i12 i9, ! Distinguish ix i12 i10, ! Distinguish ix i12 i11}. + +#[global] Hint Resolve Build_StrictProvide12 : typeclass_instances. + +Class StrictProvide13 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i1 i11, ! Distinguish ix i1 i12, ! Distinguish ix i1 i13, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i2 i11, ! Distinguish ix i2 i12, ! Distinguish ix i2 i13, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i3 i11, ! Distinguish ix i3 i12, ! Distinguish ix i3 i13, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i4 i11, ! Distinguish ix i4 i12, ! Distinguish ix i4 i13, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i5 i11, ! Distinguish ix i5 i12, ! Distinguish ix i5 i13, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i6 i11, ! Distinguish ix i6 i12, ! Distinguish ix i6 i13, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i7 i11, ! Distinguish ix i7 i12, ! Distinguish ix i7 i13, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i8 i11, ! Distinguish ix i8 i12, ! Distinguish ix i8 i13, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i9 i11, ! Distinguish ix i9 i12, ! Distinguish ix i9 i13, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9, ! Distinguish ix i10 i11, ! Distinguish ix i10 i12, ! Distinguish ix i10 i13, ! Distinguish ix i11 i1, ! Distinguish ix i11 i2, ! Distinguish ix i11 i3, ! Distinguish ix i11 i4, ! Distinguish ix i11 i5, ! Distinguish ix i11 i6, ! Distinguish ix i11 i7, ! Distinguish ix i11 i8, ! Distinguish ix i11 i9, ! Distinguish ix i11 i10, ! Distinguish ix i11 i12, ! Distinguish ix i11 i13, ! Distinguish ix i12 i1, ! Distinguish ix i12 i2, ! Distinguish ix i12 i3, ! Distinguish ix i12 i4, ! Distinguish ix i12 i5, ! Distinguish ix i12 i6, ! Distinguish ix i12 i7, ! Distinguish ix i12 i8, ! Distinguish ix i12 i9, ! Distinguish ix i12 i10, ! Distinguish ix i12 i11, ! Distinguish ix i12 i13, ! Distinguish ix i13 i1, ! Distinguish ix i13 i2, ! Distinguish ix i13 i3, ! Distinguish ix i13 i4, ! Distinguish ix i13 i5, ! Distinguish ix i13 i6, ! Distinguish ix i13 i7, ! Distinguish ix i13 i8, ! Distinguish ix i13 i9, ! Distinguish ix i13 i10, ! Distinguish ix i13 i11, ! Distinguish ix i13 i12}. + +#[global] Hint Resolve Build_StrictProvide13 : typeclass_instances. + +Class StrictProvide14 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13, Provide ix i14, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i1 i11, ! Distinguish ix i1 i12, ! Distinguish ix i1 i13, ! Distinguish ix i1 i14, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i2 i11, ! Distinguish ix i2 i12, ! Distinguish ix i2 i13, ! Distinguish ix i2 i14, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i3 i11, ! Distinguish ix i3 i12, ! Distinguish ix i3 i13, ! Distinguish ix i3 i14, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i4 i11, ! Distinguish ix i4 i12, ! Distinguish ix i4 i13, ! Distinguish ix i4 i14, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i5 i11, ! Distinguish ix i5 i12, ! Distinguish ix i5 i13, ! Distinguish ix i5 i14, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i6 i11, ! Distinguish ix i6 i12, ! Distinguish ix i6 i13, ! Distinguish ix i6 i14, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i7 i11, ! Distinguish ix i7 i12, ! Distinguish ix i7 i13, ! Distinguish ix i7 i14, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i8 i11, ! Distinguish ix i8 i12, ! Distinguish ix i8 i13, ! Distinguish ix i8 i14, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i9 i11, ! Distinguish ix i9 i12, ! Distinguish ix i9 i13, ! Distinguish ix i9 i14, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9, ! Distinguish ix i10 i11, ! Distinguish ix i10 i12, ! Distinguish ix i10 i13, ! Distinguish ix i10 i14, ! Distinguish ix i11 i1, ! Distinguish ix i11 i2, ! Distinguish ix i11 i3, ! Distinguish ix i11 i4, ! Distinguish ix i11 i5, ! Distinguish ix i11 i6, ! Distinguish ix i11 i7, ! Distinguish ix i11 i8, ! Distinguish ix i11 i9, ! Distinguish ix i11 i10, ! Distinguish ix i11 i12, ! Distinguish ix i11 i13, ! Distinguish ix i11 i14, ! Distinguish ix i12 i1, ! Distinguish ix i12 i2, ! Distinguish ix i12 i3, ! Distinguish ix i12 i4, ! Distinguish ix i12 i5, ! Distinguish ix i12 i6, ! Distinguish ix i12 i7, ! Distinguish ix i12 i8, ! Distinguish ix i12 i9, ! Distinguish ix i12 i10, ! Distinguish ix i12 i11, ! Distinguish ix i12 i13, ! Distinguish ix i12 i14, ! Distinguish ix i13 i1, ! Distinguish ix i13 i2, ! Distinguish ix i13 i3, ! Distinguish ix i13 i4, ! Distinguish ix i13 i5, ! Distinguish ix i13 i6, ! Distinguish ix i13 i7, ! Distinguish ix i13 i8, ! Distinguish ix i13 i9, ! Distinguish ix i13 i10, ! Distinguish ix i13 i11, ! Distinguish ix i13 i12, ! Distinguish ix i13 i14, ! Distinguish ix i14 i1, ! Distinguish ix i14 i2, ! Distinguish ix i14 i3, ! Distinguish ix i14 i4, ! Distinguish ix i14 i5, ! Distinguish ix i14 i6, ! Distinguish ix i14 i7, ! Distinguish ix i14 i8, ! Distinguish ix i14 i9, ! Distinguish ix i14 i10, ! Distinguish ix i14 i11, ! Distinguish ix i14 i12, ! Distinguish ix i14 i13}. + +#[global] Hint Resolve Build_StrictProvide14 : typeclass_instances. + +Class StrictProvide15 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 i15 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13, Provide ix i14, Provide ix i15, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i1 i11, ! Distinguish ix i1 i12, ! Distinguish ix i1 i13, ! Distinguish ix i1 i14, ! Distinguish ix i1 i15, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i2 i11, ! Distinguish ix i2 i12, ! Distinguish ix i2 i13, ! Distinguish ix i2 i14, ! Distinguish ix i2 i15, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i3 i11, ! Distinguish ix i3 i12, ! Distinguish ix i3 i13, ! Distinguish ix i3 i14, ! Distinguish ix i3 i15, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i4 i11, ! Distinguish ix i4 i12, ! Distinguish ix i4 i13, ! Distinguish ix i4 i14, ! Distinguish ix i4 i15, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i5 i11, ! Distinguish ix i5 i12, ! Distinguish ix i5 i13, ! Distinguish ix i5 i14, ! Distinguish ix i5 i15, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i6 i11, ! Distinguish ix i6 i12, ! Distinguish ix i6 i13, ! Distinguish ix i6 i14, ! Distinguish ix i6 i15, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i7 i11, ! Distinguish ix i7 i12, ! Distinguish ix i7 i13, ! Distinguish ix i7 i14, ! Distinguish ix i7 i15, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i8 i11, ! Distinguish ix i8 i12, ! Distinguish ix i8 i13, ! Distinguish ix i8 i14, ! Distinguish ix i8 i15, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i9 i11, ! Distinguish ix i9 i12, ! Distinguish ix i9 i13, ! Distinguish ix i9 i14, ! Distinguish ix i9 i15, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9, ! Distinguish ix i10 i11, ! Distinguish ix i10 i12, ! Distinguish ix i10 i13, ! Distinguish ix i10 i14, ! Distinguish ix i10 i15, ! Distinguish ix i11 i1, ! Distinguish ix i11 i2, ! Distinguish ix i11 i3, ! Distinguish ix i11 i4, ! Distinguish ix i11 i5, ! Distinguish ix i11 i6, ! Distinguish ix i11 i7, ! Distinguish ix i11 i8, ! Distinguish ix i11 i9, ! Distinguish ix i11 i10, ! Distinguish ix i11 i12, ! Distinguish ix i11 i13, ! Distinguish ix i11 i14, ! Distinguish ix i11 i15, ! Distinguish ix i12 i1, ! Distinguish ix i12 i2, ! Distinguish ix i12 i3, ! Distinguish ix i12 i4, ! Distinguish ix i12 i5, ! Distinguish ix i12 i6, ! Distinguish ix i12 i7, ! Distinguish ix i12 i8, ! Distinguish ix i12 i9, ! Distinguish ix i12 i10, ! Distinguish ix i12 i11, ! Distinguish ix i12 i13, ! Distinguish ix i12 i14, ! Distinguish ix i12 i15, ! Distinguish ix i13 i1, ! Distinguish ix i13 i2, ! Distinguish ix i13 i3, ! Distinguish ix i13 i4, ! Distinguish ix i13 i5, ! Distinguish ix i13 i6, ! Distinguish ix i13 i7, ! Distinguish ix i13 i8, ! Distinguish ix i13 i9, ! Distinguish ix i13 i10, ! Distinguish ix i13 i11, ! Distinguish ix i13 i12, ! Distinguish ix i13 i14, ! Distinguish ix i13 i15, ! Distinguish ix i14 i1, ! Distinguish ix i14 i2, ! Distinguish ix i14 i3, ! Distinguish ix i14 i4, ! Distinguish ix i14 i5, ! Distinguish ix i14 i6, ! Distinguish ix i14 i7, ! Distinguish ix i14 i8, ! Distinguish ix i14 i9, ! Distinguish ix i14 i10, ! Distinguish ix i14 i11, ! Distinguish ix i14 i12, ! Distinguish ix i14 i13, ! Distinguish ix i14 i15, ! Distinguish ix i15 i1, ! Distinguish ix i15 i2, ! Distinguish ix i15 i3, ! Distinguish ix i15 i4, ! Distinguish ix i15 i5, ! Distinguish ix i15 i6, ! Distinguish ix i15 i7, ! Distinguish ix i15 i8, ! Distinguish ix i15 i9, ! Distinguish ix i15 i10, ! Distinguish ix i15 i11, ! Distinguish ix i15 i12, ! Distinguish ix i15 i13, ! Distinguish ix i15 i14}. + +#[global] Hint Resolve Build_StrictProvide15 : typeclass_instances. \ No newline at end of file diff --git a/theories/dune b/theories/dune new file mode 100644 index 0000000..3f76afd --- /dev/null +++ b/theories/dune @@ -0,0 +1,8 @@ +(coq.theory + (name FreerDPS) + (package freerdps) + (synopsis "A FreeSpec rewrite to bring the power of equational reasoning and probabilities.") + (theories Stdlib infotheo monae mathcomp elpi_examples elpi_elpi elpi Ltac2 Equations HB) +) + +(include_subdirs qualified) From c9f076282d6224c01f4607bf1e82ba326656bbd9 Mon Sep 17 00:00:00 2001 From: awshanhussain Date: Tue, 9 Jun 2026 16:02:36 +0200 Subject: [PATCH 2/8] changes on FlipMonad and FreerFlip for infotheo 0.9.7 (#2) * changement sur FrlipMonad et FreerFlip pour infotheo 0.9.7 * update dune project * changes to correct the syntax of the code , changed the version of infotheo in the README --------- Co-authored-by: awshan --- README.md | 2 +- dune-project | 4 ++-- freer_playground/theories/FlipMonad.v | 25 ++++++++++++----------- freer_playground/theories/lib/FreerFlip.v | 8 +++++--- 4 files changed, 21 insertions(+), 18 deletions(-) diff --git a/README.md b/README.md index 21867fe..0ac5a3d 100644 --- a/README.md +++ b/README.md @@ -35,7 +35,7 @@ In case monae / infotheo can not be installed through opam, you can clone them f 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) +- infotheo : 0.9.7 You just need to clone the repositories and run : 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..c98c288 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,17 @@ 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 +35,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 +53,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 +94,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 +165,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..6735df5 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 From 16bc36a001af618bd22525fcb49b1c4886204ff0 Mon Sep 17 00:00:00 2001 From: awshan Date: Wed, 13 May 2026 15:59:18 +0200 Subject: [PATCH 3/8] changement sur FrlipMonad et FreerFlip pour infotheo 0.9.7 --- freer_playground/theories/FlipMonad.v | 5 ++--- freer_playground/theories/lib/FreerFlip.v | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/freer_playground/theories/FlipMonad.v b/freer_playground/theories/FlipMonad.v index c98c288..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. -From mathcomp Require Import ssreflect ssrnum ssrbool ssralg reals interval_inference. +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. @@ -17,7 +17,6 @@ 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 ; diff --git a/freer_playground/theories/lib/FreerFlip.v b/freer_playground/theories/lib/FreerFlip.v index 6735df5..31dad9a 100644 --- a/freer_playground/theories/lib/FreerFlip.v +++ b/freer_playground/theories/lib/FreerFlip.v @@ -98,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. From 4ac073d3b982d55ded30ee61a54f8365e9173c16 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 9 Jul 2026 15:31:59 +0900 Subject: [PATCH 4/8] Makefile (#3) Add a dedicated makefile and deport it code's makefile generation. --- .gitignore | 3 +-- Makefile | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 2 deletions(-) create mode 100644 Makefile diff --git a/.gitignore b/.gitignore index 77882f9..fa76ba0 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,3 @@ -**/Makefile **/Makefile.conf **/.CoqMakefile.d **/.Makefile.d @@ -8,4 +7,4 @@ **/*.vos **/.*.aux _opam -_build \ No newline at end of file +_build 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 From 2e9ba6b5ec5aacb4dd61659da2f9cd6cb44225e7 Mon Sep 17 00:00:00 2001 From: forrazh <56563878+forrazh@users.noreply.github.com> Date: Thu, 9 Jul 2026 09:05:24 +0200 Subject: [PATCH 5/8] Update README with project details and installation instructions --- README.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 0ac5a3d..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,13 +28,14 @@ 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 +- 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). From 1eb5a2b34f93b28b67bbecee38ad37e1b90d314c Mon Sep 17 00:00:00 2001 From: forrazh <56563878+forrazh@users.noreply.github.com> Date: Thu, 9 Jul 2026 09:16:33 +0200 Subject: [PATCH 6/8] Update .gitignore (#6) update .gitignore --------- Co-authored-by: Hugo Forraz --- .gitignore | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index fa76ba0..e40af63 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,7 @@ -**/Makefile.conf +**/Makefile.rocq.conf **/.CoqMakefile.d -**/.Makefile.d +**/.Makefile.rocq.d +**/.Makefile.rocq **/*.glob **/*.vo **/*.vok @@ -8,3 +9,6 @@ **/.*.aux _opam _build +freer_playground/.Makefile.d +freer_playground/Makefile +freer_playground/Makefile.conf \ No newline at end of file From 3303f2377b524313ac7e14f4c19f0a3de5258643 Mon Sep 17 00:00:00 2001 From: Hugo Forraz Date: Mon, 13 Jul 2026 04:00:58 +0200 Subject: [PATCH 7/8] fix .gitignore --- .gitignore | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index e40af63..5cd85bc 100644 --- a/.gitignore +++ b/.gitignore @@ -1,7 +1,6 @@ +**/Makefile.rocq **/Makefile.rocq.conf -**/.CoqMakefile.d **/.Makefile.rocq.d -**/.Makefile.rocq **/*.glob **/*.vo **/*.vok From 3c22f0bd15ce0c15482a7dd0febd37fac89d9174 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Mon, 13 Jul 2026 14:46:19 +0900 Subject: [PATCH 8/8] Update Hoare.v (linting / usage of logical rules) (#9) Linting of the Hoare file + simplification of the proof using logical rules. Added lemmas could be added to mathcomp, hence have been put in a `mathcomp_extra` file. --------- Co-authored-by: Hugo Forraz --- _CoqProject | 1 + theories/Hoare.v | 152 +++++++++++++++++--------------------- theories/mathcomp_extra.v | 86 +++++++++++++++++++++ 3 files changed, 156 insertions(+), 83 deletions(-) create mode 100644 theories/mathcomp_extra.v 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/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.