Improve transitivity* and replace*

EasyCrypt · Jan 20, 2025 · 12a2ed1 · 12a2ed1
1 parent 39ed501
commit 12a2ed1
Show file tree

Hide file tree

Showing 7 changed files with 136 additions and 162 deletions.
diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec
@@ -1123,8 +1123,8 @@ section PROOFS.
     ={glob A} ==> ={res, Mem.lc} /\ StLSke.gs{1} = RO.m{2}.
   proof.
     proc *.
-    transitivity*{1} { r <@ G3(StLSke(St)).main(); } => //; 1:smt(); 1: by sim.
-    transitivity* {2} { r <@ G3(OChaChaPoly(IFinRO)).main(); } => //; 1:smt().
+    transitivity* {1} { r <@ G3(StLSke(St)).main(); }; 1: by sim.
+    transitivity* {2} { r <@ G3(OChaChaPoly(IFinRO)).main(); }.
     + inline *; wp.
       call (_: StLSke.gs{1} = OCC.gs{2} /\ ={Mem.k, Mem.log, Mem.lc}).
       + by proc; inline *; auto => /> &2; case: (p{2}).

diff --git a/src/phl/ecPhlOutline.ml b/src/phl/ecPhlOutline.ml
@@ -8,96 +8,8 @@ open EcUnifyProc
 
 open EcCoreGoal
 open EcCoreGoal.FApi
-open EcLowGoal
 open EcLowPhlGoal
 
