From 12a2ed1b83d5e6f064e28d9933d20ec54e78261c Mon Sep 17 00:00:00 2001 From: Cameron Low Date: Mon, 20 Jan 2025 17:18:45 +0000 Subject: [PATCH] Improve transitivity* and replace* --- examples/ChaChaPoly/chacha_poly.ec | 4 +- src/phl/ecPhlOutline.ml | 90 +------------- src/phl/ecPhlOutline.mli | 2 - src/phl/ecPhlRwEquiv.ml | 2 +- src/phl/ecPhlTrans.ml | 191 +++++++++++++++++++---------- src/phl/ecPhlTrans.mli | 5 + theories/crypto/PROM.ec | 4 +- 7 files changed, 136 insertions(+), 162 deletions(-) diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec index 6478ebfd68..da96991394 100644 --- 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 index 6774ad118b..177cb96227 100644 --- 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 index ceb4116364..1b70326984 100644 --- 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 index 3e38064377..767138a3a2 100644 --- 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 index 542568568e..6bf9d99102 100644 --- 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 index 014e30796f..f113703fec 100644 --- 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 index 714fb1024b..ac4907b8f7 100644 --- 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].