unary/binary judgements defined directly on raw code

theories/Crypt/semantics/binary.v

@@ -87,20 +87,17 @@ End BindCoupling.
 Section Def.
   #[local] Open Scope fset.
   #[local] Open Scope fset_scope.
-  Context (Loc : {fset Location}).
-  Context (import : Interface).
 
   (* Local shorter names for code and semantics *)
-  Let C := code Loc import.
+  Let C := raw_code.
   Let M := (Def.stsubdistr heap_choiceType).
 
   Definition stsubdistr_rel [A1 A2 : choiceType] : M A1 -> M A2 -> Type :=
     fun d1 d2 => forall map1 map2, { d |  d ~[ d1 map1 , d2 map2 ] }.
 
-  (** Taking an interpretation of the imported operation as assumption *)
-  Context (import_eval : forall o, o \in import -> src o -> M (tgt o)).
+  Context (eval_op : forall o, src o -> M (tgt o)).
 
-  Let eval [A] := eval import import_eval (A:=A).
+  Let eval [A] := eval eval_op (A:=A).
 
   Definition prerelation := rel heap.
   Definition postrelation A1 A2 := (A1 * heap) -> pred (A2 * heap).
@@ -113,11 +110,10 @@ Section Def.
                  exists d, d ~[eval c1 map1, eval c2 map2] /\
                       forall p1 p2, d (p1,p2) <> 0%R -> post p1 p2.
 
-  Open Scope package_scope.
 
   (* Bindings in the pre/postcondition looks annoying here *)
   Notation "⊨ ⦃ pre ⦄ c1 ≈ c2 ⦃ post ⦄" :=
-    (binary_judgement pre {code c1} {code c2} post) : Rules_scope.
+    (binary_judgement pre c1 c2 post) : Rules_scope.
   Open Scope Rules_scope.
 
   (** Ret rule *)

theories/Crypt/semantics/unary.v

@@ -40,15 +40,6 @@ Proof.
   f_equal. rewrite fg. reflexivity.
 Qed.
 
-(* Lemma dlet_restr [A B : choiceType] (m : {distr A/R}) *)
-(*       (f : A -> {distr B /R}) : *)
-(*   \dlet_(x <- m) f x = \dlet_(x <- m) drestr [pred _ | m x != 0%R] (f x). *)
-(* Proof. *)
-(*   apply: distr_ext=> z; rewrite 2!dletE. *)
-(*   apply: eq_psum=> a; case E: (m a == 0)%R=> /=; last by rewrite drestrE. *)
-(*   move: E=> /eqP ->; by rewrite 2!GRing.mul0r. *)
-(* Qed. *)
-
 Lemma eq_dlet_partial [A B : choiceType] :
   ∀ (m : {distr A/R}) (f g : A -> {distr B /R}),
     (∀ x, m x ≠ 0%R → f x = g x) →
@@ -101,6 +92,8 @@ Section Def.
      model for single probabilistic programs with state space S *)
   Definition stsubdistr (A : choiceType) := S → {distr (A * S) / R}.
 
+  Definition stsubnull (A : choiceType) : stsubdistr A := fun _ => dnull.
+
   Definition ret [A : choiceType] (a : A) : stsubdistr A :=
     λ s, dunit (a,s).
 
@@ -148,28 +141,12 @@ Section Def.
     exists p₀. assumption.
   Qed.
 
-  Definition bind_restr [A B : choiceType]
-    (m : stsubdistr A) (P : pred A) (f : ∀ (a : A), P a → stsubdistr B) :
-    stsubdistr B :=
-    let f' (a : A) :=
-      bool_depelim (stsubdistr B) (P a) (λ h, f a h) (λ _ _, dnull)
-    in
-    Def.bind m f'.
-
-  Lemma bind_restr_not_null [A B : choiceType] :
-    ∀ (m : stsubdistr A) (P : pred A) (f : ∀ (a : A), P a → stsubdistr B)
-      (hP : ∀ map p, m map p ≠ 0%R → P p.1) map p,
-      bind_restr m P f map p ≠ 0%R →
-      ∃ p₀, { hm : m map p₀ ≠ 0%R | f p₀.1 (hP _ _ hm) p₀.2 p ≠ 0%R }.
-  Proof.
-    intros m P f hP map p.
-    move => /bind_not_null [p₀ [hm₀ hf₀]].
-    exists p₀, hm₀.
-    revert hf₀. rewrite bool_depelim_true.
-    1:{ eapply hP. eassumption. }
-    intro hb. rewrite (bool_irrelevance (hP _ _ _) hb). auto.
-  Qed.
+  Lemma bind_ext [A B : choiceType] (m : stsubdistr A) (f g : A -> stsubdistr B) :
+    f =1 g -> bind m f = bind m g.
+  Proof. move=> fg; f_equal; extensionality x; apply: fg. Qed.
 