-(*---------------------------------------------------------------------------------------*)
-(*
-   Transitivity star with (ideally) lossless pre-conditions over the intermediate
-   programs, and automatic discharging of the first two goals.
-*)
-(* FIXME: Move to ecPhlTrans *)
-
-let t_equivS_trans_eq side s tc =
-  let env = tc1_env tc in
-  let es = tc1_as_equivS tc in
-  let c,m = match side with `Left -> es.es_sl, es.es_ml | `Right -> es.es_sr, es.es_mr in
-
-  let mem_pre = split_sided (EcMemory.memory m) es.es_pr in
-  let fv_pr  = EcPV.PV.fv env (EcMemory.memory m) es.es_pr in
-  let fv_po  = EcPV.PV.fv env (fst m) es.es_po in
-  let fv_r = EcPV.s_read env c in
-  let mk_eqs fv =
-    let vfv, gfv = EcPV.PV.elements fv in
-    let veq = List.map (fun (x,ty) -> f_eq (f_pvar x ty mleft) (f_pvar x ty mright)) vfv in
-    let geq = List.map (fun mp -> f_eqglob mp mleft mp mright) gfv in
-    f_ands (veq @ geq) in
-  let pre = mk_eqs (EcPV.PV.union (EcPV.PV.union fv_pr fv_po) fv_r) in
-  let pre = f_and pre (odfl f_true mem_pre) in
-  let post = mk_eqs fv_po in
-  let c1, c2 =
-    if side = `Left then (pre, post), (es.es_pr, es.es_po)
-    else (es.es_pr, es.es_po), (pre, post)
-  in
-
-  let exists_subtac (tc : tcenv1) =
-    (* Ideally these are guaranteed fresh *)
-    let pl = EcIdent.create "&p__1" in
-    let pr = EcIdent.create "&p__2" in
-    let h  = EcIdent.create "__" in
-    let tc = t_intros_i_1 [pl; pr; h] tc in
-    let goal = tc1_goal tc in
-
-    let p = match side with | `Left -> pl | `Right -> pr in
-    let b = match side with | `Left -> true | `Right -> false in
-
-    let handle_exists () =
-      (* Pairing up the correct variables for the exists intro *)
-      let vs, fm = EcFol.destr_exists goal in
-      let eqs_pre, _ =
-        let l, r = EcFol.destr_and fm in
-        if b then l, r else r, l
-      in
-      let eqs, _ = destr_and eqs_pre in
-      let eqs = destr_ands ~deep:false eqs in
-      let doit eq =
-        let l, r = destr_eq eq in
-        let l, r = if b then r, l else l, r in
-        let v = EcFol.destr_local l in
-        v, r
-      in
-      let eqs = List.map doit eqs in
-      let exvs =
-        List.map
-          (fun (id, _) ->
-            let v = List.assoc id eqs in
-            Fsubst.f_subst_mem (EcMemory.memory m) p v)
-          vs
-      in
-
-      as_tcenv1 (t_exists_intro_s (List.map paformula exvs) tc)
-    in
-
-    let tc =
-      if EcFol.is_exists goal then
-        handle_exists ()
-      else
-        tc
-    in
-
-    t_seq
-      (t_generalize_hyp ?clear:(Some `Yes) h)
-      EcHiGoal.process_done
-      tc
-  in
-
-  let tc = t_seqsub
-             (EcPhlTrans.t_equivS_trans (EcMemory.memtype m, s) c1 c2)
-             [exists_subtac; EcHiGoal.process_done; t_id; t_id]
-             tc
-  in
-  tc
-
 (*---------------------------------------------------------------------------------------*)
 (*
    This is the improved transitivity star from above but allows for a range of code
@@ -121,7 +33,7 @@ let t_outline_stmt side start_pos end_pos s tc =
   let code_pref, _, _ = s_split_i env start_pos (stmt rest) in
 
   let new_prog = s_seq (s_seq (stmt code_pref) s) (stmt code_suff) in
-  let tc = t_equivS_trans_eq side new_prog tc in
+  let tc = EcPhlTrans.t_equivS_trans_eq side new_prog tc in
 
   (* The middle goal, showing equivalence with the replaced code, ideally solves. *)
   let tp = match side with | `Left -> 1 | `Right -> 2 in

diff --git a/src/phl/ecPhlOutline.mli b/src/phl/ecPhlOutline.mli
@@ -4,8 +4,6 @@ open EcParsetree
 open EcModules
 open EcPath
 
-val t_equivS_trans_eq : side -> stmt -> backward
-
 val t_outline_stmt : side -> codepos1 -> codepos1 -> stmt -> backward
 val t_outline_proc : side -> codepos1 -> codepos1 -> xpath -> lvalue option -> backward
 

diff --git a/src/phl/ecPhlRwEquiv.ml b/src/phl/ecPhlRwEquiv.ml
@@ -71,7 +71,7 @@ let t_rewrite_equiv side dir cp (equiv : equivF) equiv_pt rargslv tc =
   let prog = s_call (rlv, new_func, rargs) in
   let prog = s_seq prefix (s_seq prog suffix) in
 
-  let tc = EcPhlOutline.t_equivS_trans_eq side prog tc in
+  let tc = EcPhlTrans.t_equivS_trans_eq side prog tc in
 
   (* One of the goals can be simplified, often fully, using the provided equiv *)
   let tp = match side with | `Left -> 1 | `Right -> 2 in

diff --git a/src/phl/ecPhlTrans.ml b/src/phl/ecPhlTrans.ml
@@ -82,85 +82,144 @@ let t_equivS_trans = FApi.t_low3 "equiv-trans" Low.t_equivS_trans_r
 let t_equivF_trans = FApi.t_low3 "equiv-trans" Low.t_equivF_trans_r
 
 (* -------------------------------------------------------------------- *)
-let process_replace_stmt s p c p1 q1 p2 q2 tc =
+let t_equivS_trans_eq side s tc =
+  let env = FApi.tc1_env tc in
   let es = tc1_as_equivS tc in
-  let ct = match s with `Left -> es.es_sl | `Right -> es.es_sr in
-  let mt = snd (match s with `Left -> es.es_ml | `Right -> es.es_mr) in
-  (* Translation of the stmt *)
-  let regexpstmt = trans_block p in
-  let map = match RegexpStmt.search regexpstmt ct.s_node with
-    | None -> Mstr.empty
-    | Some m -> m in
-  let c = TTC.tc1_process_prhl_stmt tc s ~map c in
-  t_equivS_trans (mt, c) (p1, q1) (p2, q2) tc
+  let c, m = match side with `Left -> es.es_sl, es.es_ml | `Right -> es.es_sr, es.es_mr in
+
+  let mem_pre = EcFol.split_sided (EcMemory.memory m) es.es_pr in
+  let fv_pr  = EcPV.PV.fv env (EcMemory.memory m) es.es_pr in
+  let fv_po  = EcPV.PV.fv env (fst m) es.es_po in
+  let fv_r = EcPV.s_read env c in
+  let mk_eqs fv =
+    let vfv, gfv = EcPV.PV.elements fv in
+    let veq = List.map (fun (x,ty) -> f_eq (f_pvar x ty mleft) (f_pvar x ty mright)) vfv in
+    let geq = List.map (fun mp -> f_eqglob mp mleft mp mright) gfv in
+    f_ands (veq @ geq) in
+  let pre = mk_eqs (EcPV.PV.union (EcPV.PV.union fv_pr fv_po) fv_r) in
+  let pre = f_and pre (odfl f_true mem_pre) in
+  let post = mk_eqs fv_po in
+  let c1, c2 =
+    if side = `Left then (pre, post), (es.es_pr, es.es_po)
+    else (es.es_pr, es.es_po), (pre, post)
+  in
+
+  let exists_subtac (tc : tcenv1) =
+    (* Ideally these are guaranteed fresh *)
+    let pl = EcIdent.create "&p__1" in
+    let pr = EcIdent.create "&p__2" in
+    let h  = EcIdent.create "__" in
+    let tc = EcLowGoal.t_intros_i_1 [pl; pr; h] tc in
+    let goal = FApi.tc1_goal tc in
+
+    let p = match side with | `Left -> pl | `Right -> pr in
+    let b = match side with | `Left -> true | `Right -> false in
+
+    let handle_exists () =
+      (* Pairing up the correct variables for the exists intro *)
+      let vs, fm = EcFol.destr_exists goal in
+      let eqs_pre, _ =
+        let l, r = EcFol.destr_and fm in
+        if b then l, r else r, l
+      in
+      let eqs, _ = destr_and eqs_pre in
+      let eqs = destr_ands ~deep:false eqs in
+      let doit eq =
+        let l, r = EcFol.destr_eq eq in
+        let l, r = if b then r, l else l, r in
+        let v = EcFol.destr_local l in
+        v, r
+      in
+      let eqs = List.map doit eqs in
+      let exvs =
+        List.map
+          (fun (id, _) ->
+            let v = List.assoc id eqs in
+            Fsubst.f_subst_mem (EcMemory.memory m) p v)
+          vs
+      in
+
+      FApi.as_tcenv1 (EcLowGoal.t_exists_intro_s (List.map paformula exvs) tc)
+    in
+
+    let tc =
+      if EcFol.is_exists goal then
+        handle_exists ()
+      else
+        tc
+    in
+
+    FApi.t_seq
+      (EcLowGoal.t_generalize_hyp ?clear:(Some `Yes) h)
+      EcHiGoal.process_done
+      tc
+  in
+
+  FApi.t_seqsub
+    (t_equivS_trans (EcMemory.memtype m, s) c1 c2)
+    [exists_subtac; EcHiGoal.process_done; EcLowGoal.t_id; EcLowGoal.t_id]
+    tc
 
 (* -------------------------------------------------------------------- *)
