Upstream everything to base repo

.gitignore

@@ -1,11 +1,13 @@
-**/Makefile
-**/Makefile.conf
-**/.CoqMakefile.d
-**/.Makefile.d
+**/Makefile.rocq
+**/Makefile.rocq.conf
+**/.Makefile.rocq.d
 **/*.glob
 **/*.vo
 **/*.vok
 **/*.vos
 **/.*.aux
 _opam
-_build
+_build
+freer_playground/.Makefile.d
+freer_playground/Makefile
+freer_playground/Makefile.conf

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

README.md

@@ -4,14 +4,14 @@ FreerDPS stands for : **Freer** *E*quational *R*easoning for **D**istributed and
 
 # Code structure
 
-As of now, the code base is mainly a rewrite of [FreeSpec](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect.
+As of now, the code base is mainly a rewrite/extension of [FreeSpec Core](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect.
 
 # Install
 
 ## Libraries
 
 You need to install the following libraries for the project to work :
-- coq 9.0 (it will use rocq as soon as monae makes the move)
+- Rocq 9.0
 - monae
 - infotheo
 - mathcomp
@@ -28,14 +28,15 @@ opam pin add coq 9.0.0
 eval $(opam env)
 
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq-hierarchy-builder coq-mathcomp-ssreflect coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable coq-mathcomp-classical 
+opam install coq-hierarchy-builder coq-mathcomp-ssreflect coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable coq-mathcomp-classical
+opam install coq-monae coq-infotheo
 ```
 
 In case monae / infotheo can not be installed through opam, you can clone them from github and fix their versions.
 
 Versions known to work :
-- monae : dev
-- infotheo : 0.9.6 => [I have a local fork for now](https://github.com/forrazh/infotheo/tree/fix/0.9.6)
+- monae : 0.9.2
+- infotheo : 0.9.7
 
 You just need to clone the repositories and run : 
 
@@ -49,11 +50,10 @@ inside the repository.
 Once everything is installed, you can run the following commands :
 
 ```sh
-coq_makefile -f _CoqProject -o Makefile 
 make
 ```
 
 
 # Publications 
 
-This work has been submitted to COMPAS and is under reviewing. 
+This work has been submitted and accepted to [COMPAS26](https://2026.compas-conference.fr/) (no paper available online). 

_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

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.
 

freer_playground/theories/FlipMonad.v

@@ -1,7 +1,7 @@
 Ltac typeof X := type of X.
 
-From Stdlib Require Import ssrmatching Reals.
-From mathcomp Require Import ssreflect ssrbool ssralg reals. 
+From Stdlib Require Import ssrmatching .
+From mathcomp Require Import ssreflect ssrnum ssrbool ssralg  reals interval_inference. 
 From infotheo Require Import realType_ext.
 
 From HB Require Import structures.
@@ -14,16 +14,16 @@ Local Open Scope proba_scope.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
-
+Local Open Scope ring_scope.
 Local Open Scope reals_ext_scope.
-
+Local Open Scope convex_scope.
 (* 1st step : FlipMonad *)
 HB.mixin Record isMonadFlip {R : realType} (M : UU0 -> UU0) of Monad M := {
     flip : forall (p : {prob R}), M bool ;
     (* identity axiom *)
-    flip1 : flip 1%:pr = Ret true  ;
+    flip1 : flip 1%:i01 = Ret true  ;
     (* skewed commutativity *)
-    flipNeg : forall (p: {prob R}), flip p = flip (Prob.p p).~%:pr >>= (fun x => Ret (~~x)) ;
+    flipNeg : forall (p: {prob R}), flip p = flip p%:num.~%:i01 >>= (fun x => Ret (~~x)) ;
     (* idempotence *)
     flipmm : forall (A:UU0) p (a:M A), flip p >> a = a ;
     (* quasi associativity *)
@@ -34,7 +34,7 @@ HB.mixin Record isMonadFlip {R : realType} (M : UU0 -> UU0) of Monad M := {
     (* Prob.p p = (Prob.p r * Prob.p s)%R :> R -> ((Prob.p s).~ = (Prob.p p).~ * (Prob.p q).~)%R -> *)
 flip p >>= (fun x => if x then a else flip q >>= (fun x0 => if x0 then b else c)) = 
 flip [s_of p, q] >>= 
-  (fun x => if x then flip [r_of p, q] >>= (fun x0 => if x0 then a else b) else c) ;  
+  (fun x => if x then flip [r_of p, q] >>= (fun x0 => if x0 then a else b) else c) ;
 }.
 
 #[short(type=flipMonad)]
@@ -52,11 +52,11 @@ Module FlipLib.
 
 
 (*** identity laws ***)
-Let flip1 : flip_c 1%:pr = Ret true.
+Let flip1 : flip_c 1%:i01 = Ret true.
 Proof. exact: choice1. Qed.
 
 (*** negation law ***)
-Let flipNeg : forall p, flip_c p =  (flip_c ((Prob.p p).~ %:pr)) >>= (fun x => Ret (~~ x)).
+Let flipNeg : forall p, flip_c p =  (flip_c (p%:num.~ %:i01)) >>= (fun x => Ret (~~ x)).
 Proof.
   by move=>p; rewrite /flip_c/bcoin-choiceC choice_bindDl!bindretf.
 Qed.
@@ -93,13 +93,13 @@ Let choicef (p : {prob R}) (A:UU0) (a b : M A) : M A := flip p >>= (fun x => if
 
 
 (*** identity laws ***)
-Let choice1 : forall (A:UU0) (a b : M A), choicef 1%:pr a b =  a.
+Let choice1 : forall (A:UU0) (a b : M A), choicef 1%:i01 a b =  a.
 Proof.
   move=>A a b/=. by rewrite /choicef flip1 bindretf.
 Qed.  
 
 (*** negation law ***)
-Let choiceC : forall (A : UU0) (p:{prob R}) (a b : M A), choicef p a b = choicef ((Prob.p p).~ %:pr) b a.
+Let choiceC : forall (A : UU0) (p:{prob R}) (a b : M A), choicef p a b = choicef (p%:num.~ %:i01) b a.
 Proof.
   move=> A p a b.
   rewrite /choicef flipNeg bindA. 
@@ -164,13 +164,13 @@ Notation pr := (probMonad R).
 Definition cflip (p : {prob R}) := @bcoin R flipacto p.
 
 (*** identity laws ***)
-Let flip1 : @cflip 1%:pr = ret R bool true.
+Let flip1 : @cflip 1%:i01 = ret R bool true.
 Proof. exact: choice1. Qed.
 
 Ltac rw_choicebind_dl:=rewrite /cflip choice_bindDl!bindretf/=.
 
 (*** negation law ***)
-Let flipNeg : forall p, cflip p = (cflip ((Prob.p p).~ %:pr) >>= (fun x => ret R bool (~~ x))).
+Let flipNeg : forall p, cflip p = (cflip (p%:num.~ %:i01) >>= (fun x => ret R bool (~~ x))).
 Proof. 
   move=>p. 
   rw_choicebind_dl;

freer_playground/theories/lib/FreerFlip.v

@@ -1,5 +1,5 @@
 From Stdlib Require Import ssrmatching Reals JMeq Relations Morphisms Eqdep.
-From mathcomp Require Import ssreflect ssrbool ssrnum ssralg reals. 
+From mathcomp Require Import ssreflect ssrbool ssrnum ssralg reals interval_inference. 
 From infotheo Require Import realType_ext.
 From HB Require Import structures.
 From monae Require Import preamble hierarchy monad_lib.
@@ -11,6 +11,8 @@ Local Open Scope monae_scope.
 Local Open Scope proba_scope.
 Local Open Scope reals_ext_scope.
 Local Open Scope freer_flip_scope.
+Local Open Scope ring_scope.
+Local Open Scope convex_scope.
 
 Reserved Notation "x <|| p ||> y" (at level 40, left associativity, y at next level).
 Reserved Notation "a === b" (at level 90).
@@ -51,8 +53,8 @@ Notation "x <|| p ||> y" :=
 
 (* 5th step : Flip equiv laws *)
 Inductive flip_rel :forall `[X : UU0] (m1 m2 : M X), Prop := 
-| rflip1 : flip_rel (flipf 1%:pr) (Ret true)
-| rflipNeg : forall p, flip_rel (flipf p) ((flipf (Prob.p p).~%:pr) >>= (fun x => Ret (~~ x)))
+| rflip1 : flip_rel (flipf 1%:i01) (Ret true)
+| rflipNeg : forall p, flip_rel (flipf p) ((flipf p%:num.~%:i01) >>= (fun x => Ret (~~ x)))
 | rflipmm : forall (A:UU0) p (a: (M A)), flip_rel (flipf p >> a) a 
     (* quasi associativity *)
 | rflipA : forall (T:UU0) (p q r s : {prob R}) (a b c : M T),  flip_rel
@@ -96,7 +98,7 @@ Proof.
   all: rewrite !denote_trigger/denote_flip_effect.
   - exact/fA0. 
   - exact/flipmm.
-  - under eq_bind do rewrite denote_ret; exact/flipNeg.
+  - under eq_bind do rewrite denote_ret. exact/flipNeg.
   - rewrite denote_ret; exact/flip1.
 Qed.