fix phl while rule

EasyCrypt · Jul 22, 2022 · 3cd9c5d · 3cd9c5d
1 parent 4d79575
commit 3cd9c5d
Show file tree

Hide file tree

Showing 4 changed files with 32 additions and 9 deletions.
diff --git a/examples/PIR.ec b/examples/PIR.ec
@@ -201,8 +201,12 @@ proof.
     + by apply fsetP=> z;rewrite /restr !inE mem_oflist mem_iota /#.
   conseq (_ : _ ==> oflist PIR.s = restr x j) (_: _ ==> j = N) => //;1:smt().
   + while(0 <= j <= N);auto;smt (N_pos).
-  while (0 <= j <= N /\ is_restr (oflist PIR.s) j) (N-j) N 1%r; 2,3:smt(N_pos).
-  + by move=> &hr /> _;rewrite -set0E N_pos /=; apply is_restr_fset0.
+  conseq (: (0 <= j <= N /\ is_restr (oflist PIR.s) j) ==> _) => //.
+  + move=> />; smt(N_pos set0E is_restr_fset0).
+  while (0 <= j <= N /\ is_restr (oflist PIR.s) j) (N-j) N 1%r => //.
+  + move=> /> s j *; have ->>: j = N by smt(). 
+    by rewrite subzz expr0. 
+  + smt(N_pos).
   + move=> H.
     case (oflist PIR.s = restr x j);first last.
     + seq 3 : true _ 0%r 0%r _ (0 <= j <= N /\ is_restr (oflist PIR.s) j /\ oflist PIR.s <> restr x j).