-let process_trans_stmt s c p1 q1 p2 q2 tc =
+let process_trans_stmt tf s ?pat c tc =
+  let hyps = FApi.tc1_hyps tc in
   let es = tc1_as_equivS tc in
   let mt = snd (match s with `Left -> es.es_ml | `Right -> es.es_mr) in
+
   (* Translation of the stmt *)
-  let c = TTC.tc1_process_prhl_stmt tc s c in
-  t_equivS_trans (mt,c) (p1, q1) (p2, q2) tc
+  let map =
+    match pat with
+    | None -> Mstr.empty
+    | Some p -> begin
+      let regexpstmt = trans_block p in
+      let ct = match s with `Left -> es.es_sl | `Right -> es.es_sr in
+      match RegexpStmt.search regexpstmt ct.s_node with
+      | None -> Mstr.empty
+      | Some m -> m
+    end
+  in
+  let c = TTC.tc1_process_prhl_stmt tc s ~map c in
+
+  match tf with
+  | TFeq ->
+      t_equivS_trans_eq s c tc
+  | TFform (p1, q1, p2, q2) ->
+    let p1, q1 =
+      let hyps = LDecl.push_all [es.es_ml; (mright, mt)] hyps in
+      TTC.pf_process_form !!tc hyps tbool p1, TTC.pf_process_form !!tc hyps tbool q1
+    in
+    let p2, q2 =
+      let hyps = LDecl.push_all [(mleft, mt); es.es_mr] hyps in
+      TTC.pf_process_form !!tc hyps tbool p2, TTC.pf_process_form !!tc hyps tbool q2
+    in
+    t_equivS_trans (mt, c) (p1, q1) (p2, q2) tc
 
 (* -------------------------------------------------------------------- *)
 let process_trans_fun f p1 q1 p2 q2 tc =