+
+  (* Actually unused for now... *)
   Section Order.
 
     Context [A : choiceType].
@@ -249,32 +226,18 @@ End Def.
 
 (** Semantic evaluation of code and commands *)
 Section Evaluation.
+  #[local]
+  Notation M := (Def.stsubdistr heap_choiceType).
 
-  #[local] Open Scope fset.
-  #[local] Open Scope fset_scope.
-
-  Context (Loc : {fset Location}).
-  Context (import : Interface).
-
-  (* Local shorter names for code and semantics *)
-  Let C := code Loc import.
-  Let M := Def.stsubdistr heap_choiceType.
-
-  (** Taking an interpretation of the imported operation as assumption *)
-  Context (import_eval : ∀ o, o \in import → src o → M (tgt o)).
-
-  (* Multiple attempts for evaluation. In the end it looks simpler
-     defining evaluation on raw_code, and providing the adequate
-     rules/hoare triples only on valid code.
-   *)
+  (** Assume an interpretation of operations *)
+  Context (eval_op : ∀ o, src o → M (tgt o)).
 
   Definition eval [A : choiceType] : raw_code A → M A.
   Proof.
     elim.
     - apply: Def.ret.
     - intros o x k ih.
-      apply: (bool_depelim _ (o \in import) _ (λ _ _, dnull)) => oval.
-      exact (Def.bind (import_eval o oval x) ih).
+      exact (Def.bind (eval_op o x) ih).
     - intros l k ih.
       exact (λ map, let v := get_heap map l in ih v map).
     - intros l v k ih.
@@ -283,58 +246,25 @@ Section Evaluation.
       exact (λ map, \dlet_(x <- sampleX) ih x map).
   Defined.
 
-  (* Definition eval [A : choiceType] : C A -> M A. *)
-  (* Proof. *)
-  (*   move=> []; elim. *)
-  (*   - move=> a _ ; exact (ret _ a). *)
-  (*   - move=> o x k ih /inversion_valid_opr [oval kval]. *)
-  (*     exact (bind _ (import_eval o oval x) (fun v => ih v (kval v))). *)
-  (*   - move=> l k ih /inversion_valid_getr [lval kval]. *)
-  (*     exact (bind _ (fun map => dunit (get_heap map l, map)) *)
-  (*                 (fun v => ih v (kval v))). *)
-  (*   - move=> l v k ih /inversion_valid_putr[lval kval]. *)
-  (*     exact (bind _ (fun map => dunit (tt, set_heap map l v)) (fun=> ih kval)). *)
-  (*   - move=> [X sampleX] ++/inversion_valid_sampler. *)
-  (*     rewrite /Arit=> /=k ih kval. *)
-  (*     exact (bind _ (fun s => \dlet_(x <- sampleX) dunit (x, s)) (fun x => ih x (kval x))). *)
-  (* Defined. *)
-
-  (* Definition eval [A : choiceType] : C A -> M A. *)
-  (* Proof. *)
-  (*   move=> []; elim. *)
-  (*   - move=> a _ ; exact (Def.ret a). *)
-  (*   - move=> o x k ih /inversion_valid_opr [oval kval]. *)
-  (*     exact (Def.bind (import_eval o oval x) (fun v => ih v (kval v))). *)
-  (*   - move=> l k ih /inversion_valid_getr [lval kval]. *)
-  (*     exact (fun map => let v := get_heap map l in ih v (kval v) map). *)
-  (*   - move=> l v k ih /inversion_valid_putr[lval kval]. *)
-  (*     exact (fun map => ih kval (set_heap map l v)). *)
-  (*   - move=> [X sampleX] ++/inversion_valid_sampler. *)
-  (*     rewrite /Arit=> /=k ih kval. *)
-  (*     exact (fun map => \dlet_(x <- sampleX) ih x (kval x) map). *)
-  (* Defined. *)
 
   (** Hoare triples *)
 
   Definition precondition := pred heap.
   Definition postcondition A := pred (A * heap).
 
-  Definition unary_judgement [A : choiceType] (pre : precondition) (c : C A) (post : postcondition A) : Prop :=
+  Definition unary_judgement [A : choiceType] (pre : precondition) (c : raw_code A) (post : postcondition A) : Prop :=
     forall map, pre map -> forall p, (eval c map p <> 0)%R -> post p.
 
   Declare Scope Rules_scope.
 