@@ -251,8 +255,12 @@ proof.
     + by apply fsetP=> z;rewrite /restr !inE mem_oflist mem_iota /#.
   conseq (_ : _ ==> oflist PIR.s' = restr x j) (_: _ ==> j = N) => //;1:smt().
   + while(0 <= j <= N);auto;smt (N_pos).
-  while (0 <= j <= N /\ is_restr (oflist PIR.s') j) (N-j) N 1%r;2,3:smt(N_pos).
-  + by move=> &hr /> _;rewrite -set0E N_pos /=; apply is_restr_fset0.
+  conseq (: (0 <= j <= N /\ is_restr (oflist PIR.s') j) ==> _). 
+  + move=> />; smt(N_pos set0E is_restr_fset0).
+  while (0 <= j <= N /\ is_restr (oflist PIR.s') j) (N-j) N 1%r => //.
+  + move=> /> s j *; have ->>: j = N by smt(). 
+    by rewrite subzz expr0. 
+  + smt(N_pos).
   + move=> H.
     case (oflist PIR.s' = restr x j);first last.
     + seq 3 : true _ 0%r 0%r _ (0 <= j <= N /\ is_restr (oflist PIR.s') j /\ oflist PIR.s' <> restr x j).

diff --git a/examples/vonNeumann.eca b/examples/vonNeumann.eca
@@ -90,6 +90,7 @@ have ->:
   by proc; rnd (pred1 x \o fst); skip=> />.
 byphoare (_: true ==> res = x)=> //; proc; sp.
 conseq (: _: =(if b = b' then mu dvn (pred1 x \o fst) else b2r (b = x)))=> //.
+conseq (: true ==> _).
 while true (b2i (b = b')) 1 (2%r * p * (1%r - p))=> />.
 + by move=> /#.
 + move=> ih.

diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml
@@ -136,6 +136,7 @@ let t_choare_while_r inv qdec n (lam_cost : cost) tc =
 
 
 (* -------------------------------------------------------------------- *)
+(* rule >=, <=, =, with a stricly decreasing variant *)
 let t_bdhoare_while_r inv vrnt tc =
   let env = FApi.tc1_env tc in
   let bhs = tc1_as_bdhoareS tc in
@@ -167,6 +168,7 @@ let t_bdhoare_while_r inv vrnt tc =
   FApi.xmutate1 tc `While [b_concl; concl]
 
 (* -------------------------------------------------------------------- *)
+(* Rule for <= *)
 let t_bdhoare_while_rev_r inv tc =
   let env, hyps, _ = FApi.tc1_eflat tc in
   let bhs = tc1_as_bdhoareS tc in
@@ -211,10 +213,16 @@ let t_bdhoare_while_rev_r inv tc =
   FApi.xmutate1_hyps tc `While [(hyps', body_concl); (hyps, rem_concl)]
 
 (* -------------------------------------------------------------------- *)
+(* Rule for = or >= *)
+
 let t_bdhoare_while_rev_geq_r inv vrnt k eps tc =
   let env, hyps, _ = FApi.tc1_eflat tc in
 
   let bhs    = tc1_as_bdhoareS tc in
+
+  if bhs.bhs_cmp = FHle then
+    tc_error !!tc "only judgments with an lower/eq-bounded are supported";
+
   let b_pre  = bhs.bhs_pr in
   let b_post = bhs.bhs_po in
   let mem    = bhs.bhs_m in
@@ -233,8 +241,12 @@ let t_bdhoare_while_rev_geq_r inv vrnt k eps tc =
 
   (* 2. Pre-bound *)
   let pre_bound_concl =
-    let term_post = [b_pre; f_not lp_guard; f_not b_post] in
-    let term_post = f_imps term_post (f_eq bound f_r0) in
+    let term_post = [b_pre; f_not lp_guard] in
+    let concl =
+      if bhs.bhs_cmp = FHeq then
+        f_eq bound (f_if b_post f_r1 f_r0)
+      else f_imp (f_not b_post) (f_eq bound f_r0) in
+    let term_post = f_imps term_post concl in
     let term_post = generalize_mod env (EcMemory.memory mem) modi term_post in
       f_forall_mems [mem] term_post
   in
@@ -283,9 +295,9 @@ let t_bdhoare_while_rev_geq_r inv vrnt k eps tc =
     let while_s1 = EcModules.stmt [EcModules.i_abstract w] in
 
     let unfolded_while_s = EcModules.s_seq lp_body while_s1 in
-    let while_jgmt = f_bdHoareS_r { bhs with bhs_pr=inv; bhs_s=while_s1; } in
+    let while_jgmt = f_bdHoareS_r { bhs with bhs_pr=b_pre; bhs_s=while_s1; } in
     let unfolded_while_jgmt = f_bdHoareS_r
-      { bhs with bhs_pr=f_and inv lp_guard; bhs_s=unfolded_while_s; }
+      { bhs with bhs_pr=f_and b_pre lp_guard; bhs_s=unfolded_while_s; }
     in
     f_imp while_jgmt unfolded_while_jgmt
   in

diff --git a/theories/distributions/Dexcepted.ec b/theories/distributions/Dexcepted.ec
@@ -298,8 +298,10 @@ case @[ambient]: (mu (dt x) (X x) = weight (dt x))=> Hpt.
   by rewrite Hpt.
 conseq (: _: =(if X x r then mu (dt x \ X x) P else b2r (P r))).
 + by move=> />; rewrite y_in_Xx.
+conseq (_ : i = x /\ test = X ==> _) => //.
 while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x)))=> //=.
 + smt().
++ smt().
 + move=> ih. alias 2 r0 = r.
   (** TRANSITIVITY FOR PHOARE!! **)
   phoare split (mu (dt x) (predI P (predC (X x))))
@@ -310,7 +312,7 @@ while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x))
     rewrite -(@divrr (weight (dt x) - mu (dt x) (X x))).
     + smt().
     rewrite mulrA mulrA -mulrDl; congr.
-    by rewrite mulrDr mulrC mulrN (mulrC (_ _ (X x))) subrK dt_ll. (* dt_ll *)
+    by rewrite mulrDr mulrC mulrN (mulrC (_ _ (X x))) subrK dt_ll. 
   + seq  2: (P r0 /\ !X x r0)
             (mu (dt x) (predI P (predC (X x)))) 1%r
                                               _ 0%r