-  let env = FApi.tc1_env tc in
+  let env, hyps, _ = FApi.tc1_eflat tc in
+  let ef = tc1_as_equivF tc in
   let f = EcTyping.trans_gamepath env f in
+  let (_, prmt), (_, pomt) = Fun.hoareF_memenv f env in
+  let (prml, prmr), (poml, pomr) = Fun.equivF_memenv ef.ef_fl ef.ef_fr env in
+  let process ml mr fo =
+    TTC.pf_process_form !!tc (LDecl.push_all [ml; mr] hyps) tbool fo in
+  let p1 = process prml (mright, prmt) p1 in
+  let q1 = process poml (mright, pomt) q1 in
+  let p2 = process (mleft,prmt) prmr p2 in
+  let q2 = process (mleft,pomt) pomr q2 in
   t_equivF_trans f (p1, q1) (p2, q2) tc
 
 (* -------------------------------------------------------------------- *)
 let process_equiv_trans (tk, tf) tc =
-  let env, hyps, _ = FApi.tc1_eflat tc in
-
-  let (p1, q1, p2, q2) =
+  match tk with
+  | TKfun f -> begin
     match tf with
-    | TFform(p1, q1, p2, q2) ->
-      begin match tk with
-      | TKfun f ->
-        let ef = tc1_as_equivF tc in
-        let f = EcTyping.trans_gamepath env f in
-        let (_, prmt), (_, pomt) = Fun.hoareF_memenv f env in
-        let (prml, prmr), (poml, pomr) = Fun.equivF_memenv ef.ef_fl ef.ef_fr env in
-        let process ml mr fo =
-          TTC.pf_process_form !!tc (LDecl.push_all [ml; mr] hyps) tbool fo in
-        let p1 = process prml (mright, prmt) p1 in
-        let q1 = process poml (mright, pomt) q1 in
-        let p2 = process (mleft,prmt) prmr p2 in
-        let q2 = process (mleft,pomt) pomr q2 in
-        (p1,q1,p2,q2)
-      | TKstmt (s, _) | TKparsedStmt (s, _, _) ->
-         let es = tc1_as_equivS tc in
-         let mt = snd (match s with `Left -> es.es_ml | `Right -> es.es_mr) in
-         let p1, q1 =
-           let hyps = LDecl.push_all [es.es_ml; (mright, mt)] hyps in
-           TTC.pf_process_form !!tc hyps tbool p1,
-           TTC.pf_process_form !!tc hyps tbool q1 in
-         let p2, q2 =
-           let hyps = LDecl.push_all [(mleft, mt); es.es_mr] hyps in
-           TTC.pf_process_form !!tc hyps tbool p2,
-           TTC.pf_process_form !!tc hyps tbool q2 in
-         (p1,q1,p2,q2)
-      end
     | TFeq ->
