fix: reject a pHL bound read in another memory by call / rnd

src/phl/ecPhlCall.ml

@@ -311,6 +311,23 @@ let t_bdhoare_call fpre fpost opt_bd tc =
   let bhs_po = ss_inv_rebind (bhs_po bhs) m in
   let bhs_pr = ss_inv_rebind (bhs_pr bhs) m in
 
+  (* The bound of the specification of the called procedure (the bound of
+     the conclusion, or [opt_bd]) is interpreted in the memory the procedure
+     starts from: after [s], and with the local variables of the callee.
+     The bound of the conclusion is interpreted in the initial memory, with
+     the local variables of the caller. The two coincide only if this bound
+     depends neither on local variables nor on variables written by [s]. *)
+  let callee_bd = odfl bhs_bd opt_bd in
+  let fv_bd = PV.fv env callee_bd.m callee_bd.inv in
+
+  if List.exists (fun (pv, _) -> is_loc pv) (fst (PV.elements fv_bd)) then
+    tc_error !!tc "The bound cannot depend on local variables";
+
+  if not (PV.indep env (s_write env s) fv_bd) then
+    tc_error !!tc
+      "The bound cannot depend on variables written by the \
+       statements preceding the call";
+
   (* The function satisfies the specification *)
   let f_concl =
     bdhoare_call_spec !!tc fpre fpost f bhs.bhs_cmp bhs_bd opt_bd in

src/phl/ecPhlRnd.ml

@@ -270,6 +270,16 @@ module Core = struct
           let concl = f_forall_simpl binders concl in
           FApi.xmutate1 tc `Rnd [concl]
       | PMultRndParams ((phi,d1,d2,d3,d4),event), _ ->
+        (* [d2] and [d4] are interpreted after [s] in [sgoal2] and [sgoal4],
+           and in the initial memory in [bd_sgoal]: the two coincide only if
+           [s] does not write them. *)
+        List.iter (fun (d : ss_inv) ->
+          if not (PV.indep env (s_write env s) (PV.fv env d.m d.inv)) then
+            tc_error !!tc
+              "The bounds on the probability of the sampling (third and \
+               fifth arguments) cannot depend on variables written by the \
+               statements preceding the sampling")
+          [d2; d4];
         let event = match event ty_distr with
           | None -> {m;inv=mk_event ~simpl:false ty_distr} | Some event -> event
         in

tests/phoare-call-prefix-bound.ec

@@ -0,0 +1,49 @@
+(* pHL `call` (upstream #1124): the bound of the conclusion is interpreted
+   in the initial memory, while the specification of the called procedure
+   interprets the same formula in the memory the procedure starts from,
+   i.e. after the statements preceding the call and with the local
+   variables of the callee. A bound that depends on variables written by
+   those statements, or on local variables, must be rejected. *)
+require import AllCore.
+
+module M = {
+  var x, y : bool
+
+  proc f() = { }
+
+  proc g() : bool = { var r; M.x <- true; r <@ f(); return true; }
+
+  proc h() : bool = { var r; M.x <- true; r <@ f(); return M.y; }
+}.
+
+(* The bound `b2r M.x` is 0 initially, but 1 when `f` is called; the
+   judgment is false (`M.g` returns `true`). *)
+lemma bad : phoare[M.g : !M.x ==> res] <= (b2r M.x).
+proof.
+proc.
+fail call (_ : M.x ==> true).
+abort.
+
+module N = {
+  proc f(x : bool) : bool = { return x; }
+  proc g(x : bool) : bool = { var r; r <@ f(!x); return r; }
+}.
+
+(* The local `x` of `N.g` would be read as the argument `x` of `N.f`; the
+   judgment is false for `x = false`. *)
+lemma bad' : phoare[N.g : true ==> res] <= (b2r x).
+proof.
+proc.
+fail call (_ : true ==> res).
+abort.
+
+(* A bound on a global variable that the prefix does not write is fine. *)
+lemma ok : phoare[M.h : true ==> res] <= (b2r M.y).
+proof.
+proc.
+call (_ : true ==> M.y).
++ proc; case (M.y).
+  + by conseq (: _ ==> true : <= 1%r) => [/#|]; auto.
+  by conseq (: _ ==> _ : <= 0%r) => [/#|]; hoare; auto.
+by auto.
+qed.

tests/phoare-rnd-prefix-bound.ec

@@ -0,0 +1,36 @@
+(* pHL `rnd phi d1 d2 d3 d4` (upstream #1124): `phi => mu d E <= d2` and
+   `!phi => mu d E <= d4` are checked after the statements preceding the
+   sampling, while `d1 * d2 + d3 * d4 <= bd` is checked in the initial
+   memory. Bounds `d2` and `d4` that depend on variables written by those
+   statements must be rejected. *)
+require import AllCore Distr.
+
+module M = {
+  proc f(x : bool) : bool = { var b; x <- true; b <$ dunit true; return b; }
+}.
+
+(* `d2 = b2r x` is 0 initially, but 1 at the sampling; the judgment is
+   false for `x = false` (`M.f` returns `true`). *)
+lemma bad : phoare[M.f : !x ==> res] <= (b2r x).
+proof.
+proc.
+fail rnd x 1%r (b2r x) 0%r 1%r.
+fail rnd (!x) 0%r 1%r 1%r (b2r x).
+abort.
+
+module N = {
+  proc f(x : bool) : bool = { var b, y; y <- true; b <$ dunit x; return b; }
+}.
+
+(* Bounds that the prefix does not write are fine. *)
+lemma ok : phoare[N.f : true ==> res] <= (b2r x).
+proof.
+proc.
+rnd true 1%r (b2r x) 0%r 0%r.
++ by move=> &hr; smt().
++ by auto.
++ by move=> &hr _; rewrite dunitE.
++ by hoare; auto.
++ by move=> &hr.
++ by move=> &hr; smt().
+qed.