-  (* @théo Is there a binding key for the package_scope ?*)
-  Open Scope package_scope.
-
   (* Is there a way to have a version with and without binder for the result in
   parallel ? *)
   (* Notation "⊨ ⦃ pre ⦄ c ⦃ post ⦄" := *)
   (*   (unary_judgement pre {code c} (post)) *)
   (*     : Rules_scope. *)
 
   Notation "⊨ ⦃ pre ⦄ c ⦃ p , post ⦄" :=
-    (unary_judgement pre {code c} (fun p => post))
+    (unary_judgement pre c (fun p => post))
       (p pattern) : Rules_scope.
   Open Scope Rules_scope.
 
@@ -358,26 +288,21 @@ Section Evaluation.
     [pred pf | `[< exists p, postm p ==> postf p.1 pf >]].
 
   (* the "difficult" part of the effect observation: commutation with bind *)
-  Lemma eval_bind [A B : choiceType] (m : C A) (f : A -> C B) :
-    eval {code bind m f} = Def.bind (eval m) (eval (A:=B) \o f).
+  Lemma eval_bind [A B : choiceType] (m : raw_code A) (f : A -> raw_code B) :
+    eval (bind m f) = Def.bind (eval m) (eval (A:=B) \o f).
   Proof.
-    case: m=> []; elim=> //=.
-    - move=> ??; rewrite Def.bind_ret /comp; f_equal.
-    - move=> o?? ih /inversion_valid_opr [oval kval].
-      rewrite 2!bool_depelim_true -Def.bind_bind; f_equal.
-      extensionality x; apply: ih; apply: kval.
-    - move=> l k ih /inversion_valid_getr [lval kval].
-      extensionality map; rewrite (ih _ (kval _)) //.
-    - move=> l c k ih /inversion_valid_putr [lval kval].
-      extensionality map; rewrite (ih kval) //.
-    - move=> [X sampleX] k ih /inversion_valid_sampler kval.
-      extensionality map. rewrite /Def.bind.
+    elim: m=> //=.
+    - move=> ?; rewrite Def.bind_ret /comp; f_equal.
+    - move=> o?? ih; rewrite -Def.bind_bind; apply: Def.bind_ext=> x; apply: ih.
+    - move=> l k ih; extensionality map; rewrite (ih _) //.
+    - move=> l c k ih; extensionality map; rewrite ih //.
+    - move=> [X sampleX] k ih; extensionality map. rewrite /Def.bind.
       apply: distr_ext=> z; rewrite dlet_dlet. do 2 f_equal.
-      extensionality x; rewrite (ih x _) //.
+      extensionality x; rewrite (ih x) //.
   Qed.
 
 
-  Lemma bind_rule [A B : choiceType] (m : C A) (f : A -> C B) prem postm pref postf:
+  Lemma bind_rule [A B : choiceType] (m : raw_code A) (f : A -> raw_code B) prem postm pref postf:
     ⊨ ⦃ prem ⦄ m ⦃ p, postm p ⦄ ->
     (forall a, ⊨ ⦃ pref a ⦄ f a ⦃ p, postf a p ⦄) ->
     ⊨ ⦃ bind_pre prem postm pref ⦄ bind m f ⦃ p, bind_post postm postf p ⦄.
@@ -395,7 +320,7 @@ Section Evaluation.
   Lemma weaken_rule
         [A : choiceType]
         [pre wkpre : precondition]
-        (c : C A)
+        (c : raw_code A)
         [post wkpost : postcondition A] :
     subpred wkpre pre ->
     subpred post wkpost ->
@@ -410,3 +335,29 @@ Section Evaluation.
   (* To continue: get rule, put rule, sampling rule, rule for imported operations ? *)
 
 End Evaluation.
+
+
+Section ScopedImportEval.
+  #[local] Open Scope fset.
+  #[local] Open Scope fset_scope.
+
+  #[local]
+  Notation M := (Def.stsubdistr heap_choiceType).
+
+  Context (import : Interface).
+
+  (** Taking an interpretation of the imported operation as assumption *)
+  Context (import_eval : ∀ o, o \in import → src o → M (tgt o)).
+
+  Definition eval_op : forall o, src o -> M (tgt o) :=
+    fun o => bool_depelim _ (o \in import) (fun oval => import_eval o oval) (fun _ _ => Def.stsubnull _ _).
+
+  Let eval := (eval eval_op).
+
+  (* Problem: the notation for the judgement is parametrized by eval, how can I
+  have access to this notation instantiated with eval without redefining it ?
+  Use a functor ?*)
+
+  (* TODO: Add spec and Rule for imported operations *)
+
+End ScopedImportEval.