-      let side =
-        match tk with
-        | TKfun _ -> tc_error !!tc "transitivity * does not work on functions"
-        | TKstmt(s,_) ->  s
-        | TKparsedStmt(s,_,_) -> s in
-      let es = tc1_as_equivS tc in
-      let c,m = match side with `Left -> es.es_sl, es.es_ml | `Right -> es.es_sr, es.es_mr in
-      let fv  = EcPV.PV.fv env (fst m) es.es_po in
-      let fvr = EcPV.s_read env c in
-      let mk_eqs fv =
-        let vfv, gfv = EcPV.PV.elements fv in
-        let veq = List.map (fun (x,ty) -> f_eq (f_pvar x ty mleft) (f_pvar x ty mright)) vfv in
-        let geq = List.map (fun mp -> f_eqglob mp mleft mp mright) gfv in
-        f_ands (veq @ geq) in
-      let pre = mk_eqs (EcPV.PV.union fvr fv) in
-      let post = mk_eqs fv in
-      if side = `Left then (pre, post, es.es_pr, es.es_po)
-      else (es.es_pr, es.es_po, pre, post) in
-  match tk with
-  | TKfun f -> process_trans_fun f p1 q1 p2 q2 tc
-  | TKstmt (s, c) -> process_trans_stmt s c p1 q1 p2 q2 tc
-  | TKparsedStmt (s, p, c) -> process_replace_stmt s p c p1 q1 p2 q2 tc
+      tc_error !!tc "transitivity * does not work on functions"
+    | TFform (p1, q1, p2, q2) ->
+      process_trans_fun f p1 q1 p2 q2 tc
+  end
+  | TKstmt (side, stmt) ->
+    process_trans_stmt tf side stmt tc
+  | TKparsedStmt (side, pat, stmt) ->
+    process_trans_stmt tf side ~pat:pat stmt tc
diff --git a/src/phl/ecPhlTrans.mli b/src/phl/ecPhlTrans.mli
@@ -32,6 +32,11 @@ val t_equivF_trans :
   -> EcFol.form * EcFol.form
   -> EcCoreGoal.FApi.backward
 
+(*---------------------------------------------------------------------------------------*)
+(* Completely change the code of `side` *)
+val t_equivS_trans_eq :
+  side -> EcModules.stmt -> EcCoreGoal.FApi.backward
+
 (* -------------------------------------------------------------------- *)
 val process_equiv_trans :
   trans_kind * trans_formula -> backward
diff --git a/theories/crypto/PROM.ec b/theories/crypto/PROM.ec
@@ -918,7 +918,7 @@ equiv RO_FinRO_D : MainD(D,RO).distinguish ~ MainD(D,FinRO).distinguish :
   ={glob D, arg} ==> ={res, glob D}.
 proof.
   proc *.
-  transitivity*{1} {r <@ MainD(D, GenFinRO(LRO)).distinguish(x); } => //;1:smt().
+  transitivity*{1} {r <@ MainD(D, GenFinRO(LRO)).distinguish(x); }.
   + inline MainD(D, RO).distinguish MainD(D, GenFinRO(LRO)).distinguish; wp.
     call (_: ={glob RO});2..4: by sim.
     + by apply RO_LFinRO_init.
@@ -989,7 +989,7 @@ proc.
 transitivity*{2} {
   Vars.r <@ S.sample(dout,FinFrom.enum);
   FunRO.f <- tofun Vars.r;
-}; 1,2: smt(); last first.
+}; last first.
 - inline*; rnd : *0 *0; skip => />.
   by split => *; rewrite dmap_id dfun_dmap.
 rewrite equiv[{2} 1 Sample_Loop_first_